Thèse (h/f) : compilation certifiée de langages de bas niveau

Le langage de programmation de bas niveau Jasmin est conçu pour l’implémentation
de bibliothèques cryptographiques ayant de fortes garanties. Suffisamment de
contrôle est laissé aux programmeurs pour atteindre des performances à
l’exécution optimales tout en garantissant diverses propriétés de sûreté et de
sécurité, telles que “constant-time”, une contre-mesure répandue aux attaques
par canaux auxiliaires. Le compilateur pour ce langage, qui produit de
l’assembleur à partir de programmes Jasmin, est écrit et vérifié au moyen de
l’assistant à la preuve Coq: son théorème de correction justifie que les
résultats démontrés au niveau des programmes sources s’appliquent bien au niveau
de l’assembleur.

Le but de ce travail de thèse est d’étudier comment des techniques de
compilation, dédiées à la programmation de bas niveau, peuvent soulager tant
l’effort d’écriture des programmes que celui de leur vérification. En effet,
aujourd’hui, écrire un programme en Jasmin requiert de se soucier de nombreux
détails, généralement pris en charge automatiquement par les compilateurs:
sélection et ordonnancement des instructions, spilling, etc. En outre, comme
l’ont montré les diverses études de cas réalisées jusqu’à présent, il reste très
difficile de réutiliser tout ou partie du programmes existants ainsi que leurs
preuves. Aussi, cette thèse vise d’une part à ajouter de la flexibilité au
compilateur sans compromettre le contrôle fin des détails ni remettre en cause
la possibilité de raisonner précisément au niveau du code source, et d’autre
part à explorer des méthodes de compilation séparée pour rendre les programmes
jasmin plus modulaires. La validation de ces travaux autour du langage et de son
compilateur passera par la réalisation d’une étude de cas d’envergure.

Une expérience avec le compilateur Jasmin est fortement appréciée.


Contexte de travail

Le ou la doctorant(e) sera accueilli(e) dans les locaux du Loria à
Vandœuvre-lès-Nancy et rejoindra l’équipe Pesto et sera amené(e) a interagir
avec les membres du groupe Formosa. Le Loria est une Unité Mixte de Recherche
(UMR 7503), commune à plusieurs établissements : le CNRS, l’Université de
Lorraine, CentraleSupélec et Inria. Pesto est une équipe-projet Inria dont le
but est la construction de modèles formels et de techniques pour la conception
et l’analyse, assistées par ordinateur, de protocoles de sécurité, au sens
large. Le groupe Formosa étudie et développe la cryptographie formellement
vérifiée et ses implémentations efficaces, notamment via les outils Jasmin et
EasyCrypt.


Le poste se situe dans un secteur relevant de la protection du potentiel scientifique et technique (PPST), et nécessite donc, conformément à la réglementation, que votre arrivée soit autorisée par l'autorité compétente du MESR.