L4 Based Operating Systems
L4 provides an minimal set of mechanisms to applications
running on top of it. To be able to develop applications on top
of L4 for common hardware, one needs some basic services. These
range from minimal support libraries to fully-fledged operating-system
personalities. The latter class includes complete (virtualised)
operating systems for legacy support.
Currently supported L4-based OS environments
The Genode OS Framework is a tool kit for
building highly secure special-purpose operating systems. It scales from
embedded systems with as
little as 4 MB of memory to highly dynamic general-purpose workloads.
Genode is based on a recursive system structure. Each program runs in a
dedicated sandbox and gets granted only those access rights and resources that
are needed for its specific purpose. Programs can create and manage
sub-sandboxes out of their own resources, thereby forming hierarchies where
policies can be applied at each level. The framework provides mechanisms to
let programs communicate with each other and trade their resources, but only
in strictly-defined manners. Thanks to this rigid regime, the attack surface
of security-critical functions can be reduced by orders of magnitude compared
to contemporary operating systems.
The framework aligns the construction principles of L4 with Unix philosophy.
In line with Unix philosophy, Genode is a collection of small building blocks,
out of which sophisticated systems can be composed. But unlike Unix, those
building blocks include not only applications but also all classical OS
functionalities including kernels, device drivers, file systems, and protocol
- CPU architectures: x86 (32 and 64 bit), ARM
- Kernels: most members of the L4 family
Linux, and a custom kernel
- Virtualization: VirtualBox (on NOVA), L4Linux (on Fiasco.OC), and a
custom runtime for Unix software
- Over 100 ready-to-use
Genode is open source and commercially supported by
- L4Re is the user-level infrastructure running on top of the
Fiasco.OC kernel, providing support for applications and virtualization.
- Lightweight component framework developed at NICTA,
originally for NICTA::Pistachio-embedded, later ported to seL4.
- L4Linux is a port of Linux to the L4 µ-kernel.
L4Linux runs as an L4 server in user-mode, side-by-side with other
L4 applications (e.g. real-time components). It is currently running on
x86 and ARM and it is binary compatible with the native Linux
- Qualcomm's feature phone OS was ported to OKL4 and this version shipped from about 2006.
Obsolete or unsupported OS environments
- Mungi Single-Address-Space OS
- A single address space operating system (SASOS) on top of
L4. The goal of the project is to show that a SASOS can work on
standard hardware, can be made as secure as traditional systems, is
not inherently less efficient that traditional systems, and that for
some classes of important applications it delivers performance
advantages over traditional systems.
Iguana is designed as a base for the provision of operating system
(OS) services on top of the L4 microkernel, presently the Version 4
API as implemented by L4Ka::Pistachio, and we are observing ongoing
developments of a security-enhanced L4 API; Iguana's design is meant
to be easily adapted to new APIs. It provides the underlying OS for
Wombat, our port of Linux to L4.
Iguana borrows many ideas from the Mungi operating system,
however it is designed, primarily, for use in embedded
systems. The implications of this are:
- Iguana complements, rather than hides the underlying L4
API. It provides services virtually every OS environment requires,
such as memory and protection management, and a device driver
- the memory and cache footprints of Iguana are kept small;
- low-overhead sharing of data is supported;
- Iguana attempts to provide the best possible performance on
typical embedded processors. In particular, it supports the
separation of protection and translation that is a feature of some
embedded processors, such as ARM cores, by encouraging a
non-overlapping address-space layout.
- Wombat is a port of Linux 2.6 to run on top of the Iguana L4
based operating system. It is aimed at embedded systems and designed
to be cross-platform, currently running on IA32, ARM and
MIPS64. Unlike some other Linux ports, it uses the native Linux
scheduler to determine scheduling policy of Linux applications.
- Security critical applications like electronic signatures,
online banking, or e-government do not only need secure
cryptography, but also a trustworthy platform that reliably
separates different applications from each other and that comes
with a user interface that ensures that Trojan horses cannot
intercept the user authorization (e.g., a passphrase). PERSEUS is
an open-source project that shows that this can be achieved with
much less programming effort and more flexibility than typically
- Kenge is a minimal library environment that has been developed for the L4Ka::Pistachio kernel and focuses
on platform independence.
- E1 Distributed
- E1 is a distributed operating system project based on the
concepts of object replication, component model support, and
persistence. To provide applications with transparent access to all
resources of the computer network, state and functionality of
operating syste components and application software are encapsulated
by distributed objects.