Einführung in den seL4-Mikrokernel [PDF]

• seL4 ist ein OS-Mikrokernel, der mit minimalem Code im Kernel-Modus läuft, Hardware-Ressourcen steuert und die Sicherheit erhöht
• Er gehört zur L4-Mikrokernel-Familie und wird seit Mitte der 1990er Jahre entwickelt
• Er kann als Hypervisor arbeiten und die Ausführung von Gastbetriebssystemen wie Linux unterstützen
• Als weltweit erster OS-Kernel wurde seine funktionale Korrektheit nachgewiesen; der mathematische Beweis auf Code-Ebene ist abgeschlossen
• Für feingranulare Zugriffskontrolle wird ein Capability-basiertes Sicherheitsmodell verwendet

Architektur und Hypervisor-Funktionen von seL4

• Monolithischer Kernel vs. Mikrokernel
  • Monolithischer Kernel (Linux usw.): Der Kernel-Code ist sehr umfangreich, daher gibt es viele Sicherheitslücken → etwa 20 Millionen Zeilen Code (20M SLOC)
  • Mikrokernel (seL4): Verwendet minimalen Kernel-Code → etwa 10.000 Zeilen Code (10K SLOC)
  • Kleinere Kernel-Größe → stärkere Sicherheit und geringere Angriffsfläche
• seL4 übernimmt die Rolle eines Hypervisors
  • In VMs können vollständige Gastbetriebssysteme wie Linux ausgeführt werden
  • Jede VM läuft unabhängig, gegenseitige Beeinflussung ist nicht möglich → starke Isolation gewährleistet
  • Protected Procedure Call (PPC) → sichere Kommunikation zwischen VMs möglich

Verifikation und Sicherheitsmodell von seL4

• Verifikation der funktionalen Korrektheit
  • Für seL4 wurde auf Code-Ebene mathematisch bewiesen, dass die Funktionalität korrekt ist
  • Es wird garantiert, dass alle Kernel-Operationen gemäß der Spezifikation arbeiten
• Translation Validation
  • Es wird bewiesen, dass der vom Compiler erzeugte Binärcode exakt mit dem ursprünglichen C-Code übereinstimmt
  • Dies geschieht über eine automatisierte Toolchain
• Verifikation von Sicherheitseigenschaften
  • Vertraulichkeit: Zugriff auf Daten nur, wenn dies explizit erlaubt ist
  • Integrität: Änderung von Daten nur, wenn dies explizit erlaubt ist
  • Verfügbarkeit: Nutzung von Ressourcen nur, wenn dies explizit erlaubt ist

Capability-basiertes Sicherheitsmodell

• Was ist eine Capability?
  • Ein Sicherheitstoken, das Zugriffsrechte auf ein bestimmtes Objekt gewährt
  • Kodiert sowohl die Objektreferenz als auch die Zugriffsrechte
  • Ermöglicht detaillierte Zugriffskontrolle → Anwendung des Prinzips der geringsten Privilegien (Principle of Least Privilege, POLA)
• Vorteile von Capabilities
  • Feingranulare Zugriffskontrolle → Rechte lassen sich minimieren
  • Delegation und Entzug von Berechtigungen möglich
  • Starkes Sicherheitsmodell → herkömmlichen Zugriffskontrollmodellen (ACL) überlegen
• Lösung für das Confused-Deputy-Problem
  • In traditionellen ACL-basierten Systemen wird der Sicherheitsstatus durch die Sicherheits-ID des Subjekts bestimmt
  • In seL4 bestimmen Capabilities die Sicherheitsrechte direkt → klare Rechtekontrolle möglich

Unterstützung für Echtzeitsysteme und Mixed-Criticality-Systeme

• Unterstützung für Echtzeitsysteme
  • seL4 unterstützt prioritätsbasiertes Scheduling
  • Die Worst-Case Execution Time (WCET) aller Kernel-Operationen wurde analysiert → Hard-Real-Time-Garantien
• Unterstützung für Mixed-Criticality Systems (MCS)
  • CPU-Ressourcen werden auf Basis von Scheduling-Kontexten zugewiesen und isoliert
  • Es wird verhindert, dass Aufgaben mit hoher Priorität die CPU monopolisieren
  • Kritische und unkritische Aufgaben können gleichzeitig ausgeführt werden

Performance und Effizienz

• Mikrokernel mit Spitzenleistung
  • Selbst wenn Performance entscheidend ist, wird die Sicherheit nicht beeinträchtigt
  • Die Kosten für Systemaufrufe und IPC sind minimiert → mehr als 5-mal schneller als konkurrierende Systeme
• Überlegene Performance gegenüber Konkurrenzsystemen
  • Fiasco.OC: etwa 2-mal langsamer als seL4
  • Zircon: etwa 9-mal langsamer als seL4
  • CertiKOS: etwa 5-mal langsamer als seL4

Praxisanwendungen und schrittweise Cyber-Nachrüstung

• Reale Einsatzbeispiele

  • Erfolgreich bei Boeings ULB (unbemannter Hubschrauber) eingesetzt
  • Verbesserte Sicherheit und höhere Systemstabilität bestätigt

• Schrittweise Sicherheitsverbesserung bestehender Systeme (Incremental Cyber Retrofit)

  • Bestehende Systeme werden in VMs ausgeführt und schrittweise modularisiert
  • Höhere Sicherheit bei minimalem Performance-Verlust

Fazit

• seL4 ist der sicherste Mikrokernel der Welt, dessen funktionale Korrektheit, Sicherheit und Performance nachgewiesen wurden
• Dank verifiziertem Sicherheitsmodell und Unterstützung für Mixed-Criticality-Systeme ist er in vielen Bereichen praktisch einsetzbar
• Bestehende Systeme können sicherer gemacht und ihre Performance verbessert werden → ein innovativer Mikrokernel, der Sicherheit und Performance in Einklang bringt