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

[Mark Miller]

Hi Toby, congratulations! Looking forward to reading it. To make
online reading more pleasant, could you please add

\usepackage{hyperref}

regenerate the document and repost? Thanks.

On Tue, May 20, 2008 at 7:42 AM, Toby Murray
<toby.murray at comlab.ox.ac.uk> wrote:
> 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
> _______________________________________________
> cap-talk mailing list
> cap-talk at mail.eros-os.org
> http://www.eros-os.org/mailman/listinfo/cap-talk
>



-- 
Text by me above is hereby placed in the public domain

 Cheers,
 --MarkM