368 lemma co2sobj_

   368 lemma co2sobj_clone:

   369 

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

   370 

   370       if (obj = O_proc p')

   371 end

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

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

   373             | _       \<Rightarrow> None)

   374       else co2sobj s obj )"

   375 apply (frule vt_grant_os, frule vd_cons, case_tac obj)

   376 apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)

   377 apply (case_tac "cp2sproc (Clone p p' fds shms # s) p'")

   378 apply (drule current_proc_has_sp', simp, simp)

   379 apply ((erule conjE)+, frule_tac p = p in current_proc_has_sec, simp, erule exE, simp)

   380 apply (rule conjI, rule impI, simp)

   381 apply (simp (no_asm_simp) add:cp2sproc_clone tainted_eq_Tainted split:option.splits)

   382 

   383 apply (rule impI, simp add:cf2sfiles_other) 

   384 apply (frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp)

   385 apply (frule_tac ff = list in cf2sfile_other', simp_all)

   386 apply (simp add:is_dir_in_current)

   387 done

   388 

   389 lemma co2sobj_ptrace:

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

   391      case obj of

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

   393                      then (case (cp2sproc s p'') of 

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

   395                            | _       \<Rightarrow> None)

   396                      else if (info_flow_shm s p p'')

   397                           then (case (cp2sproc s p'') of 

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

   399                                 | _       \<Rightarrow> None)

   400                           else co2sobj s (O_proc p'')

   401     | _          \<Rightarrow> co2sobj s obj)"

   402 apply (frule vt_grant_os, frule vd_cons, case_tac obj)

   403 apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other cf2sfiles_other tainted_eq_Tainted)

   404 apply (auto simp:cp2sproc_other tainted_eq_Tainted split:option.splits

   405   dest!:current_proc_has_sec' current_proc_has_sp' intro:info_flow_shm_Tainted)[1]

   406 

   407 apply (frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp)

   408 apply (frule_tac ff = list in cf2sfile_other', simp_all)

   409 apply (simp add:is_dir_in_current)

   410 done

   411 

   412 lemma co2sobj_open:

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

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

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

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

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

   418                         | _       \<Rightarrow> None)

   419                   else co2sobj s (O_file f')

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

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

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

   423                         | _       \<Rightarrow> None)

   424                   else co2sobj s (O_proc p')

   425    | _         \<Rightarrow> co2sobj s obj )"

   426 apply (frule vt_grant_os, frule vd_cons, case_tac obj)

   427 apply (auto simp:cp2sproc_simps cf2sfiles_simps cf2sfile_simps current_files_simps 

   428 is_file_simps tainted_eq_Tainted split:option.splits

   429            dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)

   430 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)

   431 apply (auto simp:cp2sproc_simps cf2sfiles_simps cf2sfile_simps current_files_simps 

   432 is_file_simps tainted_eq_Tainted split:option.splits

   433            dest!:current_proc_has_sp' current_file_has_sfile' intro:info_flow_shm_Tainted)

   434 apply (

   435 apply 

   436 

   437 lemma co2sobj_other:

   438   "\<lbrakk>valid (e # s); alive (e # s) obj; 

   439     \<forall> p f fds. e \<noteq> Execve p f fds;

   440     \<forall> p p' fds shms. e \<noteq> Clone p p' fds shms;

   441     \<forall> p p'. e \<noteq> Ptrace p p';

   442     \<forall> 

   443    \<rbrakk> \<Longrightarrow> co2sobj (e # s) obj = co2sobj s obj"

   444 

   445 lemmas co2sobj_simps = co2sobj_execve co2sobj_clone co2sobj_ptrace