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
_______________________________________________
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems

Reply via email to