Matthew Collinson and Kevin McDonald

Abstract

We describe a uniform logical framework, based on a bunched logic that combines classical additives and very weak multiplicatives, for reasoning compositionally about access control policy models. We show how our approach takes account of the underlying system architecture, and so provides a way to identify and reason about how vulnerabilities may arise (and be removed) as a result of the architecture of the system. We consider, using frame rules, how local properties of access control policies are maintained as the system architecture evolves.

Date: June 12, 2015
Published: http://logcom.oxfordjournals.org/content/early/2015/06/12/logcom.exv020.abstract
Publisher: Oxford University Press
Publisher URL: http://logcom.oxfordjournals.org/content/early/2015/06/12/logcom.exv020.abstract
Full Text: http://logcom.oxfordjournals.org/content/early/2015/06/12/logcom.exv020.full.pdf+html
DOI: http://dx.doi.org/10.1093/logcom/exv020
Open Access: http://discovery.ucl.ac.uk/1464201/

Categories: Publications