Getting Started

In general, if you’re just getting started, you want to dive into the seL4 tutorials, then the CAmkES tutorials, then the seL4 Test suite. There’s a section on this page for each.

Aims

This page seeks to comprehensively assist new seL4 developers or interested parties to easily obtain the correct tools to duplicate the internal seL4 development environment, successfully build the seL4 tutorials, and successfully follow the seL4 tutorials.

It’s introductory – after you’ve followed these steps, you’ll be at the crest point where you can confidently begin reading the seL4 API kernel manual with a functional copy of the kernel on your own machine. From that point, the guidance for what you should do with the functional source copy that you have will come from your own intuition, interest and hopefully, inspiration that seL4 gives you.

Code

All seL4 code and proofs are available on GitHub, at https://github.com/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:

Projects

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

We modeled 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 so far are:

Other projects may be added later.

Supported Target Platforms

Read the Hardware pages to see a list of supported platforms, and special instructions for particular hardware platforms.

Setting up your machine

You can setup all the dependencies on your local OS, or you may choose to use Docker.

Using Docker

You can also use Docker to isolate the dependencies from your machine. Instructions for using Docker for building seL4, CAmkES, and L4v can be found here.

Using your local OS

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

Get Google’s “Repo” tool

Repo is a tool by Google used for managing multiple git repositories. All the seL4 related projects use multiple subprojects, and Repo will fetch all of them and place them in the correct subdirectories for you. To get repo, follow the instructions in the section “Installing Repo” here. (You don’t need to initialise a repo client yet.)

Using Repo to fetch an seL4 project and its subprojects

Choose a project to start with. As an example, we’ll use sel4test.

Getting cross compilers

There are instructions on how to get cross compilers for building ARM. We only have direct instructions for Debian/Ubuntu/Fedora, but we imagine you should be able to substitute where necessary for your distro. Instructions should be similar for other distros, links to toolchains for other distros are provided.

Start with the tutorials

The seL4 and CAmkES Tutorials are an excellent, holistic introduction to the design of seL4, and also to preparing to develop for SEL4, and they are also used internally to train new seL4 developers. 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.

Get acquainted with seL4Test

Any changes you make to seL4 should pass the tests in seL4 Test, and pull requests to seL4 which are non-trivial or related only to documentation, should come with a matching pull request and new test (if applicable) to the seL4Test repository as well.

seL4test is a comprehensive unit and functional testing suite for seL4 and can be useful when porting to new platforms or adding new features.

Project Layout

See Build System Anatomy for details of project layouts and the seL4 build system.

Configuration files in the configs directory 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.

Running on real hardware

See Hardware.

Contributing

Gernot’s presentation: seL4 is free: What does this mean for you? (2015) outlines areas where the kernel could use some contributions – other than that, gauging what you can do externally is for the time being, difficult. If you have ideas, please feel free to visit the NICTA mailing lists and chime in:

Learn more about seL4

For someone just getting to know about seL4 and wanting to first at least understand how to build it, so that you can get comfortable with editing the source code, the following pre-init steps might help you get more context, before you try building, so you have at least a conceptual understanding of exactly what sort of creature you’re about to step into the arena with. These are not pre-requisites for building the kernel, but they will help you a lot in understanding what you’re dealing with.

Publications

There are many publications available on the design of the seL4 kernel, documenting every design decision and the justifications for each one. Consider trying to read some of them, or at least scrolling through the list, and picking out the most eye-catching titles and skimming them. You can find a long list of seL4 publications here:

The seL4 project page at Data61.

Youtube