Prüfungen und Nachweise

Was make ci ausführt und was jede Prüfung zeigt, die Grundregeln, die jedes Crate einhält, wie Sie das seL4-Protokoll und die Stückliste eines Images lesen und wie das Gate schnell bleibt.

NoWayOS macht wenige Aussagen und stützt jede mit einer Prüfung, die Sie ausführen können. Diese Seite erklärt, was jede Prüfung zeigt und was nicht.

Ein Befehl für alles

make ci

make ci ist das komplette Gate, der Reihe nach ausgeführt: der Secrets-Scan, Lints, Tests, Dokumentation, die Demo, der no_std-Build, Prüfungen von Lizenzen und Sicherheitshinweisen, die Glyphenatlanten, die Stücklisten, Fuzzing und die Kani-Beweise, dann die Systemprüfungen und QEMU-Boots. Eine Änderung besteht nur, wenn jeder Schritt besteht.

Was jede Prüfung zeigt

Befehl	Was er zeigt
`make test`	Unit-, Property-, Doc- und Golden-Image-Tests: Der Code tut, was seine Tests sagen, und jeder Screen wird genau so gezeichnet wie abgenommen
`make lint`	rustfmt und clippy, mit Warnungen als Fehler
`make nostd`	Jedes Geräte-Crate baut für Bare Metal (`aarch64-unknown-none`), ohne Standardbibliothek
`make deny`	Die Grundlinie, die jeder Workspace einhalten muss, dann cargo-deny: Lizenzen, Quellen, gesperrte Crates und bekannte Sicherheitshinweise
`make secrets`	Der Quellbaum und jeder Commit, offline nach Schlüsseln und Zugangsdaten durchsucht
`make fuzz`	Jedes Fuzz-Target, gebaut mit libFuzzer und gegen generierte Eingaben ausgeführt, je `FUZZ_SECONDS` (10 s) lang
`make kani`	Die beschränkten Beweise von Kani: dass jeder Datensatz-Decoder für jede Eingabe bis zum längsten Datensatz nie eine Panic auslöst, nie überläuft und nie außerhalb der Grenzen liest, mit Mutationsprüfungen, die zeigen, dass jeder Beweis fehlschlagen kann
`make unsafe-audit`	`unsafe`-Code steht nur dort, wo die genehmigte Liste es erlaubt
`make pds-miri`	Miri führt die Tests der Crates aus, die `unsafe` verwenden dürfen, und prüft auf undefiniertes Verhalten
`make sbom`	Eine CycloneDX-Stückliste für jeden Workspace
`make image-sbom SYSTEM=NAME`	Ein Image und seine Stückliste: Kernel, Loader, Monitor und jede Schutzdomäne, mit den Crates darin und ihren Hashes
`make sel4-config-check`	Der dokumentierte Verifikationsstand von seL4 ist der für das fest versionierte Microkit SDK
`make qemu-test-all`	Jedes System bootet in QEMU, in jeder Konfiguration, die es aufführt, und gibt aus, was seine Expect-Datei vorgibt

Beschränkte Beweise sind Beweise bis zu einer festgelegten Eingabegröße, nicht für jede Eingabe, die es je geben könnte. Fuzzing findet Abstürze; es kann nicht zeigen, dass es keine gibt. Tests zeigen die Fälle, die sie testen. Jedes davon lohnt sich für das, was es tatsächlich zeigt.

Die Grundregeln, die jedes Crate einhält

Das sind Lints und Prüfungen in jedem Workspace, keine Richtlinien:

Kein unsafe, außer in einer kurzen, genehmigten Liste von Crates und Dateien, die direkt auf Hardware oder Speicher zugreifen. Ein neuer Eintrag auf dieser Liste braucht eine angegebene Begründung und ein Review.
Keine Panics bei Eingaben von außen: kein unwrap, expect oder panic! in Bibliothekscode, keine ungeprüfte Indizierung oder Arithmetik, und jede Ausnahme von einem Lint nennt ihren Grund.
Geräte-Crates sind no_std und allozieren nichts. Release-Builds behalten die Überlaufprüfungen, und eine Panic stoppt den Teil, statt ihn weiterlaufen zu lassen.
Parser lehnen übergroße Eingaben ab, bevor sie sie kopieren, geben typisierte Fehler zurück und haben Property-Tests und ein Fuzz-Target.
Nirgends Geheimnisse, nicht einmal Entwicklungsschlüssel. Testschlüssel entstehen, wenn ein Test läuft, und werden nie gespeichert.

Die Protokolle eines Images lesen

Jedes Image wird nach build/BOARD/SYSTEM/ geschrieben, mit zwei Protokollen daneben.

sel4-config.txt nennt das Image, seinen Hash, das Board, das Microkit SDK und den Kernel, sagt dann, wo das Image gegenüber den Beweisen von seL4 steht, eine status:-Zeile pro Grund, und listet jede Kerneloption, die darüber entscheidet, neben dem Wert der verifizierten Konfiguration auf. Ein Debug-Kernel ist ein Entwicklungs-Build. Ein Mehrkern- oder Mixed-Criticality-Kernel oder ein Board, das nicht auf der Liste von seL4 steht, liegt außerhalb der Beweise von seL4. Ein Kernel, der jeder Option entspricht, wird trotzdem nie “verifiziert” genannt: Das Protokoll nennt die Fakten und belässt es dabei.

sbom.cdx.json ist die CycloneDX-Software-Stückliste des Images: woraus es besteht, bis hinunter zu jedem Crate in jeder Schutzdomäne, jedes mit seinem sha256.

Das Gate schnell halten

Der volle Satz an Beweisen und Fuzzing braucht lange, daher führt das alltägliche make ci Kani, Fuzzing und Miri nur dort aus, wohin eine Änderung reicht. Es verfolgt die Änderung durch jedes Crate, das davon abhängt, und überspringt jede Prüfung, deren Eingaben sich seit ihrem letzten Bestehen nicht geändert haben. make ci CI_SCOPE=full führt jede davon aus, ohne Cache; make kani, make fuzz und make pds-miri laufen immer vollständig.

Kani ist der hungrigste Schritt: Jeder Beweisjob bekommt etwa 10 GB Arbeitsspeicher, und KANI_JOBS legt fest, wie viele gleichzeitig laufen. Geht make kani der Speicher aus, geben Sie der virtuellen Maschine von Podman mehr, oder setzen Sie KANI_JOBS=1.