Outline for April 5, 2006
Reading: text, §3.1—3.3.2
- Greetings and felicitations!
- 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 decidable?
- Theorem: there is an algorithm that decides whether a given
mono-operational system and initial state is safe for a given
- 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
- Counterpoint to HRU result
- Symmetry of take and grant rights
- Islands (maximal subject-only tg-connected subgraphs)
- Bridges (as a combination of terminal and initial spans)
- Definition: can•share(r,
x, y, G0) true
iff there exists a sequence of protection graphs
G0, ..., Gn
such that G0 ⊢*
using only take, grant, create, remove rules and in
Gn, there is an edge from
x to y labeled r
- Theorem: 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 labeled 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;
- there is a sequence of islands I1,
..., In connected by bridges
for which x′ is in I1
and y′ is in In.
- Model Interpretation
- ACM very general, broadly applicable; Take-Grant more specific,
can model fewer situations
- Theorem: G0 protection graph with exactly
one subject, no edges; R set of rights. Then
G0 ⊢* G
iff G is a finite directed graph
containing subjects and objects only, with edges labeled
from nonempty subsets of R, and with at least
one subject with no incoming edges
- Example: shared buffer managed by trusted third party
Version of April 3, 2006 at 4:40 PM
You can also obtain a PDF version of this.