Newtech
Un compilateur mathématiquement sans erreur
Par Pierre Berlemont, publié le 11 octobre 2022
Développé par des équipes de plusieurs organismes de recherche français, CompCert est un compilateur de code en langage C, destiné notamment aux logiciels critiques des avions et de l’industrie nucléaire, qui certifie une compilation sans erreur.
Le programme CompCert est né en 2004. C’est un projet de recherche sur le long terme, qui a progressivement suscité l’intérêt des industriels. Récemment, CompCert a été récompensé par l’Association for Computing Machinery (ACM) – qui remet chaque année le prix Turing.
« Avec CompCert, nous ne visons que les systèmes embarqués, critiques, donc dans les avions, les centrales nucléaires, le ferroviaire, là où il existe des garanties et des exigences de qualité très fortes. Les architectures PowerPC ou ARM y sont très présentes. S’ajoutent des processeurs plus exotiques pour des fonctions très spécialisées », explique Xavier Leroy, développeur principal et professeur au Collège de France.
D’ailleurs, seul le C est pris en charge en tant que langage le plus employé dans le monde de l’embarqué critique. Le support de langages de plus haut niveau pourrait être envisagé, mais ce n’est pas une demande.
Le principe de CompCert est simple. Grâce à des vérifications mathématiques – des méthodes formelles inventées par Alan Turing en 1949 –, il certifie le bien-fondé de la compilation : soit il l’accepte, et dans ce cas apporte la certitude qu’il n’y aura pas d’erreurs ; soit il la refuse car il ne peut pas garantir le résultat.
À LIRE AUSSI :
À quel risque répond-il, quand on sait que la plupart des bugs logiciels viennent d’erreurs dans le code source développé ? « Pourtant, on trouve aussi des erreurs dans des compilateurs, par exemple dans le GCC de GNU, tous les cinq ou dix ans. J’en ai moi-même découvert une cette année. Débusquer un bug dans un compilateur est rare, et même difficile à comprendre, car le compilateur est le dernier élément que l’on met en cause », poursuit Xavier Leroy.
Et ce risque n’est pas acceptable sur certains systèmes critiques – du bon fonctionnement desquels dépend la sécurité de personnes – qui, de plus, ont une durée de vie très longue et dont le logiciel sera difficilement patché ou mis à jour. Indépendamment de toutes les méthodes strictes de programmation et des tests renforcés effectués sur le code, la certification du compilateur n’est pas une option.
Xavier Leroy,
professeur au Collège de France
« On trouve des erreurs dans le compilateur GCC tous les cinq ou dix ans. J’en ai moi-même découvert une cette année. »
« Les ingénieurs d’Airbus sont très attentifs à sur tous ces points. Avec eux, nous avons appliqué nos techniques de vérification mathématique du programme. Nous avons vérifié que le code mathématique sorti du compilateur se comporte bien. Cela n’a pas été sans surprises. Par exemple, nous avions un test qui échouait uniquement avec une certaine version de GCC », décrit Xavier Leroy.
Du compilateur au code source
Ce formalisme mathématique commence à s’appliquer non seulement au compilateur, mais également au code source lui-même. Toutefois, cette méthode a un coût en termes de temps et exige des ingénieurs hyper pointus. De plus, le langage C, malgré son âge, continue d’évoluer, et CompCert ne prend pas encore en compte toutes les dernières nouveautés.
En outre, le formalisme mathématique ne peut s’appliquer que sur des logiciels assez simples, pas sur des applications de grande taille, ne serait-ce qu’un navigateur web. Typiquement, il peut être employé sur certains modules, en cryptographie par exemple.
La technologie est téléchargeable gratuitement, mais CompCert est aussi commercialisé par la société allemande Absint, qui compte douze ingénieurs sur le projet et a développé des versions pour des processeurs très spécialisés. Auparavant subventionné par l’ANR (Agence nationale pour la recherche), CompCert est désormais essentiellement financé par les royalties versées par Absint.
Astrée, l’autre outil français de contrôle des codes sources
Absint distribue également un autre outil de vérification des codes sources C dénommée Astrée. Né en 2021 dans le laboratoire d’informatique de l’école Normale Supérieure et financé par le CNRS, désormais enrichi et maintenu par l’INRIA, Astrée (acronyme de Analyseur statique de logiciels temps réel embarqué) est un analyseur de code C à même de prouver que le langage C est correctement utilisé tout au long du code et qu’il n’y aura pas d’erreurs RTE (Run Time Execution) lors de l’exécution du programme.
Astrée (qui vérifie le code) est utilisé par Airbus en amont d’un outil comme CompCert (qui certifie la compilation) au sein d’une chaîne de contrôle de la qualité des programmes embarqués.
