Home of the L4 community
         Home )   About L4hq )  
 L4 Kernel Projects

Currently Maintained Kernel Implementations

seL4 is a kernel developed by NICTA (now Data61) for high-assurance use. Its defining features are:
  • A new resource-management model that enhances isolation and supports reasoning about it. Using capabilities and making all memory management a user-level responsibility, memory management is fully delegatable with low overheads, and automatically extends to kernel memory.
  • It is the world's first (and, as of early 2014 still only) general-purpose OS kernel which is fully formally verified: it has a machine-checked proof that the C code implements the specification correctly (i.e., is functionally correct).
  • It has a proof that the executable binary code is a correct translation of the C implementation. This means that the compiler and linker do not need to be trusted to produce correct code.
  • It has formal proofs that the kernel mechanisms can be used to enforce integrity and confidentiality of user-level components. Together with the functional-correctness and translation-correctness proofs, these proofs hold for the kernel binary. Together these make seL4 the world's first (and still only) OS kernel that is provably secure in a very strong sense.
  • It has a complete analysis of timing, in particular, worst-case interrupt latencies. This make it the world's first (and still only) protected-mode operating-system kernel with a sound and complete worst-case timing analysis, and thus the only protected-mode OS that can actually provide hard real-time guarantees.
  • Despite all this unprecedented assurance, seL4 is (in terms of IPC cost) presently the fastest L4 kernel.
seL4 presently supports the ARM and x86 architectures (the formal verification applies to ARM only). It was open-sourced in July 2014.
Codezero started a commercial clone of the OKL4 microkernel, done by B Labs and supporting ARMv7 processors. Originally open-source, source is now available to commercial licensees only.
NOVA is a micro-hypervisor based on L4 principles and designed for VT-x enabled x86 platforms. It was created at TU Dresden by Udo Steinberg and Bernhard Kauer. NOVA is open-source and commercially supported by Genode Labs.
OKL4 is a descendant and successor of NICTA::Pistachio-embedded and is developed and commercially supported by Open Kernel Labs (OK). It comes in two versions: the OKL4 Microvisor is a micro-hypervisor which provides virtual machines as first-class citizens and is aimed at providing low-overhead virtualisation support for embedded devices. It is the successor of the OKL4 microkernel, which developed out of NICTA::Pistachio-embedded and is still shipping on mobile devices. To date, the OKL4 microkernel has shipped on several billion mobile devices, making it the most widely-deployed L4 kernel. The OKL4 microkernel was also the first L4 kernel with a capability-based access control model.
OKL4 supports the ARM v5–v7 architectures (some versions supported MIPS and x86). It was originally open-source but is now closed. The latest release (3.0) is still available from archive.org.
Fiasco.OC is a portable µ-kernel implementation and the kernel used by L4Re. It is a 3rd-generation microkernel, using capabilities as the sole access control mechanism. Being designed as a preemptible kernel it can run real-time applications and with its comprehensive virtualization features allows to host a wide variety of legacy systems. Fiasco.OC is open-source and commercially supported by Kernkonzept.
PikeOS, originally called P4, was an early commercial clone of the V2 API, created by Robert Kaiser from Sysgo AG in the late '90s. It is certified to avionics and other standards and deployed in aircraft and trains. It supports the PowerPC, x86, MIPS, ARM, SPARCv8, V850 and SH-4 architectures. PikeOS is closed-source.

L4 Kernel Family Tree

family tree

Black arrows indicate code, green arrows ABI inheritance. Source: [Elphinstone & Heiser, SOSP 2013]

Obsolete or Unmaintained Kernel Implementations

L4Ka::Pistachio is the latest L4 microkernel developed by the System Architecture Group at the University of Karlsruhe in collaboration with the DiSy group at the University of New South Wales, Australia (the ERTOS program at NICTA). It is the first available kernel implementation of the L4 Version 4 kernel API (currently code-named Version X.2), which is fully 32- and 64-bit clean, provides multiprocessor support, and super-fast local IPC. The kernel is no longer actively maintained.
NICTA::Pistachio-embedded is a descendant of L4Ka::Pistachio, optimised for use in embedded systems. It was developed by the NICTA ERTOS group. Modifications are aimed at reducing kernel complexity and memory footprint. It is superseded by OKL4 and no longer maintained.
L4Ka::Hazelnut was designed to be portable across 32bit platforms. We separated general code like IPC, thread management, and scheduling from platform dependent code like pagetable management and exception handling. L4Ka::Hazelnut is (almost) completely written in C++. With the release of L4Ka::Pistachio development on the kernel is discontinued.
The DiSy group at UNSW developed an Alpha L4 implementation based on the Version-2 API. The kernel was based on initial work done at Dresden. With the release of L4Ka::Pistachio development on the kernel is discontinued. The NICTA group maintains the Alpha architecture of the L4Ka::Pistachio kernel.
The DiSy group at UNSW developed a 64bit MIPS L4 implementations based on the Version 2 API. The MIPS kernel was used heavily for teaching and research. With the release of L4Ka::Pistachio development on the kernel is discontinued. The NICTA group maintains the MIPS architecture of the L4Ka::Pistachio kernel.