The award recognises the development of the seL4 microkernel, the first ever industrial-strength, general-purpose operating system with formally proved implementation correctness.
The Association for Computing Machinery (ACM) has awarded the prestigious ACM Software System Award to Professor Gernot Heiser and Associate Professor Kevin Elphinstone of UNSW Computer Science and Engineering, UNSW associates June Andronick, Gerwin Klein, Rafal Kolanski, and their team.
The ACM Software System Award recognises the development of a software system that has had a lasting influence, reflected in contributions to concepts, in commercial acceptance, or both. It carries a prize of USD35,000. Professor Heiser and his team receive the award for the development of the first industrial-strength, high-performance operating system to have been the subject of a complete, machine-checked proof of functional correctness.
In 2009, the Software System Awardees presented the seL4 microkernel, together with a mathematical proof of correctness of its C-language implementation. From the beginning, seL4 was built for real-world use, reflected in is best-of-class performance and design for generality and security. In subsequent years, the team further added proofs that seL4 enforces the core security properties of integrity and confidentiality, and extended the proof to the binary code of the kernel, thus removing the need to trust the C compiler. They also performed the first sound and complete worst-case execution-time analysis of a protected-mode operating system.
The seL4 microkernel and its verification 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 continuously maintained and growing proofs on seL4, now well over a million lines of proof script, gave rise to a new discipline of proof engineering—the art of proof process modelling, effort estimation, and the systematic treatment of large-scale proofs.
“This award recognises work that started at UNSW in the 1990s, and finally led to the breakthrough result of the formal correctness proof of seL4 in 2009. seL4 continues to be at the core of the research and transition activities of UNSW’s Trustworthy Systems research group, aiming to make secure and dependable computer systems a reality. A world-wide community of collaborators and ecosystem partners is deploying seL4 in security- and safety-critical systems, especially in defence, autonomous vehicles and critical infrastructure,” says Professor Gernot Heiser.
The team consists of Gernot Heiser (UNSW), Gerwin Klein (Proofcraft), Harvey Tuch (Google) Kevin Elphinstone (UNSW), 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).
ACM is the world’s largest educational and scientific computing society, uniting computing educators, researchers, and professionals to inspire dialogue, share resources, and address the field’s challenges. Recognising individuals is one way ACM educates the wider public about the science behind technologies we use every day.