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

[Matej Kosik]

Hi Toby,

Toby Murray napísal:
> 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

Try to compare the typesettiing results of you original:

	$self$

and this:

	$\mathit{self}$

They are typeset differently and I think you want the latter version. The former version is
"broken". It is because TEX interprets it as a multiplication of variables `s', `e', `l' and `f'. In
the latter case TEX is instructed to typeset word `self' in italics (and it will employ proper
kerning rules).

--------------------------------------------------------------------------------

Concerning CSP I have (wrongly?) deduced:
1. CCS [1] is not an object-capability language
   (for example, I cannot describe powerboxes there)
2. CSP and CCS are complementary
   ([1], page 247 at the bottom: "CSP ... a theory which complements the one in this book.")
3. CSP is not an object-capability language

I am sorry for the naive question :) . Where did I made a mistake?

[1]
http://www.amazon.co.uk/Communication-Concurrency-Prentice-International-Computer/dp/0131150073/ref=sr_1_1?ie=UTF8&s=books&qid=1211312637&sr=1-1
-- 
Matej