226 apply (rule_tac x = obj in exI) |
226 apply (rule_tac x = obj in exI) |
227 apply (simp add:co2sobj_detach) |
227 apply (simp add:co2sobj_detach) |
228 apply (auto simp add:co2sobj.simps tainted_eq_Tainted is_file_simps is_dir_simps split:t_object.splits)[1] |
228 apply (auto simp add:co2sobj.simps tainted_eq_Tainted is_file_simps is_dir_simps split:t_object.splits)[1] |
229 done |
229 done |
230 |
230 |
231 |
231 definition attach_Tainted_procs :: "t_state \<Rightarrow> t_process \<Rightarrow> t_shm \<Rightarrow> t_shm_attach_flag \<Rightarrow> t_process set" |
232 |
232 where |
233 lemma s2ss_attach1: |
233 "attach_Tainted_procs s p h flag \<equiv> |
234 "\<lbrakk>valid (Attach p h SHM_RDWR # s); O_proc p \<in> Tainted s\<rbrakk>\<Longrightarrow> s2ss (Attach p h SHM_RDWR # s) = ( |
234 (if (O_proc p \<in> Tainted s \<and> flag = SHM_RDWR) |
235 |
235 then {p''. \<exists> p' flag'. (p', flag') \<in> procs_of_shm s h \<and> info_flow_shm s p' p'' \<and> |
236 " |
236 O_proc p'' \<notin> Tainted s} |
237 |
237 else if (\<exists> p'. O_proc p' \<in> Tainted s \<and> (p', SHM_RDWR) \<in> procs_of_shm s h) |
238 lemma s2ss_attach1: |
238 then {p'. info_flow_shm s p p' \<and> O_proc p' \<notin> Tainted s} |
239 "\<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> |
239 else {})" |
240 \<Longrightarrow> s2ss (Attach p h SHM_RDONLY # s) = " |
240 |
241 |
241 lemma attach_Tainted_procs_prop1: |
242 lemma s2ss_attach1: |
242 "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}" |
243 "valid (Attach p h flag # s) \<Longrightarrow> s2ss (Attach p h flag # s) = " |
243 apply (auto simp:attach_Tainted_procs_def intro:info_flow_shm_Tainted) |
244 |
244 done |
245 lemma s2ss_Detach: |
245 |
246 "valid (Detach p h # s) \<Longrightarrow> s2ss (Detach p h # s) = " |
246 lemma attach_Tainted_procs_prop2: |
|
247 "valid (Attach p h flag # s) \<Longrightarrow> {O_proc p'| p'. p' \<in> attach_Tainted_procs s p h flag} \<inter> Tainted s = {}" |
|
248 by (auto simp:attach_Tainted_procs_def) |
|
249 |
|
250 lemma attach_Tainted_procs_prop3: |
|
251 "\<lbrakk>p' \<in> attach_Tainted_procs s p h flag; valid s\<rbrakk> \<Longrightarrow> p' \<in> current_procs s" |
|
252 by (auto simp:attach_Tainted_procs_def info_shm_flow_in_procs split:if_splits) |
|
253 |
|
254 lemma co2sobj_attach': |
|
255 "\<lbrakk>valid (Attach p h flag # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Attach p h flag # s) obj = |
|
256 (case obj of |
|
257 O_proc p' \<Rightarrow> if (p' = p) |
|
258 then (case cp2sproc (Attach p h flag # s) p of |
|
259 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s \<or> p \<in> attach_Tainted_procs s p h flag)) |
|
260 | _ \<Rightarrow> None) |
|
261 else if (p' \<in> attach_Tainted_procs s p h flag) |
|
262 then case cp2sproc s p' of |
|
263 None \<Rightarrow> None |
|
264 | Some sp \<Rightarrow> Some (S_proc sp True) |
|
265 else co2sobj s obj |
|
266 | _ \<Rightarrow> co2sobj s obj)" |
|
267 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
|
268 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted co2sobj.simps) |
|
269 |
|
270 apply (frule current_proc_has_sp, simp, erule exE, (erule conjE)+) |
|
271 apply (case_tac "cp2sproc (Attach p h flag # s) nat", drule current_proc_has_sp', simp+) |
|
272 apply (case_tac "cp2sproc (Attach p h flag # s) p", drule current_proc_has_sp', simp+) |
|
273 apply (simp add:tainted_eq_Tainted attach_Tainted_procs_prop1 del:Tainted.simps) |
|
274 apply (simp add:cp2sproc_attach split:if_splits) |
|
275 |
|
276 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' |
|
277 simp:current_files_simps cf2sfiles_simps cf2sfile_simps tainted_eq_Tainted |
|
278 same_inode_files_prop6 |
|
279 dest:is_file_in_current is_dir_in_current) |
|
280 done |
|
281 |
|
282 lemma s2ss_attach: |
|
283 "valid (Attach p h flag # s) \<Longrightarrow> s2ss (Attach p h flag # s) = |
|
284 update_s2ss_procs s (s2ss s) (Attach p h flag) (attach_Tainted_procs s p h flag \<union> {p})" |
|
285 apply (frule vt_grant_os, frule vd_cons) |
|
286 apply (case_tac "cp2sproc s p", drule current_proc_has_sp', simp, simp) |
|
287 apply (case_tac "ch2sshm s h", drule current_shm_has_sh', simp, simp) |
|
288 apply (case_tac "cp2sproc (Attach p h flag # s) p", drule current_proc_has_sp', simp, simp) |
|
289 |
|
290 unfolding update_s2ss_procs_def |
|
291 apply (tactic {*my_seteq_tac 1*}) |
|
292 apply (erule_tac obj = obj in co2sobj_some_caseD) |
|
293 apply (case_tac "pa = p") |
|
294 apply (rule DiffI, rule UnI2, simp, rule_tac x = pa in exI, simp) |
|
295 apply (rule notI, drule_tac p = pa in unbked_sps_D, simp, simp) |
|
296 apply (case_tac "pa \<in> attach_Tainted_procs s p h flag") |
|
297 apply (rule DiffI, rule UnI2, simp) |
|
298 apply (rule_tac x = pa in exI, simp) |
|
299 apply (rule notI, drule_tac p = pa in unbked_sps_D, simp, simp) |
|
300 apply (rule DiffI, rule UnI1, simp) |
|
301 apply (rule_tac x = obj in exI, simp add:co2sobj_attach') |
|
302 apply (rule notI, drule_tac p = pa in unbked_sps_D', simp+) |
|
303 apply (simp add:co2sobj_attach') |
|
304 apply (simp add:co2sobj_attach') |
|
305 apply (rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_attach' is_file_simps) |
|
306 apply (erule unbked_sps_I, simp) |
|
307 apply (rule DiffI,rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_attach') |
|
308 apply (erule unbked_sps_I, simp) |
|
309 apply (rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_attach' is_dir_simps) |
|
310 apply (erule unbked_sps_I, simp) |
|
311 apply (rule DiffI, rule UnI1, simp, rule_tac x = obj in exI, simp add:co2sobj_attach') |
|
312 apply (erule unbked_sps_I, simp) |
|
313 |
|
314 apply (erule DiffE, erule UnE) |
|
315 apply (tactic {*my_setiff_tac 1*}) |
|
316 apply (erule_tac obj = obj in co2sobj_some_caseD) |
|
317 apply (case_tac "pa \<in> attach_Tainted_procs s p h flag \<union> {p}") |
|
318 apply (drule_tac p = pa in not_unbked_sps_D, simp, simp) |
|
319 apply (erule disjE, erule bexE) |
|
320 apply (rule_tac x = "O_proc p'" in exI, simp) |
|
321 apply (erule disjE, simp, simp add:attach_Tainted_procs_prop3) |
|
322 apply (erule bexE, simp, (erule conjE)+) |
|
323 apply (rule_tac x = "O_proc p'" in exI, simp add:co2sobj_attach') |
|
324 apply (rule_tac x = "O_proc pa" in exI, simp add:co2sobj_attach') |
|
325 apply (rule_tac x = obj in exI, simp add:co2sobj_attach' is_file_simps) |
|
326 apply (rule_tac x = obj in exI, simp add:co2sobj_attach') |
|
327 apply (rule_tac x = obj in exI, simp add:co2sobj_attach' is_dir_simps) |
|
328 apply (rule_tac x = obj in exI, simp add:co2sobj_attach') |
|
329 apply (tactic {*my_setiff_tac 1*}, clarsimp) |
|
330 apply (rule_tac x = "O_proc pa" in exI, simp) |
|
331 apply (erule disjE, simp, simp add:attach_Tainted_procs_prop3) |
|
332 done |
247 |
333 |
248 |
334 |
249 |
335 |
250 lemmas s2ss_simps = s2ss_execve s2ss_clone s2ss_ptrace s2ss_kill s2ss_exit s2ss_open |
336 lemmas s2ss_simps = s2ss_execve s2ss_clone s2ss_ptrace s2ss_kill s2ss_exit s2ss_open |
251 s2ss_readfile s2ss_writefile s2ss_closefd s2ss_unlink s2ss_rmdir s2ss_linkhard |
337 s2ss_readfile s2ss_writefile s2ss_closefd s2ss_unlink s2ss_rmdir s2ss_linkhard |
252 s2ss_truncate s2ss_createmsgq s2ss_sendmsg s2ss_removemsgq s2ss_recvmsg |
338 s2ss_truncate s2ss_createmsgq s2ss_sendmsg s2ss_removemsgq s2ss_recvmsg |
253 s2ss_createshm |
339 s2ss_createshm s2ss_detach s2ss_deleteshm s2ss_attach |
254 |
340 |
255 |
341 |
256 end |
342 end |
257 |
343 |
258 end |
344 end |