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;