Open Zeppelin’s ERC-20 reference implementation is widely used in Web3. A bug in it would be devastating for the many contracts that derive from it. But how do we know that it is correct? And how do we know contracts that derive from it do so correctly and do not introduce bugs?

In Part One of this series on formal verification, we explained how CertiK uses formal verification to mathematically prove the correctness of ERC-20 contracts that we audit. Let’s dive in and see what happens when we apply it to OpenZeppelin’s code.

ERC-20 Standard Properties

At CertiK, we have written property templates that precisely describe the expected behaviors of ERC-20 token contracts. These templates are generic: our tools analyze the implementation details of each smart contract and adapt the templates accordingly. We have 38 property templates.

Let's look at some of the properties that we regularly verify on incoming ERC-20 token contracts. For the sake of readability, the formulas that follow are slightly simplified and omit some technical details that do not contribute to the overall understanding of the approach. CertiK's audit reports contain an appendix that reproduces the formulas that have been used during model checking. A list with all the formulas used in our ERC-20 verification approach is publicly available here.

The transferFrom() function in ERC-20 contracts requires special attention, as it needs to distinguish between the initiator of the transaction (the address is msg.sender), the accounts that spend and receive tokens, and because it needs to observe the limits imposed by the entries in _balances and _allowances.

Specifying Correct Allowance Updates

When transferFrom() succeeds, it must deduct the amount of tokens that have been transferred from the allowance that the sender has over the spender's account. However, many ERC-20 token contracts also allow the token owner to grant infinite allowance to another account. This is reflected by setting that account's allowance to the maximum value, i.e. to ((2^256)-1). Taking that exception into account, a correct allowance update can be specified by the following LTL formula 𝜑:

It states that when transferFrom() is invoked and terminates (without reverting) with a return value of true, we expect that the sender's allowance is either reduced by the amount of tokens in amt (the red subformula) or that the sender either is the owner of the transferred tokens or has unlimited allowance over the spender's tokens. In those cases, the allowance must remain unchanged (the blue subformula).

Specifying Dismissal of Transfers That Exceed the Allowance

Attempts to use transferFrom() to transfer an amount of tokens that exceeds one´s allowance should fail. This is formalized by 𝜓:

If the invocation of transferFrom() requests to transfer tokens from somebody other than their owner and if that transfer exceeds the sender's allowance, we expect the transaction to either revert, or to fail and signal its failure by returning false.

These are only two examples of the formalizations CertiK uses to capture the expected behaviors of ERC-20 token contracts. For more information about our properties and all technical details, refer to our property list.

OpenZeppelin's Reference Implementation for ERC-20 Contracts

The OpenZeppelin library provides reference implementations for many popular smart contracts. Its ERC-20 base contracts are popular and often used as building blocks for DeFi projects.

As many of the projects we audit contain contracts that derive from OpenZeppelin, we formally verified a set of 38 security properties on their ERC-20 reference implementation as of version 4.7.3. As can be seen the image below, all properties of the base contract are proven correct.

This result, however, tells us little about the security of actual ERC-20 token implementations, even when they derive from the OpenZeppelin contract! In actual blockchain projects, the reference implementation is modified by overriding its virtual functions and by introducing additional public APIs. What if someone makes a mistake?

The correctness of a base contract is generally not sufficient to ensure security in derived tokens! It is possible to introduce errors not only when overriding parts of the base implementation, but also by making changes to the contract’s state variables that were unforeseen in the base implementation.

OpenZeppelin implements their ERC-20 base contracts by making important state variables private. This ensures that contracts derived from them cannot simply destroy invariants that hold for those private variables. This encapsulation provides a certain level of protection from errors introduced within derived contracts.

Example: PancakeSwap's CAKE Token

PancakeSwap is one of the most popular decentralized exchanges. It is powered by the CAKE token, which implements the BEP20 standard (an extension of the ERC-20 standard). In general, CAKE tokens can be earned by staking and by providing liquidity to the exchange. Running our model checker on the CAKE token implementation successfully proves the basic ERC-20 behavior. The token implementation satisfies all of the properties that CertiK verifies on basic ERC-20 token contracts.

Conclusion

We’ve used formal verification to mathematically prove that OpenZeppelin’s reference ERC-20 implementation v4.8 meets basic ERC-20 properties. While it is not surprising that it does, this is good to know! We explained why just verifying OpenZeppelin’s implementation is not enough. You need to formally verify contracts that derive from it. Be sure to watch for our next blog post, where we discuss handling extensions to ERC-20 and other real-world challenges in verifying