371 |
371 |
372 lemmas current_has_sec'' = alive_obj_has_sec'' current_proc_has_sec'' is_file_has_sec'' is_dir_has_sec'' |
372 lemmas current_has_sec'' = alive_obj_has_sec'' current_proc_has_sec'' is_file_has_sec'' is_dir_has_sec'' |
373 is_tcp_has_sec'' is_udp_has_sec'' current_fd_has_sec'' init_node_has_sec'' current_shm_has_sec'' |
373 is_tcp_has_sec'' is_udp_has_sec'' current_fd_has_sec'' init_node_has_sec'' current_shm_has_sec'' |
374 current_msgq_has_sec'' current_msg_has_sec'' |
374 current_msgq_has_sec'' current_msg_has_sec'' |
375 |
375 |
|
376 (************ root sec remains ************) |
|
377 |
|
378 lemma root_type_remains: |
|
379 "valid s \<Longrightarrow> type_of_obj s (O_dir []) = init_type_of_obj (O_dir [])" |
|
380 apply (induct s) |
|
381 apply (simp) |
|
382 apply (frule vd_cons, frule vt_grant_os, case_tac a) prefer 6 |
|
383 by (case_tac option, auto) |
|
384 |
|
385 lemma root_user_remains: |
|
386 "valid s \<Longrightarrow> user_of_obj s (O_dir []) = init_user_of_obj (O_dir [])" |
|
387 apply (induct s) |
|
388 apply (simp) |
|
389 apply (frule vd_cons, frule vt_grant_os, case_tac a) prefer 6 |
|
390 by (case_tac option, auto) |
|
391 |
|
392 lemma root_has_type': |
|
393 "\<lbrakk>type_of_obj s (O_dir []) = None; valid s\<rbrakk> \<Longrightarrow> False" |
|
394 apply (drule alive_obj_has_type', simp) |
|
395 by (drule root_is_dir, simp) |
|
396 |
|
397 lemma root_has_user': |
|
398 "\<lbrakk>user_of_obj s (O_dir []) = None; valid s\<rbrakk> \<Longrightarrow> False" |
|
399 apply (drule alive_obj_has_user', simp) |
|
400 by (drule root_is_dir, simp) |
|
401 |
|
402 lemma root_has_init_type': |
|
403 "init_type_of_obj (O_dir []) = None \<Longrightarrow> False" |
|
404 using init_obj_has_type[where obj = "O_dir []"] root_is_init_dir |
|
405 by auto |
|
406 |
|
407 lemma root_has_init_user': |
|
408 "init_user_of_obj (O_dir []) = None \<Longrightarrow> False" |
|
409 using init_obj_has_user[where obj = "O_dir []"] root_is_init_dir |
|
410 by auto |
|
411 |
|
412 lemma root_sec_remains: |
|
413 "valid s \<Longrightarrow> sectxt_of_obj s (O_dir []) = init_sectxt_of_obj (O_dir [])" |
|
414 by (auto simp:root_user_remains root_type_remains sectxt_of_obj_def init_sectxt_of_obj_def |
|
415 split:option.splits) |
|
416 |
|
417 lemma root_sec_set: |
|
418 "\<exists> u t. sec_of_root = (u, R_object, t)" |
|
419 by (auto simp:sec_of_root_def split:option.splits |
|
420 dest!: root_has_init_type' root_has_init_user') |
|
421 |
|
422 lemma sec_of_root_set: |
|
423 "init_sectxt_of_obj (O_dir []) = Some sec_of_root" |
|
424 using root_has_init_type' root_has_init_user' |
|
425 apply (auto simp:init_sectxt_of_obj_def sec_of_root_def split:option.splits) |
|
426 done |
|
427 |
376 (*************** sectxt_of_obj simpset ****************) |
428 (*************** sectxt_of_obj simpset ****************) |
377 |
429 |
378 lemma sec_execve: |
430 lemma sec_execve: |
379 "valid (Execve p f fds # s) \<Longrightarrow> sectxt_of_obj (Execve p f fds # s) = |
431 "valid (Execve p f fds # s) \<Longrightarrow> sectxt_of_obj (Execve p f fds # s) = |
380 (sectxt_of_obj s) (O_proc p := ( |
432 (sectxt_of_obj s) (O_proc p := ( |