Our Partners

The seL4 Microkit

Aim

Design, implementation and evolution of the seL4 Microkit, a small, simple, lightweight, easy to use, yet flexible framework and SDK for developing statically-architected systems on seL4.

Problem

The seL4 ecosystem lacked a framework was easy to use for engineers building IoT/embedded/cyberphysical systems on seL4. This calls for an SDK that integrates with a developer's preferred development environment, rather than prescribing use of the complex build system used for the seL4 kernel (which creates a high barrier to uptake).

Experience also shows that many developers are not using the seL4 mechanisms most effectively, resulting in inefficient designs.

Solution

The Microkit is a programming model and SDK that provides a small number of simple abstractions that are very close to seL4 abstractions, and as such lend themselves to very efficient implementation. The simplicity of the abstractions rule out a number of inappropriate design patterns naturally lead to using seL4 abstractions in the way they are meant to be used. It also enables verification using fully-automated (“push-button”) techniques.

Approach

The core abstraction of the Microkit is the protection domain (PD), which encapsulates the seL4 concepts of VSpace (address space), CSpace (access rights), thread (execution), scheduling context (right to use the CPU), and Notification (semaphore-like synchronisation primitive). A PD also has executable code and a scheduling priority.

Two PDs can be connected by a Communication Channel (CC), which allows them to communicate. Memory objects can be connected to PDs to enable shared-memory communication.

The PD is the Microkit's process abstraction. Its code structure has three entry points:

1. init, which is invoked by the system exactly once before any other of the PD's code;
2. notified, which is invoked when another PD has performed a notify() operation on a CC connected to this PD;
3. protected (optional), which is invoked when another PD of lower priority performs a ppcall() operation through a CC connected to this PD.

On-going work

Microkit functionality

Besides platform and architecture ports, and adding verification support, we are working on enhancing the Microkit by adding dynamic features, specifically:

• exception handling
• starting and stopping PDs
• re-initialising PDs
• live-upgrading PD implementation
• late-loading PDs.

Our ultimate goal is to support systems with static architecture (i.e., the set of PDs) but fully dynamic implementation, including dynamic connections and a degree of dynamic allocation of memory regions to PDs. We also plan to support multi-processing PDs.

Microkit Verification

A major activity is the formal verification of the Microkit's implementation and initialisation.

Lions OS

The Microkit forms the basis for the Lions OS, a new, modular, high-performance OS we are developing.

Support

The development of the microkit was supported by an ICERA Grant awarded by the Australian Department of Defence to Breakaway Consulting, with Trustworthy Systems as a project partner. The microkit was co-developed with the Laot device for protecting critical infrastructure.

Collaborations

The microkit was jointly designed by TS and Breakaway, and implemented by Breakaway. We continue to collaborate with Breakaway on the on-going development of the microkit.

Documentation

• Microkit tutorial
• Microkit Manual
• Report on evolving the Microkit into a dynamic OS of 2022-03-26
• Guide for migrating from CAmkES to Microkit of 2023-04-11, latest available here

Availability

The Microkit is open source and available on the seL4 Foundation GitHub under a BSD License.

Latest News

• 2023-09-20: Ivan Velickovic presents the Microkit at the seL4 Summit.
• 2023-09-15: TS releases the Microkit tutorial.
• 2023-09-08: The seL4 Core Platform has been adopted by the seL4 Foundation and renamed the seL4 Microkit.
• 2022-10-10: Zoltan Kocsis presents the Microkit and our work on verifying it at the seL4 Summit.

Contact

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

People

Publications

		Trudy Weibel, Zoltan Kocsis, Mathieu Paturel, Rob Sison, Isitha Subasinghe and Gernot Heiser Verifying the seL4 Microkit https://trustworthy.systems/publications/papers/Weibel_KPSSH_24.pdf, June, 2024
		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, 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