1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 *) 6 7theory ExampleSystem 8imports Access 9begin 10 11context begin interpretation Arch . (*FIXME: arch_split*) 12 13definition 14 nat_to_bl :: "nat \<Rightarrow> nat \<Rightarrow> bool list option" 15where 16 "nat_to_bl bits n \<equiv> 17 if n \<ge> 2^bits then 18 None 19 else 20 Some $ bin_to_bl bits (of_nat n)" 21 22lemma nat_to_bl_id [simp]: "nat_to_bl (size (x :: (('a::len) word))) (unat x) = Some (to_bl x)" 23 apply (clarsimp simp: nat_to_bl_def to_bl_def) 24 apply (auto simp: uint_nat le_def word_size) 25 done 26 27 28(*---------------------------------------------------------*) 29 30subsection \<open>Purpose\<close> 31 32text \<open> 33 34This file defines some example systems using the access control 35definitions. The aim is a sanity check of the AC definitions, to 36ensure they enable to reason about reasonable systems. 37 38In particular, we want to make sure that 39 40 . the function state_objs_to_policy does not connect everything to 41 everything (Example 1) 42 . we can talk about components sharing cnodes 43 . we can talk about components sharing frames 44 . we can have more than 1 untrusted component 45 . we can have an EP between two untrusted components 46 47\<close> 48 49(*---------------------------------------------------------*) 50 51subsection \<open>Generic functions / lemmas\<close> 52 53 54text \<open>Defining the authority between labels. 55 56In addition to the intuitive authority we want, we need to add all the 57authority required to have a wellformed graph. So we define 58complete_AgentAuthGraph to add these 'extra' authorities (at least all 59the ones not depending on the current label). These are: 60 61 . self-authority (each label needs all the authorities to itself). 62 . if Control edge is present between 2 labels then we add all 63 authorities between them. 64 . Control authority is transitive: we add an Control edge 65 between 2 labels if we can connect them via Control 66 edges. Actually we add all authorities because of the second 67 clause. 68 69\<close> 70 71 72definition 73 complete_AuthGraph :: "'a auth_graph \<Rightarrow> 'a set \<Rightarrow> 'a auth_graph" 74where 75 "complete_AuthGraph g ls \<equiv> 76 g \<union> {(l,a,l) | a l. l \<in> ls}" 77 78text \<open>converting a nat to a bool list of size 10 - for the cnodes\<close> 79 80definition 81 the_nat_to_bl :: "nat \<Rightarrow> nat \<Rightarrow> bool list" 82where 83 "the_nat_to_bl sz n \<equiv> the (nat_to_bl sz n)" 84 85definition 86 the_nat_to_bl_10 :: "nat \<Rightarrow> bool list" 87where 88 "the_nat_to_bl_10 n \<equiv> the_nat_to_bl 10 n" 89 90lemma tcb_cnode_index_nat_to_bl: 91 "n<10 \<Longrightarrow> the_nat_to_bl_10 n \<noteq> tcb_cnode_index n" 92 by (clarsimp simp: the_nat_to_bl_10_def the_nat_to_bl_def 93 tcb_cnode_index_def 94 nat_to_bl_def to_bl_def bin_to_bl_aux_def) 95 96 97(*---------------------------------------------------------*) 98subsection \<open>Example 1\<close> 99 100text \<open> 101 102This example aims at checking that we can extract a reasonable policy 103from the state, i.e. that the function state_objs_to_policy does not connect 104everything to everything. 105 106This example is a system Sys1 made of 2 main components UT1 and T1, 107connected through and endpoint EP1. EP1 is made of one single kernel 108object: obj1_9, the endpoint. Both UT1 and T1 contains: 109 110 . one TCB (obj1_3079 and obj1_3080 resp.) 111 . one vspace made up of one page directory (obj1_6063 and obj1_3065 resp.) 112 . each pd contains a single page table (obj1_3072 and obj1_3077 resp.) 113 . one cspace made up of one cnode (obj1_6 and obj1_7 resp.) 114 . each cspace contains 4 caps: 115 one to the tcb 116 one to the cnode itself 117 one to the vspace 118 one to the ep 119 120UT1 can send to the ep while T1 can receive from it. 121 122Attempt to ASCII art: 123 124 125 -------- ---- ---- -------- 126 | | | | | | | | 127 V | | V S R | V | V 128obj1_3079(tcb)-->obj1_6(cnode)--->obj1_9(ep)<---obj1_7(cnode)<--obj1_3080(tcb) 129 | | | | 130 V | | V 131obj1_3063(pd)<----- -------> obj1_3065(pd) 132 | | 133 V V 134obj1_3072(pt) obj1_3077(pt) 135 136 137(the references are derived from the dump of the SAC system) 138 139 140The aim is to be able to prove 141 142 pas_refined Sys1PAS s1 143 144where Sys1PAS is the label graph defining the AC policy for Sys1 and 145s1 is the state of Sys1 described above. 146 147This shows that the aag extracted from s1 (by state_objs_to_policy) is 148included in the policy graph Sys1PAS. 149 150\<close> 151 152 153subsubsection \<open>Defining the State\<close> 154 155text \<open>We need to define the asids of each pd and pt to ensure that 156the object is included in the right ASID-label\<close> 157 158text \<open>UT1's ASID\<close> 159 160definition 161 asid1_3063 :: machine_word 162where 163 "asid1_3063 \<equiv> 1<<asid_low_bits" 164 165text \<open>T1's ASID\<close> 166 167definition 168 asid1_3065 :: machine_word 169where 170 "asid1_3065 \<equiv> 2<<asid_low_bits" 171 172lemma "asid_high_bits_of asid1_3065 \<noteq> asid_high_bits_of asid1_3063" 173by (simp add: asid1_3063_def asid_high_bits_of_def asid1_3065_def asid_low_bits_def) 174 175 176text \<open>UT1's CSpace\<close> 177 178definition 179 caps1_6 :: cnode_contents 180where 181 "caps1_6 \<equiv> 182 (empty_cnode 10) 183 ( (the_nat_to_bl_10 1) 184 \<mapsto> ThreadCap 3079, 185 (the_nat_to_bl_10 2) 186 \<mapsto> CNodeCap 6 undefined undefined, 187 (the_nat_to_bl_10 3) 188 \<mapsto> ArchObjectCap (PageDirectoryCap 3063 189 (Some asid1_3063)), 190 (the_nat_to_bl_10 318) 191 \<mapsto> EndpointCap 9 0 {AllowSend} )" 192 193 194definition 195 obj1_6 :: kernel_object 196where 197 "obj1_6 \<equiv> CNode 10 caps1_6" 198 199text \<open>T1's Cspace\<close> 200 201definition 202 caps1_7 :: cnode_contents 203where 204 "caps1_7 \<equiv> 205 (empty_cnode 10) 206 ( (the_nat_to_bl_10 1) 207 \<mapsto> ThreadCap 3080, 208 (the_nat_to_bl_10 2) 209 \<mapsto> CNodeCap 7 undefined undefined, 210 (the_nat_to_bl_10 3) 211 \<mapsto> ArchObjectCap (PageDirectoryCap 3065 212 (Some asid1_3065)), 213 (the_nat_to_bl_10 318) 214 \<mapsto> EndpointCap 9 0 {AllowRecv}) " 215 216definition 217 obj1_7 :: kernel_object 218where 219 "obj1_7 \<equiv> CNode 10 caps1_7" 220 221 222text \<open>endpoint between UT1 and T1\<close> 223 224definition 225 obj1_9 :: kernel_object 226where 227 "obj1_9 \<equiv> Endpoint IdleEP" 228 229 230text \<open>UT1's VSpace (PageDirectory)\<close> 231 232definition 233 pt1_3072 :: "word8 \<Rightarrow> pte " 234where 235 "pt1_3072 \<equiv> (\<lambda>_. InvalidPTE)" 236 237definition 238 obj1_3072 :: kernel_object 239where 240 "obj1_3072 \<equiv> ArchObj (PageTable pt1_3072)" 241 242 243definition 244 pd1_3063 :: "12 word \<Rightarrow> pde " 245where 246 "pd1_3063 \<equiv> 247 (\<lambda>_. InvalidPDE) 248 (0 := PageTablePDE 249 (addrFromPPtr 3072) 250 undefined 251 undefined )" 252 253(* used addrFromPPtr because proof gives me ptrFromAddr.. TODO: check 254if it's right *) 255 256definition 257 obj1_3063 :: kernel_object 258where 259 "obj1_3063 \<equiv> ArchObj (PageDirectory pd1_3063)" 260 261 262text \<open>T1's VSpace (PageDirectory)\<close> 263 264 265definition 266 pt1_3077 :: "word8 \<Rightarrow> pte " 267where 268 "pt1_3077 \<equiv> 269 (\<lambda>_. InvalidPTE)" 270 271 272definition 273 obj1_3077 :: kernel_object 274where 275 "obj1_3077 \<equiv> ArchObj (PageTable pt1_3077)" 276 277 278definition 279 pd1_3065 :: "12 word \<Rightarrow> pde " 280where 281 "pd1_3065 \<equiv> 282 (\<lambda>_. InvalidPDE) 283 (0 := PageTablePDE 284 (addrFromPPtr 3077) 285 undefined 286 undefined )" 287 288(* used addrFromPPtr because proof gives me ptrFromAddr.. TODO: check 289if it's right *) 290 291definition 292 obj1_3065 :: kernel_object 293where 294 "obj1_3065 \<equiv> ArchObj (PageDirectory pd1_3065)" 295 296 297text \<open>UT1's tcb\<close> 298 299definition 300 obj1_3079 :: kernel_object 301where 302 "obj1_3079 \<equiv> 303 TCB \<lparr> 304 tcb_ctable = CNodeCap 6 undefined undefined, 305 tcb_vtable = ArchObjectCap (PageDirectoryCap 3063 (Some asid1_3063)), 306 tcb_reply = ReplyCap 3079 True {AllowGrant,AllowWrite}, \<comment> \<open>master reply cap to itself\<close> 307 tcb_caller = NullCap, 308 tcb_ipcframe = NullCap, 309 tcb_state = Running, 310 tcb_fault_handler = undefined, 311 tcb_ipc_buffer = undefined, 312 tcb_fault = undefined, 313 tcb_bound_notification = None, 314 tcb_mcpriority = undefined, 315 tcb_arch = \<lparr>tcb_context = undefined\<rparr> \<rparr>" 316 317 318text \<open>T1's tcb\<close> 319 320definition 321 obj1_3080 :: kernel_object 322where 323 "obj1_3080 \<equiv> 324 TCB \<lparr> 325 tcb_ctable = CNodeCap 7 undefined undefined, 326 tcb_vtable = ArchObjectCap (PageDirectoryCap 3065 (Some asid1_3065)), 327 tcb_reply = ReplyCap 3080 True {AllowGrant,AllowWrite}, \<comment> \<open>master reply cap to itself\<close> 328 tcb_caller = NullCap, 329 tcb_ipcframe = NullCap, 330 tcb_state = BlockedOnReceive 9 \<lparr> receiver_can_grant = False \<rparr>, 331 tcb_fault_handler = undefined, 332 tcb_ipc_buffer = undefined, 333 tcb_fault = undefined, 334 tcb_bound_notification = None, 335 tcb_mcpriority = undefined, 336 tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>" 337 338definition 339 "obj1_10 \<equiv> CNode 10 (Map.empty([] \<mapsto> cap.NullCap))" 340 341 342(* the boolean in BlockedOnReceive is True if the object can receive but not send. 343but Tom says it only matters if the sender can grant - which is not the case of the UT1 - I think *) 344 345definition 346 kh1 :: kheap 347where 348 "kh1 \<equiv> [ 6 \<mapsto> obj1_6, 349 7 \<mapsto> obj1_7, 350 9 \<mapsto> obj1_9, 351 10 \<mapsto> obj1_10, 352 3063 \<mapsto> obj1_3063, 353 3065 \<mapsto> obj1_3065, 354 3072 \<mapsto> obj1_3072, 355 3077 \<mapsto> obj1_3077, 356 3079 \<mapsto> obj1_3079, 357 3080 \<mapsto> obj1_3080 ]" 358 359lemmas kh1_obj_def = 360 obj1_6_def obj1_7_def obj1_9_def obj1_10_def obj1_3063_def obj1_3065_def 361 obj1_3072_def obj1_3077_def obj1_3079_def obj1_3080_def 362 363definition exst1 :: "det_ext" where 364 "exst1 \<equiv> \<lparr>work_units_completed_internal = undefined, 365 scheduler_action_internal = undefined, 366 ekheap_internal = \<lambda>x. None, 367 domain_list_internal = undefined, 368 domain_index_internal = undefined, 369 cur_domain_internal = undefined, 370 domain_time_internal = undefined, 371 ready_queues_internal = undefined, 372 cdt_list_internal = undefined\<rparr>" 373 374definition 375 s1 :: "det_ext state" 376where 377 "s1 \<equiv> \<lparr> 378 kheap = kh1, 379 cdt = Map.empty, 380 is_original_cap = undefined, 381 cur_thread = undefined, 382 idle_thread = undefined, 383 machine_state = undefined, 384 interrupt_irq_node = (\<lambda>_. 10), 385 interrupt_states = undefined, 386 arch_state = \<lparr> 387 arm_asid_table = (\<lambda> x. None), 388 arm_hwasid_table = undefined, 389 arm_next_asid = undefined, 390 arm_asid_map = undefined, 391 arm_global_pd = undefined, 392 arm_global_pts = undefined, 393 arm_kernel_vspace = undefined 394 \<rparr>, 395 exst = exst1 396 \<rparr>" 397 398 399subsubsection \<open>Defining the policy graph\<close> 400 401 402datatype Sys1Labels = 403 UT1 | T1 | EP1 | IRQ1 404 405definition 406 Sys1AgentMap :: "Sys1Labels agent_map" 407where 408 "Sys1AgentMap \<equiv> 409 (\<lambda>_. undefined) 410 (6 := UT1, 411 7 := T1, 412 9 := EP1, 413 10 := IRQ1, 414 3063 := UT1, 415 3065 := T1, 416 3072 := UT1, 417 3077 := T1, 418 3079 := UT1, 419 3080 := T1 )" 420 421lemma Sys1AgentMap_simps: 422 "Sys1AgentMap 6 = UT1" 423 "Sys1AgentMap 7 = T1" 424 "Sys1AgentMap 9 = EP1" 425 "Sys1AgentMap 10 = IRQ1" 426 "Sys1AgentMap 3063 = UT1" 427 "Sys1AgentMap 3065 = T1" 428 "Sys1AgentMap 3072 = UT1" 429 "Sys1AgentMap 3077 = T1" 430 "Sys1AgentMap 3079 = UT1" 431 "Sys1AgentMap 3080 = T1" 432 unfolding Sys1AgentMap_def by simp_all 433 434definition 435 Sys1AuthGraph_aux :: "Sys1Labels auth_graph" 436where 437 "Sys1AuthGraph_aux \<equiv> 438 { (UT1, auth.SyncSend, EP1), 439 (UT1, auth.Reset, EP1), 440 (T1, auth.Receive, EP1), 441 (T1, auth.Reset, EP1) }" 442 443definition 444 Sys1AuthGraph:: "Sys1Labels auth_graph" 445where 446 "Sys1AuthGraph \<equiv> complete_AuthGraph Sys1AuthGraph_aux {T1, UT1}" 447 448 449definition 450 Sys1ASIDMap :: "Sys1Labels agent_asid_map" 451where 452 "Sys1ASIDMap \<equiv> 453 (\<lambda>x. if (asid_high_bits_of x = asid_high_bits_of asid1_3063) 454 then UT1 455 else if (asid_high_bits_of x = asid_high_bits_of asid1_3065) 456 then T1 else undefined)" 457 458definition Sys1PAS :: "Sys1Labels PAS" where 459 "Sys1PAS \<equiv> \<lparr> pasObjectAbs = Sys1AgentMap, pasASIDAbs = Sys1ASIDMap, pasIRQAbs = (\<lambda>_. IRQ1), 460 pasPolicy = Sys1AuthGraph, pasSubject = UT1, pasMayActivate = True, pasMayEditReadyQueues = True, pasMaySendIrqs = True, pasDomainAbs = undefined \<rparr>" 461 462subsubsection \<open>Proof of pas_refined for Sys1\<close> 463 464lemma caps1_7_well_formed: "well_formed_cnode_n 10 caps1_7" 465 apply (clarsimp simp: caps1_7_def well_formed_cnode_n_def) 466 apply (clarsimp simp: the_nat_to_bl_10_def the_nat_to_bl_def nat_to_bl_def) 467 apply (clarsimp simp: empty_cnode_def dom_def) 468 apply (rule set_eqI, clarsimp) 469 apply (rule iffI) 470 apply (elim disjE, insert len_bin_to_bl, simp_all)[1] 471 apply clarsimp 472done 473 474lemma caps1_6_well_formed: "well_formed_cnode_n 10 caps1_6" 475 apply (clarsimp simp: caps1_6_def well_formed_cnode_n_def) 476 apply (clarsimp simp: the_nat_to_bl_10_def the_nat_to_bl_def nat_to_bl_def) 477 apply (clarsimp simp: empty_cnode_def dom_def) 478 apply (rule set_eqI, clarsimp) 479 apply (rule iffI) 480 apply (elim disjE, insert len_bin_to_bl, simp_all)[1] 481 apply clarsimp 482done 483 484(* clagged from KernelInit_R *) 485lemma empty_cnode_apply[simp]: 486 "(empty_cnode n xs = Some cap) = (length xs = n \<and> cap = NullCap)" 487 by (auto simp add: empty_cnode_def) 488 489 490lemma s1_caps_of_state : 491 "caps_of_state s1 p = Some cap \<Longrightarrow> 492 cap = NullCap \<or> 493 (p,cap) \<in> 494 { ((6::obj_ref,(the_nat_to_bl_10 1)), ThreadCap 3079), 495 ((6::obj_ref,(the_nat_to_bl_10 2)), CNodeCap 6 undefined undefined), 496 ((6::obj_ref,(the_nat_to_bl_10 3)), ArchObjectCap (PageDirectoryCap 3063 (Some asid1_3063))), 497 ((6::obj_ref,(the_nat_to_bl_10 318)),EndpointCap 9 0 {AllowSend}), 498 ((7::obj_ref,(the_nat_to_bl_10 1)), ThreadCap 3080), 499 ((7::obj_ref,(the_nat_to_bl_10 2)), CNodeCap 7 undefined undefined), 500 ((7::obj_ref,(the_nat_to_bl_10 3)), ArchObjectCap (PageDirectoryCap 3065 (Some asid1_3065))), 501 ((7::obj_ref,(the_nat_to_bl_10 318)),EndpointCap 9 0 {AllowRecv}) , 502 ((3079::obj_ref, (tcb_cnode_index 0)), CNodeCap 6 undefined undefined ), 503 ((3079::obj_ref, (tcb_cnode_index 1)), ArchObjectCap (PageDirectoryCap 3063 (Some asid1_3063))), 504 ((3079::obj_ref, (tcb_cnode_index 2)), ReplyCap 3079 True {AllowGrant,AllowWrite}), 505 ((3079::obj_ref, (tcb_cnode_index 3)), NullCap), 506 ((3079::obj_ref, (tcb_cnode_index 4)), NullCap), 507 ((3080::obj_ref, (tcb_cnode_index 0)), CNodeCap 7 undefined undefined ), 508 ((3080::obj_ref, (tcb_cnode_index 1)), ArchObjectCap (PageDirectoryCap 3065 (Some asid1_3065))), 509 ((3080::obj_ref, (tcb_cnode_index 2)), ReplyCap 3080 True {AllowGrant,AllowWrite}), 510 ((3080::obj_ref, (tcb_cnode_index 3)), NullCap), 511 ((3080::obj_ref, (tcb_cnode_index 4)), NullCap)} " 512 apply (insert caps1_7_well_formed) 513 apply (insert caps1_6_well_formed) 514 apply (simp add: caps_of_state_cte_wp_at cte_wp_at_cases s1_def kh1_def kh1_obj_def) 515 apply (case_tac p, clarsimp) 516 apply (clarsimp split: if_splits) 517 apply (clarsimp simp: cte_wp_at_cases tcb_cap_cases_def 518 split: if_split_asm)+ 519 apply (clarsimp simp: caps1_7_def split: if_splits) 520 apply (clarsimp simp: caps1_6_def cte_wp_at_cases split: if_splits) 521done 522 523 524lemma Sys1_wellformed: "pas_wellformed Sys1PAS" 525 apply (clarsimp simp: Sys1PAS_def 526 policy_wellformed_def 527 Sys1AuthGraph_def 528 Sys1AuthGraph_aux_def 529 complete_AuthGraph_def) 530 apply blast 531 done 532 533lemma tcb_states_of_state_1: 534 "tcb_states_of_state s1 = [0xC08 \<mapsto> thread_state.BlockedOnReceive 9 \<lparr> receiver_can_grant = False \<rparr>, 0xC07 \<mapsto> thread_state.Running ]" 535 unfolding s1_def tcb_states_of_state_def 536 apply (rule ext) 537 apply (simp add: get_tcb_def) 538 apply (simp add: kh1_def kh1_obj_def ) 539 done 540 541lemma thread_bound_ntfns_1: 542 "thread_bound_ntfns s1 = Map.empty" 543 unfolding s1_def thread_bound_ntfns_def 544 apply (rule ext) 545 apply (simp add: get_tcb_def) 546 apply (simp add: kh1_def kh1_obj_def ) 547 done 548 549declare AllowSend_def[simp] AllowRecv_def[simp] 550 551lemma domains_of_state_s1[simp]: 552 "domains_of_state s1 = {}" 553 apply(rule equalityI) 554 apply(rule subsetI) 555 apply clarsimp 556 apply(erule domains_of_state_aux.induct) 557 apply(simp add: s1_def exst1_def) 558 apply simp 559 done 560 561lemma "pas_refined Sys1PAS s1" 562 apply (clarsimp simp: pas_refined_def) 563 apply (intro conjI) 564 subgoal by (simp add: Sys1_wellformed) 565 subgoal by (simp add: irq_map_wellformed_aux_def s1_def Sys1AgentMap_simps Sys1PAS_def) 566 subgoal by (simp add: tcb_domain_map_wellformed_aux_def) 567 apply (clarsimp simp: auth_graph_map_def 568 Sys1PAS_def 569 state_objs_to_policy_def 570 )+ 571 apply (erule state_bits_to_policy.cases, simp_all, clarsimp) 572 apply (drule s1_caps_of_state, clarsimp) 573 apply (simp add: Sys1AuthGraph_def complete_AuthGraph_def Sys1AuthGraph_aux_def) 574 apply (elim disjE conjE; solves\<open>clarsimp simp: Sys1AgentMap_simps cap_auth_conferred_def cap_rights_to_auth_def\<close>) 575 apply (drule s1_caps_of_state, clarsimp) 576 apply (elim disjE; solves \<open>simp add: thread_bound_ntfns_def\<close>) 577 apply (clarsimp simp: state_refs_of_def thread_states_def tcb_states_of_state_1 578 Sys1AuthGraph_def Sys1AgentMap_simps 579 complete_AuthGraph_def 580 Sys1AuthGraph_aux_def 581 split: if_splits) 582 apply (simp add: thread_bound_ntfns_1) 583 apply (simp add: s1_def) (* this is OK because cdt is empty..*) 584 apply (simp add: s1_def) (* this is OK because cdt is empty..*) 585 586 apply (fastforce simp: state_vrefs_def 587 vs_refs_no_global_pts_def 588 s1_def kh1_def Sys1AgentMap_simps 589 kh1_obj_def comp_def pt1_3072_def pt1_3077_def pte_ref_def pde_ref2_def pd1_3065_def pd1_3063_def 590 Sys1AuthGraph_def ptr_range_def 591 complete_AuthGraph_def 592 Sys1AuthGraph_aux_def 593 dest!: graph_ofD 594 split: if_splits) 595 596 apply (rule subsetI, clarsimp) 597 apply (erule state_asids_to_policy_aux.cases) 598 apply clarsimp 599 apply (drule s1_caps_of_state, clarsimp) 600 apply (simp add: Sys1AuthGraph_def complete_AuthGraph_def Sys1AuthGraph_aux_def Sys1PAS_def Sys1ASIDMap_def) 601 apply (elim disjE conjE, simp_all add: Sys1AgentMap_simps cap_auth_conferred_def cap_rights_to_auth_def asid1_3065_def asid1_3063_def 602 asid_low_bits_def asid_high_bits_of_def )[1] 603 apply (clarsimp simp: state_vrefs_def 604 vs_refs_no_global_pts_def 605 s1_def kh1_def Sys1AgentMap_simps 606 kh1_obj_def comp_def pt1_3072_def pt1_3077_def pte_ref_def pde_ref2_def pd1_3065_def pd1_3063_def 607 Sys1AuthGraph_def ptr_range_def 608 complete_AuthGraph_def 609 Sys1AuthGraph_aux_def 610 dest!: graph_ofD 611 split: if_splits) 612 apply (clarsimp simp: s1_def) 613 apply (rule subsetI, clarsimp) 614 apply (erule state_irqs_to_policy_aux.cases) 615 apply (simp add: Sys1AuthGraph_def complete_AuthGraph_def Sys1AuthGraph_aux_def Sys1PAS_def Sys1ASIDMap_def) 616 apply (drule s1_caps_of_state) 617 apply (simp add: Sys1AuthGraph_def complete_AuthGraph_def Sys1AuthGraph_aux_def Sys1PAS_def Sys1ASIDMap_def) 618 apply (elim disjE conjE, simp_all add: Sys1AgentMap_simps cap_auth_conferred_def cap_rights_to_auth_def asid1_3065_def asid1_3063_def 619 asid_low_bits_def asid_high_bits_of_def )[1] 620 done 621 622 623(*---------------------------------------------------------*) 624subsection \<open>Example 2\<close> 625 626text \<open> 627 628This example systems Sys2 aims at checking that we can have 2 629components, one untrusted UT2 and one truted T1, sharing a cnode obj2_5. 630 631Both UT2 and T2 contains: 632 633 . one TCB (obj2_3079 and obj2_3080 resp.) 634 . one vspace made up of one page directory (obj2_6063 and obj2_3065 resp.) 635 . each pd contains a single page table (obj2_3072 and obj2_3077 resp.) 636 . one cspace made up of one cnode (obj2_6 and obj2_7 resp.) 637 . each cspace contains 4 caps: 638 one to the tcb 639 one to the cnode itself 640 one to the vspace 641 one to obj2_5 642 643 644Attempt to ASCII art: 645 646 647 -------- ---- ---- -------- 648 | | | | | | | | 649 V | | V S R | V | V 650obj2_3079(tcb)-->obj2_6(cnode)--->obj2_5(cnode)<---obj2_7(cnode)<--obj2_3080(tcb) 651 | | | | 652 V | | V 653obj2_3063(pd)<----- -------> obj2_3065(pd) 654 | | 655 V V 656obj2_3072(pt) obj2_3077(pt) 657 658 659(the references are derived from the dump of the SAC system) 660 661 662The aim is to be able to prove 663 664 pas_refined Sys2PAS s2 665 666where Sys2PAS is the label graph defining the AC policy for Sys2 and 667s2 is the state of Sys2 described above. 668 669This shows that the aag extracted from s2 (by state_objs_to_policy) is 670included in the policy graph Sys2PAS. 671 672\<close> 673 674 675subsubsection \<open>Defining the State\<close> 676 677 678 679text \<open>We need to define the asids of each pd and pt to ensure that 680the object is included in the right ASID-label\<close> 681 682text \<open>UT2's ASID\<close> 683 684definition 685 asid2_3063 :: machine_word 686where 687 "asid2_3063 \<equiv> 1<<asid_low_bits" 688 689text \<open>T2's ASID\<close> 690 691definition 692 asid2_3065 :: machine_word 693where 694 "asid2_3065 \<equiv> 2<<asid_low_bits" 695 696lemma "asid_high_bits_of asid2_3065 \<noteq> asid_high_bits_of asid2_3063" 697by (simp add: asid2_3063_def asid_high_bits_of_def asid2_3065_def asid_low_bits_def) 698 699 700 701text \<open>the intermediaite CSpace\<close> 702 703definition 704 caps2_5 :: cnode_contents 705where 706 "caps2_5 \<equiv> 707 (empty_cnode 10)" 708 709definition 710 obj2_5 :: kernel_object 711where 712 "obj2_5 \<equiv> CNode 10 caps2_5" 713 714 715 716text \<open>UT2's CSpace\<close> 717 718definition 719 caps2_6 :: cnode_contents 720where 721 "caps2_6 \<equiv> 722 (empty_cnode 10) 723 ( (the_nat_to_bl_10 1) 724 \<mapsto> ThreadCap 3079, 725 (the_nat_to_bl_10 2) 726 \<mapsto> CNodeCap 6 undefined undefined, 727 (the_nat_to_bl_10 3) 728 \<mapsto> ArchObjectCap (PageDirectoryCap 3063 729 (Some asid2_3063)), 730 (the_nat_to_bl_10 4) 731 \<mapsto> CNodeCap 5 undefined undefined )" 732 733 734definition 735 obj2_6 :: kernel_object 736where 737 "obj2_6 \<equiv> CNode 10 caps2_6" 738 739text \<open>T2's Cspace\<close> 740 741definition 742 caps2_7 :: cnode_contents 743where 744 "caps2_7 \<equiv> 745 (empty_cnode 10) 746 ( (the_nat_to_bl_10 1) 747 \<mapsto> ThreadCap 3080, 748 (the_nat_to_bl_10 2) 749 \<mapsto> CNodeCap 7 undefined undefined, 750 (the_nat_to_bl_10 3) 751 \<mapsto> ArchObjectCap (PageDirectoryCap 3065 752 (Some asid2_3065)), 753 (the_nat_to_bl_10 4) 754 \<mapsto> CNodeCap 5 undefined undefined) " 755 756definition 757 obj2_7 :: kernel_object 758where 759 "obj2_7 \<equiv> CNode 10 caps2_7" 760 761 762text \<open>endpoint between UT2 and T2\<close> 763 764definition 765 obj2_9 :: kernel_object 766where 767 "obj2_9 \<equiv> Endpoint IdleEP" 768 769 770text \<open>UT2's VSpace (PageDirectory)\<close> 771 772definition 773 pt2_3072 :: "word8 \<Rightarrow> pte " 774where 775 "pt2_3072 \<equiv> (\<lambda>_. InvalidPTE)" 776 777definition 778 obj2_3072 :: kernel_object 779where 780 "obj2_3072 \<equiv> ArchObj (PageTable pt2_3072)" 781 782 783definition 784 pd2_3063 :: "12 word \<Rightarrow> pde " 785where 786 "pd2_3063 \<equiv> 787 (\<lambda>_. InvalidPDE) 788 (0 := PageTablePDE 789 (addrFromPPtr 3072) 790 undefined 791 undefined )" 792 793(* used addrFromPPtr because proof gives me ptrFromAddr.. TODO: check 794if it's right *) 795 796definition 797 obj2_3063 :: kernel_object 798where 799 "obj2_3063 \<equiv> ArchObj (PageDirectory pd2_3063)" 800 801 802text \<open>T1's VSpace (PageDirectory)\<close> 803 804 805definition 806 pt2_3077 :: "word8 \<Rightarrow> pte " 807where 808 "pt2_3077 \<equiv> 809 (\<lambda>_. InvalidPTE)" 810 811definition 812 obj2_3077 :: kernel_object 813where 814 "obj2_3077 \<equiv> ArchObj (PageTable pt2_3077)" 815 816 817definition 818 pd2_3065 :: "12 word \<Rightarrow> pde " 819where 820 "pd2_3065 \<equiv> 821 (\<lambda>_. InvalidPDE) 822 (0 := PageTablePDE 823 (addrFromPPtr 3077) 824 undefined 825 undefined )" 826 827(* used addrFromPPtr because proof gives me ptrFromAddr.. TODO: check 828if it's right *) 829 830definition 831 obj2_3065 :: kernel_object 832where 833 "obj2_3065 \<equiv> ArchObj (PageDirectory pd2_3065)" 834 835 836text \<open>UT1's tcb\<close> 837 838definition 839 obj2_3079 :: kernel_object 840where 841 "obj2_3079 \<equiv> 842 TCB \<lparr> 843 tcb_ctable = CNodeCap 6 undefined undefined , 844 tcb_vtable = ArchObjectCap (PageDirectoryCap 3063 (Some asid2_3063)), 845 tcb_reply = ReplyCap 3079 True {AllowGrant,AllowWrite}, \<comment> \<open>master reply cap to itself\<close> 846 tcb_caller = NullCap, 847 tcb_ipcframe = NullCap, 848 tcb_state = Running, 849 tcb_fault_handler = undefined, 850 tcb_ipc_buffer = undefined, 851 tcb_fault = undefined, 852 tcb_bound_notification = None, 853 tcb_mcpriority = undefined, 854 tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>" 855 856 857text \<open>T1's tcb\<close> 858 859definition 860 obj2_3080 :: kernel_object 861where 862 "obj2_3080 \<equiv> 863 TCB \<lparr> 864 tcb_ctable = CNodeCap 7 undefined undefined , 865 tcb_vtable = ArchObjectCap (PageDirectoryCap 3065 (Some asid2_3065)), 866 tcb_reply = ReplyCap 3080 True {AllowGrant,AllowWrite}, \<comment> \<open>master reply cap to itself\<close> 867 tcb_caller = NullCap, 868 tcb_ipcframe = NullCap, 869 tcb_state = BlockedOnReceive 9 \<lparr> receiver_can_grant = False \<rparr>, 870 tcb_fault_handler = undefined, 871 tcb_ipc_buffer = undefined, 872 tcb_fault = undefined, 873 tcb_bound_notification = None, 874 tcb_mcpriority = undefined, 875 tcb_arch = \<lparr>tcb_context = undefined\<rparr>\<rparr>" 876 877(* the boolean in BlockedOnReceive is True if the object can receive but not send. 878but Tom says it only matters if the sender can grant - which is not the case of the UT1 - I think *) 879 880definition 881 kh2 :: kheap 882where 883 "kh2 \<equiv> [ 6 \<mapsto> obj2_6, 884 7 \<mapsto> obj2_7, 885 9 \<mapsto> obj2_9, 886 3063 \<mapsto> obj2_3063, 887 3065 \<mapsto> obj2_3065, 888 3072 \<mapsto> obj2_3072, 889 3077 \<mapsto> obj2_3077, 890 3079 \<mapsto> obj2_3079, 891 3080 \<mapsto> obj2_3080 ]" 892 893lemmas kh2_obj_def = 894 obj2_6_def obj2_7_def obj2_9_def obj2_3063_def obj2_3065_def 895 obj2_3072_def obj2_3077_def obj2_3079_def obj2_3080_def 896 897 898definition 899 s2 :: "det_ext state" 900where 901 "s2 \<equiv> \<lparr> 902 kheap = kh2, 903 cdt = Map.empty, 904 is_original_cap = undefined, 905 cur_thread = undefined, 906 idle_thread = undefined, 907 machine_state = undefined, 908 interrupt_irq_node = (\<lambda>_. 9001), 909 interrupt_states = undefined, 910 arch_state = \<lparr> 911 arm_asid_table = (\<lambda> x. None), 912 arm_hwasid_table = undefined, 913 arm_next_asid = undefined, 914 arm_asid_map = undefined, 915 arm_global_pd = undefined, 916 arm_global_pts = undefined, 917 arm_kernel_vspace = undefined 918 \<rparr>, 919 exst = exst1 920 \<rparr>" 921 922 923subsubsection \<open>Defining the policy graph\<close> 924 925 926datatype Sys2Labels = 927 UT2 | T2 | IRQ2 928 929definition 930 Sys2AgentMap :: "Sys2Labels agent_map" 931where 932 "Sys2AgentMap \<equiv> 933 (\<lambda>_. undefined) 934 (5 := UT2, 935 6 := UT2, 936 7 := T2, 937 9 := T2, 938 3063 := UT2, 939 3065 := T2, 940 3072 := UT2, 941 3077 := T2, 942 3079 := UT2, 943 3080 := T2, 944 9001 := IRQ2 )" 945 946 947definition 948 Sys2AuthGraph_aux :: "Sys2Labels auth_graph" 949where 950 "Sys2AuthGraph_aux \<equiv> 951 { (T2, Control, UT2) }" 952 953definition 954 Sys2AuthGraph:: "Sys2Labels auth_graph" 955where 956 "Sys2AuthGraph \<equiv> complete_AuthGraph Sys2AuthGraph_aux {T2, UT2}" 957 958 959definition 960 Sys2ASIDMap :: "Sys2Labels agent_asid_map" 961where 962 "Sys2ASIDMap \<equiv> 963 (\<lambda>_. undefined) 964 (asid2_3063 := UT2, 965 asid2_3065 := T2 )" 966 967definition Sys2PAS :: "Sys2Labels PAS" where 968 "Sys2PAS \<equiv> \<lparr> pasObjectAbs = Sys2AgentMap, pasASIDAbs = Sys2ASIDMap, 969 pasIRQAbs = (\<lambda>_. IRQ2), 970 pasPolicy = Sys2AuthGraph, pasSubject = UT2, pasMayActivate = True, pasMayEditReadyQueues = True, pasMaySendIrqs = True, pasDomainAbs = undefined \<rparr>" 971 972 973 974subsubsection \<open>Proof of pas_refined for Sys2\<close> 975 976lemma caps2_7_well_formed: "well_formed_cnode_n 10 caps2_7" 977 apply (clarsimp simp: caps2_7_def well_formed_cnode_n_def) 978 apply (clarsimp simp: the_nat_to_bl_10_def the_nat_to_bl_def nat_to_bl_def) 979 apply (clarsimp simp: empty_cnode_def dom_def) 980 apply (rule set_eqI, clarsimp) 981 apply (rule iffI) 982 apply (elim disjE, insert len_bin_to_bl, simp_all)[1] 983 apply clarsimp 984done 985 986lemma caps2_6_well_formed: "well_formed_cnode_n 10 caps2_6" 987 apply (clarsimp simp: caps2_6_def well_formed_cnode_n_def) 988 apply (clarsimp simp: the_nat_to_bl_10_def the_nat_to_bl_def nat_to_bl_def) 989 apply (clarsimp simp: empty_cnode_def dom_def) 990 apply (rule set_eqI, clarsimp) 991 apply (rule iffI) 992 apply (elim disjE, insert len_bin_to_bl, simp_all)[1] 993 apply clarsimp 994done 995 996 997 998 999 1000 1001 1002lemma s2_caps_of_state : 1003 "caps_of_state s2 p = Some cap \<Longrightarrow> 1004 cap = NullCap \<or> 1005 (p,cap) \<in> 1006 { ((6::obj_ref,(the_nat_to_bl_10 1)), ThreadCap 3079), 1007 ((6::obj_ref,(the_nat_to_bl_10 2)), CNodeCap 6 undefined undefined), 1008 ((6::obj_ref,(the_nat_to_bl_10 3)), ArchObjectCap (PageDirectoryCap 3063 (Some asid2_3063))), 1009 ((6::obj_ref,(the_nat_to_bl_10 4)), CNodeCap 5 undefined undefined), 1010 ((7::obj_ref,(the_nat_to_bl_10 1)), ThreadCap 3080), 1011 ((7::obj_ref,(the_nat_to_bl_10 2)), CNodeCap 7 undefined undefined), 1012 ((7::obj_ref,(the_nat_to_bl_10 3)), ArchObjectCap (PageDirectoryCap 3065 (Some asid2_3065))), 1013 ((7::obj_ref,(the_nat_to_bl_10 4)), CNodeCap 5 undefined undefined), 1014 ((3079::obj_ref, (tcb_cnode_index 0)), CNodeCap 6 undefined undefined ), 1015 ((3079::obj_ref, (tcb_cnode_index 1)), ArchObjectCap (PageDirectoryCap 3063 (Some asid2_3063))), 1016 ((3079::obj_ref, (tcb_cnode_index 2)), ReplyCap 3079 True {AllowGrant,AllowWrite}), 1017 ((3079::obj_ref, (tcb_cnode_index 3)), NullCap), 1018 ((3079::obj_ref, (tcb_cnode_index 4)), NullCap), 1019 ((3080::obj_ref, (tcb_cnode_index 0)), CNodeCap 7 undefined undefined ), 1020 ((3080::obj_ref, (tcb_cnode_index 1)), ArchObjectCap (PageDirectoryCap 3065 (Some asid2_3065))), 1021 ((3080::obj_ref, (tcb_cnode_index 2)), ReplyCap 3080 True {AllowGrant,AllowWrite}), 1022 ((3080::obj_ref, (tcb_cnode_index 3)), NullCap), 1023 ((3080::obj_ref, (tcb_cnode_index 4)), NullCap)} " 1024 apply (insert caps2_7_well_formed) 1025 apply (insert caps2_6_well_formed) 1026 apply (simp add: caps_of_state_cte_wp_at cte_wp_at_cases s2_def kh2_def kh2_obj_def) 1027 apply (case_tac p, clarsimp) 1028 apply (clarsimp simp: cte_wp_at_cases split: if_splits) 1029 apply (clarsimp simp: tcb_cap_cases_def split: if_splits)+ 1030 apply (clarsimp simp: caps2_7_def split: if_splits) 1031 apply (clarsimp simp: caps2_6_def cte_wp_at_cases split: if_splits) 1032done 1033 1034lemma Sys2_wellformed: "pas_wellformed Sys2PAS" 1035 apply (clarsimp simp: Sys2PAS_def policy_wellformed_def) 1036 apply (intro conjI) 1037 apply (simp_all add: Sys2AuthGraph_def complete_AuthGraph_def 1038 Sys2AuthGraph_aux_def) 1039 done 1040 1041lemma Sys2AgentMap_simps: 1042 "Sys2AgentMap 5 = UT2" 1043 "Sys2AgentMap 6 = UT2" 1044 "Sys2AgentMap 7 = T2" 1045 "Sys2AgentMap 9 = T2" 1046 "Sys2AgentMap 3063 = UT2" 1047 "Sys2AgentMap 3065 = T2" 1048 "Sys2AgentMap 3072 = UT2" 1049 "Sys2AgentMap 3077 = T2" 1050 "Sys2AgentMap 3079 = UT2" 1051 "Sys2AgentMap 3080 = T2" 1052 "Sys2AgentMap 9001 = IRQ2" 1053 by (simp_all add: Sys2AgentMap_def) 1054 1055lemma domains_of_state_s2[simp]: 1056 "domains_of_state s2 = {}" 1057 apply(rule equalityI) 1058 apply(rule subsetI) 1059 apply clarsimp 1060 apply(erule domains_of_state_aux.induct) 1061 apply(simp add: s2_def exst1_def) 1062 apply simp 1063 done 1064 1065lemma thread_bound_ntfns_2[simp]: 1066 "thread_bound_ntfns s2 = Map.empty" 1067 unfolding s2_def thread_bound_ntfns_def 1068 apply (rule ext) 1069 apply (simp add: get_tcb_def) 1070 apply (simp add: kh2_def kh2_obj_def) 1071 done 1072 1073lemma "pas_refined Sys2PAS s2" 1074 apply (clarsimp simp: pas_refined_def) 1075 apply (intro conjI) 1076 apply (simp add: Sys2_wellformed) 1077 apply (simp add: Sys2PAS_def s2_def Sys2AgentMap_def 1078 irq_map_wellformed_aux_def) 1079 apply (clarsimp simp: auth_graph_map_def 1080 Sys2PAS_def 1081 state_objs_to_policy_def 1082 state_bits_to_policy_def tcb_domain_map_wellformed_aux_def)+ 1083 apply (erule state_bits_to_policyp.cases, simp_all) 1084 apply (drule s2_caps_of_state, clarsimp) 1085 apply (elim disjE, simp_all add: cap_auth_conferred_def 1086 Sys2AgentMap_simps 1087 Sys2AuthGraph_def Sys2AuthGraph_aux_def 1088 complete_AuthGraph_def 1089 split: if_split_asm)[1] 1090 apply (drule s2_caps_of_state, clarsimp) 1091 apply (elim disjE, simp_all)[1] 1092 apply (clarsimp simp: state_refs_of_def s2_def kh2_def kh2_obj_def 1093 split: if_splits) 1094 apply (clarsimp split:if_splits option.splits 1095 simp: thread_states_def tcb_states_of_state_def 1096 Sys2AgentMap_simps Sys2AuthGraph_def 1097 complete_AuthGraph_def Sys2AuthGraph_aux_def 1098 dest!: get_tcb_SomeD) 1099 apply (simp add: s2_def) (* this is OK because cdt is empty..*) 1100 apply (simp add: s2_def) (* this is OK because cdt is empty..*) 1101 1102 apply ((clarsimp simp: state_vrefs_def 1103 vs_refs_no_global_pts_def 1104 s2_def kh2_def 1105 kh2_obj_def 1106 split: if_splits, 1107 ((clarsimp split: if_splits 1108 simp: pd2_3065_def pd2_3063_def graph_of_def pde_ref_def 1109 Sys2AgentMap_simps Sys2AuthGraph_def 1110 complete_AuthGraph_def pt2_3077_def pte_ref_def 1111 pt2_3072_def pde_ref2_def 1112 Sys2AuthGraph_aux_def ptr_range_def)+))+)[1] 1113 apply clarsimp 1114 apply (erule state_asids_to_policy_aux.cases) 1115 apply clarsimp 1116 apply (auto simp: Sys2PAS_def Sys2AuthGraph_def Sys2AuthGraph_aux_def 1117 complete_AuthGraph_def Sys2AgentMap_simps 1118 Sys2ASIDMap_def asid2_3063_def asid2_3065_def 1119 asid_low_bits_def 1120 dest!: s2_caps_of_state)[1] 1121 apply (clarsimp simp: state_vrefs_def 1122 vs_refs_no_global_pts_def 1123 s2_def kh2_def 1124 kh2_obj_def 1125 split: if_splits) 1126 apply (clarsimp simp: s2_def) 1127 apply (clarsimp) 1128 apply (erule state_irqs_to_policy_aux.cases) 1129 apply (auto simp: Sys2PAS_def Sys2AuthGraph_def Sys2AuthGraph_aux_def 1130 complete_AuthGraph_def Sys2AgentMap_simps 1131 Sys2ASIDMap_def asid2_3063_def asid2_3065_def 1132 dest!: s2_caps_of_state)[1] 1133 done 1134 1135end 1136 1137end 1138