[cap-talk] Announcing "Analysing Object-Capability Security" Paper and Authodox v. 0.2.0

[Toby Murray]

Dear cap-talk,

A new paper "Analysing Object-Capability Security" has been accepted for
presentation/publication at FCS-ARSPA-WITS'08 (co-located with CSF
2008).

The abstract follows:

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.

---

For anyone who's interested, I'd love to get feedback on the paper
before the final version is submitted on June 1st. It's available here:
http://web.comlab.ox.ac.uk/people/toby.murray/papers/AOCS.pdf


The analysis presented in this paper was conducted using Authodox, a
small tool I've written to help ease the process of modelling systems of
interacting objects in CSP. I've put together a new release of Authodox,
version 0.2.0, to coincide with the paper. It's available here:
http://web.comlab.ox.ac.uk/people/toby.murray/tools/authodox/

Amongst other things, this release contains some example files that show
how the OCap patterns considered in the paper were modelled. (In order
to be brief, the paper considers a cut-down version of the analysis and
modelling represented in the example files.)

Again, comments, feedback, suggestions, bug reports and flames are well
very much welcome and encouraged.

Cheers

Toby