Raisonnement à l'ordre supérieur probabiliste et sensible aux ressources – HOPR

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 Easycrypt 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.