On 29 Sep 2016, at 1:44 , Richard Habeeb <richard.habeeb@gmail.com> wrote:

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.

Actually, the system provides the guarantees you need: The reply message can only have been sent by invoking the reply cap, so it can only come from whoever received the original message, or whoever they handed the reply cap to. That’s as much guarantee as you can hope for.

In other words,

   Call (ep, msg, &reply)

is logically roughly equivalent to:

   replEp = create_ep ()
   sendCap = mint (replEp, send_only)
   Send (ep, {msg,sendCap})
   Recv (replyEp, &reply)
   destroy (replyEp)

except it’s atomic, no race conditions etc

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? 

The server probably cannot be sure that it received a reply cap (someone correct me if I’m wrong here). However, it doesn’t matter, the server doesn’t care: If no reply cap was received, the reply-cap slot remains invalid. An attempt by the server to use the reply cap will simply fail, the server can’t block that way. In the normal case of the server using seL4_ReplyRecv(), the send part of the call will silently fail (message delivered to the bitbucket) and switch to the receive phase immediately. The server won’t notice the difference.

Gernot