Vérifications et éléments de preuve

Ce qu’exécute make ci et ce que montre chaque vérification, les règles de base que respecte chaque crate, comment lire le relevé seL4 et la nomenclature d’une image, et comment le contrôle reste rapide.

NoWayOS fait peu d’affirmations, et étaye chacune d’elles par une vérification que vous pouvez exécuter. Cette page explique ce que montre chaque vérification, et ce qu’elle ne montre pas.

Une seule commande pour tout

make ci

make ci est le contrôle complet, exécuté dans l’ordre : l’analyse des secrets, les lints, les tests, la documentation, la démo, la compilation no_std, les vérifications de licences et d’avis de sécurité, les atlas de glyphes, les nomenclatures, le fuzzing et les preuves Kani, puis les vérifications des systèmes et les démarrages QEMU. Une modification ne passe que si chaque étape passe.

Ce que montre chaque vérification

Commande	Ce qu’elle montre
`make test`	Tests unitaires, de propriétés, de documentation et d’images de référence : le code fait ce que disent ses tests, et chaque écran se dessine exactement comme il a été approuvé
`make lint`	rustfmt et clippy, avec les avertissements traités comme des erreurs
`make nostd`	Chaque crate d’appareil se compile pour du bare metal (`aarch64-unknown-none`), sans bibliothèque standard
`make deny`	Le socle que chaque espace de travail doit respecter, puis cargo-deny : licences, sources, crates interdites et avis de sécurité connus
`make secrets`	L’arborescence et chaque commit, analysés hors ligne à la recherche de clés et d’identifiants
`make fuzz`	Chaque cible de fuzzing, construite avec libFuzzer et exécutée sur des entrées générées, pendant `FUZZ_SECONDS` (10 s) chacune
`make kani`	Les preuves bornées de Kani : chaque décodeur d’enregistrement ne panique jamais, ne déborde jamais et ne lit jamais hors limites, pour toute entrée jusqu’à la taille du plus long enregistrement, avec des tests de mutation qui montrent que chaque preuve peut échouer
`make unsafe-audit`	Le code `unsafe` n’apparaît que là où la liste approuvée l’autorise
`make pds-miri`	Miri exécute les tests des crates autorisées à contenir du code `unsafe`, à la recherche de comportements indéfinis
`make sbom`	Une nomenclature CycloneDX pour chaque espace de travail
`make image-sbom SYSTEM=NAME`	Une image et sa nomenclature : noyau, chargeur, moniteur et chaque domaine de protection, avec les crates de chacun et leurs empreintes
`make sel4-config-check`	La position de vérification seL4 consignée est bien celle du SDK Microkit figé
`make qemu-test-all`	Chaque système démarre dans QEMU, dans chaque configuration qu’il liste, et affiche ce que dit son fichier expect

Les preuves bornées sont des preuves jusqu’à une taille d’entrée donnée, pas pour toutes les entrées imaginables. Le fuzzing trouve des plantages ; il ne peut pas montrer qu’il n’y en a aucun. Les tests montrent les cas qu’ils testent. Chacun vaut d’être là pour ce qu’il montre.

Les règles de base que respecte chaque crate

Ce sont des lints et des vérifications dans chaque espace de travail, pas des recommandations :

Pas d’unsafe, sauf dans une liste courte et approuvée de crates et de fichiers qui accèdent directement au matériel ou à la mémoire. Ajouter un élément à la liste exige une raison explicite et une relecture.
Pas de panique sur une entrée externe : ni unwrap, ni expect, ni panic! dans le code de bibliothèque, pas d’indexation ni d’arithmétique non vérifiées, et chaque exception à un lint donne sa raison.
Les crates d’appareil sont no_std et n’allouent rien. Les compilations release conservent les contrôles de débordement, et une panique arrête la partie au lieu de la laisser continuer.
Les parseurs refusent une entrée surdimensionnée avant de la copier, renvoient des erreurs typées, et ont des tests de propriétés et une cible de fuzzing.
Aucun secret nulle part, pas même des clés de développement. Les clés de test sont créées à l’exécution d’un test, et jamais stockées.

Lire les relevés d’une image

Chaque image est écrite dans build/BOARD/SYSTEM/, avec deux relevés à côté d’elle.

sel4-config.txt nomme l’image, son empreinte, la carte, le SDK Microkit et le noyau, puis indique où se situe l’image par rapport aux preuves de seL4, à raison d’une ligne status: par motif, et liste chaque option du noyau qui en décide à côté de la valeur de la configuration vérifiée. Un noyau de débogage est une version de développement. Un noyau multicœur ou à criticité mixte, ou une carte absente de la liste de seL4, est hors du périmètre des preuves de seL4. Un noyau qui correspond à chaque option n’est pourtant jamais qualifié de “vérifié” : le relevé donne les faits, et s’en tient là.

sbom.cdx.json est la nomenclature logicielle CycloneDX de l’image : ce dont elle est faite, jusqu’à chaque crate de chaque domaine de protection, chacun avec son sha256.

Garder le contrôle rapide

L’ensemble complet des preuves et du fuzzing prend beaucoup de temps : le make ci de tous les jours n’exécute donc Kani, le fuzzing et Miri que là où une modification a une incidence. Il suit la modification à travers chaque crate qui en dépend, et saute toute vérification dont les entrées n’ont pas changé depuis son dernier succès. make ci CI_SCOPE=full les exécute toutes, sans rien en cache ; make kani, make fuzz et make pds-miri s’exécutent toujours en entier.

Kani est l’étape la plus gourmande : chaque tâche de preuve dispose d’environ 10 Go de mémoire, et KANI_JOBS fixe combien s’exécutent à la fois. Si make kani manque de mémoire, donnez-en davantage à la machine virtuelle de Podman, ou définissez KANI_JOBS=1.