Verification: mkdir |
Require ModelProperties.
Require AuxiliaryLemmas.
Section mkdirIsSecure.
|
|
Lemma MkdirPSS:
(s,t:SFSstate; u:SUBJECT)
(FuncPre1 s)
->(FuncPre2 s)
->(FuncPre3 s)
->(SecureState s)->(TransFunc u s Mkdir t)->(SecureState t).
Intros s t Sub FP1 FP2 FP3 SS TF; Inversion TF.
Inversion H.
BreakSS .
Unfold SecureState.
Split.
Unfold DACSecureState; Simpl.
Intros.
Cut (Cases (fsecmat (secmat s) o) of
(Some y) => (set_In u0 (ActReaders y))->(PreDACRead s u0 o)
| None => True
end)
/\(Cases (fsecmat (secmat s) o) of
(Some y) => (set_In u0 (ActWriters y))->(PreDACWrite s u0 o)
| None => True
end).
Elim (fsecmat (secmat s) o).
Unfold PreDACRead PreDACWrite mkdir_acl; Simpl.
Elim (fsecmat (secmat s) (MyDir p)); Elim (fSSC (subjectSC s) Sub).
Elim (OBJNAMEeq_dec p (ObjName o)).
Intro y.
Rewrite y.
Replace (facl (acl s) o) with (None AccessCtrlListData).
Intros.
Elim H8; Intros.
Split; Intro.
Tauto.
Tauto.
Rewrite y in H2.
Rewrite y in H4.
Symmetry.
Unfold facl.
Apply NotInDOMIsUndef.
Auto.
Intro y.
Replace (facl
(set_add ACLeq_dec
((NEWDIR p),
(acldata Sub (primaryGrp s Sub)
(ChangeUserR Sub (empty_set SUBJECT)
(ownerp perms))
(ChangeGroupR (AllGrp s) (groupp perms)
(ChangeGroupR (primaryGrp s Sub) (groupp perms)
(empty_set GRPNAME)))
(ChangeUserW Sub (empty_set SUBJECT)
(ownerp perms))
(ChangeGroupW (AllGrp s) (groupp perms)
(ChangeGroupW (primaryGrp s Sub) (groupp perms)
(empty_set GRPNAME)))
(cons Sub (nil SUBJECT))
(cons (RootGrp s) (nil GRPNAME)))) (acl s)) o)
with (facl (acl s) o).
Auto.
Unfold facl; Apply AddEq.
Unfold NEWDIR.
Intro.
Apply y.
Rewrite H8.
Simpl.
Auto.
Auto.
Auto.
Auto.
Tauto.
Unfold DACSecureState in DAC.
Split.
Apply ReadWriteImpRead; Auto.
Apply ReadWriteImpWrite; Auto.
Unfold SimpleSecurity; Simpl; Intros.
Elim (OBJNAMEeq_dec p (ObjName o)).
Intro y.
Rewrite y.
Replace (fsecmat (secmat s) o) with (None ReadersWriters).
Replace (fOSC (objectSC s) o) with (None SecClass).
Elim (fSSC (subjectSC s) u0);
Elim (fOSC (mkdir_oSC s Sub (ObjName o)) o);
Contradiction Orelse Auto.
Symmetry.
Unfold fOSC; Apply NotInDOMIsUndef.
Replace (DOM OBJeq_dec (objectSC s)) with (DOM OBJeq_dec (acl s)).
Rewrite y in H2; Rewrite y in H4; Auto.
Symmetry; Unfold fsecmat; Apply NotInDOMIsUndef.
Cut ~(set_In o (DOM OBJeq_dec (acl s))).
Unfold not.
Intros SI1 SI2; Apply SI1.
Unfold FuncPre3 in FP3.
Unfold Included in FP3.
Auto.
Rewrite y in H2; Rewrite y in H4; Auto.
Intro y.
Replace (fOSC (mkdir_oSC s Sub p) o) with (fOSC (objectSC s) o).
Unfold SimpleSecurity in MAC; Apply MAC.
Auto.
Qed.
|
|
Lemma MkdirPSP:
(s,t:SFSstate; u:SUBJECT)
(FuncPre1 s)
->(FuncPre2 s)
->(FuncPre3 s)
->(StarProperty s)->(TransFunc u s Mkdir t)->(StarProperty t).
Intros s t Sub FP1 FP2 FP3 SP TF; Inversion TF.
Inversion H.
Unfold StarProperty; Simpl; Intros u0 o1 o2.
Elim (OBJNAMEeq_dec p (ObjName o1));
Elim (OBJNAMEeq_dec p (ObjName o2)).
Intros y y0.
Replace (fsecmat (secmat s) o1) with (None ReadersWriters).
Elim (fsecmat (secmat s) o2); Elim (fOSC (mkdir_oSC s Sub p) o2);
Elim (fOSC (mkdir_oSC s Sub p) o1); Trivial.
EAuto.
Intros y y0.
Replace (fsecmat (secmat s) o1) with (None ReadersWriters).
Elim (fsecmat (secmat s) o2); Elim (fOSC (mkdir_oSC s Sub p) o2);
Elim (fOSC (mkdir_oSC s Sub p) o1); Trivial.
EAuto.
Intros y y0.
Replace (fsecmat (secmat s) o2) with (None ReadersWriters).
Elim (fsecmat (secmat s) o1); Elim (fOSC (mkdir_oSC s Sub p) o2);
Elim (fOSC (mkdir_oSC s Sub p) o1); Trivial.
EAuto.
Intros y y0.
Replace (fOSC (mkdir_oSC s Sub p) o1) with (fOSC (objectSC s) o1).
Replace (fOSC (mkdir_oSC s Sub p) o2) with (fOSC (objectSC s) o2).
Unfold StarProperty in SP; Apply SP.
Auto.
Auto.
Qed.
|
|
Lemma MkdirPCP:
(s,t:SFSstate)
(FuncPre1 s)
->(FuncPre2 s)
->(PreservesControlProp s Mkdir t).
Intros s t FP1 FP2; Unfold PreservesControlProp; Intros Sub TF;
Inversion TF; Unfold ControlProperty.
Inversion H.
Split.
Intros.
Split.
Intro.
Inversion H8.
Simpl in H10.
Elim (OBJNAMEeq_dec p (ObjName o)).
Intro.
Cut (facl (acl s) o)=(None AccessCtrlListData).
Intro.
Rewrite H12 in H9.
Discriminate H9.
Unfold facl; Apply NotInDOMIsUndef.
Rewrite a in H2; Rewrite a in H4; Auto.
Intro.
Cut y=z.
Intro.
Cut False.
Tauto.
Rewrite H12 in H11; Inversion H11; Auto.
Cut (facl (acl s) o)=(facl (mkdir_acl s Sub p perms) o).
Intro EQ; Rewrite <- EQ in H10; Rewrite H10 in H9; Injection H9; Auto.
Auto.
Simpl in H10.
Elim (OBJNAMEeq_dec p (ObjName o)).
Intro.
Cut (facl (acl s) o)=(None AccessCtrlListData).
Intro.
Rewrite H12 in H9.
Discriminate H9.
Unfold facl; Apply NotInDOMIsUndef.
Rewrite a in H2; Rewrite a in H4; Auto.
Intro.
Cut y=z.
Intro.
Cut False.
Tauto.
Rewrite H12 in H11; Inversion H11; Auto.
Cut (facl (acl s) o)=(facl (mkdir_acl s Sub p perms) o).
Intro EQ; Rewrite <- EQ in H10; Rewrite H10 in H9; Injection H9; Auto.
Auto.
Intro.
Inversion H8.
Simpl in H10.
Elim (OBJNAMEeq_dec p (ObjName o)).
Intro.
Cut (fOSC (objectSC s) o)=(None SecClass).
Intro.
Rewrite H12 in H9; Discriminate H9.
Unfold fOSC; Apply NotInDOMIsUndef.
Replace (DOM OBJeq_dec (objectSC s)) with (DOM OBJeq_dec (acl s)).
Rewrite a in H2; Rewrite a in H4; Auto.
Auto.
Intro.
Cut x=y.
Intro.
Cut False.
Tauto.
Rewrite H12 in H11; Inversion H11; Auto.
Cut (fOSC (objectSC s) o)=(fOSC (mkdir_oSC s Sub p) o).
Intro EQ; Rewrite <- EQ in H10; Rewrite H10 in H9; Injection H9; Auto.
Auto.
Intros;
Absurd (MACSubCtrlAttrHaveChanged s
(mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s)
(RootGrp s) (SecAdmGrp s) (mkdir_oSC s Sub p)
(mkdir_acl s Sub p perms) (secmat s) (files s)
(mkdir_directories Sub p)) u0); Auto.
Qed.
End mkdirIsSecure.
Hints Resolve MkdirPSS MkdirPSP MkdirPCP.