Invariant Validation through Fuzz Testing: A Case Study on DFX Finance

Introduction

While reading this article on ImmunFi about a white-hat hacker that found a rounding error in the DFX protocol when a pool contained a token with 2 decimals, I had an idea to test if this bug could be found using a property based fuzz test. This article is an overview of how I identified the protocol invariant and setup a fuzz test against the deployed contracts on Polygon.

Protocol Invariant for DFX Finance

DFX is an implementation of the Shell protocol, which is outlined in this white paper. Equation 5 of the paper defines the protocol invariant, which states that the utility $U$ should either increase or stay the same following a transaction that changes the reserves.

$${U(x) \over T} <= {U(x+x') \over T + y}$$

$x$ represents the reserves before a change and $x'$ the amount of tokens deposited or withdrawn.

While the DFX smart contracts do not expose any public methods to compute this invariant, I found the implementation encapsulated within the Curve Math contract. To compute the invariant for this test, I copied the implementation of these functions to a new smart contract in my repo.

The Fuzz Test

Below is the basic structure of the fuzz test I created using the Woke. A flow is a method that performs test actions (for those familiar with Hypothesis, a flow is a rule) using randomized inputs. A sequence is a collection of one or more flows that are randomly ordered. Before each sequence begins, the pre_sequence is called, this is used for some initialization such as deploying the contract I created that computes the invariant. Two flows are defined, deposit and withdraw which call the corresponding methods on the DFX Curve contract. After each flow is called, the utility invariant is executed to verify that that the transactions in the prior flow did not cause the utility to decrease.

class DFXFuzzTest(FuzzTest):
    _config: DFXChainConfig
    _invariant: Invariant
    _curve: Curve

    #hypothesis style random data generators
    st_amount = st.random_int(
            min=20000000000000000000, max=200000000000000000000, edge_values_prob=0.05
        )
    st_percent = st.random_float(min=0, max=1)    

    def __init__(self, chainConfig: DFXChainConfig):
        self._config = chainConfig

    def pre_sequence(self) -> None:
        """Initialize the environment for the contract.

        This function attaches to a deployed contract and calculates the initial invariant.

        Note:
            pre_sequence is called before the first flow to setup the required state
        """
        self._curve = self._config.pool
        self._invariant = Invariant.deploy()
        self._previous_inv = self._calcInvariant()

    @flow()
    def deposit(self, st_amount : uint):
        self._impl_deposit(st_amount)

    @flow()
    def withdraw(self, st_percent : float):        
        self._impl_withdraw(st_percent)

    @invariant(period=1)
    def utility(self) -> None:
        """Check and update the utility invariant

        This function asserts that the invariant (as calculated by _calcInvariant) 
        has not decreased. This is to ensure that "utility" in the pool is not decreasing.

        Raises:
            AssertionError: If the invariant has decreased.
        """
        inv = self._calcInvariant()
        assert inv >= self._previous_inv, "utility decreased."
        self._previous_inv = inv

Running the Test

The function below is used to setup the fuzz test for execution. The connect decorator points the fuzz test at an Alchemy node instance for Polygon, using the @ syntax to specify a specific block to fork the network using [Anvil](anvil Reference - Foundry Book.

DFXChainConfig is a small class I created to store chain-specific parameters, such as all the contract addresses for the Curve contract and ERC20 tokens. Using this setup allows me to easily run the same test on Ethereum mainnet or other network.

@default_chain.connect(fork=f"{os.getenv('POL_RPC_URL')}@{39422000}")
def test_polygon_before():
    default_chain.set_default_accounts(default_chain.accounts[0])

    PolygonChain = DFXChainConfig(
        pool=Curve(Address("0x2385D7aB31F5a470B1723675846cb074988531da")),
        EURS=IERC20(Address("0xE111178A87A3BFf0c8d18DECBa5798827539Ae99")),
        USDC=IERC20(Address("0x2791Bca1f2de4661ED88A30C99A7a9449Aa84174")),
        USDC_w=Address("0xBA12222222228d8Ba445958a75a0704d566BF2C8"),
        EURS_w=Address("0x38d693ce1df5aadf7bc62595a37d667ad57922e5"),
        add=0,
    )

    DFXFuzzTest(PolygonChain).run(sequences_count=1, flows_count=30)

Finally, to execute the test with Woke. -s 44 specifies a seed for the random number generator. Using the same seed yields a reproducible result and -n 1 runs the test in 1 process.

woke fuzz -s 44 -n 1 tests/test_polygon.py

The test immediately fails on the first deposit, confirming that the invariant was violated by the deposit.

To verify the fix, I set up a second test using a recent block number and found that the test now passed, confirming the bug was resolved.

@default_chain.connect(fork=f"{os.getenv('POL_RPC_URL')}@{45204868}")
def test_polygon_after():

    default_chain.set_default_accounts(default_chain.accounts[0])

    PolygonChain = DFXChainConfig(
        pool=Curve(Address("0x2385D7aB31F5a470B1723675846cb074988531da")),
        EURS=IERC20(Address("0xE111178A87A3BFf0c8d18DECBa5798827539Ae99")),
        USDC=IERC20(Address("0x2791Bca1f2de4661ED88A30C99A7a9449Aa84174")),
        USDC_w=Address("0xBA12222222228d8Ba445958a75a0704d566BF2C8"),
        EURS_w=Address("0x38d693ce1df5aadf7bc62595a37d667ad57922e5"),
        add=100,
    )

    DFXFuzzTest(PolygonChain).run(sequences_count=1, flows_count=30)

This tests runs through randomized deposits and withdraws with no errors, indicating that the bug was fixed.

Conclusion

This article gives an overview of how to create and execute a property based fuzz test for Solidity contracts. The tests can be run against production contracts by using a local fork of the network. Building property tests to verify correct behavior when deploying to new blockchains and tokens is a vital piece of the security puzzle.

The full code for the test in this article is available on Github