[cap-talk] Backwater: some small progress

[Matej Kosik]

Toby Murray wrote:
> On Sat, 2007-04-28 at 22:58 -0700, Mark S. Miller wrote:
>> I know that Fred, in his search for a good formalism for reasoning about 
>> authority, spent some time examining Pi Calculus before deciding to base SCOLL 
>> on take-grant systems. Also, Toby Murray's 
>> <http://web.comlab.ox.ac.uk/oucl/work/toby.murray/analysing_authority.pdf> 
> 
> Now see
> http://web.comlab.ox.ac.uk/oucl/work/toby.murray/papers/analysing_authority.pdf
> 
> I'll have to look into the pi-calculus semantics sometime to see how
> easily my work can be applied to Pict code. That would be a cool thing
> indeed. Backwater appears to be the perfect "real world" target domain
> for my work in the short term, since it's correspondence to a process
> algebra so so strong and it is being used to build "real world" stuff
> right now.

I use it to
- learn about security and
- learn about low level things
- as a generator of questions for which I do not have yet answers

> 
> Awesome work Matej, btw.

Benjamin Pierce and David Turner who designed Pict did excellent job. I am only a poor hacker.

> 
>> uses another process algebra, CSP, to reason about authority. (I have easily 
>> understood Occam and Orc, and I have briefly understood Pict, but I don't 
>> understand CSP. I'm not sure why some simple process algebras seem so much 
>> easier to understand than others.)
> 
> Feel free to send CSP questions my way and I'll try to answer as best I
> can. Bill Roscoe's definitive CSP book is also online at:
> http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/68b.pdf
> 
> The first couple chapters give a good guide to CSP overall.
> 

My knowledge about CCS (similar to CSP) and the pi-calculus are weak. The pi-calculus attracted me because it introduces what Milner calls "mobility" (the system's structure can change over time because channel names can be passed over channels). This is very natural thing and I cannot imagine not to be able to use it. Understanding how to do basic things in this calculus is also relatively simple. Making proofs about systems described this way is not at all easy.
-- 
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/20070430/87b89177/attachment.bin