|
1 theory Static |
|
2 imports Static_type OS_type_def Flask_type Flask |
|
3 begin |
|
4 |
|
5 locale tainting_s = tainting |
|
6 |
|
7 begin |
|
8 |
|
9 (* |
|
10 definition init_sectxt_of_file:: "t_file \<Rightarrow> security_context_t option" |
|
11 where |
|
12 "init_sectxt_of_file f \<equiv> |
|
13 if (is_init_file f) then init_sectxt_of_obj (O_file f) |
|
14 else if (is_init_dir f) then init_sectxt_of_obj (O_dir f) |
|
15 else None" |
|
16 *) |
|
17 |
|
18 definition sroot :: "t_sfile" |
|
19 where |
|
20 "sroot \<equiv> (Init [], sec_of_root, None, {})" |
|
21 |
|
22 definition init_cf2sfile :: "t_file \<Rightarrow> t_sfile option" |
|
23 where |
|
24 "init_cf2sfile f \<equiv> |
|
25 case (parent f) of |
|
26 None \<Rightarrow> Some sroot |
|
27 | Some pf \<Rightarrow> if (is_init_file f) then |
|
28 (case (init_sectxt_of_obj (O_file f), init_sectxt_of_obj (O_dir pf), get_parentfs_ctxts [] pf) of |
|
29 (Some sec, Some psec, Some aseclist) \<Rightarrow> Some (Init f, sec, Some psec, set aseclist) |
|
30 | _ \<Rightarrow> None) else |
|
31 (case (init_sectxt_of_obj (O_dir f), init_sectxt_of_obj (O_dir pf), get_parentfs_ctxts [] pf) of |
|
32 (Some sec, Some psec, Some aseclist) \<Rightarrow> Some (Init f, sec, Some psec, set aseclist) |
|
33 | _ \<Rightarrow> None)" |
|
34 |
|
35 definition init_cf2sfiles :: "t_file \<Rightarrow> t_sfile set" |
|
36 where |
|
37 "init_cf2sfiles f \<equiv> {sf. \<exists>f' \<in> init_same_inode_files f. init_cf2sfile f' = Some sf}" |
|
38 |
|
39 definition init_cfd2sfd :: "t_process \<Rightarrow> t_fd \<Rightarrow> (security_context_t \<times> t_open_flags \<times> t_sfile) option" |
|
40 where |
|
41 "init_cfd2sfd p fd = |
|
42 (case (init_file_of_proc_fd p fd, init_oflags_of_proc_fd p fd, init_sectxt_of_obj (O_fd p fd)) of |
|
43 (Some f, Some flags, Some sec) \<Rightarrow> (case (init_cf2sfile f) of |
|
44 Some sf \<Rightarrow> Some (sec, flags, sf) |
|
45 | _ \<Rightarrow> None) |
|
46 | _ \<Rightarrow> None)" |
|
47 |
|
48 definition init_cfds2sfds :: "t_process \<Rightarrow> (security_context_t \<times> t_open_flags \<times> t_sfile) set" |
|
49 where |
|
50 "init_cfds2sfds p \<equiv> { sfd. \<exists> fd \<in> init_proc_file_fds p. init_cfd2sfd p fd = Some sfd}" |
|
51 |
|
52 (* |
|
53 definition init_ch2sshm :: "t_shm \<Rightarrow> t_sshm option" |
|
54 where |
|
55 "init_ch2sshm h \<equiv> (case (init_sectxt_of_obj (O_shm h)) of |
|
56 Some sec \<Rightarrow> Some (Init h, sec) |
|
57 | _ \<Rightarrow> None)" |
|
58 |
|
59 definition init_cph2spshs |
|
60 :: "t_process \<Rightarrow> (t_sshm \<times> t_shm_attach_flag) set" |
|
61 where |
|
62 "init_cph2spshs p \<equiv> {(sh, flag)| sh flag h. (p, flag) \<in> init_procs_of_shm h \<and> |
|
63 init_ch2sshm h = Some sh}" |
|
64 *) |
|
65 definition init_cp2sproc :: "t_process \<Rightarrow> t_sproc option" |
|
66 where |
|
67 "init_cp2sproc p \<equiv> (case (init_sectxt_of_obj (O_proc p)) of |
|
68 Some sec \<Rightarrow> Some (Init p, sec, (init_cfds2sfds p)) |
|
69 | None \<Rightarrow> None)" |
|
70 |
|
71 (* acient files of init-file |
|
72 definition init_o2s_afs :: "t_file \<Rightarrow> security_context_t set" |
|
73 where |
|
74 "init_o2s_afs f \<equiv> {sec. \<exists> f'. f' \<preceq> f \<and> init_sectxt_of_obj (O_dir f') = Some sec}" *) |
|
75 |
|
76 definition init_cm2smsg :: "t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsg option" |
|
77 where |
|
78 "init_cm2smsg q m \<equiv> (case (init_sectxt_of_obj (O_msg q m)) of |
|
79 Some sec \<Rightarrow> Some (Init m, sec, (O_msg q m) \<in> seeds) |
|
80 | _ \<Rightarrow> None)" |
|
81 |
|
82 fun init_cqm2sms :: "t_msgq \<Rightarrow> t_msg list \<Rightarrow> (t_smsg list) option" |
|
83 where |
|
84 "init_cqm2sms q [] = Some []" |
|
85 | "init_cqm2sms q (m#ms) = |
|
86 (case (init_cqm2sms q ms, init_cm2smsg q m) of |
|
87 (Some sms, Some sm) \<Rightarrow> Some (sm # sms) |
|
88 | _ \<Rightarrow> None)" |
|
89 |
|
90 definition init_cq2smsgq :: "t_msgq \<Rightarrow> t_smsgq option" |
|
91 where |
|
92 "init_cq2smsgq q \<equiv> (case (init_sectxt_of_obj (O_msgq q), init_cqm2sms q (init_msgs_of_queue q)) of |
|
93 (Some sec, Some sms) \<Rightarrow> Some (Init q, sec, sms) |
|
94 | _ \<Rightarrow> None)" |
|
95 |
|
96 fun init_obj2sobj :: "t_object \<Rightarrow> t_sobject option" |
|
97 where |
|
98 "init_obj2sobj (O_proc p) = |
|
99 (case (init_cp2sproc p) of |
|
100 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> seeds)) |
|
101 | _ \<Rightarrow> None)" |
|
102 | "init_obj2sobj (O_file f) = |
|
103 Some (S_file (init_cf2sfiles f) |
|
104 (\<exists> f'. f' \<in> (init_same_inode_files f) \<and> O_file f \<in> seeds))" |
|
105 | "init_obj2sobj (O_dir f) = |
|
106 (case (init_cf2sfile f) of |
|
107 Some sf \<Rightarrow> Some (S_dir sf) |
|
108 | _ \<Rightarrow> None)" |
|
109 | "init_obj2sobj (O_msgq q) = |
|
110 (case (init_cq2smsgq q) of |
|
111 Some sq \<Rightarrow> Some (S_msgq sq) |
|
112 | _ \<Rightarrow> None)" |
|
113 (* |
|
114 | "init_obj2sobj (O_shm h) = |
|
115 (case (init_ch2sshm h) of |
|
116 Some sh \<Rightarrow> Some (S_shm sh) |
|
117 | _ \<Rightarrow> None)" |
|
118 | "init_obj2sobj (O_msg q m) = |
|
119 (case (init_cq2smsgq q, init_cm2smsg q m) of |
|
120 (Some sq, Some sm) \<Rightarrow> Some (S_msg sq sm) |
|
121 | _ \<Rightarrow> None)" *) |
|
122 | "init_obj2sobj _ = None" |
|
123 |
|
124 definition |
|
125 "init_static_state \<equiv> {sobj. \<exists> obj. init_alive obj \<and> init_obj2sobj obj = Some sobj}" |
|
126 |
|
127 (**************** translation from dynamic to static *******************) |
|
128 |
|
129 definition cf2sfile :: "t_state \<Rightarrow> t_file \<Rightarrow> t_sfile option" |
|
130 where |
|
131 "cf2sfile s f \<equiv> |
|
132 case (parent f) of |
|
133 None \<Rightarrow> Some sroot |
|
134 | Some pf \<Rightarrow> if (is_file s f) |
|
135 then (case (sectxt_of_obj s (O_file f), sectxt_of_obj s (O_dir pf), get_parentfs_ctxts s pf) of |
|
136 (Some sec, Some psec, Some asecs) \<Rightarrow> |
|
137 Some (if (\<not> died (O_file f) s \<and> is_init_file f) then Init f else Created, sec, Some psec, set asecs) |
|
138 | _ \<Rightarrow> None) |
|
139 else (case (sectxt_of_obj s (O_dir f), sectxt_of_obj s (O_dir pf), get_parentfs_ctxts s pf) of |
|
140 (Some sec, Some psec, Some asecs) \<Rightarrow> |
|
141 Some (if (\<not> died (O_dir f) s \<and> is_init_dir f) then Init f else Created, sec, Some psec, set asecs) |
|
142 | _ \<Rightarrow> None)" |
|
143 |
|
144 definition cf2sfiles :: "t_state \<Rightarrow> t_file \<Rightarrow> t_sfile set" |
|
145 where |
|
146 "cf2sfiles s f \<equiv> {sf. \<exists> f' \<in> (same_inode_files s f). cf2sfile s f' = Some sf}" |
|
147 |
|
148 (* here cf2sfile is passed with True, because, process' fds are only for files not dirs *) |
|
149 definition cfd2sfd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd \<Rightarrow> t_sfd option" |
|
150 where |
|
151 "cfd2sfd s p fd \<equiv> |
|
152 (case (file_of_proc_fd s p fd, flags_of_proc_fd s p fd, sectxt_of_obj s (O_fd p fd)) of |
|
153 (Some f, Some flags, Some sec) \<Rightarrow> (case (cf2sfile s f) of |
|
154 Some sf \<Rightarrow> Some (sec, flags, sf) |
|
155 | _ \<Rightarrow> None) |
|
156 | _ \<Rightarrow> None)" |
|
157 |
|
158 |
|
159 definition cpfd2sfds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sfd set" |
|
160 where |
|
161 "cpfd2sfds s p \<equiv> {sfd. \<exists> fd \<in> proc_file_fds s p. cfd2sfd s p fd = Some sfd}" |
|
162 |
|
163 (* |
|
164 definition ch2sshm :: "t_state \<Rightarrow> t_shm \<Rightarrow> t_sshm option" |
|
165 where |
|
166 "ch2sshm s h \<equiv> (case (sectxt_of_obj s (O_shm h)) of |
|
167 Some sec \<Rightarrow> |
|
168 Some (if (\<not> died (O_shm h) s \<and> h \<in> init_shms) then Init h else Created, sec) |
|
169 | _ \<Rightarrow> None)" |
|
170 |
|
171 definition cph2spshs :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sproc_sshm set" |
|
172 where |
|
173 "cph2spshs s p \<equiv> {(sh, flag)| sh flag h. (p, flag) \<in> procs_of_shm s h \<and> ch2sshm s h = Some sh}" |
|
174 *) |
|
175 definition cp2sproc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sproc option" |
|
176 where |
|
177 "cp2sproc s p \<equiv> (case (sectxt_of_obj s (O_proc p)) of |
|
178 Some sec \<Rightarrow> |
|
179 Some (if (\<not> died (O_proc p) s \<and> p \<in> init_procs) then Init p else Created, sec, |
|
180 cpfd2sfds s p) |
|
181 | _ \<Rightarrow> None)" |
|
182 |
|
183 definition cm2smsg :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsg option" |
|
184 where |
|
185 "cm2smsg s q m \<equiv> (case (sectxt_of_obj s (O_msg q m)) of |
|
186 Some sec \<Rightarrow> |
|
187 Some (if (\<not> died (O_msg q m) s \<and> m \<in> set (init_msgs_of_queue q)) then Init m else Created, |
|
188 sec, O_msg q m \<in> tainted s) |
|
189 | _ \<Rightarrow> None)" |
|
190 |
|
191 fun cqm2sms:: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg list \<Rightarrow> (t_smsg list) option" |
|
192 where |
|
193 "cqm2sms s q [] = Some []" |
|
194 | "cqm2sms s q (m#ms) = |
|
195 (case (cqm2sms s q ms, cm2smsg s q m) of |
|
196 (Some sms, Some sm) \<Rightarrow> Some (sm#sms) |
|
197 | _ \<Rightarrow> None)" |
|
198 |
|
199 definition cq2smsgq :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_smsgq option" |
|
200 where |
|
201 "cq2smsgq s q \<equiv> (case (sectxt_of_obj s (O_msgq q), cqm2sms s q (msgs_of_queue s q)) of |
|
202 (Some sec, Some sms) \<Rightarrow> |
|
203 Some (if (\<not> died (O_msgq q) s \<and> q \<in> init_msgqs) then Init q else Created, |
|
204 sec, sms) |
|
205 | _ \<Rightarrow> None)" |
|
206 |
|
207 fun co2sobj :: "t_state \<Rightarrow> t_object \<Rightarrow> t_sobject option" |
|
208 where |
|
209 "co2sobj s (O_proc p) = |
|
210 (case (cp2sproc s p) of |
|
211 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s)) |
|
212 | _ \<Rightarrow> None)" |
|
213 | "co2sobj s (O_file f) = |
|
214 Some (S_file (cf2sfiles s f) (O_file f \<in> tainted s))" |
|
215 | "co2sobj s (O_dir f) = |
|
216 (case (cf2sfile s f) of |
|
217 Some sf \<Rightarrow> Some (S_dir sf) |
|
218 | _ \<Rightarrow> None)" |
|
219 | "co2sobj s (O_msgq q) = |
|
220 (case (cq2smsgq s q) of |
|
221 Some sq \<Rightarrow> Some (S_msgq sq) |
|
222 | _ \<Rightarrow> None)" |
|
223 (* |
|
224 | "co2sobj s (O_shm h) = |
|
225 (case (ch2sshm s h) of |
|
226 Some sh \<Rightarrow> Some (S_shm sh) |
|
227 | _ \<Rightarrow> None)" |
|
228 |
|
229 | "co2sobj s (O_msg q m) = |
|
230 (case (cq2smsgq s q, cm2smsg s q m) of |
|
231 (Some sq, Some sm) \<Rightarrow> Some (S_msg sq sm) |
|
232 | _ \<Rightarrow> None)" |
|
233 *) |
|
234 | "co2sobj s _ = None" |
|
235 |
|
236 |
|
237 definition s2ss :: "t_state \<Rightarrow> t_static_state" |
|
238 where |
|
239 "s2ss s \<equiv> {sobj. \<exists> obj. alive s obj \<and> co2sobj s obj = Some sobj}" |
|
240 |
|
241 |
|
242 (* ******************************************************** *) |
|
243 |
|
244 |
|
245 fun is_init_sfile :: "t_sfile \<Rightarrow> bool" |
|
246 where |
|
247 "is_init_sfile (Init _, sec, psec,asec) = True" |
|
248 | "is_init_sfile _ = False" |
|
249 |
|
250 fun is_many_sfile :: "t_sfile \<Rightarrow> bool" |
|
251 where |
|
252 "is_many_sfile (Created, sec, psec, asec) = True" |
|
253 | "is_many_sfile _ = False" |
|
254 |
|
255 fun is_init_sproc :: "t_sproc \<Rightarrow> bool" |
|
256 where |
|
257 "is_init_sproc (Init p, sec, fds) = True" |
|
258 | "is_init_sproc _ = False" |
|
259 |
|
260 fun is_many_sproc :: "t_sproc \<Rightarrow> bool" |
|
261 where |
|
262 "is_many_sproc (Created, sec,fds) = True" |
|
263 | "is_many_sproc _ = False" |
|
264 |
|
265 fun is_many_smsg :: "t_smsg \<Rightarrow> bool" |
|
266 where |
|
267 "is_many_smsg (Created,sec,tag) = True" |
|
268 | "is_many_smsg _ = False" |
|
269 |
|
270 (* wrong def |
|
271 fun is_many_smsgq :: "t_smsgq \<Rightarrow> bool" |
|
272 where |
|
273 "is_many_smsgq (Created,sec,sms) = (True \<and> (\<forall> sm \<in> (set sms). is_many_smsg sm))" |
|
274 | "is_many_smsgq _ = False" |
|
275 *) |
|
276 |
|
277 fun is_many_smsgq :: "t_smsgq \<Rightarrow> bool" |
|
278 where |
|
279 "is_many_smsgq (Created,sec,sms) = True" |
|
280 | "is_many_smsgq _ = False" |
|
281 (* |
|
282 fun is_many_sshm :: "t_sshm \<Rightarrow> bool" |
|
283 where |
|
284 "is_many_sshm (Created, sec) = True" |
|
285 | "is_many_sshm _ = False" |
|
286 *) |
|
287 fun is_many :: "t_sobject \<Rightarrow> bool" |
|
288 where |
|
289 "is_many (S_proc sp tag) = is_many_sproc sp" |
|
290 | "is_many (S_file sfs tag) = (\<forall> sf \<in> sfs. is_many_sfile sf)" |
|
291 | "is_many (S_dir sf ) = is_many_sfile sf" |
|
292 | "is_many (S_msgq sq ) = is_many_smsgq sq" |
|
293 (* |
|
294 | "is_many (S_shm sh ) = is_many_sshm sh" |
|
295 *) |
|
296 |
|
297 fun is_init_smsgq :: "t_smsgq \<Rightarrow> bool" |
|
298 where |
|
299 "is_init_smsgq (Init q,sec,sms) = True" |
|
300 | "is_init_smsgq _ = False" |
|
301 |
|
302 (* |
|
303 fun is_init_sshm :: "t_sshm \<Rightarrow> bool" |
|
304 where |
|
305 "is_init_sshm (Init h,sec) = True" |
|
306 | "is_init_sshm _ = False" |
|
307 *) |
|
308 fun is_init_sobj :: "t_sobject \<Rightarrow> bool" |
|
309 where |
|
310 "is_init_sobj (S_proc sp tag ) = is_init_sproc sp" |
|
311 | "is_init_sobj (S_file sfs tag) = (\<exists> sf \<in> sfs. is_init_sfile sf)" |
|
312 | "is_init_sobj (S_dir sf ) = is_init_sfile sf" |
|
313 | "is_init_sobj (S_msgq sq ) = is_init_smsgq sq" |
|
314 (* |
|
315 | "is_init_sobj (S_shm sh ) = is_init_sshm sh" |
|
316 *) |
|
317 (* |
|
318 fun update_ss_sp:: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state" |
|
319 where |
|
320 "update_ss_sp ss (S_proc sp tag) (S_proc sp' tag') = |
|
321 (if (is_many_sproc sp) then ss \<union> {S_proc sp' tag'} |
|
322 else (ss - {S_proc sp tag}) \<union> {S_proc sp' tag'})" |
|
323 |
|
324 fun update_ss_sd:: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state" |
|
325 where |
|
326 "update_ss_sd ss (S_dir sf tag) (S_dir sf' tag') = |
|
327 (if (is_many_sfile sf) then ss \<union> {S_dir sf' tag'} |
|
328 else (ss - {S_dir sf tag}) \<union> {S_dir sf' tag'})" |
|
329 *) |
|
330 |
|
331 (* |
|
332 fun sparent :: "t_sfile \<Rightarrow> t_sfile option" |
|
333 where |
|
334 "sparent (Sroot si sec) = None" |
|
335 | "sparent (Sfile si sec spf) = Some spf" |
|
336 |
|
337 inductive is_ancesf :: "t_sfile \<Rightarrow> t_sfile \<Rightarrow> bool" |
|
338 where |
|
339 "is_ancesf sf sf" |
|
340 | "sparent sf = Some spf \<Longrightarrow> is_ancesf spf sf" |
|
341 | "\<lbrakk>sparent sf = Some spf; is_ancesf saf spf\<rbrakk> \<Longrightarrow> is_ancesf saf sf" |
|
342 |
|
343 definition sfile_reparent :: "t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile" |
|
344 where |
|
345 "sfile_reparent (Sroot)" |
|
346 *) |
|
347 |
|
348 (* |
|
349 (* sfds rename aux definitions *) |
|
350 definition sfds_rename_notrelated |
|
351 :: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool" |
|
352 where |
|
353 "sfds_rename_notrelated sfds from to sfds' \<equiv> |
|
354 (\<forall> sec flag sf. (sec,flag,sf) \<in> sfds \<and> (\<not> from \<preceq> sf) \<longrightarrow> (sec,flag,sf) \<in> sfds')" |
|
355 |
|
356 definition sfds_rename_renamed |
|
357 :: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool" |
|
358 where |
|
359 "sfds_rename_renamed sfds sf from to sfds' \<equiv> |
|
360 (\<forall> sec flag sf'. (sec,flag,sf) \<in> sfds \<and> (sf \<preceq> sf') \<longrightarrow> |
|
361 (sec, flag, file_after_rename sf' from to) \<in> sfds' \<and> (sec,flag,sf) \<notin> sfds')" |
|
362 |
|
363 definition sfds_rename_remain |
|
364 :: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool" |
|
365 where |
|
366 "sfds_rename_remain sfds sf from to sfds' \<equiv> |
|
367 (\<forall> sec flag sf'. (sec,flag,sf') \<in> sfds \<and> (sf \<preceq> sf') \<longrightarrow> |
|
368 (sec, flag, sf') \<in> sfds' \<and> (sec,flag, file_after_rename sf' from to) \<notin> sfds')" |
|
369 |
|
370 (* for not many, choose on renamed or not *) |
|
371 definition sfds_rename_choices |
|
372 :: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool" |
|
373 where |
|
374 "sfds_rename_choices sfds sf from to sfds' \<equiv> |
|
375 sfds_rename_remain sfds sf from to sfds' \<or> sfds_rename_renamed sfds sf from to sfds'" |
|
376 |
|
377 (* for many, merge renamed with not renamed *) |
|
378 definition sfds_rename_both |
|
379 :: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool" |
|
380 where |
|
381 "sfds_rename_both sfds sf from to sfds' \<equiv> |
|
382 (\<forall> sec flag sf'. (sec,flag,sf') \<in> sfds \<and> (sf \<preceq> sf') \<longrightarrow> |
|
383 (sec, flag, sf') \<in> sfds' \<or> (sec,flag, file_after_rename sf' from to) \<in> sfds')" |
|
384 |
|
385 (* added to the new sfds, are those only under the new sfile *) |
|
386 definition sfds_rename_added |
|
387 :: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool" |
|
388 where |
|
389 "sfds_rename_added sfds from to sfds' \<equiv> |
|
390 (\<forall> sec' flag' sf' sec flag. (sec',flag',sf') \<in> sfds' \<and> (sec,flag,sf') \<notin> sfds \<longrightarrow> |
|
391 (\<exists> sf. (sec,flag,sf) \<in> sfds \<and> sf' = file_after_rename from to sf))" |
|
392 |
|
393 definition sproc_sfds_renamed |
|
394 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
395 where |
|
396 "sproc_sfds_renamed ss sf from to ss' \<equiv> |
|
397 (\<forall> pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \<in> ss \<longrightarrow> |
|
398 (\<exists> sfds'. S_proc (pi,sec,sfds',sshms) tagp \<in> ss \<and> sfds_rename_renamed sfds sf from to sfds'))" |
|
399 |
|
400 definition sproc_sfds_remain |
|
401 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
402 where |
|
403 "sproc_sfds_remain ss sf from to ss' \<equiv> |
|
404 (\<forall> pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \<in> ss \<longrightarrow> |
|
405 (\<exists> sfds'. S_proc (pi,sec,sfds',sshms) tagp \<in> ss \<and> sfds_rename_remain sfds sf from to sfds'))" |
|
406 |
|
407 (* for not many, choose on renamed or not *) |
|
408 definition sproc_sfds_choices |
|
409 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
410 where |
|
411 "sproc_sfds_choices ss sf from to ss' \<equiv> |
|
412 (\<forall> pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \<in> ss \<longrightarrow> |
|
413 (\<exists> sfds'. S_proc (pi,sec,sfds',sshms) tagp \<in> ss \<and> sfds_rename_choices sfds sf from to sfds'))" |
|
414 |
|
415 (* for many, merge renamed with not renamed *) |
|
416 definition sproc_sfds_both |
|
417 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
418 where |
|
419 "sproc_sfds_both ss sf from to ss' \<equiv> |
|
420 (\<forall> pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \<in> ss \<longrightarrow> |
|
421 (\<exists> sfds'. S_proc (pi,sec,sfds',sshms) tagp \<in> ss \<and> sfds_rename_both sfds sf from to sfds'))" |
|
422 |
|
423 (* remove (\<forall> sp tag. S_proc sp tag \<in> ss \<longrightarrow> S_proc sp tag \<in> ss'), |
|
424 * cause sfds contains sfs informations *) |
|
425 definition ss_rename_notrelated |
|
426 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
427 where |
|
428 "ss_rename_notrelated ss sf sf' ss' \<equiv> |
|
429 (\<forall> sq. S_msgq sq \<in> ss \<longrightarrow> S_msgq sq \<in> ss') \<and> |
|
430 (\<forall> pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \<in> ss \<longrightarrow> (\<exists> sfds'. |
|
431 S_proc (pi,sec,sfds',sshms) tagp \<in> ss'\<and> sfds_rename_notrelated sfds sf sf' sfds')) \<and> |
|
432 (\<forall> sfs sf'' tag. S_file sfs tag \<in> ss \<and> sf'' \<in> sfs \<and> (\<not> sf \<preceq> sf'') \<longrightarrow> (\<exists> sfs'. |
|
433 S_file sfs tag \<in> ss' \<and> sf'' \<in> sfs')) \<and> |
|
434 (\<forall> sf'' tag. S_dir sf'' tag \<in> ss \<and> (\<not> sf \<preceq> sf'') \<longrightarrow> S_dir sf'' tag \<in> ss')" |
|
435 |
|
436 (* rename from to, from should definited renamed if not many *) |
|
437 definition all_descendant_sf_renamed |
|
438 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
439 where |
|
440 "all_descendant_sf_renamed ss sf from to ss' \<equiv> |
|
441 (\<forall> sfs sf' tagf. sf \<preceq> sf' \<and> S_file sfs tagf \<in> ss \<and> sf' \<in> sfs \<longrightarrow> (\<exists> sfs'. |
|
442 S_file sfs' tagf \<in> ss' \<and> file_after_rename from to sf' \<in> sfs' \<and> sf' \<notin> sfs')) \<and> |
|
443 (\<forall> sf' tagf. sf \<preceq> sf' \<and> S_dir sf' tagf \<in> ss \<longrightarrow> S_dir (file_after_rename from to sf') tagf \<in> ss' \<and> S_dir sf' tagf \<notin> ss') \<and> |
|
444 sproc_sfds_renamed ss sf from to ss'" |
|
445 |
|
446 (* not renamed *) |
|
447 definition all_descendant_sf_remain |
|
448 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
449 where |
|
450 "all_descendant_sf_remain ss sf from to ss' \<equiv> |
|
451 (\<forall> sfs sf' tag'. sf \<preceq> sf' \<and> S_file sfs tag' \<in> ss \<and> sf' \<in> sfs \<longrightarrow> (\<exists> sfs'. |
|
452 S_file sfs' tag' \<in> ss \<and> file_after_rename from to sf' \<notin> sfs' \<and> sf' \<in> sfs')) \<and> |
|
453 (\<forall> sf' tag'. sf \<preceq> sf' \<and> S_dir sf' tag' \<in> ss \<longrightarrow> S_dir (file_after_rename from to sf') tag' \<notin> ss' \<and> S_dir sf' tag' \<in> ss') \<and> |
|
454 sproc_sfds_remain ss sf from to ss'" |
|
455 |
|
456 definition all_descendant_sf_choices |
|
457 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
458 where |
|
459 "all_descendant_sf_choices ss sf from to ss' \<equiv> |
|
460 all_descendant_sf_renamed ss sf from to ss' \<or> all_descendant_sf_remain ss sf from to ss'" |
|
461 |
|
462 definition all_descendant_sf_both |
|
463 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
464 where |
|
465 "all_descendant_sf_both ss sf from to ss' \<equiv> |
|
466 (\<forall> sfs sf' tag'. sf \<preceq> sf' \<and> S_file sfs tag' \<in> ss \<and> sf' \<in> sfs \<longrightarrow> (\<exists> sfs'. |
|
467 S_file sfs' tag' \<in> ss \<and> file_after_rename from to sf' \<in> sfs' \<or> sf' \<in> sfs')) \<and> |
|
468 (\<forall> sf' tag'. sf \<preceq> sf' \<and> S_dir sf' tag' \<in> ss \<longrightarrow> |
|
469 S_dir (file_after_rename from to sf') tag' \<in> ss' \<or> S_dir sf' tag' \<in> ss') \<and> |
|
470 sproc_sfds_both ss sf from to ss'" |
|
471 |
|
472 definition ss_renamed_file |
|
473 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
474 where |
|
475 "ss_renamed_file ss sf sf' ss' \<equiv> |
|
476 (if (is_many_sfile sf) |
|
477 then all_descendant_sf_choices ss sf sf sf' ss' |
|
478 else all_descendant_sf_renamed ss sf sf sf' ss')" |
|
479 |
|
480 (* added to the new sfs, are those only under the new sfile *) |
|
481 definition sfs_rename_added |
|
482 :: "t_sfile set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile set \<Rightarrow> bool" |
|
483 where |
|
484 "sfs_rename_added sfs from to sfs' \<equiv> |
|
485 (\<forall> sf'. sf' \<in> sfs' \<and> sf' \<notin> sfs \<longrightarrow> (\<exists> sf. sf \<in> sfs \<and> sf' = file_after_rename from to sf))" |
|
486 |
|
487 (* added to the new sfile, are those only under the new sfile *) |
|
488 definition ss_rename_added |
|
489 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
490 where |
|
491 "ss_rename_added ss from to ss' \<equiv> |
|
492 (\<forall> pi sec fds fds' shms tagp. S_proc (pi, sec, fds,shms) tagp \<in> ss \<and> |
|
493 S_proc (pi,sec,fds',shms) tagp \<in> ss' \<longrightarrow> sfds_rename_added fds from to fds') \<and> |
|
494 (\<forall> sq. S_msgq sq \<in> ss' \<longrightarrow> S_msgq sq \<in> ss) \<and> |
|
495 (\<forall> sfs sfs' tagf. S_file sfs' tagf \<in> ss' \<and> S_file sfs tagf \<in> ss \<longrightarrow> |
|
496 sfs_rename_added sfs from to sfs') \<and> |
|
497 (\<forall> sf' tagf. S_dir sf' tagf \<in> ss' \<and> S_dir sf' tagf \<notin> ss \<longrightarrow> |
|
498 (\<exists> sf. S_dir sf tagf \<in> ss \<and> sf' = file_after_rename from to sf))" |
|
499 |
|
500 definition sfile_alive :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> bool" |
|
501 where |
|
502 "sfile_alive ss sf \<equiv> (\<exists> sfs tagf. sf \<in> sfs \<and> S_file sfs tagf \<in> ss)" |
|
503 |
|
504 definition sf_alive :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> bool" |
|
505 where |
|
506 "sf_alive ss sf \<equiv> (\<exists> tagd. S_dir sf tagd \<in> ss) \<or> sfile_alive ss sf" |
|
507 |
|
508 (* constrains that the new static state should satisfy *) |
|
509 definition ss_rename:: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
510 where |
|
511 "ss_rename ss sf sf' ss' \<equiv> |
|
512 ss_rename_notrelated ss sf sf' ss' \<and> |
|
513 ss_renamed_file ss sf sf' ss' \<and> ss_rename_added ss sf sf' ss' \<and> |
|
514 (\<forall> sf''. sf_alive ss sf'' \<and> sf \<prec> sf'' \<longrightarrow> |
|
515 (if (is_many_sfile sf'') |
|
516 then all_descendant_sf_choices ss sf'' sf sf' ss' |
|
517 else all_descendant_sf_both ss sf'' sf sf' ss'))" |
|
518 |
|
519 (* two sfile, the last fname should not be equal *) |
|
520 fun sfile_same_fname:: "t_sfile \<Rightarrow> t_sfile \<Rightarrow> bool" |
|
521 where |
|
522 "sfile_same_fname ((Init n, sec)#spf) ((Init n', sec')#spf') = (n = n')" |
|
523 | "sfile_same_fname _ _ = False" |
|
524 |
|
525 (* no same init sfile/only sfile in the target-to spf, should be in static_state addmissble check *) |
|
526 definition ss_rename_no_same_fname:: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> bool" |
|
527 where |
|
528 "ss_rename_no_same_fname ss from spf \<equiv> |
|
529 \<not> (\<exists> to. sfile_same_fname from to \<and> parent to = Some spf \<and> sf_alive ss to)" |
|
530 |
|
531 (* is not a function, is a relation (one 2 many) |
|
532 definition update_ss_rename :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state" |
|
533 where |
|
534 "update_ss_rename ss sf sf' \<equiv> if (is_many_sfile sf) |
|
535 then (ss \<union> {S_file (file_after_rename sf sf' sf'') tag | sf'' tag. sf \<preceq> sf'' \<and> S_file sf'' tag \<in> ss} |
|
536 \<union> {S_dir (file_after_rename sf sf' sf'') tag | sf'' tag. sf \<preceq> sf'' \<and> S_dir sf'' tag \<in> ss}) |
|
537 else (ss - {S_file sf'' tag | sf'' tag. sf \<preceq> sf'' \<and> S_file sf'' tag \<in> ss} |
|
538 - {S_dir sf'' tag | sf'' tag. sf \<preceq> sf'' \<and> S_dir sf'' tag \<in> ss}) |
|
539 \<union> {S_file (file_after_rename sf sf' sf'') tag | sf'' tag. sf \<preceq> sf'' \<and> S_file sf'' tag \<in> ss} |
|
540 \<union> {S_dir (file_after_rename sf sf' sf'') tag | sf'' tag. sf \<preceq> sf'' \<and> S_dir sf'' tag \<in> ss}" |
|
541 *) |
|
542 *) |
|
543 |
|
544 fun sectxt_of_sproc :: "t_sproc \<Rightarrow> security_context_t" |
|
545 where |
|
546 "sectxt_of_sproc (pi,sec,fds) = sec" |
|
547 |
|
548 fun sectxt_of_sfile :: "t_sfile \<Rightarrow> security_context_t" |
|
549 where |
|
550 "sectxt_of_sfile (fi,sec,psec,asecs) = sec" |
|
551 |
|
552 fun asecs_of_sfile :: "t_sfile \<Rightarrow> security_context_t set" |
|
553 where |
|
554 "asecs_of_sfile (fi,sec,psec,asecs) = asecs" |
|
555 |
|
556 definition search_check_s :: "security_context_t \<Rightarrow> t_sfile \<Rightarrow> bool \<Rightarrow> bool" |
|
557 where |
|
558 "search_check_s pctxt sf if_file = |
|
559 (if if_file |
|
560 then search_check_ctxt pctxt (sectxt_of_sfile sf) (asecs_of_sfile sf) True |
|
561 else search_check_ctxt pctxt (sectxt_of_sfile sf) (asecs_of_sfile sf) False)" |
|
562 |
|
563 definition sectxts_of_sfds :: "t_sfd set \<Rightarrow> security_context_t set" |
|
564 where |
|
565 "sectxts_of_sfds sfds \<equiv> {ctxt. \<exists> flag sf. (ctxt, flag, sf) \<in> sfds}" |
|
566 |
|
567 definition inherit_fds_check_s :: "security_context_t \<Rightarrow> t_sfd set \<Rightarrow> bool" |
|
568 where |
|
569 "inherit_fds_check_s pctxt sfds \<equiv> inherit_fds_check_ctxt pctxt (sectxts_of_sfds sfds)" |
|
570 |
|
571 (* |
|
572 definition sectxts_of_sproc_sshms :: "t_sproc_sshm set \<Rightarrow> security_context_t set" |
|
573 where |
|
574 "sectxts_of_sproc_sshms sshms \<equiv> {ctxt. \<exists> hi flag. ((hi, ctxt),flag) \<in> sshms}" |
|
575 |
|
576 definition inherit_shms_check_s :: "security_context_t \<Rightarrow> t_sproc_sshm set \<Rightarrow> bool" |
|
577 where |
|
578 "inherit_shms_check_s pctxt sshms \<equiv> inherit_shms_check_ctxt pctxt (sectxts_of_sproc_sshms sshms)" |
|
579 |
|
580 fun info_flow_sshm :: "t_sproc \<Rightarrow> t_sproc \<Rightarrow> bool" |
|
581 where |
|
582 "info_flow_sshm (pi,sec,fds,shms) (pi',sec',fds',shms') = |
|
583 (\<exists> sh flag'. (sh, SHM_RDWR) \<in> shms \<and> (sh, flag') \<in> shms')" |
|
584 |
|
585 definition info_flow_sproc_sshms :: "t_sproc_sshm set \<Rightarrow> t_sproc_sshm set \<Rightarrow> bool" |
|
586 where |
|
587 "info_flow_sproc_sshms shms shms' \<equiv> (\<exists> sh flag'. (sh, SHM_RDWR) \<in> shms \<and> (sh, flag') \<in> shms')" |
|
588 |
|
589 |
|
590 fun info_flow_sshm :: "t_sproc \<Rightarrow> t_sproc \<Rightarrow> bool" |
|
591 where |
|
592 "info_flow_sshm (pi,sec,fds,shms) (pi',sec',fds',shms') = info_flow_sproc_sshms shms shms'" |
|
593 |
|
594 inductive info_flow_sshm :: "t_sproc \<Rightarrow> t_sproc \<Rightarrow> bool" |
|
595 where |
|
596 "info_flow_sshm sp sp" |
|
597 | "\<lbrakk>info_flow_sshm sp (pi,sec,fds,shms); info_flow_sproc_sshms shms shms'\<rbrakk> |
|
598 \<Longrightarrow> info_flow_sshm sp (pi',sec',fds',shms')" |
|
599 *) |
|
600 |
|
601 (* |
|
602 fun smsg_related :: "t_msg \<Rightarrow> t_smsg list \<Rightarrow> bool" |
|
603 where |
|
604 "smsg_related m [] = False" |
|
605 | "smsg_related m ((mi, sec, tag)#sms) = |
|
606 (if (mi = Init m) then True else smsg_related m sms)" |
|
607 |
|
608 fun smsgq_smsg_related :: "t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsgq \<Rightarrow> bool" |
|
609 where |
|
610 "smsgq_smsg_related q m (qi, sec, smsgslist) = ((qi = Init q) \<and> (smsg_related m smsgslist))" |
|
611 |
|
612 fun smsg_relatainted :: "t_msg \<Rightarrow> t_smsg list \<Rightarrow> bool" |
|
613 where |
|
614 "smsg_relatainted m [] = False" |
|
615 | "smsg_relatainted m ((mi, sec, tag)#sms) = |
|
616 (if (mi = Init m \<and> tag = True) then True else smsg_relatainted m sms)" |
|
617 |
|
618 fun smsgq_smsg_relatainted :: "t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsgq \<Rightarrow> bool" |
|
619 where |
|
620 "smsgq_smsg_relatainted q m (qi, sec, smsgslist) = |
|
621 ((qi = Init q) \<and> (smsg_relatainted m smsgslist))" |
|
622 *) |
|
623 |
|
624 fun sfile_related :: "t_sfile \<Rightarrow> t_file \<Rightarrow> bool" |
|
625 where |
|
626 "sfile_related (fi,sec,psec,asecs) f = (fi = Init f)" |
|
627 (* |
|
628 fun sproc_related :: "t_process \<Rightarrow> t_sproc \<Rightarrow> bool" |
|
629 where |
|
630 "sproc_related p (pi, sec, fds, shms) = (pi = Init p)" |
|
631 *) |
|
632 fun init_obj_related :: "t_sobject \<Rightarrow> t_object \<Rightarrow> bool" |
|
633 where |
|
634 "init_obj_related (S_proc (pi, sec, fds) tag) (O_proc p') = (pi = Init p')" |
|
635 | "init_obj_related (S_file sfs tag) (O_file f) = (\<exists> sf \<in> sfs. sfile_related sf f)" |
|
636 | "init_obj_related (S_dir sf) (O_dir f) = (sfile_related sf f)" |
|
637 | "init_obj_related (S_msgq (qi, sec, sms)) (O_msgq q') = (qi = Init q')" |
|
638 (* |
|
639 | "init_obj_related (S_shm (hi, sec)) (O_shm h') = (hi = Init h')" |
|
640 |
|
641 | "init_obj_related (S_msg (qi, sec, sms) (mi, secm, tagm)) (O_msg q' m') = (qi = Init q' \<and> mi = Init m')" |
|
642 *) |
|
643 | "init_obj_related _ _ = False" |
|
644 |
|
645 |
|
646 |
|
647 (***************** for backward proof when Instancing static objects ******************) |
|
648 |
|
649 fun all_procs :: "t_state \<Rightarrow> t_process set" |
|
650 where |
|
651 "all_procs [] = init_procs" |
|
652 | "all_procs (Clone p p' fds # s) = insert p' (all_procs s)" |
|
653 | "all_procs (e # s) = all_procs s" |
|
654 |
|
655 definition next_nat :: "nat set \<Rightarrow> nat" |
|
656 where |
|
657 "next_nat nset = (Max nset) + 1" |
|
658 |
|
659 definition new_proc :: "t_state \<Rightarrow> t_process" |
|
660 where |
|
661 "new_proc \<tau> = next_nat (current_procs \<tau>)" |
|
662 |
|
663 definition brandnew_proc :: "t_state \<Rightarrow> t_process" |
|
664 where |
|
665 "brandnew_proc s \<equiv> next_nat (all_procs s)" |
|
666 |
|
667 fun remove_create_flag :: "t_open_flags \<Rightarrow> t_open_flags" |
|
668 where |
|
669 "remove_create_flag (mflag, oflags) = (mflag, oflags - {OF_CREAT})" |
|
670 |
|
671 definition new_inode_num :: "t_state \<Rightarrow> nat" |
|
672 where |
|
673 "new_inode_num \<tau> = next_nat (current_inode_nums \<tau>)" |
|
674 |
|
675 definition new_msgq :: "t_state \<Rightarrow> t_msgq" |
|
676 where |
|
677 "new_msgq s = next_nat (current_msgqs s)" |
|
678 |
|
679 definition new_msg :: "t_state \<Rightarrow> t_msgq \<Rightarrow> nat" |
|
680 where |
|
681 "new_msg s q = next_nat (set (msgs_of_queue s q))" |
|
682 |
|
683 (* |
|
684 definition new_shm :: "t_state \<Rightarrow> nat" |
|
685 where |
|
686 "new_shm \<tau> = next_nat (current_shms \<tau>)" |
|
687 *) |
|
688 |
|
689 definition new_proc_fd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd" |
|
690 where |
|
691 "new_proc_fd \<tau> p = next_nat (current_proc_fds \<tau> p)" |
|
692 |
|
693 definition all_fname_under_dir:: "t_file \<Rightarrow> t_state \<Rightarrow> t_fname set" |
|
694 where |
|
695 "all_fname_under_dir d \<tau> = {fn. \<exists> f. fn # d = f \<and> f \<in> current_files \<tau>}" |
|
696 |
|
697 fun fname_all_a:: "nat \<Rightarrow> t_fname" |
|
698 where |
|
699 "fname_all_a 0 = []" | |
|
700 "fname_all_a (Suc n) = ''a''@(fname_all_a n)" |
|
701 |
|
702 definition fname_length_set :: "t_fname set \<Rightarrow> nat set" |
|
703 where |
|
704 "fname_length_set fns = length`fns" |
|
705 |
|
706 definition next_fname:: "t_file \<Rightarrow> t_state \<Rightarrow> t_fname" |
|
707 where |
|
708 "next_fname pf \<tau> = fname_all_a ((Max (fname_length_set (all_fname_under_dir pf \<tau>))) + 1)" |
|
709 |
|
710 definition new_childf:: "t_file \<Rightarrow> t_state \<Rightarrow> t_file" |
|
711 where |
|
712 "new_childf pf \<tau> = next_fname pf \<tau> # pf" |
|
713 |
|
714 end |
|
715 |
|
716 end |