[seL4] Capability unwrapping
gernot at nicta.com.au
Fri Feb 13 13:18:29 EST 2015
On 13 Feb 2015, at 10:30 , Thomas Sewell <Thomas.Sewell at nicta.com.au> wrote:
> In principle the reasonable limit is 1. If a sender can transfer 1 cap
> per message, it can transfer any number of caps by sending a lot of
that is true. But I’m not sure that sending 3 caps in 3 messages (plus appropriate protocols) is in all circumstances semantically equivalent to sending 3 caps in one message.
An example of 1+1<2 is round-trip IPC. One might argue that providing two IPC operations (send+receive) in a single system call is unnecessary, as you could simply make two system calls. Turns out, the functionality of the combined IPC cannot be implemented with two individual IPCs, for two reasons:
1) a call-type IPC creates the one-shot reply cap which allows to provide the server with a reply channel without trusting it. This could probably be sort-of modelled without the combined IPC, but would require many system calls (creating an endpoint, send with EP transfer, wait, destroy EP) and at best would be really expensive
2) the combined IPC is atomic, guaranteeing that the sender is ready to receive as soon as the send part is done. With two calls, the sender could be preempted between send and receive phase. With the forthcoming new real-time scheduling model, this is even more important, as it allows the server to run exclusively on client-provided time, which it couldn’t do if it had to do an explicit wait after the reply (it has no budget to run on after the reply completes).
I’m not convinced that you don’t run into similar problems with cap transfer if there’s only one cap allowed per message. I’m hoping that Norman will have some insight here.
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
More information about the Devel