--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/OS_type_def.thy Fri May 03 08:20:21 2013 +0100
@@ -0,0 +1,276 @@
+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
\ No newline at end of file