Pourquoi les logiciels ont des bugs : la preuve mathématique que la vérification parfaite est impossible

Les bugs logiciels sont partout. Ils font planter les applications, corrompent les données, et tuent parfois des personnes. Un rapport 2022 du Consortium for Information and Software Quality a estimé le coût de la mauvaise qualité logicielle aux États-Unis à 2 410 milliards de dollars. Ce n’est pas une faute de frappe. Des milliers de milliards.

La réaction naturelle est de demander : pourquoi ne pas simplement construire de meilleurs outils pour détecter les bugs avant la livraison du logiciel ? La réponse ne tient ni à la paresse ni aux contraintes budgétaires. Elle tient aux mathématiques. Trois résultats de la logique du XXe siècle prouvent que la vérification logicielle impossible à garantir n’est pas une faille du génie humain, mais une loi fondamentale de l’univers, aussi incontournable que la vitesse de la lumière. Aucun outil, aucune technique, aucune somme d’argent ne pourra jamais garantir qu’un programme est exempt de bugs. Voici pourquoi.

Le rêve qui s’est effondré : le programme de Hilbert

En 1928, le mathématicien allemand David Hilbert lança un défi audacieux au monde entier : trouver une procédure mécanique unique capable de déterminer, pour n’importe quel énoncé mathématique, s’il était vrai ou faux. Si une telle procédure existait, elle résoudrait toutes les questions des mathématiques. Elle permettrait également, par extension, de trancher toutes les questions relatives au comportement correct d’un programme informatique, puisque les programmes sont des objets mathématiques.

Trois ans plus tard, un logicien autrichien de 25 ans nommé Kurt Gödel détruisit ce rêve. Ses théorèmes d’incomplétude de 1931 prouvèrent que tout système formel suffisamment puissant pour décrire l’arithmétique de base contiendra toujours des énoncés vrais qu’il ne peut pas démontrer. Peu importe le nombre de règles que l’on ajoute, il y aura toujours des vérités qui passent entre les mailles du filet. Le système ne peut même pas prouver sa propre cohérence.

Ce fut le premier domino. Si les mathématiques elles-mêmes ont des angles morts, tout outil construit sur les mathématiques en hérite.

L’impossibilité de la vérification logicielle : Turing et le problème de l’arrêt

En 1936, Alan Turing prit l’intuition de Gödel et l’appliqua directement au calcul. Il posa une question en apparence simple : peut-on écrire un programme qui examine n’importe quel autre programme et détermine correctement s’il finira par s’arrêter ou bouclera indéfiniment ?

Turing prouva que la réponse est non. Son argument est élégant. Supposons qu’un tel programme existe. Appelons-le H. Fournissons à H un programme spécialement conçu pour faire l’inverse de ce que H prédit. Si H dit « ce programme s’arrête », le programme boucle. Si H dit « ce programme boucle », le programme s’arrête. Dans les deux cas, H se trompe. Cette contradiction prouve que H ne peut pas exister.

Ce résultat, connu sous le nom de problème de l’arrêt, a une conséquence directe pour la détection des bugs. Si on ne peut même pas déterminer si un programme finira de s’exécuter, on ne peut certainement pas déterminer s’il produira la bonne réponse. La question la plus fondamentale sur le comportement d’un logiciel est prouvablement sans réponse.

Le théorème de Rice : le coup de grâce

Si le problème de l’arrêt ressemble à un cas limite étroit et artificiel, Henry Gordon Rice a fermé cette échappatoire. Dans un article de 1953 issu de sa thèse de doctorat à l’université de Syracuse, Rice prouva quelque chose de bien plus général : toute question non triviale sur ce que fait un programme est indécidable.

« Non trivial » a ici un sens précis. Une propriété triviale est vraie pour tous les programmes ou fausse pour tous les programmes. Tout le reste est non trivial. Comme l’énonce le théorème de Rice, aucun algorithme ne peut répondre correctement à aucune question non triviale sur le comportement d’un programme pour tous les programmes possibles. Est-ce que le programme produit un jour le nombre 42 ? Indécidable. Accède-t-il jamais à une mémoire qui ne lui appartient pas ? Indécidable. Est-il exempt de failles de sécurité ? Indécidable.

Comme l’a résumé un chercheur en fiabilité logicielle : « Nous ne pouvons pas savoir avec certitude si un logiciel sera exempt d’incidents. C’est possible, mais on ne pourra jamais le prouver. »

Quand les bugs tuent : le coût réel

Ce ne sont pas des préoccupations abstraites. La machine de radiothérapie Therac-25 tua au moins trois patients entre 1985 et 1987 à cause de conditions de concurrence dans son logiciel. Les modèles précédents disposaient de verrouillages matériels pour prévenir les surdoses, mais le Therac-25 les remplaça par des vérifications logicielles seules. Le logiciel échoua. Les patients reçurent des doses de rayonnement des centaines de fois supérieures à ce qui était prévu.

En 1996, le vol inaugural de la fusée Ariane 5 dévia de sa trajectoire 37 secondes après le lancement et se détruisit. La cause : un nombre en virgule flottante sur 64 bits fut converti en entier sur 16 bits, et la valeur déborda. Le code avait été réutilisé depuis la fusée Ariane 4, où les valeurs étaient plus petites. Personne ne l’avait testé avec la trajectoire réelle d’Ariane 5. L’échec coûta plus de 370 millions de dollars.

Une étude de 2002 commandée par le NIST estima que les bugs logiciels coûtaient 59,5 milliards de dollars par an à l’économie américaine. En 2022, ce chiffre avait grimpé à 2 410 milliards. Comme le nota le NIST : « Les développeurs de logiciels consacrent déjà environ 80 % des coûts de développement à identifier et corriger les défauts, et pourtant rares sont les produits d’un autre type livrés avec un tel niveau d’erreurs. »

Si on ne peut pas le prouver, que peut-on faire ?

Les résultats d’impossibilité ne signifient pas que tout espoir est perdu. Ils signifient que nous devons être honnêtes sur ce que « testé » et « vérifié » veulent réellement dire. Plusieurs stratégies fonctionnent dans les limites des mathématiques :

• Les systèmes de types détectent certaines catégories de bugs en restreignant ce que les programmes peuvent exprimer. Des langages comme Rust préviennent des classes entières d’erreurs mémoire à la compilation. Cela fonctionne parce que la vérification de type examine la syntaxe du programme, et non son comportement, contournant ainsi le théorème de Rice.
• Les tests trouvent des bugs, mais ne peuvent jamais prouver leur absence. Comme l’a noté l’informaticien Edsger Dijkstra, les tests peuvent montrer la présence de bugs, jamais leur absence.
• La vérification de modèlesTechnique de vérification automatisée qui vérifie exhaustivement si un système satisfait une propriété donnée en explorant tous ses états possibles., qui valut à Clarke, Emerson et Sifakis le prix Turing 2007, vérifie de façon exhaustive les propriétés des systèmes à états finis. Les vérificateurs de modèles ont analysé des systèmes avec des espaces d’états de 10¹²⁰, bien plus de configurations que d’atomes dans l’univers observable. Mais ils ne fonctionnent que sur des systèmes à états bornés, pas sur des programmes arbitraires.
• Les assistants de preuve formelle comme Coq et Lean permettent aux programmeurs d’écrire des preuves mathématiques que leur code est correct. Cela déplace le problème : au lieu de vérifier automatiquement n’importe quel programme, on exige du programmeur qu’il fournisse la preuve. Cela fonctionne, mais c’est coûteux et limité aux systèmes critiques.

Chacune de ces approches échange la généralité contre la puissance. Aucune ne contredit le théorème de Rice. Elles acceptent toutes l’impossibilité et délimitent un territoire utile à l’intérieur de celle-ci.

La vérité qui dérange

Chaque fois qu’une entreprise promet une « sécurité de niveau militaire » ou un « logiciel zéro bug », elle avance une affirmation que les mathématiques ont prouvé impossible à garantir. Les trois résultats de Gödel, Turing et Rice forment une chaîne d’impossibilité : les systèmes formels ont des angles morts, le calcul a des questions indécidables, et toute propriété intéressante des programmes tombe dans la catégorie indécidable.

Cela n’excuse pas l’ingénierie bâclée. Les morts du Therac-25 auraient pu être évitées avec des pratiques de sécurité élémentaires. L’explosion d’Ariane 5 aurait pu être évitée avec des tests adéquats. Ce que les mathématiques nous disent, c’est qu’aucun niveau d’ingénierie, aussi bon soit-il, ne ramènera jamais le nombre de bugs à zéro. L’objectif n’est pas la perfection : c’est la résilience. Construire des systèmes qui échouent de façon sûre, détectent les erreurs tôt, et se dégradent avec grâce quand l’inévitable se produit.

Les bugs ne sont pas un échec de l’industrie du logiciel. Ils sont une conséquence des lois des mathématiques. Plus tôt nous l’acceptons, mieux nous pouvons nous y préparer.

Les défauts logiciels ont coûté à l’économie américaine un montant estimé à 2 410 milliards de dollars en 2022, selon le rapport bisannuel de CISQ. La persistance des bugs malgré des décennies d’amélioration des outils est souvent présentée comme un problème d’ingénierie. Ce n’en est pas un. C’est un problème mathématique. Trois résultats fondamentaux de la théorie de la calculabilité établissent que la vérification logicielle impossible à perfectionner est une contrainte prouvable et permanente sur ce que tout outil peut accomplir.

L’incomplétude de Gödel : les fondations se fissurent

En 1931, Kurt Gödel publia deux théorèmes qui démolissaient le programme de David Hilbert visant à placer toutes les mathématiques sur des fondations complètes, cohérentes et décidables.

Le premier théorème d’incomplétude énonce que tout système formel cohérent F capable d’exprimer l’arithmétique de base contient des énoncés qui sont vrais mais indémontrables dans F. La preuve construit une phrase de Gödel G_F qui dit en substance « cet énoncé n’est pas démontrable dans F ». Si G_F était démontrable, le système serait incohérent. Si G_F est indémontrable, le système est incomplet. Dans tous les cas, complétude et cohérence ne peuvent pas coexister.

Le second théorème étend cela : F ne peut pas prouver sa propre cohérence. On peut prouver la cohérence de F dans un système plus fort F’, mais F’ lui-même ne peut pas prouver sa propre cohérence, et ainsi de suite à l’infini.

Pour la vérification logicielle, l’implication est structurelle. Tout système formel suffisamment puissant pour raisonner sur des programmes (ce qui exige au moins l’arithmétique de base) contiendra des énoncés vrais sur ces programmes qu’il ne peut pas prouver. La chaîne des théorèmes se poursuivant, les résultats de Gödel menèrent directement à la preuve de Church que l’Entscheidungsproblem est insoluble, et à la preuve de Turing qu’il n’existe pas d’algorithme pour résoudre le problème de l’arrêt.

Le problème de l’arrêt : l’indécidabilité de la question la plus simple

Dans son article de 1936 « On Computable Numbers », Alan Turing formalisa le calcul via les machines de Turing et prouva que le problème de l’arrêt est indécidable.

La preuve est un argument diagonal. On suppose qu’il existe une fonction totale calculable h(i, x) qui retourne 1 si le programme i s’arrête sur l’entrée x, et 0 sinon. On construit le programme g qui, sur l’entrée i, appelle h(i, i) : si h retourne 1, g boucle indéfiniment ; si h retourne 0, g s’arrête. On évalue alors h(g, g). Si h dit que g s’arrête, alors g boucle (contradiction). Si h dit que g boucle, alors g s’arrête (contradiction). Donc h ne peut pas exister.

Ce n’est pas une limitation du matériel ou des algorithmes actuels. C’est une démonstration par l’absurde qui s’applique à tout modèle de calcul équivalent à une machine de Turing, y compris tous les langages de programmation à usage général qui existent.

La conséquence pratique : les outils d’analyse statique qui scrutent le code pour détecter des bugs se heurtent constamment au problème de l’arrêt. Des outils comme ESLint, SonarQube ou les scanners de sécurité produisent nécessairement des faux positifs ou ratent de vraies anomalies, car une analyse parfaite est mathématiquement impossible.

L’impossibilité de la vérification logicielle : le théorème de Rice

Le problème de l’arrêt peut sembler étroit : il ne concerne que la terminaison. La généralisation de 1953 par Henry Gordon Rice ferme chaque brèche restante.

Le théorème de Rice énonce : soit P un sous-ensemble des entiers naturels qui est (1) non trivial (ni vide ni égal à N tout entier) et (2) extensionnel (si les programmes m et n calculent la même fonction, alors m est dans P si et seulement si n est dans P). Alors P est indécidable.

En termes simples : toute propriété sémantique non triviale des programmes est indécidable. « Sémantique » signifie relative au comportement, non à la syntaxe. « Non triviale » signifie vraie pour certains programmes et fausse pour d’autres. Les questions suivantes sont toutes indécidables :

• Le programme P se termine-t-il sur l’entrée n ?
• P retourne-t-il 0 pour toute entrée ?
• P accède-t-il jamais à une mémoire non allouée ?
• P est-il équivalent à une spécification donnée Q ?
• P contient-il une faille de sécurité ?

Comme l’a noté un ingénieur en fiabilité logicielle appliquant le théorème de Rice à l’analyse d’incidents : « Nous ne pouvons pas savoir avec certitude si un logiciel sera exempt d’incidents. C’est possible, mais on ne pourra jamais le prouver. » Il en découle que tout modèle mental traitant le logiciel comme « stable sauf en cas de force extérieure » est mathématiquement indéfendable.

Ce que le théorème de Rice ne dit pas

Le théorème de Rice n’interdit pas toute analyse de programmes. Il vise spécifiquement les propriétés sémantiques et les langages à usage général (Turing-complets). Les propriétés syntaxiques, comme « le code source contient-il une boucle while », sont décidables. La vérification de type est décidable parce qu’elle examine la structure du texte du programme, non le comportement à l’exécution. Les systèmes de types statiques dans des langages comme Haskell, Rust ou OCaml exploitent cette distinction : ils imposent des contraintes syntaxiques qui garantissent certaines propriétés comportementales (comme la sécurité mémoire) sans avoir besoin de résoudre le cas général indécidable.

Études de cas : la théorie rencontre la pratique

Therac-25 (1985-1987)

La machine de radiothérapie Therac-25 provoqua au moins six incidents de surdosage entre 1985 et 1987, les patients recevant des doses de rayonnement des centaines de fois supérieures à la dose prévue. La cause profonde était des erreurs de programmation concurrente (conditions de concurrence). Le prédécesseur de la machine, le Therac-20, disposait de verrouillages matériels qui empêchaient physiquement les surdoses. Le Therac-25 supprima ces verrouillages et s’appuya entièrement sur des vérifications logicielles de sécurité. L’enquête de référence de Leveson et Turner en 1993 attribua les défaillances à « des pratiques généralement médiocres de conception et de développement logiciel » et à une confiance excessive dans la capacité du logiciel à assurer la sécurité.

La condition de concurrence qui tua des patients est exactement le type de propriété comportementale que le théorème de Rice déclare indécidable : « Ce programme concurrent entre-t-il jamais dans un état où le faisceau tire sans que la cible soit en position ? » Aucun algorithme général ne peut répondre à cette question pour des programmes arbitraires.

Vol 501 d’Ariane 5 (1996)

Le 4 juin 1996, le vol inaugural de la fusée Ariane 5 dévia de sa trajectoire 37 secondes après le lancement et se détruisit. Le système de référence inertielle tomba en panne parce qu’une valeur en virgule flottante 64 bits (biais horizontal, BH) fut convertie en entier signé 16 bits, et la valeur dépassa la plage 16 bits. Le code avait été réutilisé depuis Ariane 4, où le profil de vol produisait des valeurs de vitesse plus faibles. Les programmeurs n’avaient protégé que quatre des sept variables critiques contre le débordement, s’appuyant sur des hypothèses valables pour la trajectoire d’Ariane 4, mais non pour celle d’Ariane 5.

La commission d’enquête Lions nota que « la spécification du système de référence inertielle et les tests effectués au niveau des équipements n’incluaient pas spécifiquement les données de trajectoire d’Ariane 5. En conséquence, la fonction de réalignement ne fut pas testée dans des conditions de vol Ariane 5 simulées, et l’erreur de conception ne fut pas découverte. » L’échec coûta plus de 370 millions de dollars.

L’explosion combinatoire des états

Même pour les systèmes à états finis où le théorème de Rice ne s’applique pas directement, la vérification se heurte à un mur pratique : l’explosion combinatoire des états. Un système à n variables binaires possède 2ⁿ états possibles. Edmund Clarke, dont les travaux sur la vérification de modèlesTechnique de vérification automatisée qui vérifie exhaustivement si un système satisfait une propriété donnée en explorant tous ses états possibles. valurent le prix Turing ACM 2007 (partagé avec E. Allen Emerson et Joseph Sifakis), décrivit le défi fondamental : « Un système informatique exécute des opérations simples, mais ces opérations peuvent se produire dans un nombre vertigineux d’ordres différents. Il est donc impossible pour le concepteur d’envisager chaque séquence possible et d’en prédire les conséquences. »

L’avancée de Clarke et McMillan fut la vérification symbolique de modèles par diagrammes de décision binaires (BDD), qui encodent plusieurs états de façon compacte. Cela permit aux vérificateurs de modèles de traiter des systèmes avec des espaces d’états de 10¹²⁰. Mais la vérification symbolique de modèles ne fonctionne que sur des systèmes à états finis. Les logiciels réels, avec une récursion non bornée, une allocation dynamique de mémoire et des entrées de longueur arbitraire, restent hors de portée pour une vérification comportementale complète.

Travailler dans les limites du possible

Les résultats d’impossibilité définissent un plafond, non un plancher. Des progrès substantiels sont possibles à l’intérieur de ces limites :

• L’interprétation abstraite (Cousot & Cousot, 1977) calcule des sur-approximations correctes du comportement des programmes. Elle peut prouver l’absence de certaines classes de bugs au prix de faux positifs. C’est précisément le compromis que le théorème de Rice permet : « il est possible d’implémenter un outil qui surestime ou sous-estime toujours, donc en pratique il faut décider lequel des deux pose le moins de problème. »
• Les systèmes de types dépendants (Coq, Agda, Lean, Idris) permettent d’encoder des spécifications sous forme de types et des preuves sous forme de programmes. Les programmes sont restreints à des fonctions totales (garantissant la terminaison), sacrifiant délibérément la complétude de Turing pour retrouver la décidabilité.
• La vérification de modèles vérifie de façon exhaustive les propriétés de logique temporelle sur des modèles à états finis. Elle est largement utilisée dans la vérification matérielle et l’analyse de protocoles.
• La vérification bornée de modèles et les solveurs SAT/SMT vérifient des propriétés jusqu’à une profondeur bornée, transformant le problème en satisfiabilité booléenne. Ils ne peuvent pas prouver la correction non bornée, mais sont efficaces pour trouver des bugs.
• La vérification et la surveillance à l’exécution vérifient des propriétés pendant l’exécution plutôt que de façon statique, détectant les violations au moment où elles se produisent. Cette approche accepte que la vérification avant déploiement soit incomplète et ajoute un filet de sécurité.

Le fil conducteur : chaque technique efficace soit restreint le langage (le rendant sous-Turing), soit restreint la propriété (en vérifiant la syntaxe ou le comportement borné au lieu de la sémantique complète), soit accepte l’incomplétude (correct mais pas complet, ou complet mais pas correct).

La vérité qui dérange

Une étude du NIST de 2002 révéla que les développeurs de logiciels consacraient déjà environ 80 % des coûts de développement à l’identification et à la correction des défauts. En 2022, le coût total de la mauvaise qualité logicielle aux États-Unis avait atteint 2 410 milliards de dollars, avec une dette techniqueCoût accumulé des raccourcis et décisions de conception médiocres en développement logiciel, qui devront être corrigés pour que le système reste fonctionnel. accumulée de 1 520 milliards à elle seule.

Ces chiffres ne convergeront pas vers zéro. La chaîne d’impossibilité de Gödel (1931) à Turing (1936) en passant par Rice (1953) établit un plafond permanent sur ce que la vérification peut accomplir. Tout langage de programmation suffisamment expressif produira des programmes dont aucun outil ne pourra prédire entièrement le comportement. Le problème de l’arrêt n’est que l’exemple le plus simple ; le théorème de Rice garantit que toute question comportementale intéressante partage le même sort.

La réponse de l’ingénierie doit être la résilience, non la perfection. La défense en profondeurStratégie de cybersécurité utilisant plusieurs couches de protection indépendantes, de sorte qu'une défaillance isolée ne compromette pas l'ensemble du système.. La redondance. Les verrouillages matériels qui ne font pas confiance au logiciel. Des tests qui acceptent de ne pouvoir que trouver des bugs, jamais prouver leur absence. Des systèmes de types qui préviennent des catégories entières d’erreurs par construction. Et la reconnaissance honnête que le rêve d’un logiciel à usage général prouvablement correct n’est pas un problème non résolu. C’est un problème résolu. La réponse est : c’est impossible.