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