L’Académie des sciences consacre une série de podcasts, en partenariat avec Canal Académies, à l’erreur dans les sciences. Au micro, Étienne Ghys, l’un de ses deux secrétaires perpétuels. Cortex Média a retranscrit ces échanges, à lire ci-dessous.
Quand un programme informatique se trompe, d’où vient réellement l’erreur ? Pour Gérard Berry, la réponse est presque toujours la même : de l’être humain qui a conçu, écrit, assemblé ou testé le programme.
Avec Étienne Ghys, l’informaticien et ancien professeur au Collège de France revient sur la nature des bugs, les limites des tests, la preuve formelle des programmes, les erreurs qui ont failli condamner des robots martiens et les méthodes utilisées pour rendre les systèmes critiques plus sûrs.
Étienne Ghys : Gérard, tu es informaticien, ancien professeur au Collège de France. J’aime bien quand tu dis que tu es émérite.
Gérard Berry : Émérite, ça veut dire sorti du mérite.
Étienne Ghys : Tu as beaucoup travaillé sur les bugs et la certification des programmes. Tu vas participer à un colloque sur les erreurs en science, et tu voudrais qu’on se concentre sur les erreurs humaines en informatique. C’est bien ça ?
Gérard Berry : Oui, parce qu’il n’y a quasiment pas d’erreur non humaine en informatique. La physique des circuits est presque parfaite, et elle peut être très bien surveillée et corrigée. Ce n’est pas là qu’est le problème. Le problème, c’est chez les hommes.
Pour une raison extrêmement simple : l’ordinateur est une machine exactement à l’opposé de l’homme. J’ai coutume de dire que l’homme a trois caractéristiques. La première, c’est qu’il a des idées, parfois justes, parfois fausses — ce n’est pas très grave. La deuxième, c’est qu’il est très lent comparé à un ordinateur. Et la troisième, c’est qu’il fait beaucoup d’erreurs — mais ça ne le gêne pas trop, parce qu’il les corrige, et qu’en général elles n’ont pas beaucoup de conséquences.
L’ordinateur est exactement à l’envers. Il est totalement idiot : ses instructions sont d’une bêtise absolue, il ne sait pas du tout ce qu’il fait. Il est extraordinairement rapide, et il ne fait jamais d’erreur.
Étienne Ghys : Jamais d’erreur ? Pas même un rayon cosmique ?
Gérard Berry : Ça peut arriver, mais ça se détecte. Il y a beaucoup de codes correcteurs à l’intérieur des ordinateurs, surtout ceux qui sont critiques. Ce n’est pas impossible, mais disons que c’est à peu près invisible dans le domaine des bugs.
Les rayons cosmiques ne concernent pas trop les avions, mais pour les satellites, c’est un problème — et il y a des technologies spéciales. Je dirais que la physique n’est pas du tout un embêtement pour nous.
Étienne Ghys : Donc quand il y a une erreur informatique : cherchez l’homme.
Gérard Berry : Cherchez l’homme, parce que l’homme est incapable d’écrire de très longs textes — ça peut être des millions, des dizaines de millions de lignes — sans faire d’erreur. C’est extrêmement difficile.
Les gens qui ne connaissent pas du tout le sujet parlent des « petits génies de la programmation ». Ça n’existe pas. Un autodidacte mal formé va se tromper tout le temps, mais il ne s’en apercevra pas, parce qu’il ne testera jamais ses programmes correctement : il testera le comportement qui lui plaît, pas celui qui lui déplaît. C’est absolument constant. C’est vrai pour les gens non formés, et c’est vrai pour les très gros projets, qui souvent meurent de lourdeur.
Théorèmes et preuves
Étienne Ghys : En mathématiques, il y a parfois de très longs textes qui contiennent des erreurs çà et là, mais il y a une espèce de stabilité : les petites erreurs se repèrent assez facilement. Est-ce la même chose pour un programme ?
Gérard Berry : Là, c’est vraiment une différence absolue.
En mathématiques, on s’intéresse aux théorèmes, et on fait des preuves pour les garantir. Il y a en général plus d’information dans le théorème que dans la preuve. Une preuve peut être fausse très longtemps, puis corrigée.
Les mathématiques fabriquent essentiellement des théorèmes. Les programmes, eux, fabriquent essentiellement des preuves. On peut considérer qu’ils produisent des théorèmes, mais ces théorèmes sont sans intérêt : ce sont les preuves qui comptent. Par exemple, il y a un théorème trivial qui dit qu’on peut trier une liste ; un algorithme de tri, c’est une preuve qu’on peut trier une liste.
Et le problème, c’est que l’ordinateur exécute la preuve. S’il y a un bug dans la preuve, il le fait avec une conscience professionnelle absolue.
Le jeu du carrelage
Gérard Berry : Je prends un exemple tout bête. On prend un carrelage, et on trace un trajet d’un point à un autre avec trois ordres : tout droit, à droite, à gauche. À chaque croisement des lignes, on fait ce qui est indiqué.
Je fais ça dans mes classes, avec des enfants comme avec des adultes, c’est pareil. Je leur donne un texte : l’un le lit, l’autre l’exécute avec ses pieds. Ils n’arrivent absolument jamais au bon endroit. Sur un texte de quinze mots. Simplement parce que, pour nous, l’erreur n’est pas un problème. Ils sont extrêmement surpris de ne pas y arriver — c’est rigolo.
Alors il faut comprendre qu’un texte de programme, ça fait des millions de caractères.
Les mathématiciens parlent d’algorithmes, et l’algorithmique, c’est quelque chose d’assez compact, qui peut être très difficile mathématiquement, mais compact et malin, avec des textes qui ne sont pas très grands. Un programme, ce n’est pas ça : c’est énormément d’algorithmes. Et quand on prend un algorithme très malin et qu’on le traduit en programme, il arrive souvent qu’il soit faux.
En plus, il y a maintenant beaucoup de programmes parallèles, qui communiquent et travaillent en coordination. Et ça, c’est absolument terrible pour les erreurs.
Les trous de sécurité
Gérard Berry : Qu’est-ce que ça peut faire, un bug ? Énormément de choses.
Avant, on testait le comportement normal des programmes. Maintenant, ce n’est pas ça qu’il faut faire : il faut casser tous les comportements. Pourquoi ? Parce qu’un programme qui écrit dans une zone mémoire qu’il n’a pas allouée — c’est extrêmement fréquent — est à la racine de je dirais 80 % des trous de sécurité. Ça ne se voit pas quand on exécute le programme. Mais quand on le regarde de l’extérieur, quand on est un chercheur en sécurité mal intentionné, on peut utiliser ça pour entrer dans le système complet.
Étienne Ghys : Peux-tu donner des exemples qui concernent monsieur et madame Tout-le-Monde ?
Gérard Berry : Tous. Les systèmes d’exploitation, par exemple. Regardez les messages d’Apple ou de Windows : ils les rédigent très bien pour qu’on ne comprenne pas. Ils disent : « correction d’une écriture hors mémoire qui permet à un attaquant d’exécuter un code assembleur en mode superviseur ».
C’est incompréhensible pour le commun des mortels. Ça veut dire : correction d’un énorme trou qui permet à quelqu’un de prendre le pouvoir total sur la machine. C’est aussi simple que ça. Et ce n’est pas du comportement normal — or, en général, on ne teste que le comportement normal.
Les robots martiens
Étienne Ghys : Tu dis qu’il faut tester toutes les situations, y compris anormales. Elles sont probablement beaucoup trop nombreuses pour tout tester, non ?
Gérard Berry : C’est extrêmement intéressant. Prenez les deux robots martiens dont on a beaucoup parlé, Pathfinder et Spirit : ils ont failli mourir à leur naissance. Ils ne redémarraient pas, une fois sur Mars. À cause de bugs extrêmement subtils, très rigolos.
Ils ont été corrigés à distance par les ingénieurs. Sur Spirit, ils ont mis trente-quatre heures — et je crois qu’au bout de trente-six heures, il était mort, il n’y avait plus de batterie. Il redémarrait sans arrêt. Et c’était très bête : un bit à changer. Un seul bit dans le système pour que ça marche. Ça a marché.
Étienne Ghys : Pourquoi cette erreur n’a-t-elle pas été détectée au sol avant le départ ?
Gérard Berry : Parce qu’elle ne s’était pas produite. Elle était dans un cas particulier. Il y avait eu beaucoup d’informations pendant le trajet, ce qui avait un peu saturé la mémoire utilisée. La mémoire était allouée, mais mal désallouée, à cause d’une vieille bibliothèque — parce que les gens ne changent pas un programme qui marche. Très dangereux.
C’est vicieux, voilà le problème.
Tester ou prouver
Gérard Berry : Il y a deux méthodes. Il y a le test, qui fait tomber tout un tas de trucs triviaux. Dijkstra disait en 1971 : le test permet de trouver des erreurs, mais jamais de prouver qu’il n’y en a pas. C’est la méthode universelle, je dirais.
Et puis il y a une autre méthode, introduite par Turing — personne ne le sait — dans une note manuscrite de 1945, où il disait : tester les programmes ne suffit pas, il faut les prouver. Il donnait la preuve d’un programme en langage machine, avec des adresses en dur, même pas des lettres. Un programme pour la factorielle, alors qu’il n’y avait pas de multiplieur dans sa machine. Et il le prouvait, avec une méthode qu’on appelle les assertions, toujours utilisée, généralement attribuée à Floyd — mais c’est Turing.
Étienne Ghys : Donc soit on teste le programme dans les circonstances les plus variées possibles, soit on essaie de le démontrer comme un théorème.
Gérard Berry : C’est ça. Il y a la méthode vraiment informatique : on écrit rigoureusement, avec de bons langages, puis on teste. Et l’autre méthode, c’est la logique. Il y a de la logique formelle extrêmement puissante pour faire ça.
Par exemple, dans les circuits, on fait des preuves en calcul booléen. Le calcul booléen, c’est l’un des grands mystères des mathématiques. Avec ce calcul qu’on pensait absolument impossible il y a vingt ans, il existe maintenant des algorithmes absolument remarquables — dont on ne sait d’ailleurs pas pourquoi ils marchent, mais c’est comme ça. C’est un problème NP-complet : si on le résout, on gagne un million de dollars et probablement le prix Turing. Ce sont les problèmes les plus durs qui existent.
Je m’en suis beaucoup servi personnellement, sur des avions par exemple. Ça sert aussi à faire de très grandes preuves en mathématiques, en combinatoire ou en théorie des nombres — typiquement pour trouver des contre-exemples, avec des milliers de processeurs.
Il y a eu un événement marquant : le Pentium, qui faisait de temps en temps une mauvaise division. Ça a coûté extraordinairement cher à Intel, cinq cents millions de dollars. Les bugs, c’est cher. Le diviseur corrigé a été prouvé correct dans tous les cas, avec un système anglais appelé HOL. Or, pour la division, le nombre de cas est absolument incroyable.
Faut-il avoir confiance ?
Étienne Ghys : Quand on t’écoute, ça donne un peu froid dans le dos. Dois-je avoir confiance dans mon ordinateur ? Quand je monte dans un avion ?
Gérard Berry : Il y a de grosses différences. Ce qui est connecté à Internet et ce qui ne l’est pas, ce n’est pas pareil. Quand on n’est pas connecté, envahir n’est pas très facile — c’est possible, mais pas facile.
C’est le cas de l’avion. Normalement, l’avion est très ségrégué : les commandes de vol des Airbus, je sais qu’elles sont faites avec toute notre technologie française, et ce sont des ordinateurs disjoints des autres réseaux. Dès qu’on partage quelque chose, il faut être absolument sûr qu’il n’y a pas de fuite. Mais si on ne partage pas, c’est plus lourd. Les compromis sont durs à trouver en pratique.
Dix millions de lignes
Étienne Ghys : Moi, mathématicien, j’ai toujours dit à mes étudiants qu’ils n’ont pas le droit, déontologiquement, d’utiliser un théorème publié ailleurs et qu’ils ne comprennent pas. Ils doivent maîtriser ce qu’ils utilisent, au moins dans l’esprit. Est-ce que quelque chose de cette nature existe en informatique ?
Gérard Berry : Ça ne peut pas. C’est justement le problème de la taille.
Les mathématiques, fondamentalement, ne font rien. Elles produisent des théorèmes — c’est beaucoup — mais elles ne font rien dans le monde réel. Sur un ordinateur tout nu, en revanche, on ne peut rien faire. Ce qu’on appelle le démarrage des ordinateurs, le fait qu’on puisse faire quelque chose avec eux, est dû à des millions de lignes de code superposées les unes aux autres.
Des bibliothèques dont on ne sait pas ce qu’il y a dedans et qu’on importe. On sait ce qu’elles font — il y a de vagues descriptions, parfois mathématiques, mais c’est très rare. Et on dépend de Windows, de macOS : des choses qui font des dizaines de millions de lignes de code, voire davantage.
On ne peut pas avoir cette exigence-là. Aucun homme ne peut lire dix millions de lignes de code. Il faut vivre avec. Et c’est pour ça que la rigueur doit être vraiment augmentée.
On peut le faire, par exemple avec Coq, le système initié par Gérard Huet et Thierry Coquand. Il a d’abord fait ses preuves dans un autre domaine : la démonstration mathématique, avec la preuve entièrement vérifiée en machine, par Georges Gonthier, du théorème de Feit-Thompson sur la classification des groupes d’ordre impair — un théorème dont la preuve mathématique faisait deux cent cinquante pages, publiée en 1963 et corrigée jusque dans les années 2010.
Étienne Ghys : Il ne s’agit pas de trouver la démonstration, il s’agit de la vérifier.
Gérard Berry : Il s’agit de l’écrire, d’abord. Et en Coq, l’écrire et la vérifier, c’est la même chose. C’est la logique constructive.
Étienne Ghys : Je vais défendre mon business : il s’agit d’abord de la trouver.
Gérard Berry : Attention, elle était déjà là. Bien sûr. Ça n’a pas fourni de nouveaux théorèmes — il y en a eu depuis, mais ce n’est pas la question. Ça a démontré la possibilité de faire d’énormes démonstrations.
D’où vient le mot « bug »
Étienne Ghys : Peux-tu me raconter l’origine du mot « bug » ? Ce sont bien des petites bestioles qui corrompaient les programmes ?
Gérard Berry : L’origine fausse et répandue, c’est Grace Hopper — la première informaticienne, celle qui a fait le COBOL, quelqu’un d’extraordinaire. Il y avait beaucoup de femmes à l’époque, bien plus que maintenant. Un insecte s’était coincé dans les rouages de son ordinateur et l’avait planté. J’ai montré au Collège de France une photo de cet insecte.
Mais ce n’est pas de là que vient le mot « bug » : c’est beaucoup plus vieux. Edison employait déjà ce mot, en disant que lorsqu’on fait un très grand projet bien fait, il y a toujours des petits bugs qui viennent vous embêter sur le trajet.
Étienne Ghys : As-tu une musique à recommander ?
Gérard Berry : J’aime la musique classique, le jazz, et la musique contemporaine qui fait dialoguer informatique et humain — ça, c’est vraiment extraordinaire. Et j’ai une grande passion pour la musique indienne, les musiques ethniques.
Je travaille avec Philippe Manoury, qui est le roi de la musique mixte, électroacoustique et humaine. Je pense qu’on peut faire des choses que les hommes seuls ne peuvent pas faire. Un bout de Tensio, par exemple.
