# HG changeset patch
# User chunhan
# Date 1389177638 -28800
# Node ID 1a1df29d3507e7d5f4fefbe07a3949798680166e
# Parent  003cac7b8bf59fdad3af49d132a1251a13172037
enrich msgq done; but find bugs of s2ss, it should only considerate 'appropriate' objects, not including msg/fd ...

diff -r 003cac7b8bf5 -r 1a1df29d3507 no_shm_selinux/Enrich2.thy
--- 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 *)