Static.thy
changeset 56 ced9becf9eeb
parent 47 0960686df575
child 61 0d219ddd6354
equal deleted inserted replaced
55:6f3ac2861978 56:ced9becf9eeb
   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