selinux: comparison no_shm_selinux/Enrich2.thy

equal deleted inserted replaced

-:e79e3a8a4ceb
+:cebdef333899
 imports Main Flask Static Init_prop Valid_prop Tainted_prop Delete_prop Co2sobj_prop S2ss_prop S2ss_prop2
 Temp Enrich Proc_fd_of_file_prop
 begin
 context tainting_s begin
+(* \<And> *)
+lemma current_proc_fds_in_curp:
+"\<lbrakk>fd \<in> current_proc_fds s p; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s"
+apply (induct s)
+apply (simp add:init_fds_of_proc_prop1)
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac a, auto split:if_splits option.splits)
+done
 lemma get_parentfs_ctxts_prop:
 "\<lbrakk>get_parentfs_ctxts s (a # f) = Some ctxts; sectxt_of_obj s (O_dir f) = Some ctxt; valid s\<rbrakk>
 \<Longrightarrow> ctxt \<in> set (ctxts)"
 apply (induct f)
 apply (erule get_pfs_secs_prop, simp)
 apply (erule_tac search_check_allp_intro, simp_all)
 apply (simp add:parentf_is_dir_prop2)
 done
+lemma enrich_proc_dup_ffds':
+"\<lbrakk>fd \<notin> current_proc_fds (enrich_proc s p p') p'; is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
+\<Longrightarrow> fd \<notin> proc_file_fds s p \<and> file_of_proc_fd s p fd = None"
+apply (auto simp:enrich_proc_dup_ffds_eq_fds)
+apply (simp add:proc_file_fds_def)
+done
+lemma enrich_proc_cur_inof:
+"\<lbrakk>valid s; no_del_event s\<rbrakk> \<Longrightarrow> inum_of_file (enrich_proc s p p') f = inum_of_file s f"
+apply (induct s arbitrary:f)
+apply simp
+apply (frule vd_cons, frule vt_grant_os, frule vt_grant)
+apply (case_tac a, auto)
+apply (auto split:option.splits simp del:grant.simps)
+done
+lemma not_all_procs_sock:
+"\<lbrakk>p' \<notin> all_procs s; valid s\<rbrakk> \<Longrightarrow> inum_of_socket s (p', fd) = None"
+apply (frule not_all_procs_prop3)
+apply (case_tac "inum_of_socket s (p', fd)", simp_all)
+apply (drule cn_in_curp', simp+)
+done
+lemma enrich_proc_cur_inos:
+"\<lbrakk>valid s; no_del_event s; p' \<notin> all_procs s\<rbrakk>
+\<Longrightarrow> inum_of_socket (enrich_proc s p p') (tp, fd) = inum_of_socket s (tp, fd)"
+apply (induct s arbitrary:tp)
+apply simp
+apply (frule vd_cons, frule vt_grant_os)
+apply (case_tac a, auto split:option.splits simp:not_all_procs_sock)
+apply (simp add:proc_file_fds_def, erule exE)
+apply (case_tac "inum_of_socket s (nat1, fd)", simp_all)
+apply (drule filefd_socket_conflict, simp_all add:current_sockets_def)
+done
+lemma enrich_proc_cur_inums:
+"\<lbrakk>p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
+\<Longrightarrow> current_inode_nums (enrich_proc s p p') = current_inode_nums s"
+apply (auto simp:current_inode_nums_def current_file_inums_def
+current_sock_inums_def enrich_proc_cur_inof enrich_proc_cur_inos)
+done
+lemma enrich_proc_cur_itag:
+"\<lbrakk>valid s; no_del_event s; p' \<notin> all_procs s\<rbrakk>
+\<Longrightarrow> itag_of_inum (enrich_proc s p p') i = itag_of_inum s i"
+apply (induct s)
+apply simp
+apply (frule vd_cons, frule vt_grant_os)
+apply (case_tac a, auto split:option.splits t_socket_type.splits)
+done
+lemma enrich_proc_cur_tcps:
+"\<lbrakk>valid s; no_del_event s; p' \<notin> all_procs s\<rbrakk>
+\<Longrightarrow> is_tcp_sock (enrich_proc s p p') = is_tcp_sock s"
+apply (rule ext, case_tac x)
+apply (auto simp add:is_tcp_sock_def enrich_proc_cur_itag enrich_proc_cur_inos
+split:option.splits t_inode_tag.splits)
+done
+lemma enrich_proc_cur_udps:
+"\<lbrakk>valid s; no_del_event s; p' \<notin> all_procs s\<rbrakk>
+\<Longrightarrow> is_udp_sock (enrich_proc s p p') = is_udp_sock s"
+apply (rule ext, case_tac x)
+apply (auto simp add:is_udp_sock_def enrich_proc_cur_itag enrich_proc_cur_inos
+split:option.splits t_inode_tag.splits)
+done
+lemma enrich_proc_cur_msgqs:
+"valid s \<Longrightarrow> current_msgqs (enrich_proc s p p') = current_msgqs s"
+apply (induct s, simp)
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac a, auto)
+done
+lemma enrich_proc_cur_msgs:
+"valid s \<Longrightarrow> msgs_of_queue (enrich_proc s p p') q = msgs_of_queue s q "
+apply (induct s, simp)
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac a, auto)
+done
+lemma enrich_proc_cur_procs:
+"\<lbrakk>p' \<notin> all_procs s; no_del_event s; is_created_proc s p; valid s\<rbrakk>
+\<Longrightarrow> current_procs (enrich_proc s p p') = current_procs s \<union> {p'}"
+apply (induct s, simp add:is_created_proc_def)
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac a, auto simp:is_created_proc_simps)
+done
+lemma enrich_proc_cur_files:
+"\<lbrakk>valid s; no_del_event s\<rbrakk> \<Longrightarrow> current_files (enrich_proc s p p') = current_files s"
+apply (auto simp:current_files_def)
+apply (simp add: enrich_proc_cur_inof)+
+done
+lemma enrich_proc_cur_fds1:
+"\<lbrakk>p' \<notin> all_procs s; no_del_event s; is_created_proc s p; valid s; tp \<in> current_procs s\<rbrakk>
+\<Longrightarrow> current_proc_fds (enrich_proc s p p') tp = current_proc_fds s tp"
+apply (induct s, simp add:is_created_proc_def)
+apply (frule vt_grant_os, frule vd_cons)
+apply (frule not_all_procs_prop3)
+apply (case_tac a)
+apply (auto simp:is_created_proc_simps)
+done
+lemma enrich_proc_cur_fds1':
+"\<lbrakk>p' \<notin> all_procs s; no_del_event s; is_created_proc s p; valid s; tp \<noteq> p'\<rbrakk>
+\<Longrightarrow> current_proc_fds (enrich_proc s p p') tp = current_proc_fds s tp"
+apply (induct s, simp add:is_created_proc_def)
+apply (frule vt_grant_os, frule vd_cons)
+apply (frule not_all_procs_prop3)
+apply (case_tac a)
+apply (auto simp:is_created_proc_simps)
+done
+lemma enrich_proc_cur_fds:
+"\<lbrakk>p' \<notin> all_procs s; no_del_event s; is_created_proc s p; valid s\<rbrakk>
+\<Longrightarrow> current_proc_fds (enrich_proc s p p') tp = (if (tp = p') then proc_file_fds s p else current_proc_fds s tp)"
+apply (simp add:enrich_proc_cur_fds1' enrich_proc_dup_ffds_eq_fds split:if_splits)
+done
+lemma enrich_proc_not_alive:
+"\<lbrakk>enrich_not_alive s (E_proc p') obj; is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
+\<Longrightarrow> enrich_not_alive (enrich_proc s p p') (E_proc p') obj"
+apply (case_tac obj)
+apply (simp_all add:enrich_proc_cur_procs enrich_proc_cur_files enrich_proc_cur_inums
+enrich_proc_cur_msgqs enrich_proc_cur_msgs enrich_proc_cur_fds)
+done
+lemma enrich_proc_filefd:
+"\<lbrakk>file_of_proc_fd s tp fd = Some f; is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
+\<Longrightarrow> file_of_proc_fd (enrich_proc s p p') tp fd = Some f"
+apply (induct s arbitrary:tp, simp add:is_created_proc_def)
+apply (frule vt_grant_os, frule vd_cons)
+apply (frule not_all_procs_prop3)
+apply (case_tac a)
+apply (auto simp:is_created_proc_simps dest:proc_fd_in_procs split:if_splits)
+done
+lemma enrich_proc_flagfd:
+"\<lbrakk>flags_of_proc_fd s tp fd = Some f; is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
+\<Longrightarrow> flags_of_proc_fd (enrich_proc s p p') tp fd = Some f"
+apply (induct s arbitrary:tp, simp add:is_created_proc_def)
+apply (frule vt_grant_os, frule vd_cons)
+apply (frule not_all_procs_prop3)
+apply (case_tac a)
+apply (auto simp:is_created_proc_simps dest:proc_fd_in_procs current_fflag_has_ffd split:if_splits option.splits)
+done
+lemma enrich_proc_hungs:
+"\<lbrakk>valid s; no_del_event s\<rbrakk> \<Longrightarrow> files_hung_by_del (enrich_proc s p p') = files_hung_by_del s"
+apply (induct s, simp)
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac a, auto simp:files_hung_by_del.simps)
+done
+lemma enrich_proc_is_file:
+"\<lbrakk>valid s; no_del_event s; p' \<notin> all_procs s\<rbrakk>
+\<Longrightarrow> is_file (enrich_proc s p p') = is_file s"
+apply (rule ext, case_tac x)
+apply (auto simp add:is_file_def enrich_proc_cur_itag enrich_proc_cur_inof
+split:option.splits t_inode_tag.splits)
+done
+lemma enrich_proc_is_dir:
+"\<lbrakk>valid s; no_del_event s; p' \<notin> all_procs s\<rbrakk>
+\<Longrightarrow> is_dir (enrich_proc s p p') = is_dir s"
+apply (rule ext, case_tac x)
+apply (auto simp add:is_dir_def enrich_proc_cur_itag enrich_proc_cur_inof
+split:option.splits t_inode_tag.splits)
+done
+lemma enrich_proc_alive:
+"\<lbrakk>alive s obj; valid s; is_created_proc s p; p' \<notin> all_procs s; no_del_event s\<rbrakk>
+\<Longrightarrow> alive (enrich_proc s p p') obj"
+apply (case_tac obj)
+apply (simp_all add:enrich_proc_is_file enrich_proc_is_dir enrich_proc_cur_msgqs
+enrich_proc_cur_msgs enrich_proc_cur_procs enrich_proc_cur_fds
+enrich_proc_cur_tcps enrich_proc_cur_udps)
+apply (rule impI, simp)
+apply (drule current_proc_fds_in_curp, simp, simp add:not_all_procs_prop3)
+done
 lemma enrich_proc_prop:
-"\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s\<rbrakk>
+"\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s; no_del_event s\<rbrakk>
 \<Longrightarrow> valid (enrich_proc s p p') \<and>
-(\<forall> obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj) \<and>
-(\<forall> obj. enrich_not_alive s obj \<longrightarrow> enrich_not_alive (enrich_proc s p p') obj) \<and>
-(files_hung_by_del (enrich_proc s p p') = files_hung_by_del s) \<and>
 (\<forall> tp. tp \<in> current_procs s \<longrightarrow> cp2sproc (enrich_proc s p p') tp = cp2sproc s tp) \<and>
 (\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f) \<and>
 (\<forall> q. q \<in> current_msgqs s \<longrightarrow> cq2smsgq (enrich_proc s p p') q = cq2smsgq s q) \<and>
-(\<forall> tp fd f. file_of_proc_fd s tp fd = Some f \<longrightarrow> file_of_proc_fd (enrich_proc s p p') tp fd = Some f) \<and>
-(\<forall> tp fd flags. flags_of_proc_fd s tp fd = Some flags \<longrightarrow>
-flags_of_proc_fd (enrich_proc s p p') tp fd = Some flags) \<and>
-(\<forall> q. msgs_of_queue (enrich_proc s p p') q = msgs_of_queue s q) \<and>
 (\<forall> tp fd. fd \<in> proc_file_fds s tp \<longrightarrow> cfd2sfd (enrich_proc s p p') tp fd = cfd2sfd s tp fd) \<and>
 (cp2sproc (enrich_proc s p p') p' = cp2sproc s p) \<and>
 (\<forall> fd. fd \<in> proc_file_fds s p \<longrightarrow> cfd2sfd (enrich_proc s p p') p' fd = cfd2sfd s p fd)"
 proof (induct s)
 case Nil
 thus ?case by (auto simp:is_created_proc_def)
 next
 case (Cons e s)
 hence vd_cons': "valid (e # s)" and created_cons: "is_created_proc (e # s) p"
 and all_procs_cons: "p' \<notin> all_procs (e # s)" and vd: "valid s"
 and os: "os_grant s e" and grant: "grant s e"
+and nodel_cons: "no_del_event (e # s)"
 by (auto dest:vd_cons' vt_grant_os vt_grant)
 from all_procs_cons have all_procs: "p' \<notin> all_procs s" by (case_tac e, auto)
+from nodel_cons have nodel: "no_del_event s" by (case_tac e, auto)
 from Cons have pre: "is_created_proc s p \<Longrightarrow> valid (enrich_proc s p p') \<and>
-(\<forall>obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj) \<and>
-(\<forall>obj. enrich_not_alive s obj \<longrightarrow> enrich_not_alive (enrich_proc s p p') obj) \<and>
-files_hung_by_del (enrich_proc s p p') = files_hung_by_del s \<and>
 (\<forall>tp. tp \<in> current_procs s \<longrightarrow> cp2sproc (enrich_proc s p p') tp = cp2sproc s tp) \<and>
 (\<forall>f. f \<in> current_files s \<longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f) \<and>
 (\<forall>q. q \<in> current_msgqs s \<longrightarrow> cq2smsgq (enrich_proc s p p') q = cq2smsgq s q) \<and>
-(\<forall>tp fd f. file_of_proc_fd s tp fd = Some f \<longrightarrow> file_of_proc_fd (enrich_proc s p p') tp fd = Some f) \<and>
-(\<forall>tp fd flags.
-flags_of_proc_fd s tp fd = Some flags \<longrightarrow> flags_of_proc_fd (enrich_proc s p p') tp fd = Some flags) \<and>
-(\<forall>q. msgs_of_queue (enrich_proc s p p') q = msgs_of_queue s q) \<and>
 (\<forall>tp fd. fd \<in> proc_file_fds s tp \<longrightarrow> cfd2sfd (enrich_proc s p p') tp fd = cfd2sfd s tp fd) \<and>
 (cp2sproc (enrich_proc s p p') p' = cp2sproc s p) \<and>
 (\<forall> fd. fd \<in> proc_file_fds s p \<longrightarrow> cfd2sfd (enrich_proc s p p') p' fd = cfd2sfd s p fd)"
-using vd all_procs by auto
+using vd all_procs nodel by auto
-have alive_pre: "is_created_proc s p \<Longrightarrow> (\<forall>obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj)"
-using pre by simp
-hence curf_pre: "is_created_proc s p \<Longrightarrow> (\<forall>f. f \<in> current_files s \<longrightarrow> f \<in> current_files (enrich_proc s p p'))"
-using vd apply auto
-apply (drule is_file_or_dir, simp)
-apply (erule disjE)
-apply (erule_tac x = "O_file f" in allE, simp add:is_file_in_current)
-apply (erule_tac x = "O_dir f" in allE, simp add:is_dir_in_current)
-done
 have vd_enrich_cons: "valid (enrich_proc (e # s) p p')"
 proof-
 from pre have pre': "is_created_proc s p \<Longrightarrow> valid (enrich_proc s p p')" by simp
 have "is_created_proc s p \<Longrightarrow> valid (e # enrich_proc s p p')"
 apply (frule pre')
-apply (erule_tac s = s in enrich_valid_intro_cons)
+apply (erule_tac s = s and obj' = "E_proc p'" in enrich_valid_intro_cons)
-apply (simp_all add:os grant vd pre)
+apply (simp_all add: pre nodel_cons all_procs_cons vd_cons')
-done
+apply (clarsimp simp:enrich_proc_alive nodel all_procs vd)
+apply (rule allI, rule impI, erule enrich_proc_not_alive)
+apply (simp_all add:nodel all_procs vd enrich_proc_hungs enrich_proc_cur_msgs)
+apply ((rule allI| rule impI)+, erule enrich_proc_filefd)
+apply (simp_all add:nodel all_procs vd)
+apply ((rule allI| rule impI)+, erule enrich_proc_flagfd)
+apply (simp_all add:nodel all_procs vd)
+done
 moreover have "\<And>f fds. \<lbrakk>valid (Execve p f fds # enrich_proc s p p'); is_created_proc s p;
 valid (Execve p f fds # s); p' \<notin> all_procs s\<rbrakk>
 \<Longrightarrow> valid (Execve p' f (fds \<inter> proc_file_fds s p) # Execve p f fds # enrich_proc s p p')"
 proof-
 fix f fds
 assume a1: "valid (Execve p f fds # enrich_proc s p p')" and a2: "is_created_proc s p"
 and a3: "valid (Execve p f fds # s)" and a0: "p' \<notin> all_procs s"
 have cp2sp: "\<forall> tp. tp \<in> current_procs s \<longrightarrow> cp2sproc (enrich_proc s p p') tp = cp2sproc s tp"
 and cf2sf: "\<forall> tf. tf \<in> current_files s \<longrightarrow> cf2sfile (enrich_proc s p p') tf = cf2sfile s tf"
 and cfd2sfd: "\<forall> tp tfd. tfd \<in> proc_file_fds s tp \<longrightarrow> cfd2sfd (enrich_proc s p p') tp tfd = cfd2sfd s tp tfd"
-and ffd_remain: "\<forall>tp fd f. file_of_proc_fd s tp fd = Some f \<longrightarrow>
-file_of_proc_fd (enrich_proc s p p') tp fd = Some f"
 and dup_sp: "cp2sproc (enrich_proc s p p') p' = cp2sproc s p"
 and dup_sfd: "\<forall> fd. fd \<in> proc_file_fds s p \<longrightarrow> cfd2sfd (enrich_proc s p p') p' fd = cfd2sfd s p fd"
-using pre a2 by auto
+using pre a2
+by auto
 show "valid (Execve p' f (fds \<inter> proc_file_fds s p) # Execve p f fds # enrich_proc s p p')"
 proof-
 from a0 a3 have a0': "p' \<noteq> p" by (auto dest!:vt_grant_os not_all_procs_prop3)
 from a3 have grant: "grant s (Execve p f fds)" and os: "os_grant s (Execve p f fds)"
 by (auto dest:vt_grant_os vt_grant simp del:os_grant.simps)
 have f_in: "is_file (enrich_proc s p p') f"
-proof-
+using vd nodel os all_procs
-from pre a2
+by (auto dest:vt_grant_os simp:enrich_proc_is_file)
-have a4: "\<forall> obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj"
-by (auto)
-show ?thesis using a3 a4
-apply (erule_tac x = "O_file f" in allE)
-by (auto dest:vt_grant_os)
-qed
 moreover have a5: "proc_file_fds s p \<subseteq> proc_file_fds (Execve p f fds # enrich_proc s p p') p'"
 using a3 a0'
 apply (frule_tac vt_grant_os)
 apply (auto simp:proc_file_fds_def)
 apply (rule_tac x = fa in exI)
 using p1 p2 p2' vd cf2sf f_in f_in' grant p3 f_in a1
 apply (rule_tac s = s in enrich_search_check)
 apply (simp_all add:is_file_simps)
 apply (rule allI, rule impI, erule_tac x = fa in allE, simp)
 apply (drule_tac ff = fa in cf2sfile_other')
-by (auto simp:a2 curf_pre)
+apply (auto simp:a2 enrich_proc_cur_files nodel)
+done
 ultimately show ?thesis
 using p1' p2' p3
 apply (simp split:option.splits)
 using grant p1 p2
 apply simp
 assume a1: "valid (Open p f flags fd opt # enrich_proc s p p')" and a2: "is_created_proc s p"
 and a3: "valid (Open p f flags fd opt # s)" and a4: "p' \<notin> all_procs s"
 have cp2sp: "\<forall> tp. tp \<in> current_procs s \<longrightarrow> cp2sproc (enrich_proc s p p') tp = cp2sproc s tp"
 and cf2sf: "\<forall> tf. tf \<in> current_files s \<longrightarrow> cf2sfile (enrich_proc s p p') tf = cf2sfile s tf"
 and cfd2sfd: "\<forall> tp tfd. tfd \<in> proc_file_fds s tp \<longrightarrow> cfd2sfd (enrich_proc s p p') tp tfd = cfd2sfd s tp tfd"
-and ffd_remain: "\<forall>tp fd f. file_of_proc_fd s tp fd = Some f \<longrightarrow>
-file_of_proc_fd (enrich_proc s p p') tp fd = Some f"
 and dup_sp: "cp2sproc (enrich_proc s p p') p' = cp2sproc s p"
 and dup_sfd: "\<forall> fd. fd \<in> proc_file_fds s p \<longrightarrow> cfd2sfd (enrich_proc s p p') p' fd = cfd2sfd s p fd"
 using pre a2 by auto
 from a4 a3 have a0: "p' \<noteq> p" by (auto dest!:vt_grant_os not_all_procs_prop3 split:option.splits)
 have a5: "p' \<in> current_procs (enrich_proc s p p')"
 by (simp_all add:vd a4)
 have a6: "is_file (Open p f flags fd opt # enrich_proc s p p') f"
 using a1 a3
 by (auto simp:is_file_open dest:vt_grant_os)
 have a7: "fd \<notin> current_proc_fds (enrich_proc s p p') p'"
-using a2 a4 vd
+using a2 a4 vd nodel
 apply (simp add:enrich_proc_dup_ffds_eq_fds)
 apply (rule notI)
 apply (drule_tac p = p in file_fds_subset_pfds)
 apply (drule set_mp, simp)
 using a3
 from a3 have grant: "grant s (Open p f flags fd opt)" and os: "os_grant s (Open p f flags fd opt)"
 by (auto dest:vt_grant_os vt_grant)
 show "valid (Open p' f (remove_create_flag flags) fd None # Open p f flags fd opt # enrich_proc s p p')"
 proof (cases opt)
 case None
 have f_in: "is_file (enrich_proc s p p') f"
-proof-
+using vd nodel os all_procs None
-from pre a2
+by (auto dest:vt_grant_os simp:enrich_proc_is_file)
-have a4: "\<forall> obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj"
-by (auto)
-show ?thesis using a3 a4 None
-apply (erule_tac x = "O_file f" in allE)
-by (auto dest:vt_grant_os)
-qed
 from grant None 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)"
 apply (simp split:option.splits)
 by (case_tac a, case_tac aa, blast)
 apply (case_tac "fa = f")
 using os Some
 apply simp
 apply (drule_tac f' = fa in cf2sfile_open)
 apply (simp add:current_files_simps)
-using curf_pre a2
+using enrich_proc_cur_files a2 nodel
 apply simp
 apply simp
 using cf2sf
 apply simp
 done
 from a4 a3 have a0: "p' \<noteq> p" by (auto dest!:vt_grant_os not_all_procs_prop3)
 have "p' \<in> current_procs (enrich_proc s p p')"
 using a2 a3 vd
 by (auto intro:enrich_proc_dup_in)
 moreover have "fd \<in> current_proc_fds (enrich_proc s p p') p'"
-using a5 a2 a3 vd pre'
+using a5 a2 a3 vd pre' nodel
 apply (simp)
 apply (drule_tac s = "enrich_proc s p p'" and p = p' in file_fds_subset_pfds)
 apply (erule set_mp)
 apply (simp add:enrich_proc_dup_ffds)
 done
 from a3 have os: "os_grant s (ReadFile p fd)" and grant: "grant s (ReadFile p fd)"
 by (auto dest:vt_grant_os vt_grant)
 have cp2sp: "\<forall> tp. tp \<in> current_procs s \<longrightarrow> cp2sproc (enrich_proc s p p') tp = cp2sproc s tp"
 and cf2sf: "\<forall> tf. tf \<in> current_files s \<longrightarrow> cf2sfile (enrich_proc s p p') tf = cf2sfile s tf"
 and cfd2sfd: "\<forall> tp tfd. tfd \<in> proc_file_fds s tp \<longrightarrow> cfd2sfd (enrich_proc s p p') tp tfd = cfd2sfd s tp tfd"
-and ffd_remain: "\<forall>tp fd f. file_of_proc_fd s tp fd = Some f \<longrightarrow>
-file_of_proc_fd (enrich_proc s p p') tp fd = Some f"
 and dup_sp: "cp2sproc (enrich_proc s p p') p' = cp2sproc s p"
 and dup_sfd: "\<forall> fd. fd \<in> proc_file_fds s p \<longrightarrow> cfd2sfd (enrich_proc s p p') p' fd = cfd2sfd s p fd"
 using pre a2 by auto
 have vd_enrich: "valid (enrich_proc s p p')" using a1 by (auto dest:valid.cases)
 show "valid (ReadFile p' fd # ReadFile p fd # enrich_proc s p p')"
 proof-
 have "os_grant (ReadFile p fd # enrich_proc s p p') (ReadFile p' fd)"
-using a1 a2 a4 vd os
+using a1 a2 a4 vd os nodel
 apply (clarsimp simp:current_files_simps enrich_proc_dup_in enrich_proc_dup_ffds_eq_fds)
 apply (simp add:proc_file_fds_def)
 apply (rule conjI)
 apply (rule_tac x = f in exI, simp add:enrich_proc_dup_ffd)
-using curf_pre
+using enrich_proc_cur_files
 apply (simp)
 apply (drule enrich_proc_dup_fflags)
 apply simp_all
 apply (erule disjE)
 apply auto
 by (auto split:option.splits)
 from os obtain flag where p0: "flags_of_proc_fd s p fd = Some flag"
 by auto
 from os have f_in_s: "f \<in> current_files s" using p1 by simp
 from p1 vd have isfile_s: "is_file s f" by (erule_tac file_of_pfd_is_file, simp)
-with alive_pre a2 have isfile_s': "is_file (enrich_proc s p p') f"
+hence isfile_s': "is_file (enrich_proc s p p') f"
-apply simp
+using vd nodel all_procs a2
-apply (erule_tac x = "O_file f" in allE, simp)
+by (auto simp:enrich_proc_is_file)
-done
 from p0 obtain flag' where p0': "flags_of_proc_fd (enrich_proc s p p') p' fd = Some flag'"
 and p0'': "(flag' = flag) \<or> (flag' = remove_create_flag flag)"
 using a2 a4 vd
 apply (drule_tac enrich_proc_dup_fflags)
 apply auto
 using created_cons vd_cons' all_procs_cons
 apply (case_tac e)
 apply (auto simp:is_created_proc_simps split:if_splits)
 done
 qed
-moreover have "\<forall>obj. alive (e # s) obj \<longrightarrow> alive (enrich_proc (e # s) p p') obj"
+moreover have "\<forall>tp fd. fd \<in> proc_file_fds (e # s) tp \<longrightarrow>
+cfd2sfd (enrich_proc (e # s) p p') tp fd = cfd2sfd (e # s) tp fd"
 proof clarify
-fix obj
+fix tp fd
-assume a0: "alive (e # s) obj"
+assume a1: "fd \<in> proc_file_fds (e # s) tp"
-have a1: "is_created_proc s p \<Longrightarrow> \<forall> obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj"
+from a1 obtain f where a1': "file_of_proc_fd (e # s) tp fd = Some f"
-using pre by auto
+by (auto simp:proc_file_fds_def)
-show "alive (enrich_proc (e # s) p p') obj" (*
+from pre have pre_sfd: "\<And> tp fd. \<lbrakk>fd \<in> proc_file_fds s tp; is_created_proc s p\<rbrakk> \<Longrightarrow>
-proof (cases e)
+cfd2sfd (enrich_proc s p p') tp fd = cfd2sfd s tp fd" by auto
-case (Execve tp f fds)
+hence pre_sfd': "\<And> tp fd f. \<lbrakk>file_of_proc_fd s tp fd = Some f; is_created_proc s p\<rbrakk> \<Longrightarrow>
-with created_cons a1
+cfd2sfd (enrich_proc s p p') tp fd = cfd2sfd s tp fd" by (auto simp:proc_file_fds_def)
-have b1: "\<forall> obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj"
+hence pre_sfd'': "\<And> tp fd f proc. \<lbrakk>file_of_proc_fd s tp fd = Some f; is_created_proc s p; p = proc\<rbrakk> \<Longrightarrow>
-by (auto simp:is_created_proc_simps)
+cfd2sfd (enrich_proc s proc p') tp fd = cfd2sfd s tp fd" by (auto simp:proc_file_fds_def)
+from a1' all_procs_cons vd_cons' have a2: "tp \<noteq> p'"
+apply (drule_tac not_all_procs_prop3)
+apply (drule proc_fd_in_procs, simp)
+by (rule notI, simp)
+have a3: "p' \<noteq> p" using all_procs_cons created_cons
+apply (drule_tac not_all_procs_prop3)
+apply (rule notI, simp add:is_created_proc_def)
+done
+have a4: "file_of_proc_fd (enrich_proc (e # s) p p') tp fd = Some f"
+using a1' nodel_cons all_procs_cons a1' created_cons vd_cons'
+apply (frule_tac enrich_proc_filefd, simp_all)
+done
+show "cfd2sfd (enrich_proc (e # s) p p') tp fd = cfd2sfd (e # s) tp fd"
+proof-
+have b1: "\<And> proc f' fds. e = Execve proc f' fds
+\<Longrightarrow> cfd2sfd (enrich_proc (e # s) p p') tp fd = cfd2sfd (e # s) tp fd"
+using a4 vd_enrich_cons a1' vd_cons' created_cons
+apply (simp split:if_splits del:file_of_proc_fd.simps add:a2)
+apply (simp only:cfd2sfd_execve)
+apply (drule_tac s = "Execve proc f' fds # enrich_proc s proc p'" in vd_cons)
+apply (simp split:if_splits add:a2)
+apply (drule_tac p' = proc and fd' = fd and s = "enrich_proc s proc p'" in cfd2sfd_execve, simp+)
+apply (erule_tac pre_sfd'', simp add:is_created_proc_simps, simp)
+apply (drule_tac p' = tp and fd' = fd in cfd2sfd_execve, simp+)
+apply (erule_tac pre_sfd'', simp add:is_created_proc_simps, simp)
+apply (simp only:cfd2sfd_execve)
+apply (rule_tac pre_sfd')
+apply (auto split:if_splits simp:is_created_proc_simps)
+done
+have b2: "\<And> proc proc' fds. e = Clone proc proc' fds
+\<Longrightarrow> cfd2sfd (enrich_proc (e # s) p p') tp fd = cfd2sfd (e # s) tp fd"
+using a4 vd_enrich_cons a1' vd_cons' created_cons
+apply (simp split:if_splits del:file_of_proc_fd.simps)
+apply (simp add:cfd2sfd_clone add:a2)
+apply (simp add:cfd2sfd_clone split:if_splits)
+apply (erule pre_sfd'', simp add:is_created_proc_simps, simp)
+apply (erule pre_sfd', simp add:is_created_proc_simps)
+done
+have b3: "\<And> proc f' flags fd' opt. e = Open proc f' flags fd' opt
+\<Longrightarrow> cfd2sfd (enrich_proc (e # s) p p') tp fd = cfd2sfd (e # s) tp fd"
+apply (simp split:if_splits)
+thm cfd2sfd_open
+sorry
+have b4: "\<And> proc fd'. e = ReadFile proc fd'
+\<Longrightarrow> cfd2sfd (enrich_proc (e # s) p p') tp fd = cfd2sfd (e # s) tp fd"
+using a4 vd_enrich_cons a1' vd_cons' created_cons
+apply (simp split:if_splits del:file_of_proc_fd.simps)
+apply (frule_tac s = "ReadFile proc fd' # enrich_proc s proc p'" in vd_cons)
+apply (simp add:cfd2sfd_other)
+apply (erule pre_sfd'', simp add:is_created_proc_simps, simp)
+apply (simp add:cfd2sfd_other)
+apply (erule pre_sfd', simp add:is_created_proc_simps)
+done
 show ?thesis
-using created_cons all_procs_cons vd_enrich_cons Execve b1 os a0
+apply (case_tac e)
-apply (simp add:alive_execve split:if_splits)
+apply (erule b1, erule b2)
-apply (frule_tac vd_cons) defer
+prefer 4 apply (erule b3) prefer 4 apply (erule b4)
-apply (frule_tac vd_cons)
+using vd created_cons nodel_cons a1' a4 vd_enrich_cons vd_cons'
-using vd_cons' Execve vd os
+apply (auto intro!:pre_sfd' simp:cfd2sfd_simps is_created_proc_simps
-apply (auto simp:is_file_simps is_dir_simps is_created_proc_simps alive.simps
+simp del:file_of_proc_fd.simps split:if_splits dest:vd_cons enrich_proc_filefd)
-split:t_object.splits if_splits
+apply (simp_all)
-dest:set_mp file_fds_subset_pfds)
+done
-apply (erule_tac x = "O_proc nat" in allE, simp)
+qed
-apply (erule_tac x = "O_file list" in allE, simp)
+qed
-apply (drule set_mp, simp)
-apply (drule_tac s = s and p = tp in file_fds_subset_pfds)
-apply (erule_tac x = "O_fd tp nat2" in allE, simp)
-apply (auto)[1]
-apply (erule_tac x = "O_fd nat1 nat2" in allE, auto dest:set_mp file_fds_subset_pfds)[1]
-apply (erule_tac x = "O_dir list" in allE, simp)
-sorry
-show ?thesis *) sorry
-moreover have "\<forall>obj. enrich_not_alive (e # s) obj \<longrightarrow> enrich_not_alive (enrich_proc (e # s) p p') obj"
-thm enrich_not_alive.simps
-sorry
-moreover have "files_hung_by_del (enrich_proc (e # s) p p') = files_hung_by_del (e # s)"
-proof-
-have "is_created_proc s p \<Longrightarrow> files_hung_by_del (enrich_proc s p p') = files_hung_by_del s"
-and ffd_remain: "is_created_proc s p \<Longrightarrow>
-\<forall>tp fd f. file_of_proc_fd s tp fd = Some f \<longrightarrow>
-file_of_proc_fd (enrich_proc s p p') tp fd = Some f"
-using pre by auto
-with created_cons all_procs_cons os vd_cons' vd
-show ?thesis
-apply (frule_tac not_all_procs_prop3)
-apply (case_tac e)
-apply (auto simp:files_hung_by_del.simps is_created_proc_simps)
-apply (auto simp:enrich_proc_dup_ffd_eq proc_file_fds_def procfd_of_file_eq_fpfd''
-dest:procfd_of_file_imp_fpfd procfd_of_file_imp_fpfd' procfd_of_file_non_empty
-)
-apply (auto simp:enrich_proc_dup_ffd_eq proc_file_fds_def split:if_splits)[1]
-apply (auto simp:enrich_proc_dup_ffd_eq proc_file_fds_def files_hung_by_del.simps
-split:option.splits)[1]
-apply (auto split:option.splits)[1]
-thm is_created_proc_simps
-sorry
 moreover have "\<forall>tp. tp \<in> current_procs (e # s) \<longrightarrow> cp2sproc (enrich_proc (e # s) p p') tp = cp2sproc (e # s) tp"
 sorry
 moreover have "\<forall>f. f \<in> current_files (e # s) \<longrightarrow> cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f"
 sorry
 moreover have "\<forall>q. q \<in> current_msgqs (e # s) \<longrightarrow> cq2smsgq (enrich_proc (e # s) p p') q = cq2smsgq (e # s) q"
 sorry
-moreover have "\<forall>tp fd f. file_of_proc_fd (e # s) tp fd = Some f \<longrightarrow>
-file_of_proc_fd (enrich_proc (e # s) p p') tp fd = Some f"
-sorry
-moreover have "\<forall>tp fd flags. flags_of_proc_fd (e # s) tp fd = Some flags \<longrightarrow>
-flags_of_proc_fd (enrich_proc (e # s) p p') tp fd = Some flags"
-sorry
-moreover have "\<forall>q. msgs_of_queue (enrich_proc (e # s) p p') q = msgs_of_queue (e # s) q"
-sorry
-moreover have "\<forall>tp fd. fd \<in> proc_file_fds (e # s) tp \<longrightarrow>
-cfd2sfd (enrich_proc (e # s) p p') tp fd = cfd2sfd (e # s) tp fd"
-sorry
 moreover have "cp2sproc (enrich_proc (e # s) p p') p' = cp2sproc (e # s) p"
 proof-
 from pre have b0: "is_created_proc s p \<Longrightarrow> cp2sproc (enrich_proc s p p') p' = cp2sproc s p" by simp
 have b1: "\<And> tp f fds. \<lbrakk>valid (enrich_proc (Execve tp f fds # s) p p'); valid (Execve tp f fds # s);
 is_created_proc (Execve tp f fds # s) p; p' \<notin> all_procs (Execve tp f fds # s)\<rbrakk>
 and a2: "valid (Execve tp f fds # s)" and a3: "is_created_proc (Execve tp f fds # s) p"
 and a4: "p' \<notin> all_procs (Execve tp f fds # s)"
 show "cp2sproc (enrich_proc (Execve tp f fds # s) p p') p' = cp2sproc (Execve tp f fds # s) p"
 proof (cases "tp = p")
 case True
-show ?thesis using True a1 a2 a3 a4 b0
+show ?thesis using True a1 a2 a3 a4 b0 vd
 thm not_all_procs_prop3
 apply (frule_tac not_all_procs_prop2)
 apply (frule not_all_procs_prop3)
-apply (auto simp add:cp2sproc_execve is_created_proc_def split:option.splits dest!:current_has_sec'
+apply (simp add:is_created_proc_simps)
-dest:vt_grant_os)
+apply (frule vd_cons) (*
+apply (frule_tac vt_grant_os)
+apply (frule_tac \<tau> = "enrich_proc s p p'" in vt_grant_os) *)
+apply (frule_tac s = "enrich_proc s p p'" in vd_cons)
+apply (frule_tac \<tau> = s in vt_grant_os)
+apply (case_tac "p' = p", simp) (*
+apply (auto simp add:cp2sproc_execve sectxt_of_obj_simps enrich_proc_dup_in
+split:option.splits dest!:current_has_sec' dest:vt_grant is_file)
+apply (simp_all add:is_created_proc_def)
+apply (auto simp:cp2sproc_def)
+apply (simp_all add:enrich_proc_dup_in)
 apply (auto simp:sectxt_of_obj_simps split:option.splits dest:valid.cases)
+*)
 sorry
 next
 case False
 show ?thesis sorry
 qed
 sorry
 have b7: "\<And> tp fd. cp2sproc (enrich_proc (CloseFd tp fd # s) p p') p' = cp2sproc (CloseFd tp fd # s) p"
 sorry
 show ?thesis using vd_enrich_cons
 apply (case_tac e)
-apply (simp_all only:b1 b2 b3 b4 b5 b6 b7)
+using vd_cons' created_cons all_procs_cons
+apply (auto intro!:b1 b2 b3 b4 b5 b6 b7 simp del:enrich_proc.simps)
 using created_cons vd_enrich_cons vd_cons' b0
 apply (auto simp:cp2sproc_other is_created_proc_def)
 done
 qed
 moreover have "\<forall> fd. fd \<in> proc_file_fds (e # s) p \<longrightarrow>
 cfd2sfd (enrich_proc (e # s) p p') p' fd = cfd2sfd (e # s) p fd"
 sorry
-ultimately show ?case
+ultimately show ?case using vd_enrich_cons
 by simp
 qed
 lemma enrich_proc_valid:
 "\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s\<rbrakk> \<Longrightarrow> valid (enrich_proc s p p')"
 by (auto dest:enrich_proc_prop)
 lemma enrich_proc_valid:
 "\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s\<rbrakk> \<Longrightarrow> "
 lemma enrich_proc_tainted:
 "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk>
 \<Longrightarrow> tainted (enrich_proc s p p') = (if (O_proc p \<in> tainted s)
 then tainted s \<union> {O_proc p'} else tainted s)"
 apply (case_tac a)
 apply (auto simp:is_created_proc_def)[1]
 lemma enrich_proc_tainted:
-""
 end
 end

changeset 84	cebdef333899
parent 83	e79e3a8a4ceb
child 85	1d1aa5bdd37d