Un compilateur de niveau industriel
Dans le sillage de l'assistant de preuves Coq, en 2013, le logiciel CompCert vient de devenir le second logiciel issu de la recherche fondamentale Inria à obtenir un ACM Software Award, décerné aux États-Unis. Sept des chercheurs qui ont le plus contribué à son développement, aux côtés d'Inria, ont été récompensés par l'ACM (Association for Computing Machinery) : il s'agit de Xavier Leroy, professeur au Collège de France depuis 2018 et précédemment directeur de recherche chez Inria, Sandrine Blazy (Université de Rennes 1), Zaynah Dargaye (Nomadic Labs), Jacques-Henri Jourdan (CNRS), Jean-Baptiste Tristan (Boston College) et les ingénieurs Michael Schmidt et Bernhard Schommer (de l'entreprise allemande AbsInt).
CompCert, créé en 2005 dans sa première version, est un compilateur de niveau industriel pour le langage de programmation C. Qu'est-ce qu’un compilateur ? « C'est en quelque sorte un traducteur », résume Xavier Leroy, l'un des chercheurs de l'équipe-projet Cambium, commune au centre Inria de Paris et au Collège de France. « En tant que développeurs, nous écrivons du code dans différents langages de programmation (C, C++, Java...), dits de haut niveau, que nous humains pouvons écrire et comprendre, précise ce spécialiste, par ailleurs connu pour être le principal concepteur du langage de programmation OCaml. Mais pour que ce code s'exécute sur une machine, il faut le traduire en langage machine (des instructions codées, à l'aide de nombres, etc). C'est là qu'intervient le compilateur : il traduit le langage compréhensible par les humains en un langage exécutable par la machine. »
Un système de preuve d'exactitude vérifiée mécaniquement
Pourquoi s'être focalisé sur le langage C ? Tout simplement parce que ce langage, ou ses variantes (comme Caml ou OCaml), est historiquement utilisé pour de nombreux systèmes critiques. « Traditionnellement tous les codes de bas niveau, proches de la machine, sont écrits en C – même si des alternatives intéressantes, comme RUST, commencent à émerger, explique Xavier Leroy. On peut citer les systèmes d'exploitation (Linux, Windows, Mac OS), mais aussi, et c'est ce qui nous intéresse particulièrement pour CompCert, tous les logiciels critiques embarqués dans les avions, les voitures, les centrales nucléaires, les métros automatiques, les équipements médicaux… » Dans ces domaines, un bug serait désastreux et les erreurs sur le code compilé ne sont pas permises.
Comment savoir si la traduction (le code compilé) est de bonne qualité ? Il faut tester, et encore tester. Mais les essais sont difficiles, voire impossibles à réaliser de façon exhaustive sur des logiciels parfois décrits par des dizaines de millions de lignes de code et dans de multiples configurations. Les développeurs de CompCert ont donc fait le choix d'associer à leur logiciel une preuve d'exactitude vérifiée mécaniquement, unique en son genre. Le code du compilateur CompCert est formellement vérifié à l'aide de preuves mathématiques assistées par machine de sorte à éviter que de mauvaises compilations (on parle de « miscompilation », en anglais) puissent se produire : il peut ainsi être prouvé que le code compilé se comporte exactement sur la machine comme cela a été spécifié dans le programme C d'origine.
Utilisation des méthodes formelles
Pour se passer des tests « classiques », les chercheurs ont fait le choix de s'intéresser à d'autres méthodes de vérification issues du monde de la recherche : les méthodes formelles. « C'est un vieux rêve dans l'informatique, souligne Xavier Leroy. L'idée consiste à raisonner à l'aide de la logique mathématique sur le fonctionnement d'un programme, afin de démontrer sa validité par rapport à une certaine spécification. Elle a d'abord été exprimée par Alan Turing dans les années 1940-50, puis elle est revenue sur le devant de la scène à la fin des années 1960, et est restée essentiellement théorique jusque dans les années 2000. »
Quelle est la différence aujourd'hui ? « Nous avons réussi à créer des outils de vérification statiques (appelés analyseurs statiques) qui permettent d'automatiser la vérification de déduction de preuves mathématiques sur le code source des logiciels, ajoute le chercheur. Le problème était aussi d'arriver à utiliser ces mêmes méthodes pour vérifier mathématiquement la fiabilité du compilateur. »
Pour cela, les chercheurs de Cambium se sont appuyés sur Coq, un logiciel en open source développé par Inria. « Cette solution, qui est un assistant à la preuve formelle, nous permet de nous appuyer sur la puissance de la machine pour vérifier des preuves sur le compilateur lui-même », souligne Xavier Leroy. Et ce faisant de répondre aux attentes de nombreux industriels, comme Airbus, qui « s'intéressent à la vérification de compilateur » : « Après avoir chassé les bugs dans un programme, le challenge pour eux est de chasser les bugs dans le compilateur qui va produire le code exécutable. »
De nouvelles déclinaisons en perspective
Les découvertes de Cambium, au travers de CompCert, se poursuivent au sein d'Inria, notamment pour vérifier des propriétés de complexité en temps d’exécution ou en consommation de mémoire des programmes. D’autres domaines d’application restent à explorer, tels les smart contracts (des contrats utilisant la technologie de la blockchain). À plus long terme, il pourrait aussi être intéressant de le rendre compatible avec les programmes d'intelligence artificielle obtenus par apprentissage statistique (machine learning), qui ont la particularité de ne pas être codés de façon conventionnelle et d'être extrêmement volumineux.
Pour les utilisateurs, CompCert peut être téléchargé dès à présent dans une version gratuite, pour évaluation, enseignement, recherche et toute utilisation non commerciale. Le logiciel est aussi disponible dans une version commerciale, distribuée par AbsInt, un spécialiste des outils de vérification formels très présent dans les secteurs européens de l'automobile, de l'aéronautique et du nucléaire.
