# HG changeset patch
# User chunhan
# Date 1378970273 -28800
# Node ID 563194dcdbc61245072ff95fbf47688082b5d491
# Parent  137358bd49213eca3885fb974d7b525cdf734631
s2ss_readfile

diff -r 137358bd4921 -r 563194dcdbc6 S2ss_prop.thy
--- a/S2ss_prop.thy	Thu Sep 12 13:50:22 2013 +0800
+++ b/S2ss_prop.thy	Thu Sep 12 15:17:53 2013 +0800
@@ -564,8 +564,83 @@
 apply (simp add:s2ss_open_some s2ss_open_none)+
 done
 
-lemma
+lemma s2ss_readfile:
+  "valid (ReadFile p fd # s) \<Longrightarrow> s2ss (ReadFile p fd # s) = (
+     case (file_of_proc_fd s p fd) of 
+       Some f \<Rightarrow> if (O_file f \<in> Tainted s)
+                 then update_s2ss_shm s p
+                 else s2ss s
+     | _      \<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
+apply (rule set_eqI, rule iffI)
+apply (drule CollectD, (erule exE|erule conjE)+)
+apply (erule co2sobj_some_caseD)
+apply (rule DiffI)
+apply (case_tac "O_proc pa \<in> Tainted s")
+apply (rule UnI1, simp, rule_tac x = "O_proc pa" in exI)
+apply (clarsimp simp:cp2sproc_other tainted_eq_Tainted co2sobj.simps split:option.splits)
+apply (case_tac "info_flow_shm s p pa")
+apply (rule UnI2, rule CollectI, simp only:co2sobj.simps split:option.splits)
+apply (drule current_proc_has_sp', simp, simp)
+apply (rule_tac x = ab in exI, rule_tac x = pa in exI)
+apply (clarsimp simp:cp2sproc_other tainted_eq_Tainted split:option.splits)
+apply (rule UnI1, simp)
+apply (rule_tac x = "O_proc pa" in exI)
+apply (clarsimp simp:cp2sproc_other tainted_eq_Tainted co2sobj.simps split:option.splits)
+apply (rule notI, clarsimp simp:cp2sproc_other tainted_eq_Tainted co2sobj.simps split:option.splits)
+apply (erule_tac x = pa in allE, simp)
+
+apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI)
+apply (simp add:alive_simps co2sobj_readfile, rule notI, clarsimp simp:co2sobj.simps)
+apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI)
+apply (simp add:alive_simps co2sobj_readfile, rule notI, clarsimp simp:co2sobj.simps split:option.splits)
+apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI)
+apply (simp add:alive_simps co2sobj_readfile, rule notI, clarsimp simp:co2sobj.simps split:option.splits)
+apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI)
+apply (simp add:alive_simps co2sobj_readfile, rule notI, clarsimp simp:co2sobj.simps split:option.splits)
+
+apply (erule DiffE, drule s2ss_ptrace1_aux, erule UnE)
+apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)
+apply (erule co2sobj_some_caseD)
+apply (case_tac "O_proc pa \<in> Tainted s")
+apply (rule_tac x = "O_proc pa" in exI)
+apply (clarsimp simp:tainted_eq_Tainted cp2sproc_other co2sobj.simps split:option.splits)
+apply (case_tac "info_flow_shm s p pa", simp only:co2sobj.simps split:option.splits)
+apply (drule current_proc_has_sp', simp, simp)
+apply (drule Meson.not_exD, erule_tac x = ab in allE, drule Meson.not_exD, erule_tac x = pa in allE)
+apply (simp add:tainted_eq_Tainted, (erule exE|erule conjE)+)
+apply (rule_tac x = "O_proc p'" in exI)
+apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted co2sobj.simps split:option.splits)
+apply (rule_tac x = "O_proc pa" in exI)
+apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted co2sobj.simps split:option.splits)
+
+apply (rule_tac x = obj in exI,
+       auto split:option.splits simp:co2sobj_readfile alive_simps simp del:co2sobj.simps)[1]
+apply (rule_tac x = obj in exI,
+       auto split:option.splits simp:co2sobj_readfile alive_simps simp del:co2sobj.simps)[1]
+apply (rule_tac x = obj in exI,
+       auto split:option.splits simp:co2sobj_readfile alive_simps simp del:co2sobj.simps)[1]
+apply (rule_tac x = obj in exI,
+       auto split:option.splits simp:co2sobj_readfile alive_simps simp del:co2sobj.simps)[1]
+
+apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI)
+apply (rule_tac x = "O_proc pa" in exI)
+apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted info_shm_flow_in_procs co2sobj.simps)
+
+
+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, simp add:alive_simps co2sobj_readfile split:t_object.splits)
+apply (erule CollectE, erule exE, erule conjE, rule CollectI)
+apply (rule_tac x = obj in exI, simp add:alive_simps)
+apply (drule_tac obj = obj in co2sobj_readfile, simp)
+apply (simp split:t_object.splits)
+apply (simp add:co2sobj.simps)+
+done
 
 
 lemmas s2ss_simps = s2ss_execve s2ss_clone s2ss_ptrace s2ss_kill s2ss_exit s2ss_open
+  s2ss_readfile