Checking Custom Correctness Properties of Smart Contracts Using MythX
Previous attacks on smart contracts, such as the DAO attack and the Parity attacks, have demonstrated that it is incredibly challenging to write correct and secure contracts. Given how much money and reputation is on the line, developers need to use the complete arsenal of techniques at their disposal to eradicate bugs in contracts before deployment. Luckily, automated analysis tools are constantly improving and new techniques are being developed to detect bugs more reliably and, in some cases, prove their absence. This also holds for the tools that power our MythX smart contract analysis service, such as Mythril and Harvey. In this post, we will demonstrate how to use such tools more effectively to catch intricate bugs in contracts.
Imagine you were developing the following smart contract:
The contract implements a simple token for storing and transferring assets between users. It is written in the Solidity programming language and conforms to the widely-used ERC20 API.
During development, you obviously made sure to address all warnings or issues that were reported by the compiler. On top of that, you also ran our MythX analysis service and addressed all the issues it detected.
Since there are no more issues, the contract should be ready for deployment, right? Well, not quite… How can you be sure it actually does what it is supposed to do? There are a few common techniques to answer that question: for instance, you might want to write tests that exercise different usage scenarios or even hire auditors (such as our friends at ConsenSys Diligence) to make sure you did not miss something.
Most automated tools try to detect generic issues, such as reentancy or arithmetic overflows. However, to check custom properties about the intended behavior of a specific contract (often referred to as “functional correctness properties”), tools need some help. For instance, it would be great if the developer or an auditor could provide some description of what is considered “intended behavior” and the tool would report any unintended behavior as issues. If you are using MythX you can do this out-of-the-box, provided you have some properties in mind that you want to check.
For example, the transfer function should never change the sum of the two balances for msg.sender and _to. We can easily add a runtime check for such a property by adding the transferEnsures modifier to the transfer function:
We can see that the modifier stores the sum before entering the body of the transfer function in a local variable. After executing the body (_ placeholder) it checks the above property by emitting a special AssertionFailed(string) event in case it is violated. MythX will report paths to the AssertionFailed(string) event as a vulnerability. While MythX will also report violations of built-in assert-statements, the above approach allows you to specify a nice message that helps with understanding the tool’s warnings and, if necessary, mapping them to locations in the source code.
After making these minor changes to the contract, we can perform another MythX scan:
It turns out that under certain conditions the property is violated! If we inspect the transaction data (see the transaction sequence at the bottom of the above screenshot) we can see that the property only fails if one transfers tokens to oneself (msg.sender == _to). Such a case is easily missed when manually writing test cases. However, automated analysis tools are able to explore it and create a runnable test case for you to inspect.
In this post we have demonstrated how we can get more out of our automated analysis tools by adding custom check for functional correctness properties via the AssertionFailed(string) event. Such checks are able to reveal more contract-specific issues than the built-in checks for arithmetic overflows or reentrancy.
To catch even more bugs make sure to give our MythX full mode analysis a try! It runs a much deeper analysis by exploring more program paths and longer transaction sequences for up to 30 minutes (as opposed to 2 minutes for our quick mode).
Thanks to Bernhard Mueller and Nathan Peercy for feedback on drafts of this article.
