Policy as types

Greg Meredith, Sophia Drossopoulou, and I have written a paper that
grew out of discussions with Mark Miller and James Noble.

>From the introduction:

The most intriguing aspect of the capability policies proposed in [the
paper by Drossopoulou and Noble discussed here on e-lang recently] is
deniability.  Deniability differs from usual style of specifications
in the following two aspects: a) it describes policies which are open,
i.e. apply to a module as well as all its extensions, and b) describes
necessary conditions for some effect to take place. For example, a
policy may require that in order for any piece of code to modify the
balance of a bank account, it needs to have access to that account
(access to the account is a necessary condition), and that this
property is satisfied by all extensions of the account library
(open)...

To express necessary conditions, we invert the assertion and use
bisimulation (e.g. any piece of code which does not have access to the
account will be bisimilar to code in which the balance of the account
is not modified).  To express openness, we adapt the concept of the
adjoint to the separation operator, i.e. any further code P which is
attached to the current code will be bisimilar to P in parallel with
code which does not modify the balance of the account.

In short, we show that the RHO-calculus is an ocap language and sketch
a translation from a subset of JavaScript into the calculus; we also
demonstrate that the corresponding Hennessy-Milner logic suffices to
capture the key notion of deniability.

http://arxiv.org/abs/1307.7766
-- 
Mike Stay - [email protected]
http://www.cs.auckland.ac.nz/~mike
http://reperiendi.wordpress.com