equal
deleted
inserted
replaced
49 (Some sec, Some psec, Some aseclist) \<Rightarrow> Some (Init f, sec, Some psec, set aseclist) |
49 (Some sec, Some psec, Some aseclist) \<Rightarrow> Some (Init f, sec, Some psec, set aseclist) |
50 | _ \<Rightarrow> None)" |
50 | _ \<Rightarrow> None)" |
51 |
51 |
52 definition init_cfs2sfiles :: "t_file set \<Rightarrow> t_sfile set" |
52 definition init_cfs2sfiles :: "t_file set \<Rightarrow> t_sfile set" |
53 where |
53 where |
54 "init_cfs2sfiles fs \<equiv> {sf. \<exists>f \<in> fs. init_cf2sfile f = Some sf}" |
54 "init_cfs2sfiles fs \<equiv> {sf. \<exists>f \<in> fs. init_cf2sfile f = Some sf \<and> is_init_file f}" |
55 |
55 |
56 definition init_cfd2sfd :: "t_process \<Rightarrow> t_fd \<Rightarrow> (security_context_t \<times> t_open_flags \<times> t_sfile) option" |
56 definition init_cfd2sfd :: "t_process \<Rightarrow> t_fd \<Rightarrow> (security_context_t \<times> t_open_flags \<times> t_sfile) option" |
57 where |
57 where |
58 "init_cfd2sfd p fd = |
58 "init_cfd2sfd p fd = |
59 (case (init_file_of_proc_fd p fd, init_oflags_of_proc_fd p fd, init_sectxt_of_obj (O_fd p fd)) of |
59 (case (init_file_of_proc_fd p fd, init_oflags_of_proc_fd p fd, init_sectxt_of_obj (O_fd p fd)) of |
106 definition init_cq2smsgq :: "t_msgq \<Rightarrow> t_smsgq option" |
106 definition init_cq2smsgq :: "t_msgq \<Rightarrow> t_smsgq option" |
107 where |
107 where |
108 "init_cq2smsgq q \<equiv> (case (init_sectxt_of_obj (O_msgq q), init_cqm2sms q (init_msgs_of_queue q)) of |
108 "init_cq2smsgq q \<equiv> (case (init_sectxt_of_obj (O_msgq q), init_cqm2sms q (init_msgs_of_queue q)) of |
109 (Some sec, Some sms) \<Rightarrow> Some (Init q, sec, sms) |
109 (Some sec, Some sms) \<Rightarrow> Some (Init q, sec, sms) |
110 | _ \<Rightarrow> None)" |
110 | _ \<Rightarrow> None)" |
111 |
|
112 definition init_same_inode_files :: "t_file \<Rightarrow> t_file set" |
|
113 where |
|
114 "init_same_inode_files f \<equiv> {f'. init_inum_of_file f = init_inum_of_file f'}" |
|
115 |
111 |
116 fun init_obj2sobj :: "t_object \<Rightarrow> t_sobject option" |
112 fun init_obj2sobj :: "t_object \<Rightarrow> t_sobject option" |
117 where |
113 where |
118 "init_obj2sobj (O_proc p) = |
114 "init_obj2sobj (O_proc p) = |
119 (case (init_cp2sproc p) of |
115 (case (init_cp2sproc p) of |
718 |
714 |
719 definition cfs2sfiles :: "t_state \<Rightarrow> t_file set \<Rightarrow> t_sfile set" |
715 definition cfs2sfiles :: "t_state \<Rightarrow> t_file set \<Rightarrow> t_sfile set" |
720 where |
716 where |
721 "cfs2sfiles s fs \<equiv> {sf. \<exists> f \<in> fs. cf2sfile s f True = Some sf}" |
717 "cfs2sfiles s fs \<equiv> {sf. \<exists> f \<in> fs. cf2sfile s f True = Some sf}" |
722 |
718 |
723 definition same_inode_files :: "t_state \<Rightarrow> t_file \<Rightarrow> t_file set" |
|
724 where |
|
725 "same_inode_files s f \<equiv> {f'. inum_of_file s f = inum_of_file s f'}" |
|
726 |
|
727 (* here cf2sfile is passed with True, because, process' fds are only for files not dirs *) |
719 (* here cf2sfile is passed with True, because, process' fds are only for files not dirs *) |
728 definition cfd2sfd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd \<Rightarrow> t_sfd option" |
720 definition cfd2sfd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd \<Rightarrow> t_sfd option" |
729 where |
721 where |
730 "cfd2sfd s p fd \<equiv> |
722 "cfd2sfd s p fd \<equiv> |
731 (case (file_of_proc_fd s p fd, flags_of_proc_fd s p fd, sectxt_of_obj s (O_fd p fd)) of |
723 (case (file_of_proc_fd s p fd, flags_of_proc_fd s p fd, sectxt_of_obj s (O_fd p fd)) of |