# HG changeset patch
# User chunhan
# Date 1378981418 -28800
# Node ID d7fab2e2a0b8807538341a40eea6931179c4d7ac
# Parent  563194dcdbc61245072ff95fbf47688082b5d491
s2ss_writefile

diff -r 563194dcdbc6 -r d7fab2e2a0b8 S2ss_prop.thy
--- a/S2ss_prop.thy	Thu Sep 12 15:17:53 2013 +0800
+++ b/S2ss_prop.thy	Thu Sep 12 18:23:38 2013 +0800
@@ -640,7 +640,134 @@
 apply (simp add:co2sobj.simps)+
 done
 
+lemma same_inode_files_prop9:
+  "is_file s f \<Longrightarrow> f \<in> same_inode_files s f"
+by (simp add:same_inode_files_def)
+
+lemma cf2sfiles_prop:
+  "\<lbrakk>f \<in> same_inode_files s f'; valid s\<rbrakk> \<Longrightarrow> cf2sfiles s f = cf2sfiles s f'"
+apply (auto simp:cf2sfiles_def)
+apply (rule_tac x = f'a in bexI, simp)
+apply (erule same_inode_files_prop4, simp)
+apply (rule_tac x = f'a in bexI, simp)
+apply (drule same_inode_files_prop5)
+apply (erule same_inode_files_prop4, simp)
+done
+
+lemma co2sobj_writefile_unchange:
+  "\<lbrakk>valid (WriteFile p fd # s); alive s obj; file_of_proc_fd s p fd = Some f;
+    O_proc p \<in> Tainted s \<longrightarrow> O_file f \<in> Tainted s\<rbrakk> 
+   \<Longrightarrow> co2sobj (WriteFile p fd # s) obj = co2sobj s obj"
+apply (frule vd_cons, frule co2sobj_writefile, simp, simp split:t_object.splits if_splits)
+apply (simp add:co2sobj.simps)
+apply (case_tac "O_proc p \<in> Tainted s")
+apply (simp add:tainted_eq_Tainted same_inodes_Tainted)+
+done
+
+lemma s2ss_writefile:
+  "valid (WriteFile p fd # s) \<Longrightarrow> s2ss (WriteFile p fd # s) = (
+     case (file_of_proc_fd s p fd) of
+       Some f \<Rightarrow> if (O_proc p \<in> Tainted s \<and> O_file f \<notin> Tainted s)
+                 then (if (\<exists> f'. f' \<notin> same_inode_files s f \<and> is_file s f' \<and>
+                                 co2sobj s (O_file f') = co2sobj s (O_file f))
+                       then s2ss s \<union> {S_file (cf2sfiles s f) True}
+                       else s2ss s - {S_file (cf2sfiles s f) False} 
+                                   \<union> {S_file (cf2sfiles s f) True})
+                 else s2ss s
+     | _      \<Rightarrow> {})"
+apply (frule vd_cons, frule vt_grant_os)
+apply (clarsimp split:option.splits)
+unfolding s2ss_def
+apply (rule conjI|rule impI|erule exE|erule conjE)+
+apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE)
+apply (frule_tac obj =  obj in co2sobj_writefile, simp add:alive_other)
+apply (simp split:t_object.splits if_splits)
+apply (rule disjI2, rule_tac x= "O_proc nat" in exI, simp)
+apply (rule disjI1, simp add:cf2sfiles_prop)
+apply (rule disjI2, rule_tac x = obj in exI, simp add:is_file_simps)
+apply (simp add:co2sobj.simps)
+apply (rule disjI2, rule_tac x = obj in exI, simp add:is_dir_simps)
+apply (simp add:co2sobj.simps)
+apply (simp add:co2sobj.simps)
+apply (simp add:co2sobj.simps)
+apply (rule disjI2, rule_tac x = obj in exI, simp)
+apply (rule disjI2, rule_tac x = obj in exI, simp)
+apply (simp add:co2sobj.simps)
+
+apply (simp, erule disjE)
+apply (rule_tac x = "O_file aa" in exI, simp add:is_file_simps file_of_pfd_is_file)
+apply (frule_tac obj = "O_file aa" in co2sobj_writefile, simp add:file_of_pfd_is_file)
+apply (simp split:if_splits add:same_inode_files_def file_of_pfd_is_file)
+apply (erule exE, erule conjE)
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (rule_tac x = obj in exI, simp add:co2sobj_writefile)
+apply (case_tac "fa \<in> same_inode_files s aa")
+apply (frule_tac f = fa and f' = aa in cf2sfiles_prop, simp)
+apply (rule_tac x = "O_file f'" in exI, simp add:co2sobj_writefile is_file_simps)
+apply (rule conjI, rule impI, simp add:same_inode_files_prop5)
+apply (rule impI, simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted)
+apply (rule_tac x = "O_file fa" in exI, simp add:co2sobj_writefile is_file_simps)
+apply (rule impI, simp add:same_inode_files_prop5)
+apply (rule_tac x = obj in exI, simp add:co2sobj_writefile)
+apply (rule_tac x = obj in exI, simp add:co2sobj_writefile is_dir_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_writefile)
+
+apply (rule impI, rule impI, simp, rule set_eqI, rule iffI, erule CollectE, (erule conjE|erule exE)+)
+apply (rule CollectI, rule_tac x = obj in exI, simp add:alive_simps)
+apply (simp add:co2sobj_writefile split:t_object.splits if_splits)
+apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted)
+apply (case_tac "O_proc p \<in> Tainted s", simp, simp)
+apply (erule CollectE, (erule conjE|erule exE)+, rule CollectI)
+apply (rule_tac x = obj in exI)
+apply (simp add:co2sobj_writefile_unchange alive_simps)
+
+apply (rule impI| rule conjI|erule conjE)+
+apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE)
+apply (simp add:alive_simps co2sobj_writefile split:t_object.splits)
+apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp,
+  rule notI, simp add:co2sobj.simps split:option.splits)
+apply (simp split:if_splits)
+apply (rule disjI1, simp add:cf2sfiles_prop)
+apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)
+apply (erule_tac x = list in allE, simp add:tainted_eq_Tainted same_inode_files_prop5)
+apply (simp add:co2sobj.simps)
+apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp,
+  rule notI, simp add:co2sobj.simps split:option.splits)
+apply (simp add:co2sobj.simps)
+apply (simp add:co2sobj.simps)
+apply (simp add:co2sobj.simps)
+apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp,
+  rule notI, simp add:co2sobj.simps split:option.splits)
+apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp,
+  rule notI, simp add:co2sobj.simps split:option.splits)
+apply (simp add:co2sobj.simps)
+apply (simp)
+apply (erule disjE)
+apply (rule_tac x= "O_file aa" in exI, simp add:co2sobj_writefile alive_simps file_of_pfd_is_file)
+apply (rule impI, simp add:same_inode_files_def file_of_pfd_is_file)
+apply (erule exE|erule conjE)+
+apply (erule co2sobj_some_caseD)
+apply (rule_tac x = obj in exI, simp add:co2sobj_writefile)
+apply (case_tac "fa \<in> same_inode_files s aa")
+apply (frule cf2sfiles_prop, simp, simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted)
+apply (rule_tac x = obj in exI, simp add:co2sobj_writefile is_file_simps)
+apply (rule impI, simp add:same_inode_files_prop5)
+apply (rule_tac x = obj in exI, simp add:co2sobj_writefile)
+apply (rule_tac x = obj in exI, simp add:co2sobj_writefile is_dir_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_writefile)
+apply (rule impI, rule impI)
+
+apply (rule set_eqI, rule iffI, erule CollectE,erule exE,erule conjE,rule CollectI)
+apply (rule_tac x = obj in exI)
+apply (simp add:co2sobj_writefile_unchange alive_simps)
+apply (erule CollectE, erule exE, erule conjE)
+apply (rule CollectI, rule_tac x = obj in exI)
+apply (simp add:co2sobj_writefile_unchange alive_simps)
+done
+
+
 
 lemmas s2ss_simps = s2ss_execve s2ss_clone s2ss_ptrace s2ss_kill s2ss_exit s2ss_open
-  s2ss_readfile
+  s2ss_readfile s2ss_writefile