Re: Another use for Guile/Scheme/Lisp

[Jim Blandy <jimb@red-bean.com>]

> One problem with scheme is that there is no way of protecting memory
> in the case of a type conversion bug. For example, if the user figures out
> a way of converting an integer to a pointer then anything in the interpreter
> image can be trashed (or modified to duplicate higher privileges).
> Theoretically this is impossible but bugs will happen. I guess it's better
> to fix the bugs than worry about what might happen if they were there...

People periodically propose operating systems based on safe languages;
Java is the latest craze.  The best objection (in my opinion) is the
one you raise here --- that users will often be able to leverage bugs
in the compiler or runtime into security holes.  The compiler, at
least, is a very complex piece of code, so it's quite plausible that
it would have bugs.

However, there's a good answer to that objection nowadays: proof-
carrying code.  The idea is to annotate assembly code (or machine
code) with enough information that a disinterested party can determine
that it will respect the type rules required by your run-time.  It's
like machine code with really gnarly typechecking.  Once you've
typechecked the code, you know that, assuming you invoke it according
to the ABI assumed by the types, it will behave itself.  The only
problem remaining is to make sure that the run-time is correct, but if
you require all coded loaded into the system to pass the test, then
you're home free.

The checker can be much smaller than the compiler --- George Necula's
checker is about three thousand lines of C code.  So you can have some
confidence that it's correct.  And it's also very fast.

Then, it's your compiler's job to generate these annotations and stick
them in the object file with the machine code.  If you're compiling a
safe language, like Scheme or Java, then the type rules of the
language tell you exactly what annotations to make.  But the point is,
the compiler isn't trusted any more --- it's just ordinary user code.

You can even load hand-crafted assembly code from arbitrary users and
have the system remain safe.  The author needs to write the types down
that show she's doing only legal operations, but once she's done that,
the system will happily load it.

It's subtle.  This isn't a complete explanation; I've never been able
to explain it without people believing that one could cheat the
checker, but believe me, you can't.

George Necula is The Man here:
http://www.cs.cmu.edu/~necula/papers.html#annotated