This page is a quick start for working with seL4 and its ecosystem.
Background and terminology
There are many repositories. Of the most significant are:
The seL4 kernel is built as part of project. Each project has a README.md associated with it which provides further information.
Projects are a collection of git repositories, with versions managed by Android’s Repo tool. Each project consists of an XML manifest file which specifies the source dependencies, and directory structure of a project. See the RepoCheatsheet page for a quick explanation of how we use Repo and some common commands.
A subset of available projects are described below, for a full list see the list of released projects:
- verification, the seL4 proofs.
- seL4test, a test suite for seL4, including a Library OS layer.
- seL4bench, a microbenchmarking suite for seL4.
- CAmkES, a component architecture for embedded systems based on seL4. See the CAmkES pages for more documentation about CAmkES.
- x86 Camkes VMM a component-based virtual machine monitor for ia32 platforms using Intel VT-X and VT-D extensions.
Hardware and Target Platforms
Read the Hardware pages to see a list of supported platforms, and special instructions for particular hardware platforms.
Setting up your machine
Read the Host Dependencies page to find instructions on how to set up your host machine.
We use a CMake-based build system to manage dependencies.
This section presents a case study, by the end of which you can run seL4test on a simulator.
Fetching, Configuring and Building seL4test
To build a project, you need to:
- check out the sources using Repo,
- configure a target build using CMake,
- build the project using Ninja.
- Use repo to check sel4test out from GitHub. Its manifest is located in the
mkdir seL4test cd seL4test repo init -u https://github.com/seL4/sel4test-manifest.git repo sync
- Configure a x86_64 build, with a simulation target to be run by Qemu:
mkdir build-x86 cd build-x86 ../init-build.sh -DPLATFORM=x86_64 -DSIMULATION=TRUE ninja
The target configurations available for each project are potentially different depending on what the project supports. Building/Using describes how projects can generally be configured.
- The build images are available in
build-x86/images, and a script
build-x86/simulationthat will run Qemu with the correct arguments to run seL4test.
- On success, you should see:
Test VSPACE0002 passed </testcase> <testcase classname="sel4test" name="Test all tests ran"> </testcase> </testsuite> All is well in the universe
For more information on seL4test see its project page.
Using real hardware
See Hardware for supported hardware and how to set it up.
The seL4 and CAmkES Tutorials are an introduction to the design of seL4, and also to preparing to develop for seL4, and they are also used internally to train new seL4 engineers. You are strongly encouraged to complete the tutorials if you are new to seL4: they will quickly bring you up to speed and ready to practically contribute.
You can find a long list of seL4 publications here:
- seL4 is free: What does this mean for you? (2015).
- From L3 to seL4: What have we learned in 20 years of L4 microkernels? (2014).
If you have ideas or questions, please use the mailing lists: