Het idee werd al bestudeerd door de Nederlandse computerpionier Edsger Dijkstra, die zich in de jaren 70 stortte op het concept dat we nu kennen als formal verification. Daarbij wordt een programma/opdracht als 'true' (en dus authentiek) aangemerkt aan de hand van wiskundig bewijs. De logica van de statement wordt aan de hand daarvan geverifieerd voordat hij wordt uitgevoerd en dat zou een foutloos programma moeten opleveren.

Drone niet te kapen

Militair onderzoeksinstituut DARPA stort zich al jaren op zulke concepten in de hoop software te maken die vrijgewaard is van malafide inmenging. Dit is onder meer getest met een drone waarop een heleboel hackers werden losgelaten die de drone moesten kapen. Dat lukte ze in 2015 niet en dat geeft het instituut hoop dat het proces werkt, schrijft Quanta Magazine in een zeer lezenswaardig artikel.

DARPA gaf een Red Team zes weken de tijd om zich voor te bereiden op het kapen van een onbemande helikopter. Zelfs met de resources die DARPA beschikbaar stelde, lukte het de aanvallers in die tijd niet om de drone over te nemen. Dat geeft DARPA hoop dat deze methode werkt.

Aanvalsbestendig

Formal verification wordt in de praktijk nauwelijks gebruikt in de softwaresector, omdat het behoorlijk wat werk vereist - en een stevig begrip van abstracte wiskunde - en vooral omdat de baten (hoe erg is het nou dat software een keertje crasht) niet opwegen tegen die kosten. Dat laatste is aan het veranderen doordat kritieke systemen bestendig moeten zijn tegen aanvallen.