1113 | "get_parentfs_ctxts s (f#pf) = |
1113 | "get_parentfs_ctxts s (f#pf) = |
1114 (case (get_parentfs_ctxts s pf, sectxt_of_obj s (O_dir (f#pf))) of |
1114 (case (get_parentfs_ctxts s pf, sectxt_of_obj s (O_dir (f#pf))) of |
1115 (Some ctxts, Some ctxt) \<Rightarrow> Some (ctxt#ctxts) |
1115 (Some ctxts, Some ctxt) \<Rightarrow> Some (ctxt#ctxts) |
1116 | _ \<Rightarrow> None)" |
1116 | _ \<Rightarrow> None)" |
1117 |
1117 |
|
1118 definition search_check_ctxt:: |
|
1119 "security_context_t \<Rightarrow> security_context_t \<Rightarrow> security_context_t set \<Rightarrow> bool \<Rightarrow> bool" |
|
1120 where |
|
1121 "search_check_ctxt pctxt fctxt asecs if_file \<equiv> ( |
|
1122 if if_file |
|
1123 then search_check_file pctxt fctxt \<and> search_check_allp pctxt asecs |
|
1124 else search_check_dir pctxt fctxt \<and> search_check_allp pctxt asecs )" |
|
1125 |
1118 fun search_check :: "t_state \<Rightarrow> security_context_t \<Rightarrow> t_file \<Rightarrow> bool" |
1126 fun search_check :: "t_state \<Rightarrow> security_context_t \<Rightarrow> t_file \<Rightarrow> bool" |
1119 where |
1127 where |
1120 "search_check s pctxt [] = |
1128 "search_check s pctxt [] = |
1121 (case (sectxt_of_obj s (O_dir [])) of |
1129 (case (sectxt_of_obj s (O_dir [])) of |
1122 Some fctxt \<Rightarrow> search_check_dir pctxt fctxt |
1130 Some fctxt \<Rightarrow> search_check_ctxt pctxt fctxt {} False |
1123 | _ \<Rightarrow> False)" |
1131 | _ \<Rightarrow> False)" |
1124 | "search_check s pctxt (f#pf) = |
1132 | "search_check s pctxt (f#pf) = |
1125 (if (is_file s (f#pf)) |
1133 (if (is_file s (f#pf)) |
1126 then (case (sectxt_of_obj s (O_file (f#pf)), get_parentfs_ctxts s pf) of |
1134 then (case (sectxt_of_obj s (O_file (f#pf)), get_parentfs_ctxts s pf) of |
1127 (Some fctxt, Some pfctxts) \<Rightarrow> (search_check_file pctxt fctxt \<and> search_check_allp pctxt (set pfctxts)) |
1135 (Some fctxt, Some pfctxts) \<Rightarrow> search_check_ctxt pctxt fctxt (set pfctxts) True |
1128 | _ \<Rightarrow> False) |
1136 | _ \<Rightarrow> False) |
1129 else (case (sectxt_of_obj s (O_dir (f#pf)), get_parentfs_ctxts s pf) of |
1137 else (case (sectxt_of_obj s (O_dir (f#pf)), get_parentfs_ctxts s pf) of |
1130 (Some fctxt, Some pfctxts) \<Rightarrow> (search_check_dir pctxt fctxt \<and> search_check_allp pctxt (set pfctxts)) |
1138 (Some fctxt, Some pfctxts) \<Rightarrow> search_check_ctxt pctxt fctxt (set pfctxts) False |
1131 | _ \<Rightarrow> False))" |
1139 | _ \<Rightarrow> False))" |
1132 |
1140 |
1133 (* this means we should prove every current fd has a security context! *) |
1141 (* this means we should prove every current fd has a security context! *) |
1134 definition sectxts_of_fds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd set \<Rightarrow> security_context_t set" |
1142 definition sectxts_of_fds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd set \<Rightarrow> security_context_t set" |
1135 where |
1143 where |
1136 "sectxts_of_fds s p fds \<equiv> {ctxt. \<exists> fd \<in> fds. sectxt_of_obj s (O_fd p fd) = Some ctxt}" |
1144 "sectxts_of_fds s p fds \<equiv> {ctxt. \<exists> fd \<in> fds. sectxt_of_obj s (O_fd p fd) = Some ctxt}" |
1137 |
1145 |
|
1146 definition inherit_fds_check_ctxt:: "security_context_t \<Rightarrow> security_context_t set \<Rightarrow> bool" |
|
1147 where |
|
1148 "inherit_fds_check_ctxt p fds \<equiv> (\<forall> ctxt \<in> fds. permission_check p ctxt C_fd P_inherit)" |
|
1149 |
1138 definition inherit_fds_check :: "t_state \<Rightarrow> security_context_t \<Rightarrow> t_process \<Rightarrow> t_fd set \<Rightarrow> bool" |
1150 definition inherit_fds_check :: "t_state \<Rightarrow> security_context_t \<Rightarrow> t_process \<Rightarrow> t_fd set \<Rightarrow> bool" |
1139 where |
1151 where |
1140 "inherit_fds_check s npsectxt p fds \<equiv> |
1152 "inherit_fds_check s npsectxt p fds \<equiv> inherit_fds_check_ctxt npsectxt (sectxts_of_fds s p fds)" |
1141 (\<forall> ctxt \<in> sectxts_of_fds s p fds. permission_check npsectxt ctxt C_fd P_inherit)" |
|
1142 |
1153 |
1143 fun npctxt_execve :: "security_context_t \<Rightarrow> security_context_t \<Rightarrow> security_context_t option" |
1154 fun npctxt_execve :: "security_context_t \<Rightarrow> security_context_t \<Rightarrow> security_context_t option" |
1144 where |
1155 where |
1145 "npctxt_execve (pu,pr,pt) (fu,fr,ft) = |
1156 "npctxt_execve (pu,pr,pt) (fu,fr,ft) = |
1146 (case (role_transition pr ft) of |
1157 (case (role_transition pr ft) of |
1163 |
1174 |
1164 definition sectxts_of_shms :: "t_state \<Rightarrow> t_shm set \<Rightarrow> security_context_t set" |
1175 definition sectxts_of_shms :: "t_state \<Rightarrow> t_shm set \<Rightarrow> security_context_t set" |
1165 where |
1176 where |
1166 "sectxts_of_shms s shms \<equiv> {ctxt. \<exists> h \<in> shms. sectxt_of_obj s (O_shm h) = Some ctxt}" |
1177 "sectxts_of_shms s shms \<equiv> {ctxt. \<exists> h \<in> shms. sectxt_of_obj s (O_shm h) = Some ctxt}" |
1167 |
1178 |
|
1179 definition inherit_shms_check_ctxt:: "security_context_t \<Rightarrow> security_context_t set \<Rightarrow> bool" |
|
1180 where |
|
1181 "inherit_shms_check_ctxt p shms \<equiv> (\<forall> ctxt \<in> shms. permission_check p ctxt C_shm P_inherit)" |
|
1182 |
1168 definition inherit_shms_check :: "t_state \<Rightarrow> security_context_t \<Rightarrow> t_shm set \<Rightarrow> bool" |
1183 definition inherit_shms_check :: "t_state \<Rightarrow> security_context_t \<Rightarrow> t_shm set \<Rightarrow> bool" |
1169 where |
1184 where |
1170 "inherit_shms_check s npsectxt shms \<equiv> |
1185 "inherit_shms_check s npsectxt shms \<equiv> inherit_shms_check_ctxt npsectxt (sectxts_of_shms s shms)" |
1171 (\<forall> ctxt \<in> sectxts_of_shms s shms. permission_check npsectxt ctxt C_shm P_inherit)" |
|
1172 |
1186 |
1173 fun perm_of_mflag :: "t_open_must_flag \<Rightarrow> permission_t set" |
1187 fun perm_of_mflag :: "t_open_must_flag \<Rightarrow> permission_t set" |
1174 where |
1188 where |
1175 "perm_of_mflag OF_RDONLY = {P_read}" |
1189 "perm_of_mflag OF_RDONLY = {P_read}" |
1176 | "perm_of_mflag OF_WRONLY = {P_write}" |
1190 | "perm_of_mflag OF_WRONLY = {P_write}" |