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

Faulty implementation of `MathMasters.sol::mulWadUp()` function produces incorrect result for certain input values

stefanlatinovic

Summary

The MathMasters.sol::mulWadUp() function may produce incorrect results for certain input values.

Vulnerability Details

The MathMasters.sol::mulWadUp() function contains a code segment that, if certain conditions are satisfied, modifies one of the input values (x) used in later calculations, which could result in an incorrect outcome.

The code is as follows:

if iszero(sub(div(add(z, x), y), 1)) { x := add(x, 1) }

Impact

The MathMasters.sol::mulWadUp() function will produce incorrect results for certain input values.

Proof of Concept (PoC)

We can verify this behavior by running the existing test testMulWadUpFuzz in MathMasters.t.sol.

Fuzz testing using Foundry

By increasing the number of fuzz runs for each fuzz test case, we can potentially obtain counterexamples for which this test will fail.

The foundry.toml configuration file can be modified to increase the number of fuzz runs for each fuzz test case:

[profile.default]
src = "src"
out = "out"
libs = ["lib"]
​
[fuzz]
-runs = 100
+runs = 1000000
# runs = 1000000 # Use this one for prod
max_test_rejects = 65536
seed = '0x1'
dictionary_weight = 40
include_storage = true
include_push_bytes = true
extra_output = ["storageLayout", "metadata"]
​
# See more config options https://github.com/foundry-rs/foundry/blob/master/crates/config/README.md#all-options

Run a test with forge test --mt testMulWadUpFuzz.

We should see an output similar to this in the terminal:

Running 1 test for test/MathMasters.t.sol:MathMastersTest
[FAIL. Reason: assertion failed; counterexample: calldata=0xfb6ea94f00000000000000000000000000000000000000000002bfc66f73219d55eb3274000000000000000000000000000000000000000000015fe337b990ceaaf5993b args=[3323484123583475243233908 [3.323e24], 1661742061791737621616955 [1.661e24]]] testMulWadUpFuzz(uint256,uint256) (runs: 3979, μ: 944, ~: 1189)
Test result: FAILED. 0 passed; 1 failed; 0 skipped; finished in 184.17ms

Formal verification testing using Halmos

We can also use Halmos, a symbolic testing tool, to execute the same test:

halmos --function testMulWadUpFuzz --solver-timeout-assertion 0

Halmos should find counterexamples for which this test fails. We should see an output similar to this in the terminal:

Running 1 tests for test/MathMasters.t.sol:MathMastersTest
Counterexample:
p_x_uint256 = 0x0000000000000000000000000000000100000003ae000000383e000000800214 (340282367212473342719134338885200380436)
p_y_uint256 = 0x00000000000000000000000000000000d01034837fffffffbd0a10977a23ed2d (276563564976801819313845769479676751149)

Tools Used

  • Manual review

  • Foundry

  • Halmos

Recommendations

It is recommended to remove the code segment that modifies the x parameter.

Recommended changes to MathMasters.sol::mulWadUp() function:

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))
}
}

We can create a tests to check inputs that both Foundry and Halmos identified as counterexamples while running the testMulWadUpFuzz test in MathMasters.t.sol.

Add the following tests in MathMasters.t.sol:

function test_MulWadUpCounterexampleFuzz() public {
uint256 x = 3323484123583475243233908;
uint256 y = 1661742061791737621616955;
​
uint256 result = MathMasters.mulWadUp(x, y);
uint256 expected = x * y == 0 ? 0 : (x * y - 1) / 1e18 + 1;
assertEq(result, expected);
}
function test_MulWadUpCounterexampleHalmos() public {
uint256 x = 340282367212473342719134338885200380436;
uint256 y = 276563564976801819313845769479676751149;
​
uint256 result = MathMasters.mulWadUp(x, y);
uint256 expected = x * y == 0 ? 0 : (x * y - 1) / 1e18 + 1;
assertEq(result, expected);
}

Run both tests with forge test --mt test_MulWadUpCounterexample.

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.