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

Use of Decimals in MathMasters::sqrt() instead of Hexadecimals representation results in nonequivalence leading to loss of precision.

808Nestor

Summary

Use of Decimals in MathMasters::sqrt() instead of Hexadecimals representation results in nonequivalence leading to loss of precision.

Vulnerability Details

The MathMasters imlementation is based on the equivalent soladay version. However, the MathMaster implementation uses decimals to represent the constants, while the soladay implementation uses hexadecimals. In Ethereum's Solidity programming language, hexadecimal notation (base-16) is commonly used for specifying literals and values, especially when working with low-level constructs like assembly. Hexadecimal notation is more aligned with the way data is represented in the Ethereum Virtual Machine (EVM). While you can use decimal literals in high-level Solidity code, when writing assembly code in Solidity, it's generally expected to use hexadecimal notation for representing values and memory locations. In short, the EVM is expecting to receive hexadecimal values and MathMaster sqrt function is submitting decimal values instead. This results in a loss of precision in the MathMasters implementation.

POC

Step 1: As a reference implementation refer to solady sqrt: https://github.com/Vectorized/solady/blob/8919f61d14a5e7b32f3d809c9f5fe3ea2ebcbc50/src/utils/FixedPointMathLib.sol#L615

Step 2: Notice that that bottom half of both sqrt implementations (MathMasters and Solady) are identical. Let's place the identical code in a helper function.

function _identicalCodeSqrt(uint256 x, uint256 z) public pure returns (uint256 ret) {
assembly {
z := shr(1, add(z, div(x, z)))
z := shr(1, add(z, div(x, z)))
z := shr(1, add(z, div(x, z)))
z := shr(1, add(z, div(x, z)))
z := shr(1, add(z, div(x, z)))
z := shr(1, add(z, div(x, z)))
z := shr(1, add(z, div(x, z)))
​
ret := sub(z, lt(div(x, z), z))
}
}

Step 3: We can then create versions of the two sqrt functions with calls to the identical code.

// The Solady sqrt function with the bottom half replaced with a call to the helper function for the identical code.
function sharedSoladySqrt(uint256 x) public pure returns (uint256 z) {
assembly {
z := 181
​
let r := shl(7, lt(0xffffffffffffffffffffffffffffffffff, x))
r := or(r, shl(6, lt(0xffffffffffffffffff, shr(r, x))))
r := or(r, shl(5, lt(0xffffffffff, shr(r, x))))
r := or(r, shl(4, lt(0xffffff, shr(r, x))))
z := shl(shr(1, r), z)
​
z := shr(18, mul(z, add(shr(r, x), 65536)))
}
z = _identicalCodeSqrt(x, z);
}
​
// The MathMaster sqrt function with the bottom half replaced with a call to the helper function for the identical code.
function sharedMathMastersSqrt(uint256 x) internal pure returns (uint256 z) {
/// @solidity memory-safe-assembly
assembly {
z := 181
​
let r := shl(7, lt(87112285931760246646623899502532662132735, x))
r := or(r, shl(6, lt(4722366482869645213695, shr(r, x))))
r := or(r, shl(5, lt(1099511627775, shr(r, x))))
// Correct: 16777215 0xffffff
r := or(r, shl(4, lt(16777002, shr(r, x))))
z := shl(shr(1, r), z)
​
z := shr(18, mul(z, add(shr(r, x), 65536))) // A `mul()` is saved from starting `z` at 181.
}
z = _identicalCodeSqrt(x, z);
}

Step 4: We can then conduct a fuzz test to confirm that the two modified sqrt functions along with the helper function are still working correctly.

// Fuzz test to check that output for both sqrt functions with a shared helper function containing duplicate code appears to be correct.
function test_fuzz_sharedSqrtFunctions(uint32 fuzzedSolution, uint32 fuzzedRandomNum) public {
// ARRANGE: specify input conditions
uint256 solution = fuzzedSolution;
vm.assume(solution > 0);
uint256 randomNum = fuzzedRandomNum;
uint256 squaredPlusRemainder = solution * solution + (randomNum % solution);
​
// ACT: call target contracts
uint256 mathMastersOuput = Base_Test.sharedMathMastersSqrt(squaredPlusRemainder);
uint256 soladyOutput = Base_Test.sharedSoladySqrt(squaredPlusRemainder);
​
// ASSERT: check output states
assertEq(solution, mathMastersOuput);
assertEq(solution, soladyOutput);
}

Step 5: Once we've verified that the adjusted square root functions are functioning as intended, we can disregard the duplicated code and focus on testing the essential differences in the remaining code for equivalence. To begin, let's create the two square root functions, each containing only their core code.

// The core Solady function, without the identical code.
function coreSoladySqrt(uint256 x) public pure returns (uint256 z) {
assembly {
z := 181
​
let r := shl(7, lt(0xffffffffffffffffffffffffffffffffff, x))
r := or(r, shl(6, lt(0xffffffffffffffffff, shr(r, x))))
r := or(r, shl(5, lt(0xffffffffff, shr(r, x))))
r := or(r, shl(4, lt(0xffffff, shr(r, x))))
z := shl(shr(1, r), z)
​
z := shr(18, mul(z, add(shr(r, x), 65536)))
}
}
​
// The core MathMaster function, without the identical code.
function coreMathMasterSqrt(uint256 x) internal pure returns (uint256 z) {
/// @solidity memory-safe-assembly
assembly {
z := 181
​
// This segment is to get a reasonable initial estimate for the Babylonian method. With a bad
// start, the correct # of bits increases ~linearly each iteration instead of ~quadratically.
let r := shl(7, lt(87112285931760246646623899502532662132735, x))
r := or(r, shl(6, lt(4722366482869645213695, shr(r, x))))
r := or(r, shl(5, lt(1099511627775, shr(r, x))))
// Correct: 16777215 0xffffff
r := or(r, shl(4, lt(16777002, shr(r, x))))
z := shl(shr(1, r), z)
​
// There is no overflow risk here since `y < 2**136` after the first branch above.
z := shr(18, mul(z, add(shr(r, x), 65536))) // A `mul()` is saved from starting `z` at 181.
}
}

Step 6: We can now test the two core sqrt functions for equivalence using Halmos.

// halmos returns and error "counterexample-unknown". So we disble the timeout limit for the assertion; thus giving Halmos more time to find a counterexample.
/// @custom:halmos --solver-timeout-assertion 0
​
function check_coreSqrtFunctions() public {
// ARRANGE: specify input conditions
uint256 x = svm.createUint256("x");
​
// ACT: call target contracts
uint256 coreMathMastersOuput = Base_Test.coreMathMasterSqrt(x);
uint256 coreSoladyOutput = Base_Test.coreSoladySqrt(x);
​
// ASSERT: check output states
assertEq(coreMathMastersOuput, coreSoladyOutput);
}

Step 7: Having received a counter example from Halmos, let's test it using Foundry's Forge tool. Run it using "forge test --match-test test_poc_sqrt -vv"

function test_poc_sqrt() public {
// ARRANGE: specify input conditions
uint256 x = 105311293498665291426722909308999732236070323463302251608708546560;
​
// ACT: call target contracts
uint256 mathMastersOuput = Base_Test.coreMathMasterSqrt(x);
uint256 soladyOutput = Base_Test.coreSoladySqrt(x);
console.log("mathMastersOuput: ", mathMastersOuput);
console.log("soladyOutput: ", soladyOutput);
​
// ASSERT: check output states
assertEq(mathMastersOuput, soladyOutput);
}

Impact

The loss of precision can lead to incorrect results when using the MathMasters implementation.

Tools Used

  • Foundry Forge: Fuzz Testing for Correctness

  • Halmos: Formal Verification Testing for Equivalence

Recommendations

Use hexadecimals to represent the constants in the MathMasters implementation.

- let r := shl(7, lt(87112285931760246646623899502532662132735, x))
- r := or(r, shl(6, lt(4722366482869645213695, shr(r, x))))
- r := or(r, shl(5, lt(1099511627775, shr(r, x))))
- r := or(r, shl(4, lt(16777002, shr(r, x))))
​
+ let r := shl(7, lt(0xffffffffffffffffffffffffffffffffff, x))
+ r := or(r, shl(6, lt(0xffffffffffffffffff, shr(r, x))))
+ r := or(r, shl(5, lt(0xffffffffff, shr(r, x))))
+ r := or(r, shl(4, lt(0xffffff, shr(r, x))))
Updates

Lead Judging Commences

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

Sqrt yields incorrect results for certain inputs because 16777002 doesn't represent the maximum value resulting from a right shift

Support

FAQs

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