About the seL4 Kernel

This text describes how to quickly get started developing seL4 projects on a BeagleBone Black. seL4 is a formally verified micro kernel with the following properties (see https://sel4.systems/Info/FAQ/proof.pml for proof assumptions):

  • the implementation behaves according to the specification, i.e. no implementation bugs exist, which means..
  • no buffer overflows
  • no null pointer dereferences
  • no pointer errors in general
  • no memory leaks
  • no arithmetic overflows and exceptions
  • no undefined behavior
  • etc

Development Machine Setup

Start by installing Ubuntu 16.04. Then run the following commands.

Basic packages needed for seL4 development

sudo apt install build-essential realpath libxml2-utils python-tempita gcc-multilib ccache ncurses-dev
sudo apt install git repo cmake ninja-build clang gcc-multilib gcc-arm-none-eabi binutils-arm-none-eabi libncurses-dev libxml2-utils libssl-dev libsqlite3-dev libcunit1-dev expect python-pip
pip install sel4-deps
pip install camkes-deps
sudo apt install curl
curl -sSL https://get.haskellstack.org/ | sh # Or using apt, but the package lags behind a bit, sudo apt install haskell-stack
sudo apt install qemu-system-arm # Only needed for QEMU
sudo apt install qemu-system-x86 # Only needed for QEMU
      

To compile for BBB

All of these packages may not be needed, I use the arm-linux-gnueabi- toolchain to compile for BBB.

sudo apt install binutils-arm-linux-gnueabi
sudo apt install gcc-arm*
sudo apt install g++-arm-linux-gnueabi
      

For serial console debugging

sudo apt install minicom
      

To compile RefOS

pip install lxml
      

Projects to Start with

These projects are a good start for testing and learning the seL4 ecosystem.

Downloading the Code

sel4test

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

CAmkES

mkdir camkes
cd camkes
repo init -u https://github.com/seL4/camkes-manifest.git
repo sync
      

RefOS

mkdir refos
cd refos
repo init -u https://github.com/seL4/refos-manifest.git
repo sync
      

Compiling it!

Use the following scripts in the repo root folder of each project. By default the scripts compile the BBB binary, update the recipe variable to compile for simulation.

sel4test

#!/bin/sh

set -e # abort script on error
recipe="bbb"

if [ $recipe = "arm-qemu" ] ; then
  echo "Building a defconfig for arm to run on QEMU"
  make clean
  make kzm_simulation_release_xml_defconfig
  make silentoldconfig
  make
elif [ $recipe = "bbb" ] ; then
  echo "Building the BeagleBone Black defconfig"
  make clean
  make bbone_black_debug_xml_defconfig
  make
else
  echo "recipe not recognized"
fi
      

CAmkES

The CAmkES project needs a defconfig for the BBB.

wget -O configs/arm_simple_bbone_black_defconfig http://mokshasoft.com/seL4/defconfig/arm_simple_bbone_black_defconfig
      
#!/bin/sh

set -e # abort script on error
recipe="bbb"

if [ $recipe = "arm-qemu" ] ; then
  echo "Building a defconfig for arm to run on QEMU"
  make clean
  make arm_simple_defconfig
  make silentoldconfig
  make
elif [ $recipe = "bbb" ] ; then
  echo "Building the BeagleBone Black defconfig"
  make clean
  make arm_simple_bbone_black_defconfig
  make
  elf="images/capdl-loader-experimental-image-arm-am335x"
  arm-linux-gnueabi-objcopy -O binary $elf $elf.bin
else
  echo "recipe not recognized"
fi
      

RefOS

The RefOS project needs a defconfig for the BBB.

wget -O configs/bbone_black_debug_defconfig http://mokshasoft.com/seL4/defconfig/bbone_black_debug_defconfig
      
#!/bin/sh

set -e # abort script on error
recipe="bbb"

if [ $recipe = "arm-qemu" ] ; then
  echo "Building a defconfig for arm to run on QEMU"
  make clean
  make kzm_debug_defconfig
  make silentoldconfig
  make
elif [ $recipe = "bbb" ] ; then
  echo "Building the BeagleBone Black defconfig"
  make clean
  make bbone_black_debug_defconfig
  make silentoldconfig
  make
  elf="images/refos-image"
  arm-linux-gnueabi-objcopy -O binary $elf $elf.bin
else
  echo "recipe not recognized"
fi
      

Running the Binaries on BBB

Copy the binary (*.bin) in the images folder to the root of a FAT32 formatted SD card and insert it in the BBB.

Boot by interrupting U-boot using an FTDI serial cable

  1. Connect the J1 on the BBB to the black cable on the FTDI connector
  2. Connect the USB side of the FTDI cable to the dev machine
  3. Turn off hardware flow control (sudo minicom -s; Serial port setup -> Hardware Flow Control)
  4. Run, sudo minicom -D /dev/ttyUSB0 -b 115200
  5. Connect the power cable to the BBB
  6. Interrupt the boot process by pressing ENTER quickly a few times
  7. Follow instructions on how to boot from the SD card

Boot from the SD card

Enter these commands in the U-boot prompt (=>)

setenv sel4bin <bin-file> # the name of the binary file in the SD card root
setenv loadaddr 0x82000000
fatload mmc 0 ${loadaddr} ${sel4bin}
go ${loadaddr}
      

The loadaddr can be found by tracing the build with strace, and searching for the -Ttext switch in the last ld command.
strace -s 1000 -f -o make.strace -e trace=process make V=1

Running the Binaries on QEMU

Close QEMU with 'Ctrl-a x' after the programs have finished.

sel4test

qemu-system-arm -nographic -M kzm -kernel images/sel4test-driver-image-arm-imx31
      

CAmkES

qemu-system-arm -nographic -M kzm -kernel images/capdl-loader-experimental-image-arm-imx31
      

RefOS

qemu-system-arm -nographic -M kzm -kernel images/refos-image
      

Contact

Contact me if you have any questions or comments on seL4 or this tutorial.

+46 707 31 06 27

jonas.cl@protonmail.com