--- a/S2ss_prop2.thy Tue Oct 15 14:11:53 2013 +0800
+++ b/S2ss_prop2.thy Wed Oct 16 13:38:31 2013 +0800
@@ -228,29 +228,115 @@
apply (auto simp add:co2sobj.simps tainted_eq_Tainted is_file_simps is_dir_simps split:t_object.splits)[1]
done
+definition attach_Tainted_procs :: "t_state \<Rightarrow> t_process \<Rightarrow> t_shm \<Rightarrow> t_shm_attach_flag \<Rightarrow> t_process set"
+where
+ "attach_Tainted_procs s p h flag \<equiv>
+ (if (O_proc p \<in> Tainted s \<and> flag = SHM_RDWR)
+ then {p''. \<exists> p' flag'. (p', flag') \<in> procs_of_shm s h \<and> info_flow_shm s p' p'' \<and>
+ O_proc p'' \<notin> Tainted s}
+ else if (\<exists> p'. O_proc p' \<in> Tainted s \<and> (p', SHM_RDWR) \<in> procs_of_shm s h)
+ then {p'. info_flow_shm s p p' \<and> O_proc p' \<notin> Tainted s}
+ else {})"
+lemma attach_Tainted_procs_prop1:
+ "valid s \<Longrightarrow> Tainted (Attach p h flag # s) = Tainted s \<union> {O_proc p' | p'. p' \<in> attach_Tainted_procs s p h flag}"
+apply (auto simp:attach_Tainted_procs_def intro:info_flow_shm_Tainted)
+done
+
+lemma attach_Tainted_procs_prop2:
+ "valid (Attach p h flag # s) \<Longrightarrow> {O_proc p'| p'. p' \<in> attach_Tainted_procs s p h flag} \<inter> Tainted s = {}"
+by (auto simp:attach_Tainted_procs_def)
+
+lemma attach_Tainted_procs_prop3:
+ "\<lbrakk>p' \<in> attach_Tainted_procs s p h flag; valid s\<rbrakk> \<Longrightarrow> p' \<in> current_procs s"
+by (auto simp:attach_Tainted_procs_def info_shm_flow_in_procs split:if_splits)
-lemma s2ss_attach1:
- "\<lbrakk>valid (Attach p h SHM_RDWR # s); O_proc p \<in> Tainted s\<rbrakk>\<Longrightarrow> s2ss (Attach p h SHM_RDWR # s) = (
+lemma co2sobj_attach':
+ "\<lbrakk>valid (Attach p h flag # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Attach p h flag # s) obj =
+ (case obj of
+ O_proc p' \<Rightarrow> if (p' = p)
+ then (case cp2sproc (Attach p h flag # s) p of
+ Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s \<or> p \<in> attach_Tainted_procs s p h flag))
+ | _ \<Rightarrow> None)
+ else if (p' \<in> attach_Tainted_procs s p h flag)
+ then case cp2sproc s p' of
+ None \<Rightarrow> None
+ | Some sp \<Rightarrow> Some (S_proc sp True)
+ else co2sobj s obj
+ | _ \<Rightarrow> co2sobj s obj)"
+apply (frule vt_grant_os, frule vd_cons, case_tac obj)
+apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted co2sobj.simps)
- "
+apply (frule current_proc_has_sp, simp, erule exE, (erule conjE)+)
+apply (case_tac "cp2sproc (Attach p h flag # s) nat", drule current_proc_has_sp', simp+)
+apply (case_tac "cp2sproc (Attach p h flag # s) p", drule current_proc_has_sp', simp+)
+apply (simp add:tainted_eq_Tainted attach_Tainted_procs_prop1 del:Tainted.simps)
+apply (simp add:cp2sproc_attach split:if_splits)
+
+apply (auto split:if_splits option.splits dest!:current_file_has_sfile'
+ simp:current_files_simps cf2sfiles_simps cf2sfile_simps tainted_eq_Tainted
+ same_inode_files_prop6
+ dest:is_file_in_current is_dir_in_current)
+done
-lemma s2ss_attach1:
- "\<lbrakk>valid (Attach p h flag # s); O_proc p \<notin> Tainted s; (p', SHM_RDWR) \<in> procs_of_shm s; O_proc p' \<in> Tainted s\<rbrakk>
- \<Longrightarrow> s2ss (Attach p h SHM_RDONLY # s) = "
+lemma s2ss_attach:
+ "valid (Attach p h flag # s) \<Longrightarrow> s2ss (Attach p h flag # s) =
+ update_s2ss_procs s (s2ss s) (Attach p h flag) (attach_Tainted_procs s p h flag \<union> {p})"
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac "cp2sproc s p", drule current_proc_has_sp', simp, simp)
+apply (case_tac "ch2sshm s h", drule current_shm_has_sh', simp, simp)
+apply (case_tac "cp2sproc (Attach p h flag # s) p", drule current_proc_has_sp', simp, simp)
-lemma s2ss_attach1:
- "valid (Attach p h flag # s) \<Longrightarrow> s2ss (Attach p h flag # s) = "
+unfolding update_s2ss_procs_def
+apply (tactic {*my_seteq_tac 1*})
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac "pa = p")
+apply (rule DiffI, rule UnI2, simp, rule_tac x = pa in exI, simp)
+apply (rule notI, drule_tac p = pa in unbked_sps_D, simp, simp)
+apply (case_tac "pa \<in> attach_Tainted_procs s p h flag")
+apply (rule DiffI, rule UnI2, simp)
+apply (rule_tac x = pa in exI, simp)
+apply (rule notI, drule_tac p = pa in unbked_sps_D, simp, simp)
+apply (rule DiffI, rule UnI1, simp)
+apply (rule_tac x = obj in exI, simp add:co2sobj_attach')
+apply (rule notI, drule_tac p = pa in unbked_sps_D', simp+)
+apply (simp add:co2sobj_attach')
+apply (simp add:co2sobj_attach')
+apply (rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_attach' is_file_simps)
+apply (erule unbked_sps_I, simp)
+apply (rule DiffI,rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_attach')
+apply (erule unbked_sps_I, simp)
+apply (rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_attach' is_dir_simps)
+apply (erule unbked_sps_I, simp)
+apply (rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_attach')
+apply (erule unbked_sps_I, simp)
-lemma s2ss_Detach:
- "valid (Detach p h # s) \<Longrightarrow> s2ss (Detach p h # s) = "
+apply (erule DiffE, erule UnE)
+apply (tactic {*my_setiff_tac 1*})
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac "pa \<in> attach_Tainted_procs s p h flag \<union> {p}")
+apply (drule_tac p = pa in not_unbked_sps_D, simp, simp)
+apply (erule disjE, erule bexE)
+apply (rule_tac x = "O_proc p'" in exI, simp)
+apply (erule disjE, simp, simp add:attach_Tainted_procs_prop3)
+apply (erule bexE, simp, (erule conjE)+)
+apply (rule_tac x = "O_proc p'" in exI, simp add:co2sobj_attach')
+apply (rule_tac x = "O_proc pa" in exI, simp add:co2sobj_attach')
+apply (rule_tac x = obj in exI, simp add:co2sobj_attach' is_file_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_attach')
+apply (rule_tac x = obj in exI, simp add:co2sobj_attach' is_dir_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_attach')
+apply (tactic {*my_setiff_tac 1*}, clarsimp)
+apply (rule_tac x = "O_proc pa" in exI, simp)
+apply (erule disjE, simp, simp add:attach_Tainted_procs_prop3)
+done
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_sendmsg s2ss_removemsgq s2ss_recvmsg
- s2ss_createshm
+ s2ss_createshm s2ss_detach s2ss_deleteshm s2ss_attach
end