Security analysis tool for EVM bytecode. Supports smart contracts built for Ethereum, Hedera, Quorum, Vechain, Roostock, Tron and other EVM-compatible blockchains.
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.
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.
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:
The output will show the vulnerabilities in the contract. In the case of the "Exceptions" contract, Mythril detected two instances of assertion violations.
It is possible to trigger an assertion violation. Note that Solidity assert() statements should only be used to check invariants. Review the transaction trace generated for this issue and either make sure your program logic is correct, or use require() instead of assert() if your goal is to constrain user inputs or enforce preconditions. Remember to validate inputs from both callers (for instance, via passed arguments) and callees (for instance, via return values).
It is possible to trigger an assertion violation. Note that Solidity assert() statements should only be used to check invariants. Review the transaction trace generated for this issue and either make sure your program logic is correct, or use require() instead of assert() if your goal is to constrain user inputs or enforce preconditions. Remember to validate inputs from both callers (for instance, via passed arguments) and callees (for instance, via return values).
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.
To detect this vulnerability, the transaction count can be increased to four using the ``-t`` option, as shown below:
It is possible to trigger an assertion violation. Note that Solidity assert() statements should only be used to check invariants. Review the transaction trace generated for this issue and either make sure your program logic is correct, or use require() instead of assert() if your goal is to constrain user inputs or enforce preconditions. Remember to validate inputs from both callers (for instance, via passed arguments) and callees (for instance, via return values).
It is possible to trigger an assertion violation. Note that Solidity assert() statements should only be used to check invariants. Review the transaction trace generated for this issue and either make sure your program logic is correct, or use require() instead of assert() if your goal is to constrain user inputs or enforce preconditions. Remember to validate inputs from both callers (for instance, via passed arguments) and callees (for instance, via return values).
It is possible to trigger an assertion violation. Note that Solidity assert() statements should only be used to check invariants. Review the transaction trace generated for this issue and either make sure your program logic is correct, or use require() instead of assert() if your goal is to constrain user inputs or enforce preconditions. Remember to validate inputs from both callers (for instance, via passed arguments) and callees (for instance, via return values).
For the violation in the 4th transaction, the input value should be less than 10. The transaction data generated by Mythril for the
4th transaction is ``0x1d5d53dd0000000000000000000000000000000000000000000000000000000000000003``, the first 4 bytes ``1d5d53dd``
correspond to the function signature hence the input generated by Mythril is ``0000000000000000000000000000000000000000000000000000000000000003``
in hex, which is 3. For automated resolution of the input try using a different output format such as JSON.
..code-block:: bash
$ myth analyze <file_path> -o json
This leads to the following output:
..code-block:: json
{
"error": null,
"issues": [{
"address": 731,
"code": "assert(i == 0)",
"contract": "Exceptions",
"description": "An assertion violation was triggered.\nIt is possible to trigger an assertion violation. Note that Solidity assert() statements should only be used to check invariants. Review the transaction trace generated for this issue and either make sure your program logic is correct, or use require() instead of assert() if your goal is to constrain user inputs or enforce preconditions. Remember to validate inputs from both callers (for instance, via passed arguments) and callees (for instance, via return values).",
"description": "An assertion violation was triggered.\nIt is possible to trigger an assertion violation. Note that Solidity assert() statements should only be used to check invariants. Review the transaction trace generated for this issue and either make sure your program logic is correct, or use require() instead of assert() if your goal is to constrain user inputs or enforce preconditions. Remember to validate inputs from both callers (for instance, via passed arguments) and callees (for instance, via return values).",
"description": "An assertion violation was triggered.\nIt is possible to trigger an assertion violation. Note that Solidity assert() statements should only be used to check invariants. Review the transaction trace generated for this issue and either make sure your program logic is correct, or use require() instead of assert() if your goal is to constrain user inputs or enforce preconditions. Remember to validate inputs from both callers (for instance, via passed arguments) and callees (for instance, via return values).",
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:
This error occurs because Solidity cannot locate the ``PRC20.sol`` file.
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:
With this command, Mythril will be able to locate the ``PRC20.sol`` file, and the analysis should proceed without errors.
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``.
//Functions for changing variables related to the contract
function changeOwner(address payable _owner) public onlyowner {
creator = _owner;
}
function changeMultiplier(uint _mult) public onlyowner {
require(_mult <= 300 && _mult >= 120);
pyramidMultiplier = _mult;
}
function changeFeePercentage(uint _fee) public onlyowner {
require(_fee <= 10);
feePercent = _fee;
}
//Functions to provide information to end-user using JSON interface or other interfaces
function currentMultiplier() public view returns (uint multiplier, string memory info) {
multiplier = pyramidMultiplier;
info = "This multiplier applies to you as soon as transaction is received, may be lowered to hasten payouts or increased if payouts are fast enough. Due to no float or decimals, multiplier is x100 for a fractional multiplier e.g. 250 is actually a 2.5x multiplier. Capped at 3x max and 1.2x min.";
}
function currentFeePercentage() public view returns (uint fee, string memory info) {
fee = feePercent;
info = "Shown in % form. Fee is halved(50%) for amounts equal or greater than 50 ethers. (Fee may change, but is capped to a maximum of 10%)";
}
function currentPyramidBalanceApproximately() public view returns (uint pyramidBalance, string memory info) {
pyramidBalance = balance / 1 ether;
info = "All balance values are measured in Ethers, note that due to no decimal placing, these values show up as integers only, within the contract itself you will get the exact decimal value you are supposed to";
}
function nextPayoutWhenPyramidBalanceTotalsApproximately() public view returns (uint balancePayout) {
The first transaction is constrained to the function ``dynamicPyramid()``, the second one to the ``fallback()`` function, and finally, the third transaction is constrained to``collectAllFees()``, ``collectFeesInEther(uint256)`` and ``collectPercentOfFees(uint256)``.
