Efficient Design and Evaluation of Countermeasures against Fault Attacks Using Formal Verification

摘要: This paper presents a formal verification framework and tool that evaluates the robustness of software countermeasures against fault-injection attacks. By modeling reference assembly code its protected variant as automata, can generate set equations for an SMT solver, solutions which represent possible attack paths. Using we developed, evaluated state-of-the-art fault injection Based on insights gathered from this evaluation, analyze any remaining weaknesses propose applications these are more robust.