diff -r 029cccce84b4 -r 9dfc8c72565a S2ss_prop.thy
--- a/S2ss_prop.thy	Tue Sep 03 07:25:39 2013 +0800
+++ b/S2ss_prop.thy	Tue Sep 03 09:31:40 2013 +0800
@@ -137,6 +137,16 @@
   "f' \<in> same_inode_files s f \<Longrightarrow> f \<in> same_inode_files s f'"
 by (auto simp:same_inode_files_def is_file_def split:if_splits)
 
+lemma same_inode_files_prop6:
+  "f' \<in> same_inode_files s f \<Longrightarrow> same_inode_files s f' = same_inode_files s f"
+by (auto simp:same_inode_files_def is_file_def split:if_splits)
+
+lemma same_inode_files_prop7:
+  "f' \<in> same_inode_files s f \<Longrightarrow> has_same_inode s f f'"
+thm has_same_inode_def
+apply (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits)
+
+
 (* simpset for cf2sfiles *)
 
 lemma cf2sfiles_open:
@@ -355,11 +365,10 @@
             | _       \<Rightarrow> None) 
       else co2sobj s obj )"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
+apply (simp_all add:current_files_simps cf2sfiles_other ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
 apply (case_tac "cp2sproc (Execve p f fds # s) p")
 apply (drule current_proc_has_sp', simp, simp)
 apply (simp (no_asm_simp) add:cp2sproc_execve tainted_eq_Tainted split:option.splits)
-apply (rule impI, simp add:cf2sfiles_other) 
 apply (frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp)
 apply (frule_tac ff = list in cf2sfile_other', simp_all)
 apply (simp add:is_dir_in_current)
@@ -373,14 +382,13 @@
             | _       \<Rightarrow> None)
       else co2sobj s obj )"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
+apply (simp_all add:current_files_simps cf2sfiles_other ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
 apply (case_tac "cp2sproc (Clone p p' fds shms # s) p'")
 apply (drule current_proc_has_sp', simp, simp)
 apply ((erule conjE)+, frule_tac p = p in current_proc_has_sec, simp, erule exE, simp)
 apply (rule conjI, rule impI, simp)
 apply (simp (no_asm_simp) add:cp2sproc_clone tainted_eq_Tainted split:option.splits)
 
-apply (rule impI, simp add:cf2sfiles_other) 
 apply (frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp)
 apply (frule_tac ff = list in cf2sfile_other', simp_all)
 apply (simp add:is_dir_in_current)
@@ -401,6 +409,7 @@
     | _          \<Rightarrow> co2sobj s obj)"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
 apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other cf2sfiles_other tainted_eq_Tainted)
+
 apply (auto simp:cp2sproc_other tainted_eq_Tainted split:option.splits
   dest!:current_proc_has_sec' current_proc_has_sp' intro:info_flow_shm_Tainted)[1]
 
@@ -424,15 +433,72 @@
                   else co2sobj s (O_proc p')
    | _         \<Rightarrow> co2sobj s obj )"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
-apply (auto simp:cp2sproc_simps cf2sfiles_simps cf2sfile_simps current_files_simps 
-is_file_simps tainted_eq_Tainted split:option.splits
-           dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)
+apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits
+           dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]
+
+apply (simp split:if_splits t_object.splits)
+apply (rule conjI, rule impI, erule conjE, erule exE, simp, (erule exE|erule conjE)+)
+apply (case_tac "cf2sfile (Open p f flag fd (Some y) # s) f")
+apply (drule current_file_has_sfile', simp, simp add:current_files_simps, simp)
+apply (frule_tac f' = f in cf2sfiles_open, simp add:current_files_simps)
+apply (simp add:tainted_eq_Tainted)
+apply (rule impI, rule notI, drule Tainted_in_current, simp, simp add:is_file_in_current)
+apply (rule impI, simp add:tainted_eq_Tainted cf2sfiles_open is_file_in_current split:option.splits)
+
 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
-apply (auto simp:cp2sproc_simps cf2sfiles_simps cf2sfile_simps current_files_simps 
-is_file_simps tainted_eq_Tainted split:option.splits
-           dest!:current_proc_has_sp' current_file_has_sfile' intro:info_flow_shm_Tainted)
-apply (
-apply 
+
+apply (frule is_dir_in_current)
+apply (frule_tac f' = list in cf2sfile_open)
+apply (simp add:current_files_simps split:option.splits)
+apply (simp split:if_splits option.splits)
+done
+
+lemma co2sobj_readfile:
+  "\<lbrakk>valid (ReadFile p fd # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (ReadFile p fd # s) obj = (
+     case obj of
+       O_proc p' \<Rightarrow> (case (file_of_proc_fd s p fd) of
+                       Some f \<Rightarrow> (if (info_flow_shm s p p' \<and> O_file f \<in> Tainted s)
+                                  then (case (cp2sproc s p') of
+                                          Some sp \<Rightarrow> Some (S_proc sp True)
+                                        | _       \<Rightarrow> None)
+                                  else co2sobj s obj)
+                    | _       \<Rightarrow> None)
+     | _         \<Rightarrow> co2sobj s obj)"
+apply (frule vt_grant_os, frule vd_cons, case_tac obj)
+apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits
+           dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]
+apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
+
+apply (auto split:if_splits option.splits dest!:current_file_has_sfile' 
+             simp:current_files_simps cf2sfiles_simps cf2sfile_simps 
+             dest:is_file_in_current is_dir_in_current)
+done
+
+lemma co2sobj_writefile:
+  "\<lbrakk>valid (WriteFile p fd # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (WriteFile p fd # s) obj = (
+     case obj of
+       O_file f' \<Rightarrow> (case (file_of_proc_fd s p fd) of
+                       Some f \<Rightarrow> (if (f \<in> same_inode_files s f') 
+                                  then Some (S_file (cf2sfiles s f') 
+                                                    (O_file f' \<in> Tainted s \<or> O_proc p \<in> Tainted s))
+                                  else co2sobj s obj)
+                    | _       \<Rightarrow> None)
+     | _         \<Rightarrow> co2sobj s obj)"
+apply (frule vt_grant_os, frule vd_cons, case_tac obj)
+apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
+
+apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
+             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)
+thm has_same_inode_def
+done
+
+lemma co2sobj_closefd:
+  "\<lbrakk>valid (CloseFd p fd # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (CloseFd p fd # s) obj = (
+      case obj of 
+        O_file f' \<Rightarrow> (case (file_of_proc_fd s p fd) of 
+                        Some f \<Rightarrow> (if (f "
 
 lemma co2sobj_other:
   "\<lbrakk>valid (e # s); alive (e # s) obj; 
@@ -442,7 +508,7 @@
     \<forall> 
    \<rbrakk> \<Longrightarrow> co2sobj (e # s) obj = co2sobj s obj"
 
-lemmas co2sobj_simps = co2sobj_execve co2sobj_clone co2sobj_ptrace
+lemmas co2sobj_simps = co2sobj_execve co2sobj_clone co2sobj_ptrace co2sobj_open
 
 (* simpset for s2ss*)