Table of contents
Properties
- Testing the properties with fuzzing
- Additional resources
Helper functions
- Usage examples
HEVM cheat codes support
- Usage example
How to contribute to this repo?

Properties

This repository contains 168 code properties for:

ERC20 token: mintable, burnable, pausable and transferable invariants (25 properties).
ERC4626 vaults: strict specification and additional security invariants (37 properties).
ABDKMath64x64 fixed-point library invariants (106 properties).

The goals of these properties are to:

Detect vulnerabilities
Ensure adherence to relevant standards
Provide educational guidance for writing invariants

The properties can be used through unit tests or through fuzzing with Echidna.

Testing the properties with fuzzing

Install Echidna.
Import the properties into to your project:
- In case of using Hardhat, use: npm install https://github.com/crytic/properties.git or yarn add https://github.com/crytic/properties.git
- In case of using Foundry, use: forge install crytic/properties
According to tests required, go the the specific sections:

ERC20 tests

To test an ERC20 token, follow these steps:

Integration
Configuration
Run

You can see the output for a compliant token, and non compliant token.

Integration

Decide if you want to do internal or external testing. Both approaches have advantanges and disadvantages, you can check more information about them here.

For internal testing, create a new Solidity file containing the CryticERC20InternalHarness contract. USER1, USER2 and USER3 constants are initialized by default in PropertiesConstants contract to be the addresses from where echidna sends transactions, and INITIAL_BALANCE is by default 1000e18:

pragma solidity ^0.8.0;
import "@crytic/properties/contracts/ERC20/internal/properties/ERC20BasicProperties.sol";
import "./MyToken.sol";
contract CryticERC20InternalHarness is MyToken, CryticERC20BasicProperties {

    constructor() {
        // Setup balances for USER1, USER2 and USER3:
        _mint(USER1, INITIAL_BALANCE);
        _mint(USER2, INITIAL_BALANCE);
        _mint(USER3, INITIAL_BALANCE);
        // Setup total supply:
        initialSupply = totalSupply();
    }
}

For external testing, create two contracts: the CryticERC20ExternalHarness and the TokenMock as shown below. In the CryticERC20ExternalHarness contract you can specify which properties to test, via inheritance. In the TokenMock contract, you will need to modify the isMintableOrBurnable variable if your contract is able to mint or burn tokens.

pragma solidity ^0.8.0;
import "./MyToken.sol";
import {ICryticTokenMock} from "@crytic/properties/contracts/ERC20/external/util/ITokenMock.sol";
import {CryticERC20ExternalBasicProperties} from "@crytic/properties/contracts/ERC20/external/properties/ERC20ExternalBasicProperties.sol";
import {PropertiesConstants} from "@crytic/properties/contracts/util/PropertiesConstants.sol";


contract CryticERC20ExternalHarness is CryticERC20ExternalBasicProperties {   
    constructor() {
        // Deploy ERC20
        token = ICryticTokenMock(address(new CryticTokenMock()));
    }
}

contract CryticTokenMock is MyToken, PropertiesConstants {

    bool public isMintableOrBurnable;
    uint256 public initialSupply;
    constructor () {
        _mint(USER1, INITIAL_BALANCE);
        _mint(USER2, INITIAL_BALANCE);
        _mint(USER3, INITIAL_BALANCE);
        _mint(msg.sender, INITIAL_BALANCE);

        initialSupply = totalSupply();
        isMintableOrBurnable = true;
    }
}

Configuration

Create the following Echidna config file

corpusDir: "tests/crytic/erc20/echidna-corpus-internal"
testMode: assertion
testLimit: 100000
deployer: "0x10000"
sender: ["0x10000", "0x20000", "0x30000"]

If you're using external testing, you will also need to specify:

multi-abi: true

To perform more than one test, save the files with a descriptive path, to identify what test each file or corpus belongs to. For these examples, we use tests/crytic/erc20/echidna-internal.yaml and tests/crytic/erc20/echidna-external.yaml for the Echidna tests for ERC20. We recommended to modify the corpusDir for external tests accordingly.

The above configuration will start Echidna in assertion mode. Contract will be deployed from address 0x10000, and transactions will be sent from the owner and two different users (0x20000 and 0x30000). There is an initial limit of 100000 tests, but depending on the token code complexity, this can be increased. Finally, once Echidna finishes the fuzzing campaign, corpus and coverage results will be available in the tests/crytic/erc20/echidna-corpus-internal directory.

Run

Run Echidna:

For internal testing: echidna-test . --contract CryticERC20InternalHarness --config tests/crytic/erc20/echidna-internal.yaml
For external testing: echidna-test . --contract CryticERC20ExternalHarness --config tests/crytic/erc20/echidna-external.yaml

Finally, inspect the coverage report in tests/crytic/erc20/echidna-corpus-internal or tests/crytic/erc20/echidna-corpus-external when it finishes.

Example: Output for a compliant token

If the token under test is compliant and no properties will fail during fuzzing, the Echidna output should be similar to the screen below:

$ echidna-test . --contract CryticERC20InternalHarness --config tests/echidna.config.yaml 
Loaded total of 23 transactions from corpus/coverage
Analyzing contract: contracts/ERC20/CryticERC20InternalHarness.sol:CryticERC20InternalHarness
name():  passed! 🎉
test_ERC20_transferFromAndBurn():  passed! 🎉
approve(address,uint256):  passed! 🎉
test_ERC20_userBalanceNotHigherThanSupply():  passed! 🎉
totalSupply():  passed! 🎉
...

Example: Output for a non-compliant token

For this example, the ExampleToken's approval function was modified to perform no action:

function approve(address spender, uint256 amount) public virtual override(ERC20) returns (bool) {
  // do nothing
  return true;
}

In this case, the Echidna output should be similar to the screen below, notice that all functions that rely on approve() to work correctly will have their assertions broken, and will report the situation.

$ echidna-test . --contract CryticERC20ExternalHarness --config tests/echidna.config.yaml
Loaded total of 25 transactions from corpus/coverage
Analyzing contract: contracts/ERC20/CryticERC20ExternalHarness.sol:CryticERC20ExternalHarness
name():  passed! 🎉
test_ERC20_transferFromAndBurn():  passed! 🎉
approve(address,uint256):  passed! 🎉
...
test_ERC20_setAllowance(): failed!💥  
  Call sequence:
    test_ERC20_setAllowance()

Event sequence: Panic(1), AssertEqFail("Equal assertion failed. Message: Failed to set allowance") from: ERC20PropertyTests@0x00a329c0648769A73afAc7F9381E08FB43dBEA72
...

ERC4626 Tests

To test an ERC4626 token, follow these steps:

Integration
Configuration
Run

Integration

Create a new Solidity file containing the CryticERC4626Harness contract. Make sure it properly initializes your ERC4626 vault with a test token (TestERC20Token):

If you are using Hardhat:

    import {CryticERC4626PropertyTests} from "@crytic/properties/contracts/ERC4626/ERC4626PropertyTests.sol";
    // this token _must_ be the vault's underlying asset
    import {TestERC20Token} from "@crytic/properties/contracts/ERC4626/util/TestERC20Token.sol";
    // change to your vault implementation
    import "./Basic4626Impl.sol";

    contract CryticERC4626Harness is CryticERC4626PropertyTests {
        constructor () {
            TestERC20Token _asset = new TestERC20Token("Test Token", "TT", 18);
            Basic4626Impl _vault = new Basic4626Impl(_asset);
            initialize(address(_vault), address(_asset), false);
        }
    }

If you are using Foundry:

    import {CryticERC4626PropertyTests} from "properties/ERC4626/ERC4626PropertyTests.sol";
    // this token _must_ be the vault's underlying asset
    import {TestERC20Token} from "properties/ERC4626/util/TestERC20Token.sol";
    // change to your vault implementation
    import "../src/Basic4626Impl.sol";

    contract CryticERC4626Harness is CryticERC4626PropertyTests {
        constructor () {
            TestERC20Token _asset = new TestERC20Token("Test Token", "TT", 18);
            Basic4626Impl _vault = new Basic4626Impl(_asset);
            initialize(address(_vault), address(_asset), false);
        }
    }

Configuration

Create a minimal Echidna config file (e.g. tests/echidna.config.yaml)

corpusDir: "tests/echidna-corpus"
testMode: assertion
testLimit: 100000
deployer: "0x10000"
sender: ["0x10000"]

Run

Run the test suite using echidna-test . --contract CryticERC4626Harness --config tests/echidna.config.yaml and inspect the coverage report in tests/echidna-corpus when it finishes.

Example repositories are available for Hardhat and Foundry.

Once things are up and running, consider adding internal testing methods to your Vault ABI to allow testing special edge case properties like rounding. For more info, see the ERC4626 readme.

ABDKMath64x64 tests

The Solidity smart contract programming language does not have any inbuilt feature for working with decimal numbers, so for contracts dealing with non-integer values, a third party solution is needed. ABDKMath64x64 is a fixed-point arithmetic Solidity library that operates on 64.64-bit numbers.

A 64.64-bit fixed-point number is a data type that consists of a sign bit, a 63-bit integer part, and a 64bit decimal part. Since there is no direct support for fractional numbers in the EVM, the underlying data type that stores the values is a 128-bit signed integer.

ABDKMath64x64 library implements 19 arithmetic operations using fixed-point numbers and 6 conversion functions between integer types and fixed-point types.

We provide a number of tests related with fundamental mathematical properties of the floating point numbers. To include these tests into your repository, follow these steps:

Integration
Run

Integration

Create a new Solidity file containing the ABDKMath64x64Harness contract:

pragma solidity ^0.8.0;
import "@crytic/properties/contracts/Math/ABDKMath64x64/ABDKMath64x64PropertyTests.sol;

contract CryticABDKMath64x64Harness is CryticABDKMath64x64PropertyTests {
    /* Any additional test can be added here */
}

Run

Run the test suite using echidna-test . --contract CryticABDKMath64x64Harness --seq-len 1 --test-mode assertion --corpus-dir tests/echidna-corpus and inspect the coverage report in tests/echidna-corpus when it finishes.

Additional resources

Building secure contracts
Our EmpireSlacking slack server, channel #ethereum
Watch our fuzzing workshop

Helper functions

The repository provides a collection of functions and events meant to simplify the debugging and testing of assertions in Echidna. Commonly used functions, such as integer clamping or logging for different types are available in contracts/util/PropertiesHelper.sol.

Available helpers:

LogXxx: Events that can be used to log values in fuzzing tests. string, uint256 and address loggers are provided. In Echidna's assertion mode, when an assertion violation is detected, all events emitted in the call sequence are printed.
assertXxx: Asserts that a condition is met, logging violations. Assertions for equality, non-equality, greater-than, greater-than-or-equal, less-than and less-than-or-equal comparisons are provided, and user-provided messages are supported for logging.
clampXxx: Limits an int256 or uint256 to a certain range. Clamps for less-than, less-than-or-equal, greater-than, greater-than-or-equal, and range are provided.

Usage examples

Logging

Log a value for debugging. When the assertion is violated, the value of someValue will be printed:

pragma solidity ^0.8.0;

import "@crytic/properties/contracts/util/PropertiesHelper.sol";

contract TestProperties is PropertiesAsserts {
    
    // ...

    function test_some_invariant(uint256 someValue) public {
        // ...

        LogUint256("someValue is: ", someValue);

        // ...

        assert(fail);

        // ...
    }

    // ...

}

Assertions

Assert equality, and log violations:

pragma solidity ^0.8.0;

import "@crytic/properties/contracts/util/PropertiesHelper.sol";

contract TestProperties is PropertiesAsserts {
    
    // ...

    function test_some_invariant(uint256 someValue) public {
        // ...

        assertEq(someValue, 25, "someValue doesn't have the correct value");

        // ...
    }

    // ...

}

In case this assertion fails, for example if someValue is 30, the following will be printed in Echidna:

Invalid: 30!=25, reason: someValue doesn't have the correct value

Clamping

Assure that a function's fuzzed parameter is in a certain range:

pragma solidity ^0.8.0;

import "@crytic/properties/contracts/util/PropertiesHelper.sol";

contract TestProperties is PropertiesAsserts {

    int256 constant MAX_VALUE = 2**160;
    int256 constant MIN_VALUE = -2**24;
    
    // ...

    function test_some_invariant(int256 someValue) public {
        someValue = clampBetween(someValue, MIN_VALUE, MAX_VALUE);

        // ...
    }

    // ...

}

HEVM cheat codes support

Since version 2.0.5, Echidna supports HEVM cheat codes. This repository contains a Hevm.sol contract that exposes cheat codes for easy integration into contracts under test.

Cheat codes should be used with care, since they can alter the execution environment in ways that are not expected, and may introduce false positives or false negatives.

Usage example

Use prank to simulate a call from a different msg.sender:

pragma solidity ^0.8.0;

import "@crytic/properties/contracts/util/Hevm.sol";

contract TestProperties {
    
    // ...

    function test_some_invariant(uint256 someValue) public {
        // ...

        hevm.prank(newSender);
        otherContract.someFunction(someValue);  // This call's msg.sender will be newSender
        otherContract.someFunction(someValue);  // This call's msg.sender will be address(this)

        // ...
    }

    // ...

}

How to contribute to this repo?

Contributions are welcome! You can read more about the contribution guidelines and directory structure in the CONTRIBUTING.md file.

aviggiano/properties

Table of contents

Properties

Testing the properties with fuzzing

ERC20 tests

Integration

Configuration

Run

Example: Output for a compliant token

Example: Output for a non-compliant token

ERC4626 Tests

Integration

Configuration

Run

ABDKMath64x64 tests

Integration

Run

Additional resources

Helper functions

Usage examples

Logging

Assertions

Clamping

HEVM cheat codes support

Usage example

How to contribute to this repo?