--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/tainted_vs_tainted_s.thy Fri Apr 12 10:43:11 2013 +0100
@@ -0,0 +1,1466 @@
+theory tainted_vs_tainted_s
+imports Main rc_theory os_rc deleted_prop tainted obj2sobj_prop source_prop all_sobj_prop
+begin
+
+context tainting_s_complete begin
+
+lemma t2ts[rule_format]:
+ "obj \<in> tainted s \<Longrightarrow> obj2sobj s obj \<in> tainted_s "
+proof (induct rule:tainted.induct)
+ case (t_init obj)
+ assume seed: "obj \<in> seeds"
+ hence"exists [] obj" by (drule_tac seeds_in_init, case_tac obj, auto)
+ thus ?case using seed by (simp add:ts_init obj2sobj_nil_init)
+next
+ case (t_clone p s p')
+ assume p1: "Proc p \<in> tainted s"
+ and p2: "obj2sobj s (Proc p) \<in> tainted_s"
+ and p3: "valid (Clone p p' # s)"
+ from p3 have os: "os_grant s (Clone p p')" and rc: "rc_grant s (Clone p p')"
+ and vs: "valid s" by (auto dest:valid_cons valid_os valid_rc)
+ from os have exp: "exists s (Proc p)" by (simp add:os_grant.simps)
+ from exp obtain r fr pt u sp where sproc: "cp2sproc s p = Some (r,fr,pt,u)"
+ and srp: "source_proc s p = Some sp" using vs
+ apply (simp del:cp2sproc.simps)
+ by (frule current_proc_has_sproc, simp, frule current_proc_has_srp, simp, blast)
+ with exp all_sobjs_I[where obj = "Proc p" and s = s] vs
+
+ have "obj2sobj (Clone p p' # s) (Proc p') = SProc (r,fr,clone_type_aux r pt, u) (Some sp)"
+ using sproc srp p3
+ by (simp add:obj2sobj.simps cp2sproc_clone del:cp2sproc.simps)
+ moreover have "(r, Proc_type pt, CREATE) \<in> compatible" using rc sproc
+ by (auto split:option.splits)
+ moreover have "SProc (r, fr, pt, u) (Some sp) \<in> tainted_s" using p2 sproc srp
+ by simp
+ ultimately show ?case by (auto intro:ts_clone)
+next
+ case (t_exec f s p)
+ assume p1: "File f \<in> tainted s"
+ and p2: "obj2sobj s (File f) \<in> tainted_s"
+ and p3: "valid (Execute p f # s)"
+ from p3 have os: "os_grant s (Execute p f)" and rc: "rc_grant s (Execute p f)"
+ and vs: "valid s" by (auto dest:valid_cons valid_os valid_rc)
+ from os have exp: "exists s (Proc p)" and exf: "exists s (File f)" by auto
+ from exp obtain r fr pt u where sproc: "cp2sproc s p = Some (r,fr,pt,u)"
+ using vs by (auto simp del:cp2sproc.simps dest!:current_proc_has_sproc)
+ with exp all_sobjs_I[where obj = "Proc p" and s = s] vs
+ have SP: "SProc (r,fr,pt,u) (source_proc s p) \<in> all_sobjs"
+ by (auto simp:obj2sobj.simps)
+ from exf obtain ft sd where etype: "etype_of_file s f = Some ft"
+ and srdir: "source_dir s f = Some sd" using vs
+ by (simp, drule_tac current_file_has_sd, auto dest:current_file_has_etype)
+ with p2 obtain srf where TF: "SFile (ft, sd) srf \<in> tainted_s"
+ by (auto simp:obj2sobj.simps split:if_splits)
+ from sproc srdir have "u \<in> init_users" and "sd \<in> init_files" using vs
+ by (auto simp:obj2sobj.simps cp2sproc.simps
+ intro:source_dir_in_init owner_in_users
+ split:option.splits)
+ then obtain nr nfr where nrole: "exec_role_aux r sd u = Some nr"
+ and nfrole: "erole_functor init_file_forcedrole InheritUpMixed sd = Some nfr"
+ by (frule_tac r = r in exec_role_some, simp, frule_tac efffrole_sdir_some, auto)
+ hence "cp2sproc (Execute p f # s) p = Some (nr, nfr, exec_type_aux r pt, u)"
+ using p3 srdir sproc by (simp add:cp2sproc_exec)
+ with nrole nfrole TF SP rc sproc etype
+ show ?case
+ by (auto simp:obj2sobj.simps cp2sproc.simps intro!:ts_exec1 split:option.splits)
+next
+ case (t_cfile p s f)
+ assume p1: "Proc p \<in> tainted s" and p2: "obj2sobj s (Proc p) \<in> tainted_s"
+ and p3: "valid (CreateFile p f # s)"
+ from p3 have os: "os_grant s (CreateFile p f)" and rc: "rc_grant s (CreateFile p f)"
+ and vs: "valid s" by (auto dest:valid_cons valid_os valid_rc)
+ from os obtain pf where parent: "parent f = Some pf" and exp: "exists s (Proc p)"
+ and expf: "exists s (File pf)" by auto
+ from exp obtain r fr pt u where sproc: "cp2sproc s p = Some (r,fr,pt,u)"
+ using vs by (auto simp del:cp2sproc.simps dest!:current_proc_has_sproc)
+ with p2 have TP: "SProc (r,fr,pt,u) (source_proc s p) \<in> tainted_s"
+ by (auto simp:obj2sobj.simps cp2sproc.simps)
+ from expf obtain pft sd where etype: "etype_of_file s pf = Some pft"
+ and srdir: "source_dir s pf = Some sd" using vs
+ by (simp, drule_tac current_file_has_sd, auto dest:current_file_has_etype)
+ with expf all_sobjs_I[where obj = "File pf" and s = s] vs
+ obtain srpf where SF: "SFile (pft, sd) srpf \<in> all_sobjs"
+ by (auto simp:obj2sobj.simps cp2sproc.simps split:if_splits)
+ show ?case using etype srdir p3 parent os
+ apply (auto simp:source_dir_simps init_notin_curf_deleted obj2sobj.simps split:option.splits
+ dest!:current_file_has_etype')
+ apply (case_tac "default_fd_create_type r")
+ using SF TP rc sproc
+ apply (rule_tac sf = srpf in ts_cfd',
+ auto simp:etype_of_file_def etype_aux_prop3 obj2sobj.simps cp2sproc.simps
+ split:option.splits) [1]
+ using SF TP rc sproc
+ apply (rule_tac sf = srpf in ts_cfd)
+ apply (auto simp:etype_of_file_def etype_aux_prop4 cp2sproc.simps split:option.splits)
+ done
+next
+ case (t_cipc p s i)
+ assume p1: "Proc p \<in> tainted s" and p2: "obj2sobj s (Proc p) \<in> tainted_s"
+ and p3: "valid (CreateIPC p i # s)"
+ from p3 have os: "os_grant s (CreateIPC p i)" and rc: "rc_grant s (CreateIPC p i)"
+ and vs: "valid s" by (auto dest:valid_cons valid_os valid_rc)
+ from os have exp: "exists s (Proc p)" by simp
+ from exp obtain r fr pt u where sproc: "cp2sproc s p = Some (r,fr,pt,u)"
+ using vs by (auto simp del:cp2sproc.simps dest!:current_proc_has_sproc)
+ with p2 have TP: "SProc (r,fr,pt,u) (source_proc s p) \<in> tainted_s"
+ by (auto simp:obj2sobj.simps cp2sproc.simps)
+ show ?case using p3 sproc os rc TP
+ by (auto simp:ni_init_deled obj2sobj.simps cp2sproc.simps
+ split:option.splits intro!:ts_cipc)
+next
+ case (t_read f s p)
+ assume p1: "File f \<in> tainted s" and p2: "obj2sobj s (File f) \<in> tainted_s"
+ and p3: "valid (ReadFile p f # s)"
+ from p3 have os: "os_grant s (ReadFile p f)" and rc: "rc_grant s (ReadFile p f)"
+ and vs: "valid s" by (auto dest:valid_cons valid_os valid_rc)
+ from os have exp: "exists s (Proc p)" and exf: "exists s (File f)" by auto
+ from exp obtain r fr pt u where sproc: "cp2sproc s p = Some (r,fr,pt,u)"
+ using vs by (auto simp del:cp2sproc.simps dest!:current_proc_has_sproc)
+ with exp all_sobjs_I[where obj = "Proc p" and s = s] vs
+ have SP: "SProc (r,fr,pt,u) (source_proc s p) \<in> all_sobjs"
+ by (auto simp:obj2sobj.simps)
+ from exf obtain ft sd where etype: "etype_of_file s f = Some ft"
+ and srdir: "source_dir s f = Some sd" using vs
+ by (simp, drule_tac current_file_has_sd, auto dest:current_file_has_etype)
+ with p2 obtain srf where TF: "SFile (ft, sd) srf \<in> tainted_s"
+ by (auto simp:obj2sobj.simps cp2sproc.simps split:if_splits)
+ show ?case using sproc SP TF rc etype
+ by (auto simp:obj2sobj.simps cp2sproc.simps
+ split:option.splits intro!:ts_read)
+next
+ case (t_write p s f)
+ assume p1: "Proc p \<in> tainted s" and p2: "obj2sobj s (Proc p) \<in> tainted_s"
+ and p3: "valid (WriteFile p f # s)"
+ from p3 have os: "os_grant s (WriteFile p f)" and rc: "rc_grant s (WriteFile p f)"
+ and vs: "valid s" by (auto dest:valid_cons valid_os valid_rc)
+ from os have exp: "exists s (Proc p)" and exf: "exists s (File f)" by auto
+ from exf obtain ft sd where etype: "etype_of_file s f = Some ft"
+ and srdir: "source_dir s f = Some sd" using vs
+ by (simp, drule_tac current_file_has_sd, auto dest:current_file_has_etype)
+ from exp obtain r fr pt u where sproc: "cp2sproc s p = Some (r,fr,pt,u)"
+ using vs by (auto simp del:cp2sproc.simps dest!:current_proc_has_sproc)
+ with exp p2 have TP: "SProc (r,fr,pt,u) (source_proc s p) \<in> tainted_s"
+ by (auto simp:obj2sobj.simps)
+ from etype p3 have etype':"etype_of_file (WriteFile p f # s) f = Some ft"
+ by (case_tac f, auto simp:etype_of_file_def)
+ have SF: "obj2sobj s (File f) \<in> all_sobjs" using exf vs
+ by (rule_tac all_sobjs_I, simp+)
+ show ?case using sproc TP rc etype p3 srdir etype' SF
+ by (auto simp:source_dir_simps obj2sobj.simps cp2sproc.simps
+ split:option.splits intro!:ts_write)
+next
+ case (t_send p s i)
+ assume p1: "Proc p \<in> tainted s" and p2: "obj2sobj s (Proc p) \<in> tainted_s"
+ and p3: "valid (Send p i # s)"
+ from p3 have os: "os_grant s (Send p i)" and rc: "rc_grant s (Send p i)"
+ and vs: "valid s" by (auto dest:valid_cons valid_os valid_rc)
+ from os have exp: "exists s (Proc p)" and exi: "exists s (IPC i)" by auto
+ from exi obtain t where etype: "type_of_ipc s i = Some t" using vs
+ by (simp, drule_tac current_ipc_has_type, auto)
+ from exp obtain r fr pt u where sproc: "cp2sproc s p = Some (r,fr,pt,u)"
+ using vs by (auto simp del:cp2sproc.simps dest!:current_proc_has_sproc)
+ with exp p2 have TP: "SProc (r,fr,pt,u) (source_proc s p) \<in> tainted_s"
+ by (auto simp:obj2sobj.simps cp2sproc.simps)
+ have SI: "obj2sobj s (IPC i) \<in> all_sobjs" using exi vs
+ by (simp add:all_sobjs_I del:obj2sobj.simps)
+ show ?case using sproc TP rc etype p3 vs SI
+ by (auto simp:obj2sobj.simps cp2sproc.simps
+ split:option.splits intro!:ts_send)
+next
+ case (t_recv i s p)
+ assume p1: "IPC i \<in> tainted s" and p2: "obj2sobj s (IPC i) \<in> tainted_s"
+ and p3: "valid (Recv p i # s)"
+ from p3 have os: "os_grant s (Recv p i)" and rc: "rc_grant s (Recv p i)"
+ and vs: "valid s" by (auto dest:valid_cons valid_os valid_rc)
+ from os have exp: "exists s (Proc p)" and exi: "exists s (IPC i)" by auto
+ from exp obtain r fr pt u where sproc: "cp2sproc s p = Some (r,fr,pt,u)"
+ using vs by (auto simp del:cp2sproc.simps dest!:current_proc_has_sproc)
+ with exp all_sobjs_I[where obj = "Proc p" and s = s] vs
+ have SP: "SProc (r,fr,pt,u) (source_proc s p) \<in> all_sobjs"
+ by (auto simp:obj2sobj.simps)
+ from exi obtain t where etype: "type_of_ipc s i = Some t"using vs
+ by (simp, drule_tac current_ipc_has_type, auto)
+ with p2 obtain sri where TI: "SIPC t sri \<in> tainted_s"
+ by (auto simp:obj2sobj.simps split:if_splits)
+ show ?case using sproc SP TI rc etype
+ by (auto simp:obj2sobj.simps cp2sproc.simps
+ split:option.splits intro!:ts_recv)
+next
+ case (t_remain obj s e)
+ from t_remain(1) have p5: "exists s obj" by (rule tainted_is_current)
+ from t_remain(3) have os: "os_grant s e" and vs: "valid s" and rc: "rc_grant s e"
+ by (auto dest:valid_os valid_cons valid_rc)
+ show ?case
+ proof (cases obj)
+ case (File f)
+ have "obj2sobj (e # s) (File f) = obj2sobj s (File f)"
+ proof-
+ have "etype_of_file (e # s) f = etype_of_file s f"
+ using p5 os vs File t_remain(3,4)
+ apply (case_tac e, auto simp:etype_of_file_def split:option.splits)
+ by (auto dest:ancient_file_in_current intro!:etype_aux_prop)
+ moreover have "source_dir (e # s) f = source_dir s f"
+ using p5 os vs File t_remain(3,4)
+ by (case_tac e, auto simp:source_dir_simps dest:source_dir_prop)
+ ultimately show ?thesis using vs t_remain(4) File
+ apply (auto simp:obj2sobj.simps cp2sproc.simps
+ split:if_splits option.splits dest:not_deleted_cons_D)
+ by (case_tac e, auto)
+ qed
+ with File t_remain(2) show ?thesis by simp
+ next
+ case (IPC i)
+ have "obj2sobj (e # s) (IPC i) = obj2sobj s (IPC i)" using p5 t_remain(3,4) os IPC
+ by (case_tac e, auto simp:ni_init_deled ni_notin_curi obj2sobj.simps
+ split:option.splits
+ dest!:current_proc_has_role')
+ with IPC t_remain(2) show ?thesis by simp
+ next
+ case (Proc p)
+ show ?thesis
+ proof-
+ have "\<And> f. e = Execute p f \<Longrightarrow> obj2sobj (e # s) (Proc p) \<in> tainted_s"
+ proof-
+ fix f
+ assume ev: "e = Execute p f"
+ show "obj2sobj (e # s) (Proc p) \<in> tainted_s"
+ proof-
+ from os ev have exp: "exists s (Proc p)" and exf: "exists s (File f)" by auto
+ from exp obtain r fr pt u where sproc: "cp2sproc s p = Some (r,fr,pt,u)"
+ using vs by (auto simp del:cp2sproc.simps dest!:current_proc_has_sproc)
+ with Proc t_remain(2)
+ have TP: "SProc (r,fr,pt,u) (source_proc s p) \<in> tainted_s"
+ by (auto simp:obj2sobj.simps cp2sproc.simps)
+ from exf obtain ft sd where etype: "etype_of_file s f = Some ft"
+ and srdir: "source_dir s f = Some sd" using vs
+ by (simp, drule_tac current_file_has_sd, auto dest:current_file_has_etype)
+ with exf all_sobjs_I[where obj = "File f" and s = s] vs
+ obtain srf where SF: "SFile (ft, sd) srf \<in> all_sobjs"
+ by (auto simp:obj2sobj.simps split:if_splits)
+ from sproc srdir have "u \<in> init_users" and "sd \<in> init_files" using vs
+ by (auto simp:obj2sobj.simps cp2sproc.simps
+ intro:source_dir_in_init owner_in_users split:option.splits)
+ then obtain nr nfr where nrole: "exec_role_aux r sd u = Some nr"
+ and nfrole: "erole_functor init_file_forcedrole InheritUpMixed sd = Some nfr"
+ by (frule_tac r = r in exec_role_some, simp, frule_tac efffrole_sdir_some, auto)
+ hence "cp2sproc (Execute p f # s) p = Some (nr, nfr, exec_type_aux r pt, u)"
+ using t_remain(3) srdir sproc ev by (simp add:cp2sproc_exec)
+ with nrole nfrole SF TP rc sproc etype ev
+ show ?thesis
+ by (auto simp:obj2sobj.simps cp2sproc.simps
+ intro!:ts_exec2 split:option.splits)
+ qed
+ qed moreover
+ have "\<And> r'. e = ChangeRole p r' \<Longrightarrow> obj2sobj (e # s) (Proc p) \<in> tainted_s"
+ proof-
+ fix r'
+ assume ev: "e = ChangeRole p r'"
+ show "obj2sobj (e # s) (Proc p) \<in> tainted_s"
+ proof-
+ from os ev have exp: "exists s (Proc p)" by auto
+ from exp obtain r fr pt u where sproc: "cp2sproc s p = Some (r,fr,pt,u)"
+ using vs by (auto simp del:cp2sproc.simps dest!:current_proc_has_sproc)
+ with Proc t_remain(2)
+ have TP: "SProc (r,fr,pt,u) (source_proc s p) \<in> tainted_s"
+ by (auto simp:obj2sobj.simps cp2sproc.simps)
+ with rc sproc ev show ?thesis
+ apply (simp add:obj2sobj.simps cp2sproc.simps split:option.splits)
+ by (rule_tac ts_crole, simp+)
+ qed
+ qed moreover
+ have "\<And> u'. e = ChangeOwner p u' \<Longrightarrow> obj2sobj (e # s) (Proc p) \<in> tainted_s"
+ proof-
+ fix u'
+ assume ev: "e = ChangeOwner p u'"
+ show "obj2sobj (e # s) (Proc p) \<in> tainted_s"
+ proof-
+ from os ev have exp: "exists s (Proc p)" by auto
+ from exp obtain r fr pt u where sproc: "cp2sproc s p = Some (r,fr,pt,u)"
+ using vs by (auto simp del:cp2sproc.simps dest!:current_proc_has_sproc)
+ with Proc t_remain(2)
+ have TP: "SProc (r,fr,pt,u) (source_proc s p) \<in> tainted_s"
+ by (auto simp:obj2sobj.simps cp2sproc.simps)
+ from os ev have uinit: "u' \<in> init_users" by simp
+ then obtain nr where chown: "chown_role_aux r fr u' = Some nr"
+ by (auto dest:chown_role_some)
+ hence nsproc:"cp2sproc (e#s) p = Some (nr,fr,chown_type_aux r nr pt, u')"
+ using sproc ev os
+ by (auto split:option.splits t_role.splits
+ simp del:currentrole.simps type_of_process.simps
+ simp add:obj2sobj.simps cp2sproc.simps
+ chown_role_aux_valid chown_type_aux_valid)
+ with rc sproc ev TP uinit chown
+ show ?thesis
+ by (auto simp:obj2sobj.simps cp2sproc.simps
+ intro!:ts_chown split:option.splits)
+ qed
+ qed moreover
+ have "\<lbrakk>\<forall> f. e \<noteq> Execute p f; \<forall> r. e \<noteq> ChangeRole p r; \<forall> u. e \<noteq> ChangeOwner p u\<rbrakk>
+ \<Longrightarrow> obj2sobj (e # s) (Proc p) \<in> tainted_s"
+ using t_remain(2,3,4) os p5 Proc
+ by (case_tac e, auto simp add:obj2sobj.simps cp2sproc_simps np_notin_curp
+ simp del:cp2sproc.simps split:option.splits)
+ ultimately show ?thesis using Proc
+ by (case_tac e, auto simp del:obj2sobj.simps)
+ qed
+ qed
+qed
+
+end
+
+context tainting_s_sound begin
+
+lemma tainted_s'_eq1: "sobj \<in> tainted_s \<Longrightarrow> sobj \<in> tainted_s'"
+apply (erule tainted_s.induct)
+apply (auto elim:ts'_init ts'_exec1 ts'_exec2 ts'_cfd ts'_cfd' ts'_cipc ts'_read ts'_write ts'_recv ts'_send ts'_crole ts'_chown simp:all_sobjs'_eq)
+by (simp add:clone_type_aux_def clone_type_unchange)
+
+lemma tainted_s'_eq2: "sobj \<in> tainted_s' \<Longrightarrow> sobj \<in> tainted_s"
+apply (erule tainted_s'.induct)
+by (auto intro:ts_init ts_exec1 ts_exec2 ts_cfd ts_cfd' ts_cipc ts_read ts_write ts_recv ts_send ts_crole ts_chown ts_clone simp:all_sobjs'_eq)
+
+lemma tainted_s'_eq: "(sobj \<in> tainted_s) = (sobj \<in> tainted_s')"
+by (auto intro:iffI tainted_s'_eq1 tainted_s'_eq2)
+
+(* cause sobj_source_eq_sobj may conflict with initp_intact, so remove it too. *)
+lemma ts2t_intact:
+ "sobj \<in> tainted_s' \<Longrightarrow> \<exists> obj s. obj2sobj s obj = sobj \<and> obj \<in> tainted s \<and>
+ no_del_event s \<and> initp_intact s"
+
+proof (induct rule:tainted_s'.induct)
+ case (ts'_init obj)
+ hence ex: "exists [] obj"
+ apply (drule_tac seeds_in_init)
+ by (case_tac obj, simp+)
+ have "obj2sobj [] obj = init_obj2sobj obj" using ex
+ by (simp add:obj2sobj_nil_init)
+ moreover have "obj \<in> tainted []" using ts'_init by (simp add:t_init)
+ moreover have "initp_intact []"
+ by (auto simp:initp_intact_def obj2sobj.simps cp2sproc.simps split:option.splits)
+ ultimately show ?case
+ by (rule_tac x = obj in exI, rule_tac x = "[]" in exI, simp+)
+next
+ case (ts'_exec1 t sd srf r fr pt u srp r' fr')
+ then obtain f s where TF: "(File f) \<in> tainted s" and vds: "valid s"
+ and "f \<in> current_files s \<and> obj2sobj s (File f) = SFile (t, sd) srf \<and>
+ no_del_event s \<and> initp_intact s"
+ apply (clarsimp, frule_tac obj2sobj_file)
+ by (frule tainted_is_valid, frule tainted_is_current, auto)
+ with ts'_exec1(3) obtain p s' where vds's: "valid (s' @ s)"
+ and etype: "obj2sobj (s'@s) (File f) = SFile (t, sd) srf"
+ and nodels': "no_del_event (s'@s)"
+ and intacts': "initp_intact (s'@s)"
+ and ISP: "obj2sobj (s'@s) (Proc p) = SProc (r,fr,pt,u) srp"
+ and exp: "p \<in> current_procs (s' @ s)"
+ and exf: "f \<in> current_files (s' @ s)"
+ apply (drule_tac s' =s and obj' = "File f" in all_sobjs_E0, auto)
+ apply (frule_tac obj = "File f" in nodel_tainted_exists, simp)
+ by (frule obj2sobj_proc, clarsimp)
+ obtain ev \<tau> where ev: "ev = Execute (new_proc (s'@s)) f"
+ and tau: "\<tau> = Clone p (new_proc (s'@s)) # (s' @ s)" by auto
+ hence vs_tau:"valid \<tau>" using exp vds's by (auto intro:clone_event_no_limit)
+
+ have valid: "valid (ev # \<tau>)"
+ proof-
+ have "os_grant \<tau> ev"
+ using ev tau by (simp add:exf exp)
+ moreover have "rc_grant \<tau> ev"
+ using ev tau ts'_exec1 ISP etype
+ by (auto simp:etype_of_file_def cp2sproc.simps obj2sobj.simps
+ split:if_splits option.splits)
+ ultimately show ?thesis using vs_tau
+ by (erule_tac vs_step, simp+)
+ qed moreover
+ have "obj2sobj (ev # \<tau>) (Proc (new_proc (s'@s))) =
+ SProc (r', fr', exec_type_aux r pt, u) srp"
+ proof-
+ have "obj2sobj (s'@s) (Proc p) = SProc (r,fr,pt,u) srp" using ISP tau vs_tau
+ by (auto split:option.splits simp:cp2sproc_simps obj2sobj.simps)
+ hence "obj2sobj \<tau> (Proc (new_proc (s'@s))) = SProc (r,fr,pt,u) srp" using tau
+ by (auto simp:obj2sobj.simps cp2sproc.simps pct_def clone_type_unchange
+ split:option.splits)
+ moreover have "source_dir \<tau> f = Some sd" using vs_tau etype tau
+ by (auto simp:obj2sobj.simps source_dir_simps split:option.splits if_splits)
+ ultimately show ?thesis using valid ts'_exec1(5) ts'_exec1(6) ev
+ by (auto simp:cp2sproc_exec obj2sobj.simps split:option.splits)
+ qed moreover
+ have "Proc (new_proc (s'@s)) \<in> tainted (ev # \<tau>)"
+ proof-
+ have "(File f) \<in> tainted \<tau>" using TF nodels' tau vs_tau
+ by (drule_tac s = "Clone p (new_proc (s' @ s)) # s'" in t_remain_app,auto)
+ thus ?thesis using ev valid
+ by (drule_tac t_exec, simp+)
+ qed moreover
+ have "no_del_event (ev # \<tau>)" using ev tau nodels' by simp
+ moreover have "initp_intact (ev#\<tau>)" using ev tau intacts' valid
+ by (simp add:initp_intact_I_exec)
+ ultimately show ?case
+ apply (rule_tac x = "Proc (new_proc (s'@s))" in exI)
+ by (rule_tac x = "ev#\<tau>" in exI, auto)
+next
+ case (ts'_exec2 r fr pt u srp t sd srf r' fr')
+ then obtain p s where TP: "(Proc p) \<in> tainted s" and vds: "valid s"
+ and "p \<in> current_procs s \<and> obj2sobj s (Proc p) = SProc (r, fr, pt, u) srp \<and>
+ no_del_event s \<and> initp_intact s"
+ apply (clarsimp, frule_tac obj2sobj_proc)
+ by (frule tainted_is_valid, frule tainted_is_current, auto)
+ with ts'_exec2(3) obtain f s' where vds's: "valid (s' @ s)"
+ and etype: "obj2sobj (s'@s) (File f) = SFile (t, sd) srf"
+ and nodels': "no_del_event (s'@s)"
+ and intacts': "initp_intact (s'@s)"
+ and ISP: "obj2sobj (s'@s) (Proc p) = SProc (r,fr,pt,u) srp"
+ and exp: "p \<in> current_procs (s' @ s)"
+ and exf: "f \<in> current_files (s' @ s)"
+ apply (drule_tac s' =s and obj' = "Proc p" in all_sobjs_E0, auto)
+ apply (frule_tac obj = "Proc p" in nodel_tainted_exists, simp)
+ by (frule obj2sobj_file, clarsimp)
+ obtain ev \<tau> where ev: "ev = Execute (new_proc (s'@s)) f"
+ and tau: "\<tau> = Clone p (new_proc (s'@s)) # (s' @ s)" by auto
+ hence vs_tau:"valid \<tau>" using exp vds's by (auto intro:clone_event_no_limit)
+
+ have valid: "valid (ev # \<tau>)"
+ proof-
+ have "os_grant \<tau> ev"
+ using ev tau by (simp add:exf exp)
+ moreover have "rc_grant \<tau> ev"
+ using ev tau ts'_exec2(4) ISP etype
+ by (auto simp:etype_of_file_def cp2sproc.simps obj2sobj.simps
+ split:if_splits option.splits)
+ ultimately show ?thesis using vs_tau
+ by (erule_tac vs_step, simp+)
+ qed moreover
+ have "obj2sobj (ev # \<tau>) (Proc (new_proc (s'@s))) =
+ SProc (r', fr', exec_type_aux r pt, u) srp"
+ proof-
+ have "obj2sobj (s'@s) (Proc p) = SProc (r,fr,pt,u) srp" using ISP tau vs_tau
+ by (auto split:option.splits simp:cp2sproc_simps obj2sobj.simps)
+ hence "obj2sobj \<tau> (Proc (new_proc (s'@s))) = SProc (r,fr,pt,u) srp" using tau
+ by (auto simp:obj2sobj.simps cp2sproc.simps pct_def clone_type_unchange
+ split:option.splits)
+ moreover have "source_dir \<tau> f = Some sd" using vs_tau etype tau
+ by (auto simp:source_dir_simps obj2sobj.simps split:option.splits if_splits)
+ ultimately show ?thesis using valid ts'_exec2(5) ts'_exec2(6) ev
+ by (auto simp:cp2sproc_exec obj2sobj.simps split:option.splits)
+ qed moreover
+ have "Proc (new_proc (s'@s)) \<in> tainted (ev # \<tau>)"
+ proof-
+ have "Proc p \<in> tainted (s' @ s)" using TP vds's nodels'
+ by (drule_tac s = s' in t_remain_app, auto)
+ hence "Proc (new_proc (s'@s)) \<in> tainted \<tau>" using TP tau vs_tau
+ by (auto intro:t_clone)
+ thus ?thesis using ev valid
+ by (drule_tac t_remain, auto dest:valid_os)
+ qed moreover
+ have "no_del_event (ev # \<tau>)" using ev tau nodels' by simp
+ moreover have "initp_intact (ev#\<tau>)" using ev tau intacts' valid
+ by (simp add:initp_intact_I_exec)
+ ultimately show ?case
+ by (rule_tac x = "Proc (new_proc (s'@s))" in exI, rule_tac x = "ev#\<tau>" in exI, auto)
+next
+ case (ts'_cfd r fr pt u srp t sd srf t')
+ then obtain p s where TP: "(Proc p) \<in> tainted s"
+ and "valid s \<and> p \<in> current_procs s \<and> no_del_event s \<and> initp_intact s \<and>
+ obj2sobj s (Proc p) = SProc (r,fr,pt,u) srp"
+ apply (clarsimp, frule_tac obj2sobj_proc)
+ by (frule tainted_is_valid, frule tainted_is_current, auto)
+ with ts'_cfd(3) obtain pf s' where vds': "valid (s' @ s)"
+ and SF: "obj2sobj (s'@s) (File pf) = SFile (t, sd) srf"
+ and nodels': "no_del_event (s'@s)"
+ and intacts': "initp_intact (s'@s)"
+ and SP: "obj2sobj (s'@s) (Proc p) = SProc (r,fr,pt,u) srp"
+ and exp: "p \<in> current_procs (s' @ s)"
+ and exf: "pf \<in> current_files (s' @ s)"
+ apply (drule_tac s' =s and obj' = "Proc p" in all_sobjs_E0, auto)
+ apply (frule_tac obj = "Proc p" in nodel_tainted_exists, simp)
+ by (frule obj2sobj_file, clarsimp)
+ obtain e \<tau> where ev: "e = CreateFile p (new_childf pf \<tau>)"
+ and tau: "\<tau> = (s' @ s)" by auto
+
+ have valid: "valid (e# \<tau>)"
+ proof-
+ have "os_grant \<tau> e"
+ using ev tau exp exf by (simp add:ncf_notin_curf ncf_parent)
+ moreover have "rc_grant \<tau> e"
+ using ev tau ts'_cfd(4,5,6) SP SF
+ by (auto simp:etype_of_file_def cp2sproc.simps ncf_parent obj2sobj.simps
+ split:if_splits option.splits t_rc_file_type.splits)
+ ultimately show ?thesis using vds' tau
+ by (rule_tac vs_step, simp+)
+ qed moreover
+ have nodel: "no_del_event (e#\<tau>)" using nodels' tau ev by simp moreover
+ have "obj2sobj (e#\<tau>) (File (new_childf pf \<tau>)) = SFile (t', sd) None"
+ proof-
+ have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = Some t'"
+ using ev tau SF SP ts'_cfd(4)
+ by (auto simp:obj2sobj.simps etype_of_file_def cp2sproc.simps
+ split:option.splits if_splits intro!:etype_aux_prop4)
+ moreover have "source_dir (e#\<tau>) (new_childf pf \<tau>) = Some sd"
+ using ev tau SF SP valid ncf_parent
+ by (auto simp:source_dir_simps obj2sobj.simps cp2sproc.simps
+ split:if_splits option.splits)
+ ultimately show ?thesis using nodel ncf_notin_curf[where s = \<tau>]
+ nodel_imp_exists[where obj = "File (new_childf pf \<tau>)" and s =\<tau>]
+ by (auto simp:obj2sobj.simps dest:no_del_event_cons_D)
+ qed moreover
+ have "initp_intact (e#\<tau>)" using ev tau intacts' valid nodels'
+ by (auto intro!:initp_intact_I_others) moreover
+ have "File (new_childf pf \<tau>) \<in> tainted (e#\<tau>)"
+ proof-
+ have "Proc p \<in> tainted \<tau>" using nodel vds' TP ev tau
+ by (drule_tac s = "s'" and s' = s in t_remain_app, auto)
+ thus ?thesis using ev tau valid by (auto intro:t_cfile)
+ qed
+ ultimately show ?case using tau ev
+ apply (rule_tac x = "File (new_childf pf \<tau>)" in exI)
+ by (rule_tac x = "e#\<tau>" in exI, auto)
+next
+ case (ts'_cfd' r fr pt u srp t sd srf)
+ then obtain p s where TP: "(Proc p) \<in> tainted s"
+ and "valid s \<and> p \<in> current_procs s \<and> no_del_event s \<and> initp_intact s \<and>
+ obj2sobj s (Proc p) = SProc (r,fr,pt,u) srp"
+ apply (clarsimp, frule_tac obj2sobj_proc)
+ by (frule tainted_is_valid, frule tainted_is_current, auto)
+ with ts'_cfd'(3) obtain pf s' where vds': "valid (s' @ s)"
+ and SF: "obj2sobj (s'@s) (File pf) = SFile (t, sd) srf"
+ and nodels': "no_del_event (s'@s)"
+ and intacts': "initp_intact (s'@s)"
+ and SP: "obj2sobj (s'@s) (Proc p) = SProc (r,fr,pt,u) srp"
+ and exp: "p \<in> current_procs (s' @ s)"
+ and exf: "pf \<in> current_files (s' @ s)"
+ apply (drule_tac s' =s and obj' = "Proc p" in all_sobjs_E0, auto)
+ apply (frule_tac obj = "Proc p" in nodel_tainted_exists, simp)
+ by (frule obj2sobj_file, clarsimp)
+ obtain e \<tau> where ev: "e = CreateFile p (new_childf pf \<tau>)"
+ and tau: "\<tau> = (s' @ s)" by auto
+
+ have valid: "valid (e# \<tau>)"
+ proof-
+ have "os_grant \<tau> e"
+ using ev tau exp exf by (simp add:ncf_notin_curf ncf_parent)
+ moreover have "rc_grant \<tau> e"
+ using ev tau ts'_cfd'(4,5) SP SF
+ by (auto simp:etype_of_file_def cp2sproc.simps ncf_parent obj2sobj.simps
+ split:if_splits option.splits t_rc_file_type.splits)
+ ultimately show ?thesis using vds' tau
+ by (rule_tac vs_step, simp+)
+ qed moreover
+ have nodel: "no_del_event (e#\<tau>)" using nodels' tau ev by simp moreover
+ have "obj2sobj (e#\<tau>) (File (new_childf pf \<tau>)) = SFile (t, sd) None"
+ proof-
+ have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = Some t"
+ proof-
+ have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = etype_of_file \<tau> pf"
+ using ev tau SP ts'_cfd'(4)
+ by (auto simp:obj2sobj.simps ncf_parent etype_of_file_def cp2sproc.simps
+ split:option.splits intro!:etype_aux_prop3)
+ thus ?thesis using SF tau ev
+ by (auto simp:obj2sobj.simps split:option.splits if_splits)
+ qed
+ moreover have "source_dir (e#\<tau>) (new_childf pf \<tau>) = Some sd"
+ using ev tau SF SP valid ncf_parent
+ by (auto simp:source_dir_simps obj2sobj.simps cp2sproc.simps
+ split:if_splits option.splits)
+ ultimately show ?thesis using nodel ncf_notin_curf[where s = \<tau>]
+ nodel_imp_exists[where obj = "File (new_childf pf \<tau>)" and s =\<tau>]
+ by (auto simp:obj2sobj.simps dest:no_del_event_cons_D)
+ qed moreover
+ have "initp_intact (e#\<tau>)" using ev tau intacts' valid nodels'
+ by (auto intro!:initp_intact_I_others) moreover
+ have "File (new_childf pf \<tau>) \<in> tainted (e#\<tau>)"
+ proof-
+ have "Proc p \<in> tainted \<tau>" using nodel vds' TP ev tau
+ by (drule_tac s = "s'" and s' = s in t_remain_app, auto)
+ thus ?thesis using ev tau valid by (auto intro:t_cfile)
+ qed
+ ultimately show ?case using tau ev
+ apply (rule_tac x = "File (new_childf pf \<tau>)" in exI)
+ by (rule_tac x = "e#\<tau>" in exI, auto)
+next
+ case (ts'_cipc r fr pt u srp)
+ then obtain p s where TP: "(Proc p) \<in> tainted s"
+ and vds: "valid s" and exp: "p \<in> current_procs s"
+ and nodels: "no_del_event s" and intacts: "initp_intact s"
+ and SP: "obj2sobj s (Proc p) = SProc (r,fr,pt,u) srp"
+ apply (clarsimp, frule_tac obj2sobj_proc)
+ by (frule tainted_is_valid, frule tainted_is_current, auto)
+ obtain e where ev: "e = CreateIPC p (new_ipc s)" by simp
+
+ have valid: "valid (e # s)"
+ proof-
+ have "os_grant s e"
+ using ev exp by (simp)
+ moreover have "rc_grant s e"
+ using ev ts'_cipc(3) SP
+ by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits)
+ ultimately show ?thesis using vds
+ by (rule_tac vs_step, simp+)
+ qed moreover
+ have nodel: "no_del_event (e#s)" using nodels ev by simp moreover
+ have "initp_intact (e#s)" using ev intacts valid nodels
+ by (auto intro!:initp_intact_I_others) moreover
+ have "IPC (new_ipc s) \<in> tainted (e#s)" using TP ev valid
+ by (auto intro:t_cipc) moreover
+ have "obj2sobj (e#s) (IPC (new_ipc s)) = SIPC (default_ipc_create_type r) None"
+ using ev SP nodel nodel_imp_exists[where obj = "IPC (new_ipc s)" and s=s]
+ by (auto simp:obj2sobj.simps ni_notin_curi cp2sproc.simps
+ split:option.splits dest:no_del_event_cons_D)
+ ultimately show ?case using ev
+ apply (rule_tac x = "IPC (new_ipc s)" in exI)
+ by (rule_tac x = "e # s" in exI, auto)
+next
+ case (ts'_read t sd srf r fr pt u srp)
+ then obtain f s where TF: "(File f) \<in> tainted s" and vds: "valid s"
+ and "f \<in> current_files s \<and> obj2sobj s (File f) = SFile (t, sd) srf \<and>
+ no_del_event s \<and> initp_intact s"
+ apply (clarsimp, frule_tac obj2sobj_file)
+ by (frule tainted_is_valid, frule tainted_is_current, auto)
+ with ts'_read(3) obtain p s' where vds': "valid (s' @ s)"
+ and SF: "obj2sobj (s'@s) (File f) = SFile (t, sd) srf"
+ and nodels': "no_del_event (s'@s)"
+ and intacts': "initp_intact (s'@s)"
+ and SP: "obj2sobj (s'@s) (Proc p) = SProc (r,fr,pt,u) srp"
+ and exp: "p \<in> current_procs (s' @ s)"
+ and exf: "f \<in> current_files (s' @ s)"
+ apply (drule_tac s' =s and obj' = "File f" in all_sobjs_E0, auto)
+ apply (frule_tac obj = "File f" in nodel_tainted_exists, simp)
+ by (frule obj2sobj_proc, clarsimp)
+ obtain e \<tau> where ev: "e = ReadFile p f" and tau: "\<tau> = s' @ s" by auto
+
+ have valid: "valid (e # \<tau>)"
+ proof-
+ have "os_grant \<tau> e"
+ using ev tau by (simp add:exf exp)
+ moreover have "rc_grant \<tau> e"
+ using ev tau ts'_read(4) SP SF
+ by (auto simp:etype_of_file_def cp2sproc.simps obj2sobj.simps
+ split:if_splits option.splits)
+ ultimately show ?thesis using vds' tau
+ by (rule_tac vs_step, simp+)
+ qed moreover
+ have "obj2sobj (e # \<tau>) (Proc p) = SProc (r, fr, pt, u) srp" using valid tau ev SP
+ by (auto simp:obj2sobj.simps cp2sproc_simps split:option.splits)
+ moreover have "Proc p \<in> tainted (e # \<tau>)"
+ proof-
+ have "(File f) \<in> tainted \<tau>" using TF nodels' tau vds'
+ by (drule_tac s = "s'" in t_remain_app,auto)
+ thus ?thesis using ev valid
+ by (drule_tac t_read, simp+)
+ qed moreover
+ have "no_del_event (e # \<tau>)" using ev tau nodels' by simp moreover
+ have "initp_intact (e#\<tau>)" using ev intacts' valid nodels' tau
+ by (auto intro!:initp_intact_I_others)
+ ultimately show ?case
+ by (rule_tac x = "Proc p" in exI, rule_tac x = "e#\<tau>" in exI, auto)
+next
+ case (ts'_write r fr pt u srp t sd srf)
+ then obtain p s where TP: "(Proc p) \<in> tainted s"
+ and "valid s \<and> p \<in> current_procs s \<and> no_del_event s \<and> initp_intact s \<and>
+ obj2sobj s (Proc p) = SProc (r,fr,pt,u) srp"
+ apply (clarsimp, frule_tac obj2sobj_proc)
+ by (frule tainted_is_valid, frule tainted_is_current, auto)
+ with ts'_write(3) obtain f s' where vds': "valid (s' @ s)"
+ and SF: "obj2sobj (s'@s) (File f) = SFile (t, sd) srf"
+ and nodels': "no_del_event (s'@s)"
+ and intacts': "initp_intact (s'@s)"
+ and SP: "obj2sobj (s'@s) (Proc p) = SProc (r,fr,pt,u) srp"
+ and exp: "p \<in> current_procs (s' @ s)"
+ and exf: "f \<in> current_files (s' @ s)"
+ apply (drule_tac s' =s and obj' = "Proc p" in all_sobjs_E0, auto)
+ apply (frule_tac obj = "Proc p" in nodel_tainted_exists, simp)
+ by (frule obj2sobj_file, clarsimp)
+ obtain e \<tau> where ev: "e = WriteFile p f" and tau: "\<tau> = (s' @ s)" by auto
+
+ have valid: "valid (e# \<tau>)"
+ proof-
+ have "os_grant \<tau> e"
+ using ev tau exp exf by simp
+ moreover have "rc_grant \<tau> e"
+ using ev tau ts'_write(4) SP SF
+ by (auto simp:etype_of_file_def cp2sproc.simps obj2sobj.simps
+ split:if_splits option.splits)
+ ultimately show ?thesis using vds' tau
+ by (rule_tac vs_step, simp+)
+ qed moreover
+ have nodel: "no_del_event (e#\<tau>)" using nodels' tau ev by simp moreover
+ have "obj2sobj (e#\<tau>) (File f) = SFile (t, sd) srf"
+ using tau ev SF valid
+ by (auto simp:obj2sobj.simps source_dir_simps etype_of_file_def
+ split:option.splits if_splits)
+ moreover have "initp_intact (e#\<tau>)" using ev intacts' valid nodels' tau
+ by (auto intro!:initp_intact_I_others) moreover
+ have "File f \<in> tainted (e#\<tau>)"
+ proof-
+ have "Proc p \<in> tainted \<tau>" using nodel vds' TP ev tau
+ by (drule_tac s = "s'" and s' = s in t_remain_app, auto)
+ thus ?thesis using ev tau valid by (auto intro:t_write)
+ qed
+ ultimately show ?case using tau ev
+ by (rule_tac x = "File f" in exI, rule_tac x = "e#\<tau>" in exI, auto)
+next
+ case (ts'_recv t sri r fr pt u srp)
+ then obtain i s where TI: "(IPC i) \<in> tainted s" and vds: "valid s"
+ and "i \<in> current_ipcs s \<and> obj2sobj s (IPC i) = SIPC t sri \<and>
+ no_del_event s \<and> initp_intact s"
+ apply (clarsimp, frule_tac obj2sobj_ipc)
+ by (frule tainted_is_valid, frule tainted_is_current, auto)
+ with ts'_recv(3) obtain p s' where vds': "valid (s' @ s)"
+ and SI: "obj2sobj (s'@s) (IPC i) = SIPC t sri"
+ and nodels': "no_del_event (s'@s)"
+ and intacts': "initp_intact (s'@s)"
+ and SP: "obj2sobj (s'@s) (Proc p) = SProc (r,fr,pt,u) srp"
+ and exp: "p \<in> current_procs (s' @ s)"
+ and exi: "i \<in> current_ipcs (s' @ s)"
+ apply (drule_tac s' =s and obj' = "IPC i" in all_sobjs_E0, auto)
+ apply (frule_tac obj = "IPC i" in nodel_tainted_exists, simp)
+ by (frule obj2sobj_proc, clarsimp)
+ obtain e \<tau> where ev: "e = Recv p i" and tau: "\<tau> = s' @ s" by auto
+
+ have valid: "valid (e # \<tau>)"
+ proof-
+ have "os_grant \<tau> e"
+ using ev tau by (simp add:exi exp)
+ moreover have "rc_grant \<tau> e"
+ using ev tau ts'_recv(4) SP SI
+ by (auto simp:cp2sproc.simps obj2sobj.simps
+ split:if_splits option.splits)
+ ultimately show ?thesis using vds' tau
+ by (rule_tac vs_step, simp+)
+ qed moreover
+ have "obj2sobj (e # \<tau>) (Proc p) = SProc (r, fr, pt, u) srp" using valid tau ev SP
+ by (auto simp:obj2sobj.simps cp2sproc_simps split:option.splits)
+ moreover have "Proc p \<in> tainted (e # \<tau>)"
+ proof-
+ have "(IPC i) \<in> tainted \<tau>" using TI nodels' tau vds'
+ by (drule_tac s = "s'" in t_remain_app,auto)
+ thus ?thesis using ev valid
+ by (drule_tac t_recv, simp+)
+ qed moreover
+ have "no_del_event (e # \<tau>)" using ev tau nodels' by simp
+ moreover have "initp_intact (e#\<tau>)" using ev intacts' valid nodels' tau
+ by (auto intro!:initp_intact_I_others)
+ ultimately show ?case
+ by (rule_tac x = "Proc p" in exI, rule_tac x = "e#\<tau>" in exI, auto)
+next
+ case (ts'_send r fr pt u srp t sri)
+ then obtain p s where TP: "(Proc p) \<in> tainted s"
+ and "valid s \<and> p \<in> current_procs s \<and> no_del_event s \<and> initp_intact s \<and>
+ obj2sobj s (Proc p) = SProc (r,fr,pt,u) srp"
+ apply (clarsimp, frule_tac obj2sobj_proc)
+ by (frule tainted_is_valid, frule tainted_is_current, auto)
+ with ts'_send(3) obtain i s' where vds': "valid (s' @ s)"
+ and SI: "obj2sobj (s'@s) (IPC i) = SIPC t sri"
+ and nodels': "no_del_event (s'@s)"
+ and intacts': "initp_intact (s'@s)"
+ and SP: "obj2sobj (s'@s) (Proc p) = SProc (r,fr,pt,u) srp"
+ and exp: "p \<in> current_procs (s' @ s)"
+ and exi: "i \<in> current_ipcs (s' @ s)"
+ apply (drule_tac s' =s and obj' = "Proc p" in all_sobjs_E0, auto)
+ apply (frule_tac obj = "Proc p" in nodel_tainted_exists, simp)
+ by (frule obj2sobj_ipc, clarsimp)
+ obtain e \<tau> where ev: "e = Send p i" and tau: "\<tau> = (s' @ s)" by auto
+
+ have valid: "valid (e# \<tau>)"
+ proof-
+ have "os_grant \<tau> e"
+ using ev tau exp exi by simp
+ moreover have "rc_grant \<tau> e"
+ using ev tau ts'_send(4) SP SI
+ by (auto simp:cp2sproc.simps obj2sobj.simps
+ split:if_splits option.splits)
+ ultimately show ?thesis using vds' tau
+ by (rule_tac vs_step, simp+)
+ qed moreover
+ have nodel: "no_del_event (e#\<tau>)" using nodels' tau ev by simp moreover
+ have "obj2sobj (e#\<tau>) (IPC i) = SIPC t sri"
+ using tau ev SI valid
+ by (auto simp:obj2sobj.simps split:option.splits if_splits)
+ moreover have "initp_intact (e#\<tau>)" using ev intacts' valid nodels' tau
+ by (auto intro!:initp_intact_I_others) moreover
+ have "IPC i \<in> tainted (e#\<tau>)"
+ proof-
+ have "Proc p \<in> tainted \<tau>" using nodel vds' TP ev tau
+ by (drule_tac s = "s'" and s' = s in t_remain_app, auto)
+ thus ?thesis using ev tau valid by (auto intro:t_send)
+ qed
+ ultimately show ?case using tau ev
+ by (rule_tac x = "IPC i" in exI, rule_tac x = "e#\<tau>" in exI, auto)
+next
+ case (ts'_crole r fr pt u srp r')
+ then obtain p s where exp: "p \<in> current_procs s"
+ and TP: "(Proc p) \<in> tainted s" and vds: "valid s" and nodels: "no_del_event s"
+ and SP: "obj2sobj s (Proc p) = SProc (r, fr, pt, u) srp"
+ and intacts: "initp_intact s"
+ apply (clarsimp, frule_tac obj2sobj_proc)
+ by (frule tainted_is_valid, frule tainted_is_current, auto)
+ obtain e \<tau> where ev: "e = ChangeRole (new_proc s) r'"
+ and tau: "\<tau> = Clone p (new_proc s) # s" by auto
+ hence vs_tau:"valid \<tau>" using exp vds by (auto intro:clone_event_no_limit)
+
+ have valid: "valid (e # \<tau>)"
+ proof-
+ have "os_grant \<tau> e"
+ using ev tau exp by simp
+ moreover have "rc_grant \<tau> e"
+ using ev tau ts'_crole(3) SP
+ by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits)
+ ultimately show ?thesis using vs_tau
+ by (erule_tac vs_step, simp+)
+ qed moreover
+ have "obj2sobj (e # \<tau>) (Proc (new_proc s)) = SProc (r',fr,pt,u) srp"
+ proof-
+ have "obj2sobj \<tau> (Proc (new_proc s)) = SProc (r,fr,pt,u) srp" using SP tau vs_tau
+ by (auto split:option.splits simp:cp2sproc_simps' obj2sobj.simps)
+ thus ?thesis using valid ev
+ by (auto simp:cp2sproc_crole obj2sobj.simps split:option.splits)
+ qed moreover
+ have "Proc (new_proc s) \<in> tainted (e # \<tau>)"
+ proof-
+ have "(Proc (new_proc s)) \<in> tainted \<tau>" using TP tau vs_tau
+ by (auto intro!:t_clone)
+ thus ?thesis using ev valid
+ by (drule_tac t_remain, auto dest:valid_os)
+ qed moreover
+ have "no_del_event (e # \<tau>)" using ev tau nodels by simp
+ moreover have "initp_intact (e#\<tau>)" using ev intacts valid nodels tau
+ by (simp add:initp_intact_I_crole)
+ ultimately show ?case
+ by (rule_tac x = "Proc (new_proc s)" in exI, rule_tac x = "e#\<tau>" in exI, auto)
+next
+ case (ts'_chown r fr pt u srp u' nr)
+ then obtain p s where exp: "p \<in> current_procs s"
+ and TP: "(Proc p) \<in> tainted s" and vds: "valid s" and nodels: "no_del_event s"
+ and SP: "obj2sobj s (Proc p) = SProc (r, fr, pt, u) srp"
+ and intacts: "initp_intact s"
+ apply (clarsimp, frule_tac obj2sobj_proc)
+ by (frule tainted_is_valid, frule tainted_is_current, auto)
+ obtain e \<tau> where ev: "e = ChangeOwner (new_proc s) u'"
+ and tau: "\<tau> = Clone p (new_proc s) # s" by auto
+ hence vs_tau:"valid \<tau>" using exp vds by (auto intro:clone_event_no_limit)
+
+ have valid: "valid (e # \<tau>)"
+ proof-
+ have "os_grant \<tau> e"
+ using ev tau exp ts'_chown(3) by simp
+ moreover have "rc_grant \<tau> e"
+ using ev tau ts'_chown(5) SP
+ by (auto simp:cp2sproc.simps obj2sobj.simps pct_def clone_type_unchange
+ split:option.splits t_rc_proc_type.splits)
+ (* here is another place of no_limit of clone event assumption *)
+ ultimately show ?thesis using vs_tau
+ by (erule_tac vs_step, simp+)
+ qed moreover
+ have "obj2sobj (e # \<tau>) (Proc (new_proc s)) = SProc (nr, fr, chown_type_aux r nr pt, u') srp"
+ proof-
+ have "obj2sobj \<tau> (Proc (new_proc s)) = SProc (r,fr,pt,u) srp" using SP tau vs_tau
+ by (auto split:option.splits simp:cp2sproc_simps' obj2sobj.simps)
+ thus ?thesis using valid ev ts'_chown(4)
+ by (auto simp:cp2sproc_chown obj2sobj.simps split:option.splits)
+ qed moreover
+ have "Proc (new_proc s) \<in> tainted (e # \<tau>)"
+ proof-
+ have "Proc (new_proc s) \<in> tainted \<tau>" using TP tau vs_tau exp
+ by (auto intro!:t_clone)
+ thus ?thesis using ev valid
+ by (drule_tac t_remain, auto dest:valid_os)
+ qed moreover
+ have "no_del_event (e # \<tau>)" using ev tau nodels by simp
+ moreover have "initp_intact (e#\<tau>)" using ev intacts valid nodels tau
+ by (simp add:initp_intact_I_chown)
+ ultimately show ?case
+ by (rule_tac x = "Proc (new_proc s)" in exI, rule_tac x = "e#\<tau>" in exI, auto)
+qed
+
+lemma ts2t:
+ "sobj \<in> tainted_s' \<Longrightarrow> \<exists> obj s. obj2sobj s obj = sobj \<and> obj \<in> tainted s \<and>
+ sobj_source_eq_obj sobj obj \<and> no_del_event s \<and>
+ initp_intact_but s sobj"
+proof (induct rule:tainted_s'.induct)
+ case (ts'_init obj)
+ hence ex: "exists [] obj"
+ apply (drule_tac seeds_in_init)
+ by (case_tac obj, simp+)
+ have "obj2sobj [] obj = init_obj2sobj obj" using ex
+ by (simp add:obj2sobj_nil_init)
+ moreover have "obj \<in> tainted []" using ts'_init by (simp add:t_init)
+ moreover have "sobj_source_eq_obj (init_obj2sobj obj) obj" using ex
+ apply (frule_tac init_obj_has_sobj)
+ apply (case_tac "init_obj2sobj obj", case_tac[!] obj)
+ by (auto split:option.splits)
+ ultimately show ?case
+ apply (rule_tac x = obj in exI, rule_tac x = "[]" in exI)
+ by (auto simp:initp_intact_but_nil)
+next
+ case (ts'_exec1 t sd srf r fr pt u srp r' fr')
+ then obtain f s where "sobj_source_eq_obj (SFile (t, sd) srf) (File f)"
+ and TF: "(File f) \<in> tainted s" and vds: "valid s" and "f \<in> current_files s"
+ and "obj2sobj s (File f) = SFile (t, sd) srf \<and> no_del_event s \<and> initp_intact s"
+ apply (clarsimp, frule_tac obj2sobj_file)
+ by (frule tainted_is_valid, frule tainted_is_current, auto)
+ with ts'_exec1(3) obtain p s' where vds's: "valid (s' @ s)"
+ and etype: "obj2sobj (s'@s) (File f) = SFile (t, sd) srf"
+ and nodels': "no_del_event (s'@s)"
+ and intacts': "initp_intact_but (s'@s) (SProc (r,fr,pt,u) srp)"
+ and ISP: "obj2sobj (s'@s) (Proc p) = SProc (r,fr,pt,u) srp"
+ and exp: "p \<in> current_procs (s' @ s)"
+ and exf: "f \<in> current_files (s' @ s)"
+ and sreq: "sobj_source_eq_obj (SProc (r,fr,pt,u) srp) (Proc p)"
+ apply (drule_tac s' =s and obj' = "File f" in all_sobjs_E2, auto)
+ apply (frule_tac obj = "File f" in nodel_tainted_exists, simp)
+ by (frule obj2sobj_proc, clarsimp)
+ from vds's ISP sreq exp have srpeq: "srp = Some p" by (simp add:proc_source_eq_prop)
+ with exp vds's ISP have initp: "p \<in> init_processes"
+ by (auto simp:obj2sobj.simps dest:source_proc_in_init split:option.splits)
+ obtain ev \<tau> where ev: "ev = Execute p f"
+ and tau: "\<tau> = Clone p (new_proc (s'@s)) # (s' @ s)" by auto
+ hence vs_tau:"valid \<tau>" using exp vds's by (auto intro:clone_event_no_limit)
+
+ have valid: "valid (ev # \<tau>)"
+ proof-
+ have "os_grant \<tau> ev"
+ using ev tau by (simp add:exf exp)
+ moreover have "rc_grant \<tau> ev"
+ using ev tau ts'_exec1 ISP etype
+ by (auto simp:etype_of_file_def cp2sproc.simps obj2sobj.simps
+ split:if_splits option.splits)
+ ultimately show ?thesis using vs_tau
+ by (erule_tac vs_step, simp+)
+ qed moreover
+ have "obj2sobj (ev # \<tau>) (Proc p) = SProc (r', fr', exec_type_aux r pt, u) srp"
+ proof-
+ have "obj2sobj \<tau> (Proc p) = SProc (r,fr,pt,u) srp" using ISP tau vs_tau
+ by (auto split:option.splits simp:cp2sproc_simps' obj2sobj.simps)
+ moreover have "source_dir \<tau> f = Some sd" using vs_tau etype tau
+ by (auto simp:obj2sobj.simps source_dir_simps split:option.splits if_splits)
+ ultimately show ?thesis using valid ts'_exec1(5) ts'_exec1(6) ev
+ by (auto simp:cp2sproc_exec obj2sobj.simps split:option.splits)
+ qed moreover
+ have "Proc p \<in> tainted (ev # \<tau>)"
+ proof-
+ have "(File f) \<in> tainted \<tau>" using TF nodels' tau vs_tau
+ by (drule_tac s = "Clone p (new_proc (s' @ s)) # s'" in t_remain_app,auto)
+ thus ?thesis using ev valid
+ by (drule_tac t_exec, simp+)
+ qed moreover
+ have "no_del_event (ev # \<tau>)" using ev tau nodels' by simp
+ moreover have "initp_intact_but (ev#\<tau>) (SProc (r', fr', exec_type_aux r pt, u) srp)"
+ using ev tau nodels' intacts' srpeq valid initp
+ by (simp, rule_tac initp_intact_butp_I_exec, simp_all)
+ moreover have "sobj_source_eq_obj (SProc (r', fr', exec_type_aux r pt, u) srp) (Proc p)"
+ using sreq by (case_tac srp, simp+)
+ ultimately show ?case
+ by (rule_tac x = "Proc p" in exI, rule_tac x = "ev#\<tau>" in exI, auto)
+next
+ case (ts'_exec2 r fr pt u srp t sd srf r' fr')
+ then obtain p s where sreq:"sobj_source_eq_obj (SProc (r, fr, pt, u) srp) (Proc p)"
+ and TP: "(Proc p) \<in> tainted s" and vds: "valid s" and "p \<in> current_procs s"
+ and "obj2sobj s (Proc p) = SProc (r, fr, pt, u) srp \<and> no_del_event s \<and>
+ initp_intact_but s (SProc (r, fr, pt, u) srp)"
+ apply (clarsimp, frule_tac obj2sobj_proc)
+ by (frule tainted_is_valid, frule tainted_is_current, auto)
+ with ts'_exec2(3) obtain f s' where vds's: "valid (s' @ s)"
+ and etype: "obj2sobj (s'@s) (File f) = SFile (t, sd) srf"
+ and nodels': "no_del_event (s'@s)"
+ and intacts': "initp_intact_but (s'@s) (SProc (r,fr,pt,u) srp)"
+ and ISP: "obj2sobj (s'@s) (Proc p) = SProc (r,fr,pt,u) srp"
+ and exp: "p \<in> current_procs (s' @ s)"
+ and exf: "f \<in> current_files (s' @ s)"
+ apply (drule_tac s' =s and obj' = "Proc p" in all_sobjs_E1, auto)
+ apply (frule_tac obj = "Proc p" in nodel_tainted_exists, simp)
+ by (frule obj2sobj_file, clarsimp)
+ from vds's ISP sreq exp have srpeq: "srp = Some p" by (simp add:proc_source_eq_prop)
+ with exp vds's ISP have initp: "p \<in> init_processes"
+ by (auto simp:obj2sobj.simps dest:source_proc_in_init split:option.splits)
+ obtain ev \<tau> where ev: "ev = Execute p f"
+ and tau: "\<tau> = Clone p (new_proc (s'@s)) # (s' @ s)" by auto
+ hence vs_tau:"valid \<tau>" using exp vds's by (auto intro:clone_event_no_limit)
+
+ have valid: "valid (ev # \<tau>)"
+ proof-
+ have "os_grant \<tau> ev"
+ using ev tau by (simp add:exf exp)
+ moreover have "rc_grant \<tau> ev"
+ using ev tau ts'_exec2 ISP etype
+ by (auto simp:etype_of_file_def cp2sproc.simps obj2sobj.simps
+ split:if_splits option.splits)
+ ultimately show ?thesis using vs_tau
+ by (erule_tac vs_step, simp+)
+ qed moreover
+ have "obj2sobj (ev # \<tau>) (Proc p) = SProc (r', fr', exec_type_aux r pt, u) srp"
+ proof-
+ have "obj2sobj \<tau> (Proc p) = SProc (r,fr,pt,u) srp" using ISP tau vs_tau
+ by (auto split:option.splits simp:cp2sproc_simps' obj2sobj.simps)
+ moreover have "source_dir \<tau> f = Some sd" using vs_tau etype tau
+ by (auto simp:source_dir_simps obj2sobj.simps split:option.splits if_splits)
+ ultimately show ?thesis using valid ts'_exec2(5) ts'_exec2(6) ev
+ by (auto simp:cp2sproc_exec obj2sobj.simps split:option.splits)
+ qed moreover
+ have "Proc p \<in> tainted (ev # \<tau>)"
+ proof-
+ have "(Proc p) \<in> tainted \<tau>" using TP nodels' tau vs_tau
+ by (drule_tac s = "Clone p (new_proc (s' @ s)) # s'" in t_remain_app,auto)
+ thus ?thesis using ev valid
+ by (drule_tac t_remain, auto dest:valid_os)
+ qed moreover
+ have "no_del_event (ev # \<tau>)" using ev tau nodels' by simp
+ moreover have "initp_intact_but (ev#\<tau>) (SProc (r', fr', exec_type_aux r pt, u) srp)"
+ using ev tau nodels' intacts' srpeq valid initp
+ by (simp, rule_tac initp_intact_butp_I_exec, simp_all)
+ moreover have "sobj_source_eq_obj (SProc (r', fr', exec_type_aux r pt, u) srp) (Proc p)"
+ using sreq by (case_tac srp, simp+)
+ ultimately show ?case
+ by (rule_tac x = "Proc p" in exI, rule_tac x = "ev#\<tau>" in exI, auto)
+next
+ case (ts'_cfd r fr pt u srp t sd srf t')
+ from ts'_cfd(1) obtain p s where TP: "(Proc p) \<in> tainted s"
+ and "valid s \<and> p \<in> current_procs s \<and> no_del_event s \<and> initp_intact s \<and>
+ obj2sobj s (Proc p) = SProc (r,fr,pt,u) srp"
+ apply (drule_tac ts2t_intact, clarsimp, frule_tac obj2sobj_proc)
+ by (frule tainted_is_valid, frule tainted_is_current, auto)
+ with ts'_cfd(3) obtain pf s' where vds': "valid (s' @ s)"
+ and SF: "obj2sobj (s'@s) (File pf) = SFile (t, sd) srf"
+ and nodels': "no_del_event (s'@s)"
+ and intacts': "initp_intact (s'@s)"
+ and SP: "obj2sobj (s'@s) (Proc p) = SProc (r,fr,pt,u) srp"
+ and exp: "p \<in> current_procs (s' @ s)"
+ and exf: "pf \<in> current_files (s' @ s)"
+ apply (drule_tac s' =s and obj' = "Proc p" in all_sobjs_E0, auto)
+ apply (frule_tac obj = "Proc p" in nodel_tainted_exists, simp)
+ by (frule obj2sobj_file, clarsimp)
+ obtain e \<tau> where ev: "e = CreateFile p (new_childf pf \<tau>)"
+ and tau: "\<tau> = (s' @ s)" by auto
+
+ have valid: "valid (e# \<tau>)"
+ proof-
+ have "os_grant \<tau> e"
+ using ev tau exp exf by (simp add:ncf_notin_curf ncf_parent)
+ moreover have "rc_grant \<tau> e"
+ using ev tau ts'_cfd(4,5,6) SP SF
+ by (auto simp:etype_of_file_def cp2sproc.simps ncf_parent obj2sobj.simps
+ split:if_splits option.splits t_rc_file_type.splits)
+ ultimately show ?thesis using vds' tau
+ by (rule_tac vs_step, simp+)
+ qed moreover
+ have nodel: "no_del_event (e#\<tau>)" using nodels' tau ev by simp moreover
+ have "obj2sobj (e#\<tau>) (File (new_childf pf \<tau>)) = SFile (t', sd) None"
+ proof-
+ have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = Some t'"
+ using ev tau SF SP ts'_cfd(4)
+ by (auto simp:obj2sobj.simps etype_of_file_def cp2sproc.simps
+ split:option.splits if_splits intro!:etype_aux_prop4)
+ moreover have "source_dir (e#\<tau>) (new_childf pf \<tau>) = Some sd"
+ using ev tau SF SP valid ncf_parent
+ by (auto simp:source_dir_simps obj2sobj.simps cp2sproc.simps
+ split:if_splits option.splits)
+ ultimately show ?thesis using nodel ncf_notin_curf[where s = \<tau>]
+ nodel_imp_exists[where obj = "File (new_childf pf \<tau>)" and s =\<tau>]
+ by (auto simp:obj2sobj.simps dest:no_del_event_cons_D)
+ qed moreover
+ have "initp_intact (e#\<tau>)" using ev intacts' valid nodels' tau
+ by (auto intro!:initp_intact_I_others) moreover
+ have "File (new_childf pf \<tau>) \<in> tainted (e#\<tau>)"
+ proof-
+ have "Proc p \<in> tainted \<tau>" using nodel vds' TP ev tau
+ by (drule_tac s = "s'" and s' = s in t_remain_app, auto)
+ thus ?thesis using ev tau valid by (auto intro:t_cfile)
+ qed
+ ultimately show ?case using tau ev
+ apply (rule_tac x = "File (new_childf pf \<tau>)" in exI)
+ by (rule_tac x = "e#\<tau>" in exI, auto)
+next
+ case (ts'_cfd' r fr pt u srp t sd srf)
+ from ts'_cfd'(1) obtain p s where TP: "(Proc p) \<in> tainted s"
+ and "valid s \<and> p \<in> current_procs s \<and> no_del_event s \<and> initp_intact s \<and>
+ obj2sobj s (Proc p) = SProc (r,fr,pt,u) srp"
+ apply (drule_tac ts2t_intact, clarsimp, frule_tac obj2sobj_proc)
+ by (frule tainted_is_valid, frule tainted_is_current, auto)
+ with ts'_cfd'(3) obtain pf s' where vds': "valid (s' @ s)"
+ and SF: "obj2sobj (s'@s) (File pf) = SFile (t, sd) srf"
+ and nodels': "no_del_event (s'@s)"
+ and intacts': "initp_intact (s'@s)"
+ and SP: "obj2sobj (s'@s) (Proc p) = SProc (r,fr,pt,u) srp"
+ and exp: "p \<in> current_procs (s' @ s)"
+ and exf: "pf \<in> current_files (s' @ s)"
+ apply (drule_tac s' =s and obj' = "Proc p" in all_sobjs_E0, auto)
+ apply (frule_tac obj = "Proc p" in nodel_tainted_exists, simp)
+ by (frule obj2sobj_file, clarsimp)
+ obtain e \<tau> where ev: "e = CreateFile p (new_childf pf \<tau>)"
+ and tau: "\<tau> = (s' @ s)" by auto
+
+ have valid: "valid (e# \<tau>)"
+ proof-
+ have "os_grant \<tau> e"
+ using ev tau exp exf by (simp add:ncf_notin_curf ncf_parent)
+ moreover have "rc_grant \<tau> e"
+ using ev tau ts'_cfd'(4,5) SP SF
+ by (auto simp:etype_of_file_def cp2sproc.simps ncf_parent obj2sobj.simps
+ split:if_splits option.splits t_rc_file_type.splits)
+ ultimately show ?thesis using vds' tau
+ by (rule_tac vs_step, simp+)
+ qed moreover
+ have nodel: "no_del_event (e#\<tau>)" using nodels' tau ev by simp moreover
+ have "obj2sobj (e#\<tau>) (File (new_childf pf \<tau>)) = SFile (t, sd) None"
+ proof-
+ have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = Some t"
+ proof-
+ have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = etype_of_file \<tau> pf"
+ using ev tau SP ts'_cfd'(4)
+ by (auto simp:obj2sobj.simps ncf_parent etype_of_file_def cp2sproc.simps
+ split:option.splits intro!:etype_aux_prop3)
+ thus ?thesis using SF tau ev
+ by (auto simp:obj2sobj.simps split:option.splits if_splits)
+ qed
+ moreover have "source_dir (e#\<tau>) (new_childf pf \<tau>) = Some sd"
+ using ev tau SF SP valid ncf_parent
+ by (auto simp:source_dir_simps obj2sobj.simps cp2sproc.simps
+ split:if_splits option.splits)
+ ultimately show ?thesis using nodel ncf_notin_curf[where s = \<tau>]
+ nodel_imp_exists[where obj = "File (new_childf pf \<tau>)" and s =\<tau>]
+ by (auto simp:obj2sobj.simps dest:no_del_event_cons_D)
+ qed moreover
+ have "initp_intact (e#\<tau>)" using ev intacts' valid nodels' tau
+ by (auto intro!:initp_intact_I_others) moreover
+ have "File (new_childf pf \<tau>) \<in> tainted (e#\<tau>)"
+ proof-
+ have "Proc p \<in> tainted \<tau>" using nodel vds' TP ev tau
+ by (drule_tac s = "s'" and s' = s in t_remain_app, auto)
+ thus ?thesis using ev tau valid by (auto intro:t_cfile)
+ qed
+ ultimately show ?case using tau ev
+ apply (rule_tac x = "File (new_childf pf \<tau>)" in exI)
+ by (rule_tac x = "e#\<tau>" in exI, auto)
+next
+ case (ts'_cipc r fr pt u srp)
+ from ts'_cipc(1) obtain p s where TP: "(Proc p) \<in> tainted s"
+ and vds: "valid s" and exp: "p \<in> current_procs s"
+ and nodels: "no_del_event s" and intacts: "initp_intact s"
+ and SP: "obj2sobj s (Proc p) = SProc (r,fr,pt,u) srp"
+ apply (drule_tac ts2t_intact, clarsimp, frule_tac obj2sobj_proc)
+ by (frule tainted_is_valid, frule tainted_is_current, auto)
+ obtain e where ev: "e = CreateIPC p (new_ipc s)" by simp
+
+ have valid: "valid (e # s)"
+ proof-
+ have "os_grant s e"
+ using ev exp by (simp)
+ moreover have "rc_grant s e"
+ using ev ts'_cipc(3) SP
+ by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits)
+ ultimately show ?thesis using vds
+ by (rule_tac vs_step, simp+)
+ qed moreover
+ have nodel: "no_del_event (e#s)" using nodels ev by simp moreover
+ have "initp_intact (e#s)" using ev intacts valid nodels
+ by (auto intro!:initp_intact_I_others) moreover
+ have "IPC (new_ipc s) \<in> tainted (e#s)" using TP ev valid
+ by (auto intro:t_cipc) moreover
+ have "obj2sobj (e#s) (IPC (new_ipc s)) = SIPC (default_ipc_create_type r) None"
+ using ev SP nodel nodel_imp_exists[where obj = "IPC (new_ipc s)" and s=s]
+ by (auto simp:obj2sobj.simps ni_notin_curi cp2sproc.simps
+ split:option.splits dest:no_del_event_cons_D)
+ ultimately show ?case using ev
+ apply (rule_tac x = "IPC (new_ipc s)" in exI)
+ by (rule_tac x = "e # s" in exI, auto)
+next
+ case (ts'_read t sd srf r fr pt u srp)
+ then obtain f s where "sobj_source_eq_obj (SFile (t, sd) srf) (File f)"
+ and TF: "(File f) \<in> tainted s" and vds: "valid s" and "f \<in> current_files s"
+ and "obj2sobj s (File f) = SFile (t, sd) srf \<and> no_del_event s \<and> initp_intact s"
+ apply (clarsimp, frule_tac obj2sobj_file)
+ by (frule tainted_is_valid, frule tainted_is_current, auto)
+ with ts'_read(3) obtain p s' where vds': "valid (s' @ s)"
+ and SF: "obj2sobj (s'@s) (File f) = SFile (t, sd) srf"
+ and nodels': "no_del_event (s'@s)"
+ and intacts': "initp_intact_but (s'@s) (SProc (r,fr,pt,u) srp)"
+ and SP: "obj2sobj (s'@s) (Proc p) = SProc (r,fr,pt,u) srp"
+ and exp: "p \<in> current_procs (s' @ s)"
+ and exf: "f \<in> current_files (s' @ s)"
+ and sreq: "sobj_source_eq_obj (SProc (r,fr,pt,u) srp) (Proc p)"
+ apply (drule_tac s' =s and obj' = "File f" in all_sobjs_E2, auto)
+ apply (frule_tac obj = "File f" in nodel_tainted_exists, simp)
+ by (frule obj2sobj_proc, clarsimp)
+ from vds' SP sreq exp have srpeq: "srp = Some p" by (simp add:proc_source_eq_prop)
+ with exp vds' SP have initp: "p \<in> init_processes"
+ by (auto simp:obj2sobj.simps dest:source_proc_in_init split:option.splits)
+ obtain e \<tau> where ev: "e = ReadFile p f" and tau: "\<tau> = s' @ s" by auto
+
+ have valid: "valid (e # \<tau>)"
+ proof-
+ have "os_grant \<tau> e"
+ using ev tau by (simp add:exf exp)
+ moreover have "rc_grant \<tau> e"
+ using ev tau ts'_read(4) SP SF
+ by (auto simp:etype_of_file_def cp2sproc.simps obj2sobj.simps
+ split:if_splits option.splits)
+ ultimately show ?thesis using vds' tau
+ by (rule_tac vs_step, simp+)
+ qed moreover
+ have "obj2sobj (e # \<tau>) (Proc p) = SProc (r, fr, pt, u) srp" using valid tau ev SP
+ by (auto simp:obj2sobj.simps cp2sproc_simps' split:option.splits)
+ moreover have "Proc p \<in> tainted (e # \<tau>)"
+ proof-
+ have "(File f) \<in> tainted \<tau>" using TF nodels' tau vds'
+ by (drule_tac s = "s'" in t_remain_app,auto)
+ thus ?thesis using ev valid
+ by (drule_tac t_read, simp+)
+ qed moreover
+ have "no_del_event (e # \<tau>)" using ev tau nodels' by simp
+ moreover have "initp_intact_but (e#\<tau>) (SProc (r, fr, pt, u) srp)"
+ using ev tau nodels' intacts' srpeq valid initp
+ by (simp, rule_tac initp_intact_butp_I_others, simp_all)
+ moreover have "sobj_source_eq_obj (SProc (r,fr,pt,u) srp) (Proc p)"
+ using sreq by (case_tac srp, simp+)
+ ultimately show ?case
+ by (rule_tac x = "Proc p" in exI, rule_tac x = "e#\<tau>" in exI, auto)
+next
+ case (ts'_write r fr pt u srp t sd srf)
+ from ts'_write(1) obtain p s where TP: "(Proc p) \<in> tainted s"
+ and "valid s \<and> p \<in> current_procs s \<and> no_del_event s \<and> initp_intact s \<and>
+ obj2sobj s (Proc p) = SProc (r,fr,pt,u) srp"
+ apply (drule_tac ts2t_intact, clarsimp, frule_tac obj2sobj_proc)
+ by (frule tainted_is_valid, frule tainted_is_current, auto)
+ with ts'_write(3) obtain f s' where vds': "valid (s' @ s)"
+ and SF: "obj2sobj (s'@s) (File f) = SFile (t, sd) srf"
+ and nodels': "no_del_event (s'@s)"
+ and intacts': "initp_intact (s'@s)"
+ and SP: "obj2sobj (s'@s) (Proc p) = SProc (r,fr,pt,u) srp"
+ and exp: "p \<in> current_procs (s' @ s)"
+ and exf: "f \<in> current_files (s' @ s)"
+ and sreq: "sobj_source_eq_obj (SFile (t, sd) srf) (File f)"
+ apply (drule_tac s' =s and obj' = "Proc p" in all_sobjs_E2, auto)
+ apply (frule_tac obj = "Proc p" in nodel_tainted_exists, simp)
+ by (frule obj2sobj_file, clarsimp)
+ obtain e \<tau> where ev: "e = WriteFile p f" and tau: "\<tau> = (s' @ s)" by auto
+
+ have valid: "valid (e# \<tau>)"
+ proof-
+ have "os_grant \<tau> e"
+ using ev tau exp exf by simp
+ moreover have "rc_grant \<tau> e"
+ using ev tau ts'_write(4) SP SF
+ by (auto simp:etype_of_file_def cp2sproc.simps obj2sobj.simps
+ split:if_splits option.splits)
+ ultimately show ?thesis using vds' tau
+ by (rule_tac vs_step, simp+)
+ qed moreover
+ have nodel: "no_del_event (e#\<tau>)" using nodels' tau ev by simp moreover
+ have "obj2sobj (e#\<tau>) (File f) = SFile (t, sd) srf"
+ using tau ev SF valid
+ by (auto simp:obj2sobj.simps source_dir_simps etype_of_file_def
+ split:option.splits if_splits)
+ moreover
+ have "initp_intact (e#\<tau>)" using ev intacts' valid nodels' tau
+ by (auto intro!:initp_intact_I_others) moreover
+ have "File f \<in> tainted (e#\<tau>)"
+ proof-
+ have "Proc p \<in> tainted \<tau>" using nodel vds' TP ev tau
+ by (drule_tac s = "s'" and s' = s in t_remain_app, auto)
+ thus ?thesis using ev tau valid by (auto intro:t_write)
+ qed
+ ultimately show ?case using tau ev sreq
+ by (rule_tac x = "File f" in exI, rule_tac x = "e#\<tau>" in exI, auto)
+next
+ case (ts'_recv t sri r fr pt u srp)
+ then obtain i s where "sobj_source_eq_obj (SIPC t sri) (IPC i)"
+ and TI: "(IPC i) \<in> tainted s" and vds: "valid s" and "i \<in> current_ipcs s"
+ and "obj2sobj s (IPC i) = SIPC t sri \<and> no_del_event s \<and> initp_intact s"
+ apply (clarsimp, frule_tac obj2sobj_ipc)
+ by (frule tainted_is_valid, frule tainted_is_current, auto)
+ with ts'_recv(3) obtain p s' where vds': "valid (s' @ s)"
+ and SI: "obj2sobj (s'@s) (IPC i) = SIPC t sri"
+ and nodels': "no_del_event (s'@s)"
+ and intacts': "initp_intact_but (s'@s) (SProc (r,fr,pt,u) srp)"
+ and SP: "obj2sobj (s'@s) (Proc p) = SProc (r,fr,pt,u) srp"
+ and exp: "p \<in> current_procs (s' @ s)"
+ and exi: "i \<in> current_ipcs (s' @ s)"
+ and sreq: "sobj_source_eq_obj (SProc (r,fr,pt,u) srp) (Proc p)"
+ apply (drule_tac s' =s and obj' = "IPC i" in all_sobjs_E2, auto)
+ apply (frule_tac obj = "IPC i" in nodel_tainted_exists, simp)
+ by (frule obj2sobj_proc, clarsimp)
+ from vds' SP sreq exp have srpeq: "srp = Some p" by (simp add:proc_source_eq_prop)
+ with exp vds' SP have initp: "p \<in> init_processes"
+ by (auto simp:obj2sobj.simps dest:source_proc_in_init split:option.splits)
+ obtain e \<tau> where ev: "e = Recv p i" and tau: "\<tau> = s' @ s" by auto
+
+ have valid: "valid (e # \<tau>)"
+ proof-
+ have "os_grant \<tau> e"
+ using ev tau by (simp add:exi exp)
+ moreover have "rc_grant \<tau> e"
+ using ev tau ts'_recv(4) SP SI
+ by (auto simp:cp2sproc.simps obj2sobj.simps
+ split:if_splits option.splits)
+ ultimately show ?thesis using vds' tau
+ by (rule_tac vs_step, simp+)
+ qed moreover
+ have "obj2sobj (e # \<tau>) (Proc p) = SProc (r, fr, pt, u) srp" using valid tau ev SP
+ by (auto simp:obj2sobj.simps cp2sproc_simps' split:option.splits)
+ moreover have "Proc p \<in> tainted (e # \<tau>)"
+ proof-
+ have "(IPC i) \<in> tainted \<tau>" using TI nodels' tau vds'
+ by (drule_tac s = "s'" in t_remain_app,auto)
+ thus ?thesis using ev valid
+ by (drule_tac t_recv, simp+)
+ qed moreover
+ have "no_del_event (e # \<tau>)" using ev tau nodels' by simp
+ moreover have "initp_intact_but (e#\<tau>) (SProc (r, fr, pt, u) srp)"
+ using ev tau nodels' intacts' srpeq valid initp
+ by (simp, rule_tac initp_intact_butp_I_others, simp_all)
+ moreover have "sobj_source_eq_obj (SProc (r,fr,pt,u) srp) (Proc p)"
+ using sreq by (case_tac srp, simp+)
+ ultimately show ?case
+ by (rule_tac x = "Proc p" in exI, rule_tac x = "e#\<tau>" in exI, auto)
+next
+ case (ts'_send r fr pt u srp t sri)
+ from ts'_send(1) obtain p s where TP: "(Proc p) \<in> tainted s"
+ and "valid s \<and> p \<in> current_procs s \<and> no_del_event s \<and> initp_intact s \<and>
+ obj2sobj s (Proc p) = SProc (r,fr,pt,u) srp"
+ apply (drule_tac ts2t_intact, clarsimp, frule_tac obj2sobj_proc)
+ by (frule tainted_is_valid, frule tainted_is_current, auto)
+ with ts'_send(3) obtain i s' where vds': "valid (s' @ s)"
+ and SI: "obj2sobj (s'@s) (IPC i) = SIPC t sri"
+ and nodels': "no_del_event (s'@s)"
+ and intacts': "initp_intact (s'@s)"
+ and SP: "obj2sobj (s'@s) (Proc p) = SProc (r,fr,pt,u) srp"
+ and exp: "p \<in> current_procs (s' @ s)"
+ and exi: "i \<in> current_ipcs (s' @ s)"
+ and sreq: "sobj_source_eq_obj (SIPC t sri) (IPC i)"
+ apply (drule_tac s' =s and obj' = "Proc p" in all_sobjs_E2, auto)
+ apply (frule_tac obj = "Proc p" in nodel_tainted_exists, simp)
+ by (frule obj2sobj_ipc, clarsimp)
+ obtain e \<tau> where ev: "e = Send p i" and tau: "\<tau> = (s' @ s)" by auto
+
+ have valid: "valid (e# \<tau>)"
+ proof-
+ have "os_grant \<tau> e"
+ using ev tau exp exi by simp
+ moreover have "rc_grant \<tau> e"
+ using ev tau ts'_send(4) SP SI
+ by (auto simp:cp2sproc.simps obj2sobj.simps
+ split:if_splits option.splits)
+ ultimately show ?thesis using vds' tau
+ by (rule_tac vs_step, simp+)
+ qed moreover
+ have nodel: "no_del_event (e#\<tau>)" using nodels' tau ev by simp moreover
+ have "obj2sobj (e#\<tau>) (IPC i) = SIPC t sri"
+ using tau ev SI valid
+ by (auto simp:obj2sobj.simps split:option.splits if_splits)
+ moreover have "initp_intact (e#\<tau>)" using ev intacts' valid nodels' tau
+ by (auto intro!:initp_intact_I_others)
+ moreover have "IPC i \<in> tainted (e#\<tau>)"
+ proof-
+ have "Proc p \<in> tainted \<tau>" using nodel vds' TP ev tau
+ by (drule_tac s = "s'" and s' = s in t_remain_app, auto)
+ thus ?thesis using ev tau valid by (auto intro:t_send)
+ qed
+ ultimately show ?case using tau ev sreq
+ by (rule_tac x = "IPC i" in exI, rule_tac x = "e#\<tau>" in exI, auto)
+next
+ case (ts'_crole r fr pt u srp r')
+ then obtain p s where exp: "p \<in> current_procs s"
+ and sreq:"sobj_source_eq_obj (SProc (r, fr, pt, u) srp) (Proc p)"
+ and TP: "(Proc p) \<in> tainted s" and vds: "valid s" and nodels: "no_del_event s"
+ and SP: "obj2sobj s (Proc p) = SProc (r, fr, pt, u) srp"
+ and intacts: "initp_intact_but s (SProc (r, fr, pt, u) srp)"
+ apply (clarsimp, frule_tac obj2sobj_proc)
+ by (frule tainted_is_valid, frule tainted_is_current, auto)
+ from vds SP sreq exp have srpeq: "srp = Some p" by (simp add:proc_source_eq_prop)
+ with exp vds SP have initp: "p \<in> init_processes"
+ by (auto simp:obj2sobj.simps dest:source_proc_in_init split:option.splits)
+ obtain e \<tau> where ev: "e = ChangeRole p r'"
+ and tau: "\<tau> = Clone p (new_proc s) # s" by auto
+ hence vs_tau:"valid \<tau>" using exp vds by (auto intro:clone_event_no_limit)
+
+ have valid: "valid (e # \<tau>)"
+ proof-
+ have "os_grant \<tau> e"
+ using ev tau exp by simp
+ moreover have "rc_grant \<tau> e"
+ using ev tau ts'_crole(3) SP
+ by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits)
+ ultimately show ?thesis using vs_tau
+ by (erule_tac vs_step, simp+)
+ qed moreover
+ have "obj2sobj (e # \<tau>) (Proc p) = SProc (r', fr, pt, u) srp"
+ proof-
+ have "obj2sobj \<tau> (Proc p) = SProc (r,fr,pt,u) srp" using SP tau vs_tau
+ by (auto split:option.splits simp:cp2sproc_simps' obj2sobj.simps)
+ thus ?thesis using valid ev
+ by (auto simp:cp2sproc_crole obj2sobj.simps split:option.splits)
+ qed moreover
+ have "Proc p \<in> tainted (e # \<tau>)"
+ proof-
+ have "(Proc p) \<in> tainted \<tau>" using TP tau vs_tau exp
+ by (auto intro!:t_remain)
+ thus ?thesis using ev valid
+ by (drule_tac t_remain, auto dest:valid_os)
+ qed moreover
+ have "no_del_event (e # \<tau>)" using ev tau nodels by simp
+ moreover have "initp_intact_but (e#\<tau>) (SProc (r', fr, pt, u) srp)"
+ using ev tau nodels intacts srpeq valid initp
+ by (simp, rule_tac initp_intact_butp_I_crole, simp_all)
+ moreover have "sobj_source_eq_obj (SProc (r',fr,pt,u) srp) (Proc p)"
+ using sreq by (case_tac srp, simp+)
+ ultimately show ?case
+ by (rule_tac x = "Proc p" in exI, rule_tac x = "e#\<tau>" in exI, auto)
+next
+ case (ts'_chown r fr pt u srp u' nr)
+ then obtain p s where exp: "p \<in> current_procs s"
+ and sreq:"sobj_source_eq_obj (SProc (r, fr, pt, u) srp) (Proc p)"
+ and TP: "(Proc p) \<in> tainted s" and vds: "valid s" and nodels: "no_del_event s"
+ and SP: "obj2sobj s (Proc p) = SProc (r, fr, pt, u) srp"
+ and intacts: "initp_intact_but s (SProc (r, fr, pt, u) srp)"
+ apply (clarsimp, frule_tac obj2sobj_proc)
+ by (frule tainted_is_valid, frule tainted_is_current, auto)
+ from vds SP sreq exp have srpeq: "srp = Some p" by (simp add:proc_source_eq_prop)
+ with exp vds SP have initp: "p \<in> init_processes"
+ by (auto simp:obj2sobj.simps dest:source_proc_in_init split:option.splits)
+ obtain e \<tau> where ev: "e = ChangeOwner p u'"
+ and tau: "\<tau> = Clone p (new_proc s) # s" by auto
+ hence vs_tau:"valid \<tau>" using exp vds by (auto intro:clone_event_no_limit)
+
+ have valid: "valid (e # \<tau>)"
+ proof-
+ have "os_grant \<tau> e"
+ using ev tau exp ts'_chown(3) by simp
+ moreover have "rc_grant \<tau> e"
+ using ev tau ts'_chown(5) SP
+ by (auto simp:cp2sproc.simps obj2sobj.simps pct_def clone_type_unchange
+ split:option.splits t_rc_proc_type.splits)
+ (* here is another place of no_limit of clone event assumption *)
+ ultimately show ?thesis using vs_tau
+ by (erule_tac vs_step, simp+)
+ qed moreover
+ have "obj2sobj (e # \<tau>) (Proc p) = SProc (nr, fr, chown_type_aux r nr pt, u') srp"
+ proof-
+ have "obj2sobj \<tau> (Proc p) = SProc (r,fr,pt,u) srp" using SP tau vs_tau
+ by (auto split:option.splits simp:cp2sproc_simps' obj2sobj.simps)
+ thus ?thesis using valid ev ts'_chown(4)
+ by (auto simp:cp2sproc_chown obj2sobj.simps split:option.splits)
+ qed moreover
+ have "Proc p \<in> tainted (e # \<tau>)"
+ proof-
+ have "(Proc p) \<in> tainted \<tau>" using TP tau vs_tau exp
+ by (auto intro!:t_remain)
+ thus ?thesis using ev valid
+ by (drule_tac t_remain, auto dest:valid_os)
+ qed moreover
+ have "no_del_event (e # \<tau>)" using ev tau nodels by simp
+ moreover have "initp_intact_but (e#\<tau>) (SProc (nr, fr, chown_type_aux r nr pt, u') srp)"
+ using ev tau nodels intacts srpeq valid initp
+ by (simp, rule_tac initp_intact_butp_I_chown, simp_all)
+ moreover have "sobj_source_eq_obj (SProc (nr, fr, chown_type_aux r nr pt, u') srp) (Proc p)"
+ using sreq by (case_tac srp, simp+)
+ ultimately show ?case
+ by (rule_tac x = "Proc p" in exI, rule_tac x = "e#\<tau>" in exI, auto)
+qed
+
+lemma tainted_s2tainted:
+ "sobj \<in> tainted_s \<Longrightarrow> \<exists> obj s. obj2sobj s obj = sobj \<and> obj \<in> tainted s \<and>
+ sobj_source_eq_obj sobj obj \<and> no_del_event s \<and>
+ initp_intact_but s sobj"
+apply (simp add:tainted_s'_eq)
+by (erule ts2t)
+
+end
+
+end
\ No newline at end of file