selinux: comparison no_shm_selinux/Static.thy

equal deleted inserted replaced

-:690636b7b6f1
+:8d18cfc845dd
 (* acient files of init-file
 definition init_o2s_afs :: "t_file \<Rightarrow> security_context_t set"
 where
 "init_o2s_afs f \<equiv> {sec. \<exists> f'. f' \<preceq> f \<and> init_sectxt_of_obj (O_dir f') = Some sec}" *)
+(*
 definition init_cm2smsg :: "t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsg option"
 where
 "init_cm2smsg q m \<equiv> (case (init_sectxt_of_obj (O_msg q m)) of
 Some sec \<Rightarrow> Some (Init m, sec, (O_msg q m) \<in> seeds)
 | _ \<Rightarrow> None)"
 definition init_cq2smsgq :: "t_msgq \<Rightarrow> t_smsgq option"
 where
 "init_cq2smsgq q \<equiv> (case (init_sectxt_of_obj (O_msgq q), init_cqm2sms q (init_msgs_of_queue q)) of
 (Some sec, Some sms) \<Rightarrow> Some (Init q, sec, sms)
 | _ \<Rightarrow> None)"
+*)
 fun init_obj2sobj :: "t_object \<Rightarrow> t_sobject option"
 where
 "init_obj2sobj (O_proc p) =
 (case (init_cp2sproc p) of
 (\<exists> f'. f' \<in> (init_same_inode_files f) \<and> O_file f \<in> seeds))"
 | "init_obj2sobj (O_dir f) =
 (case (init_cf2sfile f) of
 Some sf \<Rightarrow> Some (S_dir sf)
 | _ \<Rightarrow> None)"
-| "init_obj2sobj (O_msgq q) =
+| "init_obj2sobj (O_msgq q) = None"
+(*
 (case (init_cq2smsgq q) of
 Some sq \<Rightarrow> Some (S_msgq sq)
 | _ \<Rightarrow> None)"
-(*
 | "init_obj2sobj (O_shm h) =
 (case (init_ch2sshm h) of
 Some sh \<Rightarrow> Some (S_shm sh)
 | _       \<Rightarrow> None)"
 | "init_obj2sobj (O_msg q m) =
 Some sec \<Rightarrow>
 Some (if (\<not> died (O_proc p) s \<and> p \<in> init_procs) then Init p else Created, sec,
 cpfd2sfds s p)
 | _ \<Rightarrow> None)"
+(*
 definition cm2smsg :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsg option"
 where
 "cm2smsg s q m \<equiv> (case (sectxt_of_obj s (O_msg q m)) of
 Some sec \<Rightarrow>
 Some (if (\<not> died (O_msg q m) s \<and> m \<in> set (init_msgs_of_queue q)) then Init m else Created,
 sec, O_msg q m \<in> tainted s)
+| _ \<Rightarrow> None)"
+*)
+definition cm2smsg :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsg option"
+where
+"cm2smsg s q m \<equiv> (case (sectxt_of_obj s (O_msg q m)) of
+Some sec \<Rightarrow> Some (Created, sec, O_msg q m \<in> tainted s)
 | _ \<Rightarrow> None)"
 fun cqm2sms:: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg list \<Rightarrow> (t_smsg list) option"
 where
 "cqm2sms s q [] = Some []"
 | "cqm2sms s q (m#ms) =
 (case (cqm2sms s q ms, cm2smsg s q m) of
 (Some sms, Some sm) \<Rightarrow> Some (sm#sms)
 | _ \<Rightarrow> None)"
+(*
 definition cq2smsgq :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_smsgq option"
 where
 "cq2smsgq s q \<equiv> (case (sectxt_of_obj s (O_msgq q), cqm2sms s q (msgs_of_queue s q)) of
 (Some sec, Some sms) \<Rightarrow>
 Some (if (\<not> died (O_msgq q) s \<and> q \<in> init_msgqs) then Init q else Created,
 sec, sms)
+| _ \<Rightarrow> None)"
+*)
+definition cq2smsgq :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_smsgq option"
+where
+"cq2smsgq s q \<equiv> (case (sectxt_of_obj s (O_msgq q), cqm2sms s q (msgs_of_queue s q)) of
+(Some sec, Some sms) \<Rightarrow> Some (Created, sec, sms)
 | _ \<Rightarrow> None)"
 fun co2sobj :: "t_state \<Rightarrow> t_object \<Rightarrow> t_sobject option"
 where
 "co2sobj s (O_proc p) =
 fun is_many_sproc :: "t_sproc \<Rightarrow> bool"
 where
 "is_many_sproc (Created, sec,fds) = True"
 | "is_many_sproc _                       = False"
+(*
 fun is_many_smsg :: "t_smsg \<Rightarrow> bool"
 where
 "is_many_smsg (Created,sec,tag) = True"
 | "is_many_smsg _                 = False"
+*)
 (* wrong def
 fun is_many_smsgq :: "t_smsgq \<Rightarrow> bool"
 where
 "is_many_smsgq (Created,sec,sms) = (True \<and> (\<forall> sm \<in> (set sms). is_many_smsg sm))"
 | "is_many_smsgq _                 = False"
 *)
+(*
 fun is_many_smsgq :: "t_smsgq \<Rightarrow> bool"
 where
 "is_many_smsgq (Created,sec,sms) = True"
 | "is_many_smsgq _                 = False"
+*)
 (*
 fun is_many_sshm :: "t_sshm \<Rightarrow> bool"
 where
 "is_many_sshm (Created, sec) = True"
 | "is_many_sshm _              = False"
 fun is_many :: "t_sobject \<Rightarrow> bool"
 where
 "is_many (S_proc sp   tag) = is_many_sproc sp"
 | "is_many (S_file sfs  tag) = (\<forall> sf \<in> sfs. is_many_sfile sf)"
 | "is_many (S_dir  sf      ) = is_many_sfile sf"
-| "is_many (S_msgq sq      ) = is_many_smsgq sq"
+| "is_many (S_msgq sq      ) = True"
 (*
 | "is_many (S_shm  sh      ) = is_many_sshm  sh"
 *)
+(*
 fun is_init_smsgq :: "t_smsgq \<Rightarrow> bool"
 where
 "is_init_smsgq (Init q,sec,sms) = True"
 | "is_init_smsgq _                = False"
+*)
 (*
 fun is_init_sshm :: "t_sshm \<Rightarrow> bool"
 where
 "is_init_sshm (Init h,sec) = True"
 | "is_init_sshm _            = False"
 fun is_init_sobj :: "t_sobject \<Rightarrow> bool"
 where
 "is_init_sobj (S_proc sp tag ) = is_init_sproc sp"
 | "is_init_sobj (S_file sfs tag) = (\<exists> sf \<in> sfs. is_init_sfile sf)"
 | "is_init_sobj (S_dir  sf     ) = is_init_sfile sf"
-| "is_init_sobj (S_msgq sq     ) = is_init_smsgq sq"
+| "is_init_sobj (S_msgq sq     ) = False"
 (*
 | "is_init_sobj (S_shm  sh     ) = is_init_sshm sh"
 *)
 (*
 fun update_ss_sp:: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state"

changeset 87	8d18cfc845dd
parent 85	1d1aa5bdd37d
child 92	d9dc04c3ea90