Avec la preuve assistée par ordinateur, Sandrine Blazy traque les bugs
La traduction d’un programme écrit par un humain dans un langage haut-niveau en un programme exécutable peut malheureusement introduire des bugs… Sandrine Blazy, professeure à l’Université de Rennes et directrice adjointe de l’Institut de recherche en informatique et systèmes aléatoires (IRISA - CNRS/Université de Rennes), s’est spécialisée dans la vérification de cette traduction en co-développant CompCert, le tout premier compilateur pour le langage C vérifié formellement. Des contributions au meilleur niveau international qui lui valent de recevoir la médaille d’argent du CNRS.
Les liens entre mathématiques et informatique sont naturellement forts, et les deux disciplines continuent de s’enrichir de nouveaux ponts. Sandrine Blazy, professeure à l’Université de Rennes et directrice adjointe de l’IRISA, aborde les sciences du logiciel selon deux approches complémentaires : l’étude des langages de programmation et l’utilisation d’assistants de preuves, des logiciels permettant d’obtenir des garanties mathématiques sur le bon fonctionnement des programmes.
« Les langages de programmation me passionnent depuis que j’ai découvert l’informatique au collège, se souvient la lauréate de la médaille d’argent du CNRS 2023. À une époque où les gens n’avaient pas d’ordinateurs chez eux, notre professeur de mathématiques en avait installé deux dans la classe. Le seul moyen de s’en servir était d’écrire des programmes, ce que j’ai appris en autodidacte. Nous n’étions que deux élèves à nous y intéresser jusqu’à la fin de l’année, et nous travaillons encore aujourd’hui dans l’informatique ! »
Sandrine Blazy a continué à programmer grâce au club d’informatique de son lycée, tandis que son parcours s’articulait autour des sciences, et en particulier des mathématiques. « Cela a toujours été ma matière préférée, j’adore dénicher la dernière pièce du puzzle d’un raisonnement » affirme Sandrine Blazy. Les études supérieures lui ont permis de concilier ses deux passions en intégrant une école d’ingénieurs en informatique, où elle s’enthousiasme pour la compilation et la sémantique des langages de programmation.
Son sujet de thèse l’a amenée dans un centre de recherche d’EDF, où il fallait trouver des moyens d’améliorer la maintenance de vastes logiciels du nucléaire en langage Fortran. Sandrine Blazy a proposé un prototype simplifiant ces logiciels, ce qui l’a poussée à se poser la question cruciale de sa carrière : comment démontrer mathématiquement qu’une transformation de programme est correcte ? Elle esquisse une première réponse dans un article qui sera primé en conférence internationale, juste avant l’obtention de sa thèse. Cette réception enthousiaste la convainc de se consacrer à une carrière académique.
Quelques années plus tard, elle découvre la preuve interactive avec l’assistant de preuve Coq, développé en France depuis les années 80 et désormais largement reconnu à l’international. En 2003, elle unit ses talents avec Xavier Leroy, actuellement professeur au Collège de France, pour se consacrer à la conception de CompCert. Il s’agit du premier compilateur pour le langage C vérifié formellement en Coq. Un compilateur est un logiciel complexe, qui produit un code de bas niveau compréhensible par la machine à partir d’un programme écrit dans un langage compréhensible par les humains. Pour tout programme passant par un compilateur, il est donc primordial de s’assurer avec les meilleures garanties que ce dernier n’introduit pas de bugs.
CompCert a été distingué par les meilleurs prix internationaux du domaine, tels que l’ACM SIGPLAN Programming Languages Software award et l’ACM Software System award. Jusqu’alors, vérifier formellement un logiciel aussi complexe qu’un compilateur semblait hors de portée des assistants de preuve. CompCert est présentement commercialisé par la société AbsInt et est utilisé dans l’aéronautique et le nucléaire. Un tel niveau de confiance dans les programmes est en effet indispensable pour les systèmes embarqués critiques, où toute erreur peut compromettre des vies humaines ou avoir d’autres conséquences catastrophiques.
Sandrine Blazy poursuit ses travaux et dote CompCert de davantage de possibilités de compilation et de garanties supplémentaires, en particulier pour les applications à la sécurité informatique. Elle enseigne la vérification de logiciels afin de développer la discipline. Depuis janvier 2021, elle est directrice adjointe de l’IRISA. Réparti entre trois sites en Bretagne et rassemblant 850 personnes, dont environ 300 chercheurs permanents, il s’agit de l’un des plus grands laboratoires d’informatique de France.
En 2021, Sandrine Blazy lance un programme avec des chercheurs de l’Imperial College de Londres sur l’utilisation de CompCert pour produire des circuits. Plusieurs thèses ont déjà démarré dans ce cadre. Preuve s’il en est de l’impact et de la pérennité des travaux de Sandrine Blazy, à présent couronnés par la médaille d’argent du CNRS.