--- 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)