Multi-level formal verification: A new approach against fault injection attack

Fault injection attack is an extremely powerful 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 questioned. The first point can be explained by their design, based on techniques from reliability domain, which result 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 second 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 capabilities 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 countermeasure can be divided by eight while maintaining an almost identical level of security. Finally, we extend the model to electromagnetic injection.