Il primo sistema in QEMU

Avviare seL4 in QEMU con un dominio di protezione in Rust, leggere i tre file che definiscono un sistema, guardare seL4 fermare una parte che si spinge troppo in là e cliccare nell'interfaccia utente.

Un sistema NoWayOS è un insieme di domini di protezione, le parti di un dispositivo, avviati insieme su seL4. Ogni sistema si avvia prima in QEMU, dentro il container di sviluppo, e verifica il proprio output. Questa pagina avvia il più piccolo, poi alcuni che mostrano di più.

Avviare hello

make qemu-test SYSTEM=hello

Questo comando compila il sistema hello, ne verifica le concessioni, avvia seL4 in QEMU senza schermo e osserva ciò che stampa. Il test passa quando sono comparse, in ordine, tutte le righe che il sistema deve stampare, e nessuna di quelle vietate.

Per avviarlo e osservarlo di persona, eseguire make qemu SYSTEM=hello. Per uscire da QEMU: Ctrl-A, poi x.

I tre file che definiscono un sistema

Ogni sistema è composto da tre file in systems/, accanto al codice Rust in pds/.

hello.system è la descrizione di sistema Microkit: ogni dominio di protezione, regione di memoria, canale e interrupt del sistema. hello ha un solo dominio di protezione e nient'altro:

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

hello.grants elenca tutto ciò che il sistema concede, un fatto per riga. La build fallisce se la descrizione concede qualcosa che qui non è elencato, o se qui è elencato qualcosa che la descrizione non concede, così una modifica a ciò che un sistema può fare è sempre visibile in revisione:

system demo
role hello app

pd hello priority=1 budget=1000 period=1000

hello.expect elenca le righe che il sistema deve stampare, in ordine, e, dopo un !, il testo che fa fallire subito il test ovunque compaia:

NOWAYOS: rust pd starting
NOWAYOS: hello from rust

!MON|ERROR
!seL4(CPU
!panicked

Lo stesso file expect verifica il sistema su un Raspberry Pi 5, a partire dal log seriale della scheda.

Il dominio di protezione vero e proprio

pds/hello/src/main.rs è l'intero programma. Segue la forma minima dell'esempio Microkit di rust-sel4: init viene eseguita una volta all'avvio, e l'handler riceverebbe le notifiche se il sistema gli assegnasse dei canali.

#![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;
}

Non c'è heap (qualsiasi allocazione fallirebbe al link), né codice unsafe, né dispositivi. La stampa funziona solo perché si tratta di una build di debug: un kernel di release non ha una console di debug.

Guardare seL4 fermare una parte

make qemu-test SYSTEM=isolation-test

Due domini di protezione sonda tentano ciascuno qualcosa che non è stato loro concesso: uno legge memoria non mappata nel proprio spazio, l'altro scrive su una pagina che può solo leggere. seL4 li ferma entrambi con un guasto, e un dominio spettatore continua a girare indisturbato. L'ultima riga del test lo conferma:

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

Altri sistemi da provare

Sistema	Cosa mostra
`ipc-demo`	Due domini di protezione si scambiano record tipizzati attraverso un ring condiviso; un record malformato viene rifiutato
`timer-demo`	Il dominio di protezione del timer risponde a due client e consegna i loro timeout in ordine di scadenza
`supervisor-test`	Il supervisore riceve un guasto e resetta la scheda, e all'avvio successivo la memoria è di nuovo pulita
`ui-demo`	La sessione scriptata dell'interfaccia utente, con l'hash di ogni frame verificato

Ognuno si esegue con make qemu-test SYSTEM=NAME, oppure tutti i sistemi con make qemu-test-all.

Cliccare nell'interfaccia utente

make qemu SYSTEM=ui-interactive VNC=1

Lo schermo di QEMU viene pubblicato via VNC su localhost:5900 della propria macchina, con una password stampata valida solo per quell'esecuzione. Su macOS, aprire vnc://localhost:5900 (nel Finder: Vai, Connessione al server) e cliccare tra le schermate della demo.

Cosa lascia la build accanto a ogni immagine

In build/BOARD/SYSTEM/ (per questi sistemi, build/qemu_virt_aarch64/hello/ e così via), accanto a loader.img:

sel4-config.txt: la configurazione seL4 dell'immagine, e se rientra nelle dimostrazioni di seL4. Una build di debug dichiara chiaramente di no. Vedi Sicurezza.
sbom.cdx.json: una distinta base del software CycloneDX per l'immagine: il kernel, il loader, ogni dominio di protezione e i crate che contiene, ciascuno con il suo hash.
I file di licenza di ciò che l'immagine contiene, come le licenze del font e delle icone.