Formal verification of a software countermeasure against instruction skip attacks - Mines Saint-Étienne
Conference Papers Year : 2013

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.
No file

Dates and versions

emse-00869509 , version 1 (03-10-2013)

Identifiers

  • HAL Id : emse-00869509 , version 1

Cite

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⟩
261 View
0 Download

Share

More