Merge to Master (#1680)

* Fix error message (#1506)

* Fix bug during checking potential issues (#1507)

* Fix bug due to list.remove() in a loop

* Mythril v0.22.25

* Add BASEFEE opcode (#1513)

* Add BASEFEE opcode

* Add test

* Support Panic(uint256) calls for asserts in v0.8.0+ (#1514)

* Support panic() asserts

* Use typing extensions

* Add typing extensions (#1516)

* Mythril v0.22.26

* [WIP] Add safe function support (#1510)

* Add safe functions cli

* Add a change

* Add tests

* Change examples

* Fix bytecode tests

* Use last jump as source for yul mapping (#1518)

* Mythril v0.22.27

* Fix issue with source mapping (#1526)

* Fix issue with source mapping

* Fix issues with deployedBytecode

* Add typing

* Refactor opcode files and fix issues (#1532)

* Use symbol_factory (#1533)

* Use symbol_factory

* Black

* Support native calls for delegatecall and callcode (#1534)

* Fix issue with calldatasize (#1537)

* Mythril v0.22.28

* Fix issue with integer arthimetic (#1541)

* Fix issues with exceptions module (#1542)

* Mythril v0.22.29

* Ignore plyvel (#1543)

* Remove additional eth transfer (#1544)

* Fix issues with out of index code (#1545)

* Mythril v0.22.30

* Fixes issues by considering future concrete hashes (#1547)

* Fix issues with hashing

* Fix offsets and edge cases

* Fix onchain storage access (#1548)

* Fix issues with onsite storage access

* Fix issue with copy

* Fix issue with get_constraints (#1549)

* Handle an edgecase from local host clients (#1550)

* Handle an edgecase from local host clients

* Fix eth-typing

* Fix pyparsing (#1551)

* Mythril v0.22.31

* Removes pyethereum Dependencies and leveldb libraries (#1555)

* change versions

* Move away from pyethereum dependency

* Remove leveldb

* Change requirements

* Add rzpad()

* Fix issues with sha3

* Fix sha3 edge cases

* Fix setup.py

* Restrict eth-utils

* Restrict eth-typing

* Fix py-ecc

* Remove mythx analysis doc

* Remove -l option from docs

* Fix typing_extensions (#1556)

* change versions

* Move away from pyethereum dependency

* Remove leveldb

* Change requirements

* Add rzpad()

* Fix issues with sha3

* Fix sha3 edge cases

* Fix setup.py

* Restrict eth-utils

* Restrict eth-typing

* Fix py-ecc

* Fix typing_extensions

* Fix blake2bpy (#1557)

* Fix case where loader is not present (#1558)

* Use empty code to denote address (#1559)

* Mythril v0.22.32

* Use concrete storage (#1562)

* Support symbolic bytecode (#1560)

* Support symbolic bytecode

* Use hex notation

* Handle swarm hash

* Use requirements in setup (#1564)

* Fix myth --version typo in docs (#1563)

Co-authored-by: Nikhil Parasaram <nikhilparasaram@gmail.com>

* Fixes issues with NoneType and restricts rlp version (#1567)

* Fix when args are NoneType

* Fix rlp

* Fix creation case and use better error message (#1569)

* Handle creation code

* Fix eth-keys

* Mythril v0.22.33

* Fix py-evm version (#1570)

* Fix py-evm when it's in alpha

* Downgrade py-evm

* upgrade py-evm

* remove py-evm restriction

* Fix trie

* Fix versions

* Edit versions

* Edit versions

* Restrict versions

* Remove eth-tester

* add blake2b

* Support multiple function names (#1571)

* Fix the leaking file descriptor when returning a z3 smt check result (#1574)

* Mythril v0.22.34

* Add more precompile tests (#1576)

* Add tests for natives

* Black updates

* Update black

* Refactor code (#1577)

* clean up code

* Update lolcat

* Fixes issues with create with symbolic bytecode (#1578)

* Handle cases when create get's symbolic bytecodes

* Refactor

* fix typing

* Mythril v0.22.35

* Handle cases with symbolic bytecode (#1581)

* Fix issues with string code

* revert solc changes

* Allow missing solc (#1582)

* allow missing solc

* reformatted

* dummy commit

Co-authored-by: mrx23dot <none>

* Handle changes in allow-paths in solc versions 0.8.8+ (#1584)

* Handle changes in allow-paths in solc versions 0.8.8+

* Add docker

* Remove test

* Mythril v0.22.36

* Update LICENSE (#1585)

* Restrict eth-rlp, eth-keyfile (#1586)

* Restrict eth-rlp

* Restrict eth-keyfile

* Helper functions for symbolic summaries (#1587)

* Restrict eth-rlp

* Restrict eth-keyfile

* Add functions for summaries

* Add some tweaks

* Revert a change

* Rewrite BaseArray class

* Remove unused variable

* Support Pragmas (#1591)

* Support Pragmas

* Fix MarkUpSafe

* Stop Edelweiss temporarily (#1593)

* Mythril v0.22.37

* Concolic tool  (#1445)

* Mythril v0.22.14

* Add trace plugin and find trace

* Add finding trace

* Add some changes

* change help text

* Add some comments

* Add support for concolic strategy

* Fix issues

* Add concolic exec tool

* Add a few fixes

* Fix a few errors

* Add tests

* Fix test interface

* Add muti flip test

* Add multi contract test

* Fix cases with multicontract calls

* Add more tests and fixes

* Fix tests

* Fix mypy

* Change tests and other small fixes

* Add more documentation

* Add some changes

* Update mythril/concolic/find_trace.py

Co-authored-by: JoranHonig <JoranHonig@users.noreply.github.com>

* Remove space

Co-authored-by: JoranHonig <JoranHonig@users.noreply.github.com>

* Fix typing

* Fix Review issues

* Change test type

* Remove deepcopy

* Use 3.8 for typing

* Use typing_extensions

* Fix prev_state

* Add changes to tests and fix some bugs

* Fix address assignment

* Fix issues and format

* Remove set_option

* Split plugins

* Refactor

Co-authored-by: JoranHonig <JoranHonig@users.noreply.github.com>

* Mythril v0.22.38

* Fix issues with sqlite3 (#1594)

* Mythril v0.22.14

* Add trace plugin and find trace

* Add finding trace

* Add some changes

* change help text

* Add some comments

* Add support for concolic strategy

* Fix issues

* Add concolic exec tool

* Add a few fixes

* Fix a few errors

* Add tests

* Fix test interface

* Add muti flip test

* Add multi contract test

* Fix cases with multicontract calls

* Add more tests and fixes

* Fix tests

* Fix mypy

* Change tests and other small fixes

* Add more documentation

* Add some changes

* Update mythril/concolic/find_trace.py

Co-authored-by: JoranHonig <JoranHonig@users.noreply.github.com>

* Remove space

Co-authored-by: JoranHonig <JoranHonig@users.noreply.github.com>

* Fix typing

* Fix Review issues

* Change test type

* Remove deepcopy

* Use 3.8 for typing

* Use typing_extensions

* Fix prev_state

* Add changes to tests and fix some bugs

* Fix address assignment

* Fix issues and format

* Remove set_option

* Split plugins

* Refactor

* Handle sqlite3

Co-authored-by: JoranHonig <JoranHonig@users.noreply.github.com>

* Mythril v0.22.39

* Init config dir (#1595)

* Mythril v0.22.40

* Fixes optimizer issue (#1597)

* Init config dir

* Fix solc optimizer

* Mythril v0.22.41

* Handle constructor edge case (#1600)

* Init config dir

* Fix solc optimizer

* Handle constructor edge case

* Fix NPM code block issue (#1602)

* Init config dir

* Fix solc optimizer

* Fix NPM code block issue

* Extend tests

* Beam search (#1606)

* Init config dir

* Fix solc optimizer

* Add beam search

* Use dict over reference

* Change default execution time

* Support TX constraints and refactor CLI (#1607)

* Support TX constraints and refactor CLI

* Fix typing

* Add additional typing

* Use dict over accessor

* Fix z3py requirements

* Init storage args

* Init storage args

* Init args in vm tests

* Unrestrict z3 to 4.8.15.0 (#1608)

* Mythril v0.22.42

* Fix caching of issues across modules (#1610)

* Fix caching of issues across modules

* Fix caching of issues across modules

* Remove logging (#1611)

* Fix caching of issues across modules

* Fix caching of issues across modules

* Use log.info

* Merge

* remove comment

* Check versions before using integer module (#1613)

* use more secure approach to call docker (#1614)

* Mythril v0.22.43

* Use better issue annotations for search (#1615)

* Check versions before using integer module

* Use IssueAnnotations

* Fix misc issues related to summaries (#1617)

* Check versions before using integer module

* Use IssueAnnotations

* Fix misc issues with summaries

* Fix issue with cache during summaries (#1619)

* Check versions before using integer module

* Use IssueAnnotations

* Fix misc issues with summaries

* Fix cache issue

* Fix safe functions

* dead link (#1616)

* Fix issue with PluginSkipState (#1620)

* Check versions before using integer module

* Use IssueAnnotations

* Fix misc issues with summaries

* Fix cache issue

* Fix safe functions

* Fix issue with PluginSkipState

* Update black

* Mythril v0.23.0

* fixed module links in documentation (#1622)

* Use int argument (#1625)

* remove depth for jump (#1628)

* Use a more precise modeling of return data (#1630)

* remove depth for jump

* Use a more precise modeling of return data

* Fix issues with lists

* Fix issues

* Fix misc issues (#1631)

* remove depth for jump

* Use a more precise modeling of return data

* Fix issues with lists

* Fix issues

* Fix misc issues

* Mythril v0.23.1

* Correct comment (#1632)

* Correct comment

* Update bitvec_helper.py

* Fix caching for exceptions module (#1633)

* Fix loop bound and other instruction performance issues (#1635)

* Fix caching for exceptions module

* Fix loop bound and other instruction performance issues

* Remove unused variable

* Increase loop bound

* Mythril v0.23.2

* Handle CRLF line endings (#1637)

* Handle CRLF line endings

* Add new line at the end of file

* Typo: External Calls now states correctly SWC-107 (#1639)

External Calls mentioned *SWC-117* but links (corrrectly) to SWC-107, fixed typo to *SWC-107*

* Fix Bitvec issue (#1641)

* Fix issues with Bitvec (#1642)

* Fix Bitvec issue

* Fix issues with Bitvec

* Mythril v0.23.3

* Use latest blake2bpy, Fix version extraction (#1644)

* Use latest blake2bpy, Fix version extraction

* Fix setup.py

* Handle setup.py

* Handle setup.py

* Handle setup.py

* Fix requirements

* Fix requirements

* Fix requirements

* restrict eth-hash

* Support py36 through py39 (#1646)

* Support py36 through py39

* Remove usage of cytoolz

* Update tox

* Add a get set for summaries (#1647)

* Support py36 through py39

* Remove usage of cytoolz

* Update tox

* Add a get set for summaries

* Mythril v0.23.4

* Deepcopy storage load and store sets (#1648)

* Support py36 through py39

* Remove usage of cytoolz

* Update tox

* Add a get set for summaries

* Support get/set

* Restrict cytoolz

* Move cytoolz up the dependency list

* Move cytoolz up the dependency list

* Fix CI (#1651)

* Support py36 through py39

* Remove usage of cytoolz

* Update tox

* Add a get set for summaries

* Support get/set

* Restrict cytoolz

* Move cytoolz up the dependency list

* Move cytoolz up the dependency list

* Add cython

* Black

* Remove from requirements

* Add cython

* Remove cython from setup

* Remove cython from setup

* Add cython

* set cytoolz version

* Add support for locking config file (#1652)

* Add support for locking config file

* Remove abi decode test

* Fix typo

* Mythril v0.23.5

* Fix issues with arbitrary jump dest (#1654)

* Add partial abi support (#1655)

* Fix issues with arbitrary jump dest

* Support abi

* Add partial abi support

* Fix test

* Fix test directory

* Mythril v0.23.6

* Update Readme

* Fix OOG issue (#1658)

* Fix issues with arbitrary jump dest

* Support abi

* Add partial abi support

* Fix test

* Fix test directory

* Fix OOG issue

* Fix issue with simplify (#1660)

* Fix issues with arbitrary jump dest

* Support abi

* Add partial abi support

* Fix test

* Fix test directory

* Fix OOG issue

* Fix issue with simplify

* Fix typo

* Fix imports for python 3.10 (#1661)

* Fix issues with arbitrary jump dest

* Support abi

* Add partial abi support

* Fix test

* Fix test directory

* Fix OOG issue

* Fix issue with simplify

* Fix typo

* Fix import

* Refactor

* Add exit code (#1662)

* Add exit code

* Fix tests

* Remove additional python runs in tox (#1663)

Since `geth` gets killed by CI after some time, it is better to run only the necessary python versions.

* Update docs and Add tutorial (#1664)

* Add exit code

* Update docs with tutorial

* Fix docs

* Reformat

* Mythril v0.23.7 (#1665)

* Handles issue with low constructor loop bound and new way to deal with solver-timeout (#1668)

* Add exit code

* Update docs with tutorial

* Fix docs

* Reformat

* Fix the issue with loop-bound and solver-timeout

* Add test changes

* Restrict hexbytes

* Mythril v0.23.8 (#1669)

* last_jump has type `int` but is used as type `None`. (#1670)

* last_jump has type `int` but is used as type `None`.

"filename": "mythril/analysis/module/modules/exceptions.py"
"warning_type": "Incompatible variable type [9]"
"warning_message": " last_jump is declared to have type `int` but is used as type `None`."
"warning_line": 28
"fix": None to 0

* Update exceptions.py

* Fix typo

* Add import

Co-authored-by: Nikhil Parasaram <tommycjniko@gmail.com>
Co-authored-by: norhh <nikhilparasaram@gmail.com>

* Handle issues with simplify (#1674)

* Add exit code

* Update docs with tutorial

* Fix docs

* Reformat

* Fix the issue with loop-bound and solver-timeout

* Add test changes

* Restrict hexbytes

* Use solver over simplify

* Handle OOG during CALL (#1675)

* Mythril v0.23.9

Co-authored-by: Peilin Zheng <tczpl@163.com>
Co-authored-by: Sir Hashalot <95114813+sirhashalot@users.noreply.github.com>
Co-authored-by: Iaroslav Zeigerman <zeigerman.ia@gmail.com>
Co-authored-by: Kis Gabor <mrx23dot@users.noreply.github.com>
Co-authored-by: Serafim Cloud <55061526+serafimcloud@users.noreply.github.com>
Co-authored-by: JoranHonig <JoranHonig@users.noreply.github.com>
Co-authored-by: shafu.eth <selfouly@gmail.com>
Co-authored-by: Zach Obront <zobront@gmail.com>
Co-authored-by: 72521 <ysl47698@gmail.com>
Co-authored-by: Christian <christiancattai@gmail.com>
Co-authored-by: Luca Di Grazia <luca.digrazia94@gmail.com>
master
Nikhil Parasaram 2 years ago committed by GitHub
parent 563332bd42
commit d22da1c212
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
  1. 2
      .circleci/config.yml
  2. 19
      .drone.yml
  3. 2
      .github/ISSUE_TEMPLATE/bug-report.md
  4. 2
      .pre-commit-config.yaml
  5. 1
      Dockerfile
  6. 2
      LICENSE
  7. 1
      MANIFEST.in
  8. 4
      README.md
  9. 5
      all_tests.sh
  10. 2
      docker_build_and_deploy.sh
  11. 2
      docs/source/analysis-modules.rst
  12. 8
      docs/source/conf.py
  13. 2
      docs/source/index.rst
  14. 3
      docs/source/installation.rst
  15. 39
      docs/source/module-list.rst
  16. 7
      docs/source/modules.rst
  17. 125
      docs/source/mythril.analysis.module.modules.rst
  18. 53
      docs/source/mythril.analysis.module.rst
  19. 110
      docs/source/mythril.analysis.modules.rst
  20. 90
      docs/source/mythril.analysis.rst
  21. 37
      docs/source/mythril.concolic.rst
  22. 19
      docs/source/mythril.disassembler.rst
  23. 46
      docs/source/mythril.ethereum.interface.leveldb.rst
  24. 37
      docs/source/mythril.ethereum.interface.rpc.rst
  25. 10
      docs/source/mythril.ethereum.interface.rst
  26. 22
      docs/source/mythril.ethereum.rst
  27. 19
      docs/source/mythril.interfaces.rst
  28. 29
      docs/source/mythril.laser.ethereum.function_managers.rst
  29. 89
      docs/source/mythril.laser.ethereum.rst
  30. 69
      docs/source/mythril.laser.ethereum.state.rst
  31. 21
      docs/source/mythril.laser.ethereum.strategy.extensions.rst
  32. 35
      docs/source/mythril.laser.ethereum.strategy.rst
  33. 25
      docs/source/mythril.laser.ethereum.transaction.rst
  34. 29
      docs/source/mythril.laser.plugin.plugins.coverage.rst
  35. 70
      docs/source/mythril.laser.plugin.plugins.rst
  36. 10
      docs/source/mythril.laser.plugin.plugins.summary_backup.rst
  37. 53
      docs/source/mythril.laser.plugin.rst
  38. 23
      docs/source/mythril.laser.rst
  39. 63
      docs/source/mythril.laser.smt.rst
  40. 37
      docs/source/mythril.laser.smt.solver.rst
  41. 37
      docs/source/mythril.mythril.rst
  42. 37
      docs/source/mythril.plugin.rst
  43. 51
      docs/source/mythril.rst
  44. 13
      docs/source/mythril.solidity.rst
  45. 81
      docs/source/mythril.support.rst
  46. 63
      docs/source/mythx-analysis.rst
  47. 3
      docs/source/security-analysis.rst
  48. 511
      docs/source/tutorial.rst
  49. 0
      docs/source/wiki.rst
  50. 1
      mypy-stubs/z3/__init__.pyi
  51. 2
      myth
  52. 2
      mythril/__version__.py
  53. 4
      mythril/analysis/call_helpers.py
  54. 34
      mythril/analysis/issue_annotation.py
  55. 57
      mythril/analysis/module/base.py
  56. 10
      mythril/analysis/module/loader.py
  57. 9
      mythril/analysis/module/module_helpers.py
  58. 49
      mythril/analysis/module/modules/arbitrary_jump.py
  59. 2
      mythril/analysis/module/modules/arbitrary_write.py
  60. 4
      mythril/analysis/module/modules/delegatecall.py
  61. 22
      mythril/analysis/module/modules/dependence_on_origin.py
  62. 27
      mythril/analysis/module/modules/dependence_on_predictable_vars.py
  63. 2
      mythril/analysis/module/modules/ether_thief.py
  64. 96
      mythril/analysis/module/modules/exceptions.py
  65. 1
      mythril/analysis/module/modules/external_calls.py
  66. 51
      mythril/analysis/module/modules/integer.py
  67. 23
      mythril/analysis/module/modules/multiple_sends.py
  68. 2
      mythril/analysis/module/modules/state_change_external_calls.py
  69. 41
      mythril/analysis/module/modules/suicide.py
  70. 38
      mythril/analysis/module/modules/unchecked_retval.py
  71. 21
      mythril/analysis/module/modules/user_assertions.py
  72. 6
      mythril/analysis/module/util.py
  73. 48
      mythril/analysis/potential_issues.py
  74. 80
      mythril/analysis/report.py
  75. 5
      mythril/analysis/security.py
  76. 51
      mythril/analysis/solver.py
  77. 21
      mythril/analysis/symbolic.py
  78. 2
      mythril/concolic/__init__.py
  79. 85
      mythril/concolic/concolic_execution.py
  80. 34
      mythril/concolic/concrete_data.py
  81. 78
      mythril/concolic/find_trace.py
  82. 55
      mythril/disassembler/asm.py
  83. 25
      mythril/disassembler/disassembly.py
  84. 7
      mythril/ethereum/evmcontract.py
  85. 0
      mythril/ethereum/interface/leveldb/__init__.py
  86. 177
      mythril/ethereum/interface/leveldb/accountindexing.py
  87. 314
      mythril/ethereum/interface/leveldb/client.py
  88. 23
      mythril/ethereum/interface/leveldb/eth_db.py
  89. 165
      mythril/ethereum/interface/leveldb/state.py
  90. 4
      mythril/ethereum/interface/rpc/utils.py
  91. 103
      mythril/ethereum/util.py
  92. 18
      mythril/exceptions.py
  93. 355
      mythril/interfaces/cli.py
  94. 42
      mythril/interfaces/epic.py
  95. 14
      mythril/laser/ethereum/call.py
  96. 2
      mythril/laser/ethereum/cfg.py
  97. 2
      mythril/laser/ethereum/function_managers/__init__.py
  98. 23
      mythril/laser/ethereum/function_managers/exponent_function_manager.py
  99. 69
      mythril/laser/ethereum/function_managers/keccak_function_manager.py
  100. 211
      mythril/laser/ethereum/instruction_data.py
  101. Some files were not shown because too many files have changed in this diff Show More

@ -40,7 +40,7 @@ jobs:
- run:
name: Black style check
command: |
pip3 install --user black==19.10b0
pip3 install --user black==22.3.0
python3 -m black --check /home/mythril/
- run:

@ -35,15 +35,16 @@ steps:
- git submodule update --init --recursive
- git submodule update --remote --recursive
# run edelewiss tests
- edelweiss-cli
-p mythril
--timeout 90
--output-dir $(pwd)
--s3
--dynamodb
--circle-ci CircleCI/mythril.csv
--ignore-false-positives $IGNORE_FALSE_POSITIVES
--ignore-regressions $IGNORE_REGRESSIONS
# Temporarily stop Edelweiss drone
#- edelweiss-cli
# -p mythril
# --timeout 90
# --output-dir $(pwd)
# --s3
# --dynamodb
# --circle-ci CircleCI/mythril.csv
# --ignore-false-positives $IGNORE_FALSE_POSITIVES
# --ignore-regressions $IGNORE_REGRESSIONS
when:
branch:
- develop

@ -37,7 +37,7 @@ or perhaps:
4. See error
If there is a Solidity source code, a truffle project, or bytecode
If there is a Solidity source code or a bytecode
that is involved, please provide that or links to it.
-->

@ -2,6 +2,6 @@
# See https://pre-commit.com/hooks.html for more hooks
repos:
- repo: https://github.com/psf/black
rev: 19.3b0
rev: 21.12b0
hooks:
- id: black

@ -15,7 +15,6 @@ RUN apt-get update \
locales \
python-pip-whl \
python3-pip \
libleveldb-dev \
python3-setuptools \
software-properties-common \
&& add-apt-repository -y ppa:ethereum/ethereum \

@ -1,6 +1,6 @@
The MIT License (MIT)
Copyright (c) 2017-present Bernhard Mueller
Copyright (c) since 2017 Bernhard Mueller
Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal

@ -1,2 +1,3 @@
include mythril/support/assets/*
include mythril/analysis/templates/*
include requirements.txt

@ -26,7 +26,7 @@ Get it with [Docker](https://www.docker.com):
$ docker pull mythril/myth
```
Install from Pypi:
Install from Pypi (Python 3.6-3.9):
```bash
$ pip3 install mythril
@ -48,7 +48,7 @@ Or:
$ myth analyze -a <contract-address>
```
Specify the maximum number of transaction to explore with `-t <number>`. You can also set a timeout with `--execution-timeout <seconds>`. Example ([source code](https://gist.github.com/b-mueller/2b251297ce88aa7628680f50f177a81a#file-killbilly-sol)):
Specify the maximum number of transaction to explore with `-t <number>`. You can also set a timeout with `--execution-timeout <seconds>`.
```
> myth a killbilly.sol -t 3

@ -7,11 +7,6 @@ assert sys.version_info[0:2] >= (3,5), \
"""Please make sure you are using Python 3.5 or later.
You ran with {}""".format(sys.version)' || exit $?
echo "Checking that truffle is installed..."
if ! which truffle ; then
echo "Please make sure you have etherum truffle installed (npm install -g truffle)"
exit 2
fi
rm -rf ./tests/testdata/outputs_current/
mkdir -p ./tests/testdata/outputs_current/

@ -17,7 +17,7 @@ LATEST_TAG=${NAME}:latest
docker build -t ${VERSION_TAG} .
docker tag ${VERSION_TAG} ${LATEST_TAG}
docker login -u $DOCKERHUB_USERNAME -p $DOCKERHUB_PASSWORD
echo "$DOCKERHUB_PASSWORD" | docker login -u $DOCKERHUB_USERNAME --password-stdin
docker push ${VERSION_TAG}
docker push ${LATEST_TAG}

@ -1,7 +1,7 @@
Analysis Modules
================
Mythril's detection capabilities are written in modules in the `/analysis/modules <https://github.com/ConsenSys/mythril/tree/master/mythril/analysis/modules>`_ directory.
Mythril's detection capabilities are written in modules in the `/analysis/module/modules <https://github.com/ConsenSys/mythril/tree/master/mythril/analysis/module/modules>`_ directory.
.. toctree::

@ -132,7 +132,13 @@ latex_elements = {
# (source start file, target name, title,
# author, documentclass [howto, manual, or own class]).
latex_documents = [
(master_doc, "Mythril.tex", "Mythril Documentation", "Bernhard Mueller", "manual")
(
master_doc,
"Mythril.tex",
"Mythril Documentation",
"ConsenSys Dilligence",
"manual",
)
]

@ -7,9 +7,9 @@ Welcome to Mythril's documentation!
about
installation
tutorial
security-analysis
analysis-modules
mythx-analysis
mythril

@ -12,7 +12,6 @@ PyPI on Mac OS
brew update
brew upgrade
brew tap ethereum/ethereum
brew install leveldb
brew install solidity
pip3 install mythril
@ -36,7 +35,7 @@ PyPI on Ubuntu
# Install mythril
pip3 install mythril
myth --version
myth version
******

@ -5,84 +5,79 @@ Modules
Delegate Call To Untrusted Contract
***********************************
The `delegatecall module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/delegatecall.py>`_ detects `SWC-112 (DELEGATECALL to Untrusted Callee) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-112>`_.
The `delegatecall module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/module/modules/delegatecall.py>`_ detects `SWC-112 (DELEGATECALL to Untrusted Callee) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-112>`_.
***********************************
Dependence on Predictable Variables
***********************************
The `predictable variables module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/dependence_on_predictable_vars.py>`_ detects `SWC-120 (Weak Randomness) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-120>`_ and `SWC-116 (Timestamp Dependence) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-116>`_.
The `predictable variables module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/module/modules/dependence_on_predictable_vars.py>`_ detects `SWC-120 (Weak Randomness) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-120>`_ and `SWC-116 (Timestamp Dependence) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-116>`_.
******************
Deprecated Opcodes
******************
The `deprecated opcodes module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/deprecated_ops.py>`_ detects `SWC-111 (Use of Deprecated Functions) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-111>`_.
***********
Ether Thief
***********
The `Ether Thief module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/ether_thief.py>`_ detects `SWC-105 (Unprotected Ether Withdrawal) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-105>`_.
The `Ether Thief module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/module/modules/ether_thief.py>`_ detects `SWC-105 (Unprotected Ether Withdrawal) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-105>`_.
**********
Exceptions
**********
The `exceptions module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/exceptions.py>`_ detects `SWC-110 (Assert Violation) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-110>`_.
The `exceptions module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/module/modules/exceptions.py>`_ detects `SWC-110 (Assert Violation) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-110>`_.
**************
External Calls
**************
The `external calls module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/external_calls.py>`_ warns about `SWC-117 (Reentrancy) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-107>`_ by detecting calls to external contracts.
The `external calls module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/module/modules/external_calls.py>`_ warns about `SWC-107 (Reentrancy) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-107>`_ by detecting calls to external contracts.
*******
Integer
*******
The `integer module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/integer.py>`_ detects `SWC-101 (Integer Overflow and Underflow) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-101>`_.
The `integer module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/module/modules/integer.py>`_ detects `SWC-101 (Integer Overflow and Underflow) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-101>`_.
**************
Multiple Sends
**************
The `multiple sends module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/multiple_sends.py>`_ detects `SWC-113 (Denial of Service with Failed Call) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-113>`_ by checking for multiple calls or sends in a single transaction.
The `multiple sends module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/module/modules/multiple_sends.py>`_ detects `SWC-113 (Denial of Service with Failed Call) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-113>`_ by checking for multiple calls or sends in a single transaction.
*******
Suicide
*******
The `suicide module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/suicide.py>`_ detects `SWC-106 (Unprotected SELFDESTRUCT) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-106>`_.
The `suicide module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/module/modules/suicide.py>`_ detects `SWC-106 (Unprotected SELFDESTRUCT) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-106>`_.
****************************
State Change External Calls
****************************
The `state change external calls module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/state_change_external_calls.py>`_ detects `SWC-107 (Reentrancy) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-107>`_ by detecting state change after calls to an external contract.
The `state change external calls module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/module/modules/state_change_external_calls.py>`_ detects `SWC-107 (Reentrancy) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-107>`_ by detecting state change after calls to an external contract.
****************
Unchecked Retval
****************
The `unchecked retval module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/unchecked_retval.py>`_ detects `SWC-104 (Unchecked Call Return Value) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-104>`_.
The `unchecked retval module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/module/modules/unchecked_retval.py>`_ detects `SWC-104 (Unchecked Call Return Value) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-104>`_.
****************
************************
User Supplied assertion
****************
************************
The `user supplied assertion module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/user_assertions.py>`_ detects `SWC-110 (Assert Violation) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-110>`_ for user-supplied assertions. User supplied assertions should be log messages of the form: :code:`emit AssertionFailed(string)`.
The `user supplied assertion module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/module/modules/user_assertions.py>`_ detects `SWC-110 (Assert Violation) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-110>`_ for user-supplied assertions. User supplied assertions should be log messages of the form: :code:`emit AssertionFailed(string)`.
****************
************************
Arbitrary Storage Write
****************
************************
The `arbitrary storage write module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/arbitrary_write.py>`_ detects `SWC-124 (Write to Arbitrary Storage Location) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-124>`_.
The `arbitrary storage write module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/module/modules/arbitrary_write.py>`_ detects `SWC-124 (Write to Arbitrary Storage Location) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-124>`_.
****************
Arbitrary Jump
****************
The `arbitrary jump module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/arbitrary_jump.py>`_ detects `SWC-127 (Arbitrary Jump with Function Type Variable) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-127>`_.
The `arbitrary jump module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/module/modules/arbitrary_jump.py>`_ detects `SWC-127 (Arbitrary Jump with Function Type Variable) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-127>`_.

@ -0,0 +1,7 @@
mythril
=======
.. toctree::
:maxdepth: 4
mythril

@ -0,0 +1,125 @@
mythril.analysis.module.modules package
=======================================
Submodules
----------
mythril.analysis.module.modules.arbitrary\_jump module
------------------------------------------------------
.. automodule:: mythril.analysis.module.modules.arbitrary_jump
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.module.modules.arbitrary\_write module
-------------------------------------------------------
.. automodule:: mythril.analysis.module.modules.arbitrary_write
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.module.modules.delegatecall module
---------------------------------------------------
.. automodule:: mythril.analysis.module.modules.delegatecall
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.module.modules.dependence\_on\_origin module
-------------------------------------------------------------
.. automodule:: mythril.analysis.module.modules.dependence_on_origin
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.module.modules.dependence\_on\_predictable\_vars module
------------------------------------------------------------------------
.. automodule:: mythril.analysis.module.modules.dependence_on_predictable_vars
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.module.modules.ether\_thief module
---------------------------------------------------
.. automodule:: mythril.analysis.module.modules.ether_thief
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.module.modules.exceptions module
-------------------------------------------------
.. automodule:: mythril.analysis.module.modules.exceptions
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.module.modules.external\_calls module
------------------------------------------------------
.. automodule:: mythril.analysis.module.modules.external_calls
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.module.modules.integer module
----------------------------------------------
.. automodule:: mythril.analysis.module.modules.integer
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.module.modules.multiple\_sends module
------------------------------------------------------
.. automodule:: mythril.analysis.module.modules.multiple_sends
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.module.modules.state\_change\_external\_calls module
---------------------------------------------------------------------
.. automodule:: mythril.analysis.module.modules.state_change_external_calls
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.module.modules.suicide module
----------------------------------------------
.. automodule:: mythril.analysis.module.modules.suicide
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.module.modules.unchecked\_retval module
--------------------------------------------------------
.. automodule:: mythril.analysis.module.modules.unchecked_retval
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.module.modules.user\_assertions module
-------------------------------------------------------
.. automodule:: mythril.analysis.module.modules.user_assertions
:members:
:undoc-members:
:show-inheritance:
Module contents
---------------
.. automodule:: mythril.analysis.module.modules
:members:
:undoc-members:
:show-inheritance:

@ -0,0 +1,53 @@
mythril.analysis.module package
===============================
Subpackages
-----------
.. toctree::
:maxdepth: 4
mythril.analysis.module.modules
Submodules
----------
mythril.analysis.module.base module
-----------------------------------
.. automodule:: mythril.analysis.module.base
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.module.loader module
-------------------------------------
.. automodule:: mythril.analysis.module.loader
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.module.module\_helpers module
----------------------------------------------
.. automodule:: mythril.analysis.module.module_helpers
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.module.util module
-----------------------------------
.. automodule:: mythril.analysis.module.util
:members:
:undoc-members:
:show-inheritance:
Module contents
---------------
.. automodule:: mythril.analysis.module
:members:
:undoc-members:
:show-inheritance:

@ -1,110 +0,0 @@
mythril.analysis.modules package
================================
Submodules
----------
mythril.analysis.modules.base module
------------------------------------
.. automodule:: mythril.analysis.modules.base
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.modules.delegatecall module
--------------------------------------------
.. automodule:: mythril.analysis.modules.delegatecall
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.modules.dependence\_on\_predictable\_vars module
-----------------------------------------------------------------
.. automodule:: mythril.analysis.modules.dependence_on_predictable_vars
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.modules.deprecated\_ops module
-----------------------------------------------
.. automodule:: mythril.analysis.modules.deprecated_ops
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.modules.ether\_thief module
--------------------------------------------
.. automodule:: mythril.analysis.modules.ether_thief
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.modules.exceptions module
------------------------------------------
.. automodule:: mythril.analysis.modules.exceptions
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.modules.external\_calls module
-----------------------------------------------
.. automodule:: mythril.analysis.modules.external_calls
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.modules.integer module
---------------------------------------
.. automodule:: mythril.analysis.modules.integer
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.modules.multiple\_sends module
-----------------------------------------------
.. automodule:: mythril.analysis.modules.multiple_sends
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.modules.suicide module
---------------------------------------
.. automodule:: mythril.analysis.modules.suicide
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.modules.transaction\_order\_dependence module
--------------------------------------------------------------
.. automodule:: mythril.analysis.modules.transaction_order_dependence
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.modules.unchecked\_retval module
-------------------------------------------------
.. automodule:: mythril.analysis.modules.unchecked_retval
:members:
:undoc-members:
:show-inheritance:
Module contents
---------------
.. automodule:: mythril.analysis.modules
:members:
:undoc-members:
:show-inheritance:

@ -5,81 +5,113 @@ Subpackages
-----------
.. toctree::
:maxdepth: 4
mythril.analysis.modules
mythril.analysis.module
Submodules
----------
mythril.analysis.analysis\_args module
--------------------------------------
.. automodule:: mythril.analysis.analysis_args
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.call\_helpers module
-------------------------------------
.. automodule:: mythril.analysis.call_helpers
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.callgraph module
---------------------------------
.. automodule:: mythril.analysis.callgraph
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.issue\_annotation module
-----------------------------------------
.. automodule:: mythril.analysis.issue_annotation
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.ops module
---------------------------
.. automodule:: mythril.analysis.ops
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.potential\_issues module
-----------------------------------------
.. automodule:: mythril.analysis.potential_issues
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.report module
------------------------------
.. automodule:: mythril.analysis.report
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.security module
--------------------------------
.. automodule:: mythril.analysis.security
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.solver module
------------------------------
.. automodule:: mythril.analysis.solver
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.swc\_data module
---------------------------------
.. automodule:: mythril.analysis.swc_data
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.symbolic module
--------------------------------
.. automodule:: mythril.analysis.symbolic
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.traceexplore module
------------------------------------
.. automodule:: mythril.analysis.traceexplore
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
Module contents
---------------
.. automodule:: mythril.analysis
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:

@ -0,0 +1,37 @@
mythril.concolic package
========================
Submodules
----------
mythril.concolic.concolic\_execution module
-------------------------------------------
.. automodule:: mythril.concolic.concolic_execution
:members:
:undoc-members:
:show-inheritance:
mythril.concolic.concrete\_data module
--------------------------------------
.. automodule:: mythril.concolic.concrete_data
:members:
:undoc-members:
:show-inheritance:
mythril.concolic.find\_trace module
-----------------------------------
.. automodule:: mythril.concolic.find_trace
:members:
:undoc-members:
:show-inheritance:
Module contents
---------------
.. automodule:: mythril.concolic
:members:
:undoc-members:
:show-inheritance:

@ -8,23 +8,22 @@ mythril.disassembler.asm module
-------------------------------
.. automodule:: mythril.disassembler.asm
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
mythril.disassembler.disassembly module
---------------------------------------
.. automodule:: mythril.disassembler.disassembly
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
Module contents
---------------
.. automodule:: mythril.disassembler
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:

@ -1,46 +0,0 @@
mythril.ethereum.interface.leveldb package
==========================================
Submodules
----------
mythril.ethereum.interface.leveldb.accountindexing module
---------------------------------------------------------
.. automodule:: mythril.ethereum.interface.leveldb.accountindexing
:members:
:undoc-members:
:show-inheritance:
mythril.ethereum.interface.leveldb.client module
------------------------------------------------
.. automodule:: mythril.ethereum.interface.leveldb.client
:members:
:undoc-members:
:show-inheritance:
mythril.ethereum.interface.leveldb.eth\_db module
-------------------------------------------------
.. automodule:: mythril.ethereum.interface.leveldb.eth_db
:members:
:undoc-members:
:show-inheritance:
mythril.ethereum.interface.leveldb.state module
-----------------------------------------------
.. automodule:: mythril.ethereum.interface.leveldb.state
:members:
:undoc-members:
:show-inheritance:
Module contents
---------------
.. automodule:: mythril.ethereum.interface.leveldb
:members:
:undoc-members:
:show-inheritance:

@ -8,47 +8,46 @@ mythril.ethereum.interface.rpc.base\_client module
--------------------------------------------------
.. automodule:: mythril.ethereum.interface.rpc.base_client
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
mythril.ethereum.interface.rpc.client module
--------------------------------------------
.. automodule:: mythril.ethereum.interface.rpc.client
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
mythril.ethereum.interface.rpc.constants module
-----------------------------------------------
.. automodule:: mythril.ethereum.interface.rpc.constants
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
mythril.ethereum.interface.rpc.exceptions module
------------------------------------------------
.. automodule:: mythril.ethereum.interface.rpc.exceptions
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
mythril.ethereum.interface.rpc.utils module
-------------------------------------------
.. automodule:: mythril.ethereum.interface.rpc.utils
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
Module contents
---------------
.. automodule:: mythril.ethereum.interface.rpc
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:

@ -5,14 +5,14 @@ Subpackages
-----------
.. toctree::
:maxdepth: 4
mythril.ethereum.interface.leveldb
mythril.ethereum.interface.rpc
mythril.ethereum.interface.rpc
Module contents
---------------
.. automodule:: mythril.ethereum.interface
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:

@ -5,8 +5,9 @@ Subpackages
-----------
.. toctree::
:maxdepth: 4
mythril.ethereum.interface
mythril.ethereum.interface
Submodules
----------
@ -15,23 +16,22 @@ mythril.ethereum.evmcontract module
-----------------------------------
.. automodule:: mythril.ethereum.evmcontract
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
mythril.ethereum.util module
----------------------------
.. automodule:: mythril.ethereum.util
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
Module contents
---------------
.. automodule:: mythril.ethereum
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:

@ -8,23 +8,22 @@ mythril.interfaces.cli module
-----------------------------
.. automodule:: mythril.interfaces.cli
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
mythril.interfaces.epic module
------------------------------
.. automodule:: mythril.interfaces.epic
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
Module contents
---------------
.. automodule:: mythril.interfaces
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:

@ -0,0 +1,29 @@
mythril.laser.ethereum.function\_managers package
=================================================
Submodules
----------
mythril.laser.ethereum.function\_managers.exponent\_function\_manager module
----------------------------------------------------------------------------
.. automodule:: mythril.laser.ethereum.function_managers.exponent_function_manager
:members:
:undoc-members:
:show-inheritance:
mythril.laser.ethereum.function\_managers.keccak\_function\_manager module
--------------------------------------------------------------------------
.. automodule:: mythril.laser.ethereum.function_managers.keccak_function_manager
:members:
:undoc-members:
:show-inheritance:
Module contents
---------------
.. automodule:: mythril.laser.ethereum.function_managers
:members:
:undoc-members:
:show-inheritance:

@ -5,10 +5,12 @@ Subpackages
-----------
.. toctree::
:maxdepth: 4
mythril.laser.ethereum.state
mythril.laser.ethereum.strategy
mythril.laser.ethereum.transaction
mythril.laser.ethereum.function_managers
mythril.laser.ethereum.state
mythril.laser.ethereum.strategy
mythril.laser.ethereum.transaction
Submodules
----------
@ -17,87 +19,78 @@ mythril.laser.ethereum.call module
----------------------------------
.. automodule:: mythril.laser.ethereum.call
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
mythril.laser.ethereum.cfg module
---------------------------------
.. automodule:: mythril.laser.ethereum.cfg
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
mythril.laser.ethereum.evm\_exceptions module
---------------------------------------------
.. automodule:: mythril.laser.ethereum.evm_exceptions
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
mythril.laser.ethereum.gas module
---------------------------------
mythril.laser.ethereum.instruction\_data module
-----------------------------------------------
.. automodule:: mythril.laser.ethereum.gas
:members:
:undoc-members:
:show-inheritance:
.. automodule:: mythril.laser.ethereum.instruction_data
:members:
:undoc-members:
:show-inheritance:
mythril.laser.ethereum.instructions module
------------------------------------------
.. automodule:: mythril.laser.ethereum.instructions
:members:
:undoc-members:
:show-inheritance:
mythril.laser.ethereum.keccak module
------------------------------------
.. automodule:: mythril.laser.ethereum.keccak
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
mythril.laser.ethereum.natives module
-------------------------------------
.. automodule:: mythril.laser.ethereum.natives
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
mythril.laser.ethereum.svm module
---------------------------------
.. automodule:: mythril.laser.ethereum.svm
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
mythril.laser.ethereum.taint\_analysis module
---------------------------------------------
mythril.laser.ethereum.time\_handler module
-------------------------------------------
.. automodule:: mythril.laser.ethereum.taint_analysis
:members:
:undoc-members:
:show-inheritance:
.. automodule:: mythril.laser.ethereum.time_handler
:members:
:undoc-members:
:show-inheritance:
mythril.laser.ethereum.util module
----------------------------------
.. automodule:: mythril.laser.ethereum.util
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
Module contents
---------------
.. automodule:: mythril.laser.ethereum
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:

@ -8,79 +8,86 @@ mythril.laser.ethereum.state.account module
-------------------------------------------
.. automodule:: mythril.laser.ethereum.state.account
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
mythril.laser.ethereum.state.annotation module
----------------------------------------------
.. automodule:: mythril.laser.ethereum.state.annotation
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
mythril.laser.ethereum.state.calldata module
--------------------------------------------
.. automodule:: mythril.laser.ethereum.state.calldata
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
mythril.laser.ethereum.state.constraints module
-----------------------------------------------
.. automodule:: mythril.laser.ethereum.state.constraints
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
mythril.laser.ethereum.state.environment module
-----------------------------------------------
.. automodule:: mythril.laser.ethereum.state.environment
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
mythril.laser.ethereum.state.global\_state module
-------------------------------------------------
.. automodule:: mythril.laser.ethereum.state.global_state
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
mythril.laser.ethereum.state.machine\_state module
--------------------------------------------------
.. automodule:: mythril.laser.ethereum.state.machine_state
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
mythril.laser.ethereum.state.memory module
------------------------------------------
.. automodule:: mythril.laser.ethereum.state.memory
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
mythril.laser.ethereum.state.return\_data module
------------------------------------------------
.. automodule:: mythril.laser.ethereum.state.return_data
:members:
:undoc-members:
:show-inheritance:
mythril.laser.ethereum.state.world\_state module
------------------------------------------------
.. automodule:: mythril.laser.ethereum.state.world_state
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
Module contents
---------------
.. automodule:: mythril.laser.ethereum.state
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:

@ -0,0 +1,21 @@
mythril.laser.ethereum.strategy.extensions package
==================================================
Submodules
----------
mythril.laser.ethereum.strategy.extensions.bounded\_loops module
----------------------------------------------------------------
.. automodule:: mythril.laser.ethereum.strategy.extensions.bounded_loops
:members:
:undoc-members:
:show-inheritance:
Module contents
---------------
.. automodule:: mythril.laser.ethereum.strategy.extensions
:members:
:undoc-members:
:show-inheritance:

@ -1,6 +1,14 @@
mythril.laser.ethereum.strategy package
=======================================
Subpackages
-----------
.. toctree::
:maxdepth: 4
mythril.laser.ethereum.strategy.extensions
Submodules
----------
@ -8,15 +16,30 @@ mythril.laser.ethereum.strategy.basic module
--------------------------------------------
.. automodule:: mythril.laser.ethereum.strategy.basic
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
mythril.laser.ethereum.strategy.beam module
-------------------------------------------
.. automodule:: mythril.laser.ethereum.strategy.beam
:members:
:undoc-members:
:show-inheritance:
mythril.laser.ethereum.strategy.concolic module
-----------------------------------------------
.. automodule:: mythril.laser.ethereum.strategy.concolic
:members:
:undoc-members:
:show-inheritance:
Module contents
---------------
.. automodule:: mythril.laser.ethereum.strategy
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:

@ -8,31 +8,30 @@ mythril.laser.ethereum.transaction.concolic module
--------------------------------------------------
.. automodule:: mythril.laser.ethereum.transaction.concolic
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
mythril.laser.ethereum.transaction.symbolic module
--------------------------------------------------
.. automodule:: mythril.laser.ethereum.transaction.symbolic
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
mythril.laser.ethereum.transaction.transaction\_models module
-------------------------------------------------------------
.. automodule:: mythril.laser.ethereum.transaction.transaction_models
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
Module contents
---------------
.. automodule:: mythril.laser.ethereum.transaction
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:

@ -0,0 +1,29 @@
mythril.laser.plugin.plugins.coverage package
=============================================
Submodules
----------
mythril.laser.plugin.plugins.coverage.coverage\_plugin module
-------------------------------------------------------------
.. automodule:: mythril.laser.plugin.plugins.coverage.coverage_plugin
:members:
:undoc-members:
:show-inheritance:
mythril.laser.plugin.plugins.coverage.coverage\_strategy module
---------------------------------------------------------------
.. automodule:: mythril.laser.plugin.plugins.coverage.coverage_strategy
:members:
:undoc-members:
:show-inheritance:
Module contents
---------------
.. automodule:: mythril.laser.plugin.plugins.coverage
:members:
:undoc-members:
:show-inheritance:

@ -0,0 +1,70 @@
mythril.laser.plugin.plugins package
====================================
Subpackages
-----------
.. toctree::
:maxdepth: 4
mythril.laser.plugin.plugins.coverage
mythril.laser.plugin.plugins.summary_backup
Submodules
----------
mythril.laser.plugin.plugins.benchmark module
---------------------------------------------
.. automodule:: mythril.laser.plugin.plugins.benchmark
:members:
:undoc-members:
:show-inheritance:
mythril.laser.plugin.plugins.call\_depth\_limiter module
--------------------------------------------------------
.. automodule:: mythril.laser.plugin.plugins.call_depth_limiter
:members:
:undoc-members:
:show-inheritance:
mythril.laser.plugin.plugins.dependency\_pruner module
------------------------------------------------------
.. automodule:: mythril.laser.plugin.plugins.dependency_pruner
:members:
:undoc-members:
:show-inheritance:
mythril.laser.plugin.plugins.instruction\_profiler module
---------------------------------------------------------
.. automodule:: mythril.laser.plugin.plugins.instruction_profiler
:members:
:undoc-members:
:show-inheritance:
mythril.laser.plugin.plugins.mutation\_pruner module
----------------------------------------------------
.. automodule:: mythril.laser.plugin.plugins.mutation_pruner
:members:
:undoc-members:
:show-inheritance:
mythril.laser.plugin.plugins.plugin\_annotations module
-------------------------------------------------------
.. automodule:: mythril.laser.plugin.plugins.plugin_annotations
:members:
:undoc-members:
:show-inheritance:
Module contents
---------------
.. automodule:: mythril.laser.plugin.plugins
:members:
:undoc-members:
:show-inheritance:

@ -0,0 +1,10 @@
mythril.laser.plugin.plugins.summary\_backup package
====================================================
Module contents
---------------
.. automodule:: mythril.laser.plugin.plugins.summary_backup
:members:
:undoc-members:
:show-inheritance:

@ -0,0 +1,53 @@
mythril.laser.plugin package
============================
Subpackages
-----------
.. toctree::
:maxdepth: 4
mythril.laser.plugin.plugins
Submodules
----------
mythril.laser.plugin.builder module
-----------------------------------
.. automodule:: mythril.laser.plugin.builder
:members:
:undoc-members:
:show-inheritance:
mythril.laser.plugin.interface module
-------------------------------------
.. automodule:: mythril.laser.plugin.interface
:members:
:undoc-members:
:show-inheritance:
mythril.laser.plugin.loader module
----------------------------------
.. automodule:: mythril.laser.plugin.loader
:members:
:undoc-members:
:show-inheritance:
mythril.laser.plugin.signals module
-----------------------------------
.. automodule:: mythril.laser.plugin.signals
:members:
:undoc-members:
:show-inheritance:
Module contents
---------------
.. automodule:: mythril.laser.plugin
:members:
:undoc-members:
:show-inheritance:

@ -5,14 +5,27 @@ Subpackages
-----------
.. toctree::
:maxdepth: 4
mythril.laser.ethereum
mythril.laser.smt
mythril.laser.ethereum
mythril.laser.plugin
mythril.laser.smt
Submodules
----------
mythril.laser.execution\_info module
------------------------------------
.. automodule:: mythril.laser.execution_info
:members:
:undoc-members:
:show-inheritance:
Module contents
---------------
.. automodule:: mythril.laser
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:

@ -1,38 +1,77 @@
mythril.laser.smt package
=========================
Subpackages
-----------
.. toctree::
:maxdepth: 4
mythril.laser.smt.solver
Submodules
----------
mythril.laser.smt.array module
------------------------------
.. automodule:: mythril.laser.smt.array
:members:
:undoc-members:
:show-inheritance:
mythril.laser.smt.bitvec module
-------------------------------
.. automodule:: mythril.laser.smt.bitvec
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
mythril.laser.smt.bitvec\_helper module
---------------------------------------
.. automodule:: mythril.laser.smt.bitvec_helper
:members:
:undoc-members:
:show-inheritance:
mythril.laser.smt.bool module
-----------------------------
.. automodule:: mythril.laser.smt.bool
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
mythril.laser.smt.expression module
-----------------------------------
.. automodule:: mythril.laser.smt.expression
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
mythril.laser.smt.function module
---------------------------------
.. automodule:: mythril.laser.smt.function
:members:
:undoc-members:
:show-inheritance:
mythril.laser.smt.model module
------------------------------
.. automodule:: mythril.laser.smt.model
:members:
:undoc-members:
:show-inheritance:
Module contents
---------------
.. automodule:: mythril.laser.smt
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:

@ -0,0 +1,37 @@
mythril.laser.smt.solver package
================================
Submodules
----------
mythril.laser.smt.solver.independence\_solver module
----------------------------------------------------
.. automodule:: mythril.laser.smt.solver.independence_solver
:members:
:undoc-members:
:show-inheritance:
mythril.laser.smt.solver.solver module
--------------------------------------
.. automodule:: mythril.laser.smt.solver.solver
:members:
:undoc-members:
:show-inheritance:
mythril.laser.smt.solver.solver\_statistics module
--------------------------------------------------
.. automodule:: mythril.laser.smt.solver.solver_statistics
:members:
:undoc-members:
:show-inheritance:
Module contents
---------------
.. automodule:: mythril.laser.smt.solver
:members:
:undoc-members:
:show-inheritance:

@ -0,0 +1,37 @@
mythril.mythril package
=======================
Submodules
----------
mythril.mythril.mythril\_analyzer module
----------------------------------------
.. automodule:: mythril.mythril.mythril_analyzer
:members:
:undoc-members:
:show-inheritance:
mythril.mythril.mythril\_config module
--------------------------------------
.. automodule:: mythril.mythril.mythril_config
:members:
:undoc-members:
:show-inheritance:
mythril.mythril.mythril\_disassembler module
--------------------------------------------
.. automodule:: mythril.mythril.mythril_disassembler
:members:
:undoc-members:
:show-inheritance:
Module contents
---------------
.. automodule:: mythril.mythril
:members:
:undoc-members:
:show-inheritance:

@ -0,0 +1,37 @@
mythril.plugin package
======================
Submodules
----------
mythril.plugin.discovery module
-------------------------------
.. automodule:: mythril.plugin.discovery
:members:
:undoc-members:
:show-inheritance:
mythril.plugin.interface module
-------------------------------
.. automodule:: mythril.plugin.interface
:members:
:undoc-members:
:show-inheritance:
mythril.plugin.loader module
----------------------------
.. automodule:: mythril.plugin.loader
:members:
:undoc-members:
:show-inheritance:
Module contents
---------------
.. automodule:: mythril.plugin
:members:
:undoc-members:
:show-inheritance:

@ -1,18 +1,22 @@
Mythril Package
mythril package
===============
Subpackages
-----------
.. toctree::
mythril.analysis
mythril.disassembler
mythril.ethereum
mythril.interfaces
mythril.laser
mythril.solidity
mythril.support
:maxdepth: 4
mythril.analysis
mythril.concolic
mythril.disassembler
mythril.ethereum
mythril.interfaces
mythril.laser
mythril.mythril
mythril.plugin
mythril.solidity
mythril.support
Submodules
----------
@ -21,31 +25,14 @@ mythril.exceptions module
-------------------------
.. automodule:: mythril.exceptions
:members:
:undoc-members:
:show-inheritance:
mythril.mythril module
----------------------
.. automodule:: mythril.mythril
:members:
:undoc-members:
:show-inheritance:
mythril.version module
----------------------
.. automodule:: mythril.version
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
Module contents
---------------
.. automodule:: mythril
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:

@ -8,15 +8,14 @@ mythril.solidity.soliditycontract module
----------------------------------------
.. automodule:: mythril.solidity.soliditycontract
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
Module contents
---------------
.. automodule:: mythril.solidity
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:

@ -8,39 +8,78 @@ mythril.support.loader module
-----------------------------
.. automodule:: mythril.support.loader
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
mythril.support.lock module
---------------------------
.. automodule:: mythril.support.lock
:members:
:undoc-members:
:show-inheritance:
mythril.support.model module
----------------------------
.. automodule:: mythril.support.model
:members:
:undoc-members:
:show-inheritance:
mythril.support.opcodes module
------------------------------
.. automodule:: mythril.support.opcodes
:members:
:undoc-members:
:show-inheritance:
mythril.support.signatures module
---------------------------------
.. automodule:: mythril.support.signatures
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:
mythril.support.support\_utils module
-------------------------------------
mythril.support.source\_support module
--------------------------------------
.. automodule:: mythril.support.support_utils
:members:
:undoc-members:
:show-inheritance:
.. automodule:: mythril.support.source_support
:members:
:undoc-members:
:show-inheritance:
mythril.support.truffle module
------------------------------
mythril.support.start\_time module
----------------------------------
.. automodule:: mythril.support.start_time
:members:
:undoc-members:
:show-inheritance:
mythril.support.support\_args module
------------------------------------
.. automodule:: mythril.support.truffle
:members:
:undoc-members:
:show-inheritance:
.. automodule:: mythril.support.support_args
:members:
:undoc-members:
:show-inheritance:
mythril.support.support\_utils module
-------------------------------------
.. automodule:: mythril.support.support_utils
:members:
:undoc-members:
:show-inheritance:
Module contents
---------------
.. automodule:: mythril.support
:members:
:undoc-members:
:show-inheritance:
:members:
:undoc-members:
:show-inheritance:

@ -1,63 +0,0 @@
MythX Analysis
=================
Run :code:`myth pro` with one of the input options described below will run a `MythX analysis <https://mythx.io>`_ on the desired input. This includes a run of Mythril, the fuzzer Harvey, and the static analysis engine Maru and has some false-positive filtering only possible by combining the tool capabilities.
**************
Authentication
**************
In order to authenticate with the MythX API, set the environment variables ``MYTHX_PASSWORD`` and ``MYTHX_ETH_ADDRESS``.
.. code-block:: bash
$ export MYTHX_ETH_ADDRESS='0x0000000000000000000000000000000000000000'
$ export MYTHX_PASSWORD='password'
***********************
Analyzing Solidity Code
***********************
The input format is the same as a regular Mythril analysis.
.. code-block:: bash
$ myth pro ether_send.sol
==== Unprotected Ether Withdrawal ====
SWC ID: 105
Severity: High
Contract: Crowdfunding
Function name: withdrawfunds()
PC address: 730
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 an equivalent amount of ETH to it. This is likely to be a vulnerability.
--------------------
In file: tests/testdata/input_contracts/ether_send.sol:21
msg.sender.transfer(address(this).balance)
--------------------
If an input file contains multiple contract definitions, Mythril analyzes the *last* bytecode output produced by solc. You can override this by specifying the contract name explicitly:
.. code-block:: bash
myth pro OmiseGo.sol:OMGToken
To specify a contract address, use :code:`-a <address>`
****************************
Analyzing On-Chain Contracts
****************************
Analyzing a mainnet contract via INFURA:
.. code-block:: bash
myth pro -a 0x5c436ff914c458983414019195e0f4ecbef9e6dd
Adding the :code:`-l` flag will cause mythril to automatically retrieve dependencies, such as dynamically linked library contracts:
.. code-block:: bash
myth -v4 pro -l -a 0xEbFD99838cb0c132016B9E117563CB41f2B02264

@ -76,11 +76,10 @@ Analyze mainnet contract via INFURA:
myth analyze -a 0x5c436ff914c458983414019195e0f4ecbef9e6dd --infura-id <ID>
You can also use the environment variable `INFURA_ID` instead of the cmd line argument or set it in ~/.mythril/config.ini.
Adding the :code:`-l` flag will cause mythril to automatically retrieve dependencies, such as dynamically linked library contracts:
.. code-block:: bash
myth -v4 analyze -l -a 0xEbFD99838cb0c132016B9E117563CB41f2B02264 --infura-id <ID>
myth -v4 analyze -a 0xEbFD99838cb0c132016B9E117563CB41f2B02264 --infura-id <ID>
******************
Speed vs. Coverage

@ -0,0 +1,511 @@
Tutorial
======================
******************************************
Executing Mythril on Simple Contracts
******************************************
We consider a contract simple if it does not have any imports, like the following contract:
.. code-block:: solidity
contract Exceptions {
uint256[8] myarray;
uint counter = 0;
function assert1() public pure {
uint256 i = 1;
assert(i == 0);
}
function counter_increase() public {
counter+=1;
}
function assert5(uint input_x) public view{
require(counter>2);
assert(input_x > 10);
}
function assert2() public pure {
uint256 i = 1;
assert(i > 0);
}
function assert3(uint256 input) public pure {
assert(input != 23);
}
function require_is_fine(uint256 input) public pure {
require(input != 23);
}
function this_is_fine(uint256 input) public pure {
if (input > 0) {
uint256 i = 1/input;
}
}
function this_is_find_2(uint256 index) public view {
if (index < 8) {
uint256 i = myarray[index];
}
}
}
We can execute such a contract by directly using the following command:
.. code-block:: bash
$ myth analyze <file_path>
This execution can give the following output:
.. code-block:: none
==== Exception State ====
SWC ID: 110
Severity: Medium
Contract: Exceptions
Function name: assert1()
PC address: 708
Estimated Gas Usage: 207 - 492
An assertion violation was triggered.
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).
--------------------
In file: solidity_examples/exceptions.sol:7
assert(i == 0)
--------------------
Initial State:
Account: [CREATOR], balance: 0x2, nonce:0, storage:{}
Account: [ATTACKER], balance: 0x0, nonce:0, storage:{}
Transaction Sequence:
Caller: [CREATOR], calldata: , value: 0x0
Caller: [ATTACKER], function: assert1(), txdata: 0xb34c3610, value: 0x0
==== Exception State ====
SWC ID: 110
Severity: Medium
Contract: Exceptions
Function name: assert3(uint256)
PC address: 708
Estimated Gas Usage: 482 - 767
An assertion violation was triggered.
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).
--------------------
In file: solidity_examples/exceptions.sol:20
assert(input != 23)
--------------------
Initial State:
Account: [CREATOR], balance: 0x40207f9b0, nonce:0, storage:{}
Account: [ATTACKER], balance: 0x0, nonce:0, storage:{}
Transaction Sequence:
Caller: [CREATOR], calldata: , value: 0x0
Caller: [SOMEGUY], function: assert3(uint256), txdata: 0x546455b50000000000000000000000000000000000000000000000000000000000000017, value: 0x0
We can observe that the function ``assert5(uint256)`` should have an assertion failure
with the assertion ``assert(input_x > 10)`` which is missing from our output. This can be attributed to
Mythril's default configuration of running three transactions. We can increase the transaction count to 4
using the ``-t <tx_count>``.
.. code-block:: bash
$ myth analyze <file_path> -t 4
This gives the following execution output:
.. code-block:: none
==== Exception State ====
SWC ID: 110
Severity: Medium
Contract: Exceptions
Function name: assert1()
PC address: 731
Estimated Gas Usage: 207 - 492
An assertion violation was triggered.
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).
--------------------
In file: solidity_examples/exceptions.sol:7
assert(i == 0)
--------------------
Initial State:
Account: [CREATOR], balance: 0x2, nonce:0, storage:{}
Account: [ATTACKER], balance: 0x0, nonce:0, storage:{}
Transaction Sequence:
Caller: [CREATOR], calldata: , value: 0x0
Caller: [ATTACKER], function: assert1(), txdata: 0xb34c3610, value: 0x0
==== Exception State ====
SWC ID: 110
Severity: Medium
Contract: Exceptions
Function name: assert3(uint256)
PC address: 731
Estimated Gas Usage: 504 - 789
An assertion violation was triggered.
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).
--------------------
In file: solidity_examples/exceptions.sol:22
assert(input != 23)
--------------------
Initial State:
Account: [CREATOR], balance: 0x3, nonce:0, storage:{}
Account: [ATTACKER], balance: 0x0, nonce:0, storage:{}
Transaction Sequence:
Caller: [CREATOR], calldata: , value: 0x0
Caller: [ATTACKER], function: assert3(uint256), txdata: 0x546455b50000000000000000000000000000000000000000000000000000000000000017, value: 0x0
==== Exception State ====
SWC ID: 110
Severity: Medium
Contract: Exceptions
Function name: assert5(uint256)
PC address: 731
Estimated Gas Usage: 1302 - 1587
An assertion violation was triggered.
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).
--------------------
In file: solidity_examples/exceptions.sol:14
assert(input_x > 10)
--------------------
Initial State:
Account: [CREATOR], balance: 0x20000000, nonce:0, storage:{}
Account: [ATTACKER], balance: 0x1000000, nonce:0, storage:{}
Transaction Sequence:
Caller: [CREATOR], calldata: , value: 0x0
Caller: [ATTACKER], function: counter_increase(), txdata: 0xe47b0253, value: 0x0
Caller: [CREATOR], function: counter_increase(), txdata: 0xe47b0253, value: 0x0
Caller: [CREATOR], function: counter_increase(), txdata: 0xe47b0253, value: 0x0
Caller: [ATTACKER], function: assert5(uint256), txdata: 0x1d5d53dd0000000000000000000000000000000000000000000000000000000000000003, value: 0x0
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).",
"filename": "solidity_examples/exceptions.sol",
"function": "assert1()",
"lineno": 7,
"max_gas_used": 492,
"min_gas_used": 207,
"severity": "Medium",
"sourceMap": ":::i",
"swc-id": "110",
"title": "Exception State",
"tx_sequence": {
"initialState": {
"accounts": {
"0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe": {
"balance": "0x2",
"code": "",
"nonce": 0,
"storage": "{}"
},
"0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef": {
"balance": "0x0",
"code": "",
"nonce": 0,
"storage": "{}"
}
}
},
"steps": [{
"address": "",
"calldata": "",
"input": "0x6080604052600060085534801561001557600080fd5b506103f7806100256000396000f3fe608060405234801561001057600080fd5b50600436106100885760003560e01c8063b34c36101161005b578063b34c3610146100fd578063b630d70614610107578063e47b025314610123578063f44f13d81461012d57610088565b806301d4277c1461008d5780631d5d53dd146100a9578063546455b5146100c557806378375f14146100e1575b600080fd5b6100a760048036038101906100a29190610251565b610137565b005b6100c360048036038101906100be9190610251565b61015e565b005b6100df60048036038101906100da9190610251565b610181565b005b6100fb60048036038101906100f69190610251565b610196565b005b6101056101a7565b005b610121600480360381019061011c9190610251565b6101c1565b005b61012b6101e0565b005b6101356101fc565b005b600881101561015b5760008082600881106101555761015461027e565b5b01549050505b50565b60026008541161016d57600080fd5b600a811161017e5761017d6102ad565b5b50565b6017811415610193576101926102ad565b5b50565b60178114156101a457600080fd5b50565b600060019050600081146101be576101bd6102ad565b5b50565b60008111156101dd5760008160016101d9919061033a565b9050505b50565b6001600860008282546101f3919061036b565b92505081905550565b60006001905060008111610213576102126102ad565b5b50565b600080fd5b6000819050919050565b61022e8161021b565b811461023957600080fd5b50565b60008135905061024b81610225565b92915050565b60006020828403121561026757610266610216565b5b60006102758482850161023c565b91505092915050565b7f4e487b7100000000000000000000000000000000000000000000000000000000600052603260045260246000fd5b7f4e487b7100000000000000000000000000000000000000000000000000000000600052600160045260246000fd5b7f4e487b7100000000000000000000000000000000000000000000000000000000600052601260045260246000fd5b7f4e487b7100000000000000000000000000000000000000000000000000000000600052601160045260246000fd5b60006103458261021b565b91506103508361021b565b9250826103605761035f6102dc565b5b828204905092915050565b60006103768261021b565b91506103818361021b565b9250827fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff038211156103b6576103b561030b565b5b82820190509291505056fea2646970667358221220b474c01fa60d997027e1ceb779bcb2b34b6752282e0ea3a038a08b889fe0163f64736f6c634300080c0033",
"name": "unknown",
"origin": "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe",
"value": "0x0"
}, {
"address": "0x901d12ebe1b195e5aa8748e62bd7734ae19b51f",
"calldata": "0xb34c3610",
"input": "0xb34c3610",
"name": "assert1()",
"origin": "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef",
"resolved_input": null,
"value": "0x0"
}]
}
}, {
"address": 731,
"code": "assert(input != 23)",
"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).",
"filename": "solidity_examples/exceptions.sol",
"function": "assert3(uint256)",
"lineno": 22,
"max_gas_used": 789,
"min_gas_used": 504,
"severity": "Medium",
"sourceMap": ":::i",
"swc-id": "110",
"title": "Exception State",
"tx_sequence": {
"initialState": {
"accounts": {
"0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe": {
"balance": "0x3",
"code": "",
"nonce": 0,
"storage": "{}"
},
"0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef": {
"balance": "0x0",
"code": "",
"nonce": 0,
"storage": "{}"
}
}
},
"steps": [{
"address": "",
"calldata": "",
"input": "0x6080604052600060085534801561001557600080fd5b506103f7806100256000396000f3fe608060405234801561001057600080fd5b50600436106100885760003560e01c8063b34c36101161005b578063b34c3610146100fd578063b630d70614610107578063e47b025314610123578063f44f13d81461012d57610088565b806301d4277c1461008d5780631d5d53dd146100a9578063546455b5146100c557806378375f14146100e1575b600080fd5b6100a760048036038101906100a29190610251565b610137565b005b6100c360048036038101906100be9190610251565b61015e565b005b6100df60048036038101906100da9190610251565b610181565b005b6100fb60048036038101906100f69190610251565b610196565b005b6101056101a7565b005b610121600480360381019061011c9190610251565b6101c1565b005b61012b6101e0565b005b6101356101fc565b005b600881101561015b5760008082600881106101555761015461027e565b5b01549050505b50565b60026008541161016d57600080fd5b600a811161017e5761017d6102ad565b5b50565b6017811415610193576101926102ad565b5b50565b60178114156101a457600080fd5b50565b600060019050600081146101be576101bd6102ad565b5b50565b60008111156101dd5760008160016101d9919061033a565b9050505b50565b6001600860008282546101f3919061036b565b92505081905550565b60006001905060008111610213576102126102ad565b5b50565b600080fd5b6000819050919050565b61022e8161021b565b811461023957600080fd5b50565b60008135905061024b81610225565b92915050565b60006020828403121561026757610266610216565b5b60006102758482850161023c565b91505092915050565b7f4e487b7100000000000000000000000000000000000000000000000000000000600052603260045260246000fd5b7f4e487b7100000000000000000000000000000000000000000000000000000000600052600160045260246000fd5b7f4e487b7100000000000000000000000000000000000000000000000000000000600052601260045260246000fd5b7f4e487b7100000000000000000000000000000000000000000000000000000000600052601160045260246000fd5b60006103458261021b565b91506103508361021b565b9250826103605761035f6102dc565b5b828204905092915050565b60006103768261021b565b91506103818361021b565b9250827fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff038211156103b6576103b561030b565b5b82820190509291505056fea2646970667358221220b474c01fa60d997027e1ceb779bcb2b34b6752282e0ea3a038a08b889fe0163f64736f6c634300080c0033",
"name": "unknown",
"origin": "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe",
"value": "0x0"
}, {
"address": "0x901d12ebe1b195e5aa8748e62bd7734ae19b51f",
"calldata": "0x546455b50000000000000000000000000000000000000000000000000000000000000017",
"input": "0x546455b50000000000000000000000000000000000000000000000000000000000000017",
"name": "assert3(uint256)",
"origin": "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef",
"resolved_input": [23],
"value": "0x0"
}]
}
}, {
"address": 731,
"code": "assert(input_x > 10)",
"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).",
"filename": "solidity_examples/exceptions.sol",
"function": "assert5(uint256)",
"lineno": 14,
"max_gas_used": 1587,
"min_gas_used": 1302,
"severity": "Medium",
"sourceMap": ":::i",
"swc-id": "110",
"title": "Exception State",
"tx_sequence": {
"initialState": {
"accounts": {
"0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe": {
"balance": "0x0",
"code": "",
"nonce": 0,
"storage": "{}"
},
"0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef": {
"balance": "0x0",
"code": "",
"nonce": 0,
"storage": "{}"
}
}
},
"steps": [{
"address": "",
"calldata": "",
"input": "0x6080604052600060085534801561001557600080fd5b506103f7806100256000396000f3fe608060405234801561001057600080fd5b50600436106100885760003560e01c8063b34c36101161005b578063b34c3610146100fd578063b630d70614610107578063e47b025314610123578063f44f13d81461012d57610088565b806301d4277c1461008d5780631d5d53dd146100a9578063546455b5146100c557806378375f14146100e1575b600080fd5b6100a760048036038101906100a29190610251565b610137565b005b6100c360048036038101906100be9190610251565b61015e565b005b6100df60048036038101906100da9190610251565b610181565b005b6100fb60048036038101906100f69190610251565b610196565b005b6101056101a7565b005b610121600480360381019061011c9190610251565b6101c1565b005b61012b6101e0565b005b6101356101fc565b005b600881101561015b5760008082600881106101555761015461027e565b5b01549050505b50565b60026008541161016d57600080fd5b600a811161017e5761017d6102ad565b5b50565b6017811415610193576101926102ad565b5b50565b60178114156101a457600080fd5b50565b600060019050600081146101be576101bd6102ad565b5b50565b60008111156101dd5760008160016101d9919061033a565b9050505b50565b6001600860008282546101f3919061036b565b92505081905550565b60006001905060008111610213576102126102ad565b5b50565b600080fd5b6000819050919050565b61022e8161021b565b811461023957600080fd5b50565b60008135905061024b81610225565b92915050565b60006020828403121561026757610266610216565b5b60006102758482850161023c565b91505092915050565b7f4e487b7100000000000000000000000000000000000000000000000000000000600052603260045260246000fd5b7f4e487b7100000000000000000000000000000000000000000000000000000000600052600160045260246000fd5b7f4e487b7100000000000000000000000000000000000000000000000000000000600052601260045260246000fd5b7f4e487b7100000000000000000000000000000000000000000000000000000000600052601160045260246000fd5b60006103458261021b565b91506103508361021b565b9250826103605761035f6102dc565b5b828204905092915050565b60006103768261021b565b91506103818361021b565b9250827fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff038211156103b6576103b561030b565b5b82820190509291505056fea2646970667358221220b474c01fa60d997027e1ceb779bcb2b34b6752282e0ea3a038a08b889fe0163f64736f6c634300080c0033",
"name": "unknown",
"origin": "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe",
"value": "0x0"
}, {
"address": "0x901d12ebe1b195e5aa8748e62bd7734ae19b51f",
"calldata": "0xe47b0253",
"input": "0xe47b0253",
"name": "counter_increase()",
"origin": "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe",
"resolved_input": null,
"value": "0x0"
}, {
"address": "0x901d12ebe1b195e5aa8748e62bd7734ae19b51f",
"calldata": "0xe47b0253",
"input": "0xe47b0253",
"name": "counter_increase()",
"origin": "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef",
"resolved_input": null,
"value": "0x0"
}, {
"address": "0x901d12ebe1b195e5aa8748e62bd7734ae19b51f",
"calldata": "0xe47b0253",
"input": "0xe47b0253",
"name": "counter_increase()",
"origin": "0xaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa",
"resolved_input": null,
"value": "0x0"
}, {
"address": "0x901d12ebe1b195e5aa8748e62bd7734ae19b51f",
"calldata": "0x1d5d53dd0000000000000000000000000000000000000000000000000000000000000003",
"input": "0x1d5d53dd0000000000000000000000000000000000000000000000000000000000000003",
"name": "assert5(uint256)",
"origin": "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef",
"resolved_input": [3],
"value": "0x0"
}]
}
}],
"success": true
}
We can observe that the "resolved_input" field for the final transaction resolves to ``[3]``. Although this resolution
fails in some circumstances where output generated by Mythril is although executable on the bytecode, it cannot be decoded due
to not being a valid ABI.
There are interesting options such as ``--execution-timeout <seconds>`` and ``--solver-timeout <milliseconds>``
which can be increased for better results. The default execution-timeout and solver-timeout are 86400 seconds and
25000 milliseconds respectively.
********************************************************
Executing Mythril on Contracts with Imports
********************************************************
Consider the following contract:
.. code-block:: solidity
import "@openzeppelin/contracts/token/PRC20/PRC20.sol";
contract Nothing is PRC20{
string x_0 = "";
bytes3 x_1 = "A";
bytes5 x_2 = "E";
bytes5 x_3 = "";
bytes3 x_4 = "I";
bytes3 x_5 = "U";
bytes3 x_6 = "O";
bytes3 x_7 = "0";
bytes3 x_8 = "U";
bytes3 x_9 = "U";
function stringCompare(string memory a, string memory b) internal pure returns (bool) {
if(bytes(a).length != bytes(b).length) {
return false;
} else {
return keccak256(bytes(a)) == keccak256(bytes(b));
}
}
function nothing(string memory g_0, bytes3 g_1, bytes5 g_2, bytes5 g_3, bytes3 g_4, bytes3 g_5, bytes3 g_6, bytes3 g_7, bytes3 g_8, bytes3 g_9, bytes3 g_10, bytes3 g_11) public view returns (bool){
if (!stringCompare(g_0, x_0)) return false;
if (g_1 != x_1) return false;
if (g_2 != x_2) return false;
if (g_3 != x_3) return false;
if (g_4 != x_4) return false;
if (g_5 != x_5) return false;
if (g_6 != x_6) return false;
if (g_7 != x_7) return false;
if (g_8 != x_8) return false;
if (g_9 != x_9) return false;
if (g_10 != x_9) return false;
if (g_11 != x_9) return false;
return true;
}
}
When this contract is directly executed, by using the following command:
.. code-block:: bash
$ myth analyze <file_path>
We encounter the following error:
.. code-block:: none
mythril.interfaces.cli [ERROR]: Solc experienced a fatal error.
ParserError: Source "@openzeppelin/contracts/token/PRC20/PRC20.sol" not found: File not found. Searched the following locations: "".
--> <file_path>:1:1:
|
1 | import "@openzeppelin/contracts/token/PRC20/PRC20.sol";
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
This is because Mythril uses Solidity to compile the program, to circumvent this issue we can use the following solc-json file:
.. code-block:: json
{
"remappings": [ "@openzeppelin/contracts/token/PRC20/=node_modules/PRC20" ],
}
Here we are mapping the import ``@openzeppelin/contracts/token/PRC20/`` to the path which contains ``PRC20.sol`` which in this case
is ``node_modules/PRC20``. This instructs the compiler to search for anything with the prefix ``@openzeppelin/contracts/token/PRC20/` `
in the path ``node_modules/PRC20`` in our file system. We feed to file to Mythril using ``--solc-json`` argument.
.. code-block:: bash
$ myth analyze {file_path} --solc-json {json_file_path}
This can effectively execute the file since the Solidity compiler can locate `PRC20.sol`. For more information on remappings, you can
refer to `Solc docs <https://docs.soliditylang.org/en/v0.8.14/using-the-compiler.html#base-path-and-import-remapping>`_.

@ -168,6 +168,7 @@ class Optimize(Z3PPObject):
sat: CheckSatResult = ...
unsat: CheckSatResult = ...
@overload
def Int(name: str) -> ArithRef: ...
@overload

@ -1,7 +1,7 @@
#!/usr/bin/env python3
# -*- coding: utf-8 -*-
"""mythril.py: Bug hunting on the Ethereum blockchain
http://www.github.com/b-mueller/mythril
http://www.github.com/ConsenSys/mythril
"""
from sys import exit
import mythril.interfaces.cli

@ -4,4 +4,4 @@ This file is suitable for sourcing inside POSIX shell, e.g. bash as well
as for importing into Python.
"""
__version__ = "v0.22.24"
__version__ = "v0.23.9"

@ -19,7 +19,7 @@ def get_call_from_state(state: GlobalState) -> Union[Call, None]:
stack = state.mstate.stack
if op in ("CALL", "CALLCODE"):
gas, to, value, meminstart, meminsz, memoutstart, memoutsz = (
gas, to, value, meminstart, meminsz, _, _ = (
get_variable(stack[-1]),
get_variable(stack[-2]),
get_variable(stack[-3]),
@ -47,7 +47,7 @@ def get_call_from_state(state: GlobalState) -> Union[Call, None]:
return Call(state.node, state, None, op, to, gas, value)
else:
gas, to, meminstart, meminsz, memoutstart, memoutsz = (
gas, to, meminstart, meminsz, _, _ = (
get_variable(stack[-1]),
get_variable(stack[-2]),
get_variable(stack[-3]),

@ -0,0 +1,34 @@
from typing import List
from mythril.analysis.report import Issue
from mythril.laser.ethereum.state.annotation import StateAnnotation
from mythril.laser.smt import Bool
from copy import deepcopy
class IssueAnnotation(StateAnnotation):
def __init__(self, conditions: List[Bool], issue: Issue, detector):
"""
Issue Annotation to propogate issues
- conditions: A list of independent conditions [a, b, c, ...]
Each of these have to be independently be satisfied
- issue: The issue of the annotation
- detector: The detection module
"""
self.conditions = conditions
self.issue = issue
self.detector = detector
def persist_to_world_state(self) -> bool:
return True
@property
def persist_over_calls(self) -> bool:
return True
def __copy__(self):
return IssueAnnotation(
conditions=deepcopy(self.conditions),
issue=self.issue,
detector=self.detector,
)

@ -4,11 +4,12 @@ This module includes an definition of the DetectionModule interface.
DetectionModules implement different analysis rules to find weaknesses and vulnerabilities.
"""
import logging
from typing import List, Set, Optional
from typing import List, Set, Optional, Tuple
from mythril.analysis.report import Issue
from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.support.support_args import args
from mythril.support.support_utils import get_code_hash
from abc import ABC, abstractmethod
from enum import Enum
@ -17,7 +18,7 @@ log = logging.getLogger(__name__)
class EntryPoint(Enum):
""" EntryPoint Enum
"""EntryPoint Enum
This enum is used to signify the entry_point of detection modules.
See also the class documentation of DetectionModule
@ -33,30 +34,41 @@ class DetectionModule(ABC):
All custom-built detection modules must inherit from this class.
There are several class properties that expose information about the detection modules
- name: The name of the detection module
- swc_id: The SWC ID associated with the weakness that the module detects
- description: A description of the detection module, and what it detects
- entry_point: Mythril can run callback style detection modules, or modules that search the statespace.
:param name: The name of the detection module
:param swc_id: The SWC ID associated with the weakness that the module detects
:param description: A description of the detection module, and what it detects
:param entry_point: Mythril can run callback style detection modules, or modules that search the statespace.
[IMPORTANT] POST entry points severely slow down the analysis, try to always use callback style modules
- pre_hooks: A list of instructions to hook the laser vm for (pre execution of the instruction)
- post_hooks: A list of instructions to hook the laser vm for (post execution of the instruction)
:param pre_hooks: A list of instructions to hook the laser vm for (pre execution of the instruction)
:param post_hooks: A list of instructions to hook the laser vm for (post execution of the instruction)
"""
name = "Detection Module Name / Title"
swc_id = "SWC-000"
description = "Detection module description"
entry_point = EntryPoint.CALLBACK # type: EntryPoint
pre_hooks = [] # type: List[str]
post_hooks = [] # type: List[str]
entry_point: EntryPoint = EntryPoint.CALLBACK
pre_hooks: List[str] = []
post_hooks: List[str] = []
def __init__(self) -> None:
self.issues = [] # type: List[Issue]
self.cache = set() # type: Set[int]
self.issues: List[Issue] = []
self.cache: Set[Tuple[int, str]] = set()
self.auto_cache = True
def reset_module(self):
""" Resets the storage of this module """
"""Resets the storage of this module"""
self.issues = []
def update_cache(self, issues=None):
"""
Updates cache with param issues, updates against self.issues, if the param is None
:param issues: The issues used to update the cache
"""
issues = issues or self.issues
for issue in issues:
self.cache.add((issue.address, issue.bytecode_hash))
def execute(self, target: GlobalState) -> Optional[List[Issue]]:
"""The entry point for execution, which is being called by Mythril.
@ -66,10 +78,23 @@ class DetectionModule(ABC):
log.debug("Entering analysis module: {}".format(self.__class__.__name__))
result = self._execute(target)
if (
target.get_current_instruction()["address"],
get_code_hash(target.environment.code.bytecode),
) in self.cache and self.auto_cache:
log.debug(
f"Issue in cache for the analysis module: {self.__class__.__name__}, address: {target.get_current_instruction()['address']}"
)
return []
result = self._execute(target)
log.debug("Exiting analysis module: {}".format(self.__class__.__name__))
if result and not args.use_issue_annotations:
if self.auto_cache:
self.update_cache(result)
self.issues += result
return result
@abstractmethod

@ -1,5 +1,6 @@
from mythril.analysis.module.base import DetectionModule, EntryPoint
from mythril.support.support_utils import Singleton
from mythril.support.support_args import args
from mythril.analysis.module.modules.arbitrary_jump import ArbitraryJump
from mythril.analysis.module.modules.arbitrary_write import ArbitraryStorage
@ -51,7 +52,7 @@ class ModuleLoader(object, metaclass=Singleton):
entry_point: Optional[EntryPoint] = None,
white_list: Optional[List[str]] = None,
) -> List[DetectionModule]:
""" Gets registered detection modules
"""Gets registered detection modules
:param entry_point: If specified: only return detection modules with this entry point
:param white_list: If specified: only return whitelisted detection modules
@ -75,7 +76,12 @@ class ModuleLoader(object, metaclass=Singleton):
result = [
module for module in result if type(module).__name__ in white_list
]
if args.use_integer_module is False:
result = [
module
for module in result
if type(module).__name__ != "IntegerArithmetics"
]
if entry_point:
result = [module for module in result if module.entry_point == entry_point]

@ -2,5 +2,12 @@ import traceback
def is_prehook() -> bool:
"""Check if we are in prehook. One of Bernhard's trademark hacks!"""
"""Check if we are in prehook. One of Bernhard's trademark hacks!
Let's leave it to this for now, unless we need to check prehook for
a lot more modules.
"""
assert ("pre_hook" in traceback.format_stack()[-5]) or (
"post_hook" in traceback.format_stack()[-5]
)
return "pre_hook" in traceback.format_stack()[-5]

@ -1,9 +1,16 @@
"""This module contains the detection code for Arbitrary jumps."""
import logging
from mythril.exceptions import UnsatError
from mythril.analysis.solver import get_transaction_sequence, UnsatError
from mythril.analysis.issue_annotation import IssueAnnotation
from mythril.analysis.module.base import DetectionModule, Issue, EntryPoint
from mythril.analysis.swc_data import ARBITRARY_JUMP
from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.laser.smt import And, BitVec, symbol_factory
from mythril.support.model import get_model
log = logging.getLogger(__name__)
@ -13,6 +20,26 @@ Search for jumps to arbitrary locations in the bytecode
"""
def is_unique_jumpdest(jump_dest: BitVec, state: GlobalState) -> bool:
"""
Handles cases where jump_dest evaluates to a single concrete value
"""
try:
model = get_model(state.world_state.constraints)
except UnsatError:
return True
concrete_jump_dest = model.eval(jump_dest.raw, model_completion=True)
try:
model = get_model(
state.world_state.constraints
+ [symbol_factory.BitVecVal(concrete_jump_dest.as_long(), 256) != jump_dest]
)
except UnsatError:
return True
return False
class ArbitraryJump(DetectionModule):
"""This module searches for JUMPs to a user-specified location."""
@ -35,12 +62,9 @@ class ArbitraryJump(DetectionModule):
:param state:
:return:
"""
if state.get_current_instruction()["address"] in self.cache:
return
self.issues.extend(self._analyze_state(state))
return self._analyze_state(state)
@staticmethod
def _analyze_state(state):
def _analyze_state(self, state):
"""
:param state:
@ -48,15 +72,20 @@ class ArbitraryJump(DetectionModule):
"""
jump_dest = state.mstate.stack[-1]
if jump_dest.symbolic is False:
return []
# Most probably the jump destination can have multiple locations in these circumstances
if is_unique_jumpdest(jump_dest, state) is True:
return []
try:
transaction_sequence = get_transaction_sequence(
state, state.world_state.constraints
)
except UnsatError:
return []
log.info("Detected arbitrary jump dest")
issue = Issue(
contract=state.environment.active_account.contract_name,
function_name=state.environment.active_function_name,
@ -72,6 +101,14 @@ class ArbitraryJump(DetectionModule):
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
transaction_sequence=transaction_sequence,
)
state.annotate(
IssueAnnotation(
conditions=[And(*state.world_state.constraints)],
issue=issue,
detector=self,
)
)
return [issue]

@ -40,8 +40,6 @@ class ArbitraryStorage(DetectionModule):
:param state:
:return:
"""
if state.get_current_instruction()["address"] in self.cache:
return
potential_issues = self._analyze_state(state)
annotation = get_potential_issues_annotation(state)

@ -14,7 +14,7 @@ from mythril.laser.ethereum.transaction.transaction_models import (
from mythril.analysis.module.base import DetectionModule, EntryPoint
from mythril.exceptions import UnsatError
from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.laser.smt import symbol_factory, UGT
from mythril.laser.smt import symbol_factory, UGT, Bool
log = logging.getLogger(__name__)
@ -34,8 +34,6 @@ class ArbitraryDelegateCall(DetectionModule):
:param state:
:return:
"""
if state.get_current_instruction()["address"] in self.cache:
return
potential_issues = self._analyze_state(state)
annotation = get_potential_issues_annotation(state)

@ -2,13 +2,14 @@
dependence."""
import logging
from copy import copy
from mythril.analysis.issue_annotation import IssueAnnotation
from mythril.analysis.module.base import DetectionModule, EntryPoint
from mythril.analysis.report import Issue
from mythril.exceptions import UnsatError
from mythril.analysis import solver
from mythril.analysis.swc_data import TX_ORIGIN_USAGE
from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.laser.smt import And
from typing import List
log = logging.getLogger(__name__)
@ -32,21 +33,15 @@ class TxOrigin(DetectionModule):
pre_hooks = ["JUMPI"]
post_hooks = ["ORIGIN"]
def _execute(self, state: GlobalState) -> None:
def _execute(self, state: GlobalState) -> List[Issue]:
"""
:param state:
:return:
"""
if state.get_current_instruction()["address"] in self.cache:
return
issues = self._analyze_state(state)
for issue in issues:
self.cache.add(issue.address)
self.issues.extend(issues)
@staticmethod
def _analyze_state(state: GlobalState) -> list:
return self._analyze_state(state)
def _analyze_state(self, state: GlobalState) -> List[Issue]:
"""
:param state:
@ -97,6 +92,11 @@ class TxOrigin(DetectionModule):
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
transaction_sequence=transaction_sequence,
)
state.annotate(
IssueAnnotation(
conditions=[And(*constraints)], issue=issue, detector=self
)
)
issues.append(issue)

@ -2,11 +2,12 @@
dependence."""
import logging
from mythril.analysis.issue_annotation import IssueAnnotation
from mythril.analysis.module.base import DetectionModule, EntryPoint
from mythril.analysis.report import Issue
from mythril.exceptions import UnsatError
from mythril.analysis import solver
from mythril.laser.smt import ULT, symbol_factory
from mythril.laser.smt import And, ULT, symbol_factory
from mythril.analysis.swc_data import TIMESTAMP_DEPENDENCE, WEAK_RANDOMNESS
from mythril.analysis.module.module_helpers import is_prehook
from mythril.laser.ethereum.state.global_state import GlobalState
@ -46,21 +47,15 @@ class PredictableVariables(DetectionModule):
pre_hooks = ["JUMPI", "BLOCKHASH"]
post_hooks = ["BLOCKHASH"] + predictable_ops
def _execute(self, state: GlobalState) -> None:
def _execute(self, state: GlobalState) -> List[Issue]:
"""
:param state:
:return:
"""
if state.get_current_instruction()["address"] in self.cache:
return
issues = self._analyze_state(state)
for issue in issues:
self.cache.add(issue.address)
self.issues.extend(issues)
@staticmethod
def _analyze_state(state: GlobalState) -> list:
return self._analyze_state(state)
def _analyze_state(self, state: GlobalState) -> List[Issue]:
"""
:param state:
@ -131,7 +126,13 @@ class PredictableVariables(DetectionModule):
),
transaction_sequence=transaction_sequence,
)
state.annotate(
IssueAnnotation(
conditions=[And(*constraints)],
issue=issue,
detector=self,
)
)
issues.append(issue)
elif opcode == "BLOCKHASH":
@ -142,7 +143,7 @@ class PredictableVariables(DetectionModule):
ULT(param, state.environment.block_number),
ULT(
state.environment.block_number,
symbol_factory.BitVecVal(2 ** 255, 256),
symbol_factory.BitVecVal(2**255, 256),
),
]

@ -46,8 +46,6 @@ class EtherThief(DetectionModule):
:param state:
:return:
"""
if state.get_current_instruction()["address"] in self.cache:
return
potential_issues = self._analyze_state(state)
annotation = get_potential_issues_annotation(state)

@ -1,15 +1,37 @@
"""This module contains the detection code for reachable exceptions."""
import logging
from typing import cast, List, Optional
from mythril.analysis import solver
from mythril.analysis.issue_annotation import IssueAnnotation
from mythril.analysis.module.base import DetectionModule, EntryPoint
from mythril.analysis.report import Issue
from mythril.analysis.swc_data import ASSERT_VIOLATION
from mythril.exceptions import UnsatError
from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.laser.ethereum.state.annotation import StateAnnotation
from mythril.laser.ethereum import util
from mythril.laser.smt import And
from mythril.support.support_utils import get_code_hash
log = logging.getLogger(__name__)
# The function signature of Panic(uint256)
PANIC_SIGNATURE = [78, 72, 123, 113]
class LastJumpAnnotation(StateAnnotation):
"""State Annotation used if an overflow is both possible and used in the annotated path"""
def __init__(self, last_jump: Optional[int] = None) -> None:
self.last_jump: int = last_jump
def __copy__(self):
new_annotation = LastJumpAnnotation(self.last_jump)
return new_annotation
class Exceptions(DetectionModule):
""""""
@ -18,33 +40,62 @@ class Exceptions(DetectionModule):
swc_id = ASSERT_VIOLATION
description = "Checks whether any exception states are reachable."
entry_point = EntryPoint.CALLBACK
pre_hooks = ["ASSERT_FAIL"]
pre_hooks = ["INVALID", "JUMP", "REVERT"]
def __init__(self):
super().__init__()
self.auto_cache = False
def _execute(self, state: GlobalState) -> None:
def _execute(self, state: GlobalState) -> List[Issue]:
"""
:param state:
:return:
"""
if state.get_current_instruction()["address"] in self.cache:
return
issues = self._analyze_state(state)
for issue in issues:
self.cache.add(issue.address)
self.issues.extend(issues)
self.cache.add((issue.source_location, issue.bytecode_hash))
return issues
@staticmethod
def _analyze_state(state) -> list:
def _analyze_state(self, state) -> List[Issue]:
"""
:param state:
:return:
"""
log.debug("ASSERT_FAIL in function " + state.environment.active_function_name)
opcode = state.get_current_instruction()["opcode"]
address = state.get_current_instruction()["address"]
try:
address = state.get_current_instruction()["address"]
annotations = cast(
List[LastJumpAnnotation],
[a for a in state.get_annotations(LastJumpAnnotation)],
)
if len(annotations) == 0:
state.annotate(LastJumpAnnotation())
annotations = cast(
List[LastJumpAnnotation],
[a for a in state.get_annotations(LastJumpAnnotation)],
)
if opcode == "JUMP":
annotations[0].last_jump = address
return []
if opcode == "REVERT" and not is_assertion_failure(state):
return []
cache_address = annotations[0].last_jump
if (
cache_address,
get_code_hash(state.environment.code.bytecode),
) in self.cache:
return []
log.debug(
"ASSERT_FAIL/REVERT in function " + state.environment.active_function_name
)
try:
description_tail = (
"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 "
@ -55,6 +106,7 @@ class Exceptions(DetectionModule):
transaction_sequence = solver.get_transaction_sequence(
state, state.world_state.constraints
)
issue = Issue(
contract=state.environment.active_account.contract_name,
function_name=state.environment.active_function_name,
@ -67,7 +119,16 @@ class Exceptions(DetectionModule):
bytecode=state.environment.code.bytecode,
transaction_sequence=transaction_sequence,
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
source_location=cache_address,
)
state.annotate(
IssueAnnotation(
conditions=[And(*state.world_state.constraints)],
issue=issue,
detector=self,
)
)
return [issue]
except UnsatError:
@ -76,4 +137,17 @@ class Exceptions(DetectionModule):
return []
def is_assertion_failure(global_state):
state = global_state.mstate
offset, length = state.stack[-1], state.stack[-2]
try:
return_data = state.memory[
util.get_concrete_int(offset) : util.get_concrete_int(offset + length)
]
except TypeError:
return False
return return_data[:4] == PANIC_SIGNATURE and return_data[-1] == 1
detector = Exceptions()

@ -59,6 +59,7 @@ class ExternalCalls(DetectionModule):
:param state:
:return:
"""
potential_issues = self._analyze_state(state)
annotation = get_potential_issues_annotation(state)

@ -4,6 +4,7 @@ underflows."""
from math import log2, ceil
from typing import cast, List, Set
from mythril.analysis import solver
from mythril.analysis.issue_annotation import IssueAnnotation
from mythril.analysis.report import Issue
from mythril.analysis.swc_data import INTEGER_OVERFLOW_AND_UNDERFLOW
from mythril.exceptions import UnsatError
@ -31,7 +32,7 @@ log = logging.getLogger(__name__)
class OverUnderflowAnnotation:
""" Symbol Annotation used if a BitVector can overflow"""
"""Symbol Annotation used if a BitVector can overflow"""
def __init__(
self, overflowing_state: GlobalState, operator: str, constraint: Bool
@ -46,7 +47,7 @@ class OverUnderflowAnnotation:
class OverUnderflowStateAnnotation(StateAnnotation):
""" State Annotation used if an overflow is both possible and used in the annotated path"""
"""State Annotation used if an overflow is both possible and used in the annotated path"""
def __init__(self) -> None:
self.overflowing_state_annotations = set() # type: Set[OverUnderflowAnnotation]
@ -102,18 +103,13 @@ class IntegerArithmetics(DetectionModule):
self._ostates_satisfiable = set()
self._ostates_unsatisfiable = set()
def _execute(self, state: GlobalState) -> None:
def _execute(self, state: GlobalState) -> List[Issue]:
"""Executes analysis module for integer underflow and integer overflow.
:param state: Statespace to analyse
:return: Found issues
"""
address = _get_address_from_state(state)
if address in self.cache:
return
opcode = state.get_current_instruction()["opcode"]
funcs = {
@ -127,8 +123,12 @@ class IntegerArithmetics(DetectionModule):
"STOP": [self._handle_transaction_end],
"EXP": [self._handle_exp],
}
results = []
for func in funcs[opcode]:
func(state)
result = func(state)
if result and len(result) > 0:
results += result
return results
def _get_args(self, state):
stack = state.mstate.stack
@ -161,25 +161,24 @@ class IntegerArithmetics(DetectionModule):
def _handle_exp(self, state):
op0, op1 = self._get_args(state)
if (op1.symbolic is False and op1.value == 0) or (
op0.symbolic is False and op0.value < 2
):
return
if op0.symbolic and op1.symbolic:
constraint = And(
op1 > symbol_factory.BitVecVal(256, 256),
op0 > symbol_factory.BitVecVal(1, 256),
)
elif op1.symbolic:
if op0.value < 2:
return
constraint = op1 >= symbol_factory.BitVecVal(
ceil(256 / log2(op0.value)), 256
)
elif op0.symbolic:
if op1.value == 0:
return
constraint = op0 >= symbol_factory.BitVecVal(
2 ** ceil(256 / op1.value), 256
)
else:
constraint = op0.value ** op1.value >= 2 ** 256
constraint = op1 >= symbol_factory.BitVecVal(
ceil(256 / log2(op0.value)), 256
)
annotation = OverUnderflowAnnotation(state, "exponentiation", constraint)
op0.annotate(annotation)
@ -208,7 +207,6 @@ class IntegerArithmetics(DetectionModule):
return
state_annotation = _get_overflowunderflow_state_annotation(state)
for annotation in value.annotations:
if isinstance(annotation, OverUnderflowAnnotation):
state_annotation.overflowing_state_annotations.add(annotation)
@ -259,10 +257,10 @@ class IntegerArithmetics(DetectionModule):
if isinstance(annotation, OverUnderflowAnnotation):
state_annotation.overflowing_state_annotations.add(annotation)
def _handle_transaction_end(self, state: GlobalState) -> None:
def _handle_transaction_end(self, state: GlobalState) -> List[Issue]:
state_annotation = _get_overflowunderflow_state_annotation(state)
issues = []
for annotation in state_annotation.overflowing_state_annotations:
ostate = annotation.overflowing_state
@ -319,10 +317,13 @@ class IntegerArithmetics(DetectionModule):
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
transaction_sequence=transaction_sequence,
)
address = _get_address_from_state(ostate)
self.cache.add(address)
self.issues.append(issue)
state.annotate(
IssueAnnotation(
issue=issue, detector=self, conditions=[And(*constraints)]
)
)
issues.append(issue)
return issues
detector = IntegerArithmetics()

@ -2,13 +2,14 @@
a single transaction."""
from copy import copy
from typing import cast, List
from mythril.analysis.issue_annotation import IssueAnnotation
from mythril.analysis.report import Issue
from mythril.analysis.solver import get_transaction_sequence, UnsatError
from mythril.analysis.swc_data import MULTIPLE_SENDS
from mythril.analysis.module.base import DetectionModule, EntryPoint
from mythril.laser.ethereum.state.annotation import StateAnnotation
from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.laser.smt import And
import logging
log = logging.getLogger(__name__)
@ -34,15 +35,9 @@ class MultipleSends(DetectionModule):
pre_hooks = ["CALL", "DELEGATECALL", "STATICCALL", "CALLCODE", "RETURN", "STOP"]
def _execute(self, state: GlobalState) -> None:
if state.get_current_instruction()["address"] in self.cache:
return
issues = self._analyze_state(state)
for issue in issues:
self.cache.add(issue.address)
self.issues.extend(issues)
@staticmethod
def _analyze_state(state: GlobalState):
return self._analyze_state(state)
def _analyze_state(self, state: GlobalState):
"""
:param state: the current state
:return: returns the issues for that corresponding state
@ -95,7 +90,13 @@ class MultipleSends(DetectionModule):
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
transaction_sequence=transaction_sequence,
)
state.annotate(
IssueAnnotation(
conditions=[And(*state.world_state.constraints)],
issue=issue,
detector=self,
)
)
return [issue]
return []

@ -111,8 +111,6 @@ class StateChangeAfterCall(DetectionModule):
pre_hooks = CALL_LIST + STATE_READ_WRITE_LIST
def _execute(self, state: GlobalState) -> None:
if state.get_current_instruction()["address"] in self.cache:
return
issues = self._analyze_state(state)
annotation = get_potential_issues_annotation(state)

@ -2,6 +2,7 @@ from mythril.analysis import solver
from mythril.analysis.report import Issue
from mythril.analysis.swc_data import UNPROTECTED_SELFDESTRUCT
from mythril.exceptions import UnsatError
from mythril.analysis.issue_annotation import IssueAnnotation
from mythril.analysis.module.base import DetectionModule, EntryPoint
from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.laser.ethereum.transaction.symbolic import ACTORS
@ -10,6 +11,7 @@ from mythril.laser.ethereum.transaction.transaction_models import (
ContractCreationTransaction,
)
import logging
from mythril.laser.ethereum.function_managers import keccak_function_manager
log = logging.getLogger(__name__)
@ -28,7 +30,7 @@ class AccidentallyKillable(DetectionModule):
swc_id = UNPROTECTED_SELFDESTRUCT
description = DESCRIPTION
entry_point = EntryPoint.CALLBACK
pre_hooks = ["SUICIDE"]
pre_hooks = ["SELFDESTRUCT"]
def __init__(self):
super().__init__()
@ -47,38 +49,34 @@ class AccidentallyKillable(DetectionModule):
:param state:
:return:
"""
if state.get_current_instruction()["address"] in self.cache:
return
issues = self._analyze_state(state)
for issue in issues:
self.cache.add(issue.address)
self.issues.extend(issues)
@staticmethod
def _analyze_state(state):
return self._analyze_state(state)
def _analyze_state(self, state):
log.info("Suicide module: Analyzing suicide instruction")
instruction = state.get_current_instruction()
to = state.mstate.stack[-1]
log.debug("SUICIDE in function %s", state.environment.active_function_name)
log.debug("SELFDESTRUCT in function %s", state.environment.active_function_name)
description_head = "Any sender can cause the contract to self-destruct."
constraints = []
attacker_constraints = []
for tx in state.world_state.transaction_sequence:
if not isinstance(tx, ContractCreationTransaction):
constraints.append(
attacker_constraints.append(
And(tx.caller == ACTORS.attacker, tx.caller == tx.origin)
)
try:
try:
transaction_sequence = solver.get_transaction_sequence(
state,
constraints = (
state.world_state.constraints
+ constraints
+ [to == ACTORS.attacker],
+ [to == ACTORS.attacker]
+ attacker_constraints
)
transaction_sequence = solver.get_transaction_sequence(
state, constraints
)
description_tail = (
@ -89,8 +87,9 @@ class AccidentallyKillable(DetectionModule):
)
except UnsatError:
constraints = state.world_state.constraints + attacker_constraints
transaction_sequence = solver.get_transaction_sequence(
state, state.world_state.constraints + constraints
state, constraints
)
description_tail = (
"Any sender can trigger execution of the SELFDESTRUCT instruction to destroy this "
@ -111,6 +110,12 @@ class AccidentallyKillable(DetectionModule):
transaction_sequence=transaction_sequence,
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
)
state.annotate(
IssueAnnotation(
conditions=[And(*constraints)], issue=issue, detector=self
)
)
return [issue]
except UnsatError:
log.debug("No model found")

@ -1,26 +1,33 @@
"""This module contains detection code to find occurrences of calls whose
return value remains unchecked."""
from copy import copy
from typing import cast, List, Union, Mapping
from typing import cast, List
from mythril.analysis import solver
from mythril.analysis.issue_annotation import IssueAnnotation
from mythril.analysis.report import Issue
from mythril.analysis.swc_data import UNCHECKED_RET_VAL
from mythril.analysis.module.base import DetectionModule, EntryPoint
from mythril.exceptions import UnsatError
from mythril.laser.smt import And
from mythril.laser.smt.bitvec import BitVec
from mythril.laser.ethereum.state.annotation import StateAnnotation
from mythril.laser.ethereum.state.global_state import GlobalState
import logging
from typing_extensions import TypedDict
log = logging.getLogger(__name__)
class RetVal(TypedDict):
address: int
retval: BitVec
class UncheckedRetvalAnnotation(StateAnnotation):
def __init__(self) -> None:
self.retvals = [] # type: List[Mapping[str, Union[int, BitVec]]]
self.retvals: List[RetVal] = []
def __copy__(self):
result = UncheckedRetvalAnnotation()
@ -46,18 +53,13 @@ class UncheckedRetval(DetectionModule):
pre_hooks = ["STOP", "RETURN"]
post_hooks = ["CALL", "DELEGATECALL", "STATICCALL", "CALLCODE"]
def _execute(self, state: GlobalState) -> None:
def _execute(self, state: GlobalState) -> List[Issue]:
"""
:param state:
:return:
"""
if state.get_current_instruction()["address"] in self.cache:
return
issues = self._analyze_state(state)
for issue in issues:
self.cache.add(issue.address)
self.issues.extend(issues)
return self._analyze_state(state)
def _analyze_state(self, state: GlobalState) -> list:
instruction = state.get_current_instruction()
@ -111,15 +113,27 @@ class UncheckedRetval(DetectionModule):
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
transaction_sequence=transaction_sequence,
)
conditions = [
And(*(state.world_state.constraints + [retval["retval"] == 1])),
And(*(state.world_state.constraints + [retval["retval"] == 1])),
]
state.annotate(
IssueAnnotation(conditions=conditions, issue=issue, detector=self)
)
issues.append(issue)
return issues
else:
log.debug("End of call, extracting retval")
assert state.environment.code.instruction_list[state.mstate.pc - 1][
if state.environment.code.instruction_list[state.mstate.pc - 1][
"opcode"
] in ["CALL", "DELEGATECALL", "STATICCALL", "CALLCODE"]
] not in ["CALL", "DELEGATECALL", "STATICCALL", "CALLCODE"]:
# Return is pointless with OOG. The pc does not get updated in such cases
return []
return_value = state.mstate.stack[-1]
retvals.append(
{"address": state.instruction["address"] - 1, "retval": return_value}

@ -2,11 +2,12 @@
calls."""
from mythril.analysis import solver
from mythril.analysis.issue_annotation import IssueAnnotation
from mythril.analysis.potential_issues import Issue
from mythril.analysis.swc_data import ASSERT_VIOLATION
from mythril.analysis.module.base import DetectionModule, EntryPoint
from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.laser.smt import Extract
from mythril.laser.smt import Extract, And
from mythril.exceptions import UnsatError
import logging
import eth_abi
@ -43,10 +44,7 @@ class UserAssertions(DetectionModule):
:return:
"""
issues = self._analyze_state(state)
for issue in issues:
self.cache.add(issue.address)
self.issues.extend(issues)
return self._analyze_state(state)
def _analyze_state(self, state: GlobalState):
"""
@ -87,8 +85,10 @@ class UserAssertions(DetectionModule):
)
if message:
description_tail = "A user-provided assertion failed with the message '{}'".format(
message
description_tail = (
"A user-provided assertion failed with the message '{}'".format(
message
)
)
else:
@ -111,6 +111,13 @@ class UserAssertions(DetectionModule):
transaction_sequence=transaction_sequence,
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
)
state.annotate(
IssueAnnotation(
detector=self,
issue=issue,
conditions=[And(*state.world_state.constraints)],
)
)
return [issue]
except UnsatError:

@ -2,18 +2,18 @@ from collections import defaultdict
from typing import List, Optional, Callable, Mapping, Dict
import logging
from mythril.support.opcodes import opcodes
from mythril.support.opcodes import OPCODES
from mythril.analysis.module.base import DetectionModule, EntryPoint
from mythril.analysis.module.loader import ModuleLoader
log = logging.getLogger(__name__)
OP_CODE_LIST = [c[0] for _, c in opcodes.items()]
OP_CODE_LIST = OPCODES.keys()
def get_detection_module_hooks(
modules: List[DetectionModule], hook_type="pre"
) -> Dict[str, List[Callable]]:
""" Gets a dictionary with the hooks for the passed detection modules
"""Gets a dictionary with the hooks for the passed detection modules
:param modules: The modules for which to retrieve hooks
:param hook_type: The type of hooks to retrieve (default: "pre")

@ -1,8 +1,11 @@
from mythril.analysis.report import Issue
from mythril.analysis.issue_annotation import IssueAnnotation
from mythril.analysis.solver import get_transaction_sequence
from mythril.exceptions import UnsatError
from mythril.laser.ethereum.state.annotation import StateAnnotation
from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.laser.smt import And
from mythril.support.support_args import args
class PotentialIssue:
@ -54,6 +57,10 @@ class PotentialIssuesAnnotation(StateAnnotation):
def __init__(self):
self.potential_issues = []
@property
def search_importance(self):
return 10 * len(self.potential_issues)
def get_potential_issues_annotation(state: GlobalState) -> PotentialIssuesAnnotation:
"""
@ -81,28 +88,39 @@ def check_potential_issues(state: GlobalState) -> None:
:return:
"""
annotation = get_potential_issues_annotation(state)
unsat_potential_issues = []
for potential_issue in annotation.potential_issues:
try:
transaction_sequence = get_transaction_sequence(
state, state.world_state.constraints + potential_issue.constraints
)
except UnsatError:
unsat_potential_issues.append(potential_issue)
continue
annotation.potential_issues.remove(potential_issue)
potential_issue.detector.cache.add(potential_issue.address)
potential_issue.detector.issues.append(
Issue(
contract=potential_issue.contract,
function_name=potential_issue.function_name,
address=potential_issue.address,
title=potential_issue.title,
bytecode=potential_issue.bytecode,
swc_id=potential_issue.swc_id,
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
severity=potential_issue.severity,
description_head=potential_issue.description_head,
description_tail=potential_issue.description_tail,
transaction_sequence=transaction_sequence,
issue = Issue(
contract=potential_issue.contract,
function_name=potential_issue.function_name,
address=potential_issue.address,
title=potential_issue.title,
bytecode=potential_issue.bytecode,
swc_id=potential_issue.swc_id,
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
severity=potential_issue.severity,
description_head=potential_issue.description_head,
description_tail=potential_issue.description_tail,
transaction_sequence=transaction_sequence,
)
state.annotate(
IssueAnnotation(
detector=potential_issue.detector,
issue=issue,
conditions=[
And(*(state.world_state.constraints + potential_issue.constraints))
],
)
)
if args.use_issue_annotations is False:
potential_issue.detector.issues.append(issue)
potential_issue.detector.update_cache([issue])
annotation.potential_issues = unsat_potential_issues

@ -1,7 +1,9 @@
"""This module provides classes that make up an issue report."""
import logging
import re
import json
import operator
from eth_abi import decode_abi
from jinja2 import PackageLoader, Environment
from typing import Dict, List, Any, Optional
import hashlib
@ -23,17 +25,18 @@ class Issue:
def __init__(
self,
contract,
function_name,
address,
swc_id,
title,
bytecode,
contract: str,
function_name: str,
address: int,
swc_id: str,
title: str,
bytecode: str,
gas_used=(None, None),
severity=None,
description_head="",
description_tail="",
transaction_sequence=None,
source_location=None,
):
"""
@ -66,15 +69,16 @@ class Issue:
self.discovery_time = time() - StartTime().global_start_time
self.bytecode_hash = get_code_hash(bytecode)
self.transaction_sequence = transaction_sequence
self.source_location = source_location
@property
def transaction_sequence_users(self):
""" Returns the transaction sequence without pre-generated block data"""
"""Returns the transaction sequence without pre-generated block data"""
return self.transaction_sequence
@property
def transaction_sequence_jsonv2(self):
""" Returns the transaction sequence as a json string with pre-generated block data"""
"""Returns the transaction sequence as a json string with pre-generated block data"""
return (
self.add_block_data(self.transaction_sequence)
if self.transaction_sequence
@ -83,7 +87,7 @@ class Issue:
@staticmethod
def add_block_data(transaction_sequence: Dict):
""" Adds sane block data to a transaction_sequence """
"""Adds sane block data to a transaction_sequence"""
for step in transaction_sequence["steps"]:
step["gasLimit"] = "0x7d000"
step["gasPrice"] = "0x773594000"
@ -141,9 +145,22 @@ class Issue:
:param contract:
"""
if self.address and isinstance(contract, SolidityContract):
codeinfo = contract.get_source_info(
self.address, constructor=(self.function == "constructor")
)
is_constructor = False
if (
contract.creation_code
in self.transaction_sequence["steps"][-1]["input"]
and self.function == "constructor"
):
is_constructor = True
if self.source_location:
codeinfo = contract.get_source_info(
self.source_location, constructor=is_constructor
)
else:
codeinfo = contract.get_source_info(
self.address, constructor=is_constructor
)
if codeinfo is None:
self.source_mapping = self.address
@ -160,7 +177,7 @@ class Issue:
self.source_mapping = self.address
def resolve_function_names(self):
""" Resolves function names for each step """
"""Resolves function names for each step"""
if (
self.transaction_sequence is None
@ -175,14 +192,37 @@ class Issue:
try:
sig = signatures.get(_hash)
# TODO: Check other mythx tools for dependency before supporting multiple possible function names
if len(sig) > 0:
step["name"] = sig[0]
step["resolved_input"] = Issue.resolve_input(
step["calldata"], sig[0]
)
else:
step["name"] = "unknown"
except ValueError:
step["name"] = "unknown"
@staticmethod
def resolve_input(data, function_name):
"""
Adds decoded calldate to the tx sequence.
"""
data = data[10:]
# Eliminates the first and last brackets
# Since signature such as func((bytes32,bytes32,uint8)[],(address[],uint32)) are valid
type_info = function_name[function_name.find("(") + 1 : -1]
type_info = re.split(r",\s*(?![^()]*\))", type_info)
if len(data) % 64 > 0:
data += "0" * (64 - len(data) % 64)
try:
decoded_output = decode_abi(type_info, bytes.fromhex(data))
return decoded_output
except Exception as e:
return None
class Report:
"""A report containing the content of multiple issues."""
@ -224,7 +264,11 @@ class Report:
:param issue:
"""
m = hashlib.md5()
m.update((issue.contract + str(issue.address) + issue.title).encode("utf-8"))
m.update(
(issue.contract + issue.function + str(issue.address) + issue.title).encode(
"utf-8"
)
)
issue.resolve_function_names()
self.issues[m.digest()] = issue
@ -262,14 +306,14 @@ class Report:
# Setup issues
_issues = []
for key, issue in self.issues.items():
for _, issue in self.issues.items():
idx = self.source.get_source_index(issue.bytecode_hash)
try:
title = SWC_TO_TITLE[issue.swc_id]
except KeyError:
title = "Unspecified Security Issue"
extra = {"discoveryTime": int(issue.discovery_time * 10 ** 9)}
extra = {"discoveryTime": int(issue.discovery_time * 10**9)}
if issue.transaction_sequence_jsonv2:
extra["testCases"] = [issue.transaction_sequence_jsonv2]
@ -294,7 +338,7 @@ class Report:
# Add execution info to meta
analysis_duration = int(
round((time() - StartTime().global_start_time) * (10 ** 9))
round((time() - StartTime().global_start_time) * (10**9))
)
meta_data["mythril_execution_info"] = {"analysis_duration": analysis_duration}
for execution_info in self.execution_info:

@ -1,7 +1,6 @@
"""This module contains functionality for hooking in detection modules and
executing them."""
from mythril.support.opcodes import opcodes
from mythril.analysis.module import ModuleLoader, reset_callback_modules
from mythril.analysis.module.base import EntryPoint
from mythril.analysis.report import Issue
@ -13,7 +12,7 @@ log = logging.getLogger(__name__)
def retrieve_callback_issues(white_list: Optional[List[str]] = None) -> List[Issue]:
""" Get the issues discovered by callback type detection modules"""
"""Get the issues discovered by callback type detection modules"""
issues = [] # type: List[Issue]
for module in ModuleLoader().get_detection_modules(
entry_point=EntryPoint.CALLBACK, white_list=white_list
@ -27,7 +26,7 @@ def retrieve_callback_issues(white_list: Optional[List[str]] = None) -> List[Iss
def fire_lasers(statespace, white_list: Optional[List[str]] = None) -> List[Issue]:
""" Fire lasers at analysed statespace object
"""Fire lasers at analysed statespace object
:param statespace: Symbolic statespace to analyze
:param white_list: Optionally whitelist modules to use for the analysis

@ -1,13 +1,14 @@
"""This module contains analysis module helpers to solve path constraints."""
import logging
from typing import Dict, List, Tuple, Union
from typing import Dict, List, Tuple, Union, Any
import z3
import logging
from z3 import FuncInterp
from mythril.exceptions import UnsatError
from mythril.laser.ethereum.function_managers import (
exponent_function_manager,
keccak_function_manager,
)
@ -21,10 +22,13 @@ from mythril.laser.smt import UGE, symbol_factory
from mythril.support.model import get_model
log = logging.getLogger(__name__)
z3.set_option(
max_args=10000000, max_lines=1000000, max_depth=10000000, max_visited=1000000
)
def pretty_print_model(model):
""" Pretty prints a z3 model
"""Pretty prints a z3 model
:param model:
:return:
@ -49,34 +53,37 @@ def pretty_print_model(model):
def get_transaction_sequence(
global_state: GlobalState, constraints: Constraints
) -> Dict:
) -> Dict[str, Any]:
"""Generate concrete transaction sequence.
Note: This function only considers the constraints in constraint argument,
which in some cases is expected to differ from global_state's constraints
:param global_state: GlobalState to generate transaction sequence for
:param constraints: list of constraints used to generate transaction sequence
"""
transaction_sequence = global_state.world_state.transaction_sequence
concrete_transactions = []
tx_constraints, minimize = _set_minimisation_constraints(
transaction_sequence, constraints.copy(), [], 5000, global_state.world_state
)
try:
model = get_model(tx_constraints, minimize=minimize)
except UnsatError:
raise UnsatError
# Include creation account in initial state
# Note: This contains the code, which should not exist until after the first tx
initial_world_state = transaction_sequence[0].world_state
if isinstance(transaction_sequence[0], ContractCreationTransaction):
initial_world_state = transaction_sequence[0].prev_world_state
else:
initial_world_state = transaction_sequence[0].world_state
initial_accounts = initial_world_state.accounts
for transaction in transaction_sequence:
concrete_transaction = _get_concrete_transaction(model, transaction)
concrete_transactions.append(concrete_transaction)
min_price_dict = {} # type: Dict[str, int]
min_price_dict: Dict[str, int] = {}
for address in initial_accounts.keys():
min_price_dict[address] = model.eval(
initial_world_state.starting_balances[
@ -111,7 +118,11 @@ def _add_calldata_placeholder(
tx["calldata"] = tx["input"]
if not isinstance(transaction_sequence[0], ContractCreationTransaction):
return
code_len = len(transaction_sequence[0].code.bytecode)
if type(transaction_sequence[0].code.bytecode) == tuple:
code_len = len(transaction_sequence[0].code.bytecode) * 2
else:
code_len = len(transaction_sequence[0].code.bytecode)
concrete_transactions[0]["calldata"] = concrete_transactions[0]["input"][
code_len + 2 :
]
@ -156,15 +167,17 @@ def _replace_with_actual_sha(
)
def _get_concrete_state(initial_accounts: Dict, min_price_dict: Dict[str, int]):
""" Gets a concrete state """
def _get_concrete_state(
initial_accounts: Dict, min_price_dict: Dict[str, int]
) -> Dict[str, Dict]:
"""Gets a concrete state"""
accounts = {}
for address, account in initial_accounts.items():
# Skip empty default account
data = dict() # type: Dict[str, Union[int, str]]
data: Dict[str, Union[int, str]] = {}
data["nonce"] = account.nonce
data["code"] = account.code.bytecode
data["code"] = account.serialised_code()
data["storage"] = str(account.storage)
data["balance"] = hex(min_price_dict.get(address, 0))
accounts[hex(address)] = data
@ -172,7 +185,7 @@ def _get_concrete_state(initial_accounts: Dict, min_price_dict: Dict[str, int]):
def _get_concrete_transaction(model: z3.Model, transaction: BaseTransaction):
""" Gets a concrete transaction from a transaction and z3 model"""
"""Gets a concrete transaction from a transaction and z3 model"""
# Get concrete values from transaction
address = hex(transaction.callee_account.address.value)
value = model.eval(transaction.call_value.raw, model_completion=True).as_long()
@ -206,7 +219,7 @@ def _get_concrete_transaction(model: z3.Model, transaction: BaseTransaction):
def _set_minimisation_constraints(
transaction_sequence, constraints, minimize, max_size, world_state
) -> Tuple[Constraints, tuple]:
""" Set constraints that minimise key transaction values
"""Set constraints that minimise key transaction values
Constraints generated:
- Upper bound on calldata size

@ -13,7 +13,7 @@ from mythril.laser.ethereum.strategy.basic import (
ReturnWeightedRandomStrategy,
BasicSearchStrategy,
)
from mythril.laser.ethereum.strategy.beam import BeamSearch
from mythril.laser.ethereum.natives import PRECOMPILE_COUNT
from mythril.laser.ethereum.transaction.symbolic import ACTORS
@ -82,7 +82,7 @@ class SymExecWrapper:
address = symbol_factory.BitVecVal(int(address, 16), 256)
if isinstance(address, int):
address = symbol_factory.BitVecVal(address, 256)
beam_width = None
if strategy == "dfs":
s_strategy = DepthFirstSearchStrategy # type: Type[BasicSearchStrategy]
elif strategy == "bfs":
@ -91,6 +91,9 @@ class SymExecWrapper:
s_strategy = ReturnRandomNaivelyStrategy
elif strategy == "weighted-random":
s_strategy = ReturnWeightedRandomStrategy
elif "beam-search: " in strategy:
beam_width = int(strategy.split("beam-search: ")[1])
s_strategy = BeamSearch
else:
raise ValueError("Invalid strategy argument supplied")
@ -121,10 +124,13 @@ class SymExecWrapper:
create_timeout=create_timeout,
transaction_count=transaction_count,
requires_statespace=requires_statespace,
beam_width=beam_width,
)
if loop_bound is not None:
self.laser.extend_strategy(BoundedLoopsStrategy, loop_bound)
self.laser.extend_strategy(
BoundedLoopsStrategy, loop_bound=loop_bound, beam_width=beam_width
)
plugin_loader = LaserPluginLoader()
plugin_loader.load(CoveragePluginBuilder())
@ -159,7 +165,7 @@ class SymExecWrapper:
),
)
if isinstance(contract, SolidityContract):
if isinstance(contract, SolidityContract) and create_timeout != 0:
self.laser.sym_exec(
creation_code=contract.creation_code,
contract_name=contract.name,
@ -172,7 +178,6 @@ class SymExecWrapper:
world_state=world_state,
)
else:
account = Account(
address,
contract.disassembly,
@ -182,7 +187,7 @@ class SymExecWrapper:
concrete_storage=True
if (dynloader is not None and dynloader.active)
else False,
)
) # concrete_storage can get overridden by global args
if dynloader is not None:
if isinstance(address, int):
@ -239,7 +244,7 @@ class SymExecWrapper:
stack = state.mstate.stack
if op in ("CALL", "CALLCODE"):
gas, to, value, meminstart, meminsz, memoutstart, memoutsz = (
gas, to, value, meminstart, meminsz, _, _ = (
get_variable(stack[-1]),
get_variable(stack[-2]),
get_variable(stack[-3]),
@ -287,7 +292,7 @@ class SymExecWrapper:
)
)
else:
gas, to, meminstart, meminsz, memoutstart, memoutsz = (
gas, to, meminstart, meminsz, _, _ = (
get_variable(stack[-1]),
get_variable(stack[-2]),
get_variable(stack[-3]),

@ -0,0 +1,2 @@
from mythril.concolic.concolic_execution import concolic_execution
from mythril.concolic.find_trace import concrete_execution

@ -0,0 +1,85 @@
import json
import binascii
from datetime import datetime, timedelta
from typing import Dict, List, Any
from copy import deepcopy
from mythril.concolic.concrete_data import ConcreteData
from mythril.concolic.find_trace import concrete_execution
from mythril.disassembler.disassembly import Disassembly
from mythril.laser.ethereum.strategy.concolic import ConcolicStrategy
from mythril.laser.ethereum.svm import LaserEVM
from mythril.laser.ethereum.state.world_state import WorldState
from mythril.laser.ethereum.state.account import Account
from mythril.laser.ethereum.transaction.symbolic import execute_transaction
from mythril.laser.ethereum.transaction.transaction_models import tx_id_manager
from mythril.laser.smt import Expression, BitVec, symbol_factory
from mythril.laser.ethereum.time_handler import time_handler
from mythril.support.support_args import args
def flip_branches(
init_state: WorldState,
concrete_data: ConcreteData,
jump_addresses: List[str],
trace: List,
) -> List[Dict[str, Dict[str, Any]]]:
"""
Flips branches and prints the input required for branch flip
:param concrete_data: Concrete data
:param jump_addresses: Jump addresses to flip
:param trace: trace to follow
"""
tx_id_manager.restart_counter()
output_list = []
laser_evm = LaserEVM(
execution_timeout=600, use_reachability_check=False, transaction_count=10
)
laser_evm.open_states = [deepcopy(init_state)]
laser_evm.strategy = ConcolicStrategy(
work_list=laser_evm.work_list,
max_depth=100,
trace=trace,
flip_branch_addresses=jump_addresses,
)
time_handler.start_execution(laser_evm.execution_timeout)
laser_evm.time = datetime.now()
for transaction in concrete_data["steps"]:
execute_transaction(
laser_evm,
callee_address=transaction["address"],
caller_address=symbol_factory.BitVecVal(
int(transaction["origin"], 16), 256
),
data=transaction["input"][2:],
)
if laser_evm.strategy.results:
for addr in jump_addresses:
output_list.append(laser_evm.strategy.results[addr])
return output_list
def concolic_execution(
concrete_data: ConcreteData, jump_addresses: List, solver_timeout=100000
) -> List[Dict[str, Dict[str, Any]]]:
"""
Executes codes and prints input required to cover the branch flips
:param input_file: Input file
:param jump_addresses: Jump addresses to flip
:param solver_timeout: Solver timeout
"""
init_state, trace = concrete_execution(concrete_data)
args.solver_timeout = solver_timeout
output_list = flip_branches(
init_state=init_state,
concrete_data=concrete_data,
jump_addresses=jump_addresses,
trace=trace,
)
return output_list

@ -0,0 +1,34 @@
from typing import Dict, List
from typing_extensions import TypedDict
class AccountData(TypedDict):
balance: str
code: str
nonce: int
storage: dict
class InitialState(TypedDict):
accounts: Dict[str, AccountData]
class TransactionData(TypedDict):
address: str
blockCoinbase: str
blockDifficulty: str
blockGasLimit: str
blockNumber: str
blockTime: str
calldata: str
gasLimit: str
gasPrice: str
input: str
name: str
origin: str
value: str
class ConcreteData(TypedDict):
initialState: InitialState
steps: List[TransactionData]

@ -0,0 +1,78 @@
import json
import binascii
from copy import deepcopy
from datetime import datetime
from typing import Dict, List, Tuple
from mythril.concolic.concrete_data import ConcreteData
from mythril.disassembler.disassembly import Disassembly
from mythril.laser.ethereum.svm import LaserEVM
from mythril.laser.ethereum.state.world_state import WorldState
from mythril.laser.ethereum.state.account import Account
from mythril.laser.ethereum.transaction.concolic import execute_transaction
from mythril.laser.plugin.loader import LaserPluginLoader
from mythril.laser.smt import Expression, BitVec, symbol_factory
from mythril.laser.ethereum.transaction.transaction_models import tx_id_manager
from mythril.plugin.discovery import PluginDiscovery
def setup_concrete_initial_state(concrete_data: ConcreteData) -> WorldState:
"""
Sets up concrete initial state
:param concrete_data: Concrete data
:return: initialised world state
"""
world_state = WorldState()
for address, details in concrete_data["initialState"]["accounts"].items():
account = Account(address, concrete_storage=True)
account.code = Disassembly(details["code"][2:])
account.nonce = details["nonce"]
if type(details["storage"]) == str:
details["storage"] = eval(details["storage"]) # type: ignore
for key, value in details["storage"].items():
key_bitvec = symbol_factory.BitVecVal(int(key, 16), 256)
account.storage[key_bitvec] = symbol_factory.BitVecVal(int(value, 16), 256)
world_state.put_account(account)
account.set_balance(int(details["balance"], 16))
return world_state
def concrete_execution(concrete_data: ConcreteData) -> Tuple[WorldState, List]:
"""
Executes code concretely to find the path to be followed by concolic executor
:param concrete_data: Concrete data
:return: path trace
"""
tx_id_manager.restart_counter()
init_state = setup_concrete_initial_state(concrete_data)
laser_evm = LaserEVM(execution_timeout=1000)
laser_evm.open_states = [deepcopy(init_state)]
plugin_loader = LaserPluginLoader()
assert PluginDiscovery().is_installed("myth_concolic_execution")
trace_plugin = PluginDiscovery().installed_plugins["myth_concolic_execution"]()
plugin_loader.load(trace_plugin)
laser_evm.time = datetime.now()
plugin_loader.instrument_virtual_machine(laser_evm, None)
for transaction in concrete_data["steps"]:
execute_transaction(
laser_evm,
callee_address=transaction["address"],
caller_address=symbol_factory.BitVecVal(
int(transaction["origin"], 16), 256
),
origin_address=symbol_factory.BitVecVal(
int(transaction["origin"], 16), 256
),
gas_limit=int(transaction.get("gasLimit", "0x9999999999999999999999"), 16),
data=binascii.a2b_hex(transaction["input"][2:]),
gas_price=int(transaction.get("gasPrice", "0x773594000"), 16),
value=int(transaction["value"], 16),
track_gas=False,
)
tx_id_manager.restart_counter()
return init_state, plugin_loader.plugin_list["MythX Trace Finder"].tx_trace # type: ignore

@ -2,14 +2,18 @@
code disassembly."""
import re
from collections import Generator
from mythril.support.opcodes import opcodes
try:
from collections.abc import Generator
except ImportError:
from collections import Generator
regex_PUSH = re.compile(r"^PUSH(\d*)$")
from functools import lru_cache
from mythril.ethereum import util
from mythril.support.opcodes import OPCODES, ADDRESS, ADDRESS_OPCODE_MAPPING
# Additional mnemonic to catch failed assertions
opcodes[254] = ("ASSERT_FAIL", 0, 0, 0)
regex_PUSH = re.compile(r"^PUSH(\d*)$")
class EvmInstruction:
@ -54,9 +58,8 @@ def get_opcode_from_name(operation_name: str) -> int:
:param operation_name:
:return:
"""
for op_code, value in opcodes.items():
if operation_name == value[0]:
return op_code
if operation_name in OPCODES:
return OPCODES[operation_name][ADDRESS]
raise RuntimeError("Unknown opcode")
@ -90,7 +93,10 @@ def is_sequence_match(pattern: list, instruction_list: list, index: int) -> bool
return True
def disassemble(bytecode: bytes) -> list:
lru_cache(maxsize=2**10)
def disassemble(bytecode) -> list:
"""Disassembles evm bytecode and returns a list of instructions.
:param bytecode:
@ -99,25 +105,40 @@ def disassemble(bytecode: bytes) -> list:
instruction_list = []
address = 0
length = len(bytecode)
if "bzzr" in str(bytecode[-43:]):
# ignore swarm hash
length -= 43
if type(bytecode) == str:
bytecode = util.safe_decode(bytecode)
length = len(bytecode)
part_code = bytecode[-43:]
else:
try:
part_code = bytes(bytecode[-43:])
except TypeError:
part_code = ""
try:
if "bzzr" in str(part_code):
# ignore swarm hash
length -= 43
except ValueError:
pass
while address < length:
try:
op_code = opcodes[bytecode[address]]
op_code = ADDRESS_OPCODE_MAPPING[bytecode[address]]
except KeyError:
instruction_list.append(EvmInstruction(address, "INVALID"))
address += 1
continue
op_code_name = op_code[0]
current_instruction = EvmInstruction(address, op_code_name)
current_instruction = EvmInstruction(address, op_code)
match = re.search(regex_PUSH, op_code_name)
match = re.search(regex_PUSH, op_code)
if match:
argument_bytes = bytecode[address + 1 : address + 1 + int(match.group(1))]
current_instruction.argument = "0x" + argument_bytes.hex()
if type(argument_bytes) == bytes:
current_instruction.argument = "0x" + argument_bytes.hex()
else:
current_instruction.argument = argument_bytes
address += int(match.group(1))
instruction_list.append(current_instruction)

@ -23,8 +23,10 @@ class Disassembly(object):
:param enable_online_lookup:
"""
self.bytecode = code
self.instruction_list = asm.disassemble(util.safe_decode(code))
if type(code) == str:
self.instruction_list = asm.disassemble(util.safe_decode(code))
else:
self.instruction_list = asm.disassemble(code)
self.func_hashes = [] # type: List[str]
self.function_name_to_address = {} # type: Dict[str, int]
self.address_to_function_name = {} # type: Dict[int, str]
@ -36,7 +38,7 @@ class Disassembly(object):
# open from default locations
# control if you want to have online signature hash lookups
signatures = SignatureDB(enable_online_lookup=self.enable_online_lookup)
self.instruction_list = asm.disassemble(util.safe_decode(bytecode))
self.instruction_list = asm.disassemble(bytecode)
# Need to take from PUSH1 to PUSH4 because solc seems to remove excess 0s at the beginning for optimizing
jump_table_indices = asm.find_op_code_sequence(
[("PUSH1", "PUSH2", "PUSH3", "PUSH4"), ("EQ",)], self.instruction_list
@ -82,16 +84,29 @@ def get_function_info(
"""
# Append with missing 0s at the beginning
function_hash = "0x" + instruction_list[index]["argument"][2:].rjust(8, "0")
if type(instruction_list[index]["argument"]) == tuple:
try:
function_hash = "0x" + bytes(
instruction_list[index]["argument"]
).hex().rjust(8, "0")
except AttributeError:
raise ValueError(
"Mythril currently does not support symbolic function signatures"
)
else:
function_hash = "0x" + instruction_list[index]["argument"][2:].rjust(8, "0")
function_names = signature_database.get(function_hash)
if len(function_names) > 0:
function_name = function_names[0]
function_name = " or ".join(set(function_names))
else:
function_name = "_function_" + function_hash
try:
offset = instruction_list[index + 2]["argument"]
if type(offset) == tuple:
offset = bytes(offset).hex()
entry_point = int(offset, 16)
except (KeyError, IndexError):
return function_hash, None, None

@ -4,7 +4,7 @@ import re
import logging
import persistent
from ethereum import utils
from mythril.support.support_utils import sha3
from mythril.disassembler.disassembly import Disassembly
from mythril.support.support_utils import get_code_hash
@ -31,11 +31,11 @@ class EVMContract(persistent.Persistent):
"""
creation_code = re.sub(r"(_{2}.{38})", "aa" * 20, creation_code)
code = re.sub(r"(_{2}.{38})", "aa" * 20, code)
self.creation_code = creation_code
self.name = name
self.code = code
self.disassembly = Disassembly(code, enable_online_lookup=enable_online_lookup)
self.creation_disassembly = Disassembly(
creation_code, enable_online_lookup=enable_online_lookup
)
@ -113,8 +113,7 @@ class EVMContract(persistent.Persistent):
if m:
sign_hash = "0x" + utils.sha3(m.group(1))[:4].hex()
sign_hash = "0x" + sha3(m.group(1))[:4].hex()
str_eval += '"' + sign_hash + '" in self.disassembly.func_hashes'
return eval(str_eval.strip())

@ -1,177 +0,0 @@
"""This module contains account indexing functionality.
This includes a sedes class for lists, account storage receipts for
LevelDB and a class for updating account addresses.
"""
import logging
import time
import rlp
from ethereum import utils
from ethereum.messages import Log
from ethereum.utils import address, hash32, int256
from rlp.sedes import big_endian_int, binary
from mythril import ethereum
from mythril.exceptions import AddressNotFoundError
log = logging.getLogger(__name__)
BATCH_SIZE = 8 * 4096
class CountableList(object):
"""A sedes for lists of arbitrary length.
:param element_sedes: when (de-)serializing a list, this sedes will be applied to all of its elements
"""
def __init__(self, element_sedes):
self.element_sedes = element_sedes
def serialize(self, obj):
"""
:param obj:
:return:
"""
return [self.element_sedes.serialize(e) for e in obj]
def deserialize(self, serial):
"""
:param serial:
:return:
"""
# needed for 2 reasons:
# 1. empty lists are not zero elements
# 2. underlying logs are stored as list - if empty will also except and receipts will be lost
try:
return [self.element_sedes.deserialize(e) for e in serial]
except:
return []
class ReceiptForStorage(rlp.Serializable):
"""Receipt format stored in levelDB."""
fields = [
("state_root", binary),
("cumulative_gas_used", big_endian_int),
("bloom", int256),
("tx_hash", hash32),
("contractAddress", address),
("logs", CountableList(Log)),
("gas_used", big_endian_int),
]
class AccountIndexer(object):
"""Updates address index."""
def __init__(self, ethDB):
self.db = ethDB
self.lastBlock = None
self.lastProcessedBlock = None
self.updateIfNeeded()
def get_contract_by_hash(self, contract_hash):
"""get mapped contract_address by its hash, if not found try
indexing."""
contract_address = self.db.reader._get_address_by_hash(contract_hash)
if contract_address is not None:
return contract_address
else:
raise AddressNotFoundError
def _process(self, startblock):
"""Processesing method."""
log.debug("Processing blocks %d to %d" % (startblock, startblock + BATCH_SIZE))
addresses = []
for blockNum in range(startblock, startblock + BATCH_SIZE):
block_hash = self.db.reader._get_block_hash(blockNum)
if block_hash is not None:
receipts = self.db.reader._get_block_receipts(block_hash, blockNum)
for receipt in receipts:
if receipt.contractAddress is not None and not all(
b == 0 for b in receipt.contractAddress
):
addresses.append(receipt.contractAddress)
else:
if len(addresses) == 0:
raise Exception()
return addresses
def updateIfNeeded(self):
"""update address index."""
headBlock = self.db.reader._get_head_block()
if headBlock is not None:
# avoid restarting search if head block is same & we already initialized
# this is required for fastSync handling
if self.lastBlock is not None:
self.lastBlock = max(self.lastBlock, headBlock.number)
else:
self.lastBlock = headBlock.number
lastProcessed = self.db.reader._get_last_indexed_number()
if lastProcessed is not None:
self.lastProcessedBlock = utils.big_endian_to_int(lastProcessed)
# in fast sync head block is at 0 (e.g. in fastSync), we can't use it to determine length
if self.lastBlock is not None and self.lastBlock == 0:
self.lastBlock = 2e9
if self.lastBlock is None or (
self.lastProcessedBlock is not None
and self.lastBlock <= self.lastProcessedBlock
):
return
blockNum = 0
if self.lastProcessedBlock is not None:
blockNum = self.lastProcessedBlock + 1
print(
"Updating hash-to-address index from block "
+ str(self.lastProcessedBlock)
)
else:
print("Starting hash-to-address index")
count = 0
processed = 0
while blockNum <= self.lastBlock:
# leveldb cannot be accessed on multiple processes (not even readonly)
# multithread version performs significantly worse than serial
try:
results = self._process(blockNum)
except:
break
# store new mappings
self.db.writer._start_writing()
count += len(results)
for addr in results:
self.db.writer._store_account_address(addr)
self.db.writer._commit_batch()
processed += BATCH_SIZE
blockNum = min(blockNum + BATCH_SIZE, self.lastBlock + 1)
cost_time = time.time() - ethereum.start_time
print(
"%d blocks processed (in %d seconds), %d unique addresses found, next block: %d"
% (processed, cost_time, count, min(self.lastBlock, blockNum))
)
self.lastProcessedBlock = blockNum - 1
self.db.writer._set_last_indexed_number(self.lastProcessedBlock)
print("Finished indexing")
self.lastBlock = self.lastProcessedBlock

@ -1,314 +0,0 @@
"""This module contains a LevelDB client."""
import binascii
import rlp
from mythril.ethereum.interface.leveldb.accountindexing import CountableList
from mythril.ethereum.interface.leveldb.accountindexing import (
ReceiptForStorage,
AccountIndexer,
)
import logging
from ethereum import utils
from ethereum.block import BlockHeader, Block
from mythril.ethereum.interface.leveldb.state import State
from mythril.ethereum.interface.leveldb.eth_db import ETH_DB
from mythril.ethereum.evmcontract import EVMContract
from mythril.exceptions import AddressNotFoundError
log = logging.getLogger(__name__)
# Per https://github.com/ethereum/go-ethereum/blob/master/core/rawdb/schema.go
# prefixes and suffixes for keys in geth
header_prefix = b"h" # header_prefix + num (uint64 big endian) + hash -> header
body_prefix = b"b" # body_prefix + num (uint64 big endian) + hash -> block body
num_suffix = b"n" # header_prefix + num (uint64 big endian) + num_suffix -> hash
block_hash_prefix = b"H" # block_hash_prefix + hash -> num (uint64 big endian)
block_receipts_prefix = (
b"r" # block_receipts_prefix + num (uint64 big endian) + hash -> block receipts
)
# known geth keys
head_header_key = b"LastBlock" # head (latest) header hash
# custom prefixes
address_prefix = b"AM" # address_prefix + hash -> address
# custom keys
address_mapping_head_key = b"accountMapping" # head (latest) number of indexed block
def _format_block_number(number):
"""Format block number to uint64 big endian."""
return utils.zpad(utils.int_to_big_endian(number), 8)
def _encode_hex(v):
"""Encode a hash string as hex."""
return "0x" + utils.encode_hex(v)
class LevelDBReader(object):
"""LevelDB reading interface, can be used with snapshot."""
def __init__(self, db):
"""
:param db:
"""
self.db = db
self.head_block_header = None
self.head_state = None
def _get_head_state(self):
"""Get head state.
:return:
"""
if not self.head_state:
root = self._get_head_block().state_root
self.head_state = State(self.db, root)
return self.head_state
def _get_account(self, address):
"""Get account by address.
:param address:
:return:
"""
state = self._get_head_state()
account_address = binascii.a2b_hex(utils.remove_0x_head(address))
return state.get_and_cache_account(account_address)
def _get_block_hash(self, number):
"""Get block hash by block number.
:param number:
:return:
"""
num = _format_block_number(number)
hash_key = header_prefix + num + num_suffix
return self.db.get(hash_key)
def _get_head_block(self):
"""Get head block header.
:return:
"""
if not self.head_block_header:
block_hash = self.db.get(head_header_key)
num = self._get_block_number(block_hash)
self.head_block_header = self._get_block_header(block_hash, num)
# find header with valid state
while (
not self.db.get(self.head_block_header.state_root)
and self.head_block_header.prevhash is not None
):
block_hash = self.head_block_header.prevhash
num = self._get_block_number(block_hash)
self.head_block_header = self._get_block_header(block_hash, num)
return self.head_block_header
def _get_block_number(self, block_hash):
"""Get block number by its hash.
:param block_hash:
:return:
"""
number_key = block_hash_prefix + block_hash
return self.db.get(number_key)
def _get_block_header(self, block_hash, num):
"""Get block header by block header hash & number.
:param block_hash:
:param num:
:return:
"""
header_key = header_prefix + num + block_hash
block_header_data = self.db.get(header_key)
header = rlp.decode(block_header_data, sedes=BlockHeader)
return header
def _get_address_by_hash(self, block_hash):
"""Get mapped address by its hash.
:param block_hash:
:return:
"""
address_key = address_prefix + block_hash
return self.db.get(address_key)
def _get_last_indexed_number(self):
"""Get latest indexed block number.
:return:
"""
return self.db.get(address_mapping_head_key)
def _get_block_receipts(self, block_hash, num):
"""Get block transaction receipts by block header hash & number.
:param block_hash:
:param num:
:return:
"""
number = _format_block_number(num)
receipts_key = block_receipts_prefix + number + block_hash
receipts_data = self.db.get(receipts_key)
receipts = rlp.decode(receipts_data, sedes=CountableList(ReceiptForStorage))
return receipts
class LevelDBWriter(object):
"""level db writing interface."""
def __init__(self, db):
"""
:param db:
"""
self.db = db
self.wb = None
def _set_last_indexed_number(self, number):
"""Set latest indexed block number.
:param number:
:return:
"""
return self.db.put(address_mapping_head_key, _format_block_number(number))
def _start_writing(self):
"""Start writing a batch."""
self.wb = self.db.write_batch()
def _commit_batch(self):
"""Commit a batch."""
self.wb.write()
def _store_account_address(self, address):
"""Get block transaction receipts by block header hash & number.
:param address:
"""
address_key = address_prefix + utils.sha3(address)
self.wb.put(address_key, address)
class EthLevelDB(object):
"""Go-Ethereum LevelDB client class."""
def __init__(self, path):
"""
:param path:
"""
self.path = path
self.db = ETH_DB(path)
self.reader = LevelDBReader(self.db)
self.writer = LevelDBWriter(self.db)
def get_contracts(self):
"""Iterate through all contracts."""
for account in self.reader._get_head_state().get_all_accounts():
if account.code is not None:
code = _encode_hex(account.code)
contract = EVMContract(code, enable_online_lookup=False)
yield contract, account.address, account.balance
def search(self, expression, callback_func):
"""Search through all contract accounts.
:param expression:
:param callback_func:
"""
cnt = 0
indexer = AccountIndexer(self)
for contract, address_hash, balance in self.get_contracts():
if contract.matches_expression(expression):
try:
address = _encode_hex(indexer.get_contract_by_hash(address_hash))
except AddressNotFoundError:
"""The hash->address mapping does not exist in our index.
If the index is up-to-date, this likely means that
the contract was created by an internal transaction.
Skip this contract as right now we don't have a good
solution for this.
"""
continue
callback_func(contract, address, balance)
cnt += 1
if not cnt % 1000:
log.info("Searched %d contracts" % cnt)
def contract_hash_to_address(self, contract_hash):
"""Try to find corresponding account address.
:param contract_hash:
:return:
"""
address_hash = binascii.a2b_hex(utils.remove_0x_head(contract_hash))
indexer = AccountIndexer(self)
return _encode_hex(indexer.get_contract_by_hash(address_hash))
def eth_getBlockHeaderByNumber(self, number):
"""Get block header by block number.
:param number:
:return:
"""
block_hash = self.reader._get_block_hash(number)
block_number = _format_block_number(number)
return self.reader._get_block_header(block_hash, block_number)
def eth_getBlockByNumber(self, number):
"""Get block body by block number.
:param number:
:return:
"""
block_hash = self.reader._get_block_hash(number)
block_number = _format_block_number(number)
body_key = body_prefix + block_number + block_hash
block_data = self.db.get(body_key)
body = rlp.decode(block_data, sedes=Block)
return body
def eth_getCode(self, address):
"""Get account code.
:param address:
:return:
"""
account = self.reader._get_account(address)
return _encode_hex(account.code)
def eth_getBalance(self, address):
"""Get account balance.
:param address:
:return:
"""
account = self.reader._get_account(address)
return account.balance
def eth_getStorageAt(self, address, position):
"""Get account storage data at position.
:param address:
:param position:
:return:
"""
account = self.reader._get_account(address)
return _encode_hex(
utils.zpad(utils.encode_int(account.get_storage_data(position)), 32)
)

@ -1,23 +0,0 @@
"""This module contains the ETH_DB class, which the base database used by
pyethereum."""
import plyvel
from ethereum.db import BaseDB
class ETH_DB(BaseDB):
"""Adopts pythereum BaseDB using plyvel."""
def __init__(self, path):
self.db = plyvel.DB(path)
def get(self, key):
"""gets value for key."""
return self.db.get(key)
def put(self, key, value):
"""puts value for key."""
self.db.put(key, value)
def write_batch(self):
"""start writing a batch."""
return self.db.write_batch()

@ -1,165 +0,0 @@
"""This module implements wrappers around the pyethereum state for LevelDB."""
import rlp
import binascii
from ethereum.utils import (
normalize_address,
hash32,
trie_root,
big_endian_int,
address,
int256,
encode_hex,
encode_int,
big_endian_to_int,
int_to_addr,
zpad,
parse_as_bin,
parse_as_int,
decode_hex,
sha3,
is_string,
is_numeric,
)
from rlp.sedes import big_endian_int, Binary, binary, CountableList
from ethereum import utils
from ethereum import trie
from ethereum.trie import Trie
from ethereum.securetrie import SecureTrie
BLANK_HASH = utils.sha3(b"")
BLANK_ROOT = utils.sha3rlp(b"")
STATE_DEFAULTS = {
"txindex": 0,
"gas_used": 0,
"gas_limit": 3141592,
"block_number": 0,
"block_coinbase": "\x00" * 20,
"block_difficulty": 1,
"timestamp": 0,
"logs": [],
"receipts": [],
"bloom": 0,
"suicides": [],
"recent_uncles": {},
"prev_headers": [],
"refunds": 0,
}
class Account(rlp.Serializable):
"""adjusted account from ethereum.state."""
fields = [
("nonce", big_endian_int),
("balance", big_endian_int),
("storage", trie_root),
("code_hash", hash32),
]
def __init__(self, nonce, balance, storage, code_hash, db, addr):
"""
:param nonce:
:param balance:
:param storage:
:param code_hash:
:param db:
:param addr:
"""
self.db = db
self.address = addr
super(Account, self).__init__(nonce, balance, storage, code_hash)
self.storage_cache = {}
self.storage_trie = SecureTrie(Trie(self.db))
self.storage_trie.root_hash = self.storage
self.touched = False
self.existent_at_start = True
self._mutable = True
self.deleted = False
@property
def code(self):
"""code rlp data."""
return self.db.get(self.code_hash)
def get_storage_data(self, key):
"""get storage data.
:param key:
:return:
"""
if key not in self.storage_cache:
v = self.storage_trie.get(utils.encode_int32(key))
self.storage_cache[key] = utils.big_endian_to_int(
rlp.decode(v) if v else b""
)
return self.storage_cache[key]
@classmethod
def blank_account(cls, db, addr, initial_nonce=0):
"""creates a blank account.
:param db:
:param addr:
:param initial_nonce:
:return:
"""
db.put(BLANK_HASH, b"")
o = cls(initial_nonce, 0, trie.BLANK_ROOT, BLANK_HASH, db, addr)
o.existent_at_start = False
return o
def is_blank(self):
"""checks if is a blank account.
:return:
"""
return self.nonce == 0 and self.balance == 0 and self.code_hash == BLANK_HASH
class State:
"""adjusted state from ethereum.state."""
def __init__(self, db, root):
"""
:param db:
:param root:
"""
self.db = db
self.trie = Trie(self.db, root)
self.secure_trie = SecureTrie(self.trie)
self.journal = []
self.cache = {}
def get_and_cache_account(self, addr):
"""Gets and caches an account for an addres, creates blank if not
found.
:param addr:
:return:
"""
if addr in self.cache:
return self.cache[addr]
rlpdata = self.secure_trie.get(addr)
if (
rlpdata == trie.BLANK_NODE and len(addr) == 32
): # support for hashed addresses
rlpdata = self.trie.get(addr)
if rlpdata != trie.BLANK_NODE:
o = rlp.decode(rlpdata, Account, db=self.db, addr=addr)
else:
o = Account.blank_account(self.db, addr, 0)
self.cache[addr] = o
o._mutable = True
o._cached_rlp = None
return o
def get_all_accounts(self):
"""iterates through trie to and yields non-blank leafs as accounts."""
for address_hash, rlpdata in self.secure_trie.trie.iter_branch():
if rlpdata != trie.BLANK_NODE:
yield rlp.decode(rlpdata, Account, db=self.db, addr=address_hash)

@ -42,7 +42,7 @@ def wei_to_ether(wei):
:param wei:
:return:
"""
return 1.0 * wei / 10 ** 18
return 1.0 * wei / 10**18
def ether_to_wei(ether):
@ -51,4 +51,4 @@ def ether_to_wei(ether):
:param ether:
:return:
"""
return ether * 10 ** 18
return ether * 10**18

@ -7,18 +7,19 @@ import os
import platform
import logging
import solc
import re
from pathlib import Path
from subprocess import PIPE, Popen
from ethereum.abi import encode_abi, encode_int, method_id
from ethereum.utils import zpad
from typing import Optional
from json.decoder import JSONDecodeError
from semantic_version import Version, NpmSpec
from mythril.exceptions import CompilerError
from semantic_version import Version
from mythril.support.support_args import args
if sys.version_info[1] >= 6:
import solcx
from solcx.exceptions import SolcNotInstalled
import solcx
log = logging.getLogger(__name__)
@ -43,14 +44,17 @@ def get_solc_json(file, solc_binary="solc", solc_settings_json=None):
:param solc_settings_json:
:return:
"""
cmd = [solc_binary, "--standard-json", "--allow-paths", "."]
cmd = [solc_binary, "--standard-json", "--allow-paths", ".,/"]
settings = {}
if solc_settings_json:
with open(solc_settings_json) as f:
settings = json.load(f)
if "optimizer" not in settings:
settings.update({"optimizer": {"enabled": False}})
settings.update(
{
"optimizer": {"enabled": True},
"outputSelection": {
"*": {
"": ["ast"],
@ -87,7 +91,7 @@ def get_solc_json(file, solc_binary="solc", solc_settings_json=None):
try:
result = json.loads(out)
except JSONDecodeError as e:
log.error(f"Encountered a decode error, stdout:{out}, stderr: {stderr}")
log.error(f"Encountered a decode error.\n stdout:{out}\n stderr: {stderr}")
raise e
for error in result.get("errors", []):
@ -99,20 +103,6 @@ def get_solc_json(file, solc_binary="solc", solc_settings_json=None):
return result
def encode_calldata(func_name, arg_types, args):
"""
:param func_name:
:param arg_types:
:param args:
:return:
"""
mid = method_id(func_name, arg_types)
function_selector = zpad(encode_int(mid), 4)
args = encode_abi(arg_types, args)
return "0x" + function_selector.hex() + args.hex()
def get_random_address():
"""
@ -138,31 +128,46 @@ def solc_exists(version):
"""
default_binary = "/usr/bin/solc"
if sys.version_info[1] >= 6:
if platform.system() == "Darwin":
solcx.import_installed_solc()
solcx.install_solc("v" + version)
solcx.set_solc_version("v" + version)
solc_binary = solcx.install.get_executable()
return solc_binary
elif Version("0.4.2") <= Version(version) <= Version("0.4.25"):
if not solc.main.is_solc_available():
solc.install_solc("v" + version)
solc_binary = solc.install.get_executable_path("v" + version)
return solc_binary
else:
solc_binaries = [
os.path.join(
os.environ.get("HOME", str(Path.home())),
".py-solc/solc-v" + version,
"bin/solc",
) # py-solc setup
]
for solc_path in solc_binaries:
if os.path.exists(solc_path):
return solc_path
elif os.path.exists(default_binary):
return default_binary
if platform.system() == "Darwin":
solcx.import_installed_solc()
solcx.install_solc("v" + version)
solcx.set_solc_version("v" + version)
solc_binary = solcx.install.get_executable()
return solc_binary
else:
all_versions = solcx.get_installable_solc_versions()
def extract_version(file: str) -> Optional[str]:
version_line = None
for line in file.split("\n"):
if "pragma solidity" not in line:
continue
version_line = line.rstrip()
break
if version_line is None:
return None
assert "pragma solidity" in version_line
if version_line[-1] == ";":
version_line = version_line[:-1]
version_line = version_line.split(";")[0]
version = re.search("pragma solidity ([\d.^]*)", version_line).group(1)
version_constraint = NpmSpec(version)
for version in all_versions:
if version in version_constraint:
return str(version)
return None
def extract_binary(file: str) -> str:
with open(file) as f:
version = extract_version(f.read())
if version and NpmSpec("^0.8.0").match(Version(version)):
args.use_integer_module = False
if version is None:
return os.environ.get("SOLC") or "solc"
return solc_exists(version)

@ -20,6 +20,13 @@ class UnsatError(MythrilBaseException):
pass
class SolverTimeOutException(UnsatError):
"""A Mythril exception denoting the unsatisfiability of a series of
constraints."""
pass
class NoContractFoundError(MythrilBaseException):
"""A Mythril exception denoting that a given contract file was not
found."""
@ -34,15 +41,14 @@ class CriticalError(MythrilBaseException):
pass
class AddressNotFoundError(MythrilBaseException):
"""A Mythril exception denoting the given smart contract address was not
found."""
class DetectorNotFoundError(MythrilBaseException):
"""A Mythril exception denoting attempted usage of a non-existant
detection module."""
pass
class DetectorNotFoundError(MythrilBaseException):
"""A Mythril exception denoting attempted usage of a non-existant
detection module."""
class IllegalArgumentError(ValueError):
"""The argument used does not exist"""
pass

@ -13,24 +13,23 @@ import sys
import coloredlogs
import traceback
from ast import literal_eval
import mythril.support.signatures as sigs
from argparse import ArgumentParser, Namespace, RawTextHelpFormatter
from mythril.concolic import concolic_execution
from mythril.exceptions import (
AddressNotFoundError,
DetectorNotFoundError,
CriticalError,
)
from mythril.laser.ethereum.transaction.symbolic import ACTORS
from mythril.plugin.discovery import PluginDiscovery
from mythril.plugin.loader import MythrilPluginLoader
from mythril.mythril import (
MythrilAnalyzer,
MythrilDisassembler,
MythrilConfig,
MythrilLevelDB,
)
from mythril.mythril import MythrilAnalyzer, MythrilDisassembler, MythrilConfig
from mythril.analysis.module import ModuleLoader
from mythril.analysis.report import Report
from mythril.__version__ import __version__ as VERSION
@ -40,19 +39,29 @@ _ = MythrilPluginLoader()
ANALYZE_LIST = ("analyze", "a")
DISASSEMBLE_LIST = ("disassemble", "d")
CONCOLIC_LIST = ("concolic", "c")
SAFE_FUNCTIONS_COMMAND = "safe-functions"
READ_STORAGE_COMNAND = "read-storage"
FUNCTION_TO_HASH_COMMAND = "function-to-hash"
HASH_TO_ADDRESS_COMMAND = "hash-to-address"
LIST_DETECTORS_COMMAND = "list-detectors"
VERSION_COMMAND = "version"
HELP_COMMAND = "help"
log = logging.getLogger(__name__)
COMMAND_LIST = (
ANALYZE_LIST
+ DISASSEMBLE_LIST
+ CONCOLIC_LIST
+ (
"read-storage",
"leveldb-search",
"function-to-hash",
"hash-to-address",
"list-detectors",
"version",
"help",
READ_STORAGE_COMNAND,
SAFE_FUNCTIONS_COMMAND,
FUNCTION_TO_HASH_COMMAND,
HASH_TO_ADDRESS_COMMAND,
LIST_DETECTORS_COMMAND,
VERSION_COMMAND,
HELP_COMMAND,
)
)
@ -124,6 +133,28 @@ def get_creation_input_parser() -> ArgumentParser:
return parser
def get_safe_functions_parser() -> ArgumentParser:
"""
Returns Parser which handles checking for safe functions
:return: Parser which handles checking for safe functions
"""
parser = ArgumentParser(add_help=False)
parser.add_argument(
"-c",
"--code",
help='hex-encoded bytecode string ("6060604052...")',
metavar="BYTECODE",
)
parser.add_argument(
"-f",
"--codefile",
help="file containing hex-encoded bytecode string",
metavar="BYTECODEFILE",
type=argparse.FileType("r"),
)
return parser
def get_output_parser() -> ArgumentParser:
"""
Get parser which handles output
@ -156,6 +187,8 @@ def get_rpc_parser() -> ArgumentParser:
parser.add_argument(
"--rpctls", type=bool, default=False, help="RPC connection over TLS"
)
parser.add_argument("--infura-id", help="set infura id for onchain analysis")
return parser
@ -177,6 +210,29 @@ def get_utilities_parser() -> ArgumentParser:
return parser
def create_concolic_parser(parser: ArgumentParser) -> ArgumentParser:
"""
Get parser which handles arguments for concolic branch flipping
"""
parser.add_argument(
"input",
help="The input jsonv2 file with concrete data",
)
parser.add_argument(
"--branches",
help="branch addresses to be flipped. usage: --branches 34,6f8,16a",
required=True,
metavar="BRANCH",
)
parser.add_argument(
"--solver-timeout",
type=int,
default=100000,
help="The maximum amount of time(in milli seconds) the solver spends for queries from analysis modules",
)
return parser
def main() -> None:
"""The main CLI interface entry point."""
@ -185,6 +241,7 @@ def main() -> None:
runtime_input_parser = get_runtime_input_parser()
creation_input_parser = get_creation_input_parser()
output_parser = get_output_parser()
parser = argparse.ArgumentParser(
description="Security analysis of Ethereum smart contracts"
)
@ -194,6 +251,18 @@ def main() -> None:
)
subparsers = parser.add_subparsers(dest="command", help="Commands")
safe_function_parser = subparsers.add_parser(
SAFE_FUNCTIONS_COMMAND,
help="Check functions which are completely safe using symbolic execution",
parents=[
rpc_parser,
utilities_parser,
creation_input_parser,
runtime_input_parser,
output_parser,
],
formatter_class=RawTextHelpFormatter,
)
analyzer_parser = subparsers.add_parser(
ANALYZE_LIST[0],
help="Triggers the analysis of the smart contract",
@ -207,6 +276,7 @@ def main() -> None:
aliases=ANALYZE_LIST[1:],
formatter_class=RawTextHelpFormatter,
)
create_safe_functions_parser(safe_function_parser)
create_analyzer_parser(analyzer_parser)
disassemble_parser = subparsers.add_parser(
@ -223,8 +293,18 @@ def main() -> None:
)
create_disassemble_parser(disassemble_parser)
if PluginDiscovery().is_installed("myth_concolic_execution"):
concolic_parser = subparsers.add_parser(
CONCOLIC_LIST[0],
help="Runs concolic execution to flip the desired branches",
aliases=CONCOLIC_LIST[1:],
parents=[],
formatter_class=RawTextHelpFormatter,
)
create_concolic_parser(concolic_parser)
subparsers.add_parser(
"list-detectors",
LIST_DETECTORS_COMMAND,
parents=[output_parser],
help="Lists available detection modules",
)
@ -233,25 +313,21 @@ def main() -> None:
help="Retrieves storage slots from a given address through rpc",
parents=[rpc_parser],
)
leveldb_search_parser = subparsers.add_parser(
"leveldb-search", help="Searches the code fragment in local leveldb"
)
contract_func_to_hash = subparsers.add_parser(
"function-to-hash", help="Returns the hash signature of the function"
FUNCTION_TO_HASH_COMMAND, help="Returns the hash signature of the function"
)
contract_hash_to_addr = subparsers.add_parser(
"hash-to-address",
HASH_TO_ADDRESS_COMMAND,
help="converts the hashes in the blockchain to ethereum address",
)
subparsers.add_parser(
"version", parents=[output_parser], help="Outputs the version"
VERSION_COMMAND, parents=[output_parser], help="Outputs the version"
)
create_read_storage_parser(read_storage_parser)
create_hash_to_addr_parser(contract_hash_to_addr)
create_func_to_hash_parser(contract_func_to_hash)
create_leveldb_parser(leveldb_search_parser)
subparsers.add_parser("help", add_help=False)
subparsers.add_parser(HELP_COMMAND, add_help=False)
# Get config values
@ -291,20 +367,6 @@ def create_read_storage_parser(read_storage_parser: ArgumentParser):
)
def create_leveldb_parser(parser: ArgumentParser):
"""
Modify parser to handle leveldb-search
:param parser:
:return:
"""
parser.add_argument("search")
parser.add_argument(
"--leveldb-dir",
help="specify leveldb directory for search or direct access operations",
metavar="LEVELDB_PATH",
)
def create_func_to_hash_parser(parser: ArgumentParser):
"""
Modify parser to handle func_to_hash command
@ -325,36 +387,42 @@ def create_hash_to_addr_parser(hash_parser: ArgumentParser):
hash_parser.add_argument(
"hash", help="Find the address from hash", metavar="FUNCTION_NAME"
)
hash_parser.add_argument(
"--leveldb-dir",
help="specify leveldb directory for search or direct access operations",
metavar="LEVELDB_PATH",
def add_graph_commands(parser: ArgumentParser):
commands = parser.add_argument_group("commands")
commands.add_argument("-g", "--graph", help="generate a control flow graph")
commands.add_argument(
"-j",
"--statespace-json",
help="dumps the statespace json",
metavar="OUTPUT_FILE",
)
def create_analyzer_parser(analyzer_parser: ArgumentParser):
def create_safe_functions_parser(parser: ArgumentParser):
"""
Modify parser to handle analyze command
:param analyzer_parser:
:return:
The duplication exists between safe-functions and analyze as some of them have different default values.
:param parser: Parser
"""
analyzer_parser.add_argument(
parser.add_argument(
"solidity_files",
nargs="*",
help="Inputs file name and contract name. \n"
"usage: file1.sol:OptionalContractName file2.sol file3.sol:OptionalContractName",
)
commands = analyzer_parser.add_argument_group("commands")
commands.add_argument("-g", "--graph", help="generate a control flow graph")
commands.add_argument(
"-j",
"--statespace-json",
help="dumps the statespace json",
metavar="OUTPUT_FILE",
)
commands.add_argument("--infura-id", help="set infura id for onchain analysis")
options = analyzer_parser.add_argument_group("options")
options = parser.add_argument_group("options")
add_analysis_args(options)
def add_analysis_args(options):
"""
Adds arguments for analysis
:param options: Analysis Options
"""
options.add_argument(
"-m",
"--modules",
@ -380,6 +448,20 @@ def create_analyzer_parser(analyzer_parser: ArgumentParser):
default="bfs",
help="Symbolic execution strategy",
)
options.add_argument(
"--transaction-sequences",
type=str,
default=None,
help="The possible transaction sequences to be executed. "
"Like [[func_hash1, func_hash2], [func_hash2, func_hash3]] where for the first transaction is constrained "
"with func_hash1 and func_hash2, and the second tx is constrained with func_hash2 and func_hash3",
)
options.add_argument(
"--beam-search",
type=int,
default=None,
help="Beam search with with",
)
options.add_argument(
"-b",
"--loop-bound",
@ -429,9 +511,10 @@ def create_analyzer_parser(analyzer_parser: ArgumentParser):
help="Don't attempt to retrieve contract code, variables and balances from the blockchain",
)
options.add_argument(
"--sparse-pruning",
action="store_true",
help="Checks for reachability after the end of tx. Recommended for short execution timeouts < 1 min",
"--pruning-factor",
type=float,
default=1,
help="Checks for reachability at the rate of <pruning-factor> (range 0-1.0). Where 1.0 would mean checking for every execution",
)
options.add_argument(
"--unconstrained-storage",
@ -481,6 +564,23 @@ def create_analyzer_parser(analyzer_parser: ArgumentParser):
)
def create_analyzer_parser(analyzer_parser: ArgumentParser):
"""
Modify parser to handle analyze command
:param analyzer_parser:
:return:
"""
analyzer_parser.add_argument(
"solidity_files",
nargs="*",
help="Inputs file name and contract name. \n"
"usage: file1.sol:OptionalContractName file2.sol file3.sol:OptionalContractName",
)
add_graph_commands(analyzer_parser)
options = analyzer_parser.add_argument_group("options")
add_analysis_args(options)
def validate_args(args: Namespace):
"""
Validate cli args
@ -505,9 +605,24 @@ def validate_args(args: Namespace):
exit_with_error(
args.outform, "Invalid -v value, you can find valid values in usage"
)
if args.command in DISASSEMBLE_LIST and len(args.solidity_files) > 1:
exit_with_error("text", "Only a single arg is supported for using disassemble")
if args.__dict__.get("transaction_sequences", None):
try:
args.transaction_sequences = literal_eval(str(args.transaction_sequences))
except ValueError:
exit_with_error(
args.outform,
"The transaction sequence is in incorrect format, It should be "
"[list of possible function hashes in 1st transaction, "
"list of possible func hashes in 2nd tx, ..]"
"If any list is empty then all possible functions are considered for that transaction",
)
if len(args.transaction_sequences) != args.transaction_count:
args.transaction_count = len(args.transaction_sequences)
if args.command in ANALYZE_LIST:
if args.query_signature and sigs.ethereum_input_decoder is None:
exit_with_error(
@ -539,37 +654,8 @@ def set_config(args: Namespace):
if args.__dict__.get("rpc", None):
# Establish RPC connection if necessary
config.set_api_rpc(rpc=args.rpc, rpctls=args.rpctls)
if args.command in ("hash-to-address", "leveldb-search"):
# Open LevelDB if necessary
if not args.__dict__.get("leveldb_dir", None):
leveldb_dir = config.leveldb_dir
else:
leveldb_dir = args.leveldb_dir
config.set_api_leveldb(leveldb_dir)
return config
def leveldb_search(config: MythrilConfig, args: Namespace):
"""
Handle leveldb search
:param config:
:param args:
:return:
"""
if args.command in ("hash-to-address", "leveldb-search"):
leveldb_searcher = MythrilLevelDB(config.eth_db)
if args.command == "leveldb-search":
# Database search ops
leveldb_searcher.search_db(args.search)
else:
# search corresponding address
try:
leveldb_searcher.contract_hash_to_address(args.hash)
except AddressNotFoundError:
print("Address not found.")
sys.exit()
return config
def load_code(disassembler: MythrilDisassembler, args: Namespace):
@ -610,6 +696,29 @@ def load_code(disassembler: MythrilDisassembler, args: Namespace):
return address
def print_function_report(myth_disassembler: MythrilDisassembler, report: Report):
"""
Prints the function report
:param report: Mythril's report
:return:
"""
contract_data = {}
for contract in myth_disassembler.contracts:
contract_data[contract.name] = list(
set(contract.disassembly.address_to_function_name.values())
)
for issue in report.issues.values():
if issue.function in contract_data[issue.contract]:
contract_data[issue.contract].remove(issue.function)
for contract, function_list in contract_data.items():
print(f"Contract {contract}: \n")
print(
f"""{len(function_list)} functions are deemed safe in this contract: {", ".join(function_list)}\n\n"""
)
def execute_command(
disassembler: MythrilDisassembler,
address: str,
@ -624,6 +733,10 @@ def execute_command(
:param args:
:return:
"""
if args.__dict__.get("beam_search"):
strategy = f"beam-search: {args.beam_search}"
else:
strategy = args.__dict__.get("strategy")
if args.command == "read-storage":
storage = disassembler.get_state_variable_from_storage(
@ -638,27 +751,30 @@ def execute_command(
if disassembler.contracts[0].creation_code:
print("Disassembly: \n" + disassembler.contracts[0].get_creation_easm())
elif args.command == SAFE_FUNCTIONS_COMMAND:
args.unconstrained_storage = True
args.pruning_factor = 1
args.disable_dependency_pruning = True
args.no_onchain_data = True
function_analyzer = MythrilAnalyzer(
strategy=strategy, disassembler=disassembler, address=address, cmd_args=args
)
try:
report = function_analyzer.fire_lasers(
modules=[m.strip() for m in args.modules.strip().split(",")]
if args.modules
else None,
transaction_count=1,
)
print_function_report(disassembler, report)
except DetectorNotFoundError as e:
exit_with_error("text", format(e))
except CriticalError as e:
exit_with_error("text", "Analysis error encountered: " + format(e))
elif args.command in ANALYZE_LIST:
analyzer = MythrilAnalyzer(
strategy=args.strategy,
disassembler=disassembler,
address=address,
max_depth=args.max_depth,
execution_timeout=args.execution_timeout,
loop_bound=args.loop_bound,
create_timeout=args.create_timeout,
enable_iprof=args.enable_iprof,
disable_dependency_pruning=args.disable_dependency_pruning,
use_onchain_data=not args.no_onchain_data,
solver_timeout=args.solver_timeout,
parallel_solving=args.parallel_solving,
custom_modules_directory=args.custom_modules_directory
if args.custom_modules_directory
else "",
call_depth_limit=args.call_depth_limit,
sparse_pruning=args.sparse_pruning,
unconstrained_storage=args.unconstrained_storage,
solver_log=args.solver_log,
strategy=strategy, disassembler=disassembler, address=address, cmd_args=args
)
if not disassembler.contracts:
@ -722,6 +838,10 @@ def execute_command(
"markdown": report.as_markdown(),
}
print(outputs[args.outform])
if len(report.issues) > 0:
exit(1)
else:
exit(0)
except DetectorNotFoundError as e:
exit_with_error(args.outform, format(e))
except CriticalError as e:
@ -760,14 +880,14 @@ def parse_args_and_execute(parser: ArgumentParser, args: Namespace) -> None:
parser.print_help()
sys.exit()
if args.command == "version":
if args.command == VERSION_COMMAND:
if args.outform == "json":
print(json.dumps({"version_str": VERSION}))
else:
print("Mythril version {}".format(VERSION))
sys.exit()
if args.command == "list-detectors":
if args.command == LIST_DETECTORS_COMMAND:
modules = []
for module in ModuleLoader().get_detection_modules():
modules.append({"classname": type(module).__name__, "title": module.name})
@ -778,17 +898,26 @@ def parse_args_and_execute(parser: ArgumentParser, args: Namespace) -> None:
print("{}: {}".format(module_data["classname"], module_data["title"]))
sys.exit()
if args.command == "help":
if args.command == HELP_COMMAND:
parser.print_help()
sys.exit()
if args.command in CONCOLIC_LIST:
_ = MythrilConfig.init_mythril_dir()
with open(args.input) as f:
concrete_data = json.load(f)
output_list = concolic_execution(
concrete_data, args.branches.split(","), args.solver_timeout
)
json.dump(output_list, sys.stdout, indent=4)
sys.exit()
# Parse cmdline args
validate_args(args)
try:
if args.command == "function-to-hash":
if args.command == FUNCTION_TO_HASH_COMMAND:
contract_hash_to_address(args)
config = set_config(args)
leveldb_search(config, args)
query_signature = args.__dict__.get("query_signature", None)
solc_json = args.__dict__.get("solc_json", None)
solv = args.__dict__.get("solv", None)

@ -16,6 +16,7 @@ import random
import re
import sys
import time
import argparse
PY3 = sys.version_info >= (3,)
@ -165,7 +166,7 @@ class LolCat(object):
if not s:
return
for i in range(1, options.duration):
for _ in range(1, options.duration):
self.output.write("\x1b[%dD" % (len(s),))
self.output.flush()
options.os += options.spread
@ -208,30 +209,29 @@ def detect_mode(term_hint="xterm-256color"):
def run():
"""Main entry point."""
import optparse
parser = optparse.OptionParser(usage=r"%prog [<options>] [file ...]")
parser.add_option(
"-p", "--spread", type="float", default=3.0, help="Rainbow spread"
parser = argparse.ArgumentParser(usage=r"%prog [<options>] [file ...]")
parser.add_argument(
"-p", "--spread", type=float, default=3.0, help="Rainbow spread"
)
parser.add_option(
"-F", "--freq", type="float", default=0.1, help="Rainbow frequency"
parser.add_argument(
"-F", "--freq", type=float, default=0.1, help="Rainbow frequency"
)
parser.add_option("-S", "--seed", type="int", default=0, help="Rainbow seed")
parser.add_option(
parser.add_argument("-S", "--seed", type=int, default=0, help="Rainbow seed")
parser.add_argument(
"-a",
"--animate",
action="store_true",
default=False,
help="Enable psychedelics",
)
parser.add_option(
"-d", "--duration", type="int", default=12, help="Animation duration"
parser.add_argument(
"-d", "--duration", type=int, default=12, help="Animation duration"
)
parser.add_option(
"-s", "--speed", type="float", default=20.0, help="Animation speed"
parser.add_argument(
"-s", "--speed", type=float, default=20.0, help="Animation speed"
)
parser.add_option(
parser.add_argument(
"-f",
"--force",
action="store_true",
@ -239,17 +239,17 @@ def run():
help="Force colour even when stdout is not a tty",
)
parser.add_option(
parser.add_argument(
"-3", action="store_const", dest="mode", const=8, help="Force 3 bit colour mode"
)
parser.add_option(
parser.add_argument(
"-4",
action="store_const",
dest="mode",
const=16,
help="Force 4 bit colour mode",
)
parser.add_option(
parser.add_argument(
"-8",
action="store_const",
dest="mode",
@ -257,21 +257,19 @@ def run():
help="Force 8 bit colour mode",
)
parser.add_option(
parser.add_argument(
"-c",
"--charset-py2",
default="utf-8",
help="Manually set a charset to convert from, for python 2.7",
)
options, args = parser.parse_args()
options = parser.parse_args()
options.os = random.randint(0, 256) if options.seed == 0 else options.seed
options.mode = options.mode or detect_mode()
lolcat = LolCat(mode=options.mode)
if not args:
args = ["-"]
args = ["-"]
for filename in args:
if filename == "-":

@ -4,8 +4,8 @@ parameters for the new global state."""
import logging
import re
from typing import Union, List, cast, Callable, Optional
from ethereum.opcodes import GSTIPEND
from typing import Union, List, cast, Optional
from eth.constants import GAS_CALLSTIPEND
import mythril.laser.ethereum.util as util
from mythril.laser.ethereum import natives
@ -18,7 +18,7 @@ from mythril.laser.ethereum.state.calldata import (
ConcreteCalldata,
)
from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.laser.smt import BitVec, is_true, If
from mythril.laser.smt import BitVec, If
from mythril.laser.smt import simplify, Expression, symbol_factory
from mythril.support.loader import DynLoader
@ -63,7 +63,7 @@ def get_call_parameters(
global_state, callee_address, dynamic_loader
)
gas = gas + If(value > 0, symbol_factory.BitVecVal(GSTIPEND, gas.size()), 0)
gas = gas + If(value > 0, symbol_factory.BitVecVal(GAS_CALLSTIPEND, gas.size()), 0)
return (
callee_address,
callee_account,
@ -101,7 +101,6 @@ def get_callee_address(
log.debug("Symbolic call encountered")
match = re.search(r"Storage\[(\d+)\]", str(simplify(symbolic_to_address)))
log.debug("CALL to: " + str(simplify(symbolic_to_address)))
if match is None or dynamic_loader is None:
return symbolic_to_address
@ -179,6 +178,7 @@ def get_call_data(
else memory_size
),
)
if memory_size.symbolic:
memory_size = SYMBOLIC_CALLDATA_SIZE
try:
@ -189,9 +189,7 @@ def get_call_data(
]
return ConcreteCalldata(transaction_id, calldata_from_mem)
except TypeError:
log.debug(
"Unsupported symbolic memory offset %s size %s", memory_start, memory_size
)
log.debug("Unsupported symbolic memory offset and size")
return SymbolicCalldata(transaction_id)

@ -66,7 +66,7 @@ class Node:
code += str(instruction["address"]) + " " + instruction["opcode"]
if instruction["opcode"].startswith("PUSH"):
code += " " + instruction["argument"]
code += " " + "".join(str(instruction["argument"]))
code += "\\n"

@ -1,2 +1,2 @@
from .exponent_function_manager import exponent_function_manager
from .keccak_function_manager import keccak_function_manager
from .keccak_function_manager import keccak_function_manager, KeccakFunctionManager

@ -1,16 +1,8 @@
import logging
from typing import Dict, List, Optional, Tuple
from typing import Tuple
from ethereum import utils
from mythril.laser.smt import (
And,
BitVec,
Bool,
Function,
URem,
symbol_factory,
)
from mythril.laser.smt import And, BitVec, Bool, Function, URem, symbol_factory
log = logging.getLogger(__name__)
@ -20,7 +12,7 @@ class ExponentFunctionManager:
Uses an uninterpreted function for exponentiation with the following properties:
1) power(a, b) > 0
2) if a = 256 => forall i if b = i then power(a, b) = (256 ^ i) % (2^256)
Only these two properties are added as to handle indexing of boolean arrays.
Caution should be exercised when increasing the conditions since it severely affects
the solving time.
@ -32,11 +24,10 @@ class ExponentFunctionManager:
self.concrete_constraints = And(
*[
power(NUMBER_256, symbol_factory.BitVecVal(i, 256))
== symbol_factory.BitVecVal(256 ** i, 256)
== symbol_factory.BitVecVal(256**i, 256)
for i in range(0, 32)
]
)
self.concrete_constraints_sent = False
def create_condition(self, base: BitVec, exponent: BitVec) -> Tuple[BitVec, Bool]:
"""
@ -50,7 +41,7 @@ class ExponentFunctionManager:
if exponent.symbolic is False and base.symbolic is False:
const_exponentiation = symbol_factory.BitVecVal(
pow(base.value, exponent.value, 2 ** 256),
pow(base.value, exponent.value, 2**256),
256,
annotations=base.annotations.union(exponent.annotations),
)
@ -58,9 +49,7 @@ class ExponentFunctionManager:
return const_exponentiation, constraint
constraint = exponentiation > 0
if self.concrete_constraints_sent is False:
constraint = And(constraint, self.concrete_constraints)
self.concrete_constraints_sent = True
constraint = And(constraint, self.concrete_constraints)
if base.value == 256:
constraint = And(
constraint,

@ -1,4 +1,3 @@
from ethereum import utils
from mythril.laser.smt import (
BitVec,
Function,
@ -10,13 +9,16 @@ from mythril.laser.smt import (
Bool,
Or,
)
from mythril.support.support_utils import sha3
from typing import Dict, Tuple, List, Optional
import logging
TOTAL_PARTS = 10 ** 40
PART = (2 ** 256 - 1) // TOTAL_PARTS
INTERVAL_DIFFERENCE = 10 ** 30
TOTAL_PARTS = 10**40
PART = (2**256 - 1) // TOTAL_PARTS
INTERVAL_DIFFERENCE = 10**30
log = logging.getLogger(__name__)
@ -34,12 +36,22 @@ class KeccakFunctionManager:
hash_matcher = "fffffff" # This is usually the prefix for the hash in the output
def __init__(self):
self.store_function = {} # type: Dict[int, Tuple[Function, Function]]
self.interval_hook_for_size = {} # type: Dict[int, int]
self.store_function: Dict[int, Tuple[Function, Function]] = {}
self.interval_hook_for_size: Dict[int, int] = {}
self._index_counter = TOTAL_PARTS - 34534
self.hash_result_store = {} # type: Dict[int, List[BitVec]]
self.quick_inverse = {} # type: Dict[BitVec, BitVec] # This is for VMTests
self.concrete_hashes = {} # type: Dict[BitVec, BitVec]
self.hash_result_store: Dict[int, List[BitVec]] = {}
self.quick_inverse: Dict[BitVec, BitVec] = {} # This is for VMTests
self.concrete_hashes: Dict[BitVec, BitVec] = {}
self.symbolic_inputs: Dict[int, List[BitVec]] = {}
def reset(self):
self.store_function = {}
self.interval_hook_for_size = {}
self.hash_result_store: Dict[int, List[BitVec]] = {}
self.quick_inverse = {}
self.concrete_hashes = {}
self.symbolic_inputs = {}
@staticmethod
def find_concrete_keccak(data: BitVec) -> BitVec:
@ -50,8 +62,7 @@ class KeccakFunctionManager:
"""
keccak = symbol_factory.BitVecVal(
int.from_bytes(
utils.sha3(data.value.to_bytes(data.size() // 8, byteorder="big")),
"big",
sha3(data.value.to_bytes(data.size() // 8, byteorder="big")), "big"
),
256,
)
@ -81,25 +92,42 @@ class KeccakFunctionManager:
val = 89477152217924674838424037953991966239322087453347756267410168184682657981552
return symbol_factory.BitVecVal(val, 256)
def create_keccak(self, data: BitVec) -> Tuple[BitVec, Bool]:
def create_keccak(self, data: BitVec) -> BitVec:
"""
Creates Keccak of the data
:param data: input
:return: Tuple of keccak and the condition it should satisfy
"""
length = data.size()
func, inverse = self.get_function(length)
func, _ = self.get_function(length)
if data.symbolic is False:
concrete_hash = self.find_concrete_keccak(data)
self.concrete_hashes[data] = concrete_hash
# This condition is essential to avoid some edge cases
condition = And(func(data) == concrete_hash, inverse(func(data)) == data)
return concrete_hash, condition
return concrete_hash
if length not in self.symbolic_inputs:
self.symbolic_inputs[length] = []
condition = self._create_condition(func_input=data)
self.symbolic_inputs[length].append(data)
self.hash_result_store[length].append(func(data))
return func(data), condition
return func(data)
def create_conditions(self) -> Bool:
condition = symbol_factory.Bool(True)
for inputs_list in self.symbolic_inputs.values():
for symbolic_input in inputs_list:
condition = And(
condition, self._create_condition(func_input=symbolic_input)
)
for concrete_input, concrete_hash in self.concrete_hashes.items():
func, inverse = self.get_function(concrete_input.size())
condition = And(
condition,
func(concrete_input) == concrete_hash,
inverse(func(concrete_input)) == concrete_input,
)
return condition
def get_concrete_hash_data(self, model) -> Dict[int, List[Optional[int]]]:
"""
@ -145,8 +173,9 @@ class KeccakFunctionManager:
)
concrete_cond = symbol_factory.Bool(False)
for key, keccak in self.concrete_hashes.items():
hash_eq = And(func(func_input) == keccak, key == func_input)
concrete_cond = Or(concrete_cond, hash_eq)
if key.size() == func_input.size():
hash_eq = And(func(func_input) == keccak, key == func_input)
concrete_cond = Or(concrete_cond, hash_eq)
return And(inv(func(func_input)) == func_input, Or(cond, concrete_cond))

@ -1,190 +1,17 @@
from ethereum import opcodes
from ethereum.utils import ceil32
from typing import Callable, Dict, Tuple, Union
Z_OPERATOR_TUPLE = (0, 1)
UN_OPERATOR_TUPLE = (1, 1)
BIN_OPERATOR_TUPLE = (2, 1)
T_OPERATOR_TUPLE = (3, 1)
GAS = "gas"
STACK = "stack"
# Gas tuple contains (min_gas, max_gas)
# stack tuple contains (no_of_elements_popped, no_of_elements_pushed)
OPCODES = {
"STOP": {GAS: (0, 0), STACK: (0, 0)},
"ADD": {GAS: (3, 3), STACK: BIN_OPERATOR_TUPLE},
"MUL": {GAS: (5, 5), STACK: BIN_OPERATOR_TUPLE},
"SUB": {GAS: (3, 3), STACK: BIN_OPERATOR_TUPLE},
"DIV": {GAS: (5, 5), STACK: BIN_OPERATOR_TUPLE},
"SDIV": {GAS: (5, 5), STACK: BIN_OPERATOR_TUPLE},
"MOD": {GAS: (5, 5), STACK: BIN_OPERATOR_TUPLE},
"SMOD": {GAS: (5, 5), STACK: BIN_OPERATOR_TUPLE},
"ADDMOD": {GAS: (8, 8), STACK: BIN_OPERATOR_TUPLE},
"MULMOD": {GAS: (8, 8), STACK: T_OPERATOR_TUPLE},
"EXP": {GAS: (10, 340), STACK: BIN_OPERATOR_TUPLE}, # exponent max 2^32
"SIGNEXTEND": {GAS: (5, 5), STACK: BIN_OPERATOR_TUPLE},
"LT": {GAS: (3, 3), STACK: BIN_OPERATOR_TUPLE},
"GT": {GAS: (3, 3), STACK: BIN_OPERATOR_TUPLE},
"SLT": {GAS: (3, 3), STACK: BIN_OPERATOR_TUPLE},
"SGT": {GAS: (3, 3), STACK: BIN_OPERATOR_TUPLE},
"EQ": {GAS: (3, 3), STACK: BIN_OPERATOR_TUPLE},
"AND": {GAS: (3, 3), STACK: BIN_OPERATOR_TUPLE},
"ISZERO": {GAS: (3, 3), STACK: UN_OPERATOR_TUPLE},
"OR": {GAS: (3, 3), STACK: BIN_OPERATOR_TUPLE},
"XOR": {GAS: (3, 3), STACK: BIN_OPERATOR_TUPLE},
"NOT": {GAS: (3, 3), STACK: UN_OPERATOR_TUPLE},
"BYTE": {GAS: (3, 3), STACK: BIN_OPERATOR_TUPLE},
"SHL": {GAS: (3, 3), STACK: BIN_OPERATOR_TUPLE},
"SHR": {GAS: (3, 3), STACK: BIN_OPERATOR_TUPLE},
"SAR": {GAS: (3, 3), STACK: BIN_OPERATOR_TUPLE},
"SHA3": {
GAS: (
30,
30 + 6 * 8,
), # max can be larger, but usually storage location with 8 words
STACK: BIN_OPERATOR_TUPLE,
},
"ADDRESS": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE},
"BALANCE": {GAS: (700, 700), STACK: UN_OPERATOR_TUPLE},
"ORIGIN": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE},
"CALLER": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE},
"CALLVALUE": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE},
"CALLDATALOAD": {GAS: (3, 3), STACK: UN_OPERATOR_TUPLE},
"CALLDATASIZE": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE},
"CALLDATACOPY": {
GAS: (2, 2 + 3 * 768), # https://ethereum.stackexchange.com/a/47556
STACK: (3, 0),
},
"CODESIZE": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE},
"CODECOPY": {
GAS: (2, 2 + 3 * 768), # https://ethereum.stackexchange.com/a/47556,
STACK: (3, 0),
},
"GASPRICE": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE},
"EXTCODESIZE": {GAS: (700, 700), STACK: Z_OPERATOR_TUPLE},
"EXTCODECOPY": {
GAS: (700, 700 + 3 * 768), # https://ethereum.stackexchange.com/a/47556
STACK: (4, 0),
},
"EXTCODEHASH": {GAS: (700, 700), STACK: UN_OPERATOR_TUPLE},
"RETURNDATASIZE": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE},
"RETURNDATACOPY": {GAS: (3, 3), STACK: (3, 0)},
"BLOCKHASH": {GAS: (20, 20), STACK: UN_OPERATOR_TUPLE},
"COINBASE": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE},
"TIMESTAMP": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE},
"NUMBER": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE},
"DIFFICULTY": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE},
"GASLIMIT": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE},
"CHAINID": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE},
"SELFBALANCE": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE},
"POP": {GAS: (2, 2), STACK: (1, 0)},
# assume 1KB memory r/w cost as upper bound
"MLOAD": {GAS: (3, 96), STACK: UN_OPERATOR_TUPLE},
"MSTORE": {GAS: (3, 98), STACK: (2, 0)},
"MSTORE8": {GAS: (3, 98), STACK: (2, 0)},
# assume 64 byte r/w cost as upper bound
"SLOAD": {GAS: (800, 800), STACK: UN_OPERATOR_TUPLE},
"SSTORE": {GAS: (5000, 25000), STACK: (1, 0)},
"JUMP": {GAS: (8, 8), STACK: (1, 0)},
"JUMPI": {GAS: (10, 10), STACK: (2, 0)},
"PC": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE},
"MSIZE": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE},
"GAS": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE},
"JUMPDEST": {GAS: (1, 1), STACK: (0, 0)},
"PUSH1": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"PUSH2": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"PUSH3": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"PUSH4": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"PUSH5": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"PUSH6": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"PUSH7": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"PUSH8": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"PUSH9": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"PUSH10": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"PUSH11": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"PUSH12": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"PUSH13": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"PUSH14": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"PUSH15": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"PUSH16": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"PUSH17": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"PUSH18": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"PUSH19": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"PUSH20": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"PUSH21": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"PUSH22": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"PUSH23": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"PUSH24": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"PUSH25": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"PUSH26": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"PUSH27": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"PUSH28": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"PUSH29": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"PUSH30": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"PUSH31": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"PUSH32": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"DUP1": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"DUP2": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"DUP3": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"DUP4": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"DUP5": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"DUP6": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"DUP7": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"DUP8": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"DUP9": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"DUP10": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"DUP11": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"DUP12": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"DUP13": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"DUP14": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"DUP15": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"DUP16": {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE},
"SWAP1": {GAS: (3, 3), STACK: (0, 0)},
"SWAP2": {GAS: (3, 3), STACK: (0, 0)},
"SWAP3": {GAS: (3, 3), STACK: (0, 0)},
"SWAP4": {GAS: (3, 3), STACK: (0, 0)},
"SWAP5": {GAS: (3, 3), STACK: (0, 0)},
"SWAP6": {GAS: (3, 3), STACK: (0, 0)},
"SWAP7": {GAS: (3, 3), STACK: (0, 0)},
"SWAP8": {GAS: (3, 3), STACK: (0, 0)},
"SWAP9": {GAS: (3, 3), STACK: (0, 0)},
"SWAP10": {GAS: (3, 3), STACK: (0, 0)},
"SWAP11": {GAS: (3, 3), STACK: (0, 0)},
"SWAP12": {GAS: (3, 3), STACK: (0, 0)},
"SWAP13": {GAS: (3, 3), STACK: (0, 0)},
"SWAP14": {GAS: (3, 3), STACK: (0, 0)},
"SWAP15": {GAS: (3, 3), STACK: (0, 0)},
"SWAP16": {GAS: (3, 3), STACK: (0, 0)},
# apparently Solidity only allows byte32 as input to the log
# function. Virtually it could be as large as the block gas limit
# allows, but let's stick to the reasonable standard here.
# https://ethereum.stackexchange.com/a/1691
"LOG0": {GAS: (375, 375 + 8 * 32), STACK: (2, 0)},
"LOG1": {GAS: (2 * 375, 2 * 375 + 8 * 32), STACK: (3, 0)},
"LOG2": {GAS: (3 * 375, 3 * 375 + 8 * 32), STACK: (4, 0)},
"LOG3": {GAS: (4 * 375, 4 * 375 + 8 * 32), STACK: (5, 0)},
"LOG4": {GAS: (5 * 375, 5 * 375 + 8 * 32), STACK: (6, 0)},
"CREATE": {GAS: (32000, 32000), STACK: T_OPERATOR_TUPLE},
"CREATE2": {
GAS: (32000, 32000), # TODO: Make the gas values dynamic
STACK: (4, 1),
},
"CALL": {GAS: (700, 700 + 9000 + 25000), STACK: (7, 1)},
"CALLCODE": {GAS: (700, 700 + 9000 + 25000), STACK: (7, 1)},
"RETURN": {GAS: (0, 0), STACK: (2, 0)},
"DELEGATECALL": {GAS: (700, 700 + 9000 + 25000), STACK: (6, 1)},
"STATICCALL": {GAS: (700, 700 + 9000 + 25000), STACK: (6, 1)},
"REVERT": {GAS: (0, 0), STACK: (2, 0)},
"SUICIDE": {GAS: (5000, 30000), STACK: (1, 0)},
"ASSERT_FAIL": {GAS: (0, 0), STACK: (0, 0)},
"INVALID": {GAS: (0, 0), STACK: (0, 0)},
"BEGINSUB": {GAS: (2, 2), STACK: (0, 0)},
"JUMPSUB": {GAS: (10, 10), STACK: (1, 0)},
"RETURNSUB": {GAS: (5, 5), STACK: (0, 0)},
} # type: Dict[str, Dict[str, Tuple[int, int]]]
from eth._utils.numeric import ceil32
from typing import Tuple
from mythril.support.opcodes import OPCODES, STACK, GAS
from eth.constants import (
GAS_ECRECOVER,
GAS_SHA256WORD,
GAS_SHA256,
GAS_RIPEMD160,
GAS_RIPEMD160WORD,
GAS_IDENTITY,
GAS_IDENTITYWORD,
GAS_SHA3WORD,
GAS_SHA3,
)
def calculate_sha3_gas(length: int):
@ -193,7 +20,7 @@ def calculate_sha3_gas(length: int):
:param length:
:return:
"""
gas_val = 30 + opcodes.GSHA3WORD * (ceil32(length) // 32)
gas_val = GAS_SHA3 + GAS_SHA3WORD * (ceil32(length) // 32)
return gas_val, gas_val
@ -207,13 +34,13 @@ def calculate_native_gas(size: int, contract: str):
gas_value = 0
word_num = ceil32(size) // 32
if contract == "ecrecover":
gas_value = opcodes.GECRECOVER
gas_value = GAS_ECRECOVER
elif contract == "sha256":
gas_value = opcodes.GSHA256BASE + word_num * opcodes.GSHA256WORD
gas_value = GAS_SHA256 + word_num * GAS_SHA256WORD
elif contract == "ripemd160":
gas_value = opcodes.GRIPEMD160BASE + word_num * opcodes.GRIPEMD160WORD
gas_value = GAS_RIPEMD160 + word_num * GAS_RIPEMD160WORD
elif contract == "identity":
gas_value = opcodes.GIDENTITYBASE + word_num * opcodes.GIDENTITYWORD
gas_value = GAS_IDENTITY + word_num * GAS_IDENTITYWORD
else:
# TODO: Add gas for other precompiles, computation should be shifted to natives.py
# as some data isn't available here

Some files were not shown because too many files have changed in this diff Show More

Loading…
Cancel
Save