MythX Pro Security Analysis Explained

MythX recently went live with a new Pro upgrade that offers more powerful analysis features than the free version. In this article I’ll explain how the new “full” analysis mode affects the performance of MythX.

MythX is a smart contract security service that integrates multiple analysis techniques. The MythX Pro plan comes with a new analysis mode called Full mode. In this mode, submitted contracts are subjected to a thorough fuzzing campaign and deep inspection using symbolic analysis. It discovers complex security issues and can be used for checking the correctness of smart contracts.

Background

When you submit a smart contract to MythX, the analysis service spawns a number of workers that perform various analysis tasks in parallel. Each worker is given a maximum time budget it may spend on testing the code. The more computing time is available, the higher the coverage achieved by the analysis engine (at the cost of having to wait longer for the results).

MythX clients can choose between two configuration presets (“modes”) via the analysisMode request parameter. Most MythX tools use Quick mode by default. In Quick mode, the time limit for analysis is 120 seconds. Quick mode is effective at finding bad coding patterns and low-complexity bugs but may miss complex bugs due to the limited computing time available.

Pro users can also select Full mode, which increases the computing time to 30 minutes. This allows the tools to explore a much larger space (up to 90 times more) of program states and execution paths.

Analysis specifications: MythX vs. MythX Pro

Analysis specifications: MythX vs. MythX Pro

Example

To demonstrate how this difference plays out in practice we’ll look at an all-time favorite: Parity WalletLibrary, the smart contract that famously self-destructed (I updated the code to be compatible with solc 0.5). Here, an initialization function is exposed due to an uninitialized variable, allowing anyone to take ownership of the contract account and subsequently call the kill() function.

MythX Quick mode reports a total of six issues for this contract (you can reproduce this with the Remix plugin):

Floating Pragma

A floating pragma is set. It is recommended to make a conscious choice on what version of Solidity is used for compilation. Currently multiple versions "^0.5.0" are allowed.
Location: Line 13

State Variable Default Visibility (4 instances)

It is best practice to set the visibility of state variables explicitly. The default visibility for state variables is internal. Other possible visibility values are public and private.
Locations: Lines 95, 99, 101 and 102

Potential denial-of-service if block gas limit is reached.

A storage modification is executed in a loop. Be aware that the transaction may fail to execute if the loop is unbounded and the necessary gas exceeds the block gas limit.
Location: Line 140 to 144

Note that the “kill” bug is not detected! Full analysis however reports an additional issue:

Unprotected SELFDESTRUCT Instruction

Anyone can kill this contract and withdraw its balance to an arbitrary address.
Location: Line 163

Transaction Sequence:

Tx #1:
Origin: 0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef [ ATTACKER ]
Decoded Calldata: initMultiowned()
Value: 0x0

Tx #2:
Origin: 0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef [ ATTACKER ] 
Decoded Calldata: kill(0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef)
Value: 0x0

Why is this bug not detected in Quick mode? The answer lies in the unbounded loop in the function initMultiowned (in practice it’s bounded by the block gas limit) which makes the function costly to analyze. In Quick mode, the tools simply don’t have enough resources available to unroll and analyze the code. In Full mode however this is easy pickings for the symbolic analyzer.

The function initMultiowned contains a loop bounded by the length of a dynamically sized array.

The function initMultiowned contains a loop bounded by the length of a dynamically sized array.

When to use Quick vs. Full analysis?

As we have seen, Quick mode gives useful feedback but can miss important bugs. It is meant to provide rapid synchronous feedback during development and deployment, for example:

  • Running an analysis from Remix or Visual Studio Code to highlight best practice violations and potential vulnerabilities during development;
  • Checking all Solidity files in the project on pull requests to a development branch, when you don’t want to wait for hours before merging.

You should definitely use Full mode in the following cases:

  • Before deploying the smart contract to the blockchain;
  • When checking custom security properties (when you want to have high confidence that the property always holds).

You should definitely use Full mode before deploying to the blockchain.

Activating Full Analysis Mode

MythX tools usually offer a configuration setting or command line argument to select the analysis mode. In Remix, Full mode is started with the “Run full mode” button. The analysis requires around 30 minutes to complete, and you can view the report on your MythX dashboard once it’s done.

full mode remix

In MythX for VS Code, open the command palette and choose “MythX: Run Full Mode Analysis”.

mythx vs code

In MythX for Truffle, full analysis is selected by adding –mode full to the command line:

$ truffle run verify --mode full

The same command line argument is supported by MythX CLI and Sabre.

$ mythx analyze --mode full ./

$ sabre analyze --mode full wallet.so

About MythX

MythX is the leading platform for smart contract bug detection and security verification. Set up a free account and install some awesome MythX tools to get started!

Thinking about smart contract security? We can provide training, ongoing advice, and smart contract auditing. Contact us.

All posts chevronRight icon

`