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