diff -r 34d01e9a772e -r 7d9c0ed02b56 Flask_type.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Flask_type.thy Fri May 03 08:20:21 2013 +0100 @@ -0,0 +1,239 @@ +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 \ executable; file \ 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 \ type_t patt \ security_class_t \ 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 \ type_t patt \ security_class_t \ 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 \ type_t patt \ security_class_t \ 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 \ (type_t patt) target_with_self_t \ security_class_t \ 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 \ 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 \ type_t \ 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 \ 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 \ role_t set)" + +type_synonym security_context_t = + "(user_t \ role_t \ 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 \ permission_t set \ (security_context_t \ security_context_t \ 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 \ security_id_t \ security_class_t \ access_vector_t) list" + + *) + +end \ No newline at end of file