Our Partners
Design, implementation and evolution of the seL4 Microkit, (formerly the “seL4 Core Platform”) a small, simple, lightweight, easy to use, yet flexible framework and SDK for developing statically-architected systems on seL4.
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.
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.
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:
init, which is invoked by the system exactly once
before any other of the PD's code;
notified, which is invoked when another PD has performed
a notify() operation on a CC connected to this PD;
protected (optional), which is invoked when another
PD of lower priority performs a ppcall()
operation through a CC connected to this PD.
Besides platform and architecture ports, and adding verification support, we are working on enhancing the Microkit by adding dynamic features, specifically:
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.
A major activity is the formal verification of the Microkit's implementation and initialisation.
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.
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.
The Microkit is open source
and available on the seL4
Foundation GitHub under a BSD License.
Current |
Past
|
|
 
|
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 |