Re: Capabilities interact nicely with Substructural Types and Reactivity

On Thu, Sep 12, 2013 at 4:13 PM, David Barbour <[email protected]> wrote:

>
> On Thu, Sep 12, 2013 at 3:40 PM, Karp, Alan H <[email protected]> wrote:
>
>>  **è **For example, it may be that we want to forbid the untrusted code
>> from constructing its own local state
>>
>> OK.  I’ll be the kid in class who asks the question a lot of the other
>> kids are too shy to ask.  What is the value of such a restriction?  It
>> sounds to me like a language that doesn’t allow you to allocate temporary
>> space.  A simple use case would help me understand the requirement.
>>
>
> Temporary space isn't the issue; it's very easy to model temporary space
> in a pure way.
>
> But controlling *state* is valuable.
>
> If you know an object isn't stateful - i.e. that it cannot remember its
> past inputs - then whole classes of security, consistency, and correctness
> issues can be eliminated. One can prevent time-bomb behaviors that might be
> resistant to basic testing and analysis.
>

E's DeepFrozen and Joe-E's Immutable give you exactly this. The fact that a
DeepFrozen object can make fresh mutable objects in no way weakens these
guarantees.



> And some implicit optimizations (e.g. parallelization) are feasible.
>

E's DeepPassByCopy or Data, which are closely aligned with DeepFrozen,
should give you this. I suspect the same should be true of Joe-E's
Immutable but I don't know. In any case, this is not a security benefit.



>
> If you can control what state an object uses - i.e. if you provide it
> through a factory - then it becomes easier to audit that state, plus a
> bunch of non-security benefits (easier to persist, extend, reset, freeze,
> rewind, etc. the state).
>

Ok, this one I understand. For example, Joe-E-on-Waterken objects could not
evade being persisted and revived, and also could not sense whether this
had happened. This is a consequence of the fact that the only memory it
could allocate is memory that the Waterken framework effectively granted
it. In KeyKOS, such patterns of granted memory rights could be expressed
directly in ocap terms. This does have security benefits. Thanks.


>
>
>
>
> _______________________________________________
> 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