seL4 on the Raspberry Pi 3


seL4 is an L4 microkernel with an end-to-end, machine-checked proof of correctness. It’s a neat project: and ever since it was released under the GPLv2, I’ve been meaning to play with it. Newer versions even have verified ARM multicore and FPU support!

I wanted to run it on my spare Raspberry Pi 3 (the other one has a camera and other gadgets attached at the moment). Unfortunately I hit a few errors on the way; this is just a note for everybody on how to quickly get it working.

Now, there is a blog post containing these instructions (in more words) from the seL4 research blog itself, posted earlier this year. However, following the wiki lead to a few dead end links, and the post had not been updated with some of the blog comments pointing to a U-Boot bug I encountered, burning half an hour of my time.

You’ll need a microSD card (like the one already inside your Pi) and a UART-to-USB adapter cable. I’m using a slightly older version of this Adafruit cable, which is simple and works fine. But plenty of other things would work too, such as a Bus Pirate or something.

Preparing the SD card

First off, get any microSD card (of essentially size) and wipe it as a FAT32 filesystem. I’m using a simple 4GB SanDisk SD card. (seL4 is so small there’s essentially no reason to use a large SD card, if you can find a small one.)

The first two things you need are the Rasbperry Pi bootloader and GPU firmware blobs. On bootup, an on-chip bootloader accesses the SD card, and boots the Second-Stage Bootloader (SSBL). The SSBL then finds the GPU firmware (based on the ThreadX RTOS) and boots that to turn on the GPU. These two blobs are proprietary.

Once the GPU is configured, it then executes a bootloader or application of the users choosing. In our case, we’re going to have the GPU firmware boot U-Boot, which will proceed to load our own ELF executable containing seL4.

You can grab these files from this location. You’ll need bootcode.bin and start.elf. bootcode.bin is the SSBL, while start.elf is the GPU firmware which will proceed to load U-Boot.

Finally, write out a config.txt file on the microSD card, with these contents:

$ cat > config.txt
enable_uart=1
kernel=u-boot.bin

This tells the GPU firmware to boot U-Boot (which we’ll build shortly) located in u-boot.bin, and to enable the UART pins with the default settings.

Building seL4 and seL4’s testsuite

seL4 has… difficult build requirements. It also has an extremely fine-grained repository structure, managed by Google’s repo tool (used by Android), which uses an XML based configuration system to check out repositories at checkpoints (such as a tag or branch). It also uses this configuration in order to determine how to “build” a project structure, by symlink repositories, and their subdirectories/subprojects, into the required locations for the build system after checking them out.

Because seL4 is a microkernel, there are many various things like the test suite that are structured as seL4 “applications”. repo allows you to structure projects around this idea, where you have many pieces that are loosely coupled, and need various subsets of libraries or project components. You use a “manifest” to describe the seL4 components you need, the kernel, libraries, utilities, repo checks them out, sets them up, and you can develop your application independently inside this ‘framework’ it creates for you. This allows you to structure projects with relatively fine control over what you use and where it comes from. You can mix and match repositories, forks, etc. All of this is described by a “manifest” repo that contains information about what components you need, and how to structure them.

The first time I tried using it, it took a few hours to get it all working. (And needless to say I’ve found tools like repo easy to screw up and annoying.)1

But there’s good news: while I’d dearly appreciate a nicer setup, since the first time I tried it – most of these problems can be avoided! The Data61 team has since made some Dockerfiles available which should help you get started very quickly. I was sweating thinking about this originally, but this setup went surprisingly smooth.

If you want to get dirty with seL4, repo and the above points are unavoidable, I think, but otherwise you should be able to get started very quickly.

First, on any Linux machine with Docker already installed, clone the seL4/CAmkES/L4v Dockerfiles:

$ git clone https://github.com/SEL4PROJ/seL4-CAmkES-L4v-dockerfiles.git
$ cd seL4-CAmkES-L4v-dockerfiles

Next, create a directory anywhere else on your system. I just created a directory in ~/tmp:

$ mkdir -p $HOME/tmp/sel4test

Now, drop into a docker container containing all of the needed build tools:

$ make user HOST_DIR=$HOME/tmp/sel4test

This will put you inside a Docker container, under a /host directory, which is mapped to the above HOST_DIR directory, with all the required build tools. Only this directory is available, and it will contain the seL4 source code and build artifacts.

Now, we need to clone the sel4test code, which we do using repo and the sel4test “manifest” repository. This can be done using repo init and repo sync:

$ repo init --config-name -u https://github.com/seL4/sel4test-manifest.git
$ repo sync

When this is done, the source code will be checked out:

$ ls
apps  CMakeLists.txt  configs  Kbuild  Kconfig	kernel	libs  Makefile	projects  tools

Now, you need to do a slight fix since it seems there’s a minor build break in the seL4 source code at the time of this writing: you need to create a symlink to libsel4testsupport under libs/ (remember how repo is easy to screw up?):

$ cd libs/
$ ln -s ../projects/sel4test/libsel4testsupport/ libsel4testsupport
$ cd ..

Now, you can compile with the default RPi3 debug configuration, and build the seL4 image:

$ make rpi3_debug_xml_defconfig
$ make

When this completes, the seL4 ELF binary, which runs the seL4 test suite, will be located under images/ under the name sel4test-driver-image-arm-bcm2837. Copy this to the microSD card under the name kernel.img:

$ cp images/sel4test-driver-image-arm-bcm2837 <mount point>/kernel.img

Building U-Boot

The easiest way to build U-Boot is to just do it inside the same Docker container that was used for seL4. The simplest reason for this is that it already has the ARM cross compiler.

Inside the seL4 container, clone U-Boot and compile it. Note: There is a bug in versions of U-Boot after v2017.01 that causes seL4 to fail to boot. You must use U-Boot v2017.01 with the Raspberry Pi 3.

$ git clone git://git.denx.de/u-boot.git
$ cd u-boot
$ git checkout -b tmp v2017.01
$ make CROSS_COMPILE=arm-linux-gnueabi- distclean
$ make CROSS_COMPILE=arm-linux-gnueabi- rpi_3_32b_defconfig
$ make CROSS_COMPILE=arm-linux-gnueabi- u-boot.bin

Done. Copy the resulting u-boot.bin to the microSD card, along with bootcode.bin and start.elf.

UART cable

For the next step, you’ll need a UART cable attached to the GPIO pins on the Pi, in order to drop into the U-Boot console and modify its environment parameters. This is necessary as the default bootcmd parameters do not properly load the seL4 kernel from the microSD card otherwise.

You need 3 pins hooked up: Pin 6 is ground (black), Pin 8 is TX (white), Pin 10 is RX (green). Remember: UART cables and pins for TX/RX are reversed (e.g. on the adafruit cable, the white pin is RX, which attaches to P8/TX on the Pi).

Use minicom to drop into a serial console on /dev/ttyUSB0 (or whatever dmesg tells you was just attached). Baud is 115200, parameters 8N1 (8-bits, no partiy, 1 stop). No hardware/software flow control.

Fixing the U-boot environment parameters

The final problem we have to fix is that the U-Boot parameters will not properly find the seL4 kernel without a little help. But this is easy to fix.

With the UART cable plugged in, plug in the microUSB cable to power on the Pi. You should see the U-Boot begin booting, and after it scans the bus, you will have 2 seconds to hit any key to stop autoload. Go ahead and do this, and you’ll get dropped into a U-Boot console:

U-Boot 2017.01 (Sep 15 2017 - 06:23:32 +0000)

DRAM:  128 MiB
RPI 3 Model B (0xa02082)
MMC:   bcm2835_sdhci: 0
reading uboot.env
In:    serial
Out:   lcd
Err:   lcd
Net:   Net Initialization Skipped
No ethernet found.
starting USB...
USB0:   Core Release: 2.80a
scanning bus 0 for devices... 3 USB Device(s) found
       scanning usb for storage devices... 0 Storage Device(s) found
       scanning usb for ethernet devices... 1 Ethernet Device(s) found
Hit any key to stop autoboot:  0
U-Boot>

You can now look at the contents of your SD card:

U-Boot> fatls mmc 0
   358576   u-boot.bin
  2870564   start.elf
    50248   bootcode.bin
       32   config.txt
  3385548   kernel.img

5 file(s), 0 dir(s)

U-boot is configured by an environment file named uboot.env located next to u-boot.bin on the microSD card. This file configures environment variables in U-boot, which can simply be variables or even contain other commands to run (similar to a simplified Bash script).

We need to tweak the U-boot environment parameters and save the environment to the SD-card, so we can properly reboot the Pi every time.

This is very easy to achieve:

U-Boot> setenv bootfile kernel.img
U-Boot> setenv bootcmd 'fatload mmc 0 ${loadaddr} ${bootfile}; bootm ${loadaddr}'
U-Boot> saveenv

The first line sets the bootfile variable to kernel.img, the location of the ELF image we want to boot (which could be anything, not just seL4).

The second environment sets the bootcmd variable, and this variable contains a sequence of commands to run, which perform the default boot sequence. fatload mmc 0 ${loadaddr} ${bootfile} requests U-Boot to load the ELF image inside bootfile, on SD/MMC card 0, to the in-memory address loadaddr (already configured for us). bootm ${loadaddr} simply boots the in-memory ELF file at the given address.

With all that done, you can reset your Pi 3, and watch the seL4 test suite begin running:

U-Boot> reset

  1. A previous version of this post had a part about the early development of seL4 and its possible influence on the repository structure, but this was incorrect. It originally implied there were many teams, stiching together the final result. But there were really only 3 teams (and 2 of those were so related that they later became 1). The “component” based repository layout described above was a choice made independently of this by the developers. And the seL4 team has plans to improve the build situation too, which is great news!

    Thanks to Adrian Danis for clarification.


Return to the homepage. π
more contrast