[cap-talk] 'Destroy' vs 'Sever'

[David Hopwood]

Jed Donnelley wrote:
> On 11/21/2007 5:05 PM, David Hopwood wrote:
>> [...]
> 1.  Our NLTSS system had what I believe are these
> operations.  We called them 'Destroy' and 'NewCap'.
[...]
> 2.  I agree that 'Sever' is similar to a 'revoke'.  It
> is more efficient and requires less setup than supporting
> revoke through a separate server - whether with the all
> references semantics or if only for a specific capability
> instance.  However, 'Sever' revokes all references to
> an object, not just a single reference as with 'revoke'.
> 
> 3.  Any extension mechanism worth it's salt can support such
> a 'Sever' call on it's objects, so the issue of whether or not
> to support 'Sever' seems to me object specific and out of
> the realm of discussion for any TCB/kernel discussions (e.g.
> vs. something like EQ).
> 
>> That's also true if 'Destroy' is available but 'Sever' is not.
> 
> 4.  I think David Hopwood (was it?) was suggesting that with
> Sever one can revoke a reference (all reverences actually
> if I have it right and it is like with NLTSS) without
> actually destroying the object itself.  I believe the
> semantics of 'Sever' can be achieved by copying out
> all the relevant object state into a new object and then
> 'Destroy'ing the old object (though of course there may
> be timing issues).
> 
>> The issue raised by 'Sever' is that the new reference it returns
>> will point to an object that may malfunction, as a result of not
>> receiving messages directed to the old object.
> 
> 5.  This of course depends on the nature of the object and its
> state.  For example, a file/page/segment will not 'malfunction'
> in this way with typical semantics.

But the objects whose storage is backed by the file/page/segment
may malfunction.

[...]
>> This is especially problematic when the object is part of a (nontrivial)
>> composite: the Sever operation will break "internal" links from other
>> objects of the composite to the severed object, but it won't destroy
>> or sever those other objects. The resulting behaviour will depend on
>> implementation details of the composite; it won't in general have a simple
>> explanation in terms of the composite's documented behaviour.
>>
>> [*] 'Destroy' also won't destroy other objects in the composite, but it
>> will prevent the destroyed object from being invoked and from performing
>> any invocations. At the point at which another object of the composite
>> tries to invoke the destroyed object via an existing reference, it will
>> receive an error (typically reported as an exception at the language level),
>> which assuming it is not ignored, will abort the current "plan" of the
>> other object.
> 
> I'm sorry, but I don't understand the issue above.  Perhaps an
> example "composite" might help?  I don't see a significant difference
> between 'Sever' and 'Destroy' with regard to any such composite
> object.  In both cases any references in the 'composite' will
> return "Invalid" when invoked.  As I noted above, equivalent
> semantics to 'Sever' can be implemented in most cases by
> copying object state and then doing a 'Destroy'.

I probably explained this poorly. Indeed the statements in the above
paragraph (marked [*]) are true for both Sever and Destroy.

The difference is that in the case of Sever, the other objects in the
composite can still be invoked by the copy of the severed object (either
because it is an active object/process, or due to invocations of the copy
via the reference returned by Sever). For Destroy, this can't happen
because the destroyed object no longer exists.

Consider an implementation of a composite data structure, say something
like a tree, with one visible facet representing the root. An operation
on this facet may delegate to one of the internal objects. Suppose that
under some circumstances, an internal object needs to call back to the
root object in order to maintain a global invariant of the composite --
for example to rebalance the tree.

(I'm assuming a concurrency model in which there is mutual exclusion
between concurrent invocations of an object, but this does not prevent
recursive invocations. Either an event-loop model, or a model using
reentrant mutexes or monitors has this property.)

Now the root object is severed. The internal objects still have references
to the old root, but they cannot be successfully invoked. We perform some
operation via the new reference to the root, that requires the callback.
It fails, but the composite's invariant has already been violated (without
Sever, it was valid to assume that the callback would succeed). Further
calls may misbehave in ways that eventually cause security problems. So
the presence of the Sever operation implies that this composite is not
defensively consistent.

The "clone then destroy" emulation of Sever doesn't have the same problem.
This is because the clone() method on the main facet of a composite should
be implemented to create a deep copy of the composite. If we then Destroy
the original main facet, the deep copy will remain intact, without any of
its internal references being broken.

Is it feasible to implement "Sever-safe" abstractions, i.e. composites
that are are defensively consistent even though some of their internal
references can be invalidated without warning? I think this is simply too
difficult in general. It may be feasible if the use of Sever were restricted
to certain objects that are passive and have a simple structure. However,
restricting Sever to these cases makes it much less useful for "unplanned"
revocation.

Since Destroy need not be restricted to passive objects with a simple
structure, it remains useful and safe for unplanned revocation. (At least,
it is not unsafe for the same reason as Sever. The paragraph marked [*]
above was attempting to argue why the fact that a composite may be only
partially destroyed, does not make Destroy unsafe. It is possible that
there may be other arguments against it that I haven't considered.)

It might also be feasible to write Sever-safe composites in a system
supporting transactional updates (because an operation that requires the
callback will be rolled back, so that the resulting state does not violate
the invariant). Most existing capability systems do not support
transactional updates.

In KeyKOS, Sever was apparently restricted to node and page objects.
But these were objects that could provide "backing storage" for other
arbitrary objects. Revoking the storage for some, but not all of the
objects that make up a composite can cause similar problems to that
described above. For this argument, it does not matter whether Sever
is a primitive, or an operation on an object such as a space bank.

It might be possible to define a Sever-like operation that would guarantee
to sever all of the objects in a composite at the same time. It isn't clear
that this is worth the complexity, given that the "clone then destroy"
emulation of Sever doesn't have the described problem.

(In E, it might be reasonable to 'sever' a vat, i.e. create a clone
of the vat that retains its outgoing references, but has no incoming
references. In that case, all of the objects of a given composite could
be assumed to be in the same vat. But I haven't really thought about this
very hard, so there may be some reason why it is a bad idea, or it may not
be sufficiently useful.)

>>>> I have not delved into such systems enough to say whether you want this to
>>>> always be available on every reference.  One issue is that it is a really
>>>> simplified instance of the revocation pattern, so many users of the
>>>> revocation pattern will not be able to use this primitive.
>>
>> Yes; both 'Sever' and 'Destroy' only work when the requirement is to
>> revoke *all* current references to an object.
> 
> 6.  and I believe the above makes 'Sever' different from 'revoke'.
> E.g. if I ask an object for a reduced permission instance
> (e.g. a RO file from a RW file), 'revoke' on either capability
> will leave the other intact (not referring to 'membrane'
> semantics which are of course richer).  'Sever' will invalidate
> all references to the underlying object.

Well, for a caretaker-based implementation of revocation, what will be
revoked is all facets that are derived from the caretaker. For example
if you create a RW file (A) with a caretaker (B), and then an RO facet (C)
derived from B, then revoking the caretaker will revoke B and C but
not A.

Similarly, Sever (or Destroy) will revoke all facets derived from the
severed object: if you create a RW file (A) with a transparent forwarder
(B), and then an RO facet (C) derived from B, then severing B will revoke
B and C but not A.

So technically, Sever (or Destroy) and caretaker-based revocation are
similarly expressive in this respect. But note that in this example we
needed to anticipate that the transparent forwarder B would be needed,
in order to revoke B but not A. In other words, TANSTAAFL: Sever doesn't
allow us to revoke objects selectively without anticipating the possible
need to do so.

> 7.  I believe 'Destroy' suffices in general.  As noted above
> I believe 'Sever' (our 'NewCap') can be effected by copying
> state and doing a 'Destroy'.

See above for why "clone then destroy" is safer because it creates a
deep copy. Sever (and NewCap?) is equivalent to atomically creating
a *shallow* copy and then destroying the original. I claim this is
usually not what you want.

-- 
David Hopwood