Ensuring security at the core of our computing world

Professor Gernot Heiser FTSE from UNSW Sydney has been thinking about operating systems for a long time. Since 1994 when he first started being concerned about secure computing devices, he has worked to develop and test radically simple, powerful and safe code to power our computers. 

At the centre of our computing devices, controlling what they can do, is the operating system, and within it, the kernel.  

The kernel is the layer of code that enables the operating system (OS) and all the applications to interact with the computing hardware underneath. It is how the system accesses the memory, processors and communication systems it needs. It is so central to the computer that a single fault can completely compromise the system, causing it to fail or allow unauthorised access. If this were to happen in a medical implant or a car, the consequences could be life threatening. With tiny computers becoming more common in everyday devices, across industries, workplaces and healthcare, the importance of secure operating systems is ever increasing. 

Gernot is on a mission to build kernels and operating systems that deliver high performance with an unprecedented level of security. 

Solving hard problems

He says, “My work is focused on ensuring the security and safety of computer systems. Computer systems are by far the most complex artefacts humanity has ever produced, and their complexity has long outgrown our ability to deal with it in a controlled fashion.” 

Gernot’s work has approached this problem by attempting something that many thought was impossible. With his team, he designed and built a kernel – seL4 – to ensure security, and then mathematically proved that it was as secure as intended. The machine-checked proof guarantees that there are no faults in the approximately 10,000 lines of code. It guarantees that the kernel is exactly as secure as it says it is, with no gaps or loopholes. 

Verifying code is orders of magnitude harder than writing code. That’s why many thought it would be impossible to fully verify a kernel complex enough for real-world applications. Many considered the amount of code needed to create a useful kernel to be too large for an effective verification to be performed on it. Now however, it has been done, and is recognised as a world-leading achievement by the computer science community. The technology has received the Software System Award in 2023 from the Association for Computing Machinery (ACM), and the original publication won a Hall of Fame Award from the ACM Special Interest Group on Operating Systems. seL4 is now in use around the world in embedded processors and Internet of Things devices, and is, for example, going to be a pivotal part of Chinese electric car company NIO’s automotive computing platform from this year onward. 

Careful planning, expert coding and a commitment to solving hard problems effectively allowed Gernot to create the world’s first operating system kernel that was proved free of faults. The next step is a complete, fully secure operating system. How will he achieve that? Radical simplicity. 

Radical simplicity

Gernot’s solution for operating system design is to go back to basics. Instead of designing a large operating systems catering for hundreds of different use cases, interaction models and configurations, he and his research group at UNSW are keeping it simple. They are using the robust seL4 kernel at the centre of a new, streamlined operating system – Lions OS. In this operating system, the seL4 kernel will handle the truly critical tasks, assisted by additional components to manage the various system functions (such as device communication and networking). 

Modern operating systems for personal computing are by necessity complex and able to perform a huge array of different tasks. The kernels of mainstream operating systems such as Windows and iOS comprise tens of millions of lines of code, with faults an inevitability as they balance performance, security and features for consumer use. However, for the growing ecosystem of cars, robots and medical devices – all controlled by embedded processors running often poorly suited general-purpose operating systems – a provably secure OS catering to their needs is the goal.  

By building modularity into the design of Lions OS, each component can be carefully designed and included only if its functionality is required. Rather than redundant code unused by the system creating potential vulnerabilities, these modules can be swapped out when and if required.  

The next step? Mathematically verifying the entire operating system.  

In Gernot’s words, “It is feasible to design a complete operating system in a way that beats Linux in performance and facilitates verification.” The simplicity of the design enables the proof techniques to be automated, which will be important as Lions OS may reach up to 100,000 lines of code when completed, up to 10 times bigger than the seL4 kernel. Yet, by leaning into a radically simple design with no frills and only code that is absolutely necessary, the team of researchers and students is aiming to build a complete, secure OS for embedded systems within the next few years. 

Building with great students

For Gernot, this work is not just about beating the expectations of what’s possible. He wants to deliver functional code, actually useful software that can make a difference to critical use cases around the world: medical implants to keep hearts beating, computers that control critical infrastructure, instruments to control electric cars and so many more. All of these rely on the security and stability of their operating systems, and the smaller the scope for failure, tampering or attacks, the safer we will all be. Gernot says, “There’s no safety without cybersecurity.” 

His ambitious goals are attainable with equally motivated students to inspire and be inspired by. The research group is made up of around 40 people, with around half of them undergraduate computer science students. They complete advanced courses in OS design and mathematical proof techniques, and contribute to the myriad of Lions OS research and development tasks. With this team, Gernot feels, anything is possible. 

The world of computing devices is constantly becoming more complex. Yet as processors have gotten more powerful, we have become used to being able to rapidly run large amounts of inefficient code. The Trustworthy Systems group, led by Professor Gernot Heiser, is pushing the other way. Instead of increasingly large code bases with ever larger areas of potential vulnerability, they are finessing the operating system code to be as small, efficient, and secure as possible. Pulling it off in a way that is useful in practice is the great challenge. Fortunately, the team is up to the task.