Using math to prove computer security

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

I started my thesis thinking that I was going to answer this difficult problem, then I moderated my ambitions! Prove that security is difficult. But I have continued in the same direction since.

Associate Professor Toby Murray and his colleagues have developed new methods to prove the security of software systems. Image: Supplied

When I was a student I thought the “math stuff” in software development was boring and unnecessary.. But math has become a necessity. What helped convince me were some cases in the 90s and early 2000s where mathematical approaches proved that systems that everyone thought safe were not in reality.

I still don’t consider myself to be a good mathematician, but it is a tool that I find very useful for my job. Computer systems are very complex, but we can summarize security issues down to the critical details. Once we have the essence of the system, we can describe its building blocks in a very elegant way using math and logic.

In 2015, we had no mathematical calculations to prove the security of large software systems that multitask. They are competing systems. We realized that there was an opportunity to develop new methods to query and test these types of software, so we developed the BLANKET logic.

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

Our research can be dry and delicate, so connecting with something practical was a wonderful opportunity. We developed COVERN to prove the security of a new defense device called the Cross-domain desktop composer (CDDC). It protects sensitive data while allowing instant access to online content.

Working on a real-world project meant that we weren’t just talking about the realm of abstract software, but actually making sure our research was useful.

The CDDC is a new device to prove computer security. Image: Supplied

Some of my partners on the CDDC project were colleagues at the time of the Defense. We worked together twenty years ago, when Wi-Fi was emerging and iPhones didn’t exist. It was a pleasure to work together again on such a successful project.

It was initially very difficult to interrogate and test the security of the CDDC. This is because it is simultaneous and dynamic, with users potentially able to handle top secret data one minute and use the public Internet the next. When we first launched the project in 2015, we had no idea how we could prove its safety. It has been very satisfying to provide a solution.

It might sound like a strange question, but now I’m asking, “How do I prove my system has a vulnerability?” “. This is the opposite question to the one I started with, which was “How do I prove my system is secure?” “. But, in reality, it is easier to look for evidence of problems rather than evidence of no problems. This means that we can search for vulnerabilities faster and easier than we might expect to find in certain types of systems.

Our mathematical methods that prove security can also prove that systems have vulnerabilities. It was really interesting to find out. They also have unique advantages over other methods. Again, it’s about deconstructing the grand system and analyzing its building blocks.

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

– As told to Catriona May, University of Melbourne

Associate Professor Toby Murray was part of the winning team Eureka Prize for Science and Technology 2021 for Outstanding Science in Saving Australia, with a colleague from the University of Melbourne Dr Robert Sisson and colleagues from the University of New South Wales and the Defense, Science and Technology Group.

Banner: Shutterstock

Margie D. Carlisle