Détection formelle de vulnérabilité créée par injection de faute au niveau binaire : un processus logiciel et une validation matérielle
Nisrine Jafri · HAL (Le Centre pour la Communication Scientifique Directe) · 2019
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.Softwarebased 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.