Gilles Barthe
email: gilles.barthe@imdea.org

François Dupressoir

Pierre-Alain Fouque
email: pierre-alain.fouque@ens.fr

Benjamin Grégoire
email: benjamin.gregoire@inria.fr

Jean-Christophe Zapalowicz
email: jean-christophe.zapalowicz@inria.fr

Synthesis of Fault Attacks on Cryptographic Implementations

Keywords: E.3 [Data encryption]: Public key cryptosystems, F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs Fault attacks, program verification, program synthesis, automated proofs

Fault attacks are attacks in which an adversary with physical access to a cryptographic device, say a smartcard, tampers with the execution of an algorithm to retrieve secret material. Since the seminal Bellcore attack on modular exponentiation, there has been extensive work to discover new fault attacks against cryptographic schemes and develop countermeasures against such attacks. Originally focused on highlevel algorithmic descriptions, these efforts increasingly focus on concrete implementations. While lowering the abstraction level leads to new fault attacks, it also makes their discovery significantly more challenging. In order to face this trend, it is therefore desirable to develop principled, tool-supported approaches that allow a systematic analysis of the security of cryptographic implementations against fault attacks.

We propose, implement, and evaluate a new approach for finding fault attacks against cryptographic implementations. Our approach is based on identifying implementationindependent mathematical properties, or fault conditions. We choose fault conditions so that it is possible to recover secret data purely by computing on sufficiently many data points that satisfy them. Fault conditions capture the essence of a large number of attacks from the literature, including lattice-based attacks on RSA. Moreover, they provide a basis for discovering automatically new attacks: using fault conditions, we specify the problem of finding faulted implementations as a program synthesis problem. Using a specialized form of program synthesis, we discover multiple faulted attacks on RSA and ECDSA. Several of the attacks found by our tool are new, and of independent interest.

INTRODUCTION

Embedded devices often play a central role in security architectures for large-scale software infrastructures. For instance, they are used pervasively for authentication, identity management, or digital signatures. As a consequence, embedded devices are also a prime target for attackers. There are primarily two means to retrieve secret material from embedded devices. The first one is to carry non-invasive monitoring of the device and to obtain information from side-channels, such as timing and power consumption, electromagnetic radiations, or even noise. The second one is to perform active attacks, injecting faults that interfere with the normal execution of the devices, and to recover the secret information through the device's normal interface, or through side-channels. The effects of these faults vary: they may modify the control flow of the program by skipping a conditional test [START_REF] Anderson | Low cost attacks on tamper resistant devices[END_REF] or induce behaviours similar to buffer overflows [START_REF] Fouque | Using faults for buffer overflow effects[END_REF]. In the context of cryptographic attacks, they often allow the adversary to directly recover secret keys. There are various ways to inject faults in devices using, for example, power spikes, glitches on the clock signal, temperature variations, or electromagnetic radiations [START_REF] Anderson | Low cost attacks on tamper resistant devices[END_REF][START_REF] Joye | Fault Analysis in Cryptography[END_REF][START_REF] Barenghi | A fault induction technique based on voltage underfeeding with application to attacks against AES and RSA[END_REF].

The existence of efficient fault attacks against cryptographic schemes was first demonstrated in [START_REF] Boneh | On the importance of checking cryptographic protocols for faults (extended abstract)[END_REF] by Boneh, DeMillo and Lipton. They consider an algorithm, shown in Figure 3, for computing RSA signatures using the Chinese Remainder Theorem (CRT) and its standard recombination formula: S = (Sq • p -1 mod q) • p + (Sp • q -1 mod p) • q mod N where Sp and Sq are modular exponentiations of the reductions modulo p and q of the integer M that encodes the message m. The algorithm is popular in practice, because it achieves a significant speedup (approximately 4 times faster) over the direct computation of S = M d mod N . The fault attack Boneh et al. exhibit allows them to retrieve the factorization of N , i.e. p and q, with a simple gcd computation. This attack requires knowledge of a valid signature S and a faulted signature S for the same padded message M . A second attack, due to Lenstra [START_REF] Joye | Chinese remaindering based cryptosystems in the presence of faults[END_REF], only requires knowledge of a single faulted signature S for a known padded message M . Injecting fault during the computation modulo p,

• in the first case, one can recover the factorization of N from the identity gcd(S -S, N ) = q;

• in the second case, one can recover the factorization of N from the identity gcd(M -S e , N ) = q. Both attacks, often known as the Bellcore attacks, are restricted to deterministic encodings. However, Boneh et al. describe another attack that applies to probabilistic encodings; unfortunately, this third attack is not as efficient as the others. In fact, it is only very recently that Fouque, Guillermin, Leresteux, Tibouchi and Zapalowicz [START_REF] Fouque | Attacking RSA-CRT signatures with faults on montgomery multiplication[END_REF] propose the first efficient fault attacks against RSA-CRT signatures with probabilistic encodings; their attacks are applicable against PKCS#1 v2.0 (PSS) signatures. In addition to the RSA-CRT signature considered in [START_REF] Boneh | On the importance of checking cryptographic protocols for faults (extended abstract)[END_REF], Fouque et al. consider another variant of RSA-CRT (Figure 4) based on Garner's recombination formula:

S = Sq + q • (q -1 • (Sp -Sq) mod p)
However, the main difference between [START_REF] Boneh | On the importance of checking cryptographic protocols for faults (extended abstract)[END_REF] and [START_REF] Fouque | Attacking RSA-CRT signatures with faults on montgomery multiplication[END_REF] lies in their level of description of RSA-CRT: whereas Boneh et al. [START_REF] Boneh | On the importance of checking cryptographic protocols for faults (extended abstract)[END_REF] consider a high-level algorithmic description in which modular exponentiation is treated abstractly, Fouque et al. consider reasonably detailed implementations, going down to algorithmic descriptions of modular multiplication. They consider four different implementations of modular exponentiation, among which the Square-and-Multiply algorithm and Montgomery's modular exponentiation algorithm [START_REF] Montgomery | Modular multiplication without trial division[END_REF]. Figure 1 shows the Coarsely Integrated Operand Scanning (CIOS) algorithm for modular multiplication, used in Montgomery's modular exponentiation algorithm (shown in Figure 2). Fouque et al. show that, by injecting faults in the implementations of Montgomery modular multiplication, one can obtain faulted signatures S that are close multiples of p or q, and then use lattice-based techniques to recover the factorization of N with about 50 faulty signatures. This example provides strong evidence that analyzing implementations rather than algorithmic descriptions can lead to the discovery of interesting attacks. However, it also highlights a number of difficulties with this approach:

1. the number of faulted implementations grows at least exponentially in the length of the original program, in particular if multiple faults are considered;

2. some fault attacks require to tamper with some (but not all) loop iterations, or to add or remove some loop iterations; hence, the number of faulted implementations cannot be bounded solely based on the length of the program;

3. analyzing the effects of faults becomes very involved and error-prone, in particular for programs with loops;

4. there exist multiple implementations of basic arithmetic operations, requiring to repeat the analysis for each;

5. there might exist numerous countermeasures against a fault attack, requiring to repeat the analysis for each of the protected implementations. This current trend towards analyzing security against fault attacks of implementations rather than high-level algorithmic descriptions is not specific to RSA signatures. In fact, it is also witnessed in elliptic curve cryptography. Biehl, Meyer and Müller [START_REF] Biehl | Differential fault attacks on elliptic curve cryptosystems[END_REF] were among the first to consider fault attacks against elliptic curve cryptosystems; more specifically, they consider an elliptic curve variant of ElGamal encryption. Their attacks exploit some of the ideas from Boneh et al. and are cast in the setting of a high-level algorithmic description of scalar multiplication between a field element and a point in the curve. These attacks were generalized to a more concrete setting by Ciet and Joye [START_REF] Ciet | Elliptic curve cryptosystems in the presence of permanent and transient faults[END_REF]. Later, Naccache, Nguyen, Tunstall and Whelan [START_REF] Naccache | Experimenting with faults, lattices and the DSA[END_REF] exhibit fault attacks on implementations of DSA and its elliptic curve variant ECDSA, whose description is given in Figure 6. Their attack introduces a fault during the generation of the nonce k and is cast in an algorithmic setting. In contrast, more recent works [START_REF] Schmidt | A fault attack on ecdsa[END_REF][START_REF] Barenghi | A novel fault attack against ECDSA[END_REF][START_REF] Bauer | Horizontal collision correlation attack on elliptic curves[END_REF][START_REF] Maimut | Fault attacks on projective-to-affine coordinates conversion[END_REF] study fault attacks against implementations of ECDSA, based on detailed accounts of integer multiplication, scalar multiplication, and point doubling. For example, the attack on integer multiplication [START_REF] Barenghi | A novel fault attack against ECDSA[END_REF] by Barenghi et al. works by injecting faults during the integer multiplication of a known random value and the secret key. Then, by considering the textbook multiplication implementation, they show that it is possible to recover the secret key. Finally, the attack of [START_REF] Maimut | Fault attacks on projective-to-affine coordinates conversion[END_REF] shows that it is possible to inject a fault during the conversion from projective to affine coordinates. These two attacks show that it is beneficial to consider all steps of an implementation-level description when looking for fault attacks. Our goal in this paper is to search for fault attacks by considering full implementationlevel descriptions of cryptographic algorithms.

1: function CIOS(x, y) 2: a ← 0 3: y0 ← y mod b 4: for j = 0 to k -1 do 5: a0 ← a mod b 6: uj ← (a0 + xj • y0) • q mod b 7: a ← a + xj • y + uj • q b 8:
end for 9:

if a ≥ q then a ← a -q 10: end if 11:

return a 12: end function

; q = -q -1 mod b is precomputed. The re- turned value is (xy • b -k mod q). Since b = 2 r , the division is a bit shift.

Our contributions

The thesis of this work is that it is beneficial to develop and implement rigorous methodologies for discovering fault attacks on cryptographic implementations. To support our thesis, we propose and validate experimentally a principled, tool-supported approach for discovering fault attacks on cryptographic implementations. Our approach relies on two broad contributions:

1. identifying fault conditions, a novel concept that captures the essence of fault attacks in a logical, implementation independent setting; 1: function ExpLadder(x, e, q, c) 2:

x ← CIOS(x, R 2 mod q) 3:

A ← R mod q 4:

for i = t down to 0 do 5:

if ei = 0 then 6:

x ← CIOS(A, x) 7:

A ← CIOS(A, A) 8:

else if ei = 1 then 9:

A ← CIOS(A, x) 10:

x ← CIOS(x, x) 11:

end if 12:

end for 13:

A ← CIOS(A, c) 14:

return A 15: end function Figure 2: Montgomery's Ladder for computing modular exponentiations: Exp Ladder (x, e, q, c) = x e • c mod q. e0, . . . , et are the bits of the exponent e (from the least to the most significant), b is the base in which computations are carried out (gcd(b, q) = 1) and R = b k .

1: function SignRSA-CRT(m) 2:
M ← µ(m) ∈ ZN message encoding 3:

S p ← ExpLadder(M mod p, dp, p, q -1 mod p) 4:

S q ← ExpLadder(M mod q, dq, q, p -1 mod q) 5:

S ← S q • p + S p • q mod N 6: return S 7: end function Figure 3: RSA-CRT signature generation. p and q are large primes and N = pq is the modulus. The public key is denoted by (N, e) and the associated private key by (p, q, d). The reductions dp, dq modulo p -1, q -1 of the private exponent, as well as the p -1 mod q and q -1 mod p CRT coefficients, are precomputed.

2. applying a form of program synthesis on concrete cryptographic implementations to automatically discover faulted implementations that realize fault conditions and lead to attacks. A third, more practical contribution is an evaluation of our approach on implementations of RSA and ECDSA signatures. During the process, we discover several faulted implementations, some of which lead to new attacks of independent interest. We elaborate on these points below.

Fault conditions. The first contribution (Section 3) is of methodological nature, and rests on the introduction of fault conditions. Informally, fault conditions are implementationindependent mathematical properties, specific to a cryptographic system, which capture sufficient conditions under which an attacker can launch a successful attack. Consider, for instance, the case of RSA signatures with public RSA modulus N = pq of length n. Any adversary with knowledge of a value Ŝ that is multiple of p but not multiple of q can obtain p by performing a simple GCD computation, and then q by division. This is captured by the fault condition Ŝ : Ŝ = 0 mod p ∧ Ŝ = 0 mod q 1: function SignRSA-Garner(m) 2:

M ← µ(m) ∈ ZN message encoding 3:

Sp ← ExpLadder(M mod p, dp, p, 1) 4:

Sq ← ExpLadder(M mod q, dq, q, 1) 5:

t ← Sp -Sq 6:

if t < 0 then t ← t + p 7:

end if 8:

S ← Sq + (t • π) mod p • q 9: return S 10: end function Figure 4: RSA-Garner signature generation. The Garner coefficient π = q -1 mod p is precomputed.

1: function ECScalMul(k,P ) 2:
R0 ← ∞ 3:

for i = t down to 0 do 4:

R0 ← [2] • R0 5: if ki = 1 then R0 ← R0 + P 6: end if 7:
end for 8:

return R0 9: end function Figure 5: Scalar Multiplication of an elliptic curve point by a field element. [START_REF] Anderson | Low cost attacks on tamper resistant devices[END_REF] • denotes point doubling, and + denotes point addition.

Figure 7 summarizes some relevant instances of fault conditions for RSA signatures; in Section 3, we also consider fault conditions for ECDSA signatures. For each of the fault conditions we consider, we exhibit an attack for retrieving the secret key. Broadly speaking, the attacks fall into two categories. The first one encompasses attacks that perform an elementary computation from a value satisfying the fault condition. The second one covers attacks that require many values that satisfy the fault condition, and involve more complex computations, typically based on lattice reductions. For the latter, we implement the attacks in a computer algebra system, and we experimentally validate their effectiveness for different choices of parameters.

Fault Models and Policies. The literature offers a wide range of fault models, that affect both data flow (for example the null fault model in which integer variables can be set to

1: function SignECDSA(m) 2: h ← H(m) message encoding 3: k $ ← [0, q -1] 4: (u, v) ← [k] • P 5:
r ← u mod q; if r = 0 then goto step 3; 6:

s ← k -1 (h + rx) mod q; if s = 0 then goto step 3; 7:

return (r, s) 8: end function Figure 6: ECDSA signature based on an elliptic curve E over a prime field Fp. P is a base point of order q and H is a cryptographic hash function of output length equal to the size of q. The private key is an element x ∈ Fq and the public key is denoted by (p, q, H, P, Q) with Q = [x]P .

Informal description

Fault condition

Attack technique Validity S is a multiple of p S = 0 mod p ∧ S = 0 mod q GCD computation Prop. 1 S is an almost full linear combination of p and q ∃α, β. S = α p + β q ∧ α, β < 2 n 2 -ε Orthogonal lattices Prop. 2 S is an almost full affine transform of p or q ∃α, β. S = α p + β ∧ α < q, β < 2 n/2-ε Orthogonal lattices Prop. 3 a null value) and control flow (for example, the instruction skip fault model, where an instruction can be skipped). We consider various fault policies, that subsume a wide range of such fault model and provide fine-grained specifications of the faults that can be performed on implementations. They model faults using replacement clauses of the form (x, e) where x is a variable and e is an expression, or (c, c ), where c and c are commands. These clauses respectively state that it is possible to replace x by e, and c by c in the execution of the program.

Automated synthesis of faulted implementations. Identifying fault conditions that allow efficient attacks to exist is a manual process that requires cryptographic expertise, and some good understanding of the mathematical tools available for cryptanalysis. The significant pay-off of fault conditions is that the process of finding complying faulted implementations can be automated. Our second contribution (Section 4) is a fully automated method for discovering faulted implementations that verify the fault condition.

Our method can be seen as an instance of program synthesis, an area that is currently undergoing rapid and significant progress (see Section 6). Broadly construed, the goal of program synthesis is to find, given a specification φ (for instance, φ might capture the input/output behavior of a program), a set of programs that satisfy φ. Because synthesis is computationally expensive, there exist many specialized forms of program synthesis that restrict the search space using non-functional requirements or by providing a partial description of the desired programs. We also specialize our synthesis algorithm to keep it computationally reasonable. Specifically, our algorithm takes as input a fault condition φ, an implementation c, and searches for all faulted implementations of c that satisfy φ. The search is constrained by two additional inputs. The first additional input is a fault policy; the second, optional input is an upper bound on the number of faults we allow.

Our algorithm exploits many of the standard techniques used in other approaches to program synthesis, including weakest preconditions and invariant generation, and interfaces with SMT solvers for checking the validity of first-order formulae. In addition, our algorithm relies on an automated prover to simplify the intermediate conditions generated by weakest precondition computations; the prover is specialized to formulae that combine arithmetic inequalities and size constraints; such formulae include many fault conditions, including all those we explore in this paper (see Figure 7). On the other hand, our algorithm noticeably departs from recent works on program synthesis by its simplicity: indeed, physical limits on the number and nature of faults sufficiently constrain the search space for faulted implementations, allowing us to dispense from using more elaborate techniques that are required to manage very large search spaces (see Section 6). Experimental results, which we report below, demonstrate that our synthesis algorithm performs well on standard examples.

Application: old and new attacks on RSA and ECDSA signatures. The third contribution of our work is a practical evaluation of our approach on RSA and ECDSA signatures. We carry out the evaluation using the computer algebra system SAGE, and the EasyCrypt tool1 . Concretely, we use the former for estimating the effectiveness of latticebased attacks for different fault conditions, and the latter (or more precisely an implementation of our synthesis algorithm built on top of EasyCrypt) for synthesizing faulted implementations of RSA and ECDSA signatures. During the process, we rediscover many known attacks; moreover, we also discover many new attacks, several of which are efficient attacks of independent interest. We summarize our main findings below:

1. For RSA-CRT signatures based on Garner's recombination, we recover the basic and most efficient attack of [START_REF] Fouque | Attacking RSA-CRT signatures with faults on montgomery multiplication[END_REF] which injects a null fault in the last call to CIOS during the computation of modular exponentiation. We also discover a new efficient attack, based on forcing additional iterations in the last call to CIOS. This attack yields almost full affine transforms of p or q, a small number of which is sufficient to recover the factorization of the RSA modulus using orthogonal lattices or Simultaneous Diophantian Approximations as in [START_REF] Fouque | Attacking unbalanced RSA-CRT using SPA[END_REF][START_REF] Lagarias | The computational complexity of simultaneous diophantine approximation problems[END_REF].

2. For RSA-CRT signatures based on the usual CRT recombination, we discover a new fault attack; to our best knowledge, this is the first efficient fault attack that works with randomized padding. The attack is based on forcing additional iterations in the last call to CIOS and yields almost full linear combinations of p and q. From a small number of such faulty signatures, the factorization of the RSA modulus can easily be recovered using orthogonal lattices.

3. For ECDSA signatures, we discover several new and efficient fault attacks for implementations based on the implementation of scalar multiplication given in Figure 5. A first attack is based on skipping the last iterations in the computation of scalar multiplication. A second attack is based on forcing the evaluation of a conditional inside the loop executed for the computation. The largest group of attacks (containing more than 100 faulted programs) is based on faulting the implementation of the point addition operation. Each faulted signature allows us to recover the least or most significant bits of the nonce; we then finish the attack using classic techniques, and obtain the secret key from a small number of faulty signatures. We also recover an existing attack [START_REF] Naccache | Experimenting with faults, lattices and the DSA[END_REF] that lets the faulted algorithm produce valid signatures that may nevertheless be exploited in a similar fashion.

BACKGROUND ON LATTICES

Lattice reduction is a powerful tool that is extensively used in the cryptanalysis of public-key cryptosystems. In this section, we provide a brief introduction to some key definitions and algorithms that are used in the paper. More background is given in the long version of this paper [START_REF] Barthe | Synthesis of fault attacks on cryptographic implementations[END_REF].

A lattice L is a subgroup of Z n , i.e. a non-empty set of vectors closed under addition and inverse. Every lattice L has a basis, i.e. a finite set of linearly independent vectors that generate all elements in L. Conversely, every set (b1, . . . , b ) of linearly independent vectors over Z n generate a lattice L = b1, . . . , b consisting of all integer linear combinations of the b i 's.

A central problem with lattices is to compute nearly reduced bases, i.e. bases that consist of reasonably short and almost orthogonal vectors. There exist many efficient algorithms for performing lattice reductions, including the celebrated Lenstra-Lenstra-Lovasz (LLL) algorithm [START_REF] Lenstra | Factoring polynomials with rational coefficients[END_REF] and Block Korkin-Zolotarev (BKZ) variants [START_REF] Schnorr | Lattice basis reduction: Improved practical algorithms and solving subset sum problems[END_REF]. Lattice reduction is an essential tool in cryptanalysis, and we use it extensively in our attacks. In theory, LLL outputs in polynomialtime a reduced basis and each vector of the base is related to the shortest ones by an approximation factor which is exponential in the dimension. BKZ algorithms allow different tradeoff between the quality of the approximation and the time complexity. In practice, LLL implementations are very fast and when the dimension is much less than 200 [START_REF] Stein | Sage Mathematics Software (Version 4.8)[END_REF], it is expected that LLL produces shorter vectors than other algorithms since its approximation factor is α ≈ 1.01, as shown experimentally in [START_REF] Gama | Predicting lattice reduction[END_REF]. In larger dimensions, the approximation factor increases (unless we greatly increase the time complexity) and the success probability of our attacks is reduced. To any lattice L in Z n is associated its orthogonal lattice L ⊥ , defined as the set of all vectors in Z n that are orthogonal to all vectors of L. It is possible to reduce the computation of the orthogonal lattice to lattice reduction in polynomial time [START_REF] Nguyen | Lattice reduction in cryptology: An update[END_REF]. Orthogonal lattices were introduced in cryptanalysis by Nguyen and Stern in [START_REF] Nguyen | Merkle-Hellman revisited: A cryptoanalysis of the Qu-Vanstone cryptosystem based on group factorizations[END_REF], and have since found many applications [START_REF] Nguyen | Lattice reduction in cryptology: An update[END_REF].

FAULT CONDITIONS

The primary goal of fault attacks is to induce outputs which satisfy an implementation-independent, mathematical property that guarantees that the secret key or some other confidential data can be efficiently recovered. Our approach critically relies on providing a precise formalization of these mathematical conditions, using fault conditions. Informally, a fault condition is a statement of the form v1, . . . , vn : φ ; s1, . . . , s k where φ is a logical formula that depend on v1, . . . , vn, and such that an attacker with access to sufficiently many distinct tuples of values (v1, . . . , vn) satisfying φ is able to recover secrets s1, . . . , s k (typically parameters of the cryptosystem) with high probability. More formally, φ is a firstorder formula over some first-order theory T , for instance modular arithmetic, and all variables that appear free in φ but not on the left of the colon can only denote parameters of the cryptosystem.

In this section, we introduce several fault conditions for RSA and ECDSA schemes, and show how, given sufficiently many satisfying values, one can efficiently retrieve either the factorization of the modulus (for the RSA case) or the secret key (for the ECDSA case). Many of these conditions appear implicitly in some variant form in the literature.

Convention. All the conditions we consider are of the form v1, . . . , vn : φ ; p, q for RSA and v1, . . . , vn : φ ; x for ECDSA. Since the secret values s1, . . . , s k are determined by the case study, from now on we simply write v1, . . . , vn : φ.

Fault conditions for RSA signatures

Throughout this section, we assume that N is an RSA modulus of size n, product of two large primes p and q. Proofs are detailed in the long version of this paper [START_REF] Barthe | Synthesis of fault attacks on cryptographic implementations[END_REF].

Finding multiples of p or q. Our first fault condition considers faulted signatures that are a multiple of p or q. This fault condition enables attacks on RSA by simple gcd computations.

Proposition 1. Given a single value S satisfying the condition:

S : S ≡ 0 mod p ∧ S ≡ 0 mod q, one can efficiently factor the RSA modulus N . Obviously the same result holds by switching p and q.

Proof. One can retrieve the factorization of N by performing a simple gcd computation between S and N . This fault condition is implicit for instance in [START_REF] Fouque | Attacking RSA-CRT signatures with faults on montgomery multiplication[END_REF].

Finding "almost full" linear combinations of p and q.

Our second fault condition considers faulted signatures that are linear combinations of p and q with almost full coefficients. A variant of this fault condition is implicit in [START_REF] Brier | Modulus fault attacks against RSA-CRT signatures[END_REF].

Proposition 2. Assume that N is a balanced RSA modulus, i.e. N = p • q such that p, q < 2 n/2 . Given a sufficient number of values that satisfy the fault condition:

S : ∃x, y. S = x • p + y • q ∧ x, y < 2 n/2-ε
with ε > 0, one can efficiently factor the RSA modulus N . The value of ε depends on n and impacts the efficiency and success probability of the algorithm to recover the factorization.

Relating this fault condition with [START_REF] Brier | Modulus fault attacks against RSA-CRT signatures[END_REF]. In [START_REF] Brier | Modulus fault attacks against RSA-CRT signatures[END_REF], the authors force random faults on the modulus during CRT recombination and obtain a fault condition of the following form.

S : ∃α, β. S = α•p(p -1 mod q)+β•q(q -1 mod p)∧α, β < 2 n/2 .
If our condition is similar to theirs, the algorithmic problem ours captures is more general. Indeed, in the analysis, the crucial parameter is the ratio between the size of p, q and the size of α, β in the relation S = α • p + β • q. The larger this ratio is, the easier the attack is since the target vector, called u above is larger. In our case, the size of this vector is close to 2 ε / √ while [START_REF] Brier | Modulus fault attacks against RSA-CRT signatures[END_REF] consider a much larger one (their ratio is N/ ). Finding "almost full" affine transforms of p or q. Our third fault condition considers faulted signatures that are almost full affine transforms of p or q. This condition is implicit in [START_REF] Fouque | Attacking RSA-CRT signatures with faults on montgomery multiplication[END_REF].

Proposition 3. Assume that N is a balanced RSA modulus, i.e. p, q such that p, q < 2 n/2 . Given a sufficient number of values that satisfy the fault condition:

S : ∃x, y. S = x • p + y ∧ x < q, |y| < 2 n/2-ε ,
one can efficiently factor the RSA modulus N . The value ε depends on n and impacts the efficiency and success probability of the algorithm to recover the factorization.

Implementation and evaluation of key recovery

We now describe how the attacks outlined above can be performed in practice. Moreover, we estimate the number of signatures required for recovering the factorization.

Implementation. We use the SAGE computer algebra system [START_REF] Stein | Sage Mathematics Software (Version 4.8)[END_REF] to implement the attacks. The attacks take as input a sufficient number of signatures S1, • • • , S satisfying the fault condition given in Proposition 2 or Proposition 3. The implementation heuristically recovers the factorization of the RSA modulus N as follows.

• Compute an LLL-reduced basis {b1, • • • , b -1 } of the lattice (S1, • • • , S ) ⊥
. This is done by applying LLL to the lattice in Z 1+ generated by the rows of the following matrix:

   κS1 1 0 . . . . . . κS 0 1   
where κ is a suitably large constant, and removing the first component of each resulting vector [START_REF] Nguyen | Merkle-Hellman revisited: A cryptoanalysis of the Qu-Vanstone cryptosystem based on group factorizations[END_REF].

• Compute an LLL-reduced basis {x , y } of the orthogonal lattice {b1, • • • , b -2 } ⊥ . Again, this is done by applying LLL to the lattice in Z -2+ generated by the rows of

   κ b1,1 • • • κ b -2,1 1 0 . . . . . . . . . κ b 1, • • • κ b -2,1 0 1   
and keeping the last components of each resulting vector.

• For all the linear combinations z of x and y that satisfy the size constraints, compute the test gcd(z1S2 -z2S1, N ) or gcd(y1 -S1, N ), depending on the fault condition considered, which allows to recover the prime factors p and q.

Evaluation. We use our SAGE implementation to evaluate the number of signatures required for the attacks to succeed.

The results are given in Figures 8 and9. We see for instance that 35 values are required to retrieve the factorization of N when p and q are 1024-bit and the size of the xis and yis have size 960, i.e. 64 bits shorter than the full size.

Fault conditions for ECDSA signatures

For ECDSA signatures, we consider fault conditions of a different nature, that rely on partial knowledge of the nonce k used in the computation. We first consider a novel fault condition focusing only on faulting the scalar multiplication. Then, we discuss an already-exploited fault condition where k can be faulted during both the scalar multiplication and the computation of its inverse, as considered in [START_REF] Naccache | Experimenting with faults, lattices and the DSA[END_REF]. In both cases, knowing some bits of the nonce k is sufficient to mount a classic lattice-based attack. In the following, we assume that the message to be signed is known and its hash value is h and we denote abs the abscissa of an elliptic curve point, lsb k the least significant bits of k and for the right-shift operator.

Faulting r. Our fault condition considers faulted signatures such that r is computed using only some of the bits of k: Proposition 4. Given sufficiently many values satisfying one of the fault conditions:

r, s : ∃k. r = abs([k ] • P ) ∧ s = k -1 (h + rx) mod q (1) r, s : ∃k. r = abs(±[2 ] • [k ] • P ) ∧ s = k -1 (h + rx) mod q (2)
one can efficiently retrieve the secret key x.

The proof of this proposition can be done in two parts, summed up by two facts. We do the proof for condition (1), but a similar proof applies for condition [START_REF] Anderson | Low cost attacks on tamper resistant devices[END_REF]. In particular, Fact 2 tells us that it is sufficient to be able to recover bits of k to recover the secret key x, and the proof of Fact 1 generalizes to condition (2), since it revolves around computations on curve points

±[2 ] • [k ] • P .
Fact 1. Given a single pair (r, s) that satisfies the fault condition:

r, s : ∃k. r = abs([k ] • P ) ∧ s = k -1 (h + rx) mod q,
one can efficiently retrieve the least significant bits of k.

Now, given sufficiently many faulty signatures, the secret x can be recovered using a technique based on lattices.

Fact 2. Given a sufficient number of ECDSA signatures whose nonces k are partially known, one can efficiently retrieve the secret key x.

Note to conclude that a similar result holds for the most significant bits. For example, condition 1 in this case could be written as follows.

r, s : r = abs([k mod 2 n-]P ) ∧ s = k -1 (h + rx) mod q.

In this case, we retrieve the most significant bits of the nonces and adapt the lattice to this case without difficulty.

Using short randomness: faulting r and s.. We also consider the following fault condition, implicitly used in the original attack on ECDSA by Nguyen et al. [START_REF] Naccache | Experimenting with faults, lattices and the DSA[END_REF], where both the scalar multiplication and field inversion are faulted to simulated short values for k (that is, values whose most significant or least significant bits are zero).

Proposition 5 ([36]

). Given a sufficient number of pairs (r, s) that satisfy the fault condition:

r, s : ∃k. r = abs([lsb(k)] • P ) ∧ s = lsb(k) -1 (h + rx) mod q,
one can efficiently recover the secret key x.

Although we do not prove it, the validity of this fault condition is justified by its use in existing attacks. Implementation and evaluation.. We also implement our key recovery attacks on ECDSA in Sage to evaluate their performance. Some experimental values of ( , d) are given in Figure 10.

q

Discussion

All the fault conditions considered above are intended to predicate over the output of faulted signatures. However, fault conditions may also relate outputs of faulted and valid signatures, or inputs and outputs of signatures. Examples of such fault conditions are given by the original Bellcore attack and by Lenstra's variant: S1, S2 : S1 -S2 ≡ 0 mod p ∧ S1 -S2 ≡ 0 mod q M, S : S -M e ≡ 0 mod p ∧ S -M e ≡ 0 mod q Both conditions can be further refined. For instance, the fault condition for the Bellcore attack can be refined to express that one of the Si, say for instance S1, is a valid signature of a message m, and S2 is a faulty signature of m. In fact, one can define a partial order on fault conditions 2 and prove that the above fault conditions are less than the fault condition given in Proposition 1.

2 (v1, . . . , vn : φ) ≤ (w1, . . . , wm : ψ) if there exists an efficient and public n-ary function f that returns mtuples of values and such that for every v1, . . . , vn such that φ(v1, . . . , vn) holds and for every w1, . . . , wm such that f (v1, . . . , vn) = (w1, . . . , wm), we also have ψ(w1, . . . , wm).

C ::= skip | C; C sequencing | V ← E deterministic assignment | V $ ← DE random assignment | if E then C else C conditional | while E do C while loop | V ← P(E, . . . , E) procedure call | return E return expression
where V denotes the set of variables, E denotes the set of expressions, DE denotes the set of distribution expressions and P denotes the set of procedures.

SYNTHESIS OF FAULTED IMPLEMEN-TATIONS

In this section, we present an automated tool that synthesizes faulted implementations that verify a fault condition. Our tool is built on top of EasyCrypt [START_REF] Barthe | Computer-aided security proofs for the working cryptographer[END_REF], a tool-assisted framework for verifying the security of cryptographic constructions.

Programming and assertion language

We consider programs that are written in a core imperative language with deterministic and probabilistic assignments, conditionals, loops, procedure calls, and sequential composition; the syntax of programs is given in Figure 11. The programming language essentially subsumes the language proposed in [START_REF] Bellare | The security of triple encryption and a framework for code-based game-playing proofs[END_REF] and in particular is sufficiently expressive to capture cryptographic implementations.

Expressions used in programs, for instance on the righthand side of assignments or as guards in conditional statements and loops are built inductively from user-defined constants, operators, and variables. In this paper, we specifically focus on expressions that are built from operations for modular arithmetic, and finite field and elliptic curve operations. We use a simple type system for expressions and programs, and we only consider well-typed programs.

Assertions are first-order formulae over the theories inherited from the expression language. Reasoning about assertions is delegated to the EasyCrypt proof engine, which can either use lemmas from libraries or invoke SMT solvers to prove the validity of an assertion.

Fault models and fault policies

Fault models. Fault models are high-level specifications of the type of faults that can be injected on embedded devices; they generally target specific architectures, and are designed to reflect the effects and capacities of specific perturbation techniques.

For the purpose of this paper, it is sufficient to know that there exist two broad classes of fault models. The first class captures faults that modify the dataflow, for instance by setting a particular register to a default value (the null fault model) or to a constant but unknown value (the constant fault model), or by setting part of the register to a constant value (the zero high-order bits fault model and its variants). In practice, it is often important to consider models that combine several kinds of faults; for instance, one can consider a fault model which allows null faults on small registers, and constant faults on larger registers. Such faults are considered for example in [START_REF] Fouque | Using faults for buffer overflow effects[END_REF], where the authors also justify their practical feasibility. The second class captures faults that modify the control flow, for instance by skipping an instruction (the instruction skip model), by forcing a conditional instruction to enter into a specific branch (the branch fault model), or by forcing the execution of a loop to be interrupted before the guard is set to false, or continued after it is set to false (the loop fault model). These models are classic and are considered in [START_REF] Page | Fault and side-channel attacks on pairing based cryptography[END_REF], for instance. Both models overlap, in the sense that one can sometimes achieve the same effect by a dataflow fault attack, or by a control flow fault attack.

Fault policies. Instead of hardcoding the different fault models, our tool allows users to specify fine-grained fault policies that delineate very precisely the space of faulted implementations by describing which faults can be injected in the program. Fault policies are program specific, and are given by two sets of replacement clauses.

The first set consists of variable replacement clauses of the form (x, e) where x is a program variable and e is an expression; such a clause says that one can replace the variable x by the expression e in the course of program execution. These declarations can be used to model data faults; for instance, the null fault on x is captured by the clause (x, 0), whereas the zero high order bits fault on x that sets r bits to zero is captured by the clause (x, msbr(x)).

The second set consists of command replacement clauses of the form (c, c ), where c and c are commands; such a clause says that one can replace the command c by the command c in the course of program execution. These declarations can be used to model control flow faults; for instance, instruction skip faults on an assignment c is captured by the clause (c, skip), whereas branch faults are captured by the clause (if b then c1 else c2, ci) where i = 1 if the goal is to force execution to go into the true branch, and i = 2, otherwise. By convention, we require that all instruction replacements do not increase the set of modified variables, i.e. the set of modified variables of a command c is a subset of the set of modified variables of the command c it replaces. This is the case for all control flow attacks described above, and is essential for the completeness of our tool.

Although it is useful in practice, fault policies do not currently include a mechanism to impose any locality constraint on the clauses, i.e. replacements may occur anywhere in the program. This can easily be circumvented by writing programs in pseudo-SSA form, for instance by adding subscripts for the different occurences of the same variable in the program.

Finally, fault policies may also include some upper bounds on the number of times a clause can be used to fault an implementation. This is useful to constrain the space of faulted implementations and to match physical constraints.

Discussion. There is a direct relation between fault models and fault policies, in the sense that every fault model determines a unique fault policy for each program. However, many fault attacks require multiple faults and can only be captured by hybrid fault models, that combine several simpler ones. An example of hybrid fault model is one that considers null faults on variables that denote small registers (for instance, variables that store values smaller than 2 8 ), and constant faults on variables representing larger registers.

It would be interesting to develop a high-level language for describing hybrid fault models, and a compiler for generating automatically fault policies from high-level specifications. However, building the compiler requires a significant amount of infrastructure, including the ability to automatically infer program invariants: for the example discussed above, the compiler would need to infer that the value held by a variable x is always smaller than 2 8 in order to generate the clause (x, 0). We leave the design of this high-level language and the implementation of the compiler for future work, and require for now that fault policies (albeit in some edulcorated form) are given as input to the tool.

Algorithm

Our tool takes as input a (non-faulted) implementation written in the programming language of EasyCrypt, a fault condition, a fault policy, and optionally a precondition ψ. It outputs a set of faulted implementations that satisfy the fault condition and are valid faults of the original implementation with respect to the fault model considered. The core of the tool is an algorithm that interleaves the computation of weakest preconditions, logical simplifications, and generation of faults. For simplicity, we describe a non-deterministic and inefficient version of the algorithm, whereas the implementation uses a more efficient implementation, and some caching and early pruning techniques for the smart exploration of the search space. We initially explain how the algorithm works on straightline programs, i.e. programs without loops, conditionals, and procedure calls. Then, we explain how to extend the algorithm to procedure calls and loops. First, we define the notion of faulted instruction.

Faulted commands. The fault policy determines for each command c of the program a set of faulted instances, consisting of commands c that can be obtained from c according to the fault policy. All commands are faulted instances of themselves, and moreover the command c is a faulted instance of c if there exists an instruction replacement clause (c, c ). Moreover, there are some specific rules for each construct of the language.

• x ← e[e1, . . . , en/y1, . . . , yn] is a faulted instance of x ← e, provided for i = 1 . . . n, the replacements of yi by ei are allowed by the fault policy. Straightline programs. The algorithm is given as input a fault policy, and manipulates triples of the form (c, φ, c). Initially, the algorithm is given the triple (c, φ, skip) consisting of the program being analyzed against fault attacks, the fault condition, and the empty statement. At each iteration, the algorithm consumes the last command of c and outputs a new triple (c , φ , c ) as follows;

1. c is decomposed into a sequence c ; i, where i is the last command of the program (necessarily an assignment or a random sampling). If c is empty, then the algorithm checks if φ is a consequence of the precondition, and returns c if this is the case and nothing otherwise; 2. the algorithm checks whether i affects φ, i.e. if any of the variables modified by i occur in φ. If not, the algorithm breaks to the next iteration with (c , φ, c ), where c = i; c; 3. if some variable modified by i occurs in φ, then the algorithm chooses non-deterministically a faulted instance i of i; 4. the algorithm computes the weakest precondition of i on φ. For instance, the rules for computing weakest preconditions of deterministic and random assignments are:

WP(x ← e, φ) = φ{x ← e} WP(x $ ← d, φ) = ∀v ∈ dom(d), φ{x ← v},
where dom(d) is the set of values that have a nonzero probability in d. Note that the weakest precondition computation takes an assertion and returns an assertion. This is achieved by viewing probabilistic assignments as non-deterministic assignments over the domain of the distribution from which the assignment is sampled; 5. the algorithm applies logical simplifications to the assertion φ output by the weakest precondition computation. The output is a new assertion φ that has fewer free variables than φ; 6. the algorithm proceeds to the next iteration with state (c, φ , c ), where c = i ; c. Breaking to the next iteration in step 2 and performing logical simplifications in Step 5 may in fact significantly prune the search space, without ruling out any potential attacks: computing the weakest precondition on a command i whose left-hand-side does not appear in the fault condition never changes that fault condition, whichever fault may be selected. Indeed, our algorithm is sound and relatively complete for straightline code, in the sense that, given an oracle that can decide logical implications, the algorithm would return all faulted versions c of c such that the Hoare triple {ψ}c {φ} is valid. In practice, logical implications are verified using SMT solvers, and hence the implementation might actually fail to find a valid fault attack.

Procedure calls. Our tool deals with programs that make non-recursive procedure calls by entering into the code of the procedure when reaching a call. This is intuitively equivalent to inlining all procedure calls and applying the nonprocedural analysis to the inlined code. Although it is certainly possible to develop more sophisticated approaches, including ones that deal with recursive procedure calls, based on state-of-the-art techniques, our elementary approach has the advantage of simplicity and is sufficient for most implementations of cryptographic algorithms.

Loops. Dealing with loops is the main source of complexity for our tool, as computing weakest preconditions requires knowing some useful loop invariants, i.e. assertions that hold throughout all iterations of the loop body. We provide two elementary mechanisms for dealing with loops: an invariant generator, and an algorithm for turning (userprovided) invariants for non-faulted loops into invariants for their faulted instances. There is admittedly significant scope for improving these mechanisms, in particular by building upon recent developments in invariant generation; we leave this avenue for future work.

Pruning. We use two main pruning techniques for improving the efficiency of the search algorithm. First, since SMT solvers are a clear performance bottleneck, we cache all SMT queries and their result. Second, we maintain a table of all intermediate statements (c, φ, c), and abort execution whenever the algorithm computes a triple which coincides in the first and second component with an element of the table.

APPLICATIONS

Using our tool, we are able to discover many attacks on implementations of RSA-CRT and ECDSA signatures. Several of these attacks are new, and of independent interest. In this section, we review in some detail the most relevant attacks we find.

RSA-CRT signatures

We consider a CRT-based implementation of RSA that uses the Montgomery ladder (Figure 2) for modular exponentiation and the CIOS algorithm (Figure 1) for modular multiplication. We consider implementations using both Garner's recombination algorithm (Figure 4) and the standard CRT recombination with optimizations (Figure 3). Most of the attacks we find involve faults injected during the last call to CIOS in the ladder (line 13, Figure 2), which takes the result of the exponentiation back into its classical representation. We assume that the parameter x in CIOS is stored in a shift-register, used to extract its individual digits in base b.

Finding multiples of p or q. Using the fault condition from Proposition 1, and allowing null faults on small variables (that contain integers mod b) we recover the most basic and efficient attack of [START_REF] Fouque | Attacking RSA-CRT signatures with faults on montgomery multiplication[END_REF], which sets q to 0 during the final call to CIOS( Sq, 1). In addition, the tool also finds several variants of the fault, indicating which (combinations of) variables can be set to 0 to fulfill the fault condition. For example, setting both uj and xj to 0 throughout the computation still yields a null result.

This attack and its variants only work when the final call to CIOS occurs with 1 as second argument. This is not always the case when CRT recombination is used, since the call to CIOS can be used to optimize a multiplication away as illustrated in Figure 3. In this case, by adding control flow faults to the fault policy, our tool also finds that faulting q to 0 and doubling the number of loop iterations during this final call forces its result to zero. Indeed, in this case, after the normal number of iterations, the shift-register initially containing x contains zero and any further loop iteration simply shifts a to the right, eventually forcing it to zero as well. A much simpler, albeit much less elegant, control flow fault involves simply faulting the initial loop condition so no computation is performed.

Finding "almost full" linear transforms of p or q. It may not always be possible to skip the loop entirely, or to ensure that the loop is run at least twice as many times as expected. However, it may be easier to inject faults on loop counters that consistently add a small (possibly unknown) number of iterations. Our tool automatically finds that such faults, when q is set to zero during the additional loop iterations are in fact sufficient to guarantee the fault condition from Proposition 3 using both Garner and CRT recombination. For each additional iteration, the size of the exponentiation's result is reduced by the size of a base b digit, quickly leading to a result that can be exploited by the classic lattice-based attacks described in Section 3.1.

Alternatively, instead of faulting the control flow and a variable, our tool also finds that simply setting q and xj to zero during the last iterations of the loop leads to a similarly faulted signature, that fulfills the desired fault condition.

Finding "almost full" linear combinations of p and q.

When given the fault condition from Proposition 2, our tool finds that running the previous size-reducing attacks on both half-exponentiations yields a suitable faulted signature when using the classic CRT recombination rather than Garner's. The relative efficiency of the lattice-based attack from Section 3.1 compared to the one from Section 3.1 may justify the additional faults.

ECDSA signatures

We also run our tool on the ECDSA signature algorithm. We consider an implementation where scalar multiplication is computed using MSB-first Double-and-Add (Figure 5). The main challenge here is that the fault conditions we consider are very precise, in the sense that they give a full functional description of the result depending on some (faulted) inputs. We therefore need not only to be able to find the faults, but also to be able to prove the functional correctness of the non-faulted algorithms.

Faults on the randomness. We first consider the fault condition from Proposition 5, that we generalized from [START_REF] Naccache | Experimenting with faults, lattices and the DSA[END_REF]. The tool finds that performing a zero-higher-order bit fault on k after it is sampled is sufficient to guarantee the fault condition (as we then have k = k

). However, we do not automatically find more complex attacks (that use proposition 5) on the algorithms computing scalar multiplications and field element inversions. We believe that our tool would in fact find such attacks given precise enough implementations for these operations, and precise enough loop invariants for their non-faulted versions.

Faults on scalar multiplication.. Fault condition (1) from Proposition 4 allows our algorithm to quickly focus the fault search on the computation of the scalar multiplication in ECDSA. The tool discovers that exiting the loop early when computing [k] • P , and letting all other computations occur normally, yields signatures (r, s) that fulfill fault condition 4(1).

The second fault condition (2) from Proposition 4 leads to a slightly more flexible overall attack, since it does not require the number of faulted iterations to be known. Given this fault condition and an abstract algorithmic description of the ECDSA algorithm, our tool finds that forcing the branch condition at line 5 (Figure 5) to false for a number of iterations towards the end of the loop yields an exploitable result. Generalizing, faulting line 6 or its implementation such that it computes R0 ← ±R0 instead of R0 ← R0 + P would yield the same result.

Faults on point addition. This observation leads us to consider more concrete refinements of the point addition algorithm. In particular, we consider a register-level algorithm for Jacobian-Jacobian point addition, as presented by Murdica [START_REF] Murdica | Physical Security of Elliptic Curve Cryptography[END_REF]Algorithm 36]. This algorithm, shown in the long version of this paper, is only correct when applied to distinct curve points that are not at infinity or inverse of each other.

Given the implementation where the partial point addition algorithm is wrapped in tests ensuring it is applied correctly (that is, Q, R = ∞ and Q = ±R), our tool quickly finds that faulting the conditional checks is sufficient to force the fault condition: by faulting the test that checks whether the second argument is infinite, we can easily force the wrapped addition algorithm to return its first argument, forcing the fault condition.

However, since the base point P is of order q, and R0 is always a scalar multiple of P , such checks can be optimized away when the addition algorithm is used for scalar multiplication. With an additional condition that none of the scalar multiples of P are on the vertical axis our tool finds null faults, and some faults in combined models involving null faults and instruction skips, that lead to the faulted computation of R0 + P returning -R0. Performing this fault during the last iterations of the Double-and-Add loop then yields a faulted ECDSA signature that fulfills fault condition 4(2) and can be used in the lattice-based attack. Our tool yields a list of more than 100 ways to fault point addition such that the faulted ECDSA signature fulfills fault condition 4(2).

RELATED WORK

Formal methods for cryptography. This work is more closely related to a recent series of articles that apply formal methods to fault attacks. However, our emphasis is on finding fault attacks against implementations, whereas other works focus on proving absence of fault attacks against algorithmic descriptions or implementations. Two independent efforts by Christofi, Chetali, Goubin and Vigilant [START_REF] Christofi | Formal verification of a CRT-RSA implementation against fault attacks[END_REF] and by Rauzy and Guilley [START_REF] Rauzy | A formal proof of countermeasures against fault injection attacks on CRT-RSA[END_REF] prove the absence of fault attacks against RSA-CRT with Vigilant countermeasure. In a similar spirit, Moro et al. [START_REF] Moro | Formal verification of a software countermeasure against instruction skip attacks[END_REF] propose an approach based on redundancy to protect implementations against instruction skip attacks. More recently, Barthe, Dupressoir, Fouque, Grégoire, Tibouchi and Zapalowicz [START_REF] Barthe | Making RSA-PSS provably secure against non-random faults[END_REF] formally verify the security RSA-PSS against non-random faults using Easy-Crypt [START_REF] Barthe | Computer-aided security proofs for the working cryptographer[END_REF].

Another recent series of papers use type systems and SMT solvers for verifying whether cryptographic implementations are correctly masked [START_REF] Moss | Compiler assisted masking[END_REF][START_REF] Bayrak | Sleuth: automated verification of software power analysis countermeasures[END_REF][START_REF] Eldib | SMT-based verification of software countermeasures against side-channel attacks[END_REF]; in particular, Eldib and Wang [START_REF] Eldib | Synthesis of masking countermeasures against side channel attacks[END_REF] have developed a method for synthesizing masking countermeasures.

Synthesis. Program synthesis is an active area of research that is undergoing rapid and significant progress, thanks to novel and practically achievable approaches, and to advances in SMT solvers. In contrast to the early works that pursue deductive program synthesis, where the program is extracted from the proof of a theorem, typically a ∀∃ statement, most of the current work focuses on inductive program synthesis, and uses SMT solvers. Many works on inductive synthesis, notably early ones, have focused on loop-free programs [START_REF] Solar-Lezama | Programming by sketching for bit-streaming programs[END_REF]23,[START_REF] Jha | Oracle-guided component-based program synthesis[END_REF]. Other recent works allow synthezing programs with loops; for instance, Srivastava, Gulwani and Foster [START_REF] Srivastava | From program verification to program synthesis[END_REF] introduce proof-theoretic synthesis, a variant of synthesis that combines inference of loop invariants and synthesis of loop-free programs. However, this approach is limited to programs whose loop invariants fall into a limited class of assertions. Syntax-guided program synthesis [START_REF] Alur | Syntax-guided synthesis[END_REF] is a recently proposed framework that subsumes many of the previous approaches to synthesis. One ambition of this project is to develop a framework for testing and comparing different implementations, and in particular to provide a common input format inspired from SMT-LIB for synthesis tools. In the future, it would be interesting to suggest automated discovery of fault attacks as a challenge for syntaxguided synthesis competitions.

Our approach shares many similarities with program repair, an instance of program synthesis that aims at automatically eliminating deficiencies in code. Informally, a program repair algorithm takes as input a program p and a property φ that must be satisfied by the output of p, and computes by small successive modifications of p a program p that satisfies φ. There exist many approaches to program repair; some of them are based on genetic algorithms [START_REF] Le Goues | Genprog: A generic method for automatic software repair[END_REF], others are based on code contracts [START_REF] Wei | Automated fixing of programs with contracts[END_REF]. We refer the reader to a recent overview [START_REF] Le Goues | Current challenges in automatic software repair[END_REF] for more information. The connection with program repair is very direct; indeed, one can even view faulted implementations as a form of program repair for the attacker. However, the techniques used in program repair are not immediately applicable to finding fault attacks on cryptographic implementations.

CONCLUDING REMARKS

We have presented a new approach to discover automatically fault attacks on cryptographic implementations. The technical core of our approach is a new and practical form of program synthesis. Pleasingly, the tool that implements our approach is able to discover new and interesting attacks. An exciting perspective for further work is to apply our tool to an extensive class of implementations. There are also interesting directions for improving and extending our tool. The first one is to integrate state-of-the-art invariant generation and synthesis techniques in the tool. Another one is to implement a synthesis algorithm based on relational verification in order to deal with relational fault conditions, i.e. fault conditions that relate faulted and valid signatures. Although cast in a different context, the work reported in [START_REF] Barthe | From relational verification to SIMD loop synthesis[END_REF] provides an excellent starting point. Yet another one would be to use synthesis for discovering countermeasures against fault attacks as done in [START_REF] Eldib | SMT-based verification of software countermeasures against side-channel attacks[END_REF] for side-channel attacks.

Whereas the focus of this paper is on implementations of public key cryptography, our method would also apply to the symmetric setting. Finding good fault conditions, as well as the considerable size of the implementations would make such an application challenging, but should allow fairly easily to find attacks on the last few rounds of computation.

Figure 1 :

 1 Figure1: The Montgomery multiplication algorithm. The xi's and yi's are the digits of x and y in base b; q = -q -1 mod b is precomputed. The returned value is (xy • b -k mod q). Since b = 2 r , the division is a bit shift.

Figure 7 :

 7 Figure 7: Fault conditions for RSA signatures. The value of ε depends on the size n of the modulus and is a multiple of the words size.

Figure 9 :

 9 Figure 9: Minimal number of signatures to be faulted depending on the bitsize of yi. Almost full affine transforms of p or q.

Figure 10 :

 10 Figure 10: Minimal number of signatures d to be faulted depending on using curves brain-poolP160r1, brainpoolP256r1 and brainpoolP384r1. The percentage given in one case represents the success rate of the attack and could be increased by increasing the value of d.

Figure 11 :

 11 Figure 11: Syntax of programs

  • the commands while b do c , and if b then c ; while b do c, and while b do c; if b then c are all faulted instances of while b do c, where c is a faulted instance of c, and b is a guard that forces exactly one less iteration of the loop body. The last clause captures faults on the first and last iteration of a loop, and can be extended to model faults on the first and last k iterations of a loop, for k ≥ 1.

https://www.easycrypt.info

Acknowledgments. The work of Barthe and Dupressoir has been partially supported by ONR grant N00014-12-1-0914, Madrid regional project S2009TIC-1465 PROMETI-DOS, and Spanish projects TIN2009-14599 DESAFIOS 10 and TIN2012-39391-C04-01 Strongsoft.