Using Rump kernels to run unmodified NetBSD drivers on seL4

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 and reusable OS components

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:

• Easy to reuse: It should be easy to run rump kernels in many different systems. Thus the underlying APIs that the rump kernel uses should be generalised and not tied to running in user-mode of NetBSD systems.
• Modules should be unmodified: It needs to be possible to take a NetBSD kernel component and be able to run it in a rump kernel without significant modification. Having to significantly modify modules in order to run them in user-mode would limit the quality. Additionally if a module has previously been run inside a rump kernel, any additional changes to the module should not reduce its ability to be run in a rump kernel.
• Minimal amount of extra code: The amount of additional code required to support the module should be minimal. In order to provide a benefit over requiring the full NetBSD kernel as support to run the single driver, running it in the rump kernel should require less overall code. This will also enable the rump kernel to be more resource efficient and faster to initialise.
• Easy to add new components: It should be easy to add components to the rump kernel. Again, in order to make module reuse low effort.
• Modules should still act the same way: There should be a low performance impact and the modules should still function the same way.

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: net, dev and 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.

The Rumprun Unikernel

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.

Why do we care about this for seL4?

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.

Some initial network throughput benchmarks

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:

• Rumprun on seL4: Our system that we built.
• Rumprun on BMK (Bare metal kernel): A bare metal ia32 target that Rumprun already supports.
• Native NetBSD: A native NetBSD kernel built from the same sources of the unikernel.
• Linux: A Linux kernel running an up to date Debian distribution.

All configurations ran on a single CPU with background tasks disabled on an Intel Corporation 82579LM Gigabit Network card.
We note that:

• All four systems max out the network capacity before reaching more than 25% CPU utilisation.
• Both Rumprun configurations have a lower CPU utilisation than the native NetBSD configuration.
• Our seL4 version has minimal overhead compared to the native BMK version. Most of this overhead is caused by older hardware features such as I/O Port instructions and using an older programmable interrupt controller (PIC) than is available on newer systems. Overhead caused by IPC send and receive is actually quite small.
• NetBSD, Rumprun on BMK and Rumprun on seL4 which all use the same driver implementation all have a higher overhead than the equivalent Linux driver.

 

How to use

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:

• Building a rump kernel sysroot 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.
• Building the base Rumprun unikernel for seL4.
• Building the rumprun-bake tool which takes a program (that was built using the above tool-chains) and the base Rumprun unikernel image and generates a single ELF file.
• Builds a simple hello world application and bakes it into a single ELF file using the above tools.
• Builds a seL4 root task which contains the simple hello world application in a CPIO archive
• Builds a seL4 kernel image.

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
bmk_platform_halt@kernel.c:95 All is well in the universe.

Rust

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

Short(er) term goals

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:

• CAmkES: Make it possible to run Rumprun unikernels inside CAmkES components. This should be fairly straight forward will require changing the seL4 Rumprun init code to work in a CAmkES component environment rather than the environment that our simple root-task provides.
• ARM: Add support for running on ARM platforms. Currently have less of an idea of how hard this will be. Rumprun and rump kernels do support ARM platforms already, but there is less device driver support.
• Rump kernels without Rumprun: We use Rumprun because it performs much of the rump kernel initialisation and management for us. We sometimes want to use rump kernels without any user-level POSIX support and in different configurations that Rumprun wasn’t designed for which means starting to provide more of our own implementations of the rump kernel interfaces that we currently rely on Rumprun for.

Still interested in seL4?

Other Projects

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:

• CAmkES: A component architecture for building static systems.
• Robigalia: A project aiming to “Build a robust Rust ecosystem around seL4” and also “Create a highly reliable persistent capability OS, continuing the heritage of EROS and Coyotos”.
• RefOS: A reference OS implementation on seL4.
• Genode OS Framework: A multi-server OS framework that supports seL4.

Want to learn?

• Tutorials: The getting started page has links to tutorials for a first introduction using seL4 and CAmkES.

Get involved

• Mailing list: Subscribe to the seL4 mailing lists. Whenever stuck on a problem involving seL4, don’t hesitate to ask a question here.
• IRC: Join our IRC channel.
• Wiki: Our wiki contains frequently asked questions and more about seL4. Contributions are welcome.
• Github: Our github projects are https://github.com/sel4, https://github.com/sel4proj.

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.