„L4 (Mikrokernel)“ – Versionsunterschied
| [ungesichtete Version] | [gesichtete Version] |
Ad.ac (Diskussion | Beiträge) KKeine Bearbeitungszusammenfassung |
Y2kbug (Diskussion | Beiträge) →Entwicklung: Korr.: 1. Intel-Plattformen bis 2017 sind nicht mehr neu, sondern waren damals neuer als jene, auf denen L4 entwickelt wurde. 2. x86 als Architektur, nicht "bloß" als Prozessor... |
||
| (109 dazwischenliegende Versionen von 70 Benutzern werden nicht angezeigt) | |||
| Zeile 1: | Zeile 1: | ||
'''L4''' ist der Name einer Familie von [[Mikrokernel]]n, basierend auf Konzepten und ersten erfolgreichen Implementierungen von [[Jochen Liedtke]] (daher '''L'''4). 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 (Kernel)|Mach]]).<ref>{{Internetquelle |autor=Jason Wu, Dan Williams, Hakim Weatherspoon |url=https://www.cs.cornell.edu/courses/cs6410/2010fa/lectures/06-microkernels.pdf |titel=Microkernels: Mach and L4 |seiten=2 |format=PDF; 1,6 MB |sprache=en |abruf=2018-08-12 |abruf-verborgen=0}}</ref> Ein weiterer Mikrokernel der zweiten Generation ist z. B. [[QNX]].<ref name="heiseonline_507011">{{Heise online |ID=507011 |Titel=Gemeinsam einsam |Autor=Peter Wächtler |Datum=2009-04-30 |Abruf=2022-10-02 |Zitat=Microkernel als Unterbau … Ein bekannter quelloffener Vertreter ist der Microkernel L4. Er zeichnet sich durch ein effizientes synchrones Message Passing aus, ebenso wie der QNX-Microkernel. Beide gelten als Microkernel der zweiten Generation – obwohl QNX älter ist als etwa Mach, der bekannteste Vertreter der ersten Generation…}}</ref> |
|||
| ⚫ | |||
== Entwicklung == |
|||
Der Mikrokernel L4 wurde von Liedtke am [[IBM T.J. Watson Research Center]] in Hawthorne entwickelt. Derzeit wird das freie Betriebssystem GNU/[[HURD]] auf L4 portiert. Inzwischen wird mit L4 hauptsächlich das [[Application Programming Interface|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. |
|||
Der erste L4-Kernel wurde von Liedtke am [[GMD-Forschungszentrum Informationstechnik]] (GMD) unter der Bezeichnung „Schnittstellenversion 2“ entwickelt. Während seines Aufenthalts am [[IBM]] [[Thomas J. Watson Research Center]] in [[Hawthorne (New York)|Hawthorne]] experimentierte er mit diversen Aspekten der Kernel-Schnittstelle (Version X). Dies führte nach seinem Umzug an die [[Karlsruher Institut für Technologie|Universität Karlsruhe]] zu mehreren vollständigen Neuimplementierungen. Parallel dazu erfolgten Implementierungen an der [[Technische Universität Dresden|TU Dresden]] und der [[University of New South Wales]] (UNSW). L4 bezeichnet somit heute eine Familie von Kerneln mit unterschiedlichen, aber verwandten Schnittstellen und Implementierungen. |
|||
Es existieren Implementierungen der L4-API der [[Universität Karlsruhe]] (Hazelnut, Pistachio) und der [[TU Dresden]] (Fiasco). |
|||
| ⚫ | 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 (Betriebssystem)|L2]]''' ('''E'''xtendable Multi'''u'''ser '''M'''icroprocessor [[ELAN (Programmiersprache)|'''EL'''AN]]-System, kurz „Eumel“) freigegeben, eine zunächst auf 8 Bit, dann auf 16 Bit ausgelegte [[Assemblersprache|Assembler]]-[[Implementierung]] auf [[Intel]]-[[x86-Architektur|x86]]-Basis, die auch nach Japan transferiert wurde. 1988 entwickelte Liedtke am [[GMD-Forschungszentrum Informationstechnik|GMD]] das 32-Bit-System '''[[L3 (Betriebssystem)|L3]]''', welches auf neueren Intel-Plattformen bis zum Jahr 2017 produktiv beim [[TÜV Süd]] im Einsatz war. |
||
| ⚫ | |||
== Versionen und Anwendungsgebiete == |
|||
Auf Basis von L4 können, dem modularen Prinzip der [[Mikrokernel|Mikrokernel]] folgend, graphische Nutzeroberflächen (wie [[DOpE]]), der [[Linux]]-Kern im Nutzermodus ([[L4Linux]], Wombat) und ganzheitlich echtzeitfähige [[Betriebssystem|Betriebssysteme]] (wie [[DROPS]]) laufen. |
|||
Mit L4 wird heute sowohl das [[Application Programming Interface|API]] als auch die Implementierung bezeichnet. Die erste stabile und veröffentlichte Version war V2, implementiert von Liedtke in [[Assemblersprache|Assembler]] auf [[Intel 80486|i486]] und [[Intel Pentium|Pentium]] (32-Bit-[[x86-Architektur|x86]] bzw. [[IA-32]]). Diese wurde später von der [[Technische Universität Dresden|TU Dresden]] unter dem Namen „Fiasco“ in [[C++]] auf Pentium umgesetzt und von der [[University of New South Wales]] (UNSW) unter dem Namen „C/Assembler Kerneln“ [[Portierung (Software)|portiert]] auf [[MIPS-Architektur|MIPS64]] und [[Alpha-Prozessor|Alpha]]. 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 auf [[Arm-Architektur|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-Architektur|x86]][[IA-32|-32]] und [[PowerPC]]-32 implementiert und leicht zeitverschoben auch auf [[Itanium-Architektur|Itanium]] portiert, jedoch nie vervollständigt. Pistachio wurde an der [[University of New South Wales|UNSW]] auf MIPS, Alpha und Arm portiert (eine [[SPARC-Architektur|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<ref>{{Webarchiv|url=http://okl4.org/ |wayback=20080820043831 |text=OKL4-Website |archiv-bot=2019-04-24 14:16:44 InternetArchiveBot }}</ref> weiterentwickelt und vermarktet, speziell im Mobilfunkbereich. |
|||
| ⚫ | |||
Die Konstruktion von beweisbar sicheren Systemen wird mit dem Projekt [[VFiasco]] angestrebt, welches durch den Einsatz von aus der [[Mathematik]] und theoretischen [[Informatik]] bekannten [[Coalgebra|Coalgebren]] verifiziert wird. |
|||
Seit 2004 entwickelte NICTA eine Version unter dem Namen seL4<ref>{{Webarchiv|url=http://ertos.nicta.com.au/research/sel4 |wayback=20090814162812 |text=sel4-Website |archiv-bot=2019-04-24 14:16:44 InternetArchiveBot }}</ref> (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 als [[Open Source]] unter [[GNU General Public License]] GPLv2-Lizenz. Bibliotheken sowie [[Ring (CPU)|Userland]]-Tools veröffentlichten die Hersteller unter der [[BSD-Lizenz]].<ref>{{Internetquelle| url=https://www.heise.de/newsticker/meldung/Microkernel-seL4-beweisbar-fehlerfrei-2277750.html |titel=Microkernel seL4: beweisbar fehlerfrei| datum=2014-07-29| zugriff=2014-08-07}}</ref> |
|||
Einige Grundkonzepte von L4 werden in der Luftfahrtindustrie eingesetzt. Bei Anwendungen im [[Airbus A400M]] sowie im [[Airbus A350]] wird, basierend auf dem [[PikeOS]]-Mikrokernel, die [[Serverpartitionierung|Partitionierung]] von sicherheitskritischen Anwendungen auf [[Eingebettetes System|eingebetteten Systemen]] sichergestellt. |
|||
== Besondere Merkmale == |
|||
| ⚫ | |||
Auf L4 können, dem modularen Prinzip des Mikrokernels folgend, graphische Nutzeroberflächen (wie [[DOpE]]), der [[Linux (Kernel)|Linux-Kernel]] im Nutzermodus ([[L4Linux]], Wombat) und ganzheitlich echtzeitfähige [[Betriebssystem]]e parallel laufen. Ein Beispiel dafür ist das Mobiltelefon „Motorola Evoke“. 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 unter 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 General Public License|GNU GPL]] als [[freie Software]] lizenziert.<ref>Homepage des Gruppe L4Linux: [https://l4linux.org/ FAQ]</ref> |
||
== Bibliotheken == |
|||
| ⚫ | |||
== seL4: Beweisbar sichere Systeme == |
|||
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.<ref>{{Webarchiv|url=http://ertos.nicta.com.au/research/l4.verified |wayback=20090822042016 |text=Archivierte Kopie |archiv-bot=2019-04-24 14:16:44 InternetArchiveBot }}</ref><ref>{{Webarchiv|url=http://pressetext.de/news/090817022/sicherheits-beweis-fuer-betriebssystem-kernel/ |wayback=20090830052254 |text=Archivierte Kopie |archiv-bot=2022-03-13 04:19:17 InternetArchiveBot }}</ref> Bei NICTA verifizierte man dafür 7500 Zeilen C-Quellcode und mehr als 10.000 Theoreme. Zur Beweisführung verwendete man den Theorembeweiser [[Isabelle (Theorembeweiser)|Isabelle/HOL]], der gesamte Beweis bestand aus etwa 200.000 Zeilen Isabelle-Code. |
|||
== Beispiel „Merkelphone" SiMKo3“ == |
|||
Seit 2013 erhält das Thema L4 unter dem Schlagwort „Merkelphone“ (dem SiMKo3) neue Aufmerksamkeit.<ref>Detlef Borchers: [https://www.heise.de/newsticker/meldung/it-sa-Telekom-zeigt-abhoersicheres-SiMKo-3-Tablet-1974527.html it-sa: Telekom zeigt abhörsicheres SiMKo-3-Tablet], Heise online, 8. Oktober 2013</ref> Siehe dazu auch die Artikel [[Sichere mobile Kommunikation]] (SiMKo) und [[Multiple Independent Levels of Security]] (MILS). |
|||
== Einzelnachweise == |
|||
<references/> |
|||
== Weblinks == |
== Weblinks == |
||
| ⚫ | |||
| ⚫ | |||
* [http://edageek.com/2007/04/17/open-kernel-labs-okl4-microkernel Open Kernel Labs Announces OKL4 ] (Commercial L4 Microkernel) – 17. April 2007 |
|||
* [http://www.l4ka.org L4Ka] - Implementierungen L4Ka::Pistachio und L4Ka::Hazelnut |
|||
* [http://os.inf.tu-dresden.de/fiasco/ Fiasco] – Eine freie C++-Implementierung für x86- und ARM-Prozessoren |
|||
* [http://www.cse.unsw.edu.au/~disy/L4/ UNSW] - Portierung auf die Architekturen [[Alpha-Prozessor|Alpha]] und [[MIPS-Architektur|MIPS]] |
|||
| ⚫ | |||
* [http://os.inf.tu-dresden.de/drops/ DROPS] - The Dresden Real-Time Operating System Project |
|||
* [http://os.inf.tu-dresden.de/vfiasco/ VFiasco] - Verified Fiasco Project |
|||
* [http://os.inf.tu-dresden.de/L4/l3.html L3] - Vorgänger-System zu L4, beim [[TÜV SÜD]] im Einsatz |
|||
| ⚫ | |||
| ⚫ | |||
* [http://ertos.nicta.com.au/ NICTA] – Versionen für eingebettete Systeme, Beweis funktionaler Korrektheit |
|||
| ⚫ | |||
[[en:L4 microkernel family]] |
|||
[[es:L4 (microkernel)]] |
|||
[[fr:L4]] |
|||
[[ja:L4]] |
|||
[[pl:L4 (informatyka)]] |
|||
[[zh:L4微内核系列]] |
|||
Aktuelle Version vom 24. Mai 2025, 12:33 Uhr
L4 ist der Name einer Familie von Mikrokerneln, basierend auf Konzepten und ersten erfolgreichen Implementierungen von Jochen Liedtke (daher L4). 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]
Entwicklung
[Bearbeiten | Quelltext bearbeiten]Der erste L4-Kernel wurde von Liedtke am GMD-Forschungszentrum Informationstechnik (GMD) unter der Bezeichnung „Schnittstellenversion 2“ entwickelt. Während seines Aufenthalts am IBM Thomas J. Watson Research Center in Hawthorne experimentierte er mit diversen Aspekten der Kernel-Schnittstelle (Version X). Dies führte nach seinem Umzug an die Universität 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 Kerneln 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 neueren Intel-Plattformen bis zum Jahr 2017 produktiv beim TÜV Süd im Einsatz war.
Versionen und Anwendungsgebiete
[Bearbeiten | Quelltext bearbeiten]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 (32-Bit-x86 bzw. IA-32). Diese wurde später von der TU Dresden unter dem Namen „Fiasco“ in C++ auf Pentium umgesetzt und von der University of New South Wales (UNSW) unter dem Namen „C/Assembler Kerneln“ portiert auf MIPS64 und Alpha. 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 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-32 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[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 als Open Source unter GNU General Public License GPLv2-Lizenz. Bibliotheken sowie Userland-Tools veröffentlichten die Hersteller unter der BSD-Lizenz.[5]
Einige Grundkonzepte von L4 werden in der Luftfahrtindustrie eingesetzt. Bei Anwendungen im Airbus A400M sowie im Airbus A350 wird, basierend auf dem PikeOS-Mikrokernel, die Partitionierung von sicherheitskritischen Anwendungen auf eingebetteten Systemen sichergestellt.
Besondere Merkmale
[Bearbeiten | Quelltext bearbeiten]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-Kernel im Nutzermodus (L4Linux, Wombat) und ganzheitlich echtzeitfähige Betriebssysteme parallel laufen. Ein Beispiel dafür ist das Mobiltelefon „Motorola Evoke“. 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 unter Linux
[Bearbeiten | Quelltext bearbeiten]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.[6]
Bibliotheken
[Bearbeiten | Quelltext bearbeiten]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.
seL4: Beweisbar sichere Systeme
[Bearbeiten | Quelltext bearbeiten]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 Theorembeweiser Isabelle/HOL, der gesamte Beweis bestand aus etwa 200.000 Zeilen Isabelle-Code.
Beispiel „Merkelphone" SiMKo3“
[Bearbeiten | Quelltext bearbeiten]Seit 2013 erhält das Thema L4 unter dem Schlagwort „Merkelphone“ (dem SiMKo3) neue Aufmerksamkeit.[9] Siehe dazu auch die Artikel Sichere mobile Kommunikation (SiMKo) und Multiple Independent Levels of Security (MILS).
Einzelnachweise
[Bearbeiten | Quelltext bearbeiten]- ↑ Jason Wu, Dan Williams, Hakim Weatherspoon: Microkernels: Mach and L4. (PDF; 1,6 MB) S. 2, abgerufen am 12. August 2018 (englisch).
- ↑ Peter Wächtler: Gemeinsam einsam. In: Heise online. 30. April 2009. Abgerufen am 2. Oktober 2022.; Zitat: „Microkernel als Unterbau … Ein bekannter quelloffener Vertreter ist der Microkernel L4. Er zeichnet sich durch ein effizientes synchrones Message Passing aus, ebenso wie der QNX-Microkernel. Beide gelten als Microkernel der zweiten Generation – obwohl QNX älter ist als etwa Mach, der bekannteste Vertreter der ersten Generation…“.
- ↑ OKL4-Website ( des vom 20. August 2008 im Internet Archive) Info: Der Archivlink wurde automatisch eingesetzt und noch nicht geprüft. Bitte prüfe Original- und Archivlink gemäß Anleitung und entferne dann diesen Hinweis.
- ↑ sel4-Website ( des vom 14. August 2009 im Internet Archive) Info: Der Archivlink wurde automatisch eingesetzt und noch nicht geprüft. Bitte prüfe Original- und Archivlink gemäß Anleitung und entferne dann diesen Hinweis.
- ↑ Microkernel seL4: beweisbar fehlerfrei. 29. Juli 2014, abgerufen am 7. August 2014.
- ↑ Homepage des Gruppe L4Linux: FAQ
- ↑ Archivierte Kopie ( des vom 22. August 2009 im Internet Archive) Info: Der Archivlink wurde automatisch eingesetzt und noch nicht geprüft. Bitte prüfe Original- und Archivlink gemäß Anleitung und entferne dann diesen Hinweis.
- ↑ Archivierte Kopie ( des vom 30. August 2009 im Internet Archive) Info: Der Archivlink wurde automatisch eingesetzt und noch nicht geprüft. Bitte prüfe Original- und Archivlink gemäß Anleitung und entferne dann diesen Hinweis.
- ↑ Detlef Borchers: it-sa: Telekom zeigt abhörsicheres SiMKo-3-Tablet, Heise online, 8. Oktober 2013
Weblinks
[Bearbeiten | Quelltext bearbeiten]- L4 auf der Website der TU Dresden
- Open Kernel Labs Announces OKL4 (Commercial L4 Microkernel) – 17. April 2007