Preuve mécanisée

Membres

Membres permanents

  • Idir Ait-Sadoune
  • Thibaut Balabonski
  • Bruno Barras
  • Véronique Benzaken
  • Frédéric Blanqui
  • Valentin Blot
  • Sylvie Boldo
  • David Baelde (conception d'un prouveur interactif pour une logique orientée sécurité, utilisation de SMT envisagée)
  • Hubert Comon
  • Évelyne Contejean
  • Stéphane Demri
  • Gilles Dowek
  • Jean-Christophe Filliâtre (développeur d'un outil, Why3, qui est utilisateur de la preuve mécanisée)
  • Jacques-Henri Jourdan (preuve en logique de séparation Iris, preuve interactive de programmes avec mémoire faible)
  • Chantal Keller
  • Stéphane Le Roux
  • Claude Marché
  • Andrei Paskevich
  • Mihaela Sighireanu (preuve en logique de séparation, certification des résultats des SMT)
  • Burkhart Wolff

Membres non-permanents

  • Loris Cros
  • Boris Djalal
  • Louise Dubois de Prisque
  • Yacine El Haddad
  • Gaspard Férey
  • Quentin Garchery
  • Émilie Grienenberger
  • Gabriel Hondet
  • Antoine Lanco
  • Amélie Ledein
  • Yann Leray
  • Nicolas Meric
  • Thomas Traversie
  • Guillaume Verdier
  • Pierre Vial
  • Rébecca Zucchini

Membres associés

  • Catherine Dubois
  • Olivier Hermant

Mots-clés

  • preuve automatique
  • preuve interactive
  • interopérabilité des systèmes de preuve
  • cadre logiques
  • vérification croisée
  • Dedukti
  • Logipedia

Communication

Toute la communication s'effectue via le canal "Preuve mécanisée" du framateam du LMF.

Description

Cette équipe regroupe les concepteurs des outils de preuve mécanisée, des systèmes eux-mêmes jusqu'aux bibliothèques, assurant ainsi un continuum. Elle s'organise en trois axes : la conception et le développement de systèmes de preuves, l'interopérabilité entre systèmes de preuves, et le développement de bibliothèques et formalisations pour des thématiques données.

Axe 1 : Conception et développement de systèmes de preuve

L'équipe est le principal concepteur et développeur des systèmes de preuve suivants.

Le formalisme du lambda-pi calcul modulo théorie

Membres : Bruno Barras, Frédéric Blanqui, Valentin Blot, Gilles Dowek, Gabriel Hondet, Amélie Ledein

Le lambda-pi calcul modulo théorie est un cadre logique développé par l'équipe depuis une dizaine d'années qui généralise divers cadres logiques précédents (calcul des prédicats, Isabelle, lambda-Prolog, pure type systems, théorie des types de Martin-Löf, lambdapi-calcul) et permet l'encodage de nombreuses logiques et systèmes de preuve actuels (HOL Light, Isabelle/HOL, Matita, Coq, Agda). Il est implémenté dans le système Dedukti. Cela soulève de nombreux problèmes théoriques et pratiques:

  • Comment encoder dans le lambda-pi calcul modulo théorie, de manière correcte et complète, les fonctionalités des systèmes de preuve actuels (proof irrelevance, predicate subtyping, inductive and co-inductive definitions, cubical type theory, etc.) tout en préservant certaines propriétés du lambda-pi calcul (terminaison, confluence, préservation du typage)?
  • Comment comparer et traduire de l'un dans l'autre dans le lambda-pi calcul modulo théorie deux systèmes de preuve différents?
  • Peut-on équiper Dedukti d'une interface et d'un mécanisme de preuve interactif? Cela permettrait de vérifier directement dans Dedukti la combinaison de preuves réalisées dans différents prouveurs sans avoir à les traduire (e.g. si on a prouvé A=>B dans X et A dans Y, a-t-on effectivement B? si oui, dans quel système?). Les fonctionalités particulières à Dedukti (réécriture, buts d'unification) permettent également de définir des objets mathématiques complexes qu'il est difficile, voire impossible, à définir dans les systèmes actuels (e.g. les infini-catégories).

Logiciels: https://github.com/Deducteam

Systèmes de preuve orientée sécurité

Membres : David Baelde

Avec Charlie Jacomme (fin de thèse LSV), Adrien Koutsos (ancien thésard LSV) ainsi que Stéphanie Delaune (IRISA) et Solène Moreau (thésarde IRISA co-encadrée par S. Delaune et D. Baelde) nous avons développé un prouveur interactif permettant d'établir des propriétés de sécurité dans le modèle calculatoire. Le point de départ de ce travail est la logique proposée en 2014 par Comon et Bana pour établir des propriétés d'indistinguabilité dans le modèle calculatoire. Il s'agit en fait d'une axiomatisation en logique du premier ordre, les axiomes exprimant notamment des propriétés de sécurité telles que la résistance aux collisions, la propriété IND-CCA d'un chiffrement, etc. Cette logique "de base" ne parle que de messsages et, pour analyser un protocole, il fallait jusque là procéder à un encodage pour chaque trace d'exécution possible. Notre méta-logique internalise cet encodage et permet de raisonner de façon uniforme sur plusieurs traces à la fois. Notre prototype intègre quelques méthodes de raisonnement automatique basiques et permet déja, sur des protocoles simples, d'obtenir des preuves concises et naturelles. Nous l'avons utilisé pour analyser des propriétés d'accessibilité (e.g. authentification) et d'équivalence (e.g. non-traçabilité) dans diverses études de cas dont plusieurs protocoles RFID et des parties du protocole SSH. Nous explorons désormais l'extension de l'outil à des protocoles plus riches (e.g. comportant des manipulations d'états), cherchons aussi à obtenir des garanties de sécurité indépendantes de la longueur des traces, et à améliorer l'automatisation via l'intégration de techniques SMT.



Il participe également au développement des systèmes suivants.

Isabelle

Membres : Idir Ait-Sadoune, Nicolas Meric, Burkhart Wolff

Au dela des developpements substantielles variés de libraries pour l' Archive of Formal Proofs (Isabelle/AFP), qui couvre des domaines fondamentales (HOL-CSP, UTP, Clean, TESL-Semantics ... ) ou applicatives (Network-Models, Security Policies, UML-Model-Transformations, OS-Kernels ...), il y a une tradition de developpements des "tools-as-components-on-top" du noyau d'Isabelle. Coté noyau, le groupe a été impliqué dans l'amelioration de sa parallelisation (Projet ANR-ParalITP 2011-2016). Coté outils, les systèmes

ont été developpés.

Il y a une groupe de discussion plus ou moins régulier concernant tout les aspects d'Isabelle, le Isabelle-Club.

Méthodes B/Event-B

Membres : Idir Ait-Sadoune, Guillaume Verdier (Post-doc)

L'objectif de cet axe est d'étudier l'extension de la méthode Event-B pour prendre en charge les développements de systèmes complexes nécessitant la modélisation d’objets mathématiques et le support des preuves associées. Plus précisément, permettre aux modèles Event-B d'importer et d'utiliser des théories de domaine. Concernant la vérification des théories définies et importées, il est important de proposer un système de preuve qui étend les prouveurs actuels de la méthode Event-B pour prendre en charge cette extension et intégrer au processus de preuve les définitions importées à partir des théories référencées.

Axe 2 : Interactions entre systèmes de preuves, bibliothèques universelles

La multiplicité des systèmes de preuve permet aujourd'hui de vérifier formellement et de manière la plus automatisée possible des énoncés complexes et variés. Cependant, cela s'accompagne d'une duplication des efforts extrêmement prononcée : valider une preuve dans un système donné demande de formaliser tous les pré-requis dans ce système, même s'ils existent par ailleurs. L'objectif de cet axe est de travailler à l'interopérabilité entre systèmes de preuve, et de proposer une bibliothèque de preuves formalisées que l'on peut importer dans la plupart des systèmes.

Certificats de preuve

Membres : Frédéric Blanqui, Valentin Blot, Boris Djalal, Gilles Dowek, Yacine El Haddad, Quentin Garchery, Chantal Keller, Claude Marché, Andrei Paskevich, Mihaela Sighireanu, Pierre Vial

L'objectif est d'explorer les preuves comme protocole de communication entre systèmes de preuves, afin d'échanger des résultats et de valider ceux-ci au sein d'un même système. Cette approche est mise en pratique dans les aspects suivants :

  • Interaction sûre entre prouveurs interactifs et prouveurs automatiques : l'objectif est de faire bénéficier chacun des deux systèmes des avantages de l'autre à travers l'échange de certificats : d'une part, via des encodages, les prouveurs interactifs pourront bénéficier de davantage d'automatisation ; d'autre part, les prouveurs automatiques pourront valider leurs résultats à l'aide d'un outil certifié. Cela est mis en pratique notamment dans l'outil SMTCoq, dont le but est de faire interagir l'assistant de preuve Coq avec des prouveurs automatiques du premier ordre (de type SMT : Satisfiabilité Modulo Théories). Une autre application est l'utilisation de prouveurs SMT en logique de séparation, pour la sécurité, ou encore pour la preuve de programmes.
  • Conception de certificats de preuves : l'objectif est de concevoir et générer des certificats de preuves pour divers outils. Dans ce cadre, l'outil ekstrakto a pour but de générer des certificats de preuves à partir de sorties de prouveurs automatiques du premier ordre. Une autre application est la génération de certificats pour les outils de preuve de programmes, et notamment les calculs d'obligation de preuves effectués dans Why3.

Logiciels : SMTCoq, ekstrakto

Groupe de travail DigiCosme UPSCaLe

Logipedia

Membres : Bruno Barras, Frédéric Blanqui, Valentin Blot, Gilles Dowek, Chantal Keller, Burkhart Wolff

À compléter (Gilles ?)

Bibliothèque : Logipedia

Axe 3 : Formalisations et développement de bibliothèques

Pour les données

Membres : David Baelde, Véronique Benzaken, Évelyne Contejean, Chantal Keller, Rébecca Zucchini

Cet axe couvre la formalisation de résultats fondamentaux en science des données, le développement d'outils certifiés pour la manipulation de données, et de bibliothèques pour la formalisation des langages centrés données. Les aspects étudiés sont :

  • la formalisation de langages centrés données et de compilateurs pour ces langages
  • la formalisation de mécanismes afférents à la manipulation des données, comme la sécurité ou la provenance des données.

Projet : DataCert

Groupe de travail DigiCosme Transform

Pour les mathématiques

Membres : Sylvie Boldo

La résolution des équations aux dérivées partielles (EDP) est au cœur de nombreux programmes de simulation dans l'industrie et la méthode des éléments finis (MEF) est un outil très populaire pour leur résolution numérique. Il s'agit de poser les fondements qui nous permettront de prouver la correction d'une bibliothèque implantant la MEF en C++, telle que FELiScE (Finite Elements for Life Sciences and Engineering). Sa vérification formelle augmentera la confiance dans tous les codes qui l'utilisent. Ce projet est interdisciplinaire avec l'analyse numérique.

Ces preuves reposent entre autres sur la théorie de la mesure, l'intégrale de Lebesgue, les distributions et les espaces de Sobolev. Nous souhaitons formaliser et prouver en Coq les bases mathématiques jusqu'à la construction de l'espace fonctionnel L 2 ainsi que les propriétés afférentes, en particulier la complétude pour la norme associée au produit scalaire.

Pour la preuve de programmes

Membres : Jean-Christophe Filliâtre, Jacques-Henri Jourdan, Andrei Paskevich, Mihaela Sighireanu, Burkhart Wolff

La preuve de programmes nécessite des bibliothèques de plusieurs natures : d'une part, des bibliothèques pour spécifier et prouver (séquence, ensembles, dictionnaires, etc.) ; d'autre part, des bibliothèques de programmes déjà prouvés servant de briques de bases (des structures de données, notamment, mais pas uniquement). Ces deux sortes de bibliothèques ne sont pas disjointes. Le code fantôme, par exemple, utilise des bibliothèques de programmes dans une activité liée exclusivement à la spécification et à la preuve. Le degré d'automatisation des preuves que l'on peut espérer dans la preuve de programmes dépend fortement de la façon dont ces bibliothèques ont été conçues.

Bibliothèques : Iris, vocal, stdlib Why3

on peut finalement aussi mentionner:

  • Isabelle/C Plateforme pour Test et Preuve des Programmes C

Bibliothèques de lemmes pour la preuve d'algorithmes sur les structures de données dynamiques (en C ou Ada). Ce travail a été effectuée pour l'outil Verifast pour la vérification de programmes C avec la logique de séparation. Il peut être étendu à d'autres structures de données et d'autres outils.

Pour la modélisation de robots

Membres : Thibaut Balabonski, Évelyne Contejean, Robin Pelle

À compléter (Thibaut)