RFC-21: Unify behaviour of the Page Map invocation

[Kswin01]

This RFC proposes to enforce the same over-map behaviour of the page map invocation across all architectures. That is,
prevent over-mapping on all architectures.

A draft implementation for preventing overmapping can be found here: seL4/seL4#1526.
The associated sel4test changes/additions can be found here: seL4/sel4test#148.

[lsf37]

My main question on this is: why not change the behaviour of RISC-V and allow overmapping everywhere? It is the smaller change and is more permissive. And it is perfectly safe from the kernel's perspective.

Overmapping will create FrameCaps with stale mapping information, but deleting page tables already does the same, so the kernel still has to deal with the issue.

I don't think we should restrict behaviour if we don't need to.

[Kswin01]

Yep, that's a valid approach as well that I mentioned in the alternatives section. I have no strong feelings either way, whether that be allowing or preventing over-mapping on all architectures. The change will be a lot simpler for allowing over-mapping on RISCV, and in my mind it would impact less existing users.

[Indanz]

The argument against allowing overmapping is that in 99% of cases when it happens, it's done accidentally, and debugging this mistake is hard. Not allowing it would make seL4 more user friendly. For the 1% of cases where it is done deliberately, people can easily unmap before remapping. (Edit: But a debug print would solve this issue though.)

Another argument is that with the current convoluted API you need both a VSpace cap and a page cap to control a VSpace. If you allow overmapping, you can effectively revoke someone else's page cap without having access to it. Deleting page tables is not the same, as those have explicit control over a subset of the virtual address space.

But if the goal is consistency, then allowing it on RISCV is indeed the more practical solution.

[lsf37]

Considering the verification cost for the change, I think adjusting RISC-V so that it aligns with the other architectures instead of disallowing overmapping is the right choice.

Basically, I can verify the removal of the RISC-V check on the side without too much effort, but the added checks proposed in the draft implementation are more work. We'd need to include that in some funded project somewhere and I don't see the change making sense for hiding under ifdef.

The revoke caveat is already documented as such for all other architectures and you do need a VSpace cap to get there, which means you already have authority over the VSpace and can do worse things to it (which is why this is passing integrity and confidentiality proofs).

[lsf37]

The TSC meeting on 3 Dec 2026 deferred approval on this RFC, but encourages progress for

• adding over-mapping checks on the remaining platforms
• while allowing access rights upgrade/downgrade
• approval will need a verification plan

When a corresponding implementation PR is available, Gerwin volunteered to estimate verification effort.