Writing Multi-Fuzzer Invariant Tests Using Chimera

Should you use Foundry, Echidna or Medusa fuzzers when writing your smart contract invariant fuzz tests? Why settle for just one when you can use all 3 from the same codebase by writing your fuzz tests using Chimera!

Chimera is best thought of as a “swiss army knife” - collection of tools that allow smart contract developers and auditors to use as few or as many of the tools, in order to achieve the goal of writing one codebase that can be used to execute multiple fuzzers.

Let’s explore how to use Chimera to write a smart contract invariant fuzz testing suite using a simplified version of a real finding from a recent private audit. The full code can be found in my Solidity Fuzzing Challenge repository.

Vulnerable Vesting Contract

Our vulnerable contract Vesting.sol implements a simplified vesting scheme where users receive points which can be redeemed for tokens once the vesting period has expired. Much of the complexity has been removed to only contain the code and functionality relevant to our example:

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.23;

contract Vesting {
    uint24 public constant TOTAL_POINTS = 100_000;

    struct AllocationInput {
        address recipient;
        uint24 points;
        uint8  vestingWeeks;
    }

    struct AllocationData {
        uint24 points;
        uint8  vestingWeeks;
        bool   claimed;
    }

    mapping(address recipient => AllocationData data) public allocations;

    constructor(AllocationInput[] memory allocInput) {
        uint256 inputLength = allocInput.length;
        require(inputLength > 0, "No allocations");

        uint24 totalPoints;
        for(uint256 i; i<inputLength; i++) {
            require(allocInput[i].points != 0, "Zero points invalid");
            require(allocations[allocInput[i].recipient].points == 0, "Already set");

            totalPoints += allocInput[i].points;
            require(totalPoints <= TOTAL_POINTS, "Too many points");

            allocations[allocInput[i].recipient].points = allocInput[i].points;
            allocations[allocInput[i].recipient].vestingWeeks = allocInput[i].vestingWeeks;
        }

        require(totalPoints == TOTAL_POINTS, "Not enough points");
    }

    // users entitled to an allocation can transfer their points to
    // another address if they haven't claimed
    function transferPoints(address to, uint24 points) external {
        require(points != 0, "Zero points invalid");

        AllocationData memory fromAllocation = allocations[msg.sender];
        require(fromAllocation.points >= points, "Insufficient points");
        require(!fromAllocation.claimed, "Already claimed");

        AllocationData memory toAllocation = allocations[to];
        require(!toAllocation.claimed, "Already claimed");

        // enforce identical vesting periods if `to` has an active vesting period
        if(toAllocation.vestingWeeks != 0) {
            require(fromAllocation.vestingWeeks == toAllocation.vestingWeeks, "Vesting mismatch");
        }

        allocations[msg.sender].points = fromAllocation.points - points;
        allocations[to].points = toAllocation.points + points;

        // if `to` had no active vesting period, copy from `from`
        if (toAllocation.vestingWeeks == 0) {
            allocations[to].vestingWeeks = fromAllocation.vestingWeeks;
        }
    }
}

Thinking In Invariants

The primary challenge of writing good invariant fuzz tests is learning to think in terms of contract and protocol invariants. One systematic way to do this is to think in terms of “contract lifecycle” and “white/black-box”.

Contract Lifecycle

Smart contracts have 3 primary phases of life:

construction / initialization
regular functioning
optionally an end state

It can be helpful to think of which properties must remain true during each of these life phases. For example in our contract at the initialization state, the total amount of points allocated to recipients must equal the expected total number of points. Since this invariant is “cheap” (in terms of gas costs) to implement, it makes sense to implement it directly into our code.

During the regular functioning and end of life phases of the contract lifecycle, a good invariant property would be:

the total amount of points allocated to users must remain equal to the total number of points

However this invariant property is “expensive” in that it is cost-prohibitive to iterate and sum every user’s points at the smart contract level. Hence such invariants should be implemented “off-chain” by developers as part of a protocol’s invariant fuzz tests.

White/Black Box

Another way of thinking about invariants is in terms of white or black boxes.

A “white box” invariant is one that we implement based upon internal knowledge of how the smart contract works, while a “black box” invariant is a property that we can glean from the protocol’s design or documentation, without needing to know about the internals of how the protocol actually implements its functionality.

For the full version of the contract a useful “end state” invariant would be that the total amount of tokens which have been distributed to users is equal to the amount of vested tokens. This invariant is “black-box” since we don’t need to know anything about the contract’s underlying implementation, we just know this property exists and should be true at the end state.

Writing The Test Setup

The first thing we need to do is create a Setup.sol file which will inherit from Chimera’s BaseSetup contract. Our Setup contract can:

either inherit directly from the contract being tested or have that contract as a member variable
contain “ghost” variables use to track important state for comparison with contract state during invariant checks

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.23;

import { Vesting } from "../../src/09-vesting/Vesting.sol";
import { BaseSetup } from "@chimera/BaseSetup.sol";

abstract contract Setup is BaseSetup {
    // contract being tested
    uint24 constant TOTAL_POINTS = 100_000;
    Vesting vesting;

    // ghost variables
    address[] recipients;

    function setup() internal virtual override {
        // use two recipients with equal allocation
        recipients.push(address(0x1111));
        recipients.push(address(0x2222));

        // prepare allocation array
        Vesting.AllocationInput[] memory inputs
            = new Vesting.AllocationInput[](2);
        inputs[0].recipient = recipients[0];
        inputs[0].points = TOTAL_POINTS / 2;
        inputs[0].vestingWeeks = 10;
        inputs[1].recipient = recipients[1];
        inputs[1].points = TOTAL_POINTS / 2;
        inputs[1].vestingWeeks = 10;

        vesting = new Vesting(inputs);
    }
}

Avoid Fuzzer-Specific Cheatcodes In Setup

When writing the test setup we need to avoid using fuzzer-specific cheatcodes. A good way to do this is to only use cheatcodes from Chimera’s IHevm interface which prevents using any cheatcodes that won’t work across all fuzzers.

Implementing The Invariants

Next we create a Properties.sol file to define our invariants; it inherits from our Setup contract and Chimera’s Asserts contract. In this file we will implement the invariants as Echidna/Medusa-style invariants which are functions that return a boolean and we’ll use property_ as the function prefix:

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.23;

import { Setup } from "./Setup.sol";
import { Asserts } from "@chimera/Asserts.sol";

abstract contract Properties is Setup, Asserts {

    function property_users_points_sum_eq_total_points() public view returns(bool result) {
        uint24 totalPoints;

        // sum up all user points
        for(uint256 i; i<recipients.length; i++) {
            (uint24 points, , ) = vesting.allocations(recipients[i]);

            totalPoints += points;
        }

        // true if invariant held, false otherwise
        if(totalPoints == TOTAL_POINTS) result = true;

        // note: Solidity always initializes to default values
        // so no need to explicitly set result = false as false
        // is the default value for bool
    }
}

Wrapping The Target Functions

With our setup complete and invariants defined, the next step is to create “handlers” which “wrap” the target functions of the contract being tested. The general goals are to:

exercise the contract’s functionality as organically as possible
prevent wasted runs that would revert due to failing to satisfy basic preconditions

A “handler” is a function with a handler_ prefix followed by the underlying function name which wraps that function and satisfies required preconditions. Create a new file TargetFunctions.sol which inherits from our Properties contract and Chimera’s BaseTargetFunctions contract:

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.23;

import { Properties } from "./Properties.sol";
import { BaseTargetFunctions } from "@chimera/BaseTargetFunctions.sol";
import { IHevm, vm } from "@chimera/Hevm.sol";

abstract contract TargetFunctions is BaseTargetFunctions, Properties {

    function handler_transferPoints(uint256 recipientIndex,
                                    uint256 senderIndex,
                                    uint24 pointsToTransfer) external {
        // get an index into the recipients array to randomly
        // select a valid recipient
        //
        // note: using `between` provided by Chimera instead of
        // Foundry's `bound` for cross-fuzzer compatibility
        recipientIndex = between(recipientIndex, 0, recipients.length-1);
        senderIndex    = between(senderIndex, 0, recipients.length-1);

        address sender = recipients[senderIndex];
        address recipient = recipients[recipientIndex];

        (uint24 senderMaxPoints, , ) = vesting.allocations(sender);

        pointsToTransfer = uint24(between(pointsToTransfer, 1, senderMaxPoints));

        // note: using `vm` from Chimera's IHevm
        // for cross-fuzzer cheatcode compatibility
        vm.prank(sender);
        vesting.transferPoints(recipient, pointsToTransfer);
    }
}

Writing Echidna & Medusa Front-End

Now that all of our components are in-place, we only need to write the “front-end” contracts for our fuzzers and provide any configuration files. Firstly let’s write the Echidna & Medusa front-end VestingCryticTester.sol which is used to execute the Echidna and Medusa fuzzers. It inherits from our TargetFunctions contract and Chimera’s CryticAsserts contract:

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.23;

import { TargetFunctions } from "./TargetFunctions.sol";
import { CryticAsserts } from "@chimera/CryticAsserts.sol";

// configure solc-select to use compiler version:
// solc-select install 0.8.23
// solc-select use 0.8.23
//
// run from base project directory with:
// echidna . --contract VestingCryticTester --config test/09-vesting/echidna.yaml
// medusa --config test/09-vesting/medusa.json fuzz
contract VestingCryticTester is TargetFunctions, CryticAsserts {
  constructor() payable {
    setup();
  }
}

Echidna Config

We also need to create the following configuration file echidna.yaml:

# don't allow fuzzer to use all functions
# since we are using handlers
allContracts: false

# record fuzzer coverage to see what parts of the code
# fuzzer executes
corpusDir: "./test/09-vesting/coverage-echidna"

# prefix of invariant function
prefix: "property_"

# instruct foundry to compile tests
cryticArgs: ["--foundry-compile-all"]

Medusa Config

Similarly we need to create Medusa’s configuration file medusa.json:

{
    "fuzzing": {
        "workers": 10,
        "workerResetLimit": 50,
        "_COMMENT_TESTING_1": "changed timeout to limit fuzzing time",
        "timeout": 10,
        "testLimit": 0,
        "callSequenceLength": 100,
        "_COMMENT_TESTING_8": "added directory to store coverage data",
        "corpusDirectory": "coverage-medusa",
        "coverageEnabled": true,
        "_COMMENT_TESTING_2": "added test contract to deploymentOrder",
        "targetContracts": ["VestingCryticTester"],
        "targetContractsBalances": [],
        "constructorArgs": {},
        "deployerAddress": "0x30000",
        "senderAddresses": [
            "0x10000",
            "0x20000",
            "0x30000"
        ],
        "blockNumberDelayMax": 60480,
        "blockTimestampDelayMax": 604800,
        "blockGasLimit": 125000000,
        "transactionGasLimit": 12500000,
        "testing": {
            "stopOnFailedTest": true,
            "stopOnFailedContractMatching": true,
            "stopOnNoTests": true,
            "testAllContracts": false,
            "traceAll": false,
            "assertionTesting": {
                "enabled": false,
                "testViewMethods": false,
                "assertionModes": {
                    "failOnCompilerInsertedPanic": false,
                    "failOnAssertion": true,
                    "failOnArithmeticUnderflow": false,
                    "failOnDivideByZero": false,
                    "failOnEnumTypeConversionOutOfBounds": false,
                    "failOnIncorrectStorageAccess": false,
                    "failOnPopEmptyArray": false,
                    "failOnOutOfBoundsArrayAccess": false,
                    "failOnAllocateTooMuchMemory": false,
                    "failOnCallUninitializedVariable": false
                }
            },
            "propertyTesting": {
                "enabled": true,
                "_COMMENT_TESTING_6": "changed prefix to match invariant function",
                "testPrefixes": [
                    "property_"
                ]
            },
            "optimizationTesting": {
                "enabled": false,
                "testPrefixes": [
                    "optimize_"
                ]
            }
        },
        "chainConfig": {
            "codeSizeCheckDisabled": true,
            "cheatCodes": {
                "cheatCodesEnabled": true,
                "enableFFI": false
            }
        }
    },
    "compilation": {
        "platform": "crytic-compile",
        "platformConfig": {
            "_COMMENT_TESTING_7": "changed target to point to main directory where command is run from",
            "target": "./../../.",
            "solcVersion": "",
            "exportDirectory": "",
            "args": ["--foundry-compile-all"]
        }
    },
    "logging": {
        "level": "info",
        "logDirectory": ""
    }
}

Writing Foundry Front-End

The final piece required is our Foundry “front-end” contract; create a new file VestingCryticToFoundry.sol. This contract will:

inherit from our TargetFunctions contract and Chimera’s FoundryAsserts contract
programmatically implement required setup as Foundry doesn’t use configuration files
wrap each of our Echidna/Medusa-style property_* invariants into Foundry-style invariant_* functions that simply assert the property_* functions return true:

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.23;

import { TargetFunctions } from "./TargetFunctions.sol";
import { FoundryAsserts } from "@chimera/FoundryAsserts.sol";
import { Test } from "forge-std/Test.sol";

// run from base project directory with:
// forge test --match-contract VestingCryticToFoundry
// (if an invariant fails add -vvvvv on the end to see what failed)
//
// get coverage report (see https://medium.com/@rohanzarathustra/forge-coverage-overview-744d967e112f):
//
// 1) forge coverage --report lcov --report-file test/09-vesting/coverage-foundry.lcov --match-contract VestingCryticToFoundry
// 2) genhtml test/09-vesting/coverage-foundry.lcov -o test/09-vesting/coverage-foundry
// 3) open test/09-vesting/coverage-foundry/index.html in your browser and
//    navigate to the relevant source file to see line-by-line execution records

contract VestingCryticToFoundry is Test, TargetFunctions, FoundryAsserts {
    function setUp() public {
      setup();

      // Foundry doesn't use config files but does
      // the setup programmatically here

      // target the fuzzer on this contract as it will
      // contain the handler functions
      targetContract(address(this));

      // handler functions to target during invariant tests
      bytes4[] memory selectors = new bytes4[](1);
      selectors[0] = this.handler_transferPoints.selector;

      targetSelector(FuzzSelector({ addr: address(this), selectors: selectors }));
    }

    // wrap every "property_*" invariant function into
    // a Foundry-style "invariant_*" function
    function invariant_users_points_sum_eq_total_points() public {
      assertTrue(property_users_points_sum_eq_total_points());
    }
}

Running All Fuzzers

Now we can run all 3 fuzzers from the project directory like this:

echidna . --contract VestingCryticTester --config test/09-vesting/echidna.yaml
medusa --config test/09-vesting/medusa.json fuzz
forge test --match-contract VestingCryticToFoundry

Additionally all 3 fuzzers will generate their own coverage folder where we can inspect line-by-line coverage. Checking coverage is very important when building a test suite for your protocol to ensure that all the relevant lines are being exercised by the test suite.

Using Chimera to build the fuzz suite also allows easy cloud-based fuzzing via getrecon.xyz.

Verifying The Fix

All 3 fuzzers are easily able to break the invariant; the Vesting::transferPoints function is vulnerable to self-transfer where a user can transfer points to themselves which ends up increasing their points. This could be weaponized by a user to give themselves maximum points then drain the entire token allocation.

To fix this prevent self-transfer in Vesting::transferPoints:

    function transferPoints(address to, uint24 points) external {
        require(points != 0, "Zero points invalid");
+       require(msg.sender != to, "Self transfer invalid");

Then re-run all 3 fuzzers and verify none are able to break the invariant.

Conclusion

Chimera is an excellent framework that lets smart contract developers and auditors more easily write invariant fuzz testing suites which can be used across multiple fuzzers. Smart contract developers should strongly consider defining contract and protocol invariants and using Chimera to create multi-fuzzer invariant fuzz testing suites for their protocols.

Writing Multi-Fuzzer Invariant Tests Using Chimera

Comments

Deep Dives

Exploiting Under-Constrained ZK Circuits

More from this blog

Using Claude To Evolve Specialist AI Smart Contract Auditors

The Yieldoor Gas Optimizoor

DeFi Liquidation Vulnerabilities

Find Highs Before External Auditors Using Certora Formal Verification

Find Highs Before External Auditors Using Invariant Fuzz Testing

Vulnerable Vesting Contract

Thinking In Invariants

Contract Lifecycle

White/Black Box

Writing The Test Setup

Avoid Fuzzer-Specific Cheatcodes In Setup

Implementing The Invariants

Wrapping The Target Functions

Writing Echidna & Medusa Front-End

Echidna Config

Medusa Config

Writing Foundry Front-End

Running All Fuzzers

Verifying The Fix

Conclusion

Command Palette

Comments

Deep Dives

Exploiting Under-Constrained ZK Circuits

More from this blog

Vulnerable Vesting Contract

Thinking In Invariants

Contract Lifecycle

White/Black Box

Writing The Test Setup

Avoid Fuzzer-Specific Cheatcodes In Setup

Implementing The Invariants

Wrapping The Target Functions

Writing Echidna & Medusa Front-End

Echidna Config

Medusa Config

Writing Foundry Front-End

Running All Fuzzers

Verifying The Fix

Conclusion