Quantitative Information Flow as Safety and LivenessHyperproperties∗
Hirotoshi Yasuoka

Tachio Terauchi

Tohoku University
Sendai, Japanyasuoka@kb.ecei.tohoku.ac.jp

Nagoya University
Nagoya, Japanterauchi@is.nagoya-u.ac.jp

We employ Clarkson and Schneider’s “hyperproperties” to classify various verification problemsof quantitative information flow. The results of this paper unify and extend the previous resultson the hardness of checking and inferring quantitative information flow. In particular, we identify
a subclass of liveness hyperproperties, which we call “k-observable hyperproperties”, that can bechecked relative to a reachability oracle via self composition.

1

Introduction

We consider programs containing high security inputs and low 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 [13] for an
overview.
In essence, quantitative information flow measures how secure, or insecure, a program (or a part of aprogram –e.g., a variable–) is. Thus, unlike non-interference [11, 15], that only tells whether a program
is completely secure or not completely secure, a definition of quantitative information flow must be able
to distinguish two programs that are both interfering but have different levels of security.
For example, consider the programs M1 ≡ if H = g then O := 0 else O := 1 and M2 ≡ O := H.
In both programs, H is a high security input and O is a low security output. Viewing H as a password,
M1 is a prototypical login program that checks if the guess g matches the password. 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, a reasonable definition of quantitative information flow should assign ahigher quantity to M2 than to M1 , whereas non-interference would merely say that M1 and M2 are bothinterfering, assuming that there are more than one possible value of H.
Researchers have attempted to formalize the definition of quantitative information flow by appealing
to information theory. This has resulted in definitions based on the Shannon entropy [13, 8, 21], the min
entropy [28], and the guessing entropy [17, 3]. All of these definitions map a program (or a part of aprogram) onto a non-negative real number, that is, they define a function X such that given a program M,
X (M) is a non-negative real number. (Concretely, X is SE[µ] for the Shannon-entropy-based definition
with the distribution µ, ME[µ] for the min-entropy-based definition with the distribution µ, and GE[µ]for the guessing-entropy-based definition with the distribution µ.)
In a previous work [32, 31], we have proved a number of hardness results on checking and inferring quantitative information flow (QIF) according to these definitions. A key concept used to connect
the hardness results to QIF verification problems was the notion of k-safety, which is an instance in a
∗ This work was supported by MEXT KAKENHI 23700026, 22300005, 23220001, and Global COE Program “CERIES.”

To appear in EPTCS.

2

Quantitative Information Flow as Safety and Liveness Hyperproperties

LBP
UBP
LBP constant bound
UBP constant boundSE[U]Liveness
Liveness
Liveness
Liveness

ME[U]Liveness
Safetyk-observablek-safety [31]GE[U]
Liveness
Safetyk-observablek-safety [31]Table 1: A summary of hyperproperty classifications
collection of the class of program properties called hyperproperties [10]. In this paper, we make theconnection explicit by providing a fine-grained classification of QIF problems, utilizing the full range ofhyperproperties. This has a number of benefits, summarized below.
1.) A unified view on the hardness results of QIF problems.
2.) New insights into hyperproperties themselves.
3.) A straightforward derivation of some complexity theoretic results.
Regarding 1.), we focus on two types of QIF problems, an upper-bounding problem that checks if QIF
of a program is bounded above by the given number, and a lower-bounding problem that checks if QIF isbounded below by the given number. Then, for each QIF definitions SE, GE, ME, we classify whether or
not they are safety hyperproperty, k-safety hyperproperty, liveness hyperproperty, or k-observable hyperproperty (and give a bound on k for k-safe/k-observable). Safety hyperproperty, k-safety hyperproperty,
liveness hyperproperty, and observable hyperproperty are classes of hyperproperties defined by Clarksonand Schneider [10]. In this paper, we identify new classes of hyperproperties, k-observable hyperproperty, that is useful for classifying QIF problems. k-observable hyperproperty is a subclass of observable
hyperproperties, and observable hyperproperty is a subclass of liveness hyperproperties.1 We focus on
the case the input distribution is uniform, that is, µ = U, as showing the hardness for a specific caseamounts to showing the hardness for the general case. Also, checking and inferring QIF under the uniformly distributed inputs has received much attention [16, 3, 18, 7, 21, 8], and so, the hardness for theuniform case is itself of research interest.2
Regarding 2.), we show that the k-observable subset of the observable hyperproperties is amenable
to verification via self composition [4, 12, 29, 25, 30], much like k-safety hyperproperties, and identify
which QIF problems belong to that family. We also show that the hardest of the QIF problems (but nevertheless one of the most popular) can only be classified as a general liveness hyperproperty, suggestingthat liveness hyperproperty is a quite permissive class of hyperproperties.
Regarding 3.), we show that many complexity theoretic results for QIF problems of loop-free boolean
programs can be derived from their hyperproperties classifications [32, 31]. We also prove new complexity theoretic results, including the (implicit state) complexity results for loop-ful boolean programs,
complementing the recently proved explicit state complexity results [6].
Table 1 and Table 2 summarize the hyperproperties classifications and computational complexities
of upper/lower-bounding problems. We abbreviate lower-bounding problem, upper-bounding problem,and boolean programs to LBP, UBP, and BP, respectively. The “constant bound” rows correspond tobounding problems with a constant bound (whereas the plain bounding problems take the bound as an
input).
The proofs omitted from the main body of the paper appear in the Appendix.
1 Technically, only non-empty observable hyperproperties are liveness hyperproperties.
2 In fact, computing QIF under other input distributions can sometimes be reduced to this case [2]. See also Section 5.3.

H. Yasuoka & T. Terauchi

3

LBP for BP
UBP for BP
LBP for loop-free BP
UBP for loop-free BP
LBP for loop-free BP, constant bound
UBP for loop-free BP, constant bound

SE[U]PSPACE-hard
PSPACE-hard
PP-hardPP-hard [31]Unknown
Unknown

ME[U]PSPACE-complete
PSPACE-complete
PP-hardPP-hard [31]NP-complete
coNP-complete

GE[U]PSPACE-complete
PSPACE-complete
PP-hardPP-hard [31]NP-complete
coNP-complete

Table 2: A summary of computational complexities

2

Preliminaries

2.1

Quantitative Information Flow

We introduce the information theoretic definitions of QIF that have been proposed in literature. First,
we review the notion of the Shannon entropy [27], H [µ](X), which is the average of the information
content, and intuitively, denotes the uncertainty of the random variable X. And, we review the notion of
the conditional entropy, H [µ](Y |Z), which denotes the uncertainty of Y after knowing Z.
Definition 2.1 (Shannon Entropy and Conditional Entropy) Let X be a random variable with sample
space X and µ be a probability distribution associated with X (we write µ explicitly for clarity). The
Shannon entropy of X is defined as
H [µ](X) = ∑ µ(X = x) logx∈X1µ(X = x)Let Y and Z be random variables with sample space Y and Z, respectively, and µ 0 be a probability
distribution associated with Y and Z. Then, the conditional entropy of Y given Z is defined as
H [µ](Y |Z) = ∑ µ(Z = z)H [µ](Y |Z = z)
z∈Z

where

1
H [µ](Y |Z = z) = ∑y∈Y µ(Y = y|Z = Z) log µ(Y =y|Z=z)=y,Z=z)µ(Y = y|Z = z) = µ(Yµ(Z=z)(The logarithm is in base 2.)
Let M be a program that takes a high security input H, and gives the low security output trace O.
For simplicity, we restrict to programs with just one variable of each kind, but it is trivial to extend theformalism to multiple variables (e.g., by letting the variables range over tuples or lists). Also, for the
purpose of the paper, unobservable (i.e., high security) output traces are irrelevant, and so we assume
that the only program output is the low security output trace. Let µ be a probability distribution over thevalues of H. Then, the semantics of M can be defined by the following probability equation. (We restrict
to deterministic programs in this paper.)µ(O = o) =∑h∈HM(h) = oµ(H = h)4

Quantitative Information Flow as Safety and Liveness Hyperproperties

Here, M(h) denotes the infinite low security output trace of the program M given a input h, and M(h) = odenotes the output trace of M given h that is equivalent to o. In this paper, we adopt the terminationinsensitive security observation model, and let the outputs o and o0 be equivalent iff ∀i ∈ ω.oi = ⊥ ∨ o0i =⊥∨oi = o0i where o and oi denotes the ith element of o, and ⊥ is the special symbol denoting termination.3
In this paper, programs are represented by sets of traces, and traces are represented by lists of storesof programs. More formally,
M(h) is equal to o iff σ0 ; σ1 ; . . . ; σi ; . . . ∈ M
where σ0 (H) = h and ∀i ≥ 1.σi (O) = oi (oi denotes the ith element of o)Here, σ denotes a store that maps variables to values. Because we restrict all programs to determin−−
istic programs, every program M satisfies the following condition: For any trace →σ ,→σ 0 ∈ M, we have
→
−
→
−
→
−
→
−
0
0
0
0
σ0 (H) = σ0 (H) ⇒ σ = σ where σ0 and σ0 denote the first elements of σ and σ , respectively. Now,
we are ready to define Shannon-entropy-based quantitative information flow.
Definition 2.2 (Shannon-Entropy-based QIF [13, 8, 21]) Let M be a program with a high security input H, and a low security output trace O. Let µ be a distribution over H. Then, the Shannon-entropybased quantitative information flow is definedSE[µ](M) = H [µ](H) − H [µ](H|O)
Intuitively, H [µ](H) denotes the initial uncertainty and H [µ](H|O) denotes the remaining uncertainty
after knowing the low security output trace. (For space, the paper focuses on the low-security-input freedefinitions of QIF.)As an example, consider the programs M1 and M2 from Section 1. For concreteness, assume thatg is the value 01 and H ranges over the space {00, 01, 10, 11}. Let U be the uniform 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 ) = H [U](H) − H [U](H|O) = log 4 − 34 log 3 ≈ .81128
SE[U](M2 ) = 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 moresecure than M2 (according to the Shannon-entropy based definition with uniformly distributed inputs),
which agrees with our intuition.
Next, we introduce the min entropy, which has recently been suggested as an alternative measure forquantitative information flow [28].
Definition 2.3 (Min Entropy) Let X and Y be random variables, 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
3 Here, we adopt the trace based QIF formalization of [22].

1V [µ](X|Y )H. Yasuoka & T. Terauchi

5

where

V [µ](X) = maxx∈X µ(X = x)V [µ](X|Y = y) = maxx∈X µ(X = x|Y = y)V [µ](X|Y ) = ∑y∈Y µ(Y = y)V [µ](X|Y = y)Intuitively, V [µ](X) represents the highest probability that an attacker guesses X in a single try. We
now define the min-entropy-based definition of QIF.
Definition 2.4 (Min-Entropy-based QIF [28]) Let M be a program with a high security input H, anda low security output trace O. Let µ be a distribution over H. Then, the min-entropy-based quantitative
information flow is definedME[µ](M) = H∞ [µ](H) − H∞ [µ](H|O)
Computing the min-entropy based quantitative information flow for our running example programs
M1 and M2 from Section 1 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 ) and ME[U](M2 ) 6≤ ME[U](M1 ), and so M2 is deemed
less secure than M1 .
The third definition of quantitative information flow treated in this paper is the one based on theguessing entropy [23], that has also recently been proposed in literature [17, 3].
Definition 2.5 (Guessing Entropy) Let X and Y be random variables, and µ be an associated probability distribution. Then, the guessing entropy of X is defined
G [µ](X) =∑ i × µ(X = xi )1≤i≤mwhere {x1 , x2 , . . . , xm } = X and ∀i, j.i ≤ j ⇒ µ(X = xi ) ≥ µ(X = x j ).
The conditional guessing entropy of X given Y is defined
G [µ](X|Y ) = ∑ µ(Y = y)y∈Y

∑ i × µ(X = xi |Y = y)1≤i≤mwhere {x1 , x2 , . . . , xm } = X and ∀i, j.i ≤ j ⇒ µ(X = xi |Y = y) ≥ µ(X = x j |Y = y).
Intuitively, G [µ](X) represents the average number of times required for the attacker to guess thevalue of X. We now define the guessing-entropy-based quantitative information flow.
Definition 2.6 (Guessing-Entropy-based QIF [17, 3]) Let M be a program with a high security input
H, and a low security output trace O. Let µ be a distribution over H. Then, the guessing-entropy-based
quantitative information flow is defined
GE[µ](M) = G [µ](H) − G [µ](H|O)
We test GE on the running example from Section 1 by calculating the quantities for the programs M1
and M2 with the uniform distribution.
GE[U](M1 ) = G [U](H) − G [U](H|O) = 25 − 74 = 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 considered less secure than M1 , even with the guessing-entropy based definition with the uniform
distribution.

6

2.2

Quantitative Information Flow as Safety and Liveness Hyperproperties

Bounding Problems

We introduce the bounding problems of quantitative information flow that we classify. First, we define
the QIF upper-bounding problems. Upper-bounding problems are defined as follows: Given a program
M and a rational number q, decide if the information flow of M is less than or equal to q.
USE = {(M, q) | SE[U](M) ≤ q}
UME = {(M, q) | ME[U](M) ≤ q}
UGE = {(M, q) | GE[U](M) ≤ q}
Recall that U denotes the uniform distribution.
Next, we define lower-bounding problems. Lower-bounding problems are defined as follows: Givena program M and a rational number q, decide if the information flow of M is greater than q.
LSE = {(M, q) | SE[U](M) > q}
LME = {(M, q) | ME[U](M) > q}
LGE = {(M, q) | GE[U](M) > q}

2.3

Non Interference

We recall the notion of non-interference, which, intuitively, says that the program leaks no information.
Definition 2.7 (Non-intereference [11, 15]) A program M is said to be non-interfering iff for any h, h0 ∈H, M(h) = M(h0 ).
Non-interference is known to be a special case of bounding problems that tests against 0.
Theorem 2.8 ([7, 31]) 1.) M is non-interfering iff (M, 0) ∈ USE . 2.) M is non-interfering iff (M, 0) ∈UME . 3.) M is non-interfering iff (M, 0) ∈ UGE .

3Liveness Hyperproperties

Clarkson and Schneider have proposed the notion of hyperproperties [10].
Definition 3.1 (Hyperproperties [10]) We say that P is a hyperproperty if P ⊆ P(Ψinf ) where Ψinf isthe set of all infinite traces, and P(X) denote the powerset of X.
Note that hyperproperties are sets of trace sets. As such, they are more suitable for classifying information properties than the classical trace properties which are sets of traces. For example, non-interference
is not a trace property but a hyperproperty.
Clarkson and Schneider have identified a subclass of hyperproperties, called liveness hyperproperties,
as a generalization of liveness properties. Intuitively, a liveness hyperproperty is a property that can not
be refuted by a finite set of finite traces. That is, if P is a liveness hyperproperty, then for any finite set offinite traces T , there exists a set of traces that contains T and satisfies P. Formally, let Obs be the set offinite sets of finite traces, and Prop be the set of sets of infinite traces (i.e., hyperproperties), that is,
Obs = P fin (Ψfin )Prop = P(Ψinf )(Here, P fin (X) denotes the finite subsets of X, Ψfin denotes the set of finite traces.) Let ≤ be therelation over Obs × Prop such that
S≤T

iff

∀t ∈ S.∃t 0 .t ◦ t 0 ∈ T

where t ◦ t 0 is the sequential composition of t and t 0 . Then,H. Yasuoka & T. Terauchi

7

Definition 3.2 (Liveness Hyperproperties [10]) We say that a hyperproperty P is a liveness hyperproperty if for any set of traces S ∈ Obs, there exists a set of traces S0 ∈ Prop such that S ≤ S0 and S0 ∈ P.
Now, we state the first main result of the paper: the lower-bounding problems are liveness hyperproperties.4
Theorem 3.3 LSE , LME , and LGE are liveness hyperproperties.5
The proof follows from the fact that, for any program M, there exists a program M 0 containing all theobservations of M and has an arbitrary large information flow.6
We show that the upper-bounding problem for Shannon-entropy based quantitative information flowis also a liveness hyperproperty.
Theorem 3.4 USE is a liveness hyperproperty.
The theorem follows from the fact that we can lower the amount of the information flow by adding traces
that have the same output trace. Therefore, for any program M, there exists M 0 having more observation
than M such that SE[U](M 0 ) ≤ q.

3.1

Observable Hyperproperties

Clarkson and Schneider [10] have identified a class of hyperproperties, called observable hyperproperties, to generalize the notion of observable properties [1] to sets of traces.7
Definition 3.5 (Observable Hyperproperties [10]) We say that P is a observable hyperproperty if forany set of traces S ∈ P, there exists a set of traces T ∈ Obs such that T ≤ S, and for any set of traces
S0 ∈ Prop, T ≤ S0 ⇒ S0 ∈ P.
We call T in the above definition an evidence.
Intuitively, observable hyperproperty is a property that can be verified by observing a finite set offinite traces. We prove a relationship between observable hyperproperties and liveness hyperproperties.
Theorem 3.6 Every non-empty observable hyperproperty is a liveness hyperproperty.
Proof: Let P be a non-empty observable hyperproperty. It must be the case that there exists a set oftraces M ∈ P. Then, there exists T ∈ Obs such that T ≤ M and ∀M 0 ∈ Prop.T ≤ M 0 ⇒ M 0 ∈ P. For
any set of traces S ∈ Obs, there exists M 0 ∈ Prop such that S ≤ M 0 . Then, we have M ∪ M 0 ∈ P, because
T ≤ M ∪ M 0 . Therefore, P is a liveness hyperproperty. 2
We note that the empty set is not a liveness hyperproperty but an observable hyperproperty.
We show that lower-bounding problems for min-entropy and guessing-entropy are observable hyperproperties.
Theorem 3.7 LME is an observable hyperproperty.
Theorem 3.8 LGE is an observable hyperproperty.
4 We implicitly extend the notion of hyperproperties to classify hyperproperties that take programs and rational numbers.

See [31].
5 More precisely, we prove that they are liveness hyperproperties for deterministic systems [10], because we restrict all
programs to deterministic programs. For sake of simplicity, we omit such annotations.
6 Here, we assume that the input domains are not bounded. Therefore, we can construct a program that leaks more highsecurity inputs by enlarging the input domain. Hyperproperty classifications of bounding problems with bounded domains
appear in Section 5.1.
7 Roughly, an observable property is a set of traces having a finite evidence prefix such that any trace having the prefix isalso in the set.

8

Quantitative Information Flow as Safety and Liveness Hyperproperties

Theorem 3.7 follows from the fact that, if (M, q) ∈ LME , then M contains an evidence of LME . This
follows from the fact that when a program M 0 contains at least as much observation as M, ME[U](M) ≤ME[U](M 0 ) (cf. Lemma 3.15). Theorem 3.8 is proven in a similar manner.
We show that neither of the bounding problems for Shannon-entropy are observable hyperproperties.
Theorem 3.9 Neither USE nor LSE is an observable hyperproperty.
We give the intuition of the proof for USE . Suppose SE[U](M) ≤ q. M does not provide an evidence ofSE[U](M) ≤ q, because for any potential evidence, we can raise the amount of the information flow byadding traces that have disjoint output traces. The result for LSE is shown in a similar manner.
It is interesting to note that the bounding problems of SE can only be classified as general livenesshyperproperties (cf. Theorem 3.3 and 3.4) even though SE is often the preferred definition of QIF inpractice [13, 8, 21]. This suggests that approximation techniques may be necessary for checking andinferring Shannon-entropy-based QIF.

3.2

K-Observable Hyperproperties

We define k-observable hyperproperty that refines the notion of observable hyperproperties. Informally,a k-observable hyperproperty is a hyperproperty that can be verified by observing k finite traces.
Definition 3.10 (K-Observable Hyperproperties) We say that a hyperproperty P is a k-observable hyperproperty if for any set of traces S ∈ P, there exists T ∈ Obs such that T ≤ S, |T | ≤ k, and for any setof traces S0 ∈ Prop, T ≤ S0 ⇒ S0 ∈ P.
Clearly, any k-observable hyperproperty is an observable hyperproperty.
We note that k-observable hyperproperties can be reduced to 1-observable hyperproperties by a simple program transformation called self composition [4, 12].
Definition 3.11 (Parallel Self Composition [10]) Parallel self composition of S is defined as follows.
S × S = {(s[0], s0 [0]); (s[1], s0 [1]); (s[2], s0 [2]); · · · | s, s0 ∈ S}
where s[i] denotes the ith element of s.
Then, a k-product parallel self composition (simply self composition henceforth) is defined as Sk .
Theorem 3.12 Every k-observable hyperproperty can be reduced to a 1-observable hyperproperty via a
k-product self composition.
As an example, consider the following hyperproperty. The hyperproperty is the set of programs that return 1 and 2 for some inputs. Intuitively, the hyperproperty expresses two good things happen (programs
return 1 and 2) for programs.
{M | ∃h, h0 .M(h) = 1 ∧ M(h0 ) = 2}This is a 2-observable hyperproperty as any program containing two traces, one having 1 as the output
and the other having 2 as the output, satisfies it.
We can check the above property by self composition. (Here, || denotes a parallel composition.)M 0 (H, H 0 )≡O := M(H) || O0 := M(H 0 ) || assert(¬(O = 1 ∧ O0 = 2))

Clearly, M satisfies the property iff the assertion failure is reachable in the above program, that is, iff thepredicate O = 1 ∧ O0 = 2 holds for some inputs H, H 0 . (Note that, for convenience, we take an assertion
failure to be a “good thing”.)
We show that neither the lower-bounding problem for min-entropy nor the lower-bounding problem
for guessing-entropy is a k-observable hyperproperty for any k.

H. Yasuoka & T. Terauchi

9

Theorem 3.13 Neither LME nor LGE is a k-observable property for any k.
However, if we let q be a constant, then we obtain different results. First, we show that the lowerbounding problem for min-entropy-based quantitative information flow under a constant bound q, is ab2q c + 1-observable hyperproperty.
Theorem 3.14 Let q be a constant. Then, LME is a b2q c + 1-observable hyperproperty.
The theorem follows from Lemma 3.15 below which states that min-entropy based quantitative information flow under the uniform distribution coincides with the logarithm of the number of output traces.
That is, (M, q) ∈ LME iff there is an evidence in M containing b2q c + 1 disjoint outputs.
Lemma 3.15 ([28]) ME[U](M) = log |{o | ∃h.M(h) = o}|
Next, we show that the lower-bounding problem for guessing-entropy-based quantitative information(bqc+1)2
flow under a constant bound q is a b bqc+1−q
c + 1-observable hyperproperty.
2(bqc+1)
c + 1-observable hyperproperty.
Theorem 3.16 Let q be a constant. Then, LGE is a b bqc+1−q

The proof of the theorem is similar to that of Theorem 3.14, in that the size of the evidence set can becomputed from the bound q.

3.3

Computational Complexities

We prove computational complexities of LME and LGE by utilizing their hyperproperty classifications.
Following previous work [32, 31, 6], we focus on boolean programs.
First, we introduce the syntax of boolean programs. The semantics of boolean programs is standard
and is deferred to Appendix (Figure 4). We call boolean programs without while statements loop-freeboolean programs.
M ::= x := ψ | M0 ; M1 | if ψ then M0 else M1 | while ψ do M | skip
φ , ψ ::= true | x | φ ∧ ψ | ¬φFigure 1: The syntax of boolean programs
In this paper, we are interested in the computational complexity with respect to the syntactic sizeof the input program (i.e., “implicit state complexity”, as opposed to [6] which studies complexity overprograms represented as explicit states).
We show that the lower-bounding problems for min-entropy and guessing-entropy are PP-hard.
Theorem 3.17 LME and LGE for loop-free boolean programs are PP-hard.
The theorem is proven by a reduction from MAJSAT, which is a PP-hard problem. PP is the set ofdecision problems solvable by a polynomial-time nondeterministic Turing machine which accepts the
input iff more than half of the computation paths accept. MAJSAT is the problem of deciding, given a→−−boolean formula φ over variables →x , if there are more than 2| x |−1 satisfying assignments to φ .
Next, we show that if q be a constant, the upper-bounding problems for min-entropy and guessingentropy become NP-complete.
Theorem 3.18 Let q be a constant. Then, LME and LGE are NP-complete for loop-free boolean programs.

10

Quantitative Information Flow as Safety and Liveness Hyperproperties

NP-hardness is proven by a reduction from SAT , which is a NP-complete problem. The proof that LME
and LGE for a constant q are in NP follows from the fact that LME and LGE are k-observable hyperproperties for some k. We give the proof intuition for LME . Recall that k-observable hyperproperties canbe reduced to 1-observable hyperproperties via self composition. Consequently, it is possible to decide
if the information flow of a given program M is greater than q by checking if the predicate of the assert
statement is violated for some inputs in the following program.
M 0 (H1 , H2 , . . . , Hn ) ≡O1 := M(H1 ); O2 := M(H2 ); . . . ; On := M(Hn );W
assert( i, j∈{1,...,n} (Oi = O j ∧ i 6= j))where n = b2q c + 1. Let φ be the weakest precondition of O1 := M(H1 ); O2 := M(H2 ); . . . ; On := M(Hn )W
with respect to the post condition i, j∈{1,...,n} (Oi = O j ∧i 6= j). Then, ME[U](M) > q iff ¬φ is satisfiable.
Because a weakest precondition of a loop-free boolean program is a polynomial size boolean formulaover the boolean variables representing the inputs8 , deciding ME[U](M) > q is reducible to SAT.
For boolean programs (with loops), LME and LGE are PSPACE-complete, and LSE is PSPACE-hard(the tight upper-bound is open for LSE ).
Theorem 3.19 LME and LGE are PSPACE-complete for boolean programs.
Theorem 3.20 LSE is PSPACE-hard for boolean programs.

4

Safety Hyperproperties

Clarkson and Schneider [10] have proposed safety hyperproperties, a subclass of hyperproperties, as a
generalization of safety properties. Intuitively, a safety hyperproperty is a hyperproperty that can be
refuted by observing a finite set of finite traces.
Definition 4.1 (Safety Hyperproperties [10]) We say that a hyperproperty P is a safety hyperproperty
if for any set of traces S 6∈ P, there exists a set of traces T ∈ Obs such that T ≤ S, and ∀S0 ∈ Prop.T ≤S0 ⇒ S0 6∈ P.
We classify some upper-bounding problems as safety hyperproperties.
Theorem 4.2 UME and UGE are safety hyperproperties.
Next, we review the definition of k-safety hyperproperties [10], which refines the notion of safety hyperproperties. Informally, a k-safety hyperproperty is a hyperproperty which can be refuted by observing
k number of finite traces.
Definition 4.3 (K-Safety Hyperproperties [10]) We say that a hyperproperty P is a k-safety property
if for any set of traces S 6∈ P, there exists a set of traces T ∈ Obs such that T ≤ S, |T | ≤ k, and ∀S0 ∈Prop.T ≤ S0 ⇒ S0 6∈ P.
Note that 1-safety hyperproperty is just the standard safety property, that is, a property that can be refutedby observing a finite execution trace. The notion of k-safety hyperproperties first came into limelightwhen it was noticed that non-interference is a 2-safety hyperproperty, but not a 1-safety hyperproperty [29].
A k-safety hyperproperty can be reduced to a 1-safety hyperproperty by self composition [4, 12].
8 For loop-free boolean programs, a weakest precondition can be constructed in polynomial time [14, 20].

H. Yasuoka & T. Terauchi

11

Theorem 4.4 ([10]) k-safety hyperproperty can be reduced to 1-safety hyperproperty by self composition.
We have shown in our previous work that UME and UGE are k-safety hyperproperties when the boundq is fixed to a constant.
Theorem 4.5 ([31]) Let q be a constant. UME is a b2q c + 1-safety property.
2(bqc+1)
Theorem 4.6 ([31]) Let q be a constant. UGE is a b bqc+1−q
c + 1-safety property.

The only hyperproperty that is both a safety hyperproperty and a liveness hyperproperty is P(Ψinf ),that is, the set of all traces [10]. Consequently, neither UME nor UGE is a liveness hyperproperty.
We have also shown in the previous work that the upper-bounding problem for Shannon-entropy
based quantitative information flow is not a k-safety hyperproperty, even when q is a constant.
Theorem 4.7 ([31]) Let q be a constant. USE is not a k-safety property for any k > 0.

4.1

Computational Complexities

We prove computational complexities of upper-bounding problems by utilizing their hyperproperty classifications. As in Section 3.3, we focus on boolean programs.
First, we show that when q is a constant, UME and UGE are coNP-complete.
Theorem 4.8 Let q be a constant. Then, UME and UGE are coNP-complete for loop-free boolean programs.
coNP-hardness follows from the fact that non-interference is coNP-hard [31]. The coNP part of theproof is similar to the NP part of Theorem 3.18, and uses the fact that UME is k-safety for a fixed q anduses self composition. By self composition, the upper-bounding problem can be reduced to a reachability
problem (i.e., an assertion failure is unreachable for any input). To decide if ME[U](M) ≤ q, we construct
the following self-composed program M 0 from the given program M.
M 0 (H1 , H2 , . . . , Hn ) ≡O1 := M(H1 ); O2 := M(H2 ); . . . ; On := M(Hn );W
assert( i, j∈{1,...,n} (Oi = O j ∧ i 6= j))where n = b2q c + 1. Then, the weakest precondition of O1 := M(H1 ); O2 := M(H2 ); . . . ; On := M(Hn )W
with respect to the post condition i, j∈{1,...,n} (Oi = O j ∧ i 6= j) is valid iff ME[U](M) ≤ q. Becausea weakest precondition of a loop-free boolean program is a polynomial size boolean formula, and the
problem of deciding a given boolean formula is valid is a coNP-complete problem, UME is in coNP.
Like the lower-bounding problems UME and UGE for boolean programs (with loops) are PSPACEcomplete, and USE is PSPACE-hard.
Theorem 4.9 UME and UGE are PSPACE-complete for boolean programs.
Theorem 4.10 USE is PSPACE-hard for boolean programs.

12

Quantitative Information Flow as Safety and Liveness Hyperproperties

5

Discussion

5.1

Bounding Domains

The notion of hyperproperty is defined over all programs regardless of their size. (For example, noninterference is a 2-safety property for all programs and reachability is a safety property for all programs.)
But, it is easy to show that the lower bounding problems would become “k-observable” hyperproperties
if we constrained and bounded the input domains because then the size of the semantics (i.e., the numberof traces) of such programs would be bounded by |H| (and upper bounding problems would become“k-safety” hyperproperties [31]). In this case, the problems are trivially |H|-observable hyperproperties.
However, these bounds are high for all but very small domains, and are unlikely to lead to a practicalverification method.

5.2

Observable Hyperproperties and Observable Properties

As remarked in [10], observable hyperproperties generalize the notion of observable properties [1]. It
can be shown that there exists a non-empty observable property that is not a liveness property (e.g., theset of all traces that starts with σ ). In contrast, Theorem 3.6 states that every non-empty observable
hyperproperty is also a liveness hyperproperty. Intuitively, this follows because the hyperproperty extension relation ≤ allows the right-hand side to contain traces that does not appear in the left-hand side.
Therefore, for any T ∈ Obs, there exists T 0 ∈ Prop that contains T and an evidence of the observable
hyperproperty.

5.3

Maximum of QIF over Distribution

Researchers have studied the maximum of QIF over the distribution. For example, channel capacity [24,22, 26] is the maximum of the Shannon-entropy based quantitative information flow over the distribution(i.e., maxµ SE[µ]). Smith [28] showed that for any program without low-security inputs, the channel
capacity is equal to the min-entropy-based quantitative information flow, that is, maxµ SE[µ] = ME[U].
Therefore, we obtain the same hyperproperty classifications and complexity results for channel capacity
as ME[U].
Min-entropy channel capacity and guessing-entropy channel capacity are respectively the maximums of min-entropy based and guessing-entropy based QIF over distributions (i.e., maxµ ME[µ] andmaxµ GE[µ]). It has been shown that maxµ ME[µ] = ME[U] [5, 19] and maxµ GE[µ] = GE[U] [33],that is, they attain their maximums when the distributions are uniform. Therefore, they have the same
hyperproperty classifications and complexities as ME[U] and GE[U], which we have already analyzed inthis paper.

6

Related WorkČerný et al. [6] have investigated the computational complexity of Shannon-entropy based QIF. Formally, they have defined a Shannon-entropy based QIF for interactive boolean programs, and showedthat the explicit-state computational complexity of their lower-bounding problem is PSPACE-complete.
In contrast, this paper’s complexity results are “implicit” complexity results of bounding problems ofboolean programs (i.e., complexity relative to the syntactic size of the input) some of which are obtainedby utilizing their hyperproperties classifications.

H. Yasuoka & T. Terauchi

13

Clarkson and Schneider [10] have classified quantitative information flow problems via hyperproperties. Namely, they have shown that the problem of deciding if the channel capacity of a given programis q, is a liveness hyperproperty. And, they have shown that an upper-bounding problem for the beliefbased QIF [9] is a safety hyperproperty. (It is possible to refine their result to show that their problem fordeterministic programs is actually equivalent to non-interference, and therefore, is a 2-safety hyperproperty [33].)

7

Conclusion

We have related the upper and lower bounding problems of quantitative information flow, for various
information theoretic definitions proposed in literature, to Clarkson and Schneider’s hyperproperties.
Hyperproperties generalize the classical trace properties, and are thought to be more suitable for classifying information flow properties as they are relations over sets of program traces. Our results confirm
this by giving a fine-grained classification and showing that it gives insights into the complexity of
the QIF bounding problems. One of the contributions is a new class of hyperproperties: k-observable
hyperproperty. We have shown that k-observable hyperproperties are amenable to verification via self
composition.

References[1] Samson Abramsky (1991): Domain Theory in Logical Form. Ann. Pure Appl. Logic 51(1-2), pp. 1–77.
Available at http://dx.doi.org/10.1016/0168-0072(91)90065-T.
[2] Michael Backes, Matthias Berg & Boris Köpf (2011): Non-uniform distributions in quantitative informationflow. In: Proceedings of the 6th ACM Symposium on Information, Computer and Communications Security,
ASIACCS ’11, ACM, New York, NY, USA, pp. 367–375, doi:http://doi.acm.org/10.1145/1966913.1966960.
Available at http://doi.acm.org/10.1145/1966913.1966960.
[3] Michael Backes, Boris Köpf & Andrey Rybalchenko (2009): Automatic Discovery and Quantification ofInformation Leaks. In: IEEE Symposium on Security and Privacy, IEEE Computer Society, pp. 141–153.
Available at http://dx.doi.org/10.1109/SP.2009.18.
[4] Gilles Barthe, Pedro R. D’Argenio & Tamara Rezk (2004): Secure Information Flow by Self-Composition.
In: CSFW, IEEE Computer Society, pp. 100–114. Available at http://doi.ieeecomputersociety.org/
10.1109/CSFW.2004.17.
[5] Christelle Braun, Konstantinos Chatzikokolakis & Catuscia Palamidessi (2009): Quantitative Notions of
Leakage for One-try Attacks. Electr. Notes Theor. Comput. Sci. 249, pp. 75–91. Available at http://dx.
doi.org/10.1016/j.entcs.2009.07.085.
[6] Pavol Černý, Krishnendu Chatterjee & Thomas A. Henzinger (2011): The Complexity of Quantitative Information Flow Problems. In: CSF, IEEE Computer Society, pp. 205–217. Available at http://doi.
ieeecomputersociety.org/10.1109/CSF.2011.21.
[7] David Clark, Sebastian Hunt & Pasquale Malacaria (2005): Quantified Interference for a While Language.
Electr. Notes Theor. Comput. Sci. 112, pp. 149–166. Available at http://dx.doi.org/10.1016/j.
entcs.2004.01.018.
[8] David Clark, Sebastian Hunt & Pasquale Malacaria (2007): A static analysis for quantifying information flow
in a simple imperative language. J. Comput. Secur. 15, pp. 321–371. Available at http://dl.acm.org/
citation.cfm?id=1370628.1370629.
[9] Michael R. Clarkson, Andrew C. Myers & Fred B. Schneider (2005): Belief in Information Flow. In: CSFW,IEEE Computer Society, pp. 31–45. Available at http://dx.doi.org/10.1109/CSFW.2005.10.

14

Quantitative Information Flow as Safety and Liveness Hyperproperties[10] Michael R. Clarkson & Fred B. Schneider (2010): Hyperproperties. Journal of Computer Security 18(6), pp.
1157–1210. Available at http://dx.doi.org/10.3233/JCS-2009-0393.
[11] Ellis S. Cohen (1977): Information Transmission in Computational Systems. In: SOSP, pp. 133–139. Available at http://doi.acm.org/10.1145/800214.806556.
[12] Ádám Darvas, Reiner Hähnle & David Sands (2005): A Theorem Proving Approach to Analysis of Secure
Information Flow. In Dieter Hutter & Markus Ullmann, editors: SPC, Lecture Notes in Computer Science
3450, Springer, pp. 193–209. Available at http://dx.doi.org/10.1007/978-3-540-32004-3_20.
[13] Dorothy Elizabeth Robling Denning (1982): Cryptography and data security. Addison-Wesley Longman
Publishing Co., Inc., Boston, MA, USA.
[14] Cormac Flanagan & James B. Saxe (2001): Avoiding exponential explosion: generating compact verification
conditions. In: POPL, pp. 193–205. Available at http://doi.acm.org/10.1145/360204.360220.
[15] Joseph A. Goguen & José Meseguer (1982): Security Policies and Security Models. In: IEEE Symposium
on Security and Privacy, pp. 11–20.
[16] Jonathan Heusser & Pasquale Malacaria (2009): Applied Quantitative Information Flow and Statistical
Databases. In Pierpaolo Degano & Joshua D. Guttman, editors: Formal Aspects in Security and Trust,Lecture Notes in Computer Science 5983, Springer, pp. 96–110. Available at http://dx.doi.org/10.
1007/978-3-642-12459-4_8.
[17] Boris Köpf & David A. Basin (2007): An information-theoretic model for adaptive side-channel attacks. In
Peng Ning, Sabrina De Capitani di Vimercati & Paul F. Syverson, editors: ACM Conference on Computer andCommunications Security, ACM, pp. 286–296. Available at http://doi.acm.org/10.1145/1315245.
1315282.
[18] Boris Köpf & Andrey Rybalchenko (2010): Approximation and Randomization for Quantitative
Information-Flow Analysis. In: CSF, IEEE Computer Society, pp. 3–14. Available at http://doi.
ieeecomputersociety.org/10.1109/CSF.2010.8.
[19] Boris Köpf & Geoffrey Smith (2010): Vulnerability Bounds and Leakage Resilience of Blinded Cryptography under Timing Attacks. In: CSF, IEEE Computer Society, pp. 44–56. Available at http://doi.ieeecomputersociety.org/10.1109/CSF.2010.11.
[20] K. Rustan M. Leino (2005): Efficient weakest preconditions. Inf. Process. Lett. 93(6), pp. 281–288. Available
at http://dx.doi.org/10.1016/j.ipl.2004.10.015.
[21] Pasquale Malacaria (2007): Assessing security threats of looping constructs. In Martin Hofmann & Matthias
Felleisen, editors: POPL, ACM, pp. 225–235. Available at http://doi.acm.org/10.1145/1190216.
1190251.
[22] Pasquale Malacaria & Han Chen (2008): Lagrange multipliers and maximum information leakage in different
observational models. In Úlfar Erlingsson & Marco Pistoia, editors: PLAS, ACM, pp. 135–146. Available
at http://doi.acm.org/10.1145/1375696.1375713.
[23] James L. Massey (1994): Guessing and Entropy. In: ISIT ’94: Proceedings of the 1994 IEEE International Symposium on Information Theory, p. 204. Available at http://dx.doi.org/10.1109/ISIT.
1994.394764.
[24] Stephen McCamant & Michael D. Ernst (2008): Quantitative information flow as network flow capacity. In
Rajiv Gupta & Saman P. Amarasinghe, editors: PLDI, ACM, pp. 193–205. Available at http://doi.acm.
org/10.1145/1375581.1375606.
[25] David A. Naumann (2006): From Coupling Relations to Mated Invariants for Checking Information Flow.
In Dieter Gollmann, Jan Meier & Andrei Sabelfeld, editors: ESORICS, Lecture Notes in Computer Science
4189, Springer, pp. 279–296. Available at http://dx.doi.org/10.1007/11863908_18.
[26] James Newsome, Stephen McCamant & Dawn Song (2009): Measuring channel capacity to distinguishundue influence. In Stephen Chong & David A. Naumann, editors: PLAS, ACM, pp. 73–85. Available at
http://doi.acm.org/10.1145/1554339.1554349.

H. Yasuoka & T. Terauchi

15[27] Claude Shannon (1948): A Mathematical Theory of Communication. Bell System Technical Journal 27, pp.
379–423, 623–656. Available at http://doi.acm.org/10.1145/584091.584093.
[28] Geoffrey Smith (2009): On the Foundations of Quantitative Information Flow. In Luca de Alfaro, editor:
FOSSACS, Lecture Notes in Computer Science 5504, Springer, pp. 288–302. Available at http://dx.doi.
org/10.1007/978-3-642-00596-1_21.
[29] Tachio Terauchi & Alexander Aiken (2005): Secure Information Flow as a Safety Problem. In Chris Hankin& Igor Siveroni, editors: SAS, Lecture Notes in Computer Science 3672, Springer, pp. 352–367. Available
at http://dx.doi.org/10.1007/11547662_24.
[30] Hiroshi Unno, Naoki Kobayashi & Akinori Yonezawa (2006): Combining type-based analysis and model
checking for finding counterexamples against non-interference. In Vugranam C. Sreedhar & Steve
Zdancewic, editors: PLAS, ACM, pp. 17–26. Available at http://doi.acm.org/10.1145/1134744.
1134750.
[31] Hirotoshi Yasuoka & Tachio Terauchi (2010): On Bounding Problems of Quantitative Information Flow. In
Dimitris Gritzalis, Bart Preneel & Marianthi Theoharidou, editors: ESORICS, Lecture Notes in Computer
Science 6345, Springer, pp. 357–372. Available at http://dx.doi.org/10.1007/978-3-642-15497-3_
22.
[32] Hirotoshi Yasuoka & Tachio Terauchi (2010): Quantitative Information Flow - Verification Hardness and Possibilities. In: CSF, IEEE Computer Society, pp. 15–27. Available at http://doi.
ieeecomputersociety.org/10.1109/CSF.2010.9.
[33] Hirotoshi Yasuoka & Tachio Terauchi (2011): On Bounding Problems of Quantitative Information Flow
(Extended version). Journal of Computer Security 19(6), pp. 1029–1082. Available at http://dx.doi.
org/10.3233/JCS-2011-0437.

A

Appendix

Figure 2: A summary of hyperproperty classifications
Fig 2 shows a summary of hyperproperty classifications.
• LH: the set of all liveness hyperproperties.
• OH: the set of all non-empty observable hyperproperties.

16

Quantitative Information Flow as Safety and Liveness Hyperproperties• 3OH: the set of all non-empty 3-observable hyperproperties.
• 5OH: the set of all non-empty 5-observable hyperproperties.
• SH: the set of all safety hyperproperties.
• 2SH: the set of all 2-safety hyperproperties.
• 3SH: the set of all 3-safety hyperproperties.
• 5SH: the set of all 5-safety hyperproperties.
• LME (1): LME under the constant bound 1.
• LGE (1): LGE under the constant bound 1.
• UME (1): UME under the constant bound 1.
• UGE (1): UGE under the constant bound 1.
• NI: the set of all non-interfering programs.

In general, for a constant bound q, LME (q) is in the class b2q c + 1-OH and LGE (q) is in the class(bqc+1)2
c + 1-OH, and such classes are all contained in OH. Likewise, for a constant bound q, UME (q)b bqc+1−q2(bqc+1)
c + 1-SH, with such classes all contained
is in the class b2q c + 1-SH and UGE (q) is in the class b bqc+1−q
in SH.

A.1

Omitted Proof

Definition A.1
In(µ, X, x) = |{x0 ∈ X | µ(x0 ) ≥ µ(x)}|Intuitively, In(µ, X, x) is the order of x defined in terms of µ.
Lemma A.2
G [µ](X) = Σ1≤i≤|X| iµ(xi ) = Σx∈X In(µ, X, x)µ(x)Proof: Trivial. 2
Theorem 2.8. 1.) M is non-interfering iff (M, 0) ∈ USE . 2.) M is non-interfering iff (M, 0) ∈ UME . 3.)
M is non-interfering iff (M, 0) ∈ UGE .
Proof: Let O = {M(h, `) | h ∈ H ∧ ` ∈ L}.
• SE(See [7].)• ME– ⇒Suppose M is non-interfering. By definition, it suffices to show that
V [U](H) = V [U](H|O)
That is,max U(h) = ∑ U(o) max U(h|o)
hohH. Yasuoka & T. Terauchi

17

The fact that M is non-interfering implies that there exists o0 such that for any h, M(h) = o0 ,and U(h, o0 ) = U(h). Therefore, we have0U(h,o )∑o U(o) maxh U(h|o) = maxh U(o0 )= maxh U(h)– ⇐We prove the contraposition. Suppose M is interfering. That is, there exist h1 and h2 suchthat M(h1 ) 6= M(h2 ). Let o1 = M(h1 ) and o2 = M(h2 ). We have∑o U(o) maxh U(h|o)= ∑o∈O\{o1 ,o2 } maxh U(h, o) + maxh U(h, o1 ) + maxh U(h, o2 )And,
max U(h) = max U(h, o1 )hhTherefore, we have ME[U](M) > 0.
• GE
– ⇒Suppose M is non-interfering. By definition,
GE[U](M)= ∑h In(λ h0 .U(h0 ), H, h)U(h)− ∑o ∑h In(λ h0 .U(h0 , o), H, h)U(h, o)= ∑h In(λ h0 .U(h0 ), H, h)U(h)− ∑h In(λ h0 .U(h0 ), H, h)U(h)=0since for all hx and ox such that U(hx , ox ) > 0, for any h0x and o0 ∈ O \ {ox }, U(h0x , o0x ) = 0.
– ⇐We prove the contraposition. Suppose M is interfering. That is, there exist h1 and h2 suchthat M(h1 ) 6= M(h2 ). Let o1 = M(h1 ) and o2 = M(h2 ). By the definition,
GE[U](M)= ∑h In(λ h0 .U(h0 ), H, h)U(h)− ∑o ∑h In(λ h0 .U(h0 , o), H, h)U(h, o)= A + ∑h In(λ h0 .U(h0 ), H, h)U(h)−B − ∑o ∑h In(λ h0 .U(h0 , o), H, h)U(h, o)
where

A = ∑h In(λ h0 .U(h0 ), H, h)U(h)B = ∑o∈O ∑h In(λ h0 .U(h0 , o), H, h)U(h, o)Trivially, we have A ≥ B and∑h In(λ h0 .U(h0 ), H, h)U(h)> ∑o ∑h In(λ h0 .U(h0 , o), H, h)U(h, o)Therefore, we have GE[U](M) > 0.

18

Quantitative Information Flow as Safety and Liveness Hyperproperties

2
Hereafter, we write sets of pairs of input and output trace to mean programs. That is, we write(h, o) ∈ M iff M(h) = o.
Lemma A.3 For any rational numbers q, for any traces T ∈ Obs, there exist M 0 and M 00 such thatT ≤ M 0 , T ≤ M 00 , SE[U](M 0 ) ≤ q, and SE[U](M 00 ) > q.
Proof: Firstly, we prove that there exists M 0 such that T ≤ M 0 and SE[U](M 0 ) ≤ q. Let MT be a program
such that |MT | = |T | and T ≤ MT . We construct the following programs.
M 0 = MT ∪ {(h, o) | h ∈ H0 }M1 = {(h, oh ) | h ∈ H} ∪ {(h, o) | h ∈ H0 }where
• H = dom(M),• H0 ∩ H = 0,/
• for any h and h0 in H, h 6= h0 ⇒ oh 6= oh0 ,• for any h ∈ H0 , o 6= M(h), and• for any h0 ∈ H0 , o 6= oh .
It follows that
SE[U](M 0 ) ≤ SE[U](M1 )And, we have
SE[U](M1 )

0

0

|H|
|H |
|H|+|H |0= |H|+|H
0 | log(|H| + |H |) + |H|+|H0 | log
|H0 |
→ 0
(|H0 | → ∞)Therefore, there exists H0 such that SE[U](M 0 ) ≤ q.
Finally, we prove that there exists M 00 such that T ≤ M 00 and SE[U](M 00 ) > q. Let MT be a program
such that |MT | = |T | and T ≤ MT . We construct the following programs.
M 00 = MT ∪ {(h, oh ) | h ∈ H0 }M1 = {(h, o) | h ∈ H} ∪ {(h, oh ) | h ∈ H0 }where
• H = dom(M),• H0 ∩ H = 0,/
• for any h and h0 in H0 , h 6= h0 ⇒ oh 6= oh0 , and• for any h0 ∈ H0 , for any h ∈ H, oh0 6= M(h)It follows that
SE[U](M 00 ) ≥ SE[U](M1 )And, we have
SE[U](M1 )

0

0

|H |
|H|
|H|+|H |0= |H|+|H
0 | log(|H| + |H |) + |H|+|H0 | log|H|→ ∞(|H0 | → ∞)Therefore, there exists H0 such that SE[U](M 00 ) > q.
2

H. Yasuoka & T. Terauchi

19

Theorem 3.3. LSE , LME , and LGE are liveness hyperproperties.
Proof: The fact that LSE is a liveness hyperproperty follows from Lemma A.3. The results for LME andLGE follow from Theorem 3.7, Theorem 3.8, and Theorem 3.6. 2
Theorem 3.4. USE is a liveness hyperproperty.
Proof: Straightforward by Lemma A.3. 2
Theorem 3.7. LME is a observable hyperproperty.
Proof: Let M be a program and q be a rational number such that (M, q) ∈ LME . By the definition of theequivalence relation on outputs, there exists T ∈ Obs such that ME[U](T ) = ME[U](M). By Lemma 3.15,
for any programs M 0 , if T ≤ M 0 , then ME[U](M 0 ) > q. Therefore, LME is a observable hyperproperty. 2
1
Lemma A.4 Let M be a program. Then, we have GE[U](M) = 2n − 2n∑o |Ho |2 where n is the number of
inputs, and Ho = {h | o = M(h)}.

Proof: By the definition, we have
GE[U](M) = G [U](H) − G [U](H|O)= ∑h In(U, H, h)U(h)− ∑o U(o) ∑h In(λ h0 .U(h0 |o), Ho , h)U(h|o)= 1n 21 n(n + 1) − ∑o |Hno | 12 |H1o | |Ho |(|Ho | + 1)
1
= 2n + 12 − 2n∑o |Ho |2 − 121
= n2 − 2n∑o |Ho |22
Lemma A.5 Let M and M 0 be programs such that [[M 0 ]] = [[M]] ∪ {(h, o)} and h 6∈ dom([[M]]). Then, we
have GE[U](M) ≤ GE[U](M 0 ).
Proof: We prove GE[U](M 0 ) − GE[U](M) ≥ 0. Let n = |[[M]]|, O = ran([[M]]), H = dom(M), and
Ho = dom(h | o = M(h)).
By Lemma A.4, we have
GE[U](M 0 ) − GE[U](M)
1
n
1
2
2
= n+1
2 − 2(n+1) (B + (|Ho | + 1) ) − 2 + 2n (B + |Ho | )1= 12 + 2n(n+1)(−n(B + (|Ho | + 1)2 ) + (n + 1)(B + |Ho |2 ))1= 2n(n+1) (n(n + 1) − n(|Ho | + 1)2 + B + (n + 1)(|Ho |2 ))1= 2n(n+1)(n2 − 2n|Ho | + |Ho |2 + B)1
= 2n(n+1)((n − |Ho |)2 + B)
≥0
where B = ∑o0 ∈O\{o} |Ho0 |2 and Ho0 = {h | o0 = M(h)}. 2
Theorem 3.8. LGE is a observable hyperproperty.
Proof: Let M be a program and q be a rational number such that (M, q) ∈ LGE . By the definition of theequivalence relation on outputs, there exists T ∈ Obs such that GE[U](T ) = GE[U](M). By Lemma A.5,
for any programs M 0 , if T ≤ M 0 , then GE[U](M 0 ) > q. Therefore, LGE is a observable hyperproperty. 2

20

Quantitative Information Flow as Safety and Liveness Hyperproperties

Theorem 3.9. Neither USE nor LSE is a observable hyperproperty.
Proof: Straightforward by Lemma A.3. 2
Theorem 3.13. Neither LME nor LGE is a k-observable hyperproperty for any k.
Proof:• LME
For a contradiction, suppose LME is a k-observable hyperproperty. Let M be a program that has
k + 1 disjoint output traces. Then, We have (M, log(k + 1)) ∈ LME . However, for any T ∈ Obs
such that |T | ≤ k and T ≤ M, ME[U](T ) ≤ log k. This leads to a contradiction.
• LGE
For a contradiction, suppose LGE is a k-observable hyperproperty. Let M be a program that has
k + 1 disjoint output traces. Then, We have (M, 2k ) ∈ LGE . However, for any T ∈ Obs such that
|T | ≤ k and T ≤ M, GE[U](T ) ≤ k−1
2 . This leads to a contradiction.
2
Theorem 3.14. Let q be a constant. Then, LME is a b2q c + 1-observable hyperproperty.
Proof: Let M be a program such that (M, q) ∈ LME . By Lemma 3.15, it must be the case that | ran(M)| ≥b2q c+1 where ran(M) is the range of M. Then, there exists T ≤ M such that |T | ≤ b2q c+1 and ran(T ) ≥b2q c + 1. Then, by Lemma 3.15, it follows that for any program M 0 such that T ≤ M 0 , (M 0 , q) ∈ LME .
Therefore, LME is a b2q c + 1-observable property. 2
Lemma A.6 Let M be a program such that GE[U](M) > q, ∀M 0 .M 0 ( M ⇒ GE[U](M 0 ) ≤ q, and∀M 00 .(GE[U](M 00 ) > q ∧ (∀M 0 .M 0 ( M 00 ⇒ GE[U](M 0 ) ≤ q)) ⇒ |M| ≥ |M 00 |. It must be the case that(bqc+1)2|M| ≤ b bqc+1−q
c + 1.
Proof: First, we prove M has exactly two outputs. Let n be an integer such that n = |M|. If M returns only
one output, we have GE[U](M) = 0. Therefore, M must have more than 1 output, since GE[U](M) > q.
We have for any o0
1(B + (n − i)2 )GE[U](M) = n2 − 2n1
= i − 2n (B + i2 )where i = ∑o∈O\{o0 } |Ho | and B = ∑o∈O\{o0 } |Ho |2 . Because GE[U](M) > q, we have i > q. Then, wehave
2GE[U](M) > q iff i − B+i2n > qB+i2
iff n > 2(i−q)
By the definition of M, we have ∀M 0 .M 0 ( M ⇒ GE[U](M 0 ) ≤ q. Let M̄ = M \ {(h0 , o0 )} where M(h0 ) =o0 . Then, we have
B+i2
GE[U](M̄) ≤ q iff i − 2(n−1)
≤q
2

B+i
iff n ≤ 2(i−q)+1Hence, we haveB + i2B + i2<n≤+12(i − q)2(i − q)

H. Yasuoka & T. Terauchi

21

T (ψ) ≡→−
case (H 0 , ψ, H )→−→−when (true, true, ) then O := H ; O0 := true; O00 := true→−−−→
when (true, false, ) then O := true; O0 := true; O00 := false
→
−
−−→
−−→
when (false, , true) then O := true; O0 := false; O00 := false
else
if H1
→
−
→
−
then O := H ; O0 := false; O00 := true→−−−→else O := true; O0 := false; O00 := false→−→−
where H 0 , H = H1 , . . . , Hn , and O0 , O00 , O are distinct.
Figure 3: The Loop-free Boolean Program for Theorem 3.17.
Because B = ∑o∈O\{o0 } |Ho |2 and i = ∑o∈O\{o0 } |Ho |, the cargest n occurs when B = i2 . That is, when2(bqc+1)
c + 1. Recall that i = ∑o∈O\{o0 } |Ho |. Let
M has exactly two outputs. Next, we prove |M| ≤ b bqc+1−qj = n − i. We have
1 2
GE[U](M) = i − 2n(i + i2 )2= i − in2
= (n − j) − (n−n j)2= j − jn>q

This means that j > q. Recall that M̄ = M \ {(h0 , o0 )} where M(h0 ) = o0 . Then, we have
GE[U](M̄) ≤ q

2i
iff i − n−1≤qi2
iff n ≤ i−q + 1
2

2

2

2

j
j
i
i
c + 1 and n ≤ b j−q
c + 1. Let f = i−q+ 1 = j−q
+ 1. By
Because n is an integer, we have n ≤ b i−qelementary real analysis, it can be shown that for integers i and j such that i > q and j > q, f attains its(bqc+1)2
c + 1. 2
maximum value when i = bqc + 1 or j = bqc + 1. Therefore, it follows that |M| = n ≤ b bqc+1−q2(bqc+1)
Theorem 3.16. Let q be a constant. Then, LGE is a b bqc+1−q
c + 1-observable hyperproperty.
Proof: Let M be a program and q be a rational number such that (M, q) ∈ LGE . By Lemma A.6, there(bqc+1)2
exists T such that T ≤ M and |T | ≤ b bqc+1−q
c + 1. By Lemma A.5, for any M 0 such that T ≤ M 0 ,GE[U](M 0 ) > q. 2

Theorem 3.17. LME and LGE are PP-hard for loop-free boolean programs.
Proof:• LME
We prove by reducing MAJSAT to LME . Let φ be a boolean formula. Let q be the rational number
such thatq = ME[U](T (ψ))= log(2n−1 + 1 + 2n−1 − 1)
= n−1

22

Quantitative Information Flow as Safety and Liveness Hyperproperties
where n is the number of boolean variables in φ , and ψ is a boolean formulas such that #SAT (ψ) =2n−1 . We have
ME[U](T (φ )) > q ⇔ ME[U](T (φ )) ≤ ME[U](T (ψ))⇔ #SAT (φ ) ≥ 2n−1 + 1⇔ #SAT (φ ) > 2n−1
⇔ φ ∈ MAJSAT
by Lemma 3.15. Therefore, we can decide if φ ∈ MAJSAT by deciding if ME[U](T (φ )) ≤ q.
Note that T (φ ) and q can be constructed in time polynomial in the size of φ . Therefore, this is areduction from MAJSAT to LME .
• LGEWe prove by reducing MAJSAT, which is a PP-complete problem, to LGE . Let φ be a boolean
formula. Let q be the rational number such thatq = GE(O := ψ ∨ H)
n+1
1
= 2 2 − 2n+2(|M −1 (true)|2 + |M −1 (false)|2 )1= 2n − 2n+2 ((2n−1 )2 + (2n+1 − 2n−1 )2 )where n is the number of boolean variables in φ , and ψ is a boolean formula such that #SAT (ψ) =2n−1 , and H be a boolean variable that does not appear in ψ and φ . We have
GE[U](O := φ ∨ H) > q ⇔ GE[U](O := φ ∨ H) > GE[U](O := ψ ∨ H)
⇔ GE[U](O := φ ∨ H) > q⇔ #SAT (φ ) > #SAT (ψ)⇔ #SAT (φ ) > 2n−1
⇔ φ ∈ MAJSAT
by Lemma A.5. Therefore, we can decide if φ ∈ MAJSAT by deciding if GE[U](O := φ ∨ H) > q.
Note that O := φ ∨ H and q can be constructed in time polynomial in the size of φ . Therefore, thisis a reduction from MAJSAT to LGE .

2
Theorem 3.18. Let q be a constant. Then, LME and LGE are NP-complete for loop-free boolean programs.
Proof:• LME
LME is NP-hardness follows from the fact that ME[U](O := φ ∧ H) > 0 iff φ ∈ SAT where H is aboolean variable that does not appear in φ .
Next, we show that LME ∈ NP. Recall that k-observable hyperproperties can be reduced to 1observable hyperproperties via self composition. We can decide if the information flow of a given
program M is greater than q by checking if the predicate of the assert statement fails for some
inputs in the following program.
M 0 (H1 , H2 , . . . , Hn ) ≡O1 := M(H1 ); O2 := M(H2 ); . . . ; On := M(Hn );W
assert( i, j∈{1,...,n} (Oi = O j ∧ i 6= j))

H. Yasuoka & T. Terauchi

23

where n = b2q c + 1. That is, if for some inputs, the weakest precondition of M 0 does not hold,then ME[U](M) > q. Since weakest preconditions of loop-free boolean programs are boolean
formulae over boolean variables representing inputs, we can reduce the problem of deciding if
ME[U](M) > q to SAT.
• LGE
We have that GE[U](O := φ ∧ H) > 0 iff φ ∈ SAT where H is a variable that does not appear in φ .
It follows that LGE is NP-hard.
Next, we show LGE ∈ NP
M 0 (H1 , H2 , . . . , Hn ) ≡O1 := M(H1 ); O2 := M(H2 ); . . . ; On := M(Hn );assert(∑o |{Oi | Oi = o}|2 < 2n( n2 + q))2(bqc+1)
where n = b bqc+1−q
c + 1.9 That is, if for some inputs, the weakest precondition of M 0 does nothold, then GE[U](M) > q. Since weakest preconditions of loop-free boolean programs are boolean
formulae over boolean variables representing inputs, we can reduce the problem of deciding if
GE[U](M) > q to SAT.

2
Theorem A.7 Checking non-interference is PSPACE-complete for boolean programs.
Proof: Straightforward from the fact that the reachability for boolean programs is PSPACE-complete. 2
Theorem 3.19. LME and LGE are PSPACE-complete for boolean programs.
Proof: PSPACE-hardness follows from Theorem 2.8 and Theorem A.7.
Next, we show that LME ∈ PSPACE. To prove that ME[U](M) > q, it suffices to show that the
number of outputs is greater than b2q c + 1. Let n be the number of inputs. The number of outputs canbe enumerated in polynomial space, because the number of outputs is less than or equal to 2n , and the
problem of deciding if a program has a particular output can be solved in polynomial space. Therefore,
we have LME ∈ PSPACE.
Finally, we show that LGE ∈ PSPACE. By Lemma A.4, we have ∑o |Ho |2 < 2n( 2n +q) iff GE[U](M) >q. Because ∑o |Ho |2 can be calculated in polynomial space, it follows the result. 2
Theorem 4.2. UME and UGE are safety hyperproperties.
Proof: Straightforward by Lemma 3.15 and Lemma A.5. 2
Theorem 4.8. Let q be a constant. Then, UME and UGE are coNP-complete for loop-free boolean programs.
Proof: By the similar manner to Theorem 3.19, we obtain the results. 2
Theorem 4.9. UME and UGE are PSPACE-complete for boolean programs.
Proof: This theorem is proven in the similar manner to Theorem 3.19. 2

9 Technically, the predicate of the assert statement is represented by a DNF of equalities over O . Therefore, the selfi
composed program can be constructed in time linear in the size of the original program.

24

Quantitative Information Flow as Safety and Liveness Hyperproperties

ev(e, σ ) = v(x := e, σ ) → σ [x 7→ v]
ev(e, σ ) = true
(M0 , σ ) → σ 0(if e then M0 else M1 , σ ) → σ 0ev(e, σ ) = false(M1 , σ ) → σ 0(if e then M0 else M1 , σ ) → σ 0ev(e, σ ) = false(while e do M, σ ) → σev(e, σ ) = true(M, σ ) → σ 00
(while e do M, σ 00 ) → σ 0(while e do M, σ ) → σ 0(skip, σ ) → σ(M, σ ) → σ 00
(M 0 , σ 00 ) → σ 0(M; M 0 , σ ) → σ 0

Figure 4: The semantics of boolean programs