* Reading*:

- 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 generic right.

- An unauthorized state is one in which a generic right
- 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

- Take-Grant
- 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)

- Sharing
- Definition:
*can•share*(*r*,**x**,**y**,*G*_{0}) true iff there exists a sequence of protection graphs*G*_{0}, ...,*G*_{n}such that*G*_{0}⊢^{*}*G*_{n}using only take, grant, create, remove rules and in*G*_{n}, there is an edge from**x**to**y**labeled*r* - Theorem:
*can•share*(*r*,**x**,**y**,*G*_{0}) iff there is an edge from**x**to**y**labelled*r*in*G*_{0}, 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**; and - there is a sequence of islands
*I*_{1}, ...,*I*_{n}connected by bridges for which**x′**is in*I*_{1}and**y′**is in*I*_{n}.

- there is a vertex

- Definition:
- Model Interpretation
- ACM very general, broadly applicable; Take-Grant more specific, can model fewer situations
- Theorem:
*G*_{0}protection graph with exactly one subject, no edges;*R*set of rights. Then*G*_{0}⊢^{*}*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.