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

Properties

This repository contains 168 code properties for:

ERC20 token: mintable, burnable, pausable and transferable invariants (25 properties).
ERC721 token: mintable, burnable, and transferable invariants (19 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 or Medusa.

Testing the properties with fuzzing

Install Echidna or Medusa.
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 advantages 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 {ITokenMock} 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 = ITokenMock(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

Echidna

Create the following Echidna config file

corpusDir: "tests/crytic/erc20/echidna-corpus-internal"
testMode: assertion
testLimit: 100000
deployer: "0x10000"
sender: ["0x10000", "0x20000", "0x30000"]
# Uncomment the following line for external testing
#allContracts: true

Medusa

Create the following Medusa config file:

{
  "fuzzing": {
    "testLimit": 100000,
    "corpusDirectory": "tests/medusa-corpus",
    "deployerAddress": "0x10000",
    "senderAddresses": ["0x10000", "0x20000", "0x30000"],
    "assertionTesting": {
      "enabled": true
    },
    "propertyTesting": {
      "enabled": false
    },
    "optimizationTesting": {
      "enabled": false
    }
  },
  // Uncomment the following lines for external testing
  //		"testing": {
  //			"testAllContracts": true
  //    },
  "compilation": {
    "platform": "crytic-compile",
    "platformConfig": {
      "target": ".",
      "solcVersion": "",
      "exportDirectory": "",
      "args": ["--foundry-compile-all"]
    }
  }
}

To perform more than one test, save the files with a descriptive path, to identify what test each file or corpus belongs to. For instace, 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 corpus directory config opction for external tests accordingly.

The above configuration will start Echidna or Medusa in assertion mode. The target contract(s) will be deployed from address 0x10000, and transactions will be sent from the owner as well as 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 our fuzzing tools finish the fuzzing campaign, corpus and coverage results will be available in the specified corpus directory.

Run

Echidna

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

Medusa

Go to the directory cd tests/crytic/erc20
For internal testing: medusa fuzz --target-contracts CryticERC20InternalHarness --config medusa-internal.yaml
For external testing: medusa fuzz --target-contracts CryticERC20ExternalHarness --config medusa-external.yaml

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 . --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 . --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

Properties

Install / Use

README

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