Modulaire halfautomatische formele verificatie van kritische systeemsoftware

In het eerste deel van deze thesis voeren we een case study uit waarin we het USB BP toetsenbordstuurprogramma van Linux verifiëren. Onze verificatieaanpak is (a) sound, (b) ondersteunt dynamische geheugentoewijzing, complexe API regels en concurrency, en (c) is toegepast op een echt kernelstuurprogramma waarbij de makers van dat stuurprogramma geen rekening hielden met verificatie toen dat stuurprogramma geschreven werd. We gebruiken VeriFast, een programma voor programmaverificatie gebaseerd op separation logic. We tonen niet enkel aan dat het mogelijk is om zulk een apparaatstuurprogramma te verifiëren, maar we identificeren ook de delen waar verificatie vlot verliep en die waarbij verder onderzoek welkom is om de verificatieaanpak te verbeteren.

In het tweede deel van de thesis stellen we een verificatieaanpak voor die gebruik maakt van een manier van redeneren gebaseerd op het concept van invoer/uitvoer. Deze verificatieaanpak kan zowel toegepast worden op programma's die invoer/uitvoer doen, en programma's die dat niet doen en in plaats daarvan geheugen aanpassen. De verificatieaanpak is sound, modulair, compositioneel (invoer-/uitvoeracties kunnen gedefinieerd worden bovenop andere acties) en ondersteunt concurrency. Het gebruikt Petri netten en separation logic. We hebben de aanpak geïmplementeerd, zowel voor programma's die wel en die geen invoer/uitvoer doen, in VeriFast en geschetst hoe de verificatieaanpak kan geïmplementeerd worden in het raamwerk Iris.