First Flight #8: Math Master
First Flight #8
Beginner FriendlyFoundry
100 EXP
View results
Previous Next
Submission Details
Severity: high
Valid

`MathMasters::mulWadUp` function outputs incorrect result for certain `x` and `y` values

0xloscar01

Summary

The MathMasters::mulWadUp function will not output a correct result for all possible x and y values due to a conditional statement that increments x by 1 when (x + z / y) - 1 = 0

https://github.com/Cyfrin/2024-01-math-master/blob/main/src/MathMasters.sol#L48-L59

​
function mulWadUp(uint256 x, uint256 y) internal pure returns (uint256 z) {
/// @solidity memory-safe-assembly
assembly {
// Equivalent to `require(y == 0 || x <= type(uint256).max / y)`.
if mul(y, gt(x, or(div(not(0), y), x))) {
mstore(0x40, 0xbac65e5b) // `MathMasters__MulWadFailed()`.
revert(0x1c, 0x04)
}
@> if iszero(sub(div(add(z, x), y), 1)) { x := add(x, 1) }
z := add(iszero(iszero(mod(mul(x, y), WAD))), div(mul(x, y), WAD))
}
}
​

Vulnerability Details

POC 1:

Halmos is required to reproduce the test case.

  1. Add the test to the MathMasters.t.sol file.

  2. Run the following command in the terminal: halmos --function formal_testMulWadUp --solver-timeout-assertion 0

​
function formal_testMulWadUp(uint64 x, uint64 y) public {
// Ignore cases where x * y overflows.
unchecked {
if (x != 0 && (x * y) / x != y) return;
}
assertEq(MathMasters.mulWadUp(x, y), x * y == 0 ? 0 : (x * y - 1) / 1e18 + 1);
}
​

Logs - POC 1:

​
Running 1 tests for test/MathMasters.t.sol:MathMastersTest
Counterexample:
p_x_uint64 = 0x0000000000000000000000000000000000000000000000000000000123e895ff (4897412607)
p_y_uint64 = 0x00000000000000000000000000000000000000000000000000000000db124ee5 (3675410149)
[FAIL] formal_testMulWadUp(uint64,uint64) (paths: 27, time: 85.98s, bounds: [])
Symbolic test result: 0 passed; 1 failed; time: 86.09s
​

POC 2:

To reproduce the test case, add the following test to the MathMasters.t.sol file and run forge test --mt test_RevertsMulWadUp -vvvv in the terminal:

​
function test_RevertsMulWadUp() public {
assertEq(MathMasters.mulWadUp(100e18, 100e18), 100e20);
}
​

Logs - POC 2:

​
Logs:
Error: a == b not satisfied [uint]
Left: 10000000000000000000100
Right: 10000000000000000000000
​

Impact

The MathMasters::mulWadUp function won't output the proper result for x and y values such that x / y = 1 and x >= 1e9 && y >= 1e9.

Tools Used

Halmos formal verification.

Recommendations

​
function mulWadUp(uint256 x, uint256 y) internal pure returns (uint256 z) {
/// @solidity memory-safe-assembly
assembly {
// Equivalent to `require(y == 0 || x <= type(uint256).max / y)`.
if mul(y, gt(x, or(div(not(0), y), x))) {
mstore(0x40, 0xbac65e5b) // `MathMasters__MulWadFailed()`.
revert(0x1c, 0x04)
}
- if iszero(sub(div(add(z, x), y), 1)) { x := add(x, 1) }
z := add(iszero(iszero(mod(mul(x, y), WAD))), div(mul(x, y), WAD))
}
}
​
Updates

Lead Judging Commences

inallhonesty Lead Judge over 1 year ago
Submission Judgement Published
Validated
Assigned finding tags:

`mulWadUp` has an unnecessary line that makes the result wrong for some inputs

Support

FAQs

Can't find an answer? Chat with us on Discord, Twitter or Linkedin.