1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 *) 6 7theory ADT_AC 8imports Syscall_AC 9begin 10 11context begin interpretation Arch . (*FIXME: arch_split*) 12 13lemma pd_of_thread_same_agent: 14 "\<lbrakk> pas_refined aag s; is_subject aag tcb_ptr; 15 get_pd_of_thread (kheap s) (arch_state s) tcb_ptr = pd; 16 pd \<noteq> arm_global_pd (arch_state s) \<rbrakk> 17 \<Longrightarrow> pasObjectAbs aag tcb_ptr = pasObjectAbs aag pd" 18 apply (rule_tac aag="pasPolicy aag" in aag_wellformed_Control[rotated]) 19 apply (fastforce simp: pas_refined_def) 20 apply (rule pas_refined_mem[rotated], simp) 21 apply (clarsimp simp: get_pd_of_thread_eq) 22 apply (cut_tac ptr="(tcb_ptr, tcb_cnode_index 1)" in sbta_caps) 23 prefer 4 24 apply (simp add: state_objs_to_policy_def) 25 apply (subst caps_of_state_tcb_cap_cases) 26 apply (simp add: get_tcb_def) 27 apply (simp add: dom_tcb_cap_cases[simplified]) 28 apply simp 29 apply (simp add: obj_refs_def) 30 apply (simp add: cap_auth_conferred_def is_page_cap_def) 31 done 32 33lemma invs_valid_global_pd_mappings: 34 "invs s \<Longrightarrow> valid_global_vspace_mappings s" 35 apply (simp add: invs_def valid_state_def) 36 done 37 38lemma objs_valid_tcb_vtable: 39 "\<lbrakk>valid_objs s; get_tcb t s = Some tcb\<rbrakk> \<Longrightarrow> s \<turnstile> tcb_vtable tcb" 40 apply (clarsimp simp: get_tcb_def split: option.splits Structures_A.kernel_object.splits) 41 apply (erule cte_wp_valid_cap[rotated]) 42 apply (rule cte_wp_at_tcbI[where t="(a, b)" for a b, where b3="tcb_cnode_index 1"]) 43 apply fastforce+ 44 done 45 46lemma pd_of_thread_page_directory_at: 47 "\<lbrakk> invs s; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s) \<rbrakk> 48 \<Longrightarrow> page_directory_at ((get_pd_of_thread (kheap s) (arch_state s) tcb)) s" 49 apply (clarsimp simp: get_pd_of_thread_def 50 split: option.splits kernel_object.splits cap.splits arch_cap.splits if_splits) 51 apply (frule_tac t=tcb in objs_valid_tcb_vtable[OF invs_valid_objs]) 52 apply (simp add: get_tcb_def) 53 apply (fastforce simp: valid_cap_def2 valid_cap_ref_def valid_arch_cap_ref_simps) 54 done 55 56lemma ptr_offset_in_ptr_range: 57 "\<lbrakk> invs s; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) 58 (get_pd_of_thread (kheap s) (arch_state s) tcb) x = 59 Some (base, sz, attr, r); x \<notin> kernel_mappings; 60 get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s) \<rbrakk> 61 \<Longrightarrow> ptrFromPAddr base + (x && mask sz) \<in> ptr_range (ptrFromPAddr base) sz" 62 apply (simp add: ptr_range_def mask_def) 63 apply (rule conjI) 64 apply (rule_tac b="2 ^ sz - 1" in word_plus_mono_right2) 65 apply (frule some_get_page_info_umapsD) 66 apply (clarsimp simp: get_pd_of_thread_reachable invs_vspace_objs 67 invs_psp_aligned invs_valid_asid_table invs_valid_objs)+ 68 apply (drule is_aligned_ptrFromPAddr_n) 69 apply (simp add: pageBitsForSize_def split: vmpage_size.splits) 70 apply (clarsimp simp: is_aligned_no_overflow' word_and_le1)+ 71 72 apply (subst p_assoc_help) 73 apply (rule word_plus_mono_right) 74 apply (rule word_and_le1) 75 apply (frule some_get_page_info_umapsD) 76 apply (clarsimp simp: get_pd_of_thread_reachable invs_vspace_objs 77 invs_psp_aligned invs_valid_asid_table invs_valid_objs)+ 78 apply (drule is_aligned_ptrFromPAddr_n) 79 apply (simp add: pageBitsForSize_def split: vmpage_size.splits) 80 apply (clarsimp simp: is_aligned_no_overflow') 81 done 82 83lemma kernel_mappings_kernel_mapping_slots: 84 "x \<notin> kernel_mappings \<Longrightarrow> ucast (x >> 20) \<notin> kernel_mapping_slots" 85 apply (rule kernel_base_kernel_mapping_slots) 86 apply (simp add: kernel_mappings_def) 87 done 88 89lemmas kernel_mappings_kernel_mapping_slots' = 90 kernel_mappings_kernel_mapping_slots[simplified kernel_mapping_slots_def, simplified] 91 92lemma ptable_state_objs_to_policy: 93 "\<lbrakk> invs s; ptable_lift tcb s x = Some ptr; 94 auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x); 95 get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); 96 \<forall>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) 97 (get_pd_of_thread (kheap s) (arch_state s) tcb) x \<noteq> 98 Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings \<rbrakk> 99 \<Longrightarrow> (get_pd_of_thread (kheap s) (arch_state s) tcb, auth, ptrFromPAddr ptr) 100 \<in> state_objs_to_policy s" 101 apply (simp add: state_objs_to_policy_def) 102 apply (rule sbta_vref) 103 apply (clarsimp simp: ptable_lift_def ptable_rights_def state_vrefs_def 104 split: option.splits) 105 apply (frule pd_of_thread_page_directory_at, simp) 106 apply (clarsimp simp: typ_at_eq_kheap_obj) 107 108 apply (clarsimp simp: vs_refs_no_global_pts_def) 109 apply (rule_tac x="(ucast (x >> 20), ptrFromPAddr a, aa, 110 vspace_cap_rights_to_auth b)" in bexI) 111 apply clarsimp 112 apply (rule_tac x="(ptrFromPAddr a + (x && mask aa), auth)" in image_eqI) 113 apply (simp add: ptrFromPAddr_def pptrBaseOffset_def pptrBase_def physBase_def) 114 apply (simp add: ptr_offset_in_ptr_range) 115 116 apply (simp add: kernel_mappings_kernel_mapping_slots') 117 apply (clarsimp simp: graph_of_def) 118 apply (clarsimp simp: get_page_info_def get_pd_entry_def pde_ref2_def 119 split: option.splits pde.splits arch_kernel_obj.splits) 120 apply (clarsimp simp: get_arch_obj_def 121 split: option.splits kernel_object.splits arch_kernel_obj.splits)+ 122 done 123 124lemma pt_in_pd_same_agent: 125 "\<lbrakk> pas_refined aag s; is_subject aag pd_ptr; vptr \<notin> kernel_mappings; 126 get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ptr vptr = Some (PageTablePDE p x xa) \<rbrakk> 127 \<Longrightarrow> pasObjectAbs aag pd_ptr = pasObjectAbs aag (ptrFromPAddr p)" 128 apply (rule_tac aag="pasPolicy aag" in aag_wellformed_Control[rotated]) 129 apply (fastforce simp: pas_refined_def) 130 apply (rule pas_refined_mem[rotated], simp) 131 apply (clarsimp simp: get_pd_entry_def get_arch_obj_def 132 split: option.splits kernel_object.splits arch_kernel_obj.splits) 133 apply (simp add: state_objs_to_policy_def) 134 apply (rule sbta_vref) 135 apply (simp add: state_vrefs_def split: option.splits) 136 137 apply (clarsimp simp: vs_refs_no_global_pts_def) 138 apply (rule_tac x="(ucast (vptr >> 20), ptrFromPAddr p, 0, {Control})" in bexI) 139 apply simp 140 141 apply (simp add: kernel_mappings_kernel_mapping_slots' graph_of_def pde_ref2_def) 142 done 143 144lemma pt_in_pd_page_table_at: 145 "\<lbrakk> invs s; get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ptr x = 146 Some (PageTablePDE word1 set1 word2); (\<exists>\<rhd> pd_ptr) s; x \<notin> kernel_mappings \<rbrakk> 147 \<Longrightarrow> page_table_at (ptrFromPAddr word1) s" 148 apply (clarsimp simp: get_pd_entry_def get_arch_obj_def 149 split: option.splits kernel_object.splits arch_kernel_obj.splits) 150 apply (rename_tac "fun") 151 apply (subgoal_tac "valid_vspace_obj (PageDirectory fun) s") 152 apply (simp add: kernel_mappings_slots_eq) 153 apply (drule bspec) 154 apply simp+ 155 apply (drule invs_vspace_objs) 156 apply (auto simp: obj_at_def invs_vspace_objs valid_vspace_objs_def) 157 done 158 159lemma get_page_info_state_objs_to_policy: 160 "\<lbrakk> invs s; auth \<in> vspace_cap_rights_to_auth r; 161 get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) 162 (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r); 163 get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); 164 get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) 165 (get_pd_of_thread (kheap s) (arch_state s) tcb) x = 166 Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings \<rbrakk> 167 \<Longrightarrow> (ptrFromPAddr word1, auth, ptrFromPAddr (base + (x && mask sz))) \<in> state_objs_to_policy s" 168 apply (simp add: state_objs_to_policy_def) 169 apply (rule sbta_vref) 170 apply (clarsimp simp: state_vrefs_def split: option.splits) 171 apply (frule pt_in_pd_page_table_at) 172 apply (simp add: get_pd_of_thread_reachable)+ 173 apply (clarsimp simp: typ_at_eq_kheap_obj) 174 175 apply (clarsimp simp: vs_refs_no_global_pts_def) 176 apply (rule_tac x="(ucast ((x >> 12) && mask 8), ptrFromPAddr base, sz, 177 vspace_cap_rights_to_auth r)" in bexI) 178 apply clarsimp 179 apply (rule_tac x="(ptrFromPAddr base + (x && mask sz), auth)" in image_eqI) 180 apply (simp add: ptrFromPAddr_def pptrBaseOffset_def pptrBase_def physBase_def) 181 apply (simp add: ptr_offset_in_ptr_range) 182 183 apply (clarsimp simp: graph_of_def) 184 apply (clarsimp simp: get_page_info_def get_pd_entry_def get_pt_info_def 185 get_pt_entry_def pte_ref_def 186 split: option.splits pte.splits pde.splits arch_kernel_obj.splits) 187 apply (clarsimp simp: get_arch_obj_def 188 split: option.splits kernel_object.splits arch_kernel_obj.splits)+ 189 done 190 191lemma user_op_access: 192 "\<lbrakk> invs s; pas_refined aag s; is_subject aag tcb; 193 ptable_lift tcb s x = Some ptr; 194 auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x) \<rbrakk> 195 \<Longrightarrow> (pasObjectAbs aag tcb, auth, pasObjectAbs aag (ptrFromPAddr ptr)) \<in> pasPolicy aag" 196 apply (case_tac "x \<in> kernel_mappings") 197 apply (clarsimp simp: ptable_lift_def ptable_rights_def split: option.splits) 198 apply (frule some_get_page_info_kmapsD) 199 apply (fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings 200 vspace_cap_rights_to_auth_def)+ 201 202 apply (case_tac "get_pd_of_thread (kheap s) (arch_state s) tcb 203 = arm_global_pd (arch_state s)") 204 apply (clarsimp simp: ptable_lift_def ptable_rights_def split: option.splits) 205 apply (frule get_page_info_gpd_kmaps[rotated, rotated]) 206 apply (fastforce simp: invs_valid_global_objs invs_arch_state)+ 207 208 apply (subst pd_of_thread_same_agent) 209 apply fastforce+ 210 211 apply (case_tac "\<exists>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) 212 (get_pd_of_thread (kheap s) (arch_state s) tcb) x = 213 Some (PageTablePDE word1 set1 word2)") 214 apply (clarsimp simp: ptable_lift_def ptable_rights_def split: option.splits) 215 apply (frule pd_of_thread_same_agent) 216 apply fastforce+ 217 apply (subst pt_in_pd_same_agent) 218 apply fastforce+ 219 apply (rule pas_refined_mem[rotated], simp) 220 apply (rule get_page_info_state_objs_to_policy) 221 apply fastforce+ 222 223 apply (rule pas_refined_mem[rotated], simp) 224 apply (rule ptable_state_objs_to_policy) 225 apply simp+ 226 done 227 228lemma user_op_access': 229 "\<lbrakk> invs s; pas_refined aag s; is_subject aag tcb; 230 ptable_lift tcb s x = Some (addrFromPPtr ptr); 231 auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x) \<rbrakk> 232 \<Longrightarrow> (pasObjectAbs aag tcb, auth, pasObjectAbs aag ptr) \<in> pasPolicy aag" 233 apply (drule user_op_access) 234 apply auto 235 done 236 237lemma integrity_underlying_mem_update: 238 "\<lbrakk> integrity aag X st s; 239 \<forall>x\<in>xs. (pasSubject aag, Write, pasObjectAbs aag x) \<in> pasPolicy aag; 240 \<forall>x\<in>-xs. um' x = underlying_memory (machine_state s) x\<rbrakk> 241 \<Longrightarrow> integrity aag X st 242 (machine_state_update (\<lambda>ms. underlying_memory_update (\<lambda>_. um') ms) s)" 243 apply (clarsimp simp: integrity_def) 244 apply (case_tac "x \<in> xs") 245 apply (erule_tac x=x in ballE) 246 apply (rule trm_write) 247 apply simp+ 248 done 249 250lemma dmo_user_memory_update_respects_Write: 251 "\<lbrace>integrity aag X st and K (\<forall>p \<in> dom um. aag_has_auth_to aag Write p)\<rbrace> 252 do_machine_op (user_memory_update um) 253 \<lbrace>\<lambda>a. integrity aag X st\<rbrace>" 254 unfolding user_memory_update_def 255 apply (wp dmo_wp) 256 apply clarsimp 257 apply (simp cong: abstract_state.fold_congs option.case_cong_weak) 258 apply (rule integrity_underlying_mem_update) 259 apply simp+ 260 apply (simp add: dom_def)+ 261 done 262 263lemma integrity_device_state_update: 264 "\<lbrakk>integrity aag X st s; 265 \<forall>x\<in>xs. (pasSubject aag, Write, pasObjectAbs aag x) \<in> pasPolicy aag; 266 \<forall>x\<in>-xs. um' x = None 267 \<rbrakk> \<Longrightarrow> integrity aag X st (machine_state_update (\<lambda>v. v\<lparr>device_state := device_state v ++ um'\<rparr>) s)" 268 apply (clarsimp simp: integrity_def) 269 apply (case_tac "x \<in> xs") 270 apply (erule_tac x=x in ballE) 271 apply (rule trd_write) 272 apply simp+ 273 apply (erule_tac x = x in allE, erule integrity_device.cases) 274 apply (erule trd_lrefl) 275 apply (rule trd_orefl) 276 apply (clarsimp simp: map_add_def) 277 apply (erule trd_write) 278 done 279 280lemma dmo_device_update_respects_Write: 281 "\<lbrace>integrity aag X st and (\<lambda>s. device_state (machine_state s) = um) 282 and K (\<forall>p \<in> dom um'. aag_has_auth_to aag Write p)\<rbrace> 283 do_machine_op (device_memory_update um') 284 \<lbrace>\<lambda>a. integrity aag X st\<rbrace>" 285 apply (simp add: device_memory_update_def) 286 apply (rule hoare_pre) 287 apply (wp dmo_wp) 288 apply clarsimp 289 apply (simp cong: abstract_state.fold_congs) 290 apply (rule integrity_device_state_update) 291 apply simp 292 apply clarify 293 apply (drule(1) bspec) 294 apply simp 295 apply fastforce 296 done 297 298lemma dmo_um_upd_machine_state: 299 "\<lbrace>\<lambda>s. P (device_state (machine_state s))\<rbrace> 300 do_machine_op (user_memory_update ms) 301 \<lbrace>\<lambda>_ s. P (device_state (machine_state s))\<rbrace>" 302 including no_pre 303 apply (wp dmo_wp) 304 by (simp add:user_memory_update_def simpler_modify_def valid_def) 305 306lemma do_user_op_respects: 307 "\<lbrace> invs and integrity aag X st and is_subject aag \<circ> cur_thread and pas_refined aag \<rbrace> 308 do_user_op uop tc 309 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 310 apply (simp add: do_user_op_def) 311 apply (wp | simp | wpc)+ 312 apply (rule dmo_device_update_respects_Write) 313 apply (wp dmo_um_upd_machine_state 314 dmo_user_memory_update_respects_Write hoare_vcg_all_lift hoare_vcg_imp_lift 315 | wpc | clarsimp)+ 316 apply (rule hoare_pre_cont) 317 apply (wp select_wp | wpc | clarsimp)+ 318 apply (simp add: restrict_map_def split:if_splits) 319 apply (rule conjI) 320 apply (clarsimp split: if_splits) 321 apply (drule_tac auth=Write in user_op_access') 322 apply (simp add: vspace_cap_rights_to_auth_def)+ 323 apply (rule conjI,simp) 324 apply (clarsimp split: if_splits) 325 apply (drule_tac auth=Write in user_op_access') 326 apply (simp add: vspace_cap_rights_to_auth_def)+ 327 done 328 329end 330 331end 332