Missions

Le ou la candidate mènera des travaux de recherche en informatique théorique au sein de l'équipe SPICY de l'IRISA (Rennes). Ce projet concerne des développements théoriques, et éventuellement pratiques, autour de l'assistant de preuve Squirrel pour les protocoles cryptographiques. Il s'agira d'étendre la logique sous-jacente pour faciliter l'utilisation d'ordre supérieur.

Activités

La logique CCSA (Computationally Complete Symbolic Attacker) permet de raisonner
sur les protocoles cryptographiques et les messages qu'ils contiennent.
Son origine se trouve dans les travaux de Bana et Comon [1], qui étaient fondés sur
la logique du premier ordre. Elle a ensuite évolué progressivement pour devenir une logique CCSA d'ordre supérieur [2], et a été implémentée dans l'assistant de preuve Squirrel [3]. Une
introduction générale à la logique CCSA et à Squirrel est disponible en [4].

Dans les preuves de sécurité cryptographiques, les attaquants considérés disposent d'une puissance de calcul limitée, car il n'est généralement pas possible de garantir la sécurité contre un attaquant tout puissant. Cette restriction apparaît donc naturellement
de plusieurs façons dans notre logique -- voici deux d'entre elles. D'une part, la logique CCSA s'accompagne d'une méthode pour encoder sous forme de schéma d'axiomes des hypothèses cryptographiques, c'est-à-dire des paires de jeux cryptographiques que l'on suppose indistinguables. Ces axiomes demandent en particulier -- de plusieurs façons que l'on ne détaillera pas ici -- que certains sous-termes soient calculables par un adversaire dans le jeu qu'ils expriment. Puisque les adversaires sont des machines de Turing probabilistes polynomiales (PPTIME), utiliser ces axiomes demande donc de vérifier que des termes sont calculables en PPTIME. D'autre part, la logique contient un prédicat exprimant l'indistinguabilité calculatoire, et le raisonnement sur ce prédicat fait souvent intervenir des réductions dans lesquelles le distingueur doit calculer lui même certaines parties d'un terme, qui doivent donc être calculables en PPTME.


Squirrel utilise actuellement des critères très simples pour s'assurer qu'un terme est calculable en PPTIME. Ceux-ci suffisent en pratique, principalement parce que les preuves de protocoles que nous faisons aujourd'hui reposent sur des définitions récursives simples et écrites en dur, qui décrivent les observables lors d'une interaction entre l'adversaire et le protocole. Cependant, la logique elle-même permet des définitions récursives plus complexes, contenant notamment des termes d'ordre supérieur. Celles-ci commencent seulement à être utilisées, dans des preuves plus compliquées et expérimentales. Prouver des garanties de complexité pour de tels termes requerra des techniques plus puissantes. Par ailleurs, le prédicat d'indistinguabilité ne peut pour l'instant s'appliquer qu'à des termes d'ordre au plus 1. L'étendre à des termes d'ordre supérieur apporterait une plus grande uniformité et flexibilité au système de preuve, mais cela demande un modèle de coût pour l'ordre supérieur.

Le but de ce post-doc sera de s'attaquer à ces problèmes au niveau de la théorie, et d'explorer de nouvelles applications aux preuves cryptographiques du langage enrichi que l'on aura mis au point. D'une part, le ou la candidate adaptera des techniques de complexité implicite et de calculabilité d'ordre supérieur, pour équiper la logique CCSA d'un modèle de coût d'ordre supérieur approprié, ainsi que de moyens d'établir des bornes de complexité. D'autre part, il ou elle étudiera comment ces fondements théoriques peuvent être mis en pratique dans Squirrel, pour permettre de nouvelles applications mettant en jeu des constructions d'ordre supérieur plus riches.




Détails supplémentaires

Les preuves de complexité en Squirrel pourraient se présenter sous divers aspects, en s'inspirant de plusieurs travaux précédents, tels que les 'sized types' [5], les preuves circulaires [6], la programmation fonctionnelle [7] ou les classements de termes [8].
Vraisemblablement, les techniques de complexité implicite les plus expressives ne deviendront utiles que dans le cas de définitions récursives plus complexes que celles qui apparaissent dans les développements Squirrel existants. De telles définitions pourraient émerger dans certaines applications cryptographiques, que nous allons maintenant décrire.

Lorsque l'on modélise des protocoles cryptographiques, il est souvent naturel de raisonner avec des oracles, qui peuvent être appelés par un adversaire pour obtenir certaines informations. Un exemple classique est celui d'une fonction de hachage, que l'on peut modéliser en donnant accès à l'adversaire à un oracle qui renvoie le haché de tout message sur lequel on l'appelle -- cet oracle peut ensuite être idéalisé, en le remplaçant par un oracle aléatoire qui renvoie toujours une valeur fraîchement générée, si l'on suppose que la fonction de hachage est pseudo-aléatoire.
Dans les preuves Squirrel existantes, de tels oracles sont modélisés par des sous-processus ajoutés à la spécification du protocole. Ce style de modélisation, hérité de versions antérieures de la logique qui n'étaient pas d'ordre supérieur, oblige les appels aux oracles à être explicitement contenus dans la trace d'exécution du protocole, ce qui permet des raisonnements basiques. Cependant, des travaux en cours sur des preuves plus complexes suggèrent qu'il serait peut-être plus pratique de modéliser les oracles par des fonctions du premier ordre, c'est-à-dire des lambdas, que l'on donnerait directement à l'adversaire.
Pour cela, il faut pouvoir raisonner sur des constructions d'ordre supérieur (l'adversaire devient lui même d'ordre au moins 2) lorsque l'on applique des arguments cryptographiques, ce que l'on ne sait pour l'instant pas faire. Des expériences ont été menées dans ce sens, et nous avons l'intention d'explorer plus en profondeur dans quelle mesure ce style de modélisation facilite l'écriture de preuves. Ceci demandera plusieurs extensions à la logique actuelle. En particulier, il faudra définir un modèle d'exécution et de coût à l'ordre supérieur : que signifie donner accès à une fonction d'ordre supérieur à l'adversaire ? Lui demander d'en renvoyer une ? Si un adversaire appelle un oracle d'ordre supérieur sur une fonction du premier ordre qu'il a lui même calculée, le temps d'exécution de cette fonction lorsque l'oracle s'en sert doit-il compter dans le temps de calcul de l'adversaire ? On doit également se demander comment raisonner, dans la logique elle-même, sur les appels aux oracles faits par l'adversaire : certaines preuves, sur le papier, fonctionnent par exemple en choisissant au hasard l'un de ces appels, ce que l'on ne sait pour l'instant pas exprimer dans la logique.

Plus généralement, il serait intéressant d'explorer des styles de modélisation alternatifs pour les protocoles eux-mêmes, en mettant à profit l'ordre supérieur. En principe, il devrait être possible de modéliser un protocole par une collection de lambda-termes donnés à l'adversaire, plutôt que comme un processus. Un protocole avec état serait alors naturellement encodé avec des continuations, soumises à une politique d'utilisation linéaire. Le raisonnement sur les protocoles prendrait une forme tout-à-fait différente, qu'il faudrait mettre au point, probablement en s'inspirant d'autres applications plus conventionnelles en vérification.


Références


[1] Bana, Comon. "A computationally complete symbolic attacker
for equivalence properties." CCS 2014.
[2] Baelde, Koutsos, Lallemand. "A higher-order indistinguishability logic for
cryptographic reasoning." LICS 2023.
[3] Baelde et al. "An interactive prover for protocol verification in the
computational model." S&P 2021.
[4] Baelde et al. The Squirrel Prover and its Logic. SIGLOG newsletter 2024/04.
[5] Avanzini & Dal Lago. Automating Sized-Type Inference for Complexity
Analysis. ICFP'17.
[6] Curzi & Das. Cyclic Implicit Complexity. LICS'22.
[7] Hoffmann, Aehlif & Hofmann. Resource aware ML. CAV'12.
[8] Avanzin, Eguchi & Moser. A New Order-theoretic Characterisation of the
Polytime Computable Functions. APLAS'12.

Compétences

- Doctorat en informatique, idéalement dans un domaine en lien avec la logique, le lambda calcul
- Le ou la candidate devra faire preuve d'une bonne expertise dans le domaine des langages d'ordre supérieur et des fondements théoriques de la calculabilité.
- Des connaissances en cryptographie ne sont pas nécessaire, bien qu'elles puissent s'avérer utiles.
- Le ou la candidate pourra éventuellement être amenée à utiliser Squirrel pour écrire des preuves de taille conséquente, ou à implémenter de nouvelles fonctionnalités dans l'outil, mais ce n'est pas une obligation. Cependant, ce projet étant à l'intersection entre théorie et application, un ou une candidate ayant la capacité et la motivation à travailler sur les deux aspects serait idéal.

Contexte de travail

Ce postdoc s'inscrit dans le cadre du projet ANR HOPR et aura lieu à l'IRISA.

A propos du laboratoire :
L'IRISA est aujourd'hui l'un des plus grands laboratoires de recherche français (plus de 850 personnes) dans le domaine de l'informatique et des technologies de l'information. Structuré en sept départements scientifiques, l'IRISA est un centre de recherche d'excellence dont les priorités scientifiques sont la bio-informatique, la sécurité des systèmes, les nouvelles architectures logicielles, la réalité virtuelle, l'analyse des big data et l'intelligence artificielle. Tourné vers l'avenir de l'informatique et nécessairement tourné vers l'international, l'IRISA est au cœur même de la transition numérique de la société et de l'innovation au service de la cybersécurité, de la santé, de l'environnement et de l'écologie, des transports, de la robotique, de l'énergie, de la culture et de l'intelligence artificielle.
Présentation de l'IRISA en tant que laboratoire d'affectation : https://www.irisa.fr/umr-6074
Présentation du CNRS en tant qu'employeur : https://www.cnrs.fr/fr/le-cnrs
présentation de l'équipe d'accueil : https://www-spicy.irisa.fr/

Contraintes et risques

Des déplacements chez les partenaires du projet (par ex. Lille, Paris, Sophia) pour des réunions d’avancement sont prévus.