nix-sel4: build Microkit systems from Nix, with a clone-and-boot example

New to seL4
1

I got tired of the setup dance every time I wanted to try something on Microkit, so I packaged it. One command gets you a booting seL4 system:

nix run github:conao3/nix-sel4

LDR|INFO: loader for seL4 starting
...
Booting all finished, dropped to user space
MON|INFO: Microkit Monitor started!
hello, world from nix-sel4

No SDK tarball to download, no aarch64-none-elf toolchain to install, no MICROKIT_SDK to point anywhere, no seL4 hardware. QEMU emulates the target, so any x86_64-linux or aarch64-linux box with Nix works.

There’s a separate repo you can clone as a starting point for your own system: GitHub - conao3/nix-sel4-example: A clone-and-boot seL4 Microkit system built with nix-sel4 · GitHub

What it gives you

Three functions, on top of the SDK:

  • buildProtectionDomain cross-compiles a PD against the SDK for a given board and config. It picks the toolchain from the board’s architecture, so you don’t repeat the libmicrokit.a and linker script paths.
  • buildSystem runs the microkit tool and returns the image, the report, and a QEMU runner for the boards that can boot under QEMU.
  • mkSystemDescription renders the system description from a Nix attribute set instead of XML.

That last one is the part I actually wanted. Writing the description in Nix means some mistakes fail at evaluation instead of at boot:

  • channel and IRQ identifiers get allocated per PD out of the same identifier space, and refuse to go past 62
  • a map naming a memory region that doesn’t exist is rejected
  • two mappings that overlap inside one PD are rejected, with both regions named
  • a program_image with no matching ELF, or an ELF nothing refers to, is rejected

Hand-written .system files still work, so you can adopt it gradually.

What’s tested

nix flake check boots the examples under QEMU and greps the console. Hello world runs on all 3 QEMU boards (qemu_virt_aarch64, qemu_virt_aarch64_el1, qemu_virt_riscv64). A second example puts 2 PDs on a shared page plus a channel, with the channel id and the mapping address patched in through setvar_id and setvar_vaddr, so nothing is hardcoded on the C side.

All 28 boards in the SDK are in the board table with their architecture and available configs. The other 25 build an image you flash yourself.

The development shell

nix develop github:conao3/nix-sel4 exports MICROKIT_SDK and puts microkit, the cross toolchains, make and QEMU on PATH. The examples shipped inside the SDK build there with their own Makefiles, unmodified. If you just want the tutorial to work and don’t care about the Nix library, that’s probably the useful part.

Relation to seL4-nix-utils

@wucke13 and the DLR-FT folks already cover a lot of ground with https://github.com/DLR-FT/seL4-nix-utils: the kernel, sel4test on simulated and physical targets, CAmkES, U-Boot, and a Microkit SDK built from source with a microkit dev shell. If you want the SDK compiled rather than downloaded, or you’re working outside Microkit, go there first.

Mine is narrower and starts where that shell ends. I take the official pre-built SDK tarball, which keeps the closure small and the build fast, and spend the effort on the layer above it. Both buildSystem and buildProtectionDomain take an sdk argument, so their from-source derivation can be dropped in.

Also in nixpkgs

There was no seL4 or Microkit package in nixpkgs at all, so I sent one: microkit: init at 2.3.0 by conao3 · Pull Request #559590 · NixOS/nixpkgs · GitHub

It installs the official pre-built SDK release, which is a tradeoff worth naming: you trust the published binaries, and in exchange a cold build takes about a minute instead of pulling a pinned kernel checkout, a rustc with rust-src and TeX Live. If you’d rather see the from-source derivation land in nixpkgs instead, say so on the PR and I’ll switch it.

Repo: GitHub - conao3/nix-sel4: Build seL4 Microkit systems from Nix: SDK, cross-compiled protection domains, generated system descriptions and a QEMU runner · GitHub
Example: GitHub - conao3/nix-sel4-example: A clone-and-boot seL4 Microkit system built with nix-sel4 · GitHub
nixpkgs PR: microkit: init at 2.3.0 by conao3 · Pull Request #559590 · NixOS/nixpkgs · GitHub

Assisted-by: Claude Code:claude-opus-5

2

There’s nix: wrap the microkit SDK as a Nix package by r4v3n6101 · Pull Request #615 · seL4/microkit · GitHub, maybe you could add your thoughts there and contribute to the existing discussion. That said, what you want is quite different than just a Nix Microkit package.

My impression is that a bunch of Nix enthusiasts want Nix packages/flakes/whatever for everything, which is absolutely fine. But I don’t see how it’s different than any other distro packaging, other than more flexibility in the package system.