Inférence de modèle d'attaquant pour la caractérisation des vulnérabilités aux fautes

Contexte et Problématique Les systèmes embarqués sont vulnérables aux attaques par injection de fautes, où un attaquant perturbe physiquement le matériel pour altérer l'exécution d'un programme et créer des failles de sécurité. Actuellement, la vérification automatique de la résistance d'un code repose sur l'utilisation d'un modèle d'attaquant (définition des capacités de l'attaquant : nombre de fautes, localisation, etc.). Le problème majeur est que ce modèle est choisi a priori comme une hypothèse. Si le modèle est légèrement erroné, les résultats de l'analyse ne sont plus valables. De plus, les outils actuels fournissent souvent un seul exemple d'attaque (témoin), sans donner de vision globale des capacités d'attaque rendant le système vulnérable. Objectif de la Thèse L'objectif est d'inverser le paradigme : au lieu de vérifier si un code est vulnérable à un modèle d'attaquant fixé, la thèse vise à synthétiser et caractériser les modèles d'attaquants face auxquels un code est vulnérable ou résistant. Il s'agit de passer de la caractérisation de l'attaque à la caractérisation de l'attaquant, en cherchant notamment : Le modèle d'attaquant minimal capable de réussir une attaque. Le modèle d'attaquant maximal contre lequel le code reste protégé. Approche Scientifique Le travail s'appuiera sur le raisonnement abductif (inférence de causes/préconditions) appliqué à l'exécution symbolique au niveau binaire. L'idée est d'étendre des techniques d'abduction déjà testées sur les entrées de programmes pour les adapter à la synthèse de capacités d'attaque. Les principaux défis scientifiques seront : Formalisation : Définir un standard pour les modèles d'attaquants et établir des relations entre eux (treillis d'attaquants). Langage d'inférence : Concevoir des grammaires adaptées pour générer des modèles d'attaques (ex: contraintes sur les bits, fréquence et localisation des injections). Complexité : Optimiser les algorithmes pour les théories des bitvecteurs et des tableaux afin de garantir le passage à l'échelle sur des codes réels. Moyens et Retombées Le doctorant intégrera ses travaux dans BINSEC, le moteur d'exécution symbolique du CEA List. Les expérimentations porteront sur des benchmarks réalistes et des codes protégés (bootloader Wookey, micro-kernel Sentry, benchmark FISSC). Les retombées sont multiples : Évaluation : Aide précieuse pour les laboratoires de certification (CESTIs) et les évaluateurs sécurité. Industrie : Applications pour les concepteurs de composants sécurisés (Apple, ARM, ST, Thalès). Sûreté : Extension possible à l'analyse des fautes non-ciblées (ex: rayonnements cosmiques dans le spatial). Encadrement et Institution La thèse se déroulera au CEA List (équipe SABR), sous la direction de Matthieu Lemerre, Sébastien Bardin et Yanis Sellami, experts en méthodes formelles et analyse binaire. École doctorale : Sciences et Technologies de l'Information et de la Communication Direction : Matthieu LEMERRE Financement : Financement du CEA - CTBU (Contrat de thèse sur budget unité)