selinux: comparison no_shm_selinux/Flask.thy

equal deleted inserted replaced

-:690636b7b6f1
+:8d18cfc845dd
 (*
 and init_file_at_writing_by:: "t_file \<Rightarrow> (t_process \<times> t_fd) set"
 *)
 and init_socket_state ::      "t_socket \<rightharpoonup> t_sock_state"
+(*
 and init_msgqs :: "t_msgq set"
 and init_msgs_of_queue:: "t_msgq \<Rightarrow> t_msg list"
+*)
+and max_queue :: "nat"
 (*
 and init_shms :: "t_shm set"
 and init_procs_of_shm :: "t_shm \<Rightarrow> (t_process \<times> t_shm_attach_flag) set"
 and init_flag_of_proc_shm :: "t_process \<Rightarrow> t_shm \<rightharpoonup> t_shm_attach_flag"
 *)
 (*
 and init_procs_has_shm:      "\<And> p h flag. (p,flag) \<in> init_procs_of_shm h \<Longrightarrow> p \<in> init_procs \<and> h \<in> init_shms \<and> init_flag_of_proc_shm p h = Some flag"
 and init_shmflag_has_proc:   "\<And> p h flag. init_flag_of_proc_shm p h = Some flag \<Longrightarrow> (p, flag) \<in> init_procs_of_shm h"
 *)
+(*
 and init_msgs_distinct:      "\<And> q. distinct (init_msgs_of_queue q)"
 and init_msgs_valid:         "\<And> m q. m \<in> set (init_msgs_of_queue q) \<Longrightarrow> q \<in> init_msgqs"
+and init_msgq_valid:         "\<And> q. length (init_msgs_of_queue q) \<le> max_queue"
+*)
 and init_socket_has_inode:   "\<And> p fd. (p, fd) \<in> init_sockets \<Longrightarrow> \<exists> im. init_inum_of_socket (p, fd) = Some im \<and> p \<in> init_procs \<and> fd \<in> init_fds_of_proc p \<and> init_file_of_proc_fd p fd = None"
 and inos_has_sock_tag:  "\<And> s im. init_inum_of_socket s = Some im \<Longrightarrow> s \<in> init_sockets \<and> (\<exists> tag. init_itag_of_inum im = Some tag \<and> is_sock_itag tag)"
 (*
 and init_netobj_has_state:   "bidirect_in_init init_netobjs init_netobj_state"
 and init_netobj_has_socktype:"bidirect_in_init init_netobjs init_netobj_socktype"
 and init_netobj_has_laddr:   "\<And> s. after_bind (init_netobj_state s) \<Longrightarrow> init_netobj_localaddr s \<noteq> None"
 and init_netobj_has_raddr:   "\<And> s. after_conacc (init_netobj_state s) \<Longrightarrow> init_netobj_remoteaddr s \<noteq> None"
 *)
-and init_finite_sets:   "finite init_files \<and> finite init_procs \<and> (\<forall> p. finite (init_fds_of_proc p)) \<and> finite init_shms \<and> finite init_msgqs \<and> finite init_users"
+and init_finite_sets:   "finite init_files \<and> finite init_procs \<and> (\<forall> p. finite (init_fds_of_proc p)) \<and> finite init_shms \<and> finite init_users"  (* finite init_msgqs *)
 begin
 definition is_init_file:: "t_file \<Rightarrow> bool"
 where
 | "init_alive (O_tcp_sock k) = (is_init_tcp_sock k)"
 | "init_alive (O_udp_sock k) = (is_init_udp_sock k)"
 (*
 | "init_alive (O_shm  h)     = (h \<in> init_shms)"
 *)
-| "init_alive (O_msgq q)     = (q \<in> init_msgqs)"
+| "init_alive (O_msgq q)     = False" (* (q \<in> init_msgqs) *)
-| "init_alive (O_msg q m)    = (m \<in> set (init_msgs_of_queue q) \<and> q \<in> init_msgqs)"
+| "init_alive (O_msg q m)    = False" (* (m \<in> set (init_msgs_of_queue q) \<and> q \<in> init_msgqs)" *)
 (************ system listeners, event-related ***********)
 fun file_of_proc_fd ::  "t_state \<Rightarrow> t_process \<Rightarrow> t_fd \<Rightarrow> t_file option"
 "info_flow_shm s from to \<equiv> (self_shm s from to) \<or> (\<exists> h. one_flow_shm s h from to)"
 *)
 fun current_msgqs :: "t_state \<Rightarrow> t_msgq set"
 where
-"current_msgqs [] = init_msgqs"
+"current_msgqs [] = {}" (* init_msgqs *)
 | "current_msgqs (CreateMsgq p q # \<tau>) = insert q (current_msgqs \<tau>)"
 | "current_msgqs (RemoveMsgq p q # \<tau>) = (current_msgqs \<tau>) - {q}"
 | "current_msgqs (_ # \<tau>) = current_msgqs \<tau>"
 fun msgs_of_queue :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg list"
 where
-"msgs_of_queue [] = init_msgs_of_queue"
+"msgs_of_queue [] = (\<lambda> x. [])" (* init_msgs_of_queue*)
 | "msgs_of_queue (CreateMsgq p q # \<tau>) = (msgs_of_queue \<tau>)(q := [])"
 | "msgs_of_queue (SendMsg p q m  # \<tau>) = (msgs_of_queue \<tau>)(q := msgs_of_queue \<tau> q @ [m])"
 | "msgs_of_queue (RecvMsg p q m  # \<tau>) = (msgs_of_queue \<tau>)(q := tl (msgs_of_queue \<tau> q))"
 | "msgs_of_queue (RemoveMsgq p q # \<tau>) = (msgs_of_queue \<tau>)(q := [])"
 | "msgs_of_queue (_ # \<tau>) = msgs_of_queue \<tau>"
 pf\<^isub>3 \<notin> files_hung_by_del \<tau>) )"
 *)
 | "os_grant \<tau> (CreateMsgq p q)                =
 (p \<in> current_procs \<tau> \<and> q \<notin> (current_msgqs \<tau>))"
 | "os_grant \<tau> (SendMsg p q m)                 =
-(p \<in> current_procs \<tau> \<and> q \<in> current_msgqs \<tau> \<and> m \<notin> (set (msgs_of_queue \<tau> q)))"
+(p \<in> current_procs \<tau> \<and> q \<in> current_msgqs \<tau> \<and> m \<notin> (set (msgs_of_queue \<tau> q)) \<and>
+length (msgs_of_queue \<tau> q) < max_queue)"
 | "os_grant \<tau> (RecvMsg p q m)                 =
 (p \<in> current_procs \<tau> \<and> q \<in> current_msgqs \<tau> \<and> m = hd (msgs_of_queue \<tau> q) \<and> msgs_of_queue \<tau> q \<noteq> [])"
 | "os_grant \<tau> (RemoveMsgq p q)                =
 (p \<in> current_procs \<tau> \<and> q \<in> current_msgqs \<tau>)"
 (*
 inductive valid :: "t_state \<Rightarrow> bool"
 where
 "valid []"
 | "\<lbrakk>valid s; os_grant s e; grant s e\<rbrakk> \<Longrightarrow> valid (e # s)"
-(* tobj: object that can be tainted *)
+(* tobj: object that can be tainted
 fun tobj_in_init :: "t_object \<Rightarrow> bool"
 where
 "tobj_in_init (O_proc p) = (p \<in> init_procs)"
 | "tobj_in_init (O_file f) = (is_init_file f)"
 (* directory is not taintable
 | "tobj_in_init (O_node n) = (n \<in> init_nodes)"
 | "tobj_in_init (O_msg q m) = (m \<in> set (init_msgs_of_queue q) \<and> q \<in> init_msgqs)"
 *)
 | "tobj_in_init _ = False" (* other kind of obj cannot be tainted *)
+*)
 (* no use
 fun no_del_event:: "t_event list \<Rightarrow> bool"
 where
 "no_del_event [] = True"

changeset 87	8d18cfc845dd
parent 83	e79e3a8a4ceb