81 |
81 |
82 lemma is_init_dir_prop2: "is_init_dir f = (init_alive (O_dir f))" |
82 lemma is_init_dir_prop2: "is_init_dir f = (init_alive (O_dir f))" |
83 by (auto simp add:is_init_dir_def is_dir_def init_inum_of_file_props split:option.splits) |
83 by (auto simp add:is_init_dir_def is_dir_def init_inum_of_file_props split:option.splits) |
84 |
84 |
85 lemmas is_init_dir_props = is_init_dir_prop1 is_init_dir_prop2 |
85 lemmas is_init_dir_props = is_init_dir_prop1 is_init_dir_prop2 |
|
86 |
|
87 lemma is_file_nil: "is_file [] = is_init_file" |
|
88 by (auto simp:is_init_file_def is_file_def init_inum_of_file_props intro!:ext split:option.splits) |
|
89 |
|
90 lemma is_dir_nil: "is_dir [] = is_init_dir" |
|
91 by (auto simp:is_init_dir_def is_dir_def init_inum_of_file_props intro!:ext split:option.splits) |
86 |
92 |
87 lemma is_init_udp_sock_prop1: "is_init_udp_sock s = (s \<in> init_sockets \<and> is_udp_sock [] s)" |
93 lemma is_init_udp_sock_prop1: "is_init_udp_sock s = (s \<in> init_sockets \<and> is_udp_sock [] s)" |
88 apply (auto simp add:is_init_udp_sock_def is_udp_sock_def init_inum_of_socket_props |
94 apply (auto simp add:is_init_udp_sock_def is_udp_sock_def init_inum_of_socket_props |
89 dest:init_socket_has_inode split:option.splits) |
95 dest:init_socket_has_inode split:option.splits) |
90 done |
96 done |
234 apply (frule init_parent_file_is_dir', simp+) |
240 apply (frule init_parent_file_is_dir', simp+) |
235 apply (drule init_files_prop1) |
241 apply (drule init_files_prop1) |
236 apply (erule_tac x = f' in allE, simp) |
242 apply (erule_tac x = f' in allE, simp) |
237 by (case_tac f', simp_all add:no_junior_def) |
243 by (case_tac f', simp_all add:no_junior_def) |
238 |
244 |
|
245 lemma same_inode_nil_prop: |
|
246 "same_inode_files [] f = init_same_inode_files f" |
|
247 by (simp add:same_inode_files_def init_same_inode_files_def) |
|
248 |
|
249 lemma init_same_inode_prop1: |
|
250 "f \<in> init_files \<Longrightarrow> \<forall> f' \<in> init_same_inode_files f. f' \<in> init_files" |
|
251 apply (simp add:init_same_inode_files_def) |
|
252 apply (drule init_files_prop3) |
|
253 apply (auto simp:init_files_prop1) |
|
254 done |
239 |
255 |
240 end |
256 end |
241 |
257 |
242 context flask begin |
258 context flask begin |
243 |
259 |
348 lemma init_dir_user_prop5: "init_user_of_obj (O_dir f) = Some u \<Longrightarrow> u \<in> init_users" |
364 lemma init_dir_user_prop5: "init_user_of_obj (O_dir f) = Some u \<Longrightarrow> u \<in> init_users" |
349 by (simp add:init_user_has_obj) |
365 by (simp add:init_user_has_obj) |
350 |
366 |
351 lemmas init_dir_users_props = init_dir_user_prop1 init_dir_user_prop2 init_dir_user_prop3 init_dir_user_prop4 init_dir_user_prop5 |
367 lemmas init_dir_users_props = init_dir_user_prop1 init_dir_user_prop2 init_dir_user_prop3 init_dir_user_prop4 init_dir_user_prop5 |
352 |
368 |
|
369 lemma init_file_dir_conflict: "\<lbrakk>is_init_file f; is_init_dir f\<rbrakk> \<Longrightarrow> False" |
|
370 by (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits) |
|
371 |
|
372 lemma init_file_dir_conflict1: "is_init_file f \<Longrightarrow> \<not> is_init_dir f" |
|
373 by (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits) |
|
374 |
|
375 lemma init_file_dir_conflict2: "is_init_dir f \<Longrightarrow> \<not> is_init_file f" |
|
376 by (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits) |
|
377 |
353 end |
378 end |
354 |
379 |
|
380 context tainting begin |
|
381 |
|
382 lemma tainted_nil_prop: |
|
383 "(x \<in> tainted []) = (x \<in> seeds)" |
|
384 apply (rule iffI) |
|
385 apply (erule tainted.cases, simp+) |
|
386 apply (erule t_init) |
|
387 done |
|
388 |
|
389 end |
355 |
390 |
356 context tainting_s begin |
391 context tainting_s begin |
357 |
392 |
358 lemma init_file_has_ctxt: |
393 lemma init_file_has_ctxt: |
359 "is_init_file f \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_file f) = Some sec" |
394 "is_init_file f \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_file f) = Some sec" |
590 apply (auto simp:init_sectxt_prop cf2sfile_def init_cf2sfile_def split:option.splits dest!:init_has_ctxt') |
625 apply (auto simp:init_sectxt_prop cf2sfile_def init_cf2sfile_def split:option.splits dest!:init_has_ctxt') |
591 apply (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits |
626 apply (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits |
592 dest:init_file_has_inum inof_has_file_tag) |
627 dest:init_file_has_inum inof_has_file_tag) |
593 done |
628 done |
594 |
629 |
595 lemma init_file_dir_conflict: "\<lbrakk>is_init_file f; is_init_dir f\<rbrakk> \<Longrightarrow> False" |
|
596 by (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits) |
|
597 |
|
598 lemma init_file_dir_conflict1: "is_init_file f \<Longrightarrow> \<not> is_init_dir f" |
|
599 by (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits) |
|
600 |
|
601 lemma init_file_dir_conflict2: "is_init_dir f \<Longrightarrow> \<not> is_init_file f" |
|
602 by (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits) |
|
603 |
630 |
604 lemma init_sec_file_dir: |
631 lemma init_sec_file_dir: |
605 "\<lbrakk>init_sectxt_of_obj (O_file f) = Some x; init_sectxt_of_obj (O_dir f) = Some y\<rbrakk> \<Longrightarrow> False" |
632 "\<lbrakk>init_sectxt_of_obj (O_file f) = Some x; init_sectxt_of_obj (O_dir f) = Some y\<rbrakk> \<Longrightarrow> False" |
606 apply (drule init_sectxt_prop2)+ |
633 apply (drule init_sectxt_prop2)+ |
607 apply (auto intro:init_file_dir_conflict) |
634 apply (auto intro:init_file_dir_conflict) |
632 by (simp add:is_init_file_prop1 is_init_dir_prop1 cf2sfile_nil_prop) |
659 by (simp add:is_init_file_prop1 is_init_dir_prop1 cf2sfile_nil_prop) |
633 |
660 |
634 lemma cfs2sfiles_nil_prop: |
661 lemma cfs2sfiles_nil_prop: |
635 "\<forall> f \<in> fs. f \<in> init_files \<Longrightarrow> cfs2sfiles [] fs = init_cfs2sfiles fs" |
662 "\<forall> f \<in> fs. f \<in> init_files \<Longrightarrow> cfs2sfiles [] fs = init_cfs2sfiles fs" |
636 apply (simp add:cfs2sfiles_def init_cfs2sfiles_def) |
663 apply (simp add:cfs2sfiles_def init_cfs2sfiles_def) |
637 using cf2sfile_nil_prop apply auto |
664 apply (rule set_eqI, rule iffI, auto simp:cf2sfile_nil_prop split:if_splits) |
|
665 done |
638 |
666 |
639 lemma cfd2sfd_nil_prop: |
667 lemma cfd2sfd_nil_prop: |
640 "init_file_of_proc_fd p fd = Some f \<Longrightarrow> cfd2sfd [] p fd = init_cfd2sfd p fd" |
668 "init_file_of_proc_fd p fd = Some f \<Longrightarrow> cfd2sfd [] p fd = init_cfd2sfd p fd" |
641 apply (simp add:cfd2sfd_def init_sectxt_prop init_cfd2sfd_def) |
669 apply (simp add:cfd2sfd_def init_sectxt_prop init_cfd2sfd_def) |
642 apply (drule init_filefd_prop1, drule cf2sfile_nil_prop) |
670 apply (frule init_filefd_prop5, drule init_filefd_prop1, drule cf2sfile_nil_prop) |
643 by (auto split:option.splits) |
671 by (auto split:option.splits) |
644 |
672 |
645 lemma cpfd2sfds_nil_prop: |
673 lemma cpfd2sfds_nil_prop: |
646 "cpfd2sfds [] p = init_cfds2sfds p" |
674 "cpfd2sfds [] p = init_cfds2sfds p" |
647 apply (simp only:cpfd2sfds_def init_cfds2sfds_def) |
675 apply (simp only:cpfd2sfds_def init_cfds2sfds_def) |
666 lemma cp2sproc_nil_prop: |
694 lemma cp2sproc_nil_prop: |
667 "p \<in> init_procs \<Longrightarrow> cp2sproc [] p = init_cp2sproc p" |
695 "p \<in> init_procs \<Longrightarrow> cp2sproc [] p = init_cp2sproc p" |
668 by (auto simp add:init_cp2sproc_def cp2sproc_def init_sectxt_prop cph2spshs_nil_prop cpfd2sfds_nil_prop |
696 by (auto simp add:init_cp2sproc_def cp2sproc_def init_sectxt_prop cph2spshs_nil_prop cpfd2sfds_nil_prop |
669 split:option.splits) |
697 split:option.splits) |
670 |
698 |
671 lemma tainted_nil_prop: |
|
672 "(x \<in> tainted []) = (x \<in> seeds)" |
|
673 apply (rule iffI) |
|
674 apply (erule tainted.cases, simp+) |
|
675 apply (erule t_init) |
|
676 done |
|
677 |
|
678 lemma msg_has_sec_imp_init: |
699 lemma msg_has_sec_imp_init: |
679 "init_sectxt_of_obj (O_msg q m) = Some sec \<Longrightarrow> q \<in> init_msgqs \<and> m \<in> set (init_msgs_of_queue q)" |
700 "init_sectxt_of_obj (O_msg q m) = Some sec \<Longrightarrow> q \<in> init_msgqs \<and> m \<in> set (init_msgs_of_queue q)" |
680 apply (simp add:init_sectxt_of_obj_def split:option.splits) |
701 apply (simp add:init_sectxt_of_obj_def split:option.splits) |
681 by (drule init_type_has_obj, simp) |
702 by (drule init_type_has_obj, simp) |
682 |
703 |
698 |
719 |
699 lemma cq2smsga_nil_prop: |
720 lemma cq2smsga_nil_prop: |
700 "cq2smsgq [] q = init_cq2smsgq q" |
721 "cq2smsgq [] q = init_cq2smsgq q" |
701 by (auto simp add:cq2smsgq_def init_cq2smsgq_def init_sectxt_prop cqm2sms_nil_prop |
722 by (auto simp add:cq2smsgq_def init_cq2smsgq_def init_sectxt_prop cqm2sms_nil_prop |
702 intro:msgq_has_sec_imp_init split:option.splits) |
723 intro:msgq_has_sec_imp_init split:option.splits) |
703 |
|
704 lemma same_inode_nil_prop: |
|
705 "same_inode_files [] f = init_same_inode_files f" |
|
706 by (simp add:same_inode_files_def init_same_inode_files_def) |
|
707 |
|
708 lemma init_same_inode_prop1: |
|
709 "f \<in> init_files \<Longrightarrow> \<forall> f' \<in> init_same_inode_files f. f' \<in> init_files" |
|
710 apply (simp add:init_same_inode_files_def) |
|
711 apply (drule init_files_prop3) |
|
712 apply (auto simp:init_files_prop1) |
|
713 done |
|
714 |
724 |
715 lemma co2sobj_nil_prop: |
725 lemma co2sobj_nil_prop: |
716 "init_alive obj \<Longrightarrow> co2sobj [] obj = init_obj2sobj obj" |
726 "init_alive obj \<Longrightarrow> co2sobj [] obj = init_obj2sobj obj" |
717 apply (case_tac obj) |
727 apply (case_tac obj) |
718 apply (auto simp add:cf2sfile_nil_prop cq2smsga_nil_prop cqm2sms_nil_prop tainted_nil_prop |
728 apply (auto simp add:cf2sfile_nil_prop cq2smsga_nil_prop cqm2sms_nil_prop tainted_nil_prop |
719 cp2sproc_nil_prop cfs2sfiles_nil_prop is_init_dir_prop1 is_init_file_prop1 |
729 cp2sproc_nil_prop cfs2sfiles_nil_prop is_init_dir_prop1 is_init_file_prop1 |
720 is_init_udp_sock_prop1 is_init_tcp_sock_prop1 ch2sshm_nil_prop |
730 is_init_udp_sock_prop1 is_init_tcp_sock_prop1 ch2sshm_nil_prop |
721 same_inode_nil_prop cm2smsg_nil_prop dest:init_same_inode_prop1 |
731 same_inode_nil_prop cm2smsg_nil_prop |
|
732 dest:init_same_inode_prop1 |
722 split:option.splits) |
733 split:option.splits) |
723 apply (rule_tac x = list in exI, simp add:init_same_inode_files_def) |
734 apply (rule_tac x = list in exI, simp add:init_same_inode_files_def) |
724 by (simp add:init_files_props) |
735 apply (simp add:init_files_props) |
|
736 apply (auto simp:is_dir_nil is_file_nil dest:init_file_dir_conflict) |
|
737 done |
725 |
738 |
726 lemma s2ss_nil_prop: |
739 lemma s2ss_nil_prop: |
727 "s2ss [] = init_static_state" |
740 "s2ss [] = init_static_state" |
728 using co2sobj_nil_prop init_alive_prop |
741 using co2sobj_nil_prop init_alive_prop |
729 by (auto simp add:s2ss_def init_static_state_def) |
742 by (auto simp add:s2ss_def init_static_state_def) |