Project 0x Case Study
Abstract
Smart contracts facilitate the transfer of value and help determine digital asset behavior. This results in a higher need for formal proofs and computer-aided checks compared to traditional software which does not typically perform these functions. 0x is an open protocol that enables the peer-to-peer exchange of assets on the Ethereum blockchain. It is one of the largest open protocols with over 30 projects building on top of it, amassing over 713,000 total transactions, and a volume of $750 million.
0x release v3.0 went live on December 2nd 2019. The release included a significantly more complex exchange environment. As such, 0x sought out MythX, along with Consensys Diligence, to perform a manual security audit in order to increase confidence in the correctness of the smart contract code.
MythX performed the following techniques in the 3.0 branch of the 0x monorepo:
- Run MythX Pro to check each smart contract individually for bugs
- Execute fuzzing campaigns on a live multi-contract environment using the Harvey greybox fuzzer
- Verify correctness properties of the smart contracts using symbolic execution and greybox fuzzing
As a result:
- 37 potential issues were detected by MythX Pro
- 149 potential issues were detected by MythX’s extended greybox fuzzing campaign
- 5 custom contract properties were verified through custom checks
Continuously verifying the code using MythX, including the custom checks built-in this project, was recommended to prevent regressions and new security issues.
Problem statement
0x’s network of decentralized exchanges has processed over $750 million since inception. As such, 0x wanted to ensure that no funds would be at risk during the transition from v2.0 to v3.0. The v3.0 release has a more complicated exchange environment due to an increased amount of smart contracts interacting with each other, resulting in more complexities and potentially introducing hidden bugs. 0x’s need to deeply analyze the code, integrate continuous analysis into their deployment pipeline, and verify specific contract properties led to a natural partnership with MythX. Both automated analysis and human auditing was conducted to ensure high confidence that the v3.0 release would be secure and bug-free.
“Working with the MythX team solidified our perspective on the effectiveness of fuzz testing, and strengthened the trust in the audit report Consensys led on our v3.0 release.” – 0x Team
Smart contract security solution
MYTHX PRO VULNERABILITY SCAN
MythX Pro, a security analysis tool that detects 26 different classes of security vulnerabilities by performing static analysis, dynamic analysis, and symbolic execution, was used to detect smart contract bugs on 197 contracts. Each smart contract was compiled individually and checked against a class of known vulnerabilities from the SWC registry. The SWC registry is a database that contains a list of known smart contract vulnerabilities, with each known vulnerability having its own SWC identifier (ID). The following table lists the bug classes that were tested for. A checkmark in the “Pass” column indicates that no issues were detected in the category, while an “X” indicates that one or more issues in the category were found.
Table 1: Vulnerabilities checked with MythX Pro
In addition, a coverage estimate was generated to estimate the residual risk that a new path or behavior would appear. This is helpful because input fuzzing is a randomized process and does not yield a guarantee that all issues have been discovered. Diagram 4 shows the estimated residual risk for the smart contracts that were analyzed. Having a lower estimated residual risk value indicates that the chances of a new vulnerability or behavior appearing is low.
Diagram 3: Estimated residual risk of the analyzed smart contracts
In total, Harvey discovered 149 issues.
Table 2: Harvey discovered issues
Diagram 4: Vulnerabilities found sorted by SWC types
The results were reviewed manually to understand why the issues were flagged, with a greater focus on the issues that were most likely to cause security risks such as re-entrancy and improper handling of external calls. All 22 instances of SWC-104, SWC-107, and SWC-113 were reviewed. The review did not uncover exploitable vulnerabilities. It was also noted that the issues with the highest risk were intended by the 0x developers. For example in Example 1, the transaction would not be reverted for failing calls, which could result in propagating the failure. However, this issue along with the others detected are mitigated since the contract that could exploit the vulnerabilities is a “trusted” contract, which is another 0x contract.
Example 1: How the transaction will not revert if the call fails
VERIFICATION OF CUSTOM PROPERTIES
Custom tests for five security properties were created for the 20 deployed smart contracts to check the intended behavior of specific contracts, also known as functional correctness. Fuzzing, symbolic execution, and SMT solving were used to determine whether the smart contracts behaved correctly with respect to the properties.
Generally, such tests are implemented by inserting runtime assertions into the code. MythX or offline versions of Harvey and Mythril, an analysis tool that performs symbolic execution and SMT solving, are then used to detect counterexamples.
The custom properties were chosen by referring to 0x’s design document on bug classes to avoid and to see which bugs were expressible for 0x’s codebase. Table 2 shows which properties were checked for. A check mark indicates that this property holds where an “x” indicates detected unintended behavior.
Table 2: List of custom properties checked for against 0x’s codebase
Three instances of integer underflows were detected for the property, Fixedpoint Integer Arithmetics.
Example 2: Outputs of three instances of integer underflows
In addition to the checks listed above in Table 2, another custom check for a more specific property was created based on an issue discovered by the Consensys Diligence audit team. The check verifies the complex state invariants for the MixinStorage contract. After using Harvey, it was determined that the code responsible for the issue was not part of the contracts that were deployed to the mainnet. It will be possible to automatically check the property once this contract is part of the migrated contracts. This would be an example of checking for violations during the course of the development life cycle.
Conclusion
The MythX team was able to detect 37 potential issues using MythX Pro, 149 potential issues using MythX’s extended greybox fuzzing campaign, and verified 5 custom contract properties through custom checks. To prevent regression and newly introduced security bugs, continuously verifying the code using MythX, including the custom checks built in this project, was recommended.
TECHNICAL MILESTONES
The completion of the 0x project performed by both MythX and Consensys Diligence not only resulted in high confidence that the upcoming 0x v3.0 release will be secure, it has also produced a significant milestone for Ethereum security.
- MythX Pro is the first automated security analysis tool that is able to perform both symbolic execution and fuzzing on a major project
- Comprehensive coverage and realistic analysis and testing was performed by deploying smart contracts to a local testnet and extracting information to create the initial state (deployed state) for the greybox fuzzing campaign
- The estimated residual risk on the likelihood that a new path or behavior would appear was calculated on smart contracts analyzed by our Harvey greybox fuzzer
“Working with the MythX team solidified our perspective on the effectiveness of fuzz testing, and strengthened the trust in the audit report Consensys led on our v3.0 release.” 0x Team
TECHNOLOGY PARTNERSHIP
About MythX
MythX, a Consensys product, scans for security vulnerabilities in Ethereum smart contracts. Its comprehensive range of analysis techniques which include static analysis, dynamic analysis, and symbolic execution, accurately detects security vulnerabilities and provides an in-depth analysis report. With a vibrant ecosystem of world-class integration partners that amplify developer productivity, MythX can be utilized in all phases of the smart contract development lifecycle.
For more information, visit mythx.io
About Consensys Diligence
Our smart contract auditing and blockchain security services are delivered by a highly experienced team, driven by their passion for enabling more secure platforms and ecosystems. Consensys Security auditors and researchers are distributed all over the world and focused on creating tools that are truly helpful to auditors and smart contract developers.
For more information, visit diligence.consensys.net
Thinking about smart contract security? We can provide training, ongoing advice, and smart contract auditing. Contact us.