[e-lang] A broken brand?

David Wagner daw at cs.berkeley.edu
Tue Mar 4 19:49:52 EST 2008

Mark Miller writes:
>Type checking would indeed have prevented the attack (at some loss of
>expressiveness that would typically have been fine).
>However, what I meant by my initial reaction is that type checking
>wouldn't have helped *detect* the bug.

I'm not sure whether this is correct, but let's assume it is:

This is why we emphasize writing code that is verifiably correct,
rather than taking some existing code where it's not obvious whether
the legacy code is correct and trying to exhaustively find and remove
all bugs from it.

I think type-checking is a plausible defense if you assume that it is
used when the code is initially implemented (not as an after-the-fact
activity).  If the code doesn't type-check, then maybe the programmer
should try to restructure it so it does.  This is like saying that if the
code isn't obviously correct, the programmer should try to restructure
the code until it is.

>I don't see a way to have
>employed a type system so that MarcS pattern with the bug fails to
>type check but without the bug passes the type check.

I don't understand this distinction.  Suppose that unseal() used a guard
to check that its box argument is of type Box, where Box is a trusted
type defined by Brand that cannot be subclassed.  Then we'd know that we
can rely upon the behavior of the call to box(): that invocation cannot
trigger the execution of untrusted code.  Unless I've missed something, it
seems like this would suffice to render the code safe against my attack.

Of course, types alone are not sufficient to render the Mint secure,
because the Mint was also vulnerable to unexpected aliasing between its
argument and its "this".

>David, would MOPS have helped?

Nope.  I think the brand bug would be hard to catch using any of the
standard mechanisms that I can think of.

I think it's possible that the Mint bugs could potentially be detected
by software verification tools like Spec# and JML.  You'd write down
a specification in terms of a set of object invariants and method
preconditions/postconditions.  One postcondition of deposit() might be
    this.getBalance() + src.getBalance() ==
      \old(this.getBalance() + src.getBalance())
where \old(e) represents the value of the expression e evaluated before
executing the method (i.e., in the pre-state rather than the
post-state).  A stronger postcondition might be
    this.getBalance() == \old(this.getBalance() + amount) &&
    src.getBalance() == \old(src.getBalance() - amount)
If the formal verification tool was sound, it ought to warn that these
postconditions could not be established.

Unfortunately, the JML tools are not sound.  One major soundness hole
is the treatment of temporarily broken object invariants: we normally
assume that the object invariant holds before every method is executed
and check that the object invariant is restored once the method returns.
Suppose method o.m() calls some other methods in the middle of
execution.  The object o might be in a temporarily inconsistent state
at that point (i.e., some object invariants of o might be false).  I
believe the JML tools allow this, because it's a very common idiom.
However if those other methods call o.n(), then n() might be invoked
on an object o whose object invariants are invalid -- contradicting the
assumptions mentioned above.  Note that this is exactly the plan
interference hazard.

Spec# has developed a special methodology to try to reason about this
kind of thing.  I don't know how successful it is, and I have yet to
fully wrap my mind around it.

As a result, I'm not convinced that the JML tools would detect my
fake-purse attack on the Mint, but Spec# might.  I would expect either
suite of tools to detect the unexpected-aliasing attack on the Mint.

But I don't think the JML/Spec# tools would detect the attack on the
brand, because the attack on the brand involved a violation of a
confidentiality property, and I can't see how to write down any
plausible spec in their invariant/precondition/postcondition language
that would have been violated by this confidentiality breach.

It would be an interesting case study to try applying those tools to
versions of the Mint and the brand and see whether they do or do not
indeed detect these (and other) attacks, given appropriate formal
specifications.  I'm speculating wildly here, so I could be way off base.

More information about the e-lang mailing list