# HG changeset patch
# User chunhan
# Date 1382578893 -28800
# Node ID 051b0ee98852a9427d06b05f9044874e81502007
# Parent  9fc384154e844684350dfeec315438bf02aa6efb
restructured

diff -r 9fc384154e84 -r 051b0ee98852 Dynamic2static.thy
--- a/Dynamic2static.thy	Tue Oct 22 10:08:27 2013 +0800
+++ b/Dynamic2static.thy	Thu Oct 24 09:41:33 2013 +0800
@@ -54,6 +54,112 @@
 
 sorry
 
+definition enrich:: "t_state \<Rightarrow> t_object set \<Rightarrow> t_state \<Rightarrow> bool"
+where
+  "enrich s objs s' \<equiv> \<forall> obj \<in> objs. \<exists> obj'. obj' \<notin> objs \<and> alive s' obj \<and> co2sobj s' obj' = co2sobj s' obj"
+
+definition reserve:: "t_state \<Rightarrow> t_object set \<Rightarrow> t_state \<Rightarrow> bool"
+where
+  "reserve s objs s' \<equiv> \<forall> obj. alive s obj \<longrightarrow> alive s' obj \<and> co2sobj s' obj = co2sobj s obj"
+
+definition enrichable :: "t_state \<Rightarrow> t_object set \<Rightarrow> bool"
+where
+  "enrichable s objs \<equiv> \<exists> s'. valid s' \<and> s2ss s' = s2ss s \<and> enrich s objs s' \<and> reserve s objs s'"
+
+definition is_created :: "t_state \<Rightarrow> t_object \<Rightarrow> bool"
+where
+  "is_created s obj \<equiv> init_alive obj \<longrightarrow> deleted obj s"
+
+definition is_inited :: "t_state \<Rightarrow> t_object \<Rightarrow> bool"
+where
+  "is_inited s obj \<equiv> init_alive obj \<and> \<not> deleted obj s"
+
+lemma is_inited_eq_not_created:
+  "is_inited s obj = (\<not> is_created s obj)"
+by (auto simp:is_created_def is_inited_def)
+
+(* recorded in our static world *)
+fun recorded :: "t_object \<Rightarrow> bool"
+where
+  "recorded (O_proc p)     = True"
+| "recorded (O_file f)     = True"
+| "recorded (O_dir  f)     = True"
+| "recorded (O_node n)     = False" (* cause socket is temperary not considered *)
+| "recorded (O_shm  h)     = True"
+| "recorded (O_msgq q)     = True"
+| "recorded _              = False"
+
+lemma enrichability: 
+  "\<lbrakk>valid s; \<forall> obj \<in> objs. alive s obj \<and> is_created s obj \<and> recorded obj\<rbrakk>
+   \<Longrightarrow> enrichable s objs"
+proof (induct s arbitrary:objs)
+  case Nil
+  hence "objs = {}" 
+    apply (auto simp:is_created_def)
+    apply (erule_tac x = x in ballE)
+    apply (auto simp:init_alive_prop)
+    done
+  thus ?case using Nil unfolding enrichable_def enrich_def reserve_def
+    by (rule_tac x = "[]" in exI, auto)
+next
+  case (Cons e s)
+  hence p1: "\<And> objs. \<forall> obj \<in> objs. alive s obj \<and> is_created s obj \<and> recorded obj \<Longrightarrow> enrichable s objs"
+    and p2: "valid (e # s)" and p3: "\<forall>obj\<in>objs. alive (e # s) obj \<and> is_created (e # s) obj \<and> recorded obj"
+    and os: "os_grant s e" and se: "grant s e" and vd: "valid s"
+    by (auto dest:vt_grant_os vd_cons vt_grant)
+  show ?case
+  proof (cases e)
+    case (Execve p f fds)
+    hence p4: "e = Execve p f fds" by simp
+    from p3 have p5: "is_inited s (O_proc p) \<Longrightarrow> (O_proc p) \<notin> objs"
+      by (auto simp:is_created_def is_inited_def p4 elim!:ballE[where x = "O_proc p"])
+    show "enrichable (e # s) objs"
+    proof (case "is_inited s (O_proc p)")
+      apply (simp add:enrichable_def p4)
+
+      
+  
+    apply auto
+    apply (auto simp:enrichable_def)
+apply (induct s)
+
+
+
+done
+
+
+(* for the object set, there exists another trace which keeps this objects but also add new identical objects
+ * that have the same static-signature
+ *)
+
+definition potential_trace:: "t_state \<Rightarrow> bool"
+where
+  "potential_trace s \<equiv> \<forall> obj. alive s obj \<and> is_created s obj \<longrightarrow> 
+      (\<exists> s' obj'. valid s' \<and> s2ss s' = ss \<and> obj' \<noteq> obj \<and> co2sobj s' obj = co2sobj s' obj)
+     "
+
+lemma s2d_main_general:
+  "ss \<in> static \<Longrightarrow> \<exists> s. valid s \<and> s2ss s = ss \<and> (\<forall> obj \<in> objs. alive s obj \<and> is_created s obj \<longrightarrow> (\<exists> s'. valid s' \<and> s2ss s' = ss \<and> (\<exists> obj'. obj' \<noteq> obj \<and> co2sobj s' obj = co2sobj s' obj')))"
+apply (erule static.induct)
+apply (rule_tac x = "[]" in exI, simp add:s2ss_nil_prop valid.intros) defer
+
+apply (erule exE|erule conjE)+
+
+apply (simp add:update_ss_def)
+
+sorry
+
+lemma s2d_main:
+  "ss \<in> static \<Longrightarrow> \<exists> s. valid s \<and> s2ss s = ss"
+apply (erule static.induct)
+apply (rule_tac x = "[]" in exI, simp add:s2ss_nil_prop valid.intros)
+
+apply (erule exE|erule conjE)+
+
+apply (simp add:update_ss_def)
+
+sorry
+
 
 lemma t2ts:
   "obj \<in> tainted s \<Longrightarrow> co2sobj s obj = Some sobj \<Longrightarrow> tainted_s (s2ss s) sobj"
@@ -219,14 +325,6 @@
 
 (************** static \<rightarrow> dynamic ***************)
 
-lemma s2d_main:
-  "ss \<in> static \<Longrightarrow> \<exists> s. valid s \<and> s2ss s = ss"
-apply (erule static.induct)
-apply (rule_tac x = "[]" in exI, simp add:s2ss_nil_prop valid.intros)
-
-apply (erule exE|erule conjE)+
-
-sorry
 
 lemma set_eq_D:
   "\<lbrakk>x \<in> S; {x. P x} = S\<rbrakk> \<Longrightarrow> P x"
diff -r 9fc384154e84 -r 051b0ee98852 Dynamic_static.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Dynamic_static.thy	Thu Oct 24 09:41:33 2013 +0800
@@ -0,0 +1,153 @@
+theory Dynamic_static
+imports Main Flask Static Init_prop Valid_prop Tainted_prop Delete_prop Co2sobj_prop S2ss_prop S2ss_prop2
+begin
+
+context tainting_s begin
+
+definition init_ss_eq:: "t_static_state \<Rightarrow> t_static_state \<Rightarrow> bool" (infix "\<doteq>" 100)
+where
+  "ss \<doteq> ss' \<equiv> ss \<subseteq> ss' \<and> {sobj. is_init_sobj sobj \<and> sobj \<in> ss'} \<subseteq> ss"
+
+lemma [simp]: "ss \<doteq> ss"
+by (auto simp:init_ss_eq_def)
+
+definition init_ss_in:: "t_static_state \<Rightarrow> t_static_state set \<Rightarrow> bool" (infix "\<propto>" 101)
+where
+  "ss \<propto> sss \<equiv> \<exists> ss' \<in> sss. ss \<doteq> ss'"
+
+lemma s2ss_included_sobj:
+  "\<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 init_ss_in_prop:
+  "\<lbrakk>s2ss s \<propto> static; co2sobj s obj = Some sobj; alive s obj; init_obj_related sobj obj\<rbrakk>
+   \<Longrightarrow> \<exists> ss \<in> static. sobj \<in> ss"
+apply (simp add:init_ss_in_def init_ss_eq_def)
+apply (erule bexE, erule conjE)
+apply (rule_tac x = ss' in bexI, auto dest!:s2ss_included_sobj)
+done
+
+
+
+
+
+definition enrich:: "t_state \<Rightarrow> t_object set \<Rightarrow> t_state \<Rightarrow> bool"
+where
+  "enrich s objs s' \<equiv> \<forall> obj \<in> objs. \<exists> obj'. obj' \<notin> objs \<and> alive s' obj \<and> co2sobj s' obj' = co2sobj s' obj"
+
+definition reserve:: "t_state \<Rightarrow> t_object set \<Rightarrow> t_state \<Rightarrow> bool"
+where
+  "reserve s objs s' \<equiv> \<forall> obj. alive s obj \<longrightarrow> alive s' obj \<and> co2sobj s' obj = co2sobj s obj"
+
+definition enrichable :: "t_state \<Rightarrow> t_object set \<Rightarrow> bool"
+where
+  "enrichable s objs \<equiv> \<exists> s'. valid s' \<and> s2ss s' = s2ss s \<and> enrich s objs s' \<and> reserve s objs s'"
+
+definition is_created :: "t_state \<Rightarrow> t_object \<Rightarrow> bool"
+where
+  "is_created s obj \<equiv> init_alive obj \<longrightarrow> deleted obj s"
+
+definition is_inited :: "t_state \<Rightarrow> t_object \<Rightarrow> bool"
+where
+  "is_inited s obj \<equiv> init_alive obj \<and> \<not> deleted obj s"
+
+lemma is_inited_eq_not_created:
+  "is_inited s obj = (\<not> is_created s obj)"
+by (auto simp:is_created_def is_inited_def)
+
+(* recorded in our static world *)
+fun recorded :: "t_object \<Rightarrow> bool"
+where
+  "recorded (O_proc p)     = True"
+| "recorded (O_file f)     = True"
+| "recorded (O_dir  f)     = True"
+| "recorded (O_node n)     = False" (* cause socket is temperary not considered *)
+| "recorded (O_shm  h)     = True"
+| "recorded (O_msgq q)     = True"
+| "recorded _              = False"
+
+
+
+
+
+
+lemma d2s_main_execve:
+  "valid (Execve p f fds # s) \<Longrightarrow> s2ss (Execve p f fds # s) \<in> static"
+apply (frule vd_cons, frule vt_grant_os, clarsimp simp:s2ss_execve)
+sorry
+
+lemma d2s_main:
+  "valid s \<Longrightarrow> s2ss s \<propto> static"
+apply (induct s, simp add:s2ss_nil_prop init_ss_in_def)
+apply (rule_tac x = "init_static_state" in bexI, simp, simp add:s_init)
+apply (frule vd_cons, frule vt_grant_os, simp)
+apply (case_tac a) 
+apply (clarsimp simp add:s2ss_execve)
+apply (rule conjI, rule impI)
+
+
+
+sorry
+
+
+lemma many_sq_imp_sms:
+  "\<lbrakk>S_msgq (Create, sec, sms) \<in> ss; ss \<in> static\<rbrakk> \<Longrightarrow> \<forall> sm \<in> (set sms). is_many_smsg sm"
+sorry
+
+
+
+lemma enrichability: 
+  "\<lbrakk>valid s; \<forall> obj \<in> objs. alive s obj \<and> is_created s obj \<and> recorded obj\<rbrakk>
+   \<Longrightarrow> enrichable s objs"
+proof (induct s arbitrary:objs)
+  case Nil
+  hence "objs = {}" 
+    apply (auto simp:is_created_def)
+    apply (erule_tac x = x in ballE)
+    apply (auto simp:init_alive_prop)
+    done
+  thus ?case using Nil unfolding enrichable_def enrich_def reserve_def
+    by (rule_tac x = "[]" in exI, auto)
+next
+  case (Cons e s)
+  hence p1: "\<And> objs. \<forall> obj \<in> objs. alive s obj \<and> is_created s obj \<and> recorded obj \<Longrightarrow> enrichable s objs"
+    and p2: "valid (e # s)" and p3: "\<forall>obj\<in>objs. alive (e # s) obj \<and> is_created (e # s) obj \<and> recorded obj"
+    and os: "os_grant s e" and se: "grant s e" and vd: "valid s"
+    by (auto dest:vt_grant_os vd_cons vt_grant)
+  show ?case sorry (*
+  proof (cases e)
+    case (Execve p f fds)
+    hence p4: "e = Execve p f fds" by simp
+    from p3 have p5: "is_inited s (O_proc p) \<Longrightarrow> (O_proc p) \<notin> objs"
+      by (auto simp:is_created_def is_inited_def p4 elim!:ballE[where x = "O_proc p"])
+    show "enrichable (e # s) objs"
+    proof (case "is_inited s (O_proc p)")
+      apply (simp add:enrichable_def p4)
+
+      
+  
+    apply auto
+    apply (auto simp:enrichable_def)
+apply (induct s)
+
+
+
+done
+*)
+qed
+
+lemma s2d_main:
+  "ss \<in> static \<Longrightarrow> \<exists> s. valid s \<and> s2ss s = ss"
+apply (erule static.induct)
+apply (rule_tac x = "[]" in exI, simp add:s2ss_nil_prop valid.intros)
+
+apply (erule exE|erule conjE)+
+
+apply (simp add:update_ss_def)
+
+sorry
+
+
+end
+
+end
\ No newline at end of file
diff -r 9fc384154e84 -r 051b0ee98852 Final_theorem.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Final_theorem.thy	Thu Oct 24 09:41:33 2013 +0800
@@ -0,0 +1,236 @@
+theory Final_theorem
+imports Main Flask Static Init_prop Valid_prop Tainted_prop Delete_prop Co2sobj_prop S2ss_prop S2ss_prop2 Dynamic_static
+begin
+
+context tainting_s begin
+
+lemma t2ts:
+  "obj \<in> tainted s \<Longrightarrow> co2sobj s obj = Some sobj \<Longrightarrow> tainted_s (s2ss s) sobj"
+apply (frule tainted_in_current, frule tainted_is_valid)
+apply (frule s2ss_included_sobj, simp)
+apply (case_tac sobj, simp_all)
+apply (case_tac [!] obj, simp_all add:co2sobj.simps split:option.splits if_splits)
+apply (drule dir_not_tainted, simp)
+apply (drule msgq_not_tainted, simp)
+apply (drule shm_not_tainted, simp)
+done
+
+lemma delq_imp_delqm:
+  "deleted (O_msgq q) s \<Longrightarrow> deleted (O_msg q m) s"
+apply (induct s, simp)
+by (case_tac a, auto)
+
+lemma tainted_s_subset_prop:
+  "\<lbrakk>tainted_s ss sobj; ss \<subseteq> ss'\<rbrakk> \<Longrightarrow> tainted_s ss' sobj"
+apply (case_tac sobj)
+apply auto
+done
+
+theorem static_complete: 
+  assumes undel: "undeletable obj" and tbl: "taintable obj"
+  shows "taintable_s obj"
+proof-
+  from tbl obtain s where tainted: "obj \<in> tainted s"
+    by (auto simp:taintable_def)
+  hence vs: "valid s" by (simp add:tainted_is_valid)
+  hence static: "s2ss s \<propto> static" using d2s_main by auto
+  from tainted tbl vs obtain sobj where sobj: "co2sobj s obj = Some sobj" 
+    apply (clarsimp simp add:taintable_def)
+    apply (frule tainted_in_current)
+    apply (case_tac obj, simp_all add:co2sobj.simps)
+    apply (frule current_proc_has_sp, simp, auto)
+    done
+  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:co2sobj.simps cp2sproc_def ch2sshm_def cq2smsgq_def cm2smsg_def delq_imp_delqm)
+    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 (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 (simp add:init_ss_in_def)
+    apply (erule bexE)
+    apply (simp add:init_ss_eq_def)
+    apply (rule_tac x = "ss'" in bexI)
+    apply (rule_tac x = "sobj" in exI)
+    by (auto intro:tainted_s_subset_prop)
+qed
+
+lemma cp2sproc_pi:
+  "\<lbrakk>cp2sproc s p = Some (Init p', sec, fds, shms); valid s\<rbrakk> \<Longrightarrow> p = p' \<and> \<not> deleted (O_proc p) s \<and> p \<in> init_procs"
+by (simp add:cp2sproc_def split:option.splits if_splits)
+
+lemma cq2smsgq_qi:
+  "\<lbrakk>cq2smsgq s q = Some (Init q', sec, sms); valid s\<rbrakk> \<Longrightarrow> q = q' \<and> \<not> deleted (O_msgq q) s \<and> q \<in> init_msgqs"
+by (simp add:cq2smsgq_def split:option.splits if_splits)
+
+lemma cm2smsg_mi:
+  "\<lbrakk>cm2smsg s q m = Some (Init m', sec, ttag); q \<in> init_msgqs; valid s\<rbrakk> 
+   \<Longrightarrow> m = m' \<and> \<not> deleted (O_msg q m) s \<and> m \<in> set (init_msgs_of_queue q) \<and> q \<in> init_msgqs"
+by (clarsimp simp add:cm2smsg_def split:if_splits option.splits)
+
+lemma ch2sshm_hi:
+  "\<lbrakk>ch2sshm s h = Some (Init h', sec); valid s\<rbrakk> \<Longrightarrow> h = h' \<and> \<not> deleted (O_shm h) s \<and> h \<in> init_shms"
+by (clarsimp simp:ch2sshm_def split:if_splits option.splits)
+
+lemma root_not_deleted:
+  "\<lbrakk>deleted (O_dir []) s; valid s\<rbrakk> \<Longrightarrow> False"
+apply (induct s, simp)
+apply (frule vd_cons, frule vt_grant_os, case_tac a, auto)
+done
+
+lemma cf2sfile_fi:
+  "\<lbrakk>cf2sfile s f = Some (Init f', sec, psecopt, asecs); valid s\<rbrakk> \<Longrightarrow> f = f' \<and> 
+     (if (is_file s f) then \<not> deleted (O_file f) s \<and> is_init_file f 
+      else \<not> deleted (O_dir f) s \<and> is_init_dir f)"
+apply (case_tac f)
+by (auto simp:sroot_def cf2sfile_def root_is_init_dir dest!:root_is_dir' root_not_deleted
+        split:if_splits option.splits) 
+
+lemma init_deled_imp_deled_s: 
+  "\<lbrakk>deleted obj s; init_alive obj; sobj \<in> (s2ss s); valid s\<rbrakk> \<Longrightarrow> \<not> init_obj_related sobj obj"
+apply (rule notI)
+apply (clarsimp simp:s2ss_def)
+apply (case_tac obj, case_tac [!] obja, case_tac sobj)
+apply (auto split:option.splits if_splits dest!:cp2sproc_pi cq2smsgq_qi ch2sshm_hi cm2smsg_mi cf2sfile_fi simp:co2sobj.simps)
+apply (auto simp:cf2sfiles_def same_inode_files_def has_same_inode_prop1' is_file_def is_dir_def co2sobj.simps
+           split:option.splits t_inode_tag.splits dest!:cf2sfile_fi)
+done
+
+lemma deleted_imp_deletable_s:
+  "\<lbrakk>deleted obj s; init_alive obj; valid s\<rbrakk> \<Longrightarrow> deletable_s obj"
+apply (simp add:deletable_s_def)
+apply (frule d2s_main)
+apply (simp add:init_ss_in_def)
+apply (erule bexE)
+apply (rule_tac x = ss' in bexI)
+apply (auto simp add: init_ss_eq_def dest!:init_deled_imp_deled_s)
+apply (case_tac obj, case_tac [!] sobj)
+apply auto
+apply (erule set_mp)
+apply (simp)
+apply auto
+apply (rule_tac x = "(Init list, (aa, ab, b), ac, ba)" in bexI)
+apply auto
+done
+
+lemma init_related_imp_init_sobj:
+  "init_obj_related sobj obj \<Longrightarrow> is_init_sobj sobj"
+apply (case_tac sobj, case_tac [!] obj, auto)
+apply (rule_tac x = "(Init list, (aa, ab, b), ac, ba)" in bexI, auto)
+done
+
+theorem undeletable_s_complete:
+  assumes undel_s: "undeletable_s obj"
+  shows "undeletable obj"
+proof-
+  from undel_s have init_alive: "init_alive obj"
+    and alive_s: "\<forall> ss \<in> static. \<exists> sobj \<in> ss. init_obj_related sobj obj" 
+    using undeletable_s_def by auto
+  have "\<not> (\<exists> s. valid s \<and> deleted obj s)" 
+  proof
+    assume "\<exists> s. valid s \<and> deleted obj s"
+    then obtain s where vs: "valid s" and del: "deleted obj s" by auto
+    from vs have vss: "s2ss s \<propto> static" by (rule d2s_main) 
+    with alive_s obtain sobj where in_ss: "sobj \<in> (s2ss s)" 
+      and related: "init_obj_related sobj obj" 
+      apply (simp add:init_ss_in_def init_ss_eq_def)
+      apply (erule bexE, erule_tac x= ss' in ballE)
+      apply (auto dest:init_related_imp_init_sobj)
+      done
+    from init_alive del vs have "deletable_s obj" 
+      by (auto elim:deleted_imp_deletable_s)
+    with alive_s
+    show False by (auto simp:deletable_s_def)
+  qed
+  with init_alive show ?thesis 
+    by (simp add:undeletable_def)
+qed
+
+theorem final_offer:
+  "\<lbrakk>undeletable_s obj; \<not> taintable_s obj; init_alive obj\<rbrakk> \<Longrightarrow> \<not> taintable obj"
+apply (erule swap)
+by (simp add:static_complete undeletable_s_complete)
+
+(************** static \<rightarrow> dynamic ***************)
+
+
+lemma set_eq_D:
+  "\<lbrakk>x \<in> S; {x. P x} = S\<rbrakk> \<Longrightarrow> P x"
+by auto
+
+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 simp:cqm2sms.simps split:option.splits)
+done
+
+lemma sq_sm_prop:
+  "\<lbrakk>sm \<in> set sms; cq2smsgq s q = Some (qi, qsec, sms); valid s\<rbrakk>
+   \<Longrightarrow> \<exists> m. cm2smsg s q m = Some sm"
+by (auto simp:cq2smsgq_def split: option.splits intro:cqm2sms_prop1)
+
+declare co2sobj.simps [simp add]
+
+lemma tainted_s_imp_tainted:
+  "\<lbrakk>tainted_s ss sobj; ss \<in> static\<rbrakk> \<Longrightarrow> \<exists> s obj. valid s \<and> co2sobj s obj = Some sobj \<and> obj \<in> tainted s"
+apply (drule s2d_main)
+apply (erule exE, erule conjE, simp add:s2ss_def)
+apply (rule_tac x = s in exI, simp)
+apply (case_tac sobj, simp_all)
+apply (erule conjE, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+) 
+apply (rule_tac x = obj in exI, simp)
+apply (case_tac obj, (simp split:option.splits if_splits)+)
+
+apply (erule conjE, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+) 
+apply (rule_tac x = obj in exI, simp)
+apply (case_tac obj, (simp split:option.splits if_splits)+)
+done
+
+lemma has_same_inode_prop3:
+  "has_same_inode s f f' \<Longrightarrow> has_same_inode s f' f"
+by (auto simp:has_same_inode_def)
+
+theorem static_sound:
+  assumes tbl_s: "taintable_s obj"
+  shows "taintable obj"
+proof-
+  from tbl_s obtain ss sobj where static: "ss \<in> static"
+    and sobj: "tainted_s ss sobj" and related: "init_obj_related sobj obj"
+    and init_alive: "init_alive obj" by (auto simp:taintable_s_def)
+  from static sobj tainted_s_imp_tainted 
+  obtain s obj' where co2sobj: "co2sobj s obj' = Some sobj"
+    and tainted': "obj' \<in> tainted s" and vs: "valid s" by blast
+  
+  from co2sobj related vs
+  have eq:"obj = obj' \<or> (\<exists> f f'. obj = O_file f \<and> obj' = O_file f' \<and> has_same_inode s f f')"
+    apply (case_tac obj', case_tac [!] obj)
+    apply (auto split:option.splits if_splits dest!:cp2sproc_pi cq2smsgq_qi ch2sshm_hi cm2smsg_mi cf2sfile_fi)
+    apply (auto simp:cf2sfiles_def same_inode_files_def has_same_inode_def is_file_def is_dir_def
+               split:option.splits t_inode_tag.splits dest!:cf2sfile_fi)
+    done
+  with tainted' vs have tainted: "obj \<in> tainted s"
+    by (auto dest:has_same_inode_prop3 intro:has_same_inode_tainted)
+  from sobj related init_alive have "appropriate obj"
+    by (case_tac obj, case_tac [!] sobj, auto)
+  with vs init_alive tainted
+  show ?thesis by (auto simp:taintable_def)
+qed
+
+end
+
+end
\ No newline at end of file