Refinement-closed security properties allow the verification of systems for all possible implementations. Some systems, however, have refinements that do not represent possible implementations. In particular, real instantiations of abstract systems comprising security-critical components surrounded by maximally hostile unrefined components are often characterised only by compositions of refinements of the abstract system's components, rather than all refinements of the abstract system. In this case, refinement-closed security properties that examine multiple behaviours of a system at once can be falsely violated by the presence of inconsistent pairs of behaviour arising from different, incompatible refinements of the system's components.
We show how to weaken a class of such properties, which includes both information flow and causation properties, to allow them to be applied to these sorts of abstract systems. The weakened properties ignore all pairs of inconsistent behaviour that would have violated the original property from which they are derived. We also show how to adapt existing automated tests for these properties to allow them to be used to test for their weakened counterparts instead. This enables greater flexibility in the application of these sorts of properties to compositions of nondeterministic components.
", author = "Toby Murray and Gavin Lowe", booktitle = "Proceedings of the Eighth International Workshop on Automated Verification of Critical Systems (AVoCS '08)", doi = "10.1016/j.entcs.2009.08.017", number = "2", pages = "49-68", series = "Electronic Notes in Theoretical Computer Science", title = "On Refinement-Closed Security Properties and Nondeterministic Compositions", url = "http://web.comlab.ox.ac.uk/people/toby.murray/papers/nondet_compositions.pdf", volume = "250", year = "2009", } @inproceedings{murray08-fcsarspawits, abstract = "Much of the power and utility of modern computing arises in the different forms of cooperation that it enables. However, today this power comes with great risk because those engaged in cooperation are left vulnerable to one another. The Object-Capability (OCap) Model is a promising remedy, because it enables the creation of security-enforcing abstractions, or patterns, that can be composed with other code to build systems that enable cooperation whilst minimising vulnerability. Unfortunately, little work has been done to adequately formally analyse standard OCap patterns. In particular, their analysis requires frameworks that are capable of reasoning about their, often novel, security properties whilst taking into account the variation that exists across different OCap systems, particularly in concurrency semantics. We use the process algebra CSP to examine the implementations of a number of OCap patterns and their security properties in various kinds of OCap system. CSP allows us to not only reason about security properties beyond the reach of previous approaches, such as revocation, but also to consider different models of concurrency that various kinds of OCap system exhibit. We find that while some implementations function correctly when moved from one kind of system to another, others exhibit subtle differences or fail to preserve their security properties altogether.", author = "Toby Murray", booktitle = "Proceedings of the Joint Workshop on Foundations of Computer Security, Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (FCS-ARSPA-WITS'08)", title = "Analysing Object-Capability Security", url = "http://web.comlab.ox.ac.uk/people/toby.murray/papers/AOCS.pdf", year = "2008", } @article{article/Murray08, abstract = "We present a novel technique, known as the non-delegatable authority (NDA), for distributing authority to unconfined subjects in capability systems that prevents them from sharing the exact same authority that they have been given with anyone else. This feature is present in common systems based on access control lists (ACLs) in which one may hand out a permission without handing out the associated "grant" right, but has been thought to be impossible to express in capability systems until now. Consequently, we demonstrate that NDAs may be used to express ACL-like constructs and their basic pattern is directly applicable for implementing Multi-Level Security and identity-based access controls in the object-capability model. The extra complexity introduced by our NDA implementation can be hidden behind constructs that allow NDAs to be wielded as if they were ordinary capabilities to the target resource. These constructs cannot break the non-delegatability constraint and allow NDAs to be used effectively, although with less efficiency than delegatable authorities.", author = "Toby Murray and Duncan Grove", doi = "10.3233/JCS-2008-0314", journal = "Journal of Computer Security", number = "6", pages = "743-759", publisher = "IOS Press", title = "Non-Delegatable Authorities in Capability Systems", url = "http://www.comlab.ox.ac.uk/people/toby.murray/papers/NDA.pdf", volume = "16", year = "2008", } @inproceedings{inproc/Grove2007, abstract = "This paper describes the security and network architecture of the Annex system, a family of technologies for secure and pervasive communication and information processing that we have developed at the Australian Government's Defence Science and Technology Organisation. Our security architecture is built on top of a distributed object-capability system, which we believe provides an ideal platform for developing very high assurance devices. Our network architecture revolves around next generation networking technologies, including Mobile IPv6 and 802.11i wireless networking, but includes a small number of important extensions to improve security, robustness and mobility in the military context. A particular and unique contribution of our work is the tight integration of our very strong security architecture with next generation networking technologies. To complete the paper we describe our reference implementation of the Annex security and networking architecture, which consists of a number of devices known collectively as the Annex Ensemble.", author = "Duncan Grove and Toby Murray and Chris Owen and Chris North and Jeremy Jones and M.R. Beaumont and B.D. Hopkins", booktitle = "{Proceedings of the Twenty-Third Annual Computer Security Applications Conference (ACSAC'07)}", doi = "10.1109/ACSAC.2007.8", title = "An Overview of the Annex System", url = "http://web.comlab.ox.ac.uk/people/toby.murray/papers/AnnexOverviewACSAC07.pdf", year = "2007", } @inproceedings{inproc/Murray2007, abstract = "The rise of limited-privilege environments has been accompanied by the emergence of vulnerabilities in which a subject is able to maliciously wield their limited privileges to indirectly cause unwanted effects. Unfortunately, conventional safety analyses for access control systems are ill-equipped to deal with this problem because they do not detect the indirect effects that a subject can cause, but merely the permissions a subject can acquire. We present a technique that characterises a subject's authority as all of the effects they can cause to occur. Our technique is based on an analysis of causation, applied to a CSP model of a system. These analyses can be expressed as CSP refinements and, hence, automatically performed by a refinement-checker such as FDR. We demonstrate the ability of our technique to successfully identify excess authority by examining the 'Confused Deputy' scenario, whose vulnerability goes undetected with conventional safety analyses. ", author = "Toby Murray and Gavin Lowe", booktitle = "{Proceedings of Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCS-ARSPA'07)}", title = "Authority Analysis for Least Privilege Environments", url = "http://web.comlab.ox.ac.uk/oucl/work/gavin.lowe/Papers/analysing_authority.pdf", year = "2007", }