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