L4 Microkernel -Familie

L4 Microkernel -Familie
Entwickler Jochen liestke
Geschrieben in Montagesprache, dann C, C ++
OS -Familie L4
Arbeitszustand Aktuell
Quellmodell Open Source, geschlossene Quelle
Erstveröffentlichung 1993; Vor 29 Jahren
Marketingziel Zuverlässiges Computer
Verfügbar in Englisch Deutsch
Plattformen Intel i386, x86, x86-64, ARM, MIPS, Sparc
Kernel Typ Mikrokernel
Lizenz Quellcode, Beweise: GPLV2
Bibliotheken, Werkzeug: BSD 2-Klausel
Vorausgegangen von Eumel
Offizielle Website OS.inf.tu-dresden.de/L4

L4 ist eine Familie der zweiten Generation Mikrokernel, verwendet, um eine Vielzahl von Arten von zu implementieren Betriebssysteme (Betriebssystem), obwohl meistens für Unix-artig, Tragbare Betriebssystemschnittstelle (Posix) konforme Typen.

L4, wie sein Vorgänger Microkernel L3wurde geschaffen von Deutsch Informatiker Jochen liestke als Reaktion auf die schlechte Leistung früherer Microkernel-basierter OSS. Lieedtke war der Ansicht, dass ein von Anfang an entworfenes System für hohe Leistung und andere Ziele zu einem Mikrokernel praktischer Verwendung führen könnte. Seine ursprüngliche Implementierung in handcodierter Intel i386-Spezifisch Montagesprache Code im Jahr 1993 weckte ein intensives Interesse an der Computerindustrie. Seit seiner Einführung wurde L4 entwickelt, um zu sein plattformübergreifend und zu verbessern Sicherheit, Isolation und Robustheit.

Es gab verschiedene Neu Implementationen des ursprünglichen Binary L4 Kernel Anwendung Binärschnittstelle (ABI) und seine Nachfolger, einschließlich L4ka :: pistazio (Karlsruhe Institut für Technologie), L4/MIPS (Universität von New South Wales (Unw)), Fiasko (Dresden University of Technology (Tu Dresden)). Aus diesem Grund der Name L4 wurde verallgemeinert und bezieht sich nicht mehr auf die ursprüngliche Implementierung von Lieedtke. Es gilt jetzt für das Ganze Mikrokernel Familie einschließlich des L4 -Kernels Schnittstelle und seine unterschiedlichen Versionen.

L4 ist weit verbreitet. Eine Variante, OKL4 von Offene Kernellabors, verschickt in Milliarden mobiler Geräte.[1][2]

Designparadigma

Angabe der allgemeinen Idee von a Mikrokernel, Logen Zustände:

Ein Konzept wird im Mikrokernel nur dann toleriert, wenn es außerhalb des Kernels bewegt wird, d. H. Durch konkurrierende Implementierungen, die Implementierung der erforderlichen Funktionen des Systems verhindern würde.[3]

In diesem Sinne bietet der L4 -Mikrokernel nur wenige grundlegende Mechanismen: Adressräume (Zusammenfassung Seitentabellen und Bereitstellung des Speicherschutzes), Themen und Planung (Zusammenfassung der Ausführung und Bereitstellung zeitlicher Schutz) und Interprozesskommunikation (für kontrollierte Kommunikation über Isolationsgrenzen hinweg).

Ein Betriebssystem, das auf einem Mikrokernel wie L4 basiert Benutzerraum das Monolithische Kerne wie Linux oder Mikrokernel der älteren Generation umfassen intern. Zum Beispiel ein sicheres Implementieren Unix-artig System, Server müssen dem Rechtsmanagement bereitgestellt werden, das Mach im Kernel enthalten.

Geschichte

Die schlechte Leistung von Mikrokernel der ersten Generation, wie z. Machveranlasste eine Reihe von Entwicklern, das gesamte Mikrokernel-Konzept Mitte der neunziger Jahre erneut zu untersuchen. Das asynchrone In-Kernel-Buffieren Prozesskommunikation Das Konzept, das in Mach verwendet wurde, erwies sich als einer der Hauptgründe für seine schlechte Leistung. Dies induzierte Entwickler von Mach-basierten Betriebssystemen, um einige zeitkritische Komponenten wie Dateisysteme oder Treiber zurück im Kernel zu verschieben. Dies verbesserte zwar die Leistungsprobleme, verstößt zwar eindeutig gegen das Minimalitätskonzept eines echten Mikrokernels (und verschwindet ihre Hauptvorteile).

Eine detaillierte Analyse des Mach -Engpasses zeigte, dass unter anderem es sich befindet Workingset ist zu groß: Der IPC -Code drückt schlechte räumliche Lokalität aus; Das heißt, es führt zu zu vielen Zwischenspeicher Fehler, von denen die meisten in Kernel sind.[3] Diese Analyse führte zu dem Prinzip, dass ein effizienter Mikrokernel so gering sein sollte, dass der Großteil des leistungskritischen Codes in den (ersten) Cache (vorzugsweise ein kleiner Teil des Cache) passt.

L3

Jochen liestke Machen Sie sich auf den Weg, um zu beweisen, dass ein gut gestalteter Dünner Interprozesskommunikation (IPC) -Schicht, mit sorgfältiger Aufmerksamkeit auf Leistung und maschinenspezifische (im Gegensatz zu plattformübergreifende Software) Das Design könnte große Leistungsverbesserungen in der Praxis ergeben. Anstelle von Machs komplexem IPC -System hat sein L3 -Mikrokernel die Nachricht einfach ohne zusätzlichen Overhead übergeben. Die Definition und Implementierung der erforderlichen Sicherheitsrichtlinien wurde als Pflichten der Benutzerraum Server. Die Rolle des Kernels bestand nur darin, den erforderlichen Mechanismus bereitzustellen, damit die Server auf Benutzerebene die Richtlinien durchsetzen können. L3, entwickelt 1988, erwies sich als sicher und robust Betriebssystem, für viele Jahre verwendet, zum Beispiel von Techniker überwachungsverein (Technische Inspektionsvereinigung).

L4 Stammbaum

L4

Nach einiger Erfahrung mit L3 kam Lieedtke zu dem Schluss, dass auch mehrere andere Mach -Konzepte verlegt wurden. Durch die Vereinfachung der Mikrokernelkonzepte entwickelte er den ersten L4 -Kernel, der hauptsächlich für hohe Leistung entwickelt wurde. Um jede Leistung zu extrahieren, wurde der gesamte Kernel geschrieben Montagespracheund sein IPC war 20 -mal schneller als Mach.[4] Solche dramatischen Leistungserhöhungen sind ein seltenes Ereignis in Betriebssystemen, und die Arbeit von Lieedtke löste neue L4-Implementierungen aus und Arbeiten an L4-basierten Systemen an einer Reihe von Universitäten und Forschungsinstituten, einschließlich IBM, wo Lieedtke 1996 zu arbeiten begann, Tu Dresden und UNSW. Bei IBM Thomas J. Watson Research Center Lieedtke und seine Kollegen setzten die Forschung zu L4- und Microkernel -basierten Systemen im Allgemeinen fort, insbesondere zum Sägewerk.[5]

L4KA :: Haselnuss

1999 übernahm Lieedtke die Systemarchitekturgruppe am Universität von Karlsruhe, wo er die Forschung zu Mikrokernel -Systemen fortsetzte. Als Beweis für das Konzept, dass ein Hochleistungsmikrokernel auch in einer höheren Sprache konstruiert werden könnte, entwickelte sich die Gruppe L4KA :: Haselnuss, a C ++ Version des Kernels, der weiterlief IA-32- und ARM-basierte Maschinen. Der Aufwand war ein Erfolg, die Leistung war immer noch akzeptabel, und mit seiner Veröffentlichung wurden die reinen Versammlungsversionen der Kerne effektiv abgesetzt.

L4/Fiasko

Parallel zur Entwicklung von L4KA :: Hazelnut begann die Betriebssystemgruppe TUD: OS des Tu Dresden, ihre eigene C ++ - Implementierung der L4 -Kernelschnittstelle mit dem Namen L4/Fiasco zu entwickeln. Im Gegensatz zu L4KA :: Haselnuss, das keine Parallelität im Kernel ermöglicht, und sein Nachfolger L4KA :: Pistazien, der Interrupts im Kernel nur an bestimmten Präsentationspunkten ermöglicht. L4/Fiasko war vollständig präventiv (mit Ausnahme von extrem kurzen atomaren Operationen), um ein niedriges zu erreichen Latenz unterbrechen. Dies wurde als notwendig angesehen, da L4/Fiasko als Grundlage für Tropfen verwendet wird,[6] ein hartes Echtzeit-Computing fähiges Betriebssystem, ebenfalls am Tu Dresden entwickelt. Die Komplexität eines vollständig präventiblen Designs veranlasste jedoch spätere Versionen von Fiasko, zum traditionellen L4 -Ansatz des Ausführens des Kernels mit deaktivierten Interrupts zurückzukehren, mit Ausnahme einer begrenzten Anzahl von Präparationspunkten.

Plattformübergreifend

L4ka :: pistazio

Bis zu Die nächste große Verschiebung der L4-Entwicklung war die Entwicklung einer plattformübergreifenden (plattformunabhängigen) Anwendungsprogrammierschnittstelle (API) Das behielte trotz seiner höheren Portabilität immer noch die Hochleistungseigenschaften. Obwohl die zugrunde liegenden Konzepte des Kernels gleich waren, lieferte die neue API viele signifikante Änderungen im Vergleich zu früheren L4 Blöcke (UTCBs) und virtuelle Register. Nach der Veröffentlichung der neuen L4 -API (Version X.2 a.k.a. Version 4) Anfang 2001 implementierte die Systemarchitekturgruppe der University of Karlsruhe einen neuen Kernel. L4ka :: pistazio, komplett von Grund auf neu, jetzt mit dem Fokus auf hohe Leistung und Portabilität. Es wurde unter dem freigelassen Zwei-Klausel-BSD-Lizenz.[7]

Neuere Fiaskoversionen

Das L4/Fiasco Microkernel wurde im Laufe der Jahre ebenfalls ausführlich verbessert. Es unterstützt jetzt mehrere Hardware -Plattformen von x86 bis AMD64 bis zu mehreren ARM -Plattformen. Insbesondere kann eine Version von Fiasco (Fiasco-UX) als Anwendung auf Benutzerebene unter Linux ausgeführt werden.

L4/Fiasco implementiert mehrere Erweiterungen in die L4v2 -API. Mit Ausnahme von IPC können der Kernel CPU-Ausnahmen an Handler-Anwendungen auf Benutzerebene senden. Mit der Hilfe von Außerirdische FädenEs ist möglich, eine feinkörnige Kontrolle über Systemaufrufe durchzuführen. UTCBs im X.2-Stil wurden hinzugefügt. Außerdem enthält Fiasko Mechanismen zur Kontrolle von Kommunikationsrechten und Ressourcenverwendung auf Kernelebene. Auf Fiasko wird eine Sammlung grundlegender Benutzerebene entwickelt (benannt L4ENV), die unter anderem verwendet werden, um die aktuelle Linux-Version (4.19 ab Mai 2019) zu para-virtuell) (genannt L4Linux).

Universität von New South Wales und Nicta

Die Entwicklung trat auch bei der auf Universität von New South Wales (UNSW), bei dem Entwickler L4 auf mehreren 64-Bit-Plattformen implementierten. Ihre Arbeit führte zu L4/MIPS und L4/Alpha, was dazu führt, dass die ursprüngliche Version von Lieedtke retrospektiv benannt wird L4/x86. Wie die ursprünglichen Kerne von Lieedtke waren die UNSW -Kerne (geschrieben in einer Mischung aus Montage und C) nicht portierbar und wurden von Grund auf neu implementiert. Mit der Veröffentlichung des hoch tragbaren L4KA :: Pistaziens hat die UNSW-Gruppe ihre eigenen Kerne aufgegeben, um hochstimmige Ports von L4KA :: Pistazie zu produzieren, einschließlich der am schnellsten gemeldeten Implementierung von Botschaft (36 Zyklen auf dem Itanium die Architektur).[8] Die Gruppe hat das auch gezeigt Gerätetreiber kann auf Benutzerebene gleich gut wie In-Kernel abschneiden,[9] und entwickelt Wombat, eine hoch tragbare Version von Linux auf l4 läuft weiter x86, ARM, und MIPS Prozessoren. An Xscale Prozessoren, Wombat-Kontext-sankte Kosten sind bis zu 50-mal niedriger als unter nativen Linux.[10]

Später die UNSW -Gruppe in ihrem neuen Zuhause bei Nicta (früher National ICT Australia, Ltd..), Forked L4Ka :: Pistazien in eine neue L4 -Version namens namens Nicta :: L4-eingebettet. Wie der Name schon sagt, war es für die Verwendung im Werbespot eingebettete Systemeund folglich favorisierten die Kompromisse für die Umsetzung eine geringe Speichergröße und eine verringerte Komplexität. Die API wurde geändert, um fast alle Systemanrufe so weit zu kurz zu halten, dass sie keine Präparationspunkte benötigen, um eine hohe Reaktionsfähigkeit in Echtzeit zu gewährleisten.[11]

Kommerzieller Einsatz

Im November 2005, Nicta angekündigt[12] das Qualcomm stellte die L4 -Version von NICTA auf ihrer ein Mobile Station Modem Chipsätze. Dies führte zur Verwendung von L4 in Handy Ab Ende 2006 zum Verkauf angeboten Gernot Heiser Ausgesponnen eine Firma namens namens Offene Kernellabors (OK LABS), um kommerzielle L4 -Benutzer zu unterstützen und L4 für den kommerziellen Gebrauch unter dem Markennamen weiter zu entwickeln OKL4in enger Zusammenarbeit mit Nicta. OKL4 Version 2.1, veröffentlicht im April 2008, war der erste allgemein erhältlich Version von L4, die vorgestellt wurde Fähigkeitsbasierte Sicherheit. OKL4 3.0, veröffentlicht im Oktober 2008, war die letzte Open-Source-Version von OKL4. Neuere Versionen sind geschlossen und basieren auf einem Umschreiben, um eine native Hypervisor -Variante mit dem Namen OKL4 Microvisor zu unterstützen. Ok Labore verteilten auch ein paravirtualisiertes Linux mit dem Namen OK: Linux, einen Nachkomme von Wombat und paravirtualisierte Versionen von Symbianos und Android. Ok Labore erworben auch die Rechte an Sel4 von nicta.

OKL4 -Sendungen überstieg Anfang 2012 1,5 Milliarden.[2] Meistens auf qualcomm drahtlosen Modemchips. Andere Bereitstellungen umfassen Kfz -Infotainment Systeme.[13]

Apfel eine Serie Prozessoren beginnen mit dem A7 eine sichere Enklave enthalten Coprozessor Ausführen eines L4 -Betriebssystems[14] basierend auf dem von L4 eingebetteten Kernel entwickelt bei Nicta in 2006.[15]Dies impliziert, dass L4 jetzt auf allen iOS -Geräten versendet wird, deren Gesamtversand für das Jahr 2015 auf 310 Millionen geschätzt wird.[16]

Hohe Gewissheit: SEL4

Im Jahr 2006 die Nicta Gruppe begann ein From-Scratch-Design von a Mikrokernel der dritten Generation, benannt SEL4, mit dem Ziel, eine Grundlage für hochsichere und zuverlässige Systeme bereitzustellen, geeignet für die Befriedigung von Sicherheitsanforderungen wie denen von Gemeinsame Kriterien und darüber hinaus. Von Anfang an zielte die Entwicklung darauf ab formelle Überprüfung des Kernels. Um die manchmal widersprüchlichen Anforderungen an Leistung und Überprüfung zu erfüllen, verwendete das Team a Middle-Out Softwareprozess aus einer ausführbaren Spezifikation, die in geschrieben wurde Haskell.[17] Sel4 verwendet Fähigkeitsbasierte Sicherheit Zugriffskontrolle, um formelle Begründungen zur Objektzugriffsfähigkeit zu ermöglichen.

A formeller Beweis der funktionalen Korrektheit wurde 2009 abgeschlossen.[18] Der Beweis bietet eine Garantie dafür, dass die Implementierung des Kernels gegen seine Spezifikation korrekt ist, und impliziert, dass sie frei von Implementierungsfehler wie Deadlocks ist. Lebensunterhalt, Pufferüberläufe, arithmetische Ausnahmen oder Verwendung von nicht initialisierten Variablen. Es wird behauptet, dass Sel4 der erste allgemeine Operationssystem-Kernel ist, der überprüft wurde.[18]

SEL4 verfolgt einen neuartigen Ansatz zum Kernel Resource Management.[19] Exportieren des Managements von Kernel -Ressourcen auf Benutzerebene und unterwirft sie demselben Fähigkeit basiert Zugriffskontrolle als Benutzerressourcen. Dieses Modell, das auch übernommen wurde von Barrelfishvereinfacht das Denken über Isolationseigenschaften und war ein Enabler für spätere Beweise, dass SEL4 die Kernsicherheitseigenschaften von Integrität und Vertraulichkeit erzwingt.[20] Das NICTA -Team erwies sich auch als Korrektheit der Übersetzung aus der Programmiersprache C ausführbare Datei Maschinensprachedas Compiler aus dem Vertrauenswürdige Computerbasis von sel4.[21] Dies impliziert, dass die auf hohen Sicherheitsbeweise für den Kernel ausführbaren Kernel-Datei. SEL4 ist auch der erste veröffentlichte Protected-Modus-OS-Kernel mit einem vollständigen und Ton Worst-Case-Ausführungszeit (WCET) Analyse, eine Voraussetzung für ihre Verwendung in hart Echtzeit-Computing.[20]

Am 29. Juli 2014, Nicta und General Dynamics C4 -Systeme kündigte an, dass SEL4 mit End -to -End -Proofs nun veröffentlicht wurde Open-Source-Lizenzen.[22] Der Kernel Quellcode und Beweise sind lizenziert unter GNU Allgemeine öffentliche Lizenz Version 2 (GPLV2) und die meisten Bibliotheken und Werkzeug sind unter dem BSD 2-Klausel. Im April 2020 wurde bekannt gegeben, dass die SEL4 -Stiftung unter dem Dach des Linux Foundation Entwicklung und Einsatz von SEL4 zu beschleunigen.[23]

Die Forscher geben an, dass die Kosten für die formelle Softwareverifizierung niedriger sind als die Kosten für die technische traditionelle "Hochversicherung" -Software, obwohl sie viel zuverlässigere Ergebnisse liefern.[24] Insbesondere die Kosten von einem Codezeile während der Entwicklung von SEL4 wurde um etwa umgeschätzt US $ 400, verglichen mit US $ 1.000 Für traditionelle Hochversicherungssysteme.[25]

Unter der Verteidigung Advanced Research Projects Agency (DARPA) HACMS-Programm (High-Assurance Cyber ​​Military Systems), NICTA zusammen mit Projektpartnern Rockwell Collins, Galois Inc, die Universität von Minnesota und Boeing entwickelte eine Hochsicherungsdrohne mit SEL4 zusammen mit anderen Assurance-Tools und Software mit geplanter Technologieübertragung auf das optional pilotierte autonome Boeing AH-6 Unbemannter kleiner Vogelhubschrauber, der von Boeing entwickelt wird. Die endgültige Demonstration der HACMS -Technologie fand im April 2017 in Sterling, VA, statt.[26] DARPA finanzierte auch mehrere Innovative Forschung kleiner Unternehmen (SBIR) Verträge im Zusammenhang mit SEL4 im Rahmen eines von Dr. gestarteten Programms John Launchbury. Zu den kleinen Unternehmen, die einen SEL4-bezogenen SBIR erhielten, gehörten: Dornerworks, TechShot, Wearable Inc, Echtzeit Innovationen und kritische Technologien.[27]

Andere Forschung und Entwicklung

Osker, ein Betriebssystem geschrieben in Haskellzielte auf die L4 -Spezifikation ab; Obwohl sich dieses Projekt hauptsächlich auf die Verwendung von a konzentrierte Funktionelle Programmierung Sprache für die OS -Entwicklung, nicht zur Mikrokernelforschung.[28]

Codezero[29] ist ein L4 -Mikrokernel für eingebettete Systeme mit Schwerpunkt auf Virtualisierung und Implementierung nativer OS -Dienste. Da ist ein Gpl-lizenzierte Version,[30] und eine Version, die von B Labs Ltd., erworben wurde, von B Labs Ltd. erworben wurde Nvidia, als geschlossene Quelle und 2010 gegabelt.[31][32]

F9 Microkernel,[33] Eine BSD-lizenzierte L4-Implementierung ist bestrebt Arm Cortex-M Prozessoren für tief eingebettete Geräte mit Speicherschutz.

Die Nova OS -Virtualisierungsarchitektur[34] ist ein Forschungsprojekt, das sich auf die Konstruktion einer sicheren und effizienten Virtualisierungsumgebung konzentriert[35][36] mit einer kleinen vertrauenswürdigen Computerbasis. Nova besteht aus einem Mikrohypervisor, einer Benutzerebene Hypervisor (virtuelle Maschine Überwachung) und eine nicht privilegierte komponentierte Multi-Server-Benutzerumgebung, die auf IT namens NUL ausgeführt wird. Nova läuft auf ARMV8-A- und X86-basierten Multi-Core-Systemen.

Wrmos[37] ist ein Echtzeit-Betriebssystem Basierend auf L4 Microkernel. Es verfügt über eigene Implementierungen von Kernel, Standardbibliotheken und Netzwerkstapel, die Architekturen von Arm, SPARC, X86 und X86-64 unterstützt. Es gibt den paravirtualisierten Linux -Kernel (W4linux[38]) Arbeiten an WRMOs.

Siehe auch

Verweise

  1. ^ "Hypervisor -Produkte: General Dynamics Mission Systems". General Dynamics Mission Systems. Archiviert Aus dem Original am 15. November 2017. Abgerufen 26. April 2018.
  2. ^ a b "Open Kernel Labs -Software übertrifft den Meilenstein von 1,5 Milliarden Sendungen für mobile Geräte" (Pressemitteilung). Offene Kernellabors. 19. Januar 2012. archiviert von das Original am 11. Februar 2012.
  3. ^ a b Lieedtke, Jungen (Dezember 1995). "Auf µ-Kernel-Konstruktion". Proceedings 15. ACM -Symposium für Betriebssystemprinzipien (SOSP). S. 237–250. Archiviert Aus dem Original am 25. Oktober 2015.
  4. ^ Lieedtke, Jungen (Dezember 1993). "IPC durch Kernel -Design verbessern". 14. ACM -Symposium für Betriebssystemprinzipien. Asheville, NC, USA. S. 175–188.
  5. ^ Gefflaut, Alain; Jaeger, Trent; Park, Yoonho; Lieedtke, Jungen; Elphinstone, Kevin; Uhlig, Volkmar; Tidswell, Jonathon; Deller, Luke; Reuther, Lars (2000). "Der Sägewerk Multiserver -Ansatz". ACM Sigops European Workshop. Kolding, Dänemark. S. 109–114.
  6. ^ "Drops - Übersicht". Dresden University of Technology. Archiviert Aus dem Original am 7. August 2011. Abgerufen 10. August 2011.
  7. ^ l4ka.org: l4ka :: pistazien microkernel Zitat: "... Die Vielfalt der unterstützten Architekturen macht L4KA :: Pistazien zu einer idealen Forschungs- und Entwicklungsplattform für eine Vielzahl von Systemen ..."
  8. ^ Gray, Charles; Chapman, Matthew; Chubb, Peter; Mosberger-Tang, David; Heiser, Gernot (April 2005). "Itanium: Die Geschichte eines Systemimplementers". Usenix jährliche technische Konferenz. Annaheim, CA, USA. S. 264–278. Archiviert Aus dem Original am 17. Februar 2007.
  9. ^ Leslie, Ben; Chubb, Peter; Fitzroy-Dale, Nicholas; Götz, Stefan; Gray, Charles; Macpherson, Luke; Potts, Daniel; Shen, Yueting; Elphinstone, Kevin; Heiser, Gernot (September 2005). "Gerätetreiber auf Benutzerebene: Leistung erzielt". Zeitschrift für Informatik und Technologie. 20 (5): 654–664. Citeseerx 10.1.1.59.6766. doi:10.1007/s11390-005-0654-4. S2CID 1121537.
  10. ^ Van Schaik, Carl; Heiser, Gernot (Januar 2007). "Hochleistungsmikrokernel und Virtualisierung auf Arm und segmentierte Architekturen". 1. Internationaler Workshop über Mikrokernel für eingebettete Systeme. Sydney, Australien: Nicta. S. 11–21. Archiviert Aus dem Original am 1. März 2015. Abgerufen 25. Oktober 2015.
  11. ^ Ruocco, Sergio (Oktober 2008). "Eine Echtzeit-Programmierer-Tour durch allgemeine L4-Microkernel". Eurasip Journal über eingebettete Systeme. 2008: 1–14. doi:10.1155/2008/234710. S2CID 7430332.
  12. ^ "Nicta L4 Microkernel, das in ausgewählten Qualcomm -Chipset -Lösungen verwendet wird" (Pressemitteilung). Nicta. 24. November 2005. archiviert von das Original am 25. August 2006.
  13. ^ "Open Kernel Labs Automotive Virtualisierung von Bosch für Infotainment -Systeme ausgewählt" (Pressemitteilung). Offene Kernellabors. 27. März 2012. archiviert von das Original am 2. Juli 2012.
  14. ^ "iOS Security, iOS 12.3" (PDF). Apple Inc. Mai 2019.
  15. ^ Mandt, Tarjei; Solnik, Mathew; Wang, David (31. Juli 2016). "Entmystifizierung des sicheren Enklavenprozessors" (PDF). Blackhat USA. Las Vegas, Nevada, USA. Archiviert (PDF) Aus dem Original am 21. Oktober 2016.
  16. ^ Elmer-Dewitt, Philip (28. Oktober 2014). "Prognose: Apple wird 2015 310 Millionen iOS -Geräte versenden". Reichtum. Archiviert Aus dem Original am 27. September 2015. Abgerufen 25. Oktober 2015.
  17. ^ Derrin, Philip; Elphinstone, Kevin; Klein, Gerwin; Schwanz, David; Chakravarty, Manuel M. T. (September 2006). "Ausführen des Handbuchs: Ein Ansatz zur Entwicklung von Mikrokernel mit hoher Versicherung". ACM Sigplan Haskell Workshop. Portland, Oregon. S. 60–71.
  18. ^ a b Klein, Gerwin; Elphinstone, Kevin; Heiser, Gernot; Andronick, Juni; Schwanz, David; Derrin, Philip; Elkaduwe, Dhammika; Engelhardt, Kai; Kolanski, Rafal; Norrish, Michael; Sewell, Thomas; Tuch, Harvey; Winwood, Simon (Oktober 2009). "SEL4: Formale Überprüfung eines OS -Kernels" (PDF). 22. ACM -Symposium für Betriebssystemprinzipien. Big Sky, MT, USA. Archiviert (PDF) Aus dem Original am 28. Juli 2011.
  19. ^ Elkaduwe, Dhammika; Derrin, Philip; Elphinstone, Kevin (April 2008). Kerneldesign für die Isolation und Gewissheit des physischen Gedächtnisses. 1. Workshop zur Isolation und Integration in eingebettete Systeme. Glasgow, Großbritannien. doi:10.1145/1435458. Abgerufen 22. Februar 2020.
  20. ^ a b Klein, Gerwin; Andronick, Juni; Elphinstone, Kevin; Murray, Toby; Sewell, Thomas; Kolanski, Rafal; Heiser, Gernot (Februar 2014). "Umfassende formale Überprüfung eines OS -Mikrokernel". ACM -Transaktionen auf Computersystemen. 32 (1): 2: 1–2: 70. Citeseerx 10.1.1.431.9140. doi:10.1145/2560537. S2CID 4474342.
  21. ^ Sewell, Thomas; Myreen, Magnus; Klein, Gerwin (Juni 2013). "Übersetzungsvalidierung für einen verifizierten OS -Kernel". ACM -Sigplan -Konferenz zum Design und Umsetzung von Programmiersprache. Seattle, WA, USA. doi:10.1145/2491956.2462183.
  22. ^ "Sicheres Betriebssystem, das von Nicta entwickelt wurde, geht Open Source" (Pressemitteilung). Nicta. 29. Juli 2014. Archiviert Aus dem Original am 15. März 2016.
  23. ^ "Sicherheit wird von Linux Foundation unterstützt" (Pressemitteilung). Linux Foundation. 7. April 2020. Archiviert Aus dem Original am 15. März 2016.
  24. ^ Klein, Gerwin; Andronick, Juni; Elphinstone, Kevin; Murray, Toby; Sewell, Thomas; Kolanski, Rafal; Heiser, Gernot (2014). "Umfassende formale Überprüfung eines OS -Mikrokernel" (PDF). ACM -Transaktionen auf Computersystemen. 32: 64. Citeseerx 10.1.1.431.9140. doi:10.1145/2560537. S2CID 4474342. Archiviert (PDF) Aus dem Original am 3. August 2014.
  25. ^ Heiser, Gernot (16. Januar 2015). SEL4 ist kostenlos: Was bedeutet das für Sie?. Auckland, Neuseeland: Linux.Conf.au.
  26. ^ "DARPA wählt Rockwell Collins aus, um Cybersicherheitstechnologie auf neue Plattformen anzuwenden" (Pressemitteilung). Rockwell Collins. 24. April 2017. Archiviert vom Original am 11. Mai 2017.
  27. ^ "DARPA -Agentur -Sponsor Dr. John Launchbury". Sbirsource. 2017. Archiviert vom Original am 29. September 2017. Abgerufen 16. Mai 2017.
  28. ^ Hallgren, T.; Jones, M.P.; Leslie, R.; Tolmach, A. (2005). "Ein prinzipieller Ansatz zur Betriebssystemkonstruktion in Haskell" (PDF). Verfahren der zehnten ACM -Sigplan -Internationalen Konferenz für funktionale Programmierung. 40 (9): 116–128. doi:10.1145/1090189.1086380. ISSN 0362-1340. Archiviert (PDF) Aus dem Original am 15. Juni 2010. Abgerufen 24. Juni 2010.
  29. ^ "Ankündigen: Einführung von Codezero". Dresden University of Technology.
  30. ^ "JServ/Codezero: Codezero Microkernel". GitHub. Archiviert Aus dem Original am 15. August 2015. Abgerufen 20. Oktober 2020.
  31. ^ "Code Null: eingebetteter Hypervisor und Betriebssystem". Archiviert von das Original am 11. Januar 2016. Abgerufen 25. Januar 2016.
  32. ^ "Archivierte Kopie". Archiviert von das Original am 2. Februar 2014. Abgerufen 2. Februar 2014.{{}}: CS1 Wartung: Archiviertes Kopie als Titel (Link)
  33. ^ "F9 Microkernel". GitHub. Abgerufen 20. Oktober 2020.
  34. ^ "Nova Microhypervisor -Website". Abgerufen 9. Januar 2021.
  35. ^ Steinberg, Udo; Kauer, Bernhard (April 2010). "Nova: Eine Mikrohypervisor-basierte sichere Virtualisierungsarchitektur". Eurosys '10: Verfahren der 5. Europäischen Konferenz über Computersysteme. Paris, Frankreich.
  36. ^ Steinberg, Udo; Kauer, Bernhard (April 2010). "Auf dem Weg zu einer skalierbaren Multiprozessor-Benutzerumgebung auf Benutzerebene". IIDS'10: Workshop zur Isolation und Integration für zuverlässige Systeme. Paris, Frankreich.
  37. ^ "Wrmos". Abgerufen 20. Oktober 2020.
  38. ^ "W4LINUX ist paravirtualisierter Linux -Kernel, der an WRMos arbeitet". Abgerufen 20. Oktober 2020.

Weitere Lektüre

Externe Links