Sites Inria

Distinction

4/11/2011

Xavier Leroy, lauréat du prix « La Recherche 2011 en sciences de l'information »

Xavier Leroy Xavier Leroy

Xavier Leroy, responsable de l'équipe-projet Gallium du centre de recherche Inria Paris - Rocquencourt, a obtenu le prix La Recherche 2011 en sciences de l'information le 18 octobre dernier aux côtés de Sandrine Blazy (université de Rennes, EPI Celtique), Zaynah Dargaye (maintenant au CEA), Jean-Baptiste Tristan (actuellement à Harvard). Récompensant ainsi leurs travaux sur la vérification formelle de compilateurs réalistes. 

Qu'est-ce que CompCert ?

Xavier Leroy : CompCert est le compilateur que nous développons dans ce projet.  Comme tout compilateur, c'est un outil qui traduit le code source, tel qu'écrit par les programmeurs (dans notre cas en langage C) en code machine, directement exécutable par l'ordinateur ou le système embarqué.  Non content de traduire, un bon compilateur réécrit également le code pour en améliorer les performances: on parle alors d'optimisations de code. Les compilateurs sont des programmes fascinants: non seulement ils sont très complexes et réalisent des optimisations que bien peu de programmeurs pourraient faire à la main, mais aussi ils ont ce pouvoir très dérangeant d'introduire des erreurs derrière le dos du programmeur, produisant du code exécutable faux à partir d'un code source correct.  Les Italiens disent "traduttore, tradittore" ("traducteur, traître"): c'est parfois vrai de la compilation comme de la traduction littéraire. Le but de notre projet CompCert est précisément d'éradiquer ce risque de mauvaise traduction par le biais d'une vérification formelle du compilateur. Nous avons mené à bien une preuve -- une véritable démonstration mathématique -- du fait que notre compilateur traduit toujours fidèlement les codes sources qu'on lui donne; ou en d'autres termes, que le code machine produit s'exécute exactement comme prescrit par la sémantique du code source.  Notre système CompCert est le premier compilateur réaliste, utilisable pour la production de logiciel embarqué, à atteindre des garanties d'un niveau aussi élevé.

A qui vont servir ces travaux ?

Xavier Leroy : Dès le départ de l'effort CompCert, notre but était d'améliorer la qualité du logiciel critique en éliminant tout risque lié au compilateur, renforçant du même coup les garanties que l'on peut obtenir par l'application de méthodes formelles aux codes sources. Nos résultats suscitent l'intérêt de plusieurs acteurs de l'aéronautique. Nous avons en particulier une collaboration fructueuse avec Airbus, qui évalue l'utilisabilité de CompCert et réfléchit à lever les obstacles, notamment réglementaires, à son intégration dans leurs processus de développement.

Comment construire une telle preuve 

Xavier Leroy : On pourrait l'écrire sur du papier, comme une démonstration mathématique ordinaire, mais la preuve serait si grosse (des milliers de pages) et si ennuyeuse qu'aucun mathématicien n'accepterait de la relire pour s'assurer qu'elle est juste. Au contraire, nous nous sommes fait aider par la puissance de l'ordinateur et avons utilisé l'assistant de preuves Coq.  Ce logiciel, développé principalement dans les équipes PiR2 et Typical, permet de construire des preuves en interaction avec l'utilisateur, et surtout de les revérifier automatiquement, garantissant de la manière la plus forte qu'aucun des cas de la preuve n'a été oublié et que toutes les déductions logiques sont valides.

Qu'est-ce qu'un logiciel sûr ?

Xavier Leroy : Dans l'absolu: un logiciel qui ne "plante" jamais et remplit correctement, en toutes circonstances, les tâches qui lui sont dévolues.  Une telle perfection est difficile à concevoir, mais certains logiciels critiques (dont dépendent des vies humaines) s'en approchent de très près, dans des domaines tels que les transports (avions, ferroviaire) et le nucléaire. Traditionnellement, une telle qualité s'obtient par des processus rigoureux de développement et d'énormes quantités de tests.  De plus en plus, on utilise également des méthodes dites "formelles", basées sur les mathématiques et la logique, telles que la preuve de programmes (comme nous l'avons fait pour CompCert) ou encore l'analyse statique (comme le fait l'outil Astrée de l'équipe Abstraction).

Mots-clés : Xavier Leroy Prix la Recherche 2011 CompCert Langage C Compilateur Code source Logiciel critique Preuve de programme Centre de recherche Inria Paris - Rocquencourt

Haut de page

Suivez Inria