30
+ − 1
theory Info_flow_shm_prop
+ − 2
imports Main Flask_type Flask My_list_prefix Init_prop Valid_prop Delete_prop Current_prop
+ − 3
begin
+ − 4
+ − 5
context flask begin
+ − 6
+ − 7
(*********** simpset for one_flow_shm **************)
+ − 8
+ − 9
lemma one_flow_not_self:
+ − 10
"one_flow_shm s h p p \<Longrightarrow> False"
+ − 11
by (simp add:one_flow_shm_def)
+ − 12
+ − 13
lemma one_flow_shm_attach:
+ − 14
"valid (Attach p h flag # s) \<Longrightarrow> one_flow_shm (Attach p h flag # s) = (\<lambda> h' pa pb.
+ − 15
if (h' = h)
+ − 16
then (pa = p \<and> pb \<noteq> p \<and> flag = SHM_RDWR \<and> (\<exists> flagb. (pb, flagb) \<in> procs_of_shm s h)) \<or>
+ − 17
(pb = p \<and> pa \<noteq> p \<and> (pa, SHM_RDWR) \<in> procs_of_shm s h) \<or>
+ − 18
(one_flow_shm s h pa pb)
+ − 19
else one_flow_shm s h' pa pb )"
+ − 20
apply (rule ext, rule ext, rule ext, frule vd_cons, frule vt_grant_os)
+ − 21
by (auto simp add: one_flow_shm_def)
+ − 22
+ − 23
lemma one_flow_shm_detach:
+ − 24
"valid (Detach p h # s) \<Longrightarrow> one_flow_shm (Detach p h # s) = (\<lambda> h' pa pb.
+ − 25
if (h' = h)
+ − 26
then (pa \<noteq> p \<and> pb \<noteq> p \<and> one_flow_shm s h' pa pb)
+ − 27
else one_flow_shm s h' pa pb)"
+ − 28
apply (rule ext, rule ext, rule ext, frule vt_grant_os)
+ − 29
by (auto simp:one_flow_shm_def)
+ − 30
+ − 31
lemma one_flow_shm_deleteshm:
+ − 32
"valid (DeleteShM p h # s) \<Longrightarrow> one_flow_shm (DeleteShM p h # s) = (\<lambda> h' pa pb.
+ − 33
if (h' = h)
+ − 34
then False
+ − 35
else one_flow_shm s h' pa pb)"
+ − 36
apply (rule ext, rule ext, rule ext, frule vt_grant_os)
+ − 37
by (auto simp: one_flow_shm_def)
+ − 38
+ − 39
lemma one_flow_shm_clone:
+ − 40
"valid (Clone p p' fds shms # s) \<Longrightarrow> one_flow_shm (Clone p p' fds shms # s) = (\<lambda> h pa pb.
+ − 41
if (pa = p' \<and> pb \<noteq> p' \<and> h \<in> shms)
+ − 42
then (if (pb = p) then (flag_of_proc_shm s p h = Some SHM_RDWR) else one_flow_shm s h p pb)
+ − 43
else if (pb = p' \<and> pa \<noteq> p' \<and> h \<in> shms)
+ − 44
then (if (pa = p) then (flag_of_proc_shm s p h = Some SHM_RDWR) else one_flow_shm s h pa p)
+ − 45
else one_flow_shm s h pa pb)"
+ − 46
apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons, clarsimp)
+ − 47
apply (frule_tac p = p' in procs_of_shm_prop2', simp)
+ − 48
apply (auto simp:one_flow_shm_def intro:procs_of_shm_prop4 flag_of_proc_shm_prop1)
+ − 49
done
+ − 50
+ − 51
lemma one_flow_shm_execve:
+ − 52
"valid (Execve p f fds # s) \<Longrightarrow> one_flow_shm (Execve p f fds # s) = (\<lambda> h pa pb.
+ − 53
pa \<noteq> p \<and> pb \<noteq> p \<and> one_flow_shm s h pa pb )"
+ − 54
apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons)
+ − 55
by (auto simp:one_flow_shm_def)
+ − 56
+ − 57
lemma one_flow_shm_kill:
+ − 58
"valid (Kill p p' # s) \<Longrightarrow> one_flow_shm (Kill p p' # s) = (\<lambda> h pa pb.
+ − 59
pa \<noteq> p' \<and> pb \<noteq> p' \<and> one_flow_shm s h pa pb )"
+ − 60
apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons)
+ − 61
by (auto simp:one_flow_shm_def)
+ − 62
+ − 63
lemma one_flow_shm_exit:
+ − 64
"valid (Exit p # s) \<Longrightarrow> one_flow_shm (Exit p # s) = (\<lambda> h pa pb.
+ − 65
pa \<noteq> p \<and> pb \<noteq> p \<and> one_flow_shm s h pa pb )"
+ − 66
apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons)
+ − 67
by (auto simp:one_flow_shm_def)
+ − 68
+ − 69
lemma one_flow_shm_other:
+ − 70
"\<lbrakk>valid (e # s);
+ − 71
\<forall> p h flag. e \<noteq> Attach p h flag;
+ − 72
\<forall> p h. e \<noteq> Detach p h;
+ − 73
\<forall> p h. e \<noteq> DeleteShM p h;
+ − 74
\<forall> p p' fds shms. e \<noteq> Clone p p' fds shms;
+ − 75
\<forall> p f fds. e \<noteq> Execve p f fds;
+ − 76
\<forall> p p'. e \<noteq> Kill p p';
+ − 77
\<forall> p. e \<noteq> Exit p
+ − 78
\<rbrakk> \<Longrightarrow> one_flow_shm (e # s) = one_flow_shm s"
+ − 79
apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons)
+ − 80
apply (case_tac e, auto simp:one_flow_shm_def dest:procs_of_shm_prop2)
+ − 81
apply (drule procs_of_shm_prop1, auto)
+ − 82
done
+ − 83
+ − 84
lemmas one_flow_shm_simps = one_flow_shm_other one_flow_shm_attach one_flow_shm_detach one_flow_shm_deleteshm
+ − 85
one_flow_shm_clone one_flow_shm_execve one_flow_shm_kill one_flow_shm_exit
+ − 86
+ − 87
type_synonym t_edge_shm = "t_process \<times> t_shm \<times> t_process"
+ − 88
fun Fst:: "t_edge_shm \<Rightarrow> t_process" where "Fst (a, b, c) = a"
+ − 89
fun Snd:: "t_edge_shm \<Rightarrow> t_shm" where "Snd (a, b, c) = b"
+ − 90
fun Trd:: "t_edge_shm \<Rightarrow> t_process" where "Trd (a, b, c) = c"
+ − 91
+ − 92
fun edge_related:: "t_edge_shm list \<Rightarrow> t_process \<Rightarrow> t_shm \<Rightarrow> bool"
+ − 93
where
+ − 94
"edge_related [] p h = False"
+ − 95
| "edge_related ((from, shm, to) # path) p h =
+ − 96
(if (((p = from) \<or> (p = to)) \<and> (h = shm)) then True
+ − 97
else edge_related path p h)"
+ − 98
+ − 99
inductive path_by_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_edge_shm list \<Rightarrow> t_process \<Rightarrow> bool"
+ − 100
where
+ − 101
pbs1: "p \<in> current_procs s \<Longrightarrow> path_by_shm s p [] p"
+ − 102
| pbs2: "\<lbrakk>path_by_shm s p path p'; one_flow_shm s h p' p''; p'' \<notin> set (map Fst path)\<rbrakk>
+ − 103
\<Longrightarrow> path_by_shm s p ((p', h, p'')# path) p''"
+ − 104
+ − 105
+ − 106
lemma one_step_path: "\<lbrakk>one_flow_shm s h p p'; valid s\<rbrakk> \<Longrightarrow> path_by_shm s p [(p, h, p')] p'"
+ − 107
apply (rule_tac path = "[]" and p = p in path_by_shm.intros(2))
+ − 108
apply (rule path_by_shm.intros(1))
+ − 109
apply (auto intro:procs_of_shm_prop2 simp:one_flow_shm_def)
+ − 110
done
+ − 111
+ − 112
lemma pbs_prop1:
+ − 113
"path_by_shm s p path p' \<Longrightarrow> ((path = []) = (p = p')) \<and> (path \<noteq> [] \<longrightarrow> p \<in> set (map Fst path))"
+ − 114
apply (erule path_by_shm.induct, simp)
+ − 115
apply (auto simp:one_flow_shm_def)
+ − 116
done
+ − 117
+ − 118
lemma pbs_prop2:
+ − 119
"path_by_shm s p path p' \<Longrightarrow> (path = []) = (p = p')"
+ − 120
by (simp add:pbs_prop1)
+ − 121
+ − 122
lemma pbs_prop2':
+ − 123
"path_by_shm s p path p \<Longrightarrow> path = []"
+ − 124
by (simp add:pbs_prop2)
+ − 125
+ − 126
lemma pbs_prop3:
+ − 127
"\<lbrakk>path_by_shm s p path p'; path \<noteq> []\<rbrakk> \<Longrightarrow> p \<in> set (map Fst path)"
+ − 128
by (drule pbs_prop1, auto)
+ − 129
+ − 130
lemma pbs_prop4[rule_format]:
+ − 131
"path_by_shm s p path p'\<Longrightarrow> path \<noteq> [] \<longrightarrow> p' \<in> set (map Trd path)"
+ − 132
by (erule path_by_shm.induct, auto)
+ − 133
+ − 134
lemma pbs_prop5[rule_format]:
+ − 135
"path_by_shm s p path p' \<Longrightarrow> path \<noteq> [] \<longrightarrow> p' \<notin> set (map Fst path)"
+ − 136
by (erule path_by_shm.induct, auto simp:one_flow_shm_def)
+ − 137
+ − 138
lemma pbs_prop6_aux:
+ − 139
"path_by_shm s pa pathac pc \<Longrightarrow> valid s \<longrightarrow> (\<forall> pb \<in> set (map Fst pathac). \<exists> pathab pathbc. path_by_shm s pa pathab pb \<and> path_by_shm s pb pathbc pc \<and> pathac = pathbc @ pathab)"
+ − 140
apply (erule path_by_shm.induct)
+ − 141
apply simp
+ − 142
apply clarify
+ − 143
apply (case_tac "pb = p'", simp)
+ − 144
apply (rule_tac x = path in exI, simp)
+ − 145
apply (erule one_step_path, simp)
+ − 146
apply (erule_tac x = pb in ballE, simp_all, clarsimp)
+ − 147
apply (rule_tac x = pathab in exI, simp)
+ − 148
apply (erule pbs2, auto)
+ − 149
done
+ − 150
+ − 151
lemma pbs_prop6:
+ − 152
"\<lbrakk>path_by_shm s pa pathac pc; pb \<in> set (map Fst pathac); valid s\<rbrakk>
+ − 153
\<Longrightarrow> \<exists> pathab pathbc. path_by_shm s pa pathab pb \<and> path_by_shm s pb pathbc pc \<and> pathac = pathbc @ pathab"
+ − 154
by (drule pbs_prop6_aux, auto)
+ − 155
+ − 156
lemma pbs_prop7_aux:
+ − 157
"path_by_shm s pa pathac pc \<Longrightarrow> valid s \<longrightarrow> (\<forall> pb \<in> set (map Trd pathac). \<exists> pathab pathbc. path_by_shm s pa pathab pb \<and> path_by_shm s pb pathbc pc \<and> pathac = pathbc @ pathab)"
+ − 158
apply (erule path_by_shm.induct)
+ − 159
apply simp
+ − 160
apply clarify
+ − 161
apply (case_tac "pb = p''", simp)
+ − 162
apply (rule_tac x = "(p',h,p'') # path" in exI, simp)
+ − 163
apply (rule conjI, erule pbs2, simp+)
+ − 164
apply (rule pbs1, clarsimp simp:one_flow_shm_def procs_of_shm_prop2)
+ − 165
apply (erule_tac x = pb in ballE, simp_all, clarsimp)
+ − 166
apply (rule_tac x = pathab in exI, simp)
+ − 167
apply (erule pbs2, auto)
+ − 168
done
+ − 169
+ − 170
lemma pbs_prop7:
+ − 171
"\<lbrakk>path_by_shm s pa pathac pc; pb \<in> set (map Trd pathac); valid s\<rbrakk>
+ − 172
\<Longrightarrow> \<exists> pathab pathbc. path_by_shm s pa pathab pb \<and> path_by_shm s pb pathbc pc \<and> pathac = pathbc @ pathab"
+ − 173
by (drule pbs_prop7_aux, drule mp, simp, erule_tac x = pb in ballE, auto)
+ − 174
+ − 175
lemma pbs_prop8:
+ − 176
"path_by_shm s p path p' \<Longrightarrow> (set (map Fst path) - {p}) = (set (map Trd path) - {p'})"
+ − 177
proof (induct rule:path_by_shm.induct)
+ − 178
case (pbs1 p s)
+ − 179
thus ?case by simp
+ − 180
next
+ − 181
case (pbs2 s p path p' h p'')
+ − 182
assume p1:"path_by_shm s p path p'" and p2: "set (map Fst path) - {p} = set (map Trd path) - {p'}"
+ − 183
and p3: "one_flow_shm s h p' p''" and p4: "p'' \<notin> set (map Fst path)"
+ − 184
show "set (map Fst ((p', h, p'') # path)) - {p} = set (map Trd ((p', h, p'') # path)) - {p''}"
+ − 185
(is "?left = ?right")
+ − 186
proof (cases "path = []")
+ − 187
case True
+ − 188
with p1 have "p = p'" by (drule_tac pbs_prop2, simp)
+ − 189
thus ?thesis using True
+ − 190
using p2 by (simp)
+ − 191
next
+ − 192
case False
+ − 193
with p1 have a1: "p \<noteq> p'" by (drule_tac pbs_prop2, simp)
+ − 194
from p3 have a2: "p' \<noteq> p''" by (simp add:one_flow_shm_def)
+ − 195
from p1 False have a3: "p' \<in> set (map Trd path)" by (drule_tac pbs_prop4, simp+)
+ − 196
from p4 p1 False have a4: "p \<noteq> p''" by (drule_tac pbs_prop3, auto)
+ − 197
with p2 a2 p4 have a5: "p'' \<notin> set (map Trd path)" by auto
+ − 198
+ − 199
have "?left = (set (map Fst path) - {p}) \<union> {p'}" using a1 by auto
+ − 200
moreover have "... = (set (map Trd path) - {p'}) \<union> {p'}"
+ − 201
using p2 by auto
+ − 202
moreover have "... = set (map Trd path)" using a3 by auto
+ − 203
moreover have "... = set (map Trd path) - {p''}" using a5 by simp
+ − 204
moreover have "... = ?right" by simp
+ − 205
ultimately show ?thesis by simp
+ − 206
qed
+ − 207
qed
+ − 208
+ − 209
lemma pbs_prop9_aux[rule_format]:
+ − 210
"path_by_shm s p path p' \<Longrightarrow> h \<in> set (map Snd path) \<and> valid s \<longrightarrow> (\<exists> pa pb patha pathb. path_by_shm s p patha pa \<and> path_by_shm s pb pathb p' \<and> one_flow_shm s h pa pb \<and> path = pathb @ [(pa, h, pb)] @ patha \<and> h \<notin> set (map Snd patha))"
+ − 211
apply (erule path_by_shm.induct, simp)
+ − 212
apply (rule impI, case_tac "h \<in> set (map Snd path)", simp_all)
+ − 213
apply (erule exE|erule conjE)+
+ − 214
apply (rule_tac x = pa in exI, rule_tac x = pb in exI, rule_tac x = patha in exI, simp)
+ − 215
apply (rule pbs2, auto)
+ − 216
apply (rule_tac x = p' in exI, rule_tac x = p'' in exI, rule_tac x = path in exI, simp)
+ − 217
apply (rule pbs1, clarsimp simp:one_flow_shm_def procs_of_shm_prop2)
+ − 218
done
+ − 219
+ − 220
lemma pbs_prop9:
+ − 221
"\<lbrakk>h \<in> set (map Snd path); path_by_shm s p path p'; valid s\<rbrakk>
+ − 222
\<Longrightarrow> \<exists> pa pb patha pathb. path_by_shm s p patha pa \<and> path_by_shm s pb pathb p' \<and>
+ − 223
one_flow_shm s h pa pb \<and> path = pathb @ [(pa, h, pb)] @ patha \<and> h \<notin> set (map Snd patha)"
+ − 224
by (rule pbs_prop9_aux, auto)
+ − 225
+ − 226
lemma path_by_shm_trans_aux[rule_format]:
+ − 227
"path_by_shm s p' path' p'' \<Longrightarrow> valid s \<longrightarrow> (\<forall> p path. path_by_shm s p path p' \<longrightarrow> (\<exists> path''. path_by_shm s p path'' p''))"
+ − 228
proof (induct rule:path_by_shm.induct)
+ − 229
case (pbs1 p s)
+ − 230
thus ?case
+ − 231
by (clarify, rule_tac x = path in exI, simp)
+ − 232
next
+ − 233
case (pbs2 s p path p' h p'')
+ − 234
hence p1: "path_by_shm s p path p'" and p2: "one_flow_shm s h p' p''"
+ − 235
and p3: "valid s \<longrightarrow> (\<forall>pa path. path_by_shm s pa path p \<longrightarrow> (\<exists>path''. path_by_shm s pa path'' p'))"
+ − 236
and p4: "p'' \<notin> set (map Fst path)" by auto
+ − 237
show ?case
+ − 238
proof clarify
+ − 239
fix pa path'
+ − 240
assume p5: "path_by_shm s pa path' p" and p6: "valid s"
+ − 241
with p3 obtain path'' where a1: "path_by_shm s pa path'' p'" by auto
+ − 242
have p3': "\<forall>pa path. path_by_shm s pa path p \<longrightarrow> (\<exists>path''. path_by_shm s pa path'' p')"
+ − 243
using p3 p6 by simp
+ − 244
show "\<exists>path''. path_by_shm s pa path'' p''"
+ − 245
proof (cases "p'' \<in> set (map Fst path'')")
+ − 246
case True
+ − 247
then obtain res where "path_by_shm s pa res p''" using a1 pbs_prop6 p6 by blast
+ − 248
thus ?thesis by auto
+ − 249
next
+ − 250
case False
+ − 251
with p2 a1 show ?thesis
+ − 252
apply (rule_tac x = "(p', h, p'') # path''" in exI)
+ − 253
apply (rule path_by_shm.intros(2), auto)
+ − 254
done
+ − 255
qed
+ − 256
qed
+ − 257
qed
+ − 258
+ − 259
lemma path_by_shm_trans:
+ − 260
"\<lbrakk>path_by_shm s p path p'; path_by_shm s p' path' p''; valid s\<rbrakk> \<Longrightarrow> \<exists> path''. path_by_shm s p path'' p''"
+ − 261
by (drule_tac p' = p' and p'' = p'' in path_by_shm_trans_aux, auto)
+ − 262
+ − 263
lemma path_by_shm_intro1_prop:
+ − 264
"\<not> path_by_shm s p [] p \<Longrightarrow> p \<notin> current_procs s"
+ − 265
by (auto dest:path_by_shm.intros(1))
+ − 266
+ − 267
lemma path_by_shm_intro3:
+ − 268
"\<lbrakk>path_by_shm s p path from; (from, SHM_RDWR) \<in> procs_of_shm s h; (to, flag) \<in> procs_of_shm s h;
+ − 269
to \<notin> set (map Fst path); from \<noteq> to\<rbrakk>
+ − 270
\<Longrightarrow> path_by_shm s p ((from, h, to)#path) to"
+ − 271
apply (rule path_by_shm.intros(2), simp_all)
+ − 272
by (auto simp:one_flow_shm_def)
+ − 273
+ − 274
lemma path_by_shm_intro4:
+ − 275
"\<lbrakk>(p, flag) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> path_by_shm s p [] p"
+ − 276
by (drule procs_of_shm_prop2, simp, simp add:path_by_shm.intros(1))
+ − 277
+ − 278
lemma path_by_shm_intro5:
+ − 279
"\<lbrakk>(from, SHM_RDWR) \<in> procs_of_shm s h; (to,flag) \<in> procs_of_shm s h; valid s; from \<noteq> to\<rbrakk>
+ − 280
\<Longrightarrow> path_by_shm s from [(from, h, to)] to"
+ − 281
apply (rule_tac p' = "from" and h = h in path_by_shm.intros(2))
+ − 282
apply (rule path_by_shm.intros(1), simp add:procs_of_shm_prop2)
+ − 283
apply (simp add:one_flow_shm_def, rule_tac x = flag in exI, auto)
+ − 284
done
+ − 285
+ − 286
(* p'' \<notin> set (map Fst path): not duplicated target process;
+ − 287
* p1 - ha \<rightarrow> p2; p2 - hb \<rightarrow> p3; p3 - ha \<rightarrow> p4; so path_by_shm p1 [(p3,ha,p4), (p2,hb,p3),(p1,ha,p2)] p4,
+ − 288
* but this could be also path_by_shm p1 [(p1,ha,p4)] p4, so the former one is redundant! *)
+ − 289
+ − 290
inductive path_by_shm':: "t_state \<Rightarrow> t_process \<Rightarrow> t_edge_shm list \<Rightarrow> t_process \<Rightarrow> bool"
+ − 291
where
+ − 292
pbs1': "p \<in> current_procs s \<Longrightarrow> path_by_shm' s p [] p"
+ − 293
| pbs2': "\<lbrakk>path_by_shm' s p path p'; one_flow_shm s h p' p''; p'' \<notin> set (map Fst path);
+ − 294
h \<notin> set (map Snd path)\<rbrakk>
+ − 295
\<Longrightarrow> path_by_shm' s p ((p', h, p'')# path) p''"
+ − 296
+ − 297
lemma pbs_prop10:
+ − 298
"\<lbrakk>path_by_shm s p path p'; one_flow_shm s h p' p''; valid s\<rbrakk> \<Longrightarrow> \<exists>path'. path_by_shm s p path' p''"
+ − 299
apply (case_tac "p'' \<in> set (map Fst path)")
+ − 300
apply (drule_tac pb = p'' in pbs_prop6, simp+)
+ − 301
apply ((erule exE|erule conjE)+, rule_tac x = pathab in exI, simp)
+ − 302
apply (rule_tac x = "(p', h, p'') # path" in exI)
+ − 303
apply (erule pbs2, simp+)
+ − 304
done
+ − 305
+ − 306
lemma pbs'_imp_pbs[rule_format]:
+ − 307
"path_by_shm' s p path p' \<Longrightarrow> valid s \<longrightarrow> (\<exists> path'. path_by_shm s p path' p')"
+ − 308
apply (erule path_by_shm'.induct)
+ − 309
apply (rule impI, rule_tac x = "[]" in exI, simp add:pbs1)
+ − 310
apply (rule impI, clarsimp)
+ − 311
apply (erule pbs_prop10, simp+)
+ − 312
done
+ − 313
+ − 314
lemma pbs_imp_pbs'[rule_format]:
+ − 315
"path_by_shm s p path p' \<Longrightarrow> valid s \<longrightarrow> (\<exists> path'. path_by_shm' s p path' p')"
+ − 316
apply (erule path_by_shm.induct)
+ − 317
apply (rule impI, rule_tac x = "[]" in exI, erule pbs1')
+ − 318
apply (rule impI, simp, erule exE) (*
+ − 319
apply ( erule exE, case_tac "h \<in> set (map Snd path)")
+ − 320
apply (drule_tac s = s and p = p and p' = p' in pbs_prop9, simp+) defer
+ − 321
apply (rule_tac x = "(p', h, p'') # path'" in exI)
+ − 322
apply (erule pbs2', simp+)
+ − 323
apply ((erule exE|erule conjE)+)
+ − 324
apply (rule_tac x = "(pa, h, p'') # patha" in exI)
+ − 325
apply (erule pbs2', auto simp:one_flow_shm_def)
+ − 326
done*)
+ − 327
sorry
+ − 328
+ − 329
+ − 330
lemma pbs'_eq_pbs:
+ − 331
"valid s \<Longrightarrow> (\<exists> path'. path_by_shm' s p path' p') = (\<exists> path. path_by_shm s p path p')"
+ − 332
by (rule iffI, auto intro:pbs_imp_pbs' pbs'_imp_pbs)
+ − 333
+ − 334
definition flow_by_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"
+ − 335
where
+ − 336
"flow_by_shm s p p' \<equiv> \<exists> path. path_by_shm s p path p'"
+ − 337
+ − 338
lemma flow_by_shm_intro':
+ − 339
"valid s \<Longrightarrow> flow_by_shm s p p' = (\<exists> path. path_by_shm' s p path p')"
+ − 340
by (auto simp:flow_by_shm_def pbs'_eq_pbs)
+ − 341
+ − 342
lemma one_step_flows: "\<lbrakk>one_flow_shm s h p p'; valid s\<rbrakk> \<Longrightarrow> flow_by_shm s p p'"
+ − 343
by (drule one_step_path, auto simp:flow_by_shm_def)
+ − 344
+ − 345
lemma flow_by_shm_trans:
+ − 346
"\<lbrakk>flow_by_shm s p p'; flow_by_shm s p' p''; valid s\<rbrakk> \<Longrightarrow> flow_by_shm s p p''"
+ − 347
by (auto simp:flow_by_shm_def intro!:path_by_shm_trans)
+ − 348
+ − 349
lemma flow_by_shm_intro1_prop:
+ − 350
"\<not> flow_by_shm s p p \<Longrightarrow> p \<notin> current_procs s"
+ − 351
by (auto dest:path_by_shm.intros(1) simp:flow_by_shm_def)
+ − 352
+ − 353
lemma flow_by_shm_intro1:
+ − 354
"p \<in> current_procs s \<Longrightarrow> flow_by_shm s p p"
+ − 355
by (auto dest:path_by_shm.intros(1) simp:flow_by_shm_def)
+ − 356
+ − 357
lemma flow_by_shm_intro2:
+ − 358
"\<lbrakk>flow_by_shm s p p'; one_flow_shm s h p' p''; valid s\<rbrakk> \<Longrightarrow> flow_by_shm s p p''"
+ − 359
by (auto intro:flow_by_shm_trans dest:one_step_flows)
+ − 360
+ − 361
lemma flow_by_shm_intro3:
+ − 362
"\<lbrakk>flow_by_shm s p from; (from, SHM_RDWR) \<in> procs_of_shm s h; (to, flag) \<in> procs_of_shm s h; from \<noteq> to; valid s\<rbrakk>
+ − 363
\<Longrightarrow> flow_by_shm s p to"
+ − 364
apply (rule flow_by_shm_intro2)
+ − 365
by (auto simp:one_flow_shm_def)
+ − 366
+ − 367
lemma flow_by_shm_intro4:
+ − 368
"\<lbrakk>(p, flag) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> flow_by_shm s p p"
+ − 369
by (drule procs_of_shm_prop2, simp, simp add:flow_by_shm_intro1)
+ − 370
+ − 371
lemma flow_by_shm_intro5:
+ − 372
"\<lbrakk>(from, SHM_RDWR) \<in> procs_of_shm s h; (to,flag) \<in> procs_of_shm s h; valid s; from \<noteq> to\<rbrakk>
+ − 373
\<Longrightarrow> flow_by_shm s from to"
+ − 374
apply (rule_tac p' = "from" and h = h in flow_by_shm_intro2)
+ − 375
apply (rule flow_by_shm_intro1, simp add:procs_of_shm_prop2)
+ − 376
apply (simp add:one_flow_shm_def, rule_tac x = flag in exI, auto)
+ − 377
done
+ − 378
+ − 379
lemma flow_by_shm_intro6:
+ − 380
"path_by_shm s p path p' \<Longrightarrow> flow_by_shm s p p'"
+ − 381
by (auto simp:flow_by_shm_def)
+ − 382
+ − 383
(********* simpset for inductive Info_flow_shm **********)
+ − 384
lemma path_by_shm_detach1_aux:
+ − 385
"path_by_shm s' pa path pb \<Longrightarrow> valid (Detach p h # s) \<and> (s' = Detach p h # s)
+ − 386
\<longrightarrow> \<not> edge_related path p h \<and> path_by_shm s pa path pb"
+ − 387
apply (erule path_by_shm.induct, simp)
+ − 388
apply (rule impI, rule path_by_shm.intros(1), simp+)
+ − 389
by (auto simp:one_flow_shm_def split:if_splits intro:path_by_shm_intro3)
+ − 390
+ − 391
lemma path_by_shm_detach1:
+ − 392
"\<lbrakk>path_by_shm (Detach p h # s) pa path pb; valid (Detach p h # s)\<rbrakk>
+ − 393
\<Longrightarrow> \<not> edge_related path p h \<and> path_by_shm s pa path pb"
+ − 394
by (auto dest:path_by_shm_detach1_aux)
+ − 395
+ − 396
lemma path_by_shm_detach2_aux[rule_format]:
+ − 397
"path_by_shm s pa path pb \<Longrightarrow> valid (Detach p h # s) \<and> \<not> edge_related path p h
+ − 398
\<longrightarrow> path_by_shm (Detach p h # s) pa path pb"
+ − 399
apply (induct rule:path_by_shm.induct)
+ − 400
apply (rule impI, rule path_by_shm.intros(1), simp)
+ − 401
apply (rule impI, erule conjE, simp split:if_splits)
+ − 402
apply (rule path_by_shm.intros(2), simp)
+ − 403
apply (simp add:one_flow_shm_detach)
+ − 404
apply (rule impI, simp+)
+ − 405
done
+ − 406
+ − 407
lemma path_by_shm_detach2:
+ − 408
"\<lbrakk>valid (Detach p h # s); \<not> edge_related path p h; path_by_shm s pa path pb\<rbrakk>
+ − 409
\<Longrightarrow> path_by_shm (Detach p h # s) pa path pb"
+ − 410
by (auto intro!:path_by_shm_detach2_aux)
+ − 411
+ − 412
lemma path_by_shm_detach:
+ − 413
"valid (Detach p h # s) \<Longrightarrow>
+ − 414
path_by_shm (Detach p h # s) pa path pb = (\<not> edge_related path p h \<and> path_by_shm s pa path pb)"
+ − 415
by (auto dest:path_by_shm_detach1 path_by_shm_detach2)
+ − 416
+ − 417
lemma flow_by_shm_detach:
+ − 418
"valid (Detach p h # s) \<Longrightarrow>
+ − 419
flow_by_shm (Detach p h # s) pa pb = (\<exists> path. \<not> edge_related path p h \<and> path_by_shm s pa path pb)"
+ − 420
by (auto dest:path_by_shm_detach simp:flow_by_shm_def)
+ − 421
+ − 422
lemma path_by_shm'_attach1_aux:
+ − 423
"path_by_shm' s' pa path pb \<Longrightarrow> valid s' \<and> (s' = Attach p h flag # s) \<longrightarrow>
+ − 424
(path_by_shm' s pa path pb) \<or>
+ − 425
(\<exists> path1 path2 p'. path_by_shm' s pa path1 p' \<and> path_by_shm' s p path2 pb \<and>
+ − 426
(p', SHM_RDWR) \<in> procs_of_shm s h \<and> path = path2 @ [(p', h, p)] @ path1 ) \<or>
+ − 427
(\<exists> path1 path2 p' flag'. path_by_shm' s pa path1 p \<and> path_by_shm' s p' path2 pb \<and>
+ − 428
(p', flag') \<in> procs_of_shm s h \<and> path = path2 @ [(p, h, p')] @ path1 \<and> flag = SHM_RDWR)"
+ − 429
apply (erule path_by_shm'.induct)
+ − 430
apply (simp, rule impI, rule pbs1', simp)
+ − 431
apply (rule impI, erule impE, clarsimp)
+ − 432
apply (erule disjE)
+ − 433
apply (clarsimp simp:one_flow_shm_attach split:if_splits)
+ − 434
apply (erule disjE, clarsimp)
+ − 435
apply (erule_tac x = path in allE, clarsimp)
+ − 436
apply (erule impE, rule pbs1', erule procs_of_shm_prop2, erule vd_cons, simp)
+ − 437
apply (erule disjE, clarsimp)
+ − 438
apply (rule_tac x = path in exI, rule_tac x = "[]" in exI, rule_tac x = p' in exI, simp)
+ − 439
apply (rule pbs1', drule vt_grant_os, clarsimp)
+ − 440
apply (drule_tac p = pa and p' = p' and p'' = p'' in pbs2', simp+)
+ − 441
apply (drule_tac p = pa and p' = p' and p'' = p'' in pbs2', simp+)
+ − 442
+ − 443
apply (erule disjE)
+ − 444
apply ((erule exE|erule conjE)+, clarsimp split:if_splits simp:one_flow_shm_attach)
+ − 445
apply (clarsimp simp:one_flow_shm_attach split:if_splits)
+ − 446
apply (erule disjE, clarsimp)
+ − 447
apply (clarsimp)
+ − 448
+ − 449
+ − 450
apply (erule conjE)+
+ − 451
+ − 452
+ − 453
+ − 454
apply (erule conjE, clarsimp simp only:one_flow_shm_attach split:if_splits)
+ − 455
apply simp
+ − 456
+ − 457
+ − 458
+ − 459
lemma path_by_shm_attach1_aux:
+ − 460
"path_by_shm s' pa path pb \<Longrightarrow> valid s' \<and> (s' = Attach p h flag # s) \<longrightarrow>
+ − 461
path_by_shm s pa path pb \<or>
+ − 462
(if (pa = p \<and> flag = SHM_RDWR)
+ − 463
then \<exists> p' flagb path'. (p', flagb) \<in> procs_of_shm s h \<and>
+ − 464
path_by_shm s p' path' pb \<and> path = path' @ [(p, h, p')]
+ − 465
else if (pb = p)
+ − 466
then \<exists> p' path'. path_by_shm s pa path' p' \<and> path = (p', h, p) # path' \<and>
+ − 467
(p', SHM_RDWR) \<in> procs_of_shm s h
+ − 468
else (\<exists> p' flag' patha pathb. path_by_shm s pa patha p \<and> flag = SHM_RDWR \<and>
+ − 469
(p', flag') \<in> procs_of_shm s h \<and> path_by_shm s p' pathb pb \<and>
+ − 470
path = pathb @ [(p, h, p')] @ patha) \<or>
+ − 471
(\<exists> p' patha pathb. path_by_shm s pa patha p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and>
+ − 472
path_by_shm s p pathb pb \<and> path = pathb @ [(p', h, p)] @ patha))"
+ − 473
proof (induct rule:path_by_shm.induct)
+ − 474
case (pbs1 proc \<tau>)
+ − 475
show ?case
+ − 476
proof (rule impI)
+ − 477
assume pre: "valid \<tau> \<and> \<tau> = Attach p h flag # s"
+ − 478
from pbs1 pre have "proc \<in> current_procs s" by simp
+ − 479
thus "path_by_shm s proc [] proc \<or>
+ − 480
(if proc = p \<and> flag = SHM_RDWR
+ − 481
then \<exists>p' flagb path'.
+ − 482
(p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' path' proc \<and> [] = path' @ [(p, h, p')]
+ − 483
else if proc = p
+ − 484
then \<exists>p' path'.
+ − 485
path_by_shm s proc path' p' \<and> [] = (p', h, p) # path' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h
+ − 486
else (\<exists>p' flag' patha pathb.
+ − 487
path_by_shm s proc patha p \<and>
+ − 488
flag = SHM_RDWR \<and>
+ − 489
(p', flag') \<in> procs_of_shm s h \<and>
+ − 490
path_by_shm s p' pathb proc \<and> [] = pathb @ [(p, h, p')] @ patha) \<or>
+ − 491
(\<exists>p' patha pathb.
+ − 492
path_by_shm s proc patha p' \<and>
+ − 493
(p', SHM_RDWR) \<in> procs_of_shm s h \<and>
+ − 494
path_by_shm s p pathb proc \<and> [] = pathb @ [(p', h, p)] @ patha))"
+ − 495
by (auto intro:path_by_shm.intros)
+ − 496
qed
+ − 497
next
+ − 498
case (pbs2 \<tau> pa path pb h' pc)
+ − 499
thus ?case
+ − 500
proof (rule_tac impI)
+ − 501
assume p1:"path_by_shm \<tau> pa path pb" and p2: "valid \<tau> \<and> \<tau> = Attach p h flag # s \<longrightarrow>
+ − 502
path_by_shm s pa path pb \<or>
+ − 503
(if pa = p \<and> flag = SHM_RDWR
+ − 504
then \<exists>p' flagb path'. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' path' pb \<and> path = path' @ [(p, h, p')]
+ − 505
else if pb = p
+ − 506
then \<exists>p' path'. path_by_shm s pa path' p' \<and> path = (p', h, p) # path' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h
+ − 507
else (\<exists>p' flag' pathaa pathb. path_by_shm s pa pathaa p \<and> flag = SHM_RDWR \<and>
+ − 508
(p', flag') \<in> procs_of_shm s h \<and> path_by_shm s p' pathb pb \<and>
+ − 509
path = pathb @ [(p, h, p')] @ pathaa) \<or>
+ − 510
(\<exists>p' pathaa pathb. path_by_shm s pa pathaa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and>
+ − 511
path_by_shm s p pathb pb \<and> path = pathb @ [(p', h, p)] @ pathaa))"
+ − 512
and p3: "one_flow_shm \<tau> h' pb pc" and p4: "valid \<tau> \<and> \<tau> = Attach p h flag # s"
+ − 513
+ − 514
from p2 and p4 have p2': "
+ − 515
path_by_shm s pa path pb \<or>
+ − 516
(if pa = p \<and> flag = SHM_RDWR
+ − 517
then \<exists>p' flagb path'. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' path' pb \<and> path = path' @ [(p, h, p')]
+ − 518
else if pb = p
+ − 519
then \<exists>p' path'. path_by_shm s pa path' p' \<and> path = (p', h, p) # path' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h
+ − 520
else (\<exists>p' flag' pathaa pathb. path_by_shm s pa pathaa p \<and> flag = SHM_RDWR \<and>
+ − 521
(p', flag') \<in> procs_of_shm s h \<and> path_by_shm s p' pathb pb \<and>
+ − 522
path = pathb @ [(p, h, p')] @ pathaa) \<or>
+ − 523
(\<exists>p' pathaa pathb. path_by_shm s pa pathaa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and>
+ − 524
path_by_shm s p pathb pb \<and> path = pathb @ [(p', h, p)] @ pathaa))"
+ − 525
by (erule_tac impE, simp)
+ − 526
from p4 have p5: "valid s" and p6: "os_grant s (Attach p h flag)" by (auto intro:vd_cons dest:vt_grant_os)
+ − 527
from p6 have "p \<in> current_procs s" by simp hence p7:"path_by_shm s p [] p" by (erule_tac path_by_shm.intros)
+ − 528
from p3 p4 have p8: "if (h' = h)
+ − 529
then (pb = p \<and> pc \<noteq> p \<and> flag = SHM_RDWR \<and> (\<exists> flagb. (pc, flagb) \<in> procs_of_shm s h)) \<or>
+ − 530
(pc = p \<and> pb \<noteq> p \<and> (pb, SHM_RDWR) \<in> procs_of_shm s h) \<or>
+ − 531
(one_flow_shm s h pb pc)
+ − 532
else one_flow_shm s h' pb pc" by (auto simp add:one_flow_shm_attach)
+ − 533
+ − 534
+ − 535
(*
+ − 536
have "\<And> flagb. (pc, flagb) \<in> procs_of_shm s h
+ − 537
\<Longrightarrow> \<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' [] pc"
+ − 538
apply (rule_tac x= pc in exI, rule_tac x = flagb in exI, frule procs_of_shm_prop2)
+ − 539
by (simp add:p5, simp add:path_by_shm.intros(1))
+ − 540
hence p10: "\<not> path_by_shm s p path pc \<Longrightarrow> (\<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' pc) \<or>
+ − 541
path_by_shm s pa pc"
+ − 542
using p2' p7 p8 p5
+ − 543
by (auto split:if_splits dest:path_by_shm.intros(2))
+ − 544
(* apply (rule_tac x = pb in exI, simp add:one_flow_flows, rule_tac x = flagb in exI, simp)+ *) *)
+ − 545
+ − 546
from p1 have a0: "(path = []) = (pa = pb)" using pbs_prop2 by simp
+ − 547
have a1:"\<lbrakk>pa = p; flag = SHM_RDWR; \<not> path_by_shm s pa path pb\<rbrakk> \<Longrightarrow>
+ − 548
\<exists>p' flagb path'. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' path' pb \<and> path = path' @ [(p, h, p')]"
+ − 549
using p2' by auto
+ − 550
have b1: "\<lbrakk>pa = p; flag = SHM_RDWR; \<not> path_by_shm s pa path pc\<rbrakk> \<Longrightarrow>
+ − 551
\<exists>p' flagb path'. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' path' pc \<and>
+ − 552
(pb, h', pc) # path = path' @ [(p, h, p')]"
+ − 553
+ − 554
+ − 555
using p8 a1 p7 p5 a0
+ − 556
apply (auto split:if_splits elim:path_by_shm_intro4)
+ − 557
apply (rule_tac x = pb in exI, rule conjI, rule_tac x = SHM_RDWR in exI, simp)
+ − 558
apply (rule_tac x = pc in exI, rule conjI, rule_tac x = flagb in exI, simp)
+ − 559
apply (rule_tac x = "[]" in exI, rule conjI)
+ − 560
apply (erule path_by_shm_intro4, simp)
+ − 561
+ − 562
apply (case_tac "path_by_shm s pa path pb", simp) defer
+ − 563
apply (drule a1, simp+, clarsimp)
+ − 564
apply (rule conjI, rule_tac x = flagb in exI, simp)
+ − 565
apply (rule path_by_shm_
+ − 566
using p2' p8 p5
+ − 567
apply (auto split:if_splits dest!:pbs_prop2' simp:path_by_shm_intro4)
+ − 568
apply (drule pbs_prop2', simp)
+ − 569
apply (erule_tac x = pc in allE, simp add:path_by_shm_intro4)
+ − 570
+ − 571
apply (drule_tac x = "pc" in allE)
+ − 572
+ − 573
apply simp
+ − 574
+ − 575
sorry
+ − 576
moreover have "pc = p \<Longrightarrow> (\<exists>p' path'. path_by_shm s pa path' p' \<and>
+ − 577
(pb, h', pc) # path = path' @ [(p', h, p)] \<and> (p', SHM_RDWR) \<in> procs_of_shm s h) \<or>
+ − 578
(path_by_shm s pa path pc \<and> \<not> edge_related path p h)"
+ − 579
using p2' p7 p8 p5
+ − 580
sorry (*
+ − 581
apply (auto split:if_splits intro:path_by_shm_intro3 simp:one_flow_shm_def) *)
+ − 582
moreover have "\<lbrakk>pc \<noteq> p; pa \<noteq> p \<or> flag \<noteq> SHM_RDWR\<rbrakk> \<Longrightarrow>
+ − 583
(\<exists>p' flag' pathaa pathb. path_by_shm s pa pathaa p \<and> flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and>
+ − 584
path_by_shm s p' pathb pc \<and> (pb, h', pc) # path = pathaa @ [(p, h, p')] @ pathb) \<or>
+ − 585
(\<exists>p' pathaa pathb. path_by_shm s pa pathaa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and>
+ − 586
path_by_shm s p pathb pc \<and> (pb, h', pc) # path = pathaa @ [(p', h, p)] @ pathb) \<or>
+ − 587
(path_by_shm s pa path pc \<and> \<not> edge_related path p h)"
+ − 588
using p2' p7 p8 p5 (*
+ − 589
apply (auto split:if_splits intro:path_by_shm_intro3 simp:one_flow_shm_def)
+ − 590
apply (rule_tac x = pc in exI, simp add:path_by_shm_intro4)
+ − 591
apply (rule_tac x = flagb in exI, simp)
+ − 592
done *)
+ − 593
sorry
+ − 594
ultimately
+ − 595
show "if (pb, h', pc) # path = [] then pa = pc \<and> pa \<in> current_procs s
+ − 596
else path_by_shm s pa ((pb, h', pc) # path) pc \<and> \<not> edge_related ((pb, h', pc) # path) p h \<or>
+ − 597
(if pa = p \<and> flag = SHM_RDWR
+ − 598
then \<exists>p' flagb path'. (p', flagb) \<in> procs_of_shm s h \<and>
+ − 599
path_by_shm s p' path' pc \<and> (pb, h', pc) # path = path' @ [(p, h, p')]
+ − 600
else if pc = p
+ − 601
then \<exists>p' path'. path_by_shm s pa path' p' \<and>
+ − 602
(pb, h', pc) # path = (p', h, p) # path' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h
+ − 603
else (\<exists>p' flag' pathaa pathb. path_by_shm s pa pathaa p \<and> flag = SHM_RDWR \<and>
+ − 604
(p', flag') \<in> procs_of_shm s h \<and>
+ − 605
path_by_shm s p' pathb pc \<and> (pb, h', pc) # path = pathb @ [(p, h, p')] @ pathaa) \<or>
+ − 606
(\<exists>p' pathaa pathb. path_by_shm s pa pathaa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and>
+ − 607
path_by_shm s p pathb pc \<and> (pb, h', pc) # path = pathb @ [(p', h, p)] @ pathaa))"
+ − 608
apply (auto split:if_splits)
+ − 609
using p7 by auto
+ − 610
qed
+ − 611
qed
+ − 612
+ − 613
lemma path_by_shm_attach1:
+ − 614
"\<lbrakk>valid (Attach p h flag # s); path_by_shm (Attach p h flag # s) pa pb\<rbrakk>
+ − 615
\<Longrightarrow> (if path_by_shm s pa pb then True else
+ − 616
(if (pa = p \<and> flag = SHM_RDWR)
+ − 617
then (\<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' pb)
+ − 618
else if (pb = p)
+ − 619
then (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> path_by_shm s pa p')
+ − 620
else (\<exists> p' flag'. path_by_shm s pa p \<and> flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and>
+ − 621
path_by_shm s p' pb) \<or>
+ − 622
(\<exists> p'. path_by_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> path_by_shm s p pb)
+ − 623
) )"
+ − 624
apply (drule_tac p = p and h = h and flag = flag in path_by_shm_attach1_aux)
+ − 625
by auto
+ − 626
+ − 627
lemma path_by_shm_attach_aux[rule_format]:
+ − 628
"path_by_shm s pa pb \<Longrightarrow> valid (Attach p h flag # s) \<longrightarrow> path_by_shm (Attach p h flag # s) pa pb"
+ − 629
apply (erule path_by_shm.induct)
+ − 630
apply (rule impI, rule path_by_shm.intros(1), simp)
+ − 631
apply (rule impI, simp, rule_tac h = ha in path_by_shm.intros(2), simp)
+ − 632
apply (auto simp add:one_flow_shm_simps)
+ − 633
done
+ − 634
+ − 635
lemma path_by_shm_attach2:
+ − 636
"\<lbrakk>valid (Attach p h flag # s); if path_by_shm s pa pb then True else
+ − 637
(if (pa = p \<and> flag = SHM_RDWR)
+ − 638
then (\<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' pb)
+ − 639
else if (pb = p)
+ − 640
then (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> path_by_shm s pa p')
+ − 641
else (\<exists> p' flag'. path_by_shm s pa p \<and> flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and>
+ − 642
path_by_shm s p' pb) \<or>
+ − 643
(\<exists> p'. path_by_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> path_by_shm s p pb))\<rbrakk>
+ − 644
\<Longrightarrow> path_by_shm (Attach p h flag # s) pa pb"
+ − 645
apply (frule vt_grant_os, frule vd_cons)
+ − 646
apply (auto split:if_splits intro:path_by_shm_intro3 simp:one_flow_shm_def intro:path_by_shm_attach_aux)
+ − 647
apply (rule_tac p' = p' in Info_flow_trans)
+ − 648
apply (rule_tac p' = p and h = h in path_by_shm.intros(2))
+ − 649
apply (rule path_by_shm.intros(1), simp)
+ − 650
apply (simp add:one_flow_shm_simps, simp add:one_flow_shm_def)
+ − 651
apply (rule conjI, rule notI, simp, rule_tac x = flagb in exI, simp)
+ − 652
apply (simp add:path_by_shm_attach_aux)
+ − 653
+ − 654
apply (rule_tac p' = p' in Info_flow_trans)
+ − 655
apply (rule_tac p' = p in Info_flow_trans)
+ − 656
apply (simp add:path_by_shm_attach_aux)
+ − 657
apply (rule_tac p' = p and h = h in path_by_shm.intros(2))
+ − 658
apply (rule path_by_shm.intros(1), simp)
+ − 659
apply (simp add:one_flow_shm_simps, simp add:one_flow_shm_def)
+ − 660
apply (rule conjI, rule notI, simp, rule_tac x = flag' in exI, simp)
+ − 661
apply (simp add:path_by_shm_attach_aux)
+ − 662
+ − 663
apply (rule_tac p' = p in Info_flow_trans)
+ − 664
apply (rule_tac p' = p' in Info_flow_trans)
+ − 665
apply (simp add:path_by_shm_attach_aux)
+ − 666
apply (rule_tac p' = p' and h = h in path_by_shm.intros(2))
+ − 667
apply (rule path_by_shm.intros(1), simp add:procs_of_shm_prop2)
+ − 668
apply (simp add:one_flow_shm_simps, simp add:one_flow_shm_def)
+ − 669
apply (rule notI, simp)
+ − 670
apply (simp add:path_by_shm_attach_aux)
+ − 671
+ − 672
apply (rule_tac p' = p in Info_flow_trans)
+ − 673
apply (rule_tac p' = p' in Info_flow_trans)
+ − 674
apply (simp add:path_by_shm_attach_aux)
+ − 675
apply (rule_tac p' = p' and h = h in path_by_shm.intros(2))
+ − 676
apply (rule path_by_shm.intros(1), simp add:procs_of_shm_prop2)
+ − 677
apply (simp add:one_flow_shm_simps, simp add:one_flow_shm_def)
+ − 678
apply (rule notI, simp)
+ − 679
apply (simp add:path_by_shm_attach_aux)
+ − 680
done
+ − 681
+ − 682
lemma path_by_shm_attach:
+ − 683
"valid (Attach p h flag # s) \<Longrightarrow> path_by_shm (Attach p h flag # s) = (\<lambda> pa pb.
+ − 684
path_by_shm s pa pb \<or>
+ − 685
(if (pa = p \<and> flag = SHM_RDWR)
+ − 686
then (\<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' pb)
+ − 687
else if (pb = p)
+ − 688
then (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> path_by_shm s pa p')
+ − 689
else (\<exists> p' flag'. path_by_shm s pa p \<and> flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and>
+ − 690
path_by_shm s p' pb) \<or>
+ − 691
(\<exists> p'. path_by_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> path_by_shm s p pb)
+ − 692
) )"
+ − 693
apply (rule ext, rule ext, rule iffI)
+ − 694
apply (drule_tac pa = pa and pb = pb in path_by_shm_attach1, simp)
+ − 695
apply (auto split:if_splits)[1]
+ − 696
apply (drule_tac pa = pa and pb = pb in path_by_shm_attach2)
+ − 697
apply (auto split:if_splits)
+ − 698
done
+ − 699
+ − 700
+ − 701
+ − 702
lemma info_flow_shm_detach:
+ − 703
"valid (Detach p h # s) \<Longrightarrow> info_flow_shm (Detach p h # s) = (\<lambda> pa pb.
+ − 704
self_shm s pa pb \<or> ((p = pa \<or> p = pb) \<and> (\<exists> h'. h' \<noteq> h \<and> one_flow_shm s h' pa pb)) \<or>
+ − 705
(pa \<noteq> p \<and> pb \<noteq> p \<and> info_flow_shm s pa pb) )"
+ − 706
apply (rule ext, rule ext, frule vt_grant_os)
+ − 707
by (auto simp:info_flow_shm_def one_flow_shm_def)
+ − 708
+ − 709
lemma info_flow_shm_deleteshm:
+ − 710
"valid (DeleteShM p h # s) \<Longrightarrow> info_flow_shm (DeleteShM p h # s) = (\<lambda> pa pb.
+ − 711
self_shm s pa pb \<or> (\<exists> h'. h' \<noteq> h \<and> one_flow_shm s h' pa pb) )"
+ − 712
apply (rule ext, rule ext, frule vt_grant_os)
+ − 713
by (auto simp:info_flow_shm_def one_flow_shm_def)
+ − 714
+ − 715
lemma info_flow_shm_clone:
+ − 716
"valid (Clone p p' fds shms # s) \<Longrightarrow> info_flow_shm (Clone p p' fds shms # s) = (\<lambda> pa pb.
+ − 717
(pa = p' \<and> pb = p') \<or> (pa = p' \<and> pb \<noteq> p' \<and> (\<exists> h \<in> shms. one_flow_shm s h p pb)) \<or>
+ − 718
(pb = p' \<and> pa \<noteq> p' \<and> (\<exists> h \<in> shms. one_flow_shm s h pa p)) \<or>
+ − 719
(pa \<noteq> p' \<and> pb \<noteq> p' \<and> info_flow_shm s pa pb))"
+ − 720
apply (rule ext, rule ext, frule vt_grant_os, frule vd_cons, clarsimp)
+ − 721
apply (frule_tac p = p' in procs_of_shm_prop2', simp)
+ − 722
sorry (*
+ − 723
apply (auto simp:info_flow_shm_def one_flow_shm_def)
+ − 724
done *)
+ − 725
+ − 726
lemma info_flow_shm_execve:
+ − 727
"valid (Execve p f fds # s) \<Longrightarrow> info_flow_shm (Execve p f fds # s) = (\<lambda> pa pb.
+ − 728
(pa = p \<and> pb = p) \<or> (pa \<noteq> p \<and> pb \<noteq> p \<and> info_flow_shm s pa pb) )"
+ − 729
apply (rule ext, rule ext, frule vt_grant_os, frule vd_cons)
+ − 730
by (auto simp:info_flow_shm_def one_flow_shm_def)
+ − 731
+ − 732
lemma info_flow_shm_kill:
+ − 733
"valid (Kill p p' # s) \<Longrightarrow> info_flow_shm (Kill p p' # s) = (\<lambda> pa pb.
+ − 734
pa \<noteq> p' \<and> pb \<noteq> p' \<and> info_flow_shm s pa pb )"
+ − 735
apply (rule ext, rule ext, frule vt_grant_os, frule vd_cons)
+ − 736
by (auto simp:info_flow_shm_def one_flow_shm_def)
+ − 737
+ − 738
lemma info_flow_shm_exit:
+ − 739
"valid (Exit p # s) \<Longrightarrow> info_flow_shm (Exit p # s) = (\<lambda> pa pb.
+ − 740
pa \<noteq> p \<and> pb \<noteq> p \<and> info_flow_shm s pa pb )"
+ − 741
apply (rule ext, rule ext, frule vt_grant_os, frule vd_cons)
+ − 742
by (auto simp:info_flow_shm_def one_flow_shm_def)
+ − 743
+ − 744
lemma info_flow_shm_other:
+ − 745
"\<lbrakk>valid (e # s);
+ − 746
\<forall> p h flag. e \<noteq> Attach p h flag;
+ − 747
\<forall> p h. e \<noteq> Detach p h;
+ − 748
\<forall> p h. e \<noteq> DeleteShM p h;
+ − 749
\<forall> p p' fds shms. e \<noteq> Clone p p' fds shms;
+ − 750
\<forall> p f fds. e \<noteq> Execve p f fds;
+ − 751
\<forall> p p'. e \<noteq> Kill p p';
+ − 752
\<forall> p. e \<noteq> Exit p
+ − 753
\<rbrakk> \<Longrightarrow> info_flow_shm (e # s) = info_flow_shm s"
+ − 754
apply (rule ext, rule ext, frule vt_grant_os, frule vd_cons)
+ − 755
apply (case_tac e, auto simp:info_flow_shm_def one_flow_shm_def dest:procs_of_shm_prop2)
+ − 756
apply (erule_tac x = h in allE, simp)
+ − 757
apply (drule procs_of_shm_prop1, auto)
+ − 758
done
+ − 759
+ − 760
+ − 761
(*
+ − 762
lemma info_flow_shm_prop1:
+ − 763
"\<lbrakk>info_flow_shm s p p'; p \<noteq> p'; valid s\<rbrakk>
+ − 764
\<Longrightarrow> \<exists> h h' flag. (p, SHM_RDWR) \<in> procs_of_shm s h \<and> (p', flag) \<in> procs_of_shm s h'"
+ − 765
by (induct rule: info_flow_shm.induct, auto)
+ − 766
+ − 767
lemma info_flow_shm_cases:
+ − 768
"\<lbrakk>info_flow_shm \<tau> pa pb; \<And>p s. \<lbrakk>s = \<tau> ; pa = p; pb = p; p \<in> current_procs s\<rbrakk> \<Longrightarrow> P;
+ − 769
\<And>s p p' h p'' flag. \<lbrakk>s = \<tau>; pa = p; pb = p''; info_flow_shm s p p'; (p', SHM_RDWR) \<in> procs_of_shm s h;
+ − 770
(p'', flag) \<in> procs_of_shm s h\<rbrakk>\<Longrightarrow> P\<rbrakk>
+ − 771
\<Longrightarrow> P"
+ − 772
by (erule info_flow_shm.cases, auto)
+ − 773
+ − 774
definition one_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"
+ − 775
where
+ − 776
"one_flow_shm s p p' \<equiv> p \<noteq> p' \<and> (\<exists> h flag. (p, SHM_RDWR) \<in> procs_of_shm s h \<and> (p', flag) \<in> procs_of_shm s h)"
+ − 777
+ − 778
inductive flows_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"
+ − 779
where
+ − 780
"p \<in> current_procs s \<Longrightarrow> flows_shm s p p"
+ − 781
| "\<lbrakk>flows_shm s p p'; one_flow_shm s p' p''\<rbrakk> \<Longrightarrow> flows_shm s p p''"
+ − 782
+ − 783
definition attached_procs :: "t_state \<Rightarrow> t_shm \<Rightarrow> t_process set"
+ − 784
where
+ − 785
"attached_procs s h \<equiv> {p. \<exists> flag. (p, flag) \<in> procs_of_shm s h}"
+ − 786
+ − 787
definition flowed_procs:: "t_state \<Rightarrow> t_shm \<Rightarrow> t_process set"
+ − 788
where
+ − 789
"flowed_procs s h \<equiv> {p'. \<exists> p \<in> attached_procs s h. flows_shm s p p'}"
+ − 790
+ − 791
inductive flowed_shm:: "t_state \<Rightarrow> t_process \<Rightarrow> t_shm set"
+ − 792
+ − 793
fun Info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process set"
+ − 794
where
+ − 795
"Info_flow_shm [] = (\<lambda> p. {p'. flows_shm [] p p'})"
+ − 796
| "Info_flow_shm (Attach p h flag # s) = (\<lambda> p'.
+ − 797
if (p' = p) then flowed_procs s h
+ − 798
else if ()
+ − 799
"
+ − 800
+ − 801
+ − 802
lemma info_flow_shm_attach:
+ − 803
"valid (Attach p h flag # s) \<Longrightarrow> info_flow_shm (Attach p h flag # s) = (\<lambda> pa pb. (info_flow_shm s pa pb) \<or>
+ − 804
(if (pa = p)
+ − 805
then (if (flag = SHM_RDWR)
+ − 806
then (\<exists> flag. (pb, flag) \<in> procs_of_shm s h)
+ − 807
else (pb = p))
+ − 808
else (if (pb = p)
+ − 809
then (pa, SHM_RDWR) \<in> procs_of_shm s h
+ − 810
else info_flow_shm s pa pb)) )"
+ − 811
apply (frule vd_cons, frule vt_grant_os, rule ext, rule ext)
+ − 812
apply (case_tac "info_flow_shm s pa pb", simp)
+ − 813
+ − 814
thm info_flow_shm.cases
+ − 815
apply (auto split:if_splits intro:info_flow_shm.intros elim:info_flow_shm_cases)
+ − 816
apply (erule info_flow_shm_cases, simp, simp split:if_splits)
+ − 817
apply (rule_tac p = pa and p' = p' in info_flow_shm.intros(2), simp+)
+ − 818
apply (rule notI, erule info_flow_shm.cases, simp+)
+ − 819
pr 5
+ − 820
*)
+ − 821
lemmas info_flow_shm_simps = info_flow_shm_other (* info_flow_shm_attach *) info_flow_shm_detach info_flow_shm_deleteshm
+ − 822
info_flow_shm_clone info_flow_shm_execve info_flow_shm_kill info_flow_shm_exit
+ − 823
+ − 824
+ − 825
+ − 826
+ − 827
+ − 828
+ − 829
end
+ − 830
+ − 831
end