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

[Matej Kosik]

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

Yes. Elsewere wrong kerning is not that obvious but still if you put:
- Object
- Membrane
- RMembrane
- arg
- targets
- boolRet
- ...
inside

	\mathit{...}

you will see difference and new version will be typeset "correctly".

> 
> 
>> 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.

Can you give me an example written in CSP which would model the powerbox pattern?

That is, there are two processes: Host and Guest.
- the Guest can interact only with the Host
  (the Guest is "invited" to the system but does not have to be fully trusted)
- the Host can interact with the Guest and also with some other processes
How would you express these processes so that:
- the Host would choose some of its capabilities and send it to the Guest (in a way that noone else
can catch it---over some private channel or something analogous)
?

As it is expressed above it does not sound very exciting that scheme is very practical. I believe it
cannot be expressed in CCS and (unless CCS and CSP are significantly different in this aspect)
neither in CSP. Is that false? It would be a surprise for me so I would be interested to know that I
am wrong.

> 
>> 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.)

These are indeed interesting properties. I am adding this as a motivation to go through the CSP book...

[snip]

Best regards
-- 
Matej