Quantitative Information Flow – Verification Hardness and Possibilities
Hirotoshi Yasuoka
Graduate School of Information Sciences
Tohoku University
Sendai, Japanyasuoka@kb.ecei.tohoku.ac.jp

Tachio Terauchi
Graduate School of Information Sciences
Tohoku University
Sendai, Japanterauchi@ecei.tohoku.ac.jp

We consider programs containing high security inputs andlow security outputs. Informally, the quantitative information
flow problem concerns the amount of information that an
attacker can learn about the high security input by executing
the program and observing the low security output. The
problem is motivated by applications in information security.
We refer to the classic by Denning [12] for an overview.
In essence, quantitative information flow measures how
secure, or insecure, a program is. Thus, unlike noninterference [14], that only tells whether a program iscompletely secure or not completely secure, a definition ofquantitative information flow must be able to distinguish two
programs that are both interferent but have different degrees
of “secureness.”
For example, consider the following two programs:

In both programs, H is a high security input and O isa low security output. Viewing H as a password, M1 isa prototypical login program that checks if the guess gmatches the password.1 By executing M1 , an attacker only
learns whether H is equal to g, whereas she would be able
to learn the entire content of H by executing M2 . Hence, areasonable definition of quantitative information flow should
assign a higher quantity to M2 than to M1 , whereas noninterference would merely say that M1 and M2 are bothinterferent, assuming that there are more than one possible
value of H.
Researchers have attempted to formalize the definition ofquantitative information flow by appealing to information
theory. This has resulted in definitions based on the Shannon
entropy [12], [7], [19], the min entropy [29], the guessing
entropy [16], [1], and channel capacity [22], [20], [26].
Much of the previous research has focused on information
theoretic properties of the definitions and approximate (i.e.,
incomplete and/or unsound) algorithms for checking andinferring quantitative information flow according to suchdefinitions.
In this paper, we give a verification theoretic and complexity theoretic analysis of quantitative information flow
and investigate precise methods for checking quantitative
information flow. In particular, we study the following comparison problem: Given two programs M1 and M2 , decide
if X (M1 ) ≤ X (M2 ). Here X (M ) denotes the information
flow quantity of the program M according to the quantitative
information flow definition X where X is either SE [µ](Shannon-entropy based with distribution µ), ME [µ] (minentropy based with distribution µ), GE [µ] (guessing-entropy
based with distribution µ), or CC (channel-capacity based).
Note that, obviously, the comparison problem is no harderthan actually computing the quantitative information flow as
we can compare the two numbers once we have computed
X (M1 ) and X (M2 ).
Concretely, we show the following negative results, where
X is CC , SE [µ], ME [µ], or GE [µ] with µ uniform.
• Checking if X (M1 ) ≤ X (M2 ) is not a k-safety

M1 ≡ if H = g then O := 0 else O := 1
M2 ≡ O := H

1 Here, for simplicity, we assume that g is a program constant. See
Section II for modeling attacker/user (i.e., low security) inputs.

Abstract—Researchers have proposed formal definitions ofquantitative information flow based on information theoretic
notions such as the Shannon entropy, the min entropy, theguessing entropy, and channel capacity. This paper investigates
the hardness and possibilities of precisely checking and inferring quantitative information flow according to such definitions.
We prove that, even for just comparing two programs on
which has the larger flow, none of the definitions is a ksafety property for any k, and therefore is not amenable
to the self-composition technique that has been successfully
applied to precisely checking non-interference. We also show
a complexity theoretic gap with non-interference by proving
that, for loop-free boolean programs whose non-interference is
coNP-complete, the comparison problem is #P-hard for all of
the definitions.
For positive results, we show that universally quantifying the
distribution in the comparison problem, that is, comparing two
programs according to the entropy based definitions on which
has the larger flow for all distributions, is a 2-safety problem
in general and is coNP-complete when restricted for loop-freeboolean programs. We prove this by showing that the problem
is equivalent to a simple relation naturally expressing the factthat one program is more secure than the other. We prove thatthe relation also refines the channel-capacity based definition,and that it can be precisely checked via the self-composition
as well as the “interleaved” self-composition technique.

I. I NTRODUCTION

property [30], [9] for any k.
Restricted to loop-free boolean programs, checking if
X (M1 ) ≤ X (M2 ) is #P-hard.
The results are in stark contrast to non-interference which
is known to be a 2-safety property in general [3], [11](technically, for the termination-insensitive case2 ) and can beshown to be coNP-complete for loop-free boolean programs(proved in Section III-C). (#P is known to be as hard as theentire polynomial hierarchy [31].) The results suggest thatprecisely inferring (i.e., computing) quantitative information
flow according to these definitions would be harder thanchecking non-interference and may require a very different
approach (i.e., not self composition [3], [11], [30]).
We also give the following positive results which showthat checking if the quantitative information flow of one program is larger than the other for all distributions according
to the entropy-based definitions is easier. Below, Y is SE ,ME , or GE .
• Checking if ∀µ.Y[µ](M1 ) ≤ Y[µ](M2 ) is a 2-safety
property.
• Restricted to loop-free boolean programs, checking if∀µ.Y[µ](M1 ) ≤ Y[µ](M2 ) is coNP-complete.
These results are proven by showing that the problems ∀µ.SE [µ](M1 ) ≤ SE [µ](M2 ), ∀µ.ME [µ](M1 ) ≤ME [µ](M2 ), and ∀µ.GE [µ](M1 ) ≤ GE [µ](M2 ) are all
actually equivalent to a simple 2-safety relation R(M1 , M2 ).
We also show that this relation refines the channel-capacity
based quantitative information flow, that is, if R(M1 , M2 )then CC (M1 ) ≤ CC (M2 ).
The fact that R(M1 , M2 ) is a 2-safety property implies
that it can be reduced to a safety problem via self composition. This leads to a new approach to precisely checking
quantitative information flow that leverages recent advancesin automated software verification [2], [15], [24], [4]. Briefly,
given M1 and M2 , R(M1 , M2 ) means that M1 is at least
as secure as M2 for all distributions while ¬R(M1 , M2 )means that there must be a distribution in which M1 is lesssecure than M2 , according to the entropy-based definitionsof quantitative information flow. Therefore, by deciding
R(M1 , M2 ), we can measure the security of the programM1 relative to another specification program M2 . Note that
this is useful even when M1 and M2 are “incomparable”
by R, that is, when ¬R(M1 , M2 ) and ¬R(M2 , M1 ). See
Section IV-B for the details.
The rest of the paper is organized as follows. Section II
reviews the existing information-theoretic definitions ofquantitative information flow. Section III proves the hardnessof their comparison problems and thus shows the hardness of
precisely inferring quantitative information flow according
to these definitions. Section IV introduces the relation R•

2 We restrict to terminating programs in this paper. (The termination
assumption is nonrestrictive because we assume safety verification as a
blackbox routine.)and proves it equivalent to the comparison problems forthe entropy-based definitions with their distributions universally quantified. The section also shows that this is a
2-safety property and is easier to decide than the nonuniversally-quantified comparison problems, and suggests
a self-composition based method for precisely checking
quantitative information flow. Section V discusses related
work, and Section VI concludes. Appendix A contains the
supporting lemmas and definitions for the proofs appearing
in the main text. The omitted proofs appear in Appendix B.
II. P RELIMINARIES
We introduce the information theoretic definitions ofquantitative information flow that have been proposed inliterature. First, we review the notion of the Shannon entropy [28], H[µ](X), which is the average of the information content, and intuitively, denotes the uncertainty of therandom variable X.
Definition 2.1 (Shannon Entropy): Let X be a randomvariable with sample space X and µ be a probability
distribution associated with X (we write µ explicitly forclarity). The Shannon entropy of X is defined as
X
1
H[µ](X) =µ(X = x) logµ(X = x)x∈X

(The logarithm is in base 2.)
Next, we define conditional entropy. Informally, the conditional entropy of X given Y denotes the uncertainty of X
after knowing Y .
Definition 2.2 (Conditional Entropy): Let X and Y be
random variables with sample spaces X and Y, respectively,
and µ be a probability distribution associated with X and
Y . Then, the conditional entropy of X given Y , written
H[µ](X|Y ) is defined asX
H[µ](X|Y ) =µ(Y = y)H[µ](X|Y = y)
y∈Y

where
H[µ](X|Y = y)X=µ(X = x|Y = y) log

1µ(X = x|Y = y)x∈Xµ(X = x, Y = y)µ(X = x|Y = y) =µ(Y = y)Next, we define (conditional) mutual information. Intuitively, the conditional mutual information of X and Y
given Z represents the mutual dependence of X and Y after
knowing Z.
Definition 2.3 (Mutual Information): Let X, Y and Z
be random variables and µ be an associated probability
distribution.3 Then, the conditional mutual information of
3 We abbreviate sample spaces of random variables when they are clear
from the context.

X and Y given Z is defined as
I[µ](X; Y |Z)= H[µ](X|Z) − H[µ](X|Y, Z)= H[µ](Y |Z) − H[µ](Y |X, Z)

Let M be a program that takes a high security input H anda low security input L, and gives the low security output O.
For simplicity, we restrict to programs with just one variableof each kind, but it is trivial to extend the formalism tomultiple variables (e.g., by letting the variables range overtuples). Also, for the purpose of the paper, unobservable(i.e., high security) outputs are irrelevant, and so we assume
that the only program output is the low security output.
Let µ be a probability distribution over the values of H
and L. Then, the semantics of M can be defined by thefollowing probability equation. (We restrict to terminating
deterministic programs in this paper.)Xµ(O = o) =µ(H = h, L = `)h, ` ∈ H, L
M (h, `) = o

Note that we write M (h, `) to denote the low security outputof the program M given inputs h and `. Now, we areready to introduce the Shannon-entropy based definition ofquantitative information flow (QIF) [12], [7], [19].
Definition 2.4 (Shannon-Entropy-based QIF): Let M
be a program with a high security input H, a low security
input L, and a low security output O. Let µ be a distribution
over H and L. Then, the Shannon-entropy-based quantitative information flow is defined
SE [µ](M )= I[µ](O; H|L)
= H[µ](H|L) − H[µ](H|O, L)

Intuitively, H[µ](H|L) denotes the initial uncertainty knowing the low security input and H[µ](H|O, L) denotes theremaining uncertainty after knowing the low security output.
As an example, consider the programs M1 and M2 from
Section I. For concreteness, assume that g is the value 01
and H ranges over the space {00, 01, 10, 11}. Let U be theuniform distribution over {00, 01, 10, 11}, that is, U (h) =1/4 for all h ∈ {00, 01, 10, 11}. The results are as follows.
SE [U ](M1 )SE [U ](M2 )= H[U ](H) − H[U ](H|O)= log 4 − 43 log 3≈ .81128= H[U ](H) − H[U ](H|O)= log 4 − log 1= 2

Consequently, we have that SE [U ](M1 ) ≤ SE [U ](M2 ), but
SE [U ](M2 ) 6≤ SE [U ](M1 ). That is, M1 is more securethan M2 (according to the Shannon-entropy based definition
with uniformly distributed inputs), which agrees with ourintuition.
Let us recall the notion of non-interference [10], [14].

Definition 2.5 (Non-intereference): A program M issaid to be non-interferent iff for any h, h0 ∈ H and ` ∈ L,
M (h, `) = M (h0 , `).
It is worth noting that non-interference can be formalized
as a special case of the Shannon-entropy based quantitative
information flow where the flow quantity is zero.
Theorem 2.6: Let M be a program that takes highsecurity input H, low-security input L, and returns lowsecurity output O. Then, M is non-interferent if and only if∀µ.SE [µ](M ) = 0.
The above theorem is complementary to the one proven by
Clark et al. [5] which states that for any µ such that µ(H =h, L = `) > 0 for all h ∈ H and ` ∈ L, SE [µ](M ) = 0 iff
M is non-interferent.
Next, we introduce the min entropy, which Smith [29]recently suggested as an alternative measure for quantitative
information flow.
Definition 2.7 (Min Entropy): Let X and Y be randomvariables, and µ be an associated probability distribution.
Then, the min entropy of X is defined
H∞ [µ](X) = log

1
V[µ](X)and the conditional min entropy of X given Y is defined
H∞ [µ](X|Y ) = log

1
V[µ](X|Y )where
V[µ](X) = maxx∈X µ(X = x)V[µ](X|Y = y) = P
maxx∈X µ(X = x|Y = y)V[µ](X|Y ) =y∈Y µ(Y = y)V[µ](X|Y = y)Intuitively, V[µ](X) represents the highest probability thatan attacker guesses X in a single try. We now define the minentropy-based definition of quantitative information flow.
Definition 2.8 (Min-Entropy-based QIF): Let M be a
program with a high security input H, a low security input
L, and a low security output O. Let µ be a distribution
over H and L. Then, the min-entropy-based quantitative
information flow is defined
ME [µ](M ) = H∞ [µ](H|L) − H∞ [µ](H|O, L)
Whereas Smith [29] focused on programs lacking low
security inputs, we extend the definition to programs withlow security inputs in the definition above. It is easy to
see that our definition coincides with Smith’s for programs
without low security inputs. Also, the extension is arguably
natural in the sense that we simply take the conditional
entropy with respect to the distribution over the low security
inputs.
Computing the min-entropy based quantitative information flow for our running example programs M1 and M2

from Section I with the uniform distribution, we obtain,
ME [U ](M1 )= H∞ [U ](H) − H∞ [U ](H|O)= log 4 − log 2= 1

ME [U ](M2 )= H∞ [U ](H) − H∞ [U ](H|O)= log 4 − log 1= 2

Again, we have that ME [U ](M1 ) ≤ ME [U ](M2 ) andME [U ](M2 ) 6≤ ME [U ](M1 ), and so M2 is deemed lesssecure than M1 .
The third definition of quantitative information flow
treated in this paper is the one based on the guessing
entropy [21], that is also recently proposed in literature [16],[1].
Definition 2.9 (Guessing Entropy): Let X and Y be
random variables, and µ be an associated probability distribution. Then, the guessing entropy of X is definedX
G[µ](X) =i × µ(X = xi )1≤i≤mwhere {x1 , x2 , . . . , xm } = X and ∀i, j.i ≤ j ⇒ µ(X =xi ) ≥ µ(X = xj ).
The conditional guessing entropy of X given Y is definedX
X
G[µ](X|Y ) =µ(Y = y)i × µ(X = xi |Y = y)
y∈Y

1≤i≤m

where {x1 , x2 , . . . , xm } = X and ∀i, j.i ≤ j ⇒ µ(X =xi |Y = y) ≥ µ(X = xj |Y = y).
Intuitively, G[µ](X) represents the average number oftimes required for the attacker to guess the value of X. We
now define the guessing-entropy-based quantitative information flow.
Definition 2.10 (Guessing-Entropy-based QIF): Let
M be a program with a high security input H, a low
security input L, and a low security output O. Let µ bea distribution over H and L. Then, the guessing-entropybased quantitative information flow is defined
GE [µ](M ) = G[µ](H|L) − G[µ](H|O, L)
Like with the min-entropy-based definition, the previous
research on guessing-entropy-based quantitative information
flow only considered programs without low security inputs [16], [1]. But, it is easy to see that our definition withlow security inputs coincides with the previous definitions
for programs without low security inputs. Also, as withthe extension for the min-entropy-based definition, it simply
takes the conditional entropy over the low security inputs.
We test GE on the running example from Section I by
calculating the quantities for the programs M1 and M2 withthe uniform distribution.
GE [U ](M1 ) = G[U ](H) − G[U ](H|O)= 25 − 47= 0.75
GE [U ](M2 )= G[U ](H) − G[U ](H|O)= 52 − 1= 1.5

Therefore, we again have that GE [U ](M1 ) ≤ GE [U ](M2 )and GE [U ](M2 ) 6≤ GE [U ](M1 ), and so M2 is consideredless secure than M1 , even with the guessing-entropy based
definition with the uniform distribution.
The fourth and the final existing definition of quantitative
information flow that we introduce in this paper is the one
based on channel capacity [22], [20], [26], which is simply
defined to be the maximum of the Shannon-entropy based
quantitative information flow over the distribution.
Definition 2.11 (Channel-Capacity-based QIF): Let
M be a program with a high security input H, a low
security input L, and a low security output O. Then, thechannel-capacity-based quantitative information flow isdefinedCC (M ) = max I[µ](O; H|L)µ

Unlike the Shannon-entropy based, the min-entropy
based, and the guessing-entropy based definitions, thechannel-capacity based definition of quantitative information
flow is not parameterized by a distribution over the inputs.
As with the other definitions, let us test the definition on therunning example from Section I by calculating the quantities
for the programs M1 and M2 :CC (M1 )= maxµ I[µ](O; H)= 1

CC (M2 )= maxµ I[µ](O; H)= 2

As with the entropy-based definitions (with the uniform
distribution), we have that CC (M1 ) ≤ CC (M2 ) andCC (M2 ) 6≤ CC (M1 ), that is, the channel-capacity based
quantitative information flow also says that M2 is less securethan M1 .
III. H ARDNESS OF C OMPARISON P ROBLEMS
We investigate the hardness of deciding the following
comparison problem CSE [µ]: Given programs M1 and M2
having the same input domain, decide if SE [µ](M1 ) ≤SE [µ](M2 ). Because we are interested in hardness, we focus
on the case where µ is the uniform distribution U . Thatis, the results we prove for the specific case applies to thegeneral case. Also note that the comparison problem is noharder than actually computing the quantitative information
flow because we can compare SE [µ](M1 ) and SE [µ](M2 )if we know their actual values.

Likewise, we study the hardness of the comparison problem CME [µ], defined to be the problem
ME [µ](M1 ) ≤ ME [µ](M2 ), CGE [µ], defined to be theproblem GE [µ](M1 ) ≤ GE [µ](M2 ), and CCC , defined tobe the problem CC (M1 ) ≤ CC (M2 ). As with CSE [µ], we
require the two programs to share the same input domain
for these problems.
We show that none of these comparison problems are ksafety problems for any k. Informally, a program property issaid to be a k-safety property [30], [9] if it can be refuted byobserving k number of (finite) execution traces. A k-safety
problem is the problem of checking a k-safety property.
Note that the standard safety property is a 1-safety property.
An important property of a k-safety problem is that it canbe reduced to a standard safety (i.e., 1-safety) problem,
such as the unreachability problem, via a simple programtransformation called self composition [3], [11].
It is well-known that non-interference is a 2-safety property,4 and this has enabled its precise checking via a
reduction to a safety problem via self composition andpiggybacking on advances in automated safety verification
methods [30], [25], [32]. Unfortunately, the results in thissection imply that quantitative information flow inference
problem is unlikely to receive the same benefits.
Because we are concerned with properties about pairs ofprograms (i.e., comparison problems), we extend the notionof k-safety to properties refutable by observing k traces fromeach of the two programs. More formally, we say that thecomparison problem C is a k-safety property if (M1 , M2 ) 6∈
C implies that there exists T1 ⊆ [[M1 ]] and T2 ⊆ [[M2 ]] suchthat(1) |T1 | ≤ k(2) |T2 | ≤ k(3) ∀M10 , M20 .T1 ⊆ [[M10 ]] ∧ T2 ⊆ [[M20 ]] ⇒ (M10 , M20 ) 6∈ C
In the above, [[M ]] denotes the semantics (i.e., traces)of M , represented by the set of input/output pairs{((h, `), o) | h ∈ H, ` ∈ L, o = M (h, `)}.
We now state the main results of the section. (Recall thatU denotes the uniform distribution.) We sketch the mainidea of the proofs. All proofs are by contradiction. Let C
be the comparison problem in the statement and suppose C
is k-safety. Let (M1 , M2 ) 6∈ C. Then, we have T1 ⊆ [[M1 ]]and T2 ⊆ [[M2 ]] satisfying the properties (1), (2), and (3)above. From this, we construct M̄1 and M̄2 such that T1 ⊆[[M̄1 ]] and T2 ⊆ [[M̄2 ]] and (M̄1 , M̄2 ) ∈ C to obtain thecontradiction.
Theorem 3.1: CSE [U ] is not a k-safety property for any
k > 0.
Theorem 3.2: CME [U ] is not a k-safety property for any
k > 0.
Theorem 3.3: CGE [U ] is not a k-safety property for any
k > 0.
4 It is also well known that it is not a 1-safety property [23].

Theorem 3.4: CCC is not a k-safety property for any
k > 0.
A. Bounding the Domains
The notion of k-safety property, like the notion of safety
property from where it extends, is defined over all programs
regardless of their size. (For example, non-interference is a
2-safety property for all programs and unreachability is asafety property for all programs.) But, it is easy to showthat the comparison problems would become “k-safety”
properties if we constrained and bounded the input domains
because then the size of the semantics (i.e., the input/output
pairs) of such programs would be bounded by |H|×|L|. In
this case, the problems are at most |H|×|L|-safety.5 However,these bounds are high for all but very small domains, andare unlikely to lead to a practical verification method.
B. Proof of Theorem 3.1
We discuss the details of the proof of Theorem 3.1. The
proofs of Theorems 3.2, 3.3, 3.4 are deferred to Appendix B.
For contradiction, suppose CSE [U ] is a k-safety property.
Let M and M 0 be programs having the same input domainsuch that (M, M 0 ) 6∈ CSE [U ]. Then, it must be the casethat there exist T ⊆ [[M ]] and T 0 ⊆ [[M 0 ]] such that |T | ≤k, |T 0 | ≤ k, and ∀Mc , Mc0 .T ⊆ [[Mc ]] ∧ T 0 ⊆ [[Mc0 ]] ⇒(Mc , Mc0 ) 6∈ CSE [U ].
Let
T = {(h1 , o1 ), (h2 , o2 ), . . . , (hi , oi )}T 0 = {(h01 , o01 ), (h02 , o02 ), . . . , (h0j , o0j )}where i, j ≤ k. Now, we construct new programs M̄ andM̄ 0 as follows.
M̄ (h1 ) = o1M̄ (h2 ) = o2...
M̄ (hi ) = oiM̄ (hi+1 ) = oM̄ (hi+2 ) = o...
M̄ (hi+j ) = oM̄ (hi+j+1 ) = or...
M̄ (hn ) = orM̄ 0 (h01 ) = o01
M̄ 0 (h02 ) = o02...
M̄ 0 (h0j ) = o0j
M̄ 0 (h0j+1 ) = o0j+1
M̄ 0 (h0j+2 ) = o0j+2...
M̄ 0 (h0j+i ) = o0j+i
M̄ 0 (h0j+i+1 ) = o0r...
M̄ 0 (h0n ) = o0r

where• o 6= or ,• {o1 , o2 , . . . , oi } ∩ {o, or } = ∅,0000
• oj+1 , oj+2 , . . . , oj+i , and or are distinct,
0
0
0
0
0
0
• {o1 , o2 , . . . , oj } ∩ {oj+1 , . . . , oj+i , or } = ∅,00
• {h1 , . . . , hn } = {h1 , . . . , hn }, and• n = 2k.
5 It is possible to get a tighter bound for the channel-capacity based
definition by also bounding the size of the output domain.

::= x := ψ | if ψ then M else M | M0 ; M1::= true | x | φ ∧ ψ | ¬φ

Mφ, ψFigure 1.

The syntax of loop-free boolean programs

wp(x := ψ, φ) = φ[ψ/x]wp(if ψ then M0 else M1 , φ)= (ψ ⇒ wp(M0 , φ)) ∧ (¬ψ ⇒ wp(M1 , φ))wp(M0 ; M1 , φ) = wp(M0 , wp(M1 , φ))Figure 2.

The weakest precondition for loop-free boolean programs

Then, comparing the Shannon-entropy-based quantitative
information flow of M̄ and M̄ 0 , we have,
SE [U ](PM̄ 0 ) − SE [U ](M̄ )= o0 ∈{o0 ,...,o0 } U (o0x ) log U (o1 0 )
x
1
i
x
1
1
0
+ U (o0 ) log U (o0 ) + U (or ) log U (o0 )rP− ( ox ∈{o1 ,...,oj } U (ox ) log U (o1 x )P+ oy ∈{oj+1 ,...,oj+i } U (oy ) log U (o1 y )1+ U (or ) log U (o)r)(Note the abbreviations from Appendix A.) By lemma A.5,
we haveP
U (ox ) log U (o1 x )ox ∈{o1 ,...,oPi}≤ o0 ∈{o0 ,...,o0 } U (o0y ) log U (o1 0 )
y

j+1

j+i

y

and
1
U (o) log U (o)≤10o0x ∈{o01 ,...,o0j } U (ox ) log U (o0x )P

Trivially, we haveU (o0r ) log

11= U (or ) log0
U (or )U (or )As a result, we have
SE [U ](M̄ 0 ) − SE [U ](M̄ ) ≥ 0
Note that M̄ and M̄ 0 have the same counterexamples T and
T 0 , that is, T ⊆ [[M̄ ]] and T 0 ⊆ [[M̄ 0 ]]. However, we have(M̄ , M̄ 0 ) ∈ CSE [U ]. This leads to a contradiction.
C. Complexities for Loop-free Boolean Programs
The purpose of this section is to show a complexity
theoretic gap between non-interference and quantitative information flow. The results strengthen the hypothesis thatquantitative information flow is quite hard to compute precisely, and also suggest an interesting connection to counting
problems.
We focus on loop-free boolean programs whose syntax isgiven in Figure 1. We assume the usual derived formulasφ ⇒ ψ, φ = ψ, φ ∨ ψ, and false. We give the usual weakest
precondition semantics in Figure 2.
To adapt the information flow framework to boolean programs, we make each information flow variable H, L, and O

range over functions mapping boolean variables of its kind toboolean values. So, for example, if x and y are low security
boolean variables and z is a high security boolean variable,
then L ranges over the functions {x, y} → {false, true}, and
H and O range over {z} → {false, true}.6 (Every boolean
variable is either a low security boolean variable or a highsecurity boolean variable.) We write M (h, `) = o for an
input (h, `) and an output o if (h, `) |= wp(M, φ) for aboolean formula φ such that o |= φ and o0 6|= φ for all output
o0 6= o. Here, |= is the usual logical satisfaction relation,using h, `, o, etc. to look up the values of the boolean
variables. (Note that this incurs two levels of lookup.)
As an example, consider the following program.
M≡z := x; w := y;
if x ∧ y then z := ¬z else w := ¬w
Let x, y be high security variables and z, w be low security
variables. Then,SE [U ](M )ME [U ](M )= 1.5= log 3
≈ 1.5849625
GE [U ](M ) = 1.25
CC (M ) = log 3≈ 1.5849625

We prove the following hardness results. These results
are proven by a reduction from #SAT, which is the problem of counting the number of solutions to a quantifierfree boolean formula. #SAT is known to be #P-complete.
Because #SAT is a function problem and the comparison
problems are decision problems, a step in the proofs makes
binary search queries to the comparison problem oracle apolynomial number of times. (Recall that the notation FPA
means the complexity class of function problems solvablein polynomial time with an oracle for the problem A.)
Theorem 3.5: #P ⊆ FPCSE [U ]Theorem 3.6: #P ⊆ FPCME [U ]Theorem 3.7: #P ⊆ FPCGE [U ]Theorem 3.8: #P ⊆ FPCCC
We remind that the above results apply (even) when thecomparison problems CSE [U ], CME [U ], CGE [U ], and CCC
are restricted to loop-free boolean programs.
In summary, each comparison problem CSE [U ], CME [U ],CGE [U ], and CCC can be used a polynomial number oftimes to solve a #P-complete problem. Because Toda’s
theorem [31] implies that the entire polynomial hierarchy
can be solved by using a #P-complete oracle a polynomial
number of times, our results show that the comparison
problems for quantitative information flow can also be used
6 We do not distinguish input boolean variables from output boolean
variables. But, a boolean variable can be made output-only by assigning a
constant to the variable at the start of the program and made input-only byassigning a constant at the end.

a polynomial number of times to solve the entire polynomial
hierarchy, for the case of loop-free boolean programs.
As shown below, this presents a gap from noninterference, which is only coNP-complete for loop-freeboolean programs.
Theorem 3.9: Checking non-interference is coNPcomplete for loop-free boolean programs.
The above is an instance of the general observation that,by solving quantitative information flow problems, one isable to solve the class of problems known as counting
problems,7 which coincides with #SAT for the case of loopfree boolean programs.
D. Proof of Theorem 3.5
We discuss the details of the proof of Theorem 3.5. The
proofs of Theorems 3.6, 3.7, 3.8 are deferred to Appendix B.
First, we prove the following lemma which states that we
can compare the number of solutions to boolean formulasby computing SE [U ]. (For convenience, we use large letters
H, L, O, etc. to range over boolean variables as well as
generic random variables.)→−Lemma 3.10: Let H and H 0 be distinct boolean randomvariables.
Let i and j be
any non-negative integers such that→−→−i ≤ 2| H | and j ≤ 2| H | . Let ψi (resp. ψj ) be a formula→−over H having i (resp. j) assignments. Then, j ≤ i iff
SE [U ](Mj ) ≤ SE [U ](Mi ) where Mj ≡ O := ψj ∧ H 0
and Mi ≡ O := ψi ∧ H 0 .
ji
Proof: Let p = 2|H|+1
and q = 2|H|+1. We have|H|+1
2|H|+1
SE [U ](Mj ) = 2|H|+1 log 2 j + 2 2|H|+1−j log 2|H|+1−j1= p log p + (1 − p) log 1−p
|H|+1
|H|+1
i
2|H|+1
SE [U ](Mi ) = 2|H|+1
log 2 i + 2 2|H|+1−i log 2|H|+1−i1= q log q + (1 − q) log 1−q

j

•

|H|+1

Only If
Suppose j ≤ i. Then,SE [U ](Mi ) − SE [U ](Mj )1= p log p1 + (1 − p) log 1−p11−q log q − (1 − q) log 1−q
q q
p 1−q
= log( 1−pp ) 1−p ( 1−q )1−qThen, from 1−p≥ 1 and p ≥ q ≥ 0, we have

SE [U ](Mi ) − SE [U ](Mj ) ≥
≥
=
=
=
=

q q
p
log( 1−pp ) ( 1−q )q qqlog( 1−pp ) ( 1−q )(1−p)q qlog( p(1−q) )q−pq qlog( p−pq)
pq−q qlog( pq−p)1− 1

The last line follows from 1− p1 ≥ 1.
q
• If
We prove the contraposition. Suppose j > i. Then,SE [U ](Mj ) − SE [U ](Mi )1= q log 1q + (1 − q) log 1−q1−p log p1 − (1 − p) log 1−p>0
The last line follows from the fact that 0 ≤ p < q ≤ 21 .
Therefore, SE [U ](Mj ) 6≤ SE [U ](Mi ).
Then, using Lemma 3.10, we prove the following lemma
which is crucial to proving Theorem 3.5.
→−
Lemma 3.11: Let H be distinct variables and φ be a→−boolean formula over H . Then, the number of assignmentsfor φ can be computed by executing an oracle that decides→−
whether programs are in CSE [U ] at most 3 × (| H | + 1) + 2
times.
Proof: First, we define a procedure that returns thenumber of solutions of φ.
→−
Let F (j) ≡ O := ψ ∧ H 0 where ψ is a formula over H
having j assignments and H 0 be a boolean variable such→−that H 0 6∈ { H }. Note that, by Lemma A.4, such ψ can begenerated in linear time.
Then, we invoke the following procedure where M 0 ≡0O := φ ∧ H 0 .
l = 0;→−
r = 2| H | ;n = (` + r)/2;
while ¬CSE [U ](F (n), M 0 ) ∨ ¬CSE [U ](M 0 , F (n))
if CSE [U ](F (n), M 0 )then {` = n; n = (` + r)/2; }else {r = n; n = (` + r)/2; }return n
Note that when the procedure terminates, we have
SE [U ](F (n)) = SE [U ](M 0 ), and so by Lemma 3.10, n
is the number of satisfying assignments to φ.
→−
We show that the procedure iterates at most | H |+1 times.
To see this, every iteration in the procedure narrows therange→
between r and ` by one half. Because r −` is bounded−→−by 2| H | , it follows that the procedure iterates at most | H |+1→−
times. Hence, the oracle CSE [U ] is accessed 3×(| H |+1)+2
times, and this proves the lemma.
Finally, Theorem 3.5 follows from Lemma 3.11 and thefact that #SAT, the problem of counting the number ofsolutions to a boolean formula, is #P-complete.

1− 1log( 1− p1 )qq≥ 0
7 Formally, a counting problem is the problem of counting the number ofsolutions to a decision problem. For instance, #P is the class of counting
problems associated with NP.

IV. U NIVERSALLY Q UANTIFYING D ISTRIBUTIONSAs proved in Section III, precisely computing quantitative
information flow is quite difficult. Indeed, we have shownthat even just comparing two programs on which has thelarger flow is difficult (i.e., CSE , CME , CGE , and CCC ).

In this section, we show that universally quantifying
the Shannon-entropy based comparison problem CSE [µ],the min-entropy based problem CME [µ], or the guessingentropy based problem CGE [µ] over the distribution µ is
equivalent to a simple relation R enjoying the following
properties.
(1) R is a 2-safety property.
(2) R is coNP-complete for loop-free boolean programs.
Note that (1) implies that we can actually check if(M1 , M2 ) ∈ CSE [µ] for all µ via self composition (andlikewise for CME [µ] and CGE [µ]). We actually show in
Section IV-B that we can even use the security-type-based
approach suggested by Terauchi and Aiken [30] to minimize
code duplication during self composition (i.e., do interleaved
self composition).
We remind that except for the coNP-completeness result(Theorem 4.8), the results in this section apply to any(deterministic and terminating) programs and not just to
loop-free boolean programs.
Definition 4.1: We define R to be the relation such that
R(M1 , M2 ) iff for all ` ∈ L and h, h0 ∈ H, if M1 (h, `) 6=
M1 (h0 , `) then M2 (h, `) 6= M2 (h0 , `).
Note that R(M1 , M2 ) essentially says that if an attacker
can distinguish a pair of high security inputs by executing
M1 , then she could do the same by executing M2 . Hence,
R naturally expresses that M1 is at least as secure as M2 . 8
It may be somewhat surprising that this simple relationis actually equivalent to the rather complex entropy-based
quantitative information flow definitions when they are castas comparison problems and the distributions are universallyquantified, as stated in the following theorems. First, weshow that R coincides exactly with CSE with its distribution
universally quantified.
Theorem 4.2: R = {(M1 , M2 ) | ∀µ.CSE [µ](M1 , M2 )}The proof is detailed in Section IV-A. The next two theorems
show that R also coincides with CME and CGE with theirdistribution universally quantified.
Theorem 4.3: R = {(M1 , M2 ) | ∀µ.CME [µ](M1 , M2 )}Theorem 4.4: R = {(M1 , M2 ) | ∀µ.CGE [µ](M1 , M2 )}The first half of the ⊆ direction of the proofs of the theorems
above is much like the that of Theorem 4.2, that is, it makes
the observation that M2 disambiguates the high security
inputs at least as fine as does M1 . Then, the proof concludes
by utilizing the particular mathematical properties relevantto the respective definitions. The proof for the ⊇ directionis also similar to the argument used in Theorem 4.2. The
details of the proofs appear in Appendix B.
Next, we show that R refines CCC in the sense that if
R(M1 , M2 ) then CCC (M1 , M2 ). This follows immediately
8 We note that notions similar to R have appeared in literature (often insomewhat different representations) [27], [18], [6]. In particular, Clark et
al. [6] have shown a result analogous to the ⊆ direction of Theorem 4.2
below. But, R’s properties have not been fully investigated.

from Theorem 4.2 and the definition of the channel-capacity
based quantitative information flow.
Theorem 4.5: R ⊆ CCC
Note that, the other direction, R ⊇ CCC , does not holdas R is not always a total order, whereas CCC is. It isalso immediate from Theorem 4.2 and the property of noninterference (Theorem 2.6) that R is compatible with thenotion of non-interference in the following sense.
Theorem 4.6: Let M2 be a non-interferent program.
Then, R(M1 , M2 ) iff M1 is also non-interferent and M1
has the same input domain as M2 .
Next, we show that R is easier to decide than the nonuniversally-quantified versions of the comparison problems.
First, it is trivial to see from Definition 4.1 that R is a 2safety property.
Theorem 4.7: R is a 2-safety property.
It can be shown that, restricted to loop-free boolean
programs, R is coNP-complete. This follows directly fromthe observation that we can decide R by self composition
thanks to its 2-safety property and the fact that, for loop-freeboolean programs, self composition reduces the problem toan UNSAT instance.9
Theorem 4.8: Restricted to loop-free boolean programs,
R is coNP-complete.
A. Proof of Theorem 4.2
We discuss the details of the proof of Theorem 4.2. The
proofs of Theorems 4.3 and 4.4 are deferred to Appendix B.
First, we prove the following lemma which says that,
if R(M, M 0 ) then SE [U ](M 0 ) is at least as large as
SE [U ](M ) per each low security input ` ∈ L.
Lemma 4.9: Suppose R(M, M 0 ), that is, for all h1 , h2
in H and ` in L, M 0 (h1 , `) = M 0 (h2 , `) ⇒ M (h1 , `) =M (h2 , `). Let O be the set of the outputs of M , andO0 bePthe set of the outputs of P
M 0 . Then, for any `, we
µ(`)
µ(`)
0
have
o0 ∈O0 µ(o , `) log µ(o0 ,`) .
o∈O µ(o, `) log µ(o,`) ≤(Recall the notational convention from Definition A.1.)
Proof: First, we prove for any output o of M , there
exist corresponding outputs Oo = {o00 , o01 , . . . , o0n } of M 0such thatµ(`)µ(o, `) log µ(o,`)Pµ(`)≤ o0 ∈Oo µ(o0r , `) log µ(o
0 ,`)
r
r

Let Ho be the set such that Ho = {h | M (h, `) = o}.
Let {h0 , h1 , . . . , hn } = Ho . Let o00 = M 0 (h0 , `),. . . and,o0n = M 0 (hn , `). For any h0 such that o0r =M 0 (h0 , `) and o0r ∈ {o00 , o01 , . . . , o0n }, we have h0 ∈9 To construct a polynomial size boolean formula from a loop-freeboolean program, we use the well-known efficient weakest precondition
construction technique [13], [17] instead of the naive rules given in Figure 2.

0{h
P1 , . . . , hn } since0 R(M, M ). Then, we have µ(o, `) =
µ(o
,
`).
By
Lemma
A.5, we havero0r ∈{o0 ,...,o0n }1µ(`)µ(o, `) log µ(o,`)Pµ(`)≤ o0 ∈{o0 ,o0 ,...,o0 } µ(o0r , `) log µ(o
0 ,`)
r

0

1

n

r

Now to prove the lemma, it suffices to show that each Oo
constructed above are disjoint. That is, for o1 and o2 outputsof M such that o1 6= o2 , Oo1 ∩ Oo2 = ∅. For contradiction,
suppose o0 ∈ Oo1 ∩ Oo2 . Then, there exist h1 and h2 suchthat o1 = M (h1 , `), o0 = M 0 (h1 , `), o2 = M (h2 , `), ando0 = M 0 (h2 , `). Since R(M, M 0 ), we have o1 = o2 , and it
leads to a contradiction. Hence, we have
X
X
µ(`)
µ(`)
≤
µ(o0 , `) logµ(o, `) logµ(o, `)µ(o0 , `)0ooWe now prove Theorem 4.2.
Proof:• ⊆Suppose (M, M 0 ) ∈ R. By Lemma A.3,
SE [µ](M )= H[µ](O|L)
P P
µ(`)
=
`
o µ(o, `) log µ(o,`)

SE [µ](M 0 )= H[µ](O0 |L)
P P
µ(`)
0
=
`
o0 µ(o , `) log µ(o0 ,`)and

By Lemma 4.9 and the fact that (M, M 0 ) ∈ R, we
obtain for any `
X
X
µ(`)
µ(`)
≤
µ(o0 , `) logµ(o, `) log
0 , `)
µ(o,
`)
µ(o
0
o

Theorems 4.2, 4.3, 4.4, and 4.7 imply that we can check if
the entropy-based quantitative information flow of a program(i.e., SE, ME, and GE) is bounded by that of anotherfor all distributions via self composition [3], [11]. Thissuggests a novel approach to precisely checking quantitative
information flow.
That is, given a target program M1 , the user would
construct a specification program M2 with the same input
domain as M1 having the desired level of security. Then, shewould check R(M1 , M2 ) via self composition. If so, thenM1 is guaranteed to be at least as secure as M2 according to
the Shannon-entropy based, the min-entropy based, and theguessing-entropy based definition of quantitative information
flow for all distributions (and also channel-capacity based
definition), and otherwise, there must be a distribution inwhich M1 is less secure than M2 according to the entropybased definitions.
Note that deciding R(M1 , M2 ) is useful even when
M1 and M2 are R-incomparable, that is, when neither
R(M1 , M2 ) nor R(M2 , M1 ). This is because ¬R(M1 , M2 )implies that M1 is less secure than M2 on some distribution.
For example, suppose M1 is some complex login programwith the high security input H and the low security input
L. And we would like to verify that M1 is at least as secureas the prototypical login program M2 below.
M2 ≡ if H = L then O := 0 else O := 1µ(`)
o µ(o, `) log µ(o,`)
P Pµ(`)≤ ` o0 µ(o0 , `) log µ(o0 ,`)Then, using this framework, it suffices to just query if
R(M1 , M2 ) is true. (Note that the output domains of M1
and M2 need not to match.)
We now describe how to actually check R(M1 , M2 ) via
self composition. From M1 and M2 , we construct the selfcomposed program M 0 shown below.

P P•

B. Quantitative Information Flow via Self CompositionoHence,`

Therefore, SE [µ](M ) 6≤ SE [µ](M 0 ), that is,(M, M 0 ) 6∈ {(M1 , M2 ) | ∀µ.(M1 , M2 ) ∈ CSE [µ]}.

⊇We prove the contraposition. Suppose (M, M 0 ) 6∈
R. Then, there exist o0 , h0 , h1 , `0 such that o0 =M 0 (h0 , `0 ) = M 0 (h1 , `0 ) and M (h0 , `0 ) 6= M (h1 , `0 ).
Pick a probability function µ such that µ(h0 , `0 ) =µ(h1 , `0 ) = 21 .
Then, we haveP Pµ(`)
H[µ](O0 |L) =`o µ(o, `) log µ(o,`)
0µ(` )= µ(o0 , `0 ) log µ(o0 ,`0 )
1
= 1 log 1= 0

Let o0 and o1 be output variables such that o0 =M (h0 , `0 ), o1 = M (h1 , `0 ), and o0 6= o1 .
Pµ(`0 )
0
H[µ](O|L) =o∈{o0 ,o1 } µ(o, ` ) log µ(o,`0 )= 12 log 11 + 21 log 1122= 1

M 0 (H, H 0 , L) ≡O1 := M1 (H, L); O10 := M1 (H 0 , L);O2 := M2 (H, L); O20 := M2 (H 0 , L);assert(O1 6= O10 ⇒ O2 6= O20 )

// L1
// L2

Note that R(M1 , M2 ) is true iff M 0 does not cause an
assertion failure. The latter can be checked via a software
safety verifier such as SLAM and BLAST [2], [15], [24], [4].
As an aside, we note that this kind of construction could
be easily generalized to reduce any k-safety problem (cf.
Section III) to a safety problem, as shown by Clarkson andSchneider [9].
Note that the line L1 (resp. L2) of the pseudo code above
is M1 (resp. M2 ) sequentially composed with a copy ofitself, which is from where the name “self composition”

M1 ≡ O := H
M2 ≡ if H = L then O := 0 else O := H&1
M3 ≡ O := 1; i := 0;
while i < 32 {m := 1 << i;if H&m 6= L&m thenO := 0; break;
else
i++;
}
M4 ≡ O := 1; i := 0;
while i < 64 {m := 1 << i;if H&m 6= L&m thenO := 0; break;
else
i++;
}
Figure 3.

Example programs.

Here, H and L are 64-bit values, & is the bit-wise andoperator, and << is the left shift operator. M1 leaks the entire
password. M2 checks the password against the user guessbut then leaks the first bit when the check fails. M3 only
checks the first 32 bits of the password. And, M4 implements
password checking correctly via a while loop.
We verify that only M4 satisfies the specification, that is,R(M4 , Mspec ). To see that ¬R(M1 , Mspec ), note that forany `, h, h0 such that h 6= `, h0 6= ` and h 6= h0 , we have that
M1 (h, `) 6= M1 (h0 , `) but Mspec (h, `) = Mspec (h0 , `) = 1.
To see that ¬R(M2 , Mspec ), note that for `, h, h0 such thath 6= `, h0 6= `, h&1 = 1 and h0 &1 = 0, we havethat 1 = M2 (h, `) 6= M2 (h0 , `) = 0 but Mspec (h, `) =Mspec (h0 , `) = 1. To see that ¬R(M3 , Mspec ), let `, h, h0
be such that h|32 = `|32 , h0 |32 6= `|32 , and h 6= `,then, 1 = M3 (h, `) 6= M3 (h0 , `) = 0 but Mspec (h, `) =Mspec (h0 , `) = 1.10 (Here, x|32 denotes x mod 232 , i.e., thefirst 32 bits of x.)
The results imply that for M1 , M2 , and M3 , there must bea distribution where the program is less secure than Mspec
according to each of the entropy-based definition of quantitative information flow. For instance, for the Shannon-entropy
based definition, we have for the uniform distribution U ,64

comes. Therefore, technically, M 0 is a composition of two
self compositions.
L1 (and L2) are actually exactly the original self composition proposed for non-interference [3], [11]. Terauchi and
Aiken [30] noted that only the parts of M1 (and M2 ) that
depend on the high security inputs H and H 0 need to be
duplicated and self composed, with the rest of the program
left intact and “interleaved” with the self-composed parts.
The resulting program tends to be verified easier than thenaive self composition by modern software safety verifiers.
They proposed a set of transformation rules that translates
a WHILE program annotated with security types [33] (ordependency analysis results) to an interleaved self-composed
program. This was subsequently improved by a numberof researchers to support a richer set of language features
and transformation patterns [32], [25]. These transformation
methods can be used in place of the naive self compositionsat L1 and L2 in building M 0 . That is, we apply a security
type inference (or a dependency analysis) to M1 and M2 toinfer program parts that depend on the high security inputs
H and H 0 so as to only duplicate and self compose thoseparts of M1 and M2 .

64

2SE [U ](Mspec ) = 2158 + 2 264−1 log 264−1−18≈ 3.46944695 × 10
SE [U ](M1 ) = 6463
264
263 −1264
SE [U ](M2 ) = 21 + 1+2
265 log 1+263 + 265 log 263 −1
≈ 1.0
64
32
64
SE [U ](M3 ) = 2127 + 2 2−2
log 2642−232
64≈ 7.78648 × 10−9

That is, SE [U ](M1 ) 6≤ SE [U ](Mspec ), SE [U ](M2 ) 6≤
SE [U ](Mspec ), and SE [U ](M3 ) 6≤ SE [U ](Mspec ).
Finally, we have that R(M4 , Mspec ), and so M4 is at least
as secure as Mspec according to all of the definitions ofquantitative information flow considered in this paper. In
fact, it can be also shown that R(Mspec , M4 ). (However,note that M4 and Mspec are not semantically equivalent,i.e., their outputs are reversed.)
V. R ELATED W ORK

Mspec ≡ if H = L then O := 0 else O := 1This work builds on previous work that proposed information theoretic notions of quantitative information flow [12],[7], [19], [29], [16], [1], [22], [20], [26]. The previous
research has mostly focused on information theoretic properties of the definitions and proposed approximate (i.e., incomplete and/or unsound) methods for checking and inferring
them. In contrast, this paper investigates the verification
theoretic and complexity theoretic hardness of precisely
inferring quantitative information flow according to the

We check the four programs shown in Figure 3 using theabove as the specification.

10 It can be also shown that ¬R(Mspec , M2 ) and ¬R(Mspec , M3 ), thatis, M2 and M3 are R-incomparable with Mspec .

C. Example
We recall the ideal login program below.

definitions and also proposes a precise method for checking quantitative information flow. Our method checks thequantitative information flow of a program against that ofa specification program having the desired level of security
via self composition for all distributions according to theentropy-based definitions.
It is quite interesting that the relation R unifies thedifferent proposals for the definition of quantitative information flow when they are cast as comparison problems andtheir distributions are universally quantified. As remarked in
Section IV, R naturally expresses the fact that one programis more secure than the other, and it could be argued that itis the essence of quantitative information flow.
Researchers have also proposed definitions of quantitative
information flow that are not detailed in the main bodyof the paper. These includes the definition based on thenotion of belief [8], and the ones that take the maximum
over the low security inputs [19], [16]. It can be shownthat R refines the comparison problems for these notionsin the same sense as in Theorem 4.5 (for the belief-based
definition, we universally quantify over the beliefs and theexperiments). In fact, it can be shown that, for the beliefbased definition, the equivalence result holds much like thosefor the entropy-based definitions.11
Despite the staggering complexity made apparent in thispaper, recent attempts have been made to (more) precisely
infer quantitative information flow (without universallyquantifying over the distribution as in our approach). Thesemethods are based on the idea of counting. As remarked in
Section III-C, quantitative information flow is closely related
to counting problems, and several attempts have been madeto reduce quantitative information flow problems to them.12
For instance, Newsome et al. [26] reduce the inference
problem to the #SAT problem and apply off-the-shelf #SAT
solvers. To achieve scalability, they sacrifice both soundness
and completeness by only computing information flow fromone execution path. Backes et al. [1] also propose a countingbased approach that involves self composition. However,unlike our method, they use self composition repeatedly tofind a new solution (i.e., more than a bounded number oftimes), and so their results do not contradict the negative
results of this paper.

the Shannon entropy, the min entropy, the guessing entropy,
and channel capacity.
We have shown that comparing two programs on which
has the larger flow according to these definitions is nota k-safety problem for any k, and therefore that it is
not possible to reduce the problem to a safety problem
via self composition. The result is in contrast to noninterference which is a 2-safety problem. We have also
shown a complexity theoretic gap with non-interference by
proving the #P-hardness of the comparison problems andcoNP-completeness of non-interference, when restricted toloop-free boolean programs.
We have also shown a positive result that checking if theentropy-based quantitative information flow of one programis larger than that of another for all distributions is a 2-safety
problem, and that it is also coNP-complete when restricted
to loop-free boolean programs.
We have done this by proving a surprising result that
universally quantifying the distribution in the comparison
problem for the entropy-based definitions is equivalent toa simple 2-safety relation. Motivated by the result, we haveproposed a novel approach to precisely checking quantitative
information flow that reduces the problem to a safety problem via self composition. Our method checks the quantitative
information flow of a program for all distributions againstthat of a specification program having the desired level of
security.
ACKNOWLEDGMENT
We would like to thank Takeshi Tsukada for important
insights and useful discussions that motivated this work.
We also thank the anonymous reviewers for their usefulcomments. This work was supported by MEXT KAKENHI 20700019 and 20240001, and Global COE Program“CERIES.”R EFERENCES[1] M. Backes, B. Köpf, and A. Rybalchenko. Automatic
discovery and quantification of information leaks. In IEEE
Symposium on Security and Privacy, pages 141–153. IEEE
Computer Society, 2009.

VI. C ONCLUSION[2] T. Ball and S. K. Rajamani. The SLAM project: debugging
system software via static analysis. In POPL, pages 1–3,
2002.

We have investigated the hardness and possibilities of precisely checking and inferring quantitative information flow
according to the various definitions proposed in literature.
Specifically, we have considered the definitions based on[3] G. Barthe, P. R. D’Argenio, and T. Rezk. Secure information
flow by self-composition. In CSFW, pages 100–114. IEEE
Computer Society, 2004.

11 The other direction does not hold for the maximum-over-low-security-

inputs definitions.
12 Note that our results only show that, restricted to loop-free boolean
programs, the comparison problems can be reduced from #SAT, and they
do not show how to reduce them (or more general cases) to #SAT or othercounting problems.

[4] D. Beyer, T. A. Henzinger, R. Jhala, and R. Majumdar. The
software model checker Blast. STTT, 9(5-6):505–525, 2007.
[5] D. Clark, S. Hunt, and P. Malacaria. Quantified interference
for a while language. Electr. Notes Theor. Comput. Sci.,
112:149–166, 2005.

[6] D. Clark, S. Hunt, and P. Malacaria. Quantitative information
flow, relations and polymorphic types. J. Log. Comput.,
15(2):181–199, 2005.

[22] S. McCamant and M. D. Ernst. Quantitative information flow
as network flow capacity. In R. Gupta and S. P. Amarasinghe,
editors, PLDI, pages 193–205. ACM, 2008.

[7] D. Clark, S. Hunt, and P. Malacaria. A static analysis forquantifying information flow in a simple imperative language.
Journal of Computer Security, 15(3):321–371, 2007.

[23] J. McLean. A general theory of composition for trace
sets closed under selective interleaving functions. In SP’94: Proceedings of the 1994 IEEE Symposium on Security
and Privacy, page 79, Washington, DC, USA, 1994. IEEE
Computer Society.

[8] M. R. Clarkson, A. C. Myers, and F. B. Schneider. Belief
in information flow. In CSFW, pages 31–45. IEEE Computer
Society, 2005.
[9] M. R. Clarkson and F. B. Schneider. Hyperproperties. In
CSF, pages 51–65. IEEE Computer Society, 2008.
[10] E. S. Cohen. Information transmission in computational
systems. In SOSP, pages 133–139, 1977.
[11] Á. Darvas, R. Hähnle, and D. Sands. A theorem proving
approach to analysis of secure information flow. In D. Hutter
and M. Ullmann, editors, SPC, volume 3450 of Lecture Notes
in Computer Science, pages 193–209. Springer, 2005.
[12] D. E. R. Denning. Cryptography and data security. AddisonWesley Longman Publishing Co., Inc., Boston, MA, USA,1982.
[13] C. Flanagan and J. B. Saxe. Avoiding exponential explosion:
generating compact verification conditions. In POPL, pages
193–205, 2001.

[24] K. L. McMillan. Lazy abstraction with interpolants. In T. Balland R. B. Jones, editors, CAV, volume 4144 of Lecture Notes
in Computer Science, pages 123–136. Springer, 2006.
[25] D. A. Naumann. From coupling relations to mated invariants
for checking information flow. In Computer Security ESORICS 2006, 11th European Symposium on Research in
Computer Security, Proceedings, pages 279–296, Hamburg,
Germany, Sept. 2006.
[26] J. Newsome, S. McCamant, and D. Song. Measuring channel
capacity to distinguish undue influence. In S. Chong and
D. A. Naumann, editors, PLAS, pages 73–85. ACM, 2009.
[27] A. Sabelfeld and A. C. Myers. A model for delimited
information release. In K. Futatsugi, F. Mizoguchi, andN. Yonezaki, editors, ISSS, volume 3233 of Lecture Notes
in Computer Science, pages 174–191. Springer, 2003.
[28] C. Shannon. A mathematical theory of communication. Bell
System Technical Journal, 27:379–423, 623–656, 1948.

[14] J. A. Goguen and J. Meseguer. Security policies and security
models. In IEEE Symposium on Security and Privacy, pages
11–20, 1982.

[29] G. Smith. On the foundations of quantitative information flow.
In L. de Alfaro, editor, FOSSACS, volume 5504 of Lecture
Notes in Computer Science, pages 288–302. Springer, 2009.

[15] T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazyabstraction. In POPL, pages 58–70, 2002.

[30] T. Terauchi and A. Aiken. Secure information flow as a safety
problem. In C. Hankin and I. Siveroni, editors, SAS, volume3672 of Lecture Notes in Computer Science, pages 352–367.
Springer, 2005.

[16] B. Köpf and D. A. Basin. An information-theoretic model
for adaptive side-channel attacks. In P. Ning, S. D. C.
di Vimercati, and P. F. Syverson, editors, ACM Conference
on Computer and Communications Security, pages 286–296.
ACM, 2007.
[17] K. R. M. Leino. Efficient weakest preconditions. Inf. Process.
Lett., 93(6):281–288, 2005.
[18] P. Li and S. Zdancewic. Downgrading policies and relaxednoninterference. In J. Palsberg and M. Abadi, editors, POPL,
pages 158–170. ACM, 2005.
[19] P. Malacaria. Assessing security threats of looping constructs.
In M. Hofmann and M. Felleisen, editors, POPL, pages 225–235. ACM, 2007.
[20] P. Malacaria and H. Chen. Lagrange multipliers and maximum information leakage in different observational models.
In Ú. Erlingsson and M. Pistoia, editors, PLAS, pages 135–
146. ACM, 2008.
[21] J. L. Massey. Guessing and entropy. In ISIT ’94: Proceedingsof the 1994 IEEE International Symposium on Information
Theory, page 204, 1994.

[31] S. Toda. PP is as hard as the polynomial-time hierarchy. SIAM
J. Comput., 20(5):865–877, 1991.
[32] H. Unno, N. Kobayashi, and A. Yonezawa. Combining
type-based analysis and model checking for finding counterexamples against non-interference. In V. C. Sreedhar and
S. Zdancewic, editors, PLAS, pages 17–26. ACM, 2006.
[33] D. Volpano, G. Smith, and C. Irvine. A sound type system forsecure flow analysis. Journal of Computer Security, 4(3):167–
187, 1996.

A PPENDIX A.
S UPPORTING D EFINITIONS AND L EMMASWe define some abbreviations.
Definition A.1: µ(x) , µ(X = x)
We use this notation whenever the correspondences between
random variables and their values are clear.
For convenience, we sometimes use large letters H, L,
O, etc. to range over boolean variables as well as genericrandom variables.

For simplicity, we often compute the Shannon-entropy
based quantitative information flow for programs that do nothave low security inputs. For such programs, the equation
SE from Definition 2.4 can be simplified as follows.
Lemma A.2:
SE [µ](M )= I[µ](O; H)= H[µ](O)We note the following property of deterministic programs [5].
Lemma A.3: For M deterministic,
SE [µ](M ) = I[µ](O; H|L) = H[µ](O|L)
The following lemma is used to show that we can generatea boolean formula that has exactly the desired number ofsolutions in polynomial (actually, linear) time.
Lemma A.4: Let k be an integer such that 0 ≤ k ≤→−2| x | − 1. Then, a boolean formula that has exactly k→
assignments over the variables −x can be computed in time→−
linear in | x |.
Proof: We define a procedure iter that returns the→boolean formula. Below, −x = x1 , x2 , . . . , i.e., xi is theith variable.
iter(, 0) = false
iter(0`, i) = xi ∧ (iter(`, i − 1))iter(1`, i) = xi ∨ (iter(`, i − 1))→
Here,  is an empty string. Let `k be a |−x |-bit binary→−
representation of k. We prove that iter(` , | x |) returns akboolean formula that has exactly k assignments by induction→
on the number of variables, that is, |−x |.
→−• |x|= 1– k=0iter(0, 1) returns x1 ∧ false, that is, false. false has
no satisfying assignment.
– k=1
iter(1, 1) returns x1 ∨ false, that is, x1 . x1 has only
one satisfying assignment.
→ 0−• |x,x |→− 0– k < 2| x ,x |−1
Let 0` be a binary representation of k.
→→iter(0`, |−x , x0 |) returns x0 ∧ iter(`, |−x |). By→−
induction hypothesis, iter(`, | x |) has k satisfying→→
assignments for −x . It follows that x0 ∧ iter(`, |−x |)has just k satisfying assignments, because→
false ∧ iter(`, |−x |) has no assignment and→−true ∧ iter(`, | x |) has just k assignments.
→−– k ≥ 2| x |Let 1` be a binary representation of k.
→−iter(1`, |−x , x0 |) returns x0 ∨ iter(`, |→x |). ` is−|→x|
a binary representation of k − 2 . By induction→−→
hypothesis, iter(`, |−x |) has k − 2| x | satisfying→→
assignments for −x . It follows that x0 ∨ iter(`, |−x |)has just k satisfying assignments, because→−→
false ∨ iter(`, |−x |) has just k − 2| x | assignments→−→−
and when x0 = true, x0 ∨ iter(`, | x |) has just 2| x |assignments.
We frequent the following property of logarithmic arithmetic when proving statements concerning the Shannon
entropy.
Lemma A.5: Let p and q be numbers such that p, q ∈1.
[0, 1]. Then, we have p log p1 + q log 1q ≥ (p + q) log p+qp+q
Proof: Because p+q
p ≥ 1 and q ≥ 1, it follows that,1p log p1 + q log 1q − (p + q) log p+q
1
1
1= p log p − p log p+q + q log 1q − q log p+q
p+q= p log p+q
p + q log q≥0

A PPENDIX B.
O MITTED P ROOFS
Theorem 2.6: Let M be a program that takes highsecurity input H, low-security input L, and returns lowsecurity output O. Then, M is non-interferent if and only if∀µ.SE [µ](M ) = 0.
Proof: Recall that M is non-interferent iff for any
h, h0 ∈ H and ` ∈ L, M (h, `) = M (h0 , `).
• (⇒) Suppose that M is non-interferent. Then, by
Lemma A.3,
SE [µ](M )= I[µ](O; H|L)
= H[µ](O|L)
P Pµ(`)µ(o, `) log µ(o,`)
=
Po P`
µ(`)
=
o
` µ(o, `) log µ(`)= 0

The last step follows from the fact that non-interference
implies µ(`) = µ(o, `).
• (⇐) Suppose that M is interferent. Then, there must be
h0 and h1 such that M (h0 , `0 ) = o0 , M (h1 , `0 ) = o1 ,and o0 6= o1 . Pick a probability function µ such thatµ(h0 , `0 ) = µ(h1 , `0 ) = 21 . Then, by Lemma A.3,
SE [µ](M )= I[µ](O; H|L)
= H[µ](O|L)
P P
µ(`)
=
o
` µ(o, `) log µ(o,`)
0µ(` )= µ(o0 , `0 ) log µ(o00 ,` )0µ(` )+µ(o1 , `0 ) log µ(o01 ,` )= 21 log 2 + 12 log 2= 1

Therefore, there exists µ such that SE [µ](M ) 6= 0, andwe have the conclusion.

We note the following equivalence of CC and ME[U] forprograms without low security inputs [29].
Lemma B.1: Let M be a program without low security
input. Then, ME [U ](M ) = CC (M ).
The min-entropy-based quantitative information flow withuniformly distributed high security input has the following
property [29].
Lemma B.2: Let M be a program without low security
input and O be the output of M . Then, ME [U ](M ) =log(|O|).

Lemma B.5: Let µ be a function such that µ : D →[0, 1]. Let P and Q be sets such
P that P ∪ Q = D and
P
∩
Q
=
∅.
Then,
we
have
x∈D In(µ, D, x)µ(x) ≥
P
P
In(µ,
P,
p)µ(p)+In(µ,Q, q)µ(q).
p∈Pq∈Q
Proof: Trivial.
Definition B.6: Let M be a function such that M : A →B. For any o ∈ B, we define M −1 (o) to mean
M −1 (o) = {i ∈ A | o = M (i)}Theorem 3.2: CME [U ] is not a k-safety property for any
k > 0.
Proof: For contradiction, suppose CME [U ] is a k-safety
property. Let M and M 0 be programs having same input
domain such that (M, M 0 ) 6∈ CME [U ]. Then, it must be thecase that there exist T ⊆ [[M ]] and T 0 ⊆ [[M 0 ]] such that
|T | ≤ k, |T 0 | ≤ k, and ∀Mc , Mc0 .T ⊆ [[Mc ]]∧T 0 ⊆ [[Mc0 ]] ⇒(Mc , Mc0 ) 6∈ CME [U ].
Let
T = {(h1 , o1 ), (h2 , o2 ), . . . , (hi , oi )}T 0 = {(h01 , o01 ), (h02 , o02 ), . . . , (h0j , o0j )}where i, j ≤ k. Now, we construct new programs M̄ andM̄ 0 as follows.
M̄ (h1 ) = o1M̄ (h2 ) = o2...
M̄ (hi ) = oiM̄ (hi+1 ) = oM̄ (hi+2 ) = o...
M̄ (hn ) = o

M̄ 0 (h01 ) = o01
M̄ 0 (h02 ) = o02...
M̄ 0 (h0j ) = o0j
M̄ 0 (h0j+1 ) = o0j+1
M̄ 0 (h0j+2 ) = o0j+2...
M̄ 0 (h0n ) = o0n

Theorem 3.3: CGE [U ] is not a k-safety property for any
k>0
Proof: For contradiction, suppose CGE [U ] is a k-safety
property. Let M and M 0 be programs having the same input
domain such that (M, M 0 ) 6∈ CGE [U ]. Then, it must be thecase that there exist T ⊆ [[M ]] and T 0 ⊆ [[M 0 ]] such that
|T | ≤ k, |T 0 | ≤ k, and ∀Mc , Mc0 .T ⊆ [[Mc ]]∧T 0 ⊆ [[Mc0 ]] ⇒(Mc , Mc0 ) 6∈ CGE [U ].
Let
T = {(h1 , o1 ), (h2 , o2 ), . . . , (hi , oi )}T 0 = {(h01 , o01 ), (h02 , o02 ), . . . , (h0j , o0j )}where i, j ≤ k. Now, we construct new programs M̄ andM̄ 0 as follows.
M̄ (h1 ) = o1M̄ (h2 ) = o2...
M̄ (hi ) = oiM̄ (hi+1 ) = oM̄ (hi+2 ) = o...
M̄ (hi+j ) = oM̄ (hi+j+1 ) = or...
M̄ (hn ) = or

where
0
0
0
• oj+1 , oj+2 , . . . , and on are distinct,
0
0
0
0
0
• {o1 , o2 , . . . , oj } ∩ {oj+1 , . . . , on } = ∅,00
• {h1 , . . . , hn } = {h1 , . . . , hn }, and• n = 2k.
The number of outputs of the program M̄ 0 is greater thanor equal to the number of the outputs of the program M̄ .
Hence, by Lemma B.2, we have (M̄ , M̄ 0 ) ∈ CME [U ]. But,
T ⊆ [[M̄ ]] and T 0 ⊆ [[M̄ 0 ]]. This leads to a contradiction.
Definition B.3:

M̄ 0 (h01 ) = o01
M̄ 0 (h02 ) = o02...
M̄ 0 (h0j ) = o0j
M̄ 0 (h0j+1 ) = o0j+1
M̄ 0 (h0j+2 ) = o0j+2...
M̄ 0 (h0j+i ) = o0j+i
M̄ 0 (h0j+i+1 ) = o0r...
M̄ 0 (h0n ) = o0r

In(µ, X, x) = |{x0 ∈ X | µ(x0 ) ≥ µ(x)}|Intuitively, In(µ, X, x) is the order of x defined in terms ofµ.
Lemma B.4:
G[µ](X)
Proof: Trivial.

= Σ1≤i≤|X| iµ(xi )= Σx∈X In(µ, X, x)µ(x)where
o 6= or ,{o1 , o2 , . . . , oi } ∩ {o, or } = ∅,0000
• oj+1 , oj+2 , . . . , oj+i , and or are distinct,
0
0
0
0
0
0
• {o1 , o2 , . . . , oj } ∩ {oj+1 , . . . , oj+i , or } = ∅,00
• {h1 , . . . , hn } = {h1 , . . . , hn }, and• n = 2k.
••

T (φ) =
if φ
→
−
→
−
then Of := true; O := H−−→→−else Of := false; O := false→−
where Of and O are distinct.
Figure 4.

Boolean formula encoding by boolean program

We compare the guessing-entropy-based quantitative information flow of the two programs.
GE [U ](M̄ 0 ) − GE [U ](M̄ )P
10−1 0 2(o )|= |H|o0 ∈M 0 (H) |M
2 − 2|H|
P
|H|
1
−1
2
− 2 + 2|H||M(o)|o∈M (H)P
1−1
2= 2|H| o∈M (H) |M (o)|P10−1 0 2
− 2|H|(o )|o0 ∈M 0 (H) |M
P
1−1= 2|H| ( ox ∈{o1 ,...,oi } |M (ox )|2
−1
2
−1
+|M
(or )|2 )P (o)| + |M 0−1
1− 2|H| ( o0 ∈{o0 ,...,o0 } |M (o0x )|2
j
Px 1+ o0 ∈{o0 ,...,o0 } |M 0−1 (o0y )|2
y
j+1
j+i
+|M 0−1 (o0r )|2 )By lemma B.5, we haveP
|M −1 (ox )|2ox ∈{oP
1 ,...,oi }≤ o0y ∈{o0 ,...,o0 } |M 0−1 (o0x )|2
j+1
j+i
and
P
|M −1 (o)|2 ≤ o0 ∈{o0 ,...,o0 } |M 0−1 (o0x )|2
x1

j

Trivially, we have→−
whether programs are in CME [U ] at most 3 × (| H | + 1) + 2
times.
Proof: First, we define a procedure that returns thenumber of solutions for φ.
→−
Let B(j) = ψ ∧ H 0 where ψ is a formula over H having0
j assignments and H is a boolean variable such that H 0 6∈→−
{ H }. Note that by Lemma A.4, such ψ can be generated inlinear time.
Then, we invoke the following procedure where T is
defined in Figure 4.
` = 0;→−
r = 2| H | ;n = (` + r)/2;
while ¬((T (φ ∧ H 0 ), T (B(n))) ∈ CME [U ]and (T (B(n)), T (φ ∧ H 0 )) ∈ CME [U ])if (T (φ ∧ H 0 ), T (B(n))) ∈ CME [U ]then {` = n; n = (` + r)/2; }else {r = n; n = (` + r)/2; }return n
Note that when the procedure terminates, we have
ME [U ](T (B(n)) = ME [U ](T (φ ∧ H 0 )), and so by
Lemma B.2 and Lemma B.7, n is the number of satisfying
assignments to φ.
→−
We show that the procedure iterates at most | H |+1 times.
To see this, note that every iteration in the procedure narrows
the range betweenr and ` by one half. Because r − ` is→−|H |bounded by 2 , it follows that the procedure iterates at→−most | H | + 1 times. Hence, the oracle CME [U ] is accessed→−
3 × (| H | + 1) + 2 times, and this proves the lemma.

|M 0−1 (o0r )|2 = |M −1 (or )|2
As a result, we have
GE [U ](M̄ 0 ) − GE [U ](M̄ ) ≥ 0
Recall that M̄ and M̄ 0 have the same counterexamples T
and T 0 , that is, T ⊆ [[M̄ ]] and T 0 ⊆ [[M̄ 0 ]]. However, wehave (M̄ , M̄ 0 ) ∈ CGE [U ]. This leads to a contradiction.
Theorem 3.4: CCC is not a k-safety property for any
k > 0.
Proof: Straightforward from Lemma B.1 and Theorem 3.2.
→−
Lemma B.7: Let H be distinct boolean variables, φ be a→−boolean formula over H , and n be thenumber of satisfying→−
assignments for φ. If n is less than 2| H | , then the number ofthe outputs of the boolean program T (φ) defined in Figure 4
is equal to n + 1.
Proof: Trivial.
→−
Lemma B.8: Let H be distinct variables and φ be a→−boolean formula over H . Then, the number of assignmentsfor φ can be computed by executing an oracle that decides

Theorem 3.6: #P ⊆ FPCME [U ]Proof: Straightforward by Lemma B.8 and the fact that
#SAT, the problem of counting the number of solutions to aboolean formula, is #P-complete.
→−
Lemma B.9: Let H and H 0 be distinct variables and φ→−
and φ0 be boolean formulas over H . Let M ≡ O := φ ∧ H 0
and M 0 ≡ O := φ0 ∧ H 0 . Then, we have #SAT (φ) ≤#SAT (φ0 ) iff GE [U ](M ) ≤ GE [U ](M 0 ).
Proof: By the definition,
GE [U ](M )= G(H) − G(H|O)
P P→−− iU (hi , o)
= 21 (| H |) + 12 − o 1≤i≤|→
H|
=

→
−
|H |
2

−

1
−1
(true)|2 + |M −1 (false)|2 )→− (|M2| H |

Therefore,
GE [U ](M ) ≤ GE [U ](M 0 )iff|M −1 (true)|2 + |M −1 (false)|2≥ |M 0−1 (true)|2 + |M 0−1 (false)|2But, trivially, the latter holds iff#SAT (φ) ≤ #SAT (φ0 )→−Lemma B.10: Let H and H 0 be distinct variables and→−φ be a boolean formula over H . Then, the number ofassignments for φ can be computed by executing an oracle
that decides whether programs are in CGE [U ] at most→−
3 × (| H | + 1) + 2 times.
Proof: First, we define a procedure that returns thenumber of solutions for φ.
→−
Let B(j) = ψ ∧ H 0 where ψ is a formula over H having
j assignments and H 0 is a boolean variable such that H 0 6∈−→
{ H }. Note that by Lemma A.4, such ψ can be generated inlinear time.
` = 0;→−
r = 2| H | ;n = (` + r)/2;
while ¬(O := φ ∧ H 0 , O := B(n)) ∈ CGE [U ]and (O := B(n), O := φ ∧ H 0 ) ∈ CGE [U ])if (O := φ ∧ H 0 , O := B(n)) ∈ CGE [U ]then {` = n; n = (` + r)/2; }else {r = n; n = (` + r)/2; }return n
Note that when this procedure terminates, we have
GE [U ](O := B(n)) = GE [U ](O := φ ∧ H 0 ), and so by
Lemma B.9, n is the number of satisfying assignments toφ.
→−We show that the procedure iterates at most | H |+1 times.
To see this, every iteration in the procedure narrows therange→
between r and ` by one half. Because r −` is bounded−→−by 2| H | , it follows that the procedure iterates at most | H |+1→−
times. Hence, the oracle CGE [U ] is accessed 3×(| H |+1)+2
times, and this proves the lemma.
Theorem 3.7: #P ⊆ FPCGE [U ]Proof: Straightforward by Lemma B.10 and the factthat #SAT, the problem of counting the number of solutions
to a boolean formula, is #P-complete.
Theorem 3.8: #P ⊆ FPCCC
Proof: Straightforward from Lemma B.1 and Theorem 3.6.
Theorem 3.9: Checking non-interferencecomplete for loop-free boolean programs.

is

coNP-

Proof: We write NI for the decision problem of checking non-interference of loop-free boolean programs. We
prove by reducing NI to and from UNSAT, which is coNPcomplete.
• NI ⊆ UNSAT

We reduce via self composition [3], [11]. Let M bea boolean program that we want to know if it is noninterferent. First, we make a copy of M , with eachvariable x in M replaced by a fresh (primed) variable→ −−→x0 . Call this copy M 0 . Let φ = wp(M ; M 0 , O = O 0 ),→−→0−where O = O is the boolean formula encoding the
conjunction of equalities O1 = O10 , O2 = O20 , . . . ,On = On0 , where O1 , . . . , On are the low security
output variables of M . Note that φ can be obtainedin time polynomial in the size of M . Here, instead of
the rules in Figure 2, we use the optimized weakest
precondition generation technique [13], [17] that generates a formula quadratic in the size of M ; M 0 . Then,
M is non-interferent if and only if φ is valid, that is,
if and only if ¬φ is unsatisfiable.
• UNSAT ⊆ NI
Let φ be a formula that we want to know if it isunsatisfiable. We prove that the following programs is
non-interferent iff φ is unsatisfiable. Here, all variables
that appear in φ are high security input variables and
H is a high security input variable that is distinct fromvariables appearing in φ, and O is the low security
output variable.
if φ ∧ H then O := true else O := false
Trivially, if φ is unsatisfiable, then this program returns
only false, that is, this program is non-interferent. If thisprogram is non-interferent, then this program returns
only true for any input, or returns only false for any
input. However, this program can not return only true,
because if H = false then φ ∧ H = false. Therefore,
this program only returns false, when this program is
non-interferent. That means φ is unsatisfiable when the
program is non-interferent.
Definition B.11: Let M be a function such that M : A →B. Then, we define the image of M on X ⊆ A, M [X], asfollows.
M [X] = {o | o = M (x) ∧ x ∈ X}
Lemma B.12: Let H be a set, and M and M 0 be
functions whose domains contain H. Suppose that wehave M 0 (h0 , l) = M 0 (h1 , l) ⇒ M (h0 , l) = M (h1 , l),for all h0 , h1 in H. Then, for all h0 ∈ H, we have{h | M 0 (h, l) = M 0 (h0 , l)} ⊆ {h | M (h, l) = M (h0 , l)}.
Proof: Trivial.
Lemma B.13: Let H, O, O0 , and L be distinct random variables. Let M and M 0 be programs. We have(M, M 0 ) ∈ R iff for any distribution µ, H∞ [µ](H|O0 , L) ≤H∞ [µ](H|O, L) where O0 = M 0 (H, L) and O = M (H, L).
Proof:•(⇒)

Suppose R(M, M 0 ). We have
H∞ [µ](H|O0 , L) ≤ H∞ [µ](H|O, L)
iff V[µ](H|O, L) ≤ V[µ](H|O0 , L)by the definition of min entropy, andV[µ](H|O,L)P= o∈O,`∈L µ(o, `) maxh∈H µ(h|o, `)P= o∈O,`∈L µ(o, `) maxh∈H µ(h,o,`)µ(o,`)P= o∈O,`∈L maxh∈H µ(o, `) µ(h,o,`)µ(o,`)P= o∈O,`∈L maxh∈H µ(h, o, `)P= o∈O,`∈L maxh∈{h0 |o=M (h0 ,`)} µ(h, `)Theorem 4.3: R = {(M1 , M2 ) | ∀µ.CME [µ](M1 , M2 )}Proof: Straightforward from Lemma B.13 and the factthat H∞ [µ](H|L) − H∞ [µ](H|O, L) ≤ H∞ [µ](H|L) −H∞ [µ](H|O0 , L) iff H∞ [µ](H|O, L) ≥ H∞ [µ](H|O0 , L).
Theorem 4.4: R = {(M1 , M2 ) | ∀µ.CGE [µ](M1 , M2 )}•GE
P [µ](M ) = 0
0`∈L,h∈H In(λh .µ(h , `), H, h)µ(h, `)P− o∈O,`∈L,h∈H In(λh0 .µ(h0 , o, `), H, h)µ(h, o, `)where O = M [{(h, `) ∈ H × L | µ(h, l) > 0}], and L
and H are sample spaces of low-security input andhigh-security input, respectively. Therefore, it suffices
to show that

and
0
GE
P [µ](M ) = 0
0`∈L,h∈H In(λh .µ(h , `), H, h)µ(h, `)P− o0 ∈O0 ,`∈L,h∈H In(λh0 .µ(h0 , o0 , `), H, h)µ(h, o0 , `)0V[µ](H|O
P , L) − V[µ](H|O, L)= o0 ∈O0 ,`∈L maxh∈{h0 |o0 =M 0 (h0 ,`)} µ(h, `)P− o∈O,`∈L maxh∈{h0 |o=M (h0 ,`)} µ(h, `)≥0where O = M [{(h, `) ∈ H × L | µ(h, `) > 0}] andO0 = M 0 [{(h, `) ∈ H × L | µ(h, `) > 0}].
It suffices to show thatP
In(λh0 .µ(h0 , o0 , `), H, h)µ(h, o0 , `)o0 ∈OP0 ,`∈L,h∈H≤ o∈O,`∈L,h∈H In(λh0 .µ(h0 , o, `), H, h)µ(h, o, `)where O0 = M 0 [{(h, `) ∈ H × L | µ(h, `) > 0}].
For any o ∈ O and ` ∈ L, there exists hm suchthat µ(hm , `) = maxh∈{h0 |o=M (h0 ,`)} µ(h, `). Because
R(M, M 0 ), by Lemma B.12, we have{h | M 0 (h, `) = M 0 (hm , `)}⊆ {h | M (h, `) = M (hm , `)}Let o ∈ O and ` ∈ L. Let o = M (h0 , `) = · · · =M (hx , `), and let o00 = M 0 (h0 , `), . . . , o0x = M 0 (hx , `).
Because R(M, M 0 ), for any h0 such that M 0 (h0 , `) ∈{o00 , . . . , o0x }, we have h0 ∈ {h0 , . . . , hx }. Then, by
Lemma B.5, we haveP
In(λh0 .µ(h0 , o0 , `), H, h)µ(h, o, `)h∈HOP≥ o0 ∈O0 o ,h∈Ho In(λh0 .µ(h0 , o0 , `), H, h)µ(h, o0 , `)Therefore,µ(hm , `) =max

h∈{h0 |o0 =M 0 (h0 ,`)}µ(h, `)

for some o0 ∈ O0 . Hence, each summand inPmaxh∈{h0 |o=M (h0 ,`)} µ(h, `) also appearso∈O,`∈LP
in o0 ∈O0 ,`∈L maxh∈{h0 |o0 =M 0 (h0 ,`)} µ(h, `). And, we
have the above proposition.
• (⇐)
We prove the contraposition. Suppose (M, M 0 ) 6∈ R.
Then, there exist h0 , h1 , `, o0 , o1 such that M 0 (h0 , `) =M 0 (h1 , `), o0 = M (h0 , `), o1 = M (h1 , `), ando0 6= o1 . Pick a probability distribution µ such thatµ(h0 , `) = µ(h1 , `) = 21 . Then, we have

where

O0 o
Ho

= {o00 , . . . , o0x }= {h0 , h1 , . . . , hx }Now we prove each Oo constructed above are disjoint.
That is, for o1 and o2 outputs of M such that o1 6=
o2 , Oo1 ∩ Oo2 = ∅. For a contradiction, suppose o0 ∈Oo1 ∩ Oo2 . Then, there exist h1 and h2 such that o1 =M (h1 , `), o0 = M 0 (h1 , `), o2 = M (h2 , `), and o0 =M 0 (h2 , `). Since R(M, M 0 ), we have o1 = o2 , and it
leads to a contradiction. Hence, we have for any ` ∈ L,
P
In(λh0 .µ(h0 , o0 , `), H, h)µ(h, o0 , `)o0 ∈OP0 ,h∈H≤ o∈O,h∈H In(λh0 .µ(h0 , o, `), H, h)µ(h, o, `)0
V[µ](H|O
P , L)= o0 ∈O0 ,`∈L maxh∈{h0 |o0 =M (h0 ,`)} µ(h, `)
= 21

and
V[µ](H|O,L)P= o∈O,`∈L maxh∈{h0 |o=M (h0 ,`)} µ(h, `)= 21 + 12=1
Therefore, H∞ [µ](H|O0 , L) 6≤ H∞ [µ](H|O, L).

Proof:⊆
Suppose (M, M 0 ) ∈ R. By the definition,

Therefore, it follows thatP
In(λh0 .µ(h0 , o0 , `), H, h)µ(h, o0 , `)o0 ∈OP0 ,`∈L,h∈H≤ o∈O,`∈L,h∈H In(λh0 .µ(h0 , o, `), H, h)µ(h, o, `)•⊇We prove the contraposition. Suppose (M, M 0 ) 6∈ R.
Then, there exist h, h0 , `, o, o0 such that
– M (h, `) = o, M (h0 , `) = o0 , and o 6= o0– M 0 (h, `) = M 0 (h0 , `)Then, we can pick µ such that µ(h, `) = µ(h0 , `) = 0.5.
We have
GE [µ](M ) = 1.5 − 1 = 0.5
andGE [µ](M 0 ) = 1.5 − 1.5 = 0
Therefore, we have (M, M 0 ) 6∈ CGE [µ].
Theorem 4.5: R ⊆ CCC
Proof: Let M and M 0 be programs such that
(M, M 0 ) ∈ R. We prove (M, M 0 ) ∈ CCC .
By Theorem 4.2, we have∀µ.SE [µ](M ) ≤ SE [µ](M 0 )Now, there exists µ0 such that
CC (M ) = SE [µ0 ](M )Therefore,
SE [µ0 ](M ) ≤ SE [µ0 ](M 0 )Trivially,
SE [µ0 ](M 0 ) ≤ CC (M 0 )Therefore, we have the conclusion.
Theorem 4.6: Let M2 be a non-interferent program.
Then, R(M1 , M2 ) iff M1 is also non-interferent and M1
has the same input domain as M2 .
Proof: Straightforward from Theorems 2.6 and 4.2.
Theorem 4.8: Restricted to loop-free boolean programs,
R is coNP-complete.

•

Proof:R ⊆ coNP
We prove by reducing R to UNSAT, which is coNPcomplete. We reduce via self composition [3], [11].
Let M and M 0 be boolean programs that we want toknow if they are in R. First, we make copies of M
and M 0 , with all variables in M and M 0 replaced by
fresh (primed) variables. Call these copies Mc and Mc0 .
−
→ −
→
→ −
−
→
Let φ = wp(M ; Mc ; M 0 ; Mc0 , O0 = Oc0 ⇒ O = Oc )
→0
−
→0
→−
−
→−
where O ,Oc ,O , and Oc are the low security outputsof M ,Mc ,M 0 , and Mc0 , respectively. Note that φ canbe obtained in time polynomial in the size of M
and M 0 . Here, like in Theorem 3.9, we use the optimized weakest precondition generation technique [13],[17] to generate a formula quadratic in the size of

M ; Mc ; M 0 ; Mc0 . Then, (M, M 0 ) ∈ R if and only if
φ is valid, that is, if and only if ¬φ is unsatisfiable.
• coNP ⊆ R
We prove by reducing NI to R, because NI is coNPcomplete by Theorem 3.9. We can check the noninterference of M by solving R(M, M 0 ) where M 0 is
non-interferent and have the same input domain as M
by Theorem 4.6. Note that such M 0 can be constructedin polynomial time. Therefore, we have coNP ⊆ R.