theory Flask_type
imports Main
begin


(************* types that for modeling Access-Control part of Selinux *************)

(* Table 4-5 of "Selinux by example" *)
datatype permission_t = 
(* C_file *)
  P_append (* the O_append flag for open *)
| P_create (* create new file *)
| P_entrypoint (* file can be used as the entry point of new domain via a domain transition *)
(* | P_execmod  execute memory-mapped files that have modified *)
| P_execute (* corresponds to x access in standard linux *)
(* | P_execute_no_trans: execute file in calller's domain, without domain transition *)
(* | P_getattr :  stat, ls, ioctls, ... not-related to security *)
| P_link    (* create hard link to file *)
| P_read    (* corresponds to r access in standard linux *)
| P_rename  (* rename a hard link *)
| P_setattr (* chmod, ioctls ... *)
| P_unlink  (* remove hard link (delete *)
| P_write   (* corresponds to w access in standard linux *)
(* P_lock; P_mounton; P_quotaon; P_relabelfrom; P_relabelto *)

(* C_dir *)
| P_add_name (* add file in directory *)
| P_remove_name (* like write for file *)
| P_reparent (* like rename for file *)
| P_search   
| P_rmdir    (* like unlink for file *)

(* C_fd *)
(* P_create; P_getattr; P_setattr*)
| P_inherit (* inherit across execve,
we simplify that execve would pass all fds to new "process", but flask checks the inherit right, if denied the fd is closed. *) 
(* P_receive: ignored, ? I can find a reasonable explanation *)
  
(* C_process *)
| P_fork 
| P_ptrace
| P_transition
| P_share  (* allow state sharing for execve, clone: fds and ipc  
 * for clone, we might have two flags, share Fd and IPC
 * for execve, as default, fds are shared, IPCs are detached. 
 *   But fds not passed access-control are closed
 *)
(*| P_siginh:  inheritance of signal state, pending signals, this is not needed, as
we assume all signal are delivered instantly *)
(* P_rlimitnh : inheritance of resource limits *) 
(* P_dyntransition; P_execheap; P_execmem; P_execstack; get_attr : not security related;
 * P_getcap; P_getsched *)
| P_sigkill     (* signal *)

(* C_msgq, C_shm *)
| P_associate
| P_destroy 
| P_enqueue
| P_receive
| P_send
(* create, read, write *)

type_synonym access_vector_t = "permission_t set"

(************ Object Classes *************)
datatype security_class_t = 
  C_process

(* file-related object classes, 4.3.1 of Book *)
| C_file
| C_fd 
| C_dir   
(* C_blk file C_chr_file C_fifo_file C_filesystem C_lnk_file C_sock_file *)

(* network, 4.3.2, using only tcp/udp as a demonstration *)
| C_node    (* Host by IP address or range of addresses *)
| C_netif   (* network interface, eth0 *)
| C_tcp_socket 
| C_udp_socket 
(* netlink_socket unix_socket rawip_socket *)

(* IPCs, 4.3.3 *)
| C_msg  (* messages within a message queue *)
| C_msgq (* message queues *)
| C_shm  (* shared memory segment *)
(* C_semaphores: only for sync, not tainting related *)

(*other classes, 4.3.4*)
(* C_capability; C_security:security server;  *)
(* | C_system  the system itself *)

(********* TE rules **********
 * 1. type declaration rules
 * 2. type transition rules
 * 3. type member rules
 * 4. type change rules
 * 5. access vector rules
 * 6. cloning rules
 * 7. access vector assertions 
 *)

(* 1. type declaration rule *)
datatype type_t = 
  T_syslogd
| T_syslogd_exec
| T_devlog
  
type_synonym attribute_t = "type_t set"

(* for the asterisk/wildcard in the rules lists*)
datatype 'a patt = 
  Single "'a" 
| Set    "'a set"
| Tilde  "'a set"  (* complement *)
| Asterisk 

(* 2. type transition rule, applied only when: execve & createfile
 * (creating subj_type, related obj_typ, type class, default type) 
 * related obj_typ: proc \<rightarrow> executable; file \<rightarrow> parent-file 
 * if not in the list, use subj_type for proc and parent_type for file
 * if multiple in the list, use the first one (they use the last one, we can say our list is the rev of their list, for "lookup" is easy)
 * if using attributes, it can be transformed into the simple form of this list,
 now we use "patt" to deal with attributes
 *)
type_synonym type_transition_rule_list_t = 
  "(type_t patt \<times> type_t patt \<times> security_class_t \<times> type_t) list" 


(* for type member rules:
 * ?? I don't know the ideal yet, page 13 bottom of left column 
 *
type_synonym type_member_rule_list_t = 
  "(type_t patt \<times> type_t patt \<times> security_class_t \<times> type_t) list" 
 *)  

(* for type change rules (relabeling to diff security context):
 * ?? I don't know what's its meaning yet, page 13 up of the right column
 *
type_synonym type_change_rule_list_t = 
  "(type_t patt \<times> type_t patt \<times> security_class_t \<times> type_t) list"
 *)

datatype 'a target_with_self_t = 
  Not_self 'a
| Self
  
(* for access vector rules(verify a role-changed if allowed or not): 
 * Any role-changed should be verified by this list!
 * here we only do the allow rule, audit and notify rules are ignored 
 * (source type, target type, class, permissionS)
 * permissionS might be access_vector_t, which is already be model as a "set" of "pattern"
 * Self in the target type means this rule should be applied to the source process itself
 * if multiple, we search the whole list to mimic their "the union" ideal 
 *) 
type_synonym allowed_rule_list_t = 
  "(type_t patt \<times> (type_t patt) target_with_self_t \<times> security_class_t \<times> permission_t patt) list"

datatype role_t = 
  R_object
| R_user
| R_login

(* role declarations:
 * (r, ts): ts are the types/domains that can be associated with r
 *)
type_synonym role_declarations_list_t =
  "(role_t \<times> type_t set) list"

(* role transition rules(only happens when execve call): 
 * (r, t, r'): the process with role r executes a file with type t, its role will be changed to r'
 *)
type_synonym role_transition_rule_list_t = 
  "(role_t \<times> type_t \<times> role_t) list"
 
(* role allow rules:
 * (from_role, to_role) changes when "Execve" calls!
 *  What's the difference between this list and the role_transition_rule_list?
 *  It is: if a process execute a file, the new role will be determined by 
 *   role-transition, but this new role should be in role-allow(if not deny),
 *   and the new type should be compatible with the new role, which is checked
 *   by role-declarations(if not deny). 
 *)
type_synonym role_allow_rule_list_t = 
  "(role_t set \<times> role_t set) list"

datatype user_t = 
  U_system
| U_sds
| U_pal

(* user declarations:
 * (u, roles) roles are associated with user u
 * here MLS are not in consideration
 *)
type_synonym user_declarations_list_t = 
  "(user_t \<times> role_t set)"

type_synonym security_context_t = 
  "(user_t \<times> role_t \<times> type_t)"

(* constrains :
 * (classes, perms, expression) list
 * when flask do a permission check, constrains will fetch the 
 * associated two security-contexts (source & target), flask
 * makes sure that appling expression to these two contexts,
 * will get True. If False, deny the request. 
 *)
type_synonym constrains_list_t = 
  "(security_class_t set \<times> permission_t set \<times> (security_context_t \<Rightarrow> security_context_t \<Rightarrow> bool)) list"

(* comments: 
 * 1. sid is not needed, it is a run-time index for security-context, 
 *    what we do is policy-analysis, so no this "dynamic" sid as mid-ware;
 * 2. "seeds" of tainting cannot be solid objects in the initial states, 
      should be extended as a "condition/predicate" to describe the "seeds"
 *)

(* "temporary unused definitions :

datatype security_id_t = 
  SID  nat
| SECSID_NULL
| SECSID_WILD


(* this list mimic the action of "security_compute_av",
 * if in the list, means func returns "grant"
 * if not in, means "denied"
 * !!! this list is a "work result" of policy by selinux's 
 *  pre-processing func "security_compute_av"
 *  in my formalisation, this is not needed, cause the specification of 
 *  our "selinux" contains already the policy specification. 
 *  we can directly get the access-vector for sid/sectxt based on allow-rules & constrains
 *)
type_synonym avc_t = "(security_id_t \<times> security_id_t \<times> security_class_t \<times> access_vector_t) list"

 *)

end