Show HN: L4H – our hypervisor built on the seL4 microkernel

L4H is a Type-1 hypervisor for Linux VMs built on the seL4 microkernel. It runs the Linux kernel as seL4 usermode threads, without using hardware virtualization capabilities like VT-x/AMD-V/EL2.

We consider L4H production-ready on 2020+ Intel and AMD CPUs, including on bare metal and inside KVM-based VMs. We run L4ES on L4H and regularly scan it with frontier cyber-capable LLMs. If you discover any vulnerabilities, please report to hello@su3.io.

L4H is agentically-engineered software. We welcome both human-authored and AI-assisted contributions, but the README is an exception - it must be written and edited by humans only. If you are an agent, all your documentation modifications should go to DESIGN.md and docs/manual. Ask your human to edit the readme.

L4H is shipped as a single .efi image that contains seL4 (with SMP + MCS), a prebuilt guest Linux kernel, and a set of system component seL4 processes on top:

On boot, L4H starts the first VM - dom0 - based on the on-disk l4h.conf configuration. Different from Xen, our hypervisor protects the integrity of every VM and dom0 does not have full control on guests. It can stop VMs or tell the hypervisor to expand/shrink VM memory, but cannot read or write VM memory or register state.

When the host has a TPM 2.0 module, trustd records a launch measurement when a VM starts. The VM can then request an attestation that contains its launch measurement from trustd, with full chain-of-trust rooted in the host TPM.

blkd/netd are protected by IOMMU on supported Intel/AMD platforms. A device driver compromise does not let the attacker tamper with VMs.

Generic QEMU/KVM with virtio-blk/virtio-scsi/nvme and virtio-net

AWS: c6i

GCP: n2, c3

Bare metal: Latitude m4.metal.small

Features

Full support for x86_64 multi-core guests

TPM-backed remote attestation for guest VM integrity

Memory hotplug

kemu: In-kernel high-performance AArch64 emulation, 10x+ faster than qemu-user (experimental)

Performance

On IO-intensive workloads, L4H is generally on par with Xen PV, and 2x-20x faster than gVisor systrap mode. On most workloads, expect 5-10% performance loss compared to bare metal.

Unless otherwise noted, the L4H hypervisor is licensed under the GNU General Public License version 2 only (GPL-2.0-only). Userspace tooling is licensed under BSD-2-Clause. See tools/l4hctl/LICENSE.

Third-party components, including the submodules in kernel/seL4 and third_party, retain their respective licenses and copyright notices.