(*<*)

theory Co2sobj_prop

begin

(*<*)

context tainting_s begin

(****************** cf2sfile path simpset ***************)

lemma sroot_only:

  "cf2sfile s [] = Some sroot"

by (simp add:cf2sfile_def)

lemma not_file_is_dir:

  "\<lbrakk>\<not> is_file s f; f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> is_dir s f"

by (auto simp:is_file_def current_files_def is_dir_def 

         dest:finum_has_itag finum_has_ftag' split:t_inode_tag.splits option.splits)

lemma not_dir_is_file:

  "\<lbrakk>\<not> is_dir s f; f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> is_file s f"

by (auto simp:is_file_def current_files_def is_dir_def 

         dest:finum_has_itag finum_has_ftag' split:t_inode_tag.splits option.splits)

lemma is_file_or_dir:

  "\<lbrakk>f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> is_file s f \<or> is_dir s f"

by (auto dest:not_dir_is_file)

lemma current_file_has_sfile:

  "\<lbrakk>f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> \<exists> sf. cf2sfile s f = Some sf"

apply (induct f)

apply (rule_tac x = "sroot" in exI, simp add:sroot_only)

apply (frule parentf_in_current', simp, clarsimp)

apply (frule parentf_is_dir'', simp)

apply (frule is_file_or_dir, simp)

apply (auto dest!:current_has_sec'

            simp:cf2sfile_def split:option.splits if_splits dest!:get_pfs_secs_prop')

done

definition sectxt_of_pf :: "t_state \<Rightarrow> t_file \<Rightarrow> security_context_t option"

where

  "sectxt_of_pf s f = (case f of [] \<Rightarrow> None | (a # pf) \<Rightarrow> sectxt_of_obj s (O_dir pf))"

definition get_parentfs_ctxts' :: "t_state \<Rightarrow> t_file \<Rightarrow> (security_context_t list) option"

where

  "get_parentfs_ctxts' s f = (case f of [] \<Rightarrow> None | (a # pf) \<Rightarrow> get_parentfs_ctxts s pf)"

lemma is_file_has_sfile:

  "\<lbrakk>is_file s f; valid s\<rbrakk> \<Longrightarrow> \<exists> sec psec asecs. cf2sfile s f = Some 

      (if (\<not> deleted (O_file f) s \<and> is_init_file f) then Init f else Created,

       sec, Some psec, set asecs) \<and> (sectxt_of_obj s (O_file f) = Some sec) \<and>

       (sectxt_of_pf s f = Some psec) \<and> (get_parentfs_ctxts' s f = Some asecs)"

apply (case_tac f, simp, drule root_is_dir', simp, simp)

apply (frule is_file_in_current)

apply (drule current_file_has_sfile, simp)

apply (auto simp:cf2sfile_def sectxt_of_pf_def get_parentfs_ctxts'_def split:if_splits option.splits)

done

lemma is_dir_has_sfile:

  "\<lbrakk>is_dir s f; valid s\<rbrakk> \<Longrightarrow> (case f of

      [] \<Rightarrow> cf2sfile s f = Some sroot

    | a # pf \<Rightarrow> (\<exists> sec psec asecs. cf2sfile s f = Some 

      (if (\<not> deleted (O_dir f) s \<and> is_init_dir f) then Init f else Created,

       sec, Some psec, set asecs) \<and> (sectxt_of_obj s (O_dir f) = Some sec) \<and>

       (sectxt_of_obj s (O_dir pf) = Some psec) \<and> (get_parentfs_ctxts s pf = Some asecs)))"

apply (case_tac f, simp add:sroot_only)

apply (frule is_dir_in_current, frule is_dir_not_file)

apply (drule current_file_has_sfile, simp)

apply (auto simp:cf2sfile_def split:if_splits option.splits)

done

lemma sroot_set:

  "valid s \<Longrightarrow> \<exists> sec. sroot = (Init [], sec, None, {}) \<and> sectxt_of_obj s (O_dir []) = Some sec"

apply (frule root_is_dir)

apply (drule is_dir_has_sec, simp)

apply (auto simp:sroot_def sec_of_root_def sectxt_of_obj_def type_of_obj.simps 

                 root_type_remains root_user_remains

           dest!:root_has_type' root_has_user' root_has_init_type' root_has_init_user'

           split:option.splits)

done

lemma cf2sfile_path_file:

  "\<lbrakk>is_file s (f # pf); valid s\<rbrakk>

   \<Longrightarrow> cf2sfile s (f # pf) = (

     case (cf2sfile s pf) of

       Some (pfi, pfsec, psec, asecs) \<Rightarrow> 

          (case (sectxt_of_obj s (O_file (f # pf))) of

              Some fsec \<Rightarrow> Some (if (\<not> deleted (O_file (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf)

                                else Created, fsec, Some pfsec, asecs \<union> {pfsec})

           | None \<Rightarrow> None)

     | _ \<Rightarrow> None)"

apply (frule is_file_in_current, drule parentf_is_dir'', simp)

apply (frule is_dir_has_sfile, simp, frule is_file_has_sfile, simp)

apply (frule sroot_set)

apply (case_tac pf, (clarsimp simp:get_parentfs_ctxts'_def sectxt_of_pf_def)+) 

done

lemma cf2sfile_path_dir:

  "\<lbrakk>is_dir s (f # pf); valid s\<rbrakk>

   \<Longrightarrow> cf2sfile s (f # pf) = (

     case (cf2sfile s pf) of

       Some (pfi, pfsec, psec, asecs) \<Rightarrow> 

          (case (sectxt_of_obj s (O_dir (f # pf))) of

              Some fsec \<Rightarrow> Some (if (\<not> deleted (O_dir (f # pf)) s \<and> is_init_dir (f # pf)) then Init (f # pf)

                                else Created, fsec, Some pfsec, asecs \<union> {pfsec})

           | None \<Rightarrow> None)

     | _ \<Rightarrow> None)"

apply (frule is_dir_in_current, drule parentf_is_dir'', simp)

apply (frule_tac f = "f # pf" in is_dir_has_sfile, simp)

apply (frule_tac f = "pf" in is_dir_has_sfile, simp)

apply (frule sroot_set)

apply (case_tac pf, (clarsimp simp:get_parentfs_ctxts'_def sectxt_of_pf_def)+) 

done  

lemma cf2sfile_path:

  "\<lbrakk>f # pf \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> cf2sfile s (f # pf) = (

     case (cf2sfile s pf) of

       Some (pfi, pfsec, psec, asecs) \<Rightarrow> (if (is_file s (f # pf))

         then (case (sectxt_of_obj s (O_file (f # pf))) of

                 Some fsec \<Rightarrow> Some (if (\<not> deleted (O_file (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf)

                                   else Created, fsec, Some pfsec, asecs \<union> {pfsec})

               | None \<Rightarrow> None)

         else (case (sectxt_of_obj s (O_dir (f # pf))) of

                 Some fsec \<Rightarrow> Some (if (\<not> deleted (O_dir (f # pf)) s \<and> is_init_dir (f # pf)) then Init (f # pf)

                                   else Created, fsec, Some pfsec, asecs \<union> {pfsec})

               | None \<Rightarrow> None)           )

     | None \<Rightarrow> None)"

apply (drule is_file_or_dir, simp)

apply (erule disjE)

apply (frule cf2sfile_path_file, simp) defer

apply (frule cf2sfile_path_dir, simp, drule is_dir_not_file)

apply (auto split:option.splits)

done

lemma cf2sfile_path_file_prop1:

  "\<lbrakk>is_file s (f # pf); cf2sfile s pf = Some (pfi, pfsec, psec, asecs); valid s\<rbrakk>

   \<Longrightarrow> \<exists> fsec. cf2sfile s (f # pf) = 

                 Some (if (\<not> deleted (O_file (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf)

                       else Created, fsec, Some pfsec, asecs \<union> {pfsec}) \<and> 

               sectxt_of_obj s (O_file (f # pf)) = Some fsec"

apply (frule is_file_has_sfile, simp)

by (auto simp:cf2sfile_path_file)

lemma cf2sfile_path_file_prop2:

  "\<lbrakk>is_file s (f # pf); cf2sfile s pf = Some (pfi, pfsec, psec, asecs); 

    sectxt_of_obj s (O_file (f # pf)) = Some fsec; valid s\<rbrakk> \<Longrightarrow> cf2sfile s (f # pf) = 

      Some (if (\<not> deleted (O_file (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf)

            else Created, fsec, Some pfsec, asecs \<union> {pfsec})"

by (drule cf2sfile_path_file_prop1, auto)

lemma cf2sfile_path_dir_prop1:

  "\<lbrakk>is_dir s (f # pf); cf2sfile s pf = Some (pfi, pfsec, psec, asecs); valid s\<rbrakk>

   \<Longrightarrow> \<exists> fsec. cf2sfile s (f # pf) = 

                 Some (if (\<not> deleted (O_dir (f # pf)) s \<and> is_init_dir (f # pf)) then Init (f # pf)

                       else Created, fsec, Some pfsec, asecs \<union> {pfsec}) \<and> 

               sectxt_of_obj s (O_dir (f # pf)) = Some fsec"

apply (frule is_dir_has_sfile, simp)

by (auto simp:cf2sfile_path_dir)

lemma cf2sfile_path_dir_prop2:

  "\<lbrakk>is_dir s (f # pf); cf2sfile s pf = Some (pfi, pfsec, psec, asecs); 

    sectxt_of_obj s (O_dir (f # pf)) = Some fsec; valid s\<rbrakk> \<Longrightarrow> cf2sfile s (f # pf) = 

      Some (if (\<not> deleted (O_dir (f # pf)) s \<and> is_init_dir (f # pf)) then Init (f # pf)

            else Created, fsec, Some pfsec, asecs \<union> {pfsec})"

by (drule cf2sfile_path_dir_prop1, auto)

(**************** cf2sfile event list simpset ****************)

lemma cf2sfile_open_none':

  "valid (Open p f flag fd None # s) \<Longrightarrow> cf2sfile (Open p f flag fd None # s) f'= cf2sfile s f'"

apply (frule vd_cons, frule vt_grant_os)

apply (induct f', simp add:cf2sfile_def)

apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 

               get_parentfs_ctxts_simps)

done

lemma cf2sfile_open_none:

  "valid (Open p f flag fd None # s) \<Longrightarrow> cf2sfile (Open p f flag fd None # s) = cf2sfile s"

apply (rule ext)

by (simp add:cf2sfile_open_none')

lemma cf2sfile_open_some1:

  "\<lbrakk>valid (Open p f flag fd (Some inum) # s); f' \<in> current_files s\<rbrakk>

   \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' = cf2sfile s f'"

apply (frule vd_cons, frule vt_grant_os, frule noroot_events)

apply (case_tac "f = f'", simp)

apply (induct f', simp add:sroot_only, simp)

apply (frule parentf_in_current', simp+)

apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 

               get_parentfs_ctxts_simps)

done

lemma cf2sfile_open_some2:

  "\<lbrakk>valid (Open p f flag fd (Some inum) # s); is_file s f'\<rbrakk>

   \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' = cf2sfile s f'"

apply (frule vd_cons, drule is_file_in_current)

by (simp add:cf2sfile_open_some1)

lemma cf2sfile_open_some3:

  "\<lbrakk>valid (Open p f flag fd (Some inum) # s); is_dir s f'\<rbrakk>

   \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' = cf2sfile s f'"

apply (frule vd_cons, drule is_dir_in_current)

by (simp add:cf2sfile_open_some1)

lemma cf2sfile_open_some4:

  "valid (Open p f flag fd (Some inum) # s) \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f = (

     case (parent f) of

       Some pf \<Rightarrow> (case (sectxt_of_obj (Open p f flag fd (Some inum) # 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 (Created, sec, Some psec, set asecs)

                  | _ \<Rightarrow> None)

     | None \<Rightarrow> None)"

apply (frule vd_cons, frule vt_grant_os, frule noroot_events)

apply (case_tac f, simp)

apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 

               get_parentfs_ctxts_simps)

apply (rule impI, (erule conjE)+)

apply (drule not_deleted_init_file, simp+)

apply (simp add:is_file_in_current)

done

lemma cf2sfile_open:

  "\<lbrakk>valid (Open p f flag fd opt # s); f' \<in> current_files (Open p f flag fd opt # s)\<rbrakk>

   \<Longrightarrow> cf2sfile (Open p f flag fd opt # s) f' = (

     if (opt = None) then cf2sfile s f'

     else if (f' = f) 

     then (case (parent f) of

             Some pf \<Rightarrow> (case (sectxt_of_obj (Open p f flag fd opt # 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 (Created, sec, Some psec, set asecs)

                        | _ \<Rightarrow> None)

           | None \<Rightarrow> None)

     else cf2sfile s f')"

apply (case_tac opt)

apply (simp add:cf2sfile_open_none)

apply (case_tac "f = f'")

apply (simp add:cf2sfile_open_some4 split:option.splits)

apply (simp add:cf2sfile_open_some1 current_files_simps)

done

lemma cf2sfile_mkdir1:

  "\<lbrakk>valid (Mkdir p f i # s); f' \<in> current_files s\<rbrakk>

   \<Longrightarrow> cf2sfile (Mkdir p f i # s) f' = cf2sfile s f'"

apply (frule vd_cons, frule vt_grant_os, frule noroot_events)

apply (case_tac "f = f'", simp)

apply (induct f', simp add:sroot_only, simp)

apply (frule parentf_in_current', simp+)

apply (case_tac "f = f'", simp)

apply (simp add:cf2sfile_path is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 

               get_parentfs_ctxts_simps split:if_splits option.splits)

done

lemma cf2sfile_mkdir2:

  "\<lbrakk>valid (Mkdir p f i # s); is_file s f'\<rbrakk>

   \<Longrightarrow> cf2sfile (Mkdir p f i # s) f' = cf2sfile s f'"

apply (frule vd_cons, drule is_file_in_current)

by (simp add:cf2sfile_mkdir1)

lemma cf2sfile_mkdir3:

  "\<lbrakk>valid (Mkdir p f i # s); is_dir s f'\<rbrakk>

   \<Longrightarrow> cf2sfile (Mkdir p f i # s) f' = cf2sfile s f'"

apply (frule vd_cons, drule is_dir_in_current)

by (simp add:cf2sfile_mkdir1)

lemma cf2sfile_mkdir4:

  "valid (Mkdir p f i # s)

  \<Longrightarrow> cf2sfile (Mkdir p f i # s) f = (case (parent f) of

         Some pf \<Rightarrow> (case (sectxt_of_obj (Mkdir p f i # 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 (Created, sec, Some psec, set asecs)

                    | _ \<Rightarrow> None)

       | None \<Rightarrow> None)"

apply (frule vd_cons, frule vt_grant_os, frule noroot_events)

apply (case_tac f, simp)

apply (clarsimp simp:os_grant.simps)

apply (simp add:sectxt_of_obj_simps)

apply (frule current_proc_has_sec, simp)

apply (frule is_dir_has_sec, simp)

apply (frule get_pfs_secs_prop, simp)

apply (frule is_dir_not_file)

apply (auto simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 

               get_parentfs_ctxts_simps split:option.splits if_splits 

            dest:not_deleted_init_dir is_dir_in_current not_deleted_init_file is_file_in_current)

done

lemma cf2sfile_mkdir:

  "\<lbrakk>valid (Mkdir p f i # s); f' \<in> current_files (Mkdir p f i # s)\<rbrakk>

  \<Longrightarrow> cf2sfile (Mkdir p f i # s) f' = (

    if (f' = f) 

    then (case (parent f) of

             Some pf \<Rightarrow> (case (sectxt_of_obj (Mkdir p f i # 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 (Created, sec, Some psec, set asecs)

                        | _ \<Rightarrow> None)

           | None \<Rightarrow> None)

     else cf2sfile s f')"

apply (case_tac "f = f'")

apply (simp add:cf2sfile_mkdir4 split:option.splits)

apply (simp add:cf2sfile_mkdir1 current_files_simps)

done

lemma cf2sfile_linkhard1:

  "\<lbrakk>valid (LinkHard p oldf f # s); f' \<in> current_files s\<rbrakk>

   \<Longrightarrow> cf2sfile (LinkHard p oldf f# s) f' = cf2sfile s f'"

apply (frule vd_cons, frule vt_grant_os, frule noroot_events)

apply (case_tac "f = f'", simp)

apply (induct f', simp add:sroot_only, simp)

apply (frule parentf_in_current', simp+)

apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 

               get_parentfs_ctxts_simps split:if_splits option.splits)

done

lemma cf2sfile_linkhard2:

  "\<lbrakk>valid (LinkHard p oldf f # s); is_file s f'\<rbrakk>

   \<Longrightarrow> cf2sfile (LinkHard p oldf f # s) f' = cf2sfile s f'"

apply (frule vd_cons, drule is_file_in_current)

by (simp add:cf2sfile_linkhard1)

lemma cf2sfile_linkhard3:

  "\<lbrakk>valid (LinkHard p oldf f # s); is_dir s f'\<rbrakk>

   \<Longrightarrow> cf2sfile (LinkHard p oldf f # s) f' = cf2sfile s f'"

apply (frule vd_cons, drule is_dir_in_current)

by (simp add:cf2sfile_linkhard1)

lemma cf2sfile_linkhard4:

  "valid (LinkHard p oldf f # s)

  \<Longrightarrow> cf2sfile (LinkHard p oldf f # s) f = (case (parent f) of

         Some pf \<Rightarrow> (case (sectxt_of_obj (LinkHard p oldf f # 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 (Created, sec, Some psec, set asecs)

                    | _ \<Rightarrow> None)

       | None \<Rightarrow> None)"

apply (frule vd_cons, frule vt_grant_os, frule noroot_events)

apply (case_tac f, simp)

apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 

               get_parentfs_ctxts_simps)

apply (rule impI, (erule conjE)+)

apply (drule not_deleted_init_file, simp+)

apply (simp add:is_file_in_current)

done

lemma cf2sfile_linkhard:

  "\<lbrakk>valid (LinkHard p oldf f # s); f' \<in> current_files (LinkHard p oldf f # s)\<rbrakk>

  \<Longrightarrow> cf2sfile (LinkHard p oldf f # s) f' = (

    if (f' = f) 

    then (case (parent f) of

             Some pf \<Rightarrow> (case (sectxt_of_obj (LinkHard p oldf f # 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 (Created, sec, Some psec, set asecs)

                        | _ \<Rightarrow> None)

           | None \<Rightarrow> None)

     else cf2sfile s f')"

apply (case_tac "f = f'")

apply (simp add:cf2sfile_linkhard4 split:option.splits)

apply (simp add:cf2sfile_linkhard1 current_files_simps)

done

lemma cf2sfile_other:

  "\<lbrakk>ff \<in> current_files s;

    \<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt;

    \<forall> p fd. e \<noteq> CloseFd p fd;

    \<forall> p f. e \<noteq> UnLink p f;

    \<forall> p f. e \<noteq> Rmdir p f;

    \<forall> p f i. e \<noteq> Mkdir p f i;

    \<forall> p f f'. e \<noteq> LinkHard p f f'; 

    valid (e # s)\<rbrakk> \<Longrightarrow> cf2sfile (e # s) ff = cf2sfile s ff"

apply (frule vd_cons, frule vt_grant_os)

apply (induct ff, simp add:sroot_only)

apply (frule parentf_in_current', simp+, case_tac e)

apply (auto simp:current_files_simps is_file_simps is_dir_simps sectxt_of_obj_simps cf2sfile_path 

           split:if_splits option.splits)                     

done     

lemma cf2sfile_unlink:

  "\<lbrakk>valid (UnLink p f # s); f' \<in> current_files (UnLink p f # s)\<rbrakk>

   \<Longrightarrow> cf2sfile (UnLink p f # s) f' = cf2sfile s f'"

apply (frule vd_cons, frule vt_grant_os)

apply (simp add:current_files_simps split:if_splits)

apply (auto simp:cf2sfile_def sectxt_of_obj_simps get_parentfs_ctxts_simps is_file_simps is_dir_simps

done

done

done

done

done