|
77
|
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 |
(*
|
|
|
10 |
definition init_sectxt_of_file:: "t_file \<Rightarrow> security_context_t option"
|
|
|
11 |
where
|
|
|
12 |
"init_sectxt_of_file f \<equiv>
|
|
|
13 |
if (is_init_file f) then init_sectxt_of_obj (O_file f)
|
|
|
14 |
else if (is_init_dir f) then init_sectxt_of_obj (O_dir f)
|
|
|
15 |
else None"
|
|
|
16 |
*)
|
|
|
17 |
|
|
|
18 |
definition sroot :: "t_sfile"
|
|
|
19 |
where
|
|
|
20 |
"sroot \<equiv> (Init [], sec_of_root, None, {})"
|
|
|
21 |
|
|
|
22 |
definition init_cf2sfile :: "t_file \<Rightarrow> t_sfile option"
|
|
|
23 |
where
|
|
|
24 |
"init_cf2sfile f \<equiv>
|
|
|
25 |
case (parent f) of
|
|
|
26 |
None \<Rightarrow> Some sroot
|
|
|
27 |
| Some pf \<Rightarrow> if (is_init_file f) then
|
|
|
28 |
(case (init_sectxt_of_obj (O_file f), init_sectxt_of_obj (O_dir pf), get_parentfs_ctxts [] pf) of
|
|
|
29 |
(Some sec, Some psec, Some aseclist) \<Rightarrow> Some (Init f, sec, Some psec, set aseclist)
|
|
|
30 |
| _ \<Rightarrow> None) else
|
|
|
31 |
(case (init_sectxt_of_obj (O_dir f), init_sectxt_of_obj (O_dir pf), get_parentfs_ctxts [] pf) of
|
|
|
32 |
(Some sec, Some psec, Some aseclist) \<Rightarrow> Some (Init f, sec, Some psec, set aseclist)
|
|
|
33 |
| _ \<Rightarrow> None)"
|
|
|
34 |
|
|
|
35 |
definition init_cf2sfiles :: "t_file \<Rightarrow> t_sfile set"
|
|
|
36 |
where
|
|
|
37 |
"init_cf2sfiles f \<equiv> {sf. \<exists>f' \<in> init_same_inode_files f. init_cf2sfile f' = Some sf}"
|
|
|
38 |
|
|
85
|
39 |
fun remove_create_flag :: "t_open_flags \<Rightarrow> t_open_flags"
|
|
|
40 |
where
|
|
|
41 |
"remove_create_flag (mflag, oflags) = (mflag, oflags - {OF_CREAT})"
|
|
|
42 |
|
|
77
|
43 |
definition init_cfd2sfd :: "t_process \<Rightarrow> t_fd \<Rightarrow> (security_context_t \<times> t_open_flags \<times> t_sfile) option"
|
|
|
44 |
where
|
|
|
45 |
"init_cfd2sfd p fd =
|
|
|
46 |
(case (init_file_of_proc_fd p fd, init_oflags_of_proc_fd p fd, init_sectxt_of_obj (O_fd p fd)) of
|
|
|
47 |
(Some f, Some flags, Some sec) \<Rightarrow> (case (init_cf2sfile f) of
|
|
85
|
48 |
Some sf \<Rightarrow> Some (sec, remove_create_flag flags, sf)
|
|
77
|
49 |
| _ \<Rightarrow> None)
|
|
|
50 |
| _ \<Rightarrow> None)"
|
|
|
51 |
|
|
|
52 |
definition init_cfds2sfds :: "t_process \<Rightarrow> (security_context_t \<times> t_open_flags \<times> t_sfile) set"
|
|
|
53 |
where
|
|
|
54 |
"init_cfds2sfds p \<equiv> { sfd. \<exists> fd \<in> init_proc_file_fds p. init_cfd2sfd p fd = Some sfd}"
|
|
|
55 |
|
|
|
56 |
(*
|
|
|
57 |
definition init_ch2sshm :: "t_shm \<Rightarrow> t_sshm option"
|
|
|
58 |
where
|
|
|
59 |
"init_ch2sshm h \<equiv> (case (init_sectxt_of_obj (O_shm h)) of
|
|
|
60 |
Some sec \<Rightarrow> Some (Init h, sec)
|
|
|
61 |
| _ \<Rightarrow> None)"
|
|
|
62 |
|
|
|
63 |
definition init_cph2spshs
|
|
|
64 |
:: "t_process \<Rightarrow> (t_sshm \<times> t_shm_attach_flag) set"
|
|
|
65 |
where
|
|
|
66 |
"init_cph2spshs p \<equiv> {(sh, flag)| sh flag h. (p, flag) \<in> init_procs_of_shm h \<and>
|
|
|
67 |
init_ch2sshm h = Some sh}"
|
|
|
68 |
*)
|
|
|
69 |
definition init_cp2sproc :: "t_process \<Rightarrow> t_sproc option"
|
|
|
70 |
where
|
|
|
71 |
"init_cp2sproc p \<equiv> (case (init_sectxt_of_obj (O_proc p)) of
|
|
|
72 |
Some sec \<Rightarrow> Some (Init p, sec, (init_cfds2sfds p))
|
|
|
73 |
| None \<Rightarrow> None)"
|
|
|
74 |
|
|
|
75 |
(* acient files of init-file
|
|
|
76 |
definition init_o2s_afs :: "t_file \<Rightarrow> security_context_t set"
|
|
|
77 |
where
|
|
|
78 |
"init_o2s_afs f \<equiv> {sec. \<exists> f'. f' \<preceq> f \<and> init_sectxt_of_obj (O_dir f') = Some sec}" *)
|
|
|
79 |
|
|
87
|
80 |
(*
|
|
77
|
81 |
definition init_cm2smsg :: "t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsg option"
|
|
|
82 |
where
|
|
|
83 |
"init_cm2smsg q m \<equiv> (case (init_sectxt_of_obj (O_msg q m)) of
|
|
|
84 |
Some sec \<Rightarrow> Some (Init m, sec, (O_msg q m) \<in> seeds)
|
|
|
85 |
| _ \<Rightarrow> None)"
|
|
|
86 |
|
|
|
87 |
fun init_cqm2sms :: "t_msgq \<Rightarrow> t_msg list \<Rightarrow> (t_smsg list) option"
|
|
|
88 |
where
|
|
|
89 |
"init_cqm2sms q [] = Some []"
|
|
|
90 |
| "init_cqm2sms q (m#ms) =
|
|
|
91 |
(case (init_cqm2sms q ms, init_cm2smsg q m) of
|
|
|
92 |
(Some sms, Some sm) \<Rightarrow> Some (sm # sms)
|
|
|
93 |
| _ \<Rightarrow> None)"
|
|
|
94 |
|
|
|
95 |
definition init_cq2smsgq :: "t_msgq \<Rightarrow> t_smsgq option"
|
|
|
96 |
where
|
|
|
97 |
"init_cq2smsgq q \<equiv> (case (init_sectxt_of_obj (O_msgq q), init_cqm2sms q (init_msgs_of_queue q)) of
|
|
|
98 |
(Some sec, Some sms) \<Rightarrow> Some (Init q, sec, sms)
|
|
|
99 |
| _ \<Rightarrow> None)"
|
|
87
|
100 |
*)
|
|
77
|
101 |
|
|
92
|
102 |
fun init_obj2sobj :: "t_dobject \<Rightarrow> t_sobject option"
|
|
77
|
103 |
where
|
|
92
|
104 |
"init_obj2sobj (D_proc p) =
|
|
77
|
105 |
(case (init_cp2sproc p) of
|
|
|
106 |
Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> seeds))
|
|
|
107 |
| _ \<Rightarrow> None)"
|
|
92
|
108 |
| "init_obj2sobj (D_file f) =
|
|
77
|
109 |
Some (S_file (init_cf2sfiles f)
|
|
|
110 |
(\<exists> f'. f' \<in> (init_same_inode_files f) \<and> O_file f \<in> seeds))"
|
|
92
|
111 |
| "init_obj2sobj (D_dir f) =
|
|
77
|
112 |
(case (init_cf2sfile f) of
|
|
|
113 |
Some sf \<Rightarrow> Some (S_dir sf)
|
|
|
114 |
| _ \<Rightarrow> None)"
|
|
92
|
115 |
| "init_obj2sobj (D_msgq q) = None"
|
|
87
|
116 |
|
|
92
|
117 |
fun init_dalive :: "t_dobject \<Rightarrow> bool"
|
|
|
118 |
where
|
|
|
119 |
"init_dalive (D_proc p) = (p \<in> init_procs)"
|
|
|
120 |
| "init_dalive (D_file f) = (is_init_file f)"
|
|
|
121 |
| "init_dalive (D_dir f) = (is_init_dir f)"
|
|
|
122 |
| "init_dalive (D_msgq q) = False"
|
|
77
|
123 |
|
|
|
124 |
definition
|
|
92
|
125 |
"init_static_state \<equiv> {sobj. \<exists> obj. init_dalive obj \<and> init_obj2sobj obj = Some sobj}"
|
|
77
|
126 |
|
|
|
127 |
(**************** translation from dynamic to static *******************)
|
|
|
128 |
|
|
|
129 |
definition cf2sfile :: "t_state \<Rightarrow> t_file \<Rightarrow> t_sfile option"
|
|
|
130 |
where
|
|
|
131 |
"cf2sfile s f \<equiv>
|
|
|
132 |
case (parent f) of
|
|
|
133 |
None \<Rightarrow> Some sroot
|
|
|
134 |
| Some pf \<Rightarrow> if (is_file s f)
|
|
|
135 |
then (case (sectxt_of_obj s (O_file f), sectxt_of_obj s (O_dir pf), get_parentfs_ctxts s pf) of
|
|
|
136 |
(Some sec, Some psec, Some asecs) \<Rightarrow>
|
|
|
137 |
Some (if (\<not> died (O_file f) s \<and> is_init_file f) then Init f else Created, sec, Some psec, set asecs)
|
|
|
138 |
| _ \<Rightarrow> None)
|
|
|
139 |
else (case (sectxt_of_obj s (O_dir f), sectxt_of_obj s (O_dir pf), get_parentfs_ctxts s pf) of
|
|
|
140 |
(Some sec, Some psec, Some asecs) \<Rightarrow>
|
|
|
141 |
Some (if (\<not> died (O_dir f) s \<and> is_init_dir f) then Init f else Created, sec, Some psec, set asecs)
|
|
|
142 |
| _ \<Rightarrow> None)"
|
|
|
143 |
|
|
|
144 |
definition cf2sfiles :: "t_state \<Rightarrow> t_file \<Rightarrow> t_sfile set"
|
|
|
145 |
where
|
|
|
146 |
"cf2sfiles s f \<equiv> {sf. \<exists> f' \<in> (same_inode_files s f). cf2sfile s f' = Some sf}"
|
|
|
147 |
|
|
|
148 |
(* here cf2sfile is passed with True, because, process' fds are only for files not dirs *)
|
|
|
149 |
definition cfd2sfd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd \<Rightarrow> t_sfd option"
|
|
|
150 |
where
|
|
|
151 |
"cfd2sfd s p fd \<equiv>
|
|
|
152 |
(case (file_of_proc_fd s p fd, flags_of_proc_fd s p fd, sectxt_of_obj s (O_fd p fd)) of
|
|
|
153 |
(Some f, Some flags, Some sec) \<Rightarrow> (case (cf2sfile s f) of
|
|
85
|
154 |
Some sf \<Rightarrow> Some (sec, remove_create_flag flags, sf)
|
|
77
|
155 |
| _ \<Rightarrow> None)
|
|
|
156 |
| _ \<Rightarrow> None)"
|
|
|
157 |
|
|
|
158 |
|
|
|
159 |
definition cpfd2sfds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sfd set"
|
|
|
160 |
where
|
|
|
161 |
"cpfd2sfds s p \<equiv> {sfd. \<exists> fd \<in> proc_file_fds s p. cfd2sfd s p fd = Some sfd}"
|
|
|
162 |
|
|
|
163 |
(*
|
|
|
164 |
definition ch2sshm :: "t_state \<Rightarrow> t_shm \<Rightarrow> t_sshm option"
|
|
|
165 |
where
|
|
|
166 |
"ch2sshm s h \<equiv> (case (sectxt_of_obj s (O_shm h)) of
|
|
|
167 |
Some sec \<Rightarrow>
|
|
|
168 |
Some (if (\<not> died (O_shm h) s \<and> h \<in> init_shms) then Init h else Created, sec)
|
|
|
169 |
| _ \<Rightarrow> None)"
|
|
|
170 |
|
|
|
171 |
definition cph2spshs :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sproc_sshm set"
|
|
|
172 |
where
|
|
|
173 |
"cph2spshs s p \<equiv> {(sh, flag)| sh flag h. (p, flag) \<in> procs_of_shm s h \<and> ch2sshm s h = Some sh}"
|
|
|
174 |
*)
|
|
|
175 |
definition cp2sproc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sproc option"
|
|
|
176 |
where
|
|
|
177 |
"cp2sproc s p \<equiv> (case (sectxt_of_obj s (O_proc p)) of
|
|
|
178 |
Some sec \<Rightarrow>
|
|
|
179 |
Some (if (\<not> died (O_proc p) s \<and> p \<in> init_procs) then Init p else Created, sec,
|
|
|
180 |
cpfd2sfds s p)
|
|
|
181 |
| _ \<Rightarrow> None)"
|
|
|
182 |
|
|
87
|
183 |
(*
|
|
77
|
184 |
definition cm2smsg :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsg option"
|
|
|
185 |
where
|
|
|
186 |
"cm2smsg s q m \<equiv> (case (sectxt_of_obj s (O_msg q m)) of
|
|
|
187 |
Some sec \<Rightarrow>
|
|
|
188 |
Some (if (\<not> died (O_msg q m) s \<and> m \<in> set (init_msgs_of_queue q)) then Init m else Created,
|
|
|
189 |
sec, O_msg q m \<in> tainted s)
|
|
|
190 |
| _ \<Rightarrow> None)"
|
|
87
|
191 |
*)
|
|
|
192 |
|
|
|
193 |
definition cm2smsg :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsg option"
|
|
|
194 |
where
|
|
|
195 |
"cm2smsg s q m \<equiv> (case (sectxt_of_obj s (O_msg q m)) of
|
|
|
196 |
Some sec \<Rightarrow> Some (Created, sec, O_msg q m \<in> tainted s)
|
|
|
197 |
| _ \<Rightarrow> None)"
|
|
77
|
198 |
|
|
|
199 |
fun cqm2sms:: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg list \<Rightarrow> (t_smsg list) option"
|
|
|
200 |
where
|
|
|
201 |
"cqm2sms s q [] = Some []"
|
|
|
202 |
| "cqm2sms s q (m#ms) =
|
|
|
203 |
(case (cqm2sms s q ms, cm2smsg s q m) of
|
|
|
204 |
(Some sms, Some sm) \<Rightarrow> Some (sm#sms)
|
|
|
205 |
| _ \<Rightarrow> None)"
|
|
87
|
206 |
(*
|
|
77
|
207 |
definition cq2smsgq :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_smsgq option"
|
|
|
208 |
where
|
|
|
209 |
"cq2smsgq s q \<equiv> (case (sectxt_of_obj s (O_msgq q), cqm2sms s q (msgs_of_queue s q)) of
|
|
|
210 |
(Some sec, Some sms) \<Rightarrow>
|
|
|
211 |
Some (if (\<not> died (O_msgq q) s \<and> q \<in> init_msgqs) then Init q else Created,
|
|
|
212 |
sec, sms)
|
|
|
213 |
| _ \<Rightarrow> None)"
|
|
87
|
214 |
*)
|
|
|
215 |
|
|
|
216 |
definition cq2smsgq :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_smsgq option"
|
|
|
217 |
where
|
|
|
218 |
"cq2smsgq s q \<equiv> (case (sectxt_of_obj s (O_msgq q), cqm2sms s q (msgs_of_queue s q)) of
|
|
|
219 |
(Some sec, Some sms) \<Rightarrow> Some (Created, sec, sms)
|
|
|
220 |
| _ \<Rightarrow> None)"
|
|
77
|
221 |
|
|
92
|
222 |
fun co2sobj :: "t_state \<Rightarrow> t_dobject \<Rightarrow> t_sobject option"
|
|
77
|
223 |
where
|
|
92
|
224 |
"co2sobj s (D_proc p) =
|
|
77
|
225 |
(case (cp2sproc s p) of
|
|
|
226 |
Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))
|
|
|
227 |
| _ \<Rightarrow> None)"
|
|
92
|
228 |
| "co2sobj s (D_file f) =
|
|
77
|
229 |
Some (S_file (cf2sfiles s f) (O_file f \<in> tainted s))"
|
|
92
|
230 |
| "co2sobj s (D_dir f) =
|
|
77
|
231 |
(case (cf2sfile s f) of
|
|
|
232 |
Some sf \<Rightarrow> Some (S_dir sf)
|
|
|
233 |
| _ \<Rightarrow> None)"
|
|
92
|
234 |
| "co2sobj s (D_msgq q) =
|
|
77
|
235 |
(case (cq2smsgq s q) of
|
|
|
236 |
Some sq \<Rightarrow> Some (S_msgq sq)
|
|
|
237 |
| _ \<Rightarrow> None)"
|
|
|
238 |
|
|
92
|
239 |
fun dalive :: "t_state \<Rightarrow> t_dobject \<Rightarrow> bool"
|
|
|
240 |
where
|
|
|
241 |
"dalive s (D_proc p) = (p \<in> current_procs s)"
|
|
|
242 |
| "dalive s (D_file f) = (is_file s f)"
|
|
|
243 |
| "dalive s (D_dir f) = (is_dir s f)"
|
|
|
244 |
| "dalive s (D_msgq q) = (q \<in> current_msgqs s)"
|
|
77
|
245 |
|
|
|
246 |
definition s2ss :: "t_state \<Rightarrow> t_static_state"
|
|
|
247 |
where
|
|
92
|
248 |
"s2ss s \<equiv> {sobj. \<exists> obj. dalive s obj \<and> co2sobj s obj = Some sobj}"
|
|
77
|
249 |
|
|
|
250 |
|
|
|
251 |
(* ******************************************************** *)
|
|
|
252 |
|
|
|
253 |
|
|
|
254 |
fun is_init_sfile :: "t_sfile \<Rightarrow> bool"
|
|
|
255 |
where
|
|
|
256 |
"is_init_sfile (Init _, sec, psec,asec) = True"
|
|
|
257 |
| "is_init_sfile _ = False"
|
|
|
258 |
|
|
|
259 |
fun is_many_sfile :: "t_sfile \<Rightarrow> bool"
|
|
|
260 |
where
|
|
|
261 |
"is_many_sfile (Created, sec, psec, asec) = True"
|
|
|
262 |
| "is_many_sfile _ = False"
|
|
|
263 |
|
|
|
264 |
fun is_init_sproc :: "t_sproc \<Rightarrow> bool"
|
|
|
265 |
where
|
|
|
266 |
"is_init_sproc (Init p, sec, fds) = True"
|
|
|
267 |
| "is_init_sproc _ = False"
|
|
|
268 |
|
|
|
269 |
fun is_many_sproc :: "t_sproc \<Rightarrow> bool"
|
|
|
270 |
where
|
|
|
271 |
"is_many_sproc (Created, sec,fds) = True"
|
|
|
272 |
| "is_many_sproc _ = False"
|
|
|
273 |
|
|
87
|
274 |
(*
|
|
77
|
275 |
fun is_many_smsg :: "t_smsg \<Rightarrow> bool"
|
|
|
276 |
where
|
|
|
277 |
"is_many_smsg (Created,sec,tag) = True"
|
|
|
278 |
| "is_many_smsg _ = False"
|
|
87
|
279 |
*)
|
|
77
|
280 |
(* wrong def
|
|
|
281 |
fun is_many_smsgq :: "t_smsgq \<Rightarrow> bool"
|
|
|
282 |
where
|
|
|
283 |
"is_many_smsgq (Created,sec,sms) = (True \<and> (\<forall> sm \<in> (set sms). is_many_smsg sm))"
|
|
|
284 |
| "is_many_smsgq _ = False"
|
|
|
285 |
*)
|
|
87
|
286 |
(*
|
|
77
|
287 |
fun is_many_smsgq :: "t_smsgq \<Rightarrow> bool"
|
|
|
288 |
where
|
|
|
289 |
"is_many_smsgq (Created,sec,sms) = True"
|
|
|
290 |
| "is_many_smsgq _ = False"
|
|
87
|
291 |
*)
|
|
77
|
292 |
(*
|
|
|
293 |
fun is_many_sshm :: "t_sshm \<Rightarrow> bool"
|
|
|
294 |
where
|
|
|
295 |
"is_many_sshm (Created, sec) = True"
|
|
|
296 |
| "is_many_sshm _ = False"
|
|
|
297 |
*)
|
|
|
298 |
fun is_many :: "t_sobject \<Rightarrow> bool"
|
|
|
299 |
where
|
|
|
300 |
"is_many (S_proc sp tag) = is_many_sproc sp"
|
|
|
301 |
| "is_many (S_file sfs tag) = (\<forall> sf \<in> sfs. is_many_sfile sf)"
|
|
|
302 |
| "is_many (S_dir sf ) = is_many_sfile sf"
|
|
87
|
303 |
| "is_many (S_msgq sq ) = True"
|
|
77
|
304 |
(*
|
|
|
305 |
| "is_many (S_shm sh ) = is_many_sshm sh"
|
|
|
306 |
*)
|
|
|
307 |
|
|
87
|
308 |
(*
|
|
77
|
309 |
fun is_init_smsgq :: "t_smsgq \<Rightarrow> bool"
|
|
|
310 |
where
|
|
|
311 |
"is_init_smsgq (Init q,sec,sms) = True"
|
|
|
312 |
| "is_init_smsgq _ = False"
|
|
87
|
313 |
*)
|
|
77
|
314 |
(*
|
|
|
315 |
fun is_init_sshm :: "t_sshm \<Rightarrow> bool"
|
|
|
316 |
where
|
|
|
317 |
"is_init_sshm (Init h,sec) = True"
|
|
|
318 |
| "is_init_sshm _ = False"
|
|
|
319 |
*)
|
|
|
320 |
fun is_init_sobj :: "t_sobject \<Rightarrow> bool"
|
|
|
321 |
where
|
|
|
322 |
"is_init_sobj (S_proc sp tag ) = is_init_sproc sp"
|
|
|
323 |
| "is_init_sobj (S_file sfs tag) = (\<exists> sf \<in> sfs. is_init_sfile sf)"
|
|
|
324 |
| "is_init_sobj (S_dir sf ) = is_init_sfile sf"
|
|
87
|
325 |
| "is_init_sobj (S_msgq sq ) = False"
|
|
77
|
326 |
(*
|
|
|
327 |
| "is_init_sobj (S_shm sh ) = is_init_sshm sh"
|
|
|
328 |
*)
|
|
|
329 |
(*
|
|
|
330 |
fun update_ss_sp:: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state"
|
|
|
331 |
where
|
|
|
332 |
"update_ss_sp ss (S_proc sp tag) (S_proc sp' tag') =
|
|
|
333 |
(if (is_many_sproc sp) then ss \<union> {S_proc sp' tag'}
|
|
|
334 |
else (ss - {S_proc sp tag}) \<union> {S_proc sp' tag'})"
|
|
|
335 |
|
|
|
336 |
fun update_ss_sd:: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state"
|
|
|
337 |
where
|
|
|
338 |
"update_ss_sd ss (S_dir sf tag) (S_dir sf' tag') =
|
|
|
339 |
(if (is_many_sfile sf) then ss \<union> {S_dir sf' tag'}
|
|
|
340 |
else (ss - {S_dir sf tag}) \<union> {S_dir sf' tag'})"
|
|
|
341 |
*)
|
|
|
342 |
|
|
|
343 |
(*
|
|
|
344 |
fun sparent :: "t_sfile \<Rightarrow> t_sfile option"
|
|
|
345 |
where
|
|
|
346 |
"sparent (Sroot si sec) = None"
|
|
|
347 |
| "sparent (Sfile si sec spf) = Some spf"
|
|
|
348 |
|
|
|
349 |
inductive is_ancesf :: "t_sfile \<Rightarrow> t_sfile \<Rightarrow> bool"
|
|
|
350 |
where
|
|
|
351 |
"is_ancesf sf sf"
|
|
|
352 |
| "sparent sf = Some spf \<Longrightarrow> is_ancesf spf sf"
|
|
|
353 |
| "\<lbrakk>sparent sf = Some spf; is_ancesf saf spf\<rbrakk> \<Longrightarrow> is_ancesf saf sf"
|
|
|
354 |
|
|
|
355 |
definition sfile_reparent :: "t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile"
|
|
|
356 |
where
|
|
|
357 |
"sfile_reparent (Sroot)"
|
|
|
358 |
*)
|
|
|
359 |
|
|
|
360 |
(*
|
|
|
361 |
(* sfds rename aux definitions *)
|
|
|
362 |
definition sfds_rename_notrelated
|
|
|
363 |
:: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool"
|
|
|
364 |
where
|
|
|
365 |
"sfds_rename_notrelated sfds from to sfds' \<equiv>
|
|
|
366 |
(\<forall> sec flag sf. (sec,flag,sf) \<in> sfds \<and> (\<not> from \<preceq> sf) \<longrightarrow> (sec,flag,sf) \<in> sfds')"
|
|
|
367 |
|
|
|
368 |
definition sfds_rename_renamed
|
|
|
369 |
:: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool"
|
|
|
370 |
where
|
|
|
371 |
"sfds_rename_renamed sfds sf from to sfds' \<equiv>
|
|
|
372 |
(\<forall> sec flag sf'. (sec,flag,sf) \<in> sfds \<and> (sf \<preceq> sf') \<longrightarrow>
|
|
|
373 |
(sec, flag, file_after_rename sf' from to) \<in> sfds' \<and> (sec,flag,sf) \<notin> sfds')"
|
|
|
374 |
|
|
|
375 |
definition sfds_rename_remain
|
|
|
376 |
:: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool"
|
|
|
377 |
where
|
|
|
378 |
"sfds_rename_remain sfds sf from to sfds' \<equiv>
|
|
|
379 |
(\<forall> sec flag sf'. (sec,flag,sf') \<in> sfds \<and> (sf \<preceq> sf') \<longrightarrow>
|
|
|
380 |
(sec, flag, sf') \<in> sfds' \<and> (sec,flag, file_after_rename sf' from to) \<notin> sfds')"
|
|
|
381 |
|
|
|
382 |
(* for not many, choose on renamed or not *)
|
|
|
383 |
definition sfds_rename_choices
|
|
|
384 |
:: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool"
|
|
|
385 |
where
|
|
|
386 |
"sfds_rename_choices sfds sf from to sfds' \<equiv>
|
|
|
387 |
sfds_rename_remain sfds sf from to sfds' \<or> sfds_rename_renamed sfds sf from to sfds'"
|
|
|
388 |
|
|
|
389 |
(* for many, merge renamed with not renamed *)
|
|
|
390 |
definition sfds_rename_both
|
|
|
391 |
:: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool"
|
|
|
392 |
where
|
|
|
393 |
"sfds_rename_both sfds sf from to sfds' \<equiv>
|
|
|
394 |
(\<forall> sec flag sf'. (sec,flag,sf') \<in> sfds \<and> (sf \<preceq> sf') \<longrightarrow>
|
|
|
395 |
(sec, flag, sf') \<in> sfds' \<or> (sec,flag, file_after_rename sf' from to) \<in> sfds')"
|
|
|
396 |
|
|
|
397 |
(* added to the new sfds, are those only under the new sfile *)
|
|
|
398 |
definition sfds_rename_added
|
|
|
399 |
:: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool"
|
|
|
400 |
where
|
|
|
401 |
"sfds_rename_added sfds from to sfds' \<equiv>
|
|
|
402 |
(\<forall> sec' flag' sf' sec flag. (sec',flag',sf') \<in> sfds' \<and> (sec,flag,sf') \<notin> sfds \<longrightarrow>
|
|
|
403 |
(\<exists> sf. (sec,flag,sf) \<in> sfds \<and> sf' = file_after_rename from to sf))"
|
|
|
404 |
|
|
|
405 |
definition sproc_sfds_renamed
|
|
|
406 |
:: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
|
|
|
407 |
where
|
|
|
408 |
"sproc_sfds_renamed ss sf from to ss' \<equiv>
|
|
|
409 |
(\<forall> pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \<in> ss \<longrightarrow>
|
|
|
410 |
(\<exists> sfds'. S_proc (pi,sec,sfds',sshms) tagp \<in> ss \<and> sfds_rename_renamed sfds sf from to sfds'))"
|
|
|
411 |
|
|
|
412 |
definition sproc_sfds_remain
|
|
|
413 |
:: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
|
|
|
414 |
where
|
|
|
415 |
"sproc_sfds_remain ss sf from to ss' \<equiv>
|
|
|
416 |
(\<forall> pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \<in> ss \<longrightarrow>
|
|
|
417 |
(\<exists> sfds'. S_proc (pi,sec,sfds',sshms) tagp \<in> ss \<and> sfds_rename_remain sfds sf from to sfds'))"
|
|
|
418 |
|
|
|
419 |
(* for not many, choose on renamed or not *)
|
|
|
420 |
definition sproc_sfds_choices
|
|
|
421 |
:: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
|
|
|
422 |
where
|
|
|
423 |
"sproc_sfds_choices ss sf from to ss' \<equiv>
|
|
|
424 |
(\<forall> pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \<in> ss \<longrightarrow>
|
|
|
425 |
(\<exists> sfds'. S_proc (pi,sec,sfds',sshms) tagp \<in> ss \<and> sfds_rename_choices sfds sf from to sfds'))"
|
|
|
426 |
|
|
|
427 |
(* for many, merge renamed with not renamed *)
|
|
|
428 |
definition sproc_sfds_both
|
|
|
429 |
:: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
|
|
|
430 |
where
|
|
|
431 |
"sproc_sfds_both ss sf from to ss' \<equiv>
|
|
|
432 |
(\<forall> pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \<in> ss \<longrightarrow>
|
|
|
433 |
(\<exists> sfds'. S_proc (pi,sec,sfds',sshms) tagp \<in> ss \<and> sfds_rename_both sfds sf from to sfds'))"
|
|
|
434 |
|
|
|
435 |
(* remove (\<forall> sp tag. S_proc sp tag \<in> ss \<longrightarrow> S_proc sp tag \<in> ss'),
|
|
|
436 |
* cause sfds contains sfs informations *)
|
|
|
437 |
definition ss_rename_notrelated
|
|
|
438 |
:: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
|
|
|
439 |
where
|
|
|
440 |
"ss_rename_notrelated ss sf sf' ss' \<equiv>
|
|
|
441 |
(\<forall> sq. S_msgq sq \<in> ss \<longrightarrow> S_msgq sq \<in> ss') \<and>
|
|
|
442 |
(\<forall> pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \<in> ss \<longrightarrow> (\<exists> sfds'.
|
|
|
443 |
S_proc (pi,sec,sfds',sshms) tagp \<in> ss'\<and> sfds_rename_notrelated sfds sf sf' sfds')) \<and>
|
|
|
444 |
(\<forall> sfs sf'' tag. S_file sfs tag \<in> ss \<and> sf'' \<in> sfs \<and> (\<not> sf \<preceq> sf'') \<longrightarrow> (\<exists> sfs'.
|
|
|
445 |
S_file sfs tag \<in> ss' \<and> sf'' \<in> sfs')) \<and>
|
|
|
446 |
(\<forall> sf'' tag. S_dir sf'' tag \<in> ss \<and> (\<not> sf \<preceq> sf'') \<longrightarrow> S_dir sf'' tag \<in> ss')"
|
|
|
447 |
|
|
|
448 |
(* rename from to, from should definited renamed if not many *)
|
|
|
449 |
definition all_descendant_sf_renamed
|
|
|
450 |
:: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
|
|
|
451 |
where
|
|
|
452 |
"all_descendant_sf_renamed ss sf from to ss' \<equiv>
|
|
|
453 |
(\<forall> sfs sf' tagf. sf \<preceq> sf' \<and> S_file sfs tagf \<in> ss \<and> sf' \<in> sfs \<longrightarrow> (\<exists> sfs'.
|
|
|
454 |
S_file sfs' tagf \<in> ss' \<and> file_after_rename from to sf' \<in> sfs' \<and> sf' \<notin> sfs')) \<and>
|
|
|
455 |
(\<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>
|
|
|
456 |
sproc_sfds_renamed ss sf from to ss'"
|
|
|
457 |
|
|
|
458 |
(* not renamed *)
|
|
|
459 |
definition all_descendant_sf_remain
|
|
|
460 |
:: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
|
|
|
461 |
where
|
|
|
462 |
"all_descendant_sf_remain ss sf from to ss' \<equiv>
|
|
|
463 |
(\<forall> sfs sf' tag'. sf \<preceq> sf' \<and> S_file sfs tag' \<in> ss \<and> sf' \<in> sfs \<longrightarrow> (\<exists> sfs'.
|
|
|
464 |
S_file sfs' tag' \<in> ss \<and> file_after_rename from to sf' \<notin> sfs' \<and> sf' \<in> sfs')) \<and>
|
|
|
465 |
(\<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>
|
|
|
466 |
sproc_sfds_remain ss sf from to ss'"
|
|
|
467 |
|
|
|
468 |
definition all_descendant_sf_choices
|
|
|
469 |
:: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
|
|
|
470 |
where
|
|
|
471 |
"all_descendant_sf_choices ss sf from to ss' \<equiv>
|
|
|
472 |
all_descendant_sf_renamed ss sf from to ss' \<or> all_descendant_sf_remain ss sf from to ss'"
|
|
|
473 |
|
|
|
474 |
definition all_descendant_sf_both
|
|
|
475 |
:: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
|
|
|
476 |
where
|
|
|
477 |
"all_descendant_sf_both ss sf from to ss' \<equiv>
|
|
|
478 |
(\<forall> sfs sf' tag'. sf \<preceq> sf' \<and> S_file sfs tag' \<in> ss \<and> sf' \<in> sfs \<longrightarrow> (\<exists> sfs'.
|
|
|
479 |
S_file sfs' tag' \<in> ss \<and> file_after_rename from to sf' \<in> sfs' \<or> sf' \<in> sfs')) \<and>
|
|
|
480 |
(\<forall> sf' tag'. sf \<preceq> sf' \<and> S_dir sf' tag' \<in> ss \<longrightarrow>
|
|
|
481 |
S_dir (file_after_rename from to sf') tag' \<in> ss' \<or> S_dir sf' tag' \<in> ss') \<and>
|
|
|
482 |
sproc_sfds_both ss sf from to ss'"
|
|
|
483 |
|
|
|
484 |
definition ss_renamed_file
|
|
|
485 |
:: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
|
|
|
486 |
where
|
|
|
487 |
"ss_renamed_file ss sf sf' ss' \<equiv>
|
|
|
488 |
(if (is_many_sfile sf)
|
|
|
489 |
then all_descendant_sf_choices ss sf sf sf' ss'
|
|
|
490 |
else all_descendant_sf_renamed ss sf sf sf' ss')"
|
|
|
491 |
|
|
|
492 |
(* added to the new sfs, are those only under the new sfile *)
|
|
|
493 |
definition sfs_rename_added
|
|
|
494 |
:: "t_sfile set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile set \<Rightarrow> bool"
|
|
|
495 |
where
|
|
|
496 |
"sfs_rename_added sfs from to sfs' \<equiv>
|
|
|
497 |
(\<forall> sf'. sf' \<in> sfs' \<and> sf' \<notin> sfs \<longrightarrow> (\<exists> sf. sf \<in> sfs \<and> sf' = file_after_rename from to sf))"
|
|
|
498 |
|
|
|
499 |
(* added to the new sfile, are those only under the new sfile *)
|
|
|
500 |
definition ss_rename_added
|
|
|
501 |
:: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
|
|
|
502 |
where
|
|
|
503 |
"ss_rename_added ss from to ss' \<equiv>
|
|
|
504 |
(\<forall> pi sec fds fds' shms tagp. S_proc (pi, sec, fds,shms) tagp \<in> ss \<and>
|
|
|
505 |
S_proc (pi,sec,fds',shms) tagp \<in> ss' \<longrightarrow> sfds_rename_added fds from to fds') \<and>
|
|
|
506 |
(\<forall> sq. S_msgq sq \<in> ss' \<longrightarrow> S_msgq sq \<in> ss) \<and>
|
|
|
507 |
(\<forall> sfs sfs' tagf. S_file sfs' tagf \<in> ss' \<and> S_file sfs tagf \<in> ss \<longrightarrow>
|
|
|
508 |
sfs_rename_added sfs from to sfs') \<and>
|
|
|
509 |
(\<forall> sf' tagf. S_dir sf' tagf \<in> ss' \<and> S_dir sf' tagf \<notin> ss \<longrightarrow>
|
|
|
510 |
(\<exists> sf. S_dir sf tagf \<in> ss \<and> sf' = file_after_rename from to sf))"
|
|
|
511 |
|
|
|
512 |
definition sfile_alive :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> bool"
|
|
|
513 |
where
|
|
|
514 |
"sfile_alive ss sf \<equiv> (\<exists> sfs tagf. sf \<in> sfs \<and> S_file sfs tagf \<in> ss)"
|
|
|
515 |
|
|
|
516 |
definition sf_alive :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> bool"
|
|
|
517 |
where
|
|
|
518 |
"sf_alive ss sf \<equiv> (\<exists> tagd. S_dir sf tagd \<in> ss) \<or> sfile_alive ss sf"
|
|
|
519 |
|
|
|
520 |
(* constrains that the new static state should satisfy *)
|
|
|
521 |
definition ss_rename:: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
|
|
|
522 |
where
|
|
|
523 |
"ss_rename ss sf sf' ss' \<equiv>
|
|
|
524 |
ss_rename_notrelated ss sf sf' ss' \<and>
|
|
|
525 |
ss_renamed_file ss sf sf' ss' \<and> ss_rename_added ss sf sf' ss' \<and>
|
|
|
526 |
(\<forall> sf''. sf_alive ss sf'' \<and> sf \<prec> sf'' \<longrightarrow>
|
|
|
527 |
(if (is_many_sfile sf'')
|
|
|
528 |
then all_descendant_sf_choices ss sf'' sf sf' ss'
|
|
|
529 |
else all_descendant_sf_both ss sf'' sf sf' ss'))"
|
|
|
530 |
|
|
|
531 |
(* two sfile, the last fname should not be equal *)
|
|
|
532 |
fun sfile_same_fname:: "t_sfile \<Rightarrow> t_sfile \<Rightarrow> bool"
|
|
|
533 |
where
|
|
|
534 |
"sfile_same_fname ((Init n, sec)#spf) ((Init n', sec')#spf') = (n = n')"
|
|
|
535 |
| "sfile_same_fname _ _ = False"
|
|
|
536 |
|
|
|
537 |
(* no same init sfile/only sfile in the target-to spf, should be in static_state addmissble check *)
|
|
|
538 |
definition ss_rename_no_same_fname:: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> bool"
|
|
|
539 |
where
|
|
|
540 |
"ss_rename_no_same_fname ss from spf \<equiv>
|
|
|
541 |
\<not> (\<exists> to. sfile_same_fname from to \<and> parent to = Some spf \<and> sf_alive ss to)"
|
|
|
542 |
|
|
|
543 |
(* is not a function, is a relation (one 2 many)
|
|
|
544 |
definition update_ss_rename :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state"
|
|
|
545 |
where
|
|
|
546 |
"update_ss_rename ss sf sf' \<equiv> if (is_many_sfile sf)
|
|
|
547 |
then (ss \<union> {S_file (file_after_rename sf sf' sf'') tag | sf'' tag. sf \<preceq> sf'' \<and> S_file sf'' tag \<in> ss}
|
|
|
548 |
\<union> {S_dir (file_after_rename sf sf' sf'') tag | sf'' tag. sf \<preceq> sf'' \<and> S_dir sf'' tag \<in> ss})
|
|
|
549 |
else (ss - {S_file sf'' tag | sf'' tag. sf \<preceq> sf'' \<and> S_file sf'' tag \<in> ss}
|
|
|
550 |
- {S_dir sf'' tag | sf'' tag. sf \<preceq> sf'' \<and> S_dir sf'' tag \<in> ss})
|
|
|
551 |
\<union> {S_file (file_after_rename sf sf' sf'') tag | sf'' tag. sf \<preceq> sf'' \<and> S_file sf'' tag \<in> ss}
|
|
|
552 |
\<union> {S_dir (file_after_rename sf sf' sf'') tag | sf'' tag. sf \<preceq> sf'' \<and> S_dir sf'' tag \<in> ss}"
|
|
|
553 |
*)
|
|
|
554 |
*)
|
|
|
555 |
|
|
|
556 |
fun sectxt_of_sproc :: "t_sproc \<Rightarrow> security_context_t"
|
|
|
557 |
where
|
|
|
558 |
"sectxt_of_sproc (pi,sec,fds) = sec"
|
|
|
559 |
|
|
|
560 |
fun sectxt_of_sfile :: "t_sfile \<Rightarrow> security_context_t"
|
|
|
561 |
where
|
|
|
562 |
"sectxt_of_sfile (fi,sec,psec,asecs) = sec"
|
|
|
563 |
|
|
|
564 |
fun asecs_of_sfile :: "t_sfile \<Rightarrow> security_context_t set"
|
|
|
565 |
where
|
|
|
566 |
"asecs_of_sfile (fi,sec,psec,asecs) = asecs"
|
|
|
567 |
|
|
|
568 |
definition search_check_s :: "security_context_t \<Rightarrow> t_sfile \<Rightarrow> bool \<Rightarrow> bool"
|
|
|
569 |
where
|
|
|
570 |
"search_check_s pctxt sf if_file =
|
|
|
571 |
(if if_file
|
|
|
572 |
then search_check_ctxt pctxt (sectxt_of_sfile sf) (asecs_of_sfile sf) True
|
|
|
573 |
else search_check_ctxt pctxt (sectxt_of_sfile sf) (asecs_of_sfile sf) False)"
|
|
|
574 |
|
|
|
575 |
definition sectxts_of_sfds :: "t_sfd set \<Rightarrow> security_context_t set"
|
|
|
576 |
where
|
|
|
577 |
"sectxts_of_sfds sfds \<equiv> {ctxt. \<exists> flag sf. (ctxt, flag, sf) \<in> sfds}"
|
|
|
578 |
|
|
|
579 |
definition inherit_fds_check_s :: "security_context_t \<Rightarrow> t_sfd set \<Rightarrow> bool"
|
|
|
580 |
where
|
|
|
581 |
"inherit_fds_check_s pctxt sfds \<equiv> inherit_fds_check_ctxt pctxt (sectxts_of_sfds sfds)"
|
|
|
582 |
|
|
|
583 |
(*
|
|
|
584 |
definition sectxts_of_sproc_sshms :: "t_sproc_sshm set \<Rightarrow> security_context_t set"
|
|
|
585 |
where
|
|
|
586 |
"sectxts_of_sproc_sshms sshms \<equiv> {ctxt. \<exists> hi flag. ((hi, ctxt),flag) \<in> sshms}"
|
|
|
587 |
|
|
|
588 |
definition inherit_shms_check_s :: "security_context_t \<Rightarrow> t_sproc_sshm set \<Rightarrow> bool"
|
|
|
589 |
where
|
|
|
590 |
"inherit_shms_check_s pctxt sshms \<equiv> inherit_shms_check_ctxt pctxt (sectxts_of_sproc_sshms sshms)"
|
|
|
591 |
|
|
|
592 |
fun info_flow_sshm :: "t_sproc \<Rightarrow> t_sproc \<Rightarrow> bool"
|
|
|
593 |
where
|
|
|
594 |
"info_flow_sshm (pi,sec,fds,shms) (pi',sec',fds',shms') =
|
|
|
595 |
(\<exists> sh flag'. (sh, SHM_RDWR) \<in> shms \<and> (sh, flag') \<in> shms')"
|
|
|
596 |
|
|
|
597 |
definition info_flow_sproc_sshms :: "t_sproc_sshm set \<Rightarrow> t_sproc_sshm set \<Rightarrow> bool"
|
|
|
598 |
where
|
|
|
599 |
"info_flow_sproc_sshms shms shms' \<equiv> (\<exists> sh flag'. (sh, SHM_RDWR) \<in> shms \<and> (sh, flag') \<in> shms')"
|
|
|
600 |
|
|
|
601 |
|
|
|
602 |
fun info_flow_sshm :: "t_sproc \<Rightarrow> t_sproc \<Rightarrow> bool"
|
|
|
603 |
where
|
|
|
604 |
"info_flow_sshm (pi,sec,fds,shms) (pi',sec',fds',shms') = info_flow_sproc_sshms shms shms'"
|
|
|
605 |
|
|
|
606 |
inductive info_flow_sshm :: "t_sproc \<Rightarrow> t_sproc \<Rightarrow> bool"
|
|
|
607 |
where
|
|
|
608 |
"info_flow_sshm sp sp"
|
|
|
609 |
| "\<lbrakk>info_flow_sshm sp (pi,sec,fds,shms); info_flow_sproc_sshms shms shms'\<rbrakk>
|
|
|
610 |
\<Longrightarrow> info_flow_sshm sp (pi',sec',fds',shms')"
|
|
|
611 |
*)
|
|
|
612 |
|
|
|
613 |
(*
|
|
|
614 |
fun smsg_related :: "t_msg \<Rightarrow> t_smsg list \<Rightarrow> bool"
|
|
|
615 |
where
|
|
|
616 |
"smsg_related m [] = False"
|
|
|
617 |
| "smsg_related m ((mi, sec, tag)#sms) =
|
|
|
618 |
(if (mi = Init m) then True else smsg_related m sms)"
|
|
|
619 |
|
|
|
620 |
fun smsgq_smsg_related :: "t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsgq \<Rightarrow> bool"
|
|
|
621 |
where
|
|
|
622 |
"smsgq_smsg_related q m (qi, sec, smsgslist) = ((qi = Init q) \<and> (smsg_related m smsgslist))"
|
|
|
623 |
|
|
|
624 |
fun smsg_relatainted :: "t_msg \<Rightarrow> t_smsg list \<Rightarrow> bool"
|
|
|
625 |
where
|
|
|
626 |
"smsg_relatainted m [] = False"
|
|
|
627 |
| "smsg_relatainted m ((mi, sec, tag)#sms) =
|
|
|
628 |
(if (mi = Init m \<and> tag = True) then True else smsg_relatainted m sms)"
|
|
|
629 |
|
|
|
630 |
fun smsgq_smsg_relatainted :: "t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsgq \<Rightarrow> bool"
|
|
|
631 |
where
|
|
|
632 |
"smsgq_smsg_relatainted q m (qi, sec, smsgslist) =
|
|
|
633 |
((qi = Init q) \<and> (smsg_relatainted m smsgslist))"
|
|
|
634 |
*)
|
|
|
635 |
|
|
|
636 |
fun sfile_related :: "t_sfile \<Rightarrow> t_file \<Rightarrow> bool"
|
|
|
637 |
where
|
|
|
638 |
"sfile_related (fi,sec,psec,asecs) f = (fi = Init f)"
|
|
|
639 |
(*
|
|
|
640 |
fun sproc_related :: "t_process \<Rightarrow> t_sproc \<Rightarrow> bool"
|
|
|
641 |
where
|
|
|
642 |
"sproc_related p (pi, sec, fds, shms) = (pi = Init p)"
|
|
|
643 |
*)
|
|
|
644 |
fun init_obj_related :: "t_sobject \<Rightarrow> t_object \<Rightarrow> bool"
|
|
|
645 |
where
|
|
|
646 |
"init_obj_related (S_proc (pi, sec, fds) tag) (O_proc p') = (pi = Init p')"
|
|
|
647 |
| "init_obj_related (S_file sfs tag) (O_file f) = (\<exists> sf \<in> sfs. sfile_related sf f)"
|
|
|
648 |
| "init_obj_related (S_dir sf) (O_dir f) = (sfile_related sf f)"
|
|
|
649 |
(*
|
|
|
650 |
| "init_obj_related (S_shm (hi, sec)) (O_shm h') = (hi = Init h')"
|
|
|
651 |
|
|
|
652 |
| "init_obj_related (S_msg (qi, sec, sms) (mi, secm, tagm)) (O_msg q' m') = (qi = Init q' \<and> mi = Init m')"
|
|
|
653 |
*)
|
|
|
654 |
| "init_obj_related _ _ = False"
|
|
|
655 |
|
|
|
656 |
|
|
|
657 |
|
|
|
658 |
(***************** for backward proof when Instancing static objects ******************)
|
|
|
659 |
|
|
93
|
660 |
(*
|
|
77
|
661 |
fun all_procs :: "t_state \<Rightarrow> t_process set"
|
|
|
662 |
where
|
|
|
663 |
"all_procs [] = init_procs"
|
|
|
664 |
| "all_procs (Clone p p' fds # s) = insert p' (all_procs s)"
|
|
|
665 |
| "all_procs (e # s) = all_procs s"
|
|
93
|
666 |
*)
|
|
77
|
667 |
|
|
|
668 |
definition next_nat :: "nat set \<Rightarrow> nat"
|
|
|
669 |
where
|
|
|
670 |
"next_nat nset = (Max nset) + 1"
|
|
|
671 |
|
|
|
672 |
definition new_proc :: "t_state \<Rightarrow> t_process"
|
|
|
673 |
where
|
|
|
674 |
"new_proc \<tau> = next_nat (current_procs \<tau>)"
|
|
|
675 |
|
|
93
|
676 |
(*
|
|
77
|
677 |
definition brandnew_proc :: "t_state \<Rightarrow> t_process"
|
|
|
678 |
where
|
|
|
679 |
"brandnew_proc s \<equiv> next_nat (all_procs s)"
|
|
93
|
680 |
*)
|
|
|
681 |
|
|
77
|
682 |
|
|
|
683 |
definition new_inode_num :: "t_state \<Rightarrow> nat"
|
|
|
684 |
where
|
|
|
685 |
"new_inode_num \<tau> = next_nat (current_inode_nums \<tau>)"
|
|
|
686 |
|
|
|
687 |
definition new_msgq :: "t_state \<Rightarrow> t_msgq"
|
|
|
688 |
where
|
|
|
689 |
"new_msgq s = next_nat (current_msgqs s)"
|
|
|
690 |
|
|
|
691 |
definition new_msg :: "t_state \<Rightarrow> t_msgq \<Rightarrow> nat"
|
|
|
692 |
where
|
|
|
693 |
"new_msg s q = next_nat (set (msgs_of_queue s q))"
|
|
|
694 |
|
|
|
695 |
(*
|
|
|
696 |
definition new_shm :: "t_state \<Rightarrow> nat"
|
|
|
697 |
where
|
|
|
698 |
"new_shm \<tau> = next_nat (current_shms \<tau>)"
|
|
|
699 |
*)
|
|
|
700 |
|
|
|
701 |
definition new_proc_fd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd"
|
|
|
702 |
where
|
|
|
703 |
"new_proc_fd \<tau> p = next_nat (current_proc_fds \<tau> p)"
|
|
|
704 |
|
|
94
|
705 |
definition all_fname_under_dir:: "t_file \<Rightarrow> t_file set \<Rightarrow> t_fname set"
|
|
77
|
706 |
where
|
|
94
|
707 |
"all_fname_under_dir d fs = {fn. fn # d \<in> fs}"
|
|
77
|
708 |
|
|
|
709 |
fun fname_all_a:: "nat \<Rightarrow> t_fname"
|
|
|
710 |
where
|
|
|
711 |
"fname_all_a 0 = []" |
|
|
|
712 |
"fname_all_a (Suc n) = ''a''@(fname_all_a n)"
|
|
|
713 |
|
|
|
714 |
definition fname_length_set :: "t_fname set \<Rightarrow> nat set"
|
|
|
715 |
where
|
|
|
716 |
"fname_length_set fns = length`fns"
|
|
|
717 |
|
|
94
|
718 |
definition next_fname:: "t_file \<Rightarrow> t_file set \<Rightarrow> t_fname"
|
|
77
|
719 |
where
|
|
94
|
720 |
"next_fname pf fs = fname_all_a ((Max (fname_length_set (all_fname_under_dir pf fs))) + 1)"
|
|
93
|
721 |
|
|
94
|
722 |
definition new_childf_general:: "t_file \<Rightarrow> t_file set \<Rightarrow> t_file"
|
|
93
|
723 |
where
|
|
94
|
724 |
"new_childf_general pf fs = next_fname pf fs # pf"
|
|
77
|
725 |
|
|
|
726 |
definition new_childf:: "t_file \<Rightarrow> t_state \<Rightarrow> t_file"
|
|
|
727 |
where
|
|
94
|
728 |
"new_childf pf \<tau> = new_childf_general pf (current_files \<tau>)"
|
|
77
|
729 |
|
|
|
730 |
end
|
|
|
731 |
|
|
|
732 |
end |