From niche to prime time: How seL4 changed a research community
Speaker: Gernot Heiser – Sydney, NSW, AustraliaTopic(s): Software Engineering and Programming
Abstract
Operating system (OS) microkernels had been around since the 1970s, and were popular in the '80, just to become highly unfashionable in the '90s resulting from poor performance and deployment debacles. The early L4 microkernels of the mid-'90s demonstrated that good performance was possible with good design, but they remained a niche research topic (although commercially deployed in critical systems, especially avionics).
Similarly, formal verification, i.e. correctness proofs, of program code looked promising in the early '90s, but failed to deliver on more than toy problems. As a result, it made little impact, especially in the systems space, with virtually no verification results published in the top venues.
This all changed when we provided a machine-checked proof of the correct implementation of the seL4 microkernel, the first ever OS kernel with such a proof. seL4 was specifically designed not to be a toy, but for real-world deployment, which required competitive performance. And it had to be written from scratch, to make verification feasible.
The effect of the work was a dramatic change in attitude to formal methods first in the research community, and with some delay government and industry. The top systems conferences now regularly have multiple verification sessions, government organisations, such as DARPA, as well as corporations such as Apple, Amazon and Facebook, are massively re-investing in formal verification. And SIGOPS recognised the work and its impact with a Hall of Fame Award in 2019.
In this talk I will discuss the story of seL4 in more detail, its real-world impact, and some of the follow-on research it triggered. I will also highlight some of the current research opportunities resulting from seL4.
About this Lecture
Number of Slides: 45 - 50Duration: 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.