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) = +
−
     (if (f \<in> init_files \<and> is_init_file f) +
−
      then Some (S_file (init_cf2sfiles f) +
−
                        (\<exists> f'. f' \<in> (init_same_inode_files f) \<and> O_file f \<in> seeds))+
−
      else None)"+
−
| "init_obj2sobj (O_dir f) = +
−
     (if (is_init_dir f) then +
−
        (case (init_cf2sfile f) of+
−
           Some sf \<Rightarrow> Some (S_dir sf) +
−
         | _ \<Rightarrow> None)+
−
      else 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}"+
−
+
−
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"+
−
+
−
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_sshm :: "t_sshm \<Rightarrow> bool"+
−
where+
−
  "is_many_sshm (Created, sec) = True"+
−
| "is_many_sshm _              = False"+
−
+
−
(*+
−
fun is_init_sobj :: "t_sobject \<Rightarrow> bool"+
−
where+
−
  "is_init_sobj (S_proc (popt, sec, fds, shms) tag) = (popt \<noteq> None)"+
−
| "is_init_sobj (S_file sf tag) = (is_init_sfile sf)"+
−
| "is_init_sobj (S_dir  sf tag) = (is_init_sfile sf)"+
−
| "is_init_sobj (S_msg" *)+
−
+
−
fun is_many :: "t_sobject \<Rightarrow> bool"+
−
where+
−
  "is_many (S_proc (Many, sec, fds, shms) tag) = True"+
−
| "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 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'})"+
−
*)+
−
+
−
definition update_ss :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state"+
−
where+
−
  "update_ss ss so so' \<equiv> if (is_many so) then ss \<union> {so'} else (ss - {so}) \<union> {so'}"+
−
+
−
definition add_ss :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_static_state"+
−
where+
−
  "add_ss ss so \<equiv> ss \<union> {so}"+
−
+
−
definition del_ss :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_static_state"+
−
where+
−
  "del_ss ss so \<equiv> if (is_many so) then ss else ss - {so}"+
−
+
−
(*+
−
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_file pctxt (sectxt_of_sfile sf) \<and> search_check_allp pctxt (asecs_of_sfile sf)+
−
      else search_check_dir  pctxt (sectxt_of_sfile sf) \<and> search_check_allp pctxt (asecs_of_sfile sf))"+
−
+
−
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> +
−
     (\<forall> ctxt \<in> sectxts_of_sfds sfds. permission_check pctxt ctxt C_fd P_inherit)"+
−
+
−
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> +
−
     (\<forall> ctxt \<in> sectxts_of_sproc_sshms sshms. permission_check pctxt ctxt C_shm P_inherit)"+
−
+
−
(*+
−
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')"+
−
+
−
definition update_ss_shms :: "t_static_state \<Rightarrow> t_sproc \<Rightarrow> bool \<Rightarrow> t_static_state"+
−
where+
−
  "update_ss_shms ss spfrom tag \<equiv> {sobj. \<exists> sobj' \<in> ss. +
−
     (case sobj' of +
−
        S_proc sp tagp \<Rightarrow> if (info_flow_sshm spfrom sp) +
−
                          then if (is_many_sproc sp)+
−
                               then (sobj = S_proc sp tagp \<or> sobj = S_proc sp (tagp \<or> tag))+
−
                               else (sobj = S_proc sp (tagp \<or> tag))+
−
                          else (sobj = S_proc sp tag)+
−
     | _ \<Rightarrow> sobj = sobj')}"+
−
+
−
+
−
+
−
(* all reachable static states(sobjects set) *)+
−
inductive_set static :: "t_static_state set"+
−
where+
−
  s_init:    "init_static_state \<in> static"+
−
| s_execve:  "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; S_file sfs tagf \<in> ss;+
−
               (fi,fsec,pfsec,asecs) \<in> sfs; npctxt_execve pctxt fsec = Some pctxt';+
−
               grant_execve pctxt fsec pctxt'; search_check_s pctxt (fi,fsec,pfsec,asecs) True; +
−
               inherit_fds_check_s pctxt' fds'; fds' \<subseteq> fds\<rbrakk>+
−
  \<Longrightarrow> (update_ss ss (S_proc (pi, pctxt, fds, shms) tagp) +
−
                    (S_proc (pi, pctxt', fds', {}) (tagp \<or> tagf))) \<in> static"+
−
| s_clone:   "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; +
−
               permission_check pctxt pctxt C_process P_fork;+
−
               inherit_fds_check_s pctxt fds'; fds' \<subseteq> fds; +
−
               inherit_shms_check_s pctxt shms'; shms' \<subseteq> shms\<rbrakk>+
−
  \<Longrightarrow> (add_ss ss (S_proc (Created, pctxt, fds', shms') tagp)) \<in> static"+
−
| s_kill:    "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; +
−
               S_proc (pi', pctxt', fds', shms') tagp' \<in> ss; +
−
               permission_check pctxt pctxt' C_process P_sigkill\<rbrakk>+
−
  \<Longrightarrow> (del_ss ss (S_proc (pi', pctxt', fds', shms') tagp')) \<in> static"+
−
| s_ptrace:  "\<lbrakk>ss \<in> static; S_proc sp tagp \<in> ss; S_proc sp' tagp' \<in> ss; +
−
               permission_check (sextxt_of_sproc sp) (sectxt_of_sproc sp') C_process P_ptrace\<rbrakk>+
−
  \<Longrightarrow> (update_ss_shms (update_ss_shms ss sp tagp) sp' tagp') \<in> static"+
−
| s_exit:    "\<lbrakk>ss \<in> static; S_proc sp tagp \<in> ss\<rbrakk> \<Longrightarrow> (del_ss ss (S_proc sp tagp)) \<in> static"+
−
| s_open:    "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; S_file sfs tagf \<in> ss; sf \<in> sfs;+
−
              search_check_s pctxt sf True; \<not> is_creat_excl_flag flags; +
−
              oflags_check flags pctxt (sectxt_of_sfile sf); permission_check pctxt pctxt C_fd P_setattr\<rbrakk>+
−
  \<Longrightarrow> (update_ss ss (S_proc (pi, pctxt, fds, shms) tagp)+
−
                    (S_proc (pi, pctxt, fds \<union> {(pctxt,flags,sf)}, shms) tagp)) \<in> static"+
−
| s_open':   "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; is_creat_excl_flag flags;+
−
               S_dir (pfi,fsec,pfsec,asecs) \<in> ss; search_check_s pctxt (pfi,fsec,pfsec,asecs) False; +
−
               nfsec = nfctxt_create pctxt fsec C_file; oflags_check flags pctxt nfsec;+
−
               permission_check pctxt fsec C_dir P_add_rename; permission_check pctxt pctxt C_fd P_setattr\<rbrakk>+
−
  \<Longrightarrow> (update_ss (add_ss ss (S_file {(Created, nfsec, Some fsec, asecs \<union> {fsec})} tagp))+
−
         (S_proc (pi, pctxt, fds, shms) tagp)+
−
         (S_proc (pi, pctxt, fds \<union> {(pctxt, flags, (Created, nfsec, Some fsec, asecs \<union> {fsec}))}, shms) tagp)+
−
      ) \<in> static"+
−
| S_readf:   "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; (fdctxt,flags,sf) \<in> fds; +
−
               permission_check pctxt fdctxt C_fd P_setattr; S_file sfs tagf \<in> ss; sf \<in> sfs;+
−
               permission_check pctxt (sectxt_of_sfile sf) C_file P_read; is_read_flag flags\<rbrakk>+
−
  \<Longrightarrow> (update_ss_shms ss (pi, pctxt,fds,shms) (tagp \<or> tagf)) \<in> static"+
−
| S_writef:  "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; (fdctxt,flags,sf) \<in> fds; +
−
               permission_check pctxt fdctxt C_fd P_setattr; sf \<in> sfs; S_file sfs tagf \<in> ss; +
−
               permission_check pctxt (sectxt_of_sfile sf) C_file P_write; is_write_flag flags\<rbrakk>+
−
  \<Longrightarrow> (update_ss ss (S_file sfs tagf) (S_file sfs (tagp \<or> tagf))) \<in> static"+
−
| S_unlink:  "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_file sfs tagf \<in> ss;  +
−
               (Init f,fsec,Some pfsec,asecs) \<in> sfs; +
−
               search_check_s pctxt (Init f,fsec,Some pfsec,asecs) True; +
−
               permission_check pctxt fsec C_file P_unlink; +
−
               permission_check pctxt pfsec C_dir P_remove_name\<rbrakk>+
−
  \<Longrightarrow> ((ss - {S_file sfs tagf}) \<union> {S_file (sfs - {(Init f,fsec,Some pfsec,asecs)}) tagf}) \<in> static"+
−
| S_rmdir:   "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; +
−
               S_dir (fi,fsec,Some pfsec,asecs) \<in> ss;  +
−
               search_check_s pctxt (fi,fsec,Some pfsec,asecs) False; +
−
               permission_check pctxt fsec C_dir P_rmdir;+
−
               permission_check pctxt pfsec C_dir P_remove_name\<rbrakk>+
−
  \<Longrightarrow> (del_ss ss (S_dir (fi,fsec,Some pfsec,asecs))) \<in> static"+
−
| S_mkdir:   "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_dir (fi,fsec,pfsec,asecs) \<in> ss;  +
−
               search_check_s pctxt (fi,fsec,pfsec,asecs) False; +
−
               permission_check pctxt (nfctxt_create pctxt fsec C_dir) C_dir P_create;+
−
               permission_check pctxt fsec C_dir P_add_name\<rbrakk>+
−
  \<Longrightarrow> (add_ss ss (S_dir (Created,nfctxt_create pctxt fsec C_dir,Some fsec,asecs \<union> {fsec}))) \<in> static"+
−
| s_link:    "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_dir (pfi,pfsec,ppfsec,asecs) \<in> ss;+
−
               S_file sfs tagf \<in> ss; sf \<in> sfs; nfsec = nfctxt_create pctxt pfsec C_file;  +
−
               search_check_s pctxt (pfi,pfsec,ppfsec,asecs) False; search_check_s pctxt sf True;+
−
               permission_check pctxt (sectxt_of_sfile sf) C_file P_link; +
−
               permission_check pctxt pfsec C_dir P_add_name\<rbrakk>+
−
  \<Longrightarrow> (update_ss ss (S_file sfs tagf) +
−
                  (S_file (sfs \<union> {(Created,nfsec,Some pfsec, asecs \<union> {pfsec})}) tagf)) \<in> static"+
−
| s_trunc:   "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_file sfs tagf \<in> ss; sf \<in> sfs; +
−
               search_check_s pctxt sf True; permission_check pctxt (sectxt_of_sfile sf) C_file P_setattr\<rbrakk>+
−
  \<Longrightarrow> (update_ss ss (S_file sfs tagf) (S_file sfs (tagf \<or> tagp))) \<in> static"+
−
(*+
−
| s_rename:  "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_file sfs tagf \<in> ss;+
−
               (sf#spf') \<in> sfs; S_dir spf tagpf \<in> ss; \<not>((sf#spf') \<preceq> (sf#spf)); +
−
               search_check_s pctxt spf False; search_check_s pctxt (sf#spf') True; +
−
               sectxt_of_sfile (sf#spf') = Some fctxt; sectxt_of_sfile spf = Some pfctxt;  +
−
               permission_check pctxt fctxt C_file P_rename;+
−
               permission_check pctxt pfctxt C_dir P_add_name;+
−
               ss_rename ss (sf#spf') (sf#spf) ss'; +
−
               ss_rename_no_same_fname ss (sf#spf') (sf#spf)\<rbrakk>+
−
              \<Longrightarrow> ss' \<in> static"+
−
| s_rename': "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_dir (sf#spf') tagf \<in> ss;+
−
               S_dir spf tagpf \<in> ss; \<not>((sf#spf') \<preceq> (sf#spf)); +
−
               search_check_s pctxt spf False; search_check_s pctxt (sf#spf') True; +
−
               sectxt_of_sfile (sf#spf') = Some fctxt; sectxt_of_sfile spf = Some pfctxt;  +
−
               permission_check pctxt fctxt C_dir P_reparent;+
−
               permission_check pctxt pfctxt C_dir P_add_name;+
−
               ss_rename ss (sf#spf') (sf#spf) ss'; +
−
               ss_rename_no_same_fname ss (sf#spf') (sf#spf)\<rbrakk>+
−
              \<Longrightarrow> ss' \<in> static"+
−
*)+
−
| s_createq: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; +
−
               permission_check pctxt pctxt C_msgq P_associate;+
−
               permission_check pctxt pctxt C_msgq P_create\<rbrakk>+
−
  \<Longrightarrow> (add_ss ss (S_msgq (Created,pctxt,[]))) \<in> static" +
−
| s_sendmsg: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_msgq (qi,qctxt,sms) \<in> ss;+
−
               permission_check pctxt qctxt C_msgq P_enqueue;+
−
               permission_check pctxt qctxt C_msgq P_write; +
−
               permission_check pctxt pctxt C_msg  P_create\<rbrakk>+
−
  \<Longrightarrow> (update_ss ss (S_msgq (qi,qctxt,sms)) +
−
                    (S_msgq (qi,qctxt,sms @ [(Created, pctxt, tagp)]))) \<in> static"+
−
| s_recvmsg: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; +
−
               S_msgq (qi,qctxt,(mi,mctxt,tagm)#sms) \<in> ss;+
−
               permission_check pctxt qctxt C_msgq P_read; +
−
               permission_check pctxt mctxt C_msg  P_receive\<rbrakk>+
−
  \<Longrightarrow> (update_ss_shms ss (pi,pctxt,fds,shms) (tagp \<or> tagm)) \<in> static"+
−
| s_removeq: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_msgq (qi,qctxt,sms) \<in> ss;+
−
               permission_check pctxt qctxt C_msgq P_destroy\<rbrakk>+
−
  \<Longrightarrow> (del_ss ss (S_msgq (qi,qctxt,sms))) \<in> static"+
−
| s_createh: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss;+
−
               permission_check pctxt pctxt C_shm P_associate; +
−
               permission_check pctxt pctxt C_shm P_create\<rbrakk>+
−
   \<Longrightarrow> (add_ss ss (S_shm (Created, pctxt))) \<in> static"+
−
| s_attach:  "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_shm (hi,hctxt) \<in> ss;+
−
               if flag = SHM_RDONLY then permission_check pctxt hctxt C_shm P_read+
−
               else (permission_check pctxt hctxt C_shm P_read \<and>+
−
                     permission_check pctxt hctxt C_shm P_write)\<rbrakk>+
−
   \<Longrightarrow> (update_ss ss (S_proc (pi,pctxt,fds,shms) tagp)+
−
                    (S_proc (pi,pctxt,fds,shms \<union> {((hi,hctxt),flag)}) tagp)) \<in> static"+
−
| s_detach:  "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_shm sh \<in> ss;+
−
               (sh,flag) \<in> shms; \<not> is_many_sshm sh\<rbrakk>+
−
   \<Longrightarrow> (update_ss ss (S_proc (pi,pctxt,fds,shms) tagp)+
−
                    (S_proc (pi,pctxt,fds,shms - {(sh,flag)}) tagp)) \<in> static"+
−
| s_deleteh: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_shm (hi,hctxt) \<in> ss;+
−
               permission_check pctxt hctxt C_shm P_destroy; \<not> is_many_sshm sh\<rbrakk>+
−
   \<Longrightarrow> (remove_sproc_sshm (del_ss ss (S_shm (hi,hctxt))) (hi,hctxt)) \<in> static"+
−
+
−
(*+
−
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"+
−
+
−
fun tainted_s :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> bool"+
−
where+
−
  "tainted_s ss (S_proc sp  tag) = (S_proc sp tag  \<in> ss \<and> tag = True)"+
−
| "tainted_s ss (S_file sfs tag) = (S_file sfs tag \<in> ss \<and> tag = True)"+
−
| "tainted_s ss (S_msg  (qi, sec, sms)  (mi, secm, tag)) = +
−
     (S_msgq (qi, sec, sms) \<in> ss \<and> (mi,secm,tag) \<in> set sms \<and> tag = True)"+
−
| "tainted_s ss _ = False"+
−
+
−
(*+
−
fun tainted_s :: "t_object \<Rightarrow> t_static_state \<Rightarrow> bool"+
−
where +
−
  "tainted_s (O_proc p)  ss = (\<exists> sp. S_proc sp True \<in> ss \<and> sproc_related p sp)"+
−
| "tainted_s (O_file f)  ss = (\<exists> sfs sf. S_file sfs True \<in> ss \<and> sf \<in> sfs \<and> sfile_related f sf)"+
−
| "tainted_s (O_msg q m) ss = (\<exists> sq. S_msgq sq \<in> ss \<and> smsgq_smsg_relatainted q m sq)"+
−
| "tainted_s _           ss = False"+
−
*)+
−
+
−
definition taintable_s :: "t_object \<Rightarrow> bool"+
−
where+
−
  "taintable_s obj \<equiv> \<exists> ss \<in> static. \<exists> sobj. tainted_s ss sobj \<and> init_obj_related sobj obj \<and> init_alive obj"+
−
+
−
definition deletable_s :: "t_object \<Rightarrow> bool"+
−
where+
−
  "deletable_s obj \<equiv> init_alive obj \<and> (\<exists> ss \<in> static. \<forall> sobj \<in> ss. \<not> init_obj_related sobj obj)"+
−
+
−
definition undeletable_s :: "t_object \<Rightarrow> bool"+
−
where+
−
  "undeletable_s obj \<equiv> init_alive obj \<and> (\<forall> ss \<in> static. \<exists> sobj \<in> ss. init_obj_related sobj obj)"+
−
+
−
+
−
(**************** 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) = +
−
     (if (f \<in> current_files s) then +
−
        Some (S_file (cf2sfiles s f) (O_file f \<in> tainted s))+
−
      else None)"+
−
| "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"+
−
+
−
+
−
(***************** 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"+
−
+
−
definition s2ss :: "t_state \<Rightarrow> t_static_state"+
−
where+
−
  "s2ss s \<equiv> {sobj. \<exists> obj. alive s obj \<and> co2sobj s obj = Some sobj}"+
−
+
−
end+
−
+
−
end+
−