[e-lang] powerbox presentation
kosik at fiit.stuba.sk
Thu Nov 16 14:22:56 CST 2006
-----BEGIN PGP SIGNED MESSAGE-----
Mark S. Miller wrote:
> Matej Kosik wrote:
>> The security picture book by Marc Stiegler misses a slide about the
>> powerbox pattern (that is why I raised a ``simple question''
>> some time ago).
>> I quite enjoyed talking about it today to few other people and the
>> presentation is online.
> Hi Matej,
> These look great! One minor comment for now:
> I notice that everywhere you have to keep repeating
> Sorry for this annoyance. With the soon to be posted 0.8.37c and all future
> releases, all these should work fine with
> which should be less annoying.
I have made a note to update it when 0.9 will be available.
Since powerbox is a useful everywhere where it can be constructed, I
have added to the slides notes about powerbox in Pict. The same problem:
run foreign code obtained in a source form
and give it authority to print at most 20 characters
at the standard output.
is solved (according to me) in Pict. Although E and Pict are different
languages (each of them makes something else more convenient), they can,
I believe, mutually simulate themselves (as opposed to lambda-calculus
which is able to describe only algorithms whereas pi-calculus is able to
describe systems with have some behavior, interact with its environment,
can be composed together, do not necessarily terminate). I am not sure
how much work would that be and whether it would make sense to try it.
Pict is a language formed (by Benjamin C. Pierce) by
- - restricting the original pi-calculus
(there are only asynchronous sends (as opposed to
synchronous sends in the original pi-calculus).
Sends are asynchronous and unbuffered and there
is no ordering enforced)
+ enriching it with various convenient syntactic suggar
+ enriching it with various primitive processes
(integers are not encoded in the Church-like way
but exist as primitives. To the outsider, there is no
+ providing a whole bunch of useful library processes.
+ Pict compiler compiles Pict programs to native code
(via generating C code)
+ adding statical type-checking to the pi-calculus
(thus any well typed Pict program certainly has (some) sense)
The language is weird (everything is a process) but it is interesting.
The whole powerbox trick in Pict case is
- - not to link untrusted code with (unsafe) standard Pict library
- - reject code that contains `ccode' (it could be used for generating
arbitrary C code)
- - reject code that contains `import' (it could be used for importing
arbitrary Pict code wich could perhaps convey more authority than
we are willing to grant).
I haven't studied all the language features and available nechanisms in
complete detail so there might be things I missed and which could/should
be banned too but due to its nature, Pict could also be useful in
security (and concurrency) field. The fact that the semantics of the
whole language is precisely defined is also appealing. The ability to
compile to native code is unexpected bonus.
Of course, Pict is only a programming language and thus there are
limitations what can be done within it (no way to influence "scheduling"
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.3 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org
-----END PGP SIGNATURE-----
More information about the e-lang