no_shm_selinux/Static.thy
changeset 77 6f7b9039715f
child 85 1d1aa5bdd37d
equal deleted inserted replaced
76:f27ba31b7e96 77:6f7b9039715f
       
     1 theory Static
       
     2 imports Static_type OS_type_def Flask_type Flask
       
     3 begin
       
     4 
       
     5 locale tainting_s = tainting 
       
     6 
       
     7 begin
       
     8 
       
     9 (*
       
    10 definition init_sectxt_of_file:: "t_file \<Rightarrow> security_context_t option"
       
    11 where
       
    12   "init_sectxt_of_file f \<equiv> 
       
    13      if (is_init_file f) then init_sectxt_of_obj (O_file f)
       
    14      else if (is_init_dir f) then init_sectxt_of_obj (O_dir f)
       
    15      else None"
       
    16 *)
       
    17 
       
    18 definition sroot :: "t_sfile"
       
    19 where
       
    20   "sroot \<equiv> (Init [], sec_of_root, None, {})"
       
    21 
       
    22 definition init_cf2sfile :: "t_file \<Rightarrow> t_sfile option"
       
    23 where
       
    24   "init_cf2sfile f \<equiv> 
       
    25      case (parent f) of 
       
    26        None \<Rightarrow> Some sroot
       
    27      | Some pf \<Rightarrow> if (is_init_file f) then 
       
    28  (case (init_sectxt_of_obj (O_file f), init_sectxt_of_obj (O_dir pf), get_parentfs_ctxts [] pf) of
       
    29     (Some sec, Some psec, Some aseclist) \<Rightarrow> Some (Init f, sec, Some psec, set aseclist)
       
    30   | _ \<Rightarrow> None)    else 
       
    31  (case (init_sectxt_of_obj (O_dir f), init_sectxt_of_obj (O_dir pf), get_parentfs_ctxts [] pf) of
       
    32     (Some sec, Some psec, Some aseclist) \<Rightarrow> Some (Init f, sec, Some psec, set aseclist)
       
    33   | _ \<Rightarrow> None)"
       
    34 
       
    35 definition init_cf2sfiles :: "t_file \<Rightarrow> t_sfile set"
       
    36 where
       
    37   "init_cf2sfiles f \<equiv> {sf. \<exists>f' \<in> init_same_inode_files f. init_cf2sfile f' = Some sf}"
       
    38 
       
    39 definition init_cfd2sfd :: "t_process \<Rightarrow> t_fd \<Rightarrow> (security_context_t \<times> t_open_flags \<times> t_sfile) option"
       
    40 where
       
    41   "init_cfd2sfd p fd = 
       
    42      (case (init_file_of_proc_fd p fd, init_oflags_of_proc_fd p fd, init_sectxt_of_obj (O_fd p fd)) of
       
    43         (Some f, Some flags, Some sec) \<Rightarrow> (case (init_cf2sfile f) of 
       
    44                                              Some sf \<Rightarrow> Some (sec, flags, sf)
       
    45                                            | _ \<Rightarrow> None)
       
    46       | _ \<Rightarrow> None)"
       
    47 
       
    48 definition init_cfds2sfds :: "t_process \<Rightarrow> (security_context_t \<times> t_open_flags \<times> t_sfile) set"
       
    49 where
       
    50   "init_cfds2sfds p \<equiv> { sfd. \<exists> fd \<in> init_proc_file_fds p. init_cfd2sfd p fd = Some sfd}"
       
    51 
       
    52 (*
       
    53 definition init_ch2sshm :: "t_shm \<Rightarrow> t_sshm option"
       
    54 where
       
    55   "init_ch2sshm h \<equiv> (case (init_sectxt_of_obj (O_shm h)) of
       
    56                        Some sec \<Rightarrow> Some (Init h, sec)
       
    57                      | _        \<Rightarrow> None)"
       
    58 
       
    59 definition init_cph2spshs 
       
    60   :: "t_process \<Rightarrow> (t_sshm \<times> t_shm_attach_flag) set"
       
    61 where
       
    62   "init_cph2spshs p \<equiv> {(sh, flag)| sh flag h. (p, flag) \<in> init_procs_of_shm h \<and> 
       
    63                                              init_ch2sshm h = Some sh}"
       
    64 *)
       
    65 definition init_cp2sproc :: "t_process \<Rightarrow> t_sproc option"
       
    66 where
       
    67   "init_cp2sproc p \<equiv> (case (init_sectxt_of_obj (O_proc p)) of 
       
    68        Some sec \<Rightarrow> Some (Init p, sec, (init_cfds2sfds p))
       
    69      | None     \<Rightarrow> None)"
       
    70 
       
    71 (* acient files of init-file 
       
    72 definition init_o2s_afs :: "t_file \<Rightarrow> security_context_t set"
       
    73 where
       
    74   "init_o2s_afs f \<equiv> {sec. \<exists> f'. f' \<preceq> f \<and> init_sectxt_of_obj (O_dir f') = Some sec}" *)
       
    75 
       
    76 definition init_cm2smsg :: "t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsg option"
       
    77 where
       
    78   "init_cm2smsg q m \<equiv> (case (init_sectxt_of_obj (O_msg q m)) of 
       
    79                          Some sec \<Rightarrow> Some (Init m, sec, (O_msg q m) \<in> seeds)
       
    80                        | _ \<Rightarrow> None)"
       
    81 
       
    82 fun init_cqm2sms :: "t_msgq \<Rightarrow> t_msg list \<Rightarrow> (t_smsg list) option"
       
    83 where
       
    84   "init_cqm2sms q []     = Some []"
       
    85 | "init_cqm2sms q (m#ms) = 
       
    86      (case (init_cqm2sms q ms, init_cm2smsg q m) of 
       
    87         (Some sms, Some sm) \<Rightarrow> Some (sm # sms)
       
    88       | _        \<Rightarrow> None)"
       
    89 
       
    90 definition init_cq2smsgq :: "t_msgq \<Rightarrow> t_smsgq option"
       
    91 where
       
    92   "init_cq2smsgq q \<equiv> (case (init_sectxt_of_obj (O_msgq q), init_cqm2sms q (init_msgs_of_queue q)) of 
       
    93        (Some sec, Some sms) \<Rightarrow> Some (Init q, sec, sms)
       
    94      | _ \<Rightarrow> None)"
       
    95 
       
    96 fun init_obj2sobj :: "t_object \<Rightarrow> t_sobject option"
       
    97 where
       
    98   "init_obj2sobj (O_proc p) = 
       
    99      (case (init_cp2sproc p) of 
       
   100        Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> seeds))
       
   101      | _ \<Rightarrow> None)"
       
   102 | "init_obj2sobj (O_file f) = 
       
   103      Some (S_file (init_cf2sfiles f) 
       
   104                   (\<exists> f'. f' \<in> (init_same_inode_files f) \<and> O_file f \<in> seeds))"
       
   105 | "init_obj2sobj (O_dir f) = 
       
   106      (case (init_cf2sfile f) of
       
   107            Some sf \<Rightarrow> Some (S_dir sf) 
       
   108          | _ \<Rightarrow> None)"
       
   109 | "init_obj2sobj (O_msgq q) = 
       
   110      (case (init_cq2smsgq q) of
       
   111        Some sq \<Rightarrow> Some (S_msgq sq)
       
   112      | _ \<Rightarrow> None)"
       
   113 (*
       
   114 | "init_obj2sobj (O_shm h) = 
       
   115      (case (init_ch2sshm h) of 
       
   116        Some sh \<Rightarrow> Some (S_shm sh)
       
   117      | _       \<Rightarrow> None)"  
       
   118 | "init_obj2sobj (O_msg q m) = 
       
   119      (case (init_cq2smsgq q, init_cm2smsg q m) of 
       
   120         (Some sq, Some sm) \<Rightarrow> Some (S_msg sq sm)
       
   121       | _                  \<Rightarrow> None)" *)
       
   122 | "init_obj2sobj _ = None"
       
   123 
       
   124 definition  
       
   125   "init_static_state \<equiv> {sobj. \<exists> obj. init_alive obj \<and> init_obj2sobj obj = Some sobj}"
       
   126 
       
   127 (**************** translation from dynamic to static *******************)
       
   128 
       
   129 definition cf2sfile :: "t_state \<Rightarrow> t_file \<Rightarrow> t_sfile option"
       
   130 where
       
   131   "cf2sfile s f \<equiv>
       
   132      case (parent f) of 
       
   133        None \<Rightarrow> Some sroot
       
   134      | Some pf \<Rightarrow> if (is_file s f) 
       
   135      then (case (sectxt_of_obj s (O_file f), sectxt_of_obj s (O_dir pf), get_parentfs_ctxts s pf) of
       
   136             (Some sec, Some psec, Some asecs) \<Rightarrow>
       
   137  Some (if (\<not> died (O_file f) s \<and> is_init_file f) then Init f else Created, sec, Some psec, set asecs)
       
   138           | _ \<Rightarrow> None) 
       
   139      else (case (sectxt_of_obj s (O_dir f), sectxt_of_obj s (O_dir pf), get_parentfs_ctxts s pf) of
       
   140             (Some sec, Some psec, Some asecs) \<Rightarrow>
       
   141  Some (if (\<not> died (O_dir f) s \<and> is_init_dir f) then Init f else Created, sec, Some psec, set asecs)
       
   142           | _ \<Rightarrow> None)"
       
   143 
       
   144 definition cf2sfiles :: "t_state \<Rightarrow> t_file \<Rightarrow> t_sfile set"
       
   145 where
       
   146   "cf2sfiles s f \<equiv> {sf. \<exists> f' \<in> (same_inode_files s f). cf2sfile s f' = Some sf}"
       
   147 
       
   148 (* here cf2sfile is passed with True, because, process' fds are only for files not dirs *)
       
   149 definition cfd2sfd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd \<Rightarrow> t_sfd option" 
       
   150 where
       
   151   "cfd2sfd s p fd \<equiv> 
       
   152     (case (file_of_proc_fd s p fd, flags_of_proc_fd s p fd, sectxt_of_obj s (O_fd p fd)) of
       
   153       (Some f, Some flags, Some sec) \<Rightarrow> (case (cf2sfile s f) of 
       
   154                                           Some sf \<Rightarrow> Some (sec, flags, sf)
       
   155                                         | _       \<Rightarrow> None)
       
   156     | _ \<Rightarrow> None)"
       
   157 
       
   158 
       
   159 definition cpfd2sfds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sfd set"
       
   160 where
       
   161   "cpfd2sfds s p \<equiv> {sfd. \<exists> fd \<in> proc_file_fds s p. cfd2sfd s p fd = Some sfd}"
       
   162 
       
   163 (*
       
   164 definition ch2sshm :: "t_state \<Rightarrow> t_shm \<Rightarrow> t_sshm option"
       
   165 where
       
   166   "ch2sshm s h \<equiv> (case (sectxt_of_obj s (O_shm h)) of
       
   167                     Some sec \<Rightarrow> 
       
   168  Some (if (\<not> died (O_shm h) s \<and> h \<in> init_shms) then Init h else Created, sec)
       
   169                   | _ \<Rightarrow> None)"
       
   170 
       
   171 definition cph2spshs :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sproc_sshm set"
       
   172 where
       
   173   "cph2spshs s p \<equiv> {(sh, flag)| sh flag h. (p, flag) \<in> procs_of_shm s h \<and> ch2sshm s h = Some sh}"
       
   174 *)
       
   175 definition cp2sproc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sproc option"
       
   176 where
       
   177   "cp2sproc s p \<equiv> (case (sectxt_of_obj s (O_proc p)) of 
       
   178                      Some sec \<Rightarrow> 
       
   179  Some (if (\<not> died (O_proc p) s \<and> p \<in> init_procs) then Init p else Created, sec, 
       
   180        cpfd2sfds s p)
       
   181                    | _ \<Rightarrow> None)"
       
   182 
       
   183 definition cm2smsg :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsg option"
       
   184 where
       
   185   "cm2smsg s q m \<equiv> (case (sectxt_of_obj s (O_msg q m)) of 
       
   186                       Some sec \<Rightarrow>
       
   187  Some (if (\<not> died (O_msg q m) s \<and> m \<in> set (init_msgs_of_queue q)) then Init m else Created,
       
   188        sec, O_msg q m \<in> tainted s)
       
   189                     | _ \<Rightarrow> None)"
       
   190 
       
   191 fun cqm2sms:: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg list \<Rightarrow> (t_smsg list) option"
       
   192 where 
       
   193   "cqm2sms s q [] = Some []"
       
   194 | "cqm2sms s q (m#ms) = 
       
   195      (case (cqm2sms s q ms, cm2smsg s q m) of 
       
   196        (Some sms, Some sm) \<Rightarrow> Some (sm#sms) 
       
   197      | _ \<Rightarrow> None)"
       
   198 
       
   199 definition cq2smsgq :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_smsgq option"
       
   200 where
       
   201   "cq2smsgq s q \<equiv> (case (sectxt_of_obj s (O_msgq q), cqm2sms s q (msgs_of_queue s q)) of 
       
   202                      (Some sec, Some sms) \<Rightarrow> 
       
   203  Some (if (\<not> died (O_msgq q) s \<and> q \<in> init_msgqs) then Init q else Created,
       
   204        sec, sms)
       
   205                    | _ \<Rightarrow> None)"
       
   206 
       
   207 fun co2sobj :: "t_state \<Rightarrow> t_object \<Rightarrow> t_sobject option"
       
   208 where
       
   209   "co2sobj s (O_proc p) = 
       
   210      (case (cp2sproc s p) of 
       
   211         Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))
       
   212       | _       \<Rightarrow> None)"
       
   213 | "co2sobj s (O_file f) = 
       
   214      Some (S_file (cf2sfiles s f) (O_file f \<in> tainted s))"
       
   215 | "co2sobj s (O_dir f) = 
       
   216      (case (cf2sfile s f) of
       
   217         Some sf  \<Rightarrow> Some (S_dir sf)
       
   218       | _ \<Rightarrow> None)"
       
   219 | "co2sobj s (O_msgq q) = 
       
   220      (case (cq2smsgq s q) of
       
   221         Some sq \<Rightarrow> Some (S_msgq sq)
       
   222       | _ \<Rightarrow> None)"
       
   223 (*
       
   224 | "co2sobj s (O_shm h) = 
       
   225      (case (ch2sshm s h) of 
       
   226         Some sh \<Rightarrow> Some (S_shm sh)
       
   227       | _ \<Rightarrow> None)"
       
   228 
       
   229 | "co2sobj s (O_msg q m) = 
       
   230      (case (cq2smsgq s q, cm2smsg s q m) of 
       
   231        (Some sq, Some sm) \<Rightarrow> Some (S_msg sq sm)
       
   232      | _ \<Rightarrow> None)"
       
   233 *)
       
   234 | "co2sobj s _ = None"
       
   235 
       
   236 
       
   237 definition s2ss :: "t_state \<Rightarrow> t_static_state"
       
   238 where
       
   239   "s2ss s \<equiv> {sobj. \<exists> obj. alive s obj \<and> co2sobj s obj = Some sobj}"
       
   240 
       
   241 
       
   242 (* ******************************************************** *)
       
   243 
       
   244 
       
   245 fun is_init_sfile :: "t_sfile \<Rightarrow> bool"
       
   246 where
       
   247   "is_init_sfile (Init _, sec, psec,asec) = True"
       
   248 | "is_init_sfile _ = False"
       
   249 
       
   250 fun is_many_sfile :: "t_sfile \<Rightarrow> bool"
       
   251 where
       
   252   "is_many_sfile (Created, sec, psec, asec) = True"
       
   253 | "is_many_sfile _ = False"
       
   254 
       
   255 fun is_init_sproc :: "t_sproc \<Rightarrow> bool"
       
   256 where
       
   257   "is_init_sproc (Init p, sec, fds) = True"
       
   258 | "is_init_sproc _                        = False"
       
   259 
       
   260 fun is_many_sproc :: "t_sproc \<Rightarrow> bool"
       
   261 where
       
   262   "is_many_sproc (Created, sec,fds) = True"
       
   263 | "is_many_sproc _                       = False"
       
   264 
       
   265 fun is_many_smsg :: "t_smsg \<Rightarrow> bool"
       
   266 where
       
   267   "is_many_smsg (Created,sec,tag) = True"
       
   268 | "is_many_smsg _                 = False"
       
   269 
       
   270 (* wrong def 
       
   271 fun is_many_smsgq :: "t_smsgq \<Rightarrow> bool"
       
   272 where
       
   273   "is_many_smsgq (Created,sec,sms) = (True \<and> (\<forall> sm \<in> (set sms). is_many_smsg sm))"
       
   274 | "is_many_smsgq _                 = False"
       
   275 *)
       
   276 
       
   277 fun is_many_smsgq :: "t_smsgq \<Rightarrow> bool"
       
   278 where
       
   279   "is_many_smsgq (Created,sec,sms) = True"
       
   280 | "is_many_smsgq _                 = False"
       
   281 (*
       
   282 fun is_many_sshm :: "t_sshm \<Rightarrow> bool"
       
   283 where
       
   284   "is_many_sshm (Created, sec) = True"
       
   285 | "is_many_sshm _              = False"
       
   286 *)
       
   287 fun is_many :: "t_sobject \<Rightarrow> bool"
       
   288 where
       
   289   "is_many (S_proc sp   tag) = is_many_sproc sp"
       
   290 | "is_many (S_file sfs  tag) = (\<forall> sf \<in> sfs. is_many_sfile sf)"
       
   291 | "is_many (S_dir  sf      ) = is_many_sfile sf"
       
   292 | "is_many (S_msgq sq      ) = is_many_smsgq sq"
       
   293 (*
       
   294 | "is_many (S_shm  sh      ) = is_many_sshm  sh"
       
   295 *)
       
   296 
       
   297 fun is_init_smsgq :: "t_smsgq \<Rightarrow> bool"
       
   298 where
       
   299   "is_init_smsgq (Init q,sec,sms) = True"
       
   300 | "is_init_smsgq _                = False"
       
   301 
       
   302 (*
       
   303 fun is_init_sshm :: "t_sshm \<Rightarrow> bool"
       
   304 where
       
   305   "is_init_sshm (Init h,sec) = True"
       
   306 | "is_init_sshm _            = False"
       
   307 *)
       
   308 fun is_init_sobj :: "t_sobject \<Rightarrow> bool"
       
   309 where
       
   310   "is_init_sobj (S_proc sp tag ) = is_init_sproc sp"
       
   311 | "is_init_sobj (S_file sfs tag) = (\<exists> sf \<in> sfs. is_init_sfile sf)"
       
   312 | "is_init_sobj (S_dir  sf     ) = is_init_sfile sf"
       
   313 | "is_init_sobj (S_msgq sq     ) = is_init_smsgq sq"
       
   314 (*
       
   315 | "is_init_sobj (S_shm  sh     ) = is_init_sshm sh"
       
   316 *)
       
   317 (*
       
   318 fun update_ss_sp:: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state"
       
   319 where
       
   320   "update_ss_sp ss (S_proc sp tag) (S_proc sp' tag') = 
       
   321      (if (is_many_sproc sp) then ss \<union> {S_proc sp' tag'} 
       
   322       else (ss - {S_proc sp tag}) \<union> {S_proc sp' tag'})"
       
   323 
       
   324 fun update_ss_sd:: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state"
       
   325 where
       
   326   "update_ss_sd ss (S_dir sf tag) (S_dir sf' tag') = 
       
   327      (if (is_many_sfile sf) then ss \<union> {S_dir sf' tag'} 
       
   328       else (ss - {S_dir sf tag}) \<union> {S_dir sf' tag'})"
       
   329 *)
       
   330 
       
   331 (*
       
   332 fun sparent :: "t_sfile \<Rightarrow> t_sfile option"
       
   333 where
       
   334   "sparent (Sroot si sec) = None"
       
   335 | "sparent (Sfile si sec spf) = Some spf"
       
   336 
       
   337 inductive is_ancesf :: "t_sfile \<Rightarrow> t_sfile \<Rightarrow> bool" 
       
   338 where
       
   339   "is_ancesf sf sf"
       
   340 | "sparent sf = Some spf \<Longrightarrow> is_ancesf spf sf"
       
   341 | "\<lbrakk>sparent sf = Some spf; is_ancesf saf spf\<rbrakk> \<Longrightarrow> is_ancesf saf sf"
       
   342 
       
   343 definition sfile_reparent :: "t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile"
       
   344 where
       
   345   "sfile_reparent (Sroot)"
       
   346 *)
       
   347 
       
   348 (*
       
   349 (* sfds rename aux definitions *)
       
   350 definition sfds_rename_notrelated 
       
   351   :: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool"
       
   352 where
       
   353   "sfds_rename_notrelated sfds from to sfds' \<equiv> 
       
   354      (\<forall> sec flag sf. (sec,flag,sf) \<in> sfds \<and> (\<not> from \<preceq> sf) \<longrightarrow> (sec,flag,sf) \<in> sfds')"
       
   355 
       
   356 definition sfds_rename_renamed
       
   357   :: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool"
       
   358 where
       
   359   "sfds_rename_renamed sfds sf from to sfds' \<equiv> 
       
   360      (\<forall> sec flag sf'. (sec,flag,sf) \<in> sfds \<and> (sf \<preceq> sf') \<longrightarrow>
       
   361          (sec, flag, file_after_rename sf' from to) \<in> sfds' \<and> (sec,flag,sf) \<notin> sfds')"
       
   362 
       
   363 definition sfds_rename_remain
       
   364   :: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool"
       
   365 where
       
   366   "sfds_rename_remain sfds sf from to sfds' \<equiv> 
       
   367      (\<forall> sec flag sf'. (sec,flag,sf') \<in> sfds \<and> (sf \<preceq> sf') \<longrightarrow> 
       
   368          (sec, flag, sf') \<in> sfds' \<and> (sec,flag, file_after_rename sf' from to) \<notin> sfds')"
       
   369 
       
   370   (* for not many, choose on renamed or not *)
       
   371 definition sfds_rename_choices
       
   372   :: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool"
       
   373 where
       
   374   "sfds_rename_choices sfds sf from to sfds' \<equiv> 
       
   375      sfds_rename_remain sfds sf from to sfds' \<or> sfds_rename_renamed sfds sf from to sfds'"
       
   376 
       
   377 (* for many, merge renamed with not renamed *)
       
   378 definition sfds_rename_both
       
   379   :: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool"
       
   380 where
       
   381   "sfds_rename_both sfds sf from to sfds' \<equiv> 
       
   382      (\<forall> sec flag sf'. (sec,flag,sf') \<in> sfds \<and> (sf \<preceq> sf') \<longrightarrow> 
       
   383          (sec, flag, sf') \<in> sfds' \<or> (sec,flag, file_after_rename sf' from to) \<in> sfds')"
       
   384   
       
   385 (* added to the new sfds, are those only under the new sfile *)
       
   386 definition sfds_rename_added
       
   387   :: "t_sfd set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfd set \<Rightarrow> bool"
       
   388 where
       
   389   "sfds_rename_added sfds from to sfds' \<equiv> 
       
   390      (\<forall> sec' flag' sf' sec flag. (sec',flag',sf') \<in> sfds' \<and> (sec,flag,sf') \<notin> sfds \<longrightarrow> 
       
   391         (\<exists> sf. (sec,flag,sf) \<in> sfds \<and> sf' = file_after_rename from to sf))"
       
   392 
       
   393 definition sproc_sfds_renamed
       
   394   :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
       
   395 where
       
   396   "sproc_sfds_renamed ss sf from to ss' \<equiv>
       
   397      (\<forall> pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \<in> ss \<longrightarrow> 
       
   398        (\<exists> sfds'. S_proc (pi,sec,sfds',sshms) tagp \<in> ss \<and> sfds_rename_renamed sfds sf from to sfds'))"
       
   399 
       
   400 definition sproc_sfds_remain
       
   401   :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
       
   402 where
       
   403   "sproc_sfds_remain ss sf from to ss' \<equiv>
       
   404      (\<forall> pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \<in> ss \<longrightarrow> 
       
   405        (\<exists> sfds'. S_proc (pi,sec,sfds',sshms) tagp \<in> ss \<and> sfds_rename_remain sfds sf from to sfds'))"
       
   406 
       
   407 (* for not many, choose on renamed or not *)
       
   408 definition sproc_sfds_choices
       
   409   :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
       
   410 where
       
   411   "sproc_sfds_choices ss sf from to ss' \<equiv>
       
   412      (\<forall> pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \<in> ss \<longrightarrow> 
       
   413        (\<exists> sfds'. S_proc (pi,sec,sfds',sshms) tagp \<in> ss \<and> sfds_rename_choices sfds sf from to sfds'))"
       
   414   
       
   415 (* for many, merge renamed with not renamed *)
       
   416 definition sproc_sfds_both
       
   417   :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
       
   418 where
       
   419   "sproc_sfds_both ss sf from to ss' \<equiv>
       
   420      (\<forall> pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \<in> ss \<longrightarrow> 
       
   421        (\<exists> sfds'. S_proc (pi,sec,sfds',sshms) tagp \<in> ss \<and> sfds_rename_both sfds sf from to sfds'))"
       
   422 
       
   423 (* remove (\<forall> sp tag. S_proc sp tag \<in> ss \<longrightarrow> S_proc sp tag \<in> ss'),
       
   424  * cause sfds contains sfs informations *)
       
   425 definition ss_rename_notrelated 
       
   426   :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
       
   427 where
       
   428   "ss_rename_notrelated ss sf sf' ss' \<equiv> 
       
   429      (\<forall> sq. S_msgq sq \<in> ss \<longrightarrow> S_msgq sq \<in> ss') \<and> 
       
   430      (\<forall> pi sec sfds sshms tagp. S_proc (pi,sec,sfds,sshms) tagp \<in> ss \<longrightarrow> (\<exists> sfds'.  
       
   431          S_proc (pi,sec,sfds',sshms) tagp \<in> ss'\<and> sfds_rename_notrelated sfds sf sf' sfds'))  \<and>
       
   432      (\<forall> sfs sf'' tag. S_file sfs tag \<in> ss \<and> sf'' \<in> sfs \<and> (\<not> sf \<preceq> sf'') \<longrightarrow> (\<exists> sfs'. 
       
   433          S_file sfs tag \<in> ss' \<and> sf'' \<in> sfs')) \<and>
       
   434      (\<forall> sf'' tag. S_dir sf'' tag \<in> ss \<and> (\<not> sf \<preceq> sf'') \<longrightarrow> S_dir sf'' tag \<in> ss')" 
       
   435 
       
   436 (* rename from to, from should definited renamed if not many *)
       
   437 definition all_descendant_sf_renamed 
       
   438   :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
       
   439 where
       
   440   "all_descendant_sf_renamed ss sf from to ss' \<equiv>
       
   441      (\<forall> sfs sf' tagf. sf \<preceq> sf' \<and> S_file sfs tagf \<in> ss \<and> sf' \<in> sfs \<longrightarrow> (\<exists> sfs'. 
       
   442        S_file sfs' tagf \<in> ss' \<and> file_after_rename from to sf' \<in> sfs' \<and> sf' \<notin> sfs')) \<and> 
       
   443      (\<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>
       
   444      sproc_sfds_renamed ss sf from to ss'"
       
   445 
       
   446 (* not renamed *)
       
   447 definition all_descendant_sf_remain
       
   448   :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
       
   449 where
       
   450   "all_descendant_sf_remain ss sf from to ss' \<equiv>
       
   451      (\<forall> sfs sf' tag'. sf \<preceq> sf' \<and> S_file sfs tag' \<in> ss \<and> sf' \<in> sfs \<longrightarrow> (\<exists> sfs'. 
       
   452        S_file sfs' tag' \<in> ss \<and> file_after_rename from to sf' \<notin> sfs' \<and> sf' \<in> sfs')) \<and> 
       
   453      (\<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>
       
   454      sproc_sfds_remain ss sf from to ss'"
       
   455 
       
   456 definition all_descendant_sf_choices
       
   457   :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
       
   458 where
       
   459   "all_descendant_sf_choices ss sf from to ss' \<equiv>
       
   460      all_descendant_sf_renamed ss sf from to ss' \<or> all_descendant_sf_remain ss sf from to ss'"
       
   461 
       
   462 definition all_descendant_sf_both
       
   463   :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
       
   464 where
       
   465   "all_descendant_sf_both ss sf from to ss' \<equiv>
       
   466      (\<forall> sfs sf' tag'. sf \<preceq> sf' \<and> S_file sfs tag' \<in> ss \<and> sf' \<in> sfs \<longrightarrow> (\<exists> sfs'. 
       
   467         S_file sfs' tag' \<in> ss \<and> file_after_rename from to sf' \<in> sfs' \<or> sf' \<in> sfs')) \<and> 
       
   468      (\<forall> sf' tag'. sf \<preceq> sf' \<and> S_dir sf' tag' \<in> ss \<longrightarrow> 
       
   469         S_dir (file_after_rename from to sf') tag' \<in> ss' \<or> S_dir sf' tag' \<in> ss') \<and>
       
   470      sproc_sfds_both ss sf from to ss'"
       
   471 
       
   472 definition ss_renamed_file 
       
   473   :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
       
   474 where
       
   475   "ss_renamed_file ss sf sf' ss' \<equiv> 
       
   476      (if (is_many_sfile sf) 
       
   477         then all_descendant_sf_choices ss sf sf sf' ss'
       
   478         else all_descendant_sf_renamed ss sf sf sf' ss')"
       
   479 
       
   480 (* added to the new sfs, are those only under the new sfile *)
       
   481 definition sfs_rename_added
       
   482   :: "t_sfile set \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_sfile set \<Rightarrow> bool"
       
   483 where
       
   484   "sfs_rename_added sfs from to sfs' \<equiv> 
       
   485      (\<forall> sf'. sf' \<in> sfs' \<and> sf' \<notin> sfs \<longrightarrow> (\<exists> sf. sf \<in> sfs \<and> sf' = file_after_rename from to sf))"
       
   486 
       
   487 (* added to the new sfile, are those only under the new sfile *)
       
   488 definition ss_rename_added
       
   489   :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
       
   490 where
       
   491   "ss_rename_added ss from to ss' \<equiv> 
       
   492      (\<forall> pi sec fds fds' shms tagp. S_proc (pi, sec, fds,shms) tagp \<in> ss \<and> 
       
   493         S_proc (pi,sec,fds',shms) tagp \<in> ss' \<longrightarrow> sfds_rename_added fds from to fds') \<and>
       
   494      (\<forall> sq. S_msgq sq \<in> ss' \<longrightarrow> S_msgq sq \<in> ss) \<and>
       
   495      (\<forall> sfs sfs' tagf. S_file sfs' tagf \<in> ss' \<and> S_file sfs tagf \<in> ss \<longrightarrow> 
       
   496         sfs_rename_added sfs from to sfs') \<and>
       
   497      (\<forall> sf' tagf. S_dir sf' tagf \<in> ss' \<and> S_dir sf' tagf \<notin> ss \<longrightarrow> 
       
   498         (\<exists> sf. S_dir sf tagf \<in> ss \<and> sf' = file_after_rename from to sf))" 
       
   499 
       
   500 definition sfile_alive :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> bool"
       
   501 where
       
   502   "sfile_alive ss sf \<equiv> (\<exists> sfs tagf. sf \<in> sfs \<and> S_file sfs tagf \<in> ss)"
       
   503 
       
   504 definition sf_alive :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> bool"
       
   505 where
       
   506   "sf_alive ss sf \<equiv> (\<exists> tagd. S_dir sf tagd \<in> ss) \<or> sfile_alive ss sf"
       
   507 
       
   508 (* constrains that the new static state should satisfy *)
       
   509 definition ss_rename:: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state \<Rightarrow> bool"
       
   510 where
       
   511   "ss_rename ss sf sf' ss' \<equiv> 
       
   512      ss_rename_notrelated ss sf sf' ss' \<and>
       
   513      ss_renamed_file ss sf sf' ss' \<and> ss_rename_added ss sf sf' ss' \<and>
       
   514      (\<forall> sf''. sf_alive ss sf'' \<and> sf \<prec> sf'' \<longrightarrow> 
       
   515        (if (is_many_sfile sf'') 
       
   516         then all_descendant_sf_choices ss sf'' sf sf' ss'
       
   517         else all_descendant_sf_both ss sf'' sf sf' ss'))"
       
   518 
       
   519 (* two sfile, the last fname should not be equal *)
       
   520 fun sfile_same_fname:: "t_sfile \<Rightarrow> t_sfile \<Rightarrow> bool"
       
   521 where
       
   522   "sfile_same_fname ((Init n, sec)#spf) ((Init n', sec')#spf') = (n = n')"
       
   523 | "sfile_same_fname _                   _                      = False"
       
   524 
       
   525 (* no same init sfile/only sfile in the target-to spf, should be in static_state addmissble check *)
       
   526 definition ss_rename_no_same_fname:: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> bool"
       
   527 where
       
   528   "ss_rename_no_same_fname ss from spf \<equiv>
       
   529     \<not> (\<exists> to. sfile_same_fname from to \<and> parent to = Some spf \<and> sf_alive ss to)" 
       
   530 
       
   531 (* is not a function, is a relation (one 2 many)
       
   532 definition update_ss_rename :: "t_static_state \<Rightarrow> t_sfile \<Rightarrow> t_sfile \<Rightarrow> t_static_state"
       
   533 where
       
   534   "update_ss_rename ss sf sf' \<equiv> if (is_many_sfile sf) 
       
   535      then (ss \<union> {S_file (file_after_rename sf sf' sf'') tag | sf'' tag. sf \<preceq> sf'' \<and> S_file sf'' tag \<in> ss}
       
   536               \<union> {S_dir  (file_after_rename sf sf' sf'') tag | sf'' tag. sf \<preceq> sf'' \<and> S_dir sf'' tag \<in> ss})
       
   537      else (ss - {S_file sf'' tag | sf'' tag. sf \<preceq> sf'' \<and> S_file sf'' tag \<in> ss}
       
   538               - {S_dir  sf'' tag | sf'' tag. sf \<preceq> sf'' \<and> S_dir sf'' tag \<in> ss})
       
   539               \<union> {S_file (file_after_rename sf sf' sf'') tag | sf'' tag. sf \<preceq> sf'' \<and> S_file sf'' tag \<in> ss}
       
   540               \<union> {S_dir  (file_after_rename sf sf' sf'') tag | sf'' tag. sf \<preceq> sf'' \<and> S_dir sf'' tag \<in> ss}" 
       
   541 *)
       
   542 *)
       
   543 
       
   544 fun sectxt_of_sproc :: "t_sproc \<Rightarrow> security_context_t"
       
   545 where
       
   546   "sectxt_of_sproc (pi,sec,fds) = sec"
       
   547 
       
   548 fun sectxt_of_sfile :: "t_sfile \<Rightarrow> security_context_t"
       
   549 where
       
   550   "sectxt_of_sfile (fi,sec,psec,asecs) = sec"
       
   551 
       
   552 fun asecs_of_sfile :: "t_sfile \<Rightarrow> security_context_t set"
       
   553 where
       
   554   "asecs_of_sfile (fi,sec,psec,asecs) = asecs"
       
   555 
       
   556 definition search_check_s :: "security_context_t \<Rightarrow> t_sfile \<Rightarrow> bool \<Rightarrow> bool"
       
   557 where
       
   558   "search_check_s pctxt sf if_file = 
       
   559     (if if_file 
       
   560       then search_check_ctxt pctxt (sectxt_of_sfile sf) (asecs_of_sfile sf) True
       
   561       else search_check_ctxt pctxt (sectxt_of_sfile sf) (asecs_of_sfile sf) False)"
       
   562 
       
   563 definition sectxts_of_sfds :: "t_sfd set \<Rightarrow> security_context_t set"
       
   564 where
       
   565   "sectxts_of_sfds sfds \<equiv> {ctxt. \<exists> flag sf. (ctxt, flag, sf) \<in> sfds}"
       
   566 
       
   567 definition inherit_fds_check_s :: "security_context_t \<Rightarrow> t_sfd set \<Rightarrow> bool"
       
   568 where
       
   569   "inherit_fds_check_s pctxt sfds \<equiv> inherit_fds_check_ctxt pctxt (sectxts_of_sfds sfds)"
       
   570 
       
   571 (*
       
   572 definition sectxts_of_sproc_sshms :: "t_sproc_sshm set \<Rightarrow> security_context_t set"
       
   573 where
       
   574   "sectxts_of_sproc_sshms sshms \<equiv> {ctxt. \<exists> hi flag. ((hi, ctxt),flag) \<in> sshms}"
       
   575 
       
   576 definition inherit_shms_check_s :: "security_context_t \<Rightarrow> t_sproc_sshm set \<Rightarrow> bool"
       
   577 where
       
   578   "inherit_shms_check_s pctxt sshms \<equiv> inherit_shms_check_ctxt pctxt (sectxts_of_sproc_sshms sshms)"
       
   579 
       
   580 fun info_flow_sshm :: "t_sproc \<Rightarrow> t_sproc \<Rightarrow> bool"
       
   581 where
       
   582   "info_flow_sshm (pi,sec,fds,shms) (pi',sec',fds',shms') = 
       
   583      (\<exists> sh flag'. (sh, SHM_RDWR) \<in> shms \<and> (sh, flag') \<in> shms')" 
       
   584 
       
   585 definition info_flow_sproc_sshms :: "t_sproc_sshm set \<Rightarrow> t_sproc_sshm set \<Rightarrow> bool"
       
   586 where
       
   587   "info_flow_sproc_sshms shms shms' \<equiv> (\<exists> sh flag'. (sh, SHM_RDWR) \<in> shms \<and> (sh, flag') \<in> shms')" 
       
   588 
       
   589 
       
   590 fun info_flow_sshm :: "t_sproc \<Rightarrow> t_sproc \<Rightarrow> bool"
       
   591 where
       
   592   "info_flow_sshm (pi,sec,fds,shms) (pi',sec',fds',shms') = info_flow_sproc_sshms shms shms'"
       
   593 
       
   594 inductive info_flow_sshm :: "t_sproc \<Rightarrow> t_sproc \<Rightarrow> bool"
       
   595 where
       
   596   "info_flow_sshm sp sp"
       
   597 | "\<lbrakk>info_flow_sshm sp (pi,sec,fds,shms); info_flow_sproc_sshms shms shms'\<rbrakk>
       
   598    \<Longrightarrow> info_flow_sshm sp (pi',sec',fds',shms')"
       
   599 *)
       
   600 
       
   601 (*
       
   602 fun smsg_related :: "t_msg \<Rightarrow> t_smsg list \<Rightarrow> bool" 
       
   603 where
       
   604   "smsg_related m []                   = False" 
       
   605 | "smsg_related m ((mi, sec, tag)#sms) =  
       
   606     (if (mi = Init m) then True else smsg_related m sms)" 
       
   607 
       
   608 fun smsgq_smsg_related :: "t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsgq \<Rightarrow> bool"
       
   609 where
       
   610   "smsgq_smsg_related q m (qi, sec, smsgslist) = ((qi = Init q) \<and> (smsg_related m smsgslist))"
       
   611 
       
   612 fun smsg_relatainted :: "t_msg \<Rightarrow> t_smsg list \<Rightarrow> bool"
       
   613 where
       
   614   "smsg_relatainted m []                     = False"
       
   615 | "smsg_relatainted m ((mi, sec, tag)#sms) = 
       
   616     (if (mi = Init m \<and> tag = True) then True else smsg_relatainted m sms)"
       
   617 
       
   618 fun smsgq_smsg_relatainted :: "t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsgq \<Rightarrow> bool"
       
   619 where
       
   620   "smsgq_smsg_relatainted q m (qi, sec, smsgslist) = 
       
   621      ((qi = Init q) \<and> (smsg_relatainted m smsgslist))"
       
   622 *)
       
   623 
       
   624 fun sfile_related :: "t_sfile \<Rightarrow> t_file \<Rightarrow> bool"
       
   625 where
       
   626   "sfile_related (fi,sec,psec,asecs) f = (fi = Init f)"
       
   627 (*
       
   628 fun sproc_related :: "t_process \<Rightarrow> t_sproc \<Rightarrow> bool"
       
   629 where
       
   630   "sproc_related p (pi, sec, fds, shms) = (pi = Init p)"
       
   631 *)
       
   632 fun init_obj_related :: "t_sobject \<Rightarrow> t_object \<Rightarrow> bool"
       
   633 where
       
   634   "init_obj_related (S_proc (pi, sec, fds) tag) (O_proc p') = (pi = Init p')"
       
   635 | "init_obj_related (S_file sfs tag) (O_file f) = (\<exists> sf \<in> sfs. sfile_related sf f)"
       
   636 | "init_obj_related (S_dir sf) (O_dir f) = (sfile_related sf f)"
       
   637 | "init_obj_related (S_msgq (qi, sec, sms)) (O_msgq q') = (qi = Init q')"
       
   638 (*
       
   639 | "init_obj_related (S_shm (hi, sec)) (O_shm h') = (hi = Init h')"
       
   640 
       
   641 | "init_obj_related (S_msg (qi, sec, sms) (mi, secm, tagm)) (O_msg q' m') = (qi = Init q' \<and> mi = Init m')"
       
   642 *)
       
   643 | "init_obj_related _ _ = False"
       
   644 
       
   645 
       
   646 
       
   647 (***************** for backward proof when Instancing static objects ******************)
       
   648 
       
   649 fun all_procs :: "t_state \<Rightarrow> t_process set"
       
   650 where
       
   651   "all_procs [] = init_procs"
       
   652 | "all_procs (Clone p p' fds # s) = insert p' (all_procs s)"
       
   653 | "all_procs (e # s) = all_procs s"
       
   654 
       
   655 definition next_nat :: "nat set \<Rightarrow> nat"
       
   656 where
       
   657   "next_nat nset = (Max nset) + 1"
       
   658 
       
   659 definition new_proc :: "t_state \<Rightarrow> t_process"
       
   660 where 
       
   661   "new_proc \<tau> = next_nat (current_procs \<tau>)"
       
   662 
       
   663 definition brandnew_proc :: "t_state \<Rightarrow> t_process"
       
   664 where
       
   665   "brandnew_proc s \<equiv> next_nat (all_procs s)"
       
   666 
       
   667 fun remove_create_flag :: "t_open_flags \<Rightarrow> t_open_flags"
       
   668 where
       
   669   "remove_create_flag (mflag, oflags) = (mflag, oflags - {OF_CREAT})"
       
   670 
       
   671 definition new_inode_num :: "t_state \<Rightarrow> nat"
       
   672 where
       
   673   "new_inode_num \<tau> = next_nat (current_inode_nums \<tau>)"
       
   674 
       
   675 definition new_msgq :: "t_state \<Rightarrow> t_msgq"
       
   676 where
       
   677   "new_msgq s = next_nat (current_msgqs s)"
       
   678 
       
   679 definition new_msg :: "t_state \<Rightarrow> t_msgq \<Rightarrow> nat"
       
   680 where
       
   681   "new_msg s q = next_nat (set (msgs_of_queue s q))"
       
   682 
       
   683 (*
       
   684 definition new_shm :: "t_state \<Rightarrow> nat"
       
   685 where
       
   686   "new_shm \<tau> = next_nat (current_shms \<tau>)"
       
   687 *)
       
   688 
       
   689 definition new_proc_fd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd"
       
   690 where
       
   691   "new_proc_fd \<tau> p = next_nat (current_proc_fds \<tau> p)"
       
   692 
       
   693 definition all_fname_under_dir:: "t_file \<Rightarrow> t_state \<Rightarrow> t_fname set"
       
   694 where
       
   695   "all_fname_under_dir d \<tau> = {fn. \<exists> f. fn # d = f \<and> f \<in> current_files \<tau>}"
       
   696 
       
   697 fun fname_all_a:: "nat \<Rightarrow> t_fname"
       
   698 where
       
   699   "fname_all_a 0 = []" |
       
   700   "fname_all_a (Suc n) = ''a''@(fname_all_a n)"
       
   701 
       
   702 definition fname_length_set :: "t_fname set \<Rightarrow> nat set"
       
   703 where
       
   704   "fname_length_set fns = length`fns"
       
   705 
       
   706 definition next_fname:: "t_file \<Rightarrow> t_state \<Rightarrow> t_fname"
       
   707 where
       
   708   "next_fname pf \<tau> = fname_all_a ((Max (fname_length_set (all_fname_under_dir pf \<tau>))) + 1)"
       
   709 
       
   710 definition new_childf:: "t_file \<Rightarrow> t_state \<Rightarrow> t_file"
       
   711 where
       
   712   "new_childf pf \<tau> = next_fname pf \<tau> # pf"
       
   713 
       
   714 end
       
   715 
       
   716 end