Our Partners

Lions Operating System

Secure, fast, adaptable!

Aim

A highly modular operating system for real-world embedded, IoT and cyberphysical systems that sets new standards in performance, verifiability, and adaptability to a wide range of use cases.

Problem

The seL4 microkernel is unrivalled in both its assurance as well as performance. However, its API is inherently very low-level and hard to use, and the microkernel (by design) does not provide the functionality expected from an operating system.

Solution

We are addressing this by developing the Lions OS whose design is driven by the KISS principle: “Keep it simple, stupid!” This calls for a highly modular design, where each component provides the absolute minimum functionality the use case requires, an approach we call radical simplicity. This simplicity is not only good for robustness, it also enables push-button verification of components. Radical simplicity calls for abandoning the traditional quest for universal policies, and instead providing use-case–specific policies. The system can adapt to a different use case by replacing components with implementations optimised for the new use case. The simplicity also enables high performance by minimising the amount of code that executes to achieve a specific function.

Name

Lions OS is named in honour of the late UNSW professor John Lions, known as the author of the Lions Book, which taught Unix to generations of programmers.

The original Unix was known for its clean and lean design, and a strong departure from prior OS designs. At TS we feel that the OS world has lost its way by forgetting the lessons from Unix, resulting in mushrooming complexity, endless critical vulnerabilities, and performance issues that are addressed by hacks and workarounds that further increase complexity. With Lions OS, we are guided by some of the principles of Unix, thus re-thinking the fundamentals of OS design.

Approach

We are designing a set of system services, each made up of simple building blocks that make best use of the underlying seL4 kernel and its features, while achieving superior performance. The building blocks are simple enough for automated verification tools (SMT solvers) to prove their implementation correctness. We are furthermore employing model checkers to verify key properties of the interaction protocols between components.

Core to this approach are simple, clean and lean designs that can be well optimised, use seL4 to the best effect, and provide templates for proper use and extension of functionality. Achieving this without sacrificing performance, while keeping the verification task simple, poses significant systems research challenges.

Building blocks

The following sub-projects presently form part of Lions OS:

• the seL4 Microkit, a lean framework for developing statically-architected OS personalities for seL4;
• the seL4 Device Driver Framework (sDDF), a set of interface specifications, device-driver template, control and data plane implementation, and tools for writing device drivers and providing device virtualisation for high-performance I/O on seL4.

Support

We gratefully acknowledge the financial support for the development of Lions OS by:

• UK's National Cyber Security Centre (NCSC)
• DARPA under the PROVERS program
• NIO America
• The John Lions Fund via the John Lions Chair

Collaboration

• Our core collaboration partner under the DARPA PROVERS program is main contractor Collins Aerosapce.

Documentation

Lions OS has its own documentation site.

Availability

Lions OS is available from the TS GitHub under a BSD license.

Latest News

• 2024-03-27: TS releases version 0.1.0 of Lions OS on the TS GitHub.
• 2023-11-30: NIO provides financial support for the development of Lions OS.
• 2023-09-19: Gernot Heiser discusses Lions OS at his TS R&D Update at the seL4 Summit.

Contact

• Gernot Heiser, gernot<at>unsw.edu.au

People

Publications

		Gernot Heiser Lions OS: secure – fast – adaptable Everything Open, Gladstone, QLD, AU, April, 2024
		Lucy Parker The seL4 device driver framework Talk at the 5th seL4 Summit, September, 2023
		Ivan Velickovic The seL4 Microkit Talk at the 5th seL4 Summit, September, 2023
		Mathieu Paturel, Isitha Subasinghe and Gernot Heiser First steps in verifying the seL4 Core Platform Asia-Pacific Workshop on Systems (APSys), Seoul, KR, August, 2023
		Gernot Heiser R&D update from Trustworthy Systems Talk at the 5th seL4 Summit, 2023
		Gernot Heiser, Lucy Parker, Ivan Velickovic, Peter Chubb and Ben Leslie Can we put the "S" into IoT? IEEE World Forum on Internet of Things, Yokohama, JP, November, 2022