# HG changeset patch
# User chunhan
# Date 1378256859 -28800
# Node ID 13bba99ca09029ff4c096a00dc8a1d44c13641e8
# Parent  9dfc8c72565a12bb81c0d06d058bfd6adc85eed5
done with co2sobj_simps

diff -r 9dfc8c72565a -r 13bba99ca090 S2ss_prop.thy
--- a/S2ss_prop.thy	Tue Sep 03 09:31:40 2013 +0800
+++ b/S2ss_prop.thy	Wed Sep 04 09:07:39 2013 +0800
@@ -143,9 +143,11 @@
 
 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)
+by (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits option.splits)
 
+lemma same_inode_files_prop8:
+  "f' \<in> same_inode_files s f \<Longrightarrow> has_same_inode s f' f"
+by (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits option.splits)
 
 (* simpset for cf2sfiles *)
 
@@ -491,24 +493,359 @@
              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
+
+(* should delete has_same_inode !?!?*)
+by (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits option.splits)
 
 lemma co2sobj_closefd:
-  "\<lbrakk>valid (CloseFd p fd # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (CloseFd p fd # s) obj = (
+  "\<lbrakk>valid (CloseFd p fd # s); alive (CloseFd p fd # 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 "
+                        Some f \<Rightarrow> (if (f' \<in> same_inode_files s f \<and> proc_fd_of_file s f = {(p, fd)} \<and>
+                                       f \<in> files_hung_by_del s \<and> (\<forall> f'' \<in> same_inode_files s f. 
+                                       f'' \<noteq> f \<longrightarrow> cf2sfile s f'' \<noteq> cf2sfile s f))
+                                   then (case (cf2sfile s f, co2sobj s (O_file f')) of
+                                           (Some sf, Some (S_file sfs b)) \<Rightarrow> Some (S_file (sfs - {sf}) b)
+                                         | _                              \<Rightarrow> None)
+                                   else co2sobj s obj)
+                     | _       \<Rightarrow> co2sobj s obj)
+      | O_proc p' \<Rightarrow> (if (p = p') 
+                      then (case (cp2sproc (CloseFd p fd # s) p) of
+                              Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s))
+                            | _       \<Rightarrow> None)
+                      else co2sobj s obj)
+      | _         \<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 tainted_eq_Tainted)
+apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits
+           dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]
+
+apply (frule is_file_in_current)
+apply (case_tac "file_of_proc_fd s p fd")
+apply (simp add:tainted_eq_Tainted)
+apply (drule_tac f' = list in cf2sfiles_closefd, simp add:current_files_closefd, simp)
+apply (frule_tac f' = list in cf2sfiles_closefd, simp)
+apply (simp add:is_file_simps current_files_simps)
+apply (auto simp add:tainted_eq_Tainted cf2sfile_closefd split:if_splits option.splits
+  dest!:current_file_has_sfile' dest:hung_file_in_current)[1]
+
+apply (simp add:is_dir_simps, frule is_dir_in_current)
+apply (frule_tac f = list in cf2sfile_closefd)
+apply (clarsimp simp:current_files_closefd split:option.splits)
+apply (drule file_of_pfd_is_file', simp+)
+done
+
+lemma co2sobj_unlink:
+  "\<lbrakk>valid (UnLink p f # s); alive (UnLink p f # s) obj\<rbrakk> \<Longrightarrow> co2sobj (UnLink p f # s) obj = (
+      case obj of
+        O_file f' \<Rightarrow> if (f' \<in> same_inode_files s f \<and> proc_fd_of_file s f = {} \<and> 
+                        (\<forall> f'' \<in> same_inode_files s f. f'' \<noteq> f \<longrightarrow> cf2sfile s f'' \<noteq> cf2sfile s f))
+                     then (case (cf2sfile s f, co2sobj s (O_file f')) of
+                             (Some sf, Some (S_file sfs b)) \<Rightarrow> Some (S_file (sfs - {sf}) b)
+                           | _                              \<Rightarrow> None)
+                     else co2sobj s obj
+      | _         \<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 tainted_eq_Tainted)
+apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits
+           dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]
+apply (frule is_file_in_current)
+apply (frule_tac f' = list in cf2sfile_unlink, simp)
+apply (frule_tac f' = list in cf2sfiles_unlink, simp)
+apply (simp add:is_file_simps current_files_simps)
+apply (auto simp add:tainted_eq_Tainted is_file_in_current split:if_splits option.splits
+  dest!:current_file_has_sfile')[1]
+
+apply (simp add:is_dir_simps, frule is_dir_in_current)
+apply (frule_tac f' = list in cf2sfile_unlink)
+apply (clarsimp simp:current_files_unlink split:option.splits)
+apply (drule file_dir_conflict, simp+)
+done
+
+lemma co2sobj_rmdir:
+  "\<lbrakk>valid (Rmdir p f # s); alive (Rmdir p f # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Rmdir p f # s) obj = 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 (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits
+           dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]
+apply (simp add:is_file_simps dir_is_empty_def)
+apply (case_tac "f = list", drule file_dir_conflict, simp, simp)
+apply (simp add:cf2sfiles_other)
+apply (auto simp:cf2sfile_simps dest:is_dir_in_current)
+done
+
+lemma co2sobj_mkdir:
+  "\<lbrakk>valid (Mkdir p f i # s); alive (Mkdir p f i # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Mkdir p f i # s) obj = (
+      if (obj = O_dir f) 
+      then (case (cf2sfile (Mkdir p f i # s) f) of 
+              Some sf \<Rightarrow> Some (S_dir sf)
+            | _       \<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 (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits
+           dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]
+apply (frule_tac cf2sfiles_other, simp+)
+apply (frule is_dir_in_current, rule impI, simp add:current_files_mkdir)
+apply (frule current_file_has_sfile, simp, erule exE, simp)
+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> 
+   \<Longrightarrow> co2sobj (LinkHard p oldf f # s) obj = (
+    case obj of
+      O_file f' \<Rightarrow> if (f' = f \<or> f' \<in> same_inode_files s oldf)
+                   then (case (cf2sfile (LinkHard p oldf f # s) f) of
+                           Some sf \<Rightarrow> Some (S_file (cf2sfiles s oldf \<union> {sf}) (O_file oldf \<in> Tainted s))
+                         | _       \<Rightarrow> None)
+                   else co2sobj s obj
+    | _         \<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 tainted_eq_Tainted)
+apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits
+           dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]
+apply (frule_tac cf2sfiles_linkhard, simp+)
+apply (frule_tac f' = f in cf2sfile_linkhard, simp add:current_files_linkhard)
+apply (auto simp:is_file_simps sectxt_of_obj_simps current_files_simps is_file_in_current same_inodes_Tainted
+  split:option.splits if_splits dest:Tainted_in_current 
+  dest!:current_has_sec' current_file_has_sfile')[1]
+
+apply (frule is_dir_in_current, simp add:current_files_linkhard is_dir_simps is_dir_in_current)
+apply (frule is_dir_in_current)
+apply (frule current_file_has_sfile, simp)
+apply (drule cf2sfile_linkhard1, simp+)
+done
+
+lemma co2sobj_truncate:
+  "\<lbrakk>valid (Truncate p f len # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Truncate p f len # s) obj = (
+      case obj of
+        O_file f' \<Rightarrow> if (f' \<in> same_inode_files s f \<and> len > 0)
+                     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> 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)
+
+(* should delete has_same_inode !?!?*)
+by (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits option.splits)
+
+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"
+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)
+done
+
+lemma co2sobj_exit:
+  "\<lbrakk>valid (Exit p # s); alive (Exit p # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Exit p # s) obj = 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)
+done
+
+lemma co2sobj_createmsgq:
+  "\<lbrakk>valid (CreateMsgq p q # s); alive (CreateMsgq p q # s) obj\<rbrakk> \<Longrightarrow> co2sobj (CreateMsgq p q # s) obj = (
+      case obj of
+        O_msgq q' \<Rightarrow> if (q' = q) then (case (cq2smsgq (CreateMsgq p q # s) q) of
+                                         Some sq \<Rightarrow> Some (S_msgq sq)
+                                       | _       \<Rightarrow> None)
+                     else co2sobj s obj
+      | _        \<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!:current_has_smsgq'
+             dest:is_file_in_current is_dir_in_current cq2smsg_createmsgq)
+done
+
+lemma co2sobj_sendmsg:
+  "\<lbrakk>valid (SendMsg p q m # s); alive (SendMsg p q m # s) obj\<rbrakk> \<Longrightarrow> co2sobj (SendMsg p q m # s) obj = (
+      case obj of
+        O_msgq q' \<Rightarrow> if (q' = q) then (case (cq2smsgq (SendMsg p q m # s) q) of
+                                         Some sq \<Rightarrow> Some (S_msgq sq)
+                                       | _       \<Rightarrow> None)
+                     else co2sobj s obj
+      | _        \<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!:current_has_smsgq'
+             dest:is_file_in_current is_dir_in_current cq2smsg_sendmsg)
+done
+
+lemma co2sobj_recvmsg:
+  "\<lbrakk>valid (RecvMsg p q m # s); alive (RecvMsg p q m # s) obj\<rbrakk> \<Longrightarrow> co2sobj (RecvMsg p q m # s) obj = (
+      case obj of
+        O_msgq q' \<Rightarrow> if (q' = q) then (case (cq2smsgq (RecvMsg p q m # s) q) of
+                                         Some sq \<Rightarrow> Some (S_msgq sq)
+                                       | _       \<Rightarrow> None)
+                     else co2sobj s obj
+      | O_proc p' \<Rightarrow> if (info_flow_shm s p p' \<and> O_msg q m \<in> Tainted s)
+                     then (case (cp2sproc s p') of
+                             Some sp \<Rightarrow> Some (S_proc sp True)
+                           | _       \<Rightarrow> None)
+                     else co2sobj s obj
+      | _         \<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!:current_has_smsgq'
+             dest:is_file_in_current is_dir_in_current cq2smsg_recvmsg)
+done
+
+lemma co2sobj_removemsgq:
+  "\<lbrakk>valid (RemoveMsgq p q # s); alive (RemoveMsgq p q # s) obj\<rbrakk> 
+   \<Longrightarrow> co2sobj (RemoveMsgq p q # s) obj = 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!:current_has_smsgq'
+             dest:is_file_in_current is_dir_in_current cq2smsg_removemsgq)
+done
+
+lemma co2sobj_createshm:
+  "\<lbrakk>valid (CreateShM p h # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (CreateShM p h # s) obj = 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 ch2sshm_simps
+             dest!:current_shm_has_sh'
+             dest:is_file_in_current is_dir_in_current)
+done
+
+lemma co2sobj_detach:
+  "\<lbrakk>valid (Detach p h # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Detach p h # s) obj = (
+      case obj of
+        O_proc p' \<Rightarrow> if (p' = p) then (case (cp2sproc (Detach p h # s) p) of
+                                         Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s))
+                                       | _       \<Rightarrow> None)
+                     else co2sobj s obj
+      | _         \<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 ch2sshm_simps
+             dest!:current_shm_has_sh'
+             dest:is_file_in_current is_dir_in_current)
+done
+
+lemma co2sobj_deleteshm:
+  "\<lbrakk>valid (DeleteShM p h # s); alive (DeleteShM p h # s) obj\<rbrakk> \<Longrightarrow> co2sobj (DeleteShM p h # s) obj = (
+      case obj of
+        O_proc p' \<Rightarrow> (case (cp2sproc (DeleteShM p h # s) p') of
+                        Some sp \<Rightarrow> Some (S_proc sp (O_proc p' \<in> Tainted s))
+                      | _       \<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 tainted_eq_Tainted
+                  same_inode_files_prop6 ch2sshm_simps
+             dest!:current_shm_has_sh' 
+             dest:is_file_in_current is_dir_in_current)
+done
+
+lemma co2sobj_attach:
+  "\<lbrakk>valid (Attach p h flag # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Attach p h flag # s) obj = (
+      case obj of
+        O_proc p' \<Rightarrow> if (p' = p)
+                     then (case (cp2sproc (Attach p h flag # s) p) of
+                             Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s \<or> 
+              (\<exists> p'. O_proc p' \<in> Tainted s \<and> (p', SHM_RDWR) \<in> procs_of_shm s h)))
+                           | _       \<Rightarrow> None)
+                     else if (\<exists> flag'. (p', flag') \<in> procs_of_shm s h)
+                          then (case (cp2sproc s p') of 
+                                  Some sp \<Rightarrow> Some (S_proc sp (O_proc p' \<in> Tainted s \<or>
+              (O_proc p \<in> Tainted s \<and> flag = SHM_RDWR)))
+                                | _       \<Rightarrow> None)
+                          else co2sobj s obj
+      | _         \<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 (rule conjI|rule impI|erule exE)+
+apply (simp split:option.splits)
+apply (rule impI, frule current_proc_has_sp, simp)
+apply ((erule exE)+, auto simp:cp2sproc_attach tainted_eq_Tainted)[1]
+apply (rule impI|rule conjI)+
+apply (subgoal_tac "p \<in> current_procs (Attach p h flag # s)")
+apply (drule_tac p = p in current_proc_has_sp, simp, erule exE)
+apply (auto simp:tainted_eq_Tainted)[1]
+apply (simp, rule impI)
+apply (subgoal_tac "nat \<in> current_procs (Attach p h flag # s)")
+apply (drule_tac p = nat in current_proc_has_sp, simp, erule exE)
+apply (drule_tac p = nat in current_proc_has_sp, simp, erule exE)
+apply (auto simp:cp2sproc_attach tainted_eq_Tainted)[1]
+apply simp
+
+apply (auto split:if_splits option.splits dest!:current_file_has_sfile' 
+             simp:current_files_simps cf2sfiles_simps cf2sfile_simps tainted_eq_Tainted
+                  same_inode_files_prop6 
+             dest:is_file_in_current is_dir_in_current)
+done
+
 
 lemma co2sobj_other:
   "\<lbrakk>valid (e # s); alive (e # s) obj; 
     \<forall> p f fds. e \<noteq> Execve p f fds;
     \<forall> p p' fds shms. e \<noteq> Clone p p' fds shms;
     \<forall> p p'. e \<noteq> Ptrace p p';
-    \<forall> 
+    \<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;
+    \<forall> p fd. e \<noteq> ReadFile p fd;
+    \<forall> p fd. e \<noteq> WriteFile p fd;
+    \<forall> p fd. e \<noteq> CloseFd p fd;
+    \<forall> p f. e \<noteq> UnLink p f;
+    \<forall> p f. e \<noteq> Rmdir p f;
+    \<forall> p f i. e \<noteq> Mkdir p f i;
+    \<forall> p f f'. e \<noteq> LinkHard p f f';
+    \<forall> p f len. e \<noteq> Truncate p f len;
+    \<forall> p q. e \<noteq> CreateMsgq p q;
+    \<forall> p q m. e \<noteq> SendMsg p q m;
+    \<forall> p q m. e \<noteq> RecvMsg p q m;
+    \<forall> p q. e \<noteq> RemoveMsgq p q;
+    \<forall> p h. e \<noteq> CreateShM p h;
+    \<forall> p h flag. e \<noteq> Attach p h flag;
+    \<forall> p h. e \<noteq> Detach p h;
+    \<forall> p h. e \<noteq> DeleteShM p h
    \<rbrakk> \<Longrightarrow> co2sobj (e # s) obj = co2sobj s obj"
+apply (frule vt_grant, case_tac e)
+apply (auto intro:co2sobj_kill co2sobj_exit)
+done
 
-lemmas co2sobj_simps = co2sobj_execve co2sobj_clone co2sobj_ptrace co2sobj_open
+lemmas co2sobj_simps = co2sobj_execve co2sobj_clone co2sobj_ptrace co2sobj_open co2sobj_readfile
+  co2sobj_writefile co2sobj_closefd co2sobj_unlink co2sobj_rmdir co2sobj_mkdir co2sobj_linkhard
+  co2sobj_truncate co2sobj_kill co2sobj_exit co2sobj_createmsgq co2sobj_sendmsg co2sobj_recvmsg
+  co2sobj_removemsgq co2sobj_attach co2sobj_detach co2sobj_createshm co2sobj_deleteshm
 
 (* simpset for s2ss*)
 
diff -r 9dfc8c72565a -r 13bba99ca090 Static.thy
--- a/Static.thy	Tue Sep 03 09:31:40 2013 +0800
+++ b/Static.thy	Wed Sep 04 09:07:39 2013 +0800
@@ -101,10 +101,10 @@
 | "init_obj2sobj (O_file f) = 
      Some (S_file (init_cf2sfiles f) 
                   (\<exists> f'. f' \<in> (init_same_inode_files f) \<and> O_file f \<in> seeds))"
-| "init_obj2sobj (O_dir f) =
+| "init_obj2sobj (O_dir f) = 
      (case (init_cf2sfile f) of
-        Some sf \<Rightarrow> Some (S_dir sf) 
-      | _ \<Rightarrow> None)"
+           Some sf \<Rightarrow> Some (S_dir sf) 
+         | _ \<Rightarrow> None)"
 | "init_obj2sobj (O_msgq q) = 
      (case (init_cq2smsgq q) of
        Some sq \<Rightarrow> Some (S_msgq sq)