Re: Capabilities interact nicely with Substructural Types and Reactivity

The most relevant paper is <
http://www.cs.berkeley.edu/~daw/papers/pure-ccs08.pdf>. It is a good read
and describes excellent work. Highly recommended.

Regarding all the points made so far on this thread, E and Joe-E are
equivalent. There are subtle differences which I will mention if they
become relevant.

DavidB,

Your point about the whitelist is valid though. DeepFrozen is equivalent in
expressiveness to the KeyKOS Factory without a whitelist. In fact, I got to
it by starting with the KeyKOS Factory and simplifying it, mostly by
throwing out the whitelist. I knew at the time that this results in a loss
of expressiveness. See the section "Can We Do Less?" at <
http://www.erights.org/elib/capability/factory.html>.

I would be interested in your opinion about whether the KeyKOS Factory with
whitelist is compositional in the way you mean. It is certainly
compositional in many ways, but I don't know precisely what you mean here
by compositional.

Whether an auditing-based system could be extended with a
KeyKOS-Factory-like whitelist is an interesting question I don't know the
answer to.



On Thu, Sep 12, 2013 at 3:00 PM, David Wagner <[email protected]> wrote:

> I admit I'm puzzled by your email.  Have you looked at
> E's DeepFrozen and Joe-E's Immutable in detail?  There
> seem to be a number of points that don't seem to match
> how I would have described the situation.
>
> I confess I don't understand how using immutable/DeepFrozen
> objects/types is "selling out", but maybe that just reflects a
> difference in values or philosophy or something.  So I'll let
> that one pass by.
>
> Despite what you write, in Joe-E, the Immutable type does
> not forbid code from constructing its own local mutable state.
> In Joe-E it is possible to write a method that is verifiably
> deterministic (meaning that its externally-observable
> behavior is deterministic) yet also uses local mutable state.
> So, your characterization is not quite right.
>
> As far as loss of expressivity, the Joe-E paper discusses some
> implementation experience with using Joe-E, so there is some data
> on this you can peruse if you are interested.  Would you like
> references to the Joe-E papers?
>
> Contrary to what you write, Joe-E's Immutable type does provide a
> way to ensure determinism.  Read the papers for details of how that
> works; it's a little more detailed than I want to try to summarize in
> this
> email.  It's a good idea to understand the design before critiquing
> it.  E's DeepFrozen might work a little bit differently, and I can't
> speak
> to the details of how it interacts with verifiable determinism, but
> others might be able to.
>
> Generally speaking, in a capability design, if you want to let untrusted
> code access some capabilities and not others, a typical strategy
> is to pass the untrusted code the capabilities you want it to have
> access to and take care to never pass it the capabilities you don't.
>
> I suspect we're talking past each other somehow....
>
> -- David
>
> On Thu, Sep 12, 2013, at 01:42 PM, David Barbour wrote:
> > What draws me to capability security is the promise of
> > security-by-construction, the promise of robust composition. I want
> > flexible expression without a computer telling me 'no' after I obey the
> > rules that are locally and syntactically valid.
> >
> > It is true that relying on deep introspection and white-box analysis can
> > offer extra guarantees.
> >
> > But to depend on it seems like cheating, like selling out.
> >
> > Further, relying on analysis can damage expressiveness. For example, it
> > may
> > be that we want to forbid the untrusted code from constructing its own
> > local state, while at the same time we wish for the untrusted code to use
> > capabilities that provide access to our (potentially audited) state.
> > Unless
> > DeepFrozen is designed with this idea in mind (e.g. accepting a
> > capability
> > whitelist), it can reject valid programs; and even if it does accept a
> > whitelist, the act of building the whitelist results in a
> > non-compositional
> > system.
> >
> > Compare: if obtaining state is granted by capability, rather than by
> > ambient authority, then you could easily enforce deep frozen or immutable
> > structures, or partially frozen, or anything in between. Without
> > analysis.
> > It would be constructive, compositional.
> >
> > ...
> >
> > And despite your selling out, a DeepFrozen auditor still doesn't address
> > the issue of determinism. It can still create a unique stateful object
> > every time it is called with the same argument.
> _______________________________________________
> cap-talk mailing list
> [email protected]
> http://www.eros-os.org/mailman/listinfo/cap-talk
>



-- 
Text by me above is hereby placed in the public domain

  Cheers,
  --MarkM

_______________________________________________
cap-talk mailing list
[email protected]
http://www.eros-os.org/mailman/listinfo/cap-talk