Sonia Belaïd

Pierre-Évariste Dagand

Darius Mercadier
email: darius.mercadier@lip6.fr

Matthieu Rivain
email: matthieu.rivain@cryptoexperts.compierre-evariste.dagand

Raphaël Wintersdorff
email: raphaelwin@hotmail.com

Tornado: Automatic Generation of Probing-Secure Masked Bitsliced Implementations

Keywords: Compiler, Masking, Automated verification, Bitslice

Cryptographic implementations deployed in real world devices often aim at (provable) security against the powerful class of side-channel attacks while keeping reasonable performances. Last year at Asiacrypt, a new formal verification tool named tightPROVE was put forward to exactly determine whether a masked implementation is secure in the well-deployed probing security model for any given security order t. Also recently, a compiler named Usuba was proposed to automatically generate bitsliced implementations of cryptographic primitives. This paper goes one step further in the security and performances achievements with a new automatic tool named Tornado. In a nutshell, from the high-level description of a cryptographic primitive, Tornado produces a functionally equivalent bitsliced masked implementation at any desired order proven secure in the probing model, but additionally in the so-called register probing model which much better fits the reality of software implementations. This framework is obtained by the integration of Usuba with tightPROVE + , which extends tightPROVE with the ability to verify the security of implementations in the register probing model and to fix them with inserting refresh gadgets at carefully chosen locations accordingly. We demonstrate Tornado on the lightweight cryptographic primitives selected to the second round of the NIST competition and which somehow claimed to be masking friendly. It advantageously displays performances of the resulting masked implementations for several masking orders and proves their security in the register probing model.

Introduction

Cryptographic implementations susceptible to power and electromagnetic side-channel attacks are usually protected by masking. The general principle of masking is to apply some secret sharing scheme to the sensitive variables processed by the implementation in order to make the side-channel information either negligible or hard to exploit in practice. Many masked implementations rely on Boolean masking in which a variable x is represented as n random shares x 1 , . . . , x n satisfying the completeness relation x 1 ⊕ • • • ⊕ x n = x (where ⊕ denotes the bitwise addition).

The probing model is widely used to analyze the security of masked (software) implementations vs. side-channel attacks. This model was introduced by Ishai, Sahai and Wagner in [START_REF] Ishai | Private circuits: Securing hardware against probing attacks[END_REF] to construct circuits resistant to hardware probing attacks. It was latter shown that this model and the underlying construction were instrumental to the design of efficient practically-secure masked cryptographic implementations [START_REF] Rivain | Provably secure higher-order masking of AES[END_REF][START_REF] Carlet | Higherorder masking schemes for S-boxes[END_REF][START_REF] Coron | Higher-order side channel security and mask refreshing[END_REF][START_REF] Coron | Fast evaluation of polynomials over binary finite fields and application to side-channel countermeasures[END_REF]. A masking scheme secure against a t-probing adversary, i.e. who can probe t arbitrary variables in the computation, is indeed secure by design against the class of side-channel attacks of order t [START_REF] Coron | Side channel cryptanalysis of a higher order masking scheme[END_REF].

Most masking schemes consider the implementation to be protected as a Boolean or arithmetic circuit composed of gates of different natures. These gates are then replaced by gadgets processing masked variables. One of the important contributions of [START_REF] Ishai | Private circuits: Securing hardware against probing attacks[END_REF] was to propose a multiplication gadget secure against t-probing attacks for any t, based on a Boolean masking of order n = 2t+1. This was Extended probing-security verification tool. We tackle the limitations of tightPROVE and propose an extended verification tool, that we shall call tightPROVE + . This tool can verify the security of any masked bitslice implementation in the register probing model (which makes more sense than the bit probing model w.r.t. masked software implementations). Given a masked bitslice/nslice implementation composed of standard gadgets for bitwise operations, tightPROVE + either produces a probing-security proof or exhibits a probing attack.

New integrated compiler for masked bitslice implementations. We present (and report on the development of) a new compiler Tornado3 which integrates Usuba and tightPROVE + in a global compiler producing masked bitsliced implementations proven secure in the bit/register probing model. This compiler takes as input a high-level, functional specification of a cryptographic primitive. If some probing attacks are detected by tightPROVE + , the Tornado compiler introduces refresh gadgets, following a sound heuristic, in order to thwart these attacks. Once a circuit has been identified as secure, Tornado produces bitsliced C code achieving register probing security at a given input order. To account for the limited resources available on embedded systems, Tornado exploits a generalization of bitslicing -implemented by Usuba -to reduce register pressure and implements several optimizations specifically tailored for Boolean masking code. The source code of Tornado is available at: https://github.com/CryptoExperts/Tornado Benchmarks of NIST lightweight cryptography candidates. We evaluate Tornado on 11 cryptographic primitives from the second round of the ongoing NIST lightweight cryptography standardization process. 4 The choice of cryptographic primitives has been made on the basis that they were self-identified as being amenable to masking. These implementation results give a benchmark of these different candidates with respect to masked software implementation for a number of shares ranging between 1 and 128. The obtained performances are pretty satisfying. For instance, the n-slice implementations of the tested primitives masked with 128 shares takes from 1 to a few dozen megacycles on an Cortex-M4 processor.

Technical Background

Usuba

Usuba is a domain-specific language for describing bitsliced algorithms. It has been designed around the observation that a bitsliced algorithm is essentially a combinational circuit implemented in software. As a consequence, Usuba's design is inspired by high-level synthesis languages, following a dataflow specification style. For instance, the language offers the possibility to manipulate bit-level quantities as well as to apply bitwise transformations to compound quantities. A domain-specific compiler then synthesizes an efficient software implementation manipulating machine words.

Figure 1 shows the Usuba implementation of the Ascon cipher. To structure programs, we use node's (Figure 1b, 1c & 1d) , of which table's (Figure 1a) are a special case of, specified through their truth table. A node specifies a set of input values, output values as well as a system of equations relating these variables. To streamline the definition of repeating systems (e.g. , the 12 rounds of Ascon), Usuba offers bounded loops, which simply desugar into standalone equations. A static analysis ensures that the system of equations admits a solution. The semantics of an Usuba program is thus straightforward: it is the (unique) solution to the system of equations.

Aside from custom syntax, Usuba features a type system that documents and enforces parallelization strategies. Traditionally, bitslicing [START_REF] Biham | A fast new DES implementation in software[END_REF] consists in treating an m-word quantity as m variables, such that a combinational circuit can be straightforwardly implemented by applying the corresponding bitwise logical operations over the variables. On a 32-bit architecture, this means that 32 circuits are evaluated "in parallel": for example, a 32-bit and instruction is seen as 32 table Sbox(x:v5) returns (y:v5) { 0x4, 0xb, 0x1f, 0x14, 0x1a, 0x15, 0x9, 0x2, 0x1b, 0x5, 0x8, 0x12, 0x1d, 0x3, 0x6, 0x1c, 0x1e, 0x13, 0x7, 0xe, 0x0, 0xd, 0x11, 0x18, 0x10, 0xc, 0x1, 0x19, 0x16, 0xa, 0xf, 0x17 } (a) S-box specified by its truth table.

node AddConstant(state:u64x5,c:u64) returns (stateR:u64x5) let stateR = (state[0,1], state [START_REF] Balasch | On the cost of lazy engineering for masked software implementations[END_REF] ^c, state [3,4]); tel ^(state[0] >>> 28); stateR [1] = state [1] ^(state [1] >>> 61) ^(state [1] >>> 39); stateR [START_REF] Balasch | On the cost of lazy engineering for masked software implementations[END_REF] = state [START_REF] Balasch | On the cost of lazy engineering for masked software implementations[END_REF] ^(state [START_REF] Balasch | On the cost of lazy engineering for masked software implementations[END_REF] >>> 1) ^(state [START_REF] Balasch | On the cost of lazy engineering for masked software implementations[END_REF] >>> 6); stateR [3] = state [3] ^(state [3] >>> 10) ^(state [3] >>> 17); stateR [4] = state [4] ^(state [4] Boolean and gates. To ensure that an algorithm admits an efficient bitsliced implementation, Usuba only allows bitwise operations and forbids stateful computations [START_REF] Mercadier | Usuba: Optimizing & trustworthy bitslicing compiler[END_REF].

However, bitslicing can be generalized to n-slicing [START_REF] Mercadier | Usuba: high-throughput and constant-time ciphers, by construction[END_REF] (with n > 1). Whereas bitslicing splits an m-word quantity into m individual bits, we can also treat it at a coarser granularity 5 , splitting it into k variables of n bits each (preserving the invariant that m = k × n). The register pressure is thus lowered, since we introduce k variables rather than m, and, provided some support from the underlying hardware or compiler, we may use arithmetic operations in addition to the usual Boolean operations. Conversely, certain operations become prohibitively expensive in this setting, such as permuting individual bits. The role of Usuba's type system is to document the parallelization strategy decided by the programmer (e.g. , u64x5 means that we chose to treat a 320-bit block at the granularity of 64-bit atoms) and ensure that the programmer only used operations that can be efficiently implemented on a given architecture.

The overall architecture of the Usuba compiler is presented in Figure 2. It involves two essential steps. Firstly, normalization expands the high-level constructs of the language to a minimal core language called Usuba 0 . Usuba 0 is the software equivalent of a netlist: it represents the sliced implementation in a flattened form, erasing tuples altogether. Secondly, optimizations are applied at this level, taking Usuba 0 circuits to (functionally equivalent) Usuba 0 circuits. In particular, scheduling is responsible for ordering the system of equations in such a way as to enable sequential execution as well as maximize instruction-level parallelism. To obtain a C program from a scheduled Usuba 0 circuit, we merely have to replace the Boolean and arithmetic operations of the circuit with the corresponding C operations. The resulting C program is in static single assignment (SSA) form, involving only operations on integer types: we thus solely rely on the C compiler to perform register allocation and produce executable code. whereas the 64-sliced primitive would have type void Ascon12 (uint64_t plain [START_REF] Barthe | Strong non-interference and type-directed higher-order masking[END_REF], uint64_t cipher [START_REF] Barthe | Strong non-interference and type-directed higher-order masking[END_REF])

Usuba targets C so as to maximize portability: it has been successfully used to deploy cryptographic primitives on Intel, PowerPC, Arm and Sparc architectures. However, a significant amount of optimization is carried by the Usuba compiler: because this programming model is subject to stringent invariants, the compiler is able to perform far-reaching, whole program optimizations that a C compiler would shy away from. For example, it features a custom instruction scheduling algorithm, aimed at minimizing the register pressure of bitsliced code. On high-end Intel architectures featuring Single Instruction Multiple Data (SIMD) extensions, Usuba has demonstrated performance on par with hand-optimized reference implementations [START_REF] Mercadier | Usuba: high-throughput and constant-time ciphers, by construction[END_REF].

Usuba offers an ideal setting in which to automate Boolean masking. Indeed, ciphers specified in Usuba are presented at a suitable level of abstraction: they consist in combinational circuits, by construction. As a result, the Usuba compiler can perform a systematic source-to-source transformation, automating away the tedious introduction of masking gadgets and refreshes. Besides, the high-level nature of the language allows us to extract a model of an algorithm, analyzable by static analysis tools such as SAT solvers -to check program equivalence, which is used internally to validate the correctness of optimizations -or tightPROVE -to verify probing security.

tightPROVE

tightPROVE is a verification tool which aims to verify the probing security of a shared Boolean circuit. It takes as input a list of instructions that describes a shared circuit made of specific multiplication, addition and refresh gadgets and outputs either a probing security proof or a probing attack. To that end, a security reduction is made through a sequence of four equivalent games. In each of them, an adversary A chooses a set of probes P (indices pointing to wires in the shared circuit) in the target circuit C, and a simulator S wins the game if it successfully simulates the distribution of the tuple of variables carried by the corresponding wires without knowledge of the secret inputs.

Game 0 corresponds to the t-probing security definition: the adversary can choose t probes in a t + 1-shared circuit, on whichever wires she wishes. In Game 1, the adversary is restricted to only probe gadget inputs: one probe on an addition or refresh gadget becomes one probe on one input share, one probe on a multiplication gadget becomes one probe on each of the input sharings. In Game 2, the circuit C is replaced by another circuit C that has a multiplicative depth of one, through a transformation called Flatten, illustrated in the original paper [START_REF] Belaïd | Tight private circuits: Achieving probing security with the least refreshing[END_REF]. In a nutshell, each output of a multiplication or refresh gadget in the original circuit gives rise to a new input with a fresh sharing in C . Finally, in Game 3, the adversary is only allowed to probe pairs of inputs of multiplication gadgets. The transition between these games is mainly made possible by an important property of the selected refresh and multiplication gadgets: in addition to being t-probing secure, they are t-strong non interfering (t-SNI for short) [START_REF] Barthe | Strong non-interference and type-directed higher-order masking[END_REF]. Satisfying the latter means that t probed variables in their circuit description can be simulated with less than t 1 shares of each input, where t 1 ≤ t denotes the number of internal probes i.e. which are not placed on output shares.

Game 3 can be interpreted as a linear algebra problem. In the flattened circuit, the inputs of multiplication gadgets are linear combinations of the circuit inputs. These can be modelled as Boolean vectors that we call operand vectors, with ones at indexes of involved inputs. From the definition of Game 3, the 2t probes made by the adversary all target these operand vectors for chosen shares. These probes can be distributed into t + 1 matrices M 0 , . . . , M t , where t + 1 corresponds to the (tight) number of shares, such that for each probe targeting the share i of an operand vector v, with i in {0, . . . , t}, v is added as a row to matrix M i . Deciding whether a circuit is t-probing secure can then be reduced to verifying whether

M T 0 ∩ • • • ∩ M T t
= ∅ (where • denotes the column space of a matrix). The latter can be solved algorithmically with the following high-level algorithm for a circuit with m multiplications:

For each operand vector w,

G i = G i-1 or w ∈ O i .
If this algorithm stops when w ∈ O i for some i, then there is a probing attack on w, i.e., for a certain t, the attacker can recover information on x • w (where x denote the vector of plain inputs), with only t probes on the (t + 1)-shared circuit. In the other two scenarios, the circuit is proven to be t-probing secure for any value of t.

3 Extending tightPROVE to the Register-Probing Model

Model of Computation

Notations. In this paper, we denote by K = F 2 the field with two elements and by V = K s the vector space of dimension s over K, for some given integer s (which will be used to denote the register size). Vectors, in any vector space, are written in bold. i, j denotes the integer interval Z ∩ [i, j] for any two integers i and j. For a finite set X , we denote by |X | the cardinality of X and by x ← X the action of picking x from X independently and uniformly at random. For some (probabilistic) algorithm A, we further denote x ← A(in) the action of running algorithm A on some inputs in (with fresh uniform random tape) and setting x to the value returned by A.

Basic Notions. We call register-based circuit any directed acyclic graph, whose vertices either correspond to an input gate, a constant gate outputting an element of V or a gate processing one of the following functions:

-XOR and AND, the coordinate-wise Boolean addition and multiplication over K s , respectively.

For the sake of intelligibility, we write a + b and a • b instead of XOR(a, b) and AND(a, b) respectively when it is clear from the context that we are performing bitwise operations between elements of V. -(ROTL r ) r∈ 1,s-1 , the family of vector Boolean rotations. For all r ∈ 1, s -1 ,

ROTL r : V → V (v 1 , . . . , v s ) → (v r+1 , . . . , v s , v 1 , . . . , v r )
-(SHIFTL r ) r∈ 1,s-1 and (SHIFTR r ) r∈ 1,s-1 , the families of vector Boolean left and right shifts.

For all r ∈ 1, s -1 ,

SHIFTL r : V → V (v 1 , . . . , v s ) → (v r+1 , . . . , v s , 0, . . . , 0) SHIFTR r : V → V (v 1 , . . . , v s ) → (0, . . . , 0, v 1 , . . . , v s-r )
A randomized circuit is a register-based circuit augmented with gates of fan-in 0 that output elements of V chosen uniformly at random.

Translation to the Masking

World. A d-sharing of x ∈ V refers to any random tuple [x] d = (x 0 , x 1 . . . , x d-1 ) ∈ V d that satisfies x = x 0 + x 1 + • • • + x d-1 . A d-sharing [x] d is uniform if it is
uniformly distributed over the subspace of tuples satisfying this condition, meaning that for any k < d, any k-tuple of the shares of x is uniformly distributed over V k . In the following, we omit the sharing order d when it is clear from the context, so a d-sharing of x is denoted by [x]. We further denote by Enc a probabilistic encoding algorithm that maps x ∈ V to a fresh uniform sharing [x].

In this paper, we call a d-shared register-based circuit a randomized register-based circuit working on d-shared variables as elements of V that takes as inputs some d-sharings [x 1 ], . . . , [x n ] and performs operations on their shares with the functions described above. Assuming that we associate an index to each edge in the circuit, a probe refers to a specific edge index. For such a circuit C, we denote by C([x 1 ], . . . , [x n ]) P the distribution of the tuple of values carried by the wires of C of indexes in P when the circuit is evaluated on

[x 1 ], . . . , [x n ].
We consider circuits composed of subcircuits called gadgets. Gadgets are d-shared circuits performing a specific operation. They can be seen as building blocks of a more complex circuit. We furthermore say that a gadget is sharewise if each output share of this gadget can be expressed as a deterministic function of its input shares of the same sharing index. In this paper, we specifically consider the following gadgets:

-The ISW-multiplication gadget 1. for every 0

≤ i < j ≤ d -1, r i,j ← V; 2. for every 0 ≤ i < j ≤ d -1, compute r j,i ← (r i,j + a i • b j ) + a j • b i ; 3. for every 0 ≤ i ≤ d -1, compute c i ← a i • b i + j =i r i,j . -The ISW-refresh gadget [R] is the ISW-multiplication gadget in which the second operand [b]
is set to the constant sharing (1, 0, . . . , 0), where 0 ∈ V and 1 ∈ V denote the all 0 and all 1 vector respectively.

Security Notions

In this section, we recall the t-probing security originally introduced in [START_REF] Ishai | Private circuits: Securing hardware against probing attacks[END_REF] as formalized through a concrete security game in [START_REF] Belaïd | Tight private circuits: Achieving probing security with the least refreshing[END_REF]. It is based on two experiments described in Figure 3 from [START_REF] Belaïd | Tight private circuits: Achieving probing security with the least refreshing[END_REF] in which an adversary A, modelled as a probabilistic algorithm, outputs of set of t probes P and n inputs x 1 , . . . , x n in a set K. In the first experiment, ExpReal, the inputs are encoded and given as inputs to the shared circuit C. The experiment then outputs a random evaluation of the chosen probes (v 1 , . . . , v t ). In the second experiment, ExpSim, the simulator outputs a simulation of the evaluation Fig. 3: t-probing security game from [START_REF] Belaïd | Tight private circuits: Achieving probing security with the least refreshing[END_REF].

In [START_REF] Belaïd | Tight private circuits: Achieving probing security with the least refreshing[END_REF], the notion of t-probing security was defined for a Boolean circuit, with K = F 2 , that is with x 1 , . . . , x n ∈ F 2 and v 1 , . . . , v t ∈ F 2 . We further refer to this specialized notion as t-bit probing security.

While the notion of t-bit probing security is relevant in a hardware scenario, in the reality of masked software embedded devices, variables are manipulated in registers which contain several bits that leak all together. To capture this model, in this paper, we extend the verification to what we call the t-register probing model in which the targeted circuit manipulates variables on registers of size s for some s ∈ N + and the adversary is able to choose t probes as registers containing values in V = F s 2 . Notice that the t-bit probing model can be seen as a specialization of the t-register probing model with s = 1.

Cautionary note.

In software implementations, we may also face transition leakages, modeled as functions of two -bit variables when they are successively stored in the same register. In that scenario, the masking order t might be halved [START_REF] Balasch | On the cost of lazy engineering for masked software implementations[END_REF][START_REF] Papagiannopoulos | Mind the gap: Towards secure 1st-order masking in software[END_REF]. While specific techniques can be settled to detect and handle such leakages, we leave it for future work and focus on simple register probing model in this paper, in which one observation reveals the content of a single register.

Security Reductions in the Register Probing Model

Just like for the bit-probing version of tightPROVE, the security notions are formalized through games. Similar notions are used which only differ in the fact that the probes in the new model now point to wires of register-based circuits, which carry vectors of V. In this section, we present the differences between the security games in the bit-probing model and the register-probing model. The games are still equivalent to one another, and we give a sketch of proof for each transition (as well as a full proof in the appendix). We then give a description of the linear algebra problem induced by the last game.

Sequence of Games. Similarly to the bit-probing case, Game 0 corresponds to the probing security definition for a register-based circuit, and still features an adversary A that chooses a set of probes P in a circuit C, and a simulator S that wins the game if it successfully simulates

C([x 1 ], . . . , [x n ]) P , for inputs x 1 , . . . , x n ∈ V.
Game 1. In Game 1, the adversary returns a set of probes P = P r ∪ P m ∪ P sw , where |P | = t and the sets P r , P m and P sw contain probes pointing to refresh gadgets' inputs, pairs of probes pointing to multiplication gadgets' inputs and probes pointing to sharewise gadgets' inputs or outputs respectively. C([x 1 ], . . . , [x n ]) P is then a q-tuple for q = 2|P m | + |P r ∪ P sw |. Besides the definition set of variables, the only difference with the bit-probing case stands in the fact that the sharewise gadgets are not restricted to addition gadgets. Game 2. In Game 2, the circuit C is replaced by an equivalent circuit C of multiplicative depth 1, just like in the bit-probing case. The Flatten operation can be trivially adapted to register-based circuits, as the outputs of refresh and multiplication gadgets can still be considered as uniform sharings.

Game 3. In this last game, the adversary is restricted to only position its t probes on multiplication gadgets, i.e. A returns a set of probes P = P r ∪ P m ∪ P sw such that P sw = P r = ∅ and P = P m . C([x 1 ], . . . , [x n ]) P thus returns a q-tuple for q = 2t since all the elements in P are pairs of inputs of multiplication gadgets.

Theorem 1. Let C be a shared circuit. We have the following equivalences: ∀A 0 , ∃S 0 , S 0 wins Game 0. ⇐⇒ ∀A 1 , ∃S 1 , S 1 wins Game 1.

⇐⇒ ∀A 2 , ∃S 2 , S 2 wins Game 2.

⇐⇒ ∀A 3 , ∃S 3 , S 3 wins Game 3.

For the sake of clarity, we define one lemma per game transition. The corresponding proofs are available in Appendix A, but an informal reasoning that supports these ideas is given in the following, as well as the differences with the proofs established in [START_REF] Belaïd | Tight private circuits: Achieving probing security with the least refreshing[END_REF].

Lemma 1. ∀A 0 , ∃S 0 , S 0 wins Game 0. ⇐⇒ ∀A 1 , ∃S 1 , S 1 wins Game 1.
Proof (sketch). The proof for the first game transition is based on the fact that multiplication and refresh gadgets are t-SNI gadgets, and that each probe on such gadgets can be replaced by at most one probe on each input sharing. The reason why this still works in the new model is that the ISW multiplication and refresh gadgets are still SNI for register-based circuits performing bitwise operations on V. This transition can thus be reduced to the original transition.

Lemma 2. ∀A 1 , ∃S 1 , S 1 wins Game 1. ⇐⇒ ∀A 2 , ∃S 2 , S 2 wins Game 2.
Proof (sketch). The proof for the second game transition relies on the fact that just as the output of a Boolean multiplication gadget is a random uniform Boolean sharing, independent of its input sharings, the outputs of the multiplication gadgets we consider can be treated as new, fresh input encodings. Thus, a circuit C is t-probing secure if and only if the circuit C = Flatten(C) is t-probing secure. Lemma 3. ∀A 2 , ∃S 2 , S 2 wins Game 2. ⇐⇒ ∀A 3 , ∃S 3 , S 3 wins Game 3.

Proof (sketch). A cross product of shares a i • b j carries informations on both shares a i and b j , as each of the s slots in the cross product carries information about each share. Thus, placing probes on multiplication gadgets only is optimal from the attacker point of view. The complete proof for Lemma 3 makes use of formal notions which are introduced in the next paragraph.

Translation to Linear Algebra. From now on, the column space of a matrix M is denoted by M and the column space of the concatenation of all the matrices in a set E is denoted by E .

From Lemma 1 and Lemma 2, checking the t-probing security of a shared circuit C has been reduced to verifying the t-probing security of a shared circuit C = Flatten(C), for which the attacker is restricted to use probes on its multiplication and refresh gadgets' inputs. We can translate this problem into a linear algebra problem that we can solve algorithmically. In the following, let us denote by x i,j ∈ V the j th share of the i th input sharing

[x i ], so that ∀i ∈ 1, N , [x i ] = (x i,0 , x i,1 , . . . , x i,t ) ∈ V t+1
We also denote by x ||j the concatenation of the j th shares of the input sharings:

∀j ∈ 0, t , x ||j = x 1,j ||x 2,j || . . . ||x N,j ∈ K sN The probed variables in the flattened circuit C form a q-tuple (v 1 , . . . , v q ) = C ([x 1 ], . . . , [x N ]) P .
It can be checked that all these variables are linear combinations of inputs shares' coordinates since (1) the circuit C has a multiplicative depth of one, (2) the adversary can only place probes on inputs for multiplication and refresh gadgets, and (3) other types of gadgets are linear. Since the gadgets other than multiplication and refresh are sharewise, we can assert that for every k ∈ 1, q , there exists a single share index j for which v k only depends on the j th share of the input sharings and thus only depends on x ||j . Therefore there exists a Boolean matrix A k ∈ K sN ×s , that we refer to as a block from now on, such that

v k = x ||j • A k ∈ V.
Let us denote by v ||j the concatenation of all n j probed variables v i with i ∈ 1, q such that v i only depends on share j. Similarly, we denote by M j ∈ K sN ×snj the matrix obtained from the concatenation of all the corresponding blocks A i (in the same order). We can now write

v ||0 = x ||0 • M 0 , v ||1 = x ||1 • M 1 , . . . , v ||t = x ||t • M t
which leads us to the following proposition. [x N ]) P can be perfectly simulated if and only if the M j matrices satisfy

Proposition 1. For any (x 1 , . . . , x N ) ∈ V N , the q-tuple of probed variables (v 1 , . . . , v q ) = C([x 1 ], [x 2 ],. . . ,
M 0 ∩ M 1 ∩ • • • ∩ M t = ∅ .
Proof. Let us denote by x = (x 1 x 2 . . . x N ) the concatenation of all the inputs. We split the proof into two parts to handle both implications.

From left to right. Let us assume that there exist a non-null vector w ∈ K sN and vectors

u 0 ∈ K sn0 , . . . , u t ∈ K snt that verify w = M 0 • u 0 = • • • = M t • u t .
This implies the following sequence of equalities:

t j=0 v ||j • u j = t j=0 x ||j • M j • u j = t j=0 x ||j • w = x • w
which implies that the distribution of (v 1 , . . . , v q ) depends on x, and thus cannot be perfectly simulated.

From right to left. Since the sharings [x 1 ], . . . , [x N ] are uniform and independent, the vectors x ||1 , . . . , x ||t are independent uniform random vectors in K sN , and can thus be perfectly simulated without the knowledge of any secret value. As a direct consequence, the distribution of (v ||1 , . . . , v ||t ) can be simulated. From the definition v ||0 = x ||0 • M 0 , each coordinate of v ||0 is the result of a product x ||0 • c where c is a column of M 0 . By assumption, there exists j ∈ {1, . . . , t} such that c / ∈ M j . Since x ||1 , . . . , x ||t are mutually independent,

x ||j •c is a random uniform bit independent of x ||1 • M 1 , . . . , x ||j-1 • M j-1 , x ||j+1 • M j+1 , . . . , x ||t • M t , and since c / ∈ M j , it is also independent of x ||j • M j . This means that x ||j • c is a random uniform bit independent of v ||1 , . . . , v ||t , and so is x ||0 • c, as x ||0 • c = x ||j • c + (x ||1 • c + • • • + x ||j-1 • c + x ||j+1 • c + • • • + x ||t • c + x • c). Since v ||0 = x ||0 • M 0 ,
we can then perfectly simulate v ||0 . As a result, (v 1 , . . . , v q ) can be perfectly simulated.

Verification in the Register Probing Model

In this section, we present a method based on Proposition 1 that checks whether a (t + 1)-shared circuit C achieves t-register probing security for every t ∈ N * . We start by introducing some notations and formalizing the problem, then we give a description of the aforementioned method, along with a pseudocode of the algorithm. The method is finally illustrated with some examples.

Formal Definitions. Now that the equivalence between the t-register probing security game was proven to be equivalent to Game 3, in which the adversary can only probe variables that are inputs of multiplication gadgets in a flattened circuit C , we formally express the verification of the t-register probing security as a linear algebra problem. For a given multiplication gadget of index g, let us denote by [a g ] and [b g ] its input sharings, i.e.

[a g ] = (x ||0 • A g , . . . , x ||t • A g ) and [b g ] = (x ||0 • B g , . . . , x ||t • B g )
for some constant blocks A g and B g that we now call operand blocks. The adversary outputs a set of t pairs of probes P = {(p 1 1 , p For all j ∈ 0, t , we define the matrix M j as the concatenation of all the blocks corresponding to probed shares of share index j. By Proposition 1, there is a register probing attack on C if and only if

t i=0 M j = ∅.
For an attack to exist, the matrices must be non-empty, and since these matrices contain 2t blocks, at least one of them is made of a single block D that belongs to the set of operand blocks {A g , B g } g .

We can now say that there exists a register probing attack on C if and only if there exists a non-empty subspace S of K sN such that S = t i=0 M j ⊆ D . In that case, there is an attack on the subset S that we now refer to as the attack span. tightPROVE + . When s = 1 (i.e., in the t-bit probing model case), the dimension of S = t i=0 M j is at most 1, so checking whether an operand block W leads to an attack or not reduces to verifying whether there exists a set of probes for which S = W . However, for s > 1, there can be many possible subspaces of W for an operand block W , so that any non-null subspace of W ∩ S leads to an attack. That is why the new method not only has to determine whether there is an attack, but also which subsets of W could possibly intersect with the attack span S.

Our method loops over all the operand blocks W ∈ {A g , B g } g of multiplication gadgets and checks whether there is a probing attack on a subset of W . For each W ∈ {A g , B g } g , we create a layered directed acyclic graph G W for which each node is associated with a permissible attack span that represents the subspace of W in which an attack could possibly be found. The permissible attack span in a node is a subset of the permissible attack span in its parent node. Each node is indexed by a layer number i and a unique index b. Besides, the permissible attack span denoted S i,b , the node contains some information in the form of three additional sets

G i,b , O i,b and Q i,b . G i,b
is a list of multiplication gadgets which could be used to find an attack. Q i,b contains the operand blocks of the multiplications in G i,b that can be combined with other operands to obtain elements of W . And then O i,b , called the set of free operand blocks, contains the other operand blocks of G i,b . If there is a way to combine free operands to obtain an element of W , then a probing attack is found.

We start with the first node root. We assign to S 1,root the span W , to G 1,root the set of multiplications for which W is an operand and to Q 1,root the operand W . O 1,root can then be deduced from G 1,root and Q 1,root :

       S 1,root = W G 1,root = {g | A g = W } ∪ {g | B g = W } O 1,root = {B g | A g = W } ∪ {A g | B g = W } Q 1,root = {W } At each step i (from i = 1) of the algorithm, for each node b in the i th layer, if S i,b ∩ O i,b = ∅,
the method stops and returns False: the circuit is not tight t-register probing secure for any t. If not, for each node b in the i th layer, for each operand block

A ∈ {A g , B g } g \Q i,b , if S i,b ∩( A + O i,b ) = ∅ (where A + O i,
       S i+1,b = S i,b ∩ ( A + O i,b ) G i+1,b = G i,b ∪ {g | A is an operand block of the multiplication gadget g} O i+1,b = O i,b ∪ {B | A is a co-operand block of B in a multiplication gadget} Q i+1,b = Q i,b ∪ {A}
If no new node is created at step i, then the algorithm stops and returns True: the circuit is tight t-register probing secure for any t. The method eventually stops, as the number of nodes we can create for each graph is finite. Indeed, at each step i, each node b can only produce |{A g , B g } g | -|Q i,b | new nodes, and for each of them the set Q grows by one. In total, each graph can contain up to (|{A g , B g } g | -1)! nodes.

The pseudocode of Algorithm 1 gives a high-level description of our method. In this algorithm, each edge on the graph corresponds to adding an operand in Q. Multiple operands can be added at once if the corresponding permissible attack span is the same for all of those operands. For the sake of simplicity, we decide to omit this optimization in the algorithm.

*/ S1,root = W G1,root = {g | Ag = W } ∪ {g | Bg = W } O1,root = {Bg | Ag = W } ∪ {Ag | Bg = W } Q1,root = {W } foreach step i do foreach branch b in layer i do if S i,b ∩ O i,b = ∅ then return False; end foreach branch b in layer i do foreach operand A / ∈ Q i,b do if S i,b ∩ ( A + O i,b ) = ∅ then /* add new branch b */ S i+1,b = S i,b ∩ ( A + O i,b ) G i+1,b = G i,b ∪ {g | A is an operand of the mult. gadget g} O i+1,b = O i,b ∪ {B | A is an operand of a mult. gadget} Q i+1,b = Q i,b ∪ {A} end end end end end return True Proposition 2. Algorithm 1 is correct.
Proof (sketch). The proof is organized in two parts. First, we show that there are no false negatives: if the algorithm returns False, then there is a probing attack on the input circuit C. This is done with a constructive proof. Assuming that the algorithm returns False, we construct from the graph a set of matrices (as defined in section 3.3) such that the intersection of their images is non-empty. Then we prove that there are no false positives by showing that if there is a probing attack on a circuit C, then the algorithm cannot stop as long as no attack is found. Since the algorithm has been proven to terminate, it must return False.

The complete proof is provided in Appendix B.

Complete Characterization. The verification algorithm can be slightly modified to output all the existing t-register probing attack paths on the input circuit. This extension mostly amounts to continuing to add new nodes to the graph even when an attack has been detected until no new node can be added, and slightly changing the condition to add a node. The new condition can be written S i,b ∩ ( A * + O i,b ) = ∅, where A * denotes the set of non-null vectors of the column space of A. And with this, it is possible to determine the least attack order, which is the least amount of probes t min that can be used to recover a secret value in a (t min + 1)-shared circuit.

Toy example. We illustrate tightPROVE + on a toy example. The flattened circuit is displayed on Figure 4 (the extended inputs are omitted for clarity as they do not have any impact on the circuit). It uses 3-bit registers and it is made of a bitwise operation layer (BOL) that takes 4 inputs x 1 , x 2 , x 3 , x 4 and produces 7 vectors a, b, e, w, f, c, d ∈ V, plus a single layer of multiplications. In the figure, the aforementioned variables are denoted by I 1 , I 2 , I 3 , I 4 and A, B, E, W, F, C, D, their corresponding blocks. The values we chose for those blocks are:

A =                   1 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 1                   B =                   0 0 1 0 0 0 0 0 1 1 0 1 0 1 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0                   C =                   0 0 0 1 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 1                   D =                   1 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 1 0 1 0 0 0 0 0 0 0 0 0                   E =                   0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 1 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0                   F =                   0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 1 0 0 0 1 0 0 0                   W =                   1 0 0 1 1 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1                   I1 I2 I3 I4 BOL A B E W F C D [⊗] [⊗] [⊗] [⊗]
Fig. 4: Graph representation of the example circuit C.

Two graphs are displayed in Figure 5 to illustrate our algorithm working on operands W and F . Operand F. The algorithm starts by creating the node root. Without any constraint yet, the permissible attack span S 1,root is initialized to F . G 1,root contains the only multiplication for which F is a block operand: (F, W ). The set of used operands Q 1,root contains F , and thus the set of free operands O 1,root only contains one operand block, W . All in one, the root node is built as follows:

       S 1,root = F G 1,root = {(F, W )} O 1,root = {W } Q 1,root = {F }
Since F ∩ W = ∅, and the current permissible attack span is not empty, new nodes are investigated to be added to the graph. Denoting by a 1 , a 2 , a 3 the 3 column vectors of A, b 1 , b 2 , b 3 the 3 column vectors of B and so on, we have

F ∩ ( A + W ) = f 3 = ∅ because f 3 = a 2
and it is clear that we cannot obtain f 1 or f 2 from column vectors of W and A.

We also have

F ∩ ( C + W ) = f 3 = ∅ (f 3 = c 2 )
and

F ∩ ( D + W ) = f 1 = ∅ (f 1 = d 1 + w 1 + w 2 ).
The other intersections being empty, 3 new nodes are connected to the root one:

       S 2,A = f 3 G 2,A = {(F, W ), (A, B)} O 2,A = {W, B} Q 2,A = {F, A}        S 2,C = f 3 G 2,C = {(F, W ), (C, D)} O 2,C = {W, D} Q 2,C = {F, C}        S 2,D = f 1 G 2,D = {(F, W ), (D, C)} O 2,D = {W, C} Q 2,D = {F, D}
None of the permissible attack spans in this new layer intersects with their set of free block operands, and none are empty, so the algorithm tries to find new nodes to add to each of them.

No new node can be found for the last one, as f 1 cannot be obtained with column vectors of blocks of O 2,D and other block operands that are not in Q 2,D . For the first two nodes, however, we have

S 2,A ∩ ( C + O 2,A ) = f 3 = ∅ and S 2,C ∩ ( A + O 2,C ) = f 3 = ∅,
so new nodes are created:

       S 3,AC = f 3 G 3,AC = {(F, W ), (A, B), (C, D)} O 3,AC = {W, B, D} Q 3,AC = {F, A, C}        S 3,CA = f 3 G 3,CA = {(F, W ), (C, D), (A, B)} O 3,CA = {W, D, B} Q 3,CA = {F, C, A}
None of the permissible attack spans in this last layer intersects with their corresponding set of free block operands, and none leads to the creation of new nodes, which is why the algorithm ends the creation of this graph and goes on to the next one.

Operand W. Since the first steps are similar to the previous example, only the steps that lead to an attack are detailed hereafter. The full graph can be found in Figure 5 in which red circles denote nodes where an attack is found. We detail the construction of the nodes on the path displayed with a double arrow. The algorithm starts by creating the root node:

       S 1,root = W G 1,root = {(W, E), (W, F )} O 1,root = {E, F } Q 1,root = {W }
As W ∩ {E, F } = ∅, the algorithm searches for new nodes to add. Since

W ∩ ( B + {E, F } ) = w 1 + w 2 = ∅ (w 1 + w 2 = b 1 + b 3 + e 1 ),
the following node is created:

       S 2,B = w 1 + w 2 G 2,B = {(W, E), (W, F ), (B, A)} O 2,B = {E, F, A} Q 2,B = {W, B}
There is still no attack at this point, as w 1 + w 2 / ∈ {E, F, A} . However,

w 1 + w 2 ∩ ( D + {E, F, A} ) = w 1 + w 2 = ∅ (w 1 + w 2 = d 1 + f 1 ),
so the following node is created:

       S 3,BD = w 1 + w 2 G 3,BD = {(W, E), (W, F ), (B, A), (D, C)} O 3,BD = {E, F, A, C} Q 3,BD = {W, B, D}
This time, we have w 1 + w 2 ∈ {E, F, A, C} , as w 1 + w 2 = a 1 + c 1 . Thus there exists a register probing attack, and the algorithm returns False.

Let us now go one step further by showing that this circuit is not tight t-register probing secure for any t ≥ 4. We assume that the circuit is d-shared with d ≥ 5, and denote by w i,j the i th coordinate of the j th share of [w], by a i,j the i th coordinate of the j th share of [a] and so on. By probing the multiplications (A, B), (C, D), (W, E) and (W, F ), an attacker can get the values of a 1,0 , b 1,1 , b 3,1 with a probe on (A, B) targeting shares 0 for A and 1 for B, c 1,0 , d 1,2 with a probe on (C, D) targeting shares 0 for C and 2 for D, w 1,3 , w 2,3 , e 1,1 with a probe on (W, E) targeting shares 3 for W and 1 for E, w 1,4 , w 2,4 , f 1,2 with a probe on (W, F ) targeting shares 4 for W and 2 for F .

With those values, one can compute:

w 1,0 + w 2,0 = a 1,0 + c 1,0 w 1,1 + w 2,1 = b 1,1 + b 3,1 + e 1,1 w 1,2 + w 2,2 = d 1,2 + f 1,2 w 1,3 + w 2,3 w 1,4 + w 2,4
With 4 probes, an attacker can thus get the sum of the first two coordinates of 5 shares of w, i.e., the circuit is not tight t-register probing secure for t ≥ 4.

Concrete Example

. We now present an example that shows how tightPROVE + applies to reallife implementations of cryptographic primitives. We take as example an Usuba implementation of the Gimli [START_REF] Daniel | Gimli : A cross-platform permutation[END_REF] cipher, a 384-bit permutation, with 32-bit registers. When applying tightPROVE + on this circuit, register probing attacks are identified. Let us describe one of them and display the subgraph of the circuit it is based on in Figure 6.

The subcircuit uses 5 input blocks I 1 , I 2 , I 3 , I 4 , I 5 . We denote by [x] the sharing obtained after the rotation of I 2 and [y] the one after the rotation of I 1 . By probing the multiplication g 1 , one can get the values x 32,0 and y 32,1 (the first index denotes the bit slot in the register and the second one denotes the share). Due to the left shifts, one can get the values x 32,2 and x 32,1 + y 32,1 by probing g 2 . The following values can thus be obtained: x 32,0 , x 32,1 = (x 32,1 + y 32,1 ) + y 32,1 , and x 32,2 . This implies that x 32 , the last slot of the secret value x, can be retrieved with t probes when the circuit is (t + 1)-shared for any t ≥ 2.

Tornado: Automating Slicing & Masking

Given a high-level description of a cryptographic primitive, Tornado synthesizes a masked implementation using the ISW-based multiplication and refresh gadgets. The gadgets are provided as C functions, presented in Figure 7 and where the macro MASKING_ORDER is instantiated at compile time to the desired masking order. The key role of Usuba is to automate the generation of a sliced implementation, upon which tightPROVE + is then able to verify either the bit probing or register probing security, or identify the necessary refreshes. By integrating both tools, we derive a masked implementation from the sliced one. This is done by mapping linear operations over all shares, by using isw_mult for bitwise and operations and by calling isw_refresh where necessary.

I1 I2 I3 I4 I5 [≪9] [≪24] [ 1] [ 1] [ 2] [⊗] g1 [⊕] [⊕] [⊕] [≪9] [⊕] [⊗] g2
Fig. 6: Graph representation of a sub-circuit of Gimli. The overall architecture of the Tornado compiler is shown in Figure 8. It consists essentially in the integration of Usuba and tightPROVE + within a single, unified framework. This integration is reasonably simple since the Usuba 0 intermediate representation amounts essentially to a registerbased circuit extended with a notion of function node (for code reuse), whereas the input language of tightPROVE + consists in unrolled inlined register-based circuits. We therefore easily obtain an input suitable for tightPROVE + by inlining all the nodes within the Usuba 0 generated by Usuba. We also need to specify the probing model to use when carrying the analysis in tightPROVE + : this corresponds exactly to the typing information specified in Usuba, whether we are considering a bitsliced implementation (in which case we select the bit probing model), or an n-sliced implementation (in which case we select the register probing model, registers whose size is m). Having sent a register-based circuit to the extended tool tightPROVE + , it may either be accepted as-is or tightPROVE + may have identified necessary refresh points to achieve bit or register probing security. In the latter case, Tornado maps these refresh points back into the initial, noninlined Usuba 0 code: each refresh point is turned into a custom refresh operator that is treated specifically by the Tornado backend (in particular, it cannot be optimized out). Upon emitting C code, this operator turns into a call to the isw_refresh gadget of Figure 7.

Addition of Refresh Gadgets

In order to make the generation of secure masked implementations fully automatic, we use heuristic methods to determine a set of operands to be refreshed in order to make the resulting circuit secure in the considered probing model.

When a circuit is built from the combination of several instances of the same subcircuit, the description of the subcircuit is analyzed first, assuming that it has random, uniform and independent inputs. If probing attacks are found, an exhaustive search of the placement of refresh gadgets can be done if the size of the subcircuit is not too big. The same placement of refresh is then applied every time this subcircuit appears. Doing so is relevant, as any attack that can be done on a subfunction alone also exists when that subfunction is part of a wider circuit.

Then, tightPROVE + verifies that the resulting circuit is secure. If probing attacks are still found, then tightPROVE + is called in full characterization mode which yields the complete list of multiplications involved in each attack. We then select an operand of the multiplication that appears the most in that list, and apply a refresh to this operand. This step is repeated until no more attacks can be found. This method is bound to stop and yield a secure circuit since, as proven in the original paper describing tightPROVE, refreshing one input per multiplication guarantees that the resulting circuit is secure.

We stress that this method is not optimal in the sense that it does not always find the minimal number of refresh gadgets needed to make a circuit secure, but it provides a sound heuristic. Finding an optimal and efficient method to place refresh gadgets is left open for future research.

Optimizations

Whereas this compilation scheme is functionally sufficient to guarantee security, further optimizations are beneficial to make it scale to large masking orders on a typical embedded platform. Tornado therefore integrates a modicum of optimizations to optimize stack usage (especially for bitsliced implementations), to reduce the overhead of repeatedly iterating over shares and to minimize the number of masked multiplications. Note that the objective of the present work is not to demonstrate best-in-class performance results: we are instead interested in 1. the asymptotic performance of a given primitive across a sizable choice of masking orders; and 2. the comparative performance of sizable number primitives at a given masking order.

To this end, Tornado has proved to be a valuable tool. We enable the first point by minimizing the impact that the C compiler can have on the quality (or lack thereof) of the resulting code. For example and as the masking order grows, the compiler tends to shy away from certain looprelated optimizations that are beneficial. We therefore systematically carry these optimizations in Tornado. We enable the second point by subjecting all the primitives to the same, predictable (even if imperfect) compilation process tailored to the platform of interest.

We have therefore identified two optimizations that are necessary to scale to large masking orders: aggressive constant propagation for multiplications and loop fusion. Masked multiplication being expensive, we strive to spot the case where the operand of a multiplication is in fact a constant value. We do so through a constant propagation analysis in Usuba 0 followed by a specific compilation rule in this case: we directly multiply all the shares with the constant.

To mask a sequence of instructions, Tornado replaces each of them with a masked gadget. Gadgets for linear operations consist in a loop applying iteratively a basic operation over each share, such as for (int i=0; i<=MASKING_ORDER; i++) A(i); for (int i=0; i<=MASKING_ORDER; i++) B(i); for (int i=0; i<=MASKING_ORDER; i++) C(i);

where A, B and C are linear operations storing their results in a number of variables linear with MASKING_ORDER. As a result, stack usage increases linearly with the masking order, which means that, when considering implementations as register-hungry as bitslicing ones, even small masking orders can be too heavy. Besides, operating each loop (increment, comparison, branching) impedes an overhead that the C compiler is something heuristically willing to optimize out at small orders, leading to confusing threshold effects when benchmarking. To address both issues, we systematically perform loop fusion, thus obtaining for (int i=0; i<=MASKING_ORDER; i++) { A(i); B(i); C(i); } on the above example, followed by instruction scheduling, which will strive to reduce the live range [START_REF] Mercadier | Usuba: high-throughput and constant-time ciphers, by construction[END_REF] (and thus the number of temporaries) of, for example, the variables set in A and used in B.

This optimization allows us to reduce stack usage of our bitsliced implementations by 11kB on average whereas this saves us, on average, 3kB of stack for our n-sliced implementations (recall that our platform offers a measly 96kB of SRAM). It also positively impacts performance, with a 16% average speedup for bitslicing and a 21% average speedup for n-slicing.

Evaluation

We evaluated Tornado on 11 cryptographic primitives from the second round of the NIST lightweight cryptography competition 6 . The choice of cryptographic primitives was made on the basis that they were self-identified as being amenable to masking. We stress that we do not focus on the full authenticated encryption, message authentication, or hash protocols but on the underlying primitives, mostly block ciphers and permutations.

Table 1 provides an overview of these primitives. Whenever possible, we generate both a bitsliced and an n-sliced implementation for each primitive, which allows us to exercise the bit-probing and the register-probing models of tightPROVE + . However, 4 primitives do not admit a straightforward n-sliced implementation. The Subterranean permutation involves a significant amount of bit-twiddling across its 257-bit state, which makes it a resolutely bitsliced primitive (as confirmed by its reference implementation). Photon, Skinny, Spongent rely on lookup tables that would be too expansive to emulate in n-sliced mode. In bitslicing, these tables are simply implemented by their Boolean circuit, either provided by the authors (Photon, Skinny) or generated through SAT [START_REF] Ko Stoffelen | Optimizing s-box implementations for several criteria using SAT solvers[END_REF] with the objective of minimizing multiplicative complexity (Spongent, with 4 ANDs and 28 XORs). Spook and Elephant respectively rely on the Clyde and Spongent primitives, which we therefore include in our evaluation.

Note that the n-sliced implementations, when they exist, are either 32-sliced or 64-sliced. This means in particular that, unlike bitslicing that processes multiple blocks in parallel, these implementations process a single block at once on our 32-bit Cortex M4.

In Subsection 5.1, we present the results of tightPROVE + on the considered primitives using the refresh placement strategy explained in Subsection 4.1. Finally, we benchmark our unmasked implementations against reference implementations in Subsection 5.2, and compare their masked versions in Subsection 5.3.

tightPROVE +

Table 2 contains the results of tightPROVE + for the aforementioned primitives. We display the output of our algorithm for each circuit, along with the size of the registers used and the time it takes for tightPROVE + to output the results. Table 3 provides additional information about the implementations that are not secure in the register probing model. This includes the size of the registers, the time it takes to find the first attack, the time it takes to find all the operands that can be retrieved, then the least attack order, the optimal number of refresh gadgets needed to make the implementation secure in the register probing model, and finally the time tightPROVE + takes to verify that the refreshed implementation is indeed secure. All calculations were made on an iMac with an intel Core i7 processor (4 GHz) and 16 GB of DDR3 RAM (1600 MHz), with parallel computing on its 8 CPUs. Following the method described in Section 4.1, tightPROVE + places refresh gadgets for the considered implementations of Ace, Clyde and Gimli. For the two first primitives, there is exactly one subcircuit which is responsible for the identified register probing attacks, which can be fixed by adding only one refresh gadget. This gives us a lower bound for the optimal number of refresh gadgets, and since tightPROVE + does not find any further attack after the addition of refresh gadgets, it is also an upper bound. Gimli, however, is made of 6 subsequent identical subcircuits that are subject to register probing attacks, but the method uses 20 refresh gadgets per subcircuits to make the implementation secure. We can thus only conclude that we have an upper bound of 120 for the optimal number of gadgets, and that it is a multiple of 6, but in the current method, we cannot ascertain that it is optimal without setting up an exhaustive search.

Baseline Performance Evaluation

In the following, we benchmark our implementations -in Usuba and compiled with Tornadoof the NIST submissions against the reference implementation provided by the contestants. This allows us to establish a performance baseline (without masking), thus providing a common frame of reference for the performance of these primitives based on their implementation synthesized from Usuba. In doing so, we have to bear in mind that the reference implementations provided by the NIST contestants are of varying quality: some appear to have been finely tuned for performance while others focus on simplicity, acting as an executable specification.

In an effort to level the playing field, we ran our benchmark on an Intel i5-6500 @ 3.20GHz, running Linux 4.15.0-54. The implementations were compiled with Clang 7.0.0 with flags -O3 -fno-slp-vectorize -fno-vectorize. These flags prevent Clang from trying to produce vectorized code, which would artificially advantage some implementations at the expense of others because of brittle, hard-to-predict vectorization heuristics. Besides, vectorized instructions remain an exception in the setting of embedded devices (e.g. , Cortex M). At the exception of Subterranean (which is bitsliced), the reference implementations follow a n-sliced implementation pattern, representing the state of the primitive through a matrix of 32-bit values, or 64-bit in the case of Ascon. To evaluate bitsliced implementations, we simulate a 32-bit architecture, meaning that the throughput we report corresponds to the parallel encryption of 32 independent blocks.

The results are shown in Table 4. We notice that Usuba often delivers performance that is on par or better than the reference implementations. Note that this does not come at the expense of intelligibility: our Usuba implementations are written in a high-level language, which is amenable to formal reasoning thanks to its straightforward semantic model (unlike any implementation in C). The reference implementations of Skinny and Photon use lookup tables, which do not admit a straightforward implementation in terms of constant-time, combinational operations. As a result, we are unable to implement a constant-time n-sliced version in Usuba and to, in Section 5.3, mask such an implementation. We now turn our attention specifically to a few implementations that exhibit interesting performance with the following observations:

-The reference implementation of Subterranean is an order of magnitude slower than in Usuba because its implementation is bit-oriented (each bit is stored in a distinct 8-bit variable) but only a single block is encrypted at a time. Switching to 32-bit variables and encrypting 32 blocks in parallel, as Usuba does, significantly improves performance.

-The reference implementation of Spongent is slowed down by a prohibitively expensive bitpermutation over 160 bits, which is spread across 20 8-bit variables. Thanks to bitslicing, Usuba turns this permutation into a purely static renaming of variable, which occurs purely at compile-time.

-On Ascon, our n-sliced implementation is twice slower than the reference implementation. Unlike the reference implementation, we have refrained from performing aggressive function inlining and loop unrolling to keep code size in check, since we target embedded systems. However, if we instruct the Usuba compiler to perform these optimizations, the performance of our n-sliced implementation is on par with the reference one.

-Ace reference implementation suffers from significant performance issues, relying on an excessive number of temporary variables to store intermediate results.

-Finally, Gimli offers two reference implementations, one being a high-performance SSE implementation with the other serving as an executable specification on general-purpose registers.

We chose the general-purpose one here (which had not been subjected to the same level of optimizations) because our target architecture (Cortex M) does not provide a vectorized instruction set.

Masking Benchmarks

We now turn to the evaluation of the masked implementations produced by Tornado using the Usuba implementations presented in the previous section. Our benchmarks are run on a Nucleo STM32F401RE offering an Arm Cortex-M4 with 512 Kbytes of Flash memory and 96 Kbytes of SRAM. We used the GNU C compiler arm-none-eabi-gcc version 9.2.0 at optimization level -O3.

We considered two modes regarding the Random Number Generator (RNG):

-Pooling mode: The RNG generates random numbers at a rate of 32 bits every 64 clock cycles. Fetching a random number can thus take up to 65 clock cycles. -Fast mode: The RNG only takes a few clock cycles to generate a 32-bit random word. The RNG routine thus can simply read a register containing this 32-bit random word without checking for its availability.

Those two modes were chosen because they are the ones used in the submission of Pyjamask, which is the only submission detailing the question of how to get random numbers for a masked implementation. Of these 11 NIST submissions, only Pyjamask provides a masked implementation. Our implementation is consistently (at every order, and with both the pooling and fast RNGs) 1.8 times slower than their masked implementation. The reason is twofold. First, their reference implementation has been heavily optimized to take advantage of the barrel shifter on the Cortex M4, which we do not exploit. Second, our implementation uses the generic ISW multiplication (Figure 7) whereas the reference implementation employs a specialized, hand-tuned implementation in assembly.

n-sliced implementations. Table 5a gives the performances of the n-sliced implementations produced by Tornado in terms of cycles per byte. Note that these implementations are provably secure, with refreshing gadgets being inserted if necessary. Since masking a multiplication has a quadratic cost in the number of shares, we expect performance at high orders to be mostly proportional with the number of multiplications used by the primitives. We thus report the number of multiplications involved in our implementation normalized to the block size (in bytes) of the primitive. This is confirmed by our results with 128 shares (on the Cortex M4). This effect is less pronounced at small orders since the execution time remains dominated by linear operations. Using the pooling RNG increases the cost of multiplications compared to the fast RNG, which results in performances being proportional to the number of multiplications at smaller order than with the fast RNG.

Pyjamask illustrates the influence of the number of multiplications on scaling. Because of its use of dense binary matrix multiplications, it involves a significant number of linear operations for only a few multiplications. As a result, it is slower than Gimli and Ace at order 3, despite the fact that they use respectively 2× and 6× more multiplications. With the fast RNG, the inflection point is reached at order 7 for Ace and order 31 for Gimli, only to improve afterward. Similarly when compared to Clyde, Pyjamask goes from 5× slower at order 3 to 50% slower at order 127 with the fast RNG and 20% slower at order 127 with the pooling RNG. The same analysis applies to Gift and Ace, where the linear overhead of Gift is only dominated at order 63 with the pooling RNG and at order 127 with the fast RNG.

One notable exception is Ascon with the fast RNG, compared in particular to Xoodoo and Clyde. Whereas Ascon uses a smaller number of multiplications, it involves a 64-sliced implementation (Table 1), unlike its counterparts that are 32-sliced. Running on our 32-bit Cortex-M4 requires GCC to generate 64-bit emulation code, which induces a significant operational overhead and prevents further optimization by the compiler. When using the pooling RNG however, Ascon is faster than both Xoodoo and Clyde at every order, thanks to its smaller number of multiplications.

For scenarios in which one is not interested in encrypting a lot of data but rather a single block, possibly short, then it makes more sense to look at the performances of a single run of a cipher, rather than its amortized performances over the amount of bytes it encrypts. This is shown in Table 5b. The ciphers that use the least amount of multiplications have the upper hand when masking order increases: Clyde is clearly the fastest primitive at order 127, closely followed by Pyjamask. Ascon, which is the fastest one when looking at the cycles/bytes actually owns its performances to his low number of multiplications compared to its 320-bit block size. Therefore, when looking at a single run, it is actually 1.7× slower than Clyde at order 127. Similarly, Xoodoo performs well on the cycles/bytes metric, but has a block size of 384 bits, making it 2.5× slower.

Bitsliced implementations.

The key limiting factor to execute bitslice code on an embedded device is the amount of memory available. Bitsliced programs tend to be large and to consume a significant amount of stack. Masking such implementations at high orders becomes quickly impractical because of the quadratic growth of the stack usage.

To reduce stack usage and allow us to explore high masking orders, our bitsliced programs manipulate 8-bit variables, meaning that 8 independent blocks can be processed in parallel. This trades memory usage for performance, as we could have used 32-bit variables and improved our throughput by a factor 4. However, doing so would have put an unbearable amount of pressure on the stack, which would have prevented us from considering masking orders beyond 7. Besides, it is not clear whether there is a use-case for such a massively parallel (32 independent blocks) encryption primitive in a lightweight setting. As a result of our compilation strategy, we have been able to mask all primitives with up to 16 shares and, additionally, reach 32 shares for Photon, Skinny, Spongent and Subterranean.

As for the n-sliced implementations, we observe a close match between the asymptotic performance of the primitive and their number of multiplications per bits (Table 6), which becomes even more prevalent as order increases and the overhead of linear operations becomes comparatively smaller. Pyjamask remains a good example to illustrate this phenomenon, the inflection point being reached at order 15 with respect to Ace (which uses 3× more multiplications).

The performance of Ascon with the fast RNG, which was slowed down by its suboptimal use of 64-bit registers in n-slicing, is streamlined in bitslicing: here, it exhibits the same number of multiplication per bits as Xoodoo and, indeed, their performance match remarkably well.

Finally, we observe that with the pooling RNG, already at order 15, the performances of our implementations is in accord with their relative number of multiplications per bits. In bitslicing (more evidently than in n-slicing), the number of multiplications is performance critical, even at relatively low masking order.

Conclusion

In this paper, we have introduced tightPROVE + , an extension of tightPROVE that operates on the register-probing model. Stepping beyond the bit-probing model allows us to establish provable security in a purely software context. By combining tightPROVE + with the Usuba programming language, we have obtained an integrated development environment, called Tornado, that streamlines the definition of symmetric ciphers and automates their compilation into provably-secure masked implementations. Thanks to this framework, we have been able to systematically evaluate 11 NIST lightweight cryptography round-2 submissions that are amenable to masking. We have identified 3 ciphers (Ace, Clyde, Gimli) that are not safe in the register probing model and proposed some refresh points to repair them. We have also carried out an extensive performance evaluation, studying the asymptotic behavior of these ciphers across a large range of masking orders.

As part of future work, we intend to further enrich our compiler backend with optimizations specific to embedded architectures (Cortex M and/or Risc-V), systematizing various primitivespecific optimizations documented in the literature [START_REF] Ko Stoffelen | Efficient cryptography on the RISC-V architecture[END_REF][START_REF] Kannwischer | pqm4: Testing and benchmarking NIST PQC on ARM cortex-m4[END_REF][START_REF] Schwabe | All the AES you need on cortex-m3 and M4[END_REF]. Previous results on Intel architecture [START_REF] Mercadier | Usuba: high-throughput and constant-time ciphers, by construction[END_REF] has demonstrated that Usuba can produce code whose performance is on par with hand-optimized, assembly implementations. and j ∈ 1, s v ij = f ij (x 1 , . . . , x n ) + g ij (v 3 , . . . , v q ) + r ij , where f ij and g ij are deterministic functions and r ij , called random part of v ij , is either a random element of K or 0. Let us start by creating a new pair of registers that is easier to work with, but for which simulating it is equivalent to simulating (v 1 , v 2 ). We first create v 1 and v 2 , defined as follows: for every i ∈ {1, 2} and j ∈ 1, s , if there exists j 2 < j such that r ij = r ij2 = 0, then v ij = v ij +v ij2 , and otherwise v ij = v ij . Since simulating a pair (v ij1 , v ij2 ) is equivalent to simulating (v ij1 , v ij1 , +v ij2 ), it is clear that simulating (v 1 , v 2 ) is equivalent to simulating (v 1 , v 2 ). Now neither v 1 nor v 2 contains two identical non-zero random parts. We then create v 1 and v 2 , defined as follows: v 1 = v 1 , v 2 = v 2 and for every j 1 ∈ 1, s , if there exists j 2 = j 1 such that r 1j1 = r 2j2 = 0, then swap the slots j 1 and j 2 of v 2 . It is not hard to see that simulating (v 1 , v 2 ) is equivalent to simulating (v 1 , v 2 ). Now, two equal and non-zero random parts in v 1 and v 2 are on the same slot. All the random parts in v 1 and v 2 cannot be random uniform independent bits, otherwise (v 1 , v 2 ) can be straightforwardly simulated, and then (v 1 , v 2 ) can be simulated, which contradicts our hypothesis). This implies that there exists a slot j for which (r 1j , r 2,j ) ∈ {(0, 0), (0, r), (r, 0), (r, r)} where r is a random uniform element of K. We consider four cases:

• There exists a slot j for which (r 1j , r 2,j ) = (0, 0) and either f 1j or f 2j is not constant.

• There exists a slot j for which (r 1j , r 2,j ) = (0, r) and f 1j is not constant.

• There exists a slot j for which (r 1j , r 2,j ) = (r, 0) and f 2j is not constant.

• There exists a slot j for which (r 1j , r 2,j ) = (r, r) and f 1j + f 2j is not constant. One of these cases must be true, as otherwise (v 1 , v 2 ) could be simulated. Then, for any j verifying one of these conditions, we can refer to the proof in the original paper to determine which probe to add to P m so that no simulator can simulate C([x 1 ], . . . , [x n ]) P .

-Finally, if P m contains more than one pair of probes, we use the same reasoning to prove that no simulator can simulate C([x 1 ], . . . , [x n ]) P1 where P 1 is obtained by replacing one pair of probes in P by a single index i or j or a probe pointing to a cross-product inside a multiplication gadget. We can then apply this method on the new set of probes P 1 , to get another set of probes P 2 where another pair of probes is replaced, and so on, until no pairs of probes are left. We then define A 0 as the adversary that returns the last set of probes obtained this way. By construction, no simulator can output a perfect simulation of the evaluation of C under this set of probes.

A.2 Game 1 -Game 2 transition

Let us show the following equivalence:

∀A 1 , ∃S 1 , S 1 wins Game 1 ⇐⇒ ∀A 2 , ∃S 2 , S 2 wins Game 2 by considering separately both implications.

We first assume that ∀A 2 , ∃S 2 , S 2 wins Game 2. Let A 1 be the adversary that outputs values x 1 , . . . , x n ∈ V and a set of probes P . We define A 2 as the adversary that outputs the same set of probes P and input values x 1 , . . . , x N where the n first elements are the inputs A 1 chose, and the N -n remaining ones are the decoded outputs of the multiplication and refresh gadgets. It has been shown in the original paper that the ISW multiplication gadget produces as output a fresh random uniform sharing. This implies that the multiplication gadgets we consider output a fresh random uniform sharing vector. These outputs can thus be treated as new uniform inputs sharing of the same plain value without modifying the evaluation. Thus, C([x 1 ], . . . , [x n ]) P , and C ([x 1 ], . . . , [x N ]) P output the same distribution. Since, by assumption, there exists S 2 that wins Game 2, there exists S 1 that wins Game 1 by outputting the same distribution as S 2 for the adversary A 2 .

We now assume that ∀A 1 , ∃S 1 , S 1 wins Game 1. Let A 2 be the adversary that outputs values x 1 , . . . , x N ∈ V and a set of probes P . We define A 1 as the adversary that outputs the same set of probes P and the first n values of x 1 , . . . , x N . For the same reasons as before, C([x 1 ], . . . , [x n ]) P , and C ([x 1 ], . . . , [x N ]) P output the same distribution, so we can just define a simulator S 2 that wins Game 2 by outputting the same distribution as S 1 , a simulator that wins Game 1 for the adversary A 1 .

B.1 There is a t-probing attack on C ⇐= A (C) is False

Let us assume that A (C) is False and let us denote by G a graph created during the execution of the algorithm such that there exists a node b in G and a layer i for which S i,b ∩ O i,b = ∅. By construction, there is exactly one path in G that goes from the node called root and b, where each node on the path is in a different layer. For the sake of readability, we now label the information contained in the nodes of that path only by the layer number. For example, S i,b ∩ O i,b can now be written S i ∩ O i without ambiguity. Let us denote by O i (α) and G i (α) the α th elements of the sets O i and G i respectively (the elements being ordered by the order in which they were added to the sets during the execution of the algorithm), and let us further denote by B(β) the β th column vector of a block B.

Since S i ∩ O i = ∅, there exists a vector w ∈ S i , indexes α 1 , . . . , α ri ∈ 1, |O i | and sets of indexes β 1 , . . . , β ri ⊆ 1, s such that w = ri r=1 β∈βr O i (α r )(β), meaning that w is a linear combination of column vectors of free operand blocks. For a given input block A of a multiplication, let us denote by A the other input operand block. We now define the matrix M 0 = O i (α 1 ) . . . O i (α ri ), the concatenation of the blocks used in the linear combination w equals to. We also define, for all k ∈ 1, r i the matrix M k = O i (α k ) ∈ Q i . Let W be the only block in the set Q 1 , and let us call S 0 the vector space W and O 0 = ∅. For all A ∈ Q i , there exists k ∈ 0, i -1 such that

S k+1 = S k ∩ ( A + O k ),
and since S i ⊆ S j for every j ≤ i, we have

w ∈ S i ⊆ S k+1 ⊆ A + O k .
As O k ⊆ O i-1 , we can further say that

w ∈ A + O i-1 ,
meaning that we can construct w from any operand in Q i along with free operands of the previous layer. For every k ∈ 1, r i , we thus have

w ∈ M k + O i-1 ,
so there exists indexes α k,1 , . . . , α k,f k ∈ 1, |O i-1 | and sets of indexes β k,0 , . . . , β k,f k ⊆ 1, s such that

w = β∈β k,0 M k (β) + f k r=1 β∈β k,r O i-1 (α k,r )(β).
meaning that w is a linear combination of column vectors of M k and column vectors of f k free operand blocks that are in O i-1 . We then complete the matrix M k by defining

M k = M k ( f k r=1 O i-1 (α k,r
)). All the blocks involved in the linear combination are then present in this matrix. In other words, we have w ∈ M k . For all r ∈ 1, f k , we also define the matrix M j (with j = r i + ( k-1 u=1 f u ) + r) by M j = O i-1 (α k,r ) ∈ Q i-1 . We now have r i-1 = f 1 + • • • + f ri new matrices M ri+1 , . . . , M ri+ri-1 made of one block of Q i-1 to complete. For the same reasons as before, for every k ∈ r i + 1, r i + r i-1 , M k ∈ Q i-1 , so w ∈ M k + O i-2 , and then we can reiterate the same process to complete the matrices M k and create r i-2 new matrices to complete, made of one block of Q i-2 . We repeat this process until we have r 1 matrices M J+1 , . . . , M J+r1 (with J = i k=2 r k ) made of one block of Q 1 . Since Q 1 = {W }, all these matrices are W , and we define M j = M j for all j ∈ J + 1, J + r 1 . If we call R = i k=1 r k , we thus have defined R + 1 matrices M 0 , M 1 , . . . , M R made of a total of R pairs of block operands that satisfy w ∈ R j=0 ( M j ), meaning that there is a probing attack on C (of order t = R).

  (b) Node manipulating a 5-uple node LinearLayer(state:u64x5) returns (stateR:u64x5) let stateR[0] = state[0] ^(state[0] >>> 19)

Fig. 1 :

 1 Fig. 1: Ascon cipher in Usuba

Fig. 2 :

 2 Fig. 2: High-level view of the Usuba compiler

  [⊗] takes two d-sharings [a] and [b] as inputs and outputs a d-sharing [c] such that c = a • b as follows:

-

  The sharewise addition gadget [⊕] computes a d-sharing [c] from sharings [a] and [b] such that c = a + b by letting c i = a i + b i for i ∈ 0, d -1 . -The sharewise left shift, right shift and rotation gadgets ([ n ], [ n ] and [≪ n ] respectively) take a sharing [a] as input and output a sharing [c] such that c = f (a) by letting c i = f (a i ) for i ∈ 0, d -1 , f being the corresponding function described in the section above. -The sharewise multiplication by a constant [⊗ k ] takes a sharing [a] and a constant k ∈ V as inputs and outputs a sharing [c] such that c = k • a by letting c i = k • a i for i ∈ 0, d -1 . -The sharewise addition with a constant [⊕ k ] takes a sharing [a] and a constant k ∈ V as input and outputs a sharing [c] such that c = a + k by letting c i = a i for i ∈ 0, d -1 and c 0 = a 0 + k. The coordinate-wise logical complement NOT is captured by this definition with k = (1, . . . , 1).

  b denotes the Minkowski sum of A and O i,b ), then we connect b to a new node b in the next layer i + 1, containing the following information:

Algorithm 1 :

 1 tightPROVE + input : A description of a circuit C output: True or False, along with a proof (and possibly a list of attacks) foreach operand W do /* create root for the new graph GW

Fig. 5 :

 5 Fig. 5: Examples of graphs G F (left) and G W (right) created during the algorithm.

Fig. 7 :

 7 Fig. 7: ISW gadgets.

Fig. 8 :

 8 Fig. 8: High-level view of the Tornado compiler.

  1. Create a set G 1 with all the multiplications for which w is one of the operand vectors. 2. Create a set O 1 with the co-operand vectors of w in the multiplications in G 1 . 3. Stop if w ∈ O 1 (O 1 's linear span), that is if w can be written as a linear combination of Boolean vectors from O 1 . 4. For i from 2 to m, create new sets G i and O i by adding to G i-1 multiplications that involve an operand w verifying w ∈ (w ⊕ O i-1 ), and adding to O i-1 the other operand vectors of these multiplications. Stop whenever i = m or

  C([x 1 ], . . . , [x n ]) P without the input sharings. It wins the game if and only if the distributions of both experiments are identical.

	Definition 1 ([8]). A shared circuit C is t-probing secure if and only if for every adversary A,
	there exists a simulator S that wins the t-probing security game defined in Figure 3, i.e. the random
	experiments ExpReal(A, C) and ExpSim(A, S, C) output identical distributions.

  1 2 ), (p 2 1 , p 2 2 ), . . . , (p t 1 , p t 2 )}, where for i in {1, . . . , t}, p i 1 and p i 2 are wire indices corresponding to one element of each input sharings of the same multiplication.

Table 1 :

 1 Overview of the selected cryptographic primitives.

	primitive	state size multiplications mult./bits n-sliceable (bits) n-slice bitslice n-slice bitslice	slice size
	Ace [1]	320	384 12288	1.2	38	32
	Ascon [23]	320	60	3840	0.19	12	64
	Clyde [9]	128	48	1536	0.37	12	32
	Gift [3]	128	160	5120	1.25	40	32
	Gimli [11]	384	288	9216	0.75	24	32
	Photon [4]	256	-	3072	-	12	-
	Pyjamask [24]	128	56	1792	0.44	14	32
	Skinny [7]	128	-	6144	-	48	-
	Spongent [13, 14]	160	-	12800	-	80	-
	Subterranean [22]	257	-	2056	-	8	-
	Xoodoo [21, 20]	384	144	4608	0.37	12	32

Table 2 :

 2 Results of tightPROVE + on all the implementations.

	submissions	primitive	time (bitslice)	bit probing security	register size	time (n-slice)	register probing security
			block ciphers
	Gift-COFB,
	HYENA, SUNDAE-	Gift-128	55 H 40 min		32	2 H 15 min
	Gift
	Pyjamask	Pyjamask-128	30 min		32	6 min
	Skinny, Romulus	Skinny-128-256	10 H		-	-	-
	Spook	Clyde-128	10 min		32	32 s
			permutations
	Ace	Ace	54 H 30 min		32	10 min
	Ascon	p 12	1 H 45 min		64	1 H 13 min
		Spongent-
	Elephant	π[160](1	6 s		-	-	-
		round)
		Spongent-
	Elephant	π[160](10	20 min 40 s		-	-	-
		rounds)
	Gimli	Gimli-36	22 H 45 min		32	1 H 10 min
	ORANGE,
	Photon-	Photon-256	2 H		-	-	-
	BEETLE
	Xoodyak	Xoodoo[12]	2 H 50 min		32	4 H 5 min
			others
	Subterranean	blank(8)	17 min		-	-	-

Table 3 :

 3 Complementary information on flawed implementations.

	primitive	register first attack size	all operands	least attack order	refresh gadgets needed	refreshed circuit
	Ace	32	10 min	25 min	1	384	70 H
	Clyde-128	32	32 s	2 min 10 s	2	6	3 min 10 s
	Gimli-36	32	1 H 10 min	66 H 20 min	2	≤ 120	8 H 50 min

Table 4 :

 4 Comparison of Usuba vs reference implementations.

	primitive	Performances (cycles/bytes) (lower is better)
		Usuba n-slice Usuba bitslice reference
	Ace	34.25	55.89	276.53
	Ascon	9.84	4.94	5.18
	Clyde	33.72	21.99	37.69
	Gimli	15.77	5.80	44.35
	Gift	565.30	45.51	517.27
	Photon	-	44.88	214.47
	Pyjamask	246.72	131.33	267.35
	Skinny	-	46.87	207.82
	Spongent	-	146.93	4824.97
	Subterranean	-	17.64	355.38
	Xoodoo	14.93	6.47	10.14

Table 5 :

 5 Performances of Tornado generated n-sliced masked implementations.

				(a) cycles per byte
					Performances (cycles/bytes)
	primitive mult./bytes TRNG	(lower is better)
				d = 0 d = 3 d = 7 d = 15 d = 31 d = 63 d = 127
	Ascon	1.375	pooling 49 fast 49	1.34k 4.57k 20.54k 79.24k 324k 1.30m 1.05k 3.08k 11.61k 42.48k 163k 640k
	Xoodoo		1.5	pooling 63 fast 63	1.71k 6.96k 29.07k 113k 448k 1.73m 889 3.26k 10.84k 39.43k 143k 555k
	Clyde		3	pooling 92 fast 92	1.88k 7.58k 31.43k 121k 483k 1.87m 961 3.53k 11.84k 41.88k 161k 653k
	Pyjamask		3	pooling 994 5.93k 17.16k 59.66k 194k 646k 2.27m fast 994 4.97k 12.84k 38.40k 108k 297k 950k
	Gimli		6	pooling 56 fast 56	3.97k 17.35k 73.42k 293k 1.17m 4.56m 1.77k 7.14k 24.71k 95.20k 356k 1.40m
	Gift		10	pooling 1.12k 15.27k 44.68k 138k 532k 1.82m 6.40m fast 1.13k 12.53k 32.27k 77.61k 285k 819k 2.64m
	Ace		19.2	pooling 92 fast 92	7.55k 32.94k 114k 495k 1.96m 7.77m 3.88k 13.29k 40.06k 190k 746k 2.84m
				(b) cycles per bloc
					Performances (cycles)
	primitive mult. TRNG		(lower is better)
				d = 0 d = 3	d = 7 d = 15 d = 31 d = 63 d = 127
	Clyde	48	pooling 1.47k 30.08k 121.28k 502.88k 1.94m 7.73m 29.92m fast 1.47k 15.38k 56.48k 189.44k 670.08k 2.58m 10.45m
	Pyjamask 56	pooling 15.90k 94.88k 274.56k 954.56k 3.10m 10.34m 36.32m fast 15.90k 79.52k 205.44k 614.40k 1.73m 4.75m 15.20m
	Ascon	60	pooling 1.96k 53.60k 182.80k 821.60k 3.17m 12.96m 52.00m fast 1.96k 42.00k 123.20k 464.40k 1.70m 6.52m 25.60m
	Xoodoo 144	pooling 3.02k 82.08k 334.08k 1.40m 5.42m 21.50m 83.04m fast 3.02k 42.67k 156.48k 520.32k 1.89m 6.86m 26.64m
	Gift	160	pooling 17.92k 244.32k 714.88k 2.21m 8.51m 29.12m 102.40m fast 18.08k 200.48k 516.32k 1.24m 4.56m 13.10m 42.24m
	Gimli	288	pooling 2.69k 190.56k 832.80k 3.52m 14.06m 56.16m 218.88m fast 2.69k 84.96k 342.72k 1.19m 4.57m 17.09m 67.20m
	Ace	384	pooling 3.68k 302.00k 1.32m 4.56m 19.80m 78.40m 310.80m fast 3.68k 155.20k 531.60k 1.60m 7.60m 29.84m 113.60m

Table 6 :

 6 Performances of Tornado generated bitslice masked implementations.

				Performances (cycles/bytes)
	primitive mult./bits TRNG	(lower is better)
			d = 0 d = 3 d = 7 d = 15 d = 31
	Subterranean	8	pooling 94 fast 94	4.46k 19.13k 79.63k 312k 2.15k 7.18k 27.03k 95.19k
	Ascon	12	pooling 101 7.33k 30.33k 125k fast 101 3.07k 11.45k 42.39k	--
	Xoodoo	12	pooling 112 6.69k 28.79k 120k fast 112 3.12k 10.49k 39.35k	--
	Clyde	12	pooling 177 7.88k 31.04k 127k fast 161 3.44k 13.57k 45.34k	--
	Photon	12	pooling 193 10.47k 31.77k 126k 476k fast 193 7.66k 14.28k 44.99k 154k
	Pyjamask	14	pooling 1.59k 20.33k 52.81k 193k fast 1.59k 16.52k 31.74k 97.88k	--
	Gimli	24	pooling 127 12.14k 53.64k 236k fast 127 5.51k 19.15k 76.91k	--
	Ace	38	pooling 336 19.94k 89.12k 395k fast 336 8.22k 35.29k 123k	--
	Gift	40	pooling 358 21.38k 93.92k 405k fast 358 11.08k 36.79k 136k	--
	Skinny	48	pooling 441 34.28k 131k 525k 1.97m fast 441 18.19k 61.75k 200k 664k
	Spongent	80	pooling 624 44.04k 188k 816k 3.15m fast 624 19.45k 64.78k 259k 948k

Tornado ambitions to be the workhorse of those cryptographers that selflessly protect their ciphers through provably secure mask ing and precise bitslicing.

https://csrc.nist.gov/Projects/lightweight-cryptography/round-2-candidates

The literature[START_REF] Mercadier | Usuba: high-throughput and constant-time ciphers, by construction[END_REF] Fig.2] distinguishes vertical from horizontal n-slicing: lacking the powerful SIMD instructions required by horizontal n-slicing, we focus here solely on vertical n-slicing, which we abbreviate unambiguously to "n-slicing".

S1,root S2,A S2,C S2,D S3,AC S3,CA S1,root S2,A S2,B S2,C S2,D S3,AC S3,BC S3,BD S3,CA S3,DA S3,DB

See https://csrc.nist.gov/Projects/lightweight-cryptography/round-2-candidates for the list of candidates together with specifications and reference implementations.

Acknowledgments. This work is partly supported by the French FUI-AAP25 VeriSiCC project, the Émergence(s) program of the City of Paris and the EDITE doctoral school.

A Proofs of section 3.3 Let us recall the formal games.

-In Game 0, the adversary A 0 outputs values x 1 , . . . , x n ∈ V and a set of probes P = P r ∪ P m ∪ P sw with no restriction on the placement of probes. -In Game 1, the adversary A 1 outputs values x 1 , . . . , x n ∈ V and a set of probes P = P r ∪ P m ∪ P sw . The probes in P sw can be any index in sharewise gadgets, those in P m are pairs of index in multiplication gadgets, and those in P r can only be an index of the input of refresh gadgets. -In Game 2, the adversary A 2 outputs values x 1 , . . . , x N ∈ V and a set of probes P = P r ∪ P m ∪ P sw as in Game 1, except that the circuit is flattened, by considering the outputs of multiplications as new inputs. -In Game 3, the adversary A 3 outputs values x 1 , . . . , x N ∈ V and a set of probes P = P r ∪ P m ∪ P sw where P r = P sw = ∅.

In each game, a simulator S aims at simulating the distribution of the probed variables, and wins the game if it manages to do so.

A.1 Game 0 -Game 1 transition

Let us prove the following equivalence: ∀A 0 , ∃S 0 , S 0 wins Game 0 ⇐⇒ ∀A 1 , ∃S 1 , S 1 wins Game 1 considering separately both implications.

In a first attempt, we assume that ∀A 1 , ∃S 1 , S 1 wins Game 1. Let A 0 be the adversary that outputs values x 1 , . . . , x n ∈ V and a set of probes P = P r ∪ P m ∪ P sw . In the bit probing model, the multiplication and refresh gadgets are t-SNI, which implies that the distribution of a variable probed inside the gadget can be simulated from at most one share of each input. In the register probing model, the multiplication (resp. refresh) gadgets can be seen as a concatenation of bitwise multiplication (resp. refresh) gadgets. As a result, they are t-SNI, and for each probe in P r ∪ P m , the distribution of the variable it points to can be simulated by (at most) one share of each input. This means that the t shares pointed by P = P r ∪ P m ∪ P sw can be perfectly simulated from a set of t probes P = P r ∪ P m ∪ P sw pointing to shares in a sharewise gadget or inputs shares of refresh gadgets or pairs of inputs shares of multiplication gadgets. We define A 1 as the adversary that outputs the same values x 1 , . . . , x n and the set of probes P . By assumption, there exists a simulator S 1 that wins Game 1, meaning that it outputs a perfect simulation of C([x 1 ], . . . , [x n ]) P , with which we can in turn simulate C([x 1 ], . . . , [x n ]) P . This means that there exists a simulator S 0 that wins Game 0.

In a second attempt, we assume that ∃A 1 , ∀S 1 , S 1 fails Game 1 and we show the contrapositive statement:

∃A 1 , ∀S 1 , S 1 fails Game 1 =⇒ ∃A 0 , ∀S 0 , S 0 fails Game 0.

By assumption, there exists an adversary A 1 that ouputs values x 1 , . . . , x n ∈ V and a set of probes P = P r ∪ P m ∪ P sw such that no simulator S 1 can simulate the tuple (v 1 , . . . , v q ) = C([x 1 ], . . . , [x n ]) P . Let A 0 be the adversary that outputs the same input values x 1 , . . . , x n and a set of probes P = P r ∪ P m ∪ P sw such that P r = P r and P sw = P sw . We now show how to construct the set P m so that no simulator S 0 can simulate C([x 1 ], . . . , [x n ]) P :

-

-If P m = {(i, j)}: we can assume that i and j are indices pointing to the variables v 1 and v 2 . We can also assume that there exists a simulator S 0 that simulates (v 3 , . . . , v q ), since otherwise we could just define A 0 as the adversary that returns the probes P r ∪ P sw . We can now say that no simulator can perfectly simulate (v 1 , v 2 ) given (v 3 , . . . , v q ). Let us denote by v ij the j th coordinate of v i . Since the coordinates of shares of inputs of multiplication gadgets are linear combinations of the coordinates of the input shares, we can write for every i ∈ {1, 2}

A.3 Game 2 -Game 3 transition

Let us show the following equivalence:

∀A 2 , ∃S 2 , S 2 wins Game 2 ⇐⇒ ∀A 3 , ∃S 3 , S 3 wins Game 3 by considering separately both implications.

From left to right, we first assume that ∀A 2 , ∃S 2 , S 2 wins Game 2. Let A 3 be the adversary that outputs values x 1 , . . . , x N ∈ V and a set of probes P pointing to pairs of inputs of multiplications. We define A 2 as the adversary that outputs the same set of probes P and the same inputs. By assumption, there exists a simulator S 2 that can perfectly simulate C ([x 1 ], . . . , [x N ]) P and thus win Game 2. We can then say that there exists S 3 that wins Game 3 by outputting the same distribution as S 2 for the adversary A 2 .

From right to left, we then assume that ∃A 2 , ∀S 2 , S 2 fails Game 2 and show the contrapositive statement:

By assumption, there exists an adversary A 2 that ouputs values x 1 , . . . , x N ∈ V and a set of probes P = P r ∪ P m ∪ P sw such that no simulator S 2 can win Game 2. Let us denote by M 0 , . . . , M t the induced matrices from P as defined in Section 3.3. Since the distribution of the variables pointed by the probes cannot be simulated, we have t i=0 M i = ∅. Since each of these matrices is non-empty and made up of a concatenation of blocks, with a total number of q ≤ 2t blocks distributed among t + 1 matrices, at least one of these matrices is made of exactly one block. We now show that one of the matrices is made of exactly one block W that is induced by a probe on a multiplication gadget. A 2 can use t probes. If t other are placed on gadgets other than multiplication gadgets, then a least t + 1 -t other matrices are filled with 2(t -t other ) blocks induced by probes on multiplication gadgets. For the same reasons as before, this implies that there exists a matrix that contain exactly one block, induced by a probe on a multiplication gadget. Let us define A 3 as the adversary that outputs the same input values as A 2 and a set of probes P defined as follows:

-Select a block W as defined above, induced by a probe on a multiplication gadget m. We can assume without loss of generality that W comes from the left operand of m. -For every pair (p 1 , p 2 ) ∈ P m , include (p 1 , p 2 ) to P .

-For every probe p ∈ P r ∪ P rw , let j be the share index of the variable pointed by p. Then, include (p 1 , p 2 ) to P , where p 1 denotes a probe on the j th share of the left operand and p 2 a probe on the right operand.

By construction, the new set of operands P induce matrices whose images still intersect, meaning that no simulator S 3 can output a perfect simulation of C ([x 1 ], . . . , [x N ]) P , and thus no simulator can win Game 3 for the adversary A 3 .

B Proof of Correctness

Let us denote by A (C) the result of Algorithm 1 when run with the circuit C as its input. We show the following equivalence:

there is a t-probing attack on C ⇐⇒ A (C) is False which is equivalent to ∃M 0 , . . . , M t (as defined in section 3.3),

B.2 There is a t-probing attack on C =⇒ A (C) is False

We now assume that there exists matrices M 0 , M 1 , . . . , M t , made of a total of 2t operand blocks of probed multiplications, that verify

In the following, we denote by dec the function that associates a matrix made of concatenated blocks to the set of blocks it is made of. For a given block operand A of a probed multiplication, we denote by A the other block operand of the multiplication.

Let w be a vector in S. As shown in the demonstration of the game transition between Game 2 and Game 3, there exists j ∈ 0, t and W ∈ {A g , B g } g a block operand of a multiplication gadget such that M j = W . Since W ∈ {A g , B g } g , the algorithm creates a graph G W , with Q 1,root = {W }. Let us define an additional fictive node root such that S 0,root = W , G 0,root = ∅, O 0,root = ∅, and Q 0,root = ∅. We now show by induction that the following statement P i is true for all i ∈ N:

Intuitively, this property means that if no attack on w was found by the algorithm before layer i, then it either finds an attack on layer i or creates a new node in layer i + 1. We start by showing that P 0 is true. Since w ∈ S 0,root ∩ ( W + O 0,root ) = W , the right predicate is true, so the implication is true as well. We now assume that P i is true for a given i ∈ N, and show that P i+1 is true. We also assume the left side of the implication to be true:

In particular, we have

and by the induction hypothesis, we deduce that we have

The former cannot be true by assumption, so the latter is true, meaning that there exists b such that w ∈ S i+1,b . We now assume that ∀b, w /

More particularly, we show that this is true for b = b . For all j ∈ 0, t , let E j be the set dec(M j ) ∩ Q i+1,b , and let us define t i = t j=0 |E j |. For all j ∈ 0, t , for every block A ∈ E j , A and A must be present in the matrices, so we have 2t i blocks of O i+1,b and Q i+1,b in the matrices. We show that however the remaining 2t -2t i blocks are placed in the matrices, the right-hand side of the implication is true.

Let us define

We have t + 1 -t α ≤ t i , so t -t i ≤ t α -1 < t α , which implies 2t -2t i < 2t α . This means that there exists at least one matrix M for which there exists a block A ∈ {A g , B g } g \Q For all i ∈ N, P i is true, but since G W has a finite number of layers l, then for i = l + 1, the implication is true while the right predicate is false, which implies that the left predicate is false, which is equivalent to ∃j ≤ l, ∃b, w ∈ S j,b ∩ O j,b .

The algorithm thus returns False, and we can further say that an attack on w is detected. And since this is true for any w ∈ S, we can also say that all the operands that can be retrieved with probing attacks can be found by the algorithm.