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

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