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 ashared memory mapping between the two components both pages are mapped to the same underlying frame of physical memory. The access rights are implementedvia mapping attributes supported by the architecture. Your reads and writesthrough your dataport pointers are acting on this shared memory directly. Thefault is generated by a hardware exception that seL4 handles by creating a fault and sending it to a registered fault handler (sendFaultIPC is thefunction 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 pagemapping 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 theseL4 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, itconstructs the system following the spec and starts each Camkes component. By this point, the seL4 invocations for setting up the shared data page mappingshave 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 youwould 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
<<attachment: File.zip>>
_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
