Tel un architecte, Aymeric Fromherz, chercheur ISFP (Inria Starting Faculty Position) depuis 2022 au sein de l'équipe-projet PROSECCO, examine les fondations mathématiques du monde numérique garantissant que chaque ligne de code repose sur une structure inébranlable. Son domaine de prédilection ? La vérification formelle, une approche rigoureuse qu'il applique à divers types de programmes. Que ce soit pour sécuriser les échanges cryptographiques, fiabiliser les systèmes d'exploitation ou même décortiquer les arcanes du droit fiscal, Aymeric s'efforce de construire des systèmes toujours plus robustes et dignes de confiance.

Son parcours, jalonné de réussites, n'était pas écrit d'avance. Après avoir passé ses années lycée à Lyon, il se tourne vers les mathématiques, intégrant l'ENS-PSL à Paris après deux années de classes préparatoires scientifiques. Pourtant, au détour d'une double licence, c'est l'informatique qui le séduit par son potentiel et sa capacité à créer.

Ses premières expériences le mènent d'abord vers le traitement du signal sur des graphes, lors d'un stage à Lyon. Mais c'est une immersion dans le monde de l'entreprise, chez Prove&Run, une société spécialisée dans les systèmes d'exploitation formellement vérifiés avec une visée industrielle, qui lui fait naître une vocation pour la vérification formelle. L'idée de modéliser mathématiquement des programmes pour prouver leur exactitude et leur fiabilité devient une ligne directrice.

Désireux de voir au-delà de l'horizon français, Aymeric s'envole pour les États-Unis, où il réalise sa thèse à l'université Carnegie Mellon. Pour Aymeric, la recherche est une source de stimulation permanente, une opportunité unique d'interagir avec des personnes partageant le même état d'esprit, où l'on ne considère rien comme acquis.

Dans la recherche, il y a toujours de nouvelles choses qui se passent. On n’a jamais vraiment fait le tour d'un sujet. C'est une sorte de stimulation permanente. C'est aussi une opportunité unique d'interagir avec des gens qui ont ce même état d'esprit.

Lors de son passage chez Microsoft Research il découvre à quel point il est crucial de relier la recherche fondamentale à des applications concrètes et industrielles : 

J’ai été impressionné par cette équipe qui rassemblait des esprits à la fois brillants et accessibles. Nous étions encouragés à échanger avec les chercheurs et chercheuses de Microsoft Research, de véritables sommités dans leur domaine (…) J’ai également apprécié l’équilibre entre recherche et applications concrètes. Garder un pied dans le concret, résoudre des problèmes applicatifs, parfois industriels, tout en faisant de la recherche, c'est vraiment très important pour moi. 

De retour en France, il rejoint l'équipe-projet PROSECCO en octobre 2021 en tant que post-doc, puis en tant que chercheur ISFP dès 2022, où il continue d'explorer des solutions pour rendre les logiciels plus sûrs et plus fiables. Aymeric veille à ce que ses travaux ne restent pas confinés aux laboratoires, mais trouvent aussi une résonance en-dehors de leurs murs. Son objectif : étendre l'application des techniques de vérification formelle à un large éventail de domaines et de systèmes.

Dans un monde où les logiciels régissent nos vies, des systèmes bancaires aux communications sécurisées, la fiabilité du code informatique est une question cruciale. C'est là qu'intervient la vérification formelle, un domaine à la croisée des mathématiques et de l'informatique, visant à garantir qu'un programme fonctionne comme prévu, sans faille ni ambiguïté. Une propriété très importante pour, par exemple, des systèmes embarqués, des systèmes aéronautiques ou encore des centrales nucléaires. 

Créer des modèles mathématiques du comportement d'un programme pour démontrer qu’il est exempt d'erreurs critiques, c’est le terrain d’étude d’Aymeric. Un des enjeux de cette discipline est la "correction fonctionnelle". Elle permet de s’assurer non seulement qu'un programme ne "crashe" pas mais aussi qu’il "fait ce qu'il doit faire". En cryptographie, par exemple, il s'agit de vérifier que l'implémentation d'un algorithme, souvent complexe, correspond fidèlement à sa spécification mathématique.

Mais la vérification formelle ne s'arrête pas à la cryptographie. Aymeric et ses collègues appliquent ces techniques aux systèmes d'exploitation, en particulier aux mécanismes de gestion de la mémoire (l'allocateur mémoire) et, récemment, ils les ont appliquées à un champ plus surprenant : les implémentations du droit fiscal.

Leurs travaux ont effectivement mis en lumière des ambiguïtés dans l'interprétation de calculs de dates dans des textes de loi, avec des conséquences réelles sur les décisions administratives et judiciaires. Ce qui leur a valu une reconnaissance lors de la conférence ESOP en avril 2024, où ils ont reçu un Best Tool Paper Award pour leur article intitulé "Formalizing date arithmetic and statically detecting ambiguities for the law". Un exemple concret de l'impact que peuvent avoir ces méthodes sur la société, bien au-delà du simple monde du développement logiciel.

Les calculs opérant sur des dates sont fréquents dans des implémentations de systèmes juridiques pour déterminer, par exemple, l’éligibilité des citoyennes et des citoyens aux prestations sociales. Cependant, ces calculs ne sont pas toujours bien définis : si on ajoute 1 mois au 31 mars, le résultat donnera-t-il la date du 30 avril ou du 1er mai ? Les implémentations existantes de calculs de dates ont rarement un comportement bien défini et spécifié pour ce genre de cas. Pour résoudre ce problème nous avons donc défini une sémantique d’arithmétique de dates qui permet de formaliser les comportements attendus. 

Dans les coulisses de l’équipe-projet PROSECCO, la recherche avance au rythme d’une réflexion approfondie, où la rigueur de la vérification formelle se conjugue à des enjeux technologiques concrets. Ici, on s’attelle à sécuriser les systèmes et langages informatiques bien avant leur déploiement. Parmi ces travaux, le langage Rust. L’équipe cherche à en comprendre ses fondements, son comportement intrinsèque, avant d’en explorer les implications en matière de raisonnement logiciel. « Ce langage apporte beaucoup de points positifs par rapport à la sûreté du logiciel mais requière aussi une nouvelle compréhension des programmes écrits en Rust par rapport à ceux écrits en C » explique Aymeric.

Mais l’expertise de PROSECCO ne s’arrête pas là. La cryptographie est aussi un pilier fondamental des recherches de l’équipe, particulièrement avec l'avènement de la cryptographie post-quantique. « Si un jour un ordinateur quantique existe, certains pans de la cryptographie moderne ne seront plus sécurisés, ils deviendront obsolètes. C'est donc important de se prémunir contre ces choses en amont, ajoute Aymeric, d'où le développement de nouvelles constructions cryptographiques dites ‘post-quantique’ ». L’objectif est donc d’anticiper ces bouleversements en développant des solutions capables de résister aux menaces que poseront ces nouvelles machines.

Et puis, il y a le défi de la vérification de la loi fiscale précédemment expliqué. À travers ce projet, l’équipe applique ses méthodes de formalisation et de preuve mathématique à la législation, afin d’accompagner les décideurs publics. « L’idée est de fournir des outils aux juristes et aux législateurs pour prévenir les ambiguïtés et les incohérences dans l’interprétation des lois », précise Aymeric. 

Cette recherche s’inscrit dans le cadre de l’action exploratoire AVoCat dont Aymeric est coresponsable scientifique avec Raphael Monat (équipe-projet SYCOMORES du Centre Inria de l’Université de Lille). AVoCat s’intéresse à la vérification automatique de programmes Catala, un nouveau langage de programmation, conçu pour être compréhensible par les juristes et suivre la structure des textes législatifs afin de transformer la loi en code. 

S’il devait recommander un ouvrage aux étudiants qui seraient intéressés par son domaine de recherche, Aymeric choisirait Mechanizing Proof: Computing, Risk, and Trust de Donald MacKenzie (MIT Press, 2001). Cet essai de sociologie des sciences retrace l’histoire de la vérification formelle des programmes et met en lumière une réalité intéressante : les grandes questions qui animent le domaine aujourd’hui étaient déjà posées il y a 40 ou 50 ans. « C'est un ouvrage assez important à mes yeux, ne serait-ce que pour avoir une vision globale de ce domaine et en comprendre l'évolution, et notamment comment l'IA a été envisagée comme outil de raisonnement mathématique dès les années 60. Il offre une perspective sur les apports, les limites et les domaines d’application de la vérification formelle », conclue Aymeric.