An attack on a mint

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