Modulaire semiautomatische formele verificatie van veiligheidsgevoelige software

In onze steeds meer computergeoriënteerde samenleving, lijken de computer- programma’s waarop we vertrouwen altijd maar groter te worden in omvang en complexiteit. Omdat we bijna geen andere keuze meer hebben dan deze programma’s onze geheimen en privacy toe te vertrouwen, is het geranderen van softwarekwaliteit steeds belangrijker geworden. Er zijn ontelbare technieken ontwikkeld om de correctheid van veiligheidsgevoelige software te demonstreren en dit proefschrift breidt een van deze, namelijk formele verificatie, verder uit.

In het eerste deel van dit proefschrift presenteren we een aanpak om verschillende onderdelen van een programma afzonderlijk te verifiëren. Deze modulaire techniek noemen we symbolisch linken en hij vermindert de complexiteit van het verificatieprocess aanzienelijk voor grote stukken software. Wanneer een annotatiegebaseerd verificatieprogramma voor de C programeertaal zowel symbolisch linken als preprocessing ondersteunt, moet men erop letten dat dit niet tot een unsoundness leidt. De moeilijkheid is dat het resultaat van een headerexpansie afhangt van de gedefinieerde macro’s. Daarom presenteren we hier een preprocessingtechniek die sound is en we tonen aan dat de resulterende semantiek na typecontrole gelijk is aan die van de C standaard. We hebben deze preprocessingtechniek uitgewerkt in VeriFast; een op annotaties gebaseerd verificatieprogramma voor de C programeertaal die symbolisch linken ondersteunt. De eerste experimenten tonen aan dat de aangepaste preprocessor de meest gebruikelijke situaties de baas kan. Voor zover wij weten, zijn wij de eersten die het zowel modulair als sound verifiëren van geannoteerde C code ondersteunen.

In het tweede deel van dit proefschrift richten we ons op beveiligingskritieke software die gebruik maakt van cryptografische bewerkingen om bepaalde beveiligingsdoelen te verwezenlijken. Meer bepaald, we hebben het uigebreide symbolische model ontwikkeld wat een methode is om protocolimplementaties te verifiëren die geschreven zijn tegen een bestaande cryptografische API. We hebben dit model uitgewerkt in VeriFast en deze encodering ondersteunt het specificeren en controleren van integriteits- en vertrouwelijkheidseigenschappen van protocolimplementaties die gebruik maken van hashcodes, willekeurig waardes, (geauthenticeerde) symmetrische en asymmetrische encryptie. Als theoretische onderbouw voor deze encodering hebben we een eenvoudig programmeertaal bedacht met een correct bewijssysteem dat de meest interessante aspecten van de encodering bevat. Dit systeem heeft alle noodzakelijke componenten om integriteitseigenschappen te speciferen en bewijzen van protocollen.