Die Begriffe, im Klartext.

Alles, was ein Angreifer gegen ein Gerät zu nutzen versuchen könnte: sein Code, seine Dienste, Schnittstellen und Eingaben. Weniger Code und weniger Funktionen lassen weniger davon übrig.

Ein Gerät weist einem entfernten Dienst kryptografisch nach, welche Software es gestartet hat. Das zeigt, was beim Booten geladen wurde, nicht alles, was seitdem geschehen ist. Für NoWayOS auf Produktionshardware geplant; noch nicht gebaut.

Ein Beweis, dass eine Eigenschaft für jede Eingabe bis zu einer festgelegten Größe gilt. NoWayOS beweist seine Nachrichtendecoder auf diese Weise, mit Kani.

In seL4 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 nur berühren, was ihre Capabilities benennen.

Ein offenes Standardformat für Software-Stücklisten. NoWayOS schreibt eine für jeden Workspace und jedes System-Image. Siehe SBOM.

Der USB-zu-Seriell-Adapter von Raspberry Pi. Am Debug-Anschluss des Raspberry Pi 5 überträgt er das Boot-Log und lädt Test-Images.

Das fest versionierte Container-Image mit der gesamten Toolchain von NoWayOS: den Rust-Toolchains, dem Microkit SDK, QEMU und den Prüfwerkzeugen. Jedes make-Target läuft darin, sodass Ihr Rechner nur Podman und make braucht (und Python 3.11, um einen Raspberry Pi 5 zu steuern).

Ein Fehler, bei dem Code Daten im gemeinsamen Speicher prüft und sie dann erneut liest, sodass die andere Seite sie dazwischen ändern kann. Verhindert durch erst kopieren, dann prüfen.

Eine Rust-Bibliothek für 2D-Grafik auf Geräten ohne den Grafikstack eines Betriebssystems. Die Benutzeroberfläche von NoWayOS zeichnet damit.

Die Regel, dass eine Nachricht aus dem gemeinsamen Speicher kopiert wird, bevor sie validiert wird, sodass der Absender sie zwischen Prüfung und Verwendung nicht ändern kann. Sie verhindert einen Double-Fetch.

systems/NAME.expect: die Zeilen, die ein System in der richtigen Reihenfolge ausgeben muss, und der Text, der den Test scheitern lässt, wenn er irgendwo auftaucht. Dieselbe Datei prüft ein System in QEMU und auf dem Raspberry Pi 5.

Wohin ein NoWayOS-Gerät geht, wenn sich die Fehler häufen: Nur der Supervisor, der Watchdog und, wo möglich, das Display laufen weiter, bis zu einem Kaltstart.

Der Fehler, den seL4 meldet, wenn eine Schutzdomäne etwas tut, das der Kernel nicht zulässt, oder eine Panic auslöst. Der Teil bleibt gestoppt, bis sein Fault-Handler handelt.

Ein mathematischer Beweis, vom Computer geprüft, dass Software ihre Spezifikation erfüllt. seL4 hat ihn für bestimmte Konfigurationen. Der eigene Code von NoWayOS stützt sich stattdessen auf Rust, Isolation, Tests und beschränkte Beweise.

systems/NAME.grants: alles, was ein System freigibt, ein Fakt pro Zeile: Prioritäten, Budgets, Speicher, Geräte, Interrupts und Kanäle. Der Build schlägt fehl, wenn die Systembeschreibung und die Freigabedatei nicht übereinstimmen.

Einen Parser mit Millionen generierter Eingaben testen, bis eine davon ihn zum Absturz bringt oder eine Prüfung verletzt. Jeder Parser für Eingaben von außen in NoWayOS hat ein Fuzz-Target.

Eine Schrift, die vorab beim Build in Bilder ihrer Zeichen gezeichnet wird, sodass ein Gerät Text zeichnet, ohne je eine Schriftdatei zu parsen.

Die Familie industrieller Arm-Prozessoren von NXP und die vorgesehene Produktionshardware von NoWayOS. Noch nicht unterstützt.

Ein System, das zu erreichen versucht, was ihm nicht freigegeben wurde, und das seL4 stoppen muss. Eine Variante mit absichtlich erweiterter Freigabe muss fehlschlagen, und das zeigt, dass der Test fehlschlagen kann.

Ein Start aus dem ausgeschalteten Zustand, im Gegensatz zu einem Reset. Nur ein Kaltstart holt ein NoWayOS-Gerät aus seinem Fail-safe-Zustand zurück.

In Microkit eine deklarierte Verbindung zwischen zwei Schutzdomänen, für Benachrichtigungen (Signale ohne Daten, darunter Interrupts) und geschützte Prozeduraufrufe.

Ein Model Checker für Rust, der Eigenschaften für jede Eingabe bis zu einer Schranke beweist. NoWayOS beweist damit, dass seine Nachrichtendecoder nie eine Panic auslösen, nie überlaufen und nie außerhalb der Grenzen lesen.

Das Framework der seL4 Foundation für statische seL4-Systeme aus Schutzdomänen, die in einer Systembeschreibung deklariert sind.

Ein Kernel, der so klein wie möglich gehalten wird, während Treiber, Netzwerk und Bildschirm außerhalb davon laufen, jeweils in einer eigenen Kammer. seL4 ist einer.

Ein Interpreter für Rust, der undefiniertes Verhalten erkennt. NoWayOS lässt ihn über die wenigen Crates laufen, die unsafe-Code verwenden dürfen.

Die Konfiguration von seL4 mit Scheduling-Budgets und -Perioden, die Microkit baut. Ihre AArch64-Beweise sind noch in Arbeit, daher liegt heute kein NoWayOS-Image innerhalb der abgeschlossenen Beweise von seL4.

Zeit, die ab dem Booten gezählt und nie gestellt wird und die nie rückwärts läuft. Jedes Timeout in NoWayOS nutzt sie, und sie vermischt sich nie mit der Wall-Clock-Zeit.

Ein Open-Source-Emulator für Rechner. Jedes NoWayOS-System bootet darin und prüft seine eigene Ausgabe, bevor es Hardware berührt.

Das günstige Board, das NoWayOS als Referenzhardware nutzt.

Eine Programmiersprache, deren sicherer Code Speichersicherheitsfehler ausschließt. Der eigene Code von NoWayOS ist durchgehend Rust.

Die Rust-Unterstützung der seL4 Foundation, einschließlich des Crates zum Schreiben von Microkit-Schutzdomänen.

Eine in Rust geschriebene TLS-Bibliothek. Der TLS-1.3-Client von NoWayOS baut darauf auf, zusammen mit RustCrypto.

Eine Software-Stückliste (Software Bill of Materials): eine Liste jeder Komponente und Version in einer Software. NoWayOS schreibt eine im Format CycloneDX für jeden Workspace und jedes System-Image.

Ein isolierter Teil eines Microkit-Systems: ein Programm mit eigenem Speicher, das nur die Capabilities hält, die ihm ausdrücklich gewährt werden. Die abgeschotteten Kammern von NoWayOS.

Das Build-Werkzeug von NoWayOS, das React-Screens, geschrieben in TSX in einer unterstützten Teilmenge, in Rust für die Benutzeroberfläche von NoWayOS umwandelt. Es lehnt alles außerhalb der Teilmenge ab, statt es näherungsweise umzusetzen.

Das seL4 Device Driver Framework: ein Referenzdesign für Treiber auf Microkit mit Queues im gemeinsamen Speicher. Die Netzwerk-Queues von NoWayOS folgen ihm.

Ein Gerät weigert sich, Software zu starten, die nicht von seinem Hersteller signiert ist. Für NoWayOS auf Produktionshardware geplant; noch nicht gebaut.

Ein Mikrokernel mit rund 10.000 Zeilen, gepflegt von der seL4 Foundation, mit maschinengeprüften Beweisen für Korrektheit und Sicherheit für bestimmte Konfigurationen. NoWayOS läuft darauf.

Das Protokoll, das neben jedes NoWayOS-Image geschrieben wird: seine seL4-Konfiguration und ob diese Konfiguration innerhalb der abgeschlossenen Beweise von seL4 liegt.

Ein Allzweckgerät sicherer machen, indem man seine Einstellungen ändert. Die Funktionen sind weiterhin da, und ein einziger Fehler kann jede Einstellung umgehen.

Ein Gerät bauen, das die riskanten Dinge nicht tun kann, weil sie nie eingebaut wurden. Der Ansatz von NoWayOS.

Ein Betriebssystem, gebaut für die eine Aufgabe eines Geräts, statt für alles gebaut und dann auf eine Sache abgeriegelt. Drei Dinge machen es aus: Es ist für eine Aufgabe gebaut (sein Image enthält die Anwendung, die Treiber, die sie nutzt, und den Kernel, sonst nichts); es ist innen abgeschottet (jeder Teil in seiner eigenen Kammer, mit Zugriff nur auf das, was ihm freigegeben wurde); und es legt seinen Rechenweg offen (die Nachweise, was darin steckt, werden mitgeliefert). Kein Kioskmodus, der ein System, das sicher durch Konfiguration ist, auf eine App abriegelt. NoWayOS ist ein Single Purpose OS: ein Computer, der sonst nichts zu tun hat.

Ein TCP/IP-Stack in Rust, der im Betrieb keinen Speicher alloziert. Der Netzwerkstack von NoWayOS baut darauf auf.

Ein Fehler wie das Lesen über das Ende eines Puffers hinaus oder die Verwendung von Speicher, nachdem er freigegeben wurde. Microsoft und Google haben jeweils berichtet, dass rund 70 % ihrer schweren Sicherheitsfehler von dieser Art sind; sicheres Rust schließt sie aus.

Die Schutzdomäne, die die Faults der anderen Teile empfängt, sie meldet und das System sauber neu startet.

Die Microkit-XML-Datei, die jede Schutzdomäne, jeden Speicherbereich, jeden Kanal und jeden Interrupt eines Systems deklariert. Sie ist das Sicherheitsdesign des Systems, und eine Änderung daran wird auch als solche geprüft.

Alles, auf dessen Korrektheit eine Sicherheitseigenschaft angewiesen ist. Für ein NoWayOS-System: der seL4-Kernel, der Microkit-Loader und -Monitor sowie die Schutzdomänen, auf die sich diese Eigenschaft stützt.

Ein Datensatz fester Größe mit explizitem Layout, der zwischen Schutzdomänen über gemeinsamen Speicher übergeben und beim Empfang geprüft wird. Siehe erst kopieren, dann prüfen.

Rust-Code, den der Compiler nicht auf Speichersicherheit prüfen kann. Verboten in jedem NoWayOS-Crate außer in einer kurzen, geprüften Liste, die die Prüfungen durchsetzen.

Datum und Uhrzeit, aus einer authentifizierten Quelle. NoWayOS hält sie als eigenen Typ getrennt von der monotonen Zeit.

Ein Hardware-Timer, der das Board zurücksetzt, wenn die Software ihn nicht bedient. Die Watchdog-Schutzdomäne von NoWayOS bedient ihn nur, solange jeder andere Teil auf seinen Heartbeat antwortet.