Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Prevent overmapping on aarch32, aarch64, x86 #967

Closed
wants to merge 6 commits into from

Conversation

alwin-joshy
Copy link
Contributor

@alwin-joshy alwin-joshy commented Jan 27, 2023

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

/* Check that we are not overwriting an existing mapping */
if (pde_ptr_get_pdeType(ret.pde_entries.base) == pde_pde_section) {
paddr_t pde_paddr = pde_pde_section_ptr_get_address(ret.pde_entries.base);
if (pde_paddr && frame_asid == asidInvalid) {
Copy link
Member

Choose a reason for hiding this comment

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

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?

Copy link
Contributor Author

@alwin-joshy alwin-joshy Jan 31, 2023

Choose a reason for hiding this comment

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

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.

Copy link
Member

Choose a reason for hiding this comment

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

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.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

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?

@alwin-joshy alwin-joshy force-pushed the prevent_overmap branch 3 times, most recently from 08eb938 to 78114af Compare February 1, 2023 02:09
@lsf37 lsf37 added the verification Needs formal verification input/change, or is motivated by verification label Feb 2, 2023
@lsf37
Copy link
Member

lsf37 commented Jul 17, 2024

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
verification Needs formal verification input/change, or is motivated by verification
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants