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 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/s...

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 listDevel@sel4.systemshttps://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 Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

-- T o m M i t c h e l l

To add a bit to what Gernot said, it is technically possible to configure two threads to have the same IPC buffer. However, the resulting system is not useful. The threads trample each other's system calls and IPC attempts. In the worst cases, thread interleavings result in the equivalent of torn writes to your IPC buffer and your kernel invocations start looking like random noise. We observed this early on in the development of CAmkES when we accidentally configured systems this way. I would not recommend the experience. On 20/03/16 13:36, Gernot Heiser wrote:

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 mailto:mitch@niftyegg.com> 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 mailto:adrian.danis@nicta.com.au> 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/s...

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 Devel@sel4.systems mailto:Devel@sel4.systems 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 Devel@sel4.systems mailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

-- T o m M i t c h e l l _______________________________________________ Devel mailing list Devel@sel4.systems mailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel