Verification: chmod |
Require ModelProperties.
Require AuxiliaryLemmas.
Section chmodIsSecure.
|
|
Lemma ChmodPSS:
(s,t:SFSstate; u:SUBJECT)
(SecureState s)->(TransFunc u s Chmod t)->(SecureState t).
StartPSS .
Inversion H.
Unfold SecureState.
BreakSS .
Split.
Unfold DACSecureState.
Simpl.
Intros.
Elim (OBJeq_dec o o0).
Intro.
Rewrite <- a.
Cut (fsecmat (secmat s) o)=(None ReadersWriters).
Intro.
Rewrite H6.
EAuto.
Unfold fsecmat.
Auto.
Intro.
Cut (Cases (fsecmat (secmat s) o0) of
(Some y) =>
((set_In u0 (ActReaders y))->(PreDACRead s u0 o0))
| None => True
end)
/\
(Cases (fsecmat (secmat s) o0) of
(Some y) =>
((set_In u0 (ActWriters y))->(PreDACWrite s u0 o0))
| None => True
end).
Elim (fsecmat (secmat s) o0).
Unfold PreDACRead PreDACWrite chmod_acl.
Simpl.
Elim (facl (acl s) o).
Intro.
Replace (facl
(set_add ACLeq_dec
(o,
(acldata (owner a) (group a)
(ChangeUserR Sub (UsersReaders a) (ownerp perms))
(ChangeGroupR (AllGrp s) (groupp perms)
(ChangeGroupR (group a) (groupp perms)
(GroupReaders a)))
(ChangeUserW Sub (UsersWriters a) (ownerp perms))
(ChangeGroupW (AllGrp s) (groupp perms)
(ChangeGroupW (group a) (groupp perms)
(GroupWriters a))) (UsersOwners a)
(GroupOwners a)))
(set_remove ACLeq_dec (o,a) (acl s))) o0)
with (facl (acl s) o0).
Elim (facl (acl s) o0).
Auto.
Auto.
Unfold facl.
Auto.
Auto.
Tauto.
Split.
Apply ReadWriteImpRead.
Auto.
Apply ReadWriteImpWrite.
Auto.
Auto.
Qed.
|
|
Lemma ChmodPSP:
(s,t:SFSstate; u:SUBJECT)
(StarProperty s)->(TransFunc u s Chmod t)->(StarProperty t).
StartPSP.
Inversion H; Auto.
Qed.
|
|
Lemma ChmodPCP:
(s,t:SFSstate)(PreservesControlProp s Chmod t).
Intros; Unfold PreservesControlProp; Intros Sub TF; Inversion TF;
Unfold ControlProperty.
Inversion H.
Split.
Intros.
Split.
Intro.
Inversion H6.
Simpl in H8.
Elim (OBJeq_dec o o0); Intro.
Rewrite <- a; Auto.
Cut y=z.
Intro.
Cut False.
Tauto.
Rewrite H10 in H9; Inversion H9; Auto.
Cut (facl (chmod_acl s Sub o perms) o0)=(facl (acl s) o0).
Intro H11; Rewrite H11 in H8; Rewrite H7 in H8; Injection H8; Auto.
Symmetry.
Unfold chmod_acl.
Elim (facl (acl s) o).
Intro; Unfold facl; Apply AddRemEq.
Auto.
Auto.
Simpl in H8.
Elim (OBJeq_dec o o0); Intro.
Rewrite <- a; Auto.
Cut y=z.
Intro.
Cut False.
Tauto.
Rewrite H10 in H9; Inversion H9; Auto.
Cut (facl (chmod_acl s Sub o perms) o0)=(facl (acl s) o0).
Intro H11; Rewrite H11 in H8; Rewrite H7 in H8; Injection H8; Auto.
Symmetry.
Unfold chmod_acl.
Elim (facl (acl s) o).
Intro; Unfold facl; Apply AddRemEq.
Auto.
Auto.
Intro;
Absurd (MACObjCtrlAttrHaveChanged s
(mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s)
(RootGrp s) (SecAdmGrp s) (objectSC s) (chmod_acl s Sub o perms)
(secmat s) (files s) (directories s)) o0);
Auto.
Intros;
Absurd (MACSubCtrlAttrHaveChanged s
(mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s)
(RootGrp s) (SecAdmGrp s) (objectSC s) (chmod_acl s Sub o perms)
(secmat s) (files s) (directories s)) u0);
Auto.
Qed.
End chmodIsSecure.
Hints Resolve ChmodPSS ChmodPSP ChmodPCP.