The Muen Separation Kernel

Trustworthy by Design – Correct by Construction

The Muen Separation Kernel is the world’s first Open Source microkernel that has been formally proven to contain no runtime errors at the source code level. It is developed in Switzerland by the Institute for Internet Technologies and Applications (ITA) at the University of Applied Sciences Rapperswil (HSR). Muen was designed specifically to meet the challenging requirements of high-assurance systems on the Intel x86/64 platform. To ensure Muen is suitable for highly critical systems and advanced national security platforms, HSR closely cooperates with the high-security specialist secunet Security Networks AG in Germany.

Example Architecture

A Separation Kernel (SK) is a specialized microkernel that provides an execution environment for components that exclusively communicate according to a given security policy and are otherwise strictly isolated from each other. The covert channel problem — largely ignored by other platforms — is addressed explicitly by these kernels. SKs are generally more static and smaller than dynamic microkernels, which minimizes the possibility of kernel failure, enables the application of formal verification techniques and the mitigation of covert channels. Muen uses Intel’s hardware-assisted virtualization technology VT-x as core mechanism to separate components. The kernel executes in VMX root mode, while user components, so called subjects, run in VMX non-root mode.

Note
Muen is currently a prototype implementation. We do not yet consider it to be fit for production use.
Features

Features

  • Minimal SK for the Intel x86/64 architecture written in the SPARK language

  • Full availability of source code and documentation

  • Proof of absence of runtime errors

  • Multicore support

  • Nested paging (EPT) and memory typing (PAT)

  • Fixed cyclic scheduling using Intel VMX preemption timer

  • Static assignment of resources according to system policy

  • Event mechanism

  • Shared memory channels for inter-subject communication

  • Minimal Zero-Footprint Run-Time (RTS)

  • Support for 64-bit native and 32/64-bit VM subjects

Resources

Resources

Documentation

The following detailed project documentation is available:

Mailing list

The muen-dev@googlegroups.com mailing list is used for project announcements and discussions regarding the Muen separation kernel.

Download

Download

The Muen sources are available through the following git repository:

$ git clone http://git.codelabs.ch/git/muen.git

A browsable version of the repository is available here:

A ZIP archive of the current Muen sources can be downloaded here:

Note
The ZIP archive cannot be used to build the example system since it does not contain all sub-projects.
Build

Build

The Muen SK has been developed and successfully tested using the development environment listed in the following table.

Operating system

Debian GNU/Linux 7 (wheezy), x86_64

Ada compiler

GNAT GPL 2013 (20130314)

GCC version

4.7.4 20130416 for GNAT GPL 2013 (20130314)

SPARK version

GPL 2012

Emulator

Bochs from svn (>= r12175)

Hardware

Lenovo T430s with Intel Core i7 3520M

Intel AMT SoL client

amtterm (>= commit 0ece513…)

Install the Debian packages needed to build Muen:

$ sudo apt-get install binutils-dev git-core iasl libc6-dev-i386 wget xorriso zlib1g-dev

The Ada and SPARK packages currently available in Debian wheezy are too old to build Muen. GNAT GPL 2013 and SPARK 2012 from AdaCore’s [libre] site must be installed instead. Extend your PATH to make the GPL compiler and tools visible to the Muen build system (assuming that they are installed below /opt):

$ export PATH=/opt/gnat/bin:/opt/spark/bin:$PATH

Because the linker of GNAT GPL 2013 is not multiarch [march] aware, export the C run-time LIBRARY_PATH:

$ export LIBRARY_PATH=/usr/lib/x86_64-linux-gnu/

To build the Muen tools, RTS, kernel and example subjects on Debian wheezy change to the Muen source directory and issue the following commands:

$ git submodule init
$ git submodule update
$ export SPARK_DIR=/opt/spark
$ make

This will create an image containing the example system which can be booted by any Multiboot [mboot] compliant bootloader.

Deploy

Deploy

The build system provides two ways to instantly deploy and test the created system image.

Emulation

To ease kernel development, the Muen project makes use of emulation by employing the Bochs IA-32 emulator [bochs]. Among many other features, Bochs has support for multiple processors, APIC emulation and VMX extensions.

Muen needs a recent Bochs version from the project’s subversion repository. Issue the following commands to checkout, build and install Bochs with /usr/local prefix:

$ sudo apt-get install libsdl1.2-dev
$ svn checkout svn://svn.code.sf.net/p/bochs/code/trunk bochs-code
$ cd bochs-code/bochs
$ ./configure           \
    --prefix=/usr/local \
    --enable-vmx=2      \
    --enable-smp        \
    --enable-cdrom      \
    --enable-x86-64     \
    --enable-avx        \
    --with-sdl
$ make
$ sudo make install

Issue the following command in the Muen project directory to start emulation:

$ make emulate

The Bochs emulator output is located at emulate/bochsout.txt, the Muen kernel serial console output is written to emulate/serial.out.

Hardware

The top-level Makefile provides two convenient targets to deploy Muen to real hardware: iso and deploy. The first creates a bootable ISO image which can be burned on a CD-ROM or dumped on a USB stick, the second uses network boot to shorten round-trips during development.

USB Stick

To create a bootable USB stick containing the Muen system, enter the following commands in the top-level directory:

$ make iso
$ sudo cat emulate/muen.iso > /dev/sdX
$ sync

The /dev/sdX device is the USB stick (e.g. /dev/sdc, without partition number). All existing data will be erased.

If your hardware differs from the default configuration, additionally specify the HARDWARE variable:

$ make iso HARDWARE=lenovo-t430s

Network Boot

For fast deployment of the Muen system image to real hardware, the iPXE [ipxe] boot firmware installed on a USB stick in conjuction with Intel Active Management Technology (AMT) is used. Please refer to the amtterm [amt] documentation on how to configure AMT on the target hardware.

To build and install iPXE with the Muen specific boot script issue the following commands:

$ git clone git://git.ipxe.org/ipxe.git
$ wget http://muen.codelabs.ch/muen.ipxe
$ cd ipxe/src
$ make bin/ipxe.usb EMBED=../../muen.ipxe
$ sudo dd if=bin/ipxe.usb of=/dev/sdX

The /dev/sdX device is the USB stick (e.g. /dev/sdc, without partition number). All existing data will be erased.

When booting from the created stick the first NIC (net0) is configured as follows:

IP Address : 192.168.254.2
Netmask    : 255.255.255.0
Gateway    : 192.168.254.1

After initialization of the network adapter iPXE tries to download and boot the kernel from the following URL:

http://192.168.254.1:8000/kernel

The development machine must be connected to the target hardware via an interface with IP address 192.168.254.1. To actually serve the created system image to the bootloader, issue the following command in the top-level Muen directory:

$ export AMT_PASSWORD=<your AMT password>
$ make deploy

To view the output of the Muen kernel debug console use the command:

$ amtterm 192.168.254.2

If your hardware differs from the default configuration, additionally specify the HARDWARE variable:

$ make deploy HARDWARE=lenovo-t430s
References

References

License

License

Copyright (C) 2013, 2014  Reto Buerki <reet@codelabs.ch>
Copyright (C) 2013, 2014  Adrian-Ken Rueegsegger <ken@codelabs.ch>

This program is free software: you can redistribute it and/or modify it under
the terms of the GNU General Public License as published by the Free Software
Foundation, either version 3 of the License, or (at your option) any later
version.