Building trustworthy systems
Locally developed technology is protecting computer systems worldwide from cyber-attacks.
Published on the 29 July 2024
In today's increasingly volatile digital landscape, cyber threats are on the rise. Scientia Professor Gernot Heiser and his team are pioneering technology to shield computer systems worldwide from malicious attacks.
Their seL4 microkernel technology ensures the security of operating systems by using mathematically proved security measures.
“Operating systems are big, complex, and full of security holes, which means they can be compromised. It’s bad enough if that happens on your laptop, but it’s even worse if it happens to a power generation station or to a safety critical device such as a car or medical implant,” says Scientia Professor Heiser, UNSW Trustworthy Systems leader and John Lions Chair.
“Much of the code and complexity of operating systems is unnecessary and almost all of it should be encapsulated in modules where failures can be contained.”
The seL4 microkernel technology addresses this by isolating different parts of the operating system from each other. This means that if one part is compromised, it won’t affect the entire system. It also enables leveraging the security guarantees of the kernel to prove the security of the overall OS.
“15 years ago, we were the first to prove correctness of an operating system kernel, then about 9,000 lines of code. Now we’re working our way up, from scratch building and verifying a complete OS, called LionsOS,” says Prof. Heiser.
“Building an operating system in a highly principled, highly modularised way inherently gives you a much more trustworthy system.”
One of the areas where Prof. Heiser’s technology is taking off is the electric vehicle space, where cyber attacks could have large consequences.
“All you have to do is hijack 10 cars, cause accidents in strategic locations and you basically grind a city to a halt for half a day – the economic damage from this is quite substantial.”
Chinese premium electric carmaker NIO are preparing to ship cars with an operating system that runs on seL4. “This is by far not the first deployment of the technology, but it’s the first tangible consumer product that utilises the security guarantees you get from the work we’ve done.”
Recognition for seL4 have is growing globally, with support from institutions like The Defense Advanced Research Projects Agency (DARPA) in the United States and the UK's National Cyber Security Centre (NCSC). Recently, the German government released the major tender for developing highly secure computer systems, referring to the seL4 system as the foundation for the technology.
For Prof. Heiser, what matters most is that his ongoing research and evolution of seL4 continues to benefit industries and communities. “I like to do stuff that has impact – to enable real-world use,” he says. “This is why our work is open source. We really believe that this tech can and should be used universally.”
Scientia Professor Gernot Heiser, leader of UNSW Trustworthy Systems
As Australia’s best engineering faculty turns 75, there are just as many reasons why we’ve earned that title. Discover new stories weekly, celebrating the successes that have enabled progress for all.
