2. The Lattice Model of Information Flow

A SOUND TYPE SYSTEM FOR SECURE FLOW

ANALYSIS

Dennis Volpano

Computer Science Department Naval Postgraduate School

Monterey, California 93943, U.S.A.

Georey Smith

School of Computer Science Florida International University Miami, Florida 33199, U.S.A.

Cynthia Irvine

Computer Science Department Naval Postgraduate School

Monterey, California 93943, U.S.A.

Abstract

Ensuring secure information ow within programs in the context of multiple sensi- tivity levels has been widely studied. Especially noteworthy is Denning's work in secure ow analysis and the lattice model 6]7]. Until now, however, the soundness of Denning's analysis has not been established satisfactorily. We formulate Denning's approach as atype systemand present a notion of soundness for the system that can be viewed as a form ofnoninterference. Soundness is established by proving, with respect to a standard programming language semantics, that all well-typed programs have this noninterference property.

Keywords: type systems, program security, soundness proofs

1. Introduction

The problem of ensuring secure information ow within systems having multiple sensitivity levels has been studied extensively, beginning with the early work of Bell and LaPadula 3]. This was extended by the lattice-model work of Denning 5]6]7]

who pioneeredprogram certication, an ecient form of static analysis that could be easily incorporated into a compiler to verify secure informationow in programs.

Denning's analysis has been characterized as an extension of an axiomatic logic for program correctness by Andrews and Reitman 1]. Other more recent eorts have been aimed at extending the analysis to properly handle language features like

procedures 15]16] and nondeterminism 2], while others have focused on integrity analysis only 18]19].

So far there has not been a satisfactory treatment of the soundness of Den- ning's analysis. After all, we want to be assured that if the analysis succeeds for a given program on some inputs, then the program in some sense executes securely.

Denning provides intuitive arguments only in 7]8]. Although a more rigorous ac- count of information ow in terms of classical information theory is given in 8], no formal soundness proof is attempted. Andrews and Reitman 1] do not address the soundness of their ow logic at all. Soundness is considered in rbk 18], but the treatment depends on an \instrumented semantics" where every value is tagged with a security class. These classes are updated for values at run time according to Denning's certication conditions. A similar approach is taken by Mizuno and Schmidt 17]. However, these approaches are unsatisfactory. By modifying the se- mantics in this way, there is no longer any basis for justifying the soundness of the analysis. Proving soundness in this framework essentially amounts to proving that the analysis is consistent with the instrumented semantics. But then it is fair to ask whether class tags are updated correctly in the instrumented semantics. There is no justication for tag manipulation in the semantics.

We take a type-based approach to the analysis. The certication conditions of Denning's analysis 7]8] are formulated as a simple type system for a deterministic language. A type system is basically a formal system of type inference rules for making judgments about programs. They are usually used to establish the type correctness of programs in a strongly-typed language, for example, Standard ML 20]. However, they are not limited to reasoning about traditional forms of type correctness. They can be regarded, in general, as logical systems in which to reason about a wide variety of program properties. In our case, the property of interest is secure information ow.

Characterizing the analysis as a type system has many advantages. It serves as a formal specication that cleanly separates the security policies from the al- gorithms for enforcing them in programs. The separation also admits a notion of soundness for the analysis that resembles traditional noninterference 9]. Intu- itively, soundness states that variables in a well-typed program do not \interfere"

with variables at lower security levels. This is formalized as a type soundness theorem and proved. It is interesting to point out that the soundness proof jus- ties a more exible treatment of local variables|in some cases, there is an im- plicit ow to a local variable, but the ow is actually harmless, so it need not be rejected. The secure ow typing rules merge some traditional type correctness concerns with secure-ow enforcement. Upward information ows are easily ac- commodated through subtyping. And nally, though not addressed in this paper, the type system can be automated, using standard type inference techniques, to analyze programs for secure ows.

We begin with an overview of Denning's lattice model followed by an informal treatment of the type system. Examples are given to show how the typing rules are used. Then we turn our attention to a formal treatment of the type system and prove a soundness theorem with respect to a standard semantics for the language.

Other soundness eorts will then be discussed along with language extensions and some directions for future research.

2. The Lattice Model of Information Flow

The lattice model is an extension of the Bell and LaPadula model 3]. In this model, an information ow policy is dened by a lattice (^SC ), where SC is a nite set ofsecurity classespartially ordered by . SC may include secrecy classes, like low (L) and high (H), as well as integrity classes, like trusted (T) and untrusted (U), where^{L H} and^{T U}. There may be combinations of them as well, likeHT.

Every program variable^xhas a security class denoted by^x. It is assumed that

xcan be determined statically and that it does not vary at run time. If^xand ^y are variables and there is a ow of information from^xto^ythen it is a permissible ow i^{x y}.

Every programming construct has acertication condition. It is a purely syn- tactic condition relating security classes. Some of these conditions controlexplicit ows while others control implicit ows. For example, the statement^y :=^xhas the condition ^{x y}, that is, the ow of information from the security class of^x to that of^y must be permitted by the ow policy. This is an example of a con- dition controlling an explicit ow. The conditions for other constructs, such as

if

statements and

while

loops, control implicit ows. For example, there is always an implicit ow from the guard of a conditional to its branches. For instance, in the statement

if

^x>y

then

^z:=^w

else

ⁱ:=ⁱ+ 1

there is an implicit ow from ^x and ^y to ^z and ⁱ. So the statement has the certication condition^{xy zi}whereanddenote least upper bound and greatest lower bound operators respectively. The lattice property makes it possible to enforce these conditions using a simple attribute grammar with synthesized attributes only.

3. An Informal Treatment of the Type System

A type system consists of a set of inference rules and axioms for deriving typing judgments. A typing judgment, for our purposes, has the form

`p:

This judgment asserts that program (or program phrase)^phas type with respect to identier typing . An identier typing is a map from identiers to types it gives the types of any free identiers of^p. A judgment follows from the type system if it is the last in a sequence of judgments where each judgment in the sequence is an axiom or one that follows from preceding judgments by a type inference rule.

For example, consider a simple type system for integer-valued expressions. It might contain the following three rules: an axiom ^{` i}: int, which asserts that every integer literalⁱhas type int, an inference rule

`x: if (^x) =

giving us the type of any free identier^x, and the inference rule

`e:int

`e 0:int

`e+^e0:int

for deducing the types of expressions of the form + . In inference rules, the judgments above the horizontal line are hypotheses and the judgment below the line is theconclusion. So if(^z) =int, then

`z+ 1 :int

is a judgment that follows from the type system. We say ^z+ 1 iswell typed with respect to in this case and that it has type int. But if (^z) = bool then the judgment no longer follows from the system and we say^z+1 is not well typed with respect to.

The preceding example illustrates a traditional type system. Our secure ow type system is also composed of types and type inference rules, but now the rules enforce secure ow as opposed to data type compatibility. The rules allow secure- ow judgments to be made for expressions and commands in a block-structured, deterministic language.

3.1.

^{Secure Flow Types}

The types of our system are stratied into two levels. At one level are the data types, denoted by , which are the security classes of SC. We assume that SC is partially ordered by . At the other level are the phrase types, denoted by

. These include data types, which are the types given to expressions, variable types of the form var, and command types of the form cmd. As one would expect, a variable of type var stores information whose security class is or lower. More novelly, a command^c has type cmd only if it is guaranteed that every assignment within^cis made to a variable whose security class is or higher.

This is aconnement property, needed to ensure secure implicit ows. We extend the partial order to asubtype relation which we denote. The subtype relation is antimonotonic (or contravariant) in the types of commands, meaning that if

0then⁰cmd cmd. As usual, there is a type coercion rule that allows a phrase of typeto be assigned a type⁰whenever ⁰.

3.2.

^{Secure Flow Typing Rules}

The typing rules guarantee secure explicit and implicit ows as do certication rules in the lattice model. Consider, for example, the typing rule for assignment:

`e: var

`e 0:

`e:=^e0: cmd

This rule essentially says that in order to ensure that the explicit ow from^e0to

e is secure, ^e0 and ^e must agree on their security levels, which is conveyed by appearing in both hypotheses of the rule. Note, however, that an upward ow from

e

0 to^e is still allowed if^e:^Hvar and ^e0:^L, then with subtyping, the type of^e0 can be coerced up to^H and the rule applied with =^H.¹

1 Keep in mind that secrecy and integrity are treated uniformly in our type system 4]11], as they are in the lattice model. Examples throughout the paper will be given for secrecy only, but they could alternatively be stated for integrity.

Notice that in the preceding typing rule, the entire assignment is given type

cmd. The reason for this is to control implicit ows. Here is a simple example.

Suppose ^xis either 0 or 1 and consider

if

^x= 1

then

^y := 1

else

^y:= 0

Although there is no explicit ow from^xto^y, there is an implicit ow because^x is indirectly copied to^y. To ensure that such implicit ows are secure, we use the following typing rule for conditionals:

`e:

`c: cmd

`c

0: cmd

`

if

^e

then

^c

else

^c0: cmd

The intuition behind the rule is that ^c and ^c0 are executed in a context where information of level is implicitly known. For this reason, ^c and ^c0 may only assign to variables of level or higher. Although the rule requires the guard^eand branches ^c and ^c0 to have the same security level, namely , it does not prevent an implicit upward ow from^eto branches^cand^c0. Again subtyping can be used to establish agreement, but unlike the case with assignment statements, there are now two ways to get it. The type of ^e can be coerced to a higher level, or the types of the branches can be coerced to lower levels using the antimonotonicity of command types. In some situations both kinds of coercions are necessary. Observe that no coercions will lead to agreement if there is downward ow from ^e. The typing rule must reject the conditional in this case.

For example, suppose (^x) = (^y) = ^Hvar. By the preceding typing rule for assignment, we have ^{` y</sup> := 1 : <sup>H</sup>cmd and <sup>` y} := 0 : ^Hcmd. This means that each statement can be placed in a context where high information is implicitly known through the guard of a conditional statement. An example is

if

^x= 1

then

^y:= 1

else

^y:= 0. With = ^H, the secure ow typing rule for conditionals gives

`

if

^x= 1

then

^y:= 1

else

^y := 0 :^Hcmd

So the statement is well typed, as is expected, knowing that since^xand^yare high variables, the implicit ow from^xto^yis secure. The resulting type^Hcmd assures us that no low variable is updated in either branch (no write down). This would permit the entire statement to be used where high information again is implicitly known. Now if(^x) =^Lvar, then the implicit ow is still secure, but establishing this fact within the type system now requires subtyping. One option is to use the antimonotonic subtyping of command types where ^Hcmd ^Lcmd since ^{L H}. Each branch then is coerced from type^Hcmd to^Lcmd so that we can let =^L and get

`

if

^x= 1

then

^y:= 1

else

^y:= 0 :^Lcmd

On the other hand, we might coerce the type of ^xupward from ^L to ^H and let

=^H instead. Then once again the conditional has type^Hcmd. This would be our only choice if we had to successfully type the conditional, say, as the branch of yet another conditional whose guard is high. And nally, if (^x) = ^Hvar and

(^y) =^Lvar, then the conditional is not well typed, which is what we would expect since now the implicit ow is downward.

if

= 1

then letvar

^y:= 1

in

^c

else letvar

^y:= 0

in

^c0

Figure 1. An implicit ow from^xto ^y

3.3.

^{Local Variable} Declarations

Our core language includes a construct for declaring local variables. A local vari- able, say^x, in our language is declared as

letvar

^x:=^e

in

^c

It creates^xinitialized with the value of expression^e. The scope and lifetime of^xis command^c. The initialization can cause an implicit ow, but it is always harmless.

Consider, for instance, the program fragment in Figure 1, for some commands

cand^c0. If^xis high and each instance of^yis low, then it might appear as though the program should be rejected because there is a downward implicit ow from^x to ^y. But if ^cand ^c0 do not update any low variables, that is, each can be typed as high commands, then the program is actually secure, despite the downward ow. The contents of ^x cannot be \laundered" via ^y. To see this, suppose ^x is high. Then the rule for typing conditionals given above forces^cand^c0to be typed as high commands. By the connement property, then, neither ^c nor^c0 has any assignments to low variables and thus^y cannot be assigned to any low variables.

3.4.

^{Type Soundness}

We prove two interesting security lemmas for our type system, namely Simple Security and Connement. Simple Security applies to expressions and Connement to commands. If an expression ^e can be given type in our system, then Simple Security says, for secrecy, that only variables at level or lower in ^e will have their contents read when ^e is evaluated (no read up). For integrity, it says that every variable in^e stores information at integrity level. On the other hand, if a command^c can be given type cmd, then Connement says, for secrecy, that no variable below level is updated in^c(no write down). For integrity, it states that every variable assigned to in^c can indeed be updated by information at integrity level.

These two lemmas are used to prove the type system is sound. Soundness is formulated as a kind of noninterference property. Intuitively, it says that variables in a well-typed program do not interfere with variables at lower security levels. That is, if a variable^v has security level, then one can change the initial values of any variables whose security levels are not dominated by, execute the program, and the nal value of^vwill be the same, provided the program terminates successfully.

3.5.

^{Type Inference}

It is possible to check automatically whether a program is well typed by using standard techniques oftype inference. While a detailed discussion of type inference is beyond the scope of this paper, the basic idea is to use type variables to represent

unknown types and to collect constraints (in the form of type inequalities) that the type variables must satisfy for the program to be well typed. In this way, one can construct a principal type for the program that represents all possible types that the program can be given.

4. A Formal Treatment of the Type System

We consider a core block-structured language described below. It consists of phrases, which are either expressions ^eor commands^c:

(phrases) ^p ::= ^{e j c}

(expressions) ^e ::= ^{x j l j n j e}+^{e0 j e;e0 j e}=^{e0 j e<e0} (commands) ^c ::= ^e := ^{e0 j cc0 j}

if

^e

then

^c

else

^{c0 j}

while

^e

do

^{c j}

letvar

^x:=^e

in

^c

Metavariable ^x ranges over identiers, ^l over locations (addresses), and ⁿ over integer literals. Integers are the only values. We use 0 for false and 1 for true, and assume that locations are well ordered.

There are no I/O primitives in the language. All I/O is done through free locations in a program. That is, if a program needs to \read input" then it does so by dereferencing an explicit location in the program. Likewise, a program that needs to \write output" does so by an assignment to an explicit location. Locations may also be created during program execution due to local variable declarations.

So a partially-evaluated program may contain newly-generated locations as well as those used for I/O.

The types of the core language are stratied as follows.

(data types) ::= ^s

(phrase types) ::= ^j var ^j cmd

Metavariable^sranges over the set SC of security classes, which is assumed to be partially ordered by . Type var is the type of a variable and cmd is the type of a command.

The typing rules for the core language are given in Figure 2. We omit typing rules for some of the expressions since they are similar to rule (arith). Typing judgments have the form

^`p:

whereis alocation typing andis anidentier typing. The judgment means that phrase^phas type, assumingprescribes types for locations in^pandprescribes types for any free identiers in^p. An identier typing is a nite function mapping identiers to types (^x) is the type assigned to ^x by . Also, ^x : ] is a modied identier typing that assigns type to ^xand assigns type (^x0) to any identier^x0other than^x. A location typing is a nite function mapping locations to types. The notational conventions for location typings are similar to those for identier typings.

The remaining rules of the type system constitute the subtyping logic and are given in Figure 3. Properties of the logic are established by the following lemmas.

(^int) ^`n:

(var) ^{`x</sup>: var if(<sup>x</sup>) = var (varloc) <sup>`l}: var if(^l) =

(arith)

^`e:

^`e0:

^{`e</sup>+<sup>e0</sup>: (r-val) <sup>`e}: var

^`e: (assign)

^`e: var

^`e0:

^`e:=^e0: cmd (compose)

^`c: cmd

^`c0: cmd

^`cc0: cmd (if)

^`e:

^`c: cmd

^`c0: cmd

^`

if

^e

then

^c

else

^c0: cmd (while)

^`e:

^`c: cmd

^`

while

^e

do

^c: cmd (letvar)

^`e:

^x: var]^`c:⁰cmd

^`

letvar

^x:=^e

in

^c:⁰cmd Figure 2. Typing rules for secure information ow

Lemma 4.1

(Structural Subtyping) If ^`0, then either (^a) is of the form,⁰is of the form⁰, and ⁰, (^b) is of the form var and⁰=, or

(^c) is of the form cmd,⁰is of the form⁰cmd, and⁰ .

Proof. By induction on the height of the derivation of ^`0. If the derivation ends with rule (base) then (^a) is true by the hypothesis of the rule. If it ends with (reflex), then=⁰. So ifis of the form, then (^a) holds since is reexive.

And ifis of the form var or cmd, then (^b) or (^c) hold, respectively.

Now suppose the derivation ends with rule (trans). Then there is a⁰⁰ such that^{`00</sup> and<sup>`000}by the hypotheses of the rule. There are three cases:

1. Ifis of the form, then by induction⁰⁰ is of the form⁰⁰ and ⁰⁰. So by

(base) ⁰

` 0

(reflex) ^`

(trans) ^{`0 `000}

` 00

(cmd^;) ^{` 0}

`

0cmd cmd (^subtype)

^`p:

` 0

^`p:⁰ Figure 3. Subtyping rules

induction again,⁰ is of the form⁰and ^{00 0}. And since is transitive,

0.

2. If is of the form var, then by induction ⁰⁰ =. So by induction again,

0=⁰⁰, and hence ⁰=.

3. If is of the form cmd, then by induction ⁰⁰ is of the form ⁰⁰cmd and

00

. So by induction again,⁰is of the form⁰cmd and^{0 00}. So, since is transitive,⁰ .

Finally, suppose the derivation ends with (cmd^;). Then is of the form

cmd, ⁰ is of the form ⁰cmd, and ^{` 0} by the hypothesis of the rule.

By induction, ⁰ . ^tu

Lemma 4.2

is a partial order.

Proof. Reexivity and transitivity follow directly from rules (reflex) and (trans). Antisymmetry follows from Lemma 4.1 and the antisymmetry of . ^tu

5. The Formal Semantics

The soundness of our type system is established with respect to a natural semantics for closed phrases in the core language. We say that a phrase is closed if it has no free identiers. A closed phrase is evaluated relative to amemory , which is a nite function from locations to values. The contents of a location^{l 2}dom() is the value(^l), and we write^l :=ⁿ] for the memory that assigns value ⁿto location^l, and value(^l0) to a location^l06=^l note that^l:=ⁿ] is anupdate of if^l2dom() and an extension ofotherwise.

The evaluation rules are given in Figure 4. They allow us to derive judgments of the form ^{` e ) n</sup> for expressions and <sup>` c ) 0} for commands. These judgments assert that evaluating closed expression^ein memoryresults in integer

nand that evaluating closed command^cin memoryresults in a new memory⁰. Note that expressions cannot cause side eects and commands do not yield values.

(^base) ^`n)n

(contents) ^{`l)</sup>(<sup>l</sup>) if<sup>l2</sup>dom() (add) <sup>`e)n `e0)n0}

`e+<sup>e0)n</sup>+<sup>n0</sup> (update) <sup>`e)n l2dom</sup>()

`l:=<sup>e)l</sup>:=<sup>n</sup>] (sequence) <sup>`c)0 0`c0)00</sup>

`c^c0)00

(branch) ^{`e)</sup>1 <sup>`c)0}

`

if

^e

then

^c

else

^c0)0

`e)0 <sup>`c0)0</sup>

`

if

^e

then

^c

else

^c0)0

(loop) ^`e)0

`

while

^e

do

^c)

`e)1

`c) 0

0

`

while

^e

do

^c)00

`

while

^e

do

^c)00

(bindvar)

`e)n

lis the rst location not indom()

^l:=ⁿ]^{`l =x}]^c)0

`

letvar

^x:=^e

in

^c)0;l

Figure 4. The evaluation rules

We write ^e=x]^c to denote the capture-avoiding substitution of ^e for all free occurrences of^xin^c, and let^;lbe memorywith location^ldeleted from its do- main. Note the use of substitution in rule (^bindvar), which governs the evaluation of

letvar

^x:=^e

in

^c. A new location^lis substituted for all free occurrences of^xin

c. The result ^{l =x}]^cis then evaluated in the extended memory^l:=ⁿ], whereⁿis the value of^e. By using substitution, we avoid having to introduce an environment mapping^x to ^l. One can view ^{l =x}]^c as a partially-evaluated command, perhaps containing other free locations.

6. Type Soundness

We now establish the soundness of the type system with respect to the semantics of the core language. The soundness theorem states that if (^l) = , for some location ^l, then one can arbitrarily alter the initial value of any location ^l0 such

(r-val⁰)

^`e: var

0

^`e:⁰ (^assign0)

^`e: var

^`e0:

0

^`e:=^e0:⁰cmd (if⁰)

^`e:

^`c: cmd

^`c0: cmd

0

^`

if

^e

then

^c

else

^c0:⁰cmd (while⁰)

^`e:

^`c: cmd

0

^`

while

^e

do

^c:⁰cmd Figure 5. Syntax-directed typing rules

that (^l0) is not a subtype of, execute the program, and the nal value of ^l will be the same provided the program terminates successfully.

To facilitate the soundness proof, we introduce asyntax-directed set of typing rules. The rules of this system are just the rules of Figure 2 with rules (r-val), (assign), (if), and (while) replaced by their syntax-directed counterparts in Fig- ure 5. The subtyping rules in Figure 3 are not included in the syntax-directed system. We shall write judgments in the syntax-directed system as ^{`sp</sup> : . The benet of the syntax-directed system is that the last rule used in the deriva- tion of a typing<sup>`sp}:is uniquely determined by the form of^pand of. For example, if^pis a

while

loop, then the derivation can only end with rule (while⁰), as opposed to (while) or (subtype) in the original system. The syntax-directed rules also suggest where a type inference algorithm should introduce coercions.

Next we establish that the syntax-directed system is actually equivalent to our original system. First we need another lemma:

Lemma 6.1

If ^{`sp</sup>:and<sup>`0}, then ^`sp:⁰.

Proof. By induction on the height of the derivation of^`sp:.

If the derivation ends with^{`sn</sup>: by rule (int), then by Lemma 4.1<sup>0</sup>is of the form<sup>0</sup>, and <sup>`sn}:⁰by rule (int).

If the derivation ends with^`se: var either by rule (var) or (varloc), then⁰=by Lemma 4.1.

If the derivation ends with^{`se</sup>+<sup>e0</sup>: by rule (arith), then<sup>`se}: and^{`se0</sup>:. By Lemma 4.1,<sup>0</sup>is of the form<sup>0</sup>. So by induction,<sup>`se}:⁰

and ^s : . Thus, ^s + : by rule (arith). The cases where the derivation ends with rule (compose) or (letvar) are similar.

If the derivation ends with^`se: by rule (r-val⁰), then there is a type

00 such that^`se:⁰⁰var and⁰⁰ . By Lemma 4.1,⁰is of the form⁰and

0. Since is transitive,^{00 0}and so^`se:⁰by rule (r-val⁰).

If the derivation ends with ^{`se</sup> := <sup>e0</sup> : cmd by rule (assign<sup>0</sup>), then there is a type <sup>00</sup> such that <sup>`se} : ⁰⁰var, ^{`se0</sup> : <sup>00</sup> and <sup>00</sup>. By Lemma 4.1, <sup>0</sup> is of the form<sup>0</sup>cmd and <sup>0</sup> . Since is transitive, <sup>0 00</sup> and so <sup>`se} := ^e0 : ⁰cmd by (assign⁰). Derivations ending with (if⁰) and

(while⁰) are handled similarly. ^tu

Equivalence is now expressed by the following theorem.

Theorem 6.2

^{`p</sup>:i<sup>`sp}:.

Proof. If^{`sp</sup>:, then it is easy to see that <sup>`p}:, because each use of the syntax-directed rules (r-val⁰), (assign⁰), (if⁰), or (while⁰) can be simulated by a use of (r-val), (assign), (if), or (while), followed by a use of (subtype).

For example, a use of (assign⁰)

^`e: var

^`e0:

0

^`e:=^e0:⁰cmd

can be simulated by using (assign) to show ^{`e</sup>:=<sup>e0</sup>: cmd, using (base) and (cmd<sup>;</sup>) to show<sup>`} cmd⁰cmd, and using (subtype) to show ^`e:=

e

0:⁰cmd.

Now suppose that^{`p</sup>:. We will prove that<sup>`sp}:by induction on the height of the derivation of^`p:.

If the derivation ends with (int), (var) or (varloc), then ^`sp : is immediate, and it follows directly by induction if the derivation ends with (arith), (compose) or (letvar).

If the derivation ends with (r-val), (assign), (if), or (while), then ^`

p:follows by an application of the corresponding syntax-directed rule, using the fact that is reexive.

Finally, suppose the derivation of ^{` p</sup> : ends with (subtype). Then by the hypotheses of this rule, there is a type <sup>0</sup> such that <sup>` p} : ⁰ and

` 0

. By induction, ^{`sp</sup> : <sup>0</sup>. Thus, <sup>`sp} : by Lemma 6.1. ^tu From now on, we shall assume that all typing derivations are done in the syntax-directed type system, and therefore shall take^{`</sup>to mean <sup>`s}.

As nal preparation, we establish the following properties of the type system and semantics.

Lemma 6.3

(Simple Security) If^`e:, then for every^l in^e,(^l) .

Proof. By induction on the structure of ^e. Suppose ^{` l} : by rule (r-val⁰).

Then there is a type⁰ such that^`l :⁰var and ⁰ . Now(^l) =⁰by rule (varloc), so(^l) .

Suppose + : . Then : and : . By two uses of induction,

(^l) , for every ^l in^e, and for every ^lin^e0. So(^l) for every^l in^e+^e0. ^tu Simple security applies to both secrecy and integrity. In the case of secrecy, it says that only locations at level or lower will have their contents read when^eis evaluated (no read up). So if^{L H} and =^L, then^ecan be evaluated without reading any^H locations.

In the case of integrity, it says that if^ehas integrity level, then every location in ^e stores information at integrity level . For example, if ^{T U}, where ^T is trusted and^U untrusted, and =^T, then the lemma states that every location in

estores trusted information.

Lemma 6.4

(Con nement) If ^`c: cmd, then for every ^l assigned to in^c,

(^l) .

Proof. By induction on the structure of ^c. Suppose ^{` l</sup> := <sup>e</sup> : cmd by (assign<sup>0</sup>). Then there is a type <sup>0</sup> such that <sup>` l} : ⁰var, ^{` e} : ⁰ and

0. By rule (varloc),(^l) =⁰, so(^l) .

The lemma follows directly by induction if ^c is the composition of two com- mands or a

letvar

command.

Suppose ^`

while

^e

do

^c0: cmd by (while⁰). Then there is a type ⁰ such that ^{` e</sup> : <sup>0</sup>, <sup>` c0} : ⁰cmd and ⁰. By induction, (^l) ⁰ for every ^l assigned to in ^c0. So, since is transitive, (^l) for every ^l assigned to in ^c0 and hence for every ^l assigned to in

while

^e

do

^c0. The case

when ^c is a conditional is handled similarly. ^tu

Connement applies to both secrecy and integrity as well. In the case of secrecy, it says that no location below level is updated in^c(no write down). For integrity, it states that every location assigned to in^c can indeed be updated by information at integrity level . So, for example, if =^U, then the lemma says that no trusted location will be updated when ^cis evaluated.

The following lemma is a straightforward variant of a lemma given in 10].

Lemma 6.5

(Substitution) If^{`l</sup>: var and<sup>x</sup>: var]<sup>`c}:⁰cmd, then

^{`l =x}]^c:⁰cmd.

Lemma 6.6

If ^`c)0, thendom() =dom(⁰).

Lemma 6.7

If ^{` c ) 0}, ^{l 2} dom(), and ^l is not assigned to in ^c, then

(^l) =⁰(^l).

The preceding two lemmas can be easily shown by induction on the structure of the derivation of^`c)0. Now we are ready to prove the soundness theorem.

Theorem 6.8

(Type Soundness) Suppose (^a) ^`c:,

(^b) ^{`c)0</sup>, (<sup>c</sup>) <sup>`c) 0},

(^d) dom() =dom( ) =dom(), and (^e) (^l) =(^l) for all^lsuch that(^l) . Then ⁰(^l) =⁰(^l) for all^l such that(^l) .