Re: Capabilities interact nicely with Substructural Types and Reactivity

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.


On Thu, Sep 12, 2013 at 11:15 AM, Mark S. Miller <[email protected]> wrote:

> I think the DeepFrozen auditor (or likewise the Immutable auditor of
> Joe-E) solve both of these quite well -- essentially by ensuring that the
> value in question has no mutable state. By the conventional meaning of
> "pure function", DeepFrozen is a looser restriction. Pure functions are
> deep frozen but not all deep frozen objects are pure functions.
> Nevertheless, DeepFrozen is adequate (and pleasant) for ensuring
> determinism and confinement. Likewise for Immutable in Joe-E.
>
>
> On Thu, Sep 12, 2013 at 9:52 AM, David Barbour <[email protected]>wrote:
>
>> Compared to languages with pure functions, such as Haskell, I do not
>> believe that E has "good support" for all forms of determinism and
>> confinement.
>>
>> For example, in E it is difficult to create large behaviors that cannot
>> remember their inputs... except by re-constructing these behaviors once per
>> input (which can be very inefficient). This regards, a form of determinism
>> - where we deterministically obtain the same output for the same input.
>>
>> Similarly, in E it can be difficult to enforce that a factory does not
>> interact with its objects after construction or prevent direct interaction
>> between objects from the same factory, unless of course it's a factory of
>> some relatively specialized 'value' types. This regards a form of
>> confinement - syntactically bounding influence and control over values in
>> the language.
>>
>> On Thu, Sep 12, 2013 at 9:00 AM, Mark S. Miller <[email protected]>wrote:
>>
>>> David, I don't think I get your point either. How would these issues
>>> affect determinism or confinement? E is oo ocaps with good support for both
>>> determinism and confinement.
>>>
>>>
>> _______________________________________________
>> cap-talk mailing list
>> [email protected]
>> http://www.eros-os.org/mailman/listinfo/cap-talk
>>
>>
>
>
> --
>     Cheers,
>     --MarkM
>
> _______________________________________________
> cap-talk mailing list
> [email protected]
> http://www.eros-os.org/mailman/listinfo/cap-talk
>
>

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