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