ocaml-solo5#

Build, inspect, and run Solo5 hvt unikernels in (almost) pure OCaml.

This repository provides the OCaml side of the Solo5 hvt world: the ABI and on-disk note formats as wire codecs, a backend-independent tender core, a C-toolchain-free CLI for unikernel manifests and inspection, and two tenders that boot the same aarch64 hvt unikernels natively -- on macOS / Apple silicon via Hypervisor.framework (solo5-hvf, a backend upstream Solo5 does not have) and on Linux via KVM (solo5-kvm, an OCaml counterpart to upstream's C tender). Everything above the hypervisor and guest-memory boundary (ELF loading, manifest and ABI decoding, aarch64 page tables, the hypercall dispatch loop) is OCaml and shared by both backends; the only per-backend C is the few hundred lines that touch the host hypervisor.

Installation#

Install with opam:

$ opam install solo5-tool

If opam cannot find the package, it may not yet be released in the public opam-repository. Add the overlay repository, then install it:

$ opam repo add samoht https://tangled.org/gazagnaire.org/opam-overlay.git
$ opam update
$ opam install solo5-tool

Packages#

Build#

The libraries and the solo5 CLI are plain OCaml and build anywhere:

dune build solo5-abi solo5-tender solo5-tool

The solo5-hvf tender needs the com.apple.security.hypervisor entitlement before it can call hv_vm_create. The build ad-hoc codesigns it for you, so it is runnable as soon as it is built or installed:

dune build solo5-hvf       # macOS / Apple silicon

dune exec solo5-hvf runs the entitled tender, and dune install solo5-hvf puts it on PATH as solo5-hvf; the solo5 CLI is _build/default/ocaml-solo5/bin/solo5.exe.

On Linux (aarch64) the solo5-kvm tender boots the same unikernels through /dev/kvm, with no entitlement or codesigning:

dune build solo5-kvm       # Linux / aarch64

Usage#

Build a unikernel#

solo5 up installs the freestanding cross toolchain for your host. Then cross-build a unikernel target through the solo5 Dune cross context:

solo5 up
dune build -x solo5 path/to/unikernel.hvt

The cross-built unikernel lands under _build/default.solo5/. A plain dune build is unaffected -- it stays host-only -- so cross-compilation is opt-in to -x solo5.

Inspect a built unikernel#

The solo5 CLI reads the ABI and manifest notes straight out of an ELF, with no C toolchain and without running the guest:

solo5 query path/to/unikernel.hvt   # the Solo5 ABI note and the device manifest
solo5 size  path/to/unikernel.hvt   # ELF section sizes

solo5 manifest manifest.json out.c generates the MFT1 manifest C source the Solo5 loader reads; solo5 startup emits the OCaml/Solo5 C entry point. The per-unikernel dune rules that call them come from mirage dune.

Run it on macOS#

_build/default/ocaml-solo5/bin/main.exe --mem=64 path/to/unikernel.hvt

Useful flags:

• --mem=MB -- guest memory in MiB (rounded down to the guest block size).
• --watchdog=SECS -- power off a runaway guest: terminate it (exit 2) when the vCPU stays inside the guest for SECS seconds without a single VM exit (a spin or fault loop at EL1). Only in-guest time counts -- a guest blocked in a long POLL is host-side and never killed. 0 (default) disables it.
• --net=BACKEND -- none (default), loopback (written frames come back on read; for testing), or slirp (an unprivileged user-mode gateway giving the guest ARP, a DHCP-leased address, and host-socket-terminated TCP/UDP/ICMP with no root and no host routing change).
• -p HOST:GUEST -- with --net=slirp, publish a host port into the guest (Docker's -p): the gateway listens on HOST and proxies each connection to the guest at 10.0.0.2:GUEST. Repeatable.
• --disk=IMAGE -- attach a raw image file as a guest block device, bound in order to the manifest's block entries. Repeatable.

# Boot a networked unikernel and forward host port 8080 to its port 80.
_build/default/ocaml-solo5/bin/main.exe \
  --mem=64 --net=slirp -p 8080:80 path/to/unikernel.hvt

Run it on Linux#

solo5-kvm takes the same flags; it just needs read/write access to /dev/kvm (no entitlement, no codesigning):

_build/default/ocaml-solo5/bin/main_kvm.exe --mem=64 path/to/unikernel.hvt

On an Apple-silicon host, /dev/kvm is reachable inside a Virtualization.framework guest (nested virtualisation), so a Linux VM there runs solo5-kvm natively while solo5-hvf runs on the host.

How the tender works#

A guest dispatches a hypercall with a 32-bit store to an unmapped MMIO address (Abi.mmio_base + nr*8). That store faults out to the tender as an MMIO access, which the backend normalises to a faulting address and the stored value (solo5-hvf decodes the exception syndrome and source register; solo5-kvm reads the access KVM already decoded). The shared core decodes the hypercall number and argument-struct address, services the call (walltime, puts, poll, halt, and the net/block hypercalls when a device is attached), and resumes the vCPU. The run loop lives in lib/tender/tender.ml, a functor over the Machine backend boundary; the ABI it decodes against is lib/abi/abi.ml, a wire-codec mirror of Solo5's include/hvt_abi.h. The same structs are exported as EverParse 3D specs -- the cleanest declarative view of the ABI layout, one .3d file per struct (e.g. Hvt_boot_info.3d) -- from which F*-verified C validators are generated.

The loaded image's text and data segments get write-xor-execute page protection: code is mapped read-only-executable, data writable-no-execute, by lib/tender/page_table.ml (a port of Solo5's aarch64_setup_memory_mapping). Guest physical memory is a Bigarray the OCaml side reads and writes through lib/tender/guest.ml, with bounds checks on every guest-supplied offset and length.

Testing#

• dune test runs the unit suites. The bulk are the backend-independent solo5-tender tests -- the ABI codec layout, the Page_table port checked against independently-derived ARM descriptor values, the Loader against synthetic ELFs (and its rejection of malformed ones), the net loopback and slirp round-trips, and the block and virtio-net device models -- so they run everywhere (macOS and Linux). The solo5-hvf suite adds the few cases that drive a live Hypervisor.framework vCPU and skip cleanly when it is unavailable.
• test/boot/run.sh PATH/TO/solo5-hvf is an end-to-end boot harness. It assembles small aarch64 guests with clang + lld, codesigns the tender, and boots each, asserting the exit code (and output where relevant): a plain halt, a puts "hello", a hostile out-of-range hypercall pointer, a bad hypercall number, a runaway guest (powered off by --watchdog, asserting the watchdog's own diagnostic), a guest blocked in a POLL longer than the watchdog budget (which must survive -- only in-guest time counts), and both halves of W^X (a store to read-only .text and a branch into no-execute .data). When the Solo5 cross toolchain is on PATH it also cross-builds a real Solo5-bindings unikernel and boots it, and exercises --net=slirp end to end with a unikernel that ARPs the gateway and reads back the reply.
• test/boot/run_kvm.sh PATH/TO/solo5-kvm is the same harness on the KVM backend, booting byte-identical guests; it gates on Linux / aarch64 with /dev/kvm and SKIPs cleanly otherwise (like the macOS harness off macOS). Each self-gates, so dune build @boot / @boot_kvm is safe to run on either platform.
• test/boot/run_kvm_vz.sh runs that KVM harness on a macOS host with no /dev/kvm: it builds the tender and guests into an initramfs in a Linux/arm64 container, then boots a linuxkit kernel + initramfs in a VM via kvm-vz (the ocaml-vz launcher that turns on nested virtualisation), where the guest kernel is itself a KVM host. So the same guests run on real KVM even on Apple silicon. Needs Docker and an M3-or-later host; SKIPs cleanly otherwise.

Benchmarking#

The no-hypervisor benchmark harness exercises the production tender paths where OCaml allocation and payload copying matter: hypercall MMIO service, net/block handlers, payload-size scaling, virtio-mmio device discovery/config registers, and virtio-net ring batching.

dune exec ocaml-solo5/bench/bench.exe --
dune exec ocaml-solo5/bench/bench.exe -- --format csv > /tmp/solo5-bench.csv
dune exec ocaml-solo5/bench/bench.exe -- --probe /tmp/solo5-bench.json --format csv > /tmp/solo5-bench.csv
dune exec -- catapult summary /tmp/solo5-bench.json

Useful flags:

• --iterations=N sets the starting iterations per row before calibration.
• --target-bytes=N bounds total payload bytes per payload-scaling row so large block sizes do not dominate the run.
• --target-time-ms=N asks each row to calibrate upward until the measured loop runs for at least that many milliseconds; use 0 to disable timing calibration.
• --format text|csv chooses human-readable output or stable CSV for tracking regressions.
• --probe=FILE captures the same single suite as a Catapult/Perfetto trace.

The key columns are B/op / allocated_bytes_per_op, minor/op, and Mops/s. Hypercall net/block cases should keep allocation roughly flat as payload size grows because the handlers move payloads directly between guest RAM and their backend; virtio cases should also stay flat per frame because the device model drains whole rings through a reused scratch buffer. Each row runs one unmeasured warmup and any time-budget calibration before counters start, so first-use scratch-buffer growth and calibration work are not amortized into the reported allocation. With --probe, rows use a bounded iteration count instead of time-budget calibration so the trace captures production solo5.hypercall and virtio spans without overrunning the probe ring. Probe captures contain solo5.bench.run, section spans for fixed rows, payload scaling and virtio batching, per-row spans, and solo5.bench.result events with numeric allocation and throughput fields.

For live VM-exit and probe/memtrace captures on Apple silicon, use bench/capture.sh with a built solo5-hvf tender; it boots a synthetic guest that issues many WALLTIME hypercalls and prints the probe summary plus memtrace hotspots.

Security#

The tender runs attacker-controlled guest ELFs and hypercall data, so the host boundary is hardened: every guest-supplied offset and length is bounds-checked (Guest.region and the Guest accessors), ELF segments are validated by the loader, puts/net lengths are capped, and a hostile or broken guest is terminated cleanly with a diagnostic and a distinct exit code (2) -- never an uncaught backtrace or host-memory corruption.

Before entering the guest, the tender narrows itself to a deny-default sandbox -- a seccomp allowlist on Linux (solo5-kvm, the same syscall set as upstream Solo5's hvt_seccomp_linux.c) and a deny-default Seatbelt profile on macOS (solo5-hvf) -- so a guest that compromised the tender cannot spawn a process, create a file, or (without --net=slirp) open a socket.

It is a single-tenant trust model, not a multi-tenant sandbox: --disk takes an arbitrary host path opened read-write, and --net=slirp gives the guest unrestricted host egress (and the sandbox then allows the network, since the user-mode gateway needs host sockets). Running untrusted tenants would need disk paths restricted to tenant-owned images and an egress allowlist.

Status#

Working and robustly tested against guest behaviour on Apple silicon (solo5-hvf): it boots real aarch64 hvt unikernels (puts, walltime, poll, halt), enforces W^X, attaches block devices and unprivileged slirp networking, rejects hostile guests cleanly, confines itself to a deny-default sandbox, powers off a runaway guest with --watchdog, and stops on SIGINT/SIGTERM (the operator's manual path, as upstream Solo5). solo5-kvm drives the same core through /dev/kvm and passes the equivalent boot harness wherever KVM is reachable (a Linux/aarch64 host, or a Virtualization.framework guest on Apple silicon).

Not yet implemented:

• A vmnet networking backend for bridged layer-2 networking. The slirp backend covers the no-root case; vmnet would need root or the restricted com.apple.vm.networking entitlement (which cannot be ad-hoc codesigned), so it must be built where those are available.
• Multi-tenant authority and resource policy (see Security).
• Tickless idle via the virtual timer.

Related work#

• Solo5 -- the C hvt tender on Linux/KVM, FreeBSD/vmm and others. solo5-kvm here is an OCaml counterpart to its KVM backend; solo5-hvf adds a Hypervisor.framework backend it has no equivalent for (no upstream macOS backend exists).
• ocaml-solo5 -- the freestanding OCaml cross-compiler that builds the unikernels this runs.

The Solo5 reference headers this mirrors are vendored verbatim under reference/ (see reference/PROVENANCE); lib/abi hand-mirrors them as wire codecs and is diffed against them on each upstream bump.

License#

ISC. See LICENSE.md. Vendored Solo5 ABI definitions are ISC (Solo5 contributors).