Hi, I have a couple of questions about the virtual memory subsystem in seL4.
1. Intel's Memory Protection keys let a process restrict the access to given virtual address ranges based on a key. This key is the bit 62:59 of the virtual address. It is stored in the PTE of the level 4/5 Page Table. I want to use this feature in my project.
Does seL4 support the setting of Memory Protection keys for virtual addresses? I couldn't find any mention of it in the source. I understand that if I use the current API of "seL4_X86_PageTable_Map" with those higher bits of the vaddr set, the kernel will ignore them. Is my understanding correct?
Furthermore, was a decision made not to support MPK at some point?
2. As per section 7.3 of the seL4 manual, seL4 doesn't allow sharing of page tables. I am trying to understand the reasoning behind this. Was this done to aid verification?
Thanks, Sidhartha S Agrawal
Hi Sid,
On 2 Mar 2022, at 02:47, Sid Agrawal siagraw@cs.ubc.ca wrote:
- Intel's Memory Protection keys let a process restrict the access to
given virtual address ranges based on a key. This key is the bit 62:59 of the virtual address. It is stored in the PTE of the level 4/5 Page Table. I want to use this feature in my project.
Does seL4 support the setting of Memory Protection keys for virtual addresses? I couldn't find any mention of it in the source. I understand that if I use the current API of "seL4_X86_PageTable_Map" with those higher bits of the vaddr set, the kernel will ignore them. Is my understanding correct?
Yes, that is correct.
Furthermore, was a decision made not to support MPK at some point?
There has been no explicit decision about this. In terms of the API I think it might be reasonably easy to support this, but I haven't thought through the access control implications of it, i.e. if we could allow setting these bits as purely user-supplied attributes (assuming you present a cap to the table), or if they would need to be controlled by cap rights.
- As per section 7.3 of the seL4 manual, seL4 doesn't allow sharing of
page tables. I am trying to understand the reasoning behind this. Was this done to aid verification?
It's more a restriction of the current design of the relationship between virtual memory caps and virtual memory objects. Allowing sharing of lower-level tables would break that design (in that sense verification would of course forbid that). seL4 does allow sharing of address spaces and frames, though.
Cheers, Gerwin
Hi Gerwin, Thank you for getting back to me.
There has been no explicit decision about this. In terms of the API I think it might be reasonably easy to support this, but I haven't thought through the access control implications of it, i.e. if we could allow setting these bits as purely user-supplied attributes (assuming you present a cap to the table), or if they would need to be controlled by cap rights.
MPK
I will need to add this support in the kernel for my project at some point in the next few months. For when I try that: - I can create a fork or seL4 and start changing the kernel. I have no background in formal verification, so I cannot imagine that upstream will accept my changes. - Is there a guide on adding new systems calls to the kernel that I could follow along?
It's more a restriction of the current design of the relationship between virtual memory caps and virtual memory objects. Allowing sharing of lower-level tables would break that design (in that sense verification would of course forbid that). seL4 does allow sharing of address spaces and frames, though.
PT Sharing
Thanks for the explanation. Do you see this restriction changing at any point? Sharing of PT would lead to smaller memory footprints when making a complete copy of the address space. Then again, the memory taken up by PT is typically of the order of 1% of the memory consumption of the process. So maybe it doesn't really matter.
Sid
Cheers, Gerwin
Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
On Fri, Mar 4, 2022 at 4:16 AM Sid Agrawal siagraw@cs.ubc.ca wrote:
Hi Gerwin, Thank you for getting back to me.
There has been no explicit decision about this. In terms of the API I think it might be reasonably easy to support this, but I haven't thought through the access control implications of it, i.e. if we could allow setting these bits as purely user-supplied attributes (assuming you present a cap to the table), or if they would need to be controlled by cap rights.
MPK
I will need to add this support in the kernel for my project at some point in the next few months. For when I try that:
- I can create a fork or seL4 and start changing the kernel. I have no
background in formal verification, so I cannot imagine that upstream will accept my changes.
- Is there a guide on adding new systems calls to the kernel that I could
follow along?
A place to start would be looking at a commit where another invocation was added: https://github.com/seL4/seL4/commit/eb0553fa7563af1c5bb2dd2736c5563c49ef057e
It's more a restriction of the current design of the relationship between virtual memory caps and virtual memory objects. Allowing sharing of lower-level tables would break that design (in that sense verification would of course forbid that). seL4 does allow sharing of address spaces and frames, though.
PT Sharing
Thanks for the explanation. Do you see this restriction changing at any point? Sharing of PT would lead to smaller memory footprints when making a complete copy of the address space. Then again, the memory taken up by PT is typically of the order of 1% of the memory consumption of the process. So maybe it doesn't really matter.
It wouldn't be possible for the kernel to perform necessary TLB maintenance instructions in an efficient way. When a page would be unmapped from a shared page table, the kernel would be required to perform a TLB invalidate operation for all address spaces that the page may be mapped in. This could be a very large number of address spaces and so would require preemption points to break up a long running operation. However preemption points can lead to a different thread being scheduled and leaving the kernel. This thread now potentially has a VSpace that is affected by the in-progress operation or may want to also perform an invocation on the shared page table. The design and also the proofs would need to be updated to reflect an in-progress vspace invalidation in the kernel state. We would also need to handle whether other operations on the page table could be performed until the invalidation had completed and also how to handle revoking the page table etc. It ends up getting quite complicated unfortunately.
As Gerwin mentioned, you can already share entire VSpaces or share individual frames which so far has been sufficient to cover most sharing requirements.
Kent
Sid
Cheers, Gerwin
Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
This is very helpful. Thank you, Kent.
-Sid
On Sat, Mar 5, 2022 at 12:43 AM Kent Mcleod kent.mcleod72@gmail.com wrote:
[CAUTION: Non-UBC Email]
On Fri, Mar 4, 2022 at 4:16 AM Sid Agrawal siagraw@cs.ubc.ca wrote:
Hi Gerwin, Thank you for getting back to me.
There has been no explicit decision about this. In terms of the API I think it might be reasonably easy to support this, but I haven't
thought
through the access control implications of it, i.e. if we could allow setting these bits as purely user-supplied attributes (assuming you
present
a cap to the table), or if they would need to be controlled by cap
rights.
MPK
I will need to add this support in the kernel for my project at some
point
in the next few months. For when I try that:
- I can create a fork or seL4 and start changing the kernel. I have no
background in formal verification, so I cannot imagine that upstream will accept my changes.
- Is there a guide on adding new systems calls to the kernel that I could
follow along?
A place to start would be looking at a commit where another invocation was added: https://github.com/seL4/seL4/commit/eb0553fa7563af1c5bb2dd2736c5563c49ef057e
It's more a restriction of the current design of the relationship
between
virtual memory caps and virtual memory objects. Allowing sharing of lower-level tables would break that design (in that sense verification would of course forbid that). seL4 does allow sharing of address
spaces and
frames, though.
PT Sharing
Thanks for the explanation. Do you see this restriction changing at any point? Sharing of PT would lead to smaller memory footprints when making a complete copy of the address space. Then again, the memory taken up by PT is typically of the order of 1% of the memory consumption of the process. So maybe it doesn't really matter.
It wouldn't be possible for the kernel to perform necessary TLB maintenance instructions in an efficient way. When a page would be unmapped from a shared page table, the kernel would be required to perform a TLB invalidate operation for all address spaces that the page may be mapped in. This could be a very large number of address spaces and so would require preemption points to break up a long running operation. However preemption points can lead to a different thread being scheduled and leaving the kernel. This thread now potentially has a VSpace that is affected by the in-progress operation or may want to also perform an invocation on the shared page table. The design and also the proofs would need to be updated to reflect an in-progress vspace invalidation in the kernel state. We would also need to handle whether other operations on the page table could be performed until the invalidation had completed and also how to handle revoking the page table etc. It ends up getting quite complicated unfortunately.
As Gerwin mentioned, you can already share entire VSpaces or share individual frames which so far has been sufficient to cover most sharing requirements.
Kent
Sid
Cheers, Gerwin
Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
-
Gerwin Klein -
Kent Mcleod -
Sid Agrawal