What,indeed,is intransitive noninterference? 1

Abstract

This paper argues that Haigh and Young’s definition of noninterference for intransitive security policies admits information flows that are not in accordance with the intuitions it seeks to formalize. Several alternative definitions are discussed, which are shown to be equivalent to the classical definition of noninterference with respect to transitive policies. Rushby’s unwinding conditions for intransitive noninterference are shown to be sound and complete for one of these definitions, TA-security. Access control systems compatible with a policy are shown to be TA-secure, and it is also shown that TA-security implies that the system can be interpreted as an access control system.

Keywords

Information flow noninterference access control verification

1. Introduction

The term ‘noninterference’ is used in the computer security literature to refer to formal definitions of information flow or causality between security domains. The classical theory of noninterference [15] dealt with transitive policies, which are closely related to partially ordered security levels. This theory is unable to deal with certain systems requiring channel control and downgrading [34]. To overcome these limitations, Haigh and Young [19] proposed a variant of the classical definition for channel control applications, which was formalized by Rushby [35] for intransitive policies more generally. In particular, Rushby established soundness of a proof technique based on “unwinding relations”, and also shows that a design discipline based on a class of systems, with access control on objects satisfying a simple static condition on reading and writing, guarantees satisfaction of the definition. The latter result is significant in that it can be understood as giving semantic content to ideas implicit in the approach of Bell and LaPadula [4], resolving questions concerning the meaning of that model [29].

Rushby’s results are cast in the setting of two deterministic state-based semantic models, resembling deterministic Moore and Mealy machines, with each security domain associated to its observations and a subset of the input alphabet. A number of authors have subsequently proposed generalizations and alternative definitions of intransitive noninterference in richer semantic frameworks, dealing with aspects such as nondeterminism, process algebraic models, programming language models and cryptographic concerns [3,5–7,17,25,26,33,43].

Of increasing prominence in recent years is an approach to secure systems construction based on minimalist operating systems kernels, whose principal functionality is the enforcement of a policy that constrains the information flow architecture. This has led to a number of secure systems verification efforts [20,22,27,39] in which noninterference style security policies have been proven to hold. Frequently these applied works are based in ideas from the work of Rushby [35], including intransitive policies and their connection to access control models. It is therefore of some significance that the theoretical foundations of intransitive noninterference be well-understood.

In this paper, we argue that this is not the case, even in the original formulation [19,35] in the setting of deterministic state machines. This formulation is based on an “intransitive purge” function, that has often been applied in subsequent work. We call the associated definition of security “IP-security”. We argue that IP-security classifies as secure some systems that contain subtle flows of information that are inappropriate in a secure system. In response, we propose alternative definitions that prohibit these flows. Moreover, we show that these alternatives lead to some very satisfying improvements of Rushby’s results concerning proof methods and connections to access control implementation mechanisms, provided we also make some intuitively well justified modifications of Rushby’s definitions of access control system.

We begin by arguing that IP-security is too weak for the intuitions it seeks to capture. We present an example that shows that it allows information to flow to an agent, that could not have come from the agents from which it is permitted to acquire information. The information concerns distinctions about the ordering of past events, which the intransitive purge definition is unable to capture.

This leads us to consider alternative definitions. We show that there is in fact a spectrum of different notions of noninterference for possibly intransitive policies, all having some intuitive plausibility, and all equivalent to the classical definition of Goguen and Meseguer [15] in the case of transitive policies. Our approach to definitions of security is to state that an agent should not have more information than the maximal amount it is permitted to have. This maximal amount of information is modelled by viewing actions as transmitting information within a concrete operational model. The notions differ in the information that may be transmitted by an action. Our principal focus in this paper is an instance of this approach, TA-security, which takes the view that an agent’s actions may transmit any information that it is permitted to have about previous actions.

We then study this new definition from the point of view of proof techniques and the application to access control systems. We begin with a discussion of “unwinding conditions”, which provide a proof technique for noninterference, but can be taken as a definition of security in their own right. Rushby proved that the classical unwinding conditions of Goguen and Meseguer provide a complete proof technique for noninterference in the transitive case. He proposes a weakening of these conditions for intransitive policies (correcting an earlier proposal by Haigh and Young [19]). He establishes soundness of the weakened unwinding conditions, but not completeness. We give an explanation of this: Rushby’s conditions are not complete for IP-security. Instead, they are sound and complete for the stronger notion of TA-security. There is a somewhat surprising subtlety in this statement: for completeness, the weakened unwinding conditions must be applied to the appropriate bisimilar system, but the existence of the weak unwindings is not preserved under bisimulation.

We also follow Rushby in considering access control systems, the class of applications originally motivating the literature on noninterference. Rushby showed that access control systems satisfying a condition of structural consistency with a policy satisfy IP-security. We argue that Rushby’s definition of access control systems can be weakened, and that access control systems consistent with a policy satisfy the stronger notion of TA-security as well as Haigh and Young’s definition of security. Moreover, we also show that TA-security implies that there is a way to interpret the system as an access control system in the weakened sense. This shows that TA-security is, in some sense, equivalent to the existence of an access control implementation of the system.

These results provide strong evidence that TA-security, rather than IP-security, best fits the original objectives for the notion of intransitive noninterference. The fact that three quite different, but all intuitive, interpretations of the meaning of intransitive noninterference coincide lends support to each.

The definition of TA-security is an instantiation of a general approach to the definition of security that compares a simple operational model of maximal permitted information flow in a system with the actual information flow in that system. Other instantiations are reasonable: we also consider some possible variants that we show to fall on a spectrum of definitions of security of increasing strength. The notion of TA-security takes the liberal view that an agent may transmit any information that it is permitted to have, even if it has not directly observed that information. (We remark that IP-security also has this property.) We also consider a notion of TO-security, which states that an agent may transmit only information that it has directly observed. This notion may well be equally significant for practical purposes. As evidence of this, we prove that access control systems structurally consistent with a policy also satisfy the stronger notion of TO-security, provided we work with an appropriate notion of observation for such systems. For purposes of comparison to related literature, we also characterize the relationship of these notions to the classical purge-based definition of Goguen and Meseguer [15], as well as a variant of TO-security that we call ITO-security. These notions can be shown to be related to definitions of Roscoe and Goldsmith [33].

The structure of the paper is as follows. Section 2 recalls Rushby’s formulation of IP-security, and Section 3 presents the example that shows a weakness of the definition. In Section 4 we introduce a new definition of noninterference for intransitive noninterference, TA-security, that avoids this weakness, and which forms the most satisfying basis for Rushby’s results concerning proof methods and access control. We substantiate this by establishing the connection to unwinding conditions in Section 5. Connections to access control systems are presented in Section 6. Some other definitions based on the general approach adopted in TA-security, and some results concerning these variants, are presented in Section 7. Section 8 discusses related work. We close in Section 9 with some remarks concerning issues requiring further investigation.

2. Intransitive noninterference

The notion of noninterference was first proposed by Goguen and Meseguer [15]. Early work on this area was motivated by multi-level secure systems, and dealt with deterministic systems and partially ordered (hence transitive) information flow policies. A significant body of work has developed since then, with a particular focus on generalization to the case of nondeterministic systems [14,28,36,40,44] and intransitive policies [3,5,6,25,33,35,43]. We focus in this paper on intransitive policies in the deterministic case.

Several different types of semantic models have been used in the literature on noninterference. (See [42] for a comparison and a discussion of their relationships.) We work here with the state-observed machine model used by Rushby [35], but similar results can be obtained for other models.2

²
In a companion paper [41] we also treat Rushby’s action-observed model, and show that the corresponding definitions in that model are related to those in the state-observed model by means of a natural mapping from action observed systems to state-observed systems.

This model consists of deterministic machines of the form

⟨ S, s_{0}, A, step, obs, dom ⟩

, where S is a set of states,

s_{0} \in S

is the initial state, A is a set of actions,

dom : A \to D

associates each action to an element of the set D of security domains,

step : S \times A \to S

is a deterministic transition function, and

obs : S \times D \to O

maps states to an observation in some set O, for each security domain. We may also refer to security domains more succinctly as “agents”. We write

s \cdot α

for the state reached by performing the sequence of actions

α \in A^{*}

from state s, defined inductively by

s \cdot ε = s

, and

s \cdot α a = step (s \cdot α, a)

for

α \in A^{*}

and

a \in A

. Here ε denotes the empty sequence.

Noninterference policies, as they are now usually presented,3

Goguen and Meseguer used a slightly richer notion.

are relations

↣ \subseteq D \times D

, with

u ↣ v

intuitively meaning that “actions of domain u are permitted to interfere with domain v”, or “information is permitted to flow from domain u to domain v”. Since, intuitively, a domain should be allowed to interfere with, or have information about, itself, this relation is assumed to be reflexive. In early work on noninterference, it is also assumed to be transitive.

Noninterference is given a formal semantics in the transitive case using a definition based on a “purge” function [15]. Given a set $E \subseteq D$ of domains and a sequence $α \in A^{*}$ , we write $α ↿ E$ for the subsequence of all actions a in α with $dom (a) \in E$ . Given a policy ↣, we define the function $purge : A^{*} \times D \to A^{*}$ by $purge (α, u) = α ↿ {v \in D ∣ v ↣ u} .$ (For clarity, we may use subscripting of agent arguments of functions, writing e.g., $purge (α, u)$ as ${purge}_{u} (α)$ .) The system M is said to be secure with respect to the transitive policy ↣ when for all $α \in A^{*}$ and domains $u \in D$ , we have ${obs}_{u} (s_{0} \cdot α) = {obs}_{u} (s_{0} \cdot {purge}_{u} (α))$ . That is, each agent’s observations are as if only interfering actions had been performed. An equivalent formulation (which we state more generally for policies that are not necessarily transitive, in anticipation of later discussion) is the following definition.

Definition 1.

A system M is P-secure with respect to a policy ↣ if for all sequences $α, α^{'} \in A^{*}$ such that ${purge}_{u} (α) = {purge}_{u} (α^{'})$ , we have ${obs}_{u} (s_{0} \cdot α) = {obs}_{u} (s_{0} \cdot α^{'})$ .

This can be understood as saying that agent u’s observation depends only on the sequence of interfering actions that have been performed. Equivalence of the two definitions follows from the following simple proposition.

Proposition 1.

Suppose that p and o are two functions with domain a set X and p also has codomain X. If p is idempotent then the following are equivalent:(1) $o (α) = o (p (α))$ for all $α \in X$ , and (2) for all $α, α^{'} \in X$ , if $p (α) = p (α^{'})$ then $o (α) = o (α^{'})$ .

Proof.

Assume (1). Then for all $α, α^{'} \in X$ , if $p (α) = p (α^{'})$ then $o (α) = o (p (α)) = o (p (α^{'})) = o (α^{'})$ . Thus (2) also holds. Conversely, suppose (2). Since p is idempotent, we have $p (α) = p (p (α))$ for all $α \in X$ . Taking $α^{'} = p (α)$ , we obtain from (2) that $o (α) = o (p (α))$ , as required for (1). □

Example 1.

To illustrate a typical application of the semantic model and the motivation for noninterference definitions of security, consider a highly simplified model for two processes $P_{0}$ , $P_{1}$ sharing a CPU or cache (which provides more rapid access to data for operations than would be possible if it were necessary to read and write from main memory).

The security policy requires that the two processes be completely isolated, so that there is no flow of information between them. Thus, we have $D = {P_{0}, P_{1}}$ and the policy is the identity relation $↣ = {(P_{0}, P_{0}), (P_{1}, P_{1})}$ . We take a memory value to consist of a single bit, and the only operations are bit complementation and writing a bit to an output device associated to the process.

We take the states S of the system to be the set of boolean assignments to the following variables: $m_{0}$ , $m_{1}$ , representing main memory data locations associated to $P_{0}$ , $P_{1}$ , respectively, c, representing the cache value, $own$ , representing the owner of the cache value (either 0 or 1 for $P_{0}$ , $P_{1}$ , respectively), and ${out}_{0}$ , ${out}_{1}$ , representing output lines for $P_{0}$ , $P_{1}$ , respectively. For the initial state, we take all variables to have value 0. We assume that the processes can observe only the value on their output device. Thus, in a state s, we take ${obs}_{P_{i}} (s) = s ({out}_{i})$ .

We have actions $A = {{comp}_{0}, {comp}_{1}, {output}_{0}, {output}_{1}}$ with $dom ({comp}_{i}) = dom ({output}_{i}) = P_{i}$ . Here ${comp}_{i}$ is, intuitively, the action of process $P_{i}$ complementing its bit, and ${output}_{i}$ is the action of process $P_{i}$ writing its memory value to its associated output line. State transitions associated to each of these actions are given by the following code (which runs atomically): $\begin{array}{rcl} {comp}_{i} : if own = i then c : = \bar{c} else {m_{\bar{i}} : = c; c : = m_{i}; own : = i; c : = \bar{c}}, \\ {output}_{i} : if own = i then {out}_{i} : = c else {out}_{i} : = m_{i} . \end{array}$ Note that the code prefers to use the fast memory c rather than the slow memory $m_{i}$ . The two processes share the fast memory c, so the implementation needs to take care to ensure that this sharing does not cause leakage of information from one process to another. This is done by carefully tracking, using the variable $own$ , which process’s information is currently in the cache, and ensuring that another process’s value is not written to an process’s output device when the cache line is used. When process $P_{i}$ performs an operation ${comp}_{i}$ , and the other process’s value is in the cache, that other value is first written back to main memory, and then $P_{i}$ ’s value is loaded into the cache and complemented.

It is not difficult to see that this system is P-secure. Intuitively, the output values ${obs}_{P_{i}} (s)$ observed by process $P_{i}$ depend only on the actions that process $P_{i}$ has performed, and are independent of the actions performed by the other process. (We note that the assumption of asynchrony of the processes is critical to this conclusion: it is known that timing information can be responsible for covert channels in a shared cache [32].) The type of resource sharing illustrated by this example is extremely common, particularly in hardware designs, and a satisfactory account of security for such designs needs to accommodate it.

It was recognized already by Goguen and Meseguer [16] that transitive policies are insufficiently expressive to handle situations involving channel control or downgrading. The following example illustrates the issues in such settings.

Example 2.

A system involving a downgrader is given by the set of domains $D = {H, D, L}$ and policy $H ↣ D$ and $D ↣ L$ . Intuitively, H is a High level domain, L a Low level domain, and D represents the downgrader, which makes decisions concerning the release of information from H to L. Note that the policy is not transitive, since we do not have $H ↣ L$ , which would follow from the above facts if the policy were transitive. The intuitive reading of this is that it is not permitted for H actions to have a direct effect on L, i.e., it should not be possible for H to pass information to L of its own accord. However, the policy does allow that H information may be transmitted to L, so long as such transmission is effected by D.

Consider the concrete system M with actions $A = {h, d}$ where $dom (h) = H$ and $dom (d) = d$ , and states S consisting of assignments to the boolean variables $x_{H}$ and $x_{L}$ . The initial state has both variables equal to 0. We assume that ${obs}_{H} (s) = s (x_{H})$ , ${obs}_{D} (s) = s (x_{H})$ and ${obs}_{L} (s) = s (x_{L})$ for all states s. The semantics of the actions is given by the code $\begin{array}{rcl} h : x_{H} : = 1, \\ d : x_{L} : = x_{H} . \end{array}$ One can understand these definitions as stating that the variable $x_{H}$ records whether or not there has been an occurrence of action h, and d transmits this information to the variable $x_{L}$ .

Intuitively, the system M is secure with respect to the policy ↣. The action h has no direct effect on the variable $x_{L}$ that is observed by L. The variable $x_{L}$ is affected by action d, but this action is consistent with the policy, because domain D is both permitted to receive information from H and transmit information to L.

On the other hand, note that ${purge}_{L} (d) = {purge}_{L} (h d) = d$ , but ${obs}_{L} (s_{0} \cdot d) = 0 \neq 1 = {obs}_{L} (s_{0} \cdot h d)$ . This means the system M is not P-secure with respect to the policy ↣. Intuitively, P-security permits L observations to depend only on the actions of D and L. This means that it prohibits D from transmitting H information to L, as the policy is intended to allow. This suggests that P-security is not the appropriate semantics to apply to intransitive policies.

In order to address such examples, Haigh and Young [19] generalized the definition of the purge function to intransitive policies as follows (we present the formalization of [35]). Intuitively, the intransitive purge of a sequence of actions with respect to a domain u is the largest subsequence of actions that could form part of a causal chain of effects (permitted by the policy) ending with an effect on domain u. More formally, the definition makes use of a function $sources : A^{*} \times D \Rightarrow P (D)$ defined inductively by $sources (ε, u) = {u}$ and $sources (a α, u) = sources (α, u) \cup {dom (a) ∣ \exists v \in sources (α, u) (dom (a) ↣ v)}$ for $a \in A$ and $α \in A^{*}$ . Intuitively, $sources (α, u)$ is the set of domains v such that there exists a sequence of permitted interferences from v to u within α. The intransitive purge function $ipurge : A^{*} \times D \to A^{*}$ is then defined inductively by $ipurge (ε, u) = ε$ and $ipurge (a α, u) = \{\begin{matrix} a \cdot ipurge (α, u) & if dom (a) \in sources (a α, u), \\ ipurge (α, u) & otherwise \end{matrix}$ for $a \in A$ and $α \in A^{*}$ . An alternative, equivalent formulation that we will find useful is the following: given a set $X \subseteq D$ , define ${ipurge}_{X} (α)$ inductively by ${ipurge}_{X} (ε) = ε$ and ${ipurge}_{X} (α a) = \{\begin{matrix} {ipurge}_{X \cup {dom (a)}} (α) \cdot a & if \exists u \in X (dom (a) ↣ u), \\ {ipurge}_{X} (α) & otherwise. \end{matrix}$ Then ${ipurge}_{u} (α)$ is identical to ${ipurge}_{{u}} (α)$ . Haigh and Young’s definition of security uses the intransitive purge function in place of the purge function in Goguen and Meseguer’s definition: M is secure with respect to a policy ↣ if for all sequences $α \in A^{*}$ , and $u \in D$ , we have ${obs}_{u} (s_{0} \cdot α) = {obs}_{u} (s_{0} \cdot {ipurge}_{u} (α))$ . Since the function ${ipurge}_{u}$ on $A^{*}$ is idempotent, this definition, like the definition for the transitive case, can, by Proposition 1, be equivalently formulated as the following definition.

Definition 2.

A system M is IP-secure with respect to a (possibly intransitive) policy ↣ if for all $u \in D$ and all sequences $α, α^{'} \in A^{*}$ with ${ipurge}_{u} (α) = {ipurge}_{u} (α^{'})$ , we have ${obs}_{u} (s_{0} \cdot α) = {obs}_{u} (s_{0} \cdot α^{'})$ .

It can be seen that ${ipurge}_{u} (α) = {purge}_{u} (α)$ when ↣ is transitive, so IP-security is in fact a generalization of the definition of security for transitive policies.

Example 3.

Reconsider the system of Example 2. This system can be shown to be IP-secure. For example, considering the particular sequences of actions d and $h d$ discussed above, we have ${ipurge}_{L} (d) = d \neq h d = {ipurge}_{L} (h d)$ , so the fact that the observations made by L after these sequences of actions differ no longer implies that the definition of security fails.

It is worth noting that both P-security and IP-security have the property that reducing the amount of information in the observations of a system preserves security. To state this precisely, say that a system $M^{'}$ is an observation–abstraction of system M if these systems are identical, except for their respective observation functions ${obs}_{u}^{'}$ and ${obs}_{u}$ , respectively, for domains u, and there exist functions $f_{u}$ such that ${obs}_{u}^{'} = f_{u} \circ {obs}_{u}$ . Intuitively, a larger set of states is consistent with each observation in the system $M^{'}$ , so the observations in this system carry less information, i.e., the agents know less. Say that a notion of security is preserved under observation abstraction, if for all systems M and $M^{'}$ , if M is secure and $M^{'}$ is an observation abstraction of M, then $M^{'}$ is also secure. If we take the point of view that security is concerned with secrecy, and that a system is secure if no agent knows more than it is entitled to know, it seems like a reasonable requirement on a definition of security that it be preserved under observation abstraction. Since ${purge}_{u} (α)$ and ${ipurge}_{u} (α)$ are unaffected by observation abstraction, it is immediate from the definitions that both P-security and IP-security are preserved under observation abstraction.

Example 4.

Consider the system $M^{'}$ obtained from the system M of Example 2 by applying the abstraction functions $f_{u}$ where $f_{H}$ and $f_{L}$ are the identity functions on observations and $f_{D}$ is the function that maps every observation to ⊥. That is, the only change is to take ${obs}_{D}^{'} (s) = ⊥$ for all states s in this example. In the system $M^{'}$ , the action d of agent D still causes information about H’s actions to flow to L, but D’s own observations now carry no information about the actions performed by H. This variant remains IP-secure. Intuitively, IP-security requires just that D was causally involved in all flows of information from H to L. It does not require that D explicitly observes or “knows” the information that its actions are causing to be transmitted to L.

It is reasonable to object that one expects a downgrader to be responsible and first inspect the information that it releases. We return to this point below, but, for the moment focus on the “causal” intuition for intransitive policies that the notion of IP-security attempts to formalize.

3. An example

We now present an example that points to a potential weakness of IP-security as the semantics of intransitive policies. Note that the intransitive purge ${ipurge}_{u} (α)$ preserves not just certain actions from the sequence α, but also their order. We claim that this allows u to “know” this order in situations where an intuitive reading of the policy would suggest that it ought not to know this order.

To give precise content to this claim, we introduce some notation from the literature on modal logics of knowledge [13]. Let $Prop$ be a set of atomic propositions. We define a propositional modal logic, with formulas defined as follows: if $p \in Prop$ then p is formula, and if ϕ and ψ are formulas and $u \in D$ is an agent and $G \subseteq D$ is a nonempty set of agents then $\neg ϕ$ , $ϕ \lor ψ$ and $K_{u} ϕ$ and $D_{G} ϕ$ are formulas. We use standard boolean abbreviations such as $ϕ \Rightarrow ψ$ for $\neg ϕ \lor ψ$ . Intuitively, the formula $K_{u} ϕ$ expresses that agent u knows ϕ, and $D_{G} ϕ$ expresses that ϕ is distributed knowledge to the group G, which means that the group G, collectively, knows ϕ.

We take the atomic propositions to be interpreted over sequences of actions of a system M with actions A, by means of an interpretation function $π : Prop \to P (A^{*})$ . Formulas ϕ are then interpreted as being satisfied at a sequence of actions $α \in A^{*}$ by means of a relation $M, π, α ⊨ ϕ$ . For atomic propositions $p \in Prop$ , this relation is defined by $M, π, α ⊨ p$ if $α \in π (p)$ .

The semantics of the operators for knowledge can be defined in a variety of ways, depending on questions such as the degree of recall and synchrony of the agents. It is appropriate in applications of the logic of knowledge to security to use a perfect recall interpretation of knowledge. An attacker with perfect memory is stronger than a forgetful attacker, so is the better assumption for security analysis. However, the semantics for noninterference are asynchronous. We therefore use an asynchronous model of the information available to the attacker. Concretely, this can be represented using the following notion of view. The definition uses an absorptive concatenation function ∘, defined over a set X by, for $s \in X^{*}$ and $x \in X$ , by $s \circ x = s$ if x is equal to the final element of s (if any), and $s \circ x = s x$ (ordinary concatenation) otherwise.

Define the view of domain u with respect to a sequence $α \in A^{*}$ using the function ${view}_{u} : A^{*} \to {(A \cup O)}^{*}$ (where O is the set of observations in the system) defined by ${view}_{u} (ε) = {obs}_{u} (s_{0})$ and ${view}_{u} (α a) = \{\begin{matrix} {view}_{u} (α) a {obs}_{u} (s_{0} \cdot α a) & if dom (a) = u, \\ {view}_{u} (α) \circ {obs}_{u} (s_{0} \cdot α a) & otherwise . \end{matrix}$ That is, ${view}_{u} (α)$ is the sequence of all observations and actions of domain u in the run generated by α, compressed by the elimination of stuttering observations. Intuitively, ${view}_{u} (α)$ is the complete record of information available to agent u in the run generated by the sequence of actions α. The reason we apply the absorptive concatenation is to capture that the system is asynchronous, with agents not having access to a global clock. Thus, two periods of different length during which a particular observation obtains are not distinguishable to the agent.

Using the notion of view, we may define for each agent u an equivalence relation $\equiv_{u}$ on sequences of actions by $α \equiv_{u} α^{'}$ if ${view}_{u} (α) = {view}_{u} (α^{'})$ . The semantics for the knowledge operators may then be given by $M, π, α ⊨ K_{u} ϕ if M, π, α^{'} ⊨ ϕ for all sequences α^{'} such that α \equiv_{u} α^{'} .$ This is essentially the definition of knowledge used in the literature on reasoning about knowledge [13] for an agent with asynchronous perfect recall.

The semantics of distributed knowledge is defined in the literature as follows. First, define the relations $\equiv_{G}$ on sequences of actions by $α \equiv_{G} α^{'}$ if $α \equiv_{u} α^{'}$ for all $u \in G$ . The operators $D_{G}$ are then given semantics by the clause $M, π, α ⊨ D_{G} ϕ if M, π, α^{'} ⊨ ϕ for all sequences α^{'} such that α \equiv_{G} α^{'} .$ Intuitively, this definition says that a fact is distributed knowledge to the set of agents G if it could be deduced after combining all the information that these agents have. While this semantics is satisfactory in synchronous settings, we will see below that a different notion of group knowledge is appropriate for our application. For a group $G \subseteq D$ , define the modal operator $D_{G}^{*}$ , with semantics given by $M, π, α ⊨ D_{G}^{*} ϕ if M, π, α^{'} ⊨ ϕ for all sequences α^{'} such that α \equiv_{G} α^{'} and α ↿ G = α^{'} ↿ G .$ Note that $α \equiv_{G} α^{'}$ already implies that α and $α^{'}$ contain the same actions for each of the members of the group G, but, because of asynchrony, these actions may be interleaved in different ways in the two sequences. The additional content of the statement $α ↿ G = α^{'} ↿ G$ is therefore that these actions are interleaved in the same way in the two sequences. Intuitively, $D_{G}^{*} ϕ$ captures that the group G would know ϕ if it were to combine all the information available to the members, with the additional information about how their actions were interleaved.

We may now present our example illustrating a weakness of IP-security. The essence of the example is that IP-security is consistent with an agent acquiring information that it could not have received from the agents from which it is permitted (by an intransitive policy) to acquire information.

Fig. 1.

An intransitive policy.

Example 5.

Consider the intransitive policy ↣ given by $H_{1} ↣ D_{1}$ , $H_{2} ↣ D_{2}$ , $D_{1} ↣ L$ and $D_{2} ↣ L$ . The policy is depicted in Fig. 1. Intuitively, $H_{1}$ , $H_{2}$ are two High security domains, $D_{1}$ , $D_{2}$ are two downgraders, and L is an aggregator of downgraded information. For this policy, channel control, one of the motivations for intransitive noninterference, requires that any information about $H_{1}$ and $H_{2}$ available to L must have reached L via the downgraders $D_{1}$ and $D_{2}$ . The policy disallows direct flows of information from $H_{1}$ or $H_{2}$ to L, but allows L to combine pieces of information it has received from $D_{1}$ and $D_{2}$ . A seemingly reasonable way to capture this requirement more formally is to interpret it as stating that if M is a system that is secure with respect to this policy and π interprets the atomic proposition p as expressing some property depending only on the behaviour of $H_{1}$ and $H_{2}$ , then we should have $M, π, α ⊨ K_{L} p \Rightarrow D_{{D_{1}, D_{2}}} p$ for all $α \in A^{*}$ . That is, if a fact about $H_{1}$ , $H_{2}$ is known to L, then it follows from combining information that is available to $D_{1}$ , $D_{2}$ . The process of combination is interpreted using the distributed knowledge operator. This suggests that if some information has been implicitly released, then the downgraders could, after combining their information, know that this is the case. Such an ability would be beneficial from the point of view of audit requirements on the system.

Some caveats on this interpretation of the informal requirement are in order, however. First, we might note that L is potentially allowed by the policy to have more information than the distributed knowledge of the downgraders. It may be possible for L to directly observe the occurrence of the downgrader actions, and consequently know how these actions are interleaved. For our asynchronous semantics for knowledge, this interleaving is not distributed knowledge to the downgraders. This suggests that the way the information known to the downgraders is aggregated, when it is transmitted to L, should be captured by the alternative distributed knowledge operator $D_{G}^{*}$ , which also takes into account the interleaving of actions that is potentially observable to L. This gives the refined requirement $M, π, α ⊨ K_{L} p \Rightarrow D_{{D_{1}, D_{2}}}^{*} p$ (1) for propositions p that are interpreted by π as depending only on ${H_{1}, H_{2}}$ .

Next, as we have already noted above in Example 4, IP-security does not require that information transmitted by a downgrader be explicitly observable to the downgrader. IP-security merely places an upper bound on the information content of the observations of the agents, and reducing the information content of an agent’s observations preserves IP-security. Since a downgrader’s knowledge is based on its observations, this means that it does not necessarily know what information it has caused to be transmitted, even if the system is secure. We may address this concern by concentrating on systems in which the agents make the maximally informative observations that are consistent with security. In the case of IP-security, this means that after sequence of actions α, we let agent u observe ${ipurge}_{u} (α)$ after sequence α. We may expect that in such a system, we have a more direct correspondence between information possessed by agents and information that they may transmit, so that the epistemic formulation (1) captures the intended requirement.

We now show that if security is interpreted as IP-security, and we work in a system where agents make their maximally informative observation, then condition (1) does not necessarily follow from security of the system, as we might expect.

Define the system M with actions $A = {h_{1}, h_{2}, d_{1}, d_{2}, l}$ with domains $H_{1}$ , $H_{2}$ , $D_{1}$ , $D_{2}$ and L, respectively. The set of states of M is the set of all strings in $A^{*}$ . The transition function is defined by concatenation, i.e. for a state $α \in A^{*}$ and an action $a \in A$ , $step (α, a) = α a$ . The observation functions are defined to be the maximally informative observations consistent with security: using the intransitive purge function associated to the above policy, we define ${obs}_{u} (α) = [ipurge (α, u)]$ . (Here we put brackets around the sequence of actions when it is interpreted as an observation, to distinguish such occurrences from the actions themselves as they occur in a view.)

An intuitive reading of this system is that it represents an operating system that maintains a log of all operations performed by users. In each state, the operating system permits each user to observe just that part of the log that IP-security permits the user to have information about.

It is plain that M is IP-secure. For, if $ipurge (α, u) = ipurge (α^{'}, u)$ then ${obs}_{u} (s_{0} \cdot α) = [ipurge (α, u)] = [ipurge (α^{'}, u)] = {obs}_{u} (s_{0} \cdot α^{'})$ . We show that it does not satisfy condition (1).

Consider the sequences of actions $α_{1} = h_{1} h_{2} d_{1} d_{2}$ and $α_{2} = h_{2} h_{1} d_{1} d_{2}$ . Note that these differ in the order of the events $h_{1}$ , $h_{2}$ . Let the atomic proposition p be interpreted by π as asserting that there is an occurrence of $h_{1}$ before an occurrence of $h_{2}$ . That is, $π (p) = {α h_{1} β h_{2} γ ∣ α, β, γ \in A^{*}}$ .

Then we have ${obs}_{L} (α_{1}) = [ipurge (α_{1}, L)] = [h_{1} h_{2} d_{1} d_{2}]$ . Hence, for any sequence $α^{'}$ with $α_{1} \equiv_{L} α^{'}$ , we have ${ipurge}_{L} (α^{'}) = h_{1} h_{2} d_{1} d_{2}$ , so $α^{'} \in π (p)$ . Thus $M, π, α_{1} ⊨ K_{L} p$ , i.e., in $α_{1}$ agent L knows the ordering of the events $h_{1}$ , $h_{2}$ . We demonstrate that $α_{2}$ is a witness showing that it is not the case that $M, π, α_{1} ⊨ D_{{D_{1}, D_{2}}}^{*} p$ , i.e., we have $α_{1} \equiv_{{D_{1}, D_{2}}} α_{2}$ and $α_{1} ↿ {D_{1}, D_{2}} = α_{2} ↿ {D_{1}, D_{2}}$ and $α_{2} \notin π (p)$ . It is trivial that $α_{2} \notin π (p)$ , and plainly $α_{1} ↿ {D_{1}, D_{2}} = d_{1} d_{2} = α_{2} ↿ {D_{1}, D_{2}}$ .

For $α_{1} \equiv_{{D_{1}, D_{2}}} α_{2}$ , note $\begin{array}{rcl} {view}_{D_{1}} (α_{1}) \\ = {obs}_{D_{1}} (ε) \circ {obs}_{D_{1}} (h_{1}) \circ {obs}_{D_{1}} (h_{1} h_{2}) \circ d_{1} \circ {obs}_{D_{1}} (h_{1} h_{2} d_{1}) \circ {obs}_{D_{1}} (h_{1} h_{2} d_{1} d_{2}) \\ = [ε] \circ [h_{1}] \circ [h_{1}] \circ d_{1} \circ [h_{1} d_{1}] \circ [h_{1} d_{1}] \\ = [ε] \circ [ε] \circ [h_{1}] \circ d_{1} \circ [h_{1} d_{1}] \circ [h_{1} d_{1}] \\ = {obs}_{D_{1}} (ε) \circ {obs}_{D_{1}} (h_{2}) \circ {obs}_{D_{1}} (h_{2} h_{1}) \circ d_{1} \circ {obs}_{D_{1}} (h_{2} h_{1} d_{1}) \circ {obs}_{D_{1}} (h_{2} h_{1} d_{1} d_{2}) \\ = {view}_{D_{1}} (α_{2}) \end{array}$ i.e., $α_{1} \equiv_{D_{1}} α_{2}$ . (Evidently, the view contains some information redundantly, but it naturally represents the information that agent $D_{1}$ may have collected over time by recording its own actions as well as the results of inspecting its observable part of the system log.) By symmetry, we also have $α_{1} \equiv_{D_{2}} α_{2}$ , hence $α_{1} \equiv_{{D_{1}, D_{2}}} α_{2}$ . This means that $D_{1}$ and $D_{2}$ do not have distributed knowledge of the ordering of the events $h_{1}$ , $h_{2}$ , even with respect to the asynchronous perfect recall interpretation of knowledge, in which they reason based on everything that they learn in the run.

Thus, L has acquired information that cannot have come from the two sources $D_{1}$ and $D_{2}$ that are supposed to be, according to the policy, its only sources of information.

Although the information flow identified in this example is troubling, it is not clear whether we have identified an exploitable avenue for attack. There are many questions raised. For one, is $D_{G}^{*}$ the appropriate model for the information that flows through a group of agents, and is it appropriate to apply this notion to the downgrading setting as we have done? Does it matter for security of the system if information about the ordering of events in independent domains leaks? Reliable transmission of information to L using the channel we have identified would seem to require $H_{1}$ and $H_{2}$ to collude, but since they are not permitted by the policy to communicate, it is unclear how they could do so. If they do collude, e.g., through a channel outside the scope of the system, does this require them to communicate using a synchronous mechanism, something that is not in the spirit of our asynchronous semantics? One might argue that it is unreasonable to expect that asynchronous defenders can secure a system against synchronous attackers. On the other hand, one potential reason for worrying about this is that there may be attacks in which an agent exploits side channels through the system scheduler.

At the very least, the example suggests that there is something troubling about the flows of information that are permitted by IP-security. We might just as well turn this around on the definition of IP-security itself. Historically, the definition was derived as a modification of the definition of P-security, motivated by problem with that definition identified in Example 2. The definition correctly handles that example, but beyond this, there does not seem to be a compelling explanation for why it is appropriate to take ${ipurge}_{u} (α)$ to be a representation of the maximal information that u is permitted to have after the sequence of actions α.

4. An alternative definition: TA-security

As a response to Example 5, we will consider several alternative definitions of security for intransitive policies. Like IP-security, each is based on a concrete model of the maximal amount of information that an agent may have after some sequence of actions has been performed, and states that an agent’s observation may not give it more than this maximal amount of information. Our definitions take the view that an agent increases its information either by performing an action or by receiving information transmitted by another agent. They differ in the choice of what information is permitted to be transmitted when an agent performs an action. In this section, we focus on one of these alternative definitions (the others are discussed in Section 7). The results of the following sections will show that this new definition proves to be more closely related than IP-security itself to the results that Rushby established about IP-security.

In our first definition, what is transmitted when an agent performs an action is information about the actions performed by other agents. The following definition expresses this in a weaker way than the $ipurge$ function.

Given sets X and A, let $T (X, A)$ be the smallest set containing X and such that if $x, y \in T (X, A)$ and $z \in A$ then $(x, y, z) \in T (X, A)$ . Intuitively, the elements of $T (X, A)$ are binary trees with leaves labelled from X and interior nodes labelled from A.

Given a policy ↣, define, for each agent $u \in D$ , the function ${ta}_{u} : A^{*} \to T ({ε}, A)$ inductively by ${ta}_{u} (ε) = ε$ , and, for $α \in A^{*}$ and $a \in A$ , ${ta}_{u} (α a) = \{\begin{matrix} {ta}_{u} (α) & when dom (a) ↣̸ u, \\ ({ta}_{u} (α), {ta}_{dom (a)} (α), a) & otherwise . \end{matrix}$ Intuitively, ${ta}_{u} (α)$ captures the maximal information that agent u may, consistently with the policy ↣, have about the past actions of other agents. (The nomenclature is intended to be suggestive of transmission of information about actions.) Initially, an agent has no information about what actions have been performed.

The recursive clause describes how the maximal information ${ta}_{u} (α)$ permitted to u after the performance of α changes when the next action a is performed. If a may not interfere with u, then there is no change to the information u is permitted to have. This is as one expects, since u is not permitted by the policy to know about events in domain $dom (a)$ , and in particular, is not permitted to know about the occurrence of the action a. Otherwise, if $dom (a) ↣ u$ , then u is permitted to know about events in domain $dom (a)$ . In this case, we allow u’s information to increase as a result of the performance of action a. Intuitively, the action a in this case transmits new information to u, which is added to the information ${ta}_{u} (α)$ that u already had. In particular, we add the maximal information permitted to $dom (a)$ at the time a is performed (represented by ${ta}_{dom (a)} (α)$ ), as well the fact that a has been performed.

Thus, this definition captures the intuition that an agent may only transmit information that it is permitted to have, and then only to agents with which it is permitted to interfere. When an agent transmits information to another, it transmits everything that it knows, as well as the name of the action that it performs, which is responsible for the information transmission. We remark that the definition and intuitions for the functions ${ta}_{u}$ are somewhat similar to the notion of full-information protocol [31] that is used in the distributed algorithms literature.

Definition 3.
A system M is TA-secure with respect to a policy ↣ if for all agents u and all $α, α^{'} \in A^{*}$ such that ${ta}_{u} (α) = {ta}_{u} (α^{'})$ , we have ${obs}_{u} (s_{0} \cdot α) = {obs}_{u} (s_{0} \cdot α^{'})$ .

Intuitively, this definition says that each agent’s observations provide the agent with no more information than the maximal amount that may have been transmitted to it, as expressed by the functions $ta$ .
Example 6.
Note that the system of Example 5 is not TA-secure. For, $\begin{array}{rcl} {ta}_{L} (h_{1} h_{2} d_{1} d_{2}) & = & ({ta}_{L} (h_{1} h_{2} d_{1}), {ta}_{D_{2}} (h_{1} h_{2} d_{1}), d_{2}) \\ = & (({ta}_{L} (h_{1} h_{2}), {ta}_{D_{1}} (h_{1} h_{2}), d_{1}), {ta}_{D_{2}} (h_{1} h_{2}), d_{2}) \\ = & (({ta}_{L} (h_{1}), {ta}_{D_{1}} (h_{1}), d_{1}), ({ta}_{D_{2}} (h_{1}), {ta}_{H_{2}} (h_{1}), h_{2}), d_{2}) \\ = & ((ε, (ε, ε, h_{1}), d_{1}), (ε, ε, h_{2}), d_{2}) \end{array}$ and $\begin{array}{rcl} {ta}_{L} (h_{2} h_{1} d_{1} d_{2}) & = & ({ta}_{L} (h_{2} h_{1} d_{1}), {ta}_{D_{2}} (h_{2} h_{1} d_{1}), d_{2}) \\ = & (({ta}_{L} (h_{2} h_{1}), {ta}_{D_{1}} (h_{2} h_{1}), d_{1}), {ta}_{D_{2}} (h_{2} h_{1}), d_{2}) \\ = & (({ta}_{L} (h_{1}), ({ta}_{D_{1}} (h_{2}), {ta}_{H_{1}} (h_{2}), h_{1}), d_{1}), {ta}_{D_{2}} (h_{2}), d_{2}) \\ = & ((ε, (ε, ε, h_{1}), d_{1}), (ε, ε, h_{2}), d_{2}) . \end{array}$ So ${ta}_{L} (h_{1} h_{2} d_{1} d_{2}) = {ta}_{L} (h_{2} h_{1} d_{1} d_{2})$ , but ${obs}_{L} (h_{1} h_{2} d_{1} d_{2}) = [h_{1} h_{2} d_{1} d_{2}] \neq [h_{2} h_{1} d_{1} d_{2}] = {obs}_{L} (h_{2} h_{1} d_{1} d_{2})$ . This illustrates that TA-security is in accordance with our intuitions about Example 5.

Plainly, the term ${ta}_{u} (α)$ grows rapidly in size as the sequence α becomes longer, and it also appears to contain a large amount of redundancy. One might wonder whether a more succinct representation is possible. We will not pursue this question here – similar questions arise in the use of the full information protocol methodology in the distributed algorithms literature, where one is interested in identifying data structures that more efficiently capture the information relevant to protocol goals. The solutions to such questions can be quite nontrivial [13]. What matters to us here is that the functions ${ta}_{u}$ correspond to a very plausible representation of how information maximally flows around the system as agents that comply with the security policy transmit information to each other by performing actions.
5. Unwinding relations

In this section we relate TA-security to “unwinding conditions” that have been discussed in the literature as a way to prove noninterference [16]. We show that Rushby’s proposed unwinding conditions for intransitive noninterference are closely related to TA-security in that they provide a sound and complete proof method for this definition of security. We also show the somewhat surprising fact that Rushby’s unwinding conditions are not preserved under bisimulation.

We begin by recalling Rushby’s results on unwinding for intransitive noninterference. Suppose we have for each domain u an equivalence relation $\sim_{u}$ on the states of M. Rushby discusses the following “unwinding” conditions on such equivalence relations.

OC: If $s \sim_{u} t$ then ${obs}_{u} (s) = {obs}_{u} (t)$ . (Output consistency)

SC: If $s \sim_{u} t$ then $s \cdot a \sim_{u} t \cdot a$ . (Step consistency)

LR: If $dom (a) ↣̸ u$ then $s \sim_{u} s \cdot a$ . (Locally respects)

If these conditions are satisfied and ↣ is a transitive policy, then M is P-secure [16]. Conversely, consider the particular equivalence relations

\approx_{u}

on states, defined by

s \approx_{u} t

if for all strings α in

A^{*}

we have

{obs}_{u} (s \cdot α) = {obs}_{u} (t \cdot α)

. Rushby uses these equivalence relations to show completeness of the unwinding conditions for transitive noninterference:

Proposition 2 ([35, Theorem 6]).

Suppose M is P-secure with respect to the transitive policy ↣. Then the relations $\approx_{u}$ satisfy OC, SC and LR.

For intransitive noninterference he introduces the following condition:

WSC: If $s \sim_{u} t$ and $s \sim_{dom (a)} t$ then $s \cdot a \sim_{u} t \cdot a$ . (Weak step consistency)

Define a weak unwinding on a system M with respect to a policy ↣ to be a family of relations

\sim_{u}

, for

u \in D

, satisfying OC, WSC and LR. It will be convenient to have the following alternate characterization of this notion. Given a system M and a policy ↣, let

{\approx_{u}^{u w}}_{u \in D}

be the smallest family of equivalence relations (under the pointwise containment order) satisfying WSC and LR.

Proposition 3.
There exists a weak unwinding for M with respect to ↣ iff the relations $\approx_{u}^{u w}$ satisfy OC.
Proof.
The implication from right to left is trivial. For the implication from left to right, suppose that ${\sim_{u}}_{u \in D}$ is a weak unwinding for M with respect to ↣. It is immediate from the definition of $\approx_{u}^{u w}$ and fact that the property of being an equivalence relation satisfying WSC and LR is defined by Horn formulas that $\approx_{u}^{u w} \subseteq \sim_{u}$ . The fact that $\sim_{u}$ satisfies OC now implies that $\approx_{u}^{u w}$ satisfies OC. □

Rushby shows the following proposition.
Proposition 4 ([35, Theorem 7]).

Suppose that the relations ${\sim_{u}}_{u \in D}$ on a system M satisfy OC, WSC and LR. Then M is IP-secure for ↣ .

However, he does not establish completeness of these unwinding conditions for IP-security. The following result yields an explanation of this fact.

Theorem 1.
Suppose that there exists a weak unwinding for M with respect to ↣. Then M is TA-secure with respect to ↣ .
Proof.
Let the weak unwinding be ${\sim_{u}}_{u \in D}$ . We show that for $u \in D$ and $α, α^{'} \in A^{}$ , if ${ta}_{u} (α) = {ta}_{u} (α^{'})$ then $s_{0} \cdot α \sim_{u} s_{0} \cdot α^{'}$ . By OC, it also follows that ${obs}_{u} (s_{0} \cdot α) = {obs}_{u} (s_{0} \cdot α^{'})$ , which is what we need for TA-security. We proceed by induction on $| α | + | α^{'} |$ . The base case of $α = α^{'} = ε$ is trivial. Supposing that the result holds for sequences of shorter combined length, consider sequences $α a$ and $α^{'}$ , where $a \in A$ and ${ta}_{u} (α a) = {ta}_{u} (α^{'})$ .

If $dom (a) ↣̸ u$ , then ${ta}_{u} (α) = {ta}_{u} (α a) = {ta}_{u} (α^{'})$ . Hence, by induction, $s_{0} \cdot α \sim_{u} s_{0} \cdot α^{'}$ . Also, by LR, we have $s_{0} \cdot α a \sim_{u} s_{0} \cdot α$ , Thus $s_{0} \cdot α a \sim_{u} s_{0} \cdot α^{'}$ by transitivity of $\sim_{u}$ .

If $dom (a) ↣ u$ , then ${ta}_{u} (α a) = ({ta}_{u} (α), {ta}_{dom (a)} (α), a)$ , which implies that the action a also occurs in $α^{'}$ as the last action in a domain interfering with u. If there are any subsequent noninterfering actions, we may switch the role of $α a$ and $α^{'}$ and apply the previous case. Hence, we may assume $α^{'} = β a$ for some sequence of actions β, so ${ta}_{u} (α^{'}) = ({ta}_{u} (β), {ta}_{dom (a)} (β), a)$ . It follows from the equality ${ta}_{u} (α a) = {ta}_{u} (α^{'})$ that ${ta}_{u} (α) = {ta}_{u} (β)$ and ${ta}_{dom (a)} (α) = {ta}_{dom (a)} (β)$ . By the inductive hypothesis, we obtain $s_{0} \cdot α \sim_{u} s_{0} \cdot β$ and $s_{0} \cdot α \sim_{dom (a)} s_{0} \cdot β$ . It follows from this by WSC that $s_{0} \cdot α a \sim_{u} s_{0} \cdot β a$ . □

Since, by Example 6 and Theorem 3(4), TA-security is stronger than IP-security, this result implies that the existence of equivalence relations $\sim_{u}$ satisfying conditions OC, WSC and LR is not* a necessary condition for IP-security, since if this were the case, then every IP-secure system would be TA-secure.

This raises the question of whether the existence of weak unwindings is equivalent to TA-security instead. We now show that this question can be answered in the positive, provided it is formulated appropriately. The existence of weak unwindings turns out to have a somewhat surprising dependency on the structure of the system.

Given a system $M = ⟨ S, s_{0}, step, obs, dom ⟩$ with actions A, define the “unfolded” system $uf (M) = ⟨ S^{'}, s_{0}^{'}, {step}^{'}, {obs}^{'}, dom ⟩$ with actions A having the same domains as in M, by $S^{'} = A^{}$ , $s_{0}^{'} = ε$ , ${step}^{'} (α, a) = α a$ , and ${obs}_{u}^{'} (α) = {obs}_{u} (s_{0} \cdot α)$ , where $s_{0} \cdot α$ is computed in M. Intuitively, this construction unfolds the graph of M into an infinite tree. Define the equivalence relations $\sim_{u}^{ta}$ on the states $S^{'} = A^{}$ of $uf (M)$ by $α \sim_{u}^{ta} α^{'}$ iff ${ta}_{u} (α) = {ta}_{u} (α^{'})$ . Then we have the following.
Theorem 2.
M is TA-secure with respect to ↣ iff there exists a weak unwinding on $uf (M)$ with respect to ↣ .
Proof.
We first note that for the relations $\approx_{u}^{u w}$ on $uf (M)$ , we have $α \approx_{u}^{u w} α^{'}$ iff $α \sim_{u}^{ta} α^{'}$ . For, the relations $\sim_{u}^{ta}$ are equivalence relations and satisfy WSC and LR by definition of ${ta}_{u}$ . Thus, we have $\approx_{u}^{u w} \subseteq \sim_{u}^{ta}$ by definition of $\approx_{u}^{u w}$ . Conversely, we show that ${ta}_{u} (α) = {ta}_{u} (α^{'})$ implies $α \approx_{u}^{u w} α^{'}$ , by induction on $| α | + | α^{'} |$ . The case of $α = α^{'} = ε$ is clear. Suppose ${ta}_{u} (α a) = {ta}_{u} (α^{'})$ . If $dom (a) ↣̸ u$ , we have ${ta}_{u} (α) = {ta}_{u} (α a) = {ta}_{u} (α^{'})$ , so by the inductive hypothesis, we have $α \approx_{u}^{u w} α^{'}$ . Since $\approx_{u}^{u w}$ satisfies LR, we obtain $α a \approx_{u}^{u w} α$ and it follows that $α a \approx_{u}^{u w} α^{'}$ . For the case $dom (a) ↣ u$ , where ${ta}_{u} (α a) = ({ta}_{u} (α), {ta}_{dom (a)} (α), a)$ , we may assume without loss of generality that the final action in $α^{'}$ may interfere with u, and derive that $α^{'} = β a$ where ${ta}_{u} (α) = {ta}_{u} (β)$ and ${ta}_{dom (a)} (α) = {ta}_{dom (a)} (β)$ . It follows by the inductive hypothesis that $α \approx_{u}^{u w} β$ and $α \approx_{dom (a)}^{u w} β$ , hence by the fact that $\approx_{u}^{u w}$ satisfies WSC that $α a \approx_{u}^{u w} β a$ , as required.

Suppose M is TA-secure with respect to ↣. Then WSC and LR for the relations $\sim_{u}^{ta}$ are immediate from the definition of the functions ${ta}_{u}$ , and OC follows directly from TA-security. Hence the family $\sim_{u}^{ta}$ is a weak unwinding on $uf (M)$ . Conversely, suppose that there exists a weak unwinding $\sim_{u}$ on $uf (M)$ with respect to ↣. Then $\sim_{u}^{ta} = \approx_{u}^{u w} \subseteq \sim_{u}$ satisfies OC, hence M is TA-secure with respect to ↣. □

It is reasonable to give a definition of security on M by reference to $uf (M)$ since these systems are bisimilar under the obvious notion of bisimulation on the state-observed system model. Bisimilarity of two systems is usually taken to imply their equivalence on all properties of interest. One might therefore expect from Theorem 2 that TA-security implies the existence of a weak unwinding on the system M as well as on $uf (M)$ . It is the case that unwindings on M can be lifted to unwindings on $uf (M)$ .
Proposition 5.
If there exists a weak unwinding for ↣ on M then there exists a weak unwinding for ↣ on $uf (M)$ .
Proof.
Suppose the relations $\sim_{u}$ are a weak unwinding for ↣ on M. Define $\sim_{u}^{'}$ on $uf (M)$ by $α \sim_{u}^{'} α^{'}$ if $s_{0} \cdot α \sim_{u} s_{0} \cdot α^{'}$ in M. It is easily checked that the relations $\sim_{u}^{'}$ are a weak unwinding on $uf (M)$ . □

However, what we need, given Theorem 2, to deduce the existence of an unwinding on M from TA-security is the converse of this result. The following example shows that the converse does not hold. The reader may obtain some intuition for this example by noting that whereas weak unwinding seems to be sensitive to information about past actions, bisimulation cares only about the future. The essence of the example is that not enough past information is encoded in the states of the system M itself.

Fig. 2.
An example showing TA-security does not imply existence of a weak unwinding.
Example 7.
Consider the system and policy depicted in Fig. 2. There are actions a, b, c of domains $A$ , $B$ , $C$ respectively, and $s_{0}$ is the initial state. For all domains u other than $D$ , we assume that the observation ${obs}_{u}$ is the same on all states. TA-security therefore depends only on the behaviour of the system with respect to domain $D$ , where there are two possible observations o, $o^{'}$ as indicated. We show that there does not exist a weak unwinding for ↣ on M, but there does exist one on $uf (M)$ .

For the former, we consider the relation family $\approx_{u}^{u w}$ on M. Note that since $B ↣̸ D$ and $s_{0} \cdot b = s_{1}$ we have by LR that $s_{0} \approx_{D}^{u w} s_{1}$ . Similarly, since $C ↣̸ A$ we have $s_{0} \approx_{A}^{u w} s_{1}$ . Hence, by WSC, for the action a, we get $s_{0} \approx_{D}^{u w} s_{2}$ . Since ${obs}_{D} (s_{0}) = o$ and ${obs}_{D} (s_{2}) = o^{'}$ , we have that $\approx_{D}^{u w}$ does not satisfy OC. Since $\approx_{u}^{u w}$ is the smallest family satisfying WSC and LR, there can exist no weak unwinding for ↣ on M.

For the unwinding on $uf (M)$ , consider $\approx_{u}^{u w} = \sim_{u}^{ta}$ . Since this family of equivalence relations satisfies WSC and LR, it suffices to consider the property OC, where we need consider only the domain $D$ , as already noted. Here, the only possible failure of OC is for states α, $α^{'}$ where ${ta}_{D} (α) = {ta}_{D} (α^{'})$ , $s_{0} \cdot α \in {s_{0}, s_{1}}$ and $s_{0} \cdot α^{'} = s_{2}$ . Now $s_{0} \cdot α^{'} = s_{2}$ implies that $α^{'}$ contains either a b and a later a, or a c and a later a. View ${ta}_{D} (α^{'})$ as a tree with nodes of the form $(x, y, e)$ representing a vertex labelled e with subtrees corresponding to x and y. Then this tree contains a path from a leaf to the root containing either b and later a, or c and later a. The same then applies to the identical tree for ${ta}_{D} (α)$ , which implies that α contains either a b and later a or a c and later a. But this means that $s_{0} \cdot α = s_{2}$ , a contradiction. Hence the family $\approx_{u}^{u w}$ satisfies OC.

Since $uf (M)$ and M are bisimilar, this example shows that bisimulation does not preserve existence of a weak unwinding. It is therefore necessary to either abandon the presumption that security properties are preserved under bisimulation, or adopt the stance that existence of a weak unwinding (on the system as presented) is not a sensible notion of security. We prefer the latter, but note that this does not hinder the utility of weak unwinding as a proof technique. The existence of a weak unwinding on some system bisimilar to the system as presented remains a sensible notion; we have shown that this is equivalent to TA-security.
6. Access control systems

As a particular application of the unwinding conditions, Rushby [35] discusses a notion of access control system that he formulates in order to give semantic content to the Bell-La Padula model [4] (which has been criticized for lacking semantics). He shows that every access control system satisfying a compatibility condition with respect to a noninterference policy is IP-secure. In this section, we formulate a weaker variant of Rushby’s definitions, and show that it implies the stronger notion of TA-security.

Moreover, we also show a converse to the result that access control systems are TA-secure, viz., that every system satisfying TA-security can be interpreted as an access control system. This proves the equivalence in some sense of access control and TA-security. We believe that these results, together with the example of Section 4 and the results of the previous section, provide strong evidence that TA-security, rather than IP-security, is the notion that best realizes the original objectives of the notion of intransitive noninterference.

According to Rushby, a system with structured state is a machine $⟨ S, s_{0}, A, step, obs, dom ⟩$ together with

a set N of names,

a set V of values, and functions,

$contents : S \times N \to V$ , with $contents (s, n)$ interpreted as the value of object n in state s,

$observe : D \to P (N)$ , with $observe (u)$ interpreted as the set of objects that domain u can observe, and

$alter : D \to P (N)$ , with $alter (u)$ interpreted as the set of objects whose values domain u is permitted to alter.

For a system with structured state, when

u \in D

and s is a state, write

{oc}_{u} (s)

for the function mapping

observe (u)

to values, defined by

{oc}_{u} (s) (n) = contents (s, n)

for

n \in observe (u)

. Intuitively,

{oc}_{u} (s)

captures all the content of the state s that is observable to u. Using this, we may define a binary relation

\sim_{u}^{oc}

of observable content equivalence on S for each domain

u \in D

, by

s \sim_{u}^{oc} t

{oc}_{u} (s) = {oc}_{u} (t)

In order to capture the conditions under which the machine operates in accordance with the intuitive interpretations of this extra structure, Rushby defines the following three Reference Monitor Assumptions.

If $s \sim_{u}^{oc} t$ then ${obs}_{u} (s) = {obs}_{u} (t)$ .

If $s \sim_{dom (a)}^{oc} t$ and either $contents (s \cdot a, n) \neq contents (s, n)$ or $contents (t \cdot a, n) \neq contents (t, n)$ then $contents (s \cdot a, n) = contents (t \cdot a, n)$ .

If $contents (s \cdot a, n) \neq contents (s, n)$ then $n \in alter (dom (a))$ .

The first of these says that an agent’s observation depends only on the values of the objects observable to the agent. The third says that if an action can change the value of an object, then the agent of that action is in fact permitted to alter that object. The condition RM2 is more subtle. The following provides a possibly more perspicuous formulation of this condition.

Proposition 6.
RM2 is equivalent to the following: For all states s, either
for all $t \sim_{dom (a)}^{oc} s$ , we have $contents (t \cdot a, n) = contents (t, n)$ , or

for all $t \sim_{dom (a)}^{oc} s$ , we have $contents (s \cdot a, n) = contents (t \cdot a, n)$ .

That is, with the choice depending only on information observable to $dom (a)$ , the effect of the action is either to make no change to n or to assign a new value to n that depends only on information observable to $dom (a)$ .

In addition to the reference monitor assumptions, Rushby considers the condition:
If $alter (u) \cap observe (v) \neq \emptyset$ then $u ↣ v$ .
Intuitively, this says that the ability to write to a value that an agent can observe counts as a way to interfere with that agent. Rushby shows the following proposition.
Proposition 7 ([35, Theorems 2 and 8]).

Suppose M is a system with structured state that satisfies RM1–RM3 and AOI. Then the family of relations $\sim_{u}^{oc}$ on M is a weak unwinding with respect to ↣. Hence M is IP-secure for ↣ .

By the results of the previous section, Rushby’s result in fact yields the stronger conclusion that access control systems consistent with a policy are TA-secure. We can further strengthen this result by weakening the precondition.

Note that the condition RM2 says that the next value of n produced on performing an action a depends only on the values of names observable to $dom (a)$ . If n is not observable to $dom (a)$ , this may be too strong. Consider, for example, the situation where n represents a block of memory, and the action a writes to a single location within this block. Here the successor value depends on the value written (which will typically depend on the values of names observable to $dom (a)$ ), but also on the previous value of n. Similarly, if the name n is an object in an object-oriented system, and the effect of the action is to call a method of this object, then the successor value will depend of the input parameters of the call (which will depend on values of names observable to $dom (a)$ ), but also on the value of n. Thus, the condition RM2 can plausibly be weakened to the following.4

⁴
A weakened condition resembling RM2′ has also been used in a slightly different context by Greve, Wilding and van Fleet [18]. A weakening has also been proposed by von Oheimb [43], who also shows that the definition of access control system consistent with a policy can be weakened while still implying the existence of unwinding conditions implying IP-security. He adds the conditions $dom (a) ↣ u$ , $n \in observe (u)$ and $s \sim_{u}^{oc} t$ to the antecedant of RM2. We would argue that whether or not a system is an access control system should be independent of the policy that may be applied to it. The fact $dom (a) ↣ u$ in the precondition is in any case derivable from $n \in observe (u)$ and $contents (s \cdot a, n) \neq contents (s, n) \lor contents (t \cdot a, n) \neq contents (t, n)$ in the context of AOI and RM3, so can be omitted without loss of generality.

For all actions a, states s, t and names $n \in alter (dom (a))$ , if $s \sim_{dom (a)}^{oc} t$ and $contents (s, n) = contents (t, n)$ we have $contents (s \cdot a, n) = contents (t \cdot a, n)$ .

That is, for

n \in alter (dom (a))

, the value

contents (s \cdot a, n)

is a function of both

contents (s, n)

and

{oc}_{dom (a)} (s)

. Using Proposition 6 it can be seen that RM2 implies RM2′. The converse does not hold.

We now weaken Rushby’s notion of access control system by replacing RM2 by RM2′. We define a system with structured states to be a weak access control system if it satisfies conditions RM1, RM2′ and RM3. We say such a system is consistent with a policy ↣ if it satisfies AOI.

We also introduce a related notion on systems without structured states, that expresses that the system behaves as if it were an access control system. Say that a system M with states S admits a weak access control implementation consistent with ↣ if there exists a set of names N, a set of values V and functions $observe : D \times S \to P (N)$ , $alter : D \times S \to P (N)$ and $contents : N \times S \to V$ , with respect to which M is a weak access control system satisfying the condition AOI.

The following shows that weak access control systems consistent with a policy satisfy Rushby’s unwinding conditions for intransitive noninterference:

Proposition 8.

Suppose M is a weak access control system consistent with ↣. Then the family of relations $\sim_{u}^{oc}$ is a weak unwinding on M with respect to ↣ .

Proof.

OC is direct from RM1 and LR follows easily from RM3 and AOI. For WSC, suppose that $s \sim_{dom (a)}^{oc} t$ and $s \sim_{u}^{oc} t$ , i.e., ${oc}_{u} (s) = {oc}_{u} (t)$ . We need to show $s \cdot a \sim_{u}^{oc} t \cdot a$ , which amounts to showing $contents (s \cdot a, n) = contents (t \cdot a, n)$ for all $n \in observe (u)$ . We consider the two possibilities $n \in alter (dom (a))$ and $n \notin alter (dom (a))$ :

If $n \in alter (dom (a))$ then we have $contents (s \cdot a, n) = contents (t \cdot a, n)$ by RM2′.

If $n \notin alter (dom (a))$ , then using RM3 we have $contents (s \cdot a, n) = contents (s, n) = contents (t, n) = contents (t \cdot a, n)$ .

Thus, we have

s \cdot a \sim_{u}^{oc} t \cdot a

. □

We may also show a converse to this result, which leads to the conclusion that unwinding and weak access control systems are essentially equivalent.

Proposition 9.

Suppose that there exists a weak unwinding on M with respect to ↣. Then M admits a weak access control interpretation consistent with ↣ .

Proof.

Let the weak unwinding be ${\sim_{u}}_{u \in D}$ . Write ${[s]}_{u}$ for the equivalence class of s under $\sim_{u}$ . We define the access control interpretation on M as follows:

$N = D$ ,

$observe (u) = {u}$ ,

$alter (u) = {v \in D ∣ u ↣ v}$ ,

$contents (s, u) = {[s]}_{u}$ .

Note that then

s \sim_{u} t

iff

{[s]}_{u} = {[t]}_{u}

iff

contents (s, u) = contents (t, u)

iff

s \sim_{u}^{oc} t

RM1 is immediate from the fact that $\sim_{u}$ satisfies OC.

For RM2′, suppose that $n \in alter (dom (a))$ and $s \sim_{dom (a)}^{oc} t$ and $contents (s, n) = contents (t, n)$ . Then $n \in D$ , and from $contents (s, n) = contents (t, n)$ we get that $s \sim_{n} t$ . From $s \sim_{dom (a)}^{oc} t$ we have that $s \sim_{dom (a)} t$ . Hence by WSC, we have $s \cdot a \sim_{n} t \cdot a$ , which is equivalent to $contents (s \cdot a, n) = contents (t \cdot a, n)$ .

For RM3, we prove the contrapositive. Suppose that $n \notin alter (dom (a))$ . Then $n \in D$ and $dom (a) ↣̸ n$ . By LR, we have $s \cdot a \sim_{n} s$ , which is equivalent to $contents (s \cdot a, n) = contents (s, n)$ , as required.

Plainly, if $n \in alter (u)$ and $n \in observe (v)$ then $n = v$ and $u ↣ v$ , so AOI also holds. □

Combining these results with those of the previous section, we see that there is a close correspondence between TA-security, weak access control interpretations, and weak unwindings.

Corollary 1.

The following are equivalent

M is TA-secure with respect to ↣ ,

$uf (M)$ admits a weak access control interpretation consistent with ↣ ,

there exists a weak unwinding on $uf (M)$ with respect to ↣ .

Proof.

The equivalence of (1) and (3) is from Theorem 2, and that between (2) and (3) follows from Propositions 8 and 9. □

From Theorem 1 and Proposition 8, we also obtain the following corollary.

Corollary 2.

If M is a weak access control system consistent with ↣ then M is TA-secure for ↣ .

This conclusion is a more general result than Proposition 7, in which we have both weakened the antecedent and strengthened the consequent.

7. Variants of TA-security

The definition of TA-security is based on the general idea of comparing the information that an agent obtains from its observations with the information that it would have in a concrete operational model of maximal permitted information transmission consistent with the policy. There are many ways that one could build such a definition: we give a few examples in this section that might also plausibly be taken as the semantics of intransitive policies.

We noted above in Example 4 that the definition of IP-security has one aspect that might reasonably be questioned: it classifies as secure situations in which an agent causes information to be transmitted to another that it has not actually observed. TA-security is similar in this regard.

Example 8.
The system $M^{'}$ of Example 4 is both IP-secure and TA-secure. In particular, let $α = α_{1} α_{2}$ and $β = β_{1} β_{2}$ , where $α_{2}$ and $β_{2}$ are the maximal suffixes of α and β in ${h}^{}$ , respectively. Then it can be shown that ${ipurge}_{L} (α) = {purge}_{L} (β)$ iff ${ta}_{L} (α) = {ta}_{L} (β)$ iff $α_{1} = β_{1}$ . Moreover, $α_{1} = β_{1}$ implies that α contains an h before a d iff β does. TA-security and IP-security follow since ${obs}_{L} (s_{0} \cdot α) = 1$ if α contains an h before a d and ${obs}_{L} (s_{0} \cdot α) = 0$ otherwise.

In particular, when ${obs}_{L} (s_{0} \cdot α) = 1$ , agent L knows that there has been an h before a d. On the other hand, since always ${obs}_{D} (s_{0} \cdot α) = ⊥$ , agent D itself has no information about the sequence α. Thus, in this system, D can be viewed as causing information to be transmitted to L that it does not itself have.

Whether one considers this example to illustrate a violation of security depends on one’s attitude to forwarding of unobserved information. It is straightforward from the definition that TA-security, like IP-security, is preserved under observation abstraction. If one takes secrecy to be the main concern of security, then this is reasonable. There are certainly situations where it seems acceptable for a downgrader not to know all the information that flows as a result of its actions. Consider a key escrow agent that releases a private decryption key upon legitimate request from police. This causes the contents of messages encrypted with the corresponding public key to flow to the police, but it does not seem reasonable to require that the escrow agent know the content of those messages (which it might not even have observed in ciphertext). Similarly, under a policy that mandates all government cabinet documents to be declassified after 30 years, it is not necessary for the declassifier to know the complete contents of a document being declassified: it suffices that the declassifier knows that the document is in fact 30 years old.

On the other hand, it also seems reasonable to state a requirement that a declassifier have inspected documents being released, and know the contents thereof. It is possible to construct a definition that would consider Example 4 as insecure, by changing the definition of the function $ta$ .

Given a policy ↣, for each domain $u \in D$ , define the function ${to}_{u} : A^{} \to T ({(A \cup O)}^{}, A)$ by ${to}_{u} (ε) = {obs}_{u} (s_{0})$ and ${to}_{u} (α a) = \{\begin{matrix} {to}_{u} (α) & when dom (a) ↣̸ u, \\ ({to}_{u} (α), {view}_{dom (a)} (α), a) & otherwise . \end{matrix}$ Intuitively, this definition takes the model of the maximal information that an action a may transmit after the sequence α to be the fact that a has occurred, together with the information that $dom (a)$ actually* has, as represented by its view ${view}_{dom (a)} (α)$ . By contrast, TA-security uses in place of this the maximal information that $dom (a)$ may have. (The nomenclature is intended to be suggestive of transmission of information about observations.) We may now base the definition of security on the function $to$ rather than $ta$ .
Definition 4.
The system M is TO-secure with respect to ↣ if for all domains $u \in D$ and all $α, α^{'} \in A^{}$ with ${to}_{u} (α) = {to}_{u} (α^{'})$ , we have ${obs}_{u} (s_{0} \cdot α) = {obs}_{u} (s_{0} \cdot α^{'})$ .
Example 9.
The system $M^{'}$ of Example 4 is not TO-secure. Note that ${to}_{L} (h d) = ({to}_{L} (h), {view}_{D} (h), d) = (ε, ⊥, d) = {to}_{L} (d)$ . However, ${obs}_{L} (s_{0} \cdot h d) = 1 \neq 0 = {obs}_{L} (s_{0} \cdot d)$ .

On the other hand, these runs do not constitute a counter-example to the TO-security of the system M of Example 3. Here we have ${to}_{L} (h d) = ({to}_{L} (h), {view}_{D} (h), d) = (ε, 01, d) \neq (ε, 0, d) = {to}_{L} (d)$ . Indeed, this system can be shown to be TO-secure.

This example demonstrates that, unlike all the previous definitions, TO-security is not preserved under observation abstraction. Note that the key difference is that the observations in the system occur in the term ${to}_{u} (α)$ , so this is not invariant under observation abstraction, as is the case for ${purge}_{u} (α)$ , ${ipurge}_{u} (α)$ and ${ta}_{u} (α)$ .

For purposes of comparison to the related literature (viz. [33]), will also consider a slight variant of this definition. Given a policy ↣, for each domain $u \in D$ , define the function ${ito}_{u} : A^{} \to T (O {(A \cup O)}^{}, A)$ by ${ito}_{u} (ε) = {obs}_{u} (s_{0})$ and ${ito}_{u} (α a) = \{\begin{matrix} {ito}_{u} (α) & if dom (a) ↣̸ u, \\ ({ito}_{u} (α), {view}_{dom (a)} (α), a) & if dom (a) = u, \\ ({ito}_{u} (α), {view}_{dom (a)} (α a), a) & otherwise . \end{matrix}$ This definition is just like that of $to$ , with the difference that the information that may be transmitted to u by an action a such that $dom (a) ↣ u$ but $dom (a) \neq u$ , includes the observation ${obs}_{dom (a)} (s_{0} \cdot α a)$ obtained in domain $dom (a)$ immediately after the occurrence of action a. Intuitively, the definition of security based on this notion will allow that the action a transmits not just the information observable to $dom (a)$ at the time that it is invoked, but also the new information that it computes and makes observable in $dom (a)$ . This information is not included in the value ${ito}_{dom (a)} (α a)$ itself, since the definition of security will state that the new observation may depend only on this value. The nomenclature in this case is intended to be suggestive of immediate* transmission of information about observations.

The following definition follows the pattern of the others, but based is on the functions $ito$ .
Definition 5.
The system M is ITO-secure with respect to ↣ if for all domains $u \in D$ and all $α, α^{'} \in A^{}$ with ${ito}_{u} (α) = {ito}_{u} (α^{'})$ , we have ${obs}_{u} (s_{0} \cdot α) = {obs}_{u} (s_{0} \cdot α^{'})$ .

The following example illustrates a key difference between the notions of TO-security and ITO-security.
Example 10.
Consider another variant of Example 2, for the same policy $H ↣ D ↣ L$ . States are defined as assignments to the boolean variables $x_{H}$ , $x_{D}$ , $x_{L}$ , all initially 0. Observations are defined by ${obs}_{H} (s) = s (x_{H})$ , ${obs}_{D} (s) = s (x_{D})$ and ${obs}_{L} (s) = s (x_{L})$ . Actions are defined by $\begin{array}{rcl} h : x_{H} : = 1, \\ d : x_{L} : = x_{H}; x_{D} : = x_{H} . \end{array}$ This example is not TO-secure, since ${to}_{L} (h d) = ({to}_{L} (h), {view}_{D} (h), d) = (ε, 0, d) = {to}_{L} (d)$ , but ${obs}_{L} (s_{0} \cdot h d) = 1 \neq 0 = {obs}_{L} (s_{0} \cdot d)$ . However, note that ${ito}_{L} (h d) = ({ito}_{L} (h), {view}_{D} (h d), d) = (ε, 0 d 1, d)$ , which is distinct from ${ito}_{L} (d) = ({ito}_{L} (ε), {view}_{D} (ε), d) = (ε, 0, d)$ . Thus, this pair of runs is not a violation of ITO-security, and indeed, the system can be shown to be ITO-secure. Intuitively, in this system D declassifies whether there has been an h action, but, at the first time it does so, it is not itself aware of whether this is the case. Only (immediately) after the declassification action has been performed does it learn whether it has declassified the occurrence of an h.

Intuitively, whereas TO-security requires that an agent know prior to performing an action what information that action may cause to be transmitted, ITO-security only requires that it have this knowledge immediately after the action has been performed. This weaker requirement may be appropriate in situations where it is only required for the agent to be able to audit, rather than control, the information flow consequences of its actions.

We now consider how all these definitions of security are related. We begin by noting that it is possible to give a flatter representation of the information in ${to}_{u} (α)$ , that clarifies the relationship of this notion to P-security. Define the possibly transmitted view* of domain u for a sequence of actions α to be the largest prefix ${tview}_{u} (α)$ of ${view}_{u} (α)$ than ends in an action a with $dom (a) = u$ . (In case there is no such action a, we take ${tview}_{u} (α) = ε$ .) Then we have the following result, which intuitively says that u’s observations depend only on (1) the parts of the views of other agents which are permitted to pass information to u, that they have actually acted to transmit, and (2) u’s knowledge of the ordering of its own actions and the actions of these other agents.
Proposition 10.
M is TO-secure with respect to a policy ↣ iff for all sequences $α, α^{'} \in A^{}$ , and domains* $u \in D$ , if ${purge}_{u} (α) = {purge}_{u} (α^{'})$ and ${tview}_{v} (α) = {tview}_{v} (α^{'})$ for all domains $v \neq u$ such that $v ↣ u$ , then ${obs}_{u} (s_{0} \cdot α) = {obs}_{u} (s_{0} \cdot α^{'})$ .
Proof.
We show that ${to}_{u} (α) = {to}_{u} (α^{'})$ iff ${purge}_{u} (α) = {purge}_{u} (α^{'})$ and ${tview}_{v} (α) = {tview}_{v} (α^{'})$ for all domains $v \neq u$ such that $v ↣ u$ .

For the proof from left to right, we proceed by induction on the combined length of α and $α^{'}$ . The base case is trivial.
Supposing the claim holds for strings of shorter combined length, consider strings $α a$ and $α^{'}$ such that ${to}_{u} (α a) = {to}_{u} (α^{'})$ where $a \in A$ and $dom (a) ↣̸ u$ . Then ${to}_{u} (α) = {to}_{u} (α a) = {to}_{u} (α^{'})$ , so by induction, we have that ${purge}_{u} (α) = {purge}_{u} (α^{'})$ and ${tview}_{v} (α) = {tview}_{v} (α^{'})$ for all domains $v \neq u$ such that $v ↣ u$ . Since $dom (a) ↣̸ u$ , we have ${purge}_{u} (α a) = {purge}_{u} (α) = {purge}_{u} (α^{'})$ . Similarly, we have that $dom (a) \neq v$ for any v such that $v ↣ u$ , so ${tview}_{v} (α a) = {tview}_{v} (α) = {tview}_{v} (α^{'})$ for all domains $v \neq u$ such that $v ↣ u$ , as required.

Alternately, suppose ${to}_{u} (α a) = {to}_{u} (α^{'})$ where $dom (a) ↣ u$ . Then $α^{'}$ cannot be ε. If the last action of $α^{'}$ does not interfere with u then we may apply the previous case. Hence, without loss of generality, $α^{'} = β b$ where $dom (b) ↣ u$ , and from ${to}_{u} (α a) = {to}_{u} (β b)$ we obtain $a = b$ , ${to}_{u} (α) = {to}_{u} (β)$ , and ${view}_{dom (a)} (α) = {view}_{dom (a)} (β)$ .

From ${to}_{u} (α) = {to}_{u} (β)$ , we have by the induction hypothesis that ${purge}_{u} (α) = {purge}_{u} (α^{'})$ and ${tview}_{v} (α) = {tview}_{v} (α^{'})$ for all domains $v \neq u$ such that $v ↣ u$ . It follows that ${purge}_{u} (α a) = {purge}_{u} (α) \cdot a = {purge}_{u} (β) \cdot a = {purge}_{u} (β a)$ . Further, it follows that ${tview}_{v} (α a) = {tview}_{v} (β a)$ for $v \neq u$ such that $v ↣ u$ . The proof of this is in two cases: (1) if $v = dom (a)$ , then ${tview}_{v} (α a) = {view}_{v} (α) \cdot a = {view}_{v} (β) \cdot a = {tview}_{v} (β a)$ ; (2) if $v \neq dom (a)$ then ${tview}_{v} (α a) = {tview}_{v} (α) = {tview}_{v} (β) = {tview}_{v} (β a)$ .

Conversely, for the implication from right to left, we again proceed by induction on the combined length of α and $α^{'}$ . The base case of $α = α^{'} = ε$ is trivial.
Consider the case where the RHS holds for $α a$ and $α^{'}$ , where $dom (a) ↣̸ u$ , and the implication from right to left holds for α, $α^{'}$ . Then from ${purge}_{u} (α a) = {purge}_{u} (α^{'})$ we obtain that ${purge}_{u} (α) = {purge}_{u} (α^{'})$ . Similarly, for $v \neq u$ , $v ↣ u$ , we have ${tview}_{v} (α a) = {tview}_{v} (α^{'})$ , so, since we cannot have $v = dom (a)$ in the present case, we obtain that ${tview}_{v} (α) = {tview}_{v} (α a) = {tview}_{v} (α^{'})$ . By the inductive hypothesis, it follows that ${to}_{u} (α) = {to}_{u} (α^{'})$ , hence ${to}_{u} (α a) = {to}_{u} (α) = {to}_{u} (α^{'})$ .

Consider the case where the RHS holds for $α a$ and $α^{'}$ , where $dom (a) ↣ u$ , and the implication from right to left holds for α, $α^{'}$ . Since ${purge}_{u} (α^{'}) = {purge}_{u} (α a) = {purge}_{u} (α) a$ , the sequence $α^{'}$ cannot be ε. We may assume without loss of generality that $α^{'} = β b$ where $dom (b) ↣ u$ , else we may apply the previous case. Thus, from ${purge}_{u} (α a) = {purge}_{u} (β b)$ it follows that ${purge}_{u} (α) = {purge}_{u} (β)$ and $a = b$ . We claim that moreover (1) ${to}_{u} (α) = {to}_{u} (β)$ and (2) ${view}_{dom (a)} (α) = {view}_{dom (a)} (β)$ , from which it follows that ${to}_{u} (α a) = {to}_{u} (β b)$ , which is the conclusion required.

We prove (2) first. Since $dom (a) ↣ u$ , $dom (a)$ is one of the domains v for which we have ${tview}_{v} (α a) = {tview}_{v} (β a)$ . It follows that ${view}_{dom (a)} (α) = {view}_{dom (a)} (β)$ , which is (2). Moreover, it also follows from (2) that ${tview}_{dom (a)} (α) = {tview}_{dom (a)} (β)$ . For all other domains $v \neq dom (a)$ such that $v ↣ u$ , we have ${tview}_{v} (α) = {tview}_{v} (α a) = {tview}_{v} (β a) = {tview}_{v} (β)$ , so in fact the second part of the antecedant of the induction hypothesis is satisfied. Since we already have the first part, i.e., ${purge}_{u} (α) = {purge}_{u} (β)$ , we obtain (1). □

We note the following property of these definitions.
Proposition 11.
Let $α, α^{'} \in A^{}$ and* $u \in D$ .
If M is TO-secure and ${to}_{u} (α) = {to}_{u} (α^{'})$ then ${view}_{u} (α) = {view}_{u} (α^{'})$ .

If M is ITO-secure and ${ito}_{u} (α) = {ito}_{u} (α^{'})$ then ${view}_{u} (α) = {view}_{u} (α^{'})$ .

If M is TA-secure and ${ta}_{u} (α) = {ta}_{u} (α^{'})$ then ${view}_{u} (α) = {view}_{u} (α^{'})$ .

Proof.
By induction on $| α | + | α^{'} |$ . We give the proof for (1), the proofs for (2) and (3) follow a similar structure. The base case of $α = α^{'} = ε$ is trivial. Consider sequences of actions $α a$ and $α^{'}$ , where $a \in A$ , such that ${to}_{u} (α a) = {to}_{u} (α^{'})$ .

If $dom (a) ↣̸ u$ , then we have ${to}_{u} (α) = {to}_{u} (α a) = {to}_{u} (α^{'})$ . By the induction hypothesis we get that ${view}_{u} (α) = {view}_{u} (α^{'})$ . Since ${to}_{u} (α a) = {to}_{u} (α)$ , we get from TO-security that ${obs}_{u} (s_{0} \cdot α a) = {obs}_{u} (s_{0} \cdot α)$ , which implies that ${view}_{u} (α a) = {view}_{u} (α) \circ {obs}_{u} (s_{0} \cdot α a) = {view}_{u} (α) \circ {obs}_{u} (s_{0} \cdot α) = {view}_{u} (α)$ . (Note that $dom (a) ↣̸ u$ implies $dom (a) \neq u$ .) It follows that ${view}_{u} (α a) = {view}_{u} (α^{'})$ .

If $dom (a) ↣̸ u$ , then ${to}_{u} (α a) = {to}_{u} (α^{'})$ implies that $α^{'} \neq ε$ . Let b be the final action in $α^{'}$ , so that $α^{'} = β b$ . If $dom (b) ↣̸ u$ , then we may apply the previous case with the roles of $α a$ and $β b$ swapped, so we may assume that $dom (b) ↣ u$ . It then follows from ${to}_{u} (α a) = {to}_{u} (β b)$ that $a = b$ and ${to}_{u} (α) = {to}_{u} (β)$ . By the inductive hypothesis we get that ${view}_{u} (α) = {view}_{u} (β)$ . From TO-security and ${to}_{u} (α a) = {to}_{u} (β a)$ we get that ${obs}_{u} (s_{0} \cdot α a) = {obs}_{u} (s_{0} \cdot β a)$ . It now follows in both the case that $dom (a) = u$ and the case that $dom (a) \neq u$ that ${view}_{u} (α a) = {view}_{u} (β a)$ , as required. □

The following result describes how these definitions are related. Like IP-security, the notions P-security, TO-security, ITO-security and TA-security are generalizations of the classical notion of noninterference in the transitive case. Theorem 3.

If M is P-secure with respect to ↣ then M is TO-secure with respect to ↣ .

If M is TO-secure with respect to ↣ then M is ITO-secure with respect to ↣ .

If M is ITO-secure with respect to ↣ then M is TA-secure with respect to ↣ .

If M is TA-secure with respect to ↣ then M is IP-secure with respect to ↣ .

If ↣ is transitive then P-security, TO-security, ITO-security, TA-security and IP-security (all with respect to ↣) are equivalent.

Proof.
Part (1) is immediate from Proposition 10. Part (5) follows from parts (1)–(4), using the fact that P-security and IP-security are equivalent with respect to transitive policies (Rushby [35, Theorem 9]).

For part (2), we claim that if ${ito}_{u} (α) = {ito}_{u} (α^{'})$ then ${to}_{u} (α) = {to}_{u} (α^{'})$ . Part (2) then follows trivially. To see that the claim holds, define the partial functions $F_{u} : T ({(A \cup O)}^{}, A) \to T ({(A \cup O)}^{}, A)$ , for $u \in D$ , defined inductively by $F_{u} (ε) = ε$ and $F_{u} (X, σ a o, a) = (F_{u} (X), σ, a)$ , where $o \in O$ and $dom (a) \neq u$ , and $F_{u} (X, σ, a) = (F_{u} (X), σ, a)$ when $dom (a) = u$ . Then it is easily shown that $F_{u} ({ito}_{u} (α)) = {to}_{u} (α)$ for all $α \in A^{}$ , from which the claim is immediate.

We now prove part (3). Assume that M is ITO-secure with respect to ↣. We claim that for all $u \in D$ and $α, α^{'} \in A^{}$ , if ${ta}_{u} (α) = {ta}_{u} (α^{'})$ then ${ito}_{u} (α) = {ito}_{u} (α^{'})$ . The result is then immediate from the definition of TO-security. The proof of the claim is by induction on $| α | + | α^{'} |$ . The base case of $α = α^{'} = ε$ is trivial. Supposing that the claim holds for strings of shorter combined length, suppose ${ta}_{u} (α a) = {ta}_{u} (α^{'})$ , where $α, α^{'} \in A^{*}$ and $a \in A$ . We consider two cases:
$dom (a) ↣̸ u$ . Then ${ta}_{u} (α) = {ta}_{u} (α a) = {ta}_{u} (α^{'})$ , so by the inductive hypothesis we have ${ito}_{u} (α) = {ito}_{u} (α^{'})$ . Since ${ito}_{u} (α a) = {ito}_{u} (α)$ in this case, it is immediate that ${ito}_{u} (α a) = {ito}_{u} (α^{'})$ .

$dom (a) ↣ u$ . We may assume without loss of generality that the last action in $α^{'}$ also interferes with u, else we may apply the previous case. So let $α^{'} = β b$ with $dom (b) ↣ u$ . Then ${ta}_{u} (α a) = {ta}_{u} (β b)$ , from which we get that $a = b$ and ${ta}_{u} (α) = {ta}_{u} (β)$ and ${ta}_{dom (a)} (α) = {ta}_{dom (a)} (β)$ . By induction, we have that ${ito}_{u} (α) = {ito}_{u} (β)$ and ${ito}_{dom (a)} (α) = {ito}_{dom (a)} (β)$ . From the latter, we obtain by ITO-security and Proposition 11 that ${view}_{dom (a)} (α) = {view}_{dom (a)} (β)$ . Together with ${ito}_{dom (a)} (α) = {ito}_{dom (a)} (β)$ this yields that ${ito}_{dom (a)} (α a) = {ito}_{dom (a)} (β a)$ , so by ITO-security, we have ${obs}_{dom (a)} (s_{0} \cdot α a) = {obs}_{dom (a)} (s_{0} \cdot β a)$ . Thus, we also have the stronger statement ${view}_{dom (a)} (α a) = {view}_{dom (a)} (β a)$ . It now follows, in both the case that $dom (a) = u$ and $dom (a) \neq u$ , that ${ito}_{u} (α a) = {ito}_{u} (β b)$ .

To show part (4), we claim that if $u \in X \subseteq D$ then ${ta}_{u} (α) = {ta}_{u} ({ipurge}_{X} (α))$ . In particular, ${ta}_{u} (α) = {ta}_{u} ({ipurge}_{u} (α))$ . Note that this straightforwardly implies that if ${ipurge}_{u} (α) = {ipurge}_{u} (α^{'})$ then ${ta}_{u} (α) = {ta}_{u} (α^{'})$ , and so if M is TA-secure with respect to ↣ then M is IP-secure with respect to ↣. To prove the claim we proceed by induction. The case of $α = ε$ is trivial. Assuming the claim holds for α, consider $α a$ where $a \in A$ . We consider two cases, depending on whether $dom (a) ↣ u$ .

If $dom (a) ↣̸ u$ , then ${ta}_{u} (α a) = {ta}_{u} (α)$ . We consider two further subcases. Write $v ↣ X$ if there exists $w \in X$ such that $v ↣ w$ .
$dom (a) ↣̸ X$ . Then ${ipurge}_{X} (α a) = {ipurge}_{X} (α)$ . Hence $\begin{array}{rcl} {ta}_{u} ({ipurge}_{X} (α a)) & = & {ta}_{u} ({ipurge}_{X} (α)) \\ = & {ta}_{u} (α) (by induction) \\ = & {ta}_{u} (α a) . \end{array}$

$dom (a) ↣ X$ . Then ${ipurge}_{X} (α a) = {ipurge}_{X \cup {dom (a)}} (α) \cdot a$ . Hence, from the induction hypothesis and the definitions, $\begin{array}{rcl} {ta}_{u} ({ipurge}_{X} (α a)) & = & {ta}_{u} ({ipurge}_{X \cup {dom (a)}} (α) \cdot a) \\ = & {ta}_{u} ({ipurge}_{X \cup {dom (a)}} (α)) \\ = & {ta}_{u} (α) (by induction) \\ = & {ta}_{u} (α a) . \end{array}$
If $dom (a) ↣ u$ , then ${ipurge}_{X} (α a) = {ipurge}_{X \cup {dom (a)}} (α) \cdot a$ . Thus $\begin{array}{rcl} {ta}_{u} ({ipurge}_{u} (α a)) & = & {ta}_{u} ({ipurge}_{X \cup {dom (a)}} (α) \cdot a) \\ = & ({ta}_{u} ({ipurge}_{X \cup {dom (a)}} (α)), {ta}_{dom (a)} ({ipurge}_{X \cup {dom (a)}} (α)), a) \\ = & ({ta}_{u} (α), {ta}_{dom (a)} (α), a) (by induction) \\ = & {ta}_{u} (α a) . \end{array}$ This completes the proof of the claim. □

7.1. Proof theory for the variants

We showed above that weak unwinding and access control systems provide sound and complete approaches to showing that a system is TA-secure. We will not attempt here to develop a similar theory for the alternatives introduced in this section, but it is worth noting a few applications of the ideas above to the variants.

First, further evidence of the utility of weak unwinding is the following result, which shows that it can be used as a proof technique not just for TA-security, but also for TO-security, provided we work with a particular relation. Define the relations $\approx_{u}^{obs}$ on states of a system M by $s \approx_{u}^{obs} t$ if ${obs}_{u} (s) = {obs}_{u} (t)$ . Then we have the following sufficient condition for TO-security.

Proposition 12.
Suppose the relation family $\approx_{u}^{obs}$ is a weak unwinding on M with respect to ↣. Then M is TO-secure with respect to ↣ .
Proof.
We claim that ${to}_{u} (α) = {to}_{u} (α^{'})$ implies $s_{0} \cdot α \approx_{u}^{obs} s_{0} \cdot α^{'}$ . The result then follows immediately using OC. The proof of the claim is by induction on the combined length of the sequences α, $α^{'}$ . In case both are ε, the claim plainly holds. Suppose that it holds for sequences of shorter combined length, and consider the sequences $α a$ and $α^{'}$ , where $a \in A$ . We consider two cases, depending on whether $dom (a) ↣ u$ .
If $dom (a) ↣̸ u$ , then it follows from the definitions that ${to}_{u} (α) = {to}_{u} (α a) = {to}_{u} (α^{'})$ , so by the inductive hypothesis, we have $s_{0} \cdot α \approx_{u}^{obs} s_{0} \cdot α^{'}$ . By LR we moreover have $s_{0} \cdot α a \approx_{u}^{obs} s_{0} \cdot α$ , and we conclude $s_{0} \cdot α a \approx_{u}^{obs} s_{0} \cdot α^{'}$ .

If $dom (a) ↣ u$ , then we may assume without loss of generality that $α^{'} = β b$ where $dom (b) ↣ u$ , else we may apply the previous case. It then follows from ${to}_{u} (α a) = {to}_{u} (β b)$ that $a = b$ and ${to}_{u} (α) = {to}_{u} (β)$ and ${view}_{dom (a)} (α) = {view}_{dom (a)} (β)$ . From the second of these facts, by the inductive hypothesis, we obtain $s_{0} \cdot α \approx_{u}^{obs} s_{0} \cdot β$ . From the third, since the final observations of the two views must be identical, we also have $s_{0} \cdot α \approx_{dom (a)}^{obs} s_{0} \cdot β$ . By WSC and $a = b$ we obtain $s_{0} \cdot α a \approx_{u}^{obs} s_{0} \cdot β b$ , as required. □

Second, Corollary 2 shows that weak access control systems consistent with a policy are TA-secure for that policy. One might wonder if it is possible to strengthen the conclusion to any of the stronger semantics of this section. The following example shows that this is not the case: we cannot further strengthen the conclusion to ITO-security.
Example 11.
Consider the system for the policy $A ↣ B ↣ C$ with structured states for the set of names $n_{A B}$ , $n_{B C}$ , taking boolean values. Intuitively, these variables represent channels between the agents, so that $n_{A B} \in alter (A) \cap observe (B)$ and $n_{B C} \in alter (B) \cap observe (C)$ . Plainly this is consistent with AOI. We represent states as tuples $s = (n_{A B}, n_{B C})$ with the obvious interpretation for $contents$ . The initial state of the system is $(0, 0)$ . Domain A has actions a with semantics $n_{A B} : = 1$ and B has action b with semantics $n_{B C} : = n_{A B}$ . The observation functions are defined on the state $s = (n_{A B}, n_{B C})$ by ${obs}_{A} (s) = {obs}_{B} (s) = ⊥$ and ${obs}_{C} (s) = n_{B C}$ . It can be verified that this system satisfies RM1, RM2′, RM3. However, it does not satisfy ITO-security. To see this, consider the sequences b and $a b$ . Here we have $\begin{array}{rcl} {ito}_{C} (b) & = & ({ito}_{C} (ε), {view}_{B} (b), b) \\ = & ({ito}_{C} (ε), ⊥ b ⊥, b) \\ = & ({ito}_{C} (a), {view}_{B} (a b), b) \\ = & {ito}_{C} (a b) \end{array}$ but ${obs}_{C} (s_{0} \cdot a) = 0 \neq 1 = {obs}_{C} (s_{0} \cdot a b)$ .

Notice that in this example, not all of the names observable to a domain have their contents visible in the observation of the domain. Say that a system with structured states is fully observable if in all states s we have ${obs}_{u} (s) = {oc}_{u} (s)$ . Note that this means that the relations $\sim_{u}^{oc}$ and $\approx_{u}^{obs}$ coincide. We now obtain the following from Propositions 8 and 12. This shows that, modulo the reasonable assumption of full observability, we can derive a result similar to Corollary 2, but with the yet stronger conclusion of TO-security.
Corollary 3.
If M is a fully observable weak access control system consistent with ↣ then M is TO-secure with respect to ↣ .

A similar result does not hold with P-security in place of TO-security. Example 12.
Note that if in Example 11 we change the definition of ${obs}_{B} (s)$ to $n_{A B}$ , then the system continues to satisfy RM1, RM2′, RM3 and AOI, and not P-security. The modified system has ${obs}_{u} (s) = {oc}_{u} (s)$ for all states s. (So it also satisfies TO-security.)

8. Related work

A great deal of the recent literature on noninterference, has been based on process algebraic semantic models. Work pursuing this direction is surveyed in [14,37]. Process algebraic models are more expressive than the semantic model of the present paper, in a number of dimensions: by allowing actions to have nondeterministic effects and by dropping the assumption of input-enabledness, i.e., allowing that not all actions are enabled at a state. (On the other hand, particularly in CCS formulations, e.g. [33], this literature has often dropped the important distinction between actions and observations, modelling both as events.)

Much of that literature, has been concerned with how to generalize existing definitions of noninterference to the resulting richer semantic setting, for the simplest policy consisting of two domains High and Low, with information flow from High to Low prohibited. This part of the literature is largely orthogonal to our concerns in this paper, in that it does not take up our main themes of intransitive policies, unwinding-based proof theory for those policies, and access control systems as a concrete engineering discipline for the construction of systems satisfying such a policy. As we have argued, there are subtleties concerning these themes even in the simple setting of deterministic, action-enabled systems we have studied.

A few works subsequent to Rushy [35] also address the semantics of intransitive policies. Bevier and Young [5] also work in a state-based model, but accommodate nondeterminism. They consider a definition of security which generalizes IP-security (and therefore suffers from the problem identified in Example 5). They also consider an unwinding-based proof technique, but work with a fixed relation derived from observations rather than allowing a general relation. There are some differences in their model (e.g., transitions are labelled not by actions but by agents) but, in a deterministic setting, their definition of unwinding amounts essentially to the statement that the family $\approx_{u}^{obs}$ is a weak unwinding. Since we showed that this relation is sound for TO-security, which is stronger than IP-security, their unwinding technique is also not complete for their definition of security, even in deterministic systems.

Roscoe and Goldsmith [33] have also argued that IP-security is not the correct definition for intransitive policies. They present a number of concrete examples to make this case, including a policy $H ↣ D ↣ L$ , intended to represent that D is a “downgrader” process that decides which of the High (H) secrets may safely be revealed to a Low process L. The key point of their argument is that the definition has the effect that a downgrader D’s action permits all information about preceding H actions to become known to L, even if the intent of the downgrading action was to release only some specific information about the preceding H actions. That is, this definition does not enable the intent of specific downgrading actions to be specified. This point has been considered debatable: it might be countered that intransitive noninterference was not intended to make such fine grained distinctions, but only to express some coarse architectural constraints on information flow. Subsequent work (e.g. [7–9]) has taken the approach of enriching the expressiveness of policies in order to capture such finer grained specifications of the downgrader.

Roscoe and Goldsmith propose two alternative semantics for intransitive noninterference, based on the notion of Low-determinism in the context of the process algebra CSP. (This is often misunderstood in the literature as implying that their theory applies only to deterministic systems. In fact, their definitions amount to saying that the possible Low nondeterminism at each step in a particular system is a function of the Low trace, but not of non-deterministic environment events.) The question of how exactly our definitions relate to RG’s definitions requires a treatment of mappings between state machine models and CSP, for which there are a number of plausible candidates. We deal with this topic in another paper [41], where we show that one transformation yields that RG’s definition is equivalent to P-security, but on another transformation, another of RG’s definitions that generalizes the first turns out to be equivalent to ITO-security.

Von Oheimb [43] generalizes Rushby’s definitions to the setting of state-observed systems with nondeterministic actions, and develops a matching generalization of unwinding relations that provides a sound proof technique for the new definition. His semantics is equivalent to IP-security when restricted to deterministic systems, so suffers from the same problems as we have identified in this paper. A discussion of access control systems is included in an appendix, where it is shown that these systems satisfy von Oheimb’s definition of intransitive noninterference. However, the result proved is for a variant of deterministic access control systems, so amounts essentially to a re-presentation of Rushby’s result using von Oheimb’s definition of intransitive noninterference. (The result could presumably also have been proved by noting that von Oheimb’s definition is equivalent to Rushby’s in the deterministic case, and applying Rushbys result.)

Mantel [25] proposes an approach to intransitive policies for nondeterministic systems. He uses a trace-based semantics: a system is represented as a set of possible sequences of events, each associated to a domain. The relationship between Mantel’s approach and the state-based model we have considered in this paper is unclear, even in the deterministic case, for a number of reasons. Mantel introduces a richer notion of policy with three types of binary relations on domains: visibility, confidentiality and “non-confidentiality”. However, he gives very little intuitive explanation of these relations, so it is not immediately apparent how one would represent an equivalence result. In particular, Mantel’s examples suggest that a domain in our model should be decomposed into two domains, for inputs and output events, so the policy writer is required to deal with three types of relations over double the number of domains.

The formal semantics associated with Mantel’s richer policy model is based on an extension of Mantel’s basic security properties [24], which describe closure conditions on the set of traces. Two particular such properties are considered, which allow for deletion and insertion of “confidential” events with respect to a given domain u. (The definitions are similar to the notion of forward correctability [21].) To accommodate intransitive policies, he requires consideration of a generalization of these conditions to certain groups of domains transitively related to u via the visibility relations. Because of these complications, establishing a formal relation between Mantel’s and other approaches would require some effort. (Mantel provides no results to this effect.) However, it appears that since only insertions and deletions of events are covered by Mantel’s semantics, the effect resembles that of the $ipurge$ function, so we expect that this approach will behave similarly to IP-security on an appropriately formulated representation of our Example 5, and therefore be distinct from the definitions we have proposed.

Backes and Pfitzmann [3] have stated a number of distinct definitions of intransitive noninterference in a cryptographic setting: their systems model encompasses probabilistic behaviour and notions of distinguishability based on computational complexity. All their definitions take the approach of checking for each pair of domains u and v with $u ↣̸ v$ that if u is given a bit b at the start of a run, then (subject to conditions that depend on the policy and definition) v has no better than probability $1 / 2$ of correctly guessing the value of b. This focus on transmission of information about an initial bit suggests that their definitions are not sensitive to the issues of ordering of actions that distinguish our definitions from IP-security.

We have been concerned in this paper with the general class of intransitive policies. These policies are able to express quite general architectures for information flow. A number of papers have addressed a very specific case of such policies, viz., the downgrader policy with $H ↣ D ↣ L$ and $L ↣ H$ but not $H ↣ L$ . (We note that issues that we raised in Example 5 do not arise for this single downgrader policy.) Mullins [30] states a definition for a nondeterministic labelled transition system model, based on the idea that H actions after the last D action should not impact the possible L traces after that point. Bossi et al. [6] work in the context of a CCS process algebraic semantics. They develop generalizations for the downgrader policy of a range of definitions for the two domain policy $L ↣̸ H$ , that consider the impact of composition of a system with H processes. Gorrieri and Vernali [17] consider such definitions in the context of a Petri net semantic model.

Another context where downgrading has been studied is the setting of language-based security, where the system is represented as a program, rather than the reactive automaton-based model we have considered. Often the program constructs (other than scheduling of concurrent threads) are deterministic in this setting. The focus is generally on what information flows about a nondeterministically chosen initial state of the system, rather than what actions have been nondeterministically selected over time, as in our models, although this gap can be bridged by representing these actions using an input stream variable [10]. Mantel and Sands [26] have proposed to introduce a programming annotation for downgrading, enabling the programmer to explicitly mark regions of code that are permitted to violate a transitive policy. The approach is synchronous, and does not separate policy from implementation. A similar, but more expressive, approach to downgrading policies is pursued by Chong and Myers [7], who propose a flexible language that attaches downgrading conditions to data items, and then state a security definition that requires that the view of a domain (defined similarly to asynchronous perfect recall) should not be able to distinguish different initial values for a variable, provided the conditions for its declassification are not met. In general, many different dimensions (e.g., who, what, where, when) can be constrained in declassification policies. Sabelfeld and Sands [38] lay out some general principles and directions for research in this area. Frequently, work in this area concentrates on the two-domain ${H, L}$ setting rather than a general set of domains with an intransitively structured policy. Definitions of security used include both bisimulation/unwinding style definitions (e.g. [26]) as well as definitions based on L knowledge of H initial values [2].

Some definitions of noninterference quantify over agent strategies, to capture additional deductive capacity that the attacker may have based on knowing the behaviour of some agents in the system. One example is nondeducibility on strategies [44], which says that a Low level observer should not be able to distinguish between High level agent strategies. Another is robust declassification [45], which allows downgrading of information, but says that what information is downgraded should not depend on attacker behavior: here the quantification is over Low level strategies. Only a few papers to date [3,6,17] have considered the strategic dimension in the context of intransitive noninterference policies.

A different direction of generalization that has been considered is to allow the policy to change over time. How to define semantics for such dynamic policies has been studied both in the state-machine setting using extensions of IP-security [11,23], as well as in a language-based framework [1].

9. Conclusion

Our results have left open a number of technical questions. We have shown that weak unwindings provide a complete proof technique for TA-security, but have not provided a complete technique for TO-security. The reason for this is that there is inherently no tractable set of conditions on the states of the system that characterizes TO-security. We treat this topic in a followup paper [12] which deals with the complexity of the notions of security discussed in this paper.

Our discussion has concentrated on a semantic model in which observations are associated to states. Rushby [35] also formulates a notion of IP-security on a model where instead of state observations, actions produce outputs, and proves similar results concerning unwinding and access control systems for this model. We treat the relationship between the two models in a companion paper [41], where we formulate a set of security notions for the action-observed model and show how these are related to the state-observed model under a transformations from the former to the latter. We also consider mappings to CSP processes there, and relate the definitions discussed in this paper to Roscoe and Goldsmith’s definitions on CSP processes.

How to accommodate quantification over strategies with our new definitions is at present unclear. Another area requiring investigation is the generalization of our definitions to nondeterministic systems and systems that are not input-enabled, as has been studied for IP-security by von Oheimb [43]. More generally, one could consider extensions to the richer semantic framework of process algebra.

Both the fact, as argued by RG, that the notion of (intransitive) noninterference on its own falls short of expressing the correctness properties of downgraders that they sought to capture, and the fact, as we have shown, that there are several plausible notions of noninterference for intransitive policies, suggests that the notion of noninterference policy expressed by a relation ↣ on domains lacks expressiveness that will be required in applications. We believe further work on richer formats for the expression of causality and information flow policies is warranted. The approach we have followed in this paper, of comparing an agent’s actual information to an intuitive concrete operational model of the maximal information that an agent is permitted to have and transmit, could well be useful in this enterprise. Some steps in this direction are taken in [8,9].

It would also be of interest to develop connections between language-based approach and the automaton based formulations of security. One possible point of connection is to use language-based techniques to verify the reference monitor conditions of access control models. Another is to use our semantic approach as a basis for language-based analyses of reactive systems described in a programming notation.

Footnotes

Acknowledgments

Thanks to the Courant Institute, New York University, for hosting a sabbatical visit during which this research was conducted. Work of the author supported by an Australian Research Council Discovery grant.

References

[1]

Askarov and

Chong, Learning is change in knowledge: knowledge-based security for dynamic policies, in: Proc. IEEE Computer Security Foundations Symposium, 2012, pp. 308–322.

[2]

Askarov and

Sabelfeld, Gradual release: unifying declassification, encryption and key release policies, in: Proc. IEEE Symposium Security and Privacy, 2007, pp. 207–221.

[3]

Backes and

Pfitzmann, Intransitive non-interference for cryptographic purposes, in: Proc. IEEE Symp. Security and Privacy, 2003, pp. 140–152.

[4]

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.

[5]

W.R.

Bevier and

W.D.

Young, A state-based approach to noninterference, in: Proc. IEEE Computer Security Foundations Workshop, 1994, pp. 11–21.

[6]

Bossi,

Piazza and

Rossi, Modelling downgrading in information flow security, in: Proc. IEEE Computer Security Foundations Workshop, 2004, pp. 187–201.

[7]

Chong and

A.C.

Myers, Security policies for downgrading, in: 11th ACM Conf. Computer and Communications Security (CCS), October 2004, 2004.

[8]

Chong and

van der Meyden, Deriving epistemic conclusions from agent architecture, in: Proc. Conf. Theoretical Aspects of Knowledge and Rationality, ACM Digital Library, 2009, pp. 61–70.

[9]

Chong and

van der Meyden, Using architecture to reason about information security, in: Proc. Layered Assurance Workshop, 2012, pp. 1–12, available at: http://www.acsac.org/2012/workshops/law/.

10.

[10]

Clark and

Hunt, Non-interference for deterministic interactive programs, in: Proc. Workshop on Formal Aspects in Security and Trust, FAST’08, LNCS, Vol. 5491, Springer, 2009, pp. 50–66.

11.

[11]

Eggert,

Schnoor and

Wilke, Noninterference with local policies, in: MFCS, LNCS, Vol. 8087, Springer, 2013, pp. 337–348.

12.

[12]

Eggert,

van der Meyden,

Schnoor and

Wilke, The complexity of intransitive noninterference, in: Proc. IEEE Symposium on Security and Privacy, 2011, pp. 196–211.

13.

[13]

Fagin,

J.Y.

Halpern,

Moses and

M.Y.

Vardi, Reasoning About Knowledge, MIT Press, 1995.

14.

[14]

Focardi and

Gorrieri, Classification of security properties (Part I: information flow), in: Foundations of Security Analysis and Design, FOSAD 2000, Bertinoro, Italy, September 2000,

Focardi and

Gorrieri, eds, LNCS, Vol. 2171, Springer, 2001, pp. 331–396.

15.

[15]

J.A.

Goguen and

Meseguer, Security policies and security models, in: Proc. IEEE Symp. on Security and Privacy, Oakland, 1982, pp. 11–20.

16.

[16]

J.A.

Goguen and

Meseguer, Unwinding and inference control, in: IEEE Symp. on Security and Privacy, 1984, pp. 75–87.

17.

[17]

Gorrieri and

Vernali, On intransitive non-interference in some models of concurrency, in: Foundations of Security Analysis and Design VI – FOSAD Tutorial Lectures, LNCS, Vol. 6858, Springer, 2011, pp. 125–151.

18.

[18]

Greve,

Wilding and

Vanfleet, A separation kernel formal security policy, in: Proc. Fourth International Workshop on the ACL2 Theorem Prover and Its Applications, 2003, Paper and associated proof scripts available at: http://www.cs.utexas.edu/users/moore/acl2/workshop-2003/.

19.

[19]

J.T.

Haigh and

W.D.

Young, Extending the noninterference version of MLS for SAT, IEEE Trans. on Software Engineering SE-13(2) (1987), 141–150.

20.

[20]

C.L.

Heitmeyer,

Archer,

E.I.

Leonard and

J.D.

McLean, Formal specification and verification of data separation in a separation kernel for an embedded system, in: Proc. ACM Conf. on Computer and Communications Security, 2006, pp. 346–355.

21.

[21]

D.M.

Johnson and

F.J.

Thayer, Security and the composition of machines, in: Proc. IEEE Security Foundations Workshop, 1988, pp. 72–89.

22.

[22]

M.N.

Krohn and

Tromer, Noninterference for a practical DIFC-based operating system, in: IEEE Symp. on Security and Privacy, 2009, pp. 61–76.

23.

[23]

Leslie, Dynamic intransitive noninterference, in: Proc. IEEE Int. Symp. on Secure Software Engineering, 2006.

24.

[24]

Mantel, Possibilistic definitions of security – an assembly kit, in: Proc. IEEE Computer Security Foundations Workshop, 2000, pp. 185–199.

25.

[25]

Mantel, Information flow control and applications – bridging a gap, in: FME 2001: Formal Methods for Increasing Software Productivity, Proc. Int. Symp. of Formal Methods Europe, LNCS, Vol. 2021, Springer, 2001, pp. 153–172.

26.

[26]

Mantel and

Sands, Controlled declassification based on intransitive noninterference, in: Proc. Asian Symp. on Programming Languages and Systems, LNCS, Vol. 3302, Springer-Verlag, 2004, pp. 129–145.

27.

[27]

W.B.

Martin,

White,

Goldberg and

F.S.

Taylor, Formal construction of the mathematically analyzed separation kernel, in: Proc. 15th IEEE Int. Conf. on Automated Software Engineering, 2000, pp. 133–141.

28.

[28]

McCullough, Noninterference and the composability of security properties, in: Proc. IEEE Symp. on Security and Privacy, 1988, pp. 177–186.

29.

[29]

McLean, Reasoning about security models, in: Proc. IEEE Conf. on Security and Privacy, 1987, pp. 123–131.

30.

[30]

Mullins, Nondeterministic admissible interference, Journal of Universal Computer Science 6(11) (2000), 1054–1070.

31.

[31]

M.C.

Pease,

R.E.

Shostak and

Lamport, Reaching agreement in the presence of faults, J. ACM 27(2) (1980), 228–234.

32.

[32]

Percival, Cache missing for fun and profit, available at: http://www.daemonology.net/papers/htt.pdf.

33.

[33]

A.W.

Roscoe and

M.H.

Goldsmith, What is intransitive noninterference? in: IEEE Computer Security Foundations Workshop, 1999, pp. 228–238.

34.

[34]

Rushby, Design and verification of secure systems, ACM Operating Systems Review 15(1) (1981), 12–21.

35.

[35]

Rushby, Noninterference, transitivity, and channel-control security policies, Technical Report CSL-92-02, SRI International, December 1992.

36.

[36]

P.Y.

Ryan, Mathematical models of computer security, in: Foundations of Security Analysis and Design, FOSAD 2000, Bertinoro, Italy, September 2000,

Focardi and

Gorrieri, eds, LNCS, Vol. 2171, Springer, 2001, pp. 1–62.

37.

[37]

P.Y.A.

Ryan and

S.A.

Schneider, Process algebra and non-interference, Journal of Computer Security 9(1,2) (2001), 75–103.

38.

[38]

Sabelfeld and

Sands, Dimensions and principles of declassification, in: Proceedings of the 18th IEEE Computer Security Foundations Workshop, IEEE Computer Society Press, 2005, pp. 255–269.

39.

[39]

Schellhorn,

Reif,

Schairer,

P.A.

Karger,

Austel and

D.C.

Toll, Verified formal security models for multiapplicative smart cards, Journal of Computer Security 10(4) (2002), 339–368.

40.

[40]

Sutherland, A model of information, in: Proc. 9th National Computer Security Conf., 1986, pp. 175–183.

41.

[41]

van der Meyden, A comparison of semantic models of intransitive noninterference, December 2007, Unpublished manuscript, available at: http://www.cse.unsw.edu.au/~meyden.

42.

[42]

van der Meyden and

Zhang, A comparison of semantic models for noninterference, Theoretical Computer Science 411(47) (2010), 4123–4147.

43.

[43]

von Oheimb, Information flow control revisited: Noninfluence = Noninterference + Nonleakage, in: Computer Security – ESORICS 2004, LNCS, Vol. 3193, Springer, 2004, pp. 225–243.

44.

[44]

J.T.

Wittbold and

D.M.

Johnson, Information flow in nondeterministic systems, in: Proc. IEEE Symp. on Security and Privacy, 1990, pp. 144–161.

45.

[45]

Zdancewic and

A.C.

Myers, Robust declassification, in: Proc. IEEE Computer Security Foundations Workshop, 2001.

What,indeed,is intransitive noninterference? 1

Abstract

Keywords

1. Introduction

2. Intransitive noninterference

2 In a companion paper [41] we also treat Rushby’s action-observed model, and show that the corresponding definitions in that model are related to those in the state-observed model by means of a natural mapping from action observed systems to state-observed systems.

Proposition 2 ([35, Theorem 6]).

9. Conclusion

Footnotes

Acknowledgments

References

²
In a companion paper [41] we also treat Rushby’s action-observed model, and show that the corresponding definitions in that model are related to those in the state-observed model by means of a natural mapping from action observed systems to state-observed systems.