The Custom-Code Gap Map

The ratification-track CHERI spec excludes its hypervisor chapter from v1.0 — the semantics of capabilities crossing into a virtual machine are still a draft. No kernel on Earth has entered V-mode with capabilities live. There is nothing to copy; there is a chapter to interpret, and our interpretation becomes evidence the spec authors can cite.

Seam

CHERI-seL4's capability context ↔ the H-extension's guest world (V=1)

We write

• VCPU object carrying capability-width guest CSRs (vstvecc, vsepcc, vsscratchc, vstidc), saved/restored on every VM entry and exit
• henvcfg.CRE policy — whether and when the guest sees CHERI at all
• Capability-fault forwarding from V-mode out to the VMM

Nearest dep

Ivan's VCPU object stops at integer-width registers; CHERI-seL4's context switch stops at V=0. Each solves half; neither meets the other.

Scope

≈300–800 LOC kernel C · plus design notes for the working group

Risk

The hard part is deciding, not typing — each choice is spec-input, and should be socialized with the WG before it lands.

The CHERI+H machinery is in the tree but has never executed: capability VS-mode CSRs, capability-aware hypervisor register swapping, capmode hypervisor loads/stores — compiled together, default-on, and publicly untested by any OS. One deferral is documented in-source: riscv_cpu_mode_cre() ignores henvcfg.CRE in V-mode (“For now, we do not support the hypervisor extension”). We will be the first execution this code ever gets; being first is the work.

Seam

CHERI-Alliance QEMU main ↔ reality. Also note: the codasip-a730 CPU model every CHERI-seL4 doc uses has no H — we run -cpu rv64.

We write

• The henvcfg.CRE gate in V-mode, per the draft chapter
• Fixes for whatever first execution shakes loose

Nearest dep

The fork itself — it stops at “compiled, never run.”

Scope

≈100–300 LOC known · plus unknown-unknowns, priced honestly as such

Risk

Every QEMU fix here is upstreamable to the Alliance fork — small patches, outsized goodwill.

Ivan's H-extension branch and Hesham's CHERI branch are both forks of seL4 that rewrite the same trap path, the same context layout, the same object table. No repository holds their union, and git can only merge text — the semantic union (a trap entry that saves capability context and detects V-mode) has to be authored.

Seam

Ivan-Velickovic/seL4 @ microkit_riscv_he (2025-07-25) ↔ CHERI-Alliance/CHERI-seL4 @ cheri-microkit (2026-03-18)

We write

• The reconciled trap entry and unified TCB/VCPU context
• The config product KernelRiscvExtY × KernelRiscVHypervisorSupport, actually building

Nearest dep

Both halves — each stops exactly at the other's first line. A year of drift between their base revisions is part of the price.

Scope

≈300–800 LOC authored · Ivan's ~2 kLOC patchset reviewed line-by-line

Risk

Merge conflicts are the visible part; semantic conflicts in the trap path are the real part. Ivan's branch being dormant since 2025-07 makes it a stable base, not a moving target.

The kernel merge repeats at the SDK layer. Ivan's Microkit fork knows how to build hypervisor-mode protection domains; CHERI-Microkit knows how to build CHERI ones (purecap libmicrokit, a Rust tool that nulls the DDC). A virtual-machine PD on a CHERI kernel needs both forks' knowledge in one tool.

Seam

Ivan's Microkit-hyp fork ↔ CHERI-Alliance/CHERI-Microkit @ cheri (2026-05-21)

We write

• Hypervisor-mode PD support merged into CHERI-Microkit's build_sdk.py, tool, and monitor
• A qemu_virt_riscv64 board config with H on and CHERI available

Nearest dep

Each fork, stopping at the other's feature.

Scope

≈200–500 LOC Python / Rust / C across the SDK

Risk

Low-novelty, high-fiddliness. First candidate PR back to CHERI-Microkit — the WG named ports like this as wanted contributions.

libvmm's riscv branch is the strongest possible base and unfinished by its own account — its newest board port says “not currently working” in the commit log, and the QEMU-virt board is publicly unproven. Separately: a RISC-V Linux guest's first act is to call its firmware (timer, IPI, console). Under the H-extension those calls trap to us — the VMM must answer with an SBI implementation, the dial-tone the guest expects before it says anything.

Seam

au-ts/libvmm @ riscv (2026-04-22) ↔ a Linux guest that actually reaches userspace

We write

• Whatever the first boot reveals — the honest definition of a delta gap
• The SBI answer set: TIME (against the kernel's virtual timers — Ivan's branch has KernelRiscVNumVTimers), IPI, RFENCE, early console

Nearest dep

The branch itself, plus libvmm main (pushed 2026-07-08) for the device framework it will eventually rebase onto.

Scope

≈200–600 LOC — unknowable until first boot; bounded by the branch's own churn

Risk

The size of this gap is the single biggest unknown in the plan. First boot attempt should happen early precisely to price it.

The window itself is dependency-covered: QEMU emulates virtio-gpu, renders the guest's screen in its own macOS window, and LionsOS's “Kitty” example proves the passthrough pattern in-tree — on aarch64. The existing code is arm-shaped: GIC interrupt injection, arm device trees. The pattern ports; the plumbing is ours.

Seam

The proven aarch64 pattern ↔ RISC-V's interrupt world (PLIC line → hvip VS-level injection) and guest device tree

We write

• Map QEMU's virtio-gpu MMIO window into guest physical space, 1:1 so device DMA just works
• Route its interrupt into the guest as a VS-level external interrupt
• Guest DTB nodes; same again for virtio-input, so the window can type back

Nearest dep

LionsOS Kitty (the pattern) + guest kernel's CONFIG_DRM_VIRTIO_GPU (the driver). Both stop at the ISA boundary.

Scope

≈200–400 LOC + device tree fragments

Risk

Low: output-only first, input second. The demo's money shot, deliberately scheduled last.

NixOS on riscv64 is real; NixOS under a non-KVM microkernel VMM has never happened. The template is microvm.nix — NixOS taught to boot under five exotic VMMs — but it has no seL4 backend. What a libvmm guest is handed (a virtio-mmio world, an SBI console, a VMM-authored device tree) becomes a NixOS hardware profile.

Seam

nixpkgs riscv64 ↔ the world libvmm actually provides a guest

We write

• A NixOS module: kernel config (virtio_mmio in initrd, DRM_VIRTIO_GPU), SBI console, no-bootloader direct-kernel boot
• Image packaging the VMM loads: kernel + initrd + rootfs closure
• The aarch64-darwin build route (nix-darwin linux-builder — dependency-covered, config only)

Nearest dep

microvm.nix, stopping one VMM short of ours.

Scope

≈150–300 lines of Nix

Risk

Low — and it carries a title: the first NixOS ever to boot on seL4.

The CHERI world builds with cheribuild — Python, non-hermetic, living in ~/cheri. Nothing packages the Alliance toolchain for Nix. The seL4 side already went there (official Microkit flake, Foundation CI inside nix develop), so a reproducible spine reads as native to half our audience and novel to the other half — the ideal shape for a first contribution.

Seam

cheribuild's world ↔ a flake the working group can run with one command

We write

• Derivations: CHERI-Alliance LLVM (codasip-cheri-riscv), QEMU main (riscv64cheri target), CHERI-Microkit SDK
• Boot harness + devshell — the one command that reproduces the whole wall

Nearest dep

lowrisc-nix proves the LLVM derivation shape, then stops before QEMU, the SDK, and the harness.

Scope

≈300–600 lines of Nix

Risk

Mechanical, front-loaded, and the foundation every other gap builds on — which is why it is M0.