Sélectionnez votre langue

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.

 

affiche hm 2024
Télécharger l'affiche.

  

Intervenant•e•s

  • 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)

Cliquez ici pour découvrir les intervenant•e•s e cette journée.

 

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

 

Vidéos et Résumés 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.
×
Stay Informed

When you subscribe to the blog, we will send you an e-mail when there are new updates on the site so you wouldn't miss them.

Séjour estival au Nesin Maths Village