1
+ − 1
theory rc_theory
+ − 2
imports Main my_list_prefix
+ − 3
begin
+ − 4
+ − 5
+ − 6
(****************** rc policy (role, type, ... ) type definitions *****************)
+ − 7
(*** normal: user-defined values for policy ***)
+ − 8
(*** others: RC special values for RC internal control ***)
+ − 9
+ − 10
datatype t_client =
+ − 11
Client1
+ − 12
| Client2
+ − 13
+ − 14
datatype t_normal_role =
+ − 15
WebServer
+ − 16
| WS "t_client"
+ − 17
| UpLoad "t_client"
+ − 18
| CGI "t_client"
+ − 19
+ − 20
datatype t_role =
+ − 21
InheritParentRole
+ − 22
| UseForcedRole
+ − 23
| InheritUpMixed
+ − 24
| InheritUserRole
+ − 25
| InheritProcessRole
+ − 26
| NormalRole "t_normal_role"
+ − 27
+ − 28
datatype t_normal_file_type =
+ − 29
Root_file_type (* special value, as 0 for root-file in the NordSec paper*)
+ − 30
| WebServerLog_file
+ − 31
| WebData_file "t_client"
+ − 32
| CGI_P_file "t_client"
+ − 33
| PrivateD_file "t_client"
+ − 34
| Executable_file (* basic protection of RC *)
+ − 35
+ − 36
datatype t_rc_file_type =
+ − 37
InheritParent_file_type
+ − 38
| NormalFile_type t_normal_file_type
+ − 39
+ − 40
datatype t_normal_proc_type =
+ − 41
WebServer_proc
+ − 42
| CGI_P_proc "t_client"
+ − 43
+ − 44
datatype t_rc_proc_type =
+ − 45
InheritParent_proc_type
+ − 46
| NormalProc_type t_normal_proc_type
+ − 47
| UseNewRoleType
+ − 48
+ − 49
datatype t_normal_ipc_type =
+ − 50
WebIPC
+ − 51
+ − 52
datatype t_normal_rc_type =
+ − 53
File_type t_normal_file_type
+ − 54
| Proc_type t_normal_proc_type
+ − 55
| IPC_type t_normal_ipc_type
+ − 56
+ − 57
+ − 58
+ − 59
(******* Operating System type definitions ********)
+ − 60
+ − 61
type_synonym t_process = nat
+ − 62
+ − 63
type_synonym t_user = nat
+ − 64
+ − 65
type_synonym t_fname = string
+ − 66
+ − 67
type_synonym t_file = "t_fname list"
+ − 68
+ − 69
type_synonym t_ipc = nat
+ − 70
+ − 71
+ − 72
+ − 73
(****** Access Control related type definitions *********)
+ − 74
+ − 75
datatype t_event =
+ − 76
ChangeOwner "t_process" "t_user"
+ − 77
| Clone "t_process" "t_process"
+ − 78
| Execute "t_process" "t_file"
+ − 79
| CreateFile "t_process" "t_file"
+ − 80
| CreateIPC "t_process" "t_ipc"
+ − 81
| ChangeRole "t_process" "t_normal_role" (* A process should change to normal role, which not specified in paper! *)
+ − 82
+ − 83
(* below are events added for tainting modelling *)
+ − 84
| ReadFile "t_process" "t_file"
+ − 85
| WriteFile "t_process" "t_file"
+ − 86
| Send "t_process" "t_ipc"
+ − 87
| Recv "t_process" "t_ipc"
+ − 88
+ − 89
| Kill "t_process" "t_process"
+ − 90
| DeleteFile "t_process" "t_file"
+ − 91
| DeleteIPC "t_process" "t_ipc"
+ − 92
+ − 93
type_synonym t_state = "t_event list"
+ − 94
+ − 95
datatype t_access_type = (*changed by wch, original: "types access_type = nat" *)
+ − 96
READ
+ − 97
| WRITE
+ − 98
| EXECUTE
+ − 99
| CHANGE_OWNER
+ − 100
| CREATE
+ − 101
| SEND
+ − 102
| RECEIVE
+ − 103
+ − 104
| DELETE
+ − 105
+ − 106
+ − 107
(****** Some global functions' definition *****)
+ − 108
+ − 109
fun parent :: "'a list \<Rightarrow> ('a list) option"
+ − 110
where
+ − 111
"parent [] = None"
+ − 112
| "parent (n#ns) = Some ns"
+ − 113
+ − 114
definition some_in_set :: "'a set \<Rightarrow> 'a"
+ − 115
where
+ − 116
"some_in_set S \<equiv> SOME x. x \<in> S"
+ − 117
+ − 118
lemma nonempty_set_has_ele: "S \<noteq> {} \<Longrightarrow> \<exists> e. e \<in> S" by auto
+ − 119
+ − 120
lemma some_in_set_prop: "S \<noteq> {} \<Longrightarrow> some_in_set S \<in> S"
+ − 121
by (drule nonempty_set_has_ele, auto simp:some_in_set_def intro:someI)
+ − 122
+ − 123
+ − 124
(*********** locale for RC+OS definitions **********)
+ − 125
+ − 126
definition bidirect_in_init :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> bool"
+ − 127
where
+ − 128
"bidirect_in_init S f \<equiv> (\<forall> a. a \<in> S \<longrightarrow> (\<exists> b. f a = Some b)) \<and>
+ − 129
(\<forall> a b. f a = Some b \<longrightarrow> a \<in> S)"
+ − 130
+ − 131
locale init =
+ − 132
fixes
+ − 133
init_files :: "t_file set"
+ − 134
and init_file_type :: "t_file \<rightharpoonup> t_normal_file_type"
+ − 135
and init_initialrole :: "t_file \<rightharpoonup> t_role"
+ − 136
and init_forcedrole :: "t_file \<rightharpoonup> t_role"
+ − 137
+ − 138
and init_processes :: "t_process set "
+ − 139
and init_process_type :: "t_process \<rightharpoonup> t_normal_proc_type"
+ − 140
and init_currentrole :: "t_process \<rightharpoonup> t_normal_role"
+ − 141
and init_proc_forcedrole:: "t_process \<rightharpoonup> t_role"
+ − 142
+ − 143
and init_ipcs :: "t_ipc set"
+ − 144
and init_ipc_type:: "t_ipc \<rightharpoonup> t_normal_ipc_type"
+ − 145
+ − 146
and init_users :: "t_user set"
+ − 147
and init_owner :: "t_process \<rightharpoonup> t_user"
+ − 148
and defrole :: "t_user \<rightharpoonup> t_normal_role" (* defrole should return normalrole, which is not
+ − 149
specified in NordSec paper *)
+ − 150
+ − 151
and default_fd_create_type :: "t_normal_role \<Rightarrow> t_rc_file_type" (* this func should only
+ − 152
return type for normal role, for RC special role, error ! NordSec paper*)
+ − 153
and default_ipc_create_type :: "t_normal_role \<Rightarrow> t_normal_ipc_type" (* like above, NordSec paper
+ − 154
does not specify the domain is normal roles *)
+ − 155
and default_process_create_type :: "t_normal_role \<Rightarrow> t_rc_proc_type"
+ − 156
and default_process_execute_type :: "t_normal_role \<Rightarrow> t_rc_proc_type"
+ − 157
and default_process_chown_type :: "t_normal_role \<Rightarrow> t_rc_proc_type"
+ − 158
+ − 159
and comproles :: "t_normal_role \<Rightarrow> t_normal_role set" (* NordSec paper do not specify all roles
+ − 160
here are normal *)
+ − 161
+ − 162
and compatible :: "(t_normal_role \<times> t_normal_rc_type \<times> t_access_type) set" (* NordSec paper do not specify all roles and all types here are normal ! *)
+ − 163
+ − 164
assumes
+ − 165
parent_file_in_init: "\<And> f pf. \<lbrakk>parent f = Some pf; f \<in> init_files\<rbrakk> \<Longrightarrow> pf \<in> init_files"
+ − 166
and root_in_filesystem: "[] \<in> init_files"
+ − 167
and init_irole_has_file: "\<And> f r. init_initialrole f = Some r \<Longrightarrow> f \<in> init_files"
+ − 168
and init_frole_has_file: "\<And> f r. init_forcedrole f = Some r \<Longrightarrow> f \<in> init_files"
+ − 169
and init_ftype_has_file: "\<And> f t. init_file_type f = Some t \<Longrightarrow> f \<in> init_files"
+ − 170
and
+ − 171
init_proc_has_role: "bidirect_in_init init_processes init_currentrole"
+ − 172
and init_proc_has_frole: "bidirect_in_init init_processes init_proc_forcedrole"
+ − 173
and init_proc_has_type: "bidirect_in_init init_processes init_process_type"
+ − 174
and
+ − 175
init_ipc_has_type: "bidirect_in_init init_ipcs init_ipc_type"
+ − 176
and
+ − 177
init_user_has_role: "bidirect_in_init init_users defrole"
+ − 178
and init_proc_has_owner: "bidirect_in_init init_processes init_owner"
+ − 179
and init_owner_valid: "\<And> p u. init_owner p = Some u \<Longrightarrow> u \<in> init_users"
+ − 180
and
+ − 181
init_finite: "finite init_files \<and> finite init_processes \<and> finite init_ipcs \<and> finite init_users"
+ − 182
begin
+ − 183
+ − 184
(***** Operating System Listeners *****)
+ − 185
+ − 186
fun current_files :: "t_state \<Rightarrow> t_file set"
+ − 187
where
+ − 188
"current_files [] = init_files"
+ − 189
| "current_files (CreateFile p f # s) = insert f (current_files s)"
+ − 190
| "current_files (DeleteFile p f # s) = current_files s - {f}"
+ − 191
| "current_files (_ # s) = current_files s"
+ − 192
+ − 193
fun current_procs :: "t_state \<Rightarrow> t_process set"
+ − 194
where
+ − 195
"current_procs [] = init_processes"
+ − 196
| "current_procs (Clone p p' # s) = insert p' (current_procs s)"
+ − 197
| "current_procs (Kill p p' # s) = current_procs s - {p'} "
+ − 198
| "current_procs (_ # s) = current_procs s"
+ − 199
+ − 200
fun current_ipcs :: "t_state \<Rightarrow> t_ipc set"
+ − 201
where
+ − 202
"current_ipcs [] = init_ipcs"
+ − 203
| "current_ipcs (CreateIPC p i # s) = insert i (current_ipcs s)"
+ − 204
| "current_ipcs (DeleteIPC p i # s) = current_ipcs s - {i}"
+ − 205
| "current_ipcs (_ # s) = current_ipcs s"
+ − 206
+ − 207
fun owner :: "t_state \<Rightarrow> t_process \<rightharpoonup> t_user"
+ − 208
where
+ − 209
"owner [] = init_owner"
+ − 210
| "owner (Clone p p' # \<tau>) = (owner \<tau>) (p' := owner \<tau> p)"
+ − 211
| "owner (ChangeOwner p u # \<tau>) = (owner \<tau>) (p := Some u)"
+ − 212
| "owner (_ # \<tau>) = owner \<tau>"
+ − 213
+ − 214
(***** functions for rc internal *****)
+ − 215
+ − 216
(*** Roles Functions ***)
+ − 217
+ − 218
(* comments:
+ − 219
We have fix init_initialrole already in locale, why need this function?
+ − 220
Cause, users may be lazy to specify every file in the initial state to some InheritParent as
+ − 221
initialrole, they can just specify all the important files with special initial role, leaving
+ − 222
all other None, it is init_file_initialrole's job to fill default value(InheritParent) for
+ − 223
other files. Accutally, this has the point of "Functional default settings" in the 2 section of
+ − 224
the NordSec paper.
+ − 225
init_file_forcedrole, and init_file_type_aux are of the same meaning.
+ − 226
*)
+ − 227
fun init_file_initialrole :: "t_file \<rightharpoonup> t_role"
+ − 228
where
+ − 229
"init_file_initialrole [] = (case (init_initialrole []) of
+ − 230
None \<Rightarrow> Some UseForcedRole
+ − 231
| Some r \<Rightarrow> Some r)"
+ − 232
| "init_file_initialrole f = (case (init_initialrole f) of
+ − 233
None \<Rightarrow> Some InheritParentRole
+ − 234
| Some r \<Rightarrow> Some r)"
+ − 235
+ − 236
fun initialrole :: "t_state \<Rightarrow> (t_file \<rightharpoonup> t_role)"
+ − 237
where
+ − 238
"initialrole [] = init_file_initialrole"
+ − 239
| "initialrole (CreateFile p f # s) = (initialrole s) (f:= Some InheritParentRole)"
+ − 240
| "initialrole (_ # s) = initialrole s"
+ − 241
+ − 242
fun erole_functor :: "(t_file \<rightharpoonup> t_role) \<Rightarrow> t_role \<Rightarrow> (t_file \<rightharpoonup> t_role)"
+ − 243
where
+ − 244
"erole_functor rfunc r [] = (
+ − 245
if (rfunc [] = Some InheritParentRole)
+ − 246
then Some r
+ − 247
else rfunc [] )"
+ − 248
| "erole_functor rfunc r (n#ns) = (
+ − 249
if (rfunc (n#ns) = Some InheritParentRole)
+ − 250
then erole_functor rfunc r ns
+ − 251
else rfunc (n#ns) )"
+ − 252
+ − 253
definition effinitialrole :: "t_state \<Rightarrow> (t_file \<rightharpoonup> t_role)"
+ − 254
where
+ − 255
"effinitialrole s \<equiv> erole_functor (initialrole s) UseForcedRole"
+ − 256
+ − 257
fun init_file_forcedrole :: "t_file \<rightharpoonup> t_role"
+ − 258
where
+ − 259
"init_file_forcedrole [] = ( case (init_forcedrole []) of
+ − 260
None \<Rightarrow> Some InheritUpMixed
+ − 261
| Some r \<Rightarrow> Some r )"
+ − 262
| "init_file_forcedrole f = ( case (init_forcedrole f) of
+ − 263
None \<Rightarrow> Some InheritParentRole
+ − 264
| Some r \<Rightarrow> Some r )"
+ − 265
+ − 266
fun forcedrole :: "t_state \<Rightarrow> (t_file \<rightharpoonup> t_role)"
+ − 267
where
+ − 268
"forcedrole [] = init_file_forcedrole"
+ − 269
| "forcedrole (CreateFile p f # s) = (forcedrole s) (f:= Some InheritParentRole)"
+ − 270
| "forcedrole (_ # s) = forcedrole s"
+ − 271
+ − 272
definition effforcedrole :: "t_state \<Rightarrow> (t_file \<rightharpoonup> t_role)"
+ − 273
where
+ − 274
"effforcedrole s \<equiv> erole_functor (forcedrole s) InheritUpMixed"
+ − 275
+ − 276
fun proc_forcedrole :: "t_state \<Rightarrow> (t_process \<rightharpoonup> t_role)" (* $6.7$ *)
+ − 277
where
+ − 278
"proc_forcedrole [] = init_proc_forcedrole"
+ − 279
| "proc_forcedrole (Execute p f # s) = (proc_forcedrole s) (p := effforcedrole s f)"
+ − 280
| "proc_forcedrole (Clone p p' # s) = (proc_forcedrole s) (p' := proc_forcedrole s p)"
+ − 281
| "proc_forcedrole (e # s) = proc_forcedrole s"
+ − 282
+ − 283
fun currentrole :: "t_state \<Rightarrow> (t_process \<rightharpoonup> t_normal_role)"
+ − 284
where
+ − 285
"currentrole [] = init_currentrole"
+ − 286
| "currentrole (Clone p p' # \<tau>) = (currentrole \<tau>) (p' := currentrole \<tau> p)"
+ − 287
| "currentrole (Execute p f # \<tau>) = (currentrole \<tau>) (p :=
+ − 288
case (effinitialrole \<tau> f) of
+ − 289
Some ir \<Rightarrow> (case ir of
+ − 290
NormalRole r \<Rightarrow> Some r
+ − 291
| UseForcedRole \<Rightarrow> (
+ − 292
case (effforcedrole \<tau> f) of
+ − 293
Some fr \<Rightarrow> (case fr of
+ − 294
NormalRole r \<Rightarrow> Some r
+ − 295
| InheritUserRole \<Rightarrow> (defrole \<circ>\<^sub>m (owner \<tau>)) p
+ − 296
| InheritProcessRole \<Rightarrow> currentrole \<tau> p
+ − 297
| InheritUpMixed \<Rightarrow> currentrole \<tau> p
+ − 298
| _ \<Rightarrow> None )
+ − 299
| _ \<Rightarrow> None )
+ − 300
| _ \<Rightarrow> None )
+ − 301
| _ \<Rightarrow> None )"
+ − 302
| "currentrole (ChangeOwner p u # \<tau>) = (currentrole \<tau>) (p :=
+ − 303
case (proc_forcedrole \<tau> p) of
+ − 304
Some fr \<Rightarrow> (case fr of
+ − 305
NormalRole r \<Rightarrow> Some r
+ − 306
| InheritProcessRole \<Rightarrow> currentrole \<tau> p
+ − 307
| InheritUserRole \<Rightarrow> defrole u
+ − 308
| InheritUpMixed \<Rightarrow> defrole u
+ − 309
| _ \<Rightarrow> None)
+ − 310
| _ \<Rightarrow> None )"
+ − 311
| "currentrole (ChangeRole p r # \<tau>) = (currentrole \<tau>) (p := Some r)"
+ − 312
| "currentrole (_ # \<tau>) = currentrole \<tau>"
+ − 313
+ − 314
(*** Types Functions ***)
+ − 315
+ − 316
fun init_file_type_aux :: "t_file \<rightharpoonup> t_rc_file_type"
+ − 317
where
+ − 318
"init_file_type_aux f = (if (f \<in> init_files)
+ − 319
then (case (init_file_type f) of
+ − 320
Some t \<Rightarrow> Some (NormalFile_type t)
+ − 321
| _ \<Rightarrow> Some InheritParent_file_type)
+ − 322
else None)"
+ − 323
+ − 324
fun type_of_file :: "t_state \<Rightarrow> (t_file \<rightharpoonup> t_rc_file_type)" (* (6) *)
+ − 325
where
+ − 326
"type_of_file [] = init_file_type_aux"
+ − 327
| "type_of_file (CreateFile p f # s) = (
+ − 328
case (currentrole s p) of
+ − 329
Some r \<Rightarrow> (type_of_file s) (f := Some (default_fd_create_type r))
+ − 330
| _ \<Rightarrow> (type_of_file s) (f := None))"
+ − 331
| "type_of_file (_ # s) = type_of_file s" (* add by wch *)
+ − 332
+ − 333
fun etype_aux:: "(t_file \<rightharpoonup> t_rc_file_type) \<Rightarrow> (t_file \<rightharpoonup> t_normal_file_type)"
+ − 334
where
+ − 335
"etype_aux typf [] = (
+ − 336
case (typf []) of
+ − 337
Some InheritParent_file_type \<Rightarrow> Some Root_file_type
+ − 338
| Some (NormalFile_type t) \<Rightarrow> Some t
+ − 339
| None \<Rightarrow> None )"
+ − 340
| "etype_aux typf (n#ns) = (
+ − 341
case (typf (n#ns)) of
+ − 342
Some InheritParent_file_type \<Rightarrow> etype_aux typf ns
+ − 343
| Some (NormalFile_type t) \<Rightarrow> Some t
+ − 344
| None \<Rightarrow> None )"
+ − 345
+ − 346
definition etype_of_file :: "t_state \<Rightarrow> (t_file \<rightharpoonup> t_normal_file_type)"
+ − 347
(* etype is always normal *)
+ − 348
where
+ − 349
"etype_of_file s \<equiv> etype_aux (type_of_file s)"
+ − 350
+ − 351
definition pct :: "t_state \<Rightarrow> (t_process \<rightharpoonup> t_rc_proc_type)"
+ − 352
where
+ − 353
"pct s p \<equiv> (case (currentrole s p) of
+ − 354
Some r \<Rightarrow> Some (default_process_create_type r)
+ − 355
| _ \<Rightarrow> None)"
+ − 356
+ − 357
definition pet :: "t_state \<Rightarrow> (t_process \<rightharpoonup> t_rc_proc_type)"
+ − 358
where
+ − 359
"pet s p \<equiv> (case (currentrole s p) of
+ − 360
Some r \<Rightarrow> Some (default_process_execute_type r)
+ − 361
| _ \<Rightarrow> None)"
+ − 362
+ − 363
definition pot :: "t_state \<Rightarrow> (t_process \<rightharpoonup> t_rc_proc_type)"
+ − 364
where
+ − 365
"pot s p \<equiv> (case (currentrole s p) of
+ − 366
Some r \<Rightarrow> Some (default_process_chown_type r)
+ − 367
| _ \<Rightarrow> None)"
+ − 368
+ − 369
fun type_of_process :: "t_state \<Rightarrow> (t_process \<rightharpoonup> t_normal_proc_type)"
+ − 370
where
+ − 371
"type_of_process [] = init_process_type"
+ − 372
| "type_of_process (Clone p p' # \<tau>) = (type_of_process \<tau>) (p' :=
+ − 373
case (pct \<tau> p) of
+ − 374
Some InheritParent_proc_type \<Rightarrow> type_of_process \<tau> p
+ − 375
| Some (NormalProc_type tp) \<Rightarrow> Some tp
+ − 376
| _ \<Rightarrow> None )" (*6.80*)
+ − 377
| "type_of_process (Execute p f # \<tau>) = (type_of_process \<tau>) (p :=
+ − 378
case (pet \<tau> p) of
+ − 379
Some InheritParent_proc_type \<Rightarrow> type_of_process \<tau> p
+ − 380
| Some (NormalProc_type tp) \<Rightarrow> Some tp
+ − 381
| _ \<Rightarrow> None )" (*6.82*)
+ − 382
| "type_of_process (ChangeOwner p u # \<tau>) = (type_of_process \<tau>) (p :=
+ − 383
case (pot \<tau> p) of
+ − 384
Some InheritParent_proc_type \<Rightarrow> type_of_process \<tau> p
+ − 385
| Some UseNewRoleType \<Rightarrow> (case (pct (ChangeOwner p u # \<tau>) p) of
+ − 386
Some InheritParent_proc_type \<Rightarrow> type_of_process \<tau> p
+ − 387
| Some (NormalProc_type tp) \<Rightarrow> Some tp
+ − 388
| _ \<Rightarrow> None)
+ − 389
| Some (NormalProc_type tp) \<Rightarrow> Some tp
+ − 390
| _ \<Rightarrow> None )" (* the UseNewRoleType case is refered with Nordsec paper 4 (11), and it is not right??! of just
+ − 391
use "pct" *)
+ − 392
| "type_of_process (_ # \<tau>) = type_of_process \<tau>"
+ − 393
+ − 394
fun type_of_ipc :: "t_state \<Rightarrow> (t_ipc \<rightharpoonup> t_normal_ipc_type)" (* (14) *)
+ − 395
where
+ − 396
"type_of_ipc [] = init_ipc_type"
+ − 397
| "type_of_ipc (CreateIPC p i # s) = (type_of_ipc s) (i :=
+ − 398
case (currentrole s p) of
+ − 399
Some r \<Rightarrow> Some (default_ipc_create_type r)
+ − 400
| _ \<Rightarrow> None )"
+ − 401
| "type_of_ipc (_ # s) = type_of_ipc s" (* add by wch *)
+ − 402
+ − 403
(*** RC access control ***)
+ − 404
fun rc_grant :: "t_state \<Rightarrow> t_event \<Rightarrow> bool"
+ − 405
where
+ − 406
"rc_grant \<tau> (CreateFile p f) = (
+ − 407
case (parent f) of
+ − 408
Some pf \<Rightarrow> (
+ − 409
case (currentrole \<tau> p, etype_of_file \<tau> pf) of
+ − 410
(Some r, Some t) \<Rightarrow> (
+ − 411
case (default_fd_create_type r) of
+ − 412
InheritParent_file_type \<Rightarrow> (r, File_type t, WRITE) \<in> compatible
+ − 413
| NormalFile_type t' \<Rightarrow> (r, File_type t, WRITE) \<in> compatible \<and> (r, File_type t', CREATE) \<in> compatible
+ − 414
)
+ − 415
| _ \<Rightarrow> False )
+ − 416
| _ \<Rightarrow> False )"
+ − 417
| "rc_grant \<tau> (ReadFile p f) = (
+ − 418
case (currentrole \<tau> p, etype_of_file \<tau> f) of
+ − 419
(Some r, Some t) \<Rightarrow> (r, File_type t, READ) \<in> compatible
+ − 420
| _ \<Rightarrow> False )"
+ − 421
| "rc_grant \<tau> (WriteFile p f) = (
+ − 422
case (currentrole \<tau> p, etype_of_file \<tau> f) of
+ − 423
(Some r, Some t) \<Rightarrow> (r, File_type t, WRITE) \<in> compatible
+ − 424
| _ \<Rightarrow> False )"
+ − 425
| "rc_grant \<tau> (Execute p f) = (
+ − 426
case (currentrole \<tau> p, etype_of_file \<tau> f) of
+ − 427
(Some r, Some t) \<Rightarrow> (r, File_type t, EXECUTE) \<in> compatible
+ − 428
| _ \<Rightarrow> False )"
+ − 429
| "rc_grant \<tau> (ChangeOwner p u) = (
+ − 430
case (currentrole \<tau> p, type_of_process \<tau> p) of
+ − 431
(Some r, Some t) \<Rightarrow> (r, Proc_type t, CHANGE_OWNER) \<in> compatible
+ − 432
| _ \<Rightarrow> False )"
+ − 433
| "rc_grant \<tau> (Clone p newproc) = (
+ − 434
case (currentrole \<tau> p, type_of_process \<tau> p) of
+ − 435
(Some r, Some t) \<Rightarrow> (r, Proc_type t, CREATE) \<in> compatible
+ − 436
| _ \<Rightarrow> False )" (* premiss of no limit to clone is removed to locale assumptions *)
+ − 437
| "rc_grant \<tau> (ChangeRole p r) = (
+ − 438
case (currentrole \<tau> p) of
+ − 439
Some cr \<Rightarrow> r \<in> comproles cr
+ − 440
| _ \<Rightarrow> False )"
+ − 441
| "rc_grant \<tau> (Send p i) = (
+ − 442
case (currentrole \<tau> p, type_of_ipc \<tau> i) of
+ − 443
(Some r, Some t) \<Rightarrow> (r, IPC_type t, SEND) \<in> compatible
+ − 444
| _ \<Rightarrow> False )"
+ − 445
| "rc_grant \<tau> (Recv p i) = (
+ − 446
case (currentrole \<tau> p, type_of_ipc \<tau> i) of
+ − 447
(Some r, Some t) \<Rightarrow> (r, IPC_type t, RECEIVE) \<in> compatible
+ − 448
| _ \<Rightarrow> False )"
+ − 449
| "rc_grant \<tau> (CreateIPC p i) = (
+ − 450
case (currentrole \<tau> p) of
+ − 451
Some r \<Rightarrow> (r, IPC_type (default_ipc_create_type r), CREATE) \<in> compatible
+ − 452
| _ \<Rightarrow> False )"
+ − 453
| "rc_grant \<tau> (DeleteFile p f) = (
+ − 454
case (currentrole \<tau> p, etype_of_file \<tau> f) of
+ − 455
(Some r, Some t) \<Rightarrow> (r, File_type t, DELETE) \<in> compatible
+ − 456
| _ \<Rightarrow> False )"
+ − 457
| "rc_grant \<tau> (DeleteIPC p i) = (
+ − 458
case (currentrole \<tau> p, type_of_ipc \<tau> i) of
+ − 459
(Some r, Some t) \<Rightarrow> (r, IPC_type t, DELETE) \<in> compatible
+ − 460
| _ \<Rightarrow> False )"
+ − 461
| "rc_grant \<tau> (Kill p p') = (
+ − 462
case (currentrole \<tau> p, type_of_process \<tau> p') of
+ − 463
(Some r, Some t) \<Rightarrow> (r, Proc_type t, DELETE) \<in> compatible
+ − 464
| _ \<Rightarrow> False )"
+ − 465
+ − 466
(* new file pathname is user-defined, so os just check if its unexistence *)
+ − 467
fun os_grant :: "t_state \<Rightarrow> t_event \<Rightarrow> bool"
+ − 468
where
+ − 469
"os_grant \<tau> (Execute p f) = (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau>)"
+ − 470
| "os_grant \<tau> (CreateFile p f) = (p \<in> current_procs \<tau> \<and> f \<notin> current_files \<tau> \<and> (\<exists> pf. (parent f = Some pf) \<and> pf \<in> current_files \<tau>))" (*cannot create disk, ?? or f = [] ??*)
+ − 471
| "os_grant \<tau> (ChangeRole p r) = (p \<in> current_procs \<tau>)"
+ − 472
| "os_grant \<tau> (ReadFile p f) = (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau>)"
+ − 473
| "os_grant \<tau> (WriteFile p f) = (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau>)"
+ − 474
| "os_grant \<tau> (ChangeOwner p u)= (p \<in> current_procs \<tau> \<and> u \<in> init_users)"
6
+ − 475
| "os_grant \<tau> (CreateIPC p i) = (p \<in> current_procs \<tau> \<and> i \<notin> current_ipcs \<tau>)" (* i = new_ipc \<tau> *)
1
+ − 476
| "os_grant \<tau> (Send p i) = (p \<in> current_procs \<tau> \<and> i \<in> current_ipcs \<tau>)"
+ − 477
| "os_grant \<tau> (Recv p i) = (p \<in> current_procs \<tau> \<and> i \<in> current_ipcs \<tau>)"
6
+ − 478
| "os_grant \<tau> (Clone p p') = (p \<in> current_procs \<tau> \<and> p' \<notin> current_procs \<tau>)" (* p' = new_proc \<tau> *)
1
+ − 479
| "os_grant \<tau> (Kill p p') = (p \<in> current_procs \<tau> \<and> p' \<in> current_procs \<tau>)"
+ − 480
| "os_grant \<tau> (DeleteFile p f) = (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau> \<and> \<not> (\<exists>fn. fn # f \<in> current_files \<tau>))"
+ − 481
| "os_grant \<tau> (DeleteIPC p i) = (p \<in> current_procs \<tau> \<and> i \<in> current_ipcs \<tau>)"
+ − 482
+ − 483
(**** system valid state ****)
+ − 484
+ − 485
inductive valid :: "t_state \<Rightarrow> bool"
+ − 486
where
+ − 487
vs_nil: "valid []"
+ − 488
| vs_step: "\<lbrakk>valid s; os_grant s e; rc_grant s e\<rbrakk> \<Longrightarrow> valid (e # s)"
+ − 489
+ − 490
end
+ − 491
+ − 492
(*** more RC constrains of type system in formalisation ***)
+ − 493
+ − 494
locale rc_basic = init +
+ − 495
assumes
+ − 496
init_initialrole_valid: "\<And> f r. init_initialrole f = Some r \<Longrightarrow> r = InheritParentRole \<or> r = UseForcedRole \<or> (\<exists> nr. r = NormalRole nr)" (* 6.10 *)
+ − 497
and init_forcedrole_valid: "\<And> f r. init_forcedrole f = Some r \<Longrightarrow> r = InheritUserRole \<or> r = InheritProcessRole \<or> r = InheritParentRole \<or> r = InheritUpMixed \<or> (\<exists> nr. r = NormalRole nr)" (* 6.11 *)
+ − 498
and init_proc_forcedrole_valid: "\<And> p r. init_proc_forcedrole p = Some r \<Longrightarrow> r = InheritUserRole \<or> r = InheritProcessRole \<or> r = InheritUpMixed \<or> (\<exists> nr. r = NormalRole nr)" (* 6.7 *)
+ − 499
and default_fd_create_type_valid: "\<And> nr t. default_fd_create_type nr = t \<Longrightarrow> t = InheritParent_file_type \<or> (\<exists> nt. t = NormalFile_type nt)" (*6.16*)
+ − 500
and default_process_create_type_valid: "\<And> nr t. default_process_create_type nr = t \<Longrightarrow> t = InheritParent_proc_type \<or> (\<exists> nt. t = NormalProc_type nt)" (*6.18*)
+ − 501
and default_process_chown_type_valid: "\<And> nr t. default_process_chown_type nr = t \<Longrightarrow> t = InheritParent_proc_type \<or> t = UseNewRoleType \<or> (\<exists> nt. t = NormalProc_type nt)" (*6.19*)
+ − 502
and default_process_execute_type_valid: "\<And> nr t. default_process_execute_type nr = t \<Longrightarrow> t = InheritParent_proc_type \<or> (\<exists> nt. t = NormalProc_type nt)" (*6.20*)
+ − 503
+ − 504
begin
+ − 505
+ − 506
lemma init_file_initialrole_valid: "init_file_initialrole f = Some r \<Longrightarrow> r = InheritParentRole \<or> r = UseForcedRole \<or> (\<exists> nr. r = NormalRole nr)"
+ − 507
apply (induct f)
+ − 508
by (auto simp:init_file_initialrole.simps dest:init_initialrole_valid split:option.splits)
+ − 509
+ − 510
lemma initialrole_valid: "initialrole \<tau> f = Some r \<Longrightarrow> r = InheritParentRole \<or> r = UseForcedRole \<or> (\<exists> nr. r = NormalRole nr)" (* 6.10 *)
+ − 511
apply (induct \<tau> arbitrary:f) defer
+ − 512
apply (case_tac a)
+ − 513
apply (auto simp:initialrole.simps dest:init_file_initialrole_valid
+ − 514
split:option.splits if_splits)
+ − 515
done
+ − 516
+ − 517
lemma effinitialrole_valid: "effinitialrole \<tau> f = Some r \<Longrightarrow> r = UseForcedRole \<or> (\<exists> nr. r = NormalRole nr)"
+ − 518
apply (induct f)
+ − 519
apply (auto simp:effinitialrole_def dest:initialrole_valid split:option.splits if_splits)
+ − 520
done
+ − 521
+ − 522
lemma init_file_forcedrole_valid:
+ − 523
"init_file_forcedrole f = Some r \<Longrightarrow> r = InheritUserRole \<or> r = InheritProcessRole \<or> r = InheritParentRole \<or> r = InheritUpMixed \<or> (\<exists> nr. r = NormalRole nr)"
+ − 524
apply (induct f)
+ − 525
by (auto simp:init_file_forcedrole.simps dest:init_forcedrole_valid split:option.splits)
+ − 526
+ − 527
lemma forcedrole_valid: "forcedrole \<tau> f = Some r \<Longrightarrow> r = InheritUserRole \<or> r = InheritProcessRole \<or> r = InheritParentRole \<or> r = InheritUpMixed \<or> (\<exists> nr. r = NormalRole nr)" (* 6.10 *)
+ − 528
apply (induct \<tau> arbitrary:f) defer
+ − 529
apply (case_tac a)
+ − 530
apply (auto simp:forcedrole.simps dest:init_file_forcedrole_valid
+ − 531
split:option.splits if_splits)
+ − 532
done
+ − 533
+ − 534
lemma effforcedrole_valid: "effforcedrole \<tau> f = Some r \<Longrightarrow> r = InheritUserRole \<or> r = InheritProcessRole \<or> r = InheritUpMixed \<or> (\<exists> nr. r = NormalRole nr)"
+ − 535
apply (induct f)
+ − 536
apply (auto simp:effforcedrole_def dest:forcedrole_valid split:option.splits if_splits)
+ − 537
done
+ − 538
+ − 539
lemma proc_forcedrole_valid: "proc_forcedrole \<tau> p = Some r \<Longrightarrow> r = InheritUserRole \<or> r = InheritProcessRole \<or> r = InheritUpMixed \<or> (\<exists> nr. r = NormalRole nr)" (* 6.7 *)
+ − 540
apply (induct \<tau> arbitrary:p) defer
+ − 541
apply (case_tac a)
+ − 542
apply (auto simp:proc_forcedrole.simps dest:init_proc_forcedrole_valid effforcedrole_valid
+ − 543
split:option.splits if_splits)
+ − 544
done
+ − 545
+ − 546
lemma pct_valid: "pct \<tau> p = Some t \<Longrightarrow> t = InheritParent_proc_type \<or> (\<exists> nt. t = NormalProc_type nt)"
+ − 547
by (auto simp:pct_def default_process_create_type_valid split:option.splits)
+ − 548
+ − 549
lemma pot_valid: "pot \<tau> p = Some t \<Longrightarrow> t = InheritParent_proc_type \<or> t = UseNewRoleType \<or> (\<exists> nt. t = NormalProc_type nt)"
+ − 550
by (auto simp:pot_def default_process_chown_type_valid split:option.splits)
+ − 551
+ − 552
lemma pet_valid: "pet \<tau> p = Some t \<Longrightarrow> t = InheritParent_proc_type \<or> (\<exists> nt. t = NormalProc_type nt)"
+ − 553
by (simp add:pet_def default_process_execute_type_valid map_comp_def split:option.splits)
+ − 554
+ − 555
end
+ − 556
+ − 557
(******* Reachable/tainting related type definitions ********)
+ − 558
+ − 559
datatype t_object =
+ − 560
Proc "t_process"
+ − 561
| File "t_file"
+ − 562
| IPC "t_ipc"
+ − 563
+ − 564
fun object_in_init :: "t_object \<Rightarrow> t_file set \<Rightarrow> t_process set \<Rightarrow> t_ipc set \<Rightarrow> bool"
+ − 565
where
+ − 566
"object_in_init (Proc p) init_files init_procs init_ipcs = (p \<in> init_procs)"
+ − 567
| "object_in_init (File f) init_files init_procs init_ipcs = (f \<in> init_files)"
+ − 568
| "object_in_init (IPC i) init_files init_procs init_ipcs = (i \<in> init_ipcs)"
+ − 569
+ − 570
(*** locale for dynamic tainting ***)
+ − 571
+ − 572
locale tainting = rc_basic +
+ − 573
+ − 574
fixes seeds :: "t_object set"
+ − 575
+ − 576
assumes
+ − 577
seeds_in_init: "\<And> obj. obj \<in> seeds \<Longrightarrow> object_in_init obj init_files init_processes init_ipcs"
+ − 578
begin
+ − 579
+ − 580
lemma finite_seeds: "finite seeds"
+ − 581
proof-
+ − 582
have "finite {obj. object_in_init obj init_files init_processes init_ipcs}"
+ − 583
proof-
+ − 584
have "finite {File f| f. f \<in> init_files}"
+ − 585
using init_finite by auto
+ − 586
moreover have "finite {Proc p| p. p \<in> init_processes}"
+ − 587
using init_finite by auto
+ − 588
moreover have "finite {IPC i| i. i \<in> init_ipcs}"
+ − 589
using init_finite by auto
+ − 590
ultimately have "finite ({File f| f. f \<in> init_files} \<union> {Proc p| p. p \<in> init_processes} \<union> {IPC i| i. i \<in> init_ipcs})"
+ − 591
by auto
+ − 592
thus ?thesis
+ − 593
apply (rule_tac B = "({File f| f. f \<in> init_files} \<union> {Proc p| p. p \<in> init_processes} \<union> {IPC i| i. i \<in> init_ipcs})" in finite_subset)
+ − 594
by (auto, case_tac x, simp+)
+ − 595
qed
+ − 596
with seeds_in_init
+ − 597
show ?thesis
+ − 598
by (rule_tac finite_subset, auto)
+ − 599
qed
+ − 600
+ − 601
fun exists :: "t_state \<Rightarrow> t_object \<Rightarrow> bool"
+ − 602
where
+ − 603
"exists s (File f) = (f \<in> current_files s)"
+ − 604
| "exists s (Proc p) = (p \<in> current_procs s)"
+ − 605
| "exists s (IPC i) = (i \<in> current_ipcs s)"
+ − 606
+ − 607
inductive tainted :: "t_object \<Rightarrow> t_state \<Rightarrow> bool" ("_ \<in> tainted _" [100, 100] 100)
+ − 608
where
+ − 609
t_init: "obj \<in> seeds \<Longrightarrow> obj \<in> tainted []"
+ − 610
| t_clone: "\<lbrakk>Proc p \<in> tainted s; valid (Clone p p' # s)\<rbrakk> \<Longrightarrow> Proc p' \<in> tainted (Clone p p' # s)"
+ − 611
| t_exec: "\<lbrakk>File f \<in> tainted s; valid (Execute p f # s)\<rbrakk> \<Longrightarrow> Proc p \<in> tainted (Execute p f # s)"
+ − 612
| t_cfile: "\<lbrakk>Proc p \<in> tainted s; valid (CreateFile p f # s)\<rbrakk> \<Longrightarrow> File f \<in> tainted (CreateFile p f # s)"
+ − 613
| t_cipc: "\<lbrakk>Proc p \<in> tainted s; valid (CreateIPC p i # s)\<rbrakk> \<Longrightarrow> IPC i \<in> tainted (CreateIPC p i # s)"
+ − 614
| t_read: "\<lbrakk>File f \<in> tainted s; valid (ReadFile p f # s)\<rbrakk> \<Longrightarrow> Proc p \<in> tainted (ReadFile p f # s)"
+ − 615
| t_write: "\<lbrakk>Proc p \<in> tainted s; valid (WriteFile p f # s)\<rbrakk> \<Longrightarrow> File f \<in> tainted (WriteFile p f # s)"
+ − 616
| t_send: "\<lbrakk>Proc p \<in> tainted s; valid (Send p i # s)\<rbrakk> \<Longrightarrow> IPC i \<in> tainted (Send p i # s)"
+ − 617
| t_recv: "\<lbrakk>IPC i \<in> tainted s; valid (Recv p i # s)\<rbrakk> \<Longrightarrow> Proc p \<in> tainted (Recv p i # s)"
+ − 618
| t_remain:"\<lbrakk>obj \<in> tainted s; valid (e # s); exists (e # s) obj\<rbrakk> \<Longrightarrow> obj \<in> tainted (e # s)"
+ − 619
+ − 620
definition taintable:: "t_object \<Rightarrow> bool"
+ − 621
where
+ − 622
"taintable obj \<equiv> \<exists> s. obj \<in> tainted s"
+ − 623
+ − 624
fun deleted :: "t_object \<Rightarrow> t_event list \<Rightarrow> bool"
+ − 625
where
+ − 626
"deleted obj [] = False"
+ − 627
| "deleted obj (Kill p p' # \<tau>) = ((obj = Proc p') \<or> deleted obj \<tau>)"
+ − 628
| "deleted obj (DeleteFile p f # \<tau>) = ((obj = File f) \<or> deleted obj \<tau>)"
+ − 629
| "deleted obj (DeleteIPC p i # \<tau>) = ((obj = IPC i) \<or> deleted obj \<tau>)"
+ − 630
| "deleted obj (_ # \<tau>) = deleted obj \<tau>"
+ − 631
+ − 632
definition undeletable :: "t_object \<Rightarrow> bool"
+ − 633
where
+ − 634
"undeletable obj \<equiv> exists [] obj \<and> \<not> (\<exists> s. valid s \<and> deleted obj s)"
+ − 635
+ − 636
fun no_del_event:: "t_event list \<Rightarrow> bool"
+ − 637
where
+ − 638
"no_del_event [] = True"
+ − 639
| "no_del_event (Kill p p' # \<tau>) = False"
+ − 640
| "no_del_event (DeleteFile p f # \<tau>) = False"
+ − 641
| "no_del_event (DeleteIPC p i # \<tau>) = False"
+ − 642
| "no_del_event (_ # \<tau>) = no_del_event \<tau>"
+ − 643
+ − 644
end
+ − 645
+ − 646
+ − 647
(***** locale for statical world *****)
+ − 648
+ − 649
type_synonym t_sprocess = "t_normal_role \<times> t_role \<times> t_normal_proc_type \<times> t_user"
+ − 650
+ − 651
type_synonym t_sfile = "t_normal_file_type \<times> t_file"
+ − 652
+ − 653
type_synonym t_sipc = "t_normal_ipc_type"
+ − 654
+ − 655
datatype t_sobject =
+ − 656
SProc "t_sprocess" "t_process option"
+ − 657
| SFile "t_sfile" "t_file option"
+ − 658
| SIPC "t_sipc" "t_ipc option"
+ − 659
| Unknown
+ − 660
+ − 661
locale tainting_s_complete = tainting
+ − 662
+ − 663
begin
+ − 664
+ − 665
definition chown_role_aux:: "t_normal_role \<Rightarrow> t_role \<Rightarrow> t_user \<Rightarrow> t_normal_role option"
+ − 666
where
+ − 667
"chown_role_aux cr fr u \<equiv> (
+ − 668
case fr of
+ − 669
NormalRole r \<Rightarrow> Some r
+ − 670
| InheritProcessRole \<Rightarrow> Some cr
+ − 671
| _ \<Rightarrow> defrole u )"
+ − 672
+ − 673
definition chown_type_aux:: "t_normal_role \<Rightarrow> t_normal_role \<Rightarrow> t_normal_proc_type \<Rightarrow> t_normal_proc_type"
+ − 674
where
+ − 675
"chown_type_aux cr nr t \<equiv> (
+ − 676
case (default_process_chown_type cr) of
+ − 677
InheritParent_proc_type \<Rightarrow> t
+ − 678
| UseNewRoleType \<Rightarrow> (case (default_process_create_type nr) of
+ − 679
InheritParent_proc_type \<Rightarrow> t
+ − 680
| NormalProc_type tp \<Rightarrow> tp)
+ − 681
| NormalProc_type tp \<Rightarrow> tp )"
+ − 682
+ − 683
definition exec_type_aux :: "t_normal_role \<Rightarrow> t_normal_proc_type \<Rightarrow> t_normal_proc_type"
+ − 684
where
+ − 685
"exec_type_aux cr t \<equiv> (case (default_process_execute_type cr) of
+ − 686
InheritParent_proc_type \<Rightarrow> t
+ − 687
| NormalProc_type tp \<Rightarrow>tp)"
+ − 688
+ − 689
definition exec_role_aux :: "t_normal_role \<Rightarrow> t_file \<Rightarrow> t_user \<Rightarrow> t_normal_role option"
+ − 690
where
+ − 691
"exec_role_aux cr sd u \<equiv> (
+ − 692
case (erole_functor init_file_initialrole UseForcedRole sd) of
+ − 693
Some ir \<Rightarrow> (case ir of
+ − 694
NormalRole r \<Rightarrow> Some r
+ − 695
| UseForcedRole \<Rightarrow> (
+ − 696
case (erole_functor init_file_forcedrole InheritUpMixed sd) of
+ − 697
Some fr \<Rightarrow> (case fr of
+ − 698
NormalRole r \<Rightarrow> Some r
+ − 699
| InheritUserRole \<Rightarrow> defrole u
+ − 700
| _ \<Rightarrow> Some cr )
+ − 701
| None \<Rightarrow> None )
+ − 702
| _ \<Rightarrow> None )
+ − 703
| _ \<Rightarrow> None )"
+ − 704
+ − 705
definition clone_type_aux :: "t_normal_role \<Rightarrow> t_normal_proc_type \<Rightarrow> t_normal_proc_type"
+ − 706
where
+ − 707
"clone_type_aux r t \<equiv> (case (default_process_create_type r) of
+ − 708
InheritParent_proc_type \<Rightarrow> t
+ − 709
| NormalProc_type tp \<Rightarrow> tp)"
+ − 710
+ − 711
(* all the static objects that dynamic objects referring to *)
+ − 712
(* they should all be in a finite set ? *)
+ − 713
(* besides, they're no clone case for all_sobjs, we have no "SProc ... None" case, Clone p p', p' statically viewed as p too, so the many2many mapping becomes to many2one, which makes all succeeded*)
+ − 714
inductive_set all_sobjs :: "t_sobject set"
+ − 715
where
+ − 716
af_init: "\<lbrakk>f \<in> init_files; etype_aux init_file_type_aux f = Some t\<rbrakk> \<Longrightarrow> SFile (t, f) (Some f) \<in> all_sobjs"
+ − 717
| af_cfd: "\<lbrakk>SFile (t, sd) sf \<in> all_sobjs; SProc (r, fr, pt, u) sp \<in> all_sobjs; default_fd_create_type r = NormalFile_type t'; (r, File_type t, WRITE) \<in> compatible; (r, File_type t', CREATE) \<in> compatible\<rbrakk> \<Longrightarrow> SFile (t', sd) None \<in> all_sobjs"
+ − 718
| af_cfd': "\<lbrakk>SFile (t, sd) sf \<in> all_sobjs; SProc (r, fr, pt, u) sp \<in> all_sobjs; default_fd_create_type r = InheritParent_file_type; (r, File_type t, WRITE) \<in> compatible\<rbrakk> \<Longrightarrow> SFile (t, sd) None \<in> all_sobjs"
+ − 719
+ − 720
| ai_init: "init_ipc_type i = Some t \<Longrightarrow> SIPC t (Some i) \<in> all_sobjs"
+ − 721
| ai_cipc: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> all_sobjs; (r, IPC_type (default_ipc_create_type r), CREATE) \<in> compatible\<rbrakk> \<Longrightarrow> SIPC (default_ipc_create_type r) None \<in> all_sobjs"
+ − 722
+ − 723
| ap_init: "\<lbrakk>init_currentrole p = Some r; init_proc_forcedrole p = Some fr; init_process_type p = Some t; init_owner p = Some u\<rbrakk> \<Longrightarrow> SProc (r, fr, t, u) (Some p) \<in> all_sobjs"
+ − 724
| ap_crole: "\<lbrakk>SProc (r, fr, t, u) sp \<in> all_sobjs; r' \<in> comproles r\<rbrakk> \<Longrightarrow> SProc (r', fr, t, u) sp \<in> all_sobjs"
+ − 725
| ap_chown: "\<lbrakk>SProc (r, fr, t, u') sp \<in> all_sobjs; u \<in> init_users; chown_role_aux r fr u = Some nr; (r, Proc_type t, CHANGE_OWNER) \<in> compatible\<rbrakk> \<Longrightarrow> SProc (nr, fr, chown_type_aux r nr t, u) sp \<in> all_sobjs"
+ − 726
| ap_exec: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> all_sobjs; SFile (t, sd) sf \<in> all_sobjs; (r, File_type t, EXECUTE) \<in> compatible; exec_role_aux r sd u = Some r'; erole_functor init_file_forcedrole InheritUpMixed sd = Some fr'\<rbrakk> \<Longrightarrow> SProc (r', fr', exec_type_aux r pt, u) sp \<in> all_sobjs"
+ − 727
| ap_clone: "SProc (r, fr, pt, u) sp \<in> all_sobjs \<Longrightarrow> SProc (r, fr, clone_type_aux r pt, u) sp \<in> all_sobjs"
+ − 728
+ − 729
fun init_obj2sobj :: "t_object \<Rightarrow> t_sobject"
+ − 730
where
+ − 731
"init_obj2sobj (File f) = (
+ − 732
case (etype_aux init_file_type_aux f) of
+ − 733
Some t \<Rightarrow> SFile (t, f) (Some f)
+ − 734
| _ \<Rightarrow> Unknown )"
+ − 735
| "init_obj2sobj (Proc p) = (
+ − 736
case (init_currentrole p, init_proc_forcedrole p, init_process_type p, init_owner p) of
+ − 737
(Some r, Some fr, Some t, Some u) \<Rightarrow> SProc (r, fr, t, u) (Some p)
+ − 738
| _ \<Rightarrow> Unknown )"
+ − 739
| "init_obj2sobj (IPC i) = (
+ − 740
case (init_ipc_type i) of
+ − 741
Some t \<Rightarrow> SIPC t (Some i)
+ − 742
| _ \<Rightarrow> Unknown )"
+ − 743
+ − 744
inductive_set tainted_s :: "t_sobject set"
+ − 745
where
+ − 746
ts_init: "obj \<in> seeds \<Longrightarrow> init_obj2sobj obj \<in> tainted_s"
+ − 747
| ts_exec1: "\<lbrakk>SFile (t, sd) sf \<in> tainted_s; SProc (r, fr, pt, u) sp \<in> all_sobjs; (r, File_type t, EXECUTE) \<in> compatible; exec_role_aux r sd u = Some r'; erole_functor init_file_forcedrole InheritUpMixed sd = Some fr'\<rbrakk> \<Longrightarrow> SProc (r', fr', exec_type_aux r pt, u) sp \<in> tainted_s"
+ − 748
| ts_exec2: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s; SFile (t, sd) sf \<in> all_sobjs; (r, File_type t, EXECUTE) \<in> compatible; exec_role_aux r sd u = Some r'; erole_functor init_file_forcedrole InheritUpMixed sd = Some fr'\<rbrakk> \<Longrightarrow> SProc (r', fr', exec_type_aux r pt, u) sp \<in> tainted_s"
+ − 749
| ts_cfd: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s; SFile (t, sd) sf \<in> all_sobjs; default_fd_create_type r = NormalFile_type t'; (r, File_type t, WRITE) \<in> compatible; (r, File_type t', CREATE) \<in> compatible\<rbrakk> \<Longrightarrow> SFile (t', sd) None \<in> tainted_s"
+ − 750
| ts_cfd': "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s; SFile (t, sd) sf \<in> all_sobjs; default_fd_create_type r = InheritParent_file_type; (r, File_type t, WRITE) \<in> compatible\<rbrakk> \<Longrightarrow> SFile (t, sd) None \<in> tainted_s"
+ − 751
| ts_cipc: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s; (r, IPC_type (default_ipc_create_type r), CREATE) \<in> compatible\<rbrakk> \<Longrightarrow> SIPC (default_ipc_create_type r) None \<in> tainted_s"
+ − 752
| ts_read: "\<lbrakk>SFile (t, sd) sf \<in> tainted_s; SProc (r, fr, pt, u) sp \<in> all_sobjs; (r, File_type t, READ) \<in> compatible\<rbrakk> \<Longrightarrow> SProc (r, fr, pt, u) sp \<in> tainted_s"
+ − 753
| ts_write: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s; SFile (t, sd) sf \<in> all_sobjs; (r, File_type t, WRITE) \<in> compatible\<rbrakk> \<Longrightarrow> SFile (t, sd) sf \<in> tainted_s"
+ − 754
| ts_recv: "\<lbrakk>SIPC t si \<in> tainted_s; SProc (r, fr, pt, u) sp \<in> all_sobjs; (r, IPC_type t, RECEIVE) \<in> compatible\<rbrakk> \<Longrightarrow> SProc (r, fr, pt, u) sp \<in> tainted_s"
+ − 755
| ts_send: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s; SIPC t si \<in> all_sobjs; (r, IPC_type t, SEND) \<in> compatible\<rbrakk> \<Longrightarrow> SIPC t si \<in> tainted_s"
+ − 756
| ts_crole: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s; r' \<in> comproles r\<rbrakk> \<Longrightarrow> SProc (r', fr, pt, u) sp \<in> tainted_s"
+ − 757
| ts_chown: "\<lbrakk>SProc (r, fr, t, u') sp \<in> tainted_s; u \<in> init_users; chown_role_aux r fr u = Some nr; (r, Proc_type t, CHANGE_OWNER) \<in> compatible\<rbrakk> \<Longrightarrow> SProc (nr, fr, chown_type_aux r nr t, u) sp \<in> tainted_s"
+ − 758
| ts_clone: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s; (r, Proc_type pt, CREATE) \<in> compatible\<rbrakk> \<Longrightarrow> SProc (r, fr, clone_type_aux r pt, u) sp \<in> tainted_s"
+ − 759
+ − 760
(*** mapping function from dynamic 2 statical ****)
+ − 761
+ − 762
fun source_dir:: "t_state \<Rightarrow> t_file \<Rightarrow> t_file option"
+ − 763
where
+ − 764
"source_dir s [] = (if ([] \<in> init_files \<and> \<not> (deleted (File []) s))
+ − 765
then Some []
+ − 766
else None
+ − 767
)"
+ − 768
| "source_dir s (f#pf) = (if ((f#pf) \<in> init_files \<and> \<not> (deleted (File (f#pf)) s))
+ − 769
then Some (f#pf)
+ − 770
else source_dir s pf
+ − 771
)"
+ − 772
+ − 773
(* cf2sfile's properities should all be under condition: f is not deleted in \<tau>*)
+ − 774
fun cf2sfile:: "t_state \<Rightarrow> t_file \<Rightarrow> t_sfile option"
+ − 775
where
+ − 776
"cf2sfile s f = (case (etype_of_file s f, source_dir s f) of
+ − 777
(Some t, Some sd) \<Rightarrow> Some (t, sd)
+ − 778
| _ \<Rightarrow> None)"
+ − 779
+ − 780
fun cp2sproc:: "t_state \<Rightarrow> t_process \<Rightarrow> t_sprocess option"
+ − 781
where
+ − 782
"cp2sproc s p = (case (currentrole s p, proc_forcedrole s p, type_of_process s p, owner s p) of
+ − 783
(Some r, Some fr, Some t, Some u) \<Rightarrow> Some (r, fr, t, u)
+ − 784
| _ \<Rightarrow> None)"
+ − 785
+ − 786
fun ci2sipc:: "t_state \<Rightarrow> t_ipc \<Rightarrow> t_sipc option"
+ − 787
where
+ − 788
"ci2sipc s i = (type_of_ipc s i)"
+ − 789
+ − 790
(*** in statical view, clone event is process to try different runs(different sprocess:role/type...),
+ − 791
so statically these sprocesses should have the same source: the process in the initial state *********)
+ − 792
fun source_proc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process option"
+ − 793
where
+ − 794
"source_proc [] p = (if (p \<in> init_processes) then Some p else None)"
+ − 795
| "source_proc (Clone p p' # s) p'' = (if (p'' = p') then source_proc s p else source_proc s p'')"
+ − 796
| "source_proc (e # s) p = source_proc s p"
+ − 797
+ − 798
fun obj2sobj :: "t_state \<Rightarrow> t_object \<Rightarrow> t_sobject"
+ − 799
where
+ − 800
"obj2sobj s (File f) = (
+ − 801
case (cf2sfile s f) of
+ − 802
Some sf \<Rightarrow> (if (f \<in> init_files \<and> (\<not> deleted (File f) s))
+ − 803
then SFile sf (Some f)
+ − 804
else SFile sf None)
+ − 805
| _ \<Rightarrow> Unknown )"
+ − 806
| "obj2sobj s (Proc p) = (
+ − 807
case (cp2sproc s p) of
+ − 808
Some sp \<Rightarrow> SProc sp (source_proc s p)
+ − 809
| _ \<Rightarrow> Unknown )"
+ − 810
| "obj2sobj s (IPC i) = (
+ − 811
case (ci2sipc s i) of
+ − 812
Some si \<Rightarrow> (if (i \<in> init_ipcs \<and> (\<not> deleted (IPC i) s))
+ − 813
then SIPC si (Some i)
+ − 814
else SIPC si None)
+ − 815
| _ \<Rightarrow> Unknown )"
+ − 816
+ − 817
fun role_of_sproc :: "t_sprocess \<Rightarrow> t_normal_role"
+ − 818
where
+ − 819
"role_of_sproc (r, fr, pt, u) = r"
+ − 820
+ − 821
fun source_of_sobj :: "t_sobject \<Rightarrow> t_object option"
+ − 822
where
+ − 823
"source_of_sobj (SFile sf tag) = (case tag of
+ − 824
Some f \<Rightarrow> Some (File f)
+ − 825
| _ \<Rightarrow> None)"
+ − 826
| "source_of_sobj (SProc sp tag) = (case tag of
+ − 827
Some p \<Rightarrow> Some (Proc p)
+ − 828
| _ \<Rightarrow> None)"
+ − 829
| "source_of_sobj (SIPC si tag) = (case tag of
+ − 830
Some i \<Rightarrow> Some (IPC i)
+ − 831
| _ \<Rightarrow> None)"
+ − 832
| "source_of_sobj Unknown = None"
+ − 833
+ − 834
definition taintable_s :: "t_object \<Rightarrow> bool"
+ − 835
where
+ − 836
"taintable_s obj \<equiv> \<exists>sobj. sobj \<in> tainted_s \<and> source_of_sobj sobj = Some obj"
+ − 837
+ − 838
(*
+ − 839
definition file_deletable_s:: "t_file \<Rightarrow> bool"
+ − 840
where
+ − 841
"file_deletable_s f \<equiv> \<forall> t sd srf. (SFile (t,sd) srf \<in> all_sobjs \<and> f \<preceq> sd \<longrightarrow> (\<exists> sp srp. SProc sp srp \<in> all_sobjs \<and> (role_of_sproc sp, File_type t, DELETE) \<in> compatible))"
+ − 842
*)
+ − 843
(*
+ − 844
definition file_deletable_s:: "t_file \<Rightarrow> bool"
+ − 845
where
+ − 846
"file_deletable_s sd \<equiv> \<forall> f. (f \<in> init_files \<and> sd \<preceq> f \<longrightarrow> (\<exists> t sp srp. SProc sp srp \<in> all_sobjs \<and> etype_of_file [] f = Some t \<and> (role_of_sproc sp, File_type t, DELETE) \<in> compatible))"*)
+ − 847
+ − 848
definition file_deletable_s:: "t_file \<Rightarrow> bool"
+ − 849
where
+ − 850
"file_deletable_s f \<equiv> \<exists> t sp srp. SProc sp srp \<in> all_sobjs \<and> etype_of_file [] f = Some t \<and> (role_of_sproc sp, File_type t, DELETE) \<in> compatible"
+ − 851
+ − 852
definition proc_deletable_s:: "t_process \<Rightarrow> bool"
+ − 853
where
+ − 854
"proc_deletable_s p \<equiv> \<exists> r fr pt u sp' srp'. SProc (r,fr,pt,u) (Some p) \<in> all_sobjs \<and> SProc sp' srp' \<in> all_sobjs \<and> (role_of_sproc sp', Proc_type pt, DELETE) \<in> compatible"
+ − 855
+ − 856
definition ipc_deletable_s:: "t_ipc \<Rightarrow> bool"
+ − 857
where
+ − 858
"ipc_deletable_s i \<equiv> \<exists> t sp srp. SProc sp srp \<in> all_sobjs \<and> type_of_ipc [] i = Some t \<and> (role_of_sproc sp, IPC_type t, DELETE) \<in> compatible"
+ − 859
+ − 860
fun deletable_s :: "t_object \<Rightarrow> bool"
+ − 861
where
+ − 862
"deletable_s (Proc p) = (p \<in> init_processes \<and> proc_deletable_s p)"
+ − 863
| "deletable_s (File f) = (f \<in> init_files \<and> file_deletable_s f)"
+ − 864
| "deletable_s (IPC i) = (i \<in> init_ipcs \<and> ipc_deletable_s i)"
+ − 865
+ − 866
definition undeletable_s:: "t_object \<Rightarrow> bool"
+ − 867
where
+ − 868
"undeletable_s obj \<equiv> exists [] obj \<and> \<not> deletable_s obj"
+ − 869
+ − 870
end
+ − 871
+ − 872
locale tainting_s_sound = tainting_s_complete +
+ − 873
+ − 874
assumes
+ − 875
clone_type_unchange: "\<And> r. default_process_create_type r = InheritParent_proc_type"
+ − 876
(* this is for statically clone do not change anything ! ! so that, there're no rule for
+ − 877
clone in all_sobjs and tainted_s *)
+ − 878
and clone_no_limit: "\<And> r t. (r, Proc_type t, CREATE) \<in> compatible"
+ − 879
+ − 880
begin
+ − 881
+ − 882
(* the all_sobjs': the soundness view of all_sobjs, just remove the clone case, cause
+ − 883
in this locale, clone doesn't change any information of such a sprocess*)
+ − 884
inductive_set all_sobjs' :: "t_sobject set"
+ − 885
where
+ − 886
af'_init: "\<lbrakk>f \<in> init_files; etype_aux init_file_type_aux f = Some t\<rbrakk> \<Longrightarrow> SFile (t, f) (Some f) \<in> all_sobjs'"
+ − 887
| af'_cfd: "\<lbrakk>SFile (t, sd) sf \<in> all_sobjs'; SProc (r, fr, pt, u) sp \<in> all_sobjs'; default_fd_create_type r = NormalFile_type t'; (r, File_type t, WRITE) \<in> compatible; (r, File_type t', CREATE) \<in> compatible\<rbrakk> \<Longrightarrow> SFile (t', sd) None \<in> all_sobjs'"
+ − 888
| af'_cfd': "\<lbrakk>SFile (t, sd) sf \<in> all_sobjs'; SProc (r, fr, pt, u) sp \<in> all_sobjs'; default_fd_create_type r = InheritParent_file_type; (r, File_type t, WRITE) \<in> compatible\<rbrakk> \<Longrightarrow> SFile (t, sd) None \<in> all_sobjs'"
+ − 889
+ − 890
| ai'_init: "init_ipc_type i = Some t \<Longrightarrow> SIPC t (Some i) \<in> all_sobjs'"
+ − 891
| ai'_cipc: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> all_sobjs'; (r, IPC_type (default_ipc_create_type r), CREATE) \<in> compatible\<rbrakk> \<Longrightarrow> SIPC (default_ipc_create_type r) None \<in> all_sobjs'"
+ − 892
+ − 893
| ap'_init: "\<lbrakk>init_currentrole p = Some r; init_proc_forcedrole p = Some fr; init_process_type p = Some t; init_owner p = Some u\<rbrakk> \<Longrightarrow> SProc (r, fr, t, u) (Some p) \<in> all_sobjs'"
+ − 894
| ap'_crole: "\<lbrakk>SProc (r, fr, t, u) sp \<in> all_sobjs'; r' \<in> comproles r\<rbrakk> \<Longrightarrow> SProc (r', fr, t, u) sp \<in> all_sobjs'"
+ − 895
| ap'_chown: "\<lbrakk>SProc (r, fr, t, u') sp \<in> all_sobjs'; u \<in> init_users; chown_role_aux r fr u = Some nr; (r, Proc_type t, CHANGE_OWNER) \<in> compatible\<rbrakk> \<Longrightarrow> SProc (nr, fr, chown_type_aux r nr t, u) sp \<in> all_sobjs'"
+ − 896
| ap'_exec: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> all_sobjs'; SFile (t, sd) sf \<in> all_sobjs'; (r, File_type t, EXECUTE) \<in> compatible; exec_role_aux r sd u = Some r'; erole_functor init_file_forcedrole InheritUpMixed sd = Some fr'\<rbrakk> \<Longrightarrow> SProc (r', fr', exec_type_aux r pt, u) sp \<in> all_sobjs'"
+ − 897
+ − 898
(* the tainted_s': the soundness view of all_sobjs, just remove the clone case, cause
+ − 899
in this locale, clone doesn't change any information of such a sprocess*)
+ − 900
inductive_set tainted_s' :: "t_sobject set"
+ − 901
where
+ − 902
ts'_init: "obj \<in> seeds \<Longrightarrow> init_obj2sobj obj \<in> tainted_s'"
+ − 903
| ts'_exec1: "\<lbrakk>SFile (t, sd) sf \<in> tainted_s'; SProc (r, fr, pt, u) sp \<in> all_sobjs'; (r, File_type t, EXECUTE) \<in> compatible; exec_role_aux r sd u = Some r'; erole_functor init_file_forcedrole InheritUpMixed sd = Some fr'\<rbrakk> \<Longrightarrow> SProc (r', fr', exec_type_aux r pt, u) sp \<in> tainted_s'"
+ − 904
| ts'_exec2: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s'; SFile (t, sd) sf \<in> all_sobjs'; (r, File_type t, EXECUTE) \<in> compatible; exec_role_aux r sd u = Some r'; erole_functor init_file_forcedrole InheritUpMixed sd = Some fr'\<rbrakk> \<Longrightarrow> SProc (r', fr', exec_type_aux r pt, u) sp \<in> tainted_s'"
+ − 905
| ts'_cfd: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s'; SFile (t, sd) sf \<in> all_sobjs'; default_fd_create_type r = NormalFile_type t'; (r, File_type t, WRITE) \<in> compatible; (r, File_type t', CREATE) \<in> compatible\<rbrakk> \<Longrightarrow> SFile (t', sd) None \<in> tainted_s'"
+ − 906
| ts'_cfd': "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s'; SFile (t, sd) sf \<in> all_sobjs'; default_fd_create_type r = InheritParent_file_type; (r, File_type t, WRITE) \<in> compatible\<rbrakk> \<Longrightarrow> SFile (t, sd) None \<in> tainted_s'"
+ − 907
| ts'_cipc: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s'; (r, IPC_type (default_ipc_create_type r), CREATE) \<in> compatible\<rbrakk> \<Longrightarrow> SIPC (default_ipc_create_type r) None \<in> tainted_s'"
+ − 908
| ts'_read: "\<lbrakk>SFile (t, sd) sf \<in> tainted_s'; SProc (r, fr, pt, u) sp \<in> all_sobjs'; (r, File_type t, READ) \<in> compatible\<rbrakk> \<Longrightarrow> SProc (r, fr, pt, u) sp \<in> tainted_s'"
+ − 909
| ts'_write: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s'; SFile (t, sd) sf \<in> all_sobjs'; (r, File_type t, WRITE) \<in> compatible\<rbrakk> \<Longrightarrow> SFile (t, sd) sf \<in> tainted_s'"
+ − 910
| ts'_recv: "\<lbrakk>SIPC t si \<in> tainted_s'; SProc (r, fr, pt, u) sp \<in> all_sobjs'; (r, IPC_type t, RECEIVE) \<in> compatible\<rbrakk> \<Longrightarrow> SProc (r, fr, pt, u) sp \<in> tainted_s'"
+ − 911
| ts'_send: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s'; SIPC t si \<in> all_sobjs'; (r, IPC_type t, SEND) \<in> compatible\<rbrakk> \<Longrightarrow> SIPC t si \<in> tainted_s'"
+ − 912
| ts'_crole: "\<lbrakk>SProc (r, fr, pt, u) sp \<in> tainted_s'; r' \<in> comproles r\<rbrakk> \<Longrightarrow> SProc (r', fr, pt, u) sp \<in> tainted_s'"
+ − 913
| ts'_chown: "\<lbrakk>SProc (r, fr, t, u') sp \<in> tainted_s'; u \<in> init_users; chown_role_aux r fr u = Some nr; (r, Proc_type t, CHANGE_OWNER) \<in> compatible\<rbrakk> \<Longrightarrow> SProc (nr, fr, chown_type_aux r nr t, u) sp \<in> tainted_s'"
+ − 914
+ − 915
fun sobj_source_eq_obj :: "t_sobject \<Rightarrow> t_object \<Rightarrow> bool"
+ − 916
where
+ − 917
"sobj_source_eq_obj (SFile sf None) (File f) = True"
+ − 918
| "sobj_source_eq_obj (SFile sf (Some f')) (File f) = (f' = f)"
+ − 919
| "sobj_source_eq_obj (SProc sp None) (Proc p) = True"
+ − 920
| "sobj_source_eq_obj (SProc sp (Some p')) (Proc p) = (p' = p)"
+ − 921
| "sobj_source_eq_obj (SIPC si None) (IPC i) = True"
+ − 922
| "sobj_source_eq_obj (SIPC si (Some i')) (IPC i) = (i' = i)"
+ − 923
| "sobj_source_eq_obj _ _ = False"
+ − 924
+ − 925
fun not_both_sproc:: "t_sobject \<Rightarrow> t_sobject \<Rightarrow> bool"
+ − 926
where
+ − 927
"not_both_sproc (SProc sp srp) (SProc sp' srp') = False"
+ − 928
| "not_both_sproc _ _ = True"
+ − 929
+ − 930
(*** definitions for init processes statical informations reservation ***)
+ − 931
+ − 932
definition initp_intact :: "t_state => bool"
+ − 933
where
+ − 934
"initp_intact s \<equiv> \<forall> p. p \<in> init_processes --> p \<in> current_procs s \<and> obj2sobj s (Proc p) = init_obj2sobj (Proc p)"
+ − 935
+ − 936
definition initp_alter :: "t_state \<Rightarrow> t_process \<Rightarrow> bool"
+ − 937
where
+ − 938
"initp_alter s p \<equiv> \<exists> p'. p' \<in> current_procs s \<and> obj2sobj s (Proc p') = init_obj2sobj (Proc p)"
+ − 939
+ − 940
definition initp_intact_butp :: "t_state \<Rightarrow> t_process \<Rightarrow> bool"
+ − 941
where
+ − 942
"initp_intact_butp s proc \<equiv> (\<forall> p. p \<in> init_processes \<and> p \<noteq> proc \<longrightarrow> p \<in> current_procs s \<and> obj2sobj s (Proc p) = init_obj2sobj (Proc p)) \<and> initp_alter s proc"
+ − 943
+ − 944
fun initp_intact_but :: "t_state \<Rightarrow> t_sobject \<Rightarrow> bool"
+ − 945
where
+ − 946
"initp_intact_but s (SProc sp (Some p)) = initp_intact_butp s p"
+ − 947
| "initp_intact_but s _ = initp_intact s"
+ − 948
6
+ − 949
(*** how to generating new valid pathname for examples of new_proc, new_ipc and new_file as CreateFile ***)
+ − 950
+ − 951
definition next_nat :: "nat set \<Rightarrow> nat"
+ − 952
where
+ − 953
"next_nat ps = (Max ps) + 1"
+ − 954
+ − 955
definition new_proc :: "t_state \<Rightarrow> t_process"
+ − 956
where
+ − 957
"new_proc \<tau> = next_nat (current_procs \<tau>)"
+ − 958
+ − 959
definition new_ipc :: "t_state \<Rightarrow> t_ipc"
+ − 960
where
+ − 961
"new_ipc \<tau> = next_nat (current_ipcs \<tau>)"
1
+ − 962
+ − 963
definition all_fname_under_dir:: "t_file \<Rightarrow> t_state \<Rightarrow> t_fname set"
+ − 964
where
+ − 965
"all_fname_under_dir d \<tau> = {fn. \<exists> f. fn # d = f \<and> f \<in> current_files \<tau>}"
+ − 966
+ − 967
fun fname_all_a:: "nat \<Rightarrow> t_fname"
+ − 968
where
+ − 969
"fname_all_a 0 = []" |
+ − 970
"fname_all_a (Suc n) = ''a''@(fname_all_a n)"
+ − 971
+ − 972
definition fname_length_set :: "t_fname set \<Rightarrow> nat set"
+ − 973
where
+ − 974
"fname_length_set fns = length`fns"
+ − 975
+ − 976
definition next_fname:: "t_file \<Rightarrow> t_state \<Rightarrow> t_fname"
+ − 977
where
+ − 978
"next_fname pf \<tau> = fname_all_a ((Max (fname_length_set (all_fname_under_dir pf \<tau>))) + 1)"
+ − 979
+ − 980
definition new_childf:: "t_file \<Rightarrow> t_state \<Rightarrow> t_file"
+ − 981
where
+ − 982
"new_childf pf \<tau> = next_fname pf \<tau> # pf"
+ − 983
+ − 984
end
+ − 985
+ − 986
end
+ − 987