Votre premier système dans QEMU

Démarrez seL4 dans QEMU avec un domaine de protection en Rust, lisez les trois fichiers qui définissent un système, regardez seL4 arrêter une partie qui va trop loin, et cliquez dans l’interface utilisateur.

Un système NoWayOS est un ensemble de domaines de protection, les parties d’un appareil, démarrés ensemble sur seL4. Chaque système démarre d’abord dans QEMU, dans le conteneur de développement, et vérifie sa propre sortie. Cette page démarre le plus petit, puis quelques autres qui en montrent davantage.

Démarrer hello

make qemu-test SYSTEM=hello

Cette commande construit le système hello, vérifie ses droits, démarre seL4 sans affichage dans QEMU et surveille ce qu’il affiche. Le test réussit quand chaque ligne que le système doit afficher est apparue, dans l’ordre, et que rien d’interdit n’est apparu.

Pour le démarrer vous-même et le regarder, lancez make qemu SYSTEM=hello. Quittez QEMU avec Ctrl-A, puis x.

Les trois fichiers qui définissent un système

Chaque système tient en trois fichiers dans systems/, à côté du code Rust dans pds/.

hello.system est la description de système Microkit : chaque domaine de protection, région mémoire, canal et interruption du système. hello a un seul domaine de protection, et rien d’autre :

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

hello.grants liste tout ce que le système accorde, un fait par ligne. La compilation échoue si la description accorde quoi que ce soit qui n’est pas listé ici, ou si le fichier liste quoi que ce soit qu’elle n’accorde pas : toute modification de ce qu’un système a le droit de faire reste ainsi visible en relecture.

system demo
role hello app

pd hello priority=1 budget=1000 period=1000

hello.expect liste les lignes que le système doit afficher, dans l’ordre, puis, après un !, le texte qui fait échouer le test immédiatement, où qu’il apparaisse :

NOWAYOS: rust pd starting
NOWAYOS: hello from rust

!MON|ERROR
!seL4(CPU
!panicked

Le même fichier expect vérifie le système sur un Raspberry Pi 5, à partir du journal série de la carte.

Le domaine de protection lui-même

pds/hello/src/main.rs est le programme entier. Il suit la forme minimale de l’exemple Microkit de rust-sel4 : init s’exécute une fois au démarrage, et le gestionnaire recevrait des notifications si le système lui donnait des canaux.

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

Il n’y a pas de tas (toute allocation échouerait à l’édition de liens), pas d’unsafe et pas de périphérique. L’affichage ne fonctionne que parce qu’il s’agit d’une version de débogage : un noyau compilé en release n’a pas de console de débogage.

Regarder seL4 arrêter une partie

make qemu-test SYSTEM=isolation-test

Deux domaines de protection sondes tentent chacun quelque chose qui ne leur a pas été accordé : l’un lit de la mémoire qui n’est pas mappée chez lui, l’autre écrit dans une page qu’il a seulement le droit de lire. seL4 arrête chacun d’eux sur une faute, et un témoin continue de tourner sans être affecté. La dernière ligne du test le confirme :

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

D’autres systèmes à essayer

Système	Ce qu’il montre
`ipc-demo`	Deux domaines de protection échangent des enregistrements typés par un anneau partagé ; un enregistrement malformé est refusé
`timer-demo`	Le domaine de protection timer répond à deux clients et déclenche leurs délais d’expiration dans l’ordre des échéances
`supervisor-test`	Le superviseur reçoit une faute et réinitialise la carte, et au démarrage suivant, la mémoire est vierge
`ui-demo`	La session scriptée de l’interface utilisateur, avec une empreinte de chaque image vérifiée

Lancez n’importe lequel avec make qemu-test SYSTEM=NAME, ou tous les systèmes avec make qemu-test-all.

Cliquer dans l’interface utilisateur

make qemu SYSTEM=ui-interactive VNC=1

L’écran de QEMU est publié en VNC sur le localhost:5900 de votre machine, avec un mot de passe affiché pour cette exécution seulement. Sur macOS, ouvrez vnc://localhost:5900 (dans le Finder : Aller, Se connecter au serveur) et cliquez dans les écrans de démo.

Ce que la compilation laisse à côté de chaque image

Dans build/BOARD/SYSTEM/ (pour ceux-ci, build/qemu_virt_aarch64/hello/ et ainsi de suite), à côté de loader.img :

sel4-config.txt : la configuration seL4 de l’image, et si elle entre dans le périmètre des preuves de seL4. Une version de débogage indique clairement que non. Voir Sécurité.
sbom.cdx.json : une nomenclature logicielle CycloneDX pour l’image : le noyau, le chargeur, chaque domaine de protection et les crates qu’il contient, chacun avec son empreinte.
Les fichiers de licence de ce que contient l’image, comme les licences de la police et des icônes.