|
1 theory Dynamic_static |
|
2 imports Main Flask Static Init_prop Valid_prop Tainted_prop Delete_prop Co2sobj_prop S2ss_prop S2ss_prop2 |
|
3 Temp |
|
4 begin |
|
5 |
|
6 context tainting_s begin |
|
7 |
|
8 fun remove_create_flag :: "t_open_flags \<Rightarrow> t_open_flags" |
|
9 where |
|
10 "remove_create_flag (mflag, oflags) = (mflag, oflags - {OF_CREAT})" |
|
11 |
|
12 fun all_procs :: "t_state \<Rightarrow> t_process set" |
|
13 where |
|
14 "all_procs [] = init_procs" |
|
15 | "all_procs (Clone p p' fds shms # s) = insert p' (all_procs s)" |
|
16 | "all_procs (e # s) = all_procs s" |
|
17 |
|
18 definition brandnew_proc :: "t_state \<Rightarrow> t_process" |
|
19 where |
|
20 "brandnew_proc s \<equiv> next_nat (all_procs s)" |
|
21 |
|
22 (* |
|
23 definition brandnew_proc :: "t_state \<Rightarrow> t_process" |
|
24 where |
|
25 "brandnew_proc s \<equiv> next_nat ({p | p s'. p \<in> current_procs s' \<and> s' \<preceq> s})" |
|
26 another approach: |
|
27 brandnew_proc = next_nat (all_procs s), |
|
28 where all_procs is a event-trace listener *) |
|
29 |
|
30 (* |
|
31 lemma brandnew_proc_prop1: |
|
32 "\<lbrakk>s' \<preceq> s; valid s\<rbrakk> \<Longrightarrow> brandnew_proc s \<notin> current_procs s'" |
|
33 apply (frule vd_preceq, simp) |
|
34 apply (simp add:brandnew_proc_def) |
|
35 apply (auto) |
|
36 sorry |
|
37 |
|
38 lemma brandnew_proc_prop2: |
|
39 "\<lbrakk>p \<in> current_procs s'; s' \<preceq> s; valid s\<rbrakk> \<Longrightarrow> brandnew_proc s \<noteq> p" |
|
40 by (auto dest:brandnew_proc_prop1) |
|
41 |
|
42 lemma brandnew_proc_prop3: |
|
43 "\<lbrakk>p \<in> current_procs s; valid (e # s)\<rbrakk> \<Longrightarrow> brandnew_proc (e # s) \<noteq> p" |
|
44 apply (rule brandnew_proc_prop2, simp) |
|
45 apply (rule no_juniorI, simp+) |
|
46 done |
|
47 *) |
|
48 |
|
49 (* enrich s target_proc duplicated_pro *) |
|
50 fun enrich_proc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> t_state" |
|
51 where |
|
52 "enrich_proc [] tp dp = []" |
|
53 | "enrich_proc (Execve p f fds # s) tp dp = ( |
|
54 if (tp = p) |
|
55 then Execve dp f (fds \<inter> proc_file_fds s p) # Execve p f fds # (enrich_proc s tp dp) |
|
56 else Execve p f fds # (enrich_proc s tp dp))" |
|
57 | "enrich_proc (Clone p p' fds shms # s) tp dp = ( |
|
58 if (tp = p') |
|
59 then Clone p dp (fds \<inter> proc_file_fds s p) shms # Clone p p' fds shms # s |
|
60 else Clone p p' fds shms # (enrich_proc s tp dp))" |
|
61 | "enrich_proc (Open p f flags fd opt # s) tp dp = ( |
|
62 if (tp = p) |
|
63 then Open dp f (remove_create_flag flags) fd opt # Open p f flags fd opt # (enrich_proc s tp dp) |
|
64 else Open p f flags fd opt # (enrich_proc s tp dp))" |
|
65 | "enrich_proc (CloseFd p fd # s) tp dp = ( |
|
66 if (tp = p) |
|
67 then CloseFd dp fd # CloseFd p fd # (enrich_proc s tp dp) |
|
68 else CloseFd p fd # (enrich_proc s tp dp))" |
|
69 | "enrich_proc (Attach p h flag # s) tp dp = ( |
|
70 if (tp = p) |
|
71 then Attach dp h flag # Attach p h flag # (enrich_proc s tp dp) |
|
72 else Attach p h flag # (enrich_proc s tp dp))" |
|
73 | "enrich_proc (Detach p h # s) tp dp = ( |
|
74 if (tp = p) |
|
75 then Detach dp h # Detach p h # (enrich_proc s tp dp) |
|
76 else Detach p h # (enrich_proc s tp dp))" |
|
77 | "enrich_proc (Kill p p' # s) tp dp = ( |
|
78 if (tp = p) then Kill p p' # s |
|
79 else Kill p p' # (enrich_proc s tp dp))" |
|
80 | "enrich_proc (Exit p # s) tp dp = ( |
|
81 if (tp = p) then Exit p # s |
|
82 else Exit p # (enrich_proc s tp dp))" |
|
83 | "enrich_proc (e # s) tp dp = e # (enrich_proc s tp dp)" |
|
84 |
|
85 definition is_created_proc:: "t_state \<Rightarrow> t_process \<Rightarrow> bool" |
|
86 where |
|
87 "is_created_proc s p \<equiv> p \<in> init_procs \<longrightarrow> deleted (O_proc p) s" |
|
88 |
|
89 lemma enrich_search_check: |
|
90 assumes grant: "search_check s (up, rp, tp) f" |
|
91 and cf2sf: "\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile s' f = cf2sfile s f" |
|
92 and vd: "valid s" and f_in: "is_file s f" and f_in': "is_file s' f" |
|
93 and sec: "sectxt_of_obj s' (O_file f) = sectxt_of_obj s (O_file f)" |
|
94 shows "search_check s' (up, rp, tp) f" |
|
95 proof (cases f) |
|
96 case Nil |
|
97 with f_in vd have "False" |
|
98 by (auto dest:root_is_dir') |
|
99 thus ?thesis by simp |
|
100 next |
|
101 case (Cons n pf) |
|
102 from vd f_in obtain sf where sf: "cf2sfile s f = Some sf" |
|
103 apply (drule_tac is_file_in_current, drule_tac current_file_has_sfile, simp) |
|
104 apply (erule exE, simp) |
|
105 done |
|
106 then obtain psfs where psfs: "get_parentfs_ctxts s pf = Some psfs" using Cons |
|
107 by (auto simp:cf2sfile_def split:option.splits if_splits) |
|
108 from sf cf2sf f_in have sf': "cf2sfile s' f = Some sf" by (auto dest:is_file_in_current) |
|
109 then obtain psfs' where psfs': "get_parentfs_ctxts s' pf = Some psfs'"using Cons |
|
110 by (auto simp:cf2sfile_def split:option.splits if_splits) |
|
111 with sf sf' psfs have psfs_eq: "set psfs' = set psfs" using Cons f_in f_in' |
|
112 apply (simp add:cf2sfile_def split:option.splits) |
|
113 apply (case_tac sf, simp) |
|
114 done |
|
115 show ?thesis using grant f_in f_in' psfs psfs' psfs_eq sec |
|
116 apply (simp add:Cons split:option.splits) |
|
117 by (case_tac a, simp) |
|
118 qed |
|
119 |
|
120 lemma proc_filefd_has_sfd: "\<lbrakk>fd \<in> proc_file_fds s p; valid s\<rbrakk> \<Longrightarrow> \<exists> sfd. cfd2sfd s p fd = Some sfd" |
|
121 apply (simp add:proc_file_fds_def) |
|
122 apply (auto dest: current_filefd_has_sfd) |
|
123 done |
|
124 |
|
125 lemma enrich_inherit_fds_check: |
|
126 assumes grant: "inherit_fds_check s (up, nr, nt) p fds" and vd: "valid s" |
|
127 and cp2sp: "\<forall> p. p \<in> current_procs s \<longrightarrow> cp2sproc s' p = cp2sproc s p" |
|
128 and p_in: "p \<in> current_procs s" and p_in': "p \<in> current_procs s'" |
|
129 and fd_in: "fds \<subseteq> proc_file_fds s p" and fd_in': "fds \<subseteq> proc_file_fds s' p" |
|
130 shows "inherit_fds_check s' (up, nr, nt) p fds" |
|
131 proof- |
|
132 have "\<And> fd. fd \<in> fds \<Longrightarrow> sectxt_of_obj s' (O_fd p fd) = sectxt_of_obj s (O_fd p fd)" |
|
133 proof- |
|
134 fix fd |
|
135 assume fd_in_fds: "fd \<in> fds" |
|
136 hence fd_in_cfds: "fd \<in> proc_file_fds s p" |
|
137 and fd_in_cfds': "fd \<in> proc_file_fds s' p" |
|
138 using fd_in fd_in' by auto |
|
139 from p_in vd obtain sp where csp: "cp2sproc s p = Some sp" |
|
140 by (drule_tac current_proc_has_sp, simp, erule_tac exE, simp) |
|
141 with cp2sp have "cpfd2sfds s p = cpfd2sfds s' p" |
|
142 apply (erule_tac x = p in allE) |
|
143 by (auto simp:cp2sproc_def split:option.splits simp:p_in) |
|
144 hence "cfd2sfd s p fd = cfd2sfd s' p fd" using fd_in_cfds fd_in_cfds' |
|
145 apply (simp add:cpfd2sfds_def) |
|
146 apply (frule proc_filefd_has_sfd, simp add:vd, erule exE) |
|
147 apply (drule_tac x = sfd in eqset_imp_iff, simp) |
|
148 (* |
|
149 thm inherit_fds_check_def |
|
150 thm sectxts_of_fds_def |
|
151 thm cpfd2sfds_def |
|
152 apply ( |
|
153 *)sorry |
|
154 show "sectxt_of_obj s' (O_fd p fd) = sectxt_of_obj s (O_fd p fd)" |
|
155 sorry |
|
156 qed |
|
157 hence "sectxts_of_fds s' p fds = sectxts_of_fds s p fds" |
|
158 by (simp add:sectxts_of_fds_def) |
|
159 thus ?thesis using grant |
|
160 by (simp add:inherit_fds_check_def) |
|
161 qed |
|
162 |
|
163 |
|
164 lemma enrich_proc_aux1: |
|
165 assumes vs': "valid s'" |
|
166 and os: "os_grant s e" and grant: "grant s e" and vd: "valid s" |
|
167 and alive: "\<forall> obj. alive s obj \<longrightarrow> alive s' obj" |
|
168 and cp2sp: "\<forall> p. p \<in> current_procs s \<longrightarrow> cp2sproc s' p = cp2sproc s p" |
|
169 and cf2sf: "\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile s' f = cf2sfile s f" |
|
170 shows "valid (e # s')" |
|
171 |
|
172 sorry (* |
|
173 proof (cases e) |
|
174 case (Execve p f fds) |
|
175 have p_in: "p \<in> current_procs s'" using os alive |
|
176 apply (erule_tac x = "O_proc p" in allE) |
|
177 by (auto simp:Execve) |
|
178 have f_in: "is_file s' f" using os alive |
|
179 apply (erule_tac x = "O_file f" in allE) |
|
180 by (auto simp:Execve) |
|
181 have fd_in: "fds \<subseteq> current_proc_fds s' p" using os alive |
|
182 apply (auto simp:Execve) |
|
183 by (erule_tac x = "O_fd p x" in allE, auto) |
|
184 have "os_grant s' e" using p_in f_in fd_in by (simp add:Execve) |
|
185 moreover have "grant s' e" apply (simp add:Execve) |
|
186 proof- |
|
187 from grant obtain up rp tp uf rf tf |
|
188 where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" |
|
189 and p2: "sectxt_of_obj s (O_file f) = Some (uf, rf, tf)" |
|
190 by (simp add:Execve split:option.splits, blast) |
|
191 with grant obtain pu nr nt where p3: "npctxt_execve (up, rp, tp) (uf, rf, tf) = Some (pu, nr, nt)" |
|
192 by (simp add:Execve split:option.splits del:npctxt_execve.simps, blast) |
|
193 from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)" |
|
194 using os cp2sp |
|
195 apply (erule_tac x = p in allE) |
|
196 by (auto simp:Execve co2sobj.simps cp2sproc_def split:option.splits) |
|
197 from os have f_in': "is_file s f" by (simp add:Execve) |
|
198 from vd os have "\<exists> sf. cf2sfile s f = Some sf" |
|
199 by (auto dest!:is_file_in_current current_file_has_sfile simp:Execve) |
|
200 hence p2': "sectxt_of_obj s' (O_file f) = Some (uf, rf, tf)" using f_in f_in' p2 cf2sf |
|
201 apply (erule_tac x = f in allE) |
|
202 apply (auto dest:is_file_in_current simp:cf2sfile_def split:option.splits) |
|
203 apply (case_tac f, simp) |
|
204 apply (drule_tac s = s in root_is_dir', simp add:vd, simp+) |
|
205 done |
|
206 show ? |
|
207 proof- |
|
208 have |
|
209 |
|
210 |
|
211 *) |
|
212 |
|
213 lemma enrich_proc_prop: |
|
214 "\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s\<rbrakk> |
|
215 \<Longrightarrow> valid (enrich_proc s p p') \<and> |
|
216 (p \<in> current_procs s \<longrightarrow> co2sobj (enrich_proc s p p') (O_proc p') = co2sobj (enrich_proc s p p') (O_proc p)) \<and> |
|
217 (\<forall> obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj) \<and> |
|
218 (\<forall> p'. p' \<in> current_procs s \<longrightarrow> cp2sproc (enrich_proc s p p') p' = cp2sproc s p) \<and> |
|
219 (\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f) \<and> |
|
220 (Tainted (enrich_proc s p p') = (Tainted s \<union> (if (O_proc p \<in> Tainted s) then {O_proc p'} else {})))" |
|
221 sorry (* |
|
222 proof (induct s) |
|
223 case Nil |
|
224 thus ?case by (auto simp:is_created_proc_def) |
|
225 next |
|
226 case (Cons e s) |
|
227 hence p1: "\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s\<rbrakk> |
|
228 \<Longrightarrow> valid (enrich_proc s p p') \<and> |
|
229 (p \<in> current_procs s \<longrightarrow> co2sobj (enrich_proc s p p') (O_proc p') = co2sobj (enrich_proc s p p') (O_proc p)) \<and> |
|
230 (alive s obj \<longrightarrow> alive (enrich_proc s p p') obj \<and> co2sobj (enrich_proc s p p') obj = co2sobj s obj)" |
|
231 and p2: "valid (e # s)" and p3: "is_created_proc (e # s) p" and p4: "p' \<notin> all_procs (e # s)" |
|
232 by auto |
|
233 from p2 have vd: "valid s" and os: "os_grant s e" and grant: "grant s e" |
|
234 by (auto dest:vd_cons vt_grant vt_grant_os) |
|
235 from p4 have p4': "p' \<notin> all_procs s" by (case_tac e, auto) |
|
236 from p1 p4' have a1: "is_created_proc s p \<Longrightarrow> valid (enrich_proc s p p')" by (auto simp:vd) |
|
237 have c1: "valid (enrich_proc (e # s) p p')" |
|
238 apply (case_tac e) |
|
239 using a1 os p3 |
|
240 apply (auto simp:is_created_proc_def) |
|
241 sorry |
|
242 moreover have c2: "p' \<in> current_procs (enrich_proc (e # s) p p')" |
|
243 sorry |
|
244 moreover have c3: "co2sobj (enrich_proc (e # s) p p') (O_proc p') = co2sobj (enrich_proc (e # s) p p') (O_proc p)" |
|
245 sorry |
|
246 moreover have c4: "alive (e # s) obj \<longrightarrow> |
|
247 alive (enrich_proc (e # s) p p') obj \<and> co2sobj (enrich_proc (e # s) p p') obj = co2sobj (e # s) obj" |
|
248 sorry |
|
249 ultimately show ?case by auto |
|
250 qed |
|
251 *) |
|
252 |
|
253 |
|
254 lemma "alive s obj \<Longrightarrow> alive (enrich_proc s p p') obj" |
|
255 apply (induct s, simp) |
|
256 apply (case_tac a, case_tac[!] obj) sorry (* |
|
257 apply (auto simp:is_file_def is_dir_def split:option.splits t_inode_tag.splits) |
|
258 thm is_file_other |
|
259 *) |
|
260 lemma enrich_proc_valid: |
|
261 "\<lbrakk>p \<in> current_procs s; valid s; p \<in> init_procs \<longrightarrow> deleted (O_proc p) s; p' \<notin> current_procs s\<rbrakk> \<Longrightarrow> valid (enrich_proc s p p')" (* |
|
262 apply (induct s, simp) |
|
263 apply (frule vd_cons, frule vt_grant, frule vt_grant_os, case_tac a) |
|
264 apply (auto intro!:valid.intros(2)) |
|
265 prefer 28 |
|
266 |
|
267 |
|
268 |
|
269 end |
|
270 *) |
|
271 sorry |
|
272 |
|
273 |
|
274 (* for any created obj, we can enrich trace with events that create new objs with the same static-properties *) |
|
275 definition enriched:: "t_state \<Rightarrow> t_object set \<Rightarrow> t_state \<Rightarrow> bool" |
|
276 where |
|
277 "enriched s objs s' \<equiv> \<forall> obj \<in> objs. \<exists> obj'. \<not> alive s obj' \<and> obj' \<notin> objs \<and> |
|
278 alive s' obj' \<and> co2sobj s' obj' = co2sobj s' obj" |
|
279 |
|
280 definition reserved:: "t_state \<Rightarrow> t_object set \<Rightarrow> t_state \<Rightarrow> bool" |
|
281 where |
|
282 "reserved s objs s' \<equiv> \<forall> obj. alive s obj \<longrightarrow> alive s' obj \<and> co2sobj s' obj = co2sobj s obj" |
|
283 |
|
284 definition enrichable :: "t_state \<Rightarrow> t_object set \<Rightarrow> bool" |
|
285 where |
|
286 "enrichable s objs \<equiv> \<exists> s'. valid s' \<and> s2ss s' = s2ss s \<and> enriched s objs s' \<and> reserved s objs s'" |
|
287 |
|
288 fun is_created :: "t_state \<Rightarrow> t_object \<Rightarrow> bool" |
|
289 where |
|
290 "is_created s (O_file f) = (\<forall> f' \<in> same_inode_files s f. init_alive (O_file f') \<longrightarrow> deleted (O_file f') s)" |
|
291 | "is_created s obj = (init_alive obj \<longrightarrow> deleted obj s)" |
|
292 |
|
293 definition is_inited :: "t_state \<Rightarrow> t_object \<Rightarrow> bool" |
|
294 where |
|
295 "is_inited s obj \<equiv> init_alive obj \<and> \<not> deleted obj s" |
|
296 |
|
297 (* |
|
298 lemma is_inited_eq_not_created: |
|
299 "is_inited s obj = (\<not> is_created s obj)" |
|
300 by (auto simp:is_created_def is_inited_def) |
|
301 *) |
|
302 |
|
303 lemma many_sq_imp_sms: |
|
304 "\<lbrakk>S_msgq (Create, sec, sms) \<in> ss; ss \<in> static\<rbrakk> \<Longrightarrow> \<forall> sm \<in> (set sms). is_many_smsg sm" |
|
305 sorry |
|
306 |
|
307 (* recorded in our static world *) |
|
308 fun recorded :: "t_object \<Rightarrow> bool" |
|
309 where |
|
310 "recorded (O_proc p) = True" |
|
311 | "recorded (O_file f) = True" |
|
312 | "recorded (O_dir f) = True" |
|
313 | "recorded (O_node n) = False" (* cause socket is temperary not considered *) |
|
314 | "recorded (O_shm h) = True" |
|
315 | "recorded (O_msgq q) = True" |
|
316 | "recorded _ = False" |
|
317 |
|
318 lemma cf2sfile_fi_init_file: |
|
319 "\<lbrakk>cf2sfile s f = Some (Init f', sec, psec, asecs); is_file s f; valid s\<rbrakk> |
|
320 \<Longrightarrow> is_init_file f \<and> \<not> deleted (O_file f) s" |
|
321 apply (simp add:cf2sfile_def sroot_def split:option.splits if_splits) |
|
322 apply (case_tac f, simp, drule root_is_dir', simp+) |
|
323 done |
|
324 |
|
325 lemma root_not_deleted: |
|
326 "valid s \<Longrightarrow> \<not> deleted (O_dir []) s" |
|
327 apply (induct s, simp) |
|
328 apply (frule vd_cons, frule vt_grant_os, case_tac a) |
|
329 by auto |
|
330 |
|
331 lemma cf2sfile_fi_init_dir: |
|
332 "\<lbrakk>cf2sfile s f = Some (Init f', sec, psec, asecs); is_dir s f; valid s\<rbrakk> |
|
333 \<Longrightarrow> is_init_dir f \<and> \<not> deleted (O_dir f) s" |
|
334 apply (simp add:cf2sfile_def sroot_def split:option.splits if_splits) |
|
335 apply (case_tac f, simp add:root_is_init_dir root_not_deleted, simp) |
|
336 apply (drule file_dir_conflict, simp+) |
|
337 done |
|
338 |
|
339 lemma is_created_imp_many: |
|
340 "\<lbrakk>is_created s obj; co2sobj s obj = Some sobj; alive s obj; valid s\<rbrakk> \<Longrightarrow> is_many sobj" |
|
341 apply (case_tac obj, auto simp:co2sobj.simps split:option.splits) |
|
342 apply (case_tac [!] a) |
|
343 apply (auto simp:cp2sproc_def ch2sshm_def cq2smsgq_def cf2sfiles_def same_inode_files_def |
|
344 split:option.splits if_splits) |
|
345 apply (frule cf2sfile_fi_init_file, simp add:is_file_def, simp) |
|
346 apply (erule_tac x = f' in allE, simp) |
|
347 apply (frule cf2sfile_fi_init_dir, simp+)+ |
|
348 done |
|
349 |
|
350 lemma anotherp_imp_manysp: |
|
351 "\<lbrakk>cp2sproc s p = Some sp; co2sobj s (O_proc p') = co2sobj s (O_proc p); p' \<noteq> p; |
|
352 p' \<in> current_procs s; p \<in> current_procs s\<rbrakk> |
|
353 \<Longrightarrow> is_many_sproc sp" |
|
354 by (case_tac sp, auto simp:cp2sproc_def co2sobj.simps split:option.splits if_splits) |
|
355 |
|
356 lemma is_file_has_sfs: |
|
357 "\<lbrakk>is_file s f; valid s; cf2sfile s f = Some sf\<rbrakk> |
|
358 \<Longrightarrow> \<exists> sfs. co2sobj s (O_file f) = Some (S_file sfs (O_file f \<in> Tainted s)) \<and> sf \<in> sfs" |
|
359 apply (rule_tac x = "{sf' | f' sf'. cf2sfile s f' = Some sf' \<and> f' \<in> same_inode_files s f}" in exI) |
|
360 apply (auto simp:co2sobj.simps cf2sfiles_def tainted_eq_Tainted) |
|
361 apply (rule_tac x = f in exI, simp add:same_inode_files_prop9) |
|
362 done |
|
363 |
|
364 declare Product_Type.split_paired_Ex Product_Type.split_paired_All [simp del] |
|
365 |
|
366 lemma current_proc_in_s2ss: |
|
367 "\<lbrakk>cp2sproc s p = Some sp; p \<in> current_procs s; valid s\<rbrakk> |
|
368 \<Longrightarrow> S_proc sp (O_proc p \<in> Tainted s) \<in> s2ss s" |
|
369 apply (simp add:s2ss_def, rule_tac x = "O_proc p" in exI) |
|
370 apply (auto simp:co2sobj.simps tainted_eq_Tainted) |
|
371 done |
|
372 |
|
373 lemma current_file_in_s2ss: |
|
374 "\<lbrakk>co2sobj s (O_file f) = Some (S_file sfs tagf); is_file s f; valid s\<rbrakk> |
|
375 \<Longrightarrow> S_file sfs tagf \<in> s2ss s" |
|
376 by (simp add:s2ss_def, rule_tac x = "O_file f" in exI, simp) |
|
377 |
|
378 declare npctxt_execve.simps grant_execve.simps search_check.simps [simp del] |
|
379 |
|
380 |
|
381 lemma npctxt_execve_eq_sec: |
|
382 "\<lbrakk>sectxt_of_obj (Execve p f fds # s) (O_proc p) = Some sec'; sectxt_of_obj s (O_proc p) = Some sec; |
|
383 sectxt_of_obj s (O_file f) = Some fsec; valid (Execve p f fds # s)\<rbrakk> |
|
384 \<Longrightarrow> npctxt_execve sec fsec = Some sec'" |
|
385 by (case_tac sec, case_tac fsec, auto simp:npctxt_execve.simps sectxt_of_obj_simps split:option.splits) |
|
386 |
|
387 lemma npctxt_execve_eq_cp2sproc: |
|
388 "\<lbrakk>cp2sproc (Execve p f fds # s) p = Some (pi', sec', sfds', shms'); valid (Execve p f fds # s); |
|
389 cp2sproc s p = Some (pi, sec, sfds, shms); cf2sfile s f = Some (fi, fsec, psec, asecs)\<rbrakk> |
|
390 \<Longrightarrow> npctxt_execve sec fsec = Some sec'" |
|
391 apply (frule vt_grant_os, frule vd_cons) |
|
392 apply (rule npctxt_execve_eq_sec, auto simp:cp2sproc_def cf2sfile_def split:option.splits) |
|
393 apply (case_tac f, auto dest:root_is_dir') |
|
394 done |
|
395 |
|
396 lemma seach_check_eq_static: |
|
397 "\<lbrakk>cf2sfile s f = Some sf; valid s; is_dir s f \<or> is_file s f\<rbrakk> |
|
398 \<Longrightarrow> search_check_s sec sf (is_file s f) = search_check s sec f" |
|
399 apply (case_tac sf) |
|
400 apply (induct f) |
|
401 apply (auto simp:search_check_s_def search_check.simps cf2sfile_def sroot_def |
|
402 root_sec_remains init_sectxt_prop sec_of_root_valid |
|
403 dest!:root_is_dir' current_has_sec' split:option.splits) |
|
404 done |
|
405 |
|
406 lemma grant_execve_intro_execve: |
|
407 "\<lbrakk>cp2sproc (Execve p f fds # s) p = Some (pi', sec', sfds', shms'); valid (Execve p f fds # s); |
|
408 cp2sproc s p = Some (pi, sec, sfds, shms); cf2sfile s f = Some (fi, fsec, psec, asecs)\<rbrakk> |
|
409 \<Longrightarrow> grant_execve sec fsec sec'" |
|
410 apply (frule vt_grant_os, frule vd_cons, frule vt_grant) |
|
411 apply (auto split:option.splits dest!:current_has_sec' simp del:grant_execve.simps simp add:cp2sproc_execve) |
|
412 apply (erule_tac x = aba in allE, erule_tac x = aca in allE, erule_tac x = bb in allE) |
|
413 apply (auto simp del:grant_execve.simps simp add:cp2sproc_def cf2sfile_def split:option.splits) |
|
414 apply (case_tac f, simp, drule root_is_dir', simp, simp, simp) |
|
415 apply (simp add:sectxt_of_obj_simps) |
|
416 done |
|
417 |
|
418 lemma search_check_intro_execve: |
|
419 "\<lbrakk>cp2sproc s p = Some (pi, sec, sfds, shms); valid (Execve p f fds # s)\<rbrakk> |
|
420 \<Longrightarrow> search_check s sec f" |
|
421 apply (frule vt_grant_os, frule vd_cons, frule vt_grant) |
|
422 apply (auto split:option.splits dest!:current_has_sec' simp del:grant_execve.simps simp add:cp2sproc_execve) |
|
423 apply (erule_tac x = aaa in allE, erule_tac x = ab in allE, erule_tac x = ba in allE) |
|
424 apply (auto simp add:cp2sproc_def cf2sfile_def split:option.splits) |
|
425 done |
|
426 |
|
427 lemma inherit_fds_check_intro_execve: |
|
428 "\<lbrakk>cp2sproc (Execve p f fds # s) p = Some (pi', sec', sfds', shms'); valid (Execve p f fds # s)\<rbrakk> |
|
429 \<Longrightarrow> inherit_fds_check s sec' p fds" |
|
430 apply (frule vt_grant_os, frule vd_cons, frule vt_grant) |
|
431 apply (auto split:option.splits dest!:current_has_sec' simp add:cp2sproc_execve) |
|
432 apply (erule_tac x = aba in allE, erule_tac x = aca in allE, erule_tac x = bb in allE) |
|
433 apply (auto simp add:cp2sproc_def cf2sfile_def split:option.splits) |
|
434 apply (simp add:sectxt_of_obj_simps) |
|
435 done |
|
436 |
|
437 lemma execve_sfds_subset: |
|
438 "\<lbrakk>cp2sproc (Execve p f fds # s) p = Some (pi', sec', sfds', shms'); valid (Execve p f fds # s); |
|
439 cp2sproc s p = Some (pi, sec, sfds, shms)\<rbrakk> |
|
440 \<Longrightarrow> sfds' \<subseteq> sfds" |
|
441 apply (frule vt_grant_os) |
|
442 apply (auto simp:cp2sproc_def cpfd2sfds_execve split:option.splits dest!:current_has_sec') |
|
443 apply (simp add:cpfd2sfds_def) |
|
444 apply (rule_tac x = fd in bexI, auto simp:proc_file_fds_def) |
|
445 done |
|
446 |
|
447 lemma inherit_fds_check_imp_static: |
|
448 "\<lbrakk>cp2sproc (Execve p f fds # s) p = Some (pi', sec', sfds', shms'); |
|
449 inherit_fds_check s sec' p fds; valid (Execve p f fds # s)\<rbrakk> |
|
450 \<Longrightarrow> inherit_fds_check_s sec' sfds'" |
|
451 apply (frule vt_grant_os, frule vd_cons, frule vt_grant) |
|
452 apply (auto simp:cp2sproc_def cpfd2sfds_execve inherit_fds_check_def inherit_fds_check_s_def split:option.splits) |
|
453 sorry (* |
|
454 apply (erule_tac x = "(ad, ae, bc)" in ballE, auto simp:sectxts_of_sfds_def sectxts_of_fds_def) |
|
455 apply (erule_tac x = fd in ballE, auto simp:cfd2sfd_def split:option.splits) |
|
456 done *) |
|
457 |
|
458 lemma d2s_main_execve_grant_aux: |
|
459 "\<lbrakk>cp2sproc (Execve p f fds # s) p = Some (pi', sec', sfds', shms'); valid (Execve p f fds # s); |
|
460 cp2sproc s p = Some (pi, sec, sfds, shms); cf2sfile s f = Some (fi, fsec, psec, asecs)\<rbrakk> |
|
461 \<Longrightarrow> (npctxt_execve sec fsec = Some sec') \<and> grant_execve sec fsec sec' \<and> |
|
462 search_check_s sec (fi, fsec, psec, asecs) (is_file s f) \<and> |
|
463 inherit_fds_check_s sec' sfds' \<and> sfds' \<subseteq> sfds" |
|
464 apply (rule conjI, erule_tac pi = pi and sec = sec and sfds = sfds and |
|
465 shms = shms and fi = fi and fsec = fsec and psec = psec and |
|
466 asecs = asecs in npctxt_execve_eq_cp2sproc, simp, simp, simp) |
|
467 apply (rule conjI, erule_tac pi = pi and sec = sec and sfds = sfds and |
|
468 shms = shms and fi = fi and fsec = fsec and psec = psec and |
|
469 asecs = asecs in grant_execve_intro_execve, simp, simp, simp) |
|
470 apply (rule conjI, drule_tac sec = sec in search_check_intro_execve, simp) |
|
471 apply (frule vd_cons, frule vt_grant_os) |
|
472 apply (drule_tac sec = sec in seach_check_eq_static, simp, simp, simp) |
|
473 apply (rule conjI, rule inherit_fds_check_imp_static, simp) |
|
474 apply (erule inherit_fds_check_intro_execve, simp, simp) |
|
475 apply (erule_tac pi = pi and sfds = sfds and shms = shms in execve_sfds_subset, simp+) |
|
476 done |
|
477 |
|
478 lemma d2s_main_execve: |
|
479 "\<lbrakk>valid (Execve p f fds # s); s2ss s \<propto> static\<rbrakk> \<Longrightarrow> s2ss (Execve p f fds # s) \<propto> static" |
|
480 apply (frule vd_cons, frule vt_grant_os, clarsimp) |
|
481 apply (frule is_file_has_sfile', simp, erule exE, frule is_file_has_sfs, simp+, erule exE, erule conjE) |
|
482 apply (auto simp:s2ss_execve split:if_splits option.splits dest:current_proc_has_sp') |
|
483 apply (clarsimp simp add:init_ss_in_def init_ss_eq_def) |
|
484 apply (rule_tac x = "update_ss ss' (S_proc (ah, (ai, aj, bd), ak, be) (O_proc p \<in> Tainted s)) |
|
485 (S_proc (ad, (ae, af, bb), ag, bc) (O_proc p \<in> Tainted s \<or> O_file f \<in> Tainted s))" in bexI) |
|
486 apply (auto simp:update_ss_def elim:Set.subset_insertI2 simp:anotherp_imp_manysp)[1] |
|
487 apply (case_tac "ah = ad", case_tac "bc = {}", simp) |
|
488 apply (erule_tac sfs = sfs and fi = a and fsec = "(aa, ab,b)" and pfsec = ac and asecs = ba in s_execve, |
|
489 auto intro:current_proc_in_s2ss current_file_in_s2ss split:option.splits dest:d2s_main_execve_grant_aux)[1] |
|
490 apply (simp add:cp2sproc_execve split:option.splits) |
|
491 apply (simp add:cp2sproc_def split:option.splits if_splits) |
|
492 |
|
493 apply (clarsimp simp add:init_ss_in_def init_ss_eq_def) |
|
494 apply (rule_tac x = "update_ss ss' (S_proc (ah, (ai, aj, bd), ak, be) (O_proc p \<in> Tainted s)) |
|
495 (S_proc (ad, (ae, af, bb), ag, bc) (O_proc p \<in> Tainted s \<or> O_file f \<in> Tainted s))" in bexI) |
|
496 apply (rule conjI, simp add:update_ss_def) |
|
497 apply (rule conjI, simp add:update_ss_def) |
|
498 apply (auto)[1] |
|
499 apply (simp add:update_ss_def) |
|
500 apply (rule conjI, rule impI) |
|
501 apply (rule subsetI, clarsimp) |
|
502 apply (erule impE) |
|
503 apply (erule set_mp, simp) |
|
504 apply (case_tac ah, simp+) |
|
505 apply (rule impI, rule subsetI, clarsimp) |
|
506 apply (erule set_mp, simp) |
|
507 |
|
508 apply (case_tac "ah = ad", case_tac "bc = {}", simp) |
|
509 apply (erule_tac sfs = sfs and fi = a and fsec = "(aa, ab,b)" and pfsec = ac and asecs = ba in s_execve, |
|
510 auto intro:current_proc_in_s2ss current_file_in_s2ss split:option.splits dest:d2s_main_execve_grant_aux)[1] |
|
511 apply (simp add:cp2sproc_execve split:option.splits) |
|
512 apply (simp add:cp2sproc_def split:option.splits if_splits) |
|
513 done |
|
514 |
|
515 lemma co2sobj_eq_alive_proc_imp: |
|
516 "\<lbrakk>co2sobj s obj = co2sobj s (O_proc p); alive s (O_proc p); valid s\<rbrakk> |
|
517 \<Longrightarrow> \<exists> p'. obj = O_proc p'" |
|
518 by (auto simp add:co2sobj.simps split:option.splits dest:current_proc_has_sp' intro:co2sobj_sproc_imp) |
|
519 |
|
520 |
|
521 lemma enrichable_execve: |
|
522 assumes p1: "\<And> objs. \<forall> obj \<in> objs. alive s obj \<and> is_created s obj \<and> recorded obj |
|
523 \<Longrightarrow> \<exists> s'. valid s' \<and> s2ss s' = s2ss s \<and> enriched s objs s' \<and> reserved s objs s'" |
|
524 and p2: "valid (e # s)" and p3: "\<forall>obj\<in>objs. alive (e # s) obj \<and> is_created (e # s) obj \<and> recorded obj" |
|
525 and p4: "e = Execve p f fds" |
|
526 shows "enrichable (e # s) objs" |
|
527 proof- |
|
528 from p2 have os: "os_grant s e" and se: "grant s e" and vd: "valid s" |
|
529 by (auto dest:vt_grant_os vd_cons vt_grant) |
|
530 from p3 have recorded: "\<forall> obj \<in> objs. recorded obj" by auto |
|
531 from p3 p4 p2 have p1': "\<forall> obj \<in> objs. alive s obj \<and> is_created s obj" |
|
532 apply clarify |
|
533 apply (erule_tac x = obj in ballE, simp add:alive_simps) |
|
534 apply (case_tac obj, auto simp:same_inode_files_simps) |
|
535 done |
|
536 then obtain s' where a1: "valid s'" and a2: "s2ss s' = s2ss s" and a3: "enriched s objs s'" |
|
537 and a4: "reserved s objs s'" |
|
538 using p1 recorded by metis |
|
539 show ?thesis |
|
540 proof (cases "O_proc p \<in> objs") |
|
541 case True |
|
542 hence p_in: "p \<in> current_procs s'" using a4 os p4 |
|
543 by (auto simp:reserved_def elim:allE[where x = "O_proc p"]) |
|
544 with a1 a3 True obtain p' where b1: "\<not> alive s (O_proc p')" and b2: "O_proc p' \<notin> objs" |
|
545 and b3: "alive s' (O_proc p')" and b4: "co2sobj s' (O_proc p') = co2sobj s' (O_proc p)" |
|
546 apply (simp only:enriched_def) |
|
547 apply (erule_tac x = "O_proc p" in ballE) |
|
548 apply (erule exE|erule conjE)+ |
|
549 apply (frule co2sobj_eq_alive_proc_imp, auto) |
|
550 done |
|
551 have "valid (Execve p' f fds # e # s')" |
|
552 sorry |
|
553 moreover have "s2ss (Execve p' f fds # e # s') = s2ss (e # s)" |
|
554 sorry |
|
555 moreover have "enriched (e # s) objs (Execve p' f fds # e # s')" |
|
556 sorry |
|
557 moreover have "reserved (e # s) objs (Execve p' f fds # e # s')" |
|
558 sorry |
|
559 ultimately show ?thesis |
|
560 apply (simp add:enrichable_def) |
|
561 apply (rule_tac x = "Execve p' f fds # e # s'" in exI) |
|
562 by auto |
|
563 next |
|
564 case False |
|
565 from a4 os p4 have "p \<in> current_procs s'" |
|
566 apply (simp add:reserved_def) |
|
567 by (erule_tac x = "O_proc p" in allE, auto) |
|
568 moreover from a4 os p4 have "is_file s' f" |
|
569 apply (simp add:reserved_def) |
|
570 by (erule_tac x = "O_file f" in allE, auto) |
|
571 moreover from a4 os p4 vd have "fds \<subseteq> proc_file_fds s' p" |
|
572 apply (rule_tac subsetI, clarsimp simp:reserved_def current_proc_fds.simps) |
|
573 apply (erule_tac x = "O_fd p x" in allE, erule impE) |
|
574 sorry |
|
575 ultimately have "os_grant s' e" |
|
576 by (simp add:p4) |
|
577 moreover have "grant s' e" |
|
578 sorry |
|
579 ultimately have "valid (e # s')" |
|
580 using a1 by (erule_tac valid.intros(2), simp+) |
|
581 thus ?thesis |
|
582 apply (simp add:enrichable_def) |
|
583 apply (rule_tac x = "e # s'" in exI) |
|
584 apply (simp) |
|
585 sorry |
|
586 qed |
|
587 qed |
|
588 |
|
589 lemma s2d_main_execve: |
|
590 "\<lbrakk>grant_execve pctxt fsec pctxt'; ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; S_file sfs tagf \<in> ss; |
|
591 (fi, fsec, pfsec, asecs) \<in> sfs; npctxt_execve pctxt fsec = Some pctxt'; |
|
592 search_check_s pctxt (fi, fsec, pfsec, asecs) True; inherit_fds_check_s pctxt' fds'; fds' \<subseteq> fds; valid s; |
|
593 s2ss s = ss\<rbrakk> \<Longrightarrow> \<exists>s. valid s \<and> |
|
594 s2ss s = update_ss ss (S_proc (pi, pctxt, fds, shms) tagp) (S_proc (pi, pctxt', fds', {}) (tagp \<or> tagf))" |
|
595 apply (simp add:update_ss_def) |
|
596 thm update_ss_def |
|
597 sorry |
|
598 |
|
599 (* |
|
600 lemma s2d_main_execve: |
|
601 "ss \<in> static \<Longrightarrow> \<exists> s. valid s \<and> s2ss s = ss" |
|
602 apply (erule static.induct) |
|
603 apply (rule_tac x = "[]" in exI, simp add:s2ss_nil_prop valid.intros) |
|
604 apply (erule exE|erule conjE)+ |
|
605 apply (rule s2d_main_execve, simp+) |
|
606 |
|
607 apply (erule exE|erule conjE)+ |
|
608 |
|
609 |
|
610 sorry |
|
611 *) |
|
612 |
|
613 |
|
614 (*********************** uppest-level 3 theorems ***********************) |
|
615 |
|
616 lemma enrichability: |
|
617 "\<lbrakk>valid s; \<forall> obj \<in> objs. alive s obj \<and> is_created s obj \<and> recorded obj\<rbrakk> |
|
618 \<Longrightarrow> enrichable s objs" sorry (* |
|
619 proof (induct s arbitrary:objs) |
|
620 case Nil |
|
621 hence "objs = {}" |
|
622 apply (auto) |
|
623 apply (erule_tac x = x in ballE) |
|
624 apply (case_tac x) |
|
625 apply (auto simp:init_alive_prop) |
|
626 sorry (* done *) |
|
627 thus ?case using Nil unfolding enrichable_def enriched_def reserved_def |
|
628 by (rule_tac x = "[]" in exI, auto) |
|
629 next |
|
630 case (Cons e s) |
|
631 hence p1: "\<And> objs. \<forall> obj \<in> objs. alive s obj \<and> is_created s obj \<and> recorded obj |
|
632 \<Longrightarrow> \<exists> s'. valid s' \<and> s2ss s' = s2ss s \<and> enriched s objs s' \<and> reserved s objs s'" |
|
633 and p2: "valid (e # s)" and p3: "\<forall>obj\<in>objs. alive (e # s) obj \<and> is_created (e # s) obj \<and> recorded obj" |
|
634 and os: "os_grant s e" and se: "grant s e" and vd: "valid s" |
|
635 by (auto dest:vt_grant_os vd_cons vt_grant simp:enrichable_def) |
|
636 show ?case |
|
637 proof (cases e) |
|
638 case (Execve p f fds) |
|
639 hence p4: "e = Execve p f fds" by simp |
|
640 from p3 have p5: "is_inited s (O_proc p) \<Longrightarrow> (O_proc p) \<notin> objs" |
|
641 by (auto simp:is_created_def is_inited_def p4 elim!:ballE[where x = "O_proc p"]) |
|
642 show "enrichable (e # s) objs" |
|
643 proof (cases "is_inited s (O_proc p)") |
|
644 case True |
|
645 with p5 have a1: "(O_proc p) \<notin> objs" by simp |
|
646 with p3 p4 p2 have a2: "\<forall> obj \<in> objs. alive s obj \<and> is_created s obj" and a2': "\<forall> obj \<in> objs. recorded obj" |
|
647 apply (auto simp:is_created_def alive_simps is_inited_def) |
|
648 apply (erule_tac x = obj in ballE, auto simp:alive_simps split:t_object.splits) |
|
649 done |
|
650 then obtain s' where a3: "valid s'" and a4: "s2ss s' = s2ss s" |
|
651 and a5: "enriched s objs s'" and a6: "reserved s objs s'" |
|
652 using p1 apply (simp add:enrichable_def) sorry |
|
653 from a5 p4 p2 a2' have a7: "enriched s objs (e # s')" |
|
654 apply (clarsimp simp add:enriched_def co2sobj_execve) |
|
655 apply (erule_tac x = obj in ballE, clarsimp) |
|
656 apply (rule_tac x = obj' in exI, auto simp:co2sobj_execve alive_simps) |
|
657 thm enriched_def |
|
658 |
|
659 |
|
660 |
|
661 obtain s' where p6:"enriched s objs s'" |
|
662 apply (simp add: alive_simps enrichable_def) |
|
663 apply auto apply (rule ballI, rule_tac x = obj in exI) |
|
664 |
|
665 have p6:"enriched (e # s) objs (e # s)" |
|
666 apply (simp add:enriched_def alive_simps) |
|
667 apply auto apply (rule ballI, rule_tac x = obj in exI) |
|
668 |
|
669 have "enrich (e # s) objs (e # s)" |
|
670 apply (simp add:enrich_def p4) |
|
671 sorry |
|
672 moreover have "reserve (e # s) objs (e # s)" |
|
673 sorry |
|
674 ultimately show ?thesis using p2 |
|
675 apply (simp add:enrichable_def) |
|
676 by (rule_tac x = "e # s" in exI, simp) |
|
677 next |
|
678 |
|
679 |
|
680 thm enrichable_def |
|
681 apply (simp add:enrichable_def p4) |
|
682 |
|
683 |
|
684 |
|
685 apply auto |
|
686 apply (auto simp:enrichable_def) |
|
687 apply (induct s) |
|
688 |
|
689 |
|
690 |
|
691 done |
|
692 |
|
693 qed |
|
694 *) |
|
695 |
|
696 lemma d2s_main: |
|
697 "valid s \<Longrightarrow> s2ss s \<propto> static" |
|
698 apply (induct s, simp add:s2ss_nil_prop init_ss_in_def) |
|
699 apply (rule_tac x = "init_static_state" in bexI, simp, simp add:s_init) |
|
700 apply (frule vd_cons, frule vt_grant_os, simp) |
|
701 apply (case_tac a) |
|
702 apply (clarsimp simp add:s2ss_execve) |
|
703 apply (rule conjI, rule impI) |
|
704 |
|
705 |
|
706 |
|
707 sorry |
|
708 |
|
709 lemma s2d_main: |
|
710 "ss \<in> static \<Longrightarrow> \<exists> s. valid s \<and> s2ss s = ss" |
|
711 apply (erule static.induct) |
|
712 apply (rule_tac x = "[]" in exI, simp add:s2ss_nil_prop valid.intros) |
|
713 |
|
714 apply (erule exE|erule conjE)+ |
|
715 |
|
716 apply (simp add:update_ss_def) |
|
717 |
|
718 sorry |
|
719 |
|
720 lemma s2d_main': |
|
721 "ss \<in> static \<Longrightarrow> \<exists> s. valid s \<and> s2ss s \<doteq> ss" |
|
722 apply (erule static.induct) |
|
723 apply (rule_tac x = "[]" in exI, simp add:s2ss_nil_prop valid.intros) |
|
724 |
|
725 apply (erule exE|erule conjE)+ |
|
726 |
|
727 apply (simp add:update_ss_def) |
|
728 |
|
729 sorry |
|
730 |
|
731 |
|
732 end |
|
733 |
|
734 end |