Formalisation et analyse de contre-mesures contre les attaques par injection de fautes dans des processeurs open-source

Rejoignez le CEA-List au sein de la division DSCIN pour une opportunité de doctorat dans le domaine de la sécurité matérielle et de l'analyse formelle des microarchitectures de processeurs. Cette recherche se concentre sur la formalisation et l'analyse des contre-mesures contre les attaques par injection de fautes sur des processeurs open-source. Nous visons à établir des garanties formelles pour la robustesse des processeurs face aux attaques par injection de fautes. Le défi scientifique de la thèse réside dans la création de méthodes et d'outils pouvant analyser efficacement la robustesse des systèmes embarqués sous injection de fautes. Vous travaillerez à la prise en compte conjointe du modèle RTL du processeur cible et du programme exécuté. Les techniques d'analyse actuelles, que ce soit par simulation ou par méthodes formelles, n'ont pas la capacité d'adresser la complexité des systèmes actuels. L'objectif est d'explorer des approches novatrices pour étendre l'analyse à des programmes plus vastes et à des microarchitectures de processeurs complexes. Le travail de thèse pourra s'appuyer sur les outils de simulation RTL comme Verilator ou QuestaSim, l'outil d'analyse formelle µARCHIFI développé au CEA-List, et des implémentations open-source de processeurs sécurisés comme le processeur RISC-V CV32E40S. Votre travail ouvrira la voie à la conception de techniques et d'outils efficaces ayant le potentiel de rationaliser l'évaluation des systèmes sécurisés, impactant des domaines tels que la certification (e.g., Critères Communs), et réduisant le temps de mise sur le marché lors de la phase de conception de systèmes sécurisés en permettant par exemple la conception de systèmes sûrs à partir de l'assemblage de composants open source.