>> 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. _______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
