Programming problem patched: PhD candidate discovers breakthrough in software security

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

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

Leiden University and CWI

Hiep conducted his research at both the Leiden Institute of Advanced Computer Sciences (LIACS) and Centrum Wiskunde & Informatica (CWI). In Amsterdam, he worked in CWI's Computer Security research group. His PhD thesis is titled 'New Foundations for Separation Logic'. Supervisor: Prof. F.S. de Boer (em. CWI & UL), co-promotores: dr. C.P.T. de Gouw (OU) and dr. A.W. Laarman (UL).

Source, with permission: news item on Hiep's PhD defence at Leiden University