In article <··············@crunch.ikp.physik.th-darmstadt.de> ···@crunch.ikp.physik.th-darmstadt.de (Thorsten Ohl) writes:
>
> In article <·················@best.best.com> ···@best.com (.) writes:
>
> Can you elaborate on the ``security story'' of the caml VM (or provide
> pointers to further information)?
In case nobody has answered yet, look at:
http://pauillac.inria.fr/~rouaix/mmm/
Its security story is based on "compile time check + authentication."
Compile time verification (type check etc.) can ensure certain type of
errors (e.g., type errors) cannot happen at runtime. Thanks to Caml
type/module system, one can ensure that correct caml program does not
cause runtime type error nor does access to insecure library routines.
The remaining issue is how to ensure that a binary (or bytecode) is
really verified by a compiler. i.e., binary/bytecode is not modified
AFTER compilation. They ensure this by putting a digital signature of
the compiler to binary/bytecode.
In this case, of course, the compiler must be trusted. If one
delivers the source code of the compiler and the malicious user
modifies the compiler so that he bypasses the type check of caml, the
malicious can still write insecure application. An alteanative, which
is also mentioned in their paper, is to put trusted compilers at
trusted hosts and let them do final delivery of an application.
I myself have never played with MMM, hence I don't know which approach
they currently take.
--
Kenjiro Taura
Yonezawa Laboratory, Department of Information Science
Tokyo University
···@is.s.u-tokyo.ac.jp