AArch64 Access Control: initial setup #837

ryybrr · 2024-12-11T07:38:48Z

Partial access control proofs for AArch64:

Introduce a minimal set of assumption such that the remaining theories build without sorries. These assumptions are defined at the end of AARCH64/ArchAccess.thy and represent new integrity constraints
Add FIXME AARCH64 comments for additional proof obligations not captured by the current spec
Update ASpec and AInvs to enforce a stricter partitioning of VCPU saves/restores

This PR is structured into 2 commits:

Port existing theories verbatim over to AArch64
Update these theories such that Access builds with quick_and_dirty enabled

To review the fine-grained changes, refer only to the 2nd commit

proof/invariant-abstract/AARCH64/ArchVCPU_AI.thy

proof/access-control/AARCH64/ArchFinalise_AC.thy

lsf37 · 2024-12-11T22:39:40Z

proof/access-control/AARCH64/ArchAccess.thy

+     PagePTE paddr _ _ rights
+       \<Rightarrow> Some (ptrFromPAddr paddr,
+                pt_bits_left level,
+                vspace_cap_rights_to_auth rights)
+   | PageTablePTE ppn
+       \<Rightarrow> Some (ptrFromPAddr (paddr_from_ppn ppn), 0, {Control})


style nitpick: the => should go on the same line as the case expression (e.g. PagePTE).

proof/access-control/AARCH64/ArchAccess.thy

lsf37

Great work! That goes a good deal beyond just setup, it already contains the bulk of the main proof and will allow us to concentrate on the tricky bits in the next part.

I have only some very minor style nitpicks. Otherwise very nice!

-Remove various instances of pspace_aligned, valid_vspace_objs, and valid_asid_table/valid_arch_state from preconditions -Relax the is_subject predicate in various Syscall_AC lemmas Signed-off-by: Ryan Barry <[email protected]>

Signed-off-by: Ryan Barry <[email protected]>

Xaphiosis · 2024-12-12T03:15:46Z

proof/access-control/Tcb_AC.thy

@@ -177,7 +176,7 @@ lemma (in is_extended') cte_wp_at[wp]: "I (cte_wp_at P a)"
  by (rule lift_inv, simp)

 lemma checked_insert_pas_refined:
-  "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and
+  "\<lbrace>pas_refined aag and valid_mdb and


this is very cheerful to see, I'm glad you're spotting these overly-strong preconditions

Xaphiosis · 2024-12-12T03:20:29Z

proof/access-control/RISCV64/ArchFinalise_AC.thy

@@ -241,7 +240,7 @@ global_interpretation Finalise_AC_1?: Finalise_AC_1
 proof goal_cases
  interpret Arch .
  case 1 show ?case
-    by (unfold_locales; (fact Finalise_AC_assms | wp finalise_cap_replaceable))
+    by (unfold_locales; wpsimp wp: Finalise_AC_assms)


This is a strange formulation, it implies that Finalise_AC_assms is only wp rules. The previous formulation said: "if it isn't a fact then it's a wp rule".

This formulation lets wp use the ones that are rules and will apply them as rule otherwise. I don't really mind, but it is true that the old version showed slightly more intention. Then again, it would also use fact with Finalise_AC_assms rules that are wp rules. So it didn't really make that distinction.

So what this is doing is making use of rules declared [wp] in Arch in order to discharge locale assumptions without having to mark the relevant rules [whatever_assms]? I guess that makes sense; in theory if you put all the assms into the wp set, then wpsimp would solve all subgoals without further arguments?

It definitely was not obvious at first glance though, and even now I seek confirmation. If we want to go down this route, we might want to say something in the arch-split docs.

Xaphiosis · 2024-12-12T03:21:29Z

proof/access-control/RISCV64/ArchFinalise_AC.thy

+declare finalise_cap_valid_list[Finalise_AC_assms]
+declare arch_finalise_cap_pas_refined[Finalise_AC_assms]
+declare prepare_thread_delete_pas_refined[Finalise_AC_assms]
+declare finalise_cap_replaceable[Finalise_AC_assms]


what happened here? previously there was a crunch, and then we picked out the Finalise_AC_assms... did the crunch move elsewhere?

Signed-off-by: Ryan Barry <[email protected]>

Xaphiosis · 2024-12-12T03:27:35Z

proof/access-control/RISCV64/ArchSyscall_AC.thy

@@ -168,7 +169,7 @@ global_interpretation Syscall_AC_1?: Syscall_AC_1
 proof goal_cases
  interpret Arch .
  case 1 show ?case
-    by (unfold_locales; (fact Syscall_AC_assms | wp init_arch_objects_inv))
+    by (unfold_locales; wpsimp wp: Syscall_AC_assms)


same as my other comment, is it only wp rules in the assms? surprised it doesn't work with fact

Xaphiosis · 2024-12-12T03:30:42Z

proof/access-control/RISCV64/ArchCNode_AC.thy

+                  \<longrightarrow> vspace_for_pool pool_ptr asid (asid_pools_of s') =
+                      vspace_for_pool pool_ptr asid (asid_pools_of s);
+       bot_level < max_pt_level \<longrightarrow> pts_of s' = pts_of s \<rbrakk>
+   \<Longrightarrow> vs_lookup_table bot_level asid vref s' = vs_lookup_table bot_level asid vref s"


indentation:

⟹ vs_lookup_table should be under ⟦

vspace_for_pool indent should be by 2 instead of 1

Xaphiosis · 2024-12-12T03:32:18Z

proof/access-control/DomainSepInv.thy

+(* similarly, the preconditions here tend to contradict one another *)
+lemma invoke_control_domain_sep_inv:
+  "\<lbrace>domain_sep_inv irqs st and irq_control_inv_valid i\<rbrace>
+    invoke_irq_control i


indentation

Xaphiosis · 2024-12-12T03:33:38Z

proof/access-control/Arch_AC.thy

-  "\<lbrace>pspace_aligned and valid_vspace_objs and valid_arch_state and pas_refined aag\<rbrace>
-   set_mrs thread buf msgs
-   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
+  "set_mrs thread buf msgs \<lbrace>pas_refined aag\<rbrace>"


I really appreciate the style overhaul you've included in this PR

Xaphiosis · 2024-12-12T03:35:03Z

proof/access-control/ARM/ArchInterrupt_AC.thy

@@ -75,7 +74,7 @@ global_interpretation Interrupt_AC_1?: Interrupt_AC_1 "arch_authorised_irq_ctl_i
 proof goal_cases
  interpret Arch .
  case 1 show ?case
-    by (unfold_locales; (fact Interrupt_AC_assms)?)
+    by (unfold_locales; fact Interrupt_AC_assms)


you can keep this change, but should know the reason for (fact Interrupt_AC_assms)?. The reason that's useful is while developing, when this instantiation errors, you can see which fact you're missing from your assumption; with the non-? one, you get "proof command failed".

Xaphiosis · 2024-12-12T03:36:04Z

proof/access-control/ARM/ArchSyscall_AC.thy

@@ -179,7 +179,7 @@ global_interpretation Syscall_AC_1?: Syscall_AC_1
 proof goal_cases
  interpret Arch .
  case 1 show ?case
-    by (unfold_locales; (fact Syscall_AC_assms)?)
+    by (unfold_locales; wpsimp wp: Syscall_AC_assms)


I don't really see why the change to instantiating locale assumptions using wpsimp is an improvement. You're very consistent with it, so I'd like to hear your thoughts.

Xaphiosis · 2024-12-12T03:36:40Z

proof/access-control/ARM/ArchDomainSepInv.thy

+  by wpsimp
+
+lemma arch_post_modify_registers_domain_sep_inv[DomainSepInv_assms, wp]:
+  "arch_post_modify_registers cur x31 \<lbrace>domain_sep_inv irqs st\<rbrace>"


Xaphiosis · 2024-12-12T03:40:43Z

proof/access-control/AARCH64/ArchInterrupt_AC.thy

+
+context begin interpretation Arch .
+
+requalify_consts arch_authorised_irq_ctl_inv


Not for this PR, but there's tech to do this more efficiently, documented in docs/arch-split.md (arch_requalify_facts)

Xaphiosis · 2024-12-12T03:43:06Z

proof/access-control/AARCH64/ArchAccess_AC.thy

+
+lemma integrity_asids_update_autarch[Access_AC_assms]:
+  "\<lbrakk> \<forall>x a. integrity_asids aag {pasSubject aag} x a st s; is_subject aag ptr \<rbrakk>
+     \<Longrightarrow> \<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>kheap := (kheap s)(ptr \<mapsto> obj)\<rparr>)"


I'm guessing all of these lemmas with old-style ==> indents are only moved from elsewhere?

They are Tom-style indents, not old style indents. I don't think anybody else has used them :-)

Right, those are not new then, fine to leave as is

Xaphiosis · 2024-12-12T03:45:11Z

proof/access-control/AARCH64/ArchAccess.thy

+   | 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).


the | should line up

Xaphiosis · 2024-12-12T03:48:28Z

proof/access-control/AARCH64/ArchAccess.thy

+| "aobj_ref' (PageTableCap ref _ _) = {ref}"
+| "aobj_ref' (VCPUCap ref) = {ref}"
+
+fun acap_asid' :: "arch_cap \<Rightarrow> asid set" where


I'm not sure I understand the role of aobj_ref' and acap_asid'. Are there non-' versions? Why are they not what we want in access?

The ASpec versions don't return sets, which we do want here.

maybe _set instead of ' or a comment then?

Xaphiosis · 2024-12-12T03:51:01Z

proof/access-control/AARCH64/ArchAccess.thy

+  "'a PAS \<Rightarrow> 'a set \<Rightarrow> obj_ref \<Rightarrow> asid \<Rightarrow> 'y::state_ext state \<Rightarrow> 'z::state_ext state  \<Rightarrow> bool" where
+  "integrity_asids aag subjects x asid s s' \<equiv>
+   integrity_asids_aux aag subjects x asid (asid_table s) (asid_table s')
+                                           (asid_pools_of s) (asid_pools_of s')"


this is interestingly the other way round to the _2 setup we use in AInvs/Refine. There we want the abbreviation to expose the state projections, and the definition to hide the complicated bits and pieces. Here you get no benefit from the definition (need to unfold to benefit from the fact that the state projections don't change), and you don't get a real benefit from the abbreviation, because it doesn't hide the complexity ... thoughts?

It might be worth trying out what happens if we do it the "right" way around. It might conflict with old style in the Access session, but it'd be good to see if that is true.

Xaphiosis · 2024-12-12T04:09:53Z

proof/access-control/AARCH64/ArchADT_AC.thy

     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"


I'm a bit surprised this lemma is in Access and not in AInvs, but I guess it's only needed up here.

Xaphiosis

I think this is very good work. Sometimes it's hard to tell what got moved/copied, and my comments may be related to something that's just being consistent with other arches, in which case ignore those. Mostly I have nitpicks/style and some questions to try bridge gaps in my knowledge.

ryybrr added AC access control proofs Aarch64 AArch64-specific proofs, specs, etc labels Dec 11, 2024

ryybrr requested review from Xaphiosis, lsf37 and corlewis December 11, 2024 07:38

ryybrr self-assigned this Dec 11, 2024

lsf37 reviewed Dec 11, 2024

View reviewed changes

proof/invariant-abstract/AARCH64/ArchVCPU_AI.thy Outdated Show resolved Hide resolved

lsf37 reviewed Dec 11, 2024

View reviewed changes

proof/access-control/AARCH64/ArchFinalise_AC.thy Outdated Show resolved Hide resolved

lsf37 reviewed Dec 11, 2024

View reviewed changes

proof/access-control/AARCH64/ArchAccess.thy Show resolved Hide resolved

lsf37 approved these changes Dec 11, 2024

View reviewed changes

ryybrr added 2 commits December 12, 2024 13:07

access: relax conditions

357ccc9

-Remove various instances of pspace_aligned, valid_vspace_objs, and valid_asid_table/valid_arch_state from preconditions -Relax the is_subject predicate in various Syscall_AC lemmas Signed-off-by: Ryan Barry <[email protected]>

aarch64 access: copy riscv64 theories

ea0ab79

Signed-off-by: Ryan Barry <[email protected]>

Xaphiosis reviewed Dec 12, 2024

View reviewed changes

aarch64 aspec+ainvs+access: access control modulo sorries

2048660

Signed-off-by: Ryan Barry <[email protected]>

ryybrr force-pushed the aarch64-access-setup branch from 5ab11b7 to 2048660 Compare December 12, 2024 03:23

Xaphiosis reviewed Dec 12, 2024

View reviewed changes

Xaphiosis approved these changes Dec 12, 2024

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

AArch64 Access Control: initial setup #837

AArch64 Access Control: initial setup #837

ryybrr commented Dec 11, 2024

lsf37 Dec 11, 2024

lsf37 left a comment

Xaphiosis Dec 12, 2024

Xaphiosis Dec 12, 2024

lsf37 Dec 12, 2024

Xaphiosis Dec 12, 2024

Xaphiosis Dec 12, 2024

Xaphiosis Dec 12, 2024

Xaphiosis Dec 12, 2024

Xaphiosis Dec 12, 2024

Xaphiosis Dec 12, 2024

Xaphiosis Dec 12, 2024

Xaphiosis Dec 12, 2024

Xaphiosis Dec 12, 2024

Xaphiosis Dec 12, 2024

Xaphiosis Dec 12, 2024

Xaphiosis Dec 12, 2024

lsf37 Dec 12, 2024

Xaphiosis Dec 12, 2024

Xaphiosis Dec 12, 2024

Xaphiosis Dec 12, 2024

lsf37 Dec 12, 2024

Xaphiosis Dec 12, 2024

Xaphiosis Dec 12, 2024

lsf37 Dec 12, 2024

Xaphiosis Dec 12, 2024

Xaphiosis left a comment


		context begin interpretation Arch .

		requalify_consts arch_authorised_irq_ctl_inv

AArch64 Access Control: initial setup #837

Are you sure you want to change the base?

AArch64 Access Control: initial setup #837

Conversation

ryybrr commented Dec 11, 2024

Choose a reason for hiding this comment

lsf37 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Xaphiosis left a comment

Choose a reason for hiding this comment