3 begin |
3 begin |
4 |
4 |
5 locale tainting_s = tainting |
5 locale tainting_s = tainting |
6 |
6 |
7 begin |
7 begin |
8 |
|
9 fun init_role_of_obj :: "t_object \<Rightarrow> role_t option" |
|
10 where |
|
11 "init_role_of_obj (O_proc p) = init_role_of_proc p" |
|
12 | "init_role_of_obj _ = Some R_object" |
|
13 |
|
14 definition init_sectxt_of_obj :: "t_object \<Rightarrow> security_context_t option" |
|
15 where |
|
16 "init_sectxt_of_obj obj \<equiv> |
|
17 (case (init_user_of_obj obj, init_role_of_obj obj, init_type_of_obj obj) of |
|
18 (Some u, Some r, Some t) \<Rightarrow> Some (u,r,t) |
|
19 | _ \<Rightarrow> None)" |
|
20 |
8 |
21 (* |
9 (* |
22 definition init_sectxt_of_file:: "t_file \<Rightarrow> security_context_t option" |
10 definition init_sectxt_of_file:: "t_file \<Rightarrow> security_context_t option" |
23 where |
11 where |
24 "init_sectxt_of_file f \<equiv> |
12 "init_sectxt_of_file f \<equiv> |
25 if (is_init_file f) then init_sectxt_of_obj (O_file f) |
13 if (is_init_file f) then init_sectxt_of_obj (O_file f) |
26 else if (is_init_dir f) then init_sectxt_of_obj (O_dir f) |
14 else if (is_init_dir f) then init_sectxt_of_obj (O_dir f) |
27 else None" |
15 else None" |
28 *) |
16 *) |
29 |
|
30 definition sec_of_root :: "security_context_t" |
|
31 where |
|
32 "sec_of_root \<equiv> (case (init_user_of_obj (O_dir []), init_type_of_obj (O_dir [])) of |
|
33 (Some u, Some t) \<Rightarrow> (u, R_object, t))" |
|
34 |
17 |
35 definition sroot :: "t_sfile" |
18 definition sroot :: "t_sfile" |
36 where |
19 where |
37 "sroot \<equiv> (Init [], sec_of_root, None, {})" |
20 "sroot \<equiv> (Init [], sec_of_root, None, {})" |
38 |
21 |