Hi Kent,
Thank you for your detailed reply. I agree that write only accesses are stored as read write mappings and reading on a write only access dataport does not give any error. I am still not very clear about the following:
a) As suggested by you, I looked through the generated spec in .cdl file. I did not find the expected configuration of the dataport. Please find attached my .cdl file along with the template file. I cannot find dataport "delta" in that. Can you please help me to figure out the same.
b) As far as I understood the .cdl configuration is setup by the camkes/kernel and corresponding page table mapping entries are made for each component. Later, whenever a component is scheduled by the kernel, MMU hardware will check whether it has the read or write access, based on the page table entries provided by the kernel. Please correct me if I have misunderstood it.
My query is that in seL4 for communicating using endpoints a thread mints endpoint capabilities into other threads cspace and gives it the required access. I am not very clear with why the similar mechanism was not used here. I mean why a thread does not mint a frame's capability into other thread cspace with the required access. I am referring to section 7.4 of seL4 manual (http://sel4.systems/Info/Docs/seL4-manual-10.1.1.pdf).
i) I feel if that would have been used, then we could take better advantage of the seL4 capability based access control guarantees and lift it to camkes. This way frame capability bits in frame capability could have been used to store/check the access rights. This way checks might have been software based rather than hardware based. ii) In case we are minting the frame in the similar way as mentioned above, can you point me towards that piece of code. iii) I hope minting is actually being used in Event connection and RPC connection.
On Jul 14, 2019, at 20:01, Amit Goyal amitgoyal@cse.iitb.ac.in wrote:
Hi Kent,
Thank you for your detailed reply. I agree that write only accesses are stored as read write mappings and reading on a write only access dataport does not give any error. I am still not very clear about the following:
a) As suggested by you, I looked through the generated spec in .cdl file. I did not find the expected configuration of the dataport. Please find attached my .cdl file along with the template file. I cannot find dataport "delta" in that. Can you please help me to figure out the same.
b) As far as I understood the .cdl configuration is setup by the camkes/kernel and corresponding page table mapping entries are made for each component. Later, whenever a component is scheduled by the kernel, MMU hardware will check whether it has the read or write access, based on the page table entries provided by the kernel. Please correct me if I have misunderstood it.
My query is that in seL4 for communicating using endpoints a thread mints endpoint capabilities into other threads cspace and gives it the required access. I am not very clear with why the similar mechanism was not used here. I mean why a thread does not mint a frame's capability into other thread cspace with the required access. I am referring to section 7.4 of seL4 manual (http://sel4.systems/Info/Docs/seL4-manual-10.1.1.pdf).
i) I feel if that would have been used, then we could take better advantage of the seL4 capability based access control guarantees and lift it to camkes. This way frame capability bits in frame capability could have been used to store/check the access rights. This way checks might have been software based rather than hardware based.
I'll let Damon/Kent answer the specifics of how this currently works, but I thought it might help to give some context of why CAmkES was designed this way. A nuance of seL4 that can be surprising and counterintuitive is that you don’t need a capability to a frame to read from it or write to it. Mapping/unmapping operations require a frame cap,¹ but accessing the backing memory is just a regular read/write through a virtual address. So if someone else sets up your virtual address space, you don’t need caps to any of the backing frames. The CapDL initialiser is the process that sets up virtual address spaces of CAmkES components and it doesn't give out caps to the dataport frames to the components because they don’t need them.
As you’ve correctly identified, an alternative would be for the CapDL initialiser to give the dataport frame caps to the components themselves and allow them to set up their own mappings. Then it seems you can reason about access control purely from caps. However, this is not the case. Your reasoning still needs to deal with the other (non-shared) pages in a component’s address space, even if it is only to prove they are not shared. But actually the situation is even more complex than this. If we were to let the components set up their own dataport mappings they would also need caps to their page directories. Now your reasoning needs to also cover everything a component can do with a page directory cap (e.g. re-map a thread’s IPC buffer virtual address to the dataport frame). Returning to the first alternative of the CapDL initialiser setting up mappings, the components themselves need neither frame caps nor page directory caps; you can see in your .cdl file that the components’ CNodes don’t hold any PD caps. This simplifies access control reasoning significantly as all cases involving PD caps and/or frame caps are vacuous.
¹ Again I’m going to have to beg Kent to correct my mistakes. At one point it was possible to unmap a page without a cap to the backing frame. You could achieve this by mapping another frame to the same virtual address. I don’t know whether I am misremembering this and/or whether this behaviour still exists.
ii) In case we are minting the frame in the similar way as mentioned above, can you point me towards that piece of code. iii) I hope minting is actually being used in Event connection and RPC connection.
-- Thanks and Regards, Amit Goyal
Thanks Matthew for answering some of Amit's questions. My query is that in seL4 for communicating using endpoints a thread mints endpoint capabilities into other threads cspace and gives it the required access. I am not very clear with why the similar mechanism was not used here. I mean why a thread does not mint a frame's capability into other thread cspace with the required access. I am referring to section 7.4 of seL4 manual (http://sel4.systems/Info/Docs/seL4-manual-10.1.1.pdf). This is correct and the exact mechanism is used here. The only difference is that this is done via the capDL initialiser (see `init_cnode()` in capdl-loader-app/src/main.c and refer to the capdl_spec.c as well as the .cdl files generated in the build directory). The capDL initialiser will make two extra copies of an endpoint capability and give the copies to the threads that will be communicating with each other.
Sincerely, Damon ________________________________ From: Matthew Fernandez matthew.fernandez@gmail.com Sent: Tuesday, 16 July 2019 10:32 AM To: Amit Goyal Cc: Mcleod, Kent (Data61, Kensington NSW); devel@sel4.systems; Lee, Damon (Data61, Kensington NSW) Subject: Re: [seL4] Understanding Camkes Dataport Interface Access Rights
On Jul 14, 2019, at 20:01, Amit Goyal <amitgoyal@cse.iitb.ac.inmailto:amitgoyal@cse.iitb.ac.in> wrote:
Hi Kent,
Thank you for your detailed reply. I agree that write only accesses are stored as read write mappings and reading on a write only access dataport does not give any error. I am still not very clear about the following:
a) As suggested by you, I looked through the generated spec in .cdl file. I did not find the expected configuration of the dataport. Please find attached my .cdl file along with the template file. I cannot find dataport "delta" in that. Can you please help me to figure out the same.
b) As far as I understood the .cdl configuration is setup by the camkes/kernel and corresponding page table mapping entries are made for each component. Later, whenever a component is scheduled by the kernel, MMU hardware will check whether it has the read or write access, based on the page table entries provided by the kernel. Please correct me if I have misunderstood it.
My query is that in seL4 for communicating using endpoints a thread mints endpoint capabilities into other threads cspace and gives it the required access. I am not very clear with why the similar mechanism was not used here. I mean why a thread does not mint a frame's capability into other thread cspace with the required access. I am referring to section 7.4 of seL4 manual (http://sel4.systems/Info/Docs/seL4-manual-10.1.1.pdf).
i) I feel if that would have been used, then we could take better advantage of the seL4 capability based access control guarantees and lift it to camkes. This way frame capability bits in frame capability could have been used to store/check the access rights. This way checks might have been software based rather than hardware based.
I'll let Damon/Kent answer the specifics of how this currently works, but I thought it might help to give some context of why CAmkES was designed this way. A nuance of seL4 that can be surprising and counterintuitive is that you don’t need a capability to a frame to read from it or write to it. Mapping/unmapping operations require a frame cap,¹ but accessing the backing memory is just a regular read/write through a virtual address. So if someone else sets up your virtual address space, you don’t need caps to any of the backing frames. The CapDL initialiser is the process that sets up virtual address spaces of CAmkES components and it doesn't give out caps to the dataport frames to the components because they don’t need them.
As you’ve correctly identified, an alternative would be for the CapDL initialiser to give the dataport frame caps to the components themselves and allow them to set up their own mappings. Then it seems you can reason about access control purely from caps. However, this is not the case. Your reasoning still needs to deal with the other (non-shared) pages in a component’s address space, even if it is only to prove they are not shared. But actually the situation is even more complex than this. If we were to let the components set up their own dataport mappings they would also need caps to their page directories. Now your reasoning needs to also cover everything a component can do with a page directory cap (e.g. re-map a thread’s IPC buffer virtual address to the dataport frame). Returning to the first alternative of the CapDL initialiser setting up mappings, the components themselves need neither frame caps nor page directory caps; you can see in your .cdl file that the components’ CNodes don’t hold any PD caps. This simplifies access control reasoning significantly as all cases involving PD caps and/or frame caps are vacuous.
¹ Again I’m going to have to beg Kent to correct my mistakes. At one point it was possible to unmap a page without a cap to the backing frame. You could achieve this by mapping another frame to the same virtual address. I don’t know whether I am misremembering this and/or whether this behaviour still exists.
ii) In case we are minting the frame in the similar way as mentioned above, can you point me towards that piece of code. iii) I hope minting is actually being used in Event connection and RPC connection.
-- Thanks and Regards, Amit Goyal
-
Amit Goyal -
Lee, Damon (Data61, Kensington NSW) -
Matthew Fernandez