[seL4] Capability unwrapping

Thomas Sewell thomas.sewell at nicta.com.au
Thu Feb 12 11:54:59 EST 2015

Hello Norman.

I'm not really qualified to talk about why the kernel only allows
copying of a single cap. The kernel designers certainly wanted to put a
hard limit on the amount of work that can happen in a single IPC, but I
don't know why they allowed three cap lookups on the sender side but
only one cap save on the receiver.

I can talk about the cap-unwrapping mechanism. Let me clarify how it
works somewhat.

The kernel will unwrap capabilities if they are to the same endpoint as
the receiver is receiving on. It does not matter whether or not the
capabilities have badges. The idea is that there's little point copying
to a server a collection of capabilities with which to talk to itself.

The receiver can identify which of the sender's capabilities were
unwrapped by inspecting the "msgCapsUnwrapped" field. That's its kernel
name - libsel4 calls it the capsUnwrapped field of seL4_MessageInfo.
It's a bitfield of length 3, with one bit per possible cap transfer
attempt. It tells you which caps were unwrapped.

For example, if the sender tried to send caps A, B, C to server X, and
caps A and C are in fact caps to the server's endpoint anyway, then the
server will receive a message with extraCaps=11 (three caps used in the
message) and capsUnwrapped=101 (first and third cap were unwrapped) and
it will find a delegate of cap B wherever it specified its receive pointer.

If it A, B, C are sent and only A is a cap to the server's endpoint, the
server will receive a delegate of B, C will be dropped, and
capsUnwrapped=001 will indicate that A was unwrapped (note the first cap
is in bottom position). I think that the server will receive
extraCaps=10 - that is, it will not be told that the sender was
attempting to send three caps. I suppose this should be part of the
client protocol, and the kernel mechanisms should focus on telling the
server what has actually been modified.

I hope that's helpful,

On 11/02/15 21:48, Norman Feske 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


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