Post by Tarides

MirageOS unikernels (https://mirage.io/) now run on seL4 (https://sel4.systems/)! 🚀 Used in safety-critical and high-assurance environments like defence and aerospace, seL4 is a natural fit as a hardware management system for MirageOS. ⚒️ seL4 is a formally verified microkernel that provides a capability system, virtual memory management, IPC, hypervisor support, and scheduling. Launched as part of Kacper Michalik’s internship project, we achieved support by taking a virtualisation approach. MirageOS unikernels run inside virtual machines managed by Microkit (https://lnkd.in/d5SxMYWh), which runs as seL4’s root task. seL4 manages the CPU scheduling and memory protection at the hypervisor level. This way, we preserved the entire MirageOS build system and bindings. Because MirageOS already had Solo5 bindings, we were able to reuse the existing virtualisation API rather than build them from scratch, which significantly reduced the implementation effort. Currently, the project supports aarch64 with a Solo5 ABI. Future improvements could include a custom ABI or VirtIO-based MirageOS bindings, expanding the driver ecosystem, and broadening platform support. The mirage-sel4-templates repo (https://lnkd.in/euVR6Qqd) with working examples has a minimal template that can have you running a MirageOS unikernel on seL4 in QEMU within minutes. Happy hacking! 🐫 Have you worked with seL4 or unikernels before? Drop a comment below! #OCaml #MirageOS #seL4 #unikernels #opensource