De Radboud Universiteit Nijmegen heeft formele softwareverificatie toegepast in een aantal praktijkstudies. Hier beschrijven Marko van Eekelen en Sjaak Smetsers er twee: de Maeslantkering en de ook in veel grote industriële systemen gebruikte Qt-toolkit. De resultaten zijn verrassend.
Onze maatschappij is in grote mate afhankelijk van software. Kleine softwarehaperingen hebben vaak hooguit enige frustratie van de gebruiker tot gevolg. Dit verandert echter zodra we te maken hebben met applicaties waarbij grote financiële belangen spelen of de veiligheid van personen in het geding komt. Kenmerkend bij deze zogeheten safety-critical of industry-critical systemen is dat één enkele softwarefout desastreuze gevolgen kan hebben: gigantische financiële schade of zelfs verlies van mensenlevens.
Daarom gelden er hoge eisen voor de kwaliteit en veiligheid van deze systemen. Zo bestaat er een keur aan ontwikkelstandaarden en -technieken die moeten garanderen dat volgens de aangegeven richtlijnen gebouwde applicaties vrij zijn van softwarefouten. Niet zelden stellen ze eisen aan het ontwikkelproces, waarbij we elke stap zorgvuldig dienen te monitoren. De standaarden voor de diverse industriële sectoren vertonen onderling ook grote verschillen. Toch bestaat er consensus over de noodzaak om tijdens de ontwikkeling van safety-critical software formele methoden te gebruiken, waarmee de correctheid van zowel ontwerp als uiteindelijke realisatie van een (deel)systeem wiskundig is aan te tonen.
Aan de Radboud Universiteit hebben we een aantal bestaande systemen geanalyseerd met state-of-the-art formele technieken. Daarbij hebben we een methodiek gehanteerd die er onder meer op berust dat van een safety-critical systeem vaak slechts een klein deel ook daadwerkelijk veiligheidskritiek is. Het idee is om die kritieke kern te isoleren, er een formeel model van op te stellen en dit model vervolgens te verifiëren en mogelijk te verbeteren. Tot slot kunnen we vanuit het model weer code genereren die als vervanging dient voor de oorspronkelijke code. Vanwege de analogie met het werk van een chirurg in het ziekenhuis hebben we deze aanpak software surgery gedoopt.
Maeslant
We illustreren de methode aan de hand van twee praktijkstudies. De eerste hebben we uitgevoerd in opdracht van Rijkswaterstaat en gaat over de Maeslantkering. Dit was het eerste onderzoek van promovendus Ken Madlener. Zijn proefschrift getiteld ‘Formally verified modular semantics’ zal naar verwachting dit jaar verschijnen.
De Maeslantkering in de Nieuwe Waterweg bestaat uit twee enorme deuren die bij dreigend hoogwater gesloten kunnen worden. Bijzonder is dat een computersysteem bestaand uit tweehonderdduizend regels C++ automatisch beslist of en wanneer zo’n sluiting aan de orde is. Het doel van onze studie was om aan te tonen dat dit Beslis en Ondersteunend Systeem (BOS) correct functioneert.
Uit code-inspectie bleek dat de meest veiligheidskritieke component de ongeveer vierhonderd regels C++ tellende routine ‘BepaalPeilOverschrijding’ is. Op grond van prognoses van waterhoogtes schat deze in of het kritieke peil wel of niet zal worden overschreden. De deuren gaan dicht zodra de functie op korte termijn een waterstand hoger dan de norm verwacht. Dit gebeurt niet bij een kleine, korte overschrijding (Figuur 1).
Om het gedrag te analyseren, hebben we de C++-code eerst omgezet in een model gespecificeerd in Promela. Met deze formele taal zijn (combinaties van) modellen op te stellen voor zowel software- als hardwarecomponenten. Zo’n model kan vervolgens als invoer dienen voor de model-checker Spin, die dan specifieke eigenschappen kan controleren voor alle mogelijke toestanden die het systeem kan doorlopen. Uiteraard moet het aantal toestanden daarvoor wel eindig zijn. De gehele toestandsruimte doorlopen heeft als grote voordeel dat geen enkele fout onopgemerkt blijft.
De verificatie leverde op dat ons model van de code de laatste twee waarden van de voorspelling niet meenam. Dus als er aan het einde van het beslissingsvenster een peiloverschrijding werd verwacht, zou de routine (nog) niet tot een sluiting besluiten. Effectief betekende dit dat de sluitingsprocedure twee tijdsintervallen korter was dan bedoeld.
Essentieel voor model-checking is dat de toestandsruimte begrensd is. Voor dit systeem was dit niet het geval; het gebruikte model vormde dan ook een benadering van de oorspronkelijke softwarecomponent. Om volledige correctheid aan te kunnen tonen, hebben we de broncode vertaald naar PVS. Dit is een hulpmiddel voor de constructie van een correctheidsbewijs voor een gegeven eigenschap van een systeemmodel. Met PVS is een geconstrueerd bewijs volautomatisch te controleren. Nadeel is dat deze manier van eigenschappen bewijzen, theorem proving geheten, vaak bijzonder tijdrovend is, zelfs voor experts. Als gevolg hiervan is de techniek nauwelijks schaalbaar, wat het verifiëren van grotere systemen onrealistisch maakt.
De verificatie van de sluitingsroutine leverde het bewijs dat het model behorend bij de code inderdaad voldoet aan de specificatie van Rijkswaterstaat. Maar was deze zélf eigenlijk wel valide? Om de specs te valideren, hebben we Spin verschillende scenario’s laten genereren waarbij het systeem verschillende besluiten zou kunnen nemen. De ene keer sloot de kering niet, de andere keer veel te laat (Figuur 2).
De conclusie van Rijkswaterstaat was dat in deze scenario’s de specificatie inderdaad niet geheel de intentie van de ontwikkelaars dekte; de kering zou in beide gevallen (eerder) moeten sluiten. Gezien de uitzonderlijkheid van de gevallen en het feit dat er altijd iemand met de kering meekijkt om eventueel in te grijpen, waren de scenario’s niet direct bedreigend voor de veiligheid. Toch hebben alle bevindingen uiteindelijk tot revisies van zowel specificatie als software geleid.
Qt
Tweede voorbeeld is een casestudie waarin we de voorgestelde methodiek hebben getoetst aan de hand van de veelgebruikte Qt-toolkit. Deze softwarebibliotheek is niet op voorhand veiligheidskritiek, maar kan wel deel uitmaken van een safety-critical systeem. Concreet betrof het de verificatie van een bekend synchronisatiemechanisme voor concurrent threads. Het in 2013 gepubliceerde proefschrift van Leonard Lensink, ‘Applying formal methods in software development’, bevat drie artikelen die (in)direct uit deze casus voortkomen.
Het doel was om aan te tonen dat het synchronisatiemechanisme zowel deadlock- als starvation-vrij is, dus dat het enerzijds niet vastloopt door wederzijdse uitsluiting en anderzijds niet voor onbepaalde tijd verstoken blijft van cruciale resources. Net al bij de vorige studie hebben we de C++-broncode eerst vertaald naar een Promela-model. De verificatie hiervan leverde voor beide eigenschappen een negatief resultaat op: de software was noch deadlock- noch starvation-vrij. Dat was verrassend omdat veel grote, vrij bekende, industriële applicaties de bibliotheek gebruiken.
Een starvation-bug is gemakkelijk over het hoofd te zien. In tegenstelling tot deadlock is starvation geen toestand waaruit een executerende applicatie nooit meer kan ontsnappen; er is altijd een kans dat het probleem zich na verloop van tijd vanzelf oplost. Dit maakt bugs van deze categorie nagenoeg onvindbaar voor andere verificatietechnieken, zoals modelgebaseerd testen.
Na de opgespoorde fouten te hebben verholpen, hebben we de verbeterde software vertaald naar PVS. Hierin hebben we vervolgens een correctheidsbewijs geconstrueerd dat formeel aantoont dat de resulterende bibliotheek aan de gestelde eisen voldoet. Overigens heeft ook de oorspronkelijke ontwikkelaar van de software, Trolltech (nu via Nokia onderdeel van Microsoft), de nieuwste versie aangepast.
Proof patterns
Beide studies laten zien dat formele softwareverificatie met behulp van model-checking en theorem-proving in principe doenlijk is. De ontwikkeling van ondersteunende tools is nog steeds in volle gang. De complexiteit van de verificatie is vergroot door het besef dat naast functionele correctheid ook beveiliging van groot belang is. Dit laatste aspect is in het verleden vaak onderbelicht gebleven omdat producenten van software in eerste instantie weinig rekening neigen te houden met opzettelijk foutief gebruik. Deze verwaarlozing heeft ertoe geleid dat beveiligingslekken tegenwoordig een van de grootste bedreigingen vormen voor het correct en dus veilig functioneren van software.
Het grootste probleem van formele verificatie is nog steeds de schaalbaarheid. Om dit aan te pakken, willen we een methodiek ontwikkelen op basis van het correctness by design-principe, waarbij herbruikbaarheid centraal staat. De traditionele benadering om herbruikbaarheid te verkrijgen, is door objectgeoriënteerde technieken te gebruiken en daarmee bouwstenen te ontwikkelen met zorgvuldig afgebakende verantwoordelijkheden. Voor softwareverificatie is het van belang om behalve de software zelf ook de eigenschappen, de bewijstechnieken en zelfs de geconstrueerde bewijzen modulair op te zetten.
Hoe we dit exact kunnen vormgeven, is nog onduidelijk. Er bestaan voorstellen die zijn gebaseerd op design patterns. Deze zijn te gebruiken als structureringsmechanisme van software en leiden dan min of meer automatisch tot een modulaire structuur. Inmiddels is er een breed scala aan ontwerppatronen beschikbaar voor tal van toepassingsgebieden. Zo zijn er patronen om security-gerelateerde problemen aan te pakken en proof patterns voor het structureren van eigenschappen en bewijsmethodieken.
Ons onderzoek zal zich concentreren op de inzet van deze patronen tijdens het softwareontwikkelproces. Hiermee denken we niet alleen het verificatieproces te kunnen versnellen maar ook de toegepaste verificatiemethode herbruikbaar te maken voor andere systemen. Het ontwikkelproces willen we ondersteunen met een combinatie van bestaande tools, waaronder de model-checker Spin en theorem-prover PVS.
Onlangs is versie 6 van PVS uitgekomen, met een nieuwe mogelijkheid tot parametrisatie met types. Deze optie lijkt bij uitstek geschikt voor het generieke gebruik van proof patterns. Door de tool te koppelen aan Frama-C, een bestaand platform om verschillende toepassingsgerichte analyses van C-programma’s uit te voeren, kunnen we uit de PVS-modellen C-code genereren, die een gecertificeerde vertaler vervolgens omzet in een executeerbare, volledig gecertificeerde applicatie (Figuur 3).