|
1 theory Flask_type |
|
2 imports Main |
|
3 begin |
|
4 |
|
5 |
|
6 (************* types that for modeling Access-Control part of Selinux *************) |
|
7 |
|
8 (* Table 4-5 of "Selinux by example" *) |
|
9 datatype permission_t = |
|
10 (* C_file *) |
|
11 P_append (* the O_append flag for open *) |
|
12 | P_create (* create new file *) |
|
13 | P_entrypoint (* file can be used as the entry point of new domain via a domain transition *) |
|
14 (* | P_execmod execute memory-mapped files that have modified *) |
|
15 | P_execute (* corresponds to x access in standard linux *) |
|
16 (* | P_execute_no_trans: execute file in calller's domain, without domain transition *) |
|
17 (* | P_getattr : stat, ls, ioctls, ... not-related to security *) |
|
18 (*| P_link (* create hard link to file *) *) |
|
19 | P_read (* corresponds to r access in standard linux *) |
|
20 | P_rename (* rename a hard link *) |
|
21 | P_setattr (* chmod, ioctls ... *) |
|
22 | P_unlink (* remove hard link (delete *) |
|
23 | P_write (* corresponds to w access in standard linux *) |
|
24 (* P_lock; P_mounton; P_quotaon; P_relabelfrom; P_relabelto *) |
|
25 |
|
26 (* C_dir *) |
|
27 | P_add_name (* add file in directory *) |
|
28 | P_remove_name (* like write for file *) |
|
29 (* |
|
30 | P_reparent (* like rename for file *) *) |
|
31 | P_search |
|
32 | P_rmdir (* like unlink for file *) |
|
33 |
|
34 (* C_fd *) |
|
35 (* P_create; P_getattr; P_setattr*) |
|
36 | P_inherit (* inherit across execve, |
|
37 we simplify that execve would pass all fds to new "process", but flask checks the inherit right, if denied the fd is closed. *) |
|
38 (* P_receive: ignored, ? I can find a reasonable explanation *) |
|
39 |
|
40 (* C_process *) |
|
41 | P_fork |
|
42 | P_ptrace |
|
43 | P_transition |
|
44 | P_share (* allow state sharing for execve, clone: fds and ipc |
|
45 * for clone, we might have two flags, share Fd and IPC |
|
46 * for execve, as default, fds are shared, IPCs are detached. |
|
47 * But fds not passed access-control are closed |
|
48 *) |
|
49 (*| P_siginh: inheritance of signal state, pending signals, this is not needed, as |
|
50 we assume all signal are delivered instantly *) |
|
51 (* P_rlimitnh : inheritance of resource limits *) |
|
52 (* P_dyntransition; P_execheap; P_execmem; P_execstack; get_attr : not security related; |
|
53 * P_getcap; P_getsched *) |
|
54 | P_sigkill (* signal *) |
|
55 |
|
56 (* C_msgq, C_shm *) |
|
57 | P_associate |
|
58 | P_destroy |
|
59 | P_enqueue |
|
60 | P_receive |
|
61 | P_send |
|
62 (* create, read, write *) |
|
63 |
|
64 type_synonym access_vector_t = "permission_t set" |
|
65 |
|
66 (************ Object Classes *************) |
|
67 datatype security_class_t = |
|
68 C_process |
|
69 |
|
70 (* file-related object classes, 4.3.1 of Book *) |
|
71 | C_file |
|
72 | C_fd |
|
73 | C_dir |
|
74 (* C_blk file C_chr_file C_fifo_file C_filesystem C_lnk_file C_sock_file *) |
|
75 |
|
76 (* network, 4.3.2, using only tcp/udp as a demonstration *) |
|
77 | C_node (* Host by IP address or range of addresses *) |
|
78 | C_netif (* network interface, eth0 *) |
|
79 | C_tcp_socket |
|
80 | C_udp_socket |
|
81 (* netlink_socket unix_socket rawip_socket *) |
|
82 |
|
83 (* IPCs, 4.3.3 *) |
|
84 | C_msg (* messages within a message queue *) |
|
85 | C_msgq (* message queues *) |
|
86 (* |
|
87 | C_shm (* shared memory segment *) *) |
|
88 (* C_semaphores: only for sync, not tainting related *) |
|
89 |
|
90 (*other classes, 4.3.4*) |
|
91 (* C_capability; C_security:security server; *) |
|
92 (* | C_system the system itself *) |
|
93 |
|
94 (********* TE rules ********** |
|
95 * 1. type declaration rules |
|
96 * 2. type transition rules |
|
97 * 3. type member rules |
|
98 * 4. type change rules |
|
99 * 5. access vector rules |
|
100 * 6. cloning rules |
|
101 * 7. access vector assertions |
|
102 *) |
|
103 |
|
104 (* 1. type declaration rule *) |
|
105 datatype type_t = |
|
106 T_syslogd |
|
107 | T_syslogd_exec |
|
108 | T_devlog |
|
109 |
|
110 type_synonym attribute_t = "type_t set" |
|
111 |
|
112 (* for the asterisk/wildcard in the rules lists*) |
|
113 datatype 'a patt = |
|
114 Single "'a" |
|
115 | Set "'a set" |
|
116 | Tilde "'a set" (* complement *) |
|
117 | Asterisk |
|
118 |
|
119 (* 2. type transition rule, applied only when: execve & createfile |
|
120 * (creating subj_type, related obj_typ, type class, default type) |
|
121 * related obj_typ: proc \<rightarrow> executable; file \<rightarrow> parent-file |
|
122 * if not in the list, use subj_type for proc and parent_type for file |
|
123 * 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) |
|
124 * if using attributes, it can be transformed into the simple form of this list, |
|
125 now we use "patt" to deal with attributes |
|
126 *) |
|
127 type_synonym type_transition_rule_list_t = |
|
128 "(type_t patt \<times> type_t patt \<times> security_class_t \<times> type_t) list" |
|
129 |
|
130 |
|
131 (* for type member rules: |
|
132 * ?? I don't know the ideal yet, page 13 bottom of left column |
|
133 * |
|
134 type_synonym type_member_rule_list_t = |
|
135 "(type_t patt \<times> type_t patt \<times> security_class_t \<times> type_t) list" |
|
136 *) |
|
137 |
|
138 (* for type change rules (relabeling to diff security context): |
|
139 * ?? I don't know what's its meaning yet, page 13 up of the right column |
|
140 * |
|
141 type_synonym type_change_rule_list_t = |
|
142 "(type_t patt \<times> type_t patt \<times> security_class_t \<times> type_t) list" |
|
143 *) |
|
144 |
|
145 datatype 'a target_with_self_t = |
|
146 Not_self 'a |
|
147 | Self |
|
148 |
|
149 (* for access vector rules(verify a role-changed if allowed or not): |
|
150 * Any role-changed should be verified by this list! |
|
151 * here we only do the allow rule, audit and notify rules are ignored |
|
152 * (source type, target type, class, permissionS) |
|
153 * permissionS might be access_vector_t, which is already be model as a "set" of "pattern" |
|
154 * Self in the target type means this rule should be applied to the source process itself |
|
155 * if multiple, we search the whole list to mimic their "the union" ideal |
|
156 *) |
|
157 type_synonym allowed_rule_list_t = |
|
158 "(type_t patt \<times> (type_t patt) target_with_self_t \<times> security_class_t \<times> permission_t patt) list" |
|
159 |
|
160 datatype role_t = |
|
161 R_object |
|
162 | R_user |
|
163 | R_login |
|
164 |
|
165 (* role declarations: |
|
166 * (r, ts): ts are the types/domains that can be associated with r |
|
167 *) |
|
168 type_synonym role_declarations_list_t = |
|
169 "(role_t \<times> type_t set) list" |
|
170 |
|
171 (* role transition rules(only happens when execve call): |
|
172 * (r, t, r'): the process with role r executes a file with type t, its role will be changed to r' |
|
173 *) |
|
174 type_synonym role_transition_rule_list_t = |
|
175 "(role_t \<times> type_t \<times> role_t) list" |
|
176 |
|
177 (* role allow rules: |
|
178 * (from_role, to_role) changes when "Execve" calls! |
|
179 * What's the difference between this list and the role_transition_rule_list? |
|
180 * It is: if a process execute a file, the new role will be determined by |
|
181 * role-transition, but this new role should be in role-allow(if not deny), |
|
182 * and the new type should be compatible with the new role, which is checked |
|
183 * by role-declarations(if not deny). |
|
184 *) |
|
185 type_synonym role_allow_rule_list_t = |
|
186 "(role_t set \<times> role_t set) list" |
|
187 |
|
188 datatype user_t = |
|
189 U_system |
|
190 | U_sds |
|
191 | U_pal |
|
192 |
|
193 (* user declarations: |
|
194 * (u, roles) roles are associated with user u |
|
195 * here MLS are not in consideration |
|
196 *) |
|
197 type_synonym user_declarations_list_t = |
|
198 "(user_t \<times> role_t set)" |
|
199 |
|
200 type_synonym security_context_t = |
|
201 "(user_t \<times> role_t \<times> type_t)" |
|
202 |
|
203 (* constrains : |
|
204 * (classes, perms, expression) list |
|
205 * when flask do a permission check, constrains will fetch the |
|
206 * associated two security-contexts (source & target), flask |
|
207 * makes sure that appling expression to these two contexts, |
|
208 * will get True. If False, deny the request. |
|
209 *) |
|
210 type_synonym constrains_list_t = |
|
211 "(security_class_t set \<times> permission_t set \<times> (security_context_t \<Rightarrow> security_context_t \<Rightarrow> bool)) list" |
|
212 |
|
213 (* comments: |
|
214 * 1. sid is not needed, it is a run-time index for security-context, |
|
215 * what we do is policy-analysis, so no this "dynamic" sid as mid-ware; |
|
216 * 2. "seeds" of tainting cannot be solid objects in the initial states, |
|
217 should be extended as a "condition/predicate" to describe the "seeds" |
|
218 *) |
|
219 |
|
220 (* "temporary unused definitions : |
|
221 |
|
222 datatype security_id_t = |
|
223 SID nat |
|
224 | SECSID_NULL |
|
225 | SECSID_WILD |
|
226 |
|
227 |
|
228 (* this list mimic the action of "security_compute_av", |
|
229 * if in the list, means func returns "grant" |
|
230 * if not in, means "denied" |
|
231 * !!! this list is a "work result" of policy by selinux's |
|
232 * pre-processing func "security_compute_av" |
|
233 * in my formalisation, this is not needed, cause the specification of |
|
234 * our "selinux" contains already the policy specification. |
|
235 * we can directly get the access-vector for sid/sectxt based on allow-rules & constrains |
|
236 *) |
|
237 type_synonym avc_t = "(security_id_t \<times> security_id_t \<times> security_class_t \<times> access_vector_t) list" |
|
238 |
|
239 *) |
|
240 |
|
241 end |