Vérification compositionnelle de la robustesse de systèmes matériels/logiciels soumis à des attaques par injection de fautes

Contexte.

La sécurité des systèmes embarqués repose sur la sécurisation des supports d’exécution matériels (HW) et des applications logicielles (SW) qui s’exécutent sur ces derniers, face à divers types de menaces, représentées par des modèles d’attaquants. Les attaques en faute visent à produire des fautes logiques induisant des modifications du comportement des applications (modification du flot d’exécution et/ou des données manipulées), afin d’en déduire un avantage (par exemple court-circuiter un test d’accès, ou récupérer une information sensible).

Afin de limiter les dommages induits par ces attaques, des contre-mesures sont déployées à différents niveaux (code source, binaire, micro-architecture du composant matériel), chacune répondant à un modèle d’attaque propre, pour un niveau de représentation et un périmètre donnés. L’analyse de la bonne complémentarité des différentes contre-mesures mises en œuvre reste une question à étudier : toutes les fautes du modèle de menace sont-elles capturées ? L’activation d’une contre-mesure n’obère-t-elle pas le fonctionnement d’une autre ? Comment construire une contre-mesure logicielle permettant de contourner une vulnérabilité matérielle (sans augmenter la surface d’attaque) ?

Les méthodes formelles présentent un intérêt particulier dans le contexte des fautes intentionnelles, puisqu’on veut prouver la sécurité du système quelque soit le point d’injection choisi par l’attaquant, ce qui suppose de faire une analyse considérant exhaustivement tous les points d’injection possibles. Elles sont cependant limitées par la combinatoire des problèmes analysés (complexité de blocs d’instructions avec ROBUSTB [Brejon et al. 2019], modèles logiques de circuits cryptographiques avec FIVER [Richter et al. 2021], code d’une centaine d’instructions sur microarchitecture RISC-V avec μArchiFI [Tollec et al. 2023]). Différentes approches permettent de repousser les limites de la complexité des systèmes analysés, tirant partie de la structure des modèles sous-jacents (k-partitionnement des ressources matérielles [Tollec et al. 2024], exploitation de la généricité des algorithmes [Tan et al. 2024], établissement de contrats liant les modèles SW et HW pour les attaques analysant les fuites d’information [Haring et al. 2024]). Par ailleurs, une approche compositionnelle peut être utilisée pour analyser le comportement de systèmes à base de composants soumis à des fautes [Baarir et al. 2011].

La méthodologie développée au CEA-List permet l’analyse de la robustesse aux fautes d’une application s’exécutant sur des cœurs de processeurs. Elle peut identifier les vulnérabilités de la plate-forme matérielle et de l’application, ou prouver la robustesse du système (vis-à-vis d’un modèle d’attaquant et d’une propriété de sécurité) ; elle s’appuie sur l’outil μArchiFI, utilisant des techniques de bounded model checking pour identifier les comportements d’un système soumis à des fautes menant à des vulnérabilités. Une approche complémentaire, le k-partitionnement (k-FRP), dédiée aux systèmes pourvus de protections basées sur une redondance matérielle, a été utilisée pour prouver la robustesse du Secure Element de l’OpenTitan vis-à-vis d’une injection de faute de type bit-flip [Tollec et al. 2024].

Objet de recherche

Le projet de recherche de la thèse est l'analyse de la composition de contre-mesures par méthode formelle, inspirée de ces méthodologies d’analyse pré-silicium (μArchiFI et/ou kFRP). On adoptera une démarche compositionnelle s’appuyant sur des points de coupure de différentes natures (composants matériels / fonctions logicielles, interface matérielle/logicielle, classes d’instructions …). L’analyse de contre-mesures dans un modèle d’attaquant combinant fautes et analyse de fuite pourrait également être une piste d’étude.

Cas d’étude.

• Cœur RISC-V CV32E40S intégrant différents types de contre-mesures et code VerifyPIN puis contre-mesure MAFIA issue de l’état de l’art
• Cas d’étude sélectionnés par les partenaires du projet PTCC-FORWARD

Le LIP6, Unité Mixte de Recherche (UMR 7606) de Sorbonne Université (SU) et du Centre National de la Recherche Scientifique (CNRS), est un laboratoire de recherche en informatique fort d’environ 450 membres, dont plus de 170 chercheurs et enseignants/chercheurs permanents.

Ses activités de recherche sont réalisées au sein de dix-huit équipes articulées autour de quatre axes transverses :

• Intelligence artificielle et sciences des données
• Architecture, systèmes et réseaux
• Sécurité, sûreté et fiabilité
• Théorie et outils mathématiques pour l’informatique

Conditions de préparation de la thèse La thèse est proposée dans le cadre du projet PTCC-FORWARD (01/2025 – 12/2028)

En partenariat entre le LIP6/Sorbonne Université (Paris) et le CEA List (Saclay & Grenoble)

La personne recrutée exercera son activité au LIP6/Sorbonne Université – campus Pierre et Marie Curie (Jussieu), Paris

L’encadrement doctoral est réalisé par

- E. Encrenaz (LIP6) et M. Jan (CEA-List) : co-direction de thèse

- Q. Meunier (LIP6) et D. Couroussé (CEA-List) : co-encadrement

Compétences souhaitées (1 ou plusieurs des thématiques citées) : Architecture et micro-architecture de processeurs, Conception de circuits intégrés : langages VHDL/Verilog, méthode et outil de synthèse (par ex. Yosys), environnements de développement : git, C++ Méthodes formelles : bounded model-checking