Ihr erstes System in QEMU

Booten Sie seL4 in QEMU mit einer Rust-Schutzdomäne, lesen Sie die drei Dateien, die ein System definieren, sehen Sie zu, wie seL4 einen Teil stoppt, der zu weit greift, und klicken Sie sich durch die Benutzeroberfläche.

Ein NoWayOS-System ist eine Menge von Schutzdomänen, den Teilen eines Geräts, die gemeinsam auf seL4 booten. Jedes System bootet zuerst in QEMU, im Dev-Container, und prüft seine eigene Ausgabe. Diese Seite bootet das kleinste, dann ein paar, die mehr zeigen.

hello booten

make qemu-test SYSTEM=hello

Das baut das System hello, prüft seine Freigaben, bootet seL4 ohne Bildschirm in QEMU und beobachtet, was es ausgibt. Der Test ist bestanden, wenn jede Zeile, die das System ausgeben muss, in der richtigen Reihenfolge erschienen ist und nichts Verbotenes.

Um es selbst zu booten und zuzusehen, führen Sie make qemu SYSTEM=hello aus. Beenden Sie QEMU mit Ctrl-A, dann x.

Die drei Dateien, die ein System definieren

Jedes System besteht aus drei Dateien in systems/, neben dem Rust-Code in pds/.

hello.system ist die Microkit-Systembeschreibung: jede Schutzdomäne, jeder Speicherbereich, jeder Kanal und jeder Interrupt, den das System hat. hello hat eine Schutzdomäne und sonst nichts:

<system>
 <protection_domain name="hello" priority="1" stack_size="0x10000">
 <program_image path="nowayos-hello.elf" />
 </protection_domain>
</system>

hello.grants listet alles auf, was das System freigibt, ein Fakt pro Zeile. Der Build schlägt fehl, wenn die Beschreibung etwas gewährt, das hier nicht steht, oder wenn hier etwas steht, das sie nicht gewährt; so ist eine Änderung daran, was ein System darf, im Review immer sichtbar:

system demo
role hello app

pd hello priority=1 budget=1000 period=1000

hello.expect listet die Zeilen auf, die das System in der richtigen Reihenfolge ausgeben muss, und, nach einem !, Text, der den Test sofort scheitern lässt, wo immer er auftaucht:

NOWAYOS: rust pd starting
NOWAYOS: hello from rust

!MON|ERROR
!seL4(CPU
!panicked

Dieselbe Expect-Datei prüft das System auf einem Raspberry Pi 5, anhand des seriellen Logs des Boards.

Die Schutzdomäne selbst

pds/hello/src/main.rs ist das ganze Programm. Es folgt der minimalen Form des Microkit-Beispiels von rust-sel4: init läuft einmal beim Start, und der Handler würde Benachrichtigungen empfangen, wenn das System ihm Kanäle gäbe.

#![no_std]
#![no_main]

use sel4_microkit::{Handler, Infallible, debug_println, protection_domain};

#[protection_domain]
fn init() -> HelloPd {
 debug_println!("NOWAYOS: rust pd starting");
 debug_println!("NOWAYOS: hello from rust");
 HelloPd
}

struct HelloPd;

impl Handler for HelloPd {
 type Error = Infallible;
}

Es gibt keinen Heap (jede Allokation würde schon beim Linken scheitern), kein unsafe und kein Gerät. Die Ausgabe funktioniert nur, weil dies ein Debug-Build ist: Ein Release-Kernel hat keine Debug-Konsole.

Zusehen, wie seL4 einen Teil stoppt

make qemu-test SYSTEM=isolation-test

Zwei Sonden-Schutzdomänen versuchen jeweils etwas, das ihnen nicht freigegeben wurde: Die eine liest Speicher, der nicht in ihren Adressraum eingeblendet ist, die andere schreibt auf eine Seite, die sie nur lesen darf. seL4 stoppt jede mit einem Fault, und eine unbeteiligte Schutzdomäne läuft unberührt weiter. Die letzte Zeile des Tests sagt es:

NOWAYOS: isolation-test: 2 of 2 forbidden accesses faulted and were contained; bystander still running

Weitere Systeme zum Ausprobieren

System	Was es zeigt
`ipc-demo`	Zwei Schutzdomänen tauschen typisierte Datensätze über einen gemeinsamen Ring aus; ein fehlerhafter Datensatz wird abgelehnt
`timer-demo`	Die Timer-Schutzdomäne bedient zwei Clients und liefert ihre Timeouts in der Reihenfolge ihrer Fristen aus
`supervisor-test`	Der Supervisor empfängt einen Fault und setzt das Board zurück, und der nächste Boot findet seinen Speicher frisch vor
`ui-demo`	Die gescriptete Sitzung der Benutzeroberfläche, mit einem geprüften Hash für jedes Frame

Starten Sie jedes davon mit make qemu-test SYSTEM=NAME, oder alle Systeme mit make qemu-test-all.

Durch die Benutzeroberfläche klicken

make qemu SYSTEM=ui-interactive VNC=1

Der Bildschirm von QEMU wird per VNC auf localhost:5900 Ihres Rechners bereitgestellt, mit einem Passwort, das nur für diesen Lauf ausgegeben wird. Öffnen Sie unter macOS vnc://localhost:5900 (im Finder: Gehe zu, Mit Server verbinden) und klicken Sie sich durch die Demo-Screens.

Was der Build neben jedem Image hinterlässt

In build/BOARD/SYSTEM/ (hier also build/qemu_virt_aarch64/hello/ und so weiter), neben loader.img:

sel4-config.txt: die seL4-Konfiguration des Images und ob es innerhalb der Beweise von seL4 liegt. Ein Debug-Build sagt klar, dass er das nicht tut. Siehe Sicherheit.
sbom.cdx.json: eine CycloneDX-Software-Stückliste für das Image: der Kernel, der Loader, jede Schutzdomäne und die Crates darin, jeweils mit ihrem Hash.
Die Lizenzdateien dessen, was das Image enthält, etwa die Lizenzen der Schrift und der Icons.