L4 microkernel family

L4 is the name of a family of micro- kernels, based on concepts and first successful implementations of Jochen Liedtke (hence L4).

Development

The first L4 kernel was of Liedtke at GMD - Research Center for Information Technology ( GMD) developed called "Interface Version 2". During his stay at the IBM Thomas J. Watson Research Center in Hawthorne, he experimented with various aspects of the kernel interface ( version X). This led after his move to the University of Karlsruhe for more complete re-implementations. In parallel implementations were carried out at the TU Dresden and the University of New South Wales ( UNSW ). Thus L4 indicates today a family of kernels with different but related interfaces and implementations.

The line of development is based on L1, one designed by Liedtke interpreter for a subset of Algol 60 on an 8 -bit machine with 4 KB of main memory. 1979 L2 ( Extendable multiuser Microprocessor ELAN system, " Eumel " for short) released a designed initially to 8-bit, then 16 bit assembler implementation on Intel x86 - base that has been transferred to Japan. In 1988, Liedtke at GMD, the 32 -bit system L3, which is productive at TÜV Süd in use on the new Intel platforms today.

Versions and applications

L4 is now both the API and the implementation respectively. The first stable version was released V2, implemented by Liedtke in assembler on i486 and Pentium. This was later used by the TU Dresden under the name of " Fiasco " in C on Intel Pentium implemented and from the University of New South Wales ( UNSW ) under the name "C / assembler kernels " ported to the MIPS architecture ( MIPS64 ) and the Alpha processor. At IBM Liedtke developed the assembler implementation as version X on, followed in Karlsruhe from a C implementation called " Hazlenut ( version X.1 ) ", originally on Pentium and later ported to ARM. According to Liedtke's death (2001) from the version was created in early 2002 in Karlsruhe X.2 ( from the later with slight changes version 4 ), implemented in C under the name of " Pistachio ". Pistachio has been implemented in parallel on x86 and PowerPC 32 and slightly time-shifted ported to Itanium, but never completed. Pistachio was at UNSW on MIPS, Alpha and ARM ported ( a SPARC version was never completed). In Dresden API Version 4 was implemented in Fiasco.

The Australian ICT research center NICTA developed based on V4, a specially tailored for embedded systems version called NICTA -embedded, implemented as NICTA :: Pistachio -embedded. This was finally developed by the NICTA spin-off Open Kernel Labs OKL4 as and marketed, especially in the mobile sector.

Since 2004 NICTA has developed a version under the name SEL4 (secure embedded L4 ), which specifically targets safety-critical applications in the embedded sector. In " SEL4 " object references and privileges exclusively by so-called skills ( "capabilities" ) are represented, and kernel resources subject to the same access mechanisms such as user objects.

Some basic concepts of L4 are used in the aerospace industry. For applications in the Airbus A400M and the A350 is based on ensuring the PikeOS microkernel, the partitioning of safety-critical applications on embedded systems.

Special Features

Kernels that are based on the L4 API, provide a synchronous IPC ( interprocess communication ), simple interrupt and thread management, and a simple, external memory management.

At L4 can following the modular principle of the micro- kernel, graphical user interfaces (such as DOPE), the Linux kernel in user mode ( L4Linux, Wombat ) and holistic real-time operating systems running in parallel. An example of this is the mobile phone "Motorola Evoke ". Here's OKL4 on a Linux system (which provides the user interface ) and at the same time as a real-time application for the modem functionality, the BREW operating system from Qualcomm active.

L4 on Linux

The L4 implementation Fiasco -UX allows the microkernel itself in turn be run as an application on Linux, which greatly simplifies the development, similar to the principle of User Mode Linux. The L4 implementation is licensed under the GNU GPL as free software.

Libraries

For developers of applications based on the microkernel libraries are L4Env ( Fiasco ), Iguana and Kenge ( Pistachio -embedded ) and libokl4 ( OKL4 ) are available.

Provably secure systems

In 2009 NICTA has been verified in collaboration with the UNSW with SEL4 first USEFULLY a general purpose kernel formally at the research institute, ie It has been proven mathematically, that the implementation satisfies the specification of the kernel and thus is functionally correct. This means, among other things, that the kernel does not contain any of the previously proven common design errors ( memory overflows ( buffer overflow ), pointer errors and memory leaks ). At NICTA to this verified 7500 lines of C source and more than 10,000 theorems. Was used to proof the theorem prover Isabelle / HOL, the entire evidence consisted of about 200,000 lines of Isabelle code.

" Merkel Phone"

At present, new attention the subject receives L4 under the slogan " Merkel Phone".

494089
de