Fuzzing ERC20 contracts with Diligence Fuzzing

Fuzzing ERC20 contracts

Learn how you can use Scribble to define a complete and checkable ERC20 specification. As a bonus, we show how you can use fuzzing to check the specification automatically!

I’m willing to bet that you’re familiar with the ERC20 standard, the best-known standard for tokens (next to ERC721). You might be less familiar with Scribble and fuzzing, which provide the easiest way to test ERC20 implementations exhaustively.

In this article, I will show you how to use Scribble to write a complete ERC20 specification. Using this specification together with the brand new “Diligence Fuzzing” platform, we’ll fuzz the contract and automatically check if a token has any bugs.

Specifications

Before we can start fuzzing, we’ll first need to write some Scribble annotations. These formal statements will essentially tell the fuzzer what to check.

Learn more about writing Scribble properties here.

With just 16 annotations, you’ll be able to start fuzzing any ERC20 token! I’ll discuss six of them in a bit more detail!

Check out this gist for the full 16 annotations.

Contract Annotations

We’ll start with the two global annotations. These talk about the functionality and behaviour that the whole contract must have. In this case (for an ERC20 contract), these will talk about the token supply.

The first property ensures that our mapping to record balances aligns with the total supply of tokens.

///#invariant {:msg "The totalSupply is equal to the sum of all balances" } unchecked_sum(_balances) == _totalSupply;

The second property ensures that the supply of tokens never changes except at contract initialisation time. This token is not in-/deflationary, no funny business!

///#if_succeeds {:msg "The sum of balances doesn't change over time"} unchecked_sum(_balances) == old(unchecked_sum(_balances)) || msg.sig == bytes4(0x00000000);

We’ll add these just above the contract because they are contract level annotations.

///#invariant {:msg "The totalSupply is equal to the sum of all balances" } unchecked_sum(_balances) == _totalSupply;
///#if_succeeds {:msg "The sum of balances doesn't change over time"} unchecked_sum(_balances) == old(unchecked_sum(_balances)) || msg.sig == bytes4(0x00000000);
contract AnnotatedToken {
	...
}

💡 The msg.sig check allows changes to the _balances sum in the constructor

Function Annotations

We’ll be looking at one of ERC20’s most important functions for the function annotations: the transfer function.

/// #if_succeeds {:msg "The sender has sufficient balance at the start"} old(_balances[msg.sender] >= _value);
/// #if_succeeds {:msg "The sender has _value less balance"} msg.sender != _to ==> old(_balances[msg.sender]) - _value == _balances[msg.sender];
/// #if_succeeds {:msg "The receiver receives _value"} msg.sender != _to ==> old(_balances[_to]) + _value == _balances[_to];
/// #if_succeeds {:msg "Transfer to self won't change the senders balance" } msg.sender == _to ==> old(_balances[msg.sender]) == _balances[msg.sender];
function transfer(address _to, uint256 _value) external returns (bool) {
	r...
}

Pre Condition

The first if_succeeds annotation describes something which is often called a “precondition”. It’s a condition that you expect to hold at the beginning of the function.

This property says the function can only succeed if (if_succeeds) at the beginning of the transaction (old(...)) the balance of the sender is bigger than or equal to the value which is being transferred (_balances[msg.sender] >= _value).

/// #if_succeeds {:msg "The sender has sufficient balance at the start"} old(_balances[msg.sender] >= _value);

Post Condition

Then we have two annotations that describe what should happen when there is a successful execution (if_succeeds) and we’re sending money to someone else (msg.sender != _to ==>).

In such cases, the sender has _value less balance after the transaction than before old(...). Similarly, the recipient has _value more balance.

/// #if_succeeds {:msg "The sender has _value less balance"} msg.sender != _to ==> old(_balances[msg.sender]) - _value == _balances[msg.sender];

/// #if_succeeds {:msg "The receiver receives _value"} msg.sender != _to ==> old(_balances[_to]) + _value == _balances[_to];

These properties are commonly post-conditions because they describe something about the result of the function.

You might have noticed that the previous two properties left out one case; The case where you send tokens to yourself. In this case, we’ll ensure that the senders’ balance doesn’t change.

/// #if_succeeds {:msg "Transfer to self won't change the senders balance" } msg.sender == _to ==> old(_balances[msg.sender]) == _balances[msg.sender];

💡 Are you writing Scribble annotations? Check out our plugin: vscode-scribble - Visual Studio Marketplace.

Fuzzing

You can use analysis methods such as fuzzing and symbolic execution to automatically find whether your code matches the specification or whether there are any bugs and vulnerabilities.

For this post, I’ll be using our very own (and insanely performant) Diligence Fuzzing.

Seed State

Before fuzzing, we always set up a “seed state”. The seed state is a deployment of the system that we would like the fuzzer to target. You can think of it as a fixture, where a sane configuration of the system is used to execute tests.

In this case, our seed is super simple! We deploy our token, and we’re set!

const AnnotatedToken = artifacts.require("AnnotatedToken");

module.exports = async function(callback) {
  try {
    let accounts = await web3.eth.getAccounts();

    contracts = []
    token = await AnnotatedToken.new()
    contracts.push(['token', token.address])

    console.log("Deployed contracts:")
    console.table(contracts)
    callback();
  } catch (e) {
    callback(e)
  }
}

Learn more about writing seed setup scripts here.

Fuzzing Results

Once the seed is ready, we only need to start the campaign and wait for results to come in! I’ve set up a fuzzing campaign and ran it for ~2 hours without running into a property violation.

Checking the coverage metrics shows me that all the functions were covered for 100% (except for the constructor), so I’m feeling pretty good about this token!

Do you want to learn more about the different kinds of metrics provided by Diligence Fuzzing? Check out our documentation!

Fin

Want to use Diligence Fuzzing to make your smart contracts more secure? Sign up for early access here!

All posts