Paper 2013/679

Formal verification of a software countermeasure against instruction skip attacks

Nicolas Moro, Karine Heydemann, Emmanuelle Encrenaz, and Bruno Robisson


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 consisting in an assembly instruction skip can be very useful for an attacker and has been obtained by using several fault injection means. To avoid this threat, 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 countermeasure schemes have also 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 almost all the instructions of the Thumb-2 instruction set and provide a formal verification for 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 article presented in the PROOFS 2013 workshop. The final article has been published in the Journal of Cryptographic Engineering (DOI 10.1007/s13389-014-0077-7), this preliminary version has been submitted to the IACR ePrint archive for self-archiving.

Available format(s)
Publication info
Published elsewhere. Minor revision. Journal of Cryptographic Engineering
microcontrollerfault attackinstruction skipcountermeasureformal verification
Contact author(s)
nicolas moro @ mines-stetienne fr
2014-02-24: revised
2013-10-24: received
See all versions
Short URL
Creative Commons Attribution


      author = {Nicolas Moro and Karine Heydemann and Emmanuelle Encrenaz and Bruno Robisson},
      title = {Formal verification of a software countermeasure against instruction skip attacks},
      howpublished = {Cryptology ePrint Archive, Paper 2013/679},
      year = {2013},
      doi = {10.1007/s13389-014-0077-7},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.