134 by (auto simp:same_inode_files_def split:if_splits) |
134 by (auto simp:same_inode_files_def split:if_splits) |
135 |
135 |
136 lemma same_inode_files_prop5: |
136 lemma same_inode_files_prop5: |
137 "f' \<in> same_inode_files s f \<Longrightarrow> f \<in> same_inode_files s f'" |
137 "f' \<in> same_inode_files s f \<Longrightarrow> f \<in> same_inode_files s f'" |
138 by (auto simp:same_inode_files_def is_file_def split:if_splits) |
138 by (auto simp:same_inode_files_def is_file_def split:if_splits) |
|
139 |
|
140 lemma same_inode_files_prop6: |
|
141 "f' \<in> same_inode_files s f \<Longrightarrow> same_inode_files s f' = same_inode_files s f" |
|
142 by (auto simp:same_inode_files_def is_file_def split:if_splits) |
|
143 |
|
144 lemma same_inode_files_prop7: |
|
145 "f' \<in> same_inode_files s f \<Longrightarrow> has_same_inode s f f'" |
|
146 thm has_same_inode_def |
|
147 apply (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits) |
|
148 |
139 |
149 |
140 (* simpset for cf2sfiles *) |
150 (* simpset for cf2sfiles *) |
141 |
151 |
142 lemma cf2sfiles_open: |
152 lemma cf2sfiles_open: |
143 "\<lbrakk>valid (Open p f flag fd opt # s); f' \<in> current_files (Open p f flag fd opt # s)\<rbrakk> |
153 "\<lbrakk>valid (Open p f flag fd opt # s); f' \<in> current_files (Open p f flag fd opt # s)\<rbrakk> |
353 then (case (cp2sproc (Execve p f fds # s) p) of |
363 then (case (cp2sproc (Execve p f fds # s) p) of |
354 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s \<or> O_file f \<in> Tainted s)) |
364 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s \<or> O_file f \<in> Tainted s)) |
355 | _ \<Rightarrow> None) |
365 | _ \<Rightarrow> None) |
356 else co2sobj s obj )" |
366 else co2sobj s obj )" |
357 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
367 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
358 apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) |
368 apply (simp_all add:current_files_simps cf2sfiles_other ch2sshm_other cq2smsgq_other tainted_eq_Tainted) |
359 apply (case_tac "cp2sproc (Execve p f fds # s) p") |
369 apply (case_tac "cp2sproc (Execve p f fds # s) p") |
360 apply (drule current_proc_has_sp', simp, simp) |
370 apply (drule current_proc_has_sp', simp, simp) |
361 apply (simp (no_asm_simp) add:cp2sproc_execve tainted_eq_Tainted split:option.splits) |
371 apply (simp (no_asm_simp) add:cp2sproc_execve tainted_eq_Tainted split:option.splits) |
362 apply (rule impI, simp add:cf2sfiles_other) |
|
363 apply (frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp) |
372 apply (frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp) |
364 apply (frule_tac ff = list in cf2sfile_other', simp_all) |
373 apply (frule_tac ff = list in cf2sfile_other', simp_all) |
365 apply (simp add:is_dir_in_current) |
374 apply (simp add:is_dir_in_current) |
366 done |
375 done |
367 |
376 |
371 then (case (cp2sproc (Clone p p' fds shms # s) p') of |
380 then (case (cp2sproc (Clone p p' fds shms # s) p') of |
372 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s)) |
381 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s)) |
373 | _ \<Rightarrow> None) |
382 | _ \<Rightarrow> None) |
374 else co2sobj s obj )" |
383 else co2sobj s obj )" |
375 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
384 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
376 apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) |
385 apply (simp_all add:current_files_simps cf2sfiles_other ch2sshm_other cq2smsgq_other tainted_eq_Tainted) |
377 apply (case_tac "cp2sproc (Clone p p' fds shms # s) p'") |
386 apply (case_tac "cp2sproc (Clone p p' fds shms # s) p'") |
378 apply (drule current_proc_has_sp', simp, simp) |
387 apply (drule current_proc_has_sp', simp, simp) |
379 apply ((erule conjE)+, frule_tac p = p in current_proc_has_sec, simp, erule exE, simp) |
388 apply ((erule conjE)+, frule_tac p = p in current_proc_has_sec, simp, erule exE, simp) |
380 apply (rule conjI, rule impI, simp) |
389 apply (rule conjI, rule impI, simp) |
381 apply (simp (no_asm_simp) add:cp2sproc_clone tainted_eq_Tainted split:option.splits) |
390 apply (simp (no_asm_simp) add:cp2sproc_clone tainted_eq_Tainted split:option.splits) |
382 |
391 |
383 apply (rule impI, simp add:cf2sfiles_other) |
|
384 apply (frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp) |
392 apply (frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp) |
385 apply (frule_tac ff = list in cf2sfile_other', simp_all) |
393 apply (frule_tac ff = list in cf2sfile_other', simp_all) |
386 apply (simp add:is_dir_in_current) |
394 apply (simp add:is_dir_in_current) |
387 done |
395 done |
388 |
396 |
399 | _ \<Rightarrow> None) |
407 | _ \<Rightarrow> None) |
400 else co2sobj s (O_proc p'') |
408 else co2sobj s (O_proc p'') |
401 | _ \<Rightarrow> co2sobj s obj)" |
409 | _ \<Rightarrow> co2sobj s obj)" |
402 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
410 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
403 apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other cf2sfiles_other tainted_eq_Tainted) |
411 apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other cf2sfiles_other tainted_eq_Tainted) |
|
412 |
404 apply (auto simp:cp2sproc_other tainted_eq_Tainted split:option.splits |
413 apply (auto simp:cp2sproc_other tainted_eq_Tainted split:option.splits |
405 dest!:current_proc_has_sec' current_proc_has_sp' intro:info_flow_shm_Tainted)[1] |
414 dest!:current_proc_has_sec' current_proc_has_sp' intro:info_flow_shm_Tainted)[1] |
406 |
415 |
407 apply (frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp) |
416 apply (frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp) |
408 apply (frule_tac ff = list in cf2sfile_other', simp_all) |
417 apply (frule_tac ff = list in cf2sfile_other', simp_all) |
422 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s)) |
431 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s)) |
423 | _ \<Rightarrow> None) |
432 | _ \<Rightarrow> None) |
424 else co2sobj s (O_proc p') |
433 else co2sobj s (O_proc p') |
425 | _ \<Rightarrow> co2sobj s obj )" |
434 | _ \<Rightarrow> co2sobj s obj )" |
426 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
435 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
427 apply (auto simp:cp2sproc_simps cf2sfiles_simps cf2sfile_simps current_files_simps |
436 apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits |
428 is_file_simps tainted_eq_Tainted split:option.splits |
437 dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1] |
429 dest!:current_proc_has_sp' intro:info_flow_shm_Tainted) |
438 |
|
439 apply (simp split:if_splits t_object.splits) |
|
440 apply (rule conjI, rule impI, erule conjE, erule exE, simp, (erule exE|erule conjE)+) |
|
441 apply (case_tac "cf2sfile (Open p f flag fd (Some y) # s) f") |
|
442 apply (drule current_file_has_sfile', simp, simp add:current_files_simps, simp) |
|
443 apply (frule_tac f' = f in cf2sfiles_open, simp add:current_files_simps) |
|
444 apply (simp add:tainted_eq_Tainted) |
|
445 apply (rule impI, rule notI, drule Tainted_in_current, simp, simp add:is_file_in_current) |
|
446 apply (rule impI, simp add:tainted_eq_Tainted cf2sfiles_open is_file_in_current split:option.splits) |
|
447 |
430 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) |
448 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) |
431 apply (auto simp:cp2sproc_simps cf2sfiles_simps cf2sfile_simps current_files_simps |
449 |
432 is_file_simps tainted_eq_Tainted split:option.splits |
450 apply (frule is_dir_in_current) |
433 dest!:current_proc_has_sp' current_file_has_sfile' intro:info_flow_shm_Tainted) |
451 apply (frule_tac f' = list in cf2sfile_open) |
434 apply ( |
452 apply (simp add:current_files_simps split:option.splits) |
435 apply |
453 apply (simp split:if_splits option.splits) |
|
454 done |
|
455 |
|
456 lemma co2sobj_readfile: |
|
457 "\<lbrakk>valid (ReadFile p fd # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (ReadFile p fd # s) obj = ( |
|
458 case obj of |
|
459 O_proc p' \<Rightarrow> (case (file_of_proc_fd s p fd) of |
|
460 Some f \<Rightarrow> (if (info_flow_shm s p p' \<and> O_file f \<in> Tainted s) |
|
461 then (case (cp2sproc s p') of |
|
462 Some sp \<Rightarrow> Some (S_proc sp True) |
|
463 | _ \<Rightarrow> None) |
|
464 else co2sobj s obj) |
|
465 | _ \<Rightarrow> None) |
|
466 | _ \<Rightarrow> co2sobj s obj)" |
|
467 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
|
468 apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits |
|
469 dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1] |
|
470 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) |
|
471 |
|
472 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' |
|
473 simp:current_files_simps cf2sfiles_simps cf2sfile_simps |
|
474 dest:is_file_in_current is_dir_in_current) |
|
475 done |
|
476 |
|
477 lemma co2sobj_writefile: |
|
478 "\<lbrakk>valid (WriteFile p fd # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (WriteFile p fd # s) obj = ( |
|
479 case obj of |
|
480 O_file f' \<Rightarrow> (case (file_of_proc_fd s p fd) of |
|
481 Some f \<Rightarrow> (if (f \<in> same_inode_files s f') |
|
482 then Some (S_file (cf2sfiles s f') |
|
483 (O_file f' \<in> Tainted s \<or> O_proc p \<in> Tainted s)) |
|
484 else co2sobj s obj) |
|
485 | _ \<Rightarrow> None) |
|
486 | _ \<Rightarrow> co2sobj s obj)" |
|
487 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
|
488 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) |
|
489 |
|
490 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp' |
|
491 simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted |
|
492 same_inode_files_prop6 |
|
493 dest:is_file_in_current is_dir_in_current) |
|
494 thm has_same_inode_def |
|
495 done |
|
496 |
|
497 lemma co2sobj_closefd: |
|
498 "\<lbrakk>valid (CloseFd p fd # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (CloseFd p fd # s) obj = ( |
|
499 case obj of |
|
500 O_file f' \<Rightarrow> (case (file_of_proc_fd s p fd) of |
|
501 Some f \<Rightarrow> (if (f " |
436 |
502 |
437 lemma co2sobj_other: |
503 lemma co2sobj_other: |
438 "\<lbrakk>valid (e # s); alive (e # s) obj; |
504 "\<lbrakk>valid (e # s); alive (e # s) obj; |
439 \<forall> p f fds. e \<noteq> Execve p f fds; |
505 \<forall> p f fds. e \<noteq> Execve p f fds; |
440 \<forall> p p' fds shms. e \<noteq> Clone p p' fds shms; |
506 \<forall> p p' fds shms. e \<noteq> Clone p p' fds shms; |
441 \<forall> p p'. e \<noteq> Ptrace p p'; |
507 \<forall> p p'. e \<noteq> Ptrace p p'; |
442 \<forall> |
508 \<forall> |
443 \<rbrakk> \<Longrightarrow> co2sobj (e # s) obj = co2sobj s obj" |
509 \<rbrakk> \<Longrightarrow> co2sobj (e # s) obj = co2sobj s obj" |
444 |
510 |
445 lemmas co2sobj_simps = co2sobj_execve co2sobj_clone co2sobj_ptrace |
511 lemmas co2sobj_simps = co2sobj_execve co2sobj_clone co2sobj_ptrace co2sobj_open |
446 |
512 |
447 (* simpset for s2ss*) |
513 (* simpset for s2ss*) |
448 |
514 |
449 lemma s2ss_execve: |
515 lemma s2ss_execve: |
450 "valid (Execve p f fds # s) \<Longrightarrow> s2ss (Execve p f fds # s) = ( |
516 "valid (Execve p f fds # s) \<Longrightarrow> s2ss (Execve p f fds # s) = ( |