An x86/64 Separation Kernel for High Assurance
Reto Buerki 7f41b2748e Fix muenblock reference in README 1 month ago
common Increase XSAVE_Area_Size constant to 4 Kb 3 months ago
components Time: Adapt pragma Warning accept message 1 month ago
config Re-enable -gnatyt switch 1 month ago
contrib contrib: Update ada-bfd to latest upstream version 1 month ago
deploy Add deploy targets for GUDE EPC power bar 6 months ago
doc Doc: Update MirageOS article 11 months ago
emulate Prepend $(E) wrapper with @ 3 months ago
kernel Fix warnings reported by -gnatyt 1 month ago
pack Prepend $(E) wrapper with @ 3 months ago
policy Policy: Increase log channel size for Genode systems 2 months ago
projects Only generate tests for root project 1 month ago
rts Prepend $(E) wrapper with @ 3 months ago
tools Fix warnings reported by -gnatyt 1 month ago
.arcconfig Set explicit repository callsign in .arcconfig 2 years ago
.arclint Enable Arcanist spelling linter 5 years ago
.gitignore Amend .gitignore (Emacs backup files) 1 year ago
.gitmodules Add Libxhcidbg library as submodule 2 years ago
.travis.yml Travis: Add script for Debian GNU/Linux 10 (Buster) 1 month ago
AUTHORS Update AUTHORS, README 5 years ago
COPYING Adjust SK specific COPYING note 6 years ago
Makeconf Makeconf: Include 3 months ago
Makefile Makefile: Drop extra colon 1 year ago
Makespark Makespark: Make proof target work for -jX (X > 1) 2 months ago
README Fix muenblock reference in README 1 month ago


The Muen Separation Kernel

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[codelabs GmbH].
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, codelabs
closely cooperates with the high-security specialist secunet Security Networks
AG in Germany.

image::example.svg[Example Architecture, width=70%, align="center"]

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.

NOTE: Muen is under active development and verification of kernel properties is


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
- SMP for Linux VMs
- Genode x86_64 base-hw system <>
- Windows 32-bit VMs
- MirageOS unikernels <>

Muen supports the hardware-accelerated virtualization of Microsoft Windows
through the use of a fully de-privileged variant of VirtualBox <> 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 <> for
more information about this exciting feature.

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 <>, <> and <> Linux kernel modules
provide virtual filesystem, network interface and block I/O drivers based on
inter-subject memory channels.

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

The <> 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
<> tool.


The following detailed project documentation is available:

* Muen project report +

* Muen project presentation +

* Muen toolchain document +

* Presentation given at High Integrity Software Conference HIS 2014 +

* Technical articles on Muen +

Mailing list
The mailing list is used for project announcements and
discussions regarding the Muen Separation Kernel.

* To subscribe to the list, send a (blank) mail to
Note: A Google account is *not* required, any email address should work.
* To post a message to the list write an email to
* The list has a Google Groups web interface:

The Muen sources are available through the following git repository:

$ git clone --recursive

A browsable version of the repository is available here:

A ZIP archive of the current Muen sources can be downloaded here:;a=snapshot;h=HEAD;sf=zip

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


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

| Operating systems | Debian GNU/Linux 9/10 x86_64 +
Ubuntu 18.04 x86_64
| Ada compiler | GNAT GPL 2019
| GCC version | 8.3.1 20190518 for GNAT Community 2019
| SPARK version | Community 2019
| Emulator | Bochs (>= version 2.6.5)
| Intel AMT SoL client | amtterm (>= commit 0ece513...)
| Intel vPro AMT / WSMan | 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 T480s | Kaby Lake | i7-8650U
| 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 bc binutils-dev bison flex 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 Community 2019 from AdaCore's <> 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

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

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

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 <> compliant bootloader.

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

To ease kernel development, the Muen project makes use of emulation by
employing the Bochs IA-32 emulator <>. 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 \
$ 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`.

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

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
<> boot firmware installed on a USB stick in conjunction with Intel Active
Management Technology (AMT) is used. Please refer to the amtterm <>
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://
$ wget
$ 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 :
Netmask :
Gateway :

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

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

$ export AMT_PASSWORD=
$ make deploy

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

$ amtterm

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

$ make deploy HARDWARE=hardware/intel-nuc-dc53427hye.xml

- [[[mboot]]] Multiboot Specification,
- [[[bochs]]] Bochs IA-32 Emulator,
- [[[ipxe]]] iPXE boot firmware,
- [[[amt]]] Intel AMT SoL client + tools,
- [[[libre]]] AdaCore Libre,
- [[[genode]]] Genode OS Framework,
- [[[genode_muen]]] Genode 16.08 release notes,
- [[[vbox]]] VirtualBox,
- [[[mirageos]]] MirageOS,
- [[[muenblock]]] Muenblock Linux kernel module,
- [[[muenfs]]] Muenfs Linux kernel module,
- [[[muennet]]] Muennet Linux kernel module,
- [[[mugenhwcfg]]] Muen hardware config generator,
- [[[mugenschedcfg]]] Muen scheduling plan generator,

Copyright (C) 2013-2019 Reto Buerki
Copyright (C) 2013-2019 Adrian-Ken Rueegsegger

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