Decomposition Instead of Self-Composition
for Proving the Absence of Timing Channels
Timos Antonopoulos, Paul Gazzillo, Michael Hicks,† Eric Koskinen, Tachio Terauchi‡ , Shiyi Wei†
Yale University, USA†

University of Maryland, USA‡

JAIST, Japan

Abstract

1. Introduction

We present a novel approach to proving the absence of timing channels. The idea is to partition the program’s execution traces in such a way that each partition component ischecked for timing attack resilience by a time complexity
analysis and that per-component resilience implies the resilience of the whole program. We construct a partition by
splitting the program traces at secret-independent branches.
This ensures that any pair of traces with the same public input has a component containing both traces. Crucially, theper-component checks can be normal safety properties expressed in terms of a single execution. Our approach is thus
in contrast to prior approaches, such as self-composition, that
aim to reason about multiple (k ≥ 2) executions at once.
We formalize the above as an approach called quotientpartitioning, generalized to any k-safety property, and proveit to be sound. A key feature of our approach is a demanddriven partitioning strategy that uses a regex-like notion
called trails to identify sets of execution traces, particularly those influenced by tainted (or secret) data. We haveapplied our technique in a prototype implementation tool
called Blazer, based on WALA, PPL, and the brics automaton library. We have proved timing-channel freedom of (orsynthesized an attack specification for) 24 programs written
in Java bytecode, including 6 classic examples from the literature and 6 examples extracted from the DARPA STAC
challenge problems.

A program has a timing channel if variations in its running
time can reveal information about secret inputs. For example, a password check whose running time depends on how
much of the guess matches the real (secret) password potentially has a timing channel. That a program is free of timing
channels is a k-safety property. Such a property involves k(terminating) runs of a program and, consequently, validation requires establishing relationships between k different
execution traces. For timing channels, we need k = 2 runs:
any pair of executions whose computations use the same
public inputs (but may differ on their secret inputs) should
nevertheless have similar running times.
We are interested in verifying that programs are free oftiming channels. It seems appealing to leverage the successof abstract interpretation. Abstract interpretation-based tools
enjoy rigorous guarantees and provide formal proofs of various safety and liveness properties. They also are efficient.
Implementations such as A STRÉE and I NTERPROC are able
to validate properties of large C programs.
Abstract interpretation-based techniques focus on single
executions, but to prove k-safety properties we need to relate multiple executions. A clever way to do this is to employ self-composition [7, 8]: To reason about k runs of aprogram, we can concatenate k copies of it (with variables
suitably renamed) and then assert a property that relates variables in different copies. For our timing channel property,
we could concatenate the program with itself, require thatpublic inputs to both copies be the same, and then assertthat execution counters inserted for each copy are (approximately) equal at the conclusion, despite allowed variation of
secret inputs. Self-composition can be expensive due to the
explosion of the cross-product state space. As such, several
works have looked to improve the basic idea by exploiting
structural similarities in the program (e.g., using interleaving composition [27, 36, 37]). Other works applied similarideas to improve relational verifiers directly [5, 11, 31, 34].
As discussed Section 7, these approaches (and others) nevertheless rely, at least implicitly, on making k copies of the
program, which means that invariants are split across the
product program. The result can be either poor performance

CCS Concepts • Security and privacy → Logic and verification; • Theory of computation → Program reasoning; Logic and verification; • Software and its engineering → Formal methods
Keywords Timing Attacks, Blazer, Verification, Subtrails,
Decomposition

or key information being lost due to abstraction during fixpoint computation.
With a focus on verifying the absence of timing channels,
we depart from the composition-based strategies and instead
establish a novel decomposition methodology. Our key insight, sketched in Section 2, is that rather than prove a relational property about all pairs of execution traces, we canprove a non-relational property about each trace in a certain
trace partition, computed iteratively.
Formally, let C be a program of interest, and JCK be allof its possible execution traces. Our method aims to produce
a partition T = T1 , ..., Tn (for some n ≥ 1) of JCK which
has the following properties:
1. For every pair of traces {π1 , π2 } ⊆ JCK, if in(π1 )[low] =in(π2 )[low] then there exists some Ti such that {π1 , π2 } ∈Ti .1 That is, if two execution traces have the same low—meaning non-secret—inputs, then they must both be partof some partition element.
2. For each Ti and π ∈ Ti there exists a function f suchthat time(π) = f (in(π)[low]) ± c; i.e., the running timeof each trace is a function of the low input, plus or minus
some constant c (which defines the observational limitsof the attacker). Importantly, the running time should not
be a function of the secret inputs.
With such a partition we establish the timing channel freedom property Φtcf we desire, which is ∀π1 , π2 ∈ JCK,in(π1 )[low] = in(π2 )[low] ⇒ time(π1 ) ≈ time(π2 )Each trace in the same partition component Ti has the samerunning time function f over low variables (only), and traces
in different partitions have unequal low inputs and thus satisfy Φtcf vacuously.
In Section 3, we make this point rigorous by formally developing a decomposition strategy we call k-quotient partitioning for proving k-safety properties Φ, showing that our
proof of Φtcf is an instance of it. k-quotient partitioning has
two components: (1) a k-ary quotient formula ψ such thateach set of k traces that satisfies ψ appears in the same partition element; and (2) a family of k-ary partition properties
Pi such that any set of k traces in a partition element Ti satisfy Pi , and all Pi together jointly imply the global property
Φ. For timing channels, we have k = 2, the quotient formulais that traces’ low inputs are equal, and the partition property
is that the running time of each partition element’s trace isa function f of its low inputs. Section 3 briefly describes
other k-safety properties whose proof may be amenable tok-quotient partitioning.
A key challenge of k-quotient partitioning is arriving at
the partition T. Our approach to proving the absence of timing channels synthesizes T iteratively, along with the corresponding per-component running times Pi . We do this us1 Technically, the T , ..., T need not be disjoint, i.e., the same trace π may
n1

appear in several Ti . But for gaining intuition this detail is unimportant.

ing an abstraction called trails. A trail t is an annotated regular expression (regex) over the edges of the control-flow
graph, and specifies a subset of the program’s execution
traces (i.e., those that follow the trail). We partition execution traces using trails annotated by the influence of secret or public inputs (“taint”). In particular, branching expressions in a trail (union or Kleene star constructors) areannotated as to whether the branch depends on inputs thatare tainted. Starting with the most general trail, which captures all executions, we attempt to prove a tight lower andupper bound on the running time of traces described by the
trail [16–18] by matching transition relations with a databaseof lemmas [17]. If we cannot, we break the trail into smaller
trails at tainted branching expressions; e.g., putting all executions that take the true branch into one trail and all thattake the false branch into another. Since we split at branches
that are taint-influenced, we ensure that execution pairs involving equal public inputs will be put in the same partition
component. The trail abstraction and our partitioning algorithm is described in detail in Section 4.
Section 5 describes the implementation of our approachin a tool called Blazer. We equip a standard abstract interpreter with the ability to consult an oracle (the synthesized trails) to decide which CFG arcs to follow, thus deriving partition-specific invariants. These invariants underlie
the per-trail running time analysis. If Blazer cannot provethat a partition Ti has tight bounds on running times, andfurther taint-based sub-partitions are not possible, it attempts
to synthesize possible attacks. In particular, it generates subpartitions and running times based on secret information; if
a difference in secret values results in observable differencesin running time, then there is a possible attack.
Section 6 presents an evaluation of Blazer on a collectionof 25 benchmarks, including 12 tricky hand-crafted benchmarks, 7 programs from the literature [15, 22, 29], and 6
fragments of the DARPA STAC challenge problems [35].
We find that Blazer is able to prove the absence of timing
channels when the program is safe or else synthesize an attack specification in all but two cases.
In summary, this paper contributes:
1. A novel program analysis technique for proving the absence of timing channels that decomposes the problem
into one of proving simpler properties of subproblems
rather than proving the relational (2-safety) property directly, e.g., by self-composition (Sec. 2).
2. A proof of soundness of a general decomposition approach for proving k-safety properties called k-quotientpartitioning, of which our timing channel approach is one
instance (Sec. 3).
3. A novel symbolic representation of partitions, trails, andan algorithm for constructing new partitions (Sec. 4).

4. An implementation of our approach in the tool Blazer
discovering timing channels in Java programs, or proving
their absence (Sec. 5).2
5. An evaluation on 25 benchmark programs, including examples from the STAC challenge problems and the cryptography literature [15, 22, 29] (Sec. 6).

2.

Overview

In this section, we give a tour of our work. We begin withsimple examples to introduce the key idea of using a partition of executions to prove timing channel freedom. We thendescribe our algorithm in more detail, explaining how partitioning is interleaved with running time computation. Finally, we explain how the same basic approach can be used
to synthesize a possible attack when timing channel freedom
cannot be proved.
2.1

Example 2.

Decomposition: The Basics

Consider the following example program.
Example 1.
1
2
3
4
5
6
7
8
9
10

where JCK is the set of all execution traces of the program
C. An obvious consequence of this is that every pair oflin
executions π1 , π2 share Plow
. As such, it is clear that there
can be no timing channel.
The key idea of our approach is to break down the executions of the program into various cases, depending on
high-independent branching, and in each case discover a running time property P that describes all traces in that case. To
do this, we symbolically (and automatically) discover a partitioningSof the execution traces T = T1 , ..., Tn such that
JCK = i∈[1,n] Ti so that we can find some Pi to characterize the running time for all π ∈ Ti . As long as each Pi
is independently acceptable (i.e., running time does not depend (much) on high), then the overall program satisfies thedesired property. In Example 1, we only needed one partition
component. Here is another example.

void foo(int high, uint low) {if (high == 0) {i = 0;
while(i < low) i++;}else {
i = low;while(i > 0) i−−;}}This program takes a secret input high, and an attackercontrolled (tainted) input, low. A program is said to have atiming channel if the attacker, assumed to know the programcode, can infer information about the high by observing
the program’s running time (perhaps iteratively varying the
input low). The execution of this particular program branches
on secret variable high so we may wonder whether there
is a timing channel. Proving there is not one requires, inprinciple, that we relate all pairs of execution traces. Doingso directly (e.g. by constructing a self-composition [7, 36] ora relational program analysis [5, 9, 11, 34, 40]) can magnify
the overall state space to consider.
We show that we can instead prove that all executions(later: execution partitions) share the same property. For
timing channels, we want to prove that each execution of theabove program has a running time that is a function of (only)
low. In this case we can be more specific: the running time
is linear in low (for some fixed linear function). We mightlin
write this as a property Plow
, and then write:lin∀π ∈ JCK. Plow(π)
2 While Blazer does not yet support recursive functions, our theoreticalresults still apply; we plan to explore an annotation-based strategy.

1
2
3
4
5
6
7
8
9
10

void bar(int high, int low) {int i;
if (low > 0) { // O(2*low)i = 0;
while(i<low) i++;while(i>0) i−−;
} else { // O(1)if (high == 0) { i = 5; } else { i = 0; i++; }}}In this program, not all executions have the same symbolic running time. If low is positive, the execution will belinear in low, otherwise it will be either one instruction or
two, depending on the value of high. To discover this, we
can form a partition of the execution traces as follows:
T> , {π | in(π)[low] > 0} and T≤ , {π | in(π)[low] ≤ 0}

where JCK ⊆ T> ∪ T≤ and in(π)[low] means the value ofthe low input variable of trace π. For now, let us assume
this partition is given to us (we describe how we get thepartition shortly). With some help (discussed below), we cancoerce an off-the-shelf abstract interpreter to now perform
two analyses proving, respectively, that:lin∀π ∈ T> . Plow(π) and ∀π ∈ T≤ . Pcconst (π).

Here, property Pcconst (π) means that the running time of
the trace is within some (fixed) small attacker-unobservablebound (say, ε) of the constant c. For this example, c = 1 withε = 1.
These two proofs establish relationships between any two
copartitional traces (two traces in T> or two traces in T≤ ).
But what about some π0 ∈ T> and some π1 ∈ T≤ ? These
two traces have different symbolic running times. However,notice that the path condition (whether low is above 0) depends only on variable low and not on secret variable high.
Consequently, we can immediately conclude that, although

1
2
3
4
5
6
7
8
9
10
11
12
13
14
1
2
3
4
5
6
7
8
9
10
11
12
13

loginSafe(String username, byte[] guess) {boolean dummy, matches = true;byte[] user_pw = retrievePassword(username);if(user_pw == null)
return false;for(int i = 0; i < guess.length; i++) {if (i < user_pw.length) {if(guess[i] != user_pw[i]) matches = false;
else dummy = true;} else {dummy = true; matches = false;}}
return matches; }loginBad(String username, byte[] guess) {byte[] user_pw = retrievePassword(username);if(user_pw == null)
return false;for(int i = 0; i < guess.length; i++) {if (i < user_pw.length) {if(guess[i] != user_pw[i])return false;} else {return false;}}
return true; }[8, 23*g.len+10]

trmg — Most general trail
All paths are possible
taint

taint

tr1 — May exit on line 5

tr2 — Must enter for loop

[8, 8][19*g.len+10,
23*g.len+10]

trmg — Most general trail
All paths are possible
taint[6 , 20*g.len+8]

taint

tr1— Exits on Line 4

tr2— Must enter for loop

[6,6]

[28 , 20*max(g.len,p.len)+8]
tr3— Within for loop,
can take early exits[6 , 20*max(g.len-1,p.len)+8]

sec

sec

tr4 — Within for loop,
cannot take early exit
[6 , 20*g.len+8]

Figure 1. Two versions of a program that validates a password (left column) and the corresponding output of our toolBlazer (right column). Each rectangle represents a trail, and each downarrow from a trail represents a subtrail; the taint andsec annotations indicate on what sort of data the subtrail was created. The balloons contain ranges [x, y] that indicate thelower/upper bound on the trail’s running time in terms of number of instructions (g.len is short for guess.length and p.len isshort for user_pw.length). Bolded (green) nodes indicate areas where the program is safe and double-line (red) nodes indicate
an attack specification.
traces from two different partition components have different running times, these differences cannot be correlatedwith high’s value.
2.2

Synthesizing Partitions with Trails

Our trace partition in Example 2 considered different input values: those for which low > 0, or not. This distinction corresponds to whether we branch at line 3, or not. Ouralgorithm likewise develops a partition by considering setsof paths, particularly those that take a branch one way vs.
the other. Paths are specified using annotated regular expressions tr that we call trails, which for the purposes of thisexample have the following grammar:
tr ::= ij || i↓ || tr1 · tr2 || tr1 |α tr2 || trα∗Trails are defined over edges ij in a control-flow graph,
where i and j represent CFG blocks in the program. We
also permit edge i ↓, meaning a block i that subsequently

moves to the exit block. We use · for sequential composition(often dropped when clear from context), vertical bar for
branching, and star for looping. Both branching and looping
regex operators are annotated with α ∈ {l,h,(l,h)}. Symboll is used to mean low, h to mean high, or l,h to mean both.
Here is an example:3
23 · (34 · 45 · 5∗l · · · ) |l (38 · · · )This represents executions of Example 2. These executions
start on line 2 and proceed to line 3, characterized by edge
23. Then they follow the branch at line 3, which depends on
low input, as indicated by the annotation l. According to thelhs of the branch, this trail considers executions that go fromline 3 to 4 and then 4 to 5 and then 0 or more times throughline 5, due to the low-dependent loop, etc. According to the
3 For this example we refer to line numbers, rather than CFG blocks (asused by our actual algorithm), for clarity.

rhs of the branch |l , the trail also considers executions thatgo from 3 to 8 (etc.).
The trail-based partition is generated iteratively. We startwith a trail that characterizes all possible executions of the
program; we call this the most general trail, trmg . We attempt to compute the running time of all paths characterized
by this trail. If the running time is primarily a function of low
input, with constant-bounded effect from high, then we aredone. If this is not possible, we further break down the trail at
low-dependent (only) branching points. For Example 2, thisresults in a trail describing all paths for all true paths throughline 3, and another for all false paths.
Ultimately, the final partition is a collection of trails
tr1 , ..., trn such that:
1. The union of all of theStrails’ languages covers the language of trmg . That is, i∈[1,n] L(tri ) ⊇ L(trmg ).
2. Trails correlate to the branching decisions that depend
only on low security variables.
3. Each trail tri is such that every execution’s running timelin
. Hencecan be described by a single function Pi , e.g. Plowit can be proved that ∀π ∈ L(tri ) ∩ JCK, that π |= Pi .
Thanks to the formal guarantees of our decomposition (Section 3), this suffices to entail that the overall program is freeof timing channels.
More elaborate example. Consider the program loginSafe
at the top of Figure 1. This function looks up the given
username (a non-secret) and if the user is known, checks thatthe given guess matches the user’s password. We return true
if so, and false otherwise.4
To the right of the code is a visual depiction of the a treeof trail specifications. The top box represents the most general trail, which is our starting point. With it, we computethe running time of executions that follow this trail. This isembodied in a component called B OUNDA NALYSIS. Technically, to implement B OUNDA NALYSIS we equip an offthe-self abstract interpreter with the ability to be restricted toa given trail, leverage the seeding technique [10] to computetransition invariants [30], and match these invariants against
a database of complexity bound lemmas [16, 17]. The resultof applying B OUNDA NALYSIS to trmg is that it computes alower bound of 8 and an upper bound of 23 × g.len + 10 (depicted as a cloud), where g.len is shorthand for guess.length.
With the range of running times in hand, we now ask
whether the range is narrow: that the running time of thegiven executions is a function of low variables plus up toa maximum constant value c, where c is a limit on theobservability of the attacker, i.e., the difference between thelongest and shortest running time is c. If we find that therange between a given lower/upper bound is narrow then weknow we mark the code as free from timing channels. For
trmg , we find that this bound is not narrow. This means we
4 We do not consider the presence or non-presence of a username in the

database to be secret information, for this example.

need to partition trmg according to (only) tainted data, andthen try again, for each partition.
We do this using a component called R EFINE PARTITION.
In this case it splits the most general trail into two based on
the branch at line 4. The parent-child relationship in the tree
shown in the figure tracks this subtrail relationship. Edges
are annotated as to whether the subtrail was chosen basedon branching on low data (when trying to prove safety) or
based on branching on high data (when trying to synthesize
an attack, discussed shortly). For legibility, we have replaced
each trail’s regular expression with an intuitive descriptionof the trail it specifies.
Now we compute the running times for these two trails
separately. The left-hand trail has running time 8—this is thetrail that exits on line 4. The right side has a running time thatis a direct function of g.len. These two running times individually satisfy our narrowness criterion for timing channel
freedom. In particular, the constant one does trivially, andthe range on the right side does assuming that g.len ≤ nfor some fixed size that does not exceed the power of the attacker (which can be specified); e.g., if n = 100, the running
time is equivalent to 21 × g.len ± 210, which is safe assuming the adversary’s observational power is bounded by theconstant 210. As such, because each one is acceptable, thetwo together are as well, and the program is sure to be freeof timing channels.
2.3 Synthesizing Attacks
Our partitioning strategy is also useful for finding possible
attacks if a program is not free of timing channels. To see
how this works, consider the bottom of Figure 1. For this example, there is a timing channel (based on a bug in the Tenex
password checker [24])—if the program exits on either lines
8 or 10, then the running time reveals the length of the prefixof guess that matches the real password.
When trying to prove this program is timing-channel free,the bound analysis will discover running time bounds similar to the correct example: a lower bound of 6 and an upperbound of 20 × g.len + 8. As such, it will partition again according to the tainted branch on line 3. This time, though,the running times of the two partition trails do not meet ournarrowness criterion: while the trail on the left hand side isnarrow (due to the exit on line 4), the trail on the right handside is not narrow: it has a constant lower bound and an upper bound that relies on both g.len and the length of the actual password. Unfortunately, we cannot easily sub-partition
the right side further, since branches in the loop also dependon secret information—partitioning is only permitted on low
data. As such we have found a potential problem.
At this point, the tool changes gears and attempts to discover a vulnerability. To this end, R EFINE PARTITION generates the next two trails (tr3 and tr4 ). These trails differ basedon whether or not the shortcut return statement can be taken
on Line 7 (or 10). For both tr3 and tr4 , our toolchain computes a lower bound of constant running time, correspondingto the early exit on line 4. For tr4 , our toolchain computes alinear running time of 20 × g.len + 8 for the upper bound.
Meanwhile, tr3 forces the program to return early after entering the loop, either by taking the return statement on Line 8or the return statement on Line 10. For tr3 , our toolchain
computes a range of running times, different from the ones
computed for tr4 . With this, the tool reports a vulnerability:
there are two trails (tr3 and tr4 ), the choice between them
depends on high data (arcs labeled sec), and yet they havedifferent running times. Therefore, for the same low input
there can be two different possible executions that yield different running times as the branching depends on the valueof the secret.
We call this output an attack specification. Because weare working with a static analysis, the result of our tool is
not immediately two concrete traces. However, it provides
a specification for two traces that witness the attack. All
that remains is to ensure that these traces are feasible byfinding justifying inputs. This can be done manually by aprogrammer or via an under-approximate analysis (e.g., asymbolic execution [29]).

3.

Semantic Partitioning

While our practical focus is timing channels, our decomposition strategy works for other k-safety properties, too. In thissection we provide a formalization of our general decomposition. The key result is Theorem 3.1 which says that we
can conclude a k-safety property of the traces of a program,using non-relational reasoning. Proving timing channel freedom, which is a 2-safety property, is a consequence of thisresult. The details of our particular algorithm are given in thesections that follow.
3.1

Programs, Traces, and k-Safety Properties

Let π range over execution traces. For a program C, we
write JCK for the set of all execution traces of C. A k-safety
property is a predicate q(C) of the following form:q(C) , ∀π1 , . . . , πk ∈ JCKk .Φq (π1 , . . . , πk )if the following is satisfied∀π1 , . . . , πk ∈ JCKk .
V
ψ(π1 , . . . , πk ) ⇒ ∃T ∈ T. 1≤i≤k πi ∈ T.
Roughly, T is a ψ-quotient partition if for each k-tuple oftraces satisfying ψ, there is an element T ∈ T to which all
the k traces belong.
Example 3. Note that, for relational properties (i.e., whenk ≥ 2), any true-quotient partition T must have an element
T ∈ T such that JCK ⊆ T .
Example 4. The partitioning based on low (tainted) inputs described earlier can be formalized as a ψtcf -quotientpartition, where ψtcf (π1 , π2 ) is the predicate in(π1 )[ℓ] =in(π2 )[ℓ] with ℓ being the low (taint) variables (at times,
we may also write in(π1 ) =low in(π2 ) for the latter predicate). For instance, recall the partition T> , T≤ described in
Section 2 where low is a low variable, T> contains all traces
with low > 0, and T≤ contains all traces with low ≤ 0. It
is easy to see that T = {T> , T≤ } is a ψtcf -quotient partition.
Let q be a k-safety property, as defined above. We say thatq is ψ-quotient partitionable if∀C.∀π1 , . . . , πk ∈ JCKk .
(ψ(π1 , . . . , πk ) ⇒ Φq (π1 , . . . , πk )) ⇒ Φq (π1 , . . . , πk ).
Note that the condition is equivalent to the following:∀C.∀π1 , . . . , πk ∈ JCKk .ψ(π1 , . . . , πk ) ∨ Φq (π1 , . . . , πk ).
In short, to verify or refute a ψ-quotient partitionable property it suffices to only consider the k-tuples of execution
traces that satisfy ψ.
Example 5. Trivially, any k-safety property is true-quotientpartitionable. However, as remarked in Example 3, any suchpartition must have an element containing all the traces.
Example 6. The timing channel freedom property is thefollowing 2-safety property:tcf(C) , ∀π1 , π2 ∈ JCK2 .
in(π1 )[ℓ] = in(π2 )[ℓ] ⇒ time(π1 ) ≈ time(π2 )where Φq is a predicate on k-tuples of execution traces.
We may assume that a program trace contains whatever
information needed for the property, such as inputs, outputs,
intermediate states, and event times. For example, assumingthat π is a sequence of states in the execution, we may referto the input value of the variable x in the execution trace π
by in(π)[x].

where ℓ are low variables and time(·) ≈ time(·) says thatthe running times of the two executions are indistinguishable. It is easy to see that the property is ψtcf -quotient partitionable with ψtcf (π1 , π2 ) , in(π1 )[ℓ] = in(π2 )[ℓ].

3.2

3.3 Relational Analysis via Non-Relational Analysis

Quotient Partition and Quotient Partitionable
Properties

A trace partition T for C is a finite set of non-empty
sets ofS
traces T = {T1 , . . . , Tn } such that JCK ⊆ 1≤i≤n Ti . Even
though we use the name “partition”, we do not enforce theTi ’s to be pairwise disjoint. Let ψ be a predicate on k-tuples
of execution traces. We say that T is a ψ-quotient partition

As we shall prove below, a quotient partitionable property can be verified by verifying each quotient partition
component individually. A key insight of our approach isthat, often, individual partition components become isolated
enough to be amenable for verification via a non-relational
analysis. Next, we formalize the idea.

A non-relational property is of the form ∀π ∈ JCK.P (π)
where P is a predicate on an execution trace. We call such a
P a trace property.
Consider a k-safety property q again. We say that a trace
property P is relational-by-property-sharing for q, denoted
RBPS(P, q), if the following holds:V∀π1 , . . . , πk . 1≤i≤k P (πi ) ⇒ Φq (π1 , . . . , πk )Roughly, RBPS(P, q) says that checking that P holds forindividual execution traces is sufficient for checking that Φq
holds for the k-tuples of the execution traces. Hence, thecondition implies that we can check the relational property
Φq on the tuples of traces from a partition component bychecking the non-relational property P on the component.
Example 7. Recall the timing channel freedom property tcf
from Example 6. Consider a non-relational complexity analysis which, given T , computes the lower and upper bound of
the running times for the execution traces in T , and checks
if the bound difference is small enough to be indistinguishable by an attacker. The analysis induces a non-relational
property Pf (π) where f is a high-independent function overtraces and Pf (π) is true iff the running time of π is closeenough to f (π). It is easy to see that RBPS(Pf , tcf).
When q is ψ-quotient partitionable, it is sufficient tocheck a relational-by-property-sharing non-relational property on each component of a ψ-quotient partition. More formally, we have the following.
Theorem 3.1 (Soundness). Suppose that q is ψ-quotientpartitionable, and T is a ψ-quotient partition for a program
C. Then, q(C) holds if for each T ∈ T, there exists P suchthat (i) RBPS(P, q), and (ii) for each π ∈ JCK ∩ T , P (π).
Proof. Let q(C) , ∀π1 , . . . , πk ∈ JCKk .Φq (π1 , . . . , πk ).
Take π1 , . . . , πk ∈ JCKk arbitrarily. It suffices to showthat Φq (π1 , . . . , πk ). Because q is ψ-quotient partitionable,Φq (π1 , . . . , πk ) iff ψ(π1 , . . . , πk ) ⇒ Φq (π1 , . . . , πk ).
Therefore, suppose that ψ(π1 , . . . , πkS). It suffices to showthat Φq (π1 , . . . , πk ). Because JCK =T, there must be
T ∈ T such that π1 ∈ T . Because T is a ψ-quotient partitionand ψ(π1 , . . . , πk ), it follows that πi ∈ T for all 1 ≤ i ≤ k.
Let P be a trace property satisfying conditions (i) and (ii) for
T . Then, we have Φq (π1 , . . . , πk ) by (ii) and the definitionof RBPS(P, q).
Example 8. Recall the trivial true-quotient partition from
Example 3. Recall from Example 5 that the any partition inthis case must have an element containing all JCK. Therefore, in this case, Theorem 3.1 only implies that q(C) holds
if P holds for all execution traces of C for some relationalby-property-sharing non-relational property P (wrt. JCK),
which is apparent from the definition.
Example 9. More generally, we would like to find a strong
ψ with which a k-safety property q is quotient partitionable, and obtain a corresponding fine-grained ψ-quotientpartition. Such a fine-grained partition improves the analysis efficiency as it divides the analysis problem into smaller
subproblems, and, perhaps more importantly, can increase
the analysis precision whereby the partition components become isolated enough for the non-relational analysis to return precise results.
For example, for tcf, applying the non-relational complexity analysis described in Example 7 on the entire trace
set JCK is unlikely to be successful since different traces arelikely to have widely different run times. By contrast, partitioning the traces via the quotient factor ψtcf , in(π1 )[ℓ] =in(π2 )[ℓ] allows dividing the problem so that traces thathave different low-security values may be analyzed separately. The non-relational analysis may compute widely different running time bounds for different partition components, but the overall verification may still succeed when thecomputed bounds are narrow within each individual partition component.
Theorem 3.1 shows the soundness of our method. In fact,
the following result shows that the method is also complete.
That is, for any k-safety property q and a program C satisfying q, there exist a quotient partition and corresponding
non-relational properties that can be used to verify that C
satisfies q via the method.
Theorem 3.2 (Completeness). Suppose q(C). Then, thereare ψ and T such that q is ψ-quotient partitionable, T is aψ-quotient partition for C, and, for each T ∈ T, there exists
P such that RBPS(P, q) and ∀π ∈ JCK ∩ T.P (π).
Proof. Let ψ be any predicate with which q is quotient partitionable, and T be any ψ-quotient partition for C (e.g.,ψ = true and T = {JCK}). Define the non-relational property P (π) = π ∈ JCK. Then, we have RBPS(P, q) and∀π ∈ JCK ∩ T.P (π) for every T .
Completeness is arguably only of theoretical interest because, as shown in the proof, it holds independently of partition choices and can use somewhat “unfair” non-relational
properties. (The proof essentially says that one can always
verify q non-relationally by checking the trace containment
against a program that is known to satisfy q).
Relational partition properties. While we have focused
our efforts on properties for each partition that are nonrelational, it is worth noting that this is not necessary: having
relational properties instead would still work. For timing
attacks, as explained earlier, we found that focusing on nonrelational properties is a good way to avoid explosion of thestate space.
More precisely, we can extend the notion of relational-byproperty-sharing so that for Θ, an m-ary relation, RBPS(Θ, q)
is the condition below.
∀πV1 , ..., πk .

′′′ }⊆{π ,...,π } Θ(π1 , . . . , πm ) ⇒ Φq (π1 , . . . , πk ){π1′ ,...,πm1kSuch relational properties Θ can replace the relational-byproperty-sharing non-relational properties P in our framework. In other words, if q is ψ-partitionable, and T is aψ-quotient partition for C, then, q(C) holds if for each
T ∈ T, there exists ΘT such that RBPS(ΘT , q) and for each
π1 , . . . , πm ∈ JCK ∩ T , ΘT (π1 , . . . , πm ). Furthermore, suchproperties ΘT can be analysed in a manner similar to Φq , ifneeded.
3.4

More General k-Safety Examples

The framework we presented above is general enough to apply to k-safety properties other than timing channel freedom.
We conclude this section with some examples.
2-safety. First, there are other commonly used 2-safety
properties on which our decomposition method can be applied. One is determinism, expressed asdet(C) , ∀ π1 , π2 .
in(π1 ) = in(π2 ) ⇒ out(π1 ) = out(π2 ).
For ψdet (π1 , π2 ) defined as in(π1 ) = in(π2 ), the property
det(C) is ψdet -quotient partitionable. Then, for any function
g over the domain of the inputs of the traces, the property
Pg (π) , out(π) = g(in(π)) is such that RBPS(Pg , det)holds. It follows from Theorem 3.1, that a program C isdeterministic, if we can find a partition T, where for each
T ∈ T, there exists a function gT such that RBPS(PgT , det)
and for each π ∈ JCK ∩ T, PgT (π).
k-safety, k > 2. The examples we have focused on until
now, are for the most part 2-safety properties, but this framework is developed generally for k-safety properties where k
can be larger than 2. One such property is the channel capacity property [4, 25, 32, 41], which is a generalization oftiming channel freedom. Note that the timing-channel freedom is defined to be the property that there can only be one
running time (up to some small attacker-unobservable fluctuation) per public input. The channel capacity property isa relaxation which says that there are at most q (for somefixed q ∈ Z) running times per public input. For instance,
the property can be formally written as follows for q = 2:
ccf(C) , ∀ π1 , π2 , π3 ∈ JCK3 .
in(π1 )[ℓ] = in(π2 )[ℓ] = in(π3 )[ℓ] ⇒time(π1 ) ≈ time(π2 )∨time(π1 ) ≈ time(π3 )∨time(π2 ) ≈ time(π3 ) .
The channel capacity property is a k-safety property
for k = q + 1 (in fact, the bound is tight [42, 43]), andthe timing channel property that we have been looking
at closely is a specialization where q = 1. Notice that
this k-safety property is ψccf -quotient partitionable with
ψccf (π1 , π2 , π3 ) , in(π1 )[ℓ] = in(π2 )[ℓ] = in(π3 )[ℓ],and the analysis closely resembles the one for the propertytcf(C) described earlier. In particular, following the sameline of thought as Example 7, properties Pf1 ,f2 (π) for highindependent functions f1 and f2 , where Pf1 ,f2 (π) holds iff
the running time of π is close enough to f1 (π) or f2 (π), aresuch that RBPS(Pf1 ,f2 , ccf) holds.

4. Symbolic Partitioning with Trails
The concept of ψ-quotient partitioning is semantic and naturally leads to the question of abstraction. This section introduces trails, a symbolic representation with which we can iteratively construct a trace partition for proving timing channel freedom, or finding a counterexample.
4.1 Definition
Given a program C and its Control Flow Graph (CFG) GC ,a trail expression tr is a regular expression where characters
represent the edges of GC , such that L(tr) is the set of strings
over the alphabet of the edges of GC that satisfy tr. We callboth the expressions as well as the set of strings they define
as trails, and use subscripted symbols tr for the expressionsand L(tr) to denote the set they define. Syntactically, a trail
tr is defined: tr ::= ǫ || b1b2 || tr1 |tr2 || tr1 · tr2 || tr∗ ,where L(ǫ) is the trail containing just the empty string, andfor each L(b1b2 ) represents a single letter of the alphabet
corresponding to the edge of GC from the block b1 to theblock b2 . The definition of L is defined inductively in theusual way. For example L(tr1 |tr2 ) is the set of strings thatare either in L(tr1 ) or L(tr2 ).
Given the CFG GC of a program C, we define the control flow graph automaton AC of C to be the automaton(Q, Σ, δ, q0 , F ) over the alphabet Σ = E(GC ) with set ofstates Q being the blocks of GC and where a transition exists form a state q to a state p with letter (q, p) exactly when
there is an edge e in GC from the block q to the block p. The
initial state q0 is the entry block of GC and the set of final
states F is a singleton containing the exit block of GC .
Given a program C, we say a trail is a most general trailof C, denoted trmg , if L(trmg ) = L(AC ), where L(AC )is the language recognized by the Control Flow Graph Automaton AC of C. Notice that the set of traces described bya trmg of C is always a (not necessarily strict) superset ofthe actual possible traces of C.
4.2 Annotating Trails with low and highWe now describe how we annotate the constructors of a trail,in particular the union (‘|’) and Kleene star (‘∗ ’) constructors, as low-dependent and/or high-dependent. As the procedure is the same for both low and high variables and dependent blocks, we consider only low-dependent blocks below.
We assume a taint-analysis module that, given a programC, returns a list of the variables in C and the blocks in the
CFG GC of C that are low-dependent, i.e., tainted. A block
can only be tainted if it is branching in some way. As a result,
there are exactly two outgoing edges from the block. We
assume a similar module for high-dependent variables andblocks.

Suppose that a block b of the CFG GC is marked as low-dependent, and let (b, b1 ) and (b, b2 ) be the two outgoingedges from block b. Then the constructor ‘|’ in a trail tr1 |tr2
is low-dependent with respect to b, if it is the outermost union
constructor such that for at least one of the two tri ’s, one of
the edges from b appears in the set of traces defined by it,
whereas the other edge does not. Similarly, the construct ‘∗ ’of a trail tr∗ is marked as low-dependent with respect to b, if
it is the outermost Kleene star constructor where one of theedges (b, bi ) is in the set of traces L(tr) and the other edge
is not. Formally, we have a recursive definition as to how
a trail constructor is marked as low/high-dependent (omitted
for lack of space).
If a union constructor of a trail is low-dependent, highdependent or both, we write ‘|l ’, ‘|h ’ or ‘|l,h ’ respectively.
Similarly for ‘∗ ’ constructs we write ‘∗l ’, ‘∗h ’ or ‘∗l,h ’ for thecorresponding scenarios.
4.3

Partition Refinement

We now describe a technique that, given a ψSC -quotientpartition T, constructs a new partition T′ that is also ψSC quotient, using a collection of pluggable strategies. In what
follows, we call a partition T safe if it is a ψSC -quotientpartition for ψSC (π1 , π2 ) , in(π1 ) =low in(π2 ) and wecall it vulnerable otherwise. A partition T′ is a refinementof a partition T if for all T ′ ∈ T′ there is T ∈ T such thatT′ ⊆ T.
One of the main goals of the algorithm is to produce
ψSC -quotient partitions. We do this using the annotations
on the trails and by representing a partition as a tree of trails
tr1 , . . . , trn , such that a trail tri is a child of a trail trj only
if L(tri ) ⊆ L(trj ). Any set of nodes of the tree with trails
tr1 , . . . , trn , forms a trail partition if L(tr1 ) ∪ . . . ∪ L(trn ) ⊇L(trmg ). As we described in Section 3, there is no need forthe partition components to be disjoint from each other, andwe don’t enforce such disjointness on the trails associatedwith the different nodes of the tree.
Suppose we have a trail tr = tr1 |l tr2 , where the union
constructor has been annotated as low-dependent with respect to some low variables l1 , . . . , lm . Consider then the partition {L(tr1 ), L(tr2 )} of L(tr). This partition can be seen tobe ψSC -quotient for the following reason. Suppose we have
two traces π1 and π2 . According to the definition of ψSC quotient partition, we want to make sure that if the low inputs of these two traces are the same, then they are both inL(tr1 ) or both in L(tr2 ). If this is the case though, it meansthat both traces agree on the variables l1 , . . . , lm , and thus all
traces will follow the same CFG edge, which in turn implies
that both π1 and π2 will either be in L(tr1 ) or in L(tr2 ).
We can apply a similar strategy for Kleene star constructors. We also take a similar approach for trails dependent onhigh data. We do this not when creating a partition to proveside-channel absence, but rather when trying to synthesize apossible attack when such a proof has failed.

safe

attack

yes
no

yes
no

CHECK
SAFE

REFINEPARTITION
safe

no moresafe
partitions

CHECK
ATTACK

REFINEPARTITION
vulnerable

unknownno morevulnerable
partitions

Figure 2. The overall algorithm.
4.4 Algorithm
The main procedure receives a program C as input, as
well as information about which variables and CFG blocks
are low/high (from a taint analysis) and attempts to provesafety. Failing at that, the algorithm tries to produce anattack specification. We further assume two procedures:
A NNOTATE T RAIL(tr) uses the annotated blocks of G to annotate the trail constructors of the input trail tr (Section 4.2);
B OUNDA NALYSIS(tr) calculates symbolic lower and upperbound expressions for the traces described by the input trailtr (Section 5). The main subprocedures of our algorithm are:
• R EFINE PARTITION(T, {safe, vulnerable}): Produces arefined partition T′ of T that is either safe or vulnerable, depending on the second argument. In Section 4.3,
details are given on how the partitions are extracted by
the tree of trails that is constructed and how the annotatedtrails obtained from A NNOTATE T RAIL are used to ensure
ψ-quotientability.
• C HECK S AFE(TS ): Returns yes if the given partition isverifiably safe, and no otherwise. For each partition component, this procedure employs B OUNDA NALYSIS, attempting to find symbolic upper and lower bounds forthe traces in the component. It returns yes if there is nocorrelation between high variables and running time.
• C HECK ATTACK(TV ): Similarly, this procedure returns
yes if there is a suspicion for an attack, and no otherwise. To this end, it attempts to either find a partition
component where B OUNDA NALYSIS calculates symbolic bounds that are correlated with high variables, oralternatively tries to find two components T1 and T2 ,such that T = T1 ⊎ T2 is not a ψSC -quotient partition,and the symbolic bounds of the two components differ
from each other (even if for each component individually the symbolic bounds obtained do not depend on highvariables).
The overall flow is as follows (depicted in Fig. 2 andillustrated in Section 2). The initial input to the algorithm
is the partition comprising only the component JCK, represented by the most general trail trmg . The procedure goes
into a first refinement loop, that (i) refines the partition into
a safe one (on the first iteration the partition {JCK} is left
unchanged), and (ii) sends the refined partition to the pro-

cedure C HECK S AFE. If the latter returns yes, the iteration
stops and outputs that the program is verifiably safe. If not,then the loop continues until either C HECK S AFE returns yes(and thus outputs that the program is safe and the algorithm
stops) or R EFINE PARTITION cannot further refine the given
partition into a safe one.
In the latter case, the algorithm enters a second refinement
loop, aimed at discovering an attack. It starts by having R E FINE PARTITION refine the given partition into a vulnerable
one, and then passes the new refined partition to C HECK ATTACK . Similarly, this loop continues until either C HECK ATTACK returns yes or R EFINE PARTITION fails to further refine the partition. In the first case, the algorithm outputs a setof possible attack specifications, and in the second case thealgorithm simply indicates that it failed to produce a meaningful summary.
In a sense, given enough strategies for R EFINE PARTI TION the procedure can continue indefinitely, but in practice we provide the procedure with parameters around thesize and form of the partitions produced, that would cause
the program to exit earlier, and without giving a concrete answer as to whether the program is safe or whether there is a
suspicion for an attack.

5.

Implementation

We have implemented our technique as the Blazer tool for
proving the absence of timing-channel vulnerabilities in Java
bytecode programs. To process bytecode, Blazer uses the
WALA front-end [39], which transforms bytecode into an
SSA-based CFG. We used the information flow (taint) analysis JOANA [33] in order to annotate blocks as to whether
branching depends on low (taint) or high (secret) variables.
For working with trails, Blazer uses the brics automaton
library [13] to check language inclusion and construct intersection, union, and complementation automata. We havewrapped this library with a translation between trails (described as regular expressions) and automata.
We have built a custom abstract interpreter on top of
WALA, using the Parma Polyhedra Library (PPL) [6] tocompute numerical invariants. The abstract interpreter canbe directed to restrict analysis to a given trail. We leverage the seeding technique [10] to compute transition invariants [30], and match these invariants against a databaseof complexity-bound lemmas [16, 17]. This embodied in
the B OUNDA NALYSIS component. While the abstract interpreter is interprocedural, B OUNDA NALYSIS currently relies
on manually-specified bound summaries for interprocedural
function calls. In the future, these summaries will be computed automatically.
When comparing running times of two nodes in the trails
tree, we need to know whether there is an observable difference between them. Blazer employs multiple approaches.
We have a generic component that computes the highest degree of the complexity bound polynomial, a rough heuristicthat works for many examples. In other cases, a platformspecific model of execution cost can be used. Here we makeassumptions about the maximum values of the input variables to compute the concrete number of instructions abound expression represents. Then the observable difference
between bounds can be defined as a threshold distance in
numbers of instructions. We currently use a simple machinemodel in which each bytecode instruction is counted as asingle unit.

6. Evaluation
We evaluated the implementation of Blazer on 24 benchmarks, including 6 examples drawn from the DARPA Space/Time Analysis for Cybersecurity (STAC) challenge problems [35] and 6 real-world programs in which timing attacks were exploited and reported in cryptography papers [15, 22, 29]. Benchmarks are paired up so that there are
two versions: the “unsafe” version is expected to be vulnerable to timing-channel attacks while the “safe” one is not. For
third-party benchmarks, we created safe versions by hand(except for User). Our experiment harness executes Blazer
on both the safe and unsafe versions of each benchmark.
6.1 Benchmarks
Our benchmarks, which reflect a broad range of code patterns, are up to 100 basic blocks in size (details reported laterin this section). Fig. 3 illustrates some selected examples.
• MicroBench. These are hand-crafted to exercise the var-ious aspects of Blazer. We start with simple examples;
nosecret_safe tests the basics of side-channel detection, which can only occur when there is a secret. The
others are more intricate. The loopAndBranch benchmark, for instance, is shown in Fig. 3. At first this seems
to have a vulnerability, but the potentially vulnerable trail
is infeasible, which is caught by the abstract interpreter.
Also shown in Fig. 3 is the classic Unix login vulnerability that leaks usernames. When line 7 is removed, theprogram takes longer when a username exists because ithashes the input password via md5.
• STAC. Several benchmarks were extracted from the
DARPA Space/Time Analysis for Cybersecurity (STAC)
engagement problems [35]. modPow1 (shown in Fig. 3)
and modPow2 perform cryptographic arithmetic using theJava BigInteger library.
• Literature. We have also crafted examples taken frompapers that demonstrate timing attacks on real-world
cryptographic methods. These include Genkin et al. [15](GPT), Kocher [22] (K96), and Pasareanu et al. [29]
(PPM16). The example from PPM16 is discussed in Section 2 and shown in Fig. 1.
Blazer supports manually-specified summaries of runningtimes so we specify running times for library calls suchas those to the Java BigInteger library (in modPow# and
Cryptography benchmarks).

1 void loopAndbranch_safe(int high, int low) {2 int i = high;
3 if(low < 0) { while(i > 0) i−−; }4 else {5
low = low + 10; // low is above 06if(low >= 10) { int j = high; while(j>0) j−−; }7else { if(high<0) { int k = high; while (k>0) k−−; } }8 }}1 boolean login_safe(String u, String p) {2 boolean outcome = false;
3 if (map.containsKey(u)) {4
if (map.get(u).equals(md5(p)))
5outcome = true;
6 } else {7
if (map.get(u).equals(md5(p))) { } // remove for unsafe
8 }9 return outcome; }1 BigInteger modPow1_safe(BigInteger base, BigInteger
exponent, BigInteger modulus) {2 BigInteger s = BigInteger.valueOf(1);3 int width = exponent.bitLength();
4 for (int i = 0; i < width; i++) {5
s = s.multiply(s).mod(modulus);6
if (exponent.testBit(width − i − 1))7s = s.multiply(base).mod(modulus);
8
else s.multiply(base).mod(modulus); // remove forunsafe9 }10 return s; }Figure 3. Some examples selected from the benchmarks.
For lack of space, only the main methods are shown.
Observer modeling. As discussed in the implementation
section, observable running time differences are modeled
in several ways. We designed the MicroBench so that distinguishing between safe and unsafe is possible by evaluating computational complexity, e.g., linear vs. quadratic. The
variables are assumed to be unbounded, while a safe program is assumed to be one where the symbolic running times
have the same polynomial degree. While sufficient for thesehand-crafted micro-benchmarks, this model of observability
is too simplistic for real-world code.
For the real-world examples from STAC and Literature,
we use a model of observable running time based on concrete differences in bytecode instructions between partitions.
We assume some reasonable maximum for the input variables, e.g., 4096 bits for the cryptographic benchmarks.
Then we plug these values into the symbolic bound expressions to get a concrete estimate of the maximum numberof bytecode instructions. Using this method, an observabledifference is defined by some minimum threshold in the difference between the number of instructions. For these benchmarks, we use a low number of instructions (25k) to define

BenchmarkMicroBencharray_safe
array_unsafe
loopBranch_safe
loopBranch_unsafe
nosecret_safe
notaint_unsafe
sanity_safe
sanity_unsafe
straightline_safe
straightline_unsafe
unixlogin_safe
unixlogin_unsafe
STAC
modPow1_safe
modPow1_unsafe
modPow2_safe
modPow2_unsafe
pwdEqual_safe
pwdEqual_unsafe
Literature
gpt14_safe
gpt14_unsafe
k96_safek96_unsafe
login_safe
login_unsafe

Size

SafetyTime (s)w/Attack
Time (s)

16
14
15
15
7
9
10
9
7
7
16
11

1.60
0.16
0.23
0.65
0.35
0.28
0.63
0.30
0.21
22.20
0.86
0.77

–
0.70
–
1.54
–
1.77
–
0.58
–
28.49
–
1.27

18
58
20
106
16
15

1.47
218.54
1.62
7813.68
2.70
1.30

–
464.52–31758.92
–
2.90

15
26
17
15
18
17

1.43
219.30
0.70
1.29
6.54
4.40

–
1554.64
–
3.14
–
9.10

Table 1. The results of applying our tool Blazer to a variety
of benchmarks: hand-made examples, examples from theliterature [15, 22, 29], and extracted from DARPA STAC
challenge problems. Median running times are shown forsafety verification alone as well as safety verification plus
the search for an attack specification. The safe benchmarks
need no search for attack specification, so they have – insteadof a running time.
the observable difference in running time. In real-world applications of this verification, observability depends on manyfactors, including hardware, operating system, network latency, etc, and would need to have application-specific calibration.
6.2 Results
The benchmarks were run sequentially on a single commodity PC with a quad-core 3.07GHz processor and 12GB of
RAM. Running time is collected for both safety verification
alone as well as safety verification plus the search for an
attack specification. The latter running time only applies tothe unsafe benchmark, since the tool halts if it proves safety.
Running time is measured by performing five runs and taking the median.

Table 1 shows the results. The Benchmark column identifies the benchmark’s method and alternates between thesafe and unsafe versions. Size indicates the number of basic blocks in the method’s control-flow graph. The Safety
Time column shows the tool’s median running time in seconds for safety verification alone, while the w/Attack Timecolumn is the median running for safety verification and thesubsequent search for an attack specification.
Our tool is sound: it either determines the program issafe, finds an attack specification, or gives up. For every safe
benchmark, Blazer verified the safety of the benchmark. In
all unsafe benchmarks, the tool found an attack specification,i.e., two candidate subtrails with differing running times,
except for gpt14_unsafe.
For most benchmarks, the safety verification takes only afew seconds, save some notable outliers. The running time
for generating an attack specification, which includes thesafety verification, often takes longer, because it is a computationally more intensive step. It takes the trails tree output from safety verification and further decomposing it into
subtrails.
As for the outliers, the running time appears loosely
related to the number of basic blocks in the program,as shown by the very high running times of the outliers
modPow1_unsafe, modPow2_unsafe, and gpt14_unsafe.
This is due to a combinatorial explosion of subtrails, superlinear with respect to the number of conditional branches, aswell as the increased memory pressure of storing and processing the tree o decomposed subtrails. The running time
for straightline_unsafe is an exception to this relationship: it has few basic blocks but a long running time. Thisis likely due to a particularly large basic block that has 90
instructions, increasing the processing time of the subtrails
that contain it.

7.

Related work

To the best of our knowledge, our approach is the first
method that tackles the timing channel freedom (TCF) verification problem by iteratively decomposing the problem
into sub-problems that require non-relational reasoning.
Type-based enforcement. TCF is a kind of noninterference: no matter the secret inputs to the program, the running times observable by adversary when given the same
set of non-secret inputs are (roughly) the same. Noninterference properties can be enforced by type systems. For example, work by Agat [1] uses a Volpano-Irvine-Smith-stylenon-interference type system [38] to transform a given program into one without timing channels (basically, by inserting padding no-op instructions in places identified by thetype system). The type-based approach can also be used
to check timing channel security, as shown by Hedin andSands [19]. Type-based enforcement is efficient but often
imprecise, falsely sounding the alarm on correct programs.

For example, here are two trivial examples that cannot be
typed with such approaches even though they are secure:1
2
3
4

void ex1(x,h) { if false { while (h < x) { h++; } }}void ex2(x,y) {if (h > x) { tick; } else { tick;tick;}if (h <= x) { tick; } else { tick;tick; } }Our technique is able to prove that these examples safe
because, through our use of trails, we can determine feasibility of different path cases. A more elaborate example
is the loopAndBranch micro-benchmark, shown in Fig. 3and discussed in Section 6. The safety of programs such as
loopAndBranch can depend on subtle conditions and ourstrategy of decomposition enables us to truly leverage invariants from abstract interpretation to this end.
Quantitative analysis. Quantitative information flow (QIF)
is a quantitative generalization of non-interference foundedon rigorous information-theoretic principles [4, 25, 32, 41](a channel is non-interferent iff its quantitative information
flow is zero). Recently, researchers have sought to apply QIF
to side channel security [14, 23, 29, 45]. For instance, Zhang
et al. [45] propose an approach that ensures the boundedness of the quantity of information leaked by the timing
channel. Their approach addresses low-level issues such as
cache uses, and comprises type-based analysis, hardware assistance, and predictive timing mitigation. The quantitative
approach is also taken in the work by Doychev et al. [14] ona static analysis for detecting leaks due to cache uses, andthe work by Pasareanu et al. [29] that quantifies information
leak amount via symbolic execution and model counting.
Due to its under-approximate nature, Pasareanu et al.’s technique is more suited to finding possible violations of TCF,
rather than verifying it.
Our analysis does not address the quantitative aspect oftiming channel security. However, ideas from our approach
may apply to them [42, 43], when viewed as k-safety problems (discussed more below). Moreover, our approach may
complement Pasareanu et al.: Our tool emits attack specifications that could be used to construct a slice of the program
where there is likely to be an attack, which can given as input
to their tool.
Self-composition. Generally speaking, TCF is a 2-safety
property in that it relates 2 executions. In particular, it relates all pairs of executions such that if they agree on nonsecret inputs then they (roughy) agree on running time. A
general approach to verifying k-safety properties (which relate k ≥ 2 executions) is to use self-composition [7, 12,27, 36, 37, 43]. The approach reduces the k-safety problem
to a 1-safety problem by composing (sequentially, in parallel, or in an interleaving fashion [27, 36, 37]) k copiesof the given program prior to applying a (standard) verification technique. More precisely, the k-safety problem∀π1 , . . . , πk ∈ JCKk .Φ(π1 , . . . , πk ) is reduced to the 1safety problem ∀π ∈ JC (k) K.Φ(π(1) , . . . , π(k) ) where C (k)is the composed program whose execution trace is a k-tupleof (copies of) C’s execution traces and π(i) projects the ith trace in the composite trace π. The approach is clearlysound and complete for arbitrary k-safety properties, relative to the soundness and completeness of the backend (1)safety verifier. However, it trades robustness for scalability
due to the rather brute force reduction, and the naïve selfcomposition approach only scales to relatively simple examples when paired with an automatic backend safety verifier.
Almedia et al. [2] have pursued the self-compositionbased approach to timing channel security verification inparticular, with mixed results. More recently, they haveproposed to check if a program is constant-time by selfcomposition [3]. A program being constant-time is a stronger
requirement than timing channel security, and it requires the
program’s control flow to be independent of the high security data. The strict requirement can be exploited to form atightly coupled self-composition, thereby allowing efficientverification [27, 36, 37] (further discussed below).
Other methods for relational reasoning. Other methods
have also been considered for verifying k-safety (and, moregenerally, relational) problems. Closely related to the selfcomposition approach is the recent work by Sousa and Dillig [34]. Similar to self-composition, their approach (implicitly) creates k copies of the program, but attempts to synchronize the verification’s reasoning process so that it keeps
the program flow of the different copies in lockstep as muchas possible. This is done via intricate program logic rulesthat they call Cartesian Hoare Logic. Similar to the interleaving self-composition technique [27, 36, 37], such a lockstep reasoning improves the performance of the approach by
more tightly coupling the key invariants across the program
copies. Relational program logics pre-date Cartesian Hoare
Logic and can be traced back to the product programs of
Reynolds [31]. More recently, Benton introduced relational
logics for program transformations and equivalence [9], andYang provided a relational version of separation logic [40].
Other recent uses of product programs for program equivalence include [28, 44]. Also, a recent work by Assaf et al. [5]proposes to verify k-safety (and more general hyper-safety)
problems via an abstract interpretation over program trace
sets (as opposed to traces), which may be understood as an
abstract interpretation over a (possibly unbounded) productof program copies. Recent work by Çiçek et al. on relational
cost analysis [11] describes a program analysis for checking and inferring resource-usage properties spanning multiple programs. Such an analysis can potentially be used forproving timing channel security by applying it to the program copies.
In contrast to self composition and its related variants
discussed above, the method proposed in this paper doesnot (explicitly or implicitly) make program copies and reduce the problem to a 1-safety problem. Instead, it decomposes the given program by utilizing a certain decomposi-tion property of the target k-safety problem that we call ψquotient partitionability. This way, we obtain the answer for
the whole by solving the decomposed sub-problems. Note
that, in our approach, a non-relational analysis (i.e., 1-safety
verification) is not applied to the self-composed programthat completely expresses the original k-safety problem, butinstead, it is applied to decomposed sub-problems of theoriginal.
Path sensitivity. Our trails act as specifications for how
a program can be restricted based on certain branching
choices. This is similar to path sensitivity approaches suchas trace partitioning [26]. Similarly, PAGAI [21] employsa technique called path focusing [20] to guide an abstract
interpreter to consider certain paths at a time. In comparison to control-flow refinement (CFR) [17] our trails are ageneralization: we allow more complicated forms of loop
unrolling (arbitrary regexes) and trails may eliminate executions whereas CFR always encompasses all executions.
To our knowledge, none of the above approaches have beenused to reason about relational properties, permit low-vshigh annotations, nor define a decomposition that reduces arelational property to trail/path (i.e., trace) properties.

8. Conclusion
We have presented a novel technique for proving that a program is free of timing channels. Our approach, which wehave proved sound, is based on a general decomposition
technique that reduces k-safety verification (timing channel
freedom has k = 2) to a task fit for a non-relational analysis. Our decomposition proceeds iteratively by symbolicallysynthesizing path-based partitions (“trails”) that case-split ininstances of taint-based or secret-based branching. The former is used to prove timing channel freedom, while the latter helps identify particular vulnerabilities. We implemented
our approach in a tool called Blazer and demonstrated its
effectiveness on a collection of 25 benchmark examples, including 6 drawn from the STAC challenge problems and 7
from the cryptography literature. We believe that our decomposition sets the stage for the development of more powerfulrelational analyses and/or other k-safety property verifiers.
Acknowledgments. We thank Sharon Shoham, our shepherd, for helpful comments and suggestions. This research
was supported in part by the National Science Foundation
under grant CNS-1314857; by MEXT Kakenhi 17H01720,
and JSPS Core-to-Core Program, A.Advanced Research
Networks; and by DARPA under contracts FA8750-15-20104 and FA8750-16-C-0022.

References[1] J. Agat. Transforming out timing leaks. In POPL, 2000.
[2] J. B. Almeida, M. Barbosa, J. S. Pinto, and B. Vieira. Formal verification of side-channel countermeasures using selfcomposition. Science of Computer Programming, 78(7),2013.

[3] J. B. Almeida, M. Barbosa, G. Barthe, F. Dupressoir, and
M. Emmi. Verifying constant-time implementations. In
USENIX Security Symposium, 2016.

[24] S. Langkemper. The password guessing bug in Tenex.
https://www.sjoerdlangkemper.nl/2016/11/01/
tenex-password-bug/, 2016.

[4] M. S. Alvim, K. Chatzikokolakis, C. Palamidessi, and
G. Smith. Measuring information leakage using generalized
gain functions. In CSF, 2012.

[25] P. Malacaria. Assessing security threats of looping constructs.
In POPL, 2007.

[5] M. Assaf, D. A. Naumann, J. Signoles, E. Totel, and F. Tronel.
Hypercollecting semantics and its application to static analysis of information flow. In POPL, 2017.
[6] R. Bagnara, P. M. Hill, and E. Zaffanella. The Parma Polyhedra Library: Toward a complete set of numerical abstractions
for the analysis and verification of hardware and software systems. Science of Compututer Programming, 72(1-2), 2008.
[7] G. Barthe, P. R. D’Argenio, and T. Rezk. Secure information
flow by self-composition. In CSFW, 2004.
[8] G. Barthe, J. M. Crespo, and C. Kunz. Relational verification
using product programs. In FM, 2011.

[26] L. Mauborgne and X. Rival. Trace partitioning in abstract
interpretation based static analyzers. In ESOP, 2005.
[27] D. A. Naumann. From coupling relations to mated invariants
for checking information flow. In ESORICS, 2006.
[28] N. Partush and E. Yahav. Abstract semantic differencing fornumerical programs. In SAS, 2013.
[29] C. S. Pasareanu, Q. Phan, and P. Malacaria. Multi-run sidechannel analysis using symbolic execution and max-SMT. In
CSF, 2016.
[30] A. Podelski and A. Rybalchenko. Transition invariants. In
LICS, 2004.

[9] N. Benton. Simple relational correctness proofs for static
analyses and program transformations. In POPL, 2004.

[31] J. C. Reynolds. The Craft of Programming. Prentice HallInternational series in computer science. Prentice Hall, 1981.

[10] J. Berdine, A. Chawdhary, B. Cook, D. Distefano, and P. W.
O’Hearn. Variance analyses from invariance analyses. In
POPL, 2007.

[32] G. Smith. On the foundations of quantitative information flow.
In FOSSACS, 2009.

[11] E. Çiçek, G. Barthe, M. Gaboardi, D. Garg, and J. Hoffmann.
Relational cost analysis. In POPL, 2017.
[12] Á. Darvas, R. Hähnle, and D. Sands. A theorem proving
approach to analysis of secure information flow. In SPC, 2005.
[13] dk.brics.automaton. Finite-state automata and regular expressions for Java. http://www.brics.dk/automaton/, 2017.
[14] G. Doychev, B. Köpf, L. Mauborgne, and J. Reineke.
CacheAudit: A tool for the static analysis of cache side channels. ACM Transactions on Information and System Security,
18(1), 2015.

[33] G. Snelting, D. Giffhorn, J. Graf, C. Hammer, M. Hecker,
M. Mohr, and D. Wasserrab. Checking probabilistic noninterference using JOANA. it - Information Technology, 56(6),2014.
[34] M. Sousa and I. Dillig. Cartesian Hoare logic for verifying
k-safety properties. In PLDI, 2016.
[35] STAC.
DARPA space/time analysis for cybersecurity(STAC) program.
http://www.darpa.mil/program/
space-time-analysis-for-cybersecurity, 2017.
[36] T. Terauchi and A. Aiken. Secure information flow as a safety
problem. In SAS, 2005.

[15] D. Genkin, I. Pipman, and E. Tromer. Get your hands off mylaptop: Physical side-channel key-extraction attacks on PCs.
In CHES, 2014.

[37] H. Unno, N. Kobayashi, and A. Yonezawa. Combining typebased analysis and model checking for finding counterexamples against non-interference. In PLAS, 2006.

[16] S. Gulwani and F. Zuleger. The reachability-bound problem.
In PLDI, 2010.

[38] D. M. Volpano, C. E. Irvine, and G. Smith. A sound type system for secure flow analysis. Journal of Computer Security, 4(2/3), 1996.

[17] S. Gulwani, S. Jain, and E. Koskinen. Control-flow refinement
and progress invariants for bound analysis. In PLDI, 2009.
[18] S. Gulwani, K. K. Mehra, and T. M. Chilimbi. SPEED: precise and efficient static estimation of program computational
complexity. In POPL, 2009.
[19] D. Hedin and D. Sands. Timing aware information flow security for a JavaCard-like bytecode. In Workshop on Bytecode
Semantics, Verification, Analysis and Transformation, 2005.
[20] J. Henry. Static analysis by path focusing. Master’s thesis,
Grenoble INP, 2011.
[21] J. Henry, D. Monniaux, and M. Moy. PAGAI: A path sensitive
static analyser. In TAPAS, 2012.
[22] P. C. Kocher. Timing attacks on implementations of DiffieHellman, RSA, DSS, and other systems. In CRYPTO, 1996.
[23] B. Köpf and D. A. Basin. Automatically deriving informationtheoretic bounds for adaptive side-channel attacks. Journal ofComputer Security, 19(1), 2011.

[39] WALA. IBM T.J. Watson Libraries for Analysis (WALA).
http://wala.sourceforge.net/, 2017.
[40] H. Yang. Relational separation logic. Theoretical Computer
Science, 375(1-3), 2007.
[41] H. Yasuoka and T. Terauchi. Quantitative information flow verification hardness and possibilities. In CSF, 2010.
[42] H. Yasuoka and T. Terauchi. On bounding problems of quantitative information flow. Journal of Computer Security, 19(6), 2011.
[43] H. Yasuoka and T. Terauchi. Quantitative information flow
as safety and liveness hyperproperties. Theoretical Computer
Science, 538, 2014.
[44] A. Zaks and A. Pnueli. CoVaC: Compiler validation by program analysis of the cross-product. In FM, 2008.
[45] D. Zhang, A. Askarov, and A. C. Myers. Language-based
control and mitigation of timing channels. In PLDI, 2012.