Secure Information Flow and CPS

Steve Zdancewic Andrew C. Myers

Cornell University, Ithaca NY 14853, USA

                      {zdance,andru}@cs.cornell.edu

Abstract. Security-typed languages enforce confidentiality or integrity policies by type checking. This paper investigates continuation-passing style (CPS) translation of such languages as a first step toward understanding their compilation. We present a low-level, secure calculus sufficient for compiling a rich source language. This language makes novel use of ordered linear continuations, which allows the first non-interference proof for language with this expressive power.

1 Introduction

Language based mechanisms for enforcing secrecy or integrity policies are attractive because, unlike ordinary access control, static information flow can enforce end-to-end policies. These policies require that data be protected despite being manipulated by programs that have access to various covert channels. For example, such a policy might prohibit a personal finance program from transmitting private account information over the Internet even though the program has Internet access to download stock market reports. To prevent the finance program from illicitly sending the private information (perhaps cleverly encoded), the compiler checks the policy allows the information flows in the program. There has been much recent work on formulating Denning’s original lattice model of information-flow control [9] in terms of type systems for static program verification [24, 31, 21, 16, 29, 20, 1, 25, 26].

Previous work has considered source-language specifications of information flow, usually accompanied by a non-interference [14] proof to demonstrate its security properties. A source-level specification of non-interference is not enough: Compiler transformations (or bugs!) may introduce new security holes. One appealing option is to verify the output of the compiler, for instance via typed assembly language [18] or proof-carrying code [22].

Programs written in continuation-passing style (CPS) are useful for representing low-level code [4, 18]. This paper takes a step toward understanding the compilation of security-typed languages by examining the interaction between CPS transformation [8, 12, 27] and information flow. We observe that a naive approach to providing security types for a continuation-passing, imperative target language yields a system that is too conservative: secure programs (in the noninterference sense) are rejected. To rectify this problem, we introduce ordered linear continuations, which allow information flow control in the CPS target language to be made as precise as in the source language.

To justify the security of our CPS language, we prove a non-interference result. To our knowledge, the proof presented here is the first for a higher-order, imperative language. The ordering property of linear continuations is crucial to the argument, which generalizes previous work by Smith and Volpano [29].

As with previous non-interference results for call-by-value languages [16, 20], the theorem holds only for programs that halt regardless of high-security data. Consequently, information about high-security values can affect termination, but because observing termination behavior leaks at most one bit on average, we consider this leakage acceptable. There are also other channels that are not captured by this notion of non-interference: high-security data can alter the amount of time it takes for the program to complete or alter the amount of memory consumed. Non-interference holds despite these apparent security leaks because the language itself provides no means for observing these resources (for instance, access to the system clock, or the ability to detect available memory). Recent work attempts to address such covert channels [3].

The next section shows why a naive type system for secure information flow is excessively restrictive for CPS and motivates the introduction of ordered linear continuations. Section 3 presents the target language, its operational semantics, and the novel features of its type system. The non-interference theorem is proved in Section 4, and Section 5 demonstrates the viability of this language as a lowlevel calculus by showing how to translate a higher-order, imperative language to CPS. We conclude with some discussion and related work in Section 6.

2 CPS and Security

Type systems for secrecy or integrity are concerned with tracking dependencies in a program [1]. One difficulty is implicit flows, which arise from the control flow of the program. Consider the code fragment A in Figure 1. There is an implicit flow between the value stored in x and the value stored in y, because examining the contents of y after the program has run gives information about the value in x. There is no information flow between x and z, however. This code is secure even when x and y are high-security variables and z is low-security. (In this paper, high security means “high secrecy” or “low integrity.” Dually, low security means “low secrecy” or “high integrity.”)

Fragment B illustrates the problem with CPS translation. It shows the code from A after control transfer has been made explicit. The variable k is bound to the continuation of the if, and the jump is indicated by the application k ⟨⟩. Because the invocation of k has been lifted into the branches of the conditional, a naive type system for information flow will conservatively require that the body of k not write to low-security memory locations, because the value of x would apparently be observable by low-security code. Program B is rejected because k writes to a low-security variable, z.

However, this code is secure: There is no information flow between x and z in B because the continuation k is invoked in both branches. As example C shows, if k is not used in one of the branches, then information about x can be learned by

(A)   if x then { y := 1; } else { y := 2; }
      z := 3; halt;
(B)   let k = (λ⟨⟩. z := 3; halt) in
      if x then { y := 1; k ⟨⟩; } else { y := 2; k ⟨⟩; }
(C)   let k = (λ⟨⟩. z := 3; halt) in
      if x then { y := 1; k ⟨⟩; } else { y:= 2; halt; }
(D)   letlin k = (λ⟨⟩. z := 3; halt) in
      if x then { y := 1; k ⟨⟩; } else { y:= 2; k ⟨⟩; }
(E)   letlin k0 = (λ⟨⟩. halt) in
      letlin k1 = (λk. z := 1; k ⟨⟩) in
      letlin k2 = (λk. z := 2; k ⟨⟩) in
      if x then { letlin k = (λ⟨⟩. k1 k0) in k2 k }
           else { letlin k = (λ⟨⟩. k2 k0) in k1 k }

Fig. 1. Examples of Information Flow in CPS

observing z. Linear type systems [13, 32, 33, 2] can express exactly the constraint that k is used in both branches. By making k’s linearity explicit, the type system can use the additional information to recover the precision of the source program analysis. Fragment D illustrates our simple approach: In addition to a normal let construct, we include letlin for introducing linear continuations. The program D certifies as secure even when z is a low-security variable, whereas C does not.

Although linearity allows for more precise reasoning about information flow, linearity alone is unsafe in the presence of first-class linear continuations. In example E, continuations k0, k1, and k2 are all linear, but there is an implicit flow from x to z because z lets us observe the order in which k1 and k2 are invoked. It is thus necessary to regulate the ordering of linear continuations.

It is simpler to make information flow analysis precise for the source language because the structure of the language limits control flow. For example, it is known that both branches of a conditional return to a common merge point. This knowledge can be exploited to obtain less conservative analysis of implicit flows. The standard CPS transformation loses this information by unifying all forms of control to a single mechanism. In our approach, the target language still has a single underlying control transfer mechanism (examples B and D execute exactly the same code), but information flow can be analyzed with the same precision as in the source.

3 The Target Calculus

The target is a call-by-value, imperative language similar to those found in the work on Typed Assembly Language [18, 6], although its type system is inspired by previous language-based security research [31, 16, 20]. This section describes the secure CPS language, its operational behavior, and its static semantics.

Types  Contexts
ℓ, pc ∈ L  Γ ::= • | Γ, x:σ
τ ::= int | 1 | σ ref | [pc](σ, κ) → 0  K ::= • | K, y:κ
σ ::= τ_{ℓ}
κ ::= 1 | ⟨pc⟩(σ, κ) → 0  Expressions
e ::= let x = prim in e
Values and Primitive Operations  | let x = ref_{ℓ}^{σ} v in e
bv ::= n | ⟨⟩ | L^{σ} | λ[pc]f(x:σ, y:κ). e  | set v := v in e
v ::= x | bv_{ℓ}  | letlin y = lv in e
lv ::= ⟨⟩ | λ⟨pc⟩(x:σ, y:κ). e  | let ⟨⟩ = lv in e
prim ::= v | v ⊕ v | deref(v)  | if0 v then e else e

| goto v v lv | lgoto lv v lv

                                                    | halt^{σ} v

Fig. 2. Syntax for the Secure CPS Language

3.1 Syntax The syntax for the secure CPS language is given in Figure 2. Elements of the lattice of security labels, L, are ranged over by meta-variables ℓ and pc. We reserve the meta-variable pc to suggest that the security label corresponds to information learned by observing the program counter. The ⊑ operator denotes the lattice ordering, with the join operation given by ⊔.

Types fall into two syntactic classes: security types, σ, and linear types, κ. Security types are the types of ordinary values and consist of a base-type component, τ, annotated with a security label, ℓ. Base types consist of integers, unit, references, and continuations (written [pc](σ, κ) → 0). Correspondingly, base values, bv, include integers, n, a unit, ⟨⟩, type annotated memory locations, L^{σ}, and continuations, λ[pc]f(x: σ, y: κ). e. All computation occurs over secure values, v, which are base values annotated with a security label. Variables, x, range over values. We adopt the notation label(τ_{ℓ}) = ℓ, and extend the join operation to security types: τ_{ℓ} ⊔ ℓ′ = τ_{(ℓ⊔ℓ′)}.

An ordinary continuation λ[pc]f(x:σ, y:κ). e is a piece of code (the expression e) which accepts a nonlinear argument of type σ and a linear argument of type κ. Continuations may recursively invoke themselves using the variable f. The notation [pc] indicates that this continuation may be called only from a context in which the program counter carries information of security at most pc. To avoid unsafe implicit flows, the body of the continuation may create effects only observable by principals able to read data with label pc.

Linear values are either unit or linear continuations, which contain code expressions parameterized by nonlinear and linear arguments just like ordinary continuations. Unlike ordinary continuations, linear continuations may not be recursive^{1}, but they may be invoked from any calling context. The syntax ⟨pc⟩

1 A linear continuation k may be discarded by a recursive ordinary continuation which loops infinitely, passing itself k. Precise terminology for our “linear” continuations would be “affine” to indicate that they may, in fact, never be invoked.

serves to distinguish linear continuations from non-linear ones. As for ordinary continuations, the label pc restricts the continuation’s effects.

The primitive operations include binary arithmetic (⊕), dereference, and a means of copying secure values. Program expressions consist of a sequence of let bindings for primitive operations, reference creation, and imperative updates (via set). The letlin construct introduces a linear continuation, and the let ⟨⟩ = lv in e expression, necessary for type-checking but operationally a noop, eliminates a linear unit before executing e. Straight-line code sequences are terminated by conditional statements, non-local transfers of control via goto (for ordinary continuations) or lgoto (for linear continuations), or the halt statement.

3.2 Operational Semantics

The operational semantics (Figure 3) are given by a transition relation between machine configurations of the form ⟨M, pc, e⟩. Memories, M, are finite partial maps from typed locations to closed values. The notation M[L^{σ} ← v] denotes the memory obtained from M by updating the location L^{σ} to contain the value v of type σ. A memory is well-formed if it is closed under the dereference operation and each value stored in the memory has the correct type. The notation e{v/x} indicates capture-avoiding substitution of value v for variable x in expression e.

The label pc in a machine configuration represents the security level of information that could be learned by observing the location of the program counter. Instructions executed with a program-counter label of pc are restricted so that they update only to memory locations with labels more secure than pc. For example, [E3 ] shows that it is valid to store a value to a memory location of type σ only if the security label of the data joined with the security labels of the program counter and the reference itself is lower than label(σ), the security clearance needed to read the data stored in the ref. Rules [E6 ] and [E7 ] show how the program-counter label changes after branching on data of security level ℓ. Observing which branch is taken reveals information about the condition variable, and so the program counter must have the higher security label pc ⊔ ℓ. The type system guarantees that all security checks in the operational semantics succeed, so no run-time representation of pc or other labels is needed.

As shown in rules [P1 ]–[P3 ], computed values are stamped with the programcounter label. Checks like the one on [E3 ] prevent illegal information flows. The two forms of let (rules [E1 ] and [E4 ]) substitute the bound value in the rest of the program.

Operationally, the rules for goto and lgoto are very similar—each causes control to be transfered to the target continuation. They differ in their treatment of the program-counter label, as seen in rules [E8 ] and [E9 ]. Ordinary continuations require that the program-counter label before the jump be bounded above by the label associated with the body of the continuation, preventing implicit flows. Linear continuations instead cause the program-counter label to be restored (potentially lowered) to that of the context in which they are declared.

[P1 ]  ⟨M, pc, bv_{ℓ}⟩ ⇓ bv_{ℓ⊔pc}
[P2 ]  ⟨M, pc, n_{ℓ} ⊕ n′_{ℓ′}⟩ ⇓ (n[[⊕]]n′)_{ℓ⊔ℓ′⊔pc}

[P3 ]

M(L^{σ}) = bv_{ℓ′}
⟨M, pc, deref(L_{ℓ}^{σ})⟩ ⇓ bv_{ℓ⊔ℓ′⊔pc}

[E1 ]

⟨M, pc, prim⟩ ⇓ v
⟨M, pc, let x = prim in e⟩ ⟼ ⟨M, pc, e{v/x}⟩

[E2 ]

ℓ ⊔ pc ⊑ label(σ) L^{σ} ∉ Dom(M)
⟨M, pc, let x = ref_{ℓ′}^{σ} bv_{ℓ} in e⟩ ⟼ ⟨M[L^{σ} ← bv_{ℓ⊔pc}], pc, e{L_{ℓ′⊔pc}^{σ}/x}⟩

[E3 ]

ℓ ⊔ ℓ′ ⊔ pc ⊑ label(σ) L^{σ} ∈ Dom(M)
⟨M, pc, set L_{ℓ}^{σ} := bv_{ℓ′} in e⟩ ⟼ ⟨M[L^{σ} ← bv_{ℓ⊔ℓ′⊔pc}], pc, e⟩
[E4 ]  ⟨M, pc, letlin y = lv in e⟩ ⟼ ⟨M, pc, e{lv/y}⟩
[E5 ]  ⟨M, pc, let ⟨⟩ = ⟨⟩ in e⟩ ⟼ ⟨M, pc, e⟩
[E6 ]  ⟨M, pc, if0 0_{ℓ} then e_{1} else e_{2}⟩ ⟼ ⟨M, pc ⊔ ℓ, e_{1}⟩
[E7 ]  ⟨M, pc, if0 n_{ℓ} then e_{1} else e_{2}⟩ ⟼ ⟨M, pc ⊔ ℓ, e_{2}⟩  (n ≠ 0)

[E8 ]

pc ⊑ pc′ v = (λ[pc′]f(x:σ, y:κ). e)_{ℓ} e′ = e{v/f}{bv_{ℓ′⊔ℓ⊔pc}/x}{lv/y}
⟨M, pc, goto (λ[pc′]f(x:σ, y:κ). e)_{ℓ} bv_{ℓ′} lv⟩ ⟼ ⟨M, pc′, e′⟩
[E9 ] ⟨M, pc, lgoto (λ⟨pc′⟩(x:σ, y:κ). e) bv_{ℓ} lv⟩ ⟼ ⟨M, pc′, e{bv_{ℓ⊔pc}/x}{lv/y}⟩

Fig. 3. Expression Evaluation

3.3 Static Semantics

The type system for the secure CPS language enforces the linearity and ordering constraints on continuations and guarantees that security labels on values are respected. Together, these restrictions rule out illegal information flows and impose enough structure on the language for us to prove a non-interference property.

As in other mixed linear–non-linear type systems [30], two separate type contexts are maintained. Γ is a finite partial map from nonlinear variables to security types, whereas K is an ordered list mapping linear variables to their types. The order in which continuations appear in K defines the order in which they are invoked; Given K = •, (y_{n}:κ_{n}), …, (y_{1} :κ_{1}), the continuation y_{1} will be executed before any of the y_{2} … y_{n}. The context Γ admits the usual weakening and exchange rules (which we omit), but K does not.

The rules for checking ordinary values, [TV1 ]–[TV6 ] shown in Figure 4, are, for the most part, standard. A value cannot contain free linear variables because discarding (or copying) it would break linearity. The lattice ordering on security

[TV1 ]  Γ ⊢ n_{ℓ} : int_{ℓ}
[TV2 ]  Γ ⊢ ⟨⟩_{ℓ} : 1_{ℓ}
[TV3 ]  Γ ⊢ L_{ℓ}^{σ} : σ ref_{ℓ}
[TV4 ]  Γ ⊢ x : σ Γ(x) = σ

[TV5 ]

f, x ∉ Dom(Γ)
σ′ = ([pc](σ, κ) → 0)_{ℓ}
Γ, f:σ′, x:σ ∥ y:κ [pc] ⊢ e
Γ ⊢ (λ[pc]f(x:σ, y:κ). e)_{ℓ} : σ′

[TV6 ]  \begin{matrix}Γ ⊢ v : σ & ⊢ σ ≤ σ′ \\ Γ ⊢ v : σ′ \end{matrix}

[TL1 ]  Γ ∥ • ⊢ ⟨⟩ : 1
[TL2 ]  Γ ∥ y:κ ⊢ y : κ

[TL3 ]

x ∉ Dom(Γ), y ∉ Dom(K)
κ′ = ⟨pc⟩(σ, κ) → 0
Γ, x:σ ∥ y:κ, K [pc] ⊢ e
Γ ∥ K ⊢ λ⟨pc⟩(x:σ, y:κ). e : κ′

[TL4 ]  \begin{matrix}Γ ∥ K ⊢ lv : κ & ⊢ κ ≤ κ′ \\ Γ ∥ K ⊢ lv : κ′ \end{matrix}

[S1 ]

pc′ ⊑ pc ⊢ σ′ ≤ σ ⊢ κ′ ≤ κ
⊢ [pc](σ, κ) → 0 ≤ [pc′](σ′, κ′) → 0 [S2 ]

\begin{matrix}⊢ τ ≤ τ′ & ℓ ⊑ ℓ′ \\ ⊢ τ_{ℓ} ≤ τ′_{ℓ′} \end{matrix}

Fig. 4. Value and Linear Value Typing

labels lifts to a subtyping relationship on values (rule [S2 ]). Continuations exhibit the expected contravariance (rule [S1 ]). We omit the obvious reflexivity and transitivity rules. Reference types are invariant, as usual.

Linear values are checked using rules [TL1 ]–[TL4 ]. It is safe for them to mention free linear variables, but these variables must not be discarded or reordered. Thus, a linear variable type-checks only when it is alone in the context (rule [TL2 ]), and unit checks only in the empty linear context (rule [TL1 ]). In a linear continuation (rule [TL3 ]), the linear argument, y, is the tail of the stack of continuations yet to be invoked. Intuitively, this judgment says that the continuation must invoke the ones in K before jumping to y. Subtyping for linear continuations is the same as for ordinary continuations.

The rules for primitive operations ([TP1 ]–[TP3 ] in Figure 5) require that the calculated value have security label at least as restrictive as the current pc, reflecting the “label stamping” behavior of the operational semantics. Values read through deref (rule [TP3 ]) pick up the label of the reference as well, which prevents illegal information flows due to aliasing.

The judgment Γ ∥ K [pc] ⊢ e (rules [TE1 ]–[TE9 ] of Figure 5) means that e is type-safe and contains no illegal information flows in the type context Γ ∥ K, when the program-counter label is at most pc. Thus, pc is a conservative approximation to the information affecting the program counter. Rule [TE4 ] illustrates how conditionals propagate this dependence: The program-counter label used to check the branches is the label before the test, pc, joined with the label on the

[TP1 ]

Γ ⊢ v : σ pc ⊑ label(σ)
Γ [pc] ⊢ v : σ [TP2 ]

Γ ⊢ v : int_{ℓ} Γ ⊢ v′ : int_{ℓ} pc ⊑ ℓ
Γ [pc] ⊢ v ⊕ v′ : int_{ℓ}

[TP3 ]

Γ ⊢ v : σ ref_{ℓ} pc ⊑ label(σ ⊔ ℓ)
Γ [pc] ⊢ deref(v) : σ ⊔ ℓ

[TE1 ]

Γ [pc] ⊢ prim : σ Γ, x:σ ∥ K [pc] ⊢ e
Γ ∥ K [pc] ⊢ let x = prim in e

[TE2 ]

Γ ⊢ v : σ pc ⊑ ℓ ⊔ label(σ) Γ, x:σ ref_{ℓ} ∥ K [pc] ⊢ e
Γ ∥ K [pc] ⊢ let x = ref_{ℓ}^{σ} v in e

[TE3 ]

Γ ⊢ v : σ ref_{ℓ} Γ ⊢ v′ : σ pc ⊔ ℓ ⊑ label(σ) Γ ∥ K [pc] ⊢ e
Γ ∥ K [pc] ⊢ set v := v′ in e

[TE4 ]

Γ ⊢ v : int_{ℓ} Γ ∥ K [pc ⊔ ℓ] ⊢ e_{i}
Γ ∥ K [pc] ⊢ if0 v then e_{1} else e_{2}

[TE5 ]

Γ ∥ K_{2} ⊢ lv : κ′ κ′ = ⟨pc⟩(σ, κ) → 0 Γ ∥ K_{1}, y:κ′ [pc] ⊢ e
Γ ∥ K_{1}, K_{2} [pc] ⊢ letlin y = lv in e

[TE6 ]

Γ ∥ K_{1} ⊢ lv : 1 Γ ∥ K_{2} [pc] ⊢ e
Γ ∥ K_{1}, K_{2} [pc] ⊢ let ⟨⟩ = lv in e

[TE7 ]

Γ ⊢ v : ([pc′](σ, κ) → 0)_{ℓ}
Γ ⊢ v′ : σ pc ⊔ ℓ ⊑ label(σ)
Γ ∥ K ⊢ lv : κ
pc ⊔ ℓ ⊑ pc′
Γ ∥ K [pc] ⊢ goto v v′ lv [TE8 ]

Γ ∥ K_{2} ⊢ lv : ⟨pc′⟩(σ, κ) → 0
Γ ⊢ v : σ
Γ ∥ K_{1} ⊢ lv′ : κ
pc ⊑ label(σ)
Γ ∥ K_{1}, K_{2} [pc] ⊢ lgoto lv v lv′

[TE9 ]

Γ ⊢ v : σ pc ⊑ label(σ)

Γ ∥ • [pc] ⊢ halt^{σ} v

Fig. 5. Primitive Operation and Expression Typing

data being tested, ℓ. The rule for goto, [TE7 ], also exhibits such a restriction because a continuation itself is labeled with a security level. The values passed to a continuation (linear or not) must also be labeled with pc because they carry information about the context in which the continuation was invoked.

The rules for letlin, [TE5 ], and lgoto, [TE8 ], manipulate the linear context to enforce the ordering property on continuations. For letlin, the linear context is split into K_{1} and K_{2}. The body e is checked under the assumption that the new continuation, y, is invoked before any continuation in K_{1}. Because y invokes the continuations in K_{2} before its linear argument (as described above for rule [TL3 ]), the ordering K_{1}, K_{2} in subsequent computation will be respected. The rule for lgoto works similarly.

Linear continuations capture the pc (or a more restrictive label) of the context in which they are introduced, as shown in rule [TE5 ]. Unlike the rule for goto, the rule for lgoto does not constrain the program-counter label of the linear continuation, reflecting that the linear continuation restores the program-counter label to the one it captured upon being introduced.

Because linear continuations capture the program counter of their introduction context, we make the mild assumption that initial programs introduce all linear continuations values (not variables) via letlin. During execution this constraint is not required, and, as we shall see, all programs in the image of our CPS translation satisfy this property.

The rule for halt, [TE9 ], requires an empty linear context, indicating that the program consumes all linear continuations before stopping. The σ annotating halt is the type of the final output of the program; its label should be constrained by the security clearance of the user of the program.

This type system is sound with respect to the operational semantics [35]. The proof is, for the most part, standard, following in the style of Wright and Felleisen [34]. We simply state the lemmas necessary for the discussion of the non-interference result of the next section.

Lemma 1 (Subject Reduction).

If • ∥ K [pc] ⊢ e and M is a well-formed memory such that Loc(e) ⊆ Dom(M) and ⟨M, pc, e⟩ ⟼ ⟨M′, pc′, e′⟩, then • ∥ K [pc′] ⊢ e′ and M′ is a well-formed memory such that Loc(e′) ⊆ Dom(M′).

Lemma 2 (Progress).

If • ∥ • [pc] ⊢ e and Mis well-formed and Loc(e) ⊆ Dom(M), then either e is of the form halt^{σ} v or there exist M′, pc′, and e′ such that ⟨M, pc, e⟩ ⟼ ⟨M′, pc′, e′⟩

Note that Subject Reduction holds for terms containing free occurrences of linear variables. This fact is important for proving that the ordering on linear continuations is respected. The Progress lemma (and hence Soundness) applies only to closed programs, as usual.

4 Non-Interference

This section proves a non-interference result for the secure CPS language, generalizing Smith and Volpano’s preservation-style argument [29]. A technical report [35] gives a more detailed account of our approach.

Informally, the non-interference result shows that low-security computations are not able to observe high-security data. Here, “low-security” refers to the set of security labels ⊑ ζ, where ζ is an arbitrary point in L, and “high-security” refers to labels ⋢ ζ. The proof shows that high-security data and computation can be arbitrarily changed without affecting the value of any computed lowsecurity result. Furthermore, memory locations visible to low-security observers (locations storing data labeled ⊑ ζ) are also unaffected by high-security values.

Non-interference reduces to showing that two programs are equivalent from the low-security perspective. Given a program e_{1} that operates on high- and low-security data, it suffices to show that e_{1} is low-equivalent to the program e_{2} that differs from e_{1} in its high-security computations.

How do we show that e_{1} and e_{2} behave the same from the low-security point of view? If pc ⊑ ζ, meaning that e_{1} and e_{2} may perform actions visible to low observers, they necessarily must perform the same computation on low-security values. Yet e_{1} and e_{2} may differ in their behavior on high-security data and still be equivalent from the low perspective. To show their equivalence, we should find substitutions γ_{1} and γ_{2} containing the relevant high-security data such that e = γ_{1}(e) and e_{2} = γ_{2}(e)—both e_{1} and e_{2} look the same after factoring out the high-security data.

On the other hand, when pc ⋢ ζ, no matter what e_{1} and e_{2} do their actions should not be visible from the low point of view; their computations are irrelevant. The operational semantics guarantee that the program-counter label is monotonically increasing except when a linear continuation is invoked. If e_{1} invokes a linear continuation causing pc to fall below ζ, e_{2} must follow suit; otherwise the low-security observer can distinguish them. The ordering on linear continuations forces e_{2} to invoke the same low-security continuation as e_{1}.

The crucial invariant maintained by well-typed programs is that it is possible to factor out (via substitutions) the relevant high-security values and those linear continuations that reset the program-counter label to be ⊑ ζ.

Definition 1 (Substitutions). For any context, Γ, we write γ ⊧ Γ to indicate that γ is a finite map from variables to closed values such that Dom(γ) = Dom(Γ) and for every x ∈ Dom(γ) it is the case that • ⊢ γ(x) : Γ(x).

For K a linear context, we write Γ ⊢ k ⊧ K to indicate that k is a finite map of variables to linear values (with free variables from Γ) with the same domain as K and such that for every y ∈ Dom(k) we have Γ ∥ • ⊢ k(y) : K(y).

Substitution application, written γ(e), indicates the capture-avoiding substitution of the value γ(x) for free occurrences of x in e, for each x in the domain of γ. We use similar notation for linear contexts, and also for substitution through primitive operations and values.

Linear continuations that set the program-counter label ⋢ ζ may appear in low-equivalent programs, because, from the low-security point of view, they are not relevant.

Definition 2 (letlin Invariant). A term satisfies the letlin invariant if every linear continuation expression λ⟨pc⟩(x:σ, y:κ). e appearing in the term is either in the binding position of a letlin or satisfies pc ⋢ ζ.

If substitution k contains only low-security linear continuations and k(e) is a closed term such that e satisfies the letlin invariant, then all the low-security continuations not letlin-bound in e must be obtained from k. This invariant ensures that k factors out all of the relevant continuations from k(e).

Extending these ideas to values, memories, and machine configurations we obtain the definitions below:

Definition 3 (ζ-Equivalence).

Γ ⊢ γ_{1} ≈_{ζ} γ_{2} If γ_{1}, γ_{2} ⊧ Γ and for every x ∈ Dom(Γ) it is the case that label(γ_{i}(x)) ⋢ ζ and γ_{i}(x) satisfies the letlin invariant.

Γ ∥ K ⊢ k_{1} ≈_{ζ} k_{2} If Γ ⊢ k_{1}, k_{2} ⊧ K and for every y ∈ Dom(K) it is the case that k_{1}(y) ≡_{α} k_{2}(y) = λ⟨pc⟩(x:σ, y′:κ). e such that pc ⊑ ζ and e satisfies the letlin invariant.

v_{1} ≈_{ζ} v_{2} : σ If there exist Γ, γ_{1}, and γ_{2} plus terms v′_{1} ≡_{α} v′_{2} such that Γ ⊢ γ_{1} ≈_{ζ} γ_{2}, and Γ ⊢ v′_{i} : σ and v_{i} = γ_{i}(v′_{i}) and each v′_{i} satisfies the letlin invariant.

M_{1} ≈_{ζ} M_{2} If for all L^{σ} ∈ Dom(M_{1}) ∪ Dom(M_{2}) if label(σ) ⊑ ζ, then L^{σ} ∈ Dom(M_{1}) ∩ Dom(M_{2}) and M_{1}(L^{σ}) ≈_{ζ} M_{2}(L^{σ}) : σ.

Definition 4 (Non-Interference Invariant). The non-interference invariant is a predicate on machine configurations, written Γ ∥ K ⊢ ⟨M_{1}, pc_{1}, e_{1}⟩ ≈_{ζ} ⟨M_{1}, pc_{2}, e_{2}⟩ that holds if the following conditions are all met:

(i) There exist substitutions γ_{1}, γ_{2}, k_{1}, k_{2} and terms e′_{1} and e′_{2} such

that e_{1} = γ_{1}(k_{1}(e′_{1})) and e_{2} = γ_{2}(k_{2}(e′_{2})).

(ii) Either (a) pc_{1} = pc_{2} ⊑ ζ and e′_{1} ≡_{α} e′_{2} or (b) Γ ∥ K [pc_{1}] ⊢ e′_{1}

and Γ ∥ K [pc_{2}] ⊢ e′_{2} and pc_{i} ⋢ ζ.
(iii) Γ ⊢ γ_{1} ≈_{ζ} γ_{2}
(iv) Γ ∥ K ⊢ k_{1} ≈_{ζ} k_{2}
(v) Loc(e_{1}) ⊆ Dom(M_{1}) and Loc(e_{2}) ⊆ Dom(M_{2}) and M_{1} ≈_{ζ} M_{2}.
(vi) Both e′_{1} and e′_{2} satisfy the letlin invariant.

Our proof is a preservation argument showing that the Non-Interference Invariant holds at each step of the computation. When the program counter is low, equivalent configurations execute in lock step (modulo the values of high-security data). After the program branches on high-security information (or jumped to a high-security continuation), the two programs may temporarily get out of sync, but during that time, they may affect only high-security data. Eventually, if the program counter drops low again (via a linear continuation), both computations return to lock-step execution.

We first show that ζ-equivalent configuration evaluate in lock-step as long as the program counter has low security.

Lemma 3 (Low-pc Step).

Suppose Γ ∥ K ⊢ ⟨M_{1}, pc_{1}, e_{1}⟩ ≈_{ζ} ⟨M_{2}, pc_{2}, e_{2}⟩, pc_{1} ⊑ ζ and pc_{2} ⊑ ζ. If ⟨M_{1}, pc_{1}, e_{1}⟩ ⟼ ⟨M′_{1}, pc′_{1}, e′_{1}⟩, then ⟨M_{2}, pc_{2}, e_{2}⟩ ⟼ ⟨M′_{2}, pc′_{2}, e′_{2}⟩ and there exist Γ′ and K′ such that Γ′ ∥ K′ ⊢ ⟨M′_{1}, pc′_{1}, e′_{1}⟩ ≈_{ζ} ⟨M′_{2}, pc′_{2}, e′_{2}⟩.

Proof. (Sketch) Let e_{1} = γ_{1}(k_{1}(e′′_{1})) and e_{2} = γ_{2}(k_{2}(e′′_{2})) where the substitutions are as described by the conditions of the Non-Interference Invariant. Because pc_{i} ⊑ ζ, clause (ii) implies that e′′_{1} and e′′_{2} must be α-equivalent expressions and pc_{1} = pc_{2} = pc. Hence the only difference in their behavior arises due to the substitutions or the different memories. We proceed by cases on the transition step taken by the first program. The main technique is to reason by cases on the security level of the value used in the step—if it’s low-security, by α-equivalence, both programs compute the same values, otherwise, we extend the substitutions γ_{1} and γ_{2} to contain the high-security data. We show the case for [E8 ] in detail to give the flavor of the argument:

In this case, each e′′_{i} = goto v v′ lv. It must be the case that γ_{1}(v) = (λ[pc′]f(x: σ, y : κ). e)_{ℓ}. If ℓ ⊑ ζ, then v = (λ[pc′]f(x: σ, y : κ). e′)_{ℓ} where e′ = γ_{1}(e) because, by invariant (iii), the continuation could not be found in γ_{1}. Note that γ_{1}(v′) ≈_{ζ} γ_{2}(v′) : σ. There are two cases, depending on whether γ_{1}(v′) has label ⊑ ζ. If so, it suffices to take Γ′ = Γ, K′ = K, and leave the substitutions unchanged, for we have e′_{i} = γ_{i}(k_{i}(e{v/f}{γ_{i}(v′) ⊔ pc ⊔ ℓ/x}{lv/y})). Otherwise, if the label of γ_{1}(v′) ⋢ ζ, we take Γ′ = Γ, x:σ and γ′_{i} = γ_{i}{x ↦ γ_{i}(v′) ⊔ pc ⊔ ℓ}. The necessary constraints are then met by e′_{i} = γ′_{i}(k_{i}(e{v/f}{lv/y})).

The other case is that ℓ ⋢ ζ, and hence the label of γ_{2}(v) is also ⋢ ζ. Thus, pc′_{1} = pc ⊔ ℓ ⋢ ζ and pc′_{2} ⋢ ζ. The resulting configurations satisfy part (b) of clause (ii). The bodies of the continuations are irrelevant, as long as the other invariants are satisfied, but this follows if we build the new value substitutions as in the previous paragraph ⊓ ⊔

Next, we prove that linear continuations do indeed get called in the order described by the linear context.

Lemma 4 (Linear Continuation Ordering).

Assume K = y_{n} : k_{n}, …, y_{1} : k_{1}, each k_{i} is a linear continuation type, and • ∥ K [pc] ⊢ e. If • ⊢ k ⊧ K, then in the evaluation starting from any wellformed configuration ⟨M, pc, k(e)⟩, the continuation k(y_{1}) will be invoked before any other k(y_{i}).

Proof. The operational semantics and Subject Reduction are valid for open terms. Progress, however, does not hold for open terms. Evaluate the open term e in the configuration ⟨M, pc, e⟩. If the computation diverges, none of the y_{i}’s ever reach an active position, and hence are not invoked. Otherwise, the computation must get stuck (it can’t halt because Subject Reduction implies that all configurations are well-typed;the halt expression requires an empty linear context). The stuck term must be of the form lgoto y_{i} v lv, and, because it is well-typed, rule [TE8 ] implies that y_{i} = y_{1}. ⊓ ⊔

We use the ordering lemma to prove that equivalent high-security configurations eventually return to equivalent low-security configurations.

Lemma 5 (High-pc Step). If Γ ∥ K ⊢ ⟨M_{1}, pc_{1}, e_{1}⟩ ≈_{ζ} ⟨M_{2}, pc_{2}, e_{2}⟩ and pc_{i} ⋢ ζ, then ⟨M_{1}, pc_{1}, e_{1}⟩ ⟼ ⟨M′_{1}, pc′_{1}, e′_{1}⟩ implies that either e_{2} diverges or ⟨M_{2}, pc_{2}, e_{2}⟩ ⟼^{∗} ⟨M′_{2}, pc′_{2}, e′_{2}⟩ and there exist Γ′ and K′ such that Γ′ ∥ K′ ⊢ ⟨M′_{1}, pc′_{1}, e′_{1}⟩ ≈_{ζ} ⟨M′_{2}, pc′_{2}, e_{2}⟩.

Proof. (Sketch) The proof is by cases on the transition step of the first configuration. Because pc_{1} ⋢ ζ and all the transition rules except [E9 ] increase the program-counter label, we may choose zero steps for the second configuration and still show that ≈_{ζ} is preserved. Condition (ii) of the invariant holds via part(b). The other invariants follow because all values computed and memory locations written to must have labels higher than pc_{1} (and hence ⋢ ζ). Thus, the only memory locations affected are high-security: M′_{1} ≈_{ζ} M_{2} = M′_{2}. Similarly, [TE5 ] forces linear continuations introduced by e_{1} to have pc ⋢ ζ. Substituting them in e_{1} maintains clause (vi) of the invariant.

Now consider the case for [E9 ]. Let e_{1} = γ_{1}(k_{1}(e′′_{1})), then e′′_{1} = lgoto lv v_{1} lv_{1} for some lv. If lv is not a variable, clause (vi) ensures that the program counter in lv’s body is ⋢ ζ. Pick 0 steps for the second configuration as above. Otherwise, if lv is a variable, y, then [TE8 ] guarantees that K = K′, y: κ. By assumption, k_{1}(y) = λ⟨pc⟩(x:σ, y′:κ′). e, where pc ⊑ ζ. Assume e_{2} does not diverge. By the ordering lemma, ⟨M_{2}, pc_{2}, e_{2}⟩ ⟼^{∗} ⟨M′_{2}, pc′_{2}, lgoto k_{2}(y) v_{2} lv_{2}⟩. Simple induction on the length of this transition sequence shows that M_{2} ≈_{ζ} M′_{2}, because the program counter may not become ⊑ ζ. Thus, M′_{1} = M_{1} ≈_{ζ} M_{2} ≈_{ζ} M′_{2}. By invariant (iv), k_{2}(y) ≡_{α} k_{1}(y). Furthermore, [TE8 ] requires that label(σ) ⋢ ζ. Let Γ′ = Γ, x: σ, γ′_{1} = γ_{1}{x ↦ γ_{1}(v_{1}) ⊔ pc_{1}}, γ′_{2} = γ_{2}{x ↦ γ_{2}(v_{2}) ⊔ pc_{2}}; take k′_{1} and k′_{2} to be the restrictions of k_{1} and k_{2} to the domain of K′, and choose e′_{1} = γ′_{1}(k′_{1}(e)) and e′_{2} = γ′_{2}(k′_{2}(e)). All of the necessary conditions are satisfied as is easily verified via the operational semantics. ⊓ ⊔

Finally, we use the above lemmas to prove non-interference. Assume a program that eventually computes a low-security value has access to high-security data. We show that arbitrarily changing the high-security data does not affect the program’s result.

First, some convenient notation for the initial continuation: Let stop(τ_{ℓ}) : κ_{stop} = λ⟨⊥⟩(x:τ_{ℓ}, y:1). let ⟨⟩ = y in halt^{τ_{ℓ}} x where κ_{stop} = [⊥](τ_{ℓ}, 1) → 0.

Theorem 1 (Non-Interference). Suppose x: σ ∥ y : κ_{stop} [⊥] ⊢ e for some initial program e. Further suppose that label(σ) ⋢ ζ and • ⊢ v_{1}, v_{2} : σ. Then

⟨∅, ⊥, e{v_{1}/x}{stop(int_{ζ})/y}⟩ ⟼^{∗} ⟨M_{1}, ζ, halt^{int^{ζ}} n_{ℓ_{1}}⟩
and
⟨∅, ⊥, e{v_{2}/x}{stop(int_{ζ})/y}⟩ ⟼^{∗} ⟨M_{2}, ζ, halt^{int^{ζ}} m_{ℓ_{2}}⟩

implies that M_{1} ≈_{ζ} M_{2} and n = m.

Proof. It is easy to verify that

x:σ ∥ y:κ_{stop} ⊢ ⟨∅, ⊥, e{v_{1}/x}{stop(int_{ζ})/y}⟩ ≈_{ζ} ⟨∅, ⊥, e{v_{2}/x}{stop(int_{ζ})/y}⟩

by letting γ_{1} = {x ↦ v_{1}}, γ_{2} = {x ↦ v_{2}}, and k_{1} = k_{2} = {y ↦ stop(int_{ζ})}. Induction on the length of the first expression’s evaluation sequence, using the Low- and High-pc Step lemmas plus the fact that the second evaluation sequence terminates implies that Γ ∥ K ⊢ ⟨M_{1}, ζ, halt^{int^{ζ}} n_{ℓ_{1}}⟩ ≈_{ζ} ⟨M_{2}, ζ, halt^{int^{ζ}} m_{ℓ_{2}}⟩. Clause (v) of the Non-interference Invariant implies that M_{1} ≈_{ζ} M_{2}. Soundness implies that ℓ_{1} ⊑ ζ and ℓ_{2} ⊑ ζ. This means, because of clause (iii), that neither n_{ℓ_{1}} nor m_{ℓ_{2}} are in the range of γ′_{i}. Thus, the integers present in the halt expressions do not arise from substitution. Because ζ ⊑ ζ, clause (ii) implies that halt^{int^{ζ}} n_{ℓ_{1}} ≡_{α} halt^{int^{ζ}} m_{ℓ_{2}}, from which we obtain n = m as desired. ⊓ ⊔

5 Translation

This section presents a CPS translation for a secure, imperative, higher-order language that includes only the features essential to demonstrating the translation. Its type system is adapted from the SLam calculus [16] to follow our “label stamping” operational semantics. The judgment Γ ⊢_{pc} e : s shows that expression e has source type s under type context Γ, assuming the program-counter label is bounded above by pc.

Source types are similar to those of the target, except that instead of continuations there are functions. Function types are labeled with their latent effect, a lower bound on the security level of memory locations that will be written to by that function. The type translation, following previous work on typed CPS conversion [15], is given in terms of three mutually recursive functions: (−)^{∗}, for base types, (−)^{+} for security types, and (−)^{−} to linear continuation types:

int^{∗} = int  (s ref)^{∗} = s^{+} ref  (s_{1} ⟶^{ℓ} s_{2})^{∗} = [ℓ](s_{1}^{+}, s_{2}^{−}) → 0
t_{ℓ}^{+} = (t^{∗})_{ℓ}  s^{−} = ⟨⊥⟩(s^{+}, 1) → 0

Figure 6 shows the term translation as a type-directed map from source typing derivations to target terms. For simplicity, we present an un-optimizing CPS translation, although we expect that first-class linear continuations will support more sophisticated translations, such as tail-call optimization [8]. To obtain the full translation of a closed term e of type s, we use the initial continuation from Section 4: letlin stop = stop(s^{+}) in [[∅ ⊢_{ℓ} e : s]]stop

The basic lemma for establishing correctness of the translation is proved by induction on the typing derivation of the source term:

Lemma 6 (Type Translation). Γ ⊢_{ℓ} e : s ⇒ Γ^{+} ∥ y:s^{−} [ℓ] ⊢ [[Γ ⊢_{ℓ} e : s]]y.

This result also shows that the CPS language is at least as precise as the source.

6 Discussion and Related Work

The constraints imposed by linearity can be seen as a form of resource management [13], in this case limiting the set of possible future computations. Linearity has been more widely used in the context of memory consumption [32, 33, 2]. Linear continuations have been studied in terms of their category theoretic semantics [11] and also as a computational interpretation of classical logic [5]

Linearity also plays a role in security types for process calculi such as the πcalculus [17]. Because the usual translation of the λ-calculus into the π-calculus

[[Γ, x:s′ ⊢_{pc} x : s′ ⊔ pc]]y ⇒ lgoto y x ⟨⟩
[ \left[{Γ, f:s, x:s_{1} ⊢_{pc}′ e : s_{2} \atop Γ ⊢_{pc} (μf(x:s_{1}). e)_{ℓ} : s ⊔ pc}\right] ]y ⇒ \{ \begin{matrix}lgoto y (λ[pc′]f(x:s_{1}^{+}, y′:s_{2}^{−}). \\ [[Γ, f:s, x:s_{1} ⊢_{pc}′ e : s_{2}]]y′)_{ℓ} ⟨⟩ \end{matrix}

[ [ Γ ⊢_{pc} e : s Γ ⊢_{pc} e′ : s_{1} ℓ ⊑ pc′ ⊓ label(s_{1}) Γ ⊢_{pc} (e e′) : s_{2} ] ]y ⇒ \{ \begin{matrix}letlin k_{1} = λ⟨pc⟩(f:s^{+}, y_{1} :1). \\ let ⟨⟩ = y_{1} in \\ letlin k_{2}=λ⟨pc⟩(x:s_{1}^{+}, y_{2} :1). \\ let ⟨⟩= y_{2} in \\ goto f x y \\ in [[Γ ⊢_{pc} e′ : s_{1}]]k_{2} \\ in [[Γ ⊢_{pc} e : s]]k_{1} \end{matrix}

[ [ Γ ⊢_{pc} e : int_{ℓ} ; Γ ⊢_{pc}′ e_{i} : s′ ; ℓ ⊑ pc′ Γ ⊢_{pc} if0 e then e_{1} else e_{2} : s′ ] ]y ⇒ \{ \begin{matrix}letlin k_{1} = λ⟨pc⟩(x:int_{ℓ}^{+}, y_{1} :1). \\ let ⟨⟩ = y_{1} in \\ if0 x then [[Γ ⊢_{pc}′ e_{1} : s′]]y \\ else [[Γ ⊢_{pc}′ e_{2} : s′]]y \\ in [[Γ ⊢_{pc} e : int_{ℓ}]]k_{1} \end{matrix}

[ [ Γ ⊢_{pc} e : s′ ref_{ℓ} Γ ⊢_{pc} e′ : s′ ℓ ⊑ label(s′) Γ ⊢_{pc} e := e′ : s′ ] ]y ⇒ \{ \begin{matrix}letlin k_{1} = λ⟨pc⟩(x_{1} :s′ ref_{ℓ}^{+}, y_{1} :1). \\ let ⟨⟩ = y_{1} in \\ letlin k_{2}=λ⟨pc⟩(x_{2} :s^{′+}, y_{2} :1). \\ let ⟨⟩ = y_{2} in \\ set x_{1} := x_{2} in \\ lgoto y x_{2} ⟨⟩ \\ in [[Γ ⊢_{pc} e′ : s′]]k_{2} \\ in [[Γ ⊢_{pc} e : s′ ref_{ℓ}]]k_{1} \end{matrix}

Fig. 6. CPS Translation (Here s = (s_{1} ⟶^{pc′} s_{2})_{ℓ}, and the k_{i}’s and y_{i}’s are fresh.)

can be seen as a form of CPS translation, it might be enlightening to investigate the connections between security in process calculi and low-level code.

The CPS translation has been studied in the context of program analysis [23, 10]. Sabry and Felleisen observed that increased precision in some CPS data flow analyses is due to duplication of analysis along different execution paths [28]. They also note that some analyses “confuse continuations” when applied to CPS programs. Our type system distinguishes linear from non-linear continuations to avoid confusing “calls” from “returns.” More recently, Damian and Danvy showed that CPS translation can improve binding-time analysis in the λ-calculus [7], suggesting that the connection between binding-time analysis and security [1] warrants more investigation.

Linear continuations appear to be a higher-order analog to post-dominators in a control-flow graph. Algorithms for determining post-dominators (see Muchnick’s text [19]) might yield inference techniques for linear continuation types. Conversely, linear continuations might yield a type-theoretic basis for correctness proofs of optimizations based on post-dominators.

Beyond CPS conversion, compilers also use closure conversion, hoisting, and various optimizations such as inlining or constant propagation. These transformations may affect information flows. How to build type systems rich enough to express security properties at this level is still an open question.

Understanding secure information flow in low-level programs is essential to providing secrecy of private data. We have shown that explicit ordering of continuations can improve the precision of security types. The extra constraints ordered linear continuations provide limit implicit flows, and make possible our non-interference proof, the first of its kind for a higher-order, imperative language.

References

1. Martín Abadi, Anindya Banerjee, Nevin Heintze, and Jon Riecke. A core calculus of dependency. In Proc. 26th ACM Symp. on Principles of Programming Languages (POPL), pages 147–160, 1999.

2. Samson Abramsky. Computational interpretations of linear logic. Theoretical Computer Science, 111:3–57, 1993.

3. Johan Agat. Transforming out timing leaks. In Proc. 27th ACM Symp. on Principles of Programming Languages (POPL), January 2000.

4. Andrew Appel. Compiling with Continuations. Cambridge University Press, 1992.

5. Gavin Bierman. A classical linear lambda calculus. Theoretical Computer Science, 227(1–2):43–78, 1999.

6. Karl Crary, David Walker, and Greg Morrisett. Typed memory management in a calculus of capabilities. In Proc. 26th ACM Symp. on Principles of Programming Languages (POPL), pages 262–275, 1999.

7. Daniel Damian and Olivier Danvy. Syntactic accidents in program analysis: On the impact of the CPS transformation. In Proc. 5th ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 209–220, 2000.

8. Olivier Danvy and Andrzej Filinski. Representing control: A study of the CPS transformation. Mathematical Structures in Computer Science, 2:361–391, 1992.

9. Dorothy E. Denning and Peter J. Denning. Certification of Programs for Secure Information Flow. Comm. of the ACM, 20(7):504–513, July 1977.

10. J. Mylaert Filho and G. Burn. Continuation passing transformations and abstract interpretation. In Proc.s First Imperial College, Department of Computing, Workshop on Theory and Formal Methods, 1993.

11. Andrzej Filinski. Linear continuations. In Proc. 19th ACM Symp. on Principles of Programming Languages (POPL), 1992.

12. Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. The essence of compiling with continuations. In Proceedings of the ACM ’93 Conference on Programming Language Design and Implementation, 1993.

13. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1–102, 1987.

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

15. Robert Harper and Mark Lillibridge. Explicit polymorphism and CPS conversion. In Proc. 20th ACM Symp. on Principles of Programming Languages (POPL), 1993.

16. Nevin Heintze and Jon G. Riecke. The SLam calculus: Programming with secrecy and integrity. In Proc. 25th ACM Symp. on Principles of Programming Languages (POPL), San Diego, California, January 1998.

17. Kohei Honda, Vasco Vasconcelos, and Nobuko Yoshida. Secure information flow as typed process behaviour. In Proc. of the 9th European Symposium on Programming, volume 1782 of Lecture Notes in Computer Science, pages 180–199. Springer, 2000.

18. Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to typed assembly language. In Proc. 25th ACM Symp. on Principles of Programming Languages (POPL), San Diego, California, January 1998.

19. Steven S. Muchnick. Advanced Compiler Design and Implementation. Morgan Kaufmann Publishers, 1997.

20. Andrew C. Myers. JFlow: Practical mostly-static information flow control. In Proc. 26th ACM Symp. on Principles of Programming Languages (POPL), San Antonio, TX, USA, January 1999.

21. Andrew C. Myers and Barbara Liskov. A decentralized model for information flow control. In Proc. 17th ACM Symp. on Operating System Principles (SOSP), pages 129–142, Saint-Malo, France, 1997.

22. George C. Necula. Proof-carrying code. In Proc. 24th ACM Symp. on Principles of Programming Languages (POPL), pages 106–119, January 1997.

23. Flemming Nielson. A denotational framework for data flow analysis. Acta Informatica, 18:265–287, 1982.

24. Jens Palsberg and Peter Ørbæk. Trust in the λ-calculus. In Proc. 2nd International Symposium on Static Analysis, number 983 in Lecture Notes in Computer Science, pages 314–329. Springer, September 1995.

25. Andrei Sabelfeld and David Sands. A PER model of secure information flow in sequential programs. In Proceedings of the European Symposium on Programming. Springer-Verlag, March 1999. LNCS volume 1576.

26. Andrei Sabelfeld and David Sands. Probabilistic noninterference for multi-threaded programs. In Proceedings of the 13th IEEE Computer Security Foundations Workshop. IEEE Computer Society Press, July 2000.

27. Amr Sabry and Matthias Felleisen. Reasoning about programs in continuationpassing style. Lisp and Symbolic Computation: An International Journal, 1993.

28. Amr Sabry and Matthias Felleisen. Is continuation-passing useful for data flow analysis? In Proc. SIGPLAN ’94 Conference on Programming Language Design and Implementation, pages 1–12, 1994.

29. Geoffrey Smith and Dennis Volpano. Secure information flow in a multi-threaded imperative language. In Proc. 25th ACM Symp. on Principles of Programming Languages (POPL), San Diego, California, January 1998.

30. David N. Turner and Philip Wadler. Operational interpretations of linear logic. Theoretical Computer Science, 2000. To Appear.

31. Dennis Volpano, Geoffrey Smith, and Cynthia Irvine. A sound type system for secure flow analysis. Journal of Computer Security, 4(3):167–187, 1996.

32. Philip Wadler. Linear types can change the world! In M. Broy and C. Jones, editors, Progarmming Concepts and Methods. North Holland, 1990.

33. Philip Wadler. A taste of linear logic. In Mathematical Foundations of Computer Science, volume 711 of Lecture Notes in Computer Science. Springer-Verlag, 1993.

34. Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38–94, 1994.

35. Steve Zdancewic and Andrew C. Myers. Confidentiality and integrity with untrusted hosts. Technical Report 2000-1810, Cornell University, 2000.