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