Ce qu’une preuve peut promettre

On fait le plus souvent confiance à un logiciel parce qu’il a été testé. Quelqu’un a imaginé ce qui pouvait mal tourner, l’a essayé, et a regardé le logiciel s’en sortir. Cela marche bien, jusqu’au cas auquel personne n’avait pensé.

Une preuve part de l’autre bout. Elle n’essaie pas des cas. Elle montre, par les mathématiques, qu’un énoncé vaut pour tous.

Tous les cas, pas seulement ceux qu’on a essayés

Prenons une petite promesse : ce code ne lit jamais au-delà de la fin de son tampon. Un test peut lui soumettre mille entrées, ou un milliard, et rapporter qu’aucune ne l’a mis en défaut. Une preuve dit autre chose, d’une autre nature : il n’existe aucune entrée qui le mette en défaut. On n’en a trouvé aucune, et il n’y en a aucune.

Le prix à payer est la rigueur. Une preuve exige un énoncé exact de ce que le code doit faire, sa spécification, et un raisonnement qui relie chaque ligne du code à cet énoncé. Pour un vrai logiciel, ce raisonnement est bien trop long pour qu’une personne le vérifie à l’œil. C’est donc un ordinateur qui le vérifie.

Vérifiée par machine

Voilà ce que signifie « vérifiée par machine ». La preuve est écrite en entier, dans un langage que sait lire un programme appelé assistant de preuve, et ce programme confronte chaque étape aux règles de la logique. Il ne fatigue pas à la page neuf cents, et il ne croit personne sur parole.

Les preuves de seL4 sont vérifiées ainsi, dans un assistant de preuve nommé Isabelle/HOL. Elles sont publiques, et chacun peut les rejouer.

Ce que disent les preuves de seL4

seL4 est le noyau sur lequel tourne chaque système NoWayOS : environ 10 000 lignes de code, et le seul code qui ait le contrôle total de l’appareil. Sa taille est l’essentiel. Un raisonnement sur dix mille lignes peut être mené à son terme. Un raisonnement sur des dizaines de millions ne le peut pas encore.

La seL4 Foundation présente ces preuves par couches :

• Le code fait ce que dit la spécification, et rien de plus. Il en découle une liste de choses que le noyau ne peut pas faire : déborder d’un tampon, suivre un pointeur nul, laisser fuir de la mémoire, diviser par zéro.
• Le programme qui s’exécute correspond au code qui a été prouvé. Un compilateur se tient entre les deux ; une preuve supplémentaire en vérifie donc la sortie.
• Le noyau peut tenir séparées les parties d’un système. Une partie ne peut ni modifier les données d’une autre, ni les lire, ni lui prendre les ressources dont elle a besoin, à moins d’en avoir reçu le droit.
• Un système peut démarrer dans l’état pour lequel il a été conçu, avec exactement les droits que sa description énumère.

Toutes les couches ne sont pas achevées pour tous les processeurs et toutes les configurations. Cela compte, et nous y reviendrons.

Ce qu’une preuve tient pour acquis

Une preuve a exactement la portée de son énoncé, et elle repose sur ses hypothèses. seL4 écrit les siennes : que le matériel se comporte comme le dit son modèle, que quelques centaines de lignes du code le plus proche du matériel sont justes, que le code exécuté avant le démarrage du noyau a fait son travail. La preuve de confidentialité ne couvre pas les temps d’exécution.

Elle ne dit rien sur la question de savoir si la spécification demande la bonne chose, et rien sur le logiciel au-dessus du noyau. Un noyau prouvé isolera fidèlement un programme qui contient un bogue. Le bogue est toujours là. Il ne peut simplement atteindre rien d’autre.

Ce n’est pas une faiblesse des preuves. C’est ce qui fait leur valeur : elles disent précisément ce qu’elles couvrent, et vous savez donc précisément ce qui reste.

Où se situe NoWayOS

Voici la position, sans détour. NoWayOS tourne sur seL4, mais aucune image NoWayOS n’entre aujourd’hui dans les preuves achevées de seL4. NoWayOS utilise la configuration à criticité mixte de seL4, dont les preuves pour nos processeurs sont en cours. Et les preuves de seL4 n’ont jamais couvert le code propre à NoWayOS. Nous ne disons donc pas que NoWayOS est “formellement vérifié”, et nous ne le dirons pas.

Chaque image dit où elle en est. Un fichier, à côté d’elle, énumère la configuration de son noyau, option par option, en regard de celle que seL4 a prouvée. La page Sécurité en montre un vrai.

De plus petites preuves, les nôtres

Le code de NoWayOS tire son assurance d’ailleurs : Rust, l’isolation, la relecture, les tests, et des preuves d’un genre plus modeste.

Chaque décodeur des messages qui circulent entre les parties d’un système a des preuves bornées, produites avec un vérificateur de modèles nommé Kani. Une preuve bornée couvre toute entrée jusqu’à une taille déclarée, ici l’enregistrement le plus long qu’un décodeur accepte. À l’intérieur de cette borne, c’est une vraie preuve : aucune entrée ne fait paniquer le décodeur, ne le fait déborder ni lire hors limites. Au-delà de la borne, elle ne dit rien, et c’est pourquoi la borne est l’entrée la plus longue qui soit.

Ensuite, nous cassons les décodeurs exprès, pour nous assurer que les preuves le remarquent. Une preuve qui ne peut pas échouer ne vaut pas mieux qu’un test qui ne le peut pas.

La juste mesure

Une preuve ne rend rien “impiratable”. Elle rend un énoncé vrai, dans tous les cas, sous des hypothèses que vous pouvez lire. Connaissez l’énoncé et les hypothèses, et vous savez ce que vous avez.

C’est pourquoi NoWayOS est bâti sur le noyau qui a ces preuves, et pourquoi il vous dit, image par image, jusqu’où elles vont.