(*<*)+
−
theory S2ss_prop+
−
imports Main Flask Flask_type Static Static_type Init_prop Tainted_prop Valid_prop Alive_prop Co2sobj_prop+
−
begin+
−
(*>*)+
−
+
−
context tainting_s begin+
−
+
−
+
−
lemma current_proc_has_sp:+
−
  "\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> sp. cp2sproc s p = Some sp"+
−
by (auto simp:cp2sproc_def split:option.splits dest!:current_has_sec')+
−
+
−
lemma current_proc_has_sp':+
−
  "\<lbrakk>cp2sproc s p = None; valid s\<rbrakk> \<Longrightarrow> p \<notin> current_procs s"+
−
by (auto dest:current_proc_has_sp)+
−
+
−
lemma is_dir_has_sdir':+
−
  "\<lbrakk>is_dir s f; valid s\<rbrakk> \<Longrightarrow> \<exists> sf. cf2sfile s f = Some sf"+
−
apply (case_tac f)+
−
apply (rule_tac x = sroot in exI)+
−
apply (simp add:sroot_only)+
−
apply (drule is_dir_has_sfile, auto)+
−
done+
−
+
−
lemma is_file_has_sfile':+
−
  "\<lbrakk>is_file s f; valid s\<rbrakk> \<Longrightarrow> \<exists> sf. cf2sfile s f = Some sf"+
−
by (drule is_file_has_sfile, auto)+
−
+
−
(* simpset for same_inode_files: Current_files_prop.thy *)+
−
+
−
lemma same_inode_files_nil:+
−
  "same_inode_files [] = init_same_inode_files"+
−
by (rule ext, simp add:same_inode_files_def init_same_inode_files_def is_file_nil)+
−
+
−
lemma iof's_im_in_cim': "Some im = inum_of_file \<tau> f \<Longrightarrow> im \<in> current_inode_nums \<tau>"+
−
by (auto simp add:current_inode_nums_def current_file_inums_def)+
−
+
−
lemma same_inode_files_open:+
−
  "valid (Open p f flags fd opt # s) \<Longrightarrow> same_inode_files (Open p f flags fd opt # s) = (\<lambda> f'.+
−
     if (f' = f \<and> opt \<noteq> None) then {f} else same_inode_files s f')"+
−
apply (frule vt_grant_os, frule vd_cons, rule ext)+
−
apply (auto simp:same_inode_files_def is_file_simps split:if_splits option.splits+
−
            dest:iof's_im_in_cim iof's_im_in_cim')+
−
apply (drule is_file_in_current)+
−
apply (simp add:current_files_def)+
−
done+
−
+
−
lemma same_inode_files_linkhard:+
−
  "valid (LinkHard p oldf f # s) \<Longrightarrow> same_inode_files (LinkHard p oldf f # s) = (\<lambda> f'. +
−
     if (f' = f \<or> f' \<in> same_inode_files s oldf) +
−
     then same_inode_files s oldf \<union> {f}+
−
     else same_inode_files s f')"+
−
apply (frule vt_grant_os, frule vd_cons, rule ext)+
−
apply (auto simp:same_inode_files_def is_file_simps split:if_splits option.splits+
−
            dest:iof's_im_in_cim iof's_im_in_cim')+
−
apply (drule is_file_in_current)+
−
apply (simp add:current_files_def is_file_def)+
−
apply (simp add:is_file_def)+
−
done+
−
+
−
lemma inum_of_file_none_prop:+
−
  "\<lbrakk>inum_of_file s f = None; valid s\<rbrakk> \<Longrightarrow> f \<notin> current_files s"+
−
by (simp add:current_files_def)+
−
+
−
lemma same_inode_files_closefd:+
−
  "\<lbrakk>valid (CloseFd p fd # s); f' \<in> current_files (CloseFd p fd # s)\<rbrakk> \<Longrightarrow> +
−
   same_inode_files (CloseFd p fd # s) f' = (+
−
     case (file_of_proc_fd s p fd) of +
−
       Some f \<Rightarrow> (if ((proc_fd_of_file s f = {(p, fd)}) \<and> (f \<in> files_hung_by_del s))+
−
                 then same_inode_files s f' - {f}+
−
                 else same_inode_files s f' )+
−
     | None   \<Rightarrow> same_inode_files s f' )"+
−
apply (frule vt_grant_os, frule vd_cons)+
−
apply (auto simp:same_inode_files_def is_file_closefd current_files_closefd +
−
           split:if_splits option.splits+
−
            dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop)+
−
done+
−
+
−
lemma same_inode_files_unlink:+
−
  "\<lbrakk>valid (UnLink p f # s); f' \<in> current_files (UnLink p f # s)\<rbrakk> +
−
   \<Longrightarrow> same_inode_files (UnLink p f # s) f' = (+
−
     if (proc_fd_of_file s f = {}) +
−
     then same_inode_files s f' - {f}+
−
     else same_inode_files s f')"+
−
apply (frule vt_grant_os, frule vd_cons)+
−
apply (auto simp:same_inode_files_def is_file_unlink current_files_unlink +
−
           split:if_splits option.splits+
−
            dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop)+
−
done+
−
+
−
lemma same_inode_files_mkdir:+
−
  "valid (Mkdir p f inum # s) \<Longrightarrow> same_inode_files (Mkdir p f inum # s) = (same_inode_files s)"+
−
apply (frule vt_grant_os, frule vd_cons, rule ext)+
−
apply (auto simp:same_inode_files_def is_file_simps current_files_simps +
−
           split:if_splits option.splits+
−
            dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop is_file_in_current)+
−
apply (simp add:current_files_def is_file_def)+
−
done+
−
+
−
lemma same_inode_files_other:+
−
  "\<lbrakk>valid (e # s); +
−
    \<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt;+
−
    \<forall> p fd. e \<noteq> CloseFd p fd;+
−
    \<forall> p f. e \<noteq> UnLink p f;+
−
    \<forall> p f f'. e \<noteq> LinkHard p f f'\<rbrakk> \<Longrightarrow> same_inode_files (e # s)  = same_inode_files s"+
−
apply (frule vt_grant_os, frule vd_cons, rule ext, case_tac e)+
−
apply (auto simp:same_inode_files_def is_file_simps current_files_simps dir_is_empty_def+
−
           split:if_splits option.splits+
−
            dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop is_file_not_dir)+
−
apply (simp add:is_file_def is_dir_def current_files_def split:option.splits t_inode_tag.splits)++
−
done+
−
 +
−
lemmas same_inode_files_simps = same_inode_files_nil same_inode_files_open same_inode_files_linkhard+
−
  same_inode_files_closefd same_inode_files_unlink same_inode_files_mkdir same_inode_files_other+
−
+
−
lemma same_inode_files_prop1:+
−
  "f \<in> same_inode_files s f' \<Longrightarrow> f \<in> current_files s"+
−
by (simp add:same_inode_files_def is_file_def current_files_def split:if_splits option.splits)+
−
+
−
lemma same_inode_files_prop2:+
−
  "\<lbrakk>f \<in> same_inode_files s f'; f'' \<notin> current_files s\<rbrakk> \<Longrightarrow> f \<noteq> f''"+
−
by (auto dest:same_inode_files_prop1)+
−
+
−
lemma same_inode_files_prop3:+
−
  "\<lbrakk>f \<in> same_inode_files s f'; is_dir s f''\<rbrakk> \<Longrightarrow> f \<noteq> f''"+
−
apply (rule notI)+
−
apply (simp add:same_inode_files_def is_file_def is_dir_def +
−
          split:if_splits option.splits t_inode_tag.splits)+
−
done+
−
+
−
lemma same_inode_files_prop4:+
−
  "\<lbrakk>f' \<in> same_inode_files s f; f'' \<in> same_inode_files s f'\<rbrakk> \<Longrightarrow> f'' \<in> same_inode_files s f"+
−
by (auto simp:same_inode_files_def split:if_splits)+
−
+
−
lemma same_inode_files_prop5:+
−
  "f' \<in> same_inode_files s f \<Longrightarrow> f \<in> same_inode_files s f'"+
−
by (auto simp:same_inode_files_def is_file_def split:if_splits)+
−
+
−
(* simpset for cf2sfiles *)+
−
+
−
lemma cf2sfiles_open:+
−
  "\<lbrakk>valid (Open p f flag fd opt # s); f' \<in> current_files (Open p f flag fd opt # s)\<rbrakk>+
−
   \<Longrightarrow> cf2sfiles (Open p f flag fd opt # s) f' = (+
−
     if (f' = f \<and> opt \<noteq> None) +
−
     then (case cf2sfile (Open p f flag fd opt # s) f of +
−
             Some sf \<Rightarrow> {sf}  +
−
           | _       \<Rightarrow> {} )+
−
     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:+
−
  "\<lbrakk>valid (e # s);+
−
    \<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt;+
−
    \<forall> p fd. e \<noteq> CloseFd p fd;+
−
    \<forall> p f. e \<noteq> UnLink p f;+
−
    \<forall> p f f'. e \<noteq> LinkHard p f f'\<rbrakk> \<Longrightarrow> 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':+
−
  "\<lbrakk>valid (LinkHard p oldf f # s); f' \<in> same_inode_files s f''\<rbrakk>+
−
   \<Longrightarrow> 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) \<Longrightarrow> cf2sfiles (LinkHard p oldf f # s) = (\<lambda> f'. +
−
     if (f' = f \<or> f' \<in> same_inode_files s oldf)+
−
     then (case (cf2sfile (LinkHard p oldf f # s) f) of+
−
             Some sf \<Rightarrow> cf2sfiles s oldf \<union> {sf}+
−
           | _       \<Rightarrow> {})+
−
     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':+
−
  "\<lbrakk>valid (UnLink p f # s); f' \<in> same_inode_files (UnLink p f # s) f''\<rbrakk>+
−
   \<Longrightarrow> cf2sfile (UnLink p f # s) f' = cf2sfile s f'"+
−
apply (drule same_inode_files_prop1)+
−
by (simp add:cf2sfile_unlink)+
−
+
−
lemma cf2sfiles_unlink:+
−
  "\<lbrakk>valid (UnLink p f # s); f' \<in> current_files (UnLink p f # s)\<rbrakk> \<Longrightarrow> cf2sfiles (UnLink p f # s) f' = ( +
−
     if (f' \<in> same_inode_files s f \<and> proc_fd_of_file s f = {} \<and> +
−
         (\<forall> f'' \<in> same_inode_files s f. f'' \<noteq> f \<longrightarrow> cf2sfile s f'' \<noteq> cf2sfile s f)) then +
−
        (case (cf2sfile s f) of +
−
           Some sf \<Rightarrow> cf2sfiles s f' - {sf}+
−
         | _       \<Rightarrow> {})+
−
     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:+
−
  "\<lbrakk>valid (CloseFd p fd # s); f' \<in> current_files (CloseFd p fd # s)\<rbrakk> \<Longrightarrow> cf2sfiles (CloseFd p fd # s) f' = (+
−
     case (file_of_proc_fd s p fd) of+
−
       Some f \<Rightarrow> if (f' \<in> same_inode_files s f \<and> proc_fd_of_file s f = {(p, fd)} \<and> f \<in> files_hung_by_del s \<and> +
−
                    (\<forall> f'' \<in> same_inode_files s f. f'' \<noteq> f \<longrightarrow> cf2sfile s f'' \<noteq> cf2sfile s f)) +
−
                 then (case (cf2sfile s f) of +
−
                         Some sf \<Rightarrow> cf2sfiles s f' - {sf}+
−
                       | _       \<Rightarrow> {})+
−
                 else cf2sfiles s f'+
−
     | _       \<Rightarrow> 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 \<in> 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:+
−
  "\<lbrakk>valid (Execve p f fds # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Execve p f fds # s) obj = (+
−
      if (obj = O_proc p)+
−
      then (case (cp2sproc (Execve p f fds # s) p) of+
−
              Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s \<or> O_file f \<in> Tainted s))+
−
            | _       \<Rightarrow> 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 (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 (rule impI, simp add:cf2sfiles_other) +
−
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_+
−
+
−
+
−
end+
−
+
−
(* simpset for s2ss*)+
−
+
−
lemma s2ss_execve:+
−
  "valid (Execve p f fds # s) \<Longrightarrow> s2ss (Execve p f fds # s) = (+
−
     if (\<exists> p'. p' \<noteq> p \<and> p' \<in> current_procs s \<and> co2sobj s (O_proc p') = co2sobj s (O_proc p))+
−
     then (case (cp2sproc (Execve p f fds # s) p) of+
−
             Some sp \<Rightarrow> s2ss s \<union> {S_proc sp (O_proc p \<in> Tainted s \<or> O_file f \<in> Tainted s)}+
−
           | _ \<Rightarrow> s2ss s)+
−
     else (case (cp2sproc (Execve p f fds # s) p) of+
−
             Some sp \<Rightarrow> s2ss s - {S_proc sp (O_proc p \<in> Tainted s)}+
−
                              \<union> {S_proc sp (O_proc p \<in> Tainted s \<or> O_file f \<in> Tainted s)}+
−
           | _ \<Rightarrow> s2ss s) )"+
−
apply (frule vd_cons, frule vt_grant_os, simp split:if_splits)+
−
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)+
−
+
−
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)+
−