115 show ?thesis using grant f_in f_in' psfs psfs' psfs_eq sec |
115 show ?thesis using grant f_in f_in' psfs psfs' psfs_eq sec |
116 apply (simp add:Cons split:option.splits) |
116 apply (simp add:Cons split:option.splits) |
117 by (case_tac a, simp) |
117 by (case_tac a, simp) |
118 qed |
118 qed |
119 |
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 |
120 lemma enrich_inherit_fds_check: |
125 lemma enrich_inherit_fds_check: |
121 assumes grant: "inherit_fds_check s (up, nr, nt) p fds" and vd: "valid s" |
126 assumes grant: "inherit_fds_check s (up, nr, nt) p fds" and vd: "valid s" |
122 and cp2sp: "\<forall> p. p \<in> current_procs s \<longrightarrow> cp2sproc s' p = cp2sproc s p" |
127 and cp2sp: "\<forall> p. p \<in> current_procs s \<longrightarrow> cp2sproc s' p = cp2sproc s p" |
123 and p_in: "p \<in> current_procs s" and p_in': "p \<in> current_procs s'" |
128 and p_in: "p \<in> current_procs s" and p_in': "p \<in> current_procs s'" |
124 and fd_in: "fds \<subseteq> current_proc_fds s p" and fd_in': "fds \<subseteq> current_proc_fds s' p" |
129 and fd_in: "fds \<subseteq> proc_file_fds s p" and fd_in': "fds \<subseteq> proc_file_fds s' p" |
125 shows "inherit_fds_check s' (up, nr, nt) p fds" |
130 shows "inherit_fds_check s' (up, nr, nt) p fds" |
126 proof- |
131 proof- |
127 have "\<And> fd. fd \<in> fds \<Longrightarrow> sectxt_of_obj s' (O_fd p fd) = sectxt_of_obj s (O_fd p fd)" |
132 have "\<And> fd. fd \<in> fds \<Longrightarrow> sectxt_of_obj s' (O_fd p fd) = sectxt_of_obj s (O_fd p fd)" |
128 proof- |
133 proof- |
129 fix fd |
134 fix fd |
130 assume fd_in_fds: "fd \<in> fds" |
135 assume fd_in_fds: "fd \<in> fds" |
131 hence fd_in_cfds: "fd \<in> current_proc_fds s p" |
136 hence fd_in_cfds: "fd \<in> proc_file_fds s p" |
132 and fd_in_cfds': "fd \<in> current_proc_fds s' p" |
137 and fd_in_cfds': "fd \<in> proc_file_fds s' p" |
133 using fd_in fd_in' by auto |
138 using fd_in fd_in' by auto |
134 from p_in vd obtain sp where csp: "cp2sproc s p = Some sp" |
139 from p_in vd obtain sp where csp: "cp2sproc s p = Some sp" |
135 by (drule_tac current_proc_has_sp, simp, erule_tac exE, simp) |
140 by (drule_tac current_proc_has_sp, simp, erule_tac exE, simp) |
136 with cp2sp have "cpfd2sfds s p = cpfd2sfds s' p" |
141 with cp2sp have "cpfd2sfds s p = cpfd2sfds s' p" |
137 apply (erule_tac x = p in allE) |
142 apply (erule_tac x = p in allE) |
138 by (auto simp:cp2sproc_def split:option.splits simp:p_in) |
143 by (auto simp:cp2sproc_def split:option.splits simp:p_in) |
139 hence "cfd2sfd s p fd = cfd2sfd s' p fd" |
144 hence "cfd2sfd s p fd = cfd2sfd s' p fd" using fd_in_cfds fd_in_cfds' |
140 apply (simp add:cpfd2sfds_def) |
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 (* |
141 thm inherit_fds_check_def |
149 thm inherit_fds_check_def |
142 thm sectxts_of_fds_def |
150 thm sectxts_of_fds_def |
143 thm cpfd2sfds_def |
151 thm cpfd2sfds_def |
144 apply ( |
152 apply ( |
145 |
153 *)sorry |
146 show "sectxt_of_obj s' (O_fd p fd) = sectxt_of_obj s (O_fd p fd)" |
154 show "sectxt_of_obj s' (O_fd p fd) = sectxt_of_obj s (O_fd p fd)" |
147 sorry |
155 sorry |
148 qed |
156 qed |
149 hence "sectxts_of_fds s' p fds = sectxts_of_fds s p fds" |
157 hence "sectxts_of_fds s' p fds = sectxts_of_fds s p fds" |
150 by (simp add:sectxts_of_fds_def) |
158 by (simp add:sectxts_of_fds_def) |
158 and os: "os_grant s e" and grant: "grant s e" and vd: "valid s" |
166 and os: "os_grant s e" and grant: "grant s e" and vd: "valid s" |
159 and alive: "\<forall> obj. alive s obj \<longrightarrow> alive s' obj" |
167 and alive: "\<forall> obj. alive s obj \<longrightarrow> alive s' obj" |
160 and cp2sp: "\<forall> p. p \<in> current_procs s \<longrightarrow> cp2sproc s' p = cp2sproc s p" |
168 and cp2sp: "\<forall> p. p \<in> current_procs s \<longrightarrow> cp2sproc s' p = cp2sproc s p" |
161 and cf2sf: "\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile s' f = cf2sfile s f" |
169 and cf2sf: "\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile s' f = cf2sfile s f" |
162 shows "valid (e # s')" |
170 shows "valid (e # s')" |
|
171 |
|
172 sorry (* |
163 proof (cases e) |
173 proof (cases e) |
164 case (Execve p f fds) |
174 case (Execve p f fds) |
165 have p_in: "p \<in> current_procs s'" using os alive |
175 have p_in: "p \<in> current_procs s'" using os alive |
166 apply (erule_tac x = "O_proc p" in allE) |
176 apply (erule_tac x = "O_proc p" in allE) |
167 by (auto simp:Execve) |
177 by (auto simp:Execve) |
196 show ? |
206 show ? |
197 proof- |
207 proof- |
198 have |
208 have |
199 |
209 |
200 |
210 |
201 |
211 *) |
202 |
212 |
203 lemma enrich_proc_prop: |
213 lemma enrich_proc_prop: |
204 "\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s\<rbrakk> |
214 "\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s\<rbrakk> |
205 \<Longrightarrow> valid (enrich_proc s p p') \<and> |
215 \<Longrightarrow> valid (enrich_proc s p p') \<and> |
206 (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> |
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> |
207 (\<forall> obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj) \<and> |
217 (\<forall> obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj) \<and> |
208 (\<forall> p'. p' \<in> current_procs s \<longrightarrow> cp2sproc (enrich_proc s p p') p' = cp2sproc s p) \<and> |
218 (\<forall> p'. p' \<in> current_procs s \<longrightarrow> cp2sproc (enrich_proc s p p') p' = cp2sproc s p) \<and> |
209 (\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f) \<and> |
219 (\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f) \<and> |
210 (Tainted (enrich_proc s p p') = (Tainted s \<union> (if (O_proc p \<in> Tainted s) then {O_proc p'} else {})))" |
220 (Tainted (enrich_proc s p p') = (Tainted s \<union> (if (O_proc p \<in> Tainted s) then {O_proc p'} else {})))" |
|
221 sorry (* |
211 proof (induct s) |
222 proof (induct s) |
212 case Nil |
223 case Nil |
213 thus ?case by (auto simp:is_created_proc_def) |
224 thus ?case by (auto simp:is_created_proc_def) |
214 next |
225 next |
215 case (Cons e s) |
226 case (Cons e s) |
235 moreover have c4: "alive (e # s) obj \<longrightarrow> |
246 moreover have c4: "alive (e # s) obj \<longrightarrow> |
236 alive (enrich_proc (e # s) p p') obj \<and> co2sobj (enrich_proc (e # s) p p') obj = co2sobj (e # s) obj" |
247 alive (enrich_proc (e # s) p p') obj \<and> co2sobj (enrich_proc (e # s) p p') obj = co2sobj (e # s) obj" |
237 sorry |
248 sorry |
238 ultimately show ?case by auto |
249 ultimately show ?case by auto |
239 qed |
250 qed |
240 |
251 *) |
241 |
252 |
242 |
253 |
243 lemma "alive s obj \<Longrightarrow> alive (enrich_proc s p p') obj" |
254 lemma "alive s obj \<Longrightarrow> alive (enrich_proc s p p') obj" |
244 apply (induct s, simp) |
255 apply (induct s, simp) |
245 apply (case_tac a, case_tac[!] obj) |
256 apply (case_tac a, case_tac[!] obj) sorry (* |
246 apply (auto simp:is_file_def is_dir_def split:option.splits t_inode_tag.splits) |
257 apply (auto simp:is_file_def is_dir_def split:option.splits t_inode_tag.splits) |
247 thm is_file_other |
258 thm is_file_other |
248 |
259 *) |
249 lemma enrich_proc_valid: |
260 lemma enrich_proc_valid: |
250 "\<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')" |
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')" (* |
251 apply (induct s, simp) |
262 apply (induct s, simp) |
252 apply (frule vd_cons, frule vt_grant, frule vt_grant_os, case_tac a) |
263 apply (frule vd_cons, frule vt_grant, frule vt_grant_os, case_tac a) |
253 apply (auto intro!:valid.intros(2)) |
264 apply (auto intro!:valid.intros(2)) |
254 prefer 28 |
265 prefer 28 |
255 |
266 |
256 |
267 |
257 |
268 |
258 end |
269 end |
|
270 *) |
|
271 sorry |
|
272 |
259 |
273 |
260 (* for any created obj, we can enrich trace with events that create new objs with the same static-properties *) |
274 (* for any created obj, we can enrich trace with events that create new objs with the same static-properties *) |
261 definition enriched:: "t_state \<Rightarrow> t_object set \<Rightarrow> t_state \<Rightarrow> bool" |
275 definition enriched:: "t_state \<Rightarrow> t_object set \<Rightarrow> t_state \<Rightarrow> bool" |
262 where |
276 where |
263 "enriched s objs s' \<equiv> \<forall> obj \<in> objs. \<exists> obj'. \<not> alive s obj' \<and> obj' \<notin> objs \<and> |
277 "enriched s objs s' \<equiv> \<forall> obj \<in> objs. \<exists> obj'. \<not> alive s obj' \<and> obj' \<notin> objs \<and> |
385 apply (case_tac sf) |
399 apply (case_tac sf) |
386 apply (induct f) |
400 apply (induct f) |
387 apply (auto simp:search_check_s_def search_check.simps cf2sfile_def sroot_def |
401 apply (auto simp:search_check_s_def search_check.simps cf2sfile_def sroot_def |
388 root_sec_remains init_sectxt_prop sec_of_root_valid |
402 root_sec_remains init_sectxt_prop sec_of_root_valid |
389 dest!:root_is_dir' current_has_sec' split:option.splits) |
403 dest!:root_is_dir' current_has_sec' split:option.splits) |
390 apply (simp add:search_check_allp_def) |
|
391 done |
404 done |
392 |
405 |
393 lemma grant_execve_intro_execve: |
406 lemma grant_execve_intro_execve: |
394 "\<lbrakk>cp2sproc (Execve p f fds # s) p = Some (pi', sec', sfds', shms'); valid (Execve p f fds # s); |
407 "\<lbrakk>cp2sproc (Execve p f fds # s) p = Some (pi', sec', sfds', shms'); valid (Execve p f fds # s); |
395 cp2sproc s p = Some (pi, sec, sfds, shms); cf2sfile s f = Some (fi, fsec, psec, asecs)\<rbrakk> |
408 cp2sproc s p = Some (pi, sec, sfds, shms); cf2sfile s f = Some (fi, fsec, psec, asecs)\<rbrakk> |
435 "\<lbrakk>cp2sproc (Execve p f fds # s) p = Some (pi', sec', sfds', shms'); |
448 "\<lbrakk>cp2sproc (Execve p f fds # s) p = Some (pi', sec', sfds', shms'); |
436 inherit_fds_check s sec' p fds; valid (Execve p f fds # s)\<rbrakk> |
449 inherit_fds_check s sec' p fds; valid (Execve p f fds # s)\<rbrakk> |
437 \<Longrightarrow> inherit_fds_check_s sec' sfds'" |
450 \<Longrightarrow> inherit_fds_check_s sec' sfds'" |
438 apply (frule vt_grant_os, frule vd_cons, frule vt_grant) |
451 apply (frule vt_grant_os, frule vd_cons, frule vt_grant) |
439 apply (auto simp:cp2sproc_def cpfd2sfds_execve inherit_fds_check_def inherit_fds_check_s_def split:option.splits) |
452 apply (auto simp:cp2sproc_def cpfd2sfds_execve inherit_fds_check_def inherit_fds_check_s_def split:option.splits) |
|
453 sorry (* |
440 apply (erule_tac x = "(ad, ae, bc)" in ballE, auto simp:sectxts_of_sfds_def sectxts_of_fds_def) |
454 apply (erule_tac x = "(ad, ae, bc)" in ballE, auto simp:sectxts_of_sfds_def sectxts_of_fds_def) |
441 apply (erule_tac x = fd in ballE, auto simp:cfd2sfd_def split:option.splits) |
455 apply (erule_tac x = fd in ballE, auto simp:cfd2sfd_def split:option.splits) |
442 done |
456 done *) |
443 |
457 |
444 lemma d2s_main_execve_grant_aux: |
458 lemma d2s_main_execve_grant_aux: |
445 "\<lbrakk>cp2sproc (Execve p f fds # s) p = Some (pi', sec', sfds', shms'); valid (Execve p f fds # s); |
459 "\<lbrakk>cp2sproc (Execve p f fds # s) p = Some (pi', sec', sfds', shms'); valid (Execve p f fds # s); |
446 cp2sproc s p = Some (pi, sec, sfds, shms); cf2sfile s f = Some (fi, fsec, psec, asecs)\<rbrakk> |
460 cp2sproc s p = Some (pi, sec, sfds, shms); cf2sfile s f = Some (fi, fsec, psec, asecs)\<rbrakk> |
447 \<Longrightarrow> (npctxt_execve sec fsec = Some sec') \<and> grant_execve sec fsec sec' \<and> |
461 \<Longrightarrow> (npctxt_execve sec fsec = Some sec') \<and> grant_execve sec fsec sec' \<and> |
552 apply (simp add:reserved_def) |
566 apply (simp add:reserved_def) |
553 by (erule_tac x = "O_proc p" in allE, auto) |
567 by (erule_tac x = "O_proc p" in allE, auto) |
554 moreover from a4 os p4 have "is_file s' f" |
568 moreover from a4 os p4 have "is_file s' f" |
555 apply (simp add:reserved_def) |
569 apply (simp add:reserved_def) |
556 by (erule_tac x = "O_file f" in allE, auto) |
570 by (erule_tac x = "O_file f" in allE, auto) |
557 moreover from a4 os p4 have "fds \<subseteq> current_proc_fds s' p" |
571 moreover from a4 os p4 vd have "fds \<subseteq> proc_file_fds s' p" |
558 apply (rule_tac subsetI, clarsimp simp:reserved_def current_proc_fds.simps) |
572 apply (rule_tac subsetI, clarsimp simp:reserved_def current_proc_fds.simps) |
559 apply (erule_tac x = "O_fd p x" in allE, erule impE) |
573 apply (erule_tac x = "O_fd p x" in allE, erule impE) |
560 apply (simp, erule set_mp, simp+) |
574 sorry |
561 done |
|
562 ultimately have "os_grant s' e" |
575 ultimately have "os_grant s' e" |
563 by (simp add:p4) |
576 by (simp add:p4) |
564 moreover have "grant s' e" |
577 moreover have "grant s' e" |
565 sorry |
578 sorry |
566 ultimately have "valid (e # s')" |
579 ultimately have "valid (e # s')" |
569 apply (simp add:enrichable_def) |
582 apply (simp add:enrichable_def) |
570 apply (rule_tac x = "e # s'" in exI) |
583 apply (rule_tac x = "e # s'" in exI) |
571 apply (simp) |
584 apply (simp) |
572 sorry |
585 sorry |
573 qed |
586 qed |
|
587 qed |
574 |
588 |
575 lemma s2d_main_execve: |
589 lemma s2d_main_execve: |
576 "\<lbrakk>grant_execve pctxt fsec pctxt'; ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; S_file sfs tagf \<in> ss; |
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; |
577 (fi, fsec, pfsec, asecs) \<in> sfs; npctxt_execve pctxt fsec = Some pctxt'; |
591 (fi, fsec, pfsec, asecs) \<in> sfs; npctxt_execve pctxt fsec = Some pctxt'; |
578 search_check_s pctxt (fi, fsec, pfsec, asecs) True; inherit_fds_check_s pctxt' fds'; fds' \<subseteq> fds; valid s; |
592 search_check_s pctxt (fi, fsec, pfsec, asecs) True; inherit_fds_check_s pctxt' fds'; fds' \<subseteq> fds; valid s; |
580 s2ss s = update_ss ss (S_proc (pi, pctxt, fds, shms) tagp) (S_proc (pi, pctxt', fds', {}) (tagp \<or> tagf))" |
594 s2ss s = update_ss ss (S_proc (pi, pctxt, fds, shms) tagp) (S_proc (pi, pctxt', fds', {}) (tagp \<or> tagf))" |
581 apply (simp add:update_ss_def) |
595 apply (simp add:update_ss_def) |
582 thm update_ss_def |
596 thm update_ss_def |
583 sorry |
597 sorry |
584 |
598 |
585 |
599 (* |
586 lemma s2d_main_execve: |
600 lemma s2d_main_execve: |
587 "ss \<in> static \<Longrightarrow> \<exists> s. valid s \<and> s2ss s = ss" |
601 "ss \<in> static \<Longrightarrow> \<exists> s. valid s \<and> s2ss s = ss" |
588 apply (erule static.induct) |
602 apply (erule static.induct) |
589 apply (rule_tac x = "[]" in exI, simp add:s2ss_nil_prop valid.intros) |
603 apply (rule_tac x = "[]" in exI, simp add:s2ss_nil_prop valid.intros) |
590 apply (erule exE|erule conjE)+ |
604 apply (erule exE|erule conjE)+ |
591 apply (rule s2d_main_execve, simp+) |
605 apply (rule s2d_main_execve, simp+) |
592 |
606 |
593 apply (erule exE|erule conjE)+ |
607 apply (erule exE|erule conjE)+ |
594 |
608 |
595 apply (simp add:update_ss_def) |
|
596 |
609 |
597 sorry |
610 sorry |
598 |
611 *) |
599 |
612 |
600 |
613 |
601 (*********************** uppest-level 3 theorems ***********************) |
614 (*********************** uppest-level 3 theorems ***********************) |
602 |
615 |
603 lemma enrichability: |
616 lemma enrichability: |
604 "\<lbrakk>valid s; \<forall> obj \<in> objs. alive s obj \<and> is_created s obj \<and> recorded obj\<rbrakk> |
617 "\<lbrakk>valid s; \<forall> obj \<in> objs. alive s obj \<and> is_created s obj \<and> recorded obj\<rbrakk> |
605 \<Longrightarrow> enrichable s objs" |
618 \<Longrightarrow> enrichable s objs" sorry (* |
606 proof (induct s arbitrary:objs) |
619 proof (induct s arbitrary:objs) |
607 case Nil |
620 case Nil |
608 hence "objs = {}" |
621 hence "objs = {}" |
609 apply (auto simp:is_created_def) |
622 apply (auto) |
610 apply (erule_tac x = x in ballE) |
623 apply (erule_tac x = x in ballE) |
|
624 apply (case_tac x) |
611 apply (auto simp:init_alive_prop) |
625 apply (auto simp:init_alive_prop) |
612 done |
626 sorry (* done *) |
613 thus ?case using Nil unfolding enrichable_def enriched_def reserved_def |
627 thus ?case using Nil unfolding enrichable_def enriched_def reserved_def |
614 by (rule_tac x = "[]" in exI, auto) |
628 by (rule_tac x = "[]" in exI, auto) |
615 next |
629 next |
616 case (Cons e s) |
630 case (Cons e s) |
617 hence p1: "\<And> objs. \<forall> obj \<in> objs. alive s obj \<and> is_created s obj \<and> recorded obj |
631 hence p1: "\<And> objs. \<forall> obj \<in> objs. alive s obj \<and> is_created s obj \<and> recorded obj |