seL4 IPC is a bit different to SYS-V in very fundamental ways, so comparisons may not be all that meaningful.
In particular, the seL4 IPC buffer is a set of *virtual registers*. This means it has the semantics of physical registers: they are strictly thread-local (which includes that any attempt by a thread to access another thread’s IPC buffer has undefined result) and cannot page fault. This is a fundamental design decision, not policy. Gernot On 20 Mar 2016, at 12:48 , Tom Mitchell <[email protected]<mailto:[email protected]>> wrote: There are questions of policy. Two processes or threads with the same security label could share a buffer used for IPC. A new buffer needs to be scrubbed of any data so no side channel or data leak is generated by object reuse. SystemV IPC could be sloppy with this and demand that the user create the buffer with correct permissions. The simple owner, group, world set of permission bits is not sufficient. Failure to dismiss and delete the object was another SysV demand made on the application programmer. Threads must have ways to communicate... Even sending signals that can be caught to a process or thread can qualify as a data communication path to violate policy and generate side channels. ...___... Interesting tip of the iceberg question. On Thu, Mar 17, 2016 at 12:04 AM, Adrian Danis <[email protected]<mailto:[email protected]>> wrote: Hi David, The global frame is a location of memory that is updated by the kernel whenever a thread switch happens. It acts as a form of thread local storage. See https://github.com/seL4/seL4/blob/51ef223945b06d38dbc9d3f6ffcee795966428d0/src/arch/arm/32/kernel/thread.c#L22 So yes, your IPC will work correctly and as intended. It would be strictly incorrect for different threads to try and use a single IPC buffer. Adrian On Wed 16-Mar-2016 6:47 PM, Qiwei Wen wrote: Hi, I'm trying to write a multithreaded seL4 application. It's to be made up of sel4util processes with different cspaces and sharing the same Vspace. I managed to achieve this, but what confuses me is that since the processes share the same Vspace, wouldn't GetIPCBuffer() return the same result for each of them? I looked at libsel4/arch_include/arm/sel4/arch/functions.h, and GetIPCBuffer() is simply: return *(seL4_IPCBuffer**)seL4_GlobalsFrame; Since seL4_GlobalsFrame is just a fixed memory location (0xffffc000) in the shared address space, why does seL4_GetIPCBuffer() return different results for different processes? Below is the output: ========================== PARENT: IPCBUFFER: 00273000 CHILD: GlobalsFrame: ffffc000, *GlobalsFrame 10076000 CHILD: setting shared to 97 PARENT: CHILD DIED, shared char: 97, MR16: 00000000 ============================= Is it that the frame ffffc000 mapping is changed on every context switch perhaps? Can I absolutely trust that IPC is still working correctly with this set up? Thanks, David _______________________________________________ Devel mailing list [email protected]<mailto:[email protected]> https://sel4.systems/lists/listinfo/devel ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. _______________________________________________ Devel mailing list [email protected]<mailto:[email protected]> https://sel4.systems/lists/listinfo/devel -- T o m M i t c h e l l _______________________________________________ Devel mailing list [email protected]<mailto:[email protected]> https://sel4.systems/lists/listinfo/devel
_______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
