July 2019 - Devel - lists.sel4.systems

sel4 on the Xilinx Zynq US+ ZCU104 Evaluation Kit
by derek65 22 Jul '19

22 Jul '19

Hi, I'm interested in running sel4 on a Xilinx Zynq UltraScale+ MPSoC evaluation board. I read the great blog post about the port from DornerWorks [1] and checked the sel4 hardware support page here [2]. Since the Zynq ZCU102 Evaluation Kit listed is quite expensive, I wanted to ask if anyone tried the procedure described in the blog post on the much cheaper Xilinx US+ ZCU104 Evaluation Kit. Might this work as well? Thanks! Kind regards, - derek [1] - https://dornerworks.com/blog/hardware-security-growing-concern-sel4-ecosyst… [2] - https://docs.sel4.systems/Hardware/

4 3

CamkES support for waiting on multiple signals
by yogidk . 22 Jul '19

22 Jul '19

Hello , I would like to know if the CamkES has support for wait on multiple signal events ? I need to wait for 3 different events (say write, read and timer), I need to wait until one of these events occur. As soon as I get an event, I need to call a common function. I cannot use emitter/consumer signal events concept of CamKES here as it allows only one to one connection and not many to one connection. So in other words a single consumer_wait() for 3 different emitter events is not possible in CamkES. Any suggestions how can this be achieved using CamkES? Regards yk

3 3

Re: [seL4] Understanding Camkes Dataport Interface Access Rights
by Amit Goyal 16 Jul '19

16 Jul '19

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

3 2

Understanding Camkes Dataport Interface Access Rights
by Amit Goyal 03 Jul '19

03 Jul '19

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

4 4