--- a/Flask.thy	Thu Jun 06 14:50:52 2013 +0800
+++ b/Flask.thy	Sat Jun 08 09:59:33 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) \<or> (\<exists> h \<in> current_shms \<tau>. \<exists> toflag. 
+  "info_flow_shm \<tau> from to \<equiv> (from = to \<and> from \<in> current_procs s) \<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)))" 
 
 fun current_msgqs :: "t_state \<Rightarrow> t_msg set"
@@ -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''; p'' \<in> current_procs s\<rbrakk>
+| t_ptrace: "\<lbrakk>O_proc p \<in> tainted s; valid (Ptrace p p' # s); info_flow_shm s p' p''\<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''; p'' \<in> current_procs s\<rbrakk>
+| t_ptrace':"\<lbrakk>O_proc p' \<in> tainted s; valid (Ptrace p p' # s); info_flow_shm s p p''\<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'; p' \<in> current_procs s\<rbrakk> 
+              file_of_proc_fd s p fd = Some f; info_flow_shm s p p'\<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'; p' \<in> current_procs s\<rbrakk>
+| t_recvmsg:"\<lbrakk>O_msg q m \<in> tainted s; valid (RecvMsg p q m # s); info_flow_shm s p p'\<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)"

--- a/Tainted_prop.thy	Thu Jun 06 14:50:52 2013 +0800
+++ b/Tainted_prop.thy	Sat Jun 08 09:59:33 2013 +0800
@@ -4,6 +4,93 @@
 
 context tainting begin
 
+fun Tainted :: "t_state \<Rightarrow> t_object set"
+where
+  "Tainted [] = seeds"
+| "Tainted (Clone p p' fds shms # s) = 
+     (if (O_proc p) \<in> Tainted s then Tainted s \<union> {O_proc p'} else Tainted s)"
+| "Tainted (Execve p f fds # s) = 
+     (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 
+      then Tainted s \<union> {O_proc p'' | p''. info_flow_shm s p' p''}
+      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}"
+| "Tainted (Open p f flags fd opt # s) = 
+     (case opt of
+        Some inum \<Rightarrow> (if (O_proc p) \<in> Tainted s
+                      then Tainted s \<union> {O_file f}
+                      else Tainted s)
+      | _         \<Rightarrow> Tainted s)" 
+| "Tainted (ReadFile p fd # s) = 
+     (case (file_of_proc_fd s p fd) of
+        Some f \<Rightarrow> if (O_file f) \<in> Tainted s
+                  then Tainted s \<union> {O_proc p' | p'. info_flow_shm s p p'}
+                  else Tainted s
+      | None   \<Rightarrow> Tainted s)"
+| "Tainted (WriteFile p fd # s) = 
+     (case (file_of_proc_fd s p fd) of 
+        Some f \<Rightarrow> if (O_proc p) \<in> Tainted s
+                  then Tainted s \<union> {O_file f' | f'. has_same_inode s f f'}
+                  else Tainted s
+      | None   \<Rightarrow> Tainted s)"
+| "Tainted (CloseFd p fd # s) = 
+     (case (file_of_proc_fd s p fd) of
+        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 (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) = 
+     (if (len > 0 \<and> O_proc p \<in> Tainted s)
+      then Tainted s \<union> {O_file f' | f'. has_same_inode s f f'}
+      else Tainted s)"
+| "Tainted (SendMsg p q m # s) = 
+     (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}
+      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"
+
+lemma valid_Tainted_obj:
+  "\<lbrakk>obj \<in> Tainted s; valid s\<rbrakk> \<Longrightarrow> (\<forall> f. obj \<noteq> O_dir f) \<and> (\<forall> q. obj \<noteq> O_msgq q) \<and> (\<forall> h. obj \<noteq> O_shm h) \<and> (\<forall> p fd. obj \<noteq> O_fd p fd) \<and> (\<forall> s. obj \<noteq> O_tcp_sock s) \<and> (\<forall> s. obj \<noteq> O_udp_sock s)"
+apply (induct s, simp, drule seeds_in_init, case_tac obj, simp+)
+apply (frule vd_cons, frule vt_grant_os, case_tac a)
+apply (auto split:if_splits option.splits)
+done
+
+lemma Tainted_in_current:
+  "\<lbrakk>obj \<in> Tainted s; valid s\<rbrakk> \<Longrightarrow> alive s obj"
+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 
+
+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)
+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)
+pr 25
+
+lemma tainted_imp_Tainted:
+  "obj \<in> tainted s \<Longrightarrow> obj \<in> Tainted s"
+
+
+
+
+
+
 lemma tainted_in_current:
   "obj \<in> tainted s \<Longrightarrow> alive s obj"
 apply (erule tainted.induct, auto dest:vt_grant_os vd_cons simp:is_file_simps)
@@ -27,7 +114,7 @@
 done
 
 lemma valid_tainted_obj:
-  "obj \<in> tainted s \<Longrightarrow> (\<forall> f. obj \<noteq> O_dir f) \<and> (\<forall> q. obj \<noteq> O_msgq q) \<and> (\<forall> h. obj \<noteq> O_shm h)"
+  "obj \<in> tainted s \<Longrightarrow> (\<forall> f. obj \<noteq> O_dir f) \<and> (\<forall> q. obj \<noteq> O_msgq q) \<and> (\<forall> h. obj \<noteq> O_shm h) \<and> (\<forall> p fd. obj \<noteq> O_fd p fd) \<and> (\<forall> s. obj \<noteq> O_tcp_sock s) \<and> (\<forall> s. obj \<noteq> O_udp_sock s)"
 apply (erule tainted.induct)
 apply (drule seeds_in_init)
 by auto