An x86/64 Separation Kernel for High Assurance

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

MirageOS Unikernels

From the MirageOS 3.0 release announcement:

MirageOS applications can be compiled to run as self-contained virtual machines (a few MB in size) on Xen or KVM hosts, FreeBSD’s bhyve, or even as regular Unix processes (allowing access to regular debugging tools). The system libraries themselves can be reused in traditional applications, just like any other software library.

MirageOS unikernels are written in OCaml and can be run directly on top of Muen via the Solo5 platform. Support for Muen was merged into Solo5 with pull-request #190. The port includes an implementation of muennet, thus networking is supported.

MirageOS on Muen

Since IncludeOS v0.11 was ported to run on Solo5, it should be possible to run it as subject on Muen as well. (We even got a mention in one of their blog posts).
According to the authors plans HalVM 3.0 will include a port to Solo5, which would enable Haskell subjects on Muen.

Unikernel Build

MirageOS heavily depends on the OCaml Package Manager (OPAM) as its build system. Follow the installation instructions here to setup OPAM on your system. However, do not yet install mirage until after the next step.

OCaml Compiler

These instructions have been tested with version 4.05.0 of the compiler. If you are not already using this compiler, you can create a new switch as follows:

$ opam switch 4.05.0

Then make sure you update the environment:

$ eval `opam config env`

The version 4.05.0 should be marked as the current version:

$ opam switch list
--  C 4.05.0  Official  4.05.0 release

Pin Repositories

Until new versions of MirageOS packages with Muen-specific extensions are released and included in the OPAM repository they must be pinned to specific versions:

$ opam pin add ocaml-freestanding -n --dev-repo
$ opam pin add mirage -n --kind git
$ opam pin add solo5-kernel-muen -n -y --kind git
These pins will be unnecessary as soon as Solo5 issue #194 has been closed.

Mirage Tool

After successfully adding the necessary pins, install the depext module. It handles external/system dependencies for opam packages.

$ opam install depext

Then install the mirage tool:

$ opam install -y mirage


A ready-made Docker image containing the required software to build MirageOS unikernels for Muen can be acquired by issuing the following command:

$ docker pull codelabsch/muen-mirageos

Running Unikernels

The Solo5 repository includes simple test cases, some of which can be executed on Muen in Bochs:

$ git clone
$ cd solo5
$ make

Copy the generated binary to the Muen policy object directory:

$ objcopy -O binary tests/test_hello/test_hello.muen path/to/muen/policy/obj/unikernel

Finally, emulate the system:

$ make SYSTEM=xml/mirage-solo5.xml emulate

The unikernel does not produce any VGA output but you should see the following messages in the log:

$ cat emulate/serial.out | tools/scripts/ 3
Solo5: Console: Muen Channel @ 0xffff00000, size 0x20000, epoch 0x26341161
            |      ___|
  __|  _ \  |  _ \ __ \
\__ \ (   | | (   |  ) |
____/\___/ _|\___/____/
Solo5: Memory map: 512 MB addressable:
Solo5:     unused @ (0x0 - 0xfffff)
Solo5:       text @ (0x100000 - 0x107fff)
Solo5:     rodata @ (0x108000 - 0x109fff)
Solo5:       data @ (0x10a000 - 0x10efff)
Solo5:       heap >= 0x10f000 < stack < 0x20000000
Solo5: Clock source: Muen PV clock, TSC frequency 50000000 Hz
Solo5: Net: No output channel

**** Solo5 standalone test_hello ****

Hello, World
Command line is: ''

Serving Static Website

The mirage-skeleton repository contains example unikernels. One of these examples serves a static website.

$ git clone -b mirage-dev
Currently there is a build issue on the master branch so make sure to be on the mirage-dev branch
$ cd mirage-skeleton/applications/static_website_tls

The content that will be served can be found in the htdocs directory. You can replace it with something more interesting, e.g. the Muen project website.

To build the unikernel using the mirage tool issue the following commands:

$ mirage configure -t muen
$ make depend
$ make

If all goes well an unikernel image called https.muen should be present in the current directory.

Copy it over to the Muen policy object directory:

$ objcopy -O binary https.muen path/to/muen/policy/obj/unikernel

Build and deploy the system to hardware:

$ make SYSTEM=xml/mirage-solo5-net.xml deploy

Routed Network

The following commands must be executed in the NIC Linux of the deployed Muen system.

Once the deployed system is booted, disable the standard muennet interface in NIC Linux and setup networking for MirageOS:

$ /etc/init.d/S51muennet stop
$ /usr/bin/mirage-net
The following commands must be executed on the development/host computer.

By default, the unikernel is listening on So in order to make it reachable from the host computer add a route:

$ sudo ip route add via

You should be able to ping the NIC Linux and the unikernel:

$ ping
PING ( 56(84) bytes of data.
64 bytes from icmp_seq=1 ttl=64 time=1.30 ms
$ ping
PING ( 56(84) bytes of data.
64 bytes from icmp_seq=1 ttl=37 time=3.52 ms

Finally you can point your browser to and after accepting the certificate warnings you should see the static website served by MirageOS.

Bridged Network

Instead of a routed connection, the muennet interface used by the unikernel can be bridged with the physical interface. This way the unikernel can talk directly to the local network.

Which IP address the unikernel is supposed to use is configured via the --ipv4* options that can either be passed as unikernel configure parameters or as boot parameters in the subject policy of the unikernel subject (policy/xml/subject_unikernel.xml).

To serve the website from, rebuild the static_website_tls unikernel by issuing the following commands:

$ mirage configure -t muen --ipv4= --ipv4-gateway=
$ make depend
$ make
$ objcopy -O binary https.muen path/to/muen/policy/obj/unikernel
Adjust the --ipv4* options to match your networking environment.

Then rebuild and deploy the system to hardware.

On the NIC Linux, use the mirage-net-bridge script to setup the bridging:

$ /etc/init.d/S51muennet stop
$ /usr/bin/mirage-net-bridge

If all goes well, the MirageOS unikernel should be reachable via the configured IP address.

The Website

While the previous MirageOS Unikernels article described how to build and deploy MirageOS/Solo5 unikernels as subjects on Muen in general, this article focuses on a practical use-case of the technology.

The project website is served by a MirageOS unikernel running on Muen. The article explains how to build such a system using multi-stage Docker images and then deploy it to actual hardware.

System Image Build

The following graph gives an overview of the system image build process:

Image creation

In order to be able to serve the page via the TLS stack provided by MirageOS, up to date SSL/TLS certificates are required. We use Letsencrypt certificates for that purpose.

Therefore, the first step in the build process is to check whether the currently deployed certificates are still valid. This is done using openssl:

openssl x509 -checkend 2592000 -noout -in certs/live/

The command checks whether the certificate expires within 30 days. If renewal is required, a new certificate is requested via the standalone feature of the Letsencrypt’s certbot client. The certificate files are then added as content of stage one in the multi-stage Docker build.

The complete Muen system image build consists of three Docker images:

  1. codelabsch/muen-website

  2. codelabsch/muen-mirageos

  3. codelabsch/muen-dev-env

These images can be found on our Docker Hub page. The key is to import artifacts from the previous build stage into the next one using the COPY --from syntax. The following command gives an example how to copy the generated site content from the website to the unikernel stage:

FROM codelabsch/muen-website:latest as website-content
# generate website content

FROM codelabsch/muen-mirageos:latest as unikernel
COPY --from=website-content /home/writer/ htdocs

The assembled Muen system image containing the unikernel subject serving the generated website content is copied out of the final Docker container. Because we want the target system to only boot cryptographically verified images, the image is signed using the following command (as described by the iPXE homepage):

openssl cms -sign -binary -noattr -in $IMAGE -signer $SIGN_CERT \
  -inkey $SIGN_KEY -certfile $CA -outform DER -out $SIG

Then the image and associated signature is uploaded to a webserver which is reachable by the target system.

iPXE Image Verification

In order to support image signature verification, the iPXE bootloader must be compiled with the IMAGE_TRUST_CMD option enabled:

diff --git a/src/config/general.h b/src/config/general.h
index 3c14a2cd..0c67a39d 100644
--- a/src/config/general.h
+++ b/src/config/general.h
@@ -144,7 +144,7 @@ FILE_LICENCE ( GPL2_OR_LATER_OR_UBDL );
 //#define PXE_CMD              /* PXE commands */
 //#define REBOOT_CMD           /* Reboot command */
 //#define POWEROFF_CMD         /* Power off command */
-//#define IMAGE_TRUST_CMD      /* Image trust management commands */
+#define IMAGE_TRUST_CMD        /* Image trust management commands */
 //#define PCI_CMD              /* PCI commands */
 //#define PARAM_CMD            /* Form parameter commands */
 //#define NEIGHBOUR_CMD                /* Neighbour management commands */

The following script instructs iPXE to only boot images which are deemed trusted (i.e. which have a valid signature). Besides the general networking setup steps, it fetches the Muen system image containing our MirageOS webserver subject from a given URL and then verifies the associated signature. The imgstat command is for debugging purposes and displays the current image state before booting into the verified Muen system.


imgtrust --permanent

ifopen net0
set net0/ip
set net0/netmask
set net0/gateway
set dns
imgverify muen.img
boot muen.img

The image is signed using a certificate issued by our own private CA. In order for iPXE to successfully verify such a signature, we need to embed and trust the appropriate certificates. The CERT and TRUST environment variables can be used for this:

make bin/ipxe.usb -j5 \
  DEBUG=open,x509 \
  CERT=ipxe-sign.crt,ca.crt \

This command compiles a bootable iPXE image which can be dumped onto an USB stick. The certificates specified via CERT are embedded into the image. Since embedded certificates are not automatically trusted, our CA must be specified explicitly via the TRUST option.

Explicit TRUST disables the default trust in well-known CA certificates. This is important to know if image fetching is intended via HTTPS. The CA of the webserver certificate must be explicitly added to the trusted certificates as well (if possible).

The DEBUG option is very helpful during initial testing if the image fetching or signature verification step fails for some reason.


The last step of the build process is to trigger a restart of the target system via Intel AMT functionality. The target system restarts and performs the steps depicted in the following graph:

System boot

Your minimal, unikernel-based website should now be served at the configured IP after system start.

In order to easily perform updates of the static Muen website with minimal downtime, the whole aforementioned process is scripted.