[cap-talk] Security and Full Abstraction (was: Cap OS question)

[David Wagner]

Sandro Magi  wrote:
> Indeed I will. Still, from the examples in Kennedy's paper on the CLR, I
> don't see why the arguably illegal instruction sequences couldn't be
> outlawed based on a static analysis, or rewritten into a correct form
> (for the bool-byte conflation).

The wrong way to do it would be to take every attack you can think
of, then devise a static analysis to ensure the program doesn't do
that.  The reason that's the wrong way is it is a blacklist: you'll
never have confidence you thought of everything.

A better goal would be to try to come up with a static analysis to
check that the JVML bytecodes could have been produced from some valid
Java source code.  In other words, check the full abstraction property.
I don't really know how to do that in a simple and clean way.  (Complex
methods scare me, because how do you know you got them right?)  The only
approach I've been able to come up with that seems plausible it might
work is to decompile JVML to Java source, then verify the Java source,
then compile the source down to JVML, then execute the result.  That's
a bit hack-ish and might have some issues.

I don't rule out the possibility of some kind of static analysis on the
bytecode, or some bytecode transformation, to deal with these issues.
I just don't see how to do it, myself.  Maybe you'll have some ideas
about how to do it, and if so, great!