A paper by Greg Meredith, Mike Stay and Sophia Drossopoulou page Of note: - Meredith was the principal architect of Microsoft’s BizTalk. He is designer of Rholang - Mike Stay worked at Google during his PhD . On category theory he concluded a new type system is required for programming distributed systems. - Drossopoulou is a professor of CS at UCL. She builds on OCap i.e. capabilities-based-dom with Mark Miller.
Types of chess pieces, are beret policies in distributed board games (so we play on single board).
> We would like a way to declare the authority that an object ought to possess and then check whether the implementation matches the intent; that is, we would like a language for declaring security policy. Drossopoulou and Noble convincingly argue that none of the current specification methods adequately capture all of the capability policies required to support OCap systems. The most intriguing aspect of the capability policies proposed in 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). In contrast, classical Hoare Logic specifications describe sufficient conditions and are closed. In this paper we con- centrate on the use of the rho-calculus for ex- pressing deniability. To express necessary conditions, we invert the assertion and use bisimulation (e.g. any piece of code which does not have access to the ac- count 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.