--- a/no_shm_selinux/Enrich2.thy	Mon Dec 23 19:47:17 2013 +0800
+++ b/no_shm_selinux/Enrich2.thy	Thu Dec 26 10:56:50 2013 +0800
@@ -1,6 +1,6 @@
 theory Enrich
 imports Main Flask Static Init_prop Valid_prop Tainted_prop Delete_prop Co2sobj_prop S2ss_prop S2ss_prop2
- Temp Enrich
+ Temp Enrich Proc_fd_of_file_prop
 begin
 
 context tainting_s begin
@@ -56,10 +56,10 @@
   thus ?case by (auto simp:is_created_proc_def)
 next
   case (Cons e s)
-  hence vd_cons: "valid (e # s)" and created_cons: "is_created_proc (e # s) p"
+  hence vd_cons': "valid (e # s)" and created_cons: "is_created_proc (e # s) p"
     and all_procs_cons: "p' \<notin> all_procs (e # s)" and vd: "valid s" 
     and os: "os_grant s e" and grant: "grant s e"
-    by (auto dest:vd_cons vt_grant_os vt_grant)
+    by (auto dest:vd_cons' vt_grant_os vt_grant)
   from all_procs_cons have all_procs: "p' \<notin> all_procs s" by (case_tac e, auto)
   from Cons have pre: "is_created_proc s p \<Longrightarrow> valid (enrich_proc s p p') \<and>
      (\<forall>obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj) \<and>
@@ -482,16 +482,66 @@
       qed
     qed
     ultimately show ?thesis 
-      using created_cons vd_cons all_procs_cons
+      using created_cons vd_cons' all_procs_cons
       apply (case_tac e)
       apply (auto simp:is_created_proc_simps split:if_splits)
       done
   qed
   moreover have "\<forall>obj. alive (e # s) obj \<longrightarrow> alive (enrich_proc (e # s) p p') obj"
+  proof clarify
+    fix obj
+    assume a0: "alive (e # s) obj"
+    have a1: "is_created_proc s p \<Longrightarrow> \<forall> obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj"
+      using pre by auto
+    show "alive (enrich_proc (e # s) p p') obj" (*
+    proof (cases e)
+      case (Execve tp f fds)
+      with created_cons a1
+      have b1: "\<forall> obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj" 
+        by (auto simp:is_created_proc_simps)
+      show ?thesis
+        using created_cons all_procs_cons vd_enrich_cons Execve b1 os a0
+        apply (simp add:alive_execve split:if_splits)
+        apply (frule_tac vd_cons) defer
+        apply (frule_tac vd_cons)
+        using vd_cons' Execve vd os
+        apply (auto simp:is_file_simps is_dir_simps is_created_proc_simps alive.simps
+          split:t_object.splits if_splits 
+          dest:set_mp file_fds_subset_pfds)
+        apply (erule_tac x = "O_proc nat" in allE, simp)
+        apply (erule_tac x = "O_file list" in allE, simp)
+        apply (drule set_mp, simp)
+        apply (drule_tac s = s and p = tp in file_fds_subset_pfds)
+        apply (erule_tac x = "O_fd tp nat2" in allE, simp)
+        apply (auto)[1]
+        apply (erule_tac x = "O_fd nat1 nat2" in allE, auto dest:set_mp file_fds_subset_pfds)[1]
+        apply (erule_tac x = "O_dir list" in allE, simp)
     sorry
+  show ?thesis *) sorry
   moreover have "\<forall>obj. enrich_not_alive (e # s) obj \<longrightarrow> enrich_not_alive (enrich_proc (e # s) p p') obj"
+    thm enrich_not_alive.simps
     sorry
   moreover have "files_hung_by_del (enrich_proc (e # s) p p') = files_hung_by_del (e # s)"
+  proof-
+    have "is_created_proc s p \<Longrightarrow> files_hung_by_del (enrich_proc s p p') = files_hung_by_del s"
+      and ffd_remain: "is_created_proc s p \<Longrightarrow> 
+      \<forall>tp fd f. file_of_proc_fd s tp fd = Some f \<longrightarrow> 
+                                   file_of_proc_fd (enrich_proc s p p') tp fd = Some f"
+      using pre by auto
+    with created_cons all_procs_cons os vd_cons' vd
+    show ?thesis
+      apply (frule_tac not_all_procs_prop3)
+      apply (case_tac e)
+      apply (auto simp:files_hung_by_del.simps is_created_proc_simps)
+      apply (auto simp:enrich_proc_dup_ffd_eq proc_file_fds_def procfd_of_file_eq_fpfd''
+        dest:procfd_of_file_imp_fpfd procfd_of_file_imp_fpfd' procfd_of_file_non_empty
+      )
+      apply (auto simp:enrich_proc_dup_ffd_eq proc_file_fds_def split:if_splits)[1]
+      
+      apply (auto simp:enrich_proc_dup_ffd_eq proc_file_fds_def files_hung_by_del.simps
+        split:option.splits)[1]
+      apply (auto split:option.splits)[1]
+      thm is_created_proc_simps
     sorry
   moreover have "\<forall>tp. tp \<in> current_procs (e # s) \<longrightarrow> cp2sproc (enrich_proc (e # s) p p') tp = cp2sproc (e # s) tp"
     sorry
@@ -524,10 +574,13 @@
       show "cp2sproc (enrich_proc (Execve tp f fds # s) p p') p' = cp2sproc (Execve tp f fds # s) p"
       proof (cases "tp = p")
         case True
-        show ?thesis using True a1 a2 a3 a4
+        show ?thesis using True a1 a2 a3 a4 b0
           thm not_all_procs_prop3
+          apply (frule_tac not_all_procs_prop2)
+          apply (frule not_all_procs_prop3)
           apply (auto simp add:cp2sproc_execve is_created_proc_def split:option.splits dest!:current_has_sec' 
-            dest:vt_grant_os not_all_procs_prop2 not_all_procs_prop3)
+            dest:vt_grant_os)
+          apply (auto simp:sectxt_of_obj_simps split:option.splits dest:valid.cases)
           
           sorry
       next
@@ -552,7 +605,7 @@
     show ?thesis using vd_enrich_cons
       apply (case_tac e)
       apply (simp_all only:b1 b2 b3 b4 b5 b6 b7)
-      using created_cons vd_enrich_cons vd_cons b0
+      using created_cons vd_enrich_cons vd_cons' b0
       apply (auto simp:cp2sproc_other is_created_proc_def)
       done
   qed