Our Partners
Design, implementation and evolution of the seL4 Core Platform, a small, simple, lightweight, easy to use, yet flexible operating system personality on seL4.
The seL4 ecosystem lacked an OS that 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. This creates a high barrier to uptake for seL4.
Experience also shows that many developers are not using the seL4 mechanisms most effectively, resulting in inefficient designs.
The seL4 Core Platform (seL4CP) is a lightweight OS 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.
The core abstraction of the seL4CP 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 seL4CP's process abstraction. Its code structure has of 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 notiry() 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 seL4CP by 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 seL4CP's implementation and initialisation.
The development of the seL4CP was supported by an ICERA Grant awarded by the Australian Department of Defence to Breakaway Consulting, with Trustworthy Systems as a project partner. The seL4CP was co-developed with the Laot device for protecting critical infrastructure.
The seL4CP was jointly designed by TS and Breakaway, and implemented by Breakaway. We continue to collaborate with Breakaway on the on-going development of seL4CP.
Current |
Past
|
 
|
  |
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 |