--- a/no_shm_selinux/Enrich.thy Thu Dec 26 10:56:50 2013 +0800
+++ b/no_shm_selinux/Enrich.thy Mon Dec 30 12:01:09 2013 +0800
@@ -103,14 +103,37 @@
apply (induct s, simp)
by (case_tac a, auto)
+lemma not_all_msgqs_cons:
+ "p \<notin> all_msgqs (e # s) \<Longrightarrow> p \<notin> all_msgqs s"
+by (case_tac e, auto)
+
+lemma not_all_msgqs_prop:
+ "\<lbrakk>p' \<notin> all_msgqs s; p \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> p' \<noteq> p"
+apply (induct s, rule notI, simp)
+apply (frule vt_grant_os, frule vd_cons, frule not_all_msgqs_cons, simp, rule notI)
+apply (case_tac a, auto)
+done
+
+lemma not_all_msgqs_prop2:
+ "p' \<notin> all_msgqs s \<Longrightarrow> p' \<notin> init_msgqs"
+apply (induct s, simp)
+by (case_tac a, auto)
+
+lemma not_all_msgqs_prop3:
+ "p' \<notin> all_msgqs s \<Longrightarrow> p' \<notin> current_msgqs s"
+apply (induct s, simp)
+by (case_tac a, auto)
+
fun enrich_not_alive :: "t_state \<Rightarrow> t_enrich_obj \<Rightarrow> t_enrich_obj \<Rightarrow> bool"
where
- "enrich_not_alive s obj (E_file f) = (f \<notin> current_files s \<and> E_file f \<noteq> obj)"
-| "enrich_not_alive s obj (E_proc p) = (p \<notin> current_procs s \<and> E_proc p \<noteq> obj)"
-| "enrich_not_alive s obj (E_fd p fd) = ((p \<in> current_procs s \<longrightarrow> fd \<notin> current_proc_fds s p) \<and> E_fd p fd \<noteq> obj)"
-| "enrich_not_alive s obj (E_msgq q) = (q \<notin> current_msgqs s \<and> E_msgq q \<noteq> obj)"
-| "enrich_not_alive s obj (E_inum i) = (i \<notin> current_inode_nums s \<and> E_inum i \<noteq> obj)"
-| "enrich_not_alive s obj (E_msg q m) = ((q \<in> current_msgqs s \<longrightarrow> m \<notin> set (msgs_of_queue s q)) \<and> E_msg q m \<noteq> obj)"
+ "enrich_not_alive s obj (E_file f) = (f \<notin> current_files s \<and> obj \<noteq> E_file f)"
+| "enrich_not_alive s obj (E_proc p) = (p \<notin> current_procs s \<and> obj \<noteq> E_proc p)"
+| "enrich_not_alive s obj (E_fd p fd) =
+ ((p \<in> current_procs s \<longrightarrow> fd \<notin> current_proc_fds s p) \<and> obj \<noteq> E_fd p fd \<and> obj \<noteq> E_proc p)"
+| "enrich_not_alive s obj (E_msgq q) = (q \<notin> current_msgqs s \<and> obj \<noteq> E_msgq q)"
+| "enrich_not_alive s obj (E_inum i) = (i \<notin> current_inode_nums s \<and> obj \<noteq> E_inum i)"
+| "enrich_not_alive s obj (E_msg q m) =
+ ((q \<in> current_msgqs s \<longrightarrow> m \<notin> set (msgs_of_queue s q)) \<and> obj \<noteq> E_msg q m \<and> obj \<noteq> E_msgq q)"
lemma file_has_parent: "\<lbrakk>is_file s f; valid s\<rbrakk> \<Longrightarrow> \<exists> pf. is_dir s pf \<and> parent f = Some pf"
apply (case_tac f)
@@ -538,7 +561,8 @@
using os alive' p_in notin_all Open None
apply (erule_tac x = "E_fd p fd" in allE)
apply (case_tac obj')
- by auto
+ apply (auto dest:not_all_procs_prop3)
+ done
have "os_grant s' e" using p_in f_in fd_not_in os
by (simp add:Open None)
moreover have "grant s' e"
@@ -589,7 +613,7 @@
have fd_not_in: "fd \<notin> current_proc_fds s' p"
using os alive' p_in Open Some notin_all
apply (erule_tac x = "E_fd p fd" in allE)
- apply (case_tac obj', auto)
+ apply (case_tac obj', auto dest:not_all_procs_prop3)
done
have inum_not_in: "inum \<notin> current_inode_nums s'"
using os alive' Open Some notin_all
@@ -1116,8 +1140,8 @@
by (simp add:SendMsg)
have m_not_in: "m \<notin> set (msgs_of_queue s' q)" using os alive' notin_all SendMsg q_in
apply (erule_tac x = "E_msg q m" in allE)
- apply (case_tac obj')
- by auto
+ apply (case_tac obj', auto dest:not_all_msgqs_prop3)
+ done
have "os_grant s' e" using p_in q_in m_not_in
by (simp add:SendMsg)
moreover have "grant s' e"
--- a/no_shm_selinux/Enrich2.thy Thu Dec 26 10:56:50 2013 +0800
+++ b/no_shm_selinux/Enrich2.thy Mon Dec 30 12:01:09 2013 +0800
@@ -5,6 +5,15 @@
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)"
@@ -35,19 +44,195 @@
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)"
@@ -58,41 +243,34 @@
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 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
- 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
+ using vd all_procs nodel by auto
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 (simp_all add:os grant vd pre)
- done
+ 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;
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')"
@@ -103,25 +281,18 @@
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-
- from pre a2
- 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
+ have f_in: "is_file (enrich_proc s p p') f"
+ using vd nodel os all_procs
+ by (auto dest:vt_grant_os simp:enrich_proc_is_file)
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)
@@ -174,7 +345,8 @@
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)
@@ -204,8 +376,6 @@
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
@@ -218,7 +388,7 @@
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)
@@ -233,15 +403,9 @@
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-
- from pre a2
- 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
+ have f_in: "is_file (enrich_proc s p p') f"
+ using vd nodel os all_procs None
+ by (auto dest:vt_grant_os simp:enrich_proc_is_file)
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)"
@@ -338,7 +502,7 @@
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
@@ -379,7 +543,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'
+ 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)
@@ -402,8 +566,6 @@
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
@@ -411,12 +573,12 @@
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
@@ -435,10 +597,9 @@
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"
- apply simp
- apply (erule_tac x = "O_file f" in allE, simp)
- done
+ hence isfile_s': "is_file (enrich_proc s p p') f"
+ using vd nodel all_procs a2
+ by (auto simp:enrich_proc_is_file)
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
@@ -487,79 +648,89 @@
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
- assume a0: "alive (e # s) obj"
- have a1: "is_created_proc s p \<Longrightarrow> \<forall> obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj"
- using pre by auto
- show "alive (enrich_proc (e # s) p p') obj" (*
- proof (cases e)
- case (Execve tp f fds)
- with created_cons a1
- have b1: "\<forall> obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj"
- by (auto simp:is_created_proc_simps)
+ fix tp fd
+ assume a1: "fd \<in> proc_file_fds (e # s) tp"
+ from a1 obtain f where a1': "file_of_proc_fd (e # s) tp fd = Some f"
+ by (auto simp:proc_file_fds_def)
+ from pre have pre_sfd: "\<And> tp fd. \<lbrakk>fd \<in> proc_file_fds s tp; is_created_proc s p\<rbrakk> \<Longrightarrow>
+ cfd2sfd (enrich_proc s p p') tp fd = cfd2sfd s tp fd" by auto
+ hence pre_sfd': "\<And> tp fd f. \<lbrakk>file_of_proc_fd s tp fd = Some f; is_created_proc s p\<rbrakk> \<Longrightarrow>
+ cfd2sfd (enrich_proc s p p') tp fd = cfd2sfd s tp fd" by (auto simp:proc_file_fds_def)
+ 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>
+ 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 (simp add:alive_execve split:if_splits)
- apply (frule_tac vd_cons) defer
- apply (frule_tac vd_cons)
- using vd_cons' Execve vd os
- apply (auto simp:is_file_simps is_dir_simps is_created_proc_simps alive.simps
- split:t_object.splits if_splits
- dest:set_mp file_fds_subset_pfds)
- apply (erule_tac x = "O_proc nat" in allE, simp)
- apply (erule_tac x = "O_file list" in allE, simp)
- 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
+ apply (case_tac e)
+ apply (erule b1, erule b2)
+ prefer 4 apply (erule b3) prefer 4 apply (erule b4)
+ using vd created_cons nodel_cons a1' a4 vd_enrich_cons vd_cons'
+ apply (auto intro!:pre_sfd' simp:cfd2sfd_simps is_created_proc_simps
+ simp del:file_of_proc_fd.simps split:if_splits dest:vd_cons enrich_proc_filefd)
+ apply (simp_all)
+ 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"
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
@@ -574,14 +745,26 @@
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'
- dest:vt_grant_os)
+ apply (simp add:is_created_proc_simps)
+ 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
@@ -604,7 +787,8 @@
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
@@ -612,7 +796,7 @@
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
@@ -624,8 +808,6 @@
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)
@@ -669,7 +851,7 @@
lemma enrich_proc_tainted:
- ""
+
end