PR34 INCYBER Injection de fautes dans la microarchitecture des processeurs et analyses formelles de
Les attaques par injection de fautes représentent une menace majeure pour la sécurité des systèmes, car elles permettent aux attaquants de déjouer des mécanismes de protection ou d’accéder à des informations sensibles, à la fois dans des implémentations matérielles et dans des implémentations logicielles. Concernant la sécurité du logiciel et des processeurs, des recherches récentes soulignent la nécessité de prendre en compte à la fois les niveaux matériel et logiciel, et en particulier de tenir compte de l’effet des injections de fautes dans la microarchitecture des processeurs pour comprendre pleinement les conséquences des attaques par injection fautes. Dans ce contexte, notre équipe élabore des techniques d’analyses exhaustives et automatisées, capables de prendre en compte à la fois les descriptions logicielles et matérielles du système, afin de fournir des garanties formelles sur sa sécurité.
Dans cette présentation, nous introduirons les attaques par injection de fautes, puis nous montrerons la nécessité de tenir compte de l’effet des fautes dans la microarchitecture des processeurs, question de recherche ignorée encore récemment. Enfin, la présentation discutera des différentes approches possibles, et des résultats récents de l’équipe pour permettre des analyses de robustesse exhaustives et automatisées, à l’aide de techniques formelles de vérification.
Allez à la source
