selinux: comparison Flask.thy

equal deleted inserted replaced

-:0c209a3e2647
+:8779d321cc2e
 | _                 \<Rightarrow> False)
 | _      \<Rightarrow> False)"
 definition init_same_inode_files :: "t_file \<Rightarrow> t_file set"
 where
-"init_same_inode_files f \<equiv> {f'. init_inum_of_file f = init_inum_of_file f'}"
+"init_same_inode_files f \<equiv> if is_init_file f then {f'. init_inum_of_file f = init_inum_of_file f'} else {}"
 fun init_alive :: "t_object \<Rightarrow> bool"
 where
 "init_alive (O_proc p)     = (p \<in> init_procs)"
 | "init_alive (O_file f)     = (is_init_file f)"
 (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>"  (* may be sth wrong with nettemp representing addr \<times> netdev in statical analysis ??? *)
+| "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
 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> {f'. inum_of_file s f = inum_of_file s f'}"
+"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' =
 where
 "os_grant \<tau> (Open p f flags fd inumopt) = (
 case inumopt of
 Some ino \<Rightarrow>
 (p \<in> current_procs \<tau> \<and> f \<notin> current_files \<tau> \<and>
-(\<exists> pf. parent f = Some pf \<and> pf \<in> current_files \<tau> \<and> is_dir \<tau> pf \<and> pf \<notin> files_hung_by_del \<tau>) \<and>
+(\<exists> pf. parent f = Some pf \<and> is_dir \<tau> pf \<and> pf \<notin> files_hung_by_del \<tau>) \<and>
 is_creat_flag flags \<and> fd \<notin> (current_proc_fds \<tau> p) \<and> ino \<notin> (current_inode_nums \<tau>))
 |   None     \<Rightarrow>
-(p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau> \<and> \<not> is_creat_excl_flag flags \<and> is_file \<tau> f \<and>
+(p \<in> current_procs \<tau> \<and> \<not> is_creat_excl_flag flags \<and> is_file \<tau> f \<and>
 fd \<notin> (current_proc_fds \<tau> p))           )"
 (*(if (is_dir \<tau> f) then (is_dir_flag flags \<and> \<not> is_write_flag flags) else (\<not> is_dir_flag flags)),
 here open is not applied to directories, readdir is for that, but it is not security-related *)
 | "os_grant \<tau> (CloseFd p fd)                  =
 (p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p)"
 | "os_grant \<tau> (UnLink p f)                    =
-(p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau> \<and> is_file \<tau> f \<and> f \<notin> files_hung_by_del \<tau>)"
+(p \<in> current_procs \<tau> \<and> is_file \<tau> f \<and> f \<notin> files_hung_by_del \<tau>)"
 | "os_grant \<tau> (Rmdir p f)                     =
-(p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau> \<and> dir_is_empty \<tau> f \<and> f \<notin> files_hung_by_del \<tau> \<and> f \<noteq> [])" (* root file cannot be deleted *)
+(p \<in> current_procs \<tau> \<and> dir_is_empty \<tau> f \<and> f \<notin> files_hung_by_del \<tau> \<and> f \<noteq> [])" (* root file cannot be deleted *)
 | "os_grant \<tau> (Mkdir p f ino)                 =
 (p \<in> current_procs \<tau> \<and> f \<notin> current_files \<tau> \<and>
-(\<exists> pf. parent f = Some pf \<and> pf \<in> current_files \<tau> \<and> is_dir \<tau> pf \<and> pf \<notin> files_hung_by_del \<tau>) \<and>
+(\<exists> pf. parent f = Some pf \<and> is_dir \<tau> pf \<and> pf \<notin> files_hung_by_del \<tau>) \<and>
 ino \<notin> (current_inode_nums \<tau>))"
 | "os_grant \<tau> (LinkHard p f\<^isub>1 f\<^isub>2)              =
-(p \<in> current_procs \<tau> \<and> f\<^isub>1 \<in> current_files \<tau> \<and> f\<^isub>2 \<notin> current_files \<tau> \<and>
+(p \<in> current_procs \<tau> \<and> is_file \<tau> f\<^isub>1 \<and> f\<^isub>2 \<notin> current_files \<tau> \<and>
-(\<exists> pf\<^isub>2. parent f\<^isub>2 = Some pf\<^isub>2 \<and> pf\<^isub>2 \<in> current_files \<tau> \<and> is_dir \<tau> pf\<^isub>2 \<and>
+(\<exists> pf\<^isub>2. parent f\<^isub>2 = Some pf\<^isub>2 \<and> is_dir \<tau> pf\<^isub>2 \<and> pf\<^isub>2 \<notin> files_hung_by_del \<tau>))"
-pf\<^isub>2 \<notin> files_hung_by_del \<tau>) \<and> is_file \<tau> f\<^isub>1)"
 | "os_grant \<tau> (Truncate p f len)              =
-(p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau> \<and> is_file \<tau> f)"
+(p \<in> current_procs \<tau> \<and> is_file \<tau> f)"
 (*
 | "os_grant \<tau> (FTruncate p fd len)            =
 (p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and>
 (\<exists> f. file_of_proc_fd \<tau> p fd = Some f \<and> f \<in> current_files \<tau> \<and> is_file \<tau> f) \<and>
 (\<exists> flags. flags_of_proc_fd \<tau> p fd = Some flags \<and> is_write_flag flags))"
 | "os_grant \<tau> (WriteFile p fd)                =
 (p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and>
 (\<exists> f. file_of_proc_fd \<tau> p fd = Some f \<and> f \<in> current_files \<tau>) \<and>
 (\<exists> flags. flags_of_proc_fd \<tau> p fd = Some flags \<and> is_write_flag flags))"
 | "os_grant \<tau> (Execve p f fds)                =
-(p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau> \<and> is_file \<tau> f \<and> fds \<subseteq> current_proc_fds \<tau> p)" (* file_at_writing_by \<tau> f = {} *)
+(p \<in> current_procs \<tau> \<and> is_file \<tau> f \<and> fds \<subseteq> current_proc_fds \<tau> p)" (* file_at_writing_by \<tau> f = {} *)
 (*
 | "os_grant \<tau> (Rename p f\<^isub>2 f\<^isub>3)                =
 (p \<in> current_procs \<tau> \<and> f\<^isub>2 \<in> current_files \<tau> \<and> \<not>(f\<^isub>2 \<preceq> f\<^isub>3) \<and> f\<^isub>3 \<notin> current_files \<tau> \<and>
 (\<exists> pf\<^isub>3. parent f\<^isub>3 = Some pf\<^isub>3 \<and> pf\<^isub>3 \<in> current_files \<tau> \<and> is_dir \<tau> pf\<^isub>3 \<and>
 pf\<^isub>3 \<notin> files_hung_by_del \<tau>) )"
 socket_state \<tau> (p, fd) = Some SS_create)" (* ?? !! (case addr of INET_ADDR ip port \<Rightarrow> ip \<in> local_ipaddrs)) *)
 | "os_grant \<tau> (Connect p fd addr)             =
 (p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and> (p, fd) \<in> current_sockets \<tau> \<and>
 socket_state \<tau> (p, fd) = Some SS_bind)"
 | "os_grant \<tau> (Listen p fd)                   =
-(p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and> (p, fd) \<in> current_sockets \<tau> \<and>
+(p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and> is_tcp_sock \<tau> (p, fd) \<and>
-socket_state \<tau> (p, fd) = Some SS_bind \<and> is_tcp_sock \<tau> (p, fd))" (* Listen and Accept should only be used for TCP sever side *)
+socket_state \<tau> (p, fd) = Some SS_bind)" (* Listen and Accept should only be used for TCP sever side *)
 | "os_grant \<tau> (SendSock p fd)                 =
 (p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and> (p, fd) \<in> current_sockets \<tau> \<and>
 socket_in_sending \<tau> (p, fd))"
 | "os_grant \<tau> (RecvSock p fd)                 =
 (p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and> (p, fd) \<in> current_sockets \<tau> \<and>
 (p\<^isub>1 \<in> current_procs \<tau> \<and> p\<^isub>2 \<in> current_procs \<tau>)" (* a process can trace itself right? *)
 fun alive :: "t_state \<Rightarrow> t_object \<Rightarrow> bool"
 where
 "alive s (O_proc p)     = (p \<in> current_procs s)"
-| "alive s (O_file f)     = (f \<in> current_files s \<and> is_file s f)"
+| "alive s (O_file f)     = (is_file s f)"
-| "alive s (O_dir  f)     = (f \<in> current_files s \<and> is_dir s f)"
+| "alive s (O_dir  f)     = (is_dir s f)"
 | "alive s (O_fd p fd)    = (fd \<in> current_proc_fds s p)"
 | "alive s (O_node n)     = (n \<in> init_nodes)"
-| "alive s (O_tcp_sock k) = (k \<in> current_sockets s \<and> is_tcp_sock s k)"
+| "alive s (O_tcp_sock k) = (is_tcp_sock s k)"
-| "alive s (O_udp_sock k) = (k \<in> current_sockets s \<and> is_udp_sock s k)"
+| "alive s (O_udp_sock k) = (is_udp_sock s k)"
 | "alive s (O_shm  h)     = (h \<in> current_shms s)"
 | "alive s (O_msgq q)     = (q \<in> current_msgqs s)"
 | "alive s (O_msg q m)    = (m \<in> set (msgs_of_queue s q) \<and> q \<in> current_msgqs s)"
 (* deleted objects should be "taintable" objects, objects like fd should not be in consideration *)

changeset 6	8779d321cc2e
parent 4	e9c5594d5963
child 7	f27882976251