Re: [seL4] Why send-only IPC doesn't and shouldn't return a success indicator

Hi Richard, This is a common misunderstanding: seL4_Call doesn’t generate a cap to the ep, but a cap to the thread that the seL4_Call went through (called the ‘reply cap’). seL4_Reply(Wait) sends directly to this thread via that capability, so the IPC is guaranteed to go to the caller. If you are dealing with multiple threads with interleaved messages, you can use seL4_CNode_SaveCaller to save the current reply cap, and invoking seL4_Send on the saved slot will do the reply. Cheers, Anna. From: Devel [mailto:devel-bounces@sel4.systems] On Behalf Of Richard Habeeb Sent: Wednesday, 28 September 2016 8:06 AM To: Heiser, Gernot (Data61, Kensington NSW) ; devel@sel4.systems Subject: Re: [seL4] Why send-only IPC doesn't and shouldn't return a success indicator So perhaps I am misunderstanding the design differences between the different IPC system calls. Let me back up and explain what I was working on. I was basically designing a kerberos-style IPC policy system. The IPC policy server is basically a trusted middle man which sets up communication between other processes. I originally thought that an EP would need to be allocated per pairwise communication, client to server. In this line of thinking, each child process had RW rights and a badged cap to communicate with the server. I am pretty new to this, and I didn't realize that seL4_Call wasn't just a function that combined seL4_Send and seL4_Recv. I see now that it grants the receiving process it's own cap to the EP, and then immediately Recvs from that EP. In this case, it seems like there only needs to one EP for the server. Clients have write and grant access, and the server gets read. Does the kernel ensure that the calling process gets the Reply? Or is a MITM possible in this scenario? Additionally, if a client does a normal send, instead of a call, the kernel just throws an exception when the server tries to reply. This sounds like it shouldn't be acceptable behavior. Finally, I am confused how a client with WG cap access is able to receive a reply, simply by using the call function. It should have no read access to the EP right? TL;DR I am testing other designs that don't use NBSend. I didn't realize that seL4_Call wasn't just a function that combined seL4_Send and seL4_Recv. Does the kernel ensure that the calling process gets the Reply? Thanks Richard Habeeb On Sat, Sep 24, 2016 at 2:48 AM mailto:Gernot.Heiser@data61.csiro.au> wrote: We have just received this comment on github, which I think merits some explanation:

There are times when IPC needs to happen, but a sending process cannot wait around for another process to be receiving. seL4_NBSend is basically the system call for this, but it never provides any feedback whether or not IPC took place.

Summary: I accept that this is a valid use case, but the suggested solution is not the right one. There are two reasons why I’m saying this: 1) the current behaviour of send-only IPC is correct and cannot be changed, 2) send-only IPC is the wrong way to address this use case. Re (1): Anyone who tried to use seL4_Send() or seL4_NBSend() will likely have noticed that they are of very little use, because you don’t know whether the message was transferred. So, why can't we return at least a boolean value, indicating whether a message has been delivered or it was dropped on the floor? It’s simple: this would violate the dataflow guarantees provided by seL4. Send-only IPC is there to enable one-way information flow, and consequently can be invoked using a send-only cap. But a send-only cap must not allow any information flow from the receiver to the sender (or else all our isolation proofs would break down). Basically, a return status that can be influenced by the receiver constitutes a back channel that is not authorised by a cap, and as such is verboten. This means that send-only IPC is of very little practical use, except where you really want one-way information transfer, or you have a higher-level protocol that lets you get away with not knowing whether the message was lost. (Eg if the receiver being not ready is a protocol violation by the receiver, and it has only itself to blame for losing the message.) So, could we make send-only IPC a bit more useful by changing the semantics slightly? For example, we could have a return value that indicates successful message delivery if the send was invoked with a send+receive cap, but will always return false if the invocation used a send-only cap? In principle that would be doable without violating security requirements. The cost would be extra checking. It would also be somewhat unsystematic if the semantics of a send-only operation would depend on whether your cap has receive rights as well. It’d be arguably misleading, as you’re doing more than sending. This gets me to (2): send-only IPC is the wrong way to solve the problem. The above use case is clearly one where info flow is inherently two-way: you send something and need an acknowledgment of receipt. This means call-type IPC is the right mechanism, it does exactly that. And on top of that it is more efficient than separate send-receiver, and avoids (thanks to reply caps) the need to set up a separate reply channel. The problem, of course, is that seL4_Call() is always blocking, there is no polling variant of this syscall. Should there be an seL4_NBCall()? Arguably yes, just as the RT branch already provides a seL4 SignalRecv() syscall, which is the non-blocking equivalent of seL4_ReplyRecv(). Will it happen? Possibly, but not in mainline the near future. The reason is that to add this (fairly simple) feature to the mainline kernel will require verifying it, and our verification engineers are presently very busy delivering on contracted milestones. We’ll discuss this internally. In the meantime I’ve added some explanation of the semantics of seL4_Send()/seL4NBSend() to the FAQ on the seL4 wiki. Gernot _______________________________________________ Devel mailing list Devel@sel4.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel -- Richard Habeeb Research Assistant, Computer Science, USF http://habeebr.bitbucket.org/