theory Flask_typeimports Mainbegin(************* 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, aswe 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_devlogtype_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