Gapend gat gedicht: promovendus ontdekt doorbraak in softwareveiligheid

Per toeval ontdekte computerwetenschapper Hans-Dieter Hiep (Universiteit Leiden en CWI) 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 promovendus even komt vertellen dat een twintig jaar oud bewijssysteem niet klopt.’ Hiep promoveerde 23 mei cum laude.

Publicatiedatum
27 mei 2024

‘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.’

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 promovendus komt vertellen dat het niet klopt. Het kostte daarom best veel moeite om mijn artikelen te publiceren. Maar het is gelukt.’

Hans-Dieter Hiep (CWI and Leiden University) outside the CWI building, with a network builduing in the background.
Hans-Dieter Hiep (right) en Marcello Bonsangue na Hieps verdediging in Leiden, 23 mei 2024. Foto: Sher Takes Care.

'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.

Leiden University en CWI

Hiep voerde zijn onderzoek uit bij zowel het Leiden Institute of Advanced Computer Sciences (LIACS) als het Centrum Wiskunde & Informatica (CWI). In Amsterdam werkte hij in CWI's Computer Security groep. Zijn proefschrift is getiteld: 'New Foundations for Separation Logic'. Promotor: prof. dr. F.S. de Boer (em. CWI & UL), co-promotores: dr. C.P.T. de Gouw (OU) en dr. A.W. Laarman (UL).

CWI building

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.