Quantitative Information Flow
for Scheduler-Dependent Systems ∗
Yusuke Kawamoto

Thomas Given-Wilson

Inria Saclay & LIX, École Polytechnique, France

Inria, France

Quantitative information flow analyses measure how much information on secrets is leaked by publicly observable outputs. One area of interest is to quantify and estimate the information leakage of
composed systems. Prior work has focused on running disjoint component systems in parallel and
reasoning about the leakage compositionally, but has not explored how the component systems are
run in parallel or how the leakage of composed systems can be minimised. In this paper we consider
the manner in which parallel systems can be combined or scheduled. This considers the effects of
scheduling channels where resources may be shared, or whether the outputs may be incrementally
observed. We also generalise the attacker’s capability, of observing outputs of the system, to consider
attackers who may be imperfect in their observations, e.g. when outputs may be confused with one
another, or when assessing the time taken for an output to appear. Our main contribution is to present
how scheduling and observation effect information leakage properties. In particular, that scheduling
can hide some leaked information from perfect observers, while some scheduling may reveal secret
information that is hidden to imperfect observers. In addition we present an algorithm to construct a
scheduler that minimises the min-entropy leakage and min-capacity in the presence of any observer.

1

Introduction

Preventing the leakage of confidential information is an important goal in research of information security. When some information leakage is unavoidable in practice, the next step is to quantify and reduce
the leakage. Recently theories and tools on quantitative information flow have been developed using
information theory to address these issues [17, 7, 23, 12, 25, 8, 16, 15]. The common approach is to
model systems as information-theoretic channels that receive secret input and returns observable output.
One area of interest is to quantify and estimate the information leakage of composed systems. When
composing systems the manner of reasoning about their behaviour is non-trivial and is complicated by
many factors. One of the first approaches is to consider the (disjoint) parallel composition, that is, simply
running the component systems independently and regarding them as a single composed system. This
approach provides some general behaviour and reasoning about the whole composed system, as shown
in the research of quantitative information flow with different operational scenarios of attack [5, 19,
20]. However, the parallel composition approach is coarse-grained and abstracts many of the channels’
behaviours that may lead to changes in information leakage. Although this approach provides useful
results on the bounds of possible leakage, it does so under the assumption that the component channels
are executed independently and observed separately. That is, their outputs can always be linked to the
disjoint component channels, and that both their outputs are observed simultaneously and without any
interleaving or reflection of how the component channels achieved their outputs.
∗ This

work has been partially supported by the project ANR-12-IS02-001 PACE, by the INRIA Equipe Associée
PRINCESS, by the INRIA Large Scale Initiative CAPPRIS, and by EU grant agreement no. 295261 (MEALS). The work
of Yusuke Kawamoto has been supported by a postdoc grant funded by the IDEX Digital Society project.

N. Bertrand and M. Tribastone (Eds.): QAPL 2015
EPTCS 194, 2015, pp. 48–62, doi:10.4204/EPTCS.194.4

c Y. Kawamoto & T. Given-Wilson
This work is licensed under the
Creative Commons Attribution License.

Y. Kawamoto & T. Given-Wilson

49

Here we take a more fine-grained approach where we consider that channels may provide a sequence
of observable actions. Thus, a channel may be observed to output a sequence of actions, or the passage
of time may be observed to pass between the initiation of the channel and a final output. This captures
more mechanics of real world systems and allows for greater refined reasoning about their behaviour.
Such sequences of observable actions also allow a more subtle approach to combining channels in
parallel. Rather than simply taking both outputs to appear together at the termination of their operations,
observations can be made of the sequence in which the outputs appear. Such a combination of channels
becomes parametrised by a scheduler, that informs on how to combine the observable sequences of actions into a single sequence. This can then represent very direct behaviour such as scheduling properties
of a shared CPU, or abstract behaviours such as routing properties, vote counting, etc.
The other novel approach presented here is the refinement of the attacker’s capability of observing the
outputs of systems. We model attackers that may have imperfect observability: they may not accurately
detect differences in outputs, or may do so only probabilistically. This captures, for example, the situation
where the attacker may be blind to some internal behaviour that other agents can detect. In this paper
such imperfect observations are modeled using what we call observer channels. This formalisation
enables us to consider a large class of observers, including probabilistic observers, which have never
been considered in the previous studies on quantitative information flow.
These refinements to composing information-theoretic channels allow us to reason about behaviours
that may be obvious, but not captured by previous approaches. In this paper we present three kinds of results regarding the effect of leakage properties due to the considering of schedulers and observers. First,
since scheduled composition can alter the leakage relative to the parallel composition, we present theorems for detecting when a scheduled composition does not alter the relative information leakage. This
means some preliminary analysis may be sufficient to determine when scheduled composition may be
worthy of further consideration. Second, scheduled composition can leak more or less information than
the parallel composition depending on the properties of the channels and the power of the observer. Although the potential effect on leakage is dependent upon many factors, we present results that determine
an upper bound for the leakage of a schedule-composed channel. Third, we present results for finding a
scheduler that minimises the min-entropy leakage and min-capacity in the presence of any observer. We
present how to construct such a scheduler by solving a linear programming problem.
In addition we evaluate our model and results with some simple yet intuitive examples, such as mix
networks for voter anonymity, and side-channel attacks against cryptographic algorithms. We provide
an implementation that can be used to calculate the behaviours of information-theoretic channels, schedulers, and observers as presented here. The implementation is available online [1], which requires the
libraries leakiEst tool [14] and the linear programming system lp solve [2].
The rest of the paper is structured as follows. Section 2 recalls the definitions of information-theoretic
channels and measures of information leakage. Section 3 defines traces, systems and channel compositions, and shows examples of schedulers. Section 4 introduces the notion of generalised observers
and defines the observed leakage. Section 5 presents our main results in a general manner. Section 6
applies these results to well known problems. Section 7 discusses some related work. Section 8 draws
conclusions and discusses future work. All proofs can be found in [21].

2

Preliminaries

2.1 Information-Theoretic Channel
Systems are modeled as information-theoretic channels to quantify information leakage using information theory. A channel K is defined as a triple (X , Y ,C) consisting of a finite set X of secret input

Quantitative Information Flow for Scheduler-Dependent Systems

50

values, a finite set Y of observable output values, and a channel matrix C each of whose row represents
a probability distribution; i.e., for all x ∈ X and y ∈ Y , 0 ≤ C[x, y] ≤ 1 and ∑y′ ∈Y C[x, y′ ] = 1. For each
x ∈ X and y ∈ Y , C[x, y] is a conditional probability p(y|x) of observing y when the secret of the system
is x. We assume some secret distribution π on X , which is also called a prior. Given a prior π on X , the
joint distribution of having a secret x ∈ X and an observable y ∈ Y is defined by p(x, y) = π [x]C[x, y].

2.2 Quantitative Information Leakage Measures
In this section we recall the definitions of two popular quantitative information leakage measures.
Mutual information is a leakage measure based on the Shannon entropy of the secret distribution.
Definition 1 Given a prior π on X and a channel K = (X , Y ,C), the mutual information I (π , K )
w.r.t. π and K is defined by:


C[x, y]
I (π , K ) = ∑ π [x]C[x, y] log
.
∑y′ ∈Y C[x, y′ ]
x∈X ,y∈Y
Then the Shannon’s channel-capacity S C (K ) of a channel K is given by max I (π , K ) where π
π

ranges over all distributions on X .

Min-entropy leakage quantifies information leakage under single-attempt guessing attacks [9, 25].
Definition 2 Given a prior π on X , and a channel K = (X , Y ,C), the prior vulnerability V (π ) and
the posterior vulnerability V (π , K ) are defined respectively as
V (π ) = max π [x]
x∈X

and V (π , K ) =

∑ max π [x]C[x, y].

y∈Y x∈X

Then the min-entropy leakage L (π , K ) and the min-capacity M C (K ) are defined by:
L (π , K ) = − logV (π ) + logV (π , K ) and

3

M C (K ) = sup L (π , K ).
π

Information Leakage of Scheduler-Dependent Systems

3.1 Traces and Systems
In general the output of an information-theoretic channel can be defined in many different ways. In this
work we consider traces, or sequences of actions, as observable values. Assume a countable set of names
denoted m, m′ , m1 , m2 , . . . and a countable set of values v, v1 , v′ , . . .. We define an action by µ , α , β ::=
τ | mhvi . Here τ denotes the traditional silent or internal action that contains no further information.
The output action mhvi can be considered to exhibit some value v via some named mechanism m. In
concurrency theory the output action typically refers to the the named mechanism as a channel name,
which is distinct from the notion of information-theoretic channel used here. Here the output action is
used in a more general sense, in that mhvi exhibits some value v such as runtime measured via mechanism
m. For example, v could be runtime, electronic power usage or other value determined by the input, and
m could be via direct communication/circuitry, indirect side effects, or any other means.
A trace is defined to be a sequence of actions of the form µ1 .µ2 . . . . .µi . The notation α ∈ µ1 .µ2 . . . . .µi
denotes that there exists a j ∈ {1, 2, . . . , i} such that µ j = α . Similarly a sequence of i actions µ can be
/ A system is modeled as an information-theoretic
denoted µ i , and an empty sequence of actions by 0.
channel (X , Y ,C) where |X | is finite and the set Y of observables is a finite set of traces.

Y. Kawamoto & T. Given-Wilson
C1 ×C2
Y1✲
X1 ✲
C1
X2 ✲

C2

Y2✲

(a) Parallel composition

51
X1 ✲
X2 ✲

CompS (C1 ,C2 )
Y1✲
C1
Y2✲ S
C2

Y✲

Obs

Z✲

(b) Observation of a scheduled composition

Figure 1: Parallel composition and scheduled composition

3.2 Scheduled Composition
In this section we model scheduler-dependent systems by introducing the notion of a scheduled composition of information-theoretic channels, which interleaves outputs from different channels.
In [20] the parallel composition K1 × K2 of two component channels K1 and K2 is defined as a
channel that outputs ordered pairs consisting of the outputs of the two component channels. That is,
given two component channels K1 = (X1 , Y1 ,C1 ) and K2 = (X2 , Y2 ,C2 ), the outputs of their parallel
composition range over the ordered pairs (y1 , y2 ) for all y1 ∈ Y1 and y2 ∈ Y2 . This composition can be
modeled using a scheduler that allows K1 to perform the whole sequence y1 of actions and some action
sep 6∈ Y1 ∪ Y2 (for separating y1 from y2 ) before K2 performs the actions in y2 .1 In this setting we can
recognise which component channel each output of the composed channel came out of.
In this paper we consider more fine-grained schedulers that may allow K2 to perform some actions
before K1 completes the whole sequence of actions. To model such schedulers, we define the set of
possible interleaving of two traces that preserves the orders of occurrences of actions in the traces.
Definition 3 (Interleaving of traces) Let us consider two traces y1 of the form α1 .α2 . . . . .αk and y2
of the form β1 .β2 . . . . .βl . The interleaving Int(y1 , y2 ) of y1 and y2 is the set of all traces of the form
µ1 .µ2 . . . . .µk+l s.t., for two sequences of distinct integers 1 ≤ i1 < i2 < . . . < ik ≤ k + l and 1 ≤ j1 < j2 <
. . . < jl ≤ k + l, we have µim = αm for all m = 1, 2, . . . , k and µ jm = βm for all m = 1, 2, . . . , l.
Definition 4 For two sets Y1 , Y2 of observables, the interleaving Int(Y1 , Y2 ) over Y1 and Y2 is defined
S
by Int(Y1 , Y2 ) = y1 ∈Y1 ,y2 ∈Y2 Int(y1 , y2 ). The definition of interleaving is extended from two traces to n
S
traces as follows: Int(y1 , y2 , . . . , yn ) = y′ ∈Int(y2 ,...,yn ) Int(y1 , y′ ). For n sets Y1 , Y2 , . . . , Yn of observables,
the interleaving Int(Y1 , Y2 , . . . , Yn ) is defined analogously.
Although the interleaving defines all possible combinations of the sets of traces, they do not define
the probability of their appearance. To reason about this, we define a scheduler that takes two sets of
traces and probabilistically schedules their actions to form each possible trace in their interleaving.
Definition 5 (Scheduler) A scheduler S on Y1 and Y2 is a function that, given two traces y1 ∈ Y1 and
y2 ∈ Y2 , produces a probability distribution over all the possible interleaving Int(y1 , y2 ). We denote by
S (y1 , y2 )[y] the conditional probability of having an interleaved trace y given y1 and y2 .
We define a deterministic scheduler as one that produces the same output for any given two traces.
Definition 6 (Deterministic scheduler) A scheduler S is deterministic if for any two traces y1 and y2 ,
there exists y ∈ Int(y1 , y2 ) such that S (y1 , y2 )[y] = 1.
This provides the basis for composing channels in general, however this requires some delicacy
since the interleaving of different traces may produce the same result. For example, given y1 = τ .mhsi
and y2 = τ then one of the possible traces produced is τ .τ .mhsi. However, given y3 = mhsi and y4 = τ .τ
then the same trace τ .τ .mhsi could also be produced.
1 Formally,

we introduce Ksep = ({sep}, {sep}, (1)) to consider the sequential execution of K1 , Ksep and K2 in this order.

Quantitative Information Flow for Scheduler-Dependent Systems

52

observable
m2 h0i τ .m2 h0i m2 h1i τ .m2 h1i

observable
m1 h0i τ .m1 h0i m1 h1i τ .m1 h1i
secret

0
1

0.5
0

0
0.5

0
0.5

0.5
0

secret

Table 1: Channel matrix C1

0
1

0
0.5

0.5
0

0.5
0

0
0.5

Table 2: Channel matrix C2

Let p(y1 , y2 ) be the joint probability that two component channels output two traces y1 and y2 .
Then the probability that S produces an interleaved trace y is given by: p(y) = ∑y1 ∈Y1 ,y2 ∈Y2 p(y1 , y2 ) ·
S (y1 , y2 )[y]. By [20] we obtain C1 [x1 , y1 ]C2 [x2 , y2 ] = p(y1 , y2 |x1 , x2 ). Hence we can define scheduled
composition of channels as follows.
Definition 7 (Scheduled composition of channels) The scheduled composition of two channels K1 =
(X1 , Y2 ,C1 ) and K2 = (X2 , Y2 ,C2 ) with respect to a scheduler S is define as the channel (X1 ×
X2 , Int(Y1 , Y2 ),C) where the matrix element for x1 ∈ X1 , x2 ∈ X2 and y ∈ Int(Y1 , Y2 ) is given by:
C[(x1 , x2 ), y] = ∑y1 ∈Y1 ,y2 ∈Y2 C1 [x1 , y1 ]C2 [x2 , y2 ]S (y1 , y2 )[y].
We denote this scheduled composition by CompS (K1 , K2 ). Note that the scheduled composition of n
channels can be defined by adapting the scheduler S to operate over n traces in the obvious manner.

3.3 Examples of Scheduled Composition
This section presents some example channels and schedulers that illustrate the main results of this paper.
For simplicity they shall all limit their secrets to the set XB = {0, 1}, and their outputs to the set Ym =
{mh0i, τ .mh0i, mh1i, τ .mh1i} for a parameter m.
Consider the channel K1 = (XB , Ym1 ,C1 ) where C1 is given by Table 1. This channel can be considered as one that half the time simply outputs the secret via m1 hsi and half the time outputs the exclusive-or
⊕ of the secret with 1 as in τ .m1 hs⊕ 1i, with the τ representing the calculation effort. Note that this channel leaks 100% of the information about the secret. Also consider the channel K2 = (XB , Ym2 ,C2 ) where
C2 is given by Table 2. This channel is similar to K1 , except that the internal action τ is observable when
disclosing the secret rather than its exclusive-or. Again this channel leaks all the secret information.
When combining channels the rôle of the scheduler is very significant with respect to the information
leakage. This section defines three types of simple schedulers for illustrating the results here.
The simplest scheduler is one that outputs the first and second observable outputs concatenated,
i.e. given y1 and y2 outputs y1 .y2 .
Definition 8 The (left-first) deterministic sequential scheduler SDS is defined as follows: SDS (y1 , y2 )[y]
is 1 if y = y1 .y2 and 0 otherwise where y1 ∈ Y1 , y2 ∈ Y2 and y ∈ Y .
Example 1 The scheduled composition CompSDS (K1 , K2 ) w.r.t. SDS has the same information leakage
as the parallel composition K1 × K2 . This can be shown since it follows from the definition of SDS that,
for each y ∈ Y , SDS uniquely identifies a pair (y1 , y2 ) of outputs. For instance, let us consider the prior
distribution π on X1 × X2 defined by (0.15, 0.20, 0.30, 0.35). Then, for both of the composed channels,
the mutual information is about 1.926 and the min-entropy leakage is about 1.515.
Next is the fair sequential scheduler SFS that fairly chooses between the first or second observable
and produces that in its entirety before producing the other.
Definition 9 The fair sequential scheduler SFS is defined by

Y. Kawamoto & T. Given-Wilson

SFS (y1 , y2 )[y]

53

def

=



 1
0.5


0

if y1 = y2 ∧ y = y1 .y2
if y1 6= y2 ∧ (y = y1 .y2 ∨ y = y2 .y1 )
otherwise.

Similar to the deterministic sequential scheduler, the information leakage can be proven to be equal to
that of the parallel composition of channels for this example.
Example 2 The scheduled composition CompSFS (K1 , K2 ) w.r.t. SFS has the same information leakage
as the parallel composition K1 × K2 . This can be shown similarly to Example 1.
Note that the leakage preservation does not hold in general as illustrated in the following example.
Example 3 Consider when Y1 = {τ , τ .τ } and Y2 = {mh0i, τ .mh0i}. The observed output τ .τ .mh0i can
arise from S (τ , τ .mh0i) and S (τ .τ , mh0i), where S can be SDS or SFS . Thus, both the schedulers
SDS and SFS may allow less information leakage than the parallel composition.
The third example scheduler is the fair interleaving scheduler SFI that evenly chooses the next action
from the two observables.
Definition 10 The fair interleaving scheduler SFI is recursively defined as


0.5SFI (y′1 , y2 )[y′ ]





 0.5SFI (y1 , y′2 )[y′ ]
def
SFI (y1 , y2 )[y] =
0.5SFI (y′1 , y2 )[y′ ] + 0.5SFI (y1 , y′2 )[y′ ]




1



0

if y = α .y′ ∧ y1 = α .y′1 ∧ y2 = β .y′2 ∧ α 6= β
if y = β .y′ ∧ y1 = α .y′1 ∧ y2 = β .y′2 ∧ α 6= β
if y = α .y′ ∧ y1 = α .y′1 ∧ y2 = α .y′2
if (y = y1 ∧ y2 = 0)
/ ∨ (y = y2 ∧ y1 = 0)
/
otherwise.

The fair interleaving scheduler SFI turns out to often have impact on the leakage compared to the parallel
composition of channels. This can occur in a variety of ways and shall be explored in detail later.
Example 4 The scheduled composition CompSF (K1 , K2 ) w.r.t. SFI has less information leakage than
the parallel composition K1 × K2 . This can be shown by considering when the output y is of the form
τ .m1 h0i.m2 h0i, which can arise from both SFI (τ .m1 h0i, m2 h0i) and SFI (m1 h0i, τ .m2 h0i). Since y does
not uniquely identify the outputs y1 and y2 , SFI could allow less leakage than the parallel composition.
For instance, for the prior (0.15, 0.20, 0.30, 0.35), the mutual information of the scheduled composition
w.r.t. SFI is 1.695. This is less than those of the parallel composition and scheduled composition w.r.t.
SDS in Example 1 (both 1.926), thus the scheduler here alone is responsible for reducing the leakage.

4

Information Leakage to Observers

4.1 Observers
Many kinds of capabilities of observing systems have been considered; e.g. an observer for strong bisimulation ∼s can recognise the internal action: τ .mhvi 6∼s mhvi, while one for weak bisimulation ∼w cannot:
τ .mhvi ∼w mhvi. To model different kinds of capabilities of observation, we define an observer’s views
Z as the set of values recognised by the observer. For example, τ .mhvi and mhvi fall into two different
views to an observer for strong bisimulation, but to the same view to an observer for weak bisimulation.
We formalise the notion of an observer using a matrix that defines relationships between observable outputs of systems and the observer’s views. In particular, we allow for probabilistic accuracy in
observation; that is the observer may not be perfectly accurate in identifying an output.

54

Quantitative Information Flow for Scheduler-Dependent Systems

Definition 11 (Generalised observer) An observer O is defined as a triple (Y , Z , Obs) consisting of a
finite set Y of observables, a finite set Z of observer’s views and an observer matrix Obs each of whose
row represents a probability distribution; i.e., for all y ∈ Y we have ∑z∈Z Obs[y, z] = 1. Each matrix
element Obs[y, z] represents the probability that the observer has the view z when the actual output is y.
The observation matrix Obs describes the capability of the attacker to distinguish between traces.
This capability of observation has been formalised as an equivalence relation between states of a system
in prior work [6]. In fact, an equivalence relation ∼ between traces characterises a class of observers.
Definition 12 (∼-observer) Given an equivalence relation ∼ on Y , an observer (Y , Z , Obs) is called
a ∼-observer if, for all y1 , y2 ∈ Y , y1 ∼ y2 is logically equivalent to Obs[y1 , z] = Obs[y2 , z] for all z ∈ Z.
For instance, we can consider the ∼s -observer for strong bisimulation ∼s and the ∼w -observer for
weak bisimulation ∼w . Observe that ∼s is the identity relation on traces here. Further, note that for every
observer O, there exists an equivalence relation ∼ between traces such that O is a ∼-observer. This
def
equivalence relation ∼ is defined by the following: ∼ = {(y1 , y2 ) ∈ Y × Y | for all z ∈ Z, Obs[y1 , z] =
Obs[y2 , z]}. On the other hand, the observation matrix is not uniquely determined by the equivalence
relation and therefore can express a wider range of observers’ capabilities than the equivalence relation.
Among ∼-observers, we often consider observers that always have the same view on the same trace.
Definition 13 (Deterministic observer) We say that an observer (Y , Z , Obs) is deterministic if each
probability in Obs is either 0 or 1; i.e., for all y ∈ Y , there exists a unique z ∈ Z such that Obs[y, z] = 1.
For any deterministic ∼-observer (Y , Z , Obs) and any y1 , y2 ∈ Y , we have y1 ∼ y2 iff, for all
z ∈ Z , we have Obs[y1 , z] = Obs[y2 , z] ∈ {0, 1}. Then this observer always detects the equivalence class
[y]∼ of the output y from any given view z. For this reason, when defining a deterministic ∼-observer,
we typically take the set Z of views as the quotient set of Y by ∼, and for any y ∈ Y and z ∈ Z ,
Obs[y, z] = 1 iff z = [y]∼ . For example, consider the deterministic observers corresponding to ∼s .
Example 5 (Deterministic ∼s -observer) A deterministic ∼s -observer (Y , Z , Obs) satisfies the property that, for any distinct y1 , y2 ∈ Y , there exists a z ∈ Z such that either Obs[y1 , z] = 0 and Obs[y2 , z] = 1
or Obs[y1 , z] = 1 and Obs[y2 , z] = 0. Therefore this observer always detects the output y of the channel
from any given view z. For this reason we call a deterministic ∼s -observer a perfect observer.
Various kinds of bisimulations, or relations on observables, have been proposed and can be represented by various deterministic observers. Indeed, other kinds of relations can also be represented; consider an observer that cannot distinguish which source mi a value is output upon. This can be formalised
by using the equivalence relation ∼ch on traces that cannot distinguishes m1 from m2 .
The last example observer here effectively ensures no leakage by seeing all outputs as the same:
Example 6 (Unit observer) An observer O = (Y , Z , Obs) is called a unit observer if Z is a singleton.
It has the same view regardless of the outputs of the channel, thus can detect no leakage of the channel.

4.2 Observed Information Leakage
The amount of observed information leakage depends on the capability of the observer. To quantify this
we introduce the notion of observed information leakage.
Definition 14 (Observed information leakage) Let K = (X , Y ,C) be a channel and O = (Y , Z , Obs)
be an observer. For each leakage measure L ∈ {I , L } and any prior π on X , we define observed
information leakage by LO (π , K ) = L(π , K · O) where K · O = (X , Z ,C · Obs) is the cascade composition [18] of K and O. Similarly, for each L ∈ {S C , M C }, we define LO (K ) = L(K · O).

Y. Kawamoto & T. Given-Wilson

55

We present properties of observed information leakage as follows. The first remark is that, for each
equivalence relation ∼ on traces, all deterministic ∼-observers give the same observed leakage values.
Proposition 1 Let π be any prior on X and K = (X , Y ,C) be any channel. For any equivalence
relation ∼ on Y and any two deterministic ∼-observers O1 , O2 , we have LO1 (π , K ) = LO2 (π , K ) for
L ∈ {I , L } and LO1 (K ) = LO2 (K ) for L ∈ {S C , M C }.
The following states that the deterministic ∼s -observers and unit observers respectively have the
maximum and minimum capabilities of distinguishing traces. That is, the deterministic ∼s -observer can
detect every behaviour of the channel accurately and does not alter the leakage of the channel in any
manner, while the unit observers cannot detect any leakage of the channel.
Proposition 2 For each L ∈ {I , L }, 0 ≤ LO (π , K ) ≤ L(π , K ). For each L ∈ {S C , M C }, 0 ≤
LO (K ) ≤ L(K ). In these inequations, the left equalities hold when O is a unit observer, and the right
ones hold when O is a deterministic ∼s -observer.
Next we compare the capabilities of generalised observers. Recall the composition-refinement relation ⊑◦ on channels [3, 24]: A channel K1 is composition-refined by another K2 , written as K1 ⊑◦ K2 ,
iff there exists a channel K ′ such that K1 = K2 · K ′ . Since the generalised observers are also channels,
we can consider this ordering ⊑◦ on observers. For example, the unit observer is composition-refined
by ∼w -observers, and the deterministic ∼w -observer is by the deterministic ∼s -observer. For another
example, any probabilistic ∼a -observer is composition-refined by the deterministic ∼a -observer:
Proposition 3 Given any equivalence relation ∼a on Y let O1 = (Y , Z , Obs1 ) and O2 = (Y , Z , Obs2 )
be two ∼a -observers. If O2 is deterministic then O1 ⊑◦ O2 .
The composition-refined observer will observe less information leakage.
Theorem 4 Let O1 and O2 be two observers such that O1 ⊑◦ O2 . Then, for any prior π and any channel
K , we have LO1 (π , K ) ≤ LO2 (π , K ) for L ∈ {I , L } and LO1 (K ) ≤ LO2 (K ) for L ∈ {S C , M C }.
These results imply that no probabilistic ∼-observer detect more leakage than deterministic ones.

4.3 Examples of Deterministic Observers
Theorem 4 implies that the deterministic ∼s -observer does not observe less information leakage than the
deterministic ∼w -observer.
Example 7 Let us consider the scheduled compositions in Examples 1 and 2 in Section 3.3. Both the
composed channels leak all secrets without considering observers; i.e., they do so in the presence of
∼s -observer. On the other hand, they leak no secrets to a weakly-bisimilar observer. For example,
for each i ∈ {1, 2}, we define the deterministic ∼w -observer Oi as ({mi h0i, τ .mi h0i, mi h1i, τ .mi h1i},
{[mi h0i]∼w , [mi h1i]∼w }, Obs) where Obs is the matrix given in Table 3. Applying the ∼w -observer Oi to
both K1 and K2 yields the same matrix presented in Table 4. Then both channels leak no information to
the ∼w -observer. Therefore, the deterministic ∼s -observer observes more information leakage than the
deterministic ∼w -observer also in this example.
The scheduled composition can also leak more information than the parallel composition (and even
than each component channel) in the presence of imperfect observers.
Example 8 (Observer dependent) Consider the scheduled composition of the channels K1 and K2
w.r.t. the fair interleaving scheduler SFI . By Example 4, the leakage of the scheduled composition w.r.t.
SFI is less than that of the parallel composition in the presence of the deterministic ∼s -observer.
However, the leakage of the scheduled composition is more than that of the parallel composition
(and even than that of each component channel) when the ∼w -observer O is being considered; e.g.,
LO (π , CompSFI (K1 , K2 )) = 0.215 > 0 = LO (π , K1 ×K2 ) = LO (π , K1 ) for π = (0.15, 0.20, 0.30, 0.35).

Quantitative Information Flow for Scheduler-Dependent Systems

56

view

view
[mi h0i]∼w [mi h1i]∼w
output

mi h0i or τ .mi h0i
mi h1i or τ .mi h1i

1
0

0
1

Table 3: Observer matrix Obs

secret

0
1

[mi h0i]∼w

[mi h1i]∼w

0.5
0.5

0.5
0.5

Table 4: Composed matrix Ci · Obs

4.4 Example of Probabilistic Observers
The notion of deterministic ∼-observers is useful to model various observers, but they may not cover
all realistic settings. For example, when the internal action τ represents time to perform internal computation, observers may recognise it only probabilistically, for instance with probability 0.7. Then such
probabilistic observers cannot be modeled as deterministic observers but as generalised observers, which
quantify the capabilities of probabilistic observation. As far as we know, no previous work on quantitative information flow analyses have considered probabilistic observers.
Example 9 Consider a probabilistic observer O that can recognise a single internal action τ only probabilistically but two or more consecutive τ ’s with probability 1. For instance, O recognises the trace
(τ .mi h0i.mi h1i) correctly with probability 0.7 and confuses it with either (mi h0i.mi h1i), (mi h0i.τ .mi h1i)
or (mi h0i.mi h1i.τ ) each with probability 0.1. Consider the schedule-composed channel CompSFI (K1 , K2 )
from Example 4. The observed mutual information is 0.783 under the probabilistic observer O, which is
between 0.090 and 1.695 as observed under the deterministic ∼w -observer and ∼s -observer.

5

Relationships between Scheduling and Observation

This section generalises the previous examples to show three kinds of results. First, we identify conditions on component channels under which leakage cannot be effected by the scheduled composition.
Second, we show that scheduled composition can leak more or less information than the parallel composition, including results on the bounds of the information leaked. Third, we present an algorithm for
finding a scheduler that minimises the min-entropy leakage/min-capacity under any observer

5.1 Information Leakage Independent of Scheduling
This section presents results for determining when the leakage is independent of the scheduler. Regardless of the scheduler and observer, the leakage of the scheduled composition is equivalent to that of the
parallel composition under certain conditions on component channels that are detailed below.
Theorem 5 Let K1 = (X1 , Y1 ,C1 ) and K2 = (X2 , Y2 ,C2 ) be channels. Assume that, for any y1 , y′1 ∈ Y1
and y2 , y′2 ∈ Y2 , if Int(y1 , y2 ) ∩ Int(y′1 , y′2 ) 6= 0/ then y1 = y′1 and y2 = y′2 . Then, for every scheduler S and
observer O, the leakage of the scheduled composition is the same as that of the parallel composition.
By adding a stronger requirement to Theorem 5, we obtain the following corollary.
Corollary 6 Let K1 = (X1 , Y1 ,C1 ) and K2 = (X2 , Y2 ,C2 ) be channels. Assume that, for all (y1 , y2 ) ∈
Y1 × Y2 , α ∈ y1 and β ∈ y2 , we have α 6= β . Then, for every scheduler S and observer O, the leakage
of the scheduled composition is the same as that of the parallel composition.

Y. Kawamoto & T. Given-Wilson

57

5.2 Schedulers for Altering Information Leakage
This section considers when schedulers can alter the leakage of a scheduled composition. This is distinct
from prior results where it has been shown that the composition cannot leak more information than the
component channels [5, 19, 20], since here more information can be leaked to imperfect observers.
In general scheduled composition can yield more or less leakage than the individual component
channels or their parallel composition. This is illustrated by Example 8. Unfortunately heuristics for
determining when more information is leaked end up being rather complicated and dependent on many
relations between traces, interleavings, equivalences, and then subject to generalities about both schedulers and observers. Ultimately it is easier to show by examples that, for some channels, prior, and
∼-observer, there is a scheduler by which the scheduled composition leaks strictly more information
than the parallel composition. Since this clearly holds by example, we consider a class of schedulers
under which the scheduled composition does not leak more information than the parallel composition.
To define this we extend an equivalence relation ∼ on traces to probability distributions of traces:
We say that two distributions D and D′ on a set Y are ∼-indistinguishable (written as D ∼ D′ ) if the
deterministic ∼-observer cannot distinguish D from D′ at all, i.e., for all equivalence class t ∈ Y /∼, we
have ∑y∈t D[y] = ∑y∈t D′ [y]. Using ∼-indistinguishability we define a scheduler that does not leak any
behaviour of the system that the ∼-observer cannot detect.
Definition 15 Let ∼ be an equivalence relation on Y1 ∪ Y2 ∪ Int(Y1 , Y2 ). A scheduler S on Y1 and Y2
is a ∼-blind scheduler when, for any two pairs (y1 , y2 ), (y′1 , y′2 ) ∈ Y1 × Y2 , we have y1 ∼ y′1 and y2 ∼ y′2
iff we have S (y1 , y2 ) ∼ S (y′1 , y′2 ).
For instance, the deterministic sequential scheduler SDS and the fair sequential scheduler SFS are ∼w blind while the fair interleaving scheduler SFI is not. Note that ∼-blind schedulers do not leak any
behaviour that would not be visible to the deterministic ∼-observers. Thus they do not gain more information from the scheduled composition w.r.t. ∼ than the parallel composition.
Theorem 7 Let π be a prior, K1 and K2 be two channels, O be a deterministic ∼-observer, and S be
a ∼-blind scheduler. For each L ∈ {I , L } we have LO (π , CompS (K1 , K2 )) ≤ LO (π , K1 × K2 ). For
each L ∈ {S C , M C } we have LO (CompS (K1 , K2 )) ≤ LO (K1 × K2 ). When S is also deterministic,
the leakage relations become equalities.
For instance, since SDS and SFS are ∼w -blind schedulers, the deterministic ∼w -observers do not
gain more information from the scheduled composition w.r.t. ∼w than the parallel composition. In fact,
they have the same leakage in Example 7.
The following result is about a heuristic for when leakage can be changed by the properties of the
scheduler. This is presented here to clarify the properties.
Theorem 8 Let K1 = (X1 , Y1 ,C1 ) and K2 = (X2 , Y2 ,C2 ) be two channels. Assume that there exist
y1 , y′1 ∈ Y1 and y2 , y′2 ∈ Y2 such that Int(y1 , y2 ) ∩ Int(y′1 , y′2 ) 6= 0.
/ Then it is possible for the scheduledcomposition of K1 and K2 to alter the mutual information and min-entropy leakage for some prior.

5.3 Schedulers for Minimising Information Leakage
This section presents results for finding a scheduler that minimises the min-entropy leakage and mincapacity in the presence of any observer.
Theorem 9 Given any prior π , two channels K1 , K2 and any observer O, there is an algorithm that
computes a scheduler S that minimises the observed min-entropy leakage LO (π , CompS (K1 , K2 )) of
the scheduled composition.

Quantitative Information Flow for Scheduler-Dependent Systems

58

Proof: To find a scheduler S that minimises the observed min-entropy leakage LO (π , CompS (K1 , K2 )),
it is sufficient to find S that minimises the observed posterior vulnerability V (π , CompS (K1 , K2 ) · O).
For (x1 , x2 ) ∈ X1 ×X2 and (y1 , y2 ) ∈ Y1 ×Y2 , let p(x1 , x2 , y1 , y2 ) = π [x1 , x2 ](C1 ×C2 )[(x1 .x2 ), (y1 , y2 )].
For each z ∈ Z let vz =max(x1 ,x2 )∈X1 ×X2 ∑y1 ,y2 ,y p(x1 , x2 , y1 , y2 )S (y1 , y2 )[y]Obs[y, z] where (y1 , y2 ) and
y range over Y1 × Y2 and Int(Y1 , Y2 ) respectively. Let Pos(y1 , y2 )[y] be the (|Y1 | × |Y2 |, |Int(Y1 , Y2 )|)matrix defined by the following: Pos(y1 , y2 )[y] = 1 if y can be obtained by interleaving y1 and y2 , and
Pos(y1 , y2 )[y] = 0 otherwise.
To find a scheduler matrix S that minimises the observed posterior vulnerability, it suffices to solve
the linear program that minimises ∑z∈Z vz , subject to
• for each (x1 , x2 , z) ∈ X1 ×X2 ×Z , ∑y1 ,y2 ,y p(x1 , x2 , y1 , y2 )S(y1 , y2 )[y]Obs[y, z] ≤ vz
• for each (y1 , y2 ) ∈ Y1 × Y2 , ∑y Pos(y1 , y2 )[y]S (y1 , y2 )[y] = 1.
Note that the second constraint means that each row of the scheduler matrix S must sum to 1. In this
linear program, the scheduler matrix element S (y1 , y2 )[y] for each (y1 , y2 ) ∈ Y1 × Y2 and y ∈ Int(Y1 , Y2 )
and vz for each z ∈ Z are variables. We can solve this problem using the simplex method or interior point
method. (In practice, we can efficiently solve it using a linear programming solver such as lp solve [2].)
Hence we obtain a scheduler matrix S that minimises ∑z∈Z vz .
✷
In the above linear program the number of variables is |Y1 | × |Y2 | × |Int(Y1 , Y2 )| + |Z |, and the
number of constraints is |X1 | × |X2 | × |Z | + |Y1 | × |Y2 |. Since the number of interleaved traces grows
exponentially in the number of traces, the time to compute a minimising scheduler is exponential in the
number of component traces. When the observer O is imperfect enough for |Z | to be very small, then
the computation time improves significantly in practice. On the other hand, when the number of traces is
very large, we may heuristically obtain a scheduler with less leakage by results in the previous section.
To obtain a scheduler that minimises the worst-case leakage value, it suffices to consider a scheduler
that minimises the min-capacity.
Corollary 10 Given two channels K1 , K2 and any observer O, there is an algorithm that computes a
scheduler S that minimises the observed min-capacity of the scheduled composition.
These two results give the minimum amount of leakage that is possible for any scheduling.
Example 10 Consider the channels K1 , K2 defined in Section 3.3. By Theorem 9, the minimum observed
min-entropy leakage w.r.t. the prior (0.15, 0.20, 0.30, 0.35) is 1.237 under the deterministic ∼s -observer,
and 0.801 under the probabilistic observer defined in Example 9. By Corollary 10, the minimum observed
min-capacity is 1.585 under the deterministic ∼s -observer, and 1.138 under the probabilistic observer.
Since the channel capacity will not exceed the min-capacity [26], the minimum observed mincapacity obtained by the above algorithm gives an upper bound on the minimum channel capacity.

6

Case Studies

6.1 Sender Anonymity
In e-voting sender anonymity can be summarised as the issue of collecting votes from a number of voters
and being able to expose the aggregate vote information while revealing as little as possible about how
each voter voted. This can be solved by a general application of a mix network [13] where all the votes
are sent via mixing systems that output the votes in a manner that should not reveal how each voter voted.

Y. Kawamoto & T. Given-Wilson
π1 ✲
π2 ✲
π3 ✲

K1
K2
K2

59
Composed votes

Y1✲
Y2✲
Y3

KA

✻
YS2
✛ Y4 K4 ✛ π4

YA✲
✲

KS1

YS1✲

KS2

✛YB

KB

✛ Y5 K5 ✛ π5

Figure 2: Structure of composed channels for voters

This can be represented here by each voter being an information-theoretic channel that outputs their
vote. For example, consider a simple voting in which possible votes are 0 and 1 and each voter outputs
the chosen vote via mh0i or mh1i, respectively. Then each voter (indexed by i) can be represented by the
channel Ki = ({0, 1}, {mh0i, mh1i},Ci ) where Ci [k, mhki] = 1 for k ∈ {0, 1} and each voter has a prior
πi on {0, 1}. Observe that each such voter channel alone fully reveals the prior for the channel.
The scheduled composition of the voters represents the mix network with the schedulers representing
the mixing algorithm and thus providing the ability to reason over their effect on information leakage.
Consider the following problem with five voters K1 to K5 . As illustrated in Figure 2, the ballot of each
voter is sent via intermediate severs (schedulers) KA , KB , KS1 that mix the order of ballots. The final
system KS2 combines KS1 and KB to output all the votes according to some mixing.
Using the deterministic sequential scheduler SDS for all compositions reveals all information on how
each voter voted. That is, the leakage is considered to be 5-bits (as each vote is 0 or 1). On the other hand,
using the fair sequential scheduler SFS for all compositions leaks less information than SDS . When π
is uniform and K is the composed channel in Figure 2 with the appropriate scheduling, we obtain
L (π , K ) = 3.426 and I (π , K ) = 2.836. Observe that here the third voter’s output can only appear
in the 1st, 3rd, or 5th position in the final trace. This is repaired by using the fair interleaving scheduler
SFI for all compositions that leaks even less information: L (π , K ) = 2.901 and I (π , K ) = 2.251.
A more interesting case is when different compositions use different schedulers. Since the votes do
not contain any information about the system they came from, let alone voter. Using the fair sequential
scheduler for KA and KB , and the fair interleaving scheduler for KS2 , along with a specially constructed
scheduler for KS1 can reduce the information leakage to a minimum. Then the min-entropy leakage is
2.824 and the mutual information is 2.234. Note that when there is only one scheduler that receives all 5
ballots, the minimum min-capacity of the composed system (over all possible schedulers) is 2.585.
The example can be extended further by adding τ steps before votes to indicate time taken for some
parts of the process. For a simple example, consider when voters 1 and 2 have a τ step before their
vote to represent the time taken, e.g. as indicative of voting order, or the time taken for the extra mixing
step. In the presence of all fair interleaving schedulers, the observed min-entropy leakage and the mutual
information are respectively 3.441 and 2.785 under the perfect observer. However, these shift to 3.381
and 2.597, respectively, under the deterministic ∼w -observer.

6.2 Side-Channel Attacks
Consider the small program shown in Figure 3, where an observable action is repeated in a loop. This
program captures, for instance, some aspects of decryption algorithms of certain cryptographic schemes,
such as RSA. Intuitively, X[ ] is the binary array representing a 3-bit secret (e.g. 011), which corresponds
to secret decryption keys. The timing of the algorithm’s operation reveals which bit of the secret key is
1, since the observable-operation mh1i can be detected, perhaps as power consumption, response time,
or some other side-effect of the algorithm [22]. We denote by K the channel defined by this program.

Quantitative Information Flow for Scheduler-Dependent Systems

60

for(i = 0; i < 3; i++) {
tau;
if(X[i] = 1) {
m<1>; //observable-operation
}
}

Figure 3: Decryption algorithm

τ
output

τ 0.8
mh1i 0.05

view
mh1i

0/

0.1
0.9

0.1
0.05

Figure 4: Probabilistic observer matrix

Consider composition of K with itself, e.g., when applying the algorithm to different parts of the
message in parallel. Clearly if the parallel composition is taken then both instances of K will leak all
their information about the key. On the other hand, the scheduled composition may have less leakage.
We first consider the case each instance of the component channel K receives a different secret bit
string independently drawn from the uniform prior. This captures the situation in which each decryption
operation uses different secret keys. When the fair interleaving scheduler mixes the two traces, the
min-entropy leakage and the mutual information are respectively 4.257 and 3.547 in the presence of the
perfect observer, and 2.807 and 2.333 in the presence of the deterministic ∼w -observer.
Next we consider the case where both instances of K share the same secret key which has been
drawn from the uniform prior. When the fair interleaving scheduler mixes the two traces, the minentropy leakage and the mutual information are respectively 3.000 and 3.000 (all 3 bits of the secret key
are leaked) under the perfect observer, and 2.000 and 1.811 under the deterministic ∼w -observer.
More interesting is to consider the case where the observer is only able to detect approximate information through the side-channel. Consider the observer O that only probabilistically observes actions
according to the matrix in Figure 4. Here 0/ indicates that nothing is detected by the attacker not even a τ .
For example, applying this observer to the trace τ .τ .τ may yield τ .τ when one τ is not observed (represented 0/ in the matrix). Such an observer is less effective even when applied to the parallel composition
of channels. However, this applies even further when applied to any scheduled composition since the loss
of information through poor detection cannot even be limited to one channel or the other. Thus, a trace
of length 5, even from a leaky scheduler such as the (left-first) sequential scheduler, would leak less than
the parallel composition (since it would be clear which composite channel had been poorly observed).
For instance, let us consider the case each instance of K independently receives a secret from the
uniform prior and the fair interleaving scheduler is used. Then the min-entropy leakage and the mutual
information are respectively 3.306 and 1.454 under this probabilistic observer. If we consider the case
both instances of K shares the same secret, then the leakage values are respectively 2.556 and 1.924.

7

Related Work

Regarding schedulers there are a variety of studies on relationships between schedulers and information
leakage [11, 4]. In [10] the authors consider a task-scheduler that is similar to our schedulers, albeit
restricted to the form of our deterministic scheduler. The schedulers in this paper are also similar to the
admissible schedulers of [4]. Both are defined to depend only upon the observable outputs, that is the
traces they schedule. This avoids the possibility of leakage via the scheduler being aware of the intended
secret directly and so leaking information. Differently to admissible schedulers, here the scheduler can
be probabilistic, which is similar in concept to the probabilistically defined (deterministic) schedulers of
[27], although they explore scheduling and determinism of Markov Chains and not information leakage.
Most work on schedulers has focused on preventing any leakage at all, indeed the problem is typically
defined to prevent any high/secret information leaking. This in turn sets extremely high requirements
upon the scheduler, and so proves to be difficult to achieve, or even impossible. Here we take an approach
to scheduling that allows for probabilistic schedulers and so reasoning about the quantitative information

Y. Kawamoto & T. Given-Wilson

61

leakage, rather than total leakage. Thus we permit schedulers that can be daemonic or angelic, as well as
many in between that may closer resemble the behaviour of real world systems.
Regarding observers there is little prior work in quantitative information flow and quantifying the
capability of the observer. [6] has some similarity where they formalise an equivalence of system states
similar in style to the deterministic ∼-observers here. However, this does not model observers as part of
information-theoretic channels, hence does not allow the probabilistic behaviour of observers.

8

Conclusions and Future Work

We have introduced the notion of the scheduled composition of channels and generalised the capabilities of the observers to reason about more systems. Then we have presented theories that can be used
as heuristics to detect when scheduled composition may have an effect on the information leakage.
This determines when scheduled composition is a potential risk/benefit to a scheduler-dependent system. Scheduling can both leak more information, or less information to an observer depending on many
factors, while some leakage bounds can be obtained for schedule-composed channels. Further, we have
shown an algorithm for finding a scheduler that minimises the leakage of the scheduled composition.
The work here provides a foundation for continuing research into concurrent behavior, including
interactive systems. Here we have limited the systems to finite sets of secrets and observables since
this aligns with the discrete version of leakage calculations. By shifting to continuous domains we can
investigate some systems with infinite secrets or observables. Similarly the schedulers here assume finite
traces and are typically defined over the entire possible traces. However, many do not require this,
and can be defined only upon the next action in the trace. This allows for alternate definitions without
changing the results, and easier applicability to infinite settings.

References
[1] http://www.cs.bham.ac.uk/research/projects/infotools/leakiest/ext/.
[2] lp solve version 5.5. http://lpsolve.sourceforge.net/.
[3] Mário S. Alvim, Konstantinos Chatzikokolakis, Catuscia Palamidessi & Geoffrey Smith (2012): Measuring
Information Leakage Using Generalized Gain Functions. In: Proc. of CSF, IEEE, pp. 265–279, doi:10.
1109/CSF.2012.26.
[4] Miguel Andres, E., Catuscia Palamidessi, Ana Sokolova & Peter Van Rossum (2011): Information Hiding
in Probabilistic Concurrent Systems. Theor. Comp. Sci. 412(28), pp. 3072–3089, doi:10.1016/j.tcs.
2011.02.045.
[5] Gilles Barthe & Boris Köpf (2011): Information-theoretic Bounds for Differentially Private Mechanisms. In:
Proc. of CSF, IEEE, pp. 191–204, doi:10.1109/CSF.2011.20.
[6] Fabrizio Biondi, Axel Legay, Pasquale Malacaria & Andrzej Wasowski (2013): Quantifying Information Leakage of Randomized Protocols.
In: Proc. of VMCAI, pp. 68–87, doi:10.1007/
978-3-642-35873-9_7.
[7] Michele Boreale (2009): Quantifying information leakage in process calculi. Inf. Comput. 207(6), pp. 699–
725, doi:10.1016/j.ic.2008.12.007.
[8] Michele Boreale, Francesca Pampaloni & Michela Paolini (2011): Asymptotic Information Leakage under
One-Try Attacks. In: Proc. of FOSSACS, pp. 396–410, doi:10.1007/978-3-642-19805-2_27.
[9] Christelle Braun, Konstantinos Chatzikokolakis & Catuscia Palamidessi (2009): Quantitative Notions of
Leakage for One-try Attacks. In: Proc. of MFPS, ENTCS 249, Elsevier, pp. 75–91, doi:10.1016/j.
entcs.2009.07.085.

62

Quantitative Information Flow for Scheduler-Dependent Systems

[10] Ran Canetti, Ling Cheung, Dilsun Kirli Kaynar, Moses Liskov, Nancy A. Lynch, Olivier Pereira & Roberto
Segala (2008): Analyzing Security Protocols Using Time-Bounded Task-PIOAs. Discrete Event Dynamic
Systems 18, pp. 111–159, doi:10.1007/s10626-007-0032-1.
[11] Konstantinos Chatzikokolakis & Catuscia Palamidessi (2007): Making random choices invisible to the scheduler. In: Proc. of CONCUR’07, Springer, pp. 42–58, doi:10.1016/j.ic.2009.06.006.
[12] Konstantinos Chatzikokolakis, Catuscia Palamidessi & Prakash Panangaden (2008): Anonymity Protocols as
Noisy Channels. Inf. Comput. 206(2–4), pp. 378–401, doi:10.1016/j.ic.2007.07.003.
[13] David Chaum (1981): Untraceable electronic mail, return addresses, and digital pseudonyms. Commun.
ACM 24(2), pp. 84–90, doi:10.1145/358549.358563.
[14] Tom Chothia, Yusuke Kawamoto & Chris Novakovic (2013): A Tool for Estimating Information Leakage.
In: Proc. of CAV’13, doi:10.1007/978-3-642-39799-8_47.
[15] Tom Chothia, Yusuke Kawamoto & Chris Novakovic (2014): LeakWatch: Estimating Information Leakage
from Java Programs. In: Proc. of ESORICS’14, pp. 219–236, doi:10.1007/978-3-319-11212-1_
13.
[16] Tom Chothia, Yusuke Kawamoto, Chris Novakovic & David Parker (2013): Probabilistic Point-to-Point
Information Leakage. In: Proc. of CSF, IEEE, pp. 193–205, doi:10.1109/CSF.2013.20.
[17] David Clark, Sebastian Hunt & Pasquale Malacaria (2001): Quantitative Analysis of the Leakage of
Confidential Data. In: Proc. of QAPL’01, ENTCS 59 (3), Elsevier, pp. 238–251, doi:10.1016/
S1571-0661(04)00290-7.
[18] Barbara Espinoza & Geoffrey Smith (2011): Min-Entropy Leakage of Channels in Cascade. In: Proc. of
FAST, LNCS 7140, Springer, pp. 70–84, doi:10.1007/978-3-642-29420-4_5.
[19] Barbara Espinoza & Geoffrey Smith (2013): Min-entropy as a resource. Inf. Comput., doi:10.1016/j.
ic.2013.03.005.
[20] Yusuke Kawamoto, Konstantinos Chatzikokolakis & Catuscia Palamidessi (2014): Compositionality
Results for Quantitative Information Flow. In: Proc. of QEST’14, pp. 368–383, doi:10.1007/
978-3-319-10696-0_28.
[21] Yusuke Kawamoto & Thomas Given-Wilson (2015): Quantitative Information Flow for SchedulerDependent Systems. Research Report, INRIA. Available at http://hal.inria.fr/hal-01114778.
[22] Paul C Kocher (1996): Timing attacks on implementations of Diffie-Hellman, RSA, DSS, and other systems.
In: Proc. of CRYPTO’96, Springer, pp. 104–113, doi:10.1007/3-540-68697-5_9.
[23] Boris Köpf & David A. Basin (2007): An information-theoretic model for adaptive side-channel attacks. In:
Proc. of CCS, ACM, pp. 286–296, doi:10.1145/1315245.1315282.
[24] Annabelle McIver, Carroll Morgan, Geoffrey Smith, Barbara Espinoza & Larissa Meinicke (2014): Abstract
Channels and Their Robust Information-Leakage Ordering. In: Proc. of POST’14, pp. 83–102, doi:10.
1007/978-3-642-54792-8_5.
[25] Geoffrey Smith (2009): On the Foundations of Quantitative Information Flow. In: Proc. of FOSSACS,
LNCS 5504, Springer, pp. 288–302, doi:10.1007/978-3-642-00596-1_21.
[26] Geoffrey Smith (2011): Quantifying Information Flow Using Min-Entropy. In: Proc. of QEST’11, pp. 159–
167, doi:10.1109/QEST.2011.31.
[27] Lijun Zhang & Martin R. Neuhäußer (2010): Model Checking Interactive Markov Chains. In: Proc. of
TACAS’10, Springer-Verlag, Berlin, Heidelberg, pp. 53–68, doi:10.1007/978-3-642-12002-2_5.

