Wie ein System zusammenspielt

Jedes NoWayOS-Gerät ist ein System: eine feste Menge von Teilen, deklariert, bevor es gebaut wird, jeder von seL4 gegen die anderen abgeschottet. Zur Laufzeit kommt nichts hinzu. Diese Seite erklärt die Bausteine und wie sie zusammenhängen.

Schutzdomänen

Eine Schutzdomäne ist ein Teil eines Systems: ein Programm mit eigenem Speicher, das nur die Capabilities hält, die ihm gewährt werden. In seL4 ist eine Capability ein unfälschbares Token, das ein Kernelobjekt und die Rechte daran benennt, wie eine Schlüsselkarte für genau eine Tür. Eine Schutzdomäne kann nichts berühren, was ihre Capabilities nicht benennen, und seL4 setzt das durch.

Ein typisches System hat eine Schutzdomäne für jede Zuständigkeit: einen Display-Treiber, den Eingabepfad, den Netzwerkstack, die Benutzeroberfläche, die Anwendung, einen Timer, einen Supervisor und einen Watchdog. Jede ist ein kleines Rust-Programm, no_std, das nach dem Start nichts mehr alloziert.

Die Systembeschreibung

Die Microkit-Systembeschreibung (systems/NAME.system, eine XML-Datei) deklariert das ganze System: jede Schutzdomäne mit ihrer Priorität, ihrem Budget und ihrem Stack; jeden Speicherbereich und wer ihn einblendet; jeden Kanal; jeden Interrupt.

• Beschreibungen benennen Geräte, nie Adressen: phys_addr="@NAME". Die Adressen stammen aus der Datei des Boards in platforms/, jede mit ihrer Quelle, sodass dieselbe Beschreibung für QEMU und für den Raspberry Pi 5 baut.
• Kanäle verbinden zwei Schutzdomänen, für Benachrichtigungen (Signale ohne Daten, darunter Interrupts) und geschützte Prozeduraufrufe (synchrone Aufrufe in einen Teil höherer Priorität).

Die Beschreibung ist das Sicherheitsdesign des Systems, daher wird eine Änderung daran als Sicherheitsänderung geprüft.

Die Freigabedatei

Neben jeder Beschreibung listet systems/NAME.grants alles auf, was das System freigibt, ein Fakt pro Zeile: Prioritäten, Budgets, Speicher, Geräte, Interrupts und Kanäle. Der Build schlägt fehl, wenn die beiden in irgendeiner Richtung voneinander abweichen.

Jede Schutzdomäne hat außerdem eine Rolle (ui, input, broker, display, driver, network, security, storage, update, app, supervisor, watchdog, clock oder test), und der Build lehnt eine Freigabe ab, die ihre Rolle nie haben darf. Einer Benutzeroberfläche kann nicht versehentlich ein Netzwerkgerät übergeben werden, und ein Testinstrument kann nicht in ein Produkt rutschen.

Typisierte Nachrichten

Schutzdomänen kommunizieren über typisierte Nachrichten: versionierte Datensätze fester Größe mit explizitem Layout, die über Single-Producer-Single-Consumer-Ringe im gemeinsamen Speicher laufen.

• Erst kopieren, dann prüfen. Ein Empfänger kopiert jeden Datensatz aus dem gemeinsamen Speicher, bevor er ihn validiert, sodass der Absender ihn zwischen Prüfung und Verwendung nicht ändern kann (der Fehler namens Double-Fetch).
• Decoder können keine Panic auslösen. Jeder Decoder gibt für alles Fehlerhafte einen typisierten Fehler zurück und hat beschränkte Kani-Beweise und ein Fuzz-Target.
• Jede Seite hat ihre eigene Sicht. Producer und Consumer sehen den Ring über getrennte Speichersichten, und gemeinsame Indizes nutzen Acquire- und Release-Ordering.

Eingaben

Anwendungen sehen kanonische Eingabeereignisse, also Tastendrücke, Zeigerbewegungen und Berührungen, geprüft gegen den Bildschirm und in ihrer Rate begrenzt. Sie sehen nie USB oder ein anderes Geräteprotokoll; der Eingabepfad parst diese in eigenen Schutzdomänen und behandelt jedes Byte als feindselig.

Faults, der Supervisor und der Fail-safe-Zustand

Wenn eine Schutzdomäne etwas tut, das seL4 nicht zulässt, oder eine Panic auslöst, stoppt seL4 sie und meldet einen Fault an ihre Eltern-Schutzdomäne.

• Der Supervisor ist die Eltern-Schutzdomäne der anderen Teile. Er empfängt jeden Fault, meldet ihn und setzt das Board zurück, sodass das System sauber neu startet. Er ist gebaut und in QEMU-Testsystemen getestet.
• Der Fail-safe-Zustand ist der Zustand, in den ein Gerät geht, wenn sich die Fehler häufen: standardmäßig beim vierten Neustart seit einem Kaltstart oder beim zweiten Fault in einem sicherheitsrelevanten Teil wie Storage oder Updates. Nur der Supervisor, der Watchdog und, wo möglich, das Display laufen weiter, und nur ein Kaltstart aus dem ausgeschalteten Zustand holt das Gerät zurück.
• Die Watchdog-Schutzdomäne bedient den Hardware-Watchdog nur, solange jeder andere Teil auf seinen Heartbeat antwortet. Antwortet einer nicht mehr, setzt die Hardware das Board zurück.

Speicher und Zeit

• Der Speicher wird festgelegt, wenn das Image gebaut wird. Gerätecode alloziert nichts: Jeder Puffer und jede Queue hat eine feste Größe, aus nowayos-bounded. Die einzige Ausnahme, der TLS-Client, arbeitet in einer eigenen Arena fester Größe.
• Zwei Arten von Zeit, die sich nie vermischen. Monotone Zeit zählt ab dem Booten und läuft nie rückwärts; jedes Timeout nutzt sie. Wall-Clock-Zeit, also Datum und Uhrzeit, stammt aus einer authentifizierten Quelle. Es sind verschiedene Rust-Typen, sodass sich die eine nicht übergeben lässt, wo die andere gemeint ist.

Eigene Systeme bauen

Die eigenen Systeme und Schutzdomänen Ihres Produkts liegen in einem eigenen Repository neben nowayos, nie darin. Das Makefile dieses Repositorys setzt SYSTEM_REPO := $(CURDIR) und bindet die Make-Fragmente von NoWayOS ein:

SYSTEM_REPO := $(CURDIR)
include ../nowayos/tools/make/container.mk
include ../nowayos/tools/make/system.mk

Dann funktionieren make image, make qemu-test, make qemu-test-all und die Prüfungen auf dessen systems/ und pds/, mit dem Dev-Container, den Board-Dateien, den Freigaberegeln und den Prüfungen von NoWayOS. Die Variablen sind oben in tools/make/system.mk dokumentiert. Das Showcase ist genau so gebaut.