Re: [seL4] Understanding Camkes Dataport Interface Access Rights
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 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 mailto:amitgo...@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 unma
Re: [seL4] Understanding Camkes Dataport Interface Access Rights
> On Jul 14, 2019, at 20:01, Amit Goyal 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 ___ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
Re: [seL4] Understanding Camkes Dataport Interface Access Rights
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. -- Thanks and Regards, Amit Goyal On 2019-07-03 07:24, Mcleod, Kent (Data61, Kensington NSW) wrote: Camkes dataports on seL4 (seL4SharedData connector) are implemented as a shared memory mapping between the two components both pages are mapped to the same underlying frame of physical memory. The access rights are implemented via mapping attributes supported by the architecture. Your reads and writes through your dataport pointers are acting on this shared memory directly. The fault is generated by a hardware exception that seL4 handles by creating a fault and sending it to a registered fault handler (sendFaultIPC is the function in the kernel). There is a setting (that is enabled by default) that causes each Camkes component to set up a fault handler for all of its threads. If any of these threads cause a fault, such as by writing to read only memory, the fault handler will receive a message from the kernel. These mapping attributes are set when the kernel creates the page mapping for each component using the relevant Map invocation [1]. The result of building a Camkes system for seL4 is a system spec that contains all of the seL4 kernel objects and capabilities described by the system. Within this spec, dataports are described as a capability to physical memory where each capability has the specified access rights. When the system initialiser (capdl-loader-app in our case) is started by seL4 as the root task, it constructs the system following the spec and starts each Camkes component. By this point, the seL4 invocations for setting up the shared data page mappings have been performed. You can look through the generated spec in the build directory by finding the file with the .cdl extension. If you search for the name of the dataport you can find the capabilities and objects to validate that the rights are as you would expect. Hope this answers your questions. @Matthew: Write only mappings are still coerced by the capdl-loader to read write mappings before calling the mapping invocation. [1] https://docs.sel4.systems/ApiDoc.html#map-4<> ___ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
Re: [seL4] Understanding Camkes Dataport Interface Access Rights
Camkes dataports on seL4 (seL4SharedData connector) are implemented as a shared memory mapping between the two components both pages are mapped to the same underlying frame of physical memory. The access rights are implemented via mapping attributes supported by the architecture. Your reads and writes through your dataport pointers are acting on this shared memory directly. The fault is generated by a hardware exception that seL4 handles by creating a fault and sending it to a registered fault handler (sendFaultIPC is the function in the kernel). There is a setting (that is enabled by default) that causes each Camkes component to set up a fault handler for all of its threads. If any of these threads cause a fault, such as by writing to read only memory, the fault handler will receive a message from the kernel. These mapping attributes are set when the kernel creates the page mapping for each component using the relevant Map invocation [1]. The result of building a Camkes system for seL4 is a system spec that contains all of the seL4 kernel objects and capabilities described by the system. Within this spec, dataports are described as a capability to physical memory where each capability has the specified access rights. When the system initialiser (capdl-loader-app in our case) is started by seL4 as the root task, it constructs the system following the spec and starts each Camkes component. By this point, the seL4 invocations for setting up the shared data page mappings have been performed. You can look through the generated spec in the build directory by finding the file with the .cdl extension. If you search for the name of the dataport you can find the capabilities and objects to validate that the rights are as you would expect. Hope this answers your questions. @Matthew: Write only mappings are still coerced by the capdl-loader to read write mappings before calling the mapping invocation. [1] https://docs.sel4.systems/ApiDoc.html#map-4 ___ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
Re: [seL4] Understanding Camkes Dataport Interface Access Rights
Thanks Damon and Matthew for the quick response. Further, I have following doubts if someone could clarify: a) As far as I read the camkes code, I understand there is a collapse function which merges the shared page in the two components and gives required capabilities to both the components on that page. If, it is same page, we can make it read only or write only at the hardware level as suggested. How would the other thread, write or read from that page for the communication to happen. b) However, if we consider we have one page each for the dataport in both components. Then, when one component writes on a dataport then that should also be written on the dataport of the other component. Can you point me towards that piece of code. c) I would like to see the piece of code which converts my read/writes of str/n/d in the client.c.template source file to the page level read and write in camkes/seL4. As far as I understand, these are just pointers. Some code must be there to convert them to page level pointers. d) I am curious to see the seL4/Camkes code which creates the page level mapping (as suggested by Matthew). e) In the entire conversation, I believe that the kernel stands for seL4 kernel and not the host system (Ubuntu in my case) kernel. Please correct me, if am wrong. -- Thanks and Regards, Amit Goyal On 2019-07-01 09:53, Matthew Fernandez wrote: I haven’t worked with CAmkES for some time, so it’s possible I’m going to inject nothing but nonsense into this conversation, but Amit’s question stirred a memory of mine. I read Amit’s question as, “why does reading from a dataport with W permission trigger a fault?” Whether you expect a read to write-only memory to trigger a fault or not depends on how you think of hardware. At one point, CAmkES was passing the user’s requested permissions directly to the kernel.¹ This meant if you asked for a write-only dataport, CAmkES asked the kernel for write-only memory. The platforms we ran on at the time (ARMv6 and 32-bit x86?) had no concept of write-only mappings, and the kernel’s logic silently downgraded this to a kernel-only mapping. When we realised this, we worked around it by coercing a write-only mapping into read/write during code generation. This seemed more consistent with the user’s expectation. I notice requesting a write-only mapping from seL4 now triggers a debug message (c.f. maskVMRights) so maybe it was in response to this. As to why reading a write-only dataport now triggers a fault, I do not know. Maybe write-only dataports now really are write-only in some clever way? If I’ve misconstrued the question, please consider this a scenic detour and we will return to our regularly scheduled program. ¹ It’s possible this was actually in the CapDL loader not CAmkES dataports and I’m misremembering the scenario. On Jun 30, 2019, at 17:47, Lee, Damon (Data61, Kensington NSW) wrote: Hi Amit, I'd like to apologise first for errors in the tutorials. The first hint for Task 8 of this tutorial should say: "use attributes ._access" instead. As for the fault handler, I assume that you didn't get a fault where we intended it to (writing to 'd_typed'). The checks aren't really done by CAmkES or seL4 but rather, by the hardware. Depending on the permissions given to the shared memory dataports, pages are mapped in with different permissions. So writing to a read-only page will trigger a page fault and the kernel will defer it to the fault handlers of your components. And as you've found out, the default handlers are found in 'component.template.c' of the CAmkES repository. I hope this answers your question. PS: Reference solutions for the tutorials can be accessed by running the init script with the --solution flag. E.g. `./init --tutorial hello-camkes-2 --solution` would get you the solutions for the 'hello-camkes-2' tutorial. Sincerely, Damon From: Devel on behalf of Amit Goyal Sent: Monday, 1 July 2019 9:16 AM To: devel@sel4.systems Subject: [seL4] Understanding Camkes Dataport Interface Access Rights Hi All, I was looking at hello-camkes-2 tutorial. I understand the concept of dataports and the access rights given on dataport interfaces. I changed the configuration in hello-camkes-2.camkes.template file by adding echo.d = "R"; client.d = "W";. I did some changes in the client.c.template file to read on the dataport interface d by trying to access its contents through str/n/d pointers. Although, it only has write access on "d" in the new configuration. This leads to the fault handler being called when I simulate the build. I was just curious to find out where are such checks being done at the backend in camkes/seL4. I could find the code of fault handler in component.template.c but I could not find anywhere the code which checks that the client only has write access on dataport d and thus calling the fault handler. Can someone point me to
Re: [seL4] Understanding Camkes Dataport Interface Access Rights
I haven’t worked with CAmkES for some time, so it’s possible I’m going to inject nothing but nonsense into this conversation, but Amit’s question stirred a memory of mine. I read Amit’s question as, “why does reading from a dataport with W permission trigger a fault?” Whether you expect a read to write-only memory to trigger a fault or not depends on how you think of hardware. At one point, CAmkES was passing the user’s requested permissions directly to the kernel.¹ This meant if you asked for a write-only dataport, CAmkES asked the kernel for write-only memory. The platforms we ran on at the time (ARMv6 and 32-bit x86?) had no concept of write-only mappings, and the kernel’s logic silently downgraded this to a kernel-only mapping. When we realised this, we worked around it by coercing a write-only mapping into read/write during code generation. This seemed more consistent with the user’s expectation. I notice requesting a write-only mapping from seL4 now triggers a debug message (c.f. maskVMRights) so maybe it was in response to this. As to why reading a write-only dataport now triggers a fault, I do not know. Maybe write-only dataports now really are write-only in some clever way? If I’ve misconstrued the question, please consider this a scenic detour and we will return to our regularly scheduled program. ¹ It’s possible this was actually in the CapDL loader not CAmkES dataports and I’m misremembering the scenario. > On Jun 30, 2019, at 17:47, Lee, Damon (Data61, Kensington NSW) > wrote: > > Hi Amit, > > I'd like to apologise first for errors in the tutorials. The first hint for > Task 8 of this tutorial should say: "use attributes . name>_access" instead. > > As for the fault handler, I assume that you didn't get a fault where we > intended it to (writing to 'd_typed'). > > The checks aren't really done by CAmkES or seL4 but rather, by the hardware. > Depending on the permissions given to the shared memory dataports, pages are > mapped in with different permissions. So writing to a read-only page will > trigger a page fault and the kernel will defer it to the fault handlers of > your components. > > And as you've found out, the default handlers are found in > 'component.template.c' of the CAmkES repository. > > I hope this answers your question. > > PS: Reference solutions for the tutorials can be accessed by running the init > script with the --solution flag. E.g. `./init --tutorial hello-camkes-2 > --solution` would get you the solutions for the 'hello-camkes-2' tutorial. > > Sincerely, > Damon > From: Devel on behalf of Amit Goyal > > Sent: Monday, 1 July 2019 9:16 AM > To: devel@sel4.systems > Subject: [seL4] Understanding Camkes Dataport Interface Access Rights > > Hi All, > > I was looking at hello-camkes-2 tutorial. I understand the concept of > dataports and the access rights given on dataport interfaces. I changed > the configuration in hello-camkes-2.camkes.template file by adding > echo.d = "R"; client.d = "W";. I did some changes in the > client.c.template file to read on the dataport interface d by trying to > access its contents through str/n/d pointers. Although, it only has > write access on "d" in the new configuration. This leads to the fault > handler being called when I simulate the build. I was just curious to > find out where are such checks being done at the backend in camkes/seL4. > I could find the code of fault handler in component.template.c but I > could not find anywhere the code which checks that the client only has > write access on dataport d and thus calling the fault handler. Can > someone point me towards that piece of code or explain what is exactly > happening at the backend in camkes/seL4? > > -- > Thanks and Regards, > Amit Goyal > > ___ > Devel mailing list > Devel@sel4.systems > https://sel4.systems/lists/listinfo/devel > <https://sel4.systems/lists/listinfo/devel> > ___ > Devel mailing list > Devel@sel4.systems <mailto:Devel@sel4.systems> > https://sel4.systems/lists/listinfo/devel > <https://sel4.systems/lists/listinfo/devel> ___ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
Re: [seL4] Understanding Camkes Dataport Interface Access Rights
Hi Amit, I'd like to apologise first for errors in the tutorials. The first hint for Task 8 of this tutorial should say: "use attributes ._access" instead. As for the fault handler, I assume that you didn't get a fault where we intended it to (writing to 'd_typed'). The checks aren't really done by CAmkES or seL4 but rather, by the hardware. Depending on the permissions given to the shared memory dataports, pages are mapped in with different permissions. So writing to a read-only page will trigger a page fault and the kernel will defer it to the fault handlers of your components. And as you've found out, the default handlers are found in 'component.template.c' of the CAmkES repository. I hope this answers your question. PS: Reference solutions for the tutorials can be accessed by running the init script with the --solution flag. E.g. `./init --tutorial hello-camkes-2 --solution` would get you the solutions for the 'hello-camkes-2' tutorial. Sincerely, Damon From: Devel on behalf of Amit Goyal Sent: Monday, 1 July 2019 9:16 AM To: devel@sel4.systems Subject: [seL4] Understanding Camkes Dataport Interface Access Rights Hi All, I was looking at hello-camkes-2 tutorial. I understand the concept of dataports and the access rights given on dataport interfaces. I changed the configuration in hello-camkes-2.camkes.template file by adding echo.d = "R"; client.d = "W";. I did some changes in the client.c.template file to read on the dataport interface d by trying to access its contents through str/n/d pointers. Although, it only has write access on "d" in the new configuration. This leads to the fault handler being called when I simulate the build. I was just curious to find out where are such checks being done at the backend in camkes/seL4. I could find the code of fault handler in component.template.c but I could not find anywhere the code which checks that the client only has write access on dataport d and thus calling the fault handler. Can someone point me towards that piece of code or explain what is exactly happening at the backend in camkes/seL4? -- Thanks and Regards, Amit Goyal ___ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel ___ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
[seL4] Understanding Camkes Dataport Interface Access Rights
Hi All, I was looking at hello-camkes-2 tutorial. I understand the concept of dataports and the access rights given on dataport interfaces. I changed the configuration in hello-camkes-2.camkes.template file by adding echo.d = "R"; client.d = "W";. I did some changes in the client.c.template file to read on the dataport interface d by trying to access its contents through str/n/d pointers. Although, it only has write access on "d" in the new configuration. This leads to the fault handler being called when I simulate the build. I was just curious to find out where are such checks being done at the backend in camkes/seL4. I could find the code of fault handler in component.template.c but I could not find anywhere the code which checks that the client only has write access on dataport d and thus calling the fault handler. Can someone point me towards that piece of code or explain what is exactly happening at the backend in camkes/seL4? -- Thanks and Regards, Amit Goyal ___ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
