--- a/Flask.thy	Tue Jun 04 15:37:49 2013 +0800
+++ b/Flask.thy	Tue Jun 04 15:51:02 2013 +0800
@@ -476,7 +476,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) \<or> (\<exists> h \<in> current_shms \<tau>. \<exists> toflag. 
-    (((from, SHM_RDWR) \<in> procs_of_shm \<tau> h) \<and> ((to, toflag) \<in> procs_of_shm \<tau> h)))"
+    (((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"
 where
@@ -1428,14 +1428,14 @@
              \<Longrightarrow> O_proc p' \<in> tainted (Clone p p' fds shms # s)"
 | t_execve: "\<lbrakk>O_file f \<in> tainted s; valid (Execve p f fds # s)\<rbrakk> 
              \<Longrightarrow> O_proc p \<in> tainted (Execve p f fds # s)"
-| t_ptrace: "\<lbrakk>O_proc p \<in> tainted s; valid (Ptrace p p' # s); info_flow_shm s p' p''\<rbrakk>
+| t_ptrace: "\<lbrakk>O_proc p \<in> tainted s; valid (Ptrace p p' # s); info_flow_shm s p' p''; p'' \<in> current_procs s\<rbrakk>
              \<Longrightarrow> O_proc p'' \<in> tainted (Ptrace p p' # s)"
-| t_ptrace':"\<lbrakk>O_proc p' \<in> tainted s; valid (Ptrace p p' # s); info_flow_shm s p p''\<rbrakk>
+| t_ptrace':"\<lbrakk>O_proc p' \<in> tainted s; valid (Ptrace p p' # s); info_flow_shm s p p''; p'' \<in> current_procs s\<rbrakk>
              \<Longrightarrow> O_proc p'' \<in> tainted (Ptrace p p' # s)"
 | t_cfile:  "\<lbrakk>O_proc p \<in> tainted s; valid (Open p f flags fd (Some inum) # s)\<rbrakk>
              \<Longrightarrow> O_file f \<in> tainted (Open p f flags fd (Some inum) # s)"
 | t_read:   "\<lbrakk>O_file f \<in> tainted s; valid (ReadFile p fd # s); 
-              file_of_proc_fd s p fd = Some f; info_flow_shm s p p'\<rbrakk> 
+              file_of_proc_fd s p fd = Some f; info_flow_shm s p p'; p' \<in> current_procs s\<rbrakk> 
              \<Longrightarrow> O_proc p' \<in> tainted (ReadFile p fd # s)"
 | t_write:  "\<lbrakk>O_proc p \<in> tainted s; valid (WriteFile p fd # s);
               file_of_proc_fd s p fd = Some f; has_same_inode s f f'\<rbrakk> 
@@ -1456,7 +1456,7 @@
 *)
 | t_sendmsg:"\<lbrakk>O_proc p \<in> tainted s; valid (SendMsg p q m # s)\<rbrakk>
              \<Longrightarrow> O_msg q m \<in> tainted (SendMsg p q m # s)"
-| t_recvmsg:"\<lbrakk>O_msg q m \<in> tainted s; valid (RecvMsg p q m # s); info_flow_shm s p p'\<rbrakk>
+| t_recvmsg:"\<lbrakk>O_msg q m \<in> tainted s; valid (RecvMsg p q m # s); info_flow_shm s p p'; p' \<in> current_procs s\<rbrakk>
              \<Longrightarrow> O_proc p' \<in> tainted (RecvMsg p q m # s)"
 | t_remain: "\<lbrakk>obj \<in> tainted s; valid (e # s); alive (e # s) obj\<rbrakk> 
              \<Longrightarrow> obj \<in> tainted (e # s)"