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

[Sandro Magi]

I agree: it's important to enforce a clear and sensible semantics.
Abstraction violations, such as those identified by Kennedy, violate the
expected semantics of VM primitives and their operations (bool is not
two-valued, virtual calls bypass overridden methods, etc.).

I think a piecewise approach is practical however: the more conservative
goal of eliminating static state and controlling calls to static
authority-bearing methods permits isolation without the overhead of
process sanboxing. This would permit safe shared hosting and hosting
cloud-computing. At the moment, hosts must rely on coarse-grained
process isolation with inflexible stack-walking access control; witness
all the headaches associated with running programs under such "medium
trust" environments.

Certainly the shared hosting clients have few guarantees that the
libraries they link to are safe, but this is a whole new degree of
assurance. I think the more conservative goal would suffice in a number
of domains.

>From the Joe-E appendix, it certainly seems like the situation is dire
for the JVM, as a great deal of information appears to be lost in the
translation to bytecode. The CIL retains full type information, so I'm a
little more optimistic here, though I admit the bool violation mentioned
above was definitely surprising. Not sure how the CLR guys let that one
through.

Sandro

David Wagner wrote:
> 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!
> _______________________________________________
> cap-talk mailing list
> cap-talk at mail.eros-os.org
> http://www.eros-os.org/mailman/listinfo/cap-talk