Ce stage se base sur un outil interne permettant la génération automatique de code C correspondant à des piles protocolaires à partir des spécifications. Ces spécifications seront écrites dans le langage F*, un langage pouvant faire l'objet de vérifications formelles de sécurité, afin de garantir la sécurité du protocole implémenté. En fonction du résultat de la vérification formelle du protocole, il est alors possible de générer le code C correspondant aux participants du protocole ou bien celui d'un attaquant implémentant une possible attaque trouvée pour l'outil de vérification. Générer automatiquement le code permet à la fois de gagner du temps de développement, de standardiser le forme du code pour différents protocoles et de réduire les erreurs humaines.

Cependant, la gestion des primitives cryptographiques dans la génération du code représente un challenge scientifique et technique. En effet, plusieurs contraintes de taille et/ou, de format peuvent exister (par exemple une clé RSA ne peut chiffrer des volumes importants de données) et ces contraintes doivent apparaître dans la modélisation afin de ne pas laisser l'utilisateur commettre des erreurs dans les choix de primitives. Certaines primitives peuvent également avoir des propriétés équivalentes et être interchangeables. Enfin, certains cas d'applications peuvent requérir des primitives très particulières (ex: crypto homomorphe) devant être modélisées au moyen de théories équationnelles.

Le candidat devra être en mesure de:

1) Prendre en main l'outil de génération de code existant, d'y ajouter des implémentations de primitives cryptographiques (basées sur des bibliothèques comme mbedTLS) et permettre une interchangeabilité des primitives si leurs propriétés le permettent ;

2) Ajouter des fonctionnalités à l'outil afin de définir des contraintes sur l'utilisation de primitives cryptographiques afin de détecter des incohérences lors de la génération de code ;

3) Permettre la modélisation de théories équationelles pour décrire des primitives aux propriétés particulières.