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

Category: infrastructure

Tags: hypervisor, sel4, microkernel, virtualization, tpm-attestation

Score: 7.0/10 (Innovation: 7, Technical: 9, Documentation: 6, Utility: 6)

L4H is a Type-1 hypervisor built on the seL4 microkernel that runs Linux VMs as seL4 userspace threads without hardware virtualization extensions like VT-x/AMD-V. It provides a TPM-backed chain of trust for VM attestation, IOMMU-protected device drivers, and performance on par with Xen PV on IO-heavy workloads. Its use of seL4 for strong isolation and formal-verification potential is a notable departure from conventional hypervisor architectures.

Target audience: systems engineers, security researchers, cloud infrastructure teams, embedded developers

Repository: https://github.com/losfair/l4h · Rust · GPL-2.0 · 9 stars

View on Hacker News