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

[David Wagner]

Sandro Magi  wrote:
> Good links! Certainly the suitability of bytecode verification depends
> on the properties being verified. If one's goal is to merely ensure that
> static state is accessed immutably, and static authority-bearing methods
> are called only via a tamed API, I think this can be achieved by
> analyzing bytecode.
>
> Joe-E is slightly more ambitious, as its scope extends beyond merely taming.

I'm not persuaded that this is sufficient.

One goal of an object-capability language should be to enable two
mutually-distrusting components to interact and collaborate securely.
The failures of full abstraction can cause severe problems for that
goal, even if they don't break the security checks surrounding, e.g.,
static authority-bearing methods.

For instance, consider this code:

    public boolean static foo(byte b) {
        return b <= 127 && b >= -128;
    }

Suppose that malicious code is able to call foo().  What values
might be returned?

That's a trick question.  The answer is, it depends.  If malicious
code is constrained to be written in Java source code, the return
value will always be "true".  But if you allow malicious JVML bytecode,
it is possible to invoke foo() in a way that causes it to return
"false".  (Nope, you don't need to posit native methods or reflection
or any of that gunk.  Yes, the malicious JVML bytecode will be
accepted by the JVML bytecode verifier.)

This is a surprise that could create unpredictable security problems
for a Java programmer who writes her code to defend against malicious
clients written in Java, without realizing the crazy things that malicious
clients can do if they are written in bytecode.  (It's arguably realistic
to expect programmers to reason about what things a malicious client
can do within the language: programmers have to be familiar with the
language to write code in it, so they have some chance of reasoning about
what arbitrary code in that language can do.  But when you introduce
a language that programmers don't write in directly, like JVML, that
argument falls apart.)

Read the Joe-E spec, particularly the appendix, for more examples.
At first, when I started to learn about these issues, I think my initial
reaction was to think, how bad can this be?  Surely this is manageable.
But as the list started to grow, I eventually gave up any hope that
programmers could be expected to keep track of all the hazards introduced
by allowing malicious JVML bytecode.  I don't even know how we'd get
confidence that we have the complete list of such hazards, let alone
train programmers to watch out for them.

Is there a strong reason to work with arbitrary JVML bytecode instead
of Java source?  If there is, perhaps you could consider an architecture
that disassembles the JVML bytecode to Java source, verifies the source,
and then recompiles the source to bytecode; this may have issues, but
at least it bypasses the failures of full abstraction in JVML bytecode.