Partager cette page :

Entretien avec David Pichardie, lauréat ERC

le 25 novembre 2017

David Pichardie, directeur du département Informatique et télécommunications de l'École normale supérieure de Rennes vient d’obtenir un financement européen pour un projet intitulé "Verified Static Analysis Platform" (VESTA), dans la catégorie Consolidator grant de l’ERC (European Research Council).

/medias/photo/ens-rennes-264-id_1519398205200-png

Vous êtes l'heureux lauréat d'un financement européen ERC : pouvez-vous nous présenter rapidement votre activité de recherche ?
Mes travaux s'inscrivent dans le cadre de la preuve de programme. Certains logiciels sont qualifiés de critiques car leur éventuel dysfonctionnement pourrait provoquer des catastrophes financières, voire humaines. C’est notamment le cas des logiciels embarqués sur les téléphones mobiles, les cartes bancaires mais aussi au coeur des avions, des centrales nucléaires ou des voitures. La preuve de programme permet de démontrer que certaines propriétés seront assurées durant l’exécution d'un programme. Plusieurs techniques de preuve existent et je m’intéresse plus particulièrement à deux d'entre elles dans mes travaux. La première approche est fondée sur les assistants de preuve : un système interactif avec lequel on peut écrire des spécifications et réaliser des preuves. L'outil se charge de vérifier la cohérence logique des interactions de l'utilisateur. L'autre approche, l'analyse statique, permet de démontrer automatiquement qu'un programme vérifie certaines propriétés comme l'absence d'erreur à l’exécution. J’effectue mes travaux dans le laboratoire IRISA sur le campus de Beaulieu, dans l’équipe Celtique dirigée par Thomas Jensen.

Pouvez-vous nous préciser la nature de ce financement ERC, son originalité, ses caractéristiques ?
Le Conseil européen de la recherche (CER) ou European Research Council (ERC) récompense des chercheurs aux idées qualifiées de novatrices. La mission de l'ERC est donc d'encourager la recherche de haut niveau en Europe grâce à un financement concurrentiel et de soutenir la recherche exploratoire dans tous les domaines de la recherche, sur la base de l'excellence scientifique. En l’occurrence, je viens d’obtenir un financement important (sur 5 ans) pour développer des recherches sur l’aide à la conception d’analyses statiques fiables. Ces outils sont en effet très complexes à concevoir et je propose d’en assurer la correction sémantique avec des techniques de preuve assistée ou preuve automatique, et si possible d’automatiser leur conception avec des technique de synthèse automatique de programmes. Mon projet s’intitule "Verified Static Analysis Platform" (VESTA) : il relève de la catégorie ‘Consolidator grant’ réservée aux chercheurs entre 7 et 12 ans après la thèse.

Quelles sont les impacts attendus pour ce projet ?
L’analyse statique est une technique de vérification de plus en plus appréciée dans l’industrie logicielle mais seuls quelques experts en maitrisent la conception algorithmique et le développement logiciel. Une entreprise souhaitant adopter cette technique doit en effet investir beaucoup d’énergie pour adapter un tel outil à ses besoins spécifiques et son parc logiciel. A l’heure actuelle, on observe que seuls les grandes sociétés américaines innovantes comme Google, Facebook, Amazon ou encore Uber, ont les moyens d’embaucher un expert pour concevoir un outil d’analyse statique finement adapté à leurs besoins. Depuis des années, je m’intéresse à la conception des analyses statiques, en me concentrant notamment sur leur fiabilité : une analyse doit donner des verdicts fiables ! Je m’appuie pour cela sur une théorie mathématique très riche appelée l’interprétation abstraite et inventée dans les années 70 par deux chercheurs français Patrick et Radhia Cousot et j’utilise l’assistant à la preuve Coq développée à Inria. Grâce au projet VESTA j’espère pouvoir démocratiser la conception des analyses statiques en simplifiant et automatisant leurs conceptions, tout en maintenant des garanties fortes sur leur fiabilité. Enfin, je compte notamment appliquer mes travaux pour développer des analyses assurant la sécurité des logiciels face à certaines attaques par canaux cachés. Dans ces scénarios, l’attaquant observe par exemple le temps d’execution d’un logiciel de cryptographie pour deviner un secret. Nos analyses devront assurer que les logiciels sont exempts de telles vulnérabilités.

Qu’est que ce financement va changer concrètement dans vos activités ?
Me voilà à l’abri des besoins pour financer des thèses et accueillir des postdocs et des chercheurs invités dans mon équipe ! Je vais donc fortement fortifier mes activités de recherche pendant 5 ans. Grâce à une charge d’enseignement et administrative réduite pour l’occasion, je vais pouvoir prendre le temps de voyager pour intensifier mes collaborations nationales et internationales. C’est aussi l'opportunité de prendre des risques accrus et explorer des approches fortement innovantes. J’ai beaucoup de chance de voir mon projet accepté dans un processus de sélection aussi difficile. C’est une reconnaissance exceptionnelle pour mes travaux et plus largement pour la recherche à l’ENS Rennes et à l'IRISA. Pour le montage de ce projet, j’ai profité d’une aide extrêmement efficace de la part de la Plateforme Projets Européens (2PE), plus précisément de Cécile Rocuet. Je tiens à la remercier pour tout cela.
Thématique(s)
Recherche - Valorisation, Vie des personnels

Mise à jour le 28 février 2018