Détection formelle de vulnérabilité créée par injection de faute au niveau binaire : un processus logiciel et une validation matérielle

Fault injection is a well known method to test the robustness and security vulnerabilities of systems. Detecting fault injection vulnerabilities has been approached with a variety of different but limited methods. Software-based and hardware-based approaches have both been used to detect fault injection vulnerabilities. Software-based approaches can provide broad and rapid coverage, but may not correlate with genuine hardware vulnerabilities. Hardware-based approaches are indisputable in their results, but rely upon expensive expert knowledge, manual testing, and can not confirm what fault model represent the created effect. First, this thesis focuses on the software-based approach and proposes a general process that uses model checking to detect fault injection vulnerabilities in binaries. The efficacy and scalability of this process is demonstrated by detecting vulnerabilities in different cryptographic real-world implementations. Then, this thesis bridges software-based and hardware-based fault injection vulnerability detection by contrasting results of the two approaches. This demonstrates that: not all software-based vulnerabilities can be reproduced in hardware; prior conjectures on the fault model for electromagnetic pulse attacks may not be accurate; and that there is a relationship between software-based and hardware-based approaches. Further, combining both software-based and hardware-based approaches can yield a vastly more accurate and efficient approach to detect genuine fault injection vulnerabilities.L'injection de faute est une méthode bien connue pour évaluer la robustesse et détecter les vulnérabilités des systèmes. La détection des vulnérabilités créées par injection de fautes a été approchée par différentes méthodes. Dans la littérature deux approches existent: les approches logicielles et les approches matérielles. Les approches logicielles peuvent fournir une large et rapide couverture, mais ne garantissent pas la présence de vulnérabilité dans le système. Les approches matérielles sont incontestables dans leurs résultats, mais nécessitent l’utilisation de matériaux assez coûteux et un savoir-faire approfondi, qui ne permet tout de même pas dans la majorité des cas de confirmer le modèle de faute représentant l'effet créé. Dans un premier lieu, cette thèse se concentre sur l'approche logicielle et propose une approche automatisée qui emploie les techniques de la vérification formelle pour détecter des vulnérabilités créées par injection de faute au niveau binaire. L'efficacité de cette approche est montrée en l'appliquant à des algorithmes de cryptographie implémentés dans les systèmes embarqués. Dans un second lieu, cette thèse établit un rapprochement entre les deux approches logicielles et matérielles sur la détection de vulnérabilité d'injection de faute en comparant les résultats des expériences des deux approches. Ce rapprochement des deux approches démontre que: toutes les vulnérabilités détectées par l'approche logicielle ne peuvent pas être reproduites dans le matériel; les conjectures antérieures sur le modèle de faute par des attaques d'impulsion électromagnétique ne sont pas précises ; et qu’il y a un lien entre les résultats de l’approche logicielle et l'approche matérielle. De plus, la combinaison des deux approches peut rapporter une approche plus précise et plus efficace pour détecter les vulnérabilités qui peuvent être créées par injection de faute