[THESIS DEFENSE] Johan Laurent - "Modélisation de fautes utilisant la description RTL de microarchitectures pour l’analyse de vulnérabilité conjointe matérielle-logicielle"

on the November 19, 2020


Johan Laurent will defend his PhD Thesis entitled "Modélisation de fautes utilisant la description RTL de microarchitectures pour l’analyse de vulnérabilité conjointe matérielle-logicielle" supervised by Vincent Beroulle (LCIS), Christophe Deleuze (LCIS) & Florian Pebay-Peyroula (CEA-Leti)

Thesis summary

"La sécurité numérique est aujourd’hui un enjeu majeur dans nos sociétés. Communications, énergie, transport, outils de production, Internet des Objets… Les systèmes numériques se multiplient et deviennent toujours plus critiques pour le bon fonctionnement du monde. Depuis un peu plus d’une vingtaine d’années, une nouvelle menace a émergé pour attaquer les systèmes : l’injection de faute. Elle consiste essentiellement à perturber un circuit pendant son fonctionnement, par diverses méthodes comme des perturbations sur l’alimentation du circuit, l’injection électromagnétique, ou l’injection laser ; afin de provoquer des erreurs. Ces erreurs peuvent ensuite être exploitées par un attaquant pour révéler des informations secrètes du circuit, ou passer outre des mesures de sécurité.

La complexification des systèmes numériques et les avancées technologiques comme la finesse de gravure rendent particulièrement vulnérables les systèmes numériques face aux attaques par injection de fautes. Pour contrer ces attaques efficacement et à un coût raisonnable, il est nécessaire de penser la sécurité dès la phase de conception du système. Pour cela, il faut comprendre précisément l’impact de ces fautes sur les processeurs. Les effets induits peuvent être modélisés à différents niveaux d’abstraction. Actuellement, si l’impact des fautes est relativement bien connu au niveau matériel, leurs effets au niveau logiciel restent mal compris. Les analyses de vulnérabilité au niveau logiciel se basent donc sur des modèles de faute logiciels simples que sont par exemple le saut d’instruction, la corruption de registre ou l’inversion de test. Ces modèles sont appliqués sans réelle prise en compte de la microarchitecture du processeur attaqué. Cette non-considération de l’aspect matériel pose la question du réalisme des modèles logiciels, qui conduit à deux types de problèmes : certains effets modélisés ne correspondent pas à des vulnérabilités réelles ; et, à l’inverse, certains effets affaiblissant la sécurité ne sont pas modélisés. Ces difficultés se transposent ensuite dans des contremesures sur-dimensionnées, ou, plus grave, sous-dimensionnées.

Pour lutter contre ces limitations des modèles de faute logiciels usuels, une étude précise de la microarchitecture des processeurs est requise. Dans cette thèse, nous explorons tout d’abord en quoi différentes structures du processeur, comme le pipeline ou les optimisations de forwarding et d’exécution spéculative, peuvent influer sur le comportement des fautes au sein du processeur et en quoi ces structures peuvent mettre à mal une vision purement logicielle de l’impact des fautes sur l’exécution d’un programme. Des injections au niveau RTL dans un processeur d’architecture RISC-V sont effectuées pour montrer que ces effets pourraient être exploités pour attaquer des contremesures logicielles typiques, ou encore une application de vérification de PIN sécurisée. Dans un deuxième temps est développée une méthode pour étudier plus généralement les effets des fautes dans un processeur. Cette méthode a un intérêt double. Le premier est la modélisation de fautes au niveau logiciel, avec notamment la définition de métriques d’évaluation des modèles. Le second est de conserver un lien avec le niveau RTL afin de pouvoir concrétiser les effets obtenus au niveau logiciel. Pour terminer cette thèse, nous étudions la possibilité d’utiliser des méthodes d’analyse statique pour analyser la sécurité de programmes face aux modèles de faute logiciels définis précédemment. Une analyse par interprétation abstraite et une analyse par exécution symbolique sont abordées.

Cette thèse, financée par l’IRT Nanoelec pour le projet Pulse, a été réalisée au sein du laboratoire LCIS de Valence, en collaboration avec le CEA-Leti de Grenoble. Elle a été dirigée par Vincent Beroulle (LCIS) et co-encadrée par Christophe Deleuze (LCIS) et Florian Pebay-Peyroula (CEA-Leti)."

Defense jury

  • Karine Heydemann  - Maître de conférences HDR Université Sorbonne (Rapportrice)
  • Jean-Max Dutertre - Professeur Université Saint-Etienne (Rapporteur)
  • Bruno Rouzeyre    - Professeur Université Montpellier (Examinateur)
  • Lilian Bossuet    - Professeur Université Saint-Etienne (Examinateur)
Published on November 19, 2020