Comment s’assemble un système

Chaque appareil NoWayOS est un système : un ensemble fixe de parties, déclaré avant d’être construit, chacune isolée des autres par seL4. Rien n’est ajouté à l’exécution. Cette page explique les pièces, et comment elles s’assemblent.

Domaines de protection

Un domaine de protection est une partie d’un système : un programme avec sa propre mémoire, qui ne détient que les capacités qui lui sont accordées. Dans seL4, une capacité est un jeton infalsifiable qui désigne un objet du noyau et les permissions détenues sur lui, comme un badge qui n’ouvre qu’une seule porte. Un domaine de protection ne peut toucher à rien que ses capacités ne désignent, et seL4 le fait respecter.

Un système type comporte un domaine de protection par préoccupation : un pilote d’affichage, le chemin des entrées, la pile réseau, l’interface utilisateur, l’application, un timer, un superviseur et un watchdog. Chacun est un petit programme Rust, no_std, qui n’alloue plus rien une fois démarré.

La description du système

La description de système Microkit (systems/NAME.system, un fichier XML) déclare le système entier : chaque domaine de protection avec sa priorité, son budget et sa pile ; chaque région mémoire et qui la mappe ; chaque canal ; chaque interruption.

• Les descriptions nomment des périphériques, jamais des adresses : phys_addr="@NAME". Les adresses proviennent du fichier de la carte dans platforms/, chacune avec sa source, si bien que la même description se construit pour QEMU et pour le Raspberry Pi 5.
• Les canaux relient deux domaines de protection, pour les notifications (des signaux sans données, dont les interruptions) et les appels de procédure protégés (des appels synchrones vers une partie de priorité plus élevée).

La description est la conception de sécurité du système : toute modification de celle-ci est donc examinée comme une modification de sécurité.

Le fichier des droits

À côté de chaque description, systems/NAME.grants liste tout ce que le système accorde, un fait par ligne : priorités, budgets, mémoire, périphériques, interruptions et canaux. La compilation échoue si les deux divergent, dans un sens comme dans l’autre.

Chaque domaine de protection a aussi un rôle (ui, input, broker, display, driver, network, security, storage, update, app, supervisor, watchdog, clock ou test), et la compilation refuse un droit que ce rôle ne doit jamais avoir. Une interface utilisateur ne peut pas recevoir un périphérique réseau par erreur, et un instrument de test ne peut pas se glisser dans un produit.

Messages typés

Les domaines de protection communiquent par des messages typés : des enregistrements versionnés de taille fixe, à la disposition explicite, transmis sur des anneaux à producteur unique et consommateur unique en mémoire partagée.

• Copier, puis vérifier. Un destinataire copie chaque enregistrement hors de la mémoire partagée avant de le valider : l’expéditeur ne peut donc pas le modifier entre la vérification et son utilisation (le bug appelé double lecture, ou double-fetch).
• Les décodeurs ne peuvent pas paniquer. Chaque décodeur renvoie une erreur typée pour toute donnée malformée, et dispose de preuves Kani bornées et d’une cible de fuzzing.
• Chaque côté a sa propre vue. Le producteur et le consommateur voient l’anneau à travers des vues mémoire distinctes, et les indices partagés utilisent les ordres mémoire acquire et release.

Entrées

Les applications voient des événements d’entrée canoniques (touches, mouvements du pointeur et contacts tactiles), vérifiés par rapport à l’écran et limités en débit. Elles ne voient jamais l’USB ni aucun autre protocole de périphérique ; le chemin des entrées les analyse dans ses propres domaines de protection, en traitant chaque octet comme hostile.

Fautes, superviseur et état de repli sûr

Quand un domaine de protection fait quelque chose que seL4 n’autorise pas, ou panique, seL4 l’arrête et signale une faute à son parent.

• Le superviseur est le parent des autres parties. Il reçoit chaque faute, la signale, et réinitialise la carte pour que le système redémarre proprement. Il est construit et testé dans des systèmes de test QEMU.
• L’état de repli sûr est l’état dans lequel passe un appareil quand les fautes s’enchaînent : par défaut, au quatrième redémarrage depuis un démarrage à froid, ou à la deuxième faute dans une partie sensible pour la sécurité, comme le stockage ou les mises à jour. Seuls le superviseur, le watchdog et, si possible, l’affichage continuent de tourner, et seul un démarrage à froid, depuis l’appareil éteint, remet l’appareil en service.
• Le domaine de protection watchdog ne réarme le watchdog matériel que tant que toutes les autres parties répondent à son signal de vie. Si l’une cesse de répondre, le matériel réinitialise la carte.

Mémoire et temps

• La mémoire est fixée à la construction de l’image. Le code de l’appareil n’alloue rien : chaque tampon et chaque file ont une taille fixe, issue de nowayos-bounded. La seule exception, le client TLS, travaille dans une arène fixe qui lui est propre.
• Deux sortes de temps qui ne se mélangent jamais. Le temps monotone compte depuis le démarrage et ne recule jamais ; chaque délai d’expiration l’utilise. Le temps calendaire, la date et l’heure du jour, provient d’une source authentifiée. Ce sont des types Rust différents : on ne peut donc pas passer l’un là où l’autre est attendu.

Construire vos propres systèmes

Les systèmes et les domaines de protection propres à votre produit vivent dans un dépôt à part, à côté de nowayos, jamais à l’intérieur. Le Makefile de ce dépôt définit SYSTEM_REPO := $(CURDIR) et inclut les fragments make de NoWayOS :

SYSTEM_REPO := $(CURDIR)
include ../nowayos/tools/make/container.mk
include ../nowayos/tools/make/system.mk

Ensuite, make image, make qemu-test, make qemu-test-all et les vérifications fonctionnent sur ses systems/ et pds/, avec le conteneur de développement, les fichiers de cartes, les règles de droits et les vérifications de NoWayOS. Les variables sont documentées en tête de tools/make/system.mk. Le Showcase est construit exactement ainsi.