1
+ − 1
theory os_rc
+ − 2
imports Main rc_theory
+ − 3
begin
+ − 4
+ − 5
(****** below context is for lemmas of OS and RC ******)
+ − 6
context rc_basic begin
+ − 7
+ − 8
inductive_cases vs_step': "valid (e # \<tau>)"
+ − 9
+ − 10
lemma valid_cons:
+ − 11
"valid (e # \<tau>) \<Longrightarrow> valid \<tau>"
+ − 12
by (drule vs_step', auto)
+ − 13
+ − 14
lemma valid_os:
+ − 15
"valid (e # \<tau>) \<Longrightarrow> os_grant \<tau> e"
+ − 16
by (drule vs_step', auto)
+ − 17
+ − 18
lemma valid_rc:
+ − 19
"valid (e # \<tau>) \<Longrightarrow> rc_grant \<tau> e"
+ − 20
by (drule vs_step', auto)
+ − 21
+ − 22
lemma vs_history:
+ − 23
"\<lbrakk>s \<preceq> s'; valid s'\<rbrakk> \<Longrightarrow> valid s"
+ − 24
apply (induct s', simp add:no_junior_def)
+ − 25
apply (case_tac "s = a # s'", simp)
+ − 26
apply (drule no_junior_noteq, simp)
+ − 27
by (drule valid_cons)
+ − 28
+ − 29
lemma parent_file_in_current:
+ − 30
"\<lbrakk>parent f = Some pf; f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> pf \<in> current_files s"
+ − 31
apply (induct s)
+ − 32
apply (simp add:parent_file_in_init)
+ − 33
apply (frule valid_cons, frule valid_rc, frule valid_os)
+ − 34
apply (case_tac a, auto split:option.splits)
+ − 35
apply (case_tac f, simp+)
+ − 36
done
+ − 37
+ − 38
lemma parent_file_in_current':
+ − 39
"\<lbrakk>fn # pf \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> pf \<in> current_files s"
+ − 40
by (auto intro!:parent_file_in_current[where pf = pf])
+ − 41
+ − 42
lemma parent_file_in_init':
+ − 43
"fn # pf \<in> init_files \<Longrightarrow> pf \<in> init_files"
+ − 44
by (auto intro!:parent_file_in_init[where pf = pf])
+ − 45
+ − 46
lemma ancient_file_in_current:
+ − 47
"\<lbrakk>f \<in> current_files s; valid s; af \<preceq> f\<rbrakk> \<Longrightarrow> af \<in> current_files s"
+ − 48
apply (induct f)
+ − 49
apply (simp add:no_junior_def)
+ − 50
apply (case_tac "af = a # f", simp)
+ − 51
apply (drule no_junior_noteq, simp)
+ − 52
apply (drule parent_file_in_current', simp+)
+ − 53
done
+ − 54
+ − 55
lemma cannot_del_root:
+ − 56
"\<lbrakk>valid (DeleteFile p [] # s); f \<noteq> []; f \<in> current_files s\<rbrakk> \<Longrightarrow> False"
+ − 57
apply (frule valid_cons, frule valid_os)
+ − 58
apply (case_tac f rule:rev_cases, simp)
+ − 59
apply (drule_tac af = "[y]" in ancient_file_in_current, simp+)
+ − 60
done
+ − 61
+ − 62
lemma init_file_initialrole_imp_some: "\<exists> r. init_file_initialrole f = Some r"
+ − 63
by (case_tac f, auto split:option.splits)
+ − 64
+ − 65
lemma file_has_initialrole: "\<lbrakk>f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> (\<exists> r. initialrole s f = Some r)"
+ − 66
apply (induct s arbitrary:f)
+ − 67
apply (simp, rule init_file_initialrole_imp_some)
+ − 68
apply (frule valid_cons, frule valid_os, case_tac a)
+ − 69
apply (auto split:if_splits option.splits)
+ − 70
done
+ − 71
+ − 72
lemma file_has_initialrole':
+ − 73
"\<lbrakk>initialrole s f = None; valid s\<rbrakk> \<Longrightarrow> f \<notin> current_files s"
+ − 74
by (rule notI, auto dest:file_has_initialrole)
+ − 75
+ − 76
lemma file_has_effinitialrole:
+ − 77
"\<lbrakk>f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> \<exists> r. effinitialrole s f = Some r"
+ − 78
apply (induct f)
+ − 79
apply (auto simp:effinitialrole_def dest:file_has_initialrole parent_file_in_current')
+ − 80
done
+ − 81
+ − 82
lemma file_has_effinitialrole':
+ − 83
"\<lbrakk>effinitialrole s f = None; valid s\<rbrakk> \<Longrightarrow> f \<notin> current_files s"
+ − 84
by (rule notI, auto dest:file_has_effinitialrole)
+ − 85
+ − 86
lemma init_file_forcedrole_imp_some: "\<exists> r. init_file_forcedrole f = Some r"
+ − 87
by (case_tac f, auto split:option.splits)
+ − 88
+ − 89
lemma file_has_forcedrole: "\<lbrakk>f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> (\<exists> r. forcedrole s f = Some r)"
+ − 90
apply (induct s arbitrary:f)
+ − 91
apply (simp add:init_file_forcedrole_imp_some)
+ − 92
apply (frule valid_cons, frule valid_os, case_tac a, auto)
+ − 93
done
+ − 94
+ − 95
lemma file_has_forcedrole':
+ − 96
"\<lbrakk>forcedrole s f = None; valid s\<rbrakk> \<Longrightarrow> f \<notin> current_files s"
+ − 97
by (rule notI, auto dest:file_has_forcedrole)
+ − 98
+ − 99
lemma file_has_effforcedrole:
+ − 100
"\<lbrakk>f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> \<exists> r. effforcedrole s f = Some r"
+ − 101
apply (induct f)
+ − 102
apply (auto simp:effforcedrole_def dest:file_has_forcedrole parent_file_in_current')
+ − 103
done
+ − 104
+ − 105
lemma file_has_effforcedrole':
+ − 106
"\<lbrakk>effforcedrole s f = None; valid s\<rbrakk> \<Longrightarrow> f \<notin> current_files s"
+ − 107
by (rule notI, auto dest:file_has_effforcedrole)
+ − 108
+ − 109
lemma current_proc_has_forcedrole:
+ − 110
"\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> r. proc_forcedrole s p = Some r"
+ − 111
apply (induct s arbitrary:p) using init_proc_has_frole
+ − 112
apply (simp add:bidirect_in_init_def)
+ − 113
apply (frule valid_cons, frule valid_os, case_tac a)
+ − 114
apply (auto split:if_splits option.splits intro:file_has_effforcedrole)
+ − 115
done
+ − 116
+ − 117
lemma current_proc_has_forcedrole':
+ − 118
"\<lbrakk>proc_forcedrole s p = None; valid s\<rbrakk> \<Longrightarrow> p \<notin> current_procs s"
+ − 119
by (rule notI, auto dest:current_proc_has_forcedrole)
+ − 120
+ − 121
lemma current_proc_has_owner: "\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> u. owner s p = Some u"
+ − 122
apply (induct s arbitrary:p) using init_proc_has_owner
+ − 123
apply (simp add:bidirect_in_init_def)
+ − 124
apply (frule valid_cons, frule valid_os, case_tac a, auto)
+ − 125
done
+ − 126
+ − 127
lemma current_proc_has_owner':
+ − 128
"\<lbrakk>owner s p = None; valid s\<rbrakk> \<Longrightarrow> p \<notin> current_procs s"
+ − 129
by (rule notI, auto dest:current_proc_has_owner)
+ − 130
+ − 131
(*
+ − 132
lemma effinitial_normal_intro:
+ − 133
"\<lbrakk>f \<in> current_files \<tau>; valid \<tau>; effinitialrole \<tau> f \<noteq> Some UseForcedRole\<rbrakk> \<Longrightarrow> \<exists>nr. effinitialrole \<tau> f = Some (NormalRole nr)"
+ − 134
apply (drule file_has_effinitialrole, simp)
+ − 135
apply (erule exE, frule effinitialrole_valid, simp)
+ − 136
done
+ − 137
+ − 138
lemma effforced_normal_intro:
+ − 139
"\<lbrakk>f \<in> current_files \<tau>; valid \<tau>; effforcedrole \<tau> f \<noteq> Some InheritUserRole; effforcedrole \<tau> f \<noteq> Some InheritProcessRole; effforcedrole \<tau> f \<noteq> Some InheritUpMixed\<rbrakk>
+ − 140
\<Longrightarrow> \<exists>nr. effforcedrole \<tau> f = Some (NormalRole nr)"
+ − 141
apply (drule file_has_effforcedrole, simp)
+ − 142
apply (erule exE, frule effforcedrole_valid, simp)
+ − 143
done
+ − 144
*)
+ − 145
+ − 146
lemma owner_in_users: "\<lbrakk>owner s p = Some u; valid s\<rbrakk> \<Longrightarrow> u \<in> init_users"
+ − 147
apply (induct s arbitrary:p) defer
+ − 148
apply (frule valid_cons, frule valid_os, case_tac a)
+ − 149
apply (auto split:if_splits option.splits intro!:init_owner_valid)
+ − 150
done
+ − 151
+ − 152
lemma user_has_normalrole:
+ − 153
"u \<in> init_users \<Longrightarrow> \<exists> nr. defrole u = Some nr" using init_user_has_role
+ − 154
by (auto simp:bidirect_in_init_def)
+ − 155
+ − 156
lemma user_has_normalrole':
+ − 157
"defrole u = None \<Longrightarrow> u \<notin> init_users"
+ − 158
by (rule notI, auto dest:user_has_normalrole)
+ − 159
+ − 160
lemma current_proc_has_role:
+ − 161
"\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> nr. currentrole s p = Some nr"
+ − 162
apply (induct s arbitrary:p) using init_proc_has_role
+ − 163
apply (simp add:bidirect_in_init_def)
+ − 164
apply (frule valid_cons, frule valid_os, case_tac a)
+ − 165
apply (auto simp:map_comp_def split:if_splits option.splits t_role.splits
+ − 166
dest!:current_proc_has_owner' user_has_normalrole' current_proc_has_forcedrole'
+ − 167
file_has_forcedrole' file_has_effforcedrole'
+ − 168
file_has_initialrole' file_has_effinitialrole'
+ − 169
intro:user_has_normalrole
+ − 170
dest:owner_in_users effinitialrole_valid effforcedrole_valid proc_forcedrole_valid)
+ − 171
done
+ − 172
+ − 173
lemma current_file_has_type:
+ − 174
"\<lbrakk>f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> \<exists> t. type_of_file s f = Some t"
+ − 175
apply (induct s)
+ − 176
apply (simp split:option.splits)
+ − 177
apply (frule valid_cons, frule valid_os, case_tac a)
+ − 178
apply (auto split:option.splits intro:current_proc_has_role)
+ − 179
done
+ − 180
+ − 181
lemma init_file_has_etype: "f \<in> init_files \<Longrightarrow> \<exists> nt. etype_aux init_file_type_aux f = Some nt"
+ − 182
apply (induct f) defer
+ − 183
apply (frule parent_file_in_init')
+ − 184
apply (auto split:option.splits t_rc_file_type.splits)
+ − 185
done
+ − 186
+ − 187
lemma current_file_has_etype[rule_format]:
+ − 188
"f \<in> current_files s \<Longrightarrow> valid s \<longrightarrow> (\<exists> nt. etype_of_file s f = Some nt)"
+ − 189
apply (induct f)
+ − 190
apply (auto simp:etype_of_file_def dest:current_file_has_type parent_file_in_current'
+ − 191
split:option.splits t_rc_file_type.splits)
+ − 192
done
+ − 193
+ − 194
lemma current_file_has_etype':
+ − 195
"\<lbrakk>etype_of_file s f = None; valid s\<rbrakk> \<Longrightarrow> f \<notin> current_files s"
+ − 196
by (rule notI, auto dest:current_file_has_etype)
+ − 197
+ − 198
(*** etype_of_file simpset ***)
+ − 199
+ − 200
lemma etype_aux_prop:
+ − 201
"\<forall> x. x \<preceq> f \<longrightarrow> func' x = func x \<Longrightarrow> etype_aux func f = etype_aux func' f"
+ − 202
apply (induct f)
+ − 203
by (auto split:t_rc_file_type.splits option.splits)
+ − 204
+ − 205
lemma etype_aux_prop1:
+ − 206
"func' = func ((a#f) := b) \<Longrightarrow> etype_aux func f = etype_aux func' f"
+ − 207
by (rule etype_aux_prop, auto simp:no_junior_def)
+ − 208
+ − 209
lemma etype_aux_prop1':
+ − 210
"etype_aux func f = x \<Longrightarrow> etype_aux (func ((a#f) := b)) f = x"
+ − 211
apply (subgoal_tac "etype_aux func f = etype_aux (func ((a#f) := b)) f")
+ − 212
apply (simp, rule etype_aux_prop1, simp)
+ − 213
done
+ − 214
+ − 215
lemma etype_aux_prop2:
+ − 216
"\<lbrakk>f \<in> current_files s; f' \<notin> current_files s; valid s\<rbrakk> \<Longrightarrow>
+ − 217
etype_aux (func (f' := b)) f = etype_aux func f"
+ − 218
apply (rule etype_aux_prop)
+ − 219
by (auto dest:ancient_file_in_current)
+ − 220
+ − 221
lemma etype_aux_prop3:
+ − 222
"parent f = Some pf
+ − 223
\<Longrightarrow> etype_aux (func (f := Some InheritParent_file_type)) f = etype_aux func pf"
+ − 224
apply (case_tac f, simp+)
+ − 225
by (rule etype_aux_prop, simp add:no_junior_def)
+ − 226
+ − 227
lemma etype_aux_prop4:
+ − 228
"etype_aux (func (f := Some (NormalFile_type t))) f = Some t"
+ − 229
by (case_tac f, auto)
+ − 230
+ − 231
lemma etype_of_file_delete:
+ − 232
"\<lbrakk>valid (DeleteFile p f # s); f' \<in> current_files s\<rbrakk>
+ − 233
\<Longrightarrow> etype_of_file (DeleteFile p f # s) f' = etype_of_file s f'"
+ − 234
apply (frule valid_cons, frule valid_os)
+ − 235
apply (simp add:etype_of_file_def)
+ − 236
done
+ − 237
+ − 238
lemma current_proc_has_type:
+ − 239
"\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> nt. type_of_process s p = Some nt"
+ − 240
apply (induct s arbitrary:p) using init_proc_has_type
+ − 241
apply (simp add:bidirect_in_init_def)
+ − 242
+ − 243
apply (frule valid_cons, frule valid_os, case_tac a)
+ − 244
+ − 245
apply (subgoal_tac "nat1 \<in> current_procs (a # s)") prefer 2 apply simp
+ − 246
apply (drule_tac p = nat1 in current_proc_has_role, simp, erule exE)
+ − 247
+ − 248
apply (auto simp:pct_def pot_def pet_def dest:current_proc_has_role
+ − 249
split:option.splits t_rc_proc_type.splits
+ − 250
dest!:default_process_create_type_valid default_process_chown_type_valid
+ − 251
default_process_execute_type_valid)
+ − 252
done
+ − 253
+ − 254
lemma current_ipc_has_type:
+ − 255
"\<lbrakk>i \<in> current_ipcs s; valid s\<rbrakk> \<Longrightarrow> \<exists> nt. type_of_ipc s i = Some nt"
+ − 256
apply (induct s) using init_ipc_has_type
+ − 257
apply (simp add:bidirect_in_init_def)
+ − 258
+ − 259
apply (frule valid_cons, frule valid_os, case_tac a)
+ − 260
apply (auto dest:current_proc_has_role)
+ − 261
done
+ − 262
+ − 263
(*** finite current_* ***)
+ − 264
+ − 265
lemma finite_cf: "finite (current_files s)"
+ − 266
apply (induct s) defer apply (case_tac a)
+ − 267
using init_finite by auto
+ − 268
+ − 269
lemma finite_cp: "finite (current_procs s)"
+ − 270
apply (induct s) defer apply (case_tac a)
+ − 271
using init_finite by auto
+ − 272
+ − 273
lemma finite_ci: "finite (current_ipcs s)"
+ − 274
apply (induct s) defer apply (case_tac a)
+ − 275
using init_finite by auto
+ − 276
6
+ − 277
end
+ − 278
+ − 279
context tainting_s_complete begin
+ − 280
+ − 281
lemma init_notin_curf_deleted:
+ − 282
"\<lbrakk>f \<notin> current_files s; f \<in> init_files\<rbrakk> \<Longrightarrow> deleted (File f) s"
+ − 283
by (induct s, simp, case_tac a, auto)
+ − 284
+ − 285
lemma init_notin_curi_deleted:
+ − 286
"\<lbrakk>i \<notin> current_ipcs s; i \<in> init_ipcs\<rbrakk> \<Longrightarrow> deleted (IPC i) s"
+ − 287
by (induct s, simp, case_tac a, auto)
+ − 288
+ − 289
lemma init_notin_curp_deleted:
+ − 290
"\<lbrakk>p \<notin> current_procs s; p \<in> init_processes\<rbrakk> \<Longrightarrow> deleted (Proc p) s"
+ − 291
by (induct s, simp, case_tac a, auto)
+ − 292
+ − 293
lemma source_dir_in_init: "source_dir s f = Some sd \<Longrightarrow> sd \<in> init_files"
+ − 294
by (induct f, auto split:if_splits)
+ − 295
+ − 296
lemma source_proc_in_init:
+ − 297
"\<lbrakk>source_proc s p = Some p'; p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> p' \<in> init_processes"
+ − 298
apply (induct s arbitrary:p, simp split:if_splits)
+ − 299
apply (frule valid_os, frule valid_cons, case_tac a)
+ − 300
by (auto split:if_splits)
+ − 301
+ − 302
end
+ − 303
+ − 304
context tainting_s_sound begin
+ − 305
1
+ − 306
(*** properties of new-proc new-ipc ... ***)
+ − 307
+ − 308
lemma nn_notin_aux: "finite s \<Longrightarrow> \<forall> a \<in> s. Max s \<ge> a "
+ − 309
apply (erule finite.induct, simp)
+ − 310
apply (rule ballI)
+ − 311
apply (case_tac "aa = a", simp+)
+ − 312
done
+ − 313
+ − 314
lemma nn_notin: "finite s \<Longrightarrow> next_nat s \<notin> s"
+ − 315
apply (drule nn_notin_aux)
+ − 316
apply (simp add:next_nat_def)
+ − 317
by (auto)
+ − 318
+ − 319
lemma np_notin_curp: "new_proc \<tau> \<notin> current_procs \<tau>" using finite_cp
+ − 320
by (simp add:new_proc_def nn_notin)
+ − 321
+ − 322
lemma np_notin_curp': "new_proc \<tau> \<in> current_procs \<tau> \<Longrightarrow> False"
+ − 323
by (simp add:np_notin_curp)
+ − 324
+ − 325
lemma ni_notin_curi: "new_ipc \<tau> \<notin> current_ipcs \<tau>" using finite_ci
+ − 326
by (simp add:new_ipc_def nn_notin)
+ − 327
+ − 328
lemma ni_notin_curi': "new_ipc \<tau> \<in> current_ipcs \<tau> \<Longrightarrow> False"
+ − 329
by (simp add:ni_notin_curi)
+ − 330
+ − 331
lemma ni_init_deled: "new_ipc s \<in> init_ipcs \<Longrightarrow> deleted (IPC (new_ipc s)) s"
+ − 332
using ni_notin_curi[where \<tau> = s]
+ − 333
by (drule_tac init_notin_curi_deleted, simp+)
+ − 334
+ − 335
lemma np_init_deled: "new_proc s \<in> init_processes \<Longrightarrow> deleted (Proc (new_proc s)) s"
+ − 336
using np_notin_curp[where \<tau> = s]
+ − 337
by (drule_tac init_notin_curp_deleted, simp+)
+ − 338
+ − 339
+ − 340
lemma len_fname_all: "length (fname_all_a len) = len"
+ − 341
by (induct len, auto simp:fname_all_a.simps)
+ − 342
+ − 343
lemma ncf_notin_curf: "new_childf f s \<notin> current_files s"
+ − 344
apply (simp add:new_childf_def next_fname_def all_fname_under_dir_def)
+ − 345
apply (rule notI)
+ − 346
apply (subgoal_tac "(CHR ''a'' # fname_all_a (Max (fname_length_set {fn. fn # f \<in> current_files s}))) \<in> {fn. fn # f \<in> current_files s}")
+ − 347
defer apply simp
+ − 348
apply (subgoal_tac "length (CHR ''a'' # fname_all_a (Max (fname_length_set {fn. fn # f \<in> current_files s}))) \<in> fname_length_set {fn. fn # f \<in> current_files s}")
+ − 349
defer apply (auto simp:fname_length_set_def image_def)[1]
+ − 350
apply (subgoal_tac "finite (fname_length_set {fn. fn # f \<in> current_files s})")
+ − 351
defer
+ − 352
apply (simp add:fname_length_set_def)
+ − 353
apply (rule finite_imageI) using finite_cf[where s = s]
+ − 354
apply (drule_tac h = "\<lambda> f'. case f' of [] \<Rightarrow> '''' | fn # pf' \<Rightarrow> if (pf' = f) then fn else ''''" in finite_imageI)
+ − 355
apply (rule_tac B = "(list_case [] (\<lambda>fn pf'. if pf' = f then fn else []) ` current_files s)" in finite_subset)
+ − 356
unfolding image_def
+ − 357
apply(auto)[1]
+ − 358
apply (rule_tac x = "x # f" in bexI, simp+)
+ − 359
apply (drule_tac s = "(fname_length_set {fn. fn # f \<in> current_files s})" in nn_notin_aux)
+ − 360
apply (erule_tac x = "length (CHR ''a'' # fname_all_a (Max (fname_length_set {fn. fn # f \<in> current_files s})))" in ballE)
+ − 361
apply (simp add:len_fname_all, simp)
+ − 362
done
+ − 363
+ − 364
lemma ncf_parent: "parent (new_childf f \<tau>) = Some f"
+ − 365
by (simp add:new_childf_def)
+ − 366
+ − 367
lemma clone_event_no_limit:
+ − 368
"\<lbrakk>p \<in> current_procs \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> valid (Clone p (new_proc \<tau>) # \<tau>)"
+ − 369
apply (rule vs_step)
6
+ − 370
apply (auto intro:clone_no_limit split:option.splits dest!:np_notin_curp'
1
+ − 371
dest:current_proc_has_role current_proc_has_type)
+ − 372
done
+ − 373
+ − 374
+ − 375
end
+ − 376
+ − 377
end