Hello,
I hope you don't mind me spamming the list with my problems.
I have a question about the association of capabilities with process-local meta data. As far as I understand, the "badging" of capabilities is the recommended mechanism for servers to attach a server-local meaningful value to a capability. After having handed out the capability to a client, it gets this value reported each time the client (or any other process to which the capability was delegated to) invokes the capability or delegates the capability back to the server (e.g., as RPC argument).
Now, I have the following scenario: There are three processes, a factory (F), a mediator (M), and a client (C). The factory is responsible for physically allocating objects (e.g., in Genode's case, one example would be the core process that hands out dataspaces). The mediator is a process that sits in-between the client and the factory (in the Genode world, this could the the init process). It keeps records about the allocation and may use this information to implement a policy. The client is the designated user of the object. To create an object, C will call M, which, in turn, will call F on behalf of C:
alloc create F <-------- M <--------- C
F will create the actual object and a corresponding badged capability and returns the badged capability as return value to M. Because M wants to keep records about the lifetime and parameters of the created objects, it needs to associate a process-local meta-data structure to the capability.
badged cap F ---------> M C : (meta data <-> cap)
M stores the meta data in a process-local data base using the cap as key. It then hands out the cap to the actual client. Sometime later, the client decides to destroy the object (or perform another operation at M that takes the cap as argument):
badged cap F M ---------> C | | uses object (e.g., invoking the cap) destroy | (cap arg) | ? <----------+
When M receives the destroy request with the cap of the to-be-destroyed object as argument, it wants to look up the corresponding meta data from its data base. But unfortunately, the cap argument of the destroy function got assigned a new local name within M (some number within the receive window of M).
How can M find the meta data associated with the allocated object?
Best regards Norman
Hi Norman,
The idea of passing the cap to identify metadata in a server that does not implement the object the cap refers to is problematic. I believe the operation you want at the kernel-level is "what is the index in my cspace corresponding to the cap I was sent". Given cspaces are arbitrary directed graph, this operation is asking what is the path between two points in the graph (if it exists) and not something we wish to support.
One approach is to have the mediator mediate all operations, i.e. have M as a proxy for access to F - obviously this has a performance impact.
Alternatively, C gets a tuple (Fcap, Mdesc) and you split the interface - which is what you seem to be doing anyway. Given C will have already have session cap to M (lets call it Mcap), destroy involves invoking Mcap with Mdesc. Note: I'm glossing over interface enforcement, i.e. M gets Fcap1 which can destroy, and C gets Fcap2 which cannot, allowing you to enforce the split interface. Note: You could have an (Fcap2,Mcap)-like tuple to the client to split interface as well.
In general, caps are more expensive and are only required when needing to pass an unforgeable authority between entities. Adding a descriptor to an existing session cap is generally cheaper. I know this statement is probably blasphemous, but performance implications of a design matter as long as the security model remains sound.
Last design pattern is to implement object "death notification" from F -> M, which would require a registration protocol: M->F. We use this in RefOS for processes, which I assume are much more coarse-grained than your dataspaces.
Note: We have mulled over the idea of an operation bool points_to_same_object(cap1,cap2), this would enable C passing a foreign cap (F) together with a handle to the metadata in M, and thus you could test if the passed cap corresponds with the cap associated with your metadata in M. I'd be interested if such an operation improve/eases the protocol design of interaction between your services.
- Kevin
-----Original Message----- From: Devel [mailto:devel-bounces@sel4.systems] On Behalf Of Norman Feske Sent: Friday, 7 November 2014 12:32 AM To: devel Subject: [seL4] Re-identification of capabilities
Hello,
I hope you don't mind me spamming the list with my problems.
I have a question about the association of capabilities with process-local meta data. As far as I understand, the "badging" of capabilities is the recommended mechanism for servers to attach a server-local meaningful value to a capability. After having handed out the capability to a client, it gets this value reported each time the client (or any other process to which the capability was delegated to) invokes the capability or delegates the capability back to the server (e.g., as RPC argument).
Now, I have the following scenario: There are three processes, a factory (F), a mediator (M), and a client (C). The factory is responsible for physically allocating objects (e.g., in Genode's case, one example would be the core process that hands out dataspaces). The mediator is a process that sits in-between the client and the factory (in the Genode world, this could the the init process). It keeps records about the allocation and may use this information to implement a policy. The client is the designated user of the object. To create an object, C will call M, which, in turn, will call F on behalf of C:
alloc create F <-------- M <--------- C
F will create the actual object and a corresponding badged capability and returns the badged capability as return value to M. Because M wants to keep records about the lifetime and parameters of the created objects, it needs to associate a process-local meta-data structure to the capability.
badged cap F ---------> M C : (meta data <-> cap)
M stores the meta data in a process-local data base using the cap as key. It then hands out the cap to the actual client. Sometime later, the client decides to destroy the object (or perform another operation at M that takes the cap as argument):
badged cap F M ---------> C | | uses object (e.g., invoking the cap) destroy | (cap arg) | ? <----------+
When M receives the destroy request with the cap of the to-be-destroyed object as argument, it wants to look up the corresponding meta data from its data base. But unfortunately, the cap argument of the destroy function got assigned a new local name within M (some number within the receive window of M).
How can M find the meta data associated with the allocated object?
Best regards Norman
-- 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
_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
________________________________
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.
Hi Kevin,
thank you for your insightful reply.
The idea of passing the cap to identify metadata in a server that does not implement the object the cap refers to is problematic. I believe the operation you want at the kernel-level is "what is the index in my cspace corresponding to the cap I was sent". Given cspaces are arbitrary directed graph, this operation is asking what is the path between two points in the graph (if it exists) and not something we wish to support.
From a user's point of view, this would indeed be perfect. On NOVA, this
feature (in NOVA speak called "translate") is implemented in a way that the graph is traversed towards the root of the tree only. So there is no search involved. Hence, in the common case, the costs are reasonably small. Still, the time needed for the traversal depends on user-land behavior, which probably contradicts with seL4's guarantees about interrupt latencies.
One approach is to have the mediator mediate all operations, i.e. have M as a proxy for access to F - obviously this has a performance impact.
Unfortunately, this works not for scenarios where C passes the capability as argument to another service of F. E.g., Genode's core process provides services for allocating RAM dataspaces or obtaining MMIO dataspaces. Dataspaces are often obtained not from core directly but from mediating processes, for example a platform driver that hands out MMIO resources to clients according to a policy.
Core also provides a region-manager (RM) service for paging processes. A process in its role of an RM client makes a dataspace visible in its address space by passing the dataspace capability as an argument to an 'attach' function on its RM session. If M implemented the dataspace interface, the dataspace capability handed out to C would be meaningless for core when C tries to attach the dataspace.
In short, this approach would not be general enough for us.
Alternatively, C gets a tuple (Fcap, Mdesc) and you split the interface - which is what you seem to be doing anyway. Given C will have already have session cap to M (lets call it Mcap), destroy involves invoking Mcap with Mdesc. Note: I'm glossing over interface enforcement, i.e. M gets Fcap1 which can destroy, and C gets Fcap2 which cannot, allowing you to enforce the split interface. Note: You could have an (Fcap2,Mcap)-like tuple to the client to split interface as well.
That leads indeed to a direction I have been thinking about: We could represent a Genode capability by a triple of seL4 capabilities.
(1) The "actual" seL4 cap that points to the real object. It is used for invocation. (2) A "local ID" that is created and badged by the local process at the time it obtained the capability. This "local ID" can be used as key to locally stored meta data associated with the Genode capability. (3) An "external ID" seL4 cap that corresponds to the "local ID" of the originator of the capability when it was delegated to the process.
When delegating a Genode capability, the sender puts all three seL4 capabilities into the message. On the receiver side, (3) will be received as badge if the Genode capability originally came from the receiver (as (3) will correspond to a "local ID" at the receiver). In this case, the receiver can use the badge to re-identify the original Genode capability.
This approach would allow us to re-identify capabilities along the branches of the delegation tree, which suffices for Genode.
In general, caps are more expensive and are only required when needing to pass an unforgeable authority between entities. Adding a descriptor to an existing session cap is generally cheaper. I know this statement is probably blasphemous, but performance implications of a design matter as long as the security model remains sound.
I see that carrying three seL4 capabilities for one Genode capability is more costly than a one-to-one relationship. This will certainly show in a microbenchmark. But the impact (if any) on application performance is completely uncertain. Most of Genode's interfaces are designed such that they avoid capabilities as arguments. For assessing the influence on application-level, we could conduct the experiment to represent a Genode capability as a tuple of (seL4 cap, globally unique ID) and compare the result to the three-caps variant.
Last design pattern is to implement object "death notification" from F -> M, which would require a registration protocol: M->F. We use this in RefOS for processes, which I assume are much more coarse-grained than your dataspaces.
This would work for the specific lifetime-management example but it does not solve the re-identification issue in other scenarios. Just to give an example, a parent process P may have both a server and a client as child processes. The client established a session to the server through the parent. So the parent is the mediator. Both the parent and the client refer to the session using the corresponding session capability created and badged by the server.
Now, the client wants to instruct the parent to transfer memory quota from the client to the server. It does so by specifying the session capability and the amount to a 'transfer_quota' call at the parent. In this scenario, the operation cannot be triggered by a mere notification but requires the client and the parent to "talk about" the session (and naturally access meta data associated to it).
Note: We have mulled over the idea of an operation bool points_to_same_object(cap1,cap2), this would enable C passing a foreign cap (F) together with a handle to the metadata in M, and thus you could test if the passed cap corresponds with the cap associated with your metadata in M. I'd be interested if such an operation improve/eases the protocol design of interaction between your services.
We actually use this approach of passing a hint value along with each capability on Fiasco.OC. The hint is used by the receiver to lookup an already present capability. If such a capability exists, it compares the incoming capability with existing one using a kernel operation.
But this approach is hardly satisfying. First, it is prone to leaking information across process boundaries because the hint values must be allocated somehow. To mitigate the leakage of information, hint values would need to be translated between incoming hints and outgoing hints, which requires complicated book keeping. For this reason, we use global hint values on Fiasco.OC as a compromise. Third, each incoming IPC that carries one or more capabilities requires at least one additional system call for comparing the incoming capabilities at the receiver.
Even though the 'points_to_same_object' operation would enable me to implement the same approach as we use on Fiasco.OC, it would still be a compromise.
Best regards Norman
I hope you don't mind me spamming the list with my problems.
My perspective: please keep the questions and comments coming! Trying to follow along is helping to test my understanding of seL4 and to identify details where I am (at best) a little shaky.
In the rest of this email, I'd like to offer some reactions to Norman's original message. I hope those with more expertise than me, either regarding seL4 or the specific problems that Norman was targeting, will step in to offer corrections and clarifications.
For example, Norman suggested using badging as a way to attach server-local meaning to capabilities. But, as I understand the API, the only capabilities that can carry a badge are those for endpoints. A typical server receives requests from its clients through a single endpoint, for example. But if different clients use different capabilities for that endpoint, each with a distinct badge, then the server will still be able to distinguish between them: it just has to inspect the (unforgeable) badge value that is delivered with each message. This is my understanding of how badges work, but it doesn't allow for badges to be attached to capabilities for other types of object (a thread, for example).
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.
In other words, the ability to transfer capabilities over IPC might be more restricted than Norman had hoped. (I can imagine how the second restriction might be eased if IPC is allowed to create a sibling instead of a child when the source is already a derived capability. But (a) I don't know if this is how it works, and (b) this doesn't address the second restriction.)
[Aside: Dhammika Elkaduwe's dissertation explained how deeper levels of capability deriving (up to 128) could be supported, but it looks like this idea has been abandoned in the current API. Can anyone comment on the motivation for this? Thanks!]
I'll end by sketching an approach that came to mind when I saw Norman's example:
Now, I have the following scenario: There are three processes, a factory (F), a mediator (M), and a client (C). ... ... alloc create F <-------- M <--------- C
The challenge here is for M to be able to access meta data for capabilities that it has passed on from F to C.
For starters, I'm imagining some kind of "registration" step that initializes the connection between M and C. This process would leave C with a badged endpoint for communicating with M, which would provide a way for M to locate its meta data for C. In addition, this process would also establish a shared CNode object, mapped in to the cspaces for both M and C.
Now, if C wants a new capability from M, then it chooses a particular unused slot number (n, say) within the shared CNode, and includes that number as part of its request to M. If M approves the request and obtains the required capability from F, it installs that capability in the specified slot, updates the corresponding meta data, and returns control to C. Now C can use the new capability, to whatever extent is permitted, without having to go back to M. In fact C would even be able to delete the capability by itself. However, for accounting purposes, we would probably still expect C to send a message to M indicating that the capability in slot n is no longer needed; this would also trigger a further update of M's meta data for C. I think this could be made to work even if C has deleted the capability or moved it to another location in its cspace. For example, M might hang on to the original capability elsewhere in its cspace (outside the shared CNode), tracking the CPTR for that original cap as part of the meta data for slot n. This would allow M to perform operations on the underlying kernel object by using the original capability, without having to assume that the derived version is still in slot n.
Would something like this work? And Norman, would this (or something like it) meet your needs?
All the best, Mark
It does seem like capability transfer via an endpoint puts a derived copy of the transferred capability in the receiver's designated slot, rather than moving the transferred capability from the sender's CNode:
"A received capability has the same rights as the original except if the receiving endpoint capability does not have the Write right. In this case, the rights on the sent capability are diminished, by removing from the received copy of that capability the Write right." (section 4.2.2)
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.
In other words, the ability to transfer capabilities over IPC might be more restricted than Norman had hoped. (I can imagine how the second restriction might be eased if IPC is allowed to create a sibling instead of a child when the source is already a derived capability. But (a) I don't know if this is how it works, and (b) this doesn't address the second restriction.)
I believe that (as you imagine) copies of derived capabilities are 1) allowed, and 2) inserted into the CDT as children of the original capability (siblings of the derived one), if I've interpreted this line from section 3.1.4 correctly: "Further copies of these derived capabilities will create siblings, in this case remaining on level 5."
So I think the bullet you cite:
• The capability being transferred cannot be derived. See Section 3.1.4 for details.
is talking about capability transfers via endpoints being limited by the general derivation restrictions for specific kinds of capabilities (e.g. IRQControl) in Table 3.2, rather than saying that you can't transfer an unrestricted derived capability. That is, it's talking only about the first of the two restrictions you mention.
If capability c1d is derived from capability c1, and capability c1dd is derived from c1d, is making c1dd's CDT parent c1 instead of c1d just an optimization to reduce the CDT depth?
For underivable capabilities like IRQControl, is a shared CNode the only way to allow multiple tasks to access them?
If whatever capability (c1) being used to represent a dataspace is not restricted in Table 3.2, does it matter whether it's passed from M to C via a shared CNode (cn1) or via IPC? If M can depend on c1's index in cn1 not changing, then M could use that index as a key in a metadata table. That would only be guaranteed if we could grant C read-only access to cn1, i.e. prevent C from moving c1 to a different slot. It isn't clear to me whether or not seL4 supports this. Table 3.1 lists access right semantics for Endpoint, AsyncEP, and Page. Can access rights be attached to CNode capabilities as well? Does guaranteeing M a unique key associated with c1 (c1's index in cn1) solve Norman's problem?
Regards, Ted
On Sun, Nov 9, 2014 at 9:11 PM, Mark Jones mpj@pdx.edu wrote:
I hope you don't mind me spamming the list with my problems.
My perspective: please keep the questions and comments coming! Trying to follow along is helping to test my understanding of seL4 and to identify details where I am (at best) a little shaky.
In the rest of this email, I'd like to offer some reactions to Norman's original message. I hope those with more expertise than me, either regarding seL4 or the specific problems that Norman was targeting, will step in to offer corrections and clarifications.
For example, Norman suggested using badging as a way to attach server-local meaning to capabilities. But, as I understand the API, the only capabilities that can carry a badge are those for endpoints. A typical server receives requests from its clients through a single endpoint, for example. But if different clients use different capabilities for that endpoint, each with a distinct badge, then the server will still be able to distinguish between them: it just has to inspect the (unforgeable) badge value that is delivered with each message. This is my understanding of how badges work, but it doesn't allow for badges to be attached to capabilities for other types of object (a thread, for example).
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.
In other words, the ability to transfer capabilities over IPC might be more restricted than Norman had hoped. (I can imagine how the second restriction might be eased if IPC is allowed to create a sibling instead of a child when the source is already a derived capability. But (a) I don't know if this is how it works, and (b) this doesn't address the second restriction.)
[Aside: Dhammika Elkaduwe's dissertation explained how deeper levels of capability deriving (up to 128) could be supported, but it looks like this idea has been abandoned in the current API. Can anyone comment on the motivation for this? Thanks!]
I'll end by sketching an approach that came to mind when I saw Norman's example:
Now, I have the following scenario: There are three processes, a factory (F), a mediator (M), and a client (C). ... ... alloc create F <-------- M <--------- C
The challenge here is for M to be able to access meta data for capabilities that it has passed on from F to C.
For starters, I'm imagining some kind of "registration" step that initializes the connection between M and C. This process would leave C with a badged endpoint for communicating with M, which would provide a way for M to locate its meta data for C. In addition, this process would also establish a shared CNode object, mapped in to the cspaces for both M and C.
Now, if C wants a new capability from M, then it chooses a particular unused slot number (n, say) within the shared CNode, and includes that number as part of its request to M. If M approves the request and obtains the required capability from F, it installs that capability in the specified slot, updates the corresponding meta data, and returns control to C. Now C can use the new capability, to whatever extent is permitted, without having to go back to M. In fact C would even be able to delete the capability by itself. However, for accounting purposes, we would probably still expect C to send a message to M indicating that the capability in slot n is no longer needed; this would also trigger a further update of M's meta data for C. I think this could be made to work even if C has deleted the capability or moved it to another location in its cspace. For example, M might hang on to the original capability elsewhere in its cspace (outside the shared CNode), tracking the CPTR for that original cap as part of the meta data for slot n. This would allow M to perform operations on the underlying kernel object by using the original capability, without having to assume that the derived version is still in slot n.
Would something like this work? And Norman, would this (or something like it) meet your needs?
All the best, Mark
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
Hi Mark,
great to get back in touch with you! I vividly remember visiting your group at OGI in 2005. Back then I presented my work on secure graphical user interfaces and you introduced me to the House project. Good times. :-)
For example, Norman suggested using badging as a way to attach server-local meaning to capabilities. But, as I understand the API, the only capabilities that can carry a badge are those for endpoints. A typical server receives requests from its clients through a single endpoint, for example. But if different clients use different capabilities for that endpoint, each with a distinct badge, then the server will still be able to distinguish between them: it just has to inspect the (unforgeable) badge value that is delivered with each message. This is my understanding of how badges work, but it doesn't allow for badges to be attached to capabilities for other types of object (a thread, for example).
This is consistent with my understanding.
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.
The challenge here is for M to be able to access meta data for capabilities that it has passed on from F to C.
For starters, I'm imagining some kind of "registration" step that initializes the connection between M and C. This process would leave C with a badged endpoint for communicating with M, which would provide a way for M to locate its meta data for C.
I omitted this detail for brevity. In my example, C has already established a "session" to M, and M has already established a "session" to F.
In addition, this process would also establish a shared CNode object, mapped in to the cspaces for both M and C. Now, if C wants a new capability from M, then it chooses a particular unused slot number (n, say) within the shared CNode, and includes that number as part of its request to M. If M approves the request and obtains the required capability from F, it installs that capability in the specified slot, updates the corresponding meta data, and returns control to C. Now C can use the new capability, to whatever extent is permitted, without having to go back to M. In fact C would even be able to delete the capability by itself. However, for accounting purposes, we would probably still expect C to send a message to M indicating that the capability in slot n is no longer needed; this would also trigger a further update of M's meta data for C. I think this could be made to work even if C has deleted the capability or moved it to another location in its cspace. For example, M might hang on to the original capability elsewhere in its cspace (outside the shared CNode), tracking the CPTR for that original cap as part of the meta data for slot n. This would allow M to perform operations on the underlying kernel object by using the original capability, without having to assume that the derived version is still in slot n.
That is an interesting approach. C and M talk merely about plain session-local numbers. It seems to be somehow similar to the "hint" approach I mentioned in my previous email but it alleviates capability delegation via IPC.
Would something like this work? And Norman, would this (or something like it) meet your needs?
I cannot answer this question right away. The challenge would be to find a good way to hide this mechanism behind the generic Genode API.
Thank you for chiming in and for the interesting idea of sharing entire CNodes (as opposed to delegating individual capabilities) between client and server.
Cheers Norman
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.
After this operation, the copy is inserted into the receivers CSpace. This operation does modify the CDT and does not fail.
To make this more precise: the CDT operation will not fail. The CSpace insertion itself may fail if the receiver did not provide sufficient free slots.
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.
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:
- 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.
- 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.
-
Gerwin Klein -
Kevin Elphinstone -
Mark Jones -
Norman Feske -
Ted Cooper