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

Contract invariants are properties of the program program state that are expected to always be true. In my previous article I discussed the use of Solidity assertions to check contract invariants. This article expands on the use of invariants and provides a couple of additional examples.

An interesting feature of invariant checking on the bytecode level is that it allows you to detect low-level issues, including issues caused by compiler optimisation or idiosyncrasies of the programming language, by defining high-level rules. For instance, in the last article we saw that a high-level rule “the contract should always remain unlocked” could be broken by exploiting Solidity memory addressing. Let’s look at some more examples for the effectiveness of contract invariants.

Example 1: Integer rounding

Integer divisions in Solidity round down to the nearest integer. Failure to consider the rounding behaviour can lead to bugs and vulnerabilities. Consider the example from Sigma Prime’s blog post which also has a great writeup on this bug class:

pragma solidity ^0.5.0;

contract FunWithNumbers {

    uint constant public tokensPerEth = 10;
    uint constant public weiPerEth = 1e18;

    mapping(address => uint) public balances;

    function buyTokens() public payable {
        uint tokens = msg.value/weiPerEth*tokensPerEth; // convert wei to eth, then multiply by token rate
        balances[msg.sender] += tokens;
    }

    function sellTokens(uint tokens) public {
        require(balances[msg.sender] >= tokens);
        uint eth = tokens/tokensPerEth;
        balances[msg.sender] -= tokens;
        msg.sender.transfer(eth*weiPerEth); 
    }
}

Let’s put on the auditor’s hat and come up with some meaningful properties to check. Amongst other things we could assert that, when comparing the contract account state at the beginning and end of a transaction, the following should always be true:

1. The token balance of msg.sender increases when the contract account balance increases;
2. The contract account balance increases when the token balance of msg.sender increases;
3. The token balance of msg.sender decreases when the contract account balance decreases;
4. The contract account balance decreases when the token balance of msg.sender decreases.

This could be generalised even more (e.g. the sum of all token balances increases if and only if the contract balance increases) and supplemented with additional checks (balance always increases by the right amount, …) to catch more possible bugs.

MythX supports standard Solidity assertions and the MythX AssertionFailed event which allows you to add a custom error message. One way of checking contract invariants is by creating a modifier to wrap all public and external functions. This ensures that the invariant holds at the end of all internal message calls and transactions. This approach has some limitations but let’s roll with it the meantime (support for inline specifications is coming to MythX soon™).

Typically we’ll create modifier along the following lines:

modifier checkInvariants {    

  // Save old state
  uint sender_balance_old = balances[msg.sender];    
  
  // Execute the function body
  _;

  // MythX AssertionFailed event    
   if (--- this should never occur ---) {
       emit AssertionFailed("Some error message");
    }

   // Solidity assertion    
   assert(--- this should always hold ---);
}

We’ll add the checks by creating a wrapper contract and overriding the public functions in FunWithNumbers:

contract VerifyFunWithNumbers is FunWithNumbers {
    
    uint contract_balance_old;
    
    constructor() public {
        contract_balance_old = address(this).balance;
    }
    
    event AssertionFailed(string message);
    
    modifier checkInvariants {
        uint sender_balance_old = balances[msg.sender];
        
        _;
        
        if (address(this).balance > contract_balance_old && balances[msg.sender] <= sender_balance_old) {
            emit AssertionFailed("Invariant violation: Sender token balance must increase when contract account balance increases");
        }
        if (balances[msg.sender] > sender_balance_old && contract_balance_old >= address(this).balance) {
            emit AssertionFailed("Invariant violation: Contract account balance must increase when sender token balance increases");
        }
        if (address(this).balance < contract_balance_old && balances[msg.sender] >= sender_balance_old) {
            emit AssertionFailed("Invariant violation: Sender token balance must decrease when contract account balance decreases");
        }
        if (balances[msg.sender] < sender_balance_old && address(this).balance >= contract_balance_old) {
            emit AssertionFailed("Invariant violation: Contract account balance must decrease when sender token balance decreases");
        }
        
        contract_balance_old = address(this).balance;
    }function buyTokens() public payable checkInvariants {
        super.buyTokens();
    }
            
    function sellTokens(uint tokens) public checkInvariants {
        super.sellTokens(tokens);
    }
}

Running this contract through the MythX Remix plugin detects two invariant violations. Let’s have a closer look at the reported issues.

The first counterexample produced by MythX shows a user attempting to buy tokens with a very low call value of 6 Wei. In this case, the 6 Wei get added to the contract balance but the balance of the user does not increase.

Taking another look at the code, we can see that if less than 1 Ether is sent when calling buyTokens(), the result of the division msg.value/weiPerEth will be rounded down to 0 and the subsequent multiplication with tokensPerEth will likewise return 0.

The second counterexample shows a user first buying one Ether (1000000000000000000 Wei) worth of tokens (transaction 2), then selling 6 tokens (transaction 3). This deducts 6 tokens from the user’s balance but does not transfer any Ether to the user due to the rounding error in sellTokens(uint tokens) : uint eth = tokens/tokensPerEth will be rounded down to 0 if tokens is lower than 10 or to the nearest multiple of 10 otherwise.

Example 2: Arbitrary storage writes via large-sized arrays

A couple of years ago I wrote about proving security properties using the open-source tool Mythril. By checking contract invariants with MythX you can achieve similar results. It is however important to point out the difference between the two methods:

• The method shown previously was based on under-constrained symbolic execution of the runtime bytecode (using an older version of Mythril) whereby storage variables were initialised as symbolic variables. This method detects all instances of a bug but also returns false positives.
• MythX combines symbolic execution and input fuzzing after partially initialising the contract account state with the concrete values. By doing this it avoids false positives but there’s a residual risk of false negatives. The risk of missing bugs declines the longer the tools are allowed to run.

With that said, let’s revisit the example shown in the old article which was based on Doug Hoyte’s classic USCC submission. This smart contract contains a hidden method of overwriting the owner state variable:

pragma solidity ^0.5.0;

contract Pwnable {
    address public owner;
    uint[] private bonusCodes;
    
    constructor() public {
        bonusCodes = new uint[](0);
        owner = msg.sender;
    }
    
    function PushBonusCode(uint c) public {
        bonusCodes.push(c);
    }
    
    function PopBonusCode() public {
        require(0 <= bonusCodes.length);
        bonusCodes.length--;
    }
    
    function UpdateBonusCodeAt(uint idx, uint c) public {
        require(idx < bonusCodes.length);
        bonusCodes[idx] = c;
    }
}

To catch improper modifications of the owner variable we can informally define the property:

• The owner must not change in the course of the transaction unless the transaction sender matches the existing owner.

Which translates to the following Solidity assertion:

assert(owner == old_owner || msg.sender == old_owner);

Using the aforementioned method of creating a wrapper around the Pwnable contract, we get:

contract VerifyPwnable is Pwnable {   

  modifier checkInvariants {
        address old_owner = owner;       
        _;        
        assert(msg.sender == old_owner || owner == old_owner);
     }
    
     function PushBonusCode(uint c) public checkInvariants {
         super.PushBonusCode(c);
     }    

    function PopBonusCode() public checkInvariants {
        super.PopBonusCode();
    }   

    function UpdateBonusCodeAt(uint idx, uint c) public checkInvariants {
        super.UpdateBonusCodeAt(idx, c);
    }}

This time MythX detects one assert violation in the code:

Apparently there is a way to change the contract owner even though the state variable owner is not explicitly accessed anywhere in the code. This happens due to the way dynamically sized arrays are laid out in storage:

• The length of the array uint[] bonusCodesis stored at storage slot 1;
• Accessing array element n points to storage address keccak(1) + n.

The state variable owner lives at storage slot 0. To access it, one must first underflow the unsigned integer variable bonusCodes.length which happens in the first function call:

• PopBonusCode()

In the second call we write to the array index that equals(MAX_UINT — keccak(1)). This will result in a write to the storage address keccak(1)+(MAX_UINT — keccak(1)) which overflows into 0:

• UpdateBonusCodeAt(35707666377435648211887908874984608119992236509074197713628505308453184860938, 0)

Voila! The owner is now set to the zero address (to set it to any other address, convert it to an unsigned integer and pass it with the second argument). You can try this out with the Remix JavaScript VM or Ganache to verify that it works.

It’s worth pointing out that even without the assertion, MythX automatically detects the two individual flaws that make the owner overwrite possible. The first issue is the integer overflow caused by decreasing bonusCodes.length. Note that this is not possible anymore with solc 6.0 or higher which makes the array length read-only.

Additionally, MythX reports that a writes to an arbitrary storage location are possible following the length underflow:

TL;DR

By checking high-level invariants using symbolic execution and input fuzzing you can verify assumptions about how your code behaves. This can uncover unexpected bugs caused by peculiarities of the Solidity programming language, such as rounding errors, unsafe integer arithmetics and addressing of elements in storage.

By the way, all examples in this article can be reproduced using the free version of MythX. You should try it out!

In previous posts, we introduced Harvey, a fuzzer for Ethereum smart contracts, and presented two techniques to boost its effectiveness: input prediction and multi-transaction fuzzing.

Harvey is being developed by MythX in collaboration with Maria Christakis from MPI-SWS. It is one of the tools that powers our smart contract analysis service. Sign up for our free plan to give it a try!

In this post, we summarize our upcoming ICSE 2020 paper and provide a high-level overview of how we use online static analysis to guide Harvey. If you are not familiar with fuzzing we suggest to check out the above post since we will assume some basic background below.

Targeted fuzzing

Let’s assume that there are specific target locations in a program you want to fuzz. For example, these could be locations that were recently modified or contain assertions that should be checked. Or maybe a static analyzer has reported warnings for these locations.

The goal of targeted fuzzing is to generate inputs that explore these locations as quickly and frequently as possible. This is challenging since the fuzzer cannot easily predict if a given input explores locations that are “close” to a target location. Unfortunately, the fuzzer only knows which locations are actually explored by the input.

To help the fuzzer with this task, we perform a static lookahead analysis for each input that is added to its queue of “interesting” inputs. The fuzzer uses this (cyclic) queue to select the next input that will be fuzzed and typically adds inputs that increase coverage.

Lookahead Analysis

The diagram below illustrates the idea behind this novel analysis. Given an input that explores a program path π (bold in the diagram), we consider several so-called split points P₁ to P_n along that path. For each of these points P_i, starting from P₁, we perform a light-weight static analysis that involves two steps.

First, we consider the prefix π_pre of the entire program path π that ends at split point P_i. We compute a condition ϕ that over-approximates all the program states at the split point when executing the prefix. We then check if any target locations are reachable when starting from P_i in a program state that satisfies the condition ϕ. In other words, we check if there are any program paths (with prefix π_pre) that reach a target location. In the diagram, the triangles represent sets of paths.

As soon as no targets are found in the second step, we stop the lookahead analysis and we consider the corresponding prefix π_pre to be a so-called no-target-ahead prefix. The fuzzer records the split points along this prefix and computes a lookahead identifier by hashing the prefix. For instance, in the diagram above π_pre is a no-target-ahead prefix since none of the targets T_x and T_y are reachable from split point P_i.

The lookahead identifier is similar to the path identifier that a greybox fuzzer computes based on which control-flow edges are traversed when executing a given input (see our post on greybox fuzzing for more details). Observe however, that two inputs with different path IDs may share the same lookahead ID if both exercise the same no-target-ahead prefix.

In our implementation, we use Bran, an abstract interpreter for EVM bytecode, to perform the static analysis. Since this analysis runs frequently it needs to be very efficient and light-weight.

Adapting the greybox fuzzing algorithm

Let’s see how we can use this additional information—the split points and the lookahead identifier—to guide the fuzzer. Before that, we will quickly recap the standard greybox fuzzing algorithm below:

// We set up the initial queue by executing the program P for the seed inputs S. 
Q := run_seed_inputs(P, S)
while (running) {
  i := select_input(Q)
  e := assign_energy(i) // Adaptation: We assign energy based on lookahead information.
  while (0 < e) {
    f := fuzz_input(i)
    pid := run_input(P, f)
    if pid not in Q {
      Q[pid] := f
      // Adaptation: We will run the lookahead analysis for input i.
    }
    e := e - 1
  }
}

The fuzzer initially runs the program P with the seed inputs S to initialize the queue Q. While the fuzzer is running, it keeps selecting inputs that will be fuzzed from the queue. It uses a function assign_energy to determine how often a selected input is fuzzed.

When a fuzzed input discovers a new path ID, it is added to the queue (here, a simple map from path ID to input). This is where we run the lookahead analysis (see third comment) to gather additional information about this newly discovered input.

We use this information to adjust how much energy we assign to it in the future (see second comment). We will assign more energy if (1) the input’s no-target-ahead prefix was rarely executed, or (2) any of its split points were rarely executed.

Intuitively, the lookahead ID groups (or partitions) the inputs in the queue since multiple inputs may share the same lookahead ID. The above energy schedule aims to prevent the fuzzer from spending disproportionate amounts of energy on a few partitions that contain many inputs. The split points partition the queue in a similar way and both factors turn out to be important in practice. The key insight is that the fuzzer gains more from discovering inputs that explore new lookahead IDs or new split points than ones that explore existing ones.

Evaluation

We evaluated the effectiveness of this approach on 27 real-world smart contracts and found that the fuzzer was able to reach 83% of the challenging target locations significantly faster (with a speedup of up to 14x). We also found that the overhead of the static analysis was very low (~3s per fuzzing campaign).

In this post, we provided a high-level overview of how we use online static analysis to guide Harvey. For more details please check out our upcoming ICSE 2020 paper.

Thanks to Maria Christakis and Joran Honig for feedback on drafts of this article.

This is the third and last post in the MythX series on integrating security analysis of smart contracts into your Continuous Integration (CI) system. In the first part we built a CircleCI configuration. In the second part we built a small and beautiful Travis CI configuration.

“But I am using a completely different CI system!” – You, maybe.

Fret not. The avid reader might have noticed a common pattern in the past two posts: In setups we used the MythX CLI and a basic Python runtime. If you have not read the previous articles yet, it is recommended to do so. Do not worry, I will wait here.

Generalizing our Approach

Sending things to MythX for analysis is rather simple if you are using one of our many tools and integrations. Roughly speaking we always do the following:

1. Download and set up an official tool
2. Run the tool on one or multiple target files
3. Wait for the results be returned by the MythX API
4. If the report contains anything critical, fail the job

Available Tools

The MythX analysis engine is made available through a REST API. This means that there are analysis tools readily available for most common languages and frameworks. Are you using Truffle? Check out the MythX Truffle plugin. Do you prefer Python and use Brownie? Brownie ships with built-in MythX integration – no setup required. Or do you prefer a minimal JS client to eliminate the Python dependency? Thy sabre! Or maybe you want it as comfortable as possible and not configure your CI server at all. Then Guardrails is for you!

Or simply roll your own. The MythX documentation is a good starting point to build the tool that perfectly fits your needs. You could also dive head-first into our OpenAPI documentation if you prefer looking at data structures instead of text blocks. Whatever your choice is, the MythX team welcomes and supports all builders!

Advanced Usage

This blog series is meant to be a starting point for CI integrations. It is by no means exhaustive. As the main developer behind the MythX CLI I can’t help it however to throw some cool ideas for advanced users out there. All setups described below are possible with the current feature set of the MythX CLI. If you have implemented them in your project, please share your experiences with me. I am determined to polish the application even more, make it more reliable, and I would love to feature your use case in another blog post!

Long Analysis Jobs

So far we have only discussed “quick” mode submissions. These usually take about 120s to finish. A CI server can wait this long. But what if you have a MythX subscription that allows you to do “standard” or “deep” mode scans? These allow for up to 90 minutes of scan time.

Given these long analysis times the CI job would probably time out and fail in any case. The MythX CLI solves this problem by introducing an --async flag. If this flag is given, a list of job IDs will be printed and the CLI will not wait for the analyses to be finished.

This in turn means that scan results are not available inside the CI logs. The submitted scans can be viewed in the MythX dashboard once they are finished. Running asynchronous analyses is as simple as:

mythx analyze --async 

Storing Artifacts

Sometimes you want to persist files from your CI job. Let’s say you have a dedicated security verification pipeline where people are continuously monitoring the state of your smart contracts and fix vulnerabilities once they come up. You now want to provide this pipeline with data as soon as the MythX analysis has finished. Disregarding the specifics of your CI system, the MythX CLI allows for file outputs in various formats. E.g. we can take the analysis results, format them in pretty-printed JSON and store them in a file:

mythx --output security.json --format json-pretty analyze 

In your CI server you can now specify the output directory as an artifact file and e.g. directly push it to AWS S3 with Travis.

Filtering Results

There might be things you do not want to see in the MythX CLI output. For that reason, we have added two features: Severity filtering and SWC blacklisting. If you are tired of us reminding you that your code has a floating pragma statement, simply blacklist this SWC.

mythx analyze --swc-blacklist SWC-103 

If this is not enough, simply add more SWC IDs as a comma-separated list to the parameter. But maybe low severity issues in general are none of your concern and you are only interested in everything above Medium. That’s what the severity filter was made for:

mythx analyze --min-severity high 

Conclusion

Security checks in continuous integration systems are not too hard. When the tooling is right and a little setup time is invested, it is not impossible to always have updated security reports at your fingertips. The Ethereum ecosystem is growing rapidly with innovations in smart contract development being made on a daily basis. It fills me with joy to see such a huge amount of projects that try to make a difference, often just driven by curiosity and passion.

At the same time, it fills me with uncertainty how we secure such massive growth. In a recent analysis with our friends over at Alethio we have found out that the number of smart contract vulnerabilities is on a downward trend. Automated tools, dedicated security auditors, and passionate developers start to value security more and more. I hope that this blog series, and MythX in general can further contribute to this trend.

Stay safe out there!

The MythX platform leverages several internal components to provide the best possible analysis results. One of these components is available open-source; the symbolic executor Mythril. In this article, I’ll demonstrate how you can use Mythril to analyze a set-up of multiple smart contracts.

By default, Mythril will analyze a contract in isolation. Interactions with external contracts are generalized so that we capture all possible vulnerabilities. Sometimes, this means we find a weakness in your smart contract that might not affect your particular setup. That’s because the specific deployment values you use can have a considerable effect on how the system behaves as a whole.

Luckily you can also use Mythril to execute multi-contract analysis and analyze a specific configuration of multiple smart contracts. As a result, you might capture fewer warnings, but the results will be tailor-made to your deployment.

To do multi-contract analysis, we’ll use Mythril’s ability to analyze contracts deployed on an Ethereum network (hint: we’ll use Ganache to launch our private test network). We will deploy our contract on a network, and in doing so, create a possible target for Mythril to analyze.

How To

To perform the multi-contract analysis, we will execute the following steps:

• Deploy a smart contract system to Ganache
• Set up Mythril to load code and world state from Ganache
• ⚡ Fire lasers at the smart contract ⚡

But first, make sure you have everything you need installed:

# The dependencies you will install are: truffle, ganache and mythrilnpm install -g trufflenpm install -g ganache-clipip3 install -U mythril

You will also need to get an example project to try multi-contract analysis on, I’ll be using the simple Metacoin contract.

# These commands create a metacoin directory,# with the metacoin truffle boxmkdir metacoincd metacointruffle unbox metacoin

Deploying your smart contract system to Ganache

We’ll start by getting a test network up and running. This network is where we deploy our contracts and where Mythril will find the smart contract state.

# Execute this command to create a new ganache networkganache-cli -p 7545 --i 5777

With the network set up, we can deploy the contracts; and because we’re using Truffle, this will be quite easy.

truffle migrate

This command will execute all the necessary steps to get your contract set up on the test network we provided. (check out the Truffle documentation for more information on this command)

Now search the ouput of the truffle migrate command for the address where the Metacoin contract (our target) was deployed. 
Look for contract address in the Deploying 'MetaCoin' section.

You can see an example of the output in the image below, where I’ve highlighted the address of the fresh Metacoin Contract: 0x8712c227680bc0c8a4c7a65317C7e7700e5D566f

Analysis Time

With the deployment completed, all that is left is to execute the following command (and possibly enjoy a ☕) :

# This command initiates the multi-contract analysismyth a -a <target_address> -l --rpc localhost:7545

As you can see, there are a few options required, here’s a brief explanation of all the elements in this command:

myth a – This is the analyze command that enables the analysis capabilities of Mythril.
-a <target_address> – This option specifies the analysis target, in our case the Metacoin contract account on the test network.
-l – This second option tells Mythril to not just use the code of the target Account, but to use world state data from the Ethereum network whenever possible.
--rpc localhost:7545 – The rpc option tells Mythril where to find an Ethereum node to get all the necessary data. In our case the node is part of our very own test network, which lives on localhost listening on port 7545.

All Good!

$ myth a -a 0x8712c227680bc0c8a4c7a65317C7e7700e5D566f --rpc localhost:7545 -lThe analysis was completed successfully. No issues were detected.

Luckily there were no bugs in the MetaCoin contract. Unfortunately this is not always the case. Try running multi-contract analysis on your own smart contracts and see what you can find!
Also, let me know if you found a nice vulnerability using multi-contract Mythril! (Nothing beats hearing about how Mythril helped catch a nasty bug 🐛)

In the second part of this series on continuous integration, we will build an easy first integration of the MythX API into the Travis continuous integration platform.

Other posts in this series:

• Part 1: CircleCI
• Part 2: Travis
• Part 3: (Coming soon)

This three-part series is about integrating MythX into Continuous Integration systems. In the first part of this series I have shown how to automatically check for smart contract vulnerabilities in CircleCI. In this part we will take a look at another popular open-source CI system: Travis.

Travis CI

Similar to CircleCI, Travis is configured using a YAML file. This time it is located in the project’s root directory as .travis.yml. The basic concepts of Travis are slightly different from other solutions, however. This greatly simplifies build definitions and job descriptions. This will work in our advantage here.

The tl;dr is that Travis has stages. Each stage consists of multiple jobs that are executed in parallel. These jobs can be grouped into builds. One of these builds will be a collection of jobs that do the MythX security analysis steps.

Sounds complicated? Once we dive into the actual configuration it will turn out to be really easy. But do not trust me, read on!

The basic setup

We will again use Python to run the MythX CLI for all our analysis needs. In the previous post we had to use a virtual environment to isolate our dependencies. In Travis we will rely on a dedicated stage that runs in parallel to all the other things we want to do. So we don’t have to isolate our dependencies. Absolute freedom!

Let’s start writing our configuration file and specify the Python version to use:

language: python
python:
  - 3.7

Before the magic starts we need to install the MythX CLI. We do this in the install phase – before any further steps are executed:

install:
- pip3 install mythx-cli

Spoiler: This line is also how you would install the MythX CLI on your machine as well (with an optional --user added into the mix.)

Submitting to MythX

Now for the analysis magic of submitting our smart contracts to MythX and making the build fail in case anything bad is found:

script:
  - mythx --ci --yes analyze --solc-version 0.5.0 contracts/

And that’s it. To dissect the mythx command a bit further:

• --ci tells the MythX CLI to return 1 if a medium or high severity issue has been found.
• --yes disables the confirmation prompt asking the user whether they really want to submit the Solidity files.
• analyze is the subcommand that tells the CLI we want to send an analysis job to the MythX API.
• --solc-version defines (you guessed it) the Solidity compiler version to compile the given files with.
• contracts/ is the directory the smart contracts live in. The MythX CLI will walk through this directory recursively and prepare analysis requests for each .sol file that has been found.

By default the CLI submits scans in quick mode. These return after roughly 120 seconds. So our complete Travis CI configuration file is short and sweet:

language: python
python:
  - 3.7

install:
- pip3 install mythx-cli

script:
  - mythx --ci --yes analyze --solc-version 0.5.0 contracts/

Run it!

I have prepared a test repository with a vulnerable smart contract and connected it to Travis with the above configuration. As soon as the CI job is finished, the following output appears:

The CI check has failed and notified me of a vulnerability. Now I want to know exactly how to trigger it so I can write a test case and validate my fix.

The benefit of signing up for an account on the MythX website (adding my API token to the CI’s environment as MYTHX_ACCESS_TOKEN) is that all my CI analyses are directly attached to my account and I can retrieve them later.

In the MythX dashboard I find my submission:

Diving into it, I see the vulnerability overview that was displayed in my CI output again:

Scrolling down, I see that my code has been highlighted with the vulnerability locations:

For each vulnerability I also have the test case data at my fingertips. Nice!

With the click of a button I can copy the raw transaction data and easily bootstrap my Truffle test cases. This helps me to validate the fix in my code and avoid the issue from occurring in the future.

What’s next?

The MythX CLI is continuously improving (CI jokes, hah!). I have written exhaustive documentation and a usage guide, which allows for more advanced patterns such as blacklisting vulnerabilities, opening custom analysis groups, delivering results in various output formats, and much more.

Do you want to store your reports as artifact files attached to the CI job? Just add the -o parameter and configure the path in Travis.

As always, feedback is a gift, and a comment here or directly in the GitHub repository would be greatly appreciated.

Next up, we will generalize our CI approach in part three. Stay tuned!

In the first post of a new series, we discuss integrating security considerations to a continuous integration pipeline, starting with CircleCI.

Continuous testing of applications can be hard to figure out. While it is difficult to measure CI/CD adoption, the blockchain ecosystem offers a great opportunity to adopt in-depth testing and continuous delivery pipelines where they make sense: right from the start.

At MythX we don’t mind which technologies you are using to get things done. Choosing the right tool for the right job means that service providers must not make assumptions about their client’s technologies. Security testing especially should be widely available and easy to use.

Behind the scenes the MythX team is working on the tech behind the smart contract analysis to make adding security to your workflow as simple as possible. For instance, we continuously run constructed samples against MythX in our QA process to keep our result quality as high as possible. This has several advantages:

• Avoid breaking changes. If things go wrong we will notice quickly and can iterate until the change is production-ready.
• Granular insights. Tests run on small change sets, one step at a time. This makes breaking changes obvious and allows for concise fixes.
• Save time on code reviews. We improve and review our internal test suites regularly. If they pass, confidence in the code’s correctness rises. That in turn keeps reviews focused on the business logic that matters.

Why CI?

There are plenty of reasons to use Continuous Integration (CI), but the above points have a nice side-effect: they also apply to smart contract development, or the software development lifecycle (SDLC) in general.

There are countless CI solutions out there and, as mentioned previously, we don’t mind which ones teams settle on.

That is why in this three-part series we will take a look at two of the most popular Continuous Integration solutions for open-source projects: CircleCI (this post), and Travis. Afterwards, we will generalize our approach to apply to other CI systems. Using the official MythX CLI it is fairly easy to get a basic test setup going.

Let’s jump right in!

CircleCI

CircleCI is configured using a YAML file located in .circleci/config.yml to describe the build steps. It defines workflows, which in turn consist of jobs. Each of the defined jobs contain a number of steps that are run. (CircleCI offers great tutorials if you need a quick refresher.)

In our case, this will be downloading MythX CLI, and running it against a set of given smart contracts. First we define our basic config:

version: 2
jobs:
  build:
    docker:
      - image: circleci/python:3.8
    steps:
      - checkout

This will define a job called build. All the steps inside this job will be executed in a Docker container running Python 3.8. The MythX CLI also runs on Python 3.6+ and PyPy.

Now for the meaty stuff. Let’s open up a virtual environment and install the MythX CLI into it. This makes sure that our Python application does not collide with any other Python code running in CI, and it avoids a range of CircleCI permission issues.

In our first step we checkout the code at the commit the CI job was given.

- run:
  name: Setup virtual environment
  command: python -m virtualenv venv
- run:
  name: Install MythX CLI
  command: |
    . venv/bin/activate
    pip install mythx-cli

There is nothing spectacular here. We define two steps, three commands, and we are set up. Now, submitting a contract to MythX can be done in a single command.

- run:
  name: Analyze with MythX
  command: |
    . venv/bin/activate
    mythx --ci --yes analyze --solc-version 0.5.0 contracts/

Well, actually two commands: Jump into the virtual environment, and then analyze the code.

There are a few things in the mythx call to note:

• --ci tells the MythX CLI to return 1 if a medium or high severity issue has been found.
• --yes disables the confirmation prompt asking the user whether they really want to submit X Solidity files.
• analyze is the subcommand that tells the CLI we want to send an analysis job to the MythX API.
• --solc-version defines, you guessed it, the Solidity compiler version to compile the given files with.
• contracts/ is the directory the smart contracts live in. The MythX CLI will walk through this directory recursively and prepare analysis requests for each .sol file that has been found.

By default the CLI submits scans in quick mode. These return after roughly 120 seconds. Now our full CircleCI config looks like this:

version: 2
jobs:
  build:
    docker:
      - image: circleci/python:3.8
    steps:
      - checkout
      - run:
          name: Setup virtual environment
          command: python -m virtualenv venv
      - run:
          name: Install MythX CLI
          command: |
            . venv/bin/activate
            pip install mythx-cli
      - run:
          name: Analyze with MythX
          command: |
            . venv/bin/activate
            mythx --ci --yes analyze --solc-version 0.5.0 contracts/

Run it!

Below I have prepared a test repository with a vulnerable smart contract and connected it to CircleCI with the above configuration. As soon as the CI job is finished, the following output appears:

The CI check has failed and notified me of a vulnerability. Now I want to note exactly how to trigger it so I can write a test case and validate my fix.

So I have signed up for a free account on the MythX website and added my API token to the CI’s environment as MYTHX_ACCESS_TOKEN. That way all my CI analyses are directly attached to my account and I can retrieve them later. In the dashboard’s analysis listing I find my submission:

Diving into it, I see the vulnerability overview that was displayed in my CI output again:

Scrolling down, I see that my code has been highlighted with the vulnerability locations:

For each vulnerability I also have the test case data at my fingertips.

With the click of a button I can copy the raw transaction data and easily bootstrap my Truffle test cases. This helps me to validate the fix in my code and avoid the issue from occurring in the future.

What’s next?

The MythX CLI is continuously improving (CI jokes, hah!) but I have written exhaustive documentation and a usage guide.

In addition to what I showed here, MythX CLI allows for more advanced patterns such as blacklisting vulnerabilities, opening custom analysis groups, delivering results in various output formats, and much more.

Do you want to store your reports as artifact files attached to the CI job? Just add the -o parameter and configure the path in CircleCI. The possibilities are endless!

Feedback is a gift and a comment here or directly in the GitHub repository is greatly appreciated. In the next part, we will be talking about the same integration in Travis CI in part two. Stay tuned!

Have you signed up for a free MythX account yet? Get started today and integrate with your own CI pipeline.

We’re introducing new plans offering the highest confidence in the correctness of your code, and allowing payment via credit/debit cards for the first time.

We’re excited to announce some changes to our MythX plans that will be going live on January 31, 2020.

Now, whenever a team announces “exciting changes” it’s often code word for something bad, but in this case, these changes should positively affect (as far as we can predict) absolutely all of our known users.

Rather than differentiating each plan based on the amount of smart contract weaknesses MythX detects, our new plans are now primarily tailored towards the security needs of your project, enabling small teams, individual developers, enterprises, and professional auditors to gain full confidence that their smart contracts are secure.

Leveraging security tools for verification can help you increase confidence in the correctness of smart contract code. Examples are given here using the MythX plugin for Remix.

Whether you are a smart contract developer or auditor you might wonder if there’s any value in using an automatic smart contract analysis tool. Assuming you know what you’re doing, will these tools tell you anything you don’t already know?

In this article I’ll describe how you can leverage security tools to increase confidence in the correctness of smart contract code and potentially detect issues that are not easily apparent.

Getting ready for takeoff

The first thing to keep in mind is that smart contracts are immutable once deployed to the blockchain (that’s the whole point). If a bug makes it into production, it’s “game over”, potentially resulting in vast financial losses.

Therefore, smart contract development should be approached with same care as developing and testing flight control systems:

• Use a minimalist approach;
• Use proven components whenever possible;
• Be very specific about how the code is supposed to behave.

Smart contracts (if done right) are relatively small programs and many traditional program analysis techniques can be applied without running into path explosion issues typically encountered with more complex programs. Analysis techniques such as symbolic execution, SMT solving and input fuzzing can provide a high degree of confidence that the code behaves correctly no matter what.

MythX is a security testing service that applies static and dynamic methods analysis to search for generic bugs and verify assumptions about Solidity code. It does this by integrating static code analysis, symbolic analysis and a grey-box fuzzing into a unified API. When developing, testing, or auditing smart contracts, MythX helps you do the following things:

• Get a quick overview of best practice violations and potential bugs in large codebases;
• Verify assumptions about code that is hard to understand;
• Gain confidence that the code behaves correctly with respect to functional specifications (with MythX you can prove correctness of some properties and achieve high certainty on others).

Running a basic scan

Remix comes with a built-in MythX security verification plugin which requires a couple of steps to set up. Once you have set up the MythX plugin you can submit contracts for analysis by clicking the “Analyze” button in the MythX tab.

MythX detects many generic security issues out-of-the-box. This includes both simple best practice violations (for example, set a specific compiler version, don’t do state writes after calls to untrusted addresses, and so on) and (mis-)behaviors that are very likely to constitute a vulnerability (for example, anyone can kill the contract).

Let’s try a basic analysis by running MythX against a couple of challenges from the OpenZeppelin Ethernaut wargame. Below is the source code of Level 2, “Fallout” (I flattened the code and updated it for compatibility with solc 5). Copy/paste the code into Remix to try this yourself.

/*
 * @source: https://ethernaut.openzeppelin.com/level/0x234094aac85628444a82dae0396c680974260be7
 * @author: Alejandro Santander (OpenZeppelin)
 * Modified by B. Mueller
 */

pragma solidity ^0.5.0;

contract Ownable {
    address payable public _owner;

    event OwnershipTransferred(address indexed previousOwner, address indexed newOwner);

    /**
     * @dev Initializes the contract setting the deployer as the initial owner.
     */
    constructor () internal {
        _owner = msg.sender;
        emit OwnershipTransferred(address(0), _owner);
    }

    /**
     * @dev Returns the address of the current owner.
     */
    function owner() public view returns (address) {
        return _owner;
    }

    /**
     * @dev Throws if called by any account other than the owner.
     */
    modifier onlyOwner() {
        require(isOwner(), "Ownable: caller is not the owner");
        _;
    }

    /**
     * @dev Returns true if the caller is the current owner.
     */
    function isOwner() public view returns (bool) {
        return msg.sender == _owner;
    }
}

library SafeMath {
    /**
     * @dev Returns the addition of two unsigned integers, reverting on
     * overflow.
     *
     * Counterpart to Solidity's `+` operator.
     *
     * Requirements:
     * - Addition cannot overflow.
     */
    function add(uint256 a, uint256 b) internal pure returns (uint256) {
        uint256 c = a + b;
        require(c >= a, "SafeMath: addition overflow");

        return c;
    }

    /**
     * @dev Returns the subtraction of two unsigned integers, reverting on
     * overflow (when the result is negative).
     *
     * Counterpart to Solidity's `-` operator.
     *
     * Requirements:
     * - Subtraction cannot overflow.
     */
    function sub(uint256 a, uint256 b) internal pure returns (uint256) {
        require(b <= a, "SafeMath: subtraction overflow");
        uint256 c = a - b;

        return c;
    }

    /**
     * @dev Returns the multiplication of two unsigned integers, reverting on
     * overflow.
     *
     * Counterpart to Solidity's `*` operator.
     *
     * Requirements:
     * - Multiplication cannot overflow.
     */
    function mul(uint256 a, uint256 b) internal pure returns (uint256) {
        // Gas optimization: this is cheaper than requiring 'a' not being zero, but the
        // benefit is lost if 'b' is also tested.
        // See: https://github.com/OpenZeppelin/openzeppelin-solidity/pull/522
        if (a == 0) {
            return 0;
        }

        uint256 c = a * b;
        require(c / a == b, "SafeMath: multiplication overflow");

        return c;
    }

    /**
     * @dev Returns the integer division of two unsigned integers. Reverts on
     * division by zero. The result is rounded towards zero.
     *
     * Counterpart to Solidity's `/` operator. Note: this function uses a
     * `revert` opcode (which leaves remaining gas untouched) while Solidity
     * uses an invalid opcode to revert (consuming all remaining gas).
     *
     * Requirements:
     * - The divisor cannot be zero.
     */
    function div(uint256 a, uint256 b) internal pure returns (uint256) {
        // Solidity only automatically asserts when dividing by 0
        require(b > 0, "SafeMath: division by zero");
        uint256 c = a / b;
        // assert(a == b * c + a % b); // There is no case in which this doesn't hold

        return c;
    }

    /**
     * @dev Returns the remainder of dividing two unsigned integers. (unsigned integer modulo),
     * Reverts when dividing by zero.
     *
     * Counterpart to Solidity's `%` operator. This function uses a `revert`
     * opcode (which leaves remaining gas untouched) while Solidity uses an
     * invalid opcode to revert (consuming all remaining gas).
     *
     * Requirements:
     * - The divisor cannot be zero.
     */
    function mod(uint256 a, uint256 b) internal pure returns (uint256) {
        require(b != 0, "SafeMath: modulo by zero");
        return a % b;
    }
}

contract Fallout is Ownable {
  
  using SafeMath for uint256;
  mapping (address => uint) allocations;

  /* constructor */
  function Fal1out() public payable {
    _owner = msg.sender;
    allocations[_owner] = msg.value;
  }

  function allocate() public payable { 
    allocations[msg.sender] = allocations[msg.sender].add(msg.value);
  }

  function sendAllocation(address payable allocator) public {
    require(allocations[allocator] > 0);
    allocator.transfer(allocations[allocator]);
  }

  function collectAllocations() public onlyOwner {
    msg.sender.transfer(address(this).balance);
  }

  function allocatorBalance(address allocator) public view returns (uint) {
    return allocations[allocator];
  }
}

Make sure the code complies and then hit the “Analyze” button in the MythX tab. This submits the code to the MythX service for an analysis in Quick Mode, the fastest and least comprehensive setting available in the free version of MythX.

After at most a couple of minutes the results should show up in the “Report” tab.

The report shows a critical issue in this contract: Anyone can become the contract owner and withdraw Ether from the account. Clicking the issue title highlights the location of the issue in the code, while clicking on the little arrow to the left expands the description.

Most importantly, this includes the list of function calls for reproducing the issue:

1. Call Fal1out()
2. Call collectAllocations()

This is especially useful when trying to understand issues when the root cause isn’t that obvious (or in this case for solving the challenge).

Custom tests

Besides running the built-in detectors, you can also use MythX to check specific properties. Let’s have a look at a basic example to illustrate the concept.

We’ll solve level 17 of the Ethernaut wargame. The goal of this challenge is to “unlock” a registrar smart contract by setting a Boolean state variable to true. A brief look at the code doesn’t show any obvious ways of achieving this:

pragma solidity ^0.4.23; 

// A Locked Name Registrar
contract Locked {

    bool public unlocked = false;  // registrar locked, no name updates
    
    struct NameRecord { // map hashes to addresses
        bytes32 name; // 
        address mappedAddress;
    }

    mapping(address => NameRecord) public registeredNameRecord; // records who registered names 
    mapping(bytes32 => address) public resolve; // resolves hashes to addresses
    
    function register(bytes32 _name, address _mappedAddress) public {
        // set up the new NameRecord
        NameRecord newRecord;
        newRecord.name = _name;
        newRecord.mappedAddress = _mappedAddress; 

        resolve[_name] = _mappedAddress;
        registeredNameRecord[msg.sender] = newRecord; 

        require(unlocked); // only allow registrations if contract is unlocked
    }
}

Let’s think about this challenge from the perspective of a security auditor who wants to ensure that, once deployed, the contract remains locked forever. To verify that this assumption holds, they can add an assertion to the code that checks the statement “the Boolean variable unlocked must never become true” (this type of property is called an invariant).

Copy/paste the challenge code into Remix and add the following function to the contract class:

function getSolution() public {
    assert(!unlocked);
}

MythX automatically searches for counter-examples to assertions contained in the submitted code. In our case, it uses SMT solving and fuzzing identify ways of setting the variable unlocked to true. When the MythX analysis is done you should see an assert violation listed in the report:

Expand the issue to find the example produced by MythX (“decoded calldata” in transaction 2). The function call is rather long – copy the line into a text editor to view it. If you reformat the output a bit you can run the example in Remix and verify that it actually sets unlocked to true:

register(0x0000000000000000000000000000000000000000000000000000000000000006,0x0000000000000000000000000000000000000000)

What’s happening here? It turns out that the function register writes to a user-supplied value to an uninitialized struct that points to storage. In that case, this results in a write to storage slot 0 which happens to contain the value we want to change.

This is a simple example but in principle you can use assertions to check arbitrarily complex properties (more on this in the next article).

Analysis modes

When you submit smart contract code to MythX the analysis engine runs fuzzing and symbolic execution in parallel with certain bounds on analysis time, loops, transaction depth, and other parameters. We offer thee modes named “quick”, “standard” and “deep”:

• In quick mode analysis time is limited to 120 seconds. In addition to the overall timeout, the following constraints apply:
  • The fuzzer will return in less than 120 seconds if the probability of detecting further issues falls below a certain threshold (coverage-based early termination).
  • Symbolic execution terminates early if all states within a depth of two transactions have been explored.

• In standard and deep mode each tool runs for a full 15 and 45 minutes, respectively. This allows the tools to explore achieve higher path coverage and lowers the residual risk of false negatives.

TL;DR

In this article I showed how to run a basic scan with MythX for Remix and how to check a simple custom property using a Solidity assertion. Check out the following Medium posts for more examples:

• Detecting critical smart contract vulnerabilities with MythX

• Advanced smart contract security verification with Remix

Sign up for a free MythX account today, and get started with your own basic scans.

We recommend using MythX through every stage of the smart contract development life-cycle, before, during, and after deployment.

(Note: This post was originally published in June 2019 and has been updated.)

We talk a lot here on the MythX team about the importance of regular, routine analysis of your smart contracts prior to deployment onto the blockchain.

The reason for this is simple: once the contract is deployed, it is immutable. Any vulnerability in your code that you deployed will be there forever.

In this way, you can think of contracts on the blockchain like embedded systems. Once the widget is sent out of the factory, it will always do whatever it was programmed to do. Forever.

(Which, incidentally, is why we should probably be slightly concerned about the Year 2038 problem. Yikes!)

Before and during

Our prescription is easily told: we recommend using MythX through every stage of the smart contract development life-cycle.

We also highly recommend a manual audit before you deploy, to find the business logic errors that an automated tool can’t detect. (We might be biased, but we can’t say enough good things about the team of auditors at ConsenSys Diligence.)

But all of that happens before deployment. What about after deployment? Can you just kick back and wash your hands of the whole security thing?

Unfortunately, no.