Horizon Maths 2024 : Preuve mathématique et sûreté logicielle
L'édition 2024 d'Horizon Maths a eu lieu le mercredi 27 mars 2024 de 9h à 18h en Amphithéâtre Hermite de l'IHP (11 rue Pierre et Marie Curie, Paris 5e) sur le thème : Preuve mathématique et sûreté logicielle.
C'est Hugo Herbelin (Inria, IRIF) qui a coordonné cette édition. Les organisateurs remercient Catherine Dubois (ENSIIE) et Xavier Leroy (Collège de France) pour leur aide.
Programme
- 9h-9h30 Accueil et allocutions d'ouverture
- 9h30 - 10h Utilisation des méthodes formelles pour les systèmes critiques, par Thierry Lecomte (CLEARSY)
- 10h - 10h30 Des méthodes formelles en pratique, par Laurent Voisin (Systerel)
- 10h30 - 11h Pause café
- 11h - 11h30 The Far Side of Software Dependability, par Danko Ilik (CNES)
- 11h30 - 12h Vérification de systèmes embarqués aérospatiaux, par Pierre Roux (ONERA)
- 12h - 12h30 Table-ronde Formation, avec Catherine Dubois (ENSIIE) et les orateurs des exposés
- 12h30-14h Pause déjeuner
- 14h - 14h30 Vérification déductive de programmes assistée par ordinateur, par Xavier Leroy (Collège de France)
- 14h30 - 15h Logique de séparation : de la gestion de la mémoire à l'établissement de protocoles personnalisés, par Armaël Guéneau (Inria Saclay, LMF)
- 15h - 15h30 High-assurance post-quantum cryptography: the ML-KEM case, par Pierre-Yves Strub (PQShield)
- 15h30 - 16h Pause café
- 16h - 16h30 Formalisation en mathématiques appliquées : définition des éléments finis, par Sylvie Boldo (Inria, LMF)
- 16h30 - 17h00 Verifying Industrial C++ Code, par Gregory Malecha (BedRock Systems)
- 17h00 - 17h45 Table-ronde Prospective, avec Catherine Dubois (ENSIIE) et les orateurs des exposés
Intervenant•e•s
Chercheuse en informatique.
Ses recherches concernent à la fois la formalisation des mathématiques et l'arithmétique des ordinateurs, notamment la vérification formelle des programmes et algorithmes utilisant l'arithmétique à virgule flottante. Elle est directrice de recherche à Inria, affiliée au laboratoire de méthodes formelles de l'université Paris-Saclay et au centre de recherche Inria Saclay-Île-de-France. Elle est également la première présidente du jury de l'agrégation française d'informatique.
Professeure à l'ENSIIE et membre de l'équipe Méthodes du laboratoire Samovar depuis le 1er janvier 2016.
Elle est actuellement en délégation dans l'équipe-projet Deducteam de INRIA Saclay au laboratoire LMF. Elle est co-directrice du GDR GPL (Génie de la programmation et du Logiciel) depuis le 1er janvier 2021. Elle a précédemment été responsable de l'équipe Conception et Programmation Raisonnées (CPR) du laboratoire Cedric jusqu'en juillet 2015 et co-responsable du groupe de travail LTP (Langages, Types et Preuves) du GDR GPL jusqu'en avril 2015. Ses principaux thèmes de recherche actuels sont la sémantique des langages de programmation, la preuve formelle et l'interopérabilité des outils de preuve.
Spécialiste du logiciel au sein du Service de sûreté de fonctionnement de la Direction du transport spatial du CNES.
Après une carrière d’enseignant-chercheur en logique et en langages de programmation, il a travaillé pendant quelques années sur l’application de la preuve mathématique dans les domaines des trains autonomes et de la cyber-sécurité. Actuellement, il s’intéresse à la sûreté de fonctionnement plus largement et en particulier à la prise en compte des pannes aléatoires dans la méthodologie de développement et de validation des systèmes critiques.
Chargé de recherche CNRS au LMF (Laboratoire Méthodes Formelles), Université Paris- Saclay, ENS Paris-Saclay, depuis 2017.
Diplômé de l'ENS Paris, il a auparavant effectué un postdoctorat au Max Plank Institute for Software Systems sur le projet RustBelt : étude et preuve formelle en Coq du système de types du langage Rust à l’aide de la logique de séparation concurrente Iris. Sa thèse, effectuée dans l’équipe Inria Gallium et soutenue à l'Université Paris-Diderot (aujourd'hui Université Paris Cité), avait obtenu le prix de thèse 2016 du GdR GPL. Il est également lauréat du prix Alonzo Church pour la conception et la mise en oeuvre de la plateforme Iris.
Directeur R&D de CLEARSY
CLEARSY est une PME française spécialisée dans l'invention de systèmes sûrs critiques, où il travaille depuis 2001 pour des projets industriels dans les domaines de la mobilité automatique et autonome terrestre et marine, de la santé, de la microélectronique, de l'énergie nucléaire et de l'espace. Ses sujets d'intérêt actuels sont la co-ingénierie de la sûreté et de la sécurité, l'intelligence artificielle sûre et la mobilité autonome, tous liés aux méthodes formelles.
Professeur du Collège de France, titulaire de la chaire Sciences du logiciel, et membre de l'Académie des sciences.
Ses travaux portent sur les langages et outils de programmation et sur la vérification formelle de logiciels critiques. Il est auteur de deux grands logiciels issus de la recherche, le langage de programmation fonctionnelle OCaml et le compilateur formellement vérifié CompCert.
Directeur des méthodes formelles chez BedRock Systems
Il dirige une équipe d'ingénieurs dans le développement et l'application d'outils pour prouver des propriétés profondes sur le code de bas niveau. Il a obtenu son doctorat à Harvard en 2014 sur les techniques évolutives de vérification dans les assistants de preuve fondamentaux. Avant BedRock, il a appliqué ces techniques à des systèmes cyber-physiques, des applications web et une base de données relationnelle.
Chargé de recherche à l'ONERA.
Après une formation en informatique théorique à l'ÉNS Lyon puis une thèse en 2013, Pierre Roux est aujourd'hui chargé de recherche à l'ONERA. Il y poursuit des travaux sur l'application des méthodes formelles aux systèmes embarqués aéronautiques, avec un intérêt particulier pour les assistants de preuve, l'optimisation convexe et l'arithmétique à virgule flottante.
Chercheur à PQShield.
Ses recherches se focalisent sur la conception et l'implémentation d'outils formels d'aide à la construction et la vérification de preuves de sécurité. Ses axes de recherche sont à la croisée de plusieurs domaines: langage de programmation, cryptographie, preuve formelle, formalisation des mathématiques. Pierre-Yves Strub est un des auteurs principaux de EasyCrypt, un assistant à la preuve dédié à la formalisation de propriétés de sécurité, dans le modèle calculatoire, de primitives cryptographiques.
Directeur technique de Systerel
Laurent Voisin applique depuis plus de 20 ans des méthodes formelles dans l'industrie, essentiellement dans le domaine ferroviaire. Il est également l'architecte principal de Rodin, la plate-forme de référence pour la modélisation formelle de systèmes en B événementiel.
Résumés et vidéos des exposés
Utilisation des méthodes formelles pour les systèmes critiques, par Thierry Lecomte (CLEARSY)
L'exposé aborde l'utilisation des méthodes formelles pour assurer la sûreté et la sécurité des infrastructures critiques. Il explique pourquoi les méthodes formelles sont utilisées, au travers du prisme des activités industrielles et du retour d'expérience collecté, notamment les accidents qui surviennent.
Des méthodes formelles en pratique, par Laurent Voisin (Systerel)
Les méthodes formelles fournissent un outil mathématique pour raisonner sur des systèmes informatique, permettant une maitrise accrue des risques. Nous donnerons quelques exemples de cas d'usage à l'échelle industrielle où leur apport est particulièrement saillant : Conception de système critique, Développement de logiciel critique, validation de données, validation de la spécification d'outils.
La face cachée de la sûreté de fonctionnement du logiciel, par Danko Ilik (CNES)
Le développement des méthodes formelles ces dernières décennies nous a fourni des outils permettant d’arriver à des niveaux de certitude élevés en ce qui concerne l’absence de pannes systématiques telles que les erreurs de conception, de programmation ou lors de la compilation. Cependant, certains modes de pannes semblent en pratique difficiles à traiter avec ces outils et c’est en particulier le cas avec les pannes aléatoires. Dans cet exposé, on s’intéressera à quelques sujets parmi les moins traités formellement et on motivera leur importance par l’exemple de certains projets relevant de la mission du CNES.
Vérification de systèmes embarqués aérospatiaux, par Pierre Roux (ONERA)
Les avions de ligne modernes embarquent de nombreux systèmes informatiques. Certains d'entre eux, comme les commandes de vol numériques, sont critiques et justifient des efforts pour augmenter notre confiance en leur correction. Nous donnerons un aperçu de quelques activités réalisées en ce sens à l'ONERA (Office National d'Étude et de Recherche Aérospatial) à Toulouse : analyse de sûreté de fonctionnement de systèmes, aspects temps réel des processeurs multicoeurs et des réseaux embarqués, et preuve formelle de propriétés numériques.
Vérification déductive de programmes assistée par ordinateur, par Xavier Leroy (Collège de France)
La vérification déductive consiste à annoter un programme par des assertions logiques et de vérifier que ces assertions sont vraies de toute exécution du programme, avec l'aide de démonstrateurs automatiques ou interactifs. En d'autres termes, on considère le programme comme une définition mathématique et on prouve des théorèmes à son sujet en s'aidant de la puissance de la machine. Après un exemple de vérification utilisant l'outil Frama-C WP, nous verrons comment les assistants à la démonstration tels que Coq et Lean permettent non seulement de vérifier des programmes, mais aussi de construire les principes de raisonnement -- les «logiques de programmes» -- adaptés à divers types de propriétés que l'on veut établir.
Logique de séparation : de la gestion de la mémoire à l'établissement de protocoles personnalisés, par Armaël Guéneau (Inria Saclay, LMF)
La logique de séparation, introduite dans les années 2000 afin de simplifier la preuve de programmes impliquant des pointeurs, est une extension de la logique de Hoare dans laquelle les assertions ne représentent non plus seulement des faits logiques, mais aussi des ressources qui sont possédées pendant la preuve du programme. Nous ferons un aperçu de cette logique dans le cadre de la gestion des pointeurs en preuve de programmes, puis nous expliquerons comment des extensions plus récentes dans la logique Iris reprend l'idée des ressources afin de permettre à l'utilisateur de définir et prouver des protocoles personnalisés entre différentes parties d'un programme.
High-assurance post-quantum cryptography: the ML-KEM case, par Pierre-Yves Strub (PQShield)
Concevoir, analyser et implémenter une bibliothèque de primitives cryptographiques correcte, sécurisée et efficace est une tâche délicate. Cette dernière peut être facilitée par l'utilisation de la cryptographie assistée par ordinateur, et notamment par le développement d'outils d'analyse formelle tirant parti des avancées dans le domaine de la vérification de programmes. Lors de cet exposé, je présenterai un aperçu des développements récents en cryptographie assistée par ordinateur et comment cette dernière a permis le développement d'une implémentation sure et efficace de la primitive cryptographique post-quantique ML-KEM.
Formalisation en mathématiques appliquées : définition des éléments finis, par Sylvie Boldo (Inria, LMF)
Dans cet exposé, on montrera des résultats de travaux communs entre informaticien(ne)s et mathématicien(ne)s appliqué(e)s. On s'intéresse ici à la résolution numérique d'équations aux dérivées partielles sur des géométries compliquées, dont une méthode de résolution commune est la méthode des éléments finis (MEF). Sur ce projet à long terme, on montrera une partie de la formalisation des mathématiques sous-jacentes, ainsi que la définition d'un élément fini, avec les valeurs, ensembles et preuves qu'il doit contenir. Enfin, on instanciera cet objet par une famille d'éléments finis simples, comme les éléments finis de Lagrange.
Verifying Industrial C++ Code, par Gregory Malecha (BedRock Systems)
BedRock secures workloads using runtime mechanisms that introspect and intervene from an independent and higher privileged security layer that runs underneath the host system. Operating outside of the system makes it possible to secure the host system in a non-circumventable manner. At the core of BedRock’s security layer is a micro-virtualization stack that we are hardening through formal methods. Verification at this layer requires reasoning about low-level, concurrent software and its interaction with hardware components. To this end, we have developed a separation logic for concurrent C++ and used it to specify a kernel-privileged micro-hypervisor and to verify host services that comprise the BedRock security layer. In this talk, I describe some of the challenges and solutions that we have developed.
L'édition 2025 d'Horizon Maths a eu lieu le lundi 12 mai 2025 de 9h à 18h dans l'Amphithéâtre Chaudron de l'ENSCP (11 rue Pierre et Marie Curie, Paris 5e).
Organisée sous la houlette de Patrice Bertail (Modal'X, Université Paris-Nanterre), la conférence avait pour thème : Mathématiques et sécurité alimentaire.
À l'automne 2023, la FSMP décide d'échanger les dates de ses conférences annuelles Mathématiques en mouvement et Horizon Maths : la première se tiendra désormais en automne, la seconde au printemps. Cette année de transition a donc vu deux conférences Mathématiques en mouvement (printemps et automne) tandis que le public d'Horizon Maths a dû patienter jusqu'au printemps 2024.
La journée Horizon Maths 2022, sur le thème Mathématiques et Gravitation, aura lieu le mardi 6 décembre 2022 de 9h à 17h à Sorbonne Université (4 place Jussieu 75005 Paris), Amphithéâre 25. Cette conférence est organisée sous la houlette de Jérôme Pérez (ENSTA Paris) et Emmanuel Trélat (Sorbonne Université).
La journée Horizon Maths 2021, sur le thème Mathématiques et Transports, a eu lieu le mardi 30 novembre 2021 de 9h à 18h à l'Institut Henri Poincaré (11 rue Pierre et Marie Curie 75005 Paris, voir l'accès ici). Cette conférence était organisée sous la houlette de Fabien Leurent (ENPC, Chaire Île-de-France Mobilités) et Bertrand Maury (ENS-PSL et Université Paris-Saclay).
En raison de l'épidémie de COVID 19, il n'y a pas eu de conférence Horizon Maths en 2020
Organisée sous la houlette de Gabriel Peyré (DMA, CNRS, ENS), Francis Bach (DI ENS) et Cordelia Schmid (Inria).
L'édition 2017 d'Horizon Maths est organisée avec Huawei sous la houlette de Gabriel Peyré (DMA, CNRS, ENS) et Merouane Debbah (Huawei), sur le thème Mathématiques et réseaux. Cette journée de conférences se tiendra le 30 novembre 2017 de 9h à 17h à l'Institut Henri Poincaré (11, rue Pierre et Marie Curie, 75005 Paris).
Exceptionnellement, il n'y a pas eu d'édition d'Horizon Maths en 2016, la FSMP était co‑organisatrice avec l'IHP du grand colloque Mathématiques, oxygène du numérique
Horizon Maths 2015 - Santé et données. Une conférence organisée par la Fondation Sciences Mathématiques de Paris et IBM France les 14 et 15 décembre 2015 à IBM.
Horizon Maths 2013 Conférences organisées par la FSMP et GDF SUEZ les 16 et 17 décembre 2013 à GDF SUEZ Thèmes abordés : Big data, Réduction de modèles, Théorie des jeux à champs moyens (mean field games theory), Problèmes en grandes dimensions, Marchés incomplets, Apprentissage.
Nouveaux modèles de climat, discrétisation des équations de la physique, en relation avec l'évolution des calculateurs, par Thomas Dubos (LMD, Ecole Polytechnique). Horizon Maths 2012, 19 et 20 décembre 2012 à l’Auditorium de Total - Conférences organisées par la FSMP et Total autour de deux thèmes : l’optimisation et le calcul massivement parallèle.
Euler 2D dans des domaines non réguliers par Christophe Lacave (IMJ, U. paris-Diderot). Une vidéo proposée dans le cadre des journées Horizon Maths 2011, organisées les 12 et 13 décembre 2011 par la Fondation Sciences Mathématiques de Paris, en partenariat avec AREVA.
Mesure et comptage des courbes planes réelles, par Jean-Yves Welschinger. Un exposé présenté lors de Horizon Maths 2010, deux journées de conférences mathématiques en direction des industriels organisées par la Fondation Sciences Mathématiques de Paris et EADS.
L'édition 2019 d'Horizon Maths a eu lieu le mardi 3 décembre 2019 de 9h à 17h dans l'amphithéâtre Charpak de Sorbonne Université (4, place Jussieu, Paris 5e).