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.
Formal methods and formal verification tools have been used for cryptographic protocols' verification of to check that an implementation could meet the Common Criteria security specifications @cite_9 . However, to the best of our knowledge, very few formal verification approaches to check the correctness of software countermeasure schemes against fault attacks have been proposed yet. One of the most significant contributions has been proposed by Christofi @cite_16 . Their approach aims at performing a source code level verification of the effectiveness of a countermeasure scheme on a CRT-RSA implementation by using the Frama-C program analyzer. In this paper, we formally prove all our proposed countermeasures against an instruction skip fault model at assembly level. Another more recent contribution of a formal methodology at algorithm level has been proposed by Rauzy @cite_21 . In their scheme, an attacker can induce faults in the data flow of a target implementation described in a high-level language. This scheme enables them to detect unnecessary countermeasures or possible flaws on several CRT-RSA implementations.
@cite_9 @cite_16 @cite_21
2092627953 2106187462 2114235603 2146070389
Cryptosystems are highly sensitive to physical attacks, which lead security developers to design more and more complex countermeasures. Nonetheless, no proof of flaw absence has been given for any implementation of these countermeasures. This paper aims to formally verify an implementation of one published countermeasure against fault injection attacks. More precisely, the formal verification concerns Vigilant’s CRT-RSA countermeasure which is designed to sufficiently protect CRT-RSA implementations against fault attacks. The goal is to formally verify whether any possible fault injection threatening the pseudo-code is detected by the countermeasure according to a predefined attack model. In this article, we describe a methodology that aims at either breaking or proving the security of CRT-RSA implementations against fault injection attacks. In the specific case-study of the BellCoRe attack, our work bridges a gap between formal proofs and implementation-level attacks. We apply our results to three implementations of CRT-RSA, namely the unprotected one, that of Shamir, and that of Our findings are that many attacks are possible on both the unprotected and the Shamir implementations, while the implementation of is resistant to all single-fault attacks. It is also resistant to double-fault attacks if we consider the less powerful threat model of its authors. In this paper we present software countermeasures specifically designed to counteract fault injection attacks during the execution of a software implementation of a cryptographic algorithm and analyze the efficiency of these countermeasures. We propose two approaches based on the insertion of redundant computations and checks, which in their general form are suitable for any cryptographic algorithm. In particular, we focus on selective instruction duplication to detect single errors, instruction triplication to support error correction, and parity checking to detect corruption of a stored value. We developed a framework to automatically add the desired countermeasure, and we support the possibility to apply the selected redundancy to either all the instructions of the cryptographic routine or restrict it to the most sensitive ones, such as table lookups and key fetching. Considering an ARM processor as a target platform and AES as a target algorithm, we evaluate the overhead of the proposed countermeasures while keeping the robustness of the implementation high enough to thwart most or all of the known fault attacks. Experimental results show that in the considered architecture, the solution with the smallest overhead is per-instruction selective doubling and checking, and that the instruction triplication scheme is a viable alternative if very high levels of injected fault resistance are required. So far many software countermeasures against fault attacks have been proposed. However, most of them are tailored to a specific cryptographic algorithm or focus on securing the processed data only. In this work we present a generic and elegant approach by using a highly fault secure algebraic structure. This structure is compatible to finite fields and rings and preserves its error detection property throughout addition and multiplication. Additionally, we introduce a method to generate a fingerprint of the instruction sequence. Thus, it is possible to check the result for data corruption as well as for modifications in the program flow. This is even possible if the order of the instructions is randomized. Furthermore, the properties of the countermeasure allow the deployment of error detection as well as error diffusion. We point out that the overhead for the calculations and for the error checking within this structure is reasonable and that the transformations are efficient. In addition we discuss how our approach increases the security in various kinds of fault scenarios.