Making Trusted Systems Trustworthy

Speaker:  Gernot Heiser – Sydney, NSW, Australia
Topic(s):  Security and Privacy


We trust computer systems all the time: with our money, our sensitive private data, our critical infrastructure and, in the age of autonomous vehicles, increasingly with our lives. Yet contemporary computer systems really do not deserve such trust. We all got used to or PCs crashing, and all too frequently they get hacked by attacker. While lack of computer reliability is often just an nuisance, increasingly it is well-resourced organised crime attacking individuals or organisations for financial gain. For critical infrastructure there is also the threat from state actors that might attack for political blackmail or to cause economic damage.

Clearly we need to do better. And, while we are still years away from making complex, general-purpose computers, such as PCs and servers, trustworthy in any real sense, we now have the core ingredients for true trustworthiness, and are able to apply them in the more restricted scenarios of embedded and cyberphysical systems. Specifically, the seL4 microkernel is the first operating system (OS) kernel with a machine-checked proof of implementation correctness-bug-free in a very strong sense. The proof states that the kernel will always behave according to its formal specification, and applies to the actual binary code that runs on hardware. Additional proofs about the specification show that the kernel can enforce the classic security properties of confidentiality, integrity and availability.

As such, seL4 is a bullet-proof base for building truly trustworthy systems, and it is already being deployed in national security, autonomous cars and critical infrastructure. However, seL4, being a microkernel, only provides the basic mechanisms for trustworthy system, it is not a complete system, and much further research and development is needed to make complete trustworthy systems a reality. These include trustworthy high-level services and abstractions, such as file systems and networking services, trustworthy application code that leverages the guarantees provided by the kernel, and system architectures that lend themselves to formal reasoning about security and safety. This will require further progress across operating systems, programming language design and implementation, formal methods as well as hardware verification. There is also on-going research on seL4 itself, especially on a principled prevention of information leakage through timing channels.

About this Lecture

Number of Slides:  45 - 50
Duration:  30 - 40 minutes
Languages Available:  English
Last Updated: 

Request this Lecture

To request this particular lecture, please complete this online form.

Request a Tour

To request a tour with this speaker, please complete this online form.

All requests will be sent to ACM headquarters for review.