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

--

  T o m    M i t c h e l l

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