Combining Type-Based Analysis and Model Checking
for Finding Counterexamples against Non-Interference
Hiroshi Unno

Naoki Kobayashi

Akinori Yonezawa

University of Tokyouhiro@yl.is.s.u-tokyo.ac.jp

Tohoku University
koba@ecei.tohoku.ac.jp

University of Tokyoyonezawa@yl.is.s.u-tokyo.ac.jp

Abstract
Type systems for secure information flow are useful for efficiently
checking that programs have secure information flow. They are,however, conservative, so that they often reject safe programs as
ill-typed. Accordingly, users have to check whether the rejected
programs indeed have insecure flows. To remedy this problem, we
propose a method for automatically finding a counterexample ofsecure information flow (input states that actually lead to leakageof secret information). Our method is a novel combination of typebased analysis and model checking; Suspicious execution paths(that may cause insecure information flow) are first found by using
the result of a type-based information flow analysis, and then amodel checker is used to check whether the paths are indeed unsafe.
We have formalized and implemented the method. The result of
preliminary experiments shows that our method can often findcounterexamples faster than a method using a model checker alone.
Categories and Subject Descriptors D.4.6 [Operating Systems]:
Security and Protection—Information flow controls; D.2.4 [Software Engineering]: Software/Program Verification—Model checking; F.3.1 [Logics and Meanings of Programs]: Specifying andVerifying and Reasoning about Programs
General Terms Security, Languages, Theory, Verification
Keywords non-interference, type system, model checking

it is rejected by type systems for secure information flow [20]1 . In
such a case, users have to manually inspect the program to check
whether the ill-typed program is indeed unsafe. Such manual inspection is error-prone; users may overlook real violation of secure
information flow.
To remedy the problem above, we propose a method for automatically finding input states that actually lead to leakage of secret information. More precisely, our method finds a counterexample against the non-interference property [3], a standard criterion
for secure information flow. The counterexample is a pair of input
states which only differ in the values of high-security variables andlead to output states that differ in the values of low-security variables. For example, a counterexample for the program:if h then l := 1 else l := 0is the pair ({h = true, l = 0}, {h = false, l = 0}). The
counterexample can convince the user that the program is indeed
unsafe.
Our method is a novel combination of type-based analysis andmodel checking. The result of a type-based information flow analysis is first used to find suspicious execution paths that may cause insecure information flow, and then a model checker is used to check
whether those paths are indeed unsafe (and if so, output a pair of
input states that go through the paths). To illustrate our approach,
we ask you to consider the following program (which is ill-typed
in the usual type system for secure information flow):
cex1

1.

Introduction

A number of type systems for secure information flow have recently been proposed [8, 9, 14, 15, 20, 21]. Those type systems
guarantee that well-typed programs never leak secret information,
so that the problem of checking secure information flow is reduced
to the problem of type checking. While the type-based information
flow analysis is fast and scalable, it is sometimes too conservativeand rejects innocent programs as ill-typed (i.e., false alarms may begenerated). For example, let h be a variable holding a high-security
value and l a variable that may be read by a low-security observer.
The assignment l := h − h does not leak secret information, but=

x0 := h;if b1 then x1 := x0 else . . .
..
.
if bn then xn := xn−1 else . . .
l := xn .

Throughout this paper, we assume that h is a high-security variable,
and l is a low-security variable. The program above leaks information about h if all the conditional expressions execute the thenbranch. Our method consists of the following two main phases.
A. Finding a pair of execution paths that may violate the noninterference property Let ρx be the security level of a variable
x. From Volpano and Smith’s type system, we obtain the following
constraints:ρh (= H) ≤ ρx0 ≤ ρx1 ≤ · · · ≤ ρxn−1 ≤ ρxn ≤ ρl (= L).
From the constraints, an inconsistent constraint H ≤ L is obtained.
Thus, we can conclude that the program is ill-typed. Actually, wec ACM, 2006. This is the author’s version of the work. It is posted here by permissionof ACM for your personal use. Not for redistribution. The definitive version was
published in the Proceedings of PLAS’06

1 Of course, this example is too simple and unlikely to appear in real
programs. In general, however, as the example shows, type-based analysis
is not good at analyzing value-dependent behavior of programs.

can obtain more information from the constraints: Notice that theexistence of a constraint ρx ≤ ρy implies that information about
the value of x may flow to the value of y. Thus, the above constraints tell us that information about the value stored in h may flow
to variable l through variables x0 , x1 , . . . , xn−1 , xn in this order.
From this reasoning, we can find the following execution path as a
suspicious execution path that may violate secure information flow:
πex1=

x0 := h;assume(b1 ); x1 := x0 ;..
.
assume(bn ); xn := xn−1 ;l := xn .

Here, the path is represented as a program with assume statement.
The statement assume(b1 ) above means that the then-branch of theoriginal conditional expression is chosen.
Let us consider another ill-typed program, which contains indirect information flow:
cex2 = if h then (l := 1)pc1 else (l := 0)pc2 .
From Volpano and Smith’s type system, we obtain the following
unsatisfiable constraints:ρh (= H) ≤ ρpc1 ≤ ρl (= L).
(We also get the constraint ρh ≤ ρpc2 ≤ ρl , but we only need
to focus on a subset of inconsistent constraints.) Here, ρpc is the
security level of information about whether the program point pc
is executed. From the constraints, we know that information about
the value stored in h may flow to pc1 , and then to l, so that thefollowing pair of execution paths (one of which visits pc1 , and theother does not) may violate the non-interference property:
Πex2 = ((assume(h); l := 1), (assume(!h); l := 0)).
Here, the path in the lefthand side takes the then-branch and thepath in the righthand side takes the else-branch.
B. Checking whether the pair of execution paths are unsafe The
next phase is to check whether the suspicious execution paths areindeed unsafe. For this purpose, we use the idea of model-checkingbased information flow analysis [1, 18]. Let (π1 , π2 ) be a pair of
suspicious execution paths that may violate the non-interference
property. Let π2 be the program obtained from π2 by renaming eachvariable x in π2 with x . Then, the two execution paths violate thenon-interference property if and only if the program π1 ; π2 withsome initial state satisfying x = x for every variable other thanhigh-security variables ends up in a state where l = l for somelow security variable l2 . We can use a model checker to check
whether the latter is the case, and if so, find an initial state. For
example, we can check whether the second program cex2 violates
secure information flow by checking whether the assertion in thefollowing program is violated:

to find a counterexample against the non-interference property. We,
however, expect that our combination of type-based analysis andmodel checking can often find counterexamples faster than themethod using model checking alone [1], since the type-based analysis allows us to prune innocent execution paths first, and to focus
on particular pairs of execution paths in the model checking phase.
For example, the program cex1 contains 2n execution paths (so thenumber of pairs of execution paths is 22n ), but after type-based
analysis, we only need to inspect a single pair of execution paths.
The expectation that our method often works faster is supported by
the result of preliminary experiments.
The rest of this paper is structured as follows. Section 2 introduces a simple imperative language and a type system for information flow analysis. The language and the type system are essentially the same as those of Volpano and Smith [20], except thatminor modification has been made for the formalization of our
method. Section 3 formalizes our method for finding a counterexample against non-interference. Section 4 and Section 5 report implementation of our method and experiments respectively. We haveused the BLAST model checker [5] and implemented our method
for a subset of C language. Section 6 compares our method withrelated work. Section 7 discusses future work and Section 8 concludes.

2.

Language and Type System

This section introduces a simple imperative language and a typesystem for information flow analysis.
2.1 Language
The abstract syntax of the language is defined as follows:(Expression)(Labeled Expression)(Command)

a
e
c

::=
::=
::=
|
|
|
|

x | n | a1 + a2 | !aaη
(skip)pc(x := e)pc
(c1 ; c2 )pc(if e then c1 else c2 )pc(while e do c)pc

Here, the meta-variables x and n range over program variables andintegers respectively. Labels ranged over by the meta-variables pc
and η are attached to commands and expressions respectively. We
assume that each command has a unique label pc and that eachlabeled expression has a unique label η. We write η2pc(η) forthe label pc of the command in which an expression labeled byη occurs.
We write (c, σ) ↓ σ  for the evaluation relation, meaning thatthe program c with the initial state σ ends up in the state σ  . The
formal definition of the relation is given in Figure 1. In the rules,
σ[x → n](y) has value n if x = y, and σ(y) otherwise.
2.2 Type System for Secure Information Flowassume(l = l );(assume(h); l := 1); (assume(!h ); l := 0);
assert(l = l ).

Our type system for secure information flow is essentially the sameas the standard type system of Volpano and Smith [20]. For the
purpose of formalizing our method, however, we present the typesystem in a slightly different way:

A model checker can find that the assertion is indeed violated, andgenerate a counterexample h = true, h = false, l = l = 0,
which is also a counterexample against the non-interference of theoriginal program cex2 .
Instead of combining type-based analysis and model checking
as described above, it is possible to use model checking alone [1]1. Instead of explicitly considering a lattice of security levels, wejust use variable names and labels (pc, η) as security levels. For
example, a variable name x also stands for the security level ofvalues stored in x.

2 Actually, part of π and π  can be shared by using the optimization
1
2
proposed by Terauchi and Aiken [18].

2. Because of the difference above, we have no usual type environment that maps each variable to its type (i.e., its security level
since we do not have compound data structures). Instead, we
have a set of constraints of the form τ1 ≤ τ2 (where τ1 , τ2 arex ≤ η ∈ C for each x ∈ FV(a)C  aη : η(skip, σ) ↓ σ(x, σ) ↓ σ(x)(n, σ) ↓ n(e, σ) ↓ n(x := e, σ) ↓ σ[x → n]

C  (skip)pc : pc cmd(c2 , σ  ) ↓ σ (c1 , σ) ↓ σ 
(c1 ; c2 , σ) ↓ σ Ce:τ
pc ≤ x ∈ Cτ ≤x∈CC  (x := e)pc : pc cmd(c1 , σ) ↓ σ (ai , σ) ↓ ni(for i = 1, 2) (e, σ) ↓ n(= 0)(if e then c1 else c2 , σ) ↓ σ (a1 + a2 , σ) ↓ n1 + n2(e, σ) ↓ n(= 0)(c, σ) ↓ σ(while e do c, σ  ) ↓ σ (while e do c, σ) ↓ σ (a, σ) ↓ 0(!a, σ) ↓ 1

Figure 1. The Evaluation Rules: (e, σ) ↓ e and (c, σ) ↓ σ variables or labels), which expresses the order of security levels(or, in which direction information may flow) as an assumptionof a type judgment.
The syntax of types and type constraints are defined as follows:(Data Type)(Constraints)

τ
C

::=
::=

x | η | pc
{τ1 ≤ τ1 , . . . , τn ≤ τn }(T-A SSIGN)(T-S EQ)Ce:τ
C  ci : τi cmdτ ≤ τi ∈ C(for i = 1, 2)
pc ≤ τi ∈ C
C  (if e then c1 else c2 )pc : pc cmd

(e, σ) ↓ 0(while e do c, σ) ↓ σ(T-S KIP)

pc ≤ τi ∈ C(for i = 1, 2)C  ci : τi cmd
C  (c1 ; c2 )pc : pc cmd(e, σ) ↓ 0(c2 , σ) ↓ σ (if e then c1 else c2 , σ) ↓ σ (a, σ) ↓ n(= 0)(!a, σ) ↓ 0(T-E XP)Ce:τ

C  c : τ  cmd
pc ≤ τ  ∈ C
C  (while e do c)pc : pc cmd(T-I F)τ ≤ τ ∈ C(T-W HILE)

Figure 2. The Typing Rules: C  e : τ and C  c : pc cmd(iii) σ1 =T2 σ2 . If there is no counterexample, we say that csatisfies (T1 , T2 )-non-interference. Here, σ1 =T σ2 means that
σ1 (z) = σ2 (z) holds for every z ∈ T . T is the complement of T .
The following is a standard type soundness theorem:
Theorem 2.1 (soundness). Let H be the set of high security variables and L be the set of low security variables. Suppose C |= h ≤l for every h ∈ H and l ∈ L. If C  c : pc cmd holds, then csatisfies (H, L)-non-interference.

A type judgment is of the form C  c : pc cmd (for a command)or C  e : τ (for a labeled expression). Intuitively, a judgment
C  c : pc cmd means that the command c conforms to thesecurity policy C, which describes in which direction information
may flow. τ1 ≤ τ2 means that the security level τ1 is lower than τ2 ;in other words, information on a value of level τ1 may flow to τ2 .
For example, {y ≤ x, pc ≤ x}  (x := y)pc : pc cmd is a valid
judgment, while {x ≤ y, pc ≤ x}  (x := y)pc : pc cmd is not.
The label pc in a judgment C  c : pc cmd expresses the security
level of information about whether c is executed (which is actually
the same as the label of c in our type system).
The typing rules are shown in Figure 2. In rule T-E XP, FV(a)denotes the set of variables occurring in a. We explain a few rules
below. In rule T-A SSIGN, the constraint pc ≤ x captures the factthat information about whether the command is executed may flow
to the value of variable x (since an observer may be able to guess
whether the command was executed by looking at the final valueof x). The constraint pc ≤ τi in rule T-S EQ captures the fact that
information about whether the command c1 ; c2 is executed flows
to information about whether the command c1 or c2 is executed(since if an observer knows that c1 has been executed, he or she
can infer that c1 ; c2 has been executed). We write C |= τ0 ≤ τn
if there exists τ1 , . . . , τn−1 such that τi ≤ τi+1 ∈ C for eachi(0 ≤ i < n).
In order to discuss the correctness of the type system, we formally define (T1 , T2 )-non-interference and its counterexample.
(T1 , T2 )-non-interference states that the final values of variables
in T2 never depend on the initial values of variables in T1 .

3.

Algorithm of Finding Counterexample

Definition 2.1. A pair of states (σ1 , σ2 ) is a counterexample
against (T1 , T2 )-non-interference of a program c if: (i) σ1 =T1 σ2 ,(ii) (c, σ1 ) ↓ σ1 and (c, σ2 ) ↓ σ2 for some σ1 and σ2 , and

3.1 Finding Suspicious Flow

As mentioned in Section 1, our method finds a pair of execution
paths that may violate the non-interference property (phase A), andthen checks whether the pair of execution paths are unsafe (phaseB). Each of (A) and (B) consists of the following sub-steps.
(A.1) Finding Suspicious Flow Perform type inference to find asuspicious flow of information from a high-security variable toa low-security variable that may be caused by a program.
(A.2) Path Pruning Generate a pair of execution paths that may
cause the suspicious flow of information found in A.1.
(B.1) Self-Composition Express the condition that the pair of execution paths (generated in A.2) satisfies the non-interference
property as a safety property, by using the idea of self-composition [1, 18].
(B.2) Finding Counterexample Use a model checker to find acounterexample (if any) against the safety property generated
in B.1. That counterexample serves as a counterexample against
the non-interference property of the original program.
We explain each step in Subsections 3.1-3.4 by using the following program cex3 :
«pc1
0 „
1pc0
η2 pc2
η1 then (x := h )
if
b
;
pc
η
B
C
else (x := 0 3 ) 3
B „«pc4 C@A
η5 pc5then (l := 1 )if (x = 1)η4
else (l := 0η6 )pc6
Given a program c, we first obtain the least set C of type constraints
such that C  c : pc cmd; Such an algorithm is easily obtained by(e, σ) ↓ n(= 0)(assume(e), σ) ↓ σ(e, σ) ↓ n(= 0)(assert(e), σ) ↓ σ(e, σ) ↓ 0(assert(e), σ) ↓ error(π1 , σ) ↓ σ (if ∗ then π1 else π2 , σ) ↓ σ (π2 , σ) ↓ σ(if ∗ then π1 else π2 , σ) ↓ σ (π, σ) ↓ σ (while ∗ do π, σ  ) ↓ σ (while ∗ do π, σ) ↓ σ (while ∗ do π, σ) ↓ σ

Figure 3. The Evaluation Rules for New Commands: (π, σ) ↓ σ (π, σ1 ) ↓ σ1
(π, σ2 ) ↓ σ2( π , σ1 , σ2 ) ↓ (σ1 , σ2 )(π1 , σ2 ) ↓ σ2(π2 , σ1 ) ↓ σ1(π1 ⊕ π2 , σ1 , σ2 ) ↓ (σ1 , σ2 )(Π1 , σ1 , σ2 ) ↓ (σ1 , σ2 )(Π2 , σ1 , σ2 ) ↓ (σ1 , σ2 )(Π1 ; Π2 , σ1 , σ2 ) ↓ (σ1 , σ2 )(π, σ2 ) ↓ σ2(π, σ1 ) ↓ σ1(repeat π , σ1 , σ2 ) ↓ (σ1 , σ2 )(repeat π , σ1 , σ2 ) ↓ (σ1 , σ2 )(π1 , σ1 ) ↓ σ1
(π2 , σ2 ) ↓ σ2(π1 ⊕ π2 , σ1 , σ2 ) ↓ (σ1 , σ2 ) (repeat π , σ1 , σ2 ) ↓ (σ1 , σ2 )Figure 4. The Evaluation
grams: (Π, σ1 , σ2 ) ↓ (σ1 , σ2 )

Rules

for

DoubledPro-

reading the typing rules in Figure 2 in a bottom-up manner. For
example, the following constraints are obtained for cex3 :C=Here, we use the first information flow path h · η2 · x · η4 · pc5 · l to
explain the succeeding steps.
Path Pruning

The next step is to construct a pair of execution paths that may
cause the suspicious information flow path obtained in the previous step (in other words, to prune paths that are irrelevant to theinformation flow path).
We first convert the information flow path to a sequence of
pc labels, which represents control flow information, by using thefunction f2pc given below. (Recall that η2pc(η) denotes the labelof the command in which η occurs.)

=
=
=


η2pc(η) · f2pc(y · τ )
η2pc(η) · pc · f2pc(y · τ )The second clause of the definition of f2pc captures the flow causedby an assignment, and the third clause captures the flow caused by
an if- or a while-statement.
The sequence generated by f2pc consists of the labels of ifstatements, while-statements and assignments. Intuitively, the labelof an if-statement occurring in the sequence expresses that two execution paths must split into the then-branch and the else-branch.
Similarly, the label of a while-statement means that the two execution paths must go through the while-loop the same number oftimes first, then the two must split: one of the paths must exit theloop and the other must not. The label of an assignment expresses
that one of the two execution paths must execute the assignment if
the two have splited, otherwise both of the two must execute theassignment. For example,
f2pc(h · η2 · x · η4 · pc5 · l) = pc2 · pc4 · pc5 .
This sequence intuitively expresses that two execution paths should
first go through the assignment labeled by pc2 , split into the thenand the else-branch of the if-statement labeled by pc4 , and then oneof the paths must go through the assignment labeled by pc5 .
Next, we construct the set of pairs of execution paths expressedby the sequence of pc labels. The set of pairs of execution paths isexpressed as a doubled program given below.
Definition 3.1. The sets of extended commands and doubled programs are given by the following syntax:(extended commands)π(doubled programs)

Π{pc0 ≤ pc1 , pc0 ≤ pc4 ,b ≤ η1 , η1 ≤ pc2 , η1 ≤ pc3 , pc1 ≤ pc2 , pc1 ≤ pc3 ,h ≤ η2 , η2 ≤ x, pc2 ≤ x, η3 ≤ x, pc3 ≤ x,x ≤ η4 , η4 ≤ pc5 , η4 ≤ pc6 , pc4 ≤ pc5 , pc4 ≤ pc6 ,η5 ≤ l, pc5 ≤ l, η6 ≤ l, pc6 ≤ l}.

Then, a suspicious flow (path) of information is constructedfrom the set of constraints. Let C be the least C  such that C   c :pc cmd. A sequence of data types τ1 ·. . .·τn is called an information
flow path from τ1 to τ2 of a program c, if τi ≤ τi+1 ∈ C for eachi(1 ≤ i ≤ n−1), and no variable occurs twice in the sequence. Let
flows(c, T1 , T2 ) denotes the set of information flow paths of c froman element of T1 to an element of T2 . We call an information flow
path τ1 ·. . .·τn suspicious if τ1 ·. . .·τn ∈ flows(c, H, L), where H
and L are sets of high- and low-security variables respectively. If c
has no suspicious flow, c has secure information flow. For example,
for the program cex3 , flows(cex3 , H, L) is:{h · η2 · x · η4 · pc5 · l, h · η2 · x · η4 · pc6 · l}.

3.2

f2pc(x)f2pc(x · η · y · τ )
 · pc · y · τ )f2pc(x · η · pc

::=
|
|
|
|
|
|
|
|
::=
|
|
|

skip
x := eassume(e)assert(e)π1 ; π2if e then π1 else π2
while e do π
if ∗ then π1 else π2
while ∗ do ππ
Π1 ; Π2
π1 ⊕ π2
repeat π

An extended command expresses a set of execution paths. The
new command assume(e) checks that the value of e is non-zero,and if so proceeds to the next command; If the value of e is 0,
the evaluation gets stuck (so that the command never terminates).
The command assert(e) is the same, except that it terminateswith a special state error if the value of e is 0. The assert
command is only used in the next step, for converting the noninterference property into a safety property (that the state error isnever reached). The command if ∗ then π1 else π2 executes π1
or π2 in a non-deterministic manner. The command while ∗ do πrepeats π an arbitrary number of times. The evaluation rules for the
new commands are given in Figure 3.
A doubled program expresses a set of pairs of execution paths.
π expresses that both of the two execution paths belong to (the setof execution paths expressed by) π. The doubled program π1 ⊕ π2
means that one of the execution paths belongs to π1 , while the otherbelongs to π2 . Π1 ; Π2 expresses the sequential composition of pathpairs. For example, (x := 1 ⊕ x := 2); (y := 1 ⊕ y := 2)
expresses the set of path pairs {((x := 1; y := 1), (x := 2; y :=2)), ((x := 1; y := 2), (x := 2; y := 1))}. repeat π expresses
that both of the two execution paths repeat paths which belong to πthe same number of times. We write (Π, σ1 , σ2 ) ↓ (σ1 , σ2 ) for theevaluation relation, meaning that the doubled program Π with theinitial states σ1 and σ2 ends up in the states σ1 and σ2 . Intuitively,
the relation expresses that Π contains a pair of execution paths, oneof which starts with state σ1 and ends in σ1 and the other starts
with state σ2 and ends in σ2 . The formal definition of the relation
is given in Figure 4.
We formalize a (non-deterministic) algorithm for constructing adoubled program from a command c and a sequence s of pc labels(generated by f2pc) by using a 4-tuple relation s  c −→ Π s .
Intuitively, the relation means that Π is the set of pairs of two
execution paths of the command c that conform to control flow
expressed by s\s (the sequence obtained by removing the postfixs from s).
The rules for s  c −→ Π s is given in Figure 5. In the rules,
PCs(c) returns the set of pc labels occurring in the command c,erase(c) erases all pc labels occurring in c, and length(s) returns
the length of the sequence s of pc labels. Let τ1 · . . . · τn be asuspicious information flow path obtained in the previous step. By
reading the rules in a bottom-up manner, we can obtain Π such that
.3 Then, the doubled programf2pc(τ1 · . . . · τn )  c −→ ΠΠ expresses a set of execution paths that may cause the suspicious
information flow.
We explain some rules below. In rule P-A SSIGN, the first label pc of the sequence indicates that both of the two execution
paths must execute (x := e)pc . Consequently, the algorithm consumes pc, and generates x := e . In rule P-I F -T HEN, the first label pc of the sequence (together with the condition pc ∈ PCs(c1 )indicates that both of the two execution paths must execute thethen-branch. Thus, the algorithm prunes the else-branch, and generates a doubled program which goes through the then-branch. In
rule P-I F -T HEN -I MP, the notation !e expresses a logical negationof the labeled expression e. The first label pc of the sequence
indicates that the two execution paths must split into the thenbranch c1 and the else-branch c2 . Suppose that the second label pc occurs in c1 . The algorithm consumes pc, and generates(assume(e); π)⊕(assume(!e); c2 ). Here, the extended command
π is generated from c1 by using the relation s  c 99K π s . The
relation s  c 99K πs is used to generate an extended command π that expresses a set of single execution paths that conformto the control flow expressed by s\s .
There are two rules P-W HILE and P-W HILE -I MP for whilestatements. Rule P-W HILE -I MP covers the case where an indirect
information flow (caused by the two execution paths going throughthe while-loop different numbers of times) occurs from the condition of the while-loop. The part repeat assume(e); erase(c)in the rule’s output means that the two execution paths must firstgo through the while-loop the same number of times, and the partπ ⊕ assume(!e) means that the paths must then split: one pathfurther goes through the while-loop, while the other path exits.
Rule P-W HILE handles the remaining case, where an information
flow first occurs inside the body of the while-loop. The first part
repeat assume(e); erase(c) of the rule’s output means that thetwo execution paths must go through the while-loop the same number of times, and the second part assume(e) ; Π means that theflow specified by pc must occur inside the body of the while-loop.
For example, the following doubled program {Πex3 } is obtained
from cex3 .
assume(b); x := h ;((assume(x = 1); l := 1) ⊕ (assume(x = 1); l := 0)).
3 There are finitely many such Π since the rules are non-deterministic. A
deterministic, complete algorithm for generating a single doubled commandfor each pair of c and τ1 · . . . · τn seems to be hard to construct. We discussa deterministic, incomplete version of the algorithm in Section 4.1.

In order to discuss the correctness of the path pruning, weformally define (T1 , T2 )-non-interference of a doubled programand its counterexample.
Definition 3.2. A pair of states (σ1 , σ2 ) is a counterexample
against (T1 , T2 )-non-interference of a doubled program Π if: (i)σ1 =T1 σ2 , (ii) (Π, σ1 , σ2 ) ↓ (σ1 , σ2 ) for some σ1 and σ2 , and(iii) σ1 =T2 σ2 . If there is no counterexample, we say that Πsatisfies (T1 , T2 )-non-interference.
The soundness and completeness of path pruning are stated as
the following theorems. Proofs are given in the full version of thispaper [19].
Theorem 3.1 (soundness). For any doubled program Π suchthat s  c −→ Πs is derivable for some s and s , ifa pair of states (σ1 , σ2 ) is a counterexample against (H, L)non-interference of Π, then (σ1 , σ2 ) is a counterexample against(H, L)-non-interference of c.
Theorem 3.2 (completeness). If a pair of states (σ1 , σ2 ) is acounterexample against (H, L)-non-interference of a program c,then there exist a doubled program Π and a sequence τ1 · · · τn thatsatisfy the following conditions:(i) τ1 · . . . · τn ∈ flows(c, H, L),(ii) f2pc(τ1 · . . . · τn )  c −→ Π , and(iii) (σ1 , σ2 ) is a counterexample against (H, {τn })-non-interferenceof Π.
Intuitively, the soundness means that if there exists a counterexample for a doubled program Π which is obtained from a programc, then it is a counterexample for c. The completeness means thatany counterexample for c is a counterexample for some doubled
program Π which is obtained from c.
3.3 Self-Composition
The next step is to turn the non-interference property of the doubled
program obtained in the previous step into a safety property, byusing the idea of self-composition [1]. As observed by Barthe etal. [1], a program c satisfies (T1 , T2 )-non-interference if and only
if the following self-composition of c never reach the state error.
assume(u = ξ(u)); c; ξ(c); assert(v = ξ(v )),Here, ξ(u) and ξ(c) are the sequence of variables and the command
obtained from u and c by renaming each variable x with a fresh
variable x . 
u is the sequence consisting of all the variables which
is not in T1 , and v is the sequence consisting of all the variables inT2 .
Similarly, a doubled program Π satisfies (T1 , T2 )-non-interference if and only if the following self-composition never reachthe state error.
assume(u = ξ(u)); Π; assert(v = ξ(v )),Here, · is defined in Figure 6. For a double program Π obtainedusing a suspicious flow τ1 ·. . .·τn , we use T1 = H and T2 = {τn }.
Actually, we adopt an optimized self-composition proposed by
Terauchi and Aiken [18] for statements whose effects never dependon the values of the variables in T1 . A predicate bd(e) holds if thevalue of e may depend on the values of the variables in T1 :bd(aη ) ≡ flows(c, T1 , {η}) = ∅.
For example, an optimized self-composition of Πex3 yields:
assume(l = l and x = x and b = b );assume(b); x := h; x := h ;assume(x = 1); l := 1; assume(x = 1); l := 0;
assert(l = l ).

s  c −→ erase(c)(P-E PSILON)s

pc · s  (x := e)pc −→ x := ess  c2 −→ Π2 s
s  c1 −→ Π1 s
s  c1 ; c2 −→ Π1 ; Π2 spc ∈ PCs(c1 )pc · s  c1 −→ Π s
pc · s  (if e then c1 else c2 )pc −→ assume(e) ; Π spc · s  c2 −→ Π spc ∈ PCs(c2 )pc · s  (if e then c1 else c2 )pc −→ assume(!e) ; Π spc · s  c1 99K π spc ∈ PCs(c1 )pc · pc · s  (if e then c1 else c2 )pc −→ (assume(e); π) ⊕ (assume(!e); erase(c2 )) spc · s  c2 99K π spc ∈ PCs(c2 )pc · pc · s  (if e then c1 else c2 )pc −→ (assume(e); erase(c1 )) ⊕ (assume(!e); π) slength(pc · s) > length(s )pc ∈ PCs(c)s  (while e do c)pc −→ Π s
pc · s  c −→ Π spcpc · s  (while e do c) −→ repeat assume(e); erase(c) ; assume(e) ; Π; Π s
pc · s  (while e do c)pc 99K π spc ∈ PCs(c)pc · pc · s  (while e do c)pc −→ repeat assume(e); erase(c) ; (π ⊕ assume(!e)) ss  c 99K erase(c) skip  x := e  x := e  assume(e)  assume(e)  π1 ; π2  if e then π1 else π2  if e then π1 else π2 

=
=
=
=
=
=
=
=

 while e do π  while e do π  if ∗ then π1 else π2 === while ∗ do π Π1 ; Π2 
π1 ⊕ π2 repeat π 

=
=
=
=

(P-S EQ)(P-I F -T HEN)
(P-I F -E LSE)
(P-I F -T HEN -I MP)(P-I F -E LSE -I MP)(P-W HILE)(P-W HILE -I MP)(Q-E PSILON)s

pc · s  (x := e)pc 99K x := e ss  c2 99K π2 ss  c1 99K π1 s
s  c1 ; c2 99K π1 ; π2 spc ∈ PCs(c1 )pc · s  c1 99K π spc · s  (if e then c1 else c2 )pc 99K assume(e); π spc · s  c2 99K π spc ∈ PCs(c2 )pc · s  (if e then c1 else c2 )pc 99K assume(!e); π slength(pc · s) > length(s )pc ∈ PCs(c)s  (while e do c)pc 99K π  spc · s  c 99K π spc · s  (while e do c)pc 99K while ∗ do (assume(e); erase(c)); assume(e); π; π Figure 5. The Path Pruning Rules: s  c −→ Π

(P-A SSIGN)s and s  c 99K π

skip
x := e; ξ(x) := xx := e; ξ(x) := ξ(e)assume(e)assume(e); assume(ξ(e))
 π1 ;  π2 
if e then  π1  else  π2 
if e then π1 else π2 ;if ξ(e) then ξ(π1 ) else ξ(π2 )while e do  π while e do π; while ξ(e) do ξ(π)
if ∗ then π1 else π2 ;if ∗ then ξ(π1 ) else ξ(π2 )while ∗ do π; while ∗ do ξ(π)
Π1 ; Π2 
if ∗ then π1 ; ξ(π2 ) else π2 ; ξ(π1 )while ∗ do  π Figure 6. The Self-Composition of Path Pairss(¬bd(e))(bd(e))(¬bd(e))(bd(e))(¬bd(e))(bd(e))(¬bd(e))(bd(e))(Q-A SSIGN)(Q-S EQ)(Q-I F -T HEN)
(Q-I F -E LSE)s

(Q-W HILE)

3.4

Finding Counterexample

The last step is to check whether the self-composition obtained in
the previous step reaches an error state, and generate a counterexample if so. In the experiments reported in Section 5, we used themodel checker BLAST [5] for this purpose. For example, the following counterexample is obtained for cex3 :l = l = 0, x = x = 0, b = b = true, h = 1, h = 0.

4.

Implementation

We have implemented our algorithm for a subset of C. We used
CIL [11] for parsing programs, and used BLAST model checker [5]for the fourth step of the algorithm described in Section 3. There aresome discrepancies between the theory described in Section 3 andthe actual implementation. First, we have traded the completenessfor the efficiency. Second, we have extended the target language
and its type system for information flow to handle C-specific features (pointers and jumps). We discuss the first point in Subsection 4.1 and then discuss the second point in Subsection 4.2.
4.1

Optimization of the Algorithm

Our implementation applies a few optimizations to speed up ouralgorithm for finding a counterexample. Some of them sacrifice thecompleteness of the algorithm. We think that losing the completeness is not so big a problem, since we can always revert to theusual self-composition approach [18] (or just give up) when ouralgorithm fails to find a counterexample.
• Prioritization of suspicious information flow paths

In the first step of our algorithm, more than one suspicious
information flow paths may be found. Our system inspects thosepaths one by one (until a counterexample is found), giving ahigher priority to information flow path which involves fewer
indirect flows.
• Deterministic algorithm for constructing doubled programs

In the second step, more than one doubled programs may begenerated for each suspicious information flow path. That is
because the rules in Figure 5 are non-deterministic; Note thatthe rule P-E PSILON is applicable to any command c. In theactual implementation, rules P-E PSILON and Q-E PSILON are
replaced with the following rules.
pc ∈/ P Cs(c)pc · s  c −→ erase(c)pc · s(P-E PSILON -D ET)

pc ∈/ P Cs(c)pc · s  c 99K erase(c)pc · s(Q-E PSILON -D ET)

Because of this change, the completeness (Theorem 3.2) is lostfor some tricky programs (see the full version [19]). However,this change makes the execution path generation algorithm deterministic (so that only one doubled program is generated foreach information flow path), which helps the system to avoid
performing duplicated computation for similar paths. As a result, a counterexample is often found much faster.
• A user can optionally instruct the system to replace the while-

loop with a loop-free program which simulates the while-loop
only a finite number of times. Again, this loses the completeness.
• Given a suspicious flow τ1 · . . . · τn and a doubled program Πwhich is constructed from the flow, the system tries to prove({τ1 }, {τn })-non-interference of Π instead of (H, {τn })-noninterference. That is partially justified by the fact that, if a pairof initial states ({h1 → n1 , h2 → n2 }, {h1 → n1 , h2 → n2 })is a counterexample, then ({h1 → n1 , h2 → n2 }, {h1 →n1 , h2 → n2 }) or ({h1 → n1 , h2 → n2 }, {h1 → n1 , h2 →n2 }) is also a counterexample unless c diverges for the initialstate {h1 → n1 , h2 → n2 }.
The optimization above has two kinds of effects. First, Terauchi and Aiken’s optimized self-composition becomes more
effective since we can set T1 = {τ1 } in the definition ofbd(e) in Section 3.3. Second, the search space explored by themodel checker is reduced by adding the assumption h1 = h1 ∧· · · ∧ hn = hn about the input states, where {h1 , . . . , hn } =H \ {τ1 }.
4.2 Extensions for C Programming Language
Our system supports various features of C programming language,
including pointers, arrays, structures, unions, and a restricted formof jumps. Our system does not support function pointers and recursive functions. The current implementation of type-based analysis
is intraprocedural. Thus, path pruning may only exploit local information within a function. Insecure information flows via global
variables are overlooked. However, the system may perform interprocedural analysis by inlining functions before a type-based analysis as we do in experiments in Section 5.
The type system and the algorithm for finding a counterexample have been extended accordingly. We briefly explain those extensions below.
4.2.1

Handling pointers, arrays, structures, and unions

Operations on arrays, structures, and unions are translated topointer operations. In order to track information flow caused bypointer operations, we introduce extended data types θ:
θ
τ

::=
::=

intτ | · · · | θ ptrτx | η | pc.

The typing rules for creating, dereferencing, and updating pointers(&e, *e, and *x = e) are similar to those of the type system forsecure information flow in ML [15].
To handle pointer arithmetic, we assume that programs arecompiled by using a C compiler ensuring the memory safety like
CCured [2, 12] and Fail-safe C [13], which guarantees that any
access to invalid memory regions (like an access beyond an arrayboundary) is caught at a run-time. (Without that assumption, we
have to assume that a pointer p + n may point to any part ofmemory.) Moreover, we force every element stored in the same
memory region (like an array, a structure, or a union) to havethe same security level. On that assumption, we use the following
typing rule for pointer arithmetic:
Γ; C  e : θ ptrτ1
Γ; C  n : intτ2
τ1 ≤ τ3 , τ 2 ≤ τ3 ∈ C
Γ; C  e + n : θ ptrτ34.2.2

Handling restricted control structures

C has jump instructions such as goto, break, and continue. Our
system supports only jumps into the outward and forward direction.
Two non-trivial extensions are required to handle the restrictedjumps.
First, we need to extend the type system so that it can handle
indirect flows caused by the restricted jumps. For example, thefollowing program has indirect flow from h to l:l := 0;while 1 do (if h then goto BL); l := 1; · · ·BL : · · ·For such a program, the type system must impose constraints {pc ≤pc1 , . . . , pc ≤ pcn }, where pc is the label of the goto-statement andpc1 , . . . , pcn are the labels of the statements that may be skippedby the jump.
Second, we need to modify the algorithm for making the selfcomposition (the third step of the algorithm described in Section 3).
In fact, the following self-composition of the program above isincorrect:
l := 0; l := l;while 1 do
(if h then goto BL); (if h then goto BL);l := 1; l := l; · · ·BL : · · ·Note that even if h is true, if h then · · · ; l := 1 should beexecuted since h may be false, in which case l := 1 should
be executed. For the program above, the current implementation
duplicates the while-statement as follows:
l := 0; l := l;while 1 do (if h then goto BL); l := 1; · · ·BL :while 1 do (if h then goto BL ); l := 1; · · ·BL : · · ·5.

Experiments

The main purpose of the experiments is to show that our methodof combining type-based analysis and model checking is effective
for showing that certain programs rejected by type-based analysis are indeed unsafe (by finding a counter-example against noninterference). In principle, our method should be effective also forcertifying that certain programs rejected by type-based analysis are
actually secure. The current implementation of our method is, however, not so effective for the latter purpose: See the discussion in
Section 7.2.
To evaluate our method, we have also implemented the original
self-composition method of Barthe et al. [1] and Terauchi and
Aiken’s optimized self-composition method [18], and compared
the running times for several programs. The result is summarizedin Table 1.
Programs expr1.c to expr4.c are artificial examples. We
examined several artificial examples. The program expr1.c is an
instance of cex1 discussed in Section 1. It has 216 paths, and only
one path leaks information of high to low through x0 to x16 . The
result shows that our method is much faster than the others.
expr2.c leaks information of high to low indirectly throughx0 to x15 . It has 216 paths, but non-interference is violated only
when two execution paths take different branches at every ifstatement. Previous methods [1, 18] have to inspect 216 × 216 =232 pairs of execution paths in the worst case to find a counterexample, while our method only needs to inspect 216 pairs of execution
paths. The table shows that our method is much faster than the others. The speed-up depends also on how BLAST search execution
paths, and expr2.c is an ideal case, where the execution paththat was first inspected by BLAST was a counterexample. To makefairer comparison, we also measured the running times for a variant expr2’.c, which is obtained by swapping bodies of thenand else-clauses of every if-statements and reducing the number of
if-statements to 8. The result shows that our method is still fasterthan the others.
expr3.c is a secure program, although the type system reports
a false alarm by detecting superfluous flows from high to x by
the if-statement. The running times show how long it takes forfoo(intH high){int b1, b2, b3, ..., b16;
int x0, x1, x2, ..., x16;
intL low;x0 = high;if (b1 ) { x1 = x0; }if (b2 ) { x2 = x1; }if (b3 ) { x3 = x2; }...
if (b16) { x16 = x15; }low = x16;}
Figure 7. A Program for Experiment (expr1.c)foo(intH high){int x0, x1, x2, ..., x16;
intL low;x0 = high;if (x0 ) { x1 = 1; }if (x1 ) { x2 = 1; }if (x2 ) { x3 = 1; }...
if (x15) { x16 = 1; }low = x16;}
Figure 8. A Program for Experiment (expr2.c)each system to report that programs are actually secure. The resultshows that our method is slightly slower than Terauchi and Aiken’s
method. It is because our current method generates and checks two
suspicious information flows: high to pc1 to x to low, and highto pc2 to x to low, where pc1 and pc2 are labels of then- and elseclauses of the if-statement.
In general, our current method is not good at proving that a
program satisfies non-interference. That is because our method may
generate multiple doubled programs, and runs a model checker
repeatedly for each of them. The doubled programs may share partof the original program, which result in duplicated computation by
the model checker. If combined with the compositional analysis
discussed in Section 7, however, our method would also be effectivefor verifying that a program is secure.
expr4.c uses 20 high-security variables and 20 low-security
variables. There is an insecure flow from high10 to low10 . From
the result of type inference, our system first infers that the only
possibility of information leakage is from highi to lowi (wherei ∈ {1, . . . , 20}), rather than an arbitrary combination of highiand lowj . As the table shows, our system runs faster than the othermethods, by taking advantage of that information .
In addition to the small artificial programs above, we havealso used a real program to compare our method with the others.
The program mod_imagemap.c is an Apache httpd server module mod_imagemap.c, which realizes server side image maps.
This program is known to have a Cross-Site Scripting vulnerability due to an omission of sanitizing HTTP_REFERER (fixed in
Apache httpd 2.2.1-dev). The system found suspicious flows fromreturn values of a function imap_url, which may be tainted by
HTTP_REFERER into arguments of a function ap_rvputs(),

Program
expr1.cexpr2.cexpr2’.c
expr3.cexpr4.cmod_imagemap.c

LOC
25
24
16
19
28
895

Naive Self-Composition (sec.)
2000.765
307.892
117.349
fail145.841658.357

Optimized Self-Composition (sec.)
75.657305.890
84.1111.774
31.857150.356

Our Method (sec.)
1.493
2.317
33.0272.181
8.848
117.849

Table 1. Experimental Results (Intel Pentium III 500MHz 256MB RAM)foo (intH high){int n, f1, f2, x, i;
intL low;while (0 < n) {f1 = f1 + f2; f2 = f1 - f2; n = n - 1;}
if (high) { x = 1; } else { x = 1; }while (i < f1) {low = low + x; i = i + 1;}}
Figure 9. A Program for Experiment (expr3.c)foo(intH high1, ..., intH high20){
int b1, b2, ..., b20;
intL low1, low2, ..., low20;
if(b1 ) { low1 = high1 - high1; }else if(b2 ) { low2 = high2 - high2; }...
else if(b9 ) { low9 = high9 - high9; }else if(b10) { low10 = high10; }else if(b11) { low11 = high11 - high11; }...
else if(b20) { low20 = high20 - high20; }}Figure 10. A Program for Experiment (expr4.c)which sends the arguments to the web browsers of clients. As thetable shows, our method could find a counterexample faster thanthe other methods, although ours was not significantly faster thanTerauchi and Aiken’s method. That seems to be because our system duplicated the body of while-loops by applying rule P-W HILE,
P-W HILE -I MP, and Q-W HILE, and the overhead caused by that
duplication canceled the gain obtained by the path pruning. If
closer cooperation with a model checker discussed in Section 7
were available, our method would be more effective for whilestatements.

6.

Related Work

Most closely related is the work by Terauchi and Aiken [18]. They
use type information to optimize the model-checking-based information flow analysis [1], but in a more limited manner than ours.
The idea of their optimization is to find expressions whose values do not depend on high-security values using type information, and avoid duplication of the expressions when making theself-composition. For example, the naive self-composition [1] of
while e do c yields while e do c; while ξ(e) do ξ(c) (whereξ renames each variable x with x ), while the optimized selfcomposition yields while e do (c; ξ(c)) when e does not dependon high-security values. This optimization avoids the duplicationof the expression e and (more importantly) the while-loop. Unlike
ours, however, their method does not use flow information (the suspicious information flow paths discussed in Section 3.1) obtainedby type inference.
Type-based analysis for secure information flow is applied tovarious languages such as simple imperative languages [20, 21] andfunctional languages [4, 14, 15], object-oriented languages [9], andconcurrent languages [6, 7, 17]. They are useful for conservatively
proving that a program has secure information flow, but not at
all for disproving it. Some systems based on such work [10, 16]
provide some useful error messages, showing how secret data may
possibly be leaked when a program is not well-typed. Unlike ours,
however, they cannot confirm that a certain program is indeed
unsafe, and generate a counterexample to show the violation of
non-interference.

7.

Future WorkWe discuss some future work in this section.
7.1 Compositional Analysis
We expect that we can make our algorithm more efficient by introducing compositional analysis. Recall that a suspicious information
flow path h · τ1 · . . . · τn · l indicates that information about the variable h may flow to l through τ1 , . . . , τn . That implies, if a flowfrom τi to τi+1 does not actually occur, then the whole information flow path h · τ1 · . . . · τn · l is superfluous. This observationsuggests us to inspect a suspicious information flow path in a compositional manner: to find a counterexample corresponding to theinformation flow path p1 p2 , we can first search counterexamples
corresponding to partial paths p1 and p2 , and combine them (andapply this recursively). This compositional analysis is, for example, effective for the program expr3.c discussed in Section 5.
From type inference, we obtain a suspicious information flow pathh · x · l (pc labels are omitted). In order to check whether there isindeed a flow from h to x, we only need to inspect the if-statement.
Since the if-statement actually does not leak information of h to x,
we can immediately conclude that expr3.c is safe, without everanalyzing the two while-loops.
Actually, we have already implemented a restricted form ofcompositional analysis sketched below (although that feature has
not been used in the experiment described in Section 5). Consider
the following program:
x := h − h; · · · ; l := x
From type inference, we obtain a suspicious information flow pathh · x · l. Since the possible flow from h to x is inferred fromthe assignment x := h − h, if there is indeed such a flow, thevalues of x and x in the self-composition should differ after theassignment. Thus, we can insert additional assume statement into
the self-composition:
assume(x = x and l = l and · · ·);x := h − h; x := h − h ; assume(x = x );..
.
l := x; l := x ;assert(l = l )The insertion of assume(x = x ) enables a model checker toconclude that no assertion violation occurs, without looking at thecode after assume(x = x ). (Note that the assert statement isnever reached since x = x does not hold.)
7.2

Closer Cooperation with a Model Checker

As the experiment in Section 5 shows, our method is sometimes
less efficient than the previous method [18]. The main source of theoverhead of our current system is that the system generates a doubled program and invokes a model checker for it repeatedly, once
for each suspicious information flow path, until a counterexample
is found. Moreover, each doubled program may contain duplicatedcopies of while-loops. Thus, some part of the original program isanalyzed by a model checker repeatedly. It seems possible to avoid
the duplicated computation to some extent by generating one doubled program for multiple suspicious flow paths, but closer cooperation with a model checker seems necessary to avoid the duplicatedcomputation completely. More cooperation with a model checker
seems also necessary for realizing the compositional analysis discussed above.

8.

Conclusion

We have formalized and implemented a novel method of combining type-based analysis and model checking to construct counterexamples against non-interference. The result of preliminary experiments shows that our method can often find counterexamples fasterthan previous methods based on model checking.

Acknowledgments
We thank Tachio Terauchi and Jun Furuse for many useful discussions. We will also like to thank anonymous referees for usefulcomments.

References[1] G. Barthe, P. R. D’Argenio, and T. Rezk. Secure information flow by
self-composition. In CSFW ’04, pages 100–114. IEEE, 2004.
[2] J. Condit, M. Harren, S. McPeak, G. C. Necula, and W. Weimer.
CCured in the real world. In PLDI ’03, pages 232–244. ACM, 2003.
[3] J. A. Goguen and J. Meseguer. Security policies and security models.
In Proceedings of the 3rd IEEE Symposium on Security and Privacy,
pages 11–20. IEEE, 1982.
[4] N. Heintze and J. G. Riecke. The SLam calculus: programming withsecrecy and integrity. In POPL ’98, pages 365–377. ACM, 1998.
[5] T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In POPL ’02, pages 58–70. ACM, 2002.
[6] K. Honda and N. Yoshida. A uniform type structure for secure
information flow. In POPL ’02, pages 81–92. ACM, 2002.
[7] N. Kobayashi. Type-based information flow analysis for the picalculus. Acta Informatica, 42(4-5):291–347, 2005.
[8] P. Li and S. Zdancewic. Practical information-flow control in webbased information systems. In CSFW ’05, pages 2–15. IEEE, 2005.
[9] A. C. Myers. JFlow: practical mostly-static information flow control.
In POPL ’99, pages 228–241. ACM, 1999.

[10] A. C. Myers, N. Nystrom, L. Zheng, and S. Zdancewic. Jif: Java
information flow. http://www.cs.cornell.edu/jif, 2001.
[11] G. C. Necula, S. McPeak, S. P. Rahul, and W. Weimer. CIL: Intermediate language and tools for analysis and transformation of C programs.
In CC ’02, volume 2304 of LNCS, pages 213–228. Springer, 2002.
[12] G. C. Necula, S. McPeak, and W. Weimer. CCured: type-safe
retrofitting of legacy code. In POPL ’02, pages 128–139. ACM, 2002.
[13] Y. Oiwa, S. Tatsurou, S. Eijiro, and Y. Akinori. Fail-safe ANSIC compiler: An approach to making C programs secure (progress
report). In ISSS ’02, volume 2609 of LNCS, pages 337–342. Springer,
2002.
[14] F. Pottier and S. Conchon. Information flow inference for free. In
ICFP ’00, pages 46–57. ACM, 2000.
[15] F. Pottier and V. Simonet. Information flow inference for ML. In
POPL ’02, pages 319–330. ACM, 2002.
[16] V. Simonet. Flow Caml in a nutshell. In Proceedings of the 1st
APPSEM-II workshop, pages 152–165, 2003.
[17] G. Smith and D. Volpano. Secure information flow in a multi-threaded
imperative language. In POPL ’98, pages 355–364. ACM, 1998.
[18] T. Terauchi and A. Aiken. Secure information flow as a safety problem. In SAS ’05, volume 3672 of LNCS, pages 352–367. Springer,
2005.
[19] H. Unno, N. Kobayashi, and A. Yonezawa. Combining type-based
analysis and model checking for finding counterexamples against noninterference. An extended version, available from http://www.
kb.ecei.tohoku.ac.jp/∼uhiro/, 2006.
[20] D. M. Volpano, C. Irvine, and G. Smith. A sound type system forsecure flow analysis. Journal of Computer Security, 4(2-3):167–187,
1996.
[21] D. M. Volpano and G. Smith. A type-based approach to program
security. In TAPSOFT ’97, volume 1214 of LNCS, pages 607–621.
Springer, 1997.