Gilles Barthe

Sonia Belaïd

Pierre-Alain Fouque

Benjamin Grégoire

Pierre-Yves Strub

Rébecca Zucchini

Strong Non-Interference and Type-Directed Higher-Order Masking *

Differential power analysis (DPA) is a side-channel attack in which an adversary retrieves cryptographic material by measuring and analyzing the power consumption of the device on which the cryptographic algorithm under attack executes. An effective countermeasure against DPA is to mask secrets by probabilistically encoding them over a set of shares, and to run masked algorithms that compute on these encodings. Masked algorithms are often expected to provide, at least, a certain level of probing security. Leveraging the deep connections between probabilistic information flow and probing security, we develop a precise, scalable, and fully automated methodology to verify the probing security of masked algorithms, and generate them from unprotected descriptions of the algorithm. Our methodology relies on several contributions of independent interest, including a stronger notion of probing security that supports compositional reasoning, and a type system for enforcing an expressive class of probing policies. Finally, we validate our methodology on examples that go significantly beyond the state-of-the-art.

Introduction

Differential power analysis, or DPA [START_REF] Paul | Differential power analysis[END_REF], is a class of side-channel attacks in which an adversary extracts secret data from the power consumption of the device on which a program manipulating the data executes. One practical countermeasure against DPA, called masking [START_REF] Chari | Towards sound approaches to counteract power-analysis attacks[END_REF][START_REF] Goubin | DES and differential power analysis (the "duplication" method)[END_REF], transforms an algorithm that performs computations over a finite ring K into a randomized algorithm that manipulates probabilistic encodings. 8 At an abstract level, any masking transformation performs two tasks. First, it replaces every algebraic operation performed by the original algorithm by a call to a gadget, i.e. a probabilistic algorithm that simulates the behavior of algebraic operations on probabilistic encodings. Second, it inserts refreshing gadgets, i.e. gadgets that take a probabilistic encoding of v and rerandomizes its shares in order to produce another probabilistic encoding w of v. Inserting refreshing gadgets does not change the functional behavior of the masked algorithm, and increases the randomness complexity and execution time of the masked program. However, it is also compulsory for achieving security. Therefore, an important line of research is to find suitable trade-offs that ensure security while minimizing the performance overhead of masking; see [START_REF] Belaïd | Randomness complexity of private circuits for multiplication[END_REF] for recent developments in this direction.

The baseline notion of security for masked algorithms is t-probing security. Informally, an algorithm P is t-probing secure if the values taken by at most t intermediate variables of P during execution do not leak any information about secrets (held by its inputs). More formally, an algorithm P achieves t-probing security iff for every set of at most t intermediate variables, the joint distributions of the values taken by these intermediate variables coincide for any two executions initiated from initial inputs that agree on t shares of each input encoding. Stated in this form, probing security is an instance of probabilistic information flow, universally quantified over all position sets that meet a cardinality constraint, and is therefore potentially amenable to formal analysis using a well-developed body of work on language-based security and program verification. Indeed, the connection between probing security and information flow has been instrumental in a promising line of research, initiated in [START_REF] Moss | Compiler assisted masking[END_REF] and further developed in [START_REF] Galip Bayrak | Sleuth: Automated verification of software power analysis countermeasures[END_REF][START_REF] Eldib | SMT-based verification of software countermeasures against side-channel attacks[END_REF][START_REF] Eldib | Synthesis of masking countermeasures against side channel attacks[END_REF][START_REF] Barthe | Verified proofs of higher-order masking[END_REF], which uses type systems, program logics, SMT solvers and other methods for verifying or synthesizing masked algorithms at small (≤ 5) orders. However, none of these works addresses the problem of composition, and all fail to scale either to higher orders or to larger algorithms.

Contributions We develop precise and scalable techniques for synthesizing masked algorithms that achieve probing security. Our techniques apply to a wide range of probing policies, including existing policies and new policies defined in this paper, and deliver masked algorithms that outperform (in terms of randomness complexity and computational efficiency) prior approaches. In more detail, we make the following broad contributions:

1. Strong non-interference. We introduce a stronger notion of probing security, which we call strong non-interference, and prove that it is in fact satisfied by many (but not all) gadgets from the literature. Furthermore, we justify that strong non-interference is the desired property for refreshing gadgets, by reconsidering known negative and positive results [START_REF] Coron | Higher-order side channel security and mask refreshing[END_REF] for a simplified example extracted from Rivain and Prouff's inversion algorithm [START_REF] Rivain | Provably secure higher-order masking of AES[END_REF]. We first observe that the refreshing gadget used in the original, flawed, algorithm does not enjoy strong non-interference. Second, we note that the refreshing gadget used in the fixed, secure, algorithm is indeed strongly non-interfering, and we show that one can prove the probing security of the fixed algorithm, based simply on the assumption that the refreshing gadget is strongly non-interfering. Generalizing these observations, we prove that every non-interfering algorithm can be turned into a strongly non-interfering algorithm, by processing its inputs or its output with a strongly noninterfering refreshing gadget. We also provide more general results about the composition of strongly non-interfering gadgets.

2. Formal proofs. We develop and implement an automated method, inspired from [START_REF] Barthe | Verified proofs of higher-order masking[END_REF], for checking strong non-interference. We apply our automated verifier for strong noninterference to several gadgets from the literature and some other interesting compositions, for orders t ≤ 6. For several more widely-used gadgets, we further use EasyCrypt [START_REF] Barthe | EasyCrypt: A tutorial[END_REF] to provide machine-checked proofs of t-probing security for all t.

3. Type-based enforcement of probing security. We define an expressive language for specifying a large class of non-interference properties with cardinality constraints. Our language can be seen as a variant of the first-order theory of finite sets with cardinality constraints [START_REF] Calogero | Combining sets with cardinals[END_REF][START_REF] Bansal | A new decision procedure for finite sets and cardinality constraints in SMT[END_REF], and can be used to specify baseline probing security and strong noninterference, among others. Then, we define a type system that enforces probing policies and prove its soundness. Furthermore, we show how to model in our language of probing policies the notion of affine gadget, and we show how it helps improve the precision of type-checking. [START_REF] Barthe | Verified proofs of higher-order masking[END_REF]. Certifying Masking Transformation. As a proof of concept, we implement a type inference algorithm and a certifying masking transformation that takes as input an arithmetic expression and returns a masked algorithm typable by our type system. 9 Our transformation improves over prior works by selectively inserting refreshing gadgets only at points where type-checking would otherwise fail. This strategy leads to improved efficiency while retaining provable soundness.

5. Practical evaluation. We evaluate our type system and masking transformation on complete algorithms at various orders, often achieving provable t-probing security levels far beyond the state-of-the-art for algorithms of those sizes, and with better performance than most known (provably secure) algorithms in terms of time, memory and randomness complexity.

Related work Section 9 discusses related work in more detail. Here we focus on recent work on automated tools for the verification of synthesis of masked algorithms, starting with Moss et al. [START_REF] Moss | Compiler assisted masking[END_REF], who point out and leverage connections between probing security and probabilistic information-flow for first-order boolean masking schemes. Subsequent works in this direction accommodate higher-order and arithmetic masking, using type systems and SMT solvers [START_REF] Galip Bayrak | Sleuth: Automated verification of software power analysis countermeasures[END_REF], or model counting and SMT solvers [START_REF] Eldib | SMT-based verification of software countermeasures against side-channel attacks[END_REF][START_REF] Eldib | Synthesis of masking countermeasures against side channel attacks[END_REF]. Although approaches based on model counting are more precise than early approaches based on type systems and can be extended to higher-order masking schemes, their algorithmic complexity constrains their applicability. In particular, existing tools based on model counting can only analyze first or second order masked implementations, and can only deal with round-reduced versions of the algorithms they consider (for instance, only analyzing a single round of Keccak at order 1, and algorithms for field operations at orders 2 and higher). Breaking away from model counting, Barthe et al. [START_REF] Barthe | Verified proofs of higher-order masking[END_REF] develop efficient algorithms for analyzing the security of masked algorithms in the probing model. Their approach outperforms previous work and can analyze a full block of AES at first-order, reduced-round (4 rounds) AES at the second-order, and several S-box computation algorithms masked at the third and fourth orders. However, their work does not readily scale either to higher orders or to larger algorithms, mainly due to the lack of composition results.

Our work also bears some connections with language-based security, and in particular with work on the specification and the enforcement of confidentiality policies using techniques from programming languages. For instance, our work has similarities with the work of Pettai and Laud [START_REF] Pettai | Automatic proofs of privacy of secure multi-party computation protocols against active adversaries[END_REF], who develop techniques for proving security of multi-party computations in the presence of strong adversaries, and work by Zdancewic et al. [START_REF] Zdancewic | Untrusted hosts and confidentiality: Secure program partitioning[END_REF], who propose a compiler that partitions programs for secure distributed execution.

Mathematical preliminaries

A function µ : B → R ≥0 is a (discrete) distribution over B if the subset supp(µ)
M : B → D(C), mlet x = µ inM x is the unique distribution µ over C such that µ (c) = b µ(b) M (b)(c).
We often use the notion of marginals. The first and second marginals of a distribution µ ∈ D(B 1 × B 2 ) are the distributions π 1 (µ) ∈ D(B 1 ) and π 2 (µ) ∈ D(B 2 ) given by

π 1 (µ)(b 1 ) = b2∈B2 µ(b 1 , b 2 ) π 2 (µ)(b 2 ) = b1∈B1 µ(b 1 , b 2 ).
The notion of marginal readily extends to distributions over finite maps (rather than pairs).

A bird's eye view of strong non-interference

Before formalizing our definitions, we give an intuitive description of our language for gadgets and of our security notions, based on simple examples.

Gadgets and Positions

Gadget RefreshM 2 (Gadget 1) shows the description in our language of a mask refreshing gadget for t = 2. The gadget takes as input an encoding variable a ∈ K 3 , where K is some finite ring and returns a new encoding c ∈ K 3 such that a = c . The gadget first makes local copies of individual input shares a ı (for 0 ≤ ı ≤ 2) of a into local variables c ı (for 0 ≤ ı ≤ 2). After this first step, we sample uniform random elements from K into a local variable r and perform some ring operations. Finally, the algorithm returns a vector in K 3 , constructed from the final value of local variables c 0 , c 1 and c 2 .

Gadget 1 SNI Mask Refreshing with t = 2 function RefreshM2(a) c0,0 ← a 0 ; c1,0 ← a 1 ; c2,0 ← a 2 ; r0 $ ← K; c0,1 ← c0,0 ⊕ r0; c1,1 ← c1,0 r0; r1 $ ← K; c0,2 ← c0,1 ⊕ r1; c2,1 ← c2,0 r1; r2 $ ← K; c1,2 ← c1,1 ⊕ r2; c2,2 ← c2,1 r2; return c0,2, c1,2, c2,2
Note that the gadget is written in single static assignment (SSA) form, an intermediate representation in which each variable is defined exactly once. Having gadgets written in SSA form allows us to easily refer to the value of a particular variable at a particular point in the program-simply by referring to its name, which corresponds to a unique definition. In this paper, we refer to positions in gadgets and algorithms, which correspond exactly to intermediate variables. We distinguish between three different kinds of positions: input positions, which correspond to shares of the gadget's input (here, I RefreshM2 = {a 0 , a 1 , a 2 }), output positions, which correspond to the variables that appear in the gadget's return vector (here, O int RefreshM2 = {c 0,2 , c 1,2 , c 2,2 }), and internal positions, which refer to all other positions (here,

O ext RefreshM2 = {c 0,0 , c 1,0 , c 2,0 , c 0,1 , c 1,1 , c 2,1 , r 0 , r 1 , r 2 }).
Intuitively, this separation allows us to distinguish between direct observations made by the adversary into a gadget (as internal positions), output shares about which the adversary may have learned some information by probing gadgets that use them as input (as output positions), and shares of the gadget's inputs (as input positions) about which the adversary is now learning information. In the following, we often write "the joint distribution of a set of positions" to discuss the joint distribution of the variables defined at these positions in the gadget (in order). For example, referring to RefreshM 2 , the joint distribution of the ordered set O = c 0,1 , c 2,2 of positions can be described as the following function of a, where we use $ to denote a fresh uniform random sample in K (using indices to denote distinct samples):

RefreshM 2 O (a) = a 0 ⊕$ 0 , (a 2 $ 1 ) $ 2 .
Probing Security and Non-Interference The RefreshM 2 gadget is known to be 2-probing secure, or 2-non-interfering (2-NI) in our terminology, in the sense that the joint distribution of any set of at most 2 of its positions, corresponding to adversary probes, depends on at most 2 shares of the gadget's inputs. This guarantees, if the input encoding is uniform, that no information about it leaks through any 2 probes in the circuit.

Considering again the set O = c 0,1 , c 2,2 of positions in RefreshM 2 and its distribution RefreshM 2 O , it is easy to see-purely syntactically-that it depends at most on shares a 0 and a 2 of the gadget's input encoding. Similarly considering all possible pairs of positions, we can prove that each of them has a joint distribution that depends on at most two shares of a.

Strong Non-Interference Probing security is generally not composable: combining tprobing secure gadgets does not necessarily yield a t-probing secure algorithm [START_REF] Coron | Higher-order side channel security and mask refreshing[END_REF]. Our main contribution is a new and stronger notion of security for gadgets, which we dub strong non-interference (or SNI), which does support some compositional reasoning. SNI reinforces probing security by requiring that the number of input shares on which the distribution of a given position set may depend be determined only by the number of internal positions present in that set. For example, consider again position set O = c 0,1 , c 2,2 in RefreshM 2 , and note that it contains only one internal position (c 0,1 ). We have seen that the joint distribution RefreshM 2 O of that position set syntactically depends on two shares of a. However, it can be equivalently expressed as RefreshM 2 O (a) = $ 0 , (a 2 $ 1 ) $ 2 (since the ring addition ⊕ is a bijection of each of its arguments and $ 0 is a fresh and uniform ring element). This shows that the distribution in fact depends on at most one share of a (here a 2 ). In fact, it can be shown that RefreshM 2 is 2-SNI. More generally, surprisingly many gadgets from the literature achieve SNI.

However, and not unexpectedly, some gadgets from the literature do not satisfy SNI. Consider for instance RefreshA 2 (Gadget 2). It is easy to see that the gadget is 2-NI (each position c ı, depends only on input share a ı , and each position r i is completely independent from the input encoding). Still, looking at position set O = c 0,1 , c 1,1 , which is composed of one internal position and one external one, we see that the distribution RefreshA 2 O = a 0 ⊕ $ 0 , a 1 ⊕ $ 0 does depend on more than one share of a. RefreshA 2 is therefore not 2-SNI.

Gadget 2 NI Mask Refreshing with t = 2 function RefreshA2(a) c0,0 ← a 0 ; c1,0 ← a 1 ; c2,0 ← a 2 ; r0 $ ← K; c0,1 ← c0,0 ⊕ r0; c1,1 ← c1,0 r0; r1 $ ← K; c0,2 ← c0,1 ⊕ r1; c2,1 ← c2,0 r1; return c0,2, c1,1, c2,1
Compositional Probing Security This small difference between NI and SNI has a significant effect on security when used in larger circuits. Indeed, the output positions of a strongly non-interfering gadgets do not depend on any of its input positions: when considered independently from internal positions (in the absence of internal probes), their distribution is uniform; and in the presence of internal probes, their joint distribution is entirely determined by that of the probed internal positions. This is essential in supporting compositional reasoning about the probing security of larger algorithms. In particular, this makes algorithms of the form shown in Algorithm 3 (for some gadgets R and G of the appropriate types that work on 2-encodings) easy to prove t-NI if R is RefreshM 2 , and illustrates why composition might fail if R is instantiated with RefreshA 2 . A key observation to make is that an adversary that observes 2 positions internal to G may learn 2 shares of both a and b. If R is instantiated with RefreshA 2 (and is thus only 2-probing secure), the 2 shares of b can be used to infer information about 2 further shares of a, which may give the adversary full knowledge of all 3 shares of a. On the other hand, if R is instantiated with RefreshM 2 (and is thus 2-SNI), the adversary's knowledge of 2 shares of b does not propagate any further back to a, and the algorithm remains secure. Broader uses of SNI The notion of strong non-interference, and the masking transformation we define here have already found applications in follow-up work. Belaïd et al. [START_REF] Belaïd | Randomness complexity of private circuits for multiplication[END_REF] prove using our compositional techniques that their new non-interfering multiplication can be securely combined with the strongly non-interfering one of Rivain and Prouff [START_REF] Rivain | Provably secure higher-order masking of AES[END_REF] to build a strongly non-interfering AES S-box with reduced randomness complexity. Similarly, Goudarzi and Rivain [START_REF] Goudarzi | How fast can higher-order masking be in software?[END_REF] use our method to ensure the compositional security of their bitsliced software implementation of AES. Battistelo et al. [START_REF] Battistello | Horizontal side-channel attacks and countermeasures on the ISW masking scheme[END_REF] use and prove t-SNI for their O(n • log n) mask refreshing gadget, allowing further randomness complexity reductions without loss of probing security. Coron et al. [START_REF] Coron | Faster evaluation of sboxes via common shares[END_REF] use and prove t-SNI for their efficient parallel algorithms for the evaluation of SBoxes.

Outline The rest of the paper is organized as follows. Section 3 formalizes our two-tier language for masked gadgets and algorithms, the notion of position, and their semantics, as well as the joint distribution of a set of positions. Sections 4, and 5 formalize probing security as t-non-interference, and formally define our new notion of t-strongnon-interference before illustrating it more generally with simple examples. In Section 6, we define a language to describe probing policies, and define a simple type system for enforcing probing policies of algorithms, formalizing and generalizing the simple compositional arguments outlined here. In Section 7, we present an automated method to verify the strong non-interference of arbitrary gadgets at small fixed orders, that follows the approach used above in arguing that RefreshM 2 is 2-SNI, and adapts algorithms by Barthe et al. [4] to reduce the number of position sets to consider. In Section 8, we extend our type system into a masking transformation which automatically builds a masked algorithm from an unprotected program, carefully choosing the proper locations for strongly non-interfering refreshing gadgets. We evaluate on full cryptographic algorithms the performance of the type system, of the resulting transformation, and of the transformed algorithms. Section 9 discusses related work on leakage models, composition for probing security, and other masking transformations. We interleave discussions of interesting leads for future work.

Masked algorithms

The formal development of this paper is based on a minimalist 2-tier language. 10 The lower tier models gagdets as sequences of probabilistic and (three-address code) deter- Fig. 1: Syntax of masked algorithms ministic assignments, whereas the upper tier models algorithms as sequences of gadget calls (we assume that each gadget call is tagged with its instruction number ∈ N). The formal definition of the language is given in Figure 1, where we use vector notations ( #» x , . . . ) to denote (t + 1)-tuples of scalar variables, ı to denote indices (such that 0 ≤ ı ≤ t) in such a tuple or in encoding variables, and exponents • ı to denote the projection of a component out of a (t + 1)-tuple (for example a ı , or #» x ı ). We require gadgets and algorithms to be well-formed, in the following sense. A gadget G is well-formed if its body is in SSA form, i.e. its scalar variables appear at most once on the left-hand side of an assignment. An algorithm P is well-formed if all its gadgets are defined and well-formed, and if, in all gadget calls b := G(a 1 , . . . , a n ), variables b, a 1 , . . . , a k are pairwise disjoint. We now turn to the semantics of gadgets and algorithms. Crucially, the semantics of gadgets and algorithms is instrumented to keep track of the joint distribution of all intermediate values computed during execution. Formally, we assume that scalar and encoding variables take values in K and K t+1 , where K is the carrier set of a finite ring (K, 0, 1, ⊕, , ). We let Val = K t+1 denote the set of encoded values. Furthermore, we let A denote the set of encoding variables and define the set of global memories as Mem = A → K t+1 . Likewise, we let V denote the set of scalar variables and define the set of local memories as LMem = V K and extended local memories as ELMem = (N × V) K. Then, the semantics of a gagdet G is a function G that takes as input a global memory and returns a distribution over pairs of local memories and values. Likewise, the semantics of an algorithm P is a function P that takes as input a global memory and returns a distribution over extended local memories and values. The semantics is outlined in Figure 2.

In order to define probing security, we first define a notion of position that corresponds to the intuition illustrated in Section 2. First, we define the set

I = {a ı | a ∈ A, 0 ≤ ı ≤ t} of input
x (m, lm) = lm(x) a ı (m, lm) = m(a) ı x y (m, lm) = lm(x) lm(y) c (m, lm) : D(Mem × LMem) with m ∈ Mem and lm ∈ LMem x ← e (m, lm) = munit(m, lm{x ← e (m, lm)}) x $ ← K (m, lm) = mlet v = U K in munit(m, lm{x ← v}) c1; c2 (m, lm) = mlet (m1, lm1) = c1 (m, lm) in c2 (m1, lm1) G (m) : D(LMem × Val) with m ∈ Mem and G(a1, . . . , an) ::= c; return #» x G (m) = mlet (m1, lm1) = c (m, ∅) in munit(lm1, lm1( #» x )) s (m, elm) : D(Mem × ELMem)
with m ∈ Mem, elm ∈ ELMem and G(a1, . . . , an)

::= c; return #» x b := G(c1, . . . , cn) (m, elm) = mlet (lm1, v) = G (m{(ai) 1≤i≤n ← (m(ci)) 1≤i≤n }) in munit(m{b ← v}, elm elm1)
where elm1 is the map that sets only

elm1( , v) = lm(v) for all v ∈ dom(lm) s1; s2 (m, elm) = mlet (m1, elm1) = s1 (m, elm) in s2 (m1, elm1) P (m) : D(ELMem × Val)
with m ∈ Mem and P (a1, . . . , an ::= s; return b

P (m) = mlet (m1, elm1) = s (m, ∅) in munit(elm1, m1(b))
where m{x1, . . . , xn ← v1, . . . , vn} denotes the map m where xi is updated with vi for each i in increasing order, and denotes the disjoint union of partial maps.

Fig. 2: Semantics of gadgets and algorithms

We first review the basic notion of probabilistic non-interference and state some of its key properties. As usual, we start by introducing a notion of equivalence on memories. Next, we define probabilistic non-interference.

Definition 2 Let G be a gadget, and let

I ⊆ I G and O ⊆ O G . G is (I, O)-non- interfering (or (I, O)-NI), iff G O (m) = G O (m ) for every m, m ∈ Mem s.t. m ∼ I m .
For every gadget G and every position set O, we define the dependency set of O as

depset G (O) = { I | G is (I, O)-NI }; thus, depset G (O) is the smallest set I ⊆ I G such that G is (I, O)-NI. Lemma 1 Let G be a gadget and O ⊆ O G be a set of positions in G. G is (depset G (O), O)- NI.
Proof (sketch). It suffices to show that there exists I such that G is (I, O)-NI and that for every

I and I , if G is (I, O)-NI and (I , O)-NI, then it is also (I ∩ I , O)-NI.
We conclude this section by providing an alternative definition of non-interference, in the style of simulation-based security.

Lemma 2 A gadget G is (I, O)-NI iff there exists a simulator Sim ∈ (I → K) → D(O → K) such that for every m ∈ Mem, G O (m) = Sim(m |I )
where m |I is the restriction of m to elements in I.

Proof. For the direct implication, define S as follows: given a function m ∈ I → K, we let S be G O (m ), where m is any memory that extends m. It is immediate to check that S satisfies the expected property. The reverse direction is immediate. This observation is useful to connect the information-flow based formulation of probing security introduced below with the simulation-based formulations of probing security often used by cryptographers. Indeed, the dependency set depset G (O) can be interpreted as a set of G's input shares that is sufficient to perfectly simulate the joint distribution of positions in O to an adversary.

Next we define our baseline notion of probing security, which we call t-noninterference, and state some of its basic properties. The notion of t-non-interference is based on the notion of degree of an input set, which we define first. Given an input set I and an encoding variable a, we define the set I |a = I ∩ a of positions in I that correspond to shares of a. Further, we define the degree of an input set I as I = max a |I |a | (where | • | is the standard notion of cardinality on finite sets). This notion captures the intuition that the adversary should not learn all shares of any single encoding variable, by bounding the information an adversary may learn about any of a gadget's shared inputs through positions probed internally to that gadget.

Definition 3 (Probing security)

A gadget G is t-non-interfering (or t-NI) whenever depset G (O) ≤ |O| for every O ⊆ O G such that |O| ≤ t.
The next lemma establishes that t-NI is already achieved under a weaker cardinality constraint on the dependency set. Variants of Lemma 3 in simulation-based settings appear in [START_REF] Carlet | Algebraic decomposition for probing security[END_REF][START_REF] Belaïd | Randomness complexity of private circuits for multiplication[END_REF].

Lemma 3 A gadget G is t-NI iff depset G (O) ≤ t for every O ⊆ O G s.t. |O| ≤ t.
Proof. The direct implication follows from transitivity of ≤. The notion of t-non-interference extends readily to algorithms. In addition, one can prove that an algorithm is secure iff the gadget obtained by fully inlining the algorithm is secure.

Lemma 4 A program P is t-NI iff the gadget inline(P ) obtained by full inlining is t-NI.
The lemma sheds some intuition on the definition of t-NI for algorithms. However, we emphasize that verifying fully inlined algorithms is a bad strategy; in fact, previous work indicates that this approach does not scale, and that composition results are needed.

Strong Non-Interference

We introduce strong non-interference, a reinforcement of probing security based on a finer analysis of cardinality constraints for dependency sets. Informally, strong noninterference distinguishes between internal and output positions, and requires that the dependency set of a position set O has degree ≤ k, i.e. contains at most k shares of each encoding input, where k is the number of internal positions in O. Formally, a local variable is an output position for G if it appears in the return tuple of G, and an internal position otherwise. Let O int (resp. O ext ) denote the subset of internal (resp. output) positions of a set O. Strong t-non-interference requires that the degree of depset(O) is smaller than |O int |, rather than |O|. Intuitively, a t-SNI gadget information-theoretically hides dependencies between each of its inputs and its outputs, even in the presence of internal probes. This essential property is what supports compositional reasoning.

Definition 4 (Strong probing security)

A gadget G is t-strongly non-interfering (or t-SNI) if depset G (O) ≤ |O int | for every position set O such that |O| ≤ t.
Fortunately, many gadgets from the literature achieve strong non-interference (see Table 1 andSection 7). First, we note that gadget RefreshM (Gadget 4b) generalized from Ishai, Sahai and Wagner [START_REF] Ishai | Private circuits: Securing hardware against probing attacks[END_REF] is t-SNI for all t. (A proof sketch for this proposition is given in Appendix C.)

Gadget 4 Mask Refreshing Gadgets 0: function RefreshA(a) 1: c 0 ← a 0 2: for i = 1 to t do 3: r $ ← K 4: c 0 ← c 0 ⊕ r 5: c i ← a i r 6: return c (4a) Addition-Based Mask Refreshing 0: function RefreshM(a) 1: for i = 0 to t do 2: c i ← a i 3: for i = 0 to t do 4: for j = i + 1 to t do 5: r $ ← K 6: c i ← c i ⊕ r 7: c j ← c j r 8: return c (4b) Multiplication-Based Mask Refreshing Proposition 1 RefreshM (Gadget 4b) is t-SNI.
On the contrary, the additive refreshing gadget RefreshA (Gadget 4a) achieves NI but fails to achieve SNI. Interestingly, Coron's linear-space variant of Ishai, Sahai and Wagner's multiplication [12, The proofs of Propositions 1, 2 and 3 have been machine-checked using Easy-Crypt [START_REF] Barthe | EasyCrypt: A tutorial[END_REF]. We also provide more detailed game-based proof sketches in the full version of this paper.

Strong Non-Interference for Mask Refreshing We now show how choosing a t-SNI refreshing gadget over a t-NI refreshing gadget critically influences the security of algorithms. Concretely, we provide a separating example, which captures the essence of the flaw in the inversion algorithm of Rivain and Prouff [START_REF] Rivain | Provably secure higher-order masking of AES[END_REF]. The example considers two algorithms (Algorithm 5) which compute a cube in GF(2 8 ) by squaring and multiplying (using, for illustration purposes, some t-NI gadgets Square and Mult for squaring and multiplication). Both algorithms use a refreshing gadget between the two operations, but they differ in which gadget they use: BadCube (Gadget 5a) uses the additive refreshing gagdet RefreshA, which is t-NI but not t-SNI, and Cube (Gadget 5b) uses the RefreshM gadget, which is t-SNI. This simple difference is fundamental for the security of the two algorithms.

Alg. 5 Cubing procedures (with

K = GF(2 8 )) function BadCube(x) y1 := Square(x) y2 := RefreshA(y1) z := Mult(x, y2) return z (5a) Insecure Cubing function Cube(x) y1 := Square(x) y2 := RefreshM(y1) z := Mult(x, y2) return z (5b) Secure Cubing Lemma 5 ([15]) BadCube is not t-NI for any t ≥ 2. Cube is t-NI for all t.
Coron et al. [START_REF] Coron | Higher-order side channel security and mask refreshing[END_REF] exhibit proofs for both statements. In Appendix C, we give a compact proof of t-NI for Cube that does not exhaustively consider all (t + 1)-tuples of positions in Cube. The key argument is that RefreshM being t-SNI essentially renders useless any information on y 2 the adversary may have learned from observing positions in Mult: those do not add any shares of y 1 to the dependency set we compute for RefreshM, and therefore do not influence the shares of x that appear in the final dependency set for Cube. On the other hand, using a simple t-NI mask refreshing gadget (such as RefreshA) in its place breaks the proof by allowing us to deduce only that each position in the multiplication may depend on 2 shares of x.

In Section 6, we show how the proof of Lemma 5 can be improved and extended into a compositional proof for the (repaired) inversion algorithm of Rivain and Prouff [START_REF] Rivain | Provably secure higher-order masking of AES[END_REF], and, in fact, outlines a general mehodology for proving algorithms t-NI or t-SNI.

A Generic Composition Result Before formalizing and automating this proof process to obtain precise probing security proofs for large circuits, we now give a coarse but simple composition result that illustrates the generality of SNI. Informally, an algorithm is t-NI if all its gadgets verify t-NI and every non-linear usage of an encoding variable is guarded by t-SNI refreshing gadgets. In addition, it shows that processing all inputs, or the output of a t-NI algorithm with a t-SNI gadget (here RefreshM) suffices to make the algorithm t-SNI.

Proposition 4 An algorithm P is t-NI provided all its gadgets are t-NI, and all encoding variables are used at most once as argument of a gadget call other than RefreshM. Moreover P is t-SNI if it is t-NI and one of the following holds:

its return expression is b and its last instruction is of the form b := RefreshM(a); its sequence of encoding parameters is (a 1 , . . . , a n ), its i th instruction is b := i RefreshM(a i ) for 1 ≤ i ≤ n, and a i is not used anywhere else in the algorithm.

Definition 5 (Probing policy) 1. A probing assertion is a pair (Γ, φ), where Γ is a map from encoding variables to expressions in the theory of finite sets, and φ is a cardinality constraint. Each probing assertion (Γ, φ) defines a set of subsets of positions for a fixed algorithm P , denoted by (Γ, φ) . (The syntax and semantics of set expressions and cardinality constraints is explained below.) 2. A probing policy is a pair of assertions

(Γ in , φ in ) ⇐= (Γ out , φ out )
where (Γ out , φ out ) is the post-assertion and (Γ in , φ in ) is the pre-assertion.

Algorithm P satisfies the policy

(Γ in , φ in ) ⇐= (Γ out , φ out ), written P |= (Γ in , φ in ) ⇐= (Γ out , φ out ), if for every position set O ∈ (Γ out , φ out ) , P is (I, O)-NI for some input position set I ∈ (Γ in , φ in ) .
The syntax of set expressions and cardinality constraints is given by the following grammar: (set expr.)

S := X | ∅ | S ∪ S (arith. expr.) l := |S| | |O | | t | l + l (cardinality constr.) φ := l ≤ l | φ ∧ φ
The syntax distinguishes between variables X that are drawn from a set X of names-that we will use to represent sets of shares of an encoding variable, and variables O, annotated with a label , that are drawn from a disjoint set Ω of names-that we will use to represent sets of internal positions probed in the gadget used at instruction . Remark 1 Our syntax for set expressions and constraints is a fragment of the (decidable) theory of finite sets with cardinality constraints. It would be possible to include other set-theoretical operations, as in [START_REF] Calogero | Combining sets with cardinals[END_REF][START_REF] Bansal | A new decision procedure for finite sets and cardinality constraints in SMT[END_REF]. However, we have found our core fragment sufficient for our purposes.

The semantics of assertions is defined using the notion of valuation. A valuation µ is a mapping from names in X and Ω to finite sets, such that ∀ X ∈ X . µ(X) ⊆ {0, . . . , t} and ∀ O ∈ Ω. µ(O ) ⊆ O G , where G is the gadget called at instruction . Every valuation µ defines, for every set expression S, a set of share indices µ(S) ⊆ {0, . . . , t} and for every arithmetic expression l an interpretation µ(l) ∈ N, using the intended interpetation of symbols (i.e. ∪ is interpreted as set union, + is interpreted as addition, . . . ).

Definition 6 (Interpretation of assertions)

1. µ satisfies a cardinality constraint φ,

written µ |= φ, if µ(l 1 ) ≤ µ(l 2 ) for every conjunct l 1 ≤ l 2 of φ. 2. The interpretation of Γ under µ is the set µ(Γ ) = a {a ı | ı ∈ µ(Γ (a))} ∪ O µ(O)
3. The interpretation of (Γ, φ) is the set

(Γ, φ) = {µ(Γ ) | µ |= φ}
We now turn to the definition of the type system. Definition 7 Algorithm P (a 1 , . . . , a n ) ::= s; return r has type (Γ in , φ in ) ⇐= (Γ out , φ out ) if the judgment s : (Γ in , φ in ) ⇐= (Γ out , φ out ) is derivable using the typing rules from Figure 3. We denote this fact P : (Γ in , φ in ) ⇐= (Γ out , φ out ).

We briefly comment on the rules. Rule (SEQ) is used for typing the sequential composition of gadget calls and is as expected. The remaining rules are used for interpreting the non-interference properties of gadgets. We now detail them.

G is t-NI φout ⇒ |Γout(b)| + |O | ≤ t Γ in := Γout{b, (a k ) 1≤k≤n ← ∅, (Γout(a k ) ∪ X k ) 1≤k≤n } b := G(a1, . . . , an) : (Γ in , φout ∧ ( 1≤k≤n |X k | ≤ |Γout(b)| + |O |)) ⇐= (Γout, φout) (NI-GADGET) G is t-SNI φout ⇒ |Γout(b)| + |O | ≤ t Γ in := Γout{b, (a k ) 1≤k≤n ← ∅, (Γout(a k ) ∪ X k ) 1≤k≤n } b := G(a1, . . . , an) : (Γ in , φout ∧ ( 1≤k≤n |X k | ≤ |O |)) ⇐= (Γout, φout) (SNI-GADGET) G is affine Γ in := Γout{b, (a k ) 1≤k≤n ← ∅, (Γout(a k ) ∪ Γout(b) ∪ X ) 1≤k≤n } b := G(a1, . . . , an) : (Γ in , φout ∧ |X | ≤ |O |) ⇐= (Γout, φout) (AFFINE)
where Γ {∀ k. v k ← ∀ k. e k } stands for the map Γ where each v k is updated to map to e k and all other indices are left untouched.

Fig. 3: Typing rules Rule (SNI-GADGET) is used for typing calls to a SNI-gadget with an arbitrary post-assertion and a pre-assertion in which the mapping Γ out is updated to reflect the dependencies created by the call, and the constraint is strenghtened with the cardinality constraint imposed by strong non-interference. The rule has a side condition |O | + |Γ out (b)| ≤ t ensuring that the total number of positions whose dependency set by G we are considering is bounded by t, where O is the name of the subset of positions that are observed in the current gadget (called at line ), and Γ out (b) is the set of shares of b the adversary has information about from positions probed in gadgets that use b later on in the algorithm. This side condition is verified under the condition φ out . Note that the variables X k are fresh, and annotated with the label that identifies the current instruction, and an indice k that identifies the argument. Rule (NI-GADGET) is similar but deals with NI-gadgets, and therefore extends Γ in with correspondingly weaker constraints on the X k .

We now turn to the rule for affine gadgets. Informally, we say that a gadget is affine if it manipulates its input encodings share by share; this includes standard implementations of ring addition, for example, but also of many other functions that are linear in K (for example, multiplication by a constant-or public-scalar, or shifts in the representation when addition is bitwise). Formally, we say that a gadget G with parameters (a 1 , . . . , a n ) is affine iff there exists a family of procedures f 0 , . . . , f t such that G is an inlining of x 0 ← f 0 (a 0 1 , . . . , a 0 n ); . . . ; x t ← f t (a t 1 , . . . , a t n ); return x 0 , . . . , x t ; Thus, one can define a mapping η : O G → {0, . . . , t} such that for every position π ∈ O G , η(π) = ı if π occurs in the computation of the ı th share (i.e. in the computation of f ı (a ı 1 , . . . , a ı n )). The fine-grained information about dependencies given by this notion of affinity is often critical to proving the probing security of algorithms. Therefore, it is important to capture affinity in Definition 8 (Typing of an algorithm) Let P be an algorithm with a definition of the form P (a 1 , . . . , a n ) ::= s; return r.

P is well-typed for NI, written NI P , whenever there exist Γ in , φ in such that

P : (Γ in , φ in ) ⇐= (∅, 1≤ ≤|P | |O | ≤ t) and, for each i ∈ {1, . . . , n}, φ in ⇒ |Γ in (a i )| ≤ t.
P is well-typed for SNI, written SNI P , whenever there exist Γ in , φ in such that

P : (Γ in , φ in ) ⇐= ([r ← O], |O| + 1≤ ≤|P | |O | ≤ t) and, for each i ∈ {1, . . . , n}, we have φ in ⇒ |Γ in (a i )| ≤ 1≤ ≤|P | |O | (where [v ← x]
is the map that associates x to v and is everywhere else undefined).

When typing for NI, we start from the empty map for Γ out and simply consider any output position observed as if they were internal. However, the same cannot be done when typing for SNI since we need to distinguish clearly between internal positions in one of the O , used to type the gadget at instruction , and output positions in O, initially used as the set of position of the algorithm's return encoding. 4, with some information relevant to its typing derivation. We recall that the function x → x 2 n is linear (for any n) in binary fields and rely on affine gadgets pow2, pow4, and pow16 to compute the corresponding functionalities.

We present the typing derivation in the slightly unusual form of a table, in Figure 4, which shows the code of the inversion algorithm along with the values of Γ in and φ in (φ in shows only the part of the constraint that is added at that program point, not the entire constraint) at each program point. By the sequence rule, these serve as Γ out and φ out for the immediately preceding program point. The table also shows the side conditions checked during the application of gadget rules where relevant. It is easier to understand the type-checking process by reading the table from the bottom up.

As per the definition of well-typedness for SNI, we start from a state where the output position set O is associated to the algorithm's return encoding r 5 , and where the constraint contains only the global constraint that the whole position set O ∪ O is of cardinality bounded by t. When treating line 9, we know that SecMult is t-SNI and try to apply rule (SNI-GADGET). We check that the number of positions observed in this instance of SecMult is bounded by t (which trivially follows from the global constraint), and construct the new value of (Γ in , φ in ) following the rule: since neither of the call's input encodings are used below, new sets X 9 1 and X 9 2 are associated to the call's inputs and the SNI constraints are added to φ in . Applying the rules further until the top of the program is reached, and performing the appropriate set unions in Γ when an encoding variable is used more than once, we observe that the resulting pre-assertion is such that

|Γ in (a)| ≤ |O 1 | + |O 2 | + |O 3 | + |O 9 | ≤
O , and therefore proves that this inversion algorithm is t-SNI.

Γ in φ in Instructions Side conditions function invert(a) a : X ∪ X 9 2 ∪ X 2 1 ∪ X 1 |X 1 | ≤ |O 1 | z1 :=1 pow2(a) a : X ; z1 : X 9 2 ∪ X 2 1 |X 2 1 | ≤ |O 2 | z2 :=2 Refresh(z1) |X 3 1 | + |O 2 | ≤ t a : X ; z1 : X 9 2 ; z2 : X 3 1 |X 3 k | ≤ |O 3 | r1 :=3 SecMult(z2, a) |X 6 1 ∪ X 8 2 ∪ X 5 1 ∪ X 4 | + |O 3 | ≤ t z1 : X 2 ; r1 : X 6 1 ∪ X 8 2 ∪ X 5 1 ∪ X 4 |X 4 | ≤ |O 4 | w1:=4 pow4(r1) z1 : X 2 ; r1 : X 6 1 ; w1 : X 8 2 ∪ X 5 1 |X 5 1 | ≤ |O 5 | w2:=5 Refresh(w1) |X 6 2 | + |O 5 | ≤ t z1 : X 2 ; r1 : X 6 1 ; w1 : X 8 2 ; w2 : X 6 2 |X 6 k | ≤ |O 6 | r2 :=6 SecMult(r1, w2) |X 8 1 ∪ X 7 | + |O 6 | ≤ t z1 : X 2 ; w1 : X 8 2 ; r2 : X 8 1 ∪ X 7 |X 7 | ≤ |O 7 | r3 :=7 pow16(r2) z1 : X 2 ; w1 : X 8 2 ; r3 : X 8 1 |X 8 k | ≤ |O 8 | r4 :=8 SecMult(r3, w1) |X 9 1 | + |O 8 | ≤ t z1 : X 2 ; r4 : X 9 1 |X 9 k | ≤ |O 9 | r5 :=9 SecMult(r4, z1) |O| + |O 9 | ≤ t r5 : O |O| + 1≤ ≤9 |O | ≤ t return r5
Fig. 4:

a -1 in GF(2 8 )
Finally, one can remark that the instances of SecMult at line 6 and 8 do not in fact need to be t-SNI. As pointed out by Belaïd et al. [START_REF] Belaïd | Randomness complexity of private circuits for multiplication[END_REF], using a t-NI multiplication gadget at these program points is sufficient to construct a type derivation for SNI.

SNI Checker for Gadgets

We present an automated method for proving that gadgets (or small algorithms, by inlining) are t-SNI at small fixed orders (up to t = 6 for ring multiplication). We then give some experimental results.

Verification algorithm

We adapt to t-SNI the algorithmic contributions of Barthe et al. [START_REF] Barthe | Verified proofs of higher-order masking[END_REF] that support the automated verification, on small to medium gadgets and for small orders, of Ishai, Sahai and Wagner's circuit privacy property [START_REF] Ishai | Private circuits: Securing hardware against probing attacks[END_REF], which is similar to our t-NI. Their work builds on two observations: first, every probabilistic program P taking input x and performing a (statically) bounded number (say q) of uniform samplings over K is equivalent, in the sense below, to composing a deterministic program P † taking inputs x and r with random sampling over K q . Formally, for every x,

P (x) = mlet r = U K q in P † O (x, r)
Second, P satisfies (I, O)-NI iff there exists a function f such that for every x 1 , x 2 and r, such that x 1 ∼ I x 2

P † O (x 1 , r) = P † O (x 2 , f (x 2 , r))
and moreover f (x, •) is a bijection for every x. The latter equality can be easily verified for all x and r using standard tools, therefore the key to proving non-interference is to exhibit a suitable function f . Their algorithm proceeds by incrementally defining bijections f 1 , . . . , f n satisfying the two conditions above until evenutally P † O (x, f n (x, r)) can be rewritten into an expression that does not depend syntactically on secrets.

However, even with efficient algorithms to prove that a program P is (I, O)-NI for some position set O, proving that P is t-NI remains a complex task: indeed this involves proving (I, O)-NI for all O with |O| ≤ t. Simply enumerating all possible position sets quickly becomes untractable as P and t grow. Therefore, [START_REF] Barthe | Verified proofs of higher-order masking[END_REF] uses the following fact: if P is (I, O )-NI then it is also (I, O)-NI for all O ⊆ O . Hence, checking that P is (I, O )-NI for some large set O is sufficient to prove that P is (I, O)-NI for every O ⊆ O , and this using only one proof of non-interference. In particular, they exhibit algorithms that rely on the explicit construction of the bijection f n to efficiently extend the set O from which it was constructed into a potentially much larger set O for which that bijection still proves (I, O )-NI. Further, they also exhibit algorithms that rely on such extensions to prove the existence of I such that (I, O)-NI for all position sets O much more efficiently than by considering all position sets individually.

We adapt their algorithms by changing the core bijection-finding algorithm in two ways: i. rather than being applied to a modified program that includes the initial uniform sampling of secret encodings, our core algorithm works directly on the gadget description (this is necessary to ensure that we prove t-SNI instead of alternative security notions); and ii. our search for a bijection stops when P † O (x, f n (x, r)) can be simplified into an expression that syntactically depends on at most d shares of the secret (for the desired bound d on I , that is d = |O int | for SNI), rather than stopping when all syntactic dependencies on the secret input have been removed. We note that replacing the bound d from the second point with d = t yields a verification algorithm for t-NI (by Lemma 3). Our full algorithm is given in App. B.

Evaluation We evaluate the performance of our SNI verifier on some medium and small gadgets: SecMult, Coron's linear-memory ring multiplication algorithm [12,

Masking Transformation

As a proof of concept, we implement our type system for a comfortable subset of C that includes basic operators, static for loops, table lookups at public indices, and mutable secret state, and extended with libraries that implement core gadgets for some choices of K. Moreover, we define a source-to-source certifying masking transformation, which takes an unprotected program and returns a masked algorithm accepted by our type system, selectively inserting refreshing gadgets as required for typing to succeed. We note that the transformation itself need not be trusted, since its result is the final program on which typing is performed. Furthermore, the choice of C as a supporting language is for convenience, since many of the algorithms we consider have reference implementations written in C. In particular, we do not claim that compiling and executing the C programs produced by our masking transformation will automatically yield secure executables: our verification results are on algorithms described in the C language rather than on C programs in general. Making use of these verification results in practice still requires to take into account details not taken into account in the probing model. Although an important problem, this is out of the scope of this paper and a research area on its own: for example Balasch et al. [START_REF] Balasch | On the cost of lazy engineering for masked software implementations[END_REF] consider some of the issues involved in securely implementing probing secure algorithms.

Implementation

We now give an overview of the different passes performed by our masking transformation. The input programs use explicit typing annotations to distinguish public variables (for example, public inputs, or public loop indices) from sensitive or secret variables that must be encoded. We call public type any type outside of those used for denoting variables that must be encoded.

Parsing and Pre-Typing This pass parses C code into our internal representation, checks that the program is within the supported subset of C, performs C type-checking and checks that variables marked as sensitive (variables given type K) are never implicitly cast to public types. Implicit casts from public types to K (when compatible, for example, when casting a public uint8 t to a protected variable in GF(2 8)) are replaced with public encoding gadgets (that set one share to the public value and all other shares to 0).

Gadget Selection and Generic Optimizations

This pass heuristically selects optimal gadgets depending on their usage. For example, multiplication of a secret by a public value can be computed by an affine gadget that multiplies each share of the secret, whereas the multiplication of two secrets must be performed using the SecMult gadget. Further efforts in formally proving precise types for specialized core gadgets may also improve this optimization step. Since the encoding replaces scalar-typed variables (passed by value) with array-typed variables (passed by reference), it is also necessary to slightly transform the program to ensure the correctness of the resulting program. In addition, we also transform the input program into a form that more closely follows the abstract language from Figure 1, which makes it easier to type-check.

Type Inference and Refresh Insertion This is the core of our transformation. We implement a type inference algorithm for the type system of Section 6. The algorithm simplifies policies on the fly, supports inferred types on sub-algorithms as gadget-invocation types, and fails when the simplified policy is inconsistent. Failure arises exactly when a refreshing operation is needed. At the cost of tracking some more information and reinforcing the typing constraint on sub-algorithms, we use this observation to automatically insert Refresh gadgets where required. When type inference fails, the variable whose masks need to be refreshed is duplicated and one of its uses is replaced with the refreshed duplicate. To avoid having to re-type the entire program after insertion of a refresh gadget, our transformation keeps track of typing information for each program point already traversed and simply rewinds the typing to the program point immediately after the modification.

Code Generation Finally, once all necessary mask refreshing operations have been inserted and the program has been type-checked, we produce a masked C program. This transformation is almost a one-to-one mapping from the instructions in the type-checked programs to calls to a library of verified core gadgets or to newly defined gadgets. Some cleanup is performed on loops to clarify the final code whenever possible, and to remove initialization code on normalized gadgets. Interestingly, our transformation produces a (set of) C files that is parameterized by the masking order t. Producing executable versions of that algorithm at a particular order, for example to evaluate its performance, is as easy as defining a pre-processor macro at compile-time.

Practical Evaluation

To test the effectiveness of our transformation, we apply it to different algorithms, generating equivalent masked algorithms at various orders. We apply our transformation to the following programs: AES ( ), a full computation (10 rounds including key schedule) of AES-128 masked using the multiplication gadget, and implemented in GF(2 8 ); AES (x g(x)), a full computation (10 rounds including key schedule) of AES-128 masked using Coron et al.'s gadget for computing x g(x), and implemented in GF(2 8 ); Keccak, a full computation (24 rounds) of Keccak-f[1600], implemented in GF(2 64 ); Simon, a block of Simon(128,128), implemented in GF(2 64 ); Speck, a block of Speck(128,128), implemented in GF(2) 64 , and using one of the following modular addition algorithms; AddLin, Coron, Großschädl and Vadnala's algorithm [START_REF] Coron | Secure conversion between boolean and arithmetic masking of any order[END_REF] for the computation of modular addition on boolean-masked variables (in GF(2) 64 ); AddLog, Coron et al.'s improved algorithm [START_REF] Coron | Conversion from arithmetic to boolean masking with logarithmic complexity[END_REF] for the computation of modular addition on boolean-masked variables (in GF(2) 64 ). We first discuss the performance of our verifier and the verification results before discussing the practical significance, in terms of time, memory and randomness complexity of our masking transformation. Finally, we discuss examples on which our tool implementation could be improved.

Verification Performance and Results

Table 2 shows resource usage statistics for generating the masked algorithms (at any order) from unprotected implementations of each algorithm. The table shows the number of mask refreshing operations inserted in the program 12 , the compilation time, and the memory consumption. For Keccak, we show two separate sets of figures: the first, marked "no refresh", is produced by running our algorithm transformer on a bare implementation of the algorithm; the second, marked "refresh in χ", is produced by running our tool on an annotated implementation, where a mask refreshing operation is manually inserted in the χ function and the tool used for verification only. We discuss discrepancies between the numbers on these two lines in Section 9, and consider the "refresh in χ" set of statistics in all discussions until then. We first note the significant improvements these results represent over the state of the art in formal verification for probing security. Indeed, our closest competitor [START_REF] Barthe | Verified proofs of higher-order masking[END_REF] report the verification of all 10 rounds of AES (including key schedule) at order 1 in 10 minutes, and could not verify all 10 rounds for higher orders. In contrast, our tool verifies the probing security of Rivain and Prouff's algorithm [START_REF] Rivain | Provably secure higher-order masking of AES[END_REF] as fixed by Coron et al. [START_REF] Coron | Higher-order side channel security and mask refreshing[END_REF] at all orders in less than a second. 13 Further, we note that the masked algorithms our transformation produce for modular addition are the first such algorithms known to be t-probing secure using only t + 1 shares. Indeed, the original proofs [START_REF] Coron | Secure conversion between boolean and arithmetic masking of any order[END_REF][START_REF] Coron | Conversion from arithmetic to boolean masking with logarithmic complexity[END_REF] rely on the ISW framework and make use of 2t + 1 shares to obtain t-probing security. We further note that Coron, Großschädl and Vadnala's algorithm [START_REF] Coron | Secure conversion between boolean and arithmetic masking of any order[END_REF] does not require the insertion of mask refreshing operations, and is thus t-probing secure with t + 1 shares as it was originally described. Finally, we note that, to the best of our knowledge, the results obtained on Keccak, Simon and Speck constitute the first generic higher-order masking schemes for these algorithms. Performance of Masked Algorithms Table 3 reports the time taken to execute the resulting programs 10,000 times at various orders on an Intel(R) Xeon(R) CPU E5-2667 0 @ 2.90GHz with 64GB of memory running Linux (Fedora). As an additional test to assess the performance of the generated algorithms at very high orders, we masked an AES computation at order 100: computation took ∼0.11 seconds per block. For AES and Speck, the figures shown in the "unmasked" column are execution times for the input to our transformation: a table-based implementation of AES or an implementation of Speck that uses machine arithmetic, rather than Coron, Großschädl and Vadnala's algorithm would be much faster, but cannot be masked directly using our transformation. Although these observations do highlight the cost of security, we note that using RefreshA when masking the AES SBox does not incur a significant timing gain for any of the masking orders we tested (t ≤ 20). However, the randomness cost is greatly reduced, which may be significant in hardware or embedded software settings. Further research in reducing the randomness cost of SNI mask refreshing, or of other gadgets, serves to make security less costly [START_REF] Belaïd | Randomness complexity of private circuits for multiplication[END_REF][START_REF] Andrychowicz | Circuit compilers with O(1/ log(n)) leakage rate[END_REF][START_REF] Battistello | Horizontal side-channel attacks and countermeasures on the ISW masking scheme[END_REF]. We also confirm the 15% timing improvements reported by Coron et al. [START_REF] Coron | Higher-order side channel security and mask refreshing[END_REF] when implementing the AES SBox using their gadget for computing x g(x). We now look more closely at statistics for the modular addition algorithms AddLin and AddLog and their effects on the performance of masked algorithms for Speck. We first note that proving AddLog t-NI requires the addition of a mask refreshing gadget, whereas AddLin does not. Despite this additional cost, however, AddLog is better than AddLin when word size k grows, since it saves k -log(k) multiplications and replaces them with a single mask refreshing operation. These performance gains on modular addition become overwhelming when seen in the context of a masked algorithm for Speck, which computes one 64-bit modular addition per round. It would be interesting to consider using our transformer to produce masked algorithms for other efficient circuits for modular addition [START_REF] Lynch | Binary adders[END_REF] and measure their performance impact in terms of randomness, time and memory when masked.

Discussions and Related Work

Here, we further discuss the relation between the definitions and results reported here and existing and future work in theoretical and practical cryptography. Our discussions focus mainly on: i. adversary and leakage models; ii. compositional security notions; iii. theoretical and practical masking transformations; and iv. limitations of our definitions and tools.

Adversary and Leakage Models for Masking

We have considered security in the probing model of Ishai, Sahai and Wagner [START_REF] Ishai | Private circuits: Securing hardware against probing attacks[END_REF], which is particularly well-suited to automated analysis due to its tight relation to probabilistic non-interference. In particular, our notion of t-NI is equivalent to the notions of t-probing security and perfect t-probing security used by Carlet et al. [START_REF] Carlet | Algebraic decomposition for probing security[END_REF] and others [START_REF] Rivain | Provably secure higher-order masking of AES[END_REF][START_REF] Coron | Higher-order side channel security and mask refreshing[END_REF].

Despite its broad usage in the literature, the practical relevance of the probing model is not immediately obvious: in practice, side-channel adversaries observe leakage traces, which contain noisy information about all intermediate computations, rather than precise information about some. This threat model is much more closely captured by the noisy leakage model, first introduced by Chari et al. [START_REF] Chari | Towards sound approaches to counteract power-analysis attacks[END_REF] and extended by Prouff and Rivain [START_REF] Prouff | Masking against side-channel attacks: A formal security proof[END_REF]. The noisy leakage model is much more complex and makes security proofs on masked algorithms significantly more involved, and much harder to verify.

Duc, Dziembowski and Faust [START_REF] Duc | Unifying leakage models: From probing attacks to noisy leakage[END_REF] show that proving probing security allows one to estimate the practical (noisy leakage) security of a masked algorithm. While Duc, Faust and Standaert [START_REF] Duc | Making masking security proofs concrete -or how to evaluate the security of any leaking device[END_REF] empirically show that some of the factors of Duc et al.'s bound [START_REF] Duc | Unifying leakage models: From probing attacks to noisy leakage[END_REF] are likely proof artefacts, the remainder of the bound, and in particular a factor that includes the size of the circuit, seems to be tight. Intuitively, Duc et al. [START_REF] Duc | Making masking security proofs concrete -or how to evaluate the security of any leaking device[END_REF] essentially show that the probing security order gives an indication of the smallest order moment of the distribution over leakage traces that contains information about the secret, whereas the size of the circuit the adversary can probe is an indicator of how easy it is to evaluate higher-order moments.

Composition, and Region and Stateful Probing This observation makes clear the importance of also considering more powerful probing adversaries that may place t probes in each of some (pre-determined) regions of an algorithm (the t-region probing model).

For example, each core gadget (field operations and mask refreshing operation) could be marked off as a separate region (as in [START_REF] Duc | Unifying leakage models: From probing attacks to noisy leakage[END_REF]). More recently, and in work contemporary with that presented here, Andrychowicz, Dziembowski and Faust [START_REF] Andrychowicz | Circuit compilers with O(1/ log(n)) leakage rate[END_REF] consider a more general notion of region whose size must be linear in the security parameter (and masking order), and exhibit a mask refreshing gadget that is linear in size and fulfills, in the probing model, the reconstructibility and re-randomization properties from Faust et al. [START_REF] Faust | Protecting circuits from leakage: the computationally-bounded and noisy cases[END_REF]. We now discuss the implications of reconstructibility and re-randomization, and their relation to our notion of SNI, based on the similarity of Prop. 4 with Ishai et al.'s remark on "Re-randomized outputs" [START_REF] Ishai | Private circuits: Securing hardware against probing attacks[END_REF], before discussing the applicability of SNI to security in the region and stateful probing models [START_REF] Ishai | Private circuits: Securing hardware against probing attacks[END_REF].

Intuitively, a gadget is t-reconstructible whenever any t of its positions can be simulated using only its (shared) inputs and outputs, and a gadget is re-randomizing whenever its output encoding is uniform and t-wise independent even if its input encoding is completely known. Our SNI notions combines both considerations. Formulating it in similar terms, a gadget is t-SNI whenever any t of its positions can be simulated using only its (shared) inputs, and if its output encoding is uniform and (t -d)-wise independent even if d shares of each of its inputs are known (for all d such that 0 ≤ d < t). Expressed in this way, it is clear that SNI is slightly weaker than "reconstructible and re-randomizable" in the probing model. This allows us to automatically verify that a gadget is SNI for some fixed t, whereas reconstructibility and re-randomization are more complex. In addition, the ability to combine the use of SNI and weaker (NI or affine) gadgets in a fine-grained way allows us to more precisely verify the security of large algorithms in models where the adversary can place t probes in the entire algorithm. We leave a formal investigation of the relation between SNI and "reconstructibility and re-randomization" as future work.

Based on reconstructibility and re-randomization, Faust et al. [START_REF] Faust | Protecting circuits from leakage: the computationally-bounded and noisy cases[END_REF][START_REF] Andrychowicz | Circuit compilers with O(1/ log(n)) leakage rate[END_REF] prove elegant and powerful composition results that in fact apply in the more powerful region probing and stateful probing models [START_REF] Ishai | Private circuits: Securing hardware against probing attacks[END_REF], where the adversary may (adaptively) place t probes in each region (or in each subsequent iteration) of the algorithm. It is worth noting that our SNI notion also enables composition in these two models: indeed, it is easy to see that any two 2t-SNI algorithms (our regions) can be composed securely when the adversary can place t probes in each of them. Further, our composition techniques also support elegant constructions that support compositional security proofs in the region and stateful probing models without doubling the number of shares computations are carried out on (instead, simply doubling the number of shares at region boundaries). We give details of these robust composition results in Appendix D. Depending on the size of regions that are considered, these robust composition results may bring significant performance gains in terms of randomness and time complexity.

Finally, our notion of SNI and the automated verification techniques presented allow the efficient, precise and automated verification of t-SNI inside each region, an issue which is not addressed by the works of Faust et al. [START_REF] Faust | Protecting circuits from leakage: the computationally-bounded and noisy cases[END_REF][START_REF] Andrychowicz | Circuit compilers with O(1/ log(n)) leakage rate[END_REF].

Existing Masking Transformations Ishai, Sahai and Wagner [START_REF] Ishai | Private circuits: Securing hardware against probing attacks[END_REF] and others [START_REF] Duc | Unifying leakage models: From probing attacks to noisy leakage[END_REF][START_REF] Andrychowicz | Circuit compilers with O(1/ log(n)) leakage rate[END_REF] also propose simple masking transformations that turn unprotected algorithms (or boolean or arithmetic circuits) into protected masked algorithms. Ishai, Sahai and Wagner [START_REF] Ishai | Private circuits: Securing hardware against probing attacks[END_REF] forgo the use of mask refreshing gadgets by doubling the number of shares on which masked computations occur-with a quadratic impact on performance and randomness complexity. Faust et al. [START_REF] Duc | Unifying leakage models: From probing attacks to noisy leakage[END_REF][START_REF] Andrychowicz | Circuit compilers with O(1/ log(n)) leakage rate[END_REF] rely on making sure that all gadgets used in the masked algorithm are reconstructible and re-randomizing. This guarantees security in a stronger probing model, but incurs an even greater loss of performance. By contrast, our transformation attempts to decide whether a mask refreshing operation is required to ensure security in the probing model, and our core contributions (the notion of SNI and the type-checker) do support composition in stronger probing models, whilst still allowing the proofs of security within regions to be handled precisely.

Coron [START_REF] Coron | Higher order masking of look-up tables[END_REF] proposes schemes for masking lookups at secret or sensitive indices in public tables. We have not investigated whether or not the proposed algorithms are SNI or simply NI, and whether or not establishing these properties can be done by adapting our type-system or if it should be done in a different way (either as a direct proof or using the checker from Section 7). We note in passing that part of the result by Coron [START_REF] Coron | Higher order masking of look-up tables[END_REF], namely that using RefreshIter 2t+1 2t between each query to the masked S-box supports security in the stateful probing model is subsumed and improved by the robust composition results described in the full version.

The security analysis of masking schemes in the t-probing model is connected to techniques from multi-party computation, exploited in parallel lines of research by threshold implementations [START_REF] Nikova | Secure hardware implementation of nonlinear functions in the presence of glitches[END_REF][START_REF] Begül Bilgin | Higher-order threshold implementations[END_REF]. In particular, higher-order threshold implementations are exposed to similar security issues due to composition, although they offer additional protection against practical considerations not captured in standard probing models, namely glitches. We believe that the results discussed here are in fact applicable to the compositional security analysis of threshold implementations but leave a formal investigation of these links as future work.

A Code for Gadgets Listed in the Paper Gadget 7 Masked multiplication [START_REF] Coron | Higher order masking of look-up tables[END_REF] 0: function SecMult(a, b) 1: for i = 0 to t do 2:

c i ← a i b i /*

B SNI Verification Algorithm

We now give a full description of our algorithm for the verification of SNI properties. Apart from notation changes, the algorithms are only slightly adapted from [START_REF] Barthe | Verified proofs of higher-order masking[END_REF]. In particular, the proof of correctness for Algorithm 11 can be easily generalized from that given in [START_REF] Barthe | Verified proofs of higher-order masking[END_REF].

In the following, we consider gadgets whose encoded inputs are all secret and denoted as a set of encodings {x ı } ı . Given a core gadget, the set of all possible positions in that gadget can be represented as a set E of K expressions over the x i k and some random variables in R (corresponding to the random samplings occurring in the gadget). All algorithms in this subsection consider gadgets represented in this form. Given such a set E, we denote with var(E) the set of all variables that appear in E, and with E int and E out the subsets that correspond to internal and output positions, respectively.

Following Barthe et al. [START_REF] Barthe | Verified proofs of higher-order masking[END_REF], our algorithm relies, at its core, on exhibiting an isomorphism between the distribution of each acceptable set of positions and some distribution that is syntactically non-interfering. In this case, we consider all sets of positions that are composed of t i internal positions and t o output positions (for any t i and t o such that t i + t o ≤ t) and find a bijection with some distribution that depends on at most t i shares of each of the gadget's inputs. Algorithm 9 takes an integer d and a set E of expressions over the x i k and random variables in R and finds, when successful, a sequence of substitutions #» h that construct a bijection between the distribution described by E and a distribution that syntactically depends on at most d shares of each one of the x i . The fact that Algorithm 9 produces a witness sequence of substitutions can be leveraged, as in [START_REF] Barthe | Verified proofs of higher-order masking[END_REF], to extend the position set E on which the corresponding bijection still proves the desired property. Algorithms 10a and 10b leverage this, and are only lightly adapted (for notation) from Barthe et al. [START_REF] Barthe | Verified proofs of higher-order masking[END_REF]. An important thing to note is that extend d {x ı }ı (X, E, #» h ) always returns a set X of expressions such that X ⊆ X ⊆ E and such that X depends (by #» h ) on at most d shares of each one of the x i . Finally, we adapt the second space-covering algorithm proposed by Barthe et al. [4] to the verification of the t-SNI property, by taking care to call NI d with the value of d that corresponds to the number of internal positions being considered. Algorithm 11 shows the adapted algorithm for the core verification task, and Algorithms 12a and 12b show the instances used to verify that a gadget is t-SNI and t-NI, respectively. Here again, Algorithm 11 is only lightly adapted from [START_REF] Barthe | Verified proofs of higher-order masking[END_REF] and their correctness proof, which establishes that whatever property is checked by NI d is true for all sets in j P dj (E j ), also applies to the new property being verified. It is then easy to prove that the calls to check d made by check t-SNI and check t-NI are sufficient to establish t-SNI and t-NI respectively (relying on Lemma 3 for t-NI).

Algorithm 10 Auxiliary algorithms for SNI verification We also note that Algorithm 11 can be used in other ways, not shown in Algorithm 12, that would enforce other, perhaps more complex, probing policies. We do not claim that all probing policies could be easily verified in this manner (and in fact, the affine policy could not), and leave as future work an investigation of efficient (or semi-efficient) algorithms-in this style-for the verification of arbitrary probing.

function recheck d {x ı }ı (E, #» h ) if #» h = [DEGREE(d)] then return ∀ı, |var(E) ∩ x ı | ≤ d if #» h = OPT(e, r) : #» h then (E ) ← choose({E | E = E [e/r]}) if E = ⊥ then return recheck d {x ı }ı (E , #» h ) else return false (

C Proofs

In this Appendix, we give proofs for lemmas, theorems, and propositions whose proof is not given in the paper, and detail some of the proof sketches.

Proof (sketch for Proposition 1). Leveraging the equivalence between simulation and non-interference (Lemma 2), we prove t-SNI by constructing a simulator that uses at most |O int | shares of the gadget's input to perfectly simulate the joint distribution of any position set O such that |O| ≤ t. The constructed simulator is very similar to those previously used in proofs of t-NI.

Let O be a set of positions such that |O| ≤ t, and let

d 1 = |O int | and d 2 = |O ext |. Note that d 1 + d 2 ≤ t.
Our goals are: i. to find an input set I such that I ≤ d 1 , ii. to construct a perfect simulator that uses only input shares a i ∈ I.

First, we identify which variables are internal (and therefore will be considered in O int ) and which are outputs (in O ext ). Internals are the a i , the r i,j (the value of r sampled at iteration i, j), and the c i,j (resp. c j,i ) which correspond to the value of the variable c i (resp. c j ) at iteration i, j of the second loop. Outputs are the final values of c i (i.e. c i,t ). Then, we define I as follows: for each position among a i , r i,j and c i,j (with j < t) we add share a i to I. It is clear that I contains at most d 1 positions, since each internal position adds at most one position to I. We now construct the simulator. For clarity, observe that the RefreshM algorithm can be represented using the following matrix, observing that c i,j is the partial sum of the first j + 2 elements of line i.

       a 0 0 r 0,1 r 0,2 • • • r 0,t a 1 r 0,1 0 r 1,2 • • • r 1,t a 2 r 0,2 r 1,2 0 • • • r 2,t . . . . . . . . . . . . . . . . . . a d r 0,t r 1,t r 2,t • • • 0        .
For each ı 0 such that a ı0 ∈ I (that is, for each line ı 0 of the matrix that contains at least one observed internal value), a ı0 is provided to the simulator (by definition of I). Thus, the simulator can sample all r ı0,j and compute all partial sums c ı0,j and the ı 0 th output normally. At this point, all values (all internals and all outputs) on lines indexed by an ı with a ı ∈ I follow the same distribution as they would in the real computation and are therefore perfectly simulated.

It remains to simulate output shares c  when a  / ∈ I. Remark that simulating the ı th line as above also necessarily fixes the value of all random variables appearing in the ı th column. After internal positions are simulated, at most d 1 lines of the matrix are fully filled. Therefore, each line  with a  / ∈ I contains at least t -d 1 ≥ d 2 holes corresponding to random values that have not yet been fixed. For each of the output position made on one such line , we can therefore pick a different r ,k that we choose so c  can be simulated by a freshly sampled uniform value.

Proof (sketch for Lemma 5). [START_REF] Coron | Higher-order side channel security and mask refreshing[END_REF] In this appendix, we give detailed proofs for Propositions 1 to 2.

Multiplication-Based Refreshing (Prop. 1) Following the proof sketch for Proposition 1, we give here a more detailed proof sketch, based on a sequence of games, that more closely follows the EasyCrypt formalization of the proof. This is only meant to illustrate the additional effort involved in obtaining formal proofs of such results, rather than convince the reader of the validity of the proof. The proof scripts can be obtained from the authors. The formal proof is done by constructing a simulator (R 3 ) and formally verifying its equivalence with an explicitly leaky version of the gadget (R 0 ).

We now construct the simulator. For clarity, observe that the SecMult algorithm can be equivalently represented using the following matrix. In this setting, c i,j corresponds to the partial sum of the j + 2 first elements of line i. For each variable r i,j (i < j) entering in the computation of an observation, we assign it a fresh random value. Then, for each observation in the first group, a i and b i are provided to the simulator (by definition of I and J) thus the observation is perfectly simulated. For an observation in the third group, we distinguish two cases. If i < j, r i,j is already assigned to a fresh random value. If i > j, either (i, j) ∈ I × J and the observation is perfectly simulated from r j,i , a i , b i , a j and b j or r j,i does not enter in the computation of any internal variable that was observed and r i,j (line 5 i,j ) was assigned a fresh random value. Each observation made in the fourth group is perfectly simulated using r i,j , a i and b j . As for an observation in the second group, the corresponding variable is a partial sum composed of a product a i ⊗ b i and of variables r i,j . Since a i and b i are provided to the simulator in this case, we focus on each remaining r i,j . Each one of them such that i < j is already assigned to a fresh random value. For the others, if r j,i enters in the computation of any other internal observation, then (i, j) ∈ I × J and r i,j is simulated with r j,i , a i , b i , a j and b j . Otherwise, r i,j is assigned a fresh random value. We still have to simulate output observations. We start with those for which an intermediate sum (group 2) is also observed. For each such variable c i , the biggest partial sum which is observed is already simulated. Thus, we consider the remaining terms r i,j . Each one of them such that i < j is already assigned to a fresh random value. For the others, either (i, j) ∈ I × J and c i is perfectly simulated from r j,i , a i , b i , a j and b j or r j,i does not enter in the computation of any internal variable observed and c i is assigned a fresh random value. We now consider output observations c i for which none of the partial sums are observed. Each of them contains t random variables of the form r i,j , at most one of which can enter in the computation of each one of the c j with i = j. Since we already considered at most t -1 observations not counting the current one, at least one of the r i,j we need to consider does not enter in the computation of any other observed variable and is unassigned. Thus, we can simulate c i using a fresh random value.

D Robust Composition

We consider the problem of securely composing algorithms or gadgets when the adversary may place t probes in each of them, capturing security in the region and stateful probing models [START_REF] Ishai | Private circuits: Securing hardware against probing attacks[END_REF]. In this informal discussion, we forbid wire duplications between regions (that is, each region's output can only be used once as input to another region). However, the same principles that allow us to compositional reason about security in the simple probing model would allow us to reason about robust composition with wire duplication, using, in particular, 2t-SNI mask refreshing gadgets where necessary.

As noted in Section 9, it is clear that any number of 2t-SNI gadgets or algorithms can be securely composed in this setting. We first observe that, for any two 2t-SNI algorithms F and G, and for any O This observation provides an elegant justification to Coron's result [START_REF] Coron | Higher order masking of look-up tables[END_REF], which states that iterating RefreshA 2t+1 2t + 1 times allows the secure stateful composition of his masked table-lookup algorithms without further doubling the number of shares. Indeed, it is also easy to see that Coron's mask refreshing algorithm is 2t-SNI.

However, the same composition could be obtained by slightly relaxing the security requirement on F and G. Indeed, we could instead use the following condition, which we call robust non-interference. The same argument that allows us to securely and robustly compose 2t-SNI gadgets allows us to securely and robustly compose t-RNI gadgets. Intuitively, t-RNI allows the adversary to place 2t probes on the gadget, as long as at most t of them are internal. This captures exactly the scenario where an adversary can place t probes inside a region, and can also learn, by probing subsequent regions, information about t shares of the output.

Constructing RNI Algorithms We now show how any t-NI algorithm can be turned into a t-RNI algorithm without doubling its internal number of shares, simply by processing its inputs and output. To do so, we consider the Double and Half gadgets (Gadget 13).14 c i ← a i r i 6: for i = 0 to 2 do 7:

for j = i + 1 to 2 do 8:

r $ ← K 9:
c i ← c i r 10:

t ← a i r j 11:

r ← r ⊕ t 12:

t ← a j r i 13:

r ← r ⊕ t 14:

c j ← c j ⊕ r 15: return c It is easy to see (and it can be checked automatically using, for example, Barthe et al.'s tool [START_REF] Barthe | Verified proofs of higher-order masking[END_REF]) that this small algorithm is private for t = 2. Intuitively, this is because, since privacy requires simulation only when the input encodings are known to be uniform, and even though the inputs to SecMult are not independent, one of them is essentially a one-time-pad of the other.

However, simulating, say, lines 10 0,1 (with value a 0 (a 1 ⊕ b 1 )) and 10 1,2 (with value a 1 (a 2 ⊕ b 2 )) using only two shares of each of a and b is not possible.

We note that, as pointed out above, the tool by Barthe et al. [START_REF] Barthe | Verified proofs of higher-order masking[END_REF] directly verify privacy, rather than going through t-NI and losing precision. However, they do not scale. When considering verification tools (or indeed even the verifiability of pen-and-paper proofs), there is therefore a tradeoff between precision and applicability.

  of B with non-zero weight under µ is discrete and moreover b∈supp(µ) µ(b) = 1. We let D(B) denote the set of discrete distributions over B. Equality of distributions is defined as pointwise equality of functions. Distributions can be given a monadic structure with the two operators munit(•) and mlet • = •. For every b ∈ B, munit(b) is the unique distribution µ such that µ(b) = 1. Moreover, given µ : D(B) and

Alg. 3

 3 An abstract algorithm function Alg 2 (a) b := R(a); c := G(a, b); return c

  positions (these correspond to shares of encodings used in the gadget or algorithm), the set O = I ∪ V of positions (composed of input positions and scalara variables) and the set O + = I ∪ (N × V) of extended positions (where scalar variables are tagged with a label in N to differentiate between uses of a variable in different gadgets). The input positions of a gadget G and of an algorithm P are denoted by I G and I P respectively and contain exactly those elements of I that correspond to encoding variables that occur in G or P . Likewise, the set of positions of a gadget G and of an algorithm P are denoted by O G ⊆ O and O P ⊆ O + respectively and consist of all positions that occur in a gadget G, and all extended positions that occur in an algorithm P . To capture the joint distribution of a set of positions O in a gadget G or an algorithm P (with O ⊆ O G , resp. O ⊆ O P ), we take the marginal of the gadget or algorithm's semantics with respect to O. These are denoted by G O : Mem → D(O → K) and P O : Mem → D(O → K) respectively. 11 e (m, lm) : K with m ∈ Mem and lm ∈ LMem

Definition 1

 1 Let G be a gadget, and let I ⊆ I G . Two memories m, m ∈ Mem are I-equivalent, written m ∼ I m , whenever m(a) ı = m (a) ı for every a ı ∈ I.

  The reverse implication proceeds by induction on k = t -|O|. The case k = 0 is immediate by definition of t-NI. For the inductive case, let O be such that t -|O| = k + 1. Let a be an encoding variable such that |depset(O) |a | = depset(O) . Since depset(O) ≤ |O| ≤ t, there necessarily exists an input position a ı such that a ı / ∈ depset(O). Let O = O ∪ {a ı }. We have depset G (O ) ≤ |O | = 1 + |O| by induction hypothesis and depset G (O ) = 1 + depset G (O) by construction, therefore we can conclude.

Proposition 2

 2 Alg. 6] (Gadget 7) and the MultLin gadget for securely multiplying linearly dependent inputs [15, Alg. 5] (Gadget 8) are both strongly noninterfering. The proof of SNI for Gadget 7 is easy to adapt to the more standard quadraticspace multiplication gadget, since they compute the same intermediate values in different orders. The SecMult gadget (Gadget 7) is t-SNI. Proposition 3 The MultLin gadget (Gadget 8) is t-SNI.

b

  := G(a1, . . . , an) : (Γ in , φ in ) ⇐= (Γ, φ) c : (Γ, φ) ⇐= (Γout, φout) b := G(a1, . . . , an); c : (Γ in , φ in ) ⇐= (Γout, φout) (SEQ)

  our type system. Let O = O int O ext be a position set, split between internal and output positions. The affine property ensures that the joint distribution of O depends only on input positions in η(O int ∪ O ext ), and furthermore that |η(O int ∪ O ext )| = |η(O int )| + |η(O ext )| = |η(O int )| + |O ext |. Rule (AFFINE) interprets this affine property into our type system, using Γ out (b) and a fresh O for O ext and O int , respectively, and encoding η(O ) into an abstract existential set X . The condition |X | ≤ |O | precisely captures the fact that |η(O)| ≤ |O| for all O.

Algorithm 9

 9 Given O, d, find I such that I ≤ d for (I, O)-NI 1: function NI d {x ı }ı (E) 2: if ∀ı, |var(E) ∩ x ı | ≤ d then 3: return DEGREE(d) 4: (E , e, r) ← choose({(E , e, r) | e is invertible in r ∧ r ∈ R ∧ E = E [e/r]}) 5: if (E , e, r) = ⊥ then 6: return OPT(e, r) : NI d {x ı }ı (E ) 7: return ⊥

  b 0 0 r 0,1 r 0,2 • • • r 0,t a 1 ⊗ b 1 r 1,0 0 r 1,2 • • • r 1,t a 2 ⊗ b 2 r 2,0 r 2,1 0 • • • r 2,t a t ⊗ b t r t,0 r t,1 r t,2 • • • 0

F

  andO G such that |O F |, |O G | ≤ t, we have depset F ;G (O F ∪ O F ) ≤ t.This allows us to conclude about the security of the composition of any number of gadgets by induction on that number.

Definition 9 (

 9 Robust Non-Interference) A gadget G is t-robustly non-interfering (or t-RNI) whenever, for any O G such that |O G | ≤ 2t and |O int G | ≤ t, we have depset G (O G ) ≤ |O int G |.

Gadget 13 The

 13 Double and Half gadgets function Doublet(a : K t+1 ) for i = 0 to t do r2i $ ← K r2i+1 ← a i r2i return r0, . . . , r2t+1 (13a) Doubling the number of shares function Halft(a : K 2t+2 ) for i = 0 to t do ri $ ← a 2i ⊕ a 2i+1 return r0, . . . , rt (13b) Halving the number of shares We first note that Double t is t-NI, and that Half t is such that, for any O H such that |O H | ≤ t, we have depset H(O H ) ≤ 2t. (Indeed, each internal position depends two shares of the input.) Gadget 15 A small separating example 1: function separator(a, b : K 3 ) 2: for i = 0 to 2 do 3: r i := a i ⊕ b i 4: for i = 0 to 2 do 5:

  Proposition 5 (Soundness of the Type System) If s : (Γ in , φ in ) ⇐= (Γ out , φ out ) then also |= P : (Γ in , φ in ) ⇐= (Γ out , φ out ) If NI P then P is t-NI If SNI P then P is t-SNI An Example: Rivain and Prouff's inversion algorithm We now illustrate the type system by describing a typing derivation on Rivain and Prouff's algorithm for computing inversion in GF(2 8 ) [31,15]. An algorithm implementing this operation securely is shown in Figure

Table 1 :

 1 Alg. 6]; MultLin, Coron et al.'s algorithm for the computation of functionalities of the form x g(x) for some linear g [15, Alg. 5]; Add, the standard affine gadget for the addition Time 2-SNI Time 3-SNI Time 4-SNI Time 5-SNI Time 6-SNI Time Experimental Results for the SNI Verifier of two encodings; RefreshA, the weakly secure mask refreshing algorithm from Rivain and Prouff[START_REF] Rivain | Provably secure higher-order masking of AES[END_REF]; RefreshIter k , the iterated additive refresh proposed byCoron [12, Alg. 4] for supporting more efficient composition in his full model (we make explicit the number of iterations k); WeakMult, the generic reduced-randomness multiplication algorithm proposed by Belaïd et al.[START_REF] Belaïd | Randomness complexity of private circuits for multiplication[END_REF]. Table1sums up our findings and some verification statistics.

	Order 1 1-SNI SecMult Gadget 0.07s	Order 2 0.08s	Order 3 0.09s	Order 4 0.86s	Order 5 36.40s	Order 6 37min
	MultLin		0.07s	0.08s	0.15s		1.19s		54.13s		48min
	RefreshA		0.07s	0.08s	0.08s	-	-	-	-	-	-
	RefreshIter 2		0.08s	0.08s	0.08s		0.08s		0.13s		.20s
	RefreshIter 3	-	-	0.09s	0.08s		0.09s		0.14s		.54s
	WeakMult		0.07s	0.07s	0.09s	-	-	-	-	-	-

Table 2 :

 2 Resource usage during masking and verification

Table 3 :

 3 Time taken by 10,000 executions of each program at various masking orders

  Yj ← choose(P d j (Ej))Algorithm 12 Algorithms for t-SNI and t-NI verification

		function extend d {x ı }ı (X, E,	#» h )
		e ← choose(E)
		if e = ⊥ then if recheck d {x ı }ı (e, return extend d {x ı }ı ((X, e), E \ {e}, #» h ) then else return extend d {x ı }ı (X, E \ {e}, #» #» h ) h )
		else return X
			(10b) Extending the Position Set
		10a) Rechecking a derivation
	4: 5: 6:	#» h ← NI d {x ı }ı ( j Yj) if #» h = ⊥ then raise CannotProve ( j Yj) Yj ← extend {x ı }ı (Yj, Ej \ Yj, #» h )
	7:	check d {x ı }ı ({(dj, Ej \ Yj)}j)
	8:	for j; 0 < ij < dj do
	9: {x 1: function check t-SNI check d {x ı }ı (E)	1: function check t-NI {x ı }ı (E)
	2: for i; 0 ≤ i ≤ t do 3: check i {x ı }ı ({(i, E int ), (t -i, Eout)})	2: check t {x ı }ı ({(t, E)}) 3: return true
	4: return true	(12b) t-NI Verification
		(12a) t-SNI Verification

Algorithm 11 Core Algorithm for (I, O)-NI Verification 1: function check d {x ı }ı ({(dj, Ej)}j) 2: if ∀j, dj ≤ |Ej| then 3: ı }ı ({(ij, Yj), (dj -ij, Ej \ Yj)}) 10: return true

  exhibit proofs for both statements. We now sketch a proof of t-NI for Cube that does not exhaustively consider all (t + 1)-tuples of positions in Cube, emphasizing the critical use of strong non-interference for the refreshing gadget. Recall that our goal is to upper-bound depset Cube (O) for all O ⊆ O Cube such that |O| ≤ t. Given such a set, we first partition it as O = O M O R O S following gadget boundaries (recall that positions in algorithms include the label of the gadget invocation they occur in). First, we consider the dependency set I M = depset Mult (O M ) of O M by Mult. We know |O M | ≤ |O| ≤ t, and by t-NI of Mult, we deduce that I M ≤ |O M |. Considering now the invocation of RefreshM, we must establish cardinality properties of the dependency set I R = depset RefreshM (O R ∪ I M|y 2 ) of those direct internal positions observed by the adversary in RefreshM, jointly with those output positions she may have learned information about through positions probed in later parts of the circuit (here, in Mult). From previous inequalities, we know that |I M|y 2 | ≤ I M ≤ |O M |, and thus we have |O R ∪ I M|y 2 | ≤ t. By t-SNI of RefreshM, we thus have I R ≤ |O R | (since positions in I M|y 2 are external to RefreshM). Finally, we consider the dependency set I S = depset Square (O S ∪ I R|y 1 ) of direct internal positions observed by the adversary in Square, jointly with those output positions she may have learned information about through positions probed in later parts of the circuit (here in RefreshM and Mult, propagated through the single use of y 1 in the invocation of RefreshM). Since we have |O S ∪ I R|y 1 | ≤ |O

S | + I R ≤ |O S | + |O R | ≤ t, and since Square is t-NI, we conclude that I S ≤ |O S | + |O R |. Overall, we have depset Cube (O) ⊆ I S|x ∪ I M|x , and we can conclude (using some of the intermediate inequalities from above), that depset Cube (O) ≤ |O S | + |O R | + |O M | ≤ t. C.1 Game-Based Proofs for SNI Gadgets

A t-encoding of an element v ∈ K is a (t + 1)-tuple v = v 0 , . . . , v t such that v = v 0 ⊕ . . . ⊕ v t = v.Each of the v ı ∈ K in an encoding v of v is called a share. Moreover, t is called the masking order. A probabilistic encoding of v is a distribution over encodings of v.

The cryptography literature often refers to such transformations as masking compilers. We purposely avoid this terminology, since the terms is used in programming languages for transformations that output executable code

However, the verification tool supports richer settings to which the theory extends smoothly and our examples are written in a more general language, closer to our implementation, that supports static for loops, direct assignments to shares (a ı ← e), arbitrary expressions on the right-hand side of assignments, and a broader return syntax. For example, Gadget 4 shows generic descriptions of the mask refreshing algorithms from Section 2.

In order to justify that the marginals have the required type, observe that one can refine the type of G given in Figure2to Mem → D(Val × (OG → K)). Similarly, one can refine the type of P to Mem → D(Val × (OP → K)) .

Enforcing probing policiesWe first define an expressive assertion language for specifying sets of position sets, and then introduce probing policies, which yield a convenient formalism for defining a large class of information flow policies with cardinality constraints.

Note that the number of mask refreshing operations executed during an execution of the algorithm may be much greater, since the sub-procedure in which the insertion occurs may be called multiple times.

This excludes the once-and-forall cost of proving the security of core gadgets.

These are only gadgets for a slightly extended notion of gadget that allows the encoding size to change between inputs and outputs.

More accurately, they define privacy for a circuit transformer that includes definitions for I and O. This is not relevant here.

Acknowledgements The work presented here was supported by projects S2013/ICE-2731 N-GREENS Software-CM, ANR-10-SEGI-015 PRINCE and ANR-14-CE28-0015 BRUTUS, and ONR Grants N000141210914 and N000141512750, as well as FP7 Marie Curie Actions-COFUND 291803.

The majority of the work presented here was performed while the author was working for the

Refining SNI We now discuss some limitations of our current implementation, and leads for future theoretical work that may yield significant practical improvements. The first point we wish to discuss is the case of Keccak, for which algorithm transformation is prohibitively expensive. This issue is due to our handling of static for loops: indeed, our tool unrolls them to perform type-checking and rolls them back up afterwards if possible (otherwise leaving them unrolled in the final algorithm). For smaller algorithms, this is not a problem, but unrolling all 24 rounds of Keccak-f, along with all the loops internal to each iteration, yields a very large program that is then backtracked over each time a mask refreshing operation is inserted. Refining our non-interference notions to multi-output gadgets and algorithms would allow us to significantly improve our tool's handling of loops and high-level composition, whilst gaining a better understanding of probing security in such scenarios. This improved understanding may in turn help inform the design of primitives that are easier to protect against higher-order probing.

Second, we discuss our greedy policy for the insertion of mask refreshing algorithms. In our experiments, we consider a version of the linear-time modular addition algorithm [START_REF] Coron | Secure conversion between boolean and arithmetic masking of any order[END_REF] whose second argument is a public (non-shared) value (for example, a round counter, as in Speck). We show its code, as produced by our masking transformer, in Gadget 6a, and display a hand-masked variant in Gadget 6b, slightly abusing notations by denoting simple gadgets with the symbol typically used for their unprotected versions. Notice that the variable w is used once per loop iteration, and that our tool refreshes each of them, while it is sufficient to mask only the first one. Improving our gadget selection algorithm to detect and implement this optimization-and others-would be an interesting avenue for future work, that could help improve our understanding of the effect on security of compiler optimizations.

function RefreshM(a) : for i = 0 to t do c i ← a i ; for i = 0 to t do for j = i + 1 to t do r i,j ← $; c i ← c i ⊕ r i,j ; c j ← c j r i,j ; return c Game 0. For clarity, we start, in Game 0, from the original refreshing gadget RefreshM, which computes the t + 1 shares c i of the gadget's output without leaking any intermediate observations. We recall its definition on the right. function R 0 (a, O) :

In Game 1, we make the leakage explicit by taking as additional input from the adversary a set of observations, whose values are written, during execution, into a table visible to the adversary. We refer to this function as R 0 (shown left). As explained in the proof sketch above, we distinguish three different kinds of internal observations a i , r i,j , c i,j and have the final definitions of c i as output observations. Considering this first game, we define the set I O as a function of O int , as:

Game 2. We modify R 0 in order to i. pre-sample all fresh randomness using a random function Sample, ii. start by computing internal observations, and output shares c i such that i ∈ I O , iii. then compute output shares such that i / ∈ I O . We refer to this new function as R 1 and we use EasyCrypt to prove that R 0 and R 1 produce equivalent distributions on the requested observations if their position sets are the same set O such that |O| ≤ t and their input encodings agree for each a i where i ∈ I O .

function R 1 (a, O) : for i = 0 to t do for j = i + 1 to t do r i,j ← Sample(i, j);

Game 3. We now delay the generation of random values as much as possible, sampling just before their first use. We refer to this new function as R 2 . We prove the equivalence between Games 2 and 3 if the share the same O such that |O| ≤ t and if they agree on input shares a i such that i ∈ I. This equivalence leverages a generic argument equating lazy and eager sampling when independent from intermediate adversary views.

function R 2 (a, O) :

In this final game, we fully simulate the computation of the c i when i / ∈ I O by showing that there exists a non-empty set of indices L O such that ∀ ∈ L, r i, is not assigned yet. Then, instead of computing the c i (for i / ∈ I) as in Game 2:

we simulate it by setting the value of r i,k as follows:

We prove the equivalence between Game 3 and Game 4 with EasyCrypt when functions R 2 and R 3 share the same O such that |O| ≤ t and agree on input shares a i with i ∈ I.

The most critical part of this step is undoubtedly to ensure that the subscript L contains at least one index. To do so, we need to show that the elements r i, with ∈ L were not already used and won't be reused anywhere. Finally, we also formally prove that the results of R 3 , which represents the final simulator, only depends on those input shares a i such that i ∈ I O for all O such that |O| ≤ t.

function SumCij(i, j) :

Finally, we have formally proved that an adversary could not distinguish between two programs which share the same inputs {a i } i∈I with at most t observations and that the cardinal of I was upper bounded by the number of internal observations d 1 .

Secure Multiplication (Prop. 2) We now give an informal proof sketch that Gadget 7 is t-SNI for all t. The proof is formalized in EasyCrypt following the model described above for Proposition 1.

Proof (sketch for Proposition 2). Let O be a set of observations such that |O| ≤ t, and let

To prove t-SNI, we aim to find an input set I such that I ≤ d 1 , and to construct a perfect simulator that uses only input shares from I to compute the same distribution over the observations O as the real gadget.

First, we identify which variables are internals and which are outputs. We directly split the internals in four groups for the needs of the proof:

1. the a i , the b i , and the a i ⊗ b i , 2. the c i,j (resp. c j,i ) which correspond to the value of the variable c i (resp. c j ) at iteration i, j, 3. the r i,j (the value of r on line 5 i,j ), and the r j,i (the value of r on line 8 i,j ), 4. the a i ⊗ b j and the a i ⊗ b j r i,j .

The output variables are the final values of c i (that is c i,t ).

We construct I. As the algorithm takes two inputs a and b, we define two sets of indices I, J {0, . . . , t} such that

It is then sufficient to show that they are such that |I|, |J| ≤ |O int |, and that the gadget is (I, O)-NI. For each observation in the first or the second group, we add the index i to both I and J. For each observation in the third or in the fourth group: if the index i is already in I, we add the index j to I, otherwise we add the index i to I and similarly for J. It is clear that the final sets I and J contain each one at most d 1 indices, since each internal observation adds at most one index to each of them.

E Privacy vs probing security

In this appendix, we exhibit a simple example that separates Ishai, Sahai and Wagner's notion of privacy [START_REF] Ishai | Private circuits: Securing hardware against probing attacks[END_REF] and the widely used simulation-based notion of t-probing security.

We recall that Ishai, Sahai and Wagner [START_REF] Ishai | Private circuits: Securing hardware against probing attacks[END_REF] define privacy for a masked circuit C as the fact that any t wires in C during an execution of O • C • I (where I and O are the encoding and decoding circuits that sample uniform encodings of the secret inputs and recombine outputs from their encodings, away from adversary interference) can be simulated without access to any wire in the circuit. 15 On the other hand, as discussed earlier in the paper, t-probing security, as defined for example by Carlet et al. [START_REF] Carlet | Algebraic decomposition for probing security[END_REF] states that a gadget or algorithm G is t-probing secure iff any t of its intermediate wires can be simulated using at most t shares of each of its inputs. Note in particular that, unlike privacy, t-probing security makes no mention of secrets, or of uniform input encodings. In Gadget 15, we exhibit a small example gadget, which computes a (a ⊕ b for t = 2, and shows that this is indeed an important detail by separating the two notions. However, we note that even Ishai, Sahai and Wagner [START_REF] Ishai | Private circuits: Securing hardware against probing attacks[END_REF] prove that their transformers are private using a t-probing style simulation argument, so the separation we exhibit here makes little difference in practice.