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

___________
|A|B|C|D|E|
-----------
    ^
    |______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
    @------>O-------O------>O
    
    x    t    y    g    z    r    a
    @-------O<------O-------O    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<-------|
    |                                        |
    |________________________________________|