L4 (Mikrokern)

L4 ist der Name einer Familie von Mikrokernen, basierend auf Konzepten und ersten erfolgreichen Implementierungen von Jochen Liedtke (daher L4).

Entwicklung

Der erste L4-Kern wurde von Liedtke am GMD-Forschungszentrum Informationstechnik (GMD) entwickelt, die sog. Schnittstellenversion 2. Während seines Aufenthalts am IBM Thomas J. Watson Research Center in Hawthorne experimentierte er mit diversen Aspekten der Kernschnittstelle (Version X). Dies führte nach seinem Umzug an die Uni Karlsruhe zu mehreren vollständigen Neuimplementierungen. Parallel dazu erfolgten Implementierungen an der TU Dresden und der University of New South Wales (UNSW). L4 bezeichnet somit heute eine Familie von Kernen mit unterschiedlichen, aber verwandten Schnittstellen und Implementierungen.

Die Entwicklungslinie basiert auf L1, einem von Liedtke konzipierten 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 heute sowohl das API, als auch die Implementierung bezeichnet. Die erste stabile und veröffentlichte Version war V2, implementiert von Liedtke in Assembler auf i486 und Pentium, in C++ von Fiasco (Dresden) auf Pentium, und von den UNSW C/Assembler Kernen auf MIPS64 und Alpha. Bei IBM entwickelte Liedtke die Assemblerimplementierung als Version X weiter, gefolgt in Karlsruhe von einer C-Implementierung namens Hazlenut (Version X.1), ursprünglich auf Pentium, später portiert auf ARM. Nach Liedtkes Tod (2001) entstand daraus Anfang 2002 in Karlsruhe die Version X.2 (aus der später mit leichten Änderungen die Version 4 wurde), implementiert in C++ unter dem Namen Pistachio. Pistachio wurde parallel auf x86 und PowerPC-32 implementiert, und leicht zeitverschoben auch auf Itanium portiert, jedoch nie vervollständigt. Pistachio wurde an der UNSW auf MIPS, Alpha und ARM portiert (eine SPARC Version wurde nie abgeschlossen). In Dresden wurde API Version 4 in Fiasco implementiert.

Das australische IKT-Forschungszentrum NICTA entwickelte, basierend auf V4, eine speziell auf eingebettete Systeme zugeschnittene Version namens NICTA-embedded, implementiert als NICTA::Pistachio-embedded. Diese wurde schließlich von der NICTA-Ausgründung Open Kernel Labs als OKL4^[1] weiterentwickelt und vermarktet, speziell im Mobilfunkbereich.

Seit 2004 entwickelte NICTA eine Version unter dem Namen seL4^[2] (secure embedded L4) die speziell auf sicherheitskritische Anwendungen im eingebetteten Bereich zielt. In seL4 werden Objektreferenzen und Zugriffsrechte ausschließlich durch capabilities repräsentiert, und Kern-Ressourcen unterliegen den gleichen Zugriffsmechanismen wie Nutzerobjekte.

Einige Grundkonzepte von L4 werden in der Luftfahrtindustrie eingesetzt. Bei Anwendungen im Airbus A400M sowie im Airbus A350 wird basierend auf dem PikeOS Microkernel die Partitionierung von sicherheitskritischen Anwendungen auf eingebetteten Systemen sichergestellt.

Besondere Merkmale

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

Auf L4 können, dem modularen Prinzip des Mikrokernels folgend, graphische Nutzeroberflächen (wie DOpE), der Linux-Kern im Nutzermodus (L4Linux, Wombat) und ganzheitlich echtzeitfähige Betriebssysteme parallel laufen. Ein Beispiel dafür ist das Motorola Evoke Mobiltelefon. Hier ist auf OKL4 ein Linux System (das die Benutzeroberfläche zur Verfügung stellt) und gleichzeitig als Echtzeitanwendung für die Modem-Funktionalität das BREW-Betriebssystem von Qualcomm aktiv.

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.^[3]

Bibliotheken

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

Beweisbar sichere Systeme

Im Jahre 2009 wurde am Forschungsinstitut NICTA in Zusammenarbeit mit der UNSW mit seL4 erstmals ein für allgemeine Anwendungen tauglicher Betriebssystemkern formal verifiziert, d.h. es wurde mathematisch bewiesen, dass die Implementierung die Spezifikation des Kerns erfüllt und somit funktional korrekt ist. Dies bedeutet unter anderem, dass der Kern nachweislich keinen der bisher verbreiteten Entwurfsfehler (Speicherüberläufe (Buffer Overflow), Zeigerfehler und Speicherlecks) enthält.^[4][5] Bei NICTA verifizierte man hierfür 7500 Zeilen C-Quellcode und mehr als 10.000 Theoreme. Die Beweisführung bediente sich des Theorembeweisers Isabelle/HOL, der gesamte Beweis bestand aus etwa 200.000 Zeilen Isabelle-Code.

Einzelnachweise

1. ↑ OKL4-Website
2. ↑ sel4-Website
3. ↑ Homepage des Gruppe L4Linux: FAQ
4. ↑ http://ertos.nicta.com.au/research/l4.verified
5. ↑ http://pressetext.de/news/090817022/sicherheits-beweis-fuer-betriebssystem-kernel/

Weblinks

• 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
• NICTA - Versionen für eingebettete Systeme, Beweis funktionaler Korrektheit
• L4Linux - Linux auf dem L4 Microkernel
• DROPS - The Dresden Real-Time Operating System Project
• VFiasco - Verified Fiasco Project
• L3 - Vorgänger-System zu L4
• Isabelle - Theorembeweiser Isabelle