Hi Sid, > On 2 Mar 2022, at 02:47, Sid Agrawal <[email protected]> wrote: > > 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?
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. > 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? 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 _______________________________________________ Devel mailing list -- [email protected] To unsubscribe send an email to [email protected]
