# HG changeset patch
# User chunhan
# Date 1381817513 -28800
# Node ID 20207806603e417462b999f6c4b2f7a9e5b8a8cd
# Parent  d7cb2fb2e3b4ba41bb45262221c26f7a6ed2e34b
s2ss_deleteshm s2ss_detach

diff -r d7cb2fb2e3b4 -r 20207806603e S2ss_prop2.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/S2ss_prop2.thy	Tue Oct 15 14:11:53 2013 +0800
@@ -0,0 +1,258 @@
+(*<*)
+theory S2ss_prop2
+imports Main Flask Flask_type Static Static_type Init_prop Tainted_prop Valid_prop Alive_prop Co2sobj_prop S2ss_prop
+begin
+(*>*)
+
+context tainting_s begin
+
+definition unbackuped_sprocs :: "t_state \<Rightarrow> t_event \<Rightarrow> t_process set \<Rightarrow> t_sobject set"
+where
+  "unbackuped_sprocs s e procs \<equiv> 
+    {sp | p sp. p \<in> procs \<and> co2sobj s (O_proc p) = Some sp \<and> 
+                (\<forall> p' \<in> procs. co2sobj (e # s) (O_proc p') \<noteq> Some sp) \<and>
+                (\<forall> p' \<in> (current_procs s - procs). co2sobj s (O_proc p') \<noteq> Some sp)}"
+
+definition update_s2ss_procs :: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_event \<Rightarrow> t_process set \<Rightarrow> t_static_state"
+where
+  "update_s2ss_procs s ss e procs \<equiv> 
+     ss \<union> {sp | p sp. p \<in> procs \<and> co2sobj (e # s) (O_proc p) = Some sp}
+        - unbackuped_sprocs s e procs"
+ (* new sp after event may exists as same before the event in procs *)
+
+lemma unbked_sps_D:
+  "\<lbrakk>x \<in> unbackuped_sprocs s e procs; p \<in> procs\<rbrakk> \<Longrightarrow> co2sobj (e # s) (O_proc p) \<noteq> Some x"
+by (auto simp add:unbackuped_sprocs_def)
+
+lemma unbked_sps_D':
+  "\<lbrakk>x \<in> unbackuped_sprocs s e procs; p \<notin> procs; p \<in> current_procs s; 
+    co2sobj (e # s) (O_proc p) = co2sobj s (O_proc p)\<rbrakk>
+   \<Longrightarrow> co2sobj (e # s) (O_proc p) \<noteq> Some x"
+by (auto simp:unbackuped_sprocs_def)
+
+lemma not_unbked_sps_D:
+  "\<lbrakk>x \<notin> unbackuped_sprocs s e procs; p \<in> procs; co2sobj s (O_proc p) = Some x\<rbrakk> 
+   \<Longrightarrow> (\<exists> p' \<in> procs. co2sobj (e # s) (O_proc p') = Some x) \<or>
+       (\<exists> p' \<in> current_procs s - procs. co2sobj s (O_proc p') = Some x)"
+by (auto simp:unbackuped_sprocs_def)
+
+lemma unbked_sps_I:
+  "\<lbrakk>co2sobj s obj = Some x; \<forall> p. obj \<noteq> O_proc p\<rbrakk> \<Longrightarrow> x \<notin> unbackuped_sprocs s' e procs"
+apply (case_tac obj)
+apply (auto simp add:unbackuped_sprocs_def co2sobj.simps split:option.splits)
+done
+
+lemma co2sobj_proc_deleteshm:
+  "\<lbrakk>valid (DeleteShM p h # s); \<forall>flag. (pa, flag) \<notin> procs_of_shm s h; pa \<in> current_procs s\<rbrakk>
+   \<Longrightarrow> co2sobj (DeleteShM p h # s) (O_proc pa) = co2sobj s (O_proc pa)"
+thm co2sobj_deleteshm
+apply (frule_tac obj = "O_proc pa" in co2sobj_deleteshm, simp)
+apply (frule vd_cons, frule_tac p = pa in current_proc_has_sp, simp, erule exE)
+apply (auto dest!:current_proc_has_sp' current_has_sec' current_shm_has_sh'
+  split:t_object.splits option.splits if_splits dest:flag_of_proc_shm_prop1
+  simp:co2sobj.simps tainted_eq_Tainted cp2sproc_deleteshm)
+done
+
+lemma s2ss_deleteshm:
+  "valid (DeleteShM p h # s) \<Longrightarrow> s2ss (DeleteShM p h # s) = 
+     (case ch2sshm s h of
+        Some sh \<Rightarrow> del_s2ss_obj s 
+                      (update_s2ss_procs s (s2ss s) (DeleteShM p h) {p'| p' flag. (p', flag) \<in> procs_of_shm s h})
+                      (O_shm h) (S_shm sh)
+      | _       \<Rightarrow> {})"
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac "ch2sshm s h")
+apply (drule current_shm_has_sh', simp, simp)
+apply (simp add:del_s2ss_obj_def)
+apply (tactic {*my_clarify_tac 1*})
+ 
+unfolding update_s2ss_procs_def
+apply (tactic {*my_seteq_tac 1*})
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac "\<exists> flag. (pa, flag) \<in> procs_of_shm s h")
+apply (erule exE, rule DiffI, rule UnI2, simp)
+apply (rule_tac x = pa in exI, simp, rule_tac x = flag in exI, simp)
+apply (rule notI, drule_tac p = pa in unbked_sps_D, simp)
+apply (rule_tac x = flag in exI, simp, simp)
+apply (rule DiffI, rule UnI1, simp)
+apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm split:option.splits)
+apply (simp add:cp2sproc_deleteshm split:option.splits if_splits)
+apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (drule current_has_sec', simp, simp)
+apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (drule flag_of_proc_shm_prop1, simp, simp)
+apply (drule flag_of_proc_shm_prop1, simp, simp)
+apply (rule notI, drule_tac p = pa in unbked_sps_D', simp+)
+apply (simp add:co2sobj_proc_deleteshm)
+apply (simp add:co2sobj_proc_deleteshm)
+apply (rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_deleteshm is_file_simps)
+apply (erule unbked_sps_I, simp)
+apply (rule DiffI,rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_deleteshm)
+apply (erule unbked_sps_I, simp)
+apply (rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_deleteshm is_dir_simps)
+apply (erule unbked_sps_I, simp)
+apply (rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_deleteshm)
+apply (erule unbked_sps_I, simp)
+
+apply (erule DiffE, erule UnE)
+apply (tactic {*my_setiff_tac 1*})
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac "\<exists> flag. (pa, flag) \<in> procs_of_shm s h", erule exE)
+apply (drule_tac p = pa in not_unbked_sps_D, simp)
+apply (rule_tac x = flag in exI, simp)
+apply (simp, erule disjE, clarsimp)
+apply (rule_tac x = "O_proc p'" in exI, simp add:procs_of_shm_prop2)
+apply (erule bexE, simp, (erule conjE)+)
+apply (frule_tac pa = p' in co2sobj_proc_deleteshm, simp+)
+apply (rule_tac x = "O_proc p'" in exI, simp)
+apply (frule_tac pa = pa in co2sobj_proc_deleteshm, simp+)
+apply (rule_tac x = "O_proc pa" in exI, simp)
+apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm is_file_simps)
+apply (frule_tac co2sobj_sshm_imp, erule exE)
+apply (case_tac "ha = h")
+apply (rule_tac x = obj' in exI, simp add:co2sobj_deleteshm)
+apply (simp add:co2sobj.simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm)
+apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm is_dir_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm)
+apply (tactic {*my_setiff_tac 1*}, clarsimp)
+apply (rule_tac x = "O_proc pa" in exI, simp add:procs_of_shm_prop2)
+
+apply (tactic {*my_clarify_tac 1*})
+unfolding update_s2ss_procs_def
+apply (tactic {*my_seteq_tac 1*})
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac "\<exists> flag. (pa, flag) \<in> procs_of_shm s h")
+apply (erule exE, rule DiffI, rule DiffI, rule UnI2, simp)
+apply (rule_tac x = pa in exI, simp, rule_tac x = flag in exI, simp)
+apply (rule notI, drule_tac p = pa in unbked_sps_D, simp)
+apply (rule_tac x = flag in exI, simp, simp)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)
+apply (rule DiffI, rule DiffI, rule UnI1, simp)
+apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm split:option.splits)
+apply (simp add:cp2sproc_deleteshm split:option.splits if_splits)
+apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (drule current_has_sec', simp, simp)
+apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (drule flag_of_proc_shm_prop1, simp, simp)
+apply (drule flag_of_proc_shm_prop1, simp, simp)
+apply (rule notI, drule_tac p = pa in unbked_sps_D', simp+)
+apply (simp add:co2sobj_proc_deleteshm)
+apply (simp add:co2sobj_proc_deleteshm)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)
+apply (rule DiffI, rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_deleteshm is_file_simps)
+apply (erule unbked_sps_I, simp, rule notI, simp add:co2sobj.simps)
+apply (case_tac "ha = h", simp)
+apply (rule DiffI, rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_deleteshm)
+apply (erule unbked_sps_I, simp)
+apply (rule notI, simp add:co2sobj_deleteshm, erule_tac x = "O_shm ha" in allE, simp)
+apply (rule DiffI, rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_deleteshm is_dir_simps)
+apply (erule unbked_sps_I, simp, rule notI, simp add:co2sobj.simps split:option.splits)
+apply (rule DiffI, rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_deleteshm)
+apply (erule unbked_sps_I, simp, rule notI, simp add:co2sobj.simps split:option.splits)
+
+apply (erule DiffE, erule DiffE, erule UnE)
+apply (tactic {*my_setiff_tac 1*})
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac "\<exists> flag. (pa, flag) \<in> procs_of_shm s h", erule exE)
+apply (drule_tac p = pa in not_unbked_sps_D, simp)
+apply (rule_tac x = flag in exI, simp)
+apply (simp, erule disjE, clarsimp)
+apply (rule_tac x = "O_proc p'" in exI, simp add:procs_of_shm_prop2)
+apply (erule bexE, simp, (erule conjE)+)
+apply (frule_tac pa = p' in co2sobj_proc_deleteshm, simp+)
+apply (rule_tac x = "O_proc p'" in exI, simp)
+apply (frule_tac pa = pa in co2sobj_proc_deleteshm, simp+)
+apply (rule_tac x = "O_proc pa" in exI, simp)
+apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm is_file_simps)
+apply (case_tac "ha = h", simp add:co2sobj.simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm)
+apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm is_dir_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_deleteshm)
+apply (tactic {*my_setiff_tac 1*}, clarsimp)
+apply (rule_tac x = "O_proc pa" in exI, simp add:procs_of_shm_prop2)
+done
+
+lemma s2ss_detach:
+  "valid (Detach p h # s) \<Longrightarrow> s2ss (Detach p h # s) = (
+     case (cp2sproc s p, cp2sproc (Detach p h # 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> {} )"
+apply (frule vd_cons, frule vt_grant_os)
+apply (case_tac "cp2sproc s p")
+apply (drule current_proc_has_sp', simp+)
+apply (case_tac "cp2sproc (Detach p h # s) p")
+apply (drule current_proc_has_sp', simp+)
+apply (erule exE|erule conjE)+
+apply (simp add:update_s2ss_obj_def)
+apply (tactic {*my_clarify_tac 1*})
+
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_proc p")
+apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (rule disjI2, simp, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_detach, simp add:alive_simps)
+apply (simp add:is_file_simps is_dir_simps split:t_object.splits)
+apply (simp add:co2sobj.simps, simp add:co2sobj.simps)
+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")
+apply (rule_tac x = obj' in exI)
+apply (frule_tac obj = obj' in co2sobj_detach, simp)
+apply (auto simp add:co2sobj.simps tainted_eq_Tainted is_file_simps is_dir_simps split:t_object.splits)[1]
+apply (rule_tac x = obj in exI)
+apply (simp add:co2sobj_detach)
+apply (auto simp add:co2sobj.simps tainted_eq_Tainted is_file_simps is_dir_simps split:t_object.splits)[1]
+
+apply (tactic {*my_clarify_tac 1*})
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_proc p")
+apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (rule disjI2, rule DiffI, simp, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_detach, simp add:alive_simps)
+apply (simp add:is_file_simps is_dir_simps split:t_object.splits)
+apply (simp add:co2sobj.simps, simp add:co2sobj.simps)
+apply (rule notI, simp, erule_tac x = obj in allE, erule impE, simp add:alive_simps, simp)
+apply (frule_tac obj = obj in co2sobj_detach)
+apply (simp add:alive_simps)
+apply (simp split:t_object.splits)
+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*}, simp)
+apply (case_tac "obj = O_proc p")
+apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (rule_tac x = obj in exI)
+apply (simp add:co2sobj_detach)
+apply (auto simp add:co2sobj.simps tainted_eq_Tainted is_file_simps is_dir_simps split:t_object.splits)[1]
+done
+
+
+
+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 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_attach1:
+  "valid (Attach p h flag # s) \<Longrightarrow> s2ss (Attach p h flag # s) = "
+
+lemma s2ss_Detach:
+  "valid (Detach p h # s) \<Longrightarrow> s2ss (Detach p h # s) = "
+
+
+
+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
+
+
+end
+
+end
\ No newline at end of file