Introducing ERCx:
Conformance and Property-checking for ERC Tokens

Have you ever interacted with an ERC-20 token/contract and wondered if it is secure or reusable? Buying a token that at least follows the required standard specification should be the norm. An ERC-20 token should abide by additional desirable properties not planned in the original specification. What can you do to figure this out? Runtime Verification has a tool for that: ERCx! 

We built ERCx to answer those questions for you. Not only can ERCx be used to check for a contract's security and reusability, but it can also help you develop your own contract that inherits desirable behaviors. In that respect, ERCx favors composability and ensures assumptions are correct.

Ensuring smart contract code is bug-free and realizes its intended mission is a difficult process. The most common practice is manual code review, which is time-consuming and nonlinear. The entry point is often unclear, and drawing conclusions is not immediate. While thorough testing is no substitute for an in-depth analysis, it accelerates and facilitates analysis. 

A significant gap exists between developers’ expectations and code. Moreover, gaining insights into the code is difficult even for good-willing developers. If code is law, the meaning of the law should be accessible to all.

What is ERCx?

ERCx is a conformance and property-checking tool. It checks smart contracts against an extensive property-based test suite using the Foundry framework, measuring conformance and behavioral risks for implementations of the supported ERC standards. Currently, ERCx supports ERC-20, and we are incorporating ERC-4626.

The tests run by the tool can be separated into four categories:

• ABI (Application Binary Interface) Tests: These measure the contract’s level of conformance to the described ABI of the standard being tested. The tests detect whether the functions required by the corresponding EIP (Ethereum Improvement Proposal) are present in the contract and that their signature are correct. Failing any of these tests means that either a function prescribed by the EIP is not implemented or its signature has been altered. For example, EIP-20 states that the transfer function of an ERC-20 contract takes in an address and an uint256 as (ordered) inputs and returns a `boolean` as output, with its state mutability set as nonpayable.
• Minimal Tests: Behaviors specified in the EIP whose failure goes against the standard. Minimal tests check for unnegotiable properties that should hold for any contract claiming to implement the standard. Minimal properties should only fail if the contract’s developers have strong and voiced reasons for it. However, failing these should be considered a bad practice when implementing a token.
• Recommended Tests: Good-to-have security properties. Contracts conforming to these requirements adhere to non-mandatory but important behaviors. It is advised that these tests successfully pass as a sanity check. Failing these tests may result in absent security guards with nontrivial consequences.
• Desirable Tests: Best practices for the standard’s implementation. Quite often, after an EIP has been finalized, time shows preferred ways of using, tweaking, or enhancing the security and functionality of the EIP. The desirable tests measure how much of this time-gained insights are put into the standard’s implementation. Failure to pass these tests should give an intuitive understanding of possible shortcomings for the tested implementation.

Who can Use ERCx?

ERCx is developed with different users in mind, namely, developers, investors, and auditors.

Developers

When considering integrating a token into a protocol, ERCx provides developers insights into the implementation of these tokens. Running tests on familiar or already integrated tokens to have a side-by-side comparison of their behavior as told by the tool is time-saving and insightful.

Also, if integrated tokens/protocols upgrade their business logic and the standards they implement are covered by ERCx, running the tool on the newly upgraded code would provide valuable insights into how the upgrade changed the previous behavior.

In summary, the prime benefit of the ERCx tool for developers is quickly gaining insights into existing code, which can alleviate the time required for correctly understanding it, and can help when comparing different implementations for the same supported standard. We also plan on integrating ERCx into major Integrated Development Environments.

Investors

When considering investing in some protocol that claims to implement specific standards, if ERCx supports these standards, investors can test the contracts to gain quick insights into the implementation’s behavior. The benefit from the investor’s perspective is a better understanding of the contract implementation and behavior to catch any red flags during an exploratory phase.

We note that satisfying (even all) properties tested by ERCx does not imply in any way that the contract is safe, nor does it provide a stamp implying that a project should be invested in.

Auditors

Time is the auditor’s natural enemy. Quickly gaining an understanding of a protocol is crucial to allocate as much time as possible to in-depth logic checks and to scan for hidden code vulnerabilities. ERCx provides a good entry point for getting familiar with protocols implementing standards covered by the tool. After running ERCx, an auditor should be able to have a high-level understanding of how compliant the standard’s implementation is, which best practices are followed or not, and possibly where to look for more in-depth understanding (or outright finding a vulnerability).

Everyone Else

Having a tool that summarizes the behavior of smart contracts contributes to the understanding of the blockchain in general. Examples of insights include how usual it is that a certain implementation has a non-mandatory but useful functionality, or how many addresses implement a specific standard. Many questions can be asked about the blockchain in general and its code, and the ERCx tool can help answer them.

Example of ERCx use with USDT

This example is tailored to developers and auditors. We will show how ERCx can point to behaviors in the code that may not be a vulnerability per se but could lead to potential vulnerabilities if overlooked. The contract of choice is USDT. USDT, also known as Tether, is a stablecoin backed by US dollars. USDT has been integrated into various blockchain protocols.

Scenario 

A developer seeks to integrate USDT into its protocol, or an auditor is auditing a protocol that could use USDT. In both cases, the user desires to know more about the behavior of USDT.

ERCx

After fetching USDT’s address (0xdAC17F958D2ee523a2206206994597C13D831ec7), we can introduce it to ERCx.

 

ERCx Report

You will see that there is already a report for the address. Note: when there is no report, ERCx will produce a new report in less than a minute. 

Now let us look at the report. In red, there are 4 ABI and 5 Desirable failing tests. Since code is often developed with the implicit assumption that implementations adhere to the ABI as described by their standard, 4 failing tests should strike our attention.

We go over to the ABI tab and see the following failing tests:

The functions transfer and transferFrom are both crucial to the token and behave differently from what EIP-20 prescribes. Both transfer and transferFrom return nothing, while they should return true if the transfer is successful.

This means that if a protocol assumes a boolean value returned by the transfer or transferFrom function, the actual behavior of the protocol when using USDT can have unintended consequences.

As an example, assume some function of the protocol requires that a token transfer is successful by doing something like:

require(token.transferFrom(user, address(this), amount));

Now, if the token was USDT, even if the transfer was successful, no value was returned. Hence, because the require clause expects a boolean, the evaluated expression would be require(false);. Thus, even successful USDT transfers would fail this check.

The consequences of a successful USDT transfer leading to a reverting execution depend on the specific protocol. Still, we can agree that having a check fail or succeed on transfers depending on the token is a risk.

This is an example of unsuspected behavior when dealing with ERC-20 tokens, which can also be detected by looking at the USDT source code. Using ERCx is not a substitute for an in-depth analysis of the code under examination. However, the advantage of using ERCx is to obtain a rich automated summary to start digging deeper.

Get in touch with us!

ERCx is actively being developed, with ERC-4626 as our next incorporation. We’re actively looking for feedback on the tool. So if you have any suggestions or features that would improve how you integrate ERCx into your workflow, please contact us.