CompCert récompensé par l’ACM pour ses garanties d’absence de bugs

Hantise des informaticiens comme des utilisateurs, le bug se combat parfois très en amont. Le domaine de la vérification déductive est ainsi consacré à établir les meilleures garanties de l’absence d’erreurs dans un programme, notamment grâce à l’apport du raisonnement mathématique. Mais la sémantique des programmes, c’est-à-dire de l’assurance que les machines « comprennent » bien ce qui leur est demandé, doit aussi être préservée.

En effet, le code source d’un programme est écrit dans un langage de programmation compréhensible par des humains, qui n’est pas celui utilisé par la machine. Un autre programme, le compilateur, va donc traduire ces instructions, mais, comme pour les langues étrangères, des contresens et des erreurs peuvent apparaître. Or ces écarts sont de sources de bugs potentiellement graves.

Initié en 2005, CompCert a été le premier compilateur capable de garantir mathématiquement la préservation de la sémantique des programmes, y compris dans des situations correspondant aux usages industriels. Il est d’autant plus important qu’il a été pensé pour les systèmes embarqués critiques, où aucune erreur ne peut être acceptée : pacemakers, aviation, centrales nucléaires, défense, etc. CompCert traduit en effet un vaste sous-ensemble du langage C, en un code assembleur exécutable sur différents micro-processeurs 32 et 64 bits (PowerPC, ARM, RISC-V and x86). Une efficacité que CompCert doit à la rigueur mathématique garantie par l’assistant à la démonstration Coq.

« Au lieu de raisonner sur des équations et des chiffres entiers, nous manipulons des programmes informatiques, souligne Sandrine Blazy, professeure à l’Université Rennes 1 et membre de l’Institut de recherche en informatique et systèmes aléatoires (IRISA, CNRS/Université Rennes 1). Nous décomposons ce problème complexe en une suite d’étapes, chacune accompagnée de sa propre démonstration. »

CompCert est commercialisé par la PME allemande AbsInt, suite à un accord avec le développeur principal Xavier Leroy, devenu depuis professeur au Collège de France sur la Chaire Sciences du logiciel. CompCert reste également un projet actif de recherche, avec par exemple à l’IRISA des travaux récents qui lui ont ajouté la préservation, lors de la compilation, de propriétés de sécurité utiles pour des implémentations cryptographiques.

Le succès de CompCert a inspiré de nombreux autres logiciels, certains développés aux États-Unis grâce à des financements significatifs de l’agence du département de la Défense des États-Unis1 . Il a également suscité un engouement autour du thème de la compilation vérifiée dans les conférences de premier plan. La consécration a eu lieu cette année avec l’obtention de l’ACM Software System Award, mais aussi de l’ACM SIGPLAN Programming Languages Software Award, dédiés aux logiciels à l’influence durable sur les plans commerciaux et/ou académiques.

« L’ACM est la principale société savante en informatique et décerne notamment le prix Turing, explique Sandrine Blazy. Elle remet de nombreux prix thématiques, et CompCert a remporté deux prix, celui du meilleur logiciel issu de la recherche, toutes catégories confondues, ainsi que celui décerné par la communauté des langages de programmation (SIGPLAN). » « Ces prix sont une très bonne nouvelle pour le domaine de la vérification formelle, complète Jacques-Henri Jourdan, chargé de recherche CNRS au Laboratoire méthodes formelles (LMF, CNRS/ENS Paris-Saclay/Université Paris-Saclay). J’espère que ce prix incitera chercheurs, étudiants et industriels à s’y intéresser. »

• 1Defense advanced research projects agency (DARPA)