# HG changeset patch # User chunhan # Date 1378965022 -28800 # Node ID 137358bd49213eca3885fb974d7b525cdf734631 # Parent 021672ec28f50c4e8712616b525384077d20bbd6 update diff -r 021672ec28f5 -r 137358bd4921 Dynamic2static.thy --- a/Dynamic2static.thy Thu Sep 05 13:23:03 2013 +0800 +++ b/Dynamic2static.thy Thu Sep 12 13:50:22 2013 +0800 @@ -22,8 +22,8 @@ "\alive s obj; co2sobj s obj= Some sobj\ \ sobj \ (s2ss s)" by (simp add:s2ss_def, rule_tac x = obj in exI, simp) -lemma alive_has_sobj: - "\alive s obj; valid s\ \ \ sobj. co2sobj s obj = Some sobj" +lemma tainted_has_sobj: + "\obj \ tainted s; valid s\ \ \ sobj. co2sobj s obj = Some sobj" sorry lemma t2ts: @@ -37,12 +37,7 @@ apply (drule dir_not_tainted, simp) apply (drule msgq_not_tainted, simp) apply (drule shm_not_tainted, simp) -apply (case_tac prod1, simp, case_tac prod2, clarsimp) -apply (rule conjI) -apply (rule_tac x = "O_msgq nat1" in exI, simp) -apply (rule conjI) defer -apply (simp add:cm2smsg_def split:option.splits) -sorry +done lemma delq_imp_delqm: "deleted (O_msgq q) s \ deleted (O_msg q m) s" @@ -57,21 +52,28 @@ by (auto simp:taintable_def) hence vs: "valid s" by (simp add:tainted_is_valid) hence static: "s2ss s \ static" using d2s_main by auto - from tainted have alive: "alive s obj" - using tainted_in_current by auto - then obtain sobj where sobj: "co2sobj s obj = Some sobj" - using vs alive_has_sobj by blast + from tainted obtain sobj where sobj: "co2sobj s obj = Some sobj" + using vs tainted_has_sobj by blast from undel vs have "\ deleted obj s" and init_alive: "init_alive obj" by (auto simp:undeletable_def) with vs sobj have "init_obj_related sobj obj" apply (case_tac obj, case_tac [!] sobj) apply (auto split:option.splits if_splits simp:cp2sproc_def ch2sshm_def cq2smsgq_def cm2smsg_def delq_imp_delqm) - apply (frule not_deleted_init_file, simp+) (* -apply (drule is_file_has_sfile, erule exE) + apply (frule not_deleted_init_file, simp+) + apply (drule is_file_has_sfile', simp, erule exE) apply (rule_tac x = sf in bexI) apply (case_tac list, auto split:option.splits simp:is_init_file_props)[1] - apply (simp add:same_inode_files_def cfs2sfiles_def) *) - sorry + apply (drule root_is_init_dir', simp) + apply (frule not_deleted_init_file, simp, simp) + apply (simp add:cf2sfile_def split:option.splits if_splits) + apply (simp add:cf2sfiles_def) + apply (rule_tac x = list in bexI, simp, simp add:same_inode_files_def not_deleted_init_file) + + apply (frule not_deleted_init_dir, simp+) + apply (simp add:cf2sfile_def split:option.splits if_splits) + apply (case_tac list, simp add:sroot_def, simp) + apply (drule file_dir_conflict, simp+) + done with tainted t2ts init_alive sobj static show ?thesis unfolding taintable_s_def apply (rule_tac x = "s2ss s" in bexI, simp) @@ -189,7 +191,7 @@ lemma cqm2sms_prop1: "\cqm2sms s q queue = Some sms; sm \ set sms\ \ \ m. cm2smsg s q m = Some sm" apply (induct queue arbitrary:sms) -apply (auto split:option.splits) +apply (auto simp:cqm2sms.simps split:option.splits) done lemma sq_sm_prop: @@ -216,7 +218,11 @@ apply (case_tac obj, simp_all split:option.splits if_splits) apply (drule_tac sm = "(aa, ba, True)" in sq_sm_prop, simp+, erule exE) apply (rule_tac x = "O_msg nat m" in exI) -apply (simp add:cm2smsg_def split:option.splits) +apply (rule conjI) +apply simp +apply (simp add +apply (simp add:co2sobj.simps) +apply (simp add:cm2smsg_def split:option.splits if_splits) done lemma has_inode_tainted_aux: diff -r 021672ec28f5 -r 137358bd4921 S2ss_prop.thy --- a/S2ss_prop.thy Thu Sep 05 13:23:03 2013 +0800 +++ b/S2ss_prop.thy Thu Sep 12 13:50:22 2013 +0800 @@ -8,17 +8,29 @@ (* simpset for s2ss*) +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_dir f \ P (O_dir f); \ q. obj = O_msgq q \ P (O_msgq q)\ + \ P obj" +by (case_tac obj, auto) + +lemma co2sobj_execve_alive: + "\alive s obj; co2sobj s obj = Some x; valid (Execve p f fds # s)\ + \ alive (Execve p f fds # s) obj" +apply (erule co2sobj_some_case) +by (auto simp:alive_simps simp del:alive.simps) lemma s2ss_execve: "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)} - | _ \ s2ss s) - else (case (cp2sproc (Execve p f fds # s) p) of - 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)} - | _ \ s2ss 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)} + | _ \ {} ) )" apply (frule vd_cons, frule vt_grant_os, simp split:if_splits) apply (rule conjI, rule impI, (erule exE|erule conjE)+) @@ -39,41 +51,521 @@ 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 (case_tac "obj = O_proc p", simp) +apply (frule co2sobj_execve_alive, simp, simp) +apply (frule_tac obj = obj in co2sobj_execve, simp) +apply (rule_tac x = obj in exI, simp, simp) -apply (case_tac obj, simp_all add:co2sobj_execve alive_simps) -thm alive_execve -thm co2sobj_execve +apply (erule conjE, frule current_proc_has_sp, simp, erule exE, rule impI, simp) +apply (subgoal_tac "p \ current_procs (Execve p f fds # s)") +apply (drule_tac p = p and s = "Execve p f fds # s" in current_proc_has_sp, simp) +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 (rule disjI1, simp split:if_splits) apply (simp add:co2sobj_execve, rule disjI2) -apply (rule_tac x = obj in exI, simp split:t_object.splits) -thm co2sobj_execve -apply (case_tac obj, auto simp:co2sobj_execve alive_simps tainted_eq_Tainted split:option.splits dest!:current_proc_has_sp')[1] -apply (simp add:co2sobj_execve) -apply clarsimp -thm current_proc_has_sp +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 disjE, simp) +apply (rule_tac x = "O_proc p" in exI, simp add:tainted_eq_Tainted) +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) +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" +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)} + | _ \ {})" +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 (rule disjI1, simp split:if_splits) +apply (simp add:tainted_eq_Tainted, 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 (erule exE| erule conjE)+ +apply (case_tac "obj = O_proc p'", simp) +apply (rule_tac x = obj in exI) +apply (frule s2ss_clone_alive, simp+) +apply (auto simp:co2sobj_clone alive_simps) +done + +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} + - {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 \ + cp2sproc s p' = Some sp \ O_proc p' \ Tainted s))}" + +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); + \ f. \co2sobj s obj = Some sobj; obj = O_file f\ \ P (O_file f); + \ h. \co2sobj s obj = Some sobj; obj = O_shm h\ \ P (O_shm h); + \ f. \co2sobj s obj = Some sobj; obj = O_dir f\ \ P (O_dir f); + \ q. \co2sobj s obj = Some sobj; obj = O_msgq q\ \ P (O_msgq q)\ + \ P obj" +by (case_tac obj, auto) + +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\ + \ s2ss (Ptrace p p' # s) = update_s2ss_shm s p'" +unfolding update_s2ss_shm_def s2ss_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 (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 (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 (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 (erule_tac x = pa in allE, simp) + +apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI, + auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1] +apply (simp) +apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI, + auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1] +apply (simp split:option.splits) +apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI, + auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1] +apply (simp split:option.splits) +apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI, + auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1] +apply (simp split:option.splits) + +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 (rule_tac x = "O_proc pa" in exI) +apply (clarsimp simp add:tainted_eq_Tainted 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 (rule_tac x = "O_proc p'a" in exI) +apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted 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 (rule_tac x = obj in exI, + auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1] +apply (rule_tac x = obj in exI, + auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1] +apply (rule_tac x = obj in exI, + auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1] +apply (rule_tac x = obj in exI, + auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1] + +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) +done + +lemma s2ss_ptrace2: + "\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 +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 (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 (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 (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 (erule_tac x = pa in allE, simp) + +apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI, + auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1] +apply (simp) +apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI, + auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1] +apply (simp split:option.splits) +apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI, + auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1] +apply (simp split:option.splits) +apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI, + auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1] +apply (simp split:option.splits) + +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 (rule_tac x = "O_proc pa" in exI) +apply (clarsimp simp add:tainted_eq_Tainted 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 (rule_tac x = "O_proc p'a" in exI) +apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted 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 (rule_tac x = obj in exI, + auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1] +apply (rule_tac x = obj in exI, + auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1] +apply (rule_tac x = obj in exI, + auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1] +apply (rule_tac x = obj in exI, + auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1] + +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) +done + +lemma s2ss_ptrace3: + "\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) +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)[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) +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) + then update_s2ss_shm s p' + 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) +apply (simp add:s2ss_ptrace2 s2ss_ptrace1 split:if_splits) +by (auto dest:s2ss_ptrace3) -apply (auto simp:s2ss_def co2sobj_execve split:option.splits) +lemma s2ss_kill: + "valid (Kill p p' # s) \ s2ss (Kill p p' # s) = ( + if (\ p''. p'' \ current_procs s \ p'' \ p' \ co2sobj s (O_proc p'') = co2sobj s (O_proc p')) + then s2ss s + else (case (co2sobj s (O_proc p')) of + Some sp \ s2ss s - {sp} + | _ \ {}))" +apply (frule vt_grant_os, frule vd_cons) +unfolding s2ss_def +apply (simp split:if_splits, rule conjI) +apply (rule impI, (erule exE|erule conjE)+) +apply (split option.splits) +apply (drule current_proc_has_sp', simp, simp) +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 (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 + 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 + 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)+ + +apply (rule impI, erule conjE, frule current_proc_has_sp, simp, erule exE, simp) +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 (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 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 + 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 + 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 + +lemma s2ss_exit: + "valid (Exit p # s) \ s2ss (Exit p # s) = ( + if (\ p'. p' \ current_procs s \ p' \ p \ co2sobj s (O_proc p') = co2sobj s (O_proc p)) + then s2ss s + else (case (co2sobj s (O_proc p)) of + Some sp \ s2ss s - {sp} + | _ \ {}))" +apply (frule vt_grant_os, frule vd_cons) +unfolding s2ss_def +apply (simp split:if_splits, rule conjI) +apply (rule impI, (erule exE|erule conjE)+) +apply (split option.splits) +apply (drule current_proc_has_sp', simp, simp) +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 (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 + 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 + 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)+ + +apply (rule impI, frule current_proc_has_sp, simp, erule exE, simp) +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 (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 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 + 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 + 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 + +lemma alive_has_sobj': + "\co2sobj s obj = None; valid s\ \ \ alive s obj" +apply (case_tac obj) +apply (auto split:option.splits) +oops + +declare co2sobj.simps [simp del] + +lemma co2sobj_open_none: + "\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)) + | _ \ None) + else co2sobj s obj)" +apply (frule vt_grant_os, frule vd_cons) +apply (frule_tac obj = obj in co2sobj_open, simp add:alive_open) +apply (auto split:t_object.splits option.splits dest!:current_proc_has_sp') +done + +lemma co2sobj_open_some: + "\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)) + | _ \ 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)) + | _ \ None) + else co2sobj s obj)" +apply (frule vt_grant_os, frule vd_cons) +apply (frule_tac obj = obj in co2sobj_open, simp add:alive_open) +apply (auto split:t_object.splits option.splits dest!:current_proc_has_sp') +done +lemma alive_co2sobj_some_open_none: + "\co2sobj s obj = Some sobj; alive s obj; valid (Open p f flag fd None # s)\ + \ alive (Open p f flag fd None # s) obj" +by (erule co2sobj_some_caseD, auto simp:alive_simps is_file_simps is_dir_simps) + +lemma alive_co2sobj_some_open_none': + "\co2sobj (Open p f flag fd None # s) obj = Some sobj; alive (Open p f flag fd None # s) obj; + valid (Open p f flag fd None # s)\ \ alive s obj" +by (erule co2sobj_some_caseD, auto simp:alive_simps is_file_simps is_dir_simps) + +lemma co2sobj_proc_obj: + "\co2sobj s obj = Some x; co2sobj s (O_proc p) = Some x\ + \ \ p'. obj = O_proc p'" +by (case_tac obj, auto simp:co2sobj.simps split:option.splits) + +lemma s2ss_open_none: + "valid (Open p f flag fd None # s) \ s2ss (Open p f flag fd None # s) = ( + case (co2sobj s (O_proc p), co2sobj (Open p f flag fd None # s) (O_proc p)) of + (Some sp, Some sp') \ + if (\ p'. p' \ current_procs s \ p' \ p \ co2sobj s (O_proc p') = Some sp) + then s2ss s \ {sp'} + else s2ss s - {sp} \ {sp'} + | _ \ {} )" +unfolding s2ss_def +apply (frule vt_grant_os, frule vd_cons) +apply (case_tac "co2sobj s (O_proc p)", simp add:co2sobj.simps split:option.splits) +apply (drule current_proc_has_sp', simp, simp) +apply (case_tac "co2sobj (Open p f flag fd None # s) (O_proc p)") +apply (simp add:co2sobj.simps split:option.splits) +apply (drule current_proc_has_sp', simp, simp) +apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE, simp) +apply (frule_tac obj = obj in alive_co2sobj_some_open_none', simp, simp) +apply (rule conjI, rule impI, erule exE, (erule conjE)+) +apply (rule Meson.disj_comm, rule disjCI, case_tac "obj = O_proc p", simp) +apply (rule_tac x = obj in exI, simp add:co2sobj_open_none) +apply (rule impI) +apply (case_tac "obj = O_proc p", simp) +apply (rule Meson.disj_comm, rule disjCI, rule conjI) +apply (rule_tac x = obj in exI, simp add:co2sobj_open_none) +apply (simp add:co2sobj_open_none split:option.splits) +apply (rule notI) +apply (frule co2sobj_proc_obj, simp, erule exE) +apply (erule_tac x = p' in allE, simp) + +apply (simp split:if_splits) +apply (erule disjE, rule_tac x = "O_proc p" in exI, simp) +apply (erule exE, erule conjE, case_tac "obj = O_proc p") +apply (rule_tac x = "O_proc p'" in exI, simp add:co2sobj_open_none) +apply (rule_tac x = obj in exI, simp add:co2sobj_open_none alive_co2sobj_some_open_none) +apply (erule disjE, rule_tac x = "O_proc p" in exI, simp) +apply (erule conjE, erule exE, erule conjE, case_tac "obj = O_proc p") +apply (rule_tac x = "O_proc p'" in exI, simp add:co2sobj_open_none) +apply (rule_tac x = obj in exI, simp add:co2sobj_open_none alive_co2sobj_some_open_none) +done + +lemma alive_co2sobj_some_open_some: + "\alive s obj; valid (Open p f flag fd (Some i) # s)\ + \ alive (Open p f flag fd (Some i) # s) obj" +by (case_tac obj, auto simp:alive_simps is_file_simps is_dir_simps) + +lemma alive_co2sobj_some_open_some': + "\co2sobj (Open p f flag fd (Some i) # s) obj = Some sobj; alive (Open p f flag fd (Some i) # s) obj; + valid (Open p f flag fd (Some i) # s); obj \ O_file f\ \ alive s obj" +by (erule co2sobj_some_caseD, auto simp:alive_simps is_file_simps is_dir_simps) + +lemma s2ss_open_some: + "valid (Open p f flag fd (Some i) # s) \ s2ss (Open p f flag fd (Some i) # s) = ( + case (co2sobj s (O_proc p), co2sobj (Open p f flag fd (Some i) # s) (O_proc p), + co2sobj (Open p f flag fd (Some i) # s) (O_file f)) of + (Some sp, Some sp', Some sf) \ + if (\ p'. p' \ current_procs s \ p' \ p \ co2sobj s (O_proc p') = Some sp) + then s2ss s \ {sp', sf} + else s2ss s - {sp} \ {sp', sf} + | _ \ {} )" +unfolding s2ss_def +apply (frule vt_grant_os, frule vd_cons) +apply (case_tac "co2sobj s (O_proc p)", simp add:co2sobj.simps split:option.splits) +apply (drule current_proc_has_sp', simp, simp) +apply (case_tac "co2sobj (Open p f flag fd (Some i) # s) (O_proc p)") +apply (simp add:co2sobj.simps split:option.splits) +apply (drule current_proc_has_sp', simp, simp) +apply (case_tac "co2sobj (Open p f flag fd (Some i) # s) (O_file f)") +apply (simp add:co2sobj.simps split:option.splits) +apply (clarsimp split del:if_splits) + +apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE) +apply (split if_splits, rule conjI, rule impI, erule exE, erule conjE, erule conjE) +apply (case_tac "obj = O_proc p", simp, case_tac "obj = O_file f", simp) +apply (rule UnI1, rule CollectI, rule_tac x = obj in exI) +apply (frule_tac obj = obj in alive_co2sobj_some_open_some', simp+) +apply (simp add:co2sobj_open split:t_object.splits) +apply (rule impI, case_tac "obj = O_proc p", simp, case_tac "obj = O_file f", simp) +apply (rule UnI1, rule DiffI, rule CollectI, rule_tac x = obj in exI) +apply (frule_tac obj = obj in alive_co2sobj_some_open_some', simp+) +apply (simp add:co2sobj_open split:t_object.splits) +apply (frule_tac obj = obj in co2sobj_open_some, simp+) +apply (simp add:alive_co2sobj_some_open_some', simp) +apply (rule notI) +apply (frule_tac obj = obj and p = p in co2sobj_proc_obj, simp+, erule exE) +apply (erule_tac x = p' in allE, simp) + +apply (simp split:if_splits, erule disjE) +apply (rule_tac x = "O_proc p" in exI, simp) +apply (erule disjE, rule_tac x = "O_file f" in exI, simp add:is_file_simps) +apply (erule exE, erule conjE) +apply (case_tac "obj = O_proc p", simp) +apply (rule_tac x = "O_proc p'" in exI, simp add:co2sobj_open_some) +apply (case_tac "obj = O_file f", simp add:is_file_in_current) +apply (rule_tac x = obj in exI, simp add:co2sobj_open_some alive_co2sobj_some_open_some) +apply (erule disjE, rule_tac x = "O_proc p" in exI, simp) +apply (erule disjE, rule_tac x = "O_file f" in exI, simp add:is_file_simps) +apply (erule conjE, erule exE, erule conjE) +apply (case_tac "obj = O_proc p", simp) +apply (case_tac "obj = O_file f", simp add:is_file_in_current) +apply (rule_tac x = obj in exI, simp add:co2sobj_open_some alive_co2sobj_some_open_some) +done + +lemma s2ss_open: + "valid (Open p f flag fd opt # s) \ s2ss (Open p f flag fd opt # s) = ( + if opt = None + then (case (co2sobj s (O_proc p), co2sobj (Open p f flag fd opt # s) (O_proc p)) of + (Some sp, Some sp') \ + if (\ p'. p' \ current_procs s \ p' \ p \ co2sobj s (O_proc p') = Some sp) + then s2ss s \ {sp'} + else s2ss s - {sp} \ {sp'} + | _ \ {} ) + else (case (co2sobj s (O_proc p), co2sobj (Open p f flag fd opt # s) (O_proc p), + co2sobj (Open p f flag fd opt # s) (O_file f)) of + (Some sp, Some sp', Some sf) \ + if (\ p'. p' \ current_procs s \ p' \ p \ co2sobj s (O_proc p') = Some sp) + then s2ss s \ {sp', sf} + else s2ss s - {sp} \ {sp', sf} + | _ \ {} ) )" +apply (case_tac opt) +apply (simp add:s2ss_open_some s2ss_open_none)+ +done + +lemma -apply (rule conjI, clarify) -apply (frule_tac p = p in current_proc_has_sp, simp, erule exE) -apply (frule_tac p = p' in current_proc_has_sp, simp, erule exE) -apply (simp, (erule conjE)+) -apply (split option.splits, rule conjI, rule impI, drule current_proc_has_sp', simp, simp) -apply (rule allI, rule impI) -apply (rule set_eqI, rule iffI) +lemmas s2ss_simps = s2ss_execve s2ss_clone s2ss_ptrace s2ss_kill s2ss_exit s2ss_open -apply (simp split:option.splits) -apply (frule_tac p = p and s = "Execve p f fds # s" in current_proc_has_sp) -thm current_proc_has_sp - - -apply (simp split:option.splits) -apply (drule current_proc_has_sp', simp, simp) -apply (rule conjI, rule impI, drule current_proc_has_sp', simp, simp) -apply (simp add:s2ss_def) -apply (rule allI|rule impI)+ -apply (rule set_eqI, rule iffI) -apply (auto simp:alive_simps) -apply (case_tac obj, auto split:option.splits simp:cp2sproc_execve) -apply (auto split:if_splits) \ No newline at end of file diff -r 021672ec28f5 -r 137358bd4921 Static.thy --- a/Static.thy Thu Sep 05 13:23:03 2013 +0800 +++ b/Static.thy Thu Sep 12 13:50:22 2013 +0800 @@ -172,7 +172,6 @@ | "is_many (S_dir sf ) = is_many_sfile sf" | "is_many (S_msgq sq ) = is_many_smsgq sq" | "is_many (S_shm sh ) = is_many_sshm sh" -| "is_many _ = False" (* fun update_ss_sp:: "t_static_state \ t_sobject \ t_sobject \ t_static_state" diff -r 021672ec28f5 -r 137358bd4921 Static_type.thy --- a/Static_type.thy Thu Sep 05 13:23:03 2013 +0800 +++ b/Static_type.thy Thu Sep 12 13:50:22 2013 +0800 @@ -77,9 +77,9 @@ | S_file "t_sfile set" "bool" (* here sfile set is for "linking", tainted is the inode *) | S_dir "t_sfile" | S_msgq "t_smsgq" -| S_shm "t_sshm" +| S_shm "t_sshm" (* | S_msg "t_smsgq" "t_smsg" - +*) (* datatype t_tainted_sobj = TS_proc "t_sproc" "bool" diff -r 021672ec28f5 -r 137358bd4921 Tainted_prop.thy --- a/Tainted_prop.thy Thu Sep 05 13:23:03 2013 +0800 +++ b/Tainted_prop.thy Thu Sep 12 13:50:22 2013 +0800 @@ -15,9 +15,9 @@ (if (O_file f) \ Tainted s then Tainted s \ {O_proc p} else Tainted s)" | "Tainted (Kill p p' # s) = Tainted s - {O_proc p'}" | "Tainted (Ptrace p p' # s) = - (if (O_proc p) \ Tainted s + (if (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 + else if (O_proc p' \ Tainted s) then Tainted s \ {O_proc p'' | p''. info_flow_shm s p p''} else Tainted s)" | "Tainted (Exit p # s) = Tainted s - {O_proc p}"