diff -r 01274a64aece -r aa1375b6c0eb Tainted_prop.thy --- a/Tainted_prop.thy Mon Aug 05 12:30:26 2013 +0800 +++ b/Tainted_prop.thy Tue Aug 27 08:50:53 2013 +0800 @@ -1,5 +1,5 @@ theory Tainted_prop -imports Main Flask Flask_type Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop Current_prop +imports Main Flask Flask_type Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop Current_prop Alive_prop begin context tainting begin @@ -86,27 +86,6 @@ "\O_proc p \ Tainted s; valid s\ \ p \ current_procs s" by (drule Tainted_in_current, simp+) -lemma has_inode_tainted_aux: - "O_file f \ tainted s \ \ f'. has_same_inode s f f' \ O_file f' \ tainted s" -apply (erule tainted.induct) -apply (auto intro:tainted.intros simp:has_same_inode_def) -(*?? need simpset for tainted *) - - -sorry - -lemma has_inode_Tainted_aux: - "\O_file f \ Tainted s; has_same_inode s f f'\ \ O_file f' \ Tainted s" -apply (induct s, auto) -apply (auto intro:tainted.intros simp:has_same_inode_def) -(*?? need simpset for tainted *) -sorry - -lemma "\info_flow_shm s pa pb; info_flow_shm s pb pc; valid s\ \ info_flow_shm s pa pc" -apply (auto simp add:info_flow_shm_def one_flow_shm_def procs_of_shm_prop2) -apply (erule_tac x = h in allE, simp) -apply (case_tac "h = ha", simp+) -sorry lemma info_flow_shm_Tainted: "\O_proc p \ Tainted s; info_flow_shm s p p'; valid s\ \ O_proc p' \ Tainted s" @@ -122,17 +101,16 @@ 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" - apply (rule p4, auto simp:info_flow_shm_def one_flow_shm_def ) (* procs_of_shm_prop2 *) - sorry - 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) *) sorry + 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) + 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)+ @@ -153,9 +131,6 @@ - - - prefer 7 apply (simp split:if_splits option.splits) apply (rule allI|rule impI|rule conjI)+ @@ -175,47 +150,60 @@ apply (drule_tac p = "nat1" and p' = p' in p4') apply (auto dest:p4'[where p = nat1 and p' = p']) -apply (induct s) (* +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 -next - case (Cons e s) - show ?case - sorry +qed qed lemma tainted_imp_Tainted: "obj \ tainted s \ obj \ Tainted s" -apply (induct rule:tainted.induct) +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 dest:vd_cons) apply (case_tac e, auto split:option.splits if_splits simp:alive_simps) 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" -proof (induct s arbitrary:obj) - case Nil - thus ?case by (auto intro:t_init) -next - case (Cons e s) - hence p1: "\ obj. obj \ Tainted s \ obj \ tainted s" - and p2: "obj \ Tainted (e # s)" and p3: "valid (e # s)" - and p4: "valid s" and p5: "os_grant s e" - by (auto dest:vd_cons intro:vd_cons vt_grant_os) - from p1 have p6: "" -apply (frule vd_cons, frule vt_grant_os, frule valid_Tainted_obj, simp) -apply (case_tac a) -apply (auto intro!:t_init t_clone t_execve t_cfile t_read t_write t_link t_trunc t_sendmsg t_recvmsg - intro:t_remain - split:if_splits option.splits dest:Tainted_in_current) -pr 25 +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) +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 tainted_imp_Tainted: - "obj \ tainted s \ obj \ Tainted s" +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 has_same_inode_Tainted: + "\O_file f \ Tainted s; has_same_inode s f f'; valid s\ \ O_file f' \ Tainted s" +apply (induct s arbitrary:f f', simp add:same_inode_in_seeds) +apply (frule vt_grant_os, frule vd_cons, case_tac a) +apply (auto split:if_splits option.splits simp:has_same_inode_def dest:iof's_im_in_cim) +apply (drule_tac obj = "O_file list2" in Tainted_in_current, simp, simp add:is_file_in_current) +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_Tainted tainted_eq_Tainted) @@ -223,7 +211,8 @@ lemma tainted_in_current: "obj \ tainted s \ alive s obj" -apply (erule tainted.induct, auto dest:vt_grant_os vd_cons simp:is_file_simps) +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)