Trustworthy Systems

Usermode OS components on seL4 with rump kernels

Authors

Kent McLeod

    School of Computer Science and Engineering
    UNSW,
    Sydney 2052, Australia

Abstract

seL4 is a formally-verified high-assurance microkernel that provides isolation to properly designed applications that it executes. Real-world cyber-physical systems can use seL4 for increased security. Many applications rely on the operating system to provide system services, such as device drivers, file systems and networking capabilities, however seL4 only provides these in a limited capacity which limits its deployment. Adding support to this wide array of systems that can benefit from the additional security seL4 provides would require reimplementing the millions of lines of operating system code that these systems require. This is infeasible without an approach that reuses existing components. Current methods either require providing services by running a paravirtualised version of the Linux kernel which provides only coarse isolation or by developing specific services on an as-needed basis which does not scale for many devices. Rump kernels are a NetBSD project for running NetBSD system services in different environments such as in user-mode on a microkernel.

This thesis evaluates rump kernels as an approach to provide driver-like operating system com- ponents in user-mode on the seL4 microkernel. This will be achieved by adding a seL4 platform to the Rumprun unikernel, an existing project that uses rump kernels. We evaluate our implementation to compare its performance with other software systems and to investigate the level of overhead our implementation adds. We also show that the effort required to use rump kernels is low and by using NetBSD system services we increase the amount of devices that can be used with seL4. This thesis contains background information and related work, details on our design and implementation and our evaluation, future work and conclusion.

BibTeX Entry

  @mastersthesis{McLeod:be,
    address          = {Sydney, Australia},
    author           = {Kent {McLeod}},
    month            = oct,
    paperUrl         = {https://trustworthy.systems/publications/theses_public/16/McLeod%3Abe.pdf},
    school           = {School of Electrical Engineering and Telecommunication},
    title            = {Usermode {OS} Components on {seL4} with Rump Kernels},
    year             = {2016}
  }

Download