|
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 fun init_role_of_obj :: "t_object \<Rightarrow> role_t option" |
|
10 where |
|
11 "init_role_of_obj (O_proc p) = init_role_of_proc p" |
|
12 | "init_role_of_obj _ = Some R_object" |
|
13 |
|
14 definition init_sectxt_of_obj :: "t_object \<Rightarrow> security_context_t option" |
|
15 where |
|
16 "init_sectxt_of_obj obj \<equiv> |
|
17 (case (init_user_of_obj obj, init_role_of_obj obj, init_type_of_obj obj) of |
|
18 (Some u, Some r, Some t) \<Rightarrow> Some (u,r,t) |
|
19 | _ \<Rightarrow> None)" |
|
20 |
|
21 (* |
|
22 definition init_sectxt_of_file:: "t_file \<Rightarrow> security_context_t option" |
|
23 where |
|
24 "init_sectxt_of_file f \<equiv> |
|
25 if (is_init_file f) then init_sectxt_of_obj (O_file f) |
|
26 else if (is_init_dir f) then init_sectxt_of_obj (O_dir f) |
|
27 else None" |
|
28 *) |
|
29 |
|
30 definition sec_of_root :: "security_context_t" |
|
31 where |
|
32 "sec_of_root \<equiv> (case (init_user_of_obj (O_dir []), init_type_of_obj (O_dir [])) of |
|
33 (Some u, Some t) \<Rightarrow> (u, R_object, t))" |
|
34 |
|
35 definition sroot :: "t_sfile" |
|
36 where |
|
37 "sroot \<equiv> (Init [], sec_of_root, None, {})" |
|
38 |
|
39 definition init_cf2sfile :: "t_file \<Rightarrow> t_sfile option" |
|
40 where |
|
41 "init_cf2sfile f \<equiv> |
|
42 case (parent f) of |
|
43 None \<Rightarrow> Some sroot |
|
44 | Some pf \<Rightarrow> if (is_init_file f) then |
|
45 (case (init_sectxt_of_obj (O_file f), init_sectxt_of_obj (O_dir pf), get_parentfs_ctxts [] pf) of |
|
46 (Some sec, Some psec, Some aseclist) \<Rightarrow> Some (Init f, sec, Some psec, set aseclist) |
|
47 | _ \<Rightarrow> None) else |
|
48 (case (init_sectxt_of_obj (O_dir f), init_sectxt_of_obj (O_dir pf), get_parentfs_ctxts [] pf) of |
|
49 (Some sec, Some psec, Some aseclist) \<Rightarrow> Some (Init f, sec, Some psec, set aseclist) |
|
50 | _ \<Rightarrow> None)" |
|
51 |
|
52 definition init_cfs2sfiles :: "t_file set \<Rightarrow> t_sfile set" |
|
53 where |
|
54 "init_cfs2sfiles fs \<equiv> {sf. \<exists>f \<in> fs. init_cf2sfile f = Some sf}" |
|
55 |
|
56 definition init_cfd2sfd :: "t_process \<Rightarrow> t_fd \<Rightarrow> (security_context_t \<times> t_open_flags \<times> t_sfile) option" |
|
57 where |
|
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 |
|
60 (Some f, Some flags, Some sec) \<Rightarrow> (case (init_cf2sfile f) of |
|
61 Some sf \<Rightarrow> Some (sec, flags, sf) |
|
62 | _ \<Rightarrow> None) |
|
63 | _ \<Rightarrow> None)" |
|
64 |
|
65 definition init_cfds2sfds :: "t_process \<Rightarrow> (security_context_t \<times> t_open_flags \<times> t_sfile) set" |
|
66 where |
|
67 "init_cfds2sfds p \<equiv> { sfd. \<exists> fd sfd f. init_file_of_proc_fd p fd = Some f \<and> init_cfd2sfd p fd = Some sfd}" |
|
68 |
|
69 definition init_ch2sshm :: "t_shm \<Rightarrow> t_sshm option" |
|
70 where |
|
71 "init_ch2sshm h \<equiv> (case (init_sectxt_of_obj (O_shm h)) of |
|
72 Some sec \<Rightarrow> Some (Init h, sec) |
|
73 | _ \<Rightarrow> None)" |
|
74 |
|
75 definition init_cph2spshs |
|
76 :: "t_process \<Rightarrow> (t_sshm \<times> t_shm_attach_flag) set" |
|
77 where |
|
78 "init_cph2spshs p \<equiv> {(sh, flag)| sh flag h. (p, flag) \<in> init_procs_of_shm h \<and> |
|
79 init_ch2sshm h = Some sh}" |
|
80 |
|
81 definition init_cp2sproc :: "t_process \<Rightarrow> t_sproc option" |
|
82 where |
|
83 "init_cp2sproc p \<equiv> (case (init_sectxt_of_obj (O_proc p)) of |
|
84 Some sec \<Rightarrow> Some (Init p, sec, (init_cfds2sfds p), (init_cph2spshs p)) |
|
85 | None \<Rightarrow> None)" |
|
86 |
|
87 (* acient files of init-file |
|
88 definition init_o2s_afs :: "t_file \<Rightarrow> security_context_t set" |
|
89 where |
|
90 "init_o2s_afs f \<equiv> {sec. \<exists> f'. f' \<preceq> f \<and> init_sectxt_of_obj (O_dir f') = Some sec}" *) |
|
91 |
|
92 definition init_cm2smsg :: "t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsg option" |
|
93 where |
|
94 "init_cm2smsg q m \<equiv> (case (init_sectxt_of_obj (O_msg q m)) of |
|
95 Some sec \<Rightarrow> Some (Init m, sec, (O_msg q m) \<in> seeds) |
|
96 | _ \<Rightarrow> None)" |
|
97 |
|
98 fun init_cqm2sms :: "t_msgq \<Rightarrow> t_msg list \<Rightarrow> (t_smsg list) option" |
|
99 where |
|
100 "init_cqm2sms q [] = Some []" |
|
101 | "init_cqm2sms q (m#ms) = |
|
102 (case (init_cqm2sms q ms, init_cm2smsg q m) of |
|
103 (Some sms, Some sm) \<Rightarrow> Some (sm # sms) |
|
104 | _ \<Rightarrow> None)" |
|
105 |
|
106 definition init_cq2smsgq :: "t_msgq \<Rightarrow> t_smsgq option" |
|
107 where |
|
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) |
|
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 |
|
116 fun init_obj2sobj :: "t_object \<Rightarrow> t_sobject option" |
|
117 where |
|
118 "init_obj2sobj (O_proc p) = |
|
119 (case (init_cp2sproc p) of |
|
120 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> seeds)) |
|
121 | _ \<Rightarrow> None)" |
|
122 | "init_obj2sobj (O_file f) = |
|
123 (if (f \<in> init_files \<and> is_init_file f) |
|
124 then Some (S_file (init_cfs2sfiles (init_same_inode_files f)) |
|
125 (\<exists> f'. f' \<in> (init_same_inode_files f) \<and> O_file f \<in> seeds)) |
|
126 else None)" |
|
127 | "init_obj2sobj (O_dir f) = |
|
128 (if (is_init_dir f) then |
|
129 (case (init_cf2sfile f) of |
|
130 Some sf \<Rightarrow> Some (S_dir sf) |
|
131 | _ \<Rightarrow> None) |
|
132 else None)" |
|
133 | "init_obj2sobj (O_msgq q) = |
|
134 (case (init_cq2smsgq q) of |
|
135 Some sq \<Rightarrow> Some (S_msgq sq) |
|
136 | _ \<Rightarrow> None)" |
|
137 | "init_obj2sobj (O_shm h) = |
|
138 (case (init_ch2sshm h) of |
|
139 Some sh \<Rightarrow> Some (S_shm sh) |
|
140 | _ \<Rightarrow> None)" |
|
141 | "init_obj2sobj (O_msg q m) = |
|
142 (case (init_cq2smsgq q, init_cm2smsg q m) of |
|
143 (Some sq, Some sm) \<Rightarrow> Some (S_msg sq sm) |
|
144 | _ \<Rightarrow> None)" |
|
145 | "init_obj2sobj _ = None" |
|
146 |
|
147 definition |
|
148 "init_static_state \<equiv> {sobj. \<exists> obj. init_alive obj \<and> init_obj2sobj obj = Some sobj}" |
|
149 |
|
150 fun is_init_sfile :: "t_sfile \<Rightarrow> bool" |
|
151 where |
|
152 "is_init_sfile (Init _, sec, psec,asec) = True" |
|
153 | "is_init_sfile _ = False" |
|
154 |
|
155 fun is_many_sfile :: "t_sfile \<Rightarrow> bool" |
|
156 where |
|
157 "is_many_sfile (Created, sec, psec, asec) = True" |
|
158 | "is_many_sfile _ = False" |
|
159 |
|
160 fun is_init_sproc :: "t_sproc \<Rightarrow> bool" |
|
161 where |
|
162 "is_init_sproc (Init p, sec, fds, shms) = True" |
|
163 | "is_init_sproc _ = False" |
|
164 |
|
165 fun is_many_sproc :: "t_sproc \<Rightarrow> bool" |
|
166 where |
|
167 "is_many_sproc (Created, sec,fds,shms) = True" |
|
168 | "is_many_sproc _ = False" |
|
169 |
|
170 fun is_many_smsg :: "t_smsg \<Rightarrow> bool" |
|
171 where |
|
172 "is_many_smsg (Created,sec,tag) = True" |
|
173 | "is_many_smsg _ = False" |
|
174 |
|
175 fun is_many_smsgq :: "t_smsgq \<Rightarrow> bool" |
|
176 where |
|
177 "is_many_smsgq (Created,sec,sms) = (True \<and> (\<forall> sm \<in> (set sms). is_many_smsg sm))" |
|
178 | "is_many_smsgq _ = False" |
|
179 |
|
180 fun is_many_sshm :: "t_sshm \<Rightarrow> bool" |
|
181 where |
|
182 "is_many_sshm (Created, sec) = True" |
|
183 | "is_many_sshm _ = False" |
|
184 |
|
185 (* |
|
186 fun is_init_sobj :: "t_sobject \<Rightarrow> bool" |
|
187 where |
|
188 "is_init_sobj (S_proc (popt, sec, fds, shms) tag) = (popt \<noteq> None)" |
|
189 | "is_init_sobj (S_file sf tag) = (is_init_sfile sf)" |
|
190 | "is_init_sobj (S_dir sf tag) = (is_init_sfile sf)" |
|
191 | "is_init_sobj (S_msg" *) |
|
192 |
|
193 fun is_many :: "t_sobject \<Rightarrow> bool" |
|
194 where |
|
195 "is_many (S_proc (Many, sec, fds, shms) tag) = True" |
|
196 | "is_many (S_file sfs tag) = (\<forall> sf \<in> sfs. is_many_sfile sf)" |
|
197 | "is_many (S_dir sf ) = is_many_sfile sf" |
|
198 | "is_many (S_msgq sq ) = is_many_smsgq sq" |
|
199 | "is_many (S_shm sh ) = is_many_sshm sh" |
|
200 |
|
201 (* |
|
202 fun update_ss_sp:: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state" |
|
203 where |
|
204 "update_ss_sp ss (S_proc sp tag) (S_proc sp' tag') = |
|
205 (if (is_many_sproc sp) then ss \<union> {S_proc sp' tag'} |
|
206 else (ss - {S_proc sp tag}) \<union> {S_proc sp' tag'})" |
|
207 |
|
208 fun update_ss_sd:: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state" |
|
209 where |
|
210 "update_ss_sd ss (S_dir sf tag) (S_dir sf' tag') = |
|
211 (if (is_many_sfile sf) then ss \<union> {S_dir sf' tag'} |
|
212 else (ss - {S_dir sf tag}) \<union> {S_dir sf' tag'})" |
|
213 *) |
|
214 |
|
215 definition update_ss :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state" |
|
216 where |
|
217 "update_ss ss so so' \<equiv> if (is_many so) then ss \<union> {so'} else (ss - {so}) \<union> {so'}" |
|
218 |
|
219 definition add_ss :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_static_state" |
|
220 where |
|
221 "add_ss ss so \<equiv> ss \<union> {so}" |
|
222 |
|
223 definition del_ss :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_static_state" |
|
224 where |
|
225 "del_ss ss so \<equiv> if (is_many so) then ss else ss - {so}" |
|
226 |
|
227 (* |
|
228 fun sparent :: "t_sfile \<Rightarrow> t_sfile option" |
|
229 where |
|
230 "sparent (Sroot si sec) = None" |
|
231 | "sparent (Sfile si sec spf) = Some spf" |
|
232 |
|
233 inductive is_ancesf :: "t_sfile \<Rightarrow> t_sfile \<Rightarrow> bool" |
|
234 where |
|
235 "is_ancesf sf sf" |
|
236 | "sparent sf = Some spf \<Longrightarrow> is_ancesf spf sf" |
|
237 | "\<lbrakk>sparent sf = Some spf; is_ancesf saf spf\<rbrakk> \<Longrightarrow> is_ancesf saf sf" |
|
238 |
|
239 definition sfile_reparent :: "t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile" |
|
240 where |
|
241 "sfile_reparent (Sroot)" |
|
242 *) |
|
243 |
|
244 (* |
|
245 (* sfds rename aux definitions *) |
|
246 definition sfds_rename_notrelated |
|
247 :: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool" |
|
248 where |
|
249 "sfds_rename_notrelated sfds from to sfds' \<equiv> |
|
250 (\<forall> sec flag sf. (sec,flag,sf) \<in> sfds \<and> (\<not> from \<preceq> sf) \<longrightarrow> (sec,flag,sf) \<in> sfds')" |
|
251 |
|
252 definition sfds_rename_renamed |
|
253 :: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool" |
|
254 where |
|
255 "sfds_rename_renamed sfds sf from to sfds' \<equiv> |
|
256 (\<forall> sec flag sf'. (sec,flag,sf) \<in> sfds \<and> (sf \<preceq> sf') \<longrightarrow> |
|
257 (sec, flag, file_after_rename sf' from to) \<in> sfds' \<and> (sec,flag,sf) \<notin> sfds')" |
|
258 |
|
259 definition sfds_rename_remain |
|
260 :: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool" |
|
261 where |
|
262 "sfds_rename_remain sfds sf from to sfds' \<equiv> |
|
263 (\<forall> sec flag sf'. (sec,flag,sf') \<in> sfds \<and> (sf \<preceq> sf') \<longrightarrow> |
|
264 (sec, flag, sf') \<in> sfds' \<and> (sec,flag, file_after_rename sf' from to) \<notin> sfds')" |
|
265 |
|
266 (* for not many, choose on renamed or not *) |
|
267 definition sfds_rename_choices |
|
268 :: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool" |
|
269 where |
|
270 "sfds_rename_choices sfds sf from to sfds' \<equiv> |
|
271 sfds_rename_remain sfds sf from to sfds' \<or> sfds_rename_renamed sfds sf from to sfds'" |
|
272 |
|
273 (* for many, merge renamed with not renamed *) |
|
274 definition sfds_rename_both |
|
275 :: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool" |
|
276 where |
|
277 "sfds_rename_both sfds sf from to sfds' \<equiv> |
|
278 (\<forall> sec flag sf'. (sec,flag,sf') \<in> sfds \<and> (sf \<preceq> sf') \<longrightarrow> |
|
279 (sec, flag, sf') \<in> sfds' \<or> (sec,flag, file_after_rename sf' from to) \<in> sfds')" |
|
280 |
|
281 (* added to the new sfds, are those only under the new sfile *) |
|
282 definition sfds_rename_added |
|
283 :: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool" |
|
284 where |
|
285 "sfds_rename_added sfds from to sfds' \<equiv> |
|
286 (\<forall> sec' flag' sf' sec flag. (sec',flag',sf') \<in> sfds' \<and> (sec,flag,sf') \<notin> sfds \<longrightarrow> |
|
287 (\<exists> sf. (sec,flag,sf) \<in> sfds \<and> sf' = file_after_rename from to sf))" |
|
288 |
|
289 definition sproc_sfds_renamed |
|
290 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
291 where |
|
292 "sproc_sfds_renamed ss sf from to ss' \<equiv> |
|
293 (\<forall> pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \<in> ss \<longrightarrow> |
|
294 (\<exists> sfds'. S_proc (pi,sec,sfds',sshms) tagp \<in> ss \<and> sfds_rename_renamed sfds sf from to sfds'))" |
|
295 |
|
296 definition sproc_sfds_remain |
|
297 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
298 where |
|
299 "sproc_sfds_remain 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_remain sfds sf from to sfds'))" |
|
302 |
|
303 (* for not many, choose on renamed or not *) |
|
304 definition sproc_sfds_choices |
|
305 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
306 where |
|
307 "sproc_sfds_choices 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_choices sfds sf from to sfds'))" |
|
310 |
|
311 (* for many, merge renamed with not renamed *) |
|
312 definition sproc_sfds_both |
|
313 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
314 where |
|
315 "sproc_sfds_both ss sf from to ss' \<equiv> |
|
316 (\<forall> pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \<in> ss \<longrightarrow> |
|
317 (\<exists> sfds'. S_proc (pi,sec,sfds',sshms) tagp \<in> ss \<and> sfds_rename_both sfds sf from to sfds'))" |
|
318 |
|
319 (* remove (\<forall> sp tag. S_proc sp tag \<in> ss \<longrightarrow> S_proc sp tag \<in> ss'), |
|
320 * cause sfds contains sfs informations *) |
|
321 definition ss_rename_notrelated |
|
322 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
323 where |
|
324 "ss_rename_notrelated ss sf sf' ss' \<equiv> |
|
325 (\<forall> sq. S_msgq sq \<in> ss \<longrightarrow> S_msgq sq \<in> ss') \<and> |
|
326 (\<forall> pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \<in> ss \<longrightarrow> (\<exists> sfds'. |
|
327 S_proc (pi,sec,sfds',sshms) tagp \<in> ss'\<and> sfds_rename_notrelated sfds sf sf' sfds')) \<and> |
|
328 (\<forall> sfs sf'' tag. S_file sfs tag \<in> ss \<and> sf'' \<in> sfs \<and> (\<not> sf \<preceq> sf'') \<longrightarrow> (\<exists> sfs'. |
|
329 S_file sfs tag \<in> ss' \<and> sf'' \<in> sfs')) \<and> |
|
330 (\<forall> sf'' tag. S_dir sf'' tag \<in> ss \<and> (\<not> sf \<preceq> sf'') \<longrightarrow> S_dir sf'' tag \<in> ss')" |
|
331 |
|
332 (* rename from to, from should definited renamed if not many *) |
|
333 definition all_descendant_sf_renamed |
|
334 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
335 where |
|
336 "all_descendant_sf_renamed ss sf from to ss' \<equiv> |
|
337 (\<forall> sfs sf' tagf. sf \<preceq> sf' \<and> S_file sfs tagf \<in> ss \<and> sf' \<in> sfs \<longrightarrow> (\<exists> sfs'. |
|
338 S_file sfs' tagf \<in> ss' \<and> file_after_rename from to sf' \<in> sfs' \<and> sf' \<notin> sfs')) \<and> |
|
339 (\<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> |
|
340 sproc_sfds_renamed ss sf from to ss'" |
|
341 |
|
342 (* not renamed *) |
|
343 definition all_descendant_sf_remain |
|
344 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
345 where |
|
346 "all_descendant_sf_remain ss sf from to ss' \<equiv> |
|
347 (\<forall> sfs sf' tag'. sf \<preceq> sf' \<and> S_file sfs tag' \<in> ss \<and> sf' \<in> sfs \<longrightarrow> (\<exists> sfs'. |
|
348 S_file sfs' tag' \<in> ss \<and> file_after_rename from to sf' \<notin> sfs' \<and> sf' \<in> sfs')) \<and> |
|
349 (\<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> |
|
350 sproc_sfds_remain ss sf from to ss'" |
|
351 |
|
352 definition all_descendant_sf_choices |
|
353 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
354 where |
|
355 "all_descendant_sf_choices ss sf from to ss' \<equiv> |
|
356 all_descendant_sf_renamed ss sf from to ss' \<or> all_descendant_sf_remain ss sf from to ss'" |
|
357 |
|
358 definition all_descendant_sf_both |
|
359 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
360 where |
|
361 "all_descendant_sf_both ss sf from to ss' \<equiv> |
|
362 (\<forall> sfs sf' tag'. sf \<preceq> sf' \<and> S_file sfs tag' \<in> ss \<and> sf' \<in> sfs \<longrightarrow> (\<exists> sfs'. |
|
363 S_file sfs' tag' \<in> ss \<and> file_after_rename from to sf' \<in> sfs' \<or> sf' \<in> sfs')) \<and> |
|
364 (\<forall> sf' tag'. sf \<preceq> sf' \<and> S_dir sf' tag' \<in> ss \<longrightarrow> |
|
365 S_dir (file_after_rename from to sf') tag' \<in> ss' \<or> S_dir sf' tag' \<in> ss') \<and> |
|
366 sproc_sfds_both ss sf from to ss'" |
|
367 |
|
368 definition ss_renamed_file |
|
369 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
370 where |
|
371 "ss_renamed_file ss sf sf' ss' \<equiv> |
|
372 (if (is_many_sfile sf) |
|
373 then all_descendant_sf_choices ss sf sf sf' ss' |
|
374 else all_descendant_sf_renamed ss sf sf sf' ss')" |
|
375 |
|
376 (* added to the new sfs, are those only under the new sfile *) |
|
377 definition sfs_rename_added |
|
378 :: "t_sfile set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile set \<Rightarrow> bool" |
|
379 where |
|
380 "sfs_rename_added sfs from to sfs' \<equiv> |
|
381 (\<forall> sf'. sf' \<in> sfs' \<and> sf' \<notin> sfs \<longrightarrow> (\<exists> sf. sf \<in> sfs \<and> sf' = file_after_rename from to sf))" |
|
382 |
|
383 (* added to the new sfile, are those only under the new sfile *) |
|
384 definition ss_rename_added |
|
385 :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
386 where |
|
387 "ss_rename_added ss from to ss' \<equiv> |
|
388 (\<forall> pi sec fds fds' shms tagp. S_proc (pi, sec, fds,shms) tagp \<in> ss \<and> |
|
389 S_proc (pi,sec,fds',shms) tagp \<in> ss' \<longrightarrow> sfds_rename_added fds from to fds') \<and> |
|
390 (\<forall> sq. S_msgq sq \<in> ss' \<longrightarrow> S_msgq sq \<in> ss) \<and> |
|
391 (\<forall> sfs sfs' tagf. S_file sfs' tagf \<in> ss' \<and> S_file sfs tagf \<in> ss \<longrightarrow> |
|
392 sfs_rename_added sfs from to sfs') \<and> |
|
393 (\<forall> sf' tagf. S_dir sf' tagf \<in> ss' \<and> S_dir sf' tagf \<notin> ss \<longrightarrow> |
|
394 (\<exists> sf. S_dir sf tagf \<in> ss \<and> sf' = file_after_rename from to sf))" |
|
395 |
|
396 definition sfile_alive :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> bool" |
|
397 where |
|
398 "sfile_alive ss sf \<equiv> (\<exists> sfs tagf. sf \<in> sfs \<and> S_file sfs tagf \<in> ss)" |
|
399 |
|
400 definition sf_alive :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> bool" |
|
401 where |
|
402 "sf_alive ss sf \<equiv> (\<exists> tagd. S_dir sf tagd \<in> ss) \<or> sfile_alive ss sf" |
|
403 |
|
404 (* constrains that the new static state should satisfy *) |
|
405 definition ss_rename:: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
406 where |
|
407 "ss_rename ss sf sf' ss' \<equiv> |
|
408 ss_rename_notrelated ss sf sf' ss' \<and> |
|
409 ss_renamed_file ss sf sf' ss' \<and> ss_rename_added ss sf sf' ss' \<and> |
|
410 (\<forall> sf''. sf_alive ss sf'' \<and> sf \<prec> sf'' \<longrightarrow> |
|
411 (if (is_many_sfile sf'') |
|
412 then all_descendant_sf_choices ss sf'' sf sf' ss' |
|
413 else all_descendant_sf_both ss sf'' sf sf' ss'))" |
|
414 |
|
415 (* two sfile, the last fname should not be equal *) |
|
416 fun sfile_same_fname:: "t_sfile \<Rightarrow> t_sfile \<Rightarrow> bool" |
|
417 where |
|
418 "sfile_same_fname ((Init n, sec)#spf) ((Init n', sec')#spf') = (n = n')" |
|
419 | "sfile_same_fname _ _ = False" |
|
420 |
|
421 (* no same init sfile/only sfile in the target-to spf, should be in static_state addmissble check *) |
|
422 definition ss_rename_no_same_fname:: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> bool" |
|
423 where |
|
424 "ss_rename_no_same_fname ss from spf \<equiv> |
|
425 \<not> (\<exists> to. sfile_same_fname from to \<and> parent to = Some spf \<and> sf_alive ss to)" |
|
426 |
|
427 (* is not a function, is a relation (one 2 many) |
|
428 definition update_ss_rename :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state" |
|
429 where |
|
430 "update_ss_rename ss sf sf' \<equiv> if (is_many_sfile sf) |
|
431 then (ss \<union> {S_file (file_after_rename sf sf' sf'') tag | sf'' tag. sf \<preceq> sf'' \<and> S_file sf'' tag \<in> ss} |
|
432 \<union> {S_dir (file_after_rename sf sf' sf'') tag | sf'' tag. sf \<preceq> sf'' \<and> S_dir sf'' tag \<in> ss}) |
|
433 else (ss - {S_file sf'' tag | sf'' tag. sf \<preceq> sf'' \<and> S_file sf'' tag \<in> ss} |
|
434 - {S_dir sf'' tag | sf'' tag. sf \<preceq> sf'' \<and> S_dir sf'' tag \<in> ss}) |
|
435 \<union> {S_file (file_after_rename sf sf' sf'') tag | sf'' tag. sf \<preceq> sf'' \<and> S_file sf'' tag \<in> ss} |
|
436 \<union> {S_dir (file_after_rename sf sf' sf'') tag | sf'' tag. sf \<preceq> sf'' \<and> S_dir sf'' tag \<in> ss}" |
|
437 *) |
|
438 *) |
|
439 |
|
440 fun sectxt_of_sproc :: "t_sproc \<Rightarrow> security_context_t" |
|
441 where |
|
442 "sectxt_of_sproc (pi,sec,fds,shms) = sec" |
|
443 |
|
444 fun sectxt_of_sfile :: "t_sfile \<Rightarrow> security_context_t" |
|
445 where |
|
446 "sectxt_of_sfile (fi,sec,psec,asecs) = sec" |
|
447 |
|
448 fun asecs_of_sfile :: "t_sfile \<Rightarrow> security_context_t set" |
|
449 where |
|
450 "asecs_of_sfile (fi,sec,psec,asecs) = asecs" |
|
451 |
|
452 definition search_check_s :: "security_context_t \<Rightarrow> t_sfile \<Rightarrow> bool \<Rightarrow> bool" |
|
453 where |
|
454 "search_check_s pctxt sf if_file = |
|
455 (if if_file |
|
456 then search_check_file pctxt (sectxt_of_sfile sf) \<and> search_check_allp pctxt (asecs_of_sfile sf) |
|
457 else search_check_dir pctxt (sectxt_of_sfile sf) \<and> search_check_allp pctxt (asecs_of_sfile sf))" |
|
458 |
|
459 definition sectxts_of_sfds :: "t_sfd set \<Rightarrow> security_context_t set" |
|
460 where |
|
461 "sectxts_of_sfds sfds \<equiv> {ctxt. \<exists> flag sf. (ctxt, flag, sf) \<in> sfds}" |
|
462 |
|
463 definition inherit_fds_check_s :: "security_context_t \<Rightarrow> t_sfd set \<Rightarrow> bool" |
|
464 where |
|
465 "inherit_fds_check_s pctxt sfds \<equiv> |
|
466 (\<forall> ctxt \<in> sectxts_of_sfds sfds. permission_check pctxt ctxt C_fd P_inherit)" |
|
467 |
|
468 definition sectxts_of_sproc_sshms :: "t_sproc_sshm set \<Rightarrow> security_context_t set" |
|
469 where |
|
470 "sectxts_of_sproc_sshms sshms \<equiv> {ctxt. \<exists> hi flag. ((hi, ctxt),flag) \<in> sshms}" |
|
471 |
|
472 definition inherit_shms_check_s :: "security_context_t \<Rightarrow> t_sproc_sshm set \<Rightarrow> bool" |
|
473 where |
|
474 "inherit_shms_check_s pctxt sshms \<equiv> |
|
475 (\<forall> ctxt \<in> sectxts_of_sproc_sshms sshms. permission_check pctxt ctxt C_shm P_inherit)" |
|
476 |
|
477 (* |
|
478 fun info_flow_sshm :: "t_sproc \<Rightarrow> t_sproc \<Rightarrow> bool" |
|
479 where |
|
480 "info_flow_sshm (pi,sec,fds,shms) (pi',sec',fds',shms') = |
|
481 (\<exists> sh flag'. (sh, SHM_RDWR) \<in> shms \<and> (sh, flag') \<in> shms')" |
|
482 *) |
|
483 definition info_flow_sproc_sshms :: "t_sproc_sshm set \<Rightarrow> t_sproc_sshm set \<Rightarrow> bool" |
|
484 where |
|
485 "info_flow_sproc_sshms shms shms' \<equiv> (\<exists> sh flag'. (sh, SHM_RDWR) \<in> shms \<and> (sh, flag') \<in> shms')" |
|
486 |
|
487 fun info_flow_sshm :: "t_sproc \<Rightarrow> t_sproc \<Rightarrow> bool" |
|
488 where |
|
489 "info_flow_sshm (pi,sec,fds,shms) (pi',sec',fds',shms') = info_flow_sproc_sshms shms shms'" |
|
490 |
|
491 definition update_ss_shms :: "t_static_state \<Rightarrow> t_sproc \<Rightarrow> bool \<Rightarrow> t_static_state" |
|
492 where |
|
493 "update_ss_shms ss spfrom tag \<equiv> {sobj. \<exists> sobj' \<in> ss. |
|
494 (case sobj' of |
|
495 S_proc sp tagp \<Rightarrow> if (info_flow_sshm spfrom sp) |
|
496 then if (is_many_sproc sp) |
|
497 then (sobj = S_proc sp tagp \<or> sobj = S_proc sp (tagp \<or> tag)) |
|
498 else (sobj = S_proc sp (tagp \<or> tag)) |
|
499 else (sobj = S_proc sp tag) |
|
500 | _ \<Rightarrow> sobj = sobj')}" |
|
501 |
|
502 |
|
503 |
|
504 (* all reachable static states(sobjects set) *) |
|
505 inductive_set static :: "t_static_state set" |
|
506 where |
|
507 s_init: "init_static_state \<in> static" |
|
508 | s_execve: "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; S_file sfs tagf \<in> ss; |
|
509 (fi,fsec,pfsec,asecs) \<in> sfs; npctxt_execve pctxt fsec = Some pctxt'; |
|
510 grant_execve pctxt fsec pctxt'; search_check_s pctxt (fi,fsec,pfsec,asecs) True; |
|
511 inherit_fds_check_s pctxt' fds'; fds' \<subseteq> fds\<rbrakk> |
|
512 \<Longrightarrow> (update_ss ss (S_proc (pi, pctxt, fds, shms) tagp) |
|
513 (S_proc (pi, pctxt', fds', {}) (tagp \<or> tagf))) \<in> static" |
|
514 | s_clone: "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; |
|
515 permission_check pctxt pctxt C_process P_fork; |
|
516 inherit_fds_check_s pctxt fds'; fds' \<subseteq> fds; |
|
517 inherit_shms_check_s pctxt shms'; shms' \<subseteq> shms\<rbrakk> |
|
518 \<Longrightarrow> (add_ss ss (S_proc (Created, pctxt, fds', shms') tagp)) \<in> static" |
|
519 | s_kill: "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; |
|
520 S_proc (pi', pctxt', fds', shms') tagp' \<in> ss; |
|
521 permission_check pctxt pctxt' C_process P_sigkill\<rbrakk> |
|
522 \<Longrightarrow> (del_ss ss (S_proc (pi', pctxt', fds', shms') tagp')) \<in> static" |
|
523 | s_ptrace: "\<lbrakk>ss \<in> static; S_proc sp tagp \<in> ss; S_proc sp' tagp' \<in> ss; |
|
524 permission_check (sextxt_of_sproc sp) (sectxt_of_sproc sp') C_process P_ptrace\<rbrakk> |
|
525 \<Longrightarrow> (update_ss_shms (update_ss_shms ss sp tagp) sp' tagp') \<in> static" |
|
526 | s_exit: "\<lbrakk>ss \<in> static; S_proc sp tagp \<in> ss\<rbrakk> \<Longrightarrow> (del_ss ss (S_proc sp tagp)) \<in> static" |
|
527 | s_open: "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; S_file sfs tagf \<in> ss; sf \<in> sfs; |
|
528 search_check_s pctxt sf True; \<not> is_creat_excl_flag flags; |
|
529 oflags_check flags pctxt (sectxt_of_sfile sf); permission_check pctxt pctxt C_fd P_setattr\<rbrakk> |
|
530 \<Longrightarrow> (update_ss ss (S_proc (pi, pctxt, fds, shms) tagp) |
|
531 (S_proc (pi, pctxt, fds \<union> {(pctxt,flags,sf)}, shms) tagp)) \<in> static" |
|
532 | s_open': "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; is_creat_excl_flag flags; |
|
533 S_dir (pfi,fsec,pfsec,asecs) \<in> ss; search_check_s pctxt (pfi,fsec,pfsec,asecs) False; |
|
534 nfsec = nfctxt_create pctxt fsec C_file; oflags_check flags pctxt nfsec; |
|
535 permission_check pctxt fsec C_dir P_add_rename; permission_check pctxt pctxt C_fd P_setattr\<rbrakk> |
|
536 \<Longrightarrow> (update_ss (add_ss ss (S_file {(Created, nfsec, Some fsec, asecs \<union> {fsec})} tagp)) |
|
537 (S_proc (pi, pctxt, fds, shms) tagp) |
|
538 (S_proc (pi, pctxt, fds \<union> {(pctxt, flags, (Created, nfsec, Some fsec, asecs \<union> {fsec}))}, shms) tagp) |
|
539 ) \<in> static" |
|
540 | S_readf: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; (fdctxt,flags,sf) \<in> fds; |
|
541 permission_check pctxt fdctxt C_fd P_setattr; S_file sfs tagf \<in> ss; sf \<in> sfs; |
|
542 permission_check pctxt (sectxt_of_sfile sf) C_file P_read; is_read_flag flags\<rbrakk> |
|
543 \<Longrightarrow> (update_ss_shms ss (pi, pctxt,fds,shms) (tagp \<or> tagf)) \<in> static" |
|
544 | S_writef: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; (fdctxt,flags,sf) \<in> fds; |
|
545 permission_check pctxt fdctxt C_fd P_setattr; sf \<in> sfs; S_file sfs tagf \<in> ss; |
|
546 permission_check pctxt (sectxt_of_sfile sf) C_file P_write; is_write_flag flags\<rbrakk> |
|
547 \<Longrightarrow> (update_ss ss (S_file sfs tagf) (S_file sfs (tagp \<or> tagf))) \<in> static" |
|
548 | S_unlink: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_file sfs tagf \<in> ss; |
|
549 (Init f,fsec,Some pfsec,asecs) \<in> sfs; |
|
550 search_check_s pctxt (Init f,fsec,Some pfsec,asecs) True; |
|
551 permission_check pctxt fsec C_file P_unlink; |
|
552 permission_check pctxt pfsec C_dir P_remove_name\<rbrakk> |
|
553 \<Longrightarrow> ((ss - {S_file sfs tagf}) \<union> {S_file (sfs - {(Init f,fsec,Some pfsec,asecs)}) tagf}) \<in> static" |
|
554 | S_rmdir: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; |
|
555 S_dir (fi,fsec,Some pfsec,asecs) \<in> ss; |
|
556 search_check_s pctxt (fi,fsec,Some pfsec,asecs) False; |
|
557 permission_check pctxt fsec C_dir P_rmdir; |
|
558 permission_check pctxt pfsec C_dir P_remove_name\<rbrakk> |
|
559 \<Longrightarrow> (del_ss ss (S_dir (fi,fsec,Some pfsec,asecs))) \<in> static" |
|
560 | S_mkdir: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_dir (fi,fsec,pfsec,asecs) \<in> ss; |
|
561 search_check_s pctxt (fi,fsec,pfsec,asecs) False; |
|
562 permission_check pctxt (nfctxt_create pctxt fsec C_dir) C_dir P_create; |
|
563 permission_check pctxt fsec C_dir P_add_name\<rbrakk> |
|
564 \<Longrightarrow> (add_ss ss (S_dir (Created,nfctxt_create pctxt fsec C_dir,Some fsec,asecs \<union> {fsec}))) \<in> static" |
|
565 | s_link: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_dir (pfi,pfsec,ppfsec,asecs) \<in> ss; |
|
566 S_file sfs tagf \<in> ss; sf \<in> sfs; nfsec = nfctxt_create pctxt pfsec C_file; |
|
567 search_check_s pctxt (pfi,pfsec,ppfsec,asecs) False; search_check_s pctxt sf True; |
|
568 permission_check pctxt (sectxt_of_sfile sf) C_file P_link; |
|
569 permission_check pctxt pfsec C_dir P_add_name\<rbrakk> |
|
570 \<Longrightarrow> (update_ss ss (S_file sfs tagf) |
|
571 (S_file (sfs \<union> {(Created,nfsec,Some pfsec, asecs \<union> {pfsec})}) tagf)) \<in> static" |
|
572 | s_trunc: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_file sfs tagf \<in> ss; sf \<in> sfs; |
|
573 search_check_s pctxt sf True; permission_check pctxt (sectxt_of_sfile sf) C_file P_setattr\<rbrakk> |
|
574 \<Longrightarrow> (update_ss ss (S_file sfs tagf) (S_file sfs (tagf \<or> tagp))) \<in> static" |
|
575 (* |
|
576 | s_rename: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_file sfs tagf \<in> ss; |
|
577 (sf#spf') \<in> sfs; S_dir spf tagpf \<in> ss; \<not>((sf#spf') \<preceq> (sf#spf)); |
|
578 search_check_s pctxt spf False; search_check_s pctxt (sf#spf') True; |
|
579 sectxt_of_sfile (sf#spf') = Some fctxt; sectxt_of_sfile spf = Some pfctxt; |
|
580 permission_check pctxt fctxt C_file P_rename; |
|
581 permission_check pctxt pfctxt C_dir P_add_name; |
|
582 ss_rename ss (sf#spf') (sf#spf) ss'; |
|
583 ss_rename_no_same_fname ss (sf#spf') (sf#spf)\<rbrakk> |
|
584 \<Longrightarrow> ss' \<in> static" |
|
585 | s_rename': "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_dir (sf#spf') tagf \<in> ss; |
|
586 S_dir spf tagpf \<in> ss; \<not>((sf#spf') \<preceq> (sf#spf)); |
|
587 search_check_s pctxt spf False; search_check_s pctxt (sf#spf') True; |
|
588 sectxt_of_sfile (sf#spf') = Some fctxt; sectxt_of_sfile spf = Some pfctxt; |
|
589 permission_check pctxt fctxt C_dir P_reparent; |
|
590 permission_check pctxt pfctxt C_dir P_add_name; |
|
591 ss_rename ss (sf#spf') (sf#spf) ss'; |
|
592 ss_rename_no_same_fname ss (sf#spf') (sf#spf)\<rbrakk> |
|
593 \<Longrightarrow> ss' \<in> static" |
|
594 *) |
|
595 | s_createq: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; |
|
596 permission_check pctxt pctxt C_msgq P_associate; |
|
597 permission_check pctxt pctxt C_msgq P_create\<rbrakk> |
|
598 \<Longrightarrow> (add_ss ss (S_msgq (Created,pctxt,[]))) \<in> static" |
|
599 | s_sendmsg: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_msgq (qi,qctxt,sms) \<in> ss; |
|
600 permission_check pctxt qctxt C_msgq P_enqueue; |
|
601 permission_check pctxt qctxt C_msgq P_write; |
|
602 permission_check pctxt pctxt C_msg P_create\<rbrakk> |
|
603 \<Longrightarrow> (update_ss ss (S_msgq (qi,qctxt,sms)) |
|
604 (S_msgq (qi,qctxt,sms @ [(Created, pctxt, tagp)]))) \<in> static" |
|
605 | s_recvmsg: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; |
|
606 S_msgq (qi,qctxt,(mi,mctxt,tagm)#sms) \<in> ss; |
|
607 permission_check pctxt qctxt C_msgq P_read; |
|
608 permission_check pctxt mctxt C_msg P_receive\<rbrakk> |
|
609 \<Longrightarrow> (update_ss_shms ss (pi,pctxt,fds,shms) (tagp \<or> tagm)) \<in> static" |
|
610 | s_removeq: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_msgq (qi,qctxt,sms) \<in> ss; |
|
611 permission_check pctxt qctxt C_msgq P_destroy\<rbrakk> |
|
612 \<Longrightarrow> (del_ss ss (S_msgq (qi,qctxt,sms))) \<in> static" |
|
613 | s_createh: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; |
|
614 permission_check pctxt pctxt C_shm P_associate; |
|
615 permission_check pctxt pctxt C_shm P_create\<rbrakk> |
|
616 \<Longrightarrow> (add_ss ss (S_shm (Created, pctxt))) \<in> static" |
|
617 | s_attach: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_shm (hi,hctxt) \<in> ss; |
|
618 if flag = SHM_RDONLY then permission_check pctxt hctxt C_shm P_read |
|
619 else (permission_check pctxt hctxt C_shm P_read \<and> |
|
620 permission_check pctxt hctxt C_shm P_write)\<rbrakk> |
|
621 \<Longrightarrow> (update_ss ss (S_proc (pi,pctxt,fds,shms) tagp) |
|
622 (S_proc (pi,pctxt,fds,shms \<union> {((hi,hctxt),flag)}) tagp)) \<in> static" |
|
623 | s_detach: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_shm sh \<in> ss; |
|
624 (sh,flag) \<in> shms; \<not> is_many_sshm sh\<rbrakk> |
|
625 \<Longrightarrow> (update_ss ss (S_proc (pi,pctxt,fds,shms) tagp) |
|
626 (S_proc (pi,pctxt,fds,shms - {(sh,flag)}) tagp)) \<in> static" |
|
627 | s_deleteh: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_shm (hi,hctxt) \<in> ss; |
|
628 permission_check pctxt hctxt C_shm P_destroy; \<not> is_many_sshm sh\<rbrakk> |
|
629 \<Longrightarrow> (remove_sproc_sshm (del_ss ss (S_shm (hi,hctxt))) (hi,hctxt)) \<in> static" |
|
630 |
|
631 (* |
|
632 fun smsg_related :: "t_msg \<Rightarrow> t_smsg list \<Rightarrow> bool" |
|
633 where |
|
634 "smsg_related m [] = False" |
|
635 | "smsg_related m ((mi, sec, tag)#sms) = |
|
636 (if (mi = Init m) then True else smsg_related m sms)" |
|
637 |
|
638 fun smsgq_smsg_related :: "t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsgq \<Rightarrow> bool" |
|
639 where |
|
640 "smsgq_smsg_related q m (qi, sec, smsgslist) = ((qi = Init q) \<and> (smsg_related m smsgslist))" |
|
641 |
|
642 fun smsg_relatainted :: "t_msg \<Rightarrow> t_smsg list \<Rightarrow> bool" |
|
643 where |
|
644 "smsg_relatainted m [] = False" |
|
645 | "smsg_relatainted m ((mi, sec, tag)#sms) = |
|
646 (if (mi = Init m \<and> tag = True) then True else smsg_relatainted m sms)" |
|
647 |
|
648 fun smsgq_smsg_relatainted :: "t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsgq \<Rightarrow> bool" |
|
649 where |
|
650 "smsgq_smsg_relatainted q m (qi, sec, smsgslist) = |
|
651 ((qi = Init q) \<and> (smsg_relatainted m smsgslist))" |
|
652 *) |
|
653 |
|
654 fun sfile_related :: "t_sfile \<Rightarrow> t_file \<Rightarrow> bool" |
|
655 where |
|
656 "sfile_related (fi,sec,psec,asecs) f = (fi = Init f)" |
|
657 (* |
|
658 fun sproc_related :: "t_process \<Rightarrow> t_sproc \<Rightarrow> bool" |
|
659 where |
|
660 "sproc_related p (pi, sec, fds, shms) = (pi = Init p)" |
|
661 *) |
|
662 fun init_obj_related :: "t_sobject \<Rightarrow> t_object \<Rightarrow> bool" |
|
663 where |
|
664 "init_obj_related (S_proc (Init p, sec, fds, shms) tag) (O_proc p') = (p = p')" |
|
665 | "init_obj_related (S_file sfs tag) (O_file f) = (\<exists> sf \<in> sfs. sfile_related sf f)" |
|
666 | "init_obj_related (S_dir sf) (O_dir f) = (sfile_related sf f)" |
|
667 | "init_obj_related (S_msgq (Init q, sec, sms)) (O_msgq q') = (q = q')" |
|
668 | "init_obj_related (S_shm (Init h, sec)) (O_shm h') = (h = h')" |
|
669 | "init_obj_related (S_msg (Init q, sec, sms) (Init m, secm, tagm)) (O_msg q' m') = (q = q' \<and> m = m')" |
|
670 | "init_obj_related _ _ = False" |
|
671 |
|
672 fun tainted_s :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> bool" |
|
673 where |
|
674 "tainted_s ss (S_proc sp tag) = (S_proc sp tag \<in> ss \<and> tag = True)" |
|
675 | "tainted_s ss (S_file sfs tag) = (S_file sfs tag \<in> ss \<and> tag = True)" |
|
676 | "tainted_s ss (S_msg (qi, sec, sms) (mi, secm, tag)) = |
|
677 (S_msgq (qi, sec, sms) \<in> ss \<and> (mi,sec,tag) \<in> set sms \<and> tag = True)" |
|
678 | "tainted_s ss _ = False" |
|
679 |
|
680 (* |
|
681 fun tainted_s :: "t_object \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
682 where |
|
683 "tainted_s (O_proc p) ss = (\<exists> sp. S_proc sp True \<in> ss \<and> sproc_related p sp)" |
|
684 | "tainted_s (O_file f) ss = (\<exists> sfs sf. S_file sfs True \<in> ss \<and> sf \<in> sfs \<and> sfile_related f sf)" |
|
685 | "tainted_s (O_msg q m) ss = (\<exists> sq. S_msgq sq \<in> ss \<and> smsgq_smsg_relatainted q m sq)" |
|
686 | "tainted_s _ ss = False" |
|
687 *) |
|
688 |
|
689 definition taintable_s :: "t_object \<Rightarrow> bool" |
|
690 where |
|
691 "taintable_s obj \<equiv> \<exists> ss \<in> static. \<exists> sobj. tainted_s ss sobj \<and> init_obj_related sobj obj \<and> init_alive obj" |
|
692 |
|
693 definition deletable_s :: "t_object \<Rightarrow> bool" |
|
694 where |
|
695 "deletable_s obj \<equiv> init_alive obj \<and> (\<exists> ss \<in> static. \<forall> sobj \<in> ss. \<not> init_obj_related sobj obj)" |
|
696 |
|
697 definition undeletable_s :: "t_object \<Rightarrow> bool" |
|
698 where |
|
699 "undeletable_s obj \<equiv> init_alive obj \<and> (\<forall> ss \<in> static. \<exists> sobj \<in> ss. init_obj_related sobj obj)" |
|
700 |
|
701 |
|
702 (**************** translation from dynamic to static *******************) |
|
703 |
|
704 definition cf2sfile :: "t_state \<Rightarrow> t_file \<Rightarrow> bool \<Rightarrow> t_sfile option" |
|
705 where |
|
706 "cf2sfile s f Is_file \<equiv> |
|
707 case (parent f) of |
|
708 None \<Rightarrow> if Is_file then None else Some sroot |
|
709 | Some pf \<Rightarrow> if Is_file |
|
710 then (case (sectxt_of_obj s (O_file f), sectxt_of_obj s (O_dir pf), get_parentfs_ctxts s pf) of |
|
711 (Some sec, Some psec, Some asecs) \<Rightarrow> |
|
712 Some (if (\<not> deleted (O_file f) s \<and> is_init_file f) then Init f else Created, sec, Some psec, set asecs) |
|
713 | _ \<Rightarrow> None) |
|
714 else (case (sectxt_of_obj s (O_dir f), sectxt_of_obj s (O_dir pf), get_parentfs_ctxts s pf) of |
|
715 (Some sec, Some psec, Some asecs) \<Rightarrow> |
|
716 Some (if (\<not> deleted (O_dir f) s \<and> is_init_dir f) then Init f else Created, sec, Some psec, set asecs) |
|
717 | _ \<Rightarrow> None)" |
|
718 |
|
719 definition cfs2sfiles :: "t_state \<Rightarrow> t_file set \<Rightarrow> t_sfile set" |
|
720 where |
|
721 "cfs2sfiles s fs \<equiv> {sf. \<exists> f \<in> fs. cf2sfile s f True = Some sf}" |
|
722 |
|
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 *) |
|
728 definition cfd2sfd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd \<Rightarrow> t_sfd option" |
|
729 where |
|
730 "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 |
|
732 (Some f, Some flags, Some sec) \<Rightarrow> (case (cf2sfile s f True) of |
|
733 Some sf \<Rightarrow> Some (sec, flags, sf) |
|
734 | _ \<Rightarrow> None) |
|
735 | _ \<Rightarrow> None)" |
|
736 |
|
737 |
|
738 definition cpfd2sfds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sfd set" |
|
739 where |
|
740 "cpfd2sfds s p \<equiv> {sfd. \<exists> fd sfd f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd}" |
|
741 |
|
742 definition ch2sshm :: "t_state \<Rightarrow> t_shm \<Rightarrow> t_sshm option" |
|
743 where |
|
744 "ch2sshm s h \<equiv> (case (sectxt_of_obj s (O_shm h)) of |
|
745 Some sec \<Rightarrow> |
|
746 Some (if (\<not> deleted (O_shm h) s \<and> h \<in> init_shms) then Init h else Created, sec) |
|
747 | _ \<Rightarrow> None)" |
|
748 |
|
749 definition cph2spshs :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sproc_sshm set" |
|
750 where |
|
751 "cph2spshs s p \<equiv> {(sh, flag) | sh flag h. (p, flag) \<in> procs_of_shm s h \<and> ch2sshm s h = Some sh}" |
|
752 |
|
753 definition cp2sproc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sproc option" |
|
754 where |
|
755 "cp2sproc s p \<equiv> (case (sectxt_of_obj s (O_proc p)) of |
|
756 Some sec \<Rightarrow> |
|
757 Some (if (\<not> deleted (O_proc p) s \<and> p \<in> init_procs) then Init p else Created, sec, |
|
758 cpfd2sfds s p, cph2spshs s p) |
|
759 | _ \<Rightarrow> None)" |
|
760 |
|
761 definition cm2smsg :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsg option" |
|
762 where |
|
763 "cm2smsg s q m \<equiv> (case (sectxt_of_obj s (O_msg q m)) of |
|
764 Some sec \<Rightarrow> |
|
765 Some (if (\<not> deleted (O_msg q m) s \<and> m \<in> set (init_msgs_of_queue q)) then Init m else Created, |
|
766 sec, O_msg q m \<in> tainted s) |
|
767 | _ \<Rightarrow> None)" |
|
768 |
|
769 fun cqm2sms:: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg list \<Rightarrow> (t_smsg list) option" |
|
770 where |
|
771 "cqm2sms s q [] = Some []" |
|
772 | "cqm2sms s q (m#ms) = |
|
773 (case (cqm2sms s q ms, cm2smsg s q m) of |
|
774 (Some sms, Some sm) \<Rightarrow> Some (sm#sms) |
|
775 | _ \<Rightarrow> None)" |
|
776 |
|
777 definition cq2smsgq :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_smsgq option" |
|
778 where |
|
779 "cq2smsgq s q \<equiv> (case (sectxt_of_obj s (O_msgq q), cqm2sms s q (msgs_of_queue s q)) of |
|
780 (Some sec, Some sms) \<Rightarrow> |
|
781 Some (if (\<not> deleted (O_msgq q) s \<and> q \<in> init_msgqs) then Init q else Created, |
|
782 sec, sms) |
|
783 | _ \<Rightarrow> None)" |
|
784 |
|
785 fun co2sobj :: "t_state \<Rightarrow> t_object \<Rightarrow> t_sobject option" |
|
786 where |
|
787 "co2sobj s (O_proc p) = |
|
788 (case (cp2sproc s p) of |
|
789 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s)) |
|
790 | _ \<Rightarrow> None)" |
|
791 | "co2sobj s (O_file f) = |
|
792 (if (f \<in> current_files s) then |
|
793 Some (S_file (cfs2sfiles s (same_inode_files s f)) (O_file f \<in> tainted s)) |
|
794 else None)" |
|
795 | "co2sobj s (O_dir f) = |
|
796 (case (cf2sfile s f False) of |
|
797 Some sf \<Rightarrow> Some (S_dir sf) |
|
798 | _ \<Rightarrow> None)" |
|
799 | "co2sobj s (O_msgq q) = |
|
800 (case (cq2smsgq s q) of |
|
801 Some sq \<Rightarrow> Some (S_msgq sq) |
|
802 | _ \<Rightarrow> None)" |
|
803 | "co2sobj s (O_shm h) = |
|
804 (case (ch2sshm s h) of |
|
805 Some sh \<Rightarrow> Some (S_shm sh) |
|
806 | _ \<Rightarrow> None)" |
|
807 | "co2sobj s (O_msg q m) = |
|
808 (case (cq2smsgq s q, cm2smsg s q m) of |
|
809 (Some sq, Some sm) \<Rightarrow> Some (S_msg sq sm) |
|
810 | _ \<Rightarrow> None)" |
|
811 | "co2sobj s _ = None" |
|
812 |
|
813 |
|
814 (***************** for backward proof when Instancing static objects ******************) |
|
815 |
|
816 definition next_nat :: "nat set \<Rightarrow> nat" |
|
817 where |
|
818 "next_nat nset = (Max nset) + 1" |
|
819 |
|
820 definition new_proc :: "t_state \<Rightarrow> t_process" |
|
821 where |
|
822 "new_proc \<tau> = next_nat (current_procs \<tau>)" |
|
823 |
|
824 definition new_inode_num :: "t_state \<Rightarrow> nat" |
|
825 where |
|
826 "new_inode_num \<tau> = next_nat (current_inode_nums \<tau>)" |
|
827 |
|
828 definition new_msgq :: "t_state \<Rightarrow> t_msgq" |
|
829 where |
|
830 "new_msgq s = next_nat (current_msgqs s)" |
|
831 |
|
832 definition new_msg :: "t_state \<Rightarrow> t_msgq \<Rightarrow> nat" |
|
833 where |
|
834 "new_msg s q = next_nat (set (msgs_of_queue s q))" |
|
835 |
|
836 definition new_shm :: "t_state \<Rightarrow> nat" |
|
837 where |
|
838 "new_shm \<tau> = next_nat (current_shms \<tau>)" |
|
839 |
|
840 definition new_proc_fd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd" |
|
841 where |
|
842 "new_proc_fd \<tau> p = next_nat (current_proc_fds \<tau> p)" |
|
843 |
|
844 definition all_fname_under_dir:: "t_file \<Rightarrow> t_state \<Rightarrow> t_fname set" |
|
845 where |
|
846 "all_fname_under_dir d \<tau> = {fn. \<exists> f. fn # d = f \<and> f \<in> current_files \<tau>}" |
|
847 |
|
848 fun fname_all_a:: "nat \<Rightarrow> t_fname" |
|
849 where |
|
850 "fname_all_a 0 = []" | |
|
851 "fname_all_a (Suc n) = ''a''@(fname_all_a n)" |
|
852 |
|
853 definition fname_length_set :: "t_fname set \<Rightarrow> nat set" |
|
854 where |
|
855 "fname_length_set fns = length`fns" |
|
856 |
|
857 definition next_fname:: "t_file \<Rightarrow> t_state \<Rightarrow> t_fname" |
|
858 where |
|
859 "next_fname pf \<tau> = fname_all_a ((Max (fname_length_set (all_fname_under_dir pf \<tau>))) + 1)" |
|
860 |
|
861 definition new_childf:: "t_file \<Rightarrow> t_state \<Rightarrow> t_file" |
|
862 where |
|
863 "new_childf pf \<tau> = next_fname pf \<tau> # pf" |
|
864 |
|
865 definition s2ss :: "t_state \<Rightarrow> t_static_state" |
|
866 where |
|
867 "s2ss s \<equiv> {sobj. \<exists> obj. alive s obj \<and> co2sobj s obj = Some sobj}" |
|
868 |
|
869 end |
|
870 |
|
871 end |