Re: cap exchange race with map/unmap

[Marcus Brinkmann]

At Wed, 19 Oct 2005 09:39:43 -0400,
"Jonathan S. Shapiro" <address@hidden> wrote:
> 
> Marcus:
> 
> Please re-send using the more careful notation. I suspect that you
> aren't getting out the revocation hierarchy that you think you are.
> Whether I am right or wrong, it is better to be sure.

I am not sure which notation you mean.  I vaguely recollect seeing
something like that, but I didn't find it in the archive anymore.

But I can give you a sequence of operations:

Initial state:

The server S implements an object, managed by the capability server C.
There is a revocable copy from S to C or vice versa, doesn't really
matter here.  What does matter is that both S and C have the privilege
to read out a protected payload field in order to identify a
capability to the object should they receive it from some client in an
RPC.  This is the identify or map_lookup operation.  The technical
details are not very important.  For example, it suffices that C can
read out the field, then S could read it out by making an upcall to C.
The details are only relevant for evaluating the performance.
However, it is of course required that the protected payload is
created by C, and globally unique among all managed capability objects
in C (and S).

Furthermore, client A has a revocable copy from C.  It also has a
communication channel to B.  Now it wants to give B a real copy.  Here
is the sequence diagram.

Please let me use "mapping" for revocable copy.  Makes it clearer in
the context of L4.

1. A calls B and maps the capability in the call.  Note: B does
   not return yet.

2. B calls C and maps the capability in the call.  Note: C does not
   return yet.

3. C identifies the capability and then unmaps the one it got from B
   (it's not needed anymore).  Now it returns to B, mapping the
   capability in the return message (either by creating a new mapping
   from the "root mapping" it holds, or by creating a new mapping from
   the mapping it got from S, depending on the details between C and
   S).

4. B installs the mapping it got from C and unmaps the mapping it got
   from A (it's not needed anymore).  B returns to A.

5. A can now revoke the mapping it gave to B.

Note: If at any point, A revokes the mapping before completion of step
3, the identify operation will fail and no copy will be created.
Afterwards, it doesn't matter.

I leave the ASCII art intact below for reference.

Thanks,
Marcus

> > Before copy operation:
> > 
> >            RevCopy               RevCopy
> > Server S ----------> CapServer -----------> A
> > 
> > After A initiated the copy operation to B:
> > 
> >            RevCopy               RevCopy        RevCopy
> > Server S ----------> CapServer -----------> A ----------> B
> > 
> > After B initiated the copy operation from the cap server.
> > 
> >            RevCopy               RevCopy        RevCopy
> > Server S ----------> CapServer -----------> A ----------> B
> >                              ^                            |
> >                              |           RevCopy          |
> >                              +----------------------------+
> > 
> > The revocable copy from B to the cap server proves to the cap server
> > that B possesses the capability, and furthermore allows the cap server
> > to identify the capability to copy in the first place!
> > 
> > At the end of copy operation:
> > 
> >            RevCopy               RevCopy        RevCopy
> > Server S ----------> CapServer -----------> A ----------> B
> >                              |                            ^
> >                              |           RevCopy          |
> >                              +----------------------------+
> > 
> > The copy from B to the cap server has been removed.  It's not needed
> > anymore.
> > 
> > After the copy operation:
> > 
> >            RevCopy               RevCopy
> > Server S ----------> CapServer -----------> A
> >                              |
> >                              |   RevCopy
> >                              +------------> B
> > 
> > The copy from A to B has been removed.  It is not needed anymore.  Now
> > A and B have a co-equal copy.
> > 
> > Thanks,
> > Marcus
> > 
> 
>