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