Re: Why COPY != SIMULATED COPY

[Marcus Brinkmann]

At Wed, 19 Oct 2005 20:06:54 +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

This is not true, as A is not involved in the SimCOPY from B to C.

Instead, what happens is this:

    STEP                         EFFECT ON SYSTEM STATE
    [Initially]                  B has Cap.1

    RevCOPY(Cap)
B ---------------> C            C has Cap.1.1

    RevCOPY(Cap)
C ---------------> CapServer    CapServer has Cap.1.1.1

CapServer   IDENTIFY  CapServer (no effect)
 Cap.1.1.1 --------->  CapObject

           RevCOPY(Cap)
CapServer -------------> C      C has Cap


Note that I had to write "CapObject" because we started out with A
having Cap, although in reality A has "Cap.1", which is a revocable
copy from Cap, which the CapServer has.  You can do a metasyntactical
substitution here, if you want.
 
> > Later, when A revokes Cap.1, C will not lose its copy. Thus
> > SIMULATED COPY does not accurately simulate COPY. More importantly,
> > the entire purpose of selective revocation has been defeated and a
> > critical security mechanism has disappeared.
> 
> 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.

You are correct, but in a mathematical (ie, painfully accurate but
meaningless :) way.  What Jonathan points out here is that B can
escape the "confinement" that the revocable copy is supposed to
create.  For example, C could sim-copy the capability back to B (or B
could just sim-copy the capability to itself!).
 
> There has been other discussions about "selective revocation" in
> UNMAP; not to be confused with "selective revocation" as discussed
> above.

Right, there is that, too.  We are in the dangerous zone of overloaded
terminology here.

> > This gives the correct outcome, because A cannot now revoke B's
> > copy, but revocation of any capability *upstream* from A causes the
> > capability held by B to be revoked.
> 
> > 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.

Which is semantically not what Jonathan wants to achieve.  A sim-copy
of a revocable copy _should_ be a mapping to A, not to the CapServer.
Jonathans result is that this is impossible without also having a real
copy operation.

> >   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).  It can use these
> permissions as a mask during the RevCopy operation.  (In L4 speak: it
> can use these permissions in the MapItem for the UNMAP operation.)

If you mean that this permission bit can be used to check if A wanted
to allow a sim-copy to happen, or if A wants to reserve the right to
revoke the copy without a chance for B (and C) to escape, then this is
what I wrote in my reply to Jonathan's mail.  It works in preventing
the "escape" problem, but it doesn't make sim-copy a real copy.

Thanks,
Marcus