Outline for January 26, 1999

1.	Greetings and felicitations!

a.	Please get your project proposals in as soon as possible, so you can get started

2.	Bell-LaPadula Model

a.	Go through security levels, categories, compartments

b.	Describe simple security property (no reads up) and *-property (no writes down)

c.	State Basic Security Theorem: if it's secure and transformations follow these rules, it's still secure

d.	Add in discretionary security policy

3.	BLP: formally

a.	Elements of system: si subjects, oi objects, 

b.	State space V = BÄMÄF where:
B set of current accesses (i.e., access modes each subject has currently to each object);
M access permission matrix;
F consists of 3 functions: fs is security level associated with each subject, fo security level associated with 
each object, and fc current security level for each subject

c.	Set of requests is R

d.	Set of decisions is D

e.	W ¼ RÄDÄVÄV is motion from one state to another.

f.	System S(R, D, W, z0) ¼ XÄYÄZ such that (x, y, z) ? S(R, D, W, z0) iff (xt, yt, zt, zt-1) ? W for each i ? T; lat-
ter is an action of system

g.	Theorem: S(R, D, W, z0) satisfies the simple security property for any initial state z0 that satisfies the simple 
security property iff W satisfies the following conditions for each action (Ri, Di, (b', M', f'), (b, M, f)):
(i)		each (s, o, x) ? b' - b satisfies the simple security condition relative to f' (ie, x is not read, or x is read 
and fs(s) dominates fo(o)
(ii)		if (s, o, x) ? b does not satisfy the simple security condition relative to f', then (s, o, x) ? b'

h.	Theorem: S(R, D, W, z0) satisfies the *-property relative to S' ¼ S, for any initial state z0 that satisfies the *-
property relative to S' iff W satisfies the following conditions for each action (Ri, Di, (b', M', f'), (b, M, f)):
(i)		for each s ? S', any (s, o, x) ? b' - b satisfies the *-property with respect to f'
(ii)		for each s ? S', if (s, o, x) ? b does not satisfy the *-property with respect to f', then (s, o, x) ? b'

i.	Theorem: S(R, D, W, z0) satisfies the ds-property iff the initial state z0 satisfies the ds-property and W satis-
fies the following conditions for each action (Ri, Di, (b', M', f'), (b, M, f)):
(i)		if (sk, oi, x) ? b' - b, then x ? M'[k, i];
(ii)		if (sk, oi, x) ? b and x ? M'[k, i] then (sk, oi, x) ? b'

j.	Basic Security Theorem: A system S(R, D, W, z0) is secure iff z0 is a secure state and W satisfies the condi-
tions of the above three theorems for each action.

4.	Biba

a.	Integrity levels and trust

b.	No reads down

c.	No writes up