Trustworthy Systems

Our Partners Breakaway Consulting Defence Science and Technology Group

The seL4 Core Platform

Aim

Design, implementation and evolution of the seL4 Core Platform, a small, simple, lightweight, easy to use, yet flexible operating system personality on seL4.

Problem

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.

Solution

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.

seL4CP abstractions

Approach

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 Channel, which allows them to communicate. Memory objects can be connected to a Channel to enable shared-memory communication.

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

  1. initialisation, which gets invoked by the system exactly once before any other of the PD's code;
  2. notification, which is invoked another PD has performs a notiry() operation on a Channel;
  3. protected (optional), which is invoked when another PD of lower priority performs a ppcall() operation through a Channel.

On-going work

seL4PD functionality

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.

seL4 Verification

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

Support

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.

Collaborations

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.

Documentation

Contact

People

Current