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