[cap-talk] Abstractions that subsume capabilities
naasking at higherlogics.com
Fri Mar 7 18:37:56 EST 2008
David-Sarah Hopwood wrote:
> Sandro Magi wrote:
>> Interesting coincidence: I had just kicked off a debate on LTU that
>> referential transparency subsumes capability security . I'm curious
>> what people here think as well.
>>  http://lambda-the-ultimate.org/node/2706#comment-40510
> I agree with almost all of Peter van Roy's comments [*]. In particular,
> referential transparency does not imply capability security, because it
> does not imply encapsulation.
> Encapsulation is independent of state -- immutable data can be kept
> private by encapsulation. Consider, for example, a 'signer' object that
> holds a private key, and will cryptographically sign given data using
> that key (using a secure algorithm that is assumed not to leak key
> information). This object is referentially transparent, but whether it
> can keep the key secret depends on other attributes of the language;
> it isn't automatic that the key is kept secret because the object (or
> any term in the language) is referentially transparent.
Ah, the perils of imprecision and unstated assumptions. :-)
When speaking of referential transparency, I am of course speaking of it
in terms of programming languages, and the lambda calculus at a minimum.
A lambda is encapsulated.
In Section 9.1, footnote 1 of MarkM's thesis, he defines the
"object-capability security model" as:
Our object-capability model is essentially the untyped call-by-value
lambda calculus with
applicative-order local side effects [...]
Preserving referential transparency eliminates the dependency on
evaluation order, while preserving all of the language's other
properties that I can see. There might be a small hit to expressiveness
due to more tightly controlled side-effects, but I think this is largely
compensated for by the increased reasoning power over effects.
This exchange and the debate has been very illuminating!
More information about the cap-talk