Re: MMM, a Web browser with applets in Caml Special Light

[Francois Rouaix <Francois.Rouaix@inria.fr>]

> Confirmation by the user sounds stupid to me. How is he supposed to know
> that the bytecode is correct ? I see a few alternatives:
> - somehow check the bytecodes (Java does it, but I have no idea if it's
>   doable with CSL's bytecodes)

Open problem. The idea here is "Keep It Simple and Stupid". CSL removes all
type information from the bytecode (except link information).
I'm not going to put it back to do type checking on the 
bytecode (assuming it is feasible at all).

> - transmit source rather than byte codes (since source code can be checked
>   easily)

Easily, easily. I would not bet on it. Besides, it would mean embedding the CSL
compiler inside the browser. Moreover, the point of distributing bytecode is
precisely not to transmit the source.

> - use authentication: the bytecode has to be signed by some trusted entity.
>   It would for instance be possible to provide a mail server that receives
>   CSL source, compiles it, and signs it with its private key: checking the
>   signature against the widely available publickey would prove that it is
>   really the output of an unmodified CSL compiler. This would probably require
>   the use of PGP3's API since forking a PGP for each execution sounds
>   awfully expensive to me (the advantage of having precompiled bytecode
>   would be less obvious)

I have the impression that I wrote about this all over the place in the
various MMM documents related to security, in particular:
<URL:http://pauillac.inria.fr/~rouaix/mmm/papers/mmm.ps.gz>
<URL:http://pauillac.inria.fr/~rouaix/mmm/manual/node4.html>

Please note that <http://pauillac.inria.fr/~rouaix/mmm/applets.html> is only
a very short introduction.

*Indeed*, I am advocating the use of trusted compilers.

Concerning the PGP3 API (for which I haven't seen public announces yet,
though I may not be watching the proper groups):
There is no need to authenticate the bytecode at each compilation during
the development. The applet author can trust his own bytecodes.
If it turns out to be a performance problem for a trusted compiler, then
yes, of course, the PGP3 API will be used.
For the browser itself, we need to fork PGP only once for each bytecode
received, so I don't think it is too much of an overhead.
There will be a legal problem if I attempt to distribute browser binaries
which include PGP code.


> I can deal with this. Providing threads would be a good idea anyway in CSL, tho.

Don't hold you breath, but threads are the latest goodie available for CSL,
and the very next thing to be integrated in MMM.

> But it should be possible to restrict the CPU and memory usage (and probably
> other aspects like network, file system, processes, etc...) of a thread.

Yes, I had the same idea. If you have more precise views on how this should be
made, feel free to share.

--
Francois.Rouaix@inria.fr                   Projet Cristal - INRIA Rocquencourt
WWW Home Page: http://pauillac.inria.fr/~rouaix/