4626 Vault Checking with ERCx:
How can we use ERCx to detect issues in our contracts?

In our previous blog post, where we introduced our new ERC-4626 test suite, we briefly described the specifications of an ERC-4626 vault and how we can leverage property tests to check that the vault satisfies the required properties stated in the EIP-4626. We showed and compared two test suites, a16zcrypto’s ERC-4626 test suite and ERCx test suite. Both test suites are available for developers to use when checking their ERC-4626 contracts. Following the publication of our last blog post, there have been many updates and changes to ERCx. We have expanded the tool's capabilities to allow the testing of 8 more network chains, including Layer 2 chains and their respective testnets. In the recent updates, we improved our ERC-4626 test suite based on users’ feedback and introduced the notion of inconclusive test results (more on this later). Thus, it is necessary for us to provide an updated guide on using ERCx to detect issues in our contracts. Although this guide will only provide information on how to use ERCx through our website interface, we also offer easy-to-use VS code extension and Open API endpoints that will allow developers to utilize the tool. Please feel free to contact us via Twitter/X, Discord, or Telegram if you require assistance using any of these features. For this blog post, we use Version 2.2.0 of the ERC-4626 test suite and ERCx4626Mock0 to guide readers through and provide a visual reference.

Guide for ERCx

This section describes how one can detect issues with tokens using ERCx. As mentioned in the introduction, we use ERCx4626Mock0 as an example throughout this section. This contract mimics a deployed contract we have found and tested with ERCx. Thus, the bug that you will find in this ERCx4626Mock0 contract is an actual bug in the deployed contract. However, as we are unable to disclose the actual deployed contract, we will use this mock contract as an example for this guide instead of the actual contract.

Step 1: Provide the address or source code of a contract in ERCx

As described in our previous blog post, we can run the appropriate ERCx test suite on a contract by providing its address (for deployed contract) or source code (for undeployed contract). For deployed contracts, we must choose the test suite we want ERCx to run on (i.e., you can run ERC20, ERC4626, ERC721, or ERC1155 test suite) and the network chain the token is deployed on. On the other hand, for undeployed contracts, ERCx currently supports only flatten source code contracts (i.e., one file containing all dependencies), and it is necessary to to select the main contract class and the appropriate test suite to run with. Figure 1 shows the required inputs to run the ERC-4626 test suite for ERCx4626Mock0 on the ERCx Test your Code page. The inputs include (i) the flatten source code of the contract, (ii) the main contract class of the contract (in this case, it is ERCx4626Mock0), and (iii) the test suite of the ERC standard you wish to run it with (in this case, it is ERC4626).

Once the contract has been evaluated by the selected test suite, a summary of the evaluation will be provided at the top of the token page, as seen in Figure 2. Additionally, the readout will show the ERC standards that have been detected. ERCx can classify up to 20 ERC standards for any token class found in the contract.

The above figure shows a token page summary for an undeployed contract being tested with ERCx. More information is available for retrieval from deployed contracts, such as their name, symbol, total supply, proxy usage, etc. Figure 3 shows the token page summary for USDC.

Step 2: Look out for inconclusive and failed test/s under each level of tests

The “Latest Evaluation Report” section, shows the “Test suite Score”, “Conformance Score” and “Security Score” of the test results, together with the summary of the ERC-4626 functions present in the contract as seen in Figure 4. Failure to achieve 100% in all of these 3 scores does not mean that the vault is a “bad” vault. Some possible reasons for not having 100% in these 3 scores could be due to (a) the contract indeed has some properties that are not satisfied for an ERC-4626 vault, (b) deviation/s in implementation of functions from the specifications stated in EIP-4626, or (c) there is some issue with allocating assets and/or shares to dummy users before running the test suite.
For the ERC-4626 test suite, the results from testDealIntendedAssetsToDummyUsers and testDealIntendedSharesToDummyUsers can be used to check if there are any issues with allocating assets and shares to dummy users respectively before running the test suite. If such an issue exists, there would be inconclusive test results that require the user to manually check the ERC-4626 properties.

Note that even if there is a high score in either the Conformance or Security Score, it is still important to check the individual scoring bars under the “Summary of test results” section as the scores do not account for inconclusive tests. A test is inconclusive if either (a) it is an ABI test of an optional function or (b) its result is inconclusive as certain conditions are not met while testing the said property test. In either case, it would require the users to manually check whether the token satisfies the stated properties from the tests that are deemed to be inconclusive ¹. The tests are also further broken down into different levels to provide better categorization of the tests ran ². Figure 5 shows the “Summary of test results” for ERCx4626Mock0, where the number of passed, inconclusive, and failed test results in each level can be viewed.

Based on the summary of test results shown in Figure 5, the following observations can be made:

1. All signature checks for the required functions of ERC-4626 standard passed for this vault, which means the vault has all required functions present with their correct signatures and output types.
2. For the “Standard” level, there are 22 passed tests (55.0%), 17 inconclusive tests (42.5%) and 1 failed test (2.5%).
3. For the “Security” level, there are 20 passed tests (45.4%), 23 inconclusive tests (52.3%) and 1 failed test (2.3%).

There are quite a number of inconclusive tests and some failed tests for this vault. To find out if there are any issues with the vault, further analysis of the tested properties at each individual level is required. Clicking on the scoring bar of the individual tests from each level will provide more information. Alternatively, details can be gained via the tabs below the scoring bars. Figure 6 shows the details of the tests under the “Standard” tab.

Step 3: Filter the test results by functions

It can be overwhelming to pinpoint if there are any concerning issues with the vault by looking through all the test results. Thus, filtering the test results by functions in each level is a good way of narrowing down to see if any of the functions are causing an issue. This can be done through the dropdown options, as seen in Figure 7.

The four main functions that allow users to exchange between shares and assets, and hence change their assets’ and shares’ balances, are deposit, mint, withdraw and redeem. Thus, it is useful to filter these four functions and summarize the test results from “Standard” and “Security” levels as shown in Table 1.

Based on the information presented in Table 1, the following observations can be made:

1. There seems to be an issue with the mint function. Since this is the only failed test present after testing the four main functions, it should be investigated first.
2. There are quite a number of inconclusive test results from the mint, withdraw and redeem functions. After cross-checking the reasons for all the inconclusive test results, there seems to be an issue with dealing tokens to dummy users ³. As mentioned previously, the ERC-4626 test suite has two tests, testDealIntendedAssetsToDummyUsers, and testDealIntendedSharesToDummyUsers, which can be used to check if there is some issue with allocating assets and shares to dummy users respectively.
3. Most of the tests regarding the deposit function passed, so this function seems less likely to cause the issue.

To investigate further, it is necessary to examine the possible reasons for failed tests, which can provide more insight into where the possible issues could originate.

Step 4: Find out possible reasons for failing tests

Each test in every token report in ERCx is expandable, which shows more details of the test in JSON format. Figure 8 shows the expanded details of the only failed test for the mint function.

The following two findings are retrieved by investigating the two failed tests:

1. testMintSupportsEIP20ApproveTransferFromAssets 
   The feedback from the failed test states that the mint function does not support EIP-20 approve/transferFrom on asset as a mint flow as stated in EIP-4626. From the decoded_logs of the expanded details, it can be seen that the dummy user, Alice, could not mint shares to herself even though she has provided enough assets’ allowance to the vault. 
2. testDealIntendedSharesToDummyUsers
   The feedback from the failed tests states that there is an issue when allocating shares to dummy users. From the decoded_logs of the expanded details, it can be seen that the two dummy users, Alice and Bob, are unable to mint shares even though each of them has enough assets.

Based on the findings, it seems that the mint function has an issue. The exact issue can be located by looking through the source code contract, which can be found on the token page from Etherscan.

Step 5: Debug source code and call queries

This step requires users to read through the contract's source code and/or make some queries on it. For deployed contracts, users can retrieve the source code and make calls through the Etherscan token page interface. For undeployed contracts, it will be necessary to read directly from the source code and make queries through an IDE, such as Remix. As ERCx4626Mock0 is an undeployed contract where we already have the flatten source code, we can read the code directly. 

After going through the code for the mint function, it became clear that the function has double reentrancy guards (see Appendix for full explanation), which results in it being uncallable. This also explains why most of the property tests for the withdraw and redeem function are inconclusive for this vault. These two functions require shares to be minted to some dummy users before either of the two functions can be called in the property tests. However, as the mint function is uncallable, the test suite is unable to initialize tokens to these dummy users to run the property tests, which causes them to be inconclusive. Thus, to conclude, the double reentrancy guards found in the mint function are indeed a bug that makes it uncallable.

Exercises

The last section covered how to use ERCx to detect issues with contracts. To demonstrate, a link to a list of ERC-4626 vault mutants is provided. This list will offer examples of “good” vaults (i.e., passing all conformance and security tests), as well as “bad” vaults that failed some of these required tests. These “bad” vaults are faulty versions of the “good” vaults generated from a mutation testing tool. These faulty programs are referred to as “mutants”. Mutation testing is a well-studied technique to evaluate and improve the efficacy of a test suite by measuring the number of artificially introduced faults it can detect. The more mutants a test suite can catch, the better the test suite is. Every test suite in the ERCx tool has been subjected to mutation testing and has caught all the possible mutants it can generate. To learn more about how ERCx uses mutation testing to benchmark our test suites, please refer to our previous blog post on Testing ERC-20 Tokens Part 2: Advancing Benchmarking with Mutation Testing.

Here is the link to the list of ERC-4626 vaults that can be used to test ERCx: https://ercx.runtimeverification.com/list/4626-vault-checking-mutants. To view the ERC-4626 test suite report of any token found in the list, click on the token first before clicking on the “ERC-4626” tab under the “Latest Evaluation Report” section.

Can you spot which vaults are the “good” ones and which are the “bad” ones? What is wrong with those “bad” vaults? Since the “bad” vaults are mutated and tweaked from the “good” ones, can you spot the differences between the “good” ones from the “bad” ones?

Concluding Words

In this blog post, we described how we detected issues in an ERC-4626 vault, ERCx4626Mock0, with the help of ERCx. Even though we only looked through an ERC-4626 contract, the method described in this blog post can be generally used to detect issues with the contract you are interested in. Doing conformance and security checks is essential and should be mandatory in preventing bugs and issues in the contracts. As mentioned previously, the bug present in ERCx4626Mock0 is an actual bug that was found in an actual deployed contract, which could have been avoided if the token had been evaluated by ERCx prior to deployment. It is important to note that passing all tests from ERCx does not guarantee that the contract is bug-free (in fact, there is no tool in the world that can do that). Every tool has its shortcomings as well like the ones described in What’s being tested page of ERCx, where test results can be inconclusive if the storage slots of the contract are inaccessible or when the contract deviates too much from standard implementations such as the ones from OpenZeppelin and Solmate. However, running property tests by ERCx is an important first step in ensuring that the contract is conformant and secure up to a certain extent. As ERCx runs property tests through fuzzing, the results may contain false negatives, i.e., some tests that are supposed to fail may pass because the fuzzing test cannot find counterexamples within the limited number of runs. To guarantee that a contract holds certain properties, one must use formal verification tools such as Kontrol or even engage a trained auditor/verification engineer ⁴.

Getting Further and Contributing

Like our ERC-4626 test suite? Want more features for our ERCx tool? Let us know! We are 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. You can also find us at Twitter, Discord and Telegram for more information and updates.

Appendix

In this section, we explain why the mint function is uncallable. From Figure 9, line 2275 to 2285, we can see that the mint function has a nonReentrant modifier applied to it. The purpose of this modifier is to prevent a contract from calling itself, which may result in reentrancy attack. As seen from Figure 10, the modifier works as follows:

1. Ensure the _status (private) variable is set to _NOT_ENTERED
2. Set the variable to _NOT_ENTERED
3. Execute the code of the main function (i.e., the function that called the modifier)
4. Reset the _status variable to _NOT_ENTERED

The issue comes when the mint function calls the deposit function as seen in line 2282 of Figure 9. The deposit function also implements the nonReentrant modifier (line 2258 of Figure 9), which leads to the modifier having applied twice for the mint function. This results in the following sequence of code implemented for the mint function:

Footnotes

1. To know more about the possible outcomes of test results, please refer to https://ercx.runtimeverification.com/whats-being-tested#outcomes. ↩

2.  For the details of each test level, please refer to https://ercx.runtimeverification.com/whats-being-tested#testlevels. ↩

3. In order to run the tests in the test suites, assets and/or shares are allocated to dummy users so that they have sufficient appropriate tokens to exchange between the shares and assets during running of the tests. ↩

4.  If you need a trained auditor/verification engineer to check and verify your contract, you can contact us at https://runtimeverification.com/contact. You can also find us at Twitter, Discord and Telegram. ↩