1(* 2 * Copyright 2014, NICTA 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(NICTA_GPL) 9 *) 10 11theory PolicySystemSAC 12imports 13 Noninterference 14 "Access.ExampleSystem" 15begin 16 17text {* 18 Reads/Affects sets: 19 - NicA, NicB, NicD: reads all except T 20 affects {RM, R, NicA, NicB, NicD} 21 - NicC: reads all except T, affects self only 22 - R: reads all except T 23 affects {NicA, NicB, NicD, R, RM, NTFN3} 24 - RM: reads all except T 25 affects {SC, EP, RM, R, NicA, NicB, NicD, NTFN2} 26 - SC: reads all except T 27 affects {EP, SC, NicC, RM, R, NicA, NicB, NicD, NTFN1} 28 - EP: reads all except T 29 affects {EP, SC, NicC, RM, R, NicA, NicB, NicD} 30 - NTFN1: reads all except T, affects {NTFN1, SC, NicC} 31 - NTFN2: '' , affects {NTFN2, RM, R, NicA, NicB, NicD} 32 - NTFN3: '' , affects {NTFN3, R, NicB, NicD} 33 - T: reads T, affects all except EP 34*} 35 36subsection {* Definitions *} 37 38datatype SACLabels = 39 NicA | NicB | NicC | NicD 40 | R | RM | SC | EP 41 | T | NTFN1 | NTFN2 | NTFN3 42 43definition complete_AgentAuthGraph where 44 "complete_AgentAuthGraph g \<equiv> 45 g \<union> {(y,a,y) | a y. True} 46 \<union> {(x,a,y) | x a y. (x,Control,y) \<in> g } 47 \<union> {(x,a,y)|x a y. \<exists> z. (x,Control,z) \<in> g \<and> (z, Control,y) \<in> g} " 48declare complete_AgentAuthGraph_def [simp] 49 50abbreviation partition_label where 51 "partition_label l \<equiv> OrdinaryLabel l" 52 53definition SACGraph where 54 "SACGraph \<equiv> 55 { (partition_label R, Read, partition_label NicB), (partition_label R, Write, partition_label NicB), 56 (partition_label R, Read, partition_label NicD), (partition_label R, Write, partition_label NicD), 57 (partition_label SC, Read, partition_label NicC), (partition_label SC, Write, partition_label NicC), 58 (partition_label SC, SyncSend, partition_label EP), 59 (partition_label RM, Receive, partition_label EP), 60 (partition_label RM, Control, partition_label R), 61 (partition_label RM, Control, partition_label NicA), 62 (partition_label RM, Control, partition_label NicB), 63 (partition_label RM, Control, partition_label NicD), 64 (partition_label T, Notify, partition_label NTFN1), 65 (partition_label T, Notify, partition_label NTFN2), 66 (partition_label T, Notify, partition_label NTFN3), 67 (partition_label SC, Receive, partition_label NTFN1), 68 (partition_label RM, Receive, partition_label NTFN2), 69 (partition_label R, Receive, partition_label NTFN3) 70 }" 71declare SACGraph_def [simp] 72 73definition SACAuthGraph where 74 "SACAuthGraph = complete_AgentAuthGraph SACGraph" 75declare SACAuthGraph_def [simp] 76 77definition SACAllLabels where 78 "SACAllLabels \<equiv> {partition_label NicB, partition_label RM, partition_label R, partition_label NicA, partition_label NicD, partition_label EP, partition_label SC, partition_label NicC}" 79 80definition RMControls where 81 "RMControls = {partition_label RM, partition_label R, partition_label NicA, partition_label NicB, partition_label NicD}" 82declare RMControls_def [simp] 83 84lemma reads_all_rm_controlled_subjects : "\<lbrakk>partition_label RM \<in> subjectReads SACAuthGraph (partition_label x); l \<in> RMControls\<rbrakk> \<Longrightarrow> l \<in> subjectReads SACAuthGraph (partition_label x)" 85 apply (simp only:RMControls_def) 86 apply (erule insertE, rule_tac t="partition_label RM" in reads_read_thread_read_pages, simp, simp)+ 87 apply simp 88done 89 90lemma reads_ntfn3_via_r : "partition_label R \<in> subjectReads SACAuthGraph (partition_label x) \<Longrightarrow> partition_label NTFN3 \<in> subjectReads SACAuthGraph (partition_label x)" 91 apply (rule_tac ep="partition_label NTFN3" and t="partition_label R" and auth="Receive" and auth'="Notify" and a="partition_label T" in reads_read_queued_thread_read_ep) 92 apply simp_all 93done 94 95lemma reads_ntfn2_via_rm : "partition_label RM \<in> subjectReads SACAuthGraph (partition_label x) \<Longrightarrow> partition_label NTFN2 \<in> subjectReads SACAuthGraph (partition_label x)" 96 apply (rule_tac ep="partition_label NTFN2" and t="partition_label RM" and auth="Receive" and auth'="Notify" and a="partition_label T" in reads_read_queued_thread_read_ep) 97 apply simp_all 98done 99 100lemma reads_ntfn1_via_sc : "partition_label SC \<in> subjectReads SACAuthGraph (partition_label x) \<Longrightarrow> partition_label NTFN1 \<in> subjectReads SACAuthGraph (partition_label x)" 101 apply (rule_tac ep="partition_label NTFN1" and t="partition_label SC" and auth="Receive" and auth'="Notify" and a="partition_label T" in reads_read_queued_thread_read_ep) 102 apply simp_all 103done 104 105subsection {* NicA, NicB, NicD reads/affects *} 106 107lemma reads_Control_rev': 108 "(x,Control,y) \<in> aag \<Longrightarrow> 109 x \<in> subjectReads (complete_AgentAuthGraph aag) y" 110 apply(rule reads_read_page_read_thread) 111 apply(rule reads_lrefl) 112 apply simp 113 done 114 115lemma reads_Control_rev: 116 "(x,Control,y) \<in> SACGraph \<Longrightarrow> 117 x \<in> subjectReads SACAuthGraph y" 118 apply(subst SACAuthGraph_def) 119 apply(erule reads_Control_rev') 120 done 121 122 123lemma abdrm_reads_ep : "x \<in> {NicA, NicB, NicD, RM} \<Longrightarrow> partition_label EP \<in> subjectReads SACAuthGraph (partition_label x)" 124 apply (rule_tac t = "partition_label RM" and a = "partition_label SC" and auth' = "SyncSend" and auth = "Receive" in reads_read_queued_thread_read_ep) 125 apply (simp+)[4] 126 apply safe 127 apply(fastforce intro: reads_Control_rev simp del: complete_AgentAuthGraph_def) 128 apply(fastforce intro: reads_Control_rev simp del: complete_AgentAuthGraph_def) 129 apply(fastforce intro: reads_Control_rev simp del: complete_AgentAuthGraph_def) 130 apply(rule reads_lrefl) 131 done 132 133lemma abdrm_reads_sc : "x \<in> {NicA, NicB, NicD, RM} \<Longrightarrow> partition_label SC \<in> subjectReads SACAuthGraph (partition_label x)" 134 apply (rule_tac auth = "Receive" and b = "partition_label SC" and a = "partition_label RM" and ep = "partition_label EP" in read_sync_ep_read_senders) 135 apply (simp, simp, simp del: SACAuthGraph_def add: abdrm_reads_ep, simp) 136done 137 138lemma abd_reads_rm : "x \<in> {NicA, NicB, NicD} \<Longrightarrow> partition_label RM \<in> subjectReads SACAuthGraph (partition_label x)" 139 apply (rule reads_Control_rev) 140 apply auto 141done 142 143lemma abd_reads_c : "x \<in> {NicA, NicB, NicD} \<Longrightarrow> partition_label NicC \<in> subjectReads SACAuthGraph (partition_label x)" 144 apply (rule_tac t = "partition_label SC" in reads_read_thread_read_pages) 145 apply (rule abdrm_reads_sc, simp, blast, simp) 146done 147 148lemma abd_reads_r : "x \<in> {NicA, NicB, NicD} \<Longrightarrow> partition_label R \<in> subjectReads SACAuthGraph (partition_label x)" 149 apply (rule_tac p="partition_label R" and t="partition_label RM" in reads_read_thread_read_pages) 150 apply (rule abd_reads_rm, simp, simp) 151done 152 153lemma abd_reads_ntfn3 : "x \<in> {NicA, NicB, NicD} \<Longrightarrow> partition_label NTFN3 \<in> subjectReads SACAuthGraph (partition_label x)" 154 apply (rule_tac ep="partition_label NTFN3" and t="partition_label R" and auth="Receive" and auth'="Notify" and a="partition_label T" in reads_read_queued_thread_read_ep) 155 apply (simp_all add: abd_reads_r del:SACAuthGraph_def, simp_all) 156done 157 158lemma abd_reads_all_bw : "x \<in> {NicA, NicB, NicD} \<Longrightarrow> {partition_label NicB, partition_label RM, partition_label R, partition_label NicA, partition_label NicD, partition_label EP, partition_label SC, partition_label NicC, partition_label NTFN1, partition_label NTFN2, partition_label NTFN3} \<subseteq> subjectReads SACAuthGraph (partition_label x)" 159 apply (rule subsetI) 160 (* refl cases *) 161 apply (case_tac "partition_label x = xa") 162 apply (simp add: reads_lrefl) 163 (* non refl cases *) 164 apply (case_tac "xa \<in> RMControls") 165 apply (rule reads_all_rm_controlled_subjects, rule abd_reads_rm, simp, simp) 166 apply (erule_tac a = xa in insertE, simp) 167 apply (erule_tac a = xa in insertE, simp only:, rule abd_reads_rm, simp) 168 apply (erule_tac a = xa in insertE, simp) 169 apply (erule_tac a = xa in insertE, simp) 170 apply (erule_tac a = xa in insertE, simp) 171 apply (erule_tac a = xa in insertE, simp only:, rule abdrm_reads_ep, simp, blast) 172 apply (erule_tac a = xa in insertE, simp only:, rule abdrm_reads_sc, simp, blast) 173 apply (erule_tac a = xa in insertE, simp only:, rule abd_reads_c, simp) 174 apply (erule_tac a = xa in insertE, simp only:, rule reads_ntfn1_via_sc, rule abdrm_reads_sc, simp, blast) 175 apply (erule_tac a = xa in insertE, simp only:, rule reads_ntfn2_via_rm, rule abd_reads_rm, simp) 176 apply (erule_tac a = xa in insertE, simp only:, rule reads_ntfn3_via_r, rule abd_reads_r, simp) 177 apply simp 178done 179 180lemma abd_reads : "x \<in> {NicA, NicB, NicD} \<Longrightarrow> subjectReads SACAuthGraph (partition_label x) = {partition_label NicB, partition_label RM, partition_label R, partition_label NicA, partition_label NicD, partition_label EP, partition_label SC, partition_label NicC, partition_label NTFN1, partition_label NTFN2, partition_label NTFN3}" 181 apply (rule subset_antisym) 182 defer 183 apply (rule abd_reads_all_bw) 184 apply (simp) 185 apply (rule subsetI) 186 apply (erule subjectReads.induct) 187 (* warning: slow *) 188 by (simp, blast?)+ 189 190 191definition abd_affects_set where 192 "abd_affects_set \<equiv> {NicB, RM, R, NicA, NicD, 193 EP, NTFN2}" (* these two added for NTFN binding *) 194declare abd_affects_set_def[simp] 195 196lemma abd_affects_bw : "x \<in> {NicA, NicB, NicD} \<Longrightarrow> partition_label ` abd_affects_set \<subseteq> subjectAffects SACAuthGraph (partition_label x)" 197 apply (simp only:abd_affects_set_def) 198 apply (rule subsetI) 199 (* refl cases *) 200 apply (case_tac "partition_label x = xa") 201 apply (simp add: affects_lrefl) 202 (* non-refl cases *) 203 apply (simp only: image_insert) 204 apply (erule_tac a = xa in insertE) 205 apply (rule_tac auth = SyncSend and ep = "partition_label x" and l' = "partition_label RM" in affects_send) 206 apply (simp, simp, simp, simp) 207 apply (erule_tac a = xa in insertE) 208 apply (simp only:) 209 apply (rule_tac ep = "partition_label x" and l' = "partition_label RM" in affects_recv) 210 apply (simp) 211 apply (auto)[1] 212 apply (erule_tac a = xa in insertE) 213 apply (simp only:) 214 apply (rule_tac auth = SyncSend and ep = "partition_label x" and l' = "partition_label RM" in affects_send) 215 apply (simp, simp, simp, simp) 216 apply (erule_tac a = xa in insertE) 217 apply (simp only:) 218 apply (clarify) 219 apply (erule notE) 220 apply (rule_tac auth = SyncSend and ep = "partition_label x" and l' = "partition_label RM" in affects_send) 221 apply (simp, simp, simp, simp) 222 apply (erule_tac a = xa in insertE) 223 apply (rule_tac auth = SyncSend and ep = "partition_label x" and l' = "partition_label RM" in affects_send) 224 apply (simp, simp, simp, simp) 225 apply (erule_tac a = xa in insertE) 226 apply (rule_tac ep = "xa" and l = "partition_label x" in affects_ep_bound_trans) 227 apply (rule_tac x = "partition_label RM" in exI) 228 apply (rule_tac x = "partition_label x" in exI) 229 apply (intro conjI) 230 apply (simp,simp,simp) 231 apply (erule_tac a = xa in insertE) 232 apply (rule_tac ep = "xa" and l = "partition_label x" in affects_ep_bound_trans) 233 apply (rule_tac x = "partition_label RM" in exI) 234 apply (rule_tac x = "partition_label x" in exI) 235 apply (intro conjI) 236 apply (simp,simp,simp,simp) 237 done 238 239lemma abd_affects : "x \<in> {NicA, NicB, NicD} \<Longrightarrow> subjectAffects SACAuthGraph (partition_label x) = partition_label ` abd_affects_set" 240 apply (rule subset_antisym) 241 defer 242 apply (rule abd_affects_bw) 243 apply (simp) 244 apply (rule subsetI) 245 apply (erule subjectAffects.induct) 246 by auto 247 248subsection {* NicC reads/affects *} 249 250lemma c_reads_sc : "partition_label SC \<in> subjectReads SACAuthGraph (partition_label NicC)" 251 apply (rule_tac b = "partition_label NicC" in reads_read_page_read_thread) 252 apply (rule reads_lrefl) 253 apply (simp) 254done 255 256lemma c_reads_ep : "partition_label EP \<in> subjectReads SACAuthGraph (partition_label NicC)" 257 apply (rule_tac a = "partition_label EP" and ep = "partition_label EP" and t = "partition_label SC" and auth = "SyncSend" and auth' = "Reset" in reads_read_queued_thread_read_ep) 258 apply (simp,simp,simp,simp) 259 apply (rule c_reads_sc) 260done 261 262lemma c_reads_rm : "partition_label RM \<in> subjectReads SACAuthGraph (partition_label NicC)" 263 apply (rule_tac auth = SyncSend and a = "partition_label SC" and ep = "partition_label EP" in read_sync_ep_read_receivers) 264 apply (simp, simp) 265 apply (rule c_reads_ep) 266 apply (simp) 267done 268 269lemma c_reads_any_controlled_by_rm : "x \<in> {partition_label R, partition_label NicA, partition_label NicB, partition_label NicD} \<Longrightarrow> x \<in> subjectReads SACAuthGraph (partition_label NicC)" 270 apply (rule_tac t = "partition_label RM" in reads_read_thread_read_pages) 271 apply (rule c_reads_rm) 272 apply auto 273done 274 275lemma c_reads : "subjectReads SACAuthGraph (partition_label NicC) = {partition_label NicB, partition_label RM, partition_label R, partition_label NicA, partition_label NicD, partition_label EP, partition_label SC, partition_label NicC, partition_label NTFN1, partition_label NTFN2, partition_label NTFN3}" 276 apply (rule subset_antisym) 277 defer 278 (* backward *) 279 apply (rule subsetI) 280 apply (case_tac "x \<in> {partition_label R, partition_label NicA, partition_label NicB, partition_label NicD}") 281 apply (rule c_reads_any_controlled_by_rm, assumption) 282 apply (erule insertE, simp) 283 apply (erule insertE, simp only:, rule c_reads_rm) 284 apply (erule insertE, simp, erule insertE, simp, erule insertE, simp) 285 apply (erule insertE, simp only:, rule c_reads_ep) 286 apply (erule insertE, simp only:, rule c_reads_sc) 287 apply (erule insertE, simp only:, rule reads_lrefl) 288 apply (erule insertE, simp only:, rule reads_ntfn1_via_sc, rule c_reads_sc) 289 apply (erule insertE, simp only:, rule reads_ntfn2_via_rm, rule c_reads_rm) 290 apply (erule insertE, simp only:, rule reads_ntfn3_via_r, rule c_reads_any_controlled_by_rm, simp) 291 apply simp 292 (* forward *) 293 apply (rule subsetI) 294 apply (erule subjectReads.induct) 295 by (simp, blast?)+ 296 297lemma c_affects_self_only : "x \<in> {partition_label NicC} \<Longrightarrow> x \<in> subjectAffects SACAuthGraph (partition_label NicC)" 298 apply (erule insertE) 299 apply (simp only:, rule affects_lrefl) 300 apply simp 301done 302 303lemma c_affects : "subjectAffects SACAuthGraph (partition_label NicC) = {partition_label NicC}" 304 apply (rule subset_antisym) 305 defer 306 (* backward *) 307 apply (rule subsetI) 308 apply (rule c_affects_self_only, assumption) 309 (* forward *) 310 apply (rule subsetI) 311 apply (erule subjectAffects.induct) 312 by (simp, blast?)+ 313 314subsection {* R reads/affects *} 315 316lemma r_reads_bd : "x \<in> {partition_label NicB, partition_label NicD} \<Longrightarrow> x \<in> subjectReads SACAuthGraph (partition_label R)" 317 apply (rule reads_read) 318 apply auto 319done 320 321lemma r_reads_ep : "partition_label EP \<in> subjectReads SACAuthGraph (partition_label R)" 322 apply (rule_tac a="partition_label SC" and auth'="SyncSend" and ep="partition_label EP" and t="partition_label RM" and auth="Receive" in reads_read_queued_thread_read_ep) 323 apply (simp, simp, simp, simp, rule reads_Control_rev, simp) 324done 325 326lemma r_reads_sc : "partition_label SC \<in> subjectReads SACAuthGraph (partition_label R)" 327 apply (rule_tac a="partition_label RM" and auth="Receive" and ep="partition_label EP" and b="partition_label SC" in read_sync_ep_read_senders) 328 apply (simp, simp, rule r_reads_ep, simp) 329done 330 331lemma r_reads_a : "partition_label NicA \<in> subjectReads SACAuthGraph (partition_label R)" 332 apply (rule_tac a="partition_label NicA" and auth'="Reset" and ep="partition_label NicA" and t="partition_label RM" and auth="Receive" in reads_read_queued_thread_read_ep) 333 apply (simp_all add:reads_Control_rev[simplified]) 334done 335 336lemma r_reads_c : "partition_label NicC \<in> subjectReads SACAuthGraph (partition_label R)" 337 apply (rule_tac t="partition_label SC" in reads_read_thread_read_pages) 338 apply (rule r_reads_sc, simp) 339done 340 341lemma r_reads : "subjectReads SACAuthGraph (partition_label R) = {partition_label NicB, partition_label RM, partition_label R, partition_label NicA, partition_label NicD, partition_label EP, partition_label SC, partition_label NicC, partition_label NTFN1, partition_label NTFN2, partition_label NTFN3}" 342 apply (rule subset_antisym) 343 defer 344 (* backward *) 345 apply (rule subsetI) 346 apply (erule insertE, rule r_reads_bd, simp) 347 apply (erule insertE, rule reads_Control_rev, simp) 348 apply (erule insertE, simp only:, rule reads_lrefl) 349 apply (erule insertE, simp only:, rule r_reads_a) 350 apply (erule insertE, rule r_reads_bd, simp) 351 apply (erule insertE, simp only:, rule r_reads_ep) 352 apply (erule insertE, simp only:, rule r_reads_sc) 353 apply (erule insertE, simp only:, rule r_reads_c) 354 apply (erule insertE, simp only:, rule reads_ntfn1_via_sc, rule r_reads_sc) 355 apply (erule insertE, simp only:, rule reads_ntfn2_via_rm, rule reads_Control_rev, simp) 356 apply (erule insertE, simp only:, rule reads_ntfn3_via_r, rule reads_lrefl) 357 apply simp 358 (* forward *) 359 apply (rule subsetI) 360 apply (erule subjectReads.induct) 361 by (simp, blast?)+ 362 363lemma r_affects_bd : "x \<in> {partition_label NicB, partition_label NicD} \<Longrightarrow> x \<in> subjectAffects SACAuthGraph (partition_label R)" 364 apply (rule_tac auth="Write" in affects_write) 365 apply auto 366done 367 368lemma r_affects_rm : "partition_label RM \<in> subjectAffects SACAuthGraph (partition_label R)" 369 apply (rule_tac l="partition_label R" and ep="partition_label R" in affects_recv) 370 apply simp_all 371done 372 373lemma r_affects_a : "partition_label NicA \<in> subjectAffects SACAuthGraph (partition_label R)" 374 apply (rule_tac l="partition_label R" and ep="partition_label R" and l'="partition_label RM" and auth="Receive" in affects_reset) 375 apply auto 376done 377 378lemma r_affects_ntfn3 : "partition_label NTFN3 \<in> subjectAffects SACAuthGraph (partition_label R)" 379 apply (rule_tac l="partition_label R" and auth="Receive" in affects_ep) 380 apply simp_all 381done 382 383lemma r_affects_ntfn2 : "partition_label NTFN2 \<in> subjectAffects SACAuthGraph (partition_label R)" 384 apply (rule_tac l="partition_label R" in affects_ep_bound_trans) 385 by auto 386 387lemma r_affects_ep : "partition_label EP \<in> subjectAffects SACAuthGraph (partition_label R)" 388 apply (rule_tac l="partition_label R" in affects_ep_bound_trans) 389 by auto 390 391lemma r_affects : "subjectAffects SACAuthGraph (partition_label R) = 392 {partition_label NicB, partition_label NicD, partition_label R, 393 partition_label RM, partition_label NicA, partition_label NTFN3, 394 partition_label EP, partition_label NTFN2 (* these 2 added for NTFN binding *) }" 395 apply (rule subset_antisym) 396 defer 397 (* backward *) 398 apply (rule subsetI) 399 apply (erule insertE, rule r_affects_bd, simp) 400 apply (erule insertE, rule r_affects_bd, simp) 401 apply (erule insertE, simp only:, rule affects_lrefl) 402 apply (erule insertE, simp only:, rule r_affects_rm) 403 apply (erule insertE, simp only:, rule r_affects_a) 404 apply (erule insertE, simp only:, rule r_affects_ntfn3) 405 apply (erule insertE, simp only:, rule r_affects_ep) 406 apply (erule insertE, simp only:, rule r_affects_ntfn2) 407 apply simp 408 (* forward *) 409 apply (rule subsetI) 410 apply (erule subjectAffects.induct) 411 by (simp, blast?)+ 412 413subsection {* RM reads/affects *} 414 415lemma rm_reads_sc : "partition_label SC \<in> subjectReads SACAuthGraph (partition_label RM)" 416 apply (rule_tac a="partition_label RM" and auth="Receive" and ep="partition_label EP" in read_sync_ep_read_senders) 417 apply (simp_all add:reads_ep) 418done 419 420lemma rm_reads_c : "partition_label NicC \<in> subjectReads SACAuthGraph (partition_label RM)" 421 apply (rule_tac t="partition_label SC" in reads_read_thread_read_pages) 422 apply (rule rm_reads_sc, simp) 423done 424 425lemma rm_reads : "subjectReads SACAuthGraph (partition_label RM) = {partition_label NicB, partition_label RM, partition_label R, partition_label NicA, partition_label NicD, partition_label EP, partition_label SC, partition_label NicC, partition_label NTFN1, partition_label NTFN2, partition_label NTFN3}" 426 apply (rule subset_antisym) 427 defer 428 (* backward *) 429 apply (rule subsetI) 430 apply (erule insertE, simp only:, rule reads_read, simp) 431 apply (erule insertE, simp only:, rule reads_lrefl) 432 apply (erule insertE, simp only:, rule reads_read, simp) 433 apply (erule insertE, simp only:, rule reads_read, simp) 434 apply (erule insertE, simp only:, rule reads_read, simp) 435 apply (erule insertE, simp only:, rule reads_ep, simp, simp) 436 apply (erule insertE, simp only:, rule rm_reads_sc) 437 apply (erule insertE, simp only:, rule rm_reads_c) 438 apply (erule insertE, simp only:, rule reads_ntfn1_via_sc, rule rm_reads_sc) 439 apply (erule insertE, simp only:, rule reads_ntfn2_via_rm, rule reads_lrefl) 440 apply (erule insertE, simp only:, rule reads_ntfn3_via_r, rule reads_read, simp) 441 apply simp 442 (* forward *) 443 apply (rule subsetI) 444 apply (erule subjectReads.induct) 445 by (simp, blast?)+ 446 447lemma rm_affects_via_control : "x \<in> {partition_label R, partition_label NicA, partition_label NicB, partition_label NicD} \<Longrightarrow> x \<in> subjectAffects SACAuthGraph (partition_label RM)" 448 apply (rule_tac l="partition_label RM" and auth="Control" in affects_write) 449 apply (simp, simp) 450done 451 452lemma rm_affects_ep : "partition_label EP \<in> subjectAffects SACAuthGraph (partition_label RM)" 453 apply (rule_tac auth="Receive" in affects_ep) 454 apply simp_all 455done 456 457lemma rm_affects_sc : "partition_label SC \<in> subjectAffects SACAuthGraph (partition_label RM)" 458 apply (rule_tac l="partition_label RM" and ep="partition_label EP" in affects_recv) 459 apply simp_all 460done 461 462lemma rm_affects_ntfn2 : "partition_label NTFN2 \<in> subjectAffects SACAuthGraph (partition_label RM)" 463 apply (rule_tac l="partition_label RM" and auth="Receive" in affects_ep) 464 apply simp_all 465done 466 467lemma rm_affects_ntfn3 : "partition_label NTFN3 \<in> subjectAffects SACAuthGraph (partition_label RM)" 468 apply (rule_tac l="partition_label RM" in affects_ep_bound_trans) 469 apply clarsimp 470 by auto 471 472 473lemma rm_affects : "subjectAffects SACAuthGraph (partition_label RM) = 474 {partition_label NicA, partition_label NicB, partition_label NicD, 475 partition_label R, partition_label SC, partition_label EP, 476 partition_label RM, partition_label NTFN2, 477 partition_label NTFN3 (* added for NTFN binding *)}" 478 apply (rule subset_antisym) 479 defer 480 (* backward *) 481 apply (rule subsetI) 482 apply (erule insertE, simp only:, rule rm_affects_via_control, simp) 483 apply (erule insertE, simp only:, rule rm_affects_via_control, simp) 484 apply (erule insertE, simp only:, rule rm_affects_via_control, simp) 485 apply (erule insertE, simp only:, rule rm_affects_via_control, simp) 486 apply (erule insertE, simp only:, rule rm_affects_sc) 487 apply (erule insertE, simp only:, rule rm_affects_ep) 488 apply (erule insertE, simp only:, rule affects_lrefl) 489 apply (erule insertE, simp only:, rule rm_affects_ntfn2) 490 apply (erule insertE, simp only:, rule rm_affects_ntfn3) 491 apply simp 492 (* forward *) 493 apply (rule subsetI) 494 apply (erule subjectAffects.induct) 495 by (simp, blast?)+ 496 497subsection {* SC *} 498 499lemma sc_reads_rm : "partition_label RM \<in> subjectReads SACAuthGraph (partition_label SC)" 500 apply (rule_tac a="partition_label SC" and ep="partition_label EP" and auth="SyncSend" and b="partition_label RM" in read_sync_ep_read_receivers) 501 apply (simp_all add:reads_ep) 502done 503 504lemma sc_reads : "subjectReads SACAuthGraph (partition_label SC) = {partition_label NicB, partition_label RM, partition_label R, partition_label NicA, partition_label NicD, partition_label EP, partition_label SC, partition_label NicC, partition_label NTFN1, partition_label NTFN2, partition_label NTFN3}" 505 apply (rule subset_antisym) 506 defer 507 (* backward *) 508 apply (rule subsetI) 509 apply (erule insertE, rule reads_all_rm_controlled_subjects, rule sc_reads_rm, simp) 510apply (erule insertE, rule reads_all_rm_controlled_subjects, rule sc_reads_rm, simp) 511apply (erule insertE, rule reads_all_rm_controlled_subjects, rule sc_reads_rm, simp) 512apply (erule insertE, rule reads_all_rm_controlled_subjects, rule sc_reads_rm, simp) 513apply (erule insertE, rule reads_all_rm_controlled_subjects, rule sc_reads_rm, simp) 514 apply (erule insertE, simp only:, rule_tac auth="SyncSend" in reads_ep, simp, simp) 515 apply (erule insertE, simp only:, rule reads_lrefl) 516 apply (erule insertE, simp only:, rule reads_read, simp) 517 apply (erule insertE, simp only:, rule reads_ntfn1_via_sc, rule reads_lrefl) 518 apply (erule insertE, simp only:, rule reads_ntfn2_via_rm, rule sc_reads_rm) 519 apply (erule insertE, simp only:, rule reads_ntfn3_via_r, rule reads_all_rm_controlled_subjects, rule sc_reads_rm, simp) 520 apply simp 521 (* forward *) 522 apply (rule subsetI) 523 apply (erule subjectReads.induct) 524 apply (simp, blast?)+ 525done 526 527lemma sc_affects_all_rm_controls : "l \<in> RMControls \<Longrightarrow> l \<in> subjectAffects SACAuthGraph (partition_label SC)" 528 apply (simp only:RMControls_def) 529 apply (erule insertE, rule_tac l="partition_label SC" and auth="SyncSend" and ep="partition_label EP" and l'="partition_label RM" in affects_send, simp, simp, simp, simp)+ 530 apply simp 531done 532 533lemma sc_affects : "subjectAffects SACAuthGraph (partition_label SC) = {partition_label NicB, partition_label RM, partition_label R, partition_label NicA, partition_label NicD, partition_label EP, partition_label SC, partition_label NicC, partition_label NTFN1}" 534 apply (rule subset_antisym) 535 defer 536 (* backward *) 537 apply (rule subsetI) 538 apply (erule insertE, rule sc_affects_all_rm_controls, simp) 539 apply (erule insertE, rule sc_affects_all_rm_controls, simp) 540 apply (erule insertE, rule sc_affects_all_rm_controls, simp) 541 apply (erule insertE, rule sc_affects_all_rm_controls, simp) 542 apply (erule insertE, rule sc_affects_all_rm_controls, simp) 543 apply (erule insertE, simp only:, rule_tac l="partition_label SC" and auth="SyncSend" in affects_ep, simp, simp) 544 apply (erule insertE, simp only:, rule affects_lrefl) 545 apply (erule insertE, simp only:, rule_tac l="partition_label SC" and auth="Write" in affects_write, simp, simp) 546 apply (erule insertE, simp only:, rule_tac l="partition_label SC" and auth="Receive" in affects_ep, simp, simp) 547 apply simp 548 (* forward *) 549 apply (rule subsetI) 550 apply (erule subjectAffects.induct) 551 apply (simp, blast?)+ 552done 553 554subsection {* EP *} 555 556lemma ep_reads_sc : "partition_label SC \<in> subjectReads SACAuthGraph (partition_label EP)" 557 apply (rule_tac a="partition_label EP" and ep="partition_label EP" and auth="Receive" in read_sync_ep_read_senders) 558 apply (simp, simp, rule reads_lrefl, simp_all) 559done 560 561lemma ep_reads_rm : "partition_label RM \<in> subjectReads SACAuthGraph (partition_label EP)" 562 apply (rule_tac a="partition_label SC" and ep="partition_label EP" and b="partition_label RM" and auth="SyncSend" in read_sync_ep_read_receivers) 563 apply (simp, simp, rule reads_lrefl, simp) 564done 565 566lemma ep_reads_c : "partition_label NicC \<in> subjectReads SACAuthGraph (partition_label EP)" 567 apply (rule_tac t="partition_label SC" and p="partition_label NicC" in reads_read_thread_read_pages) 568 apply (rule ep_reads_sc, simp) 569done 570 571lemma ep_reads : "subjectReads SACAuthGraph (partition_label EP) = {partition_label NicB, partition_label RM, partition_label R, partition_label NicA, partition_label NicD, partition_label EP, partition_label SC, partition_label NicC, partition_label NTFN1, partition_label NTFN2, partition_label NTFN3}" 572 apply (rule subset_antisym) 573 defer 574 (* backward *) 575 apply (rule subsetI) 576 apply (erule insertE, rule reads_all_rm_controlled_subjects, rule ep_reads_rm, simp) 577 apply (erule insertE, simp only:, rule ep_reads_rm) 578 apply (erule insertE, rule reads_all_rm_controlled_subjects, rule ep_reads_rm, simp) 579 apply (erule insertE, rule reads_all_rm_controlled_subjects, rule ep_reads_rm, simp) 580 apply (erule insertE, rule reads_all_rm_controlled_subjects, rule ep_reads_rm, simp) 581 apply (erule insertE, simp only:, rule reads_lrefl) 582 apply (erule insertE, simp only:, rule ep_reads_sc) 583 apply (erule insertE, simp only:, rule ep_reads_c) 584 apply (erule insertE, simp only:, rule reads_ntfn1_via_sc, rule ep_reads_sc) 585 apply (erule insertE, simp only:, rule reads_ntfn2_via_rm, rule ep_reads_rm) 586 apply (erule insertE, simp only:, rule reads_ntfn3_via_r, rule reads_all_rm_controlled_subjects, rule ep_reads_rm, simp) 587 apply simp 588 (* forward *) 589 apply (rule subsetI) 590 apply (erule subjectReads.induct) 591 apply (simp, blast?)+ 592done 593 594lemma ep_affects_sc : "partition_label SC \<in> subjectAffects SACAuthGraph (partition_label EP)" 595 apply (rule_tac l="partition_label EP" and ep="partition_label EP" in affects_recv) 596 apply simp_all 597done 598 599lemma ep_affects_c : "partition_label NicC \<in> subjectAffects SACAuthGraph (partition_label EP)" 600 apply (rule_tac l="partition_label EP" and l'="partition_label SC" and auth="SyncSend" and ep="partition_label EP" in affects_reset) 601 apply simp_all 602done 603 604lemma ep_affects_ntfn2 : "partition_label NTFN2 \<in> subjectAffects SACAuthGraph (partition_label EP)" 605 apply (rule_tac ep="partition_label NTFN2" in affects_ep_bound_trans) 606 by auto 607 608lemma ep_affects_rm_controls : "x \<in> RMControls \<Longrightarrow> x \<in> subjectAffects SACAuthGraph (partition_label EP)" 609 apply (rule_tac l="partition_label EP" and ep="partition_label EP" and auth="SyncSend" and l'="partition_label RM" in affects_send) 610 apply (simp_all) 611done 612 613lemma ep_affects: "subjectAffects SACAuthGraph (partition_label EP) = {partition_label EP, partition_label SC, partition_label NicC, partition_label NTFN2} \<union> RMControls" 614 apply (rule subset_antisym) 615 defer 616 (* backward *) 617 apply (rule subsetI) 618 apply (erule UnE) 619 apply (erule insertE, simp only:, rule affects_lrefl) 620 apply (erule insertE, simp only:, rule ep_affects_sc) 621 apply (erule insertE, simp only:, rule ep_affects_c) 622 apply (erule insertE, simp only:, rule ep_affects_ntfn2) 623 apply simp 624 apply (rule ep_affects_rm_controls, simp) 625 (* forward *) 626 apply (rule subsetI) 627 apply (erule subjectAffects.induct) 628 by (simp, blast?)+ 629 630subsection {* NTFN1,2,3 *} 631 632subsubsection {* NTFN1 reads SC, EP, RM, R*} 633 634lemma ntfn1_reads_sc : "partition_label SC \<in> subjectReads SACAuthGraph (partition_label NTFN1)" 635 apply (rule_tac ep="partition_label NTFN1" and auth="SyncSend" and a="partition_label NTFN1" in read_sync_ep_read_receivers) 636 apply (simp, simp, rule reads_lrefl, simp) 637done 638 639lemma ntfn1_reads_ep : "partition_label EP \<in> subjectReads SACAuthGraph (partition_label NTFN1)" 640 apply (rule_tac ep="partition_label EP" and auth="SyncSend" and t="partition_label SC" and auth'="Reset" and a="partition_label EP" in reads_read_queued_thread_read_ep) 641 apply (simp, simp, simp, simp, rule ntfn1_reads_sc) 642done 643 644lemma ntfn1_reads_rm : "partition_label RM \<in> subjectReads SACAuthGraph (partition_label NTFN1)" 645 apply (rule_tac b="partition_label RM" and ep="partition_label EP" and auth="SyncSend" and a="partition_label SC" in read_sync_ep_read_receivers) 646 apply (simp, simp, rule ntfn1_reads_ep, simp) 647done 648 649subsubsection {* NTFN2 reads SC, EP, RM, R *} 650 651lemma ntfn2_reads_rm : "partition_label RM \<in> subjectReads SACAuthGraph (partition_label NTFN2)" 652 apply (rule_tac ep="partition_label NTFN2" and auth="SyncSend" and a="partition_label NTFN2" in read_sync_ep_read_receivers) 653 apply (simp, simp, rule reads_lrefl, simp) 654done 655 656lemma ntfn2_reads_ep : "partition_label EP \<in> subjectReads SACAuthGraph (partition_label NTFN2)" 657 apply (rule_tac ep="partition_label EP" and auth="Receive" and t="partition_label RM" and auth'="Reset" and a="partition_label EP" in reads_read_queued_thread_read_ep) 658 apply (simp, simp, simp, simp, rule ntfn2_reads_rm) 659done 660 661lemma ntfn2_reads_sc : "partition_label SC \<in> subjectReads SACAuthGraph (partition_label NTFN2)" 662 apply (rule_tac b="partition_label SC" and ep="partition_label EP" and auth="Reset" and a="partition_label EP" in read_sync_ep_read_senders) 663 apply (simp, simp, rule ntfn2_reads_ep, simp) 664done 665 666subsubsection {* NTFN3 reads SC, EP, RM, R *} 667 668lemma ntfn3_reads_r : "partition_label R \<in> subjectReads SACAuthGraph (partition_label NTFN3)" 669 apply (rule_tac ep="partition_label NTFN3" and auth="SyncSend" and a="partition_label NTFN3" in read_sync_ep_read_receivers) 670 apply (simp, simp, rule reads_lrefl, simp) 671done 672 673lemma ntfn3_reads_rm : "partition_label RM \<in> subjectReads SACAuthGraph (partition_label NTFN3)" 674 apply (rule_tac b="partition_label R" in reads_read_page_read_thread) 675 apply (rule ntfn3_reads_r, simp) 676done 677 678lemma ntfn3_reads_ep : "partition_label EP \<in> subjectReads SACAuthGraph (partition_label NTFN3)" 679 apply (rule_tac t="partition_label RM" and auth="Receive" and auth'="SyncSend" and a="partition_label SC" in reads_read_queued_thread_read_ep) 680 apply (simp, simp, simp, simp, rule ntfn3_reads_rm) 681done 682 683lemma ntfn3_reads_sc : "partition_label SC \<in> subjectReads SACAuthGraph (partition_label NTFN3)" 684 apply (rule_tac ep="partition_label EP" and auth="Receive" and a="partition_label RM" in read_sync_ep_read_senders) 685 apply (simp, simp, rule ntfn3_reads_ep, simp) 686done 687 688subsubsection {* NTFN1,2,3 reads C *} 689 690lemma ntfn123_reads_c : "x \<in> {NTFN1, NTFN2, NTFN3} \<Longrightarrow> partition_label NicC \<in> subjectReads SACAuthGraph (partition_label x)" 691 apply (rule_tac t="partition_label SC" in reads_read_thread_read_pages) 692 apply (erule insertE, simp only:, rule ntfn1_reads_sc, erule insertE, simp only:, rule ntfn2_reads_sc, erule insertE, simp only:, rule ntfn3_reads_sc, simp) 693 apply simp 694done 695 696subsubsection {* NTFN1,2,3 reads each other *} 697 698lemma ntfn13_reads_ntfn2 : "l \<in> {NTFN1, NTFN3} \<Longrightarrow> partition_label NTFN2 \<in> subjectReads SACAuthGraph (partition_label l)" 699 apply (rule_tac t="partition_label RM" and auth="Receive" and auth'="Reset" and a="partition_label NTFN2" in reads_read_queued_thread_read_ep) 700 apply (simp, simp, simp, simp) 701 apply (erule insertE, simp only:, rule ntfn1_reads_rm, erule insertE, simp only:, rule ntfn3_reads_rm, simp) 702done 703 704lemma ntfn12_reads_ntfn3 : "l \<in> {NTFN1, NTFN2} \<Longrightarrow> partition_label NTFN3 \<in> subjectReads SACAuthGraph (partition_label l)" 705 apply (rule_tac t="partition_label R" and auth="Receive" and auth'="Reset" and a="partition_label NTFN3" in reads_read_queued_thread_read_ep) 706 apply (simp, simp, simp, simp) 707 apply (erule insertE, simp only:, rule reads_all_rm_controlled_subjects, rule ntfn1_reads_rm, simp, erule insertE, simp only:, rule reads_all_rm_controlled_subjects, rule ntfn2_reads_rm, simp_all) 708done 709 710lemma ntfn23_reads_ntfn1 : "l \<in> {NTFN2, NTFN3} \<Longrightarrow> partition_label NTFN1 \<in> subjectReads SACAuthGraph (partition_label l)" 711 apply (rule_tac t="partition_label SC" and auth="Receive" and auth'="Reset" and a="partition_label NTFN1" in reads_read_queued_thread_read_ep) 712 apply (simp, simp, simp, simp) 713 apply (erule insertE, simp only:, rule ntfn2_reads_sc, erule insertE, simp only:, rule ntfn3_reads_sc, simp) 714done 715 716subsubsection {* NTFN1,2,3 reads *} 717declare SACAuthGraph_def[simp del] 718 719lemma ntfn123_reads_rm : "l \<in> {NTFN1, NTFN2, NTFN3} \<Longrightarrow> partition_label RM \<in> subjectReads SACAuthGraph (partition_label l)" 720by (auto simp:ntfn1_reads_rm ntfn2_reads_rm ntfn3_reads_rm) 721 722lemma ntfn123_reads_sc : "l \<in> {NTFN1, NTFN2, NTFN3} \<Longrightarrow> partition_label SC \<in> subjectReads SACAuthGraph (partition_label l)" 723by (auto simp:ntfn1_reads_sc ntfn2_reads_sc ntfn3_reads_sc) 724 725lemma ntfn123_reads_ep : "l \<in> {NTFN1, NTFN2, NTFN3} \<Longrightarrow> partition_label EP \<in> subjectReads SACAuthGraph (partition_label l)" 726by (auto simp:ntfn1_reads_ep ntfn2_reads_ep ntfn3_reads_ep) 727 728lemma ntfn123_reads_ntfn123 : "\<lbrakk>l \<in> {NTFN1, NTFN2, NTFN3}; x \<in> {NTFN1, NTFN2, NTFN3}\<rbrakk> \<Longrightarrow> partition_label l \<in> subjectReads SACAuthGraph (partition_label x)" 729by (auto simp:ntfn12_reads_ntfn3 ntfn13_reads_ntfn2 ntfn23_reads_ntfn1 reads_lrefl) 730 731lemma ntfn123_reads : "l \<in> {NTFN1, NTFN2, NTFN3} \<Longrightarrow> subjectReads SACAuthGraph (partition_label l) = {partition_label NicB, partition_label RM, partition_label R, partition_label NicA, partition_label NicD, partition_label EP, partition_label SC, partition_label NicC, partition_label NTFN1, partition_label NTFN2, partition_label NTFN3}" 732 apply (rule subset_antisym) 733 defer 734 (* backward *) 735 apply (rule subsetI) 736 apply (erule_tac a=x in insertE, rule reads_all_rm_controlled_subjects, rule ntfn123_reads_rm, simp, simp) 737 apply (erule_tac a=x in insertE, simp only:, rule ntfn123_reads_rm, simp) 738 apply (erule_tac a=x in insertE, rule reads_all_rm_controlled_subjects, rule ntfn123_reads_rm, simp, simp) 739 apply (erule_tac a=x in insertE, rule reads_all_rm_controlled_subjects, rule ntfn123_reads_rm, simp, simp) 740 apply (erule_tac a=x in insertE, rule reads_all_rm_controlled_subjects, rule ntfn123_reads_rm, simp, simp) 741 apply (erule_tac a=x in insertE, simp only:, rule ntfn123_reads_ep, simp) 742 apply (erule_tac a=x in insertE, simp only:, rule ntfn123_reads_sc, simp) 743 apply (erule_tac a=x in insertE, simp only:, rule ntfn123_reads_c, simp) 744 apply (auto simp:ntfn123_reads_ntfn123)[1] 745 (* forward *) 746 apply (rule subsetI) 747 apply (erule subjectReads.induct) 748 by (simp add:SACAuthGraph_def, blast?)+ 749 750subsubsection {* NTFN1,2,3 affects *} 751 752lemma ntfn1_affects_sc : "partition_label SC \<in> subjectAffects SACAuthGraph (partition_label NTFN1)" 753 apply (rule_tac l''="partition_label SC" and l'="partition_label SC" and ep="partition_label NTFN1" and auth="Notify" and l="partition_label NTFN1" in affects_send) 754 apply (simp_all add:SACAuthGraph_def) 755done 756 757lemma ntfn1_affects_c : "partition_label NicC \<in> subjectAffects SACAuthGraph (partition_label NTFN1)" 758 apply (rule_tac l'="partition_label SC" and ep="partition_label NTFN1" and l="partition_label NTFN1" and auth="Notify" in affects_send) 759 apply (simp_all add:SACAuthGraph_def) 760done 761 762lemma ntfn1_affects : "subjectAffects SACAuthGraph (partition_label NTFN1) = {partition_label NTFN1, partition_label SC, partition_label NicC}" 763 apply (rule subset_antisym) 764 defer 765 (* backward *) 766 apply (rule subsetI) 767 apply (erule insertE, simp only:, rule affects_lrefl) 768 apply (erule insertE, simp only:, rule ntfn1_affects_sc) 769 apply (erule insertE, simp only:, rule ntfn1_affects_c) 770 apply simp 771 (* forward *) 772 apply (rule subsetI) 773 apply (erule subjectAffects.induct) 774 apply (simp add:SACAuthGraph_def, blast?)+ 775done 776 777lemma ntfn2_affects_rm : "partition_label RM \<in> subjectAffects SACAuthGraph (partition_label NTFN2)" 778 apply (rule_tac l'="partition_label RM" and ep="partition_label NTFN2" and auth="Notify" and l="partition_label NTFN2" in affects_send) 779 apply (simp_all add:SACAuthGraph_def) 780done 781 782lemma ntfn2_affects_ep : "partition_label EP \<in> subjectAffects SACAuthGraph (partition_label NTFN2)" 783 apply (rule affects_ep_bound_trans) 784 by (auto simp: SACAuthGraph_def) 785 786lemma ntfn2_affects_rm_controls : "x \<in> RMControls \<Longrightarrow> x \<in> subjectAffects SACAuthGraph (partition_label NTFN2)" 787 apply (rule_tac l="partition_label NTFN2" and ep="partition_label NTFN2" and auth="SyncSend" and l'="partition_label RM" in affects_send) 788 apply (simp_all add:SACAuthGraph_def) 789done 790 791lemma ntfn2_affects : "subjectAffects SACAuthGraph (partition_label NTFN2) = {partition_label NTFN2, partition_label RM, partition_label EP} \<union> RMControls" 792 apply (rule subset_antisym) 793 defer 794 (* backward *) 795 apply (rule subsetI) 796 apply (erule UnE) 797 apply (erule insertE, simp only:, rule affects_lrefl) 798 apply (erule insertE, simp only:, rule ntfn2_affects_rm) 799 apply (erule insertE, simp only:, rule ntfn2_affects_ep) 800 apply simp 801 apply (rule ntfn2_affects_rm_controls, simp) 802 (* forward *) 803 apply (rule subsetI) 804 apply (erule subjectAffects.induct) 805 by (simp add:SACAuthGraph_def, blast?)+ 806 807lemma ntfn3_affects_r : "partition_label R \<in> subjectAffects SACAuthGraph (partition_label NTFN3)" 808 apply (rule_tac l'="partition_label R" and ep="partition_label NTFN3" and auth="Notify" and l="partition_label NTFN3" in affects_send) 809 apply (simp_all add:SACAuthGraph_def) 810done 811 812lemma ntfn3_affects_bd : "l \<in> {NicB, NicD} \<Longrightarrow> partition_label l \<in> subjectAffects SACAuthGraph (partition_label NTFN3)" 813 apply (rule_tac l'="partition_label R" and ep="partition_label NTFN3" and l="partition_label NTFN3" and auth="Notify" in affects_send) 814 apply (simp add:SACAuthGraph_def, blast?)+ 815done 816 817lemma ntfn3_affects : "subjectAffects SACAuthGraph (partition_label NTFN3) = {partition_label NTFN3, partition_label R} \<union> {partition_label NicB, partition_label NicD}" 818 apply (rule subset_antisym) 819 defer 820 (* backward *) 821 apply (rule subsetI, erule UnE) 822 apply (erule insertE, simp only:, rule affects_lrefl) 823 apply (erule insertE, simp only:, rule ntfn3_affects_r, simp) 824 apply (auto simp:ntfn3_affects_bd)[1] 825 (* forward *) 826 apply (rule subsetI) 827 apply (erule subjectAffects.induct) 828 apply (simp add:SACAuthGraph_def, blast?)+ 829done 830 831subsection {* T *} 832 833lemma t_reads : "subjectReads SACAuthGraph (partition_label T) = {partition_label T}" 834 apply (rule subset_antisym) 835 defer 836 apply (rule subsetI, erule insertE, simp only:, rule reads_lrefl, simp) 837 apply (rule subsetI, erule subjectReads.induct) 838 apply (simp add:SACAuthGraph_def, blast?)+ 839done 840 841lemma t_affects_ntfn123 : "l \<in> {NTFN1, NTFN2, NTFN3} \<Longrightarrow> partition_label l \<in> subjectAffects SACAuthGraph (partition_label T)" 842 apply (rule_tac auth="Notify" in affects_ep) 843 apply (simp_all add:SACAuthGraph_def, blast) 844done 845 846lemma t_affects_sc : "partition_label SC \<in> subjectAffects SACAuthGraph (partition_label T)" 847 apply (rule_tac l''="partition_label SC" and l'="partition_label SC" and ep="partition_label NTFN1" and auth="Notify" and l="partition_label T" in affects_send) 848 apply (simp_all add:SACAuthGraph_def) 849done 850 851lemma t_affects_rm : "partition_label RM \<in> subjectAffects SACAuthGraph (partition_label T)" 852 apply (rule_tac l''="partition_label RM" and l'="partition_label RM" and ep="partition_label NTFN2" and auth="Notify" and l="partition_label T" in affects_send) 853 apply (simp_all add:SACAuthGraph_def) 854done 855 856lemma t_affects_r : "partition_label R \<in> subjectAffects SACAuthGraph (partition_label T)" 857 apply (rule_tac l''="partition_label R" and l'="partition_label R" and ep="partition_label NTFN3" and auth="Notify" and l="partition_label T" in affects_send) 858 apply (simp_all add:SACAuthGraph_def) 859done 860 861lemma t_affects_ep : "partition_label EP \<in> subjectAffects SACAuthGraph (partition_label T)" 862 apply (rule affects_ep_bound_trans) 863 by (auto simp: SACAuthGraph_def) 864 865lemma t_affects_c : "partition_label NicC \<in> subjectAffects SACAuthGraph (partition_label T)" 866 apply (rule_tac l''="partition_label NicC" and l'="partition_label SC" and ep="partition_label NTFN1" and auth="Notify" and l="partition_label T" in affects_send) 867 apply (simp_all add:SACAuthGraph_def) 868done 869 870lemma t_affects_a : "partition_label NicA \<in> subjectAffects SACAuthGraph (partition_label T)" 871 apply (rule_tac l''="partition_label NicA" and l'="partition_label RM" and ep="partition_label NTFN2" and auth="Notify" and l="partition_label T" in affects_send) 872 apply (simp_all add:SACAuthGraph_def) 873done 874 875lemma t_affects_bd : "l \<in> {NicB, NicD} \<Longrightarrow> partition_label l \<in> subjectAffects SACAuthGraph (partition_label T)" 876 apply (rule_tac l'="partition_label R" and ep="partition_label NTFN3" and auth="Notify" and l="partition_label T" in affects_send) 877 apply (simp_all add:SACAuthGraph_def, blast) 878done 879 880lemma t_affects : "subjectAffects SACAuthGraph (partition_label T) = {partition_label NTFN1, partition_label NTFN2, partition_label NTFN3} \<union> {partition_label T, partition_label SC, partition_label RM, partition_label R, partition_label NicA, partition_label NicB, partition_label NicD, partition_label NicC, partition_label EP}" 881 apply (rule subset_antisym) 882 defer 883 (* backward *) 884 apply (rule subsetI, erule UnE) 885 apply (auto simp:t_affects_ntfn123)[1] 886 apply (erule insertE, simp only:, rule affects_lrefl) 887 apply (erule insertE, simp only:, rule t_affects_sc) 888 apply (erule insertE, simp only:, rule t_affects_rm) 889 apply (erule insertE, simp only:, rule t_affects_r) 890 apply (erule insertE, simp only:, rule t_affects_a) 891 apply (erule insertE, simp only:, rule t_affects_bd, simp) 892 apply (erule insertE, simp only:, rule t_affects_bd, simp) 893 apply (erule insertE, simp only:, rule t_affects_c) 894 apply (erule insertE, simp only:, rule t_affects_ep) 895 apply simp 896 (* forward *) 897 apply (rule subsetI, erule subjectAffects.induct) 898 by (simp add:SACAuthGraph_def, blast?)+ 899 900subsection {* Policy *} 901 902lemmas SAC_reads = sc_reads ep_reads c_reads rm_reads r_reads abd_reads ntfn123_reads t_reads 903 904lemmas SAC_affects = sc_affects ep_affects c_affects rm_affects r_affects abd_affects ntfn1_affects ntfn2_affects ntfn3_affects t_affects 905 906definition SACFlowDoms where 907 "SACFlowDoms \<equiv> {Partition EP, Partition SC, Partition NicC, Partition RM, Partition R, Partition NicA, Partition NicB, Partition NicD, Partition NTFN1, Partition NTFN2, Partition NTFN3}" 908declare SACFlowDoms_def [simp] 909 910definition SACPolicyFlows :: "(SACLabels partition \<times> SACLabels partition) set" where 911 "SACPolicyFlows \<equiv> 912 {(PSched,d)| d. True} 913 \<union> {(Partition l, Partition k)| l k. (k = T \<longrightarrow> l = T)}" 914 915lemma SAC_partsSubjectAffects_exceptT : "x \<noteq> T \<Longrightarrow> partsSubjectAffects SACAuthGraph x = SACFlowDoms" 916 apply (rule equalityI) 917 defer 918 apply (rule subsetI) 919 apply (simp add:partsSubjectAffects_def image_def label_can_affect_partition_def) 920 apply (case_tac x) 921 apply ((erule disjE, clarify, simp add:SAC_affects SAC_reads, blast?)+, simp add:SAC_affects SAC_reads, blast?)+ 922 apply (rule subsetI) 923 apply (simp add:partsSubjectAffects_def image_def label_can_affect_partition_def) 924 apply (clarify) 925 apply (case_tac x) 926 apply (case_tac[!] xaa) 927 apply (auto simp: SAC_affects SAC_reads) 928done 929 930lemma SAC_partsSubjectAffects_T : "(partsSubjectAffects SACAuthGraph T) = {Partition NTFN1, Partition NTFN2, Partition NTFN3} \<union> {Partition T, Partition SC, Partition RM, Partition R, Partition NicA, Partition NicB, Partition NicD, Partition NicC, Partition EP}" 931 apply (rule equalityI) 932 apply (rule subsetI) 933 apply (simp add: partsSubjectAffects_def image_def label_can_affect_partition_def SAC_affects SAC_reads) 934 apply (clarify) 935 apply (case_tac xa, simp_all)[1] 936 apply (rule subsetI) 937 apply (simp add: partsSubjectAffects_def image_def label_can_affect_partition_def SAC_affects SAC_reads) 938 apply (erule disjE, simp add: SAC_reads) (* Do not collapse this in with a blast? because attempting blast takes too long *) 939 apply ((erule disjE)?, simp add: SAC_reads, blast)+ 940done 941 942lemma SAC_policyFlows : "policyFlows SACAuthGraph = SACPolicyFlows" 943 apply (rule subset_antisym) 944 (* forward *) 945 apply (rule subsetI) 946 apply clarify 947 apply (erule policyFlows.cases) 948 (* subject case *) 949 apply (clarsimp simp:SACPolicyFlows_def) 950 apply (case_tac "d = Partition T") 951 apply (case_tac l, auto simp:SAC_partsSubjectAffects_T SAC_partsSubjectAffects_exceptT)[1] 952 apply (case_tac l, auto simp:SAC_partsSubjectAffects_T SAC_partsSubjectAffects_exceptT)[1] 953 (* scheduler case *) 954 apply (simp add:SACPolicyFlows_def) 955 (* backward *) 956 apply (rule subsetI) 957 apply (clarsimp simp:SACPolicyFlows_def) 958 apply (erule disjE) 959 (* scheduler flows to all *) 960 apply (simp add:PSched_flows_to_all) 961 (* all subjects flow to all subjects *) 962 apply (clarify, simp) 963 apply (rule policy_affects) 964 apply (case_tac l, case_tac[1-12] k, auto simp:SAC_partsSubjectAffects_T SAC_partsSubjectAffects_exceptT) 965done 966 967end 968