Automated Smart Contract Audit Guide. Part 3: Mythril

Warning

This article is not an autoanalyzer performance rating. I apply them to my own contracts, intentionally synthesizing errors, and study the reactions. Such a study can not be the basis for determining the "better-worse", for this it makes sense to conduct a blind study on a large sample of contracts, which, given the capricious nature of this kind of software, is extremely difficult to conduct. It is quite possible that a small mistake in the contract can turn off a large piece of analyzer logic, and the simplest heuristic feature can add a huge amount of points to the analyzer by finding a widespread bug that competitors simply did not have time to add. Errors in the preparation and compilation of contracts may also play a role. All the software in question is quite young, and is constantly being developed, so do not take critical comments as irreparable problems.

The purpose of the article is to give the reader an understanding of how code analysis methods work in different analyzers and the ability to use them correctly, and not “make a choice”. A sensible choice is to use several tools at once, with an emphasis on the most suitable for the contract being analyzed.

Setup and preparation for launch

Mythril uses several types of analysis, here are a couple of good articles about him: the main one , this one or this one . Before continuing, it makes sense to read them.

To begin with, let's build our own Docker image of Mythril (who knows if we want to change it?):

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

Now we will try to run it on our contracts/flattened.sol (I use the same contract that was discussed in the introduction ), in which there are two main contracts, Ownable from Zeppelin and our Booking . We still have a problem with the version of the compiler, I fixed it in the same way as in the previous article, adding in the Dockerfile the lines that will replace the version of the compiler:

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

After rebuilding the image, you can try to run the contract analysis. Immediately let's use the -v4 and --verbose-report flags to see all the warnings. Go:

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

Here we work with a flattened contract without dependencies. To analyze the separate Booking.sol contract and so that Mythril can catch all the dependencies, you can use something like this:

 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 the flattened version, since we will modify a lot in the code. But Mythril also has an extremely convenient --truffle mode, which simply --truffle everything that truffle , testing the entire project for vulnerabilities. Also an important feature is the ability to specify the name of the contract to be analyzed through the colon, otherwise Mythril will analyze all the contracts that have been encountered. We believe that Ownable from OpenZeppelin is a secure contract, and we are only going to analyze Booking , so the final line to launch is:

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

Launch and contract contract

Start the analyzer with the above line, look at the output, and get, among other things, the following line:

 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 turns out that our contract was not created and "locked" in the emulator. That is why I recommend using the -v4 flag for all types of analysis to see all messages and not to miss any important ones. Let's figure out what's wrong. The solution to this practical problem is quite important for understanding how to properly use Mythril.

So, read about Mythril: It uses concolic analysis, taint analysis and control flow checking to detect a variety of security vulnerabilities . If you are not very familiar with these terms, I recommend the wiki about concolic testing here , but a good presentation about taint checking for x86. In short: Mythril emulates the execution of a contract, fixes the branches along which execution can go and tries to reach the “broken” state of the contract, sorting through various combinations of parameters and trying to get around all possible paths. Here is an approximate scheme of actions from the article above:

 1.      .   symbolic-,        . 2.      ,     ,   trace .    ,      ,    . 3.     . 4.       trace-. 5.  symbolic execution   trace,   symbolic ,    ,     ,     . 6.     ,          .    , . 7.   :   ,   ,   input-,     ,      .   input-   ,   .6    . 8.   .4 

If to simplify greatly, then Mythril, having met a branch in the code, can understand at what sets of variables one can get into one and another branch. In each branch, Mythril knows if it leads to assert , transfer , selfdestruct and other security-relevant opcodes. Therefore, Mythril analyzes which parameter sets and transactions can result in a security violation. And the way that Mythril cuts off branches that never get control and analyzes the control flow is its main feature. For more information about the guts Mythril and walking on the branches are written here .

Due to the determinism of the execution of smart contracts, the same sequence of instructions always leads strictly to one set of changes in the state, regardless of platform, architecture and environment. Also, functions in smart contracts are rather short, and resources are extremely limited, so analyzers such as Mythril, combining symbolic and native execution, for smart contracts can work extremely efficiently.

In the process of work, Mythril operates with the concept of "state" - this is the contract code, its environment, a pointer to the current command, the storage contract and the stack status. Here is the documentation:

 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 transition graph between states is the main object of study. In case of successful launch of the analysis, information about this column is displayed in the analysis log. Also, Mythril can build this graph in a readable form using the --graph option.

Now, more or less understanding what Mythril will do, we will continue to understand why the contract is not being analyzed and where did [WARNING]: No contract was created during the execution of contract creation come from [WARNING]: No contract was created during the execution of contract creation . For a start, I twisted the --create-timeout and - --max-depth parameter (as recommended) and, without getting a result, I thought the designer was to blame - something in it does not work. Here is his 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; } 

Recall the algorithm of action Mythril. To start trace, you need to call the contract constructor, because all subsequent execution will depend on the parameters with which the constructor was called. For example, if you call a constructor with _price == 0 , the constructor require(_price > 0) exception for require(_price > 0) . Even if Mythril enumerates the set of _price values, the constructor will still break if, for example, _price <= _cancellationFee . In this contract, with a dozen parameters associated with strict restrictions, and Mythril, of course, cannot guess the valid combinations of parameters. He tries to go to the next branch of execution, going through the parameters of the constructor, but he has practically no chance to guess - there are too many combinations of parameters. Therefore, the calculation of the contract does not work out - all the ways run into some kind of require(...) , and we get the above problem.

Now we have two ways: the first is to disable all require in the constructor by commenting them out. Then Mythril will be able to call the designer with any set of parameters and everything will work. But this means that by examining a contract with such parameters, Mythril will find errors that are possible with incorrect values ​​passed to the constructor. Simply put, if Mythril finds a bug that arises, if the contract creator specifies _cancellationFee a billion times more than the rent price of _mprice , then there is no sense in such a bug - such a contract will never be secured, and resources for finding errors will be spent. We mean that the contract is still secure with more or less holistic parameters, so for further analysis it makes sense to specify more realistic designer parameters so that Mythril does not look for errors that never occur if the contract is properly secured.

I spent many hours trying to understand exactly where the site was breaking, turning on and off various parts of the constructor. In addition to my troubles, the constructor uses getCurrentTime() , which returns the current time, and it is unclear how this call handles Mythril. I will not describe these adventures here, because most likely, with regular use, these details will become known to the auditor. Therefore, I chose the second way: limit the input data, and simply removed all parameters from the constructor, even getCurrentTime() , simply loading the necessary parameters directly in the constructor (ideally, you should get these parameters from the customer):

  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); } 

Plus, in order for everything to start, you must also set the max-depth parameter. It worked for me with this constructor with --max-depth=34 on the AWS instance t2.medium. At the same time, on my laptop, which is more powerful, everything runs without any max-depth . Judging by the use of this parameter , it is necessary to build branches for analysis, and its default value is infinity ( code ). So twist-and-turn this parameter, but make sure that the contract you need is analyzed. You can understand this by the message type:

 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 line describes the graph that will be analyzed, read the other lines for yourself. To analyze the various branches that can be executed, serious computational resources are required, therefore, when analyzing large contracts, you will have to wait even on a fast computer.

Search for errors

Now we will look for errors and add our own. Mythril is looking for branches that are sending ether, selfdestruct, assert, and other actions that are important from a security point of view. If somewhere in the contract code there is one of the above instructions, Mythril studies the ways in which you can come to this branch and, moreover, output a sequence of transactions leading to this branch!

First, let's see what Mythril issued for the long-suffering Booking contract. First warning:

 ==== 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. Don't use them for random number generation or to make critical decisions. -------------------- In file: contracts/flattened.sol:142 msg.sender.transfer(msg.value-m_price) 

and it arises because of

 require(m_rentDateStart > getCurrentTime()); 

in the fallback function.

Please note that Mythril realized that getCurrentTime() hiding in getCurrentTime() . Despite the fact that, according to the meaning of the contract, this is not a mistake, the fact that Mythril connects the block.timestamp with the broadcast output - this is excellent! In this case, the programmer must understand that the decision is made based on the value that the miner can control. And, if in the future in this place of the contract an auction or another bargain for the service occurs, you need to consider the possibility of front-running attacks.

See if Mythril sees a dependency on the block.timestamp if we hide the variable in a nested call, like this:

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

And yes! Mythril continues to see the connection between the block.timestamp and the transfer of the ether, this is extremely important for the auditor. The relationship between the variable controlled by the attacker and the decision-making after several changes to the contract state can be very masked by logic, and Mythril allows you to track it. Although you shouldn’t rely on all possible connections between all possible variables to be getCurrentTime() for you: if you continue to scoff at the getCurrentTime() function and make a triple depth of nesting, the warning will disappear. Each function call for Mythril requires the creation of new branches of state, so analyzing very deep levels of nesting will require huge resources.

Of course, there is a rather serious possibility that I simply use the analysis parameters incorrectly or the cutoff occurs somewhere in the depths of the analyzer. As I said, the product is in active development, I see commits with max-depth right at the moment of writing this article, so do not take the current problems seriously, we have already found enough evidence that Mythril can very effectively look for implicit connections between variables.

First, we add to the contract a function that broadcasts to anyone, but only after the client has sent the broadcast to the contract. We allowed anyone to pick up 1/5 of the air, but only when the contract is in the State.PAID state (i.e., only after the client has paid for the number on the air). Here is the function:

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

Mythril found a problem:

 ==== 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" } } 

Great, i.e. Mythril even brought out two transactions, which lead to the fact that you can take air from the contract. And now we change the State.PAID requirement to State.RENT , like this:

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

Now collectTaxes() can be called only when the contract is in the State.RENT state, and at that moment there is nothing on the balance sheet, since The contract has already sent the entire ether to the owner. And the important thing here is that Mythril this time does NOT display the error ==== Unprotected Ether Withdrawal ==== Withal = ==== Unprotected Ether Withdrawal ==== ! Under the condition of onlyState(State.RENT) , the analyzer did not get to the branch of the code that sends the air from the contract with a non-zero balance. Mythril went through different options of parameters, but you can get to State.RENT only by sending the entire broadcast to the lessor. Therefore, to reach this branch of the code, having a non-zero balance, is impossible, and Mythril does not properly disturb the auditor!

Similarly, Mythril will find selfdestruct and assert , showing the auditor what actions could lead to the destruction of a contract or a breakdown in an important function. I will not give these examples, just try to make a function similar to the one above, only causing selfdestruct , and twist its logic.

Also, do not forget that one of the parts of Mythril is the symbolic execution, and this approach, by itself, without emulating the execution, can define many vulnerabilities. For example, it is possible to consider the “Integer overflow” vulnerability any use of “+”, “-” and other arithmetic operators, if one of the operands is somehow controlled by the attacker. But I repeat once again, the most powerful feature of Mythril is the connection of symbolic and native execution and the determination of the values ​​of parameters leading to the branching of logic.

Conclusion

Of course, to show the full range of potential problems that Mythril is capable of detecting will require not one, but several articles. On top of that, he can do it all in a real blockchain, find the necessary contracts and vulnerabilities by signature, build beautiful call graphs, format reports. Also, Mythril allows you to write your own test scripts, providing the python-based interface to the contract and allowing you to test individual functions with an arbitrary degree of flexibility, fix the parameter values, or even implement your own strategy for working with disassembled code.

Mythril is still quite young software, this is not IDA Pro, and documentation, except for a few articles, is extremely small. The value of many parameters can only be read in the Mythril code, starting with cli.py. I hope that a full and deep description of the work of each parameter will appear in the documentation.

In addition, when the contract is more or less large, the output of the heap of errors takes up a lot of space, but I would like to be able to receive and compressed information about the error found, because when working with Mythril, it is imperative to look at the analysis path, see which contracts were tested as far as possible and be able to forcibly disable specific errors that the auditor regards as false-positive.

But in general, Mythril is an excellent and extremely powerful tool for analyzing smart contracts and at the moment should be in the arsenal of any auditor. It allows at least to pay attention to the critical parts of the code and detect hidden connections between variables.

In summary, the recommendations for using Mythril are:

1. Minimize the initial conditions of the contract under investigation. If, when analyzing, Mythril spends a lot of resources on branches that will never be put into practice, he will lose the ability to find really important bugs, so you should always try to narrow down the scope of potential branches.
2. Pay 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) whether the analysis of the contract has been launched, do not miss messages like 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) , otherwise you may mistakenly think that there are no bugs.
3. You can arbitrarily disable branches in the contract code, giving Mythril less variability in the choice of branches and saving resources. Try to do without max-depth restrictions so as not to chop off the analysis, but be careful not to disguise the error.
4. Be attentive to every warning, even light notes are sometimes worth it to at least add a comment to the contract code, making it easier for other developers.

In the next article we will deal with the Manticore analyzer, but the whole table of contents of articles that are ready or planned for writing:

Part 1. Introduction. Compilation, flattening, Solidity versions
Part 2. Slither
3. Mythril ( )
4. Manticore ( )
5. Echidna ( )