selinux: comparison Flask.thy

equal deleted inserted replaced

-:0753309adfc7
+:6f9a588bcfc4
 definition current_files :: "t_state \<Rightarrow> t_file set"
 where
 "current_files \<tau> = {f. \<exists> i. inum_of_file \<tau> f = Some i}"
+(* experimentary: for the delete obj's (file or socket) inode num, it is unnecessary for itag_of_inum to be NONE, cause this is the situation blocked by inum_of_file / inum_of_socket !!! *)
+(* delete a file, just recycle its inode num, but not destroy its inode \<dots>, so it is irrelative to these events, like closeFd, Rmdir, UnLink \<dots>*)
+fun itag_of_inum :: "t_state \<Rightarrow> (t_inode_num \<rightharpoonup> t_inode_tag)"
+where
+"itag_of_inum [] = init_itag_of_inum"
+| "itag_of_inum (Open p f flags fd (Some ino) # \<tau>) = (itag_of_inum \<tau>) (ino := Some Tag_FILE)"
+| "itag_of_inum (Mkdir p f ino # \<tau>) = (itag_of_inum \<tau>) (ino := Some Tag_DIR)"
+| "itag_of_inum (CreateSock p af st fd ino # \<tau>) =
+(case st of
+STREAM \<Rightarrow> (itag_of_inum \<tau>) (ino := Some Tag_TCP_SOCK)
+| DGRAM  \<Rightarrow> (itag_of_inum \<tau>) (ino := Some Tag_UDP_SOCK) )"
+| "itag_of_inum (Accept p fd addr lport' fd' ino # \<tau>) =
+(itag_of_inum \<tau>) (ino := Some Tag_TCP_SOCK)"
+| "itag_of_inum (_ # \<tau>) = itag_of_inum \<tau>"
+definition is_file:: "t_state \<Rightarrow> t_file \<Rightarrow> bool"
+where
+"is_file \<tau> f \<equiv> (case (inum_of_file \<tau> f) of
+Some i \<Rightarrow> (case (itag_of_inum \<tau> i) of
+Some Tag_FILE \<Rightarrow> True
+| _             \<Rightarrow> False)
+| _      \<Rightarrow> False)"
+definition is_dir:: "t_state \<Rightarrow> t_file \<Rightarrow> bool"
+where
+"is_dir \<tau> f \<equiv> (case (inum_of_file \<tau> f) of
+Some i \<Rightarrow> (case (itag_of_inum \<tau> i) of
+Some Tag_DIR \<Rightarrow> True
+| _            \<Rightarrow> False)
+| _      \<Rightarrow> False)"
+definition dir_is_empty :: "t_state \<Rightarrow> t_file \<Rightarrow> bool"
+where
+"dir_is_empty \<tau> f \<equiv> is_dir \<tau> f \<and> \<not> (\<exists> f'. f' \<in> current_files \<tau> \<and> f \<prec> f')"
+definition same_inode_files :: "t_state \<Rightarrow> t_file \<Rightarrow> t_file set"
+where
+"same_inode_files s f \<equiv> if is_file s f then {f'. inum_of_file s f = inum_of_file s f'} else {}"
 definition has_same_inode :: "t_state \<Rightarrow> t_file \<Rightarrow> t_file \<Rightarrow> bool"
 where
-"has_same_inode \<tau> fa fb =
+"has_same_inode s fa fb \<equiv> fb \<in> same_inode_files s fa"
-(\<exists>i. inum_of_file \<tau> fa = Some i \<and> inum_of_file \<tau> fb = Some i)"
 fun inum_of_socket :: "t_state \<Rightarrow> (t_socket \<rightharpoonup> t_inode_num)"
 where
 "inum_of_socket [] = init_inum_of_socket"
 | "inum_of_socket (CloseFd p fd # \<tau>) =
 definition current_sockets :: "t_state \<Rightarrow> t_socket set"
 where
 "current_sockets \<tau> = {s. \<exists> i. inum_of_socket \<tau> s = Some i}"
-(* experimentary: for the delete obj's (file or socket) inode num, it is unnecessary for itag_of_inum to be NONE, cause this is the situation blocked by inum_of_file / inum_of_socket !!! *)
-(* delete a file, just recycle its inode num, but not destroy its inode \<dots>, so it is irrelative to these events, like closeFd, Rmdir, UnLink \<dots>*)
-fun itag_of_inum :: "t_state \<Rightarrow> (t_inode_num \<rightharpoonup> t_inode_tag)"
-where
-"itag_of_inum [] = init_itag_of_inum"
-| "itag_of_inum (Open p f flags fd (Some ino) # \<tau>) = (itag_of_inum \<tau>) (ino := Some Tag_FILE)"
-| "itag_of_inum (Mkdir p f ino # \<tau>) = (itag_of_inum \<tau>) (ino := Some Tag_DIR)"
-| "itag_of_inum (CreateSock p af st fd ino # \<tau>) =
-(case st of
-STREAM \<Rightarrow> (itag_of_inum \<tau>) (ino := Some Tag_TCP_SOCK)
-| DGRAM  \<Rightarrow> (itag_of_inum \<tau>) (ino := Some Tag_UDP_SOCK) )"
-| "itag_of_inum (Accept p fd addr lport' fd' ino # \<tau>) =
-(itag_of_inum \<tau>) (ino := Some Tag_TCP_SOCK)"
-| "itag_of_inum (_ # \<tau>) = itag_of_inum \<tau>"
-definition is_file:: "t_state \<Rightarrow> t_file \<Rightarrow> bool"
-where
-"is_file \<tau> f \<equiv> (case (inum_of_file \<tau> f) of
-Some i \<Rightarrow> (case (itag_of_inum \<tau> i) of
-Some Tag_FILE \<Rightarrow> True
-| _             \<Rightarrow> False)
-| _      \<Rightarrow> False)"
-definition is_dir:: "t_state \<Rightarrow> t_file \<Rightarrow> bool"
-where
-"is_dir \<tau> f \<equiv> (case (inum_of_file \<tau> f) of
-Some i \<Rightarrow> (case (itag_of_inum \<tau> i) of
-Some Tag_DIR \<Rightarrow> True
-| _            \<Rightarrow> False)
-| _      \<Rightarrow> False)"
-definition dir_is_empty :: "t_state \<Rightarrow> t_file \<Rightarrow> bool"
-where
-"dir_is_empty \<tau> f \<equiv> is_dir \<tau> f \<and> \<not> (\<exists> f'. f' \<in> current_files \<tau> \<and> f \<prec> f')"
 definition is_tcp_sock :: "t_state \<Rightarrow> t_socket \<Rightarrow> bool"
 where
 "is_tcp_sock \<tau> s \<equiv> (case (inum_of_socket \<tau> s) of
 Some i \<Rightarrow> (case (itag_of_inum \<tau> i) of
 Some Tag_TCP_SOCK \<Rightarrow> True
 "current_sock_inums \<tau> = {im. \<exists> s. inum_of_socket \<tau> s = Some im}"
 definition current_inode_nums :: "t_state \<Rightarrow> nat set"
 where
 "current_inode_nums \<tau> = current_file_inums \<tau> \<union> current_sock_inums \<tau>"
-definition same_inode_files :: "t_state \<Rightarrow> t_file \<Rightarrow> t_file set"
-where
-"same_inode_files s f \<equiv> if is_file s f then {f'. inum_of_file s f = inum_of_file s f'} else {}"
 fun flags_of_proc_fd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd \<Rightarrow> t_open_flags option"
 where
 "flags_of_proc_fd [] p fd = init_oflags_of_proc_fd p fd"
 | "flags_of_proc_fd (Open p f flags fd iopt # \<tau>) p' fd' =

changeset 65	6f9a588bcfc4
parent 61	0d219ddd6354
child 67	811e3028d169