Ironclad – echtzeitfähiger Unix-artiger OS-Kernel

• Ironclad ist ein echtzeitfähiger Unix-artiger Kernel auf Basis formaler Verifikation für allgemeine und eingebettete Umgebungen
  • Formale Verifikation: eine Reihe von Prozessen und Prüfungen, die der Kernel-Code durchläuft, um Freiheit von Laufzeitfehlern (AoRTE, Absence of Runtime Errors) und die Korrektheit der Komponenten zu gewährleisten
• Geschrieben in SPARK und Ada und besteht zu 100 % aus freier Software
• Unterstützt POSIX-kompatible Schnittstellen, präemptives Multitasking, Mandatory Access Control (MAC) und Hard-Real-Time-Scheduling
• Wird unter der GPLv3-Lizenz veröffentlicht und behält eine vollständig Open-Source-Struktur ohne Firmware-Blobs bei
• Auf mehrere Plattformen portierbar; das Ökosystem wird über Distributionen wie Gloire erweitert

---

Überblick über den Ironclad-Betriebssystemkernel

• Ironclad ist ein echtzeitfähiger UNIX-artiger Kernel, bei dem formale Verifikation teilweise angewendet wird
  • Für allgemeine Zwecke und eingebettete Systeme konzipiert
  • Formale Verifikation: eine Reihe von Prozessen und Prüfungen, die der Kernel-Code durchläuft, um Freiheit von Laufzeitfehlern (AoRTE, Absence of Runtime Errors) und die Korrektheit der Komponenten zu gewährleisten
  • Dafür wird SPARK verwendet, eine Teilmenge von Ada
  • Der gesamte Code besteht aus freier Software
• Der Kernel bietet POSIX-kompatible Schnittstellen und unterstützt präemptives Multitasking, Mandatory Access Control (MAC) und Hard-Real-Time-Scheduling
  • Bietet eine Entwicklungsumgebung ähnlich zu bestehenden UNIX-Umgebungen
  • Geeignet für Systeme, die Echtzeitsteuerung erfordern

Eigenschaften als freie Software

• Ironclad wird unter der GPLv3-Lizenz als vollständiges Open Source veröffentlicht
  • Der Kernel enthält keine Firmware-Blobs
  • Alle Komponenten des Stacks werden als Open Source bereitgestellt

Formale Verifikation

• Nutzt die Funktionen zur formalen Verifikation der SPARK-Sprache, um Fehlerfreiheit und Korrektheit wichtiger Komponenten zu gewährleisten
• SPARK verifiziert die logische Konsistenz des Codes mathematisch, indem in Ada-Code Vorbedingungen (Pre), Nachbedingungen (Post) und Abhängigkeiten (Depends) angegeben werden
  • Zu den verifizierten Bereichen gehören Kryptomodule, MAC-Systeme und Funktionen rund um die Benutzeroberfläche

Portabilität und Entwicklungsumgebung

• Ironclad wurde auf verschiedene Plattformen und Boards portiert und ist so ausgelegt, dass weitere Portierungen leicht möglich sind
  • Abhängig nur von der GNU-Toolchain, wodurch einfaches Cross-Compiling möglich ist
  • Dank POSIX-Kompatibilität sind Software-Portierung und Entwicklung unkompliziert

Distributionen und Ökosystem

• Das Ironclad-Projekt bietet Distributionen für verschiedene Architekturen und Boards an
  • Eine repräsentative freie Open-Source-Distribution ist Gloire
  • Es werden herunterladbare Distributions-Images im Tarball-Format bereitgestellt

Projektförderung und Nachhaltigkeit

• Ironclad wird als Projekt zur freien Nutzung, Erforschung und Modifikation erhalten
  • Der Betrieb des Projekts hängt von Spenden und Fördergeldern ab
  • Jeder Beitrag wirkt sich direkt auf die Erweiterung und Weiterentwicklung des Projekts aus

[GN⁺]

Hacker-News-Kommentare

• Ein interessantes Projekt. Ich frage mich, wo die Grenzen der formalen Verifikation der Worst-Case Execution Time (WCET) liegen
  Es gibt auch andere verifizierte Kernel wie seL4 und atmosphere, und man könnte wie bei genode auch eine POSIX-kompatible Schicht darüberlegen
  Es gibt zudem vollständig kompatible und ausgereifte Kernel wie QNX oder VxWorks, daher ist vollständige Verifikation möglicherweise kein so großer Mehrwert
  Aber Beispiele, die WCET + formale Verifikation + POSIX-Kompatibilität zugleich bieten, habe ich kaum gesehen
  Im aktuellen Stadium würde ich den Reifegrad noch nicht für hoch genug halten, um es direkt für die in der Dokumentation genannten Echtzeit-Anwendungsfälle einzusetzen

  • Jede Regierung lebt in einer Welt, in der man RCE gegen ein OS erreichen kann. Deshalb ist die formale Verifikation der Prozessisolierung wirklich wichtig
    seL4 ist viel schneller als Linux, aber das hier wirkt eher langsam. POSIX hat von Natur aus Mängel, und MAC ist zu komplex, um in der Praxis leicht nutzbar zu sein
  • Es ist noch auf stone-Niveau, aber ich könnte mir vorstellen, dass es künftig auch offizielle Zertifizierungen erhält. Ein formal verifiziertes OS ist ein großer Fortschritt für die Sicherheit

• Ada gehört zur Wirth-Sprachfamilie (Pascal-Familie). Bisher kannte ich als Unix-ähnlichen Kernel aus einer Wirth-Sprache nur TUNIS
  TUNIS wurde in Concurrent Euclid implementiert

  • In den 90ern gab es an der University of Washington auch SPIN. Das war ein mikrokernelbasiertes System in Modula-3 mit Unterstützung für das Digital-UNIX-Systemaufruf-Interface
    Außerdem wurde in den 80ern bei INRIA Sol in einem Pascal-Dialekt implementiert und bot eine Unix-kompatible Umgebung; später ging daraus Chorus hervor

• Es gibt auch ein NDA-bezogenes Unternehmen namens Ironclad. Man sollte bei Markenrechtsproblemen vorsichtig sein
  Trotzdem freue ich mich sehr über solche Versuche. In der Realität ist jedoch die schwächste Stelle der Sicherheit die Firmware-Ebene
  Mein Traum ist Hardware wie die Computer von Framework, die verifizierte EFI-Firmware und für jede Komponente auditierte Firmware mitbringt

  • Ironclad ist auch der Name einer wichtigen Kryptografie-Bibliothek für Common Lisp (ironclad GitHub)
  • MNT Research ist ebenfalls einen Blick wert. Sie bauen reparierbare Laptops und veröffentlichen sowohl Hardware als auch Software als Open Source (mnt.re)
  • Für Firmware-Verifikation braucht es einen separaten Kernel. Solche Bereiche sollten inzwischen auf regulatorischer Ebene verwaltet werden
  • Marken sind kein Problem, wenn derselbe Name in unterschiedlichen Branchen verwendet wird. Siehe etwa Apple Computer und die Beatles mit Apple Music (xkcd 386)

• Ein neues OS zu bauen ist wirklich ambitioniert. Kürzlich wurde auch Radiant Computer vorgestellt, und ich frage mich, ob es noch mehr ähnliche spannende Projekte gibt

  • Asterinas (Linux-kompatibler Kernel) und Redox OS wirken vielversprechend
  • Es gibt auch SerenityOS
  • Als ältere Alternative ist auch Haiku OS weiterhin interessant
  • Ich habe auch selbst Ideen für ein OS. Ich denke über mehrere Komponenten nach, einschließlich Hardware, Kernel und User-Programmen
  • ReactOS entwickelt sich ebenfalls weiter. Es ist zwar kein komplett neues OS, wirkt aber trotzdem noch neu

• Ich hoffe, dass sich ein vollständig formal verifizierter Kernel irgendwann verbreitet
  Das gesamte Linux zu verifizieren ist wohl unmöglich, aber seL4 könnte in Märkten wie Smartphones vielleicht eine Chance haben

  • seL4 wird bereits in Dingen wie Secure Enclave OS verwendet (L4 microkernel family)
  • seL4 ist schon an vielen Stellen im Einsatz, und wenn man sich die Use Cases und die Mitgliederliste ansieht, könnte es sich künftig noch weiter verbreiten

• Wenn man sich ihre Verifikations-Roadmap ansieht, ist die Bezeichnung „formale Verifikation“ übertrieben
  Es gibt keine Beweise für zentrale Kernel-Eigenschaften, und das Niveau von Kerneln wie seL4 oder Tock erreicht es nicht

• CuBit ist ein weiteres in SPARK/Ada geschriebenes OS
  Den Quellcode gibt es auf GitHub

• Aus Sicht normaler Nutzer ist ein Kernel allein nicht besonders nützlich
  Ein Beispiel für ein OS, das den Ironclad-Kernel verwendet, ist Gloire

• Die Dokumentation zu MAC ist gut aufbereitet (Mandatory Access Control)

• Wenn man bei SPARK den Hinweis „Preis auf Anfrage“ sieht, klingt das weniger nach „freier Software“ als nach einer anderen Bedeutung von „free“

  • Auch bei den oben verlinkten GitHub-Projekten ist kommerzieller Support meist kostenpflichtig. „Preis auf Anfrage“ ist ein üblicher Ablauf und daher nichts Besonderes
  • Am Ende müssen Entwickler auch ihren Lebensunterhalt verdienen, und das ist völlig selbstverständlich