selinux: comparison Flask.thy

equal deleted inserted replaced

-:47a4b2ae0556
+:7b5e9fbeaf93
 | "procs_of_shm (CreateShM p h # \<tau>) =
 (procs_of_shm \<tau>) (h := {})"  (* creator may not be the sharer of the shm *)
 | "procs_of_shm (Attach p h flag # \<tau>) =
 (procs_of_shm \<tau>) (h := insert (p, flag) (procs_of_shm \<tau> h))"
 | "procs_of_shm (Detach p h # \<tau>) =
-(procs_of_shm \<tau>) (h := (procs_of_shm \<tau> h) - {(p,flag). \<exists> flag. (p, flag) \<in> procs_of_shm \<tau> h})"
+(procs_of_shm \<tau>) (h := (procs_of_shm \<tau> h) - {(p,flag) | flag. (p, flag) \<in> procs_of_shm \<tau> h})"
 | "procs_of_shm (DeleteShM p h # \<tau>) = (procs_of_shm \<tau>) (h := {})"
 | "procs_of_shm (Clone p p' fds shms # \<tau>) =
 (\<lambda> h. if (h \<in> shms)
-then (procs_of_shm \<tau> h) \<union> {(p', flag). \<exists> flag. (p, flag) \<in> procs_of_shm \<tau> h}
+then (procs_of_shm \<tau> h) \<union> {(p', flag) | flag. (p, flag) \<in> procs_of_shm \<tau> h}
 else procs_of_shm \<tau> h)"
 | "procs_of_shm (Execve p f fds # \<tau>) =
-(\<lambda> h. procs_of_shm \<tau> h - {(p, flag). \<exists> flag. (p, flag) \<in> procs_of_shm \<tau> h})"
+(\<lambda> h. procs_of_shm \<tau> h - {(p, flag) | flag. (p, flag) \<in> procs_of_shm \<tau> h})"
-| "procs_of_shm (e # \<tau>)          = procs_of_shm \<tau>"
+| "procs_of_shm (Kill p p' # s) =
+(\<lambda> h. (procs_of_shm s h) - {(p', flag) | flag. (p', flag) \<in> procs_of_shm s h})"
+| "procs_of_shm (Exit p # s) =
+(\<lambda> h. (procs_of_shm s h) - {(p, flag) | flag. (p, flag) \<in> procs_of_shm s h})"
+| "procs_of_shm (e # \<tau>) = procs_of_shm \<tau>"
 definition info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"
 where
 "info_flow_shm \<tau> from to \<equiv> (from = to) \<or> (\<exists> h \<in> current_shms \<tau>. \<exists> toflag.
 (((from, SHM_RDWR) \<in> procs_of_shm \<tau> h) \<and> ((to, toflag) \<in> procs_of_shm \<tau> h)))"
 where
 "proc_file_fds s p \<equiv> {fd. \<exists> f. file_of_proc_fd s p fd = Some f}"
 definition init_proc_file_fds:: "t_process \<Rightarrow> t_fd set"
+where
 "init_proc_file_fds p \<equiv> {fd. \<exists> f. init_file_of_proc_fd p fd = Some f}"
 end

changeset 13	7b5e9fbeaf93
parent 12	47a4b2ae0556
child 14	cc1e46225a81