547 |
547 |
548 definition search_check_s :: "security_context_t \<Rightarrow> t_sfile \<Rightarrow> bool \<Rightarrow> bool" |
548 definition search_check_s :: "security_context_t \<Rightarrow> t_sfile \<Rightarrow> bool \<Rightarrow> bool" |
549 where |
549 where |
550 "search_check_s pctxt sf if_file = |
550 "search_check_s pctxt sf if_file = |
551 (if if_file |
551 (if if_file |
552 then search_check_file pctxt (sectxt_of_sfile sf) \<and> search_check_allp pctxt (asecs_of_sfile sf) |
552 then search_check_ctxt pctxt (sectxt_of_sfile sf) (asecs_of_sfile sf) True |
553 else search_check_dir pctxt (sectxt_of_sfile sf) \<and> search_check_allp pctxt (asecs_of_sfile sf))" |
553 else search_check_ctxt pctxt (sectxt_of_sfile sf) (asecs_of_sfile sf) False)" |
554 |
554 |
555 definition sectxts_of_sfds :: "t_sfd set \<Rightarrow> security_context_t set" |
555 definition sectxts_of_sfds :: "t_sfd set \<Rightarrow> security_context_t set" |
556 where |
556 where |
557 "sectxts_of_sfds sfds \<equiv> {ctxt. \<exists> flag sf. (ctxt, flag, sf) \<in> sfds}" |
557 "sectxts_of_sfds sfds \<equiv> {ctxt. \<exists> flag sf. (ctxt, flag, sf) \<in> sfds}" |
558 |
558 |
559 definition inherit_fds_check_s :: "security_context_t \<Rightarrow> t_sfd set \<Rightarrow> bool" |
559 definition inherit_fds_check_s :: "security_context_t \<Rightarrow> t_sfd set \<Rightarrow> bool" |
560 where |
560 where |
561 "inherit_fds_check_s pctxt sfds \<equiv> |
561 "inherit_fds_check_s pctxt sfds \<equiv> inherit_fds_check_ctxt pctxt (sectxts_of_sfds sfds)" |
562 (\<forall> ctxt \<in> sectxts_of_sfds sfds. permission_check pctxt ctxt C_fd P_inherit)" |
|
563 |
562 |
564 definition sectxts_of_sproc_sshms :: "t_sproc_sshm set \<Rightarrow> security_context_t set" |
563 definition sectxts_of_sproc_sshms :: "t_sproc_sshm set \<Rightarrow> security_context_t set" |
565 where |
564 where |
566 "sectxts_of_sproc_sshms sshms \<equiv> {ctxt. \<exists> hi flag. ((hi, ctxt),flag) \<in> sshms}" |
565 "sectxts_of_sproc_sshms sshms \<equiv> {ctxt. \<exists> hi flag. ((hi, ctxt),flag) \<in> sshms}" |
567 |
566 |
568 definition inherit_shms_check_s :: "security_context_t \<Rightarrow> t_sproc_sshm set \<Rightarrow> bool" |
567 definition inherit_shms_check_s :: "security_context_t \<Rightarrow> t_sproc_sshm set \<Rightarrow> bool" |
569 where |
568 where |
570 "inherit_shms_check_s pctxt sshms \<equiv> |
569 "inherit_shms_check_s pctxt sshms \<equiv> inherit_shms_check_ctxt pctxt (sectxts_of_sproc_sshms sshms)" |
571 (\<forall> ctxt \<in> sectxts_of_sproc_sshms sshms. permission_check pctxt ctxt C_shm P_inherit)" |
|
572 |
570 |
573 (* |
571 (* |
574 fun info_flow_sshm :: "t_sproc \<Rightarrow> t_sproc \<Rightarrow> bool" |
572 fun info_flow_sshm :: "t_sproc \<Rightarrow> t_sproc \<Rightarrow> bool" |
575 where |
573 where |
576 "info_flow_sshm (pi,sec,fds,shms) (pi',sec',fds',shms') = |
574 "info_flow_sshm (pi,sec,fds,shms) (pi',sec',fds',shms') = |