Soutenance de thèse « La compilation au-delà de la sémantique pour la sécurité matérielle » par Sébastien Michelland

Nous avons l'honneur de vous inviter à la soutenance de thèse de Sébastien Michelland, intitulée « Compilation beyond semantics for hardware security », qui aura lieu le vendredi 24 octobre 2025 à 14 h au laboratoire LCIS à Valence. La soutenance se déroulera en anglais (diapositives et exposé).

Une version du manuscrit est disponible en ligne sur son site web.

Jury

En raison de leur déploiement sur le terrain, les systèmes embarqués sont exposés à des attaques physiques complexes. Par exemple, les injections de défauts provoquent des comportements anormaux dans le système en interférant avec les circuits (via des signaux, l’alimentation électrique ou tout autre moyen — tout est permis). Elles constituent une menace majeure qui ne se limite pas à des défaillances aléatoires dues à des défauts, mais qui inclut des attaques ciblées et orchestrées, capables de se faufiler même par les plus petites failles.

Les contre-mesures, lorsqu’elles existent, reposent sur un contrôle minutieux du matériel, des logiciels, ou des deux. Mais le simple fait de contrôler les couches logicielles, qui vont du code d’application de haut niveau (généralement en C) au code assembleur, s’avère difficile. Il est bien connu que la compilation des programmes peut détruire les composants logiciels des contre-mesures de sécurité. Par exemple, il est logique d’exécuter deux fois des calculs sensibles afin de détecter les erreurs induites par des défauts, mais comme cela n’a aucun effet sur la sémantique « sans défaut » du langage de programmation, le compilateur est libre (et programmé) pour supprimer les doublons.

Cette thèse analyse cette friction entre les contre-mesures de sécurité contre les attaques matérielles (principalement les injections de défauts) et la compilation du code C. Elle montre que l’ensemble de la chaîne de compilation est impliqué dans les failles de sécurité, des optimisations aux conversions (lowerings) en passant par les subtilités sémantiques des langages intermédiaires. Son principal résultat est Tracing LLVM, une extension open source légère de LLVM qui enrichit l’interface entre le programme et le compilateur afin de faciliter la mise en œuvre et la préservation des contre-mesures de sécurité.

Cette thèse a été préparée au laboratoire LCIS au sein de l’équipe CTSYS, et a bénéficié de l’expertise locale en conception matérielle et en injection de défauts.