Re: Why COPY != SIMULATED COPY

[Jonathan S. Shapiro]

On Wed, 2005-10-19 at 21:04 +0200, Espen Skoglund wrote:

> Right.  This is clear.  My question was more about what you actually
> want to achieve in practice.  That is, if C wants to be paranoid about
> the capability not suddenly disappearing (because of malice or fault),
> it must make sure that all the subjects that can revoke the cap it
> receives are subjects that it trusts.
> 
> If we have the case that C is paranoid, and if there exists a path
> between A and B above and C only trusts A, then getting a co-equal
> capability from B does not satisfy C's paranoia requirements.
> 
> On the other hand, if we don't have this paranoia requirement, then
> just adding the few lines of code that implements COPY in L4 is no big
> deal at all.
> 
> I suspect that you never really had to deal with scenarios such as
> these in EROS since you generally only perform COPY operations and
> thus don't have long chains of revocable copies.

Correct on all points, except that no paranoia is required for REVOCABLE
COPY to be a big problem. Here is a copy of a response that I sent to
Harvey Tuch yesterday concerning the semantic problems that arise from
REVOCABLE COPY.

On Tue, 2005-10-18 at 15:04 -0400, Jonathan S. Shapiro wrote: 
> On Tue, 2005-10-18 at 08:40 -0700, Harvey Tuch wrote:
> > Hi Jonathan,
> > 
> > Can you elaborate on this goal, i.e. explain what a sensible formal 
> > semantics for client/server computation would be? I've worked a fair 
> > bit with a formal semantics for L4 map/unmap and I'm interested in 
> > potential applications such as this.
> > 
> > Cheers,
> > Harvey
> 
> No, but perhaps I can clarify what I was trying to say better, translate
> your question, and answer that. :-)
> 
> First, let me introduce a sloppy notation for object creation. I assert
> that the formal semantics of object creation in a capability system is
> approximated by:
> 
>   cap = (let ((repr-state (allocate-the-object-representation)))
>           (lambda (op . args)source
>             (cond ((== op op1Opcode) (f1 args))
>                   ((== op op2Opcode) (f2 args))
>                   ...
>                   ((== op lastOpcode) (fN args)))))
> 
> Please note that I am NOT assuming first-class messages. I am also
> ignoring the fact that clients and servers exist in a coroutine
> relationship -- the above formalism is only adequate to describe RPC
> design patterns. If I want to use scheme-like notation to describe
> coroutines, I will need some primitives that need to be built on
> top of call/cc, but the continuations used by these primitives do not
> escape and will be invoked at most once.
> 
> In a system where the primitive transfer operation is COPY, then if
> process A sends a capability c0, process B will receive a capability c1
> s.t.
> 
>        c0 =ident= c1
> 
> I do not mean to imply that an EQ test is available for use by the
> communicating processes. What I am trying to say is simply that the two
> capabilities denote the same object and therefore have the same
> behavior. Depending on what the object does, we may not always be able
> to reason formally about the implementation of the object, but in some
> cases we can, and whatever the outcome it is the same for c0 and c1.
> 
> In particular, we know that the capability c1 does not depend in any way
> on the behavior of A as a consequence of COPY.
> 
> My best approximation to REVOCABLE COPY looks something like this:
> 
>   c3,c4 = (let ((valid #t))
>             (lambda () (set! valid #f))
>             (lambda ANY-ARGS
>               (if valid (apply original-cap ANY-ARGS) ; not revoked
>                         (throw InvalidCap))))  ; revoked
> 
> where c3 is a capability conveying the right to revoke, and c4 is the
> revocable capability. c4 is then transferred by COPY. [The operation can
> be done as a single operation in the implementation -- I am trying to
> tease apart the steps in order to be explicit about the semantic
> construction].
> 
> So in general we may consider the semantics of the received capability
> to be contingent on an equivalence class of capabilities similar to c3,
> and in addition dependent on a few other capabilities. Specifically, the
> received capability is contingent on the set
> 
>     { /c3/, sb, orig-cap }
> 
> where by "/c3/" I mean the open inductively defined set of revocation
> capabilities that may be created by successive applications of REVOCABLE
> COPY occurring in sequence. The capability "sb" is the capability to the
> storage source (because we are dependent on this for continuing object
> existence), and the capability "orig-cap" is the original capability to
> the object (because we are of course dependent on the object's
> behavior).
> 
> But this notation is poor, because in fact we are not dependent on the
> capabilities per se. What we are really interested in is establishing
> some understanding of the set of processes who may cause our effective
> authority to flip from "good" to "invalid". At any frozen instant in
> time, this set is the set of all processes that hold one or more of the
> above capabilities.
> 
> In order to express any theorem to the effect that invocation of a
> capability yields a predictable result, we must be able to reason about
> this set of processes and their behavior.
> 
> The empirical observation is that if you are the creator of an object,
> it is very easy for you to control the proliferation of "orig-cap".
> Depending on the design pattern, it may or may not be straightforward to
> control the proliferation of "sb", but it is usually possible to ensure
> that if "sb" dies you die with it, whereupon the resulting errors cease
> to be your problem.
> 
> But there is no hope, in general, of controlling the proliferation of
> capabilities in the equivalence class /c3/, because this proliferation
> is performed by processes whose behavior you do not know and cannot (in
> general) influence.
> 
> So I think I mis-wrote. I think we understand the semantics of
> revocation pretty well. The problem is that the implications for
> per-object operational semantics very easily spills over into a
> non-local and generally undecidable computation. While it is decidable
> in finite systems, that decision procedure requires either a "God's eye"
> view of the system (we cannot reasonably grant such authority in
> practice) or an inductively established constraint on future computation
> similar to the one imposed by the EROS constructor in order to impose
> confinement.
> 
> 
> shap