--- a/Dynamic2static.thy	Thu Sep 05 13:23:03 2013 +0800
+++ b/Dynamic2static.thy	Thu Sep 12 13:50:22 2013 +0800
@@ -22,8 +22,8 @@
   "\<lbrakk>alive s obj; co2sobj s obj= Some sobj\<rbrakk> \<Longrightarrow> sobj \<in> (s2ss s)"
 by (simp add:s2ss_def, rule_tac x = obj in exI, simp)
 
-lemma alive_has_sobj:
-  "\<lbrakk>alive s obj; valid s\<rbrakk> \<Longrightarrow> \<exists> sobj. co2sobj s obj = Some sobj"
+lemma tainted_has_sobj:
+  "\<lbrakk>obj \<in> tainted s; valid s\<rbrakk> \<Longrightarrow> \<exists> sobj. co2sobj s obj = Some sobj"
 sorry
 
 lemma t2ts:
@@ -37,12 +37,7 @@
 apply (drule dir_not_tainted, simp)
 apply (drule msgq_not_tainted, simp)
 apply (drule shm_not_tainted, simp)
-apply (case_tac prod1, simp, case_tac prod2, clarsimp)
-apply (rule conjI)
-apply (rule_tac x = "O_msgq nat1" in exI, simp)
-apply (rule conjI) defer
-apply (simp add:cm2smsg_def split:option.splits) 
-sorry
+done
 
 lemma delq_imp_delqm:
   "deleted (O_msgq q) s \<Longrightarrow> deleted (O_msg q m) s"
@@ -57,21 +52,28 @@
     by (auto simp:taintable_def)
   hence vs: "valid s" by (simp add:tainted_is_valid)
   hence static: "s2ss s \<in> static" using d2s_main by auto
-  from tainted have alive: "alive s obj" 
-    using tainted_in_current by auto
-  then obtain sobj where sobj: "co2sobj s obj = Some sobj"
-    using vs alive_has_sobj by blast
+  from tainted obtain sobj where sobj: "co2sobj s obj = Some sobj"
+    using vs tainted_has_sobj by blast
   from undel vs have "\<not> deleted obj s" and init_alive: "init_alive obj" 
     by (auto simp:undeletable_def)
   with vs sobj have "init_obj_related sobj obj"
     apply (case_tac obj, case_tac [!] sobj)
     apply (auto split:option.splits if_splits simp:cp2sproc_def ch2sshm_def cq2smsgq_def cm2smsg_def delq_imp_delqm)
-    apply (frule not_deleted_init_file, simp+) (*
-apply (drule is_file_has_sfile, erule exE)
+    apply (frule not_deleted_init_file, simp+) 
+    apply (drule is_file_has_sfile', simp, erule exE)
     apply (rule_tac x = sf in bexI)
     apply (case_tac list, auto split:option.splits simp:is_init_file_props)[1]
-    apply (simp add:same_inode_files_def cfs2sfiles_def) *)  
-    sorry
+    apply (drule root_is_init_dir', simp)
+    apply (frule not_deleted_init_file, simp, simp)
+    apply (simp add:cf2sfile_def split:option.splits if_splits)
+    apply (simp add:cf2sfiles_def)
+    apply (rule_tac x = list in bexI, simp, simp add:same_inode_files_def not_deleted_init_file)
+
+    apply (frule not_deleted_init_dir, simp+)
+    apply (simp add:cf2sfile_def split:option.splits if_splits)
+    apply (case_tac list, simp add:sroot_def, simp)
+    apply (drule file_dir_conflict, simp+)
+    done
   with tainted t2ts init_alive sobj static
   show ?thesis unfolding taintable_s_def
     apply (rule_tac x = "s2ss s" in bexI, simp)
@@ -189,7 +191,7 @@
 lemma cqm2sms_prop1:
   "\<lbrakk>cqm2sms s q queue = Some sms; sm \<in> set sms\<rbrakk> \<Longrightarrow> \<exists> m. cm2smsg s q m = Some sm"
 apply (induct queue arbitrary:sms)
-apply (auto split:option.splits)
+apply (auto simp:cqm2sms.simps split:option.splits)
 done
 
 lemma sq_sm_prop:
@@ -216,7 +218,11 @@
 apply (case_tac obj, simp_all split:option.splits if_splits)
 apply (drule_tac sm = "(aa, ba, True)" in sq_sm_prop, simp+, erule exE)
 apply (rule_tac x = "O_msg nat m" in exI)
-apply (simp add:cm2smsg_def split:option.splits)
+apply (rule conjI)
+apply simp
+apply (simp add
+apply (simp add:co2sobj.simps)
+apply (simp add:cm2smsg_def split:option.splits if_splits)
 done
 
 lemma has_inode_tainted_aux:

--- a/S2ss_prop.thy	Thu Sep 05 13:23:03 2013 +0800
+++ b/S2ss_prop.thy	Thu Sep 12 13:50:22 2013 +0800
@@ -8,17 +8,29 @@
 
 (* simpset for s2ss*)
 
+lemma co2sobj_some_case:
+  "\<lbrakk>co2sobj s obj = Some sobj; \<And> p. obj = O_proc p \<Longrightarrow> P (O_proc p);
+    \<And> f. obj = O_file f \<Longrightarrow> P (O_file f); \<And> h. obj = O_shm h \<Longrightarrow> P (O_shm h);
+    \<And> f. obj = O_dir f \<Longrightarrow> P (O_dir f); \<And> q. obj = O_msgq q \<Longrightarrow> P (O_msgq q)\<rbrakk>
+   \<Longrightarrow> P obj"
+by (case_tac obj, auto)
+
+lemma co2sobj_execve_alive:
+  "\<lbrakk>alive s obj; co2sobj s obj = Some x; valid (Execve p f fds # s)\<rbrakk>
+   \<Longrightarrow> alive (Execve p f fds # s) obj"
+apply (erule co2sobj_some_case)
+by (auto simp:alive_simps simp del:alive.simps)
 
 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) )"
+           | _ \<Rightarrow> {} )
+     else (case (cp2sproc (Execve p f fds # s) p, cp2sproc s p) of
+             (Some sp, 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> {} ) )"
 apply (frule vd_cons, frule vt_grant_os, simp split:if_splits)
 
 apply (rule conjI, rule impI, (erule exE|erule conjE)+)
@@ -39,41 +51,521 @@
 apply (case_tac "x = S_proc sp (O_proc p \<in> tainted s)")
 apply (rule_tac x = "O_proc p'" in exI)
 apply (simp add:alive_execve co2sobj_execve tainted_eq_Tainted cp2sproc_execve)
+apply (case_tac "obj = O_proc p", simp)
+apply (frule co2sobj_execve_alive, simp, simp)
+apply (frule_tac obj = obj in co2sobj_execve, simp)
+apply (rule_tac x = obj in exI, simp, simp)
 
-apply (case_tac obj, simp_all add:co2sobj_execve alive_simps)
-thm alive_execve
-thm co2sobj_execve
+apply (erule conjE, frule current_proc_has_sp, simp, erule exE, rule impI, simp)
+apply (subgoal_tac "p \<in> current_procs (Execve p f fds # s)") 
+apply (drule_tac p = p and s = "Execve p f fds # s" in current_proc_has_sp, simp)
+apply (erule exE, erule conjE, simp)
+apply (simp add:s2ss_def, rule set_eqI, rule iffI)
+apply (drule CollectD, (erule exE|erule conjE)+)
+apply (case_tac "obj = O_proc p", simp add:tainted_eq_Tainted)
+apply (rule disjI1, simp split:if_splits)
 apply (simp add:co2sobj_execve, rule disjI2)
-apply (rule_tac x = obj in exI, simp split:t_object.splits)
-thm co2sobj_execve
-apply (case_tac obj, auto simp:co2sobj_execve alive_simps tainted_eq_Tainted split:option.splits dest!:current_proc_has_sp')[1]
-apply (simp add:co2sobj_execve)
-apply clarsimp
-thm current_proc_has_sp
+apply (rule conjI,rule_tac x = obj in exI, simp add:alive_simps split:t_object.splits)
+apply (rule notI, simp, case_tac obj)
+apply (erule_tac x = nat in allE, simp add:tainted_eq_Tainted, (simp split:option.splits)+)
+apply (erule disjE, simp)
+apply (rule_tac x = "O_proc p" in exI, simp add:tainted_eq_Tainted)
+apply (erule exE|erule conjE)+
+apply (rule_tac x = obj in exI)
+apply (drule_tac obj = obj in co2sobj_execve_alive, simp+)
+apply (frule_tac obj = obj in co2sobj_execve, simp, simp)
+apply (rule impI, simp add:tainted_eq_Tainted, simp)
+done
+
+lemma s2ss_clone_alive:
+  "\<lbrakk>co2sobj s obj = Some x; alive s obj; obj \<noteq> O_proc p'; valid (Clone p p' fds shms # s)\<rbrakk>
+   \<Longrightarrow> alive (Clone p p' fds shms # s) obj"
+by (erule co2sobj_some_case, auto simp:alive_clone)
+
+lemma s2ss_clone:
+  "valid (Clone p p' fds shms # s) \<Longrightarrow> s2ss (Clone p p' fds shms # s) = (
+     case (cp2sproc (Clone p p' fds shms # s) p') of
+       Some sp \<Rightarrow> s2ss s \<union> {S_proc sp (O_proc p \<in> Tainted s)}
+     | _       \<Rightarrow> {})"
+apply (frule vd_cons, frule vt_grant_os, split option.splits)
+apply (rule conjI, rule impI, drule current_proc_has_sp', simp, simp)
+apply (rule allI, rule impI, simp add:s2ss_def)
+apply (rule set_eqI, rule iffI, drule CollectD, (erule exE|erule conjE)+)
+apply (case_tac "obj = O_proc p'", simp add:tainted_eq_Tainted)
+apply (case_tac "O_proc p' \<in> Tainted s", drule Tainted_in_current, simp+)
+apply (rule disjI1, simp split:if_splits)
+apply (simp add:tainted_eq_Tainted, rule disjI2)
+apply (frule co2sobj_clone, simp)
+apply (rule_tac x = obj in exI, simp add:alive_simps split:t_object.splits)
+
+apply (simp, erule disjE, simp)
+apply (rule_tac x = "O_proc p'" in exI, simp add:tainted_eq_Tainted)
+apply (rule impI, rule notI, drule Tainted_in_current, simp+)
+apply (erule exE| erule conjE)+
+apply (case_tac "obj = O_proc p'", simp)
+apply (rule_tac x = obj in exI)
+apply (frule s2ss_clone_alive, simp+)
+apply (auto simp:co2sobj_clone alive_simps)
+done
+
+definition update_s2ss_shm:: "t_state \<Rightarrow> t_process \<Rightarrow> t_static_state" 
+where
+  "update_s2ss_shm s pfrom \<equiv> s2ss s 
+     \<union> {S_proc sp True| sp p. info_flow_shm s pfrom p \<and> cp2sproc s p = Some sp}
+     - {S_proc sp False | sp p. info_flow_shm s pfrom p \<and> cp2sproc s p = Some sp \<and> 
+           (\<not> (\<exists> p'. \<not> info_flow_shm s pfrom p' \<and> p' \<in> current_procs s \<and> 
+                cp2sproc s p' = Some sp \<and> O_proc p' \<notin> Tainted s))}"
+
+lemma Tainted_ptrace':
+  "valid s \<Longrightarrow> Tainted (Ptrace p p' # s) = 
+     (if (O_proc p \<in> Tainted s \<and> O_proc p' \<notin> Tainted s)
+      then Tainted s \<union> {O_proc p'' | p''. info_flow_shm s p' p''}
+      else if (O_proc p' \<in> Tainted s \<and> O_proc p \<notin> Tainted s)
+           then Tainted s \<union> {O_proc p'' | p''. info_flow_shm s p p''}
+                else Tainted s)"
+using info_flow_shm_Tainted by auto
+
+lemma co2sobj_some_caseD:
+  "\<lbrakk>co2sobj s obj = Some sobj; \<And> p. \<lbrakk>co2sobj s obj = Some sobj; obj = O_proc p\<rbrakk> \<Longrightarrow> P (O_proc p);
+    \<And> f. \<lbrakk>co2sobj s obj = Some sobj; obj = O_file f\<rbrakk> \<Longrightarrow> P (O_file f); 
+    \<And> h. \<lbrakk>co2sobj s obj = Some sobj; obj = O_shm h\<rbrakk> \<Longrightarrow> P (O_shm h);
+    \<And> f. \<lbrakk>co2sobj s obj = Some sobj; obj = O_dir f\<rbrakk> \<Longrightarrow> P (O_dir f); 
+    \<And> q. \<lbrakk>co2sobj s obj = Some sobj; obj = O_msgq q\<rbrakk> \<Longrightarrow> P (O_msgq q)\<rbrakk>
+   \<Longrightarrow> P obj"
+by (case_tac obj, auto)
+
+lemma s2ss_ptrace1_aux: "x \<notin> {x. P x} \<Longrightarrow> \<not> P x" by simp
+
+lemma s2ss_ptrace1:
+  "\<lbrakk>valid (Ptrace p p' # s); O_proc p \<in> Tainted s; O_proc p' \<notin> Tainted s\<rbrakk>
+   \<Longrightarrow> s2ss (Ptrace p p' # s) = update_s2ss_shm s p'"
+unfolding update_s2ss_shm_def s2ss_def
+apply (frule vd_cons, rule set_eqI, rule iffI)
+apply (drule CollectD, (erule exE|erule conjE)+)
+apply (erule co2sobj_some_caseD)
+apply (rule DiffI)
+apply (case_tac "O_proc pa \<in> Tainted s")
+apply (rule UnI1, simp, rule_tac x = "O_proc pa" in exI)
+apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)
+apply (case_tac "info_flow_shm s p' pa")
+apply (rule UnI2, rule CollectI, simp only:co2sobj.simps split:option.splits)
+apply (drule current_proc_has_sp', simp, simp)
+apply (rule_tac x = a in exI, rule_tac x = pa in exI)
+apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)
+apply (rule UnI1, simp)
+apply (rule_tac x = "O_proc pa" in exI)
+apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)
+apply (rule notI, clarsimp simp:cp2sproc_other tainted_eq_Tainted split:option.splits)
+apply (erule_tac x = pa in allE, simp)
+
+apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI,
+       auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]
+apply (simp)
+apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI,
+       auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]
+apply (simp split:option.splits)
+apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI,
+       auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]
+apply (simp split:option.splits)
+apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI,
+       auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]
+apply (simp split:option.splits)
+
+apply (erule DiffE, drule s2ss_ptrace1_aux, erule UnE)
+apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)
+apply (erule co2sobj_some_caseD)
+apply (case_tac "O_proc pa \<in> Tainted s")
+apply (rule_tac x = "O_proc pa" in exI)
+apply (clarsimp simp add:tainted_eq_Tainted cp2sproc_other split:option.splits)
+apply (case_tac "info_flow_shm s p' pa", simp only:co2sobj.simps split:option.splits)
+apply (drule current_proc_has_sp', simp, simp)
+apply (drule Meson.not_exD, erule_tac x = a in allE, drule Meson.not_exD, erule_tac x = pa in allE)
+apply (simp add:tainted_eq_Tainted, (erule exE|erule conjE)+)
+apply (rule_tac x = "O_proc p'a" in exI)
+apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)
+apply (rule_tac x = "O_proc pa" in exI)
+apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)
+
+apply (rule_tac x = obj in exI,
+       auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]
+apply (rule_tac x = obj in exI,
+       auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]
+apply (rule_tac x = obj in exI,
+       auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]
+apply (rule_tac x = obj in exI,
+       auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]
+
+apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)
+apply (rule_tac x = "O_proc pa" in exI)
+apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted info_shm_flow_in_procs)
+done
+
+lemma s2ss_ptrace2:
+  "\<lbrakk>valid (Ptrace p p' # s); O_proc p' \<in> Tainted s; O_proc p \<notin> Tainted s\<rbrakk>
+   \<Longrightarrow> s2ss (Ptrace p p' # s) = update_s2ss_shm s p"
+unfolding update_s2ss_shm_def s2ss_def
+apply (frule vd_cons, rule set_eqI, rule iffI)
+apply (drule CollectD, (erule exE|erule conjE)+)
+apply (erule co2sobj_some_caseD)
+apply (rule DiffI)
+apply (case_tac "O_proc pa \<in> Tainted s")
+apply (rule UnI1, simp, rule_tac x = "O_proc pa" in exI)
+apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)
+apply (case_tac "info_flow_shm s p pa")
+apply (rule UnI2, rule CollectI, simp only:co2sobj.simps split:option.splits)
+apply (drule current_proc_has_sp', simp, simp)
+apply (rule_tac x = a in exI, rule_tac x = pa in exI)
+apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)
+apply (rule UnI1, simp)
+apply (rule_tac x = "O_proc pa" in exI)
+apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)
+apply (rule notI, clarsimp simp:cp2sproc_other tainted_eq_Tainted split:option.splits)
+apply (erule_tac x = pa in allE, simp)
+
+apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI,
+       auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]
+apply (simp)
+apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI,
+       auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]
+apply (simp split:option.splits)
+apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI,
+       auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]
+apply (simp split:option.splits)
+apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI,
+       auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]
+apply (simp split:option.splits)
+
+apply (erule DiffE, drule s2ss_ptrace1_aux, erule UnE)
+apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)
+apply (erule co2sobj_some_caseD)
+apply (case_tac "O_proc pa \<in> Tainted s")
+apply (rule_tac x = "O_proc pa" in exI)
+apply (clarsimp simp add:tainted_eq_Tainted cp2sproc_other split:option.splits)
+apply (case_tac "info_flow_shm s p pa", simp only:co2sobj.simps split:option.splits)
+apply (drule current_proc_has_sp', simp, simp)
+apply (drule Meson.not_exD, erule_tac x = a in allE, drule Meson.not_exD, erule_tac x = pa in allE)
+apply (simp add:tainted_eq_Tainted, (erule exE|erule conjE)+)
+apply (rule_tac x = "O_proc p'a" in exI)
+apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)
+apply (rule_tac x = "O_proc pa" in exI)
+apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted split:option.splits)
+
+apply (rule_tac x = obj in exI,
+       auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]
+apply (rule_tac x = obj in exI,
+       auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]
+apply (rule_tac x = obj in exI,
+       auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]
+apply (rule_tac x = obj in exI,
+       auto split:option.splits simp:co2sobj_ptrace alive_simps simp del:co2sobj.simps)[1]
+
+apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)
+apply (rule_tac x = "O_proc pa" in exI)
+apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted info_shm_flow_in_procs)
+done
+
+lemma s2ss_ptrace3:
+  "\<lbrakk>valid (Ptrace p p' # s); (O_proc p' \<in> Tainted s) = (O_proc p \<in> Tainted s)\<rbrakk>
+   \<Longrightarrow> s2ss (Ptrace p p' # s) = s2ss s"
+unfolding s2ss_def
+apply (frule vd_cons, rule set_eqI, rule iffI)
+apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)
+apply (rule_tac x = obj in exI)
+apply (frule alive_other, simp+)
+apply (frule_tac obj = obj in co2sobj_ptrace, simp)
+apply (auto simp add:tainted_eq_Tainted split:t_object.splits option.splits if_splits
+  intro:info_flow_shm_Tainted)[1]
+
+apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)
+apply (rule_tac x = obj in exI)
+apply (frule alive_other, simp+)
+apply (frule_tac obj = obj in co2sobj_ptrace, simp)
+apply (auto simp add:tainted_eq_Tainted split:t_object.splits option.splits if_splits 
+  intro:info_flow_shm_Tainted)
+done
+
+lemma s2ss_ptrace:
+  "valid (Ptrace p p' # s) \<Longrightarrow> s2ss (Ptrace p p' # s) = (
+     if (O_proc p \<in> Tainted s \<and> O_proc p' \<notin> Tainted s) 
+     then update_s2ss_shm s p'
+     else if (O_proc p' \<in> Tainted s \<and> O_proc p \<notin> Tainted s)
+          then update_s2ss_shm s p
+          else s2ss s                                   )"
+apply (frule vt_grant_os, frule vd_cons)
+apply (simp add:s2ss_ptrace2 s2ss_ptrace1 split:if_splits)
+by (auto dest:s2ss_ptrace3)
 
-apply (auto simp:s2ss_def co2sobj_execve split:option.splits)
+lemma s2ss_kill:
+  "valid (Kill p p' # s) \<Longrightarrow> s2ss (Kill p p' # s) = (
+     if (\<exists> p''. p'' \<in> current_procs s \<and> p'' \<noteq> p' \<and> co2sobj s (O_proc p'') = co2sobj s (O_proc p'))
+     then s2ss s 
+     else (case (co2sobj s (O_proc p')) of
+             Some sp \<Rightarrow> s2ss s - {sp}
+           | _       \<Rightarrow> {}))"
+apply (frule vt_grant_os, frule vd_cons)
+unfolding s2ss_def
+apply (simp split:if_splits, rule conjI)
+apply (rule impI, (erule exE|erule conjE)+)
+apply (split option.splits)
+apply (drule current_proc_has_sp', simp, simp)
+apply (simp split: option.splits, (erule conjE)+)
+apply (rule set_eqI, rule iffI, erule CollectE, (erule exE|erule conjE)+, rule CollectI)
+apply (rule_tac x = obj in exI)
+apply (simp add:co2sobj_kill tainted_eq_Tainted alive_kill split:t_object.splits if_splits)
+apply (erule CollectE, erule exE, erule conjE, rule CollectI)
+apply (erule co2sobj_some_caseD)
+apply (case_tac "pa = p'")
+apply (rule_tac x = "O_proc p''" in exI)
+apply (simp add:cp2sproc_kill tainted_eq_Tainted alive_kill
+  split:t_object.splits if_splits option.splits)
+apply (rule_tac x = "O_proc pa" in exI)
+apply (clarsimp simp add:cp2sproc_kill tainted_eq_Tainted alive_kill
+  split:t_object.splits if_splits option.splits)
+apply (rule_tac x = obj in exI, frule alive_kill, simp add:co2sobj_kill del:co2sobj.simps)+
+
+apply (rule impI, erule conjE, frule current_proc_has_sp, simp, erule exE, simp)
+apply (rule set_eqI, rule iffI)
+apply (erule CollectE, erule exE, erule conjE, rule DiffI)
+apply (rule CollectI, rule_tac x = obj in exI)
+apply (simp add:co2sobj_kill tainted_eq_Tainted alive_kill split:t_object.splits if_splits)
+apply (rule notI, simp, case_tac obj)
+apply (erule_tac x = nat in allE)
+apply (simp add:co2sobj_kill cp2sproc_kill tainted_eq_Tainted split:option.splits)
+apply (simp split:option.splits)+
+apply (erule co2sobj_some_caseD)
+apply (case_tac "pa = p'")
+apply (rule_tac x = "O_proc p''" in exI)
+apply (simp add:cp2sproc_kill tainted_eq_Tainted alive_kill
+  split:t_object.splits if_splits option.splits)
+apply (rule_tac x = "O_proc pa" in exI)
+apply (clarsimp simp add:cp2sproc_kill tainted_eq_Tainted alive_kill
+  split:t_object.splits if_splits option.splits)
+apply (rule_tac x = obj in exI, frule alive_kill, simp add:co2sobj_kill del:co2sobj.simps)+
+done
+
+lemma s2ss_exit:
+  "valid (Exit p # s) \<Longrightarrow> s2ss (Exit p # s) = (
+     if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (O_proc p') = co2sobj s (O_proc p))
+     then s2ss s 
+     else (case (co2sobj s (O_proc p)) of
+             Some sp \<Rightarrow> s2ss s - {sp}
+           | _       \<Rightarrow> {}))"
+apply (frule vt_grant_os, frule vd_cons)
+unfolding s2ss_def
+apply (simp split:if_splits, rule conjI)
+apply (rule impI, (erule exE|erule conjE)+)
+apply (split option.splits)
+apply (drule current_proc_has_sp', simp, simp)
+apply (simp split: option.splits, (erule conjE)+)
+apply (rule set_eqI, rule iffI, erule CollectE, (erule exE|erule conjE)+, rule CollectI)
+apply (rule_tac x = obj in exI)
+apply (simp add:co2sobj_exit tainted_eq_Tainted alive_exit split:t_object.splits if_splits)
+apply (erule CollectE, erule exE, erule conjE, rule CollectI)
+apply (erule co2sobj_some_caseD)
+apply (case_tac "pa = p")
+apply (rule_tac x = "O_proc p'" in exI)
+apply (simp add:cp2sproc_exit tainted_eq_Tainted alive_exit
+  split:t_object.splits if_splits option.splits)
+apply (rule_tac x = "O_proc pa" in exI)
+apply (clarsimp simp add:cp2sproc_exit tainted_eq_Tainted alive_exit
+  split:t_object.splits if_splits option.splits)
+apply (rule_tac x = obj in exI, frule alive_exit, simp add:co2sobj_exit del:co2sobj.simps)+
+
+apply (rule impI, frule current_proc_has_sp, simp, erule exE, simp)
+apply (rule set_eqI, rule iffI)
+apply (erule CollectE, erule exE, erule conjE, rule DiffI)
+apply (rule CollectI, rule_tac x = obj in exI)
+apply (simp add:co2sobj_exit tainted_eq_Tainted alive_exit split:t_object.splits if_splits)
+apply (rule notI, simp, case_tac obj)
+apply (erule_tac x = nat in allE)
+apply (simp add:co2sobj_exit cp2sproc_exit tainted_eq_Tainted split:option.splits)
+apply (simp split:option.splits)+
+apply (erule co2sobj_some_caseD)
+apply (case_tac "pa = p")
+apply (rule_tac x = "O_proc p'" in exI)
+apply (simp add:cp2sproc_exit tainted_eq_Tainted alive_exit
+  split:t_object.splits if_splits option.splits)
+apply (rule_tac x = "O_proc pa" in exI)
+apply (clarsimp simp add:cp2sproc_exit tainted_eq_Tainted alive_exit
+  split:t_object.splits if_splits option.splits)
+apply (rule_tac x = obj in exI, frule alive_exit, simp add:co2sobj_exit del:co2sobj.simps)+
+done
+
+lemma alive_has_sobj':
+  "\<lbrakk>co2sobj s obj = None; valid s\<rbrakk> \<Longrightarrow> \<not> alive s obj"
+apply (case_tac obj)
+apply (auto split:option.splits)
+oops
+
+declare co2sobj.simps [simp del]
+
+lemma co2sobj_open_none:
+  "\<lbrakk>valid (Open p f flag fd None # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Open p f flag fd None # s) obj = (
+      if (obj = O_proc p) 
+      then (case (cp2sproc (Open p f flag fd None # 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)
+apply (frule_tac obj = obj in co2sobj_open, simp add:alive_open)
+apply (auto split:t_object.splits option.splits dest!:current_proc_has_sp')
+done
+
+lemma co2sobj_open_some:
+  "\<lbrakk>valid (Open p f flag fd (Some i) # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Open p f flag fd (Some i) # s) obj = (
+      if (obj = O_proc p) 
+      then (case (cp2sproc (Open p f flag fd (Some i) # s) p) of
+              Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s))
+           | _       \<Rightarrow> None)
+      else if (obj = O_file f) 
+           then (case (cf2sfile (Open p f flag fd (Some i) # s) f) of
+                   Some sf \<Rightarrow> Some (S_file {sf} (O_proc p \<in> Tainted s))
+                 | _       \<Rightarrow> None)
+           else co2sobj s obj)"
+apply (frule vt_grant_os, frule vd_cons)
+apply (frule_tac obj = obj in co2sobj_open, simp add:alive_open)
+apply (auto split:t_object.splits option.splits dest!:current_proc_has_sp')
+done
 
+lemma alive_co2sobj_some_open_none:
+  "\<lbrakk>co2sobj s obj = Some sobj; alive s obj; valid (Open p f flag fd None # s)\<rbrakk>
+   \<Longrightarrow> alive (Open p f flag fd None # s) obj"
+by (erule co2sobj_some_caseD, auto simp:alive_simps is_file_simps is_dir_simps)
+
+lemma alive_co2sobj_some_open_none':
+  "\<lbrakk>co2sobj (Open p f flag fd None # s) obj = Some sobj; alive (Open p f flag fd None # s) obj; 
+    valid (Open p f flag fd None # s)\<rbrakk> \<Longrightarrow> alive s obj"
+by (erule co2sobj_some_caseD, auto simp:alive_simps is_file_simps is_dir_simps)
+
+lemma co2sobj_proc_obj:
+  "\<lbrakk>co2sobj s obj = Some x; co2sobj s (O_proc p) = Some x\<rbrakk>
+   \<Longrightarrow> \<exists> p'. obj = O_proc p'"
+by (case_tac obj, auto simp:co2sobj.simps split:option.splits)
+
+lemma s2ss_open_none:
+  "valid (Open p f flag fd None # s) \<Longrightarrow> s2ss (Open p f flag fd None # s) = (
+      case (co2sobj s (O_proc p), co2sobj (Open p f flag fd None # s) (O_proc p)) of
+        (Some sp, Some sp') \<Rightarrow> 
+           if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (O_proc p') = Some sp)
+           then s2ss s \<union> {sp'}
+           else s2ss s - {sp} \<union> {sp'} 
+      | _                   \<Rightarrow> {} )"
+unfolding s2ss_def
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac "co2sobj s (O_proc p)", simp add:co2sobj.simps split:option.splits)
+apply (drule current_proc_has_sp', simp, simp)
+apply (case_tac "co2sobj (Open p f flag fd None # s) (O_proc p)")
+apply (simp add:co2sobj.simps split:option.splits)
+apply (drule current_proc_has_sp', simp, simp)
+apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE, simp)
+apply (frule_tac obj = obj in alive_co2sobj_some_open_none', simp, simp)
+apply (rule conjI, rule impI, erule exE, (erule conjE)+)
+apply (rule Meson.disj_comm, rule disjCI, case_tac "obj = O_proc p", simp)
+apply (rule_tac x = obj in exI, simp add:co2sobj_open_none)
+apply (rule impI)
+apply (case_tac "obj = O_proc p", simp)
+apply (rule Meson.disj_comm, rule disjCI, rule conjI)
+apply (rule_tac x = obj in exI, simp add:co2sobj_open_none)
+apply (simp add:co2sobj_open_none split:option.splits)
+apply (rule notI)
+apply (frule co2sobj_proc_obj, simp, erule exE)
+apply (erule_tac x = p' in allE, simp)
+
+apply (simp split:if_splits)
+apply (erule disjE, rule_tac x = "O_proc p" in exI, simp)
+apply (erule exE, erule conjE, case_tac "obj = O_proc p")
+apply (rule_tac x = "O_proc p'" in exI, simp add:co2sobj_open_none)
+apply (rule_tac x = obj in exI, simp add:co2sobj_open_none alive_co2sobj_some_open_none)
+apply (erule disjE, rule_tac x = "O_proc p" in exI, simp)
+apply (erule conjE, erule exE, erule conjE, case_tac "obj = O_proc p")
+apply (rule_tac x = "O_proc p'" in exI, simp add:co2sobj_open_none)
+apply (rule_tac x = obj in exI, simp add:co2sobj_open_none alive_co2sobj_some_open_none)
+done
+
+lemma alive_co2sobj_some_open_some:
+  "\<lbrakk>alive s obj; valid (Open p f flag fd (Some i) # s)\<rbrakk>
+   \<Longrightarrow> alive (Open p f flag fd (Some i) # s) obj"
+by (case_tac obj, auto simp:alive_simps is_file_simps is_dir_simps)
+
+lemma alive_co2sobj_some_open_some':
+  "\<lbrakk>co2sobj (Open p f flag fd (Some i) # s) obj = Some sobj; alive (Open p f flag fd (Some i) # s) obj; 
+    valid (Open p f flag fd (Some i) # s); obj \<noteq> O_file f\<rbrakk> \<Longrightarrow> alive s obj"
+by (erule co2sobj_some_caseD, auto simp:alive_simps is_file_simps is_dir_simps)
+
+lemma s2ss_open_some:
+  "valid (Open p f flag fd (Some i) # s) \<Longrightarrow> s2ss (Open p f flag fd (Some i) # s) = (
+      case (co2sobj s (O_proc p), co2sobj (Open p f flag fd (Some i) # s) (O_proc p),
+            co2sobj (Open p f flag fd (Some i) # s) (O_file f)) of
+        (Some sp, Some sp', Some sf) \<Rightarrow> 
+           if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (O_proc p') = Some sp)
+           then s2ss s \<union> {sp', sf} 
+           else s2ss s - {sp} \<union> {sp', sf} 
+      | _                   \<Rightarrow> {} )"
+unfolding s2ss_def
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac "co2sobj s (O_proc p)", simp add:co2sobj.simps split:option.splits)
+apply (drule current_proc_has_sp', simp, simp)
+apply (case_tac "co2sobj (Open p f flag fd (Some i) # s) (O_proc p)")
+apply (simp add:co2sobj.simps split:option.splits)
+apply (drule current_proc_has_sp', simp, simp)
+apply (case_tac "co2sobj (Open p f flag fd (Some i) # s) (O_file f)")
+apply (simp add:co2sobj.simps split:option.splits)
+apply (clarsimp split del:if_splits)
+
+apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE)
+apply (split if_splits, rule conjI, rule impI, erule exE, erule conjE, erule conjE)
+apply (case_tac "obj = O_proc p", simp, case_tac "obj = O_file f", simp)
+apply (rule UnI1, rule CollectI, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in alive_co2sobj_some_open_some', simp+)
+apply (simp add:co2sobj_open split:t_object.splits)
+apply (rule impI, case_tac "obj = O_proc p", simp, case_tac "obj = O_file f", simp)
+apply (rule UnI1, rule DiffI, rule CollectI, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in alive_co2sobj_some_open_some', simp+)
+apply (simp add:co2sobj_open split:t_object.splits)
+apply (frule_tac obj = obj in co2sobj_open_some, simp+)
+apply (simp add:alive_co2sobj_some_open_some', simp)
+apply (rule notI)
+apply (frule_tac obj = obj and p = p in co2sobj_proc_obj, simp+, erule exE)
+apply (erule_tac x = p' in allE, simp)
+
+apply (simp split:if_splits, erule disjE)
+apply (rule_tac x = "O_proc p" in exI, simp)
+apply (erule disjE, rule_tac x = "O_file f" in exI, simp add:is_file_simps)
+apply (erule exE, erule conjE)
+apply (case_tac "obj = O_proc p", simp)
+apply (rule_tac x = "O_proc p'" in exI, simp add:co2sobj_open_some)
+apply (case_tac "obj = O_file f", simp add:is_file_in_current)
+apply (rule_tac x = obj in exI, simp add:co2sobj_open_some alive_co2sobj_some_open_some)
+apply (erule disjE, rule_tac x = "O_proc p" in exI, simp)
+apply (erule disjE, rule_tac x = "O_file f" in exI, simp add:is_file_simps)
+apply (erule conjE, erule exE, erule conjE)
+apply (case_tac "obj = O_proc p", simp)
+apply (case_tac "obj = O_file f", simp add:is_file_in_current)
+apply (rule_tac x = obj in exI, simp add:co2sobj_open_some alive_co2sobj_some_open_some)
+done
+
+lemma s2ss_open:
+  "valid (Open p f flag fd opt # s) \<Longrightarrow> s2ss (Open p f flag fd opt # s) = (
+     if opt = None
+     then (case (co2sobj s (O_proc p), co2sobj (Open p f flag fd opt # s) (O_proc p)) of
+        (Some sp, Some sp') \<Rightarrow> 
+           if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (O_proc p') = Some sp)
+           then s2ss s \<union> {sp'}
+           else s2ss s - {sp} \<union> {sp'} 
+      | _                   \<Rightarrow> {} )
+     else (case (co2sobj s (O_proc p), co2sobj (Open p f flag fd opt # s) (O_proc p),
+            co2sobj (Open p f flag fd opt # s) (O_file f)) of
+        (Some sp, Some sp', Some sf) \<Rightarrow> 
+           if (\<exists> p'. p' \<in> current_procs s \<and> p' \<noteq> p \<and> co2sobj s (O_proc p') = Some sp)
+           then s2ss s \<union> {sp', sf} 
+           else s2ss s - {sp} \<union> {sp', sf} 
+      | _                   \<Rightarrow> {} ) )"
+apply (case_tac opt)
+apply (simp add:s2ss_open_some s2ss_open_none)+
+done
+
+lemma
 
 
-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)
+lemmas s2ss_simps = s2ss_execve s2ss_clone s2ss_ptrace s2ss_kill s2ss_exit s2ss_open
 
-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)
\ No newline at end of file

--- a/Static.thy	Thu Sep 05 13:23:03 2013 +0800
+++ b/Static.thy	Thu Sep 12 13:50:22 2013 +0800
@@ -172,7 +172,6 @@
 | "is_many (S_dir  sf      ) = is_many_sfile sf"
 | "is_many (S_msgq sq      ) = is_many_smsgq sq"
 | "is_many (S_shm  sh      ) = is_many_sshm  sh"
-| "is_many _                 = False"
 
 (*
 fun update_ss_sp:: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state"

--- a/Static_type.thy	Thu Sep 05 13:23:03 2013 +0800
+++ b/Static_type.thy	Thu Sep 12 13:50:22 2013 +0800
@@ -77,9 +77,9 @@
 | S_file "t_sfile set" "bool"  (* here sfile set is for "linking", tainted is the inode *)
 | S_dir  "t_sfile"     
 | S_msgq "t_smsgq"
-| S_shm  "t_sshm"
+| S_shm  "t_sshm"  (*
 | S_msg  "t_smsgq"    "t_smsg"
-
+*)
 (*
 datatype t_tainted_sobj = 
   TS_proc "t_sproc"     "bool"

--- a/Tainted_prop.thy	Thu Sep 05 13:23:03 2013 +0800
+++ b/Tainted_prop.thy	Thu Sep 12 13:50:22 2013 +0800
@@ -15,9 +15,9 @@
      (if (O_file f) \<in> Tainted s then Tainted s \<union> {O_proc p} else Tainted s)"
 | "Tainted (Kill p p' # s) = Tainted s - {O_proc p'}"
 | "Tainted (Ptrace p p' # s) = 
-     (if (O_proc p) \<in> Tainted s 
+     (if (O_proc p \<in> Tainted s)
       then Tainted s \<union> {O_proc p'' | p''. info_flow_shm s p' p''}
-      else if (O_proc p') \<in> Tainted s 
+      else if (O_proc p' \<in> Tainted s)
            then Tainted s \<union> {O_proc p'' | p''. info_flow_shm s p p''}
                 else Tainted s)"
 | "Tainted (Exit p # s) = Tainted s - {O_proc p}"