|
|
|
The Bell-LaPadula Model became the target of inquiries into the foundations of computer security. The controversy led to a reexamination of security models and a deeper appreciation of the complexity of modeling real systems.
-Property and the Basic Security TheoremIn a 1985 paper [682], McLean argued that the "value of the [Basic Security Theorem] is much overrated since there is a great deal more to security than it captures. Further, what is captured by the [Basic Security Theorem] is so trivial that it is hard to imagine a realistic security model for which it does not hold" ([682], p. 47). The basis for McLean's argument was that given assumptions known to be nonsecure, the Basic Security Theorem could prove a nonsecure system to be secure. He defined a complement to the *-property:
Definition 5–11. A state (b, m, f, h) satisfies the
S, the following conditions hold:
b(s: a)
Ø
[
o
b(s: w)
b(s: r)
In other words, the -property holds for a subject s and an object o if and only if the clearance of s dominates the classification of o. This is exactly the reverse of the *property, which holds if and only if the classification of o dominates the clearance of s. A state satisfies the -property if and only if, for every triplet (s, o, p), where the right p involves writing (that is, p = a or p = w), the -property holds for s and o.
McLean then proved the analogue to Theorem 5–4:
Theorem 5–16. S(R, D, W, z0) satisfies the
S for any secure state z0 if and only if, for every action (r, d, (b, m, f, h), (b', m', f', h')), W satisfies the following conditions for every s
Every (s, o, p)
Every (s, o, p)
Proof See Exercise 8, with "*-property" replaced by "
From this theorem, and from Theorems 5–3 and 5–5, the analogue to the Basic Security Theorem follows.
Theorem 5–17. Basic Security Theorem: S(R, D, W, z0) is a secure system if and only if z0 is a secure state and W satisfies the conditions of Theorems 5–3, 5–16, and 5–5.
However, the system S(R, D, W, z0) is clearly nonsecure, because a subject with HIGH clearance can write information to an object with LOW classification. Information can flow down, from HIGH to LOW. This violates the basic notion of security in the confidentiality policy.
Consider the role of the Basic Security Theorem in the Bell-LaPadula Model. The goal of the model is to demonstrate that specific rules, such as the get-read rule, preserve security. But what is security? The model defines that term using the Basic Security Theorem: an instantiation of the model is secure if and only if the initial state satisfies the simple security condition, the *-property, and the ds-property, and the transition rules preserve those properties. In essence, the theorems are assertions about the three properties.
The rules describe the changes in a particular system instantiating the model. Showing that the system is secure, as defined by the analogue of Definition 5–5, requires proving that the rules preserve the three properties. Given that they do, the Basic Security Theorem asserts that reachable states of the system will also satisfy the three properties. The system will remain secure, given that it starts in a secure state.
LaPadula pointed out that McLean's statement does not reflect the assumptions of the Basic Security Theorem [617]. Specifically, the Bell-LaPadula Model assumes that a transition rule introduces no changes that violate security, but does not assume that any existing accesses that violate security are eliminated. The rules instantiating the model do no elimination (see the get-read rule, Section 5.2.4.1, as an example).
Furthermore, the nature of the rules is irrelevant to the model. The model accepts a definition of "secure" as axiomatic. The specific policy defines "security" and is an instantiation of the model. The Bell-LaPadula Model uses a military definition of security: information may not flow from a dominating entity to a dominated entity. The *-property captures this requirement. But McLean's variant uses a different definition: rather than meet the *-property, his policy requires that information not flow from a dominated entity to a dominating entity. This is not a confidentiality policy. Hence, a system satisfying McLean's policy will not satisfy a confidentiality policy. McLean's argument eloquently makes this point.
However, the sets of properties in both policies (the confidentiality policy and McLean's variant) are inductive, and the Basic Security Theorem holds. The properties may not make sense in a real system, but this is irrelevant to the model. It is very relevant to the interpretation of the model, however. The confidentiality policy requires that information not flow from a dominating subject to a dominated object. McLean substitutes a policy that allows this. These are alternative instantiations of the model.
McLean makes these points by stating problems that are central to the use of any security model. The model must abstract the notion of security that the system is to support. For example, McLean's variant of the confidentiality policy does not provide a correct definition of security for military purposes. An analyst examining a system could not use this variant to show that the system implemented a confidentiality classification scheme. The Basic Security Theorem, and indeed all theorems, fail to capture this, because the definition of "security" is axiomatic. The analyst must establish an appropriate definition. All the Basic Security Theorem requires is that the definition of security be inductive.
McLean's second observation asks whether an analyst can prove that the system being modeled meets the definition of "security." Again, this is beyond the province of the model. The model makes claims based on hypotheses. The issue is whether the hypotheses hold for a real system.
In a second paper [683], McLean sharpened his critique. System transitions can alter any system component, including b, f, m, and h, as long as the new state does not violate security. McLean used this property to demonstrate a system, called System Z, that satisfies the model but is not a confidentiality security policy. From this, he concluded that the Bell-LaPadula Model is inadequate for modeling systems with confidentiality security policies.
System Z has the weak tranquility property and supports exactly one action. When a subject requests any type of access to any object, the system downgrades all subjects and objects to the lowest security level, adds access permission to the access control matrix, and allows the access.
Let System Z's initial state satisfy the simple security condition, the *property, and the ds-property. It can be shown that successive states of System Z also satisfy those properties and hence System Z meets the requirements of the Basic Security Theorem. However, with respect to the confidentiality security policy requirements, the system clearly is not secure, because all entities are downgraded.
McLean reformulated the notion of a secure action. He defined an alternative version of the simple security condition, the *-property, and the discretionary security property. Intuitively, an action satisfies these properties if, given a state that satisfies the properties, the action transforms the system into a (possibly different) state that satisfies these properties, and eliminates any accesses present in the transformed state that would violate the property in the initial state. From this, he shows:
Theorem 5–18. S(R, D, W, z0) is a secure system if z0 is a secure state and each action in W satisfies the alternative versions of the simple security condition, the *-property, and the discretionary security property.
Proof See [683].
Under this reformulation, System Z is not secure because this rule is not secure. Specifically, consider an instantiation of System Z with two security clearances, (HIGH, { ALL }) and (LOW, { ALL }) (HIGH > LOW). The initial state has a subject s and an object o. Take fc(s) = (LOW, { ALL }), fo(o) = (HIGH, { ALL }), m[s, o] = { w }, and b = { (s, o, w) }. When s requests read access to o, the rule transforms the system into a state wherein fo'(o) = (LOW, { ALL }), (s, o, r) b', and m'[s, o] = { r, w }. However, because (s, o, r) b' – b and fo(o) dom fs(s), an illegal access has been added. Yet, under the traditional Bell-LaPadula formulation, in the final state fc'(s) = fo'(o), so the read access is legal and the state is secure, hence the system is secure.
McLean's conclusion is that proving that states are secure is insufficient to prove the security of a system. One must consider both states and transitions.
Bell [64] responded by exploring the fundamental nature of modeling. Modeling in the physical sciences abstracts a physical phenomenon to its fundamental properties. For example, Newtonian mathematics coupled with Kepler's laws of planetary motion provide an abstract description of how planets move. When observers noted that Uranus did not follow those laws, they calculated the existence of another, trans-Uranean planet. Adams and Lavoisier, observing independently, confirmed its existence. Refinements arise when the theories cannot adequately account for observed phenomena. For example, the precession of Mercury's orbit suggested another planet between Mercury and the sun. But none was found.[8] Einstein's theory of general relativity, which modified the theory of how planets move, explained the precession, and observations confirmed his theory.
[8] Observers reported seeing this planet, called Vulcan, in the mid-1800s. The sighting was never officially confirmed, and the refinements discussed above explained the precession adequately. Willy Ley's book [625] relates the charming history of this episode.
Modeling in the foundations of mathematics begins with a set of axioms. The model demonstrates the consistency of the axioms. A model consisting of points, lines, planes, and the axioms of Euclidean geometry can demonstrate the consistency of those axioms. Attempts to prove the inconsistency of a geometry created without the Fifth Postulate[9] failed; eventually, Riemann replaced the plane with a sphere, replaced lines with great circles, and using that model demonstrated the consistency of the axioms (which became known as "Riemannian geometry"). Gödel demonstrated that consistency cannot be proved using only axioms within a system (hence Riemannian geometry assumes the consistency of Euclidean geometry, which in turn assumes the consistency of another axiomatizable system, and so forth). So this type of modeling has natural limits.
[9] The Fifth Postulate of Euclid states that given a line and a point, there is exactly one line that can be drawn through that point parallel to the existing line. Attempts to prove this postulate failed; in the 1800s, Riemann and Lobachevsky demonstrated the axiomatic nature of the postulate by developing geometries in which the postulate does not hold [774].
The Bell-LaPadula Model was developed as a model in the first sense. Bell pointed out that McLean's work presumed the second sense.
In the first sense of modeling, the Bell-LaPadula Model is a tool for demonstrating certain properties of rules. Whether the properties of System Z are desirable is an issue the model cannot answer. If no rules should change security compartments of entities, the system should enforce the principle of strong tranquility. System Z clearly violates this principle, and hence would be considered not secure. (The principle of tranquility adds requirements to state transitions, so given that principle, the Bell-LaPadula Model actually constrains both states and state transitions.)
In the second sense, Bell pointed out that the two models (the original Bell-LaPadula Model, and McLean's variant) define security differently. Hence, that System Z is not secure under one model, but secure under the other, is not surprising. As an example, consider the following definitions of prime number.
Definition 5–12. A prime number is an integer n > 1 that has only 1 and itself as divisors.
Definition 5–13. A prime number is an integer n > 0 that has only 1 and itself as divisors.
Both definitions, from a mathematical point of view, are acceptable and consistent with the laws of mathematics. So, is the integer 1 prime? By Definition 5–12, no; by Definition 5–13, yes. Neither answer is "right" or "wrong" in an absolute sense.[10]
[10] By convention, mathematicians use Definition 5–12. The integer 1 is neither prime nor composite.
McLean's questions and observations about the Bell-LaPadula Model raised issues about the foundations of computer security, and Bell and LaPadula's responses fueled interest in those issues. The annual Foundations of Computer Security Workshop began shortly after to examine foundational questions.
|
|
|
| Top |