|
1 theory rc_theory |
|
2 imports Main my_list_prefix |
|
3 begin |
|
4 |
|
5 |
|
6 (****************** rc policy (role, type, ... ) type definitions *****************) |
|
7 (*** normal: user-defined values for policy ***) |
|
8 (*** others: RC special values for RC internal control ***) |
|
9 |
|
10 datatype t_client = |
|
11 Client1 |
|
12 | Client2 |
|
13 |
|
14 datatype t_normal_role = |
|
15 WebServer |
|
16 | WS "t_client" |
|
17 | UpLoad "t_client" |
|
18 | CGI "t_client" |
|
19 |
|
20 datatype t_role = |
|
21 InheritParentRole |
|
22 | UseForcedRole |
|
23 | InheritUpMixed |
|
24 | InheritUserRole |
|
25 | InheritProcessRole |
|
26 | NormalRole "t_normal_role" |
|
27 |
|
28 datatype t_normal_file_type = |
|
29 Root_file_type (* special value, as 0 for root-file in the NordSec paper*) |
|
30 | WebServerLog_file |
|
31 | WebData_file "t_client" |
|
32 | CGI_P_file "t_client" |
|
33 | PrivateD_file "t_client" |
|
34 | Executable_file (* basic protection of RC *) |
|
35 |
|
36 datatype t_rc_file_type = |
|
37 InheritParent_file_type |
|
38 | NormalFile_type t_normal_file_type |
|
39 |
|
40 datatype t_normal_proc_type = |
|
41 WebServer_proc |
|
42 | CGI_P_proc "t_client" |
|
43 |
|
44 datatype t_rc_proc_type = |
|
45 InheritParent_proc_type |
|
46 | NormalProc_type t_normal_proc_type |
|
47 | UseNewRoleType |
|
48 |
|
49 datatype t_normal_ipc_type = |
|
50 WebIPC |
|
51 |
|
52 datatype t_normal_rc_type = |
|
53 File_type t_normal_file_type |
|
54 | Proc_type t_normal_proc_type |
|
55 | IPC_type t_normal_ipc_type |
|
56 |
|
57 |
|
58 |
|
59 (******* Operating System type definitions ********) |
|
60 |
|
61 type_synonym t_process = nat |
|
62 |
|
63 type_synonym t_user = nat |
|
64 |
|
65 type_synonym t_fname = string |
|
66 |
|
67 type_synonym t_file = "t_fname list" |
|
68 |
|
69 type_synonym t_ipc = nat |
|
70 |
|
71 |
|
72 |
|
73 (****** Access Control related type definitions *********) |
|
74 |
|
75 datatype t_event = |
|
76 ChangeOwner "t_process" "t_user" |
|
77 | Clone "t_process" "t_process" |
|
78 | Execute "t_process" "t_file" |
|
79 | CreateFile "t_process" "t_file" |
|
80 | CreateIPC "t_process" "t_ipc" |
|
81 | ChangeRole "t_process" "t_normal_role" (* A process should change to normal role, which not specified in paper! *) |
|
82 |
|
83 (* below are events added for tainting modelling *) |
|
84 | ReadFile "t_process" "t_file" |
|
85 | WriteFile "t_process" "t_file" |
|
86 | Send "t_process" "t_ipc" |
|
87 | Recv "t_process" "t_ipc" |
|
88 |
|
89 | Kill "t_process" "t_process" |
|
90 | DeleteFile "t_process" "t_file" |
|
91 | DeleteIPC "t_process" "t_ipc" |
|
92 |
|
93 type_synonym t_state = "t_event list" |
|
94 |
|
95 datatype t_access_type = (*changed by wch, original: "types access_type = nat" *) |
|
96 READ |
|
97 | WRITE |
|
98 | EXECUTE |
|
99 | CHANGE_OWNER |
|
100 | CREATE |
|
101 | SEND |
|
102 | RECEIVE |
|
103 |
|
104 | DELETE |
|
105 |
|
106 |
|
107 (****** Some global functions' definition *****) |
|
108 |
|
109 fun parent :: "'a list \<Rightarrow> ('a list) option" |
|
110 where |
|
111 "parent [] = None" |
|
112 | "parent (n#ns) = Some ns" |
|
113 |
|
114 definition some_in_set :: "'a set \<Rightarrow> 'a" |
|
115 where |
|
116 "some_in_set S \<equiv> SOME x. x \<in> S" |
|
117 |
|
118 lemma nonempty_set_has_ele: "S \<noteq> {} \<Longrightarrow> \<exists> e. e \<in> S" by auto |
|
119 |
|
120 lemma some_in_set_prop: "S \<noteq> {} \<Longrightarrow> some_in_set S \<in> S" |
|
121 by (drule nonempty_set_has_ele, auto simp:some_in_set_def intro:someI) |
|
122 |
|
123 |
|
124 (*********** locale for RC+OS definitions **********) |
|
125 |
|
126 definition bidirect_in_init :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> bool" |
|
127 where |
|
128 "bidirect_in_init S f \<equiv> (\<forall> a. a \<in> S \<longrightarrow> (\<exists> b. f a = Some b)) \<and> |
|
129 (\<forall> a b. f a = Some b \<longrightarrow> a \<in> S)" |
|
130 |
|
131 locale init = |
|
132 fixes |
|
133 init_files :: "t_file set" |
|
134 and init_file_type :: "t_file \<rightharpoonup> t_normal_file_type" |
|
135 and init_initialrole :: "t_file \<rightharpoonup> t_role" |
|
136 and init_forcedrole :: "t_file \<rightharpoonup> t_role" |
|
137 |
|
138 and init_processes :: "t_process set " |
|
139 and init_process_type :: "t_process \<rightharpoonup> t_normal_proc_type" |
|
140 and init_currentrole :: "t_process \<rightharpoonup> t_normal_role" |
|
141 and init_proc_forcedrole:: "t_process \<rightharpoonup> t_role" |
|
142 |
|
143 and init_ipcs :: "t_ipc set" |
|
144 and init_ipc_type:: "t_ipc \<rightharpoonup> t_normal_ipc_type" |
|
145 |
|
146 and init_users :: "t_user set" |
|
147 and init_owner :: "t_process \<rightharpoonup> t_user" |
|
148 and defrole :: "t_user \<rightharpoonup> t_normal_role" (* defrole should return normalrole, which is not |
|
149 specified in NordSec paper *) |
|
150 |
|
151 and default_fd_create_type :: "t_normal_role \<Rightarrow> t_rc_file_type" (* this func should only |
|
152 return type for normal role, for RC special role, error ! NordSec paper*) |
|
153 and default_ipc_create_type :: "t_normal_role \<Rightarrow> t_normal_ipc_type" (* like above, NordSec paper |
|
154 does not specify the domain is normal roles *) |
|
155 and default_process_create_type :: "t_normal_role \<Rightarrow> t_rc_proc_type" |
|
156 and default_process_execute_type :: "t_normal_role \<Rightarrow> t_rc_proc_type" |
|
157 and default_process_chown_type :: "t_normal_role \<Rightarrow> t_rc_proc_type" |
|
158 |
|
159 and comproles :: "t_normal_role \<Rightarrow> t_normal_role set" (* NordSec paper do not specify all roles |
|
160 here are normal *) |
|
161 |
|
162 and compatible :: "(t_normal_role \<times> t_normal_rc_type \<times> t_access_type) set" (* NordSec paper do not specify all roles and all types here are normal ! *) |
|
163 |
|
164 assumes |
|
165 parent_file_in_init: "\<And> f pf. \<lbrakk>parent f = Some pf; f \<in> init_files\<rbrakk> \<Longrightarrow> pf \<in> init_files" |
|
166 and root_in_filesystem: "[] \<in> init_files" |
|
167 and init_irole_has_file: "\<And> f r. init_initialrole f = Some r \<Longrightarrow> f \<in> init_files" |
|
168 and init_frole_has_file: "\<And> f r. init_forcedrole f = Some r \<Longrightarrow> f \<in> init_files" |
|
169 and init_ftype_has_file: "\<And> f t. init_file_type f = Some t \<Longrightarrow> f \<in> init_files" |
|
170 and |
|
171 init_proc_has_role: "bidirect_in_init init_processes init_currentrole" |
|
172 and init_proc_has_frole: "bidirect_in_init init_processes init_proc_forcedrole" |
|
173 and init_proc_has_type: "bidirect_in_init init_processes init_process_type" |
|
174 and |
|
175 init_ipc_has_type: "bidirect_in_init init_ipcs init_ipc_type" |
|
176 and |
|
177 init_user_has_role: "bidirect_in_init init_users defrole" |
|
178 and init_proc_has_owner: "bidirect_in_init init_processes init_owner" |
|
179 and init_owner_valid: "\<And> p u. init_owner p = Some u \<Longrightarrow> u \<in> init_users" |
|
180 and |
|
181 init_finite: "finite init_files \<and> finite init_processes \<and> finite init_ipcs \<and> finite init_users" |
|
182 begin |
|
183 |
|
184 (***** Operating System Listeners *****) |
|
185 |
|
186 fun current_files :: "t_state \<Rightarrow> t_file set" |
|
187 where |
|
188 "current_files [] = init_files" |
|
189 | "current_files (CreateFile p f # s) = insert f (current_files s)" |
|
190 | "current_files (DeleteFile p f # s) = current_files s - {f}" |
|
191 | "current_files (_ # s) = current_files s" |
|
192 |
|
193 fun current_procs :: "t_state \<Rightarrow> t_process set" |
|
194 where |
|
195 "current_procs [] = init_processes" |
|
196 | "current_procs (Clone p p' # s) = insert p' (current_procs s)" |
|
197 | "current_procs (Kill p p' # s) = current_procs s - {p'} " |
|
198 | "current_procs (_ # s) = current_procs s" |
|
199 |
|
200 fun current_ipcs :: "t_state \<Rightarrow> t_ipc set" |
|
201 where |
|
202 "current_ipcs [] = init_ipcs" |
|
203 | "current_ipcs (CreateIPC p i # s) = insert i (current_ipcs s)" |
|
204 | "current_ipcs (DeleteIPC p i # s) = current_ipcs s - {i}" |
|
205 | "current_ipcs (_ # s) = current_ipcs s" |
|
206 |
|
207 fun owner :: "t_state \<Rightarrow> t_process \<rightharpoonup> t_user" |
|
208 where |
|
209 "owner [] = init_owner" |
|
210 | "owner (Clone p p' # \<tau>) = (owner \<tau>) (p' := owner \<tau> p)" |
|
211 | "owner (ChangeOwner p u # \<tau>) = (owner \<tau>) (p := Some u)" |
|
212 | "owner (_ # \<tau>) = owner \<tau>" |
|
213 |
|
214 (***** functions for rc internal *****) |
|
215 |
|
216 (*** Roles Functions ***) |
|
217 |
|
218 (* comments: |
|
219 We have fix init_initialrole already in locale, why need this function? |
|
220 Cause, users may be lazy to specify every file in the initial state to some InheritParent as |
|
221 initialrole, they can just specify all the important files with special initial role, leaving |
|
222 all other None, it is init_file_initialrole's job to fill default value(InheritParent) for |
|
223 other files. Accutally, this has the point of "Functional default settings" in the 2 section of |
|
224 the NordSec paper. |
|
225 init_file_forcedrole, and init_file_type_aux are of the same meaning. |
|
226 *) |
|
227 fun init_file_initialrole :: "t_file \<rightharpoonup> t_role" |
|
228 where |
|
229 "init_file_initialrole [] = (case (init_initialrole []) of |
|
230 None \<Rightarrow> Some UseForcedRole |
|
231 | Some r \<Rightarrow> Some r)" |
|
232 | "init_file_initialrole f = (case (init_initialrole f) of |
|
233 None \<Rightarrow> Some InheritParentRole |
|
234 | Some r \<Rightarrow> Some r)" |
|
235 |
|
236 fun initialrole :: "t_state \<Rightarrow> (t_file \<rightharpoonup> t_role)" |
|
237 where |
|
238 "initialrole [] = init_file_initialrole" |
|
239 | "initialrole (CreateFile p f # s) = (initialrole s) (f:= Some InheritParentRole)" |
|
240 | "initialrole (_ # s) = initialrole s" |
|
241 |
|
242 fun erole_functor :: "(t_file \<rightharpoonup> t_role) \<Rightarrow> t_role \<Rightarrow> (t_file \<rightharpoonup> t_role)" |
|
243 where |
|
244 "erole_functor rfunc r [] = ( |
|
245 if (rfunc [] = Some InheritParentRole) |
|
246 then Some r |
|
247 else rfunc [] )" |
|
248 | "erole_functor rfunc r (n#ns) = ( |
|
249 if (rfunc (n#ns) = Some InheritParentRole) |
|
250 then erole_functor rfunc r ns |
|
251 else rfunc (n#ns) )" |
|
252 |
|
253 definition effinitialrole :: "t_state \<Rightarrow> (t_file \<rightharpoonup> t_role)" |
|
254 where |
|
255 "effinitialrole s \<equiv> erole_functor (initialrole s) UseForcedRole" |
|
256 |
|
257 fun init_file_forcedrole :: "t_file \<rightharpoonup> t_role" |
|
258 where |
|
259 "init_file_forcedrole [] = ( case (init_forcedrole []) of |
|
260 None \<Rightarrow> Some InheritUpMixed |
|
261 | Some r \<Rightarrow> Some r )" |
|
262 | "init_file_forcedrole f = ( case (init_forcedrole f) of |
|
263 None \<Rightarrow> Some InheritParentRole |
|
264 | Some r \<Rightarrow> Some r )" |
|
265 |
|
266 fun forcedrole :: "t_state \<Rightarrow> (t_file \<rightharpoonup> t_role)" |
|
267 where |
|
268 "forcedrole [] = init_file_forcedrole" |
|
269 | "forcedrole (CreateFile p f # s) = (forcedrole s) (f:= Some InheritParentRole)" |
|
270 | "forcedrole (_ # s) = forcedrole s" |
|
271 |
|
272 definition effforcedrole :: "t_state \<Rightarrow> (t_file \<rightharpoonup> t_role)" |
|
273 where |
|
274 "effforcedrole s \<equiv> erole_functor (forcedrole s) InheritUpMixed" |
|
275 |
|
276 fun proc_forcedrole :: "t_state \<Rightarrow> (t_process \<rightharpoonup> t_role)" (* $6.7$ *) |
|
277 where |
|
278 "proc_forcedrole [] = init_proc_forcedrole" |
|
279 | "proc_forcedrole (Execute p f # s) = (proc_forcedrole s) (p := effforcedrole s f)" |
|
280 | "proc_forcedrole (Clone p p' # s) = (proc_forcedrole s) (p' := proc_forcedrole s p)" |
|
281 | "proc_forcedrole (e # s) = proc_forcedrole s" |
|
282 |
|
283 fun currentrole :: "t_state \<Rightarrow> (t_process \<rightharpoonup> t_normal_role)" |
|
284 where |
|
285 "currentrole [] = init_currentrole" |
|
286 | "currentrole (Clone p p' # \<tau>) = (currentrole \<tau>) (p' := currentrole \<tau> p)" |
|
287 | "currentrole (Execute p f # \<tau>) = (currentrole \<tau>) (p := |
|
288 case (effinitialrole \<tau> f) of |
|
289 Some ir \<Rightarrow> (case ir of |
|
290 NormalRole r \<Rightarrow> Some r |
|
291 | UseForcedRole \<Rightarrow> ( |
|
292 case (effforcedrole \<tau> f) of |
|
293 Some fr \<Rightarrow> (case fr of |
|
294 NormalRole r \<Rightarrow> Some r |
|
295 | InheritUserRole \<Rightarrow> (defrole \<circ>\<^sub>m (owner \<tau>)) p |
|
296 | InheritProcessRole \<Rightarrow> currentrole \<tau> p |
|
297 | InheritUpMixed \<Rightarrow> currentrole \<tau> p |
|
298 | _ \<Rightarrow> None ) |
|
299 | _ \<Rightarrow> None ) |
|
300 | _ \<Rightarrow> None ) |
|
301 | _ \<Rightarrow> None )" |
|
302 | "currentrole (ChangeOwner p u # \<tau>) = (currentrole \<tau>) (p := |
|
303 case (proc_forcedrole \<tau> p) of |
|
304 Some fr \<Rightarrow> (case fr of |
|
305 NormalRole r \<Rightarrow> Some r |
|
306 | InheritProcessRole \<Rightarrow> currentrole \<tau> p |
|
307 | InheritUserRole \<Rightarrow> defrole u |
|
308 | InheritUpMixed \<Rightarrow> defrole u |
|
309 | _ \<Rightarrow> None) |
|
310 | _ \<Rightarrow> None )" |
|
311 | "currentrole (ChangeRole p r # \<tau>) = (currentrole \<tau>) (p := Some r)" |
|
312 | "currentrole (_ # \<tau>) = currentrole \<tau>" |
|
313 |
|
314 (*** Types Functions ***) |
|
315 |
|
316 fun init_file_type_aux :: "t_file \<rightharpoonup> t_rc_file_type" |
|
317 where |
|
318 "init_file_type_aux f = (if (f \<in> init_files) |
|
319 then (case (init_file_type f) of |
|
320 Some t \<Rightarrow> Some (NormalFile_type t) |
|
321 | _ \<Rightarrow> Some InheritParent_file_type) |
|
322 else None)" |
|
323 |
|
324 fun type_of_file :: "t_state \<Rightarrow> (t_file \<rightharpoonup> t_rc_file_type)" (* (6) *) |
|
325 where |
|
326 "type_of_file [] = init_file_type_aux" |
|
327 | "type_of_file (CreateFile p f # s) = ( |
|
328 case (currentrole s p) of |
|
329 Some r \<Rightarrow> (type_of_file s) (f := Some (default_fd_create_type r)) |
|
330 | _ \<Rightarrow> (type_of_file s) (f := None))" |
|
331 | "type_of_file (_ # s) = type_of_file s" (* add by wch *) |
|
332 |
|
333 fun etype_aux:: "(t_file \<rightharpoonup> t_rc_file_type) \<Rightarrow> (t_file \<rightharpoonup> t_normal_file_type)" |
|
334 where |
|
335 "etype_aux typf [] = ( |
|
336 case (typf []) of |
|
337 Some InheritParent_file_type \<Rightarrow> Some Root_file_type |
|
338 | Some (NormalFile_type t) \<Rightarrow> Some t |
|
339 | None \<Rightarrow> None )" |
|
340 | "etype_aux typf (n#ns) = ( |
|
341 case (typf (n#ns)) of |
|
342 Some InheritParent_file_type \<Rightarrow> etype_aux typf ns |
|
343 | Some (NormalFile_type t) \<Rightarrow> Some t |
|
344 | None \<Rightarrow> None )" |
|
345 |
|
346 definition etype_of_file :: "t_state \<Rightarrow> (t_file \<rightharpoonup> t_normal_file_type)" |
|
347 (* etype is always normal *) |
|
348 where |
|
349 "etype_of_file s \<equiv> etype_aux (type_of_file s)" |
|
350 |
|
351 definition pct :: "t_state \<Rightarrow> (t_process \<rightharpoonup> t_rc_proc_type)" |
|
352 where |
|
353 "pct s p \<equiv> (case (currentrole s p) of |
|
354 Some r \<Rightarrow> Some (default_process_create_type r) |
|
355 | _ \<Rightarrow> None)" |
|
356 |
|
357 definition pet :: "t_state \<Rightarrow> (t_process \<rightharpoonup> t_rc_proc_type)" |
|
358 where |
|
359 "pet s p \<equiv> (case (currentrole s p) of |
|
360 Some r \<Rightarrow> Some (default_process_execute_type r) |
|
361 | _ \<Rightarrow> None)" |
|
362 |
|
363 definition pot :: "t_state \<Rightarrow> (t_process \<rightharpoonup> t_rc_proc_type)" |
|
364 where |
|
365 "pot s p \<equiv> (case (currentrole s p) of |
|
366 Some r \<Rightarrow> Some (default_process_chown_type r) |
|
367 | _ \<Rightarrow> None)" |
|
368 |
|
369 fun type_of_process :: "t_state \<Rightarrow> (t_process \<rightharpoonup> t_normal_proc_type)" |
|
370 where |
|
371 "type_of_process [] = init_process_type" |
|
372 | "type_of_process (Clone p p' # \<tau>) = (type_of_process \<tau>) (p' := |
|
373 case (pct \<tau> p) of |
|
374 Some InheritParent_proc_type \<Rightarrow> type_of_process \<tau> p |
|
375 | Some (NormalProc_type tp) \<Rightarrow> Some tp |
|
376 | _ \<Rightarrow> None )" (*6.80*) |
|
377 | "type_of_process (Execute p f # \<tau>) = (type_of_process \<tau>) (p := |
|
378 case (pet \<tau> p) of |
|
379 Some InheritParent_proc_type \<Rightarrow> type_of_process \<tau> p |
|
380 | Some (NormalProc_type tp) \<Rightarrow> Some tp |
|
381 | _ \<Rightarrow> None )" (*6.82*) |
|
382 | "type_of_process (ChangeOwner p u # \<tau>) = (type_of_process \<tau>) (p := |
|
383 case (pot \<tau> p) of |
|
384 Some InheritParent_proc_type \<Rightarrow> type_of_process \<tau> p |
|
385 | Some UseNewRoleType \<Rightarrow> (case (pct (ChangeOwner p u # \<tau>) p) of |
|
386 Some InheritParent_proc_type \<Rightarrow> type_of_process \<tau> p |
|
387 | Some (NormalProc_type tp) \<Rightarrow> Some tp |
|
388 | _ \<Rightarrow> None) |
|
389 | Some (NormalProc_type tp) \<Rightarrow> Some tp |
|
390 | _ \<Rightarrow> None )" (* the UseNewRoleType case is refered with Nordsec paper 4 (11), and it is not right??! of just |
|
391 use "pct" *) |
|
392 | "type_of_process (_ # \<tau>) = type_of_process \<tau>" |
|
393 |
|
394 fun type_of_ipc :: "t_state \<Rightarrow> (t_ipc \<rightharpoonup> t_normal_ipc_type)" (* (14) *) |
|
395 where |
|
396 "type_of_ipc [] = init_ipc_type" |
|
397 | "type_of_ipc (CreateIPC p i # s) = (type_of_ipc s) (i := |
|
398 case (currentrole s p) of |
|
399 Some r \<Rightarrow> Some (default_ipc_create_type r) |
|
400 | _ \<Rightarrow> None )" |
|
401 | "type_of_ipc (_ # s) = type_of_ipc s" (* add by wch *) |
|
402 |
|
403 (*** RC access control ***) |
|
404 fun rc_grant :: "t_state \<Rightarrow> t_event \<Rightarrow> bool" |
|
405 where |
|
406 "rc_grant \<tau> (CreateFile p f) = ( |
|
407 case (parent f) of |
|
408 Some pf \<Rightarrow> ( |
|
409 case (currentrole \<tau> p, etype_of_file \<tau> pf) of |
|
410 (Some r, Some t) \<Rightarrow> ( |
|
411 case (default_fd_create_type r) of |
|
412 InheritParent_file_type \<Rightarrow> (r, File_type t, WRITE) \<in> compatible |
|
413 | NormalFile_type t' \<Rightarrow> (r, File_type t, WRITE) \<in> compatible \<and> (r, File_type t', CREATE) \<in> compatible |
|
414 ) |
|
415 | _ \<Rightarrow> False ) |
|
416 | _ \<Rightarrow> False )" |
|
417 | "rc_grant \<tau> (ReadFile p f) = ( |
|
418 case (currentrole \<tau> p, etype_of_file \<tau> f) of |
|
419 (Some r, Some t) \<Rightarrow> (r, File_type t, READ) \<in> compatible |
|
420 | _ \<Rightarrow> False )" |
|
421 | "rc_grant \<tau> (WriteFile p f) = ( |
|
422 case (currentrole \<tau> p, etype_of_file \<tau> f) of |
|
423 (Some r, Some t) \<Rightarrow> (r, File_type t, WRITE) \<in> compatible |
|
424 | _ \<Rightarrow> False )" |
|
425 | "rc_grant \<tau> (Execute p f) = ( |
|
426 case (currentrole \<tau> p, etype_of_file \<tau> f) of |
|
427 (Some r, Some t) \<Rightarrow> (r, File_type t, EXECUTE) \<in> compatible |
|
428 | _ \<Rightarrow> False )" |
|
429 | "rc_grant \<tau> (ChangeOwner p u) = ( |
|
430 case (currentrole \<tau> p, type_of_process \<tau> p) of |
|
431 (Some r, Some t) \<Rightarrow> (r, Proc_type t, CHANGE_OWNER) \<in> compatible |
|
432 | _ \<Rightarrow> False )" |
|
433 | "rc_grant \<tau> (Clone p newproc) = ( |
|
434 case (currentrole \<tau> p, type_of_process \<tau> p) of |
|
435 (Some r, Some t) \<Rightarrow> (r, Proc_type t, CREATE) \<in> compatible |
|
436 | _ \<Rightarrow> False )" (* premiss of no limit to clone is removed to locale assumptions *) |
|
437 | "rc_grant \<tau> (ChangeRole p r) = ( |
|
438 case (currentrole \<tau> p) of |
|
439 Some cr \<Rightarrow> r \<in> comproles cr |
|
440 | _ \<Rightarrow> False )" |
|
441 | "rc_grant \<tau> (Send p i) = ( |
|
442 case (currentrole \<tau> p, type_of_ipc \<tau> i) of |
|
443 (Some r, Some t) \<Rightarrow> (r, IPC_type t, SEND) \<in> compatible |
|
444 | _ \<Rightarrow> False )" |
|
445 | "rc_grant \<tau> (Recv p i) = ( |
|
446 case (currentrole \<tau> p, type_of_ipc \<tau> i) of |
|
447 (Some r, Some t) \<Rightarrow> (r, IPC_type t, RECEIVE) \<in> compatible |
|
448 | _ \<Rightarrow> False )" |
|
449 | "rc_grant \<tau> (CreateIPC p i) = ( |
|
450 case (currentrole \<tau> p) of |
|
451 Some r \<Rightarrow> (r, IPC_type (default_ipc_create_type r), CREATE) \<in> compatible |
|
452 | _ \<Rightarrow> False )" |
|
453 | "rc_grant \<tau> (DeleteFile p f) = ( |
|
454 case (currentrole \<tau> p, etype_of_file \<tau> f) of |
|
455 (Some r, Some t) \<Rightarrow> (r, File_type t, DELETE) \<in> compatible |
|
456 | _ \<Rightarrow> False )" |
|
457 | "rc_grant \<tau> (DeleteIPC p i) = ( |
|
458 case (currentrole \<tau> p, type_of_ipc \<tau> i) of |
|
459 (Some r, Some t) \<Rightarrow> (r, IPC_type t, DELETE) \<in> compatible |
|
460 | _ \<Rightarrow> False )" |
|
461 | "rc_grant \<tau> (Kill p p') = ( |
|
462 case (currentrole \<tau> p, type_of_process \<tau> p') of |
|
463 (Some r, Some t) \<Rightarrow> (r, Proc_type t, DELETE) \<in> compatible |
|
464 | _ \<Rightarrow> False )" |
|
465 |
|
466 |
|
467 (**** OS' job: checking resources existence & grant new resource ****) |
|
468 |
|
469 definition next_nat :: "nat set \<Rightarrow> nat" |
|
470 where |
|
471 "next_nat ps = (Max ps) + 1" |
|
472 |
|
473 definition new_proc :: "t_state \<Rightarrow> t_process" |
|
474 where |
|
475 "new_proc \<tau> = next_nat (current_procs \<tau>)" |
|
476 |
|
477 definition new_ipc :: "t_state \<Rightarrow> t_ipc" |
|
478 where |
|
479 "new_ipc \<tau> = next_nat (current_ipcs \<tau>)" |
|
480 |
|
481 (* new file pathname is user-defined, so os just check if its unexistence *) |
|
482 fun os_grant :: "t_state \<Rightarrow> t_event \<Rightarrow> bool" |
|
483 where |
|
484 "os_grant \<tau> (Execute p f) = (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau>)" |
|
485 | "os_grant \<tau> (CreateFile p f) = (p \<in> current_procs \<tau> \<and> f \<notin> current_files \<tau> \<and> (\<exists> pf. (parent f = Some pf) \<and> pf \<in> current_files \<tau>))" (*cannot create disk, ?? or f = [] ??*) |
|
486 | "os_grant \<tau> (ChangeRole p r) = (p \<in> current_procs \<tau>)" |
|
487 | "os_grant \<tau> (ReadFile p f) = (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau>)" |
|
488 | "os_grant \<tau> (WriteFile p f) = (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau>)" |
|
489 | "os_grant \<tau> (ChangeOwner p u)= (p \<in> current_procs \<tau> \<and> u \<in> init_users)" |
|
490 | "os_grant \<tau> (CreateIPC p i) = (p \<in> current_procs \<tau> \<and> i = new_ipc \<tau>)" |
|
491 | "os_grant \<tau> (Send p i) = (p \<in> current_procs \<tau> \<and> i \<in> current_ipcs \<tau>)" |
|
492 | "os_grant \<tau> (Recv p i) = (p \<in> current_procs \<tau> \<and> i \<in> current_ipcs \<tau>)" |
|
493 | "os_grant \<tau> (Clone p p') = (p \<in> current_procs \<tau> \<and> p' = new_proc \<tau>)" |
|
494 | "os_grant \<tau> (Kill p p') = (p \<in> current_procs \<tau> \<and> p' \<in> current_procs \<tau>)" |
|
495 | "os_grant \<tau> (DeleteFile p f) = (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau> \<and> \<not> (\<exists>fn. fn # f \<in> current_files \<tau>))" |
|
496 | "os_grant \<tau> (DeleteIPC p i) = (p \<in> current_procs \<tau> \<and> i \<in> current_ipcs \<tau>)" |
|
497 |
|
498 (**** system valid state ****) |
|
499 |
|
500 inductive valid :: "t_state \<Rightarrow> bool" |
|
501 where |
|
502 vs_nil: "valid []" |
|
503 | vs_step: "\<lbrakk>valid s; os_grant s e; rc_grant s e\<rbrakk> \<Longrightarrow> valid (e # s)" |
|
504 |
|
505 end |
|
506 |
|
507 (*** more RC constrains of type system in formalisation ***) |
|
508 |
|
509 locale rc_basic = init + |
|
510 assumes |
|
511 init_initialrole_valid: "\<And> f r. init_initialrole f = Some r \<Longrightarrow> r = InheritParentRole \<or> r = UseForcedRole \<or> (\<exists> nr. r = NormalRole nr)" (* 6.10 *) |
|
512 and init_forcedrole_valid: "\<And> f r. init_forcedrole f = Some r \<Longrightarrow> r = InheritUserRole \<or> r = InheritProcessRole \<or> r = InheritParentRole \<or> r = InheritUpMixed \<or> (\<exists> nr. r = NormalRole nr)" (* 6.11 *) |
|
513 and init_proc_forcedrole_valid: "\<And> p r. init_proc_forcedrole p = Some r \<Longrightarrow> r = InheritUserRole \<or> r = InheritProcessRole \<or> r = InheritUpMixed \<or> (\<exists> nr. r = NormalRole nr)" (* 6.7 *) |
|
514 and default_fd_create_type_valid: "\<And> nr t. default_fd_create_type nr = t \<Longrightarrow> t = InheritParent_file_type \<or> (\<exists> nt. t = NormalFile_type nt)" (*6.16*) |
|
515 and default_process_create_type_valid: "\<And> nr t. default_process_create_type nr = t \<Longrightarrow> t = InheritParent_proc_type \<or> (\<exists> nt. t = NormalProc_type nt)" (*6.18*) |
|
516 and default_process_chown_type_valid: "\<And> nr t. default_process_chown_type nr = t \<Longrightarrow> t = InheritParent_proc_type \<or> t = UseNewRoleType \<or> (\<exists> nt. t = NormalProc_type nt)" (*6.19*) |
|
517 and default_process_execute_type_valid: "\<And> nr t. default_process_execute_type nr = t \<Longrightarrow> t = InheritParent_proc_type \<or> (\<exists> nt. t = NormalProc_type nt)" (*6.20*) |
|
518 |
|
519 begin |
|
520 |
|
521 lemma init_file_initialrole_valid: "init_file_initialrole f = Some r \<Longrightarrow> r = InheritParentRole \<or> r = UseForcedRole \<or> (\<exists> nr. r = NormalRole nr)" |
|
522 apply (induct f) |
|
523 by (auto simp:init_file_initialrole.simps dest:init_initialrole_valid split:option.splits) |
|
524 |
|
525 lemma initialrole_valid: "initialrole \<tau> f = Some r \<Longrightarrow> r = InheritParentRole \<or> r = UseForcedRole \<or> (\<exists> nr. r = NormalRole nr)" (* 6.10 *) |
|
526 apply (induct \<tau> arbitrary:f) defer |
|
527 apply (case_tac a) |
|
528 apply (auto simp:initialrole.simps dest:init_file_initialrole_valid |
|
529 split:option.splits if_splits) |
|
530 done |
|
531 |
|
532 lemma effinitialrole_valid: "effinitialrole \<tau> f = Some r \<Longrightarrow> r = UseForcedRole \<or> (\<exists> nr. r = NormalRole nr)" |
|
533 apply (induct f) |
|
534 apply (auto simp:effinitialrole_def dest:initialrole_valid split:option.splits if_splits) |
|
535 done |
|
536 |
|
537 lemma init_file_forcedrole_valid: |
|
538 "init_file_forcedrole f = Some r \<Longrightarrow> r = InheritUserRole \<or> r = InheritProcessRole \<or> r = InheritParentRole \<or> r = InheritUpMixed \<or> (\<exists> nr. r = NormalRole nr)" |
|
539 apply (induct f) |
|
540 by (auto simp:init_file_forcedrole.simps dest:init_forcedrole_valid split:option.splits) |
|
541 |
|
542 lemma forcedrole_valid: "forcedrole \<tau> f = Some r \<Longrightarrow> r = InheritUserRole \<or> r = InheritProcessRole \<or> r = InheritParentRole \<or> r = InheritUpMixed \<or> (\<exists> nr. r = NormalRole nr)" (* 6.10 *) |
|
543 apply (induct \<tau> arbitrary:f) defer |
|
544 apply (case_tac a) |
|
545 apply (auto simp:forcedrole.simps dest:init_file_forcedrole_valid |
|
546 split:option.splits if_splits) |
|
547 done |
|
548 |
|
549 lemma effforcedrole_valid: "effforcedrole \<tau> f = Some r \<Longrightarrow> r = InheritUserRole \<or> r = InheritProcessRole \<or> r = InheritUpMixed \<or> (\<exists> nr. r = NormalRole nr)" |
|
550 apply (induct f) |
|
551 apply (auto simp:effforcedrole_def dest:forcedrole_valid split:option.splits if_splits) |
|
552 done |
|
553 |
|
554 lemma proc_forcedrole_valid: "proc_forcedrole \<tau> p = Some r \<Longrightarrow> r = InheritUserRole \<or> r = InheritProcessRole \<or> r = InheritUpMixed \<or> (\<exists> nr. r = NormalRole nr)" (* 6.7 *) |
|
555 apply (induct \<tau> arbitrary:p) defer |
|
556 apply (case_tac a) |
|
557 apply (auto simp:proc_forcedrole.simps dest:init_proc_forcedrole_valid effforcedrole_valid |
|
558 split:option.splits if_splits) |
|
559 done |
|
560 |
|
561 lemma pct_valid: "pct \<tau> p = Some t \<Longrightarrow> t = InheritParent_proc_type \<or> (\<exists> nt. t = NormalProc_type nt)" |
|
562 by (auto simp:pct_def default_process_create_type_valid split:option.splits) |
|
563 |
|
564 lemma pot_valid: "pot \<tau> p = Some t \<Longrightarrow> t = InheritParent_proc_type \<or> t = UseNewRoleType \<or> (\<exists> nt. t = NormalProc_type nt)" |
|
565 by (auto simp:pot_def default_process_chown_type_valid split:option.splits) |
|
566 |
|
567 lemma pet_valid: "pet \<tau> p = Some t \<Longrightarrow> t = InheritParent_proc_type \<or> (\<exists> nt. t = NormalProc_type nt)" |
|
568 by (simp add:pet_def default_process_execute_type_valid map_comp_def split:option.splits) |
|
569 |
|
570 end |
|
571 |
|
572 (******* Reachable/tainting related type definitions ********) |
|
573 |
|
574 datatype t_object = |
|
575 Proc "t_process" |
|
576 | File "t_file" |
|
577 | IPC "t_ipc" |
|
578 |
|
579 fun object_in_init :: "t_object \<Rightarrow> t_file set \<Rightarrow> t_process set \<Rightarrow> t_ipc set \<Rightarrow> bool" |
|
580 where |
|
581 "object_in_init (Proc p) init_files init_procs init_ipcs = (p \<in> init_procs)" |
|
582 | "object_in_init (File f) init_files init_procs init_ipcs = (f \<in> init_files)" |
|
583 | "object_in_init (IPC i) init_files init_procs init_ipcs = (i \<in> init_ipcs)" |
|
584 |
|
585 (*** locale for dynamic tainting ***) |
|
586 |
|
587 locale tainting = rc_basic + |
|
588 |
|
589 fixes seeds :: "t_object set" |
|
590 |
|
591 assumes |
|
592 seeds_in_init: "\<And> obj. obj \<in> seeds \<Longrightarrow> object_in_init obj init_files init_processes init_ipcs" |
|
593 begin |
|
594 |
|
595 lemma finite_seeds: "finite seeds" |
|
596 proof- |
|
597 have "finite {obj. object_in_init obj init_files init_processes init_ipcs}" |
|
598 proof- |
|
599 have "finite {File f| f. f \<in> init_files}" |
|
600 using init_finite by auto |
|
601 moreover have "finite {Proc p| p. p \<in> init_processes}" |
|
602 using init_finite by auto |
|
603 moreover have "finite {IPC i| i. i \<in> init_ipcs}" |
|
604 using init_finite by auto |
|
605 ultimately have "finite ({File f| f. f \<in> init_files} \<union> {Proc p| p. p \<in> init_processes} \<union> {IPC i| i. i \<in> init_ipcs})" |
|
606 by auto |
|
607 thus ?thesis |
|
608 apply (rule_tac B = "({File f| f. f \<in> init_files} \<union> {Proc p| p. p \<in> init_processes} \<union> {IPC i| i. i \<in> init_ipcs})" in finite_subset) |
|
609 by (auto, case_tac x, simp+) |
|
610 qed |
|
611 with seeds_in_init |
|
612 show ?thesis |
|
613 by (rule_tac finite_subset, auto) |
|
614 qed |
|
615 |
|
616 fun exists :: "t_state \<Rightarrow> t_object \<Rightarrow> bool" |
|
617 where |
|
618 "exists s (File f) = (f \<in> current_files s)" |
|
619 | "exists s (Proc p) = (p \<in> current_procs s)" |
|
620 | "exists s (IPC i) = (i \<in> current_ipcs s)" |
|
621 |
|
622 inductive tainted :: "t_object \<Rightarrow> t_state \<Rightarrow> bool" ("_ \<in> tainted _" [100, 100] 100) |
|
623 where |
|
624 t_init: "obj \<in> seeds \<Longrightarrow> obj \<in> tainted []" |
|
625 | t_clone: "\<lbrakk>Proc p \<in> tainted s; valid (Clone p p' # s)\<rbrakk> \<Longrightarrow> Proc p' \<in> tainted (Clone p p' # s)" |
|
626 | t_exec: "\<lbrakk>File f \<in> tainted s; valid (Execute p f # s)\<rbrakk> \<Longrightarrow> Proc p \<in> tainted (Execute p f # s)" |
|
627 | t_cfile: "\<lbrakk>Proc p \<in> tainted s; valid (CreateFile p f # s)\<rbrakk> \<Longrightarrow> File f \<in> tainted (CreateFile p f # s)" |
|
628 | t_cipc: "\<lbrakk>Proc p \<in> tainted s; valid (CreateIPC p i # s)\<rbrakk> \<Longrightarrow> IPC i \<in> tainted (CreateIPC p i # s)" |
|
629 | t_read: "\<lbrakk>File f \<in> tainted s; valid (ReadFile p f # s)\<rbrakk> \<Longrightarrow> Proc p \<in> tainted (ReadFile p f # s)" |
|
630 | t_write: "\<lbrakk>Proc p \<in> tainted s; valid (WriteFile p f # s)\<rbrakk> \<Longrightarrow> File f \<in> tainted (WriteFile p f # s)" |
|
631 | t_send: "\<lbrakk>Proc p \<in> tainted s; valid (Send p i # s)\<rbrakk> \<Longrightarrow> IPC i \<in> tainted (Send p i # s)" |
|
632 | t_recv: "\<lbrakk>IPC i \<in> tainted s; valid (Recv p i # s)\<rbrakk> \<Longrightarrow> Proc p \<in> tainted (Recv p i # s)" |
|
633 | t_remain:"\<lbrakk>obj \<in> tainted s; valid (e # s); exists (e # s) obj\<rbrakk> \<Longrightarrow> obj \<in> tainted (e # s)" |
|
634 |
|
635 definition taintable:: "t_object \<Rightarrow> bool" |
|
636 where |
|
637 "taintable obj \<equiv> \<exists> s. obj \<in> tainted s" |
|
638 |
|
639 fun deleted :: "t_object \<Rightarrow> t_event list \<Rightarrow> bool" |
|
640 where |
|
641 "deleted obj [] = False" |
|
642 | "deleted obj (Kill p p' # \<tau>) = ((obj = Proc p') \<or> deleted obj \<tau>)" |
|
643 | "deleted obj (DeleteFile p f # \<tau>) = ((obj = File f) \<or> deleted obj \<tau>)" |
|
644 | "deleted obj (DeleteIPC p i # \<tau>) = ((obj = IPC i) \<or> deleted obj \<tau>)" |
|
645 | "deleted obj (_ # \<tau>) = deleted obj \<tau>" |
|
646 |
|
647 definition undeletable :: "t_object \<Rightarrow> bool" |
|
648 where |
|
649 "undeletable obj \<equiv> exists [] obj \<and> \<not> (\<exists> s. valid s \<and> deleted obj s)" |
|
650 |
|
651 fun no_del_event:: "t_event list \<Rightarrow> bool" |
|
652 where |
|
653 "no_del_event [] = True" |
|
654 | "no_del_event (Kill p p' # \<tau>) = False" |
|
655 | "no_del_event (DeleteFile p f # \<tau>) = False" |
|
656 | "no_del_event (DeleteIPC p i # \<tau>) = False" |
|
657 | "no_del_event (_ # \<tau>) = no_del_event \<tau>" |
|
658 |
|
659 end |
|
660 |
|
661 |
|
662 (***** locale for statical world *****) |
|
663 |
|
664 type_synonym t_sprocess = "t_normal_role \<times> t_role \<times> t_normal_proc_type \<times> t_user" |
|
665 |
|
666 type_synonym t_sfile = "t_normal_file_type \<times> t_file" |
|
667 |
|
668 type_synonym t_sipc = "t_normal_ipc_type" |
|
669 |
|
670 datatype t_sobject = |
|
671 SProc "t_sprocess" "t_process option" |
|
672 | SFile "t_sfile" "t_file option" |
|
673 | SIPC "t_sipc" "t_ipc option" |
|
674 | Unknown |
|
675 |
|
676 locale tainting_s_complete = tainting |
|
677 |
|
678 begin |
|
679 |
|
680 definition chown_role_aux:: "t_normal_role \<Rightarrow> t_role \<Rightarrow> t_user \<Rightarrow> t_normal_role option" |
|
681 where |
|
682 "chown_role_aux cr fr u \<equiv> ( |
|
683 case fr of |
|
684 NormalRole r \<Rightarrow> Some r |
|
685 | InheritProcessRole \<Rightarrow> Some cr |
|
686 | _ \<Rightarrow> defrole u )" |
|
687 |
|
688 definition chown_type_aux:: "t_normal_role \<Rightarrow> t_normal_role \<Rightarrow> t_normal_proc_type \<Rightarrow> t_normal_proc_type" |
|
689 where |
|
690 "chown_type_aux cr nr t \<equiv> ( |
|
691 case (default_process_chown_type cr) of |
|
692 InheritParent_proc_type \<Rightarrow> t |
|
693 | UseNewRoleType \<Rightarrow> (case (default_process_create_type nr) of |
|
694 InheritParent_proc_type \<Rightarrow> t |
|
695 | NormalProc_type tp \<Rightarrow> tp) |
|
696 | NormalProc_type tp \<Rightarrow> tp )" |
|
697 |
|
698 definition exec_type_aux :: "t_normal_role \<Rightarrow> t_normal_proc_type \<Rightarrow> t_normal_proc_type" |
|
699 where |
|
700 "exec_type_aux cr t \<equiv> (case (default_process_execute_type cr) of |
|
701 InheritParent_proc_type \<Rightarrow> t |
|
702 | NormalProc_type tp \<Rightarrow>tp)" |
|
703 |
|
704 definition exec_role_aux :: "t_normal_role \<Rightarrow> t_file \<Rightarrow> t_user \<Rightarrow> t_normal_role option" |
|
705 where |
|
706 "exec_role_aux cr sd u \<equiv> ( |
|
707 case (erole_functor init_file_initialrole UseForcedRole sd) of |
|
708 Some ir \<Rightarrow> (case ir of |
|
709 NormalRole r \<Rightarrow> Some r |
|
710 | UseForcedRole \<Rightarrow> ( |
|
711 case (erole_functor init_file_forcedrole InheritUpMixed sd) of |
|
712 Some fr \<Rightarrow> (case fr of |
|
713 NormalRole r \<Rightarrow> Some r |
|
714 | InheritUserRole \<Rightarrow> defrole u |
|
715 | _ \<Rightarrow> Some cr ) |
|
716 | None \<Rightarrow> None ) |
|
717 | _ \<Rightarrow> None ) |
|
718 | _ \<Rightarrow> None )" |
|
719 |
|
720 definition clone_type_aux :: "t_normal_role \<Rightarrow> t_normal_proc_type \<Rightarrow> t_normal_proc_type" |
|
721 where |
|
722 "clone_type_aux r t \<equiv> (case (default_process_create_type r) of |
|
723 InheritParent_proc_type \<Rightarrow> t |
|
724 | NormalProc_type tp \<Rightarrow> tp)" |
|
725 |
|
726 (* all the static objects that dynamic objects referring to *) |
|
727 (* they should all be in a finite set ? *) |
|
728 (* besides, they're no clone case for all_sobjs, we have no "SProc ... None" case, Clone p p', p' statically viewed as p too, so the many2many mapping becomes to many2one, which makes all succeeded*) |
|
729 inductive_set all_sobjs :: "t_sobject set" |
|
730 where |
|
731 af_init: "\<lbrakk>f \<in> init_files; etype_aux init_file_type_aux f = Some t\<rbrakk> \<Longrightarrow> SFile (t, f) (Some f) \<in> all_sobjs" |
|
732 | af_cfd: "\<lbrakk>SFile (t, sd) sf \<in> all_sobjs; SProc (r, fr, pt, u) sp \<in> all_sobjs; default_fd_create_type r = NormalFile_type t'; (r, File_type t, WRITE) \<in> compatible; (r, File_type t', CREATE) \<in> compatible\<rbrakk> \<Longrightarrow> SFile (t', sd) None \<in> all_sobjs" |
|
733 | af_cfd': "\<lbrakk>SFile (t, sd) sf \<in> all_sobjs; SProc (r, fr, pt, u) sp \<in> all_sobjs; default_fd_create_type r = InheritParent_file_type; (r, File_type t, WRITE) \<in> compatible\<rbrakk> \<Longrightarrow> SFile (t, sd) None \<in> all_sobjs" |
|
734 |
|
735 | ai_init: "init_ipc_type i = Some t \<Longrightarrow> SIPC t (Some i) \<in> all_sobjs" |
|
736 | ai_cipc: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> all_sobjs; (r, IPC_type (default_ipc_create_type r), CREATE) \<in> compatible\<rbrakk> \<Longrightarrow> SIPC (default_ipc_create_type r) None \<in> all_sobjs" |
|
737 |
|
738 | ap_init: "\<lbrakk>init_currentrole p = Some r; init_proc_forcedrole p = Some fr; init_process_type p = Some t; init_owner p = Some u\<rbrakk> \<Longrightarrow> SProc (r, fr, t, u) (Some p) \<in> all_sobjs" |
|
739 | ap_crole: "\<lbrakk>SProc (r, fr, t, u) sp \<in> all_sobjs; r' \<in> comproles r\<rbrakk> \<Longrightarrow> SProc (r', fr, t, u) sp \<in> all_sobjs" |
|
740 | ap_chown: "\<lbrakk>SProc (r, fr, t, u') sp \<in> all_sobjs; u \<in> init_users; chown_role_aux r fr u = Some nr; (r, Proc_type t, CHANGE_OWNER) \<in> compatible\<rbrakk> \<Longrightarrow> SProc (nr, fr, chown_type_aux r nr t, u) sp \<in> all_sobjs" |
|
741 | ap_exec: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> all_sobjs; SFile (t, sd) sf \<in> all_sobjs; (r, File_type t, EXECUTE) \<in> compatible; exec_role_aux r sd u = Some r'; erole_functor init_file_forcedrole InheritUpMixed sd = Some fr'\<rbrakk> \<Longrightarrow> SProc (r', fr', exec_type_aux r pt, u) sp \<in> all_sobjs" |
|
742 | ap_clone: "SProc (r, fr, pt, u) sp \<in> all_sobjs \<Longrightarrow> SProc (r, fr, clone_type_aux r pt, u) sp \<in> all_sobjs" |
|
743 |
|
744 fun init_obj2sobj :: "t_object \<Rightarrow> t_sobject" |
|
745 where |
|
746 "init_obj2sobj (File f) = ( |
|
747 case (etype_aux init_file_type_aux f) of |
|
748 Some t \<Rightarrow> SFile (t, f) (Some f) |
|
749 | _ \<Rightarrow> Unknown )" |
|
750 | "init_obj2sobj (Proc p) = ( |
|
751 case (init_currentrole p, init_proc_forcedrole p, init_process_type p, init_owner p) of |
|
752 (Some r, Some fr, Some t, Some u) \<Rightarrow> SProc (r, fr, t, u) (Some p) |
|
753 | _ \<Rightarrow> Unknown )" |
|
754 | "init_obj2sobj (IPC i) = ( |
|
755 case (init_ipc_type i) of |
|
756 Some t \<Rightarrow> SIPC t (Some i) |
|
757 | _ \<Rightarrow> Unknown )" |
|
758 |
|
759 inductive_set tainted_s :: "t_sobject set" |
|
760 where |
|
761 ts_init: "obj \<in> seeds \<Longrightarrow> init_obj2sobj obj \<in> tainted_s" |
|
762 | ts_exec1: "\<lbrakk>SFile (t, sd) sf \<in> tainted_s; SProc (r, fr, pt, u) sp \<in> all_sobjs; (r, File_type t, EXECUTE) \<in> compatible; exec_role_aux r sd u = Some r'; erole_functor init_file_forcedrole InheritUpMixed sd = Some fr'\<rbrakk> \<Longrightarrow> SProc (r', fr', exec_type_aux r pt, u) sp \<in> tainted_s" |
|
763 | ts_exec2: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s; SFile (t, sd) sf \<in> all_sobjs; (r, File_type t, EXECUTE) \<in> compatible; exec_role_aux r sd u = Some r'; erole_functor init_file_forcedrole InheritUpMixed sd = Some fr'\<rbrakk> \<Longrightarrow> SProc (r', fr', exec_type_aux r pt, u) sp \<in> tainted_s" |
|
764 | ts_cfd: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s; SFile (t, sd) sf \<in> all_sobjs; default_fd_create_type r = NormalFile_type t'; (r, File_type t, WRITE) \<in> compatible; (r, File_type t', CREATE) \<in> compatible\<rbrakk> \<Longrightarrow> SFile (t', sd) None \<in> tainted_s" |
|
765 | ts_cfd': "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s; SFile (t, sd) sf \<in> all_sobjs; default_fd_create_type r = InheritParent_file_type; (r, File_type t, WRITE) \<in> compatible\<rbrakk> \<Longrightarrow> SFile (t, sd) None \<in> tainted_s" |
|
766 | ts_cipc: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s; (r, IPC_type (default_ipc_create_type r), CREATE) \<in> compatible\<rbrakk> \<Longrightarrow> SIPC (default_ipc_create_type r) None \<in> tainted_s" |
|
767 | ts_read: "\<lbrakk>SFile (t, sd) sf \<in> tainted_s; SProc (r, fr, pt, u) sp \<in> all_sobjs; (r, File_type t, READ) \<in> compatible\<rbrakk> \<Longrightarrow> SProc (r, fr, pt, u) sp \<in> tainted_s" |
|
768 | ts_write: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s; SFile (t, sd) sf \<in> all_sobjs; (r, File_type t, WRITE) \<in> compatible\<rbrakk> \<Longrightarrow> SFile (t, sd) sf \<in> tainted_s" |
|
769 | ts_recv: "\<lbrakk>SIPC t si \<in> tainted_s; SProc (r, fr, pt, u) sp \<in> all_sobjs; (r, IPC_type t, RECEIVE) \<in> compatible\<rbrakk> \<Longrightarrow> SProc (r, fr, pt, u) sp \<in> tainted_s" |
|
770 | ts_send: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s; SIPC t si \<in> all_sobjs; (r, IPC_type t, SEND) \<in> compatible\<rbrakk> \<Longrightarrow> SIPC t si \<in> tainted_s" |
|
771 | ts_crole: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s; r' \<in> comproles r\<rbrakk> \<Longrightarrow> SProc (r', fr, pt, u) sp \<in> tainted_s" |
|
772 | ts_chown: "\<lbrakk>SProc (r, fr, t, u') sp \<in> tainted_s; u \<in> init_users; chown_role_aux r fr u = Some nr; (r, Proc_type t, CHANGE_OWNER) \<in> compatible\<rbrakk> \<Longrightarrow> SProc (nr, fr, chown_type_aux r nr t, u) sp \<in> tainted_s" |
|
773 | ts_clone: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s; (r, Proc_type pt, CREATE) \<in> compatible\<rbrakk> \<Longrightarrow> SProc (r, fr, clone_type_aux r pt, u) sp \<in> tainted_s" |
|
774 |
|
775 (*** mapping function from dynamic 2 statical ****) |
|
776 |
|
777 fun source_dir:: "t_state \<Rightarrow> t_file \<Rightarrow> t_file option" |
|
778 where |
|
779 "source_dir s [] = (if ([] \<in> init_files \<and> \<not> (deleted (File []) s)) |
|
780 then Some [] |
|
781 else None |
|
782 )" |
|
783 | "source_dir s (f#pf) = (if ((f#pf) \<in> init_files \<and> \<not> (deleted (File (f#pf)) s)) |
|
784 then Some (f#pf) |
|
785 else source_dir s pf |
|
786 )" |
|
787 |
|
788 (* cf2sfile's properities should all be under condition: f is not deleted in \<tau>*) |
|
789 fun cf2sfile:: "t_state \<Rightarrow> t_file \<Rightarrow> t_sfile option" |
|
790 where |
|
791 "cf2sfile s f = (case (etype_of_file s f, source_dir s f) of |
|
792 (Some t, Some sd) \<Rightarrow> Some (t, sd) |
|
793 | _ \<Rightarrow> None)" |
|
794 |
|
795 fun cp2sproc:: "t_state \<Rightarrow> t_process \<Rightarrow> t_sprocess option" |
|
796 where |
|
797 "cp2sproc s p = (case (currentrole s p, proc_forcedrole s p, type_of_process s p, owner s p) of |
|
798 (Some r, Some fr, Some t, Some u) \<Rightarrow> Some (r, fr, t, u) |
|
799 | _ \<Rightarrow> None)" |
|
800 |
|
801 fun ci2sipc:: "t_state \<Rightarrow> t_ipc \<Rightarrow> t_sipc option" |
|
802 where |
|
803 "ci2sipc s i = (type_of_ipc s i)" |
|
804 |
|
805 (*** in statical view, clone event is process to try different runs(different sprocess:role/type...), |
|
806 so statically these sprocesses should have the same source: the process in the initial state *********) |
|
807 fun source_proc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process option" |
|
808 where |
|
809 "source_proc [] p = (if (p \<in> init_processes) then Some p else None)" |
|
810 | "source_proc (Clone p p' # s) p'' = (if (p'' = p') then source_proc s p else source_proc s p'')" |
|
811 | "source_proc (e # s) p = source_proc s p" |
|
812 |
|
813 fun obj2sobj :: "t_state \<Rightarrow> t_object \<Rightarrow> t_sobject" |
|
814 where |
|
815 "obj2sobj s (File f) = ( |
|
816 case (cf2sfile s f) of |
|
817 Some sf \<Rightarrow> (if (f \<in> init_files \<and> (\<not> deleted (File f) s)) |
|
818 then SFile sf (Some f) |
|
819 else SFile sf None) |
|
820 | _ \<Rightarrow> Unknown )" |
|
821 | "obj2sobj s (Proc p) = ( |
|
822 case (cp2sproc s p) of |
|
823 Some sp \<Rightarrow> SProc sp (source_proc s p) |
|
824 | _ \<Rightarrow> Unknown )" |
|
825 | "obj2sobj s (IPC i) = ( |
|
826 case (ci2sipc s i) of |
|
827 Some si \<Rightarrow> (if (i \<in> init_ipcs \<and> (\<not> deleted (IPC i) s)) |
|
828 then SIPC si (Some i) |
|
829 else SIPC si None) |
|
830 | _ \<Rightarrow> Unknown )" |
|
831 |
|
832 fun role_of_sproc :: "t_sprocess \<Rightarrow> t_normal_role" |
|
833 where |
|
834 "role_of_sproc (r, fr, pt, u) = r" |
|
835 |
|
836 fun source_of_sobj :: "t_sobject \<Rightarrow> t_object option" |
|
837 where |
|
838 "source_of_sobj (SFile sf tag) = (case tag of |
|
839 Some f \<Rightarrow> Some (File f) |
|
840 | _ \<Rightarrow> None)" |
|
841 | "source_of_sobj (SProc sp tag) = (case tag of |
|
842 Some p \<Rightarrow> Some (Proc p) |
|
843 | _ \<Rightarrow> None)" |
|
844 | "source_of_sobj (SIPC si tag) = (case tag of |
|
845 Some i \<Rightarrow> Some (IPC i) |
|
846 | _ \<Rightarrow> None)" |
|
847 | "source_of_sobj Unknown = None" |
|
848 |
|
849 definition taintable_s :: "t_object \<Rightarrow> bool" |
|
850 where |
|
851 "taintable_s obj \<equiv> \<exists>sobj. sobj \<in> tainted_s \<and> source_of_sobj sobj = Some obj" |
|
852 |
|
853 (* |
|
854 definition file_deletable_s:: "t_file \<Rightarrow> bool" |
|
855 where |
|
856 "file_deletable_s f \<equiv> \<forall> t sd srf. (SFile (t,sd) srf \<in> all_sobjs \<and> f \<preceq> sd \<longrightarrow> (\<exists> sp srp. SProc sp srp \<in> all_sobjs \<and> (role_of_sproc sp, File_type t, DELETE) \<in> compatible))" |
|
857 *) |
|
858 (* |
|
859 definition file_deletable_s:: "t_file \<Rightarrow> bool" |
|
860 where |
|
861 "file_deletable_s sd \<equiv> \<forall> f. (f \<in> init_files \<and> sd \<preceq> f \<longrightarrow> (\<exists> t sp srp. SProc sp srp \<in> all_sobjs \<and> etype_of_file [] f = Some t \<and> (role_of_sproc sp, File_type t, DELETE) \<in> compatible))"*) |
|
862 |
|
863 definition file_deletable_s:: "t_file \<Rightarrow> bool" |
|
864 where |
|
865 "file_deletable_s f \<equiv> \<exists> t sp srp. SProc sp srp \<in> all_sobjs \<and> etype_of_file [] f = Some t \<and> (role_of_sproc sp, File_type t, DELETE) \<in> compatible" |
|
866 |
|
867 definition proc_deletable_s:: "t_process \<Rightarrow> bool" |
|
868 where |
|
869 "proc_deletable_s p \<equiv> \<exists> r fr pt u sp' srp'. SProc (r,fr,pt,u) (Some p) \<in> all_sobjs \<and> SProc sp' srp' \<in> all_sobjs \<and> (role_of_sproc sp', Proc_type pt, DELETE) \<in> compatible" |
|
870 |
|
871 definition ipc_deletable_s:: "t_ipc \<Rightarrow> bool" |
|
872 where |
|
873 "ipc_deletable_s i \<equiv> \<exists> t sp srp. SProc sp srp \<in> all_sobjs \<and> type_of_ipc [] i = Some t \<and> (role_of_sproc sp, IPC_type t, DELETE) \<in> compatible" |
|
874 |
|
875 fun deletable_s :: "t_object \<Rightarrow> bool" |
|
876 where |
|
877 "deletable_s (Proc p) = (p \<in> init_processes \<and> proc_deletable_s p)" |
|
878 | "deletable_s (File f) = (f \<in> init_files \<and> file_deletable_s f)" |
|
879 | "deletable_s (IPC i) = (i \<in> init_ipcs \<and> ipc_deletable_s i)" |
|
880 |
|
881 definition undeletable_s:: "t_object \<Rightarrow> bool" |
|
882 where |
|
883 "undeletable_s obj \<equiv> exists [] obj \<and> \<not> deletable_s obj" |
|
884 |
|
885 end |
|
886 |
|
887 locale tainting_s_sound = tainting_s_complete + |
|
888 |
|
889 assumes |
|
890 clone_type_unchange: "\<And> r. default_process_create_type r = InheritParent_proc_type" |
|
891 (* this is for statically clone do not change anything ! ! so that, there're no rule for |
|
892 clone in all_sobjs and tainted_s *) |
|
893 and clone_no_limit: "\<And> r t. (r, Proc_type t, CREATE) \<in> compatible" |
|
894 |
|
895 begin |
|
896 |
|
897 (* the all_sobjs': the soundness view of all_sobjs, just remove the clone case, cause |
|
898 in this locale, clone doesn't change any information of such a sprocess*) |
|
899 inductive_set all_sobjs' :: "t_sobject set" |
|
900 where |
|
901 af'_init: "\<lbrakk>f \<in> init_files; etype_aux init_file_type_aux f = Some t\<rbrakk> \<Longrightarrow> SFile (t, f) (Some f) \<in> all_sobjs'" |
|
902 | af'_cfd: "\<lbrakk>SFile (t, sd) sf \<in> all_sobjs'; SProc (r, fr, pt, u) sp \<in> all_sobjs'; default_fd_create_type r = NormalFile_type t'; (r, File_type t, WRITE) \<in> compatible; (r, File_type t', CREATE) \<in> compatible\<rbrakk> \<Longrightarrow> SFile (t', sd) None \<in> all_sobjs'" |
|
903 | af'_cfd': "\<lbrakk>SFile (t, sd) sf \<in> all_sobjs'; SProc (r, fr, pt, u) sp \<in> all_sobjs'; default_fd_create_type r = InheritParent_file_type; (r, File_type t, WRITE) \<in> compatible\<rbrakk> \<Longrightarrow> SFile (t, sd) None \<in> all_sobjs'" |
|
904 |
|
905 | ai'_init: "init_ipc_type i = Some t \<Longrightarrow> SIPC t (Some i) \<in> all_sobjs'" |
|
906 | ai'_cipc: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> all_sobjs'; (r, IPC_type (default_ipc_create_type r), CREATE) \<in> compatible\<rbrakk> \<Longrightarrow> SIPC (default_ipc_create_type r) None \<in> all_sobjs'" |
|
907 |
|
908 | ap'_init: "\<lbrakk>init_currentrole p = Some r; init_proc_forcedrole p = Some fr; init_process_type p = Some t; init_owner p = Some u\<rbrakk> \<Longrightarrow> SProc (r, fr, t, u) (Some p) \<in> all_sobjs'" |
|
909 | ap'_crole: "\<lbrakk>SProc (r, fr, t, u) sp \<in> all_sobjs'; r' \<in> comproles r\<rbrakk> \<Longrightarrow> SProc (r', fr, t, u) sp \<in> all_sobjs'" |
|
910 | ap'_chown: "\<lbrakk>SProc (r, fr, t, u') sp \<in> all_sobjs'; u \<in> init_users; chown_role_aux r fr u = Some nr; (r, Proc_type t, CHANGE_OWNER) \<in> compatible\<rbrakk> \<Longrightarrow> SProc (nr, fr, chown_type_aux r nr t, u) sp \<in> all_sobjs'" |
|
911 | ap'_exec: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> all_sobjs'; SFile (t, sd) sf \<in> all_sobjs'; (r, File_type t, EXECUTE) \<in> compatible; exec_role_aux r sd u = Some r'; erole_functor init_file_forcedrole InheritUpMixed sd = Some fr'\<rbrakk> \<Longrightarrow> SProc (r', fr', exec_type_aux r pt, u) sp \<in> all_sobjs'" |
|
912 |
|
913 (* the tainted_s': the soundness view of all_sobjs, just remove the clone case, cause |
|
914 in this locale, clone doesn't change any information of such a sprocess*) |
|
915 inductive_set tainted_s' :: "t_sobject set" |
|
916 where |
|
917 ts'_init: "obj \<in> seeds \<Longrightarrow> init_obj2sobj obj \<in> tainted_s'" |
|
918 | ts'_exec1: "\<lbrakk>SFile (t, sd) sf \<in> tainted_s'; SProc (r, fr, pt, u) sp \<in> all_sobjs'; (r, File_type t, EXECUTE) \<in> compatible; exec_role_aux r sd u = Some r'; erole_functor init_file_forcedrole InheritUpMixed sd = Some fr'\<rbrakk> \<Longrightarrow> SProc (r', fr', exec_type_aux r pt, u) sp \<in> tainted_s'" |
|
919 | ts'_exec2: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s'; SFile (t, sd) sf \<in> all_sobjs'; (r, File_type t, EXECUTE) \<in> compatible; exec_role_aux r sd u = Some r'; erole_functor init_file_forcedrole InheritUpMixed sd = Some fr'\<rbrakk> \<Longrightarrow> SProc (r', fr', exec_type_aux r pt, u) sp \<in> tainted_s'" |
|
920 | ts'_cfd: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s'; SFile (t, sd) sf \<in> all_sobjs'; default_fd_create_type r = NormalFile_type t'; (r, File_type t, WRITE) \<in> compatible; (r, File_type t', CREATE) \<in> compatible\<rbrakk> \<Longrightarrow> SFile (t', sd) None \<in> tainted_s'" |
|
921 | ts'_cfd': "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s'; SFile (t, sd) sf \<in> all_sobjs'; default_fd_create_type r = InheritParent_file_type; (r, File_type t, WRITE) \<in> compatible\<rbrakk> \<Longrightarrow> SFile (t, sd) None \<in> tainted_s'" |
|
922 | ts'_cipc: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s'; (r, IPC_type (default_ipc_create_type r), CREATE) \<in> compatible\<rbrakk> \<Longrightarrow> SIPC (default_ipc_create_type r) None \<in> tainted_s'" |
|
923 | ts'_read: "\<lbrakk>SFile (t, sd) sf \<in> tainted_s'; SProc (r, fr, pt, u) sp \<in> all_sobjs'; (r, File_type t, READ) \<in> compatible\<rbrakk> \<Longrightarrow> SProc (r, fr, pt, u) sp \<in> tainted_s'" |
|
924 | ts'_write: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s'; SFile (t, sd) sf \<in> all_sobjs'; (r, File_type t, WRITE) \<in> compatible\<rbrakk> \<Longrightarrow> SFile (t, sd) sf \<in> tainted_s'" |
|
925 | ts'_recv: "\<lbrakk>SIPC t si \<in> tainted_s'; SProc (r, fr, pt, u) sp \<in> all_sobjs'; (r, IPC_type t, RECEIVE) \<in> compatible\<rbrakk> \<Longrightarrow> SProc (r, fr, pt, u) sp \<in> tainted_s'" |
|
926 | ts'_send: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s'; SIPC t si \<in> all_sobjs'; (r, IPC_type t, SEND) \<in> compatible\<rbrakk> \<Longrightarrow> SIPC t si \<in> tainted_s'" |
|
927 | ts'_crole: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s'; r' \<in> comproles r\<rbrakk> \<Longrightarrow> SProc (r', fr, pt, u) sp \<in> tainted_s'" |
|
928 | ts'_chown: "\<lbrakk>SProc (r, fr, t, u') sp \<in> tainted_s'; u \<in> init_users; chown_role_aux r fr u = Some nr; (r, Proc_type t, CHANGE_OWNER) \<in> compatible\<rbrakk> \<Longrightarrow> SProc (nr, fr, chown_type_aux r nr t, u) sp \<in> tainted_s'" |
|
929 |
|
930 fun sobj_source_eq_obj :: "t_sobject \<Rightarrow> t_object \<Rightarrow> bool" |
|
931 where |
|
932 "sobj_source_eq_obj (SFile sf None) (File f) = True" |
|
933 | "sobj_source_eq_obj (SFile sf (Some f')) (File f) = (f' = f)" |
|
934 | "sobj_source_eq_obj (SProc sp None) (Proc p) = True" |
|
935 | "sobj_source_eq_obj (SProc sp (Some p')) (Proc p) = (p' = p)" |
|
936 | "sobj_source_eq_obj (SIPC si None) (IPC i) = True" |
|
937 | "sobj_source_eq_obj (SIPC si (Some i')) (IPC i) = (i' = i)" |
|
938 | "sobj_source_eq_obj _ _ = False" |
|
939 |
|
940 fun not_both_sproc:: "t_sobject \<Rightarrow> t_sobject \<Rightarrow> bool" |
|
941 where |
|
942 "not_both_sproc (SProc sp srp) (SProc sp' srp') = False" |
|
943 | "not_both_sproc _ _ = True" |
|
944 |
|
945 (*** definitions for init processes statical informations reservation ***) |
|
946 |
|
947 definition initp_intact :: "t_state => bool" |
|
948 where |
|
949 "initp_intact s \<equiv> \<forall> p. p \<in> init_processes --> p \<in> current_procs s \<and> obj2sobj s (Proc p) = init_obj2sobj (Proc p)" |
|
950 |
|
951 definition initp_alter :: "t_state \<Rightarrow> t_process \<Rightarrow> bool" |
|
952 where |
|
953 "initp_alter s p \<equiv> \<exists> p'. p' \<in> current_procs s \<and> obj2sobj s (Proc p') = init_obj2sobj (Proc p)" |
|
954 |
|
955 definition initp_intact_butp :: "t_state \<Rightarrow> t_process \<Rightarrow> bool" |
|
956 where |
|
957 "initp_intact_butp s proc \<equiv> (\<forall> p. p \<in> init_processes \<and> p \<noteq> proc \<longrightarrow> p \<in> current_procs s \<and> obj2sobj s (Proc p) = init_obj2sobj (Proc p)) \<and> initp_alter s proc" |
|
958 |
|
959 fun initp_intact_but :: "t_state \<Rightarrow> t_sobject \<Rightarrow> bool" |
|
960 where |
|
961 "initp_intact_but s (SProc sp (Some p)) = initp_intact_butp s p" |
|
962 | "initp_intact_but s _ = initp_intact s" |
|
963 |
|
964 (*** how to generating new valid pathname for examples of CreateFile ***) |
|
965 |
|
966 definition all_fname_under_dir:: "t_file \<Rightarrow> t_state \<Rightarrow> t_fname set" |
|
967 where |
|
968 "all_fname_under_dir d \<tau> = {fn. \<exists> f. fn # d = f \<and> f \<in> current_files \<tau>}" |
|
969 |
|
970 fun fname_all_a:: "nat \<Rightarrow> t_fname" |
|
971 where |
|
972 "fname_all_a 0 = []" | |
|
973 "fname_all_a (Suc n) = ''a''@(fname_all_a n)" |
|
974 |
|
975 definition fname_length_set :: "t_fname set \<Rightarrow> nat set" |
|
976 where |
|
977 "fname_length_set fns = length`fns" |
|
978 |
|
979 definition next_fname:: "t_file \<Rightarrow> t_state \<Rightarrow> t_fname" |
|
980 where |
|
981 "next_fname pf \<tau> = fname_all_a ((Max (fname_length_set (all_fname_under_dir pf \<tau>))) + 1)" |
|
982 |
|
983 definition new_childf:: "t_file \<Rightarrow> t_state \<Rightarrow> t_file" |
|
984 where |
|
985 "new_childf pf \<tau> = next_fname pf \<tau> # pf" |
|
986 |
|
987 end |
|
988 |
|
989 end |
|
990 |