Detecting critical smart contract vulnerabilities with MythX
MythX integrates static and dynamic analysis to detect security flaws in smart contracts. But how do you unleash this security analysis on your code? In this article I’ll show the use of Sabre, a JavaScript tool I made when MythX was first released, to detect critical smart contract vulnerabilities (in the meantime there’s also an officially supported command line interface). Updated January 2020.
While Turing-complete smart contracts are awesome, the added flexibility also allows programmers to introduce many types of security vulnerabilities. With the right tooling however, many critical flaws can be caught early in the development lifecycle.
MythX integrates static analysis, symbolic analysis and input fuzzing the detect security bugs. There are two main ways this can be used:
- Built-in detectors search for common anti-patterns and behaviours that are most likely bad, such as when anybody can kill the contract or the result of an overflowing arithmetic instruction ends up in storage. This “out-of-the-box”-type detection is discussed in this article.
- Checking custom security properties using assertions. Basically this an extension of regular testing, but instead of only checking correctness of your code for specific inputs you verify that the code behaves correctly under all circumstances.
In this article I’ll show the use of Sabre, a MythX command line client, to detect the some of the most prevalent and critical smart contract weaknesses:
If you prefer using your favourite IDE, you can also try our plugins for Remix, Truffle, Visual Studio Code, and other environments. The Solidity code used in this article can be found in the MythX playground repository.
Quick Setup
To try the examples yourself, install Sabre by running:
$ npm install -g sabre-mythxHead to mythx.io and create a MythX account to get an API key.
Set the MYTHX_API_KEY environment variable in your~/.bashrc for added convenience:
export MYTHX_API_KEY=[API_KEY]You can now analyze Solidity files as follows:
$ sabre analyze <FILENAME> [CONTRACT_NAME]By default this triggers a quick analysis which runs for about up to two minutes and is sufficient to reproduce all examples in this article. You can select other analysis modes, “standard” and “deep”, using the --mode argument.
Broken Access Control
Insufficient access controls on critical functions such as Ether transfers and self-destructs are a classic vulnerability. Let’s have a look at a simplified version of the infamous Parity WalletLibrary (specifically, I restricted the maximum number of owners to avoid an unbounded loop. Otherwise, “quick” analysis mode wouldn’t be able to detect the issue — you’d have to use one of the “deeper” analysis modes which run for up to an hour).
Sabre has the following to say:
$ sabre analyze walletlibrarydemo.sol
✔ Loaded solc v0.5.11 from local cache
✔ Compiled with solc v0.5.11 successfully
✔ Analysis job submitted: https://dashboard.mythx.io/#/console/analyses/86b9ccc5-(...)==== Unprotected SELFDESTRUCT Instruction ====
Severity: High
File: /Users/bernhardmueller/Projects/mythx-playground/generic_bugs/walletlibrarydemo.sol
Link: https://swcregistry.io/SWC-registry/docs/SWC-106--------------------
The contract can be killed by anyone.Anyone can kill this contract and withdraw its balance to an arbitrary address.
--------------------
Location: from 135:4 to 135:21selfdestruct(_to)
--------------------
Transaction Sequence:Tx #1:Origin: 0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef [ ATTACKER ]
Function: initWallet(address[],uint256,uint256) [ e46dcfeb ]
Calldata: 0xe46dcfeb000000000000000000000000000000000000000000000000000000000000004000100000001000000000000000000000000800101000004000008004080800020000000000000000000000000000000000000000000000000000000000000000
Decoded Calldata: initWallet((), 28269553043036167502617584180506572983510684017411486979470946713224085506, 0)
Value: 0x0Tx #2:Origin: 0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef [ ATTACKER ]
Function: kill(address) [ cbf0b0c0 ]
Calldata: 0xcbf0b0c0efefefefefefefefefefefefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef
Decoded Calldata: kill(0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef)
Value: 0x0
MythX has determined that it is possible for anyone to kill the contract. The security problem here is that the initWallet function lets anyone set themselves as the owner unless the contract has already been initialised (which doesn’t automatically happen during contract creation).
Note the “transaction sequence” section at the bottom of Sabre’s output: This shows the sequence of function calls required to reproduce the issue. Note that the sender address 0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef represents the attacker. The first transaction calls the initWallet function which has the prototype:
function initWallet(address[] memory _owners, uint _required, uint _daylimit);The concrete example provided by Sabre is:
initWallet((), 28269553043036167502617584180506572983510684017411486979470946713224085506, 0)address[] ownersis an empty list, making the attacker the sole owner;uint requiredis a random value (it doesn’t really matter for the purpose of killing the wallet);uint _daylimitis 0 (any value would work here).
The second function call is:
kill(0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef)Which kills the contract account and sends its balance to the attacker. Note that MythX prefers to make the attack profitable but also reports a bug if the contract can “only” be killed 🙃
Integer Overflows and Underflows
Integer arithmetic bugs are another common security flaw. Have a look at TokenSale, a vulnerable contract snagged from Steve Marx’s Capture the Ether. Spoiler: It contains at least one exploitable integer overflow. Here is what Sabre reports (boring results removed):
$ sabre analyze tokensale.sol✔ Loaded solc v0.5.11 from local cache
✔ Compiled with solc v0.5.11 successfully
✔ Analysis job submitted: https://dashboard.mythx.io/#/console/analyses/d5b2(...)==== Integer Overflow and Underflow ====
Severity: High
File: /Users/bernhardmueller/Projects/mythx-playground/generic_bugs/tokensale.sol
Link: https://swcregistry.io/SWC-registry/docs/SWC-101--------------------
The binary multiplication can overflow.The operands of the multiplication operation are not sufficiently constrained. The multiplication could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion.--------------------
Location: from 21:29 to 21:56numTokens * PRICE_PER_TOKEN
--------------------
Transaction Sequence:Tx #1:
Origin: 0xaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa [ USER ]
Function: buy(uint256) [ d96a094a ]
Calldata: 0xd96a094a0000800000000000000000000000000000000000000000000000000000000000
Decoded Calldata: buy(883423532389192164791648750371459257913741948437809479060803100646309888)
Value: 0x0
This tells us that both the multiplication in line 21 can overflow:
More specifically, MythX is telling you that there are no appropriate checks on the variables used in these arithmetic operation and that the overflow isn’t caught by an assertion or revert() statement. By overflowing numTokens * PRICE_PER_TOKEN such that the result is zero, an attacker can add a large amount of tokens to their balance without transferring any Ether.
You can “abuse” MythX to obtain the precise integer value required to mint a large number of tokens while sending zero ETH by adding an assertion to the code. To get the solution to the challenge add the following line at the end of the buy function:
assert(msg.value > 0 || numTokens == 0);
This adds a check that verifies that numTokens is always zero unless msg.value (the amount of Ether sent) is greater than zero. We already know that a counterexample exists where msg.value is exactly zero, so let’s run another analysis and see if MythX finds this example:
$ sabre analyze tokensale.sol
(...)==== Assert Violation ====
Severity: Low
File: /Users/bernhardmueller/Projects/mythx-playground/generic_bugs/tokensale.sol
Link: https://swcregistry.io/SWC-registry/docs/SWC-110--------------------A reachable exception has been detected.It is possible to trigger an exception (opcode 0xfe). Exceptions can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. Note that explicit `assert()` should only be used to check invariants. Use `require()` for regular input checking.--------------------
Location: from 25:8 to 25:47assert(msg.value > 0 || numTokens == 0)--------------------Transaction Sequence:Tx #1:
Origin: 0xaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa [ USER ]
Function: buy(uint256) [ d96a094a ]
Calldata: 0xd96a094a0000400000000000000000000000000000000000000000000000000000000000
Decoded Calldata: buy(441711766194596082395824375185729628956870974218904739530401550323154944)
Value: 0x0
The solution to the challenge is:
buy(441711766194596082395824375185729628956870974218904739530401550323154944)Note that you can use Solidity assertions to check custom security properties (I’ve written a separate article about this).
Weak Randomness
Here is another vulnerable contract “borrowed“ (stolen) from Steve Marx’s Capture the Ether (I updated the code for compatibility with solc 5). It’s a lottery smart contract that pays out Ether to lucky players who correctly guess a random number.
To analyze this contract with Sabre, save it to a file named random.sol and run sabre random.sol. This should return a list of security issues (I filtered out the relevant results):
$ sabre analyze guesstherandomnumber.sol
✔ Loaded solc v0.5.11 from local cache
✔ Compiled with solc v0.5.11 successfully
✔ Analysis job submitted: https://dashboard.mythx.io/#/console/analyses/2fc6ef94-2c87-4d82-aeda-46b682c48928==== Unprotected Ether Withdrawal ====
Severity: High
File: /Users/bernhardmueller/Desktop/guesstherandomnumber.sol
Link: https://swcregistry.io/SWC-registry/docs/SWC-105--------------------Anyone can withdraw ETH from the contract account.Arbitrary senders other than the contract creator can withdraw ETH from the contract account without previously having sent an equivalent amount of ETH to it. This is likely to be a vulnerability.--------------------
Location: from 19:12 to 19:40msg.sender.transfer(2 ether)
--------------------Transaction Sequence:
Tx #1:
Origin: 0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef [ ATTACKER ]
Function: guess(uint256) [ 9189fec1 ]
Calldata: 0x9189fec1ad3228b676f7d3cd4284a5443f17f1962b36e491b30a40b2405849e597ba5fb5
Decoded Calldata: guess(78338746147236970124700731725183845421594913511827187288591969170390706184117)
Value: 0xde0b6b3a7640000==== Weak Sources of Randomness from Chain Attributes ====
Severity: Medium
File: /Users/bernhardmueller/Desktop/guesstherandomnumber.sol
Link: https://swcregistry.io/SWC-registry/docs/SWC-120--------------------
Potential use of a weak source of randomness "blockhash".Using past or the current block hashes through "blockhash" as a source of randomness is predictable. The issue can be ignored if this is unrelated to randomness or if the usage is related to a secure implementation of a commit/reveal scheme.--------------------Location: from 8:52 to 8:79blockhash(block.number - 1)==== Weak Sources of Randomness from Chain Attributes ====
Severity: Medium
File: /Users/bernhardmueller/Desktop/guesstherandomnumber.sol
Link: https://swcregistry.io/SWC-registry/docs/SWC-120--------------------Potential use of a weak source of randomness "block.number".Using past or the current block hashes through "block.number" as a source of randomness is predictable. The issue can be ignored if this is unrelated to randomness or if the usage is related to a secure implementation of a commit/reveal scheme.--------------------
Location: from 8:62 to 8:74block.number
Note that MythX reports both the use of environment variables as sources of randomness (SWC-120) as well as the vulnerability resulting from the use of those variables to determine whether Ether can be withdrawn. Indeed, an attacker can withdraw 2 ETH from the contract account by calculating keccac256(block.blockhash(block.number — 1)) for the block in which the transaction is mined. In this case however MythX cannot produce the correct answer in advance since it depends on the block number and block hash in the environment of the concrete contract instance. Try exploiting this for yourself if you’re feeling lucky!
Re-Entrancy
Ever since the infamous DAO hack, re-entrancy has taken the Ethereum security community by storm. If one would to have to pick the ultimate smart contract security bug, it would certainly be re-entrancy.
The SWC Registry has a couple of examples for re-entrancy. Reentrance by Alejandro Santander of OpenZeppelin replicates the DAO flaw in a simplified way. Here is what Sabre reports (extra results removed):
$ sabre analyze Reentrance.sol✔ Loaded solc v0.5.11 from local cache
✔ Compiled with solc v0.5.11 successfully
✔ Analysis job submitted: https://dashboard.mythx.io/#/console/analyses/c2606d3c-3f77-4d3e-a72d-a1a55a534749==== Reentrancy ====
Severity: HighFile: /Users/bernhardmueller/Projects/mythx-playground/truffle_project/contracts/Reentrance.solLink: https://swcregistry.io/SWC-registry/docs/SWC-107
--------------------persistent state write after callThe persistent state (storage or balance) of a contract was accessed after a call to an external contract. To prevent reentrancy issues, make sure the callee is trusted or access the persistent state before the call.--------------------
Location: from 29:6 to 29:41
balances[msg.sender].sub(_amount);
--------------------Transaction Sequence:Tx #1:
Origin: 0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe [ CREATOR ]
Function: withdraw(uint256) [ 2e1a7d4d ]
Calldata: 0x2e1a7d4d000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
Decoded Calldata: withdraw(0)
Value: 0x0
There are two parts to this problem. First, a call to msg.sender is executed (line 26). Following the call there is a write to the persistent state variable balances[msg.sender] in line 30.
Persistent account state should never be updated after calls to untrusted addresses. In the example above, msg.sender can point to a smart contract account that contains code to re-enter the withdraw() function. By recursively calling back into withdraw(), an attacker can withdraw Ether multiple times before the amount withdrawn is subtracted from the attacker’s balance. Check out SWC–107 for more information.
GUI integration
If for some reason you’re command-line-averse you can use the MythX plugins for Remix or VS Code to analyze the examples shown. This will get you the same results but with a nicer user experience. You can also view the reports for all your past analyses on the MythX dashboard.
TL;DR
The MythX detects security analysis API many generic security bugs out-of-the-box. Use MythX tools to analyze Ethereum smart contracts for security vulnerabilities and verify the correctness of smart contracts. Sign up for a free account at https://mythx.io.
