Introduction

We will introduce MirageOS, the target audience, and the scope of this handbook.

MirageOS

MirageOS is a library operating system, where for each service a separate binary - a so-called unikernel - is used. MirageOS is not a generic purpose operating system. Each unikernel has a single purpose and is executed as a virtual machine.

Each unikernel is tailored to its need, and only contains the pieces of code that are strictly required for its operation: our firewall unikernel doesn't include user management, a file system. The firewall is only a single process: there is no process management and no userland vs kernel space process switching, and also no virtual memory included.

A MirageOS unikernel is minimal in size - this means that the resource consumption is low since only a tiny binary is kept in memory, and no unnecessary code is executed (i.e. a cronjob indexing the files on your file system).

In addition, MirageOS unikernels are developed in the memory-safe and statically typed programming language OCaml, which catches lots of bugs at compile time (static type system) and reduces the attack vectors (spatial and temporal memory safety issues - buffer overflow and underflows).

It is crucial to have a programming language that enforces memory safety in the setting with single address space, otherwise an attacker (from a bug in one library) could access all the memory of the other libraries. MirageOS comes with some C code, which is compiled with defense-in-depth features.

The benefits of MirageOS unikernels are (a) lower resource consumption, (b) smaller attack surface, (c) avoidance of memory safety attacks, and (d) reduced operational complexity.

Target audience and requirements

The reader of this handbook are persons who want to operate MirageOS unikernels. There won't be any OCaml code in this handbook. You don't need an OCaml compiler for this handbook. Only the operational aspects are discussed, for example how to setup networking.

Of course, you as an OCaml or MirageOS developer can use your custom unikernel instead of the stock ones provided.

You will need a hypervisor, supported are Linux kvm, FreeBSD BHyve, and OpenBSD VMM.

It is suggested to have a x86 laptop or server with one of the operating systems and the required hardware support for virtualization.

Within the handbook, we will link to reproducible binaries of the specific unikernels, available from builds.robur.coop. The unikernels are built on a daily basis using the latest releases of OCaml packages.

Our focus on running MirageOS as a hardware-supported virtual machine (also named hvt) has multiple reasons:

• from a security point of view, it leverages the CPU virtualization features, and only uses a tiny API to the host operating system,
• we are able to ship binaries that run on either of the hypervisors, no need for custom binaries depending on the hypervisor.
• it is our preferred target, and we run it since nearly a decade!

Other MirageOS targets

MirageOS supports more targets we will only discuss briefly in this section. If you want to read more, take a look at the Solo5 documentation

Unix

The default target of MirageOS for development is unix -- this uses the normal network stack by default (via the sockets API). It is nice for development, but security-wise it is not a good solution for deployment.

Linux seccomp

The Linux seccomp target uses restrictive seccomp rules and allows only a few system calls to be executed. This does not require a hypervisor, and can be executed similar to a container. From a security perspective, the attack surface is slightly bigger - it is the seccomp implementation. From the network operations perspective, this is the same as what we discuss in this handbook. Since we don't provide pre-built unikernel binaries for seccomp, you'll need to compile them yourself. And instead of executing solo5-hvt, you need to run solo5-spt.

Xen

MirageOS was originally developed by some people who also worked on Xen. Xen is a great hypervisor, but very different from the modern ones, which rely on CPU features. The Xen target is used with MirageOS, but the network setup is very different, thus we won't focus on that in this handbook.

Muen separation kernel

The Muen separation kernel is developed in Ada/SPARK - which includes a verification framework. It is a great project, and if you plan to deploy high-assurance solutions, you should dive deeper into Muen. Since its operation and configuration is custom, we won't discuss it further in this handbook.

Virtio

Virtio allows to run virtual machines on the cloud, where the hypervisor is managed for you by some company. This allows to deploy MirageOS onto the cloud. Since the configuration again is very different, we don't go into further details. But we plan to write a chapter on virtio for this handbook.

Conclusion

We briefly discussed the different MirageOS backends, and have the focus on the hypervisor backend.

This handbook is not complete, suggestions are welcome. The initial chapters is focused on network setups that were encountered when testing unikernels, e.g. at our annual MirageOS retreat.

Please file suggestions as an issue on GitHub, or a pull request.

Hello, networked world

In this chapter we will install everything necessary to run a unikernel, run the unikernel, and communicate with it from the host system.

Tender

To get started with a networking unikernel, you first need to get the solo5 tender. This is the executable that runs in the host operating system, allocates the resources for the unikernel, and handles the hypercalls. Commonly used is qemu, or bhyve - but these are pretty large binaries including emulation for e.g. a floppy disk drive. We have very minimal binaries to run as tender.

Debian and Ubuntu

For Debian and Ubuntu systems, we provide package repositories. Browse the apt package repository whether your distribution is periodically built, and add it to /etc/apt/sources.list. We use "ubuntu-20.04" as an example. Please open an issue if your distribution is not supported.

$ curl -fsSL https://apt.robur.coop/gpg.pub | gpg --dearmor > /usr/share/keyrings/apt.robur.coop.gpg
$ echo "deb [signed-by=/usr/share/keyrings/apt.robur.coop.gpg] https://apt.robur.coop ubuntu-20.04 main" > /etc/apt/sources.list.d/robur.list # replace ubuntu-20.04 with e.g. debian-11 on a debian buster machine
$ apt update
$ apt install solo5

FreeBSD

We also provide a package repository for FreeBSD. Please open an issue if your release is missing.

$ fetch -o /usr/local/etc/pkg/robur.pub https://pkg.robur.coop/repo.pub # download RSA public key
$ echo 'robur: {
  url: "https://pkg.robur.coop/${ABI}",
  mirror_type: "srv",
  signature_type: "pubkey",
  pubkey: "/usr/local/etc/pkg/robur.pub",
  enabled: yes
}' > /usr/local/etc/pkg/repos/robur.conf # Check https://pkg.robur.coop which ABI are available
$ pkg update
$ pkg install solo5

Other distributions

For other distributions and systems we do not (yet?) provide binary packages. You may be able to find a "solo5" packate as part of your distribution.

Source installation

You can also download the latest source release and compile it (the latest release is 0.8.1 at the time of writing):

$ curl -o solo5-v0.8.1.tar.gz -fsSL https://github.com/Solo5/solo5/releases/download/v0.8.1/solo5-v0.8.1.tar.gz
$ tar xzf solo5-v0.8.1.tar.gz
$ cd solo5-v0.8.1
$ ./configure.sh
$ make V=1
$ sudo make install

Get your Unikernel

Download the basic website unikernel binary.

$ curl -o website.hvt -fsSL https://builds.robur.coop/job/static-website/build/latest/main-binary

Run your unikernel

The unikernel requires a network interface for communication. You can think of it as a network cable that you need to plug into the unikernel. As usual, a cable has two ends -- one that we plug into the unikernel, and the other we have at the host system. On Linux/Unix systems, such virtual cables are implemented by a network device called tap. You need to create one on the host system, and configure it, to communicate with the unikernel guest system,

Linux:

$ sudo ip tuntap add tap0 mode tap
$ sudo ip tuntap set dev tap0 up

FreeBSD:

$ doas sysctl net.link.tap.up_on_open=1
$ doas ifconfig tap create #will return the device name, i.e. tap0

Executing the unikernel:

$ sudo solo5-hvt --net:service=tap0 -- website.hvt

You should see the output of the unikernel starting. To communicate to the website unikernel, you can use a web browser. But hold on, we first need to configure IP connectivity on the host system. We do that by assigning an IP address to the configured tap interface:

Linux:

$ sudo ip addr add 10.0.0.1/24 dev tap0

FreeBSD:

$ doas ifconfig tap0 10.0.0.1/24

From the command-line, you should now be able to communicate with the unikernel:

$ ping -c 2 10.0.0.2
64 bytes from 10.0.0.2: icmp_seq=0 ttl=64 time=0.052 ms
64 bytes from 10.0.0.2: icmp_seq=1 ttl=64 time=0.165 ms

And from the web browser as well, type "http://10.0.0.2" as URL.

Communication to/from external Internet

What are post-routing and pre-routing rules and why do I need them?

note: pre-routing only on external traffic (sysctl & post-routing rule) vs local

How can the unikernel communicate to the external world? An example may be the traceroute unikernel

How can the external world communicate to the unikernel?

Bridges

When multiple unikernels are deployed, a bridge interface may be useful. Then they can talk to each other

Also, in a server setup a bridge can be used with the physical interface attached to it.

Albatross

What is it? It sets up the tap device for you :) It doesn't setup firewall rules, though

Virtio

How to use virtio with MirageOS

DHCP

Describe and explain a setup with DHCP.

Open questions

• How to run hvt on windows (WSL)?
• How to run unikernels on macOS
• How to test virtio on a cloud provider without paying money?