--- a/no_shm_selinux/Enrich.thy Wed Jan 01 23:00:24 2014 +0800
+++ b/no_shm_selinux/Enrich.thy Mon Jan 06 23:07:51 2014 +0800
@@ -3,14 +3,28 @@
Temp
begin
-(* objects that need dynamic indexing, all nature-numbers *)
+(* enriched objects, closely related to static objects, so are only 3 kinds *)
datatype t_enrich_obj =
- E_proc "t_process"
-| E_file "t_file"
-| E_fd "t_process" "t_fd"
-| E_inum "nat"
+ E_proc "t_process" "t_msgq" "t_msgq"
+| E_file_link "t_file"
+| E_file "t_file" "nat"
+ (*
+| E_fd "t_process" "t_fd"
+| E_inum "nat" *)
| E_msgq "t_msgq"
+(*
| E_msg "t_msgq" "t_msg"
+*)
+
+
+(* objects that need dynamic indexing, all nature-numbers *)
+datatype t_index_obj =
+ I_proc "t_process"
+| I_file "t_file"
+| I_fd "t_process" "t_fd"
+| I_inum "nat"
+| I_msgq "t_msgq"
+| I_msg "t_msgq" "t_msg"
context tainting_s begin
@@ -73,6 +87,7 @@
| "all_files (LinkHard p f f' # s) = all_files s \<union> {f'}"
| "all_files (e # s) = all_files s"
+(*
fun notin_all:: "t_state \<Rightarrow> t_enrich_obj \<Rightarrow> bool"
where
"notin_all s (E_proc p) = (p \<notin> all_procs s)"
@@ -81,6 +96,37 @@
| "notin_all s (E_inum i) = (i \<notin> all_inums s)"
| "notin_all s (E_msgq q) = (q \<notin> all_msgqs s)"
| "notin_all s (E_msg q m) = (m \<notin> all_msgs s q)"
+*)
+
+fun nums_of_recvmsg:: "t_state \<Rightarrow> t_process \<Rightarrow> nat"
+where
+ "nums_of_recvmsg [] p' = 0"
+| "nums_of_recvmsg (RecvMsg p q m # s) p' =
+ (if p' = p then Suc (nums_of_recvmsg s p) else nums_of_recvmsg s p')"
+| "nums_of_recvmsg (e # s) p' = nums_of_recvmsg s p'"
+
+lemma nums_of_recv_0:
+ "\<lbrakk>p \<notin> current_procs s; no_del_event s; valid s\<rbrakk> \<Longrightarrow> nums_of_recvmsg s p = 0"
+apply (induct s, simp)
+apply (frule vt_grant_os, frule vd_cons, case_tac a)
+apply (auto)
+done
+
+lemma new_msgq_1:
+ "\<lbrakk>new_msgq s \<le> q; q \<le> new_msgq s - Suc 0\<rbrakk> \<Longrightarrow> False"
+apply (subgoal_tac "new_msgq s \<noteq> 0")
+apply (simp, simp add:new_msgq_def next_nat_def)
+done
+
+fun notin_cur:: "t_state \<Rightarrow> t_enrich_obj \<Rightarrow> bool"
+where
+ "notin_cur s (E_proc p qmin qmax) =
+ (p \<notin> current_procs s \<and> qmin = new_msgq s \<and> qmax = new_msgq s + (nums_of_recvmsg s p) - 1)"
+| "notin_cur s (E_file f inum) =
+ (f \<notin> current_files s \<and> (\<exists> pf. parent f = Some pf \<and> is_dir s pf) \<and> inum \<notin> current_inode_nums s)"
+| "notin_cur s (E_file_link f) =
+ (f \<notin> current_files s \<and> (\<exists> pf. parent f = Some pf \<and> is_dir s pf))"
+| "notin_cur s (E_msgq q) = (q \<notin> current_msgqs s)"
lemma not_all_procs_cons:
"p \<notin> all_procs (e # s) \<Longrightarrow> p \<notin> all_procs s"
@@ -118,17 +164,24 @@
"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"
+
+fun enrich_not_alive :: "t_state \<Rightarrow> t_enrich_obj \<Rightarrow> t_index_obj \<Rightarrow> bool"
where
- "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)"
+ "enrich_not_alive s obj (I_file f) =
+ (f \<notin> current_files s \<and> (\<forall> inum. obj \<noteq> E_file f inum) \<and> obj \<noteq> E_file_link f)"
+| "enrich_not_alive s obj (I_proc p) = (p \<notin> current_procs s \<and> (\<forall> qmin qmax. obj \<noteq> E_proc p qmin qmax))"
+| "enrich_not_alive s obj (I_fd p fd) =
+ ((p \<in> current_procs s \<longrightarrow> fd \<notin> current_proc_fds s p) \<and> (\<forall> qmin qmax. obj \<noteq> E_proc p qmin qmax))"
+| "enrich_not_alive s obj (I_msgq q) = (q \<notin> current_msgqs s \<and> obj \<noteq> E_msgq q \<and>
+ (case obj of
+ E_proc p qmin qmax \<Rightarrow> \<not> (q \<ge> qmin \<and> q \<le> qmax)
+ | _ \<Rightarrow> True) )"
+| "enrich_not_alive s obj (I_inum i) = (i \<notin> current_inode_nums s \<and> (\<forall> f. obj \<noteq> E_file f i))"
+| "enrich_not_alive s obj (I_msg q m) =
+ ((q \<in> current_msgqs s \<longrightarrow> m \<notin> set (msgs_of_queue s q)) \<and> obj \<noteq> E_msgq q \<and>
+ (case obj of
+ E_proc p qmin qmax \<Rightarrow> \<not> (q \<ge> qmin \<and> q \<le> qmax)
+ | _ \<Rightarrow> True) )"
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)
@@ -310,7 +363,7 @@
(* and empty_remain: "\<forall> f. dir_is_empty s f \<longrightarrow> dir_is_empty s' f" *)
and cfd2sfd: "\<forall> p fd. fd \<in> proc_file_fds s p \<longrightarrow> cfd2sfd s' p fd = cfd2sfd s p fd"
and nodel: "no_del_event (e # s)"
- and notin_all: "notin_all (e # s) obj'"
+ and notin_cur: "notin_cur (e # s) obj'"
shows "valid (e # s')"
proof-
from vd' have os: "os_grant s e" and grant: "grant s e" and vd: "valid s"
@@ -372,9 +425,9 @@
have p_in: "p \<in> current_procs s'" using os alive
apply (erule_tac x = "O_proc p" in allE)
by (auto simp:Clone)
- have p'_not_in: "p' \<notin> current_procs s'" using alive' notin_all os Clone
- apply (erule_tac x = "E_proc p'" in allE)
- apply (auto dest:not_all_procs_prop3)
+ have p'_not_in: "p' \<notin> current_procs s'" using alive' notin_cur os Clone
+ apply (erule_tac x = "I_proc p'" in allE)
+ apply (auto dest:not_all_procs_prop3 simp del:nums_of_recvmsg.simps)
done
have fd_in: "fds \<subseteq> proc_file_fds s' p" using os alive ffd_remain
by (auto simp:Clone proc_file_fds_def)
@@ -482,8 +535,8 @@
apply (erule_tac x = "O_file f" in allE)
by (auto simp:Open None)
have fd_not_in: "fd \<notin> current_proc_fds s' p"
- using os alive' p_in notin_all Open None
- apply (erule_tac x = "E_fd p fd" in allE)
+ using os alive' p_in notin_cur Open None
+ apply (erule_tac x = "I_fd p fd" in allE)
apply (case_tac obj')
apply (auto dest:not_all_procs_prop3)
done
@@ -530,19 +583,20 @@
have p_in: "p \<in> current_procs s'" using os alive
apply (erule_tac x = "O_proc p" in allE)
by (auto simp:Open Some)
- have f_not_in: "f \<notin> current_files s'" using os alive' Open Some notin_all
- apply (erule_tac x = "E_file f" in allE)
- apply (case_tac obj')
- by auto
+ have f_not_in: "f \<notin> current_files s'" using os alive' Open Some notin_cur nodel
+ apply (erule_tac x = "I_file f" in allE)
+ by (case_tac obj', auto simp:current_files_simps)
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)
+ using os alive' p_in Open Some notin_cur
+ apply (erule_tac x = "I_fd p fd" in allE)
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
- apply (erule_tac x = "E_inum inum" in allE)
- by (case_tac obj', auto)
+ using os alive' Open Some notin_cur nodel
+ apply (erule_tac x = "I_inum inum" in allE)
+ apply (case_tac obj', auto)
+ apply (auto simp add:current_inode_nums_def current_file_inums_def split:if_splits)
+ done
have "os_grant s' e" using p_in pf_in parent f_not_in fd_not_in inum_not_in os
by (simp add:Open Some hungs)
moreover have "grant s' e"
@@ -780,10 +834,10 @@
from pf_in_s alive have pf_in: "is_dir s' pf"
apply (erule_tac x = "O_dir pf" in allE)
by (auto simp:Rmdir)
- have empty_in: "dir_is_empty s' f" using os Rmdir notin_all
+ have empty_in: "dir_is_empty s' f" using os Rmdir notin_cur
apply (clarsimp simp add:dir_is_empty_def f_in)
using alive'
- apply (erule_tac x = "E_file f'" in allE)
+ apply (erule_tac x = "I_file f'" in allE)
apply simp
apply (erule disjE)
apply (erule_tac x = f' in allE, simp)
@@ -797,6 +851,16 @@
apply (erule_tac x = pf in allE)
apply (drule_tac f = pf in is_dir_in_current)
apply (simp add:noJ_Anc)
+
+ apply (clarsimp)
+ apply (drule_tac f' = f in parent_ancen)
+ apply (simp, rule notI, simp add:noJ_Anc)
+ apply (case_tac "f = pf")
+ using vd' Rmdir
+ apply (simp_all add:is_dir_rmdir)
+ apply (erule_tac x = pf in allE)
+ apply (drule_tac f = pf in is_dir_in_current)
+ apply (simp add:noJ_Anc)
done
have "os_grant s' e" using p_in f_in os empty_in
by (simp add:Rmdir hungs)
@@ -851,13 +915,15 @@
have p_in: "p \<in> current_procs s'" using os alive
apply (erule_tac x = "O_proc p" in allE)
by (auto simp:Mkdir)
- have f_not_in: "f \<notin> current_files s'" using os alive' Mkdir notin_all
- apply (erule_tac x = "E_file f" in allE)
- by (auto)
+ have f_not_in: "f \<notin> current_files s'"
+ using os alive' Mkdir notin_cur
+ apply (erule_tac x = "I_file f" in allE)
+ by (auto simp:current_files_simps)
have inum_not_in: "inum \<notin> current_inode_nums s'"
- using os alive' Mkdir notin_all
- apply (erule_tac x = "E_inum inum" in allE)
- by (auto)
+ using os alive' Mkdir notin_cur
+ apply (erule_tac x = "I_inum inum" in allE)
+ apply (auto simp:current_inode_nums_def current_file_inums_def split:if_splits)
+ done
have "os_grant s' e" using p_in pf_in parent f_not_in os inum_not_in
by (simp add:Mkdir hungs)
moreover have "grant s' e"
@@ -903,9 +969,11 @@
have p_in: "p \<in> current_procs s'" using os alive
apply (erule_tac x = "O_proc p" in allE)
by (auto simp:LinkHard)
- have f'_not_in: "f' \<notin> current_files s'" using os alive' LinkHard notin_all
- apply (erule_tac x = "E_file f'" in allE)
- by (auto simp:LinkHard)
+ have f'_not_in: "f' \<notin> current_files s'"
+ using os alive' LinkHard notin_cur vd'
+ apply (erule_tac x = "I_file f'" in allE)
+ apply (auto simp:LinkHard current_files_simps)
+ done
have f_in: "is_file s' f" using os alive
apply (erule_tac x = "O_file f" in allE)
by (auto simp:LinkHard)
@@ -1004,9 +1072,13 @@
have p_in: "p \<in> current_procs s'" using os alive
apply (erule_tac x = "O_proc p" in allE)
by (auto simp:CreateMsgq)
- have q_not_in: "q \<notin> current_msgqs s'" using os alive' CreateMsgq notin_all
- apply (erule_tac x = "E_msgq q" in allE)
- by auto
+ have q_not_in: "q \<notin> current_msgqs s'"
+ using os alive' CreateMsgq notin_cur nodel vd
+ apply (erule_tac x = "I_msgq q" in allE)
+ apply (auto split:t_enrich_obj.splits)
+ apply (drule nums_of_recv_0, simp+)
+ apply (drule new_msgq_1, simp+)
+ done
have "os_grant s' e" using p_in q_not_in by (simp add:CreateMsgq)
moreover have "grant s' e"
proof-
@@ -1062,9 +1134,12 @@
have q_in: "q \<in> current_msgqs s'" using os alive
apply (erule_tac x = "O_msgq q" in allE)
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)
+ have m_not_in: "m \<notin> set (msgs_of_queue s' q)"
+ using os alive' notin_cur SendMsg q_in nodel vd
+ apply (erule_tac x = "I_msg q m" in allE)
apply (case_tac obj', auto dest:not_all_msgqs_prop3)
+ apply (drule nums_of_recv_0, simp+)
+ apply (drule new_msgq_1, simp+)
done
have "os_grant s' e" using p_in q_in m_not_in sms_remain os
by (simp add:SendMsg)
--- a/no_shm_selinux/Enrich2.thy Wed Jan 01 23:00:24 2014 +0800
+++ b/no_shm_selinux/Enrich2.thy Mon Jan 06 23:07:51 2014 +0800
@@ -39,7 +39,7 @@
done
lemma enrich_msgq_cur_inof:
- "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+ "\<lbrakk>no_del_event s; valid s\<rbrakk>
\<Longrightarrow> inum_of_file (enrich_msgq s q q') f = inum_of_file s f"
apply (induct s arbitrary:f, simp)
apply (frule vt_grant_os, frule vd_cons, case_tac a)
@@ -47,7 +47,7 @@
done
lemma enrich_msgq_cur_inos:
- "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+ "\<lbrakk>no_del_event s; valid s\<rbrakk>
\<Longrightarrow> inum_of_socket (enrich_msgq s q q') = inum_of_socket s"
apply (rule ext)
apply (induct s, simp)
@@ -56,20 +56,20 @@
done
lemma enrich_msgq_cur_inos':
- "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+ "\<lbrakk>no_del_event s; valid s\<rbrakk>
\<Longrightarrow> inum_of_socket (enrich_msgq s q q') sock = inum_of_socket s sock"
apply (simp add:enrich_msgq_cur_inos)
done
lemma enrich_msgq_cur_inums:
- "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+ "\<lbrakk>no_del_event s; valid s\<rbrakk>
\<Longrightarrow> current_inode_nums (enrich_msgq s q q') = current_inode_nums s"
apply (auto simp:current_inode_nums_def current_file_inums_def
current_sock_inums_def enrich_msgq_cur_inof enrich_msgq_cur_inos)
done
lemma enrich_msgq_cur_itag:
- "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+ "\<lbrakk>no_del_event s; valid s\<rbrakk>
\<Longrightarrow> itag_of_inum (enrich_msgq s q q') = itag_of_inum s"
apply (rule ext)
apply (induct s, simp)
@@ -78,7 +78,7 @@
done
lemma enrich_msgq_cur_tcps:
- "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+ "\<lbrakk>no_del_event s; valid s\<rbrakk>
\<Longrightarrow> is_tcp_sock (enrich_msgq s q q') = is_tcp_sock s"
apply (rule ext)
apply (auto simp:is_tcp_sock_def enrich_msgq_cur_itag enrich_msgq_cur_inos
@@ -86,7 +86,7 @@
done
lemma enrich_msgq_cur_udps:
- "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+ "\<lbrakk>no_del_event s; valid s\<rbrakk>
\<Longrightarrow> is_udp_sock (enrich_msgq s q q') = is_udp_sock s"
apply (rule ext)
apply (auto simp:is_udp_sock_def enrich_msgq_cur_itag enrich_msgq_cur_inos
@@ -94,7 +94,7 @@
done
lemma enrich_msgq_cur_msgqs:
- "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+ "\<lbrakk>q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
\<Longrightarrow> current_msgqs (enrich_msgq s q q') = current_msgqs s \<union> {q'}"
apply (induct s, simp)
apply (frule vt_grant_os, frule vd_cons)
@@ -103,17 +103,17 @@
lemma enrich_msgq_cur_msgs:
"\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
- \<Longrightarrow> msgs_of_queue (enrich_msgq s q q') = (msgs_of_queue s) (q' := msgs_of_queue s q)"
+ \<Longrightarrow> msgs_of_queue (enrich_msgq s q q') = (msgs_of_queue s) (q' := msgs_of_queue s q)"
apply (rule ext, simp, rule conjI, rule impI)
apply (simp add:enrich_msgq_duq_sms)
-apply (rule impI)
+apply (rule impI)
apply (induct s, simp)
apply (frule vt_grant_os, frule vd_cons)
apply (case_tac a, auto)
done
lemma enrich_msgq_cur_procs:
- "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+ "\<lbrakk>no_del_event s; valid s\<rbrakk>
\<Longrightarrow> current_procs (enrich_msgq s q q') = current_procs s"
apply (induct s, simp)
apply (frule vt_grant_os, frule vd_cons)
@@ -121,14 +121,14 @@
done
lemma enrich_msgq_cur_files:
- "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+ "\<lbrakk>no_del_event s; valid s\<rbrakk>
\<Longrightarrow> current_files (enrich_msgq s q q') = current_files s"
apply (auto simp:current_files_def)
apply (simp add:enrich_msgq_cur_inof)+
done
lemma enrich_msgq_cur_fds:
- "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+ "\<lbrakk>no_del_event s; valid s\<rbrakk>
\<Longrightarrow> current_proc_fds (enrich_msgq s q q') = current_proc_fds s"
apply (induct s, simp)
apply (frule vt_grant_os, frule vd_cons, case_tac a)
@@ -136,7 +136,7 @@
done
lemma enrich_msgq_filefd:
- "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+ "\<lbrakk>no_del_event s; valid s\<rbrakk>
\<Longrightarrow> file_of_proc_fd (enrich_msgq s q q') = file_of_proc_fd s"
apply (rule ext, rule ext)
apply (induct s, simp)
@@ -145,7 +145,7 @@
done
lemma enrich_msgq_flagfd:
- "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+ "\<lbrakk>no_del_event s; valid s\<rbrakk>
\<Longrightarrow> flags_of_proc_fd (enrich_msgq s q q') = flags_of_proc_fd s"
apply (rule ext, rule ext)
apply (induct s, simp)
@@ -154,7 +154,7 @@
done
lemma enrich_msgq_proc_fds:
- "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+ "\<lbrakk>no_del_event s; valid s\<rbrakk>
\<Longrightarrow> proc_file_fds (enrich_msgq s q q') = proc_file_fds s"
apply (auto simp:proc_file_fds_def enrich_msgq_filefd)
done
@@ -168,7 +168,7 @@
done
lemma enrich_msgq_is_file:
- "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+ "\<lbrakk>no_del_event s; valid s\<rbrakk>
\<Longrightarrow> is_file (enrich_msgq s q q') = is_file s"
apply (rule ext)
apply (auto simp add:is_file_def enrich_msgq_cur_itag enrich_msgq_cur_inof
@@ -176,7 +176,7 @@
done
lemma enrich_msgq_is_dir:
- "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+ "\<lbrakk>no_del_event s; valid s\<rbrakk>
\<Longrightarrow> is_dir (enrich_msgq s q q') = is_dir s"
apply (rule ext)
apply (auto simp add:is_dir_def enrich_msgq_cur_itag enrich_msgq_cur_inof
@@ -204,30 +204,29 @@
done
(* enrich s target_proc duplicated_pro *)
-fun enrich_proc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> t_state"
+fun enrich_proc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> nat \<Rightarrow> t_state"
where
- "enrich_proc [] tp dp = []"
-| "enrich_proc (Execve p f fds # s) tp dp = (
+ "enrich_proc [] tp dp n = []"
+| "enrich_proc (Execve p f fds # s) tp dp n = (
if (tp = p)
- then Execve dp f (fds \<inter> proc_file_fds s p) # Execve p f fds # (enrich_proc s tp dp)
- else Execve p f fds # (enrich_proc s tp dp))"
-| "enrich_proc (Clone p p' fds # s) tp dp = (
+ then Execve dp f (fds \<inter> proc_file_fds s p) # Execve p f fds # (enrich_proc s tp dp n)
+ else Execve p f fds # (enrich_proc s tp dp n))"
+| "enrich_proc (Clone p p' fds # s) tp dp n = (
if (tp = p')
then Clone p dp (fds \<inter> proc_file_fds s p) # Clone p p' fds # s
- else Clone p p' fds # (enrich_proc s tp dp))"
-| "enrich_proc (Open p f flags fd opt # s) tp dp = (
+ else Clone p p' fds # (enrich_proc s tp dp n))"
+| "enrich_proc (Open p f flags fd opt # s) tp dp n= (
if (tp = p)
- then Open dp f (remove_create_flag flags) fd None # Open p f flags fd opt # (enrich_proc s tp dp)
- else Open p f flags fd opt # (enrich_proc s tp dp))"
-| "enrich_proc (ReadFile p fd # s) tp dp = (
+ then Open dp f (remove_create_flag flags) fd None # Open p f flags fd opt # (enrich_proc s tp dp n)
+ else Open p f flags fd opt # (enrich_proc s tp dp n))"
+| "enrich_proc (ReadFile p fd # s) tp dp n = (
if (tp = p)
- then ReadFile dp fd # ReadFile p fd # (enrich_proc s tp dp)
- else ReadFile p fd # (enrich_proc s tp dp))"
-| "enrich_proc (RecvMsg p q m # s) tp dp = (
+ then ReadFile dp fd # ReadFile p fd # (enrich_proc s tp dp n)
+ else ReadFile p fd # (enrich_proc s tp dp n))"
+| "enrich_proc (RecvMsg p q m # s) tp dp n = (
if (tp = p)
- then let dq = new_msgq (enrich_proc s tp dp) in
- RecvMsg dp dq m # RecvMsg p q m # (enrich_msgq (enrich_proc s tp dp) q dq)
- else RecvMsg p q m # (enrich_proc s tp dp))"
+ then RecvMsg dp n m # RecvMsg p q m # (enrich_msgq (enrich_proc s tp dp (n+1)) q n)
+ else RecvMsg p q m # (enrich_proc s tp dp n))"
(*
| "enrich_proc (CloseFd p fd # s) tp dp = (
if (tp = p \<and> fd \<in> proc_file_fds s p)
@@ -252,7 +251,7 @@
if (tp = p) then Exit p # s
else Exit p # (enrich_proc s tp dp))"
*)
-| "enrich_proc (e # s) tp dp = e # (enrich_proc s tp dp)"
+| "enrich_proc (e # s) tp dp n = e # (enrich_proc s tp dp n)"
definition is_created_proc:: "t_state \<Rightarrow> t_process \<Rightarrow> bool"
where
@@ -304,47 +303,74 @@
done
lemma enrich_proc_dup_in:
- "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk>
- \<Longrightarrow> p' \<in> current_procs (enrich_proc s p p')"
+ "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
+ \<Longrightarrow> p' \<in> current_procs (enrich_proc s p p' i)"
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_def dest:not_all_procs_prop3)
-done
+apply (case_tac a)
+apply ( auto simp:is_created_proc_def Let_def enrich_msgq_cur_procs
+ dest:not_all_procs_prop3)
+sorry
lemma enrich_proc_dup_ffd:
"\<lbrakk>file_of_proc_fd s p fd = Some f; is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk>
- \<Longrightarrow> file_of_proc_fd (enrich_proc s p p') p' fd = Some f"
+ \<Longrightarrow> file_of_proc_fd (enrich_proc s p p' i) p' fd = Some f"
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_def proc_file_fds_def
+apply (case_tac a, auto simp:is_created_proc_def proc_file_fds_def Let_def
dest:not_all_procs_prop3 split:if_splits option.splits)
-done
+sorry
lemma enrich_proc_dup_ffd':
- "\<lbrakk>file_of_proc_fd (enrich_proc s p p') p' fd = Some f; is_created_proc s p; p' \<notin> all_procs s;
+ "\<lbrakk>file_of_proc_fd (enrich_proc s p p' i) p' 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 s p fd = Some f"
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_def proc_file_fds_def
+apply (case_tac a, auto simp:is_created_proc_def proc_file_fds_def Let_def
dest:not_all_procs_prop3 split:if_splits option.splits)
-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
+sorry
lemma enrich_proc_dup_ffd_eq:
"\<lbrakk>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') p' fd = file_of_proc_fd s p fd"
+ \<Longrightarrow> file_of_proc_fd (enrich_proc s p p' i) p' fd = file_of_proc_fd s p fd"
apply (case_tac "file_of_proc_fd s p fd")
-apply (case_tac[!] "file_of_proc_fd (enrich_proc s p p') p' fd")
+apply (case_tac[!] "file_of_proc_fd (enrich_proc s p p' i) p' fd")
apply (auto dest:enrich_proc_dup_ffd enrich_proc_dup_ffd')
+apply (drule_tac i = i in enrich_proc_dup_ffd, simp+)
done
+lemma enrich_proc_cur_msgqs:
+ "\<lbrakk>valid s\<rbrakk> \<Longrightarrow> current_msgqs (enrich_proc s p p' i) = current_msgqs s \<union> {q'. q' \<ge> new_msgq s \<and> q' \<le> new_msgq s + (nums_of_recvmsg s p) - 1}"
+apply (induct s, simp)
+apply (auto)[1]
+apply (drule new_msgq_1, simp, simp)
+apply (frule vt_grant_os, frule vd_cons)
+sorry
+
+lemma enrich_proc_not_alive:
+ "\<lbrakk>enrich_not_alive s (E_proc p' (new_msgq s) (new_msgq s + (nums_of_recvmsg s p) - 1)) 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' (new_msgq s)) (E_proc p' (new_msgq s) (new_msgq s + (nums_of_recvmsg s p) - 1)) obj"
+apply (case_tac obj, simp_all)
+prefer 5
+apply (simp add:enrich_proc_cur_msgqs)
+apply (rule impI, rule notI)
+apply simp
+apply (auto)[1]
+defer
+apply simp
+apply (rule impI, rule notI)
+defer
+apply (subgoal_tac "new_msgq s \<noteq> 0")
+apply simp
+apply arith
+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)
+defer
+apply (rule impI, rule notI)
+sorry
+
lemma enrich_proc_dup_fflags:
"\<lbrakk>flags_of_proc_fd s p fd = Some flag; is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk>
@@ -352,9 +378,9 @@
flags_of_proc_fd (enrich_proc s p p') p' fd = Some flag"
apply (induct s arbitrary:p, simp add:is_created_proc_def)
apply (frule vt_grant_os, frule vd_cons)
-apply (case_tac a, auto simp:is_created_proc_def proc_file_fds_def is_creat_flag_def
+apply (case_tac a, auto simp:is_created_proc_def proc_file_fds_def is_creat_flag_def Let_def
dest:not_all_procs_prop3 split:if_splits option.splits)
-done
+sorry
lemma enrich_proc_dup_ffds:
"\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
@@ -374,7 +400,14 @@
apply (frule not_all_procs_prop3)
apply (frule vd_cons, frule vt_grant_os, case_tac a)
apply (auto split:if_splits option.splits dest:proc_fd_in_fds set_mp not_all_procs_prop3
- simp:proc_file_fds_def is_created_proc_def)
+ simp:proc_file_fds_def is_created_proc_def Let_def)
+sorry
+
+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:
@@ -383,8 +416,8 @@
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
+apply (auto split:option.splits simp del:grant.simps simp add:Let_def)
+sorry
lemma not_all_procs_sock:
"\<lbrakk>p' \<notin> all_procs s; valid s\<rbrakk> \<Longrightarrow> inum_of_socket s (p', fd) = None"
@@ -399,11 +432,11 @@
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 (case_tac a, auto split:option.splits simp:not_all_procs_sock Let_def)
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
+sorry
lemma enrich_proc_cur_inums:
"\<lbrakk>p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
@@ -418,8 +451,8 @@
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
+apply (case_tac a, auto split:option.splits t_socket_type.splits simp:Let_def)
+sorry
lemma enrich_proc_cur_tcps:
"\<lbrakk>valid s; no_del_event s; p' \<notin> all_procs s\<rbrakk>
@@ -433,31 +466,32 @@
"\<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
+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"
+ "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> q \<in> current_msgqs (enrich_proc s p p')"
apply (induct s, simp)
apply (frule vt_grant_os, frule vd_cons)
-apply (case_tac a, auto)
-done
+apply (case_tac a, auto simp:Let_def)
+sorry
lemma enrich_proc_cur_msgs:
- "valid s \<Longrightarrow> msgs_of_queue (enrich_proc s p p') q = msgs_of_queue s q "
+ "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> msgs_of_queue (enrich_proc s p p') q = msgs_of_queue s q"
apply (induct s, simp)
+apply (frule_tac p = p and p' = p' in enrich_proc_cur_msgqs, simp)
apply (frule vt_grant_os, frule vd_cons)
-apply (case_tac a, auto)
-done
+apply (case_tac a, auto simp:Let_def)
+sorry
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
+apply (case_tac a, auto simp:is_created_proc_simps Let_def)
+sorry
lemma enrich_proc_cur_files:
"\<lbrakk>valid s; no_del_event s\<rbrakk> \<Longrightarrow> current_files (enrich_proc s p p') = current_files s"
@@ -472,18 +506,22 @@
apply (frule vt_grant_os, frule vd_cons)
apply (frule not_all_procs_prop3)
apply (case_tac a)
+sorry
+(*
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 (frule not_all_procs_prop3) sorry (*
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>
@@ -497,7 +535,9 @@
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
+defer
+apply (rule impI, rule notI)
+sorry
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>
@@ -507,7 +547,7 @@
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
+sorry
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>
@@ -517,14 +557,14 @@
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
+sorry
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
+sorry
lemma enrich_proc_is_file:
"\<lbrakk>valid s; no_del_event s; p' \<notin> all_procs s\<rbrakk>