[e-lang] An attack on a mint
David Wagner
daw at cs.berkeley.edu
Mon Mar 3 12:44:15 EST 2008
Mark Miller writes:
>However, because JavaScript doesn't have integers, I pulled the
>addition out into a separate statement to ensure it didn't loose
>precision.
Oh, gosh, so my fixing this correctly is more subtle than it appears.
Here was my proposed "fix":
deposit: function(amount,src) {
caja.enforceNat(amount);
var box = src.getDecr();
brand.unseal(box)(amount);
balance = caja.enforceNat(balance+amount);
}
There's a subtle detail here. If balance+amount overflows (i.e., exceeds
MAXINT, where MAXINT+1 is the smallest non-precisely-representable natural
number), then enforceNat() will throw an exception -- *after* src.balance
has been decremented but before this.balance has been incremented.
Thus this might look like it can violate conservation of currency.
Fortunately, I think this is not exploitable as long as the total amount
of money in circulation is representable in a natural number, and I
believe that assumption is enforced by the Mint. However this shows
that my fix has made the code less robust against integer overflow;
it happens to be safe, but the reasoning needed to show that requires
more subtle, non-local invariants.
I seem to recall discussing the integer overflow issue during the
Waterken review as we reviewed Tyler's Mint. His code was also safe,
for the same reason, but I think it took us a moment to work through
the chain of reasoning.
>The enforceNat function is
>
> /**
> * Enforces that <tt>specimen</tt> is a non-negative integer within
> * the range of exactly representable consecutive integers, in which
> * case <tt>specimen</tt> is returned.
> * <p>
> * "Nat" is short for "Natural number".
> */
> function enforceNat(specimen) {
> enforceType(specimen, 'number');
> if (Math.floor(specimen) !== specimen) {
> fail('Must be integral: ', specimen);
> }
> if (specimen < 0) {
> fail('Must not be negative: ', specimen);
> }
> // Could pre-compute precision limit, but probably not faster
> // enough to be worth it.
> if (Math.floor(specimen-1) !== specimen-1) {
> fail('Beyond precision limit: ', specimen);
> }
> if (Math.floor(specimen-1) >= specimen) {
> fail('Must not be infinite: ', specimen);
> }
> return specimen;
> }
Interesting. Does this suffice? One property we want to ensure is
that if
enforceNat(x);
enforceNat(y);
z = enforceNat(x+y);
succeeds, then as integers z is the sum of x and y. But what if x is
MAXINT, and y=1. Is it possible that x+1 rounds down to x? Similarly
is it possible that there exists some sum s such that x > MAXINT but
Math.floor(s-1) === s-1 < s? Are we guaranteed by properties of floating
point arithmetic that if x > MAXINT, then enforceNat() will throw an
exception? I just don't know floating point arithmetic well enough to
reason this through.
What about
enforceNat(x);
enforceNat(y);
z = enforceNat(x*y);
?
>I do remember a different plan interference vulnerability that both
>Tyler & I independently fell into in our respective implementations of
>the IOU Mint (in Waterken/Joe-E and E respectively). By aborting a
>plan with a thrown exception, an attacker could violate conservation
>of currency. This bug was fixed well before the Waterken security
>review. But it corroborates the suspicion that we may all be
>underestimating plan interference vulnerabilities.
This seems to be shaping up to make an interesting case study in
identifying several kinds of common hazards:
- exceptions can cause plan interference
- re-entrancy can cause plan interference
(or: calling untrusted code while object invariants are
temporarily broken can introduce security holes)
- integer overflow can violate expected invariants
- aliasing can violate expected invariants
More information about the e-lang
mailing list