Muen

An x86/64 Separation Kernel for High Assurance

Checkout source code
This page is served by a MirageOS/Solo5 TLS unikernel running on Muen

Overview

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 Networked Solutions (INS) 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. Hardware passthrough is realized using Intel’s VT-d DMA and interrupt remapping technology. This enables the secure assignment of PCI devices to subjects.

Muen is under active development and verification of kernel properties is ongoing.

Features

Kernel

The following list outlines the most-prominent features of the Muen kernel:

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

  • 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

  • PCI device passthrough using Intel VT-d (DMAR and IR)

  • PCI config space emulation

  • Support for Message Signaled Interrupts (MSI)

  • Minimal Zero-Footprint Run-Time (RTS)

  • Event mechanism

  • Shared memory channels for inter-subject communication

  • Crash Audit

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

    • Native 64-bit Ada subjects

    • Native 64-bit SPARK 2014 subjects

    • Linux 32/64-bit VMs

    • Genode x86_64 base-hw system [genode]

    • Windows 32-bit VMs

    • MirageOS unikernels [mirageos]

Muen supports the hardware-accelerated virtualization of Microsoft Windows through the use of a fully de-privileged variant of VirtualBox [vbox] running inside a strongly isolated VM subject on top of Genode’s base-hw kernel. See the release notes of the Genode OS Framework version 16.08 [genode_muen] for more information about this exciting feature.

Components

The Muen platform includes re-usable components which implement common services:

  • Device Manager (DM) written in SPARK 2014

  • Subject Monitor (SM) written in SPARK 2014

  • Subject Loader (SL) written in SPARK 2014

  • Timeserver subject written in SPARK 2014

  • Debugserver subject written in Ada 2012

  • PS/2 driver subject written in Ada 2012

  • Virtual Terminal (VT) subject written in Ada 2012

Furthermore the [muenfs] and [muennet] Linux kernel modules provide virtual filesystem and network interface drivers based on inter-subject memory channels.

Toolchain

The Muen platform includes a versatile toolchain which facilitates the specification and construction of component-based systems in different application domains.

The [mugenhwcfg] tool for automated hardware description generation simplifies the addition of support for new target machines. Scheduling plans can be generated automatically from a scheduling configuration using the [mugenschedcfg] tool.

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

The Muen sources are available through the following git repository:

$ git clone --recursive https://git.codelabs.ch/git/muen.git

A browsable version of the repository is available here:

https://git.codelabs.ch/?p=muen.git

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

https://git.codelabs.ch/?p=muen.git;a=snapshot;h=HEAD;sf=zip

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

Build

Environment

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

Operating systems

Debian GNU/Linux 8/9 x86_64
Ubuntu 16.04.1 x86_64

Ada compiler

GNAT GPL 2017

GCC version

6.3.1 20170510 for GNAT GPL 2017

SPARK version

GPL 2017

Emulator

Bochs (>= version 2.6.5)

Intel AMT SoL client

amtterm (>= commit 0ece513…​)

Intel vPro AMT / WSMan

amtc (github.com/schnoddelbotz/amtc)

The following hardware is used for the development of Muen. There is a good chance similar hardware works out-of-the box if the microarchitecture is Ivy Bridge or newer.

Lenovo ThinkPad X260

Skylake

i7-6500U

Intel NUC 6i7KYK

Skylake

i7-6770HQ

Intel NUC 6CAYH

Apollo Lake

Celeron J3455

Intel NUC 5i5MYHE

Broadwell

i5-5300U

Cirrus7 Nimbus

Haswell

i7-4765T

Lenovo ThinkPad T440s

Haswell

i7-4600U

Lenovo ThinkPad T430s

Ivy Bridge

i7-3520M

Intel NUC DC53427HYE

Ivy Bridge

i5-3427U

Kontron Technology KTQM77/mITX

Ivy Bridge

i7-3610QE

The first step to build Muen is to install the required packages:

$ sudo apt-get install acpica-tools binutils-dev git-core gnuplot \
    grub-pc-bin lcov libc6-dev libelf-dev libiberty-dev libxml2-utils make \
    tidy wget xorriso xsltproc zlib1g-dev

The Ada and SPARK packages currently available in Debian and Ubuntu are too old to build Muen. GNAT/SPARK GPL 2017 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
For SPARK Discovery GPL 2017 you additionally need to install the z3 and cvc4 provers. Follow these instructions in the SPARK user guide <<sparkug>.

Docker

There is also a ready-made Docker image which contains all necessary tools for Muen development. You can install it using the following command:

$ docker pull codelabsch/muen-dev-env

Compilation

To build the Muen tools, RTS, kernel and example components change to the Muen source directory and issue the following command:

$ make

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

On Ubuntu 16.04.1 you might encounter an error of the form:

/usr/lib/x86_64-linux-gnu/crti.o: unrecognized relocation (0x2a) in section .init

If this is the case, rename the linker binary ld of GNAT GPL 2016 in order to use the one provided by Ubuntu.

$ cd /opt/gnat/libexec/gcc/x86_64-pc-linux-gnu/4.9.4
$ mv ld ld-archive

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.

Download Bochs from its project site and issue the following commands to build and install it with /usr/local prefix:

$ sudo apt-get install g++ libsdl1.2-dev
$ tar xfvz bochs-2.6.5.tar.gz
$ cd bochs-2.6.5
$ ./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.

As Bochs is missing IOMMU and PCI MMCONF emulation, device passthrough is not supported for this hardware target.

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 HARDWARE=hardware/lenovo-t440s.xml SYSTEM=xml/demo_system_vtd.xml iso

Then follow the instructions on the screen.

Network Boot

For fast deployment of the Muen system image to real hardware, the iPXE [ipxe] boot firmware installed on a USB stick in conjunction 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:

$ sudo apt-get install liblzma-dev
$ git clone git://git.ipxe.org/ipxe.git
$ wget https://muen.sk/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 system image from the following URL:

http://192.168.254.1:8000/muen.img

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=hardware/intel-nuc-dc53427hye.xml

References

License

Copyright (C) 2013-2018  Reto Buerki <reet@codelabs.ch>
Copyright (C) 2013-2018  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.