aarch64 aspec+ainvs+access: access control modulo sorries

Signed-off-by: Ryan Barry <ryan.barry@proofcraft.systems>

proof/access-control/AARCH64/ArchADT_AC.thy

@@ -8,40 +8,37 @@ theory ArchADT_AC
 imports ADT_AC
 begin
 
-context Arch begin global_naming RISCV64
+context Arch begin global_naming AARCH64
 
 named_theorems ADT_AC_assms
 
-lemma mask_ptTranslationBits_ucast_ucast:
-  "(asid && mask ptTranslationBits) = ucast (ucast asid :: 9 word)"
-  by (word_eqI_solve simp: ptTranslationBits_def)
-
 lemma ptr_offset_in_ptr_range:
-  "\<lbrakk> invs s; x \<notin> kernel_mappings;
-     get_vspace_of_thread (kheap s) (arch_state s) tcb \<noteq> global_pt s;
+  "\<lbrakk> invs s; get_vspace_of_thread (kheap s) (arch_state s) tcb \<noteq> global_pt s;
      get_page_info (aobjs_of s)
-                   (get_vspace_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r) \<rbrakk>
+       (get_vspace_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r) \<rbrakk>
      \<Longrightarrow> ptrFromPAddr base + (x && mask sz) \<in> ptr_range (ptrFromPAddr base) sz"
   apply (simp add: ptr_range_def mask_def)
   apply (rule conjI)
    apply (rule_tac b="2 ^ sz - 1" in word_plus_mono_right2)
     apply (frule some_get_page_info_umapsD)
-           apply (fastforce dest: get_vspace_of_thread_reachable
-                            simp: canonical_not_kernel_is_user get_page_info_def)+
+          apply (fastforce dest: get_vspace_of_thread_reachable
+                           simp:  get_page_info_def)+
     apply clarsimp
     apply (drule is_aligned_ptrFromPAddr_n)
-     apply (simp add: pageBitsForSize_def pageBits_def canonical_bit_def ptTranslationBits_def
+     apply (simp add: pageBitsForSize_def pageBits_def canonical_bit_def
+                      ptTranslationBits_def pptrBaseOffset_alignment_def
                split: vmpage_size.splits)
     apply (clarsimp simp: is_aligned_no_overflow' word_and_le1)+
   apply (subst p_assoc_help)
   apply (rule word_plus_mono_right)
    apply (rule word_and_le1)
   apply (frule some_get_page_info_umapsD)
-         apply (fastforce dest: get_vspace_of_thread_reachable
-                          simp: canonical_not_kernel_is_user get_page_info_def)+
+        apply (fastforce dest: get_vspace_of_thread_reachable
+                         simp: get_page_info_def)+
   apply clarsimp
   apply (drule is_aligned_ptrFromPAddr_n)
-   apply (simp add: pageBitsForSize_def pageBits_def canonical_bit_def ptTranslationBits_def
+   apply (simp add: pageBitsForSize_def pageBits_def canonical_bit_def
+                    ptTranslationBits_def pptrBaseOffset_alignment_def
              split: vmpage_size.splits)
   apply (clarsimp simp: is_aligned_no_overflow')
   done
@@ -50,24 +47,19 @@ lemma user_op_access[ADT_AC_assms]:
   "\<lbrakk> invs s; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr;
      auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x) \<rbrakk>
      \<Longrightarrow> abs_has_auth_to aag auth tcb (ptrFromPAddr ptr)"
-  apply (case_tac "x \<in> kernel_mappings")
-  using get_vspace_of_thread_asid_or_global_pt
-   apply (fastforce simp: ptable_rights_def vspace_cap_rights_to_auth_def invs_def
-                          valid_state_def valid_arch_state_def kernel_mappings_canonical
-                    dest: some_get_page_info_kmapsD split: option.splits)
   apply (clarsimp simp: ptable_lift_def split: option.splits)
   apply (insert get_vspace_of_thread_asid_or_global_pt)
   apply (erule_tac x=s in meta_allE)
   apply (erule_tac x=tcb in meta_allE)
   apply (cases "get_vspace_of_thread (kheap s) (arch_state s) tcb = global_pt s"; clarsimp)
-   apply (frule get_page_info_gpd_kmaps[rotated 2]; fastforce simp: get_page_info_def)
-  apply (frule (3) ptr_offset_in_ptr_range)
+   apply (frule get_page_info_gpd_kmaps[rotated 3]; fastforce simp: get_page_info_def)
+  apply (frule (2) ptr_offset_in_ptr_range)
   apply (frule get_vspace_of_thread_reachable; clarsimp)
   apply (frule vs_lookup_table_vspace)
      apply fastforce+
+  apply (clarsimp simp: vspace_for_asid_def entry_for_asid_def pool_for_asid_def entry_for_pool_def)
   apply (clarsimp simp: get_vspace_of_thread_def get_page_info_def ptable_rights_def pt_lookup_slot_def
-                 split: if_splits option.splits kernel_object.splits cap.splits arch_cap.splits)
-  apply (frule (1) canonical_not_kernel_is_user)
+                 split: if_splits option.splits kernel_object.splits cap.splits arch_cap.splits pt_type.splits)
   apply (frule pt_lookup_slot_from_level_is_subject)
           apply (fastforce elim: vs_lookup_table_vref_independent)+
    apply (rule aag_Control_into_owns)
@@ -86,24 +78,21 @@ lemma user_op_access[ADT_AC_assms]:
   apply (drule (1) vs_lookup_table_extend, rule order_refl)
   apply (rename_tac level vref)
   apply (case_tac "level = asid_pool_level", simp add: pt_walk_top)
-  apply (frule vs_lookup_table_is_aligned; clarsimp simp: canonical_not_kernel_is_user)
+  apply (frule vs_lookup_table_is_aligned; clarsimp)
   apply (clarsimp simp: pas_refined_def pte_info_def split: pte.splits)
   apply (erule subsetD)
-  apply (clarsimp simp: auth_graph_map_def state_objs_to_policy_def)
-  apply (intro exI conjI sbta_vref | erule sym | rule refl)+
-  apply (clarsimp simp: state_vrefs_def ptes_of_Some pts_of_Some)
-  apply (intro exI conjI)
-      apply (simp add: canonical_not_kernel_is_user)+
-  apply (clarsimp simp: vs_refs_aux_def)
-  apply (rule conjI; clarsimp)
-   apply (clarsimp simp: graph_of_def pte_ref2_def Bex_def ptes_of_Some pts_of_Some aobjs_of_Some)
-   apply (rule_tac x="table_index (pt_slot_offset max_pt_level vref x)" in exI)
-   apply (fastforce simp: table_index_max_level_slots canonical_not_kernel_is_user
-                          image_iff ptrFromPAddr_def mult_is_add.mult_ac)
-  apply (clarsimp simp: graph_of_def pte_ref2_def ptes_of_Some pts_of_Some aobjs_of_Some)
-  apply (rule_tac x="table_index (pt_slot_offset level vref x)" in exI)
-  apply (fastforce simp: image_iff table_index_offset_pt_bits_left
-                         ptrFromPAddr_def mult_is_add.mult_ac)
+  apply (clarsimp simp: auth_graph_map_def state_objs_to_policy_def vspace_for_asid_def)
+  apply (drule_tac s="pasObjectAbs aag vref" in sym)
+  apply (clarsimp simp: ptes_of_Some pts_of_Some)
+  apply (clarsimp simp: pt_apply_def split: pt.splits)
+   apply (intro exI conjI sbta_vref | simp add: state_vrefs_def vspace_objs_of_Some)+
+   apply (clarsimp simp: vs_refs_aux_def graph_of_def pte_ref2_def)
+   apply (rule_tac x="UCAST(64 \<rightarrow> vs_index_len) (pt_index max_pt_level x)" in exI)
+   apply (fastforce simp: image_iff ptrFromPAddr_def mult_is_add.mult_ac split: pte.splits)
+  apply (intro exI conjI sbta_vref | simp add: state_vrefs_def vspace_objs_of_Some)+
+  apply (clarsimp simp: vs_refs_aux_def graph_of_def pte_ref2_def)
+  apply (rule_tac x="UCAST(64 \<rightarrow> 9) (pt_index level x)" in exI)
+  apply (fastforce simp: image_iff ptrFromPAddr_def mult_is_add.mult_ac split: pte.splits)
   done
 
 lemma write_in_vspace_cap_rights[ADT_AC_assms]:

proof/access-control/AARCH64/ArchAccess.thy

@@ -8,7 +8,7 @@ theory ArchAccess
 imports Types
 begin
 
-context Arch begin global_naming RISCV64
+context Arch begin global_naming AARCH64
 
 subsection \<open>Arch-specific transformation of caps into authorities\<close>
 
@@ -25,37 +25,39 @@ subsection \<open>Generating a policy from the current ASID distribution\<close>
 
 definition pte_ref2 where
   "pte_ref2 level pte \<equiv> case pte of
-     PagePTE ppn atts rights
-       \<Rightarrow> Some (ptrFromPAddr (addr_from_ppn ppn),
-                pageBitsForSize (vmpage_size_of_level level),
+     PagePTE paddr _ _ rights
+       \<Rightarrow> Some (ptrFromPAddr paddr,
+                pt_bits_left level,
                 vspace_cap_rights_to_auth rights)
-   | PageTablePTE ppn atts
-       \<Rightarrow> Some (ptrFromPAddr (addr_from_ppn ppn), 0, {Control})
+   | PageTablePTE ppn
+       \<Rightarrow> Some (ptrFromPAddr (paddr_from_ppn ppn), 0, {Control})
    | _ \<Rightarrow> None"
 
 definition vs_refs_aux :: "vm_level \<Rightarrow> arch_kernel_obj \<Rightarrow> (obj_ref \<times> obj_ref \<times> aa_type \<times> auth) set"
   where
   "vs_refs_aux level \<equiv> \<lambda>ko. case ko of
-     ASIDPool pool \<Rightarrow> (\<lambda>(r,p). (p, ucast r, AASIDPool, Control)) ` graph_of pool
-   | PageTable pt \<Rightarrow>
-       \<Union>(r,(p, sz, auth)) \<in> graph_of (pte_ref2 level o pt) - {(x,y). x \<in> kernel_mapping_slots \<and> level = max_pt_level}.
-         (\<lambda>(p, a). (p, ucast r, APageTable, a)) ` (ptr_range p sz \<times> auth)
+     ASIDPool pool \<Rightarrow> (\<lambda>(r,p). (p, ucast r, AASIDPool, Control)) ` graph_of (option_map ap_vspace o pool)
+   | PageTable pt \<Rightarrow> (case pt of
+       VSRootPT pt \<Rightarrow> \<Union>(r,(p, sz, auth)) \<in> graph_of (pte_ref2 level o pt).
+                      (\<lambda>(p, a). (p, ucast r, APageTable VSRootPT_T, a)) ` (ptr_range p sz \<times> auth)
+     | NormalPT pt \<Rightarrow> \<Union>(r,(p, sz, auth)) \<in> graph_of (pte_ref2 level o pt).
+                      (\<lambda>(p, a). (p, ucast r, APageTable NormalPT_T, a)) ` (ptr_range p sz \<times> auth))
    | _ \<Rightarrow> {}"
 
 definition state_vrefs where
   "state_vrefs s \<equiv> \<lambda>p.
      \<Union>{vs_refs_aux lvl ao | lvl ao bot asid vref. vs_lookup_table bot asid vref s = Some (lvl, p)
-                                                   \<and> aobjs_of s p = Some ao \<and> vref \<in> user_region}"
+                                                 \<and> vspace_objs_of s p = Some ao \<and> vref \<in> user_region}"
 
 lemma state_vrefsD:
   "\<lbrakk> vs_lookup_table level asid vref s = Some (lvl, p);
-     aobjs_of s p = Some ao; vref \<in> user_region; x \<in> vs_refs_aux lvl ao \<rbrakk>
+     vspace_objs_of s p = Some ao; vref \<in> user_region; x \<in> vs_refs_aux lvl ao \<rbrakk>
      \<Longrightarrow> x \<in> state_vrefs s p"
   unfolding state_vrefs_def by fastforce
 
 end
 
-context Arch_p_arch_update_eq begin global_naming RISCV64
+context Arch_p_arch_update_eq begin global_naming AARCH64
 
 interpretation Arch .
 
@@ -64,7 +66,7 @@ lemma state_vrefs[iff]: "state_vrefs (f s) = state_vrefs s"
 
 end
 
-context Arch begin global_naming RISCV64
+context Arch begin global_naming AARCH64
 
 lemmas state_vrefs_upd =
   cur_thread_update.state_vrefs
@@ -80,17 +82,18 @@ end
 context Arch begin
 
 primrec aobj_ref' where
-  "aobj_ref' (ASIDPoolCap p as) = {p}"
+  "aobj_ref' (ASIDPoolCap ref _) = {ref}"
 | "aobj_ref' ASIDControlCap = {}"
-| "aobj_ref' (FrameCap ref cR sz dev as) = ptr_range ref (pageBitsForSize sz)"
-| "aobj_ref' (PageTableCap x as3) = {x}"
+| "aobj_ref' (FrameCap ref _ sz _ _) = ptr_range ref (pageBitsForSize sz)"
+| "aobj_ref' (PageTableCap ref _ _) = {ref}"
+| "aobj_ref' (VCPUCap ref) = {ref}"
 
 fun acap_asid' :: "arch_cap \<Rightarrow> asid set" where
   "acap_asid' (FrameCap _ _ _ _ mapping) = fst ` set_option mapping"
-| "acap_asid' (PageTableCap _ mapping) = fst ` set_option mapping"
-| "acap_asid' (ASIDPoolCap _ asid)
-     = {x. asid_high_bits_of x = asid_high_bits_of asid \<and> x \<noteq> 0}"
+| "acap_asid' (PageTableCap _ _ mapping) = fst ` set_option mapping"
+| "acap_asid' (ASIDPoolCap _ asid) = {x. asid_high_bits_of x = asid_high_bits_of asid \<and> x \<noteq> 0}"
 | "acap_asid' ASIDControlCap = UNIV"
+| "acap_asid' (VCPUCap _) = {}"
 
 inductive_set state_asids_to_policy_aux for aag caps asid_tab vrefs where
   sata_asid:
@@ -109,7 +112,7 @@ inductive_set state_asids_to_policy_aux for aag caps asid_tab vrefs where
 
 definition
   "state_asids_to_policy_arch aag caps astate vrefs \<equiv>
-     state_asids_to_policy_aux aag caps (riscv_asid_table astate)
+     state_asids_to_policy_aux aag caps (arm_asid_table astate)
                                (vrefs :: 64 word \<Rightarrow> (64 word \<times> 64 word \<times> aa_type \<times> auth) set)"
 declare state_asids_to_policy_arch_def[simp]
 
@@ -201,21 +204,21 @@ lemma integrity_asids_kh_update:
 subsection \<open>Misc definitions\<close>
 
 fun ctxt_IP_update where
-  "ctxt_IP_update (UserContext ctxt) = UserContext (ctxt(NextIP := ctxt FaultIP))"
+  "ctxt_IP_update (UserContext fpu ctxt) = UserContext fpu (ctxt(NextIP := ctxt FaultIP))"
 
 lemma ctxt_IP_update_def:
   "ctxt_IP_update ctxt =
-   (case ctxt of (UserContext ctxt') \<Rightarrow> UserContext (ctxt'(NextIP := ctxt' FaultIP)))"
+   (case ctxt of (UserContext fpu ctxt') \<Rightarrow> UserContext fpu (ctxt'(NextIP := ctxt' FaultIP)))"
   by (cases ctxt; clarsimp)
 
 abbreviation arch_IP_update where
   "arch_IP_update arch \<equiv> arch_tcb_context_set (ctxt_IP_update (arch_tcb_context_get arch)) arch"
 
 definition asid_pool_integrity ::
-  "'a set \<Rightarrow> 'a PAS \<Rightarrow> (asid_low_index \<rightharpoonup> obj_ref) \<Rightarrow> (asid_low_index \<rightharpoonup> obj_ref) \<Rightarrow> bool" where
+  "'a set \<Rightarrow> 'a PAS \<Rightarrow> (asid_low_index \<rightharpoonup> asid_pool_entry) \<Rightarrow> (asid_low_index \<rightharpoonup> asid_pool_entry) \<Rightarrow> bool" where
   "asid_pool_integrity subjects aag pool pool' \<equiv>
      \<forall>x. pool' x \<noteq> pool x
-         \<longrightarrow> pool' x = None \<and> aag_subjects_have_auth_to subjects aag Control (the (pool x))"
+         \<longrightarrow> pool' x = None \<and> aag_subjects_have_auth_to subjects aag Control (ap_vspace (the (pool x)))"
 
 inductive arch_integrity_obj_atomic ::
    "'a PAS \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> arch_kernel_obj \<Rightarrow> arch_kernel_obj \<Rightarrow> bool"
@@ -275,4 +278,86 @@ end
 declare state_vrefs_upd[simp]
 declare integrity_asids_updates[simp]
 
+
+context Arch begin global_naming AARCH64
+
+(* FIXME AARCH64: update the access control spec
+   -Parameterise arch object updates with machine state and arch state
+   -Model virtualised machine state more explicitly
+   -Specify when virtualised machine state can change (i.e. restoring from current VCPU)
+   -Specify when arm_current_vcpu can change (i.e. once current VCPU has been saved)
+   -Specify integrity constraints for FPUs
+*)
+
+\<comment> \<open>Anyone can save virtualised registers to the current VCPU\<close>
+lemma arch_troa_vcpu_save_reg:
+    "\<lbrakk> aobjs_of s vptr = Some (VCPU vcpu); ao' = VCPU vcpu';
+       option_map fst (arm_current_vcpu (arch_state s)) = Some vptr;
+       vcpu' = vcpu\<lparr>vcpu_regs := (vcpu_regs vcpu)(reg := vcpuHardwareReg_val reg (machine_state s))\<rparr> \<rbrakk>
+       \<Longrightarrow> arch_integrity_obj_atomic aag subjects l ao ao'"
+  sorry
+
+(* FIXME AARCH64: assert a connection to the current (or soon-to-be-switched-to) thread? *)
+\<comment> \<open>Anyone can update the virtual count offset in the current VCPU\<close>
+lemma arch_troa_vcpu_restore_vtimer:
+  "\<lbrakk> aobjs_of s vptr = Some (VCPU vcpu); ao' = VCPU vcpu';
+     option_map fst (arm_current_vcpu (arch_state s)) = Some vptr;
+     vcpu' = vcpu\<lparr>vcpu_regs := (vcpu_regs vcpu)
+                    (VCPURegCNTVOFF := vcpu_regs vcpu VCPURegCNTVOFF
+                                       + (read_cntpct_val (machine_state s)
+                                          - vtimerLastPCount (vcpu_vtimer vcpu)))\<rparr> \<rbrakk>
+     \<Longrightarrow> arch_integrity_obj_atomic aag subjects l ao ao'"
+  sorry
+
+\<comment> \<open>Anyone can save the physical count register to the current VCPU\<close>
+lemma arch_troa_vcpu_save_virt_timer:
+    "\<lbrakk> aobjs_of s vptr = Some (VCPU vcpu); ao' = VCPU vcpu';
+       option_map fst (arm_current_vcpu (arch_state s)) = Some vptr;
+       vcpu' = vcpu\<lparr>vcpu_vtimer := VirtTimer (read_cntpct_val (machine_state s))\<rparr> \<rbrakk>
+       \<Longrightarrow> arch_integrity_obj_atomic aag subjects l ao ao'"
+  sorry
+
+\<comment> \<open>Anyone can save virtualised GIC registers to the current VCPU\<close>
+lemma arch_troa_vcpu_save_vgic:
+    "\<lbrakk> aobjs_of s vptr = Some (VCPU vcpu); ao' = VCPU vcpu';
+       option_map fst (arm_current_vcpu (arch_state s)) = Some vptr;
+       vcpu' = vcpu \<lparr>vcpu_vgic := vgic\<rparr>;
+       vgic = vcpu_vgic vcpu\<lparr>vgic_hcr := gic_vcpu_ctrl_hcr_val (machine_state s)\<rparr> \<or>
+       vgic = vcpu_vgic vcpu\<lparr>vgic_vmcr := gic_vcpu_ctrl_vmcr_val (machine_state s)\<rparr> \<or>
+       vgic = vcpu_vgic vcpu\<lparr>vgic_apr := gic_vcpu_ctrl_apr_val (machine_state s)\<rparr> \<or>
+       vgic = vcpu_vgic vcpu\<lparr>vgic_lr := (vgic_lr (vcpu_vgic vcpu))
+                                        (vreg := gic_vcpu_ctrl_lr_val (of_nat vreg) (machine_state s))\<rparr> \<rbrakk>
+       \<Longrightarrow> arch_integrity_obj_atomic aag subjects l ao ao'"
+  sorry
+
+\<comment> \<open>Update the vmid of a pool\<close>
+lemma
+  arch_troa_asidpool_vmid:
+    "\<lbrakk> ao = ASIDPool pool; ao' = ASIDPool pool';
+       \<forall>x. (pool x = None) = (pool' x = None);
+       \<forall>x e e'. pool x = Some e \<and> pool' x = Some e'
+           \<longrightarrow> (ap_vspace e = ap_vspace e' \<and>
+               (ap_vmid e = ap_vmid e' \<or> ap_vmid e = None \<or> ap_vmid e' = None)) \<rbrakk>
+       \<Longrightarrow> arch_integrity_obj_atomic aag subjects l ao ao'"
+  sorry
+
+\<comment> \<open>If a VCPU belongs to the current agent, then so does its associated TCB\<close>
+lemma associated_tcb_is_subject:
+  "\<lbrakk> vcpus_of s v = Some vcpu; vcpu_tcb vcpu = Some t; is_subject aag v \<rbrakk>
+     \<Longrightarrow> is_subject aag t"
+  sorry
+
+\<comment> \<open>If a TCB belongs to the current agent, then so does its associated VCPU\<close>
+lemma associated_vcpu_is_subject:
+  "\<lbrakk> get_tcb t s = Some tcb; tcb_vcpu (tcb_arch tcb) = Some v; is_subject aag t \<rbrakk>
+     \<Longrightarrow> is_subject aag v"
+  sorry
+
+(* FIXME AARCH64: clarify when we can assume this *)
+lemma invs_valid_cur_vcpu:
+  "invs s \<Longrightarrow> valid_cur_vcpu s"
+  sorry
+
+end
+
 end