[cap-talk] Announcing "Analysing Object-Capability Security" Paper and Authodox v. 0.2.0
kosik at fiit.stuba.sk
Wed May 21 03:33:32 CDT 2008
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:
>> and this:
>> 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:
you will see difference and new version will be typeset "correctly".
>> Concerning CSP I have (wrongly?) deduced:
>> 1. CCS  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
>> 2. CSP and CCS are complementary
>> (, 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...
More information about the cap-talk