Vos recherches s’inscrivent dans le cadre de la preuve de programme. Comment s’assurer qu’un logiciel fonctionne bien de la manière prévue ?
David Pichardie : Mes travaux de recherche concernent le domaine de la preuve de programme, qui permet de s’assurer qu’un logiciel se comportera comme on l’avait prévu, durant son exécution. Une des techniques à laquelle je m’intéresse se base sur les assistants de preuve. Il s’agit d’outils interactifs permettant de définir des spécifications précises et de garantir qu’un programme les satisfait. Le système vérifie ainsi que l’utilisateur ne commet pas d’erreur logique durant l’écriture du programme, ce qui entrainerait des dysfonctionnements. Je m’intéresse aussi à une autre approche, appelée analyse statique, qui permet de démontrer, automatiquement cette fois, qu’un programme fonctionnera conformément à certaines spécifications, sans pour autant l’exécuter.
Pourquoi le développement de tels outils est-il primordial ?
D.P. : L’analyse statique s’appuie sur une théorie mathématique très riche développée à partir des années 70. Or ce domaine reste très peu enseigné, et les outils qui en découlent peu diffusés hors des milieux académiques, avec pour résultat que seuls quelques experts en maitrisent la conception algorithmique et le développement logiciel. Pourtant, leurs apports sont très recherchés par les industriels. En raison des progrès exponentiels de l’informatique, la taille des programmes est devenue colossale, de l’ordre de plusieurs millions de lignes de code et les grandes sociétés sont prêtes à investir pour automatiser la recherche de bugs dans leurs logiciels. Elles dépensent beaucoup d’énergie pour adapter de tels outils à leurs à leur parc logiciel et les grandes sociétés américaines comme Google, Facebook, Amazon ou encore Uber, préfèrent même embaucher des experts en analyse statique pour concevoir des logiciels spécifiquement adaptés à leurs besoins. Mais les analyseurs statiques sont eux aussi des programmes complexes et leurs concepteurs deviennent parfois au fil du temps les seuls experts capables d’assurer leur bon fonctionnement et leur évolution. Et quand ces experts doivent passer le relai, cela peut devenir problématique et leurs successeurs peuvent avoir beaucoup de difficultés à les maintenir ou à intervenir dessus.
Quelles solutions êtes-vous en train de développer ?
D.P. : Mes travaux visent à guider et automatiser le design d’outils d’analyse statique, et in fine de disposer une « boîte à outil » pour faciliter la mise au point de nouveaux programmes d’analyse statique. Il deviendrait alors possible de synthétiser, par morceau ou en totalité, un analyseur fiable à partir d’un cahier des charges répondant le plus finement possible aux spécificités définies par l’utilisateur, pour un coût réduit. A terme, j’espère que mes travaux permettront de démocratiser les outils se basant sur l’analyse statique, grâce à des techniques de synthèse automatiques et rigoureuses. De plus, j’intègre aussi dans ma démarche l’aspect sécuritaire pour les logiciels qui sont créés de cette manière, notamment en ce qui concerne les attaques par canaux cachés. Ce sont des scénarios lors desquels les attaquants utilisent des observations indirectes, comme par exemple les temps d’exécution d’un programme, pour en déduire des informations sensibles. C’est un aspect que les outils que je développe devront prendre en compte, afin de s’assurer que les logiciels ainsi conçus ne contiennent pas ce type de vulnérabilités.