theory OS_type_def
imports Main Flask_type
begin
(****************************** os files ***************************)
datatype t_open_must_flag =
OF_RDONLY
| OF_WRONLY
| OF_RDWR
datatype t_open_option_flag =
OF_APPEND
| OF_CREAT
(*
| OF_TRUNC
*)
| OF_EXCL
(*
| OF_DIRECTORY
| OF_OTHER
*)
type_synonym t_open_flags = "t_open_must_flag \<times> t_open_option_flag set"
definition is_read_flag :: "t_open_flags \<Rightarrow> bool"
where
"is_read_flag flag \<equiv> let (mflag, oflag) = flag in (mflag = OF_RDONLY \<or> mflag = OF_RDWR)"
definition is_write_flag :: "t_open_flags \<Rightarrow> bool"
where
"is_write_flag flag \<equiv> let (mflag, oflag) = flag in (mflag = OF_WRONLY \<or> mflag = OF_RDWR)"
definition is_excl_flag :: "t_open_flags \<Rightarrow> bool"
where
"is_excl_flag flag \<equiv> let (mflag, oflag) = flag in (OF_EXCL \<in> oflag)"
definition is_creat_flag :: "t_open_flags \<Rightarrow> bool"
where
"is_creat_flag flag \<equiv> let (mflag, oflag) = flag in (OF_CREAT \<in> oflag)"
definition is_creat_excl_flag :: "t_open_flags \<Rightarrow> bool"
where
"is_creat_excl_flag flag \<equiv> let (mflag, oflag) = flag in (OF_CREAT \<in> oflag \<and> OF_EXCL \<in> oflag)"
(*
definition is_trunc_flag :: "t_open_flags \<Rightarrow> bool"
where
"is_trunc_flag flag \<equiv> let (mflag, oflag) = flag in (OF_TRUNC \<in> oflag \<and> is_write_flag flag)"
definition is_cloexec_flag :: "t_open_flags \<Rightarrow> bool"
where
"is_cloexec_flag flag \<equiv> let (mflag, oflag) = flag in (OF_CLOEXEC \<in> oflag)"
*)
definition is_append_flag :: "t_open_flags \<Rightarrow> bool"
where
"is_append_flag flag \<equiv> let (mflag, oflag) = flag in (OF_APPEND \<in> oflag)"
(*
definition is_dir_flag :: "t_open_flags \<Rightarrow> bool"
where
"is_dir_flag flag \<equiv> let (mflag, oflag) = flag in (OF_DIRECTORY \<in> oflag)"
*)
type_synonym t_fname = string
(* listing of file path:
* a#b#c:: b is a's parent and c is b's parent;
* [] represents the root file
*)
type_synonym t_file = "t_fname list"
type_synonym t_fd = "nat" (* given a fd, must has funs to tell its corresponding: "t_file \<times> t_open_flags \<times> t_inode" *)
(* need not consideration, for rdonly transfer virus too
datatype t_sharememo_flag =
SHM_RDONLY
| SHM_OTHER
type_synonym t_sharememo_flags = "t_sharememo_flag set"
*)
(****************************** os sockets ***************************)
datatype t_shutdown_how =
SHUT_RD
| SHUT_WR
| SHUT_RDWR
datatype t_zero_one =
Z
| O
type_synonym t_inet_addr = "t_zero_one list"
type_synonym t_socket_port = nat
type_synonym t_netif = string
(*
datatype t_socket_af =
AF_UNIX "t_file \<times> t_file"
| AF_INET "t_inet_addr \<times> t_socket_port \<times> t_inet_addr \<times> t_socket_port \<times> t_netdev"
*)
datatype t_socket_af =
(* AF_UNIX
| *)AF_INET
datatype t_socket_type =
STREAM
| DGRAM
datatype t_sock_addr =
INET_ADDR t_inet_addr t_socket_port(*
| UNIX_ADDR t_file*)
type_synonym t_node = t_inet_addr (* a endpoint in the netword *)
datatype t_sock_trans_state =
Trans_Recv
| Trans_Send
| Trans_RS
| Trans_No
datatype t_sock_state =
SS_create
| SS_bind
| SS_connect
| SS_listen
| SS_accepted
| SS_trans "t_sock_trans_state"
(****************************** os other IPCs ***************************)
datatype t_shm_attach_flag =
SHM_RDONLY
| SHM_RDWR
type_synonym t_shm = nat
(* message queue is indexed by a nat, in OS
* but logically it is a list, created as [], updated as a queue
* so, it type should not be nat, but a t_msg list
*)
type_synonym t_msgq = nat
(* a message of ID nat, but it has meaning under "in what message queue" *)
type_synonym t_msg = "nat"
(****************************** os inodes ***************************)
type_synonym t_inode_num = nat
(*
datatype t_sock_af =
Tag_AF_UNIX "(t_file option \<times> t_file option)" "t_socket_type"
| Tag_AF_INET "(t_inet_addr \<times> t_socket_port) option \<times> (t_inet_addr \<times> t_socket_port) option \<times> t_netdev option" "t_socket_type"
*)
datatype t_inode_tag =
Tag_FILE (* this inode is a file, and its file is: "t_file" :: no need to do that and another reason is link may add two or more files to the inode, so it should be a list, can the maintainment of this list is tough *)
| Tag_DIR (* do not contain chs anymore, for more infomation see svn log
"t_inode_num list" *) (* Tag_DIR inode number list: the inode number list of subchild files (direct son the file) , means: new created child file should add to this field. *)
| Tag_TCP_SOCK (* information below is turn to seperative listener functions
"(t_inet_addr \<times> t_socket_port) option \<times> (t_inet_addr \<times> t_socket_port) option \<times> t_netdev option" "t_socket_type" *)
| Tag_UDP_SOCK
(* type_synonym t_inode = "nat \<times> t_inode_tag" (* inode (id, tag) contains file internal id and directory tag attributes *)
// not needed any more: for inode num and its tag now are seperated by two funcs.
*)
type_synonym t_process = nat
type_synonym t_trunc_len = nat
type_synonym t_socket = "t_process \<times> t_fd"
(* each constructor is defined according to each security-class *)
datatype t_object =
O_proc "t_process"
| O_file "t_file"
| O_fd "t_process" "t_fd"
| O_dir "t_file"
| O_node "t_node"
| O_tcp_sock "t_socket"
| O_udp_sock "t_socket"
| O_shm "t_shm"
| O_msgq "t_msgq"
| O_msg "t_msgq" "t_msg"
(*
datatype t_tainted_obj =
TO_proc "t_process"
| TO_file "t_file"
| TO_msg "t_msgq" "t_msg"
*)
(* not needed anymore
datatype t_clone_share_flag =
| CF_share_ipc
| CF_share_fd
| CF_share_both
| CF_no_share *)
(* unformalised system calls:
* 1. process management
* 1.1 wait: nothing to do with tainting relation
* 1.2 getpriority/setpriority/getsched/setsched: nothing to do with security
* 1.3 getcap/setcap: "at this time that will not be done"
* 1.4 getpgid/setpgid: ...
*)
datatype t_event =
(* process management *)
(* trace can be done trough tags of cloning and execving, but I ignore this. *)
Execve "t_process" "t_file" "t_fd set"
(* | Uselib "t_process" "t_file" *)
| Clone "t_process" "t_process" "t_fd set" "t_shm set" (* "t_clone_share_flag" is not needed, as event should record the fds and shms that passed to childprocess *)
| Kill "t_process" "t_process"
| Ptrace "t_process" "t_process"
| Exit "t_process"
| Open "t_process" "t_file" "t_open_flags" "t_fd" "nat option" (* the last nat option : if create file, the is Some inode_num else None *)
| ReadFile "t_process" "t_fd"
| WriteFile "t_process" "t_fd"
(* | Sendfile "t_process" "t_fd" "t_fd"
can be modeled as readfile then writefile *)
| CloseFd "t_process" "t_fd"
| UnLink "t_process" "t_file"
| Rmdir "t_process" "t_file"
| Mkdir "t_process" "t_file" "nat" (* last nat: inode_num *)
| LinkHard "t_process" "t_file" "t_file"
| Truncate "t_process" "t_file" "t_trunc_len"
(* | FTruncate "t_process" "t_fd" "t_trunc_len" *)
(*
| Rename "t_process" "t_file" "t_file"
*)
(* the message is in the msgq, so we must build a cache(list)
* to store the unreceived msg yet. And the os_grant should
* check if a message queue is empty before RecvMsg.
*)
| CreateMsgq "t_process" "t_msgq"
| SendMsg "t_process" "t_msgq" "t_msg"
| RecvMsg "t_process" "t_msgq" "t_msg"
| RemoveMsgq "t_process" "t_msgq"
| CreateShM "t_process" "t_shm"
| Attach "t_process" "t_shm" "t_shm_attach_flag"
| Detach "t_process" "t_shm"
| DeleteShM "t_process" "t_shm"
| CreateSock "t_process" "t_socket_af" "t_socket_type" "t_fd" "nat" (* last nat: inode_num *)
| Bind "t_process" "t_fd" "t_sock_addr"
| Connect "t_process" "t_fd" "t_sock_addr"
| Listen "t_process" "t_fd"
| Accept "t_process" "t_fd" "t_sock_addr" "nat" "t_fd" "nat" (* addr: remote socket address; nat: port num; last nat: inode_num *)
| SendSock "t_process" "t_fd"
| RecvSock "t_process" "t_fd"
| Shutdown "t_process" "t_fd" "t_shutdown_how"
(* the state of the system is decided by the initial state and the event trace*)
type_synonym t_state = "t_event list"
end