Ce que la preuve ne dit pas

Les quatre limites de la vérification formelle, dont une est un théorème

Les trois articles précédents décrivent des méthodes qui fonctionnent. Celui-ci décrit ce qu'elles ne donnent pas — et il est le plus utile des quatre, parce que l'erreur la plus fréquente à propos de la vérification formelle n'est pas de la croire impossible, mais de croire qu'elle termine la discussion.

Quatre limites. La première est mathématique et ne bougera jamais. Les trois autres sont pratiques, et ce sont elles qu'on rencontre.

I. L'impossibilité de principe

Alan Turing démontre en 1936 qu'aucun programme ne peut décider, pour tout programme donné, s'il s'arrêtera. C'est le problème de l'arrêt.

L'argument tient en une page et ne demande rien d'autre que de la patience. Supposons qu'existe un programme ARRET(p, e) qui répond toujours correctement « oui » ou « non » à la question « le programme p s'arrête-t-il sur l'entrée e ? ». Construisons alors :

programme DIABLE(p) :
    si ARRET(p, p) dit « oui » alors boucler indéfiniment
    sinon s'arrêter

Que fait DIABLE(DIABLE) ?

S'il s'arrête, c'est qu'ARRET a répondu « non » — donc qu'il ne s'arrête pas.
S'il ne s'arrête pas, c'est qu'ARRET a répondu « oui » — donc qu'il s'arrête.

Les deux branches se contredisent. DIABLE est pourtant un programme parfaitement écrivable, dès lors qu'ARRET existe. Donc ARRET n'existe pas.

Henry Rice généralise en 1953, et c'est la version qui concerne notre sujet. Le théorème de Rice énonce que toute propriété non triviale du comportement d'un programme est indécidable : on ne peut pas décider mécaniquement, pour un programme quelconque, s'il boucle, s'il plante, s'il divise par zéro, s'il calcule la bonne chose.

Il n'existe donc pas, et il n'existera jamais, d'outil qui prend un programme quelconque et répond « correct » ou « incorrect ». Ce n'est pas un état de l'art, c'est une impossibilité au même titre que la quadrature du cercle.

Les trois échappatoires

Tout ce qui a été décrit dans l'article II est une manière de vivre avec ce théorème. Il n'y en a que trois, et chaque outil choisit la sienne.

Approximer. L'interprétation abstraite répond « sûrement correct » ou « je ne sais pas », jamais « incorrect ». Elle échappe au théorème en renonçant à trancher : les fausses alarmes sont exactement le prix de cette échappatoire, et elles ne sont pas un défaut d'implémentation qu'une version future corrigera.

Demander de l'aide. Le solveur et l'assistant de preuve échappent au théorème en n'étant pas entièrement automatiques : c'est l'humain qui fournit les invariants, c'est-à-dire l'idée. La machine vérifie une démonstration, elle ne la trouve pas.

Restreindre. Le model checking ne considère que des systèmes à nombre fini d'états, où l'exhaustivité redevient possible. Les types restreignent les propriétés exprimables à celles qui se décident vite. On ne traite plus « un programme quelconque » mais un fragment bien choisi.

Retenir ceci : toute promesse d'un outil qui vérifierait n'importe quel programme sans aide et sans approximation est fausse, et on peut le savoir sans même l'essayer.

II. La spécification peut être fausse

C'est la limite la plus importante en pratique, et la moins comprise.

Une preuve établit : le programme est conforme à sa spécification. Elle n'établit pas : le programme fait ce qu'il faut. Entre les deux se trouve la question de savoir si la spécification, elle, était la bonne — et aucune preuve ne peut y répondre, puisque c'est elle qui sert de référence.

L'article I l'a montré sur le tri : une spécification qui omet « le résultat contient les mêmes éléments que l'entrée » est satisfaite par une fonction qui renvoie un tableau vide. La preuve serait rigoureuse. Le programme serait inutilisable. Une spécification incomplète est un trou dans lequel le programme peut être correct et faux en même temps.

Le vol 501 d'Ariane 5, le 4 juin 1996, en est l'illustration coûteuse. Quarante secondes après le décollage, le lanceur s'est détruit. La cause : une conversion d'un nombre flottant 64 bits vers un entier signé 16 bits, dans le système de référence inertielle, a débordé.

Le détail qui importe est que le code était correct. Il venait d'Ariane 4, où il fonctionnait depuis des années. L'analyse montrait même que le débordement était impossible — sous l'hypothèse, exacte pour Ariane 4, que la vitesse horizontale restait dans certaines bornes. Ariane 5 avait une trajectoire plus rapide. L'hypothèse ne tenait plus.

Le calcul était juste. La spécification était périmée. Aucune vérification du code n'aurait signalé quoi que ce soit, puisque le code respectait ce qu'on lui demandait de respecter.

Ce qu'on peut faire contre ce risque n'est pas de prouver davantage, mais autre chose : rendre les hypothèses explicites plutôt qu'implicites, les revérifier quand le contexte change, spécifier deux fois de façon indépendante, et conserver des tests — qui, eux, confrontent le programme au monde et non à sa description. C'est la raison pour laquelle les tests ne disparaissent jamais, même dans les projets les plus formellement vérifiés.

III. Il reste toujours quelque chose à croire

Une preuve ne supprime pas la confiance. Elle la déplace vers un endroit plus petit et mieux surveillé. Ce déplacement est le vrai bénéfice, et il faut savoir dire où il s'arrête.

Après une preuve complète, il reste à faire confiance à :

Le noyau du vérificateur. Quelques milliers de lignes qui relisent la preuve. Petit, stable, audité depuis des décennies — mais du logiciel.
Les axiomes. La logique dans laquelle on raisonne est supposée cohérente. On ne peut pas le démontrer à l'intérieur de cette logique : c'est le second théorème de Gödel.
La modélisation de la machine. La preuve porte sur un modèle du processeur, de la mémoire, du système. Si le modèle diffère de la machine, la preuve porte sur autre chose.
Le matériel. Un défaut de conception du processeur, un bit retourné par un rayon cosmique : hors de portée.
Le compilateur — sauf s'il est lui-même vérifié, ce qui est précisément ce que CompCert apporte, et un bon exemple de déplacement réussi : le compilateur passe du statut de chose crue à celui de chose démontrée, et la confiance se reporte sur le noyau de Rocq, plus petit.

L'ensemble porte un nom, la base de confiance. L'objectif n'a jamais été de la réduire à rien — c'est impossible — mais de la rendre assez petite pour qu'un humain puisse l'examiner entièrement. Passer de « je fais confiance à cent mille lignes que personne n'a lues » à « je fais confiance à cinq mille lignes relues depuis vingt ans » est un progrès considérable, et c'est tout ce qu'on demande.

IV. Le coût

La dernière limite est prosaïque, et c'est elle qui décide en pratique.

L'ordre de grandeur donné par seL4 : environ dix mille lignes de C, de l'ordre de deux cent mille lignes de preuve, et des années-hommes par dizaines. Une vingtaine de lignes de démonstration par ligne de code vérifiée. Les travaux ultérieurs ont fait baisser ce rapport, jamais d'un ordre de grandeur.

Ce coût explique la géographie de la discipline. La vérification formelle est employée là où l'échec ne se rattrape pas :

Aéronautique — commandes de vol, où l'interprétation abstraite s'est imposée parce qu'elle ne demande pas d'annotations.
Ferroviaire — la signalisation de plusieurs métros automatiques, dont la ligne 14 à Paris, a été développée avec la méthode B, qui dérive le code à partir d'une spécification formelle par raffinements successifs, chacun démontré.
Cryptographie — implémentations de protocoles, où une faute est directement exploitable.
Noyaux et hyperviseurs — seL4 et ses descendants.
Protocoles distribués — model checking, chez les grands opérateurs de nuage, sur la conception plutôt que sur le code.

Et elle est absente partout ailleurs, pour une raison qui n'a rien de honteux : quand un défaut se corrige en dix minutes et se déploie dans l'heure, l'assurance coûte plus cher que le sinistre.

Le milieu du gué

Ce serait toutefois une conclusion paresseuse que de s'arrêter à « c'est trop cher ». Entre le test et la preuve complète, il existe un étage à faible coût et à rendement élevé, et c'est là que se joue la qualité de la plupart des logiciels :

Des types précis. Une preuve gratuite à chaque compilation. Rendre une faute inexprimable coûte moins cher que la détecter.
Des assertions. Une précondition écrite dans le code documente le contrat, sert de test, et se prête à une vérification ultérieure. Elle coûte une ligne.
Le test de propriété. On n'écrit plus « tri([3,1,2]) donne [1,2,3] » mais « pour tout tableau, le résultat est trié et de même contenu » — et l'outil tire mille cas au hasard, en cherchant les cas dégénérés, puis réduit tout contre-exemple à sa forme minimale. C'est de l'échantillonnage, donc pas une preuve ; mais l'énoncé qu'on écrit est déjà une spécification, et il attrape ce qu'aucun exemple choisi à la main n'aurait couvert.
Le fuzzing. Des entrées malformées par millions, guidées par la couverture de code. Efficacité redoutable sur tout ce qui analyse un format.
Les contraintes en base. UNIQUE, CHECK, NOT NULL : des invariants tenus par le moteur, pour un coût de conception nul, comme l'a montré l'article III.
Les analyseurs statiques ordinaires, dans l'intégration continue.

Aucun de ces moyens ne démontre la correction. Tous éliminent des classes entières de fautes pour un effort sans commune mesure avec celui d'une preuve. Le meilleur rendement de toute la discipline se trouve dans ses trois premiers mètres, et la plupart des projets ne les ont pas parcourus.

Pour finir

Quatre énoncés à retenir de ce dossier.

Une preuve dit quelque chose de vrai sur tous les cas. C'est unique. Aucune autre méthode ne le fait.

Elle ne dit que ce qu'on lui a demandé de dire. Une preuve rigoureuse d'une spécification fausse est un objet parfaitement correct et parfaitement inutile.

Elle ne supprime pas la confiance, elle la concentre. Sur un noyau, des axiomes, un modèle de machine — assez peu de choses pour qu'on puisse les nommer, ce qui était le but.

Le choix n'est pas entre prouver et ne pas prouver. C'est un continuum, de l'absence de garantie à la preuve complète, avec un coût qui croît beaucoup plus vite que la garantie. La question d'ingénieur n'est jamais « faut-il vérifier ? » mais « jusqu'où, ici, et pourquoi s'arrêter là ? ».