# HG changeset patch # User chunhan # Date 1386081768 -28800 # Node ID 99af1986e1e0ae1ff99f22050fbe9beb461e3dcc # Parent 271e9818b6f665cfb8522bbea889294639529fae update diff -r 271e9818b6f6 -r 99af1986e1e0 simple_selinux/Alive_prop.thy --- a/simple_selinux/Alive_prop.thy Mon Dec 02 10:52:40 2013 +0800 +++ b/simple_selinux/Alive_prop.thy Tue Dec 03 22:42:48 2013 +0800 @@ -311,7 +311,6 @@ \ p f. e \ UnLink p f; \ p d. e \ Rmdir p d; \ p d inum. e \ Mkdir p d inum; - \ p f f'. e \ LinkHard p f f'; \ p q. e \ CreateMsgq p q; \ p q m. e \ SendMsg p q m; \ p q m. e \ RecvMsg p q m; diff -r 271e9818b6f6 -r 99af1986e1e0 simple_selinux/Co2sobj_prop.thy --- a/simple_selinux/Co2sobj_prop.thy Mon Dec 02 10:52:40 2013 +0800 +++ b/simple_selinux/Co2sobj_prop.thy Tue Dec 03 22:42:48 2013 +0800 @@ -24,7 +24,7 @@ apply (frule vt_grant_os, frule vd_cons, rule ext, rule ext) unfolding cm2smsg_def apply (case_tac e) -apply (auto simp:sectxt_of_obj_simps tainted_eq_Tainted +apply (auto simp:sectxt_of_obj_simps split:t_object.splits option.splits if_splits dest:not_deleted_init_msg dest!:current_has_sec') done @@ -37,7 +37,7 @@ | _ \ None) else cm2smsg s q' m') " apply (frule vd_cons, frule vt_grant_os, rule ext, rule ext) -apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps +apply (auto simp:cm2smsg_def sectxt_of_obj_simps split:if_splits option.splits dest:not_deleted_init_msg dest!:current_has_sec') done @@ -45,35 +45,35 @@ lemma cm2smsg_recvmsg1: "\q' \ q; valid (RecvMsg p q m # s)\ \ cm2smsg (RecvMsg p q m # s) q' = cm2smsg s q'" apply (frule vd_cons, frule vt_grant_os, rule ext) -apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps +apply (auto simp:cm2smsg_def sectxt_of_obj_simps split:if_splits option.splits) done lemma cm2smsg_recvmsg2: "\m' \ m; valid (RecvMsg p q m # s)\ \ cm2smsg (RecvMsg p q m # s) q m' = cm2smsg s q m'" apply (frule vd_cons, frule vt_grant_os) -apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps +apply (auto simp:cm2smsg_def sectxt_of_obj_simps split:if_splits option.splits) done lemma cm2smsg_recvmsg1': "\valid (RecvMsg p q m # s); q' \ q\ \ cm2smsg (RecvMsg p q m # s) q' = cm2smsg s q'" apply (frule vd_cons, frule vt_grant_os, rule ext) -apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps +apply (auto simp:cm2smsg_def sectxt_of_obj_simps split:if_splits option.splits) done lemma cm2smsg_recvmsg2': "\valid (RecvMsg p q m # s); m' \ m\ \ cm2smsg (RecvMsg p q m # s) q m' = cm2smsg s q m'" apply (frule vd_cons, frule vt_grant_os) -apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps +apply (auto simp:cm2smsg_def sectxt_of_obj_simps split:if_splits option.splits) done lemma cm2smsg_removemsgq: "\q' \ q; valid (RemoveMsgq p q # s)\ \ cm2smsg (RemoveMsgq p q # s) q' = cm2smsg s q'" apply (frule vd_cons, frule vt_grant_os, rule ext) -apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps +apply (auto simp:cm2smsg_def sectxt_of_obj_simps split:if_splits option.splits) done @@ -358,6 +358,7 @@ apply (drule cq2smsg_createmsgq, simp, simp) apply (drule_tac m = m and q = q and qi = qi and qsec = "(aa,ab,b)" in p1, simp+) + apply (drule_tac m = m and q = q and qi = qi and qsec = "(aa,ab,b)" in p1, simp+) apply (simp add:cq2smsgq_def split:option.splits) apply (rule_tac m = m and sm = sm in cqm2sms_prop0, simp+) @@ -670,62 +671,6 @@ apply (simp add:cf2sfile_mkdir1 current_files_simps) done -lemma cf2sfile_linkhard1: - "\valid (LinkHard p oldf f # s); f' \ current_files s\ - \ cf2sfile (LinkHard p oldf f# s) f' = cf2sfile s f'" -apply (frule vd_cons, frule vt_grant_os, frule noroot_events) -apply (case_tac "f = f'", simp) -apply (induct f', simp add:sroot_only, simp) -apply (frule parentf_in_current', simp+) -apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps - get_parentfs_ctxts_simps split:if_splits option.splits) -done - -lemma cf2sfile_linkhard2: - "\valid (LinkHard p oldf f # s); is_file s f'\ - \ cf2sfile (LinkHard p oldf f # s) f' = cf2sfile s f'" -apply (frule vd_cons, drule is_file_in_current) -by (simp add:cf2sfile_linkhard1) - -lemma cf2sfile_linkhard3: - "\valid (LinkHard p oldf f # s); is_dir s f'\ - \ cf2sfile (LinkHard p oldf f # s) f' = cf2sfile s f'" -apply (frule vd_cons, drule is_dir_in_current) -by (simp add:cf2sfile_linkhard1) - -lemma cf2sfile_linkhard4: - "valid (LinkHard p oldf f # s) - \ cf2sfile (LinkHard p oldf f # s) f = (case (parent f) of - Some pf \ (case (sectxt_of_obj (LinkHard p oldf f # s) (O_file f), sectxt_of_obj s (O_dir pf), - get_parentfs_ctxts s pf) of - (Some sec, Some psec, Some asecs) \ Some (Created, sec, Some psec, set asecs) - | _ \ None) - | None \ None)" -apply (frule vd_cons, frule vt_grant_os, frule noroot_events) -apply (case_tac f, simp) -apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps - get_parentfs_ctxts_simps) -apply (rule impI, (erule conjE)+) -apply (drule not_deleted_init_file, simp+) -apply (simp add:is_file_in_current) -done - -lemma cf2sfile_linkhard: - "\valid (LinkHard p oldf f # s); f' \ current_files (LinkHard p oldf f # s)\ - \ cf2sfile (LinkHard p oldf f # s) f' = ( - if (f' = f) - then (case (parent f) of - Some pf \ (case (sectxt_of_obj (LinkHard p oldf f # s) (O_file f), sectxt_of_obj s (O_dir pf), - get_parentfs_ctxts s pf) of - (Some sec, Some psec, Some asecs) \ Some (Created, sec, Some psec, set asecs) - | _ \ None) - | None \ None) - else cf2sfile s f')" -apply (case_tac "f = f'") -apply (simp add:cf2sfile_linkhard4 split:option.splits) -apply (simp add:cf2sfile_linkhard1 current_files_simps) -done - lemma cf2sfile_other: "\ff \ current_files s; \ p f flag fd opt. e \ Open p f flag fd opt; @@ -733,7 +678,6 @@ \ p f. e \ UnLink p f; \ p f. e \ Rmdir p f; \ p f i. e \ Mkdir p f i; - \ p f f'. e \ LinkHard p f f'; valid (e # s)\ \ cf2sfile (e # s) ff = cf2sfile s ff" apply (frule vd_cons, frule vt_grant_os) apply (induct ff, simp add:sroot_only) @@ -749,7 +693,6 @@ \ p f. e \ UnLink p f; \ p f. e \ Rmdir p f; \ p f i. e \ Mkdir p f i; - \ p f f'. e \ LinkHard p f f'; ff \ current_files s\ \ cf2sfile (e # s) ff = cf2sfile s ff" by (auto intro!:cf2sfile_other) @@ -785,15 +728,17 @@ apply (frule vd_cons, frule vt_grant_os) apply (simp add:current_files_simps split:if_splits option.splits) (* costs too much time, but solved *) - +(* apply (auto simp:cf2sfile_def sectxt_of_obj_simps get_parentfs_ctxts_simps is_file_simps is_dir_simps split:if_splits option.splits dest:init_file_dir_conflict pfdof_simp5 pfdof_simp6 file_of_pfd_is_file not_deleted_init_file not_deleted_init_dir is_file_not_dir is_dir_not_file dest!:current_has_sec') done +*) +sorry -lemmas cf2sfile_simps = cf2sfile_open cf2sfile_mkdir cf2sfile_linkhard cf2sfile_other +lemmas cf2sfile_simps = cf2sfile_open cf2sfile_mkdir cf2sfile_other cf2sfile_unlink cf2sfile_rmdir cf2sfile_closefd (*********** cfd2sfd simpset *********) @@ -871,8 +816,8 @@ done lemma cfd2sfd_clone: - "\valid (Clone p p' fds shms # s); file_of_proc_fd (Clone p p' fds shms # s) p'' fd' = Some f\ - \ cfd2sfd (Clone p p' fds shms # s) p'' fd' = ( + "\valid (Clone p p' fds # s); file_of_proc_fd (Clone p p' fds # s) p'' fd' = Some f\ + \ cfd2sfd (Clone p p' fds # s) p'' fd' = ( if (p'' = p') then cfd2sfd s p fd' else cfd2sfd s p'' fd')" apply (frule vd_cons, frule vt_grant_os) @@ -927,7 +872,7 @@ lemma cfd2sfd_other: "\valid (e # s); file_of_proc_fd (e # s) p' fd' = Some f'; \ p f flags fd opt. e \ Open p f flags fd opt; - \ p p'' fds shms. e \ Clone p p'' fds shms\ + \ p p'' fds. e \ Clone p p'' fds\ \ cfd2sfd (e # s) p' fd' = cfd2sfd s p' fd'" apply (frule vd_cons, frule vt_grant_os) apply (frule proc_fd_in_fds, simp) @@ -1057,8 +1002,8 @@ done lemma cpfd2sfds_clone: - "valid (Clone p p' fds shms # s) - \ cpfd2sfds (Clone p p' fds shms # s) = (cpfd2sfds s) (p' := {sfd. \ fd \ fds. \ f. file_of_proc_fd s p fd = Some f \ cfd2sfd s p fd = Some sfd})" + "valid (Clone p p' fds # s) + \ cpfd2sfds (Clone p p' fds # s) = (cpfd2sfds s) (p' := {sfd. \ fd \ fds. \ f. file_of_proc_fd s p fd = Some f \ cfd2sfd s p fd = Some sfd})" apply (frule vd_cons, frule vt_grant_os) apply (rule ext) apply (rule set_eqI, rule iffI) @@ -1087,7 +1032,7 @@ \ p p'. e \ Kill p p'; \ p. e \ Exit p; \ p fd. e \ CloseFd p fd; - \ p p' fds shms. e \ Clone p p' fds shms\ \ cpfd2sfds (e # s) = cpfd2sfds s" + \ p p' fds. e \ Clone p p' fds\ \ cpfd2sfds (e # s) = cpfd2sfds s" apply (frule vd_cons, frule vt_grant_os) apply (rule ext) unfolding cpfd2sfds_def proc_file_fds_def @@ -1185,265 +1130,13 @@ lemmas cpfd2sfds_simps = cpfd2sfds_open cpfd2sfds_execve cpfd2sfds_clone cpfd2sfds_kill cpfd2sfds_exit cpfd2sfds_closefd cpfd2sfds_other -(********* ch2sshm simpset ********) - -lemma ch2sshm_createshm: - "valid (CreateShM p h # s) - \ ch2sshm (CreateShM p h # s) = (ch2sshm s) (h := - (case (sectxt_of_obj (CreateShM p h # s) (O_shm h)) of - Some sec \ - Some (if (\ deleted (O_shm h) s \ h \ init_shms) then Init h else Created, sec) - | _ \ None))" -apply (frule vd_cons, frule vt_grant_os) -apply (auto simp:ch2sshm_def sectxt_of_obj_simps dest!:current_has_sec' split:option.splits if_splits) -done - -lemma ch2sshm_other: - "\valid (e # s); - \ p h. e \ CreateShM p h; - h' \ current_shms (e # s)\ \ ch2sshm (e # s) h' = ch2sshm s h'" -apply (frule vd_cons, frule vt_grant_os) -apply (case_tac e) -apply (auto simp:ch2sshm_def sectxt_of_obj_simps dest!:current_has_sec' split:option.splits if_splits) -done - -lemmas ch2sshm_simps = ch2sshm_createshm ch2sshm_other - -lemma current_shm_has_sh: - "\h \ current_shms s; valid s\ \ \ sh. ch2sshm s h = Some sh" -by (auto simp:ch2sshm_def split:option.splits dest!:current_has_sec') - -lemma current_shm_has_sh': - "\ch2sshm s h = None; valid s\ \ h \ current_shms s" -by (auto dest:current_shm_has_sh) - -(********** cph2spshs simpset **********) - -lemma cph2spshs_attach: - "valid (Attach p h flag # s) \ - cph2spshs (Attach p h flag # s) = (cph2spshs s) (p := - (case (ch2sshm s h) of - Some sh \ cph2spshs s p \ {(sh, flag)} - | _ \ cph2spshs s p) )" -apply (frule vd_cons, frule vt_grant_os, rule ext) -using ch2sshm_other[where e = "Attach p h flag" and s = s] -apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits -dest!:current_shm_has_sh' dest: procs_of_shm_prop1 simp:cph2spshs_def) -apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp) -apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp) -apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp) -apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp) -apply (erule_tac x = ha in allE, frule procs_of_shm_prop1, simp, simp) -apply (case_tac "ha = h", simp, frule procs_of_shm_prop1, simp) -apply (rule_tac x = ha in exI, simp) -apply (rule_tac x = ha in exI, simp, drule procs_of_shm_prop1, simp, simp) -apply (rule_tac x = ha in exI, simp) -apply (frule procs_of_shm_prop1, simp, simp) -apply (rule impI, simp) -done - -lemma cph2spshs_detach: "valid (Detach p h # s) \ - cph2spshs (Detach p h # s) = (cph2spshs s) (p := - (case (ch2sshm s h, flag_of_proc_shm s p h) of - (Some sh, Some flag) \ if (\ h'. h' \ h \ (p,flag) \ procs_of_shm s h' \ ch2sshm s h' = Some sh) - then cph2spshs s p else cph2spshs s p - {(sh, flag)} - | _ \ cph2spshs s p) )" -apply (frule vd_cons, frule vt_grant_os, rule ext) -apply (case_tac "x = p") defer -using ch2sshm_other[where e = "Detach p h" and s = s] -apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits -dest!:current_shm_has_sh' procs_of_shm_prop4' dest:procs_of_shm_prop1 procs_of_shm_prop3 simp:cph2spshs_def) [1] -apply (rule_tac x = ha in exI, frule_tac h = ha in procs_of_shm_prop1, simp, simp) -apply (rule_tac x = ha in exI, frule_tac h = ha in procs_of_shm_prop1, simp, simp) -apply (rule impI, simp) - -apply (clarsimp) -apply (frule current_shm_has_sh, simp, erule exE) -apply (frule procs_of_shm_prop4, simp, simp) -apply (rule allI | rule conjI| erule conjE | erule exE | rule impI)+ - -apply (simp only:cph2spshs_def, rule set_eqI, rule iffI) -apply (erule CollectE | erule exE| erule conjE| rule CollectI)+ -apply (case_tac "ha = h", simp) -apply (rule_tac x = sha in exI, rule_tac x = flaga in exI, rule_tac x = ha in exI, simp) -using ch2sshm_other[where e = "Detach p h" and s = s] apply (simp add:procs_of_shm_prop1) - -apply (erule CollectE | erule exE| erule conjE| rule CollectI)+ -apply (case_tac "ha = h", simp) -apply (rule_tac x = h' in exI, simp) -apply (frule_tac flag = flag and flag' = flaga in procs_of_shm_prop3, simp+) -apply (frule_tac flag = flaga in procs_of_shm_prop4, simp+) -using ch2sshm_other[where e = "Detach p h" and s = s] apply (simp add:procs_of_shm_prop1) -apply (frule_tac h = h' in procs_of_shm_prop1, simp, simp) -apply (rule_tac x = ha in exI, simp, frule_tac h = ha in procs_of_shm_prop1, simp+) -using ch2sshm_other[where e = "Detach p h" and s = s] apply (simp add:procs_of_shm_prop1) - -apply (rule allI | rule conjI| erule conjE | erule exE | rule impI)+ -apply (simp only:cph2spshs_def, rule set_eqI, rule iffI) -apply (erule CollectE | erule exE| erule conjE| rule DiffI |rule CollectI)+ -apply (simp split:if_splits) -apply (rule_tac x = ha in exI, simp, frule_tac h = ha in procs_of_shm_prop1, simp+) -using ch2sshm_other[where e = "Detach p h" and s = s] apply (simp add:procs_of_shm_prop1) -apply (rule notI, simp split:if_splits) -apply (erule_tac x = ha in allE, simp, frule_tac h = ha in procs_of_shm_prop1, simp+) -using ch2sshm_other[where e = "Detach p h" and s = s] apply (simp add:procs_of_shm_prop1) -apply (erule CollectE | erule exE| erule conjE| erule DiffE |rule CollectI)+ -apply (simp split:if_splits) -apply (erule_tac x = ha in allE, simp, rule_tac x = ha in exI, simp) -apply (case_tac "ha = h", simp add:procs_of_shm_prop3, frule_tac h = ha in procs_of_shm_prop1, simp+) -using ch2sshm_other[where e = "Detach p h" and s = s] apply (simp add:procs_of_shm_prop1) -done - -lemma cph2spshs_deleteshm: - "valid (DeleteShM p h # s) \ - cph2spshs (DeleteShM p h # s) = (\ p'. - (case (ch2sshm s h, flag_of_proc_shm s p' h) of - (Some sh, Some flag) \ if (\ h'. h' \ h \ (p', flag) \ procs_of_shm s h' \ ch2sshm s h' = Some sh) - then cph2spshs s p' else cph2spshs s p' - {(sh, flag)} - | _ \ cph2spshs s p') )" -apply (frule vd_cons, frule vt_grant_os, rule ext) - -apply (clarsimp) -apply (frule current_shm_has_sh, simp, erule exE, simp, simp split:option.splits) -apply (rule conjI, rule impI) -using ch2sshm_other[where e = "DeleteShM p h" and s = s] -apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits -dest!:current_shm_has_sh' procs_of_shm_prop4' dest:procs_of_shm_prop1 procs_of_shm_prop3 simp:cph2spshs_def) [1] -apply (rule_tac x = ha in exI, frule_tac h = ha in procs_of_shm_prop1, simp+) -apply (rule_tac x = ha in exI, simp) -apply (case_tac "ha = h", simp+, frule_tac h = ha in procs_of_shm_prop1, simp+) - -apply (rule allI | rule conjI| erule conjE | erule exE | rule impI)+ - -apply (simp only:cph2spshs_def, rule set_eqI, rule iffI) -apply (erule CollectE | erule exE| erule conjE| rule CollectI)+ -apply (case_tac "ha = h", simp) -apply (rule_tac x = sha in exI, rule_tac x = flag in exI, rule_tac x = ha in exI, simp) -using ch2sshm_other[where e = "DeleteShM p h" and s = s] apply (simp add:procs_of_shm_prop1) - -apply (erule CollectE | erule exE| erule conjE| rule CollectI)+ -apply (case_tac "ha = h", simp) -apply (rule_tac x = h' in exI, simp) -apply (frule_tac flag = flag in procs_of_shm_prop4, simp+) -using ch2sshm_other[where e = "DeleteShM p h" and s = s] apply (simp add:procs_of_shm_prop1) -apply (frule_tac h = h' in procs_of_shm_prop1, simp, simp) -apply (rule_tac x = ha in exI, simp, frule_tac h = ha in procs_of_shm_prop1, simp+) -using ch2sshm_other[where e = "DeleteShM p h" and s = s] apply (simp add:procs_of_shm_prop1) - -apply (rule allI | rule conjI| erule conjE | erule exE | rule impI)+ -apply (simp only:cph2spshs_def, rule set_eqI, rule iffI) -apply (erule CollectE | erule exE| erule conjE| rule DiffI |rule CollectI)+ -apply (simp split:if_splits) -apply (rule_tac x = ha in exI, simp, frule_tac h = ha in procs_of_shm_prop1, simp+) -using ch2sshm_other[where e = "DeleteShM p h" and s = s] apply (simp add:procs_of_shm_prop1) -apply (rule notI, simp split:if_splits) -apply (erule_tac x = ha in allE, simp, frule_tac h = ha in procs_of_shm_prop1, simp+) -using ch2sshm_other[where e = "DeleteShM p h" and s = s] apply (simp add:procs_of_shm_prop1) -apply (erule CollectE | erule exE| erule conjE| erule DiffE |rule CollectI)+ -apply (simp split:if_splits) -apply (erule_tac x = ha in allE, simp, rule_tac x = ha in exI, simp) -apply (case_tac "ha = h", simp add:procs_of_shm_prop4) -apply (frule_tac h = ha in procs_of_shm_prop1, simp+) -using ch2sshm_other[where e = "DeleteShM p h" and s = s] apply (simp add:procs_of_shm_prop1) -done - -lemma flag_of_proc_shm_prop1: - "\flag_of_proc_shm s p h = Some flag; valid s\ \ (p, flag) \ procs_of_shm s h" -apply (induct s arbitrary:p) -apply (simp add:init_shmflag_has_proc) -apply (frule vt_grant_os, frule vd_cons, case_tac a, auto split:if_splits option.splits) -done - -lemma cph2spshs_clone: - "valid (Clone p p' fds shms # s) \ - cph2spshs (Clone p p' fds shms # s) = (cph2spshs s) (p' := - {(sh, flag) | h sh flag. h \ shms \ ch2sshm s h = Some sh \ flag_of_proc_shm s p h = Some flag} )" -apply (frule vd_cons, frule vt_grant_os, rule ext) -using ch2sshm_other[where e = "Clone p p' fds shms" and s = s] -apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits -dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3 simp:cph2spshs_def) -apply (erule_tac x = h in allE, frule procs_of_shm_prop1, simp, simp add:procs_of_shm_prop4) -apply (rule_tac x = h in exI, simp, frule flag_of_proc_shm_prop1, simp+, simp add:procs_of_shm_prop1) -apply (rule_tac x = h in exI, simp, frule procs_of_shm_prop1, simp+)+ -done - -lemma cph2spshs_execve: - "valid (Execve p f fds # s) \ - cph2spshs (Execve p f fds # s) = (cph2spshs s) (p := {})" -apply (frule vd_cons, frule vt_grant_os, rule ext) -using ch2sshm_other[where e = "Execve p f fds" and s = s] -apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits -dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3 simp:cph2spshs_def) -apply (rule_tac x = h in exI, simp add:procs_of_shm_prop1)+ -done - -lemma cph2spshs_kill: - "valid (Kill p p' # s) \ cph2spshs (Kill p p' # s) = (cph2spshs s) (p' := {})" -apply (frule vd_cons, frule vt_grant_os, rule ext) -using ch2sshm_other[where e = "Kill p p'" and s = s] -apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits -dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3 simp:cph2spshs_def) -apply (rule_tac x = h in exI, simp add:procs_of_shm_prop1)+ -done - -lemma cph2spshs_exit: - "valid (Exit p # s) \ cph2spshs (Exit p # s) = (cph2spshs s) (p := {})" -apply (frule vd_cons, frule vt_grant_os, rule ext) -using ch2sshm_other[where e = "Exit p" and s = s] -apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits -dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3 simp:cph2spshs_def) -apply (rule_tac x = h in exI, simp add:procs_of_shm_prop1)+ -done - -lemma cph2spshs_createshm: - "valid (CreateShM p h # s) \ cph2spshs (CreateShM p h # s) = cph2spshs s" -apply (frule vt_grant_os, frule vd_cons, rule ext) -apply (auto simp:cph2spshs_def) -using ch2sshm_createshm -apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits -dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3 simp:cph2spshs_def) -apply (rule_tac x = ha in exI, auto simp:procs_of_shm_prop1) -done - -lemma cph2spshs_other: - "\valid (e # s); - \ p h flag. e \ Attach p h flag; - \ p h. e \ Detach p h; - \ p h. e \ DeleteShM p h; - \ p p' fds shms. e \ Clone p p' fds shms; - \ p f fds. e \ Execve p f fds; - \ p p'. e \ Kill p p'; - \ p. e \ Exit p\ \ cph2spshs (e # s) = cph2spshs s" -apply (frule vt_grant_os, frule vd_cons, rule ext) -unfolding cph2spshs_def -apply (rule set_eqI, rule iffI) -apply (erule CollectE | erule conjE| erule exE| rule conjI| rule impI| rule CollectI)+ -apply (frule procs_of_shm_prop1, simp, rule_tac x= sh in exI, rule_tac x = flag in exI, rule_tac x = h in exI) -apply (case_tac e) -using ch2sshm_other[where e = e and s = s] -apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits -dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3 - simp:ch2sshm_createshm) -apply (rule_tac x = h in exI, case_tac e) -using ch2sshm_other[where e = e and s = s] -apply (auto split del:t_open_must_flag.splits t_open_option_flag.splits split add:if_splits option.splits -dest!:current_shm_has_sh' dest: procs_of_shm_prop1 procs_of_shm_prop2 procs_of_shm_prop3 - simp:ch2sshm_createshm) -done - -lemmas cph2spshs_simps = cph2spshs_attach cph2spshs_detach cph2spshs_deleteshm cph2spshs_clone cph2spshs_execve - cph2spshs_exit cph2spshs_kill cph2spshs_other - -(******** cp2sproc simpset *********) - lemma cp2sproc_clone: - "valid (Clone p p' fds shms # s) \ cp2sproc (Clone p p' fds shms # s) = (cp2sproc s) (p' := + "valid (Clone p p' fds # s) \ cp2sproc (Clone p p' fds # s) = (cp2sproc s) (p' := case (sectxt_of_obj s (O_proc p)) of Some sec \ Some (Created, sec, - {sfd. \ fd \ fds. \ f. file_of_proc_fd s p fd = Some f \ cfd2sfd s p fd = Some sfd}, - {(sh, flag) | h sh flag. h \ shms \ ch2sshm s h = Some sh \ flag_of_proc_shm s p h = Some flag}) + {sfd. \ fd \ fds. \ f. file_of_proc_fd s p fd = Some f \ cfd2sfd s p fd = Some sfd}) | _ \ None)" -apply (frule cph2spshs_clone, frule cpfd2sfds_clone) +apply (frule cpfd2sfds_clone) apply (frule vd_cons, frule vt_grant_os, simp only:os_grant.simps) apply ((erule exE| erule conjE)+, frule not_init_intro_proc, simp, rule ext, case_tac "x = p'", simp) apply (auto simp:cp2sproc_def sectxt_of_obj_simps dest!:current_has_sec' @@ -1454,14 +1147,11 @@ "\valid (e # s); \ p f flags fd opt. e \ Open p f flags fd opt; \ p fd. e \ CloseFd p fd; - \ p h flag. e \ Attach p h flag; - \ p h. e \ Detach p h; - \ p h. e \ DeleteShM p h; - \ p p' fds shms. e \ Clone p p' fds shms; + \ p p' fds. e \ Clone p p' fds; \ p f fds. e \ Execve p f fds; \ p p'. e \ Kill p p'; \ p. e \ Exit p\ \ cp2sproc (e # s) = cp2sproc s" -apply (frule cph2spshs_other, simp+, frule cpfd2sfds_other, simp+) +apply (frule cpfd2sfds_other, simp+) apply (frule vt_grant_os, frule vd_cons, rule ext, case_tac e, simp_all) apply (auto simp:cp2sproc_def sectxt_of_obj_simps dest!:current_has_sec' dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits) @@ -1474,9 +1164,8 @@ cf2sfile (Open p f flags fd opt # s) f) of (Some sec, Some fdsec, Some sf) \ Some (if (\ deleted (O_proc p) s \ p \ init_procs) then Init p else Created, sec, - (cpfd2sfds s p) \ {(fdsec, flags, sf)}, cph2spshs s p) + (cpfd2sfds s p) \ {(fdsec, flags, sf)}) | _ \ None)" -apply (frule cph2spshs_other, simp, simp, simp, simp, simp, simp, simp) apply (frule cpfd2sfds_open, frule vt_grant_os, frule vd_cons, rule ext) apply (case_tac "x = p") apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps @@ -1494,29 +1183,11 @@ else (case (sectxt_of_obj s (O_proc p)) of Some sec \ Some (if (\ deleted (O_proc p) s \ p \ init_procs) then Init p else Created, - sec, cpfd2sfds s p - {sfd}, cph2spshs s p) + sec, cpfd2sfds s p - {sfd}) | _ \ None)) | _ \ cp2sproc s p) else cp2sproc s p)" -apply (frule cpfd2sfds_closefd, frule cph2spshs_other, simp, simp, simp, simp, simp, simp, simp) -apply (frule vt_grant_os, frule vd_cons, rule ext) -apply (case_tac "x = p") -apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps - dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current - dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits) -done - -lemma cp2sproc_attach: - "valid (Attach p h flag # s) \ - cp2sproc (Attach p h flag # s) = (cp2sproc s) (p := - (case (ch2sshm s h) of - Some sh \ (case (sectxt_of_obj s (O_proc p)) of - Some sec \ Some (if (\ deleted (O_proc p) s \ p \ init_procs) - then Init p else Created, - sec, cpfd2sfds s p, cph2spshs s p \ {(sh, flag)}) - | _ \ None) - | _ \ cp2sproc s p) )" -apply (frule cph2spshs_attach, frule cpfd2sfds_other, simp, simp, simp, simp, simp, simp) +apply (frule cpfd2sfds_closefd) apply (frule vt_grant_os, frule vd_cons, rule ext) apply (case_tac "x = p") apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps @@ -1524,53 +1195,14 @@ dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits) done -lemma cp2sproc_detach: - "valid (Detach p h # s) \ - cp2sproc (Detach p h # s) = (cp2sproc s) (p := - (case (ch2sshm s h, flag_of_proc_shm s p h) of - (Some sh, Some flag) \ if (\ h'. h' \ h \ (p,flag) \ procs_of_shm s h' \ ch2sshm s h' = Some sh) - then cp2sproc s p - else (case (sectxt_of_obj s (O_proc p)) of - Some sec \ Some (if (\ deleted (O_proc p) s \ p \ init_procs) - then Init p else Created, sec, - cpfd2sfds s p, cph2spshs s p - {(sh, flag)}) - | None \ None) - | _ \ cp2sproc s p) )" -apply (frule cph2spshs_detach, frule cpfd2sfds_other, simp, simp, simp, simp, simp, simp) -apply (frule vt_grant_os, frule vd_cons, rule ext) -apply (case_tac "x = p") -apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps - dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current - dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits) -done - -lemma cp2sproc_deleteshm: - "valid (DeleteShM p h # s) \ - cp2sproc (DeleteShM p h # s) = (\ p'. - (case (ch2sshm s h, flag_of_proc_shm s p' h) of - (Some sh, Some flag) \ if (\ h'. h' \ h \ (p', flag) \ procs_of_shm s h' \ ch2sshm s h' = Some sh) - then cp2sproc s p' - else (case (sectxt_of_obj s (O_proc p')) of - Some sec \ Some (if (\ deleted (O_proc p') s \ p' \ init_procs) - then Init p' else Created, sec, - cpfd2sfds s p', cph2spshs s p' - {(sh, flag)}) - | None \ None) - | _ \ cp2sproc s p') )" -apply (frule cph2spshs_deleteshm, frule cpfd2sfds_other, simp, simp, simp, simp, simp, simp) -apply (frule vt_grant_os, frule vd_cons, rule ext) -apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps - dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current - dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits) -done - lemma cp2sproc_execve: "valid (Execve p f fds # s) \ cp2sproc (Execve p f fds # s) = (cp2sproc s) (p := (case (sectxt_of_obj (Execve p f fds # s) (O_proc p)) of Some sec \ Some (if (\ deleted (O_proc p) s \ p \ init_procs) then Init p else Created, sec, - {sfd. \ fd \ fds. \ f. file_of_proc_fd s p fd = Some f \ cfd2sfd s p fd = Some sfd}, {}) + {sfd. \ fd \ fds. \ f. file_of_proc_fd s p fd = Some f \ cfd2sfd s p fd = Some sfd}) | _ \ None) )" -apply (frule cph2spshs_execve, frule cpfd2sfds_execve) +apply (frule cpfd2sfds_execve) apply (frule vt_grant_os, frule vd_cons, rule ext) apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current @@ -1580,7 +1212,7 @@ lemma cp2sproc_kill: "\valid (Kill p p' # s); p'' \ p'\ \ cp2sproc (Kill p p' # s) p'' = (cp2sproc s) p''" -apply (frule cph2spshs_kill, frule cpfd2sfds_kill) +apply (frule cpfd2sfds_kill) apply (frule vt_grant_os, frule vd_cons) apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current @@ -1595,7 +1227,7 @@ lemma cp2sproc_exit: "\valid (Exit p # s); p' \ p\ \ cp2sproc (Exit p # s) p' = (cp2sproc s) p'" -apply (frule cph2spshs_exit, frule cpfd2sfds_exit) +apply (frule cpfd2sfds_exit) apply (frule vt_grant_os, frule vd_cons) apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current @@ -1607,8 +1239,8 @@ cp2sproc (Exit p # s) p' = (cp2sproc s) p'" by (drule_tac p'= p' in cp2sproc_exit, simp+) -lemmas cp2sproc_simps = cp2sproc_open cp2sproc_closefd cp2sproc_attach cp2sproc_detach cp2sproc_deleteshm - cp2sproc_clone cp2sproc_execve cp2sproc_kill cp2sproc_exit cp2sproc_other +lemmas cp2sproc_simps = cp2sproc_open cp2sproc_closefd cp2sproc_clone cp2sproc_execve + cp2sproc_kill cp2sproc_exit cp2sproc_other lemma current_proc_has_sp: "\p \ current_procs s; valid s\ \ \ sp. cp2sproc s p = Some sp" @@ -1618,230 +1250,23 @@ "\cp2sproc s p = None; valid s\ \ p \ current_procs s" by (auto dest:current_proc_has_sp) - - -(* simpset for cf2sfiles *) - -lemma cf2sfiles_open: - "\valid (Open p f flag fd opt # s); f' \ current_files (Open p f flag fd opt # s)\ - \ cf2sfiles (Open p f flag fd opt # s) f' = ( - if (f' = f \ opt \ None) - then (case cf2sfile (Open p f flag fd opt # s) f of - Some sf \ {sf} - | _ \ {} ) - else cf2sfiles s f')" -apply (frule vt_grant_os, frule vd_cons) -apply (auto simp:cf2sfiles_def cf2sfile_open_none cf2sfile_simps same_inode_files_open - split:if_splits option.splits dest!:current_file_has_sfile' dest:cf2sfile_open) -apply (rule_tac x = "f'a" in bexI, drule same_inode_files_prop1, simp add:cf2sfile_open_some1, simp)+ -done - -lemma cf2sfiles_other: - "\valid (e # s); - \ p f flag fd opt. e \ Open p f flag fd opt; - \ p fd. e \ CloseFd p fd; - \ p f. e \ UnLink p f; - \ p f f'. e \ LinkHard p f f'\ \ cf2sfiles (e # s) = cf2sfiles s" -apply (frule vt_grant_os, frule vd_cons, rule ext) -apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI) -apply (drule Set.CollectD, erule bexE, rule CollectI) -apply (rule_tac x = f' in bexI, case_tac e) -apply (auto simp:cf2sfiles_def cf2sfile_simps same_inode_files_simps current_files_simps - split:if_splits option.splits dest!:current_file_has_sfile' dest:same_inode_files_prop1 cf2sfile_other') -apply (drule_tac f' = f' in cf2sfile_rmdir) -apply (simp add:current_files_simps same_inode_files_prop1 same_inode_files_prop3 dir_is_empty_def)+ - -apply (rule_tac x = f' in bexI, case_tac e) -apply (auto simp:cf2sfiles_def cf2sfile_simps same_inode_files_simps current_files_simps - split:if_splits option.splits dest!:current_file_has_sfile' dest:same_inode_files_prop1 cf2sfile_other') -apply (drule_tac f' = f' in cf2sfile_rmdir) -apply (simp add:current_files_simps same_inode_files_prop1 same_inode_files_prop3 dir_is_empty_def)+ -done - -lemma cf2sfile_linkhard1': - "\valid (LinkHard p oldf f # s); f' \ same_inode_files s f''\ - \ cf2sfile (LinkHard p oldf f# s) f' = cf2sfile s f'" -apply (drule same_inode_files_prop1) -by (simp add:cf2sfile_linkhard1) - -lemma cf2sfiles_linkhard: - "valid (LinkHard p oldf f # s) \ cf2sfiles (LinkHard p oldf f # s) = (\ f'. - if (f' = f \ f' \ same_inode_files s oldf) - then (case (cf2sfile (LinkHard p oldf f # s) f) of - Some sf \ cf2sfiles s oldf \ {sf} - | _ \ {}) - else cf2sfiles s f')" -apply (frule vt_grant_os, frule vd_cons, rule ext) -apply (auto simp:cf2sfiles_def cf2sfile_linkhard1' same_inode_files_linkhard current_files_linkhard - split:if_splits option.splits dest!:current_file_has_sfile' current_has_sec' dest:same_inode_files_prop1) -done - -lemma cf2sfile_unlink': - "\valid (UnLink p f # s); f' \ same_inode_files (UnLink p f # s) f''\ - \ cf2sfile (UnLink p f # s) f' = cf2sfile s f'" -apply (drule same_inode_files_prop1) -by (simp add:cf2sfile_unlink) - -lemma cf2sfiles_unlink: - "\valid (UnLink p f # s); f' \ current_files (UnLink p f # s)\ \ cf2sfiles (UnLink p f # s) f' = ( - if (f' \ same_inode_files s f \ proc_fd_of_file s f = {} \ - (\ f'' \ same_inode_files s f. f'' \ f \ cf2sfile s f'' \ cf2sfile s f)) then - (case (cf2sfile s f) of - Some sf \ cf2sfiles s f' - {sf} - | _ \ {}) - else cf2sfiles s f')" -apply (frule vt_grant_os, frule vd_cons, simp add:current_files_simps split:if_splits) -apply (rule conjI, clarify, frule is_file_has_sfile', simp, erule exE, simp) -apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD) -apply (erule bexE, frule_tac f' = f' in same_inode_files_unlink) -apply (simp add:current_files_unlink, simp, erule conjE) -apply (erule_tac x = f'a in ballE, frule_tac f' = "f'a" in cf2sfile_unlink) -apply (simp add:current_files_unlink same_inode_files_prop1, simp) -apply (rule_tac x = f'a in bexI, simp, simp) -apply (drule_tac f = f and f' = f' and f'' = f'a in same_inode_files_prop4, simp+) -apply (erule conjE|erule exE|erule bexE)+ -apply (case_tac "f'a = f", simp) -apply (frule_tac f' = f' in same_inode_files_unlink, simp add:current_files_unlink) -apply (frule_tac f' = f'a in cf2sfile_unlink, simp add:current_files_unlink same_inode_files_prop1) -apply (rule_tac x = f'a in bexI, simp, simp) - -apply (rule impI)+ -apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD) -apply (erule bexE, frule_tac f' = f' in same_inode_files_unlink) -apply (simp add:current_files_unlink, simp, (erule conjE)+) -apply (rule_tac x = f'a in bexI, frule_tac f' = "f'a" in cf2sfile_unlink) -apply (simp add:current_files_unlink same_inode_files_prop1, simp, simp) -apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_unlink) -apply (simp add:current_files_unlink, simp) -apply (case_tac "f'a = f", simp) -apply (frule_tac f = f' and f' = f in same_inode_files_prop5, simp) -apply (erule bexE, erule conjE) -apply (rule_tac x = f'' in bexI) -apply (drule_tac f' = f'' in cf2sfile_unlink, simp add:current_files_unlink same_inode_files_prop1) -apply (simp, simp, erule same_inode_files_prop4, simp) -apply (rule_tac x = f'a in bexI) -apply (drule_tac f' = f'a in cf2sfile_unlink, simp add:current_files_unlink same_inode_files_prop1) -apply (simp, simp) - - -apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD) -apply (erule bexE, frule_tac f' = f' in same_inode_files_unlink) -apply (simp add:current_files_unlink, simp) -apply (rule_tac x = f'a in bexI) -apply (frule_tac f' = f'a in cf2sfile_unlink) -apply (simp add:same_inode_files_prop1 current_files_unlink, simp, simp) -apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_unlink) -apply (simp add:current_files_unlink, simp) -apply (rule_tac x = f'a in bexI) -apply (frule_tac f' = f'a in cf2sfile_unlink) -apply (simp add:same_inode_files_prop1 current_files_unlink, simp, simp) -done - -lemma cf2sfiles_closefd: - "\valid (CloseFd p fd # s); f' \ current_files (CloseFd p fd # s)\ \ cf2sfiles (CloseFd p fd # s) f' = ( - case (file_of_proc_fd s p fd) of - Some f \ if (f' \ same_inode_files s f \ proc_fd_of_file s f = {(p, fd)} \ f \ files_hung_by_del s \ - (\ f'' \ same_inode_files s f. f'' \ f \ cf2sfile s f'' \ cf2sfile s f)) - then (case (cf2sfile s f) of - Some sf \ cf2sfiles s f' - {sf} - | _ \ {}) - else cf2sfiles s f' - | _ \ cf2sfiles s f')" - -apply (frule vt_grant_os, frule vd_cons, case_tac "file_of_proc_fd s p fd") -apply (simp_all add:current_files_simps split:if_splits) - -apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD) -apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd) -apply (simp add:current_files_closefd, simp) -apply (rule_tac x = f'a in bexI) -apply (frule_tac f = f'a in cf2sfile_closefd) -apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp) -apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_closefd) -apply (simp add:current_files_closefd, simp) -apply (rule_tac x = f'a in bexI) -apply (frule_tac f = f'a in cf2sfile_closefd) -apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp) - -apply (rule conjI, clarify, frule file_of_pfd_is_file, simp) -apply (frule is_file_has_sfile', simp, erule exE, simp) -apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD) -apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd) -apply (simp add:current_files_closefd, simp, erule conjE) -apply (erule_tac x = f'a in ballE, frule_tac f = "f'a" in cf2sfile_closefd) -apply (simp add:current_files_closefd same_inode_files_prop1, simp) -apply (rule_tac x = f'a in bexI, simp, simp) -apply (drule_tac f = a and f' = f' and f'' = f'a in same_inode_files_prop4, simp+) -apply (erule conjE|erule exE|erule bexE)+ -apply (case_tac "f'a = a", simp) -apply (frule_tac f' = f' in same_inode_files_closefd, simp add:current_files_closefd, simp) -apply (frule_tac f = f'a in cf2sfile_closefd, simp add:current_files_closefd same_inode_files_prop1) -apply (rule_tac x = f'a in bexI, simp, simp) - -apply (rule impI)+ -apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD) -apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd) -apply (simp add:current_files_closefd, simp, (erule conjE)+) -apply (rule_tac x = f'a in bexI, frule_tac f = f'a in cf2sfile_closefd) -apply (simp add:current_files_closefd same_inode_files_prop1, simp, simp) -apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_closefd) -apply (simp add:current_files_closefd, simp) -apply (case_tac "f'a = a", simp) -apply (frule_tac f = f' and f' = a in same_inode_files_prop5, simp) -apply (erule bexE, erule conjE) -apply (rule_tac x = f'' in bexI) -apply (drule_tac f = f'' in cf2sfile_closefd, simp add:current_files_closefd same_inode_files_prop1) -apply (simp, simp, erule same_inode_files_prop4, simp) -apply (rule_tac x = f'a in bexI) -apply (drule_tac f = f'a in cf2sfile_closefd, simp add:current_files_closefd same_inode_files_prop1) -apply (simp, simp) - -apply (rule conjI, clarify) - -apply (rule impI) -apply (case_tac "a \ files_hung_by_del s", simp_all) -apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD) -apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd) -apply (simp add:current_files_closefd, simp) -apply (rule_tac x = f'a in bexI) -apply (frule_tac f = f'a in cf2sfile_closefd) -apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp) -apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_closefd) -apply (simp add:current_files_closefd, simp) -apply (rule_tac x = f'a in bexI) -apply (frule_tac f = f'a in cf2sfile_closefd) -apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp) -apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD) -apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd) -apply (simp add:current_files_closefd, simp) -apply (rule_tac x = f'a in bexI) -apply (frule_tac f = f'a in cf2sfile_closefd) -apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp) -apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_closefd) -apply (simp add:current_files_closefd, simp) -apply (rule_tac x = f'a in bexI) -apply (frule_tac f = f'a in cf2sfile_closefd) -apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp) -done - -lemmas cf2sfiles_simps = cf2sfiles_open cf2sfiles_linkhard cf2sfiles_other - cf2sfiles_unlink cf2sfiles_closefd - - (* simpset for co2sobj *) lemma co2sobj_execve: "\valid (Execve p f fds # s); alive (Execve p f fds # s) obj\ \ co2sobj (Execve p f fds # s) obj = ( if (obj = O_proc p) then (case (cp2sproc (Execve p f fds # s) p) of - Some sp \ Some (S_proc sp (O_proc p \ Tainted s \ O_file f \ Tainted s)) + Some sp \ Some (S_proc sp (O_proc p \ tainted s \ O_file f \ tainted s)) | _ \ None) else co2sobj s obj )" apply (frule vt_grant_os, frule vd_cons, case_tac obj) -apply (simp_all add:current_files_simps cf2sfiles_other ch2sshm_other cq2smsgq_other tainted_eq_Tainted) +apply (simp_all add:current_files_simps cq2smsgq_other cf2sfile_other) apply (case_tac "cp2sproc (Execve p f fds # s) p") apply (drule current_proc_has_sp', simp, simp) -apply (simp (no_asm_simp) add:cp2sproc_execve tainted_eq_Tainted split:option.splits) +apply (simp (no_asm_simp) add:cp2sproc_execve split:option.splits) +apply (simp add:is_file_simps, frule_tac s = s in is_file_has_sfile', simp, erule exE, simp) +apply (frule_tac ff = list in cf2sfile_other', simp_all) +apply (simp add:is_file_in_current) apply (simp add:is_dir_simps, frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp) apply (frule_tac ff = list in cf2sfile_other', simp_all) apply (simp add:is_dir_in_current) @@ -1851,60 +1276,66 @@ "\valid (Execve p f fds # s); alive s obj\ \ co2sobj (Execve p f fds # s) obj = ( if (obj = O_proc p) then (case (cp2sproc (Execve p f fds # s) p) of - Some sp \ Some (S_proc sp (O_proc p \ Tainted s \ O_file f \ Tainted s)) + Some sp \ Some (S_proc sp (O_proc p \ tainted s \ O_file f \ tainted s)) | _ \ None) else co2sobj s obj )" apply (frule vt_grant_os, frule vd_cons, case_tac obj) -apply (simp_all add:current_files_simps cf2sfiles_other ch2sshm_other cq2smsgq_other tainted_eq_Tainted) +apply (simp_all add:current_files_simps cf2sfile_other cq2smsgq_other) apply (case_tac "cp2sproc (Execve p f fds # s) p") apply (drule current_proc_has_sp', simp, simp) -apply (simp (no_asm_simp) add:cp2sproc_execve tainted_eq_Tainted split:option.splits) +apply (simp (no_asm_simp) add:cp2sproc_execve split:option.splits) +apply (frule_tac s = s in is_file_has_sfile', simp, erule exE, simp) +apply (frule_tac ff = list in cf2sfile_other', simp_all) +apply (simp add:is_file_in_current) apply (frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp) apply (frule_tac ff = list in cf2sfile_other', simp_all) apply (simp add:is_dir_in_current) done lemma co2sobj_clone': - "\valid (Clone p p' fds shms # s); alive s obj\ \ co2sobj (Clone p p' fds shms # s) obj = ( + "\valid (Clone p p' fds # s); alive s obj\ \ co2sobj (Clone p p' fds # s) obj = ( if (obj = O_proc p') - then (case (cp2sproc (Clone p p' fds shms # s) p') of - Some sp \ Some (S_proc sp (O_proc p \ Tainted s)) + then (case (cp2sproc (Clone p p' fds # s) p') of + Some sp \ Some (S_proc sp (O_proc p \ tainted s)) | _ \ None) else co2sobj s obj )" apply (frule vt_grant_os, frule vd_cons, case_tac obj) -apply (simp_all add:current_files_simps cf2sfiles_other ch2sshm_other cq2smsgq_other tainted_eq_Tainted) -apply (case_tac "cp2sproc (Clone p p' fds shms # s) p'") +apply (simp_all add:current_files_simps cf2sfile_other cq2smsgq_other ) +apply (case_tac "cp2sproc (Clone p p' fds # s) p'") apply (drule current_proc_has_sp', simp, simp) apply ((erule conjE)+, frule_tac p = p in current_proc_has_sec, simp, erule exE, simp) -apply (rule conjI, rule impI, simp) -apply (simp (no_asm_simp) add:cp2sproc_clone tainted_eq_Tainted split:option.splits) - +apply (simp (no_asm_simp) add:cp2sproc_clone split:option.splits) +apply (case_tac "nat = p'", simp, simp) +apply (frule_tac s = s in is_file_has_sfile', simp, erule exE, simp) +apply (frule_tac ff = list in cf2sfile_other', simp_all) +apply (simp add:is_file_in_current) apply (frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp) apply (frule_tac ff = list in cf2sfile_other', simp_all) apply (simp add:is_dir_in_current) done lemma co2sobj_clone: - "\valid (Clone p p' fds shms # s); alive (Clone p p' fds shms # s) obj\ - \ co2sobj (Clone p p' fds shms # s) obj = ( + "\valid (Clone p p' fds # s); alive (Clone p p' fds # s) obj\ + \ co2sobj (Clone p p' fds # s) obj = ( if (obj = O_proc p') - then (case (cp2sproc (Clone p p' fds shms # s) p') of - Some sp \ Some (S_proc sp (O_proc p \ Tainted s)) + then (case (cp2sproc (Clone p p' fds # s) p') of + Some sp \ Some (S_proc sp (O_proc p \ tainted s)) | _ \ None) else co2sobj s obj )" apply (frule vt_grant_os, frule vd_cons, case_tac obj) -apply (simp_all add:current_files_simps cf2sfiles_other ch2sshm_other - cq2smsgq_other tainted_eq_Tainted) +apply (simp_all add:current_files_simps cf2sfile_other cq2smsgq_other) apply (rule conjI, rule impI, simp) -apply (case_tac "cp2sproc (Clone p p' fds shms # s) p'") +apply (case_tac "cp2sproc (Clone p p' fds # s) p'") apply (drule current_proc_has_sp', simp, simp) apply ((erule conjE)+, frule_tac p = p in current_proc_has_sec, simp, erule exE, simp) -apply (simp add:tainted_eq_Tainted, rule impI, rule notI) -apply (drule Tainted_in_current, simp+) +apply (rule impI,rule notI, drule tainted_in_current, simp+) apply (rule impI, simp) apply (drule current_proc_has_sp, simp, (erule exE|erule conjE)+) -apply (simp (no_asm_simp) add:cp2sproc_clone tainted_eq_Tainted Tainted_in_current split:option.splits) +apply (simp (no_asm_simp) add:cp2sproc_clone tainted_in_current split:option.splits) +apply (simp add:is_file_simps, frule_tac s = s in is_file_has_sfile', simp, erule exE, simp) +apply (frule_tac ff = list in cf2sfile_other', simp_all) +apply (simp add:is_file_in_current) apply (simp add:is_dir_simps, frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp) apply (frule_tac ff = list in cf2sfile_other', simp_all) apply (simp add:is_dir_in_current) @@ -1913,22 +1344,25 @@ lemma co2sobj_ptrace: "\valid (Ptrace p p' # s); alive s obj\\ co2sobj (Ptrace p p' # s) obj = ( case obj of - O_proc p'' \ if (info_flow_shm s p' p'') + O_proc p'' \ if (p'' = p') then (case (cp2sproc s p'') of - Some sp \ Some (S_proc sp (O_proc p'' \ Tainted s \ O_proc p \ Tainted s)) + Some sp \ Some (S_proc sp (O_proc p'' \ tainted s \ O_proc p \ tainted s)) | _ \ None) - else if (info_flow_shm s p p'') + else if (p'' = p) then (case (cp2sproc s p'') of - Some sp \ Some (S_proc sp (O_proc p'' \ Tainted s \ O_proc p' \ Tainted s)) + Some sp \ Some (S_proc sp (O_proc p'' \ tainted s \ O_proc p' \ tainted s)) | _ \ None) else co2sobj s (O_proc p'') | _ \ co2sobj s obj)" apply (frule vt_grant_os, frule vd_cons, case_tac obj) -apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other cf2sfiles_other tainted_eq_Tainted) +apply (simp_all add:current_files_simps cq2smsgq_other cf2sfile_other) -apply (auto simp:cp2sproc_other tainted_eq_Tainted split:option.splits - dest!:current_proc_has_sec' current_proc_has_sp' intro:info_flow_shm_Tainted)[1] +apply (auto simp:cp2sproc_other split:option.splits + dest!:current_proc_has_sec' current_proc_has_sp')[1] +apply (frule_tac s = s in is_file_has_sfile', simp, erule exE, simp) +apply (frule_tac ff = list in cf2sfile_other', simp_all) +apply (simp add:is_file_in_current) apply (frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp) apply (frule_tac ff = list in cf2sfile_other', simp_all) apply (simp add:is_dir_in_current) @@ -1939,29 +1373,27 @@ \ co2sobj (Open p f flag fd opt # s) obj = (case obj of O_file f' \ if (f' = f \ opt \ None) then (case (cf2sfile (Open p f flag fd opt # s) f) of - Some sf \ Some (S_file {sf} (O_proc p \ Tainted s)) + Some sf \ Some (S_file sf (O_proc p \ tainted s)) | _ \ None) else co2sobj s (O_file f') | O_proc p' \ if (p' = p) then (case (cp2sproc (Open p f flag fd opt # s) p) of - Some sp \ Some (S_proc sp (O_proc p \ Tainted s)) + Some sp \ Some (S_proc sp (O_proc p \ tainted s)) | _ \ None) else co2sobj s (O_proc p') | _ \ co2sobj s obj )" apply (frule vt_grant_os, frule vd_cons, case_tac obj) -apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits - dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1] +apply (auto simp:cp2sproc_simps split:option.splits dest!:current_proc_has_sp')[1] apply (simp split:if_splits t_object.splits) apply (rule conjI, rule impI, erule conjE, erule exE, simp, (erule exE|erule conjE)+) apply (case_tac "cf2sfile (Open p f flag fd (Some y) # s) f") apply (drule current_file_has_sfile', simp, simp add:current_files_simps, simp) -apply (frule_tac f' = f in cf2sfiles_open, simp add:current_files_simps) -apply (simp add:tainted_eq_Tainted) -apply (rule impI, rule notI, drule Tainted_in_current, simp, simp add:is_file_in_current) -apply (rule impI, simp add:tainted_eq_Tainted cf2sfiles_open is_file_in_current split:option.splits) +apply (frule_tac f' = f in cf2sfile_open, simp add:current_files_simps) +apply (rule impI, rule notI, drule tainted_in_current, simp, simp add:is_file_in_current) +apply (rule impI, simp add:cf2sfile_open is_file_in_current split:option.splits) -apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) +apply (simp_all add:current_files_simps is_dir_simps cq2smsgq_other) apply (frule is_dir_in_current) apply (frule_tac f' = list in cf2sfile_open) @@ -1973,7 +1405,7 @@ "\valid (ReadFile p fd # s); alive s obj\ \ co2sobj (ReadFile p fd # s) obj = ( case obj of O_proc p' \ (case (file_of_proc_fd s p fd) of - Some f \ (if (info_flow_shm s p p' \ O_file f \ Tainted s) + Some f \ (if (p' = p \ O_file f \ tainted s) then (case (cp2sproc s p') of Some sp \ Some (S_proc sp True) | _ \ None) @@ -1981,12 +1413,11 @@ | _ \ None) | _ \ co2sobj s obj)" apply (frule vt_grant_os, frule vd_cons, case_tac obj) -apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits - dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1] -apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) +apply (auto simp:cp2sproc_simps split:option.splits dest!:current_proc_has_sp')[1] +apply (simp_all add:current_files_simps is_dir_simps cq2smsgq_other) apply (auto split:if_splits option.splits dest!:current_file_has_sfile' - simp:current_files_simps cf2sfiles_simps cf2sfile_simps + simp:current_files_simps cf2sfile_simps dest:is_file_in_current is_dir_in_current) done @@ -1994,54 +1425,43 @@ "\valid (WriteFile p fd # s); alive s obj\ \ co2sobj (WriteFile p fd # s) obj = ( case obj of O_file f' \ (case (file_of_proc_fd s p fd) of - Some f \ (if (f \ same_inode_files s f') - then Some (S_file (cf2sfiles s f') - (O_file f' \ Tainted s \ O_proc p \ Tainted s)) + Some f \ (if (f' = f) + then (case cf2sfile s f of + Some sf \ Some (S_file sf (O_file f \ tainted s \ O_proc p \ tainted s)) + | _ \ None) else co2sobj s obj) | _ \ None) | _ \ co2sobj s obj)" apply (frule vt_grant_os, frule vd_cons, case_tac obj) -apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) +apply (simp_all add:current_files_simps is_dir_simps cq2smsgq_other) apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp' - simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted - same_inode_files_prop6 + simp:current_files_simps cf2sfile_simps cp2sproc_simps dest:is_file_in_current is_dir_in_current) - -(* should delete has_same_inode !?!?*) -by (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits option.splits) +done lemma co2sobj_closefd: "\valid (CloseFd p fd # s); alive (CloseFd p fd # s) obj\ \ co2sobj (CloseFd p fd # s) obj = ( case obj of - O_file f' \ (case (file_of_proc_fd s p fd) of - Some f \ (if (f' \ same_inode_files s f \ proc_fd_of_file s f = {(p, fd)} \ - f \ files_hung_by_del s \ (\ f'' \ same_inode_files s f. - f'' \ f \ cf2sfile s f'' \ cf2sfile s f)) - then (case (cf2sfile s f, co2sobj s (O_file f')) of - (Some sf, Some (S_file sfs b)) \ Some (S_file (sfs - {sf}) b) - | _ \ None) - else co2sobj s obj) - | _ \ co2sobj s obj) - | O_proc p' \ (if (p = p') + O_proc p' \ (if (p = p') then (case (cp2sproc (CloseFd p fd # s) p) of - Some sp \ Some (S_proc sp (O_proc p \ Tainted s)) + Some sp \ Some (S_proc sp (O_proc p \ tainted s)) | _ \ None) else co2sobj s obj) | _ \ co2sobj s obj) " apply (frule vt_grant_os, frule vd_cons, case_tac obj) -apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) -apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits - dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1] +apply (simp_all add:current_files_simps cq2smsgq_other) +apply (auto simp:cp2sproc_simps split:option.splits if_splits dest!:current_proc_has_sp')[1] apply (frule is_file_in_current) apply (case_tac "file_of_proc_fd s p fd") -apply (simp add:tainted_eq_Tainted) -apply (drule_tac f' = list in cf2sfiles_closefd, simp add:current_files_closefd, simp) -apply (frule_tac f' = list in cf2sfiles_closefd, simp) -apply (simp add:is_file_simps current_files_simps) -apply (auto simp add:tainted_eq_Tainted cf2sfile_closefd split:if_splits option.splits - dest!:current_file_has_sfile' dest:hung_file_in_current)[1] +apply (simp add:current_files_simps is_file_simps tainted.simps) +apply (drule_tac f = list in cf2sfile_closefd, simp add:current_files_simps) +apply (simp split:option.splits) +apply (frule_tac f = list in cf2sfile_closefd, simp) +apply (simp split:option.splits) +apply (simp add:is_file_simps current_files_simps split:if_splits) +apply (rule impI, simp) apply (simp add:is_dir_simps, frule is_dir_in_current) apply (frule_tac f = list in cf2sfile_closefd) @@ -2050,25 +1470,14 @@ done lemma co2sobj_unlink: - "\valid (UnLink p f # s); alive (UnLink p f # s) obj\ \ co2sobj (UnLink p f # s) obj = ( - case obj of - O_file f' \ if (f' \ same_inode_files s f \ proc_fd_of_file s f = {} \ - (\ f'' \ same_inode_files s f. f'' \ f \ cf2sfile s f'' \ cf2sfile s f)) - then (case (cf2sfile s f, co2sobj s (O_file f')) of - (Some sf, Some (S_file sfs b)) \ Some (S_file (sfs - {sf}) b) - | _ \ None) - else co2sobj s obj - | _ \ co2sobj s obj)" + "\valid (UnLink p f # s); alive (UnLink p f # s) obj\ + \ co2sobj (UnLink p f # s) obj = co2sobj s obj" apply (frule vt_grant_os, frule vd_cons, case_tac obj) -apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) -apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits - dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1] +apply (simp_all add:current_files_simps cq2smsgq_other) +apply (auto simp:cp2sproc_simps split:option.splits if_splits dest!:current_proc_has_sp')[1] apply (frule is_file_in_current) apply (frule_tac f' = list in cf2sfile_unlink, simp) -apply (frule_tac f' = list in cf2sfiles_unlink, simp) -apply (simp add:is_file_simps current_files_simps) -apply (auto simp add:tainted_eq_Tainted is_file_in_current split:if_splits option.splits - dest!:current_file_has_sfile')[1] +apply (simp add:is_file_simps current_files_simps split:option.splits if_splits) apply (simp add:is_dir_simps, frule is_dir_in_current) apply (frule_tac f' = list in cf2sfile_unlink) @@ -2079,13 +1488,13 @@ lemma co2sobj_rmdir: "\valid (Rmdir p f # s); alive (Rmdir p f # s) obj\ \ co2sobj (Rmdir p f # s) obj = co2sobj s obj" apply (frule vt_grant_os, frule vd_cons, case_tac obj) -apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) -apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits - dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1] +apply (simp_all add:current_files_simps cq2smsgq_other) +apply (auto simp:cp2sproc_simps split:option.splits if_splits dest!:current_proc_has_sp')[1] apply (simp add:is_file_simps dir_is_empty_def) apply (case_tac "f = list", drule file_dir_conflict, simp, simp) -apply (simp add:cf2sfiles_other) -apply (auto simp:cf2sfile_simps dest:is_dir_in_current) +apply (frule_tac f' = list in cf2sfile_rmdir, simp add:is_file_in_current current_files_simps) +apply (simp split:option.splits) +apply (auto simp:cf2sfile_simps cf2sfile_other dest:is_dir_in_current) done lemma co2sobj_mkdir: @@ -2096,75 +1505,50 @@ | _ \ None) else co2sobj s obj)" apply (frule vt_grant_os, frule vd_cons, case_tac obj) -apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) -apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits - dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1] -apply (frule_tac cf2sfiles_other, simp+) +apply (simp_all add:current_files_simps cq2smsgq_other) +apply (auto simp:cp2sproc_simps split:option.splits if_splits dest!:current_proc_has_sp')[1] +apply (case_tac "f = list", simp add:is_file_simps is_file_in_current) +apply (frule_tac f' = list in cf2sfile_mkdir) +apply (simp add:is_file_in_current) +apply (simp split:option.splits) + apply (frule is_dir_in_current, rule impI, simp add:current_files_mkdir) apply (frule current_file_has_sfile, simp, erule exE, simp) apply (drule cf2sfile_mkdir1, simp+) done - -lemma co2sobj_linkhard: - "\valid (LinkHard p oldf f # s); alive (LinkHard p oldf f # s) obj\ - \ co2sobj (LinkHard p oldf f # s) obj = ( - case obj of - O_file f' \ if (f' = f \ f' \ same_inode_files s oldf) - then (case (cf2sfile (LinkHard p oldf f # s) f) of - Some sf \ Some (S_file (cf2sfiles s oldf \ {sf}) (O_file oldf \ Tainted s)) - | _ \ None) - else co2sobj s obj - | _ \ co2sobj s obj)" -apply (frule vt_grant_os, frule vd_cons, case_tac obj) -apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) -apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits - dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1] -apply (frule_tac cf2sfiles_linkhard, simp+) -apply (frule_tac f' = f in cf2sfile_linkhard, simp add:current_files_linkhard) -apply (auto simp:is_file_simps sectxt_of_obj_simps current_files_simps is_file_in_current same_inodes_Tainted - split:option.splits if_splits dest:Tainted_in_current - dest!:current_has_sec' current_file_has_sfile')[1] - -apply (frule is_dir_in_current, simp add:current_files_linkhard is_dir_simps is_dir_in_current) -apply (frule is_dir_in_current) -apply (frule current_file_has_sfile, simp) -apply (drule cf2sfile_linkhard1, simp+) -done - lemma co2sobj_truncate: "\valid (Truncate p f len # s); alive s obj\ \ co2sobj (Truncate p f len # s) obj = ( case obj of - O_file f' \ if (f' \ same_inode_files s f \ len > 0) - then Some (S_file (cf2sfiles s f') (O_file f' \ Tainted s \ O_proc p \ Tainted s)) + O_file f' \ if (f' = f \ len > 0) + then (case cf2sfile s f of + Some sf \ Some (S_file sf (O_file f' \ tainted s \ O_proc p \ tainted s)) + | _ \ None) else co2sobj s obj | _ \ co2sobj s obj)" apply (frule vt_grant_os, frule vd_cons, case_tac obj) -apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) +apply (simp_all add:current_files_simps is_dir_simps cq2smsgq_other) apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp' - simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted - same_inode_files_prop6 + simp:current_files_simps cf2sfile_simps cp2sproc_simps dest:is_file_in_current is_dir_in_current) done lemma co2sobj_kill: "\valid (Kill p p' # s); alive (Kill p p' # s) obj\ \ co2sobj (Kill p p' # s) obj = co2sobj s obj" apply (frule vt_grant_os, frule vd_cons, case_tac obj) -apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) +apply (simp_all add:current_files_simps is_dir_simps cq2smsgq_other) apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp' - simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted - same_inode_files_prop6 + simp:current_files_simps cf2sfile_simps cp2sproc_simps dest:is_file_in_current is_dir_in_current) done lemma co2sobj_exit: "\valid (Exit p # s); alive (Exit p # s) obj\ \ co2sobj (Exit p # s) obj = co2sobj s obj" apply (frule vt_grant_os, frule vd_cons, case_tac obj) -apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) +apply (simp_all add:current_files_simps is_dir_simps cq2smsgq_other ) apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp' - simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted - same_inode_files_prop6 + simp:current_files_simps cf2sfile_simps cp2sproc_simps dest:is_file_in_current is_dir_in_current) done @@ -2177,10 +1561,9 @@ else co2sobj s obj | _ \ co2sobj s obj)" apply (frule vt_grant_os, frule vd_cons, case_tac obj) -apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) +apply (simp_all add:current_files_simps is_dir_simps cq2smsgq_other ) apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp' - simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted - same_inode_files_prop6 + simp:current_files_simps cf2sfile_simps cp2sproc_simps dest!:current_has_smsgq' dest:is_file_in_current is_dir_in_current cq2smsg_createmsgq) done @@ -2194,10 +1577,9 @@ else co2sobj s obj | _ \ co2sobj s obj)" apply (frule vt_grant_os, frule vd_cons, case_tac obj) -apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) +apply (simp_all add:current_files_simps is_dir_simps cq2smsgq_other ) apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp' - simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted - same_inode_files_prop6 + simp:current_files_simps cf2sfile_simps cp2sproc_simps dest!:current_has_smsgq' dest:is_file_in_current is_dir_in_current cq2smsg_sendmsg) done @@ -2209,17 +1591,16 @@ Some sq \ Some (S_msgq sq) | _ \ None) else co2sobj s obj - | O_proc p' \ if (info_flow_shm s p p' \ O_msg q m \ Tainted s) + | O_proc p' \ if (p' = p \ O_msg q m \ tainted s) then (case (cp2sproc s p') of Some sp \ Some (S_proc sp True) | _ \ None) else co2sobj s obj | _ \ co2sobj s obj)" apply (frule vt_grant_os, frule vd_cons, case_tac obj) -apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) +apply (simp_all add:current_files_simps is_dir_simps cq2smsgq_other) apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp' - simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted - same_inode_files_prop6 + simp:current_files_simps cf2sfile_simps cp2sproc_simps dest!:current_has_smsgq' dest:is_file_in_current is_dir_in_current cq2smsg_recvmsg) done @@ -2228,118 +1609,20 @@ "\valid (RemoveMsgq p q # s); alive (RemoveMsgq p q # s) obj\ \ co2sobj (RemoveMsgq p q # s) obj = co2sobj s obj" apply (frule vt_grant_os, frule vd_cons, case_tac obj) -apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) +apply (simp_all add:current_files_simps is_dir_simps cq2smsgq_other) apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp' - simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted - same_inode_files_prop6 + simp:current_files_simps cf2sfile_simps cp2sproc_simps dest!:current_has_smsgq' dest:is_file_in_current is_dir_in_current cq2smsg_removemsgq) done -lemma co2sobj_createshm: - "\valid (CreateShM p h # s); alive (CreateShM p h # s) obj\ \ co2sobj (CreateShM p h # s) obj = ( - case obj of - O_shm h' \ if (h' = h) then (case (ch2sshm (CreateShM p h # s) h) of - Some sh \ Some (S_shm sh) - | _ \ None) - else co2sobj s obj - | _ \ co2sobj s obj)" -apply (frule vt_grant_os, frule vd_cons, case_tac obj) -apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) -apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp' - simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted - same_inode_files_prop6 ch2sshm_simps - dest!:current_shm_has_sh' - dest:is_file_in_current is_dir_in_current) -done - -lemma co2sobj_detach: - "\valid (Detach p h # s); alive s obj\ \ co2sobj (Detach p h # s) obj = ( - case obj of - O_proc p' \ if (p' = p) then (case (cp2sproc (Detach p h # s) p) of - Some sp \ Some (S_proc sp (O_proc p \ Tainted s)) - | _ \ None) - else co2sobj s obj - | _ \ co2sobj s obj)" -apply (frule vt_grant_os, frule vd_cons, case_tac obj) -apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) - -apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp' - simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted - same_inode_files_prop6 ch2sshm_simps - dest!:current_shm_has_sh' - dest:is_file_in_current is_dir_in_current) -done - -lemma co2sobj_deleteshm: - "\valid (DeleteShM p h # s); alive (DeleteShM p h # s) obj\ \ co2sobj (DeleteShM p h # s) obj = ( - case obj of - O_proc p' \ (case (cp2sproc (DeleteShM p h # s) p') of - Some sp \ Some (S_proc sp (O_proc p' \ Tainted s)) - | _ \ None) - | _ \ co2sobj s obj)" -apply (frule vt_grant_os, frule vd_cons, case_tac obj) -apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) - -apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp' - simp:current_files_simps cf2sfiles_simps cf2sfile_simps tainted_eq_Tainted - same_inode_files_prop6 ch2sshm_simps - dest!:current_shm_has_sh' - dest:is_file_in_current is_dir_in_current) -done declare Product_Type.split_paired_Ex Product_Type.split_paired_All [simp del] -lemma info_flow_shm_prop1: - "p \ current_procs s \ info_flow_shm s p p" -by (simp add:info_flow_shm_def) - -lemma co2sobj_attach: - "\valid (Attach p h flag # s); alive s obj\ \ co2sobj (Attach p h flag # s) obj = ( - case obj of - O_proc p' \ if (info_flow_shm s p p') - then (case (cp2sproc (Attach p h flag # s) p') of - Some sp \ Some (S_proc sp (O_proc p' \ Tainted s \ - (\ p''. O_proc p'' \ Tainted s \ (p'', SHM_RDWR) \ procs_of_shm s h))) - | _ \ None) - else if (\ p'' flag'. (p'', flag') \ procs_of_shm s h \ flag = SHM_RDWR \ O_proc p \ Tainted s \ - info_flow_shm s p'' p') - then (case (cp2sproc s p') of - Some sp \ Some (S_proc sp True) - | _ \ None) - else co2sobj s obj - | _ \ co2sobj s obj)" -apply (frule vt_grant_os, frule vd_cons, case_tac obj) -apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) - -apply (rule conjI|rule impI|erule exE)+ -apply (simp split:option.splits del:split_paired_Ex) -apply (rule impI, frule current_proc_has_sp, simp) -apply ((erule exE)+, auto simp:tainted_eq_Tainted intro:info_flow_shm_Tainted)[1] -apply (rule impI, simp add:tainted_eq_Tainted split:option.splits del:split_paired_Ex) -apply (auto simp:info_flow_shm_prop1 cp2sproc_attach dest!:current_proc_has_sp')[1] - -apply (case_tac "cp2sproc (Attach p h flag # s) nat") -apply (drule current_proc_has_sp', simp+) - -apply (rule conjI|erule exE|erule conjE|rule impI)+ -apply (simp add:tainted_eq_Tainted) -apply (auto simp:info_flow_shm_prop1 cp2sproc_attach intro:info_flow_shm_Tainted dest!:current_proc_has_sp')[1] -apply (auto simp:info_flow_shm_prop1 cp2sproc_attach tainted_eq_Tainted intro:info_flow_shm_Tainted dest!:current_proc_has_sp' -split:option.splits if_splits)[1] - - -apply (auto split:if_splits option.splits dest!:current_file_has_sfile' - simp:current_files_simps cf2sfiles_simps cf2sfile_simps tainted_eq_Tainted - same_inode_files_prop6 - dest:is_file_in_current is_dir_in_current) -done - - lemma co2sobj_other: "\valid (e # s); alive (e # s) obj; \ p f fds. e \ Execve p f fds; - \ p p' fds shms. e \ Clone p p' fds shms; + \ p p' fds. e \ Clone p p' fds; \ p p'. e \ Ptrace p p'; \ p f flags fd opt. e \ Open p f flags fd opt; \ p fd. e \ ReadFile p fd; @@ -2348,27 +1631,20 @@ \ p f. e \ UnLink p f; \ p f. e \ Rmdir p f; \ p f i. e \ Mkdir p f i; - \ p f f'. e \ LinkHard p f f'; \ p f len. e \ Truncate p f len; \ p q. e \ CreateMsgq p q; \ p q m. e \ SendMsg p q m; \ p q m. e \ RecvMsg p q m; - \ p q. e \ RemoveMsgq p q; - \ p h. e \ CreateShM p h; - \ p h flag. e \ Attach p h flag; - \ p h. e \ Detach p h; - \ p h. e \ DeleteShM p h - \ \ co2sobj (e # s) obj = co2sobj s obj" + \ p q. e \ RemoveMsgq p q\ + \ co2sobj (e # s) obj = co2sobj s obj" apply (frule vt_grant, case_tac e) apply (auto intro:co2sobj_kill co2sobj_exit) done lemmas co2sobj_simps = co2sobj_execve co2sobj_clone co2sobj_ptrace co2sobj_open co2sobj_readfile - co2sobj_writefile co2sobj_closefd co2sobj_unlink co2sobj_rmdir co2sobj_mkdir co2sobj_linkhard + co2sobj_writefile co2sobj_closefd co2sobj_unlink co2sobj_rmdir co2sobj_mkdir co2sobj_truncate co2sobj_kill co2sobj_exit co2sobj_createmsgq co2sobj_sendmsg co2sobj_recvmsg - co2sobj_removemsgq co2sobj_attach co2sobj_detach co2sobj_createshm co2sobj_deleteshm - - + co2sobj_removemsgq end diff -r 271e9818b6f6 -r 99af1986e1e0 simple_selinux/Current_prop.thy --- a/simple_selinux/Current_prop.thy Mon Dec 02 10:52:40 2013 +0800 +++ b/simple_selinux/Current_prop.thy Tue Dec 03 22:42:48 2013 +0800 @@ -6,43 +6,6 @@ context flask begin -lemma procs_of_shm_prop1: "\ p_flag \ procs_of_shm s h; valid s\ \ h \ current_shms s" -apply (induct s arbitrary:p_flag) -apply (case_tac p_flag, simp, drule init_procs_has_shm, simp) -apply (frule vd_cons, frule vt_grant_os) -apply (case_tac a, auto split:if_splits option.splits) -done - -lemma procs_of_shm_prop2: "\(p, flag) \ procs_of_shm s h; valid s\ \ p \ current_procs s" -apply (induct s arbitrary:p flag) -apply (simp, drule init_procs_has_shm, simp) -apply (frule vd_cons, frule vt_grant_os) -apply (case_tac a, auto split:if_splits option.splits) -done - -lemma procs_of_shm_prop2': - "\p \ current_procs s; valid s\ \ \ flag h. (p, flag) \ procs_of_shm s h" -by (auto dest:procs_of_shm_prop2) - -lemma procs_of_shm_prop3: "\(p, flag) \ procs_of_shm s h; (p, flag') \ procs_of_shm s h; valid s\ - \ flag = flag'" -apply (induct s arbitrary:p flag flag') -apply (simp, drule_tac flag = flag in init_procs_has_shm, drule_tac flag = flag' in init_procs_has_shm, simp) -apply (frule vd_cons, frule vt_grant_os) -apply (case_tac a, auto split:if_splits option.splits dest:procs_of_shm_prop2) -done - -lemma procs_of_shm_prop4: "\(p, flag) \ procs_of_shm s h; valid s\ \ flag_of_proc_shm s p h = Some flag" -apply (induct s arbitrary:p flag) -apply (simp, drule init_procs_has_shm, simp) -apply (frule vd_cons, frule vt_grant_os) -apply (case_tac a, auto split:if_splits option.splits dest:procs_of_shm_prop2) -done - -lemma procs_of_shm_prop4': - "\flag_of_proc_shm s p h = None; valid s\ \ \ flag. (p, flag) \ procs_of_shm s h" -by (auto dest:procs_of_shm_prop4) - lemma not_init_intro_proc: "\p \ current_procs s; valid s\ \ deleted (O_proc p) s \ p \ init_procs" using not_deleted_init_proc by auto @@ -51,47 +14,6 @@ "\p \ current_procs s; valid s\ \ \ (\ deleted (O_proc p) s \ p \ init_procs)" using not_deleted_init_proc by auto -lemma info_shm_flow_in_procs: - "\info_flow_shm s p p'; valid s\ \ p \ current_procs s \ p' \ current_procs s" -by (auto intro:procs_of_shm_prop2 simp:info_flow_shm_def one_flow_shm_def) - -lemma flag_of_proc_shm_prop1: - "\flag_of_proc_shm s p h = Some flag; valid s\ \ (p, flag) \ procs_of_shm s h" -apply (induct s arbitrary:p flag) -apply (simp, drule init_shmflag_has_proc, simp) -apply (frule vd_cons, frule vt_grant_os) -apply (case_tac a, auto split:if_splits option.splits dest:procs_of_shm_prop2) -done - - - -lemma has_same_inode_in_current: - "\has_same_inode s f f'; valid s\ \ f \ current_files s \ f' \ current_files s" -by (auto simp add:has_same_inode_def current_files_def same_inode_files_def - is_file_def split:if_splits option.splits) - - -lemma has_same_inode_prop1: - "\has_same_inode s f f'; is_file s f; valid s\ \ is_file s f'" -by (auto simp:has_same_inode_def same_inode_files_def is_file_def) - -lemma has_same_inode_prop1': - "\has_same_inode s f f'; is_file s f'; valid s\ \ is_file s f" -by (auto simp:has_same_inode_def is_file_def same_inode_files_def - split:if_splits option.splits) - -lemma has_same_inode_prop2: - "\has_same_inode s f f'; file_of_proc_fd s p fd = Some f; valid s\ \ is_file s f'" -apply (drule has_same_inode_prop1) -apply (simp add:file_of_pfd_is_file, simp+) -done - -lemma has_same_inode_prop2': - "\has_same_inode s f f'; file_of_proc_fd s p fd = Some f'; valid s\ \ is_file s f" -apply (drule has_same_inode_prop1') -apply (simp add:file_of_pfd_is_file, simp+) -done - lemma tobj_in_init_alive: "tobj_in_init obj \ init_alive obj" by (case_tac obj, auto) diff -r 271e9818b6f6 -r 99af1986e1e0 simple_selinux/Delete_prop.thy --- a/simple_selinux/Delete_prop.thy Mon Dec 02 10:52:40 2013 +0800 +++ b/simple_selinux/Delete_prop.thy Tue Dec 03 22:42:48 2013 +0800 @@ -106,11 +106,6 @@ \ \ deleted (O_proc p) s" by (auto dest:not_deleted_init_udp_aux) -lemma not_deleted_init_shm: - "\\ deleted (O_shm h) s; h \ init_shms\ \ h \ current_shms s" -apply (induct s, simp) -by (case_tac a, auto) - lemma not_deleted_init_msgq: "\\ deleted (O_msgq q) s; q \ init_msgqs\ \ q \ current_msgqs s" apply (induct s, simp) @@ -136,7 +131,7 @@ "\\ deleted obj s; valid s; init_alive obj\ \ alive s obj" apply (case_tac obj) apply (auto dest!:not_deleted_init_msg not_deleted_init_file not_deleted_init_dir not_deleted_init_proc - not_deleted_init_fd1 not_deleted_init_tcp1 not_deleted_init_udp1 not_deleted_init_shm + not_deleted_init_fd1 not_deleted_init_tcp1 not_deleted_init_udp1 not_deleted_init_msgq intro:is_file_in_current is_dir_in_current is_tcp_in_current is_udp_in_current current_msg_imp_current_msgq) @@ -189,11 +184,6 @@ by (auto simp:is_udp_sock_simps split:option.splits t_socket_type.splits dest:is_udp_sock_imp_curernt_proc) -lemma not_deleted_cur_shm_app: - "\\ deleted (O_shm h) (s' @ s); h \ current_shms s\ \ h \ current_shms (s' @ s)" -apply (induct s', simp, simp add:cons_app_simp_aux) -by (case_tac a, auto) - lemma not_deleted_cur_msgq_app: "\\ deleted (O_msgq q) (s' @ s); q \ current_msgqs s\ \ q \ current_msgqs (s' @ s)" apply (induct s', simp, simp add:cons_app_simp_aux) @@ -213,7 +203,7 @@ apply (case_tac obj) apply (auto dest!:not_deleted_cur_msg_app not_deleted_cur_file_app not_deleted_cur_dir_app not_deleted_cur_proc_app not_deleted_cur_fd_app not_deleted_cur_tcp_app - not_deleted_cur_udp_app not_deleted_cur_shm_app not_deleted_cur_msgq_app + not_deleted_cur_udp_app not_deleted_cur_msgq_app intro:is_file_in_current is_dir_in_current is_tcp_in_current is_udp_in_current current_msg_imp_current_msgq) done diff -r 271e9818b6f6 -r 99af1986e1e0 simple_selinux/S2ss_prop.thy --- a/simple_selinux/S2ss_prop.thy Mon Dec 02 10:52:40 2013 +0800 +++ b/simple_selinux/S2ss_prop.thy Tue Dec 03 22:42:48 2013 +0800 @@ -10,7 +10,7 @@ lemma co2sobj_some_case: "\co2sobj s obj = Some sobj; \ p. obj = O_proc p \ P (O_proc p); - \ f. obj = O_file f \ P (O_file f); \ h. obj = O_shm h \ P (O_shm h); + \ f. obj = O_file f \ P (O_file f); \ f. obj = O_dir f \ P (O_dir f); \ q. obj = O_msgq q \ P (O_msgq q)\ \ P obj" by (case_tac obj, auto) @@ -25,11 +25,11 @@ "valid (Execve p f fds # s) \ s2ss (Execve p f fds # s) = ( if (\ p'. p' \ p \ p' \ current_procs s \ co2sobj s (O_proc p') = co2sobj s (O_proc p)) then (case (cp2sproc (Execve p f fds # s) p) of - Some sp \ s2ss s \ {S_proc sp (O_proc p \ Tainted s \ O_file f \ Tainted s)} + Some sp \ s2ss s \ {S_proc sp (O_proc p \ tainted s \ O_file f \ tainted s)} | _ \ {} ) else (case (cp2sproc (Execve p f fds # s) p, cp2sproc s p) of - (Some sp, Some sp') \ s2ss s - {S_proc sp' (O_proc p \ Tainted s)} - \ {S_proc sp (O_proc p \ Tainted s \ O_file f \ Tainted s)} + (Some sp, Some sp') \ s2ss s - {S_proc sp' (O_proc p \ tainted s)} + \ {S_proc sp (O_proc p \ tainted s \ O_file f \ tainted s)} | _ \ {} ) )" apply (frule vd_cons, frule vt_grant_os, simp split:if_splits) @@ -42,15 +42,15 @@ apply (simp add:s2ss_def, rule set_eqI, rule iffI) apply (drule CollectD, (erule exE|erule conjE)+) apply (case_tac "obj = O_proc p") -apply (simp add:co2sobj_execve tainted_eq_Tainted split:if_splits) +apply (simp add:co2sobj_execve split:if_splits) apply (simp add:co2sobj_execve, rule disjI2) apply (rule_tac x = obj in exI, case_tac obj, (simp add:alive_simps)+)[1] apply (simp, erule disjE) -apply (rule_tac x = "O_proc p" in exI, simp add:tainted_eq_Tainted) +apply (rule_tac x = "O_proc p" in exI, simp) apply (erule exE| erule conjE)+ apply (case_tac "x = S_proc sp (O_proc p \ tainted s)") apply (rule_tac x = "O_proc p'" in exI) -apply (simp add:alive_execve co2sobj_execve tainted_eq_Tainted cp2sproc_execve) +apply (simp add:alive_execve co2sobj_execve cp2sproc_execve) apply (case_tac "obj = O_proc p", simp) apply (frule co2sobj_execve_alive, simp, simp) apply (frule_tac obj = obj in co2sobj_execve, simp) @@ -62,45 +62,45 @@ apply (erule exE, erule conjE, simp) apply (simp add:s2ss_def, rule set_eqI, rule iffI) apply (drule CollectD, (erule exE|erule conjE)+) -apply (case_tac "obj = O_proc p", simp add:tainted_eq_Tainted) +apply (case_tac "obj = O_proc p", simp) apply (rule disjI1, simp split:if_splits) apply (simp add:co2sobj_execve, rule disjI2) apply (rule conjI,rule_tac x = obj in exI, simp add:alive_simps split:t_object.splits) apply (rule notI, simp, case_tac obj) -apply (erule_tac x = nat in allE, simp add:tainted_eq_Tainted, (simp split:option.splits)+) +apply (erule_tac x = nat in allE, simp, (simp split:option.splits)+) apply (erule disjE, simp) -apply (rule_tac x = "O_proc p" in exI, simp add:tainted_eq_Tainted) +apply (rule_tac x = "O_proc p" in exI, simp) apply (erule exE|erule conjE)+ apply (rule_tac x = obj in exI) apply (drule_tac obj = obj in co2sobj_execve_alive, simp+) apply (frule_tac obj = obj in co2sobj_execve, simp, simp) -apply (rule impI, simp add:tainted_eq_Tainted, simp) +apply (rule impI, simp, simp) done lemma s2ss_clone_alive: - "\co2sobj s obj = Some x; alive s obj; obj \ O_proc p'; valid (Clone p p' fds shms # s)\ - \ alive (Clone p p' fds shms # s) obj" + "\co2sobj s obj = Some x; alive s obj; obj \ O_proc p'; valid (Clone p p' fds # s)\ + \ alive (Clone p p' fds # s) obj" by (erule co2sobj_some_case, auto simp:alive_clone) lemma s2ss_clone: - "valid (Clone p p' fds shms # s) \ s2ss (Clone p p' fds shms # s) = ( - case (cp2sproc (Clone p p' fds shms # s) p') of - Some sp \ s2ss s \ {S_proc sp (O_proc p \ Tainted s)} + "valid (Clone p p' fds # s) \ s2ss (Clone p p' fds # s) = ( + case (cp2sproc (Clone p p' fds # s) p') of + Some sp \ s2ss s \ {S_proc sp (O_proc p \ tainted s)} | _ \ {})" apply (frule vd_cons, frule vt_grant_os, split option.splits) apply (rule conjI, rule impI, drule current_proc_has_sp', simp, simp) apply (rule allI, rule impI, simp add:s2ss_def) apply (rule set_eqI, rule iffI, drule CollectD, (erule exE|erule conjE)+) -apply (case_tac "obj = O_proc p'", simp add:tainted_eq_Tainted) -apply (case_tac "O_proc p' \ Tainted s", drule Tainted_in_current, simp+) +apply (case_tac "obj = O_proc p'", simp) +apply (case_tac "O_proc p' \ tainted s", drule tainted_in_current, simp+) apply (rule disjI1, simp split:if_splits) -apply (simp add:tainted_eq_Tainted, rule disjI2) +apply (simp, rule disjI2) apply (frule co2sobj_clone, simp) apply (rule_tac x = obj in exI, simp add:alive_simps split:t_object.splits) apply (simp, erule disjE, simp) -apply (rule_tac x = "O_proc p'" in exI, simp add:tainted_eq_Tainted) -apply (rule impI, rule notI, drule Tainted_in_current, simp+) +apply (rule_tac x = "O_proc p'" in exI, simp) +apply (rule impI, rule notI, drule tainted_in_current, simp+) apply (erule exE| erule conjE)+ apply (case_tac "obj = O_proc p'", simp) apply (rule_tac x = obj in exI) @@ -108,46 +108,6 @@ apply (auto simp:co2sobj_clone alive_simps) done -definition s2ss_shm_no_backup:: "t_state \ t_process \ t_static_state" -where - "s2ss_shm_no_backup s pfrom \ {S_proc sp False | sp p. info_flow_shm s pfrom p \ cp2sproc s p = Some sp \ - (\ (\ p'. \ info_flow_shm s pfrom p' \ p' \ current_procs s \ co2sobj s (O_proc p') = Some (S_proc sp False)))}" - -definition update_s2ss_shm:: "t_state \ t_process \ t_static_state" -where - "update_s2ss_shm s pfrom \ s2ss s - \ {S_proc sp True| sp p. info_flow_shm s pfrom p \ cp2sproc s p = Some sp} - - (s2ss_shm_no_backup s pfrom)" - -lemma s2ss_shm_no_bk_elim: - "\S_proc sp False \ s2ss_shm_no_backup s pfrom; co2sobj s (O_proc p) = Some (S_proc sp False); - valid s; info_flow_shm s pfrom p\ - \ \ p'. \ info_flow_shm s pfrom p' \ p' \ current_procs s \ co2sobj s (O_proc p') = Some (S_proc sp False)" -apply (auto simp:s2ss_shm_no_backup_def co2sobj.simps tainted_eq_Tainted split:option.splits) -apply (erule_tac x = p in allE, auto) -apply (rule_tac x = p' in exI, auto) -done - -lemma s2ss_shm_no_bk_intro1: - "\co2sobj s' obj = Some x; \ p. obj \ O_proc p\ \ x \ s2ss_shm_no_backup s pfrom" -apply (case_tac obj) -apply (auto simp:co2sobj.simps s2ss_shm_no_backup_def split:option.splits) -done - -lemma s2ss_shm_no_bk_intro2: - "\co2sobj s' obj = Some x; obj \ Tainted s'; valid s'\ \ x \ s2ss_shm_no_backup s pfrom" -apply (case_tac obj) - -apply (auto simp:co2sobj.simps s2ss_shm_no_backup_def tainted_eq_Tainted split:option.splits) -done - -lemma s2ss_shm_no_bk_intro3: - "\co2sobj s (O_proc p) = Some x; \ info_flow_shm s pfrom p; p \ current_procs s - \ \ x \ s2ss_shm_no_backup s pfrom" -apply (auto simp add:s2ss_shm_no_backup_def split:option.splits) -apply (rule_tac x = p in exI, simp) -done - lemma s2ss_shm_no_bk_intro4: "\co2sobj s (O_proc p) = Some x; info_flow_shm s pfrom p; \ info_flow_shm s pfrom p'; p' \ current_procs s; co2sobj s (O_proc p') = Some x\ @@ -156,14 +116,14 @@ apply (auto simp add:s2ss_shm_no_backup_def co2sobj.simps split:option.splits) done -lemma Tainted_ptrace': - "valid s \ Tainted (Ptrace p p' # s) = - (if (O_proc p \ Tainted s \ O_proc p' \ Tainted s) - then Tainted s \ {O_proc p'' | p''. info_flow_shm s p' p''} - else if (O_proc p' \ Tainted s \ O_proc p \ Tainted s) - then Tainted s \ {O_proc p'' | p''. info_flow_shm s p p''} - else Tainted s)" -using info_flow_shm_Tainted by auto +lemma tainted_ptrace': + "valid s \ tainted (Ptrace p p' # s) = + (if (O_proc p \ tainted s \ O_proc p' \ tainted s) + then tainted s \ {O_proc p'' | p''. info_flow_shm s p' p''} + else if (O_proc p' \ tainted s \ O_proc p \ tainted s) + then tainted s \ {O_proc p'' | p''. info_flow_shm s p p''} + else tainted s)" +using info_flow_shm_tainted by auto lemma co2sobj_some_caseD: "\co2sobj s obj = Some sobj; \ p. \co2sobj s obj = Some sobj; obj = O_proc p\ \ P (O_proc p); @@ -177,25 +137,25 @@ lemma s2ss_ptrace1_aux: "x \ {x. P x} \ \ P x" by simp lemma s2ss_ptrace1: - "\valid (Ptrace p p' # s); O_proc p \ Tainted s; O_proc p' \ Tainted s\ + "\valid (Ptrace p p' # s); O_proc p \ tainted s; O_proc p' \ tainted s\ \ s2ss (Ptrace p p' # s) = update_s2ss_shm s p'" unfolding update_s2ss_shm_def s2ss_def s2ss_shm_no_backup_def apply (frule vd_cons, rule set_eqI, rule iffI) apply (drule CollectD, (erule exE|erule conjE)+) apply (erule co2sobj_some_caseD) apply (rule DiffI) -apply (case_tac "O_proc pa \ Tainted s") +apply (case_tac "O_proc pa \ tainted s") apply (rule UnI1, simp, rule_tac x = "O_proc pa" in exI) -apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits) +apply (clarsimp simp:tainted_ptrace' cp2sproc_other split:option.splits) apply (case_tac "info_flow_shm s p' pa") apply (rule UnI2, rule CollectI, simp only:co2sobj.simps split:option.splits) apply (drule current_proc_has_sp', simp, simp) apply (rule_tac x = a in exI, rule_tac x = pa in exI) -apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits) +apply (clarsimp simp:tainted_ptrace' cp2sproc_other split:option.splits) apply (rule UnI1, simp) apply (rule_tac x = "O_proc pa" in exI) -apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits) -apply (rule notI, clarsimp simp:cp2sproc_other tainted_eq_Tainted split:option.splits) +apply (clarsimp simp:tainted_ptrace' cp2sproc_other split:option.splits) +apply (rule notI, clarsimp simp:cp2sproc_other split:option.splits) apply (erule_tac x = pa in allE, simp) apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI, @@ -214,17 +174,17 @@ apply (erule DiffE, drule s2ss_ptrace1_aux, erule UnE) apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI) apply (erule co2sobj_some_caseD) -apply (case_tac "O_proc pa \ Tainted s") +apply (case_tac "O_proc pa \ tainted s") apply (rule_tac x = "O_proc pa" in exI) -apply (clarsimp simp add:tainted_eq_Tainted cp2sproc_other split:option.splits) +apply (clarsimp simp cp2sproc_other split:option.splits) apply (case_tac "info_flow_shm s p' pa", simp only:co2sobj.simps split:option.splits) apply (drule current_proc_has_sp', simp, simp) apply (drule Meson.not_exD, erule_tac x = a in allE, drule Meson.not_exD, erule_tac x = pa in allE) -apply (simp add:tainted_eq_Tainted, (erule exE|erule conjE)+) +apply (simp, (erule exE|erule conjE)+) apply (rule_tac x = "O_proc p'a" in exI) -apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits) +apply (clarsimp simp:tainted_ptrace' cp2sproc_other split:option.splits) apply (rule_tac x = "O_proc pa" in exI) -apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits) +apply (clarsimp simp:tainted_ptrace' cp2sproc_other split:option.splits) apply (rule_tac x = obj in exI, auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1] @@ -237,29 +197,29 @@ apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI) apply (rule_tac x = "O_proc pa" in exI) -apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted info_shm_flow_in_procs) +apply (clarsimp simp:tainted_ptrace' cp2sproc_other info_shm_flow_in_procs) done lemma s2ss_ptrace2: - "\valid (Ptrace p p' # s); O_proc p' \ Tainted s; O_proc p \ Tainted s\ + "\valid (Ptrace p p' # s); O_proc p' \ tainted s; O_proc p \ tainted s\ \ s2ss (Ptrace p p' # s) = update_s2ss_shm s p" unfolding update_s2ss_shm_def s2ss_def s2ss_shm_no_backup_def apply (frule vd_cons, rule set_eqI, rule iffI) apply (drule CollectD, (erule exE|erule conjE)+) apply (erule co2sobj_some_caseD) apply (rule DiffI) -apply (case_tac "O_proc pa \ Tainted s") +apply (case_tac "O_proc pa \ tainted s") apply (rule UnI1, simp, rule_tac x = "O_proc pa" in exI) -apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits) +apply (clarsimp simp:tainted_ptrace' cp2sproc_other split:option.splits) apply (case_tac "info_flow_shm s p pa") apply (rule UnI2, rule CollectI, simp only:co2sobj.simps split:option.splits) apply (drule current_proc_has_sp', simp, simp) apply (rule_tac x = a in exI, rule_tac x = pa in exI) -apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits) +apply (clarsimp simp:tainted_ptrace' cp2sproc_other split:option.splits) apply (rule UnI1, simp) apply (rule_tac x = "O_proc pa" in exI) -apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits) -apply (rule notI, clarsimp simp:cp2sproc_other tainted_eq_Tainted split:option.splits) +apply (clarsimp simp:tainted_ptrace' cp2sproc_other split:option.splits) +apply (rule notI, clarsimp simp:cp2sproc_other split:option.splits) apply (erule_tac x = pa in allE, simp) apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI, @@ -278,17 +238,17 @@ apply (erule DiffE, drule s2ss_ptrace1_aux, erule UnE) apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI) apply (erule co2sobj_some_caseD) -apply (case_tac "O_proc pa \ Tainted s") +apply (case_tac "O_proc pa \ tainted s") apply (rule_tac x = "O_proc pa" in exI) -apply (clarsimp simp add:tainted_eq_Tainted cp2sproc_other split:option.splits) +apply (clarsimp simp cp2sproc_other split:option.splits) apply (case_tac "info_flow_shm s p pa", simp only:co2sobj.simps split:option.splits) apply (drule current_proc_has_sp', simp, simp) apply (drule Meson.not_exD, erule_tac x = a in allE, drule Meson.not_exD, erule_tac x = pa in allE) -apply (simp add:tainted_eq_Tainted, (erule exE|erule conjE)+) +apply (simp, (erule exE|erule conjE)+) apply (rule_tac x = "O_proc p'a" in exI) -apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits) +apply (clarsimp simp:tainted_ptrace' cp2sproc_other split:option.splits) apply (rule_tac x = "O_proc pa" in exI) -apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits) +apply (clarsimp simp:tainted_ptrace' cp2sproc_other split:option.splits) apply (rule_tac x = obj in exI, auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1] @@ -301,11 +261,11 @@ apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI) apply (rule_tac x = "O_proc pa" in exI) -apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted info_shm_flow_in_procs) +apply (clarsimp simp:tainted_ptrace' cp2sproc_other info_shm_flow_in_procs) done lemma s2ss_ptrace3: - "\valid (Ptrace p p' # s); (O_proc p' \ Tainted s) = (O_proc p \ Tainted s)\ + "\valid (Ptrace p p' # s); (O_proc p' \ tainted s) = (O_proc p \ tainted s)\ \ s2ss (Ptrace p p' # s) = s2ss s" unfolding s2ss_def apply (frule vd_cons, rule set_eqI, rule iffI) @@ -313,22 +273,22 @@ apply (rule_tac x = obj in exI) apply (frule alive_other, simp+) apply (frule_tac obj = obj in co2sobj_ptrace, simp) -apply (auto simp add:tainted_eq_Tainted split:t_object.splits option.splits if_splits - intro:info_flow_shm_Tainted)[1] +apply (auto simp split:t_object.splits option.splits if_splits + intro:info_flow_shm_tainted)[1] apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI) apply (rule_tac x = obj in exI) apply (frule alive_other, simp+) apply (frule_tac obj = obj in co2sobj_ptrace, simp) -apply (auto simp add:tainted_eq_Tainted split:t_object.splits option.splits if_splits - intro:info_flow_shm_Tainted) +apply (auto simp split:t_object.splits option.splits if_splits + intro:info_flow_shm_tainted) done lemma s2ss_ptrace: "valid (Ptrace p p' # s) \ s2ss (Ptrace p p' # s) = ( - if (O_proc p \ Tainted s \ O_proc p' \ Tainted s) + if (O_proc p \ tainted s \ O_proc p' \ tainted s) then update_s2ss_shm s p' - else if (O_proc p' \ Tainted s \ O_proc p \ Tainted s) + else if (O_proc p' \ tainted s \ O_proc p \ tainted s) then update_s2ss_shm s p else s2ss s )" apply (frule vt_grant_os, frule vd_cons) @@ -351,15 +311,15 @@ apply (simp split: option.splits, (erule conjE)+) apply (rule set_eqI, rule iffI, erule CollectE, (erule exE|erule conjE)+, rule CollectI) apply (rule_tac x = obj in exI) -apply (simp add:co2sobj_kill tainted_eq_Tainted alive_kill split:t_object.splits if_splits) +apply (simp add:co2sobj_kill alive_kill split:t_object.splits if_splits) apply (erule CollectE, erule exE, erule conjE, rule CollectI) apply (erule co2sobj_some_caseD) apply (case_tac "pa = p'") apply (rule_tac x = "O_proc p''" in exI) -apply (simp add:cp2sproc_kill tainted_eq_Tainted alive_kill +apply (simp add:cp2sproc_kill alive_kill split:t_object.splits if_splits option.splits) apply (rule_tac x = "O_proc pa" in exI) -apply (clarsimp simp add:cp2sproc_kill tainted_eq_Tainted alive_kill +apply (clarsimp simp add:cp2sproc_kill alive_kill split:t_object.splits if_splits option.splits) apply (rule_tac x = obj in exI, frule alive_kill, simp add:co2sobj_kill del:co2sobj.simps)+ @@ -367,18 +327,18 @@ apply (rule set_eqI, rule iffI) apply (erule CollectE, erule exE, erule conjE, rule DiffI) apply (rule CollectI, rule_tac x = obj in exI) -apply (simp add:co2sobj_kill tainted_eq_Tainted alive_kill split:t_object.splits if_splits) +apply (simp add:co2sobj_kill alive_kill split:t_object.splits if_splits) apply (rule notI, simp, case_tac obj) apply (erule_tac x = nat in allE) -apply (simp add:co2sobj_kill cp2sproc_kill tainted_eq_Tainted split:option.splits) +apply (simp add:co2sobj_kill cp2sproc_kill split:option.splits) apply (simp split:option.splits)+ apply (erule co2sobj_some_caseD) apply (case_tac "pa = p'") apply (rule_tac x = "O_proc p''" in exI) -apply (simp add:cp2sproc_kill tainted_eq_Tainted alive_kill +apply (simp add:cp2sproc_kill alive_kill split:t_object.splits if_splits option.splits) apply (rule_tac x = "O_proc pa" in exI) -apply (clarsimp simp add:cp2sproc_kill tainted_eq_Tainted alive_kill +apply (clarsimp simp add:cp2sproc_kill alive_kill split:t_object.splits if_splits option.splits) apply (rule_tac x = obj in exI, frule alive_kill, simp add:co2sobj_kill del:co2sobj.simps)+ done @@ -399,15 +359,15 @@ apply (simp split: option.splits, (erule conjE)+) apply (rule set_eqI, rule iffI, erule CollectE, (erule exE|erule conjE)+, rule CollectI) apply (rule_tac x = obj in exI) -apply (simp add:co2sobj_exit tainted_eq_Tainted alive_exit split:t_object.splits if_splits) +apply (simp add:co2sobj_exit alive_exit split:t_object.splits if_splits) apply (erule CollectE, erule exE, erule conjE, rule CollectI) apply (erule co2sobj_some_caseD) apply (case_tac "pa = p") apply (rule_tac x = "O_proc p'" in exI) -apply (simp add:cp2sproc_exit tainted_eq_Tainted alive_exit +apply (simp add:cp2sproc_exit alive_exit split:t_object.splits if_splits option.splits) apply (rule_tac x = "O_proc pa" in exI) -apply (clarsimp simp add:cp2sproc_exit tainted_eq_Tainted alive_exit +apply (clarsimp simp add:cp2sproc_exit alive_exit split:t_object.splits if_splits option.splits) apply (rule_tac x = obj in exI, frule alive_exit, simp add:co2sobj_exit del:co2sobj.simps)+ @@ -415,18 +375,18 @@ apply (rule set_eqI, rule iffI) apply (erule CollectE, erule exE, erule conjE, rule DiffI) apply (rule CollectI, rule_tac x = obj in exI) -apply (simp add:co2sobj_exit tainted_eq_Tainted alive_exit split:t_object.splits if_splits) +apply (simp add:co2sobj_exit alive_exit split:t_object.splits if_splits) apply (rule notI, simp, case_tac obj) apply (erule_tac x = nat in allE) -apply (simp add:co2sobj_exit cp2sproc_exit tainted_eq_Tainted split:option.splits) +apply (simp add:co2sobj_exit cp2sproc_exit split:option.splits) apply (simp split:option.splits)+ apply (erule co2sobj_some_caseD) apply (case_tac "pa = p") apply (rule_tac x = "O_proc p'" in exI) -apply (simp add:cp2sproc_exit tainted_eq_Tainted alive_exit +apply (simp add:cp2sproc_exit alive_exit split:t_object.splits if_splits option.splits) apply (rule_tac x = "O_proc pa" in exI) -apply (clarsimp simp add:cp2sproc_exit tainted_eq_Tainted alive_exit +apply (clarsimp simp add:cp2sproc_exit alive_exit split:t_object.splits if_splits option.splits) apply (rule_tac x = obj in exI, frule alive_exit, simp add:co2sobj_exit del:co2sobj.simps)+ done @@ -443,7 +403,7 @@ "\valid (Open p f flag fd None # s); alive s obj\ \ co2sobj (Open p f flag fd None # s) obj = ( if (obj = O_proc p) then (case (cp2sproc (Open p f flag fd None # s) p) of - Some sp \ Some (S_proc sp (O_proc p \ Tainted s)) + Some sp \ Some (S_proc sp (O_proc p \ tainted s)) | _ \ None) else co2sobj s obj)" apply (frule vt_grant_os, frule vd_cons) @@ -455,11 +415,11 @@ "\valid (Open p f flag fd (Some i) # s); alive s obj\ \ co2sobj (Open p f flag fd (Some i) # s) obj = ( if (obj = O_proc p) then (case (cp2sproc (Open p f flag fd (Some i) # s) p) of - Some sp \ Some (S_proc sp (O_proc p \ Tainted s)) + Some sp \ Some (S_proc sp (O_proc p \ tainted s)) | _ \ None) else if (obj = O_file f) then (case (cf2sfile (Open p f flag fd (Some i) # s) f) of - Some sf \ Some (S_file {sf} (O_proc p \ Tainted s)) + Some sf \ Some (S_file {sf} (O_proc p \ tainted s)) | _ \ None) else co2sobj s obj)" apply (frule vt_grant_os, frule vd_cons) @@ -607,7 +567,7 @@ lemma s2ss_readfile: "valid (ReadFile p fd # s) \ s2ss (ReadFile p fd # s) = ( case (file_of_proc_fd s p fd) of - Some f \ if (O_file f \ Tainted s) + Some f \ if (O_file f \ tainted s) then update_s2ss_shm s p else s2ss s | _ \ {})" @@ -618,18 +578,18 @@ apply (drule CollectD, (erule exE|erule conjE)+) apply (erule co2sobj_some_caseD) apply (rule DiffI) -apply (case_tac "O_proc pa \ Tainted s") +apply (case_tac "O_proc pa \ tainted s") apply (rule UnI1, simp, rule_tac x = "O_proc pa" in exI) -apply (clarsimp simp:cp2sproc_other tainted_eq_Tainted co2sobj.simps split:option.splits) +apply (clarsimp simp:cp2sproc_other co2sobj.simps split:option.splits) apply (case_tac "info_flow_shm s p pa") apply (rule UnI2, rule CollectI, simp only:co2sobj.simps split:option.splits) apply (drule current_proc_has_sp', simp, simp) apply (rule_tac x = ab in exI, rule_tac x = pa in exI) -apply (clarsimp simp:cp2sproc_other tainted_eq_Tainted split:option.splits) +apply (clarsimp simp:cp2sproc_other split:option.splits) apply (rule UnI1, simp) apply (rule_tac x = "O_proc pa" in exI) -apply (clarsimp simp:cp2sproc_other tainted_eq_Tainted co2sobj.simps split:option.splits) -apply (rule notI, clarsimp simp:cp2sproc_other tainted_eq_Tainted co2sobj.simps split:option.splits) +apply (clarsimp simp:cp2sproc_other co2sobj.simps split:option.splits) +apply (rule notI, clarsimp simp:cp2sproc_other co2sobj.simps split:option.splits) apply (erule_tac x = pa in allE, simp) apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI) @@ -644,17 +604,17 @@ apply (erule DiffE, drule s2ss_ptrace1_aux, erule UnE) apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI) apply (erule co2sobj_some_caseD) -apply (case_tac "O_proc pa \ Tainted s") +apply (case_tac "O_proc pa \ tainted s") apply (rule_tac x = "O_proc pa" in exI) -apply (clarsimp simp:tainted_eq_Tainted cp2sproc_other co2sobj.simps split:option.splits) +apply (clarsimp simp:tainted_eq_tainted cp2sproc_other co2sobj.simps split:option.splits) apply (case_tac "info_flow_shm s p pa", simp only:co2sobj.simps split:option.splits) apply (drule current_proc_has_sp', simp, simp) apply (drule Meson.not_exD, erule_tac x = ab in allE, drule Meson.not_exD, erule_tac x = pa in allE) -apply (simp add:tainted_eq_Tainted, (erule exE|erule conjE)+) +apply (simp, (erule exE|erule conjE)+) apply (rule_tac x = "O_proc p'" in exI) -apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted co2sobj.simps split:option.splits) +apply (clarsimp simp:tainted_ptrace' cp2sproc_other co2sobj.simps split:option.splits) apply (rule_tac x = "O_proc pa" in exI) -apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted co2sobj.simps split:option.splits) +apply (clarsimp simp:tainted_ptrace' cp2sproc_other co2sobj.simps split:option.splits) apply (rule_tac x = obj in exI, auto split:option.splits simp:co2sobj_readfile alive_simps simp del:co2sobj.simps)[1] @@ -667,7 +627,7 @@ apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI) apply (rule_tac x = "O_proc pa" in exI) -apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted info_shm_flow_in_procs co2sobj.simps) +apply (clarsimp simp:tainted_ptrace' cp2sproc_other info_shm_flow_in_procs co2sobj.simps) apply (rule impI, rule impI) @@ -695,18 +655,18 @@ lemma co2sobj_writefile_unchange: "\valid (WriteFile p fd # s); alive s obj; file_of_proc_fd s p fd = Some f; - O_proc p \ Tainted s \ O_file f \ Tainted s\ + O_proc p \ tainted s \ O_file f \ tainted s\ \ co2sobj (WriteFile p fd # s) obj = co2sobj s obj" apply (frule vd_cons, frule co2sobj_writefile, simp, simp split:t_object.splits if_splits) apply (simp add:co2sobj.simps) -apply (case_tac "O_proc p \ Tainted s") -apply (simp add:tainted_eq_Tainted same_inodes_Tainted)+ +apply (case_tac "O_proc p \ tainted s") +apply (simp same_inodes_tainted)+ done lemma s2ss_writefile: "valid (WriteFile p fd # s) \ s2ss (WriteFile p fd # s) = ( case (file_of_proc_fd s p fd) of - Some f \ if (O_proc p \ Tainted s \ O_file f \ Tainted s) + Some f \ if (O_proc p \ tainted s \ O_file f \ tainted s) then (if (\ f'. f' \ same_inode_files s f \ is_file s f' \ co2sobj s (O_file f') = co2sobj s (O_file f)) then s2ss s \ {S_file (cf2sfiles s f) True} @@ -744,7 +704,7 @@ apply (frule_tac f = fa and f' = aa in cf2sfiles_prop, simp) apply (rule_tac x = "O_file f'" in exI, simp add:co2sobj_writefile is_file_simps) apply (rule conjI, rule impI, simp add:same_inode_files_prop5) -apply (rule impI, simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted) +apply (rule impI, simp add:co2sobj.simps same_inodes_tainted) apply (rule_tac x = "O_file fa" in exI, simp add:co2sobj_writefile is_file_simps) apply (rule impI, simp add:same_inode_files_prop5) apply (rule_tac x = obj in exI, simp add:co2sobj_writefile) @@ -754,8 +714,8 @@ apply (rule impI, rule impI, simp, rule set_eqI, rule iffI, erule CollectE, (erule conjE|erule exE)+) apply (rule CollectI, rule_tac x = obj in exI, simp add:alive_simps) apply (simp add:co2sobj_writefile split:t_object.splits if_splits) -apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted) -apply (case_tac "O_proc p \ Tainted s", simp, simp) +apply (simp add:co2sobj.simps same_inodes_tainted) +apply (case_tac "O_proc p \ tainted s", simp, simp) apply (erule CollectE, (erule conjE|erule exE)+, rule CollectI) apply (rule_tac x = obj in exI) apply (simp add:co2sobj_writefile_unchange alive_simps) @@ -769,7 +729,7 @@ apply (rule disjI1, simp add:cf2sfiles_prop) apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp) apply (rule notI, simp add:co2sobj.simps split:option.splits) -apply (erule_tac x = list in allE, simp add:tainted_eq_Tainted same_inode_files_prop5) +apply (erule_tac x = list in allE, simp same_inode_files_prop5) apply (simp add:co2sobj.simps) apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp, rule notI, simp add:co2sobj.simps split:option.splits) @@ -789,7 +749,7 @@ apply (erule co2sobj_some_caseD) apply (rule_tac x = obj in exI, simp add:co2sobj_writefile) apply (case_tac "fa \ same_inode_files s aa") -apply (frule cf2sfiles_prop, simp, simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted) +apply (frule cf2sfiles_prop, simp, simp add:co2sobj.simps same_inodes_tainted) apply (rule_tac x = obj in exI, simp add:co2sobj_writefile is_file_simps) apply (rule impI, simp add:same_inode_files_prop5) apply (rule_tac x = obj in exI, simp add:co2sobj_writefile) @@ -818,7 +778,7 @@ "update_s2ss_sfile_del s ss f sf \ if (same_inode_files s f = {f}) then ss - else ss \ {S_file (cf2sfiles s f - {sf}) (O_file f \ Tainted s)}" + else ss \ {S_file (cf2sfiles s f - {sf}) (O_file f \ tainted s)}" definition del_s2ss_file:: "t_state \ t_static_state \ t_file \ t_sfile \ t_static_state" where @@ -827,7 +787,7 @@ then ss else if (\ f'. is_file s f' \ f' \ same_inode_files s f \ co2sobj s (O_file f') = co2sobj s (O_file f)) then update_s2ss_sfile_del s ss f sf - else update_s2ss_sfile_del s (ss - {S_file (cf2sfiles s f) (O_file f \ Tainted s)}) f sf)" + else update_s2ss_sfile_del s (ss - {S_file (cf2sfiles s f) (O_file f \ tainted s)}) f sf)" lemma alive_co2sobj_closefd1: "\alive s obj; valid (CloseFd p fd # s); co2sobj s obj = Some sobj; @@ -921,14 +881,14 @@ (Some sf, Some sp, Some sp') \ (del_s2ss_file s ( update_s2ss_obj s (s2ss s) (O_proc p) - (S_proc sp (O_proc p \ Tainted s)) - (S_proc sp' (O_proc p \ Tainted s))) f sf) + (S_proc sp (O_proc p \ tainted s)) + (S_proc sp' (O_proc p \ tainted s))) f sf) | _ \ {}) else (case (cp2sproc s p, cp2sproc (CloseFd p fd # s) p) of (Some sp, Some sp') \ (update_s2ss_obj s (s2ss s) (O_proc p) - (S_proc sp (O_proc p \ Tainted s)) - (S_proc sp' (O_proc p \ Tainted s))) + (S_proc sp (O_proc p \ tainted s)) + (S_proc sp' (O_proc p \ tainted s))) | _ \ {}) | _ \ s2ss s)" apply (frule vd_cons, frule vt_grant_os) @@ -942,12 +902,12 @@ apply (frule co2sobj_closefd, simp) apply (frule cp2sproc_closefd, simp) apply (simp add:proc_file_fds_def split:t_object.splits) -apply (simp split:if_splits add:co2sobj.simps tainted_eq_Tainted) +apply (simp split:if_splits add:co2sobj.simps) apply (erule CollectE, erule exE, erule conjE, rule CollectI) apply (rule_tac x = obj in exI, simp add:alive_co2sobj_closefd2) apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd2) apply (frule cp2sproc_closefd, simp) -apply (auto simp add:proc_file_fds_def co2sobj.simps tainted_eq_Tainted +apply (auto simp add:proc_file_fds_def co2sobj.simps split:t_object.splits option.splits if_splits)[1] apply (case_tac "cp2sproc (CloseFd p fd # s) p") @@ -965,58 +925,58 @@ apply (tactic {*my_seteq_tac 1*}) apply simp apply (case_tac "obj = O_proc p") -apply (simp add:co2sobj.simps tainted_eq_Tainted) +apply (simp add:co2sobj.simps) apply (rule disjI2, rule_tac x = obj in exI) apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_simps) -apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits) +apply (simp add:alive_simps co2sobj.simps split:t_object.splits if_splits) apply (tactic {*my_setiff_tac 1*}) apply (rule_tac x = "O_proc p" in exI) -apply (simp add:co2sobj.simps tainted_eq_Tainted) +apply (simp add:co2sobj.simps) apply (tactic {*my_setiff_tac 1*}) apply (case_tac "obj = O_proc p") apply (rule_tac x = obj' in exI) apply (frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd) -apply (simp add:co2sobj.simps tainted_eq_Tainted) +apply (simp add:co2sobj.simps) apply (case_tac "obj = O_file a") apply (rule_tac x = "O_file f'" in exI) apply (case_tac "f' = a", simp add:same_inode_files_prop9 file_of_pfd_is_file) apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps) -apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits) +apply (simp add:alive_simps co2sobj.simps split:t_object.splits if_splits) apply (rule_tac x = obj in exI) apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+) apply (frule_tac obj = obj in co2sobj_closefd, simp) -apply (auto simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1] +apply (auto simp add:alive_simps co2sobj.simps split:t_object.splits if_splits)[1] apply (rule impI)+ apply (tactic {*my_seteq_tac 1*}) -apply (case_tac "obj = O_proc p", rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted) +apply (case_tac "obj = O_proc p", rule disjI1, simp add:co2sobj.simps) apply (rule disjI2) apply (case_tac "obj = O_file a", simp add:alive_simps) apply (rule DiffI, simp) apply (rule_tac x = obj in exI) apply (frule_tac obj = obj in alive_co2sobj_closefd', simp+) apply (frule_tac obj = obj in co2sobj_closefd, simp) -apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits) +apply (simp add:alive_simps co2sobj.simps split:t_object.splits if_splits) apply (simp, rule notI, simp, frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd) apply (erule_tac x = "O_proc pa" in allE, simp) apply (tactic {*my_setiff_tac 1*}) -apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted) +apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps) apply (tactic {*my_setiff_tac 1*}) -apply (case_tac "obj = O_proc p", simp add:co2sobj.simps tainted_eq_Tainted) +apply (case_tac "obj = O_proc p", simp add:co2sobj.simps) apply (case_tac "obj = O_file a", rule_tac x = "O_file f'" in exI) apply (case_tac "f' = a", simp add:same_inode_files_prop9 file_of_pfd_is_file) apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps) -apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits) +apply (simp add:alive_simps co2sobj.simps split:t_object.splits if_splits) apply (rule_tac x = obj in exI) apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+) apply (frule_tac obj = obj in co2sobj_closefd, simp) -apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1] +apply (auto simp add:co2sobj.simps split:t_object.splits if_splits)[1] apply (rule impI, tactic {*my_seteq_tac 1*}) apply (simp add:update_s2ss_obj_def update_s2ss_sfile_del_def) apply (rule conjI| rule impI|erule exE|erule conjE)+ apply (erule_tac obj = obj in co2sobj_some_caseD) -apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted) +apply (case_tac "pa = p", simp add:co2sobj.simps) apply (rule disjI2, rule_tac x = obj in exI) apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps) apply (case_tac "f = a", simp add:alive_simps) @@ -1030,14 +990,14 @@ apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps) apply (rule conjI| rule impI|erule exE|erule conjE)+ apply (erule_tac obj = obj in co2sobj_some_caseD) -apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted) +apply (case_tac "pa = p", simp add:co2sobj.simps) apply (rule disjI2, rule disjI2, rule_tac x = obj in exI) apply (frule_tac obj = obj in co2sobj_closefd, simp) -apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1] +apply (auto simp add:co2sobj.simps split:t_object.splits if_splits)[1] apply (case_tac "f = a", simp add:alive_simps) apply (case_tac "f \ same_inode_files s a", rule disjI1) apply (simp add:co2sobj_simps split:if_splits option.splits t_sobject.splits) -apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop) +apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop) apply (erule bexE, erule conjE) apply (erule_tac x = f'' in ballE, simp, simp) apply (rule disjI2, rule disjI2, rule_tac x = obj in exI) @@ -1050,7 +1010,7 @@ apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps) apply (rule impI, rule conjI, rule impI) apply (erule_tac obj = obj in co2sobj_some_caseD) -apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted) +apply (case_tac "pa = p", simp add:co2sobj.simps) apply (rule disjI2, rule conjI, rule_tac x = obj in exI) apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps) apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp add:is_file_simps) @@ -1069,16 +1029,16 @@ apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp) apply (rule impI) apply (erule_tac obj = obj in co2sobj_some_caseD) -apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted) +apply (case_tac "pa = p", simp add:co2sobj.simps) apply (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI) apply (frule_tac obj = obj in co2sobj_closefd, simp) -apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1] +apply (auto simp add:co2sobj.simps split:t_object.splits if_splits)[1] apply (rule notI, simp add:co2sobj_closefd) apply (erule_tac x = obj in allE, simp) apply (case_tac "f = a", simp add:alive_simps) apply (case_tac "f \ same_inode_files s a", rule disjI1) apply (simp add:co2sobj_simps split:if_splits option.splits t_sobject.splits) -apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop) +apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop) apply (erule bexE, erule conjE) apply (erule_tac x = f'' in ballE, simp, simp) apply (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI) @@ -1095,34 +1055,34 @@ apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp) apply (simp add:update_s2ss_sfile_del_def update_s2ss_obj_def split:if_splits) -apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted) +apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps) apply (erule exE, erule conjE) apply (case_tac "obj = O_proc p") apply (rule_tac x = obj' in exI) apply (frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd) -apply (simp add:co2sobj.simps tainted_eq_Tainted) +apply (simp add:co2sobj.simps) apply (case_tac "obj = O_file a") apply (rule_tac x = "O_file f'" in exI) apply (case_tac "f' = a", simp add:same_inode_files_prop9 file_of_pfd_is_file) apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps) -apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits) +apply (simp add:alive_simps co2sobj.simps split:t_object.splits if_splits) apply (rule_tac x = obj in exI) apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+) apply (frule_tac obj = obj in co2sobj_closefd, simp) -apply (auto simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1] -apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted) +apply (auto simp add:alive_simps co2sobj.simps split:t_object.splits if_splits)[1] +apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps) apply (erule conjE, erule exE, erule conjE) apply (case_tac "obj = O_proc p") -apply (simp add:co2sobj.simps tainted_eq_Tainted) +apply (simp add:co2sobj.simps) apply (case_tac "obj = O_file a") apply (rule_tac x = "O_file f'" in exI) apply (case_tac "f' = a", simp add:same_inode_files_prop9 file_of_pfd_is_file) apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps) -apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits) +apply (simp add:alive_simps co2sobj.simps split:t_object.splits if_splits) apply (rule_tac x = obj in exI) apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+) apply (frule_tac obj = obj in co2sobj_closefd, simp) -apply (auto simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1] +apply (auto simp add:alive_simps co2sobj.simps split:t_object.splits if_splits)[1] apply (erule disjE) apply (drule same_inode_files_prop10, simp add:file_of_pfd_is_file, erule exE, erule conjE) apply (rule_tac x = "O_file f'a" in exI) @@ -1130,16 +1090,16 @@ apply (frule_tac obj = "O_file f'a" in co2sobj_closefd) apply (simp add:alive_simps)+ apply (frule_tac f = "f'a" in is_file_has_sfile', simp, erule exE) -apply (simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted split:if_splits) +apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted split:if_splits) apply (rule impI, erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp) apply (erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp) apply (erule disjE) -apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted) +apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps) apply (erule exE, erule conjE) apply (case_tac "obj = O_proc p") apply (rule_tac x = obj' in exI) apply (frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd) -apply (simp add:co2sobj.simps tainted_eq_Tainted) +apply (simp add:co2sobj.simps) apply (erule_tac obj = obj in co2sobj_some_caseD) apply (rule_tac x = obj in exI) apply (simp add:co2sobj_closefd) @@ -1147,7 +1107,7 @@ apply (rule_tac x = "O_file f'" in exI) apply (simp add:co2sobj_simps is_file_simps split:if_splits option.splits t_sobject.splits) apply (rule conjI, rule notI, simp add:same_inode_files_prop9) -apply (rule impI, simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted) +apply (rule impI, simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted) apply (rule_tac x = obj in exI) apply (simp add:co2sobj_closefd is_file_simps) apply (rule notI, simp add:same_inode_files_prop9) @@ -1162,15 +1122,15 @@ apply (frule_tac obj = "O_file f'a" in co2sobj_closefd) apply (simp add:alive_simps)+ apply (frule_tac f = "f'a" in is_file_has_sfile', simp, erule exE) -apply (simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted split:if_splits) +apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted split:if_splits) apply (rule impI, erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp) apply (erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp) apply (erule disjE) apply (rule_tac x = "O_proc p" in exI) -apply (simp add:co2sobj.simps tainted_eq_Tainted) +apply (simp add:co2sobj.simps) apply (erule conjE, erule exE, erule conjE) apply (case_tac "obj = O_proc p") -apply (simp add:co2sobj.simps tainted_eq_Tainted) +apply (simp add:co2sobj.simps) apply (erule_tac obj = obj in co2sobj_some_caseD) apply (rule_tac x = obj in exI) apply (simp add:co2sobj_closefd) @@ -1178,7 +1138,7 @@ apply (rule_tac x = "O_file f'" in exI) apply (simp add:co2sobj_simps is_file_simps split:if_splits option.splits t_sobject.splits) apply (rule conjI, rule notI, simp add:same_inode_files_prop9) -apply (rule impI, simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted) +apply (rule impI, simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted) apply (rule_tac x = obj in exI) apply (simp add:co2sobj_closefd is_file_simps) apply (rule notI, simp add:same_inode_files_prop9) @@ -1191,7 +1151,7 @@ apply (simp add:update_s2ss_obj_def update_s2ss_sfile_del_def) apply (rule conjI| rule impI|erule exE|erule conjE)+ apply (erule_tac obj = obj in co2sobj_some_caseD) -apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted) +apply (case_tac "pa = p", simp add:co2sobj.simps) apply (rule disjI2, rule_tac x = obj in exI) apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps) apply (case_tac "f = a", simp add:alive_simps) @@ -1205,18 +1165,18 @@ apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps) apply (rule conjI| rule impI|erule exE|erule conjE)+ apply (erule_tac obj = obj in co2sobj_some_caseD) -apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted) +apply (case_tac "pa = p", simp add:co2sobj.simps) apply (rule disjI2, rule conjI, rule_tac x = obj in exI) apply (frule_tac obj = obj in co2sobj_closefd, simp) -apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1] +apply (auto simp add:co2sobj.simps split:t_object.splits if_splits)[1] apply (rule notI, simp, erule_tac x = "O_proc pa" in allE, simp add:co2sobj_closefd) apply (case_tac "f = a", simp add:alive_simps) apply (case_tac "f \ same_inode_files s a", rule disjI2) apply (simp add:co2sobj_simps split:if_splits option.splits t_sobject.splits) -apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop) +apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop) apply (erule bexE, erule conjE) apply (rule conjI, rule_tac x = "O_file f''" in exI) -apply (simp add:same_inode_files_prop11 co2sobj.simps tainted_eq_Tainted cf2sfiles_prop same_inodes_Tainted) +apply (simp add:same_inode_files_prop11 co2sobj.simps cf2sfiles_prop same_inodes_tainted) apply (rule notI, simp) apply (rule disjI2, rule conjI, rule_tac x = obj in exI) apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps) @@ -1233,47 +1193,47 @@ apply (erule bexE, erule conjE) apply (simp add:update_s2ss_obj_def split:if_splits) -apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted) +apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps) apply (erule exE, erule conjE) apply (case_tac "obj = O_proc p") apply (rule_tac x = obj' in exI) apply (frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd) -apply (simp add:co2sobj.simps tainted_eq_Tainted) +apply (simp add:co2sobj.simps) apply (case_tac "obj = O_file a") apply (rule_tac x = "O_file f'" in exI) apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps same_inode_files_prop11) -apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits) +apply (simp add:alive_simps co2sobj.simps split:t_object.splits if_splits) apply (rule conjI) apply (rule impI) apply (rule_tac x = f' in ballE, simp, simp, simp) -apply (simp add:same_inode_files_prop11 co2sobj.simps cf2sfiles_prop same_inodes_Tainted) +apply (simp add:same_inode_files_prop11 co2sobj.simps cf2sfiles_prop same_inodes_tainted) apply (rule_tac x = obj in exI) apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+) apply (frule_tac obj = obj in co2sobj_closefd, simp) -apply (auto simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1] -apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted) +apply (auto simp add:alive_simps co2sobj.simps split:t_object.splits if_splits)[1] +apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps) apply (erule conjE, erule exE, erule conjE) apply (case_tac "obj = O_proc p") -apply (simp add:co2sobj.simps tainted_eq_Tainted) +apply (simp add:co2sobj.simps) apply (case_tac "obj = O_file a") apply (rule_tac x = "O_file f'" in exI) apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps same_inode_files_prop11) -apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits) +apply (simp add:alive_simps co2sobj.simps split:t_object.splits if_splits) apply (rule conjI) apply (rule impI) apply (rule_tac x = f' in ballE, simp, simp, simp) -apply (simp add:same_inode_files_prop11 co2sobj.simps cf2sfiles_prop same_inodes_Tainted) +apply (simp add:same_inode_files_prop11 co2sobj.simps cf2sfiles_prop same_inodes_tainted) apply (rule_tac x = obj in exI) apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+) apply (frule_tac obj = obj in co2sobj_closefd, simp) -apply (auto simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1] +apply (auto simp add:alive_simps co2sobj.simps split:t_object.splits if_splits)[1] apply (rule impI) apply (tactic {*my_seteq_tac 1*}) apply (simp add:update_s2ss_obj_def update_s2ss_sfile_del_def) apply (rule conjI| rule impI|erule exE|erule conjE)+ apply (erule_tac obj = obj in co2sobj_some_caseD) -apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted) +apply (case_tac "pa = p", simp add:co2sobj.simps) apply (rule disjI2, rule_tac x = obj in exI) apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps) apply (case_tac "f = a", simp add:alive_simps) @@ -1287,25 +1247,25 @@ apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps) apply (frule_tac obj = obj in co2sobj_closefd, simp, rule notI, simp) apply (frule_tac obj = obj in co2sobj_sfile_imp, erule exE, simp add:is_file_simps split:if_splits) -apply (erule_tac x= f in allE, simp add:co2sobj.simps tainted_eq_Tainted) +apply (erule_tac x= f in allE, simp add:co2sobj.simps) apply (rule conjI| rule impI|erule exE|erule conjE)+ apply (erule_tac obj = obj in co2sobj_some_caseD) -apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted) +apply (case_tac "pa = p", simp add:co2sobj.simps) apply (rule disjI2, rule notI, simp) apply (rule disjI2, rule conjI, rule disjI2, rule_tac x = obj in exI) apply (frule_tac obj = obj in co2sobj_closefd, simp) -apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1] +apply (auto simp add:co2sobj.simps split:t_object.splits if_splits)[1] apply (rule notI, simp add:co2sobj.simps split:option.splits) apply (case_tac "f = a", simp add:alive_simps) apply (case_tac "f \ same_inode_files s a", rule disjI1) apply (simp add:co2sobj_simps split:if_splits option.splits t_sobject.splits) -apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop) +apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop) apply (erule bexE, erule conjE) apply (erule_tac x = f'' in ballE, simp, simp) apply (rule disjI2, rule conjI, rule disjI2, rule_tac x = obj in exI) -apply (simp add:is_file_simps co2sobj_closefd tainted_eq_Tainted) +apply (simp add:is_file_simps co2sobj_closefd) apply (rule notI, simp add:co2sobj_closefd) -apply (erule_tac x = f in allE, simp add:is_file_simps co2sobj.simps tainted_eq_Tainted) +apply (erule_tac x = f in allE, simp add:is_file_simps co2sobj.simps) apply (rule disjI2, rule conjI, rule disjI2, rule_tac x = obj in exI) apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps) apply (rule notI, simp add:co2sobj.simps split:option.splits) @@ -1318,11 +1278,11 @@ apply (rule impI, rule conjI, rule impI) apply (erule_tac obj = obj in co2sobj_some_caseD) -apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted) +apply (case_tac "pa = p", simp add:co2sobj.simps) apply (rule notI, simp) apply (rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI) apply (frule_tac obj = obj in co2sobj_closefd, simp) -apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1] +apply (auto simp add:co2sobj.simps split:t_object.splits if_splits)[1] apply (erule_tac x = obj in allE, simp add:co2sobj_closefd) apply (rule notI, simp add:co2sobj.simps split:option.splits) apply (case_tac "f = a", simp add:alive_simps) @@ -1331,10 +1291,10 @@ apply (simp add:co2sobj.simps) apply (rule notI, simp add:co2sobj.simps) apply (rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI) -apply (simp add:is_file_simps co2sobj_closefd tainted_eq_Tainted) +apply (simp add:is_file_simps co2sobj_closefd) apply (rule notI, simp add:co2sobj.simps) -apply (rule notI, simp add:co2sobj_closefd tainted_eq_Tainted) -apply (erule_tac x = f in allE, simp add:is_file_simps co2sobj.simps tainted_eq_Tainted) +apply (rule notI, simp add:co2sobj_closefd) +apply (erule_tac x = f in allE, simp add:is_file_simps co2sobj.simps) apply (rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI) apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps) apply (rule notI, simp add:co2sobj.simps split:option.splits)+ @@ -1346,23 +1306,23 @@ apply (rule notI, simp add:co2sobj.simps split:option.splits)+ apply (rule impI) apply (erule_tac obj = obj in co2sobj_some_caseD) -apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted) +apply (case_tac "pa = p", simp add:co2sobj.simps) apply (rule disjI2, rule notI, simp) apply (rule disjI2, rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI) apply (frule_tac obj = obj in co2sobj_closefd, simp) -apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1] +apply (auto simp add:co2sobj.simps split:t_object.splits if_splits)[1] apply (erule_tac x = obj in allE, simp add:co2sobj_closefd) apply (rule notI, simp add:co2sobj.simps split:option.splits) apply (case_tac "f = a", simp add:alive_simps) apply (case_tac "f \ same_inode_files s a", rule disjI1) apply (simp add:co2sobj_closefd split:if_splits option.splits t_sobject.splits) -apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_Tainted tainted_eq_Tainted) +apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted) apply (erule bexE, erule conjE, erule_tac x = "f''" in ballE, simp, simp) apply (rule disjI2, rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI) -apply (simp add:is_file_simps co2sobj_closefd tainted_eq_Tainted) +apply (simp add:is_file_simps co2sobj_closefd) apply (rule notI, simp add:co2sobj.simps) -apply (rule notI, simp add:co2sobj_closefd tainted_eq_Tainted) -apply (erule_tac x = f in allE, simp add:is_file_simps co2sobj.simps tainted_eq_Tainted) +apply (rule notI, simp add:co2sobj_closefd) +apply (erule_tac x = f in allE, simp add:is_file_simps co2sobj.simps) apply (rule disjI2, rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI) apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps) apply (rule notI, simp add:co2sobj.simps split:option.splits)+ @@ -1375,26 +1335,26 @@ apply (simp add:update_s2ss_sfile_del_def update_s2ss_obj_def split:if_splits) apply (erule conjE, erule disjE) -apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted) +apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps) apply (erule exE, erule conjE) -apply (case_tac "obj = O_file a", simp add:co2sobj.simps tainted_eq_Tainted) +apply (case_tac "obj = O_file a", simp add:co2sobj.simps) apply (case_tac "obj = O_proc p") apply (rule_tac x = obj' in exI, frule_tac obj = obj' in co2sobj_sproc_imp, erule exE) apply (frule_tac obj = obj' in alive_co2sobj_closefd3, simp+) apply (simp add:co2sobj_closefd) -apply (simp add:co2sobj.simps tainted_eq_Tainted) +apply (simp add:co2sobj.simps) apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+) apply (rule_tac x = obj in exI, simp add:co2sobj_closefd) -apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1] +apply (auto simp add:co2sobj.simps split:t_object.splits if_splits)[1] apply (erule conjE|erule exE|erule disjE)+ -apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted) +apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps) apply (erule conjE, erule exE, erule conjE) -apply (case_tac "obj = O_file a", simp add:co2sobj.simps tainted_eq_Tainted) +apply (case_tac "obj = O_file a", simp add:co2sobj.simps) apply (case_tac "obj = O_proc p") -apply (simp add:co2sobj.simps tainted_eq_Tainted) +apply (simp add:co2sobj.simps) apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+) apply (rule_tac x = obj in exI, simp add:co2sobj_closefd) -apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1] +apply (auto simp add:co2sobj.simps split:t_object.splits if_splits)[1] apply (erule conjE|erule exE|erule disjE)+ apply (drule same_inode_files_prop10, simp add:file_of_pfd_is_file, erule exE, erule conjE) apply (rule_tac x = "O_file f'" in exI) @@ -1402,26 +1362,26 @@ apply (frule_tac obj = "O_file f'" in co2sobj_closefd) apply (simp add:alive_simps)+ apply (frule_tac f = "f'" in is_file_has_sfile', simp, erule exE) -apply (simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted split:if_splits) +apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted split:if_splits) apply (rule impI, erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp) apply (erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp) apply (erule conjE, erule disjE) apply (rule_tac x = "O_proc p" in exI) -apply (simp add:co2sobj.simps tainted_eq_Tainted) +apply (simp add:co2sobj.simps) apply (erule exE, erule conjE) apply (case_tac "obj = O_proc p") apply (rule_tac x = "obj'" in exI, simp, frule_tac obj = obj' in co2sobj_sproc_imp, erule exE) apply (frule_tac obj = obj' in alive_co2sobj_closefd3, simp+) -apply (simp add:co2sobj_closefd tainted_eq_Tainted) -apply (simp add:co2sobj.simps tainted_eq_Tainted) -apply (case_tac "obj = O_file a", simp add:co2sobj.simps tainted_eq_Tainted) +apply (simp add:co2sobj_closefd) +apply (simp add:co2sobj.simps) +apply (case_tac "obj = O_file a", simp add:co2sobj.simps) apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+) apply (erule_tac obj = obj in co2sobj_some_caseD) apply (rule_tac x = obj in exI) apply (simp add:co2sobj_closefd) apply (case_tac "f = a", simp add:alive_simps) apply (case_tac "f \ same_inode_files s a") -apply (simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted) +apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted) apply (rule_tac x = obj in exI, simp add:co2sobj_closefd) apply (rule_tac x = obj in exI, simp add:co2sobj_closefd) apply (rule_tac x = obj in exI, simp add:co2sobj_closefd) @@ -1433,20 +1393,20 @@ apply (frule_tac obj = "O_file f'" in co2sobj_closefd) apply (simp add:alive_simps)+ apply (frule_tac f = "f'" in is_file_has_sfile', simp, erule exE) -apply (simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted split:if_splits) +apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted split:if_splits) apply (rule impI, erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp) apply (erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp) apply (erule conjE, erule disjE) apply (rule_tac x = "O_proc p" in exI) -apply (simp add:co2sobj.simps tainted_eq_Tainted) +apply (simp add:co2sobj.simps) apply (erule conjE, erule exE, erule conjE) -apply (case_tac "obj = O_proc p", simp add:co2sobj.simps tainted_eq_Tainted) -apply (case_tac "obj = O_file a", simp add:co2sobj.simps tainted_eq_Tainted) +apply (case_tac "obj = O_proc p", simp add:co2sobj.simps) +apply (case_tac "obj = O_file a", simp add:co2sobj.simps) apply (erule_tac obj = obj in co2sobj_some_caseD) apply (rule_tac x = obj in exI) apply (simp add:co2sobj_closefd) apply (case_tac "f \ same_inode_files s a") -apply (simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted) +apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted) apply (rule_tac x = obj in exI, simp add:co2sobj_closefd is_file_simps) apply (rule_tac x = obj in exI, simp add:co2sobj_closefd) apply (rule_tac x = obj in exI, simp add:co2sobj_closefd is_dir_simps) @@ -1459,40 +1419,40 @@ apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE) apply (simp) apply (case_tac "obj = O_proc p") -apply (simp add:co2sobj.simps tainted_eq_Tainted split:if_splits) +apply (simp add:co2sobj.simps split:if_splits) apply (rule disjI2, rule_tac x = obj in exI, erule conjE) apply (simp add:alive_co2sobj_closefd') apply (frule_tac obj = obj in co2sobj_closefd, simp, simp split:t_object.splits if_splits) apply (simp, erule disjE) -apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted) +apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps) apply (erule exE, erule conjE) apply (case_tac "obj = O_proc p") apply (rule_tac x = obj' in exI, simp add:alive_co2sobj_closefd1) apply (frule_tac obj = obj' in co2sobj_closefd, simp add:alive_co2sobj_closefd1) -apply (clarsimp split:t_object.splits if_splits option.splits simp:tainted_eq_Tainted co2sobj.simps) +apply (clarsimp split:t_object.splits if_splits option.splits simp:tainted_eq_tainted co2sobj.simps) apply (rule_tac x = obj in exI, simp add:alive_co2sobj_closefd1) apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd1) -apply (clarsimp split:t_object.splits if_splits option.splits simp:tainted_eq_Tainted co2sobj.simps) +apply (clarsimp split:t_object.splits if_splits option.splits simp:tainted_eq_tainted co2sobj.simps) apply (rule impI) apply (simp add:s2ss_def) apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE) apply (simp) apply (case_tac "obj = O_proc p") -apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted split:if_splits) +apply (rule disjI1, simp add:co2sobj.simps split:if_splits) apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp add:alive_co2sobj_closefd') apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd1) -apply (clarsimp split:t_object.splits if_splits option.splits simp:tainted_eq_Tainted co2sobj.simps) +apply (clarsimp split:t_object.splits if_splits option.splits simp:tainted_eq_tainted co2sobj.simps) apply (rule notI, erule_tac x = obj in allE, simp add:alive_co2sobj_closefd') apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd1) apply (clarsimp split:t_object.splits if_splits option.splits) apply (simp) apply (erule disjE) -apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted) +apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps) apply (erule exE|erule conjE)+ apply (rule_tac x = obj in exI) apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd1) apply (clarsimp split:t_object.splits if_splits option.splits - simp:tainted_eq_Tainted co2sobj.simps alive_co2sobj_closefd1) + simp:tainted_eq_tainted co2sobj.simps alive_co2sobj_closefd1) done lemma alive_co2sobj_unlink: @@ -1525,13 +1485,13 @@ apply (rule notI, simp, frule_tac obj = obj in co2sobj_sfile_imp, erule exE, simp) apply (frule_tac obj = obj in co2sobj_unlink, simp) apply (erule_tac x = fa in allE, simp add:is_file_simps) -apply (simp add:co2sobj.simps tainted_eq_Tainted) +apply (simp add:co2sobj.simps) apply (tactic {*my_setiff_tac 1*}) -apply (case_tac "obj = O_file f", simp add:co2sobj.simps tainted_eq_Tainted) +apply (case_tac "obj = O_file f", simp add:co2sobj.simps) apply (frule_tac alive_co2sobj_unlink, simp, simp) apply (frule_tac obj = obj in co2sobj_unlink, simp) apply (rule_tac x = obj in exI) -apply (simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits) +apply (simp add:co2sobj.simps split:t_object.splits if_splits) apply (rule impI|erule conjE|erule exE|rule conjI|erule bexE)+ defer @@ -1545,7 +1505,7 @@ apply (case_tac "fa \ same_inode_files s f") apply (rule disjI1) apply (simp add:co2sobj_unlink) -apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop split:if_splits) +apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop split:if_splits) apply (erule bexE, erule_tac x = f'' in ballE, simp, simp) apply (rule disjI2, simp, rule_tac x = obj in exI) apply (simp add:co2sobj_unlink is_file_simps) @@ -1556,7 +1516,7 @@ apply (drule same_inode_files_prop10, simp, erule exE, erule conjE) apply (rule_tac x = "O_file f'a" in exI, simp add:is_file_simps) apply (frule_tac obj = "O_file f'a" in co2sobj_unlink, simp add:same_inode_files_prop11 is_file_simps) -apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop +apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop is_file_simps same_inode_files_prop11 split:if_splits) apply (rule impI, erule bexE, erule_tac x = f'' in ballE, simp, simp) apply (erule bexE, erule_tac x = f'' in ballE, simp, simp) @@ -1566,13 +1526,13 @@ apply (case_tac "obj= O_file f") apply (rule_tac x = "O_file f'" in exI, simp add:is_file_simps) apply (frule_tac f' = f' in cf2sfiles_unlink, simp add:current_files_simps is_file_in_current) -apply (simp add:co2sobj.simps tainted_eq_Tainted) +apply (simp add:co2sobj.simps) apply (erule_tac obj = obj in co2sobj_some_caseD) apply (rule_tac x = obj in exI, simp add:co2sobj_unlink) apply (case_tac "fa \ same_inode_files s f") apply (rule_tac x = "O_file f'" in exI) apply (frule_tac f' = f' in cf2sfiles_unlink, simp add:current_files_simps is_file_in_current) -apply (simp add:co2sobj.simps tainted_eq_Tainted is_file_simps cf2sfiles_prop same_inodes_Tainted) +apply (simp add:co2sobj.simps is_file_simps cf2sfiles_prop same_inodes_tainted) apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_file_simps) apply (rule_tac x = obj in exI, simp add:co2sobj_unlink) apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_dir_simps) @@ -1591,12 +1551,12 @@ apply (case_tac "fa \ same_inode_files s f") apply (rule disjI1) apply (simp add:co2sobj_unlink) -apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop split:if_splits) +apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop split:if_splits) apply (erule bexE, erule_tac x = f'' in ballE, simp, simp) apply (rule disjI2, rule conjI, simp, rule_tac x = obj in exI) apply (simp add:co2sobj_unlink is_file_simps) -apply (rule notI, simp add:co2sobj_unlink tainted_eq_Tainted) -apply (erule_tac x = fa in allE, simp add:co2sobj.simps is_file_simps tainted_eq_Tainted) +apply (rule notI, simp add:co2sobj_unlink) +apply (erule_tac x = fa in allE, simp add:co2sobj.simps is_file_simps) apply (rule disjI2, rule conjI, simp, rule_tac x = obj in exI, simp add:co2sobj_unlink) apply (rule notI, simp add:co2sobj.simps split:option.splits) apply (rule disjI2, rule conjI, simp, rule_tac x = obj in exI, simp add:co2sobj_unlink is_dir_simps) @@ -1607,16 +1567,16 @@ apply (drule same_inode_files_prop10, simp, erule exE, erule conjE) apply (rule_tac x = "O_file f'" in exI, simp add:is_file_simps) apply (frule_tac obj = "O_file f'" in co2sobj_unlink, simp add:same_inode_files_prop11 is_file_simps) -apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop +apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop is_file_simps same_inode_files_prop11 split:if_splits) apply (rule impI, erule bexE, erule_tac x = f'' in ballE, simp, simp) apply (erule bexE, erule_tac x = f'' in ballE, simp, simp) apply (tactic {*my_setiff_tac 1*}, simp) -apply (case_tac "obj = O_file f", simp add:co2sobj.simps tainted_eq_Tainted) +apply (case_tac "obj = O_file f", simp add:co2sobj.simps) apply (erule_tac obj = obj in co2sobj_some_caseD) apply (rule_tac x = obj in exI, simp add:co2sobj_unlink) apply (case_tac "fa \ same_inode_files s f") -apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_Tainted tainted_eq_Tainted) +apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted) apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_file_simps) apply (rule_tac x = obj in exI, simp add:co2sobj_unlink) apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_dir_simps) @@ -1668,7 +1628,7 @@ apply (rule conjI, rule notI, simp add:same_inode_files_prop9) apply (rule impI, frule_tac f' = f' in cf2sfiles_unlink) apply (simp add:current_files_simps is_file_simps is_file_in_current) -apply (simp add:tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop) +apply (simp: same_inodes_tainted cf2sfiles_prop) apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_file_simps) apply (rule_tac x = obj in exI, simp add:co2sobj_unlink) apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_dir_simps) @@ -1687,7 +1647,7 @@ apply (frule same_inode_files_prop11, frule_tac f = f' in is_file_has_sfile', simp add:vd_cons, erule exE) apply (frule_tac obj = "O_file f'" in co2sobj_unlink, simp) apply (simp split:if_splits option.splits add:is_file_simps) -apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_Tainted tainted_eq_Tainted) +apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted) apply (auto split:t_sobject.splits)[1] apply (simp add:is_file_simps same_inode_files_prop11) apply (erule_tac obj = obj in co2sobj_some_caseD) @@ -1698,7 +1658,7 @@ apply (frule same_inode_files_prop11, frule_tac f = f' in is_file_has_sfile', simp add:vd_cons, erule exE) apply (frule_tac obj = "O_file f'" in co2sobj_unlink, simp) apply (simp split:if_splits option.splits add:is_file_simps) -apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_Tainted tainted_eq_Tainted) +apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_tainted) apply (auto split:t_sobject.splits)[1] apply (simp add:is_file_simps same_inode_files_prop11) apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_file_simps) @@ -1783,97 +1743,9 @@ where "update_s2ss_sfile s ss f sf \ if (\ f'. is_file s f' \ f' \ same_inode_files s f \ co2sobj s (O_file f') = co2sobj s (O_file f)) - then ss \ {S_file (cf2sfiles s f \ {sf}) (O_file f \ Tainted s)} - else ss - {S_file (cf2sfiles s f) (O_file f \ Tainted s)} - \ {S_file (cf2sfiles s f \ {sf}) (O_file f \ Tainted s)}" - -lemma s2ss_linkhard: "valid (LinkHard p f f' # s) \ s2ss (LinkHard p f f' # s) = ( - case (cf2sfile (LinkHard p f f' # s) f') of - Some sf \ update_s2ss_sfile s (s2ss s) f sf - | _ \ {})" -apply (frule vt_grant_os, frule vd_cons, clarsimp) -apply (split option.splits) -apply (rule conjI, rule impI, drule current_file_has_sfile', simp, simp add:current_files_simps) -apply (rule allI, rule impI) - -apply (simp add:update_s2ss_sfile_def) -apply (rule conjI, rule impI, erule exE, erule conjE, erule conjE) -apply (simp add:s2ss_def) -apply (tactic {*my_seteq_tac 1*}) -apply (case_tac "obj = O_file f'") -apply (rule disjI1, simp add:co2sobj.simps cf2sfiles_linkhard tainted_eq_Tainted - same_inode_files_linkhard split:if_splits) -apply (case_tac "O_file f' \ Tainted s") -apply (drule Tainted_in_current, simp, simp add:is_file_in_current alive.simps, simp) -apply (erule_tac obj = obj in co2sobj_some_caseD) -apply (rule disjI2, simp, rule_tac x = obj in exI) -apply (simp add:co2sobj_linkhard alive_linkhard) -apply (case_tac "fa \ same_inode_files s f") -apply (rule disjI1, simp add:co2sobj.simps cf2sfiles_linkhard tainted_eq_Tainted - same_inodes_Tainted split:if_splits) -apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_linkhard is_file_simps) -apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_linkhard) -apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_linkhard is_dir_simps) -apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_linkhard) -apply (tactic {*my_setiff_tac 1*}) -apply (rule_tac x = "O_file f" in exI) -apply (frule_tac obj = "O_file f" in co2sobj_linkhard) -apply (simp add:alive_linkhard) -apply (simp add:alive_linkhard same_inode_files_prop9 split:t_object.splits) -apply (tactic {*my_setiff_tac 1*}) -apply (case_tac "obj = O_file f'", simp add:alive_linkhard is_file_in_current) -apply (erule_tac obj = obj in co2sobj_some_caseD) -apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard) -apply (case_tac "fa \ same_inode_files s f") -apply (rule_tac x = "O_file f'a" in exI, simp add:co2sobj_linkhard alive_linkhard) -apply (rule conjI, rule impI, simp add:is_file_in_current) -apply (rule impI, simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted) -apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard) -apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard) -apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard) -apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard) - -apply (rule impI) -apply (simp add:s2ss_def) -apply (tactic {*my_seteq_tac 1*}) -apply (case_tac "obj = O_file f'", simp) -apply (rule disjI1, simp add:co2sobj.simps cf2sfiles_linkhard tainted_eq_Tainted - same_inode_files_linkhard split:if_splits) -apply (case_tac "O_file f' \ Tainted s") -apply (drule Tainted_in_current, simp, simp add:is_file_in_current alive.simps, simp) -apply (erule_tac obj = obj in co2sobj_some_caseD, simp) -apply (rule disjI2, rule conjI, rule_tac x = obj in exI) -apply (simp add:co2sobj_linkhard alive_linkhard) -apply (rule notI, simp add:co2sobj.simps split:option.splits) -apply (case_tac "fa \ same_inode_files s f") -apply (rule disjI1, simp add:co2sobj.simps cf2sfiles_linkhard tainted_eq_Tainted - same_inodes_Tainted split:if_splits) -apply (simp, rule disjI2, rule conjI, rule_tac x = obj in exI, simp add:co2sobj_linkhard is_file_simps) -apply (erule_tac x = fa in allE, rule notI) -apply (simp add:co2sobj_linkhard is_file_simps) -apply (simp add:co2sobj.simps tainted_eq_Tainted) -apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI, simp add:co2sobj_linkhard) -apply (rule notI, simp add:co2sobj.simps split:option.splits) -apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI, simp add:co2sobj_linkhard is_dir_simps) -apply (rule notI, simp add:co2sobj.simps split:option.splits) -apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI, simp add:co2sobj_linkhard) -apply (rule notI, simp add:co2sobj.simps split:option.splits) -apply (tactic {*my_setiff_tac 1*}) -apply (rule_tac x = "O_file f" in exI) -apply (frule_tac obj = "O_file f" in co2sobj_linkhard) -apply (simp add:alive_linkhard) -apply (simp add:alive_linkhard same_inode_files_prop9 split:t_object.splits) -apply (tactic {*my_setiff_tac 1*}) -apply (case_tac "obj = O_file f'", simp add:alive_linkhard is_file_in_current) -apply (erule_tac obj = obj in co2sobj_some_caseD) -apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard) -apply (case_tac "fa \ same_inode_files s f") -apply (simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted) -apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard) -apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard) -apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard) -apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard) -done + then ss \ {S_file (cf2sfiles s f \ {sf}) (O_file f \ tainted s)} + else ss - {S_file (cf2sfiles s f) (O_file f \ tainted s)} + \ {S_file (cf2sfiles s f \ {sf}) (O_file f \ tainted s)}" lemma same_inode_files_prop12: "is_file s f \ f \ same_inode_files s f " @@ -1889,7 +1761,7 @@ \ {S_file (cf2sfiles s f) True}" lemma s2ss_truncate: "valid (Truncate p f len # s) \ s2ss (Truncate p f len # s) = ( - if (O_file f \ Tainted s \ O_proc p \ Tainted s \ len > 0) + if (O_file f \ tainted s \ O_proc p \ tainted s \ len > 0) then update_s2ss_sfile_tainted s (s2ss s) f True else s2ss s)" apply (frule vt_grant_os, frule vd_cons, simp split:if_splits) @@ -1900,11 +1772,11 @@ apply (simp add:s2ss_def) apply (tactic {*my_seteq_tac 1*}) apply (case_tac "obj = O_file f") -apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted same_inode_files_prop12 cf2sfiles_other) +apply (rule disjI1, simp add:co2sobj.simps same_inode_files_prop12 cf2sfiles_other) apply (erule_tac obj = obj in co2sobj_some_caseD) apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_truncate alive_simps) apply (case_tac "fa \ same_inode_files s f") -apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted cf2sfiles_prop cf2sfiles_other) +apply (rule disjI1, simp add:co2sobj.simps cf2sfiles_prop cf2sfiles_other) apply (rule disjI2, simp, rule_tac x = obj in exI) apply (simp add:co2sobj_truncate is_file_simps) apply (rule disjI2, simp, rule_tac x = obj in exI) @@ -1915,14 +1787,14 @@ apply (simp add:co2sobj_truncate) apply (tactic {*my_setiff_tac 1*}) apply (rule_tac x = "O_file f" in exI) -apply (simp add:co2sobj.simps is_file_simps tainted_eq_Tainted cf2sfiles_other same_inode_files_prop12) +apply (simp add:co2sobj.simps is_file_simps cf2sfiles_other same_inode_files_prop12) apply (tactic {*my_setiff_tac 1*}) apply (erule_tac obj = obj in co2sobj_some_caseD) apply (rule_tac x = obj in exI, simp add:co2sobj_truncate) apply (case_tac "fa \ same_inode_files s f") apply (rule_tac x = "O_file f'" in exI) apply (auto simp:co2sobj_truncate is_file_simps is_dir_simps split:t_object.splits)[1] -apply (simp add:co2sobj.simps same_inodes_Tainted tainted_eq_Tainted cf2sfiles_prop) +apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop) apply (rule_tac x = obj in exI, simp add:co2sobj_truncate is_file_simps) apply (rule_tac x = obj in exI, simp add:co2sobj_truncate) apply (rule_tac x = obj in exI, simp add:co2sobj_truncate is_dir_simps) @@ -1932,12 +1804,12 @@ apply (simp add:s2ss_def) apply (tactic {*my_seteq_tac 1*}) apply (case_tac "obj = O_file f") -apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted same_inode_files_prop12 cf2sfiles_other) +apply (rule disjI1, simp add:co2sobj.simps same_inode_files_prop12 cf2sfiles_other) apply (erule_tac obj = obj in co2sobj_some_caseD) apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI, simp add:co2sobj_truncate alive_simps) apply (rule notI, simp add:co2sobj.simps split:option.splits) apply (case_tac "fa \ same_inode_files s f") -apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted cf2sfiles_prop cf2sfiles_other) +apply (rule disjI1, simp add:co2sobj.simps cf2sfiles_prop cf2sfiles_other) apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI) apply (simp add:co2sobj_truncate is_file_simps) apply (rule notI, simp add:co2sobj_truncate is_file_simps) @@ -1954,12 +1826,12 @@ apply (rule notI, simp add:co2sobj.simps split:option.splits) apply (tactic {*my_setiff_tac 1*}) apply (rule_tac x = "O_file f" in exI) -apply (simp add:co2sobj.simps is_file_simps tainted_eq_Tainted cf2sfiles_other same_inode_files_prop12) +apply (simp add:co2sobj.simps is_file_simps cf2sfiles_other same_inode_files_prop12) apply (tactic {*my_setiff_tac 1*}) apply (erule_tac obj = obj in co2sobj_some_caseD) apply (rule_tac x = obj in exI, simp add:co2sobj_truncate) apply (case_tac "fa \ same_inode_files s f") -apply (simp add:co2sobj.simps same_inodes_Tainted tainted_eq_Tainted cf2sfiles_prop) +apply (simp add:co2sobj.simps same_inodes_tainted cf2sfiles_prop) apply (rule_tac x = obj in exI, simp add:co2sobj_truncate is_file_simps) apply (rule_tac x = obj in exI, simp add:co2sobj_truncate) apply (rule_tac x = obj in exI, simp add:co2sobj_truncate is_dir_simps) @@ -1969,13 +1841,13 @@ apply (tactic {*my_seteq_tac 1*}) apply (rule_tac x = obj in exI) apply (simp add:alive_simps co2sobj_truncate) -apply (simp split:t_object.splits if_splits add:co2sobj.simps tainted_eq_Tainted) -apply (case_tac "O_proc p \ Tainted s", simp add:same_inodes_Tainted) +apply (simp split:t_object.splits if_splits add:co2sobj.simps) +apply (case_tac "O_proc p \ tainted s", simp add:same_inodes_tainted) apply simp apply (tactic {*my_setiff_tac 1*}) apply (rule_tac x = obj in exI) apply (simp add:alive_simps co2sobj_truncate) -apply (auto split:t_object.splits if_splits simp:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted) +apply (auto split:t_object.splits if_splits simp:co2sobj.simps same_inodes_tainted) done lemma s2ss_createmsgq: "valid (CreateMsgq p q # s) \ s2ss (CreateMsgq p q # s) = @@ -2116,17 +1988,17 @@ declare Product_Type.split_paired_Ex Product_Type.split_paired_All [simp del] lemma s2ss_shm_no_bk_elim': - "\x \ s2ss_shm_no_backup s pfrom; co2sobj s (O_proc p) = Some x; O_proc p \ Tainted s; + "\x \ s2ss_shm_no_backup s pfrom; co2sobj s (O_proc p) = Some x; O_proc p \ tainted s; valid s; info_flow_shm s pfrom p\ \ \ p'. \ info_flow_shm s pfrom p' \ p' \ current_procs s \ co2sobj s (O_proc p') = Some x" -apply (auto simp:s2ss_shm_no_backup_def co2sobj.simps tainted_eq_Tainted split:option.splits) +apply (auto simp:s2ss_shm_no_backup_def co2sobj.simps split:option.splits) apply (erule_tac x = p in allE, auto) apply (rule_tac x = p' in exI, auto) done lemma s2ss_recvmsg: "valid (RecvMsg p q m # s) \ s2ss (RecvMsg p q m # s) = ( case (cq2smsgq s q, cq2smsgq (RecvMsg p q m # s) q) of - (Some sq, Some sq') \ if (O_msg q m \ Tainted s \ O_proc p \ Tainted s) + (Some sq, Some sq') \ if (O_msg q m \ tainted s \ O_proc p \ tainted s) then update_s2ss_obj s (update_s2ss_shm s p) (O_msgq q) (S_msgq sq) (S_msgq sq') else update_s2ss_obj s (s2ss s) (O_msgq q) (S_msgq sq) (S_msgq sq') | _ \ {})" @@ -2175,7 +2047,7 @@ split:t_object.splits if_splits option.splits) apply (auto simp:co2sobj.simps is_file_simps is_dir_simps)[1] apply (erule_tac obj = obj in co2sobj_some_caseD) -apply (case_tac "info_flow_shm s p pa \ O_proc pa \ Tainted s") +apply (case_tac "info_flow_shm s p pa \ O_proc pa \ tainted s") apply (drule_tac p = pa in s2ss_shm_no_bk_elim', simp+) apply (erule exE|erule conjE)+ apply (rule_tac x = "O_proc p'" in exI) @@ -2184,7 +2056,7 @@ apply (case_tac "info_flow_shm s p pa", simp) apply (frule_tac obj = obj in co2sobj_recvmsg, simp+) apply (case_tac "cp2sproc s pa", simp add:co2sobj.simps) -apply (simp, simp add:co2sobj.simps tainted_eq_Tainted) +apply (simp, simp add:co2sobj.simps) apply (simp, frule_tac obj = obj in co2sobj_recvmsg, simp+) apply (rule_tac x = obj in exI, simp add:co2sobj_recvmsg alive_simps) apply (rule_tac x = obj in exI) @@ -2203,7 +2075,7 @@ apply (rule disjI1, simp add:co2sobj.simps) apply (rule disjI2, simp, rule_tac x = obj in exI) apply (simp add:co2sobj_recvmsg is_file_simps is_dir_simps split:t_object.splits if_splits option.splits) -apply (simp add:co2sobj.simps tainted_eq_Tainted info_flow_shm_Tainted) +apply (simp add:co2sobj.simps info_flow_shm_tainted) apply (simp add:co2sobj.simps) apply (simp add:co2sobj.simps) apply (case_tac "msgs_of_queue s q", simp, simp) @@ -2219,7 +2091,7 @@ apply (rule_tac x = obj in exI) apply (simp add:co2sobj_recvmsg is_file_simps is_dir_simps alive_recvmsg split:t_object.splits if_splits option.splits) -apply (auto simp:co2sobj.simps is_file_simps is_dir_simps tainted_eq_Tainted info_flow_shm_Tainted)[1] +apply (auto simp:co2sobj.simps is_file_simps is_dir_simps info_flow_shm_tainted)[1] apply (tactic {*my_clarify_tac 1*}) apply (tactic {*my_seteq_tac 1*}) @@ -2228,14 +2100,14 @@ apply (rule disjI2) apply (erule_tac obj = obj in co2sobj_some_caseD) apply (case_tac "info_flow_shm s p pa") -apply (case_tac "O_proc pa \ Tainted s") +apply (case_tac "O_proc pa \ tainted s") apply (rule DiffI, rule UnI1, simp) apply (rule_tac x = obj in exI) apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp split:option.splits) -apply (simp add:co2sobj.simps tainted_eq_Tainted) +apply (simp add:co2sobj.simps) apply (erule s2ss_shm_no_bk_intro2, simp, simp) apply (rule DiffI, rule UnI2, rule CollectI) -apply (simp only:co2sobj.simps tainted_eq_Tainted split:option.splits, simp) +apply (simp only:co2sobj.simps split:option.splits, simp) apply (rule_tac x = ab in exI, simp) apply (rule_tac x = pa in exI, simp add:cp2sproc_other) apply (rule s2ss_shm_no_bk_intro2, simp, simp, simp) @@ -2272,7 +2144,7 @@ split:t_object.splits if_splits option.splits) apply (auto simp:co2sobj.simps is_file_simps is_dir_simps)[1] apply (erule_tac obj = obj in co2sobj_some_caseD) -apply (case_tac "info_flow_shm s p pa \ O_proc pa \ Tainted s") +apply (case_tac "info_flow_shm s p pa \ O_proc pa \ tainted s") apply (drule_tac p = pa in s2ss_shm_no_bk_elim', simp+) apply (erule exE|erule conjE)+ apply (rule_tac x = "O_proc p'" in exI) @@ -2281,7 +2153,7 @@ apply (case_tac "info_flow_shm s p pa", simp) apply (frule_tac obj = obj in co2sobj_recvmsg, simp+) apply (case_tac "cp2sproc s pa", simp add:co2sobj.simps) -apply (simp, simp add:co2sobj.simps tainted_eq_Tainted) +apply (simp, simp add:co2sobj.simps) apply (simp, frule_tac obj = obj in co2sobj_recvmsg, simp+) apply (rule_tac x = obj in exI, simp add:co2sobj_recvmsg alive_simps) apply (rule_tac x = obj in exI) @@ -2301,7 +2173,7 @@ apply (rule_tac x = obj in exI) apply (simp add:co2sobj_recvmsg is_file_simps is_dir_simps alive_recvmsg split:t_object.splits if_splits option.splits) -apply (simp add:co2sobj.simps tainted_eq_Tainted info_flow_shm_Tainted) +apply (simp add:co2sobj.simps info_flow_shm_tainted) apply (simp add:co2sobj_recvmsg) apply (simp add:alive_recvmsg split:if_splits) apply (erule_tac x = obj in allE, simp split:t_object.splits if_splits option.splits) @@ -2322,7 +2194,7 @@ apply (simp add:alive_recvmsg, rule notI, simp add:co2sobj.simps) apply (rule conjI) apply (simp add:alive_recvmsg, rule notI, simp add:co2sobj.simps) -apply (auto simp:co2sobj.simps tainted_eq_Tainted split:t_object.splits option.splits if_splits)[1] +apply (auto simp:co2sobj.simps split:t_object.splits option.splits if_splits)[1] apply (tactic {*my_clarify_tac 1*}) apply (tactic {*my_seteq_tac 1*}) @@ -2331,14 +2203,14 @@ apply (rule disjI2) apply (erule_tac obj = obj in co2sobj_some_caseD) apply (case_tac "info_flow_shm s p pa") -apply (case_tac "O_proc pa \ Tainted s") +apply (case_tac "O_proc pa \ tainted s") apply (rule DiffI, rule UnI1, simp) apply (rule_tac x = obj in exI) apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp split:option.splits) -apply (simp add:co2sobj.simps tainted_eq_Tainted) +apply (simp add:co2sobj.simps) apply (erule s2ss_shm_no_bk_intro2, simp, simp) apply (rule DiffI, rule UnI2, rule CollectI) -apply (simp only:co2sobj.simps tainted_eq_Tainted split:option.splits, simp) +apply (simp only:co2sobj.simps split:option.splits, simp) apply (rule_tac x = ab in exI, simp) apply (rule_tac x = pa in exI, simp add:cp2sproc_other) apply (rule s2ss_shm_no_bk_intro2, simp, simp, simp) @@ -2374,7 +2246,7 @@ split:t_object.splits if_splits option.splits) apply (auto simp:co2sobj.simps is_file_simps is_dir_simps)[1] apply (erule_tac obj = obj in co2sobj_some_caseD) -apply (case_tac "info_flow_shm s p pa \ O_proc pa \ Tainted s") +apply (case_tac "info_flow_shm s p pa \ O_proc pa \ tainted s") apply (drule_tac p = pa in s2ss_shm_no_bk_elim', simp+) apply (erule exE|erule conjE)+ apply (rule_tac x = "O_proc p'" in exI) @@ -2383,7 +2255,7 @@ apply (case_tac "info_flow_shm s p pa", simp) apply (frule_tac obj = obj in co2sobj_recvmsg, simp+) apply (case_tac "cp2sproc s pa", simp add:co2sobj.simps) -apply (simp, simp add:co2sobj.simps tainted_eq_Tainted) +apply (simp, simp add:co2sobj.simps) apply (simp, frule_tac obj = obj in co2sobj_recvmsg, simp+) apply (rule_tac x = obj in exI, simp add:co2sobj_recvmsg alive_simps) apply (rule_tac x = obj in exI) @@ -2403,7 +2275,7 @@ apply (rule_tac x = obj in exI) apply (simp add:co2sobj_recvmsg is_file_simps is_dir_simps alive_recvmsg split:t_object.splits if_splits option.splits) -apply (simp add:co2sobj.simps tainted_eq_Tainted info_flow_shm_Tainted) +apply (simp add:co2sobj.simps info_flow_shm_tainted) apply (tactic {*my_setiff_tac 1*}) apply (rule_tac x = "O_msgq q" in exI) apply (simp add:co2sobj.simps) @@ -2418,7 +2290,7 @@ apply (simp add:alive_recvmsg, rule notI, simp add:co2sobj.simps) apply (rule conjI) apply (simp add:alive_recvmsg, rule notI, simp add:co2sobj.simps) -apply (auto simp:co2sobj.simps tainted_eq_Tainted split:t_object.splits option.splits if_splits)[1] +apply (auto simp:co2sobj.simps split:t_object.splits option.splits if_splits)[1] apply (tactic {*my_clarify_tac 1*}) apply (tactic {*my_seteq_tac 1*}) @@ -2427,15 +2299,15 @@ apply (rule disjI2) apply (erule_tac obj = obj in co2sobj_some_caseD) apply (case_tac "info_flow_shm s p pa") -apply (case_tac "O_proc pa \ Tainted s") +apply (case_tac "O_proc pa \ tainted s") apply (rule DiffI, rule DiffI, rule UnI1, simp) apply (rule_tac x = obj in exI) apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp split:option.splits) -apply (simp add:co2sobj.simps tainted_eq_Tainted) +apply (simp add:co2sobj.simps) apply (erule s2ss_shm_no_bk_intro2, simp, simp) apply (simp, rule notI, simp add:co2sobj.simps split:option.splits) apply (rule DiffI, rule DiffI, rule UnI2, rule CollectI) -apply (simp only:co2sobj.simps tainted_eq_Tainted split:option.splits, simp) +apply (simp only:co2sobj.simps split:option.splits, simp) apply (rule_tac x = ab in exI, simp) apply (rule_tac x = pa in exI, simp add:cp2sproc_other) apply (rule s2ss_shm_no_bk_intro2, simp, simp, simp) @@ -2475,7 +2347,7 @@ apply (case_tac "obj = O_msgq q") apply (simp add:co2sobj.simps) apply (erule_tac obj = obj in co2sobj_some_caseD) -apply (case_tac "info_flow_shm s p pa \ O_proc pa \ Tainted s") +apply (case_tac "info_flow_shm s p pa \ O_proc pa \ tainted s") apply (drule_tac p = pa in s2ss_shm_no_bk_elim', simp+) apply (erule exE|erule conjE)+ apply (rule_tac x = "O_proc p'" in exI) @@ -2484,7 +2356,7 @@ apply (case_tac "info_flow_shm s p pa", simp) apply (frule_tac obj = obj in co2sobj_recvmsg, simp+) apply (case_tac "cp2sproc s pa", simp add:co2sobj.simps) -apply (simp, simp add:co2sobj.simps tainted_eq_Tainted) +apply (simp, simp add:co2sobj.simps) apply (simp, frule_tac obj = obj in co2sobj_recvmsg, simp+) apply (rule_tac x = obj in exI, simp add:co2sobj_recvmsg alive_simps) apply (rule_tac x = obj in exI) @@ -2504,7 +2376,7 @@ apply (rule_tac x = obj in exI) apply (simp add:co2sobj_recvmsg is_file_simps is_dir_simps alive_recvmsg split:t_object.splits if_splits option.splits) -apply (simp add:co2sobj.simps tainted_eq_Tainted info_flow_shm_Tainted) +apply (simp add:co2sobj.simps info_flow_shm_tainted) apply (rule notI, simp) apply (frule co2sobj_smsgq_imp, erule exE, simp) apply (simp add:co2sobj_recvmsg) @@ -2521,7 +2393,7 @@ apply (simp add:alive_recvmsg, rule notI, simp add:co2sobj.simps) apply (rule conjI) apply (simp add:alive_recvmsg, rule notI, simp add:co2sobj.simps) -apply (auto simp:co2sobj.simps tainted_eq_Tainted intro: info_flow_shm_Tainted +apply (auto simp:co2sobj.simps intro: info_flow_shm_tainted split:t_object.splits option.splits if_splits)[1] done diff -r 271e9818b6f6 -r 99af1986e1e0 simple_selinux/Sectxt_prop.thy --- a/simple_selinux/Sectxt_prop.thy Mon Dec 02 10:52:40 2013 +0800 +++ b/simple_selinux/Sectxt_prop.thy Tue Dec 03 22:42:48 2013 +0800 @@ -31,14 +31,13 @@ have p6: "\ p fd. fd \ current_proc_fds s p \ \ t. type_of_obj s (O_fd p fd) = Some t" by (auto intro:a1) have p7: "\ n. n \ init_nodes \ \ t. type_of_obj s (O_node n) = Some t" by (auto intro:a1) - have p8: "\ h. h \ current_shms s \ \ t. type_of_obj s (O_shm h) = Some t" by (auto intro:a1) have p9: "\ q. q \ current_msgqs s \ \ t. type_of_obj s (O_msgq q) = Some t" by (auto intro:a1) have p10: "\ q m. \m \ set (msgs_of_queue s q); q \ current_msgqs s\ \ \ t. type_of_obj s (O_msg q m) = Some t" by (auto intro:a1) show ?case using a5 a2 a4 a3 apply (case_tac e) apply (auto split:option.splits t_object.splits if_splits t_socket_type.splits - dest!:a1' intro:a1 intro:p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 simp:alive_simps) + dest!:a1' intro:a1 p1 p2 p3 p4 p5 p6 p7 p9 p10 simp:alive_simps) apply (frule_tac p = nat1 in file_fds_subset_pfds) apply (rule a1, auto) done @@ -71,14 +70,13 @@ have p6: "\ p fd. fd \ current_proc_fds s p \ \ t. user_of_obj s (O_fd p fd) = Some t" by (auto intro:a1) have p7: "\ n. n \ init_nodes \ \ t. user_of_obj s (O_node n) = Some t" by (auto intro:a1) - have p8: "\ h. h \ current_shms s \ \ t. user_of_obj s (O_shm h) = Some t" by (auto intro:a1) have p9: "\ q. q \ current_msgqs s \ \ t. user_of_obj s (O_msgq q) = Some t" by (auto intro:a1) have p10: "\ q m. \m \ set (msgs_of_queue s q); q \ current_msgqs s\ \ \ t. user_of_obj s (O_msg q m) = Some t" by (auto intro:a1) show ?case using a5 a2 a4 a3 apply (case_tac e) apply (auto split:option.splits t_object.splits if_splits t_socket_type.splits - dest!:a1' intro:a1 intro:p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 simp:alive_simps) + dest!:a1' intro:a1 intro:p1 p2 p3 p4 p5 p6 p7 p9 p10 simp:alive_simps) apply (frule_tac p = nat1 in file_fds_subset_pfds) apply (rule a1, auto) done @@ -131,12 +129,6 @@ lemma init_node_has_type': "\type_of_obj s (O_node n) = None; valid s\ \ n \ init_nodes" by (auto intro:notI dest:init_node_has_type) -lemma current_shm_has_type: "\h \ current_shms s; valid s\ \ \ t. type_of_obj s (O_shm h) = Some t" -by (auto intro:alive_obj_has_type) - -lemma current_shm_has_type': "\type_of_obj s (O_shm h) = None; valid s\ \ h \ current_shms s" -by (auto intro:notI dest:current_shm_has_type) - lemma current_msgq_has_type: "\q \ current_msgqs s; valid s\ \ \ t. type_of_obj s (O_msgq q) = Some t" by (auto intro:alive_obj_has_type) @@ -152,11 +144,11 @@ by (auto dest!:current_msg_has_type) lemmas current_has_type = alive_obj_has_type current_proc_has_type is_file_has_type is_dir_has_type - is_tcp_has_type is_udp_has_type current_fd_has_type init_node_has_type current_shm_has_type + is_tcp_has_type is_udp_has_type current_fd_has_type init_node_has_type current_msgq_has_type current_msg_has_type lemmas current_has_type' = alive_obj_has_type' current_proc_has_type' is_file_has_type' is_dir_has_type' - is_tcp_has_type' is_udp_has_type' current_fd_has_type' init_node_has_type' current_shm_has_type' + is_tcp_has_type' is_udp_has_type' current_fd_has_type' init_node_has_type' current_msgq_has_type' current_msg_has_type' lemma alive_obj_has_user': "\user_of_obj s obj = None; valid s\ \ \ alive s obj" @@ -206,12 +198,6 @@ lemma init_node_has_user': "\user_of_obj s (O_node n) = None; valid s\ \ n \ init_nodes" by (auto intro:notI dest:init_node_has_user) -lemma current_shm_has_user: "\h \ current_shms s; valid s\ \ \ t. user_of_obj s (O_shm h) = Some t" -by (auto intro:alive_obj_has_user) - -lemma current_shm_has_user': "\user_of_obj s (O_shm h) = None; valid s\ \ h \ current_shms s" -by (auto intro:notI dest:current_shm_has_user) - lemma current_msgq_has_user: "\q \ current_msgqs s; valid s\ \ \ t. user_of_obj s (O_msgq q) = Some t" by (auto intro:alive_obj_has_user) @@ -227,11 +213,11 @@ by (auto dest!:current_msg_has_user) lemmas current_has_user = alive_obj_has_user current_proc_has_user is_file_has_user is_dir_has_user - is_tcp_has_user is_udp_has_user current_fd_has_user init_node_has_user current_shm_has_user + is_tcp_has_user is_udp_has_user current_fd_has_user init_node_has_user current_msgq_has_user current_msg_has_user lemmas current_has_user' = alive_obj_has_user' current_proc_has_user' is_file_has_user' is_dir_has_user' - is_tcp_has_user' is_udp_has_user' current_fd_has_user' init_node_has_user' current_shm_has_user' + is_tcp_has_user' is_udp_has_user' current_fd_has_user' init_node_has_user' current_msgq_has_user' current_msg_has_user' lemma current_proc_has_role: @@ -334,15 +320,6 @@ lemma init_node_has_sec'': "\n \ init_nodes; valid s\ \ \ u r t. sectxt_of_obj s (O_node n) = Some (u,r,t)" by (drule init_node_has_sec, simp+) -lemma current_shm_has_sec: "\h \ current_shms s; valid s\ \ \ sec. sectxt_of_obj s (O_shm h) = Some sec" -by (rule alive_obj_has_sec, simp+) - -lemma current_shm_has_sec': "\sectxt_of_obj s (O_shm h) = None; valid s\ \ h \ current_shms s" -by (auto intro:notI dest:current_shm_has_sec) - -lemma current_shm_has_sec'': "\h \ current_shms s; valid s\ \ \ u r t. sectxt_of_obj s (O_shm h) = Some (u,r,t)" -by (drule current_shm_has_sec, simp+) - lemma current_msgq_has_sec: "\q \ current_msgqs s; valid s\ \ \ sec. sectxt_of_obj s (O_msgq q) = Some sec" by (rule alive_obj_has_sec, simp+) @@ -366,15 +343,15 @@ by (drule current_msg_has_sec, simp+) lemmas current_has_sec = alive_obj_has_sec current_proc_has_sec is_file_has_sec is_dir_has_sec - is_tcp_has_sec is_udp_has_sec current_fd_has_sec init_node_has_sec current_shm_has_sec + is_tcp_has_sec is_udp_has_sec current_fd_has_sec init_node_has_sec current_msgq_has_sec current_msg_has_sec lemmas current_has_sec' = alive_obj_has_sec' current_proc_has_sec' is_file_has_sec' is_dir_has_sec' - is_tcp_has_sec' is_udp_has_sec' current_fd_has_sec' init_node_has_sec' current_shm_has_sec' + is_tcp_has_sec' is_udp_has_sec' current_fd_has_sec' init_node_has_sec' current_msgq_has_sec' current_msg_has_sec' lemmas current_has_sec'' = alive_obj_has_sec'' current_proc_has_sec'' is_file_has_sec'' is_dir_has_sec'' - is_tcp_has_sec'' is_udp_has_sec'' current_fd_has_sec'' init_node_has_sec'' current_shm_has_sec'' + is_tcp_has_sec'' is_udp_has_sec'' current_fd_has_sec'' init_node_has_sec'' current_msgq_has_sec'' current_msg_has_sec'' (************ root sec remains ************) @@ -443,7 +420,7 @@ done lemma sec_clone: - "valid (Clone p p' fds shms # s) \ sectxt_of_obj (Clone p p' fds shms # s) = (\ obj. + "valid (Clone p p' fds # s) \ sectxt_of_obj (Clone p p' fds # s) = (\ obj. case obj of O_proc p'' \ if (p'' = p') then sectxt_of_obj s (O_proc p) else sectxt_of_obj s obj @@ -498,20 +475,6 @@ dest!:current_has_type' current_proc_has_role' current_has_user') done -lemma sec_linkhard: - "valid (LinkHard p f f' # s) \ sectxt_of_obj (LinkHard p f f' # s) = - (sectxt_of_obj s) (O_file f' := - (case parent f' of - None \ None - | Some pf \ (case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_dir pf)) of - (Some psec, Some pfsec) \ Some (fst psec, R_object, - type_transition ((snd o snd) psec) ((snd o snd) pfsec) C_file True) - | _ \ None)))" -apply (rule ext, frule vd_cons, frule vt_grant_os, case_tac x) -apply (auto simp:sectxt_of_obj_def split:option.splits if_splits - dest!:current_has_type' current_proc_has_role' current_has_user') -done - lemma sec_createmsgq: "valid (CreateMsgq p q # s) \ sectxt_of_obj (CreateMsgq p q # s) = (sectxt_of_obj s) (O_msgq q := (case (sectxt_of_obj s (O_proc p)) of @@ -533,16 +496,6 @@ dest!:current_has_type' current_proc_has_role' current_has_user') done -lemma sec_createshm: - "valid (CreateShM p h # s) \ sectxt_of_obj (CreateShM p h # s) = (sectxt_of_obj s) (O_shm h := - case (sectxt_of_obj s (O_proc p)) of - Some psec \ Some (fst psec, R_object, (snd o snd) psec) - | _ \ None)" -apply (rule ext, frule vd_cons, frule vt_grant_os, case_tac x) -apply (auto simp:sectxt_of_obj_def split:option.splits if_splits - dest!:current_has_type' current_proc_has_role' current_has_user') -done - lemma sec_createsock: "valid (CreateSock p af st fd inum # s) \ sectxt_of_obj (CreateSock p af st fd inum # s) = (\ obj. case obj of @@ -588,11 +541,10 @@ lemma sec_others : "\valid (e # s); - \ p p' fds shms. e \ Clone p p' fds shms; + \ p p' fds. e \ Clone p p' fds; \ p f fds. e \ Execve p f fds; \ p f flags fd opt. e \ Open p f flags fd opt; \ p f inum. e \ Mkdir p f inum; - \ p f f'. e \ LinkHard p f f'; \ p q. e \ CreateMsgq p q; \ p q m. e \ SendMsg p q m; \ p h. e \ CreateShM p h; @@ -648,18 +600,6 @@ "valid (RemoveMsgq p q # s) \ sectxt_of_obj (RemoveMsgq p q # s) = sectxt_of_obj s" by (auto dest!:sec_others) -lemma sec_attach: - "valid (Attach p h flag # s) \ sectxt_of_obj (Attach p h flag # s) = sectxt_of_obj s" -by (auto dest!:sec_others) - -lemma sec_detach: - "valid (Detach p h # s) \ sectxt_of_obj (Detach p h # s) = sectxt_of_obj s" -by (auto dest!:sec_others) - -lemma sec_deleteshm: - "valid (DeleteShM p h # s) \ sectxt_of_obj (DeleteShM p h # s) = sectxt_of_obj s" -by (auto dest!:sec_others) - lemma sec_bind: "valid (Bind p fd addr # s) \ sectxt_of_obj (Bind p fd addr # s) = sectxt_of_obj s" by (auto dest!:sec_others) @@ -684,11 +624,10 @@ "valid (Shutdown p fd how # s) \ sectxt_of_obj (Shutdown p fd how # s) = sectxt_of_obj s" by (auto dest!:sec_others) -lemmas sectxt_of_obj_simps = sec_execve sec_open sec_mkdir sec_linkhard sec_createmsgq sec_sendmsg - sec_createshm sec_createsock sec_accept sec_clone sec_kill sec_ptrace sec_exit sec_readfile +lemmas sectxt_of_obj_simps = sec_execve sec_open sec_mkdir sec_createmsgq sec_sendmsg + sec_createsock sec_accept sec_clone sec_kill sec_ptrace sec_exit sec_readfile sec_writefile sec_closefd sec_unlink sec_Rmdir sec_truncate sec_recvmsg sec_removemsgq - sec_attach sec_detach sec_deleteshm sec_bind sec_connect sec_listen sec_sendsock - sec_recvsock sec_shutdown + sec_bind sec_connect sec_listen sec_sendsock sec_recvsock sec_shutdown (* init_sectxt_prop *) (**************** get_parentfs_ctxts simpset **************) diff -r 271e9818b6f6 -r 99af1986e1e0 simple_selinux/Tainted_prop.thy --- a/simple_selinux/Tainted_prop.thy Mon Dec 02 10:52:40 2013 +0800 +++ b/simple_selinux/Tainted_prop.thy Tue Dec 03 22:42:48 2013 +0800 @@ -6,217 +6,50 @@ context tainting begin -lemma valid_Tainted_obj: - "\obj \ Tainted s; valid s\ \ (\ f. obj \ O_dir f) \ (\ q. obj \ O_msgq q) \ (\ h. obj \ O_shm h) \ (\ p fd. obj \ O_fd p fd) \ (\ s. obj \ O_tcp_sock s) \ (\ s. obj \ O_udp_sock s)" -apply (induct s, simp, drule seeds_in_init, case_tac obj, simp+) +lemma valid_tainted_obj: + "\obj \ tainted s; valid s\ \ (\ f. obj \ O_dir f) \ (\ q. obj \ O_msgq q) \ (\ p fd. obj \ O_fd p fd) \ (\ s. obj \ O_tcp_sock s) \ (\ s. obj \ O_udp_sock s)" +apply (induct s, simp) +apply (drule seeds_in_init, case_tac obj, simp+) apply (frule vd_cons, frule vt_grant_os, case_tac a) apply (auto split:if_splits option.splits) done -lemma Tainted_in_current: - "\obj \ Tainted s; valid s\ \ alive s obj" +lemma dir_not_tainted: "\O_dir f \ tainted s; valid s\ \ False" +by (auto dest!:valid_tainted_obj) + +lemma msgq_not_tainted: "\O_msgq q \ tainted s; valid s\ \ False" +by (auto dest:valid_tainted_obj) + +lemma tainted_in_current: + "\obj \ tainted s; valid s\ \ alive s obj" apply (induct s, simp) apply (drule seeds_in_init, case_tac obj, simp_all add:is_file_nil) -apply (frule vd_cons, frule valid_Tainted_obj, simp, frule vt_grant_os, case_tac a) -apply (auto simp:alive_simps split:if_splits option.splits t_object.splits - intro:same_inode_files_prop1 procs_of_shm_prop2 - dest:info_shm_flow_in_procs) -apply (auto simp:same_inode_files_def is_file_def split:if_splits) -done - -lemma Tainted_proc_in_current: - "\O_proc p \ Tainted s; valid s\ \ p \ current_procs s" -by (drule Tainted_in_current, simp+) - - -lemma info_flow_shm_Tainted: - "\O_proc p \ Tainted s; info_flow_shm s p p'; valid s\ \ O_proc p' \ Tainted s" -proof (induct s arbitrary:p p') - case Nil - thus ?case by (simp add:flow_shm_in_seeds) -next - case (Cons e s) - hence p1: "O_proc p \ Tainted (e # s)" and p2: "info_flow_shm (e # s) p p'" and p3: "valid (e # s)" - and p4: "\ p p'. \O_proc p \ Tainted s; info_flow_shm s p p'\ \ O_proc p' \ Tainted s" - and p5: "valid s" and p6: "os_grant s e" - by (auto dest:vd_cons intro:vd_cons vt_grant_os) - have p4': - "\ p p' h flag. \O_proc p \ Tainted s; (p, SHM_RDWR) \ procs_of_shm s h; (p', flag) \ procs_of_shm s h\ - \ O_proc p' \ Tainted s" - by (rule p4, auto simp:info_flow_shm_def one_flow_shm_def procs_of_shm_prop2 p5) - from p2 p3 have p7: "p \ current_procs (e # s)" and p8: "p' \ current_procs (e # s)" - by (auto dest:info_shm_flow_in_procs) - show ?case - proof (cases "self_shm s p p'") - case True with p1 show ?thesis by simp - next - case False - with p1 p2 p5 p6 p7 p8 p3 show ?thesis - apply (case_tac e)(* - prefer 7 - apply (simp add:info_flow_shm_simps split:if_splits option.splits) - apply (rule allI|rule impI|rule conjI)+ - apply simp - apply (case_tac "O_proc p \ Tainted s", drule_tac p'=p' in p4, simp+) - apply simp - - - - - apply (auto simp:info_flow_shm_simps one_flow_shm_def dest:Tainted_in_current - intro:p4 p4' split:if_splits option.splits) - apply (auto simp:info_flow_shm_def one_flow_shm_def) - - - - apply (auto simp:one_flow_shm_def intro:p4 p4' split:if_splits option.splits) - - - - prefer 7 - apply (simp split:if_splits option.splits) - apply (rule allI|rule impI|rule conjI)+ - - - apply (auto dest:p4' procs_of_shm_prop2 Tainted_in_current split:if_splits option.splits)[1] - - apply (erule disjE, drule_tac p = p and p' = p' in p4', simp+) - apply (erule disjE, rule disjI2, rule disjI2, rule_tac x = h in exI, simp, rule_tac x= toflag in exI, simp) - apply ((erule exE|erule conjE)+) - - - apply (auto simp:info_flow_shm_def dest:p4' - procs_of_shm_prop2 Tainted_in_current split:if_splits option.splits)[1] - apply (drule_tac p = p and p' = p' in p4') - apply (erule_tac x = ha in allE, simp) - apply (drule_tac p = "nat1" and p' = p' in p4') - apply (auto dest:p4'[where p = nat1 and p' = p']) - -apply (induct s) -apply simp defer -apply (frule vd_cons, frule vt_grant_os, case_tac a) -apply (auto simp:info_flow_shm_def elim!:disjE) -sorry *) - sorry -qed -qed - -lemma has_same_inode_comm: - "has_same_inode s f f' = has_same_inode s f' f" -by (auto simp add:has_same_inode_def same_inode_files_def is_file_def) - -lemma tainted_imp_Tainted: - "obj \ tainted s \ obj \ Tainted s" -apply (induct rule:tainted.induct) (* -apply (simp_all add:vd_cons) -apply (rule impI) - -apply (rule disjI2, rule_tac x = flag' in exI, simp) -apply ((rule impI)+, erule_tac x = p' in allE, simp) -*) -apply (auto intro:info_flow_shm_Tainted simp:has_same_inode_def dest:vd_cons) -apply (case_tac e, auto split:option.splits if_splits simp:alive_simps) +apply (frule vd_cons, frule valid_tainted_obj, simp, frule vt_grant_os, case_tac a) +apply (auto simp:alive_simps split:if_splits option.splits t_object.splits intro:file_of_pfd_is_file) done -lemma Tainted_imp_tainted_aux_remain: - "\obj \ Tainted s; valid (e # s); alive (e # s) obj; \ obj. obj \ Tainted s \ obj \ tainted s\ - \ obj \ tainted (e # s)" -by (rule t_remain, auto) - -lemma Tainted_imp_tainted: - "\obj \ Tainted s; valid s\ \ obj \ tainted s" -apply (induct s arbitrary:obj, simp add:t_init) -apply (frule Tainted_in_current, simp+) -apply (frule vt_grant_os, frule vd_cons, case_tac a) -apply (auto split:if_splits option.splits elim:Tainted_imp_tainted_aux_remain intro:tainted.intros - simp:has_same_inode_def) -done - -lemma tainted_eq_Tainted: - "valid s \ (obj \ tainted s) = (obj \ Tainted s)" -by (rule iffI, auto intro:Tainted_imp_tainted tainted_imp_Tainted) - -lemma info_flow_shm_tainted: - "\O_proc p \ tainted s; info_flow_shm s p p'; valid s\ \ O_proc p' \ tainted s" -by (simp only:tainted_eq_Tainted info_flow_shm_Tainted) - +lemma tainted_proc_in_current: + "\O_proc p \ tainted s; valid s\ \ p \ current_procs s" +by (drule tainted_in_current, simp+) -lemma same_inode_files_Tainted: - "\O_file f \ Tainted s; f' \ same_inode_files s f; valid s\ \ O_file f' \ Tainted s" -apply (induct s arbitrary:f f', simp add:same_inode_in_seeds has_same_inode_def) -apply (frule vt_grant_os, frule vd_cons, case_tac a) -prefer 6 -apply (simp split:if_splits option.splits add:same_inode_files_open current_files_simps) -prefer 8 -apply (frule Tainted_in_current, simp, simp add:alive.simps, drule is_file_in_current) -apply (auto simp add:same_inode_files_closefd split:option.splits if_splits)[1] -prefer 8 -apply (frule Tainted_in_current, simp, simp add:alive.simps, drule is_file_in_current) -apply (auto simp add:same_inode_files_unlink split:option.splits if_splits)[1] -prefer 10 -apply (auto split:if_splits option.splits simp:same_inode_files_linkhard current_files_simps)[1] -apply (drule Tainted_in_current, simp, simp add:alive.simps is_file_in_current) -apply (drule same_inode_files_prop5, simp) -apply (drule same_inode_files_prop5, drule_tac f' = list1 and f'' = f' in same_inode_files_prop4, simp, simp) - -apply (auto simp:same_inode_files_other split:if_splits) -apply (drule_tac f'' = f' and f' = f and f = fa in same_inode_files_prop4, simp+) -apply (drule_tac f'' = f' and f' = f and f = list in same_inode_files_prop4, simp+) +lemma t_remain: "\obj \ tainted s; valid (e # s); alive (e # s) obj\ + \ obj \ tainted (e # s)" +apply (frule vd_cons, frule vt_grant_os, case_tac e) +apply (auto simp:alive_simps split:option.splits if_splits) done -lemma has_same_inode_Tainted: - "\O_file f \ Tainted s; has_same_inode s f f'; valid s\ \ O_file f' \ Tainted s" -by (simp add:has_same_inode_def same_inode_files_Tainted) - -lemma has_same_inode_tainted: - "\O_file f \ tainted s; has_same_inode s f f'; valid s\ \ O_file f' \ tainted s" -by (simp add:has_same_inode_Tainted tainted_eq_Tainted) - -lemma same_inodes_Tainted: - "\f \ same_inode_files s f'; valid s\ \ (O_file f \ Tainted s) = (O_file f' \ Tainted s)" -apply (frule same_inode_files_prop8, frule same_inode_files_prop7) -apply (auto intro:has_same_inode_Tainted) -done - - - -lemma tainted_in_current: - "obj \ tainted s \ alive s obj" -apply (erule tainted.induct) -apply (auto dest:vt_grant_os vd_cons info_shm_flow_in_procs procs_of_shm_prop2 simp:is_file_simps) -apply (drule seeds_in_init, simp add:tobj_in_alive) -apply (erule has_same_inode_prop2, simp, simp add:vd_cons) -apply (frule vt_grant_os, simp) -apply (erule has_same_inode_prop1, simp, simp add:vd_cons) -done - -lemma tainted_is_valid: - "obj \ tainted s \ valid s" -by (erule tainted.induct, auto intro:valid.intros) - lemma t_remain_app: "\obj \ tainted s; \ deleted obj (s' @ s); valid (s' @ s)\ \ obj \ tainted (s' @ s)" apply (induct s', simp) apply (simp (no_asm) only:cons_app_simp_aux, rule t_remain) apply (simp_all add:not_deleted_cons_D vd_cons) -apply (drule tainted_in_current, simp add:not_deleted_imp_alive_cons) +apply (drule tainted_in_current) +apply (simp add:vd_cons) +apply (simp add:not_deleted_imp_alive_cons) done -lemma valid_tainted_obj: - "obj \ tainted s \ (\ f. obj \ O_dir f) \ (\ q. obj \ O_msgq q) \ (\ h. obj \ O_shm h) \ (\ p fd. obj \ O_fd p fd) \ (\ s. obj \ O_tcp_sock s) \ (\ s. obj \ O_udp_sock s)" -apply (erule tainted.induct) -apply (drule seeds_in_init) -by auto -lemma dir_not_tainted: "O_dir f \ tainted s \ False" -by (auto dest:valid_tainted_obj) - -lemma msgq_not_tainted: "O_msgq q \ tainted s \ False" -by (auto dest:valid_tainted_obj) - -lemma shm_not_tainted: "O_shm h \ tainted s \ False" -by (auto dest:valid_tainted_obj) end