Compilation vérifiée : vers du logiciel zéro défaut

Sandrine Blazy est professeure à l'Université de Rennes et directrice adjointe de l'UMR IRISA. Sa thématique de recherche est la vérification formelle de logiciels afin de garantir leur sûreté et leur sécurité. Elle a reçu la médaille d’argent du CNRS en 2023. Avec six collègues, elle a reçu en juin 2022 le prix « ACM software system award » et en juin 2023 le prix « ACM SIGPLAN Programming Languages Software Award » pour le développement du compilateur vérifié CompCert.

Résumé

La vérification déductive permet d’avoir des garanties très fortes sur l’absence de bug dans les logiciels; elle est utilisée pour développer des logiciels embarqués critiques, où toute erreur peut compromettre des vies humaines ou avoir d’autres conséquences catastrophiques. La vérification étant effectuée au niveau source, le compilateur, logiciel complexe et point de passage obligé pour obtenir un code écrit dans un langage compréhensible par la machine mais bien plus primitif, devient un maillon faible dans la chaîne de production du logiciel. Aussi, vérifier le compilateur lui-même permet de garantir qu’aucune erreur n’est introduite lors de la compilation. Plus généralement, cette approche ouvre la voie à la vérification des outils informatiques participant à la production et à la vérification du logiciel. Cet exposé présente les défis sémantiques qu’il a fallu résoudre pour développer CompCert, le premier compilateur optimisant ciblant plusieurs architectures et utilisé dans l'industrie, qui soit doté d’une preuve mathématique de correction vérifiée par ordinateur. Cette preuve se fonde sur un raisonnement sur la sémantique des programmes observés, c’est-à-dire une définition mathématique du comportement de ces derniers. Le code produit par CompCert est garanti se comporter comme prescrit par la sémantique du programme source C. Ce niveau de confiance dans la correction de la compilation permet à CompCert de répondre aux plus hauts niveaux de fiabilité logicielle.

Autres informations

Annonce des Colloquium

Si vous souhaitez être informé des prochains événements, vous pouvez souscrire à la liste de diffusion.
Si vous ne souhaitez plus être informé des événements, vous pouvez vous désinscrire de la liste de diffusion