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