Skip to Main content Skip to Navigation
Journal articles

Multi-Level Formal Analysis, A New Direction for Fault Injection Attack?

Laurent Sauvage 1, 2 Tarik Graba 1, 2 Thibault Porteboeuf 
1 SSH - Secure and Safe Hardware
LTCI - Laboratoire Traitement et Communication de l'Information
Abstract : Fault injection attack is an extremely pow- erful technique to extract secrets from an embedded system. Since their introduction, a large number of countermeasures have been proposed. Unfortunately, they suffer from two major drawbacks: a very high cost on system performance, and a security frequently ques- tioned. The first point can be explained by their design, based on techniques from Reliability domain, which re- sult in solutions protecting against fault models either highly improbable in a context of attack, or that do not permit secret extraction. At the opposite, the sec- ond point is due to the use of an incomplete attacker model for the security evaluation at design step. In this paper, we propose a new approach: multi-level formal verification, based on models encompassing the capabil- ities of the attacker, the susceptibility to faults of the hardware platform hosting the implementation, and the constraints imposed by the algorithm used for secret extraction. We first explain that the success of a fault injection attack depends solely on races between signals, which can be analyzed automatically. Then, we perform a multi-level evaluation on a hardware implementation of AES-128, which shows that the overhead of a coun- termeasure can be divided by eight while maintaining an almost identical level of security. Finally, we extend the model to electromagnetic injection.
Document type :
Journal articles
Complete list of metadata
Contributor : TelecomParis HAL Connect in order to contact the contributor
Submitted on : Friday, September 13, 2019 - 4:58:47 PM
Last modification on : Wednesday, November 3, 2021 - 6:18:46 AM


  • HAL Id : hal-02287457, version 1


Laurent Sauvage, Tarik Graba, Thibault Porteboeuf. Multi-Level Formal Analysis, A New Direction for Fault Injection Attack?. Journal of Cryptographic Engineering, 2016. ⟨hal-02287457⟩



Record views