Outline for April 6, 2000

1. Greetings and felicitations!
   1. Handouts
2. ACM and primitive operations
   1. Go over subjects, objects (includes subjects), and state (S, O, A) where A is ACM
   2. Transitions modify ACM entries; primitive operations follow
   3. enter r into A[s,o]
   4. delete r from A[s,o]
   5. create subject s' (note A[s',x] = A[x,s'] = ø for all x)
   6. create object o' (note A[x,o'] = ø for all x)
   7. destroy subject s'
   8. destroy object o'
3. commands

   1. command c(s1, ..., sk,
      o1, ..., ok)
      if r1 in A[s1, o1] and
         r2 in A[s2, o2] and
         ...
         rm in A[sm, om]
      then
         op1;
         op2;
         ...;
         opn;
      end.
      

   2. Example 1: creating a file

      command create_file(p, f)
         create object f;
         enter Own into A[p, f]
         enter Read into A[p, f]
         enter Write into A[p, f]
      end.
      

   3. Example 2: granting one process read rights to a file

      command grant_read(p, q, f)
      if Own in A[p, f] 
      then
         enter Read into A[q, f]
      end.
      

4. What is the safety question?
   1. An unauthorized state is one in which a generic right r could be leaked into an entry in the ACM that did not previously contain r. An initial state is safe for r if it cannot lead to a state in which r could be leaked.
   2. Question: in a given arbitrary protection system, is safety decidable?
5. Mono-operational protection systems: decidable
   1. Theorem: there is an algorithm that decides whether a given mono-operational system and initial state is safe for a given generic right.
   2. Proof: finite number of command sequences; can eliminate delete, destroy.
      Ignore more than one create as all others are conditioned on access rights in the matrix. (One exception: no subjects; then we need one create subject).
      Bound: s number of subjects (possibly one more than in original), o number of objects (same), g number of generic rights; number of command sequences to inspect is at most 2^gso.