(*<*)

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)

lemma same_inode_files_prop6:

  "f' \<in> same_inode_files s f \<Longrightarrow> same_inode_files s f' = same_inode_files s f"

by (auto simp:same_inode_files_def is_file_def split:if_splits)

lemma same_inode_files_prop7:

  "f' \<in> same_inode_files s f \<Longrightarrow> has_same_inode s f f'"

(* 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 cf2sfiles_other 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 (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:

  "\<lbrakk>valid (Clone p p' fds shms # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Clone p p' fds shms # s) obj = (

      if (obj = O_proc p')

      then (case (cp2sproc (Clone p p' fds shms # s) p') of

              Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<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 cf2sfiles_other ch2sshm_other cq2smsgq_other tainted_eq_Tainted)

apply (case_tac "cp2sproc (Clone p p' fds shms # 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 (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_ptrace:

  "\<lbrakk>valid (Ptrace p p' # s); alive s obj\<rbrakk>\<Longrightarrow> co2sobj (Ptrace p p' # s) obj = (

     case obj of

       O_proc p'' \<Rightarrow> if (info_flow_shm s p' p'') 

                     then (case (cp2sproc s p'') of 

                             Some sp \<Rightarrow> Some (S_proc sp (O_proc p'' \<in> Tainted s \<or> O_proc p \<in> Tainted s))

                           | _       \<Rightarrow> None)

                     else if (info_flow_shm s p p'')

                          then (case (cp2sproc s p'') of 

                                  Some sp \<Rightarrow> Some (S_proc sp (O_proc p'' \<in> Tainted s \<or> O_proc p' \<in> Tainted s))

                                | _       \<Rightarrow> None)

                          else co2sobj s (O_proc p'')

    | _          \<Rightarrow> 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 (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 (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_open:

  "\<lbrakk>valid (Open p f flag fd opt # s); alive (Open p f flag fd opt # s) obj\<rbrakk> 

   \<Longrightarrow> co2sobj (Open p f flag fd opt # s) obj = (case obj of 

     O_file f' \<Rightarrow> if (f' = f \<and> opt \<noteq> None)

                  then (case (cf2sfile (Open p f flag fd opt # s) f) of

                          Some sf \<Rightarrow> Some (S_file {sf} (O_proc p \<in> Tainted s))

                        | _       \<Rightarrow> None)

                  else co2sobj s (O_file f')

   | O_proc p' \<Rightarrow> if (p' = p) 

                  then (case (cp2sproc (Open p f flag fd opt # s) p) of

                          Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s))

                        | _       \<Rightarrow> None)

                  else co2sobj s (O_proc p')

   | _         \<Rightarrow> 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 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 (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)

apply (frule is_dir_in_current)

apply (frule_tac f' = list in cf2sfile_open)

apply (simp add:current_files_simps split:option.splits)

apply (simp split:if_splits option.splits)

done

lemma co2sobj_readfile:

  "\<lbrakk>valid (ReadFile p fd # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (ReadFile p fd # s) obj = (

     case obj of

       O_proc p' \<Rightarrow> (case (file_of_proc_fd s p fd) of

                       Some f \<Rightarrow> (if (info_flow_shm s p p' \<and> O_file f \<in> Tainted s)

                                  then (case (cp2sproc s p') of

                                          Some sp \<Rightarrow> Some (S_proc sp True)

                                        | _       \<Rightarrow> None)

                                  else co2sobj s obj)

                    | _       \<Rightarrow> None)

     | _         \<Rightarrow> 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 split:if_splits option.splits dest!:current_file_has_sfile' 

             simp:current_files_simps cf2sfiles_simps cf2sfile_simps 

             dest:is_file_in_current is_dir_in_current)

done

lemma co2sobj_writefile:

  "\<lbrakk>valid (WriteFile p fd # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (WriteFile p fd # s) obj = (

     case obj of

       O_file f' \<Rightarrow> (case (file_of_proc_fd s p fd) of

                       Some f \<Rightarrow> (if (f \<in> same_inode_files s f') 

                                  then Some (S_file (cf2sfiles s f') 

                                                    (O_file f' \<in> Tainted s \<or> O_proc p \<in> Tainted s))

                                  else co2sobj s obj)

                    | _       \<Rightarrow> None)

     | _         \<Rightarrow> 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