Re: Capabilities interact nicely with Substructural Types and Reactivity

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.