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

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