Confidentiality and Integrity with Untrusted Hosts: Technical Report

Steve Zdancewic Andrew C. Myers^{∗}

Cornell University

Abstract

Several security-typed languages have recently been proposed to enforce security properties such as confidentiality or integrity by type checking. We propose a new security-typed language, Spl@, that addresses two important limitations of previous approaches.

First, existing languages assume that the underlying execution platform is trusted; this assumption does not scale to distributed computation in which a variety of differently trusted hosts are available to execute programs. Our new approach, secure program partitioning, translates programs written assuming complete trust in a single executing host into programs that execute using a collection of variously trusted hosts to perform computation. As the trust configuration of a distributed system evolves, this translation can be performed as necessary for security.

Second, many common program transformations do not work in existing security-typed languages; although they produce equivalent programs, these programs are rejected because of apparent information flows. Spl@ uses a novel mechanism based on ordered linear continuations to permit a richer class of program transformations, including secure program partitioning.

This report is the technical companion to [ZM00]. It contains expanded discussion and extensive proofs of both the soundness and noninterference theorems mentioned in Section 3.3 of that work.

1 Introduction

Stronger protection for the confidentiality (secrecy, privacy) and integrity of data is becoming increasingly important, because programs containing untrusted code and networks containing untrusted hosts are the rule rather than the exception. An approach that has recently been under investigation is the idea of enforcing static information flow control [DD77] via type systems in which the types include a security attribute [PO95, VSI96, ML97, HR98, SV98, Mye99, ABHR99]. We call these languages security-typed languages.

Information flow control is attractive because, unlike ordinary access control, it can enforce end-to-end security policies. These policies require that data be protected even if it is used for computation by untrusted code: for example, a simple end-to-end confidentiality policy might require that a particular data item is readable only by a particular set of users—regardless of what code manipulates the data information derived from it. Thus, security is protected even when a program comprises many separately developed components.

∗E-mail: {zdance,andru}@cs.cornell.edu XX Effort sponsored by the Defense Advanced Research Projects Agency (DARPA) and Air Force Research Laboratory, Air Force Material Command, USAF, under agreement number F30602-99-1-0533. The U.S. Governement is authorized to reproduce and distribute reprints for Governement purposes notwithstanding any copyright annotation thereon. The views and conclusions contained herein are those of the authors and should not be interpreted as necessarily representing the official policies or endorsement, either expressed or implied, of the Defense Advanced Research Projects Agency (DARPA), the Air Force Research Laboratory, or the U.S. Government.

End-to-end security policies are particularly attractive given current trends in computation. Increasingly, computations are collaborations between principals with distinct security interests, and are distributed across a set of hosts. Ordinary web transactions already fit this description, but we can expect to see more complex, interesting examples with the increasing use of businessto-business transactions.

Because of the support for end-to-end security policies, static information flow control would seem to be ideal for enforcing the security of distributed computation. However, existing languages ignore an important aspect of distributed computation: the hosts on which computation is performed are not universally (or equally) trusted by the participants in the computation. These hosts may leak or damage data even though the programs that run on them are correct.

For security, any distributed computation should be partitioned so that no participant is required to place undue trust in a host. For example, data that is confidential to a particular principal should not be transferred to a host that is not trusted by that principal. This observation applies even to conventional security mechanisms, of course, where the partitioning is performed manually, and computations spanning multiple hosts are usually described as separate programs communicating over the network. However, this idea of program partitioning can be used to guide the automated application of information flow control to decentralized, distributed systems.

This paper proposes a new approach to security in distributed systems, called secure program partitioning. A program is written in a language in which security policies can be embedded as type annotations. Although the program is to run on a set of communicating hosts, it need not contain explicit information about where code runs or about inter-host communication. Given a set of hosts that are available for execution, a program is then transformed automatically by partitioning its code across the available hosts while ensuring that security invariants are maintained by each partition. The key invariant maintained by the partitioning transformation is that a host manipulates some data only if the host is sufficiently trusted by all principals that have an interest in the privacy or integrity of that data.

This work makes several contributions towards realizing this new model of security enforcement:

• It introduces the security-typed language Spl@ (pronounced “splat”), which has both a unlocated variant in which hosts are not mentioned and a located variant in which the host on which each piece of code runs is explicitly stated. Spl@’s type system validates the information flows within programs of either form and has been shown sound for the language with respect to a simple operational semantics.

• We give type-driven rewrite rules that transform a program from the unlocated form to the located form, partitioning the code among various hosts, while preserving typing. Transfers of control between the hosts are automatically introduced to ensure that security constraints are satisfied.

• Spl@ is the first security-typed language with support for continuations. Continuations are an important linguistic feature for an intermediate language [FSDF93] because they subsume a variety of control structures and closely model low-level computation: in this language, they are the only control structure other than conditionals. However, continuations make acceptably precise bounds on implicit information flow difficult to obtain. This language uses ordered linear continuations in a novel way to recover this precision.

• Spl@ introduces support for security labels that protect both confidentiality and integrity. It also permits selective declassification [ML97, ML00] of both security label components.

Labels

P = Principals
L = {⟨A, B⟩ | A, B ⊆ P}
ℓ, pc ∈ L
⊤ =^{def} ⟨P, ∅⟩
⊥ =^{def} ⟨∅, P⟩

Hosts

h ∈ H
TP(h) ⊆ P

Figure 1: Syntax for labels and hosts

We demonstrate a coupling between confidentiality and integrity in the presence of such a declassification mechanism.

This work does not address termination channels or timing channels. Furthermore, communication between hosts is assumed to be protected and authenticated by encryption; for example, pairwise private-key encryption will suffice. Section 2.9 discusses assumptions about the run-time environment further.

Programs are single-threaded, so various covert information flows that can arise in a concurrent language are not addressed. Termination channels and timing channels are ignored, so programs can leak one bit of information by failing to terminate, or by controlling their run time. Prevention of information flow is also subject to certain assumptions about the distributed computing environment.

The remainder of the paper is organized as follows. Section 2 overviews Spl@’s features at a high level. It then presents the security model and implementation issues. Section 3 illustrates Spl@’s type system and operational semantics, and Section 4 contains a discussion of the language’s formal properties, including the proofs of soundness and noninterference. Section 5 describes the partitioning translation. Sections 6 and 7 finish up with related work and our conclusions.

2 The Spl@ language

This section presents an informal overview of the Spl@ language and sketches how the language can be used to write programs that may then be securely partitioned. Formal definition of the typing rules and operational semantics are given in Section 3 and Appendix A.

2.1 Security labels

As in other security-typed languages [VSI96, ML97, SV98], secure values, written bv_{ℓ}, have both an ordinary value component bv (for base value) and an attached security label ℓ, expressing the security requirements (confidentiality, integrity or both) for that value. The security labels do not need to be maintained at run time, because all run-time label checks will succeed in a well-typed program.

As shown in Figure 1, the lattice of security labels, L, consists of pairs of principals, written ⟨A, B⟩. We use the meta-variables ℓ and pc to range over elements of the security lattice, using the latter to suggest that the label is annotating the program counter, as described below. Labels contain two components: a confidentiality component, A, that controls who is able to view the labeled data, and an integrity component, B, that controls who is able to affect the labeled data. The ordering ⟨A, B⟩ ⊑ ⟨A′, B′⟩ means that a value can be securely relabeled from the label on the left to that on the right. This is the case if the privacy component A′ restricts the dissemination of the value at least as much as A did (otherwise the value could go to new places as the result of a relabeling), and the integrity component B′ claims at most the integrity that B does (otherwise the integrity of the value might be claimed to increase as the result of relabeling).

The privacy and integrity components of the label are a simplified version of those in the decentralized label model [ML00], retaining only the notion of ownership needed for selective declassification. Both the privacy and integrity components are sets of principals drawn from P, which represent users, groups, roles, and other entities with authority. In a privacy component, the set contains the principals that have a stake in the data: they are owners or sources of the data. The principals are similar to categories in classic multilevel security policies [FLR77], except for their interaction with declassification. The ordering on privacy components is ordinary set inclusion: the most restrictive privacy component is the set of all principals P, in which every principal wishes to control the flow of the data; the least restrictive privacy component is the empty set, in which no principal cares about the data.

An integrity component is the set of principals that believe the data not to be corrupted. The ordering relation is reverse set inclusion, because the most restrictive integrity component is the empty set, in which no principal believes that the data has integrity. Such data can only be used in contexts where no integrity is required. The least restrictive integrity is the set of all principals P; since every principal vouches for the integrity of the data, it can be used anywhere.

Given this label structure, the ordering on the security label product lattice is as follows:

\begin{matrix}A ⊆ A′ & B ⊇ B′ \\ ⟨A, B⟩ ⊑ ⟨A′, B′⟩ \end{matrix}

The set of all principals is written as P; given this label ordering, the least possible label ⊥ and the greatest possible label ⊤ are defined as shown in the figure. We use ⊓ and ⊔ to denote the lattice meet and join operators, respectively.

In the located version of the language, hosts may be named explicitly. For each host h in the finite set of all hosts H, TP(h) a set of principals that trusts that h. This set is used statically to determine what data and computation can be placed at h.

2.2 The security context

At any given point during execution, the executing code possesses some authority, a set of principals for which the code is authorized to act. Authority is declared in the program and statements that require authority, such as the declassify primitive, are checked statically against the declared authority.

In addition to authority, each program point has an associated program counter label, pc, that indicates the security label of information on which the program counter depends. Instructions executed at a program counter labeled pc are restricted so they can only transmit information to memory locations with labels higher than pc in L. The program counter label allows implicit flows of information to be controlled conservatively [Mye99].

Together, the authority A and program counter pc constitute a security context for the evaluating code. We write this context as [A, pc].

Types

τ ::= int | 1 | σ ref | [A, ℓ](σ, κ) cont
σ ::= τ_{ℓ}
κ ::= 1 | (σ, κ) lcont

Contexts

Γ ::= • | Γ, x:σ
K ::= • | K, y:ρ

Values

bv ::= n | ⟨⟩ | L^{σ}@h

| cont@h f_{B} [A, ℓ](x:σ, y:κ) = e

v ::= bv_{ℓ} | x
lv ::= ⟨⟩ | lcont@h[A, ℓ](x:σ, y:κ) = e

Primops

prim ::= v | v ⊕ v | deref(v)

| declassify(v, ℓ)

Expressions

e ::= let x = prim in e

| let x = (ref(σ) v)_{ℓ} in e | set v := v in e | if0 v then e else e | letlin y = lv in e | goto v v lv | lgoto lv v lv | actsFor (A) then e else e | setpc (ℓ) in e | halt_{σ} v

Figure 2: Syntax

2.3 Spl@ syntax

The syntax of both the located and unlocated variants of Spl@ is given in Figure 2. The only syntactic difference between the two is that the host annotation on code (@h) is omitted in the unlocated variant. An unlocated program is always equivalent to the same program in the located language, in which annotations locate all code at a universally trusted host (TP(h) = P).

The language is call-by-value, uses continuation-passing style, and includes imperative features intended to be suitable for intermediate stages in a translation of a high-level language such as Jif to lower-level, distributed code.

Spl@ permits only primitive expressions, prim, that manipulate constant values v. Expressions, e, function as statements that return no value. They consist of nested let or letlin expressions that introduce new variables in a sequence terminated by a transfer of control.

The language has state: programs may create, observe, and modify locations in the store using the ref, deref, and set primitives respectively. In the located language, the store locations are situated at the host where the ref primitive was executed. Accesses to a location cause appropriate communication between the current host and the host of the location. When a program terminates execution by evaluating the halt expression, the final value and also the contents of the store are assumed to be visible to principals in accordance with the privacy components of their security labels.

2.4 Types

The types of the language fall into two syntactic classes: security types (ranged over by σ) and linear types (ranged over by κ). Security types are the types of ordinary values and consist of a simple type component (τ) annotated with a security label ℓ. If σ = τ_{ℓ}, then by definition, label(σ) = ℓ. In a well-typed program, the run-time label of the value of an expression is always bounded above in the lattice by the label component of that expression’s security type.

The simple types are the types of integer values, int, a unit type 1, references to a security type, σ ref, and the type of ordinary continuations, [A, pc](σ, κ) cont. Correspondingly, an ordinary base value (bv) is an integer n, a unit ⟨⟩, a memory location L^{σ}@h, or a continuation cont@h f_{B} [A, pc](x: σ, y: κ) = e. For simplicity of presentation, we have omitted even standard type constructors such as pairs and sums, although they could be added easily.

To make the examples in this paper more readable, the labels on unit values, which can transmit no information, often omitted. To avoid having to parenthesize location values like this: (L^{σ}@h)_{ℓ}, we write L_{ℓ}^{σ}@h instead.

An ordinary continuation value, denoted by cont@h f_{B} [A, pc](x: σ, y : κ) = e, is a piece of code (the expression e) located at host h. It accepts a nonlinear argument of type σ and a linear argument of type κ. The code of the continuation has been granted authority at compile time to act for the principals in the set B; presumably those principals have reviewed this code and deemed that it does not violate their security. The notation [A, pc] indicates that this continuation may only be invoked from a calling context in which authority is known to be at least A and in which the program counter is labeled with at most pc. These restrictions are indicated by its type, [A, pc](σ, κ) cont. Ordinary continuations may be recursive: the body of the continuation may invoke itself using the name f.

2.5 Ordered linear continuations

Continuations are particularly useful for an intermediate language because they subsume a variety of other control constructs. However, there is a difficulty in supporting continuations in a securitytyped language. With straightforward, sound typing rules, implicit flows arising from branches in letlin k = lcont[∅, pc](x:1, y:1) = set z := 3 in (∗pc∗) halt1 ⟨⟩

in

if0 x_{H} then set y := 1 in (∗pc ⊔ H∗) lgoto k ⟨⟩ ⟨⟩

else set y := 2 in (∗pc ⊔ H∗) lgoto k ⟨⟩ ⟨⟩

Figure 3: Using ordered linear continuations to improve precision.

the control structure can never be eliminated. Consider the following source-level program, which tests the high-security integer x_{H} and eventually performs the safe assignment to the low-security reference z:

if0 x_{H} then {y := 1; } else {y := 2; }; z := 3;

Informally, a CPS translation of the above code results in something like the following, where k is the continuation of the if0 statement:

let k = (λ(). z := 3) in if0 x_{H} then y := 1; k() else y := 2; k()

The problem is that the invocation of the continuation k appears within the branches of the conditional, so to avoid an implicit flow, the simple typing rules of both SLam [HR98] and Jif [Mye99] conservatively require that k’s body not write to z.

The Spl@ language introduces ordered linear continuations to avoid this loss of precision. Linear continuations differ from ordinary continuations in that, once introduced, they must be invoked exactly once in all subsequent control flow paths (unless the program diverges, in which case the linear continuation may never be invoked). This restriction prevents two different branches in a program from leaking information by discarding or repeating a continuation. To avoid the possibility that information could be leaked by invoking two linear continuations in different orders, Spl@ enforces a stronger property—if used at all, linear continuations that are simultaneously in scope must be used in the same order in every possible execution of the program. In conjunction, these two features allow linear continuations to capture the security context in which they are declared and restore that security context when they are invoked.

Figure 3 shows the example translated using a linear continuations to describe the mergepoint of the two branches, which is allowed because the branches both terminate in jumps to the continuation k. At k’s invocation the program counter contains no information about which branch has been taken, so its label can be restored to what it was at the declaration k. The comments indicate the label of the program counter, assuming it initially starts at label pc. Spl@’s type system enforces a stack discipline for the ordering of linear continuations which can reflect the lexical structure of a higher-level source language. Branches encode information about conditional values into the program counter; linear continuations undo this effect by forcing control back to a single point. A linear continuation is a first-class merge point in the control-flow graph that controls implicit flows with greater precision.

There are two types of linear values (lv): linear unit, used only to indicate the lack of a linear argument to a continuation, and linear continuations themselves. Because a linear continuation restores a captured security context, there are no constraints imposed on that context at the point of invocation. Therefore the types of linear continuations don’t need to mention a security context, and have the form (σ, κ) lcont. Linear values and ordinary values are have distinct syntax in Spl@, and are never allowed in the same syntactic position. For example, the first argument to a continuation must be an ordinary, nonlinear value of type σ and the second must be a linear value of linear type κ. Because Spl@ contains explicit syntax for writing down linear continuations, and their intended meaning is to capture a security context, we must restrict initial programs so that all linear continuations are introduced via the letlin construct. (Otherwise it would be possible to write down linear continuations that don’t capture any appropriate context and hence violate security.)

Linear continuations have another useful property: unlike ordinary values, linear values do not require security annotations, because there is no way to communicate information by selecting among several choices of linear continuations.

2.6 Security invariants

The type system of Spl@ maintains a number of security invariants that are desirable in a system of heterogeneously trusted machines. Type-safety in Spl@ guarantees more than traditional memory safety and progress; there are also guarantees about authority and security.

In general, integrity constraints on data with label ℓ originating from a host h are captured by the requirement that ⟨∅, TP(h)⟩ ⊑ ℓ, that is, the set of principals who trust the data labeled with ℓ is at most the set of principals who trust h. Dually, the confidentiality requirement on data labeled ℓ flowing to a host h is expressed by ℓ ⊑ ⟨TP(h), ∅⟩, which says that the set of principals who own the data are included in those principals who trust the host h. The integrity constraints are enforced when data is sent from a host: the goto, lgoto, halt, and assignment operations. Conversely, privacy constraints appear where information can arrive from another host: the rule for values (which arrive via substitution), and in the declaration rules for both kinds of continuations. These constraints apply to the label of the program counter; so ⟨∅, TP(h)⟩ ⊑ pc ⊑ ⟨TP(h), ∅⟩. For a security label ℓ that satisfies these conditions, we write ⊢ ℓ ok @h.

The requirement that ⟨∅, TP(h)⟩ ⊑ pc can be seen by thinking of the operational behavior of the goto: it effectively transfers control to a (possibly) different host machine. We think of the values that leave h as being stamped with the security label of the program counter at the point of the call (this is made explicit in the operational semantics). Because host h is trusted by only the principals TP(h), the values leaving h should never have more integrity, thus the program counter is bounded below by the integrity constraint ⟨∅, TP(h)⟩ ⊑ pc.

The type system also maintains the invariant that in every security context, A ⊆ TP(h). This guarantees that the authority used in the piece of code running on h does not exceed the maximum authority available to h.

Some simple security properties can be read directly from the operational semantics: for instance, a value with a high security label is never written to a memory location readable by low-security hosts. It is clear that full Spl@ does not exhibit the noninterference property introduced by Goguen and Meseguer [GM82, GM84] and studied in a programming languages setting more recently [VSI96, SV98, HR98], because of the presence of declassify and setpc. Because of the limitations of noninterference, these unsafe operators are important for implementing many programs and are therefore important to model in the language.

2.7 An interaction between privacy and integrity

One subtle aspect of secure program partitioning is that the declassify operator introduces a coupling between the integrity and privacy components of security labels in the program. Clearly, let secret = 42_{⟨{root},P⟩} in … let check = cont@h_{1} check_{{}}[∅, ⊥](x:int_{L}, y : 1) = (

let unsafe = cont@h_{2} unsafe_{{root}}[∅, L](z:1, y:1) = ( let s = declassify(secret, ⟨∅, {root}⟩ ⊔ L) in (∗ pc = L ∗) halt^{⟨∅,{root}⟩⊔L} s

) in

if0 x then goto unsafe ⟨⟩ ⟨⟩ (∗ pc = L ∗)

else halt^{⟨∅,{root}⟩⊔L} 0 )

Figure 4: The need for pc integrity

the declassify operation is unsafe for the principals whose security is weakened by it; it therefore requires that the program has the authority of any such principal p at the point of its use. The security invariant A ⊆ TP(h) then guarantees that the declassification takes place on a suitably trusted host.

However, there is a another invariant to be maintained. Because the declassify operation is unsafe for the principal p, the decision to perform the operation should be based on data that p trusts. This condition is expressed by requiring that the program counter label’s integrity component include p, which ensures that the code that affects the decision to declassify is run only on hosts trusted by p.

Figure 4 shows why this constraint is needed. The program in the figure contains a piece of code named check that tests its argument x and uses its value to decide whether to invoke some encapsulated code named unsafe. The unsafe code uses the authority of the principal root to release the secret value contained in the variable secret (note that the privacy component of the label is declassified from {root} to ∅). Left unspecified in the program are the label L and the two hosts h_{1} and h_{2}. It is clear that the host h_{2} must be a host that the principal root trusts. What is less obvious is that root must also trust h_{1}. If the code of check is run on a host that root does not trust, then that host is in charge of determining whether to invoke unsafe and may do so improperly. Because the integrity component of pc must include at least the principal root, according to the condition above, so must the integrity component of L. Therefore, h_{1} must be trusted by root. This example shows that integrity must be maintained in order to protect privacy.

2.8 A translation example

Figure 5 gives a small example of a C program and its equivalent in the unlocated version of Spl@. (We have omitted the label on the ref operations; assume it is ⊥.) The label H = ⟨{p_{1}, p_{2}}, {p_{1}}⟩ represents a high-security level for secret data, and the label L = ⟨∅, {p_{1}}⟩ is low-security.

The same code after partitioning might look as shown in Figure 6. Note that code that can run on the machine low has been moved there. In this simple example, the host high is trusted by {p_{1}, p_{2}} and low by {p_{1}}. Therefore the data labeled with H is not allowed to move to low ( ⊬ H ok @low). Execution begins on high, and proceeds as follows: high → low → high → low.

2.9 Implementation issues

This work assumes a secure network: messages between hosts cannot be intercepted or damaged. A secure network can be constructed atop an insecure network through well-known encryption techniques. However, the security of Spl@ also requires that some dynamic checks be performed by the run-time system when inter-host actions, such as remote reads or writes, are performed. int h1 = 0; int h2 = 0; int l1 = 0; int l2 = 0; h1 = h2; h2 = h2 + h1; l1 = l2; let h1 = ref (int_{H}) 0 in let h2 = ref (int_{H}) 0 in let l1 = ref (int_{L}) 0 in let l2 = ref (int_{L}) 0 in let t1 = deref(h2) in set h1 := t1 in let t2 = deref(l1) in let t3 = t1 + t2 in set h2 := t3 in let t4 = deref(l2) in set l1 := t4 in

halt_{L} t4

Source Program Spl@ Program

Figure 5: A simple program

let h1 = ref (int_{H}) 0 in let h2 = ref (int_{H}) 0 in letlin lc1 = lcont@low [∅, L](x:1, y:1) = (

let l1 = ref (int_{L}) 0 in let l2 = ref (int_{L}) 0 in letlin hc1 = lcont@high [∅, L](x:1, y:1) = (

let t1 = deref(h2) in set h1 := t1 in let t2 = deref(l1) in let t3 = t1 + t2 in set h2 := t3 in letlin lc2 = lcont@low [∅, L](x:1, y:1) = (

let t4 = deref(l2) in set l1 := t4 in

halt_{L} t4 ) in

lgoto lc2 ⟨⟩ ⟨⟩ ) in

lgoto hc1 ⟨⟩ ⟨⟩ ) in

lgoto lc1 ⟨⟩ ⟨⟩

Figure 6: The simple program partitioned into located form

To invoke an ordinary continuation with type ([A′, pc′](τ, σ) cont)_{ℓ}, the security context [A, pc] at the point of the invocation must satisfy the constraints A′ ⊆ A and pc⊔ℓ ⊑ pc′. A legal invocation of the continuation can only come from one of the hosts satisfying the conditions ⊢ pc′ ok @h and A ⊆ TP(h). This condition is checked dynamically to ensure that an untrusted host does not simulate a call to the continuation and thus fabricate authority. Legal reads and writes to a store location whose contents are labeled with ℓ are also checked dynamically to come only from a host h such that ⊢ l ok @h.

Enforcing the properties of linear continuations at run time requires one-time capabilities. the form (lcont@h …) is evaluated, the host h constructs a closure object and hands the remote reference back to the originating host. The call-site must present the capability to invoke the continuation, after which both the closure and the capability are destroyed.

3 Semantics

This section discusses the novel features of the Spl@ type system and operational semantics. It also sketches some of the formal properties of the language.

3.1 Type system

The type system for Spl@ is similar to those found in the literature [VSI96, ML97, HR98, SV98, Mye99]. This section examines some of the more interesting typing rules; the complete set can be found in Appendix A.

Two separate contexts are maintained for type-checking purposes. We treat Γ as a finite partial map from nonlinear variables (x and f) to security types, whereas K is an ordered list of pairs of linear variables (y) and their corresponding types. The two contexts are separated by ∥ in the typing judgments. The rules maintain the ordering on K: if K = •, (y_{n}:κ_{n}), …, (y_{1} :κ_{1}) then the continuation y_{1} will be invoked before any of the y_{2} … y_{n} are (if at all). K can be strengthened by dropping unit variables^{1}. Also, to avoid problems with associativity of the context concatenation operator, we treat linear contexts as being equivalent up to the rules described in Appendix A.

The first kind of typing judgment is of the form Γ ⊢ v : σ. It determines when the value v is well-typed, and it captures invariants that are independent of the host on which the value is residing. These rules are, for the most part, standard. Ordinary values cannot contain free linear variables because discarding the value would break the linearity constraint.

The rules for linear values are of the form Γ ∥ K ⊢ lv : κ. A linear variable may be mentioned only if no other linear variables are present in the context.

A memory location L_{ℓ}^{σ}@h is a remote pointer to a value of type σ stored on host h. The pointer itself has been annotated with the security label ℓ. In order for such a location to be well formed, it must be the case that the data pointed to by the reference is allowed to reside on h. The security label of σ must have a confidentiality requirement no greater than TP(h), the maximum confidentiality guaranteed by the machine h. Likewise, the integrity of data pointed to by the reference can be no better than TP(h), because only those principals in TP(h) trust the data generated by h. These constraints are captured in the following rules:

⊢ label(σ) ok @h
Γ ⊢ L_{ℓ}^{σ}@h : σ ref_{ℓ}

{⟨∅, TP(h)⟩ ⊑ ℓ ⊑ ⟨TP(h), ∅⟩ \atop ⊢ ℓ ok @h}

1Note that this is sound because it is impossible for linear unit values to reach an active position during evaluation.

Here is the rule for linear continuations:

pc ⊑ ⟨TP(h), ∅⟩
label(σ) ⊑ ⟨TP(h), ∅⟩
Γ, x:σ ∥ y:κ, K [A, pc] @h ⊢ e
Γ ∥ K ⊢ lcont@h[A, pc](x:σ, y:κ) = e : (σ, κ) lcont

The first two conditions require that the labels on the program counter and argument x be public enough that h is trusted to manipulate them. The linear argument, y, can be thought of as the tail of the stack of continuations that have yet to be invoked. Intuitively, this judgment says that the continuation promises to invoke the continuations in K before jumping to the continuation represented by y, and it is under these assumptions that the body e is checked.

During computation, the substitution operation will cause values to propagate to various hosts. To prevent secret data from being sent to untrusted hosts, we also require a rule that determines when it is permissible for a value to be substituted into a located expression. The following rule expresses this privacy constraint:

\begin{matrix}Γ ⊢ v : τ_{ℓ} & ℓ ⊑ ⟨TP(h), ∅⟩ \\ Γ @h ⊢ v : τ_{ℓ} \end{matrix}

The rules for both linear and nonlinear continuations need to determine when the body of the continuation is well-typed. The judgments for type-checking code expressions are of the form Γ ∥ K [A, pc] @h ⊢ e. The remainder of the judgment can be read as “in a context where the program has at least the authority to act for the principals in A, and the control flow depends on values of at most security label pc, the code e can be executed on h.”

As an example, consider the following rule for type-checking conditional branches:

Γ @h ⊢ v : int_{ℓ} Γ ∥ K [A, pc ⊔ ℓ] @h ⊢ e_{i} ⟨∅, TP(h)⟩ ⊑ pc
Γ ∥ K [A, pc] @h ⊢ if0 v then e_{1} else e_{2}

This security annotation ℓ of the integer regulating the branch is propagated to the label of the program counter when type-checking the branches, reflecting the fact that information about v can be learned by observing the program counter in either e_{1} or e_{2}.

The rule for assignment, shown below, checks that the label of the program counter is no more restrictive than the security label, label(σ), of the values that can be stored in the reference. To prevent information from being leaked via aliasing, the label ℓ of the reference value itself may be no more restrictive than the security label of its contained values [DD77, ML97, HR98].

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

Together, these two rules ensure that information learned by branching on an integer cannot be stored into a low-security memory location.

Linear continuations are introduced with the following typing rule:

Γ ∥ K_{2} ⊢ lcont@h′[A′, pc′](x′:σ′, y′:κ′) = e′ : κ′′
κ′′ = (σ, κ) lcont A′ ⊆ A pc ⊑ pc′
Γ ∥ K_{1}, y:κ′′ [A, pc] @h ⊢ e
Γ ∥ K_{1}, K_{2} [A, pc] @h ⊢ letlin y = lcont@h′[A′, pc′](x′:σ′, y′:κ′) = e′ in e

The rule above says that the actual authority declared by the linear continuation (A′) is less than that available (A) when the continuation is introduced, whereas the declared program counter pc′ is more restrictive. These measures ensure that the linear continuation “captures” the security context (or one more restrictive) at the point of declaration.

Maintaining the ordering property on requires some work. The linear context is split into two parts, K_{1} and K_{2}. The body of e is checked under the assumption that continuation y is invoked before any of the continuations in K_{1}. Because the continuation bound to y invokes the continuations in K_{2} before its argument (as seen above in the lcont checking rule), the ordering relation K_{1}, K_{2} in subsequent computation will be respected.

Compare the rules for lgoto and goto:

Γ ∥ K_{2} ⊢ lv_{1} : (σ, κ) lcont
Γ @h ⊢ v : σ
Γ ∥ K_{1} ⊢ lv_{2} : κ

⟨∅, TP(h)⟩ ⊑ pc ⊑ label(σ) A ⊆ TP(h) Γ ∥ K_{1}, K_{2} [A, pc] @h ⊢ lgoto lv_{1} v lv_{2}

Γ @h ⊢ v : [A′, pc′](σ, κ) cont_{ℓ}
Γ @h ⊢ v′ : σ pc ⊔ ℓ ⊑ label(σ)
Γ ∥ K ⊢ lv : κ
⟨∅, TP(h)⟩ ⊑ pc pc ⊔ ℓ ⊑ pc′ A′ ⊆ A ⊆ TP(h)
Γ ∥ K [A, pc] @h ⊢ goto v v′ lv

They both require that the arguments to the continuation be of the right type, and that the label of the argument to the continuation be more restrictive than the current program counter. The key differences are the constraints on the security context of the ordinary continuation. The target of a goto inherits the calling security context, while the target of a lgoto restores the security context of the point at which it was declared.

The proper ordering of the linear context is maintained in the lgoto rule because lv_{1} is being called and promises to invoke its argument after evaluating the continuations in K_{2}. The argument, lv_{2} will, in turn, invoke the continuations in K_{1}, hence keeping the order K_{1}, K_{2}.

The key difference between this rule and the one for normal continuations is that the security label of the calling context does not influence the security label of the body of the linear continuation. This means that when a linear continuation is invoked, the security context is reset to be that of the point where the continuation was declared.

The last typing judgment form in the language determines when a primitive operation is suitable for execution on a particular host in a given security context. The most interesting example is the rule for declassifying values:

Γ @h ⊢ v : τ_{ℓ′} B ⊆ A ℓ′ ⊓ ⟨P, B⟩ ⊑ ℓ ⊔ ⟨B, P⟩ pc ⊑ ⟨P, B⟩ pc ⊑ ℓ
Γ [A, pc] @h ⊢ declassify(v, ℓ) : τ_{ℓ}

This construct allows a set of principals to give up ownership of a piece of data (decrease privacy) or endorse a piece of untrusted data (increase integrity). The authority of the principals necessary to perform the declassification (B) must be included in the authority of the current security context. The relation between ℓ′, the original label of the value, and ℓ, the new label can best be seen as a combination of two simpler inequalities:

ℓ′ ⊓ ⟨P, B⟩ ⊑ ℓ ℓ′ ⊑ ℓ ⊔ ⟨B, P⟩

The left inequality says that only principals in B can add their endorsement to the integrity of the data, so that it is now trusted by those principals who originally trusted it plus the members of B. The right inequality says that only the principals in B may remove their privacy constraints from the data, all the other privacy interests of the original label must still be observed.

The condition pc ⊑ ℓ implies that it is never possible to declassify a value to below the security label on the current program counter. Effectively, each value’s label is implicitly joined with the label of the program counter—the only way to remove the effects of that stamping is to use the setpc expression to declassify the program counter.

The condition pc ⊑ ⟨B, P⟩ says that principals B trust that the program counter has been computed correctly, as discussed in Section 2.7.

3.2 Operational semantics

The operational semantics for this language are given in full in Appendix B. We mention a few salient points here. The model is given in terms of a transition relation between machine configurations of the form

⟨M[A, pc]@h ⊳ e⟩

This configuration denotes a program expression e being run on host h with run-time security context [A, pc] and memory, M.

Memories are finite partial maps from locations to values. A memory M is considered to be wellformed (written M wf) if for each location L^{σ} in M’s domain • ⊢ M(L^{σ}) : σ and, furthermore, that M is closed under dereference. That is, if L^{σ} ∈ Dom(M) and M(L^{σ}) = L^{′σ′} then L^{′σ′} ∈ Dom(M). The notation M[L^{σ} ↦ v] is used to denote both update and extension of the partial map. We use the notation Loc(e) to denote the set of locations appearing in a program e.

The notations e{v/x} and e{lv/y} denote capture-avoiding substitution of ordinary and linear values.

Evaluation of primitive operations causes no side effects and yields a value. The notation [[⊕]] is the semantic operation corresponding to ⊕; thus [[+]] is the integer addition operation.

The operational semantics takes the view that values are stamped with their security labels and these labels are checked at runtime to ensure that no explicit information leaks occur.

4 Soundness and Security

The purpose of this section is to rigorously prove the soundness of Spl@ and show that the fragment not containing declassify and setpc exhibits non-interference.

The proofs in this paper assume that all typing derivations for values and linear values are in canonical form—the derivations alternate between subsumption and non-subsumption rules, ending with a subsumption rule. (It is always possible to put proofs in this canonical form because of the reflexivity and transitivity of the ≤ relation.) Similarly, we always assume that the linear contexts, K, are equivalent up to the ≡ relation, and so omit specific equivalence rules unless needed for clarity. We also adopt the convention that label(τ_{ℓ}) = ℓ.

Ordinary contexts, Γ, are subject to the usual Strengthening, Weakening, and Exchange operations; however, linear contexts, K, are not.

As mentioned earlier, we must rule out certain well-typed programs that violate security by starting out with linear continuations that don’t correspond to merge points. For example, we need to rule out programs such as

if0 h then

lgoto (lcont@h[A, ⊥](x:1, y:1) = set l := 0 in …) ⟨⟩ ⟨⟩

else

lgoto (lcont@h[a, ⊥](x:1, y:1) = set l := 1 in …) ⟨⟩ ⟨⟩

We thus make the provision that in a well-formed initial program, all linear continuations are introduced via letlin.

Definition 4.1 (Initial Program) An initial program is an expression e such that Loc(e) = ∅, and, for each lgoto lv_{1} v lv_{2} subexpression of e, lv_{1} is a variable and lv_{2} is either a variable or ⟨⟩.

4.1 Soundness

This section proves the soundness theorem for Spl@. The proof is, for the most part, standard, following in the style of Wright and Felleisen [WF92, WF94]. We omit discussion of the Subject Reduction and Progress lemmas.

A simple proposition that we shall not prove is the following:

Proposition 4.1 (Base Value Relabeling) If Γ ⊢ bv_{ℓ} : τ_{ℓ} then Γ ⊢ bv_{ℓ′} : τ_{ℓ′}.

We shall use the Base Value Relabeling proposition without mentioning it explicitly in the proofs below.

Lemma 4.1 (Substitution I) Assume Γ @h ⊢ v : σ then

(i) If Γ, x:σ @h′ ⊢ v′ : σ′ then Γ @h′ ⊢ v′{v/x} : σ′.

(ii) If Γ, x:σ ∥ K ⊢ lv : κ then Γ ∥ K ⊢ lv{v/x} : κ.

(iii) If Γ, x:σ [A, pc] @h′ ⊢ prim : σ′ then Γ [A, pc] @h′ ⊢ prim{v/x} : σ′.

(iv) If Γ, x:σ ∥ K [A, pc] @h′ ⊢ e then Γ ∥ K [A, pc] @h′ ⊢ e{v/x}.

Proof: By mutual induction on the (canonical) derivations of (i)–(iv).

(i) By assumption, there exists a derivation of the form

\begin{matrix}Γ, x:σ ⊢ v′ : σ′′ & ⊢ σ′′ ≤ σ′ \\ Γ, x:σ ⊢ v′ : σ′ \end{matrix} label(σ′) ⊑ ⟨TP(h′), ∅⟩
Γ, x:σ @h′ ⊢ v′ : σ′

We proceed by cases on the rule used to conclude Γ, x:σ ⊢ v′ : σ′′. In cases [TV1 ], [TV2 ], and [TV3 ] we have v′{v/x} = v′, and the result follows by Strengthening and derivation above. In the case of [TV4 ], we have either x{v/x} = v, which, by assumption, has type σ = σ′′ or x′{v/x} = x′, also of type σ′′. In either case, this information plus the derivation above yields the desired result. The case of [TV5 ] follows from inductive hypothesis (iv).

(ii) This cases follows analogously to the case for (i); the rule [TL3 ] makes use of inductive hypothesis (iv).

(iii) This follows directly from the inductive hypothesis (i).

(iv) Follows by inductive hypotheses (i)–(iv).

□

Note that neither ordinary values nor primitive operations may contain free linear variables. This means that substitution of a linear value in them has no effect. The following lemma strengthens substitution to open linear values and also shows that the ordering on the linear context is maintained.

Lemma 4.2 (Substitution II) Assume • ∥ K ⊢ lv : κ and that all bound linear variables appearing in lv′ and e are disjoint from K. Furthermore, assume that K contains only linear continuation types. Then

(i) If Γ ∥ K_{1}, y:κ, K_{2} ⊢ lv′ : κ′ then Γ ∥ K_{1}, K, K_{2} ⊢ lv′{lv/y} : κ′.

(ii) If Γ ∥ K_{1}, y:κ, K_{2} [A, pc] @h′ ⊢ e then Γ ∥ K_{1}, K, K_{2} [A, pc] @h′ ⊢ e{lv/y}.

Proof: By mutual induction on the (canonical) typing derivations of (i) and (ii).

(i) The canonical typing derivation for lv′ is:

\begin{matrix}Γ ∥ K_{1}, y:κ, K_{2} ⊢ lv′ : κ′′ & ⊢ κ′′ ≤ κ′ \\ Γ ∥ K_{1}, y:κ, K_{2} ⊢ lv′ : κ′ \end{matrix}

We proceed by cases on the rule used to conclude Γ ∥ K_{1}, y:κ, K_{2} ⊢ lv′ : κ′′.

[TL1 ] Then κ′′ = 1 and K_{1}, y: κ, K_{2} ≡ •. It follows that κ = 1 and all the types mentioned in K_{1}, K_{2}, and K must be 1 as well. Thus, K = •. By the equivalence rules for linear contexts, we have K_{1}, K, K_{2} ≡ K_{1}, K_{2} ≡ •. It thus follows that ⟨⟩{lv/y} = ⟨⟩, and Γ ∥ K_{1}, K_{2} ⊢ ⟨⟩ : κ′′.

[TL2 ] If lv′ = y and κ′′ = 1 then κ = 1. It follows that K ≡ • ≡ K_{1}, y: 1, K_{2} ≡ K_{1}, K, K_{2}. By definition of substitution, lv′{lv/y} = lv and so we have Γ ∥ K_{1}, K_{2} ⊢ lv : κ′′. This, plus the fact that κ′′ ≤ κ′ concludes this case. If lv′ = y and κ′′ = κ ≠ 1, it follows that K_{1}, y : κ, K_{2} ≡ y : κ, and hence K_{1} ≡ K_{2} ≡ •. This implies that K_{1}, K, K_{2} ≡ K and thus by the assumption that lv = y{lv/y} is well-typed under K, we have Γ ∥ K_{1}, K, K_{2} ⊢ lv : κ, and the result follows from the subtyping of κ ≤ κ′. If lv′ = y′ ≠ y then σ = 1 and it follows that K ≡ •. Thus K_{1}, K, K_{2} ≡ K_{1}, K_{2}. Furthermore, lv′{lv/y} = lv′ = y′ and we have Γ ∥ K_{1}, K, K_{2} ⊢ lv′ : κ′′. The result follows via subtyping.

[TL3 ] This case follows immediately from inductive hypothesis (ii) using the assumption that the bound linear variable in the linear continuation is disjoint from K.

(ii) This part of the lemma follows almost immediately from the inductive hypotheses. The interesting cases are [TE5 ] and [TE7 ], which must ensure that the ordering on the linear context is maintained. We show the case for [TE5 ], as [TE7 ] uses the same technique.

[TE5 ] By assumption, there is a derivation of the following form:

Γ ∥ K_{b} ⊢ lcont@h′′[A′, pc′](x′:σ′, y′:κ′) = e′ : κ′′
κ′′ = (σ, κ) lcont A′ ⊆ A pc ⊑ pc′
Γ ∥ K_{a}, y:κ′′ [A, pc] @h′ ⊢ e

Γ ∥ K_{1}, y:κ, K_{2} [A, pc] @h′ ⊢ letlin y′′ = lcont@h′′[A′, pc′](x′:σ′, y′:κ′) = e′ in e

Where K_{1}, y : κ, K_{2} ≡ K_{a}, K_{b}. If y appears in K_{a} then K_{a} ≡ K_{1}, y : κ, K_{2}^{−} and K_{b} ≡ K_{2}^{+} where K_{2}^{−}, K_{2}^{+} ≡ K_{2}. In this case, y can’t appear in K_{b} and it follows that e′{lv/y} = e′. Inductive hypothesis (ii) applied to Γ ∥ K_{1}, y:κ, K_{2}^{−} [A, pc] @h′ ⊢ e yields Γ ∥ K_{1}, K, K_{2}^{−} [A, pc] @h′ ⊢ e{lv/y}. Thus, an application of rule [TE5 ] yields the desired result, as K_{1}, K, K_{2}^{−}, K_{2}^{+} ≡ K_{1}, K, K_{2}. The case in which y appears in K_{b} is similar to the one above, except that K_{1} is split into K_{1}^{−} and K_{1}^{+}. If y appears in neither K_{a} or K_{b} then κ = 1 and it follows that K ≡ •, which also yields the desired result.

□

Lemma 4.3 (Canonical Forms I) If • ⊢ v : σ then (i) If σ = int_{ℓ} then v = n_{ℓ′} for some integer n and ℓ′ ⊑ ℓ. (ii) If σ = 1_{ℓ} then v = ⟨⟩_{ℓ′} for some ℓ′ ⊑ ℓ. (iii) If σ = σ′ ref_{ℓ} then v = L_{ℓ′}^{σ′}@h for some h and ℓ′ ⊑ ℓ. (iv) If σ = [A, pc](σ′, κ) cont_{ℓ} then v = (cont@h f_{B} [A′, pc′](x : σ′′, y : κ′) = e)_{ℓ′} where ℓ′ ⊑ ℓ,

A′ ⊆ A, pc ⊑ pc′, ⊢ σ′ ≤ σ′′, and ⊢ κ ≤ κ′. Proof (sketch): By inspection of the typing rules and the form of values. □ Lemma 4.4 (Canonical Forms II) If • ∥ • ⊢ lv : κ then

(i) If κ = 1 then lv = ⟨⟩ or lv = y. (ii) If κ = (σ, κ′) lcont then lv = lcont@h[A, pc](x:σ′, y:κ′′) = e where ⊢ σ ≤ σ′ and ⊢ κ′ ≤ κ′′. Proof (sketch): By inspection of the typing rules and the form of linear values. □ Definition 4.2 (Memory Well-formedness) A memory, M, is a partial finite map from the set of locations to closed values. M is said to be well formed, written M wf, if the following conditions hold:

(i) For each L^{σ} in the domain of M, • ⊢ M(L^{σ}) : σ. (ii) M is closed under dereference, that is if M(L^{σ}) = L^{′σ′} then M(L^{′σ′}) is defined. Definition 4.3 (Locations) For any primitive operation, prim (respectively program, e), let Loc(prim) (respectively Loc(e)), be the set of all locations L^{σ}@h appearing in prim (respectively e). Lemma 4.5 (Primitive Evaluation) If • [A, pc] @h ⊢ prim : σ and M wf and Loc(prim) ⊆ Dom(M) and M[A, pc]@h ⊢ prim ⇓ v then • @h ⊢ v : σ. Proof: By cases on the evaluation rule used. [P1 ] By assumption, we have

\begin{matrix}\begin{matrix}\begin{matrix}• ⊢ bv_{ℓ} : τ_{ℓ} & ⊢ τ_{ℓ} ≤ τ′_{ℓ′} \\ • ⊢ bv_{ℓ} : τ′_{ℓ′} \end{matrix} & ℓ′ ⊑ ⟨TP(h), ∅⟩ \\ • @h ⊢ bv_{ℓ} : τ′_{ℓ′} \end{matrix} & pc ⊑ ℓ′ \\ • [A, pc] @h ⊢ bv_{ℓ} : τ′_{ℓ′} \end{matrix}

We need to show • @h ⊢ bv_{ℓ⊔pc} : . It follows from the derivation above that ℓ ⊑ ℓ′, and as pc ⊑ ℓ′ it is the case that ℓ ⊔ pc ⊑ ℓ′. Thus we have the inequality τ_{ℓ⊔pc} ≤ τ′_{ℓ′}, and so the result follows by subsumption and an application of the rule [TV7 ].

[P2 ] This case is similar to the previous one. [P3 ] In this case, we assume a derivation of the following form:

• ⊢ L_{ℓ′}^{τ_{ℓ}}@h′ : τ_{ℓ} ref_{ℓ′} ⊢ τ_{ℓ} ref_{ℓ′} ⊑ τ_{ℓ} ref_{ℓ′′}
• @h ⊢ L_{ℓ′}^{τ_{ℓ}}@h′ : τ_{ℓ} ref_{ℓ′′} pc ⊑ ℓ ⊔ ℓ′′ ⊑ ⟨TP(h), ∅⟩
• [A, pc] @h ⊢ deref(L_{ℓ′}^{τ_{ℓ}}@h′) : τ_{ℓ⊔ℓ′′}

By the well-formedness of M, M(L^{τ_{ℓ}}) = bv_{ℓ′′′} and we also have • ⊢ bv_{ℓ′′′} : τ_{ℓ}. This implies that ℓ′′′ ⊑ ℓ. We must show that • @h ⊢ bv_{ℓ′⊔ℓ′′′⊔pc} : τ_{ℓ⊔ℓ′′} but this follows from subsumption

and rule [TV7 ] because ℓ′ ⊔ ℓ′′′ ⊔ pc ⊑ ℓ ⊔ ℓ′′.

[P4 ] This case follows, as in the first two cases, from the assumption that pc ⊑ ℓ in the preconditions of rule [TP4 ] plus subsumption.

□

Lemma 4.6 (Program Counter Label) If Γ ∥ K [A, pc] @h ⊢ e then ⟨∅, TP(h)⟩ ⊑ pc ⊑ ⟨TP(h), ∅⟩

Proof (sketch): By induction on the derivation that e is well-typed. The left inequality follows from the presence of ⟨∅, TP(h)⟩ ⊑ pc on rules for expressions which end basic blocks. The right inequality follows from the presence of inequalities of the form pc ⊔ ℓ ⊑ label(σ), where σ is the type of a primitive operation or value typechecked at h. Because the rule for typechecking values (or primitive expressions) at h includes the condition label(σ) ⊑ ⟨TP(h), ∅⟩ it follows that pc ⊑ ⟨TP(h), ∅⟩. □

Lemma 4.7 (Program Counter Variance) If Γ ∥ K [A, pc ⊔ ℓ] @h ⊢ e and ⟨∅, TP(h)⟩ ⊑ pc and ℓ′ ⊑ ℓ then Γ ∥ K [A, pc ⊔ ℓ′] @h ⊢ e.

Proof: The proof is by induction on the derivation that e is well-typed. Note that because pc ⊔ ℓ′ ⊑ pc ⊔ ℓ all inequalities involving pc ⊔ ℓ on the left of ⊑ in the typing rules will still be valid with pc ⊔ ℓ′. To see that inequalities in which pc ⊔ ℓ appear on the right of ⊑ still hold, note that these occur only when the left-hand side is ⟨∅, TP(h)⟩. Because ⟨∅, TP(h)⟩ ⊑ pc ⊑ pc ⊔ ℓ′ these inequalities are still valid as well. □

Lemma 4.8 (Authority) If Γ ∥ K [A, pc] @h ⊢ e then A ⊆ TP(h).

Proof: By induction on the typing derivation for e. The base cases, halt, goto, and lgoto all explicitly mention this condition. The remainder of the cases follow immediately by the inductive hypothesis. □

Lemma 4.9 (Subject Reduction) If • ∥ K [A, pc] @h ⊢ e, and M wf, and Loc(e) ⊆ Dom(M) and

⟨M[A, pc]@h ⊳ e⟩ ⟼ ⟨M′[A′, pc′]@h′ ⊳ e′⟩

Then • ∥ K [A′, pc′] @h′ ⊢ e′ and M′ wf, and Loc(e′) ⊆ Dom(M′).

Proof: By cases on the transition step taken:

[O1 ] Because let x = prim in e is well-typed, prim is too. Thus by the Primitive Evaluation Lemma, prim evaluates to a value v of the same type. Substitution I, part (iv) tells us that e{v/x} is well-typed. Because M doesn’t change it is still well-formed, and to see that Loc(e{v/x}) ⊆ Dom(M) consider that the only way Loc(e{v/x}) could be larger than Loc(let x = prim in e) is if prim is a dereference operation and the memory location contains another location not in e. This case is covered by the requirement that M be closed under dereference.

[O2 ] By assumption, that • ∥ K [A, pc] @h ⊢ let x = (ref(σ) bv_{ℓ})_{ℓ′} in e. Working backwards through the canonical derivation yields the following antecedents: • ⊢ bv_{ℓ} : τ_{ℓ}, and ⊢ τ_{ℓ} ≤ σ, and label(σ) ⊑ ⟨TP(h), ∅⟩, and pc ⊑ label(σ), and pc ⊑ ℓ′ ⊑ ⟨TP(h), ∅⟩, and x:σ ref_{ℓ′} ∥ K [A, pc] @h ⊢ e. From these we conclude that pc ⊔ ℓ′ ⊑ ℓ′ ⊑ ⟨TP(h), ∅⟩ and via [TV3 ] and [TV7 ] it follows that • @h ⊢ L_{ℓ′⊔pc}^{σ}@h : σ ref_{ℓ′}. This fact, plus the well-typedness of e lets us apply Substitution Lemma I, (iv) to conclude • ∥ K [A, pc] @h ⊢ e{L_{ℓ′⊔pc}^{σ}@h/x}. Now, to see that the conditions on M are maintained, note that if bv is a location, then it is contained in the set of locations of the entire let expression and thus, by assumption must occur in the domain of M. This implies that M[L^{σ} ↦ bv_{ℓ⊔pc}] is still closed under dereference. Finally, we must check that • ⊢ bv_{ℓ⊔pc} : σ, but this follows from subsumption and the facts that τ_{ℓ} ≤ σ and pc ⊑ label(σ).

[O3 ] This case follows similarly to the previous case.

[O4 ] Assume that • ∥ K [A, pc] @h ⊢ if0 0_{ℓ} then e_{1} else e_{2}. It follows that • ⊢ 0_{ℓ} : int_{ℓ′} and ℓ ⊑ ℓ′ and that ℓ′ ⊑ ⟨TP(h), ∅⟩ and • ∥ K [A, pc ⊔ ℓ′] @h ⊢ e_{1}. Furthermore, pc ⊑ ⟨TP(h), ∅⟩ and so it follows by the Program Counter Variance Lemma that • ∥ K [A, pc ⊔ ℓ] @h ⊢ e_{1}. Because M doesn’t change and it initially satisfied the well-formedness conditions and the locations of e_{1} are a subset of the locations of the entire conditional, M is still valid after the transition.

[O5 ] This case is nearly identical to the previous one.

[O6 ] This case follows from Substitution II, (ii), and the fact that the conditions on M are satisfied after the substitution. Note that the order of K is preserved by the step.

[O7 ] This case follows from the well-typedness of the body of the continuation being jumped to, plus two applications of Substitution I, (iv) and one application of Substitution II, (ii). The fact that bv_{ℓ′⊔ℓ⊔pc} has type σ follows from subsumption and the fact that pc ⊔ ℓ ⊑ label(σ).

[O8 ] This case is similar to the previous case.

[O9 ] This case follows immediately from the fact that the setpc body is well-typed under pc′. The memory invariants carry through because the locations of the entire expression are just those in the body of the setpc.

□

Definition 4.4 A configuration ⟨M[A, pc]@h ⊳ e⟩ is stuck if e is not halt_{σ} v for some value v or no transition rule applies.

Lemma 4.10 (Progress) If • ∥ • [A, pc] @h ⊢ e and M wf and Loc(e) ⊆ Dom(M), then either e is of the form halt_{σ} v or there exist M′, A′, pc′, and e′ such that

⟨M[A, pc]@h ⊳ e⟩ ⟼ ⟨M′[A′, pc′]@h′ ⊳ e′⟩

Proof (sketch): By the Canonical Forms lemmas and inspection of the rules. We must ensure that conditions such as ⊢ ℓ⊔pc ok @h on rule [P1 ] are met by well-typed terms. These follow from the Program Counter Label lemma and the fact that ℓ is obtained by typing a value at h, which implies that ℓ ⊑ ⟨TP(h), ∅⟩. The conditions on the authority are implied by the Authority lemma.

□

Theorem 4.1 (Type Soundness) Well-typed programs do not get stuck.

Proof: By induction on the number of transition steps taken, using Subject Reduction and Progress. □

4.2 Noninterference

This section proves a noninterference result for the subset of Spl@ that excludes declassify and setpc. The proof is inspired by the preservation-style proof of noninterference used by Volpano and Smith [SV98], and shares some similarities with the logical-relations style proof given by Heintze and Riecke [HR98].

Informally, the noninterference result shows that low-security computations are not able to observe high-security data. Here, “low-security” refers to an arbitrary label ζ or labels ⊑ ζ, and “high-security” values are those whose labels are ⋢ ζ. At a high level, the proof works by showing that at each point in the program’s evaluation, the high-security data can be “factored out” of the computation, and arbitrarily changed. The noninterference result then states that the original computation and the one with altered high-security data eventually compute the same low-security integer as output. Furthermore, the memory locations visible to low-security observers (those location storing data labeled ⊑ ζ) will also be indistinguishable at the end of the computation.

It is worth making a few comments about the strength of this result before describing it in more detail. As with previous noninterference results for call-by-value languages [HR98], the noninterference result holds only for programs which halt regardless of the high-security data. This means that information about high-security values can affect whether the program terminates. There are other possible channels that are not captured by this notion of noninterference: high-security values can alter the amount of time it takes for the program to compute an answer or alter the memory consumption of the program. We are able to prove noninterference 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).

Intuitively, there are two things that we must keep track of to determine whether a program exhibits the noninterference property. First, values with labels higher than ζ might potentially leak to a low-security observer. This is addressed in the type system by guaranteeing that the program counter label is at least as high as the label on any value that has influenced the control flow of the program, plus checks to make sure that, for instance, high security data is not written into low-security memory locations. It is easy to verify from the operational and static semantics that the program counter label is monotonically increasing except in the case that a linear continuation is invoked. Thus, the second thing which must be carefully regulated is how linear continuations are used—the ordering property is the crucial feature here.

To capture these two important features, we will use substitutions.

Definition 4.5 (Substitutions) If Γ is any context, then 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).

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

A substitution γ will be applied to an expression e, written γ(e) to indicate the captureavoiding substitution of the value γ(x) for free occurrences of x in the expression e for each variable x ∈ Dom(γ). We use the similar notation k(e) for application of linear substitutions to a term e.

One of the invariants maintained by well-typed programs is that at each evaluation step it is possible to factor out the relevant high-security values and those linear continuations that reset the program-counter label to be ⊑ ζ.

The idea that the substitutions contain the “relevant” information is contained in the following definitions. First, we must allow linear continuations which set the program counter label ⋢ ζ to appear in the term, because, from the low-security point of view, they are not relevant. This observation motivate the following definition:

Definition 4.6 (lgoto Invariant) A term satisfies the lgoto invariant if for every subexpression of the form lgoto lv_{1} v lv_{2}, it is the case that if lv_{i} = (lcont@h_{i}[A_{i}, pc_{i}](…) = …) then pc_{i} ⋢ ζ.

If k is a substitution containing only low-security continuations, and k(e) is a closed-term such that e satisfies the lgoto Invariant, then all of the low-security continuations used in k(e) must be obtained from k. In this way, we ensure that we have factored out all of the relevant continuations.

What does it mean for us to have factored out the appropriate high-security data? Assume that we wish to show that two e_{1} and e_{2} behave the same from the low-point of view. If the program counter is ⊑ ζ, meaning that e_{1} and e_{2} can perform actions visible to the low observer, a necessary condition for them to be equivalent is that they must perform the same computation on low-security values. Thus, if e_{1} are allowed to differ in their behavior on high-security data, we should at least be able to find substitutions γ_{1} and γ_{2} such that both substitutions contain only high-security data and e_{1} = γ_{1}(e) and e_{2} = γ_{2}(e). Note that e_{1} and e_{2} can both be written in terms of e, after factoring out the high-security data. On the other hand, if the program counter is ⋢ ζ, then no-matter what e_{1} and e_{2} do, their actions should not be visible from the low point of view. If we extend these intuitions to values and memories, we obtain the formal definitions below:

Definition 4.7 (Substitution Equivalence) Γ ⊢ γ_{1} ≈_{ζ} γ_{2} and Γ ∥ K ⊢ k_{1} ≈_{ζ} k_{2} We write Γ ⊢ γ_{1} ≈_{ζ} γ_{2} if and only if γ_{1}, γ_{2} ⊧ Γ and for every x ∈ Dom(Γ) it is the case that label(γ_{1}(x)) ⋢ ζ and label(γ_{2}(x)) ⋢ ζ. Furthermore, we require that γ_{i}(x) satisfy the lgoto invariant.

We write Γ ∥ K ⊢ k_{1} ≈_{ζ} k_{2} if and only if Γ ⊢ k_{1}, k_{2} ⊧ K and for every y ∈ Dom(K) it is the case that k_{1}(y) ≡_{α} k_{2}(y) = lcont@h[A, pc](x: σ, y′: κ) = e and pc ⊑ ζ. It is also necessary that e satisfy the lgoto invariant.

Value Equivalence v_{1} ≈_{ζ} v_{2} : σ

We write v_{1} ≈_{ζ} v_{2} : σ if and only if there exist Γ, γ_{1}, and γ_{2} plus terms v′_{1} ≡_{α} v′_{2} such that Γ ⊢ γ_{1} ≈_{ζ} γ_{2} and Γ ⊢ v′_{1} : σ and Γ ⊢ v′_{2} : σ and v_{1} = γ_{1}(v′_{1}) and v_{2} = γ_{2}(v′_{2}). Furthermore, v′_{i} must each satisfy the lgoto invariant.

Memory Equivalence M_{1} ≈_{ζ} M_{2}

We write M_{1} ≈_{ζ} M_{2} if an only 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^{σ}) : σ. Furthermore, M_{1} wf and M_{2} wf.

Note that this equivalence on memories does not say anything about the locations containing high-security data.

Definition 4.8 (Noninterference Invariant) The noninterference invariant is a predicate Γ ∥ K ⊢ ⟨M_{1}[A_{1}, pc_{1}]@h_{1} ⊳ e_{1}⟩ ≈_{ζ} ⟨M_{2}[A_{2}, pc_{2}]@h_{2} ⊳ e_{2}⟩ which holds if and only if the following conditions are all met:

(i) There exist substitutions γ_{1}, γ_{2}, k_{1}, and 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 h_{1} = h_{2} and e′_{1} ≡_{α} e′_{2} or (b) Γ ∥ K [A, pc_{1}] @h ⊢ e′_{1} and Γ ∥ K [A′, pc_{2}] @h′ ⊢ 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 lgoto invariant.

The Noninterference Invariant conditions spell out the intuition above. Clause (i) says that we can factor the important high-security information and low-security linear continuation out of the computations. Clause (ii) says that if the programs are evaluating under low-security pc, then the underlying computations being performed are the same, whereas when the pc is high, it shouldn’t matter what the two computations do. Clauses (iii), (iv), and (vi) say collectively that we have factored out the relevant information. Finally, clause (v) says that the memories contain equivalent information from the low-security perspective.

The strategy for proving Noninterference is to show that evaluation preserves the invariant. When the program counter is low, equivalent configurations should evaluate in lock-step (modulo the values of high-security data). After the program has branched on high-security information (or jumped to a high-security continuation), the two configurations may temporarily get out of sync, but during that time, they may only affect high-security data. Eventually, when the program counter drops low again (via a linear continuation) both computations return to lock-step evaluation.

The first lemma we prove shows that the linear continuations do indeed get called in the order described by the linear context.

Lemma 4.11 (Linear Continuation Ordering) Assume K = y_{n}: k_{n}, …, y_{1} : k_{1} and each k_{i} is a linear continuation type and • ∥ K [A, pc] @h ⊢ e. If • ⊢ k ⊧ K then in any well-formed configuration ⟨M[A, pc]@h ⊳ k(e)⟩ the continuation k(y_{1}) will be invoked before any of the k(y_{i}).

Proof: The operational semantics is valid for open terms and, indeed, Subject Reduction was proved for open terms. The Progress Lemma, however, does not hold for open terms. Evaluate the open term e in the configuration ⟨M[A, pc]@h ⊳ e⟩. If the computation diverges, then 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, and the halt expression requires that the linear context be empty). The stuck term must be of the form lgoto y_{i} v lv, and, because this term is well-typed, rule [TE7 ] implies that y_{i} = y_{1}. Thus, in the computation of k(e), the continuation k(y_{1}) is invoked first. □

Next, we prove that equivalent configurations evaluate in lock-step as long as the program counter is low.

Lemma 4.12 (Low-pc Step) If Γ ∥ K ⊢ ⟨M_{1}[A_{1}, pc]@h⊳e_{1}⟩ ≈_{ζ} ⟨M_{2}[A_{2}, pc]@h⊳e_{2}⟩ and pc ⊑ ζ and

⟨M_{1}[A_{1}, pc]@h ⊳ e_{1}⟩ ⟼ ⟨M′_{1}[A′_{1}, pc_{1}]@h_{1} ⊳ e′_{1}⟩

then

⟨M_{2}[A_{2}, pc]@h ⊳ e_{2}⟩ ⟼ ⟨M′_{2}[A′_{2}, pc_{2}]@h_{2} ⊳ e′_{2}⟩

and there exist Γ′ and K′ such that Γ′ ∥ K′ ⊢ ⟨M′_{1}[A′_{1}, pc_{1}]@h_{1} ⊳ e′_{1}⟩ ≈_{ζ} ⟨M′_{2}[A′_{2}, pc_{2}]@h_{2} ⊳ e′_{2}⟩.

Proof: 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 Noninterference Invariant. Note that because pc ⊑ ζ, clause (ii) implies that e′′_{1} and e′′_{2} must be alpha-equivalent expressions. This means that the only difference in their operational behavior arises due to the substitutions being supplied, or the different memories. We proceed by cases on the transition step taken by the first program.

[O1 ] By α-equivalence, each e′′_{i} must be of the form let x = prim in e. Conditions (iv), (v), and (vi) will hold after the transition step because those parts of the configuration don’t change. It suffices to find γ′_{i} such that e′_{1} = γ′_{1}(k_{1}(e′′_{1})) and e′_{2} = γ′_{2}(k_{2}(e′′_{2})) where e′′_{1} ≡_{α} e′′_{2} Consider the evaluation M_{1}[A, pc]@h ⊢ γ_{1}(prim) ⇓ bv_{ℓ}. If ℓ ⊑ ζ then prim cannot contain any free variables, for otherwise condition (iii) would be violated. Thus, γ_{1}(prim) = prim = γ_{2}(prim), and because M_{1} ≈_{ζ} M_{2} it follows that M_{2}[A′, pc]@h ⊢ γ_{2}(prim) ⇓ bv_{ℓ}. Thus, we take γ′_{1} = γ_{1}, γ′_{2} = γ_{2} and e′′_{i} = e{bv_{ℓ}/x}. Condition (iii) holds because it originally did; conditions (i) and (ii) are easily verified based on the operational semantics and the fact that pc_{1} = pc_{2} = pc.

On the other hand, if ℓ ⋢ ζ then M_{2}[A′, pc]@h ⊢ γ_{2}(prim) ⇓ bv′_{ℓ′} where it is also the case that ℓ′ ⋢ ζ. (prim either contains a variable, which forces ℓ′ to be high, or prim contains a value explicitly labeled with a high-label.) It follows that • ⊢ bv_{ℓ} ≈_{ζ} bv′_{ℓ′} and so we take γ′_{1} = γ_{1}{x ↦ bv_{ℓ}} and γ′_{2} = γ_{2}{x ↦ bv′_{ℓ′}}. Take e′′_{i} = e. Condition (iii) continues to hold because the Primitive Evaluation lemma implies that the mapped values have the correct types and have high-labels. Conditions (i) and (ii) follow from the definition of the operational semantics and the fact that e ≡_{α} e, respectively.

[O2 ] Each e′′_{i} must be of the form let x = (ref(σ) v_{i})_{ℓ} in e where γ_{i}(v_{i}) = bv_{iℓ_{i}}. By condition (ii) it follows that v_{1} ≡_{α} v_{2} and hence that γ_{1}(v_{1}) ≈_{ζ} γ_{2}(v_{2}). We may thus choose M′_{i} = M_{i}[L^{σ} ↦ γ_{i}(v_{i})] and still maintain that M′_{1} ≈_{ζ} M′_{2}, which implies (v). Now, e′_{i} = γ_{i}(k_{i}(e{x/L_{ℓ⊔pc}^{σ}@h})) and from the operational semantics, we have pc_{1} = pc_{2} = pc so that both conditions (i) and (ii) still hold. Conditions (iii), (iv), and (vi) are still satisfied.

[O3 ] This case follows similarly to the previous two cases.

[O4 ] In this case, each e′′_{i} is of the form if0 v then e_{a} else e_{b}. Furthermore, γ_{1}(v_{1}) = 0_{ℓ}. In the case that ℓ ⊑ ζ, it must be the case that γ_{2}(v_{2}) = 0_{ℓ}, otherwise one of conditions (ii) or (iii) would be violated. The operational semantics thus allow us to choose γ′_{i} = γ_{i}, k′_{i} = k_{i}, M′_{i} = M_{i}, pc_{1} = pc_{2} = pc ⊔ ℓ, and e′_{1} = γ_{1}(k_{1}(e_{a})) and e′_{2} = γ_{2}(k_{2}(e_{a})). All of the conditions hold easily, as pc ⊔ ℓ ⊑ ζ.

In the case that ℓ ⋢ ζ, it is possible for γ_{1}(v) to equal 0_{ℓ} and γ_{2}(v) to equal n_{ℓ′} where n ≠ 0. In this case the first compuation takes the the first branch and the second compuation takes the second branch. However, it must be the case that ℓ′ ⋢ ζ, so in both computations the program counter after the step is ⋢ ζ, and we ma relate the resulting configurations via part (b) of clause (ii). Concretely, γ′_{i} = γ_{i}, k′_{i} = k_{i}, M′_{i} = M_{i}, pc_{1} = pc ⊔ ℓ, pc_{2} = pc ⊔ ℓ′, e′_{1} = γ_{1}(k_{1}(e_{a})) and e′_{2} is either γ_{2}(k_{2}(e_{a})) or γ_{2}(k_{2}(e_{b})). These choices correspond to the operational semantics, and allow us to verify that all of the Noninterference Invariant conditions hold.

[O5 ] This case is nearly identical to the previous one.

[O6 ] Then each e′′_{i} is of the form letlin y = lcont@h′[A, pc′](x: σ, y′: κ) = e′ in e. Furthermore, because the term is well-typed under Γ and K, we have K ≡ K_{1}, K_{2} such that the continuation typechecks under K_{2} and e typechecks under K_{1}, y: (σ′, κ′) lcont. If pc′ ⋢ ζ, then we simply take e′_{i} = γ_{i}(k_{i}(e{lcont@h′[A, pc′](x:σ, y′:κ) = e′/y})). If y appears as the target of lgoto, this satisfies invariant (vi). The rest of the invariants follow from Substitution II part (ii), the definition of the operational semantics, and the fact that the memories and program counters do not change.

Otherwise, pc′ ⊑ ζ. Let lv_{i} = lcont@h′[A, pc′](x : σ, y′ : κ) = e′{k_{i}(y_{j})/y_{j}} where the y_{j} are the members of Dom(K_{2}). Note that lv_{1} ≡_{α} lv_{2}. Let K′ be K_{1}, y : (σ′, κ′) lcont and let k′_{i} = k_{i}|_{K_{1}}{y ↦ lv_{i}}. This choice of linear contexts satisfies part (iv) of the invariant.

As above, the memories don’t change, and the operational semantics justifies the choice of e′_{i} = γ_{i}(k′_{i}(e)), which is easily seen to satisfy the remaining invariants.

[O7 ] In this case, each e′′_{i} = goto v v′ lv. It must be the case that γ_{1}(v) = (cont@h′ f_{B} [A, pc′](x: σ, y : κ) = e)_{ℓ}. If ℓ ⊑ ζ, it follows that v = (cont@h′ f_{B} [A, pc′](x: σ, y : κ) = e′)_{ℓ} where e′ = γ_{1}(e) because, by invariant (iii), the continuation could not be found in γ_{1}. There are two cases, depending on whether γ_{1}(v′) has label ⊑ ζ or not. If so, then γ_{1}(v′) ≈_{ζ} γ_{2}(v′). It thus 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})). 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 possibility is that ℓ ⋢ ζ. From α-equivalence it follows that the label of γ_{2}(v) is also ⋢ ζ. Thus, we have pc_{1} = pc ⊔ ℓ ⋢ ζ and similarly, pc_{2} ⋢ ζ. This implies that the resulting configurations may use part (b) of clause (ii), and hence it does not matter what the bodies of the continuations being invoked are, as long as the other invariants are maintained. Clause (v) is easily seen to be satisfied, because the memory does not change. Similarly, clause (vi) follows by the conditions of clause (iii) of the source configurations. We build the new value substitutions as in the previous paragraph, depending on the label of γ_{1}(v′). Note that the same linear substitutions will suffice after the transition, which is evident from the Substitution Lemma II and the fact that both continuations must consume all of the linear resources.

[O8 ] Each e′′_{i} must be of the form lgoto lv v lv′. If lv is a variable, y, then the result follows easily from the fact that k_{1}(y) ≡_{α} k_{2}(y). We take K′ to be the prefix of K excluding y (which must be the last variable in the list, by typing rule [TE7 ]). Then k′_{i} = k_{i}|_{K′}, and the rest of the invariants follow similarly to the case of normal continuations discussed above.

If lv is not a variable, then by clause (vi) of the invariant, the program counter being jumped to his ⋢ ζ, and, by α-equivalence, this holds for both configurations. The rest of the invariants are seen to hold as in the case for normal continuations, but this time, K′ = K.

□

Next, we use the ordering lemma to prove that related high-security configurations stay related by a transition step. The tricky case is when the program counter becomes low.

Lemma 4.13 (High-pc Step) If Γ ∥ K ⊢ ⟨M_{1}[A_{1}, pc_{1}]@h_{1} ⊳ e_{1}⟩ ≈_{ζ} ⟨M_{2}[A_{2}, pc_{2}]@h_{2} ⊳ e_{2}⟩ and pc_{1}, pc_{2} ⋢ ζ then

⟨M_{1}[A_{1}, pc_{1}]@h_{1} ⊳ e_{1}⟩ ⟼ ⟨M′_{1}[A′_{1}, pc′_{1}]@h′_{1} ⊳ e′_{1}⟩

implies that either e_{2} diverges or

⟨M_{2}[A_{2}, pc_{2}]@h_{2} ⊳ e_{2}⟩ ⟼^{∗} ⟨M′_{2}[A′_{2}, pc′_{2}]@h′_{2} ⊳ e′_{2}⟩

and there exist Γ′ and K′ such that Γ′ ∥ K′ ⊢ ⟨M′_{1}[A′_{1}, pc′_{1}]@h′_{1} ⊳ e′_{1}⟩ ≈_{ζ} ⟨M′_{2}[A′_{2}, pc′_{2}]@h′_{2} ⊳ e′_{2}⟩

Proof: The proof is by cases on the transition step taken by the first configuration. The intention is that because pc_{1} ⋢ ζ and all of the transition rules except [O8 ] increase the label of the program counter we may choose zero steps for the second configuration and still show that ≈_{ζ} is preserved. Condition (ii) of the Noninterference Invariant will hold via part (b). It suffices to show that in all cases except for [O8 ] we simply choose Γ′ = Γ and K′ = K and show that the remainder of the invariants can still be met. This follows easily because all of the values computed, memory locations written to, and memory locations created must have labels at least as high as pc_{1} (and hence ⋢ ζ). Thus the only memory locations affected are high-security and it follows easily that M′_{1} ≈_{ζ} M_{2}. Similarly, the conditions on the letlin rule force any linear continuation introduced by e_{1} to contain a program counter annotation that is ⋢ ζ. We may thus substitute it in e_{1} without violating clause (vi) of the invariant. Thus for all cases except [O8 ] it is easy to show that Γ ∥ K ⊢ ⟨M′_{1}[A′_{1}, pc′_{1}]@h′_{1} ⊳ e′_{1}⟩ ≈_{ζ} ⟨M_{2}[A_{2}, pc_{2}]@h_{2} ⊳ e_{2}⟩ where we pick 0 steps for the second configuration.

We now consider the case for [O8 ]. Let e_{1} = γ_{1}(k_{1}(e′′_{1})) Then e′′_{1} = lgoto lv v_{1} lv_{1} for some lv. In the case that lv is not a variable, clause (vi) of the invariant ensures that the program counter in the body of lv is ⋢ ζ. We may thus use the trick above of picking 0 steps for the second configuration, and it easily follows that the resulting configurations are ≈_{ζ} under Γ and K. If lv is a variable, y, then the typing rule for lgoto guarantees that K = K′, y : κ. By assumption, k_{1}(y) = (lcont@h[A, pc](x : σ, y′ : κ′) = e). Where pc ⊑ ζ. Assume e_{2} does not diverge. Then by the Linear Continuation Ordering Lemma, we have ⟨M_{2}[A_{2}, pc_{2}]@h_{2} ⊳ e_{2}⟩ ⟼^{∗} ⟨M′_{2}[A′_{2}, pc′_{2}]@h′_{2} ⊳lgoto k_{2}(y) v_{2} lv_{2}⟩. A simple induction on the length of this derivation sequence shows that M_{2} ≈_{ζ} M′_{2} because the program counter in this sequence may not become ⊑ ζ. We thus have M′_{1} = M_{1} ≈_{ζ} M_{2} ≈_{ζ} M′_{2}. By invariant (iv) k_{2}(y) ≡_{α} k_{1}(y). Furthermore, the typing rules require that label(σ) ⋢ ζ. Thus we may take Γ′ = Γ, x : σ, γ′_{1} = γ_{1}{x ↦ γ_{1}(v_{1}) ⊔ pc_{1}}, γ′_{2} = γ_{2}{x ↦ γ_{2}(v_{2}) ⊔ pc_{2}}. We take k′_{1} and k′_{2} to be the restrictions of k_{1} and k_{2} to the domain of K′. We may then 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, and so we are done. □

Finally, we put these lemmas together and use induction to obtain the noninterference result.

Theorem 4.2 (Noninterference) Suppose x:σ ∥ y:(int_{ζ}, 1) lcont [A, pc] @h ⊢ e and label(σ) ⋢ ζ. We also assume that e is an initial program. Further suppose that • ⊢ v_{1}, v_{2} : σ. Let stop = lcont@h′[∅, ζ](x:int_{ζ}, y:1) = halt_{int_{ζ}} x. Then

⟨∅[A, pc]@h ⊳ e{v_{1}/x}{stop/y}⟩ ⟼^{∗} ⟨M_{1}[∅, ζ]@h′ ⊳ halt_{int_{ζ}} n_{ℓ_{1}}⟩
and
⟨∅[A, pc]@h ⊳ e{v_{2}/x}{stop/y}⟩ ⟼^{∗} ⟨M_{2}[∅, ζ]@h′ ⊳ halt_{int_{ζ}} m_{ℓ_{2}}⟩

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

Proof: It is easy to verify that

x:σ ∥ y:(int_{ζ}, 1) lcont ⊢ ⟨∅[A, pc]@h ⊳ e{v_{1}/x}{stop/y}⟩ ≈_{ζ} ⟨∅[A, pc]@h ⊳ e{v_{2}/x}{stop/y}⟩

by letting γ_{1} = {x ↦ v_{1}}, γ_{2} = {x ↦ v_{2}}, and k_{1} = k_{2} = {y ↦ stop}. Induction on the length of the evaluation sequence of the first expression, using the Low- and High-pc Step lemmas plus the fact that the second evaluation sequence terminates implies that it must be the case that

Γ ∥ K ⊢ ⟨M_{1}[∅, ζ]@h′ ⊳ halt_{int_{ζ}} n_{ℓ_{1}}⟩ ≈_{ζ} ⟨M_{2}[∅, ζ]@h′ ⊳ halt_{int_{ζ}} m_{ℓ_{2}}⟩

Clause (v) of the definition of the Noninterference Invariant implies that M_{1} ≈_{ζ} M_{2}. Soundness of the operational semantics implies that ℓ_{1} ⊑ ζ and ℓ_{2} ⊑ ζ. This means, because of clause (iii) neither n_{ℓ_{1}} nor m_{ℓ_{2}} are contained in the range of γ′_{i}. Thus, the integer values present in the halt expressions do not arise from substitution. Because ζ ⊑ ζ, clause (ii) then implies that halt_{int_{ζ}} n_{ℓ_{1}} ≡_{α} halt_{int_{ζ}} m_{ℓ_{2}} from which we obtain n = m as desired. □

5 Translation

This section discusses the translation rules for converting an un-located program to one which contains host annotations.

The source language is obtained from the located variant by making the additional assumption that there is a single host h, for which TP(h) = P. It is easy to verify that with this additional assumption, all of the label inequalities involving TP(h) become trivially true. To make it clear which inference rules and expressions are from the source language, we drop all occurrences of the @h marker from them.

The goal of the partitioning translation is to find suitable conditions under which it is safe to locate a particular computation or value at a host. Our approach is to specify a set of nondeterministic rewrite rules which are guaranteed to produce valid partitions of the code, and then design algorithms which apply the rewrite rules based on trade-offs between network communication overhead and the cost or availability of trusted machines. Note that for some host machine configurations there may not be a valid partitioning.

The benefit of formalizing the degree to which hosts are trusted in the programming language is that the typing rules guide the development of a sound partitioning translation. In fact, the translation rules can be generated nearly automatically from the typing rules of the target language. Here we describe how to generate an appropriate set of rewrite rules, and illustrate the process with a few examples.

Secure values translate to themselves with the exception that continuations (both linear and nonlinear) are translated by locating them on hosts suitable for the translation of their bodies.

Primitive computations must take place on a single host, thus the primitive prim may be located at a host h if all of the values mentioned in the primitive may be located there and the TP(h) is such that Γ [A, pc] @h ⊢ prim′ : σ. For example, the rule for translating primitive values is given by:

Γ ⊢ v : σ ⟹ Γ @h ⊢ v′ : σ

pc′ ⊑ label(σ)

Γ [A, pc] ⊢ v : σ

⟹ Γ [A′, pc′] @h ⊢ v′ : σ

Here, the symbol ⟹ indicates that the source judgment on the left of the arrow translates to the target judgment on the right, and we drop the @h from source judgments.

The strategy for expressions is to provide several rewrite rules corresponding to whether or not subexpressions can be located on the same host. Consider the source expression let x = prim in e. In the case that the subexpression e can be located at the same host as prim there is no need to split the computation across hosts:

Γ [A, pc] ⊢ prim : σ ⟹ Γ [A′, pc′] @h ⊢ prim : σ
Γ, x:σ ∥ K [A, pc] ⊢ e ⟹ Γ, x:σ ∥ K [A′, pc′] @h ⊢ e′

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

⟹ Γ ∥ K′ [A′, pc′] @h ⊢ let x = prim′ in e′

If e cannot be located on the same host as prim, we use a linear continuation to split the computation across hosts:

Γ [A, pc] ⊢ prim : σ ⟹ Γ [A′, pc′] @h ⊢ prim′ : σ Γ, x:σ ∥ K [A, pc] ⊢ e ⟹ Γ, x:σ ∥ K [A′′, pc′′] @h′ ⊢ e′ A′′ ⊆ A′ ⊆ TP(h) ∩ A pc ⊔ ⟨∅, TP(h)⟩ ⊑ pc′ ⊑ pc′′ ⊑ ⟨TP(h′), ∅⟩

z ∉ F V (e) y ∉ F LV (e)

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

⟹ Γ ∥ K [A′, pc′] @h ⊢ let x = prim′ in letlin k = lcont@h′[A′′, pc′′](z:1pc′, y:1) =

in lgoto k ⟨⟩pc′ ⟨⟩

The constraints on authority and program counter labels were obtained by assuming typing derivations for e′ and prim′ and then determining what extra conditions are required for the entire translated term to type-check. This rule also forces the translated term require no more authority than the source and that the target’s program counter label be at least as restrictive as the source’s.

Translation rules for all of the expressions can be created in this way, but space limitations prevent us from including all of them. See Appendix C for several more examples.

This procedure for generating the translation rules guarantees that the resulting term is welltyped. Furthermore, because no annotations on values are changed, the security properties of the source program carry over onto the target. Correctness of the translation is easy to show using a simulation argument: disregarding the host annotations on the target code and memory locations, a source program transition step corresponds to a sequence of transitions in the translated program. These observations are captured in the following theorems.

Theorem 5.1 (Translation Preserves Typing) If • ∥ • [A, pc] ⊢ e and

• ∥ • [A, pc] ⊢ e ⟹ • ∥ • [A′, pc′] @h ⊢ e′

then • ∥ • [A′, pc′] @h ⊢ e′ and A′ ⊆ A ∩ TP(h) and pc ⊔ ⟨∅, TP(h)⟩ ⊑ pc′.

Theorem 5.2 (Translation Correctness) If • ∥ • [A, pc] ⊢ e_{S} and M_{S} is a well-formed memory such that Loc(e_{S}) ⊆ Dom(M_{S}) and memory locations in Dom(M_{S}) can be assigned locations to create the well-formed memory M_{T}, and

• ∥ • [A_{S}, pc_{S}] ⊢ e_{S} ⟹ • ∥ • [A_{T} , pc_{T}] @h ⊢ e_{T}

then

⟨M_{S}[A_{S}, pc_{S}] ⊳ e_{S}⟩ ⟼ ⟨M′_{S}[A′_{S}, pc′_{S}] ⊳ e′_{S}⟩

implies that

⟨M_{T} [A_{T} , pc_{T}]@h ⊳ e_{T} ⟩ ⟼^{∗} ⟨M′_{T} [A′_{t}, pc′_{T}]@h′ ⊳ e′_{T} ⟩

and

• ∥ • [A′_{S}, pc′_{S}] ⊢ e′_{S} ⟹ • ∥ • [A′_{T} , pc′_{T}] @h′ ⊢ e′_{T}

The substitution model of evaluation presented in this paper is standard for dealing with semantics of high level programs, but allowing variables let-bound on one host to be used on another is not realistic from the implementation standpoint. Fortunately, closure conversion provides a way of making explicit the data which must be sent to a remotely located continuation. There is one twist, however, in the security setting: our type system requires that arguments to a continuation on h be acceptable for the machine h. The problem arises when a continuation located at a high-security host is syntactically nested within the body of a low-security continuation.

cont@h_{lo} f [A, pc](x:σ, y:κ) = … (cont@h_{hi} g [A′, pc′](x′:σ′, y′:κ′) = … z_{hi} …) …

If the inner, high-security piece of code (g) mentions a high-security variable(z_{hi}) from some outer context, the standard closure conversion algorithm will put z_{hi} into the closure for f, even though this is disallowed by the type system. To circumvent this problem, we intend to use a level of indirection. Rather than putting z_{hi} in f’s closure, we will put in a (read-only) reference to z_{hi}.

6 Related work

There are three primary areas of research related to the work described in this paper: enforcement of information flow policies, systems supporting mobile processes, and systems supporting mobile code security.

There has been much research on end-to-end security policies for information flow and mandatory access control in multilevel secure systems. Most practical systems for enforcing such policies have opted for dynamic enforcement using a mix of mandatory and discretionary access control. A classic example is the Orange Book [DOD85], but others [Fen73, Fen74, MR92] have also used dynamic techniques.

Static analysis of information flow also has a long history, although it has not been as widely used. Denning [Den76, DD77] originally proposed a language with static checking, but it was never implemented. Palsberg and Ørbæk developed a simple type system for checking integrity [PO95]. Volpano, Smith and Irvine showed Denning’s rules sound using standard programming language techniques [VSI96]. Heintze and Riecke [HR98] have shown that security labels can be applied to a the typed lambda calculus with reference types.Agat shows how to blind certain eliminate covert timing channels [Aga00] by translation.

Linear language constructs [Wad90, Wad93, Abr93] have been used to regulate resource consumption. Linear continuations have been introduced earlier, but in order to study their categorytheoretic semantics [Fil92]. Riely et al. have developed a notion of partial typing that allows statements to be made about type correctness in a distributed system containing malicious hosts [RH99].

Amoeba and Sprite [DOKT91] are examples of operating systems that provide transparent distribution of programs to improve performance. Our translation is driven by security needs, however, and these operating systems do not enforce end-to-end security.

Emerald [BHJL86] and Obliq [Car95] are two examples of transparently distributed programming languages. However, distribution in accordance with information flow policies is not supported. Modern distributed interface languages such as CORBA [OMG91] or Java RMI [Jav99] also do not enforce end-to-end policies. while distribution is somewhat transparent, program code executes on the host at which its object resides. This model allows enforcement of discretionary access control, but not end-to-end security policies: confidential data may easily leak to untrusted hosts through which the computation is threaded.

The focus of the work in this paper is on protecting data against untrusted hosts by moving computation away from them when necessary. A major current thread of ongoing research focuses on the different problem of protecting hosts from mobile computation. These two threads of research seem likely to be complementary. The Java bytecode verifier [LY96] is an early and much-used example of these techniques. More recent work includes Proof Carrying Code [Nec97] and Typed Assembly Language [MWCG98].

7 Conclusions

Security-typed languages are an attractive security approach because of their ability to enforce end-to-end confidentiality and integrity policies. However, previous work in this area has suffered from important limitations that prevent practical application. In this paper, we have proposed a new security-typed language, Spl@, that addresses some of these limitations.

Previous security-typed languages assume that the host executing the program is trusted. In a single-host system, this assumption is reasonable, but computation increasingly is distributed across heterogeneously trusted hosts. Computation may be run securely (to the satisfaction of all participating principals) on a partially trusted host only if certain security invariants are satisfied, as identified in this paper.

Writing programs in an explicitly distributed form is likely not to scale to more dynamic networks and larger numbers of hosts. To address this issue, this paper introduces secure program partitioning, a new approach to writing secure distributed systems. Programs are compiled to Spl@ assuming complete trust in a single executing host, and then translated into programs that contain explicit host locations for various pieces of code.

This fine-grained partitioning would not be possible in previous security-typed languages, because the programs created by translation in these languages often contain apparent (but nonexistent) information flows. Thus, these languages have an excessively restrictive type system for information flow. To address this problem, the Spl@ language introduces ordered linear continuations. The type system is designed in such a way that ordered linear continuations can only be called once and in a fixed order with respect to other linear continuations.

This work is only a first step. Spl@ is a simple calculus that needs to be more expressive. Support for object types and polymorphism, as in Jif [Mye99], would make the language more expressive. Many improvements of the rewrite rules are possible, and more investigation of partitioning heuristics is needed.

References

[ABHR99] 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, San Antonio, TX, USA, January 1999.

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

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

[BHJL86] Andrew Black, Norman Hutchinson, Eric Jul, and Henry Levy. Object structure in the Emerald system. Proceedings of the ACM Special Interest Group on Programming Languages, 21(11):78– 86, November 1986. Proc. of OOPSLA ’86, edited by Norman Meyrowitz, September 1986, Portland, Oregon.

[Car95] Luca Cardelli. A language with distributed scope. In Proc. 22th ACM Symp. on Principles of Programming Languages (POPL), pages 286–297, San Francisco, CA, January 1995.

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

[Den76] Dorothy E. Denning. A lattice model of secure information flow. Comm. of the ACM, 19(5):236– 243, 1976.

[DOD85] Department of Defense. Department of Defense Trusted Computer System Evaluation Criteria, DOD 5200.28-STD (The Orange Book) edition, December 1985.

[DOKT91] Fred Douglis, John K. Ousterhout, M. Frans Kaashoek, and Andrew S. Tanenbaum. A comparison of two distributed systems: Amoeba and sprite. ACM Transactions on Computer Systems, 4(4), Fall 1991.

[Fen73] J. S. Fenton. Information Protection Systems. PhD thesis, University of Cambridge, Cambridge, England, 1973.

[Fen74] J. S. Fenton. Memoryless subsystems. Computing J., 17(2):143–147, May 1974.

[Fil92] Andrzej Filinski. Linear continuations. In Proceedings of the 19th ACM Symposium on Principles of Programming Languages, 1992.

[FLR77] R. J. Feiertag, K. N. Levitt, and L. Robinson. Proving multilevel security of a system design. Proc. 6th ACM Symp. on Operating System Principles (SOSP), ACM Operating Systems Review, 11(5):57–66, November 1977.

[FSDF93] 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, Albuquerque, New Mexico, June 1993.

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

[GM84] J. A. Goguen and J. Meseguer. Unwinding and inference control. In Proc. IEEE Symposium on Security and Privacy, pages 75–86, April 1984.

[HR98] 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.

[Jav99] JavaSoft. Java remote method invocation. http://java.sun.com/products/jdk/rmi, 1999.

[LY96] T. Lindholm and F. Yellin. The Java Virtual Machine. Addison-Wesley, Englewood Cliffs, NJ, May 1996.

[ML97] 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.

[ML00] Andrew C. Myers and Barbara Liskov. Protecting privacy using the decentralized label model. ACM Transactions on Software Engineering and Methodology, 2000. To appear.

[MR92] M. D. McIlroy and J. A. Reeds. Multilevel security in the UNIX tradition. Software—Practice and Experience, 22(8):673–694, August 1992.

[MWCG98] 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.

[Mye99] 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.

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

[OMG91] OMG. The Common Object Request Broker: Architecture and Specification, December 1991. OMG TC Document Number 91.12.1, Revision 1.1.

[PO95] 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.

[RH99] James Riely and Matthew Hennessy. Trust and partial typing in open systems of mobile agents. In Proceedings of the 26th ACM Symposium on Principles of Programming Languages, pages 93–104, San Antonio, TX, January 1999.

[SV98] 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.

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

[Wad90] Philip Wadler. Linear types can change the world! In M. Broy and C. Jones, editors, Progarmming Concepts and Methods, Sea of Galilee, Israel, April 1990. North Holland. IFIP TC 2 Working Conference.

[Wad93] Philip Wadler. A taste of linear logic. In Mathematical Foundations of Computer Science, volume 711 of Lecture Notes in Computer Science. Springer-Verlag, August-September 1993.

[WF92] Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Technical Report TR91-160, Rice University, June 1992.

[WF94] Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38–94, 1994. Preliminary version in Rice TR 91-160.

[ZM00] Steve Zdancewic and Andrew C. Myers. Confidentiality and integrity with untrusted hosts. Submitted for publication, 2000.

A Typing rules

⊢ σ ≤ σ′

⊢ τ ≤ τ
A ⊆ A′ ℓ′ ⊑ ℓ ⊢ σ′ ≤ σ ⊢ κ′ ≤ κ

[A, ℓ](σ, κ) cont ≤ [A′, ℓ′](σ′, κ′) cont

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

\begin{matrix}⊢ σ ≤ σ′ & ⊢ σ′ ≤ σ′′ \\ ⊢ σ ≤ σ′′ \end{matrix}

⊢ κ ≤ κ′

⊢ κ ≤ κ
⊢ σ′ ≤ σ ⊢ κ′ ≤ κ

(σ, κ) lcont ≤ (σ′, κ′) lcont

\begin{matrix}⊢ κ ≤ κ′ & ⊢ κ′ ≤ κ′′ \\ ⊢ κ ≤ κ′′ \end{matrix}

K ≡ K′

(K_{1}, K_{2}), K_{3} ≡ K_{1}, (K_{2}, K_{3})  y:1 ≡ •
•, K ≡ K  K, • ≡ K

{K_{1} ≡ K_{2} \atop K_{2} ≡ K_{1}}

\begin{matrix}K_{1} ≡ K_{2} & K_{2} ≡ K_{3} \\ K_{1} ≡ K_{3} \end{matrix}

{K_{1} ≡ K′_{1} \atop K_{1}, K_{2} ≡ K′_{1}, K_{2}}

{K_{2} ≡ K′_{2} \atop K_{1}, K_{2} ≡ K_{1}, K′_{2}}

Γ ⊢ v : σ

[TV1 ]  Γ ⊢ n_{ℓ} : int_{ℓ}
[TV2 ]  Γ ⊢ ⟨⟩_{ℓ} : 1_{ℓ}

[TV3 ]

⊢ label(σ) ok @h
Γ ⊢ L_{ℓ}^{σ}@h : σ ref_{ℓ}

[TV4 ]  {Γ(x) = σ \atop Γ ⊢ x : σ}

[TV5 ]

f, x ∉ Dom(Γ)
pc ⊑ ⟨TP(h), ∅⟩
label(σ) ⊑ ⟨TP(h), ∅⟩
σ′ = [A, pc](σ, κ) cont_{ℓ}
Γ, f:σ′, x:σ ∥ y:κ [A ∪ B, pc] @h ⊢ e

Γ ⊢ (cont@h f_{B} [A, pc](x:σ, y:κ) = e)_{ℓ} : σ′

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

Γ @h ⊢ v : σ

[TV7 ]  \begin{matrix}Γ ⊢ v : τ_{ℓ} & ℓ ⊑ ⟨TP(h), ∅⟩ \\ Γ @h ⊢ v : τ_{ℓ} \end{matrix}

Γ ∥ K ⊢ lv : κ

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

[TL3 ]

x ∉ Dom(Γ), y ∉ Dom(K)
pc ⊑ ⟨TP(h), ∅⟩
label(σ) ⊑ ⟨TP(h), ∅⟩
Γ, x:σ ∥ y:κ, K [A, pc] @h ⊢ e

Γ ∥ K ⊢ lcont@h[A, pc](x:σ, y:κ) = e : (σ, κ) lcont

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

Γ [A, pc] @h ⊢ prim : σ

[TP1 ]

Γ @h ⊢ v : σ pc ⊑ label(σ)
Γ [A, pc] @h ⊢ v : σ

[TP2 ]

Γ @h ⊢ v : int_{ℓ} Γ @h ⊢ v′ : int_{ℓ′} pc ⊑ ℓ ⊔ ℓ′
Γ [A, pc] @h ⊢ v ⊕ v′ : int_{ℓ⊔ℓ′}

[TP3 ]

Γ @h ⊢ v : σ ref_{ℓ} pc ⊑ label(σ) ⊔ ℓ ⊑ ⟨TP(h), ∅⟩
Γ [A, pc] @h ⊢ deref(v) : σ ⊔ ℓ

[TP4 ]

Γ @h ⊢ v : τ_{ℓ′} B ⊆ A ℓ′ ⊓ ⟨P, B⟩ ⊑ ℓ ⊔ ⟨B, P⟩ pc ⊑ ⟨P, B⟩ pc ⊑ ℓ
Γ [A, pc] @h ⊢ declassify(v, ℓ) : τ_{ℓ}

Γ ∥ K [A, pc] @h ⊢ e

[TE1 ]

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

[TE2 ]

Γ @h ⊢ v : σ pc ⊑ ℓ ⊑ ⟨TP(h), ∅⟩ pc ⊑ label(σ) Γ, x:σ ref_{ℓ} ∥ K [A, pc] @h ⊢ e
Γ ∥ K [A, pc] @h ⊢ let x = (ref(σ) v)_{ℓ} in e

[TE3 ]

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

[TE4 ]

Γ @h ⊢ v : int_{ℓ} Γ ∥ K [A, pc ⊔ ℓ] @h ⊢ e_{i} ⟨∅, TP(h)⟩ ⊑ pc
Γ ∥ K [A, pc] @h ⊢ if0 v then e_{1} else e_{2}

[TE5 ]

Γ ∥ K_{2} ⊢ lcont@h′[A′, pc′](x′:σ′, y′:κ′) = e′ : κ′′
κ′′ = (σ, κ) lcont A′ ⊆ A pc ⊑ pc′
Γ ∥ K_{1}, y:κ′′ [A, pc] @h ⊢ e
Γ ∥ K_{1}, K_{2} [A, pc] @h ⊢ letlin y = lcont@h′[A′, pc′](x′:σ′, y′:κ′) = e′ in e

[TE6 ]

Γ @h ⊢ v : [A′, pc′](σ, κ) cont_{ℓ}
Γ @h ⊢ v′ : σ pc ⊔ ℓ ⊑ label(σ)
Γ ∥ K ⊢ lv : κ
⟨∅, TP(h)⟩ ⊑ pc pc ⊔ ℓ ⊑ pc′ A′ ⊆ A ⊆ TP(h)
Γ ∥ K [A, pc] @h ⊢ goto v v′ lv

[TE7 ]

Γ ∥ K_{2} ⊢ lv_{1} : (σ, κ) lcont
Γ @h ⊢ v : σ
Γ ∥ K_{1} ⊢ lv_{2} : κ
⟨∅, TP(h)⟩ ⊑ pc ⊑ label(σ) A ⊆ TP(h)
Γ ∥ K_{1}, K_{2} [A, pc] @h ⊢ lgoto lv_{1} v lv_{2}

[TE8 ]

B ⊆ A pc ⊓ ⟨P, B⟩ ⊑ pc′ ⊔ ⟨B, P⟩
Γ ∥ K [A, pc′] @h ⊢ e ⊢ pc′ ok @h
Γ ∥ K [A, pc] @h ⊢ setpc (pc′) in e

[TE9 ]

Γ @h ⊢ v : σ ⟨∅, TP(h)⟩ ⊑ pc ⊑ label(σ) A ⊆ TP(h)
Γ ∥ • [A, pc] @h ⊢ halt_{σ} v
[TE10 ]  \begin{matrix}Γ ∥ K [A, pc] @h ⊢ e & K ≡ K′ \\ Γ ∥ K′ [A, pc] @h ⊢ e \end{matrix}

B Operational semantics

[P1 ]

⊢ ℓ ⊔ pc ok @h
M[A, pc]@h ⊢ bv_{ℓ} ⇓ bv_{ℓ⊔pc}

[P2 ]

⊢ ℓ ⊔ ℓ′ ⊔ pc ok @h
M[A, pc]@h ⊢ n_{ℓ} ⊕ n′_{ℓ′} ⇓ (n[[⊕]]n′)_{ℓ⊔ℓ′⊔pc}

[P3 ]

M(L^{σ}) = bv_{ℓ′} ⊢ ℓ ⊔ ℓ′ ⊔ pc ok @h
M[A, pc]@h ⊢ deref(L_{ℓ}^{σ}@h′) ⇓ bv_{ℓ⊔ℓ′⊔pc}

[P4 ]

B ⊆ A ℓ′ ⊓ ⟨P, B⟩ ⊑ ℓ ⊔ ⟨B, P⟩ pc ⊑ ⟨P, B⟩ ⊢ ℓ ⊔ pc ok @h
M[A, pc]@h ⊢ declassify(bv_{ℓ′}, ℓ) ⇓ bv_{ℓ⊔pc}

[O1 ]

M[A, pc]@h ⊢ prim ⇓ v
⟨M[A, pc]@h ⊳ let x = prim in e⟩ ⟼ ⟨M[A, pc]@h ⊳ e{v/x}⟩

[O2 ]

⊢ label(σ) ok @h ℓ ⊔ pc ⊑ label(σ) L^{σ} ∉ Dom(M)

⟨M[A, pc]@h ⊳ let x = (ref(σ) bv_{ℓ})_{ℓ′} in e⟩ ⟼ ⟨M[L^{σ} ↦ bv_{ℓ⊔pc}][A, pc]@h ⊳ e{L_{ℓ′⊔pc}^{σ}@h/x}⟩ [O3 ]

ℓ ⊔ ℓ′ ⊔ pc ⊑ label(σ) L^{σ} ∈ Dom(M)
⟨M[A, pc]@h ⊳ set L_{ℓ}^{σ}@h′ := bv_{ℓ′} in e⟩ ⟼ ⟨M[L^{σ} ↦ bv_{ℓ⊔ℓ′⊔pc}][A, pc]@h ⊳ e⟩
[O4 ]  ⟨M[A, pc]@h ⊳ if0 0_{ℓ} then e_{1} else e_{2}⟩ ⟼ ⟨M[A, pc ⊔ ℓ]@h ⊳ e_{1}⟩
[O5 ] ⟨M[A, pc]@h ⊳ if0 n_{ℓ} then e_{1} else e_{2}⟩ ⟼ ⟨M[A, pc ⊔ ℓ]@h ⊳ e_{2}⟩ (n ≠ 0)
[O6 ]  ⟨M[A, pc]@h ⊳ letlin y = lv in e⟩ ⟼ ⟨M[A, pc]@h ⊳ e{lv/y}⟩

[O7 ]

A′ ∪ B ⊆ TP(h′) ⊢ pc′ ok @h′
⟨M[A, pc]@h ⊳ goto (cont@h′ f_{B} [A′, pc′](x:σ, y:κ) = e)_{ℓ} bv_{ℓ′} lv⟩
⟼
⟨M[A′ ∪ B, pc′]@h′ ⊳ e{(cont@h′ f_{B} [A′, pc′](x:σ, y:κ) = e)_{ℓ}/f}{bv_{ℓ′⊔ℓ⊔pc}/x}{lv/y}⟩

[O8 ]

A′ ⊆ TP(h′) ⊢ pc′ ok @h′
⟨M[A, pc]@h ⊳ lgoto (lcont@h′[A′, pc′](x:σ, y:κ) = e) bv_{ℓ} lv⟩
⟼
⟨M[A′, pc′]@h′ ⊳ e{bv_{ℓ⊔pc}/x}{lv/y}⟩

[O9 ]

B ⊆ A pc ⊓ ⟨P, B⟩ ⊑ pc′ ⊔ ⟨B, P⟩  ⊢ ℓ ok @h
⟨M[A, pc]@h ⊳ setpc (pc′) in e⟩ ⟼ ⟨M[A, pc′]@h ⊳ e⟩

C Example translation rules

Γ ⊢ x : σ ⟹ Γ ⊢ x : σ
Γ ⊢ ⟨⟩_{ℓ} : 1_{ℓ} ⟹ Γ ⊢ ⟨⟩_{ℓ} : 1_{ℓ}

pc′ ⊑ ⟨TP(h), ∅⟩
label(σ) ⊑ ⟨TP(h), ∅⟩
σ′ = [A, pc](σ, κ) cont_{ℓ} A′ ⊆ A

Γ, f:σ′, x:σ ∥ y:κ [A ∪ B, pc] ⊢ e ⟹ Γ, f:σ′, x:σ ∥ y:κ [A′ ∪ B, pc′] @h ⊢ e′

Γ ⊢ (cont f_{B} [A, pc](x:σ, y:κ) = e)_{ℓ} : σ′

⟹ Γ ⊢ (cont@h f_{B} [A′, pc′](x:σ, y:κ) = e′)_{ℓ} : σ′

pc′ ⊑ ⟨TP(h), ∅⟩
label(σ) ⊑ ⟨TP(h), ∅⟩

Γ, x:σ ∥ y:κ, K [A, pc] ⊢ e ⟹ Γ, x:σ ∥ y:κ, K [A′, pc′] @h ⊢ e′

Γ ∥ K ⊢ lcont[A, pc](x:σ, y:κ) = e : (σ, κ) lcont

⟹ Γ ∥ K ⊢ lcont@h[A′, pc′](x:σ, y:κ) = e′ : (σ, κ) lcont

Γ ∥ K_{2} ⊢ lv_{1} : (σ, κ) lcont ⟹ Γ ∥ K_{2} ⊢ lv′_{1} : (σ, κ) lcont Γ ⊢ v : σ ⟹ Γ @h ⊢ v′ : σ Γ ∥ K_{1} ⊢ lv_{2} : κ ⟹ Γ ∥ K_{1} ⊢ lv′_{2} : κ pc ⊔ ⟨∅, TP(h)⟩ ⊑ pc′ ⊑ label(σ) A′ ⊆ TP(h) ∩ A

Γ ∥ K_{1}, K_{2} [A, pc] ⊢ lgoto lv_{1} v lv_{2}

⟹ Γ ∥ K_{1}, K_{2} [A′, pc′] @h ⊢ lgoto lv′_{1} v′ lv′_{2}

k_{i}, y_{i} ∉ F LV (e_{i}) x_{i} ∉ F V (e_{i})

A_{i} ⊆ A′ ⊆ TP(h_{i}) ∩ A pc ⊑ pc′ ⊑ pc_{i} ⊔ ℓ ⊑ ⟨TP(h_{i}), ∅⟩

A ⊆ TP(h_{i}) pc ⊔ ℓ ⊑ ⟨TP(h_{i}), ∅⟩ Γ @h ⊢ v : int_{ℓ} Γ ∥ K [A, pc ⊔ ℓ] ⊢ e_{i} ⟹ Γ ∥ K [A_{i}, pc_{i} ⊔ ℓ] @h_{i} ⊢ e′_{i}

Γ ∥ K [A, pc] ⊢ if0 v then e_{1} else e_{2}

⟹ Γ ∥ K [A′, pc′] @h ⊢ if0 v then

letlin k_{1} = lcont@h_{1}[A_{1}, pc_{1}](x_{1} :1pc, y_{1} :1) = e′_{1} in

lgoto k_{1} ⟨⟩pc′ ⟨⟩

else

letlin k_{2} = lcont@h_{2}[A_{2}, pc_{2}](x_{2} :1pc, y_{2} :1) = e′_{2} in
lgoto k_{2} ⟨⟩pc′ ⟨⟩

(i ∈ {1, 2})