2293 same_inode_files_prop6 ch2sshm_simps |
2293 same_inode_files_prop6 ch2sshm_simps |
2294 dest!:current_shm_has_sh' |
2294 dest!:current_shm_has_sh' |
2295 dest:is_file_in_current is_dir_in_current) |
2295 dest:is_file_in_current is_dir_in_current) |
2296 done |
2296 done |
2297 |
2297 |
|
2298 declare Product_Type.split_paired_Ex Product_Type.split_paired_All [simp del] |
|
2299 |
|
2300 lemma info_flow_shm_prop1: |
|
2301 "p \<in> current_procs s \<Longrightarrow> info_flow_shm s p p" |
|
2302 by (simp add:info_flow_shm_def) |
|
2303 |
2298 lemma co2sobj_attach: |
2304 lemma co2sobj_attach: |
2299 "\<lbrakk>valid (Attach p h flag # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Attach p h flag # s) obj = ( |
2305 "\<lbrakk>valid (Attach p h flag # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Attach p h flag # s) obj = ( |
2300 case obj of |
2306 case obj of |
2301 O_proc p' \<Rightarrow> if (p' = p) |
2307 O_proc p' \<Rightarrow> if (info_flow_shm s p p') |
2302 then (case (cp2sproc (Attach p h flag # s) p) of |
2308 then (case (cp2sproc (Attach p h flag # s) p') of |
2303 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s \<or> |
2309 Some sp \<Rightarrow> Some (S_proc sp (O_proc p' \<in> Tainted s \<or> |
2304 (\<exists> p'. O_proc p' \<in> Tainted s \<and> (p', SHM_RDWR) \<in> procs_of_shm s h))) |
2310 (\<exists> p''. O_proc p'' \<in> Tainted s \<and> (p'', SHM_RDWR) \<in> procs_of_shm s h))) |
2305 | _ \<Rightarrow> None) |
2311 | _ \<Rightarrow> None) |
2306 else if (\<exists> flag'. (p', flag') \<in> procs_of_shm s h) |
2312 else if (\<exists> p'' flag'. (p'', flag') \<in> procs_of_shm s h \<and> flag = SHM_RDWR \<and> O_proc p \<in> Tainted s \<and> |
|
2313 info_flow_shm s p'' p') |
2307 then (case (cp2sproc s p') of |
2314 then (case (cp2sproc s p') of |
2308 Some sp \<Rightarrow> Some (S_proc sp (O_proc p' \<in> Tainted s \<or> |
2315 Some sp \<Rightarrow> Some (S_proc sp True) |
2309 (O_proc p \<in> Tainted s \<and> flag = SHM_RDWR))) |
|
2310 | _ \<Rightarrow> None) |
2316 | _ \<Rightarrow> None) |
2311 else co2sobj s obj |
2317 else co2sobj s obj |
2312 | _ \<Rightarrow> co2sobj s obj)" |
2318 | _ \<Rightarrow> co2sobj s obj)" |
2313 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
2319 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
2314 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) |
2320 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) |
2315 |
2321 |
2316 apply (rule conjI|rule impI|erule exE)+ |
2322 apply (rule conjI|rule impI|erule exE)+ |
2317 apply (simp split:option.splits) |
2323 apply (simp split:option.splits del:split_paired_Ex) |
2318 apply (rule impI, frule current_proc_has_sp, simp) |
2324 apply (rule impI, frule current_proc_has_sp, simp) |
2319 apply ((erule exE)+, auto simp:cp2sproc_attach tainted_eq_Tainted)[1] |
2325 apply ((erule exE)+, auto simp:tainted_eq_Tainted intro:info_flow_shm_Tainted)[1] |
2320 apply (rule impI|rule conjI)+ |
2326 apply (rule impI, simp add:tainted_eq_Tainted split:option.splits del:split_paired_Ex) |
2321 apply (subgoal_tac "p \<in> current_procs (Attach p h flag # s)") |
2327 apply (auto simp:info_flow_shm_prop1 cp2sproc_attach dest!:current_proc_has_sp')[1] |
2322 apply (drule_tac p = p in current_proc_has_sp, simp, erule exE) |
2328 |
2323 apply (auto simp:tainted_eq_Tainted)[1] |
2329 apply (case_tac "cp2sproc (Attach p h flag # s) nat") |
2324 apply (simp, rule impI) |
2330 apply (drule current_proc_has_sp', simp+) |
2325 apply (subgoal_tac "nat \<in> current_procs (Attach p h flag # s)") |
2331 |
2326 apply (drule_tac p = nat in current_proc_has_sp, simp, erule exE) |
2332 apply (rule conjI|erule exE|erule conjE|rule impI)+ |
2327 apply (drule_tac p = nat in current_proc_has_sp, simp, erule exE) |
2333 apply (simp add:tainted_eq_Tainted) |
2328 apply (auto simp:cp2sproc_attach tainted_eq_Tainted)[1] |
2334 apply (auto simp:info_flow_shm_prop1 cp2sproc_attach intro:info_flow_shm_Tainted dest!:current_proc_has_sp')[1] |
2329 apply simp |
2335 apply (auto simp:info_flow_shm_prop1 cp2sproc_attach tainted_eq_Tainted intro:info_flow_shm_Tainted dest!:current_proc_has_sp' |
|
2336 split:option.splits if_splits)[1] |
|
2337 |
2330 |
2338 |
2331 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' |
2339 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' |
2332 simp:current_files_simps cf2sfiles_simps cf2sfile_simps tainted_eq_Tainted |
2340 simp:current_files_simps cf2sfiles_simps cf2sfile_simps tainted_eq_Tainted |
2333 same_inode_files_prop6 |
2341 same_inode_files_prop6 |
2334 dest:is_file_in_current is_dir_in_current) |
2342 dest:is_file_in_current is_dir_in_current) |