# HG changeset patch
# User chunhan
# Date 1384824445 -28800
# Node ID 5f86fb3ddd446c868d5a59f5aacfd30b7d9de769
# Parent  6f9a588bcfc4758e86c5763029467a25e09db6ee
enrich_proc

diff -r 6f9a588bcfc4 -r 5f86fb3ddd44 Dynamic_static.thy
--- a/Dynamic_static.thy	Wed Oct 30 08:18:40 2013 +0800
+++ b/Dynamic_static.thy	Tue Nov 19 09:27:25 2013 +0800
@@ -5,43 +5,565 @@
 
 context tainting_s begin
 
+fun remove_create_flag :: "t_open_flags \<Rightarrow> t_open_flags"
+where
+  "remove_create_flag (mflag, oflags) = (mflag, oflags - {OF_CREAT})"
 
+fun all_procs :: "t_state \<Rightarrow> t_process set"
+where
+  "all_procs [] = init_procs"
+| "all_procs (Clone p p' fds shms # s) = insert p' (all_procs s)"
+| "all_procs (e # s) = all_procs s"
+
+definition brandnew_proc :: "t_state \<Rightarrow> t_process"
+where
+  "brandnew_proc s \<equiv> next_nat (all_procs s)"
+
+(*
+definition brandnew_proc :: "t_state \<Rightarrow> t_process"
+where
+  "brandnew_proc s \<equiv> next_nat ({p | p s'. p \<in> current_procs s' \<and> s' \<preceq> s})"
+ another approach:
+  brandnew_proc = next_nat (all_procs s),
+    where all_procs is a event-trace listener *)
+
+(*
+lemma brandnew_proc_prop1:
+  "\<lbrakk>s' \<preceq> s; valid s\<rbrakk> \<Longrightarrow> brandnew_proc s \<notin> current_procs s'"
+apply (frule vd_preceq, simp)
+apply (simp add:brandnew_proc_def)
+apply (auto)
+sorry
+
+lemma brandnew_proc_prop2:
+  "\<lbrakk>p \<in> current_procs s'; s' \<preceq> s; valid s\<rbrakk> \<Longrightarrow> brandnew_proc s \<noteq> p"
+by (auto dest:brandnew_proc_prop1)
+
+lemma brandnew_proc_prop3:
+  "\<lbrakk>p \<in> current_procs s; valid (e # s)\<rbrakk> \<Longrightarrow> brandnew_proc (e # s) \<noteq> p"
+apply (rule brandnew_proc_prop2, simp)
+apply (rule no_juniorI, simp+)
+done
+*)
+
+(* enrich s target_proc duplicated_pro *)
+fun enrich_proc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> t_state"
+where 
+  "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)
+     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))"
+| "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)
+     else Open p f flags fd opt # (enrich_proc s tp dp))"
+| "enrich_proc (CloseFd p fd # s) tp dp = (
+     if (tp = p)
+     then CloseFd dp fd # CloseFd p fd # (enrich_proc s tp dp)
+     else CloseFd p fd # (enrich_proc s tp dp))"
+| "enrich_proc (Attach p h flag # s) tp dp = (
+     if (tp = p)
+     then Attach dp h flag # Attach p h flag # (enrich_proc s tp dp)
+     else Attach p h flag # (enrich_proc s tp dp))"
+| "enrich_proc (Detach p h # s) tp dp = (
+     if (tp = p) 
+     then Detach dp h # Detach p h # (enrich_proc s tp dp)
+     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
+     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> deleted (O_proc p) s"
+
+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> 
+       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)"
+proof (induct s)
+  case Nil
+  thus ?case by (auto simp:is_created_proc_def)
+next
+  case (Cons e s)
+  hence p1: "\<lbrakk>p \<in> current_procs s; valid s; is_created_proc s p; p' \<notin> current_procs s\<rbrakk>
+  \<Longrightarrow> valid (enrich_proc s p p') \<and>
+     p' \<in> current_procs (enrich_proc s p p') \<and>
+     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: "p \<in> current_procs (e # s)" and p3: "valid (e # s)"
+    and p4: "is_created_proc (e # s) p" and p5: "p' \<notin> current_procs (e # s)"
+    by auto
+  from p4 p2 have p4': "is_created_proc s p"
+    by (case_tac e, auto simp:is_created_proc_def)
+  from p3 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 p1 p4' have a1: "\<lbrakk>p \<in> current_procs s; p' \<notin> current_procs s\<rbrakk>
+    \<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 p5
+    apply (auto)
+    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
 
 
 
-definition enrich:: "t_state \<Rightarrow> t_object set \<Rightarrow> t_state \<Rightarrow> bool"
-where
-  "enrich s objs s' \<equiv> \<forall> obj \<in> objs. \<exists> obj'. obj' \<notin> objs \<and> alive s' obj \<and> co2sobj s' obj' = co2sobj s' obj"
+lemma "alive s obj \<Longrightarrow> alive (enrich_proc s p p') obj"
+apply (induct s, simp)
+apply (case_tac a, case_tac[!] obj)
+apply (auto simp:is_file_def is_dir_def split:option.splits t_inode_tag.splits)
+thm is_file_other
 
-definition reserve:: "t_state \<Rightarrow> t_object set \<Rightarrow> t_state \<Rightarrow> bool"
+lemma enrich_proc_valid:
+  "\<lbrakk>p \<in> current_procs s; valid s; p \<in> init_procs \<longrightarrow> deleted (O_proc p) s; p' \<notin> current_procs s\<rbrakk> \<Longrightarrow> valid (enrich_proc s p p')"
+apply (induct s, simp)
+apply (frule vd_cons, frule vt_grant, frule vt_grant_os, case_tac a)
+apply (auto intro!:valid.intros(2))
+prefer 28
+       
+
+
+end
+
+(* for any created obj, we can enrich trace with events that create new objs with the same static-properties *)
+definition enriched:: "t_state \<Rightarrow> t_object set \<Rightarrow> t_state \<Rightarrow> bool"
 where
-  "reserve s objs s' \<equiv> \<forall> obj. alive s obj \<longrightarrow> alive s' obj \<and> co2sobj s' obj = co2sobj s obj"
+  "enriched s objs s' \<equiv> \<forall> obj \<in> objs. \<exists> obj'. \<not> alive s obj' \<and> obj' \<notin> objs \<and>
+                                                alive s' obj' \<and> co2sobj s' obj' = co2sobj s' obj"
+
+definition reserved:: "t_state \<Rightarrow> t_object set \<Rightarrow> t_state \<Rightarrow> bool"
+where
+  "reserved s objs s' \<equiv> \<forall> obj. alive s obj \<longrightarrow> alive s' obj \<and> co2sobj s' obj = co2sobj s obj"
 
 definition enrichable :: "t_state \<Rightarrow> t_object set \<Rightarrow> bool"
 where
-  "enrichable s objs \<equiv> \<exists> s'. valid s' \<and> s2ss s' = s2ss s \<and> enrich s objs s' \<and> reserve s objs s'"
+  "enrichable s objs \<equiv> \<exists> s'. valid s' \<and> s2ss s' = s2ss s \<and> enriched s objs s' \<and> reserved s objs s'"
 
-definition is_created :: "t_state \<Rightarrow> t_object \<Rightarrow> bool"
+fun is_created :: "t_state \<Rightarrow> t_object \<Rightarrow> bool"
 where
-  "is_created s obj \<equiv> init_alive obj \<longrightarrow> deleted obj s"
+  "is_created s (O_file f) = (\<forall> f' \<in> same_inode_files s f. init_alive (O_file f') \<longrightarrow> deleted (O_file f') s)"
+| "is_created s obj        = (init_alive obj \<longrightarrow> deleted obj s)"
 
 definition is_inited :: "t_state \<Rightarrow> t_object \<Rightarrow> bool"
 where
   "is_inited s obj \<equiv> init_alive obj \<and> \<not> deleted obj s"
 
+(*
 lemma is_inited_eq_not_created:
   "is_inited s obj = (\<not> is_created s obj)"
 by (auto simp:is_created_def is_inited_def)
+*)
 
+lemma many_sq_imp_sms:
+  "\<lbrakk>S_msgq (Create, sec, sms) \<in> ss; ss \<in> static\<rbrakk> \<Longrightarrow> \<forall> sm \<in> (set sms). is_many_smsg sm"
+sorry
+
+(* recorded in our static world *)
+fun recorded :: "t_object \<Rightarrow> bool"
+where
+  "recorded (O_proc p)     = True"
+| "recorded (O_file f)     = True"
+| "recorded (O_dir  f)     = True"
+| "recorded (O_node n)     = False" (* cause socket is temperary not considered *)
+| "recorded (O_shm  h)     = True"
+| "recorded (O_msgq q)     = True"
+| "recorded _              = False"
+
+lemma cf2sfile_fi_init_file:
+  "\<lbrakk>cf2sfile s f = Some (Init f', sec, psec, asecs); is_file s f; valid s\<rbrakk> 
+   \<Longrightarrow> is_init_file f \<and> \<not> deleted (O_file f) s"
+apply (simp add:cf2sfile_def sroot_def split:option.splits if_splits)
+apply (case_tac f, simp, drule root_is_dir', simp+)
+done
+
+lemma root_not_deleted:
+  "valid s \<Longrightarrow> \<not> deleted (O_dir []) s"
+apply (induct s, simp)
+apply (frule vd_cons, frule vt_grant_os, case_tac a)
+by auto
+
+lemma cf2sfile_fi_init_dir:
+  "\<lbrakk>cf2sfile s f = Some (Init f', sec, psec, asecs); is_dir s f; valid s\<rbrakk> 
+   \<Longrightarrow> is_init_dir f \<and> \<not> deleted (O_dir f) s"
+apply (simp add:cf2sfile_def sroot_def split:option.splits if_splits)
+apply (case_tac f, simp add:root_is_init_dir root_not_deleted, simp)
+apply (drule file_dir_conflict, simp+)
+done
+
+lemma is_created_imp_many: 
+  "\<lbrakk>is_created s obj; co2sobj s obj = Some sobj; alive s obj; valid s\<rbrakk> \<Longrightarrow> is_many sobj"
+apply (case_tac obj, auto simp:co2sobj.simps split:option.splits)
+apply (case_tac [!] a)
+apply (auto simp:cp2sproc_def ch2sshm_def cq2smsgq_def cf2sfiles_def same_inode_files_def
+  split:option.splits if_splits)
+apply (frule cf2sfile_fi_init_file, simp add:is_file_def, simp)
+apply (erule_tac x = f' in allE, simp)
+apply (frule cf2sfile_fi_init_dir, simp+)+
+done
+
+lemma anotherp_imp_manysp: 
+  "\<lbrakk>cp2sproc s p = Some sp; co2sobj s (O_proc p') = co2sobj s (O_proc p); p' \<noteq> p;
+    p' \<in> current_procs s; p \<in> current_procs s\<rbrakk> 
+   \<Longrightarrow> is_many_sproc sp"
+by (case_tac sp, auto simp:cp2sproc_def co2sobj.simps split:option.splits if_splits)
+
+lemma is_file_has_sfs:
+  "\<lbrakk>is_file s f; valid s; cf2sfile s f = Some sf\<rbrakk> 
+   \<Longrightarrow> \<exists> sfs. co2sobj s (O_file f) = Some (S_file sfs (O_file f \<in> Tainted s)) \<and> sf \<in> sfs"
+apply (rule_tac x = "{sf' | f' sf'. cf2sfile s f' = Some sf' \<and> f' \<in> same_inode_files s f}" in exI)
+apply (auto simp:co2sobj.simps cf2sfiles_def tainted_eq_Tainted)
+apply (rule_tac x = f in exI, simp add:same_inode_files_prop9)
+done
+
+declare Product_Type.split_paired_Ex Product_Type.split_paired_All [simp del]
+
+lemma current_proc_in_s2ss:
+  "\<lbrakk>cp2sproc s p = Some sp; p \<in> current_procs s; valid s\<rbrakk>
+   \<Longrightarrow> S_proc sp (O_proc p \<in> Tainted s) \<in> s2ss s"
+apply (simp add:s2ss_def, rule_tac x = "O_proc p" in exI)
+apply (auto simp:co2sobj.simps tainted_eq_Tainted)
+done
+
+lemma current_file_in_s2ss:
+  "\<lbrakk>co2sobj s (O_file f) = Some (S_file sfs tagf); is_file s f; valid s\<rbrakk>
+   \<Longrightarrow> S_file sfs tagf \<in> s2ss s"
+by (simp add:s2ss_def, rule_tac x = "O_file f" in exI, simp)
+
+declare npctxt_execve.simps grant_execve.simps search_check.simps [simp del]
+
+
+lemma npctxt_execve_eq_sec:
+  "\<lbrakk>sectxt_of_obj (Execve p f fds # s) (O_proc p) = Some sec'; sectxt_of_obj s (O_proc p) = Some sec;
+    sectxt_of_obj s (O_file f) = Some fsec; valid (Execve p f fds # s)\<rbrakk>
+   \<Longrightarrow> npctxt_execve sec fsec = Some sec'"
+by (case_tac sec, case_tac fsec, auto simp:npctxt_execve.simps sectxt_of_obj_simps split:option.splits)
+
+lemma npctxt_execve_eq_cp2sproc:
+  "\<lbrakk>cp2sproc (Execve p f fds # s) p = Some (pi', sec', sfds', shms'); valid (Execve p f fds # s);
+    cp2sproc s p = Some (pi, sec, sfds, shms); cf2sfile s f = Some (fi, fsec, psec, asecs)\<rbrakk>
+   \<Longrightarrow> npctxt_execve sec fsec = Some sec'"
+apply (frule vt_grant_os, frule vd_cons)
+apply (rule npctxt_execve_eq_sec, auto simp:cp2sproc_def cf2sfile_def split:option.splits)
+apply (case_tac f, auto dest:root_is_dir')
+done
+
+lemma seach_check_eq_static:
+  "\<lbrakk>cf2sfile s f = Some sf; valid s; is_dir s f \<or> is_file s f\<rbrakk>
+   \<Longrightarrow> search_check_s sec sf (is_file s f) = search_check s sec f"
+apply (case_tac sf)
+apply (induct f)
+apply (auto simp:search_check_s_def search_check.simps cf2sfile_def sroot_def 
+                 root_sec_remains init_sectxt_prop sec_of_root_valid
+           dest!:root_is_dir' current_has_sec' split:option.splits)
+apply (simp add:search_check_allp_def)
+done
+
+lemma grant_execve_intro_execve:
+  "\<lbrakk>cp2sproc (Execve p f fds # s) p = Some (pi', sec', sfds', shms'); valid (Execve p f fds # s);
+     cp2sproc s p = Some (pi, sec, sfds, shms); cf2sfile s f = Some (fi, fsec, psec, asecs)\<rbrakk>
+    \<Longrightarrow> grant_execve sec fsec sec'"
+apply (frule vt_grant_os, frule vd_cons, frule vt_grant)
+apply (auto split:option.splits dest!:current_has_sec' simp del:grant_execve.simps simp add:cp2sproc_execve)
+apply (erule_tac x = aba in allE, erule_tac x = aca in allE, erule_tac x = bb in allE)
+apply (auto simp del:grant_execve.simps simp add:cp2sproc_def cf2sfile_def split:option.splits)
+apply (case_tac f, simp, drule root_is_dir', simp, simp, simp)
+apply (simp add:sectxt_of_obj_simps)
+done
+
+lemma search_check_intro_execve:
+  "\<lbrakk>cp2sproc s p = Some (pi, sec, sfds, shms); valid (Execve p f fds # s)\<rbrakk>
+   \<Longrightarrow> search_check s sec f"
+apply (frule vt_grant_os, frule vd_cons, frule vt_grant)
+apply (auto split:option.splits dest!:current_has_sec' simp del:grant_execve.simps simp add:cp2sproc_execve)
+apply (erule_tac x = aaa in allE, erule_tac x = ab in allE, erule_tac x = ba in allE)
+apply (auto simp add:cp2sproc_def cf2sfile_def split:option.splits)
+done
+
+lemma inherit_fds_check_intro_execve:
+  "\<lbrakk>cp2sproc (Execve p f fds # s) p = Some (pi', sec', sfds', shms'); valid (Execve p f fds # s)\<rbrakk>
+    \<Longrightarrow> inherit_fds_check s sec' p fds"
+apply (frule vt_grant_os, frule vd_cons, frule vt_grant)
+apply (auto split:option.splits dest!:current_has_sec' simp add:cp2sproc_execve)
+apply (erule_tac x = aba in allE, erule_tac x = aca in allE, erule_tac x = bb in allE)
+apply (auto simp add:cp2sproc_def cf2sfile_def split:option.splits)
+apply (simp add:sectxt_of_obj_simps)
+done
+
+lemma execve_sfds_subset: 
+  "\<lbrakk>cp2sproc (Execve p f fds # s) p = Some (pi', sec', sfds', shms'); valid (Execve p f fds # s);
+    cp2sproc s p = Some (pi, sec, sfds, shms)\<rbrakk>
+   \<Longrightarrow> sfds' \<subseteq> sfds"
+apply (frule vt_grant_os)
+apply (auto simp:cp2sproc_def cpfd2sfds_execve split:option.splits dest!:current_has_sec')
+apply (simp add:cpfd2sfds_def)
+apply (rule_tac x = fd in bexI, auto simp:proc_file_fds_def)
+done
+
+lemma inherit_fds_check_imp_static:
+  "\<lbrakk>cp2sproc (Execve p f fds # s) p = Some (pi', sec', sfds', shms');
+    inherit_fds_check s sec' p fds; valid (Execve p f fds # s)\<rbrakk>
+   \<Longrightarrow> inherit_fds_check_s sec' sfds'"
+apply (frule vt_grant_os, frule vd_cons, frule vt_grant)
+apply (auto simp:cp2sproc_def cpfd2sfds_execve inherit_fds_check_def inherit_fds_check_s_def split:option.splits)
+apply (erule_tac x = "(ad, ae, bc)" in ballE, auto simp:sectxts_of_sfds_def sectxts_of_fds_def)
+apply (erule_tac x = fd in ballE, auto simp:cfd2sfd_def split:option.splits)
+done
+
+lemma d2s_main_execve_grant_aux:
+  "\<lbrakk>cp2sproc (Execve p f fds # s) p = Some (pi', sec', sfds', shms'); valid (Execve p f fds # s);
+    cp2sproc s p = Some (pi, sec, sfds, shms); cf2sfile s f = Some (fi, fsec, psec, asecs)\<rbrakk>
+   \<Longrightarrow> (npctxt_execve sec fsec = Some sec') \<and> grant_execve sec fsec sec' \<and> 
+       search_check_s sec (fi, fsec, psec, asecs) (is_file s f) \<and> 
+       inherit_fds_check_s sec' sfds' \<and> sfds' \<subseteq> sfds"
+apply (rule conjI, erule_tac pi = pi and sec = sec and sfds = sfds and 
+   shms = shms and fi = fi and fsec = fsec and psec = psec and 
+   asecs = asecs in npctxt_execve_eq_cp2sproc, simp, simp, simp)
+apply (rule conjI, erule_tac pi = pi and sec = sec and sfds = sfds and 
+   shms = shms and fi = fi and fsec = fsec and psec = psec and 
+   asecs = asecs in grant_execve_intro_execve, simp, simp, simp)
+apply (rule conjI, drule_tac sec = sec in search_check_intro_execve, simp)
+apply (frule vd_cons, frule vt_grant_os)
+apply (drule_tac sec = sec in seach_check_eq_static, simp, simp, simp)
+apply (rule conjI, rule inherit_fds_check_imp_static, simp)
+apply (erule inherit_fds_check_intro_execve, simp, simp)
+apply (erule_tac pi = pi and sfds = sfds and shms = shms in execve_sfds_subset, simp+)
+done
+
+lemma d2s_main_execve:
+  "\<lbrakk>valid (Execve p f fds # s); s2ss s \<propto> static\<rbrakk> \<Longrightarrow> s2ss (Execve p f fds # s) \<propto> static"
+apply (frule vd_cons, frule vt_grant_os, clarsimp)
+apply (frule is_file_has_sfile', simp, erule exE, frule is_file_has_sfs, simp+, erule exE, erule conjE)
+apply (auto simp:s2ss_execve split:if_splits option.splits dest:current_proc_has_sp')
+apply (clarsimp simp add:init_ss_in_def init_ss_eq_def)
+apply (rule_tac x = "update_ss ss' (S_proc (ah, (ai, aj, bd), ak, be) (O_proc p \<in> Tainted s))
+  (S_proc (ad, (ae, af, bb), ag, bc) (O_proc p \<in> Tainted s \<or> O_file f \<in> Tainted s))" in bexI)
+apply (auto simp:update_ss_def elim:Set.subset_insertI2 simp:anotherp_imp_manysp)[1]
+apply (case_tac "ah = ad", case_tac "bc = {}", simp)
+apply (erule_tac sfs = sfs and fi = a and fsec = "(aa, ab,b)" and pfsec = ac and asecs = ba in s_execve,
+  auto intro:current_proc_in_s2ss current_file_in_s2ss split:option.splits dest:d2s_main_execve_grant_aux)[1]
+apply (simp add:cp2sproc_execve split:option.splits)
+apply (simp add:cp2sproc_def split:option.splits if_splits)
+
+apply (clarsimp simp add:init_ss_in_def init_ss_eq_def)
+apply (rule_tac x = "update_ss ss' (S_proc (ah, (ai, aj, bd), ak, be) (O_proc p \<in> Tainted s))
+  (S_proc (ad, (ae, af, bb), ag, bc) (O_proc p \<in> Tainted s \<or> O_file f \<in> Tainted s))" in bexI)
+apply (rule conjI, simp add:update_ss_def)
+apply (rule conjI, simp add:update_ss_def)
+apply (auto)[1]
+apply (simp add:update_ss_def)
+apply (rule conjI, rule impI)
+apply (rule subsetI, clarsimp)
+apply (erule impE)
+apply (erule set_mp, simp)
+apply (case_tac ah, simp+)
+apply (rule impI, rule subsetI, clarsimp)
+apply (erule set_mp, simp)
+
+apply (case_tac "ah = ad", case_tac "bc = {}", simp)
+apply (erule_tac sfs = sfs and fi = a and fsec = "(aa, ab,b)" and pfsec = ac and asecs = ba in s_execve,
+  auto intro:current_proc_in_s2ss current_file_in_s2ss split:option.splits dest:d2s_main_execve_grant_aux)[1]
+apply (simp add:cp2sproc_execve split:option.splits)
+apply (simp add:cp2sproc_def split:option.splits if_splits)
+done
+
+lemma co2sobj_eq_alive_proc_imp:
+  "\<lbrakk>co2sobj s obj = co2sobj s (O_proc p); alive s (O_proc p); valid s\<rbrakk>
+   \<Longrightarrow> \<exists> p'. obj = O_proc p'"
+by (auto simp add:co2sobj.simps split:option.splits dest:current_proc_has_sp' intro:co2sobj_sproc_imp)
+
+
+lemma enrichable_execve:
+ assumes p1: "\<And> objs. \<forall> obj \<in> objs. alive s obj \<and> is_created s obj \<and> recorded obj
+              \<Longrightarrow> \<exists> s'. valid s' \<and> s2ss s' = s2ss s \<and> enriched s objs s' \<and> reserved s objs s'"
+  and p2: "valid (e # s)" and p3: "\<forall>obj\<in>objs. alive (e # s) obj \<and> is_created (e # s) obj \<and> recorded obj"
+  and p4: "e = Execve p f fds" 
+  shows "enrichable (e # s) objs"
+proof-
+  from p2 have os: "os_grant s e" and se: "grant s e" and vd: "valid s"
+    by (auto dest:vt_grant_os vd_cons vt_grant)
+  from p3 have recorded: "\<forall> obj \<in> objs. recorded obj" by auto
+  from p3 p4 p2 have p1': "\<forall> obj \<in> objs. alive s obj \<and> is_created s obj"
+    apply clarify
+    apply (erule_tac x = obj in ballE, simp add:alive_simps)
+    apply (case_tac obj, auto simp:same_inode_files_simps)
+    done
+  then obtain s' where a1: "valid s'" and a2: "s2ss s' = s2ss s" and a3: "enriched s objs s'"
+    and a4: "reserved s objs s'"
+    using p1 recorded by metis 
+  show ?thesis
+  proof (cases "O_proc p \<in> objs")
+    case True
+    hence p_in: "p \<in> current_procs s'" using a4 os p4
+      by (auto simp:reserved_def elim:allE[where x = "O_proc p"])
+    with a1 a3 True obtain p' where b1: "\<not> alive s (O_proc p')" and b2: "O_proc p' \<notin> objs" 
+      and b3: "alive s' (O_proc p')" and b4: "co2sobj s' (O_proc p') = co2sobj s' (O_proc p)"
+      apply (simp only:enriched_def)
+      apply (erule_tac x = "O_proc p" in ballE)
+      apply (erule exE|erule conjE)+
+      apply (frule co2sobj_eq_alive_proc_imp, auto)
+      done
+    have "valid (Execve p' f fds # e # s')"
+      sorry
+    moreover have "s2ss (Execve p' f fds # e # s') = s2ss (e # s)"
+      sorry
+    moreover have "enriched (e # s) objs (Execve p' f fds # e # s')"
+      sorry
+    moreover have "reserved (e # s) objs (Execve p' f fds # e # s')"
+      sorry
+    ultimately show ?thesis
+      apply (simp add:enrichable_def)
+      apply (rule_tac x = "Execve p' f fds # e # s'" in exI)
+      by auto
+  next
+    case False
+    from a4 os p4 have "p \<in> current_procs s'"
+      apply (simp add:reserved_def)
+      by (erule_tac x = "O_proc p" in allE, auto)      
+    moreover from a4 os p4 have "is_file s' f"
+      apply (simp add:reserved_def)
+      by (erule_tac x = "O_file f" in allE, auto)
+    moreover from a4 os p4 have "fds \<subseteq> current_proc_fds s' p"
+      apply (rule_tac subsetI, clarsimp simp:reserved_def current_proc_fds.simps)
+      apply (erule_tac x = "O_fd p x" in allE, erule impE)
+      apply (simp, erule set_mp, simp+)
+      done
+    ultimately have "os_grant s' e" 
+      by (simp add:p4)
+    moreover have "grant s' e"
+      sorry
+    ultimately have "valid (e # s')"
+      using a1 by (erule_tac valid.intros(2), simp+)
+    thus ?thesis
+      apply (simp add:enrichable_def)
+      apply (rule_tac x = "e # s'" in exI)
+      apply (simp)
+    sorry
+qed
+
+lemma s2d_main_execve:
+  "\<lbrakk>grant_execve pctxt fsec pctxt'; ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; S_file sfs tagf \<in> ss;
+     (fi, fsec, pfsec, asecs) \<in> sfs; npctxt_execve pctxt fsec = Some pctxt'; 
+    search_check_s pctxt (fi, fsec, pfsec, asecs) True; inherit_fds_check_s pctxt' fds'; fds' \<subseteq> fds; valid s;
+    s2ss s = ss\<rbrakk> \<Longrightarrow> \<exists>s. valid s \<and> 
+    s2ss s = update_ss ss (S_proc (pi, pctxt, fds, shms) tagp) (S_proc (pi, pctxt', fds', {}) (tagp \<or> tagf))"
+apply (simp add:update_ss_def)
+thm update_ss_def
+sorry
+
+
+lemma s2d_main_execve:
+  "ss \<in> static \<Longrightarrow> \<exists> s. valid s \<and> s2ss s = ss"
+apply (erule static.induct)
+apply (rule_tac x = "[]" in exI, simp add:s2ss_nil_prop valid.intros)
+apply (erule exE|erule conjE)+
+apply (rule s2d_main_execve, simp+)
+
+apply (erule exE|erule conjE)+
+
+apply (simp add:update_ss_def)
+
+sorry
 
 
 
+(*********************** uppest-level 3 theorems ***********************)
+
+lemma enrichability: 
+  "\<lbrakk>valid s; \<forall> obj \<in> objs. alive s obj \<and> is_created s obj \<and> recorded obj\<rbrakk>
+   \<Longrightarrow> enrichable s objs"
+proof (induct s arbitrary:objs)
+  case Nil
+  hence "objs = {}" 
+    apply (auto simp:is_created_def)
+    apply (erule_tac x = x in ballE)
+    apply (auto simp:init_alive_prop)
+    done
+  thus ?case using Nil unfolding enrichable_def enriched_def reserved_def
+    by (rule_tac x = "[]" in exI, auto)
+next
+  case (Cons e s)
+  hence p1: "\<And> objs. \<forall> obj \<in> objs. alive s obj \<and> is_created s obj \<and> recorded obj
+             \<Longrightarrow> \<exists> s'. valid s' \<and> s2ss s' = s2ss s \<and> enriched s objs s' \<and> reserved s objs s'"
+    and p2: "valid (e # s)" and p3: "\<forall>obj\<in>objs. alive (e # s) obj \<and> is_created (e # s) obj \<and> recorded obj"
+    and os: "os_grant s e" and se: "grant s e" and vd: "valid s"
+    by (auto dest:vt_grant_os vd_cons vt_grant simp:enrichable_def)
+  show ?case 
+  proof (cases e)
+    case (Execve p f fds) 
+    hence p4: "e = Execve p f fds" by simp
+    from p3 have p5: "is_inited s (O_proc p) \<Longrightarrow> (O_proc p) \<notin> objs" 
+      by (auto simp:is_created_def is_inited_def p4 elim!:ballE[where x = "O_proc p"])
+    show "enrichable (e # s) objs"
+    proof (cases "is_inited s (O_proc p)")
+      case True
+      with p5 have a1: "(O_proc p) \<notin> objs" by simp
+      with p3 p4 p2 have a2: "\<forall> obj \<in> objs. alive s obj \<and> is_created s obj" and a2': "\<forall> obj \<in> objs. recorded obj"
+        apply (auto simp:is_created_def alive_simps is_inited_def)
+        apply (erule_tac x = obj in ballE, auto simp:alive_simps split:t_object.splits)
+        done
+      then obtain s' where a3: "valid s'" and a4: "s2ss s' = s2ss s"
+        and a5: "enriched s objs s'" and a6: "reserved s objs s'"
+        using p1 apply (simp add:enrichable_def) sorry
+      from a5 p4 p2 a2' have a7: "enriched s objs (e # s')"
+        apply (clarsimp simp add:enriched_def co2sobj_execve)
+        apply (erule_tac x = obj in ballE, clarsimp)
+        apply (rule_tac x = obj' in exI, auto simp:co2sobj_execve alive_simps)
+        thm enriched_def
 
 
-lemma d2s_main_execve:
-  "valid (Execve p f fds # s) \<Longrightarrow> s2ss (Execve p f fds # s) \<in> static"
-apply (frule vd_cons, frule vt_grant_os, clarsimp simp:s2ss_execve)
-sorry
+
+obtain s' where p6:"enriched s objs s'"
+        apply (simp add: alive_simps enrichable_def)       
+        apply auto apply (rule ballI, rule_tac x = obj in exI)
+
+        have p6:"enriched (e # s) objs (e # s)"
+        apply (simp add:enriched_def alive_simps)       
+        apply auto apply (rule ballI, rule_tac x = obj in exI)
+
+      have "enrich (e # s) objs (e # s)"
+        apply (simp add:enrich_def p4)
+        sorry
+      moreover have "reserve (e # s) objs (e # s)"
+        sorry
+      ultimately show ?thesis using p2
+        apply (simp add:enrichable_def)
+        by (rule_tac x = "e # s" in exI, simp)
+    next
+        
+      
+thm enrichable_def
+      apply (simp add:enrichable_def p4)
+
+      
+  
+    apply auto
+    apply (auto simp:enrichable_def)
+apply (induct s)
+
+
+
+done
+
+qed
 
 lemma d2s_main:
   "valid s \<Longrightarrow> s2ss s \<propto> static"
@@ -56,63 +578,6 @@
 
 sorry
 
-
-lemma many_sq_imp_sms:
-  "\<lbrakk>S_msgq (Create, sec, sms) \<in> ss; ss \<in> static\<rbrakk> \<Longrightarrow> \<forall> sm \<in> (set sms). is_many_smsg sm"
-sorry
-
-
-(* recorded in our static world *)
-fun recorded :: "t_object \<Rightarrow> bool"
-where
-  "recorded (O_proc p)     = True"
-| "recorded (O_file f)     = True"
-| "recorded (O_dir  f)     = True"
-| "recorded (O_node n)     = False" (* cause socket is temperary not considered *)
-| "recorded (O_shm  h)     = True"
-| "recorded (O_msgq q)     = True"
-| "recorded _              = False"
-
-lemma enrichability: 
-  "\<lbrakk>valid s; \<forall> obj \<in> objs. alive s obj \<and> is_created s obj \<and> recorded obj\<rbrakk>
-   \<Longrightarrow> enrichable s objs"
-proof (induct s arbitrary:objs)
-  case Nil
-  hence "objs = {}" 
-    apply (auto simp:is_created_def)
-    apply (erule_tac x = x in ballE)
-    apply (auto simp:init_alive_prop)
-    done
-  thus ?case using Nil unfolding enrichable_def enrich_def reserve_def
-    by (rule_tac x = "[]" in exI, auto)
-next
-  case (Cons e s)
-  hence p1: "\<And> objs. \<forall> obj \<in> objs. alive s obj \<and> is_created s obj \<and> recorded obj \<Longrightarrow> enrichable s objs"
-    and p2: "valid (e # s)" and p3: "\<forall>obj\<in>objs. alive (e # s) obj \<and> is_created (e # s) obj \<and> recorded obj"
-    and os: "os_grant s e" and se: "grant s e" and vd: "valid s"
-    by (auto dest:vt_grant_os vd_cons vt_grant)
-  show ?case sorry (*
-  proof (cases e)
-    case (Execve p f fds)
-    hence p4: "e = Execve p f fds" by simp
-    from p3 have p5: "is_inited s (O_proc p) \<Longrightarrow> (O_proc p) \<notin> objs"
-      by (auto simp:is_created_def is_inited_def p4 elim!:ballE[where x = "O_proc p"])
-    show "enrichable (e # s) objs"
-    proof (case "is_inited s (O_proc p)")
-      apply (simp add:enrichable_def p4)
-
-      
-  
-    apply auto
-    apply (auto simp:enrichable_def)
-apply (induct s)
-
-
-
-done
-*)
-qed
-
 lemma s2d_main:
   "ss \<in> static \<Longrightarrow> \<exists> s. valid s \<and> s2ss s = ss"
 apply (erule static.induct)