
diff -r 924ab7a4e7fa -r 271e9818b6f6 simple_selinux/Flask_type.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/simple_selinux/Flask_type.thy	Mon Dec 02 10:52:40 2013 +0800
@@ -0,0 +1,241 @@
+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




