Tout part de la tâche.

De l’application à l’image

Un appareil NoWayOS se construit, il ne se configure pas. Quatre étapes mènent votre code jusqu’à un appareil qui accomplit son unique tâche, et chacune laisse derrière elle quelque chose que vous pouvez vérifier.

Des compartiments étanches

Chaque partie d’un système NoWayOS (l’écran, les entrées, le réseau, votre application) s’exécute dans un domaine de protection qui lui est propre, sur le micronoyau seL4. Un domaine de protection a sa propre mémoire et ne détient que les capacités que lui accorde la description de son système : une capacité fonctionne comme un badge qui n’ouvre qu’une seule porte. seL4 les fait respecter : une partie n’atteint donc que ce qui lui a été donné, et tout est conçu pour qu’un bug dans une partie reste dans cette partie.

• Un superviseur reçoit les fautes des autres parties, arrête la partie fautive et redémarre le système proprement. Quand les fautes s’enchaînent, l’appareil passe dans un état de repli sûr, et seul un démarrage à froid l’en fait sortir.
• Un domaine de protection watchdog ne réarme le watchdog matériel que tant que toutes les autres parties répondent à son signal de vie.
• Des rôles limitent ce que chaque partie peut recevoir : la compilation refuse un droit que le rôle d’une partie ne doit jamais avoir, comme un périphérique pour une partie qui ne doit que dessiner.

Des messages typés, copiés avant d’être vérifiés

Les domaines de protection communiquent par des enregistrements versionnés de taille fixe, à la disposition explicite, transmis sur des anneaux à producteur unique en mémoire partagée. Chaque enregistrement est copié hors de la mémoire partagée avant d’être vérifié : l’expéditeur ne peut donc pas le modifier entre la vérification et son utilisation.

Chaque parseur d’entrées externes est soumis au fuzzing et construit pour ne jamais paniquer, et chaque décodeur de messages dispose de preuves bornées, établies avec le vérificateur de modèles Kani.

Un écran natif, et pas de navigateur

L’interface utilisateur repose sur un petit cœur déclaratif : mise en page, focus et détection des clics en mémoire bornée, le tout dessiné avec la bibliothèque Rust embedded-graphics, en ne redessinant que ce qui a changé. Le texte provient d’atlas de glyphes dessinés à l’avance, à la compilation, si bien que l’appareil n’analyse jamais de fichier de police. Les applications voient des événements de touche, de pointeur et de toucher, jamais l’USB ni aucun autre protocole de périphérique.

Les designers peuvent continuer à travailler en React. Le Screen Compiler convertit en Rust, à la compilation, les écrans écrits dans le sous-ensemble qu’il prend en charge, et refuse tout ce qui sort de ce sous-ensemble plutôt que de l’approximer.

Ce qu’il contient

Matériel

NoWayOS est développé sur des machines Apple silicon (arm64). Sur x86-64, les paquets de l’image de développement sont eux aussi figés et relus, mais l’image n’y a pas encore été construite et testée de bout en bout.

Bâti sur

NoWayOS s’appuie sur le travail d’autres personnes, et le dit : seL4, Microkit, rust-sel4, les files réseau du seL4 Device Driver Framework, smoltcp, rustls, RustCrypto et embedded-graphics.