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