--- a/no_shm_selinux/Enrich.thy	Wed Dec 18 10:44:36 2013 +0800
+++ b/no_shm_selinux/Enrich.thy	Thu Dec 19 10:05:13 2013 +0800
@@ -44,17 +44,13 @@
      else Detach p h # (enrich_proc s tp dp))"
 *)
 | "enrich_proc (Kill p p' # s) tp dp = (
-     if (tp = p) then Kill p p' # s
+     if (tp = p') then Kill p p' # s
      else Kill p p' # (enrich_proc s tp dp))"
 | "enrich_proc (Exit p # s) tp dp = (
      if (tp = p) then Exit p # s
      else Exit p # (enrich_proc s tp dp))"
 | "enrich_proc (e # s) tp dp = e # (enrich_proc s tp dp)"
 
-definition is_created_proc:: "t_state \<Rightarrow> t_process \<Rightarrow> bool"
-where
-  "is_created_proc s p \<equiv> p \<in> init_procs \<longrightarrow> died (O_proc p) s"
-
 lemma enrich_search_check:
   assumes grant: "search_check s (up, rp, tp) f"
   and cf2sf: "\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile s' f = cf2sfile s f"
@@ -1044,55 +1040,212 @@
     by (simp add:Shutdown)
 qed  
   
-  
-  
-  
-  
-  
-  
-  
-    
+lemma not_all_procs_prop2:
+  "p' \<notin> all_procs s \<Longrightarrow> p' \<notin> init_procs"
+apply (induct s, simp)
+by (case_tac a, auto)
+
+lemma not_all_procs_prop3:
+  "p' \<notin> all_procs s \<Longrightarrow> p' \<notin> current_procs s"
+apply (induct s, simp)
+by (case_tac a, auto)
+
+definition is_created_proc:: "t_state \<Rightarrow> t_process \<Rightarrow> bool"
+where
+  "is_created_proc s p \<equiv> p \<in> current_procs s \<and> (p \<in> init_procs \<longrightarrow> died (O_proc p) s)"
+
+lemma created_proc_clone:
+  "valid (Clone p p' fds # s) \<Longrightarrow> 
+   is_created_proc (Clone p p' fds # s) tp = (if (tp = p') then True else is_created_proc s tp)"
+apply (drule vt_grant_os)
+apply (auto simp:is_created_proc_def dest:not_all_procs_prop2)
+using not_died_init_proc
+by auto
+
+lemma created_proc_exit: 
+  "is_created_proc (Exit p # s) tp = (if (tp = p) then False else is_created_proc s tp)"
+by (simp add:is_created_proc_def)
+
+lemma created_proc_kill:
+  "is_created_proc (Kill p p' # s) tp = (if (tp = p') then False else is_created_proc s tp)"
+by (simp add:is_created_proc_def)
+
+lemma created_proc_other:
+  "\<lbrakk>\<And> p p' fds. e \<noteq> Clone p p' fds;
+    \<And> p. e \<noteq> Exit p;
+    \<And> p p'. e \<noteq> Kill p p'\<rbrakk> \<Longrightarrow> is_created_proc (e # s) tp = is_created_proc s tp"
+by (case_tac e, auto simp:is_created_proc_def)
+
+lemmas is_created_proc_simps = created_proc_clone created_proc_exit created_proc_kill created_proc_other
+(*
 
 
 
 
-    
+       (p \<in> current_procs s \<longrightarrow> co2sobj (enrich_proc s p p') (O_proc p') = co2sobj (enrich_proc s p p') (O_proc p)) \<and>
+       (\<forall> obj. alive s obj \<longrightarrow> alive (enrich_proc s p p')  obj) \<and> 
+       (\<forall> p'. p' \<in> current_procs s \<longrightarrow> cp2sproc (enrich_proc s p p') p' = cp2sproc s p) \<and>
+       (\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f) \<and>
+       (Tainted (enrich_proc s p p') = (Tainted s \<union> (if (O_proc p \<in> Tainted s) then {O_proc p'} else {})))"*)
+
+lemma enrich_proc_dup_in:
+  "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk>
+   \<Longrightarrow> p' \<in> current_procs (enrich_proc s p p')"
+apply (induct s, simp add:is_created_proc_def)
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac a, auto simp:is_created_proc_def dest:not_all_procs_prop3)
+done
+
+lemma enrich_proc_dup_ffd:
+  "\<lbrakk>file_of_proc_fd s p fd = Some f; is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk>
+   \<Longrightarrow> file_of_proc_fd (enrich_proc s p p') p' fd = Some f"
+apply (induct s, simp add:is_created_proc_def)
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac a, auto simp:is_created_proc_def proc_file_fds_def
+  dest:not_all_procs_prop3 split:if_splits option.splits)
+done 
+
+lemma current_fflag_in_fds:
+  "\<lbrakk>flags_of_proc_fd s p fd = Some flag; valid s\<rbrakk> \<Longrightarrow> fd \<in> current_proc_fds s p"
+apply (induct s arbitrary:p)
+apply (simp add:flags_of_proc_fd.simps file_of_proc_fd.simps init_oflags_prop2) 
+apply (frule vd_cons, frule vt_grant_os, case_tac a)
+apply (auto split:if_splits option.splits dest:proc_fd_in_fds)
+apply (auto simp:proc_file_fds_def)
+sorry
+
+
+lemma current_fflag_has_ffd:
+  "\<lbrakk>flags_of_proc_fd s p fd = Some flag; valid s\<rbrakk> \<Longrightarrow> \<exists> f. file_of_proc_fd s p fd = Some f"
+apply (induct s arbitrary:p)
+apply (simp add: file_of_proc_fd.simps init_fileflag_valid) 
+apply (frule vd_cons, frule vt_grant_os, case_tac a)
+apply (auto split:if_splits option.splits dest:proc_fd_in_fds)
+apply (auto simp:proc_file_fds_def)
+sorry
+
+lemma enrich_proc_dup_fflags:
+  "\<lbrakk>flags_of_proc_fd s p fd = Some f; is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk>
+   \<Longrightarrow> flags_of_proc_fd (enrich_proc s p p') p' fd = Some f"
+apply (induct s, simp add:is_created_proc_def)
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac a, auto simp:is_created_proc_def proc_file_fds_def
+  dest:not_all_procs_prop3 split:if_splits option.splits)
+sorry
 
 lemma enrich_proc_prop:
   "\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s\<rbrakk>
    \<Longrightarrow> valid (enrich_proc s p p') \<and> 
-       (p \<in> current_procs s \<longrightarrow> co2sobj (enrich_proc s p p') (O_proc p') = co2sobj (enrich_proc s p p') (O_proc p)) \<and>
-       (\<forall> obj. alive s obj \<longrightarrow> alive (enrich_proc s p p')  obj) \<and> 
-       (\<forall> p'. p' \<in> current_procs s \<longrightarrow> cp2sproc (enrich_proc s p p') p' = cp2sproc s p) \<and>
-       (\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f) \<and>
-       (Tainted (enrich_proc s p p') = (Tainted s \<union> (if (O_proc p \<in> Tainted s) then {O_proc p'} else {})))"
+       (\<forall> obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj) \<and> 
+       (\<forall> obj. enrich_not_alive s obj \<longrightarrow> enrich_not_alive (enrich_proc s p p') obj) \<and>
+       (files_hung_by_del (enrich_proc s p p') = files_hung_by_del s) \<and> 
+       (\<forall> tp. tp \<in> current_procs s \<longrightarrow> cp2sproc (enrich_proc s p p') tp = cp2sproc s tp) \<and>
+       (\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f) \<and> 
+       (\<forall> q. q \<in> current_msgqs s \<longrightarrow> cq2smsgq (enrich_proc s p p') q = cq2smsgq s q) \<and> 
+       (\<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) \<and>
+       (\<forall> tp fd flags. flags_of_proc_fd s tp fd = Some flags \<longrightarrow> 
+                      flags_of_proc_fd (enrich_proc s p p') tp fd = Some flags) \<and>
+       (\<forall> q. msgs_of_queue (enrich_proc s p p') q = msgs_of_queue s q) \<and>
+       (\<forall> tp fd. fd \<in> proc_file_fds s tp \<longrightarrow> cfd2sfd (enrich_proc s p p') tp fd = cfd2sfd s tp fd) \<and>
+       (cp2sproc (enrich_proc s p p') p' = cp2sproc s p) \<and>
+       (\<forall> fd. fd \<in> proc_file_fds s p \<longrightarrow> cfd2sfd (enrich_proc s p p') p' fd = cfd2sfd s p fd)"
 proof (induct s)
   case Nil
   thus ?case by (auto simp:is_created_proc_def)
 next
   case (Cons e s)
-  hence p1: "\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s\<rbrakk>
-  \<Longrightarrow> valid (enrich_proc s p p') \<and>
-     (p \<in> current_procs s \<longrightarrow> co2sobj (enrich_proc s p p') (O_proc p') = co2sobj (enrich_proc s p p') (O_proc p)) \<and>
-     (alive s obj \<longrightarrow> alive (enrich_proc s p p') obj \<and> co2sobj (enrich_proc s p p') obj = co2sobj s obj)"
-    and p2: "valid (e # s)" and p3: "is_created_proc (e # s) p" and p4: "p' \<notin> all_procs (e # s)"
+  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)
+  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>
+     (\<forall>obj. enrich_not_alive s obj \<longrightarrow> enrich_not_alive (enrich_proc s p p') obj) \<and>
+     files_hung_by_del (enrich_proc s p p') = files_hung_by_del s \<and>
+     (\<forall>tp. tp \<in> current_procs s \<longrightarrow> cp2sproc (enrich_proc s p p') tp = cp2sproc s tp) \<and>
+     (\<forall>f. f \<in> current_files s \<longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f) \<and>
+     (\<forall>q. q \<in> current_msgqs s \<longrightarrow> cq2smsgq (enrich_proc s p p') q = cq2smsgq s q) \<and>
+     (\<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) \<and>
+     (\<forall>tp fd flags.
+         flags_of_proc_fd s tp fd = Some flags \<longrightarrow> flags_of_proc_fd (enrich_proc s p p') tp fd = Some flags) \<and>
+     (\<forall>q. msgs_of_queue (enrich_proc s p p') q = msgs_of_queue s q) \<and>
+     (\<forall>tp fd. fd \<in> proc_file_fds s tp \<longrightarrow> cfd2sfd (enrich_proc s p p') tp fd = cfd2sfd s tp fd)"
+    using vd all_procs by auto
+  have "valid (enrich_proc (e # s) p p')"
+  proof-
+    from pre have pre': "is_created_proc s p \<Longrightarrow> valid (enrich_proc s p p')" by simp
+    have "is_created_proc s p \<Longrightarrow> valid (e # enrich_proc s p p')" 
+      apply (frule pre')
+      apply (erule_tac s = s in enrich_valid_intro_cons)
+      apply (simp_all add:os grant vd pre)
+      done  
+    moreover have "\<And>f fds. \<lbrakk>valid (Execve p f fds # enrich_proc s p p'); is_created_proc s p\<rbrakk>
+      \<Longrightarrow> valid (Execve p' f (fds \<inter> proc_file_fds s p) # Execve p f fds # enrich_proc s p p')"
+      apply (frule vt_grant_os, frule vt_grant)
+      apply (rule valid.intros(2))
+      apply (simp_all split:option.splits add:sectxt_of_obj_simps is_file_simps)
+      apply (auto simp add:proc_file_fds_def)[1]
+      
+      sorry
+    moreover have "\<And>tp fds. \<lbrakk>valid (Clone tp p fds # s); p' \<noteq> p; p' \<notin> all_procs s\<rbrakk> \<Longrightarrow> 
+      valid (Clone tp p' (fds \<inter> proc_file_fds s tp) # Clone tp p fds # s)"
+      apply (frule vt_grant_os, frule vt_grant, drule not_all_procs_prop3)
+      apply (rule valid.intros(2))
+      apply (simp_all split:option.splits add:sectxt_of_obj_simps)
+      apply (auto simp add:proc_file_fds_def)[1]
+      apply (auto simp:inherit_fds_check_def sectxt_of_obj_simps sectxts_of_fds_def inherit_fds_check_ctxt_def)
+      done
+    moreover have "\<And>f flags fd inum.
+       \<lbrakk>valid (Open p f flags fd inum # enrich_proc s p p'); is_created_proc s p\<rbrakk>
+       \<Longrightarrow> valid (Open p' f (remove_create_flag flags) fd inum # Open p f flags fd inum # enrich_proc s p p')"
+      sorry
+    moreover have "\<And>fd. \<lbrakk>valid (CloseFd p fd # enrich_proc s p p'); is_created_proc s p\<rbrakk>
+           \<Longrightarrow> valid (CloseFd p' fd # CloseFd p fd # enrich_proc s p p')"
+      sorry 
+        thus ?thesis using created_cons vd_cons all_procs_cons
+      apply (case_tac e)
+      apply (auto simp:is_created_proc_simps split:if_splits)
+        
+    ultimately show ?thesis 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"
+    sorry
+  moreover have "\<forall>obj. enrich_not_alive (e # s) obj \<longrightarrow> enrich_not_alive (enrich_proc (e # s) p p') obj"
+    sorry
+  moreover have "files_hung_by_del (enrich_proc (e # s) p p') = files_hung_by_del (e # s)"
+    sorry
+  moreover have "\<forall>p. p \<in> current_procs (e # s) \<longrightarrow> cp2sproc (enrich_proc (e # s) p p') p = cp2sproc (e # s) p"
+    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 "\<forall>p fd f. file_of_proc_fd (e # s) p fd = Some f \<longrightarrow> 
+    file_of_proc_fd (enrich_proc (e # s) p p') p fd = Some f"
+    sorry
+  moreover have "\<forall>p fd flags. flags_of_proc_fd (e # s) p fd = Some flags \<longrightarrow>
+        flags_of_proc_fd (enrich_proc (e # s) p p') p fd = Some flags"
+    sorry
+  moreover have "\<forall>q. msgs_of_queue (enrich_proc (e # s) p p') q = msgs_of_queue (e # s) q"
+    sorry
+  moreover have "\<forall>p fd. fd \<in> proc_file_fds (e # s) p \<longrightarrow> 
+    cfd2sfd (enrich_proc (e # s) p p') p fd = cfd2sfd (e # s) p fd"
+    sorry
+  ultimately show ?case
     by auto
-  from p2 have vd: "valid s" and os: "os_grant s e" and grant: "grant s e"
-    by (auto dest:vd_cons vt_grant vt_grant_os)
-  from p4 have p4': "p' \<notin> all_procs s" by (case_tac e, auto)
-  from p1 p4' have a1: "is_created_proc s p \<Longrightarrow> valid (enrich_proc s p p')" by (auto simp:vd)
-  have c1: "valid (enrich_proc (e # s) p p')"
-    apply (case_tac e)
-    using a1 os p3
-    apply (auto simp:is_created_proc_def)
-    sorry
-  moreover have c2: "p' \<in> current_procs (enrich_proc (e # s) p p')"
-    sorry
-  moreover have c3: "co2sobj (enrich_proc (e # s) p p') (O_proc p') = co2sobj (enrich_proc (e # s) p p') (O_proc p)"
-    sorry
-  moreover have c4: "alive (e # s) obj \<longrightarrow>
-     alive (enrich_proc (e # s) p p') obj \<and> co2sobj (enrich_proc (e # s) p p') obj = co2sobj (e # s) obj"
-    sorry
-  ultimately show ?case by auto
 qed
+  
 
+lemma enrich_proc_valid:
+  "\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s\<rbrakk> \<Longrightarrow> valid (enrich_proc s p p')"
+by (auto dest:enrich_proc_prop)
+
+lemma enrich_proc_valid:
+  "\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s\<rbrakk> \<Longrightarrow> "
+
+
+    
\ No newline at end of file

--- a/no_shm_selinux/Flask.thy	Wed Dec 18 10:44:36 2013 +0800
+++ b/no_shm_selinux/Flask.thy	Thu Dec 19 10:05:13 2013 +0800
@@ -550,9 +550,13 @@
 | "flags_of_proc_fd (Accept p fd addr lport' fd' ino # \<tau>) p' fd'' = 
      (if (p = p' \<and> fd' = fd'') then None else flags_of_proc_fd \<tau> p' fd'')"
 | "flags_of_proc_fd (Clone p p' fds # \<tau>) p'' fd = 
-     (if (p' = p'' \<and> fd \<in> fds) then flags_of_proc_fd \<tau> p fd else flags_of_proc_fd \<tau> p'' fd)"  
+     (if (p' = p'' \<and> fd \<in> fds) then flags_of_proc_fd \<tau> p fd 
+      else if (p' = p'') then None
+      else flags_of_proc_fd \<tau> p'' fd)"  
 | "flags_of_proc_fd (Execve p f fds # \<tau>) p' fd = 
-     (if (p' = p \<and> fd \<in> fds) then flags_of_proc_fd \<tau> p fd else flags_of_proc_fd \<tau> p' fd)"
+     (if (p' = p \<and> fd \<in> fds) then flags_of_proc_fd \<tau> p fd 
+      else if (p' = p) then None
+      else flags_of_proc_fd \<tau> p' fd)"
 | "flags_of_proc_fd (Kill p\<^isub>1 p\<^isub>2 # \<tau>) p fd = 
      (if (p = p\<^isub>2) then None else flags_of_proc_fd \<tau> p fd)"
 | "flags_of_proc_fd (Exit p # \<tau>) p' fd' =