Using maths to prove computer security

‘Secure’ computer systems get hacked all the time. We live in a world where very few systems are truly safe, and proving that a system is secure is challenging. It’s about understanding the kind of evidence required. I first became interested in how to prove a platform is secure when I was working for Defence in the early 2000s – and I’m still working on it.

I started my PhD thinking I was going to answer this tough problem and then I moderated my ambitions! Proving security is difficult. But I have continued in the same direction since.

When I was an undergraduate I thought ‘the maths stuff’ in software development was boring and useless. But maths became a necessity. What helped convince me were some cases in the 90s and early 2000s where mathematical approaches proved that systems everyone thought were secure actually weren’t.

I still don’t consider myself a good mathematician, but it’s a tool I find very useful for my work. Computer systems are highly complex but we can distil security problems down to the critical details. Once we have the essence of the system, we can describe its constituent parts really elegantly using mathematics and logic.

Back in 2015 we had no mathematics to prove the security of important software systems performing multiple tasks at once. These are known as concurrent systems. We realised there was an opportunity to develop new methods to interrogate and test these kinds of software, so we developed the COVERN logic.

It’s a tool for distilling the logic underpinning the security of software that does different things at different times. It essentially works through a computer program, but like any kind of mathematical proof it still requires some human intelligence.

Our research can be dry and tricky so connecting with something practical was a wonderful opportunity. We developed COVERN to prove the security of a new device for Defence, called the Cross Domain Desktop Compositor (CDDC). It safeguards sensitive data while allowing instant access to online content.

Working on a real-world project meant we weren’t just talking about abstract software fairyland, but actually making sure our research is useful.

Some of my partners on the CDDC project were colleagues back in my Defence days. We worked together twenty years ago, when Wi-Fi was just emerging and iPhones didn’t exist. It’s been great to work together again on such a successful project.

It was initially very difficult to interrogate and test the security of the CDDC. That was because it is concurrent and dynamic, with users potentially handling top-secret data one minute and using the public Internet the next. When we first started the project in 2015, we had no idea how we could prove its security. It’s been very satisfying to deliver a solution.

It might seem like an odd question, but now I’m asking, ‘how do I prove my system has a vulnerability?’. It’s the opposite question to the one I started with, which was ‘how do I prove my system is secure?’. But, actually, it is easier to look for evidence of trouble rather than evidence of the absence of trouble. It means we can look more quickly and easily for vulnerabilities we might expect to find in certain kinds of systems.

Our mathematical methods that prove security can also prove systems have vulnerabilities. That’s been really interesting to discover. They have some unique advantages over other methods, too. Again, it’s all about deconstructing the large system and analysing its constituent parts.

This means that when we change one part of the system, we only need to re-analyse the parts we changed, so we can search for vulnerabilities incrementally. While it’s not as assuring as proving security, proving vulnerability can be a faster and simpler process.

– As told to Catriona May, University of Melbourne

Associate Professor Toby Murray was part of the team that won the 2021 Science and Technology Eureka Prize for Outstanding Science in Safeguarding Australia, along with University of Melbourne colleague Dr Robert Sison and colleagues from the University of New South Wales and the Defence, Science and Technology Group.

Banner: Shutterstock