Flask.thy
changeset 7 f27882976251
parent 6 8779d321cc2e
child 8 289a30c4cfb7
--- a/Flask.thy	Wed May 15 11:21:39 2013 +0800
+++ b/Flask.thy	Wed May 15 15:42:46 2013 +0800
@@ -1017,6 +1017,23 @@
        (Some u, Some r, Some t) \<Rightarrow> Some (u, r, t)
      | _                        \<Rightarrow> None)"
 
+fun init_role_of_obj :: "t_object \<Rightarrow> role_t option"
+where
+  "init_role_of_obj (O_proc p) = init_role_of_proc p"
+| "init_role_of_obj _          = Some R_object"
+
+definition init_sectxt_of_obj :: "t_object \<Rightarrow> security_context_t option"
+where
+  "init_sectxt_of_obj obj \<equiv>
+     (case (init_user_of_obj obj, init_role_of_obj obj, init_type_of_obj obj) of
+        (Some u, Some r, Some t) \<Rightarrow> Some (u,r,t)
+      | _ \<Rightarrow> None)"
+
+definition sec_of_root :: "security_context_t"
+where
+  "sec_of_root \<equiv> (case (init_user_of_obj (O_dir []), init_type_of_obj (O_dir [])) of
+     (Some u, Some t) \<Rightarrow> (u, R_object, t))"
+
 (******* flask granting ********
  * involves three kinds of rules:
  *  1. allow rule of types, allowed_rule_list_t, main