Compositional Synthesis of Leakage Resilient
Programs
Arthur Blot1 , Masaki Yamamoto2,⋆ , and Tachio Terauchi3
1

ENS Lyon, Lyon, France
arthur.blot@ens-lyon.fr
2
Nagoya University, Nagoya, Japan
yamamoto-m@sqlab.jp
3
JAIST, Nomi, Japanterauchi@jaist.ac.jp

Abstract. A promising approach to defend against side channel attacks
is to build programs that are leakage resilient, in a formal sense. One
such formal notion of leakage resilience is the n-threshold-probing model
proposed in the seminal work by Ishai et al. [15]. In a recent work [8],Eldib and Wang have proposed a method for automatically synthesizing
programs that are leakage resilient according to this model, for the casen = 1. In this paper, we show that the n-threshold-probing model ofleakage resilience enjoys a certain compositionality property that can be
exploited for synthesis. We use the property to design a synthesis methodthat efficiently synthesizes leakage-resilient programs in a compositionalmanner, for the general case of n > 1. We have implemented a prototype of the synthesis algorithm, and we demonstrate its effectivenessby synthesizing leakage-resilient versions of benchmarks taken from theliterature.

1

Introduction

Side channel attacks are well recognized as serious threat to the security of computer systems. Building a system that is resilient to side channel attacks is a challenge, particularly because there are many kinds of side channels (such as, power,
timing, and electromagnetic radiation) and attacks on them. In an effort to establish a principled solution to the problem, researchers have proposed formal
definitions of resilience against side channel attacks, called leakage resilience [15,14, 10–12, 2]. The benefit of such formal models of side-channel-attack resilienceis that a program proved secure according to a model is guaranteed to be secureagainst all attacks that are permitted within the model.
The previous research has proposed various notions of leakage resilience. In
this paper, we focus on the n-threshold-probing model proposed in the seminal
work by Ishai et al. [15]. Informally, the model says that, given a program represented as a Boolean circuit, the adversary learns nothing about the secret by⋆

Author’s current affiliation: TIS Inc.

executing the program and observing the values of at most n nodes in the circuit(cf. Section 2 for the formal definition). The attractive features of the model
include its relative simplicity, and the relation to masking, a popular countermeasure technique used in security practice. More precisely, the security under then-threshold-probing model is equivalent to the security under nth -order masking [21], and often, the literature uses the terminologies interchangeably [2, 5, 9,
8, 4, 3]. Further, as recently shown by Duc et al. [7], the security under the model
also implies the security under the noisy leakage model [20] in which the adversary obtains information from every node with a probabilistically distributed
noise.
In a recent work, Eldib and Wang [8] have proposed a synthesis method that,given a program represented as a circuit, returns a functionally equivalent circuitthat is leakage resilient according to the n-threshold-probing model, for the casen = 1 (i.e., the adversary observes only one node). The method is a constraintbased algorithm whereby the constraints expressing the necessary conditions are
solved in a CEGAR (counterexample-guided abstraction refinement) style. In
this work, we extend the synthesis to the general case where n can be greater than
1. Unfortunately, naively extending (the monolithic version of) their algorithm
to the case n > 1 results in a method whose complexity is double exponential
in n, leading to an immediate roadblock.4 As we show empirically in Section 5,
the cost is highly substantial, and the naive monolithic approach fails even forthe case n = 2 on reasonably simple examples.
Our solution to the problem is to exploit a certain compositionality property admitted by the leakage resilience model. We state and prove the property formally in Theorems 2 and 3. Roughly, the compositionality theorems saythat composing n-leakage-resilient circuits results in an n-leakage-resilient circuit, under the condition that the randoms in the components are disjoint. The
composition property is quite general and is particularly convenient for synthesis. It allows a compositional synthesis method which divides the given circuit
into smaller sub-circuits, synthesizes n-leakage-resilient versions of them, andcombines the results to obtain an n-leakage-resilient version of the whole. The
correctness is ensured by using disjoint randoms in the synthesized sub-circuits.
Our approach is an interesting contrast to the approach that aims to achieve
compositionality without requiring the disjointness of the component’s randoms,
but instead at the cost of additional randoms at the site of the composition [5,3].
We remark that the compositionality is not at all obvious and quite unexpected. Indeed, at first glance, n-leakage resilience for each individual component seems to say nothing about the security of the composed circuit against
an adversary who can observe the nodes of multiple different components in thecomposition. To further substantiate the non-triviality, we remark that the compositionality property is quite sensitive, and for example, it fails to hold if the
4

Their paper [8] also shows a compositional algorithm. However, compositionality
becomes non-trivial when n > 1 because then the adversary can observe nodes fromthe different components of the composition.

bounds are relaxed even slightly so that the adversary makes at most n observations within each individual component but the total number of observations
is allowed to be just one more than n (cf. Example 2).
To synthesize n-leakage-resilient sub-circuits, we extend the monolithic algorithm from [8] to the case where n can be greater than 1. We make several
improvements to the baseline algorithm so that it scales better for the case n > 1(cf. Section 4.1). We have implemented a prototype of our compositional synthesis algorithm, and experimented with the implementation on benchmarks takenfrom the literature. We summarize our contributions below.
– A proof that the n-threshold-probing model of leakage resilience is preserved
under certain circuit compositions (Section 3).
– A compositional synthesis algorithm for the leakage-resilience model thatutilizes the compositionality property (Section 4).
– Experiments with a prototype implementation of the synthesis algorithm(Section 5).
The rest of the paper is organized as follows. Section 2 introduces preliminary
definitions and notations, including the formal definition of the n-thresholdprobing model of leakage resilience. Section 3 states and proves the compositionality property. Section 4 describes the compositional synthesis algorithm.
We report on the experience with a prototype implementation of the algorithm
in Section 5, and discuss related work in Section 6. We conclude the paper in
Section 7. Appendix contains the omitted proofs.

2

Preliminaries

We use boldface font for finite sequences. For example, b = b1 , b2 , . . . , bn . We
adopt the standard convention of the literature [9, 8, 4, 3] and assume that a
program is represented as an acyclic Boolean circuit.5 We assume the usual
Boolean operators, such as XOR gates ⊕, AND gates ∧, OR gates ∨, and NOTgates ¬.
A program has three kinds of inputs, secret inputs (often called keys) ranged
over by k, public inputs ranged over by p, and random inputs ranged over by r.
Informally, secret inputs contain the secret bits to be protected from the adversary, public inputs are those that are visible and possibly given by the adversary,and random inputs contain bits that are generated uniformly at random (hence,
it may be more intuitive to view randoms as not actual “inputs”).
Consider a program P with secret inputs k1 , . . . , kx . In the n-thresholdprobing model of leakage resilience, we prepare n+1-split shares of each ki (fori ∈ {1, . . . , x}):nMri,j )
ri,1 , . . . , ri,n , ki ⊕ (j=1
5In the implementation described in Section 5, following the previous works [9, 8], weconvert the given C program into such a form.

where each ri,j is fresh. Note that the split shares sum to ki , and (assuming thatri,j ’s are uniformly independently distributed) observing up to n many shares
reveals no information about ki . Adopting the standard terminology of the literature [15], we call the circuit that outputs such split shares the input encoderof P . The leakage resilience model also requires an output decoder, which sums
the split shares at the output. More precisely, suppose P has y many n+1-split
outputs o1 , . . . , oy (i.e., |oi | = n + 1 for each i ∈ {1, . . . , y}). Then, the outLn+1
put decoder for P is, for each oi = oi,1 , . . . , oi,n+1 , the circuit
j=1 oi,j . For
example, Fig. 1 shows a 2+1-split circuit with the secret inputs k1 , k2 , public inputs p1 , p2 , random inputs r1 , r2 , r3 , r4 , and two outputs. Note that the
input encoder (the region Input Encoder) introduces the randoms, and theoutput decoder (the region Output Decoder) sums the output split shares.
We associate a uniquelabel (ranged over by α)
to every gate of the circuit. We call the nodes of
P , nodes(P ), to be theset of labels in P excluding the gates internal to the input encoder
and the output decoder
part of P (but including
the outputs of the input
encoder and the inputs
to the output decoder).
Intuitively, nodes(P ) are
the nodes that can be observed by the adversary.
For example, in Fig. 1,
the observable nodes are
the ones in the region
Observable Nodes labeled α1 , . . . , α15 .

KƵƚƉƵƚ
ĞĐŽĚĞƌ

ŽϭْŽϮْŽϯŽϭDϭKďƐĞƌǀĂďůĞ
EŽĚĞƐ
Dϳ

Dϴ

ْ
Dϵ

ƌϭ

ŽϮ

ْ

DϭϬ

DϮ

Dϭϭ

D

DϭϮ

ƌϮ ŬϭْƌϭْƌϮ
Ŭϭ

Žϰ

ْ ϯْ

/ŶƉƵƚŶĐŽĚĞƌƉϭŽϯŽϰْŽϱْŽϲ

Dϰ

Dϭϯ

ƌϯ

Žϱ

‫ר‬

Dϱ

Žϲ

‫ר‬

Dϭϰ

Dϲ

‫ר‬

Dϭϱ

ƌϰ ŬϮْƌϯْƌϰŬϮƉϮFig. 1. Example of a 2-leakage-resilient circuit

Let ν be a mapping from the inputs of P to {0, 1}. Let α = α1 , . . . , αn be avector of nodes in nodes(P ). We define the evaluation, νP (α), to be the vector
b1 , . . . , bn ∈ {0, 1}n , such that each bi is the valuation of the node αi whenevaluating P under ν. For example, let P ′ be the circuit from Fig. 1. Let ν map
p1 , r1 , k2 to 0, and the others to 1. Then, νP ′ (α11 , α1 ) = 0, 1.
Let us write ν[v 7→ b] for the store ν except that each vi is mapped to bi(for i ∈ {1, . . . m}) where v = v1 , . . . , vm and b = b1 , . . . , bm . Let P be a circuitwith secret inputs k, public inputs p, and random inputs r. For bp ∈ {0, 1}|p| ,bk ∈ {0, 1}|k| , α ∈ nodes(P )∗ , and bα ∈ {0, 1}|α| , let #P (bp , bk , α, bα ) =|{b ∈ {0, 1}|r| | ν[r 7→ b]P (α) = bα }| where ν = {p 7→ bp , k 7→ bk }. We defineµP (bp , bk , α) to be the finite map from each bα ∈ {0, 1}|α| to #P (bp , bk , α, bα ).

We remark that µP (bp , bk , α), when normalized by the scaling factor 2−|r| , isthe joint distribution of the values of the nodes α under the public inputs bp
and the secret inputs bk .
Roughly, the n-threshold-probing model of leakage resilience says that, forany selection of n nodes, the joint distribution of the nodes’ values is independentof the secret. Formally, the leakage-resilience model is defined as follows.
Definition 1 (Leakage Resilience). Let P be an n+1-split circuit with secret
inputs k, public inputs p, and random inputs r. Then, P is said to be leakageresilient under the n-threshold-probing model (or, simply n-leakage-resilient) if
for any bp ∈ {0, 1}|p| , bk ∈ {0, 1}|k| , bk ′ ∈ {0, 1}|k| , and α ∈ nodes(P )n ,µP (bp , bk , α) = µP (bp , bk ′ , α).
We remark that, above, r includes all randoms introduced by the input encoder
as well as any additional ones that are not from the input encoder, if any. For
instance, in the case of the circuit from Fig. 1, the randoms are r1 , r2 , r3 , r4 andthey are all from the input encoder.
Informally, the n-threshold-probing model ofleakage resilience says that the attacker learnsْ‫ר‬
nothing about the secret by executing the circuitand observing the values of up to n many internalْgates and wires, excluding those that are internal
to the input encoder and the output decoder.
We say that a circuit is random-free if it has
Ɖϭ
Ŭϭ
ŬϮ
ƉϮ
no randoms. Let P be a random-free circuit with′public inputs p and secret inputs k, and P bea circuit with public inputs p, secret inputs k, Fig. 2. A circuit computing
and randoms r. We say that P ′ is IO-equivalent (p1 ⊕ k1 ⊕ k2 , k2 ∧ p2 )to P if for any bk ∈ {0, 1}|k| , bp ∈ {0, 1}|p| , andbr ∈ {0, 1}|r| , the output of P when evaluated under ν = {p 7→ bp , k 7→ bk }is equivalent to that of P ′ when evaluated under ν[r 7→ br ]. We formalize thesynthesis problem.
Definition 2 (Synthesis Problem). Given n > 0 and a random-free circuit
P as input, the synthesis problem is the problem of building a circuit P ′ suchthat 1.) P ′ is IO-equivalent to P , and 2.) P ′ is n-leakage-resilient.
An important result by Ishai et al. [15] is that any random-free circuit canbe converted to an IO-equivalent leakage-resilient form.
Theorem 1 ([15]). For any random-free circuit P , there exists an n-leakageresilient circuit that is IO-equivalent to P .
While the result is of theoretical importance, the construction is more of a proofof-concept in which every gate is transformed uniformly, and the obtained circuits can be quite unoptimized (e.g., injecting excess randoms to mask computations that do not depend on secrets). The subsequent research has proposed
to construct more optimized leakage-resilient circuits manually [21, 5], or by automatic synthesis [8]. The latter is the direction of the present paper.

Example 1. Consider the random-free circuit P shown in Fig. 2 which outputs(p1 ⊕ k1 ⊕ k2 , k2 ∧ p2 ). Let P ′ be the circuit from Fig. 1. It is easy to see thatP ′ is IO-equivalent to P . Also, it can be shown that P ′ is 2-leakage resilient.
Therefore, P ′ is a 2-leakage-resilient version of P .
Remark 1. The use of the input encoder and the output decoder is unavoidable.
It is easy to see that the input encoder is needed. Indeed, without it, one cannot
even defend against an one-node-observing attacker as she may directly observe
the secret. To see that the output decoder is also required, consider an oneoutput circuit without the output decoder and let n be the fan-in of the lastgate before the output. Then, assuming that the output depends on the secret,the circuit cannot defend itself against an n-nodes-observing attacker as she may
observe the inputs to the last gate.
Remark 2. In contrast to the previous works [5, 3] that implicitly assume thateach secret is encoded (i.e., split in n+1 shares) by only one input encoder,
we allow a secret to be encoded by multiple input encoders. The relaxation
is important in our setting because, as remarked before, the compositionality
results require disjointness of the randoms in the composed components.
Split and Non-Split Inputs / Outputs. We introduce terminologies thatare convenient when describing the compositionality results in Section 3. We use
the term split inputs to refer to the n+1 tuples of wires to which the n+1-split(secret) inputs produced by the input encoder (i.e., the pair of triples r1 , r2 , k1 ⊕r1 ⊕r2 and r3 , r4 , k2 ⊕r3 ⊕r4 in the example of Fig. 1) are passed, and use the term
non-split inputs to refer to the wires to which the original inputs before the split(i.e., k1 and k2 in Fig. 1) are passed. We define split outputs and non-split outputs
analogously. Roughly, the split inputs and outputs are the inputs and outputs of
the attacker-observable part of the circuit (i.e., the region Observable Nodesin Fig. 1), whereas the non-split inputs and outputs are those of the whole circuitwith the input encoder and the output decoder.

3

Compositionality of Leakage Resilience

This section shows the compositionality
property of the n-threshold-probing modelof leakage resilience. We state and prove
two main results (for space the proofs aredeferred to Appendix).
The first result concerns parallel compositions. It shows that given two n-leakageresilient circuits P1 and P2 that possibly
share inputs, the composed circuit thatruns P1 and P2 in parallel is also n-leakage
resilient, assuming that the randoms in thetwo components are disjoint. Fig. 3 shows

Wϭ

WϮ

ǀϮ

ǀϭ

Wϭ

ǀϭ

ǀϯ

ǀϮ

WϮ

ǀϮ

ǀϯ

Fig. 3. Parallel composition of P1
and P2 .

the diagram depicting the composition. The second result concerns sequential
compositions, and it is significantly harder to prove than the first one. The
sequential composition takes an n-leakage-resilient circuit P2 having y many
(non-split) inputs, and n-leakage-resilient circuits P11 , . . . , P1y each having one(non-split) output. The composition is done by connecting each split output of
the output-decoder-free part of P1i to the ith split input of the input-encoderfree part of P2 . Clearly, the composed circuit is IO-equivalent to the one formedby connecting each non-split output of P1i to the ith non-split input of P2 .
The sequential compositionality result states that the composed circuit is alson-leakage resilient, under the assumption that the randoms in the composedcomponents are disjoint. Fig. 4 shows the diagram of the composition. We stateand prove the parallel compositionality result formally in Section 3.1, and thesequential compositionality result in Section 3.2.
We remark that, in the sequential composition, if a (non-split) secret input,
say k, is shared by some P1i and P1j for i 6= j, then the disjoint randomness
condition requires k to be encoded by two independent input encoders. This is incontrast to the previous works [5, 3] that only use one input encoder per a secret
input. On the other hand, such works require additional randoms at the site of
the composition, whereas no additional randoms are needed at the compositionsite in our case as it directly connects the split outputs of P1i ’s to the split inputsof P2 .

WϮ͛

WϮ

WϮ͛
ǀϰ

Wϭϭ

ǀϱ

WϭϮ

Wϭϭ͛

Wϭϭ͛
WϭϮ͛
ǀϭ

ǀϭ

ǀϮ

WϭϮ͛
ǀϮ

ǀϯ

ǀϯ

Fig. 4. Sequential composition of P11 , P12 , and P2 . Here, P11 ′ (resp. P12 ′ ) is the outputdecoder-free part of P11 (resp. P12 ), and P2 ′ is the input-encoder-free part of P2 . The
composition connects the split outputs of P11 ′ and P12 ′ to the split inputs of P2 ′ .

3.1

Parallel Composition

This subsection proves the parallel compositionality result. Let us write P1 ||P2
for the parallel composition of P1 and P2 . We state and prove the result.
Theorem 2. Let P1 and P2 be n-leakage-resilient circuits having disjoint randoms. Then, P1 ||P2 is also n-leakage-resilient.
Remark 3. While Theorem 2 only states that P1 ||P2 can withstand an attack
that observes up to n nodes total from the composed circuit, a stronger property
can actually be derived from the proof of the theorem. That is, the proof showsthat P1 ||P2 can withstand an attack that observes up to n nodes from the P1
part and up to n nodes from the P2 part. (However, it is not secure against an
attack that picks more than n nodes in an arbitrary way: for example, picking
n + 1 nodes from one side.)
3.2

Sequential Composition

This subsection proves the sequential compositionality result. As remarked above,
the result is significantly harder to prove than the parallel compositionality result. Let us write (P11 , . . . , P1y )⊲P2 for the sequential composition of P11 , . . . , P1ywith a y-input circuit P2 . We state and prove the sequential compositionality
result.
Theorem 3. Let P11 , . . . , P1y be n-leakage-resilient circuits, and P2 be an yinput n-leakage-resilient circuit, having disjoint randoms. Then, (P11 , . . . , P1y )⊲P2 is n-leakage-resilient.
Example 2. As remarked in Section 3, the parallel compositionality result enjoys an additional property that the circuit is secure even under an attack thatobserves more than n nodes in the composition as long as the observation ineach component is at most n. We show that the property does not hold in thecase of sequential composition. Indeed, it can be shown that just allowing n + 1
observations breaks the security even if the number of observations made withineach component is at most n.
To see this, consider the n+1-split circuit
shown in Fig. 6. The circuit implements theidentity function, and it is easy to see thatŽ ْŽ ْ ‫ْ ڮ‬Žthe circuit is n-leakage resilient. Let P1 andŽŽŽ
P2 be copies of the circuit, and consider the䞉䞉䞉composition (P1 ) ⊲ P2 . Then, the composedƌ
circuit is not secure against an attack thatƌŬْƌ ْ ‫ْ ڮ‬ƌobserves m nodes of P1 for some 1 ≤ m ≤ n,
Ŭand observes n + 1 − m nodes of P2 such thatthe nodes picked on the P2 side are the nodes
connected to the nodes that are not picked on Fig. 6. An n-leakage resilient identity circuit.
the P1 side.
ϭ

ϭ

Ϯ

ϭ

Ŷнϭ

Ŷнϭ

Ϯ

Ϯ

ϭ

Ŷ

WϮϭ

WϮϭ͛

WϮϮ

WϮϮ͛
WϮϭ͛

WϮϮ͛

ǀ

ǀ

Wϭ͛

Wϭ

Wϭ͛
ǀϭ
ǀϭ

ǀϮ

ǀϮ

Fig. 5. Output-sharing sequential composition of P1 , P21 , and P22 . Here, P1 ′ is theoutput-decoder-free part of P1 , and P21 ′ (resp. P22 ′ ) is the input-encoder-free part ofP21 (resp. P22 ). The composition connects the split output of P1 ′ to the split inputs of
P21 ′ and P22 ′ .

Remark 4. By a reasoning similar to the one used in the proof of Theorem 3, we
can show the correctness of a more parsimonious version of parallel composition
theorem (Theorem 2) where given P1 and P2 that shares a secret, instead of
P1 ||P2 duplicating split shares of the secret as in Fig. 3, we make one split
share tuple to be used in the both sides of the composition. Combining thisimproved parallel composition with the sequential compositionality result, we
obtain compositionality for the case where an output of a circuit is shared bymore than one circuit in a sequential composition.
Fig. 5 depicts such an output-sharing sequential composition. Here, P1 , P21 ,and P22 are n-leakage-resilient circuits, and we wish to compose them by connecting the output of P1 to the input of P21 and the input of P22 . By the parallel
compositionality result, the parallel composition of P21 and P22 that shares thesame input (v) is n-leakage-resilient. Then, it follows that, sequentially composing that parallelly composed circuit with P1 , as depicted in the figure, is alson-leakage-resilient thanks to the sequential compositionality result.

4

Compositional Synthesis Algorithm

The compositionality property gives a way for a compositional approach to synthesizing leakage-resilient circuits. Algorithm 1 shows the overview of the synthesis algorithm. Given a random-free circuit as an input, the algorithm synthesizes
an IO-equivalent n-leakage-resilient circuit. It first invokes the Decomp operation to choose a suitable decomposition of the given circuit into some number of
sub-circuits. Then, it invokes MonoSynth on each sub-circuit Pi to synthesize
an n-leakage resilient circuit Pi ′ that is IO-equivalent to Pi . Finally, it returns

the composition of the obtained circuits as the synthesized n-leakage resilient
version of the original.
Algorithm 1 The Compositional Synthesis Algorithm
Input: Random-free Circuit P
Output: IO-equivalent n-leakage-resilient circuit
1: P1 , . . . , Pm := Decomp(P )2: for each Pi ∈ {P1 , . . . , Pm } do
3:
Pi ′ := MonoSynth(Pi )4: end for5: return Comp(P1 ′ , . . . , Pm ′ )Comp is the composition operation, and it composes the given n-leakageresilient circuits in the manner described in Section 3. MonoSynth is a constraintbased “monolithic” synthesis algorithm that synthesizes an n-leakage-resilient
circuit that is IO-equivalent to the given circuit without further decomposition.
We describe MonoSynth in Section 4.1, and describe the decomposition operation Decomp in Section 4.2.
The algorithm optimizes the synthesized circuits in the following ways. First,
as described in Section 4.1, the monolithic synthesis looks for tree-shaped circuitsof the shortest tree height. Secondly, as described in Section 4.2, the decomposition and composition is done in a way to avoid unnecessarily making the nonsecret-dependent parts leakage resilient, and also to re-use the synthesis results
for shared sub-circuits whenever allowed by the compositionality properties.
Remark 5. The compositional algorithm composes the n-leakage-resilient versions of the sub-circuits. Note that the compositionality property states thatthe result will be n-leakage-resilient after the composition, regardless of how the
sub-circuits are synthesized as long as they are also n-leakage-resilient and havedisjoint randoms. Thus, in principle, any method to synthesize the n-leakageresilient versions of the sub-circuits may be used in place of MonoSynth. For
instance, a possible alternative is to use a database of n-leakage-resilient versionsof commonly-used circuits (e.g., obtained via the construction of [15, 5]).
4.1

Constraint-Based Monolithic Synthesis

The monolithic synthesis algorithm is based on and extends the constraint-based
approach proposed by Eldib and Wang [8]. The algorithm synthesizes an nleakage-resilient circuit that is IO-equivalent to the given circuit. The algorithm
requires the given circuit to have only one output. Therefore, the overall algorithm to decomposes the whole circuit into such sub-circuits before passing themto MonoSynth.
We formalize the algorithm as quantified first-order logic constraint solving.
Let P be the random-free circuit given as the input. We prepare a quantifier-free

Žϭ

ŽϭْŽϮ

Dϭ
DϮ

ŽϮ

Dϰ
Dϯ

Dϱ

Dϲ

Ŭْƌ

ƌ

oV= α1 ⊕ α4 ∧i∈{1,4} ((Ci = XOR ⇒ αi = αi+1 ⊕ αi+2 ) ∧(Ci = AND ⇒ αi = αi+1 ∧ αi+2 ) ∧(C
i = OR ⇒ αi = αi+1 ∨ αi+2 )) ∧V((C
i = F ⇒ αi = 0) ∧ (Ci = T ⇒ αi = 1) ∧i∈{2,3,5,6}(Ci = P ⇒ αi = p) ∧ (Ci = K1 ⇒ αi = r) ∧(Ci = K2 ⇒ αi = k ⊕ r))

Ŭ

(a)

(b)

Fig. 7. (a) Skeleton circuit. (b) ΦSk2 for the skeleton circuit.

formula ΦP (α, p, k, o) on the free variables α, p, k, o that encodes the inputoutput behavior of P . Formally, ∃α.ΦP (α, p, k, o) is true iff P outputs o given
public inputs p and secret inputs k. The variables α are used for encoding theshared sub-circuits within P (i.e., gates of fan-out > 1). For example, for P that
outputs k ∧ p, ΦP (p, k, o) ≡ o = k ∧ p.
Adopting the approach of [8], our monolithic algorithm works by preparing
skeleton circuits of increasing size, and searching for an instance of the skeleton that is n-leakage-resilient and IO-equivalent to P . By starting from a small
skeleton, the algorithm biases toward finding an optimized leakage resilient circuit. Formally, a skeleton circuit Skℓ is a tree-shaped circuit (i.e., circuit withall non-input gates having fan-out of 1) of height ℓ whose gates have undetermined functionality except for the parts that implement the input encoder andthe output decoder. For example, Fig. 7 (a) shows the 1+1-split skeleton circuitof height 2 with one secret input.
We prepare a quantifier-free skeleton formula ΦSkℓ that expresses the skeleton
circuit. Formally, ΦSkℓ (C, α, p, k, r, o) is true iff P ′ outputs o with the valuationsof nodes(P ′ ) having the values α given public inputs p, secret inputs k, andrandom inputs r where P ′ is Skℓ with its nodes’ functionality determined by
C.6 We call C the control variables, and write Skℓ (C) for the instance of Skℓdetermined by C. For example, Fig. 7 (b) shows ΦSkℓ for the skeleton circuitfrom Fig. 7 (a), when there is one public input and no randoms besides the one
from the input encoder.
The synthesis is now reduced to the problem of finding an assignment toC that satisfies the constraint Φio (C) ∧ Φlr (C) where Φio (C) expresses thatSkℓ (C) is IO-equivalent to P , and Φlr (C) expresses that Skℓ (C) is n-leakageresilient. As we shall show next, the constraints faithfully encode IO-equivalence
and leakage-resilience according to the definitions from Section 2.
6

Technically, the number of randoms (i.e., r) can also be left undetermined in theskeleton. Here, for simplicity, we assume that the number of randoms is determinedby the factors such as n, the skeleton height, and the number of secret inputs.

Φio (C) is the formula below.
∀α, α′ , p, k, r, o, o′ . ΦP (α, p, k, o) ∧ ΦSkℓ (C, α′ , p, k, r, o′ ) ⇒ o = o′
It is easy to see that Φio correctly expresses IO equivalence.
The definition of Φlr is more involved, and we begin by introducing a usefulshorthand notation. Let m be the number of (observable) nodes in Skℓ . Without
loss of generality, we assume that m ≥ n. Let σ ∈ {1, . . . , m}∗ be a sequencesuch that |σ| ≤ n, and α = α1 , . . . , αm be a length m sequence of variables. We
write αhσi for the sequence of variables β1 , . . . β|σ| such that βi = ασi for eachi ∈ {1, . . . , |σ|}. Intuitively, σ represents a selection of nodes observed by theadversary. For example, let α = α1 , α2 , α3 and σ = 1, 3, then αhσi = α1 , α3 .
Let R = {0, 1}|r| . Then, Φlr (C) is the formula below.
′′∀σ.∀β,V α , p, k, k , o.
′′′b∈R φ[αP b /α][ob /o] ∧ φ[αb /α][oP b /o][k ′/k]⇒b∈R (αb hσi = β) =b∈R (αb hσi = β)where α′ is a sequence comprising distinct variables αb and α′b such that |αb | =|α′b | = m for each b ∈ R, o is a sequence comprising distinct variables ob and o′bfor each b ∈ R, and φ is the formula ΦSkℓ (C, α, p, k, b, o). While Φlr (C) is notstrictly a first-order logic formula, it can be converted to the form by expanding
the finitely many possible choices of σ.
Algorithm 2 MonoSynth
Input: Random-free Circuit P
Output: IO-equivalent n-leakage resilient circuit
1: ℓ := INIT HEIGHT
2: loop3:
tset := ∅; γ := n
4:
loop
5:
match FindCand(tset,γ) with
6:
nosol → ℓ++; break7:| sol(bC ) → match CheckCand(bC ) with8:
success → return Skℓ (bC )9:| cex(tset′ , γ ′ ) → tset := tset ∪ tset′ ; γ := max(γ, γ ′ )10:end loop
11: end loop

Because the domains of the quantified variables in Φio and Φlr are finite,
one approach to solving the constraint may be first eliminating the quantifiers
eagerly and then solving for C that satisfies the resulting constraint. However,
the approach is clearly impractical due to the extreme size of the resulting constraint. Instead, adopting the idea from [8], we solve the constraint by lazily
instantiating the quantifiers. The main idea is to divide the constraint solving

process in two phases: the candidate finding phase that infers a candidate solution for C, and the candidate checking phase that checks whether the candidate
is actually a solution. We run the phases iteratively in a CEGAR style untilconvergence. Algorithm 2 shows the overview of the process. We describe thedetails of the algorithm below.
Candidate Checking. The candidate checking phase is straightforward. Note
that, after expanding the choices of σ in Φlr , Φio (C) ∧ Φlr (C) only has outermost ∀ quantifiers. Therefore, given a concrete assignment to C, bC , CheckCanddirectly solves the constraint by using an SMT solver.7 (However, naively expanding σ can be costly when n > 1, and we show a modification that alleviates
the cost in the later part of the subsection.)
Candidate Finding. We describe the candidate finding process FindCand. To
find a likely candidate, we adopt the idea from [8] and prepare a test set that is
updated via the CEGAR iterations. In [8], a test set, tset, is a pair of sets tsetp
and tsetk where tsetp (resp. tsetk ) contains finitely many concrete valuations ofp (resp. k). Having such a test set, we can rewrite the constraint so that the
public inputs and secret inputs are restricted to those from the test set. That is,Φio (C) is rewritten to be the formula below.
V(bp ,bk )∈tsetp ×tsetk

ΦP (αbp bk , bp , bk , obp bk ) ∧ ΦSkℓ (C, α′bp bk , bp , bk , rbp bk , o′bp bk ) ∧ obp bk = o′bp bk

And, Φlr (C) becomes the formula below.
VV∀σ.∀β. (bp ,bk ,bk ′ )∈tsetp ×tsetk ×tsetk b∈R
φ[αbp bk b /α][obp bk b /o][bk /k] ∧ φ[α′bp b′ b /α][o′bp b′ b /o][b′k /k]
k
k
P
P
′
∧
b∈R (αbp bk b hσi = β) =b∈R (αbp b′ b hσi = β)kwhere φ is the formula ΦSkℓ (C, α, bp , k, b, o). We remark that, because fixing the
inputs to concrete values also fixes the valuations of some other variables (e.g.,
fixing p and k also fixes α and o in ΦP (α, p, k, o)), the constraint structure ismodified to remove the quantifications on such variables.
At this point, the approach of [8] can be formalized as the following process:it eagerly instantiates the possible choices of σ and β to reduce the constraint
to a quantifier-free form, and looks for a satisfying assignment to the resulting
constraint. This is a sensible approach when n is 1 because, in that case, thenumber of possible choices of σ is linear in the size of the skeleton (i.e., is m)
and the possible valuations of β are simply {0, 1}. Unfortunately, the number ofpossible choices of σ grows exponentially in n, and so does that of the possible
valuations of β.8 We remark that this is expected because σ represents the7

Also, because C are the only shared variables in Φio and Φlr , the two may be checkedindependently after instantiating C.
8Therefore, the complexity of the method is at least double exponential in n assumingthat the complexity of the constraint solving process is at least exponential in thesize of the given formula.

adversary’s node selection choice, and β represents the valuation of the selected
nodes. Indeed, in our experience with a prototype implementation, this method
fails even on quite small sub-circuits and with n just 2.
Therefore, we make the following improvements to the base algorithm.
(1) We restrict the node selection to root-most γ nodes where γ starts at n andis incremented via the CEGAR loop.
(2) We include node valuations in the test set.
(3) We use dependency analysis to reduce irrelevant node selections from theconstraint in the candidate checking phase.
The rationale for prioritizing the root-most nodes in (1) is that, in a tree-shaped
circuit, nodes closer to the root are more likely to be dependent on the secret
and therefore are expected to be better targets for the adversary. The numberof root-most nodes to select, γ, is incremented as needed by a counterexample
analysis (cf. lines 7-9 of Algorithm 2). The test set generation for node valuations
described in item (2) is done in much the same way as that for public inputs andsecret inputs. We describe the test set generation process in more detail in Test
Set Generation. With the modifications (1) and (2), the leakage-resilience constraint to be solved in the candidate finding phase is now the following formula.
VV∀σ :γ. (bp ,bk ,bk ′ ,bβ )∈tsetp ×tsetk ×tsetk ×tsetβ b∈R
φ[αbp bk b /α][obp bk b /o][bk /k] ∧ φ[α′bp b′ b /α][o′bp b′ b /o][b′k /k]
k
k
P
P
′
∧
b∈R (αbp b′ b hσi = bβ )b∈R (αbp bk b hσi = bβ ) =kwhere σ : γ restricts σ to the root most γ indexes, tsetβ is the set of test set
elements for node valuations, and φ is the formula ΦSkℓ (C, α, bp , k, b, o).
Unlike (1) and (2), the modification (3) applies to the candidate checking
phase. To see the benefit of this modification, note that, even in the candidate
checking phase, checking the leakage-resilience condition Φlr (bC ) can be quite
expensive because it involves expanding exponentially many possible choices
of node selections. To mitigate the cost, we take advantage of the fact thatthe candidate circuit is fixed in the candidate checking phase, and do a simple
dependency analysis on the candidate circuit to reduce irrelevant node-selection
choices. We describe the modification in more detail. Let P ′ be the candidate
circuit. For each node of P ′ , we collect the reachable leafs from the node toobtain the over-approximate set of inputs on which the node may depend. For anode α of P ′ , let deps(α) be the obtained
set of dependent inputs for α. Then,S
any selection of nodes α such that α∈{α} deps(α) does not contain all n+1split shares of some secret is an irrelevant selection and can be removed fromthe constraint. (Here, we use the symbols α for node labels as in Section 2, andnot as node-valuation variables in a constraint.)
Test Set Generation. Recall that our algorithm maintains three kinds of test
sets, tsetp for public inputs, tsetk for secret inputs, and tsetβ for node valuations.
As shown in lines 7-9 of Algorithm 2, we obtain new test set elements fromcandidate check failures (here, by abuse of notation, we write tset ∪ tset′ for the

component-wise union). We describe the process in more detail. In CheckCand,
we convert the constraint Φio (bC ) ∧ Φlr (bC ) to a quantifier free formula Φ byexpanding the selection choices and removing the universal quantifiers. Then,
we use an SMT solver to check the satisfiability of ¬Φ and return success if it isunsatisfiable. Otherwise, the SMT solver returns a satisfying assignment of ¬Φ,and we return the values assigned to variables corresponding to public inputs,
secret inputs and node valuations as the new elements for the respective test
sets. The number of root-most nodes to select is also raised here by taking the
maximum of the root-most nodes observed in the satisfying assignment, γ ′ , withthe current γ.
4.2

Choosing Decomposition

This subsection describes the decomposition procedure Decomp. Thanks to thegenerality of the compositionality results, in principle, we can decompose thegiven circuit into arbitrarily small sub-circuits (i.e., down to individual gates).
However, choosing a too fine-grained decomposition may lead to a sub-optimal
result.9
To this end, we have implemented the following decomposition strategy. First,
we run a dependency analysis, similar to the one used in the constraint-basedmonolithic synthesis (cf. Section 4.1). The analysis result is used to identify theparts of the given circuit that do not depend on any of the secrets. We factor
out such public-only sub-circuits from the rest so that they will not be subject
to the leakage-resilience transformation.
Next, we look for sub-circuits that are used at multiple locations (i.e., whoseroots have fan-out > 1), and prioritize them to be synthesized separately andcomposed at their use sites. Besides the saving in the synthesis effort, the approach can lead a smaller synthesis result when the shared sub-circuit is usedin contexts that lead to different outputs (cf Remark 4). Finally, as a general
strategy, we apply parallel composition at the root so that we synthesize separately for each output given a multi-output circuit. And, we set a bound on
the maximum size of the circuits that will be synthesized monolithically, anddecompose systematically based on the bound. As discussed in Section 5, in the
prototype implementation, we use an “adaptive” version of the latter decomposition process by adjusting the bound on-the-fly and also opting for a pre-madecircuit under certain conditions.
Example 3. Let us apply the compositional synthesis algorithm to the circuitfrom Fig. 2, for the case n = 2. Note that the circuit has no non-trivial publiconly sub-circuits or have non-inputs gates with fan-out greater than 1.
First, we apply the parallel compositionality result so that the circuit isdecomposed to two parts: the left tree that computes p1 ⊕ k1 ⊕ k2 and the righttree that computes k2 ⊕ p2 . The right tree cannot be decomposed further, andwe apply MonoSynth to transform it to a leakage-resilient form. A possible9

One may make the analogy to compiler optimization. Such a decomposition strategy
is analogous to optimizing each instruction individually.

name
P1
P2
P3
P4
P5
P6
P7
P8
P9

n=2
n=3
n=4
n=2
n=3
n=4
name
time size rds time size rds time size rds
time size rds time size rds time size rds
16.2s 123 32 49.4s 138 48 52.7s 160 64 P10
T/O
M/O
M/O
10.3s 64 16 1m13s 76 24 4m3s 88 32 P11
T/O
T/O
M/O
M/O
M/O
M/O
P12
T/O
T/O
T/O
M/O
M/O
M/O
P13
T/O
T/O
T/O
M/O
M/O
M/O
P14
T/O
T/O
M/O
M/O
M/O
M/O
P15
T/O
T/O
M/O
M/O
M/O
M/O
P16
T/O
T/O
T/O
M/O
M/O
M/O
P17
T/O
T/O
T/O
T/O
T/O
T/O
P18
T/O
T/O
T/O

Table 1. Experiment Results: Monolithic Only.

name
P1
P2
P3
P4
P5
P6
P7
P8
P9
P10
P11
P12
P13
P14
P15
P16
P17
P18

n=2
n=3
n=4
time
mtc
size rds
time
mtc
size rds
time
mtc
size rds
18.7s
2.7s
125
32
30.2s
4.5s
143
48
1m1s
33.3s
160
64
11.8s
3.6s
65
16
1m7s
17.3s
74
24
2m56s
1m21s
88
32
2.7s
0.8s
50
11
12.3s
6.9s
83
18
3m57s
1m4s
120
26
3.9s
3.1s
42
9
4.5s
2.1s
69
15
1m48s
1m4s
100
22
5.9s
2.1s
63
13
20.2s
6.9s
108
21
5m12s
1m4s
140
30
5.3s
1.4s
65
13
17.4s
6.9s
108
21
4m57s
1m7s
141
30
2m52s 1m28s 80
156m13s
4m6s 16330
9m7s
2m42s 231
44
3m10s 1m48s 77
155m8s
3m19s 16130
8m47s
1m44s 234
44
1.2s
1.1s
33
9
2m58s
2m55s 58
15
1m7s
1m5s
87
22
2m2s
1m1s 583 146
18m37s 4m46s 1027 249
26m51s
5m2s 1598 372
4m9s
1m5s 464 112
24m41s 5m25s 814 192
46m12s 18m28s 1269 288
10m33s 1m5s 1507 370 1h4m19s 5m56s 2643 633 2h14m24s 27m1s 4116 948
17m7s
3.4s 14369 1088
50m5s
16.1s 21163 1824 10h27m40s 1m58s 22123 2688
17m12s3.4s 14369 1088
50m0s
16.0s 21163 1824 10h27m47s 2m21s 22153 2688
17m15s3.4s 14625 1088 52m32s
16.4s 21763 1824 10h30m26s 1m35s 22927 2688
16m39s3.4s 14553 1088 52m10s
14.9s 21773 1824 10h24m23s 1m27s 22922 2688
5h28m27s 4m3s 16066 1594 19h11m33s 7m46s 23568 2592 17h37m27s 2m36s 25236 3712
34m42s3.7s 60111 3968 1h37m9s 15.5s 78418 6144 17h43m2s 1m54s 74847 8448

Table 2. Experiment Results: Compositional.

synthesis result of this is the right sub-circuit shown in Fig. 1 (i.e., the subcircuit whose observable part outputs the split output o4 , o5 , o6 ).
For the left tree, if the monolithic-synthesis size bound is set to synthesize
circuits of height 2, we apply MonoSynth directly to the tree. Alternatively,
with a lower bound set, we further decompose the left tree to a lower part thatcomputes p1 ⊕ k1 and p2 (identity function) and an upper part that computes
k ⊕p2 where the output of the lower part is to be connected to the “place-holder”
input k. Following the either strategy, we may obtain the left sub-circuit of Fig. 1
as a possible result. And, the final synthesis result after composing the left andright synthesis results is the whole circuit of Fig. 1.

5

Implementation and Experiments

We have implemented a prototype of the compositional synthesis algorithm. The
implementation takes as input a finite-data loop-free C program and converts
the program into a Boolean circuit in the standard way. We remark that, inprinciple, a program with non-input-dependent loops and recursive functions
may be converted to such a form by loop unrolling and function inlining.
The implementation is written in the OCaml programming language. We
use CIL [19] for the front-end parsing and Z3 [6] for the SMT solver used in
the constraint-based monolithic synthesis. The experiments are conducted on amachine with a 2.60GHz Intel Xeon E5-2690v3 CPU with 8GB of RAM runninga 64-bit Linux OS, with the time limit of 20 hours.
We have run the implementation on the 18 benchmark programs taken fromthe paper by Eldib and Wang [8]. The benchmarks are (parts of) various cryptographic algorithm implementations, such as a round of AES, and we referto their paper for the details of the respective benchmarks (we use the same
program names).10 Whereas their experiments synthesized leakage-resilient versions of the benchmarks only for the case n is 1, in our experiments, we do thesynthesis for the cases n = 2, n = 3, and n = 4.
We describe the decomposition strategy that is implemented in the prototype.
Specifically, we give details of the online decomposition process mentioned in
Section 4.2. The implementation employs the following adaptive strategy when
decomposing systematically based on a circuit size bound. First, we set the boundto be circuits of some fixed height (the experiments use height 3), and decompose
based on the bound. However, in some cases, the bound can be too large forthe monolithic constraint-based synthesis algorithm to complete in a reasonableamount of time. Therefore, we set a limit on the time that the constraint-based
synthesis can spend on constraint solving, and when the time limit is exceeded,
we further decompose that sub-circuit by using a smaller bound. Further, when
the time limit is exceeded even with the smallest bound, or the number of secrets
in the sub-circuit exceeds a certain bound (this is done to prevent out of memory
exceptions in the SMT solver), we use a pre-made leakage resilient circuit. Recall
from Remark 5 that the compositionality property ensures the correctness of sucha strategy.
Tables 1 and 2 summarize the experiment results. Table 2 shows the results of the compositional algorithm. Table 1 shows the results obtained bythe“monolithic-only” version of the algorithm. Specifically, the monolithic-onlyresults are obtained by, first applying the parallel compositionality property(cf. Section 3.1) to divide the given circuit into separate sub-circuit for each
output, and then applying the constraint-based monolithic synthesis to each
sub-circuit and combining the results. (The per-output parallel decomposition isneeded because the constraint-based monolithic synthesis only takes one-output
circuits as input – cf. Section 4.1.) The monolithic-only algorithm is essentiallythe monolithic algorithm of Eldib and Wang [8] with the improvements describedin Section 4.1.
10Strangely, some of the benchmarks contain inputs labeled as “random” and haverandom IO behavior (when those inputs are actually treated as randoms), despite
the method of [8] only supporting programs with non-random (i.e., deterministic)
IO behavior. We treat such “random” inputs as public inputs in our experiments.

We describe the table legends. The column labeled “name” shows the benchmark program names. The columns labeled “time” show the time taken to synthesize the circuit. Here, “T/O” means that the algorithm was not able to finish
within the time limit, and “M/O” means that the algorithm aborted due to an
out of memory error. The columns labeled “size” show the number of gates in thesynthesized circuit, and the columns labeled “rds” show the number of randoms
in the synthesized circuit.
The columns labeled “mtc” in Table 2 is the maximum time spent by the algorithm to synthesize a sub-circuit in the compositional algorithm. Our prototype
implementation currently implements a sequential version of the compositionalalgorithm where each sub-circuit is synthesized one at a time in sequence. However, in principle, the sub-circuits may be synthesized simultaneously in parallel,
and the columns mtc give a good estimate of the efficiency of such a parallel version of the compositional algorithm. We also remark that the current prototype
implementation is unoptimized and does not “cache” the synthesis results, andtherefore, it naively applies the synthesis repeatedly on the same sub-circuitsthat have been synthesized previously.
As we can see from the tables, the monolithic-only approach is not able tofinish on many of the benchmarks, even for the case n = 2. In particular, it
does not finish on any of the large benchmarks (as one can see from the sizes ofthe synthesized circuits, P13 to P18 are of considerable sizes). By contrast, thecompositional approach was able to successfully complete the synthesis for all
instances. We observe that the compositional approach was faster for the largern in some cases (e.g., P9 with n = 3 vs. n = 4). While this is partly due tothe unpredictable nature of the back-end SMT solver, it is also an artifact ofthe decomposition strategy described above. More specifically, in some cases, thealgorithm more quickly detects (e.g., in earlier iterations of the constraint-based
synthesis’s CEGAR loop) that the decomposition bound should be reduced forthe current sub-circuit, which can lead to a faster overall running time.
We also observe that the sizes of the circuits synthesized by the compositional approach are quite comparable to those of the ones synthesized by themonolithic-only approach, and the same observation can be made to the numbers of randoms in the synthesized circuits. In fact, in one case (P2 with n = 3),
the compositional approach synthesized a circuit that is smaller than the one
synthesized by the monolithic-only approach. While this is due in part to thefact that the monolithic synthesis algorithm optimizes circuit height rather thansize, in general, it is not inconceivable for the compositional approach to do better than the monolithic-only approach in terms of the quality of the synthesizedcircuit. This is because the compositional method could make a better use of thecircuit structure by sharing synthesized sub-circuits, and also because of parsimonious use of randoms allowed by the compositionality property. We remarkthat the circuits synthesized by our method are orders of magnitude smaller
than those obtained by naively applying the original construction of Ishai etal. [15] (cf. Theorem 1). For instance, for P18 with n = 4, the construction
would produce a circuit with more than 3600k gates and 500k randoms.

6

Related Work

Verification and Synthesis for n-Threshold-Probing Model of Leakage
Resilience. The n-threshold-probing model of leakage resilience was proposedin the seminal work by Ishai et al. [15]. The subsequent research has proposed
methods to build circuits that are leakage resilient according to the model [21, 5,
7, 9, 8, 4, 3]. Along this direction, the two branches of work that are most relevant
to ours are verification which aims at verifying whether the given (hand-crafted)
circuit is leakage resilient [9, 4, 3], and synthesis which aims at generating leakage
resilient circuits automatically [8]. In particular, our constraint-based monolithic
synthesis algorithm is directly inspired and extends the algorithm given by Eldib
and Wang [8]. As remarked before, their method only handles the case n = 1. Bycontrast, we propose the first compositional synthesis approach that also works
for arbitrary values of n.
On the verification side, the constraint-based verification method proposedin [9] is a precursor to their synthesis work discussed above, and it is similar
to the candidate checking phase of the synthesis. Recent papers by Barthe etal. [4, 3] investigate verification methods that aim to also support the case n > 1.
Compositional verification is considered in [3]. As remarked before, in contrast
to the compositionality property described in our paper, their composition does
not require disjointness of the randoms in the composed components but instead
require additional randoms at the site of the composition. We believe that thecompositionality property investigated in their work is complementary to ours,
and we leave for future work to combine these facets of compositionality.
We remark that synthesis is substantially harder than verification. Indeed,in our experience with the prototype implementation, most of the running time
is consumed by the candidate finding part of the monolithic synthesis processwith relatively little time spent by the candidate checking part.
Quantitative Information Flow. Quantitative information flow (QIF) [18,22, 23, 1] is a formal measure of information leak, which is based on an information theoretic notion such as Shannon entropy, Rènyi entropy, and channel
capacity. Recently, researchers have proposed QIF-based methods for side channel attack resilience [16, 17] whereby static analysis techniques for checking andinferring QIF are applied to side channels.
It is difficult to directly compare the QIF approach with the n-thresholdprobing model of leakage resilience. Whereas the notion of security ensured by
the latter is the absence of information leakage against an adversary of a certain restricted observation capability, the security ensured by the QIF approachis typically not of the form in which the adversary’s capability is restricted insome way, but instead some (small amount of) leak is permitted. We remark
that, as also observed by [4], in the terminology of information flow theory, then-threshold-probing model of leakage resilience corresponds to enforcing probabilistic non-interference [13] on every n-tuple of the circuit’s internal nodes.

7Conclusion

We have presented a new approach to synthesizing circuits that are leakage
resilient according to the n-threshold-probing model. We have shown that theleakage-resilience model admits a certain compositionality property, which roughly
says that composing n-leakage-resilient circuits results in an n-leakage-resilient
circuit, assuming the disjointness of the randoms in the composed circuit components. Then, by utilizing the property, we have designed a compositional synthesis algorithm that divides the given circuit into smaller sub-circuits, synthesizes
n-leakage-resilient versions of them containing disjoint randoms, and combines
the results to obtain an n-leakage-resilient version of the whole.
Acknowledgements. We thank the anonymous reviewers for useful comments.
This work was supported by MEXT Kakenhi 26330082 and 25280023, and JSPS
Core-to-Core Program, A.Advanced Research Networks.

References
1. M. S. Alvim, K. Chatzikokolakis, C. Palamidessi, and G. Smith. Measuring information leakage using generalized gain functions. In CSF 2012, pages 265–279,
2012.
2. J. Balasch, S. Faust, B. Gierlichs, and I. Verbauwhede. Theory and practice of aleakage resilient masking scheme. In ASIACRYPT 2012, pages 758–775, 2012.
3. G. Barthe, S. Belaı̈d, F. Dupressoir, P. Fouque, and B. Grégoire. Compositionalverification of higher-order masking: Application to a verifying masking compiler.
IACR Cryptology ePrint Archive, 2015:506, 2015.
4. G. Barthe, S. Belaı̈d, F. Dupressoir, P. Fouque, B. Grégoire, and P. Strub. Verified
proofs of higher-order masking. In EUROCRYPT 2015, pages 457–485, 2015.
5. J. Coron, E. Prouff, M. Rivain, and T. Roche. Higher-order side channel security
and mask refreshing. In FSE 2013, pages 410–424, 2013.
6. L. M. de Moura and N. Bjørner. Z3: an efficient SMT solver. In TACAS 2008,
pages 337–340, 2008.
7. A. Duc, S. Dziembowski, and S. Faust. Unifying leakage models: From probing
attacks to noisy leakage. In EUROCRYPT 2014, pages 423–440, 2014.
8. H. Eldib and C. Wang. Synthesis of masking countermeasures against side channel
attacks. In CAV 2014, pages 114–130, 2014.
9. H. Eldib, C. Wang, and P. Schaumont. SMT-based verification of software countermeasures against side-channel attacks. In TACAS 2014.
10. S. Faust, T. Rabin, L. Reyzin, E. Tromer, and V. Vaikuntanathan. Protecting
circuits from leakage: the computationally-bounded and noisy cases. In EUROCRYPT 2010, pages 135–156, 2010.
11. S. Goldwasser and G. N. Rothblum. Securing computation against continuous
leakage. In CRYPTO 2010, pages 59–79, 2010.
12. S. Goldwasser and G. N. Rothblum. How to compute in the presence of leakage.
In FOCS 2012, pages 31–40, 2012.
13. J. W. G. III. Toward a mathematical foundation for information flow security. In
1999 IEEE Symposium on Security and Privacy, pages 21–35, 1991.
14. Y. Ishai, M. Prabhakaran, A. Sahai, and D. Wagner. Private circuits II: keeping
secrets in tamperable circuits. In EUROCRYPT 2006, pages 308–327, 2006.

15. Y. Ishai, A. Sahai, and D. Wagner. Private circuits: Securing hardware againstprobing attacks. In CRYPTO 2003, pages 463–481, 2003.
16. B. Köpf and D. A. Basin. Automatically deriving information-theoretic bounds foradaptive side-channel attacks. Journal of Computer Security, 19(1):1–31, 2011.
17. B. Köpf, L. Mauborgne, and M. Ochoa. Automatic quantification of cache sidechannels. In CAV 2012, pages 564–580, 2012.
18. P. Malacaria. Assessing security threats of looping constructs. In POPL 2007,
pages 225–235, 2007.
19. G. C. Necula, S. McPeak, S. P. Rahul, and W. Weimer. CIL: Intermediate language
and tools for analysis and transformation of C programs. In CC 2002, pages 213–
228, 2002.
20. E. Prouff and M. Rivain. Masking against side-channel attacks: A formal security
proof. In EUROCRYPT 2013, pages 142–159, 2013.
21. M. Rivain and E. Prouff. Provably secure higher-order masking of AES. In CHES
2010, pages 413–427, 2010.
22. G. Smith. On the foundations of quantitative information flow. In FOSSACS 2009,
pages 288–302, 2009.
23. H. Yasuoka and T. Terauchi. Quantitative information flow - verification hardness
and possibilities. In CSF 2010, pages 15–27, 2010.

A

ProofsA.1

Proof of Theorem 2

Theorem 2. Let P1 and P2 be n-leakage-resilient circuits having disjoint randoms. Then, P1 ||P2 is also n-leakage-resilient.
Proof. Without loss of generality, we assume that P1 and P2 have the same
public and secret inputs (otherwise, they can be made so by adding dummyconnections). Let r1 (resp. r2 ) be the randoms in P1 (resp. P2 ). Let p (resp. k)
be the public (resp. secret) inputs of P1 ||P2 . Then, the result follows because forany bp ∈ {0, 1}|p| , bk , bk ′ ∈ {0, 1}|k| , α ∈ nodes(P1 ||P2 )n , and bα ∈ {0, 1}n , wehave
#P1 ||P2 (bp , bk , α, bα ) =2|r2 | · #P1 (bp , bk , α1 , bα1 ) + 2|r1 | · #P2 (bp , bk , α2 , bα2 ) =2|r2 | · #P1 (bp , b′k , α1 , bα1 ) + 2|r1 | · #P2 (bp , b′k , α2 , bα2 ) =#P1 ||P2 (bp , bk ′ , α, bα )where α1 and α2 partition α to the nodes inside P1 and those inside P2 , and bα1(resp. bα2 ) is the part of bα corresponding to the valuations of α1 (resp. α2 ).
⊓⊔A.2

Proof of Theorem 3

For simplicity, we assume that the circuits have no public inputs, and P2 only
has one (non-split) output. But, the result can be easily extended to the casewith public inputs and the case where P2 has multiple outputs.
We first focus on the case where P2 has only one (non-split) input. That is,
we consider the case where we are given P1 that takes x many inputs and P2
that takes one input. Therefore, the goal is to show the following.

Theorem 4. Let P1 be an x-input n-leakage-resilient circuit and P2 be an 1input n-leakage-resilient circuit, having disjoint randoms. Then, (P1 ) ⊲ P2 isn-leakage-resilient.
The general case where P2 takes multiple inputs follows directly from the proofof this case and is deferred to Section A.2.
We begin by introducing preliminary definitions and notations that are usedin the proof. We represent circuits by their truth tables (or, simply tables) whose
columns are the (observable) nodes of the circuit and rows are the possible
valuation of the nodes. Formally, for an x-input circuit P that is n+1-share
split, the table of P , tbl (P ), has its first (n + 1) · x columns correspond to
the input nodes,11 followed by some number of intermediate nodes (which may
include additional randoms), and followed by n + 1 columns corresponding tothe output nodes. We write #rows(t) (resp. #cols(t)) for the number of rows
(resp. columns) of the table t. We write t[i] for the ith row of the table, andt(i, j) for the value of the (i, j)th entry of t.
Example 4. Below is a table for the 1+1-share split 1-input circuit. The circuithas 6 nodes α1 , . . . , α6 where the (split) input nodes are α1 , α2 , the intermediate
nodes are α3 , α4 such that α3 is an additional random node, and the (split)
output nodes are α5 , α6 . The circuit is wired so that α4 = α1 ⊕ 1, α5 = α4 ⊕ α3 ,and α6 = α2 ⊕ α3 . That is, the circuit outputs the XOR of the input with 1 (i.e.,
it is a negation circuit).
α1 α2 α3 α4 α5 α60 0 0 1 1 0
0 0 1 1 0 1
1 1 0 0 0 1
1 1 1 0 1 0
1 0 0 0 0 0
1 0 1 0 1 1
0 1 0 1 1 1
0 1 1 1 0 0
Leakage Resilience as Table Safety The notion of n-leakage-resilience canbe formalized as a certain property of tables, which we call safety. Informally, atable being n safe means that, the number of rows of the table corresponding toeach (non-split) input remains the same even after reducing the table n times
by choosing a column and a bit and removing the rows that do not have that
bit at that column. We formalize the notion below.
Let b ∈ {0, 1}x and m > 0. For a ∈ L{0, 1}∗ of length at least x · m, we writea x,m b if for each i ∈ {1, . . . , x}, bi = (i−1)·m<j≤i·m aj . Let t be a table suchthat #cols(t) ≥ x · m. The b restriction of t wrt m, written bm (t), is defined to11

For simplicity, we assume that each secret (non-split) input in P1 and P2 is split
into shares by a single input encoder. The proof can be adopted to the case where asecret is encoded by multiple input encoders.

be a table comprising the rows i of t such that t[i] x,m b. Intuitively, bn+1 (t) is
the sub-table of t comprising the rows with the non-split input b (for the n+1
split case). For example, let t be the table from Example 4, then 02 (t) is thetable comprising the first four rows of t, and 12 (t) is the table comprising theremaining (i.e., the last four) rows of t.
(j,b)

For (j, b) ∈ {1, . . . , #cols(t)} × {0, 1}, we write t′ ←−−− t if t′ is t but with the(j,b)

rows having the value ¬b at the jth column removed. Intuitively, t ←−−− tbl (P )means that t is the state of the circuit P after the adversary observed the value
b at the jth node. For m ≥ 0, we write t′ ←m t if t′ is obtained by m adversary
observations from t, that is, if there exist (j1 , b1 ), . . . , (jm , bm ) such that t = t1 ,(ji ,bi )t′ = tm , and ti+1 ←−−−− ti for each i ∈ {1, . . . , m − 1}.
Let m ≥ 0 and ℓ > 0. We define the notion x∼m, ℓ safe inductively as follows.
We say that a table t is x ∼ 0, ℓ safe if for any b, b′ ∈ {0, 1}x , #rows(bℓ (t)) =#rows(b′ ℓ (t)). For m > 0, t is x ∼ m, ℓ safe if for any t′ such that t′ ←1 t, t′ isx ∼ m − 1, ℓ safe. Note that an empty table is x ∼ m, ℓ safe for any x, m and ℓ.
Also, it is immediate from the definition that safety is monotonic, that is, if t isx ∼ m1 , ℓ safe and m1 ≥ m2 then t is also x ∼ m2 , ℓ safe. Also, the following isimmediate from the definition.
Lemma 1. Suppose m1 ≤ m2 . Then, t is x ∼ m2 , ℓ safe iff for any t′ such thatt′ ←m1 t, t′ is x ∼ m2 − m1 , ℓ safe.
It is easy to see that the notion of safety captures leakage resilience. That is,
we have the following.
Lemma 2. The following are equivalent.
(1) x-input n+1-split P is n-leakage-resilient.
(2) tbl (P ) is x ∼ n, n + 1 safe.
(3) For any t such that t ←n tbl (P ), t is x ∼ 0, n + 1 safe.
Proof. It is not hard to see that (2) is equivalent to n-leakage-resilience. (2) ⇔(3) follows from Lemma 1.
Circuit Composition as Table Composition We capture circuit composition by composition of tables. More precisely, we shall define the table composition operation ⊲ m so that the composition of the tables tbl (P1 ) ⊲n+1 tbl (P2 )is the table of the composed circuit tbl ((P1 ) ⊲ P2 ).
For m > 0, let us write hd (b, m) (resp. tl (b, m)) for the first (resp. last)
m elements of b. For t1 and t2 , and m > 0 such that m ≤ #cols(t1 ) andm ≤ #cols(t2 ), we define t1 ⊲m t2 to be the #cols(t1 ) + #cols(t2 ) − m column
table such that each b ∈ {0, 1}#cols(t1 )+#cols(t2 )−m appears i1 · i2 times in thetable where i1 (resp. i2 ) is the number of times hd (b, #cols(t1 )) appears in t1(resp. tl (b, #cols(t2 )) appears in t2 ). (Therefore, b occurs as a row of t1 ⊲m t2
iff hd (b, #cols(t1 )) occurs as a row of t1 and tl (b, #cols(t2 )) occurs as a row oft2 .) For t1 and t2 such that #cols(t1 ) = #cols(t2 ) = m, we simply write t1 ⊲ t2
for t1 ⊲m t2 . Note that t1 ⊲ t2 = t2 ⊲ t1 .

It can be seen that the table composition correctly captures circuit composition. That is, for n+1-split circuits, we have tbl ((P1 )⊲P2 ) = tbl (P1 )⊲n+1 tbl (P2 ).
Also, it is immediate from the definitions that any attack on the composed table
can be simulated by an attack on the components. More formally, we have thefollowing.
Lemma 3. Let m, ℓ > 0. Then, t ←m t1 ⊲ℓ t2 iff there exist m1 , m2 , t′1 , and t′2
such that m1 + m2 = m, t′1 ←m1 t1 , t′2 ←m2 t2 , and t = t′1 ⊲ℓ t′2 .
We define the notion of deterministic tables. Roughly a table being deterministic means that split input valuations for the same non-split input leads
to the same non-split output. More formally, for m > 0 and b ∈ {0, 1}x letouts m,b (t) be the m column subtable of t comprising the last m columns ofrows i such that t[i] x,m b. We call outs m,b (t) the output table for the non-split
input b. We write nsv (t) for the 1-column #rows(t)-row table t′ such that foreach row i, t[i] 1,#cols(t) t′ [i]. We say that t is x ∼ m deterministic if for eachb ∈ {0, 1}x , the elements of nsv (outs m,b (t)) are either all 0 or all 1. Because
any n-leakage-resilient circuit with which we are concerned is IO-equivalent toa random-free circuit, without loss of generality, we may assume that the tabletbl (P1 ) (resp. tbl (P2 )) is x ∼ n + 1 (resp. 1 ∼ n + 1) deterministic.
Our goal is to show Theorem 4. That is, given n-leakage-resilient circuits P1
and P2 , the composed circuit (P1 ) ⊲ P2 is also n-leakage-resilient. By Lemmas 2,
1, and 3, it follows that it suffices to show that following.
Theorem 5. Let m1 > 0 and m2 > 0 such that m1 + m2 = n. Let t1 and t2 be
tables such that t1 is x ∼ n + 1 deterministic and x ∼ m1 , n + 1 safe, and t2 is
1 ∼ n + 1 deterministic and 1 ∼ m2 , n + 1 safe. Then, t1 ⊲n+1 t2 is x ∼ 0, n + 1
safe.
We prove the theorem in the following subsection.
Proof of Theorem 5 First, we prove a few technical lemmas. We write t1 ≃ t2
if t1 and t2 are equivalent up to permutation of the rows. The next lemma showsthat, for a table whose rows all sum up to a given value, the numbers of 1’s and
0’s in each column uniquely determine the table up to row permutation.
Lemma 4. Let v be a vector of non-negative integers of length m. Let b ∈ {0, 1}.
Let t1 and t2 be m column tables with #rows(t1 L) = #rows(t2 ) such that for eachtℓ (ℓ ∈ {1, 2}), 1.) for every row b ∈ tℓ , b =1≤i≤#cols(t) bi (i.e., every row
sums up to the same value), and 2.) for each column j ∈ {1, . . . , m}, there areexactly vj number of 1’s in the jth column of tℓ (and hence #rows(tℓ ) − vj
number of 0’s). Then, t1 ≃ t2 .
Proof. We show that b and v uniquely determines the table content (up to row
permutation) for tables whose row size and column size are fixed. We prove by
induction on the column size, m. The case m = 1 is immediate, since in this caseeither the table is all 0’s or all 1’s.

We show the inductive case. Let m > 1 and t be a table satisfying therequirements 1.) and 2.) for b and v. Let t0 (resp. t1 ) be m − 1 column subtableof t comprising the columns 2, . . . , m of t, but only taking the rows i suchthat t(i, 1) = 0 (resp. t(i, 1) = 1). For each i ∈ {2, . . . , m}, let v0i be thenumber of times 1 occurs in the i − 1st column of t0 and let v1i = vi − v0i .
Let v 0 = v02 , . . . , v0m and v 1 = v12 , . . . , v1m . Then, t0 (resp. t1 ) satisfies therequirement with b (resp. ¬b) and v 0 (resp. v 1 ). By induction hypothesis, t0 andt1 are uniquely determined, and therefore, so is t.
We use the above lemma to show the following, which says that, if a table is atleast 1 safe, then non-split inputs that map to the same non-split output value
have the same split output valuations.
Lemma 5. Let t be x ∼ m deterministic and x ∼ 1, m safe. Let b, b′ ∈ {0, 1}x .
Let t1 = outs m,b (t) and t2 = outs m,b′ (t). Then, either t1 ≃ t2 , or nsv (t1 ) andnsv (t2 ) have no common elements.
Proof. Note that, because of 1 safety, for each j ∈ {1, . . . , m}, the number of 1’s
and 0’s in the jth column of t1 must be the same as those of t2 . Suppose nsv (t1 )and nsv (t2 ) have a common element. Then, by determinism, every row of t1 andt2 sums up to a same value. Therefore, by Lemma 4, we have t1 ≃ t2 .
Next, we prove a couple of lemmas that focus on the case where the tablesconsidered are n + 1 column tables that are 1 ∼ , n + 1 safe. The first lemma,
Lemma 6, is used to prove Lemma 7. Lemma 7 is used in a part of the proof of
Theorem 5 that focuses on the output columns of tables obtained from P1 andthe input columns of the tables obtained from P2 , which will be n + 1 column
tables that are 1 ∼ , n + 1 safe.
Lemma 6. Let t be a table with #cols(t) = n + 1. Then, t is 1 ∼ n, n + 1 safe
iff 1.) t contains every element of {0, 1}n+1 as a row, and 2.) each element of{0, 1}n+1 appears the same number of times in t.
Proof. The if direction is trivial. We show the only if direction. Suppose that t
is 1 ∼ n, n + 1 safe. We show that 1.) and 2.) must be satisfied.
First, we show that 1.) is satisfied. Let b0 be a row of t. Then, any b′ thatdiffers from b0 at one entry must also appear as a row of t since otherwise theadversary can distinguish the 0-restriction and 1-restriction after observing all
n columns except for that entry. Because any b ∈ {0, 1}n+1 can be reached fromb0 via a series of one-entry changes, any such b must appear as a row of t.
Finally, note that by the same reasoning as above, for any row b of t, any b′different from b in one entry must appear the same number of times as b. Hence,2.) is also satisfied.
For a table t and j ∈ {1, . . . , #cols(t)}, we say that the column j is fixed in t if
there exists b ∈ {0, 1} such that for any i ∈ {1, . . . , #rows(t)}, t(i, j) = b (i.e.,the column is all b). Note that a table is 1 ∼ m, safe only if there are at least m
unfixed columns. For a table t and S ⊆ {1, . . . , #cols(t)}, we write t↾S for thetable comprising the columns S of t.

Lemma 7. Let m1 ≥ 0, m2 ≥ 0 and n = m1 + m2 . Let t1 and t2 be n + 1
column tables such that t1 (resp. t2 ) is 1 ∼ m1 , n + 1 safe (resp. 1 ∼ m2 , n + 1safe). Then, t1 ⊲ t2 is 1 ∼ 0, n + 1 safe.
Proof. We prove by simultaneous induction on n, m1 and m2 . The base casewhere n = 0, m1 = 0, or m2 = 0 follows from Lemma 6 because m2 = n or
m1 = n in this case.
We show the inductive case. Firstly, consider the case the fixed columns of t1
and t2 are the same. Without loss of generality, we assume that the fixed columns
have the same values in t1 and in t2 since otherwise t1 ⊲ t2 is empty and theresult is immediate. Let t′1 (resp. t′2 ) be the sub-table of t1 (resp. t2 ) comprising
the unfixed columns. Let k be the number of fixed columns. Then, t′1 (resp. t′2 )is 1 ∼ m1 − k, n − k + 1 (resp. 1 ∼ m2 − k, n − k + 1) safe (in fact, they are m1
and m2 safe). Therefore, by induction hypothesis, t′1 ⊲ t′2 is 1 ∼ 0, n − k + 1 safe.
Because t1 ⊲ t2 is t′1 ⊲ t′2 but with the k fixed columns of t1 (or t2 ) added, t1 ⊲ t2
is 1 ∼ 0, n + 1 safe.
Continuing with the inductive case, we now consider the case the fixedcolumns of t1 and t2 are not the same. Suppose that there exists a columnthat is fixed in t2 but not in t1 (the argument is similar for the case when there
is a column that is fixed in t1 but not in t2 ). Let j ∈ {1, . . . , n + 1} be fixed in t2(j,b)

but not in t1 . Let b be the entry of the jth column of t2 , and let t′1 ←−−− t1 . Let
S = {1, . . . , n + 1} \ {j}. Then, t′1 ↾S is 1 ∼ m1 − 1, n safe, and t2 ↾S is 1 ∼ m2 , nsafe. Therefore, by induction hypothesis, t′1 ↾S ⊲ t2 ↾S is 1 ∼ 0, n safe. Becauset′1 ⊲ t2 is t′1 ↾S ⊲ t2 ↾S but with an additional all b column, t′1 ⊲ t2 is 1 ∼ 0, n + 1
safe. Finally, because t1 ⊲ t2 = t′1 ⊲ t2 , the result follows.
We are now ready to prove Theorem 5, restated here.
Theorem 5. Let m1 > 0 and m2 > 0 such that m1 + m2 = n. Let t1 and t2 be
tables such that t1 is x ∼ n + 1 deterministic and x ∼ m1 , n + 1 safe, and t2 is
1 ∼ n + 1 deterministic and 1 ∼ m2 , n + 1 safe. Then, t1 ⊲n+1 t2 is x ∼ 0, n + 1
safe.
sum up to the
Proof. Let tout
be the last n + 1 columns of t1 . If all rows of tout
1
1
same value, then by Lemma 5, the result follows.
Otherwise, it means that not every row of t1 maps to the same non-split
output. Then, by Lemma 5 again, for each non-split output valuation (i.e., 0 or1), the output tables are equivalent for all inputs that maps to the same output.
Let b, b′ ∈ {0, 1}x be non-split inputs of t1 that map to different outputs. That
L is, there exist rows
L i and j of t1 with t1 [i] x,n+1 b, t1 [j] x,n+1b′ , and ( 1≤ℓ≤n+1 aℓ ) 6= ( 1≤ℓ≤n+1 a′ℓ ) where a = tl (t1 [i], n + 1) and a′ =tl (t1 [j], n + 1). Let t′1 be the table comprising the rows of outs n+1,b (t1 ) andouts n+1,b′ (t1 ). Let tin
2 be the table comprising the first n + 1 columns of t2 .
Then, for any m ≥ 0, to show t1 ⊲n+1 t2 is x ∼ m, n + 1, it suffices to show′that t′1 ⊲ tin
2 is 1 ∼ m, n + 1 safe (for arbitrary such t1 constructed from some′xb, b ∈ {0, 1} mapping to different outputs). Because t1 is x ∼ m1 , n + 1 safe, t′1

is 1 ∼ m1 , n + 1 safe. Also, because t2 is 1 ∼ m2 , n + 1 safe, tin
2 is 1 ∼ m2 , n + 1
safe. Therefore, by Lemma 7, t′1 ⊲ tin
is
1
∼
0,
n
+
1
safe,
and
the result follows.
2
Remark 6. In the definition of sequential composition, we have left unspecified
which wire of the P1 ’s split output is connected to which wire of the P2 ’s split
input. Because the table joining operation tbl (P1 ) ⊲n+1 tbl (P2 ) is insensitive
to how the rows of tbl (P1 ) and tbl (P2 ) are permuted, the proof shows that thecompositionality result holds regardless of the connection choice.
Case P2 Has Multiple Inputs We now extend the sequential compositionality
result to the case P2 has multiple inputs. In this case, we have y many circuits
P11 , P12 , . . . , P1y whose outputs will be connected to P2 , and we denote thecomposed circuit as (P11 , P12 , . . . , P1y ) ⊲ P2 . The goal is to show the following.
Theorem 3. Let P11 , . . . , P1y be n-leakage-resilient circuits, and P2 be an yinput n-leakage-resilient circuit, having disjoint randoms. Then, (P11 , . . . , P1y )⊲P2 is n-leakage-resilient.
The case follows immediately from the proof shown above for the case where P2
only has one input. This is because, for n = m1 + m2 and each P1i , Theorem 5
implies that attacking P1i m2 times and P2 m1 times and composing them cannot
distinguish the secret inputs given to P1i . Also, because of the disjointness of
the randoms in the components, attacks on P1j for j 6= i has no effect on thetable of P1i . Then, because m2 safety of P2 implies m2 safety of the portion of
tbl (P2 ) corresponding to the ith input, the result follows. We remark that theproof actually shows that the composition (P11 , . . . , P1y ) ⊲ P2 can withstand an
attack where the adversary observes m2 nodes of P2 and m1i nodes of each P1i
such that n ≥ m2 + maxi (m1i ).