Compilation robuste à l'injection de fautes, formellement vérifiée // Formally Verified Hardening of a Compiler Against Fault Injection

Construction d'un système formalisé dans l'assistant de preuves Rocq/Coq pour formaliser le développement de compilateurs optimisants robustes à l'injection de fautes - notamment des fautes matérielles. L'objectif est de pouvoir garantir la correction et la robustesse des programmes compilés - vis-à-vis du code source et de modèles d'attaquants à différents niveaux d'abstraction.

Concrètement, il s'agit:
- d'incorporer des modèles de fautes au sein des sémantiques formelles de programme;
- formaliser une notion de raffinement/sémantique entre de telles sémantiques formelles qui garantisse une forme de préservation des comportements, y compris en présence d'attaque correspondant aux fautes modélisées;
- permettre la décomposition du compilateur sous formes de passes indépendantes qui soit ajoutent des protections (contre-mesures), soit optimisent le code ou changent de représentation/langage, avec une preuve de raffinement;
- permettre de préciser les modèles de fautes au fur et à mesure qu'on s'approche du bas-niveau, en décrivant ces fautes dans des annotations du code.

Par rapport à d'autres travaux cherchant à ajouter une forme de robustesse à des compilateurs existants - mais qui n'avaient pas été prévus pour ça, l'objectif est ici de définir un cadre formalisé conçu pour le développement de compilateurs robustes et optimisants.

Début de la thèse : 30/09/2025

Autres financements

Université Grenoble Alpes

217 MSTII - Mathématiques, Sciences et technologies de l'information, Informatique

Connaissance de l'assistant de preuves Rocq/Coq, développement de compilateurs.
Rocq proof assistant; compiler design.