An Automated Formal Process for Detecting Fault Injection Vulnerabilities in Binaries and Case Study on PRESENT -- Extended Version
Thomas Given-Wilson, Nisrine Jafri, Jean‐Louis Lanet, Axel Legay · HAL (Le Centre pour la Communication Scientifique Directe) · 2017
Recently fault injection has increasingly been used both to attack software applications, and to test system robustness. Detecting fault injection vulnerabilities has been approached with a variety of different but limited methods. This paper proposes a general process without these limitations that uses model checking to detect fault injection vulnerabilities in binaries. The efficacy of this process is demonstrated by detecting vulnerabilities in the PRESENT binary.