[cap-talk] Wikipedia: Object-capability model

[Matej Kosik]

Jonathan S. Shapiro wrote:
> On Sat, 2007-01-06 at 11:01 +0100, Matej Kosik wrote:
>> Did anyone look at polarized pi-calculus?
>> (mentioned for example here
>>  http://citeseer.ist.psu.edu/130749.html
>>  but there might be better explanations elsewhere
>> )
>>
>> It is normal pi-calculus modified to distinguish between the `positive
>> channel names' (which can be used for receiving messages) and `negative
>> channel names' (which can be used for transmitting messages). I haven't
>> seen simpler capability secure model (of describing behavior). But there
>> are no objects. Only processes. But that is enough because everything
>> else (objects also) can be modeled via mobile processes and channels. I
>> would bet on it.
>>
>> It is formalized (so that there is no ambiguity in terms). Was
>> object-capability model also formalized in such precise way?
> 
> Yes. See:
> 
>   Verifying the EROS Confinement Mechanism
>   http://www.eros-os.org/papers/oakland2000.ps
> 
> However, the relationship to Pi Calculus had not occurred to me, so I
> want to look at the polarized pi calculus more closely. Thank you for
> bringing this to my attention.

I haven't yet studied EROS papers. My immature guess what you tried to
do there (proving that a given sub-system does not leak a given
capability) is suspiciously similar to the "does not leak" or "security"
property defined in
http://www.amazon.co.uk/Pi-Calculus-Theory-Mobile-Processes/dp/0521543274/sr=8-1/qid=1168096196/ref=sr_1_1/203-8113942-1334354?ie=UTF8&s=books
where they provide a type system to check that property at compile time.
   It can be checked effectively. I am not yet that far in reading, so I
only believe it rather than understand it. It is *tough*.
-- 
Matej Kosik

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 252 bytes
Desc: OpenPGP digital signature
Url : http://www.eros-os.org/pipermail/cap-talk/attachments/20070106/e8823f9f/attachment.bin