[seL4] Capability unwrapping

Norman Feske norman.feske at genode-labs.com
Wed Feb 11 21:48:37 EST 2015


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

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

More information about the Devel mailing list