"ERC20 Tokens: Don't Gamble with Security, Use Invariants to Ensure Safe and Reliable Tokens"
IntroductionAs smart contracts continue to grow in popularity on the Ethereum blockchain, it's becoming increasingly important to ensure their security and functionality. One way to achieve this is through a process known as "fuzzing". Fuzzing involves testing a smart contract by sending it unexpected and random inputs to see how it behaves. By doing so, developers can identify potential vulnerabilities and ensure that the contract behaves correctly under all possible scenarios. In this blog article, we'll explore how Echidna, a powerful testing tool for smart contracts, can be used for fuzzing ERC20 tokens, one of the most common types of tokens on the Ethereum blockchain. We'll also delve into the properties that an ERC20 token should satisfy and how Echidna can help ensure that these properties are met, thereby increasing the security and reliability of ERC20 tokens.
In our last blog article, we talked about the properties of ERC20 tokens which should always be satisfied in case of correct functionality of the ERC20 tokens. These properties are also known as invariants. The goal of these properties is to detect vulnerabilities. These properties can be checked using directed testing, fuzzing, or formal verification.
Setup
In this blog article, we will discuss how fuzzing can be used to check if the properties are satisfied or not. For fuzzing, we will use Echidna tool from Trail of bits. If you are not familiar with Echidna, now is a good time to check our previous blog posts on it. You can follow our previous blog articles to setup Echidna. In this blog article we will use hardhat framework, but you can use other frameworks as well. The first step is to setup a hardhat project. For this, follow the steps provided on the official website of hardhat. Once the hardhat project is setup, create a directory with name “contracts”, create a solidity file titled “ExampleToken.sol”, copy the ERC20 ExampleToken from Figure 1, and save it in ExampleToken.sol file.
pragma solidity ^0.8.19;
import "@openzeppelin/contracts/token/ERC20/ERC20.sol";
import "@openzeppelin/contracts/token/ERC20/extensions/ERC20Burnable.sol";
import "@openzeppelin/contracts/security/Pausable.sol";
import "@openzeppelin/contracts/access/Ownable.sol";
contract ExampleToken is ERC20, ERC20Burnable, Pausable, Ownable {
constructor() ERC20("Example token", "EXT") {}
function pause() public onlyOwner {
_pause();
}
function unpause() public onlyOwner {
_unpause();
}
function mint(address to, uint256 amount) public virtual onlyOwner {
_mint(to, amount);
}
/*function _beforeTokenTransfer(address from, address to, uint256 amount)
internal
virtual
whenNotPaused
override
{
ERC20._beforeTokenTransfer(from, to, amount);
}*/
}
Figure 1: Sample ERC20 token - ExampleTokenAfterwards, follow the steps below:
- Import the ERC20 properties into to your hardhat project
- If you setup your hardhat project using npm, then: npm install https://github.com/crytic/properties.git
- If you setup your hardhat project using yarn, then: yarn add https://github.com/crytic/properties.git
- Decide if you want to do internal or external testing. Both approaches have advantages and disadvantages.
- Internal testing: properties are defined inside the contract to test, with complete access to the internal state of the system.
- External testing: properties are tested using external calls from a different contract. Properties are only allowed to access external/public variables or functions.
A snippet of ERC20 properties can be found in Figure 2 for reference. You don’t need to copy them as they are already installed in the previous step. If you are interested in description of properties, refer to our blog article - The Importance of Secure ERC20 Tokens: Ensuring Trust in the World of Decentralized Finance. Please note, Figure 2 shows the properties from external testing view but ERC20 properties for internal testing are also same with slight changes.
pragma solidity ^0.8.0;
import {CryticERC20ExternalTestBase} from "../util/ERC20ExternalTestBase.sol";
abstract contract CryticERC20ExternalBasicProperties is CryticERC20ExternalTestBase {
constructor() {
}
////////////////////////////////////////
// Properties
// Total supply should change only by means of mint or burn
function test_ERC20external_constantSupply() public virtual {
require(!token.isMintableOrBurnable());
assertEq(token.initialSupply(), token.totalSupply(), "Token supply was modified");
}
// User balance must not exceed total supply
function test_ERC20external_userBalanceNotHigherThanSupply() public {
assertLte(token.balanceOf(msg.sender), token.totalSupply(), "User balance higher than total supply");
}
// Sum of users balance must not exceed total supply
function test_ERC20external_userBalancesLessThanTotalSupply() public {
uint256 sumBalances = token.balanceOf(address(this)) + token.balanceOf(USER1) + token.balanceOf(USER2) + token.balanceOf(USER3);
assertLte(sumBalances, token.totalSupply(), "Sum of user balances are greater than total supply");
}
// Address zero should have zero balance
function test_ERC20external_zeroAddressBalance() public {
assertEq(token.balanceOf(address(0)), 0, "Address zero balance not equal to zero");
}
// Transfers to zero address should not be allowed
function test_ERC20external_transferToZeroAddress() public {
uint256 balance = token.balanceOf(address(this));
require(balance > 0);
bool r = token.transfer(address(0), balance);
assertWithMsg(r == false, "Successful transfer to address zero");
}
…
…
}
Figure 2: ERC20 properties snippet for external testingInternal Testing
For internal testing, create a new Solidity file containing the ERC20HarnessIntern contract (Figure 3). 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 "./ExampleToken.sol";
contract ERC20HarnessIntern is ExampleToken, 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();
}
}
Figure 3: ERC20HarnessIntern smart contract for internal testing of ERC20 tokensThe PropertiesConstants is shown in Figure 4. Please note, you only need to create a solidity file ERC20HarnessIntern. You don’t need to create a file PropertiesConstants as it will be installed in previous step.
pragma solidity ^0.8.0;
abstract contract PropertiesConstants {
// Constant echidna addresses
address constant USER1 = address(0x10000);
address constant USER2 = address(0x20000);
address constant USER3 = address(0x30000);
uint256 constant INITIAL_BALANCE = 1000e18;
}
Figure 4: PropertiesConstants smart contract with variables and addresses.Now create a configuration file for echidna, echidna.config_intern.yaml in the project root directory (or any directory of your choice). It should contain the following text as shown in Figure 5:
corpusDir: "tests/erc20/echidna-corpus-internal" testMode: assertion testLimit: 50000 deployer: "0x10000" sender: ["0x10000", "0x20000", "0x30000"]Figure 5: echidna.config_intern.yaml file with configuration for Echidna internal testing.
The configuration in Figure 5 will start Echidna in assertion mode. The smart contract for ERC20 token 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 50000 tests, but depending on the token code complexity, this can be modified.
Now run Echidna using the following command:
echidna . --contract ERC20HarnessIntern --config echidna.config_intern.yaml
After Echidna is finished with fuzz testing, you should see the output as shown in Figure 6:
Figure 6: Echidna fuzz testing output for internal testing.
From Figure 6, it seems one of the properties fails – test_ERC20_constantSupply(). The property checks if the total supply of the contract can be manipulated by anyone during the execution of the smart contract. In Figure 1, the “mint” function can be called by owner as many times as they want.
Finally, once Echidna finishes the fuzzing campaign, corpus and coverage results will be available in the tests/erc20/echidna-corpus-internal directory.
External Testing
For external testing, create two contracts: the ERC20HarnessExtern and the MyTokenMock as shown below in Figure 7. In the ERC20HarnessExtern contract you can specify which properties to test, via inheritance, e.g., CryticERC20ExternalBasicProperties. In the MyTokenMock 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 "./ExampleToken.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 ERC20HarnessExtern is CryticERC20ExternalBasicProperties {
constructor() {
// Deploy ERC20
token = ITokenMock(address(new MyTokenMock()));
}
}
contract MyTokenMock is ExampleToken, 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;
}
}
Figure 7: ERC20HarnessExtern and the MyTokenMock for external testing.Now create a configuration file for echidna, echidna.config_extern.yaml as shown in Figure 8. It should contain the following text:
corpusDir: "tests/erc20/echidna-corpus-external" testMode: assertion testLimit: 50000 deployer: "0x10000" sender: ["0x10000", "0x20000", "0x30000"] allContracts: trueFigure 8: echidna.config_extern.yaml file with configuration for external testing.
The configuration in Figure 8 will start Echidna in assertion mode. The smart contract for ERC20 token 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 50000 tests, but depending on the token code complexity, this can be modified.
Now run Echidna using the following command:
echidna . --contract ERC20HarnessExtern --config echidna.config_extern.yamlAfter Echidna is finished with fuzz testing, you should see the output as shown in Figure 9:
Figure 9: Echidna fuzz testing output for external testing with ERC20 Basic Properties
You will notice one thing between Figure 6 and Figure 9, one property fails in Figure 6 whereas no property fails in Figure 9. It is because in our ExampleToken (Figure 1), the owner is allowed to mint as many tokens as they want. This kind of property can shed light on to centralization issues of a smart contract. The external testing tests how a 3rd party interacts with the smart contract. Hence, unless you are an owner, you won’t be able to mint unlimited tokens. As an exercise, you can remove the modifier “onlyOwner” from the “mint” function in Figure 1 and see what happens.
Finally, once Echidna finishes the fuzzing campaign, corpus and coverage results will be available in the tests/erc20/echidna-corpus-external directory.
Conclusion
As smart contracts continue to revolutionize industries, ensuring the security and robustness of ERC20 tokens becomes increasingly crucial. Fuzzing, enabled by tools like Echidna, offers a proactive approach to detect vulnerabilities and validate the properties of these tokens. Truscova, a leading smart contract security auditing company, offers a comprehensive suite of services that leverage Fuzzing and cutting-edge technologies. Truscova’s proficiency in Fuzzing and advanced testing methods enhances the resilience of smart contracts, mitigates potential vulnerabilities, and safeguards against malicious attacks. By embracing fuzz testing, developers and companies can strengthen the security posture of their ERC20 tokens and gain confidence in their smart contract solutions.
About Truscova:
Truscova comes with 30+ years of academic research and hundreds of academic publications which pioneered the area of Formal Verification. The team combines academic leadership, industrial strength and Blockchain expertise. Truscova currently analyzes Solidity code combining Formal Verification techniques: abstract interpretation, constraint solving, theorem proving, and equivalence checking.