Sicherheit

Es kümmert sich nur um seine Sache.

Ein NoWayOS-Gerät lässt weg, was seine Aufgabe nicht braucht, und schottet den Rest in Kammern ab. Diese Seite legt dar, worauf das beruht, was bewiesen ist, was noch nicht, und was Sie selbst richtig machen müssen.

Was weggelassen wird

Ein NoWayOS-Image enthält seine Anwendung, die Treiber, die diese Anwendung nutzt, und den seL4-Mikrokernel. Es gibt keine Browser-Engine, kein Fenstersystem, keine Shell, keinen Paketmanager und kein Benutzerkonto: Nichts davon wurde je eingebaut, also ist nichts davon da, um ausgenutzt, gepatcht oder falsch konfiguriert zu werden. NoWayOS ist darauf ausgelegt, unnötige Software und Dienste zu reduzieren: Wenn die Aufgabe es nicht braucht, ist es nicht im Image.

Das ist die Bedeutung des Namens: Es gibt keinen Weg, auszunutzen, was nie eingebaut wurde. Das ist eine Aussage darüber, was fehlt, kein Versprechen, dass nichts schiefgehen kann. Was eingebaut ist, kann immer noch Fehler haben; unsere Aussagen lauten: Davon gibt es viel weniger, und ein Fehler bleibt in seiner Kammer.

Ein Allzwecksystem abzuriegeln heißt sicher durch Konfiguration: Die weggesperrten Funktionen sind weiterhin vorhanden, und ein einziger Fehler kann jede Einstellung umgehen. NoWayOS will sicher durch Konstruktion sein: Die Funktionen waren nie da.

Wie ein Fehler eingedämmt wird

Jeder Teil läuft in seiner eigenen Schutzdomäne, mit eigenem Speicher, und hält nur die Capabilities, die ihm seine Systembeschreibung gewährt. seL4 setzt sie durch.
Jede Freigabe steht in der Freigabedatei des Systems, und der Build schlägt fehl, wenn die Beschreibung etwas gewährt, das die Datei nicht auflistet, oder umgekehrt. Eine Freigabe zu erweitern wird als Sicherheitsänderung geprüft.
Nachrichten zwischen Teilen sind Datensätze fester Größe, die aus dem gemeinsamen Speicher kopiert werden, bevor sie geprüft werden, sodass ein Absender einen Datensatz nicht mehr ändern kann, nachdem er die Prüfung bestanden hat.
Eingaben gelten als feindselig, bis sie geprüft sind. Jeder Parser für Eingaben von außen wird gefuzzt und ist so gebaut, dass er nie eine Panic auslöst, und Anwendungen sehen Tastatur-, Zeiger- und Touch-Ereignisse, nie Geräteprotokolle.
Ein Supervisor stoppt einen Teil, der einen Fehler auslöst, und startet das System sauber neu. Wiederholte Fehler versetzen das Gerät in einen Fail-safe-Zustand, bis zu einem Kaltstart.

Was die Beweise von seL4 abdecken und was nicht

seL4 ist ein Mikrokernel mit rund 10.000 Zeilen und maschinengeprüften Beweisen für Korrektheit und Sicherheit. Diese Beweise sind eine seltene Leistung, und sie gelten für bestimmte Konfigurationen auf bestimmten Plattformen. So ist der genaue Stand:

NoWayOS läuft auf dem seL4-Mikrokernel, der maschinengeprüfte Beweise für Korrektheit und Sicherheit für bestimmte Konfigurationen auf unserer Hardware hat; NoWayOS nutzt die Mixed-Criticality-Konfiguration von seL4, deren Beweise noch in Arbeit sind.

Plattform: Die verifizierte AArch64-Konfiguration von seL4 nennt den Raspberry Pi 5 sowie die i.MX8M Mini, Plus und Quad von NXP.
Scheduling: Microkit baut den Mixed-Criticality-Kernel (MCS) von seL4, dessen AArch64-Beweise noch in Arbeit sind. Daher liegt heute kein NoWayOS-Image innerhalb der abgeschlossenen Beweise von seL4.
Kerne: Die Beweise gelten für Single-Core-Kernel. Ein Image, das mehrere Kerne nutzt, liegt außerhalb davon und sagt das auch.
Oberhalb des Kernels: Die Werkzeuge von Microkit sowie die Schutzdomänen und Treiber von NoWayOS sind von den Beweisen von seL4 nicht abgedeckt. Ihre Vertrauenswürdigkeit stützt sich auf Rust, Isolation, Reviews, Tests und die eigenen beschränkten Beweise von NoWayOS.

Jedes Image hält seine Konfiguration in einer sel4-config.txt direkt daneben fest. Das sagt das Protokoll eines Entwicklungs-Builds des Systems hello über sich selbst:

system: hello
board: qemu_virt_aarch64
configuration: debug
sdk: Microkit 2.3.1
status: development build: a debug kernel, with printing and debug interfaces, outside seL4's proofs
status: outside seL4's completed proofs: a mixed-criticality (MCS) kernel, whose AArch64 proofs are in progress
status: outside seL4's proofs: a platform that is not on seL4's AArch64 verified list

Selbst ein Image, dessen Kernel jeder Option der verifizierten Konfiguration entspräche, würde hier nicht “verifiziert” genannt. Das Protokoll nennt die Fakten, und die Fakten genügen.

Die Nachweise und der Befehl für jeden

Jede Aussage auf dieser Seite kommt mit ihrem Nachweis, und jeder Nachweis stammt aus einem Befehl, den jeder im Dev-Container ausführen kann. make ci führt sie der Reihe nach aus, und make ci CI_SCOPE=full führt jeden Beweis und jedes Fuzz-Target aus; Prüfungen und Nachweise erklärt jeden einzelnen.

Die Aussage	Der Nachweis	Selbst ausführen
Jede Freigabe ist schriftlich festgehalten.	Die Freigabedatei jedes Systems, bei jedem Build gegen seine Systembeschreibung geprüft.	`make qemu-test SYSTEM=hello`
Ein Teil erreicht nicht, was ihm nicht freigegeben wurde.	Isolationstests, deren Sonden nicht freigegebene Lese- und Schreibzugriffe versuchen, die seL4 stoppen muss, und eine Variante mit absichtlich erweiterter Freigabe, die fehlschlagen muss.	`make qemu-test SYSTEM=isolation-test`
Nachrichtendecoder halten jeder Eingabe bis zu einer Schranke stand.	Kani-Beweise für jeden Decoder von Nachrichtendatensätzen, mit Mutationsprüfungen, die zeigen, dass die Beweise fehlschlagen können.	`make kani`
Parser für Eingaben von außen überstehen feindselige Eingaben.	Ein Fuzz-Target für jeden Parser nicht vertrauenswürdiger Eingaben. Ein Absturz wird, sobald behoben, zum Regressionstest.	`make fuzz`
Unsafe-Code steht nur dort, wo er genehmigt ist.	Eine Allow-List der wenigen Crates und Dateien, die ihn verwenden dürfen, durchgesetzt von make ci, und Miri läuft über diese Crates.	`make unsafe-audit`
Jede Komponente ist bekannt.	Eine CycloneDX-Software-Stückliste für jeden Workspace und jedes System-Image, jede Komponente mit ihrem Hash.	`make image-sbom SYSTEM=hello`
Lizenzen und Sicherheitshinweise werden geprüft.	cargo-deny über jeden Workspace: Lizenzen, Quellen, gesperrte Crates und bekannte Sicherheitshinweise.	`make deny`
Der Code enthält keine Geheimnisse.	Der Quellbaum und jeder Commit, offline nach Schlüsseln und Zugangsdaten durchsucht.	`make secrets`
Die seL4-Konfiguration jedes Images ist dokumentiert.	Eine sel4-config.txt neben jedem Image und eine Prüfung, dass die Referenzwerte dieses Protokolls zum fest versionierten Microkit SDK passen.	`make sel4-config-check`

Die Nachweise eines Images lesen

Sie müssen nichts bauen, um zu sehen, wie die Nachweise aussehen. Hier sind alle für ein echtes Image: ui-interactive, die klickbare Benutzeroberfläche, gebaut für QEMU am 1. November 2026.

Seine Software-Stückliste (CycloneDX 1.5): 62 Teile, vom seL4-Kernel und dem Loader von Microkit bis zu jedem Crate in jeder Schutzdomäne, jedes mit seinem SHA-256.
Sein seL4-Konfigurationsprotokoll: der Kernel, auf dem es läuft, Option für Option abgeglichen mit der verifizierten Konfiguration von seL4, und klar benannt, wo es außerhalb der Beweise liegt.
Seine Systembeschreibung: jede Schutzdomäne, jeder Speicherbereich, jeder Interrupt und jeder Kanal, so wie Microkit sie baut.
Seine Freigabedatei: dieselben Freigaben, festgehalten als ein Fakt pro Zeile, die der Build gegen die Beschreibung prüft.
Der Bildschirm, den es zeichnet, bei jedem Testlauf Pixel für Pixel mit diesem abgenommenen Bild verglichen.

Was Ihre Sache bleibt

NoWayOS ist eine Plattform, kein zertifiziertes Produkt. Ein sicheres Gerät hängt auch davon ab, wie es eingesetzt und betrieben wird, und dieser Teil liegt bei denen, die es bauen und betreiben.

Physische Sicherheit. Ein eingestecktes Gerät oder eine Hand am Stromkabel kann ein Gerät immer noch außer Betrieb setzen. Gehäuse, Anschlüsse und Stromversorgung gehören zum Design des Produkts, das auf NoWayOS gebaut wird.
Was jedes System freigibt. NoWayOS prüft, dass ein System und seine Freigabedatei übereinstimmen. Ob diese Freigaben für die Aufgabe richtig sind, ist eine Designentscheidung und sollte auch als solche geprüft werden.
Netze und Backends. Ein Gerät verbindet sich nur mit den Zielen, die sein System erlaubt. Was diese Dienste mit dem anfangen, was sie empfangen, müssen sie selbst absichern.
Schlüssel und Updates. Signierte Updates mit sicherem Rückfall sind entworfen, aber noch nicht gebaut. Wer die Signaturschlüssel hält und wie ein Release freigegeben wird, ist eine Entscheidung des Betriebs.
Zertifizierung. Regulierte Produkte, die auf NoWayOS laufen, tragen ihre eigene Zertifizierung. NoWayOS ist darauf ausgelegt, die Nachweise zu liefern, die sie brauchen; es ist selbst nicht zertifiziert.

Noch nicht gebaut

Secure Boot und Attestierung gehören zu Produktionshardware mit einem Hardware-Vertrauensanker. Beides ist noch nicht gebaut.
Signierte Updates, die auf dem Gerät eingespielt werden. Die Update-Datensätze und ihre Prüfungen gibt es; den Weg, der ein Update auf einem Gerät einspielt, noch nicht.
Der Raspberry Pi 5 ist ein Entwicklungsboard, kein gehärtetes Gerät. Wer eines in der Hand hat, kann seine Software austauschen, und der Speicherzugriff von USB-Geräten ist darauf noch nicht eingegrenzt.

Wörter, die Sie hier nicht finden

Wir nennen NoWayOS nicht “unhackbar”, “manipulationssicher” oder “kugelsicher”, und wir behaupten keine “Null-Angriffsfläche”. So etwas gibt es nicht, und Sie hätten recht, an dieser Stelle aufzuhören zu lesen. Die Aussagen auf dieser Seite sind kleiner als das, und jede kommt mit ihrem Nachweis.

Eine Schwachstelle melden

Bitte melden Sie eine Schwachstelle vertraulich, über die private Schwachstellenmeldung von GitHub im Security-Tab des Repositorys oder per E-Mail an security@nowayos.com, wie es die SECURITY.md jedes Repositorys beschreibt, und nicht in einem öffentlichen Issue. Weil jeder Teil in seiner eigenen Kammer läuft, ist das System so ausgelegt, dass ein Fehler dort bleibt, wo er ist, während eine Korrektur entsteht.