--- a/no_shm_selinux/Enrich2.thy Mon Dec 30 14:04:23 2013 +0800
+++ b/no_shm_selinux/Enrich2.thy Mon Dec 30 23:41:58 2013 +0800
@@ -256,22 +256,23 @@
(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 nodel by auto
+
+ from pre have pre_vd: "is_created_proc s p \<Longrightarrow> valid (enrich_proc s p p')" by simp
+ have vd_enrich:"is_created_proc s p \<Longrightarrow> valid (e # enrich_proc s p p')"
+ apply (frule pre_vd)
+ apply (erule_tac s = s and obj' = "E_proc p'" in enrich_valid_intro_cons)
+ apply (simp_all add: pre nodel_cons all_procs_cons vd_cons')
+ 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
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 and obj' = "E_proc p'" in enrich_valid_intro_cons)
- apply (simp_all add: pre nodel_cons all_procs_cons vd_cons')
- 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;
+ 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-
@@ -517,6 +518,7 @@
apply (erule_tac search_check_leveling_f)
apply (simp_all)
apply (simp add:search_check_file_def)
+ (* create new file, grant only check pf's SEARCH permission, not newfile itself, so we make assumptions of this case in the locale *)
apply (simp add:permission_check.simps)
sorry
qed
@@ -543,7 +545,7 @@
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' nodel
+ using a5 a2 a3 vd pre_vd nodel
apply (simp)
apply (drule_tac s = "enrich_proc s p p'" and p = p' in file_fds_subset_pfds)
apply (erule set_mp)
@@ -551,7 +553,7 @@
done
ultimately show "valid (CloseFd p' fd # CloseFd p fd # enrich_proc s p p')"
apply (rule_tac valid.intros(2))
- apply (simp_all add:a1 a0 a2 pre')
+ apply (simp_all add:a1 a0 a2 pre_vd)
done
qed
moreover have "\<And> fd. \<lbrakk>valid (ReadFile p fd # enrich_proc s p p');
@@ -643,11 +645,18 @@
qed
qed
ultimately show ?thesis
- using created_cons vd_cons' all_procs_cons
+ using vd_enrich created_cons vd_cons' all_procs_cons
apply (case_tac e)
apply (auto simp:is_created_proc_simps split:if_splits)
done
qed
+ have sec_proc:
+ "\<And> tp. \<lbrakk>tp \<in> current_procs s; is_created_proc s p\<rbrakk>
+ \<Longrightarrow> sectxt_of_obj (enrich_proc s p p') (O_proc tp) = sectxt_of_obj s (O_proc tp)"
+ using pre
+ apply (clarsimp)
+ apply (erule_tac x = tp in allE, auto simp:cp2sproc_def split:option.splits)
+ done
have sf_cons:
"\<forall>f. f \<in> current_files (e # s) \<longrightarrow> cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f"
proof clarify
@@ -659,18 +668,251 @@
from a1 have a1': "f \<in> current_files (enrich_proc (e # s) p p')"
using vd_cons' nodel_cons
by (simp add:enrich_proc_cur_files)
+ from a1 have a1'': "f \<in> current_files (e # enrich_proc s p p')"
+ using vd_cons' nodel_cons os vd vd_enrich created_cons
+ apply (case_tac e)
+ apply (auto simp:enrich_proc_cur_files current_files_simps is_created_proc_simps
+ dest:is_file_in_current is_dir_in_current split:option.splits)
+ done
+
+ have sec_dir:
+ "\<And> tf. \<lbrakk>is_dir s tf; is_created_proc s p\<rbrakk>
+ \<Longrightarrow> sectxt_of_obj (enrich_proc s p p') (O_dir tf) = sectxt_of_obj s (O_dir tf)"
+ proof-
+ fix tf
+ assume a1: "is_dir s tf" and a2: "is_created_proc s p"
+ from a2 pre
+ have pre': "\<And>f. f \<in> current_files s \<Longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f"
+ and vd_enrich: "valid (enrich_proc s p p')"
+ by auto
+ hence csf: "cf2sfile (enrich_proc s p p') tf = cf2sfile s tf"
+ using a1 by (auto simp:is_dir_in_current)
+ from a1 obtain sf where csf_some: "cf2sfile s tf = Some sf"
+ apply (case_tac "cf2sfile s tf")
+ apply (drule current_file_has_sfile')
+ apply (simp add:vd, simp add:is_dir_in_current, simp)
+ done
+ from a1 have a1': "is_dir (enrich_proc s p p') tf"
+ using enrich_proc_is_dir vd nodel all_procs by simp
+ from a1 have a3: "\<not> is_file s tf" using vd by (simp add:is_dir_not_file)
+ from a1' vd have a3': "\<not> is_file (enrich_proc s p p') tf" by (simp add:is_dir_not_file)
+ show "sectxt_of_obj (enrich_proc s p p') (O_dir tf) = sectxt_of_obj s (O_dir tf)"
+ using csf csf_some a3 a3' vd_enrich vd
+ apply (auto simp:cf2sfile_def split:option.splits)
+ apply (case_tac tf)
+ apply (simp add:root_sec_remains, simp)
+ done
+ qed
+ have sec_file:
+ "\<And> tf. \<lbrakk>is_file s tf; is_created_proc s p\<rbrakk>
+ \<Longrightarrow> sectxt_of_obj (enrich_proc s p p') (O_file tf) = sectxt_of_obj s (O_file tf)"
+ proof-
+ fix tf
+ assume a1: "is_file s tf" and a2: "is_created_proc s p"
+ from a2 pre
+ have pre': "\<And>f. f \<in> current_files s \<Longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f"
+ and vd_enrich: "valid (enrich_proc s p p')"
+ by auto
+ hence csf: "cf2sfile (enrich_proc s p p') tf = cf2sfile s tf"
+ using a1 by (auto simp:is_file_in_current)
+ from a1 obtain sf where csf_some: "cf2sfile s tf = Some sf"
+ apply (case_tac "cf2sfile s tf")
+ apply (drule current_file_has_sfile')
+ apply (simp add:vd, simp add:is_file_in_current, simp)
+ done
+ from a1 have a1': "is_file (enrich_proc s p p') tf"
+ using vd nodel all_procs by (simp add:enrich_proc_is_file)
+ show "sectxt_of_obj (enrich_proc s p p') (O_file tf) = sectxt_of_obj s (O_file tf)"
+ using csf csf_some vd_enrich vd a1 a1'
+ apply (auto simp:cf2sfile_def split:option.splits if_splits)
+ apply (case_tac tf, simp_all)
+ apply (drule root_is_dir', simp+)
+ done
+ qed
+ have secs_dir:
+ "\<And> tf ctxts'. \<lbrakk>is_dir s tf; is_created_proc s p; get_parentfs_ctxts s tf = Some ctxts'\<rbrakk>
+ \<Longrightarrow> \<exists> ctxts. get_parentfs_ctxts (enrich_proc s p p') tf = Some ctxts \<and> set ctxts = set ctxts'"
+ proof-
+ fix tf ctxts'
+ assume a1: "is_dir s tf" and a2: "is_created_proc s p"
+ and a4: "get_parentfs_ctxts s tf = Some ctxts'"
+ from a2 pre
+ have pre': "\<And>f. f \<in> current_files s \<Longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f"
+ and vd_enrich': "valid (enrich_proc s p p')"
+ by auto
+ hence csf: "cf2sfile (enrich_proc s p p') tf = cf2sfile s tf"
+ using a1 by (auto simp:is_dir_in_current)
+ from a1 obtain sf where csf_some: "cf2sfile s tf = Some sf"
+ apply (case_tac "cf2sfile s tf")
+ apply (drule current_file_has_sfile')
+ apply (simp add:vd, simp add:is_dir_in_current, simp)
+ done
+ from a1 have a1': "is_dir (enrich_proc s p p') tf"
+ using enrich_proc_is_dir vd nodel all_procs by simp
+ from a1 have a5: "\<not> is_file s tf" using vd by (simp add:is_dir_not_file)
+ from a1' vd have a5': "\<not> is_file (enrich_proc s p p') tf" by (simp add:is_dir_not_file)
+ from a1' pre_vd a2 obtain ctxts
+ where a3: "get_parentfs_ctxts (enrich_proc s p p') tf = Some ctxts"
+ apply (case_tac "get_parentfs_ctxts (enrich_proc s p p') tf")
+ apply (drule get_pfs_secs_prop', simp+)
+ done
+ moreover have "set ctxts = set ctxts'"
+ proof (cases tf)
+ case Nil
+ with a3 a4 vd vd_enrich'
+ show ?thesis
+ by (simp add:get_parentfs_ctxts.simps root_sec_remains split:option.splits)
+ next
+ case (Cons a ff)
+ with csf csf_some a5 a5' vd_enrich' vd a3 a4
+ show ?thesis
+ apply (auto simp:cf2sfile_def split:option.splits if_splits)
+ done
+ qed
+ ultimately
+ show "\<exists> ctxts. get_parentfs_ctxts (enrich_proc s p p') tf = Some ctxts \<and> set ctxts = set ctxts'"
+ by auto
+ qed
+ have b1: "\<And> proc f' flags fd' opt. e = Open proc f' flags fd' opt
+ \<Longrightarrow> cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f"
+ proof-
+ fix proc f' flags fd' opt
+ assume ev: "e = Open proc f' flags fd' opt"
+ have b1': "cf2sfile (e # enrich_proc s p p') f = cf2sfile (e # s) f"
+ proof (cases opt)
+ case None
+ thus ?thesis
+ using vd_cons' vd_enrich a1 created_cons
+ by (simp add:cf2sfile_open_none ev pre_sf
+ is_created_proc_simps current_files_simps)
+ next
+ case (Some inum)
+ show ?thesis
+ proof (cases "f' = f")
+ case True
+ from a1 obtain sf where csf: "cf2sfile (e # s) f = Some sf"
+ apply (case_tac "cf2sfile (e # s) f")
+ apply (drule current_file_has_sfile')
+ apply (simp add:vd_cons', simp, simp)
+ done
+ from a1 ev os Some True obtain pf where parent: "parent f = Some pf"
+ and pdir: "is_dir s pf" and proc_in: "proc \<in> current_procs s" by auto
+ have f_in: "f \<in> current_files (e # enrich_proc s p p')"
+ using ev True Some
+ by (simp add:current_files_open)
+ thus ?thesis using ev Some csf vd_enrich True created_cons vd_cons' a1 parent pdir proc_in
+ apply (simp add:is_created_proc_simps cf2sfile_open)
+ apply (simp add:sectxt_of_obj_simps sec_dir sec_proc split:option.splits)
+ apply (drule_tac tf = pf in secs_dir, simp+)
+ apply (erule exE, erule conjE, simp)
+ apply (case_tac aa, simp)
+ done
+ next
+ case False
+ have f_in: "f \<in> current_files (e # enrich_proc s p p')"
+ using ev False Some vd_enrich a1 created_cons nodel vd
+ by (simp add:current_files_open is_created_proc_simps enrich_proc_cur_files)
+ with ev Some a1 vd_enrich vd_cons' created_cons False
+ show ?thesis
+ apply (simp add:is_created_proc_simps cf2sfile_open)
+ apply (simp add:current_files_simps pre_sf)
+ done
+ qed
+ qed
+ show "cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f"
+ using ev vd_enrich_cons
+ apply simp
+ apply (rule conjI, rule impI)
+ apply (simp add:cf2sfile_open_none)
+ using b1' apply (auto dest:vd_cons)
+ done
+ qed
+ have b2: "\<And> proc f' inum. e = Mkdir proc f' inum
+ \<Longrightarrow> cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f"
+ proof-
+ fix proc f' inum
+ assume ev: "e = Mkdir proc f' inum"
+
+ show "cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f"
+ proof (cases "f' = f")
+ case True
+ from a1 obtain sf where csf: "cf2sfile (e # s) f = Some sf"
+ apply (case_tac "cf2sfile (e # s) f")
+ apply (drule current_file_has_sfile')
+ apply (simp add:vd_cons', simp, simp)
+ done
+ from a1 ev os True obtain pf where parent: "parent f = Some pf"
+ and pdir: "is_dir s pf" and proc_in: "proc \<in> current_procs s" by auto
+ have f_in: "f \<in> current_files (e # enrich_proc s p p')"
+ using ev True
+ by (simp add:current_files_mkdir)
+ thus ?thesis using ev csf vd_enrich True created_cons vd_cons' a1 parent pdir proc_in
+ apply (simp add:is_created_proc_simps cf2sfile_mkdir)
+ apply (simp add:sectxt_of_obj_simps sec_dir sec_proc split:option.splits)
+ apply (drule_tac tf = pf in secs_dir, simp+)
+ apply (erule exE, erule conjE, simp)
+ apply (case_tac aa, simp)
+ done
+ next
+ case False
+ have f_in: "f \<in> current_files (e # enrich_proc s p p')"
+ using ev False vd_enrich a1 created_cons nodel vd
+ by (simp add:current_files_mkdir is_created_proc_simps enrich_proc_cur_files)
+ with ev a1 vd_enrich vd_cons' created_cons False
+ show ?thesis
+ apply (simp add:is_created_proc_simps cf2sfile_mkdir)
+ apply (simp add:current_files_simps pre_sf)
+ done
+ qed
+ qed
+ have b3: "\<And> proc f' f''. e = LinkHard proc f' f''
+ \<Longrightarrow> cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f"
+ proof-
+ fix proc f' f''
+ assume ev: "e = LinkHard proc f' f''"
+ show "cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f"
+ proof (cases "f'' = f")
+ case True
+ from a1 obtain sf where csf: "cf2sfile (e # s) f = Some sf"
+ apply (case_tac "cf2sfile (e # s) f")
+ apply (drule current_file_has_sfile')
+ apply (simp add:vd_cons', simp, simp)
+ done
+ from a1 ev os True obtain pf where parent: "parent f'' = Some pf"
+ and pdir: "is_dir s pf" and proc_in: "proc \<in> current_procs s" by auto
+ have f_in: "f \<in> current_files (e # enrich_proc s p p')"
+ using ev True vd_enrich created_cons
+ by (simp add:current_files_simps is_created_proc_simps)
+ thus ?thesis using ev csf vd_enrich True created_cons vd_cons' a1 parent pdir proc_in
+ apply (simp add:is_created_proc_simps cf2sfile_linkhard)
+ apply (simp add:sectxt_of_obj_simps sec_dir sec_proc split:option.splits)
+ apply (drule_tac tf = pf in secs_dir, simp+)
+ apply (erule exE, erule conjE, simp)
+ apply (case_tac aa, simp)
+ done
+ next
+ case False
+ have f_in: "f \<in> current_files (e # enrich_proc s p p')"
+ using ev False vd_enrich a1 created_cons nodel vd vd_cons'
+ by (simp add:current_files_linkhard is_created_proc_simps enrich_proc_cur_files)
+ with ev a1 vd_enrich vd_cons' created_cons False
+ show ?thesis
+ apply (simp add:is_created_proc_simps cf2sfile_linkhard)
+ apply (simp add:current_files_simps pre_sf)
+ done
+ qed
+ qed
show "cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f"
- apply (case_tac e)
- using vd created_cons nodel_cons vd_enrich_cons vd_cons' a1 a1'
- apply (auto intro!:pre_sf simp:cf2sfile_simps is_created_proc_simps
- split:if_splits dest:vd_cons)
- thm cf2sfile_other
- apply (simp_all)
- done
-
-
- sorry
+ apply (case_tac e)
+ prefer 6 apply (erule b1)
+ prefer 11 apply (erule b2)
+ prefer 11 apply (erule b3)
+ using vd created_cons nodel_cons vd_enrich_cons vd_cons' a1 a1'
+ apply (auto intro!:pre_sf simp:cf2sfile_simps is_created_proc_simps current_files_simps
+ split:if_splits dest:vd_cons cf2sfile_other')
+ done
+ qed
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
@@ -799,9 +1041,26 @@
done
qed
qed
- moreover have "\<forall>tp. tp \<in> current_procs (e # s) \<longrightarrow> cp2sproc (enrich_proc (e # s) p p') tp = cp2sproc (e # s) tp"
+ moreover have "\<forall>q. q \<in> current_msgqs (e # s) \<longrightarrow> cq2smsgq (enrich_proc (e # s) p p') q = cq2smsgq (e # s) q"
+ proof clarify
+ fix q
+ assume a1: "q \<in> current_msgqs (e # s)"
+ from pre have pre_smsgq: "\<And> q. \<lbrakk>q \<in> current_msgqs s; is_created_proc s p\<rbrakk>
+ \<Longrightarrow> cq2smsgq (enrich_proc s p p') q = cq2smsgq s q"
+ by auto
+ show "cq2smsgq (enrich_proc (e # s) p p') q = cq2smsgq (e # s) q"
+ using vd_enrich_cons a1 created_cons nodel_cons vd_cons' os
+ apply (case_tac e)
+ apply (auto simp:cq2smsgq_simps cq2smsg_createmsgq is_created_proc_simps sec_proc
+ dest:cq2smsgq_other intro!:pre_smsgq split:if_splits dest:vd_cons)
+
+ apply (simp add:sectxt_of_obj_simps split:option.splits)
+
+ thm sec_proc
+ thm cq2smsgq_simps
+ thm cq2smsg_createmsgq
sorry
- moreover have "\<forall>q. q \<in> current_msgqs (e # s) \<longrightarrow> cq2smsgq (enrich_proc (e # s) p p') q = cq2smsgq (e # s) q"
+ 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 "cp2sproc (enrich_proc (e # s) p p') p' = cp2sproc (e # s) p"
proof-