enrich msgq done; but find bugs of s2ss, it should only considerate 'appropriate' objects, not including msg/fd ...
--- a/no_shm_selinux/Enrich2.thy Tue Jan 07 22:04:06 2014 +0800
+++ b/no_shm_selinux/Enrich2.thy Wed Jan 08 18:40:38 2014 +0800
@@ -183,6 +183,41 @@
split:option.splits t_inode_tag.splits)
done
+lemma enrich_msgq_sameinode:
+ "\<lbrakk>no_del_event s; valid s\<rbrakk>
+ \<Longrightarrow> (f \<in> same_inode_files (enrich_msgq s q q') f') = (f \<in> same_inode_files s f')"
+apply (induct s, simp)
+apply (simp add:same_inode_files_def)
+apply (auto simp:enrich_msgq_is_file enrich_msgq_cur_inof)
+done
+
+lemma enrich_msgq_tainted_aux1:
+ "\<lbrakk>no_del_event s; q \<in> current_msgqs s; q' \<notin> current_msgqs s; valid s\<rbrakk>
+ \<Longrightarrow> (tainted s \<union> {O_msg q' m| m. O_msg q m \<in> tainted s}) \<subseteq> tainted (enrich_msgq s q q')"
+apply (induct s, simp)
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac a)
+apply (auto split:option.splits if_splits dest:tainted_in_current
+ simp:enrich_msgq_filefd enrich_msgq_sameinode)
+done
+
+lemma enrich_msgq_tainted_aux2:
+ "\<lbrakk>no_del_event s; q \<in> current_msgqs s; q' \<notin> current_msgqs s; valid s; valid (enrich_msgq s q q')\<rbrakk>
+ \<Longrightarrow> tainted (enrich_msgq s q q') \<subseteq> (tainted s \<union> {O_msg q' m| m. O_msg q m \<in> tainted s})"
+apply (induct s, simp)
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac a)
+apply (auto split:option.splits if_splits simp:enrich_msgq_filefd enrich_msgq_sameinode
+ dest:tainted_in_current vd_cons)
+apply (drule_tac vd_cons)+
+apply (simp)
+apply (drule set_mp)
+apply simp
+apply simp
+apply (drule_tac s = s in tainted_in_current)
+apply simp+
+done
+
lemma enrich_msgq_alive:
"\<lbrakk>alive s obj; valid s; q \<in> current_msgqs s; q' \<notin> current_msgqs s; no_del_event s\<rbrakk>
\<Longrightarrow> alive (enrich_msgq s q q') obj"
@@ -211,13 +246,13 @@
enrich_msgq_cur_procs enrich_msgq_cur_inums enrich_msgq_cur_msgqs enrich_msgq_cur_msgs)
done
-lemma enrich_msgq_no_del:
- "\<lbrakk>no_del_event s\<rbrakk> \<Longrightarrow> no_del_event (enrich_msgq s q q')"
+lemma enrich_msgq_nodel:
+ "no_del_event (enrich_msgq s q q') = no_del_event s"
apply (induct s, simp)
by (case_tac a, auto)
-lemma nodel_died_proc:
- "no_del_event s \<Longrightarrow> \<not> died (O_proc p) s"
+lemma enrich_msgq_died_proc:
+ "died (O_proc p) (enrich_msgq s q q') = died (O_proc p) s"
apply (induct s, simp)
by (case_tac a, auto)
@@ -267,7 +302,8 @@
(\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile (enrich_msgq s q q') f = cf2sfile s f) \<and>
(\<forall> tq. tq \<in> current_msgqs s \<longrightarrow> cq2smsgq (enrich_msgq s q q') tq = cq2smsgq s tq) \<and>
(\<forall> tp fd. fd \<in> proc_file_fds s tp \<longrightarrow> cfd2sfd (enrich_msgq s q q') tp fd = cfd2sfd s tp fd) \<and>
- (cq2smsgq (enrich_msgq s q q') q' = cq2smsgq s q)"
+ (cq2smsgq (enrich_msgq s q q') q' = cq2smsgq s q) \<and>
+ (tainted (enrich_msgq s q q') = (tainted s \<union> {O_msg q' m| m. O_msg q m \<in> tainted s}))"
proof (induct s)
case Nil
thus ?case by (auto)
@@ -285,7 +321,8 @@
(\<forall>f. f \<in> current_files s \<longrightarrow> cf2sfile (enrich_msgq s q q') f = cf2sfile s f) \<and>
(\<forall>tq. tq \<in> current_msgqs s \<longrightarrow> cq2smsgq (enrich_msgq s q q') tq = cq2smsgq s tq) \<and>
(\<forall>tp fd. fd \<in> proc_file_fds s tp \<longrightarrow> cfd2sfd (enrich_msgq s q q') tp fd = cfd2sfd s tp fd) \<and>
- (cq2smsgq (enrich_msgq s q q') q' = cq2smsgq s q)"
+ (cq2smsgq (enrich_msgq s q q') q' = cq2smsgq s q) \<and>
+ (tainted (enrich_msgq s q q') = (tainted s \<union> {O_msg q' m| m. O_msg q m \<in> tainted s}))"
by auto
from pre have pre_vd: "q \<in> current_msgqs s \<Longrightarrow> valid (enrich_msgq s q q')" by simp
@@ -750,30 +787,181 @@
done
qed
- thm psec_cons
- thm cp2sproc_def
have pfds_cons: "\<And> tp. tp \<in> current_procs (e # s) \<Longrightarrow>
cpfd2sfds (enrich_msgq (e # s) q q') tp = cpfd2sfds (e # s) tp"
- apply (auto simp add:cpfd2sfds_def)
- sorry
+ apply (auto simp add:cpfd2sfds_def proc_file_fds_def)
+ apply (rule_tac x = fd in exI, rule conjI, rule_tac x = f in exI)
+ prefer 3
+ apply (rule_tac x = fd in exI, rule conjI, rule_tac x = f in exI)
+ apply (auto simp:sfd_cons enrich_msgq_filefd nodel_cons vd_cons')
+ done
+ have tainted_cons: "tainted (enrich_msgq (e # s) q q') =
+ (tainted (e # s) \<union> {O_msg q' m | m. O_msg q m \<in> tainted (e # s)})"
+ apply (rule equalityI)
+ using nodel_cons curq_cons curq'_cons vd_cons' vd_enrich_cons
+ apply (rule enrich_msgq_tainted_aux2)
+ using nodel_cons curq_cons curq'_cons vd_cons'
+ apply (rule enrich_msgq_tainted_aux1)
+ done
+ have pre_tainted: "q \<in> current_msgqs s \<Longrightarrow> tainted (enrich_msgq s q q') =
+ (tainted s \<union> {O_msg q' m| m. O_msg q m \<in> tainted s})" by (simp add:pre)
+
have "\<forall>tp fd. fd \<in> proc_file_fds (e # s) tp \<longrightarrow> cfd2sfd (enrich_msgq (e # s) q q') tp fd = cfd2sfd (e # s) tp fd"
by (auto simp:proc_file_fds_def elim!:sfd_cons)
moreover
have "\<forall>tp. tp \<in> current_procs (e # s) \<longrightarrow> cp2sproc (enrich_msgq (e # s) q q') tp = cp2sproc (e # s) tp"
- apply (auto simp:cp2sproc_def pfds_cons psec_cons split:option.splits)
- sorry
+ by (auto simp:cp2sproc_def pfds_cons psec_cons enrich_msgq_died_proc split:option.splits)
moreover
have "\<forall>tq. tq \<in> current_msgqs (e # s) \<longrightarrow> cq2smsgq (enrich_msgq (e # s) q q') tq = cq2smsgq (e # s) tq"
- sorry
+ proof clarify
+ fix tq assume a1: "tq \<in> current_msgqs (e # s)"
+
+ have curqsec: "\<And> tq. \<lbrakk>tq \<in> current_msgqs s; q \<in> current_msgqs s\<rbrakk> \<Longrightarrow>
+ sectxt_of_obj (enrich_msgq s q q') (O_msgq tq) = sectxt_of_obj s (O_msgq tq)"
+ using pre_vd vd
+ apply (frule_tac pre_sq, simp)
+ by (auto simp:cq2smsgq_def split:option.splits if_splits dest!:current_has_sec' current_has_sms')
+ have cursms: "\<And> q''. \<lbrakk>q'' \<in> current_msgqs s; q \<in> current_msgqs s\<rbrakk> \<Longrightarrow>
+ cqm2sms (enrich_msgq s q q') q'' (msgs_of_queue (enrich_msgq s q q') q'') =
+ cqm2sms s q'' (msgs_of_queue s q'')"
+ using pre_vd vd
+ apply (frule_tac pre_sq, simp)
+ by (auto simp:cq2smsgq_def split:option.splits if_splits dest!:current_has_sec' current_has_sms')
+ have qsec_cons: "sectxt_of_obj (enrich_msgq (e # s) q q') (O_msgq tq) = sectxt_of_obj (e # s) (O_msgq tq)"
+ using curq_cons vd_enrich_cons vd_cons' os pre_vd nodel_cons vd curq'_cons curq_cons a1
+ apply (case_tac e)
+ apply (auto intro:curqsec simp:sectxt_of_obj_simps curpsec split:option.splits dest!:current_has_sec')
+ apply (frule vd_cons) defer apply (frule vd_cons)
+ apply (auto intro:curqsec simp:sectxt_of_obj_simps)
+ done
+ have sms_cons: "cqm2sms (enrich_msgq (e # s) q q') tq (msgs_of_queue (enrich_msgq (e # s) q q') tq) =
+ cqm2sms (e # s) tq (msgs_of_queue (e # s) tq)"
+ proof-
+ have b1: "\<And> p q'' m. e = SendMsg p q'' m \<Longrightarrow>
+ cqm2sms (enrich_msgq (e # s) q q') tq (msgs_of_queue (enrich_msgq (e # s) q q') tq) =
+ cqm2sms (e # s) tq (msgs_of_queue (e # s) tq)"
+ apply (case_tac e)
+ using a1 curq_cons vd_enrich_cons vd_cons' os pre_vd nodel_cons vd curq'_cons
+ apply (auto simp:sectxt_of_obj_simps cqm2sms_simps curpsec qsec_cons curqsec cursms pre_tainted
+ split:option.splits dest!:current_has_sec' current_has_sms' simp del:cqm2sms.simps)
+ apply (tactic {*ALLGOALS (ftac @{thm vd_cons})*})
+ apply (auto simp:sectxt_of_obj_simps cqm2sms_simps curpsec qsec_cons curqsec cursms pre_tainted
+ split:option.splits dest!:current_has_sec' current_has_sms' simp del:cqm2sms.simps)
+ done
+ have b2: "\<And> p q''. e = CreateMsgq p q'' \<Longrightarrow>
+ cqm2sms (enrich_msgq (e # s) q q') tq (msgs_of_queue (enrich_msgq (e # s) q q') tq) =
+ cqm2sms (e # s) tq (msgs_of_queue (e # s) tq)"
+ using a1 curq_cons curq'_cons vd_enrich_cons vd_cons'
+ apply (auto simp:cqm2sms_simps intro:cursms)
+ apply (auto simp:cqm2sms.simps)
+ done
+ have b3: "\<And> p q'' m. e = RecvMsg p q'' m \<Longrightarrow>
+ cqm2sms (enrich_msgq (e # s) q q') tq (msgs_of_queue (enrich_msgq (e # s) q q') tq) =
+ cqm2sms (e # s) tq (msgs_of_queue (e # s) tq)"
+ using a1 curq_cons vd_enrich_cons vd_cons' os pre_vd nodel_cons vd curq'_cons
+ apply (auto simp:sectxt_of_obj_simps cqm2sms_simps curpsec qsec_cons curqsec cursms
+ split:option.splits dest!:current_has_sec' current_has_sms' simp del:cqm2sms.simps)
+ apply (frule vd_cons) defer apply (frule vd_cons)
+ apply (auto simp:sectxt_of_obj_simps cqm2sms_simps curpsec qsec_cons curqsec cursms
+ split:option.splits dest!:current_has_sec' current_has_sms' simp del:cqm2sms.simps)
+ done
+ show "cqm2sms (enrich_msgq (e # s) q q') tq (msgs_of_queue (enrich_msgq (e # s) q q') tq) =
+ cqm2sms (e # s) tq (msgs_of_queue (e # s) tq)"
+ apply (case_tac e)
+ prefer 15 apply (erule b2)
+ prefer 15 apply (erule b1)
+ prefer 15 apply (erule b3)
+ using curq_cons vd_enrich_cons vd_cons' os pre_vd nodel_cons vd curq'_cons a1
+ apply (auto intro:cursms simp:sectxt_of_obj_simps cqm2sms_simps curpsec qsec_cons curqsec
+ split:option.splits dest!:current_has_sec' current_has_sms' simp del:cqm2sms.simps)
+ done
+ qed
+
+ show "cq2smsgq (enrich_msgq (e # s) q q') tq = cq2smsgq (e # s) tq"
+ using a1 curq_cons
+ apply (simp add:cq2smsgq_def qsec_cons sms_cons)
+ done
+ qed
moreover
have "cq2smsgq (enrich_msgq (e # s) q q') q' = cq2smsgq (e # s) q"
- sorry
- ultimately show ?case using vd_enrich_cons sf_cons
+ proof-
+ have duqsec: "q \<in> current_msgqs s \<Longrightarrow>
+ sectxt_of_obj (enrich_msgq s q q') (O_msgq q') = sectxt_of_obj s (O_msgq q)"
+ apply (frule pre_duq) using vd
+ by (auto simp:cq2smsgq_def split:option.splits if_splits dest!:current_has_sec' current_has_sms')
+ have duqsms: "q \<in> current_msgqs s \<Longrightarrow>
+ cqm2sms (enrich_msgq s q q') q' (msgs_of_queue (enrich_msgq s q q') q') =
+ cqm2sms s q (msgs_of_queue s q)"
+ apply (frule pre_duq) using vd
+ by (auto simp:cq2smsgq_def split:option.splits if_splits dest!:current_has_sec' current_has_sms')
+ have qsec_cons: "sectxt_of_obj (enrich_msgq (e # s) q q') (O_msgq q') = sectxt_of_obj (e # s) (O_msgq q)"
+ using curq_cons vd_enrich_cons vd_cons' os pre_vd nodel_cons vd curq'_cons curq_cons
+ apply (case_tac e)
+ apply (auto simp:duqsec sectxt_of_obj_simps curpsec split:option.splits dest!:current_has_sec')
+ apply (frule vd_cons) defer apply (frule vd_cons)
+ apply (auto intro:duqsec simp:sectxt_of_obj_simps)
+ done
+ have sms_cons: "cqm2sms (enrich_msgq (e # s) q q') q' (msgs_of_queue (enrich_msgq (e # s) q q') q') =
+ cqm2sms (e # s) q (msgs_of_queue (e # s) q)"
+ proof-
+ have b1: "\<And> p q'' m. e = SendMsg p q'' m \<Longrightarrow>
+ cqm2sms (enrich_msgq (e # s) q q') q' (msgs_of_queue (enrich_msgq (e # s) q q') q') =
+ cqm2sms (e # s) q (msgs_of_queue (e # s) q)"
+ apply (case_tac e)
+ using curq_cons vd_enrich_cons vd_cons' os pre_vd nodel_cons vd curq'_cons
+ apply (auto simp:sectxt_of_obj_simps cqm2sms_simps curpsec qsec_cons duqsec duqsms pre_tainted
+ enrich_msgq_cur_procs enrich_msgq_cur_msgqs
+ split:option.splits dest!:current_has_sec' current_has_sms' simp del:cqm2sms.simps)
+ apply (tactic {*ALLGOALS (ftac @{thm vd_cons})*})
+ apply (auto simp:sectxt_of_obj_simps cqm2sms_simps curpsec qsec_cons duqsec duqsms pre_tainted
+ enrich_msgq_cur_procs enrich_msgq_cur_msgqs dest:tainted_in_current
+ split:option.splits dest!:current_has_sec' current_has_sms' simp del:cqm2sms.simps)
+ done
+ have b2: "\<And> p q''. e = CreateMsgq p q'' \<Longrightarrow>
+ cqm2sms (enrich_msgq (e # s) q q') q' (msgs_of_queue (enrich_msgq (e # s) q q') q') =
+ cqm2sms (e # s) q (msgs_of_queue (e # s) q)"
+ using curq_cons curq'_cons vd_enrich_cons vd_cons'
+ apply (auto simp:cqm2sms_simps intro:duqsms)
+ apply (auto simp:cqm2sms.simps)
+ done
+ have b3: "\<And> p q'' m. e = RecvMsg p q'' m \<Longrightarrow>
+ cqm2sms (enrich_msgq (e # s) q q') q' (msgs_of_queue (enrich_msgq (e # s) q q') q') =
+ cqm2sms (e # s) q (msgs_of_queue (e # s) q)"
+ using curq_cons vd_enrich_cons vd_cons' os pre_vd nodel_cons vd curq'_cons
+ apply (auto simp:sectxt_of_obj_simps cqm2sms_simps curpsec qsec_cons duqsec duqsms pre_tainted
+ enrich_msgq_cur_procs enrich_msgq_cur_msgqs
+ split:option.splits dest!:current_has_sec' current_has_sms' simp del:cqm2sms.simps)
+ apply (tactic {*ALLGOALS (ftac @{thm vd_cons})*})
+ apply (auto simp:sectxt_of_obj_simps cqm2sms_simps curpsec qsec_cons duqsec duqsms pre_tainted
+ enrich_msgq_cur_procs enrich_msgq_cur_msgqs dest:tainted_in_current
+ split:option.splits dest!:current_has_sec' current_has_sms' simp del:cqm2sms.simps)
+ done
+ show ?thesis
+ apply (case_tac e)
+ prefer 15 apply (erule b2)
+ prefer 15 apply (erule b1)
+ prefer 15 apply (erule b3)
+ using curq_cons vd_enrich_cons vd_cons' os pre_vd nodel_cons vd curq'_cons
+ apply (auto intro:duqsms simp:sectxt_of_obj_simps cqm2sms_simps curpsec qsec_cons duqsms
+ split:option.splits dest!:current_has_sec' current_has_sms' simp del:cqm2sms.simps)
+ done
+ qed
+ show ?thesis
+ using curq_cons
+ apply (simp add:cq2smsgq_def qsec_cons sms_cons)
+ done
+ qed
+ ultimately show ?case using vd_enrich_cons sf_cons tainted_cons
by auto
qed
+
+lemma enrich_msgq_s2ss:
+ ""
+
+
thm cp2sproc_def
(* enrich s target_proc duplicated_pro *)