Funding
Our Partners
LionsOS
Fast, secure, adaptable!
Aim
LionsOS aims to be 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 LionsOS, the Lions Operating System, whose design is driven by the KISS principle. 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
LionsOS 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 LionsOS, we are guided by some of the principles of Unix, thus re-thinking the fundamentals of OS design.
The LionsOS logo is, of course, a play on the name of the OS. But it is also a reference to the lion in UNSW's code of arms, and UNSW's mascot, Clancy the Lion.
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 LionsOS:
- 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.
- the Virtualisation Library that allows Linux and (on X86_64) Windows virtual machines to use device drivers from the sDDF, and provide services to other protection domains.
Reference Systems
The Point of Sale demonstrator
The picture on the right shows a reference system: A point-of-sale (PoS) system in daily use in the TS lab: Tapping your staff card on the RFID reader charges $1.- against your account.
The figure below shows the architecture of the system. It has native drivers for serial, timer, Ethernet and I2C bus, the latter connects to the RFID reader. The business logic is implemented in Python on top of a port of Micropython. It accesses the Internet using an lwIP library that connects to the Ethernet. The Ethernet is also used for accessing network storage using a NFS client, which also uses an lwIP library.
The graphics display is accessed via a driver VM, which hosts a stripped-down Linux guest that mostly wraps a graphics driver, which in turn is accessed via usermode code that uses Linux UIO to interface to the device driver.
Hence this system demonstrates, among others, sharing of a device (Ethernet) between multiple clients, as well as re-using unmodified legacy drivers via Linux driver VMs.
A Firewall
In order to test the ideas in LionsOS against a more complex system, we started to build a firewall, and make it a community-backed project. There are many small things that can be added, tweaked, or adjusted in such a project without having to delve deeply into the more difficult aspects of seL4 or inter-component communication.
Building a firewall showed many assumptions baked into the systems we
were developing for LionsOS, that needed to be relaxed. The
firewall needed many more components than anything we had built
before (currently it has fifteen separate protection domains in the
mainline branch, but experimental branches that add functionality
have nearly twice this); and their interconnection, to allow
information flows between interfaces, and between any interface and
the webserver that provides the GUI for control, required new
paradigms for tracking buffer ownership, and a new queue type
(the
The firewall currently runs on an i.MX8 platform, the IOT-GATE-iMX8 or on QEMU. It can control packet forwarding between two network interfaces for UDP and TCP, based on source and destination port and IP addresses. It has a very rudimentary GUI written in micropython. It responds to ICMP echo requests (ping); work is ongoing to provice more complete ICMP support (particularly for network routing)
Contributions and ports to new hardware are welcome, see the GitHub issues page for suggestions as to work to do.
Support
We gratefully acknowledge the financial support for the development of LionsOS by:
- Cyberagentur as part of the PISTIs-V Project under the Ecosystem formally verifiable IT – Provable cybersecurity (EvIT) program
- DARPA under the PROVERS program
- The UNSW John Lions Fund via the John Lions Chair
The project was in the past also supported by NIO America.
Collaboration
- For verifying LionsOS components we are collaborating with PlanV and University of Gothenburg.
- Our core collaboration partner under the DARPA PROVERS program is main contractor Collins Aerospace.
Documentation
LionsOS has its own documentation site.
Availability
LionsOS is available from the TS GitHub under a BSD license.
Latest News
- 2026-01-28: First commercial adoption of LionsOS announced.
- 2025-11-13: LionsOS-based firewall released as community project.
- 2025-03-25: Release 0.3.0 of LionsOS adding more file system support and new developer tooling.
- 2025-01-20: Cyberagentur launches the ÖViT program, which funds LionsOS through the PISTIs-V project.
- 2024-10-15: The seL4 web site runs on LionsOS!
- 2024-08-28: Our participation in the DARPA PROVERS program as a member of the INSPECTA Team will fund further development and verification of some components of LionsOS. 2024-08-06: Release 0.2.0 of LionsOS adds web server example and upgrades to the latest versions of Microkit and sDDF.
- 2024-04-17: Gernot launches LionsOS during his talk at the Everything Open conference (video recording to come).
- 2024-03-27: TS releases version 0.1.0 of LionsOS on the TS GitHub.
- 2023-11-30: NIO provides financial support for the development of LionsOS.
- 2023-09-19: Gernot Heiser discusses LionsOS at his TS R&D Update at the seL4 Summit.
Contact
- Gernot Heiser, gernot<at>unsw.edu.au
People
Current |
Past
|
Publications
|
 |
Gernot Heiser seL4: Operating systems with the reliability of mathematics IEEE Reliability Magazine, Volume 3, Number 2, June, 2026 |
|
|
|
Gernot Heiser MCS safety – an OS perspective Award Talk at RTAS'26, May, 2026 |
|
|
|
Gernot Heiser Why change the kernel when you have seL4? Keynote at KISV workshop, October, 2025 |
|
|
|
Gernot Heiser Trustworthy Systems R&D update Talk at the 7th seL4 Summit, September, 2025 |
|
|
|
Gernot Heiser It's time for truly secure operating systems CASA Distinguished Lecture, May, 2025 |
|
|
|
Gernot Heiser Will we ever have truly secure operating systems? Joint Keynote at ASPLOS and EuroSys, April, 2025 |
|
|
|
Gernot Heiser, Ivan Velickovic, Peter Chubb, Alwin Joshy, Anuraag Ganesh, Bill Nguyen, Cheng Li, Courtney Darville, Guangtao Zhu, James Archer, Jingyao Zhou, Krishnan Winter, Lucy Parker, Szymon Duchniewicz and Tianyi Bai Fast, secure, adaptable: LionsOS design, implementation and performance arXiv preprint, January, 2025 |
|
|
|
Rob Sison Verification status of time protection and Microkit-based OS services Talk at the 6th seL4 Summit, October, 2024 |
|
|
|
Gernot Heiser LionsOS: A highly dependable operating system for cyberphysical systems Keynote at International Symposium on Parallel Computing and Distributed Systems, September, 2024 |
|
|
|
Gernot Heiser LionsOS: Towards a truly dependable operating system Keynote at International Conference on Dependable Systems and Networks (DSN), June, 2024 |
|
|
|
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, Peter Chubb, Ivan Velickovic and Ben Leslie Can we put the "S" into IoT? IEEE World Forum on Internet of Things, Yokohama, JP, November, 2022 |