arXiv:1706.01407v2 [] 20 Jun 2017

Towards a Flow- and Path-Sensitive
Information Flow Analysis: Technical Report
Peixuan Li
Danfeng Zhang
Department of Computer Science and Engineering
Penn State University
e-mail: {pzl129,zhang}@cse.psu.edu
Abstract
This paper investigates a flow- and path-sensitive static information flow analysis. Compared with security type systems with fixed labels, it has been shown that flow-sensitive type
systems accept more secure programs. We show that an information flow analysis with fixed
labels can be both flow- and path-sensitive. The novel analysis has two major components:
1) a general-purpose program transformation that removes false dataflow dependencies in a
program that confuse a fixed-label type system, and 2) a fixed-label type system that allows
security types to depend on path conditions. We formally prove that the proposed analysis
enforces a rigorous security property: noninterference. Moreover, we show that the analysis
is strictly more precise than a classic flow-sensitive type system, and it allows sound control
of information flow in the presence of mutable variables without resorting to run-time mechanisms.

1

Introduction

Information-flow security is a promising approach to security enforcement, where the goal is
to prevent disclosure of sensitive data by applications. Since Denning and Denning’s seminal
paper [20], static program analysis has been widely adopted for information-flow control [37].
Among these program analyses, type systems (e.g., [32, 35, 40]) have enjoyed a great popularity due to their strong end-to-end security guarantee, and their inherently compositional nature to
combine secure components forming a larger secure system as long as the type signatures agree.
Conventionally, we assume secrets are stored in variables, and security levels (e.g., P for public
and S for secret) are associated with variables to describe the intended secrecy of the contents.
The security problem is to verify that the final value of the public variables (outputs visible to the
public) is not influenced by the initial value of the secret variables.
Many security type systems (e.g., [32, 35, 40]) assume fixed levels. That is, the security level
for each variable remain unchanged throughout program execution. Though this fixed-level assumption simplifies the design of those type systems, one consequence is that they tend to be
over-conservative (i.e., reject secure programs). For example, given that s has a level S (i.e., s

1

holds a secret value) and p has a level P, a fixed-level type system rejects secure programs, such as
(p := s; p := 0;), even though the publicly observable final value of p is always zero.
Previous work (e.g., [26]) observes that such inaccuracy roots from the flow-insensitive nature
(i.e., the order of program execution is ignored) of fixed-level systems. From this perspective,
the previous example is mistakenly considered insecure because the (impossible) execution order
(p := 0; p := s; ) is insecure.
Hunt and Sands [26] propose a classic flow-sensitive type system which allows a variable to
have multiple security levels over the course of computation. For example, this floating-level
type system correctly accepts the program (p := s; p := 0;) by assigning p with levels S and
P after the first and second assignments respectively. However, this floating-level system is still
path-insensitive, meaning that the predicates at conditional branches are ignored in the analysis.
For example, it incorrectly rejects the following secure program since the (impossible) branch
combination (y := s; p := y; ) is insecure.
if (x = 1) then y := 0 else y := s;
if (x = 1) then p := y
This paper develops a flow- and path-sensitive information flow analysis that is precise enough
to accept the aforementioned secure programs. The novel analysis is built on two key observations.
First, flow-sensitivity can be gained via a general-purpose program transformation that eliminates
false dataflow dependencies that confuse a flow-insensitive type system. Consider the example
(p := s; p := 0;) again. The transformation removes the false dataflow dependency between s and
p by introducing an extra copy of the variable p and keeps track of the final copy of each variable
at the same time. So, the example is transformed to (p1 := s; p2 := 0;), where p2 is marked as the
final copy. Then, a fixed-level system can easily type-check this program by assigning levels S and
P to p1 and p2 respectively.
Second, path-sensitivity can be gained via consolidating dependent type theory (e.g., [16, 38,
42]) into security labels. That is, a security label is, in general, a function from program states to
security levels. Consider the second example above with branches. We can assign y a dependent
security label: (x = 1?P : S), meaning that the level of y is P when x = 1, and S otherwise. Hence,
the information flow from y to p can be judged as secure since it only occurs when x = 1 (hence,
y has level p).
Based on the key observations, we propose a flow- and path-sensitive information flow analysis
that consists of two major components: a general purpose program transformation that removes
false dataflow dependencies that otherwise compromise the precision of a fixed-level system, as
well as a fixed-label type system with dependent labels. Each component of our analysis targets
one insensitive source of previous type systems. The modular design not only enables tunable
precision of our analysis, but also sheds light on the design of security type systems: we show that
a fixed-level system (e.g., [40]) plus the program transformation is as precise as1 the classic flowsensitive system in [26]; furthermore, a fixed-label dependent type system can soundly control
information flow in the presence of mutable variables without resorting to run-time mechanisms
(e.g., [23, 44]).
1

We note that in the information flow literature, different terms (such as “precision” and “permissiveness”) have
been used to compare the amount of false positives of various mechanisms [15]. In this paper, we say a static analysis
A is as precise as a static analysis B if A accepts every secure program that is accepted by B. Moreover, we say A is
(strictly) more precise than B if A is as precise as B, and A accepts at least one secure program that is rejected by B.

2

1 x := s;
2 Jx := 0K;
3 p := x;
(a) Flow-Insensitive Analysis
Rejects Secure Program.

1 x := s;
2 x1 := 0;
3 p := x1 ;
(b) Flow-Insensitive Analysis
Accepts Equivalent Program.

1
2
3
4

x := 0; y := 0;
if (p1 < 0) then y := s;
if (p1 > 0) then x := y;
p2 := x;

(c) Path-Insensitive Analysis Rejects Secure Program.

Figure 1: Examples: Imprecise Information Flow Analysis Rejects Secure Programs.
This paper makes the following key contributions:
1) We formalize a novel flow- and path-sensitive information flow analysis for a simple WHILE
language. The analysis consists of a novel program transformation, which eliminates imprecision due to flow-insensitivity (Section 4), and a purely static type system using dependent
security labels (Section 5).
2) We formally prove the soundness of our analysis (Section 6): the source program satisfies
termination-insensitive noninterference whenever the transformed program type-checks. Novel
proof techniques are required due to the extra variables introduced (for added precision) in the
transformed program.
3) We show that our analysis is strictly more precise than a classic flow-sensitive type system [26]
(Section 7). One interesting consequence is that the program transformation automatically
makes a sound flow-insensitive type system (e.g., [40]) as precise as the classic flow-sensitive
system [26].
4) We show that our dependent type system soundly controls information flow in the presence
of mutable variables without resorting to dynamic mechanisms, such as the dynamic erasure
mechanism in previous work [23, 44].

2
2.1

Background and Overview
Information Flow Analysis

We first review standard information flow terminology used in this paper. We assume all variables
are associated with security levels. A security policy is specified as the ordering of the security
levels, typically in the form of a security lattice. For data d1 with security level `1 and data d2 with
level `2 , the policy allows information flow from d1 to d2 if and only if `1 v `2 . In this paper, we
use two distinguished security levels S (Secret) and P (Public) for simplicity, but keep in mind that
the proposed theory is general enough to express richer security levels. The security policy on the
levels P and S is defined as P v S, while S 6v P. That is, information flow from public data to
secret variable is allowed, while the other direction is forbidden. Hereafter, we assume variable s
is labeled as S, and variable p is labeled as P unless specified otherwise.

3

Explicit and Implicit Flows An information flow analysis prohibits any explicit or implicit information flow that is inconsistent with the given policy. Explicit flows take place when confidential
data are passed directly to public variables, such as the command p := s, while implicit flows arise
from the control structure of the program. For example, the following program has an implicit
flow:
if (s = 0) then p := 0 else p := 1
Assume the secret variable s is either 0 or 1. This code is insecure since it is functionally
equivalent to p := s. That is, the confidential data s is copied to a public variable p.
An information flow security system rules out all explicit and implicit flows; any violation
of a given security policy results in an error. As in most information flow analyses, we do not
consider timing, termination and other side channels in this paper; controlling side channel leakage
(e.g., [1, 28, 43]) is largely an orthogonal issue.

2.2

Sources of Imprecision

Most information flow analyses provide soundness (i.e., if the analysis determines that a program
is secure, then the program provably prevents disclosure of sensitive data). However, since the
problem of checking information flow security is in general undecidable [37], one key challenge
of designing an information flow analysis is to maintain soundness, while improving precision
(i.e., reject fewer secure programs).
In this section, we introduce the major sources of imprecision in existing type systems. In the
next section (Section 2.3), we illustrate how does our novel information flow analysis alleviate
those sources of imprecision.
Flow-Insensitivity The first source of imprecision is flow-insensitivity, meaning that the order of
execution is not taken into account in a program analysis [34]. In the context of information flow
analysis, the intuition is that an analysis is flow-insensitive if a program is analyzed as secure only
when every subprogram is analyzed as secure [26].
Many security type systems, including [32, 35, 40], are flow-insensitive. Consider the program
in Figure 1(a) (for now, ignore the brackets). This program is secure since the public variable p
has a final value zero regardless of the secret variable s. However, it is considered insecure by a
flow-insensitive analysis because of the insecure subprogram (x := s; p := x; ). Under the hood,
the imprecision arises since the analysis requires fixed levels: the security level of a variable must
remain the same throughout the program execution. But in this example, these is no fixed-level for
the variable x: when the level is S, p := x is insecure; when the level is P, x := s is insecure.
Path-Insensitivity The second source of imprecision is path-insensitivity, meaning that the predicates at conditional branches are ignored in a program analysis [34]. In the context of information
flow analysis, the intuition is that an analysis is path-insensitive if a program is analyzed as secure only when every sequential program generated from one combination of branch outcomes is
analyzed as secure.
For instance, the flow-sensitive type system in [26] is path-insensitive; consequently, it rejects
the secure program shown in Figure 1(c) (due to Le Guernic and Jensen [29]). This example
is secure since the value of the secret variable s never flows to the public variable p2 , since the
4

assignments y := s and x := y never execute together in the same program execution. However, the
type system in [26] rejects this program because it lacks the knowledge that the two if-statements
cannot take the “then” branch in the same execution. Hence, it has to conservatively analyze the
security of an impossible program execution: x := 0; y := 0; y := s; x := y; p := x, which is
insecure due to an explicit flow from s to p.
Under the hood, we observe that the imprecision arises from the fact that a path-insensitive
analysis (e.g., [26]) requires that the security levels of a variable on two paths to be “merged” (as
the least upper bound) after a branch. Consider the first branch in Figure 1(c). The “then” branch
requires y to be S due to the flow from s to y. So after that if-statement, the label of y must be S
(i.e., which path is taken is unknown to the rest of the program). Similarly, x has label S after the
second if-statement. Hence, p2 := x is rejected due to an explicit flow from S to P.

2.3

Overview

In order to alleviate analysis imprecision due to flow- and path-insensitivity, our novel information
flow analysis has two major components: a program transformation that enables flow-sensitivity
and a type system with dependent security labels, which enables path-sensitivity.
2.3.1

Program Transformation

Consider the example in Figure 1(a) (for now, ignore the brackets). A fixed-level type system
rejects this program since the levels of x at line 1 and 3 are inconsistent. We observe that there
are indeed two copies of x in this program but only the final one (defined at line 2) is released. So
without modifying a type system, we can explicitly transform the source program to a semantically
equivalent one that explicitly marks different copies.
The source language of our program analysis (Section 3) provides a tunable knob for improved
precision: a bracketed assignment in the form of Jx := eK. Such an assignment is semantically
identical to x := e but allows a programmer to request improved precision (the source language
allows such flexibility since reduced precision might be preferred for reasons such as more efficient analysis on the program). In particular, for a bracketed assignment Jx := eK, the program
transformation (Section 4) generates a fresh copy for x and uses that copy in the rest of program
until another new copy is generated. For example, given the bracketed assignment at line 2 of
Figure 1(a), the transformed program is shown in Figure 1(b), where the second definition of x
and its use at line 3 are replaced with x1 . The benefit is that the false dataflow dependency from
s to p in the source program is eliminated. Hence, the transformed program can be accepted by a
fixed-level type system, by assigning x and x1 to levels S and P respectively. In general, we prove
that (when all assignments are bracketed) the transformation enables a fixed-level system to be at
least as precise as a classic flow-sensitive type system (Section 7).
2.3.2

Dependent Labels

Consider the example in Figure 1(c). A path-insensitive type system rejects this program since
such a type system ignores the path conditions under which assignments occur. Consequently, the
security level of y is conservatively estimated as S after line 2, though when p1 ≥ 0, variable y
only carries public information.
5

Vars
Expr
Cmds

x, y, z ∈ Vars
e ::= x | n | e op e
c ::= skip | c1 ; c2 | x := e | Jx := eK |
if (e) then c1 else c2 | while (e) c
Figure 2: Syntax of the Source Language.

In our system, path-sensitivity is gained via dependent security labels (i.e., security labels
that depend on program states). Compared with a security level drawn directly from a lattice, a
dependent security label precisely tracks all possible security levels from different branches; hence,
path-sensitivity is gained. Since dependent security labels are orthogonal to bracketed assignments,
extra precision can be gained in our system even in the absence of bracketed assignments. For
example, while the program in Figure 1(c) can not be accepted using any simple security level for
y, we can assign to y a dependent label (p1 < 0?S : P), which specifies an invariant that the level
of y is S when p1 < 0 (i.e., the “then” branch is taken at line 2); the level is P otherwise. Such
an invariant can be maintained by the type system described in Section 5. For instance, to ensure
that the explicit flow from y to x at line 3 is secure, the type system generates a proof obligation
(p1 > 0 ⇒ (p1 < 0?S : P) v P), meaning that the information flow from y to x must be permissible
under the path condition p1 < 0. This proof obligation can easily be discharged by an external
solver. The soundness of our type system (Section 6) guarantees that all security violations are
detected at compile time.

3

Language Syntax and Semantics

In this paper, we consider a simple imperative WHILE language whose syntax and operational
semantics are shown in Figures 2 and 3 respectively. The syntax and semantics are mostly standard:
expressions e consist of variables x, integers n, and composed expressions e op e, where op is a
binary arithmetic operation. Commands c consist of standard imperative instructions, including
skip, sequential composition c1 ; c2 , assignments, conditional if branch and while loop. The
semantics of expressions are given in the form of he, mi ⇓ n (big-step semantics), where memory
m maps variables to their values. The small-step semantics of commands has the form of hc, mi →
hc0 , m0 i, where hc, mi is a configuration. We use m{x 7→ n} to denote the memory that is identical
to m except that variable x is updated to the new value n.
The only interesting case is the bracketed assignment Jx := eK, which is semantically equivalent to normal assignment x := e in the source language. These commands are tunable knobs for
improved precision in our information flow analysis, as we show shortly.

4

Program Transformation

To alleviate the imprecision due to flow-insensitivity, one component of our analysis is a novel
program transformation that introduces extra variable copies to the source program, so that false
dataflow dependencies that otherwise may confuse flow-insensitive analyses are removed.
6

hn, mi ⇓ n

he1 , mi ⇓ n1
n = n1 op n2
he2 , mi ⇓ n2
he1 op e2 , mi ⇓ n

hx, mi ⇓ m(x)

S-A SSIGN

S-S KIP

hskip; c, mi → hc, mi

he, mi ⇓ n
hx := e, mi → hskip, m{x 7→ n}i
S-S EQ

S-A SSIGN -B RACKET

hc1 , mi → hc01 , m0 i
hc1 ; c2 , mi → hc01 ; c2 , m0 i

he, mi ⇓ n
hJx := eK, mi → hskip, m{x 7→ n}i
S-W HILE

hwhile (e) c, mi → hif (e) then (c; while (e) c) else skip, mi
S-I F 1

S-I F 2

he, mi ⇓ n n 6= 0
hif (e) then c1 else c2 , mi → hc1 , mi

he, mi ⇓ n n = 0
hif (e) then c1 else c2 , mi → hc2 , mi

Figure 3: Semantics of the Source Language.

4.1

Bracketed Assignments and the Transformed Program

We propose a general and flexible design for the program transformation. In particular, the program
transformation is triggered only for assignments that are marked with brackets. Such a design enables a tunable control of analysis precision for programmers or high-level program analysis built
on our meta source language: when there is no bracketed assignment, the transformed program
is simply identical to the source program; when all assignments have brackets, the transformation
generates a fresh copy of x for each bracketed assignment Jx := eK.
Due to the nature of the transformation, the transformed program follows the same syntax and
semantics as the source language, except that all bracketed assignments are removed.
To avoid confusion, we use underlined notations for the transformed program: e for expressions, c for commands and m for memories, when both the original and the transformed programs
are in the context; otherwise, we simply use e, c and m for the transformed programs as well.

4.2

Transformation Rules

The program transformation maintains one active copy for each variable in the source code. One
invariant maintained by the transformation is that for each program point, there is exactly one
active copy for each source-program variable. Intuitively, that unique active copy holds the most
recent value of the corresponding source-program variable.
Definition 1 (Active Set) An active set A : Vars 7→ Vars, is an injective function that maps a
source variable to a unique variable in the transformed program.
7

hn, Ai V n

he1 , Ai V e01 he2 , Ai V e02
he1 op e2 , Ai V e01 op e02

hx, Ai V A(x)

TRSF-A SSIGN

TRSF-S KIP

hskip, Ai V hskip, Ai

he, Ai V e
hx := e, Ai V hx := e, A{x 7→ x}i

TRSF-A SSIGN -C REATE

TRSF-S EQ

he, Ai V e i is a fresh index for x
hJx := eK, Ai V hxi := e, A{x 7→ xi }i

hc1 , Ai V hc1 , A1 i hc2 , A1 i V hc2 , A2 i
hc1 ; c2 , Ai V hc1 ; c2 , A2 i

TRSF-I F

he, Ai V e hc1 , Ai V hc1 , A1 i hc2 , Ai V hc2 , A2 i Φ(A1 , A2 ) V A3
hif (e) then c1 else c2 , Ai V hif (e) then (c1 ; A3 := A1 ) else (c2 ; A3 := A2 ), A3 i
TRSF-W HILE

hc, Ai V hc1 , A1 i Φ(A, A1 ) V A2 hc, A2 i V hc, A3 i he, A2 i V e
hwhile (e) c, Ai V hA2 := A; while (e) (c; A2 := A3 ), A2 i
Figure 4: Program Transformation. We use A := A0 as a shorthand for {A(v) := A0 (v) | v ∈
Vars ∧ A(v) 6= A0 (v)}.

(
xi , i fresh for x, A1 (x) 6= A2 (x)
merge(A1 , A2 ) = λx.
A1 (x),
A1 (x) = A2 (x)
A3 = merge(A1 , A2 )
TRSF-P HI
Φ(A1 , A2 ) V A3
Figure 5: Merge Function.

8

For simplicity, we assume that the variables in the transformed program follow the naming
convention of xi where x ∈ Vars and i is an index. Hence, for any variable v in the range of A,
we simply use v  to denote its corresponding source variable (i.e., a variable without the index).
Hence, v = A(v ) always holds by definition. Moreover, since we frequently refer to the range
of A, we abuse the notation of A to denote active copies that A may map to (i.e., the range of A).
That is, we simply write v ∈ A instead of v ∈ Ran(A) in this paper. Moreover, we use A{x 7→ xi }
to denote an active set that is identical to A except that x is mapped to xi .
The transformation rules are summarized in Figure 4. For an expression e, the transformation
has the form of he, Ai V e, where e is the transformed expression. The transformation of an
expression simply replaces the source variables with their active copies in A.
For a command c, the transformation has the form of hc, Ai V hc, A0 i, where c is the source
command and c is the transformed one. Since assignments may update the active set, A0 represents
the active set after c.
Rule (TRSF-Assign) applies to a normal assignment. It transforms the assignment to one with
the same assignee and update A accordingly. Rule (TRSF-Assgin-Create) applies to a bracketed
assignment Jx := eK. It renames the assignee to a fresh variable. For example, line 1 of the
transformed program in Figure 1(b) is exactly the same as the original program in 1(a); but the
assignee of line 2 is renamed to x1 . Rule (T RSF -I F ) uses a special Φ function, defined in Figure 5,
to merge the active sets generated from the branches. In particular, Φ(A1 , A2 ) V A3 generates
an active set A3 that maps x to a fresh variable iff A1 (x) 6= A2 (x). Transformation for the while
loop is a little tricky since we need to compute an active set that is active both before and after
each iteration. Rule (TRSF-W HILE ) shows one feasible approach: the rule transforms the loop
in a way that A1 is a fixed-point: the active set is always A1 before and after an iteration by the
transformation.
We note that given an identity function as the initial active set A, a program without any
bracketed assignment is transformed to itself with a final active set A. At the other extreme,
the transformation generates one fresh active copy for each assignment when all assignments are
bracketed.

4.3

Correctness of the Transformation

One important property of the proposed transformation is its correctness: a transformed program
is semantically equivalent to the source program. To formalize this property, we need to build an
equivalence relation on the memory for the source program (m : Vars → N) and the memory
for the transformed program (m : Vars → N). We note that the projection of m on an active
set A defined as follows shares the same domain and range as m. Hence, it naturally specifies an
equivalence relation on m and m w.r.t. A: m can be directly compared with mA .
Definition 2 (Memory Projection on Active Set) We use mA to denote the projection of m on
the active set A, defined as follows:
∀x ∈ Vars. mA (x) = m(A(x))
We formalize the correctness of our transformation as the following theorem. As stated in the
theorem, the correctness is not restricted to any particular initial active set A.
9

Theorem 1 (Correctness of Transformation) Any transformed program is semantically equivalent to its source:
∀c, c, m, m, m0 , m0 , A, A0 .
hc, Ai V hc, A0 i ∧ hc, mi →∗ hskip, m0 i
∧ hc, mi →∗ hskip, m0 i ∧ m = mA
0

⇒ m0 = (m0 )A .
Proof sketch. By induction on the transformation rules. The full proof is available in Appendix A.

4.4

Relation to Information Flow Analysis

Up to this point, it might be unclear why introducing extra variables can improve the precision of
information flow analysis. We first note that transformed programs enable more precise reasoning
for dataflows. Consider the program in Figure 1(a) and Figure 1(b). In the transformed program,
it is clear that the value stored in x never flows to variable p; but such information is not obvious
in the source program. Moreover, Theorem 1 naturally enables a more precise analysis of the
transformed program, since it implies that if any property holds on the final active set A0 for the
transformed program, then the property holds on the entire final memory for the original program.
That is, in terms of information flow security, the original program leaks no information if the
transformed program leaks no information in the subset A0 of the final memory. Consider the
example in Figure 1(b) again. Theorem 1 allows a program analysis to accept the (secure) program
even though the variable x, which is not in A0 , may leak the secret value.
In Section 7, we show that, in general, the program transformation automatically makes a
flow-insensitive type system (e.g., the Volpano, Smith and Irvine’s system [40] and the system in
Section 5) at least as precise as a classic flow-sensitive type system [26].

4.5

Relation to Single Static Assignment (SSA)

SSA [17] is used in the compilation chain to improve and simplify dataflow analysis. Viewed
in this way, it is not surprising that our program transformation shares some similarity with the
standard SSA-transformation. However, our transformation is different from the latter in major
ways:
• Most importantly, our transformation does not involve the distinguishing φ-functions of
SSA. First of all, removing φ-functions simplifies the soundness proof, since the resulting target language syntax and semantics are completely standard. Moreover, it greatly
simplifies information flow analysis on the transformed programs. Intuitively, the reason is
that in the standard SSA from, the φ-function is added after a branch (i.e., in the form of
(if (e) then c1 else c2 ); x := φ(x1 , x2 )). However, without a nontrivial program analysis
for the φ-function, the path conditions under which x := x1 and x := x2 occur (needed for
path-sensitivity) is lost in the transformed program. On the other hand, extra assignments are
inserted under the corresponding branches in our transformation. The consequence is that
the path information is immediately available for the analysis on the transformed program.
10

We defer a more detailed discussion on this topic to Section 5.6, after introducing our type
system.
• As discussed in Section 4.4, the final active set A0 generated from the transformation is crucial for enabling a more precise program analysis on the transformed program (intuitively, an
information flow analysis may safely ignore variables not in A0 ); however, such information
is lost in the standard SSA form.
• Our general transformation offers a full spectrum of analysis precision: from adding no
active copy to adding one copy for each assignment, but the standard SSA transformation
only performs the latter.

5

Type System

The second component of the analysis is a sound type system with expressive dependent labels.
The type system analyzes a transformed program along with the final active set; the type system
ensures that the final values of the public variables in the final active set are not influenced by the
initial values of secret variables.

5.1

Overview

We first introduce the nonstandard features in the type system: dependent security labels and
program predicates.
Return to the example in Figure 1(c). We observe that this program is secure because: 1) y
holds a secret value only when p1 < 0, and 2) the information flow from y to x at line 3 only
occurs when p1 > 0. Accordingly, to gain path-sensitivity, two pieces of information are needed
in the type system: 1) expressive security labels that may depend on program states, and 2) an
estimation of program states that may reach a program point.
We note that such information can be gained by introducing dependent security labels and
program predicates to the type system. For the example in Figure 1(c), the relation between the
level of y and the value of x can be described as a concise dependent label (p1 < 0?S : P), meaning
that the security level of x is S when p1 < 0; the level is P otherwise. Moreover, for precision,
explicit and implicit flows should only be checked under program states that may reach the program
point. In general, a predicate overestimates such states. For the example in Figure 1(c), checking
that the explicit flow from y to x is secure under any program state is too conservative, since it
only occurs when p1 > 0. With a program predicate that p1 > 0 for the assignment x := y, the
label of y can be precisely estimated as P. Note that our analysis agrees with the definition of
path-sensitivity: it understands that the two assignments y := s and x := y; never execute together
in one execution. The example in Figure 1(c) is accepted by our type system.

5.2

Challenge: Statically Checking Implicit Declassification

Though designing a dependent security type system may seem simple at the first glance, handling
mutable variables can be challenging. The implicit declassification problem, as defined in [44],
occurs whenever the level of a variable changes to a less restrictive one, but its value remains the
11

1
2
3
4
5
6
7

x := 0; y := 0;
if (p1 < 0) then
y := s;
Jp1 := 1K;
if (p1 > 0) then
x := y;
p2 := x;
(a) Insecure Program.

x := 0; y := 0;
if (p1 < 0) then
y := s;
p3 := 1;
if (p3 > 0) then
x := y;
p2 := x;

1
2
3
4
5
6
7

(b) Transformed Program of 6(a).

Figure 6: Examples: Implicit Declassification.
same. Consider the insecure program in Figure 6(a), which is identical to the secure program in
Figure 1(c) except for line 4. This program is obviously insecure since the sequence y := s; p1 :=
1; x := y; p2 := x; may be executed together. Compared with Figure 1(c), the root cause of this
program being insecure is that at line 4 (when p1 is updated), y’s new level P (according to the
label p1 < 0?S : P) is no longer consistent with the value it holds.
The type systems in [23, 44] resort to a run-time mechanism to tackle the implicit declassification problem. However, that also means that the type system might change the semantics of the
program being analyzed. In this paper, we aim for a purely static solution.
Program Transformation and Implicit Declassification Although the program transformation
in Section 4 is mainly designed for flow-sensitivity, we observe that it also helps to detect implicit
declassification. Consider the example in Figure 6(a) again, where the assignment at line 4 has
brackets. The corresponding transformed program (Figure 6(b)) does not have an implicit declassification problem since updating p3 at line 4 does not change y’s level, which depends on the value
of p1 , rather than p3 . Moreover, the insecure program cannot be type-checked since both “then”
branches might be executed together.
While adding extra variable copies helps in the previous example, it unfortunately does not
eliminate the issue. The intuition is that even for a fully-bracketed program, variables modified in
a loop might still be mutable (since the local variables defined in the loop might change in each
iteration). Consider the program in 7(a). This program is insecure since it copies s to y in the first
iteration, and copies y to p in the next iteration. When fully-bracketed, the loop body becomes
if (x2 %2 = 0) then y1 := s; y3 := y1 else . . .;
x3 := x2 + 1; x2 := x3 ; y2 := y3 ;
where the labels of y1 and y3 depend on x2 . In this program, implicit declassification happens
when x2 is updated.
One naive solution is to disallow mutable variables in a program. However, dependence on
mutable variables does not necessarily break security. Consider the program in Figure 7(b), which
is identical to the previous example except that y is updated at line 8. In this program, y’s level
depends on the mutable variable x, but it is secure since the value of s never flows to the next
iteration.
Our Solution Our insight is that changing y’s level at line 7 in Figure 7(b) is secure since the
value of y is not used in the future (in terms of dataflow analysis, y is dead after line 6). This
12

1 x = 0;
2 while (x < 10) {
3
if (x%2 = 0) then
4
y := s;
5
else
6
p := y;
7
x := x + 1;
8 }
(a) Insecure Program.

1 x = 0;
2 while (x < 10) {
3
if (x%2 = 0) then
4
y := s;
5
else
6
p := y;
7
x := x + 1;
8
y := 0;
9 }
(b) Secure Program.

Figure 7: Examples: Implicit Declassification in Loop.
Level
Label

`∈L
τ ::= ` | e?τ1 : τ2 | τ1 t τ2 | τ1 u τ2
Figure 8: Syntax of Security Labels.

observation motivates us to incorporate a customized liveness analysis (Section 5.4) into the type
system: an update to a variable x is allowed if no labels of the live variables at that program point
depend on x.

5.3

Type Syntax and Typing Environment

In our type system, types are extended with security labels, whose syntax is shown in Figure 8. The
simplest form of label τ is a concrete security level ` drawn from a security lattice L. Dependent
labels, specifying levels that depend on run-time values, have the form of (e?τ1 : τ2 ), where e is
an expression. Semantically, if e evaluates to a non-zero value, the dependent label evaluates to τ1 ,
otherwise, τ2 . A security label can also be the least upper bound, or the greatest lower bound of
two labels.
We use Γ to denote a typing environment, a function from program variables to security labels. The integration of dependent labels puts constraints on the typing environment Γ to ensure
soundness. In particular, we say Γ is well-formed, denoted as ` Γ, if: 1) no variable depends on
a more restrictive variable, preventing leakage from labels; 2) there is no chain of dependency.
These restrictions are formalized as follows, where FV(τ ) denotes the free variables in τ :
Definition 3 (Well-Formedness) A typing environment Γ is well-formed, written ` Γ, if and only
if:
∀x ∈ Vars. (∀x0 ∈ FV(Γ(x)). Γ(x0 ) v Γ(x))
∧(∀x0 ∈ FV(Γ(x)). FV(Γ(x0 )) = ∅)
We note that the definition rules out self-dependence, since if x ∈ FV(Γ(x)), we have FV(Γ(x)) =
∅. Contradiction.

13

LIVEout [final] = A
LIVEin [s] = GEN[s] ∪ (LIVEout [s] − KILL[s])
[
LIVEout [s] =
LIVEin [p]
p∈succ[s]

GEN[x :=η e] = FV(e) ∪ (

[

FV(Γ(v)))

v∈FV(e)

KILL[x :=η e] = {x}
Figure 9: Liveness Analysis of ŁA .

5.4

Predicates and Variable Liveness

Our type system is parameterized on two static program analyses: a predicate generator and a customized liveness analysis. Instead of embedding these analyses into our type system, we follow
the modular design introduced in [44] to decouple program analyses from the type system. Consequently, the soundness of the type system is only based on the correctness of those analyses,
regardless of the efficiency or the precision of those analyses.
Predicate Generator We assume a predicate generator that generates a (conservative) program
predicate for each assignment η in the transformed program, denoted as P(η). A predicate generator is correct as long as each predicate is always true when the corresponding assignment is
executed.
A variety of techniques, regarding the trade-offs between precision and complexity, can be used
to generate predicates that describe the run-time state. For example, weakest preconditions [21] or
the linear propagation [44] could be used. Our observation is that for path-sensitivity, only shallow
knowledge containing branch conditions is good enough for our type system.
Liveness Analysis Traditionally, a variable is defined as alive if its value will be read in the
future. But in our type system, if a variable x is alive, then any free variable in the label of x
should also be considered as alive, because the concrete level of x depends on those variables.
Moreover, we assume at the end of a program, only the variables in the final active set are alive,
due to Theorem 1.
The liveness analysis is defined in Figure 9, where s denotes a program command, and final
refers to the last command of the program being analyzed. Here, final is the initial state for the
backward dataflow analysis. succ[s] returns the successors
(as a set) of the command s. In the
S
GEN set of an assignment x := e, both FV(e), and v∈FV(e) FV(Γ(v)), the free variables inside their
labels, are included. Since we are analyzing the transformed program, the state of the final active
set is crucial for precision. Therefore, the analysis also enforces that, at the end of the program, all
active copies in A are alive. Other rules are standard for liveness analysis.
Interface to the Type System We assume each assignment in the transformed language is associated with a unique identifier η. We use •η and η• to denote the precise program points right

14

Γ(x) = τ
T-VAR
Γ`x:τ

T-C ONST

Γ`n:⊥

Γ ` e : τ1
Γ ` e0 : τ2
T-O P
Γ ` e op e0 : τ1 t τ2

Figure 10: Typing Rules: Expressions.

Γ, pc ` skip

Γ, pc ` c1 Γ, pc ` c2
T-S EQ
Γ, pc ` c1 ; c2

T-S KIP

Γ ` e : τ Γ, τ t pc ` c1 Γ, τ t pc ` c2
T-I F
Γ, pc ` if (e) then c1 else c2
Γ`e:τ

|= P(•η) ⇒ τ t pc v Γ(x) ∀v ∈ ŁA (η•).x 6∈ FV(Γ(v))
T-A SSIGN
Γ, pc ` x :=η e
Γ ` e : τ Γ, τ t pc ` c
T-W HILE
Γ, pc ` while (e) c
Figure 11: Typing Rules: Commands.

before and after the assignment respectively. For example, P(•η) represents the predicates right
before statement η, and ŁA (η•) denotes the alive set right after statement η with initialization of A
as the final live set.

5.5

Typing Rules

The type system is formalized in Figure 10 and Figure 11. Typing rules for expressions have the
form of Γ ` e : τ , where e is the expression being checked and τ is the label of e. The typing
judgment of commands has the form of Γ, pc ` c. Here, pc is the usual program-counter label [37],
used to control implicit flows.
Most rules are standard, thanks to the modular design of our type system. The only interesting
one is rule (T-A SSIGN ). For an assignment x :=η e, this rule checks that both the explicit and
implicit flows are allowed in the security lattice: τ t pc v Γ(x). Note that since τ might be a
dependent label that involves free program variables, the v relation is technically the lifted version
of the relation on the security lattice. Hence, the constraint τ t pc v Γ(x) requires the label of
x to be at least as restrictive as the label of current context pc and the label e under any program
execution. For precision, the type system validates the partial ordering under the predicate P(•η),
the predicate that must hold for any execution that reaches the assignment.
Moreover, the assignment rule checks that for any variable in the liveness set after the assignment, its security label must not depend on x; otherwise, its label might be inconsistent with its
value. As discussed in Section 5.2, this check is required to rule out insecure implicit declassification.
At the top level, the type system collects proof obligations in the form of |= P ⇒ τ1 v τ2 ,
where τ1 and τ2 are security labels, and P is a predicate. Such proof obligations can easily be
15

discharged by theorem solvers, such as Z3 [19].
As an example, consider again the interesting examples in Figure 7. In both programs, we can
assign y to the dependent label (x%2 = 0?S : P), and assign x to the label P. From the liveness
analysis, we know that the live sets right after line 7 are {x, y, s} and {x, p, s} for Figure 7(a)
and Figure 7(b) respectively. Hence, the type system correctly rejects the insecure program in
Figure 7(a) since the check at line 7, ∀v ∈ ŁA (η•). x 6∈ FV(Γ(v)), fails. On the other hand, the
check at line 7 succeeds for the program in Figure 7(b). For line 4 in Figure 7(b), the assignment
rule generates one proof obligation
|= (x%2 = 0) ⇒ P t S v (x%2 = 0?S : P)
which is clearly true for any value of x. In fact, the secure program in Figure 7(b) is correctly
accepted by the type system in Figure 10 and Figure 11.

5.6

Program Transformation and Information Flow Analysis

We now discuss the benefits of the program transformation in Section 4 for information flow analysis in details.
5.6.1

Simplifying Information Flow Analysis

As discussed in Section 4.5, our transformation does not involve the distinguishing φ-functions of
SSA. Doing so simplifies information flow analysis on the transformed programs. We illustrate
this using the following example, where y is expected to have the label (x = 1?P : S) afterwards.
if (x = 1) then y := 0 else y := s
Our transformation yields the following program, which can be verified with labels y1 : P, y2 : S,
y3 : (x = 1?P : S).
if (x = 1) then (y1 := 0; y3 := y1 )
else (y2 := s; y3 := y2 );
In comparison, the standard SSA form is:
(if (x = 1) then y1 := 0 else y2 := s; )y3 := φ(y1 , y2 );
To verify this program, a type system would need at least a nontrivial typing rule for φ, which
somehow “remembers” that y3 := y2 occurs only when x = 1. Even with such knowledge, the
type of y2 cannot simply be S, since otherwise, assigning y2 to y3 at φ is insecure. In fact, the labels
required for verification are y1 , y2 , y3 : (x = 1?S : P).
Similar complexity is also involved for the φ-functions inserted for loops: to precisely reason
about information flow, the semantics and typing rules of φ also need to track the number of
iterations.
5.6.2

Improving Analysis Precision

Precision-Wise, bracketed assignments improve analysis precision in two ways. First, as discussed
in Section 4.4, they improve flow-sensitivity by introducing new variable definitions. Second,
they also improve path-sensitivity by enabling more accurate program predicates. Consider the
following example.
16

x := −1;
if (x > 0) then y := S; else y := 1;
Jx := −xK;
if (x > 0) then p := y;
This program is secure since p becomes 1 regardless of the value of s. However, without the bracket
shown, the type system rejects it since no such label τy satisfies the constraints that (x > 0) ⇒
(S v τy ) (arising from the first if) and (x > 0) ⇒ (τy v P) (arising from the second if).
However, with the bracket, the last two lines become
x1 := −x;
if (x1 > 0) then p := y;
This program can be type-checked with y’s label as (x > 0?S : P) and a precise enough predicate
generator, which generates x1 = −x after the assignment x1 := −x, because constraints (x >
0) ⇒ (S v τy ) and (x1 > 0 ∧ x1 = −x) ⇒ (τy v P) can be solved with y’s label mentioned
above.

6

Soundness

Central to our analysis is rigorous enforcement of a strong information security property. We formalize this property in this section and sketch a soundness proof. The complete proof is available
in Appendix B.

6.1

Noninterference

Our formal definition of information flow security is based on noninterference [24]. Informally,
a program satisfies noninterference if an attacker cannot observe any difference between two program executions that only differ in their confidential inputs. This intuition can be naturally expressed by semantics models of program executions.
Since a security label may contain program variables, its concrete level cannot be determined
statically in general. But it can always be evaluated under a concrete memory:
Definition 4 For a security label τ , we evaluate its concrete level under memory m as follows:
V(τ, m) = `, where hτ, mi ⇓ `
Moreover, to simplify notation, we use TΓ (x, m) to denote the concrete level of x under m and
Γ (i.e., TΓ (x, m) = V(Γ(x), m)).
To formally define noninterference in the presence of dependent labels, we first introduce an
equivalence relation on memories. Intuitively, two memories are (Γ, `)-equivalent if all variables
with a level below level ` agree on both their concrete levels and values.
Definition 5 ((Γ, `)-Equivalence) Given any concrete level ` and Γ, we say two memories m1 and
m2 are equivalent up to ` under Γ (denoted by m1 ≈`Γ m2 ) iff
∀x ∈ Vars.
(TΓ (x, m1 ) v ` ⇐⇒ TΓ (x, m2 ) v `) ∧ TΓ (x, m1 ) v `
=⇒ m1 (x) = m2 (x)
17

It is straightforward to check that ≈`Γ is an equivalence relation on memories. Note that we
require type of x be bounded by ` in m2 whenever TΓ (x, m1 ) v `. The reason is to avoid label
channels, where confidential data is leaked via the security level of a variable [36, 44].
Given initial labels Γ on variables and final labels Γ0 on variables, we can formalize noninterference as follows:
Definition 6 (Noninterference) We say a program c satisfies noninterference w.r.t. Γ, Γ0 if equivalent initial memories produce equivalent final memories:
∀m1 , m2 , `.
m1 ≈`Γ m2 ∧ hc, m1 i →∗ hskip, m01 i ∧
hc, m2 i →∗ hskip, m02 i
=⇒ m01 ≈`Γ0 m02
The main theorem of this paper is the soundness of our analysis: informally, if the transformed
program type-checks, then the original program satisfies noninterference. Since the type system
applies to the transformed program, we first need to connect the types in the original and the
transformed programs. To do that, we define the projection of types for the transformed program
in a way similar to Definition 2:
Definition 7 (Projection of Types) Given an active set A and Γ, types of variables in the transformed program, we use ΓA to denote a mapping from Vars to τ as follows:
∀v ∈ Vars. ΓA (v) = Γ(A(v))
Formally, the soundness theorem states that if a program c under active set A (e.g., an identity
function) is transformed to c and final active set A0 , and c is well-typed under the type system
0
(parameterized on A0 ), then c satisfies noninterference w.r.t. ΓA and ΓA :
Theorem 2 (Soundness)
∀c, c, m1 , m2 , m01 , m02 , `, Γ, A, A0 .
hc, Ai V hc, A0 i∧ ` Γ ∧ Γ ` c ∧ m1 ≈`ΓA m2 ∧
hc, m1 i →∗ hskip, m01 i ∧ hc, m2 i →∗ hskip, m02 i
=⇒ m01 ≈`ΓA0 m02
To approach a formal proof, we notice that by the correctness of the program transformation
(Theorem 1), it is sufficient to show that the transformed program leaks no information on the subset A0 . Such connection is illustrated in Figure 12. We formalize the soundness for the transformed
program w.r.t. initial and final active sets as follows:
Theorem 3 (Soundness of Transformed Program)
∀c, m1 , m2 , m3 , m4 , `, Γ, A, A0 .
`
A
hc, Ai V hc, A0 i∧ ` Γ ∧ Γ ` c ∧ mA
1 ≈ΓA m2

∧ hc, m1 i →∗ hskip, m3 i ∧ hc, m2 i →∗ hskip, m4 i
0

0

`
A
=⇒ mA
3 ≈ΓA0 m4

18

<c, m2>
<c, m1>

<skip, m2’>
<skip, m1 >
’

<c, m2>
<c, m1>

Soundness
(Original)

<skip, m2’>
<skip, m1’>

Soundness
(Transformed)

Figure 12: Soundness of original and transformed programs.
(
0,
x ∈ FV(x0 ) ∧ x0 6∈ ŁA0 (η)
erase(m, x, η)(x0 ) =
m(x0 ), otherwise
hx, mi ⇓ n m0 = m{x 7→ n}
ST-E RASE
hx :=η e, mi →ER(A0 ) hskip, erase(m0 , x)i
Figure 13: Erasure Semantics of Assignment.
Proof sketch. One challenge in the formal proof is that the equivalence relation ≈`Γ only holds
on the active copies and it may break temporarily during the program execution. Consider the
example in Figure 7(b). During the first iteration of the loop body, y holds a secret value but
its level is P right after line 8. Hence, the relation ≈`Γ may break at that point in the small-step
evaluation starting from two memories that only differ in secrets. To tolerate such temporary
violation of the ≈`Γ relation, we prove the soundness with a new semantics which enforces that the
relation ≈`Γ holds for all variables, and the final values of variables in A0 agree with those in the
standard semantics. The new semantics, called the erasure semantics is shown in Figure 13. The
semantics is parameterized on the final active set A0 . The only difference from the standard one is
for assignments: the new assignment rule (ST-E RASE ) sets variables that are not alive and whose
types depend on x to be zero. It is easy to check that the erasure semantics agrees on the final
value of the variables in A0 . Also, it removes the temporary violation of the equivalence relation
by forcing value of y to be zero after line 7 of Figure 7(b). The complete proof is available in
Appendix B.

7

Enabling Flow-Sensitivity with Program Transformation

Recall that the dependent security type system (without program transformation) is flow-insensitive;
yet, our program analysis is flow-sensitive with the novel program transformation in Section 4. In
this section, we show that this is not a coincidence: the program transformation automatically
makes a flow-insensitive type system (e.g., the Volpano, Smith and Irvine’s system [40] and the
system in Section 5) flow-sensitive.

19

HS-S KIP

pc `HS Γ{skip}Γ
HS-A SSIGN

HS-I F

HS-W HILE

HS-S EQ

Γ `HS e : τ

pc `HS Γ{c1 }Γ00

pc `HS Γ{c1 ; c2 }Γ0

Γ `HS e : τ
pc `HS Γ{x := e}Γ{x 7→ pc t τ }

τ t pc `HS Γ{c1 }Γ1

τ t pc `HS Γ{c2 }Γ2

pc `HS Γ{if (e) then c1 else c2 }Γ0

Γ0i `HS e : τi

pc `HS Γ00 {c2 }Γ0

τi t pc `HS Γ0i {c}Γ00i

pc `HS Γ{while (e)

where Γ0 = Γ1 t Γ2

0≤i≤n

c}Γ0n

where Γ00 = Γ, Γ0i+1 = Γ00i tΓ, Γ0n+1 = Γ0n

Figure 14: The Hunt and Sands System [26].

7.1

The Hunt and Sands System

In [26], Hunt and Sands define a classic flow-sensitive type system where the security level of a
program variable may “float” in the program. In particular, Hunt and Sands (HS) judgments have
the form of pc `HS Γ{c}Γ0 , where Γ and Γ0 are intuitively the typing environments before and after
executing c respectively.
Consider the program in Figure 1(a). While a flow-insensitive type system rejects it, the HS
system accepts it with the following typing environments:
Γ{x := s; }Γ{x := 0; }Γ0 {p := x; }Γ0
where Γ = {x 7→ S, p 7→ P} and Γ0 = {x 7→ P, p 7→ P}.
The HS typing rules for commands are summarized in Figure 14. We use `HS to distinguish
those judgments from the ones in our system. The interesting rules are rule (HS-I F ) and rule (HSW HILE ): the former computes the type for each variable as the least upper bound of its labels in
the two branches; the latter computes the least fixed-point of a monotone function (the while loop)
on a finite lattice.

7.2

Program Transformation and Flow-Sensitivity

We show that the program transformation in Section 4 along with a flow-insensitive type system
subsumes the HS system: for any program c that can be type-checked in the HS system, the transformed program of JcK (i.e., a fully-bracketed program) can be type-checked in a flow-insensitive
type system. This result has at least two interesting consequences:
1. The program transformation removes the source of “flow-insensitivity”; a flow-insensitivity
type system can be automatically upgraded to a flow-sensitive one.
2. The flow- and path-sensitive system in this paper strictly subsumes the HS system: any
secure program accepted by the latter is accepted by the former, but not vise versa (e.g., the
program in Figure 1(c)).

20

C-S KIP

C-S EQ

(pc, Γ, A){skip V skip}(Γ, A) ,→ ΓA

(pc, Γ, A){c1 V c1 }(Γ00 , A00 ) ,→ Γ1 (pc, Γ00 , A00 ){c2 V c2 }(Γ0 , A0 ) ,→ Γ2
(pc, Γ, A){c1 ; c2 V c1 ; c2 }(Γ0 , A0 ) ,→ ∪(Γ1 , Γ2 )

C-A SSIGN

pc `HS Γ{x := e}Γ{x 7→ τ } hJx := eK, Ai V hxi := e, A{x 7→ xi }i
(pc, Γ, A){Jx := eK V xi := e}(Γ{x 7→ τ }, A{x 7→ xi }) ,→ ΓA ∪ {xi 7→ τ }

Γ `HS e : τ (τ t pc, Γ, A){c1 V c1 }(Γ1 , A1 ) ,→ Γ1
Φ(A1 , A2 ) V A3 Γ0 = Γ1 t Γ2
he, Ai V e (τ t pc, Γ, A){c2 V c2 }(Γ2 , A2 ) ,→ Γ2
C-I F
(pc, Γ, A){if (e) then c1 else c2 V if (e) then (c1 ; A3 := A1 ) else (c2 ; A3 := A2 )}(Γ0 , A3 ) ,→ ∪(Γ1 , Γ2 , Γ0A3 )
pc `HS Γ{while (e) c}Γ0
Φ(A, A1 ) V A2
hc, Ai V hc1 , A1 i
(τ t pc, Γ0 , A2 ){c V c}(Γ0 , A3 ) ,→ Γ0
Γ0 `HS e : τ
he, A2 i V e
C-W HILE
(pc, Γ, A){while (e) c V A2 := A; while (e) (c; A2 := A3 )}(Γ0 , A2 ) ,→ ∪(Γ0 , ΓA )

Figure 15: Type Construction in Transformed Program.
To construct types in the transformed program, we first introduce a few notations. Given a
typing environment Γ : Vars → τ for the original program and an active set A, we can straightforwardly construct a (minimal) typing environment, written ΓA , whose projection on A is Γ:
∀v ∈ A. ΓA (v) , Γ(v )
Easy to check that (ΓA )A = Γ.
Moreover, given a sequence of tying environments for the transformed program, say Γ1 , Γ2 , . . . ,
we define a merge function, denoted as ∪, that returns the union of Γ1 , Γ2 , . . . so that conflicts in the
environments are resolved in the order of Γ1 , Γ2 , . . . . For example, ∪({x1 7→ S, y2 7→ P}, {x1 7→
P, y2 7→ P}) = {x1 7→ S, y2 7→ P}.
For a fully bracketed program JcK, we can inductively define the construction of Γ as inference
rules in the form of
(pc, Γ, A){JcK V c}(Γ0 , A0 ) ,→ Γ
where pc, Γ, c, Γ0 are consistent with the HS typing rules in the form of pc `HS Γ{c}Γ0 ; A, JcK, A0 , c
are consistent with the program transformation rules in the form of hJcK, Ai V hc, A0 i. Γ is the
constructed typing environment that, as we show shortly in Theorem 4, satisfies Γ, pc ` c. The
construction algorithm is formalized in Figure 15.
Most parts of the rules are straightforward; they are simply constructed to be consistent with
the HS typing rules and the transformation rules in Figure 4. The following lemma makes such
connections explicit.
Lemma 1
∀pc, Γ, Γ0 , A, A0 , c, c. pc `HS Γ{c}Γ0 ∧ hJcK, Ai V hc, A0 i
⇒ ∃Γ. (pc, Γ, A){JcK V c}(Γ0 , A0 ) ,→ Γ
Proof. By induction on the structure of c.


21

To construct types for the transformed program: for skip, we use ΓA (the typing environment
before this command); for assignment, since xi must be fresh, we can simply augment ΓA with
{xi 7→ τ }. Other rules simply merge constructed types from subexpressions in a conflict-solving
manner, using ∪. An eagle-eyed reader may find the construction is intuitively correct if there is
no conflict at all in the merge operations.
We show that there is no conflict during construction by two observations. First, if a variable
has the same active copy before and after transforming a fully-bracketed command JcK, then its
type must remain the same (before and after c) in the HS system. This property is formalized as
follows:
Lemma 2
pc `HS Γ{c}Γ0 ∧ hJcK, Ai V hc, A0 i ⇒
∀v ∈ Vars. (A(v) = A0 (v)) ⇒ (Γ(v) = Γ0 (v))
Proof sketch. By induction on the structure of c. The most interesting cases are for branch and
loop.
• if (e) then c1 else c2 : by the HS typing rule, pc `HS Γ{c1 }Γ1 ∧ pc `HS Γ{c2 }Γ2 ∧ Γ0 =
Γ1 t Γ2 . By the transformation rules, hJci K, Ai V hci , Ai i, i ∈ {1, 2}. Suppose A(v) 6=
A1 (v), A1 (v) must be a fresh variable generated in c1 , and hence, cannot be in A2 . By the
definition of Φ, A3 (v) must be fresh. This contradicts the assumption A(v) = A0 (v). Hence,
Γ(v) = Γ1 (v) by the induction hypothesis. Similarly, we can infer that Γ(v) = Γ2 (v). So
Γ0 (v) = Γ1 (v) t Γ2 (v) = Γ(v).
• while (e) c: By rule (TRSF-W HILE ), we have hJcK, Ai V hc1 , A1 i, where A0 is A1 in this
case. Hence, by the assumption, we have A(v) = A1 (v). By rule (HS-W HILE ), there is a
sequence of environments Γ0i , Γ00i such that pc t τi ` Γ0i {c}Γ00i . By the induction hypothesis,
Γ00i (v) = Γ0i (v). Since Γ00 = Γ and Γ0i+1 = Γ t Γ00i in rule (HS-W HILE ), we can further infer
that Γ0i+1 (v) = Γ00i (v). Hence, we have Γ0 (v) = Γn (v) = Γ0 (v) = Γ(v).
Second, the constructed environment is minimal, meaning that it just specifies types for the
variables in A and the freshly generated variables in c (denoted as FVars(c)).
For technical reasons, we formalize this property along with the main correctness theorem of
the construction, stating that the transformed program c type-checks under the constructed environment Γ. Note that given any A, a fully bracketed command JcK always transforms to some c
and A0 . Hence, by Lemma 1, the following theorem is sufficient to show that our program analysis
is at least as precise as the HS system:
Theorem 4
∀c, c, pc, A, A0 , Γ, Γ0 , Γ. (pc, Γ, A){JcK V c}(Γ0 , A0 ) ,→ Γ
⇒ Dom(Γ) ⊆ A ∪ FVars(c) ∧ Γ, pc ` c
Proof. Complete proof is available in Appendix C.
22



An interesting corollary of Theorem 4 is that the transformed program can be type-checked
under the classic fixed-level system in [40] as well.
Corollary 1 Theorem 4 also applies to the type system in Figure 10 and Figure 11 with the restriction that all labels are security levels (i.e., non-dependent labels), which is identical to the system
in [40].
Proof. We note that the construction in Figure 15 only uses the non-dependent part of our type
system. Given all labels are security levels, it is straightforward to check that our type system
degenerates to the system in [40].

Theorem 4 has a strong prerequisite that all assignments in the original program are bracketed.
We note that the result remains true when such prerequisite is relaxed. Intuitively, a bracket is
unnecessary when the old and new definitions have the same security label. Otherwise, a bracket
is needed for flow-sensitivity. For example, to gain flow-sensitivity, only the second assignment
in Figure 1(a) needs a bracket. The strong prerequisite is used in Theorem 4 to make the result
general (i.e., type-agnostic).
According to Corollary 1, the result that any secure program accepted by the HS system is
accepted by our analysis is true even if all dependent security labels degenerate to simple security
levels. On the other hand, introducing dependent security labels makes our analysis strictly more
precise than the HS system. For example, the program in Figure 1(c) cannot be verified without
dependent security labels, but it can be type-checked with a label y : (p1 < 0?S : P).

7.3

Comparison with the transformation in [26]

Hunt and Sands show that if a program can be type-checked in the HS system, then there is
an equivalent program which can be type-checked by a fixed level system [26]. However, their
construction of the equivalent program is type guided, meaning that the program transformation
assumes that security labels have already been obtained in the HS system, while our program
transformation (Figure 4) is general and syntax-directed. An interesting application of our transformation is to test the typeability of the HS system without obtaining the types needed in the HS
system in the first place.
It is noteworthy that our transformation is arguably simpler than the HS transformation since
our rule for loop has no fixed-point construction while the latter has one. The reason is that compared with the HS transformation, the goal of our transformation is easier to achieve: our transformation improves analysis precision, while the HS transformation infers the type for each variable
in a program. For example, consider a loop with only one assignment x := x + 1, and x is initially
P. In the HS system, the transformed program is xP := xP + 1, where xP is the public version
of variable x. On the other hand, our transformation generates x1 := x2 ; x2 := x1 + 1. From the
perspective of inferring labels, introducing x1 and x2 might seem unnecessary since they must have
the same label according to the type system. However, doing so might improve analysis precision
(e.g., the type system can specify the dependencies on x1 and x2 separately with two copies of x).

23

8

Related Work

We refer to [37] for a comprehensive survey of static information flow analysis. Here, we focus on
the most relevant ones.
Dependent Labels and Information Flow Security Dependent types have been widely studied
and have been applied to practical programming languages (e.g., [7, 16, 31, 32, 41, 42]). New
challenges emerge for information flow analysis, such as precise, sound handling of information
channels arising from label changes.
For security type systems, the most related works are SecVerilog [23,44], Lourenço and Caires [30]
and Murray et al. [31]. SecVerilog is a Verilog-like language with dependent security labels for
verifying timing-sensitive noninterference in hardware designs. The type systems in [23, 44] are
not purely static: they remove implicit declassification by a run-time enforcement that modifies
program semantics. A recent extension to SecVerilog [22] alleviates such limitation by hardwarespecific static reasoning. However, those type systems do not handle loops (absent in hardware
description languages), which gives rise to new challenges for soundness. Moreover, they are
not flow-sensitive. The recent work [30] also allows the security type to depend on runtime values. However, the system is flow-insensitive, and it does not have a modular design that allows
tunable precision. Moreover, the language has limited expressiveness: it has no support for recursion, and it disallows dependence on mutable variables. Exploring dependent labels to their
full extent exposes new challenges that we tackle in this work, such as implicit declassification.
Murray et al. [31] present a flow-sensitive dependent security type system for shared-memory programs. The type system enforces a stronger security property: timing-sensitive non-interference
for concurrent programs. However, even when the extra complexity due to concurrency and timing
sensitivity are factored out, extra precision in their system is achieved via a floating type system
that tracks the typing environments and program states throughout the program. In comparison,
our analysis achieves flow-sensitivity via a separate program transformation, which results in an
arguably simpler type system. Moreover, for dependency on mutable variables, their system only
allows a variable’s security level to upgrade to a higher one, while our system allows a downgrade
to a lower level when doing so is secure.
Some prior type systems for information flow also support limited forms of dependent labels [25, 27, 32, 38, 39, 45]. The dependence on run-time program state, though, is absent in most
of these, and most of them are flow- and path-insensitive.
Flow-Sensitive Information Flow Analysis Flow-sensitive information flow control [8, 26, 36]
allows security labels to change over the course of computation. Those systems rely on a floating
type system or a run-time monitor to track the security labels at each program point. On the
other hand, the program transformation in our paper eliminates analysis imprecision due to flowinsensitivity. Moreover, the bracketed assignments in a source program provide tunable control
for needed analysis precision. These features offer better flexibility and make it possible to turn a
flow-insensitive analysis to be flow-sensitive.
Semantic-Based Information Flow Analysis Another direction of information flow security is
to verify the semantic definition of noninterference based on program logics. The first work that
24

1
2
3
4

x := 1; y := 1;
if (s == 0) then skip
else x := y;
p := x;

Figure 16: False Control-Flow Dependency.
used a Hoare-style semantics to reason about information flow is by Andrews and Reitman [5].
Independence analysis based on customized logics [2–4] was proposed to check whether two variables are independent or not. Self-Composition [9, 18] composes a program with a copy of itself,
where all variables are renamed. The insight is that noninterference of a program P can be reduced
to a safety property for the self-composition form of P .
Relational Hoare Logic [13] was first introduced for a core imperative program to reason about
the relation of two program executions. It was later extended to verify security proofs of cryptographic constructions [11] and differential privacy of randomized algorithms [10, 12]. In the
context of information flow security, Relational Hoare Type Theory [33] extends Hoare Type Theory and has been used to reason about advanced information flow policies.
Though some semantic-based information flow analyses are flow- and path-sensitive, most
mechanisms incur heavy annotation burden and steep learning curve on programmers. We believe
our approach shows that it is not necessary to resort to those heavyweight methods to achieve both
flow- and path-sensitivity.

9

Conclusions and Future Work

This paper presents a sound yet flow- and path-sensitive information flow analysis. The proposed
analysis consists of a novel program transformation as well as a dependent security type system that
rigorously controls information flow. We show that our analysis is both flow- and path-sensitive.
Compared with existing work, we show that our analysis is strictly more precise than a classic
flow-sensitive type system, and it tackles the tricky implicit declassification issue completely at
the compile time. Moreover, the novel design of our analysis allows a user to control the analysis
precision as desired. We believe our analysis offers a lightweight approach to static information
flow analysis along with improved precision.
The proposed analysis alleviates analysis imprecision due to data- and path-sensitivity, but it
still may suffer from other sources of imprecision, such as the presence of insecure dead code and
false control-flow dependency. For example, consider the secure program in Figure 16 (simplified
from an example in [14]) with security labels s : S, p : P. In this example, although x is updated
under a confidential branch condition, both branches result in the same state where x = 1; thus,
the outcome of p is independent of the value of s. However, our analysis rejects this program since
rule (T-A SSIGN ) conservatively assumes that any public variable modified in a confidential branch
would leak information. Motivated by the type system in [14], a promising direction that we plan to
investigate is to incorporate sophisticated static program analyses so that the implicit flows can be
ignored for the variables whose values are independent of branch outcomes. Additionally, hybrid
information flow monitors (e.g., [6, 14, 36]) are shown to be more precise than static flow-sensitive
type systems. We plan to compare the analysis precision with those systems in our future work.

25

Acknowledgments
We thank our shepherd Nataliia Bielova and anonymous reviewers for their helpful suggestions.
The noninterference proof in Appendix B is based on a note by Andrew Myers. This work was
supported by NSF grant CCF-1566411.

References
[1] J. Agat, “Transforming out timing leaks,” in Proc. Proc. ACM Symposium on Principles of
Programming Languages (POPL), Jan. 2000, pp. 40–53.
[2] T. Amtoft, S. Bandhakavi, and A. Banerjee, “A logic for information flow in object-oriented
programs,” in Proc. ACM Symposium on Principles of Programming Languages (POPL),
2006, pp. 91–102.
[3] T. Amtoft and A. Banerjee, Information Flow Analysis in Logical Form.
Heidelberg, 2004, pp. 100–115.

Springer Berlin

[4] ——, “A logic for information flow analysis with an application to forward slicing of simple
imperative programs,” Science of Computer Programming, vol. 64, no. 1, pp. 3–28, 2007.
[5] G. R. Andrews and R. P. Reitman, “An axiomatic approach to information flow in programs,”
ACM Trans. on Programming Languages and Systems, vol. 2, no. 1, pp. 56–76, 1980.
[6] A. Askarov, S. Chong, and H. Mantel, “Hybrid monitors for concurrent noninterference,” in
IEEE Symp. on Computer Security Foundations (CSF), 2015, pp. 137–151.
[7] L. Augustsson, “Cayenne—a language with dependent types,” in Proc. 3rd ACM SIGPLAN
Int’l Conf. on Functional Programming (ICFP), 1998, pp. 239–250.
[8] T. H. Austin and C. Flanagan, “Efficient purely-dynamic information flow analysis,” in Proc.
4th ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS),
2009, pp. 113–124.
[9] G. Barthe, P. R. D’Argenio, and T. Rezk, “Secure information flow by self-composition,” in
IEEE Computer Security Foundations Workshop (CSF). IEEE, 2004, pp. 100–114.
[10] G. Barthe, M. Gaboardi, E. J. G. Arias, J. Hsu, A. Roth, and P. Strub, “Higher-order approximate relational refinement types for mechanism design and differential privacy,” in
Proc. ACM Symposium on Principles of Programming Languages (POPL), 2015.
[11] G. Barthe, B. Grégoire, and S. Zanella Béguelin, “Formal certification of code-based cryptographic proofs,” in Proc. ACM Symposium on Principles of Programming Languages
(POPL), 2009, pp. 90–101.
[12] G. Barthe, B. Köpf, F. Olmedo, and S. Zanella Béguelin, “Probabilistic relational reasoning
for differential privacy,” in Proc. ACM Symposium on Principles of Programming Languages
(POPL), 2012, pp. 97–110.
26

[13] N. Benton, “Simple relational correctness proofs for static analyses and program transformations,” in Proc. ACM Symposium on Principles of Programming Languages (POPL), 2004,
pp. 14–25.
[14] F. Besson, N. Bielova, and T. Jensen, “Hybrid information flow monitoring against web tracking,” in Computer Security Foundations Symposium (CSF), 2013 IEEE 26th, 2013, pp. 240–
254.
[15] N. Bielova and T. Rezk, “A taxonomy of information flow monitors,” in Principles of Security
and Trust - 5th International Conference, POST 2016, Held as Part of the European Joint
Conferences on Theory and Practice of Software, ETAPS 2016. Springer LNCS, 2016, pp.
46–67.
[16] J. Condit, M. Harren, Z. Anderson, D. Gay, and G. C. Necula, “Dependent types for low-level
programming,” in Proc. European Symposium on Programming (ESOP), 2007, pp. 520–535.
[17] R. Cytron, J. Ferrante, B. K. Rosen, M. N. Wegman, and F. K. Zadeck, “An efficient method
of computing static single assignment form,” in Proc. ACM Symposium on Principles of Programming Languages (POPL), 1989, pp. 25–35.
[18] Á. Darvas, R. Hähnle, and D. Sands, “A theorem proving approach to analysis of secure information flow,” in International Conference on Security in Pervasive Computing. Springer,
2005, pp. 193–209.
[19] L. M. de Moura and N. Bjørner, “Z3: An efficient SMT solver,” in Proc. Conf. on Tools and
Algorithms for the Construction and Analysis of Systems (TACAS), 2008.
[20] D. E. Denning and P. J. Denning, “Certification of programs for secure information flow,”
Comm. of the ACM, vol. 20, no. 7, pp. 504–513, Jul. 1977.
[21] E. W. Dijkstra, “Guarded commands, nondeterminacy and formal derivation of programs,”
CACM, vol. 18, no. 8, pp. 453–457, Aug. 1975.
[22] A. Ferraiuolo, W. Hua, A. C. Myers, and G. E. Suh, “Secure information flow verification
with mutable dependent types,” in 54th Design Automation Conference (DAC), 2017, to appear.
[23] A. Ferraiuolo, R. Xu, D. Zhang, A. C. Myers, and G. E. Suh, “Verification of a practical
hardware security architecture through static information flow analysis,” in Int’l Conf. on
Architectural Support for Programming Languages and Operating Systems (ASPLOS), 2017,
pp. 555–568.
[24] J. A. Goguen and J. Meseguer, “Security policies and security models,” in Proc. IEEE
Symp. on Security and Privacy (S&P), Apr. 1982, pp. 11–20.
[25] R. Grabowski and L. Beringer, “Noninterference with dynamic security domains and policies,” in Advances in Computer Science – ASIAN 2009. Information Security and Privacy,
2009, pp. 54–68, lNCS 5913.

27

[26] S. Hunt and D. Sands, “On flow-sensitive security types,” in Proc. 33rd Proc. ACM Symposium
on Principles of Programming Languages (POPL), 2006, pp. 79–90.
[27] L. Jia, J. A. Vaughan, K. Mazurak, J. Zhao, L. Zarko, J. Schorr, and S. Zdancewic, “Aura: A
programming language for authorization and audit,” in Proc. ACM SIGPLAN Int’l Conf. on
Functional Programming (ICFP), 2008, pp. 27–38.
[28] B. Köpf and M. Dürmuth, “A provably secure and efficient countermeasure against timing
attacks,” in 2009 IEEE Computer Security Foundations, Jul. 2009.
[29] G. Le Guernic and T. Jensen, “Monitoring Information Flow,” in Workshop on Foundations
of Computer Security - FCS’05, 2005, pp. 19–30.
[30] L. Lourenço and L. Caires, “Dependent information flow types,” in Proc. ACM Symposium
on Principles of Programming Languages (POPL), 2015, pp. 317–328.
[31] T. Murray, R. Sison, E. Pierzchalski, and C. Rizkallah, “Compositional verification and refinement of concurrent value-dependent noninterference,” in Computer Security Foundations
Symposium (CSF), 2016 IEEE 29th. IEEE, 2016, pp. 417–431.
[32] A. C. Myers, “JFlow: Practical mostly-static information flow control,” in Proc. 26th ACM
Symposium on Principles of Programming Languages (POPL), Jan. 1999, pp. 228–241.
[33] A. Nanevski, A. Banerjee, and D. Garg, “Verification of information flow and access control
policies with dependent types,” in Proc. IEEE Symp. on Security and Privacy, 2011, pp.
165–179.
[34] F. Nielson, H. R. Nielson, and C. Hankin, Principles of program analysis.

Springer, 2015.

[35] F. Pottier and V. Simonet, “Information flow inference for ML,” in Proc. 29th ACM Symposium on Principles of Programming Languages (POPL), 2002, pp. 319–330.
[36] A. Russo and A. Sabelfeld, “Dynamic vs. static flow-sensitive security analysis,” in Proc. 23rd
IEEE Symp. on Computer Security Foundations (CSF), 2010, pp. 186–199.
[37] A. Sabelfeld and A. C. Myers, “Language-based information-flow security,” IEEE Journal
on Selected Areas in Communications, vol. 21, no. 1, pp. 5–19, Jan. 2003.
[38] N. Swamy, B. J. Corcoran, and M. Hicks, “Fable: A language for enforcing user-defined
security policies,” in Proc. IEEE Symp. on Security and Privacy, 2008, pp. 369–383.
[39] S. Tse and S. Zdancewic, “Run-time principals in information-flow type systems,” ACM
Trans. on Programming Languages and Systems, vol. 30, no. 1, p. 6, 2007.
[40] D. Volpano, G. Smith, and C. Irvine, “A sound type system for secure flow analysis,” Journal
of Computer Security, vol. 4, no. 3, pp. 167–187, 1996.
[41] H. Xi, “Imperative programming with dependent types,” in Proc. IEEE Symposium on Logic
in Computer Science, 2000, pp. 375–387.
28

[42] H. Xi and F. Pfenning, “Dependent types in practical programming,” in Proc. ACM Symposium on Principles of Programming Languages (POPL), 1999, pp. 214–227.
[43] D. Zhang, A. Askarov, and A. C. Myers, “Language-based control and mitigation of timing channels,” in Proc. Proc. ACM SIGPLAN Conf. on Programming Language Design and
Implementation (PLDI), 2012, pp. 99–110.
[44] D. Zhang, Y. Wang, G. E. Suh, and A. C. Myers, “A hardware design language for timingsensitive information-flow security,” in Proc. 20th Int’l Conf. on Architectural Support for
Programming Languages and Operating Systems (ASPLOS), 2015, pp. 503–516.
[45] L. Zheng and A. C. Myers, “Dynamic security labels and static information flow control,”
Intl’ J. of Information Security, vol. 6, no. 2–3, Mar. 2007.

29

A

Correctness of the Transformation

We first show a few lemmas needed to prove the correctness of the program transformation.
Lemma 3 (Equal Expression) Any transformed expression e evaluates to the same value as in
the original program, and the transformation does not introduce fresh variables.
∀e, A, m, m.
m = mA ∧ he, Ai V e ∧ he, mi ⇓ n ∧ he, mi ⇓ n0
⇒ n = n0 ∧ Vars(e) ⊆ A.
Proof. By induction on the structure of the expression e:
• Case e = n: trivial since e = n and Vars(e) = ∅.
• Case e = x: trivial since we have e = A(x) by the transformation rule. By the assumption
m = mA , we have m(x) = mA (x). Moreover, Vars(e) = A(x) ∈ A.
• Case e = e1 op e2 : from the transformation, we know that e has the form of e1 op e2 . By
the induction hypothesis, we have he1 , mi ⇓ n1 , he2 , mi ⇓ n2 , he1 , mi ⇓ n01 , he2 , mi ⇓ n02 ,
and n1 = n01 ∧ n2 = n02 . Thus, we have e and e evaluate to the same value. Moreover,
Vars(e) ⊆ A by the induction hypothesis.

Lemma 4 (Set-Assignment)
∀A1 , A2 , m1 , m2 .
hA2 := A1 , m1 i → hskip, m2 i
A2
1
⇒ mA
1 = m2

Proof. Recall that A2 := A1 is just a shorthand for assigning vj ∈ A1 to vi ∈ A2 for each v ∈
A1
2
Vars when i 6= j. Hence, for all x ∈ Vars such that A1 (x) 6= A2 (x), we have mA
2 (x) = m1 (x).
For any other variable x (such that A1 (x) = A2 (x)), we know its value is not updated. Thus, we
A2
1
have mA
1 = m2 .

Proof of Theorem 1: Any transformed program is semantically equivalent to its source:
∀c, c, m, m, m0 , m0 , A, A0 .
hc, Ai V hc, A0 i ∧ hc, mi →∗ hskip, m0 i ∧ hc, mi →∗ hskip, m0 i ∧ m = mA
0

⇒ m0 = (m0 )A .
Proof. By induction on the transformation rules in the form of hc, Ai V hc, A0 i.
• Case hskip, Ai V hskip, Ai : trivial since no change is made to the memory m and the
active set A.
30

• Case hx := e, Ai V hx :=η e, A{x 7→ x}i: From Lemma 3, we know that given he, mi ⇓ n
and he, mi ⇓ n0 , then n = n0 . We know from the semantics rule S-Assign that m0 (x) = n
0
0
and (m0 )A (x) = m(x) = n0 . Thus, we have m0 (x) = (m0 )A (x). For all variables other than
0
x, they remain unchanged. Thus, we have m0 = (m0 )A .
• Case hJx := eK, Ai V hxi :=η e, A{x 7→ xi }i: Similar to the previous case.
• Case hc1 ; c2 , Ai V hc1 ; c2 , A2 i: By the induction hypothesis, given hc1 , Ai V hc1 , A1 i,
1
hc1 , mi →∗ hskip, m1 i and hc1 , mi →∗ hskip, m1 i, we have m1 = mA
1 . By the semantics,
hskip; c2 , m1 i → hc2 , m1 i →∗ hskip, m2 i and hskip; c2 , m1 i → hc2 , m1 i →∗ hskip, m2 i.
1
By the induction hypothesis on hc2 , A1 i V hc2 , A2 i (given m1 = mA
1 ), we have m2 =
0
0
0 A
2
mA
2 . Thus, we have m = (m ) .
• Case hif (e) then c1 else c2 , Ai V hif (e) then (c1 ; A3 := A1 ) else (c2 ; A3 = A2 ), A3 i:
From Lemma 3, we know e and e must evaluate to some value n. Thus, both evaluation must
take the same branch. Without losing generality, we consider the case when n 6= 0.
By the induction hypothesis on the transformation hc1 , Ai V hc1 , A1 i, we know that given
1
hc1 , mi →∗ hskip, m1 i and hc1 , mi →∗ hskip, m1 i, we have m1 = mA
1 . For the rest of the
evaluation ( hskip; A3 := A1 , m1 i → hA3 := A1 , m1 i →∗ hskip, m3 i), by Lemma 4, we
A1
A3
0
0 A0
3
have mA
3 = m1 = m1 . Thus, we have m = m1 = m3 = (m ) .
• hwhile (e) c, Ai V hA1 := A; while (e) (c; A1 := A2 ), A1 i: The evaluation looks like:
hA1 := A; while (e) (c; A1 = A2 ), mi
→ hwhile (e) (c; A1 = A2 ), m1 i → ...
1
By Lemma 4, we have mA
= mA = m. We proceed by induction on the number of
1
iterations being executed in the evaluation:

– Base case: 0 iteration is executed in the original program. It must be true that he, mi ⇓ 0
and m0 = m. Since the transformation requires that he, A1 i V e, we have he, m1 i ⇓ 0
by Lemma 3. Hence, 0 iteration is executed in the transformed program, and m0 = m1 .
0
1
Hence, m0A1 = mA
1 = m = m in this case.
– Induction case for N iterations (N ≥ 1): The evaluation of original while looks like:
hwhile (e) c, mi
→ hif (e) then (c; while (e) c) else skip, mi
→ hc; while (e) c, mi
→∗ hskip; while (e) c, m1 i
→ hwhile (e) c, m1 i
→ . . . N − 1 iterations . . .

31

The evaluation of the transformed while looks like:
hwhile (e) (c; A1 := A2 ), m1 i
→ hif (e) then (c; A1 := A2 ; while (e) (c; A1 := A2 )) else skip, m1 i
→ hc; A1 := A2 ; while (e) (c; A1 := A2 ), m1 i
→∗ hskip; A1 := A2 ; while (e) (c; A1 := A2 ), m2 i
→ hA1 := A2 ; while (e) (c; A1 := A2 ), m2 i
→ hwhile (e) (c; A1 := A2 ), m3 i → ...
Here, we know that the transformed program must take the “if” branch due to the same
1
argument as in the base case. Since mA
1 = m, by (structural) induction hypothesis on
2
c and the transformation rule which requires hc, A1 i V hc, A2 i, we have m1 = mA
2 .
2
By Lemma 4, we have m3A1 = mA
= m1 . By the induction hypothesis when the
2
original program runs for N − 1 iterations, we have m0A1 = m0 as desired.


32

n ∼ n [n1 ] ∼ [n2 ]
e ::= . . . | [n]
c ::= . . . | [c]

c∼c

m1 ∼ m2 =⇒ ∀x.m1 (x) ∼ m2 (x)

c1 ∼ c3
c2 ∼ c4
c1 ; c2 ∼ c3 ; c4

[c1 ] ∼ [c2 ]

Figure 17: Extended Syntax
Figure 18: Equivalence on Memories and Commands

B

Soundness

We need more definitions before showing the soundness of our analysis. We first use a distinguished label L (“low”) to define what is observable to the low observer. Since the lemmas and
theorems are valid regardless of what level L is, the propositions proved hold for any label ` in the
security lattice.
As discussed in Section 6, we prove the soundness based on the erasure semantics in Figure 13.
The connection between the erasure and the standard semantics is established by the following
lemma:
Lemma 5
∀c, m, m1 , m2 , A. hm, ci →∗ hm1 , skipi ∧ hm, ci →∗ER(A) hm2 , skipi
⇒ ∀v ∈ A. m1 (v) = m2 (v)
Proof. We note that the erasure semantics only changes the values of dead variables. Hence, the
result is trivial given that the live variable analysis is correct.

Next, we prove that any well-typed target program under the erasure semantics satisfies the
noninterference property. To simplify notation, we will use → instead of →ER(A) hereafter. To
prove soundness, we extend the language syntax and semantics with explicitly marked high values
and commands. Memory is extended to track high values as well. The extension is useful since the
low equivalence relation we defined earlier corresponds to the equivalence relation on the marked
memories.
By showing the completeness of the extended language, all interesting proof are then conducted
on the extended language. To do that, we first prove several useful lemmas, and then show the type
system enforces noninterference.

B.1

Extended Language

Extended syntax The extended syntax is shown in Figure 17. We augment memories to map
high variables to bracketed results. In a similar way, syntax is augmented to include bracketed results, and bracketed commands. Intuitively, bracketed results represent values from high memory,
and bracketed commands represent commands executed in a high pc context (such as in a branch
with a high guard).

33

he1 , mi ⇓ [n1 ]
h[n], mi ⇓ [n]

he2 , mi ⇓ n2
n = n1 op n2
he1 op e2 , mi ⇓ [n]

he1 , mi ⇓ n1

he2 , mi ⇓ [n2 ]
n = n1 op n2
he1 op e2 , mi ⇓ [n]

he1 , mi ⇓ [n1 ]

he2 , mi ⇓ [n2 ]
he1 op e2 , mi ⇓ [n]

n = n1 op n2

Figure 19: Extended Semantics: Expressions


x ∈ FV(x0 ) ∧ x0 ∈
6 ŁA (η) ∧ T (x0 , m) v L
0,
erase(m, x, η)(x0 ) = [0],
x ∈ FV(x0 ) ∧ x0 6∈ ŁA (η) ∧ T (x0 , m) 6v L


m(x0 ), otherwise
S-B RACKET

S-S KIP 1

hc, mi → hc0 , m0 i
h[c], mi → h[c0 ], m0 i

h[skip], mi → hskip, mi
S-A SGN 1

he, mi ⇓ n
T (x, m) v L
m0 = m{x 7→ n}
hx :=η e, mi → hskip, erase(m0 , x, η)i

S-A SGN 2

he, mi ⇓ n
T (x, m) 6v L
m0 = m{x 7→ [n]}
hx :=η e, mi → hskip, erase(m0 , x, η)i

S-A SGN 3

S-I F 3

he, mi ⇓ [n]
m0 = m{x 7→ [n]}
hx :=η e, mi → hskip, erase(m0 , x, η)i

he, mi ⇓ [n]
n 6= 0
hif (e) then c1 else c2 , mi → h[c1 ], mi

S-I F 4

he, mi ⇓ [n]
n=0
hif (e) then c1 else c2 , mi → h[c2 ], mi
Figure 20: Extended Semantics: Commands

34

T-B RACKET C MD

Γ, τ ` c

` 6v L
T-B RACKET E XP
Γ ` [n] : `

pc v τ
Γ, pc ` [c]

τ 6v L

Figure 21: Extended Typing Rules: Expressions Figure 22: Extended Typing Rules: Commands
Extended Semantics The operational semantics is augmented to propagate brackets, as shown
in Figure 19, 20. All rules are extensions to the original grammar except that (S-A SGN ) is split
into three rules: (S-A SGN 1), (S-A SGN 2), (S-A SGN 3). Moreover, the erasure semantics for the
extended language also adds brackets when needed. All rules with brackets work the same way as
the normal rules from computational perspective. Brackets are just syntactic markers.
The extended language requires extra typing rules, shown in Figure 21. Rule (T-B RACKET E XP )
treats bracketed expression as high. Note that this rule requires a security level `, which by definition cannot depend on any program state. Rule (T-B RACKET C MD ) in Figure 22 is given to
support the soundness proof. Bracketed command should be type-checked under a pc label that is
not bounded by L in the type system.
Equivalence on Memories and Commands We define the equivalence of memories and commands up to label L as in Fig. 18. Intuitively, bracketed memory and commands are indistinguishable. An equivalence relation ∼ is defined on memories such that m1 ∼ m2 if and only if they
agree on all low variables, and the rest of variables are all high (with brackets).
The type system enforces an important invariant on the memory: a variable holds bracketed
value if and only if the security level of that variable is high. This is formalized as follows:
Definition 8 (Well-Formedness) A variable x is well-formed under memory m, denoted as `m x
if the following condition holds:
T (x, m) 6v L ⇐⇒ ∃n.hx, mi ⇓ [n]
A memory m is well-formed, denoted as ` m if all variables are well formed under m:
` m ⇐⇒ (∀x ∈ m. `m x)
Completeness of the Extended Language It is then clear that for any two low-equivalent standard memories m1 , m2 , there are augmented memories, simply by putting brackets for high variables, that agree with standard memories on all low variables; and vise versa. Hence, the completeness result (Lemma 6) justifies the noninterference result in the unextended language, by showing
that starting from any m1 ∼ m2 that are both well-formed, the resulting memories are still equivalent in the augmented language.
Completeness means that every step in the new semantics can be performed in the unextended
semantics (maybe with removal of brackets) and vice versa. More formally, given that c is a
command in the extended language, let us use the notation of bcc to denote removal of all brackets
from c in the obvious way, yielding a command from the original language. Similarly, we define
bmc to convert memory. Completeness can be expressed as the following lemma.
35

Lemma 6 (Completeness of the Extended Language)
Γ, pc ` c ∧ hbcc, bmci →∗ hskip, m0 i =⇒ ∃m00 . hc, mi →∗ hskip, m00 i ∧ m0 = bm00 c
Proof. By rule induction on each evaluation step.

B.2



Soundness Proof

Next, we prove the soundness of the type system on the extended language language with the
erasure semantics. We first introduce a couple of useful lemmas.
Lemma 7 The type comparison is conservative:
∀m, τ1 , τ2 . τ1 v τ2 =⇒ V(τ1 , m) v V(τ2 , m)
Proof. Clear from the lifted definition of v on (dependent) labels.



Lemma 8 Low expressions always evaluate to ordinary integers (without brackets) under wellformed memory:
` m ∧ Γ ` e : τ ∧ V(τ, m) v L =⇒ ∃n.he, mi ⇓ n
Proof. By induction on the structure of the expression e:
• Case e = n: trivial.
• Case e = [n]: contradiction to the typing rule (T-B RACKET E XP ).
• Case e = x: x could be either low or high.
– Case x is low (T (x, m) v L ): clear from the definition of ` m.
– Case x is high (T (x, m) 6v L ): contradiction to the assumption V(τ, m) v L.
• Case e = e1 op e2 : From Γ ` e : τ , we can infer that Γ ` e1 : τ1 , Γ ` e2 : τ2 and
τ = τ1 t τ2 . By Lemma 7, V(τ1 , m) v L and V(τ2 , m) v L. Hence by induction hypothesis,
∃n1 , n2 .he1 , mi ⇓ n1 , he2 , mi ⇓ n2 . Thus, he, mi ⇓ n, where n = n1 op n2 by the semantics.

Lemma 9 (PC Subsumption)
Γ, pc ` c ∧ pc 0 v pc =⇒ Γ, pc 0 ` c
Proof. By rule induction on the typing derivation for c :
• Case skip : From typing rule (T-S KIP ), we know that Γ, pc 0 ` skip for any pc 0 .
• Case x :=η e : From typing rule (T-A SSIGN ), we know that Γ ` e : τ and |= P(•η) ⇒
τ t pc v Γ(x) and ∀v ∈ ŁA (η•).x 6∈ FV(Γ(v)). Since pc 0 v pc, we have τ t pc 0 v τ t pc v
Γ(x). Thus, we have |= P(•η) ⇒ τ t pc 0 v Γ(x) and there is no change to the other
conditions. So we can derive Γ, pc 0 ` x :=η e.
36

• Case c1 ; c2 : From typing rule (T-S EQ ), we know that Γ, pc ` c1 and Γ, pc ` c2 . By the
induction hypothesis, we have Γ, pc 0 ` c1 and Γ, pc 0 ` c2 . Thus, we can derive Γ, pc 0 ` c1 ; c2 .
• Case if (e) then c1 else c2 : From typing rule (T-I F ), we know that Γ ` e : τ , Γ, pctτ ` c1
and Γ, pc tτ ` c2 . Since pc 0 v pc, we have τ tpc 0 v τ tpc. So by the induction hypothesis,
we have Γ, pc 0 t τ ` c1 and Γ, pc 0 t τ ` c2 . Hence, Γ, pc 0 ` if (e) then c1 else c2 .
• Case while (e) c : From typing rule (T-W HILE ), we know that Γ ` e : τ , Γ, pc t τ ` c.
Since pc 0 v pc, we have τ t pc 0 v τ t pc. So by the induction hypothesis, we have
Γ, pc 0 t τ ` c. Hence, Γ, pc 0 ` while (e) c.

Lemma 10 (Preservation)
Γ, pc ` c ∧ hc, m1 i → hc0 , m2 i ∧ ` m1
=⇒ ` m2 ∧ Γ, pc ` c0
Proof. By rule induction on the evaluation rules hc, m1 i → hc0 , m2 i:
• Case h[skip], m1 i → hskip, m1 i: trivial.
• Case hskip; c, m1 i → hc, m1 i : Trivial since m does not change and Γ, pc ` c is required in
rule (T-S EQ ).
• Case hc1 ; c2 , m1 i → hc01 ; c2 , m2 i: From the assumption, we have hc1 , m1 i → hc01 , m2 i. From
typing rule (T-S EQ ), we have Γ, pc ` ci , i ∈ {1, 2}. So by the induction hypothesis, we
have Γ, pc ` c01 and ` m2 . Hence we can derive Γ, pc ` c01 ; c2 .
• Case h[c], m1 i → h[c0 ], m2 i: From typing rule (T-B RACKET C MD ), we know that there exists
some label τ such that τ 6v L ∧ pc v τ and Γ, τ ` c. From the assumption, we know that
hc, m1 i → hc0 , m2 i. By induction hypothesis, we have Γ, τ ` c0 and ` m2 . Thus, we can
derive Γ, pc ` [c0 ] .
• Case hx :=η e, m1 i → hskip, erase(m0 , x, η)i: We have Γ, pc ` skip trivially. Next, we
prove that ` m2 (in this case, m2 is erase(m0 , x, η)) by showing that every variable x0 is
well-formed under m2 . To do so, we first note that T (x0 , m2 ) = T (x0 , m0 ) since there is no
chain of dependence or self dependency.
– Case x 6∈ FV(Γ(x0 )): We first show that the level of x0 does not change after the assignment. Since x0 does not depend on x, we have T (x0 , m1 ) = T (x0 , m0 ). Further, we can
infer that T (x0 , m2 ) = T (x0 , m0 ) = T (x0 , m1 ).
By the definition of erase, we have m2 (x0 ) = m0 (x0 ). So if x0 6= x, we have `m2 x0
trivially since neither its value (since m0 (x0 ) = m(x0 )) nor its type is changed after the
assignment; otherwise, if x0 = x we have three cases:
∗ Case S-Asgn1: We have m2 (x) = m0 (x) = m1 {x 7→ n}(x) = n and T (x, m2 ) =
T (x, m1 ) v L. Thus, `m2 x.
37

∗ Case S-Asgn2: We have m2 (x) = m0 (x) = m1 {x 7→ [n]}(x) = [n] and T (x, m2 ) =
T (x, m1 ) 6v L. Thus, we can derive `m2 x since x is high and is given a bracketed
value.
∗ Case S-Asgn3: We have m2 (x) = m0 (x) = m1 {x 7→ [n]}(x) = [n]. We also know
from the typing rule (T-A SSGN ) that Γ ` e : τ, |= P(•η) ⇒ τ t pc v Γ(x). By
assumption, he, m1 i ⇓ [n]. By Lemma 8, V(τ, m1 ) 6v L. Hence, T (x, m1 ) 6v L
due to Lemma 7. Thus, we have T (x, m2 ) = T (x, m1 ) 6v L. So `m2 x since x is
high and is given a bracketed value.
Thus, in all three cases, we have `m2 x0 .
– Case x ∈ FV(x0 ): by the definition of erase, x0 is erased to 0 or [0] according to
T (x0 , m0 ). We already showed T (x0 , m0 ) = T (x0 , m2 ). Thus, we have `m2 x0 .
• Case hif (e) then c1 else c2 , m1 i → hc1 , m1 i and hif (e) then c1 else c2 , m1 i → hc2 , m1 i
: ` m2 is trivial since m2 = m1 . For types, from the typing rule (T-I F ), we have Γ ` e : τ ,
Γ, pc t τ ` c1 and Γ, pc t τ ` c2 . Since pc v pc t τ , we can derive from Lemma 9 that
Γ, pc ` c1 and Γ, pc ` c2 .
• Case hif (e) then c1 else c2 , m1 i → h[c1 ], m1 i, and hif (e) then c1 else c2 , m1 i →
h[c2 ], m1 i : ` m2 is trivial since m2 = m1 . For types, from the typing rule (T-I F ), we have
Γ ` e : τ , Γ, pc t τ ` c1 and Γ, pc t τ ` c2 . From the assumption, we have he, m1 i ⇓ [n].
By Lemma 8, V(τ, m1 ) 6v L. Hence, T (pc t τ, m1 ) 6v L due to Lemma 7. Thus, we can
derive Γ, pc ` [c1 ] and Γ, pc ` [c2 ] by using pc t τ as the “τ ” in rule (T-B RACKET C MD ).
• Case hwhile (e) c, m1 i → hif (e) then (while (e) c) else skip, m1 i :
` m2 is trivial since m2 = m1 . By the typing rule (T-W HILE ), we have two assumptions
A = Γ ` e : τ and B = Γ, τ t pc ` c. So the program after evaluation can be typed as
follows:
A B
Γ, τ t pc ` while (e) c Γ, τ t pc ` skip
Γ, pc ` if (e) then (while (e) c) else skip

A


Lemma 11 (High-Step) A command that type-checks in a high-pc context only modifies high variables.
∀m1 , m2 , c, pc . V(pc, m1 ) 6v L ∧ Γ, pc ` c ∧ ` m1 ∧ hc, m1 i → hc0 , m2 i =⇒ m1 ∼ m2
Proof. By induction on evaluation rules hc, m1 i → hc0 , m2 i:
• Cases h[skip], m1 i → hskip, m1 i,hskip; c, m1 i → hc, m1 i,
hif (e) then c1 else c2 , m1 i → hc1 , m1 i, hif (e) then c1 else c2 , m1 i → hc2 , m1 i,
hif (e) then c1 else c2 , m1 i → h[c1 ], m1 i, hif (e) then c1 else c2 , m1 i → h[c2 ], m1 i,
hwhile (e) c, m1 i → hif (e) then (while (e) c) else skip, m1 i:
Trivial since m2 = m1 .
38

• Case hc1 ; c2 , m1 i → hc01 ; c2 , m2 i : From the type rule (T-S EQ ), we have Γ, pc ` c1 . By
induction hypothesis on the assumption hc1 , m1 i → hc01 , m2 i , we have m1 ∼ m2 .
• Case h[c], m1 i → h[c0 ], m2 i : From the evaluation rule, we have hc, m1 i → hc0 , m2 i. From
the typing rule, we have Γ, τ ` c for some τ such that pc v τ . Since by assumption,
V(pc, m1 ) 6v L, we have V(τ, m1 ) 6v L by Lemma 7. Hence, by induction hypothesis on the
evaluation assumption, we have m1 ∼ m2 .
• Casehx :=η e, m1 i → hskip, erase(m0 , x)i : First, we can infer from the type rule that
Γ ` e : τ , |= P(•η) ⇒ τ t pc v Γ(x). Due to the correctness of predicate generator, we
have τ t pc v Γ(x). Since V(pc, m1 ) 6v L, we have T (x, m1 ) 6v L by Lemma 7. From
assumption ` m1 , we know x must hold a bracketed value in m1 . We also know that S-Asgn1
can not be applied since it requires T (x, m1 ) v L. When S-Asgn2 or S-Asgn3 is applied,
we have m0 = m1 {x 7→ [n]}. Since there is no self-dependence, m2 (x) = m0 (x) = [n]. So
m2 (x) ∼ m1 (x). Next, we show that for variable x0 6= x, we have m1 (x0 ) ∼ m2 (x0 ):
– Case x 6∈ FV(x0 ): by definition of erase, m2 (x0 ) = m0 (x0 ) = m1 (x0 ). Hence,
m1 (x0 ) ∼ m2 (x0 ).
– Case x ∈ FV(x0 ): by definition of erase, x0 is erased to 0 or [0] according to T (x0 , m0 ).
We already know that T (x, m1 ) 6v L. Since there is no self-dependence, T (x, m0 ) 6v
L. Recall that x ∈ FV(x0 ) implies Γ(x) v Γ(x0 ). Hence, by Lemma 7, T (x0 , m1 ) 6v L
and T (x0 , m0 ) 6v L. By assumption ` m1 , x0 holds a bracketed value in m1 . Moreover,
by the erasure semantics, x0 is erased to [0] after the assignment. So m1 (x0 ) ∼ m2 (x0 ).

Lemma 12
∀m1 , m2 . m1 ∼ m2 ∧ he, m1 i ⇓ v1 =⇒ ∃v2 .he, m2 i ⇓ v2 ∧ v1 ∼ v2
Proof. By rule induction on the structure of expression e.
• Case e = n: trivial since we have he, mi ⇓ n for any memory, so v1 = v2 = n.
• Case e = [n]: trivial since we have he, mi ⇓ [n] for any memory, so v1 = v2 = [n].
• Case e = x: From m1 ∼ m2 , we have m1 (x) = m2 (x), thus, v1 ∼ v2 .
• Case e = e1 op e2 : By the induction hypothesis, we have he1 , m1 i ⇓ v3 , he1 , m2 i ⇓
v30 , he2 , m1 i ⇓ v4 , he2 , m2 i ⇓ v40 , and v3 ∼ v30 , v4 ∼ v40 .
– If both v3 , v4 are non-bracketed values, then v3 = v30 and v4 = v40 . Result is trivial.
– If at least one of v3 and v4 holds bracketed value, we know that at least one of v30 and v40
holds a bracketed value. From the semantics we know e must be evaluated to bracketed
values under both m1 and m2 . Thus, v1 ∼ v2 .

39

Lemma 13 (Unwinding)
∀c1 , c2 , m1 , m2 , m3 , m4 .
` c1 ∧ ` c2 ∧ c1 ∼ c2 ∧ ` m1 ∧ ` m2 ∧ m1 ∼ m2
∧ hc1 , m1 i → hc3 , m3 i
=⇒ (∃c4 , m4 . c4 ∼ c3 ∧ hc2 , m2 i →∗ hc4 , m4 i ∧ m3 ∼ m4 ) ∨ (hc2 , m2 i ⇑∧ ∃c. c2 = [c])
Proof. By rule induction on hc1 , m1 i → hc3 , m3 i.
• Case h[skip], m1 i → hskip, m1 i: From c1 ∼ c2 , we know c2 has the form of [c5 ], for
some c5 . If c2 diverges, we are done with c = c5 . Otherwise, we have h[c5 ], m2 i →∗
h[skip], m4 i → hskip, m4 i. By induction on the number of steps using Lemma 11, we have
m4 ∼ m2 ∼ m1 . So we can choose c4 = skip.
• Case h[c5 ], m1 i → h[c05 ], m3 i: From c1 ∼ c2 , we know c2 has the form of [c6 ] for some c6 .
Hence, c2 = [c6 ] ∼ [c05 ]. Moreover, by Lemma 11, m3 ∼ m1 . Hence, m2 ∼ m3 . Therefore,
we can choose c4 = c2 and make zero step under m2 .
• Case hskip; c5 , m1 i → hc5 , m1 i: Command c2 must also have the form of skip; c6 where
c5 ∼ c6 . So hskip; c6 , m2 i → hc6 , m2 i preserves the equivalence on memory and command
as required.
• Case hc5 ; c6 , m1 i → hc05 ; c6 , m3 i: Command c2 must have the form of c7 ; c8 where c5 ∼
c7 , c6 ∼ c8 . We can infer from c5 ∼ c7 and the evaluation assumption hc5 , m1 i → hc05 , m3 i
that hc7 , m2 i →∗ hc07 , m5 i and m5 ∼ m3 and c07 ∼ c05 . Thus, we can derive hc7 ; c8 , m2 i →∗
hc07 ; c8 , m5 i. Therefore, we can choose c4 = c07 ; c8 and m4 = m5 .
• Case hx :=η e, m1 i → hskip, erase(m01 , x, η)i: From c1 ∼ c2 , we know c2 = (x :=η e),
and hx :=η e, m2 i → hskip, erase(m02 , x, η)i. Trivially, skip ∼ skip. Next, we show
erase(m01 , x, η) ∼ erase(m02 , x, η).
From Lemma 12, we know that he, m1 i ⇓ v1 , he, m2 i ⇓ v2 , then v1 ∼ v2 . We know
m01 = m1 {x 7→ v1 } and m02 = m2 {x 7→ v2 }. Thus, m01 ∼ m02 given m1 ∼ m2 . Since there
is no self-dependence, we have m3 (x) = m01 (x) ∼ m02 (x) = m4 (x). Next, we show for any
x0 6= x, we have m3 (x0 ) ∼ m4 (x0 ):
– Case x 6∈ FV(x0 ): by definition of erase, we have m3 (x0 ) = m01 (x0 ) ∼ m02 (x0 ) =
m4 (x0 ).
– Case x ∈ FV(x0 ): by definition of erase, x0 is erased to 0 or [0] according to its type
T (x0 , m01 ) or T (x0 , m02 ).
∗ Case S-Asgn1, we have he, m1 i ⇓ n, T (x, m1 ) v L and m01 (x) = n. By
Lemma 12 and 8, he, m2 i ⇓ n, T (x, m2 ) v L. So S-Asgn1 applies under m2
as well, and m02 (x) = n ∧ m01 ∼ m02 . When x0 depends on no variable whose level
is low under m1 , we have T (x0 , m01 ) = T (x0 , m02 ) since all variables it depends on
must be identical under m01 and m02 . So x0 will be erased to the same value in this
case. Otherwise, say x0 depends on y such that T (y, m01 ) 6v L. By Lemma 8, y has
40

a bracketed value under m01 . Since m01 ∼ m02 , y has a bracketed value under m02 as
well. By Lemma 8 again, T (y, m02 ) 6v L. Since Γ(y) v Γ(x0 ) when x0 depends
on y, we have T (x0 , m01 ) 6v L and T (x0 , m02 ) 6v L by Lemma 7. Hence, x0 will be
erased to [0] under m01 and m02 .
∗ Case S-Asgn2: we have T (x, m1 ) 6v L. Since m1 ∼ m2 , we have T (x, m2 ) 6v L
by Lemma 12 and 8. So S-Asgn2 applies under m2 as well. Since there is no self
dependence, we have T (x, m01 ) = T (x, m1 ) 6v L and T (x, m02 ) = T (x, m2 ) 6v L.
Since x0 depends on x, we must have T (x0 , m01 ) 6v L and T (x0 , m02 ) 6v L. So by
the definition of erase, m3 (x0 ) = m4 (x0 ) = [0].
∗ Case S-Asgn3: we have he, m1 i ⇓ [n1 ] for some n1 . By Lemma 12, v2 = [n2 ]
for some n2 . So S-Asgn3 applies under m2 as well. Moreover, given Γ ` e : τ ,
V(τ, m1 ) 6v L and V(τ, m2 ) 6v L by Lemma 8. We also know from typing rule
T-Assgn that |= P(•η) ⇒ τ t pc v Γ(x). Due to the correctness of predicate
generation, τ t pc v Γ(x). By Lemma 7, T (x, m1 ) 6v L ∧ T (x, m2 ) 6v L. Similar
to case S-Asgn2, we know that m3 (x0 ) = m4 (x0 ) = [0] in this case.
• Case hif (e) then c5 else c6 , m1 i → hc5 , m1 i and hif (e) then c5 else c6 , m1 i →
hc6 , m1 i: From c1 ∼ c2 , we know c2 must be if (e) then c5 else c6 . This rule is applied
only when e’s value under m1 is not bracketed. By Lemma 12, e’s value is not bracketed
under m2 and e must evaluate to the same value under m1 and m2 . Therefore, c1 and c2 must
evaluate using the same rule. We can construct c4 as the corresponding branch taken under
m1 .
• Case hif (e) then c5 else c6 , m1 i → h[c5 ], m1 i and hif (e) then c5 else c6 , m1 i →
h[c6 ], m1 i. From c1 ∼ c2 , we know c2 must be if (e) then c5 else c6 . This rule is applied
when he, m1 i ⇓ [n1 ]. By Lemma 12, we know that he, m2 i ⇓ [n2 ] . We construct c4 as the
branch taken under m2 in one step. According to the semantics, c4 evaluates to either [c5 ] or
[c6 ]. That is, both c3 and c4 evaluate to bracket commands. Hence, we have c3 ∼ c4 .
• Case hwhile (e) c5 , m1 i → hif (e) then (while (e) c5 ) else skip, m1 i: From c1 ∼ c2 , we
know c2 has the form of while (e) c5 . Therefore, we construct c4 as
if (e) then (while (e) c5 ) else skip. Hence, m2 ∼ m4 and c3 ∼ c4 .

Theorem 5 (Soundness under Erasure Semantics) Any transforms program that type checks satisfies noninterference:
∀c, m1 , m2 , m3 , m4 , Γ, `, A0 .
Γ ` c ∧ m1 ≈`Γ m2 ∧
hc, m1 i →∗ER(A0 ) hskip, m3 i ∧ hc, m2 i →0∗
ER(A) hskip, m4 i
=⇒ m01 ≈`Γ m02
Proof. By the construction of the extended language, for any particular `, the relation m1 ≈`Γ m2
is the same as ` m1 , ` m2 , m1 ∼ m2 in the extended language. We proceed by induction on the
number of steps in the execution under m1 .
41

Case zero step: trivial since c must be skip.
Case N + 1 steps: consider the first step of the execution under m1 . By Lemma 13, we know
either c diverges under m2 or we can make multiple steps under m2 and m3 ∼ m4 . By Lemma 10,
we also have ` m3 , ` m4 and the remaining programs c1 and c2 type-checks. Hence, result is true
by the induction hypothesis.

Proof of Theorem 3
∀c, m1 , m2 , m3 , m4 , `, A, A0 , Γ .
`
A
hc, Ai V hc, A0 i∧ ` Γ ∧ Γ ` c ∧ mA
1 ≈ΓA m2

∧ hc, m1 i →∗ hskip, m3 i ∧ hc, m2 i →∗ hskip, m4 i
0

0

`
A
=⇒ mA
3 ≈ΓA0 m4

Proof. Trivial by Theorem 5 and Lemma 5, which states that the erasure semantics agrees with
the standard semantics on active copies in A0 .

Proof of Theorem 2
∀c, c, m1 , m2 , m01 , m02 , `, Γ, A, A0 .
hc, Ai V hc, A0 i∧ ` Γ ∧ Γ ` c ∧ m1 ≈`ΓA m2 ∧
hc, m1 i →∗ hskip, m01 i ∧ hc, m2 i →∗ hskip, m02 i
=⇒ m01 ≈`ΓA0 m02
Proof. Trivial by Theorem 3 and Theorem 1, the correctness of program transformation.

42



C

Enabling Flow-Sensitivity with Program Transformation

To facilitate the proof, we say a typing environment Γ0 is an extension of Γ, written Γ  Γ0 , if
∀x ∈ Dom(Γ). Γ(x) = Γ0 (x). Easy to check that this relation is an partial order on environments
(i.e., the relation satisfies reflexivity, antisymmetry and transitivity).
Lemma 14
hJcK, Ai V hc, A0 i ⇒ A0 ⊆ (A ∪ FVars(c))
Proof. By induction on the structure of c.
• skip: A0 ⊆ A ∪ FVars(c) since A = A0 in this case.
• x := e: we have A0 ⊆ A ∪ FVars(c) since A0 = {xi } ∪ (A − {A(x)}).
• c1 ; c2 : by the transformation rule we have hJc1 K, Ai V hc1 , A1 i and hJc2 K, A1 i V hc2 , A0 i
for some A1 . By the induction hypothesis, we have
A1 ⊆ (A ∪ FVars(c1 )) ∧ A0 ⊆ (A1 ∪ FVars(c2 ))
Hence, we have
A0 ⊆ (A1 ∪ FVars(c1 ) ∪ FVars(c2 )) ⊆ (A ∪ FVars(c1 ) ∪ FVars(c2 ))
Therefore, A0 ⊆ (A ∪ FVars(c1 ; c2 )).
• if (e) then c1 else c2 : by the transformation rule, we have he, Ai V e and
hJci K, Ai V hci , Ai i, i ∈ {1, 2}. By the induction hypothesis, we have
A1 ⊆ (A ∪ FVars(c1 )) ∧ A2 ⊆ (A ∪ FVars(c2 ))
The transformed branch has the form of ci ; A3 := Ai where A3 = Φ(A1 , A2 ). By the
definition of Φ, A3 ⊆ A1 ∪ A2 ∪ FVars(A3 := A1 ; A3 := A2 ) ⊆ A ∪ FVars(c).
• while (e) c: by the transformation rule, we have
hJcK, Ai V hc1 , A1 i hJcK, A1 i V hc0 , A2 i he, A1 i V e
hJwhile (e) cK, Ai V hA1 := A; while (e) (c0 ; A1 := A2 ), A1 i
By induction on hJcK, Ai V hc1 , A1 i, we have A1 ⊆ A ∪ FVars(c1 ). For a variable v in
A1 but not in A, we know that v ∈ FVars(A1 := A) since by definition, A1 := A assigns
to any v ∈ A1 ∧ v 6∈ A. Hence, A1 ⊆ A ∪ FVars(c).

The next lemma shows that the extension of a typing environment Γ subsumes Γ:
Lemma 15
Γ  Γ0 ∧ Γ ` c ⇒ Γ0 ` c
43

Proof. We first show Γ  Γ0 ∧ Γ ` e : τ ⇒ Γ0 ` e : τ by induction on the structure of e. Then we
can prove the lemma by induction on the structure of c.

Proof of Lemma 2
pc `HS Γ{c}Γ0 ∧ hJcK, Ai V hc, A0 i ⇒
∀v ∈ Vars. (A(v) = A0 (v)) ⇒ (Γ(v) = Γ0 (v))
Proof. By induction on the structure of c.
• skip: trivial since Γ = Γ0 .
• x := e: when v = x, A0 (v) = xi 6= A(x) since xi is fresh. So the result is trivially true. For
other variables, Γ(v) = Γ0 (v) by the HS typing rule (HS-A SSIGN ).
• c1 ; c2 : by the transformation rule and HS typing rule, we have hJc1 K, Ai V hc1 , A1 i and
hJc2 K, A1 i V hc2 , A0 i for some A1 , as well as pc `HS Γ{c1 }Γ1 and pc `HS Γ1 {c2 }Γ0 for
some Γ1 . By Lemma 14, A0 ⊆ A1 ∪ FVars(c2 ). So when A(v) = A0 (v), it must be true
that A1 (v) = A0 (v) since otherwise, A0 (v) must be a fresh variable in c2 , and hence, cannot
appear in A. Therefore, we have A(v) = A0 (v) = A1 (v). By the induction hypothesis, it
must be true that Γ(v) = Γ1 (v) = Γ0 (v).
• if (e) then c1 else c2 : by the HS typing rule, pc `HS Γ{c1 }Γ1 ∧ pc `HS Γ{c2 }Γ2 ∧ Γ0 =
Γ1 t Γ2 . By the transformation rules, hJci K, Ai V hci , Ai i, i ∈ {1, 2}.

By Lemma 14, A1 ⊆ A ∪ FVars(c1 ). So when A(v) 6= A1 (v), A1 (v) must be a fresh
variable generated in c1 , and hence, cannot be in A2 . By the definition of Φ, A3 (v) must
be fresh as well. This contradicts the assumption that A(v) = A0 (v). Hence, we have
A(v) = A1 (v) (and similarly, A(v) = A2 (v)). So Γ(v) = Γi (v) by the induction hypothesis.
Therefore, Γ0 (v) = Γ1 (v) t Γ2 (v) = Γ(v).

• while (e) c: By rule (TRSF-W HILE ), we have hJcK, Ai V hc1 , A1 i, where A0 is A1 in this
case. Hence, by the assumption, we have A(v) = A1 (v). By rule (HS-W HILE ), there is a
sequence of environments Γ0i , Γ00i such that pc t τi ` Γ0i {c}Γ00i . By the induction hypothesis,
Γ00i (v) = Γ0i (v). Since Γ00 = Γ and Γ0i+1 = Γ t Γ00i in rule (HS-W HILE ), we can further infer
that Γ0i+1 (v) = Γ00i (v). Hence, we have Γ0 (v) = Γn (v) = Γ0 (v) = Γ(v).

Lemma 16
Γ `HS e : τ ∧ he, Ai V e ∧ Γ = ΓA ⇒
Γ`e:τ
Proof. By rule induction on the transformation.

44



Proof of Theorem 4 We prove a lightly stronger version of Theorem 4:
∀c, c, pc, A, A0 , Γ, Γ0 , Γ.
(pc, Γ, A){JcK V c}(Γ0 , A0 ) ,→ Γ
0

⇒ Dom(Γ) ⊆ A ∪ FVars(c) ∧ Γ = ΓA ∧ Γ0 = ΓA ∧ Γ, pc ` c
Proof. By induction on the structure of c.
• skip: Γ, pc ` c is trivial since skip can be type-checked with any pc, Γ. Other conditions
are trivial.
• x := e: by the construction rule, we have Γ0 (x) = τ for some τ , c has the form of xi := e,
A0 (x) = xi and Γ = ΓA ∪ {xi 7→ τ }.
0

0

– Γ = ΓA , Γ0 = ΓA : Since xi is fresh, Γ = ΓA . Moreover, ΓA = Γ{x 7→ τ } = Γ0 .
– Γ, pc ` c: let Γ `HS e : τ0 . By the HS typing rule, we have τ = τ0 t pc. Moreover, we
have Γ ` e : τ due to Lemma 16 and the fact Γ = ΓA . By the construction, Γ(xi ) = τ .
Hence, Γ, pc ` xi := e.
– Dom(Γ) ⊆ A ∪ FVars(c): By the construction, Dom(Γ) = A ∪ {xi }.
• c1 ; c2 : from the construction rule, we have (pc, Γ, A){Jc1 K V c1 }(Γ00 , A00 ) ,→ Γ1 and
(pc, Γ00 , A00 ){Jc2 K V c2 }(Γ0 , A0 ) ,→ Γ2 for some Γ00 ,A00 , Γ1 and Γ2 . By the induction
hypothesis, we have
00

A
00
Γ = ΓA
1 ∧ Γ = Γ1 ∧ Dom(Γ1 ) ⊆ A ∪ FVars(c1 )
00

0

A
0
00
Γ00 = ΓA
2 ∧ Γ = Γ2 ∧ Dom(Γ2 ) ⊆ A ∪ FVars(c2 )

Γ1 , pc ` c1 ∧ Γ2 , pc ` c2
0

– Γ = ΓA , Γ0 = ΓA : By the construction, we have Γ1  Γ. Next, we check Γ2  Γ.
Due to the results above on Dom(Γ1 ) and Dom(Γ2 ), we know that if v ∈ Dom(Γ1 ) ∩
Dom(Γ2 ), then v ∈ A00 since FVars(c2 ) contain fresh variables generated in c2 (hence,
00
A00
00
not in A and c1 ). Therefore, Γ1 (v) = Γ2 (v) because ΓA
1 = Γ = Γ2 by the induction
hypothesis. Therefore, Γ2  Γ.
Moreover, by the definition, Γ = ΓA
1 is equivalent to ΓA 0 Γ1 . So we have ΓA  Γ,
and hence, Γ = ΓA . Similarly, we can prove that Γ0 = ΓA .
– Γ, pc ` c: we know that Γ, pc ` c1 ∧ Γ, pc ` c2 by Lemma 15. So Γ, pc ` c1 ; c2 .
– Dom(Γ) ⊆ A ∪ FVars(c): by the construction, Dom(Γ) = Dom(Γ1 ) ∪ Dom(Γ2 ). The
result is true since A00 ⊆ A ∪ FVars(c1 ) by Lemma 1 and Lemma 14.
• if (e) then c1 else c2 : from the construction rule, we have (pctτ, Γ, A){Jci K V ci }(Γi , Ai ) ,→
Γi for i ∈ {1, 2}, and Φ(A1 , A2 ) V A3 , where Γ `HS e : τ . By the induction hypothesis,
we have
Ai
Γ = ΓA
i ∧ Γi = Γi ∧ Γi , pc t τ ` ci ∧ Dom(Γi ) ⊆ A ∪ FVars(ci )

45

– Γ1  Γ, Γ2  Γ: By the construction, we have Γ1  Γ. Next, we check Γ2  Γ.
Since Dom(Γi ) ⊆ A ∪ FVars(ci ), if v ∈ Dom(Γ1 ) ∩ Dom(Γ2 ), then it must be true that
A
v ∈ A. Since we know that Γ = ΓA
1 and Γ = Γ2 from the induction hypothesis,
Γ(v) = Γ1 (v) = Γ2 (v) for such variables. Hence, we have Γ2  Γ.
A3
0
– Γ = ΓA , Γ0 = ΓA3 : We have Γ = ΓA since Γ = ΓA
1 and Γ1  Γ. To check Γ = Γ ,
consider v ∈ A3 ∩ (Dom(Γ1 ) ∪ Dom(Γ2 )). We use v to denote v .

∗ When v ∈ Dom(Γ1 ): we have v ∈ A or v ∈ FVars(c1 ) since Dom(Γ1 ) ⊆ A ∪
FVars(c1 ).
In the latter case, we have A1 (v) 6= A2 (v) since A2 ⊆ A∪FVars(c2 ) by Lemma 1
and Lemma 14. So A3 (v) must be a fresh variable by the definition of Φ, and hence
v 6∈ A3 . Contradiction.
So v ∈ A. By the assumption that v ∈ A3 and the definition of the Φ function, we
have v ∈ A1 and v ∈ A2 . That is, A(v) = A1 (v) = A2 (v). By Lemma 2, we have
Γ1 (v) = Γ(v) = Γ2 (v). Hence, Γ0 (v) = Γ1 (v) t Γ2 (v) = Γ(v) = Γ(v), where the
last equation is true since v ∈ A ∧ ΓA = Γ.
∗ When v ∈ Dom(Γ2 ): same argument as the case above.
Therefore, for any v ∈ A3 ∩ (Dom(Γ1 ) ∪ Dom(Γ2 )), Γ(v) = Γ0 (v). For other variables,
Γ(v) = Γ0 (v) is trivial from the construction. So Γ0 = ΓA3 .
– Γ, pc ` c: We know that he, Ai V e in the transformation assumption. Given ΓA = Γ,
we have Γ ` e : τ by Lemma 16. Moreover, Γ, pc t τ ` ci since Γ1  Γ, Γ2  Γ.
Furthermore, both A3 := A1 and A3 := A2 type-checks by our construction since:
1) by the defintion, the extra assignments only assign to fresh variables in A3 (i.e.,
v 6∈ A1 ∩ A2 ); 2) for those variables, we have Γ(v) = Γ0 (v) by the construction; 3) the
HS system ensures that Γi (v) v Γ0 (v) for i ∈ {1, 2} and pc t τ v Γi (v) for i = 1 or
2 (v must be assigned to under some branch since v 6∈ A1 ∩ A2 ). Therefore, we have
pc t τ v Γ0 (v) = Γ(v), and Γ(Ai (v)) = Γi (v) v Γ0 (v) = Γ(v).
– Dom(Γ) ⊆ A ∪ FVars(c): by the construction, Dom(Γ) = Dom(Γ1 ) ∪ Dom(Γ2 ) ∪ A3 .
By Lemma 14, A3 ⊆ A ∪ FVars(c). Result is true since we also have Dom(Γi ) ⊆
A ∪ FVars(ci ).
• while (e) c: by the construction rule, we have
Γ0 `HS e : τ, (τ t pc, Γ0 , A1 ){JcK V c0 }(Γ0 , A2 ) ,→ Γ0
By the induction hypothesis, we have
A2
0
0
0
1
Γ0 = ΓA
0 ∧ Γ = Γ0 ∧ Γ0 , pc t τ ` c ∧ Dom(Γ0 ) ⊆ A1 ∪ FVars(c )
1
– Γ = ΓA , Γ0 = ΓA1 : We have Γ0  Γ by the construction. Given Γ0 = ΓA
0 , we know
A
A
that Γ0 = Γ 1 . Next, we show that Γ = Γ .

∗ When v ∈ A∩Dom(Γ0 ) (we use v to denote v ). Since Dom(Γ0 ) ⊆ A1 ∪FVars(c0 )
from the induction hypothesis, we have v ∈ A1 or v is fresh in c0 . But the latter
must be false since v ∈ A. So v ∈ A1 .
46

From the construction rule assumption, we have pc `HS Γ{while (e) c}Γ0 . By
Lemma 1, we have hJwhile (e) cK, Ai V hc, A1 i. In addition, we just showed
that v ∈ A and v ∈ A1 . Hence, by Lemma 2, Γ(v) = Γ0 (v).
Because v ∈ A1 and v ∈ A, A(v) = A1 (v). Therefore, ΓA (v) = Γ(A(v)) =
Γ(A1 (v)) = Γ0 (v)(since Γ0 = ΓA1 ) = Γ(v).
∗ When v ∈ A − Dom(Γ0 ), the result is trivial by the construction.
– Γ, pc ` c: we have showed that ΓA1 = Γ0 . In the transformation assumption, we have
he, A1 i V e. So by Lemma 16, Γ ` e : τ . Moreover, we have Γ, pc t τ ` c0 by
Lemma 15 and the induction hypothesis Γ0 , pc t τ ` c0 . Next, we show that the extra
assignments (i.e., A1 := A and A1 := A2 ) type-check.
A2
A1
0
1
Since Γ0 = ΓA
= ΓA2 . Moreover,
0 ∧Γ = Γ0 by the induction hypothesis, we have Γ
by the same argument as in the “if” case, the LHS of A1 := A2 must have a level that
is higher than pc t τ in the HS system. So Γ, pc t τ ` A1 := A2 . Moreover, we know
that ∀v ∈ Vars. Γ(v) v Γ0 (v) in the HS system. Since ΓA = Γ and ΓA1 = Γ0 , we have
Γ, pc ` A1 := A.
– Dom(Γ) ⊆ A ∪ FVars(c): by the construction, Dom(Γ) = Dom(Γ0 ) ∪ A. From the
induction hypothesis, we have Dom(Γ0 ) ⊆ A1 ∪ FVars(c0 ). Hence, Dom(Γ0 ) ⊆ A1 ∪
FVars(c). We know from Lemmas 1 and 14 that A1 ⊆ A ∪ FVars(c). Hence,
Dom(Γ) ⊆ A ∪ FVars(c).


47

