AArch64: support SMC calls in verified kernel #945

lsf37 · 2025-12-14T23:36:30Z

This adds support for SMC (Secure Monitor Calls), see also RFC-9.

Currently, this forces KernelAllowSMCCalls to be ON for AArch64 builds. The plan is to remove all SMC ifdefs in the C code apart from the one that provides the initial SMC master cap at boot. (Or, if people are happy with that, just have SMC always on, because the initialiser will not pass on the SMC master cap if it is not explicitly requested).

The main proof change on the generic interface side is the introduction of arch_cap_badge/arch_capBadge, which was necessary because the proofs previously assumed that arch caps never have a badge that is managed with the standard badge mechanisms.

Since we know nothing about the actual content of SMC operations, the best we can do is assume that the doSMC_mop will only modify machine state the kernel does not manage, and leave kernel-visible memory unchanged. This appears to be a true assumption in how SMC is used so far in seL4 (power management and device access). Other uses will have to make their own assessment.

There is a companion seL4 PR (seL4/seL4#1572) with a minor code refactor that aligns the C more to the usual decode/invoke split and argument passing. Not behaviour change is intended.

During the proofs it came up that the capclass definition was placed in a generic ASpec file, but has architecture-specific content (e.g. IOPorts). It turns out that we only make use of 3 actual cap classes: physical, reply, and the rest. Since this still works in the generic setting, instead of arch splitting the type, I have adjusted it into these 3 classes in a separate commit at the end. The initial ASpec commit for SMC caps introduces an SMCClass which is later removed in that consolidation.

Test with: seL4/seL4#1572

lsf37 · 2025-12-14T23:41:15Z

@michaelmcinerney this one should not break MCS proofs -- even though it introduces new interface constants, the C code changes are all constrained to AArch64.

lsf37 · 2025-12-14T23:52:25Z

I should mention that I had to move around some lemmas and definitions in CRefine: the auxiliary definition of setMR (we only have setMRs in Haskell, but C has setMR) needed a common ancestor between Arch_R and Ipc_R, which was a bit tricky to find -- the monad definitions could go into TcbAcc_C, where I think it makes sense, but the setMR_ccorres lemma only works further down in SyscallArgs_C because it needs the helper lemmas defined there (I tried moving those up, but that pulls out a whole tree of dependencies). setMR does make some sense in SyscallArgs because it is for the system call protocol, so I don't think it's too terrible.

proof/crefine/AARCH64/Arch_C.thy

Xaphiosis · 2025-12-18T20:40:43Z

spec/design/skel/AARCH64/ArchRetype_H.thy

 context Arch begin arch_global_naming (H)

-#INCLUDE_HASKELL SEL4/Object/ObjectType/AARCH64.hs CONTEXT AARCH64_H Arch.Types=ArchTypes_H ArchInv=ArchRetypeDecls_H NOT bodies_only
+#INCLUDE_HASKELL SEL4/Object/ObjectType/AARCH64.hs CONTEXT AARCH64_H Arch.Types=ArchTypes_H ArchInv= NOT bodies_only


Looking in this commit and reading the commit message, I'm wondering if the other way of going about these would be to do the global. vs Arch. renaming dance as we do for arch-split (the context begin global_naming global one).

The reason I bring it up is because the commit message has a "it works by coincidence now" vibes, but I'm not 100% on what's going on.

It worked purely by coincidence before (because it was basically unused) and works more reliably now, but it does not yet fully work without restrictions. It would make sense to look at this a bit more globally separately, because you are right, it would be nice to have a proper documented general solution for this.

Xaphiosis · 2025-12-18T20:50:31Z

commit nitpicks/suggestions while I warm up:

declare constants for SMC caps doesn't declare the consts, only flags them for import?
Haskell is using -> Haskell uses
It appears that "||" has been correctly -> should that be \|? Confused
Similarly to AInvs in the previous commit, this commit introduces -> ..., introduce ?
This introduces -> Introduces
This commit introduces -> Introduce
orphanage -> Orphanage
arm+arm-hyp+riscv_x64 should have a + there, and arch_cap_bade should be badge

Also, is the plan to squash any of these at the end, or leave as is? The other thing is that the order is a bit strange. I was expecting a story, like aspec, then haskell / design infrastructure, then aarch64 proofs, and then mop-up operations for other arches. The later parts seem in order, but at the start it's a bit confusing to follow since I'm reviewing commit-by-commit.

spec/machine/AARCH64/MachineOps.thy

tools/haskell-translator/lhs_pars.py

Xaphiosis · 2025-12-18T21:17:12Z

spec/haskell/src/SEL4/Object/ObjectType/AARCH64.hs


 updateCapData :: Bool -> Word -> ArchCapability -> Capability
+updateCapData preserve newBadge (SMCCap badge) =
+    if not preserve &&  badge == 0


two spaces?

do you mean indent by 2 instead of 4? Haskell uses 4, no? (at least everything else in this file does)

Xaphiosis · 2025-12-18T21:18:52Z

spec/haskell/src/SEL4/Object/ObjectType/AARCH64.hs

+    unless (invocationType label == ArchInvocationLabel ARMSMCCall) $ throw IllegalOperation
+    unless (length args >= numSMCRegs) $ throw TruncatedMessage
+    smcFuncID <- return $ args !! 0
+    when (badge /= 0 && badge /= smcFuncID) $ throw IllegalOperation


can you refresh my memory: what is the significance of badge 0?

It's like for endpoints and notifications: badge 0 means it is the unbadged "master" cap which has more authority than badged caps. For SMC caps that additional authority means it can invoke any SMC function.

proof/invariant-abstract/AARCH64/ArchTcb_AI.thy

proof/invariant-abstract/Tcb_AI.thy

Xaphiosis · 2025-12-18T21:37:17Z

proof/refine/CSpace1_R.thy

  is_derived'
  capASID cap_asid_base' cap_vptr' (* needed to define weak_derived' *)
+  arch_capMasterCap
+  arch_capBadge


interesting that this was not needed before

arch_capBadge is new and the interface lemma about it talks about arch_capMasterCap. We don't have that many separate generic properties about arch caps, so I guess this is the first time we make an interface that manages to go by master cap instead of something more specific.

proof/refine/CSpace1_R.thy

Xaphiosis · 2025-12-18T21:41:39Z

proof/refine/AARCH64/CNodeInv_R.thy

   apply simp
   apply (erule_tac x=p' in allE)
-   apply (solves \<open>clarsimp simp: mdb_next_unfold\<close>)
+   apply (rule conjI; solves \<open>clarsimp simp: mdb_next_unfold\<close>)


do you really need the conjI here? surprising

It does for speed. fastforce and the other more aggressive tactics go down a wrong path and take forever.

proof/refine/AARCH64/CNodeInv_R.thy

Xaphiosis · 2025-12-18T21:49:34Z

proof/refine/AARCH64/ArchCSpace_I.thy

     | FrameCap _ _ _ _ m \<Rightarrow> m
-     | PageTableCap _ _ m \<Rightarrow> m"
+     | PageTableCap _ _ m \<Rightarrow> m
+     | _ \<Rightarrow> None"


hmm, I think we had this discussion before, whether we want to have the benefit of complete pattern match without dummy; in this case I think I'd like having the SMC cap here and no default

We did have the discussion for Haskell, but I don't think we did for Isabelle.

For Isabelle, I definitely don't agree (for Haskell I partially I agree, depending on context). In this case, it is specifically an Isabelle function for extracting info from VM caps. You don't get a warning for missing cases, you just get undefined, which is worse (I actually hit that). I would only be adding noise if I added cases for other caps. I would in fact argue that we should remove the ASIDControlCap case, because it obscures what is going on.

If we had written it with the default case in the first place, I would not have had to backtrack from the failed proof and edit this definition. If I had been adding a VM cap instead, I might still have missed this case, and have had to backtrack from a failed proof, but that is no worse than what we have now. So the default case is strictly better for this.

I don't want to go as far as saying that default cases are always better for Isabelle definitions, but for these extractor functions, I'm pretty sure.

proof/refine/AARCH64/ArchCSpace1_R.thy

Xaphiosis · 2025-12-18T22:08:14Z

proof/crefine/AARCH64/Machine_C.thy

+     \<lambda>(x0, x1, x2, x3, x4, x5, x6, x7).
+       smc_args_t__C (ARRAY i. [x0, x1, x2, x3, x4, x5, x6, x7] ! i)"
+
+end


why context kernel for this one, instead of dumping it into kernel_m below? I don't remember how long it takes to enter/leave kernel context, but I don't think it's fast; might be a little faster to say definition (in kernel) if you really want it to be in kernel here

I think I had to do that, because it is also used in theories that are not using kernel_m, but just kernel (I was surprised to find out these existed, but there is a whole bunch of theories that don't need any machine interface assumptions, and they are not using kernel_m).

proof/crefine/AARCH64/CSpace_C.thy

Xaphiosis · 2025-12-18T22:19:27Z

proof/crefine/AARCH64/Arch_C.thy

+                   unified back into just msg_len which is the variable we wanted to get rid of.
+                   Rewriting with word_of_nat_8_n_msgRegisters makes the schematic parameter
+                   different from the message length parameter in the program and prevents that
+                   unwanted unification *)


I am getting the feeling I would have changed the C somehow to prevent this loop unrolling and related mess, especially since the number is fixed in the SMC spec to 8. Out of curiosity, was this not possible?

You mean unroll the loop in C directly? That could be done, but it is kinda ugly and unidiomatic and doesn't really help much, because the issue is mostly on the abstract/Haskell side where setMR is supposed to return how many registers where actually transferred. We'd still be ignoring the first 7 of these return values and then match up the 8th one.

We could also unroll fully in Haskell/abstract, but it's a lot repetition. This way, the repetition is confined to the proof. The main annoyance is that we can't avoid the repetition in the proof without proving new rules that do not really warrant the complexity they would need. Hence the proof methods and comments.

If you want to confine it to the proof, would unrolling via monadic_rewrite or something like that work?

rewriting was my first idea for this as well, but it doesn't work, because you have to unroll both sides simultaneously, and we don't have good infrastructure for doing that on the C side. I was halfway through trying to do something with ccores_rewrite, when I realised that we have all of the necessary infrastructure available to do this directly in the proof. It is a bit ugly, but the alternatives are a lot bigger and not prettier.

Xaphiosis · 2025-12-18T22:20:10Z

proof/crefine/AARCH64/Arch_C.thy

+           apply wpsimp
+          apply wpsimp
+         apply wpsimp
+        apply wpsimp


worth using a ((wpsimp ...)+)[n] here?

Hm, 4 is roughly my threshold for these. I find the double parenthesis thing not so nice to read and it is a bit unwieldy in maintenance, because you tend to have to unroll them when something breaks. If there were 7 of these, sure. 4 I think are borderline, but still fine.

I'm happy to be overruled on this one if people have strong opinions about it, though. I'm more explaining how I got there than saying that this is how it should be.

proof/crefine/AARCH64/Arch_C.thy

spec/abstract/CSpace_A.thy

Xaphiosis · 2025-12-18T22:31:59Z

spec/abstract/CSpace_A.thy

+text \<open>@{const PhysicalClass} is for caps to objects that consume physical
+memory. This includes anything that can be retyped from Untyped caps.
+@{const ReplyClass} is specifically for reply caps. @{const OtherCapClass} for
+anything else.\<close>


might also want to indent per style guide

The rest of this file doesn't indent on text, and since it's using it consistently I think I'd prefer leaving it until we update the entire thing at some point.

proof/invariant-abstract/ARM_HYP/ArchCSpaceInvPre_AI.thy

proof/refine/X64/Tcb_R.thy

Xaphiosis

I have the usual pile of questions and nitpicks, but looks good from my side. That C loop thing though, wow. Wouldn't have come up with that easily.

Haskell uses the prefix "ArchInvs." to refer to arch specific invocations, but in Isabelle those are in the global name space and will error if accessed via "ArchRetypeDecls_H.". So far, all of the "ArchInvs." occurrences happened to be only in caseconvs where they were manually translated without prefix. Now there are some occurrences that come through the Haskell translator directly. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

The string "\|" is invalid in python and has so far only been interpreted correctly by accident. Since we don't want the operator |, we do want the \ in the resulting string. The previous non-raw string "\|\|" was interpreted as "||", and it appears that "||" has in turn been correctly interpreted as the character | twice, not the operator | twice, but we should not rely on that. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Print translation string for unknown type assignments with parameters -- this is the part that needs to go into the "known types" list. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

lsf37 · 2026-01-08T23:39:54Z

commit nitpicks/suggestions while I warm up:

declare constants for SMC caps doesn't declare the consts, only flags them for import?

Haskell is using -> Haskell uses

It appears that "||" has been correctly -> should that be \|? Confused

Similarly to AInvs in the previous commit, this commit introduces -> ..., introduce ?

This introduces -> Introduces

This commit introduces -> Introduce

orphanage -> Orphanage

arm+arm-hyp+riscv_x64 should have a + there, and arch_cap_bade should be badge

Thanks, all done.

Also, is the plan to squash any of these at the end, or leave as is?

I was planning to leave them as is, but happy to squash more if there are suggestions. We could squash all of the aarch64 proofs into one commit, for instance. I don't have a big preference either way.

The other thing is that the order is a bit strange. I was expecting a story, like aspec, then haskell / design infrastructure, then aarch64 proofs, and then mop-up operations for other arches. The later parts seem in order, but at the start it's a bit confusing to follow since I'm reviewing commit-by-commit.

True, the current version did not have a good flow. I have now tried to group it as:

general tool and import fixes
machine
Haskell
tool fixes that depend on Haskell update, caseconvs
design
aspec
aarch64 proofs
other proofs

(ASpec doesn't build without the Haskell update, hence Haskell first)

SMC caps add the ability to make SMC (Secure Monitor Call) invocations on AArch64. See RFC-9 for more details: https://sel4.github.io/rfcs/implemented/0090-smc-cap.html Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Add the translations of "EightTuple a" and "FPUState" as known to the translator to avoid warnings. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

numSMCRegs and doSMC_mop are imported from machine/ Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

This introduces a new cap class SMCClass in generic CSpace_A. The plan is to later consolidate cap classes so that most cap changes no longer require any update to the `capclass` data type. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Introduce a new arch_cap_badge interface. The previous definition of cap_badge made the assumption that arch caps will never have a badge, but SMC caps do. This comes with a few interface lemmas about arch_cap_badge, which allow us to keep existing lemmas about cap_badge generic. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Similarly to AInvs in the previous commit, introduce an arch_capBadge interface with corresponding lemmas since SMC caps have badges and use the general badge mechanisms. The previous assumption that arch caps do not have badges also comes out in the is_arch_update' predicate which now needs to explicitly demand that the cap badge is None. This actually simplifies some proofs in the architecture dependent part, but needs minor updates in Orphanage. Also move up the definition of arch_cap'_fun_lift and introduce an abbreviation arch_cap'_pred that can be used to lift arch cap predicates to all caps (returning False on generic caps). Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Adjustments for new arch_cap_badge/arch_capBadge interface. Mostly trivial. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

lsf37 added the seL4-PR requires merging a corresponding seL4 pull request label Dec 14, 2025

lsf37 requested review from Xaphiosis and corlewis December 14, 2025 23:40

lsf37 force-pushed the smc-caps branch from da3374f to 969658e Compare December 14, 2025 23:42

lsf37 commented Dec 15, 2025

View reviewed changes

proof/crefine/AARCH64/Arch_C.thy Outdated Show resolved Hide resolved

lsf37 force-pushed the smc-caps branch 2 times, most recently from cdd2456 to 60cfba2 Compare December 15, 2025 03:50

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