At the forefront of cyber security

To combat the challenges presented by an increasingly volatile cyber-security environment, Professor Gernot Heiser and his team’s seL4 microkernel technology provides secure isolation between computer programs – thereby making them extremely hard to hack and limiting any potential damage from future compromises.

Professor Gernot Heiser, leader of UNSW Trustworthy Systems.

While the operating systems used by billions each day provide a level of cyber protection, UNSW Trustworthy Systems leader and John Lions Chair, Scientia Professor Gernot Heiser understands the risks they also present. “Operating systems are big and overly complex and full of security holes, which means they can be compromised,” he explains. “There are dozens if not hundreds of critical exploits in mainstream operating systems per year, which is bad enough if it happens on your laptop but even worse if it happens on a public service or within a safety critical device such as a car.”

Prof. Heiser explains that most software will have one to five faults per thousand lines of code. “These operating systems are comprised of tens of millions of lines of code, so they’re full of holes and many of these are exploitable, which is why these systems get compromised.” To combat these significant problems, Prof. Heiser and his team developed the globally adopted seL4 microkernel technology, which leverages mathematically proved security enforcement.

“For a long time, our approach has been to fundamentally change the game of cyber security from the bottom up, by building operating systems that are extremely trustworthy and secure to the point where you can mathematically prove the security."

- Professor Heiser

“We pioneered this 14 years ago when we were the first group to prove correctness of an operating system kernel of about 9,000 lines of code, and now we’re working our way up, building and verifying a complete OS.”

Prof. Heiser believes this isn’t just possible but necessary. “Mainstream operating systems don’t have tens of millions of lines of code for nothing,” he explains. “Some of that code is needed to provide services, so you can’t build an OS with just 10,000 lines of code, but much of that code and complexity is unnecessary and almost all of it should be encapsulated in modules where failures can be contained – really standard engineering practice, but mostly ignored in operating systems,” he adds. “What we should and can do is build an operating system with sufficient functionality in a highly principled, highly modularised way that inherently gives you a much more trustworthy system. The seL4 microkernel is key, as it protects the various operating-system components from each other, which allows us to leverage the security guarantees of the kernel to prove the security of the overall OS – provided it is modular enough.”

The math behind the idea

Mathematical proof techniques scale poorly, so Prof. Heiser’s approach was to rethink the structure and design of his technology from the start. “Rather than adding more bells and whistles as we go, we’ve adopted the time-honoured KISS principle: keep it simple, stupid!” he says. “Not only does this result in a better system, it enables the use of mathematical proof techniques on the complete operating system.”

seL4 microkernal technology provides critical security enforcement to operating systems.

seL4 is part of an ecosystem supporting active use in various domains including automotive, aviation, infrastructure, medical, and defence.

Steering cyber security in the right direction

One of the areas where Prof. Heiser’s technology is taking off is the electric vehicle space, as attacks on cars have been demonstrated for quite a few years now. “Many cyber-attacks these days are used by well-resourced players for economic blackmail or political reasons, so the potential attackers will hold back until they get the most benefit,” explains Prof. Heiser. “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.”

With the adoption of seL4 however, car manufacturers can significantly improve safety of cars, both in terms of normal use and protecting it from cyber-attacks. Chinese premium electric carmaker, NIO, who are already selling in Europe and are expanding into the US market, 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.”

Safety online means safety offline

While Prof. Heiser believes there is still a lack of understanding about the real threats society faces when it comes to software hacks, he’s hoping this will change in the near future. “There tends to be a lack of understanding that security issues are safety issues – there’s no safety without cybersecurity,” he says. “That hasn’t reached the general consciousness yet, and that really needs to change.”

Thankfully, in countries such as the US, UK and Germany, there’s a strong desire to utilise Prof. Heiser’s technology. The Defense Advanced Research Projects Agency (DARPA) in the United States and the UK's National Cyber Security Centre (NCSC) have supported seL4 for years, and the German government just released the major tender for developing highly secure computer systems,” he says. “They explicitly referred to our seL4 system on the basis of which to build the technology. My hope however is that everyone gets to the point where they do adopt what we provide for free as open source.”

A real-world deployment of the seL4 in an autonomous helicopter as part of the DARPA-funded HACMS program, where seL4 is used to protect against cyber-attacks.

Prof. Heiser and his UNSW team from The Trustworthy Systems Group.

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 we made the decision early on to open source what we do.” It’s one of the many ways Prof. Heiser hopes to see his technology reach more people through widespread uptake.