Université de Rennes 1 Formal fault injection vulnerability detection in binaries : a software process and hardware validation Détection formelle de vulnérabilité crée par injection de faute au niveau binaire : un processus logiciel et une validation matérielle Injection de fautedétection de vulnérabilitémodel checkingméthodes formelles Fault InjectionVulnerability DetectionModel CheckingFormal Methods Vérification de modèles (informatique)Thèses et écrits académiques Méthodes formelles (informatique)Thèses et écrits académiques Systèmes de détection d'intrusion (informatique)Thèses et écrits académiques 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. 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. Electronic Thesis or DissertationText en application/pdf1 : 1659 Kohttps://ged.univ-rennes1.fr/nuxeo/site/esupversions/5992dcf2-8a54-4046-8cd3-a897e9cfdf14 Jafri Nisrine 1991-05-25 XX 236578081 nisrine.jafri@gmail.com 2019REN1S014 http://www.theses.fr/2019REN1S014 2019-03-25 Informatique Universite de Rennes 1thesis.degree.grantor_1 02778715X Doctorat non ouiLanetJean-Louisintervenant_1151767475LegayAxelintervenant_2183874129 MATHSTICecoleDoctorale_1 204770424 Universite Bretagne LoirepartenaireRecherche_1 191639044 INRIA-RENNES partenaireRecherche_2 133175863 TamispartenaireRecherche_3 ddc:004 LanetJean-LouisLegayAxelUniversite de Rennes 1Sciences et technologie, medecine, pharmacie, odontologie, droit, economie, gestion, philosophieMATHSTICÉcole doctorale Mathématiques et sciences et technologies de l'information et de la communication (Rennes)Universite Bretagne Loire Communaute des etablissements d enseignement superieur et de recherche (ComuE) INRIA-RENNES Tamis ASCII PDF 1698706