Le vocabulaire, en clair.

Une police dessinée à l’avance, à la compilation, sous forme d’images de ses caractères, pour qu’un appareil affiche du texte sans jamais analyser de fichier de police.

Le fait, pour un appareil, de prouver cryptographiquement à un service distant quel logiciel il a démarré. Elle montre ce qui a été chargé au démarrage, pas tout ce qui s’est passé depuis. Prévue pour NoWayOS sur le matériel de production ; pas encore réalisée.

Tout ce qui doit être correct pour qu’une propriété de sécurité tienne. Pour un système NoWayOS : le noyau seL4, le chargeur et le moniteur Microkit, et les domaines de protection sur lesquels repose cette propriété.

Une erreur comme lire au-delà de la fin d’un tampon ou utiliser de la mémoire après sa libération. Microsoft et Google ont chacun indiqué qu’environ 70 % de leurs bugs de sécurité graves sont de ce type ; le Rust sûr les exclut.

Dans Microkit, une connexion déclarée entre deux domaines de protection, pour les notifications (des signaux sans données, dont les interruptions) et les appels de procédure protégés.

Dans seL4, 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 qu’à ce que ses capacités désignent.

L’image de conteneur figée qui contient toute la chaîne d’outils de NoWayOS : les chaînes d’outils Rust, le SDK Microkit, QEMU et les outils de vérification. Chaque cible make s’y exécute, si bien que votre machine n’a besoin que de Podman et de make (et de Python 3.11 pour piloter un Raspberry Pi 5).

La règle selon laquelle un message est copié hors de la mémoire partagée avant d’être validé, pour que l’expéditeur ne puisse pas le modifier entre la vérification et son utilisation. Elle empêche une double lecture.

Un format standard ouvert pour les nomenclatures logicielles. NoWayOS en produit une pour chaque espace de travail et chaque image système. Voir SBOM.

L’adaptateur USB-série de Raspberry Pi. Sur le connecteur de débogage du Raspberry Pi 5, il transporte le journal de démarrage et charge les images de test.

Un démarrage depuis l’appareil éteint, par opposition à une réinitialisation. Seul un démarrage à froid fait sortir un appareil NoWayOS de son état de repli sûr.

Le refus, par un appareil, de démarrer un logiciel qui n’est pas signé par son fabricant. Prévu pour NoWayOS sur le matériel de production ; pas encore réalisé.

Le fichier XML Microkit qui déclare chaque domaine de protection, région mémoire, canal et interruption d’un système. C’est la conception de sécurité du système, et toute modification de ce fichier est examinée comme telle.

Une partie isolée d’un système Microkit : un programme avec sa propre mémoire, qui ne détient que les capacités qui lui sont explicitement accordées. Ce sont les compartiments étanches de NoWayOS.

Un bug dans lequel le code vérifie des données en mémoire partagée puis les relit, ce qui laisse l’autre côté les modifier entre-temps. Empêché par copier, puis vérifier.

Une bibliothèque Rust de graphisme 2D pour les appareils dépourvus de pile graphique fournie par un système d’exploitation. L’interface utilisateur de NoWayOS dessine avec elle.

L’état dans lequel passe un appareil NoWayOS quand les fautes s’enchaînent : seuls le superviseur, le watchdog et, si possible, l’affichage continuent de tourner, jusqu’à un démarrage à froid.

Ce que seL4 signale quand un domaine de protection fait quelque chose que le noyau n’autorise pas, ou panique. La partie reste arrêtée jusqu’à ce que son gestionnaire de fautes agisse.

systems/NAME.grants : tout ce qu’un système accorde, à raison d’un fait par ligne (priorités, budgets, mémoire, périphériques, interruptions et canaux). La compilation échoue si la description du système et le fichier des droits divergent.

systems/NAME.expect : les lignes qu’un système doit afficher, dans l’ordre, et le texte qui fait échouer le test s’il apparaît où que ce soit. Le même fichier vérifie un système dans QEMU et sur le Raspberry Pi 5.

Tester un parseur avec des millions d’entrées générées jusqu’à ce que l’une d’elles le fasse planter ou mette une vérification en défaut. Chaque parseur d’entrées externes de NoWayOS a une cible de fuzzing.

La famille de processeurs Arm industriels de NXP, et le matériel de production visé par NoWayOS. Pas encore pris en charge.

Un vérificateur de modèles (model checker) pour Rust qui prouve des propriétés pour toute entrée jusqu’à une borne. NoWayOS l’utilise pour prouver que ses décodeurs de messages ne paniquent jamais, ne débordent jamais et ne lisent jamais hors limites.

Un enregistrement de taille fixe à la disposition explicite, transmis entre domaines de protection par la mémoire partagée et vérifié à la réception. Voir copier, puis vérifier.

Le framework de la seL4 Foundation pour des systèmes seL4 statiques, construits à partir de domaines de protection déclarés dans une description du système.

Un noyau réduit au strict minimum, les pilotes, le réseau et l’écran s’exécutant en dehors de lui, chacun dans son propre compartiment. seL4 en est un.

Un interpréteur pour Rust qui détecte les comportements indéfinis. NoWayOS l’exécute sur les quelques crates autorisées à contenir du code unsafe.

La configuration de seL4 avec budgets et périodes d’ordonnancement, que Microkit construit. Ses preuves AArch64 sont en cours : aucune image NoWayOS n’entre donc aujourd’hui dans le périmètre des preuves achevées de seL4.

Une preuve qu’une propriété est vraie pour toute entrée jusqu’à une taille donnée. NoWayOS prouve ainsi ses décodeurs de messages, avec Kani.

Un émulateur de machines open source. Chaque système NoWayOS y démarre, et vérifie sa propre sortie, avant de toucher au matériel.

La carte bon marché que NoWayOS utilise comme matériel de référence.

Un langage de programmation dont le code sûr exclut les bugs de sûreté mémoire. Le code propre de NoWayOS est entièrement en Rust.

Le support Rust de la seL4 Foundation, dont la crate qui permet d’écrire des domaines de protection Microkit.

Une bibliothèque TLS écrite en Rust. Le client TLS 1.3 de NoWayOS est construit dessus, avec RustCrypto.

Une nomenclature logicielle (software bill of materials) : la liste de chaque composant d’un logiciel, avec sa version. NoWayOS en produit une au format CycloneDX pour chaque espace de travail et chaque image système.

L’outil de compilation de NoWayOS qui convertit des écrans React, écrits en TSX dans un sous-ensemble pris en charge, en Rust pour l’interface utilisateur de NoWayOS. Il refuse tout ce qui sort du sous-ensemble plutôt que de l’approximer.

Le seL4 Device Driver Framework : une architecture de référence pour les pilotes sur Microkit, fondée sur des files en mémoire partagée. Les files réseau de NoWayOS la suivent.

Rendre un appareil généraliste plus sûr en modifiant ses réglages. Les fonctions sont toujours là, et un seul bug peut contourner tous les réglages.

Construire un appareil incapable de faire les choses risquées, parce qu’elles n’y ont jamais été intégrées. L’approche de NoWayOS.

Un micronoyau d’environ 10 000 lignes, maintenu par la seL4 Foundation, doté de preuves de correction et de sécurité vérifiées par machine pour des configurations précises. NoWayOS tourne dessus.

Le relevé écrit à côté de chaque image NoWayOS : sa configuration seL4, et si cette configuration entre dans le périmètre des preuves achevées de seL4.

Un système d’exploitation construit pour l’unique tâche d’un appareil, au lieu d’être construit pour tout faire tourner puis verrouillé sur une seule chose. Trois traits le définissent : il est construit pour une seule tâche (son image contient l’application, les pilotes qu’elle utilise et le noyau, et rien d’autre) ; il est cloisonné de l’intérieur (chaque partie dans son propre compartiment, n’atteignant que ce qui lui a été accordé) ; et il apporte ses preuves (les éléments de preuve de ce qu’il contient l’accompagnent). Ce n’est pas un mode kiosque, qui verrouille un système sécurisé par configuration sur une seule application. NoWayOS est un Single Purpose OS : un ordinateur qui n’a rien d’autre à faire.

Une pile TCP/IP en Rust qui n’alloue pas de mémoire pendant son fonctionnement. La pile réseau de NoWayOS est construite dessus.

Le domaine de protection qui reçoit les fautes des autres parties, les signale et redémarre le système proprement.

Tout ce qu’un attaquant pourrait tenter d’utiliser contre un appareil : son code, ses services, ses interfaces et ses entrées. Moins de code et moins de fonctions en laissent moins.

La date et l’heure du jour, issues d’une source authentifiée. NoWayOS le tient à l’écart du temps monotone, sous un type différent.

Le temps compté depuis le démarrage, jamais réglé et qui ne recule jamais. Chaque délai d’expiration de NoWayOS l’utilise, et il ne se mélange jamais au temps calendaire.

Un système qui tente d’atteindre ce qui ne lui a pas été accordé, ce que seL4 doit empêcher. Une variante dont un droit a été volontairement élargi doit échouer, ce qui montre que le test peut échouer.

Du code Rust dont le compilateur ne peut pas vérifier la sûreté mémoire. Interdit dans chaque crate NoWayOS, sauf dans une liste courte et relue que les vérifications font respecter.

Une preuve mathématique, vérifiée par ordinateur, qu’un logiciel respecte sa spécification. seL4 en bénéficie pour des configurations précises. Le code propre de NoWayOS repose plutôt sur Rust, l’isolation, les tests et les preuves bornées.

Un timer matériel qui réinitialise la carte si le logiciel ne le réarme pas. Le domaine de protection watchdog de NoWayOS ne le réarme que tant que toutes les autres parties répondent à son signal de vie.