
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 \<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




