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