theory Static
imports Static_type OS_type_def Flask_type Flask
begin
locale tainting_s = tainting
begin
(*
definition init_sectxt_of_file:: "t_file \<Rightarrow> security_context_t option"
where
"init_sectxt_of_file f \<equiv>
if (is_init_file f) then init_sectxt_of_obj (O_file f)
else if (is_init_dir f) then init_sectxt_of_obj (O_dir f)
else None"
*)
definition sroot :: "t_sfile"
where
"sroot \<equiv> (Init [], sec_of_root, None, {})"
definition init_cf2sfile :: "t_file \<Rightarrow> t_sfile option"
where
"init_cf2sfile f \<equiv>
case (parent f) of
None \<Rightarrow> Some sroot
| Some pf \<Rightarrow> if (is_init_file f) then
(case (init_sectxt_of_obj (O_file f), init_sectxt_of_obj (O_dir pf), get_parentfs_ctxts [] pf) of
(Some sec, Some psec, Some aseclist) \<Rightarrow> Some (Init f, sec, Some psec, set aseclist)
| _ \<Rightarrow> None) else
(case (init_sectxt_of_obj (O_dir f), init_sectxt_of_obj (O_dir pf), get_parentfs_ctxts [] pf) of
(Some sec, Some psec, Some aseclist) \<Rightarrow> Some (Init f, sec, Some psec, set aseclist)
| _ \<Rightarrow> None)"
definition init_cf2sfiles :: "t_file \<Rightarrow> t_sfile set"
where
"init_cf2sfiles f \<equiv> {sf. \<exists>f' \<in> init_same_inode_files f. init_cf2sfile f' = Some sf}"
definition init_cfd2sfd :: "t_process \<Rightarrow> t_fd \<Rightarrow> (security_context_t \<times> t_open_flags \<times> t_sfile) option"
where
"init_cfd2sfd p fd =
(case (init_file_of_proc_fd p fd, init_oflags_of_proc_fd p fd, init_sectxt_of_obj (O_fd p fd)) of
(Some f, Some flags, Some sec) \<Rightarrow> (case (init_cf2sfile f) of
Some sf \<Rightarrow> Some (sec, flags, sf)
| _ \<Rightarrow> None)
| _ \<Rightarrow> None)"
definition init_cfds2sfds :: "t_process \<Rightarrow> (security_context_t \<times> t_open_flags \<times> t_sfile) set"
where
"init_cfds2sfds p \<equiv> { sfd. \<exists> fd \<in> init_proc_file_fds p. init_cfd2sfd p fd = Some sfd}"
definition init_ch2sshm :: "t_shm \<Rightarrow> t_sshm option"
where
"init_ch2sshm h \<equiv> (case (init_sectxt_of_obj (O_shm h)) of
Some sec \<Rightarrow> Some (Init h, sec)
| _ \<Rightarrow> None)"
definition init_cph2spshs
:: "t_process \<Rightarrow> (t_sshm \<times> t_shm_attach_flag) set"
where
"init_cph2spshs p \<equiv> {(sh, flag)| sh flag h. (p, flag) \<in> init_procs_of_shm h \<and>
init_ch2sshm h = Some sh}"
definition init_cp2sproc :: "t_process \<Rightarrow> t_sproc option"
where
"init_cp2sproc p \<equiv> (case (init_sectxt_of_obj (O_proc p)) of
Some sec \<Rightarrow> Some (Init p, sec, (init_cfds2sfds p), (init_cph2spshs p))
| None \<Rightarrow> None)"
(* acient files of init-file
definition init_o2s_afs :: "t_file \<Rightarrow> security_context_t set"
where
"init_o2s_afs f \<equiv> {sec. \<exists> f'. f' \<preceq> f \<and> init_sectxt_of_obj (O_dir f') = Some sec}" *)
definition init_cm2smsg :: "t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsg option"
where
"init_cm2smsg q m \<equiv> (case (init_sectxt_of_obj (O_msg q m)) of
Some sec \<Rightarrow> Some (Init m, sec, (O_msg q m) \<in> seeds)
| _ \<Rightarrow> None)"
fun init_cqm2sms :: "t_msgq \<Rightarrow> t_msg list \<Rightarrow> (t_smsg list) option"
where
"init_cqm2sms q [] = Some []"
| "init_cqm2sms q (m#ms) =
(case (init_cqm2sms q ms, init_cm2smsg q m) of
(Some sms, Some sm) \<Rightarrow> Some (sm # sms)
| _ \<Rightarrow> None)"
definition init_cq2smsgq :: "t_msgq \<Rightarrow> t_smsgq option"
where
"init_cq2smsgq q \<equiv> (case (init_sectxt_of_obj (O_msgq q), init_cqm2sms q (init_msgs_of_queue q)) of
(Some sec, Some sms) \<Rightarrow> Some (Init q, sec, sms)
| _ \<Rightarrow> None)"
fun init_obj2sobj :: "t_object \<Rightarrow> t_sobject option"
where
"init_obj2sobj (O_proc p) =
(case (init_cp2sproc p) of
Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> seeds))
| _ \<Rightarrow> None)"
| "init_obj2sobj (O_file f) =
Some (S_file (init_cf2sfiles f)
(\<exists> f'. f' \<in> (init_same_inode_files f) \<and> O_file f \<in> seeds))"
| "init_obj2sobj (O_dir f) =
(case (init_cf2sfile f) of
Some sf \<Rightarrow> Some (S_dir sf)
| _ \<Rightarrow> None)"
| "init_obj2sobj (O_msgq q) =
(case (init_cq2smsgq q) of
Some sq \<Rightarrow> Some (S_msgq sq)
| _ \<Rightarrow> None)"
| "init_obj2sobj (O_shm h) =
(case (init_ch2sshm h) of
Some sh \<Rightarrow> Some (S_shm sh)
| _ \<Rightarrow> None)" (*
| "init_obj2sobj (O_msg q m) =
(case (init_cq2smsgq q, init_cm2smsg q m) of
(Some sq, Some sm) \<Rightarrow> Some (S_msg sq sm)
| _ \<Rightarrow> None)" *)
| "init_obj2sobj _ = None"
definition
"init_static_state \<equiv> {sobj. \<exists> obj. init_alive obj \<and> init_obj2sobj obj = Some sobj}"
(**************** translation from dynamic to static *******************)
definition cf2sfile :: "t_state \<Rightarrow> t_file \<Rightarrow> t_sfile option"
where
"cf2sfile s f \<equiv>
case (parent f) of
None \<Rightarrow> Some sroot
| Some pf \<Rightarrow> if (is_file s f)
then (case (sectxt_of_obj s (O_file f), sectxt_of_obj s (O_dir pf), get_parentfs_ctxts s pf) of
(Some sec, Some psec, Some asecs) \<Rightarrow>
Some (if (\<not> deleted (O_file f) s \<and> is_init_file f) then Init f else Created, sec, Some psec, set asecs)
| _ \<Rightarrow> None)
else (case (sectxt_of_obj s (O_dir f), sectxt_of_obj s (O_dir pf), get_parentfs_ctxts s pf) of
(Some sec, Some psec, Some asecs) \<Rightarrow>
Some (if (\<not> deleted (O_dir f) s \<and> is_init_dir f) then Init f else Created, sec, Some psec, set asecs)
| _ \<Rightarrow> None)"
definition cf2sfiles :: "t_state \<Rightarrow> t_file \<Rightarrow> t_sfile set"
where
"cf2sfiles s f \<equiv> {sf. \<exists> f' \<in> (same_inode_files s f). cf2sfile s f' = Some sf}"
(* here cf2sfile is passed with True, because, process' fds are only for files not dirs *)
definition cfd2sfd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd \<Rightarrow> t_sfd option"
where
"cfd2sfd s p fd \<equiv>
(case (file_of_proc_fd s p fd, flags_of_proc_fd s p fd, sectxt_of_obj s (O_fd p fd)) of
(Some f, Some flags, Some sec) \<Rightarrow> (case (cf2sfile s f) of
Some sf \<Rightarrow> Some (sec, flags, sf)
| _ \<Rightarrow> None)
| _ \<Rightarrow> None)"
definition cpfd2sfds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sfd set"
where
"cpfd2sfds s p \<equiv> {sfd. \<exists> fd \<in> proc_file_fds s p. cfd2sfd s p fd = Some sfd}"
definition ch2sshm :: "t_state \<Rightarrow> t_shm \<Rightarrow> t_sshm option"
where
"ch2sshm s h \<equiv> (case (sectxt_of_obj s (O_shm h)) of
Some sec \<Rightarrow>
Some (if (\<not> deleted (O_shm h) s \<and> h \<in> init_shms) then Init h else Created, sec)
| _ \<Rightarrow> None)"
definition cph2spshs :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sproc_sshm set"
where
"cph2spshs s p \<equiv> {(sh, flag)| sh flag h. (p, flag) \<in> procs_of_shm s h \<and> ch2sshm s h = Some sh}"
definition cp2sproc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sproc option"
where
"cp2sproc s p \<equiv> (case (sectxt_of_obj s (O_proc p)) of
Some sec \<Rightarrow>
Some (if (\<not> deleted (O_proc p) s \<and> p \<in> init_procs) then Init p else Created, sec,
cpfd2sfds s p, cph2spshs s p)
| _ \<Rightarrow> None)"
definition cm2smsg :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsg option"
where
"cm2smsg s q m \<equiv> (case (sectxt_of_obj s (O_msg q m)) of
Some sec \<Rightarrow>
Some (if (\<not> deleted (O_msg q m) s \<and> m \<in> set (init_msgs_of_queue q)) then Init m else Created,
sec, O_msg q m \<in> tainted s)
| _ \<Rightarrow> None)"
fun cqm2sms:: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg list \<Rightarrow> (t_smsg list) option"
where
"cqm2sms s q [] = Some []"
| "cqm2sms s q (m#ms) =
(case (cqm2sms s q ms, cm2smsg s q m) of
(Some sms, Some sm) \<Rightarrow> Some (sm#sms)
| _ \<Rightarrow> None)"
definition cq2smsgq :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_smsgq option"
where
"cq2smsgq s q \<equiv> (case (sectxt_of_obj s (O_msgq q), cqm2sms s q (msgs_of_queue s q)) of
(Some sec, Some sms) \<Rightarrow>
Some (if (\<not> deleted (O_msgq q) s \<and> q \<in> init_msgqs) then Init q else Created,
sec, sms)
| _ \<Rightarrow> None)"
fun co2sobj :: "t_state \<Rightarrow> t_object \<Rightarrow> t_sobject option"
where
"co2sobj s (O_proc p) =
(case (cp2sproc s p) of
Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))
| _ \<Rightarrow> None)"
| "co2sobj s (O_file f) =
Some (S_file (cf2sfiles s f) (O_file f \<in> tainted s))"
| "co2sobj s (O_dir f) =
(case (cf2sfile s f) of
Some sf \<Rightarrow> Some (S_dir sf)
| _ \<Rightarrow> None)"
| "co2sobj s (O_msgq q) =
(case (cq2smsgq s q) of
Some sq \<Rightarrow> Some (S_msgq sq)
| _ \<Rightarrow> None)"
| "co2sobj s (O_shm h) =
(case (ch2sshm s h) of
Some sh \<Rightarrow> Some (S_shm sh)
| _ \<Rightarrow> None)"
(*
| "co2sobj s (O_msg q m) =
(case (cq2smsgq s q, cm2smsg s q m) of
(Some sq, Some sm) \<Rightarrow> Some (S_msg sq sm)
| _ \<Rightarrow> None)"
*)
| "co2sobj s _ = None"
definition s2ss :: "t_state \<Rightarrow> t_static_state"
where
"s2ss s \<equiv> {sobj. \<exists> obj. alive s obj \<and> co2sobj s obj = Some sobj}"
(* ******************************************************** *)
fun is_init_sfile :: "t_sfile \<Rightarrow> bool"
where
"is_init_sfile (Init _, sec, psec,asec) = True"
| "is_init_sfile _ = False"
fun is_many_sfile :: "t_sfile \<Rightarrow> bool"
where
"is_many_sfile (Created, sec, psec, asec) = True"
| "is_many_sfile _ = False"
fun is_init_sproc :: "t_sproc \<Rightarrow> bool"
where
"is_init_sproc (Init p, sec, fds, shms) = True"
| "is_init_sproc _ = False"
fun is_many_sproc :: "t_sproc \<Rightarrow> bool"
where
"is_many_sproc (Created, sec,fds,shms) = True"
| "is_many_sproc _ = False"
fun is_many_smsg :: "t_smsg \<Rightarrow> bool"
where
"is_many_smsg (Created,sec,tag) = True"
| "is_many_smsg _ = False"
(* wrong def
fun is_many_smsgq :: "t_smsgq \<Rightarrow> bool"
where
"is_many_smsgq (Created,sec,sms) = (True \<and> (\<forall> sm \<in> (set sms). is_many_smsg sm))"
| "is_many_smsgq _ = False"
*)
fun is_many_smsgq :: "t_smsgq \<Rightarrow> bool"
where
"is_many_smsgq (Created,sec,sms) = True"
| "is_many_smsgq _ = False"
fun is_many_sshm :: "t_sshm \<Rightarrow> bool"
where
"is_many_sshm (Created, sec) = True"
| "is_many_sshm _ = False"
fun is_many :: "t_sobject \<Rightarrow> bool"
where
"is_many (S_proc sp tag) = is_many_sproc sp"
| "is_many (S_file sfs tag) = (\<forall> sf \<in> sfs. is_many_sfile sf)"
| "is_many (S_dir sf ) = is_many_sfile sf"
| "is_many (S_msgq sq ) = is_many_smsgq sq"
| "is_many (S_shm sh ) = is_many_sshm sh"
fun is_init_smsgq :: "t_smsgq \<Rightarrow> bool"
where
"is_init_smsgq (Init q,sec,sms) = True"
| "is_init_smsgq _ = False"
fun is_init_sshm :: "t_sshm \<Rightarrow> bool"
where
"is_init_sshm (Init h,sec) = True"
| "is_init_sshm _ = False"
fun is_init_sobj :: "t_sobject \<Rightarrow> bool"
where
"is_init_sobj (S_proc sp tag ) = is_init_sproc sp"
| "is_init_sobj (S_file sfs tag) = (\<exists> sf \<in> sfs. is_init_sfile sf)"
| "is_init_sobj (S_dir sf ) = is_init_sfile sf"
| "is_init_sobj (S_msgq sq ) = is_init_smsgq sq"
| "is_init_sobj (S_shm sh ) = is_init_sshm sh"
(*
fun update_ss_sp:: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state"
where
"update_ss_sp ss (S_proc sp tag) (S_proc sp' tag') =
(if (is_many_sproc sp) then ss \<union> {S_proc sp' tag'}
else (ss - {S_proc sp tag}) \<union> {S_proc sp' tag'})"
fun update_ss_sd:: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state"
where
"update_ss_sd ss (S_dir sf tag) (S_dir sf' tag') =
(if (is_many_sfile sf) then ss \<union> {S_dir sf' tag'}
else (ss - {S_dir sf tag}) \<union> {S_dir sf' tag'})"
*)
(*
fun sparent :: "t_sfile \<Rightarrow> t_sfile option"
where
"sparent (Sroot si sec) = None"
| "sparent (Sfile si sec spf) = Some spf"
inductive is_ancesf :: "t_sfile \<Rightarrow> t_sfile \<Rightarrow> bool"
where
"is_ancesf sf sf"
| "sparent sf = Some spf \<Longrightarrow> is_ancesf spf sf"
| "\<lbrakk>sparent sf = Some spf; is_ancesf saf spf\<rbrakk> \<Longrightarrow> is_ancesf saf sf"
definition sfile_reparent :: "t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile"
where
"sfile_reparent (Sroot)"
*)
(*
(* sfds rename aux definitions *)
definition sfds_rename_notrelated
:: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool"
where
"sfds_rename_notrelated sfds from to sfds' \<equiv>
(\<forall> sec flag sf. (sec,flag,sf) \<in> sfds \<and> (\<not> from \<preceq> sf) \<longrightarrow> (sec,flag,sf) \<in> sfds')"
definition sfds_rename_renamed
:: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool"
where
"sfds_rename_renamed sfds sf from to sfds' \<equiv>
(\<forall> sec flag sf'. (sec,flag,sf) \<in> sfds \<and> (sf \<preceq> sf') \<longrightarrow>
(sec, flag, file_after_rename sf' from to) \<in> sfds' \<and> (sec,flag,sf) \<notin> sfds')"
definition sfds_rename_remain
:: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool"
where
"sfds_rename_remain sfds sf from to sfds' \<equiv>
(\<forall> sec flag sf'. (sec,flag,sf') \<in> sfds \<and> (sf \<preceq> sf') \<longrightarrow>
(sec, flag, sf') \<in> sfds' \<and> (sec,flag, file_after_rename sf' from to) \<notin> sfds')"
(* for not many, choose on renamed or not *)
definition sfds_rename_choices
:: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool"
where
"sfds_rename_choices sfds sf from to sfds' \<equiv>
sfds_rename_remain sfds sf from to sfds' \<or> sfds_rename_renamed sfds sf from to sfds'"
(* for many, merge renamed with not renamed *)
definition sfds_rename_both
:: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool"
where
"sfds_rename_both sfds sf from to sfds' \<equiv>
(\<forall> sec flag sf'. (sec,flag,sf') \<in> sfds \<and> (sf \<preceq> sf') \<longrightarrow>
(sec, flag, sf') \<in> sfds' \<or> (sec,flag, file_after_rename sf' from to) \<in> sfds')"
(* added to the new sfds, are those only under the new sfile *)
definition sfds_rename_added
:: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool"
where
"sfds_rename_added sfds from to sfds' \<equiv>
(\<forall> sec' flag' sf' sec flag. (sec',flag',sf') \<in> sfds' \<and> (sec,flag,sf') \<notin> sfds \<longrightarrow>
(\<exists> sf. (sec,flag,sf) \<in> sfds \<and> sf' = file_after_rename from to sf))"
definition sproc_sfds_renamed
:: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
where
"sproc_sfds_renamed ss sf from to ss' \<equiv>
(\<forall> pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \<in> ss \<longrightarrow>
(\<exists> sfds'. S_proc (pi,sec,sfds',sshms) tagp \<in> ss \<and> sfds_rename_renamed sfds sf from to sfds'))"
definition sproc_sfds_remain
:: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
where
"sproc_sfds_remain ss sf from to ss' \<equiv>
(\<forall> pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \<in> ss \<longrightarrow>
(\<exists> sfds'. S_proc (pi,sec,sfds',sshms) tagp \<in> ss \<and> sfds_rename_remain sfds sf from to sfds'))"
(* for not many, choose on renamed or not *)
definition sproc_sfds_choices
:: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
where
"sproc_sfds_choices ss sf from to ss' \<equiv>
(\<forall> pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \<in> ss \<longrightarrow>
(\<exists> sfds'. S_proc (pi,sec,sfds',sshms) tagp \<in> ss \<and> sfds_rename_choices sfds sf from to sfds'))"
(* for many, merge renamed with not renamed *)
definition sproc_sfds_both
:: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
where
"sproc_sfds_both ss sf from to ss' \<equiv>
(\<forall> pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \<in> ss \<longrightarrow>
(\<exists> sfds'. S_proc (pi,sec,sfds',sshms) tagp \<in> ss \<and> sfds_rename_both sfds sf from to sfds'))"
(* remove (\<forall> sp tag. S_proc sp tag \<in> ss \<longrightarrow> S_proc sp tag \<in> ss'),
* cause sfds contains sfs informations *)
definition ss_rename_notrelated
:: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
where
"ss_rename_notrelated ss sf sf' ss' \<equiv>
(\<forall> sq. S_msgq sq \<in> ss \<longrightarrow> S_msgq sq \<in> ss') \<and>
(\<forall> pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \<in> ss \<longrightarrow> (\<exists> sfds'.
S_proc (pi,sec,sfds',sshms) tagp \<in> ss'\<and> sfds_rename_notrelated sfds sf sf' sfds')) \<and>
(\<forall> sfs sf'' tag. S_file sfs tag \<in> ss \<and> sf'' \<in> sfs \<and> (\<not> sf \<preceq> sf'') \<longrightarrow> (\<exists> sfs'.
S_file sfs tag \<in> ss' \<and> sf'' \<in> sfs')) \<and>
(\<forall> sf'' tag. S_dir sf'' tag \<in> ss \<and> (\<not> sf \<preceq> sf'') \<longrightarrow> S_dir sf'' tag \<in> ss')"
(* rename from to, from should definited renamed if not many *)
definition all_descendant_sf_renamed
:: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
where
"all_descendant_sf_renamed ss sf from to ss' \<equiv>
(\<forall> sfs sf' tagf. sf \<preceq> sf' \<and> S_file sfs tagf \<in> ss \<and> sf' \<in> sfs \<longrightarrow> (\<exists> sfs'.
S_file sfs' tagf \<in> ss' \<and> file_after_rename from to sf' \<in> sfs' \<and> sf' \<notin> sfs')) \<and>
(\<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>
sproc_sfds_renamed ss sf from to ss'"
(* not renamed *)
definition all_descendant_sf_remain
:: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
where
"all_descendant_sf_remain ss sf from to ss' \<equiv>
(\<forall> sfs sf' tag'. sf \<preceq> sf' \<and> S_file sfs tag' \<in> ss \<and> sf' \<in> sfs \<longrightarrow> (\<exists> sfs'.
S_file sfs' tag' \<in> ss \<and> file_after_rename from to sf' \<notin> sfs' \<and> sf' \<in> sfs')) \<and>
(\<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>
sproc_sfds_remain ss sf from to ss'"
definition all_descendant_sf_choices
:: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
where
"all_descendant_sf_choices ss sf from to ss' \<equiv>
all_descendant_sf_renamed ss sf from to ss' \<or> all_descendant_sf_remain ss sf from to ss'"
definition all_descendant_sf_both
:: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
where
"all_descendant_sf_both ss sf from to ss' \<equiv>
(\<forall> sfs sf' tag'. sf \<preceq> sf' \<and> S_file sfs tag' \<in> ss \<and> sf' \<in> sfs \<longrightarrow> (\<exists> sfs'.
S_file sfs' tag' \<in> ss \<and> file_after_rename from to sf' \<in> sfs' \<or> sf' \<in> sfs')) \<and>
(\<forall> sf' tag'. sf \<preceq> sf' \<and> S_dir sf' tag' \<in> ss \<longrightarrow>
S_dir (file_after_rename from to sf') tag' \<in> ss' \<or> S_dir sf' tag' \<in> ss') \<and>
sproc_sfds_both ss sf from to ss'"
definition ss_renamed_file
:: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
where
"ss_renamed_file ss sf sf' ss' \<equiv>
(if (is_many_sfile sf)
then all_descendant_sf_choices ss sf sf sf' ss'
else all_descendant_sf_renamed ss sf sf sf' ss')"
(* added to the new sfs, are those only under the new sfile *)
definition sfs_rename_added
:: "t_sfile set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile set \<Rightarrow> bool"
where
"sfs_rename_added sfs from to sfs' \<equiv>
(\<forall> sf'. sf' \<in> sfs' \<and> sf' \<notin> sfs \<longrightarrow> (\<exists> sf. sf \<in> sfs \<and> sf' = file_after_rename from to sf))"
(* added to the new sfile, are those only under the new sfile *)
definition ss_rename_added
:: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
where
"ss_rename_added ss from to ss' \<equiv>
(\<forall> pi sec fds fds' shms tagp. S_proc (pi, sec, fds,shms) tagp \<in> ss \<and>
S_proc (pi,sec,fds',shms) tagp \<in> ss' \<longrightarrow> sfds_rename_added fds from to fds') \<and>
(\<forall> sq. S_msgq sq \<in> ss' \<longrightarrow> S_msgq sq \<in> ss) \<and>
(\<forall> sfs sfs' tagf. S_file sfs' tagf \<in> ss' \<and> S_file sfs tagf \<in> ss \<longrightarrow>
sfs_rename_added sfs from to sfs') \<and>
(\<forall> sf' tagf. S_dir sf' tagf \<in> ss' \<and> S_dir sf' tagf \<notin> ss \<longrightarrow>
(\<exists> sf. S_dir sf tagf \<in> ss \<and> sf' = file_after_rename from to sf))"
definition sfile_alive :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> bool"
where
"sfile_alive ss sf \<equiv> (\<exists> sfs tagf. sf \<in> sfs \<and> S_file sfs tagf \<in> ss)"
definition sf_alive :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> bool"
where
"sf_alive ss sf \<equiv> (\<exists> tagd. S_dir sf tagd \<in> ss) \<or> sfile_alive ss sf"
(* constrains that the new static state should satisfy *)
definition ss_rename:: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
where
"ss_rename ss sf sf' ss' \<equiv>
ss_rename_notrelated ss sf sf' ss' \<and>
ss_renamed_file ss sf sf' ss' \<and> ss_rename_added ss sf sf' ss' \<and>
(\<forall> sf''. sf_alive ss sf'' \<and> sf \<prec> sf'' \<longrightarrow>
(if (is_many_sfile sf'')
then all_descendant_sf_choices ss sf'' sf sf' ss'
else all_descendant_sf_both ss sf'' sf sf' ss'))"
(* two sfile, the last fname should not be equal *)
fun sfile_same_fname:: "t_sfile \<Rightarrow> t_sfile \<Rightarrow> bool"
where
"sfile_same_fname ((Init n, sec)#spf) ((Init n', sec')#spf') = (n = n')"
| "sfile_same_fname _ _ = False"
(* no same init sfile/only sfile in the target-to spf, should be in static_state addmissble check *)
definition ss_rename_no_same_fname:: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> bool"
where
"ss_rename_no_same_fname ss from spf \<equiv>
\<not> (\<exists> to. sfile_same_fname from to \<and> parent to = Some spf \<and> sf_alive ss to)"
(* is not a function, is a relation (one 2 many)
definition update_ss_rename :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state"
where
"update_ss_rename ss sf sf' \<equiv> if (is_many_sfile sf)
then (ss \<union> {S_file (file_after_rename sf sf' sf'') tag | sf'' tag. sf \<preceq> sf'' \<and> S_file sf'' tag \<in> ss}
\<union> {S_dir (file_after_rename sf sf' sf'') tag | sf'' tag. sf \<preceq> sf'' \<and> S_dir sf'' tag \<in> ss})
else (ss - {S_file sf'' tag | sf'' tag. sf \<preceq> sf'' \<and> S_file sf'' tag \<in> ss}
- {S_dir sf'' tag | sf'' tag. sf \<preceq> sf'' \<and> S_dir sf'' tag \<in> ss})
\<union> {S_file (file_after_rename sf sf' sf'') tag | sf'' tag. sf \<preceq> sf'' \<and> S_file sf'' tag \<in> ss}
\<union> {S_dir (file_after_rename sf sf' sf'') tag | sf'' tag. sf \<preceq> sf'' \<and> S_dir sf'' tag \<in> ss}"
*)
*)
fun sectxt_of_sproc :: "t_sproc \<Rightarrow> security_context_t"
where
"sectxt_of_sproc (pi,sec,fds,shms) = sec"
fun sectxt_of_sfile :: "t_sfile \<Rightarrow> security_context_t"
where
"sectxt_of_sfile (fi,sec,psec,asecs) = sec"
fun asecs_of_sfile :: "t_sfile \<Rightarrow> security_context_t set"
where
"asecs_of_sfile (fi,sec,psec,asecs) = asecs"
definition search_check_s :: "security_context_t \<Rightarrow> t_sfile \<Rightarrow> bool \<Rightarrow> bool"
where
"search_check_s pctxt sf if_file =
(if if_file
then search_check_ctxt pctxt (sectxt_of_sfile sf) (asecs_of_sfile sf) True
else search_check_ctxt pctxt (sectxt_of_sfile sf) (asecs_of_sfile sf) False)"
definition sectxts_of_sfds :: "t_sfd set \<Rightarrow> security_context_t set"
where
"sectxts_of_sfds sfds \<equiv> {ctxt. \<exists> flag sf. (ctxt, flag, sf) \<in> sfds}"
definition inherit_fds_check_s :: "security_context_t \<Rightarrow> t_sfd set \<Rightarrow> bool"
where
"inherit_fds_check_s pctxt sfds \<equiv> inherit_fds_check_ctxt pctxt (sectxts_of_sfds sfds)"
definition sectxts_of_sproc_sshms :: "t_sproc_sshm set \<Rightarrow> security_context_t set"
where
"sectxts_of_sproc_sshms sshms \<equiv> {ctxt. \<exists> hi flag. ((hi, ctxt),flag) \<in> sshms}"
definition inherit_shms_check_s :: "security_context_t \<Rightarrow> t_sproc_sshm set \<Rightarrow> bool"
where
"inherit_shms_check_s pctxt sshms \<equiv> inherit_shms_check_ctxt pctxt (sectxts_of_sproc_sshms sshms)"
(*
fun info_flow_sshm :: "t_sproc \<Rightarrow> t_sproc \<Rightarrow> bool"
where
"info_flow_sshm (pi,sec,fds,shms) (pi',sec',fds',shms') =
(\<exists> sh flag'. (sh, SHM_RDWR) \<in> shms \<and> (sh, flag') \<in> shms')"
*)
definition info_flow_sproc_sshms :: "t_sproc_sshm set \<Rightarrow> t_sproc_sshm set \<Rightarrow> bool"
where
"info_flow_sproc_sshms shms shms' \<equiv> (\<exists> sh flag'. (sh, SHM_RDWR) \<in> shms \<and> (sh, flag') \<in> shms')"
(*
fun info_flow_sshm :: "t_sproc \<Rightarrow> t_sproc \<Rightarrow> bool"
where
"info_flow_sshm (pi,sec,fds,shms) (pi',sec',fds',shms') = info_flow_sproc_sshms shms shms'"
*)
inductive info_flow_sshm :: "t_sproc \<Rightarrow> t_sproc \<Rightarrow> bool"
where
"info_flow_sshm sp sp"
| "\<lbrakk>info_flow_sshm sp (pi,sec,fds,shms); info_flow_sproc_sshms shms shms'\<rbrakk>
\<Longrightarrow> info_flow_sshm sp (pi',sec',fds',shms')"
(*
fun smsg_related :: "t_msg \<Rightarrow> t_smsg list \<Rightarrow> bool"
where
"smsg_related m [] = False"
| "smsg_related m ((mi, sec, tag)#sms) =
(if (mi = Init m) then True else smsg_related m sms)"
fun smsgq_smsg_related :: "t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsgq \<Rightarrow> bool"
where
"smsgq_smsg_related q m (qi, sec, smsgslist) = ((qi = Init q) \<and> (smsg_related m smsgslist))"
fun smsg_relatainted :: "t_msg \<Rightarrow> t_smsg list \<Rightarrow> bool"
where
"smsg_relatainted m [] = False"
| "smsg_relatainted m ((mi, sec, tag)#sms) =
(if (mi = Init m \<and> tag = True) then True else smsg_relatainted m sms)"
fun smsgq_smsg_relatainted :: "t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsgq \<Rightarrow> bool"
where
"smsgq_smsg_relatainted q m (qi, sec, smsgslist) =
((qi = Init q) \<and> (smsg_relatainted m smsgslist))"
*)
fun sfile_related :: "t_sfile \<Rightarrow> t_file \<Rightarrow> bool"
where
"sfile_related (fi,sec,psec,asecs) f = (fi = Init f)"
(*
fun sproc_related :: "t_process \<Rightarrow> t_sproc \<Rightarrow> bool"
where
"sproc_related p (pi, sec, fds, shms) = (pi = Init p)"
*)
fun init_obj_related :: "t_sobject \<Rightarrow> t_object \<Rightarrow> bool"
where
"init_obj_related (S_proc (pi, sec, fds, shms) tag) (O_proc p') = (pi = Init p')"
| "init_obj_related (S_file sfs tag) (O_file f) = (\<exists> sf \<in> sfs. sfile_related sf f)"
| "init_obj_related (S_dir sf) (O_dir f) = (sfile_related sf f)"
| "init_obj_related (S_msgq (qi, sec, sms)) (O_msgq q') = (qi = Init q')"
| "init_obj_related (S_shm (hi, sec)) (O_shm h') = (hi = Init h')"
(*
| "init_obj_related (S_msg (qi, sec, sms) (mi, secm, tagm)) (O_msg q' m') = (qi = Init q' \<and> mi = Init m')"
*)
| "init_obj_related _ _ = False"
(***************** for backward proof when Instancing static objects ******************)
definition next_nat :: "nat set \<Rightarrow> nat"
where
"next_nat nset = (Max nset) + 1"
definition new_proc :: "t_state \<Rightarrow> t_process"
where
"new_proc \<tau> = next_nat (current_procs \<tau>)"
definition new_inode_num :: "t_state \<Rightarrow> nat"
where
"new_inode_num \<tau> = next_nat (current_inode_nums \<tau>)"
definition new_msgq :: "t_state \<Rightarrow> t_msgq"
where
"new_msgq s = next_nat (current_msgqs s)"
definition new_msg :: "t_state \<Rightarrow> t_msgq \<Rightarrow> nat"
where
"new_msg s q = next_nat (set (msgs_of_queue s q))"
definition new_shm :: "t_state \<Rightarrow> nat"
where
"new_shm \<tau> = next_nat (current_shms \<tau>)"
definition new_proc_fd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd"
where
"new_proc_fd \<tau> p = next_nat (current_proc_fds \<tau> p)"
definition all_fname_under_dir:: "t_file \<Rightarrow> t_state \<Rightarrow> t_fname set"
where
"all_fname_under_dir d \<tau> = {fn. \<exists> f. fn # d = f \<and> f \<in> current_files \<tau>}"
fun fname_all_a:: "nat \<Rightarrow> t_fname"
where
"fname_all_a 0 = []" |
"fname_all_a (Suc n) = ''a''@(fname_all_a n)"
definition fname_length_set :: "t_fname set \<Rightarrow> nat set"
where
"fname_length_set fns = length`fns"
definition next_fname:: "t_file \<Rightarrow> t_state \<Rightarrow> t_fname"
where
"next_fname pf \<tau> = fname_all_a ((Max (fname_length_set (all_fname_under_dir pf \<tau>))) + 1)"
definition new_childf:: "t_file \<Rightarrow> t_state \<Rightarrow> t_file"
where
"new_childf pf \<tau> = next_fname pf \<tau> # pf"
end
end