Probabilistic Point-to-Point Information Leakage
Tom Chothia∗ , Yusuke Kawamoto∗ , Chris Novakovic∗ and David Parker∗∗ School of Computer Science
University of Birmingham, Birmingham, UK

Abstract—The outputs of a program that processes secret data
may reveal information about the values of these secrets. This
paper develops an information leakage model that can measure
the leakage between arbitrary points in a probabilistic program.
Our aim is to create a model of information leakage that makes
it convenient to measure specific leaks, and provide a tool that
may be used to investigate a program’s information security. To
make our leakage model precise, we base our work on a simple
probabilistic, imperative language in which secret values may
be specified at any point in the program; other points in the
program may then be marked as potential sites of information
leakage. We extend our leakage model to address both nonterminating programs (with potentially infinite numbers of secretand observable values) and user input. Finally, we show how
statistical approximation techniques can be used to estimate ourleakage measure in real-world Java programs.
Keywords-information leakage; probabilistic language; nontermination

I. I NTRODUCTION
This paper presents a framework that can be used to measure
information leaks between arbitrary points in a program. Our
motivation is to allow a programmer or analyst examining
source code to verify that the values stored in particularvariables at particular times cannot be deduced from the values
that will be visible to an attacker. Our framework introduces
two annotations: secret, for marking the values stored inselected variables as secret at particular points in the program,and observe, for identifying variables as potential leakage sites
due to an attacker’s ability to observe their values at thosepoints. After an analyst annotates their secret and observablevariables, our framework measures how much information canbe deduced about the secret values from the observable values.
As a motivating example, we consider the following hypothetical fragment of source code from a card game:...
Card theirCard = deck.drawCard();observe(theirCard);
socket.write(theirCard);...
Card myCard = deck.drawCard();secret(myCard);...
determineWinner();In this example, a Card object (theirCard) is drawn
from the deck and sent over an insecure socket to a remote
opposing player; since this is a site of a potential information
leak, the object is marked as observable. Later, another Card
object (myCard) is drawn from the deck, and the winner ofthe game then depends on this object in some way (e.g., on its
face value); therefore, it is marked as secret. In this example,
we wish to measure how much information an opponent learns
about myCard by observing theirCard (rather than the
randomness of myCard in isolation). The best possible implementation of this program provides the opponent observing
theirCard with only a very small amount of information
about the face value of myCard (i.e., that it is not theface value of theirCard). However, this may not be thecase in poor implementations: if the deck is shuffled with aweak pseudorandom number generator (PRNG), the face valueof myCard may be predictable from that of theirCard;in an even poorer implementation, the deck itself may be
stored inside the Card object of theirCard somehow andthe future face value of myCard is leaked entirely when
theirCard is sent over the socket. A similar example is a
program that generates a nonce that is exposed to a potential
attacker, and then uses the same PRNG to generate a session
key; the programmer would want to ensure that the session
key cannot be guessed from the value of the nonce.
In this sense, our aim is to create a model of information
leakage that makes it convenient to measure leaks between
given points in a program, rather than a system that guarantees
freedom from all types of leakage between variables at all
times. Our model may not detect information leaks that occur
between variables that have not been annotated, but we believethat in most cases the programmer understands their code best,
and therefore that the ability to detect leaks at selected points
will provide a more practical, targeted mechanism than one
that attempts to detect all possible leaks (and may also return
many false positives).
A complication of introducing these annotations is thatthey can occur anywhere (e.g., in loop bodies) and in any
order, so it is important to precisely define the leakage being
measured. To provide the theoretical base for a tool thatmeasures such leakage, we present a formal framework inwhich secret information and potential sites of leakage can be
annotated. Probability is an important aspect of many security
protocols and systems, so we base our framework on a simple
probabilistic, imperative language that we call CH-IMP. The
language includes primitives for declaring new variables ina particular scope, assigning new values to variables, andannotating the values stored in selected variables as either
secret or observable at that particular point during execution.
We note that both the secret and observe commands operateon the variable only when the command is evaluated, and do
not indicate that all values ever stored in the variable should beInitial secrets: XISecrets: X

SystemSystemObservations: Y

Observations: Y(a) Classic modelFig. 1.

Secrets: X(b) Our model

SystemObservations: Y

Secrets: XI+(c) Our model, with initial secrets

Initial secrets: XI

Input function: f

SystemObservations: Y

Secrets: XI+(d) Our model, with initial secrets anduser input

An overview of the classic information leakage model and our leakage model (including variations on our leakage model).

information leakage is what can be learnt about these values
from the observations.
In Section V, we extend the model further to include afunction that supplies inputs to a program from a finite range,
based on the previously-observed values (Fig. 1d). The initial
secret values cannot be affected by the input function, but
the secret values present upon termination of the program can(e.g., if the program uses an attacker-controlled input as asecret value at a later point, our extended model considers theattacker to have learnt the secret value). We show that, when
deciding whether there exists any input function that causes a
program to leak information, it is sufficient to test the programwith the input function that produces all possible inputs withequal probability.
Our framework also allows us to define the information
leakage of programs that do not terminate and therefore may
produce an infinite list of values as their output. We define
the leakage of non-terminating programs to be the limit of
the leakage as the number of observations tends to infinity.
We show this limit exists, and can be calculated by taking
the limit of the finite leakage measurements; we also give anexact expression of its value using Lebesgue integration [1].
Our contribution here is to provide a meaningful method ofreasoning about leakage from non-terminating programs that
may have an infinite number of secret and observable values.
We provide a prototype implementation of our semantics
in OCaml that is suitable for checking for information leaks
in programs of low to moderate complexity. We present an
example that shows how this tool can be used to calculate
meaningful measures of information leakage.
To allow our framework to scale, we apply statistical approximation techniques [2] to estimate the measure of information leakage. These techniques provide a confidence interval
for an estimation of information leakage from trial runs ofa program. We have developed a tool, LeakWatch, which
repeatedly executes Java classes annotated with “secret” and“observe” commands and estimates our framework’s leakage
measure. We show that, for small programs, the OCaml and
LeakWatch implementations of the framework produce com-treated as secret or observable for the duration of the program.
Therefore, the values we wish to keep secret may be stored invariables that are declared at the start of the program, or may
be values that result from complex computations performed
during the program’s execution.
We define the semantics for a CH-IMP program in termsof a discrete-time Markov chain (DTMC) augmented withinformation about occurrences of secret and observable values.
The DTMC can then be used to calculate the joint probability
distribution of the secret and observable values, and therefore
any of the standard measures of information leakage, suchas mutual information, min-entropy leakage, and guessing
entropy. To explain the intuition behind our model of leakage,
we define the “worst possible semantics” for a program thatallows an attacker to observe the value of every variable
annotated with the secret command, ignoring all other outputs.
Our framework reveals how much an attacker learns about
the output of a program executed with this worst possible
semantics by observing the output of the program when
executed with CH-IMP’s standard semantics.
Our framework moves away from the standard model ofmeasuring information leakage, where secret inputs are declared before a program executes and publicly observable
outputs are produced upon termination (as depicted in Fig. 1a).
Instead, the framework permits secret values and observable
outputs to occur at arbitrary points (e.g., inside loops or inblocks of code that are only reached with a small probability).
Since our model produces both secret and observable values asa side-effect of program execution (see Fig. 1b), our systems
are not formal information-theoretic channels. Although for
any terminating program there exists an equivalent programthat defines all of its secrets before execution and outputs
the observations upon termination, real-world programs are
sufficiently complex that rewriting them in this way becomesdifficult or impractical. Our model is general enough to also
allow secret values to be defined before execution (see Fig. 1c),which we will later formalise in Section III-B. In this case,the secret values present upon termination of the program arethose defined before or during execution, and our measure of2parable results and that statistical approximation can be used toestimate meaningful measures of information leakage in large
programs written in real-world programming languages.
The rest of the paper is organised as follows. In Section II,
we define the CH-IMP syntax and motivate our leakage model.
In Section III, we define the semantics of our framework using
DTMCs and formalise the corresponding notion of information
leakage using probability spaces and mutual information. We
then extend our model to address non-terminating programsin Section IV by considering programs that produce an unbounded number of both secret and observable values. In
Section V, we extend our model further to include external
inputs. We discuss implementations of our framework in
Sections VI and VII, and conclude in Section VIII.
A version of this paper with full proofs can be found at [3].

Tools that quantitatively measure information leakage insimple languages have been designed previously. QIF [19] is arelated tool capable of measuring leakage from a single highsecurity input to a single low-security output in a language
similar to CH-IMP, but a probability distribution on thevalues of the high-security input must be defined before theprogram is executed; CH-IMP can measure the leakage fromsecret values to observable values at arbitrary points duringexecution. QUAIL [20] measures information leakage from
non-terminating programs and uses a probabilistic language
syntactically similar to CH-IMP, but relies on a different
information leakage model: all variables must be declared
before the system executes.
Various practical frameworks have previously been createdfor measuring information leakage in real-world source code:like CH-IMP, Jif [21] uses source code-level annotations todetect leaks in large Java projects, although it is based on aqualitative information leakage model, and cannot calculate
the severity of leaks it detects. Flowcheck [22], a Valgrindbased information leakage tool for C, is able to operate onlarge software projects, but at the expense of the programmer
being able to annotate the source code easily, which is a
specific objective of our work.

A. Related Work
Information leakage in deterministic programs has been investigated previously (e.g., [4], [5], [6], [7], [8]). While related
to our work, much of this previous research does not directly
investigate the detection of information leaks in probabilistic
programs. A number of probabilistic languages have beenpresented previously (e.g., [9], [10]), but most were designed
for reasoning under uncertainty, which is inappropriate forour work where the entire state space must be known. A
related probabilistic language is described in [11]. This work
uses operational and denotational semantics to describe thebehaviour of the language that, while intuitive, make it moredifficult to measure the leakage of non-terminating programs;
this complexity is not present in CH-IMP’s semantics.
Using information theory to measure leakage in probabilistic systems is also common (e.g., [12], [13]), but most of thiswork is based on models that measure leakage from secrets
declared at the start of a program to outputs observed upon
termination; our model of information leakage is more complex. McIver & Morgan [14] propose a method of formalising
sequential, non-deterministic programs probabilistically; theirwork preserves the secrecy of high-security variables throughout execution of the program, rather than just protecting theirinitial values. We note that our model intentionally does notconsider the overwriting of secret variables to be the cause of
an information leak. More recent work by McIver et al. [15]develops the model further. Askarov & Sabelfield’s [16] information leakage model allows for the safe public disclosureof previously-secret values during program execution, but isqualitative rather than quantitative. Alvim et al. [17] propose
the use of channels with memory and feedback to model anattacker with the ability to influence the distribution on secretvalues in terminating interactive programs; the attacker in ourmodel does not have this ability, and studies the information
leakage from non-terminating programs. Theoretical models
of information leakage in non-terminating programs have been
proposed before: O’Neill et al. [18] propose one such model,
but it focuses on protecting the strategies of high-level usersof the system rather than the values stored in particular highsecurity variables at specific moments.

II. I NFORMATION L EAKAGE : M OTIVATION AND M ODELIn this section, we formally define the syntax of the CH-IMP
language, and motivate our leakage model with some example
programs that subtly leak information.
A. The CH-IMP Language
The goal of our work is to formally define an information
leakage model that can detect and measure information leaks
between arbitrary points in programs. Our motivation is tomake it as convenient as possible for programmers to utilise
this model in their own programs, so we allow variables in
CH-IMP to be identified as secret or observable at specificpoints in a program with minimal annotation. The syntax ofthe language is defined as follows.
Definition 1: A CH-IMP program is a command C conforming to the grammar
C

::=
|
|
|
|
|
|
|
|

new V := ρV := ρ
if (B) { C } else { C }while (B) { C }
C; C
start
end
secret V
observe V

where V ranges over variable names, B ranges over Boolean
expressions (i.e., evaluating to one of {true, false}), and ρ
ranges over probability distributions on arithmetic expressions:variables, integers, or the result of evaluating two variables
or integers with one of the standard arithmetic operations{+, -, *, /, mod, xor}.
We only consider CH-IMP programs that are well-formed;
i.e., ones where variables are declared only once and are not3accessed out of scope. We provide the formal semantics for
CH-IMP in Section III-B. The first five production rules areconventional: new declares a new variable V and assigns toit an integer value according to the probability distribution ρ(e.g., ρ = { 0 7→ 0.5, 1 7→ 0.5 } could simulate the tossingof a fair coin); assignments, conditional statements, loops andsequential composition are also standard constructs. start andend are not used directly, but are inserted by the semantic
rules to create and destroy levels of variable scope (e.g., whenevaluated, “while (B) { C }” is expanded to “while (B) { start;
C; end }”).

those that are observed before other variables are annotated as
secret.
Secondly, we consider the possible leakage from sets ofsecrets:
new sec1 := { 0 7→ 0.5, 1 7→ 0.5 };new sec2 := { 0 7→ 0.5, 1 7→ 0.5 };secret sec1;
secret sec2;
new out := sec1 xor sec2;
observe out;

While this program does not leak any information about thesecret values of sec1 or sec2 , an attacker does learn whether
the values are equal; therefore, some information is leaked.
This example shows that we must consider the leakage fromthe set of all secret values, rather than measuring the leakage
from each secret value individually.
Thirdly, we consider a secret annotation occurring inside aloop:

B. Leakage Model: Examples
The measurement of information leakage from secret values
declared at the start of a program to public values at its end
is an established and well-understood concept (e.g., [7], [12],[6]), as is detecting information leaks to public variables at any
location within a program (e.g., [21]). Allowing both secretand observable values to occur at arbitrary points in programs
causes subtleties that must be addressed before we can fully
define our model of information leakage.
We model an attacker that has access to both the sourcecode of a program and the observable values produced by
the program. The attacker cannot identify which observe
command caused a particular observation beyond what canbe deduced from the source code and the observable values.
We note that a more powerful attacker that does have thisability can be modelled by adding a unique identifier to eachobservable value.
Our model measures how much information is learnt (i.e.,
the reduction in uncertainty) about the program’s secret values
from its observable values. We do not measure the randomness
or predictability of the secrets in isolation; our goal is toanswer the question “is it safe to allow an attacker to observe
the values of variables annotated with the observe command?”.
Likewise, marking values dependent on each other as secretdoes not increase the overall uncertainty about the secretvalues, and thus does not increase the overall leakage.
Our first example demonstrates that we must measure theinformation leakage from secret values to all observablevalues, rather than each individual observable value:

new result := 0; new i := 0; new sec := 0;
while (i < 4) {observe result;sec := { 1 7→ 0.0625, . . ., 16 7→ 0.0625 };secret sec;
if (i == 2) {result := sec;}
i := i + 1;}

This program marks different variables’ values as secretand observable inside a loop, and leaks sec ’s third value
via result on the fourth iteration of the loop (thus, 4 bits of
information are leaked). Again, this example shows that the setof all observable values must be considered when calculating
the possible leakage of any secret value, and not just theobservable values that occur in a particular iteration of theloop. It also shows that, when a variable contains different
secret values at different times during execution, we mustmeasure the leakage from the set of all secret values that havebeen stored in that variable.
Our fourth example contains a situation in which no variable’s value may be marked as secret:new rand := { 0 7→ 0.5, 1 7→ 0.5 };observe rand ;new sec := { 0 7→ 0.5, 1 7→ 0.5 };secret sec;
new out := sec xor rand ;observe out;

new rand := { 0 7→ 0.5, 1 7→ 0.5 };if (rand == 1) {new sec := { 0 7→ 0.5, 1 7→ 0.5 };secret sec;
observe sec;
} else {observe rand ;}In this program, the attacker observes two values: the valueof rand on line 2, and the value of out on line 6. The secretannotation on line 4 indicates the programmer’s concern about
possible information leaks regarding the value of sec at thatpoint. In this case, the two observed values together leakthe secret value, but individually they leak no information to
the attacker. This example shows that we must measure theinformation leakage to the list of all observed values, including

If an attacker observes 1 as the output of this program, theyknow the secret value of sec is 1; however, if the attacker
observes the output 0, there is a 13 probability that sec ’s
secret value is 0 and a 23 probability that no variable’s value
was annotated as secret. If we restrict our measurement of
the leakage to only those cases in which the variable’s value
4

by G if it is the smallest σ-algebra containing G. P : B → [0, 1]
is a probability measure over (Ω, B); for each member of B it
gives the probability of an event from that set occurring. We
call (Ω, B) a measurable space and sets b ∈ B are said to bemeasurable.
Let (ΩX , BX ) be another measurable space. A randomvariable X defined on (Ω, B) and taking values in (ΩX , BX )is a function X : Ω → ΩX such that, for each bX ∈ BX ,X −1 (bX ) ∈ B where X −1 (bX ) = {ω ∈ Ω | X(ω) ∈ bX }.
This means that the random variable X has an associatedprobability distribution PX : BX → [0, 1] giving the probability of each bX ∈ BX :is marked as secret, we would conclude that this program
always leaks the value, which would be an overestimation.
Therefore, in programs where a variable’s value may or may
not be marked as secret, our model states that the program
leaks some information if an attacker can identify whether
a variable is annotated as secret, even if they do not learn
anything else about the value.
Similarly, we state that the attacker learns information if
they discover the order or number of secret declarations, even
if they learn nothing about the values themselves. For example,
we consider the following program to leak information:
new x := { 0 7→ 0.5, 1 7→ 0.5 };new y := { 0 7→ 0.5, 1 7→ 0.5 };observe y ;if (y == 1) {new z := { 0 7→ 0.5, 1 7→ 0.5 };secret x ; secret z;} else {secret x ;}PX (bX ) = P (X −1 (bX )).
Finally, for two (probability) measures P1 and P2 , we saythat P1 is absolutely continuous with respect to P2 , if P1 (b) =0 for every set b for which P2 (b) = 0.
2) Discrete-Time Markov Chains: We use a discrete-timeMarkov chain (DTMC) to represent the possible executionsof a CH-IMP program, and then to generate the probability
spaces that represent a program’s secret and observable values.
A DTMC is a tuple D = (S, s̄, P) where:

In this program, the attacker learns whether only x or bothx and z were annotated as secret, but learns nothing about thevalue of either variable. We consider this to be an information
leak, since the fact that a program is processing some confidential data, and what the program considers confidential for aparticular execution, may reasonably be sensitive information.
These definitions of what is and is not an information
leak are enforced by the semantic rules in Section III-B. We
note that it is possible to define a sound leakage model that
does not consider the order or number of secret declarations
as confidential by making minor changes to our semantics;
however, we have chosen the most conservative leakage modelon the grounds that a user may consider the order and numberof secrets a program possesses to be secret information in its
own right.

S is a (countable) set of states;s̄ ∈ S is an initial state;• P : S×S → [0, 1] is a transition probability matrix suchP
that s′ ∈S P(s, s′ ) = 1 for all s ∈ S.

••

The matrix P gives the probability P(s, s′ ) of making atransition between any pair of states s, s′ ∈ S. A path of D
is a (finite or infinite) sequence of states ω = s0 s1 s2 . . . suchthat s0 = s̄ and P(si , si+1 ) > 0 for all i ≥ 0. The set of all
infinite paths of D is denoted ΩD and we can build (following[23]) a probability space over ΩD as follows.
For a finite pathdef Qn−1π=s0 . . . sn , we assign probability P(π) = i=0 P(si , si+1 ).
The basic cylinder Cyl(π) consists of all infinite paths startingwith π. We then define a probability space (ΩD , BD , PD ) overthe infinite paths ΩD of D, where:

III. I NFORMATION L EAKAGE FOR THE CH-IMP
L ANGUAGE

BD ⊆ 2ΩD is the σ-algebra generated by the set of basic
cylinders {Cyl(π) | π is a finite path in D};• PD is the unique measure with PD (Cyl(π)) = P(π) for
all finite paths π.

We now formally define the semantics of CH-IMP and
the corresponding model of information leakage outlined in
Section II. We will define the semantics in terms of discretetime Markov chains, so we begin with some brief backgroundmaterial on this topic.

•

The probability measure PD allows us to define the probabilityof certain (measurable) events of interest in the system being
modelled by the DTMC. We will also define random variableson this probability space.

A. Probability Spaces and Discrete-Time Markov Chains
1) Probability Spaces: Non-terminating programs may produce an infinite number of observable values; therefore, wecannot represent the probability of observing values as asimple mapping from particular values to a number between 0
and 1. Instead we must represent the probability of observing
values as a probability space, which is a triple (Ω, B, P ).
Here, Ω is the set of all possible events (i.e., secret andobservable values), which is often infinite. B is a σ-algebra
over the set Ω, which is a set B ⊆ 2Ω of subsets of Ω that
contains ∅ and is closed under complement and countable
unions. For a set G ⊆ 2Ω , we say that σ-algebra B is generated

B. CH-IMP Semantics
We define the semantics of a CH-IMP program P as adiscrete-time Markov chain D. The states of D describe
the current status of the program, annotated with additional
information needed to compute information leakage; they areof the form (C, σ, S, O), where:•5

C is the list of commands to be executed (i.e., an
expression derived from the CH-IMP grammar);(Declaration)
ρ(n)(new V := ρ; C, o :: σ, S, O) −−−→ (C, ({V 7→ n} ∪ o) :: σ, S, O)(Secrecy)1(secret V ; C, σ, S, O) −→ (C, σ, S :: (V 7→ [[V ]]σ), O)(Observation)1(observe V ; C, σ, S, O) −→ (C, σ, S, O :: [[V ]]σ)(Assignment)ρ(n)(V := ρ; C, σ, S, O) −−−→ (C, σ ⊕ {V 7→ n}, S, O)
σ(B) → true

(If true)1(if (B) { CT } else { CF }; C, σ, S, O) −→ (start; CT ; end; C, σ, S, O)
σ(B) → false(If false)1(if (B) { CT } else { CF }; C, σ, S, O) −→ (start; CF ; end; C, σ, S, O)
σ(B) → true

(While true)1(while (B) { CW }; C, σ, S, O) −→ (start; CW ; end; while (B) { CW }; C, σ, S, O)
σ(B) → false(While false)1(while (B) { CW }; C, σ, S, O) −→ (C, σ, S, O)(Scope creation)

1(start; C, σ, S, O) −→ (C, {} :: σ, S, O)(Scope destruction)1(end; C, o :: σ, S, O) −→ (C, σ, S, O)
Fig. 2. The information leakage semantics of CH-IMP. These rules define the transition probability matrix for the discrete-time Markov chain described in
Section III-B.

σ is a list of variable scopes (consisting of mappings fromvariable names to values), with the narrowest scope at thestart of the list;• S is a list of mappings from variable names to secretvalues at particular points during execution (as declaredwith the secret command);• O is a list of values that have been marked as observable (with observe commands) up to this point in the
program’s execution.

The key new rules of our semantics are those for secretand observe. The “observe V ” command signifies that thevalue of the variable V is observable by the attacker, so thesemantic rule adds the value of V to the end of the list ofobservable values O. We note that only the value is added to
the list: nothing is added that indicates the variable name or the
position in the program of this particular command; therefore,
the attacker cannot learn this information (per Section II-B).
A stronger attacker model, in which the attacker could learn
the variable name or location of the command in the program,
could be encoded in our framework by inserting an additional
observation that revealed this information.

•

The transition probability matrix of the DTMC (P) ispdefined according to the semantic rules in Fig. 2. s −→ s′denotes the existence of a transition from state s to state s′with probability p, and σ ⊕ {V 7→ n} denotes the replacementof the mapping for V with V 7→ n in the narrowest scope in
σ already containing a mapping for V .
The declaration rule adds a new variable mapping to thecurrent scope according to the probability distribution ρ. The
assignment rule uses the ⊕ operator to overwrite the mapping
for the variable in the narrowest possible scope. The rules
for if and while are standard, with the addition of start andend to signify the creation and destruction of a level of scope
respectively: start adds an empty mapping to the start of thelist of mappings that will contain all new declarations in thecurrent scope, and end removes the leftmost mapping fromthe list, unbinding its variables and potentially reducing thenumber of states (since two states may only differ by thevariables bound in their narrowest scopes).

The “secret V” command signifies that the value of V
is to be treated as secret at this point during execution.
Its semantic rule therefore records both the name of thevariable and its value at this point. As these are stored in anordered list, our model also considers the order in which secretannotations occur to be confidential. If this were instead a setof mappings from variables to ordered lists, our model would
not consider the ordering of secret commands operating on
different variables to be confidential, and if it were simply a setof mappings, the ordering of secret commands would not be
confidential at all. We have constructed the most conservativemodel, since it provides the strongest security guarantees.
By inspecting the semantic rules in Fig. 2, we see that at
most one rule can be applied to any state s and that the sum of
the outgoing transitions for any such rule is always 1. Since6

our definition of a DTMC insists on transition probabilities
summing to 1 for all states, we add a self-loop (i.e., setP(s, s) = 1) for any (terminating) state s that matches nosemantic rules. Alternatively, we could adapt our definition of
the probability space over DTMC paths to range over bothinfinite paths and finite paths ending such a terminating state.
The initial state of D is (P, h{}i, hi, hi) and we will assume
that the state space, denoted S, is the set of all possible statesthat can be reached from this state by applying the rules inFig. 2; this gives a set of (infinite) paths ΩD ⊆ S ω and aprobability space (ΩD , BD , PD ) over ΩD .
We can also adapt our semantics to allow for the possibilityof defining initial secret values (i.e., before P is executed)
according to some probability distribution PXI . We do soby, for each valuation of variables xi in the support of PXI ,adding a new state s̄i = (P, h{xi }i, hxi i, hi) to S and adding atransition from the original initial state s̄ to s̄i with probabilityP(s̄, s̄i ) = PXI (xi ).

As mentioned in Section III-A, these random variables
induce the probability distributions PX and PY over DX and
DY , respectively. We can also define the joint probability
distribution PXY over DX ×DY . The mutual information
between secret values and observable values is given by theequation:X
PXY (x, y).
PXY (x, y) log2
I(X; Y ) =PX (x)PY (y)x∈DX ,y∈DY

Note that PX (x)=Σy PXY (x, y) and PY (y)=Σx PXY (x, y),so the mutual information can be calculated from the joint
probability distribution PXY alone. Under the finiteness assumptions that we impose in this section, the joint probability
distribution PXY can be determined from an analysis of thetransient probabilities of D, which give the probability of
being in each possible state at a particular time step n. In
this section, we require that all secret and observe commands
always occur within some finite number of steps of execution,
say nf . We can therefore compute PXY (x, y) for each x, yby summing the transient probabilities at step nf for all states(C, σ, S, O) of the DTMC in which x matches S and ymatches O.
A related measure is the conditional entropy of X given
Y , which describes the attacker’s uncertainty about the secretvalues when the observable values are known. It is given by
the equation:X
PY (y)PXY (x, y) log2
H(X|Y ) =.
PXY (x, y)

C. Leakage Measurement
To quantify the information leakage from the program’s
secret values to its observable values, we use the informationtheoretic measure of mutual information [24]. This is a common measure of information leakage: the mutual informationof the probability distributions on the secret values and on theobservable values tells us how much information an attacker
learns about the secret values by inspecting the observablevalues. (For a discussion of the precise security guarantees
provided by mutual information and other leakage measures,
we refer the reader to the literature; e.g., [25], [26].)
We use X and Y to refer to secret and observable values,
respectively. We denote by DX the set of all possible secretvalues (including a unique value to indicate that no secretvalues have been seen) and by DY the set of all possible
observable values. In accordance with the presentation of
the semantics in Section III-B, DX comprises all possible
sequences of mappings from a variable name to an (integer)
value and DY comprises sequences of (integer) values. In
this section, we consider finite scenarios: we assume that any
execution of the program results in a finite number of secretand observable values, and that these always occur within afinite number of steps of execution. In later sections, we will
relax this requirement.
The probability of a program’s list of secret value mappings
being x ∈ DX will be denoted PX (x) and the probability of
it producing the observable values y ∈ DY will be PY (y).
More precisely (and to aid the more general definitions laterin the paper), mutual information is defined in terms of a pairof random variables: one for the secret values and one for theobservable values. Thus, we define random variables X and Y
on the probability space over paths in the DTMC D. For secretvalues, the function X : ΩD → DX projects any path ω ∈ ΩD
onto a list of secret value mappings (S in the state tuple). For
observable values, the function Y : ΩD → DY projects any
path ω ∈ ΩD onto the finite sequence of observable (integer)
values (O in the state tuple).

x∈DX ,y∈DY

Another popular measure of information leakage is the
min-entropy leakage of the secret values after inspecting theobservable values [25]; this gives a measure of how difficult
it is for the attacker to guess the secret values in one attempt.
It is defined as:
X
X
PXY (x, y).
max PXY (x, y) − log2 max
log2
y∈DY

x∈DX

x∈DX

y∈DY

Like mutual information, conditional entropy and minentropy leakage can both be calculated from the joint probability distribution, so we can also compute these measures forfinite, terminating programs.
D. Intuition: The Worst Possible Program Semantics
The measure of leakage given above defines what an attacker learns about the stream of secret values by observing the stream of observable values. To give some intuition
about what this actually means, we introduce the idea of
the “worst possible” semantics for a program that simply
leaks all information marked as secret to the attacker: states
are of the form (C, σ, S), the observe command is replacedwith a skip (no-op) command, and the secret command is
replaced with one that exposes the variable name and its secretvalue to the attacker (thus the attacker can observe S). A
program evaluated with this “worst possible” semantics leaks
all information about every occurrence of the secret command.
Let W be the random variable representing the secret values
7generated by these semantics. Our measure of leakage can beunderstood as the amount of information an attacker learns
about the output a program when it is executed with this“worst possible” semantics by observing the output of the
program when it is executed with the semantics of Fig. 2;
i.e., I(X; Y ) = I(W ; Y ). This trivially holds because X and
W are defined in the same way.

number of observable values is:lim I(X (n) ; Y (n) )
X
(n)
= lim
PXY (x, y) log2
n→∞

n→∞
(n)
(n)
x∈DX , y∈DY

A. Leakage over Infinitely Many Observable Values
Since programs do not necessarily terminate, we now extend
our leakage model to programs that may produce an infinitelylong list of observable values. In what follows, we use “nonterminating” specifically to refer to such programs (rather
than those that may continue indefinitely, but only generate
a finite number of observable values). Our contribution in thissection is to formalise a way in which we can reason about
information leakage for such non-terminating programs. For
now, we continue to assume that the number of secret values
is finite; in Section IV-C, we also relax this requirement.
We approximate mutual information for an infinite numberof observable values by considering bounded versions of it.
We do so by restricting our attention to the first n observablevalues and the corresponding secret values.
(n)
We define ΩD to be the set of paths in the DTMC fora program that have been pruned after the first n observable(n)values, i.e., every path in ΩD either has exactly n observablevalues or has fewer than n observable values and terminates,(n)or diverges silently. We note that ΩD may include an arbitrary
number of paths that may be arbitrarily long. We denote the(n)sets of secret values and observable values in the paths of ΩD(n)(n)
as DX and DY respectively.
(n)(n)
Let PX (x) and PY (y) denote the probabilities of secret(n)values being equal to x ∈ DX and observable values being(n)(n)
equal to y ∈ DY respectively. As before, we write PXY
for the joint probability distribution. We can now define theleakage that occurs after n observations as:
I(X

;Y

(n)

)=

X

(n)

(n)
PXY (x, y) log2(n)x∈DX , y∈DY(n)

PXY (x, y)
(n)

(n)

PX (x)PY (y)

(n)

(n)

PX (x)PY (y)!

.

The intuition here is that the leakage from a non-terminating
program is defined as the amount of information an attacker
learns about the secret values by inspecting the observablevalues forever. While it may not be practical for a real attacker
to learn this exact amount of information, our definitionindicates that a patient attacker will be able to learn anarbitrary approximation of it. We note that this does not allow
the attacker to observe the time at which the observations takeplace; we discuss an extension that permits timed observationsin Section IV-D.
Due to our assumption of a finite number of secret values,
the limit in Definition 2 always exists, and the leakage iswell-defined. Formally, we state this as follows:

IV. C ALCULATING THE L EAKAGE OF N ON -T ERMINATINGP ROGRAMS

(n)

(n)

PXY (x, y)

Theorem 1: The leakage from a non-terminating programwith a finite number of secret values and a possibly infinite
number of observable values (as defined in Definition 2)
exists; i.e., I(X (n) ; Y (n) ) converges.
Note that I( lim X (n) ; lim Y (n) ) is not defined, so thisn→∞n→∞proof is not trivial. To prove Theorem 1, we use the following
lemma:
Lemma 1: For all n, I(X (n+1) ; Y (n+1) ) ≥ I(X (n) ; Y (n) ).
Proof of Theorem 1: We note that I(X (n) ; Y (n) ) ≤I(X (n+1) ; Y (n+1) ) for any n and that I(X (n) ; Y (n) ) ≤log2 |DX |, where |DX | is the (finite) number of secret values.
Therefore I(X (n) ; Y (n) ) is non-decreasing and bounded fromabove, and so it converges.
B. An Exact Expression for Non-Terminating Leakage
Theorem 1 reveals our notion of non-terminating leakage
to be well-defined, and taking the limit provides a method of
calculating it. However, we believe that it is also interesting
to find an exact expression that defines its value.
Firstly, we note that it does not suffice to use a definition
expressed in terms of (Riemann) integration:ZZ
PXY (x, y)
PXY (x, y) dy dx
log2
PX (x)PY (y)
DX DY

!

where X (n) and Y (n) denote the random variables correspond(n)(n)
ing to PX and PY . Notice that, since we only consider nobservations, and we restrict the number of secret values to(n)(n)
be finite, the sets of values DX and DY are also finite forany given n.
Next, we define the leakage from a non-terminating program
to be the limit of the above expression as n tends to infinity.
Definition 2: The leakage from a non-terminating programwith a finite number of secret values and a possibly infinite

since the probability distributions PX and PY are not continuous functions on the real numbers, but defined in termsof infinite sequences of integers; therefore, this equation
does not define a value that exists. Instead, we consider the
more general notion of mutual information [1] defined using
Lebesgue integration as follows. Riemann integration works
by partitioning the domain of a function, and here the domainof the probability distributions (the observable values) is not8continuous. Lebesgue integration, however, works by partitioning the range of a function, so using Lebesgue integration we
can find an exact expression for leakage from non-terminating
programs.
Recall, from Section III-C, that we defined random variables
X and Y on the probability space over (infinite) paths of thediscrete-time Markov chain semantics of a CH-IMP program.
These induced the probability distributions PX and PY overthe sets DX and DY , giving the probability of each possible
list of secret value mappings x ∈ DX and list of observablevalues y ∈ DY .
Previously, we imposed restrictions of finiteness on DX and
DY (which ensured that PX and PY were discrete probability
distributions and allowed us to express mutual information
as a finite summation). However, by relaxing this restriction(and allowing DY to contain infinite sequences of observablevalues), we see that X and Y remain well-defined randomvariables, with corresponding probability measures PX andPY . We can also define the joint probability distribution PXY
and the product distribution PX × PY of PX and PY .
P(n)Definition 3: The rate of leakage from a non-terminating
program with a potentially infinite number of secret andobservable values is defined as:!
(n)X
PXY (x, y)1(n)
P (x, y) log2
lim
(n)
(n)
n→∞
secrets(x) XY
P (x)P (y)
x,y
X

Y

where n is the number of observable values and secrets(x)is the number of individual secret values defined in x (unlessx is the single value that indicates that there were no secretvalues, in which case secrets(x) = 1).1
This gives the average amount of information learned by
an attacker per secret command. We note that this limit is
not guaranteed to exist. For instance, a program might leaksecret values from progressively larger domains and so thevalue might tend to infinity, or a program could alternately
leak secret values and then not leak secret values, causing
the leakage rate to oscillate rather than converge. However,
we argue that for programs where this leakage rate does notconverge, there is no natural definition of information leakage;for programs where this rate does converge, it provides anatural measure of leakage for non-terminating programs.

(x,y)

as n tends to infinity,
To find the fraction (n)XY (n)PX (x)PY (y)we use the Radon Nikodym Theorem (see e.g., [27]), whichstates that for Lebesgue integration:

D. Detecting Time-Based Leakage
We do not model an attacker that is capable of measuringtime, and we therefore do not consider time-based information
leaks. We could model an attacker’s ability to observe thepassing of time by appending a symbol τ to the list ofobservations at each time step, e.g.:

Theorem 2 (Radon Nikodym Theorem): Given two σ-finite
measures ν and µ, such that ν is absolutely continuous withrespect tof such that for any A:
R µ, there exists a functiondν.
ν(A) = A f dµ. We write f as dµ(n)Since PXY (x, y) is absolutely continuous with respect
(n)
(n)
XY
to PX (x)PY (y), we know that d(PdP
is defined.
X ×PY )
We can then give an exact expression for the leakage from
non-terminating programs:ρ(n)(V := ρ; C, σ, S, O) −−−→ (C, σ ⊕ {V 7→ n}, S, O :: τ )One side-effect of this addition is that the n that tends toinfinity for non-terminating processes would equal both thenumber of observable values and the number of steps takenby the DTMC, therefore simplifying our framework. However,
it would also lead to a very strong attacker model and such asimple discrete model of time may be unrealistic. If a realistic
model of a program’s execution time and the observable
power of the attacker existed, it could be represented in ourframework in this way.

Theorem 3: The leakage lim I(X (n) ; Y (n) ) from nonn→∞terminating programs as defined in Definition 2 equals:


Z
dPXY
dPXY .
I(X; Y ) = log2d(PX × PY )Proof Sketch: Gray ([1], p. 80, Lemma 5.2.3) provesthat if P is absolutely
continuous with respect to M thenRdP
D(P ||M ) = log2 dM(ω)dP (ω), where D is the relative
entropy. As PXY is absolutely continuous with respect to
PX × PY , we obtain D(PXY ||PX × PY ) = I(X; Y ), thus
the result follows.

V. E XTERNAL I NPUTS TO A P ROGRAM
We extend our model to account for external inputs to a
program by defining an “input V : R” command that takes an(integer) value as input from a finite range R and binds it to
the variable V . To represent the selection of particular inputs,
we introduce a probabilistic input strategy function f , whichtakes the observable values encountered at this execution stepand returns a probability distribution ρ on the values R. For a
fixed input strategy f , the resulting semantics for a CH-IMP
program is obtained by combining the following semantic rulewith those in Fig. 2:

C. Leakage over Infinitely Many Secret Values
We now consider non-terminating programs that produce an
infinite number of secret values. Clearly, an infinite amount ofsecret information could be leaked by such a program, so theleakage as defined by Definition 2 may tend to infinity. It is
more useful to consider a measure of the rate of leakage, or,more precisely, the amount of information leaked per secretvalue.

(n)

(n)

(n)

1 When there are no secret values, P
XY (x, y) = PX (x)PY (y);therefore, the leakage rate is zero.

9

for all strategies f, f ′ , then, if the mutual information isfzero for the uniform input strategy, ∀f, x, y PX|Y
(x|y) =f
fU
fU
PX|Y (x|y) = PX (x) and therefore PX is independent of
PYf , and so the mutual information is zero.
A question that naturally arises from this is “what input
strategy maximises the leakage?”. However we show that, for
non-terminating programs, such an input strategy may notexist:

f (O) → ρρ(n)(input V : R; C, o :: σ, S, O) −−−→(C, ({V 7→ n} ∪ o) :: σ, S, O :: ni )A program without an input strategy can be imagined asa (partially-observable) Markov decision process. Combining
this with a particular input strategy (sometimes referred toas a policy, or adversary in the context of Markov decision
processes) induces a discrete-time Markov chain equivalent
to the one defined by our semantics above. Our use of input
strategies is similar to that of O’Neill et al. [18], who definea language with non-probabilistic user strategies and adapt
Volpano et al.’s [4] information leakage type system to support
these user strategies.
An attacker can observe and possibly control the inputs,
so they are considered to be observable values in our model;
therefore, the semantic rule above adds the input to the listof observable values, with an i subscript to identify it as
an input. We also note that secret values defined after the
input occurs may depend on the value of the input. Here, aleak does exist; this case may, for instance, correspond to a
program in which the user must choose a secret key, and theattacker, via a particular sequence of inputs, forces the user tochoose a particular key, “revealing” its value to the attacker.
As discussed in Section I, this cannot be modelled as a formal
information-theoretic channel. Alvim et al. [17] present analternative model of interactive leakage that uses channels
with feedback to make it possible to model the system as
an information-theoretic channel.
This extension allows us to calculate the leakage froma program with a particular input strategy. Two obvious
questions that arise are “does there exist an input strategy that
leads to an information leak?” and “what function maximises
the leakage?”. To answer the first question we show that,when establishing whether a leak exists, it is sufficient toexecute a program with the strategy that chooses all inputs
uniformly:

Proposition 1: There exists a program such that, for any
input strategy f (that results in the random variables on secretvalues X f and on observable values and inputs Y f ), there
exists an input strategy f + (with random variables on secretvalues X f + and on observable values and inputs Y f + ) suchthat I(X f + ; Y f + ) > I(X f ; Y f ).
Proof: Consider the following program:new result := 0; new i := 0; new sec := { 1 7→ 0.5, 2 7→ 0.5 };secret sec;
while (i == 0) {new z := { 1 7→ 0.5, 2 7→ 0.5 };if (z == 2) { result := sec; }input i : [ 0, 1 ];}observe result;

Each time the attacker inputs 0, the probability of thesecret being copied into the variable result is increased, butnever becomes 1. When the attacker inputs 1, the program
terminates and allows the attacker to observe the outcomeof the execution. In this example, any given strategy can be
improved by inputting more 0s before inputting 1, so there isno input strategy for this program that leaks the most possible
information.
A possible extension of this work is to define the maximum
leakage as the supremium of the leakage caused by all possible
input strategies. We leave the investigation of this as future
work. O’Neill et al. [18] allow for user input strategies thatmust be kept secret from the attacker; another extension of thiswork would be to adapt their methods to add secret strategies
to our framework.

Theorem 4: For any program, there exists an input strategy
that makes the program leak information if, and only if, theprogram leaks information for an input strategy that chooses
inputs with a uniform distribution.

VI. I MPLEMENTATION
We have implemented the semantics of CH-IMP in an interpreter written in OCaml; our interpreter, along with a CH-IMP
implementation of the Dining Cryptographers protocol [28]with an arbitrary number of participants, the motivating examples in Section II-B and other programs, can be found at [29].
An interface to the interpreter reads source code in CH-IMPsyntax from a file and parses and executes it, thereby constructing the DTMC described in Section III-A. It then collapses
the DTMC to the initial and terminating states, and saves it ina machine-readable form. The interface can then be used tolist the variables whose values were marked as secret during
the program’s execution, and calculate the information leakage
from the values of any given subset of them to the observable

Proof Sketch: We note that the choice of an input strategy
may affect the probability distribution on the observable values
and inputs (PY ) and the probability distribution on the secretvalues (PX ), but it does not affect the conditional probabilityof the secret values given a particular sequence of inputs
and observable values (PX|Y ). Let P f denote the probability
distributions produced by executing a program with input
strategy f . If the mutual information is zero for the uniform
fU
and PYfU are independent andinput strategy fU , then PX
f
f′
fU
fU
(x). Since PX|Y
= PX|Y
therefore ∀x, yPX|Y (x|y) = PX
10

new m := 8192;
new a := 4801;
new c := 83;
new seed := [ 0 .. 8191 ];VII. F ROM C OMPUTATION TO E STIMATION OF L EAKAGE
Given these limitations of the OCaml implementation,
along with the difficulty of expressing complex algorithms in
CH-IMP syntax, it would be ideal to a) accurately measure
information leakage through means other than precise computation, and b) measure leakage from programs written ina widely-used, real-world programming language. We havetherefore developed a second tool, LeakWatch, that estimatesthe information leakage from secret to observable values inJava programs. Programmers identify the secret and observablevalues in their programs by calling methods exposed by the
LeakWatch API. LeakWatch repeatedly executes a program’s
main method and collects the lists of secret and observablevalues defined during each execution, then estimates the joint
probability distribution of the secret and observable values(rather than computing it precisely, as in Section III-C). Thisapproximated distribution can then be used to estimate theleakage from the secret values to the observable values, as
described in our earlier work on statistical approximation ofmutual information [2]. Other tools, e.g., Weka [30], containloosely similar functionality, but do not calculate confidence
intervals for their estimates or test for compatibility with zeroleakage. LeakWatch does, and is thus more reliably able toidentify statistically significant information leaks in sourcecode.
To demonstrate how LeakWatch can be used to find information leaks in larger, more complex programs, we use it toestimate the information leakage from several real-world Java
examples. The examples encompass a number of the models
in Fig. 1, rather than only the classic leakage model shownin Fig. 1a. Table I shows how LeakWatch performs on theseexamples, in terms of the approximate number of executions
required for the leakage estimation to “stabilise” (i.e., forsuccessive estimations to differ by fewer than 0.01 bits) tothe nearest 1,000 executions, and the total time required to
produce this estimation. For instance, LeakWatch estimates theinformation leakage in ChimpLCG, a Java reimplementationof the example in Fig. 3, to be ≈ 2.5 bits after 50,000
executions in 21 seconds, thus demonstrating the viability of
our statistical estimation technique.
The Java source code for all of these examples, along withthe tool itself, can be downloaded from [32]. Further examplesof the underlying estimation technique being applied to realworld scenarios can be found in [2], [33].

new rand1 := (a * seed + c) mod m;
new card1 := rand1 mod 52;
observe card1;
new rand2 := (a * rand1 + c) mod m;
new card2 := (card1 + 1 + (rand2 mod 51)) mod 52;
secret card2;
Fig. 3. A CH-IMP implementation of a random playing card selector using
a linear congruential generator. “[ m .. n ]” is syntactic sugar for the uniform
distribution ranging over the integers (m, . . . , n).

values. The tool can calculate the mutual information, minentropy leakage and conditional entropy of the selected secretvalues and observable values.
A. Example: A Pseudorandom Number Generator
Linear congruential generators (LCGs) are widely used
for generating pseudorandomness. An LCG L is defined by
Ln ≡ (a · Ln−1 + c) mod m, where m (the modulus), a (themultiplier) and c (the increment) are parameters chosen by
the programmer, and L0 is the LCG’s seed value. The choiceof m, a and c controls the quality of the pseudorandomness
provided by the LCG: good values maximise the period of the
LCG and thus make the sequence of generated numbers lesspredictable, while bad values shorten the period and make thesequence more predictable.
Fig. 3 presents a CH-IMP implementation of a random
playing card selector. It answers the following question: if
playing cards are chosen randomly from a deck according toan LCG with m = 8192, a = 4801 and c = 83 and dealt toeach player, how much information does a player learn about
the face value of the next card dealt to their opponent basedon the face value of the card they were just dealt? In thiscase, the answer is ≈ 2.5 bits, which constitutes a significant
leak; these values of m, a and c therefore produce lowquality pseudorandomness. By making the minor modificationa = 4805 the leakage is reduced to ≈ 0.03 bits, underlining theimportance of choosing appropriate parameters for an LCG.
B. Performance
Our OCaml implementation of CH-IMP’s semantics performs well on programs of any length provided that thecorresponding DTMC remains relatively small: the playing
card selector example above, which has a state space of
3+213 ×7 = 57347, terminates in under a second on a modest
desktop computer. The time required to analyse a CH-IMP
program in this way can be exponential in the number ofsecret values, observable values and variables in scope: cases
where the size of the DTMC explodes exponentially take much
longer to terminate, as commands must be evaluated in more(and larger) states; nevertheless, our implementation provides aworking prototype of the semantics, gives us confidence in its
correctness, and allows for the precise computation of leakage
from programs with low to medium complexity.

A. Example: Visual Basic’s Rnd() Function
The API for the Visual Basic family of programming
languages exposes a Rnd() function that uses an LCG toreturn pseudorandom numbers. Visual Basic uses the LCG parameters m = 224 , a = 1140671485 and c = 12820163; thesevalues are too large to be used in the OCaml implementation
presented in Section VI, particularly that of m: since the valueof L0 must fall between 0 and m, a precise computation of
the leakage from such a program would require the generationand traversal of a DTMC with 3 + 224 × 7 ≈ 117 million
states, which is impractical. In a Java reimplementation of11

Program name

Description

Observable(s)Secret(s)Executions

Time (min)ChimpLCG

Reimplementation of CH-IMP playing card
selector (see Section VI-A)
Playing card selector example with emulation of Visual Basic’s Rnd() function
Leakage about Bloom filter set membershipbased on its internal state

Opponent’s card

Our card

50,0000.3

Opponent’s card

Our card

60,0000.4

Bloom filter’s internal
bit array

1 integer

4,000

0.2

20,00044,00088,000234,000
513,000
23,000

0.9
2.0
4.2
11.6
24.4
4.4

VisualBasicLCG
BloomFilter

SDM

Information learnt about contents of Secure
Data Manager [31] databases

Size ofdatabaseencrypted

2 integers
3 integers
4 integers
5 integers
6 integers
Number of accounts
in database

TABLE IB ENCHMARKING L EAK WATCH ’ S PERFORMANCE WHEN ESTIMATING LEAKAGE FROM SEVERAL JAVA PROGRAMS .

the example in Fig. 3 with Visual Basic’s LCG parameters,
LeakWatch reveals a leak of ≈ 0.93 bits from the face valueof the first chosen card to the face value of the second.
B. Example: Internal State of a Bloom Filter
A Bloom filter is a probabilistic data structure used to test
for set membership. The filter’s internal state is a bit arrayof length l, with all bits initially set to 0; when elements are“added” to the filter, some of these bits are set to 1 to indicatethat element’s membership of the set. The precise bits that are
set is determined by the output of a hash function H that takes
the element’s value as input and and outputs the indeces of kbits whose values should be set to 1. Membership of the set
can then be tested by checking whether the k bits of the filter
corresponding to the test value are set to 1.
Since Bloom filters are probabilistic, it is possible (andindeed common, for small values of l) for collisions to occur inthe output of H. Thus, the filter could mistakenly identify anelement as a member of the set if all of its corresponding k bits
were set to 1 by other additions to the filter, resulting in a false
positive. The filter’s internal state therefore leaks a variable
amount of information about the values of the elements added
to it depending on the size of l and k and the number of
elements added.
In this example, n integers between 0 and 7 inclusive areadded to an existing Java implementation of a Bloom filter [34]with parameters l = 16 and k = 2. LeakWatch demonstrates
that, as n increases, the average amount of information leaked
about each integer added to the filter decreases as more
collisions occur and the probability of encountering false
positives increases (see Table II).

Integers added

Leakage (bits)

Leakage per integer (bits)

1
2
3
4
5
6

2.80
5.04
6.20
6.64
6.84
6.86

2.8
2.5
2.1
1.6
1.4
1.1

TABLE II
T HE AMOUNT OF INFORMATION LEAKED ABOUT THE INTEGERS ADDEDTO A B LOOM FILTER FROM THE FILTER ’ S INTERNAL STATE .

must be taken when designing password managers to ensurethat information about the database is not inadvertently leaked
when it is encrypted. Secure Data Manager [31], a free password manager written in Java, contains such a flaw: databases
are serialised and DES-encrypted under a user-specified key
but are not padded before being written to disk, so the sizeof the encrypted file leaks information about the numberof accounts stored in the unencrypted database. LeakWatch
indicates that an attacker can guess the approximate numberof accounts in the database by observing the size of theencrypted file; this can be verified by randomly inserting
between 1 and 32 accounts into an empty database, thenannotating the number of accounts as a secret value and thesize of the encrypted database (truncated to the nearest 100
bytes) as an observable value. The size of the leakage isestimated to be 4.72 out of 5 bits. This is a security risk:
attackers will therefore target larger encrypted files known tobe written by Secure Data Manager since they are more likely
to contain larger numbers of account details. This example
demonstrates how software developers can use LeakWatch todetect new information leaks in their own software as part oftheir development flow.

C. Example: A Password Manager
Password management software is commonly used to securely store databases of sensitive account details, such as
login names and passwords for web sites. To protect the
database, the password manager encrypts it with a userspecified passphrase before writing it to a file on disk; toretrieve the database at a later time, the user must load theencrypted file and re-enter the passphrase for decryption. Care

VIII. C ONCLUSION
We have presented a framework that can be used to measure
information leaks between arbitrary points in a program. To
do so, we have introduced CH-IMP, a language that allows
variables’ values to be annotated as either secret or observable12

by an attacker, and that provides a mechanism for quantifying information leaks from secret to observable values. The
language is underlied by a coherent model of information
leakage for terminating programs, which we extended to nonterminating programs by taking the limit of the leakage formutual information, and extended further to programs that
produce potentially infinite numbers of secret and observablevalues. These methods could equally be applied to minentropy leakage, and we plan to do so in further work. We
also modelled attacker input strategies in our framework andshowed that, when we wish to discover if a leak exists for any
possible input strategy, it is sufficient to test a program witha uniform input strategy that ignores the observable values.
We have built a prototype implementation of our semantics
in OCaml that can be used to measure information leakage
from programs of low to medium complexity; we extended
this to real-world programs by developing a tool, LeakWatch,that uses statistical approximation to estimate leakage fromJava programs. In both cases, the secret and observable values
occur at arbitrary points throughout the program; therefore, ourmethods of quantifying leakage were only achievable using theleakage model presented in this paper.

[12] K. Chatzikokolakis, C. Palamidessi, and P. Panangaden, “Anonymity
Protocols as Noisy Channels,” Information and Computation, vol. 206,
no. 2–4, pp. 378–401, 2008.
[13] F. Biondi, A. Legay, P. Malacaria, and A. Wasowski, “Quantifying
information leakage of randomized protocols,” in Proc. VMCAI’13,
2013, pp. 68–87.
[14] A. McIver and C. Morgan, “Programming methodology,” A. McIver
and C. Morgan, Eds. New York, NY, USA: Springer-Verlag New York,
Inc., 2003, ch. A probabilistic approach to information hiding, pp.
441–460. [Online]. Available: http://dl.acm.org/citation.cfm?id=766951.
766972[15] A. McIver, L. Meinicke, and C. Morgan, “Security, probability andnearly fair coins in the cryptographers’ cafe;,” in Proceedings of the 2ndWorld Congress on Formal Methods, ser. FM ’09. Berlin, Heidelberg:
Springer-Verlag, 2009, pp. 41–71.
[16] A. Askarov and A. Sabelfeld, “Gradual release: Unifying declassification, encryption and key release policies,” in Security and Privacy, 2007.
SP’07. IEEE Symposium on. IEEE, 2007, pp. 207–221.
[17] M. S. Alvim, M. E. Andrés, and C. Palamidessi, “Quantitative information flow in interactive systems,” Journal of Computer Security, vol. 20,
no. 1, pp. 3–50, 2012.
[18] K. R. O’Neill, M. R. Clarkson, and S. Chong, “Information-flow security
for interactive programs,” in Computer Security Foundations Workshop,
2006. 19th IEEE, 2006.
[19] C. Mu and D. Clark, “A tool: quantitative analyser for programs,”
in Proceedings of the 8th International Conference on Quantitative
Evaluation of Systems (QEST 2011), 2011, pp. 145–146.
[20] F. Biondi, A. Legay, L. Traonouez, and A. Wasowski, “QUAIL: A
Quantitative Security Analyzer for Imperative Code,” in Proceedingsof the 25th International Conference on Computer Aided Verification(CAV 2013), 2013.
[21] A. C. Myers and B. Liskov, “Complete, Safe Information Flow with
Decentralized Labels,” in Proceedings of the 1998 IEEE Symposium
on Security and Privacy. Oakland, California, USA: IEEE Computer
Society, May 1998, pp. 186–197.
[22] S. McCamant and M. D. Ernst, “Quantitative Information Flow as
Network Flow Capacity,” in Proceedings of the ACM SIGPLAN 2008
Conference on Programming Language Design and Implementation(PLDI 2008). Tucson, Arizona, USA: ACM Press, Jun. 2008, pp.
193–205.
[23] J. Kemeny, J. Snell, and A. Knapp, Denumerable Markov Chains,
2nd ed. Springer-Verlag, 1976.
[24] T. M. Cover and J. A. Thomas, Elements of Information Theory, 2nd ed.
Wiley-Interscience, 2006.
[25] G. Smith, “On the foundations of quantitative information flow,” in
FOSSACS ’09: Proceedings of the 12th International Conference onFoundations of Software Science and Computational Structures. Berlin,
Heidelberg: Springer-Verlag, 2009, pp. 288–302.
[26] ——, “Quantifying Information Flow Using Min-Entropy,” in Proceedings of the 8th International Conference on Quantitative Evaluation of
Systems (QEST 2011), 2011, pp. 159–167.
[27] A. C. Zaanen, Introduction to Operator Theory in Riesz spaces.
Springer, 1996.
[28] D. Chaum, “The Dining Cryptographers Problem: Unconditional Senderand Recipient Untraceability,” in Journal of Cryptology, 1988, pp. 65–
75.
[29] http://www.cs.bham.ac.uk/research/projects/infotools/chimp/.
[30] M. Hall, E. Frank, G. Holmes, B. Pfahringer, P. Reutemann, and I. H.
Witten, “The WEKA data mining software,” SIGKDD Explorations,vol. 11, no. 1, pp. 10–18, 2009.
[31] “Secure Data Manager,” http://sdm.sourceforge.net.
[32] http://www.cs.bham.ac.uk/research/projects/infotools/leakwatch/.
[33] T. Chothia, Y. Kawamoto, and C. Novakovic, “A Tool for Estimating
Information Leakage,” in Proceedings of the 25th International Conference on Computer Aided Verification (CAV 2013), 2013.
[34] “Bloom filters in Java,” http://www.javamex.com/tutorials/collections/bloom filter.shtml.

ACKNOWLEDGEMENT
This work was supported by EPSRC Research Grant
EP/J009075/1. We also wish to thank Olga Maleva for her
helpful advice.
R EFERENCES[1] R. Gray, Entropy and Information Theory, 1st ed. Springer, 1991.
[2] K. Chatzikokolakis, T. Chothia, and A. Guha, “Statistical Measurementof Information Leakage,” in The 16th International Conference on Tools
and Algorithms for the Construction and Analysis of Systems (TACAS2010), ser. LNCS, 2010, pp. 390–404.
[3] http://www.cs.bham.ac.uk/research/projects/infotools/.
[4] D. Volpano, C. Irvine, and G. Smith, “A sound type system for secureflow analysis,” Journal of Computer Security, vol. 4, no. 2–3, pp. 167–
187, Jan. 1996.
[5] D. Clark, S. Hunt, and P. Malacaria, “Quantified interference for a while
language,” Electron. Notes Theor. Comput. Sci., vol. 112, pp. 149–166,
2005.
[6] ——, “A static analysis for quantifying information flow in a simple
imperative language,” Journal of Computer Security, vol. 15, no. 3, pp.
321–371, 2007.
[7] M. Backes, B. Köpf, and A. Rybalchenko, “Automatic Discovery and
Quantification of Information Leaks,” in Proceedings of the 30th IEEE
Symposium on Security and Privacy. Oakland, California, USA: IEEE
Computer Society, May 2009, pp. 141–153.
[8] A. Almeida Matos and G. Boudol, “On declassification and the nondisclosure policy,” Journal of Computer Security, vol. 17, no. 5, pp.
549–597, 2009.
[9] A. Dekhtyar and V. S. Subrahmanian, “Hybrid Probabilistic Programs,”
Journal of Logic Programming, vol. 3, no. 2, pp. 187–250, Jun. 2000.
[10] A. Pfeffer, “IBAL: A Probabilistic Rational Programming Language,” inProceedings of the 17th International Joint Conference on Artificial Intelligence (IJCAI 2001). Seattle, Washington, USA: Morgan Kaufmann,
Aug. 2001, pp. 733–740.
[11] D. Kozen, “Semantics of probabilistic programs,” Journal of Computerand System Sciences, vol. 22, no. 3, pp. 328–350, 1981.

13