--- a/no_shm_selinux/Enrich2.thy	Tue Dec 31 14:57:13 2013 +0800
+++ b/no_shm_selinux/Enrich2.thy	Wed Jan 01 23:00:24 2014 +0800
@@ -1,11 +1,10 @@
-theory Enrich
+theory Enrich2
 imports Main Flask Static Init_prop Valid_prop Tainted_prop Delete_prop Co2sobj_prop S2ss_prop S2ss_prop2
  Temp Enrich Proc_fd_of_file_prop
 begin
 
 context tainting_s begin
 
-
 fun enrich_msgq :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msgq \<Rightarrow> t_state"
 where
   "enrich_msgq [] tq dq = []"
@@ -23,7 +22,186 @@
      else RecvMsg p q m # (enrich_msgq s tq dq))"
 | "enrich_msgq (e # s) tq dq = e # (enrich_msgq s tq dq)"
 
+lemma enrich_msgq_duq_in:
+  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> q' \<in> current_msgqs (enrich_msgq s q q')"
+apply (induct s, simp)
+apply (frule vt_grant_os, frule vd_cons, case_tac a)
+apply auto
+done
 
+lemma enrich_msgq_duq_sms:
+  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> msgs_of_queue (enrich_msgq s q q') q' = msgs_of_queue s q"
+apply (induct s, simp)
+apply (frule vt_grant_os, frule vd_cons, case_tac a)
+apply auto
+done
+
+lemma enrich_msgq_cur_inof:
+  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> inum_of_file (enrich_msgq s q q') f = inum_of_file s f"
+apply (induct s arbitrary:f, simp)
+apply (frule vt_grant_os, frule vd_cons, case_tac a)
+apply (auto split:option.splits)
+done
+
+lemma enrich_msgq_cur_inos:
+  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> inum_of_socket (enrich_msgq s q q') = inum_of_socket s"
+apply (rule ext)
+apply (induct s, simp)
+apply (frule vt_grant_os, frule vd_cons, case_tac a)
+apply (auto split:option.splits)
+done
+
+lemma enrich_msgq_cur_inos':
+  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> inum_of_socket (enrich_msgq s q q') sock = inum_of_socket s sock"
+apply (simp add:enrich_msgq_cur_inos)
+done
+
+lemma enrich_msgq_cur_inums:
+  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> current_inode_nums (enrich_msgq s q q') = current_inode_nums s"
+apply (auto simp:current_inode_nums_def current_file_inums_def 
+  current_sock_inums_def enrich_msgq_cur_inof enrich_msgq_cur_inos)
+done
+
+lemma enrich_msgq_cur_itag:
+  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> itag_of_inum (enrich_msgq s q q') = itag_of_inum s"
+apply (rule ext)
+apply (induct s, simp)
+apply (frule vt_grant_os, frule vd_cons, case_tac a)
+apply (auto split:option.splits t_socket_type.splits)
+done
+
+lemma enrich_msgq_cur_tcps:
+  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> is_tcp_sock (enrich_msgq s q q') = is_tcp_sock s"
+apply (rule ext)
+apply (auto simp:is_tcp_sock_def enrich_msgq_cur_itag enrich_msgq_cur_inos
+  split:option.splits t_inode_tag.splits)
+done
+
+lemma enrich_msgq_cur_udps:
+  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> is_udp_sock (enrich_msgq s q q') = is_udp_sock s"
+apply (rule ext)
+apply (auto simp:is_udp_sock_def enrich_msgq_cur_itag enrich_msgq_cur_inos
+  split:option.splits t_inode_tag.splits)
+done
+
+lemma enrich_msgq_cur_msgqs:
+  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> current_msgqs (enrich_msgq s q q') = current_msgqs s \<union> {q'}"
+apply (induct s, simp)
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac a, auto)
+done
+
+lemma enrich_msgq_cur_msgs:
+  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> msgs_of_queue (enrich_msgq s q q') =  (msgs_of_queue s) (q' := msgs_of_queue s q)"
+apply (rule ext, simp, rule conjI, rule impI)
+apply (simp add:enrich_msgq_duq_sms)
+apply (rule impI)
+apply (induct s, simp)
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac a, auto)
+done
+
+lemma enrich_msgq_cur_procs:
+  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> current_procs (enrich_msgq s q q') = current_procs s"
+apply (induct s, simp)
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac a, auto)
+done
+  
+lemma enrich_msgq_cur_files:
+  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> current_files (enrich_msgq s q q') = current_files s"
+apply (auto simp:current_files_def)
+apply (simp add:enrich_msgq_cur_inof)+
+done
+
+lemma enrich_msgq_cur_fds:
+  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> current_proc_fds (enrich_msgq s q q') = current_proc_fds s"
+apply (induct s, simp)
+apply (frule vt_grant_os, frule vd_cons, case_tac a)
+apply auto
+done
+
+lemma enrich_msgq_filefd:
+  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> file_of_proc_fd (enrich_msgq s q q') = file_of_proc_fd s"
+apply (rule ext, rule ext)
+apply (induct s, simp)
+apply (frule vt_grant_os, frule vd_cons, case_tac a)
+apply auto
+done
+
+lemma enrich_msgq_flagfd:
+  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> flags_of_proc_fd (enrich_msgq s q q') = flags_of_proc_fd s"
+apply (rule ext, rule ext)
+apply (induct s, simp)
+apply (frule vt_grant_os, frule vd_cons, case_tac a)
+apply auto
+done
+
+lemma enrich_msgq_proc_fds:
+  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> proc_file_fds (enrich_msgq s q q') = proc_file_fds s"
+apply (auto simp:proc_file_fds_def enrich_msgq_filefd)
+done
+
+lemma enrich_msgq_hungs:
+  "\<lbrakk>no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> files_hung_by_del (enrich_msgq s q q') = files_hung_by_del s"
+apply (induct s, simp)
+apply (frule vt_grant_os, frule vd_cons, case_tac a)
+apply (auto simp:files_hung_by_del.simps)
+done
+  
+lemma enrich_msgq_is_file:
+  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> is_file (enrich_msgq s q q') = is_file s"
+apply (rule ext)
+apply (auto simp add:is_file_def enrich_msgq_cur_itag enrich_msgq_cur_inof
+  split:option.splits t_inode_tag.splits)
+done
+
+lemma enrich_msgq_is_dir:
+  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> is_dir (enrich_msgq s q q') = is_dir s"
+apply (rule ext)
+apply (auto simp add:is_dir_def enrich_msgq_cur_itag enrich_msgq_cur_inof
+  split:option.splits t_inode_tag.splits)
+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"
+apply (case_tac obj)
+apply (simp_all add:enrich_msgq_is_file enrich_msgq_is_dir enrich_msgq_cur_msgqs 
+  enrich_msgq_cur_msgs enrich_msgq_cur_procs enrich_msgq_cur_fds
+  enrich_msgq_cur_tcps enrich_msgq_cur_udps)
+apply (rule impI, simp)
+done
+
+lemma enrich_msgq_alive':
+  "\<lbrakk>alive (enrich_msgq s q q') obj; valid s; q \<in> current_msgqs s; q' \<notin> current_msgqs s; no_del_event s\<rbrakk>
+   \<Longrightarrow> alive s obj \<or> obj = O_msgq q' \<or> (\<exists> m. obj = O_msg q' m \<and> alive s (O_msg q m))"
+apply (case_tac obj)
+apply (simp_all add:enrich_msgq_is_file enrich_msgq_is_dir enrich_msgq_cur_msgqs 
+  enrich_msgq_cur_msgs enrich_msgq_cur_procs enrich_msgq_cur_fds
+  enrich_msgq_cur_tcps enrich_msgq_cur_udps)
+apply (auto split:if_splits)
+done
 
 (* enrich s target_proc duplicated_pro *)
 fun enrich_proc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> t_state"
@@ -45,6 +223,11 @@
      if (tp = p) 
      then ReadFile dp fd # ReadFile p fd # (enrich_proc s tp dp)
      else ReadFile p fd # (enrich_proc s tp dp))"
+| "enrich_proc (RecvMsg p q m # s) tp dp = (
+     if (tp = p) 
+     then let dq = new_msgq (enrich_proc s tp dp) in
+          RecvMsg dp dq m # RecvMsg p q m # (enrich_msgq (enrich_proc s tp dp) q dq)
+     else RecvMsg p q m # (enrich_proc s tp dp))"
 (*
 | "enrich_proc (CloseFd p fd # s) tp dp = (
      if (tp = p \<and> fd \<in> proc_file_fds s p)
@@ -1274,6 +1457,8 @@
     by simp
 qed
   
+lemma enrich_proc_s2ss:
+  "\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s\<rbrakk> \<Longrightarrow> s2ss (enrich_proc s p p') = s2ss s"
 
 lemma enrich_proc_valid:
   "\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s\<rbrakk> \<Longrightarrow> valid (enrich_proc s p p')"