Introducing Recon: Invariant Testing Within Minutes

What is Recon?

Recon is a tool created to speed up the process of writing invariant tests. It connects to any open-source Solidity project and automatically generates the boilerplate code to create invariant tests for Echidna, Medusa, and Foundry, all in a few clicks.

Instead of spending hours setting up the test suite, developers and auditors can instead focus on creating the relevant properties that might uncover vulnerabilities in their systems.

How It Works

In this demo of the test harness, we'll be using the Uniswap v3 repository, as it's a well-known codebase by most auditors and developers.

Before launch, Uniswap V3 underwent an audit by Trail of Bits where they expanded the existing Echidna test suite and defined the properties that should hold throughout the system. The property we'll look at in this example is: 

1. If calling swap does not change the sqrtPriceX96, liquidity will not change (Property-17)

We'll see how in a few steps, we can create a new test suite with Recon, and start testing this property.

The repo created from the following example is available here.

Project Setup

After logging into the Recon web app you'll be prompted to upload a public GitHub repo:

Clicking "Start Job" will start a build job on the Recon cloud service, which will return all contracts from the project with the ability to select which functions to add to the testing harness.

Since in this demo we'll only be testing properties related to the Pool contract's functions and TestERC20's state variables using assertion tests we don't need to select any functions from the contracts we're targeting. If we were to create Echidna boolean property tests to fuzz input values for specific functions we'd select the functions of interest here and define our properties in the Properties contract. In our case we leave the mint and swap functions selected in case we decide to add boolean property tests at a future time from the "Build your Handlers" page and deselect (in red) all functions not of interest: 

From the "Before and After Trackers" tab, we can select the state variables in the Pool contract that we want to keep track of for making assertions, analogous to "ghost variables" in Certora or Foundry tutorials.

In our case, we'll only be using balanceOf from the TestERC20 contract and feeGrowthGlobal0X128 , feeGrowthGlobal1X128, liquidity, slot0 and ticks from UniswapV3Pool since they're all we need to prove our property about liquidity:

Once we have selected these variables, we can see the "Results Page" where we have all the files for our test harness available to us:

TargetFunctions.sol

This file provides us an entry point to functions of our contract of interest which get called by Echidna/Medusa/Foundry when running boolean property tests and is where we can define assertion test. 

BeforeAfter.sol

This exposes ghost copies of contract variables that get stored in a struct which gets updated via calls to the __before and __after functions. These simplify the process of accessing state variable values in a contract, making everything more easily accessed from the _before and _after structs which store the ghost variables. 

Setup.sol

The Setup contract is simply used to deploy all contracts required by our system. Since the deployment may be specific for each system, a manual fix is required, which is why the default for this is as a TODO for the implementer of the test suite. In this example because of some quirks about how a UniswapVPool is deployed we don't instantiate it here but instead using the _init function. 

CryticToFoundry.sol

This contract is used for creating Foundry unit tests for failing cases of fuzz runs by Echidna/Medusa/Foundry. This is useful for integrating into a development pipeline as it can allow you to see if changes have resolved previously discovered failing cases or if they create new violations of them. 

CryticTester.sol

This is the main entry point for Echidna and Medusa to call into the fuzzed contracts.

Properties.sol

This is where you'll write properties to be tested on the contracts of interest.

medusa.json & echidna.yaml

These are just configuration files for Echidna and Medusa used for adjusting configurations of the fuzzers in the tests that you run. 

Running The Fuzzer

Setup

Recon defaults to configuring Echidna to run boolean property tests on functions whose names are prefixed with invariant_ instead of the standard echidna_ prefix.

We'll be using the assertion tests created by the Trail of Bits team for the above-selected property with modifications so they work with the harness created by Recon. Since these tests are assertion tests they require calling contract functions to verify a specific state and so we define them in the TargetFunctions contract instead of in Properties and we can use any prefix when naming and so use test_. 

**Note: the accompanying repo has already included the following setup steps but if you're using your own repo you'll need to follow these steps to add your Recon harness

For projects that don't use Foundry: Since the Uniswap V3 repo doesn't implement Foundry we'll first need to add it using forge install. This gives us the ability to debug issues using Foundry's enhanced debugging tools as well as creating Foundry tests for any failing cases that may be discovered during a fuzzing campaign.

From the "Results Page"in Recon you'll be given the option to download the files from the created harness, this should be added to the tests/ directory created by Foundry.

We'll also need to add the Chimera dependency using forge install Recon-Fuzz/chimera which helps with configuring our project to use the Recon harness. 

We then add Chimera to our remappings in a foundry.toml file along with some configurations to ensure the CryticCompiler works with the solc compiler version being used by Uniswap: 

[profile.default]
remappings = [
    'forge-std/=lib/forge-std/src/',
    '@chimera/=lib/chimera/src/'
]
solc = "0.7.6"
evm_version = "istanbul"

Swap Property Test

For the property we want to test:

•  If calling swap does not change the sqrtPriceX96, liquidity will not change

we define an assertion in the following function that has been defined in the Setup contract that checks this:

function check_swap_invariants(
        int24 tick_bfre,
        int24 tick_aftr,
        uint128 liq_bfre,
        uint128 liq_aftr,
        uint256 bal_sell_bfre,
        uint256 bal_sell_aftr,
        uint256 bal_buy_bfre,
        uint256 bal_buy_aftr,
        uint256 feegrowth_sell_bfre,
        uint256 feegrowth_sell_aftr,
        uint256 feegrowth_buy_bfre,
        uint256 feegrowth_buy_aftr
    ) internal {
        // prop #17
        if (tick_bfre == tick_aftr) {
            assert(liq_bfre == liq_aftr);
        }
    }

which is evaluated in the following test functions in TargetFunctions: test_swap_exactIn_zeroForOne, 

test_swap_exactIn_oneForZero, test_swap_exactOut_zeroForOne, test_swap_exactOut_oneForZero. 

 

Our tests use the before and after ghost variables provided by the BeforeAfter contract to check the state of the system and ensure that the property isn't violated: 

        __before();
        swapper.doSwap(true, _amountSpecified, sqrtPriceLimitX96);
        __after();

        int24 beforeCurrentTick = _before.uniswapV3Pool_currentTick;
        int24 afterCurrentTick = _after.uniswapV3Pool_currentTick;

        check_swap_invariants(
            beforeCurrentTick,
            afterCurrentTick,
            _before.uniswapV3Pool_liquidity,
            _after.uniswapV3Pool_liquidity,
            _before.testERC20_balanceOfToken0,
            _after.testERC20_balanceOfToken0,
            _before.testERC20_balanceOfToken1,
            _after.testERC20_balanceOfToken1,
            _before.uniswapV3Pool_feeGrowthGlobal0X128,
            _after.uniswapV3Pool_feeGrowthGlobal0X128,
            _before.uniswapV3Pool_feeGrowthGlobal1X128,
            _after.uniswapV3Pool_feeGrowthGlobal1X128
        );

 

We can run the above tests implementing this assertion using the following command from the root directory:

echidna test/recon/CryticTester.sol --contract CryticTester --config echidna.yaml 

 

Note: If you're following along with the accompanying repo you'll need to make some changes to the chimera submodule dependency because of incompatible solidity compiler versions to get Echidna to run. You'll need to replace all occurrences of pragma solidity ^0.8.0 with pragma solidity ^0.7.6 and in Hevm.sol you'll need to replace the pragma statement with pragma abicoder v2. 

 

We can see from the results that the tests pass meaning that none of the assertions failed: 

 

Now to ensure that our tests are properly verifying the property that we desire we can introduce a mutation into the swap function on line 724 which sets the liquidity of the tick to 0 if the price hasn't changed:

// shift tick if we reached the next price
            if (state.sqrtPriceX96 == step.sqrtPriceNextX96) {
                ...
            } 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);
                // MUTATION
                state.liquidity = 0;
            }

 

and we see that it gets violated when we run echidna again in the 

test_swap_exactOut_zeroForOne function

This demonstrates that if the price stays the same our property tests do indeed catch incorrect functionality by the system that would cause the liquidity within the tick range to change, giving us more confidence that our tests have been properly implemented. 

Enhancing The Suite

Recon provides a harness to reduce the time to set up your test suite.

In the above example, we've shown how we can replicate part of the existing test suite for Uniswap V3 with this harness with only a fraction of the setup required if we were to have done so manually.

This is the core value that Recon offers, less time to implement your test suite, so you can focus on writing tests instead of configuring your test harness.

I would like to offer my very great appreciation to Nican0r, who has created this in-depth guide on how to use Recon on Uniswap v3.