Checking Custom Correctness Properties of Smart Contracts Using MythX

Valentin Wüstholz
Oct 8, 2019 · 3 min read

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:

Image for post
Image for post
Output of running MythX on the contract (with custom property check)

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.

ConsenSys Diligence has the mission of solving Ethereum…

Sign up for Smart Contract Security Newsletter

By ConsenSys Diligence

The goal of this newsletter is to help you keep up with, (and understand) the latest attacks, threats and defenses, and security best practices in the blockchain and smart contract security. Take a look

By signing up, you will create a Medium account if you don’t already have one. Review our Privacy Policy for more information about our privacy practices.

Check your inbox
Medium sent you an email at to complete your subscription.

Valentin Wüstholz

Written by

ConsenSys Diligence
Valentin Wüstholz

Written by

Software Security Researcher at ConsenSys Diligence

ConsenSys Diligence

ConsenSys Diligence has the mission of solving Ethereum smart contract security. Contact us for an audit at

Medium is an open platform where 170 million readers come to find insightful and dynamic thinking. Here, expert and undiscovered voices alike dive into the heart of any topic and bring new ideas to the surface. Learn more

Follow the writers, publications, and topics that matter to you, and you’ll see them on your homepage and in your inbox. Explore

If you have a story to tell, knowledge to share, or a perspective to offer — welcome home. It’s easy and free to post your thinking on any topic. Write on Medium

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store