1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 *) 6 7theory Tcb_AC 8imports Finalise_AC 9begin 10 11context begin interpretation Arch . (*FIXME: arch_split*) 12 13(* FIXME-NTFN: The 'NotificationControl' case of the following definition needs to be changed. *) 14 15definition 16 authorised_tcb_inv :: "'a PAS \<Rightarrow> Invocations_A.tcb_invocation \<Rightarrow> bool" 17where 18 "authorised_tcb_inv aag ti \<equiv> case ti of 19 tcb_invocation.Suspend t \<Rightarrow> is_subject aag t 20 | tcb_invocation.Resume t \<Rightarrow> is_subject aag t 21 | tcb_invocation.ThreadControl t sl ep mcp priority croot vroot buf 22 \<Rightarrow> is_subject aag t \<and> 23 (\<forall>(cap, slot) \<in> (set_option croot \<union> set_option vroot \<union> 24 (case_option {} (set_option \<circ> snd) buf)). 25 pas_cap_cur_auth aag cap \<and> is_subject aag (fst slot)) 26 | tcb_invocation.NotificationControl t ntfn \<Rightarrow> is_subject aag t \<and> 27 case_option True (\<lambda>a. \<forall>auth \<in> {Receive, Reset}. 28 (pasSubject aag, auth, pasObjectAbs aag a) \<in> pasPolicy aag) ntfn 29 | tcb_invocation.ReadRegisters src susp n arch \<Rightarrow> is_subject aag src 30 | tcb_invocation.WriteRegisters dest res values arch \<Rightarrow> is_subject aag dest 31 | tcb_invocation.CopyRegisters dest src susp res frame int_regs arch \<Rightarrow> 32 is_subject aag src \<and> is_subject aag dest 33 | tcb_invocation.SetTLSBase tcb tls_base \<Rightarrow> is_subject aag tcb" 34 35subsection\<open>invoke\<close> 36 37lemma setup_reply_master_respects: 38 "\<lbrace>integrity aag X st and K (is_subject aag t)\<rbrace> 39 setup_reply_master t 40 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 41 apply (simp add: setup_reply_master_def) 42 apply (wp get_cap_wp set_cap_integrity_autarch[unfolded K_def pred_conj_def] 43 set_original_integrity_autarch)+ 44 apply simp 45 done 46 47crunch eintegrity[wp]: possible_switch_to "integrity aag X st" 48 (ignore: tcb_sched_action) 49 50lemma restart_integrity_autarch: 51 "\<lbrace>integrity aag X st and K (is_subject aag t) and einvs 52 and tcb_at t 53 and pas_refined aag\<rbrace> 54 restart t 55 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 56 apply (simp add: restart_def) 57 apply (wp set_thread_state_integrity_autarch setup_reply_master_respects 58 hoare_drop_imps 59 | simp add: if_apply_def2)+ 60 done 61 62crunch integrity_autarch: option_update_thread "integrity aag X st" 63 64crunch arch_state [wp]: cap_swap_for_delete "\<lambda>s. P (arch_state s)" 65 66lemma schematic_lift_tuple3_l: 67 "P (fst (a, b, c)) (fst (snd (a, b, c))) (snd (snd (a, b, c))) \<and> Q \<Longrightarrow> P a b c" by simp 68 69lemma schematic_lift_tuple3_r: 70 "Q \<and> P (fst (a, b, c)) (fst (snd (a, b, c))) (snd (snd (a, b, c))) \<Longrightarrow> P a b c" by simp 71 72(* FIXME: MOVE *) 73lemma invoke_tcb_cases: 74 "invoke_tcb ti = (case ti of 75 tcb_invocation.Suspend t \<Rightarrow> invoke_tcb (tcb_invocation.Suspend t) 76 | tcb_invocation.Resume t \<Rightarrow> invoke_tcb (tcb_invocation.Resume t) 77 | tcb_invocation.ThreadControl t sl ep mcp priority croot vroot buf \<Rightarrow> 78 invoke_tcb (tcb_invocation.ThreadControl t sl ep mcp priority croot vroot buf) 79 | tcb_invocation.NotificationControl t ntfn \<Rightarrow> 80 invoke_tcb (tcb_invocation.NotificationControl t ntfn) 81 | tcb_invocation.ReadRegisters src susp n arch \<Rightarrow> 82 invoke_tcb (tcb_invocation.ReadRegisters src susp n arch) 83 | tcb_invocation.WriteRegisters dest res values arch \<Rightarrow> 84 invoke_tcb (tcb_invocation.WriteRegisters dest res values arch) 85 | tcb_invocation.CopyRegisters dest src susp res frame int_regs arch \<Rightarrow> 86 invoke_tcb (tcb_invocation.CopyRegisters dest src susp res frame int_regs arch) 87 | tcb_invocation.SetTLSBase tcb tls_base \<Rightarrow> invoke_tcb (tcb_invocation.SetTLSBase tcb tls_base))" 88 by (cases ti, simp_all) 89 90lemmas itr_wps = restart_integrity_autarch as_user_integrity_autarch thread_set_integrity_autarch 91 option_update_thread_integrity_autarch thread_set_pas_refined 92 cap_insert_integrity_autarch cap_insert_pas_refined 93 hoare_vcg_all_liftE hoare_weak_lift_impE hoare_weak_lift_imp hoare_vcg_all_lift 94 check_cap_inv[where P="valid_cap c" for c] 95 check_cap_inv[where P="tcb_cap_valid c p" for c p] 96 check_cap_inv[where P="cte_at p0" for p0] 97 check_cap_inv[where P="tcb_at p0" for p0] 98 check_cap_inv[where P="ex_cte_cap_wp_to P p" for P p] 99 check_cap_inv[where P="ex_nonz_cap_to p" for p] 100 check_cap_inv2[where Q="\<lambda>_. integrity aag X st" for aag X st] 101 check_cap_inv2[where Q="\<lambda>_. pas_refined aag" for aag] 102 checked_insert_no_cap_to cap_insert_ex_cap 103 cap_delete_valid_cap cap_delete_deletes 104 hoare_case_option_wp thread_set_valid_cap 105 thread_set_tcb_ipc_buffer_cap_cleared_invs 106 thread_set_invs_trivial[OF ball_tcb_cap_casesI] 107 thread_set_cte_wp_at_trivial[where Q="\<lambda>x. x", OF ball_tcb_cap_casesI] 108 thread_set_no_cap_to_trivial[OF ball_tcb_cap_casesI] 109 110(*FIXME MOVE *) 111 112lemma aag_cap_auth_master_Reply: 113 "\<lbrakk>pas_refined aag s ; AllowGrant \<in> R\<rbrakk> 114 \<Longrightarrow> pas_cap_cur_auth aag (cap.ReplyCap tcb True R) = is_subject aag tcb" 115 unfolding aag_cap_auth_def 116 by (fastforce intro: aag_wellformed_refl aag_wellformed_control_is_owns[THEN iffD1] 117 simp: pas_refined_def cli_no_irqs clas_no_asid cap_auth_conferred_def 118 reply_cap_rights_to_auth_def) 119 120 121 122(* FIXME MOVE *) 123lemma cdt_NullCap: 124 "valid_mdb s \<Longrightarrow> caps_of_state s src = Some NullCap \<Longrightarrow> cdt s src = None" 125 by (rule ccontr) (force dest: mdb_cte_atD simp: valid_mdb_def2) 126 127 128lemma setup_reply_master_pas_refined: 129 "\<lbrace>pas_refined aag and valid_mdb and K (is_subject aag t)\<rbrace> 130 setup_reply_master t 131 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 132 apply (simp add: setup_reply_master_def) 133 apply (wp get_cap_wp set_cap_pas_refined set_original_wp)+ 134 by (force dest: cdt_NullCap simp: aag_cap_auth_master_Reply cte_wp_at_caps_of_state) 135 136crunches possible_switch_to 137 for tcb_domain_map_wellformed[wp]: " tcb_domain_map_wellformed aag" 138 139lemma restart_pas_refined: 140 "\<lbrace>pas_refined aag and invs and tcb_at t and K (is_subject aag t)\<rbrace> restart t \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 141 apply (simp add: restart_def get_thread_state_def) 142 apply (wp set_thread_state_pas_refined setup_reply_master_pas_refined thread_get_wp' 143 | strengthen invs_mdb 144 | simp)+ 145 done 146 147lemma option_update_thread_set_safe_lift: 148 "\<lbrakk> \<And>v. \<lbrace>P\<rbrace> thread_set (f v) t \<lbrace>\<lambda>rv. P\<rbrace> \<rbrakk> 149 \<Longrightarrow> \<lbrace>P\<rbrace> option_update_thread t f v \<lbrace>\<lambda>rv. P\<rbrace>" 150 by (simp add: option_update_thread_def split: option.split) 151 152lemmas option_update_thread_pas_refined 153 = option_update_thread_set_safe_lift [OF thread_set_pas_refined] 154 155crunch integrity_autarch[wp]: thread_set_priority "integrity aag X st" 156 (ignore: tcb_sched_action) 157 158lemma set_priority_integrity_autarch[wp]: 159 "\<lbrace>integrity aag X st and pas_refined aag and K (is_subject aag tptr)\<rbrace> 160 set_priority tptr prio \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" 161 by (simp add: set_priority_def | wp)+ 162 163lemma set_priority_pas_refined[wp]: 164 "\<lbrace>pas_refined aag\<rbrace> 165 set_priority tptr prio \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" 166 apply (simp add: set_priority_def thread_set_priority_def ethread_set_def set_eobject_def get_etcb_def 167 | wp hoare_vcg_imp_lift')+ 168 apply (simp add: tcb_sched_action_def | wp)+ 169 apply (clarsimp simp: etcb_at_def pas_refined_def tcb_domain_map_wellformed_aux_def 170 split: option.splits) 171 apply (erule_tac x="(a, b)" in ballE) 172 apply simp 173 apply (erule domains_of_state_aux.cases) 174 apply (force intro: domtcbs split: if_split_asm) 175 done 176 177lemma gts_test[wp]: "\<lbrace>\<top>\<rbrace> get_thread_state t \<lbrace>\<lambda>rv s. test rv = st_tcb_at test t s\<rbrace>" 178 apply (simp add: get_thread_state_def thread_get_def) 179 apply wp 180 apply (clarsimp simp add: st_tcb_def2) 181 done 182 183crunch exst[wp]: option_update_thread "\<lambda>s. P (exst s)" 184 185lemma out_valid_sched: "(\<And>x a. tcb_state (f a x) = tcb_state x) \<Longrightarrow> 186 \<lbrace>valid_sched\<rbrace> option_update_thread tptr f v \<lbrace>\<lambda>rv. valid_sched\<rbrace>" 187 apply (simp add: option_update_thread_def) 188 apply (rule hoare_pre) 189 apply (wp thread_set_not_state_valid_sched | wpc | simp)+ 190 done 191 192 193definition "safe_id x \<equiv> x" 194 195lemma use_safe_id: "safe_id x \<Longrightarrow> x" 196 by (simp add: safe_id_def) 197 198lemma simplify_post: 199 "\<lbrakk>\<And>r s. x r s \<Longrightarrow> safe_id (Q' r s) \<Longrightarrow> Q r s; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. x r s \<and> Q' r s\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> 200 \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 201 apply (rule hoare_post_impErr) 202 apply assumption 203 apply (clarsimp simp add: safe_id_def)+ 204 done 205 206end 207 208lemma (in is_extended') valid_cap_syn[wp]: "I (\<lambda>s. valid_cap_syn s a)" by (rule lift_inv,simp) 209 210lemma (in is_extended') no_cap_to_obj_dr_emp[wp]: "I (no_cap_to_obj_dr_emp a)" by (rule lift_inv,simp) 211 212lemma (in is_extended') cte_wp_at[wp]: "I (cte_wp_at P a)" by (rule lift_inv,simp) 213 214crunch pas_refined[wp]: set_mcpriority "pas_refined aag" 215 216crunch integrity_autarch: set_mcpriority "integrity aag X st" 217 218context begin interpretation Arch . (*FIXME: arch_split*) 219 220lemma checked_insert_pas_refined: 221 "\<lbrace>pas_refined aag and valid_mdb and 222 K(\<not> is_master_reply_cap new_cap \<and> is_subject aag target \<and> 223 is_subject aag (fst src_slot) \<and> pas_cap_cur_auth aag new_cap)\<rbrace> 224 check_cap_at new_cap src_slot ( 225 check_cap_at (ThreadCap target) slot( 226 cap_insert new_cap src_slot (target, ref))) 227 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 228 apply (unfold check_cap_at_def) 229 apply (wp cap_insert_pas_refined_same_object_as get_cap_wp) 230 by (fastforce simp:cte_wp_at_caps_of_state) 231 232(* FIXME MOVE *) 233lemma update_cdt_wp: 234 "\<lbrace>\<lambda>s. P (s\<lparr>cdt := m (cdt s)\<rparr>)\<rbrace> update_cdt m \<lbrace>\<lambda>_. P\<rbrace>" 235 by (simp add: update_cdt_def set_cdt_def) wp 236 237(* FIXME MOVE *) 238lemma parent_ofD: "m \<Turnstile> src \<leadsto> x \<Longrightarrow> m x = Some src" 239 by (simp add: cdt_parent_of_def) 240 241 242crunch tcb_states_of_state[wp]: set_untyped_cap_as_full "\<lambda>s. P (tcb_states_of_state s)" 243 244 245(* FIXME MOVE *) 246lemma map_le_to_rtrancl: 247 "m \<subseteq>\<^sub>m m' \<Longrightarrow> m \<Turnstile> pptr \<rightarrow>* ptr \<Longrightarrow> m' \<Turnstile> pptr \<rightarrow>* ptr" 248 apply (erule subsetD[rotated]) 249 apply (rule rtrancl_mono) 250 apply (fastforce simp:cdt_parent_of_def map_le_def dom_def) 251 done 252 253lemma map_le_to_cca: 254 "m \<subseteq>\<^sub>m m' \<Longrightarrow> cdt_change_allowed aag subjects m tcbsts ptr 255 \<Longrightarrow> cdt_change_allowed aag subjects m' tcbsts ptr" 256 apply (elim cdt_change_allowedE cdt_change_allowedI[rotated]) 257 by (rule map_le_to_rtrancl) 258 259lemma cap_insert_cdt_change_allowed[wp]: 260 "\<lbrace> valid_mdb and cdt_change_allowed' aag slot\<rbrace> 261 cap_insert new_cap src_slot dest_slot 262 \<lbrace>\<lambda>_. cdt_change_allowed' aag slot \<rbrace>" 263 apply (rule hoare_pre, unfold cap_insert_def) 264 apply (wp add: dxo_wp_weak update_cdt_wp | simp)+ 265 apply (rule hoare_post_imp[of 266 "\<lambda>_. cdt_change_allowed' aag slot and (\<lambda>s. cdt s dest_slot = None)"]) 267 apply (fastforce elim: map_le_to_cca[rotated] simp:map_le_def dom_def) 268 apply (wps|wp get_cap_wp)+ 269 apply (clarsimp) 270 apply (drule valid_mdb_mdb_cte_at) 271 apply (subst not_Some_eq[symmetric]) 272 apply (intro allI notI) 273 apply (drule(1) mdb_cte_atD[rotated]) 274 apply (simp add:cte_wp_at_caps_of_state) 275 done 276 277 278lemma invoke_tcb_tc_respects_aag: 279 "\<lbrace> integrity aag X st and pas_refined aag 280 and einvs and simple_sched_action 281 and tcb_inv_wf (ThreadControl t sl ep mcp priority croot vroot buf) 282 and K (authorised_tcb_inv aag (ThreadControl t sl ep mcp priority croot vroot buf))\<rbrace> 283 invoke_tcb (ThreadControl t sl ep mcp priority croot vroot buf) 284 \<lbrace>\<lambda>rv. integrity aag X st and pas_refined aag\<rbrace>" 285 apply (rule hoare_gen_asm)+ 286 apply (subst invoke_tcb.simps) 287 apply (subst set_priority_extended.dxo_eq) 288 apply (rule hoare_vcg_precond_imp) 289 apply (rule_tac P="case ep of Some v \<Rightarrow> length v = word_bits | _ \<Rightarrow> True" 290 in hoare_gen_asm) 291 apply (simp only: split_def) 292 apply ((simp add: conj_comms del: hoare_True_E_R, 293 strengthen imp_consequent[where Q="x = None" for x], simp cong: conj_cong) 294 | rule wp_split_const_if wp_split_const_if_R 295 hoare_vcg_all_lift_R 296 hoare_vcg_E_elim hoare_vcg_const_imp_lift_R 297 hoare_vcg_R_conj 298 | wp 299 restart_integrity_autarch set_mcpriority_integrity_autarch 300 as_user_integrity_autarch thread_set_integrity_autarch 301 option_update_thread_integrity_autarch 302 out_valid_sched static_imp_wp 303 cap_insert_integrity_autarch checked_insert_pas_refined 304 cap_delete_respects' cap_delete_pas_refined' 305 check_cap_inv2[where Q="\<lambda>_. integrity aag X st"] 306 as_user_pas_refined restart_pas_refined 307 thread_set_pas_refined 308 option_update_thread_pas_refined 309 out_invs_trivial case_option_wpE cap_delete_deletes 310 cap_delete_valid_cap cap_insert_valid_cap out_cte_at 311 cap_insert_cte_at cap_delete_cte_at out_valid_cap out_tcb_valid 312 hoare_vcg_const_imp_lift_R hoare_vcg_all_lift_R 313 thread_set_tcb_ipc_buffer_cap_cleared_invs 314 thread_set_invs_trivial[OF ball_tcb_cap_casesI] 315 hoare_vcg_all_lift thread_set_valid_cap out_emptyable 316 check_cap_inv[where P="valid_cap c" for c] 317 check_cap_inv[where P="tcb_cap_valid c p" for c p] 318 check_cap_inv[where P="cte_at p0" for p0] 319 check_cap_inv[where P="tcb_at p0" for p0] 320 check_cap_inv[where P="simple_sched_action"] 321 check_cap_inv[where P="valid_list"] 322 check_cap_inv[where P="valid_sched"] 323 thread_set_cte_at 324 thread_set_cte_wp_at_trivial[where Q="\<lambda>x. x", OF ball_tcb_cap_casesI] 325 thread_set_no_cap_to_trivial[OF ball_tcb_cap_casesI] 326 checked_insert_no_cap_to 327 out_no_cap_to_trivial[OF ball_tcb_cap_casesI] 328 thread_set_ipc_tcb_cap_valid 329 cap_delete_pas_refined'[THEN valid_validE_E] thread_set_cte_wp_at_trivial 330 | simp add: ran_tcb_cap_cases dom_tcb_cap_cases[simplified] 331 emptyable_def a_type_def partial_inv_def 332 del: hoare_True_E_R 333 | wpc 334 | strengthen invs_mdb use_no_cap_to_obj_asid_strg 335 tcb_cap_always_valid_strg[where p="tcb_cnode_index 0"] 336 tcb_cap_always_valid_strg[where p="tcb_cnode_index (Suc 0)"] 337 )+ 338 apply (clarsimp simp: authorised_tcb_inv_def) 339 apply (clarsimp simp: tcb_at_cte_at_0 tcb_at_cte_at_1[simplified] 340 is_cap_simps is_valid_vtable_root_def 341 is_cnode_or_valid_arch_def tcb_cap_valid_def 342 tcb_at_st_tcb_at[symmetric] invs_valid_objs 343 cap_asid_def vs_cap_ref_def 344 clas_no_asid cli_no_irqs 345 emptyable_def 346 | rule conjI | erule pas_refined_refl)+ 347 done 348 349lemma invoke_tcb_unbind_notification_respects: 350 "\<lbrace>integrity aag X st and pas_refined aag and simple_sched_action 351 and einvs and Tcb_AI.tcb_inv_wf (tcb_invocation.NotificationControl t None) 352 and K (authorised_tcb_inv aag (tcb_invocation.NotificationControl t None))\<rbrace> 353 invoke_tcb (tcb_invocation.NotificationControl t None) 354 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 355 apply (clarsimp) 356 apply (wp unbind_notification_respects) 357 apply (clarsimp simp: authorised_tcb_inv_def tcb_at_def pred_tcb_def2) 358 apply (clarsimp split: option.split) 359 apply (frule(1) bound_tcb_at_implies_reset[unfolded pred_tcb_def2, OF _ exI, OF _ conjI]) 360 apply simp 361 apply simp 362 done 363 364lemma sbn_bind_respects: 365 "\<lbrace>integrity aag X st and bound_tcb_at ((=) None) t 366 and K ((pasSubject aag, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag \<and> is_subject aag t)\<rbrace> 367 set_bound_notification t (Some ntfn) 368 \<lbrace>\<lambda>rv. integrity aag X st \<rbrace>" 369 apply (simp add: set_bound_notification_def) 370 apply (wpsimp wp: set_object_wp) 371 apply (erule integrity_trans) 372 apply (clarsimp simp: integrity_def obj_at_def pred_tcb_at_def) 373 done 374 375 376lemma bind_notification_respects: 377 "\<lbrace>integrity aag X st and pas_refined aag and bound_tcb_at ((=) None) t 378 and K ((pasSubject aag, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> 379 is_subject aag t)\<rbrace> 380 bind_notification t ntfnptr 381 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 382 apply (rule hoare_gen_asm) 383 apply (clarsimp simp: bind_notification_def) 384 apply (rule hoare_seq_ext[OF _ get_simple_ko_sp]) 385 apply (wp set_ntfn_respects hoare_vcg_imp_lift sbn_bind_respects | wpc | clarsimp)+ 386 apply fastforce 387 done 388 389lemma invoke_tcb_bind_notification_respects: 390 "\<lbrace>integrity aag X st and pas_refined aag 391 and einvs and Tcb_AI.tcb_inv_wf (tcb_invocation.NotificationControl t (Some ntfn)) 392 and simple_sched_action 393 and K (authorised_tcb_inv aag (tcb_invocation.NotificationControl t (Some ntfn)))\<rbrace> 394 invoke_tcb (tcb_invocation.NotificationControl t (Some ntfn)) 395 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 396 apply (rule hoare_gen_asm) 397 apply (clarsimp) 398 apply (wp bind_notification_respects) 399 apply (clarsimp simp: authorised_tcb_inv_def) 400 done 401 402lemma invoke_tcb_ntfn_control_respects[wp]: 403 "\<lbrace>integrity aag X st and pas_refined aag 404 and einvs and Tcb_AI.tcb_inv_wf (tcb_invocation.NotificationControl t ntfn) 405 and simple_sched_action 406 and K (authorised_tcb_inv aag (tcb_invocation.NotificationControl t ntfn))\<rbrace> 407 invoke_tcb (tcb_invocation.NotificationControl t ntfn) 408 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 409 apply (case_tac ntfn, simp_all del: invoke_tcb.simps Tcb_AI.tcb_inv_wf.simps K_def) 410 apply (wp invoke_tcb_bind_notification_respects invoke_tcb_unbind_notification_respects | simp)+ 411 done 412 413lemma invoke_tcb_respects: 414 "\<lbrace>integrity aag X st and pas_refined aag 415 and einvs and simple_sched_action and Tcb_AI.tcb_inv_wf ti 416 and K (authorised_tcb_inv aag ti)\<rbrace> 417 invoke_tcb ti 418 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 419 apply (cases ti, simp_all add: hoare_conjD1 [OF invoke_tcb_tc_respects_aag [simplified simp_thms]] 420 del: invoke_tcb.simps Tcb_AI.tcb_inv_wf.simps K_def) 421 apply (safe intro!: hoare_gen_asm) 422 apply ((wp itr_wps mapM_x_wp' | simp add: if_apply_def2 split del: if_split 423 | wpc | clarsimp simp: authorised_tcb_inv_def arch_get_sanitise_register_info_def 424 | rule conjI | subst(asm) idle_no_ex_cap)+) 425 done 426 427subsubsection\<open>@{term "pas_refined"}\<close> 428 429lemmas ita_wps = as_user_pas_refined restart_pas_refined cap_insert_pas_refined 430 thread_set_pas_refined cap_delete_pas_refined' check_cap_inv2 hoare_vcg_all_liftE 431 hoare_weak_lift_impE hoare_weak_lift_imp hoare_vcg_all_lift 432 433lemma hoare_st_refl: 434 "\<lbrakk>\<And>st. \<lbrace>P st\<rbrace> f \<lbrace>Q st\<rbrace>; \<And>r s st. Q st r s \<Longrightarrow> Q' r s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s s\<rbrace> f \<lbrace>Q'\<rbrace>" 435 apply (clarsimp simp add: valid_def) 436 apply (drule_tac x=s in meta_spec) 437 apply force 438 done 439 440lemma bind_notification_pas_refined[wp]: 441 "\<lbrace>pas_refined aag 442 and K (\<forall>auth \<in> {Receive, Reset}. 443 (pasObjectAbs aag t, auth, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag)\<rbrace> 444 bind_notification t ntfnptr 445 \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" 446 apply (clarsimp simp: bind_notification_def) 447 apply (wp set_simple_ko_pas_refined | wpc | simp)+ 448 done 449 450lemma invoke_tcb_ntfn_control_pas_refined[wp]: 451 "\<lbrace>pas_refined aag and Tcb_AI.tcb_inv_wf (tcb_invocation.NotificationControl t ntfn) 452 and einvs and simple_sched_action 453 and K (authorised_tcb_inv aag (tcb_invocation.NotificationControl t ntfn))\<rbrace> 454 invoke_tcb (tcb_invocation.NotificationControl t ntfn) 455 \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" 456 apply (case_tac ntfn, simp_all del: K_def) 457 apply (safe intro!: hoare_gen_asm) 458 apply (wp | simp add: authorised_tcb_inv_def)+ 459 done 460 461lemma invoke_tcb_pas_refined: 462 "\<lbrace>pas_refined aag and Tcb_AI.tcb_inv_wf ti and einvs and simple_sched_action 463 and K (authorised_tcb_inv aag ti)\<rbrace> 464 invoke_tcb ti 465 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 466 apply (cases "\<exists>t sl ep mcp priority croot vroot buf. 467 ti = tcb_invocation.ThreadControl t sl ep mcp priority croot vroot buf") 468 apply safe 469 apply (rule hoare_chain, rule_tac Q'="\<lambda>_. pas_refined aag" and st1="\<lambda>x. x" in 470 hoare_st_refl[OF invoke_tcb_tc_respects_aag]) 471 apply force 472 apply fastforce 473 apply assumption 474 apply (rule hoare_gen_asm) 475 apply (cases ti, simp_all add: authorised_tcb_inv_def) 476 apply (wp ita_wps hoare_drop_imps mapM_x_wp' 477 | simp add: emptyable_def if_apply_def2 authorised_tcb_inv_def 478 arch_get_sanitise_register_info_def 479 | rule ball_tcb_cap_casesI 480 | wpc 481 | fastforce intro: notE[rotated,OF idle_no_ex_cap,simplified] 482 simp: invs_valid_global_refs invs_valid_objs)+ 483 done 484 485subsection\<open>TCB / decode\<close> 486 487lemma decode_registers_authorised: 488 "\<lbrace>K (is_subject aag t)\<rbrace> decode_read_registers msg (cap.ThreadCap t) \<lbrace>\<lambda>rv s. authorised_tcb_inv aag rv\<rbrace>, -" 489 "\<lbrace>K (is_subject aag t)\<rbrace> decode_write_registers msg (cap.ThreadCap t) \<lbrace>\<lambda>rv s. authorised_tcb_inv aag rv\<rbrace>, -" 490 "\<lbrace>pas_refined aag and K (is_subject aag t \<and> (\<forall>(cap, slot) \<in> set excaps. pas_cap_cur_auth aag cap \<and> is_subject aag (fst slot)))\<rbrace> 491 decode_copy_registers msg (cap.ThreadCap t) (map fst excaps) 492 \<lbrace>\<lambda>rv s. authorised_tcb_inv aag rv\<rbrace>, -" 493 unfolding decode_read_registers_def decode_write_registers_def decode_copy_registers_def authorised_tcb_inv_def 494 by (rule hoare_pre, simp cong: list.case_cong, (wp | wpc)+, clarsimp simp: cap_auth_conferred_def pas_refined_all_auth_is_owns aag_cap_auth_def)+ 495 496 497lemma stupid_strg: 498 "cap_links_asid_slot aag (pasObjectAbs aag (fst y)) x \<longrightarrow> 499 (x = cap \<and> (\<exists>b. y = (a, b)) \<longrightarrow> cap_links_asid_slot aag (pasObjectAbs aag a) cap)" 500 by auto 501 502lemma decode_set_ipc_buffer_authorised: 503 "\<lbrace>K (is_subject aag t \<and> (\<forall>x \<in> set excaps. is_subject aag (fst (snd x))) 504 \<and> (\<forall>x \<in> set excaps. pas_cap_cur_auth aag (fst x))) \<rbrace> 505 decode_set_ipc_buffer msg (cap.ThreadCap t) slot excaps 506 \<lbrace>\<lambda>rv s. authorised_tcb_inv aag rv\<rbrace>, -" 507 unfolding decode_set_ipc_buffer_def authorised_tcb_inv_def 508 apply (cases "excaps ! 0") 509 apply (clarsimp cong: list.case_cong split del: if_split) 510 apply (rule hoare_pre) 511 apply (clarsimp simp: ball_Un aag_cap_auth_def split del: if_split split: prod.split 512 | strengthen stupid_strg 513 | wp (once) derive_cap_obj_refs_auth derive_cap_untyped_range_subset derive_cap_clas derive_cap_cli 514 hoare_vcg_all_lift_R whenE_throwError_wp slot_long_running_inv 515 | wpc)+ 516 apply (cases excaps, simp) 517 apply fastforce 518 done 519 520lemma decode_set_space_authorised: 521 "\<lbrace>K (is_subject aag t \<and> (\<forall>x \<in> set excaps. is_subject aag (fst (snd x))) 522 \<and> (\<forall>x \<in> set excaps. pas_cap_cur_auth aag (fst x))) \<rbrace> 523 decode_set_space ws (cap.ThreadCap t) slot excaps 524 \<lbrace>\<lambda>rv s. authorised_tcb_inv aag rv\<rbrace>, -" 525 unfolding decode_set_space_def authorised_tcb_inv_def 526 apply (rule hoare_pre) 527 apply (simp cong: list.case_cong split del: if_split) 528 apply (clarsimp simp: ball_Un split del: if_split 529 | wp (once) derive_cap_obj_refs_auth derive_cap_untyped_range_subset derive_cap_clas derive_cap_cli 530 hoare_vcg_const_imp_lift_R hoare_vcg_all_lift_R whenE_throwError_wp slot_long_running_inv)+ 531 apply (clarsimp simp: not_less all_set_conv_all_nth dest!: P_0_1_spec) 532 apply (auto simp: aag_cap_auth_def update_cap_cli intro: update_cap_obj_refs_subset dest!: update_cap_untyped_range_subset update_cap_cap_auth_conferred_subset) 533 done 534 535(* grot: this is from the bowels of decode_tcb_configure_authorised. *) 536lemma decode_tcb_configure_authorised_helper: 537 "\<lbrace>K True and K (is_subject aag t \<and> (\<forall>x \<in> set excaps. is_subject aag (fst (snd x))) 538 \<and> (\<forall>x \<in> set excaps. pas_cap_cur_auth aag (fst x)) 539 \<and> authorised_tcb_inv aag set_param \<and> is_thread_control set_param)\<rbrace> 540 decode_set_space ws (cap.ThreadCap t) slot excaps 541 \<lbrace>\<lambda>rv s. authorised_tcb_inv aag (tcb_invocation.ThreadControl t slot (tc_new_fault_ep rv) 542 None None (tc_new_croot rv) 543 (tc_new_vroot rv) (tc_new_buffer set_param))\<rbrace>, -" 544 apply (rule hoare_gen_asmE) 545 apply (cases set_param) 546 apply (simp_all add: is_thread_control_def decode_set_space_def authorised_tcb_inv_def 547 cong: list.case_cong option.case_cong prod.case_cong 548 split: prod.split_asm split del: if_split) 549 apply (cases "excaps!0") 550 apply (cases "excaps!Suc 0") 551 apply (rule hoare_pre) 552 apply (clarsimp simp: ball_Un split del: if_split split: prod.split 553 | strengthen stupid_strg 554 | wp (once) derive_cap_obj_refs_auth derive_cap_untyped_range_subset derive_cap_clas derive_cap_cli 555 hoare_vcg_all_lift_R whenE_throwError_wp slot_long_running_inv)+ 556 apply (clarsimp cong: list.case_cong option.case_cong prod.case_cong split: prod.split_asm) 557 apply (clarsimp simp: not_less all_set_conv_all_nth dest!: P_0_1_spec) 558 apply (auto simp: aag_cap_auth_def update_cap_cli intro: update_cap_untyped_range_subset update_cap_obj_refs_subset dest!: update_cap_cap_auth_conferred_subset elim: bspec) 559 done 560 561lemma decode_tcb_configure_authorised: 562 "\<lbrace>K (is_subject aag t \<and> (\<forall>x \<in> set excaps. is_subject aag (fst (snd x))) 563 \<and> (\<forall>x \<in> set excaps. pas_cap_cur_auth aag (fst x))) \<rbrace> 564 decode_tcb_configure msg (cap.ThreadCap t) slot excaps 565 \<lbrace>\<lambda>rv s. authorised_tcb_inv aag rv\<rbrace>, -" 566 apply (wpsimp simp: decode_tcb_configure_def 567 wp: whenE_throwError_wp decode_tcb_configure_authorised_helper 568 decode_set_ipc_buffer_authorised) 569 apply (auto dest: in_set_takeD) 570 done 571 572lemma decode_set_priority_authorised: 573 "\<lbrace>K (is_subject aag t)\<rbrace> 574 decode_set_priority msg (ThreadCap t) slot excs 575 \<lbrace>\<lambda>rv s. authorised_tcb_inv aag rv\<rbrace>, -" 576 by (wpsimp simp: decode_set_priority_def check_prio_def authorised_tcb_inv_def) 577 578lemma decode_set_mcpriority_authorised: 579 "\<lbrace>K (is_subject aag t)\<rbrace> 580 decode_set_mcpriority msg (ThreadCap t) slot excs 581 \<lbrace>\<lambda>rv s. authorised_tcb_inv aag rv\<rbrace>, -" 582 by (wpsimp simp: decode_set_mcpriority_def check_prio_def authorised_tcb_inv_def) 583 584lemma decode_set_sched_params_authorised: 585 "\<lbrace>K (is_subject aag t)\<rbrace> 586 decode_set_sched_params msg (ThreadCap t) slot excs 587 \<lbrace>\<lambda>rv s. authorised_tcb_inv aag rv\<rbrace>, -" 588 by (wpsimp simp: decode_set_sched_params_def check_prio_def authorised_tcb_inv_def) 589 590lemma decode_unbind_notification_authorised: 591 "\<lbrace>K (is_subject aag t)\<rbrace> 592 decode_unbind_notification (cap.ThreadCap t) 593 \<lbrace>\<lambda>rv s. authorised_tcb_inv aag rv\<rbrace>, -" 594 unfolding decode_unbind_notification_def authorised_tcb_inv_def 595 apply clarsimp 596 apply (wp gbn_wp, clarsimp) 597 done 598 599lemma decode_bind_notification_authorised: 600 "\<lbrace>K (is_subject aag t \<and> (\<forall>x \<in> set excaps. is_subject aag (fst (snd x))) 601 \<and> (\<forall>x \<in> set excaps. pas_cap_cur_auth aag (fst x)) )\<rbrace> 602 decode_bind_notification (cap.ThreadCap t) excaps 603 \<lbrace>\<lambda>rv s. authorised_tcb_inv aag rv\<rbrace>, -" 604 unfolding decode_bind_notification_def authorised_tcb_inv_def 605 apply clarsimp 606 apply (wp gbn_wp get_simple_ko_wp whenE_throwError_wp | wpc | simp add:)+ 607 apply (clarsimp dest!: hd_in_set) 608 apply (drule_tac x="hd excaps" in bspec, simp)+ 609 apply (auto simp: aag_cap_auth_def cap_auth_conferred_def cap_rights_to_auth_def AllowRecv_def) 610 done 611 612lemma decode_set_tls_base_authorised: 613 "\<lbrace>K (is_subject aag t)\<rbrace> 614 decode_set_tls_base msg (cap.ThreadCap t) 615 \<lbrace>\<lambda>rv s. authorised_tcb_inv aag rv\<rbrace>, -" 616 unfolding decode_set_tls_base_def authorised_tcb_inv_def 617 apply clarsimp 618 apply (wpsimp wp: gbn_wp) 619 done 620 621lemma decode_tcb_invocation_authorised: 622 "\<lbrace>invs and pas_refined aag and K (is_subject aag t \<and> (\<forall>x \<in> set excaps. is_subject aag (fst (snd x))) 623 \<and> (\<forall>x \<in> set excaps. pas_cap_cur_auth aag (fst x)))\<rbrace> 624 decode_tcb_invocation label msg (cap.ThreadCap t) slot excaps 625 \<lbrace>\<lambda>rv s. authorised_tcb_inv aag rv\<rbrace>,-" 626 unfolding decode_tcb_invocation_def 627 apply (rule hoare_pre) 628 apply wpc 629 apply (wp decode_registers_authorised decode_tcb_configure_authorised 630 decode_set_priority_authorised decode_set_mcpriority_authorised 631 decode_set_sched_params_authorised 632 decode_set_ipc_buffer_authorised decode_set_space_authorised 633 decode_bind_notification_authorised 634 decode_unbind_notification_authorised 635 decode_set_tls_base_authorised)+ 636 by (auto iff: authorised_tcb_inv_def) 637 638text\<open> 639 640@{term "decode_tcb_invocation"} preserves all invariants, so no need 641to show @{term "integrity"} or @{term "pas_refined"}. 642 643\<close> 644 645end 646 647end 648