Bucketing and information flow analysis for provable timing attack mitigation

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 is effective 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 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 independently of concerns of 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 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. 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,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 and security-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 performance because outputs must be delayed to the next bucket time. Nonetheless, in comparison to the constant-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

¹
Sometimes, the terminology “constant-time implementation” is used to mean even stricter requirements, such as requiring control 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.

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 clear that 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 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 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 the regular 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 a system 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-channel-only-observing adversaries, the degree of attacker-controlled-input influence on the side channel, and the 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 concerns of 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 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 is $BLISCC$ , the whole system 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 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 $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 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.

Our results make use of ideas from (quantitative) information flow research such as refinement order relation [33,34,38,48] and channel capacity [5,9,32,39,48,49]. It is interesting to note that we use the ideas 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, for example, 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 that bucketing 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 that they 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 manner 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.

A preliminary version of this paper appeared in [43]. The present paper substantially improves that version 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:

$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 to every 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).

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 is restricted to 1 (Definition 3.8 in Section 3.2).

The extensions (1) and (2) together improve the $BLISCC$ ( $LISCNI$ in [43]) soundness theorem and the 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).

An additional example demonstrating the usefulness of the $BLISCC$ condition is added (Example 3.14).

An extended analysis of the leaky login program is added. The analysis shows a limitation with the permissive definition of bucketing that is used in this paper (and in [43]) (Example 3.15 in Section 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 derivation of the strong bounds.

2. Security against adaptive side-channel attacks

Formally, a system (or, program) is a tuple $(rc, sc, S, I, O^{rc}, O^{sc})$ 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 family of sets of secrets (or, high inputs) and $I$ is a security-parameter-indexed family of sets of attacker-controlled inputs (or, low inputs). A security parameter is a natural number that represents the size of secrets, and we write $S_{n}$ for the set of secrets of size n and $I_{n}$ for the set of corresponding attacker-controlled inputs. We assume that each $S_{n}$ and $I_{n}$ are finite. Each indexed function ${rc}_{n}$ (respectively ${sc}_{n}$ ) is a function from $S_{n} \times I_{n}$ to $O_{n}^{rc}$ (resp. $O_{n}^{sc}$ ), where $O^{rc}$ and $O^{sc}$ are indexed families of sets of possible regular-channel and side-channel outputs, respectively. For $(s, v) \in S_{n} \times I_{n}$ , we write ${rc}_{n} (s, v)$ (resp. ${sc}_{n} (s, v)$ ) for the regular-channel (resp. side-channel) output given the secret s and the attacker-controlled input v.2

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

For a system

C = (rc, sc, S, I, O^{rc}, O^{sc})

, we often write

rc ⟨ C ⟩

for

rc

sc ⟨ C ⟩

for

sc

S ⟨ C ⟩

for

S

I ⟨ C ⟩

for

I

O^{rc} ⟨ C ⟩

for

O^{rc}

, and

O^{sc} ⟨ C ⟩

for

O^{sc}

. We often omit the parameter C when it is clear from the context.

For a system C and $s \in S_{n}$ , we write $C_{n} (s)$ for the oracle which, given $v \in I_{n}$ , returns a pair of outputs $(o_{1}, o_{2}) \in O_{n}^{rc} \times O_{n}^{sc}$ such that ${rc}_{n} (s, v) = o_{1}$ and ${sc}_{n} (s, v) = o_{2}$ . 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 \in N$ , we write $A^{C_{n} (s)} (i)$ for the adversary $A$ that makes at most i oracle queries to $C_{n} (s)$ . We impose no restriction on how the adversary chooses the inputs to the oracle. 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 the standard 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 of adversaries is the class of resource-unlimited randomized algorithms.

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 ${Win}_{A}^{C} (n, f)$ to be the event that the following game outputs true. $\begin{array}{l} s \leftarrow S_{n} \\ s^{'} \leftarrow A^{C_{n} (s)} (f (n)) \\ Output s = s^{'} \end{array}$ Here, the first line selects s uniformly at random from $S_{n}$ . 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 ${Win}_{A}^{C} (n, f)$ . Now, we are ready to give the definition of $(f, ϵ)$ -security.

Definition 2.1 (

(f, ϵ)

-security).

Let $f : N \to N$ and $ϵ : N \to R$ be such that $0 < ϵ (n) ⩽ 1$ for all $n \in N$ . We say that a system C is $(f, ϵ)$ -secure if there exists $N \in N$ such that for all adversaries $A$ and $n ⩾ N$ , it holds that $Pr [{Win}_{A}^{C} (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 our previous works [7,43] and it also corresponds closely to the definition used in the DARPA STAC program [17].3

³
A slight difference is that the definition in [7] is not asymptotic, i.e., it asserts $Pr [{Win}_{A}^{C} (n, f)]$ for all n. The relaxed definition in this paper facilitates derivations of asymptotic bounds.

By abuse of notation, we often implicitly treat an expression e on the security parameter n as the function $λ n \in N . e$ . Therefore, for example, $(n, ϵ)$ -secure means that there is no attack that is able to recover 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 abuse of 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 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.

Fig. 1.

Timing insecure login program.

We formalize the program as the system C where for all $n \in N$ ,

$S_{n} = I_{n} = {0, 1}^{n}$ ;

$O_{n}^{rc} = {true, false}$ and $O_{n}^{sc} = {i \in N ∣ i ⩽ n}$ ;

For all $(s, v) \in S_{n} \times I_{n}$ , ${rc}_{n} (s, v) = true$ if $s = v$ and ${rc}_{n} (s, v) = false$ if $s \neq v$ ; and

For all $(s, v) \in S_{n} \times I_{n}$ , ${sc}_{n} (s, v) = {argmax}_{i} 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 \in S_{n}$ , the adversary $A^{C_{n} (s)} (n)$ efficiently recovers s as follows. He picks an arbitrary $v_{1} \in I_{n}$ as the initial guess. By seeing the timing-channel output ${sc}_{n} (s, v_{1})$ , he would be able to discover at least the first bit of s, $s [0]$ , because $s [0] = v_{1} [0]$ if and only if ${sc}_{n} (s, v_{1}) > 0$ . Then, he picks an arbitrary $v_{2} \in {0, 1}^{n}$ satisfying $v_{2} [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 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.

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 \cdot n / k$ for natural $i ⩽ k$ .4

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

For simplicity, we assume that n is divisible by k. The bucketed program can be formalized as the system where

$rc$ , $sc$ , $I$ , $O^{rc}$ are as in Example 2.2;

For all $n \in N$ , $O_{n}^{sc} = {i \in N ∣ i ⩽ k}$ ; and

For all $n \in N$ and $(s, v) \in S_{n} \times I_{n}$ , ${sc}_{n} (s, v) = bkt ({argmax}_{i} s ↾_{i} = v ↾_{i}, n / k)$

where

bkt (i, j)

is the smallest

a \in N

such that

i ⩽ a \cdot j

. It is easy to see that the system is not constant-time for any

k > 1

. Nonetheless, with the analysis method that we will present in Section 3.1, we can show that the system is

(f, ϵ)

-secure where

f (n) = 2^{n / k} - (N + 1)

and

ϵ (n) = 1 - \frac{N - 1}{2^{n / k}}

for any

1 ⩽ N < 2^{n / k}

(cf. Example 3.5). Note that as k approaches 1 (and hence the system becomes constant-time), f approaches

2^{n} - (N + 1)

and ϵ approaches

1 - \frac{N - 1}{2^{n}}

, which match the security bound of the ideal login program that only leaks whether the input guess matched the password or not.5

⁵

Roughly, the bound for the ideal login program follows from the fact that the probability of guessing an element in a set of size M in X tries is $X / M + (1 - X / M) (1 / (M - X))$ and letting $X = 2^{n} - N$ and $M = 2^{n}$ . We refer to [7] for a method for formally deriving such a bound.

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 $2^{n / k} - 2$ . Typically, a larger ϵ implies a larger f and vice versa. Such a correlation is expected as requiring the attacker to succeed with a higher probability by making ϵ 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 in terms of the change in the f and ϵ parameters. As we shall show, the statements of the theorems say that only the ϵ parameter is affected, possibly giving a false impression that bucketing only affects the probability 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 adaptive side-channel attacks. In fact, we show that bucketing with even 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, our result applies to any side channels, and it shows that there are systems with just two possible side-channel outputs and completely secure (i.e., non-interferent [23,47]) regular channel that is efficiently attackable by side-channel-observing adversaries.

Consider the system such that, for all $n \in N$ ,

$S_{n} = {0, 1}^{n}$ and $I_{n} = {i \in N ∣ i ⩽ n}$ ;

$O_{n}^{rc} = {∙}$ and $O_{n}^{sc} = {0, 1}$ ;

For all $(s, v) \in S_{n} \times I_{n}$ , ${rc}_{n} (s, v) = ∙$ ; and

For all $(s, v) \in S_{n} \times I_{n}$ , ${sc}_{n} (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 side channel, given an attacker-controlled input

v \in I_{n}

, reveals the v-th bit of s. It is easy to see that the system is linearly attackable. That is, for any secret

s \in S_{n}

, 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 high probability with only a small amount of queries. This is in contrast to the bucketed leaky login program from Example 2.3 which, while still leaking information through the side channel, is secure in the sense that any attack that recovers the secret with a high probability must make an exponential number of queries. 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, the counterexample actually shows that bucketing can be made ineffective by just allowing multiple non-adaptive side-channel observations.

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 $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 side channels. 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 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 disjoint subsets of secrets $S^{'} \subseteq P (S_{n})$ such that for each $S^{″} \in 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, the entire 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 $c_{1}$ is said to be a refinement of a channel $c_{2}$ if, for every attacker-controlled input, every pair of secrets that $c_{2}$ can distinguish can also be distinguished by $c_{1}$ .

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 $O_{n}^{∙} = {∙}$ for all $n \in N$ . Also, we write ${sc}^{∙}$ for the indexed family of functions such that ${sc}_{n}^{∙} (s, v) = ∙$ for all $n \in N$ and $(s, v) \in S_{n} \times I_{n}$ . For $C = (rc, sc, S, I, O^{rc}, O^{sc})$ , we write $C^{∙}$ for the system $(rc, {sc}^{∙}, S, I, O^{rc}, 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 \in R ∣ 0 < a ⩽ 1}$ . Let us fix a system $C = (rc, sc, S, I, O^{rc}, O^{sc})$ . We call X a secret restriction of $S$ when (1) X is an indexed family such that $X_{n} \subseteq P (S_{n}) \times (0, 1]$ for each $n \in N$ and (2) for each $n \in N$ , $(S_{1}, p_{1}) \in X_{n}$ and $(S_{2}, p_{2}) \in X_{n}$ , $(S_{1}, p_{1}) \neq (S_{2}, p_{2})$ implies $S_{1} \cap S_{2} = \emptyset$ . 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 $U_{n} \in X_{n}$ for each n. Note that such U satisfies $U_{n} \in P (S_{n}) \times (0, 1]$ for each n. For an indexed family of sets of secrets T such that $T_{n} \subseteq S_{n}$ for each $n \in N$ , we write $C |_{T}$ for the system $(rc, sc, T, I, O^{rc}, O^{sc})$ . We write $C |_{U}$ for $C |_{#_{1} U}$ , and write ${err}_{U}$ for the function from $N$ to $(0, 1]$ such that ${err}_{U} (n) = {(#_{2} U)}_{n}$ for each n. Here, ${(#_{1} U)}_{n} = #_{1} (U_{n})$ and ${(#_{2} U)}_{n} = #_{2} (U_{n})$ for each n. Roughly, ${err}_{U}$ is the error bound function stipulated by U.

Refinement order relation. Let us fix a system $C = (rc, sc, S, I, O^{rc}, O^{sc})$ . Let T be an indexed family of sets of secrets such that $T_{n} \subseteq S_{n}$ for each $n \in N$ . We say that C satisfies the side-channel refinement order relation condition on the secrets T, written $RR (T)$ , if for all $n \in N$ , $s_{1} \in T_{n}$ , $s_{2} \in T_{n}$ and $v \in I_{n}$ , it holds that ${sc}_{n} (s_{1}, v) \neq {sc}_{n} (s_{2}, v) \Rightarrow {rc}_{n} (s_{1}, v) \neq {rc}_{n} (s_{2}, v)$ . Roughly, $RR (T)$ says that the system’s side channel reveals no more information than its regular-channel on the secrets T. We formalize the intuition in Lemma 3.2.

Lemma 3.1.
Let T be an indexed family of sets of secrets such that $T_{n} \subseteq S_{n}$ for each $n \in N$ . Suppose that C satisfies $RR (T)$ . Then, for any $n \in N$ , $o^{rc} \in O_{n}^{rc}$ and $v \in I_{n}$ , there exists $o^{sc} \in O_{n}^{sc}$ such that for any $s \in T_{n}$ , ${rc}_{n} (s, v) = o^{rc} \Rightarrow {sc}_{n} (s, v) = o^{sc}$ .
Proof.
Let $o^{rc} \in O_{n}^{rc}$ , $v \in I_{n}$ and $s \in T_{n}$ be such that ${rc}_{n} (s, v) = o^{rc}$ . Let $o^{sc} = {sc}_{n} (s, v)$ . Then, by $RR (T)$ , for any $s^{'} \in T_{n}$ such that ${rc}_{n} (s^{'}, v) = o^{rc}$ , we have ${sc}_{n} (s^{'}, v) = o^{sc}$ . □
Lemma 3.2.
Let T be an indexed family of sets of secrets such that $T_{n} \subseteq S_{n}$ for each $n \in N$ . Suppose that 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 that ${Win}_{A}^{C |_{T}} (n, f) > ϵ (n)$ for infinitely many $n \in N$ . We prove the lemma by constructing a (regular-channel) adversary $A^{'}$ such that $Pr [{Win}_{A^{'}}^{C |_{T}^{∙}} (n, f)] > ϵ (n)$ for infinitely many $n \in N$ .

We construct such $A^{'}$ by letting it simulate $A$ . Fix $n \in N$ . By $RR (T)$ and Lemma 3.1, for any $o^{rc} \in O_{n}^{rc}$ and $v \in I_{n}$ , there exists $o^{sc} \in O_{n}^{sc}$ such that for any $s \in T_{n}$ , ${rc}_{n} (s, v) = o^{rc} \Rightarrow {sc}_{n} (s, v) = o^{sc}$ . Let ${cor}_{n} : O_{n}^{rc} \times I_{n} \to O_{n}^{sc}$ be the mapping where ${cor}_{n} (o^{rc}, v)$ is such $o^{sc}$ , for each $o^{rc} \in O_{n}^{rc}$ and $v \in I_{n}$ . Then, $A^{'}$ works by running $A$ but hijacking its process whenever it makes a query to the system. That is, whenever $A$ attempts to query the system with an input $v \in I_{n}$ , $A^{'}$ sends the query to the regular-channel-only system to obtain the regular-channel output $o^{rc} = rc (s, v)$ and communicates back to $A$ the regular-and-side-channel output $(o^{rc}, {cor}_{n} (o^{rc}, v))$ . It is easy to see that $A^{'}$ and $A$ behave in exactly the same manner on secrets from $T_{n}$ . Therefore, $Pr {Win}_{A^{'}}^{C |_{T}^{∙}} (n, f)] > ϵ (n)$ for infinitely many $n \in N$ . □

We are now ready to formally state the $SRSCR$ condition.
Definition 3.3 ( $SRSCR$ ).

Let $C = (rc, sc, S, I, O^{rc}, O^{sc})$ . Let $f : N \to N$ and X be a secret restriction of $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

For all $U ≺ X$ , $C |_{U}$ is regular-channel $(f, {err}_{U})$ -secure; and

For all $U ≺ X$ , $RR (#_{1} U)$ holds.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.

We informally describe why $SRSCR$ is a sufficient condition for security. Let $(S, p) \in X_{n}$ . 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 case when 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 to recover the secret is bounded below by $\frac{| S |}{| S_{n} |} (1 - p)$ . Then, since the secret subsets in $X_{n}$ are disjoint (i.e., $(S_{1}, p_{1}) \neq (S_{2}, p_{2})$ implies $S_{1} \cap S_{2} = \emptyset$ for any $(S_{1}, p_{1}) \in X_{n}$ and $(S_{2}, p_{2}) \in X_{n}$ ), the attack must fail with the probability at least $\sum_{(S, p) \in X_{n}} \frac{| S |}{| S_{n} |} (1 - p)$ . The theorem below formalizes the intuition.

Theorem 3.4 (

SRSCR

soundness).

Suppose C satisfies $SRSCR (f, X)$ . Then, C is $(f, ϵ)$ -secure where $ϵ : N \to (0, 1]$ is any function satisfying the condition below:

There exists $N \in N$ such that for all $n ⩾ N$ , $1 - \sum_{(S, p) \in X_{n}} \frac{| 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 [{Win}_{A}^{C} (n, f)] ⩾ ϵ (n)$ for infinitely many $n \in N$ . To prove the theorem, it suffices to construct an adversary $A^{'}$ and $U ≺ X$ such that $Pr [{Win}_{A^{'}}^{C |_{U}^{∙}} (n, f)] ⩾ {err}_{U} (n)$ for infinitely many $n \in 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-channel observations. That is, it suffices to construct $A^{'}$ and U such that $Pr [{Win}_{A^{'}}^{C |_{U}} (n, f)] ⩾ {err}_{U} (n)$ for infinitely many $n \in N$ . By condition (♠), there exists $N \in N$ such that $1 - \sum_{(S, p) \in X_{n}} \frac{| S |}{| S_{n} |} (1 - p) ⩽ ϵ (n)$ for all $n ⩾ N$ (♢). Let $Y = {n \in N ∣ n ⩾ N \land Pr [{Win}_{A}^{C} (n, f)] ⩾ ϵ (n)}$ . Note that Y is an infinite set. Fix $n \in Y$ . For $S \subseteq S_{n}$ , let us write ${Win}_{\cdot}^{C |_{S}} (n, \cdot)$ for the winning event of the modified game in which the space of secrets (of size n) is S. Note that, given $S \subseteq S_{n}$ , the probability that a secret randomly selected from $S_{n}$ belongs to S is $| S | / | S_{n} |$ , that is, $Pr [s \in S ∣ s \leftarrow S_{n}] = | S | / | S_{n} |$ . Therefore, by disjointness of the secret subsets in $X_{n}$ , it follows that $\begin{matrix} Pr [{Win}_{A}^{C} (n, f)] & ⩽ 1 - \sum_{(S,_) \in X_{n}} Pr [s \in S ∣ s \leftarrow S_{n}] \cdot (1 - Pr [{Win}_{A}^{C |_{S}} (n, f)]) \\ = 1 - \sum_{(S,_) \in X_{n}} \frac{| S |}{| S_{n} |} \cdot (1 - Pr [{Win}_{A}^{C |_{S}} (n, f)]) . \end{matrix}$ Then, because $Pr [{Win}_{A}^{C} (n, f)] ⩾ ϵ (n)$ , from (♢) above, we have that $\begin{matrix} 1 - \sum_{(S, p) \in X_{n}} \frac{| S |}{| S_{n} |} (1 - p) ⩽ ϵ (n) ⩽ Pr [{Win}_{A}^{C} (n, f)] ⩽ 1 - \sum_{(S,_) \in X_{n}} \frac{| S |}{| S_{n} |} \cdot (1 - Pr [{Win}_{A}^{C |_{S}} (n, f)]), \end{matrix}$ and thus $\begin{matrix} \sum_{(S, p) \in X_{n}} \frac{| S |}{| S_{n} |} (1 - p) ⩾ \sum_{(S,_) \in X_{n}} \frac{| S |}{| S_{n} |} \cdot (1 - Pr [{Win}_{A}^{C |_{S}} (n, f)]) . \end{matrix}$ Therefore there must be $(S^{'}, p^{'}) \in X_{n}$ such that $p^{'} ⩽ Pr [{Win}_{A}^{C_{S^{'}}} (n, f)]$ . Denote by $S_{n}^{res}$ any such $S^{'}$ , for each $n \in Y$ . Let $U ≺ X$ be such that $#_{1} U_{n} = S_{n}^{res}$ for each $n \in Y$ ( $U_{n}$ is allowed to be an arbitrary element of $X_{n}$ for $n \notin Y$ ), and let $A^{'} = A$ . Then, it follows that $Pr [{Win}_{A^{'}}^{C |_{U}} (n, f)] ⩾ {err}_{U} (n)$ for each $n \in Y$ . □

We remark about a restricted case of the $SRSCR$ soundness theorem. Let X be a secret restriction and suppose that there exist $ϵ : N \to (0, 1]$ and $r \in (0, 1]$ satisfying the following: for all $n \in N$ , $p = ϵ (n)$ for all $(_, p) \in X_{n}$ and $\frac{| ⋃_{(S,_) \in X_{n}} S |}{| S_{n} |} ⩽ r$ . Then, Theorem 3.4 implies that a system satisfying $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 because the improved $SRSCR$ condition allows assignments of different error bounds to different secret subsets, 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 program satisfies the $SRSCR$ condition. For each $n \in N$ , $a \in {0, 1}^{n - n / k}$ , and $0 ⩽ i < k$ , let $S_{n}^{a, i} \subseteq S_{n}$ be the set of secrets whose sub-bits from $i \cdot n / k$ to $(i + 1) \cdot n / k - 1$ may differ but the remaining $n - n / k$ bits are as in a (and therefore same). That is, $\begin{matrix} S_{n}^{a, i} & = {s \in S_{n} ∣ s [0, \dots, i \cdot n / k - 1] = a [0, \dots, i \cdot n / k - 1] \\ and s [(i + 1) \cdot n / k, \dots, n - 1] = a [i \cdot n / k, \dots, n - n / k - 1]}, \end{matrix}$ where $s [m, \dots, m^{'}]$ and $a [m, \dots, m^{'}]$ , for $m > m^{'}$ , are arrays with no elements and in which case $s [m, \dots, m^{'}] = a [m, \dots, m^{'}]$ . Fix some $i \in {0, \dots, k - 1}$ and $N \in {1, \dots, 2^{n / k} - 1}$ . Recall $ϵ : N \to (0, 1]$ such that $ϵ (n) = 1 - \frac{N - 1}{2^{n / k}}$ from Example 2.3. Let X be an indexed family such that $X_{n} = {(S_{n}^{a, i}, ϵ (n)) ∣ a \in {0, 1}^{n - n / k}}$ for each $n \in N$ . Note that X is a secret restriction for the system because $S_{n}^{a, i} \cap S_{n}^{a^{'}, i} = \emptyset$ for any $a \neq a^{'}$ . Also, $⋃_{S \in X_{n}} S = S_{n}$ for each n.

Recall f such that $f (n) = 2^{n / k} - (N + 1)$ from Example 2.3. We argue that the system satisfies $SRSCR (f, X)$ . We note that condition (1) is satisfied because $| S_{n}^{a, i} | = 2^{n / k}$ and $(f, ϵ)$ matches the security of the ideal login program without side channels for the set of secrets of size $2^{n / k}$ .7
⁷
The latter follows by an argument similar to the one given in footnote 5 in Example 2.3.

To see why condition (2) is satisfied, note that for any $v \in I_{n}$ and $s \in S_{n}^{a, i}$ , ${sc}_{n} (s, v) = i$ if $s \neq v$ , and ${sc}_{n} (s, v) = k$ if $s = v$ . Hence, for any $v \in I_{n}$ and $s_{1}, s_{2} \in S_{n}^{a, i}$ , ${sc}_{n} (s_{1}, v) \neq {sc}_{n} (s_{2}, v) \Rightarrow {rc}_{n} (s_{1}, v) \neq {rc}_{n} (s_{2}, v)$ . Therefore, by Theorem 3.4, it follows that bucketed leaky login program is $(f, ϵ)$ -secure. Note that the bound 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 regular channel can be proven independently of side channels, and the 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 (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 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 (2^{n / k} - 2), 1)$ -secure, whereas the bound derived in Example 3.5 only showed that it is $(2^{n / k} - 2, 1)$ -secure. That is, there is a factor k gap in the bounds. Intuitively, the gap 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 \in {0, \dots, k - 1}$ to construct the restriction X). Extending the technique to enable tighter 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, {err}_{U})$ -secure when the secrets are restricted to the indexed family of subsets of secrets $#_{1} U$ for each $U ≺ X$ , then the whole system is $(f, ϵ)$ -secure under certain conditions for some ϵ determined by the parameter 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 of oracle 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 ${err}_{U}$ to ϵ) may need to be compensated by 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, {err}_{U})$ -secure for each restricted indexed family of subsets of secrets $#_{1} U$ rather than the entire 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 $(2^{n} - 2, 1)$ -secure, but when restricted to each $U ≺ X$ used in the analysis of Example 3.5, it is only $(2^{n / 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 such that each $U \in X$ is large and satisfies the conditions is important for deriving good security bounds, even when the ratio $| ⋃_{S \in X_{n}} S | / | S_{n} |$ 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 low-input 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 that the regular channel is secure (for the entire space of secrets) and that the side-channel outputs depend on 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], which measures 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 is applied, where the degree of security (i.e., the parameters f and X of $SRSCR$ ) will be proportional to the degree 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.

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 used compositionally 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 $\sim \subseteq A \times A$ , we write $A / \sim$ for the set of equivalence classes of A. That is, $A / \sim = {{[a]}_{\sim} ∣ a \in A}$ where ${[a]}_{\sim} = {x \in A ∣ x \sim a}$ . For a system C and $n \in N$ , we say that $v_{1} \in I_{n}$ and $v_{2} \in I_{n}$ are low-input side-channel equivalent, written $v_{1} \sim_{n}^{lisc} v_{2}$ , if ${sc}_{n} (s, v_{1}) = {sc}_{n} (s, v_{2})$ for all $s \in S_{n}$ . It is easy to see that $\sim_{n}^{lisc}$ is an equivalence relation on $I_{n}$ .

Definition 3.7 ( $LISCC$ ).

We define the low-input side-channel capacity of C for $n \in N$ , $LISCC (C, n)$ , as follows: $LISCC (C, n) = | I_{n} / \sim_{n}^{lisc} |$ .

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

⁸
In QIF literature, channel capacity is typically defined to be the log of the number of equivalence classes. Here, we use the non-log form which turns out to be more convenient for our purposes.

That is, while the standard channel capacity measures the amount of influence that the high inputs exert on the channel 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 is the standard definition of (side-channel) non-interference [23,47] with the roles of high inputs and low inputs reversed: for all $n \in N$ , $v_{1} \in I_{n}$ , $v_{2} \in I_{n}$ and $s \in S_{n}$ , ${sc}_{n} (s, v_{1}) = {sc}_{n} (s, v_{2})$ .

We now define the bounded low-input side-channel capacity condition.

Definition 3.8 (

BLISCC

Let $f : N \to N$ , $ϵ : N \to (0, 1]$ , and $ℓ \in N$ . We say that the system C satisfies the bounded low-input side-channel capacity condition with f, ϵ and ℓ, written $BLISCC (f, ϵ, ℓ)$ , if the following conditions are satisfied:

C is regular-channel $(f, ϵ)$ -secure; and

For all $n \in N$ , $LISCC (C, n) ⩽ ℓ$ .9

⁹
It is easy to relax the notion to be asymptotic so that channel capacity only needs to be bounded for large n.

We remark that, when $ℓ = 1$ , $BLISCC (f, ϵ, ℓ)$ implies that the side channel is low-input non-interferent. 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 \in N$ such that $k > 0$ . The system C after k-bucketing is applied, written ${Bkt}_{k} (C)$ , is a system $C^{'}$ that satisfies the following:

$rc ⟨ C^{'} ⟩ = rc ⟨ C ⟩$ , $S ⟨ C^{'} ⟩ = S ⟨ C ⟩$ , $I ⟨ C^{'} ⟩ = I ⟨ C ⟩$ , and $O^{rc} ⟨ C^{'} ⟩ = O^{rc} ⟨ C ⟩$ ;

For all $n \in N$ , $O^{sc} {⟨ C^{'} ⟩}_{n} = {⋆_{1}, \dots, ⋆_{k}}$ where $⋆_{i} \neq ⋆_{j}$ for each $i \neq j$ ; and

For all $n \in N$ , $s_{1}, s_{2} \in S_{n}$ and $v_{1}, v_{2} \in I_{n}$ , $sc {⟨ C ⟩}_{n} (s_{1}, v_{1}) = sc {⟨ C ⟩}_{n} (s_{2}, v_{2}) \Rightarrow sc {⟨ C^{'} ⟩}_{n} (s_{1}, v_{2}) = sc {⟨ C^{'} ⟩}_{n} (s_{2}, v_{2})$ .

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 that $LISCC (C, n) ⩽ ℓ$ implies that $LISCC ({Bkt}_{k} (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 \in N$ , and $ℓ ⩾ 1$ . Then, $LISCC (C, n) ⩽ ℓ$ if and only if there exist $I^{1}, \dots, I^{ℓ}$ such that the following conditions hold:
$I_{n} = ⋃_{i = 1}^{ℓ} I^{i}$ , and $I^{i} \cap I^{j} = \emptyset$ for $i \neq j$ ; and

For each $i \in {1, \dots, ℓ}$ , $s \in S_{n}$ , $v_{1} \in I^{i}$ and $v_{2} \in I^{i}$ , ${sc}_{n} (s, v_{1}) = {sc}_{n} (s, v_{2})$ .

Proof.
We show the if direction. We have that $| I_{n} / \sim_{n}^{lisc} | ⩽ ℓ$ . Therefore, we can construct $I^{1}, \dots, I^{ℓ}$ satisfying (a) and (b) by letting $I^{1}, \dots, I^{m}$ be the elements of $I_{n} / \sim_{n}^{lisc}$ , and $I^{i} = \emptyset$ for each $m < i ⩽ ℓ$ where $m = | I_{n} / \sim_{n}^{lisc} |$ .

We show the only-if direction. Let $I^{1}, \dots, I^{ℓ}$ satisfy (a) and (b). For each $I^{i} \in {I^{1}, \dots, I^{ℓ}}$ , there must be an equivalence class ${[v]}_{\sim_{n}^{lisc}} \in I_{n} / \sim_{n}^{lisc}$ such that $I^{i} \subseteq {[v]}_{\sim_{n}^{lisc}}$ . Let us choose one such ${[v]}_{\sim_{n}^{lisc}}$ and identify it by ${[v_{i}]}_{\sim_{n}^{lisc}}$ , for each $I^{i} \in {I^{1}, \dots, I^{ℓ}}$ . Then, ${{[v_{i}]}_{\sim_{n}^{lisc}} ∣ i \in {1, \dots, ℓ}}$ is the set of equivalence classes $I_{n} / \sim_{n}^{lisc}$ . Therefore, $| I_{n} / \sim_{n}^{lisc} | = | {{[v_{i}]}_{\sim_{n}^{lisc}} ∣ i \in {1, \dots, ℓ}} | ⩽ ℓ$ . □

We now state and prove the $BLISCC$ soundness theorem. Informally, the soundness theorem says that a system satisfying the $BLISCC$ condition becomes one that satisfies the $SRSCR$ condition after some suitable bucketing is applied.
Theorem 3.11 ( $BLISCC$ soundness).

Suppose that C satisfies $BLISCC (f, ϵ, ℓ)$ . Let $k > 0$ be such that $k^{ℓ} ϵ ⩽ 1$ . Then, ${Bkt}_{k} (C)$ satisfies $SRSCR (f, X)$ for some X satisfying the following:

For all $n \in N$ , $1 - \sum_{(S, p) \in X_{n}} \frac{| S |}{| S_{n} |} (1 - p) ⩽ k^{ℓ} \cdot ϵ (n)$ .

Proof.
Let $C^{'} = {Bkt}_{k} (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) ⩽ ℓ$ for all $n \in N$ and therefore $LISCC (C^{'}, n) ⩽ ℓ$ for all $n \in N$ . Therefore, by Lemma 3.10, for each $n \in N$ , there exist $I_{n}^{1}, \dots, I_{n}^{ℓ}$ such that (a) $I_{n}^{1}, \dots, I_{n}^{ℓ}$ partition $I_{n}$ , and (b) $sc {⟨ C^{'} ⟩}_{n} (s, v_{1}) = sc {⟨ C^{'} ⟩}_{n} (s, v_{2})$ for all $s \in S_{n}$ , $v_{1} \in I_{n}^{i}$ and $v_{2} \in I_{n}^{i}$ . set ${i \in N ∣ 1 ⩽ i ⩽ a}$ . For each $n \in N$ and $p : [1, ℓ] \to [1, k]$ , let $S_{n}^{p} = {s \in S_{n} ∣ ⋀_{i \in [1, ℓ]} \forall v \in I_{n}^{i} . sc {⟨ C^{'} ⟩}_{n} (s, v) = ⋆_{p (i)}}$ . From (a) and (b), it follows that, for each $s \in S_{n}$ , there is a unique $p : [1, ℓ] \to [1, k]$ satisfying $⋀_{i \in [1, ℓ]} \forall v \in I_{n}^{i} . {sc}_{n} (s, v) = ⋆_{p (i)}$ . Therefore, $S_{n}^{p}$ ’s partition $S_{n}$ , that is, $S_{n} = ⋃_{p : [1, ℓ] \to [1, k]} S_{n}^{p}$ and $S_{n}^{p_{1}} \cap S_{n}^{p_{2}} = \emptyset$ for $p_{1} \neq p_{2}$ . Let X be the indexed family defined by $\begin{matrix} X_{n} = {(S_{n}^{p}, \frac{| S_{n} |}{| S_{n}^{p} |} ϵ (n)) | p : [1, ℓ] \to [1, k] \land S_{n}^{p} \neq \emptyset \land (| S_{n} | / | S_{n}^{p} |) ϵ (n) ⩽ 1} for each n \in N . \end{matrix}$

We show that X satisfies (♣). Fix $n \in N$ . Let $A = {S ∣ (S,_) \in X_{n}}$ and let $A^{c}$ be the complement of A, that is, $A^{c} = {S_{n}^{p} ∣ p : [1, ℓ] \to [1, k] \land S_{n}^{p} \notin A}$ . Note that $| A | + | A^{c} | ⩽ k^{ℓ}$ and $| S_{n} | ϵ (n) > | S |$ for each $S \in A^{c}$ . Therefore, $\begin{array}{l} 1 - \sum_{(S, p) \in X_{n}} \frac{| S |}{| S_{n} |} (1 - p) & = 1 - \sum_{S \in A} \frac{| S |}{| S_{n} |} (1 - \frac{| S_{n} |}{| S |} ϵ (n)) \\ = 1 - \sum_{S \in A} \frac{| S |}{| S_{n} |} + | A | ϵ (n) \\ = 1 - (1 - \sum_{S \in A^{c}} \frac{| S |}{| S_{n} |}) + | A | ϵ (n) \\ ⩽ 1 - (1 - | A^{c} | max_{S \in A^{c}} \frac{| S |}{| S_{n} |}) + | A | ϵ (n) \\ ⩽ 1 - (1 - | A^{c} | ϵ (n)) + | A | ϵ (n) ⩽ k^{ℓ} ϵ (n) . \end{array}$ Above, the third line follows from the fact that $S_{n}^{p}$ ’s partition $S_{n}$ , that is, $⋃ (A \cup A^{c}) = S_{n}$ .

Therefore, it suffices to show that $C^{'}$ satisfies $SRSCR (f, X)$ (with the X we constructed). First, we show that the condition (2) of $SRSCR (f, X)$ is satisfied. From the construction of $S_{n}^{p}$ ’s, it follows that $sc {⟨ C^{'} ⟩}_{n} (s_{1}, v) = sc {⟨ C^{'} ⟩}_{n} (s_{2}, v) = ⋆_{p (i)}$ for all $s_{1} \in S_{n}^{p}$ , $s_{2} \in S_{n}^{p}$ and $v \in I_{n}$ where v belongs to the (unique) low-input partition $I_{n}^{i}$ . That is, the side channel of $C^{'}$ is non-interferent (with respect to high inputs) for the subset $S_{n}^{p}$ . 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 that $C^{'} |_{U}$ is not regular-channel $(f, {err}_{U})$ -secure for some $U ≺ X$ . Let $A$ be a regular-channel adversary for $C^{'} |_{U}$ such that for infinitely many $n ⩾ N$ , $A$ queries (the regular channel of) $C^{'} |_{U}$ at most $f (n)$ many times and successfully recovers the secret with probability at least ${err}_{U} (n)$ . We show that running $A$ against $C^{'}$ (by allowing arbitrary behavior when the secret is not from U) successfully recovers the secret with probability at least $ϵ (n)$ for infinitely many n. To see this, let $n \in N$ be such that $A$ successfully recovers the secret from $C^{'} |_{U}$ with probability at least ${err}_{U} (n)$ . Note that the probability that a secret randomly selected from $S_{n}$ belongs to $S_{n}^{p}$ is $| S_{n}^{p} | / | S_{n} |$ , i.e., $Pr [s \in S_{n}^{p} ∣ s \leftarrow S_{n}] = | S_{n}^{p} | / | S_{n} |$ . Then, because ${err}_{U} (n) = (| S_{n} | / | S_{n}^{p} |) ϵ (n)$ where $S_{n}^{p} = #_{1} U_{n}$ , it follows that $\begin{matrix} Pr [{Win}_{A}^{C^{' ∙}} (n, f)] ⩾ Pr [s \in S_{n}^{p} ∣ s \leftarrow S_{n}] \cdot Pr [{Win}_{A}^{C^{'} |_{U}^{∙}} (n, f)] ⩾ \frac{| S_{n}^{p} |}{| S_{n} |} \cdot {err}_{U} (n) = ϵ (n) . \end{matrix}$ Because $Pr [{Win}_{A}^{C^{∙}} (n, f)] = Pr [{Win}_{A}^{C^{' ∙}} (n, f)]$ , this contradicts condition (1) of $BLISCC (f, ϵ, ℓ)$ which says that C is regular-channel $(f, ϵ)$ -secure. Therefore, $C^{'} |_{U}$ is regular-channel $(f, {err}_{U})$ -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^{ℓ} \cdot ϵ ⩽ 1$ . Then, ${Bkt}_{k} (C)$ is $(f, k^{ℓ} \cdot ϵ)$ -secure.

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 3.4, Theorem 3.11 may give an impression that the 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 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 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.

We remark that Theorem 3.11 and Corollary 3.12 substantially improve the corresponding results from [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 side-channel 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 the system 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 \cdot ϵ)$ -security, substantially improving the previously derivable bound (note that $k \cdot ϵ ⩽ 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
¹⁰
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]).

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 to different 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 $y^{x} mod m$ where $x$ is the secret represented as a length $n$ bit array, $y$ is an attacker controlled-input, and $m$ is a constant. The program is not constant-time (assuming that then and else branches in the loop have different running times), and effective timing attacks have been proposed for the program [27,35].

Fig. 2.

Fast modular exponentiation.

However, assuming that running time of the operation (a * y) % m is independent of $y$ , it can be seen that the program satisfies the $BLISCC$ condition.11

¹¹

This is admittedly an optimistic assumption. Indeed, proposed timing attacks exploit the fact that the running time of the operation can depend on $y$ [27,35]. Here, we assume that the running time of the operation is made independent of $y$ by some means (e.g., by adopting the constant-time implementation technique).

Under the assumption, the program can be formalized as the system C where, for all

n \in N

$S_{n} = I_{n} = {0, 1}^{n}$ ;

$O_{n}^{rc} = O_{n}^{sc} = N$ ;

For all $(s, v) \in S_{n} \times I_{n}$ , ${rc}_{n} (s, v) = v^{s} mod m$ ; and

For all $(s, v) \in S_{n} \times I_{n}$ , ${sc}_{n} (s, v) = {time}_{t} \cdot num (s, 1) + {time}_{f} \cdot num (s, 0)$ .

Here,

num (s, b) = | {i \in N ∣ i < n \land s [i] = b} |

for

b \in {0, 1}

, and

{time}_{t}

(resp.

{time}_{f}

) 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 side-channel outputs are independent of low inputs, and the regular-channel is $(f, ϵ)$ -secure for any f and negligible ϵ under the assumption.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.

Therefore, by applying bucketing, it can be made

(f, k \cdot ϵ)

-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 a non-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 all $n \in N$ . Let $T = {t_{1}, \dots, t_{m}} \subseteq N \cup {\infty}$ be a finite set of timeout options where $t < \infty$ for any $t \in N$ . Then, C with the timeout option T is a system $C^{'}$ such that

$rc ⟨ C^{'} ⟩ = rc ⟨ C ⟩$ , $S ⟨ C^{'} ⟩ = S ⟨ C ⟩$ , and $O^{rc} ⟨ C^{'} ⟩ = O^{rc} ⟨ C ⟩$ ;

For all $n \in N$ , $I {⟨ C^{'} ⟩}_{n} = I {⟨ C ⟩}_{n} \times T$ ;

For all $n \in N$ , $O^{sc} {⟨ C^{'} ⟩}_{n} = O^{sc} {⟨ C ⟩}_{n} \cup {⊥}$ ; and

For all $n \in N$ , $s \in S_{n}$ and $(v, t) \in I {⟨ C^{'} ⟩}_{n}$ , $sc {⟨ C^{'} ⟩}_{n} (s, (v, t)) = timeout (t, sc {⟨ C ⟩}_{n} (s, v))$ where $timeout = λ t_{1}, t_{2} . if t_{1} < t_{2} then ⊥ else t_{2}$ .

Roughly,

C^{'}

takes an additional timeout parameter in its low input so that the execution is halted at the time 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 be used 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

¹³
We have allowed $C^{'}$ to output the (actual) regular-channel output even when timeout has reached. This is sufficient for deriving a security bound as it only increases the attacker’s knowledge.

First, we show that $LISCC (C^{'}, n) ⩽ ℓ \times m$ for all $n \in N$ (recall that $| T | = m$ ). Let $n \in N$ . Because $LISCC (C, n) ⩽ ℓ$ , by Lemma 3.10, there exists a partition $I^{1}, \dots, I^{ℓ}$ of $I {⟨ C ⟩}_{n}$ such that for all $i \in {1, \dots, ℓ}$ , $s \in S_{n}$ , $v_{1} \in I^{i}$ and $v_{2} \in I^{i}$ , $sc {⟨ C ⟩}_{n} (s, v_{1}) = sc {⟨ C ⟩}_{n} (s, v_{2})$ . For each $s \in S_{n}$ and $i \in {1, \dots, ℓ}$ , let $o_{s, i}$ be the unique $o \in O^{sc} {⟨ C ⟩}_{n}$ satisfying $\forall v \in I^{i} . sc {⟨ C ⟩}_{n} (s, v) = o$ . For each $i \in {1, \dots, ℓ}$ and $j \in {1, \dots, m}$ , let $I^{i, j} = I^{i} \times {t_{j}}$ . Clearly, $I^{1, 1}, \dots, I^{ℓ, m}$ partition $I {⟨ C^{'} ⟩}_{n}$ . Also, for all $s \in S_{n}$ , $(v_{1}, t_{j}) \in I^{i, j}$ and $(v_{2}, t_{j}) \in I^{i, j}$ , $sc {⟨ C^{'} ⟩}_{n} (s, v_{1}) = sc {⟨ C^{'} ⟩}_{n} (s, v_{2}) = timeout (t_{j}, o_{s, i})$ . Therefore, by Lemma 3.10, $LISCC (C^{'}, n) ⩽ ℓ \times m$ . Therefore, $BLISCC (f, ϵ, m ℓ)$ is satisfied. Therefore, by Corollary 3.12, ${Bkt}_{k} (C^{'})$ is $(f, k^{m ℓ} \cdot ϵ)$ -secure, for k satisfying $k^{m ℓ} \cdot ϵ ⩽ 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 be shown that $LISCC (C, n) = | I_{n} | = 2^{n}$ , because for every pair of low inputs $v_{1} \in I_{n}$ and $v_{2} \in I_{n}$ such that $v_{1} \neq v_{2}$ , there exists a secret $s \in S_{n}$ that distinguishes $v_{1}$ and $v_{2}$ (namely, s whose lengths of matching prefixes are different for $v_{1}$ and $v_{2}$ ). 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 of buckets, but placed no restriction on which side-channel outputs are put into which bucket. Below, we show 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 a rather unrealistic manner. This bucketed leaky login program is formalized as the following system:

$rc$ , $sc$ , $I$ , $O^{rc}$ are as in Example 2.2;

For all $n \in N$ , $O_{n}^{sc} = {0, 1}$ ; and

For all $n \in N$ and $(s, v) \in S_{n} \times I_{n}$ , ${sc}_{n} (s, v) = ({argmax}_{i} 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 \in {0, 1}$ , let $\overline{b}$ be the complement of b, that is, $\overline{0} = 1$ and $\overline{1} = 0$ . For $v \in {0, 1}^{n}$ and $0 ⩽ i ⩽ n - 1$ , let $flip (v, i)$ be the n-bit sequence such that $flip (v, i) [i] = \overline{v [i]}$ and $flip (v, i) [j] = v [j]$ for $j \neq i$ . For $s \in S_{n}$ and $v \in I_{n}$ , let us write $mplen (s, v)$ to be the length of the matching prefix, that is, $mplen (s, v) = {argmax}_{i} s ↾_{i} = v ↾_{i}$ .

The attack on the system proceeds as follows. The adversary $A$ chooses an arbitrary $v_{1} \in I_{n}$ as the initial input and records the output $o_{1}$ . Note that $o_{1} = 0$ if and only if $mplen (s, v_{1})$ is even. Then, $A$ chooses $v_{1, 1} = flip (v_{1}, o_{1} + 1)$ as the next input and observes the output $o_{1, 1}$ . Note that $o_{1} = o_{1, 1}$ if and only if $mplen (s, v_{1}) = o_{1}$ . $A$ continues the process, each time choosing $v_{1, j} = flip (v_{1}, o_{1} + 2 j - 1)$ as the input for each $j \in {j \in N ∣ j ⩾ 1 \land o_{1} + 2 j - 1 < n}$ in the increasing order, until he observes $o_{1, j}$ such that $o_{1} = o_{1, j}$ (if no such j is found and $s \neq v_{1}$ which $A$ can detect by observing the regular channel, then $s = flip (v_{1}, n - 1)$ and so $A$ has recovered the entire s). At such a point, $A$ has discovered that $mplen (s, v_{1}) = o_{1} + 2 j - 2$ . Let $x_{1} = mplen (s, v_{1})$ . Note that $A$ at this point has recovered the first $x_{1} + 1$ bits of s (the $x_{1} + 1$ -th bit, $s [x_{1}]$ , is equal to $\overline{v_{1} [x_{1}]}$ ). Also, $A$ makes $j + 1 = (x_{1} - o_{1}) / 2 + 2 ⩽ 2 (x_{1} + 1)$ queries for this (i.e., the queries $v_{1}, v_{1, 1}, \dots, v_{1, j}$ ). $A$ then chooses as the next input an arbitrary $v_{2} \in I_{n}$ satisfying $v_{2} [i] = s [i]$ for all $0 ⩽ i < x_{1} + 1$ . $A$ now uses the same process that he used to discover $x_{1}$ to discover $x_{2} = mplen (s, v_{2})$ , except that this time, he starts with the query $v_{2, 1} = flip (v_{2}, x_{1} + o_{2} + 2)$ where $o_{2}$ is the output given the input $v_{2}$ . By this process, $A$ will recover up to the $x_{2} + 1$ -th bit of s in at most $2 (x_{2} - x_{1})$ additional queries. Repeating this, $A$ makes at most $2 n$ queries total to recover the entire bits of s. Thus, the system is not $(2 n, ϵ)$ -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, partitioning of side-channel outputs. Note that partitioning odd timings from even timings cannot happen in reality because for any timing outputs $o_{1}$ , $o_{2}$ , $o_{3}$ such that $o_{1} ⩽ o_{2} ⩽ o_{3}$ , if $o_{1}$ and $o_{3}$ are put in a same bucket then so must $o_{2}$ (recall that bucketing is a technique that buffers and delays the output until the next time interval). A possible remedy for the issue is to incorporate the ordering constraint in the definition of bucketing 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 have noted 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 side-channel non-interference is a 2-safety property and can be checked by the methods for checking ordinary side-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 of secrets (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 from bucketing 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 \to N$ and $ϵ : N \to (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 the following is satisfied:

C is regular-channel $(f, ϵ)$ -secure; and

For all $n \in N$ , $v \in I_{n}$ , and $s_{1}, s_{2} \in S_{n}$ , ${sc}_{n} (s_{1}, v) = {sc}_{n} (s_{2}, v)$ .

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. Both $sec$ 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 non-interferent. Therefore, only the timing channel is of concern.

Fig. 3.
A non-constant-time program that cannot be made secure by globally applying bucketing.

The program can be formalized as the system $C_{comp}$ where for all $n \in N$ ,
$S_{n} = I_{n} = {0, 1}^{n}$ ;

$O_{n}^{rc} = {∙}$ ;

$O_{n}^{sc} = {i \in N ∣ i ⩽ 2^{n + 1}}$ ;

For all $(s, v) \in S_{n} \times I_{n}$ , ${rc}_{n} (s, v) = ∙$ ; and

For all $(s, v) \in S_{n} \times I_{n}$ , ${sc}_{n} (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 $BLISCC (f, ϵ, ℓ)$ for any f, ϵ and ℓ either. This is because ${sc}_{n} (s, v_{1}) \neq {sc}_{n} (s, v_{2})$ for any s and $v_{1} \neq v_{2}$ , and therefore $LISCC (C_{comp}, n) = | I_{n} | = 2^{n}$ . 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 the possible running times in two halves so that running times less than or equal to $2^{n}$ fall into the first bucket and those greater than $2^{n}$ fall into the other bucket. After applying bucketing, the system is $C^{'}$ where
$rc ⟨ C^{'} ⟩$ , $S ⟨ C^{'} ⟩$ , $I ⟨ C^{'} ⟩$ , and $O^{rc} ⟨ C^{'} ⟩$ are same as those of $C_{comp}$ ;

For all $n \in N$ , $O^{sc} {⟨ C^{'} ⟩}_{n} = {0, 1}$ ; and

For all $n \in N$ and $(s, v) \in S_{n} \times I_{n}$ , $sc {⟨ C^{'} ⟩}_{n} (s, v) = 0$ if $s + v ⩽ 2^{n}$ , and $sc {⟨ C^{'} ⟩}_{n} (s, v) = 1$ otherwise.

We show that there exists an efficient adaptive attack against $C^{'}$ . Let $s \in S_{n}$ . The adversary $A$ recovers s by only making linearly many queries via the following process. First, $A$ queries with the input $v_{1} = 2^{n - 1}$ . By observing the side-channel output, $A$ will know whether $0 ⩽ s ⩽ 2^{n - 1}$ (i.e., the side-channel output was 0) or $2^{n - 1} < s ⩽ 2^{n}$ (i.e., the side-channel output was 1). In the former case, $A$ picks the input $v_{2} = 2^{n - 1} + 2^{n - 2}$ for the next query, and in the latter case, he picks $v_{2} = 2^{n - 2}$ . Continuing the process in a binary search manner and reducing the space of possible secrets by $1 / 2$ in each query, $A$ is able 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 side channel 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 is relative 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 ${CT}^{sc}$ , if it satisfies condition (2) of $CT (_,_)$ , that is, for all $n \in N$ , $v \in I_{n}$ , and $s_{1}, s_{2} \in S_{n}$ , ${sc}_{n} (s_{1}, v) = {sc}_{n} (s_{2}, v)$ . Also, we say that C satisfies ${BLISCC}^{sc} (ℓ)$ if it satisfies condition (2) of $BLISCC (_,_, ℓ)$ , that is, for all $n \in 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 \in N$ , $O^{sc} {⟨ C^{‡} ⟩}_{n} \subseteq N$ and $O^{sc} {⟨ C^{‡} ⟩}_{n} \subseteq N$ . The sequential composition of $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 \in N$ and $(s, v) \in S_{n} \times I_{n}$ , $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 side-channel 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 $S_{n} \times I_{n}$ . We are now ready to state the compositionality theorem.

Theorem 3.21 (Compositionality).

Let $C^{†}$ be a system that satisfies ${BLISCC}^{sc} (ℓ)$ and $C^{‡}$ be a system that satisfies ${CT}^{sc}$ . Let $k > 0$ . Suppose that ${Bkt}_{k} (C^{†}); C^{‡}$ is regular-channel $(f, ϵ)$ -secure where $k \cdot ϵ ⩽ 1$ . Then, ${Bkt}_{k} (C^{†}); C^{‡}$ satisfies $SRSCR (f, X)$ for some X satisfying the following:

For all $n \in N$ , $1 - \sum_{(S, p) \in X_{n}} \frac{| S |}{| S_{n} |} (1 - p) ⩽ k^{ℓ} \cdot ϵ (n)$ .

Proof.
Let $C = {Bkt}_{k} (C^{†}); C^{‡}$ . The proof is similar to that of Theorem 3.11, and we prove by constructing an indexed family X such that X satisfies (♣) and C satisfies $SRSCR (f, X)$ . First, by ${BLISCC}^{sc}$ , it follows that $LISCC ({Bkt}_{k} (C^{†}), n) ⩽ ℓ$ for all $n \in N$ . Therefore, by Lemma 3.10, for each $n \in N$ , there exist $I_{n}^{1}, \dots, I_{n}^{ℓ}$ such that (a) $I_{n}^{1}, \dots, I_{n}^{ℓ}$ partition $I_{n}$ , and (b) for each $i \in {1, \dots, ℓ}$ , $sc {⟨ {Bkt}_{k} (C^{†}) ⟩}_{n} (s, v_{1}) = sc {⟨ {Bkt}_{k} (C^{†}) ⟩}_{n} (s, v_{2})$ for all $s \in S_{n}$ , $v_{1} \in I_{n}^{i}$ and $v_{2} \in I_{n}^{i}$ . For each $n \in N$ and $p : [1, ℓ] \to [1, k]$ , let $S_{n}^{p} = {s \in S_{n} ∣ ⋀_{i \in [1, ℓ]} \forall v \in I_{n}^{i} . sc {⟨ {Bkt}_{k} (C^{†}) ⟩}_{n} (s, v) = ⋆_{p (i)}}$ . From (a) and (b), it is immediate that $S_{n}^{p}$ ’s partition $S_{n}$ , that is, $S_{n} = ⋃_{p : [1, ℓ] \to [1, k]} S_{n}^{p}$ and $S_{n}^{p_{1}} \cap S_{n}^{p_{2}} = \emptyset$ for $p_{1} \neq p_{2}$ . Let X be the indexed family defined by $\begin{matrix} X_{n} = {(S_{n}^{p}, \frac{| S_{n} |}{| S_{n}^{p} |} ϵ (n)) | p : [1, ℓ] \to [1, k] \land S_{n}^{p} \neq \emptyset \land (| S_{n} | / | S_{n}^{p} |) ϵ (n) ⩽ 1} for each n \in N . \end{matrix}$

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 the condition (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)$ . From the construction of $S_{n}^{p}$ ’s, it follows that $sc {⟨ {Bkt}_{k} (C^{†}) ⟩}_{n} (s_{1}, v) = sc {⟨ {Bkt}_{k} (C^{†}) ⟩}_{n} (s_{2}, v) = ⋆_{p (i)}$ for all $s_{1} \in S_{n}^{p}$ , $s_{2} \in S_{n}^{p}$ and $v \in I_{n}$ where $I_{n}^{i}$ is the unique low input partition such that $v \in I_{n}^{i}$ . Then, because $sc {⟨ C^{‡} ⟩}_{n} (s_{1}, v) = sc {⟨ C^{‡} ⟩}_{n} (s_{2}, v)$ by ${CT}^{sc}$ of $C^{‡}$ , for all $v \in I_{n}$ , $s_{1} \in S_{n}^{p}$ and $s_{2} \in S_{n}^{p}$ , we have $\begin{matrix} sc {⟨ C ⟩}_{n} (s_{1}, v) & = sc {⟨ {Bkt}_{k} (C^{†}) ⟩}_{n} (s_{1}, v) + sc {⟨ C^{‡} ⟩}_{n} (s_{1}, v) \\ = sc {⟨ {Bkt}_{k} (C^{†}) ⟩}_{n} (s_{2}, v) + sc {⟨ C^{‡} ⟩}_{n} (s_{2}, v) \\ = sc {⟨ C ⟩}_{n} (s_{2}, v) . \end{matrix}$ Therefore, the side channel of C is non-interferent (with respect to high inputs) for the subset $S_{n}^{p}$ . 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 ${BLISCC}^{sc} (ℓ)$ and $C^{‡}$ be a system that satisfies ${CT}^{sc}$ . Let $k > 0$ . Suppose that ${Bkt}_{k} (C^{†}); C^{‡}$ is regular-channel $(f, ϵ)$ -secure where $k \cdot ϵ ⩽ 1$ . Then, ${Bkt}_{k} (C^{†}); C^{‡}$ is $(f, k^{ℓ} \cdot ϵ)$ -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^{‡}; {Bkt}_{k} (C^{†})$ , is also secure provided that its 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 ${CT}^{sc}$ ) and a component with a bounded low-input side-channel capacity (i.e., satisfies ${BLISCC}^{sc}$ ), 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 $C_{comp}$ 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 $C_{comp} = C^{†}; C^{‡}$ where $C^{†}$ and $C^{‡}$ satisfy the following:
$S$ and $I$ are as in $C_{comp}$ ;

For all $n \in N$ , $O^{sc} {⟨ C^{†} ⟩}_{n} = O^{sc} {⟨ C^{‡} ⟩}_{n} = {i \in N ∣ i ⩽ 2^{n}}$ ; and

For all $n \in N$ and $(s, v) \in S_{n} \times I_{n}$ , $sc {⟨ C^{†} ⟩}_{n} (s, v) = s$ and $sc {⟨ C^{‡} ⟩}_{n} (s, v) = v$ .
Roughly, $C_{comp}$ is decomposed so that $C^{†}$ is the first loop and $C^{‡}$ is the second loop (cf. Fig. 3).

Note that $C^{‡}$ satisfies ${CT}^{sc}$ as its side-channel outputs are high-input independent, and, $C^{†}$ satisfies ${BLISCC}^{sc} (1)$ as its side-channel outputs are low-input independent. By applying bucketing only to the component $C^{†}$ , we obtain the system ${Bkt}_{k} (C^{†}); C^{‡}$ . The regular-channel of ${Bkt}_{k} (C^{†}); C^{‡}$ (i.e., that of $C_{comp}$ ) 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 for such a system is at most $1 / | S_{n} |$ .14
¹⁴
Therefore, a similar analysis can be done for any strictly sub-exponential number of buckets.

Therefore, by Corollary 3.22, ${Bkt}_{k} (C^{†}); C^{‡}$ is $(f, k^{ℓ} ϵ)$ -secure for any f and negligible ϵ, and therefore, ${Bkt}_{k} (C^{†}); C^{‡}$ is $(f, ϵ)$ -secure for any f and negligible ϵ.

The above example shows that compositional bucketing can be used to ensure security of non-constant-time systems that cannot be made secure by a whole-system bucketing. It is interesting to observe that the constant-time condition, ${CT}^{sc}$ , requires the side-channel outputs to be independent of high 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 ${CT}^{sc}$ results in a system that satisfies ${CT}^{sc}$ . Likewise, as shown below, sequentially composing components that satisfy ${BLISCC}^{sc}$ results in a system that satisfies ${BLISCC}^{sc}$ .
Lemma 3.24.
Suppose that $C_{1}$ satisfies ${BLISCC}^{sc} (ℓ_{1})$ and $C_{2}$ satisfies ${BLISCC}^{sc} (ℓ_{2})$ , then $C_{1}; C_{2}$ satisfies ${BLISCC}^{sc} (ℓ_{1} \cdot ℓ_{2})$ .
Proof.
Fix $n \in N$ . By Lemma 3.10, for each $j \in {1, 2}$ , there exist $I_{j}^{1}, \dots, I_{j}^{ℓ_{i}}$ such that (a) $I_{j}^{1}, \dots, I_{j}^{ℓ_{j}}$ partition $I_{n}$ , and (b) for each $i \in {1, \dots, ℓ_{j}}$ , $sc {⟨ C_{i} ⟩}_{n} (s, v_{1}) = sc {⟨ C^{'} ⟩}_{n} (s, v_{2})$ for all $s \in S_{n}$ , $v_{1} \in I_{j}^{i}$ and $v_{2} \in I_{j}^{i}$ .

For each $(i_{1}, i_{2}) \in [1, ℓ_{1}] \times [1, ℓ_{2}]$ , let $I^{i_{1}, i_{2}} = {v \in I_{n} ∣ v \in I_{1}^{i_{1}} \land v \in I_{2}^{i_{2}}}$ . It is easy to see that the sets $I^{i_{1}, i_{2}}$ partition $I_{n}$ , that is, $I_{n} = ⋃_{(i_{1}, i_{2}) \in [1, ℓ_{1}] \times [1, ℓ_{2}]} I^{i_{1}, i_{2}}$ and $I^{i_{1}, i_{2}} \cap I^{i_{1}^{'}, i_{2}^{'}} = \emptyset$ for any $(i_{1}, i_{2}) \neq (i_{1}^{'}, i_{2}^{'})$ . Also, for any $s \in S_{n}$ , $v \in I^{i_{1}, i_{2}}$ and $v^{'} \in I^{i_{1}, i_{2}}$ , we have $\begin{matrix} sc {⟨ C_{1}; C_{2} ⟩}_{n} (s, v) & = sc {⟨ C_{1} ⟩}_{n} (s, v) + sc {⟨ C_{2} ⟩}_{n} (s, v) \\ = sc {⟨ C_{1} ⟩}_{n} (s, v^{'}) + sc {⟨ C_{2} ⟩}_{n} (s, v^{'}) \\ = sc {⟨ C_{1}; C_{2} ⟩}_{n} (s, v) \end{matrix}$ because $sc {⟨ C_{1} ⟩}_{n} (s, v) = sc {⟨ C_{1} ⟩}_{n} (s, v^{'})$ and $sc {⟨ C_{2} ⟩}_{n} (s, v) = sc {⟨ C_{2} ⟩}_{n} (s, v^{'})$ . Therefore, by Lemma 3.10, $C_{1}; C_{2}$ satisfies $BLISCC (ℓ_{1} \cdot ℓ_{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.
4. Related work

As remarked in Section 1, much research has been done on defending against timing attacks and more generally 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 a blinded cryptography algorithm whose regular channel is IND-CCA2 secure results in an algorithm that is 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 instance of 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 given in the form of $(f, ϵ)$ -security, which can provide precise bounds on the number of queries needed by adaptive 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 the given system is constant-time [3,6,11,24] or transforming it to one that is constant-time [1,26]. As we have 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 that bucketing 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 regular-channel-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 interval by blackbox monitoring, they propose to monitor the internal of the system so that different amounts of delay 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 a best 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 guarantee of security. Also, unlike our work which uses a parametric notion of security (i.e., (f, ϵ)-security), 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). Note that 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 the target system does. That is, the side channel of the target system is in the refinement order relation with the 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 by a 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 technique against 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 both conditions 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 the concerns of its side-channel behavior. By doing so, the security of the regular-channel is transferred, to certain 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 the condition ♠ in Theorem 3.4 to be non-asymptotic, that is, $\forall n \in N .1 - \sum_{(S, p) \in X_{n}} \frac{| 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 are limited to deterministic systems, and such an extension would be needed to assess the effect of bucketing when it is used together with countermeasure techniques that involve randomization. We would also like to improve the conditions and the security bounds thereof to be able to better analyze systems such as the leaky login program shown in Examples 2.2, 2.3 and 3.5. Finally, we would like to extend the applicability 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.

Footnotes

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

Agat, Transforming out timing leaks, in: Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2000), ACM, 2000, pp. 40–53.

Aguirre,

Barthe,

Gaboardi,

Garg and

Strub, A relational logic for higher-order programs, PACMPL 1(ICFP) (2017), 21:1–21:29.

J.B.

Almeida,

Barbosa,

Barthe,

Dupressoir and

Emmi, Verifying constant-time implementations, in: USENIX Security Symposium, 2016, pp. 53–70.

J.B.

Almeida,

Barbosa,

J.S.

Pinto and

Vieira, Formal verification of side-channel countermeasures using self-composition, Science of Compututer Programming 78(7) (2013), 796–812. doi:10.1016/j.scico.2011.10.008.

M.S.

Alvim,

Chatzikokolakis,

Palamidessi and

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.

Antonopoulos,

Gazzillo,

Hicks,

Koskinen,

Terauchi and

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.

Antonopoulos and

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.

Askarov,

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.

Backes,

Köpf and

Rybalchenko, Automatic discovery and quantification of information leaks, in: Proceedings of 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.

Barthe,

P.R.

D’Argenio and

Rezk, Secure information flow by self-composition, Mathematical Structures in Computer Science 21(6) (2011), 1207–1252. doi:10.1017/S0960129511000193.

11.

Barthe,

Grégoire and

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.

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.

Blot,

Yamamoto and

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.

Boreale and

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.

16.

Y.G.

Dantas,

Gay,

Hamann,

Mantel and

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.

Doychev,

Köpf,

Mauborgne and

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.

Eilers,

Müller and

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.

Eldib and

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.

Gandolfi,

Mourtel and

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.

Gay,

Mantel and

Sudbrock, An empirical bandwidth analysis of interrupt-related covert channels, IJSSE 6(2) (2015), 1–22.

23.

J.A.

Goguen and

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.

Hedin and

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.

Ishai,

Sahai and

D.A.

Wagner, Private circuits: Securing hardware against probing attacks, in: Proceedings of the 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.

Kobayashi and

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: Proceedings of 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,

Jaffe and

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.

Köpf and

D.A.

Basin, Automatically deriving information-theoretic bounds for adaptive side-channel attacks, Journal of Computer Security 19(1) (2011), 1–31. doi:10.3233/JCS-2009-0397.

30.

Köpf and

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.

Köpf and

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.

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.

Malacaria, Algebraic foundations for quantitative information flow, Mathematical Structures in Computer Science 25(2) (2015), 404–428. doi:10.1017/S0960129513000649.

34.

McIver,

Morgan,

Smith,

Espinoza and

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,

Phan and

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.

Quisquater and

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 (E-Smart 2001), Lecture Notes in Computer Science, Vol. 2140, Springer, 2001, pp. 200–210. doi:10.1007/3-540-45418-7_17.

37.

J.C.

Reynolds, The Craft of Programming, Prentice Hall International Series in Computer Science, Prentice Hall, 1981.

38.

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.

Smith, On the foundations of quantitative information flow, in: Proceedings of the 12th International Conference on Foundations of Software Science and Computational Structures (FOSSACS 2009), Lecture Notes in Computer Science, Vol. 5504, Springer, 2009, pp. 288–302.

40.

Sousa and

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.

Svenningsson and

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.

Terauchi and

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.

Terauchi and

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.

Terauchi and

Antonopoulos, A formal analysis of timing channel security via bucketing, http://www.f.waseda.jp/terauchi.

45.

Tizpaz-Niari,

Cerný and

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.

Tromer,

D.A.

Osvik and

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

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.

Yasuoka and

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.

Yasuoka and

Terauchi, On bounding problems of quantitative information flow, Journal of Computer Security 19(6) (2011), 1029–1082. doi:10.3233/JCS-2011-0437.

50.

Yasuoka and

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.

Zhang,

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.

Bucketing and information flow analysis for provable timing attack mitigation

Abstract

Keywords

1. Introduction

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

3 A slight difference is that the definition in [7] is not asymptotic, i.e., it asserts Pr [ Win A C ( n , f ) ] for all n. The relaxed definition in this paper facilitates derivations of asymptotic bounds.

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

2.1. Insufficiency of bucketing

3. Sufficient conditions for security against adaptive side-channel attacks

3.1. Secret-restricted side-channel refinement condition

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.

Definition 3.7 ( LISCC ).

8 In QIF literature, channel capacity is typically defined to be the log of the number of equivalence classes. Here, we use the non-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.

13 We have allowed C ′ to output the (actual) regular-channel output even when timeout has reached. This is sufficient for deriving a security bound as it only increases the attacker’s knowledge.

Definition 3.17 (Constant-time).

Theorem 3.18 ( CT soundness).

Theorem 3.21 (Compositionality).

5. Conclusion and future work

Footnotes

Acknowledgments

References

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

³
A slight difference is that the definition in [7] is not asymptotic, i.e., it asserts $Pr [{Win}_{A}^{C} (n, f)]$ for all n. The relaxed definition in this paper facilitates derivations of asymptotic bounds.

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

⁶
It is easy to relax the condition to also be asymptotic so that the refinement order relation only needs to hold for large n.

Definition 3.7 ( $LISCC$ ).

⁸
In QIF literature, channel capacity is typically defined to be the log of the number of equivalence classes. Here, we use the non-log form which turns out to be more convenient for our purposes.

⁹
It is easy to relax the notion to be asymptotic so that channel capacity only needs to be bounded for large n.

¹³
We have allowed $C^{'}$ to output the (actual) regular-channel output even when timeout has reached. This is sufficient for deriving a security bound as it only increases the attacker’s knowledge.

Theorem 3.18 ( $CT$ soundness).