Thanks Anna and Gernot for clarifying.

I think I should be able to make it work with Call/Reply. I don't really like that the calling process isn't able to verify the identity/badge of the replying process, but I realize why this is the case now. I have more questions:

Is there a way on the receiving end to know if you have received a reply cap?
Could the calling process somehow maliciously cause the replying process to block on reply?

Thanks again,

Richard

On Tue, Sep 27, 2016 at 8:10 PM <Gernot.Heiser@data61.csiro.au> wrote:

On 28 Sep 2016, at 8:34 , Anna.Lyons@data61.csiro.au wrote:

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.

What Anna describes is the implementation viewpoint.

The conceptual view is that seL4_Call() generates a transient (virtual) endpoint to which the invoker of Call gets a (transient, virtual) receive cap, and is made to block on a receive from that virtual EP. The destination of the Call gets the send cap to the virtual EP (which is called the Reply cap). The virtual EP vanishes once the reply cap is invoked.

Interposing on an EP should not be a problem.

Gernot

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