[cap-talk] Wikipedia: Object-capability model
kosik at fiit.stuba.sk
Sat Jan 6 09:17:10 CST 2007
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
>> 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
> 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
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*.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 252 bytes
Desc: OpenPGP digital signature
Url : http://www.eros-os.org/pipermail/cap-talk/attachments/20070106/e8823f9f/attachment.bin
More information about the cap-talk