Mythril is a popular security analysis tool for smart contracts. It is an open-source tool that can analyze Ethereum smart contracts and report potential security vulnerabilities in them. By analyzing the bytecode of a smart contract, Mythril can identify and report on possible security vulnerabilities, such as reentrancy attacks, integer overflows, and other common smart contract vulnerabilities.
This tutorial explains how to use Mythril to analyze simple Solidity contracts for security vulnerabilities. A simple contract is one that does not have any imports.
******************************************
******************************************
Executing Mythril on Simple Contracts
Executing Mythril on Simple Contracts
******************************************
******************************************
We consider a contract simple if it does not have any imports, like the following contract:
To start, we consider this simple contract, ``Exceptions``, which has a number of functions, including ``assert1()``, ``assert2()``, and ``assert3()``, that contain Solidity ``assert()`` statements. We will use Mythril to analyze this contract and report any potential vulnerabilities.
..code-block:: solidity
..code-block:: solidity
@ -51,13 +61,14 @@ We consider a contract simple if it does not have any imports, like the followin
}
}
We can execute such a contract by directly using the following command:
The sample contract has several functions, some of which contain vulnerabilities. For instance, the ``assert1()`` function contains an assertion violation. To analyze the contract using Mythril, the following command can be used:
..code-block:: bash
..code-block:: bash
$ myth analyze <file_path>
$ myth analyze <file_path>
This execution can give the following output:
The output will show the vulnerabilities in the contract. In the case of the "Exceptions" contract, Mythril detected two instances of assertion violations.
..code-block:: none
..code-block:: none
@ -112,10 +123,8 @@ This execution can give the following output:
We can observe that the function ``assert5(uint256)`` should have an assertion failure
One of the functions, ``assert5(uint256)``, should also have an assertion failure, but it is not detected because Mythril's default configuration is to run three transactions.
with the assertion ``assert(input_x > 10)`` which is missing from our output. This can be attributed to
To detect this vulnerability, the transaction count can be increased to four using the ``-t`` option, as shown below:
Mythril's default configuration of running three transactions. We can increase the transaction count to 4
using the ``-t <tx_count>``.
..code-block:: bash
..code-block:: bash
@ -204,6 +213,8 @@ This gives the following execution output:
When using Mythril to analyze a Solidity contract, you may encounter issues related to import statements. Solidity does not have access to the import locations, which can result in errors when compiling the program. In order to provide import information to Solidity, you can use the remappings option in Mythril.
Consider the following Solidity contract, which imports the PRC20 contract from the ``@openzeppelin/contracts/token/PRC20/PRC20.sol`` file:
..code-block:: solidity
..code-block:: solidity
@ -483,9 +497,13 @@ We encounter the following error:
This is because Mythril uses Solidity to compile the program. Solidity does not have access to the import locations.
This import information has to be explicitly provided to Solidity through Mythril.
This error occurs because Solidity cannot locate the ``PRC20.sol`` file.
We can do this by providing the remapping information to Mythril as follows:
To solve this issue, you need to provide remapping information to Mythril, which will relay it to the Solidity compiler.
Remapping involves mapping an import statement to the path that contains the corresponding file.
In this example, we can map the import statement ``@openzeppelin/contracts/token/PRC20/`` to the path that contains ``PRC20.sol``. Let's assume that the file is located at ``node_modules/PRC20/PRC20.sol``. We can provide the remapping information to Mythril in a JSON file like this:
..code-block:: json
..code-block:: json
@ -493,32 +511,40 @@ We can do this by providing the remapping information to Mythril as follows:
This can effectively execute the file since the Solidity compiler can locate `PRC20.sol`. For more information on remappings, you can
With this command, Mythril will be able to locate the ``PRC20.sol`` file, and the analysis should proceed without errors.
refer to `Solc docs <https://docs.soliditylang.org/en/v0.8.14/using-the-compiler.html#base-path-and-import-remapping>`_.
For more information on remappings, you can refer to the `Solidity documentation <https://docs.soliditylang.org/en/v0.8.14/using-the-compiler.html#base-path-and-import-remapping>`_.
Mythril is a security analysis tool that can be used to search certain transaction sequences.
The `--transaction-sequences` argument can be used to direct the search.
You should provide a list of transactions that are sequenced in the same order that they will be executed in the contract.
For example, suppose you want to find vulnerabilities in a contract that executes three transactions, where the first transaction is constrained with ``func_hash1`` and ``func_hash2``,
the second transaction is constrained with ``func_hash2`` and ``func_hash3``, and the final transaction is unconstrained on any function. You would provide ``--transaction-sequences [[func_hash1,func_hash2], [func_hash2,func_hash3],[]]`` as an argument to Mythril.
You can use ``-1`` as a proxy for the hash of the `fallback()` function and ``-2`` as a proxy for the hash of the ``receive()`` function.
Here is an example contract that demonstrates how to use Mythril with ``--transaction-sequences``.
Consider the following contract:
You can use Mythril to search certain transaction sequences. You can use ``--transaction-sequences`` argument to direct the search.
An example usage is ``[[func_hash1,func_hash2], [func_hash2,func_hash3],[]]`` where the first transaction is constrained with ``func_hash1`` and ``func_hash2``, the second tx is constrained with ``func_hash2`` and ``func_hash3`` and the final transaction is unconstrained on any function.
Use ``-1`` as a proxy for the hash of ``fallback()`` function and ``-2`` as a proxy for the hash of ``receive()`` function.
Consider the following contract
..code-block:: solidity
..code-block:: solidity
pragma solidity 0.5.0;
pragma solidity ^0.5.0;
contract Rubixi {
contract Rubixi {
@ -671,6 +697,7 @@ Consider the following contract
}
}
}
}
Since this contract has ``16`` functions, it is infeasible to execute uninteresting functions such as ``feesSeperateFromBalanceApproximately()``.
Since this contract has ``16`` functions, it is infeasible to execute uninteresting functions such as ``feesSeperateFromBalanceApproximately()``.
To successfully explore useful transaction sequences we can use Mythril's ``--transaction-sequences`` argument.
To successfully explore useful transaction sequences we can use Mythril's ``--transaction-sequences`` argument.
Nikhil Parasaram
2 years ago
committed by
GitHub