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

[Toby Murray]

On Tue, 2008-05-20 at 22:14 +0200, Matej Kosik wrote:
> Hi 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).

You're right. Do I need to do this pervasively throughout the document
for all such names (e.g. Membrane, RMembrane, wrap, etc.)? Which part of
the text alerted you to this for $self$ ?


> Concerning CSP I have (wrongly?) deduced:
> 1. CCS [1] is not an object-capability language
>    (for example, I cannot describe powerboxes there)

CCS is not an object-capability language. This does not mean that you
cannot describe a powerbox in it though but to do so, you need to impose
certain restrictions on how it is used.

> 2. CSP and CCS are complementary
>    ([1], page 247 at the bottom: "CSP ... a theory which complements the one in this book.")

Controversial -- that's like saying that Haskell and Scheme are
complimentary ;)

CSP has some features that CCS does not:
 - denotational semantics rooted in the notion of refinement that are
congruent with its operational semantics -- refinement is very important
in CSP and is where much of its power comes from.
 - a model checker, FDR -- technically, FDR is a refinement checker but
refinement can be used to express all sorts of interesting properties
 - a test for process equivalence that is preserved under all contexts
(e.g. if P = P', then F(P) = F(P') for any CSP context F(_). This is not
the case for CCS's notion of equivalence (bisimulation). For example,
a.0 is bisimilar to tau.a.0, but a.0 + b.0 is not bisimilar to tau.a.0 +
b.0. This has to do with how CCS handles the + operator.)

CSP is also much less fashionable ;) 

I'm sure CCS has features that CSP does not as well, but despite my best
intentions, I'm yet to study it properly. Of course, I'm totally biased
here in my opinions regarding the two so keep that in mind when you read
this.

CCS does have the advantage of laying the foundations for much of the
current work in process calculi -- e.g. anything based on the pi
calculus which most of it seems to be. However, like ocap security, I
believe the ideas embodied in CSP have great power, despite their
limited visibility. CSP does have its shortcomings, but I think its
unique features have allowed it to live much longer than many expected.
My preferred process calculus would be some sort of polarised
pi-calculus with decent denotational semantics and a sound notion of
refinement. 

> 3. CSP is not an object-capability language

No. But it can be used to model object-capability systems. It's worth
debating the accuracy to which ocap systems can be approximated in CSP,
however. This paper gives a data point from which arguments can be
drawn. In particular, see the Conclusion section that discusses the
shortcomings of the approach.

> 
> I am sorry for the naive question :) .

Never be sorry for asking curious questions. Particularly when they're
so well phrased as to enable easy answering. I only hope my answers were
as intelligible as the questions to which they apply.

Cheers

Toby