480 else (sobj = S_proc sp (tagp \<or> tag)) |
480 else (sobj = S_proc sp (tagp \<or> tag)) |
481 else (sobj = S_proc sp tag) |
481 else (sobj = S_proc sp tag) |
482 | _ \<Rightarrow> sobj = sobj')}" |
482 | _ \<Rightarrow> sobj = sobj')}" |
483 |
483 |
484 |
484 |
485 (* no del |
485 |
486 (* all reachable static states(sobjects set) *) |
486 (* all reachable static states(sobjects set) *) |
487 inductive_set static :: "t_static_state set" |
487 inductive_set static :: "t_static_state set" |
488 where |
488 where |
489 s_init: "init_static_state \<in> static" |
489 s_init: "init_static_state \<in> static" |
490 | s_execve: "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; S_file sfs tagf \<in> ss; |
490 | s_execve: "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; S_file sfs tagf \<in> ss; |
648 "init_obj_related (S_proc (pi, sec, fds, shms) tag) (O_proc p') = (pi = Init p')" |
648 "init_obj_related (S_proc (pi, sec, fds, shms) tag) (O_proc p') = (pi = Init p')" |
649 | "init_obj_related (S_file sfs tag) (O_file f) = (\<exists> sf \<in> sfs. sfile_related sf f)" |
649 | "init_obj_related (S_file sfs tag) (O_file f) = (\<exists> sf \<in> sfs. sfile_related sf f)" |
650 | "init_obj_related (S_dir sf) (O_dir f) = (sfile_related sf f)" |
650 | "init_obj_related (S_dir sf) (O_dir f) = (sfile_related sf f)" |
651 | "init_obj_related (S_msgq (qi, sec, sms)) (O_msgq q') = (qi = Init q')" |
651 | "init_obj_related (S_msgq (qi, sec, sms)) (O_msgq q') = (qi = Init q')" |
652 | "init_obj_related (S_shm (hi, sec)) (O_shm h') = (hi = Init h')" |
652 | "init_obj_related (S_shm (hi, sec)) (O_shm h') = (hi = Init h')" |
|
653 (* |
653 | "init_obj_related (S_msg (qi, sec, sms) (mi, secm, tagm)) (O_msg q' m') = (qi = Init q' \<and> mi = Init m')" |
654 | "init_obj_related (S_msg (qi, sec, sms) (mi, secm, tagm)) (O_msg q' m') = (qi = Init q' \<and> mi = Init m')" |
|
655 *) |
654 | "init_obj_related _ _ = False" |
656 | "init_obj_related _ _ = False" |
655 |
657 |
656 fun tainted_s :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> bool" |
658 fun tainted_s :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> bool" |
657 where |
659 where |
658 "tainted_s ss (S_proc sp tag) = (S_proc sp tag \<in> ss \<and> tag = True)" |
660 "tainted_s ss (S_proc sp tag) = (S_proc sp tag \<in> ss \<and> tag = True)" |
659 | "tainted_s ss (S_file sfs tag) = (S_file sfs tag \<in> ss \<and> tag = True)" |
661 | "tainted_s ss (S_file sfs tag) = (S_file sfs tag \<in> ss \<and> tag = True)" |
|
662 (* |
660 | "tainted_s ss (S_msg (qi, sec, sms) (mi, secm, tag)) = |
663 | "tainted_s ss (S_msg (qi, sec, sms) (mi, secm, tag)) = |
661 (S_msgq (qi, sec, sms) \<in> ss \<and> (mi,secm,tag) \<in> set sms \<and> tag = True)" |
664 (S_msgq (qi, sec, sms) \<in> ss \<and> (mi,secm,tag) \<in> set sms \<and> tag = True)" |
|
665 *) |
662 | "tainted_s ss _ = False" |
666 | "tainted_s ss _ = False" |
663 |
667 |
664 (* |
668 (* |
665 fun tainted_s :: "t_object \<Rightarrow> t_static_state \<Rightarrow> bool" |
669 fun tainted_s :: "t_object \<Rightarrow> t_static_state \<Rightarrow> bool" |
666 where |
670 where |