Verification: chown |
Require ModelProperties.
Require AuxiliaryLemmas.
Section chownIsSecure.
|
|
Lemma ChownPSS:
(s,t:SFSstate; u:SUBJECT)
(SecureState s)->(TransFunc u s Chown 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 chown_acl.
Simpl.
Elim (facl (acl s) o).
Intro.
Replace (facl
(set_add ACLeq_dec
(o,
(acldata p g (UsersReaders a)
Cases
(set_In_dec GRPeq_dec (group a)
(GroupReaders a))
of
(left _) =>
(set_add GRPeq_dec g
(set_remove GRPeq_dec (group a)
(GroupReaders a)))
| (right _) => (GroupReaders a)
end (UsersWriters a)
Cases
(set_In_dec GRPeq_dec (group a)
(GroupWriters a))
of
(left _) =>
(set_add GRPeq_dec g
(set_remove GRPeq_dec (group a)
(GroupWriters a)))
| (right _) => (GroupWriters a)
end
(set_add SUBeq_dec p
(set_remove SUBeq_dec (owner 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 ChownPSP:
(s,t:SFSstate; u:SUBJECT)
(StarProperty s)->(TransFunc u s Chown t)->(StarProperty t).
StartPSP.
Inversion H; Auto.
Qed.
|
|
Lemma ChownPCP:
(s,t:SFSstate)(PreservesControlProp s Chown 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 (chown_acl s o p g) o0)=(facl (acl s) o0).
Intro H11; Rewrite H11 in H8; Rewrite H7 in H8; Injection H8; Auto.
Symmetry.
Unfold chown_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 (chown_acl s o p g) o0)=(facl (acl s) o0).
Intro H11; Rewrite H11 in H8; Rewrite H7 in H8; Injection H8; Auto.
Symmetry.
Unfold chown_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) (chown_acl s o p g)
(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) (chown_acl s o p g)
(secmat s) (files s) (directories s)) u0);
Auto.
Qed.
End chownIsSecure.
Hints Resolve ChownPSS ChownPSP ChownPCP.