A Type System for Observational Determinism
Tachio Terauchi
Tohoku University
terauchi@ecei.tohoku.ac.jp

Abstract
Zdancewic and Myers introduced observational determinism as a scheduler independent notion of security for
concurrent programs. This paper proposes a type systemfor verifying observational determinism. Our type systemverifies observational determinism by itself, and does not
require the type checked program to be confluent. A polynomial time type inference algorithm is also presented.

1

Introduction

Non-interference is a property of a program which statesthat the program’s publicly observable (i.e., low security)
behavior is independent of its confidential (i.e., high security) inputs. Non-interference has applications in software
security. We refer to the survey by Sabelfeld and Myers [11]for a general overview.
Motivated by earlier work by Roscoe [10], Zdancewic
and Myers proposed observational determinism [14] as a
notion of non-interference for concurrent programs whichroughly says that a program is secure if and only if its
publicly observable behavior is independent of its confidential data and independent of process/thread scheduling. As
such, unlike other notions of non-interference such as possibilistic security, observational determinism implies security
regardless of the scheduler choice.
In the same paper, Zdancewic and Myers proposed a typesystem for enforcing observational determinism. However,their type system required the type checked program to beconfluent in order to be verified secure. Confluence, even if
relaxed to confluence up to observational parts of the program, can be a restrictive requirement. (Definitional observational determinism does not imply confluence.) This
paper presents, to the best of our knowledge, the first typesystem that verifies observational determinism by itself fornon-trivial concurrent programs. The type system integrates
a flow-based security analysis with a fractional capabilitiesbased determinism checker in a novel way to allow programs to be non-deterministic in non-security-relevant por-

e ::=
|
|
|
|
s ::=
|
|
|
|
|
|
|
|
|

x
`
n
e1 op e2!e
ref x = e in schan x in s
s1 ; s2e := eif e then s1 else s2
while e do s
spawn {s}send ewait eskip(variable)(location)(integer constant)(integer operations)(location read)(new location)(new channel)(sequence)(location write)(branch)(loop)(new thread)(signal send)(signal receive)(skip)

Figure 1. The syntax of the simple concurrent
language.

tions of the program. In particular, our type system does notforce confluence and can verify some non-confluent programs to be secure. In addition to added flexibility (e.g.,
being able to check determinism of concurrent reads), fractional capabilities enable efficient (polynomial time) type
inference algorithm via linear programming.

2

Preliminaries

To concretize the presentation, we focus on the simple
concurrent language shown in Figure 1. We briefly describe the syntax. Meta variables x, x1 , etc. range over(program) variables. Variables are immutable like in functional languages, whereas locations (i.e., first class reference cells) can be used for destructive updates. The construct ref x = e in s, creates a new location and initializes it to the result of evaluating e, and binds the location
to the variable x. Note that the language allows locations toappear in the source syntax. This is needed so that low se-curity variables and high security variables in the classicalinformation flow setting can be expressed as low security
locations and high security locations. The language contains branches and loops. The construct spawn {s} createsa new thread to evaluate s. Threads may synchronize eachother by sending signals over channels. Channels are dynamically created by chan x in s, which allocates a freshchannel, binds it to the variable x, and evaluates s. Signals
are “asynchronous” in the sense that the sender does notneed to wait for a receiver to send the signal. Finally, thelanguage contains integer constants. Binary (deterministic)
operations over integers (+, −, ×, ≤, etc.) are ranged overby the symbol op.
To describe non-interference, we consider programs withfree locations, some of which are classified as high security
locations or low security locations. The essence of information flow is to check if information contained in high security locations could leak to an attacker who can only observe
the contents of low security locations. For instance, the program below leaks information in the high security location`h to the low security location `l .
`l := 0; while !`h > 0 do (`l := !`l + 1; `h := !`h − 1)
We define the semantics of the language by small-step
reductions from states to states. A state is a triple (S, B, p)
where S is a store mapping locations to values (v, see below), B is a mapping from channel constants (c) to a nonzero integer indicating the number of pending signals, andp is a program state defined as follows.
v ::= c | ` | n
e ::= · · · | cp ::= s | p1 || p2
Here, the meta variable c ranges over channel constants.
Expressions are extended to contain channel constants. A
program state (p) is a parallel composition of (extended)statements.
We define the following general notations. Given a function f , f [u 7→ v] denotes the function {w 7→ f (w) | w ∈dom(f ) \ {u}} ∪ {u 7→ v}. Given a function f and a set
X ⊆ dom(f ), f |X denotes the restriction of f to X, thatis, {u 7→ f (u) | u ∈ X}. Given strings u and v, we writeu ∼ v if u and v are stutter equivalent. We write u ≺ v if
there exists a prefix w of v such that u ∼ w.
Figure 2 shows the reduction rules. The evaluation contexts are defined as follows.
E ::= [ ] | E; s | E||p | p||EThe reduction rules are mostly self-explanatory. The reduction rules use the evaluation rules for expressions of theform (S, e) ; v, also shown in Figure 2. In the rule forbinary operation, [[op]] denotes the standard semantics of(S, v) ; v(S, e1 ) ; n1 (S, e2 ) ; n2(S, e1 op e2 ) ; n1 [[op]]n2(S, e) ; `(S, !e) ; S(`)(S, e) ; n n 6= 0
(S, B, E[if e then s1 else s2 ]) → (S, B, E[s1 ])(S, e) ; 0(S, B, E[if e then s1 else s2 ]) → (S, B, E[s2 ])(S, B, E[while e do s])→ (S, B, E[if e then (s; while e do s) else skip])(S, B, E[spawn {s}]) → (S, B, E[skip] || s)(S, e) ; v ` ∈/ dom(S)(S, B, E[ref x = e in s]) → (S[` 7→ v], B, E[s[`/x]])(S, e1 ) ; ` (S, e2 ) ; v(S, B, E[e1 := e2 ]) → (S[` 7→ v], B, E[skip])c∈/ dom(B)(S, B, E[chan x in s]) → (S, B[c 7→ 0], E[s[c/x]])(S, e) ; c(S, B, E[send e]) → (S, B[c 7→ B(c) + 1], E[skip])(S, e) ; c B(c) > 0(S, B, E[wait e]) → (S, B[c 7→ B(c) − 1], E[skip])Figure 2. The reduction rules.
the binary operator op. We let the sequential composition
operator ; be associative with skip as an identity, that is,s1 ; s2 ; s3 = (s1 ; s2 ); s3 = s1 ; (s2 ; s3 )skip; s = s; skip = s
The bottom three rules handle communication of signals
over channels. A new channel is created with its numberof pending signals set to 0. When a sender sends a signal
over the channel, the number is incremented. The receiverblocks on a channel until there is a signal over the channel,
and decrements the number by receiving the signal.
A trace, T , is a finite sequence of states. For i ≤ |T |, wewrite T (i) to denote the ith state of T . We write (S, B, p) ⇓T if (S, B, p) = T (1) and T (i) → T (i + 1) for 1 ≤ i <|T |. We write s ⇓ T if (S, ∅, s) ⇓ T for some S suchthat dom(S) is the set of free locations in s and ran(S) ⊆ Z(for simplicity, we assume that the initial store only containsintegers). For a set of locations K ⊆ dom(S), we write(S, B, p)|K for S|K . We extend the same notation to traces,that is, T |K is a sequence of stores restricted to K such thatthe ith element is T (i)|K .
We define observational determinism following [14, 6]1 .
Informally, s is observationally deterministic if its trace restricted to the updates to the low security locations is independent of thread scheduling and the initial contents of thehigh security locations.
Definition 2.1 (Observational Determinism) Let s be a
program with no free variables and K be the set of freelocations of s. Let L ⊆ K be low security locations andH ⊆ K be high security locations. Let H̄ = K \ H. We
say that s is observationally deterministic w.r.t. (L, H) if for
any T, T 0 such that s ⇓ T , s ⇓ T 0 , and T (1)|H̄ = T 0 (1)|H̄ ,we have T |L ≺ T 0 |L or T 0 |L ≺ T |L .
Observational determinism is a quite strong notion of security. For instance, observational determinism implies deterministic updates to the low security locations (because
t|H̄ = t|H̄ for any state t). Therefore, for example,
the following program is not observationally deterministic
w.r.t. ({`l }, ∅). (There are no high security locations.)
spawn {`l := 0}; `l := 1
For motivation behind the definition of observational determinism, we refer to the paper by Zdancewic and Myers [14](or the paper by Huisman et al. [6]) which contains excellent
examples illustrating why a more relaxed notion of security
may be problematic.

3

The Type System

We present a type system that guarantees that a typable
program is observationally deterministic. We informallydescribe the basic idea. In short, the type system combines
a flow-based analysis for non-interference [14] with a fractional capability-based determinism checker for concurrent
programs [2, 13]. Intuitively, the type system applies a security flow analysis to check that there is no flow (including
implicit flow from branches and loops) from high security
level to low security level, and also infers the program parts
that must be at low security level and therefore need to be
deterministic. Then, the type system applies a fractional
capability analysis to verify that those parts are indeed deterministic. Only checking determinism for parts of the program allows the type system to accept programs that are nottotally deterministic (see Section 3.1 and 4 for some examples.)1 The definition given here differs somewhat from those in [14] and [6].
It turns out that there are some subtle issues with their definitions, which
are discussed in Appendix A

The following example illustrates the basic idea.
ref x = 0 in
spawn {x := 1};
if !x then `l := 0 else `l := 1
Note that the program is not observationally deterministic
w.r.t. ({`l }, ∅) because depending on the thread scheduling,`l is either assigned 0 or 1. To detect this, the type system
first infers that, for `l to be at low security level, the branch
condition !x must be at low security level and thus needs tobe deterministic. Then, the type system tries to find a fractional capability assignment that would prove the determinism of !x, and fails to do so (because it is non-deterministic),
and the program is rejected as possibly not observationallydeterministic.
We now formally describe the type system. The types
are defined as follows.
κ ∈ Abstract Locationsγ ∈ Abstract Channels
ρ ::= κ | γ
q ::= h | lτ ::= intq | ref(κ, τ )q | chan(γ, Ψ)q
Each type is qualified by a security level: h or l. Intuitively,
values of the type qualified by h may depend on high security information or thread scheduling, whereas those qualified by l are guaranteed to be independent of them. Security
levels form the usual two point lattice such that l v h andh 6v l. The least upper bound of q1 and q2 is written q1 t q2 .
The accessor function qual and ty are defined as follows.
qual(intq ) = q
qual(ref(κ, τ )q ) = q
qual(chan(γ, Ψ)q ) = q
ty(intq ) = intty(ref(κ, τ )q ) = ref(κ, τ )ty(chan(γ, Ψ)q ) = chan(γ, Ψ)Security levels induce the subtyping relationqual(τ1 ) v qual(τ2 ) ty(τ1 ) = ty(τ2 )τ1 v τ2
The type system represents locations statically as abstract locations, ranged over by meta variables κ, κ1 , etc.
Each abstract location denotes a set of (concrete) locations so that a location of the type ref(κ, τ )q is in the set
represented by κ. Similarly, channels are represented byas abstract channels, ranged over by γ, γ1 , etc., each denoting a set of (concrete) channels. Meta variables ρ, ρ1 ,etc. range over abstract resources, used to refer to bothabstract locations and abstract channels. Meta variables
Ψ, Ψ1 , etc. range over capability mappings, which are functions from abstract resources to non-negative rational numbers [0, ∞).

There are two reasons for using abstract resources. One
is to allow aliasing of resources, because both locations andchannels are first class objects and so the static system cannot track their identity precisely. The second reason is togroup all low security locations in the same abstract location. The type system ensures that accesses to l-level locations (i.e., locations with the type of the form ref(κ, τ )q
such that qual(τ ) = l) happen observationally deterministically at the granularity of abstract resources. Therefore, if
multiple l-level locations are grouped in the same abstract
location, then access to all those locations as a whole happen observationally deterministically.
Recall capability mapping (Ψ, Ψ1 , etc.) is a function
from abstract resources to non-negative rational numbers[0, ∞). A capability mapping denotes access capabilities toabstract resources. Each thread holds some amount of capabilities, representing the access capabilities of the thread.
Only the threads holding the capability Ψ such that
Ψ(κ) ≥ 1 are allowed to write to an l-level abstract location κ, whereas only the threads holding the capability Ψsuch that Ψ(κ) > 0 are allowed to read low security values.
(Therefore, the write capability implies the read capability.)
The type system ensures that the total amount of capabilities
summed across all live threads is at most 1 for any abstraction location. This guarantees that there are no other threads
that can access an l-level location when some thread is writing to the location, guaranteeing deterministic low-security
accesses to the location.
For example, this scheme soundly rejects the following
program where `l is a low security location. To see this, notethat in order to type check both writes to `l , both threads
must be given the capability 1 to access the abstract location
representing `l , but this violates the “at most 1” criteria.
spawn {`l := 0}; `l := 1
Only demanding non-negative rationals for reads allow parallel deterministic reads. For instance, the following program, where `l is a low security location, can be typechecked by giving both the spawned and the spawner
threads a fractional amount (e.g., 0.5) of the capability toaccess x.
ref x = 0 in
ref y = 0 in
spawn {`l := !x}; y := !x
The type system allows capability passing between
threads so that multiple threads may access the same l-level
location. Capabilities can be passed when threads synchronize over a channel. For instance, to type check the following program (where `l is a low security location), wepass the capability to access `l initially held by the spawned
thread (i.e., the one that does `l := 0) to the spawner thread(i.e., the one that does `l := 1) when sending a signal overthe channel c.
chan c inspawn {`l := 0; send c};
wait c; `l := 1
To statically reason about capability passing, a channel typecontains a capability mapping indicating the amount of capabilities passed from the sender to the receiver when communicating over the channel. That is, a channel of the type
type chan(γ, Ψ)q can be used to pass Ψ amount of capabilities from the sender to the receiver.
It is necessary to check that capability passing happens
observationally deterministically to disallow cases such as
the one below where `l is a low security location.
chan c inspawn {wait c; `l := 0};
spawn {wait c; `l := 1};
send cTo this end, the type system only allows the threads holding
the capability Ψ such that Ψ(γ) ≥ 1 to receive capabilities from channels in γ. As with abstract locations, the typesystem ensures that the total amount of capabilities summed
across all live threads is at most 1 for an abstract channel.
Therefore, at any point in time, there is at most one threadthat can receive capabilities from the channel. As with locations, capabilities to access channels can also be passed,
allowing multiple threads to use the same channel to passcapabilities.
We define arithmetic operations over capabilities. The
addition and subtraction of capability mappings are defined
point-wise as Ψ1 + Ψ2 = λρ.Ψ1 (ρ) + Ψ2 (ρ) and Ψ1 −
Ψ2 = λρ.Ψ1 (ρ) − Ψ2 (ρ). Because capabilities must be
non-negative, Ψ1 − Ψ2 is undefined if Ψ1 (ρ) < Ψ2 (ρ) forsome ρ. The relation Ψ1 ≥ Ψ2 is defined as ∀ρ.Ψ1 (ρ) ≥Ψ2 (ρ), and Ψ1 > Ψ2 is defined as ∀ρ.Ψ1 (ρ) > Ψ2 (ρ). For
convenience, we let 0 denote a constant capability mappingthat maps all abstract resources to 0, that is, 0 = λρ.0.
Therefore, for example, 0 [ρ 7→ 1] is a capability mappingthat maps ρ to 1 and ρ0 to 0 for all ρ0 6= ρ.
Figure 3 and Figure 4 show the type checking rules. The
judgement for expressions is of the form Γ, Ψ ` e : τ whereΓ is a type environment mapping variables and locations totheir types, Ψ is the pre-capability before the evaluation ofe (and after, because expressions do not change thread’s capabilities), and τ is the type of e. The judgement for statements is of the form Γ, Ψ1 , q ` s : Ψ2 where the context security level q is used to capture implicit flow inducedby branches, Ψ1 is the pre-capability of s, and the postcapability Ψ2 is the capability after the evaluation of s.
We briefly discuss each rule. VAR, INT, LOC, OP,
SEQ, and SKIP are self-explanatory. IF and WHILE increase the security level inside the branch/loop bodies byΓ, Ψ ` x : Γ(x)VARΓ, Ψ ` n : intq1

INT

LOC

Γ, Ψ ` ` : Γ(`)Γ, Ψ ` e1 : intq1 Γ, Ψ1 ` e2 : intq2 q1 t q2 v q3
OPΓ, Ψ ` e1 op e2 : intq3
Γ, Ψ ` e : ref(κ, τ1 )q1 τ1 v τ q1 v qual(τ )qual(τ ) = l ⇒ Ψ(κ) > 0
READΓ, Ψ ` !e : τ
Figure 3. The type checking rules for expressions.
Γ, Ψ ` e : intq1

Γ, Ψ, q2 ` s1 : Ψ1 Γ, Ψ, q2 ` s2 : Ψ2 q t q1 v q2
Γ, Ψ, q ` if e then s1 else s2 : Ψ3

Γ, Ψ1 ` e : intq1

Γ, Ψ1 , q2 ` s : Ψ2 q t q1 v q2 Ψ2 ≥ Ψ1
Γ, Ψ, q ` while e do s : Ψ1

Γ, Ψ, q ` skip : ΨΓ, Ψ ` e : τ1

SKIP

Ψ1 ≥ Ψ3Ψ ≥ Ψ1Ψ2 ≥ Ψ3IF

WHILE

Γ, Ψ, q ` s1 : Ψ1 Γ, Ψ1 , q ` s2 : Ψ2
SEQΓ, Ψ, q ` s1 ; s2 : Ψ2

q1

τ1 v τ Γ[x 7→ ref(κ, τ ) ], Ψ, q ` s : Ψ1
Γ, Ψ, q ` ref x = e in s : Ψ1

REFΓ, Ψ ` e1 : ref(κ, τ )q1 Γ, Ψ ` e2 : τ1 τ1 v τq t q1 v qual(τ ) qual(τ ) = l ⇒ Ψ(κ) ≥ 1
Γ, Ψ, q ` e1 := e2 : ΨWRITEΓ, Ψ1 , q ` s : Ψ2
Γ[x 7→ chan(γ, Ψ1 )q1 ], Ψ, q ` s : Ψ2
SPAWN
NEWC
Γ, Ψ, q ` spawn {s} : Ψ − Ψ1
Γ, Ψ, q ` chan x in s : Ψ2
Γ, Ψ ` e : chan(γ, Ψ1 )lSENDΓ, Ψ, l ` send e : Ψ − Ψ1Γ, Ψ ` e : chan(γ, Ψ1 )l 0 < Ψ1 ⇒ Ψ(γ) ≥ 1
Γ, Ψ, l ` wait e : Ψ + Ψ1

RECV

Figure 4. The type checking rules for statements.
the security level of the branch/loop condition to accountfor the implicit information flow. Note that these rules
make sure that capabilities are “conserved” through the sequential flow of computation, that is, the post-capability
may not exceed their pre-capability. At SPAWN, the parent thread gives a part of its capability (Ψ1 ) to the newly
created thread, and so Ψ − Ψ1 amount of capability is left
for the continuation of the parent thread.
REF, READ, and WRITE type location accesses. REF
is self-explanatory. At WRITE, the hypothesis q t q1 v
qual(τ ) ensures that the context security level (i.e., q) is
below that of the location (i.e., qual(τ )). This is needed todisallow implicit information flow such asif !`h then `l := 0 else `l := 1
where `h is a high security location and `l is a low security
location. Also, the security level of the reference (i.e., q1 )must be below qual(τ ). This is needed because locations
are first class, and disallows programs like the one below.
ref x = `l1 in
if !`h then x := `l2 else skip;`l1 := 1;
where `h is a high security location and `l1 , `l2 are low
security locations. As remarked before, the hypothesisqual(τ ) = ` ⇒ Ψ(κ) ≥ 1 asserts that to write to a low
security location, the thread must own the full (i.e., 1) capability to access it. Note that WRITE allows writing a low
security level value to an h-level location. In such a case,no capability constraints are imposed.
As remarked before READ’s hypothesis qual(τ ) = l ⇒Ψ(κ) > 0 ensures that only a thread holding a non-zero
capability may read a low security value from the location.
Also, READ ensures q1 v qual(τ ). As in WRITE, this isΓ, Ψ ` e : chan(γ, Ψ1 )q1
0 < Ψ1 ⇒ q = q1 = l
SEND’Γ, Ψ, q ` send e, Ψ − Ψ1q1

Γ, Ψ ` e : chan(γ, Ψ1 )0 < Ψ1 ⇒ (Ψ(γ) ≥ 1 ∧ q = q1 = l)RECV’Γ, Ψ, q ` wait e : Ψ + Ψ1
Figure 5. The relaxed rules for signal send
and receive.

curity level constraints, and make type inference somewhat
more complex.
We now state the soundness of the type system.
Definition 3.1 (Well-typed Program) Let s be a programwith no free variables and L, H be its low security locations
and high security locations. We write ` (s, L, H) if there
exists Γ such that
(1) For all free location ` of s, Γ(`) = ref(κ, intq1 )q2 forsome κ, q1 , q2 .
(2) For all ` ∈ H, Γ(`) = ref(κ, inth )q for some κ, q.
(3) There exists κ such that for all ` ∈ L, Γ(`) =ref(κ, intl )q for some q.

needed because locations are first class and disallows programs like the one below.
ref x = `a inif !`h then x := `b else skip;`l := !!xwhere `h is a high security location and `l is a low security locations. (`a , `b are some arbitrary locations.) Notethat READ allows reading a high security value from an llevel location. In such a case, no capability constraints are
imposed.
NEWC, SEND, and RECV handle signals. NEWC
checks channel allocation, and is self-explanatory. Note thatthe post-capabilities in SEND and RECV reflect the capability passing remarked earlier, that is, the capability Ψ1 ispassed from the sender to the receiver.
At RECV, the hypothesis 0 < Ψ1 ⇒ Ψ(γ) ≥ 1 ensuresthat if the passed capability is non-zero, then the threadmust have the full capability to access the channel. As remarked before, this is needed to ensure that the capability
passing happens deterministically. SEND and RECV require the context security level and the security level of thechannel to be at l. This disallows cases such as the one
below where `h is a high security location and `l is a low
security location.
chan c inchan d inspawn {wait c; `l := 0};
spawn {wait d; `l := 1};
if !`h then send c; else send d;
Note that this program would type check if the hypothesis
were missing because it would allow sending the capability
to access `l via both the channel c and d. The type systemremains sound if the rule is relaxed so that the security levels need to be l only if the passed capability is non-zero,as shown in Figure 5. Unfortunately, these rules induce
cyclic dependencies between capability constraints and se-(4) Γ, Ψ, q ` s : Ψ0 for some Ψ, q, Ψ0 such that Ψ(ρ) ≤ 1
for all ρ.
The condition (1) follows from the fact that initial stores
map locations to integers. The condition (2) ensures thathigh security locations have high security level. The condition (3) ensures that low security locations share the same
abstract location, and have low security level. The condition (4) ensures that s can be typed with a pre-capability ofat most 1 for any abstract resource.
Theorem 3.2 (Soundness) If ` (s, L, H) then s is observationally deterministic w.r.t. (L, H).
The proof of the theorem appears in Appendix B.

3.1

ExampleConsider the following program.
chan c inspawn {
`a := 1;
wait c;if !`h then `b := 1 else 0;`2 := 1;send c};`a := 0; `b := 0; `c := 0;
send c; wait c;`l := !`cThe
programisobservationallydeterministic
w.r.t. ({`l }, {`h }) as the content of `c at the last lineof the program must be 1 because the reads and writes aresynchronized properly via communication over the channelc. Note that the contents of `a at the end of the program is
non-deterministic as it depends on the thread scheduling,
and the content of `b at the end of the program depends onthe value of the high security location.
The type system can type check this program. The
key is to give the channel c the type of the form

ref x = 0 in
ref i = 0 in
ref j = 0 inchan c1 inchan c2 inchan d inspawn {while !i < 10 do(x := !i; i := !i + 1; send c1 ; wait c2 )};spawn {while 1; do(wait c1 ; wait d; `l := !x; send c2 )};spawn {while !j < 10 do (j := !j + 1; send d)};spawn {while 1 do wait d}Figure 6. Producer-consumer example.
chan(γ, 0 [κ 7→ 1])q where `c is given the type of the form
ref(κ, intl )l . This allows passing of the (full) capability toaccess `c to the spawned thread after the write to `c by the
spawner thread, and back to the spawner thread after the
spawned thread is done with its write to `c . Thus, !`c at thelast line can be given a low security type, and the program
type checks.

4

Confluence and Observational Determinism

Note that the example above is not confluent as updates
to `a cannot be “undone”, though the low security part ofthe store (i.e., `l ) is confluent. However, in general, observational determinism does not imply confluence even restricted to the low security locations. We show that our typesystem can actually check some of such “observationallynon-confluent” programs to be observationally deterministic.
Let t1 →∗ t2 be 0 or more reduction steps from t1 to
t2 . Formally, a state t is said to be confluent if t →∗ t1 andt →∗ t2 imply that there exist states t01 , t02 such that t1 →∗t01 and t1 →∗ t02 and t01 ≡ t02 where ≡ is some suitableequivalence relation. A program s is confluent if for all S
such that dom(S) is the set of free locations in s, (S, ∅, s)is confluent. A reasonable choice for ≡ may be equality
up to renaming of variables/locations/channels and process
reordering. A more relaxed notion can be obtained by only
requiring such a relation on the stores, or some portion of
the stores.
Consider the simple producer-consumer program shownin Figure 6. The program spawns four threads, the firstthread is the producer thread that writes 0, 1, . . . , 9 to x. The
second thread is the consumer thread that reads from x. Viachannels c1 and c2 , the second thread (the consumer) synchronizes with the first thread (the producer) to read (someprefix of ) 0, 1, . . . 9. The consumer thread also waits on signals sent via d, which are sent by the third thread. Finally,
the fourth thread also receives signals via d.
The program is observationally deterministic
w.r.t. ({`l }, ∅). Note that because there are no highsecurity locations, the only source of information leak isthrough non-determinism due to the thread scheduling.
The program is observationally deterministic because theupdates to `l is some prefix of 0, 1, . . . , 9 regardless ofthe thread scheduling. Our type system is able to typecheck this program by assigning the location `l the typeref(κ, int)l , channels c1 , c2 the type chan(γ, 0 [κ 7→ 1])l forsome γ, and channel d the type chan(γ 0 , 0 )q for some q, γ 0 .
This program is not confluent even restricted to the low
security location `l . To see this, consider a series of reductions in which the loop in the fourth thread waits on d until
after the consumer thread writes to `l ten times. In this series, the updates to `l are exactly 0, 1, . . . , 9. Now, consider
another series of execution where the fourth thread receives
a signal from d at least once before the consumer thread
writes to `l ten times. Then, the sequence of updates to `l issome strict prefix of 0, 1, . . . , 9. It is impossible for the twoseries to reduce to states that have the same value for `l , inparticular, the latter series cannot reach the 10th update.
In general, even when restricted to differences in low
security locations, it would be difficult to guarantee confluence because it would mean that any potential operation
preceding an update to a low security location must be deterministically blocking or non-blocking. In particular, this
implies that termination/non-termination of the preceding
loops must be deterministic.

5

Type Inference

We give a polynomial time type inference algorithm(more precisely, a typability algorithm). That is, given(s, L, H), the algorithm decides whether ` (s, L, H). We
informally describe the algorithm. The algorithm is separated in three phases. The first phase is a security flow
analysis phase that decorates the derivation tree with security levels. We make the first phase find the greatest security level assignments (i.e., preferring h over l wherever
possible). If no solution can be found in this phase (e.g.,trying to find q such that h v q and q v l), the algorithm
rejects the program as untypable. The first phase ignores
capability constraints. The second phase finds capability
assignments for channels, which involves resolving the constraints 0 < Ψ1 ⇒ Ψ(γ) ≥ 1 from RECV, i.e., determines
when Ψ2 (γ) < 1 so that it must be the case that Ψ = 0 .
Finally, the third phase uses the information obtained fromthe first two phases to find capability assignments for locations. The third phase uses the inferred security levels todetermine which Ψ(ρ) > 0 and Ψ(ρ) ≥ 1 constraints to dis-∆, ϕ ` x : ∆(x); ∅α, r fresh∆, ϕ ` n : αr ; {α = int}∆, ϕ ` ` : ∆(`); ∅∆, ϕ1 ` e1 : α1r1 ; C1 ∆, ϕ2 ` e2 : α2r2 ; C2 r fresh∆, ϕ1 ` e1 op e2 : α2r ; C1 ∪ C2 ∪ {α1 = α2 = int, r1 v r, r2 v r, ϕ1 = ϕ2 }∆, ϕ ` e : αr ; C α1 , r1 , r2 , % freshr1∆, ϕ ` !e : α1 ; C ∪ {α = ref(%, α1r2 ), r v r1 , r2 v r1 , (r1 = l ⇒ ϕ(%) > 0)}∆, ϕ ` e : α1r1 ; C1 ∆, ϕ1 , r ` s : ϕ2 ; C2 %, r2 , r3 fresh∆, ϕ, r ` ref x = e in s : ϕ2 ; C1 ∪ C2 ∪ {ref(%, α1r3 )r2 = ∆(x), r1 v r3 , ϕ = ϕ1 }∆, ϕ ` e : αr1 ; C r, ζ, ϕ1 , ϕ2 fresh∆, ϕ, r ` wait e : ϕ2 ; C ∪ {α = chan(ζ, ϕ1 ), r = r1 = l, ϕ2 = ϕ + ϕ1 , (0 < ϕ1 ⇒ ϕ(ζ) ≥ 1)}
Figure 7. Representative type inference rules.
charge (i.e., the hypothesis qual(τ ) = l ⇒ . . . at WRITE
and READ). The second and the third phase finds the capability assignments by reducing the capability constraint
satisfaction problem to linear programming instances.

5.1

Phase 1

The first phase is mostly a standard unification-based
type inference, generating security level constraints and capability constraints on the side. Figure 7 shows a few
representative constraint generation rules (corresponding to
the type rules VAR, INT, LOC, OP, READ, REF, andRECV). Here, r’s are security level variables, ϕ’s are capability mapping variables, α’s are type variables (actually,
types with the outer-most security level stripped), %’s are abstract location variables, and ζ’s are abstract channel variables. Each rule is a straightforward syntax-directed constraint generation rule for a rule from Figure 3 and Figure 4.
The judgement for expressions, ∆, ϕ ` e : αr ; C, isread “given environment ∆, e is inferred to have the typeαr and the pre-capability ϕ, with the set of constraints C.”
The judgement for statements is of the form ∆, ϕ1 , r ` s :ϕ2 ; C, and is read “under given environment ∆, s is inferred to have the pre-capability ϕ1 , the post-capability ϕ2 ,and the context security level r, with the set of constraints
C.” For simplicity, we assume that let-bound variables are
distinct. We initialize ∆ to map each variable and location
to a fresh type variable qualified by a fresh security levelvariable (i.e., αr ’s where each α and r are distinct). Then,we visit each expression in a bottom up manner to build
the set of constraints, applying a syntax-directed constraint
generation rule at each AST node.
Analyzing a program s, we get ∆, ϕs , r ` s : ϕ0s ; C. We
use the generated constraints C and the pre-capability of thewhole program, ϕs , in the rest of the algorithm.

We add to C the following constraints to enforce the conditions (1), (2), and (3) from Definition 3.1.
• For each ` free in the program s, the constraint ∆(`) =ref(%, intr1 )r2 where %, r1 , r2 are fresh.
• For each ` ∈ H, the constraint ∆(`) = ref(%, inth )rwhere %, r are fresh.
• Let % be a fresh abstract location variable, then, foreach ` ∈ L, the constraint ∆(`) = ref(%, intl )r wherer is fresh.
The resulting set of constraints contains six kinds of constraints:(a) Type unification constraints: σ1 = σ2 .
(b) Abstract resource constraints: %1 = %2 and ζ1 = ζ2(c) Security level constraints: o1 v o2(d) Capability inequality constraints: φ1 ≥ φ2 .
(e) Channel access constraints: 0 < ϕ1 ⇒ ϕ2 (ζ) ≥ 1.
(f) Location access constraints: r = l ⇒ ϕ(%) ≥ 1 andr = l ⇒ ϕ(%) > 0.
where
σ ::= α | ref(%, αr ) | chan(%, ϕ) | int
φ ::= ϕ | φ + φ | φ − φo ::= r | l | hNote that an equality constraint o1 = o2 can be expressedby the constraints o1 v o2 and o2 v o1 , and an equality constraint φ1 = φ2 can be expressed by the constraints
φ1 ≥ φ2 and φ2 ≥ φ1 .

Input : C and ϕe computed by the first phase
Output : ZC
NonNeg := {ϕ ≥ 0 | ϕ appears in C}
CI := Capability inequality constraints in C
Consts := {1 ≥ ϕe } ∪ CI ∪ NonNeg
Z := ∅
loop :
for each ζ ∈/ Z doif ¬LPSat(Consts ∪ CC (ζ) ∪ {cz (ζ) | ζ ∈ Z})
then Z := Z ∪ {ζ}goto loop
ZC := {cz (ζ) | ζ ∈ Z}
Figure 8. The second phase of the type inference algorithm.

The first phase deals with the constraint kinds (a), (b),and (c), and leaves the rest for the other two phases. Constraints of the kind (a) can be solved by the standard unification algorithm, which may generate more constraints of
the kinds (b) and (c) (as types may contain security levels
and capability mappings). Constraints of the kind (b) can
also be resolved by the standard unification algorithm. The
unification may fail to find a solution to the constraints of
the kind (a), e.g., if the program uses an integer constantas a channel. If so, the algorithm rejects the program as
untypable at this point.
After processing all constraints of the kind (a) and (b),the algorithm tries to find the greatest solution for the constraints of the kind (c). By greatest, we mean the solutionthat assigns h to the largest set of security level variables.
The reason for wanting the greatest solution is to prevent
discharging local access constraints (f) as much as possible
to reduce capability constraints solved in the third phase.
The greatest solution can be obtained by repeatedly selecting a constraint r v l from the constraint set, and substituting l for r until there are no more constraints of that kind.
The constraints are unsatisfiable if h v l appears in the constraints as a result, in which case, the program is rejected
as untypable. Otherwise, all unassigned security level variables are set to h, and phase 1 returns the resulting constraint set C with all the security level variables, type variables, and abstract location/channel variables substituted bytheir computed assignments.

5.2

Phase 2The second phase takes care of the channel access constraints, i.e., the constraints of the kind (e) and (d) (constraints (d) are also used in phase 3). We informally describe the process. Note that each channel access con-straint, that is, 0 < ϕ1 ⇒ ϕ2 (ζ) ≥ 1, can be restatedas ϕ2 (ζ) < 1 ⇒ 0 ≥ ϕ1 . For each ζ (that is, its equivalence class obtained by the unification in phase 1), we look
for a capabilities assignment that minimizes discharging of
the right hand side of ϕ2 (ζ) < 1 ⇒ 0 ≥ ϕ1 . Notethat the constraint resolution in phase 1 guarantees that if
ϕ2 (ζ) < 1 ⇒ 0 ≥ ϕ1 and ϕ02 (ζ) < 1 ⇒ 0 ≥ ϕ01 are inC, then ϕ1 = ϕ01 (more precisely, it is implied by the channel inequality constraints of the kind (d)) because ϕ1 , ϕ01
are both denote the capabilities passed when communicating over a channel in ζ. Thus, it suffices to add a single
constraint 0 ≥ ϕ1 to discharge all constraints for ζ if theirleft hand sides (in the original form) are found to be unsatisfiable.
We now describe the process more formally. For each ζ,
let CC(ζ) be the right hand side of set of all channel accessconstraints for ζ, and cz(ζ) is negation of one of the left
hand sides. More precisely, CC(ζ) and cz(ζ) are defined
as follows.
CC(ζ) = {ϕ2 ≥ 1 | (0 < ϕ1 ⇒ ϕ2 (ζ) ≥ 1) ∈ C}
cz(ζ) = 0 ≥ ϕ2 such that (0 < ϕ1 ⇒ ϕ2 (ζ) ≥ 1) ∈ C
The algorithm maintains the set Z of ζ’s that are found tohave unsatisfiable CC(ζ), and tries to minimize Z. We startwith Z = ∅, and iterate over each ζ and try to satisfy CC(ζ)
along with the capability inequality constraints and the constraints {cz(ζ) | ζ ∈ Z}. If unsatisfied, we add ζ to Z, andrepeat the process all over. Eventually, the algorithm comesto a fixed point where no more elements are added to Z.
Figure 8 shows the pseudo-code implementing phase 2.
The algorithm takes the set of constraints C computed byphase 1 as the input. The algorithm instantiates each capability variable as a fresh linear programming variable so thatthe procedure LPSat checks whether the given set of rational linear inequality constraints is satisfiable. Such a procedure can be implemented by well-known linear programming algorithms such as the simplex algorithm and interior
points methods. Recall that ϕe is the pre-capability of thewhole program. The constraint 1 ≥ ϕe enforces the condition (3) from Definition 3.1. The constraints NonNeg enforces the non-negativity of capabilities. The algorithm returns ZC which contains the capability variables that must
be set to 0 .

5.3

Phase 3

The third phase completes the type inference by taking
care of the location access constraints (i.e., the constraintsof the kind (f)). Like phase 2, we use linear programming tofind satisfying assignments for the location access capabilities. For each %, let LC(%) be the set of constraints consisting of the right hand sides of the discharged location accessconstraints for %. More precisely, LC(%) can be defined asfollows.
LC(%)= {ϕ ≥ 1 | (l = l ⇒ ϕ(%) ≥ 1) ∈ C}∪{ϕ > 0 | (l = l ⇒ ϕ(%) > 0) ∈ C}

where C is the constraints computed by phase 1. Note thatphase 1 has computed assignments for all the security levelvariables and so we know which location access constraints
to discharge at this point. As in phase 2, let
NonNeg := {ϕ ≥ 0 | ϕ appears in C}
CI = Capability inequality constraints in C
Then, we check whether LPSat(LC(%) ∪ NonNeg ∪ ZC ∪CI ∪ {1 ≥ ϕe }) where ZC was computed by phase 2. If
the constraints are satisfiable for all %, then the program isfound to be typable. Otherwise, the program is rejected as
untypable.
Handling Strict Inequalities Note that the constraint
ϕ > 0 is strict, which is often not (directly) supported bylinear programming algorithms. To this end, we add a fresh
linear programming variable  and replace each ϕ > 0 withϕ ≥ , and set the objective function to be . We ask thelinear programming algorithm to find a solution that maximizes . If the solver returns a solution such that  > 0,then we have found a satisfying assignment. Otherwise, theconstraint set is rejected as unsatisfiable.

5.4

Computational Complexity

We discuss the computational complexity of the type
inference algorithm. The size of linear programming instances solved in phase 2 and phase 3 is linear in the size ofthe capability constraints generated by phase 1. The number of linear programming instances solved in phase 2 is at
most quadratic to the number of distinct equivalence classes
ζ from phase 1, and the number of linear programming instances solved in phase 3 is at equal to the number of distinct
equivalence classes % from phase 1. The linear programming instances from phase 1 and phase 2 can be solved inpolynomial time by linear programming algorithms such as
interior points methods. Hence, both phase 1 and phase 2
can be solved in time polynomial in the size of the constraints generated by phase 1.
Finally, phase 1 can resolve the type and security levels
constraints in time polynomial in the size of the program,and therefore, the size of the constraints passed to phase
2 and 3 is at most polynomial in the size of the program.
Hence, the total running time is polynomial in the size ofthe program.

6

Related Work

Most type systems (e.g., [5, 9, 7]) for non-interference in
concurrent programs are designed to check a security notion

weaker than or incomparable to observational determinism,
such as possibilistic security. As such, they are unsuitablefor enforcing observational determinism.
Zdancewic and Myers [14] propose to verify observational determinism by applying security flow analysis anddeterminism checking (in fact, confluence) separately. In
contrast, our type system utilizes information obtained fromthe security flow analysis to check determinism only forthe parts of the program that are inferred to require determinism. Among other things, this scheme allows thetype system to verify some non-confluent observationallydeterministic programs.
Huisman et al. [6] propose to check observational determinism via self composition [4, 1]. Because they use
a different definition of observational determinism (see Appendix A), their self composition does not reduce to a safety
problem. It is easy to reduce observational determinism defined in this paper to a safety problem via self composition.
Combining security type systems with self composition has
been investigated for sequential programs [12, 8]. We leave
for future work to investigate if they can be combined forchecking observational determinism.
The use of fractional capabilities for checking determinism is inspired by Terauchi and Aiken’s type system forchecking determinism of concurrent programs [13], which
was in turn inspired by static capability systems for reasoning about program resources [2, 3]. However, their typesystem enforces confluence and demands determinism overthe entire program, whereas the type system in this paper
only checks determinism for some parts of the program.

7

Conclusions

We have presented a type system for verifying observational determinism. The type system enforces observational determinism by itself, and does not require the typechecked program to be confluent. The type system combines a flow-based analysis for non-interference with a fractional capability-based determinism checker so that only theparts that are inferred to be relevant for security are checkedfor determinism. We have also presented a polynomial time
type inference algorithm that utilizes linear programming.

References[1] G. Barthe, P. D’Argenio, and T. Rezk. Secure information flow by self-composition. In 17th IEEE
Computer Security Foundations Workshop, (CSFW-17
2004), pages 100–114, Pacific Grove, CA, June 2004.
IEEE Computer Society.

[2] J. Boyland. Checking interference with fractional permissions. In Static Analysis, Tenth International Symposium, pages 55–72, San Diego, CA, June 2003.
[3] K. Crary, D. Walker, and G. Morrisett. Typed memory
management in a calculus of capabilities. In Proceedings of the 26th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,
pages 262–275, San Antonio, Texas, Jan. 1999.
[4] A. Darvas, R. Hähnle, and D. Sands. A theorem proving approach to analysis of secure information flow. In
R. Gorrieri, editor, Workshop on Issues in the Theoryof Security, WITS. IFIP WG 1.7, ACM SIGPLAN and
GI FoMSESS, 2003.
[5] K. Honda and N. Yoshida. A uniform type structure
for secure information flow. In Proceedings of the 29th
Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 81–92, Portland, Oregon, Jan. 2002.
[6] M. Huisman, P. Worah, and K. Sunesen. A temporal logic characterisation of observational determinism. In 19th IEEE Computer Security Foundations
Workshop, (CSFW-19 2006), pages 3–, Venice, Italy,
July 2006. IEEE Computer Society.
[7] N. Kobayashi. Type-based information flow analysis
for the pi-calculus. Acta Informatica, 42(4-5):291–
347, 2005.
[8] D. A. Naumann. From coupling relations to matedinvariants for checking information flow. In Computer Security - ESORICS 2006, 11th European Symposium on Research in Computer Security, Proceedings, pages 279–296, Hamburg, Germany, Sept. 2006.
[9] F. Pottier. A simple view of type-secure information
flow in the pi-calculus. In 15th IEEE Computer Security Foundations Workshop (CSFW-15 2002, pages
320–330.
[10] A. W. Roscoe. CSP and determinism in security modelling. In SP’95: Proceedings of the 1995 IEEE
Symposium on Security and Privacy, pages 114–127,
Washington, DC, 1995. IEEE Computer Society.
[11] A. Sabelfeld and A. C. Myers. Language-based
information-flow security. IEEE J. Selected Areas inCommunications, 21(1):5–19, Jan. 2003.
[12] T. Terauchi and A. Aiken. Secure information flow
as a safety problem. In Static Analysis, Eleventh International Symposium, pages 352–367, Verona, Italy,
August 2004.

[13] T. Terauchi and A. Aiken. A capability calculus
for concurrency and determinism. In Concurrency
Theory, 17th International Conference, volume 4137,
pages 218–232, Bonn, Germany, Aug. 2006.
[14] S. Zdancewic and A. C. Myers. Observational determinism for concurrent program security. In 16th IEEE
Computer Security Foundations Workshop (CSFW-16
2003), pages 29–, Pacific Grove, CA, June 2003. IEEE
Computer Society.

A

Definitions of Observational Determinism

The definition of observational determinism in this paper differs from the ones given previously in the literature [14, 6]. Zdancewic and Myers’ original definition canbe obtained by weakening ours such that the traces only
need to agree on updates to individual locations in L instead of L as a whole. More precisely, their notion can bestated as follows. (Only the last sentence differs from Definition 2.1.)
Definition A.1 (Observational Determinism [14]) Let s
be a program with no free variables and K be the set of freelocations of s. Let L ⊆ K be low security locations andH ⊆ K be high security locations. Let H̄ = K \ H. We
say that s is observationally deterministic w.r.t. (L, H) if for
any T, T 0 such that s ⇓ T , s ⇓ T 0 , and T (1)|H̄ = T 0 (1)|H̄ ,we have T |{`} ≺ T 0 |{`} or T 0 |{`} ≺ T |{`} for all ` ∈ L.
Huisman et al. [6] noted an issue with this definition,
citing the following program as an example that leaks information while being observationally deterministic.
`l1 := 0; `l2 := 0;
while !`h > 0 do (`l1 := !`l1 + 1; `h := `h − 1);`l2 := 1
Here, `h is a high security location, and `l1 , `l2 are low security locations. The program satisfies Definition A.1 as asequence of updates to `l1 is always a prefix of 0, 1, 2, . . . ,and a sequence of updates to `l2 is always a prefix of 0, 1.
But the attacker can learn about the content of `h by checking the value written to `l1 just before 1 is written to `l2
Our definition of observational determinism is strong
enough to reject this program. For instance, with the initial content of `h set to 1, the sequence of updates to thelow security locations is`l1 ← 0, `l2 ← 0, `l1 ← 1, `l2 ← 1
but with the initial content of `h set to 2, the sequence of
updates to the low security locations is`l1 ← 0, `l2 ← 0, `l1 ← 1, `l1 ← 2, `l2 ← 1

Huisman et al. [6] proposed yet another definition ofobservational determinism as a remedy for the above issue. Essentially their definition still enforces observational
determinism only per location basis, but requires that thetraces to eventually be able to perform all the updates toa low security location made by the other traces. To formally state their definition, we need to introduce infinite
traces. For a state t, we write t ⇓∞ U where U is a infinite sequence of states such that either U (1) = t andU (i) → U (i + 1) for all i ≥ 1, or there exists n ≥ 1 whereU (1) = t, U (i) → U (i + 1) for all 1 ≤ i < n, there exists
no state t0 such that U (n) → t0 , and U (i) = U (i + 1) for alli ≥ n. We write s ⇓∞ U if (S, ∅, s) ⇓∞ U where dom(S)is the set of free locations in e. We extend restriction operation (|K ) and stutter equivalence (∼) to infinite strings in astraightforward way. Then, their definition of observational
determinism can be stated as follows.
Definition A.2 (Observational Determinism [6]) Let s bea program with no free variables and K be the set of freelocations of s. Let L ⊆ K be low security locations andH ⊆ K be high security locations. Let H̄ = K \ H. We
say that s is observationally deterministic w.r.t. (L, H) if
for any U, U 0 such that s ⇓∞ U , s ⇓∞ U 0 , and U (1)|H̄ =U 0 (1)|H̄ , we have U |{`} ∼ U 0 |{`} for all ` ∈ L.
There are two issues with this definition. One is that it
still allows information leak as seen in the program below.
if !`h then `l1 := 1; `l2 := 1 else `l2 := 1; `l1 := 1
Here, `h is a high security location and `l1 , `l2 are low security locations. The program is observationally deterministic according to their definition (and not according to ours).
But, the attacker can learn information about the content of`h by observing if `l1 is updated before `l2 .
The second issue is that checking observational determinism according to their definition requires the static analysis to be able to answer a liveness2 question of the form
“eventually, the traces agree on each other, forever.” For
this reason, the self composition reduction in their paper [6]is not a safety problem. It also seems difficult to enforce
such a requirement via type-based methods without being
overly conservative.

B

Proof of Soundness

We give a rough outline of the proof. The idea is to define an instrumented semantics that records updates to thelow security locations. Then, confluence with this semantics implies determinism restricted to updates to the low security locations. Unfortunately, our type system does not
2 Definitionally, it is not a liveness property as it is not a property abouta single trace.

guarantee confluence, and we also have to take in accountof high security locations. To this end, we define an erasure operation that erases all portions of the program thatare typable in a high security program context or has a highsecurity level type. In addition to recording updates for each
abstract location, we let the reduction rules for erased states
ignore updates to h-level locations and the number of pending signals for non-capability passing channels. It is shownthat the erased semantics is confluent, and simulates the low
security updates of the original. Then, observational determinism follows from these facts.
The individual techniques used in the proof are notnew. Erasure technique is often used to prove correctnessof non-interference type systems (e.g., [7]), and fractional
capabilities-based confluence argument is from [13]. Therefore, we only detail the part of the proof that shows how theexisting techniques are integrated.
First, we define the notion of a well-typed state. We extend the type rule to type run-time states by extending Γ tomap constant channels to types and introducing the following rule.
Γ, Ψ ` c : Γ(c)Let cap(chan(γ, Ψ)) = Ψ. We write Γ ` S if for each` ∈ dom(S), Γ, 0 , l ` S(`) : τ, 0 where Γ(`) = ref(κ, τ )for some κ. Recall that a program state p is a parallel composition of finitely many threads, that is, it is of the form
s1 ||s2 || . . . ||sn .
Definition B.1 (Well-typed State) Supposep = s1 || . . . ||sn
We write Γ ` (S, B, p) if there exist Ψ1 , . . . , Ψn such that
(1) For all ` ∈ H, Γ(`) = ref(κ, inth )q for some κ, q.
(2) There exists κ such that for all ` ∈ L, Γ(`) =ref(κ, intl )q for some q.
(3) For each si , Γ, Ψi , q ` si : Ψ0 for some Ψ, q, Ψ0 .
(4) Γ ` S.
(5) LetΨ=X

B(c) × cap(Γ(c)) +c∈dom(B)

n
X

Ψi

i=1

Then ∀ρ.1 ≥ Ψ(ρ).
In (5), a × Ψ = λρ.a × Ψ(ρ).
Lemma B.2 Initial states of a well-typed program are welltyped.

B.1

Marking• p2 is p1 with the statements marked h replaced byskip and expression marked h replaced by >.

To prepare the source program for erasure, we define amarking of the program which marks program parts to beerased. Given a typable program , we mark each statement with its context security level and each expression
with the security level of its type. We write mark(s) todenote the mark of s and mark(e) to denote the mark ofe. That is, if Γ, Ψ ` e : τ is a subderivation for the program, then mark(e) = qual(τ ), and if Γ, Ψ1 , q ` s : Ψ2 is
a subderivation of the type derivation for the program, thenmark(s) = q. Note that the type rules guarantee that if asubexpression is marked h, then the expression is markedh, and if a statement is marked h, then its substatements aremarked h.
To preserve marks across reductions, we introduce thefollowing derived type rule.
Γ, Ψ1 , h ` s : Ψ2
Γ, Ψ1 , l ` s : Ψ2
Above, we let mark(s) = h. Note that adding the rule does
not change the power of the type system as the rule can bederived as a lemma. With the additional rule, the following
holds.
Lemma B.3 (Preservation) Suppose Γ1 ` (S1 , B1 , p1 )and (S1 , B1 , p1 ) → (S2 , B2 , p2 ). Then there exists Γ2 ⊇
Γ1 such that Γ2 ` (S2 , B2 , p2 ), preserving the marks. Also,Γ2 ) Γ1 only if allocating a new location or a channel.
Proof: By case analysis on the reduction kind. The derived
rule is used to prove the cases for if and while. 2
Justified by the above lemma, in the remainder of theproof, we usually carry typing along the reductions, e.g.,Γ1 ` (S1 , B1 , p1 ) → Γ2 ` (S2 , B2 , p2 ), and assume thatthe statements are marked according to the typing.

B.2

Erasureq

Let loclev(ref(κ, τ ) ) = qual(τ ). We extend values forerasure states with a special value > such that v  v 0 iffv = v 0 or v 0 = >. Given Γ ` (S, B, p), we define erasure
as follows. We type > byΓ, Ψ ` > : τ
Definition B.4 (Erasure) Γ0 ` (S 0 , B 0 , p0 ) is an erasure ofΓ ` (S, B, p), writtenΓ ` (S, B, p)  Γ0 ` (S 0 , B 0 , p0 )if the following holds.
• Γ0 ` (S 0 , B 0 , p0 )• dom(S) ⊇ dom(S 0 ) ⊇ L.
• For all ` ∈ dom(S 0 ), S(`)  S 0 (`).
• For all ` ∈ dom(S 0 ) such that loclev(Γ0 (`)) = l,
S 0 (`) 6= >.
• dom(B) ⊇ dom(B 0 )• For all c ∈ dom(B 0 ), B(c)  B 0 (c).
• For all c ∈ dom(B 0 ) such that cap(Γ0 (c)) 6= ∅,B 0 (c) 6= >.
Note that > may appear as a counter in the buffer. Essentially, an erasure state agrees on l-marked parts of the program, l-level locations with the original, and the buffers forchannels with non-0 capability.
We also define the semantics for erasure states to beequivalent to the original except that writes to a h-level location writes >, and receives from a 0 -channel never blocks,
and branch on > is arbitrary (it does not matter as bothbranch bodies are guaranteed to be skip). A write to >is a no-op. More formally, we use the following modified
rules.
(S, e1 ) ; ` loclev(Γ(`)) = hΓ ` (S, B, E[e1 := e2 ])→ Γ ` (S, B, S[` 7→ >], E[skip])(S, e) ; c cap(Γ(c)) = 0
Γ ` (S, B, E[wait c])→ Γ ` (S, B[c 7→ >], E[skip])Γ ` (S, B, E[if > then skip else skip])→ Γ ` (S1 , B1 , E[skip])Γ ` (S, B, E[> := e2 ])→ Γ ` (S, B, S, E[skip])Γ ` on the reduced state is justified by preservation lemma
essentially equivalent to Lemma B.3.
Note that all expressions whose type is h are erased.
Then, the following follows from the type rule READ.
Lemma B.5 Erasure semantics never reads a h-level location (which includes high security locations H).
We can construct an erasure from the initial state.
Lemma B.6 Let Γ ` (S, ∅, s) be an initial state of the program. Then there exists an erasure Γ0 ` (S 0 , ∅, s0 ) of thatstate. In particular, it suffices to let Γ0 = Γ and S 0 = S.

B.3

Simulation

Erasure semantics simulates the original up to l-level locations. More formally,
Lemma B.7 SupposeΓ1 ` (S1 , B1 , p1 )  Γ01 ` (S10 , B10 , p01 )Γ1 ` (S1 , B1 , p) → Γ2 ` (S2 , B2 , p2 )Then, either•

Γ2 ` (S2 , B2 , p2 )  Γ01 ` (S10 , B10 , p01 ), or• There exists Γ02 ` (S20 , B20 , p02 ) such that
Γ01 ` (S10 , B10 , p01 ) → Γ02 ` (S20 , B20 , p02 )Γ2 ` (S2 , B2 , p2 )  Γ02 ` (S20 , B20 , p02 )Proof: By case analysis on the reduction kind. The key observation is that non-erased parts of the program are equivalent in the both sides of . 2
From Definition B.4 and the lemma above, it is immediate that the erasure semantics simulates the updates to llevel locations by the original. More formally,
Lemma B.8 Suppose Γ ` (S, B, p)  Γ0 ` (S 0 , B 0 , p0 ).
Let K = {` ∈ dom(S 0 ) | loclev(Γ0 (`)) = l}. Then, Γ `(S, B, p) ⇓ T implies that there exists T 0 such that Γ0 `(S 0 , B 0 , p0 ) ⇓ T 0 and T |K ∼ T 0 |K . In particular, T |L ∼T 0 |L

B.4

Instrumented Semantics

We now instrument the semantics for erased states sothat updates to locations are recorded per abstract location basis. Let absloc(ref(κ, τ )q ) = κ. A state is nowΓ ` (S, B, p); R where R is a mapping from abstract locations such that R(κ) contains list of updates for `’s suchthat absloc(Γ(`)) = κ. We extend the transition rules in astraightforward manner to record the updates.

B.5

Determinism

Let the states to be equivalent up to process reorderingand renaming of locations, channels, and variables. The
erased states (with the instrumentation) are confluent.
Lemma B.9 Suppose Γ ` (S, B, p); R is a erased state.
Then for all t1 , t2 such that Γ ` (S, B, p); R →∗ t1 andΓ ` (S, B, p); R →∗ t2 , there exists a state t3 such thatt1 →∗ t3 and t2 →∗ t3 .

The proof is much like the confluence theorem from [13].
The key observation is that capabilities guarantee that there
can be at most one thread that can write to an l-level location, and that there can be at most one thread that canbe blocked on a channel (recall that 0 channels are nonblocking in the erasure semantics). Thus any possible combination of reductions at a state commutes.
Because all the updates are recorded, the above lemma
implies that updates to locations are deterministic as records
cannot be “undone.”
Lemma B.10 Suppose Γ ` (S, B, p) is an erased state. Let
K(κ) = {` | absloc(Γ(`)) = κ}. Then Γ ` (S, B, p) ⇓ T
and Γ ` (S, B, p) ⇓ T 0 imply T |K (κ) ∼ T 0 |K (κ). In
particular, T |L ∼ T 0 |L
The formal proof is much like that for confluence implying
per-thread determinism from [13].
Finally, the soundness theorem follows from Lemmas B.2, B.5, B.6 B.8, and B.10, that is, it follows fromthe fact that updates to low security locations L in the original semantics are simulated (i.e., over-approximated) by theerasure semantics (B.6,B.8), and that the erasure semantics
is observationally deterministic (Lemmas B.5,B.10).