TOBY MURRAY

ACM Software System Award

Australia - 2022

citation

For the development of the first industrial-strength, high-performance operating system kernel to have been the subject of a complete, mechanically checked proof of full functional correctness

In 2009, the seL4 microkernel became the first ever industrial-strength, general-purpose operating system (OS) with formally proved implementation correctness. The seL4 team further added proofs that seL4 enforces the core security properties of integrity (2011) and confidentiality (2013), while also removing the assumption that the C compiler must be trusted (2013), and performed the first sound and complete worst-case execution-time analysis of a protected-mode OS (2011).

 The seL4 high-assurance microkernel has fundamentally changed the research community's perception of what formal methods can accomplish: it showed that not only is it possible to complete a formal proof of correctness and security for an industrial-strength operating system kernel, but that this can be accomplished without compromising performance or generality.

 The functional correctness proof of seL4 was at the time one of the largest, and has now outgrown any other formal proof, consisting of over 1 million lines across three ISAs. Remarkably, the proofs have been maintained over a system that evolved significantly in 13 years, with less than half of the original kernel code still in use, and significant new features added. This has given rise to a new discipline of proof engineering---the art of proof process modelling, effort estimation, and the systematic treatment of large-scale proofs.

seL4?s real-world impact began with its open-sourcing (2014) and the DARPA HACMS (High-Assurance Cyber Military Systems) program, which was explicitly motivated by progress on seL4 and on the verified compiler CompCert. HACMS demonstrated seL4?s ability to protect autonomous systems from cyber-attacks, which led to a re-assessment of formal methods in US defense, and to seL4's deployment into defense systems. Responding to the growing open-source community, the seL4 Foundation, created in 2020, enlists several companies that rely on seL4 in their products, especially autonomous cars. Today, a vibrant seL4 ecosystem is forming, enabling verification for real systems where security and safety are critical.

Press Release

2022 ACM Software System Award

Gernot Heiser, University of New South Wales; Gerwin Klein, Proofcraft; Harvey Tuch, Google; Kevin Elphinstone, University of New South Wales; June Andronick, Proofcraft; David Cock, ETH Zurich; Philip Derrin, Qualcomm; Dhammika Elkaduwe, University of Peradeniya; Kai Engelhardt; Toby Murray, University of Melbourne; Rafal Kolanski, Proofcraft; Michael Norrish, Australian National University; Thomas Sewell, University of Cambridge; and Simon Winwood, Galois, receive the ACM Software System Award for the development of the first industrial-strength, high-performance operating system to have been the subject of a complete, mechanically-checked proof of full functional correctness.

In 2009, the Software System Awardees presented the seL4 microkernel, which became the first ever industrial-strength, general-purpose operating system with formally proved implementation correctness. In subsequent years, the team further added proofs that seL4 enforces the core security properties of integrity and confidentiality, extended the proof to the binary code of the kernel, and performed the first sound and complete worst-case execution-time analysis of a protected mode OS.

The seL4 high-assurance microkernel has fundamentally changed the research community’s perception of what formal methods can accomplish: it showed that not only is it possible to complete a formal proof of correctness and security for an industrial-strength operating system but that this can be accomplished without compromising performance or generality. The continuously maintained and growing proofs on seL4 have helped to give rise to a new discipline of proof engineering—the art of proof process modelling, effort estimation, and the systematic treatment of large-scale proofs.