[seL4] Capability unwrapping

Norman Feske norman.feske at genode-labs.com
Thu Feb 12 23:27:06 EST 2015

Hi Gernot,

> I’d like to understand the specific use cases better. I accept that
> one cap isn’t enough, there are likely unsolvable races, which
> require >1 caps to be transferred atomically. My intuition is that 3
> should enough to solve all fundamental problems, and anything beyond
> that boils down to efficiency arguments/trade-offs.

I agree that more than 3 caps per IPC are unlikely. Actually, in
Genode's current RPC interfaces, the maximum is 2.

The value of 6 accounts for the fact that I cannot directly represent a
Genode capability by an seL4 endpoint capability. As discussed in the
responses to [1], seL4 does not allow the receiver to re-identify a
capability that he forwarded and then received back.

However, Genode relies on a way to re-identify capabilities. The badge
is not enough because it cannot be used by intermediate components. To
solve this problem, I came up with the idea to represent each Genode
capability by 3 seL4 endpoint capabilities.

* The first is the actual capability referring to the object at the

* The second is an endpoint capability locally created within
  the component when the Genode capability entered the component.
  It is badged using a component-local endpoint. Hence, it can be
  re-identified when passed to another component and handed back.

* The third is an endpoint capability created by the direct
  originator of the capability. It corresponds to the second
  capability at the originating component.

Under the hood, when passing a Genode capability as argument to an RPC
call, all three seL4 endpoint capabilities will be transferred. When
such a Genode capability is handed back to the component, the third
received seL4 capability can be used to re-identify the context
associated with the Genode capability because its badge was imprinted
locally by the component.

Effectively, the second and third seL4 capabilities record the last two
steps of the delegation history. They are never invoked or used otherwise.

The approach does not entirely solve the general re-identification
problem but, as far as I can see, it covers the patterns found in
Genode. I admit that it seems to be a bit wasteful. But I have not come
up with a better solution. The alternative approaches (see [2]) are even
less satisfying.

[1] http://sel4.systems/pipermail/devel/2014-November/000112.html
[2] http://sel4.systems/pipermail/devel/2014-November/000114.html


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