Papers we love: statische analyses op code uitvoeren

De paper die ik deze maand in het zonnetje wil zitten is er een uit het jaar 2000. Hij heet “Checking system rules using system-specific, programmer-written compiler extensions” en is te downloaden . Dit paper beschrijft een systeem om eenvoudig en efficiënt statische analyses uit te kunnen voeren van een stuk software. De auteurs stellen dat “meta-level compilation” gebruikt kan worden om op een eenvoudige manier systeem-specifieke regels vast te leggen en als automatisch controlemiddel toe te passen om de kwaliteit van software te kunnen verhogen.

Een compiler heeft veel technisch specifieke kennis is, bijvoorbeeld over het typesystem van een programmeertaal. Deze is hierdoor in staat om zaken als typefouten zoals int != string eenvoudig te signaleren, al zijn er natuurlijk ook complexere variaties op mogelijk. Persoonlijk vind ik dit bijvoorbeeld erg fijn, hiermee minimaliseer je duidelijk je feedbackloop tijdens het schrijven van code. In de paper stelt men echter dat de wat domein-specifiekere zaken lastiger automatisch te controleren zijn. Een van de voorbeelden die ze beschrijven is er een uit de Linux kernel. In sommige stukken van de code moet men interrupts uit kunnen zetten, maar het wordt in sommige executiepaden weleens vergeten weer terug aan te zetten. Dit kan bijvoorbeeld doordat er een early exit uit een functie is waarbij men vergeten is de handler weer aan te zetten. De bijdrage van deze paper is dat men een manier beschrijft om in een DSL, gebaseerd op de oorspronkelijke taal die de compiler aan het verwerken is, abstracte testcondities vast te leggen.

In de DSL, Metal genoemd, geeft men op een declaratieve manier aan wat voor state transities er mogelijk zijn binnen de te controleren code. Om hetzelfde voorbeeld te hanteren: als men begint met het uitschakelen van de interrupt handler dan verwacht ik dat hij daarna wordt ingeschakeld of dat zijn oorspronkelijke configuratie wordt hersteld. Deze condities worden op een vrij abstracte manier gespecificeerd, waarbij de transities worden herkend aan de hand van patronen die in de regeldefinitie worden opgegeven. Als er na analyse van de code blijkt dat er paden mogelijk zijn die de state machine een ongeldige transitie uit laten voeren, wordt de code aangewezen als mogelijk defect. Dit signaal kan de engineer vervolgens gebruiken om een gerichte analyse te doen van de code.

Het mooie van dit soort analyses is dat het een crossover is tussen de formele specificaties en de meer (unit)testing achtige aanpakken. Formele specificaties hebben het probleem dat ze een enorme leercurve en tijdsdrempel kennen om op te stellen. Daarnaast kun je je afvragen of een formele specificatie hetzelfde zal zeggen als de daadwerkelijke code zou moeten doen. De talen waarin je aan het werk bent verschillen dusdanig veel van elkaar dat dit ook erg lastig is om te vergelijken. De testing-hoek heeft dan weer het probleem dat je combinatorisch in de problemen kunt komen wat betreft het aantal testpaden dat je af dient te lopen. Daarnaast is het in sommige domeinen lastig om alles echt goed te testen omdat je afhankelijkheden hebt op bijvoorbeeld hardware. In het geval van een kernel die met een interrupt handler, device driver of memory allocator bezig is kunnen we ons daar allemaal wel wat bij indenken vermoed ik.

Een van de fijne dingen van deze paper is dat hij heel erg gemakkelijk te lezen is. De hoeveelheid voorkennis die vereist wordt om een goed beeld te krijgen is vrij laag en daarnaast is het technisch inhoudelijk een dusdanig andere aanpak dan je normaliter hebt bij het definiëren van testen dat je je goed kunt indenken dat hier een duidelijke waarde van is. De directe toepasbaarheid is wellicht wat minder, maar dat neemt niet weg dat een mooie kans biedt om hier toch leuke dingen van op te steken. Ook zijn de besproken technieken de basis zijn van het bedrijf Coverity, een grote commerciële jongen die klanten als Microsoft, Nasa en RSA als klant heeft. Het bedrijf is opgericht nadat men van de universiteit is vertrokken en verdient momenteel nog steeds zijn geld met statische analyse van software. In nederland vinden dit soort spinoffs ook plaats, een van de bekendste hiervan is het bedrijf SIG (Software Improvement Group). Dit bedrijf is in Amsterdam opgericht en houdt zich tot vandaag de dag ook nog bezig met vraagstukken omtrent software kwaliteit en analyse.

De paper geeft een heel uitgebreide studie weer naar hoe effectief de controlemiddelen zijn, welke klasse fouten goed worden opgespoord maar ook wanneer dit juist niet zo is. Er wordt een heel gebalanceerd totaalplaatje neergezet, wat duidelijk vanaf een praktische wens tot een verbeterslag is opgebouwd tot een (in mijn ogen) erg goed onderzoek. Wat mij betreft is het dan ook echt een aanrader om deze paper even door te nemen!


Over deze Papers we Love: binnen Sogyo hebben we de traditie dat we maandelijks een nieuwsbrief rondsturen. De nieuwsbrief gaat veel over interne feitjes, echter sinds februari 2015 verzorgd Kevin van der Vlist het topic: papers we love. Hij deelt met ons papers die interessant zijn om te lezen en ons kunnen inspireren. De topic is uitgegroeid tot een mooie verzameling die we ook graag hier willen delen.