1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 *) 6 7theory Interrupt_AC 8imports 9 Finalise_AC 10begin 11 12context begin interpretation Arch . (*FIXME: arch_split*) 13 14definition 15 arch_authorised_irq_ctl_inv :: "'a PAS \<Rightarrow> Invocations_A.arch_irq_control_invocation \<Rightarrow> bool" 16where 17 "arch_authorised_irq_ctl_inv aag cinv \<equiv> 18 case cinv of 19 (ArchIRQControlIssue irq x1 x2 trigger) \<Rightarrow> 20 is_subject aag (fst x1) \<and> is_subject aag (fst x2) \<and> 21 (pasSubject aag, Control, pasIRQAbs aag irq) \<in> pasPolicy aag" 22 23definition 24 authorised_irq_ctl_inv :: "'a PAS \<Rightarrow> Invocations_A.irq_control_invocation \<Rightarrow> bool" 25where 26 "authorised_irq_ctl_inv aag cinv \<equiv> 27 case cinv of 28 IRQControl irq x1 x2 \<Rightarrow> is_subject aag (fst x1) \<and> is_subject aag (fst x2) \<and> 29 (pasSubject aag, Control, pasIRQAbs aag irq) \<in> pasPolicy aag 30 | ArchIRQControl acinv \<Rightarrow> arch_authorised_irq_ctl_inv aag acinv" 31 32lemma arch_invoke_irq_control_pas_refined: 33 "\<lbrace>pas_refined aag and valid_mdb and arch_irq_control_inv_valid irq_ctl_inv and 34 K (arch_authorised_irq_ctl_inv aag irq_ctl_inv)\<rbrace> 35 arch_invoke_irq_control irq_ctl_inv 36 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 37 apply (cases irq_ctl_inv; simp) 38 apply (wpsimp wp: cap_insert_pas_refined_not_transferable) 39 apply (clarsimp simp: cte_wp_at_caps_of_state clas_no_asid cap_links_irq_def 40 arch_authorised_irq_ctl_inv_def aag_cap_auth_def 41 arch_irq_control_inv_valid_def) 42 done 43 44lemma invoke_irq_control_pas_refined: 45 "\<lbrace>pas_refined aag and valid_mdb and irq_control_inv_valid irq_ctl_inv 46 and K (authorised_irq_ctl_inv aag irq_ctl_inv)\<rbrace> 47 invoke_irq_control irq_ctl_inv 48 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 49 apply (cases irq_ctl_inv; simp) 50 apply (wpsimp wp: cap_insert_pas_refined_not_transferable) 51 apply (clarsimp simp: cte_wp_at_caps_of_state clas_no_asid cap_links_irq_def 52 authorised_irq_ctl_inv_def aag_cap_auth_def) 53 apply (wp arch_invoke_irq_control_pas_refined) 54 apply (clarsimp simp: cte_wp_at_caps_of_state clas_no_asid cap_links_irq_def 55 authorised_irq_ctl_inv_def aag_cap_auth_def) 56 done 57 58definition 59 authorised_irq_hdl_inv :: "'a PAS \<Rightarrow> Invocations_A.irq_handler_invocation \<Rightarrow> bool" 60where 61 "authorised_irq_hdl_inv aag hinv \<equiv> 62 case hinv of 63 irq_handler_invocation.SetIRQHandler word cap x \<Rightarrow> 64 is_subject aag (fst x) \<and> pas_cap_cur_auth aag cap \<and> is_subject_irq aag word 65 | irq_handler_invocation.ClearIRQHandler word \<Rightarrow> is_subject_irq aag word 66 | _ \<Rightarrow> True" 67 68lemma emptyable_irq_node: 69 "emptyable (interrupt_irq_node s x21, []) s" 70 by (simp add:emptyable_def tcb_cnode_index_def) 71 72lemma pas_refined_is_subject_irqD: 73 "\<lbrakk>is_subject_irq aag irq ; pas_refined aag s \<rbrakk> \<Longrightarrow> is_subject aag (interrupt_irq_node s irq)" 74 by (simp add:pas_refined_def irq_map_wellformed_aux_def) 75 76lemma invoke_irq_handler_pas_refined: 77 "\<lbrace>pas_refined aag and invs and irq_handler_inv_valid irq_inv 78 and K (authorised_irq_hdl_inv aag irq_inv)\<rbrace> 79 invoke_irq_handler irq_inv 80 \<lbrace>\<lambda>rv (s::det_ext state). pas_refined aag s\<rbrace>" 81 apply (rule hoare_gen_asm) 82 apply (cases irq_inv, simp_all add: authorised_irq_hdl_inv_def) 83 apply (wp cap_insert_pas_refined_not_transferable delete_one_caps_of_state 84 | strengthen invs_mdb aag_Control_owns_strg 85 | simp add: pas_refined_wellformed cte_wp_at_caps_of_state)+ 86 apply (rename_tac irq cap slot) 87 apply (rule_tac Q = 88 "\<lambda> irq_slot. K(irq_slot \<noteq> slot) and invs and emptyable irq_slot 89 and cte_wp_at can_fast_finalise irq_slot 90 and not cte_wp_at is_transferable_cap slot 91 and K(is_subject aag (fst irq_slot))" in hoare_post_imp) 92 apply (force simp: cte_wp_at_caps_of_state) 93 apply simp 94 apply (wp get_irq_slot_different) 95 96 apply (clarsimp simp: emptyable_irq_node cte_wp_at_caps_of_state) 97 apply (fastforce simp: interrupt_derived_def is_cap_simps cap_master_cap_def split: cap.splits) 98 apply (wp delete_one_caps_of_state | simp add: get_irq_slot_def)+ 99 apply (fastforce dest: pas_refined_is_subject_irqD) 100 done 101 102 103lemma invoke_irq_control_respects: 104 "\<lbrace>integrity aag X st and pas_refined aag and K (authorised_irq_ctl_inv aag irq_ctl_inv)\<rbrace> 105 invoke_irq_control irq_ctl_inv 106 \<lbrace>\<lambda>y. integrity aag X st\<rbrace>" 107 apply (rule hoare_gen_asm) 108 apply (cases irq_ctl_inv) 109 subgoal \<comment>\<open>generic case\<close> 110 apply (simp add: authorised_irq_ctl_inv_def) 111 apply (wp cap_insert_integrity_autarch aag_Control_into_owns_irq | simp | blast)+ 112 done 113 subgoal for arch_irq_ctl_inv \<comment>\<open>arch case\<close> 114 apply (simp add: arch_authorised_irq_ctl_inv_def authorised_irq_ctl_inv_def) 115 apply (case_tac arch_irq_ctl_inv, clarsimp simp add: setIRQTrigger_def) 116 apply (wp cap_insert_integrity_autarch aag_Control_into_owns_irq dmo_mol_respects do_machine_op_pas_refined | simp)+ 117 apply auto 118 done 119 done 120 121lemma integrity_irq_masks [iff]: 122 "integrity aag X st (s\<lparr>machine_state := machine_state s \<lparr>irq_masks := v \<rparr>\<rparr>) = integrity aag X st s" 123 unfolding integrity_def 124 by simp 125 126lemma invoke_irq_handler_respects: 127 "\<lbrace>integrity aag X st and pas_refined aag and einvs and 128 K (authorised_irq_hdl_inv aag irq_inv)\<rbrace> 129 invoke_irq_handler irq_inv 130 \<lbrace>\<lambda>y. integrity aag X st\<rbrace>" 131 apply (rule hoare_gen_asm) 132 apply (cases irq_inv, simp_all add: authorised_irq_hdl_inv_def) 133 apply (rule hoare_pre) 134 apply (wp cap_insert_integrity_autarch get_irq_slot_owns dmo_wp | simp add: maskInterrupt_def )+ 135 done 136 137lemma decode_irq_control_invocation_authorised [wp]: 138 "\<lbrace>pas_refined aag 139 and K (is_subject aag (fst slot) 140 \<and> (\<forall>cap \<in> set caps. pas_cap_cur_auth aag cap) 141 \<and> (args \<noteq> [] \<longrightarrow> 142 (pasSubject aag, Control, pasIRQAbs aag (ucast (args ! 0))) \<in> pasPolicy aag))\<rbrace> 143 decode_irq_control_invocation info_label args slot caps 144 \<lbrace>\<lambda>x s. authorised_irq_ctl_inv aag x\<rbrace>, -" 145 unfolding decode_irq_control_invocation_def arch_decode_irq_control_invocation_def authorised_irq_ctl_inv_def arch_authorised_irq_ctl_inv_def arch_check_irq_def 146 apply (rule hoare_gen_asmE) 147 apply (rule hoare_pre) 148 apply (simp add: Let_def split del: if_split cong: if_cong) 149 apply (wp whenE_throwError_wp hoare_vcg_imp_lift hoare_drop_imps 150 | strengthen aag_Control_owns_strg 151 | simp add: o_def del: hoare_True_E_R)+ 152 apply (cases args, simp_all) 153 apply (cases caps, simp_all) 154 apply (simp add: ucast_mask_drop) 155 apply (auto simp: is_cap_simps cap_auth_conferred_def 156 pas_refined_wellformed 157 pas_refined_all_auth_is_owns aag_cap_auth_def) 158 done 159 160lemma decode_irq_handler_invocation_authorised [wp]: 161 "\<lbrace>K (is_subject_irq aag irq 162 \<and> (\<forall>cap_slot \<in> set caps. pas_cap_cur_auth aag (fst cap_slot) 163 \<and> is_subject aag (fst (snd cap_slot))))\<rbrace> 164 decode_irq_handler_invocation info_label irq caps 165 \<lbrace>\<lambda>x s. authorised_irq_hdl_inv aag x\<rbrace>, -" 166 unfolding decode_irq_handler_invocation_def authorised_irq_hdl_inv_def 167 apply (rule hoare_pre) 168 apply (simp add: Let_def split_def split del: if_split cong: if_cong) 169 apply wp 170 apply (auto dest!: hd_in_set) 171 done 172 173end 174 175end 176