6 Nov
2014
6 Nov
'14
1:31 p.m.
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
6 Nov
6 Nov
10:31 p.m.
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(a)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.
7 Nov
7 Nov
6:09 p.m.
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
--
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
10 Nov
10 Nov
5:11 a.m.
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
11 Nov
11 Nov
2:27 a.m.
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(a)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(a)sel4.systems
> https://sel4.systems/lists/listinfo/devel
12:32 p.m.
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
--
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
10 p.m.
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.
11:21 p.m.
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.
13 Nov
13 Nov
10:58 a.m.
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:
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
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.
2745
days inactive
2752
days old
8 comments
5 participants
participants (5)
-
Gerwin Klein -
Kevin Elphinstone -
Mark Jones -
Norman Feske -
Ted Cooper