First Flight #8: Math Master

Summary

The MathMasters::mulWadUp function should revert if the input parameters uint256 x and uint256 y do not satisfy the condition: y == 0 || x <= type(uint256).max / y. But the function does not revert as expected.

Vulnerability Details

The function MathMasters::mulWadUp accepts two input parameters (uint256 x and uint256 y) and calculates the expression x * y / 1e18 and rounds the result up. The function has check for input values which lead to overflow. In the comment of the function is written that it is required y to be 0 or x <= type(uint256).max / y. But the if statement that should check for this conditions does not check correctly:

Let's consider the if statement: mul(y, gt(x, or(div(not(0), y), x))):

• not(0): This computes the bitwise not of 0, which results in a value where all bits are set to 1. In the context of a uint256, this is equivalent to the maximum possible value for a uint256, which is 2^256 - 1.

• div(not(0), y): This calculates the maximum value that can be safely multiplied by y without causing an overflow.

• or(div(not(0), y), x): This performs a bitwise or between the result of div(not(0), y) and x.
  However, this doesn't make sense in the context of an overflow check, as the or operation here would not serve a purpose in preventing overflow.

• gt(x, or(div(not(0), y), x)): This will return 1 if x is greater than the result of a bitwise or operation and 0 otherwise.

• mul(y, gt(x, or(div(not(0), y), x))): The final operation will multiply y with the result of gt operation.

The described overflow check bypasses values for x and y which does not meet the requirement: x <= type(uint256).max / y and result in an overflow.

Impact

Let's consider the following scenario:
The value of the input parameter uint256 x is 2 and the value of the second input parameter uint256 y is 57896044618658097711785492504343953926634992332820282019728792003956564819968 which is 2^255.
The requirement: x <= type(uint256).max / y is not satisfied because type(uint256).max / y is 1 and x is 2. Therefore, the if statement in MathMasters::mulWadUp function should be true and the function should revert.
But the if statement returns false and the function continue with the calculations.

Let's consider again the if statement but this time with values for x and y:

• not(0) is equivalent to 2^256 - 1.

• div(not(0), y) divides the maximum uint256 value by y. If y is 2^255, this division results in 2.

• gt(x, or(div(not(0), y), x)) checks if x is greater than the result of the division. Since x is 2, it is not greater than 2, so the gt function returns 0.

• mul(y, gt(x, or(div(not(0), y), x))) multiplies y by the result of the gt function. Since gt returns 0, the multiplication result is 0, and the condition inside the if statement is false.

In that way the function will not revert as expected.

The following test function testMulWadUpFuzzOverflow in Foundry found the described scenario. You can add the test function to the file MathMasters.t.sol and execute it with the command: forge test --match-test "testMulWadUpFuzzOverflow"

At the end the result of the function MathMasters::mulWadUp with the provided arguments will be incorrect due to the overflow.

Tools Used

VS Code, Foundry

Recommendations

Change the condition in the if statement in the MathMasters::mulWadUp function to ensure that the values of x and y satisfy the condition: y == 0 || x <= type(uint256).max / y.