Noninterference, Transitivity, and Channel-Control Security Policies^{1}

John Rushby Computer Science Laboratory SRI International Menlo Park CA 94025 USA

                       Rushby@csl.sri.com

Phone: +1 (415) 859-5456 Fax: +1 (415) 859-2844

Technical Report CSL-92-02 December 1992

1This research was supported in part by the Office of Cryptological Research (OCREAE) under contract MDA904–85–K–0001, by the Naval Research Laboratory and NASA under contract NAS1 18969 (Task 4), and by the US Government under contract MDA904-90-C-

Abstract

We consider noninterference formulations of security policies [10] in which the “interferes” relation is intransitive. Such policies provide a formal basis for several real security concerns, such as channel control [22, 23], and assured pipelines [4]. We show that the appropriate formulation of noninterference for the intransitive case is that developed by Haigh and Young for “multidomain security” (MDS) [12, 13]. We construct an “unwinding theorem” [11] for intransitive polices and show that it differs significantly from that of Haigh and Young. We argue that their theorem is incorrect. An appendix presents a mechanically-checked formal specification and verification of our unwinding theorem.

We also consider the relationship between transitive and intransitive formulations of security. We show that the standard formulations of noninterference and unwinding [10, 11] correspond exactly to our intransitive formulations, specialized to the transitive case. We show that transitive polices are precisely the “multilevel security” (MLS) polices, and that any MLS secure system satisfies the conditions of the unwinding theorem.

In addition, we consider the relationship between noninterference formulations of security and access control formulations, and we identify the “reference monitor assumptions” that play a crucial role in establishing the soundness of access control implementations.

Contents

1 Introduction 1

2 Basic Noninterference 6 2.1 Access Control Interpretations . . . . . . . . . . . . . . . . . . . . . 12

3 Noninterference and Transitivity 16 3.1 Properties of Transitive Policies . . . . . . . . . . . . . . . . . . . . . 18

4 Intransitive Noninterference 24

5 Comparisons among the Formulations 31 5.1 Intransitive vs. Standard Noninterference . . . . . . . . . . . . . . . 31 5.2 Comparison with Haigh and Young’s Formulation . . . . . . . . . . . 33

6 Summary and Conclusions 37

Bibliography 38

Appendix: Formal Verification 42

A Description of the Formal Specification and Verification 44

A.1 Lists . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 A.1.1 The Consistency of the Lists Specification . . . . . . . . . . . 45 A.1.2 List Inductions . . . . . . . . . . . . . . . . . . . . . . . . . . 46

A.2 Sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 A.3 Noninterference . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 A.4 Top . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49

B Cross-Reference Listing 50 C Proof-Chain Analysis 56

C.1 Proof-Chain for the Unwinding Theorem . . . . . . . . . . . . . . . . 56 C.2 Proof-Chain for the Mapping of the Lists Module . . . . . . . . . . . 60

D Specifications 62 lists . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62 lists model . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 lists model tcc . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 lists map . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65 lists map map . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66 lists map proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 list inductions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68 noetherian . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69 sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70 intrans nonint . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71 intrans nonint tcc . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78 intrans nonint tcc proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80 top . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81

Chapter 1

Introduction

The concept of noninterference was introduced by Goguen and Meseguer [10] in order to provide a formal foundation for the specification and analysis of security policies and the mechanisms that enforce them. Apart from the work of Feiertag, Levitt, and Robinson [9]—which can be seen as a precursor to that of Goguen and Meseguer—previous efforts, among which those of Bell and La Padula [3] were the most influential, formulated security in terms of access control. Access control formulations suffer from a number of difficulties. First, because they are described in terms of a mechanism for enforcing security, they provide no guidance in circumstances where those mechanisms prove inadequate. Second, it is easy to construct perverse interpretations of access control policies that satisfy the letter, but not the intent of the policy, to the point of being obviously unsecure [17,18]. The proponents of access control formulations counter that interpretations or implementations must be “faithful representations” of the model, but they provide no formal definition of that term.

In contrast, noninterference formulations are pure statements of policy, with no commitment to a specific mechanism for enforcing them—although techniques have been developed for demonstrating that specific mechanisms enforce given noninterference policies. Secondly, noninterference policies have the form of a logical theory; any implementation that is a model for the theory (i.e., validates its axioms) will be secure.

The idea of noninterference is really rather simple: a security domain u is noninterfering with domain v if no action performed by u can influence subsequent outputs seen by v. Noninterference has been quite successful in providing formal underpinnings for military multilevel security policies and for the methods of verifying their implementations [11, 25].

There are, however, a number of practical security problems that seem beyond the scope of noninterference formulations. One of these is “channel-control,” first formulated by Rushby [22, 23]. Channel control security policies can be represented by directed graphs, where nodes represent security domains and edges indicate the direct information flows that are allowed. The paradigmatic example of a channel-control problem is a controller for end-to-end encryption, as portrayed in Figure 1.1 [1, 22].

[figure: Bypass; Crypto; Red; Black]

Figure 1.1: End-to-end encryption controller

Plaintext messages arrive at the Red side of the controller; their bodies are sent through the encryption device (Crypto); their headers, which must remain in plaintext so that network switches can interpret them, are sent through the Bypass. Headers and encrypted bodies are reassembled in the Black side and sent out onto the network. The security policy we would like to specify here is the requirement that the only channels for information flow from Red to Black must be those through the Crypto and the Bypass.^{1} Thus, an important characteristic of many channel control policies is that the edges indicating allowed information flows are not transitive: information is allowed to flow from Red to Black via the Crypto and Bypass, but cannot do so directly.

Another example is shown in Figure 1.2, where transitive and intransitive elements are combined. The edges to the left represent the conventional transitive flow relations between the classification levels used in the USA. On the right are edges to and from a special Downgrader domain that are intransitive. The flows represented by these edges are intransitive because, although information can flow, for example, from the Top Secret to the Confidential domain via the Downgrader, it cannot flow directly from Top Secret to Confidential. Thus, information can flow “upward” in

1It is a separate problem to specify what those components must do.

Unclassified  Downgrader Confidential Secret Top Secret

Figure 1.2: Controlled downgrading

security level without restriction, but only flow “downward” through the mediation of the presumably trusted Downgrader domain.

Channel control policies such as those just described seem able to specify a number of security concerns that are beyond the reach of standard security modeling techniques. Boebert and Kain have argued persuasively [4] that a variation on channel-control called “type enforcement” can be used to solve many vexing security problems. A worthwhile challenge, then, is to find an adequate formal foundation for channel-control policies and their ilk.

An early attempt to provide a formal method for verifying, though not specifying, channel-control policies was based on a technique for verifying complete separation [22,24]. The idea was to remove the mechanisms that provided the intended channels, and then prove that the components of the resulting system were isolated. This approach has recently been shown to be subtly flawed [14], although the method for establishing complete separation has survived fairly intensive scrutiny [15, 28] with only minor emendations.

The success of noninterference formulations in explicating multilevel security policies naturally invites consideration of a noninterference foundation for channelcontrol. This presents quite a challenge, however. For example, it is clear the Red side of the encryption controller of Figure 1.1 necessarily interferes with the Black; we need to find a way of saying that this interference must only occur through the mediation of the Crypto or the Bypass. Goguen and Meseguer proposed a way of doing this in their original paper on noninterference [10], but the method was incorrect. Goguen and Meseguer recognized this in their second paper on the subject [11] and they introduced several extensions to the basic formulation of noninterference. However, the first really satisfactory treatment of intransitive noninterference policies was given by Haigh and Young [12], with a more polished version the following year [13]. They showed that it was necessary to consider the complete sequence of actions performed subsequent to a given action in order to determine whether that action is allowed to interfere with another domain. For example, an action by the Red domain is allowed to interfere with the Black domain only if there is some intervening action from either the Crypto or the Bypass.

The main purpose of this report is to show that channel-control security policies can be modeled by noninterference policies in which the “interferes” relation is intransitive and in which the definition used for “interference” is that of Haigh and Young. We also show that conventional multilevel policies are a special case of channel-control policies, corresponding to those whose “interferes” relation is transitive. We show that our results collapse to the familiar ones in this special case, thereby providing some additional evidence for their veracity.

An important component of noninterference formulations of security are the “unwinding” theorems [11, 13] that establish conditions on the behavior of individual actions sufficient to ensure security of the system. These unwinding theorems provide the basis of practical methods for formally verifying that an implementation satisfies a noninterference security policy. The main result of this report is the derivation of an unwinding theorem for the channel-control case. We show that this theorem differs significantly from that of Haigh and Young and we argue that their result is incorrect.

The development of noninterference and unwinding for the channel-control case is surprisingly intricate, and in view of the previous history of failed attempts, we present our development rather formally and describe the proofs in detail. An appendix describes the formal verification of our main theorem using the Ehdm formal specification and verification system [27].

This report is organized as follows. In the next chapter we present a development of the standard noninterference formulation of security, and then consider the relationship between noninterference security policies and access control policies. This development is structured to provide a model and a basis for comparison with the generalization given later. Chapter 3 examines the case of intransitive noninterference policies and argues that these have no useful interpretation within the standard formulation of noninterference. The second part of Chapter 3 examines the special properties of transitive policies and shows that they are identical to classical multilevel security. Chapter 4 presents a modified formulation of noninterference that does provide a meaningful interpretation to intransitive policies and derives an unwinding theorem for that interpretation. Chapter 5 compares the transitive and intransitive noninterference formulations, and compares our unwinding theorem with that of Haigh and Young. Chapter 6 presents our conclusions. The appendix presents a formal specification and verification of our Intransitive Unwinding Theorem that has been mechanically checked using the Ehdm Verification System [27].

Basic Noninterference

In this chapter we present the core of Goguen and Meseguer’s formulation of security in terms of noninterference assertions [10], and the unwinding theorem [11] that underlies the associated verification techniques. Our notation differs considerably from that of Goguen and Meseguer and is more similar to that of later authors, such as Haigh and Young [13].

We model a computer system by a conventional finite-state automaton.

Definition 1 A system (or machine) M is composed of

• a set S of states, with an initial state s_{0} ∈ S,

• a set A of actions, and

• a set O of outputs,

together with the functions step and output:

• step: S × A → S,

• output: S × A → O.

We generally use the letters … s, t, … to denote states, letters a, b, … from the front of the alphabet to denote actions, and Greek letters α, β, … to denote sequences of actions.

Actions can be thought of as “inputs,” or “commands,” or “instructions” to be performed by the machine; step(s, a) denotes the next state of the system when action a is applied in state s, while output(s, a) denotes the result returned by the action.

We derive a function run

• run: S × A^{∗} → S,

the natural extension of step to sequences of actions, by the equations

run(s, Λ) = s, and
run(s, a ∘ α) = run(step(s, a), α),

where Λ denotes the empty sequence and ∘ denotes concatenation.^{1}

In order to discuss security, we must assume some set of security “domains” and a policy that restricts the allowable flow of information among those domains. The agents or subjects of a particular security domain interact with the system by presenting it with actions, and observing the results obtained. Thus we assume

• a set D of security domains, and

• a function dom: A → D that associates a security domain with each action.

We use letters … u, v, w, … to denote domains.

A security policy is specified by a reflexive relation ⇝ on D. We use ⇝̸ to denote the complement relation, that is

⇝̸= (D × D)\ ⇝

where \ denotes set difference. We speak of ⇝ and ⇝̸ as the interference and noninterference relations, respectively. A policy is said to be transitive if its interference relation has that property. □

We wish to define security in terms of information flow, so the next step is to capture the idea of the “flow of information” formally. The key observation is that information can be said to flow from a domain u to a domain v exactly when actions submitted by domain u cause the behavior of the system perceived by domain v to be different from that perceived when those actions are not present. We therefore define a function that removes, or “purges,” from an action sequence all those actions submitted by domains that are required to be noninterfering with a given domain. The machine is secure if a given domain v is unable to distinguish between the state of the machine after it has processed a given action sequence, and the state after processing the same sequence purged of actions required to be noninterfering with v.

1Observe that we define run using right recursion: that is, we specify run(s, a ∘ α) = run(step(s, a), α), rather than the more common left recursive form run(s, α∘a) = step(run(s, α), a).

The choice of right recursion slightly complicates the proof of the basic unwinding theorem (Theorem 1); we employ it here for consistency with the later, more complex development in which its use is essential.

Definition 2 For v ∈ D and α an action sequence in A^{∗}, we define purge(α, v) to be the subsequence of α formed by deleting all actions associated with domains u such that u ⇝̸ v, that is:

purge(Λ, v) = Λ
purge(a ∘ α, v) = \{ \begin{matrix}a ∘ purge(α, v) & if dom(a) ⇝ v \\ purge(α, v) & otherwise. \end{matrix}

We identify security with the requirement that

output(run(s_{0}, α), a) = output(run(s_{0}, purge(α, dom(a))), a).

Because we frequently use expressions of the form output(run(s_{0}, α), a), it is convenient to first introduce the functions do and test to abbreviate these forms:

• do: A^{∗} → S

• test: A^{∗} × A → O

where

do(α) = run(s_{0}, α), and
test(α, a) = output(do(α), a).

Then we say a system is secure for the policy ⇝ if

test(α, a) = test(purge(α, dom(a)), a).^{2}

□

The intuition here is that the machine starts off in the initial state s_{0} and is presented with a sequence α ∈ A^{∗} of actions. This causes the machine to produce a series of outputs and to progress through a series of states, eventually reaching the state do(α). At that point the action a is performed, and the corresponding output test(α, a) is observed. We can think of presentation of the action a and observation of its output as an experiment performed by dom(a) in order to learn something about the action sequence α. If dom(a) can distinguish between the action sequences α and purge(α, dom(a)) by such experiments, then an action by some domain u ⇝̸ dom(a) has “interfered” with dom(a) and the system is not secure with respect to policies that specify u ⇝̸ dom(a).

There are several plausible variations on this notion of security. For example, rather than restricting dom(a) to observe only the individual outputs test(α, a), and test(purge(α, dom(a)), a) in its attempt to distinguish α from purge(α, dom(a)), we could allow the whole sequence of outputs produced by actions b in α satisfying dom(b) ⇝ dom(a) (i.e., the outputs of the actions in α which dom(a) can legitimately observe) to be considered. It is fairly straightforward to prove that such variations are equivalent to the definition used here.

2Formulas such as these are to be read as universally quantified over their free variables (here a and α).

The noninterference definition of security is expressed in terms of sequences of actions and state transitions; in order to obtain straightforward techniques for verifying the security of systems, we would like to derive conditions on individual state transitions. The first step in this development is to partition the states of the system into equivalence classes that all “appear identical” to a given domain. The verification technique will then be to prove that each domain’s view of the system is unaffected by the actions of domains that are required to be noninterfering with it.

Definition 3 A system M is view-partitioned if, for each domain u ∈ D, there is an equivalence relation ∼^{u} on S. These equivalence relations are said to be output consistent if

s ∼^{dom(a)} t ⊃ output(s, a) = output(t, a).^{3}

□

Output consistency is required in order to ensure that two states s and t that appear identical to domain u really are indistinguishable in terms of the outputs they produce in response to actions from u.

The definition of security requires that the outputs seen by one domain are unaffected by the actions of other domains that are required to be noninterfering with the first. The next result shows that, for an output consistent system, security is achieved if “views” are similarly unaffected.

Lemma 1 Let ⇝ be a policy and M a view-partitioned, output consistent system such that,

do(α) ∼^{u} do(purge(α, u)).

Then M is secure for ⇝.

Proof: Setting u = dom(a) in the statement of the lemma gives

do(α) ∼^{dom(a)} do(purge(α, dom(a))),

and output consistency then provides

output(do(α), a) = output(do(purge(α, dom(a))), a).

3We use ⊃ to denote implication.

But this is simply

test(α, a) = test(purge(α, dom(a)), a),

which is the definition of security for ⇝ given by Definition 2. □

Next, we define constraints on individual state transitions.

Definition 4 Let M be a view-partitioned system and ⇝ a policy. We say that M locally respects ⇝ if

dom(a) ⇝̸ u ⊃ s ∼^{u} step(s, a)

and that M is step consistent if

s ∼^{u} t ⊃ step(s, a) ∼^{u} step(t, a).

□

We now have the local conditions on individual state transitions that are sufficient to guarantee security. This result is a version of the unwinding theorem of Goguen and Meseguer [11].

Theorem 1 (Unwinding Theorem) Let ⇝ be a policy and M a view-partitioned system that is

1. output consistent,

2. step consistent, and

3. locally respects ⇝.

Then M is secure for ⇝.

Proof: We use proof by induction on the length of α to establish

s ∼^{u} t ⊃ run(s, α) ∼^{u} run(t, purge(α, u)).  (2.1)

The basis is the case α = Λ and is elementary. For the inductive step, we assume the inductive hypothesis for α of length n and consider a ∘ α. By definition,

run(s, a ∘ α) = run(step(s, a), α).  (2.2)

For run(t, purge(a ∘ α, u)), there are two cases to consider.

Case 1: dom(a) ⇝ u. In this case, the definition of purge provides

run(t, purge(a ∘ α, u)) = run(t, a ∘ purge(α, u)),

and the right hand side expands to give

run(t, purge(a ∘ α, u)) = run(step(t, a), purge(α, u)).  (2.3)

Since s ∼^{u} t and the system is step consistent, it follows that

step(s, a) ∼^{u} step(t, a)

and the inductive hypothesis then gives

run(step(s, a), α) ∼^{u} run(step(t, a), purge(α, u))

which, by virtue of (2.2) and (2.3), completes the inductive step in this case.

Case 2: dom(a) ⇝̸ u. In this case, the definition of purge provides

run(t, purge(a ∘ α, u)) = run(t, purge(α, u))  (2.4)

and the facts that dom(a) ⇝̸ u and that M locally respects ⇝ ensure

s ∼^{u} step(s, a).

Since s ∼^{u} t and ∼^{u} is an equivalence relation, the latter provides

step(s, a) ∼^{u} t

and the inductive hypothesis then gives

run(step(s, a), α) ∼^{v} run(t, purge(α, u)),

which, by virtue of (2.2) and (2.4), completes the inductive step.

In order to complete the proof, we take s = t = s_{0} in 2.1 to obtain

do(α) ∼^{u} do(purge(α, u))

and then, since M is output consistent, invoke Lemma 1 to complete the proof. □

The unwinding theorem is important because it provides a basis for practical methods for verifying systems that enforce noninterference policies, and also serves to relate noninterference policies to access control mechanisms. We illustrate the latter point by using the unwinding theorem to establish the security of a simple access control mechanism.

2.1 Access Control Interpretations

In order to consider access control mechanisms formally, we need a more elaborate system model. First of all, we need to impose some internal structure on the system state, supposing it to be composed of individual storage locations, or “objects,” each of which has a name and a value. The name of each location is fixed, but its value may change from one state to another. Access control functions determine whether a given security domain may “observe” or “alter” the values in given storage locations. We collect these ideas together and introduce convenient notation in the following definition.

Definition 5 A machine has a structured state if there exist

• a set N of names,

• a set V of values, and a function

• contents: S × N → V

with the interpretation that contents(s, n) is the value of the object named n in state s. In addition, we require functions

• observe: D → P(N), where P denotes powerset, and

• alter: D → P(N)

with the interpretation that observe(u) is the set of locations whose values can be observed by domain u, while alter(u) is the set of locations whose values can be changed by u. These functions encode the “access control matrix” that represents the access control policy of the system. An access control policy is enforced when the behavior of the system matches the intended interpretation of the observe and alter functions. This requires the following three conditions to be satisfied:

Reference Monitor Assumptions

1. First, for u ∈ D define the relation ∼^{u} on states by

s ∼^{u} t iff (∀n ∈ observe(u): contents(s, n) = contents(t, n)).

Then, in order for the output of an action a to depend only on the values of objects to which dom(a) has observe access, we require:

s ∼^{dom(a)} t ⊃ output(s, a) = output(t, a).

2. Next, when an action a transforms the system from one state to another, the new values of all changed objects must depend only on the values of objects to which dom(a) has observe access. That is:

s ∼^{dom(a)} t ∧ (contents(step(s, a), n) ≠ contents(s, n)  (2.5)

∨contents(step(t, a), n) ≠ contents(t, n))

⊃ contents(step(s, a), n) = contents(step(t, a), n).

This condition is rather difficult; we discuss it following the complete definition.

3. Finally, if an action a changes the value of object n, then dom(a) must have alter access to n:

contents(step(s, a), n) ≠ contents(s, n) ⊃ n ∈ alter(dom(a)).

These three conditions are called the “Reference Monitor Assumptions” since they capture the assumptions on the “reference monitor” that performs the access control function in any concrete instantiation of the theory. □

The second of the Reference Monitor Assumptions is somewhat tricky, so we will now explain it in more detail. The goal is to specify that if action a changes the value of location n, then the only information that may be used in creating the new value should be that provided in variables to which dom(a) has observe access. Thus, if two states s and t have the same values in all the locations to which dom(a)

has observe access (i.e., if s ∼^{dom(a)} t), then it seems we should specify

contents(step(s, a), n) = contents(step(t, a), n)  (2.6)

for all locations n. The flaw in this specification is that if dom(a) does not have

observe access to n, then s ∼^{dom(a)} t does not prevent contents(s, n) ≠ contents(t, n). If a does not change the value of location n we will then legitimately have

contents(step(s, a), n) ≠ contents(step(t, a), n).

The repair to the definition is to require (2.6) to hold only if a does change the value of location n. This is accomplished in (2.5), the second of the Reference Monitor Assumptions specified in Definition 5 above.

This problem of specifying what it means for an operation to “reference” a location has been studied before; Popek and Farber [21], for example, construct the dual notion “NoRef ” as follows. First, for n ∈ N, define the equivalence relation ≅^{n} by

s ≅^{n} t =^{def} (∀m ∈ N : contents(s, m) = contents(t, m) ∨ m = n).

That is, s ≅^{n} t if the values of all locations, except possibly that of n, are the same in both of states s and t. Then the predicate NoRef (a, n), which is to be true when action a does not reference location n, is defined by

NoRef (a, n) =^{def} s ≅^{n} t ⊃ step(s, a) ≅^{n} step(t, a).

The motivation for this definition is the idea that if a does not reference the value of location n, then changing the value of that location should have no effect on the values assigned to other locations by action a. It is easy to prove that our notion of reference, as embodied in (2.5), implies the notion embodied in Popek and Farber’s definition. The converse is not true. This is due to a weakness in Popek and Farber’s definition which they discuss in [21, page 742 (footnote 5)]; they suggest a stronger definition whose motivation is identical to that given in our discussion of the formulation of (2.5). Unfortunately, the formal statement of Popek and Farber’s stronger definition contains serious typographical errors and it is impossible to tell what was intended. Nonetheless, we consider the relationship between the description of their definition and ours to be sufficiently close that they provide additional confidence in the correctness of our formulation of the second Reference Monitor Assumption.

Given these definitions, we can now state a theorem that relates noninterference to access control mechanisms.

Theorem 2 Let M be a system with structured state that satisfies the Reference Monitor Assumptions and the following two conditions.

1. u ⇝ v ⊃ observe(u) ⊆ observe(v), and

2. n ∈ alter(u) ∧ n ∈ observe(v) ⊃ u ⇝ v.

Then M is secure for ⇝.

Proof: We show that the conditions of the theorem satisfy those of the unwinding theorem. We identify the view-partitioning relations ∼^{u} of the Unwinding Theorem with the corresponding relations defined in the statement of the Reference Monitor Assumptions. Output consistency is then satisfied immediately by the first of the Reference Monitor Assumptions.

To establish step consistency, we must prove

s ∼^{u} t ⊃ step(s, a) ∼^{u} step(t, a).

This can be rewritten as

s ∼^{u} t ⊃ contents(step(s, a), n) = contents(step(t, a), n)

Case 1: contents(step(s, a), n) ≠ contents(s, n). The third of the Reference Monitor Assumptions gives n ∈ alter(dom(a)); since n ∈ observe(u), the second of the conditions in the statement of the theorem then gives dom(a) ⇝ u. The first of the conditions in the statement of the theorem then gives

observe(dom(a)) ⊆ observe(u),

and s ∼^{u} t then implies s ∼^{dom(a)} t. The second of the Reference Monitor Assumptions then provides the conclusion we require.

Case 2: contents(step(t, a), n) ≠ contents(t, n). This case is symmetrical with the first.

Case 3: contents(step(t, a), n) = contents(t, n) ∧ contents(step(t, a), n) = contents(t, n). Since s ∼^{u} t and n ∈ observe(u), we have contents(s, n) = contents(t, n) and the conclusion follows immediately.

It remains to show that the construction locally respects ⇝. That is, we need to show

dom(a) ⇝̸ u ⊃ s ∼^{u} step(s, a).

Taking the contrapositive and expanding the definition of ∼^{u}, this becomes

(∃n ∈ observe(u): contents(s, n) ≠ contents(step(s, a), n)) ⊃ dom(a) ⇝ u.

Now if contents(s, n) ≠ contents(step(s, a), n), the third condition of the Reference Monitor Assumptions gives n ∈ alter(dom(a)). Hence, we have

n ∈ alter(dom(a)) ∧ n ∈ observe(u)

and so the second condition to the theorem requires dom(a) ⇝ u and the proof is complete. □

In the following chapter, we will show that transitive noninterference policies satisfy the conditions of Theorem 2 and thereby relate noninterference to the familiar Bell and La Padula [3] formulation of security.

Noninterference and Transitivity

The only restriction we placed on the relation ⇝ defining a security policy was that it should be reflexive. However, we will show that, within the formulation presented so far, only relations that are also transitive have a useful interpretation.

In their original paper on the subject, Goguen and Meseguer [10] suggested that intransitive policies could be used to specify channel control policies. For example, the policy of the encryption controller shown in Figure 1.1 could be specified by the four assertions

Red ⇝ Bypass
Red ⇝ Crypto
Bypass ⇝ Black
Crypto ⇝ Black

with the understanding that all other combinations, except the reflexive ones, should be noninterfering. In particular, Red ⇝̸ Black, even though Red ⇝ Bypass and Bypass ⇝ Black, so that the policy ⇝ is intransitive. This is certainly an intuitively attractive specification of the desired policy; unfortunately, it does not accurately capture the desired properties. The problem is that noninterference is a very strong property: the assertion Red ⇝̸ Black means that there must be no way for Black to observe activity by Red. This is not what is required here; Black must certainly be able to observe activity by Red (after all, it is the source of all incoming data), but we want all such observations to be mediated by the Bypass or the Crypto.

If the requirement Red ⇝̸ Black is too strong, it is obvious that the complementary requirement Red ⇝ Black is too weak: it would allow unrestricted communication from Red to Black.

We conclude that noninterference, as formulated so far, cannot specify channelcontrol policies exemplified by Figure 1.1. The question, then, is what interpretation is to be placed on intransitive policies within the current formulation? In its simplest form, we ask how we are to interpret assertions such as

A ⇝̸ C
A ⇝ B
B ⇝ C.

The hope is that this policy describes the “assured pipeline” [4] suggested by

[figure: A; B; C]

Figure 3.1: Desired interpretation of an intransitive policy

Figure 3.1. But as we have already seen, this hope is not fulfilled: the requirement A ⇝̸ C precludes all interference by domain A on domain C, including that which would use domain B as an intermediary. The only satisfactory interpretation seems to be one in which the intermediate domain B is internally composed of two isolated parts, B1 and B2 as suggested in Figure 3.2. A can interfere with the B1 part of

[figure: A; C; B1; B2]

Figure 3.2: Plausible interpretation of an intransitive policy

B (hence A ⇝ B) and the B2 part of B can interfere with C (hence B ⇝ C), but the internal dichotomy of B allows A ⇝̸ C. Under this interpretation, however, it is surely more natural to recognize B as two domains and to formulate the policy accordingly:

A ⇝̸ C
A ⇝ B1
B1 ⇝̸ B2
B2 ⇝ C

But this is (trivially) a transitive policy. We conclude that intransitive policies seem to have no useful interpretation under the present formulation of noninterference.

In the following section, we will develop a formulation of noninterference that does provide a useful interpretation to intransitive policies, and in fact it is an interpretation satisfying the original goal of using noninterference to provide a formal foundation for the specification and verification of channel-control policies. Before we proceed to an examination of intransitive policies, however, we pause to examine the properties of transitive policies.

3.1 Properties of Transitive Policies

To begin, we define the class of multilevel security policies that model the systems of clearances and classifications used in the pen-and-paper world.

Definition 6 Let L be a set of security labels (comprising “levels,” possibly augmented by “compartments”) with a partial ordering ⪯ (usually read as “is dominated by”). The interpretation of l_{1} ⪯ l_{2} is that l_{2} is more highly classified (in the case of data), or more highly trusted (in the case of individuals), and that information is permitted to flow from l_{1} to l_{2}, but not vice-versa (unless l_{1} = l_{2}).

Let clearance : D → L be a function that assigns a fixed security label to each domain in D. Then the multilevel security (MLS) policy is:

u ⇝ v iff clearance(u) ⪯ clearance(v).  (3.1)

That is, u may interfere with v if the clearance of v dominates that of u.

An arbitrary security policy given by a relation ⇝ on D is said to be an MLS-type policy if a label set L with a partial ordering ⪯ and a function clearance : D → L can be found such that (3.1) holds. □

Clearly we have:

Theorem 3 All MLS-type policies are transitive.

Proof: This follows directly from the transitivity of the partial order ⪯. □

The converse is also true. An essentially similar result (using a slightly different construction) was discovered by Dorothy Denning in 1976 [8].

Theorem 4 All transitive policies are MLS-type policies.

Proof: Let ⇝ be a transitive security policy. Define a further relation ↔ on D by:

u ↔ v =^{def} u ⇝ v ∧ v ⇝ u.

The construction ensures that ↔ is symmetric. Reflexivity and transitivity of ↔ follow from that of ⇝ (recall that all policies are reflexive). Thus ↔ is an equivalence relation. We identify a label set L with the equivalence classes of ↔ and use [u] to denote the equivalence class of domain u under ↔. We define a relation ⪯ on L as follows:

[u] ⪯ [v] =^{def} ∃ domains x ∈ [u] and y ∈ [v] such that x ⇝ y.

It is easy to see that ⪯ is a partial order on L (i.e., it is reflexive, transitive, and antisymmetric). Finally, we define the function clearance : U → L by

clearance(u) =^{def} [u].

It is then easy to verify that

u ⇝ v iff clearance(u) ⪯ clearance(v),

and so it follows that ⇝ is an MLS-type policy. □

The access control conditions of Theorem 2 reveal a familiar appearance when they are recast into the notation natural for MLS-type policies. To show this, we must first assign a classification label to each storage object by means of a function

• classification: N → D.

Then we have:

Corollary 1 (Bell and La Padula Interpretation) Let ⇝ be an MLS-type policy, and M a system with structured state that satisfies the Reference Monitor Assumptions and the following two properties.

ss-property: n ∈ observe(u) ⊃ classification(n) ⪯ clearance(u),

∗-property: n ∈ alter(u) ⊃ clearance(u) ⪯ classification(n).

Then M is secure for ⇝.

Proof: Using Theorem 2, we need to prove

u ⇝ v ⊃ observe(u) ⊆ observe(v),

and

n ∈ alter(u) ∧ n ∈ observe(v) ⊃ u ⇝ v.

The first of these can be restated as

u ⇝ v ∧ n ∈ observe(u) ⊃ n ∈ observe(v).

Using the notation of MLS-type policies and the ss-property, this becomes

clearance(u) ⪯ clearance(v) ∧ classification(n) ⪯ clearance(u)

⊃ classification(n) ⪯ clearance(v)

and is satisfied immediately by the transitivity of the partial order ⪯.

Using the notation of MLS-type policies, the second of the conditions in Theorem 2 becomes

n ∈ alter(u) ∧ n ∈ observe(v) ⊃ clearance(u) ⪯ clearance(v).

Using the ss- and ∗-properties, the antecedent to this implication becomes

clearance(u) ⪯ classification(n) ∧ classification(n) ⪯ clearance(v)

and the conclusion then follows from the transitivity of the partial order ⪯. □

The ss- and ∗-properties named in this result correspond to the “simple-security” and “star” properties of the Bell and La Padula security model [2, 3]. The simplesecurity condition asserts that a subject must only be able to observe objects whose classification is dominated by its own clearance, while the star-property asserts the dual condition that it must only be able to alter objects whose classification dominates its own clearance. Since the corollary establishes that these conditions are adequate to ensure the security of a system that enforces an MLS-type policy, it may seem puzzling that the Bell and La Padula formulation is known to have severe weaknesses [17, 18]. In fact, there are two sources for these weaknesses and it may be useful to briefly indicate what they are, and why Corollary 1 is not vulnerable to them.

• One source of weaknesses derives from the lack of a semantic characterization of what is meant by “observe” and “alter” in the Bell and La Padula model. It is possible to subvert the model by inverting the intended interpretations of these terms. (So that the simple-security property says the subjects may alter only objects of lower classification.) Corollary 1 does not share this weakness because the Reference Monitor Assumptions provide an adequate semantic characterization of the intended interpretation of observe and alter access.

• The other source of weakness concerns the behavior of actions that modify the access control functions. Our notion of a system with structured state is very limited; more realistic models include more implementation detail and also extend the set of access control functions and provide actions for manipulating them. Such actions are called “rules” by Bell and La Padula, who gave a representative set in their Multics interpretation [3]. Two of these rules are known to permit unsecure information flow [19,30]. The reason for this is that the access control “table” and other implementation-level state data of the reference monitor are not treated as objects in the Bell and La Padula model; although the model prevents unsecure information flow through the objects that it explicitly recognizes, it places no constraints on the flow of information through the mechanisms of its own realization.

Corollary 1 does not share this weakness because its system model is very limited and does permit the access control tables to change; thus, it admits no “rules.” In more complex models, that do permit modification to the access control and other internal tables, the “rules” should be individually verified by direct reference to the appropriate unwinding theorem.

The verification of individual “rules” using the unwinding theorem requires identification of the “views” of the machine state held by different security domains. The next result provides some guidance in the identification of such views, by showing that, for a transitive ⇝ relation, they are “nested” within each other. This is obvious in the Bell and La Padula model (i.e., everything observable by a subject at level l_{1} is also observable to a subject of level l_{2} where l_{1} ⪯ l_{2}). What is interesting here is that Theorem 5 shows that this nesting property is inherent, not accidental.

Definition 7 A view-partitioned machine is said to have the nesting property if

u ⇝ v ∧ s ∼^{v} t ⊃ s ∼^{u} t.

That is, if states s and t appear identical to domain v, then they also appear identical to those domains u that may interfere with v. □

Theorem 5 Let ⇝ be a transitive policy and M a view-partitioned machine which satisfies the conditions of the unwinding theorem. Then there is a nested viewpartitioning of M that also satisfies the conditions of the unwinding theorem.

Proof: Define a new view-partitioning relation ≃^{u} on D by

s ≃^{u} t =^{def} (∀v: v ⇝ u ⊃ s ∼^{v} t).

That ≃^{u} is an equivalence relation follows straightforwardly from the fact that ∼^{u} is. Output consistency and step consistency of ≃^{u} likewise follow from those properties of the ∼^{u} relation. For ≃^{u} to locally respect ⇝, we require

∀v ⇝ u : dom(a) ⇝̸ u ⊃ s ∼^{v} step(s, a).  (3.2)

The transitivity of ⇝ ensures dom(a) ⇝̸ v (since otherwise we could combine dom(a) ⇝ v with v ⇝ u and contradict dom(a) ⇝̸ u), and (3.2) then follows from the fact that ∼^{v} locally respects ⇝.

For the nesting property, we need to demonstrate x ⇝ u ⊃ s ∼^{x} t given u ⇝ v and s ≃^{v} t. Transitivity provides x ⇝ v, and the result then follows from the defini-

tion of s ≃^{v} t. □

Finally, we prove that unwinding is, in a certain sense, complete: for any secure system, we can find a view-partitioning that satisfies the conditions of the unwinding theorem. Note that this result does not depend on the transitivity of ⇝, but it does depend on the present interpretation of noninterference which, as we have seen, makes sense only for transitive policies.

Theorem 6 If M is a secure system, then for each domain u ∈ D an equivalence relation ∼^{u} on the set of states can be found that satisfies the conditions of the unwinding theorem.

Proof: We use the following construction: for u ∈ D and reachable states s and t, define

s ∼^{u} t =^{def} (∀α ∈ A^{∗}, b ∈ A : dom(b) = u
⊃ output(run(s, α), b) = output(run(t, α), b)).  (3.3)

Clearly, ∼^{u} is an equivalence relation. Output consistency follows by taking α = Λ in (3.3). For step consistency, we need

s ∼^{u} t ⊃ step(s, a) ∼^{u} step(t, a).

The conclusion to this implication expands to

output(run(step(s, a), α), b) = output(run(step(t, a), α), b)

and this is equivalent to

output(run(s, a ∘ α), b) = output(run(t, a ∘ α), b),

which follows directly from the definition of s ∼^{u} t.

To show that the construction locally respects ⇝, we need to demonstrate

dom(a) ⇝̸ u ⊃ s ∼^{u} step(s, a).

The conclusion expands to

output(run(s, α), b) = output(run(step(s, a), α), b)  (3.4)

where dom(b) = u. If s is a reachable state, there exists γ such that s = do(γ) and so (3.4) can be written as

test(γ ∘ α, b) = test(γ ∘ a ∘ α, b).

Since the machine is secure, the definition of noninterference gives

test(γ ∘ α, b) = test(purge(γ ∘ α, dom(b)), b)

3.1. Properties of Transitive Policies 23 and

test(γ ∘ a ∘ α, b) = test(purge(γ ∘ a ∘ α, dom(b)), b).

But, clearly, since dom(a) ⇝̸ u and u = dom(b),

purge(γ ∘ α, dom(b)) = purge(γ ∘ a ∘ α, dom(b))

and the result follows. □

Intransitive Noninterference

Goguen and Meseguer recognized the inability of standard noninterference to model channel-control policies and they introduced several extensions to the basic formulation in their second paper on the subject [11]. However, the first really satisfactory treatment of intransitive noninterference policies was given by Haigh and Young [13], with an earlier version the previous year [12].

Both Goguen and Meseguer, and Haigh and Young, recognized that the standard definition of noninterference is too draconian. If u ⇝̸ v, the requirement is that deleting all actions performed by u should produce no change in the behavior of the system as perceived by v. This is too strong if we also have the assertions u ⇝ w and w ⇝ v. Surely we should only delete those actions of u that are not followed by actions of w: this is the essence of Haigh and Young’s reformulation of noninterference. In order to give a formal definition, we need to identify those actions in an action sequence that should not be deleted. This is the purpose of the function sources.

Definition 8 We define the function

• sources: A^{∗} × D → P(D)

by the equations

sources(Λ, u) = {u}
sources(a ∘ α, u)^{1} = \{ \begin{matrix}sources(α, u) ∪ \{dom(a)\} & if ∃v : v ∈ sources(α, u) \\ & ∧ dom(a) ⇝ v \\ sources(α, u) & otherwise. \end{matrix}

Our function sources corresponds to the function purgeable of Haigh and Young [13], although Haigh and Young gave only an informal characterization of their function. In essence v ∈ sources(α, u) means either that v = u or that there is a subsequence of α consisting of actions performed by domains w_{1}, w_{2}, …, w_{n} such that w_{1} ⇝ w_{2} ⇝ ⋯ ⇝ w_{n}, v = w_{1}, and u = w_{n}. In considering whether an action a performed prior to the action sequence α should be allowed to influence u, we ask whether there is any v ∈ sources(α, u) such that dom(a) ⇝ v. Notice that always

1This is the definition in which right-recursion is essential.

sources(α, u) ⊆ sources(a ∘ α, u), and
u ∈ sources(α, u).

We can now define the function ipurge (for intransitive-purge):

• ipurge: A^{∗} × D → A^{∗}

by the equations

ipurge(Λ, u) = Λ
ipurge(a ∘ α, u) = \{ \begin{matrix}a ∘ ipurge(α, u) & if dom(a) ∈ sources(a ∘ α, u) \\ ipurge(α, u) & otherwise. \end{matrix}

Informally, ipurge(α, u) consists of the subsequence of α with all those actions that should not be able to interfere with u removed. Thus, security is now defined in terms of the ipurge function:

A machine is secure for the policy ⇝ if

test(α, a) = test(ipurge(α, dom(a)), a).

□

From this point on, our treatment diverges from that of Haigh and Young. We will argue later that their treatment is incorrect. The first step is to establish the revised form of Lemma 1.

Lemma 2 Let ⇝ be a policy and M a view-partitioned, output consistent system such that,

do(α) ∼^{u} do(ipurge(α, u)).

Then M is secure for ⇝.

Proof: The proof is essentially identical to that of Lemma 1.

Setting u = dom(a) in the statement of the lemma gives

do(α) ∼^{dom(a)} do(ipurge(α, dom(a))),

and output consistency then provides

output(do(α), a) = output(do(ipurge(α, dom(a))), a).

But this is simply

test(α, a) = test(ipurge(α, dom(a)), a),

which is the definition of security for ⇝ given by Definition 8. □

Next, we present a series of definitions and lemmas that culminate in the revised form of the unwinding theorem.

Definition 9 Let M be a view-partitioned system and C ⊆ D a set of domains. We define the equivalence relation ≈^{C} on the states of M as follows:

s ≈^{C} t =^{def} (∀u ∈ C : s ∼^{u} t).

Thus s ≈^{C} t exactly when the states s and t appear identical to all the members of C. □

Definition 10 Let M be a view-partitioned system and ⇝ a policy. We say that M is weakly step consistent if

s ∼^{u} t ∧ s ∼^{dom(a)} t ⊃ step(s, a) ∼^{u} step(t, a).

□

Lemma 3 Let ⇝ be a policy and M a view-partitioned system which is weakly step consistent, and locally respects ⇝. Then

s ≈^{sources(a∘α,u)} t ⊃ step(s, a) ≈^{sources(α,u)} step(t, a).

Proof: Suppose v ∈ sources(α, u). We need to show that

step(s, a) ∼^{v} step(t, a).  (4.1)

Note that v ∈ sources(α, u) implies v ∈ sources(a ∘ α, u), and so the hypothesis to the lemma provides

s ∼^{v} t.  (4.2)

We now consider two cases.

Case 1: dom(a) ⇝ v. Then, by the definition of the sources function, we have dom(a) ∈ sources(a ∘ α, u) and the hypothesis to the lemma provides

s ∼^{dom(a)} t.  (4.3)

(4.1) then follows from (4.2) and (4.3) by weak step consistency.

Case 2: dom(a) ⇝̸ v. Then by local respect for ⇝̸,

step(s, a) ∼^{v} s,
step(t, a) ∼^{v} t

and (4.1) follows from (4.2).

□

Lemma 4 Let ⇝ be a policy and M a view-partitioned system that locally respects ⇝. Then

dom(a) ∉ sources(a ∘ α, u) ⊃ s ≈^{sources(α,u)} step(s, a).

Proof: We assume the hypothesis and let v ∈ sources(α, u). It must be that dom(a) ⇝̸ v, since otherwise dom(a) ∈ sources(a ∘ α, u). Hence, by local respect for ⇝̸,

s ∼^{v} step(s, a)

and the conclusion follows. □

Lemma 5 Let ⇝ be a policy and M a view-partitioned system which is weakly step consistent, and locally respects ⇝. Then

s ≈^{sources(α,u)} t ⊃ run(s, α) ∼^{u} run(t, ipurge(α, u)).

Proof: The proof proceeds by induction on the length of α. The basis is the case α = Λ and follows straightforwardly by application of definitions. For the inductive step, we assume the result for α of length n, and consider a ∘ α. We then need to show

s ≈^{sources(a∘α,u)} t ⊃ run(s, a ∘ α) ∼^{u} run(t, ipurge(a ∘ α, u)).

We now consider two cases.

Case 1: dom(a) ∈ sources(a ∘ α, u). Then ipurge(a ∘ α, u) = a ∘ ipurge(α, u) and we need to show

s ≈^{sources(a∘α,u)} t ⊃ run(step(s, a), α) ∼^{u} run(step(t, a), ipurge(α, u)).

Lemma 3 gives

s ≈^{sources(a∘α,u)} t ⊃ step(s, a) ≈^{sources(α,u)} step(t, a)

and the result then follows from the inductive hypothesis.

Case 2: dom(a) ∉ sources(a ∘ α, u). Then ipurge(a ∘ α, u) = ipurge(α, u) and we need to show

s ≈^{sources(a∘α,u)} t ⊃ run(step(s, a), α) ∼^{u} run(t, ipurge(α, u)).

Now Lemma 4 gives

dom(a) ∉ sources(a ∘ α, u) ⊃ s ≈^{sources(α,u)} step(s, a)

and, since sources(α, u) ⊆ sources(a ∘ α, u), s ≈^{sources(a∘α,u)} t implies

s ≈^{sources(α,u)} t.

Because ≈^{sources(α,u)} is an equivalence relation, it follows that

step(s, a) ≈^{sources(α,u)} t

and the result then follows from the inductive hypothesis.

□

Finally, we can present the unwinding theorem for intransitive noninterference policies.

Theorem 7 (Unwinding Theorem for Intransitive Policies) Let ⇝ be a policy and M a view-partitioned system that is

1. is output consistent,

2. weakly step consistent, and

3. locally respects ⇝.

Then M is secure for ⇝.

Proof: Taking s = t = s_{0} in Lemma 5 gives

run(s_{0}, α) ∼^{u} run(s_{0}, ipurge(α, u)),

which can be rewritten in the form

do(α) ∼^{u} do(ipurge(α, u)),

so that the conclusion follows from Lemma 2. □ A formal verification of this theorem has been performed using the Ehdm specification and verification system and is described in in the Appendix to this report. The mechanically checked proof follows the argument of Lemmas 3 to 5 very closely.

In the following chapter, we consider the differences and similarities between this unwinding theorem and both the ordinary unwinding theorem and that of Haigh and Young. Before doing so, however, we note that the access control mechanism described in Definition 5 on page 12 of Chapter 2 works for intransitive noninterference policies as well as for transitive ones.

Theorem 8 Let M be a system with structured state that satisfies the Reference Monitor Assumptions and the condition

n ∈ alter(u) ∧ n ∈ observe(v) ⊃ u ⇝ v.

Then M is secure for ⇝.

Proof: The proof is similar to that of Theorem 2. We show that the conditions of the theorem satisfy those of the intransitive unwinding theorem. We identify the view-partitioning relations ∼^{u} of the Intransitive Unwinding Theorem with the corresponding relations defined in the statement of the Reference Monitor Assumptions. Output consistency is then satisfied immediately by the first of the Reference Monitor Assumptions.

To establish weak step consistency, we must prove

s ∼^{u} t ∧ s ∼^{dom(a)} t ⊃ step(s, a) ∼^{u} step(t, a).

This can be rewritten as

s ∼^{u} t ∧ s ∼^{dom(a)} t ⊃ contents(step(s, a), n) = contents(step(t, a), n)

Case 1: contents(step(s, a), n) ≠ contents(s, n). The second of the Reference Monitor Assumptions provides the desired conclusion directly (from the hypothesis

s ∼^{dom(a)} t).

Case 2: contents(step(t, a), n) ≠ contents(t, n). This case is symmetrical with the first.

Case 3: contents(step(t, a), n) = contents(t, n) ∧ contents(step(t, a), n) = contents(t, n). Since s ∼^{u} t, we have contents(s, n) = contents(t, n) and the conclusion is immediate.

It remains to show that the construction locally respects ⇝. This follows by exactly the same argument as that used in the proof of Theorem 2. □

It is illuminating to examine the similarity between this access control theorem and the ordinary one (Theorem 2). The only difference between the two theorems is that the ordinary one requires the additional condition

u ⇝ v ⊃ observe(u) ⊆ observe(v).

Theorem 8 is able to dispense with this condition because the intransitive unwinding theorem, from which it is derived, requires only weak step consistency.

To see how this apparently small difference in formulation allows Theorem 8, but not Theorem 2, to provide an access control interpretation for an intransitive policy, consider the system sketched in Figure 3.1. Theorem 8, allows domain A to have alter access to locations to which domain B has observe access. Similarly, it permits domain B to have alter access to locations to which domain C has observe access. In this way, information can flow from A to B and from B to C. However, A may not have alter access to any locations to which C has observe access; in this way, direct flow of information from A to C is prevented.

The conditions of Theorem 2 also allow domain A to have alter access to locations to which domain B has observe access, but they also require that B have observe access to every location to which A has observe access. Similarly, considering domains B and C, the conditions of Theorem 2 require that C have observe access to every location to which B has observe access. Transitively, therefore, C has observe access to every location to which A has observe access and so A can have “no secrets” from C. Thus, the additional condition of Theorem 2 forces the transitive completion of the policy, and so allows the direct flow of information from A to C.

Comparisons among the Formulations

In this chapter we compare our treatment of intransitive noninterference policies with the standard treatment of noninterference and with that of Haigh and Young.

5.1 Intransitive vs. Standard Noninterference

We first compare our treatment of intransitive noninterference policies (Chapter 4) with the standard treatment of noninterference policies (Chapter 2) and the special properties of transitive policies (Chapter 3). We will show that, when restricted to transitive policies, our formulation of noninterference corresponds exactly with the standard treatment. This provides some assurance that our treatment is a natural extension of the standard one. To begin, we establish that the definitions of security coincide in the case of transitive polices.

Lemma 6 If ⇝ is transitive, then

v ∈ sources(α, u) ⊃ v ⇝ u.

Proof: The proof is by induction on the length of α. The basis is the case α = Λ, and reference to Definition 8 shows that

sources(Λ, u) = {u}

and the lemma is satisfied in this case by the reflexivity of ⇝.

For the inductive step, Definition 8 gives v ∈ sources(a ∘ α, u) if either v ∈ sources(α, u) or

v = dom(a) ∧ (∃w ∈ sources(α, u) ∧ dom(a) ⇝ w).

In the first case, the inductive hypothesis provides v ⇝ u directly; in the second, the inductive hypothesis provides w ⇝ u, we also have v = dom(a) and dom(a) ⇝ w, and so transitivity provides v ⇝ u as required. □

Lemma 7 If ⇝ is transitive, then ipurge(α, u) = purge(α, u).

Proof: Comparison of Definitions 2 and 8 reveals that we only need to demonstrate

dom(a) ⇝ u iff dom(a) ∈ sources(a ∘ α, u).

The “if” direction was established by the previous lemma. For the “only if” direction, note that u ∈ sources(α, u), so that dom(a) ∈ sources(a ∘ α, u) follows immediately from Definition 8 and dom(a) ⇝ u. □

Theorem 9 Definitions 2 and 8 of security agree when the relation ⇝ is transitive.

Proof: Since the two definitions differ only in their “purge” functions, this result is an immediate consequence of the previous lemma. □

We now know that the two definitions of security coincide in the case of transitive policies; next, we show that the unwinding theorems do so as well.

Theorem 10 The Unwinding Theorems 1 and 7 agree when the relation ⇝ is transitive.

Proof: The unwinding theorems differ only in that the intransitive version uses weak step consistency where the regular one uses (ordinary) step consistency. Weak step consistency is the condition

s ∼^{u} t ∧ s ∼^{dom(a)} t ⊃ step(s, a) ∼^{u} step(t, a),

while ordinary step consistency is the condition

s ∼^{u} t ⊃ step(s, a) ∼^{u} step(t, a).

Ordinary step consistency obviously implies weak step consistency; thus, we only need to show that weak step consistency implies ordinary step consistency when ⇝ is transitive. However, it is not necessarily the case that a given view partitioning that satisfies weak step consistency also satisfies ordinary step consistency; thus we must prove that a view partitioning satisfying the intransitive unwinding theorem implies the existence of (another) view partitioning satisfying the ordinary unwinding theorem.

The construction we use is the same as that for the nesting theorem (Theorem 5): we define a new view-partitioning relation ≃^{u} on D by

s ≃^{u} t =^{def} (∀v: v ⇝ u ⊃ s ∼^{v} t).

The output consistency and local respect for ⇝ of ≃^{u} follow by the same arguments used in Theorem 5, as does the fact that ≃^{u} is an equivalence relation. For (ordinary) step consistency, we must show that

s ≃^{u} t ⊃ step(s, a) ≃^{u} step(t, a),

or, equivalently,

s ≃^{u} t ∧ v ⇝ u ⊃ step(s, a) ∼^{v} step(t, a).

Note that s ≃^{u} t ∧ v ⇝ u ⊃ s ∼^{v} t. There are now two cases to consider.

Case 1: dom(a) ⇝ u. In this case, s ≃^{u} t implies s ∼^{dom(a)} t, and since we already have s ∼^{v} t, weak step consistency then supplies step(s, a) ∼^{v} step(t, a) as required.

Case 2: dom(a) ⇝̸ u. In this case, since we have v ⇝ u, transitivity of ⇝ requires dom(a) ⇝̸ v. But then, local respect of ⇝ by ∼^{v} requires step(s, a) ∼^{v} s and step(t, a) ∼^{v} t, and so step(s, a) ∼^{v} step(t, a) follows directly from s ∼^{v} t.

□

5.2 Comparison with Haigh and Young’s Formulation

The system model used by Haigh and Young [13] differs slightly from that used here. Their output function has signature

• output: S × D → O

whereas we use

• output: S × A → O.

Thus, their output function allows a domain u to inspect the system state s directly as output(s, u), whereas ours requires the mediation of an action a with dom(a) = u to form output(s, a). Converting our formulation to theirs requires a corresponding change in the definition of the function test to signature

• test: A^{∗} × D → O with definition

test(α, u) = output(do(α), u).

The definition of security becomes

test(α, u) = test(ipurge(α, u), u),

and that of output consistency changes to

s ∼^{u} t ⊃ output(s, u) = output(t, u).

Some small changes are then needed in the proof of Lemma 2 in order to take account of the modified function signatures. No other changes are needed in the development. We have checked this by modifying the formal verification of the Appendix in the manner described above and then re-running all the proofs. The ability to readily check the effect of changed assumptions in this way is one of the great benefits of formal verification: assumptions are recorded with great precision and the “ripple” effect of perturbations can be evaluated mechanically.

Since the slight differences between the system model used here and that used by Haigh and Young have only a trivial impact on the definition of intransitive noninterference, and none at all on our intransitive unwinding theorem, it is reasonable to compare our definitions and theorems with those of Haigh and Young.

Under the proviso that our function sources is the same as their informally defined function purgeable, our definition for intransitive noninterference is the same as that given by Haigh and Young for “MDS Security.” However, the corresponding unwinding theorems differ and in this section we compare our unwinding theorem for intransitive policies with the “SAT MDS Unwinding Theorem” of Haigh and Young.

In our terminology and notation, the SAT MDS Unwinding Theorem of Haigh and Young is the following.

Proposition 1 (SAT MDS Unwinding Theorem) Let ⇝ be a policy and M a viewpartitioned system that is

1. is output consistent,

2. step consistent, and

3. MDS-respects ⇝.

Then M is secure for ⇝.

That is, Haigh and Young require step consistency where we require weak step consistency, and they require a condition we call “MDS-respect” for ⇝ where we require local respect. The condition MDS-respect is defined as follows by Haigh and Young [13, p. 147, formula (10)].

Definition 11 Let M be a view-partitioned system and ⇝ a policy. We say that M MDS-respects ⇝ if, for any choice of action a and state s, if a is purgeable with respect to domain u, then

s ∼^{u} step(s, a).

□

This definition presents a considerable challenge to interpretation. The function purgeable is not defined formally by Haigh and Young, but in its informal definition, and in all previous uses within their paper, it is used in contexts such as “a is purgeable with respect to u in α.” That is, the purgeability of an action is defined relative to a domain and an action sequence. In the definition of MDS-respects, however, there is no reference to an action sequence. Examination of Haigh and Young’s proof of their SAT MDS Unwinding Theorem sheds no light on the interpretation of the crucial notion MDS-respects: the proof is only a sketch and does not employ formal use of definitions.

Any interpretation of MDS-respects that differs from locally respects must be either weaker or stronger than that alternative notion. A stronger notion would require s ∼^{u} step(s, a) even in some circumstances where dom(a) ⇝ u. This does not seem very plausible, since the other conditions of the SAT MDS Unwinding Theorem are the same as for the ordinary unwinding theorem, and strengthening one of them must restrict, rather than enlarge, the class of policies admitted. We conclude that MDS-respects must allow s ≁^{u} step(s, a) in some circumstances where dom(a) ⇝̸ u. The constraint on the possible values of step(s, a) in this case must be provided by the other conditions of the theorem, namely output consistency, and step consistency. However, as these are both the same as in the ordinary noninterference case, it is difficult to see how adequate constraints on the effect of a state transition step(s, a) with dom(a) ⇝̸ u and s ≁^{u} step(s, a) can be achieved by these constraints.

In contrast, our formulation of the unwinding theorem for intransitive policies leaves the locally respects constraint unchanged from the ordinary case, but changes the step consistency constraint to weak step consistency. That is, the condition:

s ∼^{u} t ⊃ step(s, a) ∼^{u} step(t, a)

of the ordinary case is changed to

s ∼^{u} t ∧ s ∼^{dom(a)} t ⊃ step(s, a) ∼^{u} step(t, a)

for the intransitive case.

The second of these conditions is very natural: its intuitive interpretation is that when an action a is performed, those elements of the system state visible to u change in a way that depends only on those same elements, plus those visible to the domain that performed the action.

The ordinary step consistency condition requires that when an action a is performed, those elements of the system state visible to u change in a way that depends on those elements alone. This seems more, not less, restrictive than the previous case, until we recall that for transitive policies there is always a view-partitioning that satisfies

u ⇝ v ∧ s ∼^{v} t ⊃ s ∼^{u} t.

In other words, those elements of the state space visible to u include all the elements of the state space visible to domains that may interfere with u.

We should now ask whether a similar explanation can provide a sound interpretation to Haigh and Young’s SAT MDS Unwinding Theorem. We believe not, and we use the following example to make our case. Consider a system with four domains U, V, W, and X; U and V may interfere with W, and W may interfere with X, but U and V must not directly interfere with X. The system state is composed of three internal registers, u, v, and x, all initially zero. Each domain has a single action associated with it: U’s action sets the register u to 1, V ’s action sets the register v to 2, W ’s action sets the register x to the sum of the contents of u and v, and X’s action outputs the contents of the register x. It should be clear that this system satisfies the stated policy. We need to be able to distinguish it from the insecure variant in which X’s action outputs the sum of the registers u and v directly. In our formulation of intransitive noninterference, U, V and X’s view of the system state is restricted to the registers u, v and x respectively, while W can view both registers u and v. It is easy to see that our unwinding theorem for intransitive policies is satisfied by this assignment.

Haigh and Young’s unwinding theorem is not satisfied, however, since the effect of W ’s action on the register x cannot be explained in terms of the objects visible to X. It seems that the set of objects visible to X must be enlarged to include the registers u and v. But how, then, are we to distinguish the system from its unsecure variant?

We conclude that all possible interpretations of Haigh and Young’s SAT MDS Unwinding Theorem are unsatisfactory. Because there is no precise definition of the crucial requirement that we call “MDS-respects,” it is impossible to assign a definitive status to the theorem, and its utility becomes questionable.

We have, we believe, presented adequate evidence that our unwinding theorem for intransitive policies is both true and useful; indeed, we believe it is the strongest theorem possible. We have also presented evidence that Haigh and Young’s theorem is essentially different than ours—differing in the crucial step consistency condition, not just the uncertain MDS-respects condition. We therefore believe it unlikely that their theorem, if true, is as generally applicable as ours. Consequently, we consider it likely that their theorem is either false, or true but applicable to a very small class of systems and/or policies.

Summary and Conclusions

We have examined the issue of transitivity in noninterference security policies. Intransitive noninterference policies would seem, intuitively, to be exactly what is required for the formal specification of channel control and type enforcement policies. We have shown, however, that the standard interpretation of noninterference does not fulfill this expectation. Fortunately, the interpretation of noninterference introduced by Haigh and Young for multidomain security (MDS) does have the properties we require. Our contribution has been the identification of intransitivity of the ⇝ relation as the key distinction between channel control, type enforcement, and MDS policies on the one hand, and MLS policies on the other.

It can be considered a historical accident that the theory for the transitive case was invented and developed before the intransitive one, and has therefore become regarded as the standard case. We submit that it is now more helpful to regard the intransitive case as the basis for noninterference formulations of security, with the formerly standard treatment regarded as a specialization for the case of transitive policies. The advantage of regarding the development in this light is that one does not have to trouble with the rather difficult and informal argument that the standard treatment makes little sense for intransitive policies; one can simply present the general theory and then show that there is a simpler treatment available in the special case of transitive policies. The attempt to use the standard treatment in the case of intransitive policies simply does not arise with this approach.

Our main technical contributions have been the formulation, rigorous proof, and mechanically-checked formal verification of an unwinding theorem for intransitive polices, a demonstration that the definitions and theorems of the intransitive theory collapse to the standard ones in the case of transitive policies, and an exploration of the properties of transitive policies. Our demonstrations of the equivalence of MLS and transitive noninterference policies, of the nesting property, and of the result that all MLS secure systems satisfy the conditions of the unwinding theorem, shed some new light on the properties of transitive noninterference security policies.

However, the novel and more interesting case, and the one that prompted this investigation in the first place, is that of intransitive noninterference policies. In future work we hope to explore the practical application of intransitive noninterference formulations to problems of channel control, and to develop effective methods for verifying mechanisms that enforce such policies. We also plan to explore the connection between intransitive noninterference policies and the class of properties, discussed in [26], that can be enforced by kernelization.

Bibliography

[1] D. H. Barnes. The provision of security for user data on packet switched networks. In Proceedings of the Symposium on Security and Privacy, pages 121– 126, Oakland, CA, April 1983. IEEE Computer Society.

[2] D. E. Bell and L. J. La Padula. Secure computer systems: Vol. I—mathematical foundations, Vol. II—a mathematical model, Vol. III—a refinement of the mathematical model. Technical Report MTR-2547 (three volumes), Mitre Corporation, Bedford, MA, March–December 1973.

[3] D. E. Bell and L. J. La Padula. Secure computer system: Unified exposition and Multics interpretation. Technical Report ESD-TR-75-306, Mitre Corporation, Bedford, MA, March 1976.

[4] W. E. Boebert and R. Y. Kain. A practical alternative to hierarchical integrity policies. In Proceedings 8th DoD/NBS Computer Security Initiative Conference, pages 18–27, Gaithersburg, MD, September 1985.

[5] Ehdm Specification and Verification System Version 4.1—User’s Guide. Computer Science Laboratory, SRI International, Menlo Park, CA, November 1988. See [7] for the updates to Version 5.2.

[6] Ehdm Specification and Verification System Version 5.0—Description of the Ehdm Specification Language. Computer Science Laboratory, SRI International, Menlo Park, CA, January 1990. See [7] for the updates to Version 5.2.

[7] Ehdm Specification and Verification System Version 5.X—Supplement to User’s and Language Manuals. Computer Science Laboratory, SRI International, Menlo Park, CA, August 1991. Current version number is 5.2.

[8] D. E. Denning. On the derivation of lattice structured information flow policies. Technical Report CSD TR 180, Purdue University, March 1976.

[9] R. J. Feiertag, K. N. Levitt, and L. Robinson. Proving multilevel security of a system design. In 6th ACM Symposium on Operating System Principles, pages 57–65, November 1977.

[10] J. A. Goguen and J. Meseguer. Security policies and security models. In Proceedings of the Symposium on Security and Privacy, pages 11–20, Oakland, CA, April 1982. IEEE Computer Society.

[11] J. A. Goguen and J. Meseguer. Inference control and unwinding. In Proceedings of the Symposium on Security and Privacy, pages 75–86, Oakland, CA, April 1984. IEEE Computer Society.

[12] J. Haigh and W. Young. Extending the non-interference model of MLS for SAT. In Proceedings of the Symposium on Security and Privacy, pages 232– 239, Oakland, CA, April 1986. IEEE Computer Society.

[13] J. Thomas Haigh and William D. Young. Extending the noninterference version of MLS for SAT. IEEE Transactions on Software Engineering, SE-13(2):141– 150, February 1987.

[14] Jeremy Jacob. A note on the use of separability for the detection of covert channels. Cipher (Newsletter of the IEEE Technical Committee on Security and Privacy), pages 25–33, Summer 1989.

[15] Nancy L. Kelem and Richard J. Feiertag. A separation model for virtual machine monitors. In Proceedings of the Symposium on Research in Security and Privacy, pages 78–86, Oakland, CA, May 1991. IEEE Computer Society.

[16] Zohar Manna and Richard Waldinger. The Logical Basis for Computer Programming, volume 2: Deductive Systems. Addison-Wesley, 1990.

[17] John McLean. A comment on the “basic security theorem” of Bell and La Padula. Information Processing Letters, 20:67–70, 1985.

[18] John McLean. Reasoning about security models. In Proceedings of the Symposium on Security and Privacy, pages 123–131, Oakland, CA, April 1987. IEEE Computer Society.

[19] J. K. Millen and C. M. Cerniglia. Computer security models. Working Paper WP25068, Mitre Corporation, Bedford, MA, September 1983.

[20] S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In Deepak Kapur, editor, 11th International Conference on Automated Deduction (CADE), pages 748–752, Saratoga, NY, 1992. Springer Verlag, volume 607 of Lecture Notes in Artificial Intelligence.

[21] Gerald J. Popek and David R. Farber. A model for verification of data security in operating systems. Communications of the ACM, 21(9):737–749, September [22] John Rushby. The design and verification of secure systems. In 8th ACM Sym-

posium on Operating System Principles, pages 12–21, Asilomar, CA, December 1981. (ACM Operating Systems Review, Vol. 15, No. 5).

[23] John Rushby. Verification of secure systems. Technical Report 166, Computing Laboratory, University of Newcastle upon Tyne, Newcastle upon Tyne, UK, August 1981.

[24] John Rushby. Proof of Separability—a verification technique for a class of security kernels. In Proc. 5th International Symposium on Programming, pages 352–367, Turin, Italy, April 1982. Springer Verlag, volume 137 of Lecture Notes in Computer Science.

[25] John Rushby. The security model of Enhanced HDM. In Proceedings 7th DoD/NBS Computer Security Initiative Conference, pages 120–136, Gaithersburg, MD, September 1984.

[26] John Rushby. Kernels for safety? In T. Anderson, editor, Safe and Secure Computing Systems, chapter 13, pages 210–220. Blackwell Scientific Publications, 1989. (Proceedings of a Symposium held in Glasgow, October 1986).

[27] John Rushby, Friedrich von Henke, and Sam Owre. An introduction to formal specification and verification using Ehdm. Technical Report SRI-CSL-91-2, Computer Science Laboratory, SRI International, Menlo Park, CA, February 1991.

[28] C. T. Sennett and R. Macdonald. Separability and security models. Technical Report 87020, Royal Signals and Radar Establishment, Malvern, UK, November 1987.

[29] Joseph R. Shoenfield. Mathematical Logic. Addison-Wesley, Reading, MA, 1967.

[30] T. Taylor. Comparison paper between the Bell and La Padula model and the SRI model. In Proceedings of the Symposium on Security and Privacy, pages 195–202, Oakland, CA, April 1984. IEEE Computer Society.

[31] F. W. von Henke, J. S. Crow, R. Lee, J. M. Rushby, and R. A. Whitehurst. The Ehdm verification environment: An overview. In Proceedings 11th National Computer Security Conference, pages 147–155, Baltimore, MD, October 1988. NBS/NCSC.

Appendix: Formal Verification

Formulation of noninterference and derivation of the corresponding unwinding theorem is surprisingly intricate for the case of intransitive security policies. We have shown that our treatment differs somewhat from that of Haigh and Young, and have argued that their unwinding theorem is incorrect. Because of its intricacy, we presented our development in detail and described the proofs fully in the main body of this report. We also presented collateral evidence for the correctness of our results, by showing that they collapse to the familiar ones in the case of transitive policies. In this Appendix, we present additional evidence for the correctness of our development in the form of a mechanically checked proof for the intransitive unwinding theorem.^{1} The proof was performed using the Ehdm formal specification and verification system developed by the Computer Science Laboratory of SRI [5,6,27,31].^{2}

Although we do not claim that verification in Ehdm is a certification of “correctness,” the successful outcome of the formal verification increases our confidence that the theorem is correct. This confidence derives from the greater understanding that a truly formal development requires as much as it does from mechanized checking of the proofs.

A secondary benefit of formal verification in Ehdm is the enumeration, by its “Proof Chain Checker,” of all the definitions and axioms on which a proof depends. In this way, we are able to identify the logical foundation of a verification; those definitions and axioms comprising the foundation can then be subjected to careful scrutiny and peer review. The logical foundation of the Intransitive Unwinding Theorem is listed in Section C.1 and can be seen to comprise 14 definitions needed to develop the noninterference model, plus one definition and six axioms required for the supporting theories such as lists and sets.

Another benefit of a formal verification is that it can assist in the exploration of alternative formulations and specifications. For example, we noted in Chapter 5.2 that our basic system model differs slightly from that of Haigh and Young [13]. When this was drawn to our attention, we were able to incorporate the changes in our formal specification and explore its consequences very quickly. In this case, we found that the proof to one theorem needed slight adjustment, but everything else could be left unchanged. In our experience, manual checking of the consequences of revised definitions and axioms is very error-prone, since proofs are seldom checked for the second time (to see if they need adjusting) with the same care that they are constructed in the first place. In contrast, a verification system explores the “ripple” effect of changes with mechanical precision and speed.

1We have also developed a mechanically-checked formal verification of the unwinding theorem for classical (i.e., transitive) noninterference. This verification, which is much simpler than the one described here, is available from the author on request.

2This formal specification and verification was performed in early 1991 using the then-current Version 5.2 of Ehdm. The now-current Version 6.1 of Ehdm is a completely new implementation that differs in some significant details from 5.2.

We consider that the benefits of the formal specification and verification of the intransitive noninterference model and its unwinding theorem amply repay the modest cost required. It really does not take much longer to develop a fully formal, mechanically checked specification in Ehdm than it does to construct a comparably detailed model in conventional mathematical notation. Simple parsing and typechecking of the specification is sufficient to identify mismatches between the definition and use of terms, such as those in Haigh and Young’s MDS Unwinding Theorem [13]. Furthermore, in an expressive specification language such as that of Ehdm, the specifications are perfectly readable and compare well with those developed in conventional, informal, mathematical notation. The additional discipline of a formal specification also encourages simplicity and consistency of notation and presentation.

Appendix A

Description of the Formal Specification and Verification

The formal verification described here was performed using the Ehdm system; as we do not describe Ehdm in any detail here, readers unfamiliar with its specification language and verification environment are referred to [27]. The formal specification and verification follows closely the conventional mathematical presentation in Chapter 4, using the same notation and names wherever possible.

The formal specification and verification in Ehdm is shown in full in Appendix D, and a cross-reference in Appendix B. Notice that Ehdm proof declarations appear as part the specification: they provide a list of premises and ground substitutions for variables, and constitute the only information provided to the theorem prover. A “proof-chain” analysis of the verification appears in Appendix C. This analysis checks that the premises to each theorem are either axioms or proved theorems. Type-correctness of certain Ehdm constructions (for example, recursive function definitions) requires that certain system-generated formulas called Type Consistency Conditions (TCCs) are proved; in addition, some modules (such as those defining induction) declare assumptions that must be proved in any instantiation of the module. The proof-chain analyzer checks that both these kinds of proof obligations are discharged.

The generation of all the tables in the appendices was performed automatically by Ehdm. In addition, the specifications that appear in Appendix D were prettyprinted into conventional mathematical notation using the Ehdm LaTEXtranslator [7, 27].

A.1 Lists

Inspection of the development in Chapter 4 shows that several functions range over sequences, but that recursions and inductions over these sequences always occur right-recursively. Thus we do not require a general theory of sequences, only a theory of sequences constructed right-recursively; such a theory is the theory of lists with constructor cons (which we generally write as infix ∘), base element nil (which we generally write as Λ), and selectors car and cdr.^{1} A length function is also defined on lists.

This theory is presented in the module lists shown on page 62. Observe that the module is parameterized by the type over which the lists are constructed. It is worth noting that a rather large number of axioms (six) are required in this module. Axioms must always be scrutinized with great care since they can introduce inconsistencies. In fact, the module lists can be systematically generated from a simple definitional facility for abstract data types (this is done automatically in PVS [20], our other verification system) and the soundness of the construction can be proved once and for all. For illustrative purposes, however, we specifically demonstrate the consistency of the lists theory by exhibiting a model. In Ehdm, this is done via theory interpretation [29, Section 4.7] using the MAPPING mechanism [27]. The construction of such an interpretation is described in the following section.

A.1.1 The Consistency of the Lists Specification

The topic discussed in this section is somewhat technical and may be skipped without loss to the main theme.

We demonstrate the consistency of the lists module, and also confirm our understanding of what it specifies, by mapping it to a constructively defined module called lists model shown on page 63. The latter module interprets lists as records consisting of a natural number (intuitively, this can be regarded as a pointer) and an array. The list is “stored” in consecutive locations of the array, starting at 0. The pointer points one location past the end of the list. The cons function simply stores a new element in the array and advances the pointer; conversely, cdr simply reduces the pointer. The car function returns the value of the location in the list immediately prior to the pointer. Arrays and records in Ehdm are simply functions; “storing” a value in an array or record is performed using function modification, indicated by the with keyword: f with [(x) := y] is the function that has the same value everywhere as f, except that it has the value y at x.

1Although adequate for our purposes, this really is a very limited theory of lists; in fact, it is rather closer to a theory of stacks.

The specification of these functions in the module lists model shown on page 63 is straightforward.^{2} The module lists model generates a TCC module shown on page 64; an adequate proof of its single TCC formula is given in the module top shown on page 81.

It is also necessary to define a concrete-equality predicate on the lists representation type; this predicate must be true when two representations both represent the same abstract list. This will be so if their pointers are the same and the contents of their arrays are equal at all locations between 0 and one less than the pointer. The predicate is specified as ce in the module lists model. It is a matter of pragmatic convenience that ce and cons are specified by ordinary definitions (using a single =), while the other functions are specified by literal definitions (using double ==): the literally-defined functions will be expanded automatically in proofs, whereas the more complex ce and cons must be cited explicitly.

The mapping module that links lists to lists model is the module lists map shown on page 65. This module explicitly indicates that equality on lists is to be mapped to the ce predicate in the interpretation; all other types and constants are to be mapped using name-identity. The system-generated mapped module lists map map is shown on page 66. The axioms of lists, interpreted in the theory of lists model as indicated by lists map, become formulas to be proven in lists map map. Notice that we are required to prove that ce is an equivalence relation. We should also be required to prove that it satisfies the property of substitutivity and hence is a congruence relation, but this check was missing from Ehdm Version 5.2 (however, it is enforced in Version 6).

Ehdm automatically generates trivial proof declarations for the formulas in mapped and TCC modules. Often, these suffice, but in the present case the trivial system-generated proofs in lists map map are inadequate; effective proofs are provided in the module lists map proofs shown on page 67.

A.1.2 List Inductions

The module list inductions on page 68 states the higher-order formula list induction that specifies an induction scheme used to prove properties of lists:

list induction: Theorem p(Λ) ∧ ( ∀ α, x: p(α) ⊃ p(x ∘ α)) ⊃ p(γ)

where p is an arbitrary predicate over lists. This formula is given as a theorem and proven from the formula general induction, which states the general scheme for Nötherian induction and is given in the module noetherian on page 69. The module noetherian is a library module of Ehdm and is described in detail in the Ehdm tutorial [27, Chapter 6]. Interested readers should refer to the discussion in the tutorial for an explanation of the well founded assumption in the module noetherian, and the manner in which it is discharged by the module list inductions. The formula general induction is stated as an axiom and justified by reference to standard texts (for example [16, page 6]).

2This entire construction is very similar to that described for stacks in the Ehdm tutorial [27, Chapter 5]; readers seeking further explanation of mappings in Ehdm should consult that description.

A.2 Sets

The module sets (page 70) introduces sets and the basic set operations of union, intersection, subset, and the like. Sets are modeled by their characteristic predicates and the set operations are defined as higher-order functions. Those unfamiliar with the use of higher-order logic in specifications may find these definitions particularly interesting. Notice that the type of (the predicate representing) a given set is dependent on the type supplied as the actual parameter to the sets module.

A.3 Noninterference

The specification of intransitive noninterference and the proof of its unwinding theorem are presented in the module intrans nonint starting on page 71. The specification begins by introducing the basic types and functions used to state the noninterference notion of security. The names of the types and functions used are the same as those in the conventional mathematical development given in the main body of this report, and the definitions are likewise fairly straightforward transliterations. The main differences occur in the specifications of the functions run, sources, and ipurge: whereas these are defined by (pattern matching) cases over the list constructors Λ and ∘ in the conventional mathematical presentation, the Ehdm specification defines these functions recursively. Recursive definitions in Ehdm require measure functions to be supplied in order to ensure that the recursion is well-founded. The measure functions used here, step count and step count2, employ the length of the list as the measure. The TCCs generated from these recursive definitions appear in the system-generated module intrans nonint tcc on page 78, and effective proofs (the system-generated proofs are inadequate) are given in the module

intrans nonint tcc proofs on page 80.

The equivalence relation that induces view-partitioning is written in infix notation in the form s ∼^{u} t in the conventional mathematical presentation. In the Ehdm specification it is written as view id(u, ss, tt) and is specified as

view id: function[D, S, S → bool] ≡ ( λ u, st, tt: view(u, st) = view(u, tt)) where view is an uninterpreted function. The pragmatic advantage of this method of specification is that view id expands to an equation; thus we do not need to cite the properties of reflexivity, symmetry, and transitivity in proofs that use view id.

   The predicates secure, output consistent, and local respect are the formal

counterparts of the properties of similar names given in the conventional mathematical presentation. The predicate view consistent is introduced to name the main condition in the statement of Lemma 2. In specifying these four predicates, there is a choice as to which of the variables should be locally quantified and which should be specified as parameters in the predicate definition and quantified at a higher level. We chose to locally quantify all variables in these predicates, except the list variables in view consistent and secure. This is really a matter of taste and other choices would work equally well.

Lemmas 2 to 5 in the conventional mathematical development are mirrored by the formulas with similar names in the formal development. The proofs of Lemmas 2 to 4 in the formal verification correspond almost directly to those in the conventional mathematical development. However, the formal verification interposes between the proofs of Lemmas 2 and 3 the statements and proofs of a number of minor technical results that are taken as obvious in the conventional mathematical presentation. The first six of these:

single step lemma: Lemma run(st, a ∘ α) = run(step(st, a), α)

purge lemma: Lemma

ipurge(a ∘ α, u)

= if dom(a) ∈ sources(a ∘ α, u)

then a ∘ ipurge(α, u) else ipurge(α, u) end if

sources subset: Lemma sources(α, u) ⊆ sources(a ∘ α, u)

sources grows: Lemma v ∈ sources(α, u) ⊃ v ∈ sources(a ∘ α, u)

sources defn base case: Lemma sources(Λ, u) = {u}

sources defn inductive case: Lemma

( ∃ v: v ∈ sources(α, u) ∧ dom(a) ⇝ v)

⊃ sources(a ∘ α, u) = {dom(a)} ∪ sources(α, u)

are obvious and have straightforward proofs. However, the next one

in own sources: Lemma u ∈ sources(α, u) requires a proof by induction and uses several intermediate lemmas. When performing a proof by induction in Ehdm, it is usually convenient to define a predicate equivalent to all, or part of, the formula to be proven. The predicate should be parameterized by the induction variable in order to allow inductive instances to be written conveniently. In the present specification, the predicate in own sources pred fulfills this role with respect to the formula in own sources.

The predicate strong view id stands in the same relationship to the equivalence relation ≈^{C} in the conventional mathematical presentation as the predicate view id does to ∼^{u}. However, because strong view id does not reduce to an equation, the properties of reflexivity, symmetry, and transitivity have to proven, and later cited, explicitly. The technical lemma

strong view id sources prop: Lemma

strong view id(sources(a ∘ α, u), st, tt) ⊃ strong view id(sources(α, u), st, tt)

is also proven at this point. Following the proofs of Lemmas 3 and 4, come the definitions and lemmas that establish Lemma 5. The proof is by induction, and we introduce a predicate lemma5 pred to simplify its expression and proof. The module ends with the proof of the unwinding theorem. As in the conventional mathematical presentation, this is a straightforward consequence of Lemmas 2 and 5.

A.4 Top

This module serves to tie the main modules of the specification together. It also contains a proof for the TCC formula car TCC1 from the module lists model tcc shown on page 64. The proof cites the formula nat invariant, which is the subtype invariant for natural numbers—i.e., (λn : n ≥ 0)—from the standard prelude.

Appendix B

Cross-Reference Listing

This Appendix provides two cross-reference tables to assist in reading and navigating the Ehdm specifications that follow. The first provides a cross-reference listing to the identifiers declared in the Ehdm specification; the second provides the translations from raw Ehdm identifiers appearing in the first table and in Appendix B to the symbols appearing in the LaTEX-printed version of the specifications given in Appendix C. All the material appearing in these Appendices was generated mechanically by Ehdm.

Identifier  Declaration Module

A  type  intrans_nonint

add  literal-fn  sets

arbitrary  const  lists_model
Astar  type  intrans_nonint
car  function  lists
car  literal-fn  lists_model
car_ax  axiom  lists
car_ax  formula  lists_map_map
car_ax_PROOF  prove  lists_map_map
car_ax_PROOF  prove  lists_map_proofs
car_TCC1  formula  lists_model_tcc
car_TCC1_PROOF  prove  lists_model_tcc
cdr  function  lists
cdr  literal-fn  lists_model
cdr_ax  axiom  lists
cdr_ax  formula  lists_map_map
cdr_ax_PROOF  prove  lists_map_map
cdr_ax_PROOF  prove  lists_map_proofs
cdr_cons_lemma1  formula  lists_map_proofs
cdr_cons_lemma1_proof prove  lists_map_proofs
cdr_cons_lemma2  formula  lists_map_proofs
cdr_cons_lemma2_proof prove  lists_map_proofs
ce  defined-fn lists_model
ce_isreflexive  formula  lists_map_map
ce_isreflexive_PROOF  prove  lists_map_map
ce_isreflexive_PROOF  prove  lists_map_proofs
ce_issymmetric  formula  lists_map_map
ce_issymmetric_PROOF  prove  lists_map_map
ce_issymmetric_PROOF  prove  lists_map_proofs
ce_istransitive  formula  lists_map_map
ce_istransitive_PROOF prove  lists_map_map
ce_istransitive_PROOF prove  lists_map_proofs
connects  defined-fn intrans_nonint
cons  defined-fn lists_model
cons  function  lists
cons_ax  axiom  lists
cons_ax  formula  lists_map_map
cons_ax_PROOF  prove  lists_map_map
cons_ax_PROOF  prove  lists_map_proofs
cons_induction_proof  prove  list_inductions
D  type  intrans_nonint
difference  literal-fn  sets
discharge_well_founded prove  list_inductions
dof  defined-fn intrans_nonint

52 Appendix B. Cross-Reference Listing

Identifier  Declaration Module

dom  function  intrans_nonint
empty  defined-fn  sets

emptyset  literal-const sets

extends  literal-fn  list_inductions
extensionality  axiom  sets

fullset  literal-const sets

general_induction  axiom  noetherian
in_own_sources  formula  intrans_nonint
in_own_sources_basis  formula  intrans_nonint
in_own_sources_basis_proof prove  intrans_nonint
in_own_sources_form  formula  intrans_nonint
in_own_sources_form_proof  prove  intrans_nonint
in_own_sources_induct  formula  intrans_nonint
in_own_sources_induct_proof prove  intrans_nonint
in_own_sources_pred  defined-fn  intrans_nonint
in_own_sources_proof  prove  intrans_nonint
interfere  function  intrans_nonint
intersection  literal-fn  sets
intrans_nonint  module  intrans_nonint
intrans_nonint_tcc  module  intrans_nonint_tcc
intrans_nonint_tcc_proofs  module  intrans_nonint_tcc_proofs
ipurge  recursive-fn intrans_nonint
ipurge_TCC1  formula  intrans_nonint_tcc
ipurge_TCC1_PROOF  prove  intrans_nonint_tcc
ipurge_TCC2  formula  intrans_nonint_tcc
ipurge_TCC2_PROOF  prove  intrans_nonint_tcc
lemma2  formula  intrans_nonint
lemma2_proof  prove  intrans_nonint
lemma3  formula  intrans_nonint
lemma3_proof  prove  intrans_nonint
lemma4  formula  intrans_nonint
lemma4_proof  prove  intrans_nonint
lemma5  formula  intrans_nonint
lemma5_basis  formula  intrans_nonint
lemma5_basis_proof  prove  intrans_nonint
lemma5_induct  formula  intrans_nonint
lemma5_induct_proof  prove  intrans_nonint
lemma5_pred  defined-fn  intrans_nonint
lemma5_proof  prove  intrans_nonint
length  function  lists
length  literal-fn  lists_model
length_cdr  formula  lists
length_cdr_proof  prove  lists
length_cons  axiom  lists

Identifier  Declaration Module

length_cons  formula  lists_map_map
length_cons_PROOF prove  lists_map_map
length_cons_PROOF prove  lists_map_proofs
length_nil  axiom  lists
length_nil  formula  lists_map_map
length_nil_PROOF  prove  lists_map_map
length_nil_PROOF  prove  lists_map_proofs
list  type  lists_model
list  type  lists
listarray  type  lists_model
list_induction  formula  list_inductions
list_inductions  module  list_inductions
lists  module  lists
lists_map  module  lists_map
lists_map_map  module  lists_map_map
lists_map_proofs  module  lists_map_proofs
lists_model  module  lists_model
lists_model_tcc  module  lists_model_tcc
local_respect  defined-const intrans_nonint
member  literal-fn  sets
nil  const  lists_model
nil  const  lists
nilax  axiom  lists_model
nilorcons_ax  axiom  lists
nilorcons_ax  formula  lists_map_map
nilorcons_ax_PROOF prove  lists_map_map
nilorcons_ax_PROOF prove  lists_map_proofs
noetherian  module  noetherian
noninterfere  literal-fn  intrans_nonint

null  literal-fn  lists

O  type  intrans_nonint
output  function  intrans_nonint
output_consistent defined-const intrans_nonint
purge_lemma  formula  intrans_nonint
purge_lemma_proof prove  intrans_nonint
purge_TCC1_PROOF  prove  intrans_nonint_tcc_proofs
purge_TCC2_PROOF  prove  intrans_nonint_tcc_proofs
run  recursive-fn intrans_nonint
run_TCC1  formula  intrans_nonint_tcc
run_TCC1_PROOF  prove  intrans_nonint_tcc
run_TCC1_PROOF  prove  intrans_nonint_tcc_proofs
S  type  intrans_nonint
secure  defined-fn  intrans_nonint
set  type  sets

54 Appendix B. Cross-Reference Listing

Identifier  Declaration Module

sets  module  sets
single_step_lemma  formula  intrans_nonint
single_step_lemma_proof  prove  intrans_nonint
singleton  literal-fn  sets
sources  recursive-fn intrans_nonint
sources_defn_base_case  formula  intrans_nonint
sources_defn_base_case_proof  prove  intrans_nonint
sources_defn_inductive_case  formula  intrans_nonint
sources_defn_inductive_case_proof prove  intrans_nonint
sources_grows  formula  intrans_nonint
sources_grows_proof  prove  intrans_nonint
sources_subset  formula  intrans_nonint
sources_subset_proof  prove  intrans_nonint
sources_TCC1  formula  intrans_nonint_tcc
sources_TCC1_PROOF  prove  intrans_nonint_tcc
sources_TCC1_PROOF  prove  intrans_nonint_tcc_proofs
sources_TCC2  formula  intrans_nonint_tcc
sources_TCC2_PROOF  prove  intrans_nonint_tcc
sources_TCC2_PROOF  prove  intrans_nonint_tcc_proofs
sources_TCC3  formula  intrans_nonint_tcc
sources_TCC3_PROOF  prove  intrans_nonint_tcc
sources_TCC3_PROOF  prove  intrans_nonint_tcc_proofs
st0  const  intrans_nonint
step  function  intrans_nonint
step_count  literal-fn  intrans_nonint
step_count2  literal-fn  intrans_nonint
strong_view_id  defined-fn intrans_nonint
strong_view_id_reflexive  formula  intrans_nonint
strong_view_id_reflexive_proof  prove  intrans_nonint
strong_view_id_sources_prop  formula  intrans_nonint
strong_view_id_sources_prop_proof prove  intrans_nonint
strong_view_id_symmetric  formula  intrans_nonint
strong_view_id_symmetric_proof  prove  intrans_nonint
strong_view_id_transitive  formula  intrans_nonint
strong_view_id_transitive_proof  prove  intrans_nonint
subset  defined-fn sets
subset_add  formula  sets
subset_add_proof  prove  sets
subset_self  formula  sets
subset_self_proof  prove  sets
TCC_proof  prove  top
test  defined-fn intrans_nonint
top  module  top

union  literal-fn  sets

Identifier  Declaration Module

unwinding  formula  intrans_nonint
unwinding_proof  prove  intrans_nonint
V  type  intrans_nonint
value  const  lists_model
view  function  intrans_nonint
view_consistent  defined-fn  intrans_nonint
view_id  literal-fn  intrans_nonint
weak_step_consistent defined-const intrans_nonint
well_founded  formula  noetherian

Table B.1: Ehdm Identifers used in the Specification

Identifier  Translation

           A  A

add  {x} ∪ a

           alist  α
           Astar  A^{⋆}
           cons  s ∘ α
           D  D
           difference  a − b
           dof  do
           emptyset  ∅
           I  I
           interfere  u ⇝ v
           intersection a ⋂ b
           member  x ∈ b
           nil  Λ
           noninterfere u ⇝̸ v
           O  O
           singleton  {x}
           S  S
           st0  st_{0}
           subset  a ⊆ b
           union  a ⋃ b

Table B.2: Translations for Identifiers Used in the Specification

Appendix C

Proof-Chain Analysis

The following pages reproduce the output from the Ehdm proof-chain analyzer in terse mode applied first to the formula unwinding in module intrans nonint and then to all the formulas in the mapped module lists map map. The Ehdm proofchain analyzer examines the macroscopic structure of a verification by checking that all the premises used in a proof are either axioms, definitions, or formulas which are, themselves, the target of a successful proof elsewhere in the verification. If any formulas are used from a module with an assuming clause, then the proof-chain analyzer checks that those assumptions are discharged by successful proofs; similarly, if formulas are used from a module with a TCC module, then the proof-chain analyzer checks that all the TCCs in that module are discharged by successful proofs. The trivial system-generated proof declarations in the TCC module itself are often unsuccessful, so the user must supply more adequate proofs in another module (TCC modules cannot be altered). The proof-chain analyzer ignores unsuccessful proofs, such as system-generated TCC proofs, when a successful proof for the same formula can be found. The terse mode output reproduced here provides a commentary on only the “interesting” cases, namely proof obligations involving assuming clauses and TCCs, and a summary. A shortcoming of the analysis is that literal constants (i.e., those defined with a double ==) are not reported. All the proofs listed in the summary were performed by the Ehdm theorem prover in checking mode.

C.1 Proof-Chain for the Unwinding Theorem

The following pages reproduce the output from the Ehdm proof-chain analyzer applied to the formula unwinding in module intrans nonint. It can be seen that the proof chain is complete.

Terse proof chain for formula unwinding in module intrans_nonint
Use of the formula
  intrans_nonint.unwinding
requires the following TCCs to be proven

C.1. Proof-Chain for the Unwinding Theorem 57

  intrans_nonint_tcc.run_TCC1
  intrans_nonint_tcc.sources_TCC1
  intrans_nonint_tcc.sources_TCC2
  intrans_nonint_tcc.sources_TCC3
  intrans_nonint_tcc.ipurge_TCC1
  intrans_nonint_tcc.ipurge_TCC2
Formula intrans_nonint_tcc.run_TCC1 is a termination TCC for intrans_nonint.run
Proof of
  intrans_nonint_tcc.run_TCC1
must not use
  intrans_nonint.run
Formula intrans_nonint_tcc.sources_TCC1 is a termination TCC for
intrans_nonint.sources
Proof of
  intrans_nonint_tcc.sources_TCC1
must not use
  intrans_nonint.sources
Formula intrans_nonint_tcc.sources_TCC2 is a termination TCC for
intrans_nonint.sources
Proof of
  intrans_nonint_tcc.sources_TCC2
must not use
  intrans_nonint.sources
Formula intrans_nonint_tcc.sources_TCC3 is a termination TCC for
intrans_nonint.sources
Proof of
  intrans_nonint_tcc.sources_TCC3
must not use
  intrans_nonint.sources
Formula intrans_nonint_tcc.ipurge_TCC1 is a termination TCC for
intrans_nonint.ipurge
Proof of
  intrans_nonint_tcc.ipurge_TCC1
must not use
  intrans_nonint.ipurge
Formula intrans_nonint_tcc.ipurge_TCC2 is a termination TCC for
intrans_nonint.ipurge
Proof of
  intrans_nonint_tcc.ipurge_TCC2
must not use
  intrans_nonint.ipurge

58 Appendix C. Proof-Chain Analysis

Use of the formula
noetherian[lists[...].list, list_inductions[...].extends].general_induction
requires the following assumptions to be discharged
noetherian[lists[...].list, list_inductions[...].extends].well_founded
 ================== SUMMARY ==================
The proof chain is complete
The axioms and assumptions at the base are:
lists[EXPR].car_ax
lists[EXPR].cdr_ax
lists[EXPR].cons_ax
lists[EXPR].length_cons
lists[EXPR].nilorcons_ax
noetherian[EXPR, EXPR].general_induction
Total: 6
The definitions and type-constraints are:
intrans_nonint.connects
intrans_nonint.dof
intrans_nonint.in_own_sources_pred
intrans_nonint.ipurge
intrans_nonint.lemma5_pred
intrans_nonint.local_respect
intrans_nonint.output_consistent
intrans_nonint.run
intrans_nonint.secure
intrans_nonint.sources
intrans_nonint.strong_view_id
intrans_nonint.test
intrans_nonint.view_consistent
intrans_nonint.weak_step_consistent
sets[EXPR].subset
Total: 15
The formulae used are:
intrans_nonint.in_own_sources
intrans_nonint.in_own_sources_basis
intrans_nonint.in_own_sources_form
intrans_nonint.in_own_sources_induct
intrans_nonint.lemma2
intrans_nonint.lemma3
intrans_nonint.lemma4
intrans_nonint.lemma5
intrans_nonint.lemma5_basis
intrans_nonint.lemma5_induct
intrans_nonint.purge_lemma

C.1. Proof-Chain for the Unwinding Theorem 59

intrans_nonint.single_step_lemma
intrans_nonint.sources_defn_base_case
intrans_nonint.sources_defn_inductive_case
intrans_nonint.sources_grows
intrans_nonint.sources_subset
intrans_nonint.strong_view_id_reflexive
intrans_nonint.strong_view_id_sources_prop
intrans_nonint.strong_view_id_symmetric
intrans_nonint.strong_view_id_transitive
intrans_nonint.unwinding
intrans_nonint_tcc.ipurge_TCC1
intrans_nonint_tcc.ipurge_TCC2
intrans_nonint_tcc.run_TCC1
intrans_nonint_tcc.sources_TCC1
intrans_nonint_tcc.sources_TCC2
intrans_nonint_tcc.sources_TCC3
list_inductions[EXPR].list_induction
lists[EXPR].length_cdr
noetherian[lists[...].list, list_inductions[...].extends].well_founded
sets[EXPR].subset_add
sets[EXPR].subset_self
Total: 32
The completed proofs are:
intrans_nonint.in_own_sources_basis_proof
intrans_nonint.in_own_sources_form_proof
intrans_nonint.in_own_sources_induct_proof
intrans_nonint.in_own_sources_proof
intrans_nonint.lemma2_proof
intrans_nonint.lemma3_proof
intrans_nonint.lemma4_proof
intrans_nonint.lemma5_basis_proof
intrans_nonint.lemma5_induct_proof
intrans_nonint.lemma5_proof
intrans_nonint.purge_lemma_proof
intrans_nonint.single_step_lemma_proof
intrans_nonint.sources_defn_base_case_proof
intrans_nonint.sources_defn_inductive_case_proof
intrans_nonint.sources_grows_proof
intrans_nonint.sources_subset_proof
intrans_nonint.strong_view_id_reflexive_proof
intrans_nonint.strong_view_id_sources_prop_proof
intrans_nonint.strong_view_id_symmetric_proof
intrans_nonint.strong_view_id_transitive_proof
intrans_nonint.unwinding_proof
intrans_nonint_tcc_proofs.purge_TCC1_PROOF
intrans_nonint_tcc_proofs.purge_TCC2_PROOF
intrans_nonint_tcc_proofs.run_TCC1_PROOF

60 Appendix C. Proof-Chain Analysis

intrans_nonint_tcc_proofs.sources_TCC1_PROOF
intrans_nonint_tcc_proofs.sources_TCC2_PROOF
intrans_nonint_tcc_proofs.sources_TCC3_PROOF
list_inductions[EXPR].cons_induction_proof
list_inductions[EXPR].discharge_well_founded
lists[EXPR].length_cdr_proof
sets[EXPR].subset_add_proof
sets[EXPR].subset_self_proof
Total: 32

C.2 Proof-Chain for the Mapping of the Lists Module

The following pages reproduce the output from the Ehdm proof-chain analyzer applied to all the formulas in the mapped module lists map map. It can be seen that the proof chain is complete, thereby demonstrating the soundness of the mapping.

Terse proof chains of all formulas in module lists_map_map
Use of the formula
lists_model[EXPR].ce
requires the following TCCs to be proven
lists_model_tcc[EXPR].car_TCC1
                      SUMMARY
The proof chain is complete
The axioms and assumptions at the base are:
lists_model[EXPR].nilax
Total: 1
The definitions and type-constraints are:
lists_model[EXPR].ce
lists_model[EXPR].cons
naturalnumbers.nat_invariant
Total: 3
The formulae used are:
lists_map_map[EXPR].car_ax
lists_map_map[EXPR].cdr_ax
lists_map_map[EXPR].ce_isreflexive
lists_map_map[EXPR].ce_issymmetric
lists_map_map[EXPR].ce_istransitive
lists_map_map[EXPR].cons_ax
lists_map_map[EXPR].length_cons

C.2. Proof-Chain for the Mapping of the Lists Module 61

lists_map_map[EXPR].length_nil
lists_map_map[EXPR].nilorcons_ax
lists_map_proofs[EXPR].cdr_cons_lemma1
lists_map_proofs[EXPR].cdr_cons_lemma2
lists_model_tcc[EXPR].car_TCC1
Total: 12
The completed proofs are:
lists_map_proofs[EXPR].car_ax_PROOF
lists_map_proofs[EXPR].cdr_ax_PROOF
lists_map_proofs[EXPR].cdr_cons_lemma1_proof
lists_map_proofs[EXPR].cdr_cons_lemma2_proof
lists_map_proofs[EXPR].ce_isreflexive_PROOF
lists_map_proofs[EXPR].ce_issymmetric_PROOF
lists_map_proofs[EXPR].ce_istransitive_PROOF
lists_map_proofs[EXPR].cons_ax_PROOF
lists_map_proofs[EXPR].length_cons_PROOF
lists_map_proofs[EXPR].length_nil_PROOF
lists_map_proofs[EXPR].nilorcons_ax_PROOF
top[EXPR].TCC_proof
Total: 12

Appendix D

Specifications

lists: Module [T : Type]

Exporting all Theory

list: Type Λ: list s, t: Var T ρ: Var list null: function[list → bool] == ( λ ρ : ρ = Λ) s ∘ ρ: function[T , list → list] car: function[list → T ] cdr: function[list → list] cons ax: Axiom ¬(s ∘ ρ = Λ) car ax: Axiom car(s ∘ ρ) = s cdr ax: Axiom cdr(s ∘ ρ) = ρ nilorcons ax: Axiom ρ = Λ ∨ ρ = car(ρ) ∘ cdr(ρ) length: function[list → nat] length nil: Axiom length(Λ) = 0 length cons: Axiom length(s ∘ ρ) = length(ρ) + 1 length cdr: Lemma ¬(null(ρ)) ⊃ length(ρ) > length(cdr(ρ))

Proof

length cdr proof: Prove length cdr from

nilorcons ax, length cons {ρ ← cdr(ρ@p1), s ← car(ρ@p1)} End lists

lists model 63

lists model: Module [T : Type]

Exporting all Theory

listarray: Type = array[nat]of T list: Type = Record nextpos : nat,

value : listarray end record

arbitrary: T Λ: list nilax: Axiom Λ.nextpos = 0 s, t: Var T ρ, σ: Var list n: Var nat ce: function[list, list → bool] =

( λ ρ, σ :

ρ.nextpos = σ.nextpos

∧ ( ∀ n : n < ρ.nextpos ⊃ ρ.value(n) = σ.value(n)))

s ∘ ρ: function[T , list → list] =

( λ s, ρ : ρ

with [(value) := ρ.value with [(ρ.nextpos) := s],

(nextpos) := ρ.nextpos + 1])

car: function[list → T ] ==

( λ ρ : if ρ.nextpos = 0

then arbitrary

else ρ.value(ρ.nextpos − 1)

end if)

cdr: function[list → list] ==

( λ ρ : if ρ.nextpos = 0 then Λ else ρ with [(nextpos) := ρ.nextpos − 1] end if)

64 Appendix D. Specifications

length: function[list → nat] == ( λ ρ : ρ.nextpos) End lists model lists model tcc: Module [T : Type]

Using lists model[T ] Exporting all with lists model Theory

ρ: Var list

(* Subtype TCC generated for the first argument to rho in car  AND
   Subtype TCC generated for cdr *)

car TCC1: Formula (¬(ρ.nextpos = 0)) ⊃ (ρ.nextpos − 1 ≥ 0)

Proof

car TCC1 PROOF: Prove car TCC1 End lists model tcc

lists map 65

lists map: Module [T : Type] Mapping lists[T ] onto lists model[T ]

=[list[T ]] → ce End lists map lists map map: Module [T : Type]

Using lists model[T ] Exporting all with lists model[T ] Theory

ρ: Var lists model[T ].list s: Var T x_{1}: Var lists model[T ].list x_{2}: Var lists model[T ].list x_{3}: Var lists model[T ].list ce isreflexive: Formula ce(x_{1}, x_{1}) ce issymmetric: Formula ce(x_{1}, x_{2}) ⊃ ce(x_{2}, x_{1}) ce istransitive: Formula ce(x_{1}, x_{2}) ∧ ce(x_{2}, x_{3}) ⊃ ce(x_{1}, x_{3}) cons ax: Formula ¬(ce(s ∘ ρ, Λ)) car ax: Formula car(s ∘ ρ) = s cdr ax: Formula ce(cdr(s ∘ ρ), ρ) nilorcons ax: Formula ce(ρ, Λ) ∨ ce(ρ, car(ρ) ∘ cdr(ρ)) length nil: Formula length(Λ) = 0 length cons: Formula length(s ∘ ρ) = length(ρ) + 1

Proof

ce isreflexive PROOF: Prove ce isreflexive ce issymmetric PROOF: Prove ce issymmetric ce istransitive PROOF: Prove ce istransitive cons ax PROOF: Prove cons ax car ax PROOF: Prove car ax cdr ax PROOF: Prove cdr ax nilorcons ax PROOF: Prove nilorcons ax length nil PROOF: Prove length nil length cons PROOF: Prove length cons

End lists map map

lists map proofs 67

lists map proofs: Module [T : Type]

Using lists map map[T ] Proof

ce isreflexive PROOF: Prove ce isreflexive from

ce {ρ ← x_{1}, σ ← x_{1}} ce issymmetric PROOF: Prove ce issymmetric from

ce {ρ ← x_{2}, σ ← x_{1}}, ce {ρ ← x_{1}, σ ← x_{2}, n ← n@p1}

ce istransitive PROOF: Prove ce istransitive from ce {ρ ← x_{1}, σ ← x_{3}}, ce {ρ ← x_{2}, σ ← x_{3}, n ← n@p1}, ce {ρ ← x_{1}, σ ← x_{2}, n ← n@p1}

cons ax PROOF: Prove cons ax from ce {ρ ← s ∘ ρ, σ ← Λ}, nilax, s ∘ ρ, nat invariant {nat var ← (ρ@c).nextpos}

car ax PROOF: Prove car ax from

s ∘ ρ, nat invariant {nat var ← (ρ@c).nextpos} ρ, σ: Var lists model[T ].list s: Var T n: Var nat cdr cons lemma1: Lemma length(cdr(s ∘ ρ)) = length(ρ) cdr cons lemma1 proof: Prove cdr cons lemma1 from

s ∘ ρ, nat invariant {nat var ← (ρ@c).nextpos} cdr cons lemma2: Lemma n < length(ρ) ⊃ (cdr(s ∘ ρ)).value(n) = ρ.value(n) cdr cons lemma2 proof: Prove cdr cons lemma2 from

s ∘ ρ, nat invariant {nat var ← (ρ@c).nextpos} cdr ax PROOF: Prove cdr ax from

ce {σ ← ρ, ρ ← cdr(s ∘ ρ)}, cdr cons lemma1, cdr cons lemma2 {n ← n@p1}

nilorcons ax PROOF: Prove nilorcons ax from ce {σ ← Λ, ρ ← ρ@c}, ce {σ ← car(ρ) ∘ cdr(ρ)}, s ∘ ρ {s ← car(ρ), ρ ← cdr(ρ)}, nilax, nat invariant {nat var ← (ρ@c).nextpos}

length nil PROOF: Prove length nil from nilax length cons PROOF: Prove length cons from s ∘ ρ

End lists map proofs list inductions: Module [t: Type]

Using lists[t] Theory

x: Var t ρ, σ, τ: Var list p: Var function[list → bool] extends: function[list, list → bool] == ( λ ρ, σ : σ ≠ Λ ∧ ρ = cdr(σ)) list induction: Theorem p(Λ) ∧ ( ∀ ρ, x : p(ρ) ⊃ p(x ∘ ρ)) ⊃ p(τ)

Proof Using noetherian[list, extends]

cons induction proof: Prove list induction {ρ ← cdr(d_{1}@p1), x ← car(d_{1}@p1)} from general induction {d ← τ, d_{2} ← ρ}, nilorcons ax {ρ ← d_{1}@p1}

discharge well founded: Prove well founded {measure ← length} from

length cdr {ρ ← b} End list inductions

noetherian 69

noetherian: Module [dom: Type, <: function[dom, dom → bool]]

Assuming

measure: Var function[dom → nat] a, b: Var dom well founded: Formula ( ∃ measure : a < b ⊃ measure(a) < measure(b))

Theory

p: Var function[dom → bool] d, d_{1}, d_{2}: Var dom general induction: Axiom

( ∀ d_{1} : ( ∀ d_{2} : d_{2} < d_{1} ⊃ p(d_{2})) ⊃ p(d_{1})) ⊃ ( ∀ d : p(d)) End noetherian sets: Module [T : Type]

Exporting all Theory

set: Type is function[T → bool] x, y, z: Var T a, b: Var set x ∈ b: function[T , set → bool] == ( λ x, b : b(x)) a ∪ b: function[set, set → set] == ( λ a, b : ( λ x : x ∈ a ∨ x ∈ b)) a ∩ b: function[set, set → set] == ( λ a, b : ( λ x : x ∈ a ∧ x ∈ b)) a − b: function[set, set → set] == ( λ a, b : ( λ x : x ∈ a ∧ ¬x ∈ b)) {x} ∪ a: function[T , set → set] == ( λ x, a : ( λ y : x = y ∨ a(y))) {x}: function[T → set] == ( λ x : ( λ y : y = x)) a ⊆ b: function[set, set → bool] = ( λ a, b : ( ∀ z : z ∈ a ⊃ z ∈ b)) empty: function[set → bool] = ( λ a : ( ∀ x : ¬x ∈ a)) ∅: set == ( λ x : false) fullset: set == ( λ x : true) extensionality: Axiom ( ∀ x : x ∈ a = x ∈ b) ⊃ (a = b) subset self: Lemma a ⊆ a subset add: Lemma a ⊆ {x} ∪ a

Proof

subset self proof: Prove subset self from a ⊆ b {b ← a} subset add proof: Prove subset add from a ⊆ b {b ← {x} ∪ a}

intrans nonint 71

End sets intrans nonint: Module

Using lists, sets Exporting all with lists, sets Theory

S : Type(* States *)
st_{0}: S(* Initial State *)

st, tt, wt: Var S

D : Type(* security domains *)

A : Type dom: function[A → D] a, b: Var A A^{⋆} : Type is list[A] α: Var A^{⋆} step: function[S, A → S] step count: function[S, A^{⋆} → nat] == ( λ st, α : length(α)) run: Recursive function[S, A^{⋆} → S] =

( λ st, α : if null(α) then st else run(step(st, car(α)), cdr(α)) end if) by step count

u, v: Var D u ⇝ v: function[D, D → bool] u ⇝̸ v: function[D, D → bool] == ( λ u, v : ¬u ⇝ v) step count2: function[A^{⋆}, D → nat] == ( λ α, u : length(α)) src: Var set[D] connects: function[set, D → bool] =

( λ src, u : ( ∃ v : v ∈ src ∧ u ⇝ v)) sources: Recursive function[A^{⋆}, D → function[D → bool]] =

( λ α, u :

if null(α) then {u} elsif connects(sources(cdr(α), u), (dom(car(α)))) then {(dom(car(α)))} ∪ sources(cdr(α), u) else sources(cdr(α), u)

end if) by step count2 ipurge: Recursive function[A^{⋆}, D → A^{⋆}] =

( λ α, u :

if null(α) then Λ elsif (dom(car(α))) ∈ sources(α, u) then car(α) ∘ ipurge(cdr(α), u) else ipurge(cdr(α), u)

end if) by step count2

O : Type (* outputs *)

output: function[S, A → O]

do: function[A^{⋆} → S] = ( λ α : run(st_{0}, α))

test: function[A^{⋆}, A → O] = ( λ α, a : output(do(α), a))

secure: function[A^{⋆} → bool] = ( λ α : ( ∀ a : test(α, a) = test(ipurge(α, dom(a)), a)))

V: Type

view: function[D, S → V]

view id: function[D, S, S → bool] == ( λ u, st, tt : view(u, st) = view(u, tt))

output consistent: bool =

( ∀ a, st, tt :

view id(dom(a), st, tt) ⊃ output(st, a) = output(tt, a))

view consistent: function[A^{⋆} → bool] = ( λ α : ( ∀ u : view id(u, do(α), do(ipurge(α, u)))))

local respect: bool = ( ∀ v, st, a : dom(a) ⇝̸ v ⊃ view id(v, st, step(st, a)))

weak step consistent: bool =

( ∀ u, st, tt, a :

view id(u, st, tt) ∧ view id(dom(a), st, tt) ⊃ view id(u, step(st, a), step(tt, a)))

lemma2: Lemma view consistent(α) ∧ output consistent ⊃ secure(α)

unwinding: Theorem local respect ∧ weak step consistent ∧ output consistent ⊃ secure(α)

Proof

Using list inductions

lemma2 proof: Prove lemma2 from secure, view consistent {u ← dom(a@p1)}, output consistent

{a ← a@p1, st ← do(α), tt ← do(ipurge(α, u@p2f))},

test {a ← a@p1}, test {a ← a@p1, α ← ipurge(α, u@p2f)}

single step lemma: Lemma run(st, a ∘ α) = run(step(st, a), α)

single step lemma proof: Prove single step lemma from run {α ← a ∘ α}, cons ax[A ] {ρ ← α, s ← a}, car ax[A ] {ρ ← α, s ← a}, cdr ax[A ] {ρ ← α, s ← a}

purge lemma: Lemma

ipurge(a ∘ α, u)

= if dom(a) ∈ sources(a ∘ α, u) then a ∘ ipurge(α, u) else ipurge(α, u) end if

purge lemma proof: Prove purge lemma from ipurge {α ← a ∘ α}, cons ax[A ] {ρ ← α, s ← a}, car ax[A ] {ρ ← α, s ← a}, cdr ax[A ] {ρ ← α, s ← a}

sources subset: Lemma sources(α, u) ⊆ sources(a ∘ α, u)

sources subset proof: Prove sources subset from sources {α ← a ∘ α}, cons ax[A ] {s ← a, ρ ← α}, cdr ax[A ] {s ← a, ρ ← α}, car ax[A ] {s ← a, ρ ← α}, subset self[D ] {a ← sources(α, u)}, subset add[D ] {a ← sources(α, u), x ← dom(a)}

sources grows: Lemma v ∈ sources(α, u) ⊃ v ∈ sources(a ∘ α, u)

sources grows proof: Prove sources grows from sources subset, a ⊆ b [D ] {a ← sources(α, u), b ← sources(a ∘ α, u), z ← v}

sources defn base case: Lemma sources(Λ, u) = {u}

sources defn base case proof: Prove sources defn base case from sources {α ← Λ} sources defn inductive case: Lemma

( ∃ v : v ∈ sources(α, u) ∧ dom(a) ⇝ v)

⊃ sources(a ∘ α, u) = {dom(a)} ∪ sources(α, u)

sources defn inductive case proof: Prove sources defn inductive case from sources {α ← a ∘ α}, connects {src ← sources(α, u), u ← dom(a)}, cons ax[A ] {s ← a, ρ ← α}, cdr ax[A ] {s ← a, ρ ← α}, car ax[A ] {s ← a, ρ ← α}

in own sources: Lemma u ∈ sources(α, u)

in own sources pred: function[A^{⋆} → bool] = ( λ α : ( ∀ u : u ∈ sources(α, u)))

in own sources form: Lemma in own sources pred(α)

in own sources basis: Lemma in own sources pred(Λ)

in own sources basis proof: Prove in own sources basis from in own sources pred {α ← Λ}, sources defn base case {u ← u@p1}

in own sources induct: Lemma in own sources pred(α) ⊃ in own sources pred(a ∘ α)

in own sources induct proof: Prove in own sources induct from in own sources pred {u ← u@p2}, in own sources pred {α ← a ∘ α}, sources grows {u ← u@p2, v ← u@p2}

in own sources form proof: Prove in own sources form from list induction {τ ← α, p ← in own sources pred}, in own sources basis, in own sources induct {a ← x@p1, α ← ρ@p1}

in own sources proof: Prove in own sources from in own sources form, in own sources pred

C: Var set[D]

strong view id: function[set, S, S → bool] = ( λ C, st, tt : ( ∀ v : v ∈ C ⊃ view(v, st) = view(v, tt)))

strong view id reflexive: Lemma strong view id(C, st, st)

strong view id reflexive proof: Prove strong view id reflexive from strong view id {tt ← st}

strong view id symmetric: Lemma strong view id(C, st, tt) ⊃ strong view id(C, tt, st)

strong view id symmetric proof: Prove strong view id symmetric from strong view id {v ← v@p2}, strong view id {st ← tt, tt ← st} strong view id transitive: Lemma

strong view id(C, st, tt) ∧ strong view id(C, tt, wt) ⊃ strong view id(C, st, wt)

strong view id transitive proof: Prove strong view id transitive from strong view id {v ← v@p3}, strong view id {v ← v@p3, st ← tt, tt ← wt}, strong view id {tt ← wt}

strong view id sources prop: Lemma

strong view id(sources(a ∘ α, u), st, tt)

⊃ strong view id(sources(α, u), st, tt)

strong view id sources prop proof: Prove strong view id sources prop from strong view id {C ← sources(α, u)}, strong view id {C ← sources(a ∘ α, u), v ← v@p1}, sources grows {v ← v@p1}

lemma3: Lemma

weak step consistent

∧ local respect ∧ strong view id(sources(a ∘ α, u), st, tt) ⊃ strong view id(sources(α, u), step(st, a), step(tt, a))

lemma3 proof: Prove lemma3 from strong view id {v ← v@p2, C ← sources(a ∘ α, u)}, strong view id

{C ← sources(α, u), st ← step(st, a), tt ← step(tt, a)},

sources grows {v ← v@p2}, local respect {v ← v@p2}, local respect {v ← v@p2, st ← tt}, weak step consistent {u ← v@p2}, strong view id {v ← dom(a), C ← sources(a ∘ α, u)}, sources defn inductive case {v ← v@p2}

lemma4: Lemma

local respect ∧ ¬dom(a) ∈ sources(a ∘ α, u)

⊃ strong view id(sources(α, u), st, step(st, a))

lemma4 proof: Prove lemma4 from local respect {v ← v@p2}, strong view id {C ← sources(α, u), tt ← step(st, a)}, sources defn inductive case {v ← v@p2}

lemma5: Lemma

weak step consistent

∧ local respect ∧ strong view id(sources(α, u), st, tt) ⊃ view id(u, run(st, α), run(tt, ipurge(α, u))) lemma5 pred: function[A^{⋆} → bool] =

( λ α : ( ∀ u, st, tt :

weak step consistent

∧ local respect ∧ strong view id(sources(α, u), st, tt) ⊃ view id(u, run(st, α), run(tt, ipurge(α, u)))))

lemma5 basis: Lemma lemma5 pred(Λ)

lemma5 basis proof: Prove lemma5 basis from lemma5 pred {α ← Λ}, strong view id

{v ← u@p1,

C ← sources(Λ, u@p1), st ← st@p1, tt ← tt@p1},

ipurge {α ← Λ, u ← u@p1}, run {α ← Λ, st ← st@p1}, run {α ← Λ, st ← tt@p1}, in own sources {α ← Λ, u ← u@p1}

lemma5 induct: Lemma lemma5 pred(α) ⊃ lemma5 pred(a ∘ α)

lemma5 induct proof: Prove lemma5 induct from lemma5 pred {α ← a ∘ α}, lemma5 pred

{u ← u@p1,

st ← step(st@p1, a), tt ← step(tt@p1, a)},

lemma5 pred {u ← u@p1, st ← step(st@p1, a), tt ← tt@p1}, lemma3 {u ← u@p1, st ← st@p1, tt ← tt@p1}, single step lemma {st ← st@p1}, single step lemma {α ← ipurge(α, u@p1), st ← tt@p1}, purge lemma {u ← u@p1}, lemma4 {u ← u@p1, st ← st@p1}, strong view id sources prop

{u ← u@p1,

st ← st@p1,

tt ← tt@p1}, strong view id symmetric

{C ← sources(α, u@p1), st ← st@p1, tt ← step(st@p1, a)},

strong view id transitive {C ← sources(α, u@p1), st ← step(st@p1, a), tt ← st@p1, wt ← tt@p1} lemma5 proof: Prove lemma5 from

list induction {τ ← α, p ← lemma5 pred}, lemma5 basis, lemma5 induct {a ← x@p1, α ← ρ@p1}, lemma5 pred

unwinding proof: Prove unwinding from view consistent, lemma2, lemma5 {u ← u@p1, st ← st_{0}, tt ← st_{0}}, do, do {α ← ipurge(α, u@p1)}, strong view id reflexive {C ← sources(α, u@p1), st ← st_{0}}

End intrans nonint intrans nonint tcc: Module

Using intrans nonint Exporting all with intrans nonint Theory

α: Var lists[A].list tt: Var S st: Var S v: Var D ρ: Var lists[A].list x: Var A u: Var D a: Var A

(* Termination TCC generated for run *)

run TCC1: Formula

(¬(null(α))) ⊃ step count(st, α) > step count(step(st, car(α)), cdr(α))

(* Termination TCC generated for sources *)

sources TCC1: Formula

(¬(null(α))) ⊃ step count2(α, u) > step count2(cdr(α), u)

(* Termination TCC generated for sources *)

sources TCC2: Formula

(connects(sources(cdr(α), u), (dom(car(α))))) ∧ (¬(null(α)))

⊃ step count2(α, u) > step count2(cdr(α), u)

(* Termination TCC generated for sources *)

sources TCC3: Formula

(¬(connects(sources(cdr(α), u), (dom(car(α)))))) ∧ (¬(null(α)))

⊃ step count2(α, u) > step count2(cdr(α), u)

(* Termination TCC generated for ipurge *)

ipurge TCC1: Formula

((dom(car(α))) ∈ sources(α, u)) ∧ (¬(null(α)))

⊃ step count2(α, u) > step count2(cdr(α), u)

(* Termination TCC generated for ipurge *)

ipurge TCC2: Formula

(¬((dom(car(α))) ∈ sources(α, u))) ∧ (¬(null(α)))

⊃ step count2(α, u) > step count2(cdr(α), u)

intrans nonint tcc 79

Proof

run TCC1 PROOF: Prove run TCC1 sources TCC1 PROOF: Prove sources TCC1 sources TCC2 PROOF: Prove sources TCC2 sources TCC3 PROOF: Prove sources TCC3 ipurge TCC1 PROOF: Prove ipurge TCC1 ipurge TCC2 PROOF: Prove ipurge TCC2

End intrans nonint tcc intrans nonint tcc proofs: Module

Using intrans nonint, intrans nonint tcc Proof

run TCC1 PROOF: Prove run TCC1 from length cdr[A ] {ρ ← α} sources TCC1 PROOF: Prove sources TCC1 from length cdr[A ] {ρ ← α} sources TCC2 PROOF: Prove sources TCC2 from length cdr[A ] {ρ ← α} sources TCC3 PROOF: Prove sources TCC3 from length cdr[A ] {ρ ← α} purge TCC1 PROOF: Prove ipurge TCC1 from length cdr[A ] {ρ ← α} purge TCC2 PROOF: Prove ipurge TCC2 from length cdr[A ] {ρ ← α}

End intrans nonint tcc proofs

top 81

top: Module [T : Type] Using lists model[T ], lists model tcc[T ], lists map[T ],

lists map proofs[T ], intrans nonint tcc proofs

Proof

TCC proof: Prove car TCC1 from

nat invariant {nat var ← (ρ@c).nextpos}

End top