1014 where |
1014 where |
1015 "sectxt_of_obj s obj = ( |
1015 "sectxt_of_obj s obj = ( |
1016 case (user_of_obj s obj, role_of_obj s obj, type_of_obj s obj) of |
1016 case (user_of_obj s obj, role_of_obj s obj, type_of_obj s obj) of |
1017 (Some u, Some r, Some t) \<Rightarrow> Some (u, r, t) |
1017 (Some u, Some r, Some t) \<Rightarrow> Some (u, r, t) |
1018 | _ \<Rightarrow> None)" |
1018 | _ \<Rightarrow> None)" |
|
1019 |
|
1020 fun init_role_of_obj :: "t_object \<Rightarrow> role_t option" |
|
1021 where |
|
1022 "init_role_of_obj (O_proc p) = init_role_of_proc p" |
|
1023 | "init_role_of_obj _ = Some R_object" |
|
1024 |
|
1025 definition init_sectxt_of_obj :: "t_object \<Rightarrow> security_context_t option" |
|
1026 where |
|
1027 "init_sectxt_of_obj obj \<equiv> |
|
1028 (case (init_user_of_obj obj, init_role_of_obj obj, init_type_of_obj obj) of |
|
1029 (Some u, Some r, Some t) \<Rightarrow> Some (u,r,t) |
|
1030 | _ \<Rightarrow> None)" |
|
1031 |
|
1032 definition sec_of_root :: "security_context_t" |
|
1033 where |
|
1034 "sec_of_root \<equiv> (case (init_user_of_obj (O_dir []), init_type_of_obj (O_dir [])) of |
|
1035 (Some u, Some t) \<Rightarrow> (u, R_object, t))" |
1019 |
1036 |
1020 (******* flask granting ******** |
1037 (******* flask granting ******** |
1021 * involves three kinds of rules: |
1038 * involves three kinds of rules: |
1022 * 1. allow rule of types, allowed_rule_list_t, main |
1039 * 1. allow rule of types, allowed_rule_list_t, main |
1023 * 2. allow rule of roles, role_allow_rule_list_t, mainly for execve call |
1040 * 2. allow rule of roles, role_allow_rule_list_t, mainly for execve call |