Gapend gat gedicht: Leidse promovendus ontdekt doorbraak in softwareveiligheid
Per toeval ontdekte computerwetenschapper Hans-Dieter Hiep (Leiden Institute of Advanced Computer Science en Centrum Wiskunde & Informatica) een ‘gapend gat’ in een veelgebruikte manier om de veiligheid van software te evalueren. Hiep dichtte het gat en zorgde daarmee voor aardig wat opschudding in zijn vakgebied. ‘Het is niet leuk als een Leidse promovendus even komt vertellen dat een twintig jaar oud bewijssysteem niet klopt.’ Hiep promoveerde 23 mei cum laude.
‘Kleine programmeerfoutjes kunnen grote gevolgen hebben,’ vertelt Hiep. ‘Vooral als dat foutje precies in het stukje software zit dat ons werkgeheugen behandelt en beschermt.’ Deze systemen zorgen er bijvoorbeeld voor dat gebruikers zonder gevaar tijdelijk geheugen met elkaar kunnen uitwisselen. Hiep: ‘Zit er een fout in zo’n besturingssysteem, dan kun je zomaar een datalek krijgen en ligt alles op straat. Fouten in de beveiliging van het geheugen zijn de grootste veroorzaker van veelvoorkomende kwetsbaarheden en lekken.’
Dat dit soort bugs een bedreiging voor de digitale veiligheid zijn, bewijst ook een persbericht van het Witte Huis van afgelopen februari. Daarin roept het de wetenschappelijke gemeenschap op om met oplossingen te komen om dit ‘hardnekkige probleem op te lossen.’
Bugs in software elimineren
Hiep houdt zich bezig met programmacorrectheid, oftewel: het elimineren van bugs in software. ‘Dit vakgebied is inmiddels alweer vijftig jaar oud’, vertelt hij. ‘Ik richt me op de correctheid van zogenaamde pointer programma’s. Dat zijn programma’s die werken met een geheugen dat adresseerbaar is met behulp van pointers: daartoe behoren nagenoeg alle programma’s van vandaag de dag.’
'Als fabrikant moet je eerst kunnen aantonen dat jouw printer geen gevaar is voor de systemen van Microsoft.'
Al twintig jaar bestaat er een methode om te bewijzen dat er geen bugs in dat soort pointerprogramma’s zitten: separatielogica. Een fundamenteel onderzoeksgebied met veel toepassingen in de praktijk. Hiep: ‘Als je als printerfabrikant wilt dat Microsoft automatisch jouw printers herkent, moet je bijvoorbeeld eerst kunnen aantonen dat de software van die printers geen gevaar is voor hun besturingssysteem. Dat gebeurt met separatielogica. Ook Facebook maakt er veel gebruik van. Daar zijn duizenden programmeurs in dienst die, met behulp van AI, non-stop analyseren of er geen fouten in de programmatuur staan. En hoe werkt die AI? Met separatielogica.’
Een gapend gat, dat wil niet iedereen horen
Separatielogica is dus een manier om fouten in computerprogramma’s te vinden. Maar Hieps onderzoek gaat nog een niveau hoger, legt hij uit. ‘Het richt zich op het vinden van fouten in dat bewijssysteem, in de separatielogica zelf.’ Het is niet zo dat het huidige systeem incorrect is. ‘Dat wil zeggen: als je een formule bewijst, dan is het wel degelijk waar. Alleen ik heb ontdekt dat er ook ware formules zijn die je met deze logica niet kon bewijzen. Je hebt dus een onvolledig bewijssysteem dat zelf wel correct is, maar niet alles kan bewijzen dat waar is.’
Je zou het een gapend gat in de bewijslast kunnen noemen. En dat vond niet iedereen even leuk om te horen. Hiep: ‘Als je al tijden werkt in dit onderzoeksgebied, of je hebt er als bedrijf miljoenen ingestopt, is het niet leuk als een Leidse promovendus komt vertellen dat het niet klopt. Het kostte daarom best veel moeite om mijn artikelen te publiceren. Maar het is gelukt.’
'Dan zit je dus opeens met een gat'
Maar waarom zou je iets onderzoeken dat we al twintig jaar (vermeend) succesvol gebruiken? ‘Het kwam min of meer toevallig op mijn pad’, aldus Hiep. ‘Ik werkte in eerste instantie aan een nieuw soort separatielogica: de dynamische separatielogica. Maar toen stuitte ik op een probleem. Ik kwam op twee formules en ik wilde laten zien dat die gelijk waren aan elkaar. Dat bleek zo te zijn, maar met geen enkele van de bestaande systemen kon ik dat aantonen: ik had een gat gevonden. Nou, dan zit je dus opeens met een gat. Dan moet je erin duiken. Een hoop werk, maar nu is het gat wel gedicht.’
Ontdekkingen toepassen in de praktijk
Ondanks het feit dat hij direct aan de slag kon als universitair docent in Leiden, koos Hiep voor een nieuwe uitdaging in Cambridge. ‘Ik ga aan de slag bij Amazon. Daar kan ik al mijn nieuwe inzichten en ontdekking meteen toepassen in de praktijk.’ En het Witte Huis? ‘Mijn proefschrift inclusief begeleidende brief zitten inmiddels op de post,’ besluit Hiep.
Hans-Dieter Hiep promoveerde 23 mei cum laude op het proefschrift 'New Foundations for Separation Logic'.
Totstandkoming
Hiep voerde zijn onderzoek uit bij zowel het Leiden Institute of Advanced Computer Sciences (LIACS) als het Centrum Wiskunde & Informatica (CWI), onder dagelijkse begeleiding van promotor Frank de Boer, en co-promotoren Alfons Laarman en Stijn de Gouw.
Over het CWI
Centrum Wiskunde & Informatica (CWI) is sinds 1946 het nationale onderzoeksinstituut voor wiskunde en informatica. Het is gevestigd op het Amsterdam Science Park en is onderdeel van de institutenorganisatie van NWO. Het instituut heeft een sterke internationale positie. Ruim 150 wetenschappers doen er grensverleggend onderzoek en dragen de verkregen kennis over aan de maatschappij. Meer dan 30 van de onderzoekers zijn hoogleraar aan een universiteit. Het instituut heeft 29 spin-off bedrijven voortgebracht.