Prix FIEEC Carnot de la Recherche Appliquée : Claude Marché ''fait ses preuves''

Claude Marché  : Je suis honoré par ce prix qui récompense les partenariats de recherche appliquée menées avec un industriel ayant eu un réel impact économique. Nous avons conduit depuis 2010 avec la société AdaCore, un certain nombre de recherches sur la vérification déductive de programmes. Le prix est nominatif, mais à mon sens l'équipe Toccata et la société AdaCore mériteraient aussi d'être distinguées et récompensées.

Yannick Moy  : Avant de rejoindre AdaCore , j'ai fait partie d’équipe Inria ProVal dans laquelle travaillait Claude qui fut mon directeur de recherche, entre 2006 et 2009. Lorsque j'ai rejoint cet éditeur, j'ai rapidement proposé de remplacer la partie "preuve" de la solution utilisée à l'époque par la technologie open source Why3 (anciennement Why) développée par Inria. Cela a été suivi d’un partenariat industriel donnant lieu à des collaborations multiples dans le cadre de projets coopératifs soutenus par les pôles de compétitivité, puis par la création d'un laboratoire commun (ProofInUse ) financé par l'Agence nationale de recherche (ANR) entre 2014 et 2017. Nous avons depuis signé un contrat de coopération bilatérale, qui court jusqu'en 2022, en vertu duquel AdaCore finance en partie les travaux de recherche de Toccata.

Qu'est-ce que la preuve informatique ?

Claude Marché  : Plusieurs équipes Inria se sont historiquement intéressées à ce sujet. Au niveau de Toccata, notre originalité est d'avoir décidé d'utiliser les techniques de preuve pour valider des programmes informatiques. Concrètement, les preuves de mathématiques sur des logiciels démontrent qu'ils réalisent bien ce qu'ils sont censés faire et qu'ils répondent à tous les critères de sûreté de fonctionnement définis par l'entreprise. Jusqu'ici, la méthode la plus courante consiste à effectuer des tests : cette technique est efficace mais elle est forcément limitée dans son périmètre et elle est coûteuse. Lorsque l'on "fait la preuve", on peut au contraire tester le programme dans le maximum de configurations possible . Nous avons ainsi développé un mécanisme qui permet d'exprimer mathématiquement l'ensemble des configurations possibles pour un programme et de vérifier qu'il s'exécute à chaque fois conformément à ce que souhaite l'utilisateur.

Yannick Moy  : Nous avons intégré plusieurs logiciels développés par l'équipe-projet Toccata au sein de notre environnement de vérification logicielle SPARK . En tant qu'industriel de l'open source, la preuve de programme nous aide à donner des garanties aux utilisateurs des logiciels que nous concevons  : ces sociétés – par exemple Airbus, Altran ou Nvidia – nous rémunèrent pour le support de la plate-forme et pour notre capacité à les aider à utiliser nos logiciels de façon ultrasécurisée.  

Qui sont les utilisateurs de ce type de technologies ?

Claude Marché  : Beaucoup d'entreprises du secteur de l'aéronautique et des transports sont depuis longtemps intéressées : elles emploient des logiciels pour lesquels la fiabilité, l’efficacité et la sécurité sont critiques. Elles dépensent donc déjà beaucoup d'argent dans les tests de logiciels ; certaines d'entre elles espèrent optimiser leurs investissements grâce à des technologies de preuve. Notre partenariat avec AdaCore nous permet de développer des applications pour ces secteurs, et donc de faire en sorte que nos recherches, forcément très théoriques, aient des retombées concrètes dans l'industrie .

Yannick Moy  : Il s'agit d'une technologie de pointe, qui suscite de plus en plus d'intérêt en dehors de l'avionique ou du ferroviaire : elle intéresse aujourd'hui des constructeurs de voitures autonomes, des spécialistes de la sécurité, des acteurs des appareillages médicaux ou des fournisseurs de services de cloud computing. Les entreprises de ces secteurs ont, elles aussi, des impératifs de sûreté afin d'éviter qu'une erreur ou qu’une attaque délibérée ne mette en danger la vie de leurs utilisateurs. Il s’agit par exemple d’assurer l'absence de failles de sécurité des plates-formes embarquées dans ces voitures ou implémentées dans des humains, tout en permettant de les connecter à des réseaux comme Internet. À nous de comprendre leurs besoins et de les partager avec Inria pour que nous puissions avancer ensemble sur les aspects les plus complexes.

Quels sont vos objectifs pour l'avenir ?

Claude Marché  : J'espère diversifier notre écosystème de partenaires, par exemple en travaillant avec d'autres éditeurs d'outils de programmation et de logiciels critiques destinés à d'autres secteurs d'activité. D'un point de vue académique, mon rêve est que nous réussissions à ce que les outils de preuve de programmes puissent être de plus en plus utilisés tout au long du cycle de conception  : la preuve se ferait en même temps que le développement du logiciel et la prise en compte de la sûreté serait donc beaucoup plus précoce.

Yannick Moy  : Du côté d’AdaCore, notre principale tâche sera de développer les briques technologiques permettant de faciliter l'utilisation des techniques de preuve.