Detecting fault injection vulnerabilities in binaries with symbolic execution

We propose a framework based on symbolic execution to identify automatically and consistently the effects of fault injection on embedded software at assembly level, for C (compiled to assembly) and Java (compiled to bytecode) binaries, for faults affecting the control flow or the values in memory. We implement our framework on top of the angr symbolic execution engine, with built-in support for various fault models (Stuck-at, Hamming weight, Unconstrained). We assess the performances of our framework on open source programs considering single and double fault injections, showing that it identifies all possible fault injections in a fraction of the time required by manual review.