--- a/S2ss_prop.thy Thu Sep 12 19:00:26 2013 +0800
+++ b/S2ss_prop.thy Tue Sep 24 14:02:15 2013 +0800
@@ -766,11 +766,302 @@
apply (simp add:co2sobj_writefile_unchange alive_simps)
done
+
+definition update_s2ss_obj :: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_object \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state"
+where
+ "update_s2ss_obj s ss obj sobj sobj' =
+ (if (\<exists> obj'. alive s obj' \<and> obj' \<noteq> obj \<and> co2sobj s obj' = Some sobj)
+ 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"
+where
+ "update_s2ss_sfile 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)}"
+
+definition del_s2ss_file:: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_file \<Rightarrow> t_sfile \<Rightarrow> t_static_state"
+where
+ "del_s2ss_file s ss f sf =
+ (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"
+
+lemma alive_co2sobj_closefd1:
+ "\<lbrakk>alive s obj; valid (CloseFd p fd # s); co2sobj s obj = Some sobj;
+ file_of_proc_fd s p fd = Some f; \<not> (f \<in> files_hung_by_del s \<and> proc_fd_of_file s f = {(p, fd)})\<rbrakk>
+ \<Longrightarrow> alive (CloseFd p fd # s) obj"
+apply (erule co2sobj_some_caseD)
+by (auto simp:alive_simps is_file_simps is_dir_simps split:option.splits)
+
+lemma alive_co2sobj_closefd3:
+ "\<lbrakk>alive s obj; valid (CloseFd p fd # s); co2sobj s obj = Some sobj; obj \<noteq> O_file f;
+ file_of_proc_fd s p fd = Some f; f \<in> files_hung_by_del s; proc_fd_of_file s f = {(p, fd)}\<rbrakk>
+ \<Longrightarrow> alive (CloseFd p fd # s) obj"
+apply (erule co2sobj_some_caseD)
+by (auto simp:alive_simps is_file_simps is_dir_simps split:option.splits)
+
+lemma alive_co2sobj_closefd2:
+ "\<lbrakk>alive s obj; valid (CloseFd p fd # s); co2sobj s obj = Some sobj; file_of_proc_fd s p fd = None\<rbrakk>
+ \<Longrightarrow> alive (CloseFd p fd # s) obj"
+apply (erule co2sobj_some_caseD)
+by (auto simp:alive_simps is_file_simps is_dir_simps split:option.splits)
+
+lemma alive_co2sobj_closefd':
+ "\<lbrakk>co2sobj (CloseFd p fd # s) obj = Some sobj; alive (CloseFd p fd # s) obj;
+ valid (CloseFd p fd # s)\<rbrakk> \<Longrightarrow> alive s obj"
+apply (erule co2sobj_some_caseD)
+by (auto simp:alive_simps is_file_simps is_dir_simps split:option.splits if_splits)
+
+ML {*asm_full_simp_tac*}
+
+ML {*
+fun my_setiff_tac i =
+ (etac @{thm CollectE} i
+ ORELSE ( asm_full_simp_tac (HOL_ss addsimps @{thms Set.insert_iff}) i
+ THEN etac @{thm disjE} i)
+ ORELSE ( asm_full_simp_tac (HOL_ss addsimps @{thms Set.Diff_iff}) i
+ THEN etac @{thm conjE} i
+ THEN (REPEAT (etac @{thm CollectE} i))))
+THEN (REPEAT (( etac @{thm exE}
+ ORELSE' etac @{thm conjE}
+ ORELSE' etac @{thm bexE}) i))
+THEN (rtac @{thm CollectI} i
+ ORELSE ( asm_full_simp_tac (HOL_ss addsimps @{thms Set.insert_iff}) i))
+
+*}
+
+ML {*
+fun my_seteq_tac i =
+ (simp_tac (HOL_ss addsimps @{thms s2ss_def}) 1)
+THEN (rtac @{thm set_eqI} i)
+THEN (rtac @{thm iffI} i)
+THEN my_setiff_tac i
+*}
+
+lemma co2sobj_sproc_imp:
+ "co2sobj s obj = Some (S_proc sp tag) \<Longrightarrow> \<exists> p. obj = O_proc p"
+by (case_tac obj, auto simp:co2sobj.simps split:option.splits)
+
+lemma co2sobj_sfile_imp:
+ "co2sobj s obj = Some (S_file sfs tag) \<Longrightarrow> \<exists> f. obj = O_file f"
+by (case_tac obj, auto simp:co2sobj.simps split:option.splits)
+
+lemma co2sobj_sdir_imp:
+ "co2sobj s obj = Some (S_dir sf) \<Longrightarrow> \<exists> f. obj = O_dir f"
+by (case_tac obj, auto simp:co2sobj.simps split:option.splits)
+
+lemma co2sobj_sshm_imp:
+ "co2sobj s obj = Some (S_shm sh) \<Longrightarrow> \<exists> h. obj = O_shm h"
+by (case_tac obj, auto simp:co2sobj.simps split:option.splits)
+
+lemma co2sobj_smsgq_imp:
+ "co2sobj s obj = Some (S_msgq sq) \<Longrightarrow> \<exists> q. obj = O_msgq q"
+by (case_tac obj, auto simp:co2sobj.simps split:option.splits)
+
lemma s2ss_closefd:
"valid (CloseFd p fd # s) \<Longrightarrow> s2ss (CloseFd p fd # s) = (
case (file_of_proc_fd s p fd) of
- Some f \<Rightarrow> if ("
+ Some f \<Rightarrow> if (f \<in> files_hung_by_del s \<and> proc_fd_of_file s f = {(p, fd)})
+ then (case (cf2sfile s f, cp2sproc s p, cp2sproc (CloseFd p fd # s) p) of
+ (Some sf, Some sp, Some sp') \<Rightarrow>
+ (del_s2ss_file s (
+ update_s2ss_obj s (s2ss s) (O_proc p)
+ (S_proc sp (O_proc p \<in> Tainted s))
+ (S_proc sp' (O_proc p \<in> Tainted s))) f sf)
+ | _ \<Rightarrow> {})
+ else (case (cp2sproc s p, cp2sproc (CloseFd p fd # s) p) of
+ (Some sp, Some sp') \<Rightarrow>
+ (update_s2ss_obj s (s2ss s) (O_proc p)
+ (S_proc sp (O_proc p \<in> Tainted s))
+ (S_proc sp' (O_proc p \<in> Tainted s)))
+ | _ \<Rightarrow> {})
+ | _ \<Rightarrow> s2ss s)"
+apply (frule vd_cons, frule vt_grant_os)
+apply (clarsimp simp only:os_grant.simps)
+apply (frule current_proc_has_sp, simp, erule exE)
+apply (case_tac "file_of_proc_fd s p fd")
+
+apply (simp add:s2ss_def)
+apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE, rule CollectI)
+apply (rule_tac x = obj in exI, simp add:alive_co2sobj_closefd')
+apply (frule co2sobj_closefd, simp)
+apply (frule cp2sproc_closefd, simp)
+apply (simp add:proc_file_fds_def split:t_object.splits)
+apply (simp split:if_splits add:co2sobj.simps tainted_eq_Tainted)
+apply (erule CollectE, erule exE, erule conjE, rule CollectI)
+apply (rule_tac x = obj in exI, simp add:alive_co2sobj_closefd2)
+apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd2)
+apply (frule cp2sproc_closefd, simp)
+apply (auto simp add:proc_file_fds_def co2sobj.simps tainted_eq_Tainted
+ split:t_object.splits option.splits if_splits)[1]
+
+apply (case_tac "cp2sproc (CloseFd p fd # s) p")
+apply (drule current_proc_has_sp', simp, simp)
+apply (case_tac "cf2sfile s a")
+apply (drule current_file_has_sfile', simp, simp add:file_of_pfd_in_current)
+apply (simp)
+
+apply (rule conjI, rule impI, erule conjE)
+apply (simp add:del_s2ss_file_def)
+apply (rule conjI|rule impI|erule exE|erule conjE|erule bexE)+
+
+apply (simp add:update_s2ss_obj_def)
+apply (rule conjI|rule impI|erule exE|erule conjE|erule bexE)+
+apply (tactic {*my_seteq_tac 1*})
+apply simp
+apply (case_tac "obj = O_proc p")
+apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (rule disjI2, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_simps)
+apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_proc p" in exI)
+apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_proc p")
+apply (rule_tac x = obj' in exI)
+apply (frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd)
+apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (case_tac "obj = O_file a")
+apply (rule_tac x = "O_file f'" in exI)
+apply (case_tac "f' = a", simp add:same_inode_files_prop9 file_of_pfd_is_file)
+apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps)
+apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
+apply (frule_tac obj = obj in co2sobj_closefd, simp)
+apply (auto simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
+
+apply (rule impI)+
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_proc p", rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (rule disjI2)
+apply (case_tac "obj = O_file a", simp add:alive_simps)
+apply (rule DiffI, simp)
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in alive_co2sobj_closefd', simp+)
+apply (frule_tac obj = obj in co2sobj_closefd, simp)
+apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)
+apply (simp, rule notI, simp, frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd)
+apply (erule_tac x = "O_proc pa" in allE, simp)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_proc p", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (case_tac "obj = O_file a", rule_tac x = "O_file f'" in exI)
+apply (case_tac "f' = a", simp add:same_inode_files_prop9 file_of_pfd_is_file)
+apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps)
+apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
+apply (frule_tac obj = obj in co2sobj_closefd, simp)
+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)
+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)
+apply (rule disjI2, rule disjI2, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp)
+apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
+apply (case_tac "f = a", simp add:alive_simps)
+apply (case_tac "f \<in> same_inode_files s a", rule disjI1)
+apply (simp add:co2sobj_simps split:if_splits option.splits t_sobject.splits)
+apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop)
+apply (erule bexE, erule conjE)
+apply (erule_tac x = f'' in ballE, simp, simp)
+apply (rule disjI2, rule disjI2, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule disjI2, rule disjI2, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule disjI2, rule disjI2, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule disjI2, rule disjI2, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule impI)
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp)
+apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
+apply (rule notI, simp add:co2sobj_closefd)
+apply (erule_tac x = obj in allE, simp)
+apply (case_tac "f = a", simp add:alive_simps)
+apply (case_tac "f \<in> same_inode_files s a", rule disjI1)
+apply (simp add:co2sobj_simps split:if_splits option.splits t_sobject.splits)
+apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop)
+apply (erule bexE, erule conjE)
+apply (erule_tac x = f'' in ballE, simp, simp)
+apply (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI)
+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 add:is_file_simps)
+apply (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI)
+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 (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI)
+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 add:is_dir_simps)
+apply (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI)
+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 (tactic {*my_setiff_tac 1*})
+
+
+
+
+defer
+apply (rule impI)
+apply (simp add:update_s2ss_obj_def)
+apply (rule conjI, rule impI, erule exE, erule conjE)
+apply (simp add:s2ss_def)
+apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE)
+apply (simp)
+apply (case_tac "obj = O_proc p")
+apply (simp add:co2sobj.simps tainted_eq_Tainted split:if_splits)
+apply (rule disjI2, rule_tac x = obj in exI, erule conjE)
+apply (simp add:alive_co2sobj_closefd')
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp split:t_object.splits if_splits)
+apply (simp, erule disjE)
+apply (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")
+apply (rule_tac x = obj' in exI, simp add:alive_co2sobj_closefd1)
+apply (frule_tac obj = obj' in co2sobj_closefd, simp add:alive_co2sobj_closefd1)
+apply (clarsimp split:t_object.splits if_splits option.splits simp:tainted_eq_Tainted co2sobj.simps)
+apply (rule_tac x = obj in exI, simp add:alive_co2sobj_closefd1)
+apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd1)
+apply (clarsimp split:t_object.splits if_splits option.splits simp:tainted_eq_Tainted co2sobj.simps)
+apply (rule impI)
+apply (simp add:s2ss_def)
+apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE)
+apply (simp)
+apply (case_tac "obj = O_proc p")
+apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted split:if_splits)
+apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp add:alive_co2sobj_closefd')
+apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd1)
+apply (clarsimp split:t_object.splits if_splits option.splits simp:tainted_eq_Tainted co2sobj.simps)
+apply (rule notI, erule_tac x = obj in allE, simp add:alive_co2sobj_closefd')
+apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd1)
+apply (clarsimp split:t_object.splits if_splits option.splits)
+apply (simp)
+apply (erule disjE)
+apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (erule exE|erule conjE)+
+apply (rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd1)
+apply (clarsimp split:t_object.splits if_splits option.splits
+ simp:tainted_eq_Tainted co2sobj.simps alive_co2sobj_closefd1)
+done
+
+
+
+
lemmas s2ss_simps = s2ss_execve s2ss_clone s2ss_ptrace s2ss_kill s2ss_exit s2ss_open
- s2ss_readfile s2ss_writefile
+ s2ss_readfile s2ss_writefile s2ss_closefd