Paper 2013/679
Formal verification of a software countermeasure against instruction skip attacks
Karine Heydemann and Nicolas Moro and Emmanuelle Encrenaz and Bruno Robisson
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.
Note: Extended version of the paper presented at PROOFS 2013 (Santa Barbara)
Metadata
- Available format(s)
- Category
- Implementation
- Publication info
- Preprint. MINOR revision.
- Keywords
- microcontrollerfault attackinstruction skipcountermeasureformal proof
- Contact author(s)
- nicolas moro @ mines-stetienne fr
- History
- 2014-02-24: revised
- 2013-10-24: received
- See all versions
- Short URL
- https://ia.cr/2013/679
- License
-
CC BY