Formele verificatie: wiskundig bewijs dat software doet wat ze moet doen
Stel je voor dat je een brug wilt bouwen. Je zou nooit accepteren dat een ingenieur zegt: "we hebben hem honderd keer belast met een vrachtwagen en hij stortte niet in, dus het zit wel snor." Je wilt een wiskundige berekening zien die aantoont dat de brug elke belasting binnen de ontwerpgrenzen aankan. Formele verificatie doet voor software en computerchips wat die berekening doet voor een brug: het levert een wiskundig bewijs dat een systeem zich exact gedraagt zoals bedoeld, in plaats van alleen "het werkte in de gevallen die we hebben getest."
De meeste software wordt vandaag gecontroleerd door te testen: programmeurs bedenken een aantal situaties, draaien het programma en kijken of de uitkomst klopt. Dat werkt goed voor veelvoorkomende fouten, maar een test kan nooit alle mogelijke situaties afdekken. Formele verificatie probeert dat gat te dichten door met logica en wiskunde te bewijzen dat een programma voor alle mogelijke invoer aan zijn specificatie voldoet, niet alleen voor de gevallen die iemand toevallig heeft geprobeerd.
Wat is het precies?
Formele verificatie begint met een specificatie: een precieze, wiskundige beschrijving van wat een systeem wel en niet mag doen. Bijvoorbeeld: "twee treinen mogen nooit tegelijk op hetzelfde spoorsegment staan" of "deze functie geeft altijd een gesorteerde lijst terug". Zo'n specificatie wordt geschreven in een formele, wiskundig eenduidige taal, niet in gewone spreektaal die voor meerdere uitleg vatbaar is.
Daarna volgt het eigenlijke bewijs, en daarvoor bestaan grofweg twee benaderingen. De eerste is modelcontrole (model checking): een computerprogramma doorzoekt automatisch alle mogelijke toestanden waarin een systeem kan verkeren en controleert of de specificatie in elke toestand klopt. Dit werkt goed voor systemen met een beperkt, overzichtelijk aantal toestanden, zoals een verkeersregelalgoritme of een stuk chiplogica.
De tweede benadering is het gebruik van een stellingbewijzer (theorem prover of proof assistant), zoals Coq, Isabelle/HOL of het nieuwere Lean. Hierbij formuleert een mens een wiskundige stelling ("dit programma stort nooit vast") en bouwt vervolgens, stap voor stap, een bewijs op dat de computer controleert op logische fouten. De computer rekent dus niet zelf een bewijs uit zoals bij modelcontrole, maar checkt of een door mensen bedacht bewijs waterdicht is. Dat is precies werk, dat kan maanden tot jaren duren voor een complex systeem.
Een verwante tool is TLA+, ontwikkeld door informaticus Leslie Lamport. Daarmee beschrijf je niet zozeer code, maar het gedrag van een systeem over tijd, wat het bijzonder geschikt maakt voor gedistribueerde systemen: meerdere computers die met elkaar moeten samenwerken en waarbij dingen tegelijkertijd of in onverwachte volgorde kunnen gebeuren.
Wat wil men ermee bereiken?
Het hoofddoel is simpel te formuleren: bepaalde categorieën fouten volledig uitsluiten, in plaats van ze alleen minder waarschijnlijk te maken. Voor gewone consumentensoftware is een crash vervelend. Maar voor de software die een vliegtuig, een kerncentrale, een pacemaker of het banksysteem aanstuurt, kan een enkele fout levens kosten of enorme financiële schade veroorzaken. Formele verificatie wil in die gevallen een garantie geven die verder gaat dan "we hebben ons best gedaan om te testen".
Een tweede doel is het vinden van fouten die mensen nooit zouden bedenken om te testen: extreem zeldzame combinaties van omstandigheden, race conditions (waarbij de uitkomst afhangt van de precieze timing tussen processen) of grensgevallen die pas na jaren in productie aan het licht komen. Een formeel bewijs dekt per definitie alle gevallen, dus ook de gevallen die niemand had voorzien.
Tot slot speelt ook vertrouwen een rol. Bij cryptografische software bijvoorbeeld, wil je niet alleen dat een encryptie-algoritme correct is geïmplementeerd, maar kunnen aantonen dát het correct is, zodat gebruikers en toezichthouders dat kunnen controleren zonder blind op de leverancier te moeten vertrouwen.
Voorbeelden uit de praktijk
Het bekendste voorbeeld is seL4, een microkernel (de kleine kern van een besturingssysteem die de basisfuncties zoals geheugenbeheer regelt). Onderzoekers van het Australische instituut NICTA (tegenwoordig onderdeel van Data61/CSIRO) leverden in 2009 het eerste volledige wiskundige bewijs dat een besturingssysteemkern precies doet wat zijn specificatie voorschrijft, inclusief de afwezigheid van crashes en bufferoverloop. seL4 wordt sindsdien gebruikt in veiligheidskritische toepassingen zoals defensie- en luchtvaartsystemen.
Een vergelijkbaar project is CompCert, een C-compiler (een programma dat broncode omzet naar machinecode) ontwikkeld sinds 2008 door Xavier Leroy en collega's bij het Franse onderzoeksinstituut INRIA. CompCert is zelf bewezen correct in de stellingbewijzer Coq: de kans dat de compiler zelf een fout introduceert die niet in de oorspronkelijke broncode zat, is daardoor wiskundig uitgesloten voor het geverifieerde deel van de vertaling.
Ook buiten de softwarewereld is formele verificatie al decennia in gebruik. Voor de automatische, bestuurderloze metrolijn 14 in Parijs (bekend als Météor, geopend in 1998) gebruikten Matra en de vervoerder RATP de zogeheten B-methode om de besturingssoftware van de treinen formeel te verifiëren, nog voordat de term "formele verificatie" gangbaar was buiten academische kringen.
In de commerciële clouddiensten paste Amazon Web Services vanaf begin jaren 2010 TLA+ toe om kernonderdelen van diensten als S3 (opslag) en DynamoDB (database) te modelleren en te controleren op ontwerpfouten, nog voordat er een regel code werd geschreven. Amazon heeft in eigen technische publicaties uitgelegd dat deze aanpak subtiele fouten in gedistribueerde protocollen aan het licht bracht die met testen alleen waarschijnlijk niet gevonden waren.
In de chipindustrie kreeg formele verificatie een grote impuls na de beruchte Pentium FDIV-bug van 1994, waarbij een rekenfout in de deelfunctie van Intels Pentium-processor tot een kostbare terugroepactie leidde. Sindsdien investeren Intel en AMD zwaar in formele verificatietechnieken om te bewijzen dat de rekenkundige eenheden in hun processoren geen soortgelijke fouten bevatten.
Hoe ver is de techniek?
Formele verificatie is geen toekomstmuziek, het bestaat al sinds de jaren zeventig en tachtig van de vorige eeuw en wordt vandaag operationeel ingezet. Toch blijft het een niche in vergelijking met de totale hoeveelheid software die wereldwijd wordt geschreven. Het grootste obstakel is schaal: een volledig formeel bewijs voor seL4 kostte destijds naar schatting meerdere mensjaren werk voor een kernel van maar enkele tienduizenden regels code. De meeste besturingssystemen en applicaties zijn vele malen groter, wat volledige verificatie op dit moment onbetaalbaar of praktisch onhaalbaar maakt.
Een tweede beperking is dat een bewijs alleen zo goed is als de specificatie waarmee het vergeleken wordt. Als de specificatie zelf een fout of omissie bevat, bijvoorbeeld omdat een ontwerper een scenario over het hoofd zag, dan bewijst formele verificatie keurig dat het systeem voldoet aan een onvolledige of foute beschrijving. Het correct opstellen van specificaties blijft mensenwerk en foutgevoelig.
Daarnaast vraagt het vak gespecialiseerde kennis van wiskundige logica die weinig reguliere software-ontwikkelaars bezitten, wat de bredere toepassing afremt. Om die reden zien we formele verificatie vooral terug in nauw afgebakende niches waar de kosten van een fout torenhoog zijn: lucht- en ruimtevaart, spoorwegbeveiliging, chipontwerp, cryptografische bibliotheken en de kernonderdelen van besturingssystemen en compilers. Voor gewone apps, websites en de meeste bedrijfssoftware blijft testen, code review en typecontrole door programmeertalen de dominante en meest praktische aanpak.
De laatste jaren neemt de belangstelling wel toe, mede dankzij snellere computers, betere gereedschappen zoals Lean en Dafny, en groeiende zorgen over cyberveiligheid en de betrouwbaarheid van AI-systemen. Sommige onderzoekers experimenteren zelfs met AI-modellen die meehelpen bewijzen te genereren, al staat dat onderzoek nog in een pril stadium en vervangt het de menselijke expertise vooralsnog niet.
Wie werken eraan?
Frankrijk speelt een vooraanstaande rol via het onderzoeksinstituut INRIA, waar onder meer de stellingbewijzer Coq en de CompCert-compiler zijn ontwikkeld. In het Verenigd Koninkrijk heeft de University of Cambridge een lange traditie in formele methoden, terwijl het Australische Data61 (voortgekomen uit NICTA) wereldwijd bekend staat om het seL4-project.
In de Verenigde Staten investeert Microsoft Research in gereedschappen als Lean, Dafny en F*, en past het bedrijf Amazon via AWS TLA+ toe op zijn cloud-infrastructuur. Het gespecialiseerde bedrijf Galois Inc. ontwikkelt formeel geverifieerde software voor veiligheidskritische en defensieve toepassingen, vaak in opdracht van Amerikaanse overheidsinstanties.
In de halfgeleiderindustrie zetten Intel, AMD en ARM formele verificatietechnieken in om chipontwerpen te controleren voordat ze in productie gaan, omdat een fout in silicium achteraf vrijwel niet meer te herstellen is. Verder werken tal van universiteiten wereldwijd, waaronder in Duitsland (TU München) en de Verenigde Staten (onder meer Carnegie Mellon University en MIT), mee aan de ontwikkeling van nieuwe bewijsmethoden en -gereedschappen.