Introduction

Recon is a tool for automatically scaffolding and running invariant testing in the cloud.

We also maintain a suite of tools that help with invariant testing and security research more generally.

Creating An Account

To get started using Recon's free tools, you don't need to create an account and can use any of the tools in the Free Recon Tools section.

To use more advanced features (running jobs in the cloud, alerts, etc.) you'll need to create an account using your GitHub account and sign up for Recon Pro.

Once you've created an account, you'll be redirected to the dashboard where you'll have access to all of the tools in the Recon suite.

Learn Invariant Testing

Most of our guides and documentation are focused on using fuzzing tools, primarily Echidna and Medusa because we use them internally at Recon. However, we also support running other tools on our cloud infrastructure such as Foundry (fuzzing), Halmos (formal verification), and Kontrol (formal verification).

After having chosen a tool best suited to your needs and downloading it locally, you can get started by running jobs directly on the jobs pge.

If you're new to invariant testing, we recommend you starting with the following posts:

  1. First Day At Invariant School
  2. How To Define Invariants
  3. Implementing Your First Smart Contract Invariants: A Practical Guide

If you prefer a full end-to-end video bootcamp, checkout this series on everything you need to know about invariant testing.

Once you've grasped the basics of invariant testing you can setup your first suite and run it on Recon. For a step-by-step guide on how to do this, check out the First Steps guide.

If you have any questions about how to use Recon or invariant testing in general, you can reach out to our team on Discord.

Additional Learning Resources

Invariant Testing In General

If you're looking for more resources to help you get started with invariant testing, see the following:

Fuzzers

For more resources on our favorite fuzzers (Echidna and Medusa) see the following:

Retrospectives

Deep dives into the work we've done with our elite customers with tips and tricks on building effective invariant testing suites:

Suggested Office Hours (Video)

Office hours are improvised live recordings of useful tips and tricks for invariant testing. They provide a lot of hot takes and insights based on what the Recon Team was working on at the time.

Trophies

A sample of some publicly disclosed bugs we've found using invariant testing. You can use these to understand what kinds of properties will help you find issues that manual review sometimes can't.

First Steps

To make getting started with Invariant Testing as easy as possible, we created the create-chimera-app repository which serves as a template that you can use to create a new project with invariant testing built in.

This template uses our Chimera framework to let you run invariant tests with Echidna and Medusa that can be easily debugged using Foundry. We've also incorporated contracts from our Setup Helpers repo which make managing the test suite setup much simpler.

Creating A New Project

If you haven't already, first create a recon account as described in the create an account section and install either Echidna or Medusa.

Next you'll need to create a new project using the create-chimera-app template. You can use the Use this template button on GitHub to do this. This will automatically create a new repository using the create-chimera-app template on your GitHub account.

Create-chimera-app ships with the default foundry project as an example. This is a simple Counter.sol contract that you can use to test the fuzzing capabilities of Echidna and Medusa.

Testing

An example invariant is implemented in the Properties contract and some in-line properties are defined in the TargetFunctions contract.

You can run the default fuzzing tests using the following commands

Echidna

echidna . --contract CryticTester --config echidna.yaml

Medusa

medusa fuzz

Expanding The Example Project

Create-chimera-app is meant to be a starting point for your own project. You can expand the example project by adding your own contracts and properties. See the Chimera Framework section on what the role of each contract is and how to expand the example project.

This substack post walks you through the process of converting invariants from English to Solidity using a ERC4626 vault on an example project using Chimera.

To add new contracts just delete the existing Counter.sol and Counter.t.sol files and add your own.

After adding your new contracts, you can add handlers for the contracts you want to test using invariant testing by using the Build Handlers page on Recon (see this section for how to do this).

Introduction

In this section, we'll use Create Chimera App to create a simple contract and run invariant tests on it.

Getting started

Clone the create-chimera-app repo.

Or

Use forge init --template https://github.com/Recon-Fuzz/create-chimera-app

Writing the contract

First we'll create a simple contract that given a deposit will give you points proportional to the amount of time you've deposited for, where longer deposits equals more points:


contract Points {
    mapping (address => uint256) depositAmount;
    mapping (address => uint256) depositTime;

    function deposit(uint256 amt) external {
        depositAmount[msg.sender] += amt;
        depositTime[msg.sender] = block.timestamp;
    }

    function power(address who) external view returns (uint256) {
        return depositAmount[msg.sender] * (block.timestamp - depositTime[msg.sender]);
    }
}

Dealing with the boilerplate

We can delete Counter.t.sol since we won't be writing unit tests and rename Counter.sol to Points.sol

Next, we need to fix some imports.

1. Delete all handlers in the TargetFunctions, AdminTargets and DoomsdayTargets

After deleting all the handler functions in the TargetFunctions your contract should look like:

abstract contract TargetFunctions is
    AdminTargets,
    DoomsdayTargets,
    ManagersTargets
{ }

Similarly for AdminTargets:

abstract contract AdminTargets is
    BaseTargetFunctions,
    Properties
{ }

Similarly for DoomsdayTargets

abstract contract DoomsdayTargets is
    BaseTargetFunctions,
    Properties
{
    ...

    modifier stateless() {
        _;
        revert("stateless");
    }
}

2. Delete the calls for ghost variables

abstract contract BeforeAfter is Setup {
    struct Vars {
        uint256 counter_number;
    }

    Vars internal _before;
    Vars internal _after;

    modifier updateGhosts {
        __before();
        _;
        __after();
    }

    function __before() internal {
    }

    function __after() internal {
    }
}

3. Delete the targetContract line from CryticToFoundry

// forge test --match-contract CryticToFoundry -vv
contract CryticToFoundry is Test, TargetFunctions, FoundryAsserts {
    function setUp() public {
        setup();
 }

    // forge test --match-test test_crytic -vvv
    function test_crytic() public {
        // TODO: add failing property tests here for debugging
    }
}

4. Delete the properties

abstract contract Properties is BeforeAfter, Asserts {
}

5. Fixing the Setup contract

The code should fail to compile due to:

Error: Compiler run failed:
Error (6275): Source "src/Counter.sol" not found: File not found. Searched the following locations: "/temp/example-recon".
ParserError: Source "src/Counter.sol" not found: File not found. Searched the following locations: "/temp/example-recon".
  --> test/recon/Setup.sol:16:1:
 |
16 | import "src/Counter.sol";

To resolve this, we just have to change the import and deploy the new Points contract, the rest of the setup remains the same:

...

/// @notice we change the import to include the Points contract 
import "src/Points.sol";

abstract contract Setup is BaseSetup, ActorManager, AssetManager, Utils {
    Points points;

    /// === Setup === ///
    function setup() internal virtual override {
        ...

        /// @notice we deploy the Points contract 
        points = new Points();

        ...
    }

    ...
}

Running the fuzzer

We should now be able to run the fuzzer with no state exploration since we haven't added handler functions.

Before we commit to using the fuzzer (better tool but slower feedback cycle), we'll use Foundry to check that everything compiles.

Running forge build we see that it passes, meaning the deployment in the Setup contract is working.

We can now run the Medusa fuzzer using:

medusa fuzz

which gives us the following output:

medusa fuzz
⇾ Reading the configuration file at: /temp/example-recon/medusa.json
⇾ Compiling targets with crytic-compile
⇾ Running command:
crytic-compile . --export-format solc --foundry-compile-all
⇾ Finished compiling targets in 5s
⇾ No Slither cached results found at slither_results.json
⇾ Running Slither:
slither . --ignore-compile --print echidna --json -
⇾ Finished running Slither in 7s
⇾ Initializing corpus
⇾ Setting up test chain
⇾ Finished setting up test chain
⇾ Fuzzing with 16 workers
⇾ [NOT STARTED] Assertion Test: CryticTester.switch_asset(uint256)
⇾ [NOT STARTED] Assertion Test: CryticTester.add_new_asset(uint8)
⇾ fuzz: elapsed: 0s, calls: 0 (0/sec), seq/s: 0, branches hit: 289, corpus: 0, failures: 0/0, gas/s: 0
⇾ [NOT STARTED] Assertion Test: CryticTester.asset_approve(address,uint128)
⇾ [NOT STARTED] Assertion Test: CryticTester.asset_mint(address,uint128)
⇾ [NOT STARTED] Assertion Test: CryticTester.switchActor(uint256)
⇾ fuzz: elapsed: 3s, calls: 70172 (23389/sec), seq/s: 230, branches hit: 481, corpus: 126, failures: 0/692, gas/s: 8560148887
⇾ fuzz: elapsed: 6s, calls: 141341 (236

At this point, we expect close to no lines to be covered (indicated by the corpus value in the output). You can now stop medusa with CTRL + C.

We can note that because the corpus value is nonzero, something is being covered, in our case these are the only exposed functions in the ManagerTargets which can help you setup tests with multiple tokens and multiple actors.

We can now pen the coverage report located at /medusa/coverage/coverage_report.html to confirm that none of the lines in the Points contract are actually being covered.

In our coverage report a line highlighted in green means the line was hit, a line highlighted in red means the line was not hit.

Medusa Coverage

Let's rectify the lack of coverage in our Points contract by adding target function handlers.

Building target functions

Foundry produces an /out folder any time you compile your project, this contains the ABI of the Points contract.

We'll use this in conjunction with our ABI builder to quickly generate target function handlers for our TargetFunctions contract:

  1. Open out/Points.sol/Points.json
  2. Copy the entire content
  3. Navigate to the ABI Builder
  4. Paste the ABI
  5. Rename the contract to points replacing the text in the "Your_contract" form field

This generates the TargetFunctions for Points. In our case we'll first just add the handler created for the deposit function:

Target Function For Points

For simplicity you can just copy the individual handler into your TargetFunctions.sol contract. When working on a larger project however you can use the "Download All Files" button to add these directly into your project.

Make sure to add the updateGhosts and asActor modifiers to this function if they are not present:

  • updateGhosts - will update all ghost variables before and after the call to the function
  • asActor - will ensure that the call is done by the currently active actor (returned by _getActor())

Your TargetFunctions contract should now look like:

abstract contract TargetFunctions is
    AdminTargets,
    DoomsdayTargets,
    ManagersTargets
{
    function points_deposit(uint256 amt) public updateGhosts asActor {
        points.deposit(amt);
    }
}

We can now run Medusa again to see how our newly added target function has changed our coverage. The coverage report is effectively our eyes into what the fuzzer is doing.

Better Coverage

We now see that the deposit function is fully covered, but the power function is not since we haven't added a handler for it.

We can now start defining some properties to see if there are any edge cases in our Points contract that we may not have expected.

Checking for overflow

Reverts are not detected by default by Medusa and Echidna, so to explicitly test for this we can use a try catch in our DoomsdayTargets.sol contract (this contract is meant for us to define things that should never happen in a system):

...

abstract contract DoomsdayTargets is
    BaseTargetFunctions,
    Properties
{
    /// Makes a handler have no side effects
    /// The fuzzer will call this anyway, and because it reverts it will be removed from shrinking
    /// Replace the "withGhosts" with "stateless" to make the code clean
    modifier stateless() {
        _;
        revert("stateless");
    }

    function doomsday_deposit_revert(uint256 amt) public stateless asActor {
        try points.deposit(amt) {} catch {
            t(false, "Should never revert");
        }
    }
}

The handler doomsday_deposit_revert is what we call a doomsday test, a property that should never fail as a failure indicates the system breaking in some way.

We use the stateless modifier to make it so that we don't need to track ghost variables for this test by undoing any state changes made by the function call.

This pattern is very useful if you want to perform extremely specific tests that would make your code more complex.

If we now run medusa fuzz we should get a broken property!

Debugging broken properties

The Chimera Framework is extremely opinionated, because we believe that reading Medusa and Echdina traces is a very slow and difficult way to debug broken properties.

That's why all of our templates come with the ability to reproduce broken properties as unit tests in Foundry.

So instead of debugging our broken property from the Medusa logs directly, we'll use Foundry:

  1. Copy the Medusa output logs in your terminal
  2. Go to the Medusa Log Scraper tool
  3. Paste the logs
  4. A reproducer unit test will be created for the broken property automatically
  5. Click the dropdown arrow to show the unit test
  6. Disable the vm.prank cheatcode by clicking the button (as we're overriding Medusa's behavior)
  7. Click on the clipboard icon to copy the reproducer

Medusa Repro

  1. Go to CryticToFoundry.sol
  2. Paste the reproducer unit test
  3. Run it with Foundry using the forge test --match-test test_doomsday_deposit_revert_0 -vvv command in the comment above it
// forge test --match-contract CryticToFoundry -vv
contract CryticToFoundry is Test, TargetFunctions, FoundryAsserts {
    function setUp() public {
        setup();
    }

    // forge test --match-test test_doomsday_deposit_revert_0 -vvv 
    function test_doomsday_deposit_revert_0() public {
        vm.roll(20125);
        vm.warp(424303);
        points_deposit(47847039802010376432191764575089043774271359955637698993445805766260571833418);
        
        vm.roll(51974);
        vm.warp(542538);
        doomsday_deposit_revert(71706648638691613974674094072029978422499381042277843030097252733530259068757);
    }
}

We now have a Foundry reproducer! This makes it much easier to debug because we can quickly test just the call sequence that causes the property to break and add logging statements wherever needed.

Testing for monotonicity

We can say that the Points contract's power should be monotonically increasing since there's no way to withdraw.

Let's prove this with a global property and ghost variables.

To keep things simple, let's we'll just test this property on the current actor (handled by the ActorManager).

Next go to the BeforeAfter contract and add a way to fetch the power for the deposited user before and after each call to the target function:

abstract contract BeforeAfter is Setup {
    struct Vars {
        uint256 power;
    }

    Vars internal _before;
    Vars internal _after;

    modifier updateGhosts {
        __before();
        _;
        __after();
    }

    function __before() internal {
        _before.power = points.power(_getActor());
    }

    function __after() internal {
        _after.power = points.power(_getActor());
    }
}

From this, we can specify the property in Properties contract:

abstract contract Properties is BeforeAfter, Asserts {
    function property_powerIsMonotonic() public {
        gte(_after.power, _before.power, "property_powerIsMonotonic");
    }
}

We don't expect this property to break, but you should still run the fuzzer to check. And interestingly, the fuzzer breaks the property.

I'll leave it to you as an exercise to figure out why!

Chimera Framework

The Chimera framework lets you run invariant tests with Echidna and Medusa that can be easily debugged using Foundry.

The framework is made up of the following files:

  • Setup.sol
  • TargetFunctions.sol
  • Properties.sol
  • CryticToFoundry.sol
  • BeforeAfter.sol
  • CryticTester.sol

When you build your handlers using Recon these files get automatically generated and populated for you. To use the framework in your project, you just need to download these files that get generated for you and add the Chimera dependency to your project: 

forge install Recon-Fuzz/chimera

The Contracts

We'll now look at the role each of the above contracts serve in building an extensible and maintainable fuzzing suite. We'll be looking at examples using the create-chimera-app template project.

Setup

This contract is used to deploy and initialize the state of your target contracts. It's called by the fuzzer before any of the target functions are called.

Any contracts you want to track in your fuzzing suite should live here.

In our create-chimera-app template project, the Setup contract is used to deploy the Counter contract:

abstract contract Setup is BaseSetup {
    Counter counter;

    function setup() internal virtual override {
        counter = new Counter();
    }
}

TargetFunctions

This is perhaps the most important file in your fuzzing suite, it defines the target function handlers that will be called by the fuzzer to manipulate the state of your target contracts.

Note: These are the only functions that will be called by the fuzzer.

Because these functions have the aim of changing the state of the target contract, they usually only include non-view and non-pure functions.

Target functions make calls to the target contracts deployed in the Setup contract. The handler that wraps the target function allows you to add clamping (reducing the possible fuzzed input values) before the call to the target contract and properties (assertions about the state of the target contract) after the call to the target contract.

In our create-chimera-app template project, the TargetFunctions contract is used to define the increment and setNumber functions:

abstract contract TargetFunctions is
    BaseTargetFunctions,
    Properties
{
    function counter_increment() public {
        counter.increment();
    }

    function counter_setNumber1(uint256 newNumber) public {
        // clamping can be added here before the call to the target contract
        // ex: newNumber = newNumber % 100;

        // example assertion test replicating testFuzz_SetNumber
        try counter.setNumber(newNumber) {
            if (newNumber != 0) {
                t(counter.number() == newNumber, "number != newNumber");
            }
        } catch {
            t(false, "setNumber reverts");
        }
    }

    function counter_setNumber2(uint256 newNumber) public {
        // same example assertion test as counter_setNumber1 using ghost variables
        __before();

        counter.setNumber(newNumber);

        __after();

        if (newNumber != 0) {
            t(_after.counter_number == newNumber, "number != newNumber");
        }
    }
}

Properties

This contract is used to define the properties that will be checked after the target functions are called.

At Recon our preference is to define these as Echidna/Medusa assertion properties but they can also be defined as boolean properties.

In our create-chimera-app template project, the Properties contract is used to define a property that states that the number can never be 0:

abstract contract Properties is BeforeAfter, Asserts {
    // example property test
    function invariant_number_never_zero() public {
        t(counter.number() != 0, "number is 0");
    }
}

CryticToFoundry

This contract is used to debug broken properties by converting the breaking call sequence from Echidna/Medusa into a Foundry unit test. When running jobs on Recon this is done automatically for all broken properties using the fuzzer logs.

If you are running the fuzzers locally you can use the Echidna and Medusa tools on Recon to convert the breaking call sequence from the logs into a Foundry unit test.

This contract is also useful for debugging issues related to the setup function and allows testing individual handlers in isolation to verify if they're working as expected for specific inputs.

In our create-chimera-app template project, the CryticToFoundry contract doesn't include any reproducer tests because all the properties pass.

The test_crytic function demonstrates the template for adding a reproducer test:

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

        targetContract(address(counter));
    }

    function test_crytic() public {
        // TODO: add failing property tests here for debugging
    }
}

BeforeAfter

This contract is used to store the state of the target contract before and after the target functions are called in a Vars struct.

These variables can be used in property definitions to check if function calls have modified the state of the target contract in an unexpected way.

In our create-chimera-app template project, the BeforeAfter contract is used to track the counter_number variable:

// ghost variables for tracking state variable values before and after function calls
abstract contract BeforeAfter is Setup {
    struct Vars {
        uint256 counter_number;
    }

    Vars internal _before;
    Vars internal _after;

    function __before() internal {
        _before.counter_number = counter.number();
    }

    function __after() internal {
        _after.counter_number = counter.number();
    }
}

CryticTester

This is the entrypoint for the fuzzer into the suite. All target functions will be called on an instance of this contract since it inherits from the TargetFunctions contract.

In our create-chimera-app template project, the CryticTester contract is used to call the counter_increment and counter_setNumber1 functions:

// echidna . --contract CryticTester --config echidna.yaml
// medusa fuzz
contract CryticTester is TargetFunctions, CryticAsserts {
    constructor() payable {
        setup();
    }
}

Assertions

When using assertions from Chimera in your properties, they use a different interface than the standard assertions from foundry's forge-std.

The following assertions are available in Chimera's Asserts contract:

abstract contract Asserts {
    // greater than
    function gt(uint256 a, uint256 b, string memory reason) internal virtual;

    // greater than or equal to
    function gte(uint256 a, uint256 b, string memory reason) internal virtual;

    // less than
    function lt(uint256 a, uint256 b, string memory reason) internal virtual;

    // less than or equal to
    function lte(uint256 a, uint256 b, string memory reason) internal virtual;

    // equal to
    function eq(uint256 a, uint256 b, string memory reason) internal virtual;

    // true
    function t(bool b, string memory reason) internal virtual;

    // between uint256
    function between(uint256 value, uint256 low, uint256 high) internal virtual returns (uint256);

    // between int256
    function between(int256 value, int256 low, int256 high) internal virtual returns (int256);

    // precondition
    function precondition(bool p) internal virtual;
}

Invariant Testing Bootcamp

The Invariant Testing Bootcamp at Home:

  • A 5 part online self-paced couse around writing Invariant Testing for Security

Advanced Fuzzing Tips

This is a compilation of best practices that the Recon team has developed while using the Chimera framework.

Target Functions

For each contract you want to fuzz (your target contract), select the state-changing functions (target functions) you want to include in your fuzzing suite. Wrap the function in a handler which passes in the input to the function call and allows the fuzzer to test random values. 

// contract to target
contract Counter {
       uint256 public number;

       function increment() public {
              number++;
       }
}

abstract contract TargetFunctions {
       // function handler that targets our contract of interest
       function counter_increment() public asActor {
              counter.increment();
       }
}

The easiest way to do this is with our Invariants Builder tool or with the Recon Extension directly in your code editor.

By using the asActor or asAdmin modifiers in combination with an Actor Manager ensures efficient fuzzing by not wasting tests that should be executed only by an admin getting executed by a non-admin actor. These modifiers prank the call to the target contract as the given actor, ensuring that the call is made with the actor as the msg.sender.

// contract to target
contract Yield {
       address admin;
       uint256 yield;

       modifier onlyAdmin() {
              require(msg.sender == admin);
       }

       function resetYield(address _newAdmin) public onlyAdmin {
              yield = 0;
       }
}

abstract contract TargetFunctions {
       // calling this as an actor would waste fuzz calls because it would always revert so we use the asAdmin modifier
       function yield_resetYield() public asAdmin {
              yield.resetYield();
       }
}

Clamping Target Functions

Clamping reduces the search space for the fuzzer, making it more likely that you'll explore interesting states in your system.

Clamped handlers should be a subset of all target functions by calling the unclamped handlers with the clamped inputs. This ensures that the fuzzer doesn't become overbiased, preventing it from exploring potentially interesting states, and also ensures checks for inlined properties which are implemented in the unclamped handlers are always performed. 


contract Counter {
    uint256 public number = 1;

    function setNumber(uint256 newNumber) public {
        if (newNumber != 0) {
            number = newNumber;
        }
    }
}

abstract contract TargetFunctions {
       function counter_setNumber(uint256 newNumber) public asActor {
              // unclamped handler explores the entire search space; allows the input to be 0
              counter.setNumber(newNumber);

              // inlined property check in the handler always gets executed
              if (newNumber != 0) {
                     t(counter.number == newNumber, "number != newNumber");
              }
       }

       function counter_setNumber_clamped(uint256 newNumber) public asActor {
              // clamping prevents the newNumber passed into setNumber from ever being 0
              newNumber = between(newNumber, 1, type(uint256).max);
              // clamped handler calls the unclamped handler
              counter_setNumber(newNumber);
       }
}

Disabling Target Functions

Certain state-changing functions in your target contract may not actually explore interesting state transitions and therefore waste calls made by the fuzzer which is why our ABI to invariants tool only scrapes functions from the targeted contract ABI that are non-view/pure. Other functions (generally admin privileged ones) introduce so many false positives into properties being tested (usually via things like contract upgrades or token sweeping functions) that it's better to ignore them. Doing so is perfectly okay even though it will reduce overall coverage of the targeted contracts.

To make sure it's understood by others looking at the test suite that you purposefully meant to ignore a function we tend to prefer commenting out the handler or including a alwaysRevert modifier that causes the handler to revert every time it's called by the fuzzer.

Setup

This section covers a few rules we've come to follow in our engagements regarding setting up invariant testing suites.

  1. Create your own test setup
  2. Keep the story clean
  3. State exploration and coverage
  4. Programmatic deployment
  5. Implicit clamping

Create Your Own Test Setup

If you're working on a codebase which you didn't originally develop, it's tempting to use the Foundry test setup that the developers used for their unit tests, however this can lead to introducing any of the biases present in the existing setup into the invariant testing suite.

We've found that it's best to create the simplest setup possible starting from scratch, where you only deploy the necessary contracts of interest and periphery contracts.

Periphery contracts can also often be mocked (see this section on how to automatically generate mocks using the Recon Extension) if their behavior is irrelevant to the contracts of interest. This further reduces complexity, making the suite more easily understood by collaborators and making it more likely you'll get full line coverage over the contracts of interest more quickly.

Keep The Story Clean

We call the "story" the view of the state changes made by a given call sequence in a tester. By maintaining only one state-changing operation per target function handler, it makes it much simpler to understand what's happening within a call sequence when a tool generates a reproducer that breaks a property that you've defined.

If you include multiple state-changing operations within a single handler it adds additional mental overhead when trying to debug a breaking call sequence because you not only need to identify which handler is the source of the issue, but the individual operation within the handler as well.

Take the following example of handlers defined for an ERC4626 vault:

       // having multiple state-changing operations in one handler makes it difficult to understand what's happening in the story
       function vault_deposit_and_redeem(uint256 assets) public asActor {
              uint256 sharesReceived = vault.deposit(assets);

              vault.redeem(sharesReceived);
       }

       // having separate target function handlers makes it easier to understand the logical flow that lead to a broken property in a reproducer call sequence
       function vault_deposit(uint256 assets) public asActor {
              uint256 sharesReceived = vault.deposit(assets);
       }

       function vault_redeem(uint256 assets) public asActor {
              uint256 sharesReceived = vault.deposit(assets);

              vault.redeem(sharesReceived);
       }

Although this is a simplified example we can see that maintaining separate handlers for each state-changing function makes our story much simpler to read.

If you need to perform multiple state-changing operations to test a given property, consider making the function stateless as discussed in the inlined fuzz properties section

State Exploration and Coverage

The most important aspect of invariant testing is what you actually test, and what you actually test is implied by the target functions you define in your test suite setup.

Some contracts, like oracles, may be too complex to fully model (e.g. having to reach a quorom of 3 signers to update the price) because they would add overhead in terms of function handlers that require specific clamping and test suite setup.

In these cases, mocking is preferred because it simplifies the process for the fuzzer to change return values (price in the case of the oracle example) or allow more straightforward interactions to be made by your targeted contracts (without requiring things like input validation on the mocked contract's side).

Mocking is a destructive operation because it causes a loss of information, but the simplification it provides leads fuzzing and formal verification tools to explore possible system states much faster.

Adding additional handlers for things like token donations (transfering/minting tokens directly to one of your targeted contracts) can allow you to explore interesting states that otherwise wouldn't be possible if you only had handlers for your contracts of interest.

Programmatic Deployment

Most developers tend to write static deployments for their test suites where specific contract are deployed with some default values.

However, this can lead to missing a vast amount of possible system states, some of which would be considered admin mistakes (because they're related to deployment configurations), others which are valid system configurations that are never tested with fixed deployment parameters.

This is why we now prefer using programmatic deployments because they allow us to use the randomness of the fuzzer to introduce randomness into the system configuration that's being tested against. Although programmatic deployments make running a suite slower (because the fuzzer needs to find a valid deployment configuration before achieving meaningful line coverage), they turn simple suites into multi-dimensional ones.

This is best understood with an example of a system designed to accept multiple tokens. With a static deployment you may end up testing tokens with 6 and 18 decimals (the two most common extremes). However, with a programmatic deployment, you can test many token configurations (say all tokens with 6-24 decimals) to ensure that your system works with all of them.

We've standardized these ideas around programmatic deployments in our Manager contracts.

Programmatic deployment consists of adding 4 general function types:

  • A deploy handler, which will deploy a new version of the target (e.g a token via _newAsset in the AssetManager)
  • A switchTo handler, to change the current target being used (e.g the _switchAsset function in the AssetManager)
  • A getCurrent internal function, to know which is the current active target (e.g the _getAsset function in the AssetManager)
  • A getAll internal function, to retrieve all deployments (e.g the _getAssets function in the AssetManager)

Using the pattern of managers can help you add multi-dimensionality to your test setup and make tracking deployed components simpler.

Implicit Clamping

Based on your deployments, configuration, and the target functions you expose, a subset of all possible system states will be reachable. This leads to what we call implicit clamping as the states not reachable by your test suite setup will obviously not be tested and therefore have a similar effect as if they were excluded via clamping.

Mapping out what behavior is and isn't possible given your suite setup can therefore be helpful for understanding the limitations of your suite.

With these limitations outlined, you can write properties that define what behaviors should and shouldn't be possible given your setup. Checking these properties with fuzzing or formal verification won't necessarily prove they're always true, simply that they're true for the setup you've created.

This tends to be the source of bugs that are missed with fuzzing, as ultimately you can only detect what you test and if your system isn't configured so that it can reach a certain state in which there's a bug, you won't ever be able to detect it.

Ghost Variables

Ghost variables are a supporting tool that allow you to track system state over time. These can then be used in properties to check if the state has evolved as expected.

In the Chimera Framework we've concretized our prefered method of tracking ghost variables using a BeforeAfter contract which exposes an updateGhosts modifier that allows you to cache the system state before and after a call to a given target function.

As a rule of thumb it's best to avoid computation in your updates to the ghost variables as it ends up adding addtional operations that need to be performed for each call executed by the fuzzer, slowing down fuzzing efficiency.

Do NOT put any assertions in your ghost variables and avoid any operation or call that may cause a revert. These cause all operations in the call sequence created by the fuzzer to be undone, leaving the fuzzer with a blindspot because it will be unable to reach certain valid states.

Overcomplicating ghost variables has the unfortunate side effect of making the coverage report look promising as it will show certain lines fully covered but in reality might be applying implicit clamping by causing reverts that prevent edge cases for certain properties being explored since an update that reverts before the property is checked will not generate a reproducer call sequence.

contract Counter {
    uint256 public number = 1;

    function setNumber(uint256 newNumber) public {
        if (newNumber != 0) {
            number = newNumber;
        }
    }
}

abstract contract TargetFunctions {
       // updateGhosts updates the ghost variables before and after the call to the target function
       function counter_setNumber1(uint256 newNumber) public updateGhosts asActor {
              counter.setNumber(newNumber);
       }
}

abstract contract BeforeAfter is Setup {
    struct Vars {
       uint256 counter_difference;
       uint256 counter_number;
    }

    Vars internal _before;
    Vars internal _after;

    modifier updateGhosts {
       __before();
       _;
       __after();
    }

    function __before() internal {
       // this line would revert for any value where the number before < the new number
       _before.counter_difference = _before.counter_number - counter.number();
    }

    function __after() internal {
       _after.counter_difference = _before.counter_number - counter.number();
    }
}

In the above example we can see that the __before() function would revert for any values where the newNumber passed into setNumber is greater than the value stored in _before.counter_number. This would still allow the coverage report to show the function as covered however because for all newNumber values less than or equal to _before.counter_number the update would succeed. This means that fundamentally we'd be limiting the search space of the fuzzer, preventing it from exploring any call sequences where newNumber is greater than the value stored in _before.counter_number and potentially missing bugs because of it.

Grouping Function Types

A simple pattern for grouping function types using ghost variables so they can easily be used as a precondition to a global property check is to group operations by their effects.

For example, you may have multiple deposit/mint operations that have the effect of "adding" and others of "removing".

You can group these effects using an enum type as follows:

enum OpType {
    GENERIC,
    ADD,
    REMOVE
}

modifier updateGhostsWithType(OpType op) {
       currentOperation = op;
       __before();
       _;
       __after();
}

modifier updateGhosts() {
       currentOperation = OpType.GENERIC;
       __before();
       _;
       __after();
}

And add the updateGhostsWithType modifier only to handlers which perform one of the operations of interest. All other handlers using the standard updateGhosts modifier will default to the GENERIC operation type so that you don't have to refactor any existing modifiers.

Now with the ability to elegantly track the current operation you can easily use the operation type to write a global property for it like so:

contract Counter {
       uint256 public number = 1;

       function increment() public {
              number++;
       }

       function decrement() public {
              number--;
       }
}

abstract contract TargetFunctions {
       // we set the respective operation type on our target function handlers
       function counter_increment() public updateGhostsWithType(OpType.INCREASE) asActor {
              counter.setNumber(newNumber);
       }

       function counter_increment() public updateGhostsWithType(OpType.DECREASE) asActor {
              counter.setNumber(newNumber);
       }
}

abstract contract BeforeAfter is Setup {
       enum OpType {
              INCREASE,
              DECREASE
       }

       struct Vars {
              uint256 counter_number;
       }

       Vars internal _before;
       Vars internal _after;

       modifier updateGhosts {
              __before();
              _;
              __after();
       }

       modifier updateGhostsWithType(OpType op) {
              currentOperation = op;
              __before();
              _;
              __after();
       }

       function __before() internal {
              _before.counter_number = counter.number();
       }

       function __after() internal {
              _after.counter_number = counter.number();
       }
}

abstract contract Properties is BeforeAfter, Asserts {
       function propert_number_decreases() public {
              // we can use the operation type as a precondition to a check in a global property
              if(currentOperation == OpType.DECREASE)
                     gte(_before.counter_number, _after.counter_number, "number does not decrease");
              }
       }
}

Inlined Fuzz Properties

Inlined properties allow you to make an assertion about the system state immediately after a given state-changing target function call:

contract Counter {
    uint256 public number = 1;

    function setNumber(uint256 newNumber) public {
       if (newNumber != 0) {
           number = newNumber;
       }
    }
}

abstract contract TargetFunctions
{
    function counter_setNumber(uint256 newNumber) public updateGhosts asActor {
       try counter.setNumber(newNumber) {
              // if the call to the target contract was successful, we make an assertion about the expected system state after
              if (newNumber != 0) {
                     t(counter.number() == newNumber, "number != newNumber");
              }
       }
    }
}

Repeating the same inlined property in multiple places should be avoided whenever possible.

Implementing the same inlined property in multiple places is essentially asking the fuzzer to break the property, not change the state (as an assertion failure prevents the call to the handler from completing), then to break the same property in a different way via another handler while already knowing that the property breaks. This is a waste of computational resources as you're asking the fuzzer to prove a fact that you already know instead of asking it to prove a new fact for which you're not sure if there's a proof (in the sense of a broken property, not a mathematical proof) or not.

If you find yourself implementing the same inline property multiple times, you should refactor them to only be assessed in one handler or checked as a global property using ghost variables.

If you can only implement a property as an inlined test but don't want multiple state changes to be maintained as it would make the story difficult to read, you can make your handler stateless using a stateless modifier. 

modifier stateless() {
       _;
       // the revert is only made after the handler function execution completes
       revert("stateless")
}

This causes the handler to revert only at the end of execution, meaning any coverage exploration will be maintained and any assertion failures will happen before the revert.

Exploring Rounding Errors

Fuzzing is a particularly useful technique for finding precision loss related issues, as highlighted by @DevDacian in this blog post.

Simply put the approach for finding such issues is as follows. For any place where there is a division operation which you believe may lead to potential loss of precision:

  • Start by using and exact check in a property assertion to check if the return value of a variable/function is as expected.
  • Run the fuzzer and allow it to find a case where the return value is not what's expected via a falsified assertion.
  • Create an Echidna optimization test to increase the difference with the expected value.

The results of the optimization run will allow you to determine the severity of any potential precision loss and how it may be used as part of an exploit path.

Opsec Resources

These are a few resources, stemming from this talk we did to help founders ship safely: https://docs.google.com/presentation/d/1Tzcj7FPj8QmvjdO79vPqPsRxyyyEwFhWl6SoRzFZ_do/edit?usp=sharing

1 Hour Consultation

Recon offers ongoing security retainers to review multisig operations and transactions, to see if it's a fit and get some free advice, get in touch here: https://tally.so/r/3jpV6E

Smart Contracts

Governance

Web2

Physical Opsec

List of most known Physical Attacks tied to Crypto: https://github.com/jlopp/physical-bitcoin-attacks

Recon Extension

The Recon extension is a Visual Studio Code extension that allows you to use Recon's suite of tools directly in your code editor. It requires a Foundry project to be open in your workspace to use.

Getting Started

After installing the extension, your project will automatically be compiled when you open a new window in your code editor.

If your foundry.toml file is located in a directory other than the root of your project, your project will not be compiled automatically. You can select the location in the sidebar under the RECON COCKPIT section:

image

which will allow you to build your project from the directory containing the foundry.toml file.

Scaffold Your Target Functions

After building your project, you can choose which of your contract functions you want to add target functions for using the CONTRACTS section in the sidebar.

Contracts Section

Once you've selected the contract functions you'd like to scaffold, you can generate a Chimera Framework template for your project using the Scaffold button in the sidebar under the RECON COCKPIT section:

Scaffold

This will install the Chimera dependency, generate the necessary fuzzer config files, and generate all the necessary test files for your project using the Create Chimera App template.

Your scaffolded target functions will be added to the recon/targets directory as ContractName + TargetFunctions.sol (e.g. Counter.sol's target functions will be called CounterTargetFunctions.sol).

Note: You can change settings for the project build configurations by clicking the gear icon next to the Generate Chimera Template button. This allows you to change the Echidna and Medusa configuration files as well as the project settings.

For more on how to use the Chimera Framework, check out the Chimera Framework section.

Function Handlers

Testing Modes

When selecting which contract functions you'd like to target, you can select from three testing modes to help define how you'd like to test your target functions:

Testing Mode

  • Normal Mode - This just adds a handler function as a wrapper around the underlying target function.
  • Fail Mode - This will add a handler function that includes an assertion at the end of the call to the target function. You can replace this assertion with any other assertion you'd like to test.
  • Catch Mode - This will add a handler function that includes a try catch block around the call to the target function. You can add any custom logic to the catch block such as an assertion about when a function should or shouldn't revert.

The testing mode for each target function can later be changed in the generated target function contract above each function using the codelense buttons:

Testing Modes Codelense

Actor Mode

Actor modes allow you to specify which actor should be calling the target function:

Actor Mode

  • Actor - This uses the currently set actor returned by _getActor() to prank and call the target function.
  • Admin - This uses the admin role to call the target function (this is defaulted to address(this)).

The actor mode for each target function can later be changed in the generated target function contract above each function using the codelense buttons:

Actor Mode Codelense

Auto Mocking

The Recon extension allows you to auto-mock specific contracts needed for your setup using the ABI to Mock tool. This tool will generate a mock of system contracts based on the contract's parameters and return values. This is useful for quickly getting coverage on the core contracts of your project that you target with your target functions while simulating functionality of periphery contracts whose behavior is unimportants.

Auto Mocking Section

Auto Mocking is triggered by right clicking on a contract's ABI file in the out directory or directly via the Contract file of the contract you'd like to mock and selecting Generate Solidity Mock. This will generate a mock of the contract in the path specified in the RECON COCKPIT settings in the Mocks Folder Path field as ContractName + Mocks.sol (e.g. Counter.sol's mocks will be called CounterMocks.sol).

Mocks Folder Path

Run with Echidna and Medusa

After generating a Chimera template for your project you can use the Run Echidna and Run Medusa buttons in the bar at the bottom of your code editor to run your suite with Echidna and Medusa.

Run Fuzzer Buttons

Report Generation

After running your suite with Echidna or Medusa a report is automatically generated which you can see in the COVERAGE REPORT section in the sidebar.

Coverage Report Section

This provides an markdown report of all the properties that were tested and the results.

Recon Report

You can also view a condensed version of the coverage report which removes contracts that aren't touched by the fuzzer by clicking the open in new tab button in the report section.

Recon Compressed Coverage

Reproducer Generation

If a property breaks, the extension will automatically generate a Foundry unit test reproducer for the property.

Prompt Repro

Clicking yes will add the reproducer to the CryticToFoundry contract that's created when you generate a Chimera template.

Crytic To Foundry

The Recon extension also provides a codelense utility for running the Foundry reproducer unit test above the function via the Run Test button. Run Tests

Coverage Report Compressor

  • Right click on the coverage report and select "Clean Up Coverage Report"
  • This will compress the report by removing contracts not touched by the fuzzer from the coverage report

Display coverage report as overlay with coverage gutters

  • To do this you just need to have the coverage gutters extension installed and click the report in the COVERAGE REPORT section
  • This will display the coverage report as an overlay using coverage gutters
  • To remove the coverage gutters you can click the File Uncovered button on the bottom of your VS code window

Coverage Gutters

Medusa Log Scraper

Medusa Logs Scraper

Usage

  1. Paste your Medusa logs generated at the end of your test run
  2. All function calls will be scraped automatically from the pasted logs
  3. Each property will generate a Foundry reproducer unit test
  4. Toggle cheatcodes as needed

Echidna Log Scraper

Echidna Logs Parser

Usage

  1. Paste your Echidna logs generated at the end of your test run
  2. All function calls will be scraped automatically from the pasted logs
  3. Each property will generate a Foundry reproducer unit test
  4. Toggle cheatcodes as needed

Invariants Builder

Builder

Scaffold an Invariant Testing suite in seconds!

Usage

  • Paste your contract's ABI (available in the out/ directory after building your contracts using Foundry)
  • Add the name of your pasted contract's ABI in the "Your_Contract" form field
  • Download the generated contracts into your repo using the "Download All Files" button
  • Follow the instructions in the "Installation Help" section for the next steps after you've added the files to your repo

Bytecode Compare

Bytecode Comparison Tool

Usage

  1. Paste 2 contract bytecodes
  2. Use the "Compare" button to generate a diff between them, optionally ignoring metadata

Bytecode To Interface

Bytecode to Interface Tool

Usage

  1. Add a contract's bytecode: a. Using an rpc-url and contract address b. By pasting the bytecode directly
  2. Define an interface name to give your contract in the "Interface Name" form field
  3. Use the "Generate Interface" button to generate a Solidity interface for the given bytecode

Chimera

Chimera is a smart contract property-based testing framework. Write once, run everywhere.

Supports invariant tests written for:

  • Foundry
  • Echidna
  • Medusa
  • Halmos

Installation

forge install Recon-Fuzz/chimera

Motivation

When writing property-based tests, developers commonly face several issues:

  • the amount of boilerplate code required
  • the challenge of switching tools after the initial setup
  • the difficulty in sharing results between different tools

Writing invariant tests that work seamlessly with Foundry, Echidna, Medusa, and Halmos is not straightforward.

Chimera addresses this problem by enabling a "write once, run everywhere" approach.

Limitations

Chimera currently only supports cheatcodes implemented by HEVM.

Foundry has extended these and offers functionality not supported by the HEVM cheatcodes, subsequently these must be accounted for when adding Chimera to a Foundry project as they will cause issues when running Echidna and Medusa. If adding Chimera to an existing Foundry project ensure that there are no cheatcodes implemented that aren't supported by HEVM as they will throw the following error: VM failed for unhandled reason, BadCheatCode <cheatcode hash>.

While medusa supports etch, echidna does not support it yet. Please note when using etch in an echidna environment it will not work as expected.

Create Chimera App

A Foundry template that allows you to bootstrap an invariant fuzz testing suite the Chimera Framework that works out of the box with:

  • Foundry for invariant testing and debugging of broken property reproducers
  • Echidna and Medusa for stateful fuzzing
  • Halmos for invariant testing

It extends the default Foundry template used when running forge init to include example property tests supported by Echidna and Medusa.

Prerequisites

To use this template you'll need to have Foundry installed and at least one fuzzer (Echidna or Medusa):

Usage

To initialize a new Foundry repo using this template run the following command in the terminal.

forge init --template https://github.com/Recon-Fuzz/create-chimera-app

Build

This template is configured to use Foundry as it's build system for Echidna and Medusa so after making any changes the project must successfully compile using the following command before running either fuzzer:

forge build

Property Testing

This template comes with property tests defined for the Counter contract in the Properties contract and in the function handlers in the TargetFunctions contract.

Echidna Property Testing

To locally test properties using Echidna, run the following command in your terminal:

echidna . --contract CryticTester --config echidna.yaml

Medusa Property Testing

To locally test properties using Medusa, run the following command in your terminal:

medusa fuzz

Foundry Testing

Broken properties found when running Echidna and/or Medusa can be turned into unit tests for easier debugging with Recon (for Echidna/for Medusa) and added to the CryticToFoundry contract.

forge test --match-contract CryticToFoundry -vv

Halmos Invariant Testing

The template works out of the box with Halmos, however Halmos Invariant Testing is currently in preview

Simply run halmos on the root of this repository to run Halmos for Invariant Testing

Expanding Target Functions

After you've added new contracts in the src directory, they can then be deployed in the Setup contract.

The ABIs of these contracts can be taken from the out directory and added to Recon's Invariants Builder. The target functions that the sandbox generates can then be added to the existing TargetFunctions contract.

Log Parser

A TypeScript package to convert Medusa and Echidna traces into Foundry reproducer unit tests.

Available in an easy to use UI in our:

NPM

npm

Installation

yarn add @recon-fuzz/log-parser

Usage

import { processLogs, Fuzzer } from '@recon-fuzz/log-parser';

// Process Medusa logs
const medusaResults = processLogs(medusaLogContent, Fuzzer.MEDUSA);

// Process Echidna logs
const echidnaResults = processLogs(echidnaLogContent, Fuzzer.ECHIDNA);

API Reference

processLogs(logs: string, tool: Fuzzer): FuzzingResults

Processes fuzzing logs and returns structured results.

Parameters

  • logs: string - The raw log content as a string
  • tool: Fuzzer - The fuzzer tool used (Fuzzer.MEDUSA or Fuzzer.ECHIDNA)

Returns: FuzzingResults

interface FuzzingResults {
  duration: string;
  coverage: number;
  failed: number;
  passed: number;
  results: any[];
  traces: any[];
  brokenProperties: any[];
  numberOfTests: number;
}

Medusa and Echidna Conversion to Foundry

Converting Fuzzer Logs to Foundry Tests

Both Medusa and Echidna logs can be converted into Foundry test cases using the provided utility functions:

// For Echidna logs
import { echidnaLogsToFunctions } from '@recon-fuzz/log-parser';

const foundryTest = echidnaLogsToFunctions(
  echidnaLogs,
  "test_identifier",
  "brokenProperty",
  { roll: true, time: true, prank: true }
);

// For Medusa logs
import { medusaLogsToFunctions } from '@recon-fuzz/log-parser';

const foundryTest = medusaLogsToFunctions(
  medusaLogs,
  "test_identifier",
  { roll: true, time: true, prank: true }
);

The conversion handles:

  • VM state manipulation (block numbers, timestamps)
  • Actor simulation (pranks for different senders)
  • Function call sequences
  • Special data types (addresses, bytes)

Generated tests will include the exact sequence of calls that triggered the property violation, making it easy to reproduce and debug issues found during fuzzing.

ABI to Invariants

NOTE: This repo is private, it's coming soon!

Given a contract ABI and options it creates:

Available in an easy to use UI in our Invariants Builder

ABI to Mock

Given an ABI file generate a mock contract with functions that allow setting the return value of all view functions.

The simplest form of mocking that generates contracts that can be easily integrated into a fuzz testing suite.

Works well with the Recon Extension (coming soon) and the ABI to Invariants Builder.

Features

  • Generates fully functional Solidity mock contracts
  • Supports complex data types including structs and nested arrays
  • Maintains function signatures and event definitions
  • Customizable contract names and output locations
  • Available as both a CLI tool and JavaScript library

Generated Mock Features

  • Complete function signatures matching the original contract
  • Setter functions for return values
  • Complex type support (structs, arrays, mappings)

Installation

npm install abi-to-mock

Usage

Command Line Interface

npx abi-to-mock <abi-file> [options]

Options:
  --out, -o   Output directory (default: "./out")
  --name, -n  Contract name (default: "Contract")

Example:

npx abi-to-mock ./MyContract.json --out ./mocks --name MyContract

Using with Foundry

forge build

npx abi-to-mock out/ERC20Mock.sol/ERC20Mock.json --name Erc20Mock --out src/

Programmatic Usage

// Node.js
const AbiToMock = require('abi-to-mock');
// or ES Modules
import AbiToMock from 'abi-to-mock';

// From file
AbiToMock('./MyContract.json', './mocks', 'MyContract');

// From ABI object
const abi = [
  {
    "inputs": [],
    "name": "getValue",
    "outputs": [{"type": "uint256"}],
    "type": "function"
  }
];
AbiToMock.generateMock(abi, './mocks', 'MyContract');

// Browser usage
import { generateMockString } from 'abi-to-mock';
const mockCode = generateMockString(abi, 'MyContract');

API Reference

// Node.js API
AbiToMock(abiPath: string, outputDir?: string, name?: string): MockContract
AbiToMock.generateMock(abi: ABI[], outputDir: string, name: string): MockContract

// Browser API
generateMockString(abi: ABI[], name: string): string

Setup Helpers

These contracts were created with the intention of speeding up the setup process for an invariant testing suite.

For an example implementation of these contracts in use see the create-chimera-app repo.

ActorManager

The ActorManager contract serves as the source of truth for actors that are being used in the fuzzing suite setup.

The primary functions of interest when setting up a suite are:

  • _addActor - allows adding a new address as an actor that can be tracked
  • _switchActor - this should be exposed in a target function that can be called by the fuzzer to randomly switch between actors

To use the actors stored in the ActorManager, add the asActor modifier on all of your target function handlers which pranks as the currently set actor.

For privileged functions you can use the asAdmin modifier which calls the target functions as the tester contract (address(this)). The tester contract is typically set as the default admin address by convention.

AssetManager

The AssetManager allows tracking all assets being used in the fuzz suite setup. Similar to the ActorManager this serves as the source of truth for all assets used in the test suite and therefore no target function should be called that may transfer an asset not tracked in the AssetManager.

The primary functions of interest when setting up a suite are:

  • _newAsset - deploys an instance of the MockERC20 contract and adds it to tracking so it can be accessed as needed
  • _getAsset - used to clamp values used for tokens in calls to target functions
  • _finalizeAssetDeployment - a utility for minting tokens added via _newAsset to all actors that have been setup and approving it to all contracts in the the system that may need to call transferFrom on it

Utils

Provides utilities for invariant testing

  • checkError - allows checking if a revert reason from a function call is equivalent to the reason passed in as the expected argument

Panic

A library that provides named variables corresponding to compiler panic messages. Used to more easily access these messages when using the checkError utility.

library Panic {
    // compiler panics
    string constant assertionPanic = "Panic(1)";
    string constant arithmeticPanic = "Panic(17)";
    string constant divisionPanic = "Panic(18)";
    string constant enumPanic = "Panic(33)";
    string constant arrayPanic = "Panic(34)";
    string constant emptyArrayPanic = "Panic(49)";
    string constant outOfBoundsPanic = "Panic(50)";
    string constant memoryPanic = "Panic(65)";
    string constant functionPanic = "Panic(81)";
}

MockERC20

A minimal MockERC20 contract that lets you mock any standard ERC20 tokens that will be interacting with the system without requiring external dependencies.

Properties Table

Properties Table

This repo provides a template for creating a table to track properties that have been implemented for an invariant testing suite using the format that the Recon team uses in our engagements.

Examples

The following are examples of the use of this table for Recon engagements:

ERC7540 Reusable Properties

A collection of reusable properties for ERC-7540 asynchronous vaults.

Written in collaboration with Centrifuge.

Specification

PropertyDescriptionCategory
7540-1convertToAssets(totalSupply) == totalAssets unless price is 0.0High Level
7540-2convertToShares(totalAssets) == totalSupply unless price is 0.0High Level
7540-3max* never revertsDOS Invariant
7540-4claiming more than max always revertsStateful Test
7540-5requestRedeem reverts if the share balance is less than amountStateful Test
7540-6preview* always revertsStateful Test
7540-7if max[method] > 0, then [method] (max) should not revertDOS Invariant

Usage

  1. Install the repo as a dependency to a Foundry project
forge install Recon-Fuzz/erc7540-reusable-properties --no-commit
  1. Inherit from the ERC7540Properties contract in the contract where you've defined your properties. For a test suite harnessed with Recon it will look something like this: 
abstract contract Properties is Setup, Asserts, ERC7540Properties {}
  1. Add a way to change the actor state variable in the ERC7540Properties contract. The simplest way to do this is by exposing a target function with something like the following implementation: 
    function setup_switchActor(uint8 actorIndex) public {
        actor = actorsArray[actorIndex % actorsArray.length];
    }
  1. The properties defined in the ERC7540Properties contract are meant to hold for a vault implementation conforming to the ERC specification. If your implementation doesn't require certain properties to hold you can simply exclude them from your contract in which you define your properties:
abstract contract Properties is Setup, Asserts, ERC7540Properties {
    function crytic_erc7540_1() public returns (bool test) {
        test = erc7540_1(address(vault));
    }

    function crytic_erc7540_2() public returns (bool test) {
        test = erc7540_2(address(vault));
    }
}

by not adding a wrapper for properties other than erc7540_2 and erc7540_2 the other properties defined in ERC7540Properties don't get evaluated by the fuzzer.

Glossary

Actor

The address that will perform the calls specific to TargetFunctions. See ActorManager for how to use these in a test suite.

CryticTester

The invariant testing contract that's deployed in the Chimera Framework and that the fuzzer will use to explore state and properties with the target functions defined on it.

CryticToFoundry

A Foundry test contract used to implement unit tests of property breaking call sequences (reproducers) obtained with testing tools (i.e. Echidna, Medusa, Halmos, etc.).

Invariant Testing

The act of testing logical statements about smart contracts using tools that manipulate their state randomly (fuzzers) or following all possible paths (formal verifiers).

Property

A logical statement about a smart contract or system that can be tested.

Reproducer

A call trace generated by a tool (fuzzer, formal verifier) that breaks a property of a contract or system.

Invariant

A property that should always hold for a smart contract or system.

Fuzzer

An engine/solver, a program that can perform stateful tests on a smart contract or system.

Some fuzzes are concrete, others concolyc, and others symbolic.

Handler

A wrapper around a target function that makes a call to a target contract.

Target Function

The set of functions that the fuzzer will call to explore state and properties for the smart contract or system.

Scaffolding

The set of smart contracts put into place to organize the code and tell the fuzzer how to explore states and test properties.

Echidna

A concrete fuzzer written in Haskell, using HEVM as its EVM engine

Medusa

A concrete fuzzer written in Go, using GETH for the EVM engine.

Halmos

A symbolic fuzzer written in Python, using its own SEVM for the EVM engine