Le LMF, un nouveau laboratoire d’informatique sur le plateau !

Issu de la réunion de deux groupes de recherche, le Laboratoire méthodes formelles (LMF - Université Paris-Saclay, ENS Paris-Saclay, CNRS) est aujourd’hui la référence en matière de recherche en sûreté et sécurité des systèmes informatiques grâce aux outils mathématiques. Il ambitionne de diffuser ses méthodes d’analyse à d’autres domaines.  

Le 1^er janvier 2020 est né le Laboratoire méthodes formelles (LMF - Université Paris-Saclay, ENS Paris-Saclay, CNRS). Il est issu de la réunion du Laboratoire spécification et vérification (LSV - ENS Paris-Saclay, CNRS) et de l’équipe VALS (Vérification d'algorithmes, de langages et de systèmes) du Laboratoire de recherche en informatique (LRI - Université Paris-Saclay, CNRS). À ces trois tutelles principales s’ajoutent deux autres tutelles secondaires : Inria et CentraleSupélec. Dirigée par Patricia Bouyer et son adjointe Évelyne Contejean, cette nouvelle entité située à Gif-sur-Yvette résulte d’une restructuration de l’informatique décidée par les organismes de tutelle au printemps 2018, et validée par le Haut Conseil de l’évaluation de la recherche et de l’enseignement supérieur (Hcéres) lors de la phase d’évaluation quinquennale des laboratoires de recherche publique. « Le LSV et l’équipe VALS travaillent ensemble depuis des années, ce regroupement est donc très opportun. Il nous ravit et nous enthousiasme beaucoup car en réunissant les aspects théoriques et appliqués de nos domaines d’étude, nous allons partager et nourrir de nouveaux projets ambitieux », commente Patricia Bouyer. Le laboratoire compte une centaine de chercheurs permanents, doctorants, post-doctorants et personnels soutien-support. Il est structuré en trois pôles : son cœur de métier en comporte deux, « Preuves » et « Modèles », où s’élaborent les méthodes d’analyse, de modélisation et de raisonnement pour les langages, les programmes, les protocoles et les systèmes informatiques ; le troisième, « Interactions », vise l’ouverture de ces recherches à d’autres domaines scientifiques. Les trois équipes-projets communes (EPC) Inria Deducteam, Mexico et Toccata, enrichissent cette structuration par une vision agile liée au modèle d’EPC Inria, qui promeut le développement technologique et l’innovation.

Le domaine de recherche des méthodes formelles

En informatique, les méthodes formelles sont des techniques permettant de raisonner rigoureusement sur des programmes ou des systèmes informatiques, afin de prouver leur conformité par rapport à un comportement attendu. Elles utilisent des outils mathématiques comme la logique, les automates, les probabilités, la topologie ou encore l’algorithmique. Évelyne Contejean note : « Notre laboratoire est à la croisée des chemins de l’informatique et des mathématiques. Galilée utilisait ces dernières pour étudier la nature et nous, nous nous en servons pour décoder le monde numérique ». Le cœur de métier du LMF est en effet de manipuler ces outils pour élaborer des méthodes d’analyse de programmes informatiques, afin de garantir leur fiabilité et leurs performances. 

Le LMF reconnu par ses pairs

Ce domaine de recherche est thématiquement très ciblé, mais il couvre tous les registres de la théorie aux applications. Cette diversité de points de vue s’illustre notamment par les deux Computer-Aided Verification (CAV) awards obtenus lors de conférences internationales du CAV. En 2017, Alain Finkel et Philippe Schnoebelen, chercheurs du LMF, reçoivent ce prix pour le développement de structures mathématiques conduisant à des résultats généraux de décidabilité pour la vérification des systèmes de transitions infinis ; et en 2019, Jean-Christophe Filliâtre, aussi du LMF, reçoit celui pour la conception et le développement de langages de vérification intermédiaires réutilisables, qui ont considérablement simplifié et accéléré la construction d’outils de vérification déductive automatiques et utilisables en pratique. « Le LMF est l’un des seuls laboratoires en France et dans le monde à rassembler en son sein une telle force de frappe sur les méthodes formelles », commente Evelyne Contejean.  

Recherche fondamentale et appliquée

Les applications traditionnelles des méthodes formelles consistent à garantir la sécurité de composants logiciels utilisés par des acteurs issus de secteurs très sensibles, comme le transport ferroviaire, l’aéronautique, l’aérospatial, le nucléaire, la défense ou encore la santé. « Une fusée qui explose au lancement ou une cyber-attaque sont typiquement des catastrophes liées à des problèmes de sécurité ou de sûreté de fonctionnement des systèmes informatiques », précise Patricia Bouyer. Cette garantie de bon fonctionnement de composants logiciels intéresse les industriels et le laboratoire collabore avec de nombreuses entreprises, notamment Alstom, Altran, Airbus, Dassault, Intel ou encore Thales. Certaines de ces compagnies utilisent des logiciels co-développés avec le LMF et certifiés TRL9 -  le Technology Readiness Level (TRL) est un standard ISO de mesure du niveau de maturité technologique sur une échelle d’un à neuf - à des fins de recherche et développement, et de production, comme Why3, Alt-Ergo et HOL-TestGen. D’autres bénéficient aussi de ces solutions applicatives par l’intermédiaire du laboratoire commun (Labcom) ProofInUse, porté par l’EPC Inria Toccata du LMF et l’éditeur de logiciels Adacore.

Ouverture vers d’autres domaines scientifiques

Fort de ses succès, le LMF diffuse ses méthodes d’analyse à d’autres domaines. Par exemple, le laboratoire s'intéresse à l'intelligence artificielle, notamment via sa participation au projet de recherche en réseaux neuronaux LeaRNNify, issu du programme de coopération européenne avec l’Allemagne Procope. Mais aussi au domaine de l’informatique quantique, car les nouvelles capacités de calcul offertes par la mécanique quantique nécessitent de revoir tous les protocoles, langages et techniques de vérification traditionnels. Ou encore à la cybersécurité, sujet où les garanties de performance sont essentielles, notamment en matière de protection du droit d’auteur, de la confidentialité des données et du respect de la vie privée. Pour tous ces domaines, le LMF s’inspire aussi de leurs innovations pour enrichir sa propre panoplie de techniques.

A Suivre avec la création  du Laboratoire interdisciplinaire des sciences du numérique – LISN, unité de recherche du CNRS et de l’Université Paris-Saclay.