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

sqrt function does not pass symbolic verification

kiqo

Summary

Performing symbolic execution in the MathMasters::sqrt function and solmateSqrt results in different outcomes.

Vulnerability Details

Using Helmos we can determine that comparing sqrt calculation of MathMasters and Solmate fails in formal verification.

POC

Add the following contract to the MathMasters.t.sol file, which contains the differing parts of the square root calculation of MathMasters and SolMate

contract sqrTest {
function mathMastersSqrt(uint256 x) public pure returns (uint256 z) {
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))))
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)))
}
}
​
function solmateSqrt(uint256 x) public pure returns (uint256 z) {
assembly {
let y := x
z := 181
if iszero(lt(y, 0x10000000000000000000000000000000000)) {
y := shr(128, y)
z := shl(64, z)
}
if iszero(lt(y, 0x1000000000000000000)) {
y := shr(64, y)
z := shl(32, z)
}
if iszero(lt(y, 0x10000000000)) {
y := shr(32, y)
z := shl(16, z)
}
if iszero(lt(y, 0x1000000)) {
y := shr(16, y)
z := shl(8, z)
}
z := shr(18, mul(z, add(y, 65536)))
}
}
}
​

And add the following function to MathMasters.t.sol::MathMastersTest

/// @custom:halmos --solver-timeout-assertion 0
function testSqrtEquivalence(uint256 x) public {
sqrTest t = new sqrTest();
uint256 solmate = t.solmateSqrt(x);
uint256 mathMasters = t.mathMastersSqrt(x);
assertEq(solmate, mathMasters);
}

Then run the following command:
halmos --function testSqrtEquivalence

Impact

The calculation result leads to a different result.

Tools Used

Foundry and Halmos.

Recommendations

Make the following change in MathMasters::sqrt:

- r := or(r, shl(4, lt(16777002, shr(r, x))))
+ r := or(r, shl(4, lt(16777215, 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

AcT3R Auditor
over 1 year ago
inallhonesty Lead Judge
over 1 year ago

Support

FAQs

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