13 novembre 2026
Nous attaquons notre propre build à chaque modification
Un test de sécurité qui ne peut pas échouer ne prouve rien. Les tests de NoWayOS viennent donc avec des variantes faites pour échouer, et ses contrôles vivent là où une pull request ne peut pas les atteindre.
Voici une question gênante pour tout test de sécurité : a-t-il déjà échoué ? Un test qui n’a jamais échoué réussit peut-être parce que le système est sain, ou parce que le test ne voit rien du tout. De l’extérieur, les deux se ressemblent trait pour trait.
NoWayOS ne se contente donc pas de tester sa sécurité. Il l’attaque, à chaque modification, et vérifie que les attaques sont arrêtées.
Tendre la main vers ce qui n’est pas à soi
Chaque partie d’un système NoWayOS tourne dans son propre compartiment sur seL4, et ne détient que ce qui lui a été accordé. Les tests d’isolation envoient exprès des sondes à travers ces frontières. L’une lit une adresse qu’on ne lui a jamais donnée. Une autre écrit sur une page qu’elle ne peut que lire. Une autre, qui détient exactement ce que détient l’interface utilisateur, tente d’écrire sur la page de contrôle de l’écran, que l’interface ne peut que lire. Une autre encore, qui détient exactement ce que détient le client réseau, tente d’écrire dans la mémoire du pilote réseau.
seL4 doit les arrêter toutes, et une partie témoin doit continuer de tourner, intacte.
Un test fait pour échouer
Vient ensuite le retournement. À côté du test d’isolation de l’interface utilisateur se trouve une variante dont un droit a été élargi exprès : la doublure de l’interface reçoit la page privée de l’écran. Le test de cette variante doit échouer. S’il réussissait un jour, le test d’isolation serait aveugle, et la compilation le dirait.
La même idée traverse le reste des contrôles. Chaque décodeur des messages entre parties a des preuves bornées, issues du vérificateur de modèles Kani, établissant qu’il ne panique jamais, ne déborde jamais et ne lit jamais hors limites. Des contrôles par mutation cassent ensuite les décodeurs exprès, pour montrer que les preuves le remarquent. Chaque analyseur d’entrées venues de l’extérieur est soumis au fuzzing avec des données hostiles.
Tout cela fait partie de make ci, le contrôle que chaque modification doit franchir. Les tests d’isolation tournent à chaque fois ; une preuve ou une campagne de fuzzing est rejouée dès que le code qu’elle couvre change.
Un test fait pour échouer
Le testLa sonde tend la main vers une page qui ne lui a jamais été accordée. seL4 l’arrête, et le test réussit.
La varianteUn droit est élargi exprès. La sonde passe, donc ce test doit échouer. S’il réussissait un jour, le premier test serait aveugle.
Des contrôles hors de portée
Un contrôle ne vaut que par la main qui peut le modifier. Les contrôles que chaque contribution à NoWayOS doit franchir sont donc définis dans Defence Agent, un dépôt public à part. Une pull request qui touche à un contrôle est signalée au mainteneur.
Defence Agent se teste lui-même de la même façon : vingt pull requests piégées, chacune cachant quelque chose qu’un relecteur pourrait manquer. Il y a du texte caché écrit de droite à gauche dans un commentaire, une lettre remplacée par son sosie cyrillique, une dépendance récupérée directement depuis un dépôt git, un workflow qui exécuterait du code non fiable. Chacune doit être arrêtée, tandis que trois vraies modifications passées doivent passer.
Des preuves, pas des adjectifs
Rien de tout cela ne rend un appareil “impiratable”. Rien ne le fait, et nous ne le dirons jamais. Ce que vous obtenez, ce sont des éléments de preuve : la trace de ce qui a été tenté, de ce qui a été arrêté, et la commande qui le montre. Lisez les éléments de preuve d’une image réelle, ou les contrôles eux-mêmes.