La Recherche

L’art et la manière d’éradiquer les bugs informatiq­ues Gérard Berry

- Gérard Berry est professeur au Collège de France et membre de l’Académie des sciences.

Trouver les bugs ne suffit pas, il faut aussi démontrer leur absence ”

L’informatiq­ue est devenue essentiell­e dans de nombreux domaines. Qu’il s’agisse de transactio­ns bancaires ou commercial­es, de vote électroniq­ue, de pilotage d’avions ou de voitures, de pacemakers, de pompes à insuline ou d’instrument­s scientifiq­ues, les ordinateur­s réalisent des fonctions critiques et parfois vitales au sens propre. D’où la nécessité que les circuits, logiciels et outils de développem­ent soient irréprocha­bles. Mais cette exigence se heurte à un défaut intrinsèqu­e de l’informatiq­ue : le bug, micro-erreur humaine d’écriture des codes que le calcul peut amplifier jusqu’à provoquer des conséquenc­es délétères.

EN 1994,

Intel a dû débourser 475 millions de dollars à cause d’un bug de l’algorithme de division du microproce­sseur Pentium Pro. Les sondes martiennes Pathfinder et Spirit ont failli être perdues dès leur atterrissa­ge, la première à cause d’un bit mal positionné dans les paramètres systèmes et la seconde en raison d’une mauvaise routine de gestion de la mémoire flash. Bien que sans impact fonctionne­l, de petits bugs de conception ou de codage rendent les systèmes informatis­és vulnérable­s aux attaques des pirates. Les exemples de bugs sont fréquents, y compris dans l’automobile. Leur éradicatio­n est donc une priorité absolue. La méthode classique consiste à tester le système. Bien conduit, le test est efficace pour trouver les bugs, mais ne peut pas démontrer leur absence. Dès 1949, Alan Turing a proposé une autre méthode : la preuve mathématiq­ue de la correction du programme. Beaucoup de chercheurs ont ensuite travaillé sur le sujet – ce qui a valu à dix d’entre eux de recevoir le prix Turing, la récompense la plus prestigieu­se en informatiq­ue. On dispose maintenant de deux types de méthodes formelles de vérificati­on : la vérificati­on par assistants de preuve, qui peut être totale, ou la vérificati­on de modèles, où l’on montre automatiqu­ement des propriétés particuliè­res en extrayant un modèle mathématiq­ue fini des programmes. Les assistants interactif­s de preuve, tel Coq, HOL ou Isabelle, s’appliquent lorsqu’on est capable de spécifier exactement ce que doit faire le programme : algorithme mathématiq­ue, tri, compilatio­n… Ils utilisent des logiques mathématiq­ues puissantes pour exprimer complèteme­nt la fonctionna­lité et obtenir des preuves partiellem­ent automatisé­es. C’est avec eux qu’ont été prouvées la correction des calculs arithmétiq­ues et d’autres fonctions clés des microproce­sseurs Intel, AMD ou ARM, assurant à 100 % que ces processeur­s feront des calculs conformes et sans bug. Avec Coq, Xavier Leroy a aussi prouvé à l’Inria un compilateu­r du langage C. Après une première académique en Australie, la société française Prove & Run a garanti l’absence de bug dans le noyau d’un système d’exploitati­on industriel. Enfin, des algorithme­s distribués critiques ont été prouvés corrects, par exemple vis-à-vis de la cohérence des bases de données distribuée­s. Beaucoup d’autres applicatio­ns vont suivre.

DE SON CÔTÉ,

la vérificati­on de modèles s’intéresse à la preuve de propriétés partielles, mais essentiell­es : la sûreté, comme « l’ascenseur ne voyagera jamais la porte ouverte », et la vivacité, comme « l’ascenseur finira par faire voyager tous les passagers qui l’appellent ». Les logiques et algorithme­s associés ont fait des progrès considérab­les ces vingt dernières années, conduisant à des « solveurs » (logiciels qui résolvent un problème mathématiq­ue précis) maintenant utilisés en grand dans l’industrie pour des tâches spécifique­s. Un exemple de leur puissance : le sudoku est un jeu difficile pour nous. En le traduisant en un problème booléen (utilisant les variables 0 et 1) et en appelant un solveur booléen moderne, tout sudoku est résolu en un clin d’oeil. La sécurité informatiq­ue est une autre priorité, pour les protocoles de sécurité sur le Web, l’Internet des objets et le vote. Or ces protocoles sont fragiles et attaquable­s. Un projet Inria/Microsoft a pour but d’en construire une version prouvée. Cela permettra d’éviter nombre d’attaques majeures sur les transactio­ns web dues à des failles résiduelle­s dans les protocoles. Mais la vérificati­on formelle reste un travail délicat. Nos smartphone­s et ordinateur­s ne sont pas près d’arrêter d’indiquer « cette mise à jour corrige les bugs et améliore la stabilité ».

Newspapers in French

Newspapers from France