Littérature scientifique sur le sujet « Attaques de microarchitecture »

Les systèmes embarqués numériques sont omniprésents dans notre environnement quotidien. Ces systèmes embarqués, par leur caractère nomade, sont particulièrement sensibles aux attaques dites par injection de fautes. Par exemple, un attaquant peut injecter une perturbation physique dans un circuit électronique pour compromettre les fonctionnalités de sécurité du système. Originellement utilisées pour compromettre des systèmes cryptographiques, ces attaques permettent aujourd'hui de cibler n'importe quel type de système. Ces attaques permettent notamment de compromettre l'exécution d'un programme. Dans ce manuscrit, nous introduisons une nouvelle propriété de sécurité pour protéger l'exécution des instructions dans la microarchitecture: l'intégrité d'exécution. À partir de cette propriété, nous décrivons le concept de SCI-FI, une contre-mesure qui assure la protection de l'intégralité du chemin d'instructions en assurant l'intégrité du code, du flot de contrôle et d'exécution. Pour cela, nous construisons un vecteur de bits que nous appelons pipeline state à partir de signaux de contrôle dans la microarchitecture. À partir du pipeline state, deux modules s'articulent pour assurer les propriétés de sécurité. Le premier module calcule une signature à partir du pipeline state assurant ainsi l'intégrité du code, du flot de contrôle et une partie de l'intégrité d'exécution. Le second module complète l'intégrité d'exécution dans la microarchitecture en utilisant un mécanisme de redondance. Nous proposons également le support et la sécurisation des branchements indirects et des interruptions, nécessaires pour la conception de systèmes embarqués. Nous réalisons deux imPlémentations de SCI-FI, l'une construite sur une primitive cryptographique assurant un niveau de sécurité maximal et l'autre plus légère construite sur une fonction CRC privilégiant les performances. Pour cela, nous intégrons SCI-FI dans un processeur RISC-V 32 bits et modifions la chaîne de compilation LLVM. Nous réalisons une analyse de sécurité des différents éléments qui composent SCI-FI dans chaque implémentation. Nous montrons ainsi que SCI-FI, même avec l'implémentation privilégiant les performances, est robuste face à un attaquant disposant de moyens d'injection de fautes à l'état de l'art. Enfin, nous évaluons les performances de nos implémentations par une synthèse dans un flot de conception ASIC et par l'exécution en simulation de la suite de test Embench-IOT. Nous montrons ainsi que SCI-FI a des performances équivalentes aux contre-mesures de l'état de l'art tout en assurant une propriété de sécurité supplémentaire, l'intégrité d'exécution
Embedded systems are ubiquitous in our everyday life. Those embedded systems, by their nomadic nature, are particularly sensitive to the so-called fault injection attacks. For example, an attacker might inject a physical perturbation in an integrated circuit to compromise the security features of the system. Originally used to compromise cryptographic systems, those attacks can now target any kind of system. Notably, those attacks enable to compromise the execution of a program. In this manuscript, we introduce a new security property to protect the execution of instructions in the microarchitecture: execution integrity. From this property, we describe the concept of SCI-FI, a counter-measure that ensures the protection of the whole instruction path thanks to code, control-flow and execution integrity properties. We build SCI-FI around a bit vector that we call pipeline state and that is composed of microarchitecture control signals. Two modules interact around the pipeline state to ensure the security properties. The first module computes a signature from the pipeline state to ensure code and control-flow integrity and partially execution integrity. The second module completes the execution integrity support in the microarchitecture thanks to a redundancy mechanism. We also propose a solution for indirect branches and interrupts that are required to design embedded systems. We implement two versions of SCI-FI, one built around a cryptographic primitive which provides the best security level and another lighter one built around a CRC to maximize the performances. We integrate SCI-FI into a 32 bits RISC-V processor, and we modify the LLVM compiler. We analyze the security provided by our two implementations and we show that SCI-FI, even with the lightweight implementation, is robust against state-of-the-art attacker. Finally, we evaluate the performances of our implementations through an ASIC synthesis and through the execution of the benchmark suite Embench-IoT. We show that SCI-FI has comparable performances to state-of-the-art counter-measures while ensuring a new security property: execution integrity

Le désassemblage par canaux auxiliaires (SCBD) est une famille d’attaques par canaux auxiliaires (SCA) dont le but est de retrouver de l’information à propos du code exécuté par un processeur via l’observation de canaux physiques comme la consommation électrique ou le rayonnement électromagnétique. Alors que les SCA classiques ciblent majoritairement des clés cryptographiques, le SCBD vise à récupérer du code assembleur difficile à extraire par d’autres moyens. Un exemple typique est le bootloader, qui est le premier programme exécuté au démarrage d’un dispositif électronique. La découverte d’une vulnérabilité dans un bootloader peut mener à la compromission totale du dispositif qui l’exécute. Le SCBD a été montré faisable sur de petits microcontrôleurs possédant une microarchitecture simple et un jeu d’instructions réduit. Cependant, l’essor des System-on-Chips (SoCs) complexes dans les smartphones, l’automobile ou l’avionique, rend nécessaire l’évaluation du risque posé par le SCBD sur ces plateformes. Par conséquent, dans cette thèse, nous nous intéressons à la faisabilité du SCBD sur les SoCs. Dans un premier temps, nous investiguons l’impact de la complexité microarchitecturale des SoCs sur les techniques de SCBD existantes. Nous montrons que ces dernières ont des difficultés à fournir des prédictions fiables sur des phénomènes de petite échelle, laissant une grande quantité d’incertitude à l’attaquant. Néanmoins, les phénomènes manipulant plus de ressources, comme les accès à la mémoire DRAM, peuvent être plus facilement distingués. Cette observation nous conduit à proposer trois nouvelles attaques hybrides, à l’intersection entre les attaques physiques et les attaques de microarchitecture. Dans un second temps, nous traitons l’incertitude inhérente au SCBD sur SoC en développant un outil générique et flexible. Cet outil permet de réaliser des attaques à base de modèles probabilistes (SASCA). Il se base sur un algorithme de propagation de croyances (BP) qui opère sur un modèle de graphe appelé factor graph. Cet outil nous permet d’opérer à des attaques sur les fonctions de hachage SHA-2 et SHA-3, ce qui, dans certains cas d’usage, mène à un moyen détourné de réaliser du SCBD. Enfin, nous introduisons un modèle probabiliste de désassemblage par canaux auxiliaires (SASCBD), qui permet d’agréger les prédictions imparfaites issues d’un SCBD classique. En plus d’exploiter efficacement la structure du jeu d’instruction, ce modèle permet d’incorporer de la connaissance bien plus riche, comme par exemple les propriétés du code assembleur à l’échelle d’un programme entier
Side-Channel Based Disassembly (SCBD) is a category of Side-Channel Analysis (SCA) that aims at recovering information on the code executed by a processor through the observation of physical side-channels such as power consumption or electromagnetic radiations. While traditional SCA often targets cryptographic keys, SCBD focuses on retrieving assembly code that can hardly be extracted via other means. A typical example is bootloader code, which is the first program executed by a processor at a device startup. Finding vulnerabilities in bootloader code could allow an attacker to compromise the entire device. SCBD has been shown feasible on microcontrollers with simple microachitectural complexity and small Instruction Sets Architecture (ISA). However, as System-on-Chips (SoCs) become ubiquitous in various systems such as smartphones, automotive or avionics, the threat posed by SCBD on these devices needs to be evaluated. In this thesis, we investigate the feasibility of SCBD on SoCs. We first study the impact of the microachitectural complexity of SoC’s processors on existing SCBD techniques. This brings us to the observation that the latter struggle to provide accurate predictions on small-scale phenomena, leaving a high amount of uncertainty from an attacker’s perspective. However, coarse-grained events, such as accesses to the main memory, can be accurately distinguished. We exploit this property to mount three new hybrid attacks, at the intersection of physical and microarchitectural attack. In the second part of this thesis, we deal with the uncertainty inherent to SCBD on SoCs by developing a generic and flexible Soft-Analytical Side-Channel Attack (SASCA) framework. This tool leverages factor graphs and the Belief Propagation (BP) algorithm to efficiently handle probabilistic information. This framework allows us to derive an attack on hash functions from the SHA-2 and SHA-3 families, which could lead to a twisted way to perform SCBD. Finally, we introduce the concept of Soft-Analytical Side-Channel Based Disassembly (SASCBD), which leverages the aforementioned framework to efficiently aggregate imperfect predictions from SCBD. This new approach efficiently exploits the structure of ISA and supports the addition of rich knowledge, such as behaviors at the scale of full programs

Les attaques par canaux auxiliaire sont redoutables face aux implémentations cryptographiques. Malgré les attaques passées, et la prolifération d'outils de vérification, ces attaques affectent encore de nombreuses implémentations. Dans ce manuscrit, nous abordons deux aspects de cette problématique, centrés autour de l'attaque et de la défense. Nous avons dévoilé plusieurs attaques par canaux auxiliaires microarchitecturaux sur des implémentations de protocoles PAKE. En particulier, nous avons exposé des attaques sur Dragonfly, utilisé dans la nouvelle norme Wi-Fi WPA3, et SRP, déployé dans de nombreux logiciel tels que ProtonMail ou Apple HomeKit. Nous avons également exploré le manque d'utilisation par les développeurs d'outil permettant de détecter de telles attaques. Nous avons questionné des personnes impliqués dans différents projets cryptographiques afin d'identifier l'origine de ce manque. De leur réponses, nous avons émis des recommandations. Enfin, dans l'optique de mettre fin à la spirale d'attaques-correction sur les implémentations de Dragonfly, nous avons fournis une implémentation formellement vérifiée de la couche cryptographique du protocole, dont l'exécution est indépendante des secrets
Side-channel attacks are daunting for cryptographic implementations. Despite past attacks, and the proliferation of verification tools, these attacks still affect many implementations. In this manuscript, we address two aspects of this problem, centered around attack and defense. We unveil several microarchitectural side-channel attacks on implementations of PAKE protocols. In particular, we exposed attacks on Dragonfly, used in the new Wi-Fi standard WPA3, and SRP, deployed in many software such as ProtonMail or Apple HomeKit. We also explored the lack of use by developers of tools to detect such attacks. We questioned developers from various cryptographic projects to identify the origin of this lack. From their answers, we issued recommendations. Finally, in order to stop the spiral of attack-patch on Dragonfly implementations, we provide a formally verified implementation of the cryptographic layer of the protocol, whose execution is secret-independent

Les attaques par canaux cachés basées sur les accès aux mémoires caches constituent une sous-catégorie représentant un puissant arsenal permettant de remettre en cause la sécurité d’algorithmes cryptographiques en ciblant leurs implémentations. Malgré de nombreux efforts, les techniques de protection contre ces attaques ne sont pas encore assez matures. Ceci est principalement dû au fait que la plupart des techniques ne protègent généralement pas contre tous les scénarii d’attaques. De plus, ces solutions peuvent impacter fortement les performances des systèmes. Cette thèse propose des arguments en faveur du renforcement de la sécurité et de la confidentialité dans les systèmes informatiques modernes tout en conservant leurs performances. Pour cela, la thèse développe une protection basée sur les besoins, qui permettent au système d’exploitation d’appliquer uniquement des mesures de protection après la détection des attaques. Ainsi, la détection peut servir de première ligne de défense. Cependant, pour que la stratégie de protection basée sur la détection soit efficace, il faut que cette dernière soit fiable, n’impacte que faiblement les performances et couvre un large spectre d’attaques avant que ces dernières atteignent leur but. Dans cette optique, cette thèse propose un cadre complet pour la protection basée sur la détection d’un ensemble d’attaques exploitant les mémoires caches lors de l’exécution sous des conditions de charge variables du système. De plus, la thèse propose de coupler l’utilisation du principe de détection avec un mécanisme de protection intégré au système d’exploitation Linux. Bien que le mécanisme de protection proposé soit appliqué à Linux, la solution est extensible à d’autres systèmes d’exploitation. Cette thèse démontre que la sécurité et la confidentialité doivent être pris en compte au niveau système et que les solutions de protection doivent adopter une approche holistique
Access-driven cache-based sidechannel attacks, a sub-category of SCAs, are strong cryptanalysis techniques that break cryptographic algorithms by targeting their implementations. Despite valiant efforts, mitigation techniques against such attacks are not very effective. This is mainly because most mitigation techniques usually protect against any given specific vulnerability and do not take a system-wide approach. Moreover, these solutions either completely remove or greatly reduce the prevailing performance benefits in computing systems that are hard earned over many decades. This thesis presents arguments in favor of enhancing security and privacy in modern computing architectures while retaining the performance benefits. The thesis argues in favor of a need-based protection, which would allow the operating system to apply mitigation only after successful detection of CSCAs. Thus, detection can serve as a first line of defense against such attacks. However, for detection-based protection strategy to be effective, detection needs to be highly accurate, should incur minimum system overhead at run-time, should cover a large set of attacks and should be capable of early stage detection, i.e., before the attack completes. This thesis proposes a complete framework for detection-based protection. At first, the thesis presents a highly accurate, fast and lightweight detection framework to detect a large set of Cache-based SCAs at run-time under variable system load conditions. In the follow up, the thesis demonstrates the use of this detection framework through the proposition of an OS-level run-time detection-based mitigation mechanism for Linux generalpurpose distribution. Though the proposed mitigation mechanism is proposed for Linux general distributions, which is widely used in commodity hardware, the solution is scalable to other operating systems. We provide extensive experiments to validate the proposed detection framework and mitigation mechanism. This thesis demonstrates that security and privacy are system-wide concerns and the mitigation solutions must take a holistic approach

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. Alors que la sécurité de ces systèmes est traditionnellement évaluée au niveau du logiciel ou du matériel, des recherches récentes soulignent la nécessité de prendre en compte les deux niveaux et d'analyser la microarchitecture du processeur pour comprendre pleinement les conséquences des attaques par injection fautes. Dans ce contexte, cette thèse vise à élaborer une méthodologie d'analyse exhaustive et automatisée, prenant en compte à la fois les descriptions logicielles et matérielles du système, afin d'avoir une évaluation fine des conséquences des fautes sur le logiciel ou de fournir des garanties formelles sur la sécurité du système. À cette fin, nous proposons µArchiFI, une méthodologie formelle de modélisation et de vérification permettant d'évaluer les effets des fautes sur les systèmes combinés matériel/logiciel. Contrairement aux méthodologies existantes, µArchiFI est exhaustif et permet l'identification automatique des vulnérabilités difficiles à détecter, ainsi que la preuve de robustesse des systèmes contre les attaques par injection de fautes. Implémenté à partir de l'infrastructure de compilation Yosys, notre approche génère une modélisation du système adaptée aux techniques de vérification formelle telles que le model checking borné. Nous validons notre méthodologie sur les processeurs RISC-V en identifiant automatiquement les attaques connues exploitant les mécanismes microarchitecturaux et en découvrant des effets de fautes jusqu'alors inconnus que les techniques de simulation classique pourraient manquer. De plus, nous évaluons formellement la sécurité d'une contre-mesure conjointe logiciel et matériel MAFIA, tâche qui ne n'aurait pas été possible en ne travaillant uniquement qu'à l'un de ces niveaux. Pour améliorer les performances de notre approche et résoudre le problème de l'explosion de l'espace d'état, l'un des défis majeurs des techniques exhaustives, nous décomposons la co-vérification matériel/logiciel en étapes plus faciles à résoudre. Cette décomposition s'appuie sur une évaluation préliminaire des contre-mesures matérielles potentielles existantes. Par conséquent, nous démontrons que des problèmes auparavant insolubles, tels que l'analyse de la robustesse de l'élément sécurisé OpenTitan exécutant un processus de démarrage sécurisé, peuvent désormais être résolus grâce à notre méthodologie. Notre approche a également identifié des vulnérabilités dans le banc de registres, pour lesquelles nous avons fourni et prouvé un correctif de sécurité qui a ensuite été intégré dans le projet OpenTitan
Fault injection attacks are a serious threat to system security, enabling attackers to bypass protection mechanisms or access sensitive information. While the security of these systems is traditionally assessed at the software or hardware level, recent research highlights the need to consider both and analyze the processor microarchitecture to fully understand the consequences of fault attacks. In this context, this thesis introduces an exhaustive and automated analysis technique, comprising both software and hardware system descriptions, to better understand the final consequences of hardware-level faults on software and provide formal guarantees of software security. For this purpose, we propose µArchiFI, a formal modeling and verification methodology to evaluate fault effects on combined hardware/software systems. Built on top of the Yosys compiler, this tool generates a system model suitable for formal verification techniques such as bounded model checking. Unlike previous methodologies, µArchiFI is exhaustive and allows for automatic identification of corner-case vulnerabilities, as well as proving system robustness against fault attacks. We validate our methodology on RISC-V processors by automatically identifying known fault attacks exploiting microarchitectural mechanisms and by discovering previously unreported fault effects that existing simulation-based techniques might miss. Additionally, we formally evaluate the security of the combined countermeasure MAFIA, something that would not be possible through hardware or software verification alone. To improve performance and address the state space explosion problem---one of the most significant challenges of exhaustive techniques---we decompose hardware/software co-verification into more manageable steps. This decomposition leverages a preliminary evaluation of potential hardware-level countermeasures. Consequently, we demonstrate that previously intractable problems, such as analyzing the robustness of the OpenTitan secure element running a secure boot process, can now be solved using our methodology. Our approach also identified vulnerabilities in the register file, for which we provided and proved a security fix before integrating it into the OpenTitan project