47 | _ \<Rightarrow> None) else |
47 | _ \<Rightarrow> None) else |
48 (case (init_sectxt_of_obj (O_dir f), init_sectxt_of_obj (O_dir pf), get_parentfs_ctxts [] pf) of |
48 (case (init_sectxt_of_obj (O_dir f), init_sectxt_of_obj (O_dir pf), get_parentfs_ctxts [] pf) of |
49 (Some sec, Some psec, Some aseclist) \<Rightarrow> Some (Init f, sec, Some psec, set aseclist) |
49 (Some sec, Some psec, Some aseclist) \<Rightarrow> Some (Init f, sec, Some psec, set aseclist) |
50 | _ \<Rightarrow> None)" |
50 | _ \<Rightarrow> None)" |
51 |
51 |
52 definition init_cfs2sfiles :: "t_file set \<Rightarrow> t_sfile set" |
52 definition init_cf2sfiles :: "t_file \<Rightarrow> t_sfile set" |
53 where |
53 where |
54 "init_cfs2sfiles fs \<equiv> {sf. \<exists>f \<in> fs. init_cf2sfile f = Some sf \<and> is_init_file f}" |
54 "init_cf2sfiles f \<equiv> {sf. \<exists>f' \<in> init_same_inode_files f. init_cf2sfile f' = Some sf}" |
55 |
55 |
56 definition init_cfd2sfd :: "t_process \<Rightarrow> t_fd \<Rightarrow> (security_context_t \<times> t_open_flags \<times> t_sfile) option" |
56 definition init_cfd2sfd :: "t_process \<Rightarrow> t_fd \<Rightarrow> (security_context_t \<times> t_open_flags \<times> t_sfile) option" |
57 where |
57 where |
58 "init_cfd2sfd p fd = |
58 "init_cfd2sfd p fd = |
59 (case (init_file_of_proc_fd p fd, init_oflags_of_proc_fd p fd, init_sectxt_of_obj (O_fd p fd)) of |
59 (case (init_file_of_proc_fd p fd, init_oflags_of_proc_fd p fd, init_sectxt_of_obj (O_fd p fd)) of |
115 (case (init_cp2sproc p) of |
115 (case (init_cp2sproc p) of |
116 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> seeds)) |
116 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> seeds)) |
117 | _ \<Rightarrow> None)" |
117 | _ \<Rightarrow> None)" |
118 | "init_obj2sobj (O_file f) = |
118 | "init_obj2sobj (O_file f) = |
119 (if (f \<in> init_files \<and> is_init_file f) |
119 (if (f \<in> init_files \<and> is_init_file f) |
120 then Some (S_file (init_cfs2sfiles (init_same_inode_files f)) |
120 then Some (S_file (init_cf2sfiles f) |
121 (\<exists> f'. f' \<in> (init_same_inode_files f) \<and> O_file f \<in> seeds)) |
121 (\<exists> f'. f' \<in> (init_same_inode_files f) \<and> O_file f \<in> seeds)) |
122 else None)" |
122 else None)" |
123 | "init_obj2sobj (O_dir f) = |
123 | "init_obj2sobj (O_dir f) = |
124 (if (is_init_dir f) then |
124 (if (is_init_dir f) then |
125 (case (init_cf2sfile f) of |
125 (case (init_cf2sfile f) of |
695 "undeletable_s obj \<equiv> init_alive obj \<and> (\<forall> ss \<in> static. \<exists> sobj \<in> ss. init_obj_related sobj obj)" |
695 "undeletable_s obj \<equiv> init_alive obj \<and> (\<forall> ss \<in> static. \<exists> sobj \<in> ss. init_obj_related sobj obj)" |
696 |
696 |
697 |
697 |
698 (**************** translation from dynamic to static *******************) |
698 (**************** translation from dynamic to static *******************) |
699 |
699 |
700 definition cf2sfile :: "t_state \<Rightarrow> t_file \<Rightarrow> bool \<Rightarrow> t_sfile option" |
700 definition cf2sfile :: "t_state \<Rightarrow> t_file \<Rightarrow> t_sfile option" |
701 where |
701 where |
702 "cf2sfile s f Is_file \<equiv> |
702 "cf2sfile s f \<equiv> |
703 case (parent f) of |
703 case (parent f) of |
704 None \<Rightarrow> if Is_file then None else Some sroot |
704 None \<Rightarrow> Some sroot |
705 | Some pf \<Rightarrow> if Is_file |
705 | Some pf \<Rightarrow> if (is_file s f) |
706 then (case (sectxt_of_obj s (O_file f), sectxt_of_obj s (O_dir pf), get_parentfs_ctxts s pf) of |
706 then (case (sectxt_of_obj s (O_file f), sectxt_of_obj s (O_dir pf), get_parentfs_ctxts s pf) of |
707 (Some sec, Some psec, Some asecs) \<Rightarrow> |
707 (Some sec, Some psec, Some asecs) \<Rightarrow> |
708 Some (if (\<not> deleted (O_file f) s \<and> is_init_file f) then Init f else Created, sec, Some psec, set asecs) |
708 Some (if (\<not> deleted (O_file f) s \<and> is_init_file f) then Init f else Created, sec, Some psec, set asecs) |
709 | _ \<Rightarrow> None) |
709 | _ \<Rightarrow> None) |
710 else (case (sectxt_of_obj s (O_dir f), sectxt_of_obj s (O_dir pf), get_parentfs_ctxts s pf) of |
710 else (case (sectxt_of_obj s (O_dir f), sectxt_of_obj s (O_dir pf), get_parentfs_ctxts s pf) of |
711 (Some sec, Some psec, Some asecs) \<Rightarrow> |
711 (Some sec, Some psec, Some asecs) \<Rightarrow> |
712 Some (if (\<not> deleted (O_dir f) s \<and> is_init_dir f) then Init f else Created, sec, Some psec, set asecs) |
712 Some (if (\<not> deleted (O_dir f) s \<and> is_init_dir f) then Init f else Created, sec, Some psec, set asecs) |
713 | _ \<Rightarrow> None)" |
713 | _ \<Rightarrow> None)" |
714 |
714 |
715 definition cfs2sfiles :: "t_state \<Rightarrow> t_file set \<Rightarrow> t_sfile set" |
715 definition cf2sfiles :: "t_state \<Rightarrow> t_file \<Rightarrow> t_sfile set" |
716 where |
716 where |
717 "cfs2sfiles s fs \<equiv> {sf. \<exists> f \<in> fs. cf2sfile s f True = Some sf}" |
717 "cf2sfiles s f \<equiv> {sf. \<exists> f' \<in> (same_inode_files s f). cf2sfile s f' = Some sf}" |
718 |
718 |
719 (* here cf2sfile is passed with True, because, process' fds are only for files not dirs *) |
719 (* here cf2sfile is passed with True, because, process' fds are only for files not dirs *) |
720 definition cfd2sfd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd \<Rightarrow> t_sfd option" |
720 definition cfd2sfd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd \<Rightarrow> t_sfd option" |
721 where |
721 where |
722 "cfd2sfd s p fd \<equiv> |
722 "cfd2sfd s p fd \<equiv> |
723 (case (file_of_proc_fd s p fd, flags_of_proc_fd s p fd, sectxt_of_obj s (O_fd p fd)) of |
723 (case (file_of_proc_fd s p fd, flags_of_proc_fd s p fd, sectxt_of_obj s (O_fd p fd)) of |
724 (Some f, Some flags, Some sec) \<Rightarrow> (case (cf2sfile s f True) of |
724 (Some f, Some flags, Some sec) \<Rightarrow> (case (cf2sfile s f) of |
725 Some sf \<Rightarrow> Some (sec, flags, sf) |
725 Some sf \<Rightarrow> Some (sec, flags, sf) |
726 | _ \<Rightarrow> None) |
726 | _ \<Rightarrow> None) |
727 | _ \<Rightarrow> None)" |
727 | _ \<Rightarrow> None)" |
728 |
728 |
729 |
729 |
780 (case (cp2sproc s p) of |
780 (case (cp2sproc s p) of |
781 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s)) |
781 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s)) |
782 | _ \<Rightarrow> None)" |
782 | _ \<Rightarrow> None)" |
783 | "co2sobj s (O_file f) = |
783 | "co2sobj s (O_file f) = |
784 (if (f \<in> current_files s) then |
784 (if (f \<in> current_files s) then |
785 Some (S_file (cfs2sfiles s (same_inode_files s f)) (O_file f \<in> tainted s)) |
785 Some (S_file (cf2sfiles s f) (O_file f \<in> tainted s)) |
786 else None)" |
786 else None)" |
787 | "co2sobj s (O_dir f) = |
787 | "co2sobj s (O_dir f) = |
788 (case (cf2sfile s f False) of |
788 (case (cf2sfile s f) of |
789 Some sf \<Rightarrow> Some (S_dir sf) |
789 Some sf \<Rightarrow> Some (S_dir sf) |
790 | _ \<Rightarrow> None)" |
790 | _ \<Rightarrow> None)" |
791 | "co2sobj s (O_msgq q) = |
791 | "co2sobj s (O_msgq q) = |
792 (case (cq2smsgq s q) of |
792 (case (cq2smsgq s q) of |
793 Some sq \<Rightarrow> Some (S_msgq sq) |
793 Some sq \<Rightarrow> Some (S_msgq sq) |