L4Re Technology

arch-gen.svg

The L4Re System is based on a microkernel / microhypervisor powering systems that need to consolidate multiple applications with differing security, safety, or real-time requirements, and where a minimal trusted computing base is required.

The L4Re system comprises an L4 microkernel that can run trusted native applications and act as a trusted hypervisor for legacy operating systems; the L4Re Runtime Environment, a programming and execution environment for native applications; and L4Linux, a paravirtualized Linux kernel used to run untrusted applications or device drivers.

L4Re is a mature technology previously developed at TU Dresden and is available as open-source software.

The diagram above depicts an architecture overview of an L4Re system. The only component running in the most privileged mode of the CPU is the L4Re Microkernel. All other components are running in user mode, including legacy systems encapsulated in virtual machines. On top of the “L4Re Runtime Environment” you see a selection of native components (“microapps”): real-time applications, cryptographic services, and drivers. The L4Re system isolates all components from each other, spatially and temporally.

L4Re Microkernel

The L4Re microkernel uses an evolved L4 microkernel interface based on object capabilities. The microkernel manages and protects capabilities as object references with virtual (protection-domain-local) names. L4Re microkernel and runtime environment constitute a seamless capability system that names all (kernel and userspace-implemented) objects and resources and provides a uniform and secure access method for them (invoke system call).

The microkernel is the kernel component of the L4Re system. In traditional L4 microkernel fashion, it implements only those mechanisms that need to reside in kernel mode: address spaces, threads, and inter-process communication. All other operating-system components, including all device drivers and access policies, are implemented in user-mode application programs.

Unlike traditional L4 kernels, the L4Re microkernel provides access control (through local naming) and security enhancements aimed at preventing resource exhaustion.

The L4Re microkernel supports various modern hardware platforms with ARM, MIPS, and x86 CPUs (32 and 64 bits), multicore and SMP multiprocessing, and hardware virtualization.

L4Re Runtime Environment

The L4Re runtime environment comprises a set of runtime services, APIs, and libraries for developing native L4Re applications. These applications do not have to rely on legacy monolithic operating systems (such as a Linux system running in a separate compartment or VM). Hence, they may have an extremely small trusted computing base (TCB). L4Re services and libraries are structured in modules, allowing them to scale to even the smallest systems or TCBs.

L4Re contains the following components: C and C++ standard libraries, pthreads, scriptable initialization component, shared memory services, memory and address-space management, memory allocation, program loader and shared libraries, device management, and a secure GUI component; the latter allows users to exactly determine the component that is presenting the current screen contents and receiving input events.

L4Re’s standard programming language for native applications is C++. In this language, L4Re capabilities, data types and module interfaces can be expressed natively. C bindings are available as well; these are typically used when porting existing applications or systems (like L4Linux).

L4Linux and L4Android

L4Linux is a paravirtualized Linux kernel that has been ported to the native L4Re interfaces. It provides L4Re with a complete Linux environment including Linux device drivers. L4Linux does not depend on hardware virtualization and is available on both ARM and x86 CPUs.

L4Linux is binary compatible with native Linux kernels, allowing the execution of unmodified user applications. Any Linux distribution can be used as the Linux user environment. Android is supported as well.

Learn more

L4Re is a mature system that has evolved for more than a decade out of earlier microkernel-based systems at TU Dresden. Please find more information at the L4Re website:

Kernkonzept will provide additional documentation resources on its own website as they become available.