diff -r 34d01e9a772e -r 7d9c0ed02b56 OS_type_def.thy --- /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 \ t_open_option_flag set" + +definition is_read_flag :: "t_open_flags \ bool" +where + "is_read_flag flag \ let (mflag, oflag) = flag in (mflag = OF_RDONLY \ mflag = OF_RDWR)" + +definition is_write_flag :: "t_open_flags \ bool" +where + "is_write_flag flag \ let (mflag, oflag) = flag in (mflag = OF_WRONLY \ mflag = OF_RDWR)" + +definition is_excl_flag :: "t_open_flags \ bool" +where + "is_excl_flag flag \ let (mflag, oflag) = flag in (OF_EXCL \ oflag)" + +definition is_creat_flag :: "t_open_flags \ bool" +where + "is_creat_flag flag \ let (mflag, oflag) = flag in (OF_CREAT \ oflag)" + +definition is_creat_excl_flag :: "t_open_flags \ bool" +where + "is_creat_excl_flag flag \ let (mflag, oflag) = flag in (OF_CREAT \ oflag \ OF_EXCL \ oflag)" +(* +definition is_trunc_flag :: "t_open_flags \ bool" +where + "is_trunc_flag flag \ let (mflag, oflag) = flag in (OF_TRUNC \ oflag \ is_write_flag flag)" + +definition is_cloexec_flag :: "t_open_flags \ bool" +where + "is_cloexec_flag flag \ let (mflag, oflag) = flag in (OF_CLOEXEC \ oflag)" +*) +definition is_append_flag :: "t_open_flags \ bool" +where + "is_append_flag flag \ let (mflag, oflag) = flag in (OF_APPEND \ oflag)" + +(* +definition is_dir_flag :: "t_open_flags \ bool" +where + "is_dir_flag flag \ let (mflag, oflag) = flag in (OF_DIRECTORY \ 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 \ t_open_flags \ 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 \ t_file" +| AF_INET "t_inet_addr \ t_socket_port \ t_inet_addr \ t_socket_port \ 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 \ t_file option)" "t_socket_type" +| Tag_AF_INET "(t_inet_addr \ t_socket_port) option \ (t_inet_addr \ t_socket_port) option \ 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 \ t_socket_port) option \ (t_inet_addr \ t_socket_port) option \ t_netdev option" "t_socket_type" *) +| Tag_UDP_SOCK + +(* type_synonym t_inode = "nat \ 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 \ 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