L4hq.org
Home of the L4 community
         Home )   About L4hq )  
 L4 Based Operating Systems
 

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

Genode

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 stacks.

Features:
  • CPU architectures: x86 (32 and 64 bit), ARM
  • Kernels: most members of the L4 family (NOVA, Fiasco.OC, OKL4 v2.1, L4Ka::Pistachio, Codezero, L4/Fiasco), 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 components

Genode is open source and commercially supported by Genode Labs.

L4Re
L4Re is the user-level infrastructure running on top of the Fiasco.OC kernel, providing support for applications and virtualization.
CAmkES
Lightweight component framework developed at NICTA, originally for NICTA::Pistachio-embedded, later ported to seL4.
L4Linux
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 kernels.
BREW
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

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 framework;
  • 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
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.
Perseus
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 thought.
Kenge
Kenge is a minimal library environment that has been developed for the L4Ka::Pistachio kernel and focuses on platform independence.
E1 Distributed Operating System
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.