Les circuits cryptographiques, parce qu'ils contiennent des informations confidentielles, font l'objet de manipulations frauduleuses, appelées communément attaques, de la part de personnes mal intentionnées. Plusieurs attaques ont été répertoriées et analysées. L'une des plus efficaces actuellement, appelée cryptanalyse DFA (Differential Fault Analysis), exploite la présence de fautes, injectées volontairement par l’attaquant par exemple à l’aide d’un laser, dans les calculs. Cependant, les modèles de fautes utilisés dans ces attaques sont parfois très restrictifs et conditionnent leur efficacité. Il est donc important de bien connaître quel modèle de faute est pertinent ou réalisable en fonction du circuit cible et du moyen d'injection (dans notre cas le laser). Un première étude portant sur le type de fautes (Bit-set, Bit-reset ou Bit-flip) injectées sur des points mémoires SRAM a mis en évidence la forte dépendance des fautes injectées vis à vis des données manipulées et la quasi inexistence de fautes de type Bit-flip. Ce dernier résultat favorise grandement les attaques de type Safe Error et engendre donc un réel problème de sécurité. La mise en évidence de tels résultats a été possible grâce à des cartographies de sensibilité au laser réalisées sur une cellule SRAM isolée puis sur la mémoire RAM d'un micro-contrôleur 8 bits. Pour confirmer ces résultats expérimentaux, des simulations SPICE d'injection de fautes laser ont été réalisées à partir d'un modèle développé dans l’équipe. Ce modèle prend en compte la topologie de la cible. Des tests ont ensuite été réalisés sur un circuit ASIC implémentant l'algorithme AES. L'analyse des fautes a montré la présence des trois types de fautes mais aussi un faible taux d'injection. En revanche, le taux de répétabilité des fautes était particulièrement élevé. Cela nous a permis d'améliorer une attaque existante et d'obtenir au final une attaque plus efficace que les attaques classiques, nécessitant moins de chiffrements fautés et une analyse des résultats réduite pour retrouver la clef secrète. Enfin, une évaluation des contre-mesures embarquées dans ce circuit a montré leurs inefficacités vis à vis des attaques en fautes par laser. Des pistes d'amélioration ont ensuite été proposées. / Cryptographic circuits, because they contain confidential informations, are subject to fraud from malicious users, commonly known as attacks. Several attacks have been published and analysed. One of the most effective attack, called Differential Fault Analysis (DFA), uses some fault, voluntary injected by the attacker during the computations, for example with a laser. However, fault models used by these attacks can be restrictive and determine the effectiveness of the attack. Thus, it is important to know which fault model is useful or feasible according to the targeted device or injection means (in our case the laser).A first study about the injected fault types (Bit-set, Bit-reset or Bit-flip) on SRAM memory cells highlighted the strong data dependency of the injected faults and the irrelevance of the Bit-flip fault type. This last result allows to mount Safe Error attacks and creates a real security issue. These results were obtain thanks to sensitivity laser map performed on an isolated SRAM cell and on an 8-bits micro-controller RAM memory. To confirm these experimental results, SPICE simulations have been made with a model developed in the department. This model takes into account the topology of the target.Tests were then carried out on an ASIC implementing the AES algorithm. The fault analysis showed the presence of the three types of faults but also a low injection rates. In contrast, the error repeatability was particularly high. This allowed us to simplify an existing attack and to obtain an attack more effective than conventional attacks, requiring fewer faulted cipher text and reducing the complexity of the analysis to find the secret key. Finally, an assessment of the countermeasure of this circuit showed their ineffectiveness with respect to fault laser attacks. Areas for improvement were then proposed.

Les circuits cryptographiques, parce qu'ils contiennent des informations confidentielles, font l'objet de manipulations frauduleuses, appelées communément attaques, de la part de personnes mal intentionnées. Plusieurs attaques ont été répertoriées et analysées. L'une des plus efficaces actuellement, appelée cryptanalyse DFA (Differential Fault Analysis), exploite la présence de fautes, injectées volontairement par l'attaquant par exemple à l'aide d'un laser, dans les calculs. Cependant, les modèles de fautes utilisés dans ces attaques sont parfois très restrictifs et conditionnent leur efficacité. Il est donc important de bien connaître quel modèle de faute est pertinent ou réalisable en fonction du circuit cible et du moyen d'injection (dans notre cas le laser). Un première étude portant sur le type de fautes (Bit-set, Bit-reset ou Bit-flip) injectées sur des points mémoires SRAM a mis en évidence la forte dépendance des fautes injectées vis à vis des données manipulées et la quasi inexistence de fautes de type Bit-flip. Ce dernier résultat favorise grandement les attaques de type Safe Error et engendre donc un réel problème de sécurité. La mise en évidence de tels résultats a été possible grâce à des cartographies de sensibilité au laser réalisées sur une cellule SRAM isolée puis sur la mémoire RAM d'un micro-contrôleur 8 bits. Pour confirmer ces résultats expérimentaux, des simulations SPICE d'injection de fautes laser ont été réalisées à partir d'un modèle développé dans l'équipe. Ce modèle prend en compte la topologie de la cible. Des tests ont ensuite été réalisés sur un circuit ASIC implémentant l'algorithme AES. L'analyse des fautes a montré la présence des trois types de fautes mais aussi un faible taux d'injection. En revanche, le taux de répétabilité des fautes était particulièrement élevé. Cela nous a permis d'améliorer une attaque existante et d'obtenir au final une attaque plus efficace que les attaques classiques, nécessitant moins de chiffrements fautés et une analyse des résultats réduite pour retrouver la clef secrète. Enfin, une évaluation des contre-mesures embarquées dans ce circuit a montré leurs inefficacités vis à vis des attaques en fautes par laser. Des pistes d'amélioration ont ensuite été proposées.

Les implémentations cryptographiques sont vulnérables aux attaques physiques, et ont donc besoin d'en être protégées. Bien sûr, des protections défectueuses sont inutiles. L'utilisation des méthodes formelles permet de développer des systèmes tout en garantissant leur conformité à des spécifications données. Le premier objectif de ma thèse, et son aspect novateur, est de montrer que les méthodes formelles peuvent être utilisées pour prouver non seulement les principes des contre-mesures dans le cadre d'un modèle, mais aussi leurs implémentations, étant donné que c'est là que les vulnérabilités physiques sont exploitées. Mon second objectif est la preuve et l'automatisation des techniques de protection elles-même, car l'écriture manuelle de code est sujette à de nombreuses erreurs, particulièrement lorsqu'il s'agit de code de sécurité. / Implementations of cryptosystems are vulnerable to physical attacks, and thus need to be protected against them. Of course, malfunctioning protections are useless. Formal methods help to develop systems while assessing their conformity to a rigorous specification. The first goal of my thesis, and its innovative aspect, is to show that formal methods can be used to prove not only the principle of the countermeasures according to a model, but also their implementations, as it is where the physical vulnerabilities are exploited. My second goal is the proof and the automation of the protection techniques themselves, because handwritten security code is error-prone.

Au cours de cette thèse, nous nous sommes concentrés sur la sécurité des appareils mobiles. Pour cela, nous avons exploré les attaques physiques par perturbation (injection de fautes) ainsi que par observation, toutes deux basées sur les émissions électromagnétiques. Nous avons sélectionné deux types de cibles représentant deux catégories d'appareils mobiles. D'une part les microcontrôleurs qui équipent les appareils de type IoT. Et d'autre part les System-on-Chip (SoC) que l'on retrouve sur les smartphones. Nous nous sommes concentrés sur les puces conçue par ARM. Au travers d'attaques physiques nous avons voulu montrer qu'il était possible d'affecter la microarchitecture sur laquelle repose tout le fonctionnement de ces systèmes. Toutes les protections pouvant être mises en place par la suite au niveau logiciel, sont basées sur la microarchitecture et deviennent donc inopérantes lorsque l'on s'attaque à celle-ci. Pour les appareils de type IoT, nous avons mis en évidence la possibilité d'obtenir des informations ou un contrôle total de l'appareil à l'aide d'une injection de faute. Les injections de fautes sont dans ce cas les déclencheurs d'attaques logicielles et permettent d'outrepasser des protections logicielles. Pour les appareils de type smartphone, nous avons dans un premier temps été capable d'extraire des informations contenue à l'intérieur d'un SoC, à l'aide d'une écoute électromagnétique et de la caractérisation du comportement de celui-ci. Dans un deuxième temps, nous avons pu montrer qu'en cas de faute des comportements aléatoire peuvent se produire, tout en caractérisant ces comportements. Démontrant ainsi que sur des systèmes plus complexes, il est tout de même possible d'avoir recours à des attaques physiques. Enfin nous avons proposé des pistes d'améliorations en lien avec nos différentes constatations au cours de ces travaux. / During this thesis, we focused on the security of mobile devices. To do this, we explored physical attacks by perturbation (fault injections) as well as by observation, both based on electromagnetic emissions. We selected two types of targets representing two categories of mobile devices. On the one hand, the microcontrollers that equip IoT devices. And on the other hand the System-on-Chip (SoC) that can be found on smartphones. We focused on the chips designed by ARM. Through physical attacks we wanted to show that it was possible to affect the microarchitecture on which the entire functioning of these systems is based. All the protections that can be implemented later at the software level are based on the microarchitecture and therefore become ineffective when it is attacked. For IoT devices, we have highlighted the possibility of obtaining information or total control of the device by means of a fault injection. In this case, fault injections are used as software attack triggers. They also allow software protection to be bypassed. For smartphone devices, we were initially able to extract information contained within a SoC, using electromagnetic listening and characterization of its behavior. In a second step, we were able to show that in the event of a fault, random behaviours can occur, we characterized and proposed explanations for these behaviours. Demonstrating and on systems more advanced than IoT, it is still possible to use physical attacks. Finally, we proposed possible improvements in relation to our various findings during this work.