Einführung in den seL4-Mikrokernel [PDF]

 (sel4.systems)
1 Punkte von GN⁺ 2025-03-24 | 1 Kommentare | Auf WhatsApp teilen
  • seL4 ist ein OS-Mikrokernel für Embedded- und cyber-physische Systeme, bei denen Sicherheit und Safety entscheidend sind. Er isoliert und multiplexed Hardware-Ressourcen, ist aber kein vollständiges Allzweck-OS.
  • Durch die Reduzierung des Kernel-Mode-Codes auf etwa 10 kSLOC verkleinert seL4 die TCB und die Angriffsfläche; OS-Dienste wie Dateisysteme, Netzwerke und Treiber werden in den User Mode verlagert.
  • seL4 ist der weltweit erste OS-Kernel mit formaler Verifikation auf Code-Ebene; in korrekt konfigurierten Systemen garantiert der Kernel sogar Sicherheitseigenschaften wie Vertraulichkeit, Integrität und Verfügbarkeit.
  • Durch die Kombination von capability-basierter Zugriffskontrolle, WCET-Analyse, Unterstützung für Mixed-Criticality-Echtzeitsysteme und Hypervisor-Funktionen adressiert seL4 zugleich feingranulare Isolation und Echtzeitfähigkeit.
  • Die seL4-API ist sehr low-level, sodass komplexe Systeme schwer direkt darauf aufzubauen sind; wenn eine statische Architektur passt, ist der Einsatz eines Frameworks wie Microkit der pragmatische Weg.

Der Zuständigkeitsbereich von seL4

  • seL4 ist ein Mikrokernel, also der Low-Level-Kern eines Betriebssystems.
    • Ein OS kontrolliert Hardware und Ressourcen im Kernel Mode, einem Ausführungsmodus des Prozessors mit höheren Privilegien.
    • Anwendungen laufen im User Mode und greifen nur auf die vom OS erlaubte Weise auf Hardware zu.
  • Ein Mikrokernel ist der Kern eines OS, bei dem der mit hohen Privilegien ausgeführte Code minimiert ist.
    • seL4 gehört zur L4-Familie von Mikrokerneln, deren Geschichte bis in die Mitte der 1990er-Jahre zurückreicht.
    • seL4 hat nichts mit seLinux zu tun.
  • seL4 ist kein vollständiges OS, sondern ein Low-Level-Kernel, der Hardware-Ressourcen sicher multiplexed und isoliert.
    • Allgemeine OS-Dienste wie Dateisysteme, Netzwerk-Stacks und Gerätetreiber befinden sich nicht im Kernel.
    • Solche Dienste müssen als Programme im User Mode bereitgestellt werden.

Mikrokernel-Architektur und Verringerung der Angriffsfläche

  • Monolithische Kernel wie Linux stellen OS-Dienste wie Dateispeicherung und Networking als Kernel-Mode-Code bereit.
    • Kernel-Mode-Code hat uneingeschränkten Zugriff auf Systemressourcen; wenn Bugs zu Privilege Escalation oder zur Ausführung beliebigen Codes führen, kann das gesamte System kompromittiert werden.
    • Der Linux-Kernel umfasst etwa 20 MSLOC, und es wird geschätzt, dass er Zehntausende Bugs enthalten könnte.
  • Ein gut entworfener Mikrokernel wie seL4 reduziert den Kernel-Mode-Code auf etwa 10 kSLOC.
    • Das ist um mehrere Größenordnungen kleiner als der Linux-Kernel.
    • Mit der kleineren TCB schrumpft auch die Angriffsfläche.
  • Die meisten OS-Dienste werden aus dem Kernel herausgelöst, und der Mikrokernel verhält sich wie ein dünner Wrapper um die Hardware.
    • Die zentralen bereitgestellten Funktionen sind Isolation zwischen Programmen und ein sicherer Aufrufmechanismus.
    • Dienste werden zu User-Mode-Programmen, die nicht im Kernel, sondern in separaten Sandboxes laufen.
  • In einer Studie, die schwere bekannte Linux-Kompromittierungen analysierte, konnte ein Mikrokernel-Design 29 % vollständig eliminieren und weitere 55 % so weit abschwächen, dass sie nicht mehr als schwerwiegend eingestuft würden.

PPC, Capabilities und feingranulare Rechtekontrolle

  • seL4 stellt einen Mechanismus für Protected Procedure Calls (PPC) bereit.
    • Aus historischen Gründen ist der Begriff IPC erhalten geblieben, doch die Bezeichnung IPC kann missverstanden werden und zu schlechtem Design führen.
    • PPC erlaubt es einem Programm, sicher eine Funktion eines Programms in einer anderen Sandbox aufzurufen.
  • Der Mikrokernel übergibt bei PPC Eingaben und Ausgaben und setzt Interfaces durch.
    • Remote-Funktionen können nur über exportierte Einstiegspunkte aufgerufen werden.
    • Nur explizit autorisierte Clients, die die passende Capability erhalten haben, können sie aufrufen.
  • Eine Capability ist ein Zugriffstoken, das den Zugriff auf eine bestimmte Ressource des Systems ermöglicht.
    • Sie steuert sehr feingranular, welche Entität auf welche Ressource zugreifen darf.
    • Sie unterstützt das Least-Privilege-Prinzip beziehungsweise das Principle of Least Authority (POLA).
  • Mit den Zugriffskontrollmodellen verbreiteter Systeme wie Linux oder Windows lässt sich dieses Maß an Least Privilege nicht erreichen.
  • seL4 gilt als weltweit einziges OS, das zugleich capability-basiert und formal verifiziert ist; diese Kombination untermauert die vertretbare Behauptung, es sei das sicherste OS der Welt.

Formale Verifikation und Sicherheitsgarantien

  • seL4 bietet einen formalen, mathematischen und maschinengeprüften Beweis für die Korrektheit der Implementierung.
    • Dieser Beweis bedeutet, dass der Kernel in einem sehr starken Sinn „bugfrei“ in Bezug auf seine Spezifikation ist.
    • seL4 war der weltweit erste OS-Kernel mit einem solchen Beweis auf Code-Ebene.
  • Neben der Implementierungskorrektheit bietet seL4 zusätzliche Beweise für die Durchsetzung von Sicherheit.
    • In einem korrekt konfigurierten seL4-basierten System garantiert der Kernel Vertraulichkeit, Integrität und Verfügbarkeit.
  • Die Verifikationskette ist ein zentrales Alleinstellungsmerkmal von seL4.
    • Damit der Kernel in sicherheits- und safety-kritischen Systemen als Vertrauensbasis dienen kann, braucht es starke Zusicherungen für Implementierung und Sicherheitseigenschaften.

Echtzeitfähigkeit und Mixed-Criticality-Systeme

  • seL4 ist ein OS-Kernel, der einer vollständigen und soliden Analyse der Worst-Case Execution Time (WCET) unterzogen wurde.
    • Wenn der Kernel entsprechend konfiguriert ist, sind alle Kernel-Operationen zeitlich begrenzt.
    • Diese Grenzen sind zudem bekannt.
  • Diese Eigenschaft ist eine Voraussetzung für den Aufbau von Hard-Real-Time-Systemen.
    • Sie richten sich an Systeme, bei denen es katastrophale Folgen haben kann, wenn sie nicht innerhalb strikt begrenzter Zeit auf Ereignisse reagieren.
  • seL4 unterstützt auch Mixed-Criticality-Echtzeitsysteme (MCS).
    • Es zielt auf Umgebungen, in denen die Timing-Eigenschaften kritischer Aktivitäten garantiert werden müssen, obwohl weniger vertrauenswürdiger Code auf derselben Plattform mitläuft.
    • Anders als die strikte und unflexible Zeit- und Raum-Partitionierung bestehender MCS-OS bietet seL4 ein flexibles Modell, das die Ressourcenauslastung erhält.

seL4 als Hypervisor

  • seL4 ist sowohl Mikrokernel als auch Hypervisor.
    • Auf seL4 lassen sich virtuelle Maschinen ausführen.
    • In virtuellen Maschinen können allgemeine Gastbetriebssysteme wie Linux laufen.
  • Gäste und Anwendungen können entsprechend den von seL4 erzwungenen Kommunikationskanälen miteinander kommunizieren.
    • Auch die Kommunikation mit nativen Anwendungen ist möglich.
  • Linux-VMs können als Mittel zur Bereitstellung von Systemdiensten genutzt werden.
    • In einer Beispielkonfiguration werden Dienste wie Networking und Storage von mehreren Linux-Instanzen bezogen, die in separaten VMs laufen.

Systeme auf seL4 bauen

  • Die seL4-API ist selbst im Vergleich zu anderen Mikrokerneln sehr low-level.
    • Sie stellt nur die minimalen Abstraktionen bereit, die für das sichere Management von Hardware nötig sind.
    • seL4 wird mit der „Assemblersprache des Betriebssystems“ verglichen.
  • Komplexe Systeme direkt auf seL4 aufzubauen, ist kein geeigneter Ansatz.
    • Höherstufige Frameworks sollten es ermöglichen, sich auf den Implementierungscode der Dienste zu konzentrieren, und Hardware-Komplexität sowie Systemintegration automatisieren.
  • Für seL4 gibt es drei wichtige Open-Source-Komponenten-Frameworks.
    • Microkit: vereinfacht die seL4-API mit wenigen Abstraktionen rund um Protection Domains und bietet ein SDK, das separat kompilierte Module und das Kernel-Binary zu einem bootfähigen Image integriert.
    • CAmkES: der Vorgänger von Microkit und ein Komponenten-Framework für Systeme mit statischer Architektur; da es jedoch kein SDK bietet, ist der Build-Prozess umständlicher und der Overhead höher.
    • Genode: unterstützt mehrere Mikrokernel und bietet viele Dienste und Treiber für x86-Plattformen; es erzwingt keine statische Architektur, kann aber nicht alle Sicherheits- und Safety-Funktionen von seL4 nutzen und bietet keine Garantie-Story.
  • Solange eine statische Systemarchitektur zu den Anforderungen passt, wird Microkit für den Aufbau seL4-basierter Systeme empfohlen.
    • Eine statische Architektur ist ein Modell, bei dem die Menge der Module und die Kommunikationsstruktur zum Zeitpunkt der Systemkonfiguration definiert werden.
    • Dieses Modell gilt als passend für die Anforderungen der meisten Embedded-Systeme, einschließlich komplexer cyber-physischer Systeme wie Autos und Flugzeuge.

Verwandte Beiträge

1 Kommentare

 
GN⁺ 2025-03-24
Hacker-News-Meinungen

  • seL4 selbst ist ein altes Thema, aber ich frage mich, ob über den Mikrokernel hinaus neue formal verifizierte Schichten oder Komponenten hinzugekommen sind.
    Außerdem scheinen manche Menschen beim Wort „Beweis“ emotional überlastet zu sein und gedanklich abzuschalten. Formale Verifikation ist weder ein Allheilmittel, das das unendliche Problem sicherer IT löst, noch eine Methode, um vollkommen fehlerfreie Software zu erzeugen.
    Soweit ich es verstehe, handelt es sich um den Nachweis, dass unter bestimmten Bedingungen bestimmte Anforderungen erfüllt werden; diese Anforderungen und Bedingungen können ziemlich eng gefasst sein, und über Funktionen und Bedingungen außerhalb der Spezifikation wird keine Aussage getroffen. Ich frage mich, ob das ungefähr stimmt.
    Mich interessiert auch, was Sicherheitsexperten in der Praxis erwarten, wenn sie „formal verifizierte Software“ sehen. Welche Spezifikation seL4 erfüllt, scheint mir hier die zentrale Information zu sein.

    • Auch wenn formal verifiziert wurde, dass mehrere Fehlerklassen nicht vorhanden sind, war seL4 nicht immun gegen Speicherbeschädigungsfehler. Vor einigen Jahren wurde ein solcher Fehler gefunden; der Commit, der ihn behob, und der PR, der den seL4-Beweis anpasste, sind öffentlich.
      https://github.com/seL4/seL4/pull/243
      https://github.com/seL4/l4v/pull/453
      Im Issue-Tracker gibt es auch mehrere speicherbezogene Bugs.
      https://github.com/seL4/seL4/issues?q=is%3Aissue%20label%3Ab...
      Interessanterweise trägt der PR, der „register clobbering“ im Speicher behob, kein bug-Label und taucht daher nicht auf, wenn man nach „bug“ filtert. Früher dachte ich, seL4 sei dank der Beweise gegen solche Probleme immun; danach kam ich zu der Ansicht, dass die Beweise nicht so umfassend sind, wie die Community zu glauben begann. Trotzdem ist seL4 nach wie vor eine sehr beeindruckende Software.
      Um die Frage zu beantworten: Die Spezifikation, die seL4 erfüllt, ist auf GitHub veröffentlicht.
      https://github.com/seL4/l4v
    • Formal verifizierte Schichten oder Komponenten werden laufend hinzugefügt. Zuletzt kamen Unterstützung für neue Architekturen wie RISC-V, Mixed-Criticality-Scheduling, Microkit und das Device Driver Framework hinzu.
      Mixed-Criticality-Scheduling bietet capability-basierten Zugriff auf CPU-Zeit, Begrenzungen für die Ausführungszeit von Threads, garantierte Priorität und Ressourcenzugriffe für hochkritische Tasks sowie „passive servers“, die mit vom Aufrufer gespendeter Scheduling-Zeit laufen.
      Microkit ist eine verifizierte Abstraktionsschicht, die den Bau realer Systeme auf seL4 deutlich erleichtert; das Device Driver Framework umfasst Gerätetreiber-Templates, Control-/Data-Plane-Implementierungen sowie Werkzeuge zum Schreiben von Treibern und zur Gerätevirtualisierung für Hochleistungs-I/O auf seL4.
      Formale Verifikation kann garantieren, dass bestimmte Anforderungen unter bestimmten Bedingungen gelten. Im Allgemeinen stimmt es, dass solche Anforderungen und Bedingungen eng sein können; seL4 selbst verfügt jedoch über viele Beweise, die ein breites Spektrum von Eigenschaften abdecken, die man von einem Kernel erwarten würde, und diese Garantien gelten auch unter sehr schwachen Annahmen. Nicht einmal die Korrektheit des C-Compilers wird vorausgesetzt: Es gibt ein separates Werkzeug, das den Compiler-Output betrachtet und beweist, dass das kompilierte Binary gemäß der geforderten C-Semantik funktioniert.
      Zu den Anforderungen, die seL4 erfüllt, gehört, dass der Binärcode des seL4-Kernels exakt das in der abstrakten Spezifikation beschriebene Verhalten implementiert und nichts darüber hinaus. Es gibt keine Buffer Overflows, Speicherlecks, Pointer-Fehler, Null-Pointer-Dereferenzierungen, undefiniertes Verhalten im C-Code oder Kernel-Beendigungen außer über die in der Spezifikation ausdrücklich aufgeführten Wege.
      Die Spezifikation und das seL4-Binary erfüllen außerdem Sicherheitseigenschaften für Integrität und Vertraulichkeit. Integrität bedeutet, dass ein Prozess keinerlei Möglichkeit hat, Daten zu verändern, für die er keine ausdrückliche Berechtigung besitzt; Vertraulichkeit bedeutet, dass er nicht autorisierte Daten auf keinerlei Weise lesen kann. Es wird sogar gezeigt, dass Daten nicht indirekt über bestimmte Seitenkanäle erschlossen werden können. Neben Sicherheit werden auch Garantien für erwartete Worst-Case-Ausführungszeiten und Scheduling-Eigenschaften erfüllt.
    • Die seL4-Entwickler leiden seit Jahren unter Finanzierungsproblemen. Ein Großteil der Arbeit war DARPA-Forschung für ferngesteuerte Drohnen, und das US-Militär möchte unbedingt Drohnen, die nicht gehackt werden können.
      Die aktuelle Arbeit zielt mit LionsOS auf eine breitere Einführung: https://lionsos.org/
    • Zum Beispiel gibt es keine Buffer Overflows, Null-Pointer-Ausnahmen, Use-after-free usw. Auf ARM und RISCV64 wurde funktionale Korrektheit für das Binary bewiesen, sodass man nicht einmal dem C-Compiler vertrauen muss. Neben funktionaler Korrektheit gibt es noch weitere Beweise.
      https://docs.sel4.systems/projects/sel4/frequently-asked-que...
    • https://github.com/auxoncorp/ferros
      Es nutzt viel Typ-Level-Programmierung, um Ressourcen, Hardwarezugriff und Capabilities zur Compile-Zeit zu verfolgen. Probleme erst zur Laufzeit zu finden und zu debuggen ist so furchtbar, dass dies ein Versuch ist, einen Teil der zugrunde liegenden Kernel-Garantien in Richtung Compiler zu verlagern.

  • Ich mag Mikrokernel-Hosts, auf denen monolithische Gast-Kernel laufen; daher betreiben unsere Server seL4 als Sicherheitsschicht und Backup für FreeBSD-VMs und nutzen darin Jails für renderfarm, BEAM-Cluster und Jenkins.
    Schade ist, dass es keinen ARM-Port für DragonflyBSDs Threading und den Kernel innerhalb des Prozesses gibt, also für ein hybrides Kernel-Design. Der Traum wäre, OpenMoonRay auf einem 128-Core Ampere Altra effizienter laufen zu lassen.

    • Ich würde gern genauer wissen, wie seL4 auf dem Server eingesetzt wird. Und ob es sich dabei um kommerzielle Produktionsserver handelt.
    • Diese Konfiguration wäre als längerer Beitrag wahrscheinlich ziemlich interessant zu lesen.

  • Inzwischen scheint die Debatte für oder gegen Microkernel selbst nicht mehr besonders bedeutend zu sein. Der einzige Weg, schnell, effizient und sicher auf privilegierte Dienste zuzugreifen, sind Hardware-Gegenmaßnahmen; dem, was Software leisten kann, sind Grenzen gesetzt.
    Das ist ähnlich wie der Unterschied zwischen 80286 und 80386. Letzterer fügte echte Hardware-Unterstützung für Multitasking hinzu, die Ersterer nicht hatte. Seitdem sind immer mehr Schutzmechanismen auf Hardware-Ebene hinzugekommen, etwa solche, die Hypervisoren ermöglicht haben.
    Insbesondere Apple baut in seine SoCs viele Funktionen ein, die Kernel, Treiber und Komponenten auf Chip-Ebene schützen und bei laufenden Threads sowie bei der Nutzung von Pointern Berechtigungen erzwingen. https://support.apple.com/guide/security/operating-system-in...
    Das heißt nicht, dass ein OS nicht kompromittiert werden kann, aber es ist deutlich wirksamer als eine Strategie, die Berechtigungen ausschließlich per Software verwaltet. Wenn man solche Funktionen oder Ähnliches nutzt, scheint die Kernel-Architektur nicht mehr so wichtig zu sein; ich frage mich, ob ich da falschliege.

    • Du liegst falsch. Im Bereich der OS-Forschung gibt es noch viel zu tun, und für neue Hardware braucht es Software-Schnittstellen und APIs.
      Auch von stärker komponierbaren Mikro-/Hybrid-Systemen lässt sich viel lernen. Plan 9 ist zum Beispiel ein hervorragendes Hybrid-System, das alle Objekte des Systems über ein einziges Protokoll, 9P, im User Space bereitstellt. Hybrid ist es, weil Teile wie IP oder TLS im Kernel liegen, um System-Call-Overhead zu vermeiden.
      Ein weiteres interessantes Design ist, dass Treiber im Kernel meist nur minimale 9P-Schnittstellen zur Hardware-Logik sind. Dadurch werden Maschinenobjekte wie Pointer oder Records zu durchsuchbaren Dateien, diese Dateien lassen sich mit Standard-Unix-Rechten schützen, und Komponenten können leicht über das Netzwerk auf mehrere Maschinen verteilt werden. Dadurch kann Treiberlogik sicher in User-Space-Programme verschoben werden.
      9P ist gegenüber Netzwerk und Architektur transparent, sodass Maschinen mit Arm, x86, MIPS usw. direkt zusammenarbeiten können. Wenn man von Plan 9 zu Linux/Unix oder Windows zurückgeht, ist das traurig und frustrierend. Die Flexibilität ist praktisch auf dem Niveau von magmatischem Gestein, und Funktionen werden über zahllose inkompatible Protokolle für dieselbe Aufgabe – Dateien/Objekte bereitzustellen – angeflanscht.
    • Der Nutzen von Microkerneln ist eine eigene Achse, getrennt vom Hardware/Software-Co-Design.
      Aus praktischer Engineering-Sicht waren monolithische Kernel schneller, einfacher und hatten mehr Ressourcen; Sicherheit war das, was mit C möglich war: Best Effort und sehr viele Bugs. Um dieses Chaos abzumildern, wurde viel Hardware eingeführt. Mit seL4 hingegen ist das Vertrauen in die Isolation zwischen Prozessen und in die Abwesenheit von Root-Level-Exploits sehr hoch, sodass man theoretisch keinen Sicherheits-Coprozessor brauchen könnte. Insofern ist Hardware/Software-Co-Design wichtig.
      Allerdings musste auch das seL4-Team viele Engineering-Ressourcen darauf verwenden, Seitenkanäle der Hardware zu eliminieren. Die reale Welt kümmert sich nicht um Physiksimulationen, daher hat auch Hardware Fehler.
      Der Vorteil eines Microkernels ist hier, dass er klein genug ist, um mit formaler Verifikation handhabbar zu sein. Der Beweis selbst ist zehnmal so groß wie der Kernel. Kontextwechsel in seL4 sind um eine Größenordnung schneller als in Linux, daher sollte der Performance-Effekt vernachlässigbar sein. Wenn man aber auf magische Weise einen monolithischen Kernel mit Millionen Zeilen verifizieren könnte, wäre es weiterhin schneller, keine Kontextwechsel zu machen. Tatsächlich wollte das seL4-Team den Scheduler in den User Space verlagern, aber die Performance-Kosten waren zu hoch, daher blieb er im Kernel und wurde zur Beweislast hinzugefügt.
    • Ich weiß nicht, ob der Vergleich zwischen 80286 und 80386 eine gute Analogie ist. Auch der 286 unterstützte im Protected Mode echtes Multitasking und wurde in mehreren Nicht-DOS-Betriebssystemen genutzt. Eine der Neuerungen des 386 war der Virtual-8086-Modus, der Multitasking für bestehende Real-Mode-DOS-Anwendungen ermöglichte, die direkt auf die Hardware zugriffen.
    • Diese Erklärung scheint nicht zu stimmen. Selbst mit starkem Hardwareschutz: Wie sollte die Trusted Computing Base von Linux mit der eines Microkernels vergleichbar sein? Solange man nicht dieselben Schutzdomänen nachbildet, bleiben in Linux mehr Schwachstellen übrig.
      Die Hauptrolle der Hardware ist eher, die Effizienz zu erhöhen. Moderne Microkernel nutzen zum Beispiel bereits Hardware wie die MMU gut aus und sind deshalb ziemlich robust. Danach verleiht die kleine Trusted Computing Base des Microkernels dem Kernel Vertrauenswürdigkeit, und Kernel und Hardware bilden gemeinsam eine solide Grundlage.
      Letztlich ist es eine Frage, wie viel „Schummeln“ man der Hardware erlauben will, aber insgesamt nutzen Microkernel Schutzfunktionen besser aus. Oder man schaut sich Exokernel an.

  • https://genode.org/index
    Ein Betriebssystem mit seL4-Unterstützung.

    • Ich frage mich, ob es bemerkenswerte Einsatzgebiete von Genode gibt.

  • Ich habe einmal bei einem lokalen OWASP-Chapter einen Vortrag über SeL4 gehalten. Keine Ahnung, ob ich die Unterlagen noch finden kann.
    Dieses Projekt ist wirklich sehr gut gemacht, aber insbesondere im General-Purpose-Computing zögere ich, es als Linux-Ersatz zu sehen. Das heißt nicht, dass Microkernel generell schlecht für den allgemeinen Einsatz wären. RedoxOS scheint in letzter Zeit gewisse Fortschritte zu machen und verwendet einen in Rust geschriebenen Microkernel.

    • Das Problem ist immer: „Von welchem Umfang der Ersetzung sprechen wir?“ Redox scheint stark darauf zu achten, POSIX-Interoperabilität zu wahren, und das beeinflusst natürlich Designentscheidungen. Zwischen technischer Befähigung und Erfolg liegt außerdem ein großer Unterschied.
      Trotzdem wäre allein ein Erfolg von Redox schon ein guter Fortschritt. Bei seL4 sind diese Eigenschaften noch extremer. Die technischen Vorzüge sind hervorragend, aber es hatte bisher nicht – und wird vermutlich auch künftig nicht – das gewisse Etwas, um zum „nächsten großen Ding“ zu werden. Politische Überlegungen einmal ausgeklammert, glaube ich, dass Microkernel erfolgreich sein werden und es auch sein sollten.
    • Ob es Linux ersetzen kann, hängt vom Szenario ab. Natürlich ist Linux einfacher zu handhaben, aber umgekehrt gibt es auch Anforderungen, die nur seL4 erfüllen kann.
      Damit seL4 in der Praxis nützlich ist, braucht es einiges darüber. Glücklicherweise ist auch in diesem Bereich viel Open-Source-Arbeit geleistet worden, und die Lage ist deutlich besser als noch vor einigen Jahren.
      Für statische Szenarien gibt es LionsOS[0], das bereits recht brauchbar ist.
      Für dynamische Szenarien gibt es Provably Secure, General-Purpose Operating System[1], das sich allerdings noch in einem frühen Stadium befindet.
      Beides findet man auf der Projects-Seite[2] von trustworthy systems, die auf der seL4-Website verlinkt ist.
      [0] https://trustworthy.systems/projects/LionsOS/
      [1] https://trustworthy.systems/projects/smos/
      [2] https://trustworthy.systems/projects/

  • Ich frage mich, ob auch das OS, das auf diesem Kernel läuft, formal verifiziert sein muss, damit die Sicherheitsgarantien gelten.

    • Die Garantien, die der Kernel bereitstellt, können von unprivilegierten Prozessen, die darauf laufen, nicht gebrochen werden.
      Natürlich ist ein Kernel allein nicht besonders nützlich; daher bleibt das Design der auf dem Kernel laufenden Treiber, Dateisystem-Server und sonstigen Dienste weiterhin wichtig.
      Wichtig ist auch: Die meisten anderen Systeme, einschließlich Linux, sind auf einer grundlegenden Ebene fehlerhaft, während seL4 es tatsächlich ermöglicht, sichere und vertrauenswürdige Systeme zu bauen.
    • Nein. Der Vorteil ist, dass der Kernel Isolation garantiert, sodass man dem Kernel und den Prozessen nicht vertrauen muss.
      Deshalb kann man einen Linux-Kernel neben einem Hochsicherheitsprozess ausführen und trotzdem die Garantie haben, dass beide – abgesehen von erlaubter IPC – voneinander isoliert sind.
    • Nein.
      Es gibt aber Grenzen. DMA muss deaktiviert werden, und auch Treiber sollten nur formal verifizierte verwendet werden.
      Wichtig ist außerdem, dass der Multicore-Kernel von seL4 noch nicht verifiziert ist.
    • Im absoluten Sinn könnte man das so sehen. Auf praktischer Ebene findet man in Abschnitt 7.2 des Papers eine teilweise Antwort.

  • Drew DeVaults Helios Microkernel ist ebenfalls einen Blick wert. Er soll auf SeL4 basieren.
    https://ares-os.org/docs/helios/

    • Zwischen „basiert auf“ und „inspiriert von“ gibt es einen bedeutsamen Unterschied, und Helios scheint eher Letzteres zu sein.

  • An der Universität Karlsruhe war L4 beliebt. Ich habe es mir nie im Detail angesehen, aber es wirkte wie ein Projekt, das vor allem daran interessiert war, theoretische Ideen zu testen, statt etwas praktisch Nützliches zu bauen.
    Das war vor 20 Jahren, und aus meiner Sicht hat sich daran bis heute nicht viel geändert. Eine schnelle Suche legt nahe, dass es Versuche gibt, darauf ein OS zu bauen, aber sie wirken eher wie Proofs of Concept als wie etwas für den realen Einsatz.

    • Wenn man sich https://en.wikipedia.org/wiki/L4_microkernel_family ansieht, wurde L4 an mehreren Stellen eingesetzt, offenbar hauptsächlich in Embedded-Umgebungen.
      „Die Auslieferungen von OKL4 überschritten Anfang 2012 1,5 Milliarden Stück, größtenteils in Qualcomm-Wireless-Modem-Chips. Weitere Einsätze umfassen Automotive-Infotainment-Systeme.“
      „Die Apple-A-Serienprozessoren ab dem A7 enthalten einen Secure-Enclave-Coprozessor, der ein L4-Betriebssystem ausführt; dieses OS ist sepOS, basierend auf dem L4-embedded-Kernel, der 2006 bei NICTA entwickelt wurde. Infolgedessen ist L4 auf allen modernen Apple-Geräten enthalten, einschließlich Macs mit Apple silicon.“
    • Jochen Liedtke wurde 1999 Professor in Karlsruhe, verstarb aber leider kurz darauf im Jahr 2001. Ich weiß nicht, ob sein Nachfolger Bellosa noch L4-Forschung betreibt. Es gab das L4Ka-Projekt, aber es scheint abgeschlossen zu sein. In Bellosas Bachelor-Vorlesung zu Betriebssystemen ist es nicht Teil des Curriculums.
      Bellosas ehemaliger Student Rittinghaus ist an Unikraft[0] beteiligt, das auch ein paar Mal auf HN vorgestellt wurde, und nutzt Unikernel-Technologie.
      [0] https://unikraft.org/
    • Im iPhone kommt eine L4-Variante zum Einsatz.
      „Der Secure Enclave Processor führt eine von Apple angepasste Version des L4-Mikrokernels aus.“
      https://support.apple.com/de-at/guide/security/sec59b0b31ff/...
    • Der Open-Source-Ableger L4Re läuft auf der zentralen „icas1“-ECU aller id.X-Fahrzeuge von Volkswagen und hostet Linux und andere Gäste.
      https://www.kernkonzept.com/kk_events/elektrobit-advances-au...
      Meiner Ansicht nach ist der L4Re-Kernel auch Teil von Elektrobit Safe Linux.
    • Mir gefallen die Arbeit und die Richtung des Karlsruher Teams bei L4Ka, insbesondere bei Pistachio. Das Design war sauber, einfach und leicht verständlich.
      Für meine Abschlussarbeit habe ich ein auf Pistachio basierendes OS gebaut. Ich habe immer gedacht, dass ich wohl in die OS-Forschung gegangen wäre, wenn ich in Karlsruhe studiert hätte.

  • Ich hatte ebenfalls Ideen für das Design eines Betriebssystems, und die Capability, die ich in Betracht zog, nutzte dieselben Funktionen für Zwischenschaltung und Delegation wie seL4. Neben dem, was dort steht, gibt es weitere Vorteile. Beispielsweise kann man Proxy-Capabilities verwenden, um Filter auf Audio anzuwenden oder Netzwerktransparenz umzusetzen.
    Ich dachte, Echtzeitfunktionen könnten als optionale Implementierung erlaubt sein. Meine Idee war eher eine Spezifikation als eine einzelne Implementierung.
    Eine weitere gewünschte Eigenschaft war, dass sich alle Programme deterministisch verhalten, abgesehen von Ein-/Ausgabe. Ohne Ein-/Ausgabe kann man weder Datum/Uhrzeit noch die Laufzeit des Programms kennen, und auch Prozessorfunktionen lassen sich nicht feststellen. Wenn eine Funktion genutzt wird, die die Hardware nicht unterstützt, könnte das Betriebssystem sie emulieren.
    Zur Umsetzung wollte ich eine Mischung aus Hardware- und Software-Unterstützung verwenden. Im Dokument gibt es eine Anmerkung zu Angriffen auf in Hardware implementierte Capabilities, aber ich habe die Referenzdokumente nicht vorliegen und weiß daher nicht, ob dieser Angriff auch auf den von mir gedachten Ansatz zutrifft.

  • Aus Sicherheitsperspektive scheint es ähnliche Schwächen zu zeigen wie KVM im Linux-Kernel. Wenn der Hypervisor in Ring 0 läuft, besteht das Risiko, aus einer VM in eine andere VM oder in den Host selbst auszubrechen.
    Ich frage mich, wie dieses Risiko gemindert wird.

    • Bei der Virtualisierungsunterstützung von seL4 werden VM-Exceptions in Nachrichten umgewandelt, und ein VMM, also eine Aufgabe, die im nicht privilegierten Modus läuft, verarbeitet sie.
      Der VMM hat nicht mehr Capabilities als die VM selbst, daher ist ein VM-Escape außerhalb des akademischen Sinns wertlos.
      Siehe Seiten 8–10 des ursprünglichen PDFs.