- Greetings and felicitations!
- Please get your project proposals in as soon as possible, so you can get started

- Bell-LaPadula Model
- Go through security levels, categories, compartments
- Describe simple security property (no reads up) and *-property (no writes down)
- State Basic Security Theorem: if it's secure and transformations follow these rules, it's still secure
- Add in discretionary security policy

- BLP: formally
- Elements of system:
*s*subjects,_{i}*o*objects,_{i} - State space
*V*=*B*x*M*x*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:*f*is security level associated with each subject,_{s}*f*security level associated with each object, and_{o}*f*current security level for each subject_{c} - Set of requests is
*R* - Set of decisions is
*D* - W SUBSETEQ
*R*x*D*x*V*x*V*is motion from one state to another. - System [[Sigma]](
*R*,*D*,*W*,*z*_{0}) SUBSETEQ*X*x*Y*x*Z*such that (*x*,*y*,*z*) IN [[Sigma]](*R*,*D*,*W*,*z*_{0}) iff (*x*,_{t}*y*,_{t}*z*,_{t}*z*_{t-1}) IN*W*for each*i*IN*T*; latter is an action of system - Theorem: [[Sigma]](
*R*,*D*,*W*,*z*_{0}) satisfies the simple security property for any initial state*z*_{0}that satisfies the simple security property iff*W*satisfies the following conditions for each action (*R*,_{i}*D*, (_{i}*b*',*M*',*f*'), (*b*,*M*,*f*)):- each (
*s*,*o*,*x*) IN*b*' -*b*satisfies the simple security condition relative to*f*' (*i*.*e*.,*x*is not read, or*x*is read and*f*(_{s}*s*) dominates*f*(_{o}*o*) -
if (
*s*,*o*,*x*) IN*b*does not satisfy the simple security condition relative to*f*', then (*s*,*o*,*x*) NOTIN*b*' - Theorem: [[Sigma]](
*R*,*D*,*W*,*z*_{0}) satisfies the *-property relative to*S*' SUBSETEQ*S*, for any initial state*z*_{0}that satisfies the *-property relative to*S*' iff*W*satisfies the following conditions for each action (*R*,_{i}*D*, (_{i}*b*',*M*',*f*'), (*b*,*M*,*f*)):- for each
*s*IN*S*', any (*s*,*o*,*x*) IN*b*' -*b*satisfies the *-property with respect to*f*' - for each
*s*IN*S*', if (*s*,*o*,*x*) IN*b*does not satisfy the *-property with respect to*f*', then (*s*,*o*,*x*) NOTIN*b*'

- for each
- Theorem: [[Sigma]](
*R*,*D*,*W*,*z*_{0}) satisfies the ds-property iff the initial state*z*_{0}satisfies the ds-property and*W*satisfies the following conditions for each action (*R*,_{i}*D*, (_{i}*b*',*M*',*f*'), (*b*,*M*,*f*)):- if (
*s*,_{k}*o*,_{i}*x*) IN*b*' -*b*, then*x*IN*M*'[*k*,*i*]; - if (
*s*,_{k}*o*,_{i}*x*) IN*b*and*x*IN*M*'[*k*,*i*] then (*s*k,*o*i,*x*) IN*b*'

- if (
- Basic Security Theorem: A system [[Sigma]](
*R*,*D*,*W*,*z*_{0}) is secure iff*z*_{0}is a secure state and*W*satisfies the conditions of the above three theorems for each action.

- each (
- Biba
- Integrity levels and trust
- No reads down
- No writes up

You can get this document in ASCII text, Framemaker+SGML version 5.5, PDF (for Acrobat 3.0 or later), or Postscript.

Send email to cs253@csif.cs.ucdavis.edu. Department of Computer Science

University of California at Davis

Davis, CA 95616-8562

Page last modified on 3/19/99 - Elements of system: