< Terug naar vorige pagina
Project
Formalisation and Soundness of Static Verification Algorithms for Imperative Programs (Formalisatie en correctheid van statische verificatiealgoritmes voor imperatieve programma's)
Niet alleen wordt onze software alsmaar omvangrijker en complexer, we hangen er eveneens steeds meer van af, wat het des te noodzakelijker maakt hulpmiddelen te ontwikkelen om ons bij te staan bij het schrijven van correcte programma's. Bijgevolg werd veel onderzoek gevoerd in het domein van statische verificatie, d.i. het uitwerken van algoritmes dewelke broncode analyseren en uitmaken of het bepaalde types fouten bevat. Dit kan variëren van het nakijken dat er geen null dereferences</> gebeuren tijdens de uitvoering van het programma tot het verifiëren van volledige functionele correctheid.
Verificatiealgoritmes zijn echter eveneens onderhevig aan fouten. Daarom is het belangrijk om deze algoritmes nauwkeurig te onderzoeken: het vertrouwen dat we hebben in onze software kan niet sterker zijn dan dat in onze verificatiehulpmiddelen. In een eerste stap bekijken we verschillende benaderingen tot verificatie; meer in het bijzonder formaliseren we de algoritmes en bewijzen we hun correctheid.
Indien we niet bereid zijn onze software noch onze verificatiealgoritmes te vertrouwen, kunnen we ons afvragen waarom we onze formalisaties en correctheidsbewijzen wel zouden vertrouwen. Om deze reden implementeren we in een tweede stap alle door ons beschouwde verificatiealgoritmes in Coq en bieden we in de meeste gevallen ook machinaal nagekeken correctheidsbewijzen aan.
Deze thesis bestaat uit twee delen. In het eerste deel behandelen we het genereren van verificatiecondities. Dit houdtin dat we op basis van de broncode van een programma een logische formule genereren waarvan de validiteit impliceert dat het programma correct werkt ten opzichte van gegeven specificaties. We onderzoeken drie zulke algoritmes, namelijk de sterkste postconditie, de zwakste vrije preconditie en de zwakste preconditie.
Extra aandacht wordt besteed aan het zwakste preconditie algoritme. In zijn klassieke vorm genereert het een verificatieconditie die exponentieel groeit in de grootte van het programma. Er bestaat echter wel een alternatieve formulering die polynomiale verificatiecondities produceert, maar deze kan enkel gebruikt worden op passieve programma's, met andere woorden programma's die geen toekenningen bevatten. Het is gelukkig mogelijk om willekeurige programma's om te zetten naar een equivalente passieve vorm. We implementeren deze programmatransformatie samen met de efficiëntere vorm van het zwakste preconditie algoritme in Coq, waarna we machinaal bewijzen dat deze aanpak correctis.
In het tweede deel van de thesis behandelen we symbolische uitvoering. Dit bestaat erin om een programma op abstracte wijze te interpreten zodat alle uitvoeringspaden tegelijkertijd beschouwd worden. Verificatie slaagt indien men geen fouten tegenkomt tijdens deze uitvoering.
Op basis van deze techniek ontwerpen we Featherweight VeriFast, dewelke de kern voorstelt van VeriFast, een bestaand verificatieprogramma dat ontwikkeld wordt aan de KU Leuven. Featherweight Verifast wordt formeel gedefinieerd als een denotationele semantiek, maar vermits het geïmplementeerd werd in Coq en extraheerbaar is, is het eveneens bruikbaar als verificatieprogramma.
De formalisatie van Featherweight VeriFast steunt op drie abstractielagen. In een eerste laag definiëren we de resultatenalgebra. Deze laat ons toe te redeneren over demonisch en angeliek nondeterminisme, dewelke nodig zijn om de resultaten van symbolische uitvoeringuit te drukken. De tweede laag definieert operatoren: dit zijn samenstelbare monadische functies die ons toelaten om op elegante wijze om te gaan met de twee types nondeterminisme en bieden ons toestand aan binnen een zuiver functionele context. De derde laag definieert de basisoperatoren. Samen vormen deze een domeinspecifieke taal die de details van de resultatenalgebra wegabstraheert. De symbolische uitvoering, de centrale component van Featherweight VeriFast, wordt dan uitgedrukt in termen van deze basisoperatoren. We geven ook een (gedeeltelijk machinaal nagekeken) correctheidsbewijs van Featherweight VeriFast.
Het laatste hoofdstuk bespreekt verificatie-automatiseringstechnieken. Sommige verificatieprogramma's, waaronder VeriFast, vereisen dat de code geannoteerd wordt met bijvoorbeeld routinecontracten en lusinvarianten. Het automatisch genereren van deze annotaties kan de hoeveelheid werk dat nodig is om een programma te verifiëren drastisch doen afnemen. Om af te sluiten stellen we een algemeen kader voor dat het mogelijk maakt om nieuwe automatiseringstechnieken toe te voegen zonder daarbij de betrouwbaarheid van de verificatie in het gedrang te brengen.
Verificatiealgoritmes zijn echter eveneens onderhevig aan fouten. Daarom is het belangrijk om deze algoritmes nauwkeurig te onderzoeken: het vertrouwen dat we hebben in onze software kan niet sterker zijn dan dat in onze verificatiehulpmiddelen. In een eerste stap bekijken we verschillende benaderingen tot verificatie; meer in het bijzonder formaliseren we de algoritmes en bewijzen we hun correctheid.
Indien we niet bereid zijn onze software noch onze verificatiealgoritmes te vertrouwen, kunnen we ons afvragen waarom we onze formalisaties en correctheidsbewijzen wel zouden vertrouwen. Om deze reden implementeren we in een tweede stap alle door ons beschouwde verificatiealgoritmes in Coq en bieden we in de meeste gevallen ook machinaal nagekeken correctheidsbewijzen aan.
Deze thesis bestaat uit twee delen. In het eerste deel behandelen we het genereren van verificatiecondities. Dit houdtin dat we op basis van de broncode van een programma een logische formule genereren waarvan de validiteit impliceert dat het programma correct werkt ten opzichte van gegeven specificaties. We onderzoeken drie zulke algoritmes, namelijk de sterkste postconditie, de zwakste vrije preconditie en de zwakste preconditie.
Extra aandacht wordt besteed aan het zwakste preconditie algoritme. In zijn klassieke vorm genereert het een verificatieconditie die exponentieel groeit in de grootte van het programma. Er bestaat echter wel een alternatieve formulering die polynomiale verificatiecondities produceert, maar deze kan enkel gebruikt worden op passieve programma's, met andere woorden programma's die geen toekenningen bevatten. Het is gelukkig mogelijk om willekeurige programma's om te zetten naar een equivalente passieve vorm. We implementeren deze programmatransformatie samen met de efficiëntere vorm van het zwakste preconditie algoritme in Coq, waarna we machinaal bewijzen dat deze aanpak correctis.
In het tweede deel van de thesis behandelen we symbolische uitvoering. Dit bestaat erin om een programma op abstracte wijze te interpreten zodat alle uitvoeringspaden tegelijkertijd beschouwd worden. Verificatie slaagt indien men geen fouten tegenkomt tijdens deze uitvoering.
Op basis van deze techniek ontwerpen we Featherweight VeriFast, dewelke de kern voorstelt van VeriFast, een bestaand verificatieprogramma dat ontwikkeld wordt aan de KU Leuven. Featherweight Verifast wordt formeel gedefinieerd als een denotationele semantiek, maar vermits het geïmplementeerd werd in Coq en extraheerbaar is, is het eveneens bruikbaar als verificatieprogramma.
De formalisatie van Featherweight VeriFast steunt op drie abstractielagen. In een eerste laag definiëren we de resultatenalgebra. Deze laat ons toe te redeneren over demonisch en angeliek nondeterminisme, dewelke nodig zijn om de resultaten van symbolische uitvoeringuit te drukken. De tweede laag definieert operatoren: dit zijn samenstelbare monadische functies die ons toelaten om op elegante wijze om te gaan met de twee types nondeterminisme en bieden ons toestand aan binnen een zuiver functionele context. De derde laag definieert de basisoperatoren. Samen vormen deze een domeinspecifieke taal die de details van de resultatenalgebra wegabstraheert. De symbolische uitvoering, de centrale component van Featherweight VeriFast, wordt dan uitgedrukt in termen van deze basisoperatoren. We geven ook een (gedeeltelijk machinaal nagekeken) correctheidsbewijs van Featherweight VeriFast.
Het laatste hoofdstuk bespreekt verificatie-automatiseringstechnieken. Sommige verificatieprogramma's, waaronder VeriFast, vereisen dat de code geannoteerd wordt met bijvoorbeeld routinecontracten en lusinvarianten. Het automatisch genereren van deze annotaties kan de hoeveelheid werk dat nodig is om een programma te verifiëren drastisch doen afnemen. Om af te sluiten stellen we een algemeen kader voor dat het mogelijk maakt om nieuwe automatiseringstechnieken toe te voegen zonder daarbij de betrouwbaarheid van de verificatie in het gedrang te brengen.
Datum:5 feb 2008 → 13 dec 2012
Trefwoorden:Specific languages
Disciplines:Toegepaste wiskunde, Computerarchitectuur en -netwerken, Distributed computing, Informatiewetenschappen, Informatiesystemen, Programmeertalen, Scientific computing, Theoretische informatica, Visual computing, Andere informatie- en computerwetenschappen
Project type:PhD project