I wanted to run OCaml on seL4. Not “install OCaml” — actually get it running inside a virtual machine hosted by seL4, the formally verified microkernel that’s supposed to be one of the most secure pieces of software ever written. The idea was simple on paper: seL4 as a hypervisor, a normal Linux guest running on top of it, OCaml living in that guest like it would anywhere else.
The idea was simple. The execution was not.
The plan
seL4 doesn’t run applications directly — it’s a microkernel with no filesystem, no process model, nothing you’d recognize as an OS. To get a normal Linux environment on top of it, you use the CAmkES VM project, which implements a Virtual Machine Monitor (VMM) as a set of seL4 components. The VMM boots a real Linux kernel as a guest, with seL4 underneath enforcing isolation.
Step one: get the stock camkes-vm-examples project building and booting something — anything — before touching OCaml at all.
Where it went sideways
I cloned the project with repo, and the first build attempt picked the wrong architecture entirely — it defaulted to ARM and demanded a platform like tk1 or qemu-arm-virt. Fine, forced it to x86 with the right app name (minimal, not vm_minimal — the naming isn’t consistent between ARM and x86 examples).
Then came the dependency chain. CMake’s config generator is Python, and it wanted PyYAML. Then plyplus. Then aenum. Then pyfdt. Each one surfaced one at a time, a fresh crash after every fix, because I was chasing them individually instead of just installing the project’s actual metapackage (sel4-deps) up front, which would’ve saved probably forty minutes of whack-a-mole.
Once Python stopped complaining, the build hit a completely different toolchain: Haskell. The CapDL tool — which translates the CAmkES component spec into something the kernel can load — is written in Haskell and built with stack. I hadn’t touched Haskell tooling in this environment at all, so that meant installing stack from scratch, which then pulled down its own GHC compiler toolchain before it could compile a single line.
Then the C toolchain itself turned on me. My system had just upgraded gcc as a side effect of installing 32-bit multilib support, and the build started referencing stale paths to the old gcc version’s crtbegin.o/crtend.o — 64-bit-only files being linked into a 32-bit target. A clean CMake reconfigure fixed that once I realized the compiler had moved out from under the build mid-session.
The Meltdown wall
Here’s the one that actually stopped me cold. I finally got a full, clean build — 416 out of 416 targets — and booted it in QEMU. seL4 came up, parsed ACPI, detected the CPU… and then halted:
CPU reports vulnerable to Rogue Data Cache Load (aka Meltdown) yet SKIM window is not enabled. Please re-build with SKIM window enabled.
seL4 refuses to boot on a Meltdown-vulnerable CPU unless it was built with a specific mitigation (a “SKIM window,” their term for a reduced kernel memory exposure window). My desktop’s CPU predates the Meltdown-immune generation, so this wasn’t optional.
The catch: that mitigation option is only available when building the 64-bit kernel. I’d been building the 32-bit target the whole time (minimal), and 32-bit seL4 on x86 doesn’t even expose the SKIM window as a config option — it’s hard-tied to KernelSel4ArchX86_64. The fix wasn’t a flag, it was a completely different app target: minimal_64 instead of minimal. Once I rebuilt against that, the kernel booted straight past the Meltdown check with the mitigation on by default.
The most anticlimactic bug of the whole project
With the kernel finally booting the guest, I hit a Buildroot login prompt. Tried a blank password — the standard, documented default for this image. “Login incorrect.” Tried again, more carefully, waited for the prompt to settle. “Login incorrect.” I even edited the guest kernel’s boot command line to skip login entirely with init=/bin/sh — no effect at all, which told me this particular prebuilt kernel has its command line baked in at compile time and ignores anything CAmkES passes it.
The actual fix was almost insulting in its simplicity: the password was root. Not blank. Just root. Typed it, hit enter, dropped straight into a live shell.
What I actually have now
A genuine, working seL4 microkernel hosting a CAmkES-managed virtual machine, running a real Linux 4.8.16 guest, verified under real hardware virtualization (VT-x/KVM) with Meltdown mitigations satisfied. uname -a confirms it. I have a root shell inside a Linux system that a formally verified microkernel is directly responsible for isolating.
It’s not OCaml yet. This particular guest image is deliberately minimal — no network interface beyond loopback, no package manager, no compiler. Getting OCaml running means either wiring in virtio networking and baking opam into the Buildroot image at build time,or swapping this rootfs for something like a small Debian image with real package management. That’s the next project.
But the hard part — the actual hypervisor stack, built from source, booting cleanly under KVM on real hardware — is done and verified working.