Journal of Computer Security 28 (2020) 607–634
DOI 10.3233/JCS-191356
IOS Press

607

Bucketing and information flow analysis forprovable timing attack mitigation
Tachio Terauchi a,∗ and Timos Antonopoulos ba

Department of Computer Science and Engineering, Waseda University, Tokyo, Japan
E-mail: terauchi@waseda.jpbDepartment of Computer Science, Yale University, New Haven, CT, U.S.A.
E-mail: timos.antonopoulos@yale.edu
Abstract. This paper investigates the effect of bucketing in security against timing-channel attacks. Bucketing is a techniqueproposed to mitigate timing-channel attacks by restricting a system’s outputs to only occur at designated time intervals, and has
the effect of reducing the possible timing-channel observations to a small number of possibilities. However, there is little formal
analysis on when and to what degree bucketing is effective against timing-channel attacks. In this paper, we show that bucketingis in general insufficient to ensure security. Then, we present two conditions that can be used to ensure security of systems
against adaptive timing-channel attacks. The first is a general condition that ensures that the security of a system decreases
only by a limited degree by allowing timing-channel observations, whereas the second condition ensures that the system would
satisfy the first condition when bucketing is applied and hence becomes secure against timing-channel attacks. A main benefit of
the conditions is that they allow separation of concerns whereby the security of the regular channel can be proven independentlyof concerns of side-channel information leakage, and certain conditions are placed on the side channel to guarantee the securityof the whole system. Further, we show that the bucketing technique can be applied compositionally in conjunction with theconstant-time-implementation technique to increase their applicability. While we instantiate our contributions to timing channel
and bucketing, many of the results are actually quite general and are applicable to any side channels and techniques that reduce
the number of possible observations on the channel. It is interesting to note that our results make non-trivial (and somewhat
unconventional) uses of ideas from information flow research such as channel capacity and refinement order relation.
Keywords: Side-channel attacks, timing attacks, bucketing, information flow

1. Introduction
Side-channel attacks aim to recover a computer system’s secret information by observing the target
system’s side channels such as cache, power, timing and electromagnetic radiation [13,18,20,21,25,27–
29,36,46]. They are well recognized as a serious threat to the security of computer systems. Timingchannel (or simply timing) attacks are a class of side-channel attacks in which the adversary makes
observations on the system’s running time. Much research has been done to detect and prevent timing
attacks [1,3,4,6,8,11,22,24,26,30,31,35,51].
Bucketing is a technique proposed for mitigating timing attacks [8,16,30,31,51]. It restricts the system’s outputs to only occur at pre-determined and input-independent (but possibly non-periodic andsecurity-parameter-dependent) time intervals. Therefore, bucketing has the effect of reducing the possible timing-channel observations to a small number of possibilities. This is at some cost of the system’s* Corresponding author. E-mail: terauchi@waseda.jp.

0926-227X/20/$35.00 © 2020 – IOS Press and the authors. All rights reserved

608

T. Terauchi and T. Antonopoulos / Bucketing for timing attack mitigation

performance because outputs must be delayed to the next bucket time. Nonetheless, in comparison to theconstant-time implementation technique [1,3,6,11,24,26] which restricts the system’s running time to be
independent of secrets, bucketing is often said to be more efficient and easier to implement as it allows
running times to vary depending on secrets [30,31].1 For example, bucketing may be implemented in a
blackbox-style by a monitor that buffers and delays outputs [8,51]. On the other hand, while it is clearthat constant-time implementation entirely removes information leaks from timing channels, bucketing
only mitigates the leaks and the precise degree of security achieved by the mitigation has been little
understood. A main motivation of the paper is to clarify the degree of security achieved by bucketing.
In this paper, we formally study the effect of bucketing on security against adaptive timing attacks. To
this end, first, we review a formal notion of security against adaptive side-channel-observing adversaries,
called (f, )-security, which was introduced in our previous work [7,43] inspired by a closely related
notion from the DARPA STAC program [17]. Roughly, (f, )-security says that the probability that anadversary can recover the secret by making at most f (n) many queries to the system is bounded by (n),where n is the security parameter.
Next, we show that bucketing alone is in general insufficient to guarantee security against adaptiveside-channel attacks by presenting a counterexample that has only two timing observations and yet
is efficiently attackable. This motivates a search for conditions sufficient for security. We present a
condition, called secret-restricted side-channel refinement (SRSCR), which roughly says that a system
is secure if there are sufficiently large disjoint subsets of secrets such that, when the space of possible
secrets is restricted to each subset, (1) the system’s side channel reveals no more information than theregular channel and (2) the system is secure against adversaries who only observe the regular channel.
The degree of security (i.e., f and ) is proportional to those against regular-channel-only-observing
adversaries for the restricted subset of secrets and the sizes of the subsets.
Because of the insufficiency of bucketing mentioned above, applying bucketing to an arbitrary system
may not lead to a system that satisfies SRSCR (for good f and ). To this end, we present a condition, called bounded low-input side-channel capacity (BLISCC). We show that applying bucketing to asystem that satisfies the condition would result in a system that satisfies SRSCR. Therefore, BLISCC
is a sufficient condition for security under the bucketing technique. Roughly, BLISCC says that (1) the
attacker-controlled inputs only have some bounded influence on the side channel (while secrets are allowed to influence the side channel arbitrarily), and (2) the system is secure against adversaries who
only observe the regular channel. The degree of security is proportional to that against regular-channelonly-observing adversaries, the degree of attacker-controlled-input influence on the side channel, andthe granularity of buckets. A main benefit of the conditions SRSCR and BLISCC is that they allow separation of concerns whereby the security of the regular channel can be proven independently of concernsof side-channel information leakage, and certain conditions are placed on the side channel to guarantee
the security of the whole system.
Finally, we show that the bucketing technique can be applied in a compositional manner with theconstant-time implementation technique. Specifically, we show that when a system is a sequential composition of components in which one component is constant-time and the other component is BLISCC,
the whole system can be made secure by applying bucketing only to the non-constant-time part. We showthat the combined approach is able to ensure security of some non-constant-time systems that cannot bemade secure by applying bucketing to the whole system. We summarize the main contributions below.
1 Sometimes, the terminology “constant-time implementation” is used to mean even stricter requirements, such as requiringcontrol flows to be secret independent [3,11]. In this paper, we use the terminology for a more permissive notion in which only
the running time is required to be secret independent.

T. Terauchi and T. Antonopoulos / Bucketing for timing attack mitigation609• A counterexample which shows that bucketing alone is insufficient for security against adaptiveside-channel attacks (Section 2.1).
• A condition SRSCR which guarantees (f, )-security (Section 3.1).
• A condition BLISCC which guarantees that the system satisfying it becomes one that satisfies
SRSCR and therefore becomes (f, )-secure after suitable bucketing is applied (Section 3.2).
• A compositional approach that combines bucketing and the constant-time technique (Section 3.3).
As remarked before, these results are given in terms of a formal notion of security called (f, )-security
that we will review in Section 2.
While the paper focuses on timing channels and bucketing, many of the results are actually quite
general and are applicable to side channels other than timing channels. Specifically, aside from thecompositional bucketing result that exploits the “additive” nature of timing channels (cf. Section 3.3),
the results are applicable to any side channels and techniques that reduce the number of possible sidechannel observations.
Our results make use of ideas from (quantitative) information flow research such as refinement orderrelation [33,34,38,48] and channel capacity [5,9,32,39,48,49]. It is interesting to note that we use theideas somewhat unconventionally. Rather than using them directly to, for example, derive the degree of
security in terms of information theoretic measures such as Shannon entropy, we use them indirectly, forexample, to bound the degree of influence that attacker-controlled inputs have on side-channel outputs.
We show that, combined with certain additional conditions and program transformations, this allows us
to derive the security of the final system.
The rest of the paper is organized as follows. Section 2 formalizes the setting, and defines (f, )security which is a formal notion of security against adaptive side-channel attacks. We also show thatbucketing is in general insufficient to guarantee security of systems against adaptive side-channel attacks.
Section 3 presents sufficient conditions for ensuring (f, )-security: SRSCR and BLISCC. We show thatthey facilitate proving the security of systems by allowing system designers to prove the security of
regular channels separately from the concern of side channels. We also show that the BLISCC condition
may be used in combination with the constant-time implementation technique in a compositional mannerso as to prove the security of systems that are neither constant-time nor can be made secure by (globally)
applying bucketing. Section 4 discusses related work. Section 5 concludes the paper with a discussion
on future work.
A preliminary version of this paper appeared in [43]. The present paper substantially improves thatversion by extending the key results. Namely, the conditions SRSCR and LISCNI and their compositional
application have been substantially extended. The extensions allow derivation of much better security
bounds. Accordingly, the theorems stating the derivable security bounds and the proofs of the theorems
have also been renovated. We list the main changes below:(1) SRSCR is extended to allow different secret subsets to be assigned different regular-channel adversary error probability bounds. The extension allows the derivation of much better security
bounds. SRSCR in [43] is a restricted case of the new one where the same bound was assigned toevery subset. We also correct a bug in [43] that allowed non-disjoint secret subsets (Definition 3.3,
Lemma 3.2 and Theorem 3.4 in Section 3.1).
(2) The condition called low-input side-channel non-interference (LISCNI) in [43] is extended to what
we now call bounded low-input side-channel capacity (BLISCC) condition. BLISCC is a generalization of LISCNI in that the latter is a special case of the former where the capacity bound isrestricted to 1 (Definition 3.8 in Section 3.2).

610

T. Terauchi and T. Antonopoulos / Bucketing for timing attack mitigation(3) The extensions (1) and (2) together improve the BLISCC (LISCNI in [43]) soundness theorem andthe compositionality theorem to allow derivation of tighter security bounds (Lemma 3.10, Theorem 3.11 and Corollary 3.12 in Section 3.2, and Theorem 3.21 and Corollary 3.22 in Section 3.3).
(4) An additional example demonstrating the usefulness of the BLISCC condition is added (Example 3.14).
(5) An extended analysis of the leaky login program is added. The analysis shows a limitation withthe permissive definition of bucketing that is used in this paper (and in [43]) (Example 3.15 inSection 3.2).
In summary, the main technical contributions given in Sections 3.1, 3.2 and 3.3 (same section numbers
are used in [43]) have all been substantially extended to allow improved security analysis. Also, as a side
effect of the extended results, we were able to “fix” the bugs in the examples of [43] where we claimed
security bounds that cannot be derived by the results in that version (the authors’ online copy of [43]corrects the bug by stating weaker bounds [44]). The extensions in this submission allow the derivationof the strong bounds.
2. Security against adaptive side-channel attacks
Formally, a system (or, program) is a tuple (rc, sc, S , I , Orc , Osc ) where rc and sc are indexed families
of functions (indexed by the security parameter) that represent the regular-channel and side-channel
input-output relation of the system, respectively. Furthermore, S is a security-parameter-indexed familyof sets of secrets (or, high inputs) and I is a security-parameter-indexed family of sets of attackercontrolled inputs (or, low inputs). A security parameter is a natural number that represents the size of
secrets, and we write Sn for the set of secrets of size n and In for the set of corresponding attackercontrolled inputs. We assume that each Sn and In are finite. Each indexed function rcn (respectively
scn ) is a function from Sn × In to Onrc (resp. Onsc ), where O rc and O sc are indexed families of sets ofpossible regular-channel and side-channel outputs, respectively. For (s, v) ∈ Sn × In , we write rcn (s, v)(resp. scn (s, v)) for the regular-channel (resp. side-channel) output given the secret s and the attackercontrolled input v.2 For a system C = (rc, sc, S , I , Orc , Osc ), we often write rcC for rc, scC for sc,
S C for S , I C for I , Orc C for Orc , and Osc C for Osc . We often omit the parameter C when it isclear from the context.
For a system C and s ∈ Sn , we write Cn (s) for the oracle which, given v ∈ In , returns a pair of outputs(o1 , o2 ) ∈ Onrc × Onsc such that rcn (s, v) = o1 and scn (s, v) = o2 . An adversary A is an algorithm that
attempts to discover the secret by making some number of oracle queries. As standard, we assume that
A has the full knowledge of the system. For i ∈ N, we write ACn (s) (i) for the adversary A that makes atmost i oracle queries to Cn (s). We impose no restriction on how the adversary chooses the inputs to theoracle. Importantly, he may choose the inputs based on the outputs of previous oracle queries. Such an
adversary is said to be adaptive [29].
Also, for generality, we intentionally leave the computation class of adversaries unspecified. The methods presented in this paper work for any computation class, including the class of polynomial time
randomized algorithms and the class of resource-unlimited randomized algorithms. The former is thestandard for arguing the security of cryptography algorithms, and the latter ensures information theoretic security. In what follows, unless specified otherwise, we assume that the computation class ofadversaries is the class of resource-unlimited randomized algorithms.
2 We restrict to deterministic systems in this paper. Extension to probabilistic systems is left for future work.

T. Terauchi and T. Antonopoulos / Bucketing for timing attack mitigation

611

As standard, we define security as the bound on the probability that an adversary wins a certain game.
Let f be a function from N to N. We define WinCA (n, f ) to be the event that the following game outputstrue.
s ← Sns  ← ACn (s) (f (n))
Output s = s Here, the first line selects s uniformly at random from Sn . We note that, while we restrict to deterministic
systems, the adversary algorithm A may be probabilistic and also the secret s is selected randomly.
Therefore, the full range of probabilities is possible for the event WinCA (n, f ). Now, we are ready to givethe definition of (f, )-security.
Definition 2.1 ((f, )-security). Let f : N → N and  : N → R be such that 0 < (n)  1 for alln ∈ N. We say that a system C is (f, )-secure if there exists N ∈ N such that for all adversaries A andn  N, it holds that Pr[WinCA (n, f )] < (n).
Roughly, (f, )-secure means that, for all sufficiently large n, there is no attack that is able to recover secrets in f (n) number of queries with the probability of success (n), assuming that the secrets are uniformly distributed. It should be noted that this definition of security is also used in ourprevious works [7,43] and it also corresponds closely to the definition used in the DARPA STAC program [17].3
By abuse of notation, we often implicitly treat an expression e on the security parameter n as thefunction λn ∈ N.e. Therefore, for example, (n, )-secure means that there is no attack that is able torecover secrets in n many queries with the probability of success (n), and (f, 1)-secure means that
there is no attack that makes at most f (n) number of queries and is always successful. Also, by abuseof notation, we often write     when (n)    (n) for all sufficiently large n, and likewise for < .
Example 2.2 (Leaky login). Consider the program shown in Fig. 1 written in a C-like language. The
program is an abridged version of the timing insecure login program from [6]. Here, pass is the secretand guess is the attacker-controlled input, each represented as a length n bit array. We show that there
is an efficient adaptive timing attack against the program that recovers the secret in a linear number ofqueries.
i = 0;
while (i < n) {if (pass[i] != guess[i]) return false;i++;}return true;
Fig. 1. Timing insecure login program.
3 A slight difference is that the definition in [7] is not asymptotic, i.e., it asserts Pr[WinC (n, f )] for all n. The relaxed definitionA

in this paper facilitates derivations of asymptotic bounds.

612

T. Terauchi and T. Antonopoulos / Bucketing for timing attack mitigation

We formalize the program as the system C where for all n ∈ N,
• Sn = In = {0, 1}n ;• Onrc = {true, false} and Onsc = {i ∈ N | i  n};• For all (s, v) ∈ Sn × In , rcn (s, v) = true if s = v and rcn (s, v) = false if s = v; and• For all (s, v) ∈ Sn × In , scn (s, v) = argmaxi si = vi .
Here, ai denotes the length i prefix of a. Note that sc expresses the timing-channel observation, as its
output corresponds to the number of times the loop iterated.
For a secret s ∈ Sn , the adversary ACn (s) (n) efficiently recovers s as follows. He picks an arbitraryv1 ∈ In as the initial guess. By seeing the timing-channel output scn (s, v1 ), he would be able to discoverat least the first bit of s, s[0], because s[0] = v1 [0] if and only if scn (s, v1 ) > 0. Then, he picks anarbitrary v2 ∈ {0, 1}n satisfying v2 [0] = s[0], and by seeing the timing-channel output, he would be able
to discover at least up to the second bit of s. Repeating the process n times, he will recover all n bitsof s. Therefore, the system is not (n, )-secure for any . This is an example of an adaptive attack since
the adversary crafts the next input by using the knowledge of previous observations.
Example 2.3 (Bucketed leaky login). Next, we consider the security of the program from Example 2.2
but with bucketing applied. Here, we assume a constant number of buckets, k, such that the program
returns its output at time intervals i · n/k for natural i  k.4 For simplicity, we assume that n is divisible
by k. The bucketed program can be formalized as the system where• rc, sc, I , Orc are as in Example 2.2;
• For all n ∈ N, Onsc = {i ∈ N | i  k}; and• For all n ∈ N and (s, v) ∈ Sn × In , scn (s, v) = bkt(argmaxi si = vi , n/k)
where bkt(i, j ) is the smallest a ∈ N such that i  a · j . It is easy to see that the system is not constanttime for any k > 1. Nonetheless, with the analysis method that we will present in Section 3.1, we can−1show that the system is (f, )-secure where f (n) = 2n/k − (N + 1) and (n) = 1 − N2n/k
for anyn/k
1  N < 2 (cf. Example 3.5). Note that as k approaches 1 (and hence the system becomes constanttime), f approaches 2n − (N + 1) and  approaches 1 − N2−1
n , which match the security bound of theideal login program that only leaks whether the input guess matched the password or not.5
Remark 2.4 (Parameter correlation in (f, )-security). Note that in Example 2.3, the parameters f and in (f, )-security are correlated. For instance, when  is maximized (i.e., letting  = 1 by letting N = 1),
the corresponding f is also maximized to be 2n/k − 2. Typically, a larger  implies a larger f and viceversa. Such a correlation is expected as requiring the attacker to succeed with a higher probability bymaking  larger means that the attacker has to work harder by making more queries which implies
enlarging f .
As we shall see later in the paper, the main results of the paper (cf. Theorem 3.4, Theorem 3.11,
Corollary 3.12 and Theorem 3.21) show, given a system with or without bucketing, how to transfer the
regular-channel security of the system in which the adversary only observes the regular channel (cf.
Section 3.1) to that for the case when the adversary observes both the regular and the side channel.
Some amount of security is lost in the transfer and each theorem stipulates how much security is lost
4 A similar analysis can be done for any strictly sub-linear number of buckets.
5 Roughly, the bound for the ideal login program follows from the fact that the probability of guessing an element in a set ofsize M in X tries is X/M + (1 − X/M)(1/(M − X)) and letting X = 2n − N and M = 2n . We refer to [7] for a method forformally deriving such a bound.

T. Terauchi and T. Antonopoulos / Bucketing for timing attack mitigation

613

in terms of the change in the f and  parameters. As we shall show, the statements of the theorems saythat only the  parameter is affected, possibly giving a false impression that bucketing only affects theprobability of the attack success. However, due to the parameter correlation, the results actually imply
that the change in the  parameter may need to be compensated by a change in the f parameter, that is,
the transfer also affects the number of queries the adversary needs to make to recover the secret.
2.1. Insufficiency of bucketing
We show that bucketing is in general insufficient to guarantee the security of systems against adaptiveside-channel attacks. In fact, we show that bucketing with even just two buckets is insufficient (two is theminimum number of buckets that can be used to show the insufficiency because having only one bucket
implies that the system is constant-time and therefore is secure). More generally, our result applies toany side channels, and it shows that there are systems with just two possible side-channel outputs andcompletely secure (i.e., non-interferent [23,47]) regular channel that is efficiently attackable by sidechannel-observing adversaries.
Consider the system such that, for all n ∈ N,
• Sn = {0, 1}n and In = {i ∈ N | i  n};• Onrc = {•} and Onsc = {0, 1};• For all (s, v) ∈ Sn × In , rcn (s, v) = •; and• For all (s, v) ∈ Sn × In , scn (s, v) = s[v].
Note that the regular channel rc only has one possible output and therefore is non-interferent. The sidechannel sc has just two possible outputs. The side channel, given an attacker-controlled input v ∈ In ,reveals the v-th bit of s. It is easy to see that the system is linearly attackable. That is, for any secrets ∈ Sn , the adversary may recover the entire n bits of s by querying with each of the n-many possible
attacker-controlled inputs. Therefore, the system is not (n, )-secure for any . Note that the side channel
is easily realizable as a timing channel, for example, by having a branch with the branch condition“s[v] = 0” and different running times for the branches as shown in the program below.
if (s[v] == 0) {sleep(100);}
return true;
We remark that the above attack is efficient. That is, the attacker recovers the secret with a highprobability with only a small amount of queries. This is in contrast to the bucketed leaky login programfrom Example 2.3 which, while still leaking information through the side channel, is secure in the sensethat any attack that recovers the secret with a high probability must make an exponential number ofqueries. Secondly, we remark that leaking information does not mean that attacker can always recover
the secret with a high probability, even with an unlimited number of queries. For instance, if a line v = 0;
is added at the beginning of the program above, the attacker would have little chance of recovering
the secret with any number of queries, even though the program still leaks information for any query(namely, the first bit of s). Finally, we remark that the above attack is not adaptive. Therefore, thecounterexample actually shows that bucketing can be made ineffective by just allowing multiple nonadaptive side-channel observations.

614

T. Terauchi and T. Antonopoulos / Bucketing for timing attack mitigation

3. Sufficient conditions for security against adaptive side-channel attacks
In this section, we present conditions that guarantee the security of systems against adaptive sidechannel-observing adversaries. The condition SRSCR presented in Section 3.1 guarantees that systems
that satisfy it are secure, whereas the condition BLISCC presented in Section 3.2 guarantees that systems
that satisfy it become secure once bucketing is applied. We shall show that the conditions facilitate
proving (f, )-security of systems by separating the concerns of regular channels from those of sidechannels. In addition, we show in Section 3.3 that the BLISCC condition may be used in combination
with constant-time implementation techniques in a compositional manner so as to prove the security ofsystems that are neither constant-time nor can be made secure by (globally) applying bucketing.
3.1. Secret-restricted side-channel refinement condition
We present the secret-restricted side-channel refinement condition (SRSCR). Informally, the idea here
is to find large disjoint subsets of secrets S  ⊆ P (Sn ) such that for each S  ∈ S  , the secrets are difficult
for an adversary to recover by just observing the regular channel, and that the side channel reveals no
more information than the regular channel for those sets of secrets. Then, because each S  is large, theentire system is also ensured to be secure with high probability. We adopt refinement order relation[33,34,38,48], which had been studied in quantitative information flow (QIF) research, to formalize
the notion of “reveals no more information”. Roughly, a channel c1 is said to be a refinement of achannel c2 if, for every attacker-controlled input, every pair of secrets that c2 can distinguish can also be
distinguished by c1 .
We begin by introducing preliminary notions that we shall use to state the SRSCR condition.
Regular-channel security. We write O• for the indexed family of sets such that On• = {•} for alln ∈ N. Also, we write sc• for the indexed family of functions such that sc•n (s, v) = • for all n ∈ N and(s, v) ∈ Sn ×In . For C = (rc, sc, S , I , Orc , Osc ), we write C • for the system (rc, sc• , S , I , Orc , O• ). We
say that the system C is regular-channel (f, )-secure if C • is (f, )-secure. Roughly, regular-channel
security says that the system is secure against attacks that only observe the regular channel output.
Secret restriction. Let us write (0, 1] for the set {a ∈ R | 0 < a  1}. Let us fix a system C =(rc, sc, S , I , Orc , Osc ). We call X a secret restriction of S when (1) X is an indexed family such thatXn ⊆ P (Sn ) × (0, 1] for each n ∈ N and (2) for each n ∈ N, (S1 , p1 ) ∈ Xn and (S2 , p2 ) ∈ Xn ,(S1 , p1 ) = (S2 , p2 ) implies S1 ∩ S2 = ∅. Let us write #1 (S, p) for S and #2 (S, p) for p. For a secret
restriction X, we write U ≺ X when U is an indexed family such that Un ∈ Xn for each n. Note that such
U satisfies Un ∈ P (Sn ) × (0, 1] for each n. For an indexed family of sets of secrets T such that Tn ⊆ Sn
for each n ∈ N, we write C|T for the system (rc, sc, T , I , Orc , Osc ). We write C|U for C|#1 U , and write
errU for the function from N to (0, 1] such that errU (n) = (#2 U )n for each n. Here, (#1 U )n = #1 (Un )and (#2 U )n = #2 (Un ) for each n. Roughly, errU is the error bound function stipulated by U .
Refinement order relation. Let us fix a system C = (rc, sc, S , I , Orc , Osc ). Let T be an indexed familyof sets of secrets such that Tn ⊆ Sn for each n ∈ N. We say that C satisfies the side-channel refinement
order relation condition on the secrets T , written RR(T ), if for all n ∈ N, s1 ∈ Tn , s2 ∈ Tn and v ∈ In ,it holds that scn (s1 , v) = scn (s2 , v) ⇒ rcn (s1 , v) = rcn (s2 , v). Roughly, RR(T ) says that the system’sside channel reveals no more information than its regular-channel on the secrets T . We formalize theintuition in Lemma 3.2.

T. Terauchi and T. Antonopoulos / Bucketing for timing attack mitigation

615

Lemma 3.1. Let T be an indexed family of sets of secrets such that Tn ⊆ Sn for each n ∈ N. Supposethat C satisfies RR(T ). Then, for any n ∈ N, orc ∈ Onrc and v ∈ In , there exists osc ∈ Onsc such that forany s ∈ Tn , rcn (s, v) = orc ⇒ scn (s, v) = osc .
Proof. Let orc ∈ Onrc , v ∈ In and s ∈ Tn be such that rcn (s, v) = orc . Let osc = scn (s, v). Then, by
RR(T ), for any s  ∈ Tn such that rcn (s  , v) = orc , we have scn (s  , v) = osc . Lemma 3.2. Let T be an indexed family of sets of secrets such that Tn ⊆ Sn for each n ∈ N. Supposethat C satisfies RR(T ) and C|T is regular-channel (f, )-secure. Then, C|T is (f, )-secure.
Proof. Suppose for contradiction that C|T is not (f, )-secure. Then, there exists A such thatT
WinC|
many n ∈ N. We prove the lemma by constructing a (regular-channel)
A (n, f ) > (n) for infinitely
C|•T
adversary A such that Pr[WinA (n, f )] > (n) for infinitely many n ∈ N.
We construct such A by letting it simulate A. Fix n ∈ N. By RR(T ) and Lemma 3.1, for any orc ∈ Onrc
and v ∈ In , there exists osc ∈ Onsc such that for any s ∈ Tn , rcn (s, v) = orc ⇒ scn (s, v) = osc . Let
corn : Onrc × In → Onsc be the mapping where corn (orc , v) is such osc , for each orc ∈ Onrc and v ∈ In .
Then, A works by running A but hijacking its process whenever it makes a query to the system. Thatis, whenever A attempts to query the system with an input v ∈ In , A sends the query to the regularchannel-only system to obtain the regular-channel output orc = rc(s, v) and communicates back to A
the regular-and-side-channel output (orc , corn (orc , v)). It is easy to see that A and A behave in exactlyC|•
the same manner on secrets from Tn . Therefore, Pr WinAT (n, f )] > (n) for infinitely many n ∈ N. 
We are now ready to formally state the SRSCR condition.
Definition 3.3 (SRSCR). Let C = (rc, sc, S , I , Orc , Osc ). Let f : N → N and X be a secret restrictionof S . We say that C satisfies the secret-restricted side-channel refinement condition with f and X written
SRSCR(f, X), if the following condition holds(1) For all U ≺ X, C|U is regular-channel (f, errU )-secure; and(2) For all U ≺ X, RR(#1 U ) holds.6
We informally describe why SRSCR is a sufficient condition for security. Let (S, p) ∈ Xn . The condition (2) guarantees that an attacker gains no additional information by observing the side-channel
compared to what he already knew by observing the regular-channel to distinguish secrets in S. As
seen in Lemma 3.2, this implies that regular-channel security transfers to the side-channel aware casewhen the secrets are restricted to S. And, the condition (1) says that the regular-channel attack succeeds with the probability at most p (technically, the condition only stipulates that this holds for all
but finitely many n’s; for simplicity, we assume the stronger non-asymptotic condition in this informal discussion). Therefore, the probability that a secret is selected from S and that the attack fails torecover the secret is bounded below by |S|S|n | (1 − p). Then, since the secret subsets in Xn are disjoint
S2 = ∅ for any (S1 , p1 ) ∈ Xn and (S2 , p2 ) ∈ Xn ), the attack(i.e., (S1 , p1 ) = (S2 , p2 ) implies S1 ∩must fail with the probability at least (S,p)∈Xn |S|S|n | (1 − p). The theorem below formalizes the intuition.
6 It is easy to relax the condition to also be asymptotic so that the refinement order relation only needs to hold for large n.

616

T. Terauchi and T. Antonopoulos / Bucketing for timing attack mitigation

Theorem 3.4 (SRSCR soundness). Suppose C satisfies SRSCR(f, X). Then, C is (f, )-secure where : N → (0, 1] is any function satisfying the condition below:
(♠) There exists N ∈ N such that for all n  N, 1 − (S,p)∈Xn |S|S|n | (1 − p)  (n).
Proof. Suppose for contradiction that C is not (f, )-secure for  satisfying ♠. That is, there exists
an adversary A such that Pr[WinCA (n, f )]  (n) for infinitely many n ∈ N. To prove the theorem, itC|•suffices to construct an adversary A and U ≺ X such that Pr[WinAU (n, f )]  errU (n) for infinitely
many n ∈ N because that would contradict the condition (1) of SRSCR(f, X).
We now show the construction of A and U (A turns out to be simply A). Because of the condition(2) of SRSCR(f, X) and Lemma 3.2, it suffices to allow such an adversary A to also make side-channelUobservations. That is, it suffices to construct A and U such that Pr[WinC|
A (n, f )]  err U (n) for in
finitely many n ∈ N. By condition (♠), there exists N ∈ N such that 1 − (S,p)∈Xn |S|S|n | (1 − p)  (n)for all n  N (♦). Let Y = {n ∈ N | n  N ∧ Pr[WinCA (n, f )]  (n)}. Note that Y is an infinite set.
S
Fix n ∈ Y . For S ⊆ Sn , let us write WinC|· (n, ·) for the winning event of the modified game in which thespace of secrets (of size n) is S. Note that, given S ⊆ Sn , the probability that a secret randomly selectedfrom Sn belongs to S is |S|/|Sn |, that is, Pr[s ∈ S | s ← Sn ] = |S|/|Sn |. Therefore, by disjointness ofthe secret subsets in Xn , it follows that






S
Pr WinCA (n, f )  1 −Pr[s ∈ S | s ← Sn ] · 1 − Pr WinC|
A (n, f )(S,_)∈Xn

=1−





|S| 
S
· 1 − Pr WinC|
A (n, f ) .
|Sn |(S,_)∈Xn

Then, because Pr[WinCA (n, f )]  (n), from (♦) above, we have that1−

 |S| 




|S|
S
(1 − p)  (n)  Pr WinCA (n, f )  1 −· 1 − Pr WinC|
A (n, f ) ,
|Sn |
|Sn |
(S,p)∈X(S,_)∈Xnn

and thus
 |S| |S|S
(1 − p) · 1 − Pr WinC|
A (n, f ) .
|Sn |
|Sn |
(S,p)∈X(S,_)∈X


n

n

C 

Therefore there must be (S  , p ) ∈ Xn such that p  Pr[WinAS (n, f )]. Denote by Snres any such S  , foreach n ∈ Y . Let U ≺ X be such that #1 Un = Snres for each n ∈ Y (Un is allowed to be an arbitraryU/ Y ), and let A = A. Then, it follows that Pr[WinC|
element of Xn for n ∈A (n, f )]  err U (n) for eachn ∈ Y. 
We remark about a restricted case of the SRSCR soundness theorem. Let X be a secret restriction
and suppose that there exist  : N → (0, 1] and r ∈ (0, 1] satisfying the following: for all n ∈ N,|S|n
 r. Then, Theorem 3.4 implies that a system satisfying
p = (n) for all (_, p) ∈ Xn and (S,_)∈X|Sn |SRSCR(f, X) is (f, 1 − r(1 − )) secure. The restricted case corresponds to the version of the theorem presented in [43] (with the disjointness bug corrected). Theorem 3.4 of this paper is more general

T. Terauchi and T. Antonopoulos / Bucketing for timing attack mitigation

617

because the improved SRSCR condition allows assignments of different error bounds to different secretsubsets, stipulated by the secret restriction parameter X. Importantly, as we shall show in the next sections, the more general result allows derivations of substantially tighter security bounds (cf. Corollaries
3.12 and 3.22).
Example 3.5. Recall the bucketed leaky login program from Example 2.3. We show that the programsatisfies the SRSCR condition. For each n ∈ N, a ∈ {0, 1}n−n/k , and 0  i < k, let Sna,i ⊆ Sn be the setof secrets whose sub-bits from i · n/k to (i + 1) · n/k − 1 may differ but the remaining n − n/k bits are
as in a (and therefore same). That is,
Sna,i = s ∈ Sn | s[0, . . . , i · n/k − 1] = a[0, . . . , i · n/k − 1]and s (i + 1) · n/k, . . . , n − 1 = a[i · n/k, . . . , n − n/k − 1] ,where s[m, . . . , m ] and a[m, . . . , m ], for m > m , are arrays with no elements and in which cases[m, . . . , m ] = a[m, . . . , m ]. Fix some i ∈ {0, . . . , k − 1} and N ∈ {1, . . . , 2n/k − 1}. Recall  :−1
N → (0, 1] such that (n) = 1 − N2n/kfrom Example 2.3. Let X be an indexed family such that
a,i
n−n/k
} for each n ∈ N. Note that X is a secret restriction for the system
Xn = {(Sn , (n)) | a ∈ {0, 1}
because Sna,i ∩ Sna ,i = ∅ for any a = a  . Also, S∈Xn S = Sn for each n.
Recall f such that f (n) = 2n/k − (N + 1) from Example 2.3. We argue that the system satisfies
SRSCR(f, X). We note that condition (1) is satisfied because |Sna,i | = 2n/k and (f, ) matches the
security of the ideal login program without side channels for the set of secrets of size 2n/k .7 To see why
condition (2) is satisfied, note that for any v ∈ In and s ∈ Sna,i , scn (s, v) = i if s = v, and scn (s, v) = k
if s = v. Hence, for any v ∈ In and s1 , s2 ∈ Sna,i , scn (s1 , v) = scn (s2 , v) ⇒ rcn (s1 , v) = rcn (s2 , v).
Therefore, by Theorem 3.4, it follows that bucketed leaky login program is (f, )-secure. Note that thebound matches the one given in Example 2.3.
To effectively apply Theorem 3.4, one needs to find a suitable secret restriction X on which the system’s regular channel is secure and the side channel satisfies the refinement order relation with respect
to the regular channel. As also observed in a prior work [48], the refinement order relation is a 2-safety
property [15,42] for which there are a number of effective verification methods [2,6,12,37,40]. For instance, self-composition [3,4,10,19,42] is a well-known technique that can be used to verify arbitrary
2-safety properties.
We note that a main benefit of Theorem 3.4 is separation of concerns whereby the security of regularchannel can be proven independently of side channels, and the conditions required for side channels canbe checked separately. For instance, a system designer may prove the regular-channel (f, )-security byan elaborate manual reasoning (e.g., by following the method proposed in [7]), while the side-channel
conditions are checked, possibly automatically, by established program verification methods such as self
composition.
Remark 3.6. We make some additional observations regarding the SRSCR condition. First, while Theorem 3.4 derives a sound security bound, the bound may not be the tightest one. Indeed, when theadversary’s error probability (i.e., the “” part of (f, )-security) is 1, the bucketed leaky login program
can be shown to be actually (k(2n/k − 2), 1)-secure, whereas the bound derived in Example 3.5 only
showed that it is (2n/k − 2, 1)-secure. That is, there is a factor k gap in the bounds. Intuitively, the gap
7 The latter follows by an argument similar to the one given in footnote 5 in Example 2.3.

618

T. Terauchi and T. Antonopoulos / Bucketing for timing attack mitigation

occurs for the example because the buckets partition a secret into k number of n/k bit blocks, and while
an adversary needs to recover the bits of every block in order to recover the entire secret, the analysis
derived the bound by assessing only the effort required to recover bits from one of the blocks (i.e., we
fixed an arbitrary i ∈ {0, . . . , k − 1} to construct the restriction X). Extending the technique to enabletighter analyses is left for future work.
Secondly, Theorem 3.4 says that, given a secret restriction X, if the regular channel of the system is(f, errU )-secure when the secrets are restricted to the indexed family of subsets of secrets #1 U for eachU ≺ X, then the whole system is (f, )-secure under certain conditions for some  determined by theparameter X. This may give an impression that only the adversary-success probability parameter (i.e.,) of (f, )-security is affected by the additional consideration of side channels, leaving the number oforacle queries parameter (i.e., f ) unaffected. However, as also remarked in Remark 2.4, the two parameters are often correlated so that smaller f implies smaller  and vice versa. Therefore, Theorem 3.4
suggests that the change in the probability parameter (i.e., from errU to ) may need to be compensatedby a change in the degree of security with respect to the number of oracle queries.
Finally, condition (1) of SRSCR stipulates that the regular channel is (f, errU )-secure for each restricted indexed family of subsets of secrets #1 U rather than the entire space of secrets S . In general, asystem can be less secure when secrets are restricted because the adversary has a smaller space of secrets
to search. Indeed, in the case when the error probability is 1, the regular channel of the bucketed leaky
login program can be shown to be (2n − 2, 1)-secure, but when restricted to each U ≺ X used in theanalysis of Example 3.5, it is only (2n/k − 2, 1)-secure. That is, there is an implicit correlation between
the sizes of the restricted subsets and the degree of regular-channel security. Therefore, finding X suchthat each U ∈ X is large
 and satisfies the conditions is important for deriving good security bounds,
even when the ratio | S∈Xn S|/|Sn | is large as in the analysis of the bucketed leaky login program.
3.2. Bounded low-input side-channel capacity condition
While SRSCR facilitates proving security of systems by separating regular channels from side channels, it requires one to identify a suitable secret restriction that satisfies the conditions. This can be a
hurdle to applying the proof method. To this end, this section presents a condition, called bounded lowinput side-channel capacity (BLISCC), which guarantees that a system satisfying it becomes secure after
applying bucketing (or other techniques) to reduce the number of side-channel outputs. Unlike SRSCR,
the condition does not require identifying restricted secret subsets. Roughly, the condition stipulates thatthe regular channel is secure (for the entire space of secrets) and that the side-channel outputs dependon attacker-controlled inputs only in a bounded way. As we shall show, the degree of dependency that
we will use is related to channel capacity, a notion studied in QIF research [5,9,32,39,48,49], whichmeasures the number of possible observations one can make on the channel.
We show that the system satisfying BLISCC becomes a system satisfying SRSCR once bucketing isapplied, where the degree of security (i.e., the parameters f and X of SRSCR) will be proportional to thedegree of regular-channel security, capacity bound and the granularity of buckets. Roughly, this holds
because for a system whose side-channel capacity relative to attacker-controlled inputs is bounded, bucketing is guaranteed to partition the secrets into a small number of sets (relative to the bucket granularity
and the capacity bound) such that for each of the sets, the side channel cannot distinguish the secrets
in the set, and the regular-channel security transfers to a certain degree to the case when the secrets are
restricted to the ones in the set.

T. Terauchi and T. Antonopoulos / Bucketing for timing attack mitigation

619

As we shall show next, while the condition is not permissive enough to prove security of the leaky
login program (cf. Examples 2.2, 2.3 and 3.5), it covers interesting scenarios such as fast modular exponentiation (cf. Example 3.13). Also, as we shall show in Section 3.3, the condition may be usedcompositionally in combination with the constant-time implementation technique [1,3,11,26] to further
widen its applicability.
For a set A and an equivalence relation ∼ ⊆ A × A, we write A/∼ for the set of equivalence classes of
A. That is, A/∼ = {[a]∼ | a ∈ A} where [a]∼ = {x ∈ A | x ∼ a}. For a system C and n ∈ N, we say thatv1 ∈ In and v2 ∈ In are low-input side-channel equivalent, written v1 ∼lisc
n v2 , if scn (s, v1 ) = scn (s, v2 )for all s ∈ Sn . It is easy to see that ∼liscisanequivalence
relationonI.
nn
Definition 3.7 (LISCC). We define the low-input side-channel capacity of C for n ∈ N, LISCC(C, n),
as follows: LISCC(C, n) = |In /∼liscn |.
Intuitively, low-input side-channel capacity measures the number of equivalence classes of low inputs(i.e., attacker-controlled inputs) that can be obtained by observing the side-channel output, where two
low inputs are considered equivalent if they yield the same side-channel output for each high input (i.e.,secret). It is interesting to note that this is the standard definition of channel capacity for deterministic
systems [5,9,32,39,48,49], except that the roles of high inputs and low inputs are reversed.8 That is,while the standard channel capacity measures the amount of influence that the high inputs exert on thechannel output, our low-input channel capacity measures that exerted by the low inputs.
As a special case, we say that C is low-input side-channel non-interferent when LISCC(C, n) = 1 for
all n. Note that low-input side-channel non-interference is equivalent to the following condition which isthe standard definition of (side-channel) non-interference [23,47] with the roles of high inputs and low
inputs reversed: for all n ∈ N, v1 ∈ In , v2 ∈ In and s ∈ Sn , scn (s, v1 ) = scn (s, v2 ).
We now define the bounded low-input side-channel capacity condition.
Definition 3.8 (BLISCC). Let f : N → N,  : N → (0, 1], and  ∈ N. We say that the system C satisfies
the bounded low-input side-channel capacity condition with f ,  and , written BLISCC(f, , ), if thefollowing conditions are satisfied:(1) C is regular-channel (f, )-secure; and(2) For all n ∈ N, LISCC(C, n)  .9
We remark that, when  = 1, BLISCC(f, , ) implies that the side channel is low-input noninterferent. This restricted case corresponds to the LISCNI condition presented in [43].
The BLISCC condition ensures the security of systems after bucketing is applied. We next formalize
the notion of “applying bucketing”.
Definition 3.9 (Bucketing). Let C be a system and k ∈ N such that k > 0. The system C after kbucketing is applied, written Bktk (C), is a system C  that satisfies the following:(1) rcC   = rcC, S C   = S C, I C   = I C, and Orc C   = Orc C;(2) For all n ∈ N, Osc C  n = {1 , . . . , k } where i = j for each i = j ; and(3) For all n ∈ N, s1 , s2 ∈ Sn and v1 , v2 ∈ In , scCn (s1 , v1 ) = scCn (s2 , v2 ) ⇒ scC  n (s1 , v2 ) =scC  n (s2 , v2 ).
8 In QIF literature, channel capacity is typically defined to be the log of the number of equivalence classes. Here, we use thenon-log form which turns out to be more convenient for our purposes.
9 It is easy to relax the notion to be asymptotic so that channel capacity only needs to be bounded for large n.

620

T. Terauchi and T. Antonopoulos / Bucketing for timing attack mitigation

Roughly, k-bucketing partitions the side channel outputs into k number of buckets. We note that
our notion of “bucketing” is quite general in that it does not specify how the side channel outputs
are partitioned into the buckets. Indeed, as we shall show next, the security guarantee derived by
BLISCC only requires the fact that side channel outputs are partitioned into a small number of buckets. This makes our results applicable to any techniques (beyond the usual bucketing technique for timing channels [8,16,30,31,51]) that reduce the number of possible side-channel outputs. We remark thatLISCC(C, n)   implies that LISCC(Bktk (C), n)  .
We shall make use of the following lemma in the proof of BLISCC soundness theorem.
Lemma 3.10. Let C be a system, n ∈ N, and   1. Then, LISCC(C, n)   if and only if there exist
I 1 , . . . , I  such that the following conditions hold:(a) In = i=1 I i , and I i ∩ I j = ∅ for i = j ; and(b) For each i ∈ {1, . . . , }, s ∈ Sn , v1 ∈ I i and v2 ∈ I i , scn (s, v1 ) = scn (s, v2 ).
1Proof. We show the if direction. We have that |In /∼liscn |  . Therefore, we can construct I , . . . , I
1
m
lisc
i
satisfying (a) and (b) by letting I , . . . , I be the elements of In /∼n , and I = ∅ for each m < i  where m = |In /∼liscn |.
We show the only-if direction. Let I 1 , . . . , I  satisfy (a) and (b). For each I i ∈ {I 1 , . . . , I  }, therei∈ In /∼lisc. Let us choose one such [v]∼lisc
must be an equivalence class [v]∼lisc
n such that I ⊆ [v]∼lisc
n
n
n
i
1

and identify it by [vi ]∼lisc, for each I ∈ {I , . . . , I }. Then, {[vi ]∼lisc| i ∈ {1, . . . , }} is the set ofnnlisc| i ∈ {1, . . . , }}|  . 
equivalence classes In /∼lisc
n . Therefore, |In /∼n | = |{[vi ]∼liscn

We now state and prove the BLISCC soundness theorem. Informally, the soundness theorem says thata system satisfying the BLISCC condition becomes one that satisfies the SRSCR condition after somesuitable bucketing is applied.
Theorem 3.11 (BLISCC soundness). Suppose that C satisfies BLISCC(f, , ). Let k > 0 be such thatk    1. Then, Bktk (C) satisfies SRSCR(f, X) for some X satisfying the following:(♣) For all n ∈ N, 1 − (S,p)∈Xn |S|S|n | (1 − p)  k  · (n).
Proof. Let C  = Bktk (C). We shall prove by constructing an indexed family X such that X satisfies (♣)
and C  satisfies SRSCR(f, X). First, by condition (2) of BLISCC, it follows that LISCC(C, n)   forall n ∈ N and therefore LISCC(C  , n)   for all n ∈ N. Therefore, by Lemma 3.10, for each n ∈ N,
there exist In1 , . . . , In such that (a) In1 , . . . , In partition In , and (b) scC  n (s, v1 ) = scC  n (s, v2 ) forall s ∈ Sn , v1 ∈ Ini and v2 ∈ Ini . set {i ∈ N | 1  i  a}. For each n ∈ N and p : [1, ] → [1, k],p
let Sn = {s ∈ Sn | i∈[1,] ∀v ∈ Ini .scC  n (s, v) = p(i) }. From (a) and (b), it follows that, for eachs ∈ Sn , there is a unique p : [1, ] → [1, k] satisfying i∈[1,] ∀v ∈ Ini .scn (s, v) = p(i) . Therefore,

p
p
p
p
Sn ’s partition Sn , that is, Sn = p:[1,]→[1,k] Sn and Sn 1 ∩ Sn 2 = ∅ for p1 = p2 . Let X be the indexedfamily defined by p 
p |Sn |pSn , p (n)  p : [1, ] → [1, k] ∧ Sn = ∅ ∧ |Sn |/ Sn (n)  1
for each n ∈ N.
Xn =
|Sn |
We show that X satisfies (♣). Fix n ∈ N. Let A = {S | (S, _) ∈ Xn } and let Ac be the complement ofpp/ A}. Note that |A| + |Ac |  k  and |Sn |(n) > |S| forA, that is, Ac = {Sn | p : [1, ] → [1, k] ∧ Sn ∈

T. Terauchi and T. Antonopoulos / Bucketing for timing attack mitigation

621

each S ∈ Ac . Therefore,

 |S|
|Sn |
|S|
(1 − p) = 1 −
1−
(n)
1−
|Sn |
|Sn |
|S|
S∈A
(S,p)∈X


n

=1−

 |S|
|Sn |
S∈A

=1− 1−+ |A|(n) |S| 

S∈Ac

|Sn |

+ |A|(n)


 c
|S|


+ |A|(n) 1 − 1 − A maxc
S∈A |Sn |  1 − 1 − Ac (n) + |A|(n)  k  (n).
pAbove, the third line follows from the fact that Sn ’s partition Sn , that is, (A ∪ Ac ) = Sn .
Therefore, it suffices to show that C  satisfies SRSCR(f, X) (with the X we constructed). First, wepshow that the condition (2) of SRSCR(f, X) is satisfied. From the construction of Sn ’s, it follows thatppscC n (s1 , v) = scC n (s2 , v) = p(i) for all s1 ∈ Sn , s2 ∈ Sn and v ∈ In where v belongs to the(unique) low-input partition Ini . That is, the side channel of C  is non-interferent (with respect to highpinputs) for the subset Sn . Therefore, C  satisfies RR(#1 U ) for any U ≺ X.
It remains to show that the condition (1) of SRSCR(f, X) is satisfied. For contradiction, suppose thatC  |U is not regular-channel (f, errU )-secure for some U ≺ X. Let A be a regular-channel adversary forC  |U such that for infinitely many n  N, A queries (the regular channel of) C  |U at most f (n) manytimes and successfully recovers the secret with probability at least errU (n). We show that running A
against C  (by allowing arbitrary behavior when the secret is not from U ) successfully recovers the secretwith probability at least (n) for infinitely many n. To see this, let n ∈ N be such that A successfully
recovers the secret from C  |U with probability at least errU (n). Note that the probability that a secretpppprandomly selected from Sn belongs to Sn is |Sn |/|Sn |, i.e., Pr[s ∈ Sn | s ← Sn ] = |Sn |/|Sn |. Then,ppbecause errU (n) = (|Sn |/|Sn |)(n) where Sn = #1 Un , it follows that
 |Snp |•C  |•· errU (n) = (n).
Pr WinCA (n, f )  Pr[s ∈ Snp | s ← Sn ] · Pr WinA U (n, f ) 
|Sn |
•

•

Because Pr[WinCA (n, f )] = Pr[WinCA (n, f )], this contradicts condition (1) of BLISCC(f, , ) whichsays that C is regular-channel (f, )-secure. Therefore, C  |U is regular-channel (f, errU )-secure. As a corollary of Theorems 3.4 and 3.11, we have the following.
Corollary 3.12. Suppose that C satisfies BLISCC(f, , ). Let k > 0 be such that k  ·   1. Then,
Bktk (C) is (f, k  · )-secure.
Note that as k approaches 1 (and hence the system becomes constant-time), the security bound of
Bktk (C) approaches (f, ), matching the regular-channel security of C. As with Theorem 3.4, Theorem 3.11 may give an impression that the conditions only affect the adversary-success probability

622

T. Terauchi and T. Antonopoulos / Bucketing for timing attack mitigation

parameter (i.e., ) of (f, )-security, leaving the number of queries parameter (i.e., f ) unaffected. However, as also remarked in Remark 2.4, the two parameters are often correlated so that a change in one
can affect the other. Also, like SRSCR, BLISCC separates the concerns regarding regular channels fromthose regarding side channels. A system designer may check the security of the regular channel while
disregarding the side channel, and separately prove the condition on the side channel.
We remark that Theorem 3.11 and Corollary 3.12 substantially improve the corresponding resultsfrom [43]. First, the results in [43] were restricted only to the low-input side-channel non-interference,that is, the case where  is restricted to be 1 in BLISCC(f, , ). Secondly, even for the low-input sidechannel non-interferent case, it could only deduce rather pessimistic security bounds, that is, (f, 1 −1/k + )-security. By contrast, this paper generalizes the results to be applicable to cases where thesystem is not low-input side-channel non-interferent but has a bounded low-input side-channel capacity,that is, the cases where  > 1. In addition, the new results are able to derive much tighter security
bounds. Namely, when  = 1, we are able to derive (f, k · )-security, substantially improving thepreviously derivable bound (note that k ·   1 − 1/k +  for all valid k and ). For example, this allows
the derivation of a strong security bound in Example 3.13 below.10 We remark that the improvements
are made possible by the extended SRSCR soundness theorem of this paper (cf. Theorem 3.4) which
generalized the corresponding theorem from [43] by allowing different error bounds to be assigned todifferent secret subsets.
Example 3.13 (Fast modular exponentiation). Fast modular exponentiation is an operation that is often
found in cryptography algorithms such as RSA [27,35]. Figure 2 shows its implementation written in a
C-like language. It computes yx mod m where x is the secret represented as a length n bit array, y is anattacker controlled-input, and m is a constant. The program is not constant-time (assuming that then andelse branches in the loop have different running times), and effective timing attacks have been proposed
for the program [27,35].
i = 0;
a = 1;
while (i < n) {if (x[i] == 1) {r = (a * y) % m;
} else {r = a;}a = (r * r) % m;i++;}return r;
Fig. 2. Fast modular exponentiation.

10 For the same example, [43] erroneously asserts the strong bound which cannot be actually derived by the results in that

paper (the error is corrected in the authors’ online copy of that paper by asserting a weaker bound [44]).

T. Terauchi and T. Antonopoulos / Bucketing for timing attack mitigation

623

However, assuming that running time of the operation (a * y) % m is independent of y, it canbe seen that the program satisfies the BLISCC condition.11 Under the assumption, the program can beformalized as the system C where, for all n ∈ N,
• Sn = In = {0, 1}n ;• Onrc = Onsc = N;
• For all (s, v) ∈ Sn × In , rcn (s, v) = v s mod m; and• For all (s, v) ∈ Sn × In , scn (s, v) = timet · num(s, 1) + timef · num(s, 0).
Here, num(s, b) = |{i ∈ N | i < n ∧ s[i] = b}| for b ∈ {0, 1}, and timet (resp. timef ) is the running
time of the then (resp. else) branch.
Let the computation class of adversaries be the class of randomized polynomial time algorithms.
Then, under the standard computational assumption that inverting modular exponentiation is hard, one
can show that C satisfies BLISCC(f, , 1) for any f and negligible . This follows because the sidechannel outputs are independent of low inputs, and the regular-channel is (f, )-secure for any f andnegligible  under the assumption.12 Therefore, by applying bucketing, it can be made (f, k · )-secure
for any f and negligible  (and hence (f, )-secure for any f and negligible ). We remark that the same
security bound can also be obtained even when the assumption is relaxed so that low input y can exert anon-zero (but bounded) influence on the running time (i.e., when the program satisfies BLISCC(f, , )
for some  > 1).
Example 3.14 (Timeout options). We show another example demonstrating the usefulness of the
BLISCC condition. This is a meta example, in which we add timeout options to the given program.
Suppose that we are given a system C that is regular-channel (f, )-secure and LISCC(C, n)   for alln ∈ N. Let T = {t1 , . . . , tm } ⊆ N ∪ {∞} be a finite set of timeout options where t < ∞ for any t ∈ N.
Then, C with the timeout option T is a system C  such that• rcC   = rcC, S C   = S C, and Orc C   = Orc C;• For all n ∈ N, I C  n = I Cn × T ;• For all n ∈ N, Osc C  n = Osc Cn ∪ {⊥}; and• For all n ∈ N, s ∈ Sn and (v, t) ∈ I C  n , scC  n (s, (v, t)) = timeout(t, scCn (s, v)) where
timeout = λt1 , t2 .if t1 < t2 then ⊥ else t2 .
Roughly, C  takes an additional timeout parameter in its low input so that the execution is halted at thetime given as the parameter and using ∞ for the parameter means no timeout. The occurrence of timeout
is represented by the side channel output ⊥. As we shall show below, BLISCC soundness theorem can beused to deduce that, even with the addition of the timeout option, the security of the system is ensured
to a certain degree when bucketing is applied.13
First, we show that LISCC(C  , n)   × m for all n ∈ N (recall that |T | = m). Let n ∈ N. Because
LISCC(C, n)  , by Lemma 3.10, there exists a partition I 1 , . . . , I  of I Cn such that for all i ∈11 This is admittedly an optimistic assumption. Indeed, proposed timing attacks exploit the fact that the running time of theoperation can depend on y [27,35]. Here, we assume that the running time of the operation is made independent of y by somemeans (e.g., by adopting the constant-time implementation technique).
12 The latter holds because (f, )-security is asymptotic and the probability that any regular-channel adversary of the computation class may correctly guess the secret for this system is negligible (under the computational hardness assumption).
Therefore, a similar analysis can be done for any sub-polynomial number of buckets.
13 We have allowed C  to output the (actual) regular-channel output even when timeout has reached. This is sufficient forderiving a security bound as it only increases the attacker’s knowledge.

624

T. Terauchi and T. Antonopoulos / Bucketing for timing attack mitigation{1, . . . , }, s ∈ Sn , v1 ∈ I i and v2 ∈ I i , scCn (s, v1 ) = scCn (s, v2 ). For each s ∈ Sn and i ∈{1, . . . , }, let os,i be the unique o ∈ Osc Cn satisfying ∀v ∈ I i .scCn (s, v) = o. For each i ∈{1, . . . , } and j ∈ {1, . . . , m}, let I i,j = I i × {tj }. Clearly, I 1,1 , . . . , I ,m partition I C  n . Also,
for all s ∈ Sn , (v1 , tj ) ∈ I i,j and (v2 , tj ) ∈ I i,j , scC  n (s, v1 ) = scC  n (s, v2 ) = timeout(tj , os,i ).
Therefore, by Lemma 3.10, LISCC(C  , n)   × m. Therefore, BLISCC(f, , m) is satisfied. Therefore,
by Corollary 3.12, Bktk (C  ) is (f, k m · )-secure, for k satisfying k m ·   1.
Example 3.15 (Failure of BLISCC-like conditions on the leaky login program). We cannot apply
BLISCC to the leaky login program from Example 2.2 to prove its security after applying bucketing.
This is because the program’s low-input side-channel capacity is unbounded. Specifically, it can beshown that LISCC(C, n) = |In | = 2n , because for every pair of low inputs v1 ∈ In and v2 ∈ In suchthat v1 = v2 , there exists a secret s ∈ Sn that distinguishes v1 and v2 (namely, s whose lengths of matching prefixes are different for v1 and v2 ). Nevertheless, as we have shown in Example 3.5, the program
can be made secure by applying bucketing. In fact, as we have shown there, it becomes one that satisfies
SRSCR after applying bucketing. Ideally, we would like to find a relatively simple condition (on systems before bucketing is applied) that can cover many systems that would become secure by applying
bucketing, such as the leaky login program.
Unfortunately, as we shall show next, there cannot be such a condition if bucketing is formalized in
the very permissive way as we have done in this paper. Recall that in Definition 3.9, we have formalized
bucketing to be a program transformation that partitions the side-channel outputs into some number ofbuckets, but placed no restriction on which side-channel outputs are put into which bucket. Below, weshow a bucketed version of the leaky login program that is efficiently attackable by an adaptive adversary.
As we shall show, bucketing partitions the side-channel outputs into only two buckets, but does so in arather unrealistic manner. This bucketed leaky login program is formalized as the following system:• rc, sc, I , Orc are as in Example 2.2;
• For all n ∈ N, Onsc = {0, 1}; and• For all n ∈ N and (s, v) ∈ Sn × In , scn (s, v) = (argmaxi si = vi ) mod 2.
Note that the side-channel outputs are partitioned into two buckets, that is, the side channel outputs 0 if
the length of the matching prefix is even and outputs 1 if it is odd.
We show that the system is efficiently attackable. For b ∈ {0, 1}, let b be the complement of b, thatis, 0 = 1 and 1 = 0. For v ∈ {0, 1}n and 0  i  n − 1, let flip(v, i) be the n-bit sequence such thatflip(v, i)[i] = v[i] and flip(v, i)[j ] = v[j ] for j = i. For s ∈ Sn and v ∈ In , let us write mplen(s, v) tobe the length of the matching prefix, that is, mplen(s, v) = argmaxi si = vi .
The attack on the system proceeds as follows. The adversary A chooses an arbitrary v1 ∈ In as theinitial input and records the output o1 . Note that o1 = 0 if and only if mplen(s, v1 ) is even. Then, A
chooses v1,1 = flip(v1 , o1 + 1) as the next input and observes the output o1,1 . Note that o1 = o1,1 if andonly if mplen(s, v1 ) = o1 . A continues the process, each time choosing v1,j = flip(v1 , o1 +2j −1) as the
input for each j ∈ {j ∈ N | j  1 ∧ o1 + 2j − 1 < n} in the increasing order, until he observes o1,j suchthat o1 = o1,j (if no such j is found and s = v1 which A can detect by observing the regular channel,
then s = flip(v1 , n − 1) and so A has recovered the entire s). At such a point, A has discovered that
mplen(s, v1 ) = o1 +2j −2. Let x1 = mplen(s, v1 ). Note that A at this point has recovered the first x1 +1
bits of s (the x1 + 1-th bit, s[x1 ], is equal to v1 [x1 ]). Also, A makes j + 1 = (x1 − o1 )/2 + 2  2(x1 + 1)
queries for this (i.e., the queries v1 , v1,1 , . . . , v1,j ). A then chooses as the next input an arbitrary v2 ∈ In
satisfying v2 [i] = s[i] for all 0  i < x1 + 1. A now uses the same process that he used to discover x1

T. Terauchi and T. Antonopoulos / Bucketing for timing attack mitigation625

to discover x2 = mplen(s, v2 ), except that this time, he starts with the query v2,1 = flip(v2 , x1 + o2 + 2)
where o2 is the output given the input v2 . By this process, A will recover up to the x2 + 1-th bit of s inat most 2(x2 − x1 ) additional queries. Repeating this, A makes at most 2n queries total to recover theentire bits of s. Thus, the system is not (2n, )-secure for any .
The above shows that our definition of bucketing is too permissive for proving its effectiveness on the
leaky login program. The issue here is that the definition allows an arbitrary, even unrealistic, partitioningof side-channel outputs. Note that partitioning odd timings from even timings cannot happen in reality
because for any timing outputs o1 , o2 , o3 such that o1  o2  o3 , if o1 and o3 are put in a same bucket
then so must o2 (recall that bucketing is a technique that buffers and delays the output until the next timeinterval). A possible remedy for the issue is to incorporate the ordering constraint in the definition ofbucketing so that an unrealistic partitioning like the above would be disallowed. We leave the issue for
future work.
Remark 3.16. We make some additional observations regarding the BLISCC condition. First, as we havenoted before, low-input side-channel capacity is equivalent to the ordinary (i.e., high-input) side-channel
capacity but with the roles of high inputs and low inputs reversed. Therefore, it is amenable to various
techniques proposed for checking and inferring channel capacity [5,9,32,39,48,49]. Furthermore, as
we have noted before, in the case where the bound is 1, the problem becomes low-input side-channel
non-interference. Similar to the refinement order relation (i.e., condition (2) of SRSCR), low-input sidechannel non-interference is a 2-safety property and can be checked by the methods for checking ordinaryside-channel non-interference by reversing the roles of high inputs and low inputs [1,3,6,11,24].
Secondly, we remark that it is easy to extend the channel capacity parameter  in BLISCC(f, , )
to be a function on the security parameter (i.e., n) similar to f and . Such an extension would allow
us to reason about the case where the low-input side-channel capacity can vary for different sizes ofsecrets (however, because  appears in the exponent of the deduced security bound, the extension will
only be useful for the case when the channel capacity grows very slowly). Likewise, while we restricted
the number of buckets parameter k in the definition of bucketing constant, it is easy to extend it to
be a function on the security parameter, which would allow us to analyze the security guarantee frombucketing strategies that use different numbers of buckets for different sizes of secrets.
3.3. Combining bucketing and constant-time implementation compositionally
We show that the BLISCC condition may be applied compositionally with the constant-time implementation technique (technically, we will only apply the condition (2) of BLISCC compositionally). As
we shall show next, the combined approach is able to ensure security of some non-constant-time systems that cannot be made secure by applying bucketing globally to the whole system. We remark that,in contrast to those of the previous sections of the paper, the results of this section are more specialized
to the case of timing channels. First, we formalize the notion of constant-time implementation.
Definition 3.17 (Constant-time). Let f : N → N and  : N → (0, 1]. We say that a system C satisfies
the constant-time condition (or, timing-channel non-interference) with f and , written CT(f, ), if thefollowing is satisfied:(1) C is regular-channel (f, )-secure; and(2) For all n ∈ N, v ∈ In , and s1 , s2 ∈ Sn , scn (s1 , v) = scn (s2 , v).

626

T. Terauchi and T. Antonopoulos / Bucketing for timing attack mitigation

Note that CT requires that the side channel is non-interferent (with respect to secrets). The following
theorem is immediate from the definition, and states that CT is a sufficient condition for security.
Theorem 3.18 (CT soundness). If C satisfies CT(f, ), then C is (f, )-secure.
To motivate the combined application of CT and BLISCC, let us consider the following example which
is neither constant-time nor can be made secure by (globally) applying bucketing.
Example 3.19. Figure 3 shows a simple, albeit contrived, program that we will use to motivate the
combined approach. Here, sec is an n-bit secret and inp is an n-bit attacker-controlled input. Bothsec and inp are interpreted as unsigned n-bit integers where − and > are the usual unsigned integer
subtraction and comparison operations. The regular channel always outputs true and hence is noninterferent. Therefore, only the timing channel is of concern.
The program can be formalized as the system Ccomp where for all n ∈ N,
• Sn = In = {0, 1}n ;• Onrc = {•};• Onsc = {i ∈ N | i  2n+1 };• For all (s, v) ∈ Sn × In , rcn (s, v) = •; and• For all (s, v) ∈ Sn × In , scn (s, v) = s + v.
Note that the side channel outputs the sum of the high input and the low input. It is easy to see that thesystem is not constant-time (i.e., not CT(f, ) for any f and ). Furthermore, the system is not secure as
is, because an adversary can immediately recover the secret by querying with any input and subtracting
the input from the side-channel output.
Also, it is easy to see that the system does not satisfy BLISCC(f, , ) for any f ,  and  either. This isbecause scn (s, v1 ) = scn (s, v2 ) for any s and v1 = v2 , and therefore LISCC(Ccomp , n) = |In | = 2n . In
fact, we can show that arbitrarily applying bucketing (globally) to the system does not guarantee security.
To see this, let us consider applying bucketing with just two buckets whereby the buckets partition thepossible running times in two halves so that running times less than or equal to 2n fall into the first bucket
and those greater than 2n fall into the other bucket. After applying bucketing, the system is C  where• rcC  , S C  , I C  , and Orc C   are same as those of Ccomp ;• For all n ∈ N, Osc C  n = {0, 1}; and• For all n ∈ N and (s, v) ∈ Sn × In , scC  n (s, v) = 0 if s + v  2n , and scC  n (s, v) = 1
otherwise.
while (sec > 0) {sec = sec - 1;}
while (inp > 0) {inp = inp - 1;}
return true;
Fig. 3. A non-constant-time program that cannot be made secure by globally applying bucketing.

T. Terauchi and T. Antonopoulos / Bucketing for timing attack mitigation

627

We show that there exists an efficient adaptive attack against C  . Let s ∈ Sn . The adversary A recoverss by only making linearly many queries via the following process. First, A queries with the input v1 =2n−1 . By observing the side-channel output, A will know whether 0  s  2n−1 (i.e., the side-channel
output was 0) or 2n−1 < s  2n (i.e., the side-channel output was 1). In the former case, A picks the
input v2 = 2n−1 + 2n−2 for the next query, and in the latter case, he picks v2 = 2n−2 . Continuing theprocess in a binary search manner and reducing the space of possible secrets by 1/2 in each query, A isable to hone in on s within n many queries. Therefore, C  is not (n, )-secure for any .
Next, we present the compositional bucketing approach. Roughly, our compositionality theorem (Theorem 3.21) states that the sequential composition of a constant-time system with a system whose sidechannel has a bounded low-input channel capacity can be made secure by applying bucketing to only
the non-constant-time component. As with BLISCC, the degree of security of the composed system isrelative to that of the regular channel, the channel capacity quantity, and the granularity of buckets.
To state the compositionality theorem, we explicitly separate the conditions on side channels of CT and
BLISCC from those on regular channels and introduce terminologies that only refer to the side-channel
conditions. Let us fix C. We say that C satisfies CTsc , if it satisfies condition (2) of CT(_, _), that is, for
all n ∈ N, v ∈ In , and s1 , s2 ∈ Sn , scn (s1 , v) = scn (s2 , v). Also, we say that C satisfies BLISCCsc ()if it satisfies condition (2) of BLISCC(_, _, ), that is, for all n ∈ N, LISCC(C, n)  . Next, we define
sequential composition of systems.
Definition 3.20 (Sequential composition). Let C † and C ‡ be systems such that S C †  = S C ‡ ,
I C †  = I C ‡ , and for all n ∈ N, Osc C ‡ n ⊆ N and Osc C ‡ n ⊆ N. The sequential compositionof C † with C ‡ , written C † ; C ‡ , is the system C such that• S C = S (C † ) and I C = I (C † ); and• For all n ∈ N and (s, v) ∈ Sn × In , scC  n (s, v) = scC † n (s, v) + scC ‡ n (s, v).
We note that the definition of sequential composition specifically targets the case when the side channel is a timing channel, and says that the side-channels outputs are numeric values and that the sidechannel output of the composed system is the sum of those of the components. Also, the definition
leaves the composition of regular channels open, and allows the regular channel of the composed system
to be any function from Sn × In . We are now ready to state the compositionality theorem.
Theorem 3.21 (Compositionality). Let C † be a system that satisfies BLISCCsc () and C ‡ be a systemthat satisfies CTsc . Let k > 0. Suppose that Bktk (C † ); C ‡ is regular-channel (f, )-secure where k·  1.
Then, Bktk (C † ); C ‡ satisfies SRSCR(f, X) for some X satisfying the following:(♣) For all n ∈ N, 1 − (S,p)∈Xn |S|S|n | (1 − p)  k  · (n).
Proof. Let C = Bktk (C † ); C ‡ . The proof is similar to that of Theorem 3.11, and we prove byconstructing an indexed family X such that X satisfies (♣) and C satisfies SRSCR(f, X). First, by
BLISCCsc , it follows that LISCC(Bktk (C † ), n)   for all n ∈ N. Therefore, by Lemma 3.10, for eachn ∈ N, there exist In1 , . . . , In such that (a) In1 , . . . , In partition In , and (b) for each i ∈ {1, . . . , },scBktk (C † )n (s, v1 ) = scBktk (C † )n (s, v2 ) for all s ∈ Sn , v1 ∈ Ini and v2 ∈ Ini . For each n ∈ N andpp : [1, ] → [1, k], let Sn = {s ∈ Sn | i∈[1,] ∀v ∈ Ini .scBktk (C † )n (s, v) = p(i) }. From (a) and (b),

p
p
p
p
it is immediate that Sn ’s partition Sn , that is, Sn = p:[1,]→[1,k] Sn and Sn 1 ∩ Sn 2 = ∅ for p1 = p2 . Let

628

T. Terauchi and T. Antonopoulos / Bucketing for timing attack mitigation

X be the indexed family defined by
Xn =



 p p p : [1, ] → [1, k] ∧ Sn = ∅ ∧ |Sn |/Sn  (n)  1|Sn |Snp , p (n)|Sn |for each n ∈ N.

By an argument similar to that in the proof of Theorem 3.11, we can show that X satisfies (♣). Therefore, it suffices to show that C satisfies SRSCR(f, X) (with the X we constructed). We can show thecondition (1) of SRSCR(f, X) by an argument similar to that in the proof of Theorem 3.11 as the argument only concerns the regular channel. Therefore, it remains to show the condition (2) of SRSCR(f, X).
p
From the construction of Sn ’s, it follows that scBktk (C † )n (s1 , v) = scBktk (C † )n (s2 , v) = p(i) forpp
all s1 ∈ Sn , s2 ∈ Sn and v ∈ In where Ini is the unique low input partition such that v ∈ Ini . Then,ppbecause scC ‡ n (s1 , v) = scC ‡ n (s2 , v) by CTsc of C ‡ , for all v ∈ In , s1 ∈ Sn and s2 ∈ Sn , we have




 
(s1 , v) + sc C ‡ n (s1 , v)

 
 
= sc Bktk C † n (s2 , v) + sc C ‡ n (s2 , v)

scCn (s1 , v) = sc Bktk C †n= scCn (s2 , v).
p

Therefore, the side channel of C is non-interferent (with respect to high inputs) for the subset Sn . Therefore, C satisfies RR(#1 U ) for any U ≺ X. 
As a corollary of Theorems 3.4 and 3.21, we have the following.
Corollary 3.22. Let C † be a system that satisfies BLISCCsc () and C ‡ be a system that satisfies CTsc . Let
k > 0. Suppose that Bktk (C † ); C ‡ is regular-channel (f, )-secure where k ·   1. Then, Bktk (C † ); C ‡is (f, k  · )-secure.
We note that the notion of sequential composition is symmetric. Therefore, Corollary 3.22 implies
that composing the components in the reverse order, that is, C ‡ ; Bktk (C † ), is also secure provided thatits regular channel is secure.
The compositionality theorem suggests the following compositional approach to ensuring security.
Given a system C that is a sequential composition of a component that satisfies the constant-time property (i.e., satisfies CTsc ) and a component with a bounded low-input side-channel capacity (i.e., satisfies
BLISCCsc ), we can ensure the security of C by proving its regular-channel security and applying bucketing only to the non-constant-time component.
Example 3.23. Let us apply compositional bucketing to the system Ccomp from Example 3.19. Recall
that the system is neither constant-time nor applying bucketing to the whole system ensures its security.
The system can be seen as the sequential composition Ccomp = C † ; C ‡ where C † and C ‡ satisfy thefollowing:• S and I are as in Ccomp ;• For all n ∈ N, Osc C † n = Osc C ‡ n = {i ∈ N | i  2n }; and• For all n ∈ N and (s, v) ∈ Sn × In , scC † n (s, v) = s and scC ‡ n (s, v) = v.
Roughly, Ccomp is decomposed so that C † is the first loop and C ‡ is the second loop (cf. Fig. 3).

T. Terauchi and T. Antonopoulos / Bucketing for timing attack mitigation

629

Note that C ‡ satisfies CTsc as its side-channel outputs are high-input independent, and, C † satisfies
BLISCCsc (1) as its side-channel outputs are low-input independent. By applying bucketing only to thecomponent C † , we obtain the system Bktk (C † ); C ‡ . The regular-channel of Bktk (C † ); C ‡ (i.e., that ofCcomp ) is (f, )-secure for any f and negligible  because it is non-interferent (with respect to highinputs) and the probability that an adversary may recover a secret for such a system is at most 1/|Sn |.14
Therefore, by Corollary 3.22, Bktk (C † ); C ‡ is (f, k  )-secure for any f and negligible , and therefore,
Bktk (C † ); C ‡ is (f, )-secure for any f and negligible .
The above example shows that compositional bucketing can be used to ensure security of nonconstant-time systems that cannot be made secure by a whole-system bucketing. It is interesting toobserve that the constant-time condition, CTsc , requires the side-channel outputs to be independent ofhigh inputs but allows dependency on low inputs, while BLISCC is the dual and says that the side-channel
outputs have a limited dependency on low inputs but may depend arbitrarily on high inputs. Our compositionality theorem (Theorem 3.21) states that a system consisting of such parts can be made secure
by applying bucketing only to the part that satisfies the latter condition.
It is easy to see that sequentially composing components that satisfy CTsc results in a system thatsatisfies CTsc . Likewise, as shown below, sequentially composing components that satisfy BLISCCsc
results in a system that satisfies BLISCCsc .
Lemma 3.24. Suppose that C1 satisfies BLISCCsc (1 ) and C2 satisfies BLISCCsc (2 ), then C1 ; C2 satisfies BLISCCsc (1 · 2 ).
Proof. Fix n ∈ N. By Lemma 3.10, for each j ∈ {1, 2}, there exist Ij1 , . . . , Iji such that (a) Ij1 , . . . , Ij jpartition In , and (b) for each i ∈ {1, . . . , j }, scCi n (s, v1 ) = scC  n (s, v2 ) for all s ∈ Sn , v1 ∈ Iji andv2 ∈ Iji .
For each (i1 , i2 ) ∈ [1, 1 ]×[1, 2 ], let I i1 ,i2 = {v ∈ In | v ∈ I1i1 ∧ v ∈ I2i2 }. It is easy to see that the sets 
I i1 ,i2 partition In , that is, In = (i1 ,i2 )∈[1,1 ]×[1,2 ] I i1 ,i2 and I i1 ,i2 ∩ I i1 ,i2 = ∅ for any (i1 , i2 ) = (i1 , i2 ).
Also, for any s ∈ Sn , v ∈ I i1 ,i2 and v  ∈ I i1 ,i2 , we havescC1 ; C2 n (s, v) = scC1 n (s, v) + scC2 n (s, v)= scC1 n s, v  + scC2 n s, v = scC1 ; C2 n (s, v)
because scC1 n (s, v) = scC1 n (s, v  ) and scC2 n (s, v) = scC2 n (s, v  ). Therefore, by Lemma 3.10,
C1 ; C2 satisfies BLISCC(1 · 2 ). 
Therefore, such compositions can be used freely in conjunction with the compositional bucketing
technique of this section. We also conjecture that components that are made secure by compositional
bucketing can themselves be sequentially composed to form a secure system (possibly with some decrease in the degree of security). We leave a more detailed investigation for future work.
14 Therefore, a similar analysis can be done for any strictly sub-exponential number of buckets.

630

T. Terauchi and T. Antonopoulos / Bucketing for timing attack mitigation

4. Related work
As remarked in Section 1, much research has been done on defending against timing attacks and moregenerally side channel attacks. For instance, there have been experimental evaluations on the effectiveness of bucketing and other timing-channel mitigation schemes [16,22], and other works have proposed
information-theoretic methods for formally analyzing the security of (deterministic and probabilistic)
systems against adaptive adversaries [14,29].
However, few prior works have formally analyzed the effect of bucketing on timing channel security(or similar techniques for other side channels) against adaptive adversaries. Indeed, to our knowledge,
the only prior work to do so are the series of works by Köpf et al. [30,31] who investigated the effect of bucketing applied to blinded cryptography algorithms. They show that applying bucketing to ablinded cryptography algorithm whose regular channel is IND-CCA2 secure results in an algorithm thatis IND-CCA2 secure against timing-channel-observing adversaries. In addition, they show bounds on
information leaked by such bucketed blinded cryptography algorithms in terms of quantitative information flow [5,32,39,49,50]. By contrast, we analyze the effect of applying bucketing to general systems,
show that bucketing is in general insufficient against adaptive adversaries, and present novel conditions
that guarantee security against such adversaries. In fact, the results of [30,31] may be seen as an instanceof our BLISCC(f, , ) condition for the case  = 1 because blinding makes the behavior of cryptographic algorithms effectively independent of attacker-controlled inputs. Also, our results are givenin the form of (f, )-security, which can provide precise bounds on the number of queries needed byadaptive adversaries to recover secrets.
Next, we compare our work with the works on constant-time implementations (i.e., timing-channel
non-interference) [1,3,6,11,24,26]. The previous works have proposed methods for verifying that thegiven system is constant-time [3,6,11,24] or transforming it to one that is constant-time [1,26]. As wehave also discussed in this paper (cf. Theorem 3.18), it is easy to see that the constant-time condition
directly transfers the regular-channel-only security to the security for the case with timing channels.
By contrast, security implied by bucketing is less straightforward. In this paper, we have shown thatbucketing is in general insufficient to guarantee the security of systems even when their regular channel
is perfectly secure. And, we have presented results that show that, under certain conditions, the regularchannel-only security can be transferred to the side-channel-observing case to certain degrees. Because
there are advantages of bucketing such as efficiency and ease of implementation [8,16,30,31,51], we
hope that our results will contribute to a better understanding of the bucketing technique and foster
further research on the topic.
Next, we remark on a recent work by Tizpaz-Niari et al. [45] that proposes an interesting mitigation
scheme against timing channel attacks. Like every timing channel mitigation schemes, their scheme
works by changing the time when an output is released to the adversary-observing environment. However, whereas bucketing simply delays the output of the (unmodified) system until the next time intervalby blackbox monitoring, they propose to monitor the internal of the system so that different amounts ofdelay can be added for different runs of the system. Similar to bucketing, they use the delays to partition
the outputs to a small set of possibilities. However, a much more flexible partitioning is possible thanks
to the internal monitoring (indeed, an arbitrary partitioning can be achieved by this scheme). They argue the security in terms of quantitative information flow. However, they implement their scheme as abest effort method that uses dynamic analyses to estimate the timing channel leakage and adds delays
based on run-time characteristics such as basic block calls, and therefore they lack a formal guaranteeof security. Also, unlike our work which uses a parametric notion of security (i.e., (f , )-security),

T. Terauchi and T. Antonopoulos / Bucketing for timing attack mitigation

631

they use what they call a functional observation model of security, which amounts to security against
an adversary who makes an unlimited number of queries (i.e., with every possible public inputs). Notethat a parametric notion of security is required to argue the security of systems like the bucketed leaky
login program, because an adversary is able to always recover the secret for that system if an unlimited
number of queries to the side channel are allowed.
Finally, we remark on a work by Svenningsson and Sands [41] which is related to the SRSCR condition of this paper in an interesting way. Their work suggests to verify side-channel security by having the
programmer provide a declassification program (similarly in style to delimited information release [38])whose regular channel leaks at least as much information about the secrets as the side channel of thetarget system does. That is, the side channel of the target system is in the refinement order relation withthe regular channel of the declassification program. This allows the side-channel security of the target
system to be reduced to the regular-channel security of the target system and that of the declassification
program. As such, their work is related to our SRSCR condition that also relates information leaked bya side channel to that leaked by a regular channel. However, whereas our SRSCR considers refinement
order relation on subsets of secrets (for which the regular-channel can be proven secure), their work considers that on the entire space of secrets. Furthermore, their approach requires a separate declassification
program whose regular-channel is related to the target system’s side-channel whereas SRSCR relates
the regular and side channels of the same target system.
5. Conclusion and future work
In this paper, we have presented a formal analysis of the effectiveness of the bucketing techniqueagainst adaptive side-channel-observing adversaries. We have shown that bucketing is in general insufficient against such adversaries, and presented two novel conditions, SRSCR and BLISCC, that guarantee
security against such adversaries. SRSCR states that a system that satisfies it is secure, whereas BLISCC
states that a system that satisfies it becomes secure when bucketing is applied. We have shown that bothconditions facilitate proving the security of systems against adaptive side-channel-observing adversaries
by allowing a system designer to prove the security of the system’s regular channel separately from theconcerns of its side-channel behavior. By doing so, the security of the regular-channel is transferred, tocertain degrees, to the full side-channel-aware security. We have also shown that the BLISCC condition
can be used in conjunction with the constant-time implementation technique in a compositional manner to further increase its applicability. We have formalized our results via the notion of (f, )-security,
which gives precise bounds on the number of queries needed by adaptive adversaries to recover secrets.
We have opted to adopt an asymptotic notion of security to define (f, )-security, mainly to simplify the
exposition of applying our techniques to programs with only computational security guarantee, such as
the fast modular exponentiation program. However, all of our results hold even if the definition of security is changed to be non-asymptotic (i.e., by requiring N to be 0 in Definition
2.1) by only changing thecondition ♠ in Theorem 3.4 to be non-asymptotic, that is, ∀n ∈ N.1 − (S,p)∈Xn |S|S|n | (1 − p)  (n).
While we have instantiated our results to timing channels and bucketing, many of the results are
actually quite general and are applicable to side channels other than timing channels. Specifically, aside
from the compositional bucketing result that exploits the “additive” nature of timing channels, the results
are applicable to any side channels and techniques that reduce the number of possible side-channel
observations.
As future work, we would like to extend our results to probabilistic systems. Currently, our results arelimited to deterministic systems, and such an extension would be needed to assess the effect of bucketing

632

T. Terauchi and T. Antonopoulos / Bucketing for timing attack mitigation

when it is used together with countermeasure techniques that involve randomization. We would also liketo improve the conditions and the security bounds thereof to be able to better analyze systems suchas the leaky login program shown in Examples 2.2, 2.3 and 3.5. Finally, we would like to extend theapplicability of the compositional bucketing technique by considering more patterns of compositions,such as sequentially composing components that themselves have been made secure by compositional
bucketing.
Acknowledgments
This work was supported by JSPS KAKENHI Grant Numbers 17H01720, 18K19787, 20H04162 and
20K20625, JSPS Core-to-Core Program, A.Advanced Research Networks, and Office of Naval Research(ONR) award #N00014-17-1-2787.
References[1] J. Agat, Transforming out timing leaks, in: Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles ofProgramming Languages (POPL 2000), ACM, 2000, pp. 40–53.
[2] A. Aguirre, G. Barthe, M. Gaboardi, D. Garg and P. Strub, A relational logic for higher-order programs, PACMPL 1(ICFP)(2017), 21:1–21:29.
[3] J.B. Almeida, M. Barbosa, G. Barthe, F. Dupressoir and M. Emmi, Verifying constant-time implementations, in: USENIX
Security Symposium, 2016, pp. 53–70.
[4] J.B. Almeida, M. Barbosa, J.S. Pinto and B. Vieira, Formal verification of side-channel countermeasures using selfcomposition, Science of Compututer Programming 78(7) (2013), 796–812. doi:10.1016/j.scico.2011.10.008.
[5] M.S. Alvim, K. Chatzikokolakis, C. Palamidessi and G. Smith, Measuring information leakage using generalized gain
functions, in: Proceedings of the 25th IEEE Computer Security Foundations Symposium (CSF 2012), IEEE Computer
Society, 2012, pp. 265–279. doi:10.1109/CSF.2012.26.
[6] T. Antonopoulos, P. Gazzillo, M. Hicks, E. Koskinen, T. Terauchi and S. Wei, Decomposition instead of self-composition
for proving the absence of timing channels, in: Proceedings of the 38th ACM SIGPLAN Conference on Programming
Language Design and Implementation (PLDI 2017), ACM, 2017, pp. 362–375. doi:10.1145/3062341.3062378.
[7] T. Antonopoulos and T. Terauchi, Games for security under adaptive adversaries, in: Proceedings of the 31st IEEE Computer Security Foundations Symposium (CSF 2019), IEEE Computer Society, 2019, pp. 216–229. doi:10.1109/CSF.2019.
00022.
[8] A. Askarov, D. Zhang and A.C. Myers, Predictive black-box mitigation of timing channels, in: Proceedings of the 17th
ACM Conference on Computer and Communications Security (CCS 2010), ACM, 2010, pp. 297–307.
[9] M. Backes, B. Köpf and A. Rybalchenko, Automatic discovery and quantification of information leaks, in: Proceedingsof the 30th IEEE Symposium on Security and Privacy (S&P 2009), IEEE Computer Society, 2009, pp. 141–153. doi:10.
1109/SP.2009.18.
[10] G. Barthe, P.R. D’Argenio and T. Rezk, Secure information flow by self-composition, Mathematical Structures in Computer Science 21(6) (2011), 1207–1252. doi:10.1017/S0960129511000193.
[11] G. Barthe, B. Grégoire and V. Laporte, Secure compilation of side-channel countermeasures: The case of cryptographic“constant-time”, in: Proceedings of the 31st IEEE Computer Security Foundations Symposium (CSF 2018), IEEE Computer Society, 2018, pp. 328–343. doi:10.1109/CSF.2018.00031.
[12] N. Benton, Simple relational correctness proofs for static analyses and program transformations, in: Proceedings of the
31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2004), ACM, 2004, pp. 14–
25.
[13] A. Blot, M. Yamamoto and T. Terauchi, Compositional synthesis of leakage resilient programs, in: Proceedings of the
6th International Conference on Principles of Security and Trust (POST 2017), Lecture Notes in Computer Science,Vol. 10204, Springer, 2017, pp. 277–297. doi:10.1007/978-3-662-54455-6_13.
[14] M. Boreale and F. Pampaloni, Quantitative information flow under generic leakage functions and adaptive adversaries,
Logical Methods in Computer Science 11(4) (2015). doi:10.2168/LMCS-11(4:5)2015.
[15] M.R. Clarkson and F.B. Schneider, Hyperproperties, Journal of Computer Security 18(6) (2010), 1157–1210. doi:10.
3233/JCS-2009-0393.

T. Terauchi and T. Antonopoulos / Bucketing for timing attack mitigation

633[16] Y.G. Dantas, R. Gay, T. Hamann, H. Mantel and J. Schickel, An evaluation of bucketing in systems with non-deterministic
timing behavior, in: Proceedings of the 33rd IFIP TC 11 International Conference on ICT Systems Security and Privacy
Protection (Section 2018), IFIP Advances in Information and Communication Technology, Vol. 529, Springer, 2018,
pp. 323–338. doi:10.1007/978-3-319-99828-2_23.
[17] DARPA Space/Time Analysis for Cybersecurity (STAC) program, 2017.
[18] G. Doychev, B. Köpf, L. Mauborgne and J. Reineke, CacheAudit: A tool for the static analysis of cache side channels,
ACM Transactions on Information and System Security 18(1) (2015), 4:1–4:32. doi:10.1145/2756550.
[19] M. Eilers, P. Müller and S. Hitz, Modular product programs, in: Proceedings of the 27th European Symposium on Programming (ESOP 2018), Lecture Notes in Computer Science, Vol. 10801, Springer, 2018, pp. 502–529.
[20] H. Eldib and C. Wang, Synthesis of masking countermeasures against side channel attacks, in: Proceedings of the 28th
International Conference on Computer Aided Verification (CAV 2014), Lecture Notes in Computer Science, Vol. 8559,
Springer, 2014, pp. 114–130.
[21] K. Gandolfi, C. Mourtel and F. Olivier, Electromagnetic analysis: Concrete results, in: Proceedings of the 3rd International Workshop on Cryptographic Hardware and Embedded Systems (CHES 2001), Lecture Notes in Computer Science,Vol. 2162, Springer, 2001, pp. 251–261. doi:10.1007/3-540-44709-1_21.
[22] R. Gay, H. Mantel and H. Sudbrock, An empirical bandwidth analysis of interrupt-related covert channels, IJSSE 6(2)(2015), 1–22.
[23] J.A. Goguen and J. Meseguer, Security policies and security models, in: Proceedings of the 3rd IEEE Symposium on
Security and Privacy (S&P 1982), IEEE Computer Society, 1982, pp. 11–20. doi:10.1109/SP.1982.10014.
[24] D. Hedin and D. Sands, Timing aware information flow security for a JavaCard-like bytecode, in: Proceedings of the 1st
Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTE 2005), Electronic Notes in Theoretical Computer Science, Vol. 141, Elsevier, 2005, pp. 163–182.
[25] Y. Ishai, A. Sahai and D.A. Wagner, Private circuits: Securing hardware against probing attacks, in: Proceedings ofthe 23rd Annual International Cryptology Conference on Advances in Cryptology (CRYPTO 2003), Lecture Notes in
Computer Science, Vol. 2729, Springer, 2003, pp. 463–481. doi:10.1007/978-3-540-45146-4_27.
[26] N. Kobayashi and K. Shirane, Type-based information analysis for low-level languages, in: Proceedings of the 3rd Asian
Workshop on Programming Languages and Systems (APLAS 2002), 2002, pp. 302–316.
[27] P.C. Kocher, Timing Attacks on Implementations of Diffie-Hellman, RSA, DSS, and Other Systems, in: Proceedingsof the 16th Annual International Cryptology Conference on Advances in Cryptology (CRYPTO 1996), Lecture Notes in
Computer Science, Vol. 1109, Springer, 1996, pp. 104–113.
[28] P.C. Kocher, J. Jaffe and B. Jun, Differential power analysis, in: Proceedings of the 19th Annual International Cryptology
Conference on Advances in Cryptology (CRYPTO 1999), Lecture Notes in Computer Science, Vol. 1666, Springer, 1999,
pp. 388–397.
[29] B. Köpf and D.A. Basin, Automatically deriving information-theoretic bounds for adaptive side-channel attacks, Journalof Computer Security 19(1) (2011), 1–31. doi:10.3233/JCS-2009-0397.
[30] B. Köpf and M. Dürmuth, A provably secure and efficient countermeasure against timing attacks, in: Proceedings of the
22nd IEEE Computer Security Foundations Symposium (CSF 2009), IEEE Computer Society, 2009, pp. 324–335. doi:10.
1109/CSF.2009.21.
[31] B. Köpf and G. Smith, Vulnerability bounds and leakage resilience of blinded cryptography under timing attacks, in:Proceedings of the 23rd IEEE Computer Security Foundations Symposium (CSF 2010), IEEE Computer Society, 2010,
pp. 44–56. doi:10.1109/CSF.2010.11.
[32] P. Malacaria, Assessing security threats of looping constructs, in: Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2007), ACM, 2007, pp. 225–235.
[33] P. Malacaria, Algebraic foundations for quantitative information flow, Mathematical Structures in Computer Science 25(2)(2015), 404–428. doi:10.1017/S0960129513000649.
[34] A. McIver, C. Morgan, G. Smith, B. Espinoza and L. Meinicke, Abstract channels and their robust information-leakage
ordering, in: Proceedings of the 3rd International Conference on Principles of Security and Trust (POST 2014), 2014,
pp. 83–102. doi:10.1007/978-3-642-54792-8_5.
[35] C.S. Pasareanu, Q. Phan and P. Malacaria, Multi-run side-channel analysis using symbolic execution and max-SMT, in:Proceedings of the 29th IEEE Computer Security Foundations Symposium (CSF 2016), IEEE Computer Society, 2016,
pp. 387–400. doi:10.1109/CSF.2016.34.
[36] J. Quisquater and D. Samyde, ElectroMagnetic analysis (EMA): Measures and counter-measures for smart cards, in:Proceedings of the Smart Card Programming and Security, International Conference on Research in Smart Cards (ESmart 2001), Lecture Notes in Computer Science, Vol. 2140, Springer, 2001, pp. 200–210. doi:10.1007/3-540-454187_17.
[37] J.C. Reynolds, The Craft of Programming, Prentice Hall International Series in Computer Science, Prentice Hall, 1981.

634

T. Terauchi and T. Antonopoulos / Bucketing for timing attack mitigation[38] A. Sabelfeld and A.C. Myers, A model for delimited information release, in: Proceedings of the Software Security –Theories and Systems, Second Mext-NSF-JSPS International Symposium (ISSS 2003), Lecture Notes in Computer Science,Vol. 3233, Springer, 2003, pp. 174–191.
[39] G. Smith, On the foundations of quantitative information flow, in: Proceedings of the 12th International Conference onFoundations of Software Science and Computational Structures (FOSSACS 2009), Lecture Notes in Computer Science,Vol. 5504, Springer, 2009, pp. 288–302.
[40] M. Sousa and I. Dillig, Cartesian hoare logic for verifying k-safety properties, in: Proceedings of the 37th ACM SIGPLAN
Conference on Programming Language Design and Implementation (PLDI 2016), ACM, 2016, pp. 57–69. doi:10.1145/
2908080.2908092.
[41] J. Svenningsson and D. Sands, Specification and verification of side channel declassification, in: Proceedings of the
6th International Workshop on Formal Aspects in Security and Trust (FAST 2009), Lecture Notes in Computer Science,Vol. 5983, Springer, 2009, pp. 111–125. doi:10.1007/978-3-642-12459-4_9.
[42] T. Terauchi and A. Aiken, Secure information flow as a safety problem, in: Proceedings of the 12th International Symposium (SAS 2005), Lecture Notes in Computer Science, Vol. 3672, Springer, 2005, pp. 352–367.
[43] T. Terauchi and T. Antonopoulos, A formal analysis of timing channel security via bucketing, in: Proceedings of the
8th International Conference on Principles of Security and Trust (POST 2019), Lecture Notes in Computer Science,Vol. 11426, Springer, 2019, pp. 29–50. doi:10.1007/978-3-030-17138-4_2.
[44] T. Terauchi and T. Antonopoulos, A formal analysis of timing channel security via bucketing, http://www.f.waseda.jp/
terauchi.
[45] S. Tizpaz-Niari, P. Cerný and A. Trivedi, Quantitative mitigation of timing side channels, in: Proceedings of the 31st
International Conference on Computer Aided Verification (CAV 2019), 2019, pp. 140–160.
[46] E. Tromer, D.A. Osvik and A. Shamir, Efficient cache attacks on AES, and countermeasures, Journal of Cryptology 23(1)(2010), 37–71. doi:10.1007/s00145-009-9049-y.
[47] D.M. Volpano, C.E. Irvine and G. Smith, A sound type system for secure flow analysis, Journal of Computer Security
4(2/3) (1996), 167–188. doi:10.3233/JCS-1996-42-304.
[48] H. Yasuoka and T. Terauchi, Quantitative information flow – verification hardness and possibilities, in: Proceedings of the
23rd IEEE Computer Security Foundations Symposium (CSF 2010), IEEE Computer Society, 2010, pp. 15–27. doi:10.
1109/CSF.2010.9.
[49] H. Yasuoka and T. Terauchi, On bounding problems of quantitative information flow, Journal of Computer Security 19(6)(2011), 1029–1082. doi:10.3233/JCS-2011-0437.
[50] H. Yasuoka and T. Terauchi, Quantitative information flow as safety and liveness hyperproperties, Theoretical Compututer
Science 538 (2014), 167–182. doi:10.1016/j.tcs.2013.07.031.
[51] D. Zhang, A. Askarov and A.C. Myers, Language-based control and mitigation of timing channels, in: Proceedings of the
ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2012), ACM, 2012, pp. 99–
110.