A Formal Analysis of Timing Channel Security
via Bucketing
Tachio Terauchi1 and Timos Antonopoulos2
1

Waseda University, Tokyo, Japanterauchi@waseda.jp
2
Yale University, New Haven, U.S.A.
timos.antonopoulos@yale.edu

Abstract. This paper investigates the effect of bucketing in security
against timing channel attacks. Bucketing is a technique proposed 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 iseffective against timing-channel attacks. In this paper, we show that bucketing is 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 thatthe security of a system decreases only by a limited degree by allowing
timing-channel observations, whereas the second condition ensures thatthe system would satisfy the first condition when bucketing is appliedand 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 independently of concernsof side-channel information leakage, and certain conditions are placed on
the side channel to guarantee the security of the whole system. Further,
we show that the bucketing technique can be applied compositionally in
conjunction with the constant-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 areapplicable to any side channels and techniques that reduce the numberof possible observations on the channel.

1

Introduction

Side-channel attacks aim to recover a computer system’s secret information byobserving the target system’s side channels such as cache, power, timing andelectromagnetic radiation [23, 24, 17, 31, 21, 36, 25, 16, 15, 11]. They are well recognized as a serious threat to the security of computer systems. Timing-channel(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, 22, 20, 26, 7, 27, 41, 4, 18, 3, 30, 6, 9].

Bucketing is a technique proposed for mitigating timing attacks [26, 27, 7, 41,14]. It restricts the system’s outputs to only occur at designated 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 system’s
performance because outputs must be delayed to the next bucket time. Nonetheless, in comparison to the constant-time implementation technique [1, 22, 20, 3,
6, 9] 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 [26, 27].3 For example, bucketing
may be implemented in a blackbox-style by a monitor that buffers and delays
outputs [7, 41].
In this paper, we formally study the effect of bucketing on security against
adaptive timing attacks. To this end, first, we give a formal notion of security against adaptive side-channel-observing adversaries, called (f, ǫ)-security.
Roughly, (f, ǫ)-security says that the probability that an adversary 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 adaptive side-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 thata system is secure if there are sufficiently large subsets of secrets such that (1)the system’s side channel reveals no more information than the regular channelon the subsets and (2) the system is secure on the subsets against adversaries
who only observe the regular channel. The degree of security (i.e., f and ǫ) is
proportional to that against regular-channel-only-observing adversaries and thesize 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 (forgood f and ǫ). To this end, we present a condition, called low-input side-channel
non-interference (LISCNI). We show that applying bucketing to a system thatsatisfies the condition would result in a system that satisfies SRSCR. Therefore, LISCNI is a sufficient condition for security under the bucketing technique.
Roughly, LISCNI says that (1) the side-channel observation does not depend on
attacker-controlled inputs (but may depend on secrets) and (2) the system issecure against adversaries who only observe the regular channel. The degree of
security is proportional to that against regular-channel-only-observing adversaries and the granularity of buckets. A main benefit of the conditions SRSCR
and LISCNI is that they allow separation of concerns whereby the security of
the regular channel can be proven independently of concerns of side-channel
3

Sometimes, the terminology “constant-time implementation” is used to mean evenstricter requirements, such as requiring control flows to be secret independent [3, 9].
In this paper, we use the terminology for a more permissive notion in which only
the running time is required to be secret independent.

information leakage, and certain conditions are placed on the side channel toguarantee the security of the whole system.
Finally, we show that the bucketing technique can be applied in a compositional manner with the constant-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 LISCNI, the wholesystem can be made secure by applying bucketing only to the non-constant-time
part. We show that the combined approach is able to ensure security of some
non-constant-time systems that cannot be made secure by applying bucketing
to the whole system. We summarize the main contributions below.
– A formal notion of security against adaptive side-channel-observing adversaries, called (f, ǫ)-security. (Section 2)– A counterexample which shows that bucketing alone is insufficient for security against adaptive side-channel attacks. (Section 2.1)
– A condition SRSCR which guarantees (f, ǫ)-security. (Section 3.1)
– A condition LISCNI which guarantees that the system satisfying it becomes
one that satisfies SRSCR and therefore becomes (f, ǫ)-secure after suitablebucketing is applied. (Section 3.2)
– A compositional approach that combines bucketing and the constant-time
technique. (Section 3.3)
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 the compositional 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
side-channel observations
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 adaptiveside-channel attacks. We also show that bucketing is in general insufficient toguarantee security of systems against adaptive side-channel attacks. Section 3
presents sufficient conditions for ensuring (f, ǫ)-security: SRSCR and LISCNI. We
show that they facilitate proving the security of systems by allowing system designers to prove the security of regular channels separately from the concern ofside channels. We also show that the LISCNI condition may be used in combination with the constant-time implementation technique in a compositionalmanner so 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.

2

Security against Adaptive Side-Channel Attacks

Formally, a system (or, program) is a tuple (rc, sc, S, I, Orc , Osc ) where rc andsc 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. S is a security-parameter-indexed family of 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 andIn for the set of corresponding attacker-controlled inputs. Each indexed functionrcn (respectively scn ) is a function from Sn × In to Onrc (resp. Onsc ), where Orc
and Osc are indexed families of sets of possible 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 theattacker-controlled input v.4 For a system C = (rc, sc, S, I, Orc , Osc ), we often
write rchCi for rc, schCi for sc, ShCi for S, IhCi for I, Orc hCi for Orc , andOsc hCi for Osc . We often omit “hCi” when it is clear from the context.
For a system C and s ∈ Sn , we write Cn (s) for the oracle which, givenv ∈ 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 at most i oracle queries to Cn (s). We impose norestriction on how the adversary chooses the inputs to the oracle. Importantly,
he may choose the inputs based on the outputs of previous oracle queries. Suchan adversary is said to be adaptive [25].
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 andthe class of resource-unlimited randomized algorithms. The former is the standard for arguing the security of cryptography algorithms, and the latter ensuresinformation theoretic security. In what follows, unless specified otherwise, we assume that the computation class of adversaries is the class of resource-unlimited
randomized algorithms.
As standard, we define security as the bound on the probability that anadversary wins a certain game. Let f be a function from N to N. We define
Win A (n, f ) to be the event that the following game outputs true.
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 ofprobabilities is possible for the event Win A (n, f ). Now, we are ready to give thedefinition of (f, ǫ)-security.
4

We restrict to deterministic systems in this paper. Extension to probabilistic systems
is left for future work.

i = 0;while (i < n) {if (pass[i] != guess[i]) return false;i++;}return true;
Fig. 1. Timing insecure login program

Definition 1 ((f, ǫ)-security). Let f : N → N and ǫ : N → R be such that 0 <ǫ(n) ≤ 1 for all n ∈ N. We say that a system is (f, ǫ)-secure if there exists N ∈ Nsuch that for all adversaries A and n ≥ N , it holds that Pr[Win A (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 ofsuccess ǫ(n).
By abuse of notation, we often implicitly treat an expression e on the security
parameter n as the function λn∈N.e. Therefore, for example, (n, ǫ)-secure meansthat there is no attack that is able to recover secrets in n many queries with theprobability of success ǫ(n), and (f, 1)-secure means that there is no attack thatmakes 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 1 (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 secret and 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 of queries.
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 6= 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 timingchannel 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 arbitrary v1 ∈ In as the initial guess. By seeing the timing-channel
output scn (s, v1 ), he would be able to discover at least the first bit of s, s[0],because s[0] = v1 [0] if and only if scn (s, v1 ) > 0. Then, he picks an arbitraryv2 ∈ {0, 1}n satisfying v2 [0] = s[0], and by seeing the timing-channel output, hewould be able to discover at least up to the second bit of s. Repeating the process

n times, he will recover all n bits of 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.
N
Example 2 (Bucketed Leaky Login). Next, we consider the security of the program from Example 1 but with bucketing applied. Here, we assume a constantnumber of buckets, k, such that the program returns its output at time intervals
i · n/k for i ∈ {j ∈ N | j ≤ k}.5 (For simplicity, we assume that n is divisible byk.) The bucketed program can be formalized as the system where– rc, sc, I, Orc are as in Example 1;– 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 thatthe system is not constant-time for any k > 1. Nonetheless, we can show that−1
forthe system is (f, ǫ)-secure where f (n) = 2n/k − (N + 1) and ǫ(n) = 1 − N
2n/kn/kany 1 ≤ N < 2 . Note that as k approaches 1 (and hence the system becomes
constant-time), f approaches 2n − (N + 1) and ǫ approaches 1 − N2−1
n , whichmatch the security bound of the ideal login program that only leaks whether
the input guess matched the password or not. We will show that the approachpresented in Section 3.1 can be used to derive such a bound.
N
2.1

Insufficiency of Bucketing

We show that bucketing is in general insufficient to guarantee the security of systems against adaptive side-channel attacks. In fact, we show that bucketing witheven just two buckets is insufficient. (Two is the minimum 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, ourresult applies to any side channels, and it shows that there are systems with justtwo possible side-channel outputs and completely secure (i.e., non-interferent [19,37]) regular channel that is efficiently attackable by side-channel-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 side channel sc has just two possible outputs. The sidechannel, 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 each5

A similar analysis can be done for any strictly sub-linear number of buckets.

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.
We remark that the above attack is not adaptive. Therefore, the counterexample actually shows that bucketing can be made ineffective by just allowing
multiple non-adaptive side-channel observations. We also remark that the counterexample shows that some previously proposed measures are insufficient. For
example, the capacity measure [28, 33, 5, 39] would not be able to detect the vulnerability of the example, because the measure is equivalent to the log of thenumber of possible outputs for deterministic systems.

3

Sufficient Conditions for Security against Adaptive
Side-Channel Attacks

In this section, we present conditions that guarantee the security of systems
against adaptive side-channel-observing adversaries. The condition SRSCR presented in Section 3.1 guarantees that systems that satisfy it are secure, whereas
the condition LISCNI 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 regularchannels from those of side channels. In addition, we show in Section 3.3 that the
LISCNI condition may be used in combination with constant-time implementation techniques in a compositional manner so as to prove the security of systems
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 subsets of secrets S ′ ⊆ P(Sn ) such thatfor each S ′′ ∈ S ′ , the secrets are difficult for an adversary to recover by only
observing the regular channel, and that the side channel reveals no more information than the regular channel for those sets of secrets. Then, because S ′ islarge, the entire system is also ensured to be secure with high probability. We
adopt refinement order [38, 29], which had been studied in quantitative information flow research, to formalize the notion of “reveals no more information”.
Roughly, a channel C1 is said to be a refinement of a channel C2 if, for every
attacker-controlled input, every pair of secrets that C2 can distinguish can also
be distinguished by C1 .
We write O• for the indexed family of sets such that On• = {•} for all n ∈ N.
Also, we write sc• for the indexed family of functions such that sc•n (s, v) = • forall n ∈ N and (s, v) ∈ Sn ×In . For C = (rc, sc, S, I, Orc , Osc ), we write C • for thesystem (rc, sc• , S, I, Orc , O• ). We define the notion of regular-channel security.

Definition 2 (Regular-channel (f, ǫ)-security). We say that the C is regularchannel (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.
Let us fix a system C = (rc, sc, S, I, Orc , Osc ). For an indexed family of setsof sets of secrets S ′ (i.e., Sn′ ⊆ P(Sn ) for each n), we write S ′′ ≺ S ′ when S ′′is an indexed family of sets of secrets such that Sn′′ ∈ Sn′ for each n. Note thatsuch S ′′ satisfies Sn′′ ⊆ Sn for each n. Also, for S ′′ ≺ S ′ , we write C|S ′′ for thesystem that is equal to C except that its secrets are restricted to S ′′ , that is,(rc, sc, S ′′ , I, Orc , Osc ). For a set of sets X, we say that X is mutually disjoint if
for all S1 ∈ X and S2 ∈ X, S1 ∩S2 = ∅. Next, we formalize the SRSCR condition.
Definition 3 (Secret-Restricted Side-Channel Refinement). Let f : N →N, ǫ : N → (0, 1], and 0 < r ≤ 1. We say that the system C = (rc, sc, S, I, Orc , Osc )satisfies the secret-restricted side-channel refinement condition with f , ǫ, and r,
written SRSCR(f, ǫ, r), if there exists an indexed family of sets of sets of secrets
S res such that Snres is mutually disjoint and Snres ⊆ P(Sn ) for all n ∈ N, and:S
(1) For all n ∈ N, r ≤ | Snres |/|Sn |;(2) For all S ′′ ≺ S res , C|S ′′ is regular-channel (f, ǫ)-secure; and(3) For all n ∈ N, S ∈ Snres , v ∈ In and s1 , s2 ∈ S, it holds that scn (s1 , v) 6=
scn (s2 , v) ⇒ rcn (s1 , v) 6= rcn (s2 , v).
Condition (2) says that the system is regular-channel (f, ǫ)-secure when restricted to any subset of secrets S ′′ ≺ S res . Condition (3) says that the system’s side channel reveals no more information than its regular channel for the
restricted secret subsets. Condition (1) says that the ratio of the restricted set
over the entire space of secrets is at least r.6
We informally describe why SRSCR is a sufficient condition for security. The
condition guarantees that, for the restricted secrets S res , the attacker gains noadditional information by observing the side-channel compared to what he already knew by observing the regular channel. Then, because r is a bound on
the probability that a randomly selected secret falls in S res , the system is secureprovided that r is suitably large and the system is regular-channel secure. The
theorem below formalizes the above intuition.
Theorem 1 (SRSCR Soundness). Suppose C satisfies SRSCR(f, ǫ, r). Then,
C is (f, ǫ′ )-secure, where ǫ′ = 1 − r(1 − ǫ).
Proof. Let S res be an indexed family of sets of secret subsets that satisfies conditions (1), (2), and (3) of SRSCR(f, ǫ, r). By condition (2), for all sufficiently
large n and adversaries A, Pr[Win•,res(n, f )] < ǫ(n) where Win•,res(n, f ) is theAAmodified game in which the oracle oracle Cn (s) always outputs•
as its sideS
channel output and the secret s is selected randomly from Snres (rather thanfrom Sn ).
6

It is easy to relax the notion to be asymptotic so that the conditions need to hold
only for n ≥ N for some N ∈ N.

any n, the probability that a randomly selectedSelement from Sn is in
S For
Snres is at least r by condition (1). That is, Pr[s ∈ Snres | s ← Sn ] ≥ r.
Also, Pr[¬Win•,res(n, f )] > 1 − ǫ(n) (for sufficiently large n) for any A by theAargument above. Therefore, by condition (3), for sufficiently large n,Pr[¬Win A (n, f )] ≥ Pr[s ∈ Snres | s ←[Sn ] · Pr[¬Win•,res(n, f )] > r · (1 − ǫ(n))
A

Therefore, Pr[Win A (n, f )] < 1 − r(1 − ǫ(n)) for sufficiently large n.

⊓⊔

As a special case where the ratio r is 1, Theorem 1 implies that if a system
satisfies SRSCR(f, ǫ, 1) then it is (f, ǫ)-secure.
Example 3. Recall the bucketed leaky login program from Example 2. We showthat the program satisfies the SRSCR condition. For each n, a ∈ {0, 1}n , and0 ≤ i < k, let Sna,i ⊆ Sn be the set of secrets whose sub-bits from i · n/k to(i + 1) · n/k − 1 may differ but the remaining n − n/k bits are a (and thereforesame). 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 + 1) · n/k, . . . , n − 1]}
Let S res be the indexed family of sets of sets of secrets such that Snres =a,i{Sn | a ∈ {0, 1}n } for some i. Then, the system satisfies conditions (1), (2),−1
and (3) of SRSCR(f, ǫ, r) with r = 1, f (n) = 2n/k − (N + 1), and ǫ = 1 − N
2n/kS
for any 1 ≤ N < 2n/k . Note that (1) is satisfied with r = 1 because Sn = Snres ,and (2) is satisfied because |Sna,i | = 2n/k and (f, ǫ) matches the security of then/kideal login program without side channels for the set of secrets of size 2 . To
see why (3) is satisfied, note that for any v ∈ In and s ∈ Sna,i , scn (s, v) = i
if s 6= v, and scn (s, v) = k if s = v. Hence, for any v ∈ In and s1 , s2 ∈ Sna,i ,scn (s1 , v) 6= scn (s2 , v) ⇒ rcn (s1 , v) 6= rcn (s2 , v). Therefore, by Theorem 1, it
follows that bucketed leaky login program is (f, ǫ)-secure. Note that the boundmatches the one given in Example 2.
N
To effectively apply Theorem 1, one needs to find suitable subsets of secrets
S res on which the system’s regular channel is (f, ǫ)-secure and the side channel
satisfies the refinement relation with respect to the regular channel. As also
observed in prior works [38, 29], the refinement relation is a 2-safety property [35,13] for which there are a number of effective verification methods [32, 10, 34, 2,
6]. For instance, self-composition [35, 8, 4, 3] is a well-known technique that canbe used to verify arbitrary 2-safety properties.
We note that a main benefit of Theorem 1 is separation of concerns whereby
the security of regular channel can be proven independently of side channels, andthe conditions required for side channels can be checked separately. For instance,a system designer may prove the regular-channel (f, ǫ)-security by an elaborate
manual reasoning, while the side-channel conditions are checked, possibly automatically, by established program verification methods such as self composition.

Remarks. We make some additional observations regarding the SRSCR condition. First, while Theorem 1 derives a sound security bound, the bound may
not be the tightest one. Indeed, when the adversary’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
only showed that it is (2n/k − 2, 1)-secure. That is, there is a factor k gap in thebounds. Intuitively, the gap occurs for the example because the buckets partitiona 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 theblocks. Extending the technique to enable tighter analyses is left for future work.
Secondly, the statement of Theorem 1 says that when regular channel of thesystem is (f, ǫ)-secure for certain subsets of secrets, then the whole system is(f, ǫ′ )-secure under certain conditions. This may give an impression that only
the adversary-success probability parameter (i.e., ǫ) of (f, ǫ)-security is affectedby the additional consideration of side channels, leaving the number of oracle
queries parameter (i.e., f ) unaffected. However, as also seen in Example 2, thetwo parameters are often correlated so that smaller f implies smaller ǫ andvice versa. Therefore, Theorem 1 suggests that the change in the probability
parameter (i.e., from ǫ to ǫ′ ) may need to be compensated by a change in the
degree of security with respect to the number of oracle queries.
Finally, condition (2) of SRSCR stipulates that the regular channel is (f, ǫ)secure for each restricted family of sets of secrets S ′′ ≺ S res rather than theentire space of secrets S. In general, a system 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 S ′′ ≺ S res used in the analysis of Example 3, it is only (2n/k − 2, 1)secure. That is, there is an implicit correlation between the sizes of the restrictedsubsets and the degree of regular-channel security. Therefore, finding S res suchthat each S ′′ ∈ Snres is large and satisfies theSconditions is important for deriving
good security bounds, even when the ratio | Snres |/|Sn | is large as in the analysisof the bucketed leaky login program.
3.2

Low-Input Side-Channel Non-Interference Condition

While SRSCR facilitates proving security of systems by separating regular channels from side channels, it requires one to identify suitable subsets of secrets S res
that satisfy the conditions. This can be a hurdle to applying the proof method.
To this end, this section presents a condition, called low-input side-channel noninterference (LISCNI), which guarantees that a system satisfying it becomes secure after applying bucketing (or other techniques) to reduce the number ofside-channel outputs. Unlike SRSCR, the condition does not require identifying secret subsets. Roughly, the condition stipulates that the regular channel
is secure (for the entire space of secrets) and that the side-channel outputs are
independent of attacker-controlled inputs.

We show that the system satisfying the condition becomes a system satisfying
SRSCR once bucketing is applied, where the degree of security (i.e., the parameters f , ǫ, r of SRSCR) will be proportional to the degree of regular-channel
security and the granularity of buckets. Roughly, this holds because for a system
whose side-channel outputs are independent of attacker-controlled inputs, bucketing is guaranteed to partition the secrets into a small number of sets (relative
to the bucket granularity) such that for each of the sets, the side channel cannot
distinguish the secrets in the set, and the regular-channel security transfers to acertain degree to the case when the secrets are restricted to the ones in the set.
As we shall show next, while the condition is not permissive enough to provesecurity of the leaky login program (cf. Examples 1, 2 and 3), it covers interesting
scenarios such as fast modular exponentiation (cf. Example 4). Also, as we shallshow in Section 3.3, the condition may be used compositionally in combination
with the constant-time implementation technique [1, 22, 3, 9] to further widen its
applicability.
Definition 4 (Low-Input Side-Channel Non-Interference). Let f : N →N and ǫ : N → (0, 1]. We say that the system C satisfies the low-input sidechannel non-interference condition with f and ǫ, written LISCNI(f, ǫ), if thefollowing conditions are satisfied:(1) C is regular-channel (f, ǫ)-secure; and(2) For all n ∈ N, s ∈ Sn , and v1 , v2 ∈ In , it holds that scn (s, v1 ) = scn (s, v2 ).
Condition (2) says that the side-channel outputs are independent of low inputs(i.e., attacker-controlled inputs). We note that this is non-interference with respect to low inputs, whereas the usual notion of non-interference says that theoutputs are independent of high inputs (i.e., secrets) [19, 37].7
The LISCNI condition ensures the security of systems after bucketing is applied. We next formalize the notion of “applying bucketing”.
Definition 5 (Bucketing). Let C be a system and k ∈ N such that k > 0.
The system C after k-bucketing is applied, written Bkt k (C), is a system C ′ thatsatisfies the following:(1) rchC ′ i = rchCi, ShC ′ i = ShCi, IhC ′ i = IhCi, and Orc hC ′ i = Orc hCi;
(2) For all n ∈ N, Osc hC ′ in = {⋆1 , . . . , ⋆k } where ⋆i 6= ⋆j for each i 6= j; and(3) For all n ∈ N, s1 , s2 ∈ Sn and v1 , v2 ∈ In , schCin (s1 , v1 ) = schCin (s2 , v2 ) ⇒schC ′ in (s1 , v2 ) = schC ′ in (s2 , v2 ).
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 LISCNI only requires thefact that side channel outputs are partitioned into a small number of buckets.
7

As with SRSCR, it is easy to relax the notion to be asymptotic so that condition (2)only needs to hold for large n.

This makes our results applicable to any techniques (beyond the usual bucketing technique for timing channels [26, 27, 7, 41, 14]) that reduce the number ofpossible side-channel outputs.
Below states that a system satisfying the LISCNI condition becomes one thatsatisfies the SRSCR condition after suitable bucketing is applied.
Theorem 2 (LISCNI Soundness). Suppose that C satisfies LISCNI(f, ǫ). Let
k > 0 be such that k · ǫ ≤ 1. Then, Bkt k (C) satisfies SRSCR(f, k · ǫ, 1/k).
Proof. Let C ′ = Bkt k (C). By condition (2) of k-bucketing and condition (2) of
LISCNI(f, ǫ), we have that for all n ∈ N, s ∈ Sn and v1 , v2 ∈ In , schC ′ in (s, v1 ) =schC ′ in (s, v2 ). Therefore, by k-bucketing, there must be an indexed family ofsets of secrets S ′ such that for all n, (a) Sn′ ⊆ Sn , (b) |Sn′ | ≥ |Sn |/k, and (c) forall s1 , s2 ∈ Sn′ and v1 , v2 ∈ In , schC ′ in (s1 , v1 ) = schC ′ in (s2 , v2 ). Note that such
S ′ can be found by, for each n, choosing a bucket into which a maximal numberof secrets fall. We define an indexed family of sets of sets of secrets S res to besuch that Snres is the singleton set {Sn′ } for each n.
We show that C ′ satisfies conditions (1), (2), and (3) of SRSCR(f, k · ǫ, 1/k)with the restricted secret subsets S res defined above. Firstly, (1) is satisfied
because |Sn′ | ≥ |Sn |/k. Also, (3) is satisfied because of property (c) above (i.e.,the side channel is non-interferent for the subset).
It remains to show that (2) is satisfied. That is, C ′ |S ′ is regular-channel(f, k · ǫ)-secure. For contradiction, suppose that C ′ |S ′ is not regular-channel(f, k · ǫ)-secure, that is, there exists a regular-channel attack A that queries (theregular channel of) C ′ |S ′ at most f (n) many times and successfully recovers thesecret with probability at least k · ǫ(n). Then, we can construct a regular-channel
adversary for C which simply runs A (on any secret from Sn ). Note that theadversary makes at most f (n) many queries. We argue that the probability thatthe adversary succeeds in recovering the secret is at least ǫ. That is, we showthat Pr[Win•A (n, f )] ≥ ǫ(n) (for sufficiently large n) where Win•A (n, f ) is themodified game in which the oracle always outputs • as its side-channel output.
To see this, note that the probability that a secret randomly selected from
Sn is in Sn′ is at least 1/k, that is, Pr[s ∈ Sn′ | s ← Sn ] ≥ 1/k. Also, A’s regularchannel attack succeeds with probability at least k · ǫ given a randomly chosen(n, f )] ≥ k · ǫ(n) where Win•,res(n, f ) is thesecret from Sn′ , that is, Pr[Win•,res
A
A
modified game in which the oracle always outputs • as its side-channel output
and the secret is selected randomly from Sn′ (rather than from Sn ). Therefore,
for sufficiently large n, we have:
Pr[Win•A (n, f )] ≥ Pr[s ∈ Sn′ | s ← Sn ] · Pr[Win•,res(n, f )] ≥ 1/k · (k · ǫ(n)) = ǫ(n)AThis contradicts condition (1) of LISCNI(f, ǫ) which says that C is regular⊓⊔
channel (f, ǫ)-secure. Therefore, C ′ |S ′ is regular-channel (f, k · ǫ)-secure.
As a corollary of Theorems 1 and 2, we have the following.
Corollary 1. Suppose that C satisfies LISCNI(f, ǫ). Let k > 0 be such that k·ǫ ≤1. Then, Bkt k (C) is (f, ǫ′ )-secure where ǫ′ = 1 − 1/k + ǫ.

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

Note that as k approaches 1 (and hence the system becomes constant-time),
the security bound of Bkt k (C) approaches (f, ǫ), matching the regular-channel
security of C. As with Theorem 1, Theorem 2 may give an impression thatthe conditions only affect the adversary-success probability parameter (i.e., ǫ)of (f, ǫ)-security, leaving the number of queries parameter (i.e., f ) unaffected.
However, as also remarked in Section 3.1, the two parameters are often correlated
so that a change in one can affect the other. Also, like SRSCR, LISCNI separates
the concerns regarding regular channels from those 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.
Example 4 (Fast Modular Exponentiation). Fast modular exponentiation is anoperation that is often found in cryptography algorithms such as RSA [23,30]. Fig. 2 shows its implementation written in a C-like language. It computesyx mod m where x is the secret represented as a length n bit array and y is anattacker controlled-input. The program is not constant-time (assuming that thenand else branches in the loop have different running times), and effective timing
attacks have been proposed for the program [23, 30].
However, assuming that running time of the operation (a * y) % m is independent of y, it can be seen that the program satisfies the LISCNI condition.8
Under the assumption, the program can be formalized 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).
8This is admittedly an optimistic assumption. Indeed, proposed timing attacks exploit
the fact that the running time of the operation can depend on y [23, 30]. 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).

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 assumptionthat inverting modular exponentiation is hard, one can show that C satisfies
LISCNI(f, ǫ) for any f and negligible ǫ. This follows because the side-channel
outputs are independent of low inputs, and the regular-channel is (f, ǫ)-secure
for any f and negligible ǫ under the assumption.9 Therefore, it can be made(f, 1 − 1/k + ǫ)-secure for any f and negligible ǫ by applying bucketing.
N
Remarks. We make some additional observations regarding the LISCNI condition. First, similar to condition (3) of SRSCR, the low-input independence
condition of LISCNI (condition (2)) is a 2-safety property and is amenable tovarious verification methods proposed for the class of properties. In fact, because the condition is essentially side-channel non-interference but with respect
to low inputs instead of high inputs, it can be checked by the methods for checking ordinary side-channel non-interference by reversing the roles of high inputs
and low inputs [1, 20, 3, 6, 9].
Secondly, we note that the leaky login program from Example 1 does notsatisfy LISCNI. This is because the program’s side channel is not non-interferent
with respect to low inputs. Indeed, given any secret s ∈ Sn , one can vary therunning times by choosing low inputs v, v ′ ∈ In with differing lengths of matching prefixes, that is, (argmaxi s↾i = v↾i ) 6= (argmaxi s↾i = v ′ ↾i ). Nevertheless, as
we have shown in Examples 2 and 3, the program becomes secure once bucketing
is applied. In fact, it becomes one that satisfies SRSCR as shown in Example 3.
Ideally, we would like to find a relatively simple condition (on systems before
bucketing is applied) that covers many systems that would become secure by
applying bucketing. However, finding such a condition that covers a system likethe leaky login program may be non-trivial. Indeed, predicting that the leaky
login program become secure after applying bucketing appears to require more
subtle analysis of interaction between low inputs and high inputs. (In fact, it
can be shown that arbitrarily partitioning the side-channel outputs to a small
number of buckets does not ensure security for this program.) Extending thetechnique to cover such scenarios is left for future work.
3.3

Combining Bucketing and Constant-Time Implementation
Compositionally

We show that the LISCNI condition may be applied compositionally with theconstant-time implementation technique (technically, we will only apply the condition (2) of LISCNI compositionally). As we shall show next, the combined approach is able to ensure security of some non-constant-time systems that cannot
9

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 forthis system is negligible (under the computational hardness assumption). Therefore,a similar analysis can be done for any sub-polynomial number of buckets.

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.

be made sure 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 thissection are more specialized to the case of timing channels. First, we formalize
the notion of constant-time implementation.
Definition 6 (Constant-Time). Let f : N → N and ǫ : N → (0, 1]. We saythat a system C satisfies the constant-time condition (or, timing-channel noninterference) with f and ǫ, written CT(f, ǫ), if the following 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).
Note that CT requires that the side channel is non-interferent (with respect tosecrets). The following theorem is immediate from the definition, and states that
CT is a sufficient condition for security.
Theorem 3 (CT Soundness). If C satisfies CT(f, ǫ), then C is (f, ǫ)-secure.
To motivate the combined application of CT and LISCNI, let us consider thefollowing example which is neither constant-time nor can be made secure by(globally) applying bucketing.
Example 5. Fig. 3 shows a simple, albeit contrived, program that we will use
to motivate the combined approach. Here, sec is a n-bit secret and inp is an-bit attacker-controlled input. Both sec and inp are interpreted as unsigned
n-bit integers where − and > are the usual unsigned integer subtraction andcomparison operations. The regular channel always outputs true and hence is
non-interferent. Therefore, only the timing channel is of concern.
The program can be formalized as 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 the system 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 LISCNI(f, ǫ) for any fand ǫ either, because its side-channel outputs are not independent of low inputs.
In fact, we can show that arbitrarily applying bucketing (globally) to the systemdoes not guarantee security. To see this, let us consider applying bucketing withjust two buckets whereby the buckets partition the possible 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– rchC ′ i, ShC ′ i, IhC ′ i, and Orc hC ′ i are same as those of Ccomp ;– For all n ∈ N, Osc hC ′ in = {0, 1}; and– For all n ∈ N and (s, v) ∈ Sn × In , schC ′ in (s, v) = 0 if s + v ≤ 2n , andschC ′ in (s, v) = 1 otherwise.
We show that there exists an efficient adaptive attack against C ′ . Let s ∈Sn . The adversary A recovers s by only making linearly many queries via thefollowing process. First, A queries with the input v1 = 2n−1 . By observing theside-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 theformer 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 the process in a binary searchmanner 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 forany ǫ.
N
Next, we present the compositional bucketing approach. Roughly, our compositionality theorem (Theorem 4) states that the sequential composition of aconstant-time system with a system whose side channel is non-interferent withrespect to low inputs can be made secure by applying bucketing to only the
non-constant-time component. As with LISCNI, the degree of security of thecomposed system is relative to the that of the regular channel and the granularity of buckets.
To state the compositionality theorem, we explicitly separate the conditions
on side channels of CT and LISCNI 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
LISCNIsc if it satisfies condition (2) of LISCNI, that is, for all n ∈ N, s ∈ Sn ,and v1 , v2 ∈ In , scn (s, v1 ) = scn (s, v2 ). Next, we define sequential compositionof systems.
Definition 7 (Sequential Composition). Let C † and C ‡ be systems suchthat ShC † i = ShC ‡ i, IhC † i = IhC ‡ i, and for all n ∈ N, Osc hC ‡ in ⊆ N and
Osc hC ‡ in ⊆ N. The sequential composition of C † with C ‡ , written C † ; C ‡ , is thesystem C such that

– ShCi = S(C † ) and IhCi = I(C † ); and– For all n ∈ N and (s, v) ∈ Sn ×In , schC ′ in (s, v) = schC † in (s, v)+schC ‡ in (s, v).
We note that the definition of sequential composition specifically targets thecase when the side channel is a timing channel, and says that the side-channels
outputs are numeric values and that the side-channel output of the composedsystem is the sum of those of the components. Also, the definition leaves thecomposition of regular channels open, and allows the regular channel of thecomposed system to be any function from Sn × In . We are now ready to state
the compositionality theorem.
Theorem 4 (Compositionality). Let C † be a system that satisfies LISCNIsc
and C ‡ be a system that satisfies CTsc . Suppose that Bkt k (C † ); C ‡ is regularchannel (f, ǫ)-secure where k · ǫ ≤ 1. Then, Bkt k (C † ); C ‡ is (f, ǫ′ )-secure, whereǫ′ = 1 − 1/k + ǫ.
Proof. By Theorem 1, it suffices to show that Bkt k (C † ); C ‡ satisfies SRSCR(f, k ·ǫ, 1/k). By an argument similar to the proof of Theorem 2, there must be anindexed family of sets of secrets S ′ such that, for all n ∈ N, (a) Sn′ ⊆ Sn , (b)|Sn′ | ≥ |Sn |/k, and (c) for all s1 , s2 ∈ Sn′ and v1 , v2 ∈ In , schBkt k (C † )in (s1 , v1 ) =schBkt k (C † )in (s2 , v2 ). We define an indexed family of sets of sets of secrets S res
to be such that Snres is the singleton set {Sn′ } for each n.
We show that C = Bkt k (C † ); C ‡ satisfies conditions (1), (2), and (3) of
SRSCR(f, k · ǫ, 1/k) with the restricted secret subsets S res defined above. Firstly,(1) is satisfied because |Sn′ | ≥ |Sn |/k. Also, because Bkt k (C † ); C ‡ is regularchannel (f, ǫ)-secure, we can show that (2) is satisfied by an argument similar
to the one in the proof of Theorem 2.
It remains to show that (3) is satisfied. It suffices to show that for all n ∈ N,v ∈ In , and s1 , s2 ∈ Sn′ , schCin (s1 , v) = schCin (s2 , v). That is, the side channelof the composed system is non-interferent (with respect to high inputs) for thesubset S ′ . By the definition of the sequential composition, for all v ∈ In ands ∈ Sn , schCin (s, v) = schBkt k (C † )in (s, v) + schC ‡ in (s, v). Therefore, for allv ∈ In and s1 , s2 ∈ Sn′ ,schCin (s1 , v) = schBkt k (C † )in (s1 , v) + schC ‡ in (s1 , v)
= schBkt k (C † )in (s2 , v) + sc(C ‡ )n (s2 , v)
= schCin (s2 , v)
because schC ‡ in (s1 , v) = schC ‡ in (s2 , v) by CTsc of C ‡ , and schBkt k (C † )in (s1 , v) =schBkt k (C † )in (s2 , v) by (c) above.
⊓⊔
We note that the notion of sequential composition is symmetric. Therefore,
Theorem 4 implies that the composing the components in the reverse order, that
is, C ‡ ; Bkt k (C † ), is also secure provided that its regular channel is secure.
The compositionality theorem suggests the following compositional approachto ensuring security. Given a system C that is a sequential composition of acomponent whose side channel outputs are independent of high inputs (i.e.,
satisfies CTsc ) and a component whose side channel outputs are independent oflow inputs (i.e., satisfies LISCNIsc ), we can ensure the security of C by proving its
regular-channel security and applying bucketing only to the non-constant-timecomponent.
Example 6. Let us apply compositional bucketing to the system Ccomp from Example 5. 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 the following:– S and I are as in Ccomp ;– For all n ∈ N, Osc hC † in = Osc hC ‡ in = {i ∈ N | i ≤ 2n }; and– For all n ∈ N and (s, v) ∈ Sn × In , schC † in (s, v) = s and schC ‡ in (s, v) = v.
Note that C ‡ satisfies CTsc as its side-channel outputs are high-input independent, and, C † satisfies LISCNIsc as its side-channel outputs are low-input
independent. By applying bucketing only to the component C † , we obtain thesystem Bkt k (C † ); C ‡ . The regular-channel of Bkt k (C † ); C ‡ (i.e., that of Ccomp ) is(f, ǫ)-secure for any f and negligible ǫ because it is non-interferent (with respect
to high inputs) and the probability that an adversary may recover a secret forsuch a system is at most 1/|Sn |.10 Therefore, by Theorem 4, Bkt k (C † ); C ‡ is(f, 1 − 1/k + ǫ)-secure for any f and negligible ǫ.
N
The above example shows that compositional bucketing can be used to ensure security of non-constant-time systems that cannot be made secure by awhole-system bucketing. It is interesting to observe that the constant-time condition, CTsc , requires the side-channel outputs to be independent of high inputs
but allows dependency on low inputs, while LISCNIsc is the dual and says thatthe side-channel outputs are independent of low inputs but may depend on highinputs. Our compositionality theorem (Theorem 4) states that a system consisting of such parts can be made secure by applying bucketing only to the partthat satisfies the latter condition.
It is easy to see that sequentially composing components that satisfy CTsc
results in a system that satisfies CTsc , and likewise, sequentially composing components that satisfy LISCNIsc results in a system that satisfies LISCNIsc . 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.

4

Related WorkAs remarked in Section 1, much research has been done on defending against
timing attacks and more generally side channel attacks. For instance, there have
10

Therefore, a similar analysis can be done for any strictly sub-exponential number ofbuckets.

been experimental evaluation on the effectiveness of bucketing and other timingchannel mitigation schemes [18, 14], and other works have proposed informationtheoretic methods for formally analyzing the security of (deterministic and probabilistic) systems against adaptive adversaries [25, 12].
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 Köpf et al. [26, 27] who investigated the effect ofbucketing applied to blinded cryptography algorithms. They show that applying
bucketing to a blinded cryptography algorithm whose regular channel is INDCCA2 secure results in an algorithm that is IND-CCA2 secure against timingchannel-observing adversaries. In addition, they show bounds on information
leaked by such bucketed blinded cryptography algorithms in terms of quantitative information flow [28, 33, 5, 39, 40]. By contrast, we analyze the effect ofapplying bucketing to general systems, show that bucketing is in general insufficient against adaptive adversaries, and present novel conditions that guarantee
security against such adversaries. Also, our results are given in 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, 22, 20, 3, 6, 9]. The previous works
have proposed methods for verifying that the given system is constant-time [20,3, 6, 9] or transforming it to one that is constant-time [1, 22]. As we have also
discussed in this paper (cf. Theorem 3), it is easy to see that the constant-time
condition directly transfers the regular-channel-only security to the security forthe case with timing channels. By contrast, security implied by bucketing isless straightforward. In this paper, we have shown that bucketing is in general insufficient to guarantee the security of systems even when their regularchannel is perfectly secure. And, we have presented results that show that, under certain conditions, the regular-channel-only security can be transferred tothe side-channel-observing case to certain degrees. Because there are advantagesof bucketing such as efficiency and ease of implementation [26, 27, 7, 41, 14], we
hope that our results will contribute to a better understanding of the bucketing
technique and foster further research on the topic.

5

Conclusion and Future WorkIn this paper, we have presented a formal analysis of the effectiveness of thebucketing technique against adaptive timing-channel-observing adversaries. We
have shown that bucketing is in general insufficient against such adversaries,
and presented two novel conditions, SRSCR and LISCNI, that guarantee security against such adversaries. SRSCR states that a system that satisfies it issecure, whereas LISCNI states that the a system that satisfies it becomes secure when bucketing is applied. We have shown that both conditions facilitate
proving the security of systems against adaptive side-channel-observing adver-saries by allowing a system designer to prove the security of the system’s regularchannel separately from the concerns of its side-channel behavior. By doing so,
the security of the regular-channel is transferred, to certain degrees, to the fullside-channel-aware security. We have also shown that the LISCNI condition canbe used in conjunction with the constant-time implementation technique in acompositional manner to further increase its applicability. We have formalized
our results via the notion of (f, ǫ)-security, which gives precise bounds on thenumber of queries needed by adaptive adversaries to recover secrets.
While we have instantiated our results to timing channel and bucketing, manyof the results are actually quite general and are applicable to side channels otherthan timing channels. Specifically, aside from the compositional bucketing resultthat exploits the “additive” nature of timing channels, the results are applicable
to any side channels and techniques that reduce the number of possible sidechannel observations.
As future work, we would like to extend our results to probabilistic systems.
Currently, our results are limited to deterministic systems, and such an extension
would be needed to assess the effect of bucketing when it is used together withcountermeasure techniques that involve randomization. We would also like toimprove the conditions and the security bounds thereof to be able to better
analyze systems such as the leaky login program shown in Examples 1, 2 and 3.
Finally, we would like to extend the applicability of the compositional bucketing
technique by considering more patterns of compositions, such as sequentiallycomposing components that themselves have been made secure by compositional
bucketing.
Acknowledgements. We thank the anonymous reviewers for useful comments.
This work was supported by JSPS KAKENHI Grant Numbers 17H01720 and
18K19787, JSPS Core-to-Core Program, A.Advanced Research Networks, JSPS
Bilateral Collaboration Research, and Office of Naval Research (ONR) award#N00014-17-1-2787.

References
1. J. Agat. Transforming out timing leaks. In POPL, 2000.
2. A. Aguirre, G. Barthe, M. Gaboardi, D. Garg, and P. Strub. A relational logic forhigher-order programs. PACMPL, 1(ICFP), 2017.
3. J. B. Almeida, M. Barbosa, G. Barthe, F. Dupressoir, and M. Emmi. Verifying
constant-time implementations. In USENIX Security Symposium, 2016.
4. J. B. Almeida, M. Barbosa, J. S. Pinto, and B. Vieira. Formal verification ofside-channel countermeasures using self-composition. Science of Compututer Programming, 78(7), 2013.
5. M. S. Alvim, K. Chatzikokolakis, C. Palamidessi, and G. Smith. Measuring information leakage using generalized gain functions. In CSF, 2012.
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 PLDI, 2017.

7. A. Askarov, D. Zhang, and A. C. Myers. Predictive black-box mitigation of timing
channels. In CCS, 2010.
8. G. Barthe, P. R. D’Argenio, and T. Rezk. Secure information flow by selfcomposition. Mathematical Structures in Computer Science, 21(6), 2011.
9. G. Barthe, B. Grégoire, and V. Laporte. Secure compilation of side-channel countermeasures: The case of cryptographic ”constant-time”. In CSF, 2018.
10. N. Benton. Simple relational correctness proofs for static analyses and programtransformations. In POPL, 2004.
11. A. Blot, M. Yamamoto, and T. Terauchi. Compositional synthesis of leakage resilient programs. In POST, 2017.
12. M. Boreale and F. Pampaloni. Quantitative information flow under generic leakage
functions and adaptive adversaries. Logical Methods in Computer Science, 11(4),2015.
13. M. R. Clarkson and F. B. Schneider. Hyperproperties. Journal of Computer
Security, 18(6), 2010.
14. Y. G. Dantas, R. Gay, T. Hamann, H. Mantel, and J. Schickel. An evaluationof bucketing in systems with non-deterministic timing behavior. In ICT Systems
Security and Privacy Protection, 2018.
15. G. Doychev, B. Köpf, L. Mauborgne, and J. Reineke. Cacheaudit: A tool forthe static analysis of cache side channels. ACM Transactions on Information and
System Security, 18(1), 2015.
16. H. Eldib and C. Wang. Synthesis of masking countermeasures against side channel
attacks. In CAV, 2014.
17. K. Gandolfi, C. Mourtel, and F. Olivier. Electromagnetic analysis: Concrete results.
In CHES, 2001.
18. R. Gay, H. Mantel, and H. Sudbrock. An empirical bandwidth analysis of interruptrelated covert channels. IJSSE, 6(2), 2015.
19. J. A. Goguen and J. Meseguer. Security policies and security models. In IEEE
Symposium on Security and Privacy, 1982.
20. D. Hedin and D. Sands. Timing aware information flow security for a JavaCard-like
bytecode. 2005.
21. Y. Ishai, A. Sahai, and D. A. Wagner. Private circuits: Securing hardware againstprobing attacks. In CRYPTO, 2003.
22. N. Kobayashi and K. Shirane. Type-based information analysis for low-level languages. In APLAS, 2002.
23. P. C. Kocher. Timing attacks on implementations of Diffie-Hellman, RSA, DSS,
and other systems. In CRYPTO, 1996.
24. P. C. Kocher, J. Jaffe, and B. Jun. Differential power analysis. In CRYPTO, 1999.
25. B. Köpf and D. A. Basin. Automatically deriving information-theoretic bounds foradaptive side-channel attacks. Journal of Computer Security, 19(1), 2011.
26. B. Köpf and M. Dürmuth. A provably secure and efficient countermeasure against
timing attacks. In CSF, 2009.
27. B. Köpf and G. Smith. Vulnerability bounds and leakage resilience of blinded
cryptography under timing attacks. In CSF, 2010.
28. P. Malacaria. Assessing security threats of looping constructs. In POPL, 2007.
29. P. Malacaria. Algebraic foundations for quantitative information flow. Mathematical Structures in Computer Science, 25(2), 2015.
30. C. S. Pasareanu, Q. Phan, and P. Malacaria. Multi-run side-channel analysis using
symbolic execution and max-SMT. In CSF, 2016.

31. J. Quisquater and D. Samyde. Electromagnetic analysis (EMA): measures andcounter-measures for smart cards. In Smart Card Programming and Security, International Conference on Research in Smart Cards, E-Smart, 2001.
32. J. C. Reynolds. The Craft of Programming. Prentice Hall International series incomputer science. Prentice Hall, 1981.
33. G. Smith. On the foundations of quantitative information flow. In FOSSACS,
2009.
34. M. Sousa and I. Dillig. Cartesian Hoare logic for verifying k-safety properties. In
PLDI, 2016.
35. T. Terauchi and A. Aiken. Secure information flow as a safety problem. In SAS,2005.
36. E. Tromer, D. A. Osvik, and A. Shamir. Efficient cache attacks on AES, andcountermeasures. Journal of Cryptology, 23(1), 2010.
37. 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.
38. H. Yasuoka and T. Terauchi. Quantitative information flow - verification hardness
and possibilities. In CSF, 2010.
39. H. Yasuoka and T. Terauchi. On bounding problems of quantitative information
flow. Journal of Computer Security, 19(6), 2011.
40. H. Yasuoka and T. Terauchi. Quantitative information flow as safety and livenesshyperproperties. Theoretical Compututer Science, 538, 2014.
41. D. Zhang, A. Askarov, and A. C. Myers. Language-based control and mitigationof timing channels. In PLDI, 2012.