Re: [Caja] Important new paper: The Need for Capability Policiies

Tangentially related:

I once wrote an article "Why programming
languages?<http://soft.vub.ac.be/~tvcutsem/invokedynamic/node/11>"
where I make the point that a language designer, unlike a library designer,
has the ability to define a language as a little universe with "physical
laws" by which all programs written in that language must abide. The
opening sentence I used was: "no amount of library code is going to turn C
into a memory-safe language. Just so, no amount of library code is going to
turn Java into a thread-safe language."

To me, these properties feel closely related to the "deny" properties that
Sophia and James point out. In fact, a fruitful line of related work might
be tools that aim to prove certain safety and liveness properties such as
data race and deadlock freedom for programs written in a language with
shared mutable state (such as Java). These properties, like ocap security,
depend on *all code* in the system to play by the rules.

Regards,
Tom



2013/7/18 Mark S. Miller <[email protected]>

> Shriram, I appreciate the distinction you point out, but it does not fit
> with my sense of the meaning of "policy". Policies need to be expressed,
> understood, and enforced. To be enforced, there needs to be some mechanism
> that brings about the enforcement. Does this mechanism succeed at enforcing
> the stated policy? How should we verify this? This question seems
> independent of whether the code we're verifying is the code which also
> implements the functionality, or is separate from that code. Sophia's
> formulation would seem to apply equally well to both scenarios.
>
> Many policies of interest cannot be enforced separately from the code
> implementing the functionality -- which I think echoes what Ben was saying.
> Hence the subtitle of <http://www.erights.org/talks/no-sep/> is "Why
> security is not a separable concern". (This expanded into Part 4 of my
> thesis, but I unwisely dropped the subtitle at that time. I've always
> missed it.)
>
> Shriram, this is the second message from you where I saw only the replies.
> I also don't see your messages in the e-lang archive. Do you know why we're
> missing these?
>
>
>
>
>
> On Wed, Jul 17, 2013 at 1:49 PM, Drossopoulou, Sophia <
> s.drossopoulou-AQ/[email protected]> wrote:
>
>>  Hi Shriram,
>>
>>  Thank you for clarifying the terminology.
>>
>>   Sophia Drossopoulou asked about a distinction I introduced in my
>> message. To repeat it -- and I should be clear that I don't think
>> there is any standard terminology here -- I want to make a distinction
>> between "statements about programs that are automatically enforced by
>> the implementation mechanism" and "statements about programs that need
>> to be checked for by some external mechanism". I use the terms
>> "policy" for the former and "property" for the latter. Properties are
>> the things that verification engines have consumed for ages, and the
>> properties I saw in the very nice Drossopoulou/Noble paper struck me,
>> ultimately, are not much different from a variety of properties that
>> have been written down about programs down the ages. (Short answer to
>> Sophia's question: Yes.)
>>
>>
>>  Indeed, with the terminology suggested by Shriram Krishnamurthi, what
>> James Noble and I are looking for is "properties".
>>
>>  However, I believe that expressing policies through program properties
>> leads to properties which are somewhat different from those usually written
>> down about programs,  because a) they are "open|, and b) they have "deny"
>> elements. "Open" means that these properties need to be maintained by the
>> code as well as any extension of that code, and "deny" elements are
>> properties of the code itself rather than of the effects of the code.
>> Policy Pol_2 from the paper has such deny elements.
>>
>>  In a sun strand of this discussion, together with Greg Meredith, Mike
>> Stay, Mark Miller and James Noble, we discussed more the shape of
>> formalisation of  such properties, and we came up with the following
>> proposal:
>>
>>   a module P satisfies Policy(E,A)                 ****
>>             iff****
>>  for all modules Q, and code CD:
>>            if we execute code CD in the presence of P augmented with Q,
>>  and observe effect E, then the code CD has property A.
>>
>>  Cheers,
>>
>>  Sophia
>>
>> _______________________________________________
>> e-lang mailing list
>> [email protected]
>> http://www.eros-os.org/mailman/listinfo/e-lang
>>
>>
>
>
> --
>     Cheers,
>     --MarkM
>
> _______________________________________________
> e-lang mailing list
> [email protected]
> http://www.eros-os.org/mailman/listinfo/e-lang
>
>

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