On Wed, Sep 28, 2016 at 4:40 PM,  <[email protected]> wrote:
> On 29 Sep 2016, at 1:44 , Richard Habeeb <[email protected]> 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

FWIW, I finally found where this is documented in the manual in

http://sel4.systems/Info/Docs/seL4-manual-latest.pdf#section.2.2
under seL4_Call, I was looking for it in all of the places for
performing a reply,

> 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).

I don't see how one can, seL4_CNode_SaveCaller will set the cap to a null cap
and call userError() if debugging is enabled, but it doesn't cause any
actual error return code afaict.

perhaps if there is a public mechanism for checking whether a cap is a null cap?
I haven't been able to find a mechanism for checking cap type

> 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.

_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel

Reply via email to