|
|
Require Export DACandMAC.
Require Export setACLdata.
Section Chmod.
Variable s:SFSstate.
Some preliminary definitions |
Local ChangeGAR
[o:OBJECT; oct:RIGHTS] : (Exc (set GRPNAME)) :=
Cases (facl (acl s) o) of
|None => (None (set GRPNAME))
|(Some y) =>
(Some (set GRPNAME)
(ChangeGroupR (AllGrp s)
oct
(ChangeGroupR (group y)
oct
(GroupReaders y))))
end.
Local ChangeGAW
[o:OBJECT; oct:RIGHTS] : (Exc (set GRPNAME)) :=
Cases (facl (acl s) o) of
|None => (None (set GRPNAME))
|(Some y) =>
(Some (set GRPNAME)
(ChangeGroupW (AllGrp s)
oct
(ChangeGroupW (group y)
oct
(GroupWriters y))))
end.
Local NEW [u:SUBJECT; o:OBJECT; perms:PERMS]:(Exc AccessCtrlListData):=
Cases (facl (acl s) o)
(ChangeGAR o (groupp perms))
(ChangeGAW o (groupp perms)) of
|None _ _ => (None AccessCtrlListData)
|_ None _ => (None AccessCtrlListData)
|_ _ None => (None AccessCtrlListData)
|(Some y)
(Some gar)
(Some gaw) =>
(Some AccessCtrlListData
(acldata (owner y)
(group y)
(ChangeUserR u (UsersReaders y) (ownerp perms))
gar
(ChangeUserW u (UsersWriters y) (ownerp perms))
gaw
(UsersOwners y)
(GroupOwners y)))
end.
Definition chmod_acl
[u:SUBJECT; o:OBJECT; perms:PERMS] : (set OBJECT*AccessCtrlListData):=
Cases (facl (acl s) o)
(NEW u o perms) of
|None _ => (acl s)
|_ None => (acl s)
|(Some y)
(Some z) => (set_add ACLeq_dec
(o,z)
(set_remove ACLeq_dec (o,y) (acl s)))
end.
Next state definition |
Local t [u:SUBJECT; o:OBJECT; perms:PERMS] : SFSstate :=
(mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s)
(RootGrp s) (SecAdmGrp s) (objectSC s)
(chmod_acl u o perms) (secmat s) (files s) (directories s)).
Operation definition |
Inductive chmod
[u:SUBJECT; o:OBJECT; perms:PERMS] : SFSstate -> Prop :=
|ChmodOK:
(ExecuterIsOwner s u o)
->~(set_In o (domsecmat (secmat s)))
->(chmod u o perms (t u o perms)).
|
|
Hints Resolve ChangeGAR ChangeGAW chmod_acl t.
End Chmod.