562 | _ \<Rightarrow> {} ) )" |
562 | _ \<Rightarrow> {} ) )" |
563 apply (case_tac opt) |
563 apply (case_tac opt) |
564 apply (simp add:s2ss_open_some s2ss_open_none)+ |
564 apply (simp add:s2ss_open_some s2ss_open_none)+ |
565 done |
565 done |
566 |
566 |
567 lemma |
567 lemma s2ss_readfile: |
|
568 "valid (ReadFile p fd # s) \<Longrightarrow> s2ss (ReadFile p fd # s) = ( |
|
569 case (file_of_proc_fd s p fd) of |
|
570 Some f \<Rightarrow> if (O_file f \<in> Tainted s) |
|
571 then update_s2ss_shm s p |
|
572 else s2ss s |
|
573 | _ \<Rightarrow> {})" |
|
574 apply (frule vt_grant_os, frule vd_cons, clarsimp split:option.splits) |
|
575 apply (rule conjI, rule impI, rule impI, simp) |
|
576 unfolding update_s2ss_shm_def s2ss_def |
|
577 apply (rule set_eqI, rule iffI) |
|
578 apply (drule CollectD, (erule exE|erule conjE)+) |
|
579 apply (erule co2sobj_some_caseD) |
|
580 apply (rule DiffI) |
|
581 apply (case_tac "O_proc pa \<in> Tainted s") |
|
582 apply (rule UnI1, simp, rule_tac x = "O_proc pa" in exI) |
|
583 apply (clarsimp simp:cp2sproc_other tainted_eq_Tainted co2sobj.simps split:option.splits) |
|
584 apply (case_tac "info_flow_shm s p pa") |
|
585 apply (rule UnI2, rule CollectI, simp only:co2sobj.simps split:option.splits) |
|
586 apply (drule current_proc_has_sp', simp, simp) |
|
587 apply (rule_tac x = ab in exI, rule_tac x = pa in exI) |
|
588 apply (clarsimp simp:cp2sproc_other tainted_eq_Tainted split:option.splits) |
|
589 apply (rule UnI1, simp) |
|
590 apply (rule_tac x = "O_proc pa" in exI) |
|
591 apply (clarsimp simp:cp2sproc_other tainted_eq_Tainted co2sobj.simps split:option.splits) |
|
592 apply (rule notI, clarsimp simp:cp2sproc_other tainted_eq_Tainted co2sobj.simps split:option.splits) |
|
593 apply (erule_tac x = pa in allE, simp) |
|
594 |
|
595 apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI) |
|
596 apply (simp add:alive_simps co2sobj_readfile, rule notI, clarsimp simp:co2sobj.simps) |
|
597 apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI) |
|
598 apply (simp add:alive_simps co2sobj_readfile, rule notI, clarsimp simp:co2sobj.simps split:option.splits) |
|
599 apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI) |
|
600 apply (simp add:alive_simps co2sobj_readfile, rule notI, clarsimp simp:co2sobj.simps split:option.splits) |
|
601 apply (rule DiffI, rule UnI1, rule CollectI, rule_tac x = obj in exI) |
|
602 apply (simp add:alive_simps co2sobj_readfile, rule notI, clarsimp simp:co2sobj.simps split:option.splits) |
|
603 |
|
604 apply (erule DiffE, drule s2ss_ptrace1_aux, erule UnE) |
|
605 apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI) |
|
606 apply (erule co2sobj_some_caseD) |
|
607 apply (case_tac "O_proc pa \<in> Tainted s") |
|
608 apply (rule_tac x = "O_proc pa" in exI) |
|
609 apply (clarsimp simp:tainted_eq_Tainted cp2sproc_other co2sobj.simps split:option.splits) |
|
610 apply (case_tac "info_flow_shm s p pa", simp only:co2sobj.simps split:option.splits) |
|
611 apply (drule current_proc_has_sp', simp, simp) |
|
612 apply (drule Meson.not_exD, erule_tac x = ab in allE, drule Meson.not_exD, erule_tac x = pa in allE) |
|
613 apply (simp add:tainted_eq_Tainted, (erule exE|erule conjE)+) |
|
614 apply (rule_tac x = "O_proc p'" in exI) |
|
615 apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted co2sobj.simps split:option.splits) |
|
616 apply (rule_tac x = "O_proc pa" in exI) |
|
617 apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted co2sobj.simps split:option.splits) |
|
618 |
|
619 apply (rule_tac x = obj in exI, |
|
620 auto split:option.splits simp:co2sobj_readfile alive_simps simp del:co2sobj.simps)[1] |
|
621 apply (rule_tac x = obj in exI, |
|
622 auto split:option.splits simp:co2sobj_readfile alive_simps simp del:co2sobj.simps)[1] |
|
623 apply (rule_tac x = obj in exI, |
|
624 auto split:option.splits simp:co2sobj_readfile alive_simps simp del:co2sobj.simps)[1] |
|
625 apply (rule_tac x = obj in exI, |
|
626 auto split:option.splits simp:co2sobj_readfile alive_simps simp del:co2sobj.simps)[1] |
|
627 |
|
628 apply (erule CollectE, (erule exE|erule conjE)+, rule CollectI) |
|
629 apply (rule_tac x = "O_proc pa" in exI) |
|
630 apply (clarsimp simp:Tainted_ptrace' cp2sproc_other tainted_eq_Tainted info_shm_flow_in_procs co2sobj.simps) |
|
631 |
|
632 |
|
633 apply (rule impI, rule impI) |
|
634 apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE, rule CollectI) |
|
635 apply (rule_tac x = obj in exI, simp add:alive_simps co2sobj_readfile split:t_object.splits) |
|
636 apply (erule CollectE, erule exE, erule conjE, rule CollectI) |
|
637 apply (rule_tac x = obj in exI, simp add:alive_simps) |
|
638 apply (drule_tac obj = obj in co2sobj_readfile, simp) |
|
639 apply (simp split:t_object.splits) |
|
640 apply (simp add:co2sobj.simps)+ |
|
641 done |
568 |
642 |
569 |
643 |
570 lemmas s2ss_simps = s2ss_execve s2ss_clone s2ss_ptrace s2ss_kill s2ss_exit s2ss_open |
644 lemmas s2ss_simps = s2ss_execve s2ss_clone s2ss_ptrace s2ss_kill s2ss_exit s2ss_open |
571 |
645 s2ss_readfile |
|
646 |