--- a/no_shm_selinux/Co2sobj_prop.thy	Mon Dec 30 12:01:09 2013 +0800
+++ b/no_shm_selinux/Co2sobj_prop.thy	Mon Dec 30 14:04:23 2013 +0800
@@ -805,7 +805,7 @@
   "valid (Open p f flags fd opt # s)
    \<Longrightarrow> cfd2sfd (Open p f flags fd opt # s) p fd = 
      (case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of
-        (Some sec, Some sf) \<Rightarrow> Some (sec, flags, sf)
+        (Some sec, Some sf) \<Rightarrow> Some (sec, remove_create_flag flags, sf)
       | _ \<Rightarrow> None)"
 by (simp add:cfd2sfd_def sectxt_of_obj_simps split:if_splits)
 
@@ -854,7 +854,7 @@
   "\<lbrakk>valid (Open p f flags fd opt # s); file_of_proc_fd (Open p f flags fd opt # s) p' fd' = Some f'\<rbrakk>
    \<Longrightarrow> cfd2sfd (Open p f flags fd opt # s) p' fd' = (if (p' = p \<and> fd' = fd) then 
      (case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of
-        (Some sec, Some sf) \<Rightarrow> Some (sec, flags, sf)
+        (Some sec, Some sf) \<Rightarrow> Some (sec, remove_create_flag flags, sf)
       | _ \<Rightarrow> None)         else cfd2sfd s p' fd')"
 apply (simp split:if_splits)
 apply (simp add:cfd2sfd_open1 split:option.splits)
@@ -1003,7 +1003,7 @@
   "valid (Open p f flags fd opt # s) \<Longrightarrow>
    cpfd2sfds (Open p f flags fd opt # s) p = (
     case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of
-        (Some sec, Some sf) \<Rightarrow> (cpfd2sfds s p) \<union> {(sec, flags, sf)}
+        (Some sec, Some sf) \<Rightarrow> (cpfd2sfds s p) \<union> {(sec, remove_create_flag flags, sf)}
       | _ \<Rightarrow> cpfd2sfds s p)"
 apply (frule cfd2sfd_open1)
 apply (auto dest:cpfd2sfds_open1 split:option.splits)
@@ -1027,7 +1027,7 @@
   "valid (Open p f flags fd opt # s)
    \<Longrightarrow> cpfd2sfds (Open p f flags fd opt # s) = (cpfd2sfds s) (p := (
     case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of
-        (Some sec, Some sf) \<Rightarrow> (cpfd2sfds s p) \<union> {(sec, flags, sf)}
+        (Some sec, Some sf) \<Rightarrow> (cpfd2sfds s p) \<union> {(sec, remove_create_flag flags, sf)}
       | _ \<Rightarrow> cpfd2sfds s p))"
 apply (rule ext)
 apply (case_tac "x \<noteq> p")
@@ -1479,7 +1479,7 @@
            cf2sfile (Open p f flags fd opt # s) f) of 
        (Some sec, Some fdsec, Some sf) \<Rightarrow> Some (if (\<not> died (O_proc p) s \<and> p \<in> init_procs) 
                                                then Init p else Created, sec, 
-                                                (cpfd2sfds s p) \<union> {(fdsec, flags, sf)})
+                                                (cpfd2sfds s p) \<union> {(fdsec, remove_create_flag flags, sf)})
      | _        \<Rightarrow> None)" (*, cph2spshs s p 
 apply (frule cph2spshs_other, simp, simp, simp, simp, simp, simp, simp) *)
 apply (frule cpfd2sfds_open, frule vt_grant_os, frule vd_cons, rule ext)

--- a/no_shm_selinux/Enrich2.thy	Mon Dec 30 12:01:09 2013 +0800
+++ b/no_shm_selinux/Enrich2.thy	Mon Dec 30 14:04:23 2013 +0800
@@ -648,6 +648,29 @@
       apply (auto simp:is_created_proc_simps split:if_splits)
       done
   qed
+  have sf_cons:
+    "\<forall>f. f \<in> current_files (e # s) \<longrightarrow> cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f"
+  proof clarify
+    fix f 
+    assume a1: "f \<in> current_files (e # s)"
+    from pre have pre_sf: "\<And> f. \<lbrakk>f \<in> current_files s; is_created_proc s p\<rbrakk>
+      \<Longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f"
+      by auto
+    from a1 have a1': "f \<in> current_files (enrich_proc (e # s) p p')"
+      using vd_cons' nodel_cons
+      by (simp add:enrich_proc_cur_files)
+      
+    show "cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f"
+        apply (case_tac e)
+        using vd created_cons nodel_cons vd_enrich_cons vd_cons' a1 a1'
+        apply (auto intro!:pre_sf simp:cf2sfile_simps is_created_proc_simps 
+          split:if_splits dest:vd_cons)
+        thm cf2sfile_other
+        apply (simp_all)
+        done
+      
+    
+    sorry
   moreover have "\<forall>tp fd. fd \<in> proc_file_fds (e # s) tp \<longrightarrow> 
     cfd2sfd (enrich_proc (e # s) p p') tp fd = cfd2sfd (e # s) tp fd"
   proof clarify
@@ -673,6 +696,18 @@
       using a1' nodel_cons all_procs_cons a1' created_cons vd_cons'
       apply (frule_tac enrich_proc_filefd, simp_all)
       done
+    have sec_proc:
+      "\<And> tp. \<lbrakk>tp \<in> current_procs s; is_created_proc s p\<rbrakk> 
+       \<Longrightarrow> sectxt_of_obj (enrich_proc s p p') (O_proc tp) = sectxt_of_obj s (O_proc tp)"
+      using pre 
+      apply (clarsimp)
+      apply (erule_tac x = tp in allE, auto simp:cp2sproc_def split:option.splits)
+      done
+    have sec_proc':
+      "\<And> tp. \<lbrakk>tp \<in> current_procs s; is_created_proc s p; p = tp\<rbrakk> 
+       \<Longrightarrow> sectxt_of_obj (enrich_proc s tp p') (O_proc tp) = sectxt_of_obj s (O_proc tp)"
+      apply (drule_tac sec_proc, simp+)
+      done
     show "cfd2sfd (enrich_proc (e # s) p p') tp fd = cfd2sfd (e # s) tp fd"
     proof-
       have b1: "\<And> proc f' fds. e = Execve proc f' fds
@@ -701,9 +736,48 @@
         done 
       have b3: "\<And> proc f' flags fd' opt. e = Open proc f' flags fd' opt 
          \<Longrightarrow> cfd2sfd (enrich_proc (e # s) p p') tp fd = cfd2sfd (e # s) tp fd"
+        using a4 a1' vd_enrich_cons vd_cons' created_cons 
+        apply (simp split:if_splits del:file_of_proc_fd.simps) 
+        
+        apply (simp add:cfd2sfd_open sec_open is_created_proc_simps a2 del:file_of_proc_fd.simps)
+        apply (tactic {*my_clarify_tac 1*})
+        apply (drule vd_cons)
+        apply (simp add:cfd2sfd_open sec_open a3 a2 split:if_splits)
+        apply (case_tac "proc \<in> current_procs s")
+        apply (simp add:sec_proc')
+        apply (case_tac "sectxt_of_obj s (O_proc proc)", simp+)        
+        apply (case_tac "f \<in> current_files (e # s)")
+        apply (drule sf_cons[rule_format], simp)
+        using vd_enrich_cons
+        apply (simp add:cf2sfile_open_none)
+        using os
+        apply (simp add:current_files_simps is_file_in_current split:option.splits)
+        using os
+        apply (simp split:option.splits)
+        apply (rule impI)
+        apply (simp add:cfd2sfd_open sec_open a3 a2 split:if_splits)
+        apply (drule vd_cons)
+        apply (drule_tac p' = tp and fd' = fd and f' = f and s = "enrich_proc s proc p'" in cfd2sfd_open)
+        apply (simp, rule impI, simp)
+        apply (simp split:if_splits, rule conjI, rule impI, simp)
+        apply (drule pre_sfd', simp, simp)
+
+        apply (simp add:cfd2sfd_open sec_open is_created_proc_simps a2 del:file_of_proc_fd.simps)
+        apply (case_tac "proc \<in> current_procs s")
+        apply (simp add:sec_proc)
+        apply (case_tac "f' \<in> current_files (e # s)")
+        apply (drule sf_cons[rule_format], simp)
+        apply (simp split:option.splits)
+        apply (rule impI|rule conjI)+
+        apply (drule current_has_sec', simp add:vd, simp add:os)
+        apply (rule impI, rule impI)
         apply (simp split:if_splits)
-        thm cfd2sfd_open
-        sorry
+        apply (simp add:pre_sfd')
+        using os
+        apply (simp add:current_files_simps is_file_in_current split:option.splits)
+        using os
+        apply (simp split:option.splits)
+        done
       have b4: "\<And> proc fd'. e = ReadFile proc fd' 
          \<Longrightarrow> cfd2sfd (enrich_proc (e # s) p p') tp fd = cfd2sfd (e # s) tp fd"
         using a4 vd_enrich_cons a1' vd_cons' created_cons
@@ -727,8 +801,6 @@
   qed
   moreover have "\<forall>tp. tp \<in> current_procs (e # s) \<longrightarrow> cp2sproc (enrich_proc (e # s) p p') tp = cp2sproc (e # s) tp"
     sorry
-  moreover have "\<forall>f. f \<in> current_files (e # s) \<longrightarrow> cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f"
-    sorry
   moreover have "\<forall>q. q \<in> current_msgqs (e # s) \<longrightarrow> cq2smsgq (enrich_proc (e # s) p p') q = cq2smsgq (e # s) q"
     sorry
   moreover have "cp2sproc (enrich_proc (e # s) p p') p' = cp2sproc (e # s) p"

--- a/no_shm_selinux/OS_type_def.thy	Mon Dec 30 12:01:09 2013 +0800
+++ b/no_shm_selinux/OS_type_def.thy	Mon Dec 30 14:04:23 2013 +0800
@@ -230,7 +230,7 @@
 | Clone      "t_process" "t_process"  "t_fd set" (* "t_shm set" *) (* "t_clone_share_flag" is not needed, as event should record the fds and shms that passed to childprocess *)
 | Kill       "t_process" "t_process"
 | Ptrace     "t_process" "t_process"
-| Exit       "t_process"
+| Exit       "t_process" 
 
 | Open          "t_process" "t_file" "t_open_flags" "t_fd" "nat option"  (* the last nat option : if create file, the is Some inode_num else None *)
 | ReadFile      "t_process" "t_fd"                          

--- a/no_shm_selinux/Static.thy	Mon Dec 30 12:01:09 2013 +0800
+++ b/no_shm_selinux/Static.thy	Mon Dec 30 14:04:23 2013 +0800
@@ -36,12 +36,16 @@
 where
   "init_cf2sfiles f \<equiv> {sf. \<exists>f' \<in> init_same_inode_files f. init_cf2sfile f' = Some sf}"
 
+fun remove_create_flag :: "t_open_flags \<Rightarrow> t_open_flags"
+where
+  "remove_create_flag (mflag, oflags) = (mflag, oflags - {OF_CREAT})"
+
 definition init_cfd2sfd :: "t_process \<Rightarrow> t_fd \<Rightarrow> (security_context_t \<times> t_open_flags \<times> t_sfile) option"
 where
   "init_cfd2sfd p fd = 
      (case (init_file_of_proc_fd p fd, init_oflags_of_proc_fd p fd, init_sectxt_of_obj (O_fd p fd)) of
         (Some f, Some flags, Some sec) \<Rightarrow> (case (init_cf2sfile f) of 
-                                             Some sf \<Rightarrow> Some (sec, flags, sf)
+                                             Some sf \<Rightarrow> Some (sec, remove_create_flag flags, sf)
                                            | _ \<Rightarrow> None)
       | _ \<Rightarrow> None)"
 
@@ -151,7 +155,7 @@
   "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)
+                                          Some sf \<Rightarrow> Some (sec, remove_create_flag flags, sf)
                                         | _       \<Rightarrow> None)
     | _ \<Rightarrow> None)"
 
@@ -664,10 +668,6 @@
 where
   "brandnew_proc s \<equiv> next_nat (all_procs s)"
 
-fun remove_create_flag :: "t_open_flags \<Rightarrow> t_open_flags"
-where
-  "remove_create_flag (mflag, oflags) = (mflag, oflags - {OF_CREAT})"
-
 definition new_inode_num :: "t_state \<Rightarrow> nat"
 where
   "new_inode_num \<tau> = next_nat (current_inode_nums \<tau>)"