--- a/Flask.thy	Wed Oct 16 14:43:28 2013 +0800
+++ b/Flask.thy	Mon Oct 21 16:18:19 2013 +0800
@@ -1483,9 +1483,28 @@
 | t_remain: "\<lbrakk>obj \<in> tainted s; valid (e # s); alive (e # s) obj\<rbrakk> 
              \<Longrightarrow> obj \<in> tainted (e # s)"
 
+(* reasonable tainted object, fd and sock and msgq and msg is excluded 
+ * this is different from tainted, which already excluded some of them,
+ * tainted not excluded msg, which does not have the meaning of "tainteable", but 
+ * but acting as a media to "pass" the virus. We normally will not say that 
+ * a message is tableable or not.
+ *)
+fun appropriate :: "t_object \<Rightarrow> bool"
+where
+  "appropriate (O_proc p)     = (p \<in> init_procs)"
+| "appropriate (O_file f)     = (is_init_file f)"
+| "appropriate (O_dir  f)     = False"
+| "appropriate (O_fd p fd)    = False"
+| "appropriate (O_node n)     = False" (* cause socket is temperary not considered *)
+| "appropriate (O_tcp_sock k) = False"
+| "appropriate (O_udp_sock k) = False"
+| "appropriate (O_shm  h)     = False"
+| "appropriate (O_msgq q)     = False"
+| "appropriate (O_msg q m)    = False"
+
 definition taintable:: "t_object \<Rightarrow> bool"
 where
-  "taintable obj \<equiv> init_alive obj \<and> (\<exists> s. obj \<in> tainted s)"
+  "taintable obj \<equiv> init_alive obj \<and> appropriate obj \<and> (\<exists> s. obj \<in> tainted s)"
 
 definition undeletable :: "t_object \<Rightarrow> bool"
 where