wrong of info-flow-shm, it is a inductive(transitive) notion, not a simple relation just between 2 nodes, more information, see 5.7 of ideas_of_selinux.txt
theory Flaskimports Main Flask_type OS_type_def File_renaming begin(****** Policy-language-level rule match/auxiliary functions ******)fun patt_match :: "'a patt \<Rightarrow> 'a \<Rightarrow> bool"where "patt_match (Single x) y = (x = y)"| "patt_match (Set s) x = (x \<in> s)"| "patt_match (Tilde s) x = (x \<notin> s)"| "patt_match Asterisk x = True"(* match a target with a patt, but including the SELF special * patt_match_self patt target source *)fun patt_match_self :: "(type_t patt) target_with_self_t \<Rightarrow> type_t \<Rightarrow> type_t \<Rightarrow> bool"where "patt_match_self Self tt st = (tt = st)"| "patt_match_self (Not_self (Single p)) tt st = (tt = p)"| "patt_match_self (Not_self (Set p)) tt st = (tt \<in> p)"| "patt_match_self (Not_self (Tilde p)) tt st = (tt \<notin> p)"| "patt_match_self (Not_self Asterisk) tt st = True"(* list lookup: find the first one *)fun lookup :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a option"where "lookup [] P = None"| "lookup (x # xs) P = (if (P x) then Some x else lookup xs P)"(* list member: if exists an element satisfy predicate P *)fun member :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"where "member [] P = False"| "member (x # xs) P = (if (P x) then True else member xs P)"(******* socket related aux functions ********)fun is_remote_request :: "t_event \<Rightarrow> bool" where "is_remote_request (Accept p fd addr port fd' i) = True"| "is_remote_request (Connect p fd addr) = True"| "is_remote_request (SendSock p fd) = True"| "is_remote_request (RecvSock p fd) = True"| "is_remote_request e = False"fun ip_of_addr:: "t_sock_addr \<Rightarrow> t_inet_addr"where "ip_of_addr (INET_ADDR saddr sport) = saddr"fun port_of_addr:: "t_sock_addr \<Rightarrow> t_socket_port"where "port_of_addr (INET_ADDR saddr sport) = sport"fun after_bind:: "t_sock_state option \<Rightarrow> bool"where "after_bind None = False"| "after_bind (Some SS_create) = False"| "after_bind _= True" (* after bind , it should have local addr *)fun after_conacc:: "t_sock_state option \<Rightarrow> bool"where "after_conacc None = False"| "after_conacc (Some SS_create) = False"| "after_conacc (Some SS_bind) = False"| "after_conacc (Some SS_listen) = False"| "after_conacc _ = True" (* after connect or accept, it should have remote addr *)(* inet_addr_compare addr1 addr2 \<equiv> addr1 \<le> addr2; but in \<le>'s def,there is a \<exists>, is not a function*)fun subnet_addr :: "t_inet_addr \<Rightarrow> t_inet_addr \<Rightarrow> bool"where "subnet_addr [] addr = True"| "subnet_addr (x#xs) [] = False"| "subnet_addr (x#xs) (y#ys) = ((x = y) \<and> subnet_addr xs ys)"definition port_in_range :: "t_socket_port \<Rightarrow> t_socket_port \<Rightarrow> t_socket_port \<Rightarrow> bool"where "port_in_range minp maxp p \<equiv> ((p < maxp \<or> p = maxp) \<and> (p > minp \<or> p = minp))"(* initial value of initiate state constrains aux function *)definition bidirect_in_init :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> bool"where "bidirect_in_init S f \<equiv> (\<forall> a. a \<in> S \<longrightarrow> (\<exists> b. f a = Some b)) \<and> (\<forall> a b. f a = Some b \<longrightarrow> a \<in> S)" fun is_file_itag :: "t_inode_tag \<Rightarrow> bool"where "is_file_itag Tag_FILE = True"| "is_file_itag tag = False"fun is_dir_itag :: "t_inode_tag \<Rightarrow> bool"where "is_dir_itag Tag_DIR = True"| "is_dir_itag tag = False"fun is_file_dir_itag :: "t_inode_tag \<Rightarrow> bool"where "is_file_dir_itag Tag_FILE = True"| "is_file_dir_itag Tag_DIR = True"| "is_file_dir_itag tag = False"fun is_tcp_itag :: "t_inode_tag \<Rightarrow> bool"where "is_tcp_itag Tag_TCP_SOCK = True"| "is_tcp_itag tag = False"fun is_udp_itag :: "t_inode_tag \<Rightarrow> bool"where "is_udp_itag Tag_UDP_SOCK = True"| "is_udp_itag tag = False"fun is_sock_itag :: "t_inode_tag \<Rightarrow> bool"where "is_sock_itag Tag_TCP_SOCK = True"| "is_sock_itag Tag_UDP_SOCK = True"| "is_sock_itag tag = False"locale init = fixes init_files :: "t_file set" and init_procs :: "t_process set" and init_nodes :: "t_node set" and init_sockets :: "t_socket set" and init_users :: "user_t set" and init_file_of_proc_fd :: "t_process \<Rightarrow> t_fd \<rightharpoonup> t_file" and init_fds_of_proc :: "t_process \<Rightarrow> t_fd set" and init_oflags_of_proc_fd:: "t_process \<Rightarrow> t_fd \<rightharpoonup> t_open_flags" and init_inum_of_file :: "t_file \<rightharpoonup> t_inode_num" and init_inum_of_socket:: "t_socket \<rightharpoonup> t_inode_num" and init_itag_of_inum:: "t_inode_num \<rightharpoonup> t_inode_tag" and init_files_hung_by_del :: "t_file set"(* 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 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" assumes parent_file_in_init: "\<And> f pf. \<lbrakk>parent f = Some pf; f \<in> init_files\<rbrakk> \<Longrightarrow> pf \<in> init_files" and root_is_dir: "\<exists> i. init_inum_of_file [] = Some i \<and> init_itag_of_inum i = Some Tag_DIR" and init_file_has_inum: "\<And> f. f \<in> init_files \<Longrightarrow> \<exists> im. init_inum_of_file f = Some im" and inof_has_file_tag: "\<And> f im. init_inum_of_file f = Some im \<Longrightarrow> f \<in> init_files \<and> (\<exists> tag. init_itag_of_inum im = Some tag \<and> is_file_dir_itag tag)" and init_file_no_son: "\<And> f im. \<lbrakk>init_inum_of_file f = Some im; init_itag_of_inum im = Some Tag_FILE\<rbrakk> \<Longrightarrow> \<not> (\<exists> f' \<in> init_files. parent f' = Some f)" and init_parentf_is_dir: "\<And> f pf im. \<lbrakk>parent f = Some pf; f \<in> init_files; init_inum_of_file pf = Some im\<rbrakk> \<Longrightarrow> init_itag_of_inum im = Some Tag_DIR" and init_files_hung_valid: "\<And> f. f \<in> init_files_hung_by_del \<Longrightarrow> f \<in> init_files \<and> (\<exists> p fd. init_file_of_proc_fd p fd = Some f)" and init_files_hung_valid': "\<And> f im. \<lbrakk>f \<in> init_files_hung_by_del; init_inum_of_file f = Some im\<rbrakk> \<Longrightarrow> init_itag_of_inum im = Some Tag_FILE \<or> (init_itag_of_inum im = Some Tag_DIR \<and> \<not> (\<exists> f'. f' \<in> init_files \<and> f \<prec> f'))" and init_procfds_valid: "\<And> p fd. fd \<in> init_fds_of_proc p \<Longrightarrow> p \<in> init_procs \<and> ((\<exists> f \<in> init_files. init_file_of_proc_fd p fd = Some f) \<or> (p, fd) \<in> init_sockets)" and init_filefd_valid: "\<And> p fd f. init_file_of_proc_fd p fd = Some f \<Longrightarrow> fd \<in> init_fds_of_proc p \<and> (\<exists> im. init_inum_of_file f = Some im \<and> init_itag_of_inum im = Some Tag_FILE) \<and> p \<in> init_procs \<and> (\<exists> flags. init_oflags_of_proc_fd p fd = Some flags)" and init_fileflag_valid: "\<And> p fd flags. init_oflags_of_proc_fd p fd = Some flags \<Longrightarrow> \<exists> f. init_file_of_proc_fd p fd = Some f" 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_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 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" begin definition is_init_file:: "t_file \<Rightarrow> bool"where "is_init_file f \<equiv> (case (init_inum_of_file f) of Some i \<Rightarrow> (case (init_itag_of_inum i) of Some Tag_FILE \<Rightarrow> True | _ \<Rightarrow> False) | _ \<Rightarrow> False)"definition is_init_dir:: "t_file \<Rightarrow> bool"where "is_init_dir f \<equiv> (case (init_inum_of_file f) of Some i \<Rightarrow> (case (init_itag_of_inum i) of Some Tag_DIR \<Rightarrow> True | _ \<Rightarrow> False) | _ \<Rightarrow> False)"definition is_init_tcp_sock:: "t_socket \<Rightarrow> bool"where "is_init_tcp_sock s \<equiv> (case (init_inum_of_socket s) of Some i \<Rightarrow> (case (init_itag_of_inum i) of Some Tag_TCP_SOCK \<Rightarrow> True | _ \<Rightarrow> False) | _ \<Rightarrow> False)"definition is_init_udp_sock:: "t_socket \<Rightarrow> bool"where "is_init_udp_sock s \<equiv> (case (init_inum_of_socket s) of Some i \<Rightarrow> (case (init_itag_of_inum i) of Some Tag_UDP_SOCK \<Rightarrow> True | _ \<Rightarrow> False) | _ \<Rightarrow> False)"definition init_same_inode_files :: "t_file \<Rightarrow> t_file set"where "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)"| "init_alive (O_dir f) = (is_init_dir f)"| "init_alive (O_fd p fd) = (fd \<in> init_fds_of_proc p)"| "init_alive (O_node n) = (n \<in> init_nodes)"| "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_msg q m) = (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"where "file_of_proc_fd [] p' fd' = (init_file_of_proc_fd p' fd')"| "file_of_proc_fd (Open p f flags fd iopt # \<tau>) p' fd' = (if (p' = p \<and> fd = fd') then Some f else file_of_proc_fd \<tau> p' fd')"| "file_of_proc_fd (CloseFd p fd # \<tau>) p' fd' = (if (p = p' \<and> fd = fd') then None else file_of_proc_fd \<tau> p' fd')"(*deleted: if (f\<^isub>3 \<preceq> f\<^isub>1) then None else *)(*| "file_of_proc_fd (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) p' fd = (case (file_of_proc_fd \<tau> p' fd) of Some f\<^isub>1 \<Rightarrow> (if (f\<^isub>2 \<preceq> f\<^isub>1) then Some (file_after_rename f\<^isub>2 f\<^isub>3 f\<^isub>1) else Some f\<^isub>1) | None \<Rightarrow> None )"*)| "file_of_proc_fd (Execve p f fds # \<tau>) p' fd = (if (p' = p \<and> fd \<in> fds) then file_of_proc_fd \<tau> p fd else if (p' = p) then None else file_of_proc_fd \<tau> p' fd) "| "file_of_proc_fd (Clone p p' fds shms # \<tau>) p'' fd = (if (p'' = p' \<and> fd \<in> fds) then file_of_proc_fd \<tau> p fd else if (p'' = p') then None else file_of_proc_fd \<tau> p'' fd)"| "file_of_proc_fd (Kill p\<^isub> p\<^isub>' # \<tau>) p'' fd = (if (p'' = p\<^isub>') then None else file_of_proc_fd \<tau> p'' fd)"| "file_of_proc_fd (Exit p # \<tau>) p' fd = (if (p = p') then None else file_of_proc_fd \<tau> p' fd)"| "file_of_proc_fd (_ # \<tau>) p fd = file_of_proc_fd \<tau> p fd"definition proc_fd_of_file :: "t_state \<Rightarrow> t_file \<Rightarrow> (t_process \<times> t_fd) set"where "proc_fd_of_file \<tau> f = {(p, fd) | p fd. file_of_proc_fd \<tau> p fd = Some f}"(****** files and directories ******)fun files_hung_by_del :: "t_state \<Rightarrow> t_file set"where "files_hung_by_del [] = init_files_hung_by_del"| "files_hung_by_del (UnLink p f # \<tau>) = ( if (proc_fd_of_file \<tau> f = {}) then files_hung_by_del \<tau> else insert f (files_hung_by_del \<tau>))"(* | files_hung_by_del (Rmdir p f) is not need, for open can only apply to file not dir *)| "files_hung_by_del (CloseFd p fd # \<tau>) = ( case (file_of_proc_fd \<tau> p fd) of Some f \<Rightarrow> (if (proc_fd_of_file \<tau> f = {(p, fd)}) then files_hung_by_del \<tau> - {f} else files_hung_by_del \<tau>) | None \<Rightarrow> files_hung_by_del \<tau> )"(*| "files_hung_by_del (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) = {file_after_rename f\<^isub>2 f\<^isub>3 f\<^isub>1| f\<^isub>1. f\<^isub>1 \<in> files_hung_by_del \<tau>}" (* for rename(2) does not infect on fd of the file, see man -S 2 rename *)*)| "files_hung_by_del (e # \<tau>) = files_hung_by_del \<tau>"declare files_hung_by_del.simps [simp del]fun inum_of_file :: "t_state \<Rightarrow> (t_file \<rightharpoonup> t_inode_num)"where "inum_of_file [] = init_inum_of_file"| "inum_of_file (Open p f flags fd (Some inum) # \<tau>) = (inum_of_file \<tau>) (f := Some inum)" | "inum_of_file (CloseFd p fd # \<tau>) = ( case (file_of_proc_fd \<tau> p fd) of Some f \<Rightarrow> ( if ((proc_fd_of_file \<tau> f = {(p, fd)}) \<and> (f \<in> files_hung_by_del \<tau>)) then (inum_of_file \<tau>) (f := None) else inum_of_file \<tau> ) | _ \<Rightarrow> (inum_of_file \<tau>) )"| "inum_of_file (UnLink p f # \<tau>) = ( if (proc_fd_of_file \<tau> f = {}) then (inum_of_file \<tau>) (f := None) else inum_of_file \<tau> )" | "inum_of_file (Rmdir p f # \<tau>) = (inum_of_file \<tau>) (f := None)"| "inum_of_file (Mkdir p f ino # \<tau>) = (inum_of_file \<tau>) (f:= Some ino)"| "inum_of_file (LinkHard p f\<^isub>1 f\<^isub>2 # \<tau>) = (inum_of_file \<tau>) (f\<^isub>2 := inum_of_file \<tau> f\<^isub>1)"(*| "inum_of_file (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) = (\<lambda> f. if (f\<^isub>2 \<preceq> f) then None else if (f\<^isub>3 \<preceq> f) then inum_of_file \<tau> (file_before_rename f\<^isub>2 f\<^isub>3 f) else inum_of_file \<tau> f )"*)| "inum_of_file (e # \<tau>) = inum_of_file \<tau>" definition current_files :: "t_state \<Rightarrow> t_file set"where "current_files \<tau> = {f. \<exists> i. inum_of_file \<tau> f = Some i}" definition has_same_inode :: "t_state \<Rightarrow> t_file \<Rightarrow> t_file \<Rightarrow> bool"where "has_same_inode \<tau> fa fb = (\<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>) = (inum_of_socket \<tau>) ((p, fd):= None)"| "inum_of_socket (CreateSock p af st fd ino # \<tau>) = (inum_of_socket \<tau>) ((p, fd) := Some ino)"| "inum_of_socket (Accept p fd addr lport' fd' ino # \<tau>) = (inum_of_socket \<tau>) ((p, fd') := Some ino)"| "inum_of_socket (Clone p p' fds shms # \<tau>) = (\<lambda> (p'', fd). if (p'' = p' \<and> fd \<in> fds) then inum_of_socket \<tau> (p, fd) else if (p'' = p') then None else inum_of_socket \<tau> (p'',fd))" | "inum_of_socket (Execve p f fds # \<tau>) = (\<lambda> (p', fd). if (p' = p \<and> fd \<in> fds) then inum_of_socket \<tau> (p, fd) else if (p' = p) then None else inum_of_socket \<tau> (p', fd))"| "inum_of_socket (Kill p\<^isub>1 p\<^isub>2 # \<tau>) = (\<lambda> (p, fd). if (p = p\<^isub>2) then None else inum_of_socket \<tau> (p, fd) )"| "inum_of_socket (Exit p # \<tau>) = (\<lambda> (p', fd). if (p' = p) then None else inum_of_socket \<tau> (p', fd))"| "inum_of_socket (_ # \<tau>) = inum_of_socket \<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 | _ \<Rightarrow> False) | _ \<Rightarrow> False)"definition is_udp_sock :: "t_state \<Rightarrow> t_socket \<Rightarrow> bool"where "is_udp_sock \<tau> s \<equiv> (case (inum_of_socket \<tau> s) of Some i \<Rightarrow> (case (itag_of_inum \<tau> i) of Some Tag_UDP_SOCK \<Rightarrow> True | _ \<Rightarrow> False) | _ \<Rightarrow> False)"fun current_procs :: "t_state \<Rightarrow> t_process set"where "current_procs [] = init_procs"| "current_procs (Clone p p' fds shms # \<tau>) = (insert p' (current_procs \<tau>))"| "current_procs (Exit p # \<tau>) = (current_procs \<tau> - {p})"| "current_procs (Kill p p' # \<tau>) = (current_procs \<tau> - {p'})"| "current_procs (_ # \<tau>) = current_procs \<tau>" fun current_proc_fds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd set" where "current_proc_fds [] = init_fds_of_proc"| "current_proc_fds (Open p f flags fd iopt # \<tau>) = (current_proc_fds \<tau>) (p:= insert fd (current_proc_fds \<tau> p))"| "current_proc_fds (CreateSock p sf st newfd newi # \<tau>) = (current_proc_fds \<tau>) (p:= insert newfd (current_proc_fds \<tau> p))" | "current_proc_fds (Accept p fd raddr port fd' ino # \<tau>) = (current_proc_fds \<tau>) (p:= insert fd' (current_proc_fds \<tau> p))"| "current_proc_fds (CloseFd p fd # \<tau>) = (current_proc_fds \<tau>) (p:= (current_proc_fds \<tau> p) - {fd})"| "current_proc_fds (Clone p p' fds shms # \<tau>) = (current_proc_fds \<tau>) (p':= fds)"| "current_proc_fds (Execve p f fds # \<tau>) = (current_proc_fds \<tau>) (p:= fds)"| "current_proc_fds (Exit p # \<tau>) = (current_proc_fds \<tau>) (p := {})"| "current_proc_fds (Kill p p' # \<tau>) = (current_proc_fds \<tau>) (p' := {})"| "current_proc_fds (_ # \<tau>) = current_proc_fds \<tau>"fun current_shms :: "t_state \<Rightarrow> t_shm set"where "current_shms [] = init_shms"| "current_shms (CreateShM p newshm # \<tau>) = insert newshm (current_shms \<tau>)"| "current_shms (DeleteShM p s # \<tau>) = (current_shms \<tau>) - {s}"| "current_shms (e # \<tau>) = current_shms \<tau> "fun flag_of_proc_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_shm \<Rightarrow> t_shm_attach_flag option"where "flag_of_proc_shm [] = init_flag_of_proc_shm"| "flag_of_proc_shm (Attach p h flag # s) = (\<lambda> p' h'. if (p' = p \<and> h' = h) then Some flag else flag_of_proc_shm s p' h')"| "flag_of_proc_shm (Detach p h # s) = (\<lambda> p' h'. if (p' = p \<and> h' = h) then None else flag_of_proc_shm s p' h')"| "flag_of_proc_shm (CreateShM p h # s) = (\<lambda> p' h'. if (h' = h) then None else flag_of_proc_shm s p' h')"| "flag_of_proc_shm (DeleteShM p h # s) = (\<lambda> p' h'. if (h' = h) then None else flag_of_proc_shm s p' h')"| "flag_of_proc_shm (Clone p p' fds shms # s) = (\<lambda> p'' h. if (p'' = p' \<and> h \<in> shms) then flag_of_proc_shm s p h else if (p'' = p') then None else flag_of_proc_shm s p'' h)"| "flag_of_proc_shm (Execve p f fds # s) = (\<lambda> p' h. if (p' = p) then None else flag_of_proc_shm s p' h)"| "flag_of_proc_shm (Kill p p' # s) = (\<lambda> p'' h. if (p'' = p') then None else flag_of_proc_shm s p'' h)"| "flag_of_proc_shm (Exit p # s) = (\<lambda> p' h. if (p' = p) then None else flag_of_proc_shm s p' h)"| "flag_of_proc_shm (e # s) = flag_of_proc_shm s"fun procs_of_shm :: "t_state \<Rightarrow> t_shm \<Rightarrow> (t_process \<times> t_shm_attach_flag) set"where "procs_of_shm [] = init_procs_of_shm"| "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) | 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) | 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) | flag. (p, flag) \<in> procs_of_shm \<tau> h})"| "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>"inductive info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"where "p \<in> current_procs s \<Longrightarrow> info_flow_shm s p p"| "\<lbrakk>info_flow_shm s p p'; (p', SHM_RDWR) \<in> procs_of_shm s h; (p'', flag) \<in> procs_of_shm s h; p' \<noteq> p''\<rbrakk> \<Longrightarrow> info_flow_shm s p p''"(*definition info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"where "info_flow_shm \<tau> from to \<equiv> (from = to \<and> from \<in> current_procs \<tau>) \<or> (\<exists> h toflag. (((from, SHM_RDWR) \<in> procs_of_shm \<tau> h) \<and> ((to, toflag) \<in> procs_of_shm \<tau> h)))" *)fun current_msgqs :: "t_state \<Rightarrow> t_msg set"where "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 (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>" definition current_file_inums :: "t_state \<Rightarrow> t_inode_num set"where "current_file_inums \<tau> \<equiv> {im. \<exists> f. inum_of_file \<tau> f = Some im}"definition current_sock_inums :: "t_state \<Rightarrow> t_inode_num set"where "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' = (if (p = p' \<and> fd = fd') then Some flags else flags_of_proc_fd \<tau> p' fd')"| "flags_of_proc_fd (CloseFd p fd # \<tau>) p' fd' = (if (p = p' \<and> fd = fd') then None else flags_of_proc_fd \<tau> p' fd')"| "flags_of_proc_fd (CreateSock p af st fd ino # \<tau>) p' fd' = (if (p = p' \<and> fd = fd') then None else flags_of_proc_fd \<tau> p' fd')"| "flags_of_proc_fd (Accept p fd addr lport' fd' ino # \<tau>) p' fd'' = (if (p = p' \<and> fd' = fd'') then None else flags_of_proc_fd \<tau> p' fd'')"| "flags_of_proc_fd (Clone p p' fds shms # \<tau>) p'' fd = (if (p' = p'' \<and> fd \<in> fds) then flags_of_proc_fd \<tau> p fd else flags_of_proc_fd \<tau> p'' fd)" | "flags_of_proc_fd (Execve p f fds # \<tau>) p' fd = (if (p' = p \<and> fd \<in> fds) then flags_of_proc_fd \<tau> p fd else flags_of_proc_fd \<tau> p' fd)"| "flags_of_proc_fd (Kill p\<^isub>1 p\<^isub>2 # \<tau>) p fd = (if (p = p\<^isub>2) then None else flags_of_proc_fd \<tau> p fd)"| "flags_of_proc_fd (Exit p # \<tau>) p' fd' = (if (p = p') then None else flags_of_proc_fd \<tau> p' fd')"| "flags_of_proc_fd (e # \<tau>) p fd = flags_of_proc_fd \<tau> p fd" (* fun file_at_writing_by:: "t_state \<Rightarrow> t_file \<Rightarrow> (t_process \<times> t_fd) set"where "file_at_writing_by [] f = init_file_at_writing_by f" | "file_at_writing_by (Open p f flags fd (Some inum) # \<tau>) f' = ( if (f' = f) then ( if (is_write_flag flags) then {(p, fd)} else {} ) else file_at_writing_by \<tau> f' )"| "file_at_writing_by (Open p f flags fd None # \<tau>) f' = ( if (f' = f \<and> is_write_flag flags) then insert (p, fd) (file_at_writing_by \<tau> f) else file_at_writing_by \<tau> f' )"| "file_at_writing_by (Mkdir p f inum # \<tau>) f' = (if (f' = f) then {} else file_at_writing_by \<tau> f')"| "file_at_writing_by (LinkHard p f f' # \<tau>) f'' = (if (f'' = f') then file_at_writing_by \<tau> f else file_at_writing_by \<tau> f'')"| "file_at_writing_by (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) f = ( if (f\<^isub>3 \<preceq> f) then file_at_writing_by \<tau> (file_before_rename f\<^isub>2 f\<^isub>3 f) else file_at_writing_by \<tau> f )"| "file_at_writing_by (CloseFd p fd # \<tau>) f = (file_at_writing_by \<tau> f - {(p, fd)})"| "file_at_writing_by (Clone p p' fds shms # \<tau>) f = (file_at_writing_by \<tau> f) \<union> {(p',fd)| fd. fd \<in> fds \<and> (p, fd) \<in> file_at_writing_by \<tau> f}"| "file_at_writing_by (Execve p f fds # \<tau>) f' = (if (f' = f) then {} else file_at_writing_by \<tau> f')"| "file_at_writing_by (Exit p # \<tau>) f = (file_at_writing_by \<tau> f - {(p, fd)| fd. (p, fd) \<in> file_at_writing_by \<tau> f})"| "file_at_writing_by (Kill p p' # \<tau>) f = (file_at_writing_by \<tau> f - {(p', fd)| fd. (p', fd) \<in> file_at_writing_by \<tau> f})"| "file_at_writing_by (e # \<tau>) f = file_at_writing_by \<tau> f"*)definition current_users :: "t_state \<Rightarrow> user_t set"where "current_users \<tau> \<equiv> init_users" fun update_with_shuthow :: "t_sock_state option \<Rightarrow> t_shutdown_how \<Rightarrow> t_sock_state option"where "update_with_shuthow (Some (SS_trans Trans_Recv)) SHUT_RD = Some (SS_trans Trans_No)"| "update_with_shuthow (Some (SS_trans Trans_RS)) SHUT_RD = Some (SS_trans Trans_Send)"| "update_with_shuthow (Some (SS_trans Trans_Send)) SHUT_RD = Some (SS_trans Trans_Send)"| "update_with_shuthow (Some (SS_trans Trans_No)) SHUT_RD = Some (SS_trans Trans_No)"| "update_with_shuthow (Some (SS_trans Trans_Recv)) SHUT_WR = Some (SS_trans Trans_Recv)"| "update_with_shuthow (Some (SS_trans Trans_RS)) SHUT_WR = Some (SS_trans Trans_Recv)"| "update_with_shuthow (Some (SS_trans Trans_Send)) SHUT_WR = Some (SS_trans Trans_No)"| "update_with_shuthow (Some (SS_trans Trans_No)) SHUT_WR = Some (SS_trans Trans_No)"| "update_with_shuthow (Some (SS_trans Trans_Recv)) SHUT_RDWR = Some (SS_trans Trans_No)"| "update_with_shuthow (Some (SS_trans Trans_RS)) SHUT_RDWR = Some (SS_trans Trans_No)"| "update_with_shuthow (Some (SS_trans Trans_Send)) SHUT_RDWR = Some (SS_trans Trans_No)"| "update_with_shuthow (Some (SS_trans Trans_No)) SHUT_RDWR = Some (SS_trans Trans_No)"| "update_with_shuthow opt1 how = None" fun socket_state :: "t_state \<Rightarrow> t_socket \<Rightarrow> t_sock_state option"where "socket_state [] = init_socket_state"| "socket_state (CloseFd p fd # \<tau>) = (socket_state \<tau>) ((p, fd):= None)"| "socket_state (CreateSock p af st fd ino # \<tau>) = (socket_state \<tau>) ((p, fd) := Some SS_create)"| "socket_state (Bind p fd addr # \<tau>) = (socket_state \<tau>) ((p, fd) := Some SS_bind)"| "socket_state (Connect p fd addr # \<tau>) = (socket_state \<tau>) ((p, fd) := Some (SS_trans Trans_RS))"| "socket_state (Listen p fd # \<tau>) = (socket_state \<tau>) ((p, fd) := Some SS_listen)"| "socket_state (Accept p fd addr lport' fd' ino # \<tau>) = (socket_state \<tau>) ((p, fd') := Some (SS_trans Trans_RS))"| "socket_state (Shutdown p fd sh # \<tau>) = (socket_state \<tau>) ((p, fd) := update_with_shuthow (socket_state \<tau> (p, fd)) sh)"| "socket_state (Clone p p' fds shms # \<tau>) = (\<lambda> (p'', fd). if (p'' = p' \<and> fd \<in> fds) then socket_state \<tau> (p, fd) else if (p'' = p') then None else socket_state \<tau> (p'', fd))" | "socket_state (Execve p f fds # \<tau>) = (\<lambda> (p', fd). if (p' = p \<and> fd \<in> fds) then socket_state \<tau> (p, fd) else if (p' = p) then None else socket_state \<tau> (p', fd))" | "socket_state (Kill p\<^isub>1 p\<^isub>2 # \<tau>) = (\<lambda> (p, fd). if (p = p\<^isub>2) then None else socket_state \<tau> (p, fd))"| "socket_state (Exit p # \<tau>) = (\<lambda> (p', fd'). if (p = p') then None else socket_state \<tau> (p', fd'))"| "socket_state (e # \<tau>) = socket_state \<tau>" definition socket_in_trans :: "t_state \<Rightarrow> t_socket \<Rightarrow> bool"where "socket_in_trans \<tau> s \<equiv> (case (socket_state \<tau> s) of Some st \<Rightarrow> (case st of SS_trans para \<Rightarrow> True | _ \<Rightarrow> False) | _ \<Rightarrow> False)"definition socket_in_sending :: "t_state \<Rightarrow> t_socket \<Rightarrow> bool"where "socket_in_sending \<tau> s \<equiv> (socket_state \<tau> s = Some (SS_trans Trans_Send)) \<or> (socket_state \<tau> s = Some (SS_trans Trans_RS))"definition socket_in_recving :: "t_state \<Rightarrow> t_socket \<Rightarrow> bool"where "socket_in_recving \<tau> s \<equiv> (socket_state \<tau> s = Some (SS_trans Trans_Recv)) \<or> (socket_state \<tau> s = Some (SS_trans Trans_RS))"(******* admissable check by the OS *******)fun os_grant :: "t_state \<Rightarrow> t_event \<Rightarrow> bool"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> 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> \<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> is_file \<tau> f \<and> f \<notin> files_hung_by_del \<tau>)"| "os_grant \<tau> (Rmdir p f) = (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> 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> 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> is_dir \<tau> pf\<^isub>2 \<and> pf\<^isub>2 \<notin> files_hung_by_del \<tau>))"| "os_grant \<tau> (Truncate p f len) = (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> (ReadFile 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_read_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> 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>) )"*)| "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)))"| "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))"| "os_grant \<tau> (RemoveMsgq p q) = (p \<in> current_procs \<tau> \<and> q \<in> current_msgqs \<tau>)"| "os_grant \<tau> (CreateShM p h) = (p \<in> current_procs \<tau> \<and> h \<notin> (current_shms \<tau>))"| "os_grant \<tau> (Attach p h flag) = (p \<in> current_procs \<tau> \<and> h \<in> current_shms \<tau> \<and> \<not> (\<exists> flag. (p, flag) \<in> procs_of_shm \<tau> h))"| "os_grant \<tau> (Detach p h) = (p \<in> current_procs \<tau> \<and> h \<in> current_shms \<tau> \<and> (\<exists> flag. (p, flag) \<in> procs_of_shm \<tau> h))"| "os_grant \<tau> (DeleteShM p h) = (p \<in> current_procs \<tau> \<and> h \<in> current_shms \<tau>)"| "os_grant \<tau> (CreateSock p af st fd ino) = (p \<in> current_procs \<tau> \<and> af = AF_INET \<and> fd \<notin> (current_proc_fds \<tau> p) \<and> ino \<notin> (current_inode_nums \<tau>))"| "os_grant \<tau> (Accept p fd addr port fd' ino) = (p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and> (p, fd) \<in> current_sockets \<tau> \<and> fd' \<notin> (current_proc_fds \<tau> p) \<and> socket_state \<tau> (p, fd) = Some SS_listen \<and> is_tcp_sock \<tau> (p, fd) \<and> ino \<notin> (current_inode_nums \<tau>))"| "os_grant \<tau> (Bind 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_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> is_tcp_sock \<tau> (p, fd) \<and> 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> socket_in_recving \<tau> (p, fd))"| "os_grant \<tau> (Shutdown p fd sh) = (p \<in> current_procs \<tau> \<and> fd \<in> current_proc_fds \<tau> p \<and> (p, fd) \<in> current_sockets \<tau> \<and> socket_in_trans \<tau> (p, fd))"(*| "os_grant \<tau> (ChangeOwner p u) = (p \<in> current_procs \<tau> \<and> u \<in> current_users \<tau>)"*)| "os_grant \<tau> (Clone p p' fds shms) = (p \<in> current_procs \<tau> \<and> p' \<notin> (current_procs \<tau>) \<and> fds \<subseteq> current_proc_fds \<tau> p \<and> (\<forall> h \<in> shms. \<exists> flag. (p, flag) \<in> procs_of_shm \<tau> h))"| "os_grant \<tau> (Kill p\<^isub>1 p\<^isub>2) = (p\<^isub>1 \<in> current_procs \<tau> \<and> p\<^isub>2 \<in> current_procs \<tau>)" (* a process can kill itself right? *)| "os_grant \<tau> (Exit p) = (p \<in> current_procs \<tau>)"| "os_grant \<tau> (Ptrace p\<^isub>1 p\<^isub>2) = (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) = (is_file 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) = (is_tcp_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 *)(* actually, deleted should be renamed as "vanished", cause "exit/closefd" *)fun deleted :: "t_object \<Rightarrow> t_event list \<Rightarrow> bool"where "deleted obj [] = False"| "deleted obj (Kill p p' # s) = ((obj = O_proc p') \<or> (\<exists> fd \<in> current_proc_fds s p'. obj = O_fd p' fd) \<or> (\<exists> fd. obj = O_tcp_sock (p', fd) \<and> is_tcp_sock s (p',fd)) \<or> (\<exists> fd. obj = O_udp_sock (p', fd) \<and> is_udp_sock s (p',fd)) \<or> deleted obj s)"| "deleted obj (CloseFd p fd # s) = ((obj = O_fd p fd) \<or> (obj = O_tcp_sock (p,fd) \<and> is_tcp_sock s (p,fd)) \<or> (obj = O_udp_sock (p,fd) \<and> is_udp_sock s (p, fd)) \<or> (\<exists> f. obj = O_file f \<and> proc_fd_of_file s f = {(p, fd)} \<and> f \<in> files_hung_by_del s) \<or> deleted obj s)"| "deleted obj (Execve p f fds # s) = ((\<exists> fd \<in> current_proc_fds s p. obj = O_fd p fd \<and> fd \<notin> fds) \<or> (\<exists> fd. obj = O_tcp_sock (p, fd) \<and> is_tcp_sock s (p,fd) \<and> fd \<notin> fds) \<or> (\<exists> fd. obj = O_udp_sock (p, fd) \<and> is_udp_sock s (p,fd) \<and> fd \<notin> fds) \<or> deleted obj s)"| "deleted obj (Clone p p' fds shms # s) = ((\<exists> fd \<in> current_proc_fds s p. obj = O_fd p' fd \<and> fd \<notin> fds) \<or> deleted obj s)"| "deleted obj (UnLink p f # s) = ((proc_fd_of_file s f = {} \<and> obj = O_file f) \<or> deleted obj s)"| "deleted obj (Rmdir p f # s) = ((obj = O_dir f) \<or> deleted obj s)"| "deleted obj (Exit p # s) = ((obj = O_proc p) \<or> (\<exists> fd \<in> current_proc_fds s p. obj = O_fd p fd) \<or> (\<exists> fd. obj = O_tcp_sock (p, fd) \<and> is_tcp_sock s (p,fd)) \<or> (\<exists> fd. obj = O_udp_sock (p, fd) \<and> is_udp_sock s (p,fd)) \<or> deleted obj s)"(*| "deleted obj (Rename p f f' # s) = (case obj of O_file f'' \<Rightarrow> f \<preceq> f'' \<or> deleted obj s | O_dir f'' \<Rightarrow> f \<preceq> f'' \<or> deleted obj s | _ \<Rightarrow> deleted obj s)"*)| "deleted obj (RemoveMsgq p q # s) = (obj = O_msgq q \<or> (\<exists> m. obj = O_msg q m) \<or> deleted obj s)"| "deleted obj (DeleteShM p h # s) = (obj = O_shm h \<or> deleted obj s)"| "deleted obj (RecvMsg p q m # s) = (obj = O_msg q m \<or> deleted obj s)"| "deleted obj (_ # s) = deleted obj s"definition proc_file_fds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd set"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}"endlocale flask = init + fixes (***************** Policy-specific Parameters *************) type_transition_rules :: "type_transition_rule_list_t" and allowed_rules :: "allowed_rule_list_t" and role_allowed_rules :: "role_allow_rule_list_t" and role_declaration_rules :: "role_declarations_list_t" and role_transition_rules:: "role_transition_rule_list_t" and constrains_rules :: "constrains_list_t" and init_type_of_obj :: "t_object \<rightharpoonup> type_t" and init_user_of_obj :: "t_object \<rightharpoonup> user_t" and init_role_of_proc :: "t_process \<rightharpoonup> role_t" assumes init_obj_has_type: "\<And> obj. init_alive obj \<Longrightarrow> \<exists> t. init_type_of_obj obj = Some t" and init_type_has_obj: "\<And> obj t. init_type_of_obj obj = Some t \<Longrightarrow> init_alive obj" and init_obj_has_user: "\<And> obj. init_alive obj \<Longrightarrow> \<exists> u. init_user_of_obj obj = Some u" and init_user_has_obj: "\<And> obj u. init_user_of_obj obj = Some u \<Longrightarrow> init_alive obj \<and> u \<in> init_users" and init_proc_has_role: "bidirect_in_init init_procs init_role_of_proc"begin(*********** policy-specified computations, not-event-related ************)(* security_transition_sid : type_transition_rules * It's a system-call offered by security-server? So access-control-checked too? * according to selinux, it deals only with execve and file-creation * is_execve: if is the execve case * is_file: if is the creation of file/dir * change from is_execve to is_file, because the new message by default use * the type of the sending process too. *)definition type_transition :: "type_t \<Rightarrow> type_t \<Rightarrow> security_class_t \<Rightarrow> bool \<Rightarrow> type_t"where "type_transition st rt tc IS_file \<equiv> ( case (lookup type_transition_rules (\<lambda> (stp, rtp, tc', dt). patt_match stp st \<and> patt_match rtp rt \<and> tc = tc')) of None \<Rightarrow> (if IS_file then rt else st) | Some (stp,rtp,tc',dt) \<Rightarrow> dt)"(* allowed_rule_list *)definition TE_allow :: "type_t \<Rightarrow> type_t \<Rightarrow> security_class_t \<Rightarrow> permission_t \<Rightarrow> bool"where "TE_allow st tt tc perm \<equiv> member allowed_rules (\<lambda> (stp, ttp, tc', pp). tc = tc' \<and> patt_match stp st \<and> patt_match_self ttp tt st \<and> patt_match pp perm)"(* role_allow_rule_list_t *)definition role_transition :: "role_t \<Rightarrow> type_t \<Rightarrow> role_t option"where "role_transition r t \<equiv> (case (lookup role_transition_rules (\<lambda> (pr, ft, nr). pr = r \<and> t = ft)) of None \<Rightarrow> None | Some (pr,ft,nr) \<Rightarrow> Some nr)"definition role_decl_check :: "role_t \<Rightarrow> type_t \<Rightarrow> bool"where "role_decl_check r t \<equiv> member role_declaration_rules (\<lambda> (role, types). r = role \<and> t \<in> types)"definition role_allow :: "role_t \<Rightarrow> role_t \<Rightarrow> bool"where "role_allow r nr \<equiv> member role_allowed_rules (\<lambda> (from, to). r \<in> from \<and> nr \<in> to)"(* here don't use lookup, because constrains should all be satisfied, * while transitions always choose the "first" one *)definition constrains_satisfied :: "security_context_t \<Rightarrow> security_context_t \<Rightarrow> security_class_t \<Rightarrow> permission_t \<Rightarrow> bool"where "constrains_satisfied sctxt tctxt c p \<equiv> (fold (\<lambda> (cset, pset, P) res. res \<and> (if (c \<in> cset \<and> p \<in> pset) then P sctxt tctxt else True)) constrains_rules True)"(* main interface for TE_allow check and constrains check *)fun permission_check:: "security_context_t \<Rightarrow> security_context_t \<Rightarrow> security_class_t \<Rightarrow> permission_t \<Rightarrow> bool"where "permission_check (su,sr,st) (tu,tr,tt) c p = ((TE_allow st tt c p) \<and> (constrains_satisfied (su,sr,st) (tu,tr,tt) c p))"declare permission_check.simps [simp del](* no changeowner ??? : by adding "relabel obj sectxt" event or "login" event? * or this explanation: the running of the sever will not grant any login but running * of the server-programs! *)fun user_of_obj :: "t_state \<Rightarrow> t_object \<Rightarrow> user_t option"where "user_of_obj [] = init_user_of_obj"| "user_of_obj (Clone p p' fds shms # s) = (\<lambda> obj. case obj of O_proc p'' \<Rightarrow> if (p'' = p') then user_of_obj s (O_proc p) else user_of_obj s obj | O_fd p'' fd \<Rightarrow> if (p'' = p' \<and> fd \<in> fds) then user_of_obj s (O_fd p fd) else if (p'' = p') then None else user_of_obj s obj | O_tcp_sock (p'',fd) \<Rightarrow> if (p'' = p' \<and> fd \<in> fds) then user_of_obj s (O_tcp_sock (p, fd)) else if (p'' = p') then None else user_of_obj s obj | O_udp_sock (p'',fd) \<Rightarrow> if (p'' = p' \<and> fd \<in> fds) then user_of_obj s (O_udp_sock (p, fd)) else if (p'' = p') then None else user_of_obj s obj | _ \<Rightarrow> user_of_obj s obj)"| "user_of_obj (Open p f flags fd iopt # s) = (case iopt of None \<Rightarrow> (user_of_obj s) ((O_fd p fd) := user_of_obj s (O_proc p)) | _ \<Rightarrow> ((user_of_obj s) ((O_fd p fd) := user_of_obj s (O_proc p))) ((O_file f) := user_of_obj s (O_proc p)))"| "user_of_obj (Mkdir p f inum # s) = (user_of_obj s) ((O_dir f) := user_of_obj s (O_proc p))"| "user_of_obj (LinkHard p f f' # s) = (user_of_obj s) ((O_file f') := user_of_obj s (O_proc p))"(*| "user_of_obj (Rename p f2 f3 # s) = (\<lambda> obj. case obj of O_file f \<Rightarrow> if (f3 \<preceq> f) then user_of_obj s (O_file (file_before_rename f2 f3 f)) else user_of_obj s obj | O_dir f \<Rightarrow> if (f3 \<preceq> f) then user_of_obj s (O_dir (file_before_rename f2 f3 f)) else user_of_obj s obj | _ \<Rightarrow> user_of_obj s obj)"*)| "user_of_obj (CreateMsgq p q # s) = (user_of_obj s) ((O_msgq q) := user_of_obj s (O_proc p))" | "user_of_obj (SendMsg p q m # s) = (user_of_obj s) ((O_msg q m) := user_of_obj s (O_proc p))"| "user_of_obj (CreateShM p h # s) = (user_of_obj s) ((O_shm h) := user_of_obj s (O_proc p))"| "user_of_obj (CreateSock p af st fd inum # s) = (\<lambda> obj. case obj of O_fd p' fd' \<Rightarrow> if (p' = p \<and> fd' = fd) then user_of_obj s (O_proc p) else user_of_obj s obj | O_tcp_sock (p', fd') \<Rightarrow> if (p' = p \<and> fd' = fd \<and> st = STREAM) then user_of_obj s (O_proc p) else user_of_obj s obj | O_udp_sock (p', fd') \<Rightarrow> if (p' = p \<and> fd' = fd \<and> st = DGRAM) then user_of_obj s (O_proc p) else user_of_obj s obj | _ \<Rightarrow> user_of_obj s obj )"| "user_of_obj (Accept p fd addr port fd' inum # s) = (\<lambda> obj. case obj of O_fd p' fd'' \<Rightarrow> if (p' = p \<and> fd'' = fd') then user_of_obj s (O_proc p) else user_of_obj s obj | O_tcp_sock (p', fd'') \<Rightarrow> if (p' = p \<and> fd'' = fd') then user_of_obj s (O_proc p) else user_of_obj s obj | _ \<Rightarrow> user_of_obj s obj )"| "user_of_obj (_ # s) = user_of_obj s"fun type_of_obj :: "t_state \<Rightarrow> (t_object \<Rightarrow> type_t option)"where "type_of_obj [] = init_type_of_obj"| "type_of_obj (Clone p p' fds shms # s) = (\<lambda> obj. case obj of O_proc p'' \<Rightarrow> if (p'' = p') then type_of_obj s (O_proc p) else type_of_obj s obj | O_fd p'' fd \<Rightarrow> if (p'' = p' \<and> fd \<in> fds) then type_of_obj s (O_fd p fd) else if (p'' = p') then None else type_of_obj s obj | O_tcp_sock (p'', fd) \<Rightarrow> if (p'' = p' \<and> fd \<in> fds) then type_of_obj s (O_tcp_sock (p, fd)) else if (p'' = p') then None else type_of_obj s obj | O_udp_sock (p'', fd) \<Rightarrow> if (p'' = p' \<and> fd \<in> fds) then type_of_obj s (O_udp_sock (p, fd)) else if (p'' = p') then None else type_of_obj s obj | _ \<Rightarrow> type_of_obj s obj )"| "type_of_obj (Execve p f fds # s) = (type_of_obj s) ((O_proc p) := (case (type_of_obj s (O_proc p), type_of_obj s (O_file f)) of (Some tp, Some tf) \<Rightarrow> Some (type_transition tp tf C_process False) | _ \<Rightarrow> None) )"| "type_of_obj (Open p f flags fd (Some inum) # s) = ((type_of_obj s) ((O_file f) := (case (parent f) of Some pf \<Rightarrow> (case (type_of_obj s (O_proc p), type_of_obj s (O_dir pf)) of (Some tp, Some tpf) \<Rightarrow> Some (type_transition tp tpf C_file True) | _ \<Rightarrow> None) | _ \<Rightarrow> None) )) ((O_fd p fd) := type_of_obj s (O_proc p))"| "type_of_obj (Open p f flags fd None # s) = (type_of_obj s) ((O_fd p fd) := type_of_obj s (O_proc p))"| "type_of_obj (Mkdir p f inum # s) = (type_of_obj s) ((O_dir f) := (case (parent f) of Some pf \<Rightarrow> (case (type_of_obj s (O_proc p), type_of_obj s (O_dir pf)) of (Some tp, Some tpf) \<Rightarrow> Some (type_transition tp tpf C_dir True) | _ \<Rightarrow> None) | _ \<Rightarrow> None) )"| "type_of_obj (LinkHard p f f' # s) = (type_of_obj s) ((O_file f') := (case (parent f') of Some pf \<Rightarrow> (case (type_of_obj s (O_proc p), type_of_obj s (O_dir pf)) of (Some tp, Some tpf) \<Rightarrow> Some (type_transition tp tpf C_file True) | _ \<Rightarrow> None) | _ \<Rightarrow> None) )"(*| "type_of_obj (Rename p f f' # s) = (\<lambda> obj. case obj of O_file f'' \<Rightarrow> (if (f' \<preceq> f'') then type_of_obj s (O_file (file_before_rename f f' f'')) else type_of_obj s (O_file f'')) | O_dir f'' \<Rightarrow> (if (f' \<preceq> f'') then type_of_obj s (O_file (file_before_rename f f' f'')) else type_of_obj s (O_file f'')) | _ \<Rightarrow> type_of_obj s obj )"*)| "type_of_obj (CreateMsgq p q # s) = (type_of_obj s) ((O_msgq q) := (case (type_of_obj s (O_proc p)) of Some tp \<Rightarrow> Some tp | _ \<Rightarrow> None) )"| "type_of_obj (SendMsg p q m # s) = (type_of_obj s) ((O_msg q m) := (case (type_of_obj s (O_proc p), type_of_obj s (O_msgq q)) of (Some tp, Some tq) \<Rightarrow> Some (type_transition tp tq C_msg False) | _ \<Rightarrow> None) )"| "type_of_obj (CreateShM p h # s) = (type_of_obj s) ((O_shm h) := (case (type_of_obj s (O_proc p)) of Some tp \<Rightarrow> Some tp | _ \<Rightarrow> None) )"| "type_of_obj (CreateSock p af st fd inum # s) = (\<lambda> obj. case obj of O_fd p' fd' \<Rightarrow> if (p' = p \<and> fd' = fd) then type_of_obj s (O_proc p) else type_of_obj s obj | O_tcp_sock (p', fd') \<Rightarrow> if (p' = p \<and> fd' = fd \<and> st = STREAM) then type_of_obj s (O_proc p) else type_of_obj s obj | O_udp_sock (p', fd') \<Rightarrow> if (p' = p \<and> fd' = fd \<and> st = DGRAM) then type_of_obj s (O_proc p) else type_of_obj s obj | _ \<Rightarrow> type_of_obj s obj )"| "type_of_obj (Accept p fd addr port fd' inum # s) = (\<lambda> obj. case obj of O_fd p' fd'' \<Rightarrow> if (p' = p \<and> fd'' = fd') then type_of_obj s (O_proc p) else type_of_obj s obj | O_tcp_sock (p', fd'') \<Rightarrow> if (p' = p \<and> fd'' = fd') then type_of_obj s (O_proc p) else type_of_obj s obj | _ \<Rightarrow> type_of_obj s obj )"| "type_of_obj (_ # s) = type_of_obj s"fun role_of_proc :: "t_state \<Rightarrow> (t_process \<Rightarrow> role_t option)"where "role_of_proc [] = init_role_of_proc"| "role_of_proc (Clone p p' fds shms # s) = (role_of_proc s) (p' := role_of_proc s p)"| "role_of_proc (Execve p f fds # s) = (role_of_proc s) (p := (case (role_of_proc s p, type_of_obj s (O_file f)) of (Some r, Some ft) \<Rightarrow> role_transition r ft | _ \<Rightarrow> None) )"| "role_of_proc (_ # s) = role_of_proc s"fun role_of_obj :: "t_state \<Rightarrow> t_object \<Rightarrow> role_t option"where "role_of_obj s (O_proc p) = role_of_proc s p"| "role_of_obj s _ = Some R_object" (* object_r *)definition sectxt_of_obj :: "t_state \<Rightarrow> t_object \<Rightarrow> security_context_t option"where "sectxt_of_obj s obj = ( case (user_of_obj s obj, role_of_obj s obj, type_of_obj s obj) of (Some u, Some r, Some t) \<Rightarrow> Some (u, r, t) | _ \<Rightarrow> None)"fun init_role_of_obj :: "t_object \<Rightarrow> role_t option"where "init_role_of_obj (O_proc p) = init_role_of_proc p"| "init_role_of_obj _ = Some R_object"definition init_sectxt_of_obj :: "t_object \<Rightarrow> security_context_t option"where "init_sectxt_of_obj obj \<equiv> (case (init_user_of_obj obj, init_role_of_obj obj, init_type_of_obj obj) of (Some u, Some r, Some t) \<Rightarrow> Some (u,r,t) | _ \<Rightarrow> None)"definition sec_of_root :: "security_context_t"where "sec_of_root \<equiv> (case (init_user_of_obj (O_dir []), init_type_of_obj (O_dir [])) of (Some u, Some t) \<Rightarrow> (u, R_object, t))"(******* flask granting ******** * involves three kinds of rules: * 1. allow rule of types, allowed_rule_list_t, main * 2. allow rule of roles, role_allow_rule_list_t, mainly for execve call * 3. constrains, section 3.4.5, user-specifically defined. * Passed all these 3, then grant Yes, else No *) definition search_check_allp :: "security_context_t \<Rightarrow> security_context_t set \<Rightarrow> bool"where "search_check_allp pctxt sectxts = (\<forall> sec \<in> sectxts. permission_check pctxt sec C_dir P_search)"definition search_check_file :: "security_context_t \<Rightarrow> security_context_t \<Rightarrow> bool"where "search_check_file sctxt fctxt \<equiv> permission_check sctxt fctxt C_file P_search"definition search_check_dir :: "security_context_t \<Rightarrow> security_context_t \<Rightarrow> bool"where "search_check_dir sctxt fctxt \<equiv> permission_check sctxt fctxt C_dir P_search"fun get_parentfs_ctxts :: "t_state \<Rightarrow> t_file \<Rightarrow> (security_context_t list) option"where "get_parentfs_ctxts s [] = (case (sectxt_of_obj s (O_dir [])) of Some ctxt \<Rightarrow> Some [ctxt] | _ \<Rightarrow> None)"| "get_parentfs_ctxts s (f#pf) = (case (get_parentfs_ctxts s pf, sectxt_of_obj s (O_dir (f#pf))) of (Some ctxts, Some ctxt) \<Rightarrow> Some (ctxt#ctxts) | _ \<Rightarrow> None)"fun search_check :: "t_state \<Rightarrow> security_context_t \<Rightarrow> t_file \<Rightarrow> bool"where "search_check s pctxt [] = (case (sectxt_of_obj s (O_dir [])) of Some fctxt \<Rightarrow> search_check_dir pctxt fctxt | _ \<Rightarrow> False)"| "search_check s pctxt (f#pf) = (if (is_file s (f#pf)) then (case (sectxt_of_obj s (O_file (f#pf)), get_parentfs_ctxts s pf) of (Some fctxt, Some pfctxts) \<Rightarrow> (search_check_file pctxt fctxt \<and> search_check_allp pctxt (set pfctxts)) | _ \<Rightarrow> False) else (case (sectxt_of_obj s (O_dir (f#pf)), get_parentfs_ctxts s pf) of (Some fctxt, Some pfctxts) \<Rightarrow> (search_check_dir pctxt fctxt \<and> search_check_allp pctxt (set pfctxts)) | _ \<Rightarrow> False))"(* this means we should prove every current fd has a security context! *)definition sectxts_of_fds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd set \<Rightarrow> security_context_t set"where "sectxts_of_fds s p fds \<equiv> {ctxt. \<exists> fd \<in> fds. sectxt_of_obj s (O_fd p fd) = Some ctxt}"definition inherit_fds_check :: "t_state \<Rightarrow> security_context_t \<Rightarrow> t_process \<Rightarrow> t_fd set \<Rightarrow> bool"where "inherit_fds_check s npsectxt p fds \<equiv> (\<forall> ctxt \<in> sectxts_of_fds s p fds. permission_check npsectxt ctxt C_fd P_inherit)"fun npctxt_execve :: "security_context_t \<Rightarrow> security_context_t \<Rightarrow> security_context_t option"where "npctxt_execve (pu,pr,pt) (fu,fr,ft) = (case (role_transition pr ft) of Some nr \<Rightarrow> Some (pu, nr, type_transition pt ft C_process False) | _ \<Rightarrow> None)"fun nfctxt_create :: "security_context_t \<Rightarrow> security_context_t \<Rightarrow> security_class_t \<Rightarrow> security_context_t"where "nfctxt_create (pu,pr,pt) (fu,fr,ft) cls = (pu, R_object, type_transition pt ft cls True)"fun grant_execve :: "security_context_t \<Rightarrow> security_context_t \<Rightarrow> security_context_t \<Rightarrow> bool"where "grant_execve (up,rp,tp) (uf,rf,tf) (up',nr,nt) = (role_decl_check nr nt \<and> role_allow rp nr \<and> permission_check (up,rp,tp) (uf,rf,tf) C_file P_execute \<and> permission_check (up,nr,nt) (uf,rf,tf) C_file P_entrypoint \<and> permission_check (up,rp,tp) (up,nr,nt) C_process P_transition \<and> permission_check (up,nr,nt) (uf,rf,tf) C_process P_execute)"definition sectxts_of_shms :: "t_state \<Rightarrow> t_shm set \<Rightarrow> security_context_t set"where "sectxts_of_shms s shms \<equiv> {ctxt. \<exists> h \<in> shms. sectxt_of_obj s (O_shm h) = Some ctxt}"definition inherit_shms_check :: "t_state \<Rightarrow> security_context_t \<Rightarrow> t_shm set \<Rightarrow> bool"where "inherit_shms_check s npsectxt shms \<equiv> (\<forall> ctxt \<in> sectxts_of_shms s shms. permission_check npsectxt ctxt C_shm P_inherit)"fun perm_of_mflag :: "t_open_must_flag \<Rightarrow> permission_t set"where "perm_of_mflag OF_RDONLY = {P_read}"| "perm_of_mflag OF_WRONLY = {P_write}"| "perm_of_mflag OF_RDWR = {P_read, P_write}"definition perm_of_oflag :: "t_open_option_flag set \<Rightarrow> permission_t set"where "perm_of_oflag oflags \<equiv> (case (OF_APPEND \<in> oflags, OF_CREAT \<in> oflags) of (True, True) \<Rightarrow> {P_append, P_create} | (True, _ ) \<Rightarrow> {P_append} | (_ , True) \<Rightarrow> {P_create} | _ \<Rightarrow> {})"definition perms_of_flags :: "t_open_flags \<Rightarrow> permission_t set"where "perms_of_flags flags \<equiv> (case flags of (mflag,oflags) \<Rightarrow> (perm_of_mflag mflag \<union> perm_of_oflag oflags))"(*definition class_of_flags :: "t_open_flags \<Rightarrow> security_class_t"where "class_of_flags flags \<equiv> (case flags of (mflag, oflags) \<Rightarrow> if (OF_DIRECTORY \<in> oflags) then C_dir else C_file)"definition obj_of_flags :: "t_open_flags \<Rightarrow> t_file \<Rightarrow> t_object"where "obj_of_flags flags f \<equiv> (case flags of (mflag, oflags) \<Rightarrow> if (OF_DIRECTORY \<in> oflags) then O_dir f else O_file f)"*)definition oflags_check :: "t_open_flags \<Rightarrow> security_context_t \<Rightarrow> security_context_t \<Rightarrow> bool"where "oflags_check flags pctxt fctxt \<equiv> \<forall> perm \<in> (perms_of_flags flags). permission_check pctxt fctxt C_file perm"fun grant :: "t_state \<Rightarrow> t_event \<Rightarrow> bool"where "grant s (Execve p f fds) = (case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_file f)) of (Some (up, rp, tp), Some (uf, rf, tf)) \<Rightarrow> (case (npctxt_execve (up,rp,tp) (uf,rf,tf)) of Some (pu,nr,nt) \<Rightarrow> ( search_check s (up,rp,tp) f \<and> grant_execve (up,rp,tp) (uf,rf,tf) (up,nr,nt) \<and> inherit_fds_check s (up,nr,nt) p fds) | _ \<Rightarrow> False) | _ \<Rightarrow> False )"| "grant s (Clone p p' fds shms) = (case (sectxt_of_obj s (O_proc p)) of Some (up, rp, tp) \<Rightarrow> (permission_check (up,rp,tp) (up,rp,tp) C_process P_fork \<and> inherit_fds_check s (up,rp,tp) p fds \<and> inherit_shms_check s (up,rp,tp) shms) | _ \<Rightarrow> False )"| "grant s (Kill p p') = (case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_proc p')) of (Some (su,sr,st), Some (tu,tr,tt)) \<Rightarrow> permission_check (su,sr,st) (tu,tr,tt) C_process P_sigkill | _ \<Rightarrow> False)"| "grant s (Ptrace p p') = (case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_proc p')) of (Some (su,sr,st), Some (tu,tr,tt)) \<Rightarrow> permission_check (su,sr,st) (tu,tr,tt) C_process P_ptrace | _ \<Rightarrow> False)"| "grant s (Exit p) = True"| "grant s (Open p f flags fd None) = (case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_file f)) of (Some (pu,pr,pt), Some (fu,fr,ft)) \<Rightarrow> search_check s (pu,pr,pt) f \<and> oflags_check flags (pu,pr,pt) (fu,fr,ft) \<and> permission_check (pu,pr,pt) (pu,pr,pt) C_fd P_setattr | _ \<Rightarrow>False)"| "grant s (Open p f flags fd (Some inum)) = (case (parent f) of Some pf \<Rightarrow> (case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_dir pf)) of (Some (pu,pr,pt), Some (pfu,pfr,pft)) \<Rightarrow> (search_check s (pu,pr,pt) pf \<and> oflags_check flags (pu,pr,pt) (nfctxt_create (pu,pr,pt) (pfu,pfr,pft) C_file) \<and> permission_check (pu,pr,pt) (pfu,pfr,pft) C_dir P_add_name \<and> permission_check (pu,pr,pt) (pu,pr,pt) C_fd P_setattr) | _ \<Rightarrow> False) | _ \<Rightarrow> False)"| "grant s (ReadFile p fd) = (case (file_of_proc_fd s p fd) of Some f \<Rightarrow> (case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_fd p fd), sectxt_of_obj s (O_file f)) of (Some (pu,pr,pt), Some (fdu,fdr,fdt), Some (fu,fr,ft)) \<Rightarrow> (permission_check (pu,pr,pt) (fdu,fdr,fdt) C_fd P_setattr \<and> permission_check (pu,pr,pt) (fu,fr,ft) C_file P_read) | _ \<Rightarrow> False) | _ \<Rightarrow> False)"| "grant s (WriteFile p fd) = (case (file_of_proc_fd s p fd) of Some f \<Rightarrow> (case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_fd p fd), sectxt_of_obj s (O_file f)) of (Some (pu,pr,pt), Some (fdu,fdr,fdt), Some (fu,fr,ft)) \<Rightarrow> (permission_check (pu,pr,pt) (fdu,fdr,fdt) C_fd P_setattr \<and> permission_check (pu,pr,pt) (fu,fr,ft) C_file P_write) | _ \<Rightarrow> False) | _ \<Rightarrow> False)" | "grant s (CloseFd p fd) = True"| "grant s (UnLink p f) = (case (parent f) of Some pf \<Rightarrow> (case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_dir pf), sectxt_of_obj s (O_file f)) of (Some (pu,pr,pt), Some (du,dr,dt), Some (fu,fr,ft)) \<Rightarrow> (search_check s (pu,pr,pt) f \<and> permission_check (pu,pr,pt) (fu,fr,ft) C_file P_unlink \<and> permission_check (pu,pr,pt) (du,dr,dt) C_dir P_remove_name) | _ \<Rightarrow> False) | _ \<Rightarrow> False)"| "grant s (Rmdir p f) = (case (parent f) of Some pf \<Rightarrow> (case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_dir pf), sectxt_of_obj s (O_dir f)) of (Some (pu,pr,pt), Some (du,dr,dt), Some (fu,fr,ft)) \<Rightarrow> (search_check s (pu,pr,pt) f \<and> permission_check (pu,pr,pt) (fu,fr,ft) C_dir P_rmdir \<and> permission_check (pu,pr,pt) (du,dr,dt) C_dir P_remove_name) | _ \<Rightarrow> False) | _ \<Rightarrow> False)"| "grant s (Mkdir p f inum) = (case (parent f) of Some pf \<Rightarrow> (case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_dir pf)) of (Some (pu,pr,pt), Some (du,dr,dt)) \<Rightarrow> (search_check s (pu,pr,pt) f \<and> permission_check (pu,pr,pt) (nfctxt_create (pu,pr,pt) (du,dr,dt) C_dir) C_dir P_create \<and> permission_check (pu,pr,pt) (du,dr,dt) C_dir P_add_name) | _ \<Rightarrow> False) | _ \<Rightarrow> False)"| "grant s (LinkHard p f f') = (case (parent f') of Some pf \<Rightarrow> (case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_dir pf), sectxt_of_obj s (O_file f)) of (Some (pu,pr,pt), Some (du,dr,dt), Some (fu,fr,ft)) \<Rightarrow> (search_check s (pu,pr,pt) f \<and> search_check s (pu,pr,pt) pf \<and> permission_check (pu,pr,pt) (fu,fr,ft) C_file P_link \<and> permission_check (pu,pr,pt) (du,dr,dt) C_dir P_add_name) | _ \<Rightarrow> False) | _ \<Rightarrow> False)"| "grant s (Truncate p f len) = (case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_file f)) of (Some (pu,pr,pt), Some (fu,fr,ft)) \<Rightarrow> (search_check s (pu,pr,pt) f \<and> permission_check (pu,pr,pt) (fu,fr,ft) C_file P_setattr) | _ \<Rightarrow> False)"(*| "grant s (Rename p f f') = (case (parent f, parent f') of (Some pf, Some pf') \<Rightarrow> (case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_dir pf), sectxt_of_obj s (O_file f), sectxt_of_obj s (O_dir pf')) of (Some (pu,pr,pt), Some (pfu,pfr,pft), Some (fu,fr,ft), Some (pfu',pfr',pft')) \<Rightarrow> (search_check s (pu,pr,pt) f \<and> permission_check (pu,pr,pt) (pfu,pfr,pft) C_dir P_remove_name \<and> (if (is_file s f) then permission_check (pu,pr,pt) (fu,fr,ft) C_file P_rename else permission_check (pu,pr,pt) (fu,fr,ft) C_dir P_reparent) \<and> search_check s (pu,pr,pt) pf' \<and> permission_check (pu,pr,pt) (pfu',pfr',pft') C_dir P_add_name) | _ \<Rightarrow> False) | _ \<Rightarrow> False)"*)| "grant s (CreateMsgq p q) = (case (sectxt_of_obj s (O_proc p)) of Some (pu,pr,pt) \<Rightarrow> (permission_check (pu,pr,pt) (pu,pr,pt) C_msgq P_associate \<and> permission_check (pu,pr,pt) (pu,pr,pt) C_msgq P_create) | _ \<Rightarrow> False)"| "grant s (SendMsg p q m) = (case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_msgq q)) of (Some (pu,pr,pt), Some (qu,qr,qt)) \<Rightarrow> (permission_check (pu,pr,pt) (qu,qr,qt) C_msgq P_enqueue \<and> permission_check (pu,pr,pt) (qu,qr,qt) C_msgq P_write \<and> permission_check (pu,pr,pt) (pu,pr,pt) C_msg P_send) | _ \<Rightarrow> False)"| "grant s (RecvMsg p q m) = (case (sectxt_of_obj s (O_proc p),sectxt_of_obj s (O_msgq q),sectxt_of_obj s (O_msg q m)) of (Some (pu,pr,pt), Some (qu,qr,qt), Some (mu,mr,mt)) \<Rightarrow> permission_check (pu,pr,pt) (qu,qr,qt) C_msgq P_read \<and> permission_check (pu,pr,pt) (mu,mr,mt) C_msg P_receive | _ \<Rightarrow> False)"| "grant s (RemoveMsgq p q) = (case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_msgq q)) of (Some (pu,pr,pt), Some (qu,qr,qt)) \<Rightarrow> permission_check (pu,pr,pt) (qu,qr,qt) C_msgq P_destroy | _ \<Rightarrow> False)"| "grant s (CreateShM p h) = (case (sectxt_of_obj s (O_proc p)) of Some (pu,pr,pt) \<Rightarrow> (permission_check (pu,pr,pt) (pu,pr,pt) C_shm P_associate \<and> permission_check (pu,pr,pt) (pu,pr,pt) C_shm P_create) | _ \<Rightarrow> False)"| "grant s (Attach p h flag) = (case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_shm h)) of (Some (pu,pr,pt), Some (hu,hr,ht)) \<Rightarrow> if flag = SHM_RDONLY then permission_check (pu,pr,pt) (hu,hr,ht) C_shm P_read else permission_check (pu,pr,pt) (hu,hr,ht) C_shm P_read \<and> permission_check (pu,pr,pt) (hu,hr,ht) C_shm P_write | _ \<Rightarrow> False)"| "grant s (Detach p h) = True" (*?*)| "grant s (DeleteShM p h) = (case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_shm h)) of (Some (pu,pr,pt), Some (hu,hr,ht)) \<Rightarrow> permission_check (pu,pr,pt) (hu,hr,ht) C_shm P_destroy | _ \<Rightarrow> False)"| "grant s _ = False" (* socket event is currently not in consideration *)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 *)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_dir f) = (f \<in> init_files)"*)| "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 usefun no_del_event:: "t_event list \<Rightarrow> bool"where "no_del_event [] = True"| "no_del_event (Kill p p' # \<tau>) = False"| "no_del_event (CloseFd p fd # \<tau>) = False"| "no_del_event (UnLink p f # \<tau>) = False"| "no_del_event (Rmdir p f # \<tau>) = False"(*| "no_del_event (Rename p f f' # \<tau>) = False"*)| "no_del_event (RemoveMsgq p q # \<tau>) = False"| "no_del_event (RecvMsg p q m # \<tau>) = False"| "no_del_event (_ # \<tau>) = no_del_event \<tau>"*)endlocale tainting = flask + fixes seeds :: "t_object set"assumes seeds_in_init: "\<And> obj. obj \<in> seeds \<Longrightarrow> tobj_in_init obj" and same_inode_in_seeds: "\<And> f f'. \<lbrakk>O_file f \<in> seeds; has_same_inode [] f f'\<rbrakk> \<Longrightarrow> O_file f' \<in> seeds" and flow_shm_in_seeds: "\<And> p p'. \<lbrakk>O_proc p \<in> seeds; info_flow_shm [] p p'\<rbrakk> \<Longrightarrow> O_proc p' \<in> seeds"begininductive tainted :: "t_object \<Rightarrow> t_state \<Rightarrow> bool" ("_ \<in> tainted _" [100, 100] 100)where t_init: "obj \<in> seeds \<Longrightarrow> obj \<in> tainted []"| t_clone: "\<lbrakk>O_proc p \<in> tainted s; valid (Clone p p' fds shms # s)\<rbrakk> \<Longrightarrow> O_proc p' \<in> tainted (Clone p p' fds shms # s)"| t_execve: "\<lbrakk>O_file f \<in> tainted s; valid (Execve p f fds # s)\<rbrakk> \<Longrightarrow> O_proc p \<in> tainted (Execve p f fds # s)"| t_ptrace: "\<lbrakk>O_proc p \<in> tainted s; valid (Ptrace p p' # s); info_flow_shm s p' p''\<rbrakk> \<Longrightarrow> O_proc p'' \<in> tainted (Ptrace p p' # s)"| t_ptrace':"\<lbrakk>O_proc p' \<in> tainted s; valid (Ptrace p p' # s); info_flow_shm s p p''\<rbrakk> \<Longrightarrow> O_proc p'' \<in> tainted (Ptrace p p' # s)"| t_cfile: "\<lbrakk>O_proc p \<in> tainted s; valid (Open p f flags fd (Some inum) # s)\<rbrakk> \<Longrightarrow> O_file f \<in> tainted (Open p f flags fd (Some inum) # s)"| t_read: "\<lbrakk>O_file f \<in> tainted s; valid (ReadFile p fd # s); file_of_proc_fd s p fd = Some f; info_flow_shm s p p'\<rbrakk> \<Longrightarrow> O_proc p' \<in> tainted (ReadFile p fd # s)"| t_write: "\<lbrakk>O_proc p \<in> tainted s; valid (WriteFile p fd # s); file_of_proc_fd s p fd = Some f; has_same_inode s f f'\<rbrakk> \<Longrightarrow> O_file f' \<in> tainted (WriteFile p fd # s)"(* directory is not tainted | t_mkdir: "\<lbrakk>O_proc p \<in> tainted s; valid (Mkdir p f inum # s)\<rbrakk> \<Longrightarrow> O_dir f \<in> tainted (Mkdir p f inum # s)" *)| t_link: "\<lbrakk>O_file f \<in> tainted s; valid (LinkHard p f f' # s)\<rbrakk> \<Longrightarrow> O_file f' \<in> tainted (LinkHard p f f' # s)"| t_trunc: "\<lbrakk>O_proc p \<in> tainted s; valid (Truncate p f len # s); len > 0; has_same_inode s f f'\<rbrakk> \<Longrightarrow> O_file f' \<in> tainted (Truncate p f len # s)"(*| t_rename: "\<lbrakk>O_file f'' \<in> tainted s; valid (Rename p f f' # s);f \<preceq> f''\<rbrakk> \<Longrightarrow> O_file (file_after_rename f f' f'') \<in> tainted (Rename p f f' # s)"| t_rename':"\<lbrakk>O_dir f'' \<in> tainted s; valid (Rename p f f' # s);f \<preceq> f''\<rbrakk> \<Longrightarrow> O_dir (file_after_rename f f' f'') \<in> tainted (Rename p f f' # s)"*)| t_sendmsg:"\<lbrakk>O_proc p \<in> tainted s; valid (SendMsg p q m # s)\<rbrakk> \<Longrightarrow> O_msg q m \<in> tainted (SendMsg p q m # s)"| t_recvmsg:"\<lbrakk>O_msg q m \<in> tainted s; valid (RecvMsg p q m # s); info_flow_shm s p p'\<rbrakk> \<Longrightarrow> O_proc p' \<in> tainted (RecvMsg p q m # s)"| t_remain: "\<lbrakk>obj \<in> tainted s; valid (e # s); alive (e # s) obj\<rbrakk> \<Longrightarrow> obj \<in> tainted (e # s)"definition taintable:: "t_object \<Rightarrow> bool"where "taintable obj \<equiv> init_alive obj \<and> (\<exists> s. obj \<in> tainted s)"definition undeletable :: "t_object \<Rightarrow> bool"where "undeletable obj \<equiv> init_alive obj \<and> \<not> (\<exists> s. valid s \<and> deleted obj s)"endend