L4 ist der Name eines Mikrokernels, entworfen und implementiert von Jochen Liedtke. Der Kernel wurde von Liedtke am IBM Thomas J. Watson Research Center in Hawthorne entwickelt. Später wurde er in verschiedenen Implementierungen an der Uni Karlsruhe, der TU Dresden und der University of New South Wales weiterentwickelt.

Entwicklung

Die Entwicklungslinie basiert auf L1, einem Interpreter für eine Teilmenge von Algol 60 auf einem 8-Bit Rechner mit 4 KB Hauptspeicher. 1979 wurde L2 (Extendable Multiuser Microprocessor ELAN-System, kurz „Eumel“) freigegeben, eine zunächst auf 8 Bit, dann auf 16 Bit ausgelegte Assembler-Implementierung auf Intel-x86-Basis, die auch nach Japan transferiert wurde. 1988 entwickelte Liedtke am GMD das 32-Bit-System L3, welches auf neuen Intel-Plattformen bis heute produktiv beim TÜV Süd im Einsatz ist.

Applikationen

Mit L4 wird hauptsächlich das API bezeichnet. Dieses wird nach den stabilen Versionen Version 2 und Version 4 unterschieden, zwischen denen die Entwicklungsstadien X.0, X.1 und X.2 liegen. Aktueller Stand ist Version X.2. Es existieren Implementierungen der L4-API der Universität Karlsruhe (Hazelnut, Pistachio) und der TU Dresden (Fiasco).

Besondere Merkmale

Kernel, die auf dem L4-API basieren, bieten eine synchrone IPC (Interprozesskommunikation), einfaches Interrupt- und Threadmanagement sowie eine einfache, externe Speicherverwaltung.

Auf Basis von L4 können, dem modularen Prinzip der Mikrokernel folgend, graphische Nutzeroberflächen (wie DOpE), der Linux-Kern im Nutzermodus (L4Linux, Wombat) und ganzheitlich echtzeitfähige Betriebssysteme (wie DROPS) laufen.

L4 auf Linux

Die L4-Implementierung Fiasco-UX erlaubt, dass der Mikrokernel selbst wiederum als Anwendung unter Linux betrieben werden kann, was die Entwicklung deutlich vereinfacht, ähnlich dem Prinzip von User Mode Linux. Die L4-Implementierung wurde unter der GNU GPL als Freie Software lizenziert.^[1]

Bibliotheken

Für Entwickler von Anwendungen auf Basis des Mikrokernels stehen die Bibliotheken L4Env (Fiasco), Iguana und Kenge (Pistachio) zur Verfügung.

Beweisbar sichere Systeme

Im Jahre 2009 wurde erstmals am Beispiel des Mikrokernels “Secure Embedded L4″ (seL4) formal und maschinell geprüft der Beweis erbracht, dass ein Betriebssystem-Kern keinen der bisher verbreiteten Entwurfsfehler (Buffer Overflow, Zeigerfehler, Speicherlecks und Speicherüberläufe) enthält ^[2]. Am australischen IKT-Forschungsinstitut NICTA prüfte man hierfür mit einem Programm 7500 C-Quellcode-Zeilen anhand von mehr als 10.000 Theoremen. Die Beweisführung bedient sich der in der theoretischen Informatik bekannten Koalgebren.

Einzelnachweise

1. ↑ Homepage des Gruppe L4Linux: FAQ
2. ↑ http://pressetext.de/news/090817022/sicherheits-beweis-fuer-betriebssystem-kernel/

Weblinks zu zu

• Open Kernel Labs Announces OKL4 (Commercial L4 Microkernel) – 17. April 2007
• L4Hq – L4 Headquarters, Community-Seite für L4-Projekte
• L4Ka – Implementierungen L4Ka::Pistachio und L4Ka::Hazelnut
• Fiasco – Eine freie C++-Implementierung für x86- und ARM-Prozessoren
• UNSW – Portierung auf die Architekturen Alpha und MIPS
• L4Linux – Linux auf dem L4 Microkernel
• DROPS – The Dresden Real-Time Operating System Project
• VFiasco – Verified Fiasco Project
• L3 – Vorgänger-System zu L4