--- a/Dynamic_static.thy	Tue Nov 19 12:31:56 2013 +0800
+++ b/Dynamic_static.thy	Wed Nov 20 13:43:09 2013 +0800
@@ -52,12 +52,12 @@
   "enrich_proc [] tp dp = []"
 | "enrich_proc (Execve p f fds # s) tp dp = (
      if (tp = p) 
-     then Execve dp f fds # Execve p f fds # (enrich_proc s tp dp)
+     then Execve dp f (fds \<inter> proc_file_fds s p) # Execve p f fds # (enrich_proc s tp dp)
      else Execve p f fds # (enrich_proc s tp dp))"
 | "enrich_proc (Clone p p' fds shms # s) tp dp = (
      if (tp = p') 
-     then Clone p dp fds shms # Clone p p' fds shms # s
-     else Clone p dp fds shms # (enrich_proc s tp dp))"
+     then Clone p dp (fds \<inter> proc_file_fds s p) shms # Clone p p' fds shms # s
+     else Clone p p' fds shms # (enrich_proc s tp dp))"
 | "enrich_proc (Open p f flags fd opt # s) tp dp = (
      if (tp = p)
      then Open dp f (remove_create_flag flags) fd opt # Open p f flags fd opt # (enrich_proc s tp dp)
@@ -86,9 +86,76 @@
 where
   "is_created_proc s p \<equiv> p \<in> init_procs \<longrightarrow> deleted (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"
+  and vd: "valid s" and f_in: "is_file s f"  and f_in': "is_file s' f"
+  and sec: "sectxt_of_obj s' (O_file f) = sectxt_of_obj s (O_file f)"
+  shows "search_check s' (up, rp, tp) f"
+proof (cases f)
+  case Nil
+  with f_in vd have "False" 
+    by (auto dest:root_is_dir') 
+  thus ?thesis by simp
+next
+  case (Cons n pf)
+  from vd f_in obtain sf where sf: "cf2sfile s f = Some sf"
+    apply (drule_tac is_file_in_current, drule_tac current_file_has_sfile, simp)
+    apply (erule exE, simp)
+    done
+  then obtain psfs where psfs: "get_parentfs_ctxts s pf = Some psfs" using Cons
+    by (auto simp:cf2sfile_def split:option.splits if_splits)
+  from sf cf2sf f_in have sf': "cf2sfile s' f = Some sf" by (auto dest:is_file_in_current)
+  then obtain psfs' where psfs': "get_parentfs_ctxts s' pf = Some psfs'"using Cons
+    by (auto simp:cf2sfile_def split:option.splits if_splits)
+  with sf sf' psfs have psfs_eq: "set psfs' = set psfs" using Cons f_in f_in'
+    apply (simp add:cf2sfile_def split:option.splits)
+    apply (case_tac sf, simp)
+    done
+  show ?thesis using grant f_in f_in' psfs psfs' psfs_eq sec
+    apply (simp add:Cons split:option.splits)
+    by (case_tac a, simp)
+qed
+
+lemma enrich_inherit_fds_check:
+  assumes grant: "inherit_fds_check s (up, nr, nt) p fds"  and vd: "valid s"
+  and fd2sfd: "\<forall> fd. fd \<in> current_procs s \<longrightarrow> cp2sproc s' p = cp2sproc s p"
+  and p_in: "p \<in> current_procs s" and p_in': "p \<in> current_procs s'"
+  and fd_in: "fds \<subseteq> current_proc_fds s p" and fd_in': "fds \<subseteq> current_proc_fds s' p"
+  shows "inherit_fds_check s' (up, nr, nt) p fds"
+proof-
+  have "\<And> fd. fd \<in> fds \<Longrightarrow> sectxt_of_obj s' (O_fd p fd) = sectxt_of_obj s (O_fd p fd)"
+  proof-
+    fix fd
+    assume fd_in_fds: "fd \<in> fds"
+    hence fd_in_cfds: "fd \<in> current_proc_fds s p" 
+      and fd_in_cfds': "fd \<in> current_proc_fds s' p" 
+      using fd_in fd_in' by auto
+    from p_in vd obtain sp where csp: "cp2sproc s p = Some sp" 
+      by (drule_tac current_proc_has_sp, simp, erule_tac exE, simp)
+    with cp2sp have "cpfd2sfds s p = cpfd2sfds s' p"
+      apply (erule_tac x = p in allE)
+      by (auto simp:cp2sproc_def split:option.splits simp:p_in)
+    hence "cfd2sfd s p fd = cfd2sfd s' p fd"
+      apply (simp add:cpfd2sfds_def)
+      thm inherit_fds_check_def
+      thm sectxts_of_fds_def
+      thm cpfd2sfds_def
+      apply (
+
+    show "sectxt_of_obj s' (O_fd p fd) = sectxt_of_obj s (O_fd p fd)"
+      sorry
+  qed
+  hence "sectxts_of_fds s' p fds = sectxts_of_fds s p fds"
+    by (simp add:sectxts_of_fds_def)
+  thus ?thesis using grant
+    by (simp add:inherit_fds_check_def)
+qed
+  
+
 lemma enrich_proc_aux1:
   assumes vs': "valid s'"
-    and os: "os_grant s e" and grant: "grant s e"
+    and os: "os_grant s e" and grant: "grant s e" and vd: "valid s"
     and alive: "\<forall> obj. alive s obj \<longrightarrow> alive s' obj"
     and cp2sp: "\<forall> p. p \<in> current_procs s \<longrightarrow> cp2sproc s' p = cp2sproc s p"
     and cf2sf: "\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile s' f = cf2sfile s f"
@@ -105,7 +172,7 @@
     apply (auto simp:Execve)
     by (erule_tac x = "O_fd p x" in allE, auto)
   have "os_grant s' e" using p_in f_in fd_in by (simp add:Execve)
-  moreover have "grant s' e"
+  moreover have "grant s' e" apply (simp add:Execve)
   proof-
     from grant obtain up rp tp uf rf tf 
       where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)"
@@ -117,17 +184,16 @@
       using os cp2sp
       apply (erule_tac x = p in allE)
       by (auto simp:Execve co2sobj.simps cp2sproc_def split:option.splits)
-    from p2 have p2': "sectxt_of_obj s' (O_file f) = Some (uf, rf, tf)" 
-      using os cf2sf
-      apply (erule_tac x = "f" in allE)
-      apply (auto simp:Execve dest:is_file_in_current)
-      thm cf2sfile_def
-      apply (auto simp:cf2sfile_def split:option.splits)
-      apply (auto simp:Execve co2sobj.simps cf2sfile_simps split:option.splits)
-      apply (simp add:cf2sfiles_def)
-      apply (auto)[1]
-      using os pre
-  show ?thesis
+    from os have f_in': "is_file s f" by (simp add:Execve)
+    from vd os have "\<exists> sf. cf2sfile s f = Some sf"
+      by (auto dest!:is_file_in_current current_file_has_sfile simp:Execve)
+    hence p2': "sectxt_of_obj s' (O_file f) = Some (uf, rf, tf)" using f_in f_in' p2 cf2sf
+      apply (erule_tac x = f in allE)
+      apply (auto dest:is_file_in_current simp:cf2sfile_def split:option.splits)
+      apply (case_tac f, simp)
+      apply (drule_tac s = s in root_is_dir', simp add:vd, simp+)
+      done
+  show ?
   proof-
     have
     
@@ -138,7 +204,10 @@
   "\<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> co2sobj (enrich_proc s p p') obj = co2sobj s obj)"
+       (\<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 {})))"
 proof (induct s)
   case Nil
   thus ?case by (auto simp:is_created_proc_def)

--- a/Flask.thy	Tue Nov 19 12:31:56 2013 +0800
+++ b/Flask.thy	Wed Nov 20 13:43:09 2013 +0800
@@ -692,7 +692,7 @@
      (\<exists> f. file_of_proc_fd \<tau> p fd = Some f \<and> f \<in> current_files \<tau>) \<and> 
      (\<exists> flags. flags_of_proc_fd \<tau> p fd = Some flags \<and> is_write_flag flags))"
 | "os_grant \<tau> (Execve p f fds)                = 
-    (p \<in> current_procs \<tau> \<and> is_file \<tau> f \<and> fds \<subseteq> current_proc_fds \<tau> p)" (* file_at_writing_by \<tau> f = {} *)
+    (p \<in> current_procs \<tau> \<and> is_file \<tau> f \<and> fds \<subseteq> proc_file_fds \<tau> p)" (* file_at_writing_by \<tau> f = {} \<and> fds \<subseteq> current_proc_fds \<tau> p *)
 (*
 | "os_grant \<tau> (Rename p f\<^isub>2 f\<^isub>3)                = 
     (p \<in> current_procs \<tau> \<and> f\<^isub>2 \<in> current_files \<tau> \<and> \<not>(f\<^isub>2 \<preceq> f\<^isub>3) \<and> f\<^isub>3 \<notin> current_files \<tau> \<and>
@@ -744,8 +744,8 @@
 | "os_grant \<tau> (ChangeOwner p u)               = (p \<in> current_procs \<tau> \<and> u \<in> current_users \<tau>)"
 *)
 | "os_grant \<tau> (Clone p p' fds shms)           = 
-    (p \<in> current_procs \<tau> \<and> p' \<notin> (current_procs \<tau>) \<and> fds \<subseteq> current_proc_fds \<tau> p \<and>
-     (\<forall> h \<in> shms. \<exists> flag. (p, flag) \<in> procs_of_shm \<tau> h))"
+    (p \<in> current_procs \<tau> \<and> p' \<notin> (current_procs \<tau>) \<and> fds \<subseteq> proc_file_fds \<tau> p \<and>
+     (\<forall> h \<in> shms. \<exists> flag. (p, flag) \<in> procs_of_shm \<tau> h))" (* current_proc_fds \<rightarrow> proc_file_fds *)
 | "os_grant \<tau> (Kill p\<^isub>1 p\<^isub>2)                    = 
     (p\<^isub>1 \<in> current_procs \<tau> \<and> p\<^isub>2 \<in> current_procs \<tau>)" (* a process can kill itself right? *)
 | "os_grant \<tau> (Exit p)                        =