HOPR - Raisonnement à l’ordre supérieur probabiliste et sensible aux ressources

Coordinateur : Patrick Baillot, CNRS, CRIStAL

Équipe : SyCoMoRES du Groupe Thématique : SISE

Dates : 2025 - 2029

Résumé :

La transition numérique s’accompagne de risques croissants en sécurité et en protection de la vie privée. Les méthodes formelles, au départ motivées par la vérification des logiciels critiques, ont été graduellement appliquées à la cryptographie et à la protection de la vie privée. En particulier les assistants de preuve spécifiques Easycrypt et Squirrel permettent de prouver la sécurité de constructions cryptographiques. La confidentialité différentielle, elle, est une notion de protection de la vie privée reposant sur des garanties statistiques. Vérifier qu’un programme donné satisfait la confidentialité différentielle peut cependant être difficile, et des méthodes formelles ont aussi été introduites à cet effet. Une différence entre Easycrypt/Squirrel et l’assistant de preuve généraliste Coq est que Coq gère les fonctions d’ordre supérieur, c’est-à-dire les fonctionnelles qui prennent des fonctions comme arguments. Ceci permet des preuves modulaires, et a ouvert la voie à la vérification de compilateurs et de théorèmes mathématiques. Squirrel et Eastcrypt ne disposent que d’une forme limitée d’ordre supérieur, insuffisante pour une véritable modularité, et ne permettent pas non plus de raisonner sur la complexité des attaquants. Cela vient de la difficulté de combiner dans un cadre logique commun trois caractéristiques : le calcul d’ordre supérieur, le raisonnement probabiliste et le calcul de complexité bornée. Notre 1er objectif est de définir des cadres logiques capables de gérer ensemble ces caractéristiques. Notre 2e objectif est d’exploiter ces cadres logiques dans les deux domaines d’application précédents. En cryptographie, nous étendrons le traitement de l’ordre supérieur et de la complexité de Squirrel et Easycrypt. En confidentialité différentielle nous définirons une nouvelle logique permettant à la fois la vérification de primitives et la définition de règles de typage permettant d’automatiser la vérification de grands programmes.

Abstract :

The digitalization of our societies comes with increasing risks in security and privacy. Formal methods based on logic initially developed for verification of critical software have been progressively applied to cryptography and privacy. In particular some domain-specific proof-assistant tools like Easycrypt and Squirrel can prove security of cryptographic constructions in the computational model, which provides strong guarantees. Differential privacy is a well-accepted notion of privacy relying on statistical guarantees. Ensuring that a given program is differentially private can however be a difficult task, and some formal methods have also been introduced for that. One difference though between the specialized tools above and the general-purpose Coq proof-assistant is that Coq supports higher-order functions, that is to say functionals which can take functions as arguments. This allows for modular proofs, which have been the key to some successes in verification of compilers and mathematical theorems. Squirrel and Easycrypt currently only feature a limited form of higher-order which is not sufficient for full modularity. They also lack reasoning on the complexity of attackers. This is due to the difficulty of combining in a common logical framework three advanced features : higher-order computation, probabilistic reasoning and representation of complexity-bounded computation. Our first objective is thus to define some logical frameworks that can handle together these features. Our second objective is to use these logical frameworks in the two application domains mentioned above. In cryptography we plan to extend the higher-order features and complexity analysis capabilities of Squirrel and Easycrypt. In differential privacy we plan to define a new Hoare logic combining the benefits of two existing approaches, that is to say allowing both for verification of primitives and for defining typing rules allowing to automate verification of large programs.