An Automated Formal Process for Detecting Fault Injection Vulnerabilities in Binaries and Case Study on PRESENT -- Extended Version

Given-Wilson, Thomas Jafri, Nisrine Lanet, Jean-Louis Legay, Axel [UCL]

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.