Bell LaPadula
Bell LaPadula
Bell LaPadula
C. Edward Chow
CS691 Chapter 5 of Matt Bishop
cs691
chow
cs691
chow
cs691
chow
cs691
chow
cs691
chow
cs691
chow
Q
S
read(D)
T
If the mandatory controls not present, S would be able to read
(write) O.
cs691
chow
Bell-LaPadula Model
cs691
chow
Informal Description
cs691
chow
cs691
10
chow
cs691
11
chow
cs691
12
chow
Security Lattice
{NUC, EUR,
US}
{NUC, EUR}
{NUC}
{NUC, US}
{EUR}
{EUR, US}
{US}
cs691
13
chow
cs691
14
chow
cs691
15
chow
cs691
16
chow
cs691
17
chow
18
chow
cs691
19
chow
Multilevel Directory
cs691
20
chow
1.
2.
3.
4.
5.
cs691
21
chow
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/alb.
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 Mode
numbers, computing the label of symbolic links is straightforward. If /x/y/z is a sym
bolic 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.
cs691
22
chow
cs691
23
chow
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, a for write, w for read/write, and e for
empty.
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
(fs,fo,fc), where fs and, fc associate with each subject maximum and
current security levels, respectively, and, fo, associates with each object a
security level.
The system objects may be organized as a set of hierarchies (trees and
single nodes).
Let H represent the set of hierarchy functions h: OP(O).
P(O) is the power set of O, i.e., the set of all possible subsets of O.
The hierarchy functions have two properties: Let oi, oj, ok O.
1. If oi oj, then h(oi) h(oj) = .
2. There is no set { o1, o2, ..., ok } O such that
for each i = 1, ..., k, oi+1 h(oi), and ok+1= o1.
cs691
24
chow
cs691
25
chow
cs691
26
chow
Define b(s: p1, ..., pn) to be the set of all objects that s has p1, ..., pn
access to.
b(s: p1, ..., pn)={ o | oO [(s,o,p1)b ...(s,o,pn)b]}
cs691
27
chow
cs691
28
chow
Theorem 5-3. (R, D, W, z0) satisfies the simple security condition 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:
a. Every (s, o, p) b - b' satisfies ssc rel f.
b. Every (s, o, p) b' that does not satisfy ssc rel f is not in b.
Theorem 5-4. (R, D, W, z0) satisfies the *-property relative to S' 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 for every s S':
a. Every (s, o, p) b - b' satisfies the *-property with respect to S'.
b. Every (s, o, p) b' that does not satisfy the *-property with respect to S' is
not in b.
Theorem 5-5. (R, D, W, z0) satisfies the ds-property 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:
a. Every (s, o, p) b - b ' satisfies the ds-property.
b. Every (s, o, p) b' that does not satisfy the ds-property is not in b.
Theorem 5-6. Basic Security Theorem: (R, D. W, z0) is a secure system if
z0 is a secure state and W satisfies the conditions of Theorems 5-3, 5-4,
and 5-5.
cs691
29
chow
Rules of Transformation
cs691
30
chow
cs691
31
chow
Properties
Theorem 5-10. Let v= (b, m, f, h) satisfy the *-property. Let (s, o, p) b, b' = b { (s,
o, p) }, and v' = (b', m, f, h). Then v' satisfies the *-property if and only if one of the
following conditions holds.
a. p = a and fo(o) dom fc(s)
b. p = w and. fo(o) = fc(s)
c. p = r and fc(s) dom fo(o)
Theorem 5-11. Let be a set of ds-property-preserving rules, and let z0 be a state
satisfying the ds-property. Then (R, D, W, z0) satisfies the ds-property.
Theorem 5-12. Let v = (b, m,,f; h) satisfy the ds-property. Let (s, o, p) b, b' = b
{ (s, o. p) }, and v' = (b', m, f, h).
Then v' satisfies the ds-property if and only if p m[s, o].
Theorem 5-13. Let he a rule and (r, v) = (d, v'), where v= (b, m, f, h) and v' = (b',
m', f', h'). Then:
a. If b' b, f'=,f, and v satisfies the simple security condition, then v satisfies
the simple security condition.
b. If b' h, f' =f, and v satisfies the *-property, then v' satisfies the *-property.
c. If b' h, , m[s, o] m' [s, o] for all s S and o O, and v satisfies the dsproperty, then v' satisfies the ds-property.
cs691
32
chow
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 ST are trusted not to violate that
property.
For each rule , define () as the domain of the request (that is, whether or not the components
of the request form a valid operand for the rule).
cs691
33
chow
cs691
34
chow
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 = (s1, give, s2, o, r) R(2), and let the current state of the
system be v = (b, m, f, h). Then, give-read is the rule 6(r, v):
if (r (6)) then 6(r, v) = (i, v);
else if ( [ o root(o) and parent(o) root(o) and parent(o) b(s1: w)] or
[ parent(o) = root(o) and canallow(s1, o, v) ] or
[ o = root(o) and canallow(s1, root(o), v) ])
then 6(r, v) = (y, (b, m m[s2, o]r, f, h));
else 6(r, v) = (n, v);
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 1 must have write
rights to the parent. If the object or its parent is the root of the hierarchy, then s 1 must have
special permission to give s 2 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.
cs691
35
chow
Tranquility
The principle of tranquility states that subjects and objects may not change their
security levels once they have been instantiated.
Suppose that security levels of objects can be changed, and consider the effects on
a system with one category and two security clearances, HIGH and LOW. If an
object's security classification is raised from LOW to HIGH, then any subjects
cleared to only LOW can no longer read that object. Similarly, if an object's
classification is dropped from HIGH to LOW, any subject can now read that object.
Both situations violate fundamental restrictions.
Raising the classification of an object means that information that was available is no
longer available; lowering the classification means that information previously
considered restricted is now available to all.
Raising the classification of an object is not considered a problem. The model does
not define how to determine the appropriate classification of information. It merely
describes how to manipulate an object containing the information once that object
has been assigned a classification.
declassification problem. Because this makes information available to subjects who
did not have access to it before, it is in effect a "write down" that violates the
*-property. The typical solution is to define a set of trusted entities or subjects that will
remove all sensitive information from the HIGH object before its classification is
changed to LOW.
cs691
36
chow
Strong/Weak Tranquility
Definition 5-9. The principle of strong tranquility states that security levels do not
change during the lifetime of the system.
Strong tranquility eliminates the need for trusted declassifiers, because no
declassification can occur. Moreover, no raising of security levels can occur. This
eliminates the problems discussed above. However, strong tranquility is also
inflexible and in practice is usually too strong a requirement.
Definition 5-10. The principle of weak tranquility states that security levels do not
change in a way that violates the rules of a given security policy.
Weak tranquility moderates the restriction to allow harmless changes of security
levels. It is more flexible, because it allows changes, but it disallows any violations of
the security policy (in the context of the Bell-LaPadula Model, the simple security
condition and *-property).
EXAMPLE: In the Data General DG/UX system, only the security administrator, a
trusted user, can change MAC labels on objects. In general, when a user wishes to
assume a new MAC label, that user must initiate a new session; the MAC labels of
processes cannot be changed. However, a user may be designated as able to
change a process label within a specified range. This makes the system more
amenable to commercial environments.
cs691
37
chow
1985 McLean define a property which is not secure (allow write down) and show that the basic
theorem is not correct.
Definition 5-11. A state (b, m, f, h) satisfies the -property if and only if, for each subject s c S,
the following conditions hold:
a. b(s: a) [ ob(s: a) [fc(s) dom fo(o) ] ]
b. b(s: w) [ ob(s: w) [fc(s) = fo(o) ] ]
c. b(s: r) [ ob(s: r) [fc(s) dom fo(o) ] ]
McLean then proved the analogue to Theorem 5-4:
Theorem 5-16. (R, D, W, z0) satisfies the -property relative to S' 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 S
a. Every (s, o, p) b - b' satisfies the -property with respect to S
b. Every (s, o, p) b' that does not satisfy the -property with respect to S' is not in b.
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: (R, D, W, z0) is a secure system if and only if zt is a
secure state and W satisfies the conditions of Theorems 5-3, 5-16, and 5-5.
But the system (R, D, W, z0) is clearly not secure.
Bell-LaPadula argue that their model assumes the transition introduces no changes that violate
security.
cs691
38
chow
McCleans System Z
cs691
39
chow
cs691
40
chow
cs691
41
chow
SELinux
Support
Separation policies:
Enforce legal restriction on data
Establish well-defined user roles
Restrict access to classified data
Containment policies for
Restrict web server access to only authorized data
Minimize damage caused by virues/malicious code
Integrity policies that protect unauthorized modifications to data
and applications
Invocation policies that guarantee data is processed as required.
cs691
42
chow