Limited support is now available for running unmodified NetBSD drivers on seL4 using rump kernels. We have modified the Rumprun unikernel to use seL4 as a supported platform on ia32 and x86_64. This makes it possible to run unmodified POSIX applications on Rumprun on seL4. The Rumprun unikernel uses NetBSD rump kernels to provide operating system (OS) components such as device drivers and filesystems so that applications can be run without an underlying OS. Sample applications that can be run on the Rumprun unikernel can be found here. Our fork can be found here and a sample project that demonstrates seL4 support can be found here. This blog post will go into some detail about what rump kernels are, why we want to use them in user-level on seL4, how to setup and run applications on Rumprun on seL4 and conclude with a list of our goals for the near future concerning rump kernels and seL4.
Rump kernels are a project that aims to make NetBSD OS components more portable to allow reuse in other systems. Device drivers, filesystems and networking modules can be run inside a rump kernel in an unmodified way.
The rump kernel can then be easily ported to run in different configurations such as in a different OS, on top of a POSIX application interface or as its own system. This is made possible by a set of common software interfaces that are designed to provide low level OS primitives to the rump kernel. The rump kernel then uses these primitives to support the NetBSD OS components.
Rump kernels were designed with the following considerations:
In order to achieve these requirements the rump kernel picked a modular design. Common kernel functionality is provided by the core rump module and three extra modules known as the three factions:
vfs which contain common functionality for networking, device and filesystem components. Each NetBSD OS component is provided as a different module. A component for an Ethernet card driver has its own module. Different components are provided in different modules. If the Ethernet card is connected to a PCI bus, the driver for the PCI bus is in a different module from the Ethernet card driver module. Modules for components that are not needed in the rump kernel do not need to be provided. This reduces the amount of code required to run rump kernels compared to running the NetBSD kernel.
Modules are linked together with user applications and even other modules either through direct symbol linking, providing or using device VFS nodes through the
vfs subsystem or by registering system-call implementations to the rump kernel’s syscall table. Adding additional custom modules is fairly easy – all the components exist in the same address space so additional modules can be compiled and linked into the binary in the same way.
Rump kernels can be used in different configurations. There are two configurations relevant to seL4. In one configuration, the rump kernel runs in the same process and address space as the single application that is using it. In this configuration the rump kernel is used as a library OS for a single application running in that environment. Underlying software or hardware is used to isolate different applications, each with their own rump kernel, from each other. This is the configuration that the Rumprun unikernel uses. The other configuration is a remote configuration where the rump kernel is used to implement a server that provides certain OS system services. This could be used to provide fault isolation between NetBSD OS components running in different rump kernels in a system such as CAmkES or other multi-server OS design built on seL4.
Rumprun is a unikernel project that uses a rump kernel to provide OS functionality to singular POSIX applications. This library OS design is commonly used when an application does not require the support of a full time-sharing operating system. Its system architecture is shown above. The POSIX application is linked against a
libc and other supporting libraries. The
libc can then dispatch syscalls which the rump kernel handles either through direct access to hardware or by calling lower level platform interfaces. The entirety of the unikernel runs in the same address space. Therefore it would be possible for the POSIX application to bypass the rump kernel and interact with low level hardware directly. This is allowed because the Rumprun unikernel assumes that it is running on a hypervisor and the hypervisor is providing fault isolation and protection between different applications, where each application runs inside its own Rumprun unikernel. Currently on seL4 we use a separate root task to configure a new Rumprun unikernel process which is isolated from the rest of the system apart from the initial seL4 capabilities that it is given.
seL4 is a microkernel with highly critical applications. Real-world cyber-physical systems can use seL4 for increased security. However, to run seL4 on a wide range of heterogeneous devices, driver software is required, which is millions of lines of code that we don’t have, therefore limiting seL4’s deployment. Allowing driver reuse will increase the number of drivers that work with seL4 so as to ultimately increase the range of real world devices that can be made more secure.
Our current approach involves using a virtualised Linux kernel to provide device drivers, otherwise drivers have to be re-implemented on an as-needed basis. The Linux approach is very heavy handed and does not necessarily scale well if we want to isolate drivers from each other which would require separate Linux instances – driving up overheads. Re-implementing drivers is also non-ideal as it requires a large engineering effort and still can’t necessarily capture the benefits that widely tested mature drivers can give you.
We see rump kernels as a way of being able to reuse device drivers (and filesystems and networking stacks) from NetBSD which targets a wide range of platforms and has a reasonable amount of driver support. The low overhead, both in terms of run-time binary size and metrics such as I/O throughput and CPU utilisation, that rump kernels claim is appealing.
Adding support for the Rumprun unikernel to use seL4 as a target platform gave us a way to evaluate the rump kernel claims and get a feel for how easy it is to reuse NetBSD components.
A slightly more comprehensive analysis of performance and our design can be found here. We generally found that the drivers that we tested perform well enough and the claim that the NetBSD drivers can be used unmodified holds true. After getting the networking drivers working, the work required for other drivers, such as USB was quite straight-forward.
We used Iperf3, a networking benchmark to measure CPU utilisation against different levels of TCP network throughput on a 1Gb network. We measured four different configurations:
All configurations ran on a single CPU with background tasks disabled on an Intel Corporation 82579LM Gigabit Network card.
We note that:
If you want to test this out, there is a git repository rumprun-sel4-demoapps which contains a few sample applications such as a hello world, Redis server, NGINX and a Rust TCP echo server.
If you haven’t built seL4 projects before then you will need to set up the required dependencies.
Note: to test that you have correctly set up your dependencies it might be a good idea to test that the seL4-test project correctly passes all tests.
To checkout and build a Rumprun on seL4 image you will need to run the following commands in a fresh directory:
repo init -u https://github.com/SEL4PROJ/rumprun-sel4-demoapps.git repo sync source scripts/init-all.sh make hello-ia32-x86_64_qemu_defconfig make
This results in:
build2/ia32/rumprun. Tool-chains can be found in
build2/ia32/rumprun/bin. These tool-chains are needed to build any program that runs on seL4.
hello worldapplication and bakes it into a single ELF file using the above tools.
hello worldapplication in a CPIO archive
The seL4 kernel image and seL4 root task are needed to run your project.
To run the final images on qemu (a i386-compatible hardware simulator):
qemu-system-i386 -m 512 -nographic -kernel images/kernel-ia32-pc99 -initrd images/roottask-image-ia32-pc99 # quit with Ctrl-A X
To run on actual bare-metal hardware you can load seL4 images using grub2 or via PXEBOOT. The seL4 wiki has instructions on how to do this here.
You should expect to see something similar to the output below:
... Rump on seL4 ============ ... rump kernel bare metal bootstrap Starting paddr: 0x110d8000 Copyright (c) 1996, 1997, 1998, 1999, 2000, 2001, 2002, 2003, 2004, 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016 The NetBSD Foundation, Inc. All rights reserved. Copyright (c) 1982, 1986, 1989, 1991, 1993 The Regents of the University of California. All rights reserved. NetBSD 7.99.34 (RUMP-ROAST) total memory = 39872 KB timecounter: Timecounters tick every 10.000 msec timecounter: Timecounter "clockinterrupt" frequency 100 Hz quality 0 cpu0 at thinair0: rump virtual cpu root file system type: rumpfs kern.module.path=/stand/i386/7.99.34/modules ... === calling "hello" main() === Hello world1 1sec 10sec === main() of "hello" returned 0 === === _exit(0) called === rump kernel halting... syncing disks... done unmounting file systems... unmounted tmpfs on /tmp type tmpfs unmounted rumpfs on / type rumpfs unmounting done halted firstname.lastname@example.org:95 All is well in the universe.
Rust supports a rumprun x86_64 target which also works on seL4. To run a rust TCP echo server on seL4 you can build one using the commands below:
curl https://sh.rustup.rs -sSf | sh -s -- -y --default-toolchain nightly # this installs rust globally rustup target add x86_64-rumprun-netbsd make clean make rust-x86_64-x86_64_qemu_defconfig make qemu-system-x86_64 m 512 -nographic -kernel images/kernel-x86_64-pc99 -initrd images/roottask-image-x86_64-pc99 -cpu Haswell
Currently our support for rump kernels only supports ia32 or x86_64 architectures and only a single Rumprun unikernel running in its own process in user-space on seL4. We are excited to extend this however so that we can start using rump kernels in a much wider variety of seL4 related applications. Our current goals are:
seL4 is a microkernel and not a fully fledged operating system – we rely on user-level for that. Other interesting projects that aim to provide a wider range of OS support for building and running applications on seL4 are listed below:
We are currently committed to providing support for using rump kernels on seL4. Feel free to post questions or issues to the seL4 developers mailing list, or opening issues on Github.