Lions OS: Fast, Secure, Adaptable
Emu (Nurin) | Thu 18 Apr 11:40 a.m.–12:25 p.m.
Presented by
-
Gernot Heiser
https://gernot-heiser.org
Gernot has been building high-performance microkernels and microkernel-based operating systems for about 30 years. This includes the OKL4 microkernel which shipped on billions of Qualcomm modem chips, a kernel that runs on the Secure Enclave processor of iOS devices, and seL4 microkernel, the world's first OS kernel with a mathematical proof of implementation correctness. seL4, which won the 2023 ACM Software System Award, still has the most comprehensive mathematical assurance story of any non-toy OS kernel, and is still the only formally verified kernel with capability-based access control. It is deployed in critical systems around the world, aided by the seL4 Foundation which Gernot chairs. Electric car maker NIO has recently announced that their seL4-based SkyOS will ship in mass-production cars from 2024.
Gernot is Scientia (distinguished) Professor at UNSW Sydney, a member of the German Academy of Science Leopoldina, and a Fellow of the Academy of the Australian Technology and Engineering (ATSE), the Royal Society NSW, the ACM, the IEEE, and Engineers Australia.
Gernot Heiser
https://gernot-heiser.org
Abstract
seL4 is the world's most secure operating system (OS) kernel, but it is a far cry from being an OS. As a microkernel, it provides core mechanisms for securely multiplexing the hardware, but none of the services application programmers expect, so adopters are forced to develop those themselves. Furthermore, a high level of expertise is required to design performant systems on top of seL4. The result is frequently a poor design, and far too often people giving up.
The Trustworthy Systems team at UNSW has now decided to build Lions OS, a complete seL4-based OS aimed to support the needs of developers of cyberphysical, IoT and other embedded systems. Lions OS, named after John Lions (of Lions Book fame, arguably one of the fathers of open source), is being designed and implemented from scratch, with the seemingly conflicting goals of high performance, high security and adaptability to a wide class of use cases. Specifically we plan to prove the correct implementation of its critical components.
In the talk I will explain why I think this is not only achievable, but will be achieved within 2-3 years, by strictly adhering to the time-honoured engineering principle KISS – keep it simple, stupid! I will present our initial results that show that, with the right design, this simplicity can not only achieve excellent performance (outperforming Linux networking by a factor three) but also enable proofs of implementation correctness. By the time of the conference, an initial release (of limited functionality but reasonable maturity) will have been made. Needless to say, Lions OS is open source.
seL4 is the world's most secure operating system (OS) kernel, but it is a far cry from being an OS. As a microkernel, it provides core mechanisms for securely multiplexing the hardware, but none of the services application programmers expect, so adopters are forced to develop those themselves. Furthermore, a high level of expertise is required to design performant systems on top of seL4. The result is frequently a poor design, and far too often people giving up. The Trustworthy Systems team at UNSW has now decided to build Lions OS, a complete seL4-based OS aimed to support the needs of developers of cyberphysical, IoT and other embedded systems. Lions OS, named after John Lions (of Lions Book fame, arguably one of the fathers of open source), is being designed and implemented from scratch, with the seemingly conflicting goals of high performance, high security and adaptability to a wide class of use cases. Specifically we plan to prove the correct implementation of its critical components. In the talk I will explain why I think this is not only achievable, but will be achieved within 2-3 years, by strictly adhering to the time-honoured engineering principle KISS – keep it simple, stupid! I will present our initial results that show that, with the right design, this simplicity can not only achieve excellent performance (outperforming Linux networking by a factor three) but also enable proofs of implementation correctness. By the time of the conference, an initial release (of limited functionality but reasonable maturity) will have been made. Needless to say, Lions OS is open source.