diff -r cebdef333899 -r 1d1aa5bdd37d no_shm_selinux/Enrich2.thy --- a/no_shm_selinux/Enrich2.thy Mon Dec 30 12:01:09 2013 +0800 +++ b/no_shm_selinux/Enrich2.thy Mon Dec 30 14:04:23 2013 +0800 @@ -648,6 +648,29 @@ apply (auto simp:is_created_proc_simps split:if_splits) done qed + have sf_cons: + "\<forall>f. f \<in> current_files (e # s) \<longrightarrow> cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f" + proof clarify + fix f + assume a1: "f \<in> current_files (e # s)" + from pre have pre_sf: "\<And> f. \<lbrakk>f \<in> current_files s; is_created_proc s p\<rbrakk> + \<Longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f" + by auto + from a1 have a1': "f \<in> current_files (enrich_proc (e # s) p p')" + using vd_cons' nodel_cons + by (simp add:enrich_proc_cur_files) + + show "cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f" + apply (case_tac e) + using vd created_cons nodel_cons vd_enrich_cons vd_cons' a1 a1' + apply (auto intro!:pre_sf simp:cf2sfile_simps is_created_proc_simps + split:if_splits dest:vd_cons) + thm cf2sfile_other + apply (simp_all) + done + + + sorry moreover have "\<forall>tp fd. fd \<in> proc_file_fds (e # s) tp \<longrightarrow> cfd2sfd (enrich_proc (e # s) p p') tp fd = cfd2sfd (e # s) tp fd" proof clarify @@ -673,6 +696,18 @@ using a1' nodel_cons all_procs_cons a1' created_cons vd_cons' apply (frule_tac enrich_proc_filefd, simp_all) done + have sec_proc: + "\<And> tp. \<lbrakk>tp \<in> current_procs s; is_created_proc s p\<rbrakk> + \<Longrightarrow> sectxt_of_obj (enrich_proc s p p') (O_proc tp) = sectxt_of_obj s (O_proc tp)" + using pre + apply (clarsimp) + apply (erule_tac x = tp in allE, auto simp:cp2sproc_def split:option.splits) + done + have sec_proc': + "\<And> tp. \<lbrakk>tp \<in> current_procs s; is_created_proc s p; p = tp\<rbrakk> + \<Longrightarrow> sectxt_of_obj (enrich_proc s tp p') (O_proc tp) = sectxt_of_obj s (O_proc tp)" + apply (drule_tac sec_proc, simp+) + done show "cfd2sfd (enrich_proc (e # s) p p') tp fd = cfd2sfd (e # s) tp fd" proof- have b1: "\<And> proc f' fds. e = Execve proc f' fds @@ -701,9 +736,48 @@ done have b3: "\<And> proc f' flags fd' opt. e = Open proc f' flags fd' opt \<Longrightarrow> cfd2sfd (enrich_proc (e # s) p p') tp fd = cfd2sfd (e # s) tp fd" + using a4 a1' vd_enrich_cons vd_cons' created_cons + apply (simp split:if_splits del:file_of_proc_fd.simps) + + apply (simp add:cfd2sfd_open sec_open is_created_proc_simps a2 del:file_of_proc_fd.simps) + apply (tactic {*my_clarify_tac 1*}) + apply (drule vd_cons) + apply (simp add:cfd2sfd_open sec_open a3 a2 split:if_splits) + apply (case_tac "proc \<in> current_procs s") + apply (simp add:sec_proc') + apply (case_tac "sectxt_of_obj s (O_proc proc)", simp+) + apply (case_tac "f \<in> current_files (e # s)") + apply (drule sf_cons[rule_format], simp) + using vd_enrich_cons + apply (simp add:cf2sfile_open_none) + using os + apply (simp add:current_files_simps is_file_in_current split:option.splits) + using os + apply (simp split:option.splits) + apply (rule impI) + apply (simp add:cfd2sfd_open sec_open a3 a2 split:if_splits) + apply (drule vd_cons) + apply (drule_tac p' = tp and fd' = fd and f' = f and s = "enrich_proc s proc p'" in cfd2sfd_open) + apply (simp, rule impI, simp) + apply (simp split:if_splits, rule conjI, rule impI, simp) + apply (drule pre_sfd', simp, simp) + + apply (simp add:cfd2sfd_open sec_open is_created_proc_simps a2 del:file_of_proc_fd.simps) + apply (case_tac "proc \<in> current_procs s") + apply (simp add:sec_proc) + apply (case_tac "f' \<in> current_files (e # s)") + apply (drule sf_cons[rule_format], simp) + apply (simp split:option.splits) + apply (rule impI|rule conjI)+ + apply (drule current_has_sec', simp add:vd, simp add:os) + apply (rule impI, rule impI) apply (simp split:if_splits) - thm cfd2sfd_open - sorry + apply (simp add:pre_sfd') + using os + apply (simp add:current_files_simps is_file_in_current split:option.splits) + using os + apply (simp split:option.splits) + done have b4: "\<And> proc fd'. e = ReadFile proc fd' \<Longrightarrow> cfd2sfd (enrich_proc (e # s) p p') tp fd = cfd2sfd (e # s) tp fd" using a4 vd_enrich_cons a1' vd_cons' created_cons @@ -727,8 +801,6 @@ qed moreover have "\<forall>tp. tp \<in> current_procs (e # s) \<longrightarrow> cp2sproc (enrich_proc (e # s) p p') tp = cp2sproc (e # s) tp" sorry - moreover have "\<forall>f. f \<in> current_files (e # s) \<longrightarrow> cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f" - sorry moreover have "\<forall>q. q \<in> current_msgqs (e # s) \<longrightarrow> cq2smsgq (enrich_proc (e # s) p p') q = cq2smsgq (e # s) q" sorry moreover have "cp2sproc (enrich_proc (e # s) p p') p' = cp2sproc (e # s) p"