Re: Why COPY != SIMULATED COPY

[Jonathan S. Shapiro]

On Wed, 2005-10-19 at 20:06 +0200, Espen Skoglund wrote:
> [Jonathan S Shapiro]
> > Now consider what happens in the Marcus/Neal protocol (as described):
> 
> >     STEP                         EFFECT ON SYSTEM STATE
> >     [Initially]                  A has Cap
> 
> >       RevCOPY(Cap)
> >    A --------------> B           B has Cap.1
> 
> >       SimCOPY(Cap.1)
> >    B --------------> C           C has Cap
> 
> > At the end, A has the initial capability Cap, B has a revocable
> > capability Cap.1, but what does C have? In the Marcus/Neal protocol,
> > C has Cap, not Cap.1.
> 
> As far as I understood the protocol proposed, the last step you
> describe is wrong.  During SimCopy() the following will happen:
> 
>         RevCOPY(Cap)
>      A --------------> C           C has Cap.2

Thank you. This is a WONDERFUL illustration of why none of us can afford
to take shortcuts describing these protocols. I wrote the fully expanded
protocol on my classroom blackboard today. It really is wrong, but I
agree that I have failed to illustrate this adequately here.

Since it is Marcus and Neal's protocol, perhaps it would be better for
*them* to try to state it in this form. That way I will not introduce
new errors from misinterpretation.

> The question now is how revokation works.  Using the current L4 UNMAP
> semantics, "Revoke(Cap)" actually means something like
> "Revoke(Cap.*)".  That is, all revokable copies derived from Cap are
> revoked (including Cap.2).  You thus don't defeat selective
> revocation.

Yes, but this is because my description of the protocol is wrong. Let us
both wait and respond to a concretely captured protocol from them.

> There has been other discussions about "selective revocation" in
> UNMAP; not to be confused with "selective revocation" as discussed
> above.  The selective revocation I'm talking about here (let's call it
> "targeted revocation" to avoid confusion) allows you to specify
> something like "Revoke(Cap.S)", where S is a subset of all natural
> numbers (implemented as a number range, or mask, or whatever you
> like).  The other important change with targeted revocation is that
> someone performing a RevCOPY can decide on the child number of the new
> cap.

We considered a similar kind of "filtered revoke" in EROS many years
ago. Unfortunately, it is incompatible in practice with persistence (I
can just hear the pages going in and out from the disk now while we
search for all of those capabilities).

Actually, this appears to be a problem with the scalability of the L4
mapping database too. Is there some way to preserve reasonable
efficiency of traversal when the mapping database becomes an on-disk
data structure? It seems to me that it doesn't matter whether it is a
kernel or user data structure at that point. Either way it is a
disk-based tree, and we are doing an extended tree traversal. Wrappers
do not have this issue, so I am sure that there must be a representation
trick that could be used in L4sec to avoid this concern.

> Anyhow, this "targeted revocation" is a bit of a digression.  It is
> not important for the discussion at hand.  I only mention it in case
> someone has heard about the alternative UNMAP operation and wonders
> how it fits in.

Thank you!

> 
> [...]
> 
> > Given such a CapServer, the initial part of the protocol remains
> > similar:
> 
> >     STEP                         EFFECT ON SYSTEM STATE
> >     [Initially]                  CapServer has Cap.1
> >                                  A has Cap.1..x.1
> 
> >       RevCopy(Cap.1..x.1)
> >    A --------------> CapServer   CapServer has Cap.1..x.1.1
> 
> >      [Intention: A is saying: I authorize CapServer to create
> >       capabilities that are co-equal to mine]
> 
> >    CapServer ------> A           [none: CapServer is returning]
> 
> >       RevCopy(Cap.1..x.1)
> >    A --------------> B           B has Cap.1..x.1.2
> 
> >       RevCopy(Cap.1..x.1.2)
> >    B --------------> CapServer   CapServer has Cap.1...1.2.1
> 
> >       ??MagicOp??(Cap.1...x)
> >    CapServer ------> B           [B has Cap.1..x.2]
> 
> Since CapServer knows that Cap.1..x.1.1 is identical to Cap.1, it can
> perform the following last step:

How does it know this? By what authority?

> > The remaining questions are:
> 
> >   1. By what authority is CapServer permitted to fabricate a
> >      capability cap.x....y (for arbitrary y) given that it already
> >      holds a capability cap.x? That is: what is "MagicOp"
> 
> CapServer need not have the authority to fabricate a new capability.
> It simply needs to identify "its own version" of the the capability
> and RevCopy this version to B.

My question was not clear enough. Yes, CapServer can certainly fabricate
a new capability, *provided* the new capability is a direct child (in
the revocation tree) of some capability that CapServer already holds.
The question here is: how is CapServer authorized to create a new
capability NewCap that will become a child of some other capability
OtherCap that is not held by CapServer. This is required because NewCap
must end up installed at the proper place in the revocation hierarchy.
In justifying the operation, we may assume that CapServer holds an
ancestor of OtherCap.

And assuming that we can rationalize this justification, what operation
is used to actually perform the fabrication of this distantly descended
capability?

> >   2. How do we make sure we get the permissions right? That is: what
> >      are the proper arguments to MagicOp?
> 
> CapServer must have the right to inspect the permissions of the
> capability it receives from A (i.e., Cap.1..x.1.1).

Or the permissions reduction can be made part of the primitive operation
that constructs a distantly descended capability.


shap