Uniswap v3: A Fuzzing Review

Uniswap v3

Uniswap, one of the most popular DEXes in the Ethereum ecosystem, introduced the innovative idea of concentrated liquidity via ticks ranges in their third version, allowing for greater capital efficiency. This efficiency however came at the cost of increased complexity in their codebase, requiring the implementation of custom math libraries and other contracts for supporting functionality. This increased complexity meant a greater need for testing to ensure all of their contracts functioned as expected.

In a review of their codebase, Trail of Bits determined that Uniswap's test suite was extensive, including unit as well as fuzz tests for their Echidna fuzzer. Even so, there was still unexpected behavior that was uncovered by the Trail of Bits team when they expanded this Echidna test suite to include more properties.

One of these vulnerabilities discovered with Echidna will be the focus of this post to demonstrate how defining properties with such tools can uncover edge cases that would be practically impossible for someone to find with purely manual methods or unit testing alone. 

The Vulnerability 

Because of the introduction of tick-concentrated liquidity, Uniswap V3 required the implementation of new TickMath and SqrtPriceMath libraries for performing operations related to ticks and their corresponding prices. One of these operations is getNextSqrtPriceFromInput/getNextSqrtPriceFromOutput which as their names suggest return the next square root price after adding or removing a given amount of tokens in a swap, respectively. The sqrtQX96 price that each of these returns is used in the swap flow for determining what the price of the swapped asset in the pool will be after the swap. This takes into account the amount of liquidity provided at the given tick and how much the price needs to be moved to provide the desired amount of output tokens to the swapper. This is then used to determine the current tick that gets set in the Pool's state by a call to getTickAtSqrtRatio.

As we can see from the vulnerability description the square root ratio price should be bounded by the MIN_SQRT_RATIO and MAX_SQRT_RATIO defined in the TickMath library contract to ensure that a price can't be returned that is outside of the range where liquidity is provided in the Pool.

/// @dev The minimum value that can be returned from #getSqrtRatioAtTick. Equivalent to getSqrtRatioAtTick(MIN_TICK)
uint160 internal constant MIN_SQRT_RATIO = 4295128739;
/// @dev The maximum value that can be returned from #getSqrtRatioAtTick. Equivalent to getSqrtRatioAtTick(MAX_TICK)
uint160 internal constant MAX_SQRT_RATIO = 1461446703485210103287273052203988822378723970342;

the functions of interest to us are defined in SqrtPriceMath as 

 /// @notice Gets the next sqrt price given an input amount of token0 or token1
    /// @dev Throws if price or liquidity are 0, or if the next price is out of bounds
    /// @param sqrtPX96 The starting price, i.e., before accounting for the input amount
    /// @param liquidity The amount of usable liquidity
    /// @param amountIn How much of token0, or token1, is being swapped in
    /// @param zeroForOne Whether the amount in is token0 or token1
    /// @return sqrtQX96 The price after adding the input amount to token0 or token1
    function getNextSqrtPriceFromInput(
        uint160 sqrtPX96,
        uint128 liquidity,
        uint256 amountIn,
        bool zeroForOne
    ) internal pure returns (uint160 sqrtQX96) {
        require(sqrtPX96 > 0);
        require(liquidity > 0);

        // round to make sure that we don't pass the target price
        return
            zeroForOne
                ? getNextSqrtPriceFromAmount0RoundingUp(sqrtPX96, liquidity, amountIn, true)
                : getNextSqrtPriceFromAmount1RoundingDown(sqrtPX96, liquidity, amountIn, true);
    }

and 

 /// @notice Gets the next sqrt price given an output amount of token0 or token1
    /// @dev Throws if price or liquidity are 0 or the next price is out of bounds
    /// @param sqrtPX96 The starting price before accounting for the output amount
    /// @param liquidity The amount of usable liquidity
    /// @param amountOut How much of token0, or token1, is being swapped out
    /// @param zeroForOne Whether the amount out is token0 or token1
    /// @return sqrtQX96 The price after removing the output amount of token0 or token1
    function getNextSqrtPriceFromOutput(
        uint160 sqrtPX96,
        uint128 liquidity,
        uint256 amountOut,
        bool zeroForOne
    ) internal pure returns (uint160 sqrtQX96) {
        require(sqrtPX96 > 0);
        require(liquidity > 0);

        // round to make sure that we pass the target price
        return
            zeroForOne
                ? getNextSqrtPriceFromAmount1RoundingDown(sqrtPX96, liquidity, amountOut, false)
                : getNextSqrtPriceFromAmount0RoundingUp(sqrtPX96, liquidity, amountOut, false);
    }

The Trail of Bits team defined the above-mentioned property as "getNextSqrtPriceFromInput/getNextSqrtPriceFromOutput always returns a price between MIN_SQRT_RATIO and MAX_SQRT_RATIO" which they turned into an Echidna test as: 

contract Other {
    // prop #30
    function test_getNextSqrtPriceFromInAndOutput(
        uint160 sqrtPX96,
        uint128 liquidity,
        uint256 amount,
        bool add
    ) public {
        require(sqrtPX96 >= TickMath.MIN_SQRT_RATIO && sqrtPX96 < TickMath.MAX_SQRT_RATIO);
        require(liquidity < 3121856577256316178563069792952001939); // max liquidity per tick
        uint256 next_sqrt = SqrtPriceMath.getNextSqrtPriceFromInput(sqrtPX96, liquidity, amount, add);
        assert(next_sqrt >= TickMath.MIN_SQRT_RATIO && next_sqrt < TickMath.MAX_SQRT_RATIO);
        next_sqrt = SqrtPriceMath.getNextSqrtPriceFromOutput(sqrtPX96, liquidity, amount, add);
        assert(next_sqrt >= TickMath.MIN_SQRT_RATIO && next_sqrt < TickMath.MAX_SQRT_RATIO);
    }
}

We can see that the test uses assertions to define the property that the next_sqrt is never less than MIN_SQRT_RATIO and never greater than the MAX_SQRT_RATIO.

To run the tests locally clone the UniswapV3 repo and checkout commit fd69d1e where the Echidna tests of interest were added, you'll just need to change the first line of the Other.config.yaml file from checkAsserts: true -> testMode: assertion since the repo was created with an older version of Echidna.

You can run the test using: 

echidna v3-core/audits/tob/contracts/crytic/echidna/Other.sol --contract Other --config v3-core/audits/tob/contracts/crytic/echidna/Other.config.yaml

we can see from the results that Echidna finds the following case where the assertion fails 

    function getTickAtSqrtRatio(uint160 sqrtPriceX96) internal pure returns (int24 tick) {
        // second inequality must be < because the price can never reach the price at the max tick
        require(sqrtPriceX96 >= MIN_SQRT_RATIO && sqrtPriceX96 < MAX_SQRT_RATIO, 'R');
        uint256 ratio = uint256(sqrtPriceX96) << 32;

/// @return sqrtRatioNextX96 The price after swapping the amount in/out, not to exceed the price target
    ...
    function computeSwapStep(
        uint160 sqrtRatioCurrentX96,
        ...
    )
        internal
        pure
        returns (
            uint160 sqrtRatioNextX96,
            ...
        )
    {
        ...
        if (exactIn) {
            ...
            if (amountRemainingLessFee >= amountIn) sqrtRatioNextX96 = sqrtRatioTargetX96;
            else
                sqrtRatioNextX96 = SqrtPriceMath.getNextSqrtPriceFromInput(
                    sqrtRatioCurrentX96,
                    liquidity,
                    amountRemainingLessFee,
                    zeroForOne
                );
        } else {
            ...
            if (uint256(-amountRemaining) >= amountOut) sqrtRatioNextX96 = sqrtRatioTargetX96;
            else
                sqrtRatioNextX96 = SqrtPriceMath.getNextSqrtPriceFromOutput(
                    sqrtRatioCurrentX96,
                    liquidity,
                    uint256(-amountRemaining),
                    zeroForOne
                );
        }

function swap(
        address recipient,
        bool zeroForOne,
        int256 amountSpecified,
        uint160 sqrtPriceLimitX96,
        bytes calldata data
    ) external override noDelegateCall returns (int256 amount0, int256 amount1) {
...
// compute values to swap to the target tick, price limit, or point where input/output amount is exhausted
            (state.sqrtPriceX96, step.amountIn, step.amountOut, step.feeAmount) = SwapMath.computeSwapStep(
                state.sqrtPriceX96,
                (zeroForOne ? step.sqrtPriceNextX96 < sqrtPriceLimitX96 : step.sqrtPriceNextX96 > sqrtPriceLimitX96)
                    ? sqrtPriceLimitX96
                    : step.sqrtPriceNextX96,
                state.liquidity,
                state.amountSpecifiedRemaining,
                fee
            );
...
 } else if (state.sqrtPriceX96 != step.sqrtPriceStartX96) {
                // recompute unless we're on a lower tick boundary (i.e. already transitioned ticks), and haven't moved
                state.tick = TickMath.getTickAtSqrtRatio(state.sqrtPriceX96);
            }