Nu steeds vaker allerlei digitale inbraken en overvallen worden gemeld, gecombineerd met de nog steeds toenemende digitalisering van de maatschappij doet zich de vraag voor hoe we van die ellende af kunnen komen. Dat schijnt te kunnen stelt het Amerikaanse  Quanta Magazine, met wat zij ‘formele verificatie’ noemt; een programmeermethode die sluitend is als een wiskundig bewijs en ik daarom aanduid met wiskundige programmeren. Die programmeerwijze zou foutloze programmatuur opleveren. E-krakers en ander digitaal geboefte maken meestal juist gebruik van fouten in de code. Die gaan moeilijke tijden tegemoet

Zomer vorig jaar probeerde  een groepje e-krakers (gelegitimeerd) een onbemande militaire helicopter (Little Bird) te kapen. Dat ding lijkt op zijn bemande evenknie die de Amerikanen lange tijd gebruikt hebben voor speciale operaties. Het werd de krakers niet al te moeilijk gemaakt: ze hadden al toegang tot het computersysteem van de helicopter. Het enige wat ze moesten doen de boordcomputer te kraken en dan was de droon van hun.
Dat bleek een koud kunstje, maar technici van de legeronderzoekorganisatie DARPA ontwikkelden vervolgens een nieuw beveiligingssysteem dat niet zou kunnen worden overgenomen. De groep krakers kregen zes weken en meer toegang tot het computernetwerk dan onverlaten ooit zouden krijgen, maar het lukte hen niet door het nieuwe verdedigingsmechanisme van Little Bird heen te breken. “Op geen enkele manier”, zegt informatica Kathleen Fisher van de Tufts-universiteit. “De mensen bij DARPA gingen geloven dat ze een technologie in handen hadden die ze konden gebruiken bij systemen waar het er om gaat.”

Wiskundig programmeren

De programmeertechniek waar het hierbij om gaat is, zoals verklapt de formele verificatie of, in mijn woorden, wiskundig programmeren. De meeste computercode wordt, een beetje populair gezegd, uit de losse pols geschreven. Daarbij gaat het er om of die werkt. Dat is het criterium, niet of die code foutloos is. Bij wiskundig programmeren volgt elke regel code logisch op de voorgaande als in een wiskundig bewijs. Het hele programma kan worden getest met de zekerheid waarmee wiskundigen stellingen bewijzen.
Deze manier van programmeren bestaat al bijna zo lang als de informatica bestaat. Lange tijd waren de middelen er niet de formele verificatie in de praktijk te brengen, maar daarin is inmiddels het een en ander veranderd. Vandaag de dag is wiskundig programmeren in de buurt van de hanteerbare praktijk gekomen, zeker voor grote ondernemingen of organisaties als Microsoft of het Amerikaanse leger.
De noodzaak om code zonder fouten te produceren groeit ook naarmate de wereld steeds meer verknoopt en gedigitaliseerd raakt. Als er in de tijd voor het wereldwijde web fouten in de code zaten dan was dat vervelend, want dat kon je dat programma (soms) niet gebruiken of moest je het vaak opnieuw openen. Nu zijn die fouten het doelwit van krakers, waarmee ze computernetwerken kunnen binnendringen of -systemen kunnen overnemen.
“Een formele specificatie of doelstelling bedenken dat een machine kan lezen is nogal lastig”, zegt Bryan Parno van Microsoft research. “Het is makkelijk om op hoger niveau te zeggen ‘Geef mijn wachtwoord niet weg”, maar om dat in wiskundige termen te vertalen vergt wat denkwerk.” Het is lastig een idee te vertalen in een formele specificatie dat alle niet-bedoelde interpretaties uitsluit.
Hoe moet je, bijvoorbeeld, een wachtwoord beschermen? Parno: “Dan moet je dus een wiskundige omschrijving geven van wat het betekent om iets geheim te houden of wat het betekent voor een versleutelingsalgoritme om echt veilig te zijn. Dat zijn allemaal problemen waarmee wij en vele anderen hebben geworsteld en waarbij we vooruitgang hebben geboekt.”
Dat heeft lang geduurd. Zelfs de pioniers van het wiskundige programmeren zoals Tony Hoare leken de moed te verliezen. In 1995 zei Hoare: “Tien jaar geleden dachten we dat de programmeerwereld de formalisering zou omarmen, maar het lijkt er nu op dat de wereld niet erg lijdt onder het probleem dat we wilden oplossen.”

Internet

Internet heeft dat allemaal veranderd. Fouten werd kansen voor krakers. Tegen de tijd dat dat besef doordrong stond wiskundig programmeren weer in de startblokken. Het gereedschap dat de wiskundige programmeurs daarbij terzijde kon staan was inmiddels gegroeid.
De formele codeschrijvers matigden ook hun doelen. In de jaren 70 en 80 streefden ze naar volledig geverifieerde systemen, van het het geïntegreerde circuit tot de programma’s. Nu concentreren formele programmeurs zich op belangrijke onderdelen van een systeem zoals een besturingssysteem of versleutelingsprotocollen.
Bij het HACMS-project werkt, onder meer, Fisher aan de uiterste beveiliging van militaire systemen. Daarin wordt aangetoond dat je een hoge mate van beveiliging kunt creëren door een deel van het systeem formeel te programmeren. Het eerste doel was een onkraakbare droon te ontwerpen. Daar schijnen ze al weer twee jaar mee bezig te zijn, waarbij de architectuur van de gebruikte software ook onderhanden wordt genomen, zodat er een soort ‘onkraakbare’ bouwstenen ontstonden. Die verbouwde programmatuur werd later voor Little Bird gebruikt en ook in andere systemen toegepast zoals satellieten en zelfrijdende vrachtwagens.

Zo langzamerhand worden er steeds ambitieuzere projecten aangepakt. Zo wordt er gewerkt aan het onneembaar maken van een webserver. Microsoft Research is aan twee ambitieuze projecten bezig. Het ene, Everest genaamd, moet een absoluut veilige internetverbinding creëren (https). Het tweede project moet systemen als droons of zelfrijdende auto’s veiliger maken. Dat is een fikse klus, waar, om het allemaal wat moeilijker te maken, ook nog een kusntmatige intelligentie een complicerende rol in speelt. Het is misschien nog wat voorzichtig, maar wiskundig programmeren lijkt eindelijk zijn draai gevonden te hebben.

Bron: Quanta Magazine