Farm

Blog

Audit

Ensure the security of your smart contracts

Book an audit

A Practical Guide to Smart Contract Security Tools.
Part 3: Mythril

Author: MixBytes team

Warning

Configuration and pre-launch

Contract launch and deployment

Errors search

Conclusion

Warning

This article is NOT a rating of automated analyzers. I use them for my own contracts: deliberately add pseudo-errors and study the responses. It is not a "better-or-worse" type of research, such tasks require a blind review of a large number of contracts and actual results won't be very precise, given the nature of this kind of software. A small mistake in a particular contract may knock out a large piece of analyzer logic, whereas a simple heuristic feature, such as finding a typical bug that competitors simply forgot to add, can level up the analyzer. Also, contract compiling errors may affect the outcome. All reviewed software is quite fresh and is constantly under development, thus serious errors should not be considered unsolvable.

In this article we don't aim to help a reader decide which analyzer is better but demonstrate different code analysis methods in practice and how to choose the right ones. We recommend applying several tools at once, choosing the most suitable one for the audited contract.

Configuration and pre-launch

Mythril performs several types of analysis. Here are some awesome articles on the subject: navigate here, check out this one and this one for a change. I strongly recommend to read them before we proceed.

For starters, let's build a Mythril Docker image (who knows what we may want to change?):

git clone 
https://github.com/ConsenSys/mythril-classic.git
cd mythril-classic
docker build -t myth .

Now we will run contracts/flattened.sol (I am using the same contract I mentioned in Introduction) that contains 2 main contracts, an OpenZeppelin Ownable and our Booking one. We are still facing the compiler version issue (our contract has 0.4.20), I will solve it the same way I did last time: add a compiler change command to a Dockerfile:

COPY --from=ethereum/solc:0.4.20 /usr/bin/solc /usr/bin

After recompiling the image, we proceed to the contract analysis. Do not forget to activate the flags -v4 and --verbose-report to see all warnings. Here we go:

docker run -v $(pwd):/tmp \
           -w /tmp myth:latest \
           -v4 \
           --verbose-report \
           -x contracts/flattened.sol

Now we are dealing with a flattened contract without dependencies. To analyze a Booking.sol contract separately with all dependencies loaded correctly, we will use the following command:

docker run -v $(pwd):/tmp \
           -w /tmp myth:latest \
           --solc-args="--allow-paths 
/tmp/node_modules/zeppelin-solidity/  
zeppelin-solidity=/tmp/node_modules/zeppelin-solidity" \
           -v4 \
           --verbose-report \
           -x contracts/Booking.sol

I prefer to work with a flattened contract, as we are going to modify the code a lot. Mythril has a very convenient --truffle mode that tests everything compiled by truffle and checks the whole project for vulnerabilities. Adding a contract name after a contract filename as -x contracts/flattened.sol:Booking using colon, is also an important feature, otherwise Mythril analyzes all available contracts. We believe that Ownable by OpenZeppelin is a secure contract and we will analyze only Booking. The last command before the launch is as follows:

docker run -v $(pwd):/tmp -w /tmp myth:latest -x 
contracts/flattened.sol:Booking -v4 --verbose-report

Contract launch and deployment

After running a contract, we get the following message:

mythril.laser.ethereum.svm [WARNING]: 
No contract was created during the execution of contract creation 
Increase the resources for creation execution (--max-depth or --create-timeout)
The analysis was completed successfully. No issues were detected.

It turned out our contract was not created and "deployed" in the emulator. That's why I recommend using the flag -v4 for all analyses not to miss an important message. Let's figure out what went wrong. A solution to this practical issue will help us understand how to run Mythril correctly. The Mythril guide says: "It uses concolic analysis, taint analysis and control flow checking to detect a variety of security vulnerabilities". If you are not comfortable with these terms, I suggest a wiki article about concolic testing and an awesome presentation about taint checking for x86. In a nutshell, Mythril emulates contract execution, stores all execution branches, and strives to reach a "dangerous" contract state trying different parameter combinations and possible options. Roughly the process goes like this (see the article above):

1. Define the set of input variables. They will serve as symbolic variables, all other 
variables will be treated as concrete values.
2. These variables and each operation which may affect a symbolic variable value 
should be logged to a trace file, as well as path conditions or any error that occurs.
3. Choose an set of input variables to begin with.
4. Execute the native contract code and save the trace file.
5. Symbolically re-execute the program on the trace, generating a set of symbolic 
constraints (including path conditions)for future analysis.
6. Exclude the last path condition from the “already analyzed” ones to analyze 
a new execution path next time. If there is no such path condition, the algorithm 
terminates.
7. Analyze the path condition: generate a new input for all path conditions to fix them. 
If there is no such input, return to step 6 and try the next execution path.
8. Go to step 4.

In plain words, Mythril goes through branches and detects combinations of input values that enable getting to each of them. Thanks to knowing which branches are traceable to assert, transfer, selfdestruct and other dangerous opcodes, Mythril detects input values and transaction combinations that affect execution security. What makes Mythril unique is its method of disconnecting branches that will never take over control and analyzing the control flow. To have a closer look under Mythril's hood, click here.

Due to deterministic nature of smart contracts, the same instruction sequence always entails the same set of state changes regardless of the platform, architecture and environment. Mythril and similar analysis tools combining symbolic and native execution can be highly effective for smart contracts which functions are quite concise and resources are limited. Mythril operates the notion of "state" which implies the contract code, its environment, current command indicator, storage and stack contents. Here is how the documentation reads:

The machine state μ is defined as the tuple (g, pc, m, i, s) which are the gas available, 
the program counter pc ∈ P256, the memory contents, the active number of words in memory 
(counting continuously from position 0), and the stack contents. 
The memory contents μm are a series of zeroes of size 256.

The state change graph is our main research item. If analysis execution is successful, graph details are included in the output log. Also, Mythril has the --graph option that allows building this graph in a friendly readable format. Now, having a more or less clear idea of how Mythril is going to work, let's get back to our contract and find out why the analysis fails and returns the [WARNING]: No contract was created during the execution of contract creation. First I tuned up the --create-timeout and --max-depth parameters as recommended. Nothing happened. My guess was to blame it on the constructor; I thought something was wrong with it. Here is the code:

function Booking(
    string _description,
    string _fileUrl,
    bytes32 _fileHash,
    uint256 _price,
    uint256 _cancellationFee,
    uint256 _rentDateStart,
    uint256 _rentDateEnd,
    uint256 _noCancelPeriod,
    uint256 _acceptObjectPeriod
) public payable {
    require(_price > 0);
    require(_price > _cancellationFee);
    require(_rentDateStart > getCurrentTime());
    require(_rentDateEnd > _rentDateStart);

    require(_rentDateStart+_acceptObjectPeriod < _rentDateEnd);
    require(_rentDateStart > _noCancelPeriod);

    m_description = _description;
    m_fileUrl = _fileUrl;
    m_fileHash = _fileHash;
    m_price = _price;
    m_cancellationFee = _cancellationFee;
    m_rentDateStart = _rentDateStart;
    m_rentDateEnd = _rentDateEnd;
    m_noCancelPeriod = _noCancelPeriod;
    m_acceptObjectPeriod = _acceptObjectPeriod;
}

Getting back to Mythril action pattern, to launch trace it has to call the contract constructor as the entire following execution process is determined by parameters in the constructor. For instance, if _price == 0 is used to call the constructor, the require(_price > 0) exception is returned. Also, the constructor will keep on failing despite Mythril's attempts to try different _price values, as long as _price <= _cancellationFee. This contract has about a dozen of parameters with strict limitations; by all means, Mythril cannot guess valid combinations for all. Thus, it will attempt to move to the next execution path, sorting through the constructor parameters, but it has almost zero changes to make the right guess, given the huge number of parameter combinations. Therefore, contract upload fails as each action path hits some require(...) and we are facing the above problem.

Now we have two options. The first is turning all require off by commenting them out. Then Mythril will be able to use any parameter combination to call the constructor and run successfully. Yet, using random parameters implies detecting random bugs caused by sending invalid values to the constructor. Plainly put, Mythril can detect a bug occuring when a contract creator defines _cancellationFee exceeding the _mprice by million times, but such bug and contract are useless for creator and Mythril simply waste resources to find this error. If we want more or less comprehensive deploy parameters, it makes sense to indicate more realistic constructor parameters for further analysis to prevent Mythril from searching for errors that will never occur as long as a contract is deployed correctly.

I spent many hours turning various constructor segments on and off, trying to pinpoint the deploy failure spot. As if these troubles were not enough, the constructor uses getCurrentTime() that returns the current time and it is totally unclear how Mythril processes this call. I will omit further details of my adventures, as auditors are most likely to learn the ins and outs themselves during regular usage. Therefore, I chose the second option: I removed all parameters from the constructor, even getCurrentTime() and merely hardcoded those that I need directly in the constructor:

   function Booking(
    ) public payable {
        m_description = "My very long booking text about hotel and beautiful sea view!";
        m_fileUrl = "https://ether-airbnb.bam/some-url/";
        m_fileHash = 0x1628f3170cc16d40aad2e8fa1ab084f542fcb12e75ce1add62891dd75ba1ffd7;
        m_price =           1000000000000000000; // 1 ETH
        m_cancellationFee = 100000000000000000; // 0.1 ETH
        m_rentDateStart = 1550664800 + 3600 * 24; // current time + 1 day
        m_rentDateEnd = 1550664800 + 3600 * 24 * 4; // current time + 4 days
        m_acceptObjectPeriod = 3600 * 8; // 8 hours
        m_noCancelPeriod = 3600 * 24; // 1 day

        require(m_price > 0);
        require(m_price > m_cancellationFee);
        require(m_rentDateStart > 1550664800);
        require(m_rentDateEnd > m_rentDateStart);
        require((m_rentDateStart + m_acceptObjectPeriod) < m_rentDateEnd);
        require(m_rentDateStart > m_noCancelPeriod);
    }

Also, do not forget to define the max-depth parameter. In my case, --max-depth=34 worked at AWS t2.medium instance. Note that when I use a more powerful laptop, no max-depth is needed. Judging by the way the parameter is used here, it is a part of the analysis branch setup strategy and the default value is infinity (see code). You may vary this parameter, but have your contract analyzed. After analysis launch, you'll see the messages like these:

mythril.laser.ethereum.svm [INFO]: 248 nodes, 247 edges, 2510 total states
mythril.laser.ethereum.svm [INFO]: Achieved 59.86% coverage for code: .............

The first string describes the analysis graph parameters. Analyzing alternative execution branches requires huge computational power, therefore auditing larger contracts takes time even at powerful PCs.

Errors search

Now we will search for errors and add our own ones. Mythril looks for all branches containing transfer, selfdestruct, assert, and detects other security-specific issues. Therefore, if the code contains one of the above mentioned instructions, Mythril identifies possible execution branches and even displays all transactions leading to them! For starters, let's see what Mythril has in store for the unfortunate Booking contract. The first warning goes like that:

==== Dependence on predictable environment variable ====
SWC ID: 116
Severity: Low
Contract: Booking
Function name: fallback
PC address: 566
Estimated Gas Usage: 17908 - 61696
Sending of Ether depends on a predictable variable.
The contract sends Ether depending on the values of the following variables:
- block.timestamp
Note that the values of variables like coinbase, gaslimit, block number and timestamp 
are predictable and/or can be manipulated by a malicious miner. 
Do not use them for random number generation or to make critical decisions.
--------------------
In file: contracts/flattened.sol:142

msg.sender.transfer(msg.value-m_price)

It happens because of

require(m_rentDateStart > getCurrentTime());

in a fallback function.

Please note that Mythril found a block.timestamp issue in getCurrentTime(). Broadly speaking, this is not a contract error, but the fact that Mythril relates block.timestamp to ether transfer is really great! A programmer should be aware that the decision depends on values controlled by miners. In case of future auctions or other competition, there's a risk of a front-running attack.

Now let's see whether Mythril identifies a block.timestamp dependence if we hide a variable in the function call:

function getCurrentTime() public view returns (uint256) {
-     return now;
+     return getCurrentTimeInner();              
}                     

+ function getCurrentTimeInner() internal returns (uint256) {
+     return now;
+ }

Ta-da! Mythril still sees block.timestamp - ether transfer dependence which is really important for an auditor. Mythril allows tracking the dependence between the variable and decision making after several contract state changes even if it's hidden in the logic. However, Mythril is not almighty, it won't trace all possible variable interdependencies. If we proceed with the getCurrentTime() function and make 3 levels of nesting, the warning will disappear. Every function call demands new state branches and huge resources for analyzing deep code nesting levels. I might misuse analysis parameters, and the analyzer still may identify the error somewhere deep inside. As I already mentioned, the product is being actively developed, and while writing this article I can see the commits with max-depth tags in the repository. Please don't take the current issues too close to heart, we have already found enough evidence Mythril effectively tracks variable dependencies.

We will add a function of random ether sending, i.e. anyone can withdraw a ⅕ of ether when a contract is in the State.PAID and the client has already paid the booking with ether. Here's the function:

function collectTaxes() external onlyState(State.PAID) {
    msg.sender.transfer(address(this).balance / 5);
}

Mythril detected the issue:

==== Unprotected Ether Withdrawal ====
SWC ID: 105                 
Severity: High               
Contract: Booking
Function name: collectTaxes()
PC address: 2492
Estimated Gas Usage: 2135 - 2746
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 a equivalent amount of ETH to it. 
This is likely to be a vulnerability.
--------------------
In file: contracts/flattened.sol:149

msg.sender.transfer(address(this).balance / 5)

--------------------
--------------------
Transaction Sequence:

{
    "2": {
        "calldata": "0x",
        "call_value": "0xde0b6b3a7640000",
        "caller": "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef"
    },
    "3": {
        "calldata": "0x01b613a5",
        "call_value": "0x0",
        "caller": "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef"
    }
}

That's great, Mythril even displayed 2 transactions causing possible ether withdrawal! Now we will change State.PAID for State.RENT, and it goes like this:

- function collectTaxes() external onlyState(State.PAID){
+ function collectTaxes() external onlyState(State.RENT) {

Now the collectTaxes() function can be called only when the contract is in State.RENT and there is nothing left on the account, since the contract has already sent ether to the owner. This time Mythril does NOT display the error Unprotected Ether Withdrawal ====! The onlyState(State.RENT) modifier prevents the analyzer from reaching the branch with sending ether to a non-zero account balance. Mythril went through different parameter options, but State.RENT is only available after all ether is sent to the owner. Therefore, getting to this code branch with a non-zero balance is impossible, and Mythril does not disturb the auditor!

Similarly, Mythril will trace selfdestruct and assert, showing the auditor what actions could lead to contract destruction or an important function breakdown. I will omit these examples and suggest testing a similar function causing selfdestruct.

Do not forget that Mythril performs symbolic execution analysis that entails vulnerabilities check without emulating. For instance, any use of "+", "-" and other arithmetic operations can be considered an "Integer overflow" vulnerability if an operand is at any rate controlled by the attacker. But as I said, the most powerful feature of Mythril is the mix of symbolic and native execution and detecting values for logic branching.

Conclusion

Without any doubt, one article is not enough to describe a full range of issues Mythril is capable of detecting. On top of that, it works in a real blockchain environment, finds necessary contracts and vulnerabilities by signature, builds beautiful call graphs, and edits reports. Mythril allows to write individual test scripts in a python-based interface, test particular functions quite easily, fix parameter values, or even implement a custom strategy for working with disassembled code.

Unlike IDA Pro, Mythril is still a young software, and there's almost no documentation except for a few articles. Many Mythril parameters are only described in the code (starting with a cli.py). I hope that a full and comprehensive documentation with parameter description will appear soon.

When the contract is more or less large, displaying error heaps takes a lot of space. I would like to receive a compressed data about detected errors. Working with Mythril, it is necessary to track the process, contracts that were tested and, if necessary, deliberately remove the errors the auditor knows are false-positives.

On the whole, Mythril is an excellent and very powerful tool for analyzing smart contracts. Every auditor should use it, as it draws attention to the critical parts of the code and detects hidden connections between variables.

To sum up, the recommendations for using Mythril are the following:

This bug was found with the Echidna fuzzer.
We have revert for the type(int256).min value in the abs function because the range for int256 is \(-2^{255}\)… \(2^{255} - 1\).

A Practical Guide to Smart Contract Security Tools.Part 3: Mythril

A Practical Guide to Smart Contract Security Tools.
Part 3: Mythril