First Flight #8: Math Master

Summary

The MathMasters::mulWadUp function should calculates the expression (x * y) / 1e18 and to round the result up. The function correctly check if there is a remainder and add 1 if it is necessary. But by some values for x and y the function increments x with 1 which leads to incorrect calculation and incorrect final result of z.

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.

There is a if statement in the function that increments the x value with 1. Maybe, the reason for doing that is the result to be rounded up, but this is incorrect.

Let's take a look to the if statement that increments the value of x: iszero(sub(div(add(z, x), y), 1)).

• add(z, x): This add z and x. But z is supposed to be the result from the MathMasters::mulWadUp function, it is not initialized and therefore its value is 0. So, this addition is useless.

• div(add(z, x), y): This divides the result of addition that is x by the value of y.

• sub(div(add(z, x), y), 1): This subtracts the result of division by 1.

• iszero(sub(div(add(z, x), y), 1)): This checks if the result after subtraction is 0. If it is 0, the if statement will be true and the x value will be incremented by 1.

When this result can be 0?

• If the values of x and y are equal.

• If the value of x is slightly greater than the value of y but not enough to make the division result reach 2 when rounded down to the nearest integer.

In theese cases the value of x will be incremented by 1. But this incremention leads to incorrect final result.
In the last line of the function is assigned the final result to the variable z: z := add(iszero(iszero(mod(mul(x, y), WAD))), div(mul(x, y), WAD)). Also, there is a check if the result of the expression (x * y) / WAD has a remainder. If there is a remainder, 1 is added to round up the result.

Impact

Let's consider the following scenario:

The values of x and y are both equal to 3e18. The following test function testMulWadUpCalculation calculates the expected solution and compares it to the solution retrieved from the MathMasters::mulWadUp function. You can add this test function in the MathMasters.t.sol file and execute it with the Foundry command: forge test --match-test "testMulWadUpCalculation"

Test fails:

The result from the MathMasters::mulWadUp function is 9000000000000000003 and the expected result is 9000000000000000000. This difference is because the incorrect incrementation of the value of x.

The following test in Halmos found also the case by which the value of x is slightly greater than the value of y but not enough to make the division result reach 2 when rounded down to the nearest integer. Halmos is a great tool for formal verification. To execute this test you should have Halmos installed and import the SymTest from lib/halmos-cheatcodes/src/SymTest.sol. Then you can use the command to execute the test function: halmos --function check_check_MulWadUp --solver-timeout-assertion 0.

The input arguments for the functions are of type uint128, because with the type uint256 the result was Killed.
So, the Halmos found the counterexample: x = 20901944742440337407 and y = 15364007485707028177. I stoped Halmos after the first found example because it took about 30 minutes. After that, I decided to compare the results from MathMasters::mulWadUp function and Solody::mulWadUp function. The following test demonstrates this, again with the help of Halmos:

This time the type of the input arguments is not changed and the result is:

All tests show that the function MathMasters::mulWadUp calculates the expression (x * y) / 1e18 incorrectly due to the unnecessary increment of x.

Tools Used

VS Code, Foundry, Halmos

Recommendations

Remove the if statement that increments the value of x.