Antoine Miné, ERC Consolidator Grant 2015
Les erreurs de programmation sont omniprésentes avec des conséquences allant de la frustration des utilisateurs à d’énormes pertes économiques ou humaines. Les méthodes de vérification des programmes sont coûteuses en temps et en expertise, c’est pourquoi seules les industries peuvent généralement les appliquer. Le projet ERC Mopsa d’Antoine Miné, enseignant-chercheur à l’Université Pierre et Marie Curie et membre du Laboratoire d’informatique de Paris 6 (LIP6 - CNRS/UPMC), vise à simplifier cette démarche en élargissant les méthodes d’analyse statique par interprétation abstraite et en les intégrant dans une plate-forme open-source pour que tout développeur puisse vérifier son programme.
Pour s’assurer de l’absence de bugs dans les logiciels informatiques, plusieurs techniques existent. Les techniques les plus répandues, basées sur le test, n’examinent qu’un échantillon des exécutions possibles d’un programme, et ne peuvent donc garantir l’absence de bug. Les méthodes formelles cherchent au contraire l’exhaustivité. Les méthodes traditionnelles de model-checking, qui permettent de vérifier des modèles assez complexes sur de petits systèmes, ne suffisent pas à éliminer toutes les erreurs car elles sont basées sur des modèles simplifiés. Des techniques de vérification par analyse statique ont été développées, mais uniquement pour les besoins des industries les plus critiques. Antoine Miné a notamment travaillé dans ce cadre sur la conception du logiciel Astrée aujourd’hui utilisé par Airbus. Le but de l’ERC Mopsa est d’étendre ces méthodes pour qu’elles soient utilisables dans des contextes plus larges.
La vérification par analyse statique a en effet plusieurs avantages. Les outils qui l’emploient sont automatiques, la vérification d’un logiciel est faite par un autre logiciel, avec le moins d’assistance de l’utilisateur possible. Cela permet un passage à l’échelle pour un traitement de logiciels de plusieurs millions de lignes, de plus en plus courants aujourd’hui. D’autre part, les outils analysent directement le code du logiciel et non un modèle simplifié, il y a un lien direct entre le code analysé et le code exécuté, pour qu’ainsi aucune caractéristique ne soit perdue.
En tirant parti de l’interprétation abstraite, l’analyse statique permet également de contourner les problèmes d’indécidabilité, où les méthodes classiques ne permettent pas de résolution complète. La méthode prévoit ainsi de faire une approximation du programme dans le pire des cas, comme si au supermarché en prenant plusieurs articles à 6,99€, 8,49€, etc., vous estimiez qu’ils coûtent tous 10€ pour calculer plus facilement le prix total tout en étant sûr de ne pas dépasser votre budget. En surapproximant les bornes de la variable à chaque calcul, on s’assure que les bornes ne seront jamais dépassées. Les détails qui ne sont pas utiles pour la correction du programme sont ainsi laissés de côté, alors qu’ils étaient potentiellement bloquants pour le problème d’indécidabilité. La version abstraite du programme est créée automatiquement au fur et à mesure de l’exploration du programme.
La méthode permet d’éviter le problème des faux négatifs, où des erreurs ne sont pas détectées, car par construction le pire cas est envisagé. Les fausses alarmes en revanche sont possibles, si l’abstraction du programme est un peu trop « large » et identifie des risques qui n’existent pas. Toute la difficulté pour Antoine Miné est donc d’être à la fois suffisamment précis pour prouver que le programme est correct, mais de trouver la bonne adaptation parmi les constellations d’abstractions pour que la vérification se fasse de façon efficace.
Après avoir travaillé dans le contexte spécifique et bien contrôlé des systèmes embarqués critiques, Antoine Miné souhaite apporter l’analyse statique à l’étape supérieure en touchant des pans plus grands de l’informatique, et en s’attaquant à des logiciels plus grands, plus complexes et hétérogènes. Il souhaite également se concentrer sur les logiciels open-source qui sont facilement disponibles et très répandus. Ce passage à l’échelle pourrait s’appliquer tout particulièrement à l’ensemble des technologies au cœur de l’internet, sur lequel l’analyse statique pourrait être appliquée pour certifier un Internet plus sûr. En effet, des serveurs de noms ou services web ne sont pas considérés comme des logiciels critiques, mais s’il y avait des vulnérabilités exploitables, les conséquences pourraient être néfastes sur la société.
La difficulté vient du fait que ces logiciels sont écrits de manière beaucoup plus libérale : contrairement aux logiciels critiques, les développeurs ne se limitent ni sur les traits de langages, ni sur la longueur du code du programme. D’autre part, de plus en plus de logiciels sont écrits dans des langages dynamiques comme Python. Ces langages ont le plus à bénéficier de l’analyse statique qui permet de déterminer le plus de comportements possibles dès la compilation, pour rendre le programme plus prévisible.
L’aboutissement de ce projet se traduira par la mise en place d’une plate-forme open-source mettant à disposition les méthodes développées. Il existe à l’heure actuelle peu d’analyses statiques qui soient open-source, ce qui constitue un frein à leur développement. De plus, ouvrir l’analyse statique à des logiciels variés demande de travailler sur différentes classes de langages, ce qui correspond à un travail trop important pour une seule équipe. La volonté d’Antoine Miné est de créer un mouvement de chercheurs, voire même de développeurs, qui participeront de manière libre à ces recherches. En étant utile au plus grand nombre, il espère que les utilisateurs se mobiliseront pour contribuer eux aussi à l’amélioration de la méthode.