Postée il y a 13 heures
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.