Preconditions for DAC and MAC


Section Preconditions.

Variable s: SFSstate.



This predicate asserts that for a subject to read an object, theformer must belong to the set of readers of the last. Also, thiscondition holds if the subject belongs to a group wich in turnbelongs to the object's readers.



Definition PreDACRead [u:SUBJECT; o:OBJECT]: Prop :=
  Cases (facl (acl s) o) of
   |(Some y) => (set_In u (UsersReaders y))
                 \/(EX g:GRPNAME | (set_In u ((groups s) g))
                                   /\(set_In g (GroupReaders y)))
   |None => False
  end.




This predicate asserts that for a subject to write to an object,the former must belong to the set of writers of the last. Also, this condition holds if the subject belongs to a group wich in turnbelongs to the object's writers.



Definition PreDACWrite [u:SUBJECT; o:OBJECT]: Prop :=
  Cases (facl (acl s) o) of
   |(Some y) => (set_In u (UsersWriters y))
                 \/(EX g:GRPNAME | (set_In u ((groups s) g))
                                   /\(set_In g (GroupWriters y)))
   |None => False
  end.




This predicate asserts that for a subject to read or write anobject, the object's security class must be dominated by the subject's security class.



Definition PreMAC [u:SUBJECT; o:OBJECT] : Prop :=
  Cases (fOSC (objectSC s) o) (fSSC (subjectSC s) u) of
   |None _ => False
   |_ None => False
   |(Some a)
    (Some b) => (le_sc a b)
  end.




This predicate asserts that if a user is an active writer of anyobject b, then the security class of b must dominates the securityclass of o. This predicate is used to preserve the *-property.



Definition PreStarPropRead [u:SUBJECT; o:OBJECT]: Prop :=
   (b:OBJECT)
       Cases (fsecmat (secmat s) b)
             (fOSC (objectSC s) o) (fOSC (objectSC s) b) of
        |None _ _ => False
        |_ None _ => False
        |_ _ None => False
        |(Some x)
         (Some y)
         (Some z) => (set_In u (ActWriters x)) -> (le_sc y z)
       end.


This predicate asserts that if a user is an active reader of anyobject b, then the security class of b must be dominated by thesecurity class of o. This predicate is used to preserve the -property.

Definition PreStarPropWrite [u:SUBJECT; o:OBJECT]: Prop :=
   (b:OBJECT)
       Cases (fsecmat (secmat s) b)
             (fOSC (objectSC s) o) (fOSC (objectSC s) b) of
        |None _ _ => False
        |_ None _ => False
        |_ _ None => False
        |(Some x)
         (Some y)
         (Some z) => (set_In u (ActReaders x)) -> (le_sc z y)
       end.




This predicate determines if a given user is one of the owners or belong to one of the owner groups of a given object.



Inductive IsUNIXOwner [u:SUBJECT] : AccessCtrlListData -> Prop :=

 |IUO: (a: AccessCtrlListData)
       (IsUNIXOwner u (acldata u (group a)
                               (UsersReaders a) (GroupReaders a)
                               (UsersWriters a) (GroupWriters a)
                               (UsersOwners a) (GroupOwners a))).


   
Inductive ExecuterIsOwner [u:SUBJECT; o:OBJECT] : Prop :=

 |UNIXOwner: (y:AccessCtrlListData)
               (facl (acl s) o)=(Some AccessCtrlListData y)
               ->(IsUNIXOwner u y)
               ->(ExecuterIsOwner u o)

 |ACLOwner : (y:AccessCtrlListData)
               (facl (acl s) o)=(Some AccessCtrlListData y)
               ->(set_In u (UsersOwners y))
               ->(ExecuterIsOwner u o)

 |ACLGrp : (y:AccessCtrlListData)
               (facl (acl s) o)=(Some AccessCtrlListData y)
               ->(EX g:GRPNAME | (set_In u (groups s g))
                                 /\(set_In g (GroupOwners y)))
               ->(ExecuterIsOwner u o).




InFileSystem is True if o is a file or a directory, False otherwise.

Definition InFileSystem [o:OBJECT] : Prop :=
 (set_In o (set_union OBJeq_dec
                      (DOM OBJeq_dec (files s))
                      (DOM OBJeq_dec (directories s)))).



End Preconditions.



Hints Resolve IUO UNIXOwner ACLOwner ACLGrp.



Hints Unfold PreDACRead PreDACWrite PreMAC
             PreStarPropRead PreStarPropWrite
             InFileSystem.