NoWayOS
DE
GitHub
MenüSchließen

Plattform

Von der Aufgabe her gebaut.

Sie schreiben Ihre Anwendung in Rust. NoWayOS baut sie, mit genau den Treibern, die sie nutzt, auf den seL4-Mikrokernel. Das fertige Image enthält genau das und sonst nichts.

Erste SchritteSicherheit

Von der Anwendung zum Image

Ein NoWayOS-Gerät wird gebaut, nicht konfiguriert. Vier Schritte bringen Ihren Code auf ein Gerät, das seine eine Aufgabe erledigt, und jeder Schritt hinterlässt etwas, das Sie prüfen können.

  1. Die Anwendung schreiben

    In Rust, als eine oder mehrere Schutzdomänen. Bauen Sie ihre Screens mit dem kleinen deklarativen UI-Kern von NoWayOS, oder gestalten Sie sie in React und wandeln Sie sie beim Build mit dem Screen Compiler um.

  2. Das System beschreiben

    Eine Microkit-Systembeschreibung deklariert jede Schutzdomäne, jeden Speicherbereich, jeden Kanal und jeden Interrupt. Daneben listet eine Freigabedatei alles auf, was das System freigibt, und eine Expect-Datei, was es beim Laufen ausgeben muss.

    systems/hello.system   systems/hello.grants   systems/hello.expect

  3. Es bauen

    Im Dev-Container. Der Build gleicht die Freigaben mit der Beschreibung ab und schreibt dann das Image, zusammen mit seiner Software-Stückliste und einem Protokoll seiner seL4-Konfiguration.

    make image SYSTEM=hello

  4. Es booten und sich selbst prüfen lassen

    Zuerst in QEMU: Das System bootet ohne Bildschirm und muss jede Zeile, die seine Expect-Datei auflistet, in der richtigen Reihenfolge ausgeben, und nichts, was die Datei verbietet. Dann auf dem Raspberry Pi 5, geprüft gegen dieselbe Datei.

    make qemu-test SYSTEM=hello

Abgeschottete Kammern

Jeder Teil eines NoWayOS-Systems (der Bildschirm, die Eingabe, das Netzwerk, Ihre Anwendung) läuft in einer eigenen Schutzdomäne auf dem seL4-Mikrokernel. Eine Schutzdomäne hat ihren eigenen Speicher und hält nur die Capabilities, die ihr die Systembeschreibung gewährt: Eine Capability funktioniert wie eine Schlüsselkarte für genau eine Tür. seL4 setzt sie durch, sodass ein Teil nur erreicht, was ihm gegeben wurde, und das System ist so ausgelegt, dass ein Fehler in einem Teil in diesem Teil bleibt.

  • Ein Supervisor empfängt die Fehler der anderen Teile, stoppt den fehlerhaften Teil und startet das System sauber neu. Häufen sich die Fehler, geht das Gerät in einen Fail-safe-Zustand, aus dem es nur ein Kaltstart zurückholt.
  • Eine Watchdog-Schutzdomäne bedient den Hardware-Watchdog nur, solange jeder andere Teil auf seinen Heartbeat antwortet.
  • Rollen begrenzen, was jeder Teil bekommen darf: Der Build lehnt eine Freigabe ab, die die Rolle eines Teils nie haben darf, etwa ein Gerät für einen Teil, der nur zeichnen soll.

Typisierte Nachrichten, kopiert, bevor sie geprüft werden

Schutzdomänen kommunizieren über versionierte Datensätze fester Größe mit explizitem Layout, die über Single-Producer-Ringe im gemeinsamen Speicher laufen. Jeder Datensatz wird aus dem gemeinsamen Speicher kopiert, bevor er geprüft wird, sodass der Absender ihn zwischen Prüfung und Verwendung nicht ändern kann.

Jeder Parser für Eingaben von außen wird gefuzzt und ist so gebaut, dass er nie eine Panic auslöst, und für jeden Nachrichtendecoder gibt es beschränkte Beweise, erstellt mit dem Model Checker Kani.

Ein nativer Bildschirm, und kein Browser

Die Benutzeroberfläche ist ein kleiner deklarativer Kern: Layout, Fokus und Hit-Testing in begrenztem Speicher, gezeichnet mit der Rust-Bibliothek embedded-graphics, und neu gezeichnet wird nur, was sich geändert hat. Text stammt aus Glyphenatlanten, die beim Build vorab gezeichnet werden, sodass das Gerät nie eine Schriftdatei parst. Anwendungen sehen Tastatur-, Zeiger- und Touch-Ereignisse, nie USB oder ein anderes Geräteprotokoll.

Designer können weiter in React arbeiten. Der Screen Compiler wandelt Screens, die in der unterstützten Teilmenge geschrieben sind, beim Build in Rust um und lehnt alles außerhalb dieser Teilmenge ab, statt es näherungsweise umzusetzen.

Was drinsteckt

Bereich Was NoWayOS Ihnen bietet
Laufzeit Muster für Schutzdomänen auf Microkit und rust-sel4; ein Supervisor, der einen fehlerhaften Teil stoppt und das System sauber neu startet, mit einem Fail-safe-Zustand nach wiederholten Fehlern; ein Watchdog
Nachrichten Typisierte Datensätze mit explizitem Wire-Layout und Single-Producer-Ringe im gemeinsamen Speicher
Treiber Display (ramfb von QEMU, der Framebuffer des Raspberry Pi 5); Eingabe (virtio, USB-Tastaturen, -Mäuse und -Tablets); Netzwerk (virtio-net, das Ethernet des Pi 5); USB-Host (xHCI); UART; Timer; der Lüfter des Pi 5
Netzwerk Ein IP-Stack auf smoltcp mit DHCP und TCP, der sich nur mit den Zielen verbindet, die ein System erlaubt; ein TLS-1.3-Client auf rustls und RustCrypto
Zeit und Vertrauen Monotone Zeit und Wall-Clock-Zeit als Typen, die sich nie vermischen; ECDSA-P-256-Signaturprüfungen; die Datensätze signierter Updates; Seeds aus einer Hardware-Zufallsquelle mit Gesundheitstests
Benutzeroberfläche Ein begrenzter deklarativer UI-Kern mit Layout, Fokus und Hit-Testing; ein Renderer auf embedded-graphics; vorab gezeichnete Glyphenatlanten und Icons
Werkzeuge Der Dev-Container; Make-Fragmente, mit denen Produkt-Repositories bauen; die Prüfungen für Freigaben, unsafe, Lizenzen und Geheimnisse; Werkzeuge für SBOM und Release-Nachweise; Runner für QEMU und den Raspberry Pi

Hardware

Wo Seine Rolle
QEMU (AArch64) Jedes System bootet zuerst hier, im Dev-Container, und prüft seine eigene Ausgabe
Raspberry Pi 5 Das günstige Referenzboard, das jeder kaufen kann. Benutzeroberfläche, USB-Eingabe, Timer und Watchdog laufen heute darauf
NXP i.MX8 Die vorgesehene Produktionshardware, mit einem Hardware-Vertrauensanker. Noch nicht unterstützt

NoWayOS wird auf Rechnern mit Apple Silicon (arm64) entwickelt. Auch für x86-64 sind die Pakete des Dev-Images fest versioniert und geprüft, doch dort wurde das Image noch nicht durchgängig gebaut und getestet.

Gebaut auf

NoWayOS steht auf der Arbeit anderer und sagt das auch: seL4, Microkit, rust-sel4, die Netzwerk-Queues des seL4 Device Driver Framework, smoltcp, rustls, RustCrypto und embedded-graphics.