Analysing Object−Capability Security

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.