Lions OS: Secure, Fast, Adaptable
Abstract:
The formal verification of the seL4 microkernel, almost 15 years ago, was a major step towards making a secure OS a reality, but not more than a first step. While seL4 has now been deployed in a number of defence and civilian projects, and cars running an seL4-based OS are about to hit the road, the sad reality is that there are probably more failures than successes in seL4 deployment. We have to conclude that they BYO services approach doesn’t work: coming up with a good design of an seL4-based system, including re-use of legacy services, requires far too much expertise.
At Trustworthy Systems we have therefore embarked on a project to design and implement a complete seL4-based OS, Lions OS (named after the author of the Lions Book that taught Unix to generations of programmers). The name is program: we aim to make the project tractable by applying some of the core principles of Unix, especially simplicity and clean design. In addition we are restricting ourselves (for now, at least) to systems with a static architecture, i.e. the set of components and (the ceiling of) the communication channels connecting them are fixed at system build time. This restriction is compatible with at least the vast majority of cyberphysical, IoT and other embedded systems.
Specifically, our aim is to build an OS that is (a) provably secure, (b) performing at par with insecure mainstream systems such as Linux, and (c) adaptable to a wide range of use cases within the target domain. I will report on our progress so far, which includes the development and verification of the seL4 Microkit, a thin abstraction layer on which Lions OS is built, and our experience with building a highly modular, yet high-performant networking layer. We plan to release a first, complete reference system demonstrating a rump Lions OS by March this year.
Shortbio:
Gernot Heiser is Scientia (distinguished) Professor and John Lions Chair of Operating Systems at UNSW Sydney, where he leads the Trustworthy Systems research group. His research interest are in operating systems, real-time systems, security and safety. His research vision is to completely change the cybersecurity game from playing catch-up with attackers to systems that are provably secure. With his team he pioneered the large-scale formal verification of systems code, specifically the design, implementation and formal verification of the seL4 microkernel; seL4 is now being used in real- world security- and safety-critical systems.
Heiser's former company Open Kernel Labs, acquired by General Dynamics in 2012, marketed the OKL4 microkernel, which shipped on billions of mobile wireless chips and is deployed on the secure enclave of all iOS devices. He presently serves as Chief Scientist of Neutrality, and Chairman of the seL4 Foundation. Gernot is a Fellow of the ACM, the IEEE, Engineers Australia, the Australian Academy of Technology and Engineering (ATSE) and the Royal Society of New South Wales (RSN) and a Member of the German Academy of Sciences Leopoldina. He is also an ACM Distinguished Lecturer and an IEEE Distinguished Visitor.external page