L’erreur en informatique est la plupart du temps nommée bug, mot anglais qui désignait à l’origine une mite¹.

L’origine du nouveau sens de ce mot est souvent attribuée à Grace Hopper, informaticienne visionnaire qui a conçu le premier compilateur en 1951 puis le langage COBOL (COmmon Business-Oriented Language) en 1959 — c’était le premier langage de programmation digne d’être dit « de haut niveau ». Un jour de 1947, l’ordinateur Harvard Mark II sur lequel son équipe travaillait est tombé en panne à cause d’une mite qui avait bloqué un relai (voir la figure ci-dessus, extraite de ses notes).

En fait, Grace Hopper n’était pas présente ce jour-là, et ce n’est pas non plus la vraie source de ce mot, déjà attesté en 1874, et utilisé par exemple par Edison pour nommer tous les petits ennuis qui surviennent entre la naissance d’une idée et sa mise en place industrielle. Il n’empêche qu’il a été popularisé par les notes de Grace Hopper et qu’il nous est resté.

Nous allons voir que les bugs sont très fréquents dans les systèmes et applications informatiques, difficiles à éviter, et étonnamment tolérés par les utilisateurs qui ont longtemps considéré comme inutile de comprendre ce qu’est vraiment l’informatique (y compris dans l’industrie et même chez beaucoup de scientifiques). Au début, quand les programmes informatiques ne faisaient pas grand-chose, les bugs avaient un côté amusant. Maintenant qu’ils font fonctionner nos téléphones, les grands réseaux d’information, la plupart des appareils scientifiques et tout un tas de machines bien physiques utilisées par le terrien moyen, ils sont devenus franchement nocifs. Ils peuvent soit provoquer de mauvais comportements des programmes et machines, qui peuvent aller de l’ennuyeux au franchement cher et dangereux, soit constituer un des principaux points d’entrée des attaques sur la sécurité des systèmes informatisés qui se généralisent avec des conséquences éminemment délétères. Et même les circuits intégrés électroniques, passés en 50 ans de quelques milliers à quelques dizaines de milliards de transistors, comportent encore des bugs sournois malgré l’extrême soin apporté à leur conception, bien supérieur à ce qu’on trouve pour les logiciels mis en service trop vite sous prétexte qu’on pourra toujours en livrer de nouvelles versions mises à jour.

Mais pourquoi sommes-nous dans cette situation ? La première partie de ce billet va répondre très simplement à cette question, en montrant l’énorme fossé qui sépare l’homme de l’ordinateur, pas encore assez compris du public général. La deuxième partie donnera des exemples de bugs, allant du croustillant au vraiment délétère. La dernière partie sera consacrée aux moyens d’éviter et de contrôler les bugs, moyens efficaces mais encore pas assez souvent employés ; elle sera suivie d’une rapide conclusion. Les discussions présentées ici sont pour la plupart issues de mon livre L’hyperpuissance de l’informatique, paru en 2017² – le sujet n’ayant fait que s’aggraver depuis.

1. L’homme et l’ordinateur : deux exacts opposés

La figure 1 ci-contre illustre l’opposition fondamentale entre l’homme et le circuit électronique : l’homme est intuitif³, lent, et se trompe souvent ; à l’inverse, le circuit est totalement stupide, hyper-rapide et ne fait jamais d’erreur⁴. Faire passer une idée de l’un à l’autre est donc comme passer sur un pont de lianes au-dessus d’un grand gouffre.

Cela n’a rien d’intuitif. Illustrons-le avec un exemple que j’utilise souvent avec des paires d’enfants, l’un qui dicte et l’autre qui se déplace, pour leur expliquer la différence entre l’ordinateur et eux-mêmes (ça marche aussi avec des adultes).

La figure 2 à droite de ce paragraphe présente un trajet sur une grille, avec dans la première ligne son programme écrit avec trois instructions à appliquer à chaque carrefour : T = tout droit, D = à droite et G = à gauche. Un enfant dicte le programme, l’autre l’exécute sur un carrelage à gros carreaux. Le bon trajet est celui du zigzag bleu. Je n’ai encore jamais vu le marcheur le suivre précisément et arriver au bon endroit, bien que les deux essayent de se concentrer au mieux ! Comme l’illustrent les deux lignes en dessous, une erreur d’un seul caractère à la lecture ou à l’exécution fait aller n’importe où, et les n’importe où sont très nombreux.

 

Mais l’ordinateur matériel n’est pas du tout comme l’enfant : il fait toujours exactement ce qui est écrit dans son logiciel — ici le mot décrivant le chemin à suivre. Toute erreur dans l’écriture de ce logiciel, comme celle minime des textes bleus et marrons, est exécutée par ses circuits électroniques avec une conscience professionnelle remarquable, quelles que soient ses conséquences. Autrement dit, l’ordinateur est un excellent amplificateur d’erreur de programmation, et donc d’erreur de pensée humaine ! Cela explique en particulier pourquoi des erreurs minimes dans des coins des programmes peuvent avoir des impacts vraiment délétères.

Mais le programme ci-dessus est tout petit. En pratique, les programmes dont on se sert tous les jours font très vite des dizaines ou centaines de milliers de lignes de code, voire des millions ou dizaines de millions pour les plus gros. Peut-on réellement écrire des programmes de cette taille sans faire de bugs ? La pratique nous force à dire non, et de loin.

2. Quelques exemples de bugs

Les bugs se trouvent presque partout, et vous en avez sûrement détectés quelques-uns en utilisant des ordinateurs, voire en essayant de les programmer. Par exemple, quand vous téléchargez la nouvelle version d’une application sur votre téléphone, vous la voyez souvent accompagnée d’un message du type « amélioration de la stabilité et de l’expérience utilisateur », donc écrit en novlangue commerciale. Sa traduction en français classique est plus claire : correction de bugs logiciels et de défauts de conception de l’interface homme-machine !

Je vais surtout citer ici plusieurs bugs qui ont affecté des systèmes physiques contrôlés « par ordinateur », expression accrochée à la pensée matérielle qu’il faut en fait traduire en « par logiciel ». Leur impact sur le monde physique les rend bien plus dangereux et plus chers. Je n’en présenterai ici que des analyses très simplifiées, tous les détails étant écrits dans mon livre précité.

Le Patriot rate le scud

Voici un accident dramatique, dû à un bug informatique dans un système vraiment critique. Le 25 février 1991, lors de la première guerre du Golfe, la chute d’un missile Scud irakien sur une caserne américaine à Dharan fit 28 morts et 98 blessés parmi les militaires présents. Pourtant, la caserne était protégée par des antimissiles Patriot. La raison était que l’informatique de la rampe de lancement de ces Patriot était très ancienne et ne respirait pas la qualité. En particulier, au lieu d’être gérée en binaire, l’heure était gérée en décimal avec des arrondis douteux et dérivait régulièrement. C’était connu des militaires, et il était conseillé de redémarrer le système toutes les quatre ou cinq heures (!). Mais la tension était forte et le système est resté beaucoup plus longtemps en alerte, presque une centaine d’heures. Quand le Patriot a été lancé, l’heure avait dérivé de 0,34 seconde par rapport aux autres systèmes, ce qui lui a suffi pour rater la cible : comme le Patriot voyage à 1 676 mètres par seconde, l’erreur était de 569 mètres. 

Les Raptors perdent la tête

Autre bug lié à la représentation du temps, qui a affecté le F22A Raptor, un des avions furtifs les plus avancés produits aux Etats-Unis — une merveille de technologie à 330 millions de dollars pièce. Le 11 février 2007, douze Raptor se rendaient de Hawaii au Japon. Quand ils ont traversé la ligne de changement de date, tous leurs systèmes informatiques de navigation, de communication et de jauge de carburant commandés par l’ordinateur de bord se sont éteints en même temps pour ne jamais se rallumer. Les pilotes se sont donc retrouvés sans instruments. Heureusement, il faisait beau et les Raptor étaient accompagnés par leurs ravitailleurs. Ils ont pu faire demi-tour, suivre les ravitailleurs et se remplir d’essence à vue, puis atterrir à Hawaii. Comme ils ne transportent pas de passagers, les avions de chasse ne sont pas soumis au régime safety critical, réservé aux avions de ligne !

Le bug d’Ariane 501

Lors du premier lancement d’Ariane 5 le 4 juin 1996, la fusée a explosé après 37 secondes d’un vol jusque–là nominal. L’explosion a fait suite à deux erreurs identiques et quasi-simultanées dans les logiciels internes des deux centrales à inertie du même modèle : elles avaient chacune détecté un débordement arithmétique lors du stockage d’une trop grande valeur numérique dans une mémoire qui ne pouvait pas la contenir. Ce problème ne gênait en fait pas du tout le bon fonctionnement d’Ariane 5 car la valeur numérique en cause ne lui avait jamais servi à rien⁵ Mais les centrales à inertie, en parfait fonctionnement par ailleurs, avaient décidé d’abandonner leur tâche en envoyant un message d’erreur au système global, qui s’est trouvé incapable de stabiliser la fusée par manque de données sur son attitude. 

Les causes de ce bug sont diverses, mais viennent quasiment toutes d’une compréhension trop limitée de la vraie nature de l’informatique et de ses dangers. Par exemple, le problème aurait pu être détecté en simulation si Ariane 5 avait été simulée sur sa propre trajectoire et non sur celle d’Ariane 4, très différente et ne provoquant pas le bug, ou encore en abonnant le vieux principe « si ça a bien marché jusqu’à maintenant, surtout ne rien changer » — sans valeur en informatique dès qu’on sort du fonctionnement nominal. Heureusement, les leçons en ont été tirées et les lancements suivants ont été informatiquement parfaits (sauf le second, mais cette fois à cause d’un problème physique).

Le sauvetage de deux célèbres robots martiens

Les deux bugs suivants ont affecté les très fameux robots martiens américains, Pathfinder en 1997 et Spirit en 2004, juste après leur arrivée sur Mars. Ils ont eu des effets similaires malgré des causes différentes : un cycle de redémarrages permanents de l’ordinateur central du robot, que les ingénieurs ont réussi à contrôler in extremis avant que les batteries soient épuisées. Entrons un peu dans les détails.

Après son arrivée, l’ordinateur interne de Pathfinder s’est remis en marche normalement, a pris contact avec la terre, mais est entré dans un cycle infernal de redémarrages au bout de quelques minutes. La raison était ce qu’on appelle un interblocage entre deux tâches assez simples, qui ne faisaient qu’attendre chacune que l’autre lui rende la main. Heureusement, un circuit de surveillance redémarrait périodiquement le système en voyant s’il ne se passait plus rien pendant trop longtemps. Les ingénieurs ont mis longtemps à comprendre ce bug, qu’ils ont pu ensuite corriger depuis la terre. Pour Pathfinder, il a suffi de faire passer un seul bit de 0 à 1 à l’intérieur du système d’exploitation (pour les connaisseurs, pour rétablir l’héritage de priorité dans la gestion des tâches, mis à 0 probablement pour optimiser le code).

La même chose est arrivée à Spirit, mais pour une raison bien différente : un bug dans une vieille version du logiciel de gestion de sa mémoire flash permanente. Pendant le long trajet vers Mars, elle enregistrait divers paramètres qui étaient ensuite transmis à la terre puis effacés pour faire place aux suivants. La mémoire utilisée par ces paramètres était bien restituée au système d’exploitation, mais leurs descripteurs qui contenaient les adresses des données individuelles ne l’était pas — un bug d’une vieille version du pilote de mémoires externes de Microsoft qui n’avait pas été mise à jour. Or, plus de la moitié de la flash était occupée par des descripteurs devenus obsolètes qui aurait dû être détruits en même temps que leurs données. Mais la mémoire de travail de l’ordinateur était deux fois plus petite que la flash, et une des premières actions de l’ordinateur à son réveil était de copier en mémoire la table des descripteurs. Quand sa mémoire de travail a été pleine d’entrées périmées, le système s’est bloqué, avant qu’un circuit de surveillance le fasse redémarrer comme pour Pathfinder. Ce bug bien caché dans un programme de bibliothèque que personne ne suspectait a été détecté sur terre au dernier moment par un ingénieur tenace, peu avant l’épuisement des batteries de Spirit ; il a fallu de vraies acrobaties pour le corriger en transmettant petit à petit des corrections à Spirit, qui a ensuite fait des merveilles.

Le problème de ma propre Citroën Berlingo

Pour ma part, j’ai eu un bug étonnant sur ma Citroën Berlingo Diesel : un soir, quand j’ai enlevé la clef du contact, le moteur ne s’est pas arrêté, ce qu’il a quand même fini par faire au bout d’une vingtaine de tournages de clef. Au garage, le lendemain, les gens ont fini par trouver la panne : un tout petit circuit attaché à la pédale de frein pour commander l’allumage du feu stop envoyait des signaux électriques incohérents dans l’unique bus de communication qui remplace la filasse du 20^e siècle, brouillant les autres messages, dont celui de la clef de contact ! Aucune étude sérieuse de sécurité pour l’interaction de l’ensemble des fonctions n’avait visiblement été faite. Maintenant que les voitures sont devenues des sortes de réseaux d’ordinateurs montés sur roues et que la publicité ne parle plus que de leurs fonctions informatisées, espérons que la compétence en informatique des fabricants et sous-traitants s’améliore. 

Les bugs létaux de la Toyota Camry

Voici un cas bien plus dramatique : en 2015, le logiciel interne du moteur de la voiture Toyota Camry a tué de façon attestée 89 personnes aux USA, et probablement davantage, ce qui a coûté de l’ordre de 2,5 milliards de dollars à Toyota, procès publics compris — sans que personne ne soit visiblement au courant dans notre pays. La cause est une organisation déplorable des diverses tâches de calcul pour le fonctionnement du moteur. Parmi bien d’autres bugs, la pile d’exécution qui stocke les adresses des tâches en cours d’exécution pouvait déborder de la zone qui lui avait été allouée et écraser les paramètres cruciaux du moteur ! Selon le rapport officiel, dont seulement une petite partie a été publié, l’architecture logicielle était un château de cartes, toutes les méthodes connues pour faire qu’un programme soit plein de bugs avaient été employées simultanément, et corriger un bug détecté en aurait probablement créé d’autres.

Étonnant de la part du plus grand constructeur mondial, non ? Pas vraiment pour qui connaît le domaine : à cette époque, l’industrie automobile était encore dominée par la mécanique, et l’informatique était considérée comme un truc pour technicien spécialisé sans formation particulière…

Des bugs aux trous de sécurité

Chacun connaît maintenant les problèmes de sécurité posés par les attaques sur les systèmes informatiques. Mais peu de gens savent que les points d’entrées de ces attaques sont souvent des bugs anodins mais assez faciles à exploiter par les attaquants. Je n’en citerai ici qu’un seul type, fréquent : l’utilisation par un attaquant d’une portion de mémoire utilisée par un programme mais lisible et écrivable par qui veut car pas explicitement alloué par le système d’exploitation, sans que le concepteur du programme ne l’ait remarqué. Un tel bug ne se voit pas en fonctionnement normal, et il est souvent introuvable par les tests classiques qui ne testent que les cas normaux d’utilisation.

Les exemples sont innombrables, et je n’en citerai qu’un, décrit dans un rapport public accompagnant une nouvelle version du système d’exploitation macOS d’Apple – sans accuser la marque, chaque annonce de chaque version des autres systèmes d’exploitation contenant aussi plusieurs rapports de bugs de ce type. Voici donc le rapport de correction de bug, bien sûr pas rédigé pour le public moyen :

Traduction en français usuel : le bug est dans le noyau du système d’exploitation, sa partie la plus critique. Il y a un problème de lecture / écriture hors des limites de la mémoire réservée par le programme, et donc dans une zone lisible et écrivable par n’importe qui. Cela peut permettre à un attaquant de prendre le pouvoir le plus total sur la machine, et Apple a conscience que ça a pu se produire — voire que ça s’est produit. Le bug a été corrigé en ajoutant une meilleure allocation mémoire vérifiée par un simple test, ce qui aurait dû être là depuis le début.

Le même type de correction de bug se trouve dans toutes les mises à jour de macOS, d’iOS, et de Windows ou même Linux (je suppose, car je n’ai pas vérifié…), sans parler de la masse d’autres programmes que nos ordinateurs font tourner…

Conclusion : les bugs conduisant à des trous de sécurité sont nombreux et dangereux car ils rendent les attaques faciles, et merci aux chercheurs ou ingénieurs qui les mettent en évidence, souvent contre un bonus financier. Il faut donc vraiment utiliser les nouvelles versions des systèmes et logiciels dès qu’elles sont disponibles car elles les corrigent en général correctement.

3. Construire des programmes corrects

Passons maintenant aux méthodes permettant de détecter les bugs, et surtout de les éviter dès le départ. 

Spécifier et tester : des méthodes standards mais limitées

Comment savoir si un programme fonctionne comme souhaité ou pas ? La méthode la plus simple et la plus universellement appliquée est le test : on essaie le programme sur plusieurs jeux de données, et on regarde si les résultats sont corrects. Mais le test a deux points de faiblesse, surtout quand l’application devient grosse. D’abord, comment fait-on pour exprimer non seulement ce qui est souhaité, mais aussi ce qui ne l’est pas, ce qu’on appelle spécifier la fonctionnalité de l’application et donc de son programme ? Cette étape indispensable est souvent informelle et incomplète, et il est encore fréquent de compter sur les retours des utilisateurs pour détecter les problèmes — ce qui reste cependant pertinent pour les interfaces homme-machine, une importante source de faiblesses dans beaucoup d’applications. De toutes façons, le nombre de cas à tester est souvent très grand⁶.

On essaie souvent de construire des tests « couvrants », c’est à dire qui exercent (couvrent) toutes les lignes de code ainsi qu’un maximum de comportements. Mais c’est souvent une quête sans fin, car passer dans toutes les lignes n’est pas passer dans toutes leurs combinaisons possibles.

Mais, à la fin des fins, il reste une difficulté fondamentale. Comme le disait dès 1967 le grand informaticien Esdger W. Dijkstra (prix Turing 1969), tester permet de trouver des bugs mais pas de montrer qu’il n’y en a pas. C’est particulièrement vrai pour les programmes parallèles, ceux divisés en plusieurs composants distribués sur une ou plusieurs machines et qui communiquent pour se synchroniser ou partager des valeurs, par exemple dans le cloud computing : vu l’explosion du nombre de comportements possibles, ils sont particulièrement difficiles à tester.

Une méthode potentiellement plus habile est le test aléatoire dirigé : pour une application donnée, on engendre automatiquement et selon des règles probabilistes un grand nombre de données aléatoires, si possible avec les résultats prévus. Mais il faut savoir comment le faire et avoir une idée de la représentativité des données engendrées. 

Un bel exemple est fourni par Csmith, un générateur aléatoire de programmes C destiné à vérifier que les codes machines générés par les compilateurs C calculent bien les résultats spécifiés par leurs codes sources. Ce qui rend ce travail important est que les compilateurs C font partie des programmes les plus utilisés et aussi les plus critiques, car ils peuvent rendre faux les programmes des utilisateurs même quand ceux-ci sont en fait justes. Csmith a généré plus d’un million de programme C, que l’équipe a utilisés pour tester la plupart des compilateurs publics et commerciaux. Des centaines d’erreurs ont été trouvées dans la plupart d’entre eux. Elles ont été d’abord ignorées par leurs auteurs, puis heureusement corrigées. Un seul compilateur a résisté : CompCert, dont nous allons reparler plus loin.

Vers des langages de programmation plus rigoureux et défensifs

Le cas le plus simple est celui des circuits électroniques digitaux. Lors de leur conception on ne parle plus jamais directement de transistors, la technologie physique précise étant du domaine de la fabrication et de moins en moins de celui de la conception, mais seulement de fonctions logiques qui peuvent être écrites en calcul Booléen, avec des variables prenant comme valeur 0 ou 1 et les opérateurs et, ou et non. Ce niveau étant trop bas en pratique, on utilise des langages de bien plus haut niveau comme Verilog ou VHDL, qui ne sont pas très formalisés⁷. Cependant, ils savent fabriquer du calcul Booléen, et donc une spécification formelle analysable du circuit considéré.

Pour les langages de programmation destinés aux logiciels, la situation est contrastée. Certains sont loin d’être formels, comme C (très ancien) ou C++, ce que doit calculer un programme donné étant assez loin d’être toujours défini, d’autres sont beaucoup plus rigoureux. Citons d’abord Rust, du niveau de C qui est le langage de bas niveau universel mais qui ajoute beaucoup de garde-fous automatisés bien conçus à la compilation pour éviter par exemple les écritures hors mémoire allouée. Citons aussi les langages fonctionnels de beaucoup plus haut niveau comme OCaml (français) qui assurent que ce que fait un programme est mathématiquement défini et pratiquement clair, ou encore Esterel, Lustre et SCADE 6 (français aussi) pour les systèmes industriels de commande de machines complexes, dont les définitions sont purement mathématiques. Notons aussi que le langage JavaScript est devenu le langage numéro 1 pour les sites Web, mais qu’il n’offre quasiment aucune sécurité ; le récent langage TypeScript de Microsoft en ajoute beaucoup et devient populaire.

Mais le langage en vue en ce moment — particulièrement chez les scientifiques des autres disciplines ou dans l’enseignement — est Python, langage joliment design mais qui n’offre quasiment aucun mécanisme de sûreté ou de sécurité.

Les langages pour la spécification formelle

La spécification de ce qu’il faut faire ou ne pas faire reste trop souvent un point faible, et beaucoup d’efforts ont été fait pour rendre ce sujet formel en utilisant les ressources de la logique mathématique. En effet, le niveau des langages de programmation est trop bas de ce point de vue : quand on programme, on est conduit à exprimer nombre de détails secondaires relativement à la fonctionnalité cherchée. Cela a conduit des chercheurs à chercher des langages de spécification pas forcément exécutables, mais permettant d’écrire et de vérifier plus ou moins formellement le bon fonctionnement d’une application à un niveau plus abstrait.

Cette idée était déjà présente chez Turing, qui a introduit dans une note de 1947 la notion fondamentale d’assertion, ou prédicat logique associable à chaque pas d’un programme et qu’on peut soit tester à l’exécution soit prouver par des méthodes logiques. Reprises plus tard en particulier par Bob Floyd et Tony Hoare, ces assertions jouent toujours un rôle essentiel dans le développement des programmes.

D’autres méthodes ont été ensuite développées, par exemple avec le langage LOTOS pour la spécification des protocoles de communications sur les réseaux puis avec la galaxie UML (Universal Modeling Language). Ce sujet n’avance cependant pas bien vite, car pas simple et souvent victime de l’« effet comité » qui essaie de mettre tout le monde d’accord (UML en est un bon exemple).

Prouver formellement

La preuve formelle de bon comportement est le niveau ultime de la vérification. Elle consiste à vérifier de façon mathématique que tous les comportements possibles d’une spécification ou encore mieux d’un programme exécutable sont complètement justes auquel cas on parle de preuve totale, ou au moins que certaines de leur propriétés sont préservées et empêchent certains types de bugs, et on parle alors de preuve partielle.

L’utilisation d’assertions logiques

En termes de preuves partielles, revenons d’abord sur l’idée de Turing d’associer des assertions logiques à des points d’un programme, expliquée dans une note de 1947. Il l’explique sur l’exemple de la factorielle écrite en langage machine⁸ sans multiplieur précâblé, donc par itération d’additions, sa preuve enchaînant des déductions ponctuelles assez simples. Cette même méthode a été retenue et partiellement automatisée ensuite de plusieurs façons. La plus élaborée est par l’interprétation abstraite, une très belle notion développée au cours des ans en France par Patrick et Radhia Cousot (hélas décédée) et leurs équipes, fondée sur des mécanismes itératifs très fins. Implémentée par le regretté Alain Deutsch dans les années 1980, elle a permis de détecter automatiquement le bug d’Ariane 5 précité. Le système Polyspace issu de cette expérience continue à être développé par la société américaine MathWorks, éditrice des fameux Matlab et Simulink, et reste très utilisé par l’industrie automobile. Mais les Cousot et leur équipe ont continué à améliorer leur théorie et sa pratique, développant ensuite le système Astrée, qui a permis de montrer à 100% que le code de vol de l’A380 ne peut pas faire de crash à l’exécution du type celui qui a tué Ariane 501. Astrée est maintenant distribué par la société allemande AbsInt.

Le calcul Booléen, les solveurs SAT et leur enrichissement SMT 

Revenons aux circuits et au calcul Booléen, celui de 0,1, et, ou, non. Le fondement de toute analyse formelle y est de savoir si une formule donnée peut être rendu vraie, ce qu’on appelle le problème SAT. On peut bien sûr essayer toutes les combinaisons de valeurs Booléennes des variables. Mais c’est clairement impraticable car exponentiel : pour n variables, le coût pour une formule vraie est toujours kⁿ, où k est le temps d’évaluation pour une combinaison (toujours faible) car il faut tester tous les cas possibles. Aucun algorithme n’est actuellement connu pour faire mieux dans les pires cas, c’est à dire en temps polynômial en n. Par ailleurs, on connaît des centaines de problèmes liés à d’autres besoins pratiques qui sont équivalents à SAT, comme le fameux problème du voyageur de commerce qui cherche un itinéraire passant une fois et une seule dans chaque ville d’une liste donnée ; si on savait résoudre l’un d’entre eux, on saurait les résoudre tous ! C’est ce qu’on appelle le problème P=NP, formalisé en 1971 et considéré par l’Institut Clay comme un des 7 problèmes mathématiques du millénaire – cet institut offre un million de dollars à qui le résoudra.

Mais les chercheurs ne se sont pas laissés impressionner. En 1992, Randy Bryant a inventé les BDDs (Binary Decision Diagrams), une structure de données qui donne souvent une forme canonique compacte aux expressions Booléennes et permet dans certains cas de résoudre SAT. Les BDDs ont vite été utilisés pour faire des preuves et des optimisations de circuits, mais aussi de programmes logiciels. Je m’en suis servi pour brancher un prouveur BDD sur mon langage Esterel, vérifiant par exemple avec Dassault Aviation des propriétés critiques de logiciels du Rafale, ou encore des propriétés critiques de circuits électroniques décrits en Esterel-v7, une version d’Esterel spécifiquement dédiée au design de circuits complexes.

 

Mais les choses ont progressé rapidement ensuite. A la fin des années 1990, D’autres chercheurs ont inventé une série assez étonnante d’heuristiques (algorithmes approchés) qui permettent de résoudre SAT dans une grande variété de cas pratiques. Les courbes de la figure 3 montrent les progrès extraordinaires de ces systèmes mis en compétition sur plus de 400 problèmes différents, dont certains restent encore non résolus par des méthodes automatiques. Notons que le temps de calcul nécessaire pour résoudre un Sudoku « difficile » est devenu quasi-négligeable ! Les solveurs SAT sont très utilisés en CAO électronique où ils permettent de résoudre de très gros problèmes, mais aussi de plus en plus dans d’autres domaines.

 

D’autres solveurs plus riches fondés sur les mêmes principes sont les solveurs SMT (Satisfaction Modulo Theories) qui enrichissent le calcul booléen avec des théories variées, comme celles des nombres avec des opérations assez simples (pas de multiplication) ou d’autres plus spécialisées. Ils sont plus difficiles à utiliser et plus chers, mais ont aussi obtenu de beaux succès en preuves d’assertions de programmes.

Plusieurs systèmes de preuve de spécification ou de programmes fondés sur SAT et SMT sont développés et appliqués à travers le monde. 

Les preuves totales en logique formelle

Le domaine le plus ambitieux est celui des preuves totales en logique formelle. Il a été initié par le travail pionnier de Robin Milner (prix Turing 1991) sur son système LCF (Logic for Computable Functions)⁹.

Ensuite ont été développés d’autres systèmes comme HOL par Michael Gordon, Isabelle par Larry Paulson et Tobias Nipkow, et Coq par plusieurs équipes françaises — ce dernier en application du Calcul des Constructions de Gérard Huet et Thierry Coquand. Chacun de ces systèmes est fondé sur une logique très générale dite d’ordre supérieur avec laquelle on peut quantifier aussi bien les fonctions que les variables, ce qui procure une très grande expressivité — mais qui n’est pas toujours facile à maîtriser. Il faut aussi citer le prouveur TLA+ de Leslie Lamport, qui n’utilise que la logique du premier ordre et s’attaque lui aux algorithmes distribués, sujet difficile dont je ne parlerai pas ici. 

La première preuve totale de grande importance a été faite par 2002 Harrison chez Intel avec son système HOL Light, pour vérifier la correction de l’unité arithmétique révisée du Pentium Pro. Celle-ci contenait au départ un bug subtil de division, qui avait été détecté par des clients en 1994 et a coûté officiellement 475 millions de dollars à Intel ! L’algorithme de division utilisé était efficace mais subtil, et la preuve formelle de sa version corrigée a vraiment changé le domaine. Les preuves de corrections de ce type ont été depuis étendues à bien d’autres fonctions critiques des circuits inaccessibles pour les méthodes SAT.

Ensuite, l’équipe de Gerwin Klein et Gernot Heiser au labo NICTA de Sydney a pu complètement prouver avec Isabelle la correction du noyau de système d’exploitation industriel seL4, une très belle réalisation. 

Mais ce qui a vraiment démontré le changement d’échelle qu’on pouvait atteindre avec la preuve automatique a d’abord concerné les mathématiques : mon ancien thésard Georges Gonthier, Médaille d’or aux Olympiades de mathématiques mais fondamentalement informaticien, a réussi deux exploits : le premier est d’avoir une preuve complètement formelle et en machine du fameux théorème des 4 couleurs sur les cartes planaires, qui avait connu plusieurs preuves fausses entre 1879 et 1976, jusqu’à ce que les mathématiciens Kenneth Appel et Wolfgang Haken aient pu réaliser une preuve en deux temps : d’abord avec un papier de maths pures montrant qu’on peut se contenter d’étudier un nombre fini de cartes (1478), puis par une étude informatique indépendante pour chacune de ces cartes sur un IBM de l’époque. Les mathématiciens avaient accepté le papier théorique, mais restaient sceptiques sur les résultats de l’ordinateur. Gonthier et Benjamin Werner ont réussi à prouver le théorème intégralement en Coq en simplifiant aussi la preuve mathématique (qui n’était pas si parfaite que ça), exploit retentissant à l’époque.

Puis Gonthier et son équipe se sont attaqués à un résultat mathématique d’un tout autre calibre, le théorème de Feit-Thompson sur la classification des groupes finis à nombre impair d’éléments. Sa preuve mathématique initiale en avait été publiée en 1963, puis de petites erreurs y ont été corrigées jusqu’en 1992, moment où la preuve finale de plus de 250 pages de maths dures a été publiée. Elle a été formalisée en Coq puis formellement vérifiée en 2012. La formalisation de la preuve est difficile, mais sa vérification automatique ne demande maintenant que quelques dizaines de minutes de CPU sur un ordinateur banal avec un programme de vérification pas compliqué. Tout ce travail a aussi en partie changé la façon de voir les preuves mathématiques, les mathématiciens cherchant de plus en plus à intégrer maths classiques et maths sur ordinateur. Ceci a été bien expliqué par l’immense mathématicien Terence Tao quand il a reçu la Médaille d’Or de l’Académie des sciences en 2023.

Mais revenons à l’informatique. Les exploits de Coq en maths ont encouragé Xavier Leroy, chercheur à l’Inria devenu Professeur au Collège de France en 2019, à utiliser Coq avec sa forte équipe pour prouver la correction dans tous les cas d’un compilateur C nommé CompCert pour Compilateur Certifié¹⁰. Nous avons vu précédemment que de très nombreux bugs ont été trouvés par Csmith sur tous les compilateurs classiques. Mais il n’en a bien sûr trouvé aucun sur les codes générés par CompCert. Notons que celui-ci se contente de compiler un sous-ensemble de C parfaitement défini, qui correspond à ce qui est majoritairement utilisé par les industriels de l’avionique, du spatial, etc., domaines dans lesquels éviter les bugs est essentiel ; en effet, le langage C complet est très ancien et comporte pas mal de zones d’ombre. Aux USA, un grand projet nomme DeepSpec a été ensuite lancé dans diverses universités pour prouver des chaînes de programmes cruciaux dans le développement d’application, voir deepspec.org.

Eh oui, les progrès en logique formelle d’ordre supérieur, sujet autrefois considéré comme aride et difficile, ont des retombées tangibles par rapport à un des problèmes pratiques les plus importants de l’informatique — au moins pour les gens sérieux, l’élimination des bugs !

Conclusion

J’espère avoir convaincu le lecteur que les erreurs (bugs) sont intrinsèques à l’informatique, et qu’elles peuvent aussi servir de points d’entrée à de graves attaques de sécurité informatique. Leur ubiquité est en quelque sorte favorisée par une trop grande ignorance du public général sur les sujets informatiques et en particulier sur la vraie nature des bugs, ignorance encore répandue dans un certain nombre d’industries et aussi chez trop de scientifiques. Mais il n’y a pas de fatalité : des solutions existent à différents niveaux, du test bien conduit aux preuves totales de bon comportement en passant par plusieurs niveaux de preuves partielles. Ces solutions reposant vraiment sur de la science dure commencent à être appliquées un peu partout, en particulier là où les organismes se sont fait mordre très fort par des bugs informatiques ou des trous de sécurité. Elles ont encore beaucoup d’avenir.

 

Gérard Berry

La rédaction de ce billet fait suite au colloque Erreurs en sciences, qui s’est tenu le 30 avril 2024 à l’Académie des sciences.

---

Crédits des illustrations :

• Illustration de couverture : la première “mite informatique” (“Computer Bug”), trouvée coincée entre les points du relais # 70, panneau F, du calculateur de relais Mark II Aiken, alors qu’il était en test à l’université de Harvard, le 9 septembre 1947 (source). Les opérateurs ont apposé la mite sur le registre de l’ordinateur, avec l’inscription : “Premier cas réel de découverte d’un bogue” (le terme “débogage” existait déjà ; la découverte d’un véritable bogue était donc un événement amusant). En 1988, le journal, avec la mite toujours collée dedans, se trouvait au Naval Surface Warfare Center Computer Museum de Dahlgren (Virginie, États-Unis), qui l’a daté par erreur du 9 septembre 1945. Le Smithsonian Institute’s National Museum of American History et d’autres sources donnent la date correcte du 9 septembre 1947. L’ordinateur Harvard Mark II n’a été achevé qu’à l’été 1947. Domaine public.
• Figure 1 : le gouffre homme/microprocesseur. Figure extraite de la présentation de G. Berry “À la chasse aux bugs : comment rendre l’informatique plus sûre ?“, donnée le 14 juin 2017 au GDR GPL de Montpellier (diapositive n°12). Tous droits réservés.
• Figure 2 : Figure extraite de la présentation de G. Berry “À la chasse aux bugs : comment rendre l’informatique plus sûre ?“, donnée le 14 juin 2017 au GDR GPL de Montpellier (diapositive n°13). Tous droits réservés.
• Figure 3 : bug du système d’exploitation MacOS repéré par l’auteur. CC-BY 4.0.
• Figure 4 : figure illustrant les progrès des solveurs SAT, fournie par l’auteur. CC-BY 4.0.

1. Officiellement, il faut dire bogue en français, traduction qui a eu un impact négligeable et que je n’emploierai pas ici. [↩]
2. Gérard Berry, L’hyperpuissance de l’informatique, Paris : Odile Jacob, octobre 2017. [↩]
3. Je ne dis pas « intelligent », car je n’ai jamais trouvé de définition claire de ce mot dans les dictionnaires… [↩]
4. Les erreurs « hardware » existent, mais elles sont rarissimes en pratique et quasiment toujours détectées. [↩]
5. C’était la vitesse horizontale, en fait écrite en mode write-only, comme on dit dans le jargon informatique. [↩]
6. Exponentiel, comme disent souvent les journalistes, mais sans savoir vraiment par rapport à quoi… [↩]
7. Feu le langage Esterel v7 que j’avais développé avec succès chez Esterel Technologies avec une forte équipe était lui défini mathématiquement, mais il n’est hélas plus disponible à cause de la crise de 2008… [↩]
8. Avec des numéros de case mémoire en dur[1], on est en 1947 ! [↩]
9. C’est avec lui que j’ai eu l’honneur de vraiment débuter ma carrière par le plus grand des hasards en 1972, on n’est jamais à l’abri d’un coup de bol ! [↩]
10. En fait, le code généré n’est strictement équivalent au code source que si le compilateur termine ; s’il se crashe, ce qui n’arrive pas en pratique, c’est ennuyeux mais sans ambiguïté, et bien moins que la génération d’un code faux. [↩]

---

---