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
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