Overview

We have developed a series of tutorials to introduce seL4 and developing systems on seL4.

List of tutorials

The tutorials are split into a number of broad categories, and have been designed around developer needs.

  • The seL4 tutorials are for people keen to learn about the base mechanisms provided by the seL4 kernel. The kernel API is explained with short exercises that show basic examples.

  • MCS introduces seL4 Mixed-Criticality System extensions, which are detailed in this paper and PhD.

  • Libraries provides walkthroughs and exercises for using the libraries provided in seL4_libs, which were developed for rapidly prototyping systems on seL4.

  • CAmkES generates the glue code for interacting with seL4 and is designed for building high-assurance, static systems. These tutorials demonstrate how to configure static systems through components.

  • Microkit enables system designers to create static software systems based on the seL4 microkernel. We recommend this as a potential introduction to seL4, bearing in mind that the Microkit hides many of the seL4 mechanisms - it is designed that way, to make building on top of seL4 easier.

  • Rust allows people to write safer user-level code on top of seL4 without needing full formal verification, with a language that is receiving increasing interest and that aligns extremely well with security and safety critical embedded systems programming.

Recommended reading

Note that all of these tutorials require C programming experience and some understanding of operating systems and computer architecture. Suggested resources for these include:

Resources

Additional resources to assist with learning:

Next: Pathways through the tutorials