Programming problem patched: Leiden PhD candidate discovers breakthrough in software security
By chance, computer scientist Hans-Dieter Hiep (Leiden Institute of Advanced Computer Science and Centrum Wiskunde & Informatica) discovered a ‘gaping hole’ in a widely used method for evaluating software security. Hiep patched the hole, causing quite a stir in his field. 'It’s not pleasant when a PhD candidate from Leiden comes along and points out that a twenty-year-old proof system is flawed.’ Hiep graduated cum laude on 23 May.
‘Small programming errors can have significant consequences,’ says Hiep. ‘Especially if the error is in the part of the software that handles and protects our working memory.’ These systems ensure, for example, that users can temporarily share their memory without risk. Hiep explains: ‘If there’s a mistake in such an operating system, you can easily get a data breach, and everything is out in the open. Errors in memory security are the leading cause of common vulnerabilities and leaks.’
The threat posed by such bugs to digital security is underscored by a White House press release from last February. It calls on the scientific community to come up with solutions to this ‘persistent problem’.
Eliminating bugs in software
Hiep works on program correctness, which means eliminating bugs in software. ‘This field is already fifty years old,’ he says. ‘I focus on the correctness of so-called pointer programs. These are programs that work with memory addressable by pointers: this includes almost all programs today.’
'As a manufacturer, you must first be able to demonstrate that your printer poses no threat to Microsoft systems.'
For twenty years, there has been a method to prove there are no bugs in such pointer programs: separation logic. It’s a fundamental field with many practical applications. Hiep explains: ‘If you’re a printer manufacturer and you want Microsoft to automatically recognise your printers, you first need to prove that the printer’s software is no threat to their operating system. This is done using separation logic. Facebook also makes extensive use of it. Thousands of programmers are employed there, using AI to continuously analyse for errors in the software. And how does that AI work? With separation logic.’
A gaping hole not everyone wants to hear about
Separation logic is thus a way to find errors in computer programs. But Hiep’s research goes one level higher, as he explains: ‘It focuses on finding errors in that proof system, in the separation logic itself.’ It’s not that the current system is incorrect. ‘That is, if you prove a formula, then it is indeed true. Only I discovered that there are also true formulas that you couldn’t prove with this logic. So you have an incomplete proof system that is correct but cannot prove everything true.’
You could call it a gaping hole in the proof system. And not everyone was happy to hear that. Hiep explains: ‘If you've been working in this research area for a long time, or if your company has invested millions in it, it’s not pleasant when a PhD student from Leiden comes along and says it doesn’t add up. It took quite a bit of effort to get my articles published. But I succeeded.’
‘Suddenly, I was faced with a challenge’
But why investigate something we’ve been (supposedly) successfully using for twenty years? ‘I discovered it almost by accident,’ says Hiep. ‘I initially worked on a new type of separation logic: dynamic separation logic. But then I encountered a problem. I came up with two formulas and wanted to show they were equivalent. They were, but none of the existing systems could prove it: I had found a gap. Suddenly, I was faced with this challenge. It was no easy feat, but I finally managed to close the gap.’
Applying discoveries in practice
Despite being able to start immediately as a university lecturer in Leiden, Hiep chose a new challenge in Cambridge. ‘I’m going to work at Amazon. There, I can immediately apply all my new insights and discoveries in practice.’ And the White House? ‘My dissertation, including an accompanying letter, is already in the mail,’ concludes Hiep.
Hans-Dieter Hiep defended his doctoral thesis titled 'New Foundations for Separation Logic' on 23 May. He graduated cum laude.
Realisation of the research
Hiep conducted his research at both the Leiden Institute of Advanced Computer Sciences (LIACS) and Centrum Wiskunde & Informatica (CWI), under the daily supervision of supervisor Frank de Boer and co-supervisors Alfons Laarman and Stijn de Gouw.
About CWI
Founded in 1946, Centrum Wiskunde & Informatica (CWI) is the national research institute for mathematics and computer science in the Netherlands. It is located at Amsterdam Science Park and is part of the Institutes Organisation of NWO. The institute is internationally renowned. Over 150 researchers conduct pioneering research and share their acquired knowledge with society. Over 30 researchers are also employed as professors at universities. The institute has generated twenty-nine spin-off companies.