Lecture 17 Notes; May 7, 1997; Notetaker: Michael Clifford
ECS 253 Class notes for Wednesday, May 7'th 1997
Proof of HRU result:
Given:
Turing machine T with a tape that is infinite in one direction
finite set of states k
tape symbols 
Moves: rho : K x  > k x  x {L,R}
rho(q,x) = (p,Y,R)
start state: Qo
halting state: Qf
We can use an Access Control Matrix (ACM) to encode the state of the machine:
moves are AC commands
 represents access rights
tape cell = subject
S1 S2 S3 q = head position.
S1 A own End = end of squares that have been
S2 B own examined.
S3 Cq own
S4 D E,End,q
___________
ABCDE

^
______HEAD
Rules:
1) cell s contains X
> X is an element of A[s,s]
2) ordered
> own is an element of A[S,s+1]
3) Mark end of tape
> End is an element of A[Sk,Sk]
4) Tape head at cells
> q is an element of A[S,S]
rho(q,x) = (p,y,L)
command (q,x(s,s')
If: q is an element of A[s',s'], own is an element of A[s,s'], x is an element
of A[s',s']
Then: delete q from s'
enter q into s
delete x from s'
enter y into s
end
___________________
The Take  Grant model:
entities are either subjects or objects
subject: @
object: O
Subject or object: %
(note: the actual symbols used for this are a filled circle, an open circle,
and a circle with an X in it.)
x t is an element of alpha y z
take (t) @>%>%
^
B = some set of rights
x can take any right from y
y takes (r to z) from y
z r x g y
grant(g) %<@>%
^
r
create @>%
x alpha y
delete @>%
x alpha  beta y
example)
Graph number Graph
G0 O<@>@
a x t y
G1 O<@>@>@ y creates (tg to z)
a x t y tg z
G2 O<@>@>@ z
a x\ t y tg ^
\ 
\_______________
g
z
G3 a O<@>@>@
^ x\ y tg ^  x grants (alpha t = a)
 \   to z
 \_______________ 
 g 
 
__________________________________

v 
G4 a O<@>@>@
^ x\ t y tg ^  y takes (alpha to a)
 \   from z
 \_______________ 
 g 
 
_________________________________
Thus, assignment of access rights on grant and take edges is two way.
Definition: canshare (alpha,x,y,G0) is true iff x can acquire alpha's rights
over y beginning in G0
canshare(alpha,x,y,G0)
x t z t y alpha a
@>@<@O
^  \
______________________________ 
g  v
>@ c

 t
v
@ k
Dynamically linked libraries are both files and code, so they are considered
to be both subjects and objects
Access rights: no paths can be added where they do not already exist:
Outgoing edges are never added to a vertex with only incoming edges
Incoming edges are never added to a vertex with only outgoing edges
x t y t z r a
@>OO>O
x t y g z r a
@O<OO rights can't be taken on this graph
_>
Define initial path t
The initial path is a sequence of takes
terminal paths:
y g x3 t x2 t alpha a alpha
O<O<O<>O<
 
________________________________________