Code

All seL4 code and proofs are available on github, at https://github.com.au/seL4, under standard open-source licenses.

There are several repositories; the most interesting ones are the project repositories (whose names end in -manifest) and these two:

seL4 projects

The seL4 kernel is usually built as part of project. Each project has a wiki entry associated with it that gives more information. The information on this page is common to all of them.

We modelled the seL4 development process on the Android development process. Each project consist of an XML file that describes which repositories to use, and how to lay them out to make a buildable system.

The available projects at release are:

Other projects may be added later.

Running the Proofs

Information about how to get started with the seL4 proofs.

Supported Target Platforms

Platforms that are supported in general are in the following list. Not all projects support all these platforms.

To build for the ARM targets you will need a cross-development toolchain.

Getting a project

These instructions are for building on Linux. They assume you already know the basics of using the command line, compilers, and GNU Make.

Get repo

The latest repo is available from Google at https://storage.googleapis.com/git-repo-downloads/repo. Download it, and put it somewhere in your PATH

mkdir -p ~/bin
export PATH=~/bin:$PATH
curl https://storage.googleapis.com/git-repo-downloads/repo > ~/bin/repo
chmod a+x ~/bin/repo

repo relies on git and python which should be available in your distribution packaging system.

On Debian or Ubuntu:

sudo apt-get install git python

On Fedora, CentOS or RedHAT

sudo yum install git python gpg

Using repo

Choose a project to start with. As an example, we'll use sel4test. First create a directory to work in, and initialise it using repo:

mkdir seL4test
cd seL4test
repo init -u https://github.com/seL4/sel4test-manifest.git

This will download the latest version of repo from Google, and the manifest for the seL4test project. To get the actual source, you'll then need to use repo sync:

repo sync

repo will churn through for around ten minutes fetching all the repositories needed.

Toolchains and Prerequisites

To build a seL4 project you need the appropriate toolchain. sel4test needs only the appropriate compiler, linker and GNU make. For running the images, qemu is desirable.

Building the project

Each project has an associated wiki, accessible via github, that has up-to-date dependencies and instructions. The general instructions here apply to all projects.

The top level layout of all projects is similar. After a build it looks something like this:

$ ls -F
Kbuild@   Makefile@  build/    images/   kernel/  projects/  tools/
Kconfig@  apps@      configs@  include/  libs/    stage/
build
contains built files.
apps
is a symlink to a subdirectory of projects containing the source for applications.
configs
is a symlink to a subdirectory of projects containing default configurations
images
contains the final linked ready-to-run artefacts after a build
include
is where header files from libraries and the kernel are staged
kernel
contains the seL4 kernel
libs
contains the source to libraries
projects
is a placeholder for project-specific parts
stage
is where built libraries are put
tools
contains parts of the build system, and other tools needed to build a project

Configuration files in configs are named by target machine, then something about what they do. Most have either `release' or `debug' in their names. Debug kernels are built with debug symbols (so one can use gdb), enable assertions, and provide the sel4debug interfaces to allow debug printout on a serial port.

Some configurations are intended to run under qemu. Because qemu does not produce a completely faithful emulation of the hardware, sometimes features have to be disabled or worked around. These configurations have ‘simulation’ in their names.

To get started, choose a target to build for, and find the name of the corresponding config file.

For example, let's build seL4test for ia32, to run on the QEMU simulator:

make ia32_simulation_release_xml_defconfig

This copies configs/ia32_simulation_release_xml_defconfig to ./.config, and sets up various header files.

You can look at the configuration options using

make menuconfig

Alternatively you can use any text editor to change ./.config; if you change anything you need to rebuild header files with make oldconfig. It's advisable also to make clean to clear out anything already built — the build system does not track as many dependencies as it ought to.

For the ia32 target you should not have to change anything. For ARM targets you may need to change the cross-compiler prefix in the menuconfig under toolchain options

When you've configured the system, you can build by doing

make

After about five or ten minutes, depending on how fast your machine is, this should finish with a pair of files in images.

Currently parallel builds do not work, so don't try to speed things up by using -j. The build system does however support ccache if you have it installed.

Simulating the result

make simulate-ia32

There is a make target to run under qemu for some of the targets. Look in the Makefile for details. On Debian you will need a recent qemu — the one in Wheezy is too old, and does not support the KZM or Beagle targets. The one in Jessie is OK.

To exit qemu after the All is well in the universe message that indicates the test suite has passed, type control-a c q

Useful configuration options

Cross compiler prefix

For cross compilation (targetting ARM), you can set the cross compiler triple. This will typically be arm-linux-gnueabi- or arm-none-eabi-. Do make menuconfig and look for toolchain-options

Some of the default configurations specify a particular x86 compiler. It is usually safe to set the triple to the empty string when building for x86, if you have a multilib gcc installed.

Fiddling with most of the other configuration options will lead to systems that will either not compile, or not run.

Caveats

kzm simulation hangs

qemu does not simulate all the timers needed for a full sel4 test run. Use the kzm_simulation_ configurations to avoid tests that rely on unimplemented timers.

arm-none-eabi

If you use arm-none-eabi compilers, the prebuilt libraries will fail to link, with a message something like

  /usr/lib64/gcc/arm-none-eabi/4.8.1/../../../../arm-none-eabi/bin/ld: warning: /usr/src/seL4test/stage/arm/imx31/lib/libmuslc.a(internal.o) uses 32-bit enums yet the output is to use variable-size enums; use of enum values across objects may fail

To fix, do make menuconfig visit seL4 Libraries→Build musl C Library and untick libmuslc use precompiled archive then do make clean and attempt to rebuild.

hard float compilers

The default configuration on newer compilers from Debian and Ubuntu use hardware floating point. Binaries built with these compilers are incompatible with the prebuilt musl C library. You can either tweak the flags (in tools/common/Makefile.flags: add -mfloat-abi=soft to NK_CFLAGS) or disable the use of the prebuilt libraries as above.

Running on real hardware

Details of how to boot seL4 on hardware vary from system to system.

IA32

The build system produces a multiboot compliant image for x86; a grub2 stanza is here, but we usually boot via PXE for convenience.

 menuentry "Load seL4 VM"  --class os {
   load_video
   insmod gzio
   insmod part_msdos
   insmod ext2
   set root='(hd0,msdos2)'
   multiboot /boot/sel4kernel
   module /boot/sel4rootserver
}

ARM platforms

Load from u-boot, from SD card or flash, or using fastboot or tftp. Most applications have two parts: treat the `kernel' part as a kernel, and the `application' part like an initrd. If there is only one part to an image (e.g., seL4test for some platforms) treat it like a kernel.

Detailed instructions differ from board to board. See The General Hardware Page for general instructions; it has links to board specific instructions as well.

Debian cross compilers

Unfortunately Debian is in a state of flux between the old ‘Use Emdebian’ and the new MultiArch system. This was meant to be fixed for Jessie; but for now you can either:

  1. Use an old compiler, with bugs that have been fixed in newer releases
  2. Install a compiler from Mentor Graphics (formerly Code Sourcery), or
  3. Build a cross compiler from source

CAmkES defconfigs want specific compiler

Most of the x86 default configurations for CAmkES use the triple i686-pc-linux-gnu- which is the 32-bit CodeSourcery compiler. It is usually safe to use whatever your system x86 compiler is — just set this field to blank in the .config file.