L4 ist der Name einer Familie vonMikrokerneln, basierend auf Konzepten und ersten erfolgreichen Implementierungen vonJochen Liedtke (daherL4). L4 gilt als ein Mikrokernel der zweiten Generation, der das Problem des zu langsamen Interkommunikationsprozesses der ersten Mikrokernel-Generation nicht mehr aufweist (zur ersten Generation zählt u. a.Mach).[1] Ein weiterer Mikrokernel der zweiten Generation ist z. B.QNX.[2]
Der erste L4-Kernel wurde von Liedtke amGMD-Forschungszentrum Informationstechnik (GMD) unter der Bezeichnung „Schnittstellenversion 2“ entwickelt. Während seines Aufenthalts amIBMThomas J. Watson Research Center inHawthorne experimentierte er mit diversen Aspekten der Kernel-Schnittstelle (Version X). Dies führte nach seinem Umzug an dieUniversität Karlsruhe zu mehreren vollständigen Neuimplementierungen. Parallel dazu erfolgten Implementierungen an derTU Dresden und derUniversity of New South Wales (UNSW). L4 bezeichnet somit heute eine Familie von Kerneln mit unterschiedlichen, aber verwandten Schnittstellen und Implementierungen.
Die Entwicklungslinie basiert aufL1, einem von Liedtke konzipierten Interpreter für eine Teilmenge vonAlgol 60 auf einem 8-Bit-Rechner mit 4 KB Hauptspeicher. 1979 wurdeL2 (Extendable MultiuserMicroprocessorELAN-System, kurz „Eumel“) freigegeben, eine zunächst auf 8 Bit, dann auf 16 Bit ausgelegteAssembler-Implementierung aufIntel-x86-Basis, die auch nach Japan transferiert wurde. 1988 entwickelte Liedtke amGMD das 32-Bit-SystemL3, welches auf neuen Intel-Plattformen bis zum Jahr 2017 produktiv beimTÜV Süd im Einsatz war.
Mit L4 wird heute sowohl dasAPI als auch die Implementierung bezeichnet. Die erste stabile und veröffentlichte Version war V2, implementiert von Liedtke inAssembler aufi486 undPentium (32-Bit-x86 bzw.IA-32). Diese wurde später von derTU Dresden unter dem Namen „Fiasco“ inC++ auf Pentium umgesetzt und von derUniversity of New South Wales (UNSW) unter dem Namen „C/Assembler Kerneln“portiert aufMIPS64 undAlpha. Bei IBM entwickelte Liedtke die Assembler-Implementierung als Version X weiter, gefolgt in Karlsruhe von einer C-Implementierung namens „Hazelnut (Version X.1)“, ursprünglich auf Pentium, später portiert aufArm. 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 aufx86-32 undPowerPC-32 implementiert und leicht zeitverschoben auch aufItanium portiert, jedoch nie vervollständigt. Pistachio wurde an derUNSW auf MIPS, Alpha und Arm portiert (eineSPARC-Version wurde nie abgeschlossen). In Dresden wurde API Version 4 in Fiasco implementiert.
Das australische IKT-ForschungszentrumNICTA entwickelte, basierend auf V4, eine speziell aufeingebettete 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[3] weiterentwickelt und vermarktet, speziell im Mobilfunkbereich.
Seit 2004 entwickelte NICTA eine Version unter dem Namen seL4[4] (secure embedded L4), die speziell auf sicherheitskritische Anwendungen im eingebetteten Bereich zielt. In „seL4“ werden Objektreferenzen und Zugriffsrechte ausschließlich durch sogenannte Fähigkeiten (capabilities) repräsentiert, und Kernel-Ressourcen unterliegen denselben Zugriffsmechanismen wie Nutzerobjekte. Im Juli 2014 veröffentlichten die Hersteller General Dynamics C4 Systems und NICTA den Quellcode von seL4 alsOpen Source unterGNU General Public License GPLv2-Lizenz. Bibliotheken sowieUserland-Tools veröffentlichten die Hersteller unter derBSD-Lizenz.[5]
Einige Grundkonzepte von L4 werden in der Luftfahrtindustrie eingesetzt. Bei Anwendungen imAirbus A400M sowie imAirbus A350 wird, basierend auf demPikeOS-Mikrokernel, diePartitionierung von sicherheitskritischen Anwendungen aufeingebetteten Systemen sichergestellt.
Kernel, die auf dem L4-API basieren, bieten eine synchroneIPC (Interprozesskommunikation), einfachesInterrupt- und Threadmanagement sowie eine einfache, externeSpeicherverwaltung.
Auf L4 können, dem modularen Prinzip des Mikrokernels folgend, graphische Nutzeroberflächen (wieDOpE), derLinux-Kernel im Nutzermodus (L4Linux, Wombat) und ganzheitlich echtzeitfähigeBetriebssysteme parallel laufen. Ein Beispiel dafür ist das Mobiltelefon „Motorola Evoke“. Hier ist auf OKL4 einLinux-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.
Die L4-ImplementierungFiasco-UX erlaubt, dass der Mikrokernel selbst wiederum als Anwendung unterLinux betrieben werden kann, was die Entwicklung deutlich vereinfacht, ähnlich dem Prinzip vonUser Mode Linux. Die L4-Implementierung wurde unter derGNU GPL alsfreie Software lizenziert.[6]
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.
Im Jahr 2009 wurde am Forschungsinstitut NICTA in Zusammenarbeit mit der UNSW mit seL4 erstmals ein für allgemeine Anwendungen tauglicher Kernel formal verifiziert, d. h., es wurde mathematisch bewiesen, dass die Implementierung die Spezifikation des Kernels erfüllt und somit funktional korrekt ist. Dies bedeutet unter anderem, dass der Kernel nachweislich keinen der bisher verbreiteten Entwurfsfehler (Speicherüberläufe (Buffer Overflow), Zeigerfehler und Speicherlecks) enthält.[7][8] Bei NICTA verifizierte man dafür 7500 Zeilen C-Quellcode und mehr als 10.000 Theoreme. Zur Beweisführung verwendete man den TheorembeweiserIsabelle/HOL, der gesamte Beweis bestand aus etwa 200.000 Zeilen Isabelle-Code.
Seit 2013 erhält das Thema L4 unter dem Schlagwort „Merkelphone“ (dem SiMKo3) neue Aufmerksamkeit.[9] Siehe dazu auch die ArtikelSichere mobile Kommunikation (SiMKo) undMultiple Independent Levels of Security (MILS).
