638 where |
638 where |
639 "sproc_related p (pi, sec, fds, shms) = (pi = Init p)" |
639 "sproc_related p (pi, sec, fds, shms) = (pi = Init p)" |
640 *) |
640 *) |
641 fun init_obj_related :: "t_sobject \<Rightarrow> t_object \<Rightarrow> bool" |
641 fun init_obj_related :: "t_sobject \<Rightarrow> t_object \<Rightarrow> bool" |
642 where |
642 where |
643 "init_obj_related (S_proc (Init p, sec, fds, shms) tag) (O_proc p') = (p = p')" |
643 "init_obj_related (S_proc (pi, sec, fds, shms) tag) (O_proc p') = (pi = Init p')" |
644 | "init_obj_related (S_file sfs tag) (O_file f) = (\<exists> sf \<in> sfs. sfile_related sf f)" |
644 | "init_obj_related (S_file sfs tag) (O_file f) = (\<exists> sf \<in> sfs. sfile_related sf f)" |
645 | "init_obj_related (S_dir sf) (O_dir f) = (sfile_related sf f)" |
645 | "init_obj_related (S_dir sf) (O_dir f) = (sfile_related sf f)" |
646 | "init_obj_related (S_msgq (Init q, sec, sms)) (O_msgq q') = (q = q')" |
646 | "init_obj_related (S_msgq (qi, sec, sms)) (O_msgq q') = (qi = Init q')" |
647 | "init_obj_related (S_shm (Init h, sec)) (O_shm h') = (h = h')" |
647 | "init_obj_related (S_shm (hi, sec)) (O_shm h') = (hi = Init h')" |
648 | "init_obj_related (S_msg (Init q, sec, sms) (Init m, secm, tagm)) (O_msg q' m') = (q = q' \<and> m = m')" |
648 | "init_obj_related (S_msg (qi, sec, sms) (mi, secm, tagm)) (O_msg q' m') = (qi = Init q' \<and> mi = Init m')" |
649 | "init_obj_related _ _ = False" |
649 | "init_obj_related _ _ = False" |
650 |
650 |
651 fun tainted_s :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> bool" |
651 fun tainted_s :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> bool" |
652 where |
652 where |
653 "tainted_s ss (S_proc sp tag) = (S_proc sp tag \<in> ss \<and> tag = True)" |
653 "tainted_s ss (S_proc sp tag) = (S_proc sp tag \<in> ss \<and> tag = True)" |