theory Dynamic_staticimports Main Flask Static Init_prop Valid_prop Tainted_prop Delete_prop Co2sobj_prop S2ss_prop S2ss_prop2 Tempbegincontext tainting_s beginfun 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)sorrylemma 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 \<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 \<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) 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_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 simpnext 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)qedlemma proc_filefd_has_sfd: "\<lbrakk>fd \<in> proc_file_fds s p; valid s\<rbrakk> \<Longrightarrow> \<exists> sfd. cfd2sfd s p fd = Some sfd"apply (simp add:proc_file_fds_def)apply (auto dest: current_filefd_has_sfd)donelemma enrich_inherit_fds_check: assumes grant: "inherit_fds_check s (up, nr, nt) p fds" and vd: "valid s" and cp2sp: "\<forall> p. p \<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> proc_file_fds s p" and fd_in': "fds \<subseteq> proc_file_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> proc_file_fds s p" and fd_in_cfds': "fd \<in> proc_file_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" using fd_in_cfds fd_in_cfds' apply (simp add:cpfd2sfds_def) apply (frule proc_filefd_has_sfd, simp add:vd, erule exE) apply (drule_tac x = sfd in eqset_imp_iff, simp) (* thm inherit_fds_check_def thm sectxts_of_fds_def thm cpfd2sfds_def apply ( *)sorry 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)qedlemma enrich_proc_aux1: assumes vs': "valid s'" 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" shows "valid (e # s')"sorry (*proof (cases e) case (Execve p f fds) have p_in: "p \<in> current_procs s'" using os alive apply (erule_tac x = "O_proc p" in allE) by (auto simp:Execve) have f_in: "is_file s' f" using os alive apply (erule_tac x = "O_file f" in allE) by (auto simp:Execve) have fd_in: "fds \<subseteq> current_proc_fds s' p" using os alive 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" 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)" and p2: "sectxt_of_obj s (O_file f) = Some (uf, rf, tf)" by (simp add:Execve split:option.splits, blast) with grant obtain pu nr nt where p3: "npctxt_execve (up, rp, tp) (uf, rf, tf) = Some (pu, nr, nt)" by (simp add:Execve split:option.splits del:npctxt_execve.simps, blast) from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)" using os cp2sp apply (erule_tac x = p in allE) by (auto simp:Execve co2sobj.simps cp2sproc_def split:option.splits) 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*)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 {})))"sorry (*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)" 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 autoqed*)lemma "alive s obj \<Longrightarrow> alive (enrich_proc s p p') obj"apply (induct s, simp)apply (case_tac a, case_tac[!] obj) sorry (*apply (auto simp:is_file_def is_dir_def split:option.splits t_inode_tag.splits)thm is_file_other*)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 28end*)sorry(* 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 "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> enriched s objs s' \<and> reserved s objs s'"fun is_created :: "t_state \<Rightarrow> t_object \<Rightarrow> bool"where "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+)donelemma 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 autolemma 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+)donelemma 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+)+donelemma 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)donedeclare 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)donelemma 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')donelemma 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)donelemma 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)donelemma 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)donelemma 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)donelemma 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)donelemma 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)sorry (*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+)donelemma 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)donelemma 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 vd have "fds \<subseteq> proc_file_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) sorry 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) sorryqedqedlemma 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_defsorry(*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)+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" sorry (* proof (induct s arbitrary:objs) case Nil hence "objs = {}" apply (auto) apply (erule_tac x = x in ballE) apply (case_tac x) apply (auto simp:init_alive_prop) sorry (* 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_defobtain 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) nextthm enrichable_def apply (simp add:enrichable_def p4) apply auto apply (auto simp:enrichable_def)apply (induct s)doneqed *)lemma d2s_main: "valid s \<Longrightarrow> s2ss s \<propto> static"apply (induct s, simp add:s2ss_nil_prop init_ss_in_def)apply (rule_tac x = "init_static_state" in bexI, simp, simp add:s_init)apply (frule vd_cons, frule vt_grant_os, simp)apply (case_tac a) apply (clarsimp simp add:s2ss_execve)apply (rule conjI, rule impI)sorrylemma s2d_main: "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 (simp add:update_ss_def)sorrylemma s2d_main': "ss \<in> static \<Longrightarrow> \<exists> s. valid s \<and> s2ss s \<doteq> ss"apply (erule static.induct)apply (rule_tac x = "[]" in exI, simp add:s2ss_nil_prop valid.intros)apply (erule exE|erule conjE)+apply (simp add:update_ss_def)sorryendend