March 27 2024 : HORIZON MATHS

Mathematical proofs and software safety

The 2024 edition of Horizon Maths will take place on Wednesday March 27^th 2024 from 9 a.m. to 6 p.m. at IHP (11 rue Pierre et Marie Curie, Paris 5^e), Amphi Hermite, on the theme Mathematical proofs and software safety. The conference is organized under the coordination of Hugo Herbelin (IRIF, Inria). The organizers also thank Catherine Dubois (ENSIIE) and Xavier Leroy (Collège de France) for their precious help.

The day will include lectures and a round-table discussion. The full program will soon be available on this page.

Download the poster.

Registration

Registration is free but mandatory. Please register via the online form.

Speakers

Sylvie Boldo (Inria, LMF)
Catherine Dubois (ENSIIE)
Danko Ilik (CNES)
Jacques-Henri Jourdan (CNRS, LMF)
Thierry Lecomte (CLEARSY)
Xavier Leroy (Collège de France)
Gregory Malecha (BedRock Systems)
Pierre Roux (ONERA)
Pierre-Yves Strub (PQShield)
Laurent Voisin (Systerel)

Read more about the speakers.

Program

9:00-9:30 Welcoming and opening speeches

9:30-10:00 Utilisation des méthodes formelles pour les systèmes critiques, by Thierry Lecomte (CLEARSY)
10:00-10:30 Des méthodes formelles en pratique, by Laurent Voisin (Systerel)

10:30-11:00 Coffee break

11:00-11h:00 The Far Side of Software Dependability, by Danko Ilik (CNES)
11:30-12:00 Vérification de systèmes embarqués aérospatiaux, by Pierre Roux (ONERA)

12:00-12:30 Round table discussion: Training, with Catherine Dubois (ENSIIE) and the lectures speakers

12:30-14:00 Lunch break

14:00-14:30 Vérification déductive de programmes assistée par ordinateur, by Xavier Leroy (Collège de France)
14:30-15:00 Logique de séparation : de la gestion de la mémoire à l'établissement de protocoles personnalisés, by Jacques-Henri Jourdan (CNRS, LMF)
15:00-15:30 High-assurance post-quantum cryptography: the ML-KEM case, by Pierre-Yves Strub (PQShield)

15:30-16:00 Coffee break

16:00-16:30 Formalisation en mathématiques appliquées : définition des éléments finis, by Sylvie Boldo (Inria, LMF)
16:30-17:00 Verifying Industrial C++ Code, by Gregory Malecha (BedRock Systems)
17:00-17:45 Final foresight round table discussion, with Catherine Dubois (ENSIIE) and the lectures speakers

Summary of the talks

Utilisation des méthodes formelles pour les systèmes critiques, by 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, by 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, by 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, by 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, by 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, by Jacques-Henri Jourdan (CNRS, 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, by 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, by 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, by 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.