[seL4] Capability unwrapping

Gerwin Klein Gerwin.Klein at nicta.com.au
Thu Feb 12 13:42:21 EST 2015

Hi Norman,

we’ll have an internal discussion whether we can allow more cap transfers in one IPC. I don’t remember any fundamental limitation there, but we’ll need to dig into it a bit.

As Tom pointed out, there will have to be some limit on the number of caps transferred, just to get a bounded and not too large WCET, but that limit can probably be quite a bit larger than 1.

How many would your application need at most, and more generally speaking, what would you think is a good limit?


> On 11 Feb 2015, at 21:48, Norman Feske <norman.feske at genode-labs.com> wrote:
> Hello,
> after a rather long break, I picked up my work with porting Genode to
> seL4. More specifically, I try to find a good way to realize Genode's
> RPC mechanism with seL4 IPC. But admittedly, I am struggling a bit.
> Ideally, each Genode RPC should be realized as a seL4 IPC call.
> Unfortunately, however, I find the kernel interface too restrictive to
> do that. There are two issues.
> 1. Delegation of multiple capabilities at once
> According to Chapter 4.2.2 of the manual, the kernel allows the
> delegation of merely a single capability for each IPC whereas the Genode
> API does not have such a restriction. It effectively renders my idea for
> working around the capability re-identification problem [1] by
> representing each Genode capability by a tuple (or triple) of seL4
> endpoint capabilities moot.
> [1] http://sel4.systems/pipermail/devel/2014-November/000112.html
> Is there a fundamental reason for this restriction? If not, would you be
> open to make the kernel more flexible with regard to the maximum number
> of delegations per IPC?
> 2. Aliasing of unwrapped capabilities with delegated capabilities
> I understand that the kernel will automatically "unwrap" capabilities if
> the receiver imprinted a badge into the received capability. In my
> experiments, the mechanism works as expected. However, how can the
> receiver determine, which capability got unwrapped if multiple
> capabilities were transferred?
> For example, if the sender specifies three capabilities, two of them
> "unwrappable" and one delegated, the receiver will see 3 capabilities.
> The delegated cap is written to the specified 'ReceivePath' whereas the
> badges of the two unwrapped caps can be read from the message buffer.
> But I see no way for the receiver to decide, which of the three
> capability arguments got unwrapped and which got delegated. How could
> the receiver determine this information?
> Best regards
> Norman
> --
> Dr.-Ing. Norman Feske
> Genode Labs
> http://www.genode-labs.com · http://genode.org
> Genode Labs GmbH · Amtsgericht Dresden · HRB 28424 · Sitz Dresden
> Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth
> _______________________________________________
> Devel mailing list
> Devel at sel4.systems
> https://sel4.systems/lists/listinfo/devel


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 mailing list