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

Published in

mixbytes

13 min readMar 5, 2019

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 open-source security analysis tool for Ethereum smart contracts 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. The article is related to current versions of software, at the moment when you read this article many things can be changed

Analyzer: Mythril

Description: Open-source security analysis tool for Ethereum smart contracts

Github: https://github.com/ConsenSys/mythril-classic

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 two 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 in the article about Slither: 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 code will not follow, and analyzing the control flow. To have a closer look under Mythril’s hood, click here. Due to the 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 small 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 many 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 chances 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 off all “require”-s 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 auditor and Mythril simply waste resources to find this error. If we want more or less comprehensive deploy parameters, it makes sense to set 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. The best way is to use real parameter values, that will be used in future contract deployment.

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 for me 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 a successful 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 take 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:142msg.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. For example, in case of future development of 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. Also, there is a probability 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.

Now, we will add a function of random ether sending to the “Booking” contract, 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:149msg.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 two 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 — excellent result!

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

Do not forget that Mythril performs symbolic execution analysis that can detect vulnerabilities even without emulation. For instance, any use of “+”, “-” and other arithmetic operations can be considered as “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 branch conditions.

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 using 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 full and comprehensive documentation with parameter description and their internal logic will appear soon.

When the contract is more or less large, displaying error messages takes a lot of space. I would like to receive “compressed” data about detected errors (one error per line), because, working with Mythril, it is necessary to thoroughly track the process of analysis. Also, the useful feature can be the possibility to deliberately remove the errors the auditor knows are false-positives from output.

On the whole, Mythril is an excellent and very powerful tool for analyzing smart contracts. Every smart-contracts 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:

Minimize initial contract conditions. If Mythril wastes its resources on branches that will never be executed, it will miss really important bugs. Always try to narrow down the number of possible branches, if applicable.
Make sure the analysis has started, do not ignore the messages like “mythril.laser.ethereum.svm [WARNING]: No contract was created during the execution of contract creation…”, otherwise you may think there are no bugs.
You can easily negate code branches, limit Mythril choice and save resources. Try to do without max-depth constraints not to cut off the analysis and be careful not to disguise the error.
Pay attention to every warning, add even minor comments to the contract code — make it simpler for other developers.

Our next article will be dedicated to Manticore. Stay tuned! Other articles to be published or in production are as follows:

Part 1. Introduction. Compilation, Flattening, Solidity Versions

Part 2. Slither

Part 3. Mythril (this article)

In case you have a specific question regarding the use of Mythril or other automatic tools for your project, feel free to contact us on our website or via Telegram.

Originally published at mixbytes.io.