“Le logiciel zéro bug est possible”

Chercheur à l’Inria, Xavier Leroy a ciblé une bonne partie de ses recherches autour de la qualité des logiciels. Des travaux récompensés par plusieurs prix dont le prestigieux Milner Award en 2016. Il revient avec nous sur les moyens à mettre en œuvre pour obtenir des logiciels — presque — parfaits.  

De plus en plus d’incidents et accidents sont imputés — éventuellement à tort — aux logiciels. Le logiciel zéro bug ne peut-il pas exister ?

Si. Au risque d’en surprendre plus d’un, et a contrario de nombre de mes collègues, je pense que le logiciel sans bug est possible. Plus précisément, il n’existe pas d’impossibilité fondamentale interdisant ce résultat. Bien sûr, l’expérience quotidienne témoigne du contraire. Mais quand le logiciel devient critique, quand des vies humaines sont en jeu, les organisations qui le produisent investissent des moyens considérables pour le fiabiliser. L’aéronautique, le nucléaire, le ferroviaire — malgré la dernière panne à Montparnasse… —, les fabricants de cartes à puce et d’autres travaillent dans cette logique. Et les résultats obtenus sont probants. Chez Airbus, les bugs liés aux logiciels d’avionique, chargés des commandes de vol, sont quasiment inconnus.

Pourtant, quelques incidents ou accidents ont toujours lieu…

C’est vrai, mais généralement ce ne sont pas de simples bugs informatiques. Continuons l’exemple des commandes électroniques de vol. Le remplacement de la mécanique par du logiciel sur les commandes de vol, entre le palonnier et les ailerons par exemple, remonte aux années 80. C’est ce qui a été mis en place sur l’A320. Dans son cahier des charges initial, l’avionneur avait placé la barre haut : une erreur sur 10 millions d’heures de vol, bien au-delà des taux habituels dans l’informatique. Après environ 50 millions d’heures de vol, aucun incident causé par ce logiciel n’a été constaté. Par contre, d’autres accidents sont survenus qui ne sont pas dus à des bugs mais, entre autres, à des questions de modélisation. En d’autres termes, le logiciel a fait exactement ce qui lui était demandé. L’accident est survenu suite à des événements non prévus, et donc non pris en charge par le logiciel.

Pouvez-vous nous détailler un exemple ?

Le 14 septembre 1993, un Airbus de la Lufthansa s’est posé dans des conditions météo déplorables à Varsovie. Il a atterri en crabe et, piste inondée oblige, est parti en aquaplaning. Ce qui rendait caduque la possibilité d’utiliser le freinage classique. Dans ce cas, la procédure prévoit d’inverser la poussée des réacteurs pour freiner. Or le logiciel n’a pas pris en compte l’ordre de rétro-poussée donné par les pilotes. L’avion est donc sorti de piste et a heurté un pylône. Un des passagers et un des pilotes sont morts. L’enquête a démontré que le logiciel avait fait exactement ce pourquoi il était programmé. À savoir, la rétro-poussée n’était possible que si un minimum de 12 tonnes portait sur chacun des trois trains d’atterrissage, ce, pour empêcher cette action en vol car elle aurait alors des conséquences désastreuses. Dans le cas de cet atterrissage, l’un des trois trains était délesté et ne respectait pas ce critère des 12 tonnes. Le problème était lié à une modélisation qui n’avait pas prévu tous les cas de figures. Depuis cet accident, les critères appliqués par le logiciel ont été revus pour couvrir tous les atterrissages, même les plus délicats.

Quelles méthodes Airbus, et plus largement les autres industriels, utilisent-ils pour atteindre le zéro bug ?

Il s’agit de combiner les meilleures pratiques de modélisation et de programmation avec une validation extrêmement poussée du logiciel. Par exemple, il est plus sûr de ne pas utiliser tout langage de programmation pour tout type d’usage. Ainsi, Le C n’est pas très sûr, et il vaut mieux mettre en œuvre des langages spécialisés, par exemple Scade et Simulink, pour les applications de contrôle commande (capteurs et actionneurs). S’ils ne disposent que d’une expressivité restreinte — certains de ces langages ne permettent même pas de faire des boucles —, ils demeurent a contrario plus faciles à contrôler, à suivre sur la consommation de la mémoire et, au final, leur utilisation limite la possibilité de bugs. Deuxième étape, le développement doit être systématiquement validé par des tests extrêmement rigoureux. Souvent, la préparation et l’administration des tests est ce qui prend le plus de temps et coûte le plus cher dans un développement de logiciel critique. Mais, comme l’a très bien résumé Edsger Dijkstra, un des fondateurs de la science informatique, tester un logiciel peut identifier la présence de bugs, mais pas garantir leur absence ! D’où l’apparition d’une troisième grande étape, l’utilisation des méthodes formelles pour améliorer encore la qualité.

Pourquoi et comment utiliser ces méthodes formelles ? Pouvez-vous décrire leur fonctionnement ?

Les méthodes formelles reposent sur une approche mathématique qui ne remplace pas, mais complète l’approche empirique du test. Très schématiquement, il s’agit de transcrire le code en équations et de démontrer mathématiquement des propriétés de ces équations. Ces méthodes ont émergé dans le milieu universitaire dans les années 1965-1975. Mais il a fallu attendre les années 2000 et l’apparition d’outils qui automatisent ces méthodes formelles pour qu’elles commencent à être utilisées dans l’industrie. À la main, avec un crayon et du papier, on peut appliquer ces méthodes à quelques dizaines de lignes de code. On est loin des 100 000 lignes des commandes de vol de l’A320 et du million de lignes de celles de l’A380 ! En revanche, un analyseur statique, un outil logiciel mettant en œuvre des méthodes formelles, peut analyser ce million de lignes en quelques dizaines d’heures. Un tel outil assure que le code ne présente pas de bugs de type débordement de tableau ou de pile. D’autres outils donnent des garanties sur les temps d’exécution indispensables pour les systèmes destinés au temps réel. Par exemple, un autre outil, l’assistant de preuves Coq, permet de construire des preuves avec le concours de l’utilisateur, puis de tester automatiquement le logiciel pour vérifier que toutes les déductions logiques formulées par le code sont valides.

D’autres facteurs sont néanmoins à prendre en compte. L’étape de compilation pose apparemment certains problèmes.

Tout à fait. Pour rappel, un compilateur a pour fonction de traduire en code machine un langage de haut niveau. Une fonction de traduction à laquelle se sont ajoutées, au fil du temps, des fonctions d’optimisation pour améliorer les performances. Des tâches complexes, qui génèrent parfois des erreurs indépendamment du code source. Problème numéro un, ces bugs introduits par le compilateur restent par nature inconnus du développeur comme du concepteur. Problème numéro deux, ils sont très difficiles à identifier. Les industriels cherchent à contrôler ces risques en désactivant les options d’optimisation, par exemple. Une approche pas totalement fiable parce qu’elle reste aveugle sur le code machine généré. Pour contourner ce type de problèmes, mon équipe de recherche et moi-même avons développé Comp-Cert, un compilateur capable d’éradiquer tout risque de mauvaise traduction par le biais d’une vérification formelle du compilateur. L’utilisation de méthodes formelles garantit l’exactitude de cette étape de traduction. Ce faisant, elle augmente la confiance que l’on peut avoir dans les résultats d’une vérification formelle du code source. Cette approche intéresse plusieurs grands noms de l’aéronautique et du nucléaire.

Qu’en est-il des tests d’intégration, des interactions entre les différentes grandes parties d’un logiciel ?

Les tests d’intégration et plus encore les tests de £validation par l’utilisateur final restent essentiels. C’est une chose de vérifier, par le test et les méthodes formelles, que le logiciel est conforme à son cahier des charges technique. Mais il est tout aussi important de valider que le logiciel fait bien ce qu’il est censé faire et que ses « actions » sont bien adaptées à la situation réelle. Comme l’atterrissage raté de Varsovie le montre, tester ou simuler des situations réelles reste essentiel. Cette dernière étape doit se concrétiser par des mises en situations réalistes, et ce le plus tôt possible lors du développement du logiciel. Dans l’aéronautique, passée l’étape de tests proprement dite, la suivante consiste à réaliser un banc d’intégration, sorte de maquette regroupant tous les systèmes hydrauliques, électriques et informatiques de l’avion, et de le faire voler — virtuellement — aux commandes d’un pilote d’essai. Une démarche de simulation très poussée qui reste à développer dans beaucoup d’autres industries.

Sur le plan organisationnel, que pensez-vous de l’externalisation des tests et, plus globalement, sur le rôle du développeur ?

La partie vérification et intégration repose, entre autres, sur une bonne coordination entre les équipes de développement et de test. Personnellement, je ne pense pas que l’externalisation complète des tests soit une bonne option. Au contraire, il est préférable d’associer plus étroitement les développeurs aux phases de test et de vérification formelle. Historiquement, le découpage des fonctions pour produire des programmes tenait notamment à des raisons économiques. Développeur et analyste-développeur étaient deux fonctions différentes il n’y a encore pas si longtemps. À l’époque, les ressources humaines étaient moins chères que le temps machine. C’est l’inverse aujourd’hui. Les développeurs travaillent mieux lorsqu’ils reçoivent des retours très rapides sur la qualité de leur code. L’externalisation ne me paraît pas être l’option la plus sûre. Une proximité entre les développeurs et les testeurs, ainsi qu’un accès direct aux outils d’analyse statique, est plus efficace à mon sens.

Qu’en est-il de la maturité des autres secteurs d’activité ?

Il reste encore du pain sur la planche ! Les risques sont souvent encore, malheureusement, bien réels. Un modèle de Toyota a défrayé la chronique avec un accélérateur défaillant. En cause ? Un débordement de pile dans le code source qui corrompait la mémoire : une erreur banale qui aurait pu être facilement détectée par analyse statique lors du développement. Il est vrai que produire un nouveau modèle de véhicule tous les 18 mois semble difficile à rendre compatible avec la réalisation de logiciels de haute qualité. Autre illustration, l’industrie médicale n’a pas complètement intégré la culture du zéro bug. Si les procédures respectent un haut niveau d’exigence sur les effets secondaires des médicaments, les risques découlant de l’usage de logiciels dans les équipements médicaux ne suivent pas les mêmes processus. Le rappel de certains équipements, comme des pacemakers qui présentaient un risque létal pour les patients, en témoigne.

Au-delà des seuls logiciels critiques, que peut apporter cette approche dans les autres applications ?

Toutes les applications gagnent à être améliorées. Même si des vérifications poussées, comme dans le secteur de l’avionique, sont trop coûteuses et non indispensables pour des logiciels non critiques, de bonnes pratiques comme l’utilisation d’outils d’analyse statique sont applicables à de nombreux logiciels. Facteur aggravant pour l’informatique de gestion, pour diverses raisons notamment organisationnelles, les logiciels de cette famille sont souvent hétérogènes, voire « filandreux ». La complexité de ces logiciels reflète surtout la complexité des organisations de nos entreprises et de nos administrations, plus que la difficulté du problème à résoudre. Au-delà des bugs, une démarche de qualité limite les risques en termes de cybersécurité. Un risque qui concerne tous les secteurs d’activité et tous les logiciels. L’utilisation de méthodes formelles permet de détecter non seulement des bugs, mais peut aussi identifier des fuites de données possibles.

Comment voyez-vous l’avenir des tests et des méthodes formelles ? L’Intelligence artificielle va-t-elle changer la donne ?

Les techniques d’apprentissage statistique ou les réseaux de neurones, qui jouent un rôle central dans l’IA, posent de gros problèmes de vérification. Les méthodes formelles contemporaines ont beaucoup de mal à raisonner sur les logiciels obtenus par ces techniques, des logiciels qui sont principalement « appris » à partir d’exemples plutôt que vraiment « écrits ». Même les techniques de test et de revue de code plus traditionnelles ne s’appliquent pas facilement. On ne sait pas relire une matrice de coefficients d’un réseau neuronal, pas plus qu’on ne sait mesurer la couverture d’un jeu de tests sur un tel réseau. Or la traçabilité et la lisibilité des tests sont indispensables pour qualifier un logiciel. En dehors de l’IA, la marge de progression, au niveau théorique comme pour les outils et les méthodes, est grande. La chasse au bug continue.

Propos recueillis par Patrick Brébion

XAVIER LEROY

2016 Prix Milner de laRoyal Society

DEPUIS 2000 Directeur de recherche, Inria

1999-2004 Ingénieur R&D, Trusted Logic

1994-1999 Chargé de recherche, Inria

1993-1994 Post-doctorat, Stanford University

1989-1992 Doctorat en informatique, Université Paris-Diderot

1987-1991 Élève de l’École Normale Supérieure (Paris)

Abonnez-vous à la newsletter hebdo d'IT for Business !

Rejoignez notre liste de diffusion pour recevoir toutes les semaines une sélection d'articles et quelques autres surprises préparées spécialement pour vous par notre rédaction.

ABONNEZ-VOUS !

Nous vous envoyons un e-mail de validation !