Our current standards-based verification covers the basic behaviors of ERC-20 token contracts. However, some tokens implement functionality that goes beyond the standard. These cases are generally more challenging for formal verification, and some other contracts have computations that are generally hard to verify. Let's dive into the details of these challenges and discuss how to handle them.

ERC-20 Extensions

In many practical cases, tool supported verification is not fully automatic. For example, some ERC-20 token contracts implement extensions – such as timelocks – for specific addresses. An example of such logic is the following code snippet, where token transfers may be suspended for dedicated addresses. Depending on the project's context, such a policy may be well justified or pose a security risk.

In our verification, we apply automated analyses on smart contracts to determine the most appropriate set of properties to apply. If the underlying heuristic is unaware of the use of such time locks, it may impose a specification on the contract that does not fully capture its intended behavior. Unfortunately, it is not always possible to avoid such misclassifications. When they happen, formal verification usually proceeds to analyze the contract with respect to a property specification that does not reflect some of the contract's behavior. Such specification mismatches may result in the model checker flagging property violations due to the contract's intended behavior not being adequately represented by the chosen property, as it does in the above example.

Our basic ERC-20 specification contains four properties requiring any request to transfer tokens to only succeed if the spender's token balance suffices (and, in the case of transferFrom(), that the sender has sufficient allowance): They are named erc20-transfer-succeed-normal, erc20-transfer-succeed-self, erc20-transferfrom-succeed-normal, and erc20-transferfrom-succeed-self. Because of the timelocks in the contract, our model checker reports those four properties as being violated:

That is where CertiK's team of security experts comes in. We manually review any such property violation. In the example above, we would recognize the violations as being false positives, add a remark that explains the specification misfit, and classify the formal verification results that we report accordingly:

In that sense, not every property violation is a security vulnerability. On the other hand, we believe that such false positives are still a good indicator; they highlight non-standard behavior that requires extra scrutiny. In our example, the possibility of imposing time locks on dedicated addresses may or may not be considered a centralization risk. That kind of judgment is out of the scope of any formal verification tool and can only be made by a domain expert. False positives may help to identify potential issues and thereby contribute to the overall audit quality, while serving to illustrate the synergy of human and automated review.

Computational Limitations of Tool-Assisted Formal Verification

A more fundamental challenge in formally verifying smart contracts is that many properties are actually undecidable in general. Computability theory has proven that for many classes of properties, there does not exist an algorithm that can generally decide if a property from that class is satisfied or not.

While smart contracts have a lot of nice characteristics such as their gas consumption guaranteeing termination, they often perform complex mathematical computations that implement their bigger-picture business models. With integers having 2^256 possible values, such smart contracts have a practically infinite state space.

Even worse, if the contracts perform simple non-linear arithmetic operations such as multiplying or dividing variables, automated reasoning about the contracts is generally undecidable. Still, that fundamental result leaves room for improvements on more specific sub-problems. Today's automated reasoning tools are continually improving, which extends the set of properties that can be dealt with automatically. However, such tools often fail to decide if a smart contract that involves complex arithmetic computations satisfies a property that requires reasoning about those computations.

Other limitations are less fundamental. They can be caused by verification algorithms running out of time or available main memory.

If we encounter such a situation, we report the verification result as being "inconclusive." In practice, such results are treated much like false positives: CertiK security experts inspect the smart contract and manually check its implementation for any problems (numeric, overflow-related, or higher-level such as centralization risks).

Overcoming These Limitations

If a blockchain project goes considerably beyond standard behaviors or makes heavy use of complex arithmetic computations, it will most likely require customized formal verification. With our foundations in deductive verification and a team of world-class experts in formal verification, CertiK offers custom verification services that use both semi-automated and proof-assistant based methods to verify complex smart contracts.

Conclusion

Since September 2022, we have applied standards-based formal verification to analyze the expected behaviors of incoming ERC-20 token contracts and check them for security vulnerabilities. By using automated techniques, we routinely check basic properties for most ERC-20 contracts. In our experience, this approach has at least two advantages.

1. If a smart contract satisfies a property, all its potential executions are known to be covered by that property. In essence, the smart contract is highly unlikely to violate the property (though there could be bugs in the tools or assumptions about the blockchain environment). This result is stronger than testing (where corner cases might be missed) or manual code review.

2. Reported violations hint at potential security vulnerabilities or at non-standard behavior that require extra scrutiny during an audit. Deviations from standard behavior are routinely detected and brought to auditors’ attention. Auditors investigate these findings and ultimately decide if the deviation is a security vulnerability, if it might raise governance issues, or if it is an acceptable (or even desired) extended behavior.

We believe that formal verification of contracts that implement standards such as ERC-20 adds another layer of security to our customer's projects. This lesson has been learned through experience: we’ve verified more than 300 ERC-20 contracts from over 100 projects.

In a previous post, we showed our results of formally-verifying OpenZeppelin’s reference ERC-20 implementation and explained how we verify actual token implementations that derive from it.

This article concludes our deep dive into the formal verification of ERC-20 token contracts.