5.2 The Bell-LaPadula Model

The Bell-LaPadula Model [67, 68] corresponds to military-style classifications. It has influenced the development of many other models and indeed much of the development of computer security technologies.^[1]

^[1] The terminology in this section follows that of the unified exposition of the Bell-LaPadula Model [68].

5.2.1 Informal Description

The simplest type of confidentiality classification is a set of security clearances arranged in a linear (total) ordering (see Figure 5-1). These clearances represent sensitivity levels. The higher the security clearance, the more sensitive the information (and the greater the need to keep it confidential). A subject has a security clearance. In the figure, Claire's security clearance is C (for CONFIDENTIAL), and Thomas' is TS (for TOP SECRET). An object has a security classification; the security classification of the electronic mail files is S (for SECRET), and that of the telephone list files is UC (for UNCLASSIFIED). (When we refer to both subject clearances and object classifications, we use the term "classification.") The goal of the Bell-LaPadula security model is to prevent read access to objects at a security classification higher than the subject's clearance.

The Bell-LaPadula security model combines mandatory and discretionary access controls. In what follows, "S has discretionary read (write) access to O" means that the access control matrix entry for S and O corresponding to the discretionary access control component contains a read (write) right. In other words, were the mandatory controls not present, S would be able to read (write) O.

Let L(S) = l_s be the security clearance of subject S, and let L(O) = l_o be the security classification of object O. For all security classifications l_i, i = 0, ..., k – 1, l_i < l_i+1.

• Simple Security Condition, Preliminary Version: S can read O if and only if l_o l_s and S has discretionary read access to O.

In Figure 5-1, for example, Claire and Clarence cannot read personnel files, but Tamara and Sally can read the activity log files (and, in fact, Tamara can read any of the files, given her clearance), assuming that the discretionary access controls allow it.

Should Tamara decide to copy the contents of the personnel files into the activity log files and set the discretionary access permissions appropriately, Claire could then read the personnel files. Thus, for all practical purposes, Claire could read the files at a higher level of security. A second property prevents this:

• *-Property (Star Property), Preliminary Version: S can write O if and only if l_s l_o and S has discretionary write access to O.

Because the activity log files are classified C and Tamara has a clearance of TS, she cannot write to the activity log files.

Define a secure system as one in which both the simple security condition, preliminary version, and the *-property, preliminary version, hold. A straightforward induction establishes the following theorem.

Theorem 5–1. Basic Security Theorem, Preliminary Version: Let S be a system with a secure initial state s₀, and let T be a set of state transformations. If every element of T preserves the simple security condition, preliminary version, and the *-property, preliminary version, then every state s_i, i 0, is secure.

Expand the model by adding a set of categories to each security classification. Each category describes a kind of information. Objects placed in multiple categories have the kinds of information in all of those categories. These categories arise from the "need to know" principle, which states that no subject should be able to read objects unless reading them is necessary for that subject to perform its functions. The sets of categories to which a person may have access is simply the power set of the set of categories. For example, if the categories are NUC, EUR, and US, someone can have access to any of the following sets of categories: Ø (none), { NUC }, { EUR }, { US }, { NUC, EUR }, {NUC, US }, { EUR, US }, and { NUC, EUR, US }. These sets of categories form a lattice under the operation (subset of); see Figure 5-2. (Chapter 30, "Lattices," discusses the mathematical nature of lattices.)

Each security level and category form a security level.^[2] As before, we say that subjects have clearance at (or are cleared into, or are in) a security level and that objects are at the level of (or are in) a security level. For example, William may be cleared into the level (SECRET, { EUR }) and George into the level (TOP SECRET, { NUC, US }). A document may be classified as (CONFIDENTIAL, {EUR }).

^[2] There is less than full agreement on this terminology. Some call security levels "compartments." However, others use this term as a synonym for "categories." We follow the terminology of the unified exposition [68].

Security levels change access. Because categories are based on a "need to know," someone with access to the category set { NUC, US } presumably has no need to access items in the category EUR. Hence, read access should be denied, even if the security clearance of the subject is higher than the security classification of the object. But if the desired object is in any of the security levels Ø, { NUC }, { US }, or { NUC, US } and the subject's security clearance is no less than the document's security classification, access should be granted because the subject is cleared into the same category set as the object.

This suggests a new relation for capturing the combination of security classification and category set. Define the relation dom (dominates) as follows.

Definition 5–1. The security level (L, C) dominates the security level (L', C') if and only if L' L and C' C.

We write (L, C) ¬dom (L', C') when (L, C) dom (L', C') is false. This relation also induces a lattice on the set of security levels [267].

EXAMPLE: George is cleared into security level (SECRET, { NUC, EUR} ), DocA is classified as ( CONFIDENTIAL, { NUC } ), DocB is classified as ( SECRET, { EUR, US}), and DocC is classified as (SECRET, { EUR }). Then: George dom DocA as CONFIDENTIAL SECRET and { NUC } { NUC, EUR } George ¬dom DocB as { EUR, US } { NUC, EUR } George dom DocC as SECRET SECRET and { EUR } { NUC, EUR }

Let C(S) be the category set of subject S, and let C(O) be the category set of object O. The simple security condition, preliminary version, is modified in the obvious way:

• Simple Security Condition: S can read O if and only if S dom O and S has discretionary read access to O.

In the example above, George can read DocA and DocC but not DocB (again, assuming that the discretionary access controls allow such access).

Suppose Paul is cleared into security level (SECRET, { EUR, US, NUC }) and has discretionary read access to DocB. Paul can read DocB; were he to copy its contents to DocA and set its access permissions accordingly, George could then read DocB. The modified *-property prevents this:

• *-Property: S can write to O if and only if O dom S and S has discretionary write access to O.

Because DocA dom Paul is false (because C(Paul) C(DocA)), Paul cannot write to DocA.

The simple security condition is often described as "no reads up" and the *-property as "no writes down."

Redefine a secure system as one in which both the simple security property and the *-property hold. The analogue to the Basic Security Theorem, preliminary version, can also be established by induction.

Theorem 5–2. Basic Security Theorem: Let S be a system with a secure initial state s₀, and let T be a set of state transformations. If every element of T preserves the simple security condition and the *-property, then every s_i, i 0, is secure.

At times, a subject must communicate with another subject at a lower level. This requires the higher-level subject to write into a lower-level object that the lower-level subject can read.

EXAMPLE: A colonel with (SECRET, { NUC, EUR }) clearance needs to send a message to a major with (SECRET, { EUR }) clearance. The colonel must write a document that has at most the (SECRET, { EUR }) classification. But this violates the *-property, because (SECRET, { NUC, EUR }) dom (SECRET, { EUR }).

The model provides a mechanism for allowing this type of communication. A subject has a maximum security level and a current security level. The maximum security level must dominate the current security level. A subject may (effectively) decrease its security level from the maximum in order to communicate with entities at lower security levels.

EXAMPLE: The colonel's maximum security level is (SECRET, { NUC, EUR }). She changes her current security level to (SECRET, { EUR }). This is valid, because the maximum security level dominates the current security level. She can then create the document at the major's clearance level and send it to him.

How this policy is instantiated in different environments depends on the requirements of each environment. The conventional use is to define "read" as "allowing information to flow from the object being read to the subject reading," and "write" as "allowing information to flow from the subject writing to the object being written." Thus, "read" usually includes "execute" (because by monitoring the instructions executed, one can determine the contents of portions of the file) and "write" includes "append" (as the information is placed in the file, it does not overwrite what is already in the file, however). Other actions may be included as appropriate; however, those who instantiate the model must understand exactly what those actions are. Chapter 8, "Noninterference and Policy Composition," and Chapter 17, "Confinement Problem," will discuss this subject in considerably more detail.

5.2.2 Example: The Data General B2 UNIX System

The Data General B2 UNIX (DG/UX) system provides mandatory access controls (MACs). The MAC label is a label identifying a particular compartment. This section describes only the default labels; the system enables other labels to be created.

5.2.2.1 Assigning MAC Labels

When a process (subject) begins, it is assigned the MAC label of its parent. The initial label (assigned at login time) is the label assigned to the user in a database called the Authorization and Authentication (A&A) Database. Objects are assigned labels at creation, but the labels may be either explicit or implicit. The system stores explicit labels as parts of the object's attributes. It determines implicit labels from the parent directory of the object.

The least upper bound of all compartments in the DG/UX lattice has the label IMPL_HI (for "implementation high"); the greatest lower bound has the label IMPL_LO (for "implementation low"). The lattice is divided into three regions, which are summarized in Figure 5-3.^[3]

^[3] The terminology used here corresponds to that of the DG/UX system. Note that "hierarchy level" corresponds to "clearance" or "classification" in the preceding section.

The highest region (administrative region) is reserved for data that users cannot access, such as logs, MAC label definitions, and so forth. Because reading up and writing up are disallowed (the latter is a DG/UX extension to the multilevel security model; see Section 5.2.2.2), users can neither read nor alter data in this region. Administrative processes such as servers execute with MAC labels in this region; however, they sanitize data sent to user processes with MAC labels in the user region.

System programs are in the lowest region (virus prevention region). No user process can write to them, so no user process can alter them. Because execution requires read access, users can execute the programs. The name of this region comes from the fact that viruses and other forms of malicious logic involve alterations of trusted executables.^[4]

^[4] The TCB, or trusted computing base, is that part of the system that enforces security (see Section 19.1.2.2).

Problems arise when programs of different levels access the same directory. If a program with MAC label MAC_A tries to create a file, and a file of that name but with MAC label MAC_B (MAC_B dom MAC_A) exists, the create will fail. To prevent this leakage of information, only programs with the same MAC label as the directory can create files in that directory. For the /tmp directory, and the mail spool directory /var/mail, this restriction will prevent standard operations such as compiling and delivering mail. DG/UX introduces a "multilevel directory" to solve this problem.

A multilevel directory is a directory with a set of subdirectories, one for each label. These "hidden directories" normally are not visible to the user, but if a process with MAC label MAC_A tries to create a file in /tmp, it actually creates a file in the hidden directory under /tmp with MAC label MAC_A. The file can have the same name as one in the hidden directory corresponding to label MAC_A. The parent directory of a file in /tmp is the hidden directory. Furthermore, a reference to the parent directory goes to the hidden directory.

EXAMPLE: A process with label MAC_A creates a directory /tmp/a. Another process with label MAC_B creates a directory /tmp/a. The processes then change the correct working directory to /tmp/a and then to .. (the parent directory). Both processes will appear to have /tmp as the current working directory. However, the system call stat(".", &stat_buffer) returns a different inode number for each process, because it returns the inode number of the current working directory—the hidden directory. The system call dg_mstat(".", &stat_buffer) translates the notion of "current working directory" to the multilevel directory when the current working directory is a hidden directory.

Mounting unlabeled file systems requires the files to be labeled. Symbolic links aggravate this problem. Does the MAC label the target of the link control, or does the MAC label the link itself? DG/UX uses a notion of inherited labels (called implicit labels) to solve this problem. The following rules control the way objects are labeled.

Rules 1 and 2 ensure that every file system object has a MAC label, either implicit or explicit. But when a file object has an implicit label, and two hard links from different directories, it may have two labels. Let /x/y/z and /x/a/b be hard links to the same object. Suppose y has an explicit label IMPL_HI and a an explicit label IMPL_B. Then the file object can be accessed by a process at IMPL_HI as /x/y/z and by a process at IMPL_B as /x/a/b. Which label is correct? Two cases arise.

Suppose the hard link is created while the file system is on a DG/UX B2 system. Then the DG/UX system converts the target's implicit label to an explicit one (rule 3). Thus, regardless of the path used to refer to the object, the label of the object will be the same.

Suppose the hard link exists when the file system is mounted on the DG/UX B2 system. In this case, the target had no file label when it was created, and one must be added. If no objects on the paths to the target have explicit labels, the target will have the same (implicit) label regardless of the path being used. But if any object on any path to the target of the link acquires an explicit label, the target's label may depend on which path is taken. To avoid this, the implicit labels of a directory's children must be preserved when the directory's label is made explicit. Rule 4 does this.

Because symbolic links interpolate path names of files, rather than store inode numbers, computing the label of symbolic links is straightforward. If /x/y/z is a symbolic link to /a/b/c, then the MAC label of c is computed in the usual way. However, the symbolic link itself is a file, and so the process must also have access to the link file z.

5.2.2.2 Using MAC Labels

The DG/UX B2 system uses the Bell-LaPadula notion of dominance, with one change. The system obeys the simple security condition (reading down is permitted), but the implementation of the *-property requires that the process MAC label and the object MAC label be equal, so writing up is not permitted, but writing is permitted in the same compartment.

Because of this restriction on writing, the DG/UX system provides processes and objects with a range of labels called a MAC tuple. A range is a set of labels expressed by a lower bound and an upper bound. A MAC tuple consists of up to three ranges (one for each of the regions in Figure 5-3).

EXAMPLE: A system has two security levels, TS and S, the former dominating the latter. The categories are COMP, NUC, and ASIA. Examples of ranges are [( S, { COMP } ), ( TS, { COMP } )] [( S, Ø ), ( TS, { COMP, NUC, ASIA } )] [( S, { ASIA } ), ( TS, { ASIA, NUC } )] The label ( TS, {COMP} ) is in the first two ranges. The label ( S, {NUC, ASIA} ) is in the last two ranges. However, [( S, {ASIA} ), ( TS, { COMP, NUC} )] is not a valid range because ( TS, { COMP, NUC } ) dom ( S, { ASIA } ).

An object can have a MAC tuple as well as the required MAC label. If both are present, the tuple overrides the label. A process has read access when its MAC label grants read access to the upper bound of the range. A process has write access when its MAC label grants write access to any label in the MAC tuple range.

EXAMPLE: Suppose an object's MAC tuple is the single range [( S, { ASIA } ), ( TS, { ASIA, COMP} )] A subject with MAC label ( S, { ASIA } ) cannot read the object, because ( TS, { ASIA, COMP} ) dom ( S, { ASIA } ) It can write to the object, because (S, { ASIA }) dominates the lower bound and is dominated by the upper bound. A subject with MAC label ( TS, { ASIA, COMP, NUC } ) can read the object but cannot write the object. A subject with MAC label (TS, { ASIA, COMP } ) can both read and write the object. A subject with MAC label (TS, {EUR} ) can neither read nor write the object, because its label is incomparable to that of the object, and the dom relation does not hold.

A process has both a MAC label and a MAC tuple. The label always lies within the range for the region in which the process is executing. Initially, the subject's accesses are restricted by its MAC label. However, the process may extend its read and write capabilities to within the bounds of the MAC tuple.

5.2.3 Formal Model

Let S be the set of subjects of a system and let O be the set of objects. Let P be the set of rights r for read, q for write, w for read/write, and e for empty.^[5] Let M be a set of possible access control matrices for the system. Let C be the set of classifications (or clearances), let K be the set of categories, and let L = C x K be the set of security levels. Finally, let F be the set of 3-tuples (f_s, f_o, f_c), where f_s and f_c associate with each subject maximum and current security levels, respectively, and f_o associates with each object a security level. The relation dom from Definition 5–1 is defined here in the obvious way.

^[5] The right called "empty" here is called "execute" in Bell and LaPadula [68]. However, they define "execute" as "neither observation nor alteration" (and note that it differs from the notion of "execute" that most systems implement). For clarity, we changed the e right's name to the more descriptive "empty."

The system objects may be organized as a set of hierarchies (trees and single nodes). Let H represent the set of hierarchy functions h: O P(O).^[6] These functions have two properties. Let o_i, o_j, o_k O. Then:

^[6] P(O) is the power set of O—that is, the set of all possible subsets of O.

(See Exercise 6.)

A state n n of a system is a 4-tuple (b, m, f, h), where b P(S x O x P) indicates which subjects have access to which objects, and what those access rights are; m M is the access control matrix for the current state; f F is the 3-tuple indicating the current subject and object clearances and categories; and h H is the hierarchy of objects for the current state. The difference between b and m is that the rights in m may be unusable because of differences in security levels; b contains the set of rights that may be exercised, and m contains the set of discretionary rights.

R denotes the set of requests for access. The form of the requests affects the instantiation, not the formal model, and is not discussed further here. Four outcomes of each request are possible: y for yes (allowed), n for no (not allowed), i for illegal request, and o for error (multiple outcomes are possible). D denotes the set of outcomes. The set W R x D x n x n is the set of actions of the system. This notation means that an entity issues a request in R, and a decision in D occurs, moving the system from one state in n to another (possibly different) state in n. Given these definitions, we can now define the history of a system as it executes.

Let N be the set of positive integers. These integers represent times. Let X = R^N be a set whose elements x are sequences of requests, let Y = D^N be a set whose elements y are sequences of decisions, and let Z = V^N be a set whose elements z are sequences of states. The ith components of x, y, and z are represented as x_i, y_i, and z_i, respectively. The interpretation is that for some t N, the system is in state z_t–1 n; a subject makes request x_t R, the system makes a decision y_t D, and as a result the system transitions into a (possibly new) state z_t n.

A system is represented as an initial state and a sequence of requests, decisions, and states. In formal terms, S(R, D, W, z₀) X x Y x Z represents the system, and z₀ is the initial state of the system. (x, y, z) S(R, D, W, z₀) if and only if (x_t, y_t, z_t, z_t–1) W for all t N. (x, y, z) is an appearance of S(R, D, W, z₀).

EXAMPLE: Consider a system with two levels (HIGH and LOW), one category (ALL), one subject s, one object o, and two rights, read (r) and write (w). Then: S = { s }, O = { o }, P = { r, w }, C = { HIGH, LOW }, K = { ALL } For every function f F, fc(s) is either (LOW, { ALL}) or (HIGH, { ALL}), and fo(o) is either (LOW, { ALL}) or (HIGH, { ALL}). Now, suppose b1 = { (s, o, r) }, m1 M gives s read access over o, and for f1 F, fc,1(s) = (HIGH, { ALL}) and fo,1(o) = (LOW, { ALL}). This describes a state of the system in which s has read rights to o, so n0 = (b1, m1, f1) n. Now suppose S = { s,s' },fs,1(s')=(LOW, { ALL}), and m1 gives s' write access over o as well as giving s read access over o. Becauses s' has not yet written o, b1 is unchanged. Take z0=(b1,m1,f1) and consider the system S(R, D, W, z0). If s' makes the request r1 to write to o, the system will decide d1 = y (yes), and will transition to the state n1 = (b2, m1, f1) n, where b2 = { (s, o, r), (s', o, w) }. In this case, x = (r1), y = (yes), and z = (n0, n1).

The next request r₂ is for s to write to o; however, this is disallowed (d₂ = n, or no). The resulting state is the same as the preceding one. Now x = (r₁, r₂), y = (y, n), and z = (n₀, n₁, n₂), where n₂ = v₁.

5.2.3.1 Basic Security Theorem

The Basic Security Theorem combines the simple security condition, the *-property, and a discretionary security property. We now formalize these three properties.

Formally, the simple security condition is:

Definition 5–2. (s, o, p) S x O x P satisfies the simple security condition relative to f (written ssc rel f) if and only if one of the following holds:

1. p = e or p = a

2. p = r or p = w and f_c(s) dom f_o(o)

In other words, if s can read o (or read and write to it), s must dominate o. A state (b, m, f, h) satisfies the simple security condition if all elements of b satisfy ssc rel f. A system satisfies the simple security condition if all its states satisfy the simple security condition.

Define b(s: p₁, ..., p_n) to be the set of all objects that s has p₁, ..., p_n access to:

b(s: p₁, ..., p_n) = { o | o O [ (s, o, p₁) b v ... v (s, o, p_n) b ] }

Definition 5–3. A state (b, m, f, h) satisfies the *-property if and only if, for each s S, the following hold:

1. b(s: a) Ø [ o b(s: a) [ f_o(o) dom f_c(s) ] ]

2. b(s: w) Ø [ o b(s: w) [ f_o(o) = f_c(s) ] ]

3. b(s: r) Ø [ o b(s: r) [ f_c(s) dom f_o(o) ] ]

This definition says that if a subject can write to an object, the object's classification must dominate the subject's clearance ("write up"); if the subject can also read the object, the subject's clearance must be the same as the object's classification ("equality for read"). A system satisfies the *-property if all its states satisfy the *-property. In many systems, only a subset S' of subjects satisfy the *-property; in this case, we say that the *-property is satisfied relative to S' S.

Definition 5–4. A state (b, m, f, h) satisfies the discretionary security property (ds-property) if and only if, for each triple (s, o, p) b, p m[s, o].

The access control matrix allows the controller of an object to condition access based on identity. The model therefore supports both mandatory and discretionary controls, and defines "secure" in terms of both. A system satisfies the discretionary security property if all its states satisfy the discretionary security property.

Definition 5–5. A system is secure if it satisfies the simple security condition, the *-property, and the discretionary security property.

The notion of an action, or a request and decision that moves the system from one state to another, must also be formalized, as follows.

Definition 5–6. (r, d, v, v') R x D x n x n is an action of S(R, D, W, z₀) if and only if there is an (x, y, z) S(R, D, W, z₀) and a t N such that (r, d, v, v') = (x_t, y_t, z_t, z_t–1).

Thus, an action is a request/decision pair that occurs during the execution of the system.

We now can establish conditions under which the three properties hold.

Theorem 5–3. S(R, D, W, z₀) satisfies the simple security condition for any secure state z₀ if and only if, for every action (r, d, (b, m, f, h), (b', m', f', h')), W satisfies the following:

1. Every (s, o, p) b – b' satisfies ssc rel f.

2. Every (s, o, p) b' that does not satisfy ssc rel f is not in b.

Proof Let (x, y, z) S(R, D, W, z₀) and write z_t = (b_t, a_t, f_t) for t N.

() By contradiction. Without loss of generality, take b = b_t and b' = b_t–1. Assume that S(R, D, W, z₀) satisfies the simple security condition for some secure state z₀, and that either some (s, o, p) b – b' = b_t – b_t–1 does not satisfy ssc rel f_t or some (s, o, p) b' = b_t–1 that does not satisfy ssc rel f_t is in b = b_t. If the former, there is some (s, o, p) b_t that does not satisfy ssc rel f_t, because b_t – b_t–1 b_t. If the latter, there is some (s, o, p) b_t–1 that does not satisfy ssc rel f_t but that is in b_t. In either case, there is some (s, o, p) b_t that does not satisfy the simple security condition relative to f_t, which means that S(R, D, W, z₀) does not satisfy the simple security condition for some secure state z₀, contradicting the hypothesis.

() By induction on t.

Induction basis. z₀ = (b₀, m₀, f₀, h₀) is secure, by the hypothesis of the claim.

Induction hypothesis. z_t–1 = (b_t–1, m_t–1, f_t–1, h_t–1) is secure, for t < n

Induction step. Let (x_t, y_t, z_t, z_t–1) W. By (a), every (s, o, p) b_t – b_t–1 satisfies ssc rel f_t. Let = { (s, o, p) | (s, o, p) b_t–1 (s, o, p) does not satisfy ssc rel f_t }. By (b), b_t = Ø; so, (b_t b_t–1) = ( b_t) b_t–1 = Ø. This means that if (s, o, p) b_t b_t–1, then (s, o, p) and so (s, o, p) satisfies ssc rel f_t. Hence, if (s, o, p) b_t, then either (s, o, p) b_t b_t–1 or (s, o, p) b_t – b_t–1. In the first case, the induction hypothesis ensures that (s, o, p) satisfies the simple security condition. In the second case, (a) ensures that (s, o, p) satisfies the simple security condition. Hence, z_t = (b_t, m_t, f_t, h_t) is secure. This completes the proof.

Theorem 5–4. S(R, D, W, z₀) satisfies the *-property relative to S' S for any secure state z₀ if and only if, for every action (r, d, (b, m, f, h), (b', m', f', h')), W satisfies the following for every s S':

1. Every (s, o, p) b – b' satisfies the *-property with respect to S'.

2. Every (s, o, p) b' that does not satisfy the *-property with respect to S' is not in b.

Proof See Exercise 8.

Theorem 5–5. S(R, D, W, z₀) satisfies the ds-property for any secure state z₀ if and only if, for every action (r, d, (b, m, f, h), (b', m', f', h')), W satisfies the following:

1. Every (s, o, p) b – b' satisfies the ds-property.

2. Every (s, o, p) b' that does not satisfy the ds-property is not in b.

Proof See Exercise 9.

Theorems 5–3, 5–4, and 5–5 combine to give us the Basic Security Theorem:

Theorem 5–6. Basic Security Theorem: S(R, D, W, z₀) is a secure system if z₀ is a secure state and W satisfies the conditions of Theorems 5–3, 5–4, and 5–5.

Proof Immediate from Theorems 5–3, 5–4, and 5–5.

5.2.3.2 Rules of Transformation

A rule is a function r:R x nD x n. Intuitively, a rule takes a state and a request, and determines if the request meets the conditions of the rule (the decision). If so, it moves the system to a (possibly different) state. The idea is that a rule captures the means by which a system may transition from one state to another.

Of course, the rules affect the security of a system. For example, a rule that changes all read rights so that a subject has the ability to read objects with classifications higher than the subject's clearance may move the system from a secure state to a nonsecure state. In this section we develop constraints that rules must meet to preserve security, and we give an example rule.

Definition 5–7. A rule r is ssc-preserving if, for all (r, v) R x n and n satisfying ssc rel f, r(r, v) = (d, v') means that n' satisfies ssc rel f'.

Similar definitions hold for the *-property and the ds-property. If a rule is ssc-preserving, *-property-preserving, and ds-property-preserving, the rule is said to be security-preserving.

We define a relation with respect to a set of rules w = { r₁, ..., r_m } in such a way that each type of request is handled by at most one rule; this eliminates ambiguity and ensures that the mapping from R x n to D x n is one-to-one.

Definition 5–8. Let w = { r₁, ..., r_m } be a set of rules. For request r R, decision d D, and states v, v' n, (r, d, v, v') W(w) if and only if d i and there is a unique integer i, 1 i m, such that r_i(r, v) = (d, v').

This definition says that if the request is legal and there is only one rule that will change the state of the system from n to n', the corresponding action is in W(w).

The next theorem presents conditions under which a set of rules preserves the simple security condition.

Theorem 5–7. Let w be a set of ssc-preserving rules, and let z₀ be a state satisfying the simple security condition. Then S(R, D, W, z₀) satisfies the simple security condition.

Proof By contradiction. Let (x, y, z) S(R, D, W(w), z₀) be a state that does not satisfy the simple security property. Without loss of generality, choose t N such that (x_t, y_t, z_t) is the first appearance of S(R, D, W(w), z₀) that does not satisfy the simple security property. Because (x_t, y_t, z_t, z_t–1) W(w), there is a unique rule r w such that r(x_t, z_t–1) = (y_t, z_t), and y_t i. Because r is ssc-preserving, and z_t–1 satisfies the simple security condition, by Definition 5–7, z_t must meet the simple security condition. This contradicts our choice of t, and the assumption that (x, y, z) does not meet the simple security property. Hence, the theorem is proved.

When does adding a state preserve the simple security property?

Theorem 5–8. Let n = (b, m, f, h) satisfy the simple security condition. Let (s, o, p) b, b' = b { (s, o, p) }, and n' = (b', m, f, h). Then n' satisfies the simple security condition if and only if either of the following conditions is true.

1. Either p = e or p = a.

2. Either p = r or p = w, and f_s(s) dom f_o(o).

Proof For (a), the theorem follows from Definition 5–3 and n' satisfying ssc rel f. For (b), if n' satisfies the simple security condition, then, by definition, f_s(s) dom f_o(o). Moreover, if f_s(s) dom f_o(o), then (s, o, p) b' satisfies ssc rel f; hence, v' is secure.

Similar theorems hold for the *-property:

Theorem 5–9. Let w be a set of *-property-preserving rules, and let z₀ be a state satisfying the *-property. Then S(R, D, W, z₀) satisfies the *-property.

Proof See Exercise 11.

Theorem 5–10. Let n = (b, m, f, h) satisfy the *-property. Let (s, o, p) b, b' = b { (s, o, p) }, and n' = (b', a, f, h). Then v' satisfies the *-property if and only if one of the following conditions holds.

1. p = a and f_o(o) dom f_c(s)

2. p = w and f_o(o) = f_c(s)

3. p = r and f_c(s) dom f_o(o)

Proof If n' satisfies the *-property, then the claim follows immediately from Definition 5–3. Conversely, assume that conditions (a), (b), and (c) hold. Let (s', o', p') b'. If (s', o', p') b, the assumption that n satisfies the *-property means that n' also satisfies the *-property. Otherwise, (s', o', p') = (s, o, p) and, by conditions (a), (b), and (c), the *-property holds. Thus, n' satisfies the *-property.

Theorem 5–11. Let w be a set of ds-property-preserving rules, and let z₀ be a state satisfying the ds-property. Then S(R, D, W, z₀) satisfies the ds-property.

Proof See Exercise 11.

Theorem 5–12. Let n = (b, m, f, h) satisfy the ds-property. Let (s, o, p) b, b' = b { (s, o, p) }, and n' = (b', m, f, h). Then v' satisfies the ds-property if and only if p m[s, o].

Proof If n' satisfies the ds-property, then the claim follows immediately from Definition 5–4. Conversely, assume that p m[s, o]. Because (s', o', p') b', the ds-property holds for n'. Thus, n' satisfies the ds-property.

Finally, we present the following theorem.

Theorem 5–13. Let r be a rule and r(r, v) = (d, v'), where n = (b, m, f, h) and n' = (b', m', f', h'). Then:

1. If b' b, f' = f, and n satisfies the simple security condition, then v' satisfies the simple security condition.

2. If b' b, f' = f, and n satisfies the *-property, then v' satisfies the *-property.

3. If b' b, m[s, o] m'[s, o] for all s S and o O, and n satisfies the dsproperty, then v' satisfies the ds-property.

Proof Suppose that n satisfies the simple security property. Because b' b, (s, o, r) b' implies (s, o, r) b, and (s, o, w) b' implies (s, o, w) b. So f_s(s) dom f_o(o). But f' = f. Thus, f_s'(s) dom f_o'(o). So n' satisfies the simple security condition.

The proofs of the other two parts are analogous.

5.2.4 Example Model Instantiation: Multics

We now examine the modeling of specific actions. The Multics system [68, 788] has 11 rules affecting the rights on the system. These rules are divided into five groups. Let the set Q contain the set of request operations (such as get, give, and so forth). Then:

Then, the set of requests R = R⁽¹⁾ R⁽²⁾ R⁽³⁾ R⁽⁴⁾ R⁽⁵⁾.

The Multics system includes the notion of trusted users. The system does not enforce the *-property for this set of subjects S_T S; however, members of S_T are trusted not to violate that property.

For each rule r, define D(r) as the domain of the request (that is, whether or not the components of the request form a valid operand for the rule).

We next consider two rules in order to demonstrate how to prove that the rules preserve the simple security property, the *-property, and the discretionary security property.

5.2.4.1 The get-read Rule

The get-read rule enables a subject s to request the right to read an object o. Represent this request as r = (get, s, o, r) R⁽¹⁾, and let the current state of the system be n = (b, m, f, h). Then get-read is the rule r₁(r, v):

if (r  D(r₁)) then r₁(r, v) = (i, n);
else if (f_s(s) dom f_o(o) and [s  S_T or f_c(s) dom f_o(o)] and r  m[s, o])
            then r₁(r, v) = (y, (b  { (s, o, r) }, m, f, h));
else r₁(r, v) = (n, n);

The first if tests the parameters of the request; if any of them are incorrect, the decision is "illegal" and the system state remains unchanged. The second if checks three conditions. The simple security property for the maximum security level of the subject and the classification of the object must hold. Either the subject making the request must be trusted, or the simple security property must hold for the current security level of the subject (this allows trusted subjects to read information from objects above their current security levels but at or below their maximum security levels; they are trusted not to reveal the information inappropriately). Finally, the discretionary security property must hold. If these three conditions hold, so does the Basic Security Theorem. The decision is "yes" and the system state is updated to reflect the new access. Otherwise, the decision is "no" and the system state remains unchanged.

We now show that if the current state of the system satisfies the simple security condition, the *-property, and the ds-property, then after the get-read rule is applied, the state of the system also satisfies those three conditions.

Theorem 5–14. The get-read rule r₁ preserves the simple security condition, the *-property, and the ds-property.

Proof Let n satisfy the simple security condition, the *-property, and the ds-property. Let r₁(r, v) = (d, v'). Either n' = n or n' = (b { (s₂, o, r) }, m, f, h), by the get-read rule. In the former case, because n satisfies the simple security condition, the *-property, and the ds-property, so does n'. So let n' = (b { (s₂, o, r) }, m, f, h).

Consider the simple security condition. From the choice of n', either b' – b = Ø or b' – b = { (s₂, o, r) }. If b' – b = Ø, then { (s₂, o, r) } b, so n = n', proving that v' satisfies the simple security condition. Otherwise, because the get-read rule requires that f_c(s) dom f_o(o), Theorem 5–8 says that n' satisfies the simple security condition.

Consider the *-property. From the definition of the get-read rule, either s S_T or f_c(s) dom f_o(o). If s S_T, then s is trusted and the *-property holds by the definition of S_T. Otherwise, by Theorem 5–10, because f_c(s) dom f_o(o), n' satisfies the *-property.

Finally, consider the ds-property. The condition in the get-read rule requires that r m[s, o] and b' – b = Ø or b' – b = { (s₂, o, r) }. If b' – b = Ø, then { (s₂, o, r) } b, so n = n', proving that v' satisfies the ds-property. Otherwise, { (s₂, o, r) } b, which meets the conditions of Theorem 5–12. From that theorem, v' satisfies the ds-property.

Hence, the get-read rule preserves the security of the system.

5.2.4.2 The give-read Rule

The give-read rule^[7] enables a subject s to give subject s₂ the (discretionary) right to read an object o. Conceptually, a subject can give another subject read access to an object if the giver can alter (write to) the parent of the object. If the parent is the root of the hierarchy containing the object, or if the object itself is the root of the hierarchy, the subject must be specially authorized to grant access.

^[7] Actually, the rule is give-read/execute/write/append. The generalization is left as an exercise for the reader.

Some terms simplify the definitions and proofs. Define root(o) as the root object of the hierarchy h containing o, and define parent(o) as the parent of o in h. If the subject is specially authorized to grant access to the object in the situation just mentioned, the predicate canallow(s, o, v) is true. Finally, define m m[s, o]r as the access control matrix m with the right r added to entry m[s, o].

Represent the give-read request as r = (s₁, give, s₂, o, r) R⁽²⁾, and let the current state of the system be n = (b, m, f, h). Then, give-read is the rule r₆(r, v):

if (r  D(r₆)) then r₁(r, v) = (i, n);
else if ( [ o  root(o) and parent(o)  root(o) and parent(o)  b(s₁: w)] or
           [ parent(o) = root(o) and canallow(s₁, o, v) ] or
           [ o = root(o) and canallow(s₁, root(o), n) ])
           then r₁(r, v) = (y, (b, m  m[s₂, o]r, f, h));
else r₁(r, v) = (n, n);

The first if tests the parameters of the request; if any of them are incorrect, the decision is "illegal" and the system state remains unchanged. The second if checks several conditions. If neither the object nor its parent is the root of the hierarchy containing the object, then s₁ must have write rights to the parent. If the object or its parent is the root of the hierarchy, then s₁ must have special permission to give s₂ the read right to o. The decision is "yes" and the access control matrix is updated to reflect the new access. Otherwise, the decision is "no" and the system state remains unchanged.

We now show that if the current state of the system satisfies the simple security condition, the *-property, and the ds-property, then after the give-read rule is applied, the state of the system also satisfies those three conditions.

Theorem 5–15. The give-read rule r₆ preserves the simple security condition, the *-property, and the ds-property.

Proof Let n satisfy the simple security condition, the *-property, and the ds-property. Let r₆(r, v) = (d, v'). Either n' = n or n' = (b, m m[s, o]r, f, h), by the give-read rule. In the former case, because n satisfies the simple security condition, the *-property, and the ds-property, so does n'. So, let n' = (b, m m[s, o]r, f, h).

Here, b' = b, f' = f, and m[x, y] = m'[x, y] for all x S and y O such that x s and y o. In that case, m[s, o] m'[s, o]. Hence, by Theorem 5–13, v' satisfies the simple security condition, the *-property, and the ds-property.

Hence, the get-read rule preserves the security of the system.