Outline for April 8, 2004

1. 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?
   3. Mono-operational protection systems: decidable
   4. Theorem: there is an algorithm that decides whether a given mono-operational system and initial state is safe for a given generic right.
2. General case: It is undecidable whether a given state of a given protection system is safe for a given generic right.
   1. Represent TM as ACM; reduce halting problem to it
3. Take-Grant
   1. Introduce as counterpoint to HRU result
   2. Show symmetry
   3. Show islands (maximal subject-only tg-connected subgraphs)
   4. Show bridges (as a combination of terminal and initial spans)
4. Predicates
   1. can·share(r, x, y, G₀) iff there is an edge from x to y labelled r in G₀, or all of the following hold:
      1. there is a vertex y′ with an edge from y′ to y labelled r;
      2. there is a subject y′′ which terminally spans to y′, or y′′ = y′;
      3. there is a subject x′ which initially spans to x, or x′ = x; and
      4. there is a sequence of islands I₁, ..., I_n connected by bridges for which x′ is in I₁ and y′ is in I_n.
   2. Go through interpretation
5. Schematic Protection Model
   1. Model components
   2. Link function
   3. Filter function
   4. Example: Take-Grant as an instance of SPM
   5. Create operations and attenuation
6. Expressive power
   1. HRU vs. SPM
   2. Multiparent joint creates in HRU
   3. Adding multiparent joint creates to SPM (giving ESPM)