Compile-time division for signed integer edge case

[cyberthirst]

Submitted by Franfran._

Relevant GitHub Links

https://github.com/vyperlang/vyper/blob/3b310d5292c4d1448e673d7b3adb223f9353260e/vyper/ir/optimizer.py#L54-L55

https://github.com/vyperlang/vyper/assets/51274081/3f619c79-88e0-4d15-9ace-7d9ba02d16bc

Summary

At compile-time, division is using the same logic for both signed and unsigned integers. This is causing some corectness issues.

Vulnerability Details

Compile time div operation for both signed and unsigned are defined by evm_div

def evm_div(x, y):
    if y == 0:
        return 0
    # NOTE: should be same as: round_towards_zero(Decimal(x)/Decimal(y))
    sign = -1 if (x * y) < 0 else 1
    return sign * (abs(x) // abs(y))  # adapted from py-evm

But there should be an edge case according to the Ethereum yellow paper:

As you can see, DIV and SDIV are not purely equivalent. There is an edge case when $\mu[0] = -2^{255}$ and $\mu[1] = -1$. If we evaluate the expression with the Python engine, this is what we get for this function:

>>> def evm_div(x, y):
...     if y == 0:
...         return 0
...     # NOTE: should be same as: round_towards_zero(Decimal(x)/Decimal(y))
...     sign = -1 if (x * y) < 0 else 1
...     return sign * (abs(x) // abs(y))  # adapted from py-evm
...
>>> evm_div(-2**255, -1)
57896044618658097711785492504343953926634992332820282019728792003956564819968
>>> assert evm_div(-2**255, -1) == 2**255

It's 2**255, while it should be -2**255.

Impact

Here are some examples at looking how this could be exploited:

@external
def div_bug() -> int256:
    return -2**255 / -1

Doesn't work, caught by the type checker:

vyper.exceptions.InvalidType: Expected int256 but literal can only be cast as uint256.
  contract "src/div.vy:3", function "div_bug", line 3:11
       2 def div_bug() -> int256:
  ---> 3     return -2**255 / -1
  ------------------^
       4

While it should compile.

But we can for instance make it compile this way, while it should revert since as_wei_value does not support negative values.

@external
def div_bug() -> uint256:
    return as_wei_value(-2**255 / -1, "wei")

This compiles while the value should evaluate to a negative value, and returns 0x8000000000000000000000000000000000000000000000000000000000000000.

Another example:

@external
def div_bug() -> uint256:
    return max(-2**255 / -1, 0)

returns 0x8000000000000000000000000000000000000000000000000000000000000000 because max is evaluated at compile-time with the wrong computation of -2**255 / -1. The expected result should be 0.

@external
def div_bug() -> int256:
    return min(-2**255 / -1, 0)

returns 0

Other things that compile while it shouldn't:

@external
def div_bug() -> String[100]:
    return uint2str(-2**255 / -1)

@external
def div_bug() -> uint256:
    return uint256_addmod(-2**255 / -1, -2**255 / -1, -2**255 / -1)

@external
def div_bug() -> uint256:
    return uint256_mulmod(-2**255 / -1, -2**255 / -1, -2**255 / -1)

@external
def div_bug() -> uint256:
    return pow_mod256(-2**255 / -1, -2**255 / -1)

Tools Used

Manual review

Recommendations

def evm_div(x, y):
    if y == 0:
        return 0
	elif x == -2**255 and y == -1:
		return -2**255
    sign = -1 if (x / y) < 0 else 1
    return sign * abs(x // y)

(might be better to create a evm_sdiv to make sure that it won't cause any issue in the future)

[trocher]

I think that

@external
def div_bug() -> int256:
    return -2**255 / -1

not compiling is a feature and not a bug, in the same way, safe_div is reverting in those case: https://github.com/vyperlang/vyper/blob/e1adb7b3344c1ac03facfa553830a94dd7def2e2/vyper/codegen/arithmetic.py#L315

All other examples compiling are caused by issues with the old constant folding not doing proper type checking (https://github.com/vyperlang/vyper/issues/2830), none of them should compile in master from what I've tested.

An idea to have a better exception however would be to have something like that in FloorDiv._op():

if left == -2**255 and right == -1:
    raise OverflowException("Cannot divide min_value(int256) by -1", self)

[charles-cooper]

2**255 and -2**255 are the same on the evm.