What is a Separation Kernel?

A separation kernel (SK) is a minimal microkernel that enforces strict isolation between independently running components, or subjects, according to a defined security policy. Unlike traditional operating systems, an SK provides no generic services; instead, all functionality is supplied by separate, formally verified subjects. This architecture eliminates the attack surface that plagues monolithic kernels and makes it possible to reason formally about the entire system.

Muen’s Design Goals

Muen was conceived in Switzerland by codelabs GmbH in partnership with Germany’s secunet Security Networks AG. Its primary objectives are:

  • Formal correctness – The entire kernel is written in SPARK 2014 and has been proven to contain no runtime errors at the source level.
  • Hardware‑assisted isolation – It leverages Intel VT‑x for VMX root/non‑root separation and VT‑d for secure PCI passthrough.
  • Minimalism – With a footprint of only a few kilobytes, Muen keeps the attack surface razor‑thin, enabling exhaustive proof and static analysis.
  • Flexibility – A static System Composer called Tau0 composes system images while preserving isolation invariants, allowing gradual increases in configurability.

Key Features

  • Formal verification – SPARK 2014 source code with proof of absence of runtime errors.
  • Multicore support – Parallel execution across CPUs while maintaining isolation.
  • Fixed‑cycle scheduling – Uses the VMX preemption timer for deterministic timing.
  • PCI passthrough – VT‑d DMA and interrupt remapping enable secure device assignment.
  • Zero‑footprint runtime – The kernel itself occupies only a few kilobytes.
  • Event and shared‑memory channels – Lightweight inter‑subject communication.
  • Crash audit – Built‑in logging for post‑mortem analysis.
  • Native support for Ada/SPARK, Linux VMs, MirageOS unikernels, and more.

Toolchain and Development

Muen ships with a comprehensive toolchain:

# Install the Bob build tool
pipx install bob
# Clone the recipes
git clone https://git.codelabs.ch/muen/muen.git
# Build a demo system for QEMU
bob dev x86

The project also provides reusable subjects such as an AHCI driver, a device manager, and a virtual terminal, all written in SPARK or Ada. Linux kernel modules like muenblock, muenevents, muenfs, and muennet expose block I/O, events, a virtual filesystem, and networking over shared memory channels.

Use Cases

Because of its formal guarantees and tight hardware isolation, Muen is ideal for:

  • National‑security platforms – Secure execution of classified workloads on commodity Intel hardware.
  • Embedded safety systems – Reliable isolation for avionics, automotive, and industrial control.
  • Research and education – A sandbox for studying formal verification, OS design, and secure virtualization.

Community and Resources

Muen’s mailing list ([email protected]) and Git repositories are open to contributors. Detailed specifications, a master thesis, and conference presentations are available at the project website.

“Muen demonstrates that formal verification can be applied to a real‑world, high‑performance kernel without sacrificing practicality.” – Source: https://muen.codelabs.ch/

Conclusion

Muen represents a significant step toward trustworthy computing on mainstream hardware. By combining formal proofs, hardware‑assisted isolation, and a minimal, modular design, it offers developers a secure, verifiable foundation for the next generation of high‑assurance systems.

Source: https://muen.codelabs.ch/