Formal fault injection vulnerability detection in binaries: a software process and hardware validation

From bibtex.

Abstract

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 cannot confirm what fault model represents 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.