Verification: rmdir |
Require ModelProperties.
Require AuxiliaryLemmas.
Section rmdirIsSecure.
|
|
Lemma RmdirPSS:
(s,t:SFSstate; u:SUBJECT)
(SecureState s)->(TransFunc u s Rmdir t)->(SecureState t).
StartPSS .
Inversion H.
Unfold SecureState; BreakSS ; Split.
Unfold DACSecureState; Simpl; Intros.
Elim (OBJeq_dec o o0); Intros.
Rewrite <- a.
Replace (fsecmat (secmat s) o) with (None ReadersWriters).
Trivial.
Symmetry; Unfold fsecmat; Auto.
Unfold PreDACRead PreDACWrite; Simpl.
Replace (facl (rmdir_acl s o) o0) with (facl (acl s) o0).
Unfold DACSecureState PreDACRead PreDACWrite in DAC; Apply DAC.
Auto.
Unfold SimpleSecurity; Simpl.
Intros.
Elim (OBJeq_dec o o0).
Intro; Rewrite <- a.
Replace (fsecmat (secmat s) o) with (None ReadersWriters).
Elim (fOSC (rmdir_oSC s o) o); Elim (fSSC (subjectSC s) u0); Trivial.
Symmetry; Unfold fsecmat; Auto.
Intro EQ.
Replace (fOSC (rmdir_oSC s o) o0) with (fOSC (objectSC s) o0).
Unfold SimpleSecurity in MAC; Apply MAC.
Auto.
Qed.
|
|
Lemma RmdirPSP:
(s,t:SFSstate; u:SUBJECT)
(StarProperty s)->(TransFunc u s Rmdir t)->(StarProperty t).
StartPSP .
Inversion H.
Unfold StarProperty; Simpl; Intros.
Elim (OBJeq_dec o o1); Elim (OBJeq_dec o o2); Intros EQ2 EQ1.
Replace (fsecmat (secmat s) o1) with (None ReadersWriters).
Elim (fOSC (objectSC s) o2); Elim (fOSC (objectSC s) o1);
Elim (fOSC (rmdir_oSC s o) o2); Elim (fOSC (rmdir_oSC s o) o1);
Elim (fsecmat (secmat s) o2); Trivial.
Rewrite <- EQ1; Symmetry; Unfold fsecmat; Auto.
Replace (fsecmat (secmat s) o1) with (None ReadersWriters).
Elim (fsecmat (secmat s) o2); Elim (fOSC (objectSC s) o2);
Elim (fOSC (objectSC s) o1); Elim (fOSC (rmdir_oSC s o) o2);
Elim (fOSC (rmdir_oSC s o) o1); Trivial.
Rewrite <- EQ1; Symmetry; Unfold fsecmat; Auto.
Replace (fsecmat (secmat s) o2) with (None ReadersWriters).
Elim (fsecmat (secmat s) o1); Elim (fOSC (objectSC s) o2);
Elim (fOSC (objectSC s) o1); Elim (fOSC (rmdir_oSC s o) o2);
Elim (fOSC (rmdir_oSC s o) o1); Trivial.
Rewrite <- EQ2; Symmetry; Unfold fsecmat; Auto.
Replace (fOSC (rmdir_oSC s o) o2) with (fOSC (objectSC s) o2).
Replace (fOSC (rmdir_oSC s o) o1) with (fOSC (objectSC s) o1).
Unfold StarProperty in SP; Apply SP.
Auto.
Auto.
Qed.
|
|
Lemma RmdirPCP:
(s,t:SFSstate)
(FuncPre4 s)
->(FuncPre6 s)
->(PreservesControlProp s Rmdir t).
Intros s t FP4 FP6; Unfold PreservesControlProp; Intros Sub TF;
Inversion TF; Unfold ControlProperty.
Inversion H.
Split.
Intros.
Split.
Intro.
Inversion H8.
Elim (OBJeq_dec o o0); Simpl in H10; Intro y0.
Cut False.
Tauto.
Rewrite y0 in H10.
EAuto.
Cut y=z.
Intro; Rewrite H12 in H11; Cut False; [ Tauto | Inversion H11; Auto ].
Cut (facl (acl s) o0)=(facl (rmdir_acl s o) o0);
[ Rewrite H9; Rewrite H10; Intro; Injection H12; Auto | Auto ].
Elim (OBJeq_dec o o0); Simpl in H10; Intro y0.
Cut False.
Tauto.
Rewrite y0 in H10.
EAuto.
Cut y=z.
Intro; Rewrite H12 in H11; Cut False; [ Tauto | Inversion H11; Auto ].
Cut (facl (acl s) o0)=(facl (rmdir_acl s o) o0);
[ Rewrite H9; Rewrite H10; Intro; Injection H12; Auto | Auto ].
Intro.
Inversion H8.
Elim (OBJeq_dec o o0); Simpl in H10; Intros y0.
Cut False.
Tauto.
Rewrite y0 in H10.
EAuto.
Cut x=y.
Intro; Rewrite H12 in H11; Cut False; [ Tauto | Inversion H11; Auto ].
Cut (fOSC (objectSC s) o0)=(fOSC (rmdir_oSC s o) o0);
[ Rewrite H9; Rewrite H10; Intro; Injection H12; Auto | Auto ].
Intros;
Absurd (MACSubCtrlAttrHaveChanged s
(mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s)
(RootGrp s) (SecAdmGrp s) (rmdir_oSC s o) (rmdir_acl s o)
(secmat s) (files s) (rmdir_directories o)) u0); Auto.
Qed.
End rmdirIsSecure.
Hints Resolve RmdirPSS RmdirPSP RmdirPCP.