
diff -r e832378a2ff2 -r ded3f83f6cb9 no_shm_selinux/Enrich.thy
--- 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)




