[e-lang] Taming of Pict

[Matej Kosik]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Hi Toby,

Toby Murray wrote:
> Hi Matej,
> 
> Interesting stuff.
> 
> Some quick questions on Pict:
> 
>  - Pict channels are typed. Say one has a channel that is typed to carry
> values of type T. Can one declare this channel so that it is read-only
> (ie. can only be used to read values of type T) or write only (can only
> be used to write values of type T).

Yes. These
- - read-write
- - read-only
- - write-only
permissions are guarded by the typing system of the language. If you create a channel c as follows:

	new c : ^Int

you create new bound variable with name c that is bound to the fresh channel. Visibility of this
variable obeys normal statical-scoping rules.

The c variable can be used both
- - for sending an integer (value of type Int) to channel designated by c
- - for receiving an integer from channel designated by c

>  - If one has a read-write channel (can be read and written to), can one
> get a read-only capability to this channel, and another write-only
> capability to this same channel?

Yes. Pict supports discrimination between these different kind of permissions (1. to send as weel to
receive from a channel; 2. to send to a channel; 3. to receive from a channel) at typing level. Of
course they are separately defined in the Pict language definition. But the more general idea of it
is called:

	i/o types

and it is described here:

	Sangiorgi, Walker:  The Pi-Calculus: A Theory of Mobile Processes 	

(page 263). The Pict uses diffent syntax for denoting types but the meaning is the same.

	i T    (input capability) is written in Pict as ?T
	o T    (output capability) is written in Pict as !T
        # T    is written in Pict as ^T

(Sangiorgi and Walker indeed use the term `capability').

> Then one could hand the read-only
> capability to one module and the write-only capability to a second
> module, allowing the second to write values to the first, but not vice
> versa.

Yes, you can achieve your security goals analogously as you would achieve them in i/o-typed
pi-calculus. That is, with the help of subtyping.

> 
> 
> In the article you say:
> 
> "From the security point of view Pict is in principle as good as E."
> 
> I presume you mean Pict, like E, implements object-capability semantics
> (equivalently it implements the "rules of allowed reference graph
> dynamics" as you say in the paper). 

Yes. The goals was to show that the "rules of allowed reference graph dynamics" hold in all
"untrusted modules".

> 
> However, Pict could well be far more secure than E because the Pict
> implementation (compiler, basically) is likely far smaller than the E
> runtime.
> 
> I'd much rather run an OS kernel written in Tamed Pict than one written
> in E, simply because Pict is so much more compact -- hence the TCB that
> underpins Pict is much smaller than that which underpins E.

Pict compiler has 6568 lines. It co-forms TCB. But if you count JVM to the TCB of E-on-Java, then it
is fair to count `ocamlc', `gcc', `gas', `ld' `libc' that participate on creation of executable Pict
binary. Unless someone proves their correctness, they are not correct but trusted).

On the other hand, if you look at the notion of vat in E and servers in Minix, it is possible to
see, how perfect (in theory) E is for these kind of systems.

(there are other interesting connections:
 - OTP in Erlang vs. Minix's reincarnation server vs. strong typing and memory safety of Pict
)

I think, both options are interesting: using Pict and using E-on-Something for creating an OS
kernel. It might close A.Tannenbaum vs. L.Torvalds dispute (its various points). That is a hypotheses.

> 
> Perhaps more questions later as I keep reading.
> 
> Cheers
> 
> Toby
> 
> 
> On Thu, 2008-01-24 at 17:49 +0100, Matej Kosik wrote:
> Friends,
> 
> During the summer, I have posted a lightweight article about taming of Pict (turning Pict into a
> proper object-capability language) and to a nearby conference (SOFSEM).
> 
> (paper)
> http://altair.sk:60001/mediawiki/upload/d/de/Sofsem2008.pdf
> 
> (slides)
> http://altair.sk:60001/mediawiki/upload/6/65/Sofsem2008-presentation.beamer.pdf
> 
> (prepared talk)
> http://altair.sk:60001/mediawiki/upload/4/4b/Sofsem2008-presentation.article.pdf
> 
> The talk is already over. It did not go to detail about the language (there was not much time) but
> hopefully covered usefullness object-capabilities.
> 
> The open problem were not solved yet (related to possibilities of untrusted components to waste as
> much memory and as much CPU without proper bounds). As soon as I complete boring commercial Erlang
> project, I will try tackle that. I believe they are solvable. The question is only the price---how
> much will TCB grow and how much flexible mechanisms for constraining "memory consumption" and "CPU
> consumption" will be available.
> 
> Two people helped me:
> - Frank Piessens (as a shepherd helped me a lot with turning "conditionally accepted" paper to
> "accepted")
> - Norman Hardy (helped me filter out some errors I was not able to recognize)
> I am grateful to both of them.
> 

- --
mk
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.6 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iD8DBQFHqf+KL+CaXfJI/hgRAov1AJ9EwjXWo5BRqwMamyOGcf72vtRP+gCgmhea
EbpBK+N2U2YLKZlzGAkbt7g=
=n4TM
-----END PGP SIGNATURE-----