|
|
Require Export DACandMAC.
Section Chown.
Variable s: SFSstate.
Some preliminary definitions |
Local NEW_GRP [old,new:GRPNAME; gs:(set GRPNAME)] : (set GRPNAME) :=
Cases (set_In_dec GRPeq_dec old gs) of
|(left _) => (set_add GRPeq_dec new (set_remove GRPeq_dec old gs))
|(right _) => gs
end.
Local NEW_UO [old,new:SUBJECT; us:(set SUBJECT)] : (set SUBJECT) :=
(set_add SUBeq_dec new (set_remove SUBeq_dec old us)).
Local NEW [o:OBJECT; p:SUBJECT; g:GRPNAME] : (Exc AccessCtrlListData):=
Cases (facl (acl s) o) of
|None => (None AccessCtrlListData)
|(Some y) => (Some AccessCtrlListData
(acldata p g
(UsersReaders y)
(NEW_GRP (group y) g (GroupReaders y))
(UsersWriters y)
(NEW_GRP (group y) g (GroupWriters y))
(NEW_UO (owner y) p (UsersOwners y))
(GroupOwners y)))
end.
Definition chown_acl
[o:OBJECT; p:SUBJECT; g:GRPNAME]: (set OBJECT*AccessCtrlListData) :=
Cases (facl (acl s) o)
(NEW o p g) 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 [o:OBJECT; p:SUBJECT; g:GRPNAME] : SFSstate :=
(mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s)
(RootGrp s) (SecAdmGrp s) (objectSC s) (chown_acl o p g)
(secmat s) (files s) (directories s)).
Operation definition |
Inductive chown
[u:SUBJECT; o:OBJECT; p:SUBJECT; g:GRPNAME] : SFSstate -> Prop :=
|ChownOK:
(ExecuterIsOwner s u o)
->~(set_In o (domsecmat (secmat s)))
->(chown u o p g (t o p g)).
|
|
Hints Unfold chown_acl t.
End Chown.