--- a/S2ss_prop.thy	Thu Sep 26 22:08:32 2013 +0800
+++ b/S2ss_prop.thy	Fri Sep 27 11:36:51 2013 +0800
@@ -774,9 +774,9 @@
       then ss \<union> {sobj'}
       else ss - {sobj} \<union> {sobj'})"
 
-definition update_s2ss_sfile :: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_file \<Rightarrow> t_sfile \<Rightarrow> t_static_state"
+definition update_s2ss_sfile_del :: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_file \<Rightarrow> t_sfile \<Rightarrow> t_static_state"
 where 
-  "update_s2ss_sfile s ss f sf \<equiv> 
+  "update_s2ss_sfile_del s ss f sf \<equiv> 
      if (same_inode_files s f = {f})
      then ss
      else ss \<union> {S_file (cf2sfiles s f - {sf}) (O_file f \<in> Tainted s)}"
@@ -787,8 +787,8 @@
      (if (\<exists> f' \<in> same_inode_files s f. f' \<noteq> f \<and> cf2sfile s f' = Some sf)
       then ss
       else if (\<exists> f'. is_file s f' \<and> f' \<notin> same_inode_files s f \<and> co2sobj s (O_file f') = co2sobj s (O_file f))
-           then update_s2ss_sfile s ss f sf
-           else update_s2ss_sfile s (ss - {S_file (cf2sfiles s f) (O_file f \<in> Tainted s)}) f sf)"
+           then update_s2ss_sfile_del s ss f sf
+           else update_s2ss_sfile_del s (ss - {S_file (cf2sfiles s f) (O_file f \<in> Tainted s)}) f sf)"
 
 lemma alive_co2sobj_closefd1:
   "\<lbrakk>alive s obj; valid (CloseFd p fd # s); co2sobj s obj = Some sobj; 
@@ -974,7 +974,7 @@
 apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
 
 apply (rule impI, tactic {*my_seteq_tac 1*})
-apply (simp add:update_s2ss_obj_def update_s2ss_sfile_def)
+apply (simp add:update_s2ss_obj_def update_s2ss_sfile_del_def)
 apply (rule conjI| rule impI|erule exE|erule conjE)+
 apply (erule_tac obj = obj in co2sobj_some_caseD)
 apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
@@ -1055,7 +1055,7 @@
 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp)
 
-apply (simp add:update_s2ss_sfile_def update_s2ss_obj_def split:if_splits)
+apply (simp add:update_s2ss_sfile_del_def update_s2ss_obj_def split:if_splits)
 apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
 apply (erule exE, erule conjE)
 apply (case_tac "obj = O_proc p")
@@ -1149,7 +1149,7 @@
 
 apply (rule impI, rule conjI, rule impI)
 apply (tactic {*my_seteq_tac 1*})
-apply (simp add:update_s2ss_obj_def update_s2ss_sfile_def)
+apply (simp add:update_s2ss_obj_def update_s2ss_sfile_del_def)
 apply (rule conjI| rule impI|erule exE|erule conjE)+
 apply (erule_tac obj = obj in co2sobj_some_caseD)
 apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
@@ -1231,7 +1231,7 @@
 
 apply (rule impI)
 apply (tactic {*my_seteq_tac 1*})
-apply (simp add:update_s2ss_obj_def update_s2ss_sfile_def)
+apply (simp add:update_s2ss_obj_def update_s2ss_sfile_del_def)
 apply (rule conjI| rule impI|erule exE|erule conjE)+
 apply (erule_tac obj = obj in co2sobj_some_caseD)
 apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
@@ -1334,7 +1334,7 @@
 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 apply (rule notI, simp add:co2sobj.simps split:option.splits)+
 
-apply (simp add:update_s2ss_sfile_def update_s2ss_obj_def split:if_splits)
+apply (simp add:update_s2ss_sfile_del_def update_s2ss_obj_def split:if_splits)
 apply (erule conjE, erule disjE)
 apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
 apply (erule exE, erule conjE)
@@ -1471,7 +1471,7 @@
 apply (frule vd_cons, frule vt_grant_os, clarsimp split:if_splits)
 apply (frule is_file_has_sfile', simp, erule exE, simp)
 apply (rule conjI, rule impI)
-apply (simp add:update_s2ss_sfile_def del_s2ss_file_def)
+apply (simp add:update_s2ss_sfile_del_def del_s2ss_file_def)
 apply (rule impI|erule conjE|erule exE|rule conjI|erule bexE)+ defer
 apply (rule impI|erule conjE|erule exE|rule conjI|erule bexE)+ 
 
@@ -1740,9 +1740,9 @@
 apply (rule_tac x = obj in exI, simp add:co2sobj_mkdir alive_mkdir)
 done
 
-definition update_s2ss_sfile_link:: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_file \<Rightarrow> t_sfile \<Rightarrow> t_static_state"
+definition update_s2ss_sfile:: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_file \<Rightarrow> t_sfile \<Rightarrow> t_static_state"
 where
- "update_s2ss_sfile_link s ss f sf \<equiv>
+ "update_s2ss_sfile s ss f sf \<equiv>
     if (\<exists> f'. is_file s f' \<and> f' \<notin> same_inode_files s f \<and> co2sobj s (O_file f') = co2sobj s (O_file f))
        then ss \<union> {S_file (cf2sfiles s f \<union> {sf}) (O_file f \<in> Tainted s)}
        else ss - {S_file (cf2sfiles s f) (O_file f \<in> Tainted s)} 
@@ -1750,14 +1750,14 @@
 
 lemma s2ss_linkhard: "valid (LinkHard p f f' # s) \<Longrightarrow> s2ss (LinkHard p f f' # s) = (
   case (cf2sfile (LinkHard p f f' # s) f') of
-    Some sf \<Rightarrow> update_s2ss_sfile_link s (s2ss s) f sf
+    Some sf \<Rightarrow> update_s2ss_sfile s (s2ss s) f sf
   | _       \<Rightarrow> {})"
 apply (frule vt_grant_os, frule vd_cons, clarsimp)
 apply (split option.splits)
 apply (rule conjI, rule impI, drule current_file_has_sfile', simp, simp add:current_files_simps)
 apply (rule allI, rule impI)
 
-apply (simp add:update_s2ss_sfile_link_def)
+apply (simp add:update_s2ss_sfile_def)
 apply (rule conjI, rule impI, erule exE, erule conjE, erule conjE)
 apply (simp add:s2ss_def)
 apply (tactic {*my_seteq_tac 1*})
@@ -1836,8 +1836,142 @@
 apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
 done
 
+lemma has_same_inode_prop3:
+  "is_file s f \<Longrightarrow> has_same_inode s f f"
+by (auto simp:is_file_def has_same_inode_def split:option.splits)
+
+definition update_s2ss_sfile_tainted:: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_file \<Rightarrow> bool \<Rightarrow> t_static_state"
+where
+ "update_s2ss_sfile_tainted s ss f tag \<equiv>
+    if (\<exists> f'. is_file s f' \<and> f' \<notin> same_inode_files s f \<and> 
+              co2sobj s (O_file f') = Some (S_file (cf2sfiles s f) False))
+       then ss \<union> {S_file (cf2sfiles s f) True}
+       else ss - {S_file (cf2sfiles s f) False} 
+               \<union> {S_file (cf2sfiles s f) True}"
+
+lemma s2ss_truncate: "valid (Truncate p f len # s) \<Longrightarrow> s2ss (Truncate p f len # s) = (
+  if (O_file f \<notin> Tainted s \<and> O_proc p \<in> Tainted s \<and> len > 0)
+  then update_s2ss_sfile_tainted s (s2ss s) f True
+  else s2ss s)"
+apply (frule vt_grant_os, frule vd_cons, simp split:if_splits)
+apply (rule conjI, rule impI, (erule conjE)+)
+
+apply (simp add:update_s2ss_sfile_tainted_def)
+apply (rule conjI|rule impI|erule exE|erule conjE)+
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_file f")
+apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted has_same_inode_prop3 cf2sfiles_other)
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_truncate alive_simps)
+apply (case_tac "fa \<in> same_inode_files s f")
+apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted cf2sfiles_prop cf2sfiles_other)
+apply (simp add:same_inode_files_prop7)
+apply (rule disjI2, simp, rule_tac x = obj in exI)
+apply (simp add:co2sobj_truncate is_file_simps)
+apply (rule disjI2, simp, rule_tac x = obj in exI)
+apply (simp add:co2sobj_truncate)
+apply (rule disjI2, simp, rule_tac x = obj in exI)
+apply (simp add:co2sobj_truncate is_dir_simps)
+apply (rule disjI2, simp, rule_tac x = obj in exI)
+apply (simp add:co2sobj_truncate)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_file f" in exI)
+apply (simp add:co2sobj.simps is_file_simps tainted_eq_Tainted cf2sfiles_other has_same_inode_prop3)
+apply (tactic {*my_setiff_tac 1*})
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (rule_tac x = obj in exI, simp add:co2sobj_truncate)
+apply (case_tac "fa \<in> same_inode_files s f")
+apply (rule_tac x = "O_file f'" in exI)
+apply (auto simp:co2sobj_truncate is_file_simps is_dir_simps split:t_object.splits)[1]
+apply (simp add:co2sobj.simps same_inodes_Tainted tainted_eq_Tainted cf2sfiles_prop)
+apply (rule_tac x = obj in exI, simp add:co2sobj_truncate is_file_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_truncate)
+apply (rule_tac x = obj in exI, simp add:co2sobj_truncate is_dir_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_truncate)
+
+apply (rule conjI|rule impI|erule exE|erule conjE)+
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_file f")
+apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted has_same_inode_prop3 cf2sfiles_other)
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI, simp add:co2sobj_truncate alive_simps)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)
+apply (case_tac "fa \<in> same_inode_files s f")
+apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted cf2sfiles_prop cf2sfiles_other)
+apply (simp add:same_inode_files_prop7)
+apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI)
+apply (simp add:co2sobj_truncate is_file_simps)
+apply (rule notI, simp add:co2sobj_truncate is_file_simps)
+apply (erule_tac x = fa in allE)
+apply (simp add:co2sobj.simps)
+apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI)
+apply (simp add:co2sobj_truncate)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)
+apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI)
+apply (simp add:co2sobj_truncate is_dir_simps)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)
+apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI)
+apply (simp add:co2sobj_truncate)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_file f" in exI)
+apply (simp add:co2sobj.simps is_file_simps tainted_eq_Tainted cf2sfiles_other has_same_inode_prop3)
+apply (tactic {*my_setiff_tac 1*})
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (rule_tac x = obj in exI, simp add:co2sobj_truncate)
+apply (case_tac "fa \<in> same_inode_files s f")
+apply (simp add:co2sobj.simps same_inodes_Tainted tainted_eq_Tainted cf2sfiles_prop)
+apply (rule_tac x = obj in exI, simp add:co2sobj_truncate is_file_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_truncate)
+apply (rule_tac x = obj in exI, simp add:co2sobj_truncate is_dir_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_truncate)
+
+apply (rule impI, simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (rule_tac x = obj in exI)
+apply (simp add:alive_simps co2sobj_truncate)
+apply (simp split:t_object.splits if_splits add:co2sobj.simps tainted_eq_Tainted)
+apply (case_tac "O_proc p \<in> Tainted s", simp add:same_inodes_Tainted)
+apply simp
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = obj in exI)
+apply (simp add:alive_simps co2sobj_truncate)
+apply (auto split:t_object.splits if_splits simp:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted)
+done
+
+lemma s2ss_createmsgq: "valid (CreateMsgq p q # s) \<Longrightarrow> s2ss (CreateMsgq p q # s) = 
+  (case (cq2smsgq (CreateMsgq p q # s) q) of 
+     Some sq \<Rightarrow> s2ss s \<union> {S_msgq sq}
+   | _       \<Rightarrow> {})"
+apply (frule vd_cons, frule vt_grant_os, clarsimp)
+apply (case_tac "cq2smsgq (CreateMsgq p q # s) q")
+apply (drule current_has_smsgq', simp+)
+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_createmsgq 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_msgq q" in exI, simp add:co2sobj.simps)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_msgq q")
+apply simp
+apply (rule_tac x = obj in exI)
+apply (auto simp add:co2sobj_createmsgq alive_simps split:t_object.splits if_splits)
+done
+
+lemma s2ss_sendmsg:
+
+lemma s2ss_recvmsg:
+
+lemma s2ss_removemsgq:
 
 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
+  s2ss_truncate s2ss_createmsgq