1(* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 *) 6 7(* 8Abstract model of CSpace. 9*) 10 11chapter "CSpace" 12 13theory CSpace_A 14imports 15 ArchVSpace_A 16 IpcCancel_A 17 ArchCSpace_A 18 "Lib.NonDetMonadLemmas" 19 "HOL-Library.Prefix_Order" 20begin 21 22context begin interpretation Arch . 23 24requalify_consts 25 aobjs_of 26 arch_update_cap_data 27 arch_derive_cap 28 arch_finalise_cap 29 arch_is_physical 30 arch_same_region_as 31 same_aobject_as 32 prepare_thread_delete 33 update_cnode_cap_data 34 cnode_padding_bits 35 cnode_guard_size_bits 36 arch_is_cap_revocable 37 38end 39 40 41text \<open>This theory develops an abstract model of \emph{capability 42spaces}, or CSpace, in seL4. The CSpace of a thread can be thought of 43as the set of all capabilities it has access to. More precisely, it 44is a directed graph of CNodes starting in the CSpace slot of a TCB. 45Capabilities are accessed from the user side by specifying a path in this 46graph. The kernel internally uses references to CNodes with an index into 47the CNode to identify capabilities. 48 49The following sections show basic manipulation of capabilities, 50resolving user-specified, path-based capability references into 51internal kernel references, transfer, revokation, deletion, 52and finally toplevel capability invocations. 53\<close> 54 55section \<open>Basic capability manipulation\<close> 56 57text \<open>Interpret a set of rights from a user data word.\<close> 58definition 59 data_to_rights :: "data \<Rightarrow> cap_rights" where 60 "data_to_rights data \<equiv> let 61 w = data_to_16 data 62 in {x. case x of AllowWrite \<Rightarrow> w !! 0 63 | AllowRead \<Rightarrow> w !! 1 64 | AllowGrant \<Rightarrow> w !! 2 65 | AllowGrantReply \<Rightarrow> w !! 3}" 66 67text \<open>Check that a capability stored in a slot is not a parent of any other 68capability.\<close> 69definition 70 ensure_no_children :: "cslot_ptr \<Rightarrow> (unit,'z::state_ext) se_monad" where 71 "ensure_no_children cslot_ptr \<equiv> doE 72 cdt \<leftarrow> liftE $ gets cdt; 73 whenE (\<exists>c. cdt c = Some cslot_ptr) (throwError RevokeFirst) 74 odE" 75 76definition 77 max_free_index :: "nat \<Rightarrow> nat" where 78 "max_free_index magnitude_bits \<equiv> 2 ^ magnitude_bits" 79 80definition 81 free_index_update :: "(nat \<Rightarrow> nat) \<Rightarrow> cap \<Rightarrow> cap" 82where 83 "free_index_update g cap \<equiv> 84 case cap of UntypedCap dev ref sz f \<Rightarrow> UntypedCap dev ref sz (g f) | _ \<Rightarrow> cap" 85 86primrec (nonexhaustive) 87 untyped_sz_bits :: "cap \<Rightarrow> nat" 88where 89 "untyped_sz_bits (UntypedCap dev ref sz f) = sz" 90 91abbreviation 92 max_free_index_update :: "cap \<Rightarrow> cap" 93where 94 "max_free_index_update cap \<equiv> cap \<lparr> free_index:= max_free_index (untyped_sz_bits cap) \<rparr>" 95 96definition 97 set_untyped_cap_as_full :: "cap \<Rightarrow> cap \<Rightarrow> obj_ref \<times> bool list \<Rightarrow> (unit,'z::state_ext) s_monad" 98where 99 "set_untyped_cap_as_full src_cap new_cap src_slot \<equiv> 100 if (is_untyped_cap src_cap \<and> is_untyped_cap new_cap 101 \<and> obj_ref_of src_cap = obj_ref_of new_cap \<and> cap_bits_untyped src_cap = cap_bits_untyped new_cap) 102 then set_cap (max_free_index_update src_cap) src_slot else return ()" 103 104text \<open>Derive a cap into a form in which it can be copied. For internal reasons 105not all capability types can be copied at all times and not all capability types 106can be copied unchanged.\<close> 107definition 108derive_cap :: "cslot_ptr \<Rightarrow> cap \<Rightarrow> (cap,'z::state_ext) se_monad" where 109"derive_cap slot cap \<equiv> 110 case cap of 111 ArchObjectCap c \<Rightarrow> arch_derive_cap c 112 | UntypedCap dev ptr sz f \<Rightarrow> doE ensure_no_children slot; returnOk cap odE 113 | Zombie ptr n sz \<Rightarrow> returnOk NullCap 114 | ReplyCap ptr m cr \<Rightarrow> returnOk NullCap 115 | IRQControlCap \<Rightarrow> returnOk NullCap 116 | _ \<Rightarrow> returnOk cap" 117 118text \<open>Transform a capability on request from a user thread. The user-supplied 119argument word is interpreted differently for different cap types. If the 120preserve flag is set this transformation is being done in-place which means some 121changes are disallowed because they would invalidate existing CDT relationships. 122\<close> 123definition 124 update_cap_data :: "bool \<Rightarrow> data \<Rightarrow> cap \<Rightarrow> cap" where 125"update_cap_data preserve w cap \<equiv> 126 if is_ep_cap cap then 127 if cap_ep_badge cap = 0 \<and> \<not> preserve then 128 badge_update w cap 129 else NullCap 130 else if is_ntfn_cap cap then 131 if cap_ep_badge cap = 0 \<and> \<not> preserve then 132 badge_update w cap 133 else NullCap 134 else if is_cnode_cap cap then 135 let 136 (oref, bits, guard) = the_cnode_cap cap; 137 (guard_size', guard'') = update_cnode_cap_data w; 138 guard' = drop (size guard'' - guard_size') (to_bl guard'') 139 in 140 if guard_size' + bits > word_bits 141 then NullCap 142 else CNodeCap oref bits guard' 143 else if is_arch_cap cap then 144 arch_update_cap_data preserve w (the_arch_cap cap) 145 else 146 cap" 147 148section \<open>Resolving capability references\<close> 149 150text \<open> 151Recursively looks up a capability address to a CNode slot by walking over 152multiple CNodes until all the bits in the address are used or there are 153no further CNodes. 154\<close> 155function resolve_address_bits' :: "'z itself \<Rightarrow> cap \<times> cap_ref \<Rightarrow> (cslot_ptr \<times> cap_ref,'z::state_ext) lf_monad" 156where 157 "resolve_address_bits' z (cap, cref) = 158 (case cap of 159 CNodeCap oref radix_bits guard \<Rightarrow> 160 if radix_bits + size guard = 0 then 161 fail \<comment> \<open>nothing is translated: table broken\<close> 162 else doE 163 whenE (\<not> guard \<le> cref) 164 \<comment> \<open>guard does not match\<close> 165 (throwError $ GuardMismatch (size cref) guard); 166 167 whenE (size cref < radix_bits + size guard) 168 \<comment> \<open>not enough bits to resolve: table malformed\<close> 169 (throwError $ DepthMismatch (size cref) (radix_bits+size guard)); 170 171 offset \<leftarrow> returnOk $ take radix_bits (drop (size guard) cref); 172 rest \<leftarrow> returnOk $ drop (radix_bits + size guard) cref; 173 if rest = [] then 174 returnOk ((oref,offset), []) 175 else doE 176 next_cap \<leftarrow> liftE $ get_cap (oref, offset); 177 if is_cnode_cap next_cap then 178 resolve_address_bits' z (next_cap, rest) 179 else 180 returnOk ((oref,offset), rest) 181 odE 182 odE 183 | _ \<Rightarrow> throwError InvalidRoot)" 184 by auto 185 186lemma rab_termination: 187 "\<forall>cref guard radix_bits. 188 \<not> length cref \<le> radix_bits + length guard \<and> 189 (0 < radix_bits \<or> guard \<noteq> []) \<longrightarrow> 190 length cref - (radix_bits + length guard) < length cref" 191 apply clarsimp 192 apply (erule disjE) 193 apply arith 194 apply (clarsimp simp: neq_Nil_conv) 195 apply arith 196 done 197 198termination 199 apply (relation "measure (\<lambda>(z,cap, cs). size cs)") 200 apply (auto simp: whenE_def returnOk_def return_def rab_termination) 201 done 202 203declare resolve_address_bits'.simps[simp del] 204 205definition resolve_address_bits where 206"resolve_address_bits \<equiv> resolve_address_bits' TYPE('z::state_ext)" 207 208text \<open>Specialisations of the capability lookup process to various standard 209cases.\<close> 210definition 211 lookup_slot_for_thread :: "obj_ref \<Rightarrow> cap_ref \<Rightarrow> (cslot_ptr \<times> cap_ref,'z::state_ext) lf_monad" 212where 213 "lookup_slot_for_thread thread cref \<equiv> doE 214 tcb \<leftarrow> liftE $ gets_the $ get_tcb thread; 215 resolve_address_bits (tcb_ctable tcb, cref) 216 odE" 217 218definition 219 lookup_cap_and_slot :: "obj_ref \<Rightarrow> cap_ref \<Rightarrow> (cap \<times> cslot_ptr,'z::state_ext) lf_monad" where 220 "lookup_cap_and_slot thread cptr \<equiv> doE 221 (slot, cr) \<leftarrow> lookup_slot_for_thread thread cptr; 222 cap \<leftarrow> liftE $ get_cap slot; 223 returnOk (cap, slot) 224 odE" 225 226definition 227 lookup_cap :: "obj_ref \<Rightarrow> cap_ref \<Rightarrow> (cap,'z::state_ext) lf_monad" where 228 "lookup_cap thread ref \<equiv> doE 229 (ref', _) \<leftarrow> lookup_slot_for_thread thread ref; 230 liftE $ get_cap ref' 231 odE" 232 233definition 234 lookup_slot_for_cnode_op :: 235 "bool \<Rightarrow> cap \<Rightarrow> cap_ref \<Rightarrow> nat \<Rightarrow> (cslot_ptr,'z::state_ext) se_monad" 236where 237 "lookup_slot_for_cnode_op is_source croot ptr depth \<equiv> 238 if is_cnode_cap croot then 239 doE 240 whenE (depth < 1 \<or> depth > word_bits) 241 $ throwError (RangeError 1 (of_nat word_bits)); 242 lookup_error_on_failure is_source $ doE 243 ptrbits_for_depth \<leftarrow> returnOk $ drop (length ptr - depth) ptr; 244 (slot, rem) \<leftarrow> resolve_address_bits (croot, ptrbits_for_depth); 245 case rem of 246 [] \<Rightarrow> returnOk slot 247 | _ \<Rightarrow> throwError $ DepthMismatch (length rem) 0 248 odE 249 odE 250 else 251 throwError (FailedLookup is_source InvalidRoot)" 252 253definition 254 lookup_source_slot :: "cap \<Rightarrow> cap_ref \<Rightarrow> nat \<Rightarrow> (cslot_ptr,'z::state_ext) se_monad" 255where 256 "lookup_source_slot \<equiv> lookup_slot_for_cnode_op True" 257 258definition 259 lookup_target_slot :: "cap \<Rightarrow> cap_ref \<Rightarrow> nat \<Rightarrow> (cslot_ptr,'z::state_ext) se_monad" 260where 261 "lookup_target_slot \<equiv> lookup_slot_for_cnode_op False" 262 263definition 264 lookup_pivot_slot :: "cap \<Rightarrow> cap_ref \<Rightarrow> nat \<Rightarrow> (cslot_ptr,'z::state_ext) se_monad" 265where 266 "lookup_pivot_slot \<equiv> lookup_slot_for_cnode_op True" 267 268 269section \<open>Transferring capabilities\<close> 270 271text \<open>These functions are used in interpreting from user arguments the manner 272in which a capability transfer should take place.\<close> 273 274definition 275 captransfer_from_words :: "machine_word \<Rightarrow> (captransfer,'z::state_ext) s_monad" 276where 277 "captransfer_from_words ptr \<equiv> do 278 w0 \<leftarrow> do_machine_op $ loadWord ptr; 279 w1 \<leftarrow> do_machine_op $ loadWord (ptr + word_size); 280 w2 \<leftarrow> do_machine_op $ loadWord (ptr + 2 * word_size); 281 return \<lparr> ct_receive_root = data_to_cptr w0, 282 ct_receive_index = data_to_cptr w1, 283 ct_receive_depth = w2 \<rparr> 284 od" 285 286definition 287 load_cap_transfer :: "obj_ref \<Rightarrow> (captransfer,'z::state_ext) s_monad" where 288 "load_cap_transfer buffer \<equiv> do 289 offset \<leftarrow> return $ msg_max_length + msg_max_extra_caps + 2; 290 captransfer_from_words (buffer + of_nat offset * word_size) 291 od" 292 293fun 294 get_receive_slots :: "obj_ref \<Rightarrow> obj_ref option \<Rightarrow> 295 (cslot_ptr list,'z::state_ext) s_monad" 296where 297 "get_receive_slots thread (Some buffer) = do 298 ct \<leftarrow> load_cap_transfer buffer; 299 300 empty_on_failure $ doE 301 cnode \<leftarrow> unify_failure $ 302 lookup_cap thread (ct_receive_root ct); 303 slot \<leftarrow> unify_failure $ lookup_target_slot cnode 304 (ct_receive_index ct) (unat (ct_receive_depth ct)); 305 306 cap \<leftarrow> liftE $ get_cap slot; 307 308 whenE (cap \<noteq> NullCap) (throwError ()); 309 310 returnOk [slot] 311 odE 312 od" 313| "get_receive_slots x None = return []" 314 315 316section \<open>Revoking and deleting capabilities\<close> 317 318text \<open>Deletion of the final capability to any object is a long running 319operation if the capability is of these types.\<close> 320definition 321 long_running_delete :: "cap \<Rightarrow> bool" where 322 "long_running_delete cap \<equiv> case cap of 323 CNodeCap ptr bits gd \<Rightarrow> True 324 | Zombie ptr bits n \<Rightarrow> True 325 | ThreadCap ptr \<Rightarrow> True 326 | _ \<Rightarrow> False" 327 328 329definition 330 slot_cap_long_running_delete :: "cslot_ptr \<Rightarrow> (bool,'z::state_ext) s_monad" 331where 332 "slot_cap_long_running_delete slot \<equiv> do 333 cap \<leftarrow> get_cap slot; 334 case cap of 335 NullCap \<Rightarrow> return False 336 | _ \<Rightarrow> do 337 final \<leftarrow> is_final_cap cap; 338 return (final \<and> long_running_delete cap) 339 od 340 od" 341 342text \<open>Swap the contents of two capability slots. The capability parameters are 343the new states of the capabilities, as the user may request that the 344capabilities are transformed as they are swapped.\<close> 345definition 346 cap_swap :: "cap \<Rightarrow> cslot_ptr \<Rightarrow> cap \<Rightarrow> cslot_ptr \<Rightarrow> (unit,'z::state_ext) s_monad" 347where 348 "cap_swap cap1 slot1 cap2 slot2 \<equiv> 349 do 350 set_cap cap2 slot1; 351 set_cap cap1 slot2; 352 slot1_p \<leftarrow> gets (\<lambda>s. cdt s slot1); 353 slot2_p \<leftarrow> gets (\<lambda>s. cdt s slot2); 354 cdt \<leftarrow> gets cdt; 355 \<comment> \<open>update children:\<close> 356 cdt' \<leftarrow> return (\<lambda>n. if cdt n = Some slot1 357 then Some slot2 358 else if cdt n = Some slot2 359 then Some slot1 360 else cdt n); 361 \<comment> \<open>update parents:\<close> 362 set_cdt (cdt' (slot1 := cdt' slot2, slot2 := cdt' slot1)); 363 do_extended_op (cap_swap_ext slot1 slot2 slot1_p slot2_p); 364 is_original \<leftarrow> gets is_original_cap; 365 set_original slot1 (is_original slot2); 366 set_original slot2 (is_original slot1) 367 od" 368 369text \<open>Move a capability from one slot to another. Once again the new 370capability is a parameter as it may be transformed while it is moved.\<close> 371definition 372 cap_move :: "cap \<Rightarrow> cslot_ptr \<Rightarrow> cslot_ptr \<Rightarrow> (unit,'z::state_ext) s_monad" 373where 374 "cap_move new_cap src_slot dest_slot \<equiv> do 375 set_cap new_cap dest_slot; 376 set_cap NullCap src_slot; 377 src_p \<leftarrow> gets (\<lambda>s. cdt s src_slot); 378 dest_p \<leftarrow> gets (\<lambda>s. cdt s dest_slot); 379 cdt \<leftarrow> gets cdt; 380 parent \<leftarrow> return $ cdt src_slot; 381 cdt' \<leftarrow> return $ cdt(dest_slot := parent, src_slot := None); 382 set_cdt (\<lambda>r. if cdt' r = Some src_slot then Some dest_slot else cdt' r); 383 do_extended_op (cap_move_ext src_slot dest_slot src_p dest_p); 384 is_original \<leftarrow> gets is_original_cap; 385 set_original dest_slot (is_original src_slot); 386 set_original src_slot False 387 od" 388 389text \<open>This version of capability swap does not change the capabilities that 390are swapped, passing the existing capabilities to the more general function.\<close> 391definition 392 cap_swap_for_delete :: "cslot_ptr \<Rightarrow> cslot_ptr \<Rightarrow> (unit,'z::state_ext) s_monad" 393where 394 "cap_swap_for_delete slot1 slot2 \<equiv> 395 when (slot1 \<noteq> slot2) $ do 396 cap1 \<leftarrow> get_cap slot1; 397 cap2 \<leftarrow> get_cap slot2; 398 cap_swap cap1 slot1 cap2 slot2 399 od" 400 401text \<open>The type of possible recursive deletes.\<close> 402datatype 403 rec_del_call 404 = CTEDeleteCall cslot_ptr bool 405 | FinaliseSlotCall cslot_ptr bool 406 | ReduceZombieCall cap cslot_ptr bool 407 408text \<open>Locate the nth capability beyond some base capability slot.\<close> 409definition 410 locate_slot :: "cslot_ptr \<Rightarrow> nat \<Rightarrow> cslot_ptr" where 411 "locate_slot \<equiv> \<lambda>(a, b) n. (a, drop (32 - length b) 412 (to_bl (of_bl b + of_nat n :: word32)))" 413 414text \<open>Actions to be taken after deleting an IRQ Handler capability.\<close> 415definition 416 deleting_irq_handler :: "irq \<Rightarrow> (unit,'z::state_ext) s_monad" 417where 418 "deleting_irq_handler irq \<equiv> do 419 slot \<leftarrow> get_irq_slot irq; 420 cap_delete_one slot 421 od" 422 423text \<open>Actions that must be taken when a capability is deleted. Returns two 424capabilities: The first is a capability to be re-inserted into the slot in place 425of the deleted capability; in particular, this will be a Zombie if the deletion 426requires a long-running operation. The second represents some further 427post-deletion action to be performed after the slot is cleared. For example, 428an IRQHandlerCap indicates an IRQ to be cleared. Arch capabilities may also be 429associated with arch-specific post-deletion actions. For most cases, however, 430NullCap is used to indicate that no post-deletion action is required.\<close> 431 432fun 433 finalise_cap :: "cap \<Rightarrow> bool \<Rightarrow> (cap \<times> cap,'z::state_ext) s_monad" 434where 435 "finalise_cap NullCap final = return (NullCap, NullCap)" 436| "finalise_cap (UntypedCap dev r bits f) final = return (NullCap, NullCap)" 437| "finalise_cap (ReplyCap r m R) final = return (NullCap, NullCap)" 438| "finalise_cap (EndpointCap r b R) final = 439 (liftM (K (NullCap, NullCap)) $ when final $ cancel_all_ipc r)" 440| "finalise_cap (NotificationCap r b R) final = 441 (liftM (K (NullCap, NullCap)) $ when final $ do 442 unbind_maybe_notification r; 443 cancel_all_signals r 444 od)" 445| "finalise_cap (CNodeCap r bits g) final = 446 return (if final then Zombie r (Some bits) (2 ^ bits) else NullCap, NullCap)" 447| "finalise_cap (ThreadCap r) final = 448 do 449 when final $ unbind_notification r; 450 when final $ suspend r; 451 when final $ prepare_thread_delete r; 452 return (if final then (Zombie r None 5) else NullCap, NullCap) 453 od" 454| "finalise_cap DomainCap final = return (NullCap, NullCap)" 455| "finalise_cap (Zombie r b n) final = 456 do assert final; return (Zombie r b n, NullCap) od" 457| "finalise_cap IRQControlCap final = return (NullCap, NullCap)" 458| "finalise_cap (IRQHandlerCap irq) final = ( 459 if final then do 460 deleting_irq_handler irq; 461 return (NullCap, (IRQHandlerCap irq)) 462 od 463 else return (NullCap, NullCap))" 464| "finalise_cap (ArchObjectCap a) final = 465 (arch_finalise_cap a final)" 466 467definition 468 can_fast_finalise :: "cap \<Rightarrow> bool" where 469 "can_fast_finalise cap \<equiv> case cap of 470 ReplyCap r m R \<Rightarrow> True 471 | EndpointCap r b R \<Rightarrow> True 472 | NotificationCap r b R \<Rightarrow> True 473 | NullCap \<Rightarrow> True 474 | _ \<Rightarrow> False" 475 476text \<open>This operation is used to delete a capability when it is known that a 477long-running operation is impossible. It is equivalent to calling the regular 478finalisation operation. It cannot be defined in that way as doing so 479would create a circular definition.\<close> 480 481 482lemma fast_finalise_def2: 483 "fast_finalise cap final = do 484 assert (can_fast_finalise cap); 485 result \<leftarrow> finalise_cap cap final; 486 assert (result = (NullCap, NullCap)) 487 od" 488 supply K_def[simp] 489 by (cases cap, simp_all add: liftM_def assert_def can_fast_finalise_def) 490 491text \<open>The finalisation process on a Zombie or Null capability is finished for 492all Null capabilities and for Zombies that cover no slots or only the slot they 493are currently stored in.\<close> 494primrec (nonexhaustive) 495 cap_removeable :: "cap \<Rightarrow> cslot_ptr \<Rightarrow> bool" 496where 497 "cap_removeable NullCap slot = True" 498| "cap_removeable (Zombie slot' bits n) slot = 499 ((n = 0) \<or> (n = 1 \<and> (slot', replicate (zombie_cte_bits bits) False) = slot))" 500 501text \<open>Checks for Zombie capabilities that refer to the CNode or TCB they are 502stored in.\<close> 503definition 504 cap_cyclic_zombie :: "cap \<Rightarrow> cslot_ptr \<Rightarrow> bool" where 505 "cap_cyclic_zombie cap slot \<equiv> case cap of 506 Zombie slot' bits n \<Rightarrow> (slot', replicate (zombie_cte_bits bits) False) = slot 507 | _ \<Rightarrow> False" 508 509text \<open>The complete recursive delete operation.\<close> 510function (sequential) 511 rec_del :: "rec_del_call \<Rightarrow> (bool * cap,'z::state_ext) p_monad" 512where 513 "rec_del (CTEDeleteCall slot exposed) s = 514 (doE 515 (success, cleanup_info) \<leftarrow> rec_del (FinaliseSlotCall slot exposed); 516 without_preemption $ when (exposed \<or> success) $ empty_slot slot cleanup_info; 517 returnOk undefined 518 odE) s" 519| 520 "rec_del (FinaliseSlotCall slot exposed) s = 521 (doE 522 cap \<leftarrow> without_preemption $ get_cap slot; 523 if (cap = NullCap) 524 then returnOk (True, NullCap) 525 else (doE 526 is_final \<leftarrow> without_preemption $ is_final_cap cap; 527 (remainder, cleanup_info) \<leftarrow> without_preemption $ finalise_cap cap is_final; 528 if (cap_removeable remainder slot) 529 then returnOk (True, cleanup_info) 530 else if (cap_cyclic_zombie remainder slot \<and> \<not> exposed) 531 then doE 532 without_preemption $ set_cap remainder slot; 533 returnOk (False, NullCap) 534 odE 535 else doE 536 without_preemption $ set_cap remainder slot; 537 rec_del (ReduceZombieCall remainder slot exposed); 538 preemption_point; 539 rec_del (FinaliseSlotCall slot exposed) 540 odE 541 odE) 542 odE) s" 543 544| "rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot False) s = 545 (doE 546 cn \<leftarrow> returnOk $ first_cslot_of (Zombie ptr bits (Suc n)); 547 assertE (cn \<noteq> slot); 548 without_preemption $ cap_swap_for_delete cn slot; 549 returnOk undefined 550 odE) s" 551| 552 "rec_del (ReduceZombieCall (Zombie ptr bits (Suc n)) slot True) s = 553 (doE 554 end_slot \<leftarrow> returnOk (ptr, nat_to_cref (zombie_cte_bits bits) n); 555 rec_del (CTEDeleteCall end_slot False); 556 new_cap \<leftarrow> without_preemption $ get_cap slot; 557 if (new_cap = Zombie ptr bits (Suc n)) 558 then without_preemption $ set_cap (Zombie ptr bits n) slot 559 else assertE (new_cap = NullCap \<or> 560 is_zombie new_cap \<and> first_cslot_of new_cap = slot 561 \<and> first_cslot_of (Zombie ptr bits (Suc n)) \<noteq> slot); 562 returnOk undefined 563 odE) s" 564| 565 "rec_del (ReduceZombieCall cap slot exposed) s = 566 fail s" 567 by pat_completeness auto 568 569text \<open>Delete a capability by calling the recursive delete operation.\<close> 570definition 571 cap_delete :: "cslot_ptr \<Rightarrow> (unit,'z::state_ext) p_monad" where 572 "cap_delete slot \<equiv> doE rec_del (CTEDeleteCall slot True); returnOk () odE" 573 574text \<open>Prepare the capability in a slot for deletion but do not delete it.\<close> 575definition 576 finalise_slot :: "cslot_ptr \<Rightarrow> bool \<Rightarrow> (bool * cap,'z::state_ext) p_monad" 577where 578 "finalise_slot p e \<equiv> rec_del (FinaliseSlotCall p e)" 579 580text \<open>Helper functions for the type of recursive delete calls.\<close> 581primrec 582 exposed_rdcall :: "rec_del_call \<Rightarrow> bool" 583where 584 "exposed_rdcall (CTEDeleteCall slot exposed) = exposed" 585| "exposed_rdcall (FinaliseSlotCall slot exposed) = exposed" 586| "exposed_rdcall (ReduceZombieCall cap slot exposed) = exposed" 587 588primrec 589 isCTEDeleteCall :: "rec_del_call \<Rightarrow> bool" 590where 591 "isCTEDeleteCall (CTEDeleteCall slot exposed) = True" 592| "isCTEDeleteCall (FinaliseSlotCall slot exposed) = False" 593| "isCTEDeleteCall (ReduceZombieCall cap slot exposed) = False" 594 595primrec 596 slot_rdcall :: "rec_del_call \<Rightarrow> cslot_ptr" 597where 598 "slot_rdcall (CTEDeleteCall slot exposed) = slot" 599| "slot_rdcall (FinaliseSlotCall slot exposed) = slot" 600| "slot_rdcall (ReduceZombieCall cap slot exposed) = slot" 601 602text \<open>Revoke the derived capabilities of a given capability, deleting them 603all.\<close> 604 605function cap_revoke :: "cslot_ptr \<Rightarrow> (unit,'z::state_ext) p_monad" 606where 607"cap_revoke slot s = (doE 608 cap \<leftarrow> without_preemption $ get_cap slot; 609 cdt \<leftarrow> without_preemption $ gets cdt; 610 descendants \<leftarrow> returnOk $ descendants_of slot cdt; 611 whenE (cap \<noteq> NullCap \<and> descendants \<noteq> {}) (doE 612 child \<leftarrow> without_preemption $ select_ext (next_revoke_cap slot) descendants; 613 cap \<leftarrow> without_preemption $ get_cap child; 614 assertE (cap \<noteq> NullCap); 615 cap_delete child; 616 preemption_point; 617 cap_revoke slot 618 odE) 619odE) s" 620by auto 621 622section \<open>Inserting and moving capabilities\<close> 623 624definition 625 get_badge :: "cap \<Rightarrow> badge option" where 626 "get_badge cap \<equiv> case cap of 627 NotificationCap oref badge cr \<Rightarrow> Some badge 628 | EndpointCap oref badge cr \<Rightarrow> Some badge 629 | _ \<Rightarrow> None" 630 631 632definition 633 is_physical :: "cap \<Rightarrow> bool" where 634 "is_physical cap \<equiv> case cap of 635 NullCap \<Rightarrow> False 636 | DomainCap \<Rightarrow> False 637 | IRQControlCap \<Rightarrow> False 638 | IRQHandlerCap _ \<Rightarrow> False 639 | ReplyCap _ _ _ \<Rightarrow> False 640 | ArchObjectCap c \<Rightarrow> arch_is_physical c 641 | _ \<Rightarrow> True" 642 643fun 644 same_region_as :: "cap \<Rightarrow> cap \<Rightarrow> bool" 645where 646 "same_region_as NullCap c' = False" 647| "same_region_as (UntypedCap dev r bits free) c' = 648 (is_physical c' \<and> 649 r \<le> obj_ref_of c' \<and> 650 obj_ref_of c' \<le> obj_ref_of c' + obj_size c' - 1 \<and> 651 obj_ref_of c' + obj_size c' - 1 \<le> r + (1 << bits) - 1)" 652| "same_region_as (EndpointCap r b R) c' = 653 (is_ep_cap c' \<and> obj_ref_of c' = r)" 654| "same_region_as (NotificationCap r b R) c' = 655 (is_ntfn_cap c' \<and> obj_ref_of c' = r)" 656| "same_region_as (CNodeCap r bits g) c' = 657 (is_cnode_cap c' \<and> obj_ref_of c' = r \<and> bits_of c' = bits)" 658| "same_region_as (ReplyCap n m cr) c' = (\<exists>m' cr. c' = ReplyCap n m' cr)" 659| "same_region_as (ThreadCap r) c' = 660 (is_thread_cap c' \<and> obj_ref_of c' = r)" 661| "same_region_as (Zombie r b n) c' = False" 662| "same_region_as (IRQControlCap) c' = 663 (c' = IRQControlCap \<or> (\<exists>n. c' = IRQHandlerCap n))" 664| "same_region_as DomainCap c' = (c' = DomainCap)" 665| "same_region_as (IRQHandlerCap n) c' = 666 (c' = IRQHandlerCap n)" 667| "same_region_as (ArchObjectCap a) c' = 668 (case c' of ArchObjectCap a' \<Rightarrow> arch_same_region_as a a' | _ \<Rightarrow> False)" 669 670text \<open>Check whether two capabilities are to the same object.\<close> 671definition 672 same_object_as :: "cap \<Rightarrow> cap \<Rightarrow> bool" where 673 "same_object_as cp cp' \<equiv> 674 (case (cp, cp') of 675 (UntypedCap dev r bits free, _) \<Rightarrow> False 676 | (IRQControlCap, IRQHandlerCap n) \<Rightarrow> False 677 | (ArchObjectCap ac, ArchObjectCap ac') \<Rightarrow> same_aobject_as ac ac' 678 | _ \<Rightarrow> same_region_as cp cp')" 679 680 681 682text \<open> 683The function @{text "should_be_parent_of"} 684checks whether an existing capability should be a parent of 685another to-be-inserted capability. The test is the following: 686For capability @{term c} to be a parent of capability @{term c'}, 687@{term c} needs to be the original capability to the object and needs 688to cover the same memory region as @{term c'} (i.e.\ cover the same 689object). In the case of endpoint capabilities, if @{term c} is a 690badged endpoint cap (@{text "badge \<noteq> 0"}), then it should be a parent 691of @{text c'} if @{text c'} has the same badge and is itself not an 692original badged endpoint cap. 693 694\begin{figure} 695\begin{center} 696\includegraphics[width=0.8\textwidth]{imgs/CDT} 697\end{center} 698\caption{Example capability derivation tree.}\label{fig:CDT} 699\end{figure} 700 701Figure \ref{fig:CDT} shows an example capability derivation tree that 702illustrates a standard scenario: the top level is a large untyped 703capability, the second level splits this capability into two regions 704covered by their own untyped caps, both are children of the first 705level. The third level on the left is a copy of the level 2 untyped 706capability. Untyped capabilities when copied always create children, 707never siblings. In this scenario, the untyped capability was typed 708into two separate objects, creating two capabilities on level 4, both 709are the original capability to the respective object, both are 710children of the untyped capability they were created from. 711 712 Ordinary original capabilities can have one level of derived capabilities 713(created, for instance, by the copy or mint operations). Further copies 714of these derived capabilities will create sibling, in this case 715remaining on level 5. There is an exception to this scheme for endpoint 716capabilities --- they support an additional layer of depth with the 717concept of badged and unbadged endpoints. The original endpoint 718capability will be unbadged. Using the mint operation, a copy of 719the capability with a specific badge can be created. This new, badged 720capability to the same object is treated as an original capability 721(the ``original badged endpoint capability'') and supports one level 722of derived children like other capabilities. 723\<close> 724definition 725 should_be_parent_of :: "cap \<Rightarrow> bool \<Rightarrow> cap \<Rightarrow> bool \<Rightarrow> bool" where 726 "should_be_parent_of c original c' original' \<equiv> 727 original \<and> 728 same_region_as c c' \<and> 729 (case c of 730 EndpointCap ref badge R \<Rightarrow> badge \<noteq> 0 \<longrightarrow> cap_ep_badge c' = badge \<and> \<not>original' 731 | NotificationCap ref badge R \<Rightarrow> badge \<noteq> 0 \<longrightarrow> cap_ep_badge c' = badge \<and> \<not>original' 732 | _ \<Rightarrow> True)" 733 734text \<open>This helper function determines if the new capability 735should be counted as the original capability to the object. This test 736is usually false, apart from the exceptions listed (newly badged 737endpoint capabilities, irq handlers, untyped caps, and possibly some 738arch caps).\<close> 739definition 740 is_cap_revocable :: "cap \<Rightarrow> cap \<Rightarrow> bool" 741where 742 "is_cap_revocable new_cap src_cap \<equiv> case new_cap of 743 ArchObjectCap acap \<Rightarrow> arch_is_cap_revocable new_cap src_cap 744 | EndpointCap _ _ _ \<Rightarrow> cap_ep_badge new_cap \<noteq> cap_ep_badge src_cap 745 | NotificationCap _ _ _ \<Rightarrow> cap_ep_badge new_cap \<noteq> cap_ep_badge src_cap 746 | IRQHandlerCap _ \<Rightarrow> src_cap = IRQControlCap 747 | UntypedCap _ _ _ _ \<Rightarrow> True 748 | _ \<Rightarrow> False" 749 750text \<open>Insert a new capability as either a sibling or child of an 751existing capability. The function @{const should_be_parent_of} 752determines which it will be. 753 754The term for @{text dest_original} determines if the new capability 755should be counted as the original capability to the object. This test 756is usually false, apart from the exceptions listed (newly badged 757endpoint capabilities, irq handlers, and untyped caps). 758\<close> 759 760 761definition 762 cap_insert :: "cap \<Rightarrow> cslot_ptr \<Rightarrow> cslot_ptr \<Rightarrow> (unit,'z::state_ext) s_monad" where 763 "cap_insert new_cap src_slot dest_slot \<equiv> do 764 src_cap \<leftarrow> get_cap src_slot; 765 766 dest_original \<leftarrow> return $ is_cap_revocable new_cap src_cap; 767 768 old_cap \<leftarrow> get_cap dest_slot; 769 assert (old_cap = NullCap); 770 set_untyped_cap_as_full src_cap new_cap src_slot; 771 set_cap new_cap dest_slot; 772 773 is_original \<leftarrow> gets is_original_cap; 774 src_parent \<leftarrow> return $ 775 should_be_parent_of src_cap (is_original src_slot) new_cap dest_original; 776 src_p \<leftarrow> gets (\<lambda>s. cdt s src_slot); 777 dest_p \<leftarrow> gets (\<lambda>s. cdt s dest_slot); 778 update_cdt (\<lambda>cdt. cdt (dest_slot := if src_parent 779 then Some src_slot 780 else cdt src_slot)); 781 do_extended_op (cap_insert_ext src_parent src_slot dest_slot src_p dest_p); 782 set_original dest_slot dest_original 783 od" 784 785 786definition 787 has_cancel_send_rights :: "cap \<Rightarrow> bool" where 788 "has_cancel_send_rights cap \<equiv> case cap of 789 EndpointCap _ _ R \<Rightarrow> R = all_rights 790 | _ \<Rightarrow> False" 791 792text \<open>Overwrite the capabilities stored in a TCB while preserving the register 793set and other fields.\<close> 794definition 795 tcb_registers_caps_merge :: "tcb \<Rightarrow> tcb \<Rightarrow> tcb" 796where 797 "tcb_registers_caps_merge regtcb captcb \<equiv> 798 regtcb \<lparr> tcb_ctable := tcb_ctable captcb, 799 tcb_vtable := tcb_vtable captcb, 800 tcb_reply := tcb_reply captcb, 801 tcb_caller := tcb_caller captcb, 802 tcb_ipcframe := tcb_ipcframe captcb \<rparr>" 803 804section \<open>Invoking CNode capabilities\<close> 805 806text \<open>The CNode capability confers authority to various methods 807which act on CNodes and the capabilities within them. Copies of 808capabilities may be inserted in empty CNode slots by 809Insert. Capabilities may be moved to empty slots with Move or swapped 810with others in a three way rotate by Rotate. A Reply capability stored 811in a thread's last-caller slot may be saved into a regular CNode slot 812with Save. The Revoke, Delete and Recycle methods may also be 813invoked on the capabilities stored in the CNode.\<close> 814 815definition 816 invoke_cnode :: "cnode_invocation \<Rightarrow> (unit,'z::state_ext) p_monad" where 817 "invoke_cnode i \<equiv> case i of 818 RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot 819 | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot 820 | InsertCall cap src_slot dest_slot \<Rightarrow> 821 without_preemption $ cap_insert cap src_slot dest_slot 822 | MoveCall cap src_slot dest_slot \<Rightarrow> 823 without_preemption $ cap_move cap src_slot dest_slot 824 | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> 825 without_preemption $ 826 if slot1 = slot3 then 827 cap_swap cap1 slot1 cap2 slot2 828 else 829 do cap_move cap2 slot2 slot3; cap_move cap1 slot1 slot2 od 830 | SaveCall slot \<Rightarrow> without_preemption $ do 831 thread \<leftarrow> gets cur_thread; 832 src_slot \<leftarrow> return (thread, tcb_cnode_index 3); 833 cap \<leftarrow> get_cap src_slot; 834 (case cap of 835 NullCap \<Rightarrow> return () 836 | ReplyCap _ False _ \<Rightarrow> cap_move cap src_slot slot 837 | _ \<Rightarrow> fail) od 838 | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> 839 without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b 840 | CancelBadgedSendsCall _ \<Rightarrow> fail" 841 842 843section "Cap classification used to define invariants" 844 845datatype capclass = 846 PhysicalClass | ReplyClass "obj_ref" | IRQClass | ASIDMasterClass | NullClass | DomainClass | IOPortClass 847 848end 849