PC99

seL4 runs on 32-bit ia32 and 64-bit x64 machines, on qemu and on hardware.

Simulation

Checkout the sel4test project using repo as per seL4Test

repo init -u https://github.com/seL4/sel4test-manifest.git
repo sync
make x64_simulation_debug_xml_defconfig
# The defconfig provides a set build configuration. You can use `make menuconfig` to customize build settings further if necessary.
make
make simulate-x86_64

Generated binaries can be found in the images/ directory.

Real Hardware

When running on real hardware console output will be over serial. You will need to plug a serial cable into your machine to see any output.

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
}

Booting via PXEBOOT using syslinux PXELINUX requires setting up a tftp and dhcp server on the network that the machine you want to boot is connected to. This debian page explains how to setup a tftp and dhcp server, and the syslinux site has a download for pxelinux which we load over PXEBOOT that then can load seL4. The configuration for pxelinux.cfg/default is provided below.

label seL4
        kernel mboot.c32
        append kernel-ia32-pc99 --- apps-ia32-pc99

Booting off USB with syslinux

Use syslinux to create a bootable USB stick as follows.

Assuming your USB flash drive is at /dev/sdb with a FAT partition at /dev/sdb1:

install-mbr /dev/sdb
syslinux --install /dev/sdb1
mount /dev/sdb1 /mnt
cp images/sel4test-driver-image-ia32-pc99 /mnt/rootserver
cp images/kernel-ia32-pc99 /mnt/sel4kernel
cat > /mnt/syslinux.cfg <<EOF
SERIAL 0 115200
DEFAULT seL4test
LABEL seL4test
    kernel mboot.c32
    append sel4kernel --- rootserver
EOF
cp /usr/lib/syslinux/modules/bios/mboot.c32 /mnt
cp /usr/lib/syslinux/modules/bios/libcom32.c32 /mnt
umount /mnt

Use fdisk to make sure the first partition is bootable.

And you’re done. Output will come on the serial port

Some more information about some of the hardware we use: