[e-lang] An attack on a mint

[Mark Miller]

On Mon, Mar 3, 2008 at 9:44 AM, David Wagner <daw at cs.berkeley.edu> wrote:
> 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.

Sigh. Yes, this is probably why, when I "fixed" the += with the
enforceNat, I placed the enforceNat early, and so created the bug you
exploited.

This brings us back to what's so scary about all this: when writing
security code, even if you do write it correctly at first, the amount
of rationale that needs to be captured per line of code is much
greater than I can imagine being captured by any process people can
use. Without capturing this rationale, we need some other form of
cross-check to ensure that security isn't lost under maintenance -- as
I have done here for one of my own most beloved and well examined
examples.


>  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.

How? I understand how this is enforced by the IOU mint. I don't think
it is enforced by the simple-money mint.


>  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?

enforceNat doesn't round or coerce in any other way. If x+y isn't
already an integer in the appropriate range, enforceNat (I hope)
throws. If floating point works as I am counting on, then we should
have the property you state above. enforceNat(MAXINT + 1) should
throw. At least that's the intention. Needs testing on all JavaScript
platforms.


> 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.

I'm not sure I do either, but the properties you state are what I intend.


>  What about
>   enforceNat(x);
>   enforceNat(y);
>   z = enforceNat(x*y);
>
> ?

I never count on this property, but I believe it should hold as well.


>  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

Indeed! All this needs to be better understood and well explained.


-- 
Text by me above is hereby placed in the public domain

    Cheers,
    --MarkM