Prevent overmapping on aarch32, aarch64, x86

[alwin-joshy]

Last year, I published a pre-rfc regarding new mapping operations which allowed you to batch unmaps and access right changes in order to make operations on a process' virtual address space more efficient. While discussing the RFC, we found some problems with my implementation based on a misunderstanding of if over-mapping is allowed to occur.

Over-mapping refers to when you overwrite an existing mapping with a new one i.e. you invoke seL4_ARCH_map on a frame cap B and overwrite an existing mapping of a page that was backed by frame cap A. My implementation assumed that over-mapping was always allowed to happen and left stale capabilities, since frame cap A would retain internal book-keeping which linked it to the page even though it was now associated with frame cap B.

The reason I thought this is because the ARM and x86 platforms both allow for over-mapping to occur, and I was originally developing my code on AARCH64. However, spurred on by the issues raised in the RFC, I looked into the implementation of the Page_Map on RISCV and found that it did not allow over-mapping. This means that there are different semantics in the implementation of mapping pages between the architectures, which is likely problematic. As pointed out by Kent in the RFC discussion, the API states that seL4_DeleteFirst should be returned if A mapping already exists in <texttt text="vspace"/> at <texttt text="vaddr", which seems to suggest that the RISCV interpretation is correct.

This PR changes all of the architectures to be consistent with the behavior of RISCV. It passes the seL4test suite on x86_64 and aarch64 but breaks the PT0002 test on AARCH32, as this relies on overmapping. I have also added a set of new tests across these architectures to check that overmapping no longer works.

Test with: seL4/sel4test#88

[kent-mcleod]

Would this check also work as if (pde_paddr && pde_paddr != base)? Which is encoding: Either the current pde entry isn't mapped, or if it is mapped, the destination paddr isn't being changed. Additionally, would it be better to test the actual bit for a valid mapping instead of a 0 paddr which could be a valid mapping address?

[alwin-joshy]

I thought about doing it like that initially since it doesn't require you to pass around the frame_asid but the behaviour would be a little different between riscv and the other archs.

As an example, suppose you have frame cap A which refers to frame X of physical memory. You do a seL4_ARCH_Page_Map(frame_cap_A, vaddr, ...) so that the page vaddr lies in is backed by frame X with frame cap A. You then make a copy of frame cap A with seL4_CNode_Copy, which gives you frame cap B. This also points to frame X of phsyical memory but has asid = asidInvalid and mapped_address = NULL.

If we implemented it as if (pde_paddr && pde_paddr != base), I believe doing seL4_ARCH_Page_Map(frame_cap_B, vaddr, ...) would not work on RISCV but would work on the other architectures.

EDIT: If it would be okay to change RISCV to have the same behaviour, then I think it would also be okay to have this. However, I'm not super clear on the nuances of when we want to allow over-mapping or if this case is even considered over-mapping, so if that's cleared up I don't mind changing them to do this instead.

As for the second part of your question, yeah I suppose that might be better. I thought a paddr of 0 would be an invalid address for some reason.

[kent-mcleod]

Right, I think that it might be easier to follow if instead of passing the frame_asid in and testing whether it is invalid or not, to instead pass in a flag indicating whether the mapping is new or an update. If it is new, it should then fail if there's already a mapping in the page table slot. If it's an update then the asid is guaranteed to match because of earlier checks. But what about if the physical address doesn't match? This could happen if the page table was deleted and then recreated as this wouldn't invalidate any existing frame caps.

[alwin-joshy]

Right, but I thought this scenario fell under the other kind of stale cap behavior that was documented and should be allowed. Or do you think that this is something that needs to be addressed as well?

[lsf37]

This PR changes existing API behaviour and needs an RFC first.

There is no reason per se why the behaviour should have to be the same on all architectures, so some policy-level discussion should be had wether we want this kind of consistency in general, and if yes if we should instead change the RISC-V behaviour.

Since there are conflicts accumulating, I'll close this PR for now. This is not to say this wouldn't be a valid candidate implementation if an RFC discussion would resolve in this direction. Happy for the PR to be re-opened when it comes to that.

[Indanz]

This PR changes existing API behaviour and needs an RFC first.

Agreed.

There is no reason per se why the behaviour should have to be the same on all architectures, so some policy-level discussion should be had wether we want this kind of consistency in general, and if yes if we should instead change the RISC-V behaviour.

Disagreed. Kernel policy decisions like these should be the same on all architectures. It's okay if behaviour is different because of actual architectural differences (or proof reasons following from those), but that isn't the case here I think.

Edit: That said, fixing this may introduce too much proof work at this point to make it practical though. The diff is bigger than I expected.

Since there are conflicts accumulating, I'll close this PR for now. This is not to say this wouldn't be a valid candidate implementation if an RFC discussion would resolve in this direction. Happy for the PR to be re-opened when it comes to that.

Looks like @Kswin01 is picking this up.

[Kswin01]

Edit: That said, fixing this may introduce too much proof work at this point to make it practical though. The diff is bigger than I expected.

The diff at least for aarch64 is reduced now with all the page table refactors that have occurred since this PR. The rebase can be found here: https://github.com/au-ts/seL4/tree/prevent_overmap. I've only tested aarch64 and aarch32, ill make a PR and RFC once i've tested the rest (it's pretty much untouched from this PR). Also a rebase of Alwin's sel4test branch: https://github.com/au-ts/sel4test/tree/prevent_overmap