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

```MathMasters::sqrt``` fails for some ```x``` input values

kiteweb3

Summary

The MathMasters::sqrt function designed to calculate the square root of a given input using inline assembly exhibits unexpected behavior for specific inputs. Formal verification tests have identified several counterexamples where the function fails to return the correct square root.

Vulnerability Details

The logic in the assembly code is incorrect; the initial estimate for the Babylonian method is wrong.

/// @dev Returns the square root of `x`.
function sqrt(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))))
@> 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)))
​
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)))
​
z := sub(z, lt(div(x, z), z))
}
}

Impact

As described in the the MathMaster library Natspec the sqrt() function code is an optimized version of the Solmate sqrt() function. In my Poc, I will compare the Solmate sqrt() function with the sqrt() in the MathMaster library and I will prove that the sqrt() function in the the MathMaster library doesn't work as expected.

Looking at the two functions, it can be see the all the division happens in the "Babylonian method cycles" at the end, and that part of the function is identical between the two implementations. So we can can remove it to the test equivalence and speed up the test (differently it takes a lot of time).

Code Copy and paste the Sqrt.sol smart contract (it includes the 2 "modified" functions ```sqrtStripped``` and ```solmateSqrtStripped``` we are going to compare running Halmos).
// SPDX-License-Identifier: MIT
​
pragma solidity ^0.8.3;
​
contract Sqrt {
​
function sqrtStripped(uint256 x) public 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))))
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 solmateSqrtStripped(uint256 x) public pure returns (uint256 z) {
/// @solidity memory-safe-assembly
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)))
}
}
}
Test Copy and paste the MathCatcherTest.t.sol
//SPDX-License-Identifier: AGPL-3.0-only
pragma solidity ^0.8.3;
​
import {SymTest} from "../lib/halmos-cheatcodes/src/SymTest.sol";
import {Test, console2} from "forge-std/Test.sol";
import {Sqrt} from "../src/Sqrt.sol";
​
contract MathCatcherTest is Test, SymTest {
Sqrt c;
​
function setUp() public {
c = new Sqrt();
}
​
function check_sqrtEquivalence(uint256 x) public {
vm.assume(x > 0);
​
uint256 solmate = c.solmateSqrtStripped(x);
uint256 math = c.sqrtStripped(x);
​
assertEq(solmate, math);
}
​
Run: halmos --function check_sqrtEquivalence --solver-timeout-assertion 0
​
Logs:
Running 1 tests for test/MathCatcher.t.sol:MathCatcherTest
Counterexample:
p_x_uint256 = 0x0000000000000000000000000000000000ffff4b000000000000000000000000 (1329213655487500791058702628825333760)
Counterexample:
p_x_uint256 = 0x000000000000000000000000000000000000000000ffff87000000000000ffff (309482777765312149869101055)
Counterexample:
p_x_uint256 = 0x00000000000000000000000000000000000000000000000000ffffa100000000 (72057186016034816)
Counterexample:
p_x_uint256 = 0x000000000000000000ffff4a0000000000000000000000000000000000000000 (24519662660556227509402439363765392574390248575214813184)
Counterexample:
p_x_uint256 = 0x00ffffc600000000000000000000000000000000000000000000000000000000 (452311284906359693636216069503312092913256806645781945925927283521516208128)
Counterexample:
p_x_uint256 = 0x0000000000fffff1000000000000000000000000000000000000000000000000 (105312197512031155897706570146829084203898853865217444293793284096)
Counterexample:
p_x_uint256 = 0x00000000000000000000000000ffffe60000000000000000000000000000ffff (5708981923482299579833093830058187319557554175)
[FAIL] check_sqrtEquivalence(uint256) (paths: 48, time: 17.54s, bounds: [])

The test fails, these counterexamples represent values of x for which the function does not correctly compute the square root, due the incorrectness logic in the assembly code (the initial estimate for the Babylonian method is wrong).

This function is part of a library that can be used in smart contracts. Incorrect calculations in mathematical operations in smart contract can lead to vulnerabilities depending where is used this function (just for reference are listed some non exhaustive examples: allowing attackers to exploit for financial gain, wrong price calculation, wrong token distribution, or any form of financial decision-making).

Tools Used

Halmos

Recommendations

Use the sqrt solmate function as is.

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.