--- /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 \<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
\ No newline at end of file