AArch64 Information Flow: initial setup #944

ryybrr · 2025-12-06T05:42:29Z

Partial information flow proofs for AArch64. Please see c75ee1a when reviewing the bulk of the changes as this provides the most minimal diff.

Removed various instances of pspace_aligned, valid_vspace_objs, and
valid_arch_state. This mirrors previous cleanup efforts for access control (see: a759ea1).
Strengthened domain_sep_inv, allowing proofs to relate getActiveIRQ instances with different flags.
Ported the RISCV64 InfoFlow proofs to AARCH64. The majority of breakages have been addressed, with outstanding proof obligations deferred using the sorry command. Additional context is provided by FIXME AARCH64 IF comments in the theory files.

Remove various instances of pspace_aligned, valid_vspace_objs, and valid_arch_state Signed-off-by: Ryan Barry <[email protected]>

Assert that non-kernel IRQs are non-timer IRQs Signed-off-by: Ryan Barry <[email protected]>

Use the RISCV64 InfoFlow proofs as a basis for AARCH64. Proofs have been copied verbatim modulo renaming the architecture. Signed-off-by: Ryan Barry <[email protected]>

Initial sorry run for AARCH64 InfoFlow proofs Signed-off-by: Ryan Barry <[email protected]>

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

Xaphiosis · 2025-12-08T02:33:40Z

run_tests


-EXCLUDE["ARM"]=[]
+EXCLUDE["ARM"]=[
+    "InfoFlow" # for development only


I don't understand. You're saying "build InfoFlow with sorries" in ROOT in this commit, but you're disabling InfoFlow testing for all arches that had it? Wouldn't we want to still test those arches, but have AARCH64 run through with sorries?

Unless there are changes to the generic files that are temporarily breaking the infoflow proofs on ARM/RISCV. @ryybrr is that the case? If not, we should indeed not remove them.

Yep, have made changes to the generic files without updating ARM/RISCV. I was planning to leave them for now; since this PR also includes partial proofs, the interface may shift further. If you'd prefer, I could see if it's a quick fix?

It's worth checking out, but not high priority. We're not expecting this to be a very long-lived branch.

Xaphiosis · 2025-12-08T02:36:32Z

proof/infoflow/RISCV64/ArchUserOp_IF.thy

+           apply fastforce
+           apply fastforce
+           apply fastforce
+           apply fastforce


proof indentation

Xaphiosis · 2025-12-08T02:38:45Z

proof/infoflow/FinalCaps.thy

+lemma thread_set_tcb_arch_update_silc_inv[wp]:
+  "\<lbrace>silc_inv aag st\<rbrace>
+   thread_set (tcb_arch_update blah) t
+   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"


trivial: can use thread_set (tcb_arch_update blah) t ⦃silc_inv aag st⦄ short syntax for same pre/post and no rv

proof/infoflow/ADT_IF.thy

Xaphiosis · 2025-12-08T02:43:07Z

proof/infoflow/AARCH64/ArchADT_IF.thy

+  done
+
+lemma thread_set_context_state_hyp_refs_of[CNode_AC_assms]:
+  "thread_set (tcb_arch_update (arch_tcb_context_set ctxt)) t \<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace>"


this kind of thing feels like it could be moved to AInvs during cleanup, possible FIXME move?

I should be able to cut it altogether. CNode_AC_assms appearing here makes me think it's an unused remnant from WIP proofs.

Likely. I think normally we don't unfold it, i.e.

lemma arch_thread_set_is_thread_set: "arch_thread_set f t = thread_set (tcb_arch_update f) t"

but then we have this:

lemma arch_thread_set_sym_refs_hyp': "⟦⋀tcb. hyp_refs_of (TCB tcb) = hyp_refs_of (TCB (tcb_arch_update f tcb))⟧ ⟹ arch_thread_set f t ⦃λs. P (state_hyp_refs_of s)⦄

which can't be interfaced directly. There's an instantiated version for FPU state, but not one for state_hyp_refs_of. There's also an ominous comment a bit above it in ArchTcbAcc_AI:

― ‹FIXME: Shouldn't state_hyp_refs_of be generic? If it was, then this and arch_thread_set_sym_refs_hyp' could be generic as well›

so that might be worth fixing up.

Xaphiosis · 2025-12-08T02:43:36Z

proof/infoflow/AARCH64/ArchADT_IF.thy

+   apply (wps thread_set_state_vrefs thread_set_context_state_hyp_refs_of)
+   apply (rule hoare_lift_Pf2[where f="caps_of_state"])
+    apply (rule hoare_lift_Pf2[where f="thread_st_auth"])
+     apply (rule hoare_lift_Pf2[where f="thread_bound_ntfns"])


no chance for wps for these?

I'll review, but I recall there being a reason why it didn't work.

Xaphiosis · 2025-12-08T02:44:12Z

proof/infoflow/AARCH64/ArchCNode_IF.thy

+  "irq_at pos masks \<equiv> let i = irq_oracle pos in (if masks i then None else Some i)"
+
+lemma dmo_getActiveIRQ_globals_equiv[CNode_IF_assms]:
+  "\<lbrace>globals_equiv st\<rbrace> do_machine_op (getActiveIRQ in_kernel) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>"


can use short form

Xaphiosis · 2025-12-08T02:45:07Z

proof/infoflow/AARCH64/ArchIpc_IF.thy

+lemma arch_thread_get_reads_respects[wp]:
+  "reads_respects aag l (K (aag_can_read_or_affect aag l t)) (arch_thread_get f t)"
+  unfolding arch_thread_get_def
+  apply (wpsimp)


parentheses, can use two line by proof

Xaphiosis · 2025-12-08T02:52:01Z

proof/infoflow/AARCH64/ArchUserOp_IF.thy

+  apply (rename_tac n)
+  apply (case_tac n; clarsimp)
+   apply (clarsimp simp: pt_bits_left_def pageBits_def ptTranslationBits_def max_pt_level_def asid_pool_level_def split: if_splits)
+   apply (clarsimp simp: pt_bits_left_def pageBits_def ptTranslationBits_def max_pt_level_def asid_pool_level_def pt_bits_left_bound_def split: if_splits)


AARCH64 we have level_defs and bit_simps which should greatly reduce the amount of things you need to mention; you can find them by doing:

find_names asid_pool_level_def find_names ptTranslationBits_def

Not directly related, but these lemmas tagged with FIXME AARCH64 IF: move were copied from other architectures as I couldn't find equivalent rules. Do you know if something similar exists for AARCH64 already?

RISCV64 has these in ArchInvariants_AI.thy but I'm not seeing anything in AARCH64 (if you mean "is there something like pt_bits_left_le_canonical already in AARCH64)

Xaphiosis · 2025-12-08T02:53:17Z

proof/infoflow/AARCH64/ArchUserOp_IF.thy

+    apply (clarsimp simp: pt_lookup_slot_def)
+    apply (rule_tac pt_lookup_slot_from_level_is_subject)
+            apply fastforce+
+  apply (rule requiv_get_pt_entry_eq; fastforce)


potentially can fold into previous with intro!: requiv_get_pt_entry_eq, no?

Xaphiosis · 2025-12-08T02:56:16Z

proof/infoflow/AARCH64/ArchNoninterference.thy

+   \<lbrace>P\<rbrace>"
+  apply (simp add: do_machine_op_def getActiveIRQ_def non_kernel_IRQs_def)
+  apply (wp modify_wp | wpc)+
+  apply clarsimp


wpsimp usually supplants wpc and clarsimp

Xaphiosis · 2025-12-08T02:57:49Z

proof/infoflow/AARCH64/ArchFinalCaps.thy

+  for silc_inv[FinalCaps_assms, wp]: "silc_inv aag st"
+  (wp: crunch_wps)
+
+


extra newline?

Xaphiosis · 2025-12-08T03:00:22Z

proof/infoflow/AARCH64/ArchArch_IF.thy

+   \<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
+  unfolding set_cap_def
+  apply (simp only: split_def)
+  apply (wp set_object_globals_equiv hoare_vcg_all_lift get_object_wp | wpc | simp)+


wpsimp possible here?

Xaphiosis · 2025-12-08T03:03:12Z

proof/infoflow/AARCH64/ArchArch_IF.thy

             | InvokePage oper \<Rightarrow> authorised_for_globals_page_inv oper
             | _ \<Rightarrow> \<top>"

+(*


tag with FIXME?

Xaphiosis · 2025-12-08T03:04:29Z

proof/infoflow/AARCH64/ArchDecode_IF.thy

+  notes reads_respects_f_inv' = reads_respects_f_inv[where st=st]
+  notes whenE_wps[wp_split del]
+  shows reads_respects_f_check_vspace_root[wp]:
+  "reads_respects_f aag l \<top> (check_vspace_root cap arg)"


hang on, can't the name move from the shows to the lemma? this is very unusual format

Agreed, unless we have multiple parts to the shows (separated with and), the name should be at lemma so it remains searchable.

Xaphiosis · 2025-12-08T03:05:26Z

proof/infoflow/AARCH64/ArchDecode_IF.thy

+  apply (clarsimp simp: valid_arch_cap_def wellformed_mapdata_def)
+  done
+
+lemma helper:


helper is a poor name, usually these are named after the lemma(s) they help with (e.g. blah_update_helper)

This part of the file comes under a previous FIXME AARCH64 IF: proof cleanup comment, so ideally this lemma would be removed altogether. I wanted to brute force a proof but didn't have the time to perform the proper cleanup.

Xaphiosis · 2025-12-08T03:10:11Z

Proof-wise, the quality is very good, thank you. I found some nitpicks while looking around to figure out what's going on (as I'm a rather behind on the Access/InfoFlow comprehension).

My main concern for this one is for the comprehension/longer-term maintenance aspect. Commits:

relax assumptions : were these unnecessary assumptions? what's the reason for their removal? might want to say that in the commit message, even briefly
access: strengthen domain_sep_inv: again, I feel like there was discussion about this. The commit only says what the commit contains, but is this a conclusion of some deeper discussion?

None of the commits say anything about what's happened, what's majorly different/difficult for AARCH64 (e.g. the kernel interrupt situation). I feel like we'd want more of the "why" in the historical record. I looked through the commits and didn't see any comments talking about any of this stuff either (indeed, not many comments at all aside from the FIXMEs).

Now, it may be the case that the interrupt situation was already handled by Access and I missed it somehow, or the problem is brushed under the sorries at the moment (fine for initial setup), but I feel like I would've come across some trace of documentation in this one.

ryybrr added 5 commits December 6, 2025 15:20

arm+riscv64 infoflow: relax assumptions

747da25

Remove various instances of pspace_aligned, valid_vspace_objs, and valid_arch_state Signed-off-by: Ryan Barry <[email protected]>

access: strengthen domain_sep_inv

0b1b2d2

Assert that non-kernel IRQs are non-timer IRQs Signed-off-by: Ryan Barry <[email protected]>

aarch64 infoflow: copy riscv64 theories

8413530

Use the RISCV64 InfoFlow proofs as a basis for AARCH64. Proofs have been copied verbatim modulo renaming the architecture. Signed-off-by: Ryan Barry <[email protected]>

aarch64 infoflow: initial setup

c75ee1a

Initial sorry run for AARCH64 InfoFlow proofs Signed-off-by: Ryan Barry <[email protected]>

run_tests: enable InfoFlow for AARCH64

b0a237c

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

ryybrr requested review from Xaphiosis, corlewis and lsf37 December 6, 2025 05:42

Xaphiosis reviewed Dec 8, 2025

View reviewed changes

proof/infoflow/RISCV64/ArchUserOp_IF.thy

apply fastforce

apply fastforce

apply fastforce

apply fastforce

Copy link

Member

Xaphiosis Dec 8, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

proof indentation

Xaphiosis reviewed Dec 8, 2025

View reviewed changes

proof/infoflow/ADT_IF.thy Show resolved Hide resolved

Xaphiosis reviewed Dec 8, 2025

View reviewed changes

proof/infoflow/AARCH64/ArchFinalCaps.thy

for silc_inv[FinalCaps_assms, wp]: "silc_inv aag st"

(wp: crunch_wps)

Copy link

Member

Xaphiosis Dec 8, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

extra newline?

Xaphiosis reviewed Dec 8, 2025

View reviewed changes

lsf37 added the Aarch64 AArch64-specific proofs, specs, etc label Dec 15, 2025

		for silc_inv[FinalCaps_assms, wp]: "silc_inv aag st"
		(wp: crunch_wps)

AArch64 Information Flow: initial setup #944

Are you sure you want to change the base?

AArch64 Information Flow: initial setup #944

Uh oh!

Conversation

ryybrr commented Dec 6, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Xaphiosis Dec 8, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Xaphiosis commented Dec 8, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Xaphiosis Dec 8, 2025 •

edited

Loading