# HG changeset patch
# User chunhan
# Date 1383092320 -28800
# Node ID 6f9a588bcfc4758e86c5763029467a25e09db6ee
# Parent  0753309adfc7e8bbf57b411a39c59e65f8bf116c
update

diff -r 0753309adfc7 -r 6f9a588bcfc4 Co2sobj_prop.thy
--- a/Co2sobj_prop.thy	Thu Oct 24 09:42:35 2013 +0800
+++ b/Co2sobj_prop.thy	Wed Oct 30 08:18:40 2013 +0800
@@ -2105,11 +2105,6 @@
 apply (drule cf2sfile_mkdir1, simp+)
 done
 
-lemma same_inodes_Tainted:
-  "\<lbrakk>f \<in> same_inode_files s f'; valid s\<rbrakk> \<Longrightarrow> (O_file f \<in> Tainted s) = (O_file f' \<in> Tainted s)"
-apply (frule same_inode_files_prop8, frule same_inode_files_prop7)
-apply (auto intro:has_same_inode_Tainted)
-done
 
 lemma co2sobj_linkhard:
   "\<lbrakk>valid (LinkHard p oldf f # s); alive (LinkHard p oldf f # s) obj\<rbrakk> 
@@ -2151,9 +2146,7 @@
              simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted
                   same_inode_files_prop6
              dest:is_file_in_current is_dir_in_current)
-
-(* should delete has_same_inode !?!?*)
-by (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits option.splits)
+done
 
 lemma co2sobj_kill:
   "\<lbrakk>valid (Kill p p' # s); alive (Kill p p' # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Kill p p' # s) obj = co2sobj s obj"
diff -r 0753309adfc7 -r 6f9a588bcfc4 Current_prop.thy
--- a/Current_prop.thy	Thu Oct 24 09:42:35 2013 +0800
+++ b/Current_prop.thy	Wed Oct 30 08:18:40 2013 +0800
@@ -67,15 +67,18 @@
 
 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)
+by (auto simp add:has_same_inode_def current_files_def same_inode_files_def 
+  is_file_def split:if_splits option.splits)
+
 
 lemma has_same_inode_prop1:
   "\<lbrakk>has_same_inode s f f'; is_file s f; valid s\<rbrakk> \<Longrightarrow> is_file s f'"
-by (auto simp:has_same_inode_def is_file_def)
+by (auto simp:has_same_inode_def same_inode_files_def is_file_def)
 
 lemma has_same_inode_prop1':
   "\<lbrakk>has_same_inode s f f'; is_file s f'; valid s\<rbrakk> \<Longrightarrow> is_file s f"
-by (auto simp:has_same_inode_def is_file_def)
+by (auto simp:has_same_inode_def is_file_def same_inode_files_def 
+ split:if_splits option.splits)
 
 lemma has_same_inode_prop2:
   "\<lbrakk>has_same_inode s f f'; file_of_proc_fd s p fd = Some f; valid s\<rbrakk> \<Longrightarrow> is_file s f'"
diff -r 0753309adfc7 -r 6f9a588bcfc4 Dynamic_static.thy
--- a/Dynamic_static.thy	Thu Oct 24 09:42:35 2013 +0800
+++ b/Dynamic_static.thy	Wed Oct 30 08:18:40 2013 +0800
@@ -1,32 +1,10 @@
 theory Dynamic_static
 imports Main Flask Static Init_prop Valid_prop Tainted_prop Delete_prop Co2sobj_prop S2ss_prop S2ss_prop2
+ Temp
 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
-
 
 
 
@@ -55,17 +33,6 @@
   "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"
-
 
 
 
@@ -95,6 +62,16 @@
 sorry
 
 
+(* 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>
diff -r 0753309adfc7 -r 6f9a588bcfc4 Flask.thy
--- a/Flask.thy	Thu Oct 24 09:42:35 2013 +0800
+++ b/Flask.thy	Wed Oct 30 08:18:40 2013 +0800
@@ -311,38 +311,6 @@
 where
   "current_files \<tau> = {f. \<exists> i. inum_of_file \<tau> f = Some i}" 
 
-definition has_same_inode :: "t_state \<Rightarrow> t_file \<Rightarrow> t_file \<Rightarrow> bool"
-where 
-  "has_same_inode \<tau> fa fb = 
-     (\<exists>i. inum_of_file \<tau> fa = Some i \<and> inum_of_file \<tau> fb = Some i)"
-
-fun inum_of_socket :: "t_state \<Rightarrow> (t_socket \<rightharpoonup> t_inode_num)"
-where
-  "inum_of_socket [] = init_inum_of_socket"
-| "inum_of_socket (CloseFd p fd # \<tau>) = 
-     (inum_of_socket \<tau>) ((p, fd):= None)"
-| "inum_of_socket (CreateSock p af st fd ino # \<tau>) = 
-     (inum_of_socket \<tau>) ((p, fd) := Some ino)"
-| "inum_of_socket (Accept p fd addr lport' fd' ino # \<tau>) = 
-     (inum_of_socket \<tau>) ((p, fd') := Some ino)"
-| "inum_of_socket (Clone p p' fds shms # \<tau>) = 
-     (\<lambda> (p'', fd). if (p'' = p' \<and> fd \<in> fds) then inum_of_socket \<tau> (p, fd) 
-                   else if (p'' = p') then None
-                   else inum_of_socket \<tau> (p'',fd))" 
-| "inum_of_socket (Execve p f fds # \<tau>) = 
-     (\<lambda> (p', fd). if (p' = p \<and> fd \<in> fds) then inum_of_socket \<tau> (p, fd)
-                  else if (p' = p) then None
-                  else inum_of_socket \<tau> (p', fd))"
-| "inum_of_socket (Kill p\<^isub>1 p\<^isub>2 # \<tau>) = 
-     (\<lambda> (p, fd). if (p = p\<^isub>2) then None else inum_of_socket \<tau> (p, fd) )"
-| "inum_of_socket (Exit p # \<tau>) = 
-     (\<lambda> (p', fd). if (p' = p) then None else inum_of_socket \<tau> (p', fd))"
-| "inum_of_socket (_ # \<tau>) = inum_of_socket \<tau>" 
-
-definition current_sockets :: "t_state \<Rightarrow> t_socket set"
-where
-  "current_sockets \<tau> = {s. \<exists> i. inum_of_socket \<tau> s = Some i}"
-
 (* experimentary: for the delete obj's (file or socket) inode num, it is unnecessary for itag_of_inum to be NONE, cause this is the situation blocked by inum_of_file / inum_of_socket !!! *)  
 (* delete a file, just recycle its inode num, but not destroy its inode \<dots>, so it is irrelative to these events, like closeFd, Rmdir, UnLink \<dots>*)
 fun itag_of_inum :: "t_state \<Rightarrow> (t_inode_num \<rightharpoonup> t_inode_tag)"
@@ -378,6 +346,41 @@
 where
   "dir_is_empty \<tau> f \<equiv> is_dir \<tau> f \<and> \<not> (\<exists> f'. f' \<in> current_files \<tau> \<and> f \<prec> f')"
 
+definition same_inode_files :: "t_state \<Rightarrow> t_file \<Rightarrow> t_file set"
+where
+  "same_inode_files s f \<equiv> if is_file s f then {f'. inum_of_file s f = inum_of_file s f'} else {}"
+
+definition has_same_inode :: "t_state \<Rightarrow> t_file \<Rightarrow> t_file \<Rightarrow> bool"
+where 
+  "has_same_inode s fa fb \<equiv> fb \<in> same_inode_files s fa"
+
+fun inum_of_socket :: "t_state \<Rightarrow> (t_socket \<rightharpoonup> t_inode_num)"
+where
+  "inum_of_socket [] = init_inum_of_socket"
+| "inum_of_socket (CloseFd p fd # \<tau>) = 
+     (inum_of_socket \<tau>) ((p, fd):= None)"
+| "inum_of_socket (CreateSock p af st fd ino # \<tau>) = 
+     (inum_of_socket \<tau>) ((p, fd) := Some ino)"
+| "inum_of_socket (Accept p fd addr lport' fd' ino # \<tau>) = 
+     (inum_of_socket \<tau>) ((p, fd') := Some ino)"
+| "inum_of_socket (Clone p p' fds shms # \<tau>) = 
+     (\<lambda> (p'', fd). if (p'' = p' \<and> fd \<in> fds) then inum_of_socket \<tau> (p, fd) 
+                   else if (p'' = p') then None
+                   else inum_of_socket \<tau> (p'',fd))" 
+| "inum_of_socket (Execve p f fds # \<tau>) = 
+     (\<lambda> (p', fd). if (p' = p \<and> fd \<in> fds) then inum_of_socket \<tau> (p, fd)
+                  else if (p' = p) then None
+                  else inum_of_socket \<tau> (p', fd))"
+| "inum_of_socket (Kill p\<^isub>1 p\<^isub>2 # \<tau>) = 
+     (\<lambda> (p, fd). if (p = p\<^isub>2) then None else inum_of_socket \<tau> (p, fd) )"
+| "inum_of_socket (Exit p # \<tau>) = 
+     (\<lambda> (p', fd). if (p' = p) then None else inum_of_socket \<tau> (p', fd))"
+| "inum_of_socket (_ # \<tau>) = inum_of_socket \<tau>" 
+
+definition current_sockets :: "t_state \<Rightarrow> t_socket set"
+where
+  "current_sockets \<tau> = {s. \<exists> i. inum_of_socket \<tau> s = Some i}"
+
 definition is_tcp_sock :: "t_state \<Rightarrow> t_socket \<Rightarrow> bool"
 where
   "is_tcp_sock \<tau> s \<equiv> (case (inum_of_socket \<tau> s) of
@@ -522,10 +525,6 @@
 where
   "current_inode_nums \<tau> = current_file_inums \<tau> \<union> current_sock_inums \<tau>"
 
-definition same_inode_files :: "t_state \<Rightarrow> t_file \<Rightarrow> t_file set"
-where
-  "same_inode_files s f \<equiv> if is_file s f then {f'. inum_of_file s f = inum_of_file s f'} else {}"
-
 fun flags_of_proc_fd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd \<Rightarrow> t_open_flags option"
 where
   "flags_of_proc_fd [] p fd = init_oflags_of_proc_fd p fd" 
diff -r 0753309adfc7 -r 6f9a588bcfc4 ROOT
--- a/ROOT	Thu Oct 24 09:42:35 2013 +0800
+++ b/ROOT	Wed Oct 30 08:18:40 2013 +0800
@@ -34,4 +34,5 @@
 session "s2ss" = "co2sobj" +
   options [document = false]
   theories
-    S2ss_prop
\ No newline at end of file
+    S2ss_prop
+    S2ss_prop2
\ No newline at end of file
diff -r 0753309adfc7 -r 6f9a588bcfc4 S2ss_prop.thy
--- a/S2ss_prop.thy	Thu Oct 24 09:42:35 2013 +0800
+++ b/S2ss_prop.thy	Wed Oct 30 08:18:40 2013 +0800
@@ -1875,9 +1875,9 @@
 apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
 done
 
-lemma has_same_inode_prop3:
-  "is_file s f \<Longrightarrow> has_same_inode s f f"
-by (auto simp:is_file_def has_same_inode_def split:option.splits)
+lemma same_inode_files_prop12:
+  "is_file s f \<Longrightarrow> f \<in> same_inode_files s f "
+by (auto simp:is_file_def  same_inode_files_def split:option.splits)
 
 definition update_s2ss_sfile_tainted:: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_file \<Rightarrow> bool \<Rightarrow> t_static_state"
 where
@@ -1900,12 +1900,11 @@
 apply (simp add:s2ss_def)
 apply (tactic {*my_seteq_tac 1*})
 apply (case_tac "obj = O_file f")
-apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted has_same_inode_prop3 cf2sfiles_other)
+apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted same_inode_files_prop12 cf2sfiles_other)
 apply (erule_tac obj = obj in co2sobj_some_caseD)
 apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_truncate alive_simps)
 apply (case_tac "fa \<in> same_inode_files s f")
 apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted cf2sfiles_prop cf2sfiles_other)
-apply (simp add:same_inode_files_prop7)
 apply (rule disjI2, simp, rule_tac x = obj in exI)
 apply (simp add:co2sobj_truncate is_file_simps)
 apply (rule disjI2, simp, rule_tac x = obj in exI)
@@ -1916,7 +1915,7 @@
 apply (simp add:co2sobj_truncate)
 apply (tactic {*my_setiff_tac 1*})
 apply (rule_tac x = "O_file f" in exI)
-apply (simp add:co2sobj.simps is_file_simps tainted_eq_Tainted cf2sfiles_other has_same_inode_prop3)
+apply (simp add:co2sobj.simps is_file_simps tainted_eq_Tainted cf2sfiles_other same_inode_files_prop12)
 apply (tactic {*my_setiff_tac 1*})
 apply (erule_tac obj = obj in co2sobj_some_caseD)
 apply (rule_tac x = obj in exI, simp add:co2sobj_truncate)
@@ -1933,13 +1932,12 @@
 apply (simp add:s2ss_def)
 apply (tactic {*my_seteq_tac 1*})
 apply (case_tac "obj = O_file f")
-apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted has_same_inode_prop3 cf2sfiles_other)
+apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted same_inode_files_prop12 cf2sfiles_other)
 apply (erule_tac obj = obj in co2sobj_some_caseD)
 apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI, simp add:co2sobj_truncate alive_simps)
 apply (rule notI, simp add:co2sobj.simps split:option.splits)
 apply (case_tac "fa \<in> same_inode_files s f")
 apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted cf2sfiles_prop cf2sfiles_other)
-apply (simp add:same_inode_files_prop7)
 apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI)
 apply (simp add:co2sobj_truncate is_file_simps)
 apply (rule notI, simp add:co2sobj_truncate is_file_simps)
@@ -1956,7 +1954,7 @@
 apply (rule notI, simp add:co2sobj.simps split:option.splits)
 apply (tactic {*my_setiff_tac 1*})
 apply (rule_tac x = "O_file f" in exI)
-apply (simp add:co2sobj.simps is_file_simps tainted_eq_Tainted cf2sfiles_other has_same_inode_prop3)
+apply (simp add:co2sobj.simps is_file_simps tainted_eq_Tainted cf2sfiles_other same_inode_files_prop12)
 apply (tactic {*my_setiff_tac 1*})
 apply (erule_tac obj = obj in co2sobj_some_caseD)
 apply (rule_tac x = obj in exI, simp add:co2sobj_truncate)
diff -r 0753309adfc7 -r 6f9a588bcfc4 Static.thy
--- a/Static.thy	Thu Oct 24 09:42:35 2013 +0800
+++ b/Static.thy	Wed Oct 30 08:18:40 2013 +0800
@@ -122,6 +122,122 @@
 definition  
   "init_static_state \<equiv> {sobj. \<exists> obj. init_alive obj \<and> init_obj2sobj obj = Some sobj}"
 
+(**************** translation from dynamic to static *******************)
+
+definition cf2sfile :: "t_state \<Rightarrow> t_file \<Rightarrow> t_sfile option"
+where
+  "cf2sfile s f \<equiv>
+     case (parent f) of 
+       None \<Rightarrow> Some sroot
+     | Some pf \<Rightarrow> if (is_file s f) 
+     then (case (sectxt_of_obj s (O_file f), sectxt_of_obj s (O_dir pf), get_parentfs_ctxts s pf) of
+            (Some sec, Some psec, Some asecs) \<Rightarrow>
+ Some (if (\<not> deleted (O_file f) s \<and> is_init_file f) then Init f else Created, sec, Some psec, set asecs)
+          | _ \<Rightarrow> None) 
+     else (case (sectxt_of_obj s (O_dir f), sectxt_of_obj s (O_dir pf), get_parentfs_ctxts s pf) of
+            (Some sec, Some psec, Some asecs) \<Rightarrow>
+ Some (if (\<not> deleted (O_dir f) s \<and> is_init_dir f) then Init f else Created, sec, Some psec, set asecs)
+          | _ \<Rightarrow> None)"
+
+definition cf2sfiles :: "t_state \<Rightarrow> t_file \<Rightarrow> t_sfile set"
+where
+  "cf2sfiles s f \<equiv> {sf. \<exists> f' \<in> (same_inode_files s f). cf2sfile s f' = Some sf}"
+
+(* here cf2sfile is passed with True, because, process' fds are only for files not dirs *)
+definition cfd2sfd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd \<Rightarrow> t_sfd option" 
+where
+  "cfd2sfd s p fd \<equiv> 
+    (case (file_of_proc_fd s p fd, flags_of_proc_fd s p fd, sectxt_of_obj s (O_fd p fd)) of
+      (Some f, Some flags, Some sec) \<Rightarrow> (case (cf2sfile s f) of 
+                                          Some sf \<Rightarrow> Some (sec, flags, sf)
+                                        | _       \<Rightarrow> None)
+    | _ \<Rightarrow> None)"
+
+
+definition cpfd2sfds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sfd set"
+where
+  "cpfd2sfds s p \<equiv> {sfd. \<exists> fd \<in> proc_file_fds s p. cfd2sfd s p fd = Some sfd}"
+
+definition ch2sshm :: "t_state \<Rightarrow> t_shm \<Rightarrow> t_sshm option"
+where
+  "ch2sshm s h \<equiv> (case (sectxt_of_obj s (O_shm h)) of
+                    Some sec \<Rightarrow> 
+ Some (if (\<not> deleted (O_shm h) s \<and> h \<in> init_shms) then Init h else Created, sec)
+                  | _ \<Rightarrow> None)"
+
+definition cph2spshs :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sproc_sshm set"
+where
+  "cph2spshs s p \<equiv> {(sh, flag)| sh flag h. (p, flag) \<in> procs_of_shm s h \<and> ch2sshm s h = Some sh}"
+
+definition cp2sproc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sproc option"
+where
+  "cp2sproc s p \<equiv> (case (sectxt_of_obj s (O_proc p)) of 
+                     Some sec \<Rightarrow> 
+ Some (if (\<not> deleted (O_proc p) s \<and> p \<in> init_procs) then Init p else Created, sec, 
+       cpfd2sfds s p, cph2spshs s p)
+                   | _ \<Rightarrow> None)"
+
+definition cm2smsg :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsg option"
+where
+  "cm2smsg s q m \<equiv> (case (sectxt_of_obj s (O_msg q m)) of 
+                      Some sec \<Rightarrow>
+ Some (if (\<not> deleted (O_msg q m) s \<and> m \<in> set (init_msgs_of_queue q)) then Init m else Created,
+       sec, O_msg q m \<in> tainted s)
+                    | _ \<Rightarrow> None)"
+
+fun cqm2sms:: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg list \<Rightarrow> (t_smsg list) option"
+where 
+  "cqm2sms s q [] = Some []"
+| "cqm2sms s q (m#ms) = 
+     (case (cqm2sms s q ms, cm2smsg s q m) of 
+       (Some sms, Some sm) \<Rightarrow> Some (sm#sms) 
+     | _ \<Rightarrow> None)"
+
+definition cq2smsgq :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_smsgq option"
+where
+  "cq2smsgq s q \<equiv> (case (sectxt_of_obj s (O_msgq q), cqm2sms s q (msgs_of_queue s q)) of 
+                     (Some sec, Some sms) \<Rightarrow> 
+ Some (if (\<not> deleted (O_msgq q) s \<and> q \<in> init_msgqs) then Init q else Created,
+       sec, sms)
+                   | _ \<Rightarrow> None)"
+
+fun co2sobj :: "t_state \<Rightarrow> t_object \<Rightarrow> t_sobject option"
+where
+  "co2sobj s (O_proc p) = 
+     (case (cp2sproc s p) of 
+        Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))
+      | _       \<Rightarrow> None)"
+| "co2sobj s (O_file f) = 
+     Some (S_file (cf2sfiles s f) (O_file f \<in> tainted s))"
+| "co2sobj s (O_dir f) = 
+     (case (cf2sfile s f) of
+        Some sf  \<Rightarrow> Some (S_dir sf)
+      | _ \<Rightarrow> None)"
+| "co2sobj s (O_msgq q) = 
+     (case (cq2smsgq s q) of
+        Some sq \<Rightarrow> Some (S_msgq sq)
+      | _ \<Rightarrow> None)"
+| "co2sobj s (O_shm h) = 
+     (case (ch2sshm s h) of 
+        Some sh \<Rightarrow> Some (S_shm sh)
+      | _ \<Rightarrow> None)"
+(*
+| "co2sobj s (O_msg q m) = 
+     (case (cq2smsgq s q, cm2smsg s q m) of 
+       (Some sq, Some sm) \<Rightarrow> Some (S_msg sq sm)
+     | _ \<Rightarrow> None)"
+*)
+| "co2sobj s _ = None"
+
+
+definition s2ss :: "t_state \<Rightarrow> t_static_state"
+where
+  "s2ss s \<equiv> {sobj. \<exists> obj. alive s obj \<and> co2sobj s obj = Some sobj}"
+
+
+(* ******************************************************** *)
+
+
 fun is_init_sfile :: "t_sfile \<Rightarrow> bool"
 where
   "is_init_sfile (Init _, sec, psec,asec) = True"
@@ -204,18 +320,6 @@
       else (ss - {S_dir sf tag}) \<union> {S_dir sf' tag'})"
 *)
 
-definition update_ss :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state"
-where
-  "update_ss ss so so' \<equiv> if (is_many so) then ss \<union> {so'} else (ss - {so}) \<union> {so'}"
-
-definition add_ss :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_static_state"
-where
-  "add_ss ss so \<equiv> ss \<union> {so}"
-
-definition del_ss :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_static_state"
-where
-  "del_ss ss so \<equiv> if (is_many so) then ss else ss - {so}"
-
 (*
 fun sparent :: "t_sfile \<Rightarrow> t_sfile option"
 where
@@ -487,147 +591,6 @@
 | "\<lbrakk>info_flow_sshm sp (pi,sec,fds,shms); info_flow_sproc_sshms shms shms'\<rbrakk>
    \<Longrightarrow> info_flow_sshm sp (pi',sec',fds',shms')"
 
-definition update_ss_shms :: "t_static_state \<Rightarrow> t_sproc \<Rightarrow> bool \<Rightarrow> t_static_state"
-where
-  "update_ss_shms ss spfrom tag \<equiv> {sobj. \<exists> sobj' \<in> ss. 
-     (case sobj' of 
-        S_proc sp tagp \<Rightarrow> if (info_flow_sshm spfrom sp) 
-                          then if (is_many_sproc sp)
-                               then (sobj = S_proc sp tagp \<or> sobj = S_proc sp (tagp \<or> tag))
-                               else (sobj = S_proc sp (tagp \<or> tag))
-                          else (sobj = S_proc sp tag)
-     | _ \<Rightarrow> sobj = sobj')}"
-
-
-
-(* all reachable static states(sobjects set) *)
-inductive_set static :: "t_static_state set"
-where
-  s_init:    "init_static_state \<in> static"
-| s_execve:  "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; S_file sfs tagf \<in> ss;
-               (fi,fsec,pfsec,asecs) \<in> sfs; npctxt_execve pctxt fsec = Some pctxt';
-               grant_execve pctxt fsec pctxt'; search_check_s pctxt (fi,fsec,pfsec,asecs) True; 
-               inherit_fds_check_s pctxt' fds'; fds' \<subseteq> fds\<rbrakk>
-  \<Longrightarrow> (update_ss ss (S_proc (pi, pctxt, fds, shms) tagp) 
-                    (S_proc (pi, pctxt', fds', {}) (tagp \<or> tagf))) \<in> static"
-| s_clone:   "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; 
-               permission_check pctxt pctxt C_process P_fork;
-               inherit_fds_check_s pctxt fds'; fds' \<subseteq> fds; 
-               inherit_shms_check_s pctxt shms'; shms' \<subseteq> shms\<rbrakk>
-  \<Longrightarrow> (add_ss ss (S_proc (Created, pctxt, fds', shms') tagp)) \<in> static"
-| s_kill:    "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; 
-               S_proc (pi', pctxt', fds', shms') tagp' \<in> ss; 
-               permission_check pctxt pctxt' C_process P_sigkill\<rbrakk>
-  \<Longrightarrow> (del_ss ss (S_proc (pi', pctxt', fds', shms') tagp')) \<in> static"
-| s_ptrace:  "\<lbrakk>ss \<in> static; S_proc sp tagp \<in> ss; S_proc sp' tagp' \<in> ss; 
-               permission_check (sextxt_of_sproc sp) (sectxt_of_sproc sp') C_process P_ptrace\<rbrakk>
-  \<Longrightarrow> (update_ss_shms (update_ss_shms ss sp tagp) sp' tagp') \<in> static"
-| s_exit:    "\<lbrakk>ss \<in> static; S_proc sp tagp \<in> ss\<rbrakk> \<Longrightarrow> (del_ss ss (S_proc sp tagp)) \<in> static"
-| s_open:    "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; S_file sfs tagf \<in> ss; sf \<in> sfs;
-              search_check_s pctxt sf True; \<not> is_creat_excl_flag flags; 
-              oflags_check flags pctxt (sectxt_of_sfile sf); permission_check pctxt pctxt C_fd P_setattr\<rbrakk>
-  \<Longrightarrow> (update_ss ss (S_proc (pi, pctxt, fds, shms) tagp)
-                    (S_proc (pi, pctxt, fds \<union> {(pctxt,flags,sf)}, shms) tagp)) \<in> static"
-| s_open':   "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; is_creat_excl_flag flags;
-               S_dir (pfi,fsec,pfsec,asecs) \<in> ss; search_check_s pctxt (pfi,fsec,pfsec,asecs) False; 
-               nfsec = nfctxt_create pctxt fsec C_file; oflags_check flags pctxt nfsec;
-               permission_check pctxt fsec C_dir P_add_rename; permission_check pctxt pctxt C_fd P_setattr\<rbrakk>
-  \<Longrightarrow> (update_ss (add_ss ss (S_file {(Created, nfsec, Some fsec, asecs \<union> {fsec})} tagp))
-         (S_proc (pi, pctxt, fds, shms) tagp)
-         (S_proc (pi, pctxt, fds \<union> {(pctxt, flags, (Created, nfsec, Some fsec, asecs \<union> {fsec}))}, shms) tagp)
-      ) \<in> static"
-| S_readf:   "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; (fdctxt,flags,sf) \<in> fds; 
-               permission_check pctxt fdctxt C_fd P_setattr; S_file sfs tagf \<in> ss; sf \<in> sfs;
-               permission_check pctxt (sectxt_of_sfile sf) C_file P_read; is_read_flag flags\<rbrakk>
-  \<Longrightarrow> (update_ss_shms ss (pi, pctxt,fds,shms) (tagp \<or> tagf)) \<in> static"
-| S_writef:  "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; (fdctxt,flags,sf) \<in> fds; 
-               permission_check pctxt fdctxt C_fd P_setattr; sf \<in> sfs; S_file sfs tagf \<in> ss; 
-               permission_check pctxt (sectxt_of_sfile sf) C_file P_write; is_write_flag flags\<rbrakk>
-  \<Longrightarrow> (update_ss ss (S_file sfs tagf) (S_file sfs (tagp \<or> tagf))) \<in> static"
-| S_unlink:  "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_file sfs tagf \<in> ss;  
-               (Init f,fsec,Some pfsec,asecs) \<in> sfs; 
-               search_check_s pctxt (Init f,fsec,Some pfsec,asecs) True; 
-               permission_check pctxt fsec C_file P_unlink; 
-               permission_check pctxt pfsec C_dir P_remove_name\<rbrakk>
-  \<Longrightarrow> ((ss - {S_file sfs tagf}) \<union> {S_file (sfs - {(Init f,fsec,Some pfsec,asecs)}) tagf}) \<in> static"
-| S_rmdir:   "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; 
-               S_dir (fi,fsec,Some pfsec,asecs) \<in> ss;  
-               search_check_s pctxt (fi,fsec,Some pfsec,asecs) False; 
-               permission_check pctxt fsec C_dir P_rmdir;
-               permission_check pctxt pfsec C_dir P_remove_name\<rbrakk>
-  \<Longrightarrow> (del_ss ss (S_dir (fi,fsec,Some pfsec,asecs))) \<in> static"
-| S_mkdir:   "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_dir (fi,fsec,pfsec,asecs) \<in> ss;  
-               search_check_s pctxt (fi,fsec,pfsec,asecs) False; 
-               permission_check pctxt (nfctxt_create pctxt fsec C_dir) C_dir P_create;
-               permission_check pctxt fsec C_dir P_add_name\<rbrakk>
-  \<Longrightarrow> (add_ss ss (S_dir (Created,nfctxt_create pctxt fsec C_dir,Some fsec,asecs \<union> {fsec}))) \<in> static"
-| s_link:    "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_dir (pfi,pfsec,ppfsec,asecs) \<in> ss;
-               S_file sfs tagf \<in> ss; sf \<in> sfs; nfsec = nfctxt_create pctxt pfsec C_file;  
-               search_check_s pctxt (pfi,pfsec,ppfsec,asecs) False; search_check_s pctxt sf True;
-               permission_check pctxt (sectxt_of_sfile sf) C_file P_link; 
-               permission_check pctxt pfsec C_dir P_add_name\<rbrakk>
-  \<Longrightarrow> (update_ss ss (S_file sfs tagf) 
-                  (S_file (sfs \<union> {(Created,nfsec,Some pfsec, asecs \<union> {pfsec})}) tagf)) \<in> static"
-| s_trunc:   "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_file sfs tagf \<in> ss; sf \<in> sfs; 
-               search_check_s pctxt sf True; permission_check pctxt (sectxt_of_sfile sf) C_file P_setattr\<rbrakk>
-  \<Longrightarrow> (update_ss ss (S_file sfs tagf) (S_file sfs (tagf \<or> tagp))) \<in> static"
-(*
-| s_rename:  "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_file sfs tagf \<in> ss;
-               (sf#spf') \<in> sfs; S_dir spf tagpf \<in> ss; \<not>((sf#spf') \<preceq> (sf#spf)); 
-               search_check_s pctxt spf False; search_check_s pctxt (sf#spf') True; 
-               sectxt_of_sfile (sf#spf') = Some fctxt; sectxt_of_sfile spf = Some pfctxt;  
-               permission_check pctxt fctxt C_file P_rename;
-               permission_check pctxt pfctxt C_dir P_add_name;
-               ss_rename ss (sf#spf') (sf#spf) ss'; 
-               ss_rename_no_same_fname ss (sf#spf') (sf#spf)\<rbrakk>
-              \<Longrightarrow> ss' \<in> static"
-| s_rename': "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_dir (sf#spf') tagf \<in> ss;
-               S_dir spf tagpf \<in> ss; \<not>((sf#spf') \<preceq> (sf#spf)); 
-               search_check_s pctxt spf False; search_check_s pctxt (sf#spf') True; 
-               sectxt_of_sfile (sf#spf') = Some fctxt; sectxt_of_sfile spf = Some pfctxt;  
-               permission_check pctxt fctxt C_dir P_reparent;
-               permission_check pctxt pfctxt C_dir P_add_name;
-               ss_rename ss (sf#spf') (sf#spf) ss'; 
-               ss_rename_no_same_fname ss (sf#spf') (sf#spf)\<rbrakk>
-              \<Longrightarrow> ss' \<in> static"
-*)
-| s_createq: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; 
-               permission_check pctxt pctxt C_msgq P_associate;
-               permission_check pctxt pctxt C_msgq P_create\<rbrakk>
-  \<Longrightarrow> (add_ss ss (S_msgq (Created,pctxt,[]))) \<in> static" 
-| s_sendmsg: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_msgq (qi,qctxt,sms) \<in> ss;
-               permission_check pctxt qctxt C_msgq P_enqueue;
-               permission_check pctxt qctxt C_msgq P_write; 
-               permission_check pctxt pctxt C_msg  P_create\<rbrakk>
-  \<Longrightarrow> (update_ss ss (S_msgq (qi,qctxt,sms)) 
-                    (S_msgq (qi,qctxt,sms @ [(Created, pctxt, tagp)]))) \<in> static"
-| s_recvmsg: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; 
-               S_msgq (qi,qctxt,(mi,mctxt,tagm)#sms) \<in> ss;
-               permission_check pctxt qctxt C_msgq P_read; 
-               permission_check pctxt mctxt C_msg  P_receive\<rbrakk>
-  \<Longrightarrow> (update_ss (update_ss_shms ss (pi,pctxt,fds,shms) (tagp \<or> tagm)) 
-                 (S_msgq (qi, qctxt, (mi, mctxt, tagm)#sms))
-                 (S_msgq (qi, qctxt, sms))) \<in> static"
-| s_removeq: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_msgq (qi,qctxt,sms) \<in> ss;
-               permission_check pctxt qctxt C_msgq P_destroy\<rbrakk>
-  \<Longrightarrow> (del_ss ss (S_msgq (qi,qctxt,sms))) \<in> static"
-| s_createh: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss;
-               permission_check pctxt pctxt C_shm P_associate; 
-               permission_check pctxt pctxt C_shm P_create\<rbrakk>
-   \<Longrightarrow> (add_ss ss (S_shm (Created, pctxt))) \<in> static"
-| s_attach:  "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_shm (hi,hctxt) \<in> ss;
-               if flag = SHM_RDONLY then permission_check pctxt hctxt C_shm P_read
-               else (permission_check pctxt hctxt C_shm P_read \<and>
-                     permission_check pctxt hctxt C_shm P_write)\<rbrakk>
-   \<Longrightarrow> (update_ss ss (S_proc (pi,pctxt,fds,shms) tagp)
-                    (S_proc (pi,pctxt,fds,shms \<union> {((hi,hctxt),flag)}) tagp)) \<in> static"
-| s_detach:  "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_shm sh \<in> ss;
-               (sh,flag) \<in> shms; \<not> is_many_sshm sh\<rbrakk>
-   \<Longrightarrow> (update_ss ss (S_proc (pi,pctxt,fds,shms) tagp)
-                    (S_proc (pi,pctxt,fds,shms - {(sh,flag)}) tagp)) \<in> static"
-| s_deleteh: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_shm (hi,hctxt) \<in> ss;
-               permission_check pctxt hctxt C_shm P_destroy; \<not> is_many_sshm sh\<rbrakk>
-   \<Longrightarrow> (remove_sproc_sshm (del_ss ss (S_shm (hi,hctxt))) (hi,hctxt)) \<in> static"
 
 (*
 fun smsg_related :: "t_msg \<Rightarrow> t_smsg list \<Rightarrow> bool" 
@@ -672,144 +635,6 @@
 *)
 | "init_obj_related _ _ = False"
 
-fun tainted_s :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> bool"
-where
-  "tainted_s ss (S_proc sp  tag) = (S_proc sp tag  \<in> ss \<and> tag = True)"
-| "tainted_s ss (S_file sfs tag) = (S_file sfs tag \<in> ss \<and> tag = True)"
-(*
-| "tainted_s ss (S_msg  (qi, sec, sms)  (mi, secm, tag)) = 
-     (S_msgq (qi, sec, sms) \<in> ss \<and> (mi,secm,tag) \<in> set sms \<and> tag = True)"
-*)
-| "tainted_s ss _ = False"
-
-(*
-fun tainted_s :: "t_object \<Rightarrow> t_static_state \<Rightarrow> bool"
-where 
-  "tainted_s (O_proc p)  ss = (\<exists> sp. S_proc sp True \<in> ss \<and> sproc_related p sp)"
-| "tainted_s (O_file f)  ss = (\<exists> sfs sf. S_file sfs True \<in> ss \<and> sf \<in> sfs \<and> sfile_related f sf)"
-| "tainted_s (O_msg q m) ss = (\<exists> sq. S_msgq sq \<in> ss \<and> smsgq_smsg_relatainted q m sq)"
-| "tainted_s _           ss = False"
-*)
-
-definition taintable_s :: "t_object \<Rightarrow> bool"
-where
-  "taintable_s obj \<equiv> \<exists> ss \<in> static. \<exists> sobj. tainted_s ss sobj \<and> init_obj_related sobj obj \<and> init_alive obj"
-
-definition deletable_s :: "t_object \<Rightarrow> bool"
-where
-  "deletable_s obj \<equiv> init_alive obj \<and> (\<exists> ss \<in> static. \<forall> sobj \<in> ss. \<not> init_obj_related sobj obj)"
-
-definition undeletable_s :: "t_object \<Rightarrow> bool"
-where
-  "undeletable_s obj \<equiv> init_alive obj \<and> (\<forall> ss \<in> static. \<exists> sobj \<in> ss. init_obj_related sobj obj)"
-
-
-(**************** translation from dynamic to static *******************)
-
-definition cf2sfile :: "t_state \<Rightarrow> t_file \<Rightarrow> t_sfile option"
-where
-  "cf2sfile s f \<equiv>
-     case (parent f) of 
-       None \<Rightarrow> Some sroot
-     | Some pf \<Rightarrow> if (is_file s f) 
-     then (case (sectxt_of_obj s (O_file f), sectxt_of_obj s (O_dir pf), get_parentfs_ctxts s pf) of
-            (Some sec, Some psec, Some asecs) \<Rightarrow>
- Some (if (\<not> deleted (O_file f) s \<and> is_init_file f) then Init f else Created, sec, Some psec, set asecs)
-          | _ \<Rightarrow> None) 
-     else (case (sectxt_of_obj s (O_dir f), sectxt_of_obj s (O_dir pf), get_parentfs_ctxts s pf) of
-            (Some sec, Some psec, Some asecs) \<Rightarrow>
- Some (if (\<not> deleted (O_dir f) s \<and> is_init_dir f) then Init f else Created, sec, Some psec, set asecs)
-          | _ \<Rightarrow> None)"
-
-definition cf2sfiles :: "t_state \<Rightarrow> t_file \<Rightarrow> t_sfile set"
-where
-  "cf2sfiles s f \<equiv> {sf. \<exists> f' \<in> (same_inode_files s f). cf2sfile s f' = Some sf}"
-
-(* here cf2sfile is passed with True, because, process' fds are only for files not dirs *)
-definition cfd2sfd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd \<Rightarrow> t_sfd option" 
-where
-  "cfd2sfd s p fd \<equiv> 
-    (case (file_of_proc_fd s p fd, flags_of_proc_fd s p fd, sectxt_of_obj s (O_fd p fd)) of
-      (Some f, Some flags, Some sec) \<Rightarrow> (case (cf2sfile s f) of 
-                                          Some sf \<Rightarrow> Some (sec, flags, sf)
-                                        | _       \<Rightarrow> None)
-    | _ \<Rightarrow> None)"
-
-
-definition cpfd2sfds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sfd set"
-where
-  "cpfd2sfds s p \<equiv> {sfd. \<exists> fd \<in> proc_file_fds s p. cfd2sfd s p fd = Some sfd}"
-
-definition ch2sshm :: "t_state \<Rightarrow> t_shm \<Rightarrow> t_sshm option"
-where
-  "ch2sshm s h \<equiv> (case (sectxt_of_obj s (O_shm h)) of
-                    Some sec \<Rightarrow> 
- Some (if (\<not> deleted (O_shm h) s \<and> h \<in> init_shms) then Init h else Created, sec)
-                  | _ \<Rightarrow> None)"
-
-definition cph2spshs :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sproc_sshm set"
-where
-  "cph2spshs s p \<equiv> {(sh, flag)| sh flag h. (p, flag) \<in> procs_of_shm s h \<and> ch2sshm s h = Some sh}"
-
-definition cp2sproc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sproc option"
-where
-  "cp2sproc s p \<equiv> (case (sectxt_of_obj s (O_proc p)) of 
-                     Some sec \<Rightarrow> 
- Some (if (\<not> deleted (O_proc p) s \<and> p \<in> init_procs) then Init p else Created, sec, 
-       cpfd2sfds s p, cph2spshs s p)
-                   | _ \<Rightarrow> None)"
-
-definition cm2smsg :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsg option"
-where
-  "cm2smsg s q m \<equiv> (case (sectxt_of_obj s (O_msg q m)) of 
-                      Some sec \<Rightarrow>
- Some (if (\<not> deleted (O_msg q m) s \<and> m \<in> set (init_msgs_of_queue q)) then Init m else Created,
-       sec, O_msg q m \<in> tainted s)
-                    | _ \<Rightarrow> None)"
-
-fun cqm2sms:: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg list \<Rightarrow> (t_smsg list) option"
-where 
-  "cqm2sms s q [] = Some []"
-| "cqm2sms s q (m#ms) = 
-     (case (cqm2sms s q ms, cm2smsg s q m) of 
-       (Some sms, Some sm) \<Rightarrow> Some (sm#sms) 
-     | _ \<Rightarrow> None)"
-
-definition cq2smsgq :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_smsgq option"
-where
-  "cq2smsgq s q \<equiv> (case (sectxt_of_obj s (O_msgq q), cqm2sms s q (msgs_of_queue s q)) of 
-                     (Some sec, Some sms) \<Rightarrow> 
- Some (if (\<not> deleted (O_msgq q) s \<and> q \<in> init_msgqs) then Init q else Created,
-       sec, sms)
-                   | _ \<Rightarrow> None)"
-
-fun co2sobj :: "t_state \<Rightarrow> t_object \<Rightarrow> t_sobject option"
-where
-  "co2sobj s (O_proc p) = 
-     (case (cp2sproc s p) of 
-        Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))
-      | _       \<Rightarrow> None)"
-| "co2sobj s (O_file f) = 
-     Some (S_file (cf2sfiles s f) (O_file f \<in> tainted s))"
-| "co2sobj s (O_dir f) = 
-     (case (cf2sfile s f) of
-        Some sf  \<Rightarrow> Some (S_dir sf)
-      | _ \<Rightarrow> None)"
-| "co2sobj s (O_msgq q) = 
-     (case (cq2smsgq s q) of
-        Some sq \<Rightarrow> Some (S_msgq sq)
-      | _ \<Rightarrow> None)"
-| "co2sobj s (O_shm h) = 
-     (case (ch2sshm s h) of 
-        Some sh \<Rightarrow> Some (S_shm sh)
-      | _ \<Rightarrow> None)"
-(*
-| "co2sobj s (O_msg q m) = 
-     (case (cq2smsgq s q, cm2smsg s q m) of 
-       (Some sq, Some sm) \<Rightarrow> Some (S_msg sq sm)
-     | _ \<Rightarrow> None)"
-*)
-| "co2sobj s _ = None"
 
 
 (***************** for backward proof when Instancing static objects ******************)
@@ -863,10 +688,6 @@
 where
   "new_childf pf \<tau> = next_fname pf \<tau> # pf"
 
-definition s2ss :: "t_state \<Rightarrow> t_static_state"
-where
-  "s2ss s \<equiv> {sobj. \<exists> obj. alive s obj \<and> co2sobj s obj = Some sobj}"
-
 end
 
 end
\ No newline at end of file
diff -r 0753309adfc7 -r 6f9a588bcfc4 Tainted_prop.thy
--- a/Tainted_prop.thy	Thu Oct 24 09:42:35 2013 +0800
+++ b/Tainted_prop.thy	Wed Oct 30 08:18:40 2013 +0800
@@ -36,7 +36,7 @@
 | "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'}
+                  then Tainted s \<union> {O_file f' | f'. f' \<in> same_inode_files s f}
                   else Tainted s
       | None   \<Rightarrow> Tainted s)"
 | "Tainted (CloseFd p fd # s) = 
@@ -50,7 +50,7 @@
      (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'}
+      then Tainted s \<union> {O_file f' | f'. f' \<in> same_inode_files s f}
       else Tainted s)"
 | "Tainted (Attach p h flag # s) = 
      (if (O_proc p \<in> Tainted s \<and> flag = SHM_RDWR) 
@@ -80,8 +80,9 @@
 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
-           intro:has_same_inode_prop2 has_same_inode_prop1 procs_of_shm_prop2 
+           intro:same_inode_files_prop1 procs_of_shm_prop2 
             dest:info_shm_flow_in_procs)
+apply (auto simp:same_inode_files_def is_file_def split:if_splits)
 done 
 
 lemma Tainted_proc_in_current:
@@ -161,6 +162,10 @@
 qed
 qed
 
+lemma has_same_inode_comm:
+  "has_same_inode s f f' = has_same_inode s f' f"
+by (auto simp add:has_same_inode_def same_inode_files_def is_file_def)
+
 lemma tainted_imp_Tainted:
   "obj \<in> tainted s \<Longrightarrow> obj \<in> Tainted s"
 apply (induct rule:tainted.induct)  (*
@@ -170,7 +175,7 @@
 apply (rule disjI2, rule_tac x = flag' in exI, simp)
 apply ((rule impI)+, erule_tac x = p' in allE, simp)
 *)
-apply (auto intro:info_flow_shm_Tainted dest:vd_cons)
+apply (auto intro:info_flow_shm_Tainted simp:has_same_inode_def dest:vd_cons)
 apply (case_tac e, auto split:option.splits if_splits simp:alive_simps)
 done
 
@@ -184,7 +189,8 @@
 apply (induct s arbitrary:obj, simp add:t_init)
 apply (frule Tainted_in_current, simp+)
 apply (frule vt_grant_os, frule vd_cons, case_tac a)
-apply (auto split:if_splits option.splits elim:Tainted_imp_tainted_aux_remain intro:tainted.intros)
+apply (auto split:if_splits option.splits elim:Tainted_imp_tainted_aux_remain intro:tainted.intros
+  simp:has_same_inode_def)
 done
 
 lemma tainted_eq_Tainted:
@@ -195,19 +201,43 @@
   "\<lbrakk>O_proc p \<in> tainted s; info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> O_proc p' \<in> tainted s"
 by (simp only:tainted_eq_Tainted info_flow_shm_Tainted)
 
+
+lemma same_inode_files_Tainted:
+  "\<lbrakk>O_file f \<in> Tainted s; f' \<in> same_inode_files s f; valid s\<rbrakk> \<Longrightarrow> O_file f' \<in> Tainted s"
+apply (induct s arbitrary:f f', simp add:same_inode_in_seeds has_same_inode_def)
+apply (frule vt_grant_os, frule vd_cons, case_tac a)
+prefer 6
+apply (simp split:if_splits option.splits add:same_inode_files_open current_files_simps)
+prefer 8
+apply (frule Tainted_in_current, simp, simp add:alive.simps, drule is_file_in_current)
+apply (auto simp add:same_inode_files_closefd split:option.splits if_splits)[1]
+prefer 8
+apply (frule Tainted_in_current, simp, simp add:alive.simps, drule is_file_in_current)
+apply (auto simp add:same_inode_files_unlink split:option.splits if_splits)[1]
+prefer 10
+apply (auto split:if_splits option.splits simp:same_inode_files_linkhard current_files_simps)[1]
+apply (drule Tainted_in_current, simp, simp add:alive.simps is_file_in_current)
+apply (drule same_inode_files_prop5, simp)
+apply (drule same_inode_files_prop5, drule_tac f' = list1 and f'' = f' in same_inode_files_prop4, simp, simp)
+
+apply (auto simp:same_inode_files_other split:if_splits)
+apply (drule_tac f'' = f' and f' = f and f = fa in same_inode_files_prop4, simp+)
+apply (drule_tac f'' = f' and f' = f and f = list in same_inode_files_prop4, simp+)
+done
+
 lemma has_same_inode_Tainted:
   "\<lbrakk>O_file f \<in> Tainted s; has_same_inode s f f'; valid s\<rbrakk> \<Longrightarrow> O_file f' \<in> Tainted s"
-apply (induct s arbitrary:f f', simp add:same_inode_in_seeds)
-apply (frule vt_grant_os, frule vd_cons, case_tac a)
-apply (auto split:if_splits option.splits simp:has_same_inode_def dest:iof's_im_in_cim)
-apply (drule_tac obj = "O_file list2" in Tainted_in_current, simp, simp add:is_file_in_current) 
-done
+by (simp add:has_same_inode_def same_inode_files_Tainted)
 
 lemma has_same_inode_tainted:
   "\<lbrakk>O_file f \<in> tainted s; has_same_inode s f f'; valid s\<rbrakk> \<Longrightarrow> O_file f' \<in> tainted s"
 by (simp add:has_same_inode_Tainted tainted_eq_Tainted)
 
-
+lemma same_inodes_Tainted:
+  "\<lbrakk>f \<in> same_inode_files s f'; valid s\<rbrakk> \<Longrightarrow> (O_file f \<in> Tainted s) = (O_file f' \<in> Tainted s)"
+apply (frule same_inode_files_prop8, frule same_inode_files_prop7)
+apply (auto intro:has_same_inode_Tainted)
+done