Sécurité

Il ne se mêle que de ses affaires.

Un appareil NoWayOS laisse de côté ce dont sa tâche n’a pas besoin et cloisonne le reste en compartiments. Cette page expose ce sur quoi cela repose, ce qui est prouvé, ce qui ne l’est pas encore, et ce qu’il vous revient de faire correctement.

Ce qui est laissé de côté

Une image NoWayOS contient son application, les pilotes que cette application utilise, et le micronoyau seL4. Il n’y a ni moteur de navigateur, ni système de fenêtrage, ni shell, ni gestionnaire de paquets, ni compte utilisateur : rien de tout cela n’a jamais été intégré, donc rien n’est là pour être exploité, corrigé ou mal configuré. NoWayOS est conçu pour réduire les logiciels et services superflus : si la tâche n’en a pas besoin, ce n’est pas dans l’image.

C’est le sens du nom : aucun moyen d’exploiter ce qui n’a jamais été intégré. C’est un constat sur ce qui est absent, pas la promesse que rien ne peut mal tourner. Ce qui est intégré peut encore contenir des bugs ; ce que nous affirmons, c’est qu’il y a bien moins de code intégré, et qu’un bug reste dans son compartiment.

Verrouiller un système généraliste, c’est être sécurisé par configuration : les fonctions mises sous clé sont toujours présentes, et un seul bug peut contourner tous les réglages. NoWayOS vise à être sécurisé par construction : les fonctions n’ont jamais été là.

Comment une défaillance est confinée

Chaque partie s’exécute dans son propre domaine de protection, avec sa propre mémoire, et ne détient que les capacités que lui accorde la description de son système. seL4 les fait respecter.
Chaque droit est listé dans le fichier des droits du système, et la compilation échoue si la description accorde quoi que ce soit que le fichier ne liste pas, ou l’inverse. Élargir un droit est examiné comme une modification de sécurité.
Les messages entre parties sont des enregistrements de taille fixe, copiés hors de la mémoire partagée avant d’être vérifiés, si bien qu’un expéditeur ne peut pas modifier un enregistrement une fois que celui-ci a été validé.
Toute entrée est hostile jusqu’à vérification. Chaque parseur d’entrées externes est soumis au fuzzing et construit pour ne jamais paniquer, et les applications voient des événements de touche, de pointeur et de toucher, jamais des protocoles de périphériques.
Un superviseur arrête une partie fautive et redémarre le système proprement. Des fautes répétées placent l’appareil dans un état de repli sûr jusqu’à un démarrage à froid.

Ce que couvrent les preuves de seL4, et ce qu’elles ne couvrent pas

seL4 est un micronoyau d’environ 10 000 lignes, doté de preuves de correction et de sécurité vérifiées par machine. Ces preuves sont une réussite rare, et elles valent pour des configurations précises sur des plateformes précises. Voici la position exacte :

NoWayOS tourne sur le micronoyau seL4, qui dispose de preuves de correction et de sécurité vérifiées par machine pour des configurations précises sur notre matériel ; NoWayOS utilise la configuration à criticité mixte de seL4, dont les preuves sont en cours.

Plateforme : la configuration vérifiée AArch64 de seL4 inclut le Raspberry Pi 5 et les i.MX8M Mini, Plus et Quad de NXP.
Ordonnancement : Microkit construit le noyau à criticité mixte (MCS) de seL4, dont les preuves AArch64 sont en cours. Aucune image NoWayOS n’entre donc aujourd’hui dans le périmètre des preuves achevées de seL4.
Cœurs : les preuves portent sur des noyaux monocœurs. Une image qui utilise plusieurs cœurs sort de leur périmètre, et le dit.
Au-dessus du noyau : l’outillage de Microkit, ainsi que les domaines de protection et les pilotes de NoWayOS, ne sont pas couverts par les preuves de seL4. Leur assurance repose sur Rust, l’isolation, la relecture, les tests et les preuves bornées propres à NoWayOS.

Chaque image consigne sa configuration dans un sel4-config.txt placé à côté d’elle. Voici ce que dit d’elle-même le relevé d’une version de développement du système hello :

system: hello
board: qemu_virt_aarch64
configuration: debug
sdk: Microkit 2.3.1
status: development build: a debug kernel, with printing and debug interfaces, outside seL4's proofs
status: outside seL4's completed proofs: a mixed-criticality (MCS) kernel, whose AArch64 proofs are in progress
status: outside seL4's proofs: a platform that is not on seL4's AArch64 verified list

Même une image dont le noyau correspondrait à chaque option de la configuration vérifiée ne serait pas qualifiée de “vérifiée” ici. Le relevé énonce les faits, et les faits suffisent.

Les éléments de preuve, et la commande pour chacun

Chaque affirmation de cette page s’accompagne de ses éléments de preuve, et chacun d’eux provient d’une commande que n’importe qui peut exécuter dans le conteneur de développement. make ci les exécute dans l’ordre, et make ci CI_SCOPE=full exécute toutes les preuves et toutes les cibles de fuzzing ; Vérifications et éléments de preuve explique chacune d’elles.

L’affirmation	Les éléments de preuve	À exécuter
Chaque droit est consigné.	Le fichier des droits de chaque système, vérifié par rapport à la description du système à chaque compilation.	`make qemu-test SYSTEM=hello`
Une partie ne peut pas atteindre ce qui ne lui a pas été accordé.	Des tests d’isolation dont les sondes effectuent des lectures et des écritures non accordées, que seL4 doit arrêter, et une variante dont un droit a été volontairement élargi, qui doit échouer.	`make qemu-test SYSTEM=isolation-test`
Les décodeurs de messages tiennent pour toute entrée jusqu’à une borne.	Des preuves Kani pour chaque décodeur d’enregistrements de messages, avec des tests de mutation qui montrent que les preuves peuvent échouer.	`make kani`
Les parseurs d’entrées externes résistent aux entrées hostiles.	Une cible de fuzzing pour chaque parseur d’entrées non fiables. Un plantage, une fois corrigé, devient un test de non-régression.	`make fuzz`
Le code unsafe ne se trouve que là où il est approuvé.	Une liste d’autorisation des quelques crates et fichiers qui peuvent l’utiliser, imposée par make ci, avec Miri exécuté sur ces crates.	`make unsafe-audit`
Chaque composant est connu.	Une nomenclature logicielle CycloneDX pour chaque espace de travail et chaque image système, chaque composant avec son empreinte.	`make image-sbom SYSTEM=hello`
Les licences et les avis de sécurité sont vérifiés.	cargo-deny sur chaque espace de travail : licences, sources, crates interdites et avis de sécurité connus.	`make deny`
Il n’y a aucun secret dans le code.	L’arborescence et chaque commit analysés, hors ligne, à la recherche de clés et d’identifiants.	`make secrets`
La configuration seL4 de chaque image est consignée.	Un sel4-config.txt à côté de chaque image, et une vérification que les valeurs de référence du relevé correspondent au SDK Microkit figé.	`make sel4-config-check`

Lire les éléments de preuve d’une image

Inutile de construire quoi que ce soit pour voir à quoi ressemblent les éléments de preuve. Les voici au complet pour une image réelle : ui-interactive, l’interface utilisateur cliquable, construite pour QEMU le 1er novembre 2026.

Sa nomenclature logicielle (CycloneDX 1.5) : 62 composants, du noyau seL4 et du chargeur de Microkit jusqu’à chaque crate de chaque domaine de protection, chacun avec son SHA-256.
Le relevé de sa configuration seL4 : le noyau qu’elle exécute, option par option face à la configuration vérifiée de seL4, et clairement là où elle sort du périmètre des preuves.
La description de son système : chaque domaine de protection, région mémoire, interruption et canal, tels que Microkit les construit.
Son fichier des droits : les mêmes droits consignés à raison d’un fait par ligne, que la compilation vérifie par rapport à la description.
L’écran qu’elle dessine, comparé pixel par pixel à cette image approuvée à chaque exécution de son test.

Ce qui reste à votre charge

NoWayOS est une plateforme, pas un produit certifié. Un appareil sécurisé dépend aussi de la façon dont il est déployé et exploité, et cette part revient à qui le construit et l’exploite.

Sécurité physique. Un périphérique branché ou une main sur le câble d’alimentation peuvent toujours mettre un appareil hors service. Les boîtiers, les ports et l’alimentation relèvent de la conception du produit construit sur NoWayOS.
Ce que chaque système accorde. NoWayOS vérifie qu’un système et son fichier des droits concordent. Savoir si ces droits conviennent à la tâche est une décision de conception, et doit être examiné comme telle.
Réseaux et back-ends. Un appareil ne se connecte qu’aux destinations que son système autorise. Ce que ces services font de ce qu’ils reçoivent, c’est à eux de le sécuriser.
Clés et mises à jour. Les mises à jour signées avec retour arrière sûr sont conçues, pas encore réalisées. Qui détient les clés de signature, et comment une version est approuvée, relève d’une décision d’exploitation.
Certification. Les produits réglementés qui fonctionnent sur NoWayOS portent leur propre certification. NoWayOS est conçu pour fournir les éléments de preuve dont ils ont besoin ; il n’est pas certifié lui-même.

Pas encore construit

Le démarrage sécurisé et l’attestation relèvent du matériel de production doté d’une racine de confiance matérielle. Ni l’un ni l’autre n’est construit.
Les mises à jour signées appliquées sur l’appareil. Les enregistrements de mise à jour et leurs vérifications existent ; le chemin qui applique une mise à jour sur un appareil, pas encore.
Le Raspberry Pi 5 est une carte de développement, pas un appareil durci. Quiconque en a un entre les mains peut remplacer son logiciel, et les accès mémoire des périphériques USB n’y sont pas encore confinés.

Les mots que vous ne trouverez pas ici

Nous ne disons pas de NoWayOS qu’il est “impiratable”, “inviolable” ou “à toute épreuve”, et nous ne prétendons pas à une “surface d’attaque nulle”. Rien ne l’est, et vous auriez raison d’arrêter de lire. Les affirmations de cette page sont plus modestes, et chacune s’accompagne de ses éléments de preuve.

Signaler une vulnérabilité

Merci de signaler toute vulnérabilité en privé, via le signalement privé de vulnérabilités de GitHub, dans l’onglet Security du dépôt, ou par e-mail à security@nowayos.com, comme le décrit le SECURITY.md de chaque dépôt, et non dans un ticket public. Comme chaque partie s’exécute dans son propre compartiment, tout est conçu pour qu’une faille reste là où elle se trouve le temps qu’un correctif soit élaboré.