Currently Maintained Kernel Implementations
- seL4 is a kernel developed by NICTA (now Data61) for high-assurance use.
Its defining features are:
seL4 presently supports the ARM and x86 architectures (the
formal verification applies to ARM only). It was open-sourced in July 2014.
- 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
- 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
- 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
- Despite all this unprecedented assurance, seL4 is (in terms of IPC cost)
presently the fastest L4 kernel.
- 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
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,
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
- 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.