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

Description de l'offre : 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 lapos;analyse formelle des microarchitectures de processeurs. Cette recherche se concentre sur la formalisation et lapos;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 dapos;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 dapos;analyse actuelles, que ce soit par simulation ou par méthodes formelles, napos;ont pas la capacité dapos;adresser la complexité des systèmes actuels. Lapos;objectif est dapos;explorer des approches novatrices pour étendre lapos;analyse à des programmes plus vastes et à des microarchitectures de processeurs complexes. Le travail de thèse pourra sapos;appuyer sur les outils de simulation RTL comme Verilator ou QuestaSim, lapos;outil dapos;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 dapos;outils efficaces ayant le potentiel de rationaliser lapos;é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 lapos;assemblage de composants open source.

Profil du candidat : M.Sc. in Computer Science or Computer Engineering