Partenariats européens

Assistants de preuve : renforcer la position européenne via EuroProofNet

Date:
Mis à jour le 10/05/2022
Inria est le porteur d’EuroProofNet, une action du programme européen COST qui concerne la sûreté et la sécurité des systèmes informatiques critiques. Des chercheurs en informatique de l’institut, avec leurs homologues d’une trentaine de pays d’Europe, unissent leurs forces pour améliorer l’interopérabilité des assistants de preuve. Un enjeu majeur de cybersécurité.
Vérification de programme
© Inria / Photo C. Lebedinsky

Fédérer une communauté de chercheurs en Europe

Lancée en novembre 2021, EuroProofNet, vient d’atteindre en ce début d’année sa vitesse de croisière. L’objectif de cette action du programme européen COST (European Cooperation in Science and Technology), dirigée par Frédéric Blanqui, chargé de recherche au sein de l’équipe commune Deducteam (Inria de SaclayENS Paris-Saclay - Université Paris-Saclay) du Laboratoire des Méthodes Formelles ? Fédérer une communauté de chercheurs en Europe s’intéressant à la vérification des programmes informatiques et aux systèmes de preuve numérique, avec pour finalité d’améliorer l'interopérabilité de différents outils et d’en faciliter l’utilisation en Europe et dans le monde.

Frédéric Blanqui, à l’origine du projet, a su réunir autour de cette problématique une large communauté scientifique : plus de 200 participants, représentant une trentaine de pays d’Europe. Dotée d’un budget de 150 000 euros pour sa première année (sur ses quatre ans d’existence au total), EuroProofNet permet de mener des activités de mise en réseau, comme l’organisation de conférences, de colloques, des visites scientifiques, des échanges entre chercheurs, etc.

Biographie express de Frédéric Blanqui

Frédéric Blanqui s’intéresse depuis plus de 20 ans à des sujets de nature pratique et théorique en informatique : les « systèmes de types » et « les systèmes de réécriture », dont la combinaison est au cœur de ses recherches sur les systèmes de preuve. Après avoir obtenu un doctorat à l’Université d’Orsay en 2001 et poursuivi ses recherches en postdoctorat à l’Université de Cambridge en 2002, il rejoint les équipes Inria en 2003, tout d’abord sur le site de Nancy, puis de Paris et enfin de Cachan et Saclay.

Une expérience de cinq ans à Pékin, dans le cadre de la création d’une équipe au sein du laboratoire européo-chinois d’informatique, le LIAMA, lui donne une ouverture internationale. Un atout indéniable pour animer le réseau des 220 chercheurs européens participant à EuroProofNet !  

Des assistants de preuve indispensables

Le champ de recherche de cette communauté revêt une importance scientifique et technique majeure car les systèmes de preuve sont indispensables à la validation des systèmes critiques ! Ceux-ci permettent ainsi de s’assurer du bon fonctionnement de programmes informatiques complexes, utilisées dans de nombreux secteurs : par exemple l’industrie aérospatiale (pour le guidage de lanceurs spatiaux), la santé (pour la fiabilité de dispositifs médicaux, en radiographie, cardiologie, etc.), la banque (pour la sécurité des systèmes de gestion de données ou le cryptage de transactions), l’énergie (pour le pilotage de centrales nucléaires), ou encore la cybersécurité.

Quel est le but de la vérification ? « La preuve démontre la validité d’un programme informatique ou d’un système électronique, que les concepteurs d’applications critiques cherchent à établir. Un système de preuve permet de montrer que les logiciels impliqués réalisent bien la tâche pour laquelle ils ont été conçus et donnent les résultats que l’on attend d’eux », résume Frédéric Blanqui.

Image
Frederic Blanqui
Verbatim

Chaque assistant de preuve opère selon un système logique et informatique qui lui est propre et il existe parfois des incompatibilités entre les approches proposées par des outils différents. 

Auteur

Frédéric Blanqui

Poste

Chercheur Inria au sein de l'équipe-projet Deducteam

Le chercheur précise : « Il existe deux types de systèmes de preuve. Pour des problèmes simples, des programmes spécifiques s’avèrent capables de détecter automatiquement des erreurs dans un code. Cependant, leur périmètre d’action est limité, et, pour des problèmes plus complexes, les preuves formelles de validité s’obtiennent ‘à la main’, à l’aide d’assistants de preuve ».

L’Europe très investie dans la recherche

L’Europe constitue, avec les États-Unis, l’un des principaux centres mondiaux de recherche et développement en matière d’assistants de preuve. Les équipes européennes sont particulièrement actives sur ce sujet, en constant développement en raison des demandes. Les logiciels comme Coq, développé par Inria, ou Isabelle, conçu au Royaume-Uni et en Allemagne, comptent parmi les assistants de preuve les plus utilisés par les informaticiens, auxquels s’ajoutent d’autres outils développés par différentes équipes.

Un système de preuve se fonde sur quelques axiomes (des énoncés considérés comme universels), assortis de règles de raisonnement, à partir desquelles s’énoncent, comme en mathématiques, des conclusions logiques. Les logiciels utilisent en outre des fonctions informatiques, disponibles dans des librairies spécifiques à l’outil. « Chaque assistant de preuve opère selon un système logique et informatique qui lui est propre et il existe parfois des incompatibilités entre les approches proposées par des outils différents » éclaire Frédéric Blanqui.

L’interopérabilité des assistants de preuve au cœur du projet

Comment garantir alors que les conclusions obtenues avec un assistant de preuve sur la validité ou la sécurité d’un programme soient fiables – c’est-à-dire qu’elles ne dépendent pas du système utilisé ? « On pourra par exemple réaliser des vérifications indépendantes avec des outils différents et renforcer la confiance en un système de preuve par confrontation de ses conclusions avec celles obtenues avec d’autres systèmes, répond Frédéric Blanqui. Pour cela, il faut pouvoir ’traduire’ les fonctionnalités d’un outil vers un autre ».

L’interopérabilité des assistants de preuve est donc au cœur d’EuroProofNet qui compte au total six groupes de travail, dédiés chacun à une thématique scientifique. Outre l'interopérabilité des systèmes de preuve, figurent ainsi la preuve automatisée, la vérification de programmes, le développement de bibliothèques de preuves formelles, le développement des techniques d’apprentissage automatique dans les preuves, et les recherches sur la théorie des types qui est à la base des assistants de preuve modernes.

Des ambitions scientifiques élevées

Verbatim

L’action aura aussi d’autres résultats, comme celui de renforcer la position européenne, académique et industrielle, sur un marché stratégique émergent et économiquement dynamique.

Auteur

Frédéric Blanqui

Poste

Chercheur Inria au sein de l'équipe-projet Deducteam

« Nous avons engagé les premiers échanges au sein du réseau d’EuroProofNet début février, avec une première réunion ‘hybride’, en raison du contexte sanitaire actuel, à Valence en Espagne, explique Frédéric Blanqui. D’autres réunions sont prévues cette année, dont une école d’été prévue en France à Nantes, à l’occasion de laquelle nous allons mieux faire connaître Dedukti, un langage développé chez Inria qui permet d’encoder différentes fonctionnalités des systèmes logiques de manière modulaire ».

EuroProofNet s’est donné des ambitions scientifiques élevées, comme celle de développer des outils de traduction entre systèmes de preuve ou d’aboutir à un standard européen. « L’action aura aussi d’autres résultats, comme celui de renforcer la position européenne, académique et industrielle, sur un marché stratégique émergent et économiquement dynamique », conclut Frédéric Blanqui.  

L'équipe-projet Deducteam

Équipe commune entre Inria et l’ENS Paris-Saclay, Deducteam regroupe, autour de Gilles Dowek son responsable, quatre chercheurs permanents (Bruno Barras, Frédéric Blanqui, Valentin Blot et Jean-Pierre Jouannaud) et plus d’une dizaine de non-permanents. Elle explore les applications de la théorie de la démonstration à la conception de cadres logiques, s’intéresse à l'interopérabilité entre systèmes de preuve (un sujet sur lequel elle est leader dans le monde) et travaille à la construction de bibliothèques mathématiques universelles. Deducteam échange régulièrement avec le secteur industriel, dans les domaines de l’informatique (Clearsy, Nomadic-Labs, etc.) ou de l’énergie (Mitsubishi), en particulier dans le cadre de projets de recherche collaborative.

En savoir plus