--- a/Current_prop.thy	Sat Jun 08 09:59:33 2013 +0800
+++ b/Current_prop.thy	Sun Jun 09 14:28:58 2013 +0800
@@ -47,6 +47,10 @@
   "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<not> (\<not> deleted (O_proc p) s \<and> p \<in> init_procs)"
 using not_deleted_init_proc by auto
 
+lemma info_shm_flow_in_procs:
+  "\<lbrakk>info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s \<and> p' \<in> current_procs s"
+by (auto simp:info_flow_shm_def intro:procs_of_shm_prop2)
+
 lemma has_same_inode_in_current:
   "\<lbrakk>has_same_inode s f f'; valid s\<rbrakk> \<Longrightarrow> f \<in> current_files s \<and> f' \<in> current_files s"
 by (auto simp add:has_same_inode_def current_files_def)

--- a/Flask.thy	Sat Jun 08 09:59:33 2013 +0800
+++ b/Flask.thy	Sun Jun 09 14:28:58 2013 +0800
@@ -475,7 +475,7 @@
 
 definition info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"
 where
-  "info_flow_shm \<tau> from to \<equiv> (from = to \<and> from \<in> current_procs s) \<or> (\<exists> h \<in> current_shms \<tau>. \<exists> toflag. 
+  "info_flow_shm \<tau> from to \<equiv> (from = to \<and> from \<in> current_procs \<tau>) \<or> (\<exists> h toflag. 
     (((from, SHM_RDWR) \<in> procs_of_shm \<tau> h) \<and> ((to, toflag) \<in> procs_of_shm \<tau> h)))" 
 
 fun current_msgqs :: "t_state \<Rightarrow> t_msg set"
@@ -1417,7 +1417,9 @@
 
 fixes seeds :: "t_object set"
 assumes 
-  seeds_in_init: "\<And> obj. obj \<in> seeds \<Longrightarrow> tobj_in_init obj"
+      seeds_in_init: "\<And> obj. obj \<in> seeds \<Longrightarrow> tobj_in_init obj"
+  and same_inode_in_seeds: "\<And> f f'. \<lbrakk>O_file f \<in> seeds; has_same_inode [] f f'\<rbrakk> \<Longrightarrow> O_file f' \<in> seeds"
+  and flow_shm_in_seeds: "\<And> p p'. \<lbrakk>O_proc p \<in> seeds; info_flow_shm [] p p'\<rbrakk> \<Longrightarrow> O_proc p' \<in> seeds"
 
 begin
 

--- a/Tainted_prop.thy	Sat Jun 08 09:59:33 2013 +0800
+++ b/Tainted_prop.thy	Sun Jun 09 14:28:58 2013 +0800
@@ -42,7 +42,8 @@
         Some f \<Rightarrow> ( if ((proc_fd_of_file s f = {(p,fd)}) \<and> (f \<in> files_hung_by_del s))
                     then Tainted s - {O_file f} else Tainted s )
       | _      \<Rightarrow> Tainted s)"
-| "Tainted (UnLink p f # s) = Tainted s - {O_file f}"
+| "Tainted (UnLink p f # s) = 
+     (if (proc_fd_of_file s f = {}) then Tainted s - {O_file f} else Tainted s)"
 | "Tainted (LinkHard p f f' # s) = 
      (if (O_file f \<in> Tainted s) then Tainted s \<union> {O_file f'} else Tainted s)"
 | "Tainted (Truncate p f len # s) = 
@@ -53,7 +54,7 @@
      (if (O_proc p \<in> Tainted s) then Tainted s \<union> {O_msg q m} else Tainted s)"
 | "Tainted (RecvMsg p q m # s) = 
      (if (O_msg q m \<in> Tainted s) 
-      then Tainted s \<union> {O_proc p' | p'. info_flow_shm s p p'} - {O_msg q m}
+      then (Tainted s \<union> {O_proc p' | p'. info_flow_shm s p p'}) - {O_msg q m}
       else Tainted s)"
 | "Tainted (RemoveMsgq p q # s) = Tainted s - {O_msg q m| m. O_msg q m \<in> Tainted s}"
 | "Tainted (e # s) = Tainted s"
@@ -70,17 +71,54 @@
 apply (induct s, simp)
 apply (drule seeds_in_init, case_tac obj, simp_all add:is_file_nil)
 apply (frule vd_cons, frule valid_Tainted_obj, simp, frule vt_grant_os, case_tac a)
-apply (auto simp:alive_simps split:if_splits option.splits t_object.splits)
-apply (auto intro:has_same_inode_prop2 has_same_inode_prop1)
-apply 
+apply (auto simp:alive_simps split:if_splits option.splits t_object.splits
+           intro:has_same_inode_prop2 has_same_inode_prop1 dest:info_shm_flow_in_procs)
+done
+
+
+lemma has_inode_Tainted_aux:
+  "\<lbrakk>O_file f \<in> tainted s; has_same_inode s f f'\<rbrakk> \<Longrightarrow> O_file f' \<in> tainted s"
+apply (erule tainted.induct)
+apply (auto intro:tainted.intros simp:has_same_inode_def)
+(*?? need simpset for tainted *)
+sorry
+
+lemma info_flow_shm_Tainted:
+  "\<lbrakk>O_proc p \<in> Tainted s; info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> O_proc p' \<in> Tainted s"
+proof (induct s)
+  case Nil
+  thus ?case
+    apply simp
+apply (induct s)
+apply simp defer
+apply (frule vd_cons, frule vt_grant_os, case_tac a)
+apply (auto simp:info_flow_shm_def elim!:disjE)
+sorry
+
+lemma tainted_imp_Tainted:
+  "obj \<in> tainted s \<Longrightarrow> obj \<in> Tainted s"
+apply (induct rule:tainted.induct)
+apply (auto intro:info_flow_shm_Tainted dest:vd_cons)
+apply (case_tac e, auto split:option.splits if_splits simp:alive_simps)
+done
 
 lemma Tainted_imp_tainted:
   "\<lbrakk>obj \<in> Tainted s; valid s\<rbrakk> \<Longrightarrow> obj \<in> tainted s"
-apply (induct s arbitrary:obj, rule t_init, simp)
-apply (frule vd_cons, frule vt_grant_os)
+proof (induct s arbitrary:obj)
+  case Nil
+  thus ?case by (auto intro:t_init)
+next
+  case (Cons e s)
+  hence p1: "\<And> obj. obj \<in> Tainted s \<Longrightarrow> obj \<in> tainted s"
+    and p2: "obj \<in> Tainted (e # s)" and p3: "valid (e # s)" 
+    and p4: "valid s" and p5: "os_grant s e"
+    by (auto dest:vd_cons intro:vd_cons vt_grant_os)
+  from p1 have p6: ""
+apply (frule vd_cons, frule vt_grant_os, frule valid_Tainted_obj, simp)
 apply (case_tac a)
 apply (auto intro!:t_init t_clone t_execve t_cfile t_read t_write t_link t_trunc t_sendmsg t_recvmsg
-             split:if_splits option.splits)
+            intro:t_remain
+             split:if_splits option.splits dest:Tainted_in_current)
 pr 25
 
 lemma tainted_imp_Tainted: