Karthik Bhargavan:…bewezen veilig …

Programmeren is mensenwerk, maar de wiskunde is onverslaanbaar. Als je het programmeren wiskundiger zou maken zou je daarmee voorkomen dat er fouten in de code sluipen die kunnen worden misbruikt door e-krakers en veiligheidsdiensten, denken informatici. Een stap in die richting is de manier waarop de kryptobieb EverCrypt is ontwikkeld. De onderzoekers die daaraan gewerkt hebben konden bewijzen dat hun code geheel ongevoelig is voor de belangrijkste webaanvallen die in het verleden slachtoffers hebben gemaakt. “Als we zeggen bewijs dan bedoelen we dat onze code geen last heeft van zulke aanvallen”, zegt Karthik Bhargavan, een informaticus die in Parijs bij Inria werkt. Dat zou moeten smaken naar meer.
Evercrypt is niet geschreven zoals de meeste code. Normaal ontwikkelt een team de protuur waarvan ze hopen dat die voldoet aan bepaalde doelen. Als het programma klaar is dan wordt dat getest. Als dat voldoet aan de eisen en geen ongewenst gedrag vertoont dan is het okee. Programmeerfouten vindt je vaak in duistere hoeken en gaten, vaak bij een onwaarschijnlijke, maar daarom niet onmogelijke, samenloop. Veel webaanvallen de laatste jaren maakten misbruik van dergelijke onvoorzienbare samenlopen.
“Het is een kettingreactie en die fouten zijn moeilijk op een systematische manier te vinden omdat die elk op zich erg onwaarschijnlijk zijn” zegt medeontwikkelaar Bryan Parno werkzaam bij de Carnegie Mellon-universiteit.
Parno en zijn medeontwikkelaars hebben vooraf precies gespecificeerd wat hun code moet doen en bewezen toen dat die code ook alleen maar dat doet: geen onverwachte zijpaadjes, geen wilde samenlopen. Dat heet dan ‘formele verificatie’. Parno: “Je kunt de vraag hoe een programma zich gedraagt omzetten in een wiskundige formule en je kunt dan controleren of die formule overeind blijft. Als dat zo is dan heeft de code die eigenschap.”

Omdat het vrijwel onmogelijk is de functie van zoiets ingewikkelds als een webprogramma formeel te specificeren, hebben de onderzoekers zich gericht op programma’s die wel te hanteren zijn en wiskundig kunnen worden beschreven. EverCrypt is een softwearebibliotheek voor kryptografie, het versleutelen en ontsleutelen van gevoelige informatie. Deze bibliotheken zijn op zichzelf al heel wiskundig gestructureerd. We praten dan over priemgetallen en operaties van wiskundige functies zoals ellipsen. Het is een eitje om daarvan de functie formeel te omschrijven.
Het werk aan EverCrypt begon in 2016 als onderdeel van het Project Everest van Microsoft Research. Toen en ook nu nog vormden kryptografische bibliotheken een zwakke plek in vele toepassingen. Ze draaiden traag en zaten vol fouten. “Ik denk dat ontwikkelaars beseften dat er een ramp op til stond”, zegt Jonathan Protzenko die bij Microsoft Research aan EverCrypt heeft gewerkt. “De softwarewereld is rijp voor iets nieuws dat waarborgen geeft.”

Ontwikkelplatform

De belangrijkste hobbel om EverCrypt foutvrij te ontwikkelen was het creëren van een programmeringsplatform dat in staat was al de dingen te doen die nodig waren voor een kryptobieb. Dat moest de capaciteit hebben van een traditionele ontwikkeltaal zoals C++ en de logische opbouw en structuur van een ondersteuningsprogramma zoals Isabelle en Coq die wiskundigen al jaren gebruiken.
Zo’n alles-in-eenplatform was er niet, dus begonnen de ontwikkelaars maar met het creëren van een nieuwe programmeertaal F*.  Daarmee zouden wiskunde en programmeren op hetzelfde niveau zijn gebracht. “We hebben deze dingen samengebracht in een coherent raamwerk zodat het onderscheid tussen programmeren en bewijzen sterk is teruggebracht”, zegt Bhargavan. “Je kan programmeren als een ontwikkelaar maar tezelfdertijd een bewijs leveren als een wiskundige.”

De nieuwe kryptobieb geeft een aantal veiligheidswaarborgen. De onderzoekers bewezen dat EverCrypt geen fouten in de code bevat, die aanvallen mogelijk maken. Ze bewezen ook dat bij EverCrypt de versleuteling in orde is. De belangrijkste waarborg is echter dat een aanvaller ook niet achter de versleutelde inhoud kan komen door te kijken hoe het programma werkt. Bhargavan: “Ergens diep in je algoritme of in de wijze waarop het algoritme wordt uitgevoerd lek je informatie waardoor het hele idee van versleuteling zinloos wordt.” Dat soort ‘zijaanvallen’ deden zich voor bij een bekende kraakoperatie als Lucky Thirteen. Dat zal EverCrypt nooit gebeuren, bewezen de onderzoekers.
Het zwakke punt blijft natuurlijk dat je kunt bewijzen dat iets werkt tegen aanval A, B of C die bekend zijn, maar dat je niet weet hoe dat werkt tegen een nog onbekende aanval X. Daar bij komt dat ook een ‘intrinsiek veilig’ programma vaak samenwerkt met allerlei andere programma’s. Het is dan net zoals bij de beveiliging van je huis. Die is zo goed als de zwakste schakel. Protzenko: “We werken niet aan zoiets complex als een tekstverwerker of een telefoontoepassing als Skype. Het is moeilijk om over het bedoelde gedrag van zoiets na te denken.”

Omdat ‘aanpalende’ programma’s de kryptobieb kunnen ‘dwarszitten’ wordt er binnen Project Everest bij voorkeur gewerkt met geverifieerde programma’s. Het overkoepelend idee is om HTTPS volledig geverifieerd te krijgen. Dan heb je het over een stuk of zes onderdelen zoals EverCrypt, die allemaal formeel als veilig moeten worden bewezen. Parno: “Binnen project Everest proberen we programma’s te ontwikkelen die alle geverifieerd zijn ook als ze met elkaar werken. Met de tijd groeit die geverifieerde programmatuur, hopen we.”

Bron: Quanta Magazine