# HG changeset patch
# User chunhan
# Date 1381220483 -28800
# Node ID e934f9a697f52f1340c81e0e484871277249f4eb
# Parent  e3ad1b294fd9dcd758f5d77bf4ae4afa923cf595
s2ss_recvmsg

diff -r e3ad1b294fd9 -r e934f9a697f5 S2ss_prop.thy
--- a/S2ss_prop.thy	Fri Sep 27 11:36:51 2013 +0800
+++ b/S2ss_prop.thy	Tue Oct 08 16:21:23 2013 +0800
@@ -108,13 +108,53 @@
 apply (auto simp:co2sobj_clone alive_simps)
 done
 
+definition s2ss_shm_no_backup:: "t_state \<Rightarrow> t_process \<Rightarrow> t_static_state"
+where
+  "s2ss_shm_no_backup s pfrom \<equiv> {S_proc sp False | sp p. info_flow_shm s pfrom p \<and> cp2sproc s p = Some sp \<and>
+     (\<not> (\<exists> p'. \<not> info_flow_shm s pfrom p' \<and> p' \<in> current_procs s \<and> co2sobj s (O_proc p') = Some (S_proc sp False)))}"
+
 definition update_s2ss_shm:: "t_state \<Rightarrow> t_process \<Rightarrow> t_static_state" 
 where
   "update_s2ss_shm s pfrom \<equiv> s2ss s 
      \<union> {S_proc sp True| sp p. info_flow_shm s pfrom p \<and> cp2sproc s p = Some sp}
-     - {S_proc sp False | sp p. info_flow_shm s pfrom p \<and> cp2sproc s p = Some sp \<and> 
-           (\<not> (\<exists> p'. \<not> info_flow_shm s pfrom p' \<and> p' \<in> current_procs s \<and> 
-                cp2sproc s p' = Some sp \<and> O_proc p' \<notin> Tainted s))}"
+     - (s2ss_shm_no_backup s pfrom)"
+
+lemma s2ss_shm_no_bk_elim:
+  "\<lbrakk>S_proc sp False \<notin> s2ss_shm_no_backup s pfrom; co2sobj s (O_proc p) = Some (S_proc sp False); 
+    valid s; info_flow_shm s pfrom p\<rbrakk>
+   \<Longrightarrow> \<exists> p'. \<not> info_flow_shm s pfrom p' \<and> p' \<in> current_procs s \<and> co2sobj s (O_proc p') = Some (S_proc sp False)"
+apply (auto simp:s2ss_shm_no_backup_def co2sobj.simps tainted_eq_Tainted split:option.splits)
+apply (erule_tac x = p in allE, auto)
+apply (rule_tac x = p' in exI, auto)
+done
+
+lemma s2ss_shm_no_bk_intro1:
+  "\<lbrakk>co2sobj s' obj = Some x; \<forall> p. obj \<noteq> O_proc p\<rbrakk> \<Longrightarrow> x \<notin> s2ss_shm_no_backup s pfrom"
+apply (case_tac obj)
+apply (auto simp:co2sobj.simps s2ss_shm_no_backup_def split:option.splits)
+done
+
+lemma s2ss_shm_no_bk_intro2:
+  "\<lbrakk>co2sobj s' obj = Some x; obj \<in> Tainted s'; valid s'\<rbrakk> \<Longrightarrow> x \<notin> s2ss_shm_no_backup s pfrom"
+apply (case_tac obj)
+
+apply (auto simp:co2sobj.simps s2ss_shm_no_backup_def tainted_eq_Tainted split:option.splits)
+done
+
+lemma s2ss_shm_no_bk_intro3:
+  "\<lbrakk>co2sobj s (O_proc p) = Some x; \<not> info_flow_shm s pfrom p; p \<in> current_procs s
+   \<rbrakk> \<Longrightarrow> x \<notin> s2ss_shm_no_backup s pfrom"
+apply (auto simp add:s2ss_shm_no_backup_def split:option.splits)
+apply (rule_tac x = p in exI, simp)
+done
+
+lemma s2ss_shm_no_bk_intro4:
+  "\<lbrakk>co2sobj s (O_proc p) = Some x; info_flow_shm s pfrom p; 
+    \<not> info_flow_shm s pfrom p'; p' \<in> current_procs s; co2sobj s (O_proc p') = Some x\<rbrakk>
+   \<Longrightarrow> x \<notin> s2ss_shm_no_backup s pfrom"
+apply (rule notI)
+apply (auto simp add:s2ss_shm_no_backup_def co2sobj.simps split:option.splits)
+done  
 
 lemma Tainted_ptrace':
   "valid s \<Longrightarrow> Tainted (Ptrace p p' # s) = 
@@ -139,7 +179,7 @@
 lemma s2ss_ptrace1:
   "\<lbrakk>valid (Ptrace p p' # s); O_proc p \<in> Tainted s; O_proc p' \<notin> Tainted s\<rbrakk>
    \<Longrightarrow> s2ss (Ptrace p p' # s) = update_s2ss_shm s p'"
-unfolding update_s2ss_shm_def s2ss_def
+unfolding update_s2ss_shm_def s2ss_def s2ss_shm_no_backup_def 
 apply (frule vd_cons, rule set_eqI, rule iffI)
 apply (drule CollectD, (erule exE|erule conjE)+)
 apply (erule co2sobj_some_caseD)
@@ -203,7 +243,7 @@
 lemma s2ss_ptrace2:
   "\<lbrakk>valid (Ptrace p p' # s); O_proc p' \<in> Tainted s; O_proc p \<notin> Tainted s\<rbrakk>
    \<Longrightarrow> s2ss (Ptrace p p' # s) = update_s2ss_shm s p"
-unfolding update_s2ss_shm_def s2ss_def
+unfolding update_s2ss_shm_def s2ss_def s2ss_shm_no_backup_def
 apply (frule vd_cons, rule set_eqI, rule iffI)
 apply (drule CollectD, (erule exE|erule conjE)+)
 apply (erule co2sobj_some_caseD)
@@ -573,7 +613,7 @@
      | _      \<Rightarrow> {})"
 apply (frule vt_grant_os, frule vd_cons, clarsimp split:option.splits)
 apply (rule conjI, rule impI, rule impI, simp)
-unfolding update_s2ss_shm_def s2ss_def
+unfolding update_s2ss_shm_def s2ss_def s2ss_shm_no_backup_def
 apply (rule set_eqI, rule iffI)
 apply (drule CollectD, (erule exE|erule conjE)+)
 apply (erule co2sobj_some_caseD)
@@ -1965,13 +2005,573 @@
 apply (auto simp add:co2sobj_createmsgq alive_simps split:t_object.splits if_splits)
 done
 
-lemma s2ss_sendmsg:
+ML {*fun my_clarify_tac i = 
+REPEAT ((  rtac @{thm impI}
+   ORELSE' rtac @{thm allI}
+   ORELSE' rtac @{thm ballI}
+   ORELSE' rtac @{thm conjI}
+   ORELSE' etac @{thm conjE}
+   ORELSE' etac @{thm exE}
+   ORELSE' etac @{thm bexE}
+   ORELSE' etac @{thm disjE}) i)
+*}
+
+lemma s2ss_sendmsg: "valid (SendMsg p q m # s) \<Longrightarrow> s2ss (SendMsg p q m # s) = (
+  case (cq2smsgq s q, cq2smsgq (SendMsg p q m # s) q) of
+    (Some sq, Some sq') \<Rightarrow> update_s2ss_obj s (s2ss s) (O_msgq q) (S_msgq sq) (S_msgq sq')
+  | _  \<Rightarrow> {})"
+apply (frule vd_cons, frule vt_grant_os, clarsimp)
+apply (case_tac "cq2smsgq s q")
+apply (drule current_has_smsgq', simp+)
+apply (case_tac "cq2smsgq (SendMsg p q m # s) q")
+apply (drule current_has_smsgq', simp+)
+
+apply (simp add:update_s2ss_obj_def)
+apply (tactic {*my_clarify_tac 1*})
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_msgq q")
+apply (rule disjI1, simp add:co2sobj.simps)
+apply (rule disjI2, simp, rule_tac x = obj in exI)
+apply (simp add:co2sobj_sendmsg is_file_simps is_dir_simps split:t_object.splits if_splits)
+apply (simp add:co2sobj.simps)
+apply (simp add:co2sobj.simps)
+apply (simp add:co2sobj.simps)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_msgq q" in exI, simp add:co2sobj.simps)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_msgq q")
+apply (rule_tac x = obj' in exI)
+apply (simp add:co2sobj_sendmsg alive_sendmsg split:t_object.splits if_splits)
+apply (auto simp:co2sobj.simps)[1]
+apply (rule_tac x = obj in exI, simp add:co2sobj_sendmsg alive_sendmsg split:t_object.splits)
+apply (auto simp:co2sobj.simps)[1]
+
+apply (rule impI)
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_msgq q")
+apply (rule disjI1, simp add:co2sobj.simps)
+apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI)
+apply (simp add:co2sobj_sendmsg is_file_simps is_dir_simps split:t_object.splits if_splits)
+apply (simp add:co2sobj.simps)
+apply (simp add:co2sobj.simps)
+apply (simp add:co2sobj.simps)
+apply (rule notI, simp)
+apply (frule_tac obj = obj in co2sobj_smsgq_imp, erule exE, simp)
+apply (erule_tac x = obj in allE, simp add:co2sobj_sendmsg)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_msgq q" in exI, simp add:co2sobj.simps)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_msgq q")
+apply (simp add:co2sobj.simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_sendmsg alive_sendmsg split:t_object.splits)
+apply (auto simp:co2sobj.simps)[1]
+done
+
+lemma alive_co2sobj_removemsgq:
+  "\<lbrakk>alive s obj; valid (RemoveMsgq p q # s); co2sobj s obj = Some sobj; obj \<noteq> O_msgq q\<rbrakk> 
+   \<Longrightarrow> alive (RemoveMsgq p q # s) obj"
+apply (erule co2sobj_some_caseD)
+apply (auto simp:is_file_simps is_dir_simps)
+done
+
+lemma s2ss_removemsgq: "valid (RemoveMsgq p q # s) \<Longrightarrow> s2ss (RemoveMsgq p q # s) = 
+  (case (cq2smsgq s q) of
+     Some sq \<Rightarrow> del_s2ss_obj s (s2ss s) (O_msgq q) (S_msgq sq)
+   | _       \<Rightarrow> {})"
+apply (frule vd_cons, frule vt_grant_os, clarsimp)
+apply (split option.splits, rule conjI, rule impI)
+apply (drule current_has_smsgq', simp, simp)
+apply (rule allI, rule impI)
+
+apply (simp add:del_s2ss_obj_def)
+apply (tactic {*my_clarify_tac 1*})
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_msgq q", simp)
+apply (rule_tac x = obj in exI)
+apply (simp add:co2sobj_removemsgq alive_simps split:t_object.splits if_splits)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_msgq q", simp)
+apply (rule_tac x = obj' in exI)
+apply (frule_tac obj = obj' in co2sobj_smsgq_imp, erule exE)
+apply (simp add:co2sobj_removemsgq alive_simps split:t_object.splits if_splits)
+apply (simp add:co2sobj.simps)
+apply (rule_tac x = obj in exI)
+apply (simp add:co2sobj_removemsgq alive_co2sobj_removemsgq)
+
+apply (rule impI)
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_msgq q", simp)
+apply (simp, rule conjI, rule_tac x = obj in exI)
+apply (simp add:co2sobj_removemsgq alive_simps split:t_object.splits if_splits)
+apply (rule notI, simp, frule_tac obj = obj in co2sobj_smsgq_imp, erule exE)
+apply (erule_tac x = obj in allE, simp add:co2sobj_removemsgq alive_co2sobj_removemsgq)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_msgq q", simp)
+apply (simp add:co2sobj.simps)
+apply (rule_tac x = obj in exI)
+apply (simp add:co2sobj_removemsgq alive_co2sobj_removemsgq)
+done
+
+declare Product_Type.split_paired_Ex Product_Type.split_paired_All [simp del]
+
+lemma s2ss_shm_no_bk_elim':
+  "\<lbrakk>x \<notin> s2ss_shm_no_backup s pfrom; co2sobj s (O_proc p) = Some x; O_proc p \<notin> Tainted s;
+    valid s; info_flow_shm s pfrom p\<rbrakk>
+   \<Longrightarrow> \<exists> p'. \<not> info_flow_shm s pfrom p' \<and> p' \<in> current_procs s \<and> co2sobj s (O_proc p') = Some x"
+apply (auto simp:s2ss_shm_no_backup_def co2sobj.simps tainted_eq_Tainted split:option.splits)
+apply (erule_tac x = p in allE, auto)
+apply (rule_tac x = p' in exI, auto)
+done
+
+lemma s2ss_recvmsg: "valid (RecvMsg p q m # s) \<Longrightarrow> s2ss (RecvMsg p q m # s) = (
+  case (cq2smsgq s q, cq2smsgq (RecvMsg p q m # s) q) of
+    (Some sq, Some sq') \<Rightarrow> if (O_msg q m \<in> Tainted s \<and> O_proc p \<notin> Tainted s)
+                          then update_s2ss_obj s (update_s2ss_shm s p) (O_msgq q) (S_msgq sq) (S_msgq sq')
+                          else update_s2ss_obj s (s2ss s) (O_msgq q) (S_msgq sq) (S_msgq sq')
+  | _ \<Rightarrow> {})"
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac "cq2smsgq s q")
+apply (drule current_has_smsgq', simp, simp)
+apply (case_tac "cq2smsgq (RecvMsg p q m # s) q")
+apply (drule current_has_smsgq', simp, simp)
+apply (simp split:if_splits add:update_s2ss_obj_def)
+
+apply (tactic {*my_clarify_tac 1*})
+unfolding s2ss_def update_s2ss_shm_def
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_msgq q")
+apply (rule disjI1, simp add:co2sobj.simps)
+apply (rule disjI2)
+apply (rule DiffI)
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac "info_flow_shm s p pa")
+apply (rule UnI2)
+apply (simp add:co2sobj_recvmsg del:Product_Type.split_paired_Ex
+  split:t_object.splits option.splits)
+apply (rule_tac x = ab in exI, simp, rule_tac x = pa in exI, simp)
+apply (rule UnI1,simp, rule_tac x = obj in exI)
+apply (simp add:co2sobj_recvmsg split:t_object.splits option.splits)
+apply (rule UnI1,simp, rule_tac x = obj in exI)
+apply (simp add:co2sobj_recvmsg is_file_simps split:t_object.splits option.splits)
+apply (rule UnI1, simp,rule_tac x = obj in exI)
+apply (simp add:co2sobj_recvmsg split:t_object.splits option.splits)
+apply (rule UnI1, simp,rule_tac x = obj in exI)
+apply (simp add:co2sobj_recvmsg is_dir_simps split:t_object.splits option.splits)
+apply (rule UnI1, simp, rule_tac x = obj in exI)
+apply (simp add:co2sobj_recvmsg split:t_object.splits option.splits if_splits)
+apply (rule notI, simp add:s2ss_shm_no_backup_def del:Product_Type.split_paired_Ex)
+apply (erule exE|erule conjE)+
+apply (simp, frule co2sobj_sproc_imp, erule exE, simp)
+apply (simp add:co2sobj_recvmsg split:if_splits option.splits)
+apply (erule_tac x = paa in allE, simp)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_msgq q" in exI, simp add:co2sobj.simps alive_recvmsg)
+apply (tactic {*my_setiff_tac 1*}, erule UnE)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_msgq q")
+apply (rule_tac x = obj' in exI)
+apply (simp add:co2sobj_recvmsg is_file_simps is_dir_simps alive_recvmsg 
+  split:t_object.splits if_splits option.splits)
+apply (auto simp:co2sobj.simps is_file_simps is_dir_simps)[1]
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac "info_flow_shm s p pa \<and> O_proc pa \<notin> Tainted s")
+apply (drule_tac p = pa in s2ss_shm_no_bk_elim', simp+)
+apply (erule exE|erule conjE)+
+apply (rule_tac x = "O_proc p'" in exI)
+apply (simp add:co2sobj_recvmsg alive_simps)
+apply (rule_tac x = obj in exI)
+apply (case_tac "info_flow_shm s p pa", simp)
+apply (frule_tac obj = obj in co2sobj_recvmsg, simp+)
+apply (case_tac "cp2sproc s pa", simp add:co2sobj.simps)
+apply (simp, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (simp, frule_tac obj = obj in co2sobj_recvmsg, simp+)
+apply (rule_tac x = obj in exI, simp add:co2sobj_recvmsg alive_simps)
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_recvmsg, simp split:t_object.splits)
+apply (simp split:t_object.splits)
+apply (rule_tac x = obj in exI, simp add:co2sobj_recvmsg is_dir_simps) 
+apply (rule_tac x = obj in exI, simp add:co2sobj_recvmsg) 
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_proc pa" in exI)
+apply (frule_tac obj = "O_proc pa" in co2sobj_recvmsg)
+apply (simp add:info_shm_flow_in_procs, simp add:info_shm_flow_in_procs)
+
+apply (tactic {*my_clarify_tac 1*})
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_msgq q")
+apply (rule disjI1, simp add:co2sobj.simps)
+apply (rule disjI2, simp, rule_tac x = obj in exI)
+apply (simp add:co2sobj_recvmsg is_file_simps is_dir_simps split:t_object.splits if_splits option.splits)
+apply (simp add:co2sobj.simps tainted_eq_Tainted info_flow_shm_Tainted)
+apply (simp add:co2sobj.simps)
+apply (simp add:co2sobj.simps)
+apply (case_tac "msgs_of_queue s q", simp, simp)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_msgq q" in exI)
+apply (simp add:co2sobj.simps)
+apply (tactic {*my_setiff_tac 1 *})
+apply (case_tac "obj = O_msgq q")
+apply (rule_tac x = obj' in exI)
+apply (simp add:co2sobj_recvmsg is_file_simps is_dir_simps alive_recvmsg 
+  split:t_object.splits if_splits option.splits)
+apply (auto simp:co2sobj.simps is_file_simps is_dir_simps)[1]
+apply (rule_tac x = obj in exI)
+apply (simp add:co2sobj_recvmsg is_file_simps is_dir_simps alive_recvmsg 
+  split:t_object.splits if_splits option.splits)
+apply (auto simp:co2sobj.simps is_file_simps is_dir_simps tainted_eq_Tainted info_flow_shm_Tainted)[1]
+
+apply (tactic {*my_clarify_tac 1*})
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_msgq q")
+apply (rule disjI1, simp add:co2sobj.simps)
+apply (rule disjI2)
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac "info_flow_shm s p pa")
+apply (case_tac "O_proc pa \<in> Tainted s")
+apply (rule DiffI, rule UnI1, simp)
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp split:option.splits)
+apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (erule s2ss_shm_no_bk_intro2, simp, simp)
+apply (rule DiffI, rule UnI2, rule CollectI)
+apply (simp only:co2sobj.simps tainted_eq_Tainted split:option.splits, simp)
+apply (rule_tac x = ab in exI, simp)
+apply (rule_tac x = pa in exI, simp add:cp2sproc_other)
+apply (rule s2ss_shm_no_bk_intro2, simp, simp, simp)
+apply (rule DiffI, rule UnI1, simp)
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp split:option.splits)
+apply (rule_tac p = pa in s2ss_shm_no_bk_intro3)
+apply (simp add:co2sobj_recvmsg, simp, simp)
+apply (rule DiffI, rule UnI1, simp)
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp add:is_file_simps split:option.splits)
+apply (simp add:co2sobj_recvmsg s2ss_shm_no_bk_intro1)
+apply (rule DiffI, rule UnI1, simp)
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp split:option.splits)
+apply (simp add:co2sobj_recvmsg s2ss_shm_no_bk_intro1)
+apply (rule DiffI, rule UnI1, simp)
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp add:is_dir_simps split:option.splits)
+apply (simp add:co2sobj_recvmsg s2ss_shm_no_bk_intro1)
+apply (rule DiffI, rule UnI1, simp)
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp split:option.splits)
+apply (simp add:co2sobj_recvmsg s2ss_shm_no_bk_intro1)
 
-lemma s2ss_recvmsg:
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_msgq q" in exI)
+apply (simp add:co2sobj.simps)
+apply (tactic {*my_setiff_tac 1*})
+apply (erule UnE, tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_msgq q")
+apply (rule_tac x = obj' in exI)
+apply (simp add:co2sobj_recvmsg is_file_simps is_dir_simps alive_recvmsg 
+  split:t_object.splits if_splits option.splits)
+apply (auto simp:co2sobj.simps is_file_simps is_dir_simps)[1]
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac "info_flow_shm s p pa \<and> O_proc pa \<notin> Tainted s")
+apply (drule_tac p = pa in s2ss_shm_no_bk_elim', simp+)
+apply (erule exE|erule conjE)+
+apply (rule_tac x = "O_proc p'" in exI)
+apply (simp add:co2sobj_recvmsg alive_simps)
+apply (rule_tac x = obj in exI)
+apply (case_tac "info_flow_shm s p pa", simp)
+apply (frule_tac obj = obj in co2sobj_recvmsg, simp+)
+apply (case_tac "cp2sproc s pa", simp add:co2sobj.simps)
+apply (simp, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (simp, frule_tac obj = obj in co2sobj_recvmsg, simp+)
+apply (rule_tac x = obj in exI, simp add:co2sobj_recvmsg alive_simps)
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_recvmsg, simp split:t_object.splits)
+apply (simp split:t_object.splits)
+apply (rule_tac x = obj in exI, simp add:co2sobj_recvmsg is_dir_simps) 
+apply (rule_tac x = obj in exI, simp add:co2sobj_recvmsg) 
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_proc pa" in exI)
+apply (frule_tac obj = "O_proc pa" in co2sobj_recvmsg)
+apply (simp add:info_shm_flow_in_procs, simp add:info_shm_flow_in_procs)
+
+apply (rule impI, tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_msgq q")
+apply (rule disjI1, simp add:co2sobj.simps)
+apply (rule disjI2, simp, rule conjI)
+apply (rule_tac x = obj in exI)
+apply (simp add:co2sobj_recvmsg is_file_simps is_dir_simps alive_recvmsg 
+  split:t_object.splits if_splits option.splits)
+apply (simp add:co2sobj.simps tainted_eq_Tainted info_flow_shm_Tainted)
+apply (simp add:co2sobj_recvmsg)
+apply (simp add:alive_recvmsg split:if_splits)
+apply (erule_tac x = obj in allE, simp split:t_object.splits if_splits option.splits)
+apply (rule notI, simp add:co2sobj.simps)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_msgq q" in exI)
+apply (simp add:co2sobj.simps)
+apply (tactic {*my_setiff_tac 1*})
+apply simp
+apply (tactic {*my_clarify_tac 1*})
+apply (case_tac "obj = O_msgq q")
+apply (rule_tac x = obj' in exI)
+apply (simp add:co2sobj_recvmsg is_file_simps is_dir_simps alive_recvmsg 
+  split:t_object.splits if_splits option.splits)
+apply (auto simp:co2sobj.simps is_file_simps is_dir_simps)[1]
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_recvmsg)
+apply (simp add:alive_recvmsg, rule notI, simp add:co2sobj.simps)
+apply (rule conjI)
+apply (simp add:alive_recvmsg, rule notI, simp add:co2sobj.simps)
+apply (auto simp:co2sobj.simps tainted_eq_Tainted split:t_object.splits option.splits if_splits)[1]
+
+apply (tactic {*my_clarify_tac 1*})
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_msgq q")
+apply (rule disjI1, simp add:co2sobj.simps)
+apply (rule disjI2)
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac "info_flow_shm s p pa")
+apply (case_tac "O_proc pa \<in> Tainted s")
+apply (rule DiffI, rule UnI1, simp)
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp split:option.splits)
+apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (erule s2ss_shm_no_bk_intro2, simp, simp)
+apply (rule DiffI, rule UnI2, rule CollectI)
+apply (simp only:co2sobj.simps tainted_eq_Tainted split:option.splits, simp)
+apply (rule_tac x = ab in exI, simp)
+apply (rule_tac x = pa in exI, simp add:cp2sproc_other)
+apply (rule s2ss_shm_no_bk_intro2, simp, simp, simp)
+apply (rule DiffI, rule UnI1, simp)
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp split:option.splits)
+apply (rule_tac p = pa in s2ss_shm_no_bk_intro3)
+apply (simp add:co2sobj_recvmsg, simp, simp)
+apply (rule DiffI, rule UnI1, simp)
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp add:is_file_simps split:option.splits)
+apply (simp add:co2sobj_recvmsg s2ss_shm_no_bk_intro1)
+apply (rule DiffI, rule UnI1, simp)
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp split:option.splits)
+apply (simp add:co2sobj_recvmsg s2ss_shm_no_bk_intro1)
+apply (rule DiffI, rule UnI1, simp)
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp add:is_dir_simps split:option.splits)
+apply (simp add:co2sobj_recvmsg s2ss_shm_no_bk_intro1)
+apply (rule DiffI, rule UnI1, simp)
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp split:option.splits)
+apply (simp add:co2sobj_recvmsg s2ss_shm_no_bk_intro1)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_msgq q" in exI)
+apply (simp add:co2sobj.simps)
+apply (tactic {*my_setiff_tac 1*})
+apply (erule UnE, tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_msgq q")
+apply (rule_tac x = obj' in exI)
+apply (simp add:co2sobj_recvmsg is_file_simps is_dir_simps alive_recvmsg 
+  split:t_object.splits if_splits option.splits)
+apply (auto simp:co2sobj.simps is_file_simps is_dir_simps)[1]
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac "info_flow_shm s p pa \<and> O_proc pa \<notin> Tainted s")
+apply (drule_tac p = pa in s2ss_shm_no_bk_elim', simp+)
+apply (erule exE|erule conjE)+
+apply (rule_tac x = "O_proc p'" in exI)
+apply (simp add:co2sobj_recvmsg alive_simps)
+apply (rule_tac x = obj in exI)
+apply (case_tac "info_flow_shm s p pa", simp)
+apply (frule_tac obj = obj in co2sobj_recvmsg, simp+)
+apply (case_tac "cp2sproc s pa", simp add:co2sobj.simps)
+apply (simp, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (simp, frule_tac obj = obj in co2sobj_recvmsg, simp+)
+apply (rule_tac x = obj in exI, simp add:co2sobj_recvmsg alive_simps)
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_recvmsg, simp split:t_object.splits)
+apply (simp split:t_object.splits)
+apply (rule_tac x = obj in exI, simp add:co2sobj_recvmsg is_dir_simps) 
+apply (rule_tac x = obj in exI, simp add:co2sobj_recvmsg) 
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_proc pa" in exI)
+apply (frule_tac obj = "O_proc pa" in co2sobj_recvmsg)
+apply (simp add:info_shm_flow_in_procs, simp add:info_shm_flow_in_procs)
 
-lemma s2ss_removemsgq:
+apply (rule impI, tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_msgq q")
+apply (rule disjI1, simp add:co2sobj.simps)
+apply (rule disjI2, simp)
+apply (rule_tac x = obj in exI)
+apply (simp add:co2sobj_recvmsg is_file_simps is_dir_simps alive_recvmsg 
+  split:t_object.splits if_splits option.splits)
+apply (simp add:co2sobj.simps tainted_eq_Tainted info_flow_shm_Tainted)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_msgq q" in exI)
+apply (simp add:co2sobj.simps)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_msgq q")
+apply (rule_tac x = obj' in exI)
+apply (simp add:co2sobj_recvmsg is_file_simps is_dir_simps alive_recvmsg 
+  split:t_object.splits if_splits option.splits)
+apply (auto simp:co2sobj.simps is_file_simps is_dir_simps)[1]
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_recvmsg)
+apply (simp add:alive_recvmsg, rule notI, simp add:co2sobj.simps)
+apply (rule conjI)
+apply (simp add:alive_recvmsg, rule notI, simp add:co2sobj.simps)
+apply (auto simp:co2sobj.simps tainted_eq_Tainted split:t_object.splits option.splits if_splits)[1]
+
+apply (tactic {*my_clarify_tac 1*})
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_msgq q")
+apply (rule disjI1, simp add:co2sobj.simps)
+apply (rule disjI2)
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac "info_flow_shm s p pa")
+apply (case_tac "O_proc pa \<in> Tainted s")
+apply (rule DiffI, rule DiffI, rule UnI1, simp)
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp split:option.splits)
+apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (erule s2ss_shm_no_bk_intro2, simp, simp)
+apply (simp, rule notI, simp add:co2sobj.simps split:option.splits)
+apply (rule DiffI, rule DiffI, rule UnI2, rule CollectI)
+apply (simp only:co2sobj.simps tainted_eq_Tainted split:option.splits, simp)
+apply (rule_tac x = ab in exI, simp)
+apply (rule_tac x = pa in exI, simp add:cp2sproc_other)
+apply (rule s2ss_shm_no_bk_intro2, simp, simp, simp)
+apply (simp, rule notI, simp add:co2sobj.simps split:option.splits)
+apply (rule DiffI, rule DiffI, rule UnI1, simp)
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp split:option.splits)
+apply (rule_tac p = pa in s2ss_shm_no_bk_intro3)
+apply (simp add:co2sobj_recvmsg, simp, simp)
+apply (simp, rule notI, simp add:co2sobj.simps split:option.splits)
+apply (rule DiffI, rule DiffI, rule UnI1, simp)
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp add:is_file_simps split:option.splits)
+apply (simp add:co2sobj_recvmsg s2ss_shm_no_bk_intro1)
+apply (simp, rule notI, simp add:co2sobj.simps split:option.splits)
+apply (rule DiffI, rule DiffI, rule UnI1, simp)
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp split:option.splits)
+apply (simp add:co2sobj_recvmsg s2ss_shm_no_bk_intro1)
+apply (simp, rule notI, simp add:co2sobj.simps split:option.splits)
+apply (rule DiffI, rule DiffI, rule UnI1, simp)
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp add:is_dir_simps split:option.splits)
+apply (simp add:co2sobj_recvmsg s2ss_shm_no_bk_intro1)
+apply (simp, rule notI, simp add:co2sobj.simps split:option.splits)
+apply (rule DiffI, rule DiffI, rule UnI1, simp)
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp split:option.splits)
+apply (simp add:co2sobj_recvmsg s2ss_shm_no_bk_intro1)
+apply (simp, rule notI, erule_tac x = obj in allE, simp)
+apply (simp add:co2sobj_recvmsg)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_msgq q" in exI)
+apply (simp add:co2sobj.simps)
+apply (tactic {*my_setiff_tac 1*})
+apply (erule UnE, tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_msgq q")
+apply (simp add:co2sobj.simps)
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac "info_flow_shm s p pa \<and> O_proc pa \<notin> Tainted s")
+apply (drule_tac p = pa in s2ss_shm_no_bk_elim', simp+)
+apply (erule exE|erule conjE)+
+apply (rule_tac x = "O_proc p'" in exI)
+apply (simp add:co2sobj_recvmsg alive_simps)
+apply (rule_tac x = obj in exI)
+apply (case_tac "info_flow_shm s p pa", simp)
+apply (frule_tac obj = obj in co2sobj_recvmsg, simp+)
+apply (case_tac "cp2sproc s pa", simp add:co2sobj.simps)
+apply (simp, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (simp, frule_tac obj = obj in co2sobj_recvmsg, simp+)
+apply (rule_tac x = obj in exI, simp add:co2sobj_recvmsg alive_simps)
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_recvmsg, simp split:t_object.splits)
+apply (simp split:t_object.splits)
+apply (rule_tac x = obj in exI, simp add:co2sobj_recvmsg is_dir_simps) 
+apply (rule_tac x = obj in exI, simp add:co2sobj_recvmsg) 
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_proc pa" in exI)
+apply (frule_tac obj = "O_proc pa" in co2sobj_recvmsg)
+apply (simp add:info_shm_flow_in_procs, simp add:info_shm_flow_in_procs)
+
+apply (rule impI, tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_msgq q")
+apply (rule disjI1, simp add:co2sobj.simps)
+apply (rule disjI2, simp, rule conjI)
+apply (rule_tac x = obj in exI)
+apply (simp add:co2sobj_recvmsg is_file_simps is_dir_simps alive_recvmsg 
+  split:t_object.splits if_splits option.splits)
+apply (simp add:co2sobj.simps tainted_eq_Tainted info_flow_shm_Tainted)
+apply (rule notI, simp)
+apply (frule co2sobj_smsgq_imp, erule exE, simp)
+apply (simp add:co2sobj_recvmsg)
+apply (erule_tac x = obj in allE, simp)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_msgq q" in exI)
+apply (simp add:co2sobj.simps)
+apply (tactic {*my_setiff_tac 1*})
+apply (simp, erule exE, erule conjE)
+apply (case_tac "obj = O_msgq q")
+apply (simp add:co2sobj.simps)
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_recvmsg)
+apply (simp add:alive_recvmsg, rule notI, simp add:co2sobj.simps)
+apply (rule conjI)
+apply (simp add:alive_recvmsg, rule notI, simp add:co2sobj.simps)
+apply (auto simp:co2sobj.simps tainted_eq_Tainted intro: info_flow_shm_Tainted 
+split:t_object.splits option.splits if_splits)[1]
+done
+
+lemma s2ss_createshm:
+  "valid (CreateShM p h # s) \<Longrightarrow> s2ss (CreateShM p h # s) = 
+     (case (ch2sshm (CreateShM p h # s) h) of
+        Some sh \<Rightarrow> s2ss s \<union> {S_shm sh}
+      | _       \<Rightarrow> {})"
+apply (frule vd_cons, frule vt_grant_os, clarsimp)
+apply (case_tac "ch2sshm (CreateShM p h # s) h")
+apply (drule current_shm_has_sh', simp+)
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_shm h")
+apply (rule disjI1, simp add:co2sobj.simps)
+apply (rule disjI2, simp, rule_tac x = obj in exI)
+apply (simp add:co2sobj_createshm is_file_simps is_dir_simps split:t_object.splits if_splits)
+apply (simp add:co2sobj.simps)
+apply (simp add:co2sobj.simps)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_shm h" in exI, simp add:co2sobj.simps)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_shm h")
+apply simp
+apply (rule_tac x = obj in exI)
+apply (auto simp add:co2sobj_createshm alive_simps split:t_object.splits if_splits)
+done
+
+
+lemma s2ss_attach1:
+  "valid (Attach p h SHM_RDWR # s) \<Longrightarrow> s2ss (Attach p h SHM_RDWR # s) = "
+
+lemma s2ss_attach1:
+  "valid (Attach p h SHM_RDONLY # s) \<Longrightarrow> s2ss (Attach p h SHM_RDONLY # s) = "
+
+lemma s2ss_attach1:
+  "valid (Attach p h flag # s) \<Longrightarrow> s2ss (Attach p h flag # s) = "
+
+lemma s2ss_Detach:
+  "valid (Detach p h # s) \<Longrightarrow> s2ss (Detach p h # s) = "
+
+lemma s2ss_deleteshm:
+  "valid (DeleteShM p h # s) \<Longrightarrow> s2ss (DeleteShM p h # s)"
+
 
 lemmas s2ss_simps = s2ss_execve s2ss_clone s2ss_ptrace s2ss_kill s2ss_exit s2ss_open
   s2ss_readfile s2ss_writefile s2ss_closefd s2ss_unlink s2ss_rmdir s2ss_linkhard
-  s2ss_truncate s2ss_createmsgq 
+  s2ss_truncate s2ss_createmsgq s2ss_sendmsg s2ss_removemsgq s2ss_recvmsg
+  s2ss_createshm