An x86/64 Separation Kernel for High Assurance

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

MirageOS Unikernels

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 and is part of the official Mirage release since version 3.5.0. The port includes an implementation of muennet, thus networking is supported.

MirageOS on Muen

Muen Version

The instructions in this article have been tested with Muen revision 1cd1f88.

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.


We provide ready-made Docker images containing all required software to build Muen system images and MirageOS unikernels. Issue the following command to get the Muen Development environment:

$ docker pull

By default, the commands given in this article are expected to be run in the muen-dev-env container. You can use the run script provided as part of the Muen repository to enter the container like so:

$ tools/docker/run.muen-dev-env \
 EXTRA_EXPOSE="--expose 4433"

The EXTRA_EXPOSE environment variable makes sure that port 4433 is accessible from outside of the container. It is required for accessing the website served by the static_website_tls unikernel as described in section "Serving Static Website".

For building MirageOS unikernels, there is a separate image, which you can acquire by issuing the following command:

$ docker pull

This container is only used for building unikernels and it is explicitly stated in this article when commands should be executed in the muen-mirageos container.

If you use Docker to build the unikernels and Muen system images, you can skip the rest of this section and continue reading at "Running unikernels".

OCaml Compiler

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

$ opam switch create 4.14.1

Then make sure you update the environment:

$ eval $(opam env --switch=4.14.1)

The version 4.14.1 should be marked as the current version:

$ opam switch list
#   switch  compiler                    description
->  4.14.1  ocaml-base-compiler.4.14.1  4.14.1

Update the Opam repository to the latest state:

$ opam update
$ opam upgrade

Mirage Tool

These instructions have been tested with MirageOS version 4.4.0. Install the mirage tool:

$ opam install -y mirage.4.4.0

Solo5 ELF tool

Since version v0.6.0, Solo5 unikernels contain a so called "application manifest", which enables support for multiple network and block devices. In order to query this information the solo5-elftool needs to be installed. For that purpose, download Solo5 and install the tool like so:

$ wget
$ tar -zxf solo5-v0.8.0.tar.gz
$ cd solo5-v0.8.0
$ ./ --only-tools
$ make install-tools

By default, the tools are made accessible by installing them in /usr/local/bin. You can change the destination directory via the DESTDIR environment variable.

Running Unikernels

Solo5 comes bundled with simple test cases, most of which can be executed on Muen in QEMU/KVM. Download Solo5 and build the tests like so:

$ wget
$ tar -zxf solo5-v0.8.0.tar.gz
$ cd solo5-v0.8.0
You only need to download the Solo5 source if you are using the muen-dev-env Docker container and have not done so in the previous step.

Then, build the tests:

$ ./
$ make

This should leave you with a Hello World unikernel ready to go, which you can find at tests/test_hello/test_hello.muen. Post-process the compiled binary with the solo5-muen-gencspec script invoking it from the Muen toplevel directory as follows:

$ tools/scripts/ [..]/solo5-v0.8.0/tests/test_hello/test_hello.muen \
 policy/xml/mirageos/cspec_src.xml policy/obj \
 --out_spec policy/xml/mirageos/component_unikernel.xml \
 --bootparams "Hi!" --disable-reset

The script generates a Muen component specification for the unikernel and copies the test_hello.muen binary to the Muen build directory. It is expected to be found in the policy/obj directory when assembling the Muen system image.

Boot parameters are optional and can be omitted. Additionally, you can specify the amount of unikernel RAM via the --ram parameter.

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:

$ tools/scripts/ 7 emulate/serial.out
Solo5: Console: Muen Channel @ 0xffff00000, size 0x20000, epoch 0x1d94c593e
            |      ___|
  __|  _ \  |  _ \ __ \
\__ \ (   | | (   |  ) |
____/\___/ _|\___/____/
Solo5: Bindings version v0.8.0
Solo5: Memory map: 514 MB addressable:
Solo5:   reserved @ (0x0 - 0x1fffff)
Solo5:       text @ (0x200000 - 0x204fff)
Solo5:     rodata @ (0x205000 - 0x206fff)
Solo5:       data @ (0x207000 - 0x20cfff)
Solo5:       heap >= 0x20d000 < stack < 0x2020d000
Solo5: Clock source: Muen PV clock, TSC frequency 2112002000 Hz

**** Solo5 standalone test_hello ****

Hello, World
Command line is: 'Hi!'
Solo5: solo5_exit(0) called
Solo5: Halted
If the following failure pops up, run the script again in order to (re-)generate the component specification and copy the unikernel binary to the expected directory: make[1]: * No rule to make target [..]/muen/policy/obj/test_hello.muen.

Serving Static Website

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

$ git clone
$ cd mirage-skeleton/applications/static_website_tls
$ git checkout 3a955d604d45
If you are using Docker containers, execute the above commands in the muen-mirageos container.
We checkout a specific revision to make sure we are using a version which is known to work.

The content that will be served can be found in the htdocs directory. You can replace it with something more interesting, e.g. an article about your successful adventures with MirageOS and Muen.

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 using the --bootparams parameter of the script.

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

$ mirage configure -t muen --ipv4= --ipv4-gateway=
$ make depend
$ make
If you are using Docker containers, execute the above commands in the muen-mirageos container.

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

As before, process the ELF binary using the script:

$ tools/scripts/ [..]/static_website_tls/https.muen \
 policy/xml/mirageos/cspec_src.xml policy/obj \
 --out_spec policy/xml/mirageos/component_unikernel.xml

The unikernel serves the website via https on port 4433. Since we are using QEMU’s host forwarding to expose networking of the emulated system to the host, we must forward this port by setting the QEMU_NETDEV_EXTRA_OPTS environment variable:

$ export QEMU_NETDEV_EXTRA_OPTS="hostfwd=tcp::4433-"
Make sure to use the same IP address that you specified in the mirage configure step.

Now once more build and emulate the system:

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

Since system startup time varies, you can check the log file to make sure networking is up and ready:

$ tools/scripts/ 2 emulate/serial.out | grep "Interface"
[    6.339000] net0: Interface added
[    6.339000] service: Interface added

Finally, you can point your browser to https://localhost:4433/ and after accepting the certificate warnings you should see the static website served by MirageOS. Congratulations, you have just successfully served yourself a website via a MirageOS unikernel running on Muen!

When deploying the system to hardware you must direct your browser to the IP address, which was used to configure the unikernel, e.g.

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 the Unipi MirageOS unikernel running on Muen. Unipi fetches the static website content to serve from a Git repository. 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 two Docker images:



These images can be found on our GitHub page. The key is to import artifacts from the previous build stage into the next one using the COPY --from syntax. The following commands serve as an example of how to copy the unikernel binary the MirageOS container to the Muen system image build stage:

FROM as unikernel
# compile unikernel

COPY --from=unikernel /home/opam/opam-repository/unipi/unipi.muen /tmp/unikernel

The assembled Muen system image containing the unikernel subject serving the Muen website 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 muen.iso -signer $SIGN_CERT \
  -inkey $SIGN_KEY -certfile $CA -outform DER -out $SIG

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

memdisk is a small kernel extracted from syslinux required to reliably boot the ISO image via HTTP(S). The files and associated signatures are 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 memdisk kernel and the Muen system image containing our MirageOS webserver subject from a given URL and then verifies the associated signatures. The imgstat command is for debugging purposes and displays the current image state before booting the verified Muen system.


imgtrust --permanent

ifopen net0
set net0/ip
set net0/netmask
set net0/gateway


imgverify memdisk
imgverify muen.iso

imgargs memdisk iso raw

The files are 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.