Hello Gerwin, thank you very much for the clarification. So opposed to Mark's assumption, the delegation of a capability through a chain of components is no problem. Opposed to my prior understanding, each transitive delegation does indeed modify the CDT because a sibling needs to be inserted. Note to myself: I should (learn how to) read the formal specification sometime. :-) While the fog in my head about the seL4 design is lifting, I have spent a few more thoughts about my original feature request of being able to re-identify capabilities. Now I can more clearly see that it would be difficult to support by the kernel. Given an endpoint capability (specified as IPC argument), the lookup of the corresponding address in the receiver's CSpace would involve at least two problems. First, the kernel would need to revisit each sibling of the given CDT entry to check if it belongs to the CSpace of the the receiver. If this is the case, it would need to find the sibling's address in the receiver's CSpace via a reverse lookup in the guarded page table hierarchy of the receiver's CSpace. Regardless of how feasible both operations are to implement, the result may still be ambiguous because multiple caps to the same EP could be present in one CSpace. I understand that it's not very tempting to accommodate my scenario. To sum up the discussion from my perspective, I'll first try to represent each Genode capability by a triple of seL4 endpoint capabilities (as I briefly outlined in my response to Kevin's email) and see where this approach takes me. Best regards Norman On 11/11/2014 11:00 PM, Gerwin Klein wrote:
A second detail has to do with the way that capabilities are transferred via IPC. As I understand Norman's example, he is imagining a situation in which capabilities might be passed freely from F, to M, to C, and then perhaps back to M or on to other recipients. But as I understand it, capability transfer via IPC involves making a "derived" version of the capability in the sender's cspace. [I'm looking, in particular at the language in the 3rd bullet of Section 4.2.3 in the 1.3 API manual.] But:
- Some capabilities cannot be derived at all (Table 3.2), which would prevent F from sending them to M via IPC.
- Other capabilities only allow a single level of deriving, which might be enough for transmission from F to M, but could prevent further IPC transfers.
As far as I understand, the delegation of a capability (i.e., as IPC argument) does not imply a "derivation" in the sense of Figure 3.1. So the capability-derivation tree is not modified by delegating a capability via IPC. (this is different from the design of the L4 mapping database for memory mappings)
After the delegation of a capability via IPC, a slot in the receiver's CSpace will simply refer to the same endpoint (and carry the same badge) as the capability that was specified as argument at the sender side.
If this is the case, the delegation of capabilities (e.g., from F to M to C) can happen transitively without any problems.
I’ll attempt an authoritative answer for the IPC cap transfer question.
There are a number of cases, especially for endpoint caps. The actual transfer spec is in: https://github.com/seL4/l4v/blob/master/spec/abstract/Ipc_A.thy#L90
The cases are:
1) the cap is being sent to the endpoint it points to itself: This is a special case, in which the cap is not transferred, but the receiver gets the badge of the sending cap. The rationale is that the receiver already has a cap to this endpoint (the receive cap it is listening to), but will want to identify the sender based on the badge.
2) any other cap, including endpoint caps pointing to another endpoint than the one they are being sent through: A copy of the cap is created (“derived”, but not yet in the CDT sense). This operation will return most capabilities unchanged, may diminish access rights if the send operation is a diminishing one, or may fail. It does not fail for endpoint caps. It does fail for Untyped caps that are not empty, for Reply caps, for Zombies (in the process of being deleted), and IRQContol caps. VM caps and other arch specific caps have further rules (mostly, they can’t be mapped when being transferred). The derive_cap spec is at:
https://github.com/seL4/l4v/blob/master/spec/abstract/CSpace_A.thy#L91
After this operation, the copy is inserted into the receivers CSpace. This operation does modify the CDT and does not fail. The operation will insert the new cap as a child of the sender capability if that is possible, and as a sibling otherwise. Figure 3.2 in section 3.1.4 has the most important cases for endpoints: - sender is the original cap (badged or unbadged): received cap will be a child - sender is already a derived cap: received cap will be a sibling
This mostly has implications for revocation: the owner of the original cap can revoke all copies of the cap in the system; owners of derived capabilities can only revoke their own one copy.
I hope this makes things clearer and not worse ;-)
Cheers, Gerwin
________________________________
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.
-- 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