[cap-talk] Selling capabilities programming

[Marcus Brinkmann]

At Thu, 26 Jul 2007 00:41:59 -0400,
"Jonathan S. Shapiro" <shap at eros-os.com> wrote:
> This question reveals a fairly fundamental point that Marcus Brinkmann
> made in passing earlier: should capabilities pass by "copy" (i.e. the
> received capability is co-temporal) or by "map" (received capability is
> destroyed when the send capability is destroyed). There are arguments to
> be made in both directions. L4.sec  has a map operation but no copy
> operation (at least, not when I looked last).

I should say that seL4 (NICTA) has different semantics.  They use a
mapping database, but in a very restricted fashion.  I am abstaining
from given details, because I did not understand it in full yet, and
don't want to say anything wrong, but most delegations seem to have
copy semantics, while only some delegations have map semantics (with
tight restrictions).

I also don't know how/if L4.sec developed recently.

> I believe that L4 is missing an operation, which we might call
> "unsplice". This is a variant unmap operation in which the process
> performing the unsplice is voluntarily relinquishing it's right to unmap
> recursively. That is, if we have a revocation chain A->B->C, unsplice(B)
> yields the chain A->C. Such an operation would allow your intervening
> word processor to exit sensibly, which appears (to me) to be difficult
> to handle in the current L4.sec design. Perhaps they have a simple
> solution. They often do.

A very simple solution is for the word processor to stay alife as a
shell for the excel process, dropping most of its resources.  

> In effect, "map" may be considered to introduce a "wrapper" on every
> communication. For reasons that we discussed extensively here, wrappers
> are not entirely effective as membranes, and therefore do not form an
> effective basis for revocation. However: the L4 "map" primitive is
> somewhat better than simple wrappers. If handled correctly by the object
> server, the object server is able to ensure that the temporal scope of a
> read-only cap derived from a read-write cap is bounded by the temporal
> scope of the read-write cap.

Ah yes, there is that.

Thanks,
Marcus