Skip to Main content Skip to Navigation
Conference papers

Formal verification of a software countermeasure against instruction skip attacks

Abstract : Fault attacks against embedded circuits enabled to define many new attack paths against secure circuits. Every attack path relies on a specific fault model which defines the type of faults that the attacker can perform. On embedded processors, a fault model in which an attacker is able to skip an assembly instruction is practical and has been obtained by using several fault injection means. To handle this issue, some countermeasure schemes which rely on temporal redundancy have been proposed. Nevertheless, double fault injection in a long enough time interval is practical and can bypass those countermeasure schemes. Some fine-grained other countermeasure schemes have been proposed for specific instructions. However, to the best of our knowledge, no approach that enables to secure a generic assembly program in order to make it fault-tolerant to instruction skip attacks has been formally proven yet. In this paper, we provide a fault-tolerant replacement sequence for every instruction of the whole Thumb2 instruction set and provide a formal proof of this fault tolerance. This simple transformation enables to add a reasonably good security level to an embedded program and makes practical fault injection attacks much harder to achieve.
Complete list of metadata
Contributor : Nicolas Moro Connect in order to contact the contributor
Submitted on : Thursday, October 3, 2013 - 2:57:47 PM
Last modification on : Sunday, June 26, 2022 - 9:38:26 AM


  • HAL Id : emse-00869509, version 1


Karine Heydemann, Nicolas Moro, Emmanuelle Encrenaz, Bruno Robisson. Formal verification of a software countermeasure against instruction skip attacks. PROOFS 2013, Aug 2013, Santa-Barbara, United States. ⟨emse-00869509⟩



Record views