120 | "init_obj2sobj _ = None" |
120 | "init_obj2sobj _ = None" |
121 |
121 |
122 definition |
122 definition |
123 "init_static_state \<equiv> {sobj. \<exists> obj. init_alive obj \<and> init_obj2sobj obj = Some sobj}" |
123 "init_static_state \<equiv> {sobj. \<exists> obj. init_alive obj \<and> init_obj2sobj obj = Some sobj}" |
124 |
124 |
125 fun is_init_sfile :: "t_sfile \<Rightarrow> bool" |
|
126 where |
|
127 "is_init_sfile (Init _, sec, psec,asec) = True" |
|
128 | "is_init_sfile _ = False" |
|
129 |
|
130 fun is_many_sfile :: "t_sfile \<Rightarrow> bool" |
|
131 where |
|
132 "is_many_sfile (Created, sec, psec, asec) = True" |
|
133 | "is_many_sfile _ = False" |
|
134 |
|
135 fun is_init_sproc :: "t_sproc \<Rightarrow> bool" |
|
136 where |
|
137 "is_init_sproc (Init p, sec, fds, shms) = True" |
|
138 | "is_init_sproc _ = False" |
|
139 |
|
140 fun is_many_sproc :: "t_sproc \<Rightarrow> bool" |
|
141 where |
|
142 "is_many_sproc (Created, sec,fds,shms) = True" |
|
143 | "is_many_sproc _ = False" |
|
144 |
|
145 fun is_many_smsg :: "t_smsg \<Rightarrow> bool" |
|
146 where |
|
147 "is_many_smsg (Created,sec,tag) = True" |
|
148 | "is_many_smsg _ = False" |
|
149 |
|
150 (* wrong def |
|
151 fun is_many_smsgq :: "t_smsgq \<Rightarrow> bool" |
|
152 where |
|
153 "is_many_smsgq (Created,sec,sms) = (True \<and> (\<forall> sm \<in> (set sms). is_many_smsg sm))" |
|
154 | "is_many_smsgq _ = False" |
|
155 *) |
|
156 |
|
157 fun is_many_smsgq :: "t_smsgq \<Rightarrow> bool" |
|
158 where |
|
159 "is_many_smsgq (Created,sec,sms) = True" |
|
160 | "is_many_smsgq _ = False" |
|
161 |
|
162 fun is_many_sshm :: "t_sshm \<Rightarrow> bool" |
|
163 where |
|
164 "is_many_sshm (Created, sec) = True" |
|
165 | "is_many_sshm _ = False" |
|
166 |
|
167 fun is_many :: "t_sobject \<Rightarrow> bool" |
|
168 where |
|
169 "is_many (S_proc sp tag) = is_many_sproc sp" |
|
170 | "is_many (S_file sfs tag) = (\<forall> sf \<in> sfs. is_many_sfile sf)" |
|
171 | "is_many (S_dir sf ) = is_many_sfile sf" |
|
172 | "is_many (S_msgq sq ) = is_many_smsgq sq" |
|
173 | "is_many (S_shm sh ) = is_many_sshm sh" |
|
174 |
|
175 fun is_init_smsgq :: "t_smsgq \<Rightarrow> bool" |
|
176 where |
|
177 "is_init_smsgq (Init q,sec,sms) = True" |
|
178 | "is_init_smsgq _ = False" |
|
179 |
|
180 fun is_init_sshm :: "t_sshm \<Rightarrow> bool" |
|
181 where |
|
182 "is_init_sshm (Init h,sec) = True" |
|
183 | "is_init_sshm _ = False" |
|
184 |
|
185 fun is_init_sobj :: "t_sobject \<Rightarrow> bool" |
|
186 where |
|
187 "is_init_sobj (S_proc sp tag ) = is_init_sproc sp" |
|
188 | "is_init_sobj (S_file sfs tag) = (\<exists> sf \<in> sfs. is_init_sfile sf)" |
|
189 | "is_init_sobj (S_dir sf ) = is_init_sfile sf" |
|
190 | "is_init_sobj (S_msgq sq ) = is_init_smsgq sq" |
|
191 | "is_init_sobj (S_shm sh ) = is_init_sshm sh" |
|
192 |
|
193 (* |
|
194 fun update_ss_sp:: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state" |
|
195 where |
|
196 "update_ss_sp ss (S_proc sp tag) (S_proc sp' tag') = |
|
197 (if (is_many_sproc sp) then ss \<union> {S_proc sp' tag'} |
|
198 else (ss - {S_proc sp tag}) \<union> {S_proc sp' tag'})" |
|
199 |
|
200 fun update_ss_sd:: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state" |
|
201 where |
|
202 "update_ss_sd ss (S_dir sf tag) (S_dir sf' tag') = |
|
203 (if (is_many_sfile sf) then ss \<union> {S_dir sf' tag'} |
|
204 else (ss - {S_dir sf tag}) \<union> {S_dir sf' tag'})" |
|
205 *) |
|
206 |
|
207 definition update_ss :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state" |
|
208 where |
|
209 "update_ss ss so so' \<equiv> if (is_many so) then ss \<union> {so'} else (ss - {so}) \<union> {so'}" |
|
210 |
|
211 definition add_ss :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_static_state" |
|
212 where |
|
213 "add_ss ss so \<equiv> ss \<union> {so}" |
|
214 |
|
215 definition del_ss :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_static_state" |
|
216 where |
|
217 "del_ss ss so \<equiv> if (is_many so) then ss else ss - {so}" |
|
218 |
|
219 (* |
|
220 fun sparent :: "t_sfile \<Rightarrow> t_sfile option" |
|
221 where |
|
222 "sparent (Sroot si sec) = None" |
|
223 | "sparent (Sfile si sec spf) = Some spf" |
|
224 |
|
225 inductive is_ancesf :: "t_sfile \<Rightarrow> t_sfile \<Rightarrow> bool" |
|
226 where |
|
227 "is_ancesf sf sf" |
|
228 | "sparent sf = Some spf \<Longrightarrow> is_ancesf spf sf" |
|
229 | "\<lbrakk>sparent sf = Some spf; is_ancesf saf spf\<rbrakk> \<Longrightarrow> is_ancesf saf sf" |
|
230 |
|
231 definition sfile_reparent :: "t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile" |
|
232 where |
|
233 "sfile_reparent (Sroot)" |
|
234 *) |
|
235 |
|
236 (* |
|
237 (* sfds rename aux definitions *) |
|
238 definition sfds_rename_notrelated |
|
239 :: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool" |
|
240 where |
|
241 "sfds_rename_notrelated sfds from to sfds' \<equiv> |
|
242 (\<forall> sec flag sf. (sec,flag,sf) \<in> sfds \<and> (\<not> from \<preceq> sf) \<longrightarrow> (sec,flag,sf) \<in> sfds')" |
|
243 |
|
244 definition sfds_rename_renamed |
|
245 :: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool" |
|
246 where |
|
247 "sfds_rename_renamed sfds sf from to sfds' \<equiv> |
|
248 (\<forall> sec flag sf'. (sec,flag,sf) \<in> sfds \<and> (sf \<preceq> sf') \<longrightarrow> |
|
249 (sec, flag, file_after_rename sf' from to) \<in> sfds' \<and> (sec,flag,sf) \<notin> sfds')" |
|
250 |
|
251 definition sfds_rename_remain |
|
252 :: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool" |
|
253 where |
|
254 "sfds_rename_remain sfds sf from to sfds' \<equiv> |
|
255 (\<forall> sec flag sf'. (sec,flag,sf') \<in> sfds \<and> (sf \<preceq> sf') \<longrightarrow> |
|
256 (sec, flag, sf') \<in> sfds' \<and> (sec,flag, file_after_rename sf' from to) \<notin> sfds')" |
|
257 |
|
258 (* for not many, choose on renamed or not *) |
|
259 definition sfds_rename_choices |
|
260 :: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool" |
|
261 where |
|
262 "sfds_rename_choices sfds sf from to sfds' \<equiv> |
|
263 sfds_rename_remain sfds sf from to sfds' \<or> sfds_rename_renamed sfds sf from to sfds'" |
|
264 |
|
265 (* for many, merge renamed with not renamed *) |
|
266 definition sfds_rename_both |
|
267 :: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool" |
|
268 where |
|
269 "sfds_rename_both sfds sf from to sfds' \<equiv> |
|
270 (\<forall> sec flag sf'. (sec,flag,sf') \<in> sfds \<and> (sf \<preceq> sf') \<longrightarrow> |
|
271 (sec, flag, sf') \<in> sfds' \<or> (sec,flag, file_after_rename sf' from to) \<in> sfds')" |
|
272 |
|
273 (* added to the new sfds, are those only under the new sfile *) |
|
274 definition sfds_rename_added |
|
275 :: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool" |
|
276 where |
|
277 "sfds_rename_added sfds from to sfds' \<equiv> |
|
278 (\<forall> sec' flag' sf' sec flag. (sec',flag',sf') \<in> sfds' \<and> (sec,flag,sf') \<notin> sfds \<longrightarrow> |
|
279 (\<exists> sf. (sec,flag,sf) \<in> sfds \<and> sf' = file_after_rename from to sf))" |
|
280 |
|
281 definition sproc_sfds_renamed |
|
282 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
283 where |
|
284 "sproc_sfds_renamed ss sf from to ss' \<equiv> |
|
285 (\<forall> pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \<in> ss \<longrightarrow> |
|
286 (\<exists> sfds'. S_proc (pi,sec,sfds',sshms) tagp \<in> ss \<and> sfds_rename_renamed sfds sf from to sfds'))" |
|
287 |
|
288 definition sproc_sfds_remain |
|
289 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
290 where |
|
291 "sproc_sfds_remain ss sf from to ss' \<equiv> |
|
292 (\<forall> pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \<in> ss \<longrightarrow> |
|
293 (\<exists> sfds'. S_proc (pi,sec,sfds',sshms) tagp \<in> ss \<and> sfds_rename_remain sfds sf from to sfds'))" |
|
294 |
|
295 (* for not many, choose on renamed or not *) |
|
296 definition sproc_sfds_choices |
|
297 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
298 where |
|
299 "sproc_sfds_choices ss sf from to ss' \<equiv> |
|
300 (\<forall> pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \<in> ss \<longrightarrow> |
|
301 (\<exists> sfds'. S_proc (pi,sec,sfds',sshms) tagp \<in> ss \<and> sfds_rename_choices sfds sf from to sfds'))" |
|
302 |
|
303 (* for many, merge renamed with not renamed *) |
|
304 definition sproc_sfds_both |
|
305 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
306 where |
|
307 "sproc_sfds_both ss sf from to ss' \<equiv> |
|
308 (\<forall> pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \<in> ss \<longrightarrow> |
|
309 (\<exists> sfds'. S_proc (pi,sec,sfds',sshms) tagp \<in> ss \<and> sfds_rename_both sfds sf from to sfds'))" |
|
310 |
|
311 (* remove (\<forall> sp tag. S_proc sp tag \<in> ss \<longrightarrow> S_proc sp tag \<in> ss'), |
|
312 * cause sfds contains sfs informations *) |
|
313 definition ss_rename_notrelated |
|
314 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
315 where |
|
316 "ss_rename_notrelated ss sf sf' ss' \<equiv> |
|
317 (\<forall> sq. S_msgq sq \<in> ss \<longrightarrow> S_msgq sq \<in> ss') \<and> |
|
318 (\<forall> pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \<in> ss \<longrightarrow> (\<exists> sfds'. |
|
319 S_proc (pi,sec,sfds',sshms) tagp \<in> ss'\<and> sfds_rename_notrelated sfds sf sf' sfds')) \<and> |
|
320 (\<forall> sfs sf'' tag. S_file sfs tag \<in> ss \<and> sf'' \<in> sfs \<and> (\<not> sf \<preceq> sf'') \<longrightarrow> (\<exists> sfs'. |
|
321 S_file sfs tag \<in> ss' \<and> sf'' \<in> sfs')) \<and> |
|
322 (\<forall> sf'' tag. S_dir sf'' tag \<in> ss \<and> (\<not> sf \<preceq> sf'') \<longrightarrow> S_dir sf'' tag \<in> ss')" |
|
323 |
|
324 (* rename from to, from should definited renamed if not many *) |
|
325 definition all_descendant_sf_renamed |
|
326 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
327 where |
|
328 "all_descendant_sf_renamed ss sf from to ss' \<equiv> |
|
329 (\<forall> sfs sf' tagf. sf \<preceq> sf' \<and> S_file sfs tagf \<in> ss \<and> sf' \<in> sfs \<longrightarrow> (\<exists> sfs'. |
|
330 S_file sfs' tagf \<in> ss' \<and> file_after_rename from to sf' \<in> sfs' \<and> sf' \<notin> sfs')) \<and> |
|
331 (\<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> |
|
332 sproc_sfds_renamed ss sf from to ss'" |
|
333 |
|
334 (* not renamed *) |
|
335 definition all_descendant_sf_remain |
|
336 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
337 where |
|
338 "all_descendant_sf_remain ss sf from to ss' \<equiv> |
|
339 (\<forall> sfs sf' tag'. sf \<preceq> sf' \<and> S_file sfs tag' \<in> ss \<and> sf' \<in> sfs \<longrightarrow> (\<exists> sfs'. |
|
340 S_file sfs' tag' \<in> ss \<and> file_after_rename from to sf' \<notin> sfs' \<and> sf' \<in> sfs')) \<and> |
|
341 (\<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> |
|
342 sproc_sfds_remain ss sf from to ss'" |
|
343 |
|
344 definition all_descendant_sf_choices |
|
345 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
346 where |
|
347 "all_descendant_sf_choices ss sf from to ss' \<equiv> |
|
348 all_descendant_sf_renamed ss sf from to ss' \<or> all_descendant_sf_remain ss sf from to ss'" |
|
349 |
|
350 definition all_descendant_sf_both |
|
351 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
352 where |
|
353 "all_descendant_sf_both ss sf from to ss' \<equiv> |
|
354 (\<forall> sfs sf' tag'. sf \<preceq> sf' \<and> S_file sfs tag' \<in> ss \<and> sf' \<in> sfs \<longrightarrow> (\<exists> sfs'. |
|
355 S_file sfs' tag' \<in> ss \<and> file_after_rename from to sf' \<in> sfs' \<or> sf' \<in> sfs')) \<and> |
|
356 (\<forall> sf' tag'. sf \<preceq> sf' \<and> S_dir sf' tag' \<in> ss \<longrightarrow> |
|
357 S_dir (file_after_rename from to sf') tag' \<in> ss' \<or> S_dir sf' tag' \<in> ss') \<and> |
|
358 sproc_sfds_both ss sf from to ss'" |
|
359 |
|
360 definition ss_renamed_file |
|
361 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
362 where |
|
363 "ss_renamed_file ss sf sf' ss' \<equiv> |
|
364 (if (is_many_sfile sf) |
|
365 then all_descendant_sf_choices ss sf sf sf' ss' |
|
366 else all_descendant_sf_renamed ss sf sf sf' ss')" |
|
367 |
|
368 (* added to the new sfs, are those only under the new sfile *) |
|
369 definition sfs_rename_added |
|
370 :: "t_sfile set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile set \<Rightarrow> bool" |
|
371 where |
|
372 "sfs_rename_added sfs from to sfs' \<equiv> |
|
373 (\<forall> sf'. sf' \<in> sfs' \<and> sf' \<notin> sfs \<longrightarrow> (\<exists> sf. sf \<in> sfs \<and> sf' = file_after_rename from to sf))" |
|
374 |
|
375 (* added to the new sfile, are those only under the new sfile *) |
|
376 definition ss_rename_added |
|
377 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
378 where |
|
379 "ss_rename_added ss from to ss' \<equiv> |
|
380 (\<forall> pi sec fds fds' shms tagp. S_proc (pi, sec, fds,shms) tagp \<in> ss \<and> |
|
381 S_proc (pi,sec,fds',shms) tagp \<in> ss' \<longrightarrow> sfds_rename_added fds from to fds') \<and> |
|
382 (\<forall> sq. S_msgq sq \<in> ss' \<longrightarrow> S_msgq sq \<in> ss) \<and> |
|
383 (\<forall> sfs sfs' tagf. S_file sfs' tagf \<in> ss' \<and> S_file sfs tagf \<in> ss \<longrightarrow> |
|
384 sfs_rename_added sfs from to sfs') \<and> |
|
385 (\<forall> sf' tagf. S_dir sf' tagf \<in> ss' \<and> S_dir sf' tagf \<notin> ss \<longrightarrow> |
|
386 (\<exists> sf. S_dir sf tagf \<in> ss \<and> sf' = file_after_rename from to sf))" |
|
387 |
|
388 definition sfile_alive :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> bool" |
|
389 where |
|
390 "sfile_alive ss sf \<equiv> (\<exists> sfs tagf. sf \<in> sfs \<and> S_file sfs tagf \<in> ss)" |
|
391 |
|
392 definition sf_alive :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> bool" |
|
393 where |
|
394 "sf_alive ss sf \<equiv> (\<exists> tagd. S_dir sf tagd \<in> ss) \<or> sfile_alive ss sf" |
|
395 |
|
396 (* constrains that the new static state should satisfy *) |
|
397 definition ss_rename:: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
398 where |
|
399 "ss_rename ss sf sf' ss' \<equiv> |
|
400 ss_rename_notrelated ss sf sf' ss' \<and> |
|
401 ss_renamed_file ss sf sf' ss' \<and> ss_rename_added ss sf sf' ss' \<and> |
|
402 (\<forall> sf''. sf_alive ss sf'' \<and> sf \<prec> sf'' \<longrightarrow> |
|
403 (if (is_many_sfile sf'') |
|
404 then all_descendant_sf_choices ss sf'' sf sf' ss' |
|
405 else all_descendant_sf_both ss sf'' sf sf' ss'))" |
|
406 |
|
407 (* two sfile, the last fname should not be equal *) |
|
408 fun sfile_same_fname:: "t_sfile \<Rightarrow> t_sfile \<Rightarrow> bool" |
|
409 where |
|
410 "sfile_same_fname ((Init n, sec)#spf) ((Init n', sec')#spf') = (n = n')" |
|
411 | "sfile_same_fname _ _ = False" |
|
412 |
|
413 (* no same init sfile/only sfile in the target-to spf, should be in static_state addmissble check *) |
|
414 definition ss_rename_no_same_fname:: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> bool" |
|
415 where |
|
416 "ss_rename_no_same_fname ss from spf \<equiv> |
|
417 \<not> (\<exists> to. sfile_same_fname from to \<and> parent to = Some spf \<and> sf_alive ss to)" |
|
418 |
|
419 (* is not a function, is a relation (one 2 many) |
|
420 definition update_ss_rename :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state" |
|
421 where |
|
422 "update_ss_rename ss sf sf' \<equiv> if (is_many_sfile sf) |
|
423 then (ss \<union> {S_file (file_after_rename sf sf' sf'') tag | sf'' tag. sf \<preceq> sf'' \<and> S_file sf'' tag \<in> ss} |
|
424 \<union> {S_dir (file_after_rename sf sf' sf'') tag | sf'' tag. sf \<preceq> sf'' \<and> S_dir sf'' tag \<in> ss}) |
|
425 else (ss - {S_file sf'' tag | sf'' tag. sf \<preceq> sf'' \<and> S_file sf'' tag \<in> ss} |
|
426 - {S_dir sf'' tag | sf'' tag. sf \<preceq> sf'' \<and> S_dir sf'' tag \<in> ss}) |
|
427 \<union> {S_file (file_after_rename sf sf' sf'') tag | sf'' tag. sf \<preceq> sf'' \<and> S_file sf'' tag \<in> ss} |
|
428 \<union> {S_dir (file_after_rename sf sf' sf'') tag | sf'' tag. sf \<preceq> sf'' \<and> S_dir sf'' tag \<in> ss}" |
|
429 *) |
|
430 *) |
|
431 |
|
432 fun sectxt_of_sproc :: "t_sproc \<Rightarrow> security_context_t" |
|
433 where |
|
434 "sectxt_of_sproc (pi,sec,fds,shms) = sec" |
|
435 |
|
436 fun sectxt_of_sfile :: "t_sfile \<Rightarrow> security_context_t" |
|
437 where |
|
438 "sectxt_of_sfile (fi,sec,psec,asecs) = sec" |
|
439 |
|
440 fun asecs_of_sfile :: "t_sfile \<Rightarrow> security_context_t set" |
|
441 where |
|
442 "asecs_of_sfile (fi,sec,psec,asecs) = asecs" |
|
443 |
|
444 definition search_check_s :: "security_context_t \<Rightarrow> t_sfile \<Rightarrow> bool \<Rightarrow> bool" |
|
445 where |
|
446 "search_check_s pctxt sf if_file = |
|
447 (if if_file |
|
448 then search_check_file pctxt (sectxt_of_sfile sf) \<and> search_check_allp pctxt (asecs_of_sfile sf) |
|
449 else search_check_dir pctxt (sectxt_of_sfile sf) \<and> search_check_allp pctxt (asecs_of_sfile sf))" |
|
450 |
|
451 definition sectxts_of_sfds :: "t_sfd set \<Rightarrow> security_context_t set" |
|
452 where |
|
453 "sectxts_of_sfds sfds \<equiv> {ctxt. \<exists> flag sf. (ctxt, flag, sf) \<in> sfds}" |
|
454 |
|
455 definition inherit_fds_check_s :: "security_context_t \<Rightarrow> t_sfd set \<Rightarrow> bool" |
|
456 where |
|
457 "inherit_fds_check_s pctxt sfds \<equiv> |
|
458 (\<forall> ctxt \<in> sectxts_of_sfds sfds. permission_check pctxt ctxt C_fd P_inherit)" |
|
459 |
|
460 definition sectxts_of_sproc_sshms :: "t_sproc_sshm set \<Rightarrow> security_context_t set" |
|
461 where |
|
462 "sectxts_of_sproc_sshms sshms \<equiv> {ctxt. \<exists> hi flag. ((hi, ctxt),flag) \<in> sshms}" |
|
463 |
|
464 definition inherit_shms_check_s :: "security_context_t \<Rightarrow> t_sproc_sshm set \<Rightarrow> bool" |
|
465 where |
|
466 "inherit_shms_check_s pctxt sshms \<equiv> |
|
467 (\<forall> ctxt \<in> sectxts_of_sproc_sshms sshms. permission_check pctxt ctxt C_shm P_inherit)" |
|
468 |
|
469 (* |
|
470 fun info_flow_sshm :: "t_sproc \<Rightarrow> t_sproc \<Rightarrow> bool" |
|
471 where |
|
472 "info_flow_sshm (pi,sec,fds,shms) (pi',sec',fds',shms') = |
|
473 (\<exists> sh flag'. (sh, SHM_RDWR) \<in> shms \<and> (sh, flag') \<in> shms')" |
|
474 *) |
|
475 definition info_flow_sproc_sshms :: "t_sproc_sshm set \<Rightarrow> t_sproc_sshm set \<Rightarrow> bool" |
|
476 where |
|
477 "info_flow_sproc_sshms shms shms' \<equiv> (\<exists> sh flag'. (sh, SHM_RDWR) \<in> shms \<and> (sh, flag') \<in> shms')" |
|
478 |
|
479 (* |
|
480 fun info_flow_sshm :: "t_sproc \<Rightarrow> t_sproc \<Rightarrow> bool" |
|
481 where |
|
482 "info_flow_sshm (pi,sec,fds,shms) (pi',sec',fds',shms') = info_flow_sproc_sshms shms shms'" |
|
483 *) |
|
484 inductive info_flow_sshm :: "t_sproc \<Rightarrow> t_sproc \<Rightarrow> bool" |
|
485 where |
|
486 "info_flow_sshm sp sp" |
|
487 | "\<lbrakk>info_flow_sshm sp (pi,sec,fds,shms); info_flow_sproc_sshms shms shms'\<rbrakk> |
|
488 \<Longrightarrow> info_flow_sshm sp (pi',sec',fds',shms')" |
|
489 |
|
490 definition update_ss_shms :: "t_static_state \<Rightarrow> t_sproc \<Rightarrow> bool \<Rightarrow> t_static_state" |
|
491 where |
|
492 "update_ss_shms ss spfrom tag \<equiv> {sobj. \<exists> sobj' \<in> ss. |
|
493 (case sobj' of |
|
494 S_proc sp tagp \<Rightarrow> if (info_flow_sshm spfrom sp) |
|
495 then if (is_many_sproc sp) |
|
496 then (sobj = S_proc sp tagp \<or> sobj = S_proc sp (tagp \<or> tag)) |
|
497 else (sobj = S_proc sp (tagp \<or> tag)) |
|
498 else (sobj = S_proc sp tag) |
|
499 | _ \<Rightarrow> sobj = sobj')}" |
|
500 |
|
501 |
|
502 |
|
503 (* all reachable static states(sobjects set) *) |
|
504 inductive_set static :: "t_static_state set" |
|
505 where |
|
506 s_init: "init_static_state \<in> static" |
|
507 | s_execve: "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; S_file sfs tagf \<in> ss; |
|
508 (fi,fsec,pfsec,asecs) \<in> sfs; npctxt_execve pctxt fsec = Some pctxt'; |
|
509 grant_execve pctxt fsec pctxt'; search_check_s pctxt (fi,fsec,pfsec,asecs) True; |
|
510 inherit_fds_check_s pctxt' fds'; fds' \<subseteq> fds\<rbrakk> |
|
511 \<Longrightarrow> (update_ss ss (S_proc (pi, pctxt, fds, shms) tagp) |
|
512 (S_proc (pi, pctxt', fds', {}) (tagp \<or> tagf))) \<in> static" |
|
513 | s_clone: "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; |
|
514 permission_check pctxt pctxt C_process P_fork; |
|
515 inherit_fds_check_s pctxt fds'; fds' \<subseteq> fds; |
|
516 inherit_shms_check_s pctxt shms'; shms' \<subseteq> shms\<rbrakk> |
|
517 \<Longrightarrow> (add_ss ss (S_proc (Created, pctxt, fds', shms') tagp)) \<in> static" |
|
518 | s_kill: "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; |
|
519 S_proc (pi', pctxt', fds', shms') tagp' \<in> ss; |
|
520 permission_check pctxt pctxt' C_process P_sigkill\<rbrakk> |
|
521 \<Longrightarrow> (del_ss ss (S_proc (pi', pctxt', fds', shms') tagp')) \<in> static" |
|
522 | s_ptrace: "\<lbrakk>ss \<in> static; S_proc sp tagp \<in> ss; S_proc sp' tagp' \<in> ss; |
|
523 permission_check (sextxt_of_sproc sp) (sectxt_of_sproc sp') C_process P_ptrace\<rbrakk> |
|
524 \<Longrightarrow> (update_ss_shms (update_ss_shms ss sp tagp) sp' tagp') \<in> static" |
|
525 | s_exit: "\<lbrakk>ss \<in> static; S_proc sp tagp \<in> ss\<rbrakk> \<Longrightarrow> (del_ss ss (S_proc sp tagp)) \<in> static" |
|
526 | s_open: "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; S_file sfs tagf \<in> ss; sf \<in> sfs; |
|
527 search_check_s pctxt sf True; \<not> is_creat_excl_flag flags; |
|
528 oflags_check flags pctxt (sectxt_of_sfile sf); permission_check pctxt pctxt C_fd P_setattr\<rbrakk> |
|
529 \<Longrightarrow> (update_ss ss (S_proc (pi, pctxt, fds, shms) tagp) |
|
530 (S_proc (pi, pctxt, fds \<union> {(pctxt,flags,sf)}, shms) tagp)) \<in> static" |
|
531 | s_open': "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; is_creat_excl_flag flags; |
|
532 S_dir (pfi,fsec,pfsec,asecs) \<in> ss; search_check_s pctxt (pfi,fsec,pfsec,asecs) False; |
|
533 nfsec = nfctxt_create pctxt fsec C_file; oflags_check flags pctxt nfsec; |
|
534 permission_check pctxt fsec C_dir P_add_rename; permission_check pctxt pctxt C_fd P_setattr\<rbrakk> |
|
535 \<Longrightarrow> (update_ss (add_ss ss (S_file {(Created, nfsec, Some fsec, asecs \<union> {fsec})} tagp)) |
|
536 (S_proc (pi, pctxt, fds, shms) tagp) |
|
537 (S_proc (pi, pctxt, fds \<union> {(pctxt, flags, (Created, nfsec, Some fsec, asecs \<union> {fsec}))}, shms) tagp) |
|
538 ) \<in> static" |
|
539 | S_readf: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; (fdctxt,flags,sf) \<in> fds; |
|
540 permission_check pctxt fdctxt C_fd P_setattr; S_file sfs tagf \<in> ss; sf \<in> sfs; |
|
541 permission_check pctxt (sectxt_of_sfile sf) C_file P_read; is_read_flag flags\<rbrakk> |
|
542 \<Longrightarrow> (update_ss_shms ss (pi, pctxt,fds,shms) (tagp \<or> tagf)) \<in> static" |
|
543 | S_writef: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; (fdctxt,flags,sf) \<in> fds; |
|
544 permission_check pctxt fdctxt C_fd P_setattr; sf \<in> sfs; S_file sfs tagf \<in> ss; |
|
545 permission_check pctxt (sectxt_of_sfile sf) C_file P_write; is_write_flag flags\<rbrakk> |
|
546 \<Longrightarrow> (update_ss ss (S_file sfs tagf) (S_file sfs (tagp \<or> tagf))) \<in> static" |
|
547 | S_unlink: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_file sfs tagf \<in> ss; |
|
548 (Init f,fsec,Some pfsec,asecs) \<in> sfs; |
|
549 search_check_s pctxt (Init f,fsec,Some pfsec,asecs) True; |
|
550 permission_check pctxt fsec C_file P_unlink; |
|
551 permission_check pctxt pfsec C_dir P_remove_name\<rbrakk> |
|
552 \<Longrightarrow> ((ss - {S_file sfs tagf}) \<union> {S_file (sfs - {(Init f,fsec,Some pfsec,asecs)}) tagf}) \<in> static" |
|
553 | S_rmdir: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; |
|
554 S_dir (fi,fsec,Some pfsec,asecs) \<in> ss; |
|
555 search_check_s pctxt (fi,fsec,Some pfsec,asecs) False; |
|
556 permission_check pctxt fsec C_dir P_rmdir; |
|
557 permission_check pctxt pfsec C_dir P_remove_name\<rbrakk> |
|
558 \<Longrightarrow> (del_ss ss (S_dir (fi,fsec,Some pfsec,asecs))) \<in> static" |
|
559 | S_mkdir: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_dir (fi,fsec,pfsec,asecs) \<in> ss; |
|
560 search_check_s pctxt (fi,fsec,pfsec,asecs) False; |
|
561 permission_check pctxt (nfctxt_create pctxt fsec C_dir) C_dir P_create; |
|
562 permission_check pctxt fsec C_dir P_add_name\<rbrakk> |
|
563 \<Longrightarrow> (add_ss ss (S_dir (Created,nfctxt_create pctxt fsec C_dir,Some fsec,asecs \<union> {fsec}))) \<in> static" |
|
564 | s_link: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_dir (pfi,pfsec,ppfsec,asecs) \<in> ss; |
|
565 S_file sfs tagf \<in> ss; sf \<in> sfs; nfsec = nfctxt_create pctxt pfsec C_file; |
|
566 search_check_s pctxt (pfi,pfsec,ppfsec,asecs) False; search_check_s pctxt sf True; |
|
567 permission_check pctxt (sectxt_of_sfile sf) C_file P_link; |
|
568 permission_check pctxt pfsec C_dir P_add_name\<rbrakk> |
|
569 \<Longrightarrow> (update_ss ss (S_file sfs tagf) |
|
570 (S_file (sfs \<union> {(Created,nfsec,Some pfsec, asecs \<union> {pfsec})}) tagf)) \<in> static" |
|
571 | s_trunc: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_file sfs tagf \<in> ss; sf \<in> sfs; |
|
572 search_check_s pctxt sf True; permission_check pctxt (sectxt_of_sfile sf) C_file P_setattr\<rbrakk> |
|
573 \<Longrightarrow> (update_ss ss (S_file sfs tagf) (S_file sfs (tagf \<or> tagp))) \<in> static" |
|
574 (* |
|
575 | s_rename: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_file sfs tagf \<in> ss; |
|
576 (sf#spf') \<in> sfs; S_dir spf tagpf \<in> ss; \<not>((sf#spf') \<preceq> (sf#spf)); |
|
577 search_check_s pctxt spf False; search_check_s pctxt (sf#spf') True; |
|
578 sectxt_of_sfile (sf#spf') = Some fctxt; sectxt_of_sfile spf = Some pfctxt; |
|
579 permission_check pctxt fctxt C_file P_rename; |
|
580 permission_check pctxt pfctxt C_dir P_add_name; |
|
581 ss_rename ss (sf#spf') (sf#spf) ss'; |
|
582 ss_rename_no_same_fname ss (sf#spf') (sf#spf)\<rbrakk> |
|
583 \<Longrightarrow> ss' \<in> static" |
|
584 | s_rename': "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_dir (sf#spf') tagf \<in> ss; |
|
585 S_dir spf tagpf \<in> ss; \<not>((sf#spf') \<preceq> (sf#spf)); |
|
586 search_check_s pctxt spf False; search_check_s pctxt (sf#spf') True; |
|
587 sectxt_of_sfile (sf#spf') = Some fctxt; sectxt_of_sfile spf = Some pfctxt; |
|
588 permission_check pctxt fctxt C_dir P_reparent; |
|
589 permission_check pctxt pfctxt C_dir P_add_name; |
|
590 ss_rename ss (sf#spf') (sf#spf) ss'; |
|
591 ss_rename_no_same_fname ss (sf#spf') (sf#spf)\<rbrakk> |
|
592 \<Longrightarrow> ss' \<in> static" |
|
593 *) |
|
594 | s_createq: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; |
|
595 permission_check pctxt pctxt C_msgq P_associate; |
|
596 permission_check pctxt pctxt C_msgq P_create\<rbrakk> |
|
597 \<Longrightarrow> (add_ss ss (S_msgq (Created,pctxt,[]))) \<in> static" |
|
598 | s_sendmsg: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_msgq (qi,qctxt,sms) \<in> ss; |
|
599 permission_check pctxt qctxt C_msgq P_enqueue; |
|
600 permission_check pctxt qctxt C_msgq P_write; |
|
601 permission_check pctxt pctxt C_msg P_create\<rbrakk> |
|
602 \<Longrightarrow> (update_ss ss (S_msgq (qi,qctxt,sms)) |
|
603 (S_msgq (qi,qctxt,sms @ [(Created, pctxt, tagp)]))) \<in> static" |
|
604 | s_recvmsg: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; |
|
605 S_msgq (qi,qctxt,(mi,mctxt,tagm)#sms) \<in> ss; |
|
606 permission_check pctxt qctxt C_msgq P_read; |
|
607 permission_check pctxt mctxt C_msg P_receive\<rbrakk> |
|
608 \<Longrightarrow> (update_ss (update_ss_shms ss (pi,pctxt,fds,shms) (tagp \<or> tagm)) |
|
609 (S_msgq (qi, qctxt, (mi, mctxt, tagm)#sms)) |
|
610 (S_msgq (qi, qctxt, sms))) \<in> static" |
|
611 | s_removeq: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_msgq (qi,qctxt,sms) \<in> ss; |
|
612 permission_check pctxt qctxt C_msgq P_destroy\<rbrakk> |
|
613 \<Longrightarrow> (del_ss ss (S_msgq (qi,qctxt,sms))) \<in> static" |
|
614 | s_createh: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; |
|
615 permission_check pctxt pctxt C_shm P_associate; |
|
616 permission_check pctxt pctxt C_shm P_create\<rbrakk> |
|
617 \<Longrightarrow> (add_ss ss (S_shm (Created, pctxt))) \<in> static" |
|
618 | s_attach: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_shm (hi,hctxt) \<in> ss; |
|
619 if flag = SHM_RDONLY then permission_check pctxt hctxt C_shm P_read |
|
620 else (permission_check pctxt hctxt C_shm P_read \<and> |
|
621 permission_check pctxt hctxt C_shm P_write)\<rbrakk> |
|
622 \<Longrightarrow> (update_ss ss (S_proc (pi,pctxt,fds,shms) tagp) |
|
623 (S_proc (pi,pctxt,fds,shms \<union> {((hi,hctxt),flag)}) tagp)) \<in> static" |
|
624 | s_detach: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_shm sh \<in> ss; |
|
625 (sh,flag) \<in> shms; \<not> is_many_sshm sh\<rbrakk> |
|
626 \<Longrightarrow> (update_ss ss (S_proc (pi,pctxt,fds,shms) tagp) |
|
627 (S_proc (pi,pctxt,fds,shms - {(sh,flag)}) tagp)) \<in> static" |
|
628 | s_deleteh: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_shm (hi,hctxt) \<in> ss; |
|
629 permission_check pctxt hctxt C_shm P_destroy; \<not> is_many_sshm sh\<rbrakk> |
|
630 \<Longrightarrow> (remove_sproc_sshm (del_ss ss (S_shm (hi,hctxt))) (hi,hctxt)) \<in> static" |
|
631 |
|
632 (* |
|
633 fun smsg_related :: "t_msg \<Rightarrow> t_smsg list \<Rightarrow> bool" |
|
634 where |
|
635 "smsg_related m [] = False" |
|
636 | "smsg_related m ((mi, sec, tag)#sms) = |
|
637 (if (mi = Init m) then True else smsg_related m sms)" |
|
638 |
|
639 fun smsgq_smsg_related :: "t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsgq \<Rightarrow> bool" |
|
640 where |
|
641 "smsgq_smsg_related q m (qi, sec, smsgslist) = ((qi = Init q) \<and> (smsg_related m smsgslist))" |
|
642 |
|
643 fun smsg_relatainted :: "t_msg \<Rightarrow> t_smsg list \<Rightarrow> bool" |
|
644 where |
|
645 "smsg_relatainted m [] = False" |
|
646 | "smsg_relatainted m ((mi, sec, tag)#sms) = |
|
647 (if (mi = Init m \<and> tag = True) then True else smsg_relatainted m sms)" |
|
648 |
|
649 fun smsgq_smsg_relatainted :: "t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsgq \<Rightarrow> bool" |
|
650 where |
|
651 "smsgq_smsg_relatainted q m (qi, sec, smsgslist) = |
|
652 ((qi = Init q) \<and> (smsg_relatainted m smsgslist))" |
|
653 *) |
|
654 |
|
655 fun sfile_related :: "t_sfile \<Rightarrow> t_file \<Rightarrow> bool" |
|
656 where |
|
657 "sfile_related (fi,sec,psec,asecs) f = (fi = Init f)" |
|
658 (* |
|
659 fun sproc_related :: "t_process \<Rightarrow> t_sproc \<Rightarrow> bool" |
|
660 where |
|
661 "sproc_related p (pi, sec, fds, shms) = (pi = Init p)" |
|
662 *) |
|
663 fun init_obj_related :: "t_sobject \<Rightarrow> t_object \<Rightarrow> bool" |
|
664 where |
|
665 "init_obj_related (S_proc (pi, sec, fds, shms) tag) (O_proc p') = (pi = Init p')" |
|
666 | "init_obj_related (S_file sfs tag) (O_file f) = (\<exists> sf \<in> sfs. sfile_related sf f)" |
|
667 | "init_obj_related (S_dir sf) (O_dir f) = (sfile_related sf f)" |
|
668 | "init_obj_related (S_msgq (qi, sec, sms)) (O_msgq q') = (qi = Init q')" |
|
669 | "init_obj_related (S_shm (hi, sec)) (O_shm h') = (hi = Init h')" |
|
670 (* |
|
671 | "init_obj_related (S_msg (qi, sec, sms) (mi, secm, tagm)) (O_msg q' m') = (qi = Init q' \<and> mi = Init m')" |
|
672 *) |
|
673 | "init_obj_related _ _ = False" |
|
674 |
|
675 fun tainted_s :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> bool" |
|
676 where |
|
677 "tainted_s ss (S_proc sp tag) = (S_proc sp tag \<in> ss \<and> tag = True)" |
|
678 | "tainted_s ss (S_file sfs tag) = (S_file sfs tag \<in> ss \<and> tag = True)" |
|
679 (* |
|
680 | "tainted_s ss (S_msg (qi, sec, sms) (mi, secm, tag)) = |
|
681 (S_msgq (qi, sec, sms) \<in> ss \<and> (mi,secm,tag) \<in> set sms \<and> tag = True)" |
|
682 *) |
|
683 | "tainted_s ss _ = False" |
|
684 |
|
685 (* |
|
686 fun tainted_s :: "t_object \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
687 where |
|
688 "tainted_s (O_proc p) ss = (\<exists> sp. S_proc sp True \<in> ss \<and> sproc_related p sp)" |
|
689 | "tainted_s (O_file f) ss = (\<exists> sfs sf. S_file sfs True \<in> ss \<and> sf \<in> sfs \<and> sfile_related f sf)" |
|
690 | "tainted_s (O_msg q m) ss = (\<exists> sq. S_msgq sq \<in> ss \<and> smsgq_smsg_relatainted q m sq)" |
|
691 | "tainted_s _ ss = False" |
|
692 *) |
|
693 |
|
694 definition taintable_s :: "t_object \<Rightarrow> bool" |
|
695 where |
|
696 "taintable_s obj \<equiv> \<exists> ss \<in> static. \<exists> sobj. tainted_s ss sobj \<and> init_obj_related sobj obj \<and> init_alive obj" |
|
697 |
|
698 definition deletable_s :: "t_object \<Rightarrow> bool" |
|
699 where |
|
700 "deletable_s obj \<equiv> init_alive obj \<and> (\<exists> ss \<in> static. \<forall> sobj \<in> ss. \<not> init_obj_related sobj obj)" |
|
701 |
|
702 definition undeletable_s :: "t_object \<Rightarrow> bool" |
|
703 where |
|
704 "undeletable_s obj \<equiv> init_alive obj \<and> (\<forall> ss \<in> static. \<exists> sobj \<in> ss. init_obj_related sobj obj)" |
|
705 |
|
706 |
|
707 (**************** translation from dynamic to static *******************) |
125 (**************** translation from dynamic to static *******************) |
708 |
126 |
709 definition cf2sfile :: "t_state \<Rightarrow> t_file \<Rightarrow> t_sfile option" |
127 definition cf2sfile :: "t_state \<Rightarrow> t_file \<Rightarrow> t_sfile option" |
710 where |
128 where |
711 "cf2sfile s f \<equiv> |
129 "cf2sfile s f \<equiv> |
810 | _ \<Rightarrow> None)" |
228 | _ \<Rightarrow> None)" |
811 *) |
229 *) |
812 | "co2sobj s _ = None" |
230 | "co2sobj s _ = None" |
813 |
231 |
814 |
232 |
|
233 definition s2ss :: "t_state \<Rightarrow> t_static_state" |
|
234 where |
|
235 "s2ss s \<equiv> {sobj. \<exists> obj. alive s obj \<and> co2sobj s obj = Some sobj}" |
|
236 |
|
237 |
|
238 (* ******************************************************** *) |
|
239 |
|
240 |
|
241 fun is_init_sfile :: "t_sfile \<Rightarrow> bool" |
|
242 where |
|
243 "is_init_sfile (Init _, sec, psec,asec) = True" |
|
244 | "is_init_sfile _ = False" |
|
245 |
|
246 fun is_many_sfile :: "t_sfile \<Rightarrow> bool" |
|
247 where |
|
248 "is_many_sfile (Created, sec, psec, asec) = True" |
|
249 | "is_many_sfile _ = False" |
|
250 |
|
251 fun is_init_sproc :: "t_sproc \<Rightarrow> bool" |
|
252 where |
|
253 "is_init_sproc (Init p, sec, fds, shms) = True" |
|
254 | "is_init_sproc _ = False" |
|
255 |
|
256 fun is_many_sproc :: "t_sproc \<Rightarrow> bool" |
|
257 where |
|
258 "is_many_sproc (Created, sec,fds,shms) = True" |
|
259 | "is_many_sproc _ = False" |
|
260 |
|
261 fun is_many_smsg :: "t_smsg \<Rightarrow> bool" |
|
262 where |
|
263 "is_many_smsg (Created,sec,tag) = True" |
|
264 | "is_many_smsg _ = False" |
|
265 |
|
266 (* wrong def |
|
267 fun is_many_smsgq :: "t_smsgq \<Rightarrow> bool" |
|
268 where |
|
269 "is_many_smsgq (Created,sec,sms) = (True \<and> (\<forall> sm \<in> (set sms). is_many_smsg sm))" |
|
270 | "is_many_smsgq _ = False" |
|
271 *) |
|
272 |
|
273 fun is_many_smsgq :: "t_smsgq \<Rightarrow> bool" |
|
274 where |
|
275 "is_many_smsgq (Created,sec,sms) = True" |
|
276 | "is_many_smsgq _ = False" |
|
277 |
|
278 fun is_many_sshm :: "t_sshm \<Rightarrow> bool" |
|
279 where |
|
280 "is_many_sshm (Created, sec) = True" |
|
281 | "is_many_sshm _ = False" |
|
282 |
|
283 fun is_many :: "t_sobject \<Rightarrow> bool" |
|
284 where |
|
285 "is_many (S_proc sp tag) = is_many_sproc sp" |
|
286 | "is_many (S_file sfs tag) = (\<forall> sf \<in> sfs. is_many_sfile sf)" |
|
287 | "is_many (S_dir sf ) = is_many_sfile sf" |
|
288 | "is_many (S_msgq sq ) = is_many_smsgq sq" |
|
289 | "is_many (S_shm sh ) = is_many_sshm sh" |
|
290 |
|
291 fun is_init_smsgq :: "t_smsgq \<Rightarrow> bool" |
|
292 where |
|
293 "is_init_smsgq (Init q,sec,sms) = True" |
|
294 | "is_init_smsgq _ = False" |
|
295 |
|
296 fun is_init_sshm :: "t_sshm \<Rightarrow> bool" |
|
297 where |
|
298 "is_init_sshm (Init h,sec) = True" |
|
299 | "is_init_sshm _ = False" |
|
300 |
|
301 fun is_init_sobj :: "t_sobject \<Rightarrow> bool" |
|
302 where |
|
303 "is_init_sobj (S_proc sp tag ) = is_init_sproc sp" |
|
304 | "is_init_sobj (S_file sfs tag) = (\<exists> sf \<in> sfs. is_init_sfile sf)" |
|
305 | "is_init_sobj (S_dir sf ) = is_init_sfile sf" |
|
306 | "is_init_sobj (S_msgq sq ) = is_init_smsgq sq" |
|
307 | "is_init_sobj (S_shm sh ) = is_init_sshm sh" |
|
308 |
|
309 (* |
|
310 fun update_ss_sp:: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state" |
|
311 where |
|
312 "update_ss_sp ss (S_proc sp tag) (S_proc sp' tag') = |
|
313 (if (is_many_sproc sp) then ss \<union> {S_proc sp' tag'} |
|
314 else (ss - {S_proc sp tag}) \<union> {S_proc sp' tag'})" |
|
315 |
|
316 fun update_ss_sd:: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state" |
|
317 where |
|
318 "update_ss_sd ss (S_dir sf tag) (S_dir sf' tag') = |
|
319 (if (is_many_sfile sf) then ss \<union> {S_dir sf' tag'} |
|
320 else (ss - {S_dir sf tag}) \<union> {S_dir sf' tag'})" |
|
321 *) |
|
322 |
|
323 (* |
|
324 fun sparent :: "t_sfile \<Rightarrow> t_sfile option" |
|
325 where |
|
326 "sparent (Sroot si sec) = None" |
|
327 | "sparent (Sfile si sec spf) = Some spf" |
|
328 |
|
329 inductive is_ancesf :: "t_sfile \<Rightarrow> t_sfile \<Rightarrow> bool" |
|
330 where |
|
331 "is_ancesf sf sf" |
|
332 | "sparent sf = Some spf \<Longrightarrow> is_ancesf spf sf" |
|
333 | "\<lbrakk>sparent sf = Some spf; is_ancesf saf spf\<rbrakk> \<Longrightarrow> is_ancesf saf sf" |
|
334 |
|
335 definition sfile_reparent :: "t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile" |
|
336 where |
|
337 "sfile_reparent (Sroot)" |
|
338 *) |
|
339 |
|
340 (* |
|
341 (* sfds rename aux definitions *) |
|
342 definition sfds_rename_notrelated |
|
343 :: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool" |
|
344 where |
|
345 "sfds_rename_notrelated sfds from to sfds' \<equiv> |
|
346 (\<forall> sec flag sf. (sec,flag,sf) \<in> sfds \<and> (\<not> from \<preceq> sf) \<longrightarrow> (sec,flag,sf) \<in> sfds')" |
|
347 |
|
348 definition sfds_rename_renamed |
|
349 :: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool" |
|
350 where |
|
351 "sfds_rename_renamed sfds sf from to sfds' \<equiv> |
|
352 (\<forall> sec flag sf'. (sec,flag,sf) \<in> sfds \<and> (sf \<preceq> sf') \<longrightarrow> |
|
353 (sec, flag, file_after_rename sf' from to) \<in> sfds' \<and> (sec,flag,sf) \<notin> sfds')" |
|
354 |
|
355 definition sfds_rename_remain |
|
356 :: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool" |
|
357 where |
|
358 "sfds_rename_remain sfds sf from to sfds' \<equiv> |
|
359 (\<forall> sec flag sf'. (sec,flag,sf') \<in> sfds \<and> (sf \<preceq> sf') \<longrightarrow> |
|
360 (sec, flag, sf') \<in> sfds' \<and> (sec,flag, file_after_rename sf' from to) \<notin> sfds')" |
|
361 |
|
362 (* for not many, choose on renamed or not *) |
|
363 definition sfds_rename_choices |
|
364 :: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool" |
|
365 where |
|
366 "sfds_rename_choices sfds sf from to sfds' \<equiv> |
|
367 sfds_rename_remain sfds sf from to sfds' \<or> sfds_rename_renamed sfds sf from to sfds'" |
|
368 |
|
369 (* for many, merge renamed with not renamed *) |
|
370 definition sfds_rename_both |
|
371 :: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool" |
|
372 where |
|
373 "sfds_rename_both sfds sf from to sfds' \<equiv> |
|
374 (\<forall> sec flag sf'. (sec,flag,sf') \<in> sfds \<and> (sf \<preceq> sf') \<longrightarrow> |
|
375 (sec, flag, sf') \<in> sfds' \<or> (sec,flag, file_after_rename sf' from to) \<in> sfds')" |
|
376 |
|
377 (* added to the new sfds, are those only under the new sfile *) |
|
378 definition sfds_rename_added |
|
379 :: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool" |
|
380 where |
|
381 "sfds_rename_added sfds from to sfds' \<equiv> |
|
382 (\<forall> sec' flag' sf' sec flag. (sec',flag',sf') \<in> sfds' \<and> (sec,flag,sf') \<notin> sfds \<longrightarrow> |
|
383 (\<exists> sf. (sec,flag,sf) \<in> sfds \<and> sf' = file_after_rename from to sf))" |
|
384 |
|
385 definition sproc_sfds_renamed |
|
386 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
387 where |
|
388 "sproc_sfds_renamed ss sf from to ss' \<equiv> |
|
389 (\<forall> pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \<in> ss \<longrightarrow> |
|
390 (\<exists> sfds'. S_proc (pi,sec,sfds',sshms) tagp \<in> ss \<and> sfds_rename_renamed sfds sf from to sfds'))" |
|
391 |
|
392 definition sproc_sfds_remain |
|
393 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
394 where |
|
395 "sproc_sfds_remain ss sf from to ss' \<equiv> |
|
396 (\<forall> pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \<in> ss \<longrightarrow> |
|
397 (\<exists> sfds'. S_proc (pi,sec,sfds',sshms) tagp \<in> ss \<and> sfds_rename_remain sfds sf from to sfds'))" |
|
398 |
|
399 (* for not many, choose on renamed or not *) |
|
400 definition sproc_sfds_choices |
|
401 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
402 where |
|
403 "sproc_sfds_choices 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_choices sfds sf from to sfds'))" |
|
406 |
|
407 (* for many, merge renamed with not renamed *) |
|
408 definition sproc_sfds_both |
|
409 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
410 where |
|
411 "sproc_sfds_both 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_both sfds sf from to sfds'))" |
|
414 |
|
415 (* remove (\<forall> sp tag. S_proc sp tag \<in> ss \<longrightarrow> S_proc sp tag \<in> ss'), |
|
416 * cause sfds contains sfs informations *) |
|
417 definition ss_rename_notrelated |
|
418 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
419 where |
|
420 "ss_rename_notrelated ss sf sf' ss' \<equiv> |
|
421 (\<forall> sq. S_msgq sq \<in> ss \<longrightarrow> S_msgq sq \<in> ss') \<and> |
|
422 (\<forall> pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \<in> ss \<longrightarrow> (\<exists> sfds'. |
|
423 S_proc (pi,sec,sfds',sshms) tagp \<in> ss'\<and> sfds_rename_notrelated sfds sf sf' sfds')) \<and> |
|
424 (\<forall> sfs sf'' tag. S_file sfs tag \<in> ss \<and> sf'' \<in> sfs \<and> (\<not> sf \<preceq> sf'') \<longrightarrow> (\<exists> sfs'. |
|
425 S_file sfs tag \<in> ss' \<and> sf'' \<in> sfs')) \<and> |
|
426 (\<forall> sf'' tag. S_dir sf'' tag \<in> ss \<and> (\<not> sf \<preceq> sf'') \<longrightarrow> S_dir sf'' tag \<in> ss')" |
|
427 |
|
428 (* rename from to, from should definited renamed if not many *) |
|
429 definition all_descendant_sf_renamed |
|
430 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
431 where |
|
432 "all_descendant_sf_renamed ss sf from to ss' \<equiv> |
|
433 (\<forall> sfs sf' tagf. sf \<preceq> sf' \<and> S_file sfs tagf \<in> ss \<and> sf' \<in> sfs \<longrightarrow> (\<exists> sfs'. |
|
434 S_file sfs' tagf \<in> ss' \<and> file_after_rename from to sf' \<in> sfs' \<and> sf' \<notin> sfs')) \<and> |
|
435 (\<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> |
|
436 sproc_sfds_renamed ss sf from to ss'" |
|
437 |
|
438 (* not renamed *) |
|
439 definition all_descendant_sf_remain |
|
440 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
441 where |
|
442 "all_descendant_sf_remain ss sf from to ss' \<equiv> |
|
443 (\<forall> sfs sf' tag'. sf \<preceq> sf' \<and> S_file sfs tag' \<in> ss \<and> sf' \<in> sfs \<longrightarrow> (\<exists> sfs'. |
|
444 S_file sfs' tag' \<in> ss \<and> file_after_rename from to sf' \<notin> sfs' \<and> sf' \<in> sfs')) \<and> |
|
445 (\<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> |
|
446 sproc_sfds_remain ss sf from to ss'" |
|
447 |
|
448 definition all_descendant_sf_choices |
|
449 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
450 where |
|
451 "all_descendant_sf_choices ss sf from to ss' \<equiv> |
|
452 all_descendant_sf_renamed ss sf from to ss' \<or> all_descendant_sf_remain ss sf from to ss'" |
|
453 |
|
454 definition all_descendant_sf_both |
|
455 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
456 where |
|
457 "all_descendant_sf_both ss sf from to ss' \<equiv> |
|
458 (\<forall> sfs sf' tag'. sf \<preceq> sf' \<and> S_file sfs tag' \<in> ss \<and> sf' \<in> sfs \<longrightarrow> (\<exists> sfs'. |
|
459 S_file sfs' tag' \<in> ss \<and> file_after_rename from to sf' \<in> sfs' \<or> sf' \<in> sfs')) \<and> |
|
460 (\<forall> sf' tag'. sf \<preceq> sf' \<and> S_dir sf' tag' \<in> ss \<longrightarrow> |
|
461 S_dir (file_after_rename from to sf') tag' \<in> ss' \<or> S_dir sf' tag' \<in> ss') \<and> |
|
462 sproc_sfds_both ss sf from to ss'" |
|
463 |
|
464 definition ss_renamed_file |
|
465 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
466 where |
|
467 "ss_renamed_file ss sf sf' ss' \<equiv> |
|
468 (if (is_many_sfile sf) |
|
469 then all_descendant_sf_choices ss sf sf sf' ss' |
|
470 else all_descendant_sf_renamed ss sf sf sf' ss')" |
|
471 |
|
472 (* added to the new sfs, are those only under the new sfile *) |
|
473 definition sfs_rename_added |
|
474 :: "t_sfile set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile set \<Rightarrow> bool" |
|
475 where |
|
476 "sfs_rename_added sfs from to sfs' \<equiv> |
|
477 (\<forall> sf'. sf' \<in> sfs' \<and> sf' \<notin> sfs \<longrightarrow> (\<exists> sf. sf \<in> sfs \<and> sf' = file_after_rename from to sf))" |
|
478 |
|
479 (* added to the new sfile, are those only under the new sfile *) |
|
480 definition ss_rename_added |
|
481 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
482 where |
|
483 "ss_rename_added ss from to ss' \<equiv> |
|
484 (\<forall> pi sec fds fds' shms tagp. S_proc (pi, sec, fds,shms) tagp \<in> ss \<and> |
|
485 S_proc (pi,sec,fds',shms) tagp \<in> ss' \<longrightarrow> sfds_rename_added fds from to fds') \<and> |
|
486 (\<forall> sq. S_msgq sq \<in> ss' \<longrightarrow> S_msgq sq \<in> ss) \<and> |
|
487 (\<forall> sfs sfs' tagf. S_file sfs' tagf \<in> ss' \<and> S_file sfs tagf \<in> ss \<longrightarrow> |
|
488 sfs_rename_added sfs from to sfs') \<and> |
|
489 (\<forall> sf' tagf. S_dir sf' tagf \<in> ss' \<and> S_dir sf' tagf \<notin> ss \<longrightarrow> |
|
490 (\<exists> sf. S_dir sf tagf \<in> ss \<and> sf' = file_after_rename from to sf))" |
|
491 |
|
492 definition sfile_alive :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> bool" |
|
493 where |
|
494 "sfile_alive ss sf \<equiv> (\<exists> sfs tagf. sf \<in> sfs \<and> S_file sfs tagf \<in> ss)" |
|
495 |
|
496 definition sf_alive :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> bool" |
|
497 where |
|
498 "sf_alive ss sf \<equiv> (\<exists> tagd. S_dir sf tagd \<in> ss) \<or> sfile_alive ss sf" |
|
499 |
|
500 (* constrains that the new static state should satisfy *) |
|
501 definition ss_rename:: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
502 where |
|
503 "ss_rename ss sf sf' ss' \<equiv> |
|
504 ss_rename_notrelated ss sf sf' ss' \<and> |
|
505 ss_renamed_file ss sf sf' ss' \<and> ss_rename_added ss sf sf' ss' \<and> |
|
506 (\<forall> sf''. sf_alive ss sf'' \<and> sf \<prec> sf'' \<longrightarrow> |
|
507 (if (is_many_sfile sf'') |
|
508 then all_descendant_sf_choices ss sf'' sf sf' ss' |
|
509 else all_descendant_sf_both ss sf'' sf sf' ss'))" |
|
510 |
|
511 (* two sfile, the last fname should not be equal *) |
|
512 fun sfile_same_fname:: "t_sfile \<Rightarrow> t_sfile \<Rightarrow> bool" |
|
513 where |
|
514 "sfile_same_fname ((Init n, sec)#spf) ((Init n', sec')#spf') = (n = n')" |
|
515 | "sfile_same_fname _ _ = False" |
|
516 |
|
517 (* no same init sfile/only sfile in the target-to spf, should be in static_state addmissble check *) |
|
518 definition ss_rename_no_same_fname:: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> bool" |
|
519 where |
|
520 "ss_rename_no_same_fname ss from spf \<equiv> |
|
521 \<not> (\<exists> to. sfile_same_fname from to \<and> parent to = Some spf \<and> sf_alive ss to)" |
|
522 |
|
523 (* is not a function, is a relation (one 2 many) |
|
524 definition update_ss_rename :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state" |
|
525 where |
|
526 "update_ss_rename ss sf sf' \<equiv> if (is_many_sfile sf) |
|
527 then (ss \<union> {S_file (file_after_rename sf sf' sf'') tag | sf'' tag. sf \<preceq> sf'' \<and> S_file sf'' tag \<in> ss} |
|
528 \<union> {S_dir (file_after_rename sf sf' sf'') tag | sf'' tag. sf \<preceq> sf'' \<and> S_dir sf'' tag \<in> ss}) |
|
529 else (ss - {S_file sf'' tag | sf'' tag. sf \<preceq> sf'' \<and> S_file sf'' tag \<in> ss} |
|
530 - {S_dir sf'' tag | sf'' tag. sf \<preceq> sf'' \<and> S_dir sf'' tag \<in> ss}) |
|
531 \<union> {S_file (file_after_rename sf sf' sf'') tag | sf'' tag. sf \<preceq> sf'' \<and> S_file sf'' tag \<in> ss} |
|
532 \<union> {S_dir (file_after_rename sf sf' sf'') tag | sf'' tag. sf \<preceq> sf'' \<and> S_dir sf'' tag \<in> ss}" |
|
533 *) |
|
534 *) |
|
535 |
|
536 fun sectxt_of_sproc :: "t_sproc \<Rightarrow> security_context_t" |
|
537 where |
|
538 "sectxt_of_sproc (pi,sec,fds,shms) = sec" |
|
539 |
|
540 fun sectxt_of_sfile :: "t_sfile \<Rightarrow> security_context_t" |
|
541 where |
|
542 "sectxt_of_sfile (fi,sec,psec,asecs) = sec" |
|
543 |
|
544 fun asecs_of_sfile :: "t_sfile \<Rightarrow> security_context_t set" |
|
545 where |
|
546 "asecs_of_sfile (fi,sec,psec,asecs) = asecs" |
|
547 |
|
548 definition search_check_s :: "security_context_t \<Rightarrow> t_sfile \<Rightarrow> bool \<Rightarrow> bool" |
|
549 where |
|
550 "search_check_s pctxt sf if_file = |
|
551 (if if_file |
|
552 then search_check_file pctxt (sectxt_of_sfile sf) \<and> search_check_allp pctxt (asecs_of_sfile sf) |
|
553 else search_check_dir pctxt (sectxt_of_sfile sf) \<and> search_check_allp pctxt (asecs_of_sfile sf))" |
|
554 |
|
555 definition sectxts_of_sfds :: "t_sfd set \<Rightarrow> security_context_t set" |
|
556 where |
|
557 "sectxts_of_sfds sfds \<equiv> {ctxt. \<exists> flag sf. (ctxt, flag, sf) \<in> sfds}" |
|
558 |
|
559 definition inherit_fds_check_s :: "security_context_t \<Rightarrow> t_sfd set \<Rightarrow> bool" |
|
560 where |
|
561 "inherit_fds_check_s pctxt sfds \<equiv> |
|
562 (\<forall> ctxt \<in> sectxts_of_sfds sfds. permission_check pctxt ctxt C_fd P_inherit)" |
|
563 |
|
564 definition sectxts_of_sproc_sshms :: "t_sproc_sshm set \<Rightarrow> security_context_t set" |
|
565 where |
|
566 "sectxts_of_sproc_sshms sshms \<equiv> {ctxt. \<exists> hi flag. ((hi, ctxt),flag) \<in> sshms}" |
|
567 |
|
568 definition inherit_shms_check_s :: "security_context_t \<Rightarrow> t_sproc_sshm set \<Rightarrow> bool" |
|
569 where |
|
570 "inherit_shms_check_s pctxt sshms \<equiv> |
|
571 (\<forall> ctxt \<in> sectxts_of_sproc_sshms sshms. permission_check pctxt ctxt C_shm P_inherit)" |
|
572 |
|
573 (* |
|
574 fun info_flow_sshm :: "t_sproc \<Rightarrow> t_sproc \<Rightarrow> bool" |
|
575 where |
|
576 "info_flow_sshm (pi,sec,fds,shms) (pi',sec',fds',shms') = |
|
577 (\<exists> sh flag'. (sh, SHM_RDWR) \<in> shms \<and> (sh, flag') \<in> shms')" |
|
578 *) |
|
579 definition info_flow_sproc_sshms :: "t_sproc_sshm set \<Rightarrow> t_sproc_sshm set \<Rightarrow> bool" |
|
580 where |
|
581 "info_flow_sproc_sshms shms shms' \<equiv> (\<exists> sh flag'. (sh, SHM_RDWR) \<in> shms \<and> (sh, flag') \<in> shms')" |
|
582 |
|
583 (* |
|
584 fun info_flow_sshm :: "t_sproc \<Rightarrow> t_sproc \<Rightarrow> bool" |
|
585 where |
|
586 "info_flow_sshm (pi,sec,fds,shms) (pi',sec',fds',shms') = info_flow_sproc_sshms shms shms'" |
|
587 *) |
|
588 inductive info_flow_sshm :: "t_sproc \<Rightarrow> t_sproc \<Rightarrow> bool" |
|
589 where |
|
590 "info_flow_sshm sp sp" |
|
591 | "\<lbrakk>info_flow_sshm sp (pi,sec,fds,shms); info_flow_sproc_sshms shms shms'\<rbrakk> |
|
592 \<Longrightarrow> info_flow_sshm sp (pi',sec',fds',shms')" |
|
593 |
|
594 |
|
595 (* |
|
596 fun smsg_related :: "t_msg \<Rightarrow> t_smsg list \<Rightarrow> bool" |
|
597 where |
|
598 "smsg_related m [] = False" |
|
599 | "smsg_related m ((mi, sec, tag)#sms) = |
|
600 (if (mi = Init m) then True else smsg_related m sms)" |
|
601 |
|
602 fun smsgq_smsg_related :: "t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsgq \<Rightarrow> bool" |
|
603 where |
|
604 "smsgq_smsg_related q m (qi, sec, smsgslist) = ((qi = Init q) \<and> (smsg_related m smsgslist))" |
|
605 |
|
606 fun smsg_relatainted :: "t_msg \<Rightarrow> t_smsg list \<Rightarrow> bool" |
|
607 where |
|
608 "smsg_relatainted m [] = False" |
|
609 | "smsg_relatainted m ((mi, sec, tag)#sms) = |
|
610 (if (mi = Init m \<and> tag = True) then True else smsg_relatainted m sms)" |
|
611 |
|
612 fun smsgq_smsg_relatainted :: "t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsgq \<Rightarrow> bool" |
|
613 where |
|
614 "smsgq_smsg_relatainted q m (qi, sec, smsgslist) = |
|
615 ((qi = Init q) \<and> (smsg_relatainted m smsgslist))" |
|
616 *) |
|
617 |
|
618 fun sfile_related :: "t_sfile \<Rightarrow> t_file \<Rightarrow> bool" |
|
619 where |
|
620 "sfile_related (fi,sec,psec,asecs) f = (fi = Init f)" |
|
621 (* |
|
622 fun sproc_related :: "t_process \<Rightarrow> t_sproc \<Rightarrow> bool" |
|
623 where |
|
624 "sproc_related p (pi, sec, fds, shms) = (pi = Init p)" |
|
625 *) |
|
626 fun init_obj_related :: "t_sobject \<Rightarrow> t_object \<Rightarrow> bool" |
|
627 where |
|
628 "init_obj_related (S_proc (pi, sec, fds, shms) tag) (O_proc p') = (pi = Init p')" |
|
629 | "init_obj_related (S_file sfs tag) (O_file f) = (\<exists> sf \<in> sfs. sfile_related sf f)" |
|
630 | "init_obj_related (S_dir sf) (O_dir f) = (sfile_related sf f)" |
|
631 | "init_obj_related (S_msgq (qi, sec, sms)) (O_msgq q') = (qi = Init q')" |
|
632 | "init_obj_related (S_shm (hi, sec)) (O_shm h') = (hi = Init h')" |
|
633 (* |
|
634 | "init_obj_related (S_msg (qi, sec, sms) (mi, secm, tagm)) (O_msg q' m') = (qi = Init q' \<and> mi = Init m')" |
|
635 *) |
|
636 | "init_obj_related _ _ = False" |
|
637 |
|
638 |
|
639 |
815 (***************** for backward proof when Instancing static objects ******************) |
640 (***************** for backward proof when Instancing static objects ******************) |
816 |
641 |
817 definition next_nat :: "nat set \<Rightarrow> nat" |
642 definition next_nat :: "nat set \<Rightarrow> nat" |
818 where |
643 where |
819 "next_nat nset = (Max nset) + 1" |
644 "next_nat nset = (Max nset) + 1" |