This paper presents a formal verification framework and tool that evaluates the robustness of software countermeasures against faultinjection attacks. By modeling reference assembly code and its protected variant as automata, the framework can generate a set of equations for an SMT solver, the solutions of which represent possible attack paths. Using the tool we developed, we evaluated the robustness of state-of-theart countermeasures against fault injection attacks. Based on insights gathered from this evaluation, we analyze any remaining weaknesses and propose applications of these countermeasures that are more robust.
CITATION STYLE
Goubet, L., Heydemann, K., Encrenaz, E., & De Keulenaer, R. (2016). Efficient design and evaluation of countermeasures against fault attacks using formal verification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9514, pp. 177–192). Springer Verlag. https://doi.org/10.1007/978-3-319-31271-2_11
Mendeley helps you to discover research relevant for your work.