L4 (microkernel)
L4 is the name of a family of microkernels based on concepts and first successful implementations by Jochen Liedtke (hence L 4).
development
The first L4 kernel was developed by Liedtke at the GMD Research Center for Information Technology (GMD) under the name "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). After moving to the University of Karlsruhe, this led to several complete new implementations. At the same time, implementations took place at the TU Dresden and the University of New South Wales (UNSW). Today L4 denotes a family of kernels with different, but related interfaces and implementations.
The development line is based on L1 , an interpreter designed by Liedtke for a subset of Algol 60 on an 8-bit computer with 4 KB main memory. 1979 L2 ( E xtendable Multi u ser M icroprocessor EL AN system, known as "Eumel") released a designed initially to 8 bits, then to 16-bit assembly language - Implementation on Intel - x86 basis that has been transferred to Japan . In 1988 Liedtke developed the 32-bit system L3 at the GMD , which was used productively at TÜV Süd on new Intel platforms until 2017 .
Versions and areas of application
L4 is now used to denote both the API and the implementation. The first stable and published version was V2, implemented by Liedtke in assembler on i486 and Pentium . This was later implemented by the TU Dresden under the name "Fiasco" in C ++ to Intel Pentium and ported to the MIPS architecture (MIPS64) and by the University of New South Wales (UNSW) under the name "C / Assembler Kerneln" the alpha processor . At IBM, Liedtke further developed the assembler implementation as version X, followed in Karlsruhe by a C implementation called "Hazelnut (version X.1)", originally on Pentium, later ported to ARM . After Liedtke's death (2001), version X.2 emerged from this in early 2002 in Karlsruhe (which later became version 4 with slight changes), implemented in C ++ under the name “Pistachio”. Pistachio was implemented in parallel on x86 and PowerPC- 32 and ported to Itanium with a slight time lag, but never completed. Pistachio was ported to MIPS, Alpha and ARM at UNSW (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 version specially tailored for embedded systems called NICTA-embedded, implemented as NICTA :: Pistachio-embedded. This was finally further developed and marketed as OKL4 by the NICTA spin-off Open Kernel Labs, especially in the mobile communications sector.
Since 2004 NICTA has developed a version under the name seL4 (secure embedded L4), which is specifically aimed at security-critical applications in the embedded area. In "seL4", object references and access rights are represented exclusively by so-called capabilities , and kernel resources are subject to the same access mechanisms as user objects. In July 2014 the manufacturers General Dynamics C4 Systems and NICTA published the source code of seL4 as Open Source under the GNU General Public License GPLv2 license. Libraries, and userland tools published manufacturers under the BSD license .
Some basic concepts of L4 are used in the aerospace industry. For applications in the Airbus A400M and the Airbus A350 , the partitioning of safety-critical applications on embedded systems is ensured based on the PikeOS microkernel .
Special features
Kernels based on the L4 API offer a synchronous IPC (interprocess communication) , simple interrupt and thread management as well as simple, external memory management .
Following the modular principle of the microkernel, graphical user interfaces (such as DOpE ), the Linux kernel in user mode ( L4Linux , Wombat) and fully real-time operating systems can run in parallel on L4. One example of this is the Motorola Evoke mobile phone. A Linux system (which provides the user interface) is on OKL4 and, at the same time, Qualcomm's BREW operating system is active as a real-time application for the modem functionality.
L4 on Linux
The L4 implementation Fiasco-UX allows the microkernel itself to be operated as an application under Linux , which significantly simplifies development, similar to the principle of User Mode Linux . The L4 implementation was licensed as free software under the GNU GPL .
Libraries
The libraries L4Env (Fiasco), Iguana and Kenge (Pistachio-embedded) and libokl4 (OKL4) are available for developers of applications based on the microkernel.
seL4: Demonstrably secure systems
In 2009, a kernel suitable for general applications was formally verified for the first time at the research institute NICTA in cooperation with UNSW with seL4. That is, it has been mathematically proven that the implementation meets the specification of the kernel and is therefore functionally correct. This means, among other things, that the kernel has been proven not to contain any of the design errors ( buffer overflows , pointer errors and memory leaks) that have been widespread to date. NICTA verified 7500 lines of C source code and more than 10,000 theorems. The theorem prover Isabelle / HOL was used for the proof, the entire proof consisted of about 200,000 lines of Isabelle code.
Example "Merkelphone" SiMKo3 "
Since 2013, the topic L4 has received new attention under the keyword “Merkelphone” (the SiMKo3). See also the articles Secure mobile communication (SiMKo) and Multiple Independent Levels of Security (MILS).
Individual evidence
- ↑ OKL4 website ( Memento of the original from August 20, 2008 in the Internet Archive ) Info: The archive link was inserted automatically and has not yet been checked. Please check the original and archive link according to the instructions and then remove this notice.
- ↑ sel4 website ( memento of the original dated August 14, 2009 in the Internet Archive ) Info: The archive link was inserted automatically and has not yet been checked. Please check the original and archive link according to the instructions and then remove this notice.
- ↑ Microkernel seL4: demonstrably free of errors. July 29, 2014, accessed August 7, 2014 .
- ↑ Homepage of the L4Linux group: FAQ
- ↑ Archived copy ( Memento of the original from August 22, 2009 in the Internet Archive ) Info: The archive link was inserted automatically and has not yet been checked. Please check the original and archive link according to the instructions and then remove this notice.
- ↑ http://pressetext.de/news/090817022/sicherheits-beweis-fuer-betriebssystem-kernel/
- ↑ Detlef Borchers: it-sa: Telekom shows tap-proof SiMKo-3 tablet , Heise online, October 8, 2013
Web links
- L4 on the website of the TU Dresden
- Open Kernel Labs Announces OKL4 (Commercial L4 Microkernel) - April 17, 2007