Merge with develop and add bugfixes

pull/869/head
Nikhil Parasaram 6 years ago
commit 0b66e0207c
  1. 1
      .gitignore
  2. 10
      README.md
  3. 19
      docs/Makefile
  4. 35
      docs/make.bat
  5. 190
      docs/source/conf.py
  6. 17
      docs/source/index.rst
  7. 7
      docs/source/modules.rst
  8. 110
      docs/source/mythril.analysis.modules.rst
  9. 85
      docs/source/mythril.analysis.rst
  10. 30
      docs/source/mythril.disassembler.rst
  11. 46
      docs/source/mythril.ethereum.interface.leveldb.rst
  12. 54
      docs/source/mythril.ethereum.interface.rpc.rst
  13. 18
      docs/source/mythril.ethereum.interface.rst
  14. 37
      docs/source/mythril.ethereum.rst
  15. 30
      docs/source/mythril.interfaces.rst
  16. 103
      docs/source/mythril.laser.ethereum.rst
  17. 86
      docs/source/mythril.laser.ethereum.state.rst
  18. 22
      docs/source/mythril.laser.ethereum.strategy.rst
  19. 38
      docs/source/mythril.laser.ethereum.transaction.rst
  20. 18
      docs/source/mythril.laser.rst
  21. 38
      docs/source/mythril.laser.smt.rst
  22. 51
      docs/source/mythril.rst
  23. 22
      docs/source/mythril.solidity.rst
  24. 46
      docs/source/mythril.support.rst
  25. 25
      mythril/alarm.py
  26. 7
      mythril/analysis/call_helpers.py
  27. 25
      mythril/analysis/callgraph.py
  28. 29
      mythril/analysis/modules/base.py
  29. 14
      mythril/analysis/modules/delegatecall.py
  30. 52
      mythril/analysis/modules/dependence_on_predictable_vars.py
  31. 21
      mythril/analysis/modules/deprecated_ops.py
  32. 150
      mythril/analysis/modules/ether_thief.py
  33. 27
      mythril/analysis/modules/exceptions.py
  34. 25
      mythril/analysis/modules/external_calls.py
  35. 89
      mythril/analysis/modules/integer.py
  36. 10
      mythril/analysis/modules/multiple_sends.py
  37. 15
      mythril/analysis/modules/suicide.py
  38. 69
      mythril/analysis/modules/transaction_order_dependence.py
  39. 14
      mythril/analysis/modules/unchecked_retval.py
  40. 45
      mythril/analysis/ops.py
  41. 59
      mythril/analysis/report.py
  42. 22
      mythril/analysis/security.py
  43. 17
      mythril/analysis/solver.py
  44. 2
      mythril/analysis/swc_data.py
  45. 34
      mythril/analysis/symbolic.py
  46. 12
      mythril/analysis/traceexplore.py
  47. 42
      mythril/disassembler/asm.py
  48. 28
      mythril/disassembler/disassembly.py
  49. 38
      mythril/ethereum/evmcontract.py
  50. 50
      mythril/ethereum/interface/leveldb/accountindexing.py
  51. 162
      mythril/ethereum/interface/leveldb/client.py
  52. 18
      mythril/ethereum/interface/leveldb/eth_db.py
  53. 57
      mythril/ethereum/interface/leveldb/state.py
  54. 42
      mythril/ethereum/interface/rpc/base_client.py
  55. 33
      mythril/ethereum/interface/rpc/client.py
  56. 2
      mythril/ethereum/interface/rpc/constants.py
  57. 17
      mythril/ethereum/interface/rpc/exceptions.py
  58. 33
      mythril/ethereum/interface/rpc/utils.py
  59. 46
      mythril/ethereum/util.py
  60. 23
      mythril/exceptions.py
  61. 18
      mythril/interfaces/cli.py
  62. 45
      mythril/interfaces/epic.py
  63. 22
      mythril/laser/ethereum/call.py
  64. 37
      mythril/laser/ethereum/cfg.py
  65. 15
      mythril/laser/ethereum/evm_exceptions.py
  66. 13
      mythril/laser/ethereum/gas.py
  67. 443
      mythril/laser/ethereum/instructions.py
  68. 20
      mythril/laser/ethereum/keccak.py
  69. 46
      mythril/laser/ethereum/natives.py
  70. 41
      mythril/laser/ethereum/state/account.py
  71. 27
      mythril/laser/ethereum/state/annotation.py
  72. 128
      mythril/laser/ethereum/state/calldata.py
  73. 48
      mythril/laser/ethereum/state/constraints.py
  74. 30
      mythril/laser/ethereum/state/environment.py
  75. 58
      mythril/laser/ethereum/state/global_state.py
  76. 86
      mythril/laser/ethereum/state/machine_state.py
  77. 42
      mythril/laser/ethereum/state/memory.py
  78. 55
      mythril/laser/ethereum/state/world_state.py
  79. 3
      mythril/laser/ethereum/strategy/__init__.py
  80. 49
      mythril/laser/ethereum/strategy/basic.py
  81. 193
      mythril/laser/ethereum/svm.py
  82. 147
      mythril/laser/ethereum/taint_analysis.py
  83. 23
      mythril/laser/ethereum/transaction/concolic.py
  84. 22
      mythril/laser/ethereum/transaction/symbolic.py
  85. 57
      mythril/laser/ethereum/transaction/transaction_models.py
  86. 65
      mythril/laser/ethereum/util.py
  87. 20
      mythril/laser/smt/__init__.py
  88. 31
      mythril/laser/smt/array.py
  89. 190
      mythril/laser/smt/bitvec.py
  90. 65
      mythril/laser/smt/bool.py
  91. 30
      mythril/laser/smt/expression.py
  92. 58
      mythril/laser/smt/solver.py
  93. 137
      mythril/mythril.py
  94. 27
      mythril/solidity/soliditycontract.py
  95. 20
      mythril/support/loader.py
  96. 95
      mythril/support/signatures.py
  97. 1
      mythril/support/support_utils.py
  98. 32
      mythril/support/truffle.py
  99. 8
      mythril/version.py
  100. 11
      setup.py
  101. Some files were not shown because too many files have changed in this diff Show More

1
.gitignore vendored

@ -168,7 +168,6 @@ $RECYCLE.BIN/
# End of https://www.gitignore.io/api/linux,macos,python,windows
*.asm
*.rst
*.lock
*.svg
lol*

@ -39,6 +39,16 @@ Instructions for using Mythril Classic are found on the [Wiki](https://github.co
For support or general discussions please join the Mythril community on [Discord](https://discord.gg/E3YrVtG).
## Bulding the Documentation
Mythril Classic's documentation is contained in the `docs` folder. It is based on Sphinx and can be built using the Makefile contained in the subdirectory:
```
cd docs
make html
```
This will create a `build` output directory containing the HTML output. Alternatively, PDF documentation can be built with `make latexpdf`. The available output format options can be seen with `make help`.
## Vulnerability Remediation
Visit the [Smart Contract Vulnerability Classification Registry](https://smartcontractsecurity.github.io/SWC-registry/) to find detailed information and remediation guidance for the vulnerabilities reported.

@ -0,0 +1,19 @@
# Minimal makefile for Sphinx documentation
#
# You can set these variables from the command line.
SPHINXOPTS =
SPHINXBUILD = sphinx-build
SOURCEDIR = source
BUILDDIR = build
# Put it first so that "make" without argument is like "make help".
help:
@$(SPHINXBUILD) -M help "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O)
.PHONY: help Makefile
# Catch-all target: route all unknown targets to Sphinx using the new
# "make mode" option. $(O) is meant as a shortcut for $(SPHINXOPTS).
%: Makefile
@$(SPHINXBUILD) -M $@ "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O)

@ -0,0 +1,35 @@
@ECHO OFF
pushd %~dp0
REM Command file for Sphinx documentation
if "%SPHINXBUILD%" == "" (
set SPHINXBUILD=sphinx-build
)
set SOURCEDIR=source
set BUILDDIR=build
if "%1" == "" goto help
%SPHINXBUILD% >NUL 2>NUL
if errorlevel 9009 (
echo.
echo.The 'sphinx-build' command was not found. Make sure you have Sphinx
echo.installed, then set the SPHINXBUILD environment variable to point
echo.to the full path of the 'sphinx-build' executable. Alternatively you
echo.may add the Sphinx directory to PATH.
echo.
echo.If you don't have Sphinx installed, grab it from
echo.http://sphinx-doc.org/
exit /b 1
)
%SPHINXBUILD% -M %1 %SOURCEDIR% %BUILDDIR% %SPHINXOPTS%
goto end
:help
%SPHINXBUILD% -M help %SOURCEDIR% %BUILDDIR% %SPHINXOPTS%
:end
popd

@ -0,0 +1,190 @@
# -*- coding: utf-8 -*-
#
# Configuration file for the Sphinx documentation builder.
#
# This file does only contain a selection of the most common options. For a
# full list see the documentation:
# http://www.sphinx-doc.org/en/master/config
# -- Path setup --------------------------------------------------------------
# If extensions (or modules to document with autodoc) are in another directory,
# add these directories to sys.path here. If the directory is relative to the
# documentation root, use os.path.abspath to make it absolute, like shown here.
import os
import sys
sys.path.insert(0, os.path.abspath("../../"))
# -- Project information -----------------------------------------------------
project = "Mythril Classic"
copyright = "2018, Bernhard Mueller"
author = "Bernhard Mueller"
# The short X.Y version
version = ""
# The full version, including alpha/beta/rc tags
from mythril.version import VERSION
release = VERSION
# -- General configuration ---------------------------------------------------
# If your documentation needs a minimal Sphinx version, state it here.
#
# needs_sphinx = '1.0'
# Add any Sphinx extension module names here, as strings. They can be
# extensions coming with Sphinx (named 'sphinx.ext.*') or your custom
# ones.
extensions = [
"sphinx.ext.autodoc",
"sphinx.ext.coverage",
"sphinx.ext.mathjax",
"sphinx.ext.viewcode",
]
# Add any paths that contain templates here, relative to this directory.
templates_path = ["_templates"]
# The suffix(es) of source filenames.
# You can specify multiple suffix as a list of string:
#
# source_suffix = ['.rst', '.md']
source_suffix = ".rst"
# The master toctree document.
master_doc = "index"
# The language for content autogenerated by Sphinx. Refer to documentation
# for a list of supported languages.
#
# This is also used if you do content translation via gettext catalogs.
# Usually you set "language" from the command line for these cases.
language = None
# List of patterns, relative to source directory, that match files and
# directories to ignore when looking for source files.
# This pattern also affects html_static_path and html_extra_path.
exclude_patterns = []
# The name of the Pygments (syntax highlighting) style to use.
pygments_style = None
# -- Options for HTML output -------------------------------------------------
# The theme to use for HTML and HTML Help pages. See the documentation for
# a list of builtin themes.
#
html_theme = "alabaster"
# Theme options are theme-specific and customize the look and feel of a theme
# further. For a list of options available for each theme, see the
# documentation.
#
# html_theme_options = {}
# Add any paths that contain custom static files (such as style sheets) here,
# relative to this directory. They are copied after the builtin static files,
# so a file named "default.css" will overwrite the builtin "default.css".
html_static_path = ["_static"]
# Custom sidebar templates, must be a dictionary that maps document names
# to template names.
#
# The default sidebars (for documents that don't match any pattern) are
# defined by theme itself. Builtin themes are using these templates by
# default: ``['localtoc.html', 'relations.html', 'sourcelink.html',
# 'searchbox.html']``.
#
# html_sidebars = {}
# -- Options for HTMLHelp output ---------------------------------------------
# Output file base name for HTML help builder.
htmlhelp_basename = "MythrilClassicdoc"
# -- Options for LaTeX output ------------------------------------------------
latex_elements = {
# The paper size ('letterpaper' or 'a4paper').
#
# 'papersize': 'letterpaper',
# The font size ('10pt', '11pt' or '12pt').
#
# 'pointsize': '10pt',
# Additional stuff for the LaTeX preamble.
#
# 'preamble': '',
# Latex figure (float) alignment
#
# 'figure_align': 'htbp',
}
# Grouping the document tree into LaTeX files. List of tuples
# (source start file, target name, title,
# author, documentclass [howto, manual, or own class]).
latex_documents = [
(
master_doc,
"MythrilClassic.tex",
"Mythril Classic Documentation",
"Bernhard Mueller",
"manual",
)
]
# -- Options for manual page output ------------------------------------------
# One entry per manual page. List of tuples
# (source start file, name, description, authors, manual section).
man_pages = [
(master_doc, "mythrilclassic", "Mythril Classic Documentation", [author], 1)
]
# -- Options for Texinfo output ----------------------------------------------
# Grouping the document tree into Texinfo files. List of tuples
# (source start file, target name, title, author,
# dir menu entry, description, category)
texinfo_documents = [
(
master_doc,
"MythrilClassic",
"Mythril Classic Documentation",
author,
"MythrilClassic",
"One line description of project.",
"Miscellaneous",
)
]
# -- Options for Epub output -------------------------------------------------
# Bibliographic Dublin Core info.
epub_title = project
# The unique identifier of the text. This can be a ISBN number
# or the project homepage.
#
# epub_identifier = ''
# A unique identification for the text.
#
# epub_uid = ''
# A list of files that should not be packed into the epub file.
epub_exclude_files = ["search.html"]
# -- Extension configuration -------------------------------------------------

@ -0,0 +1,17 @@
Welcome to Mythril Classic's documentation!
===========================================
.. toctree::
:maxdepth: 3
:caption: Package Contents:
mythril
Indices and tables
==================
* :ref:`genindex`
* :ref:`modindex`
* :ref:`search`

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

@ -0,0 +1,110 @@
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:

@ -0,0 +1,85 @@
mythril.analysis package
========================
Subpackages
-----------
.. toctree::
mythril.analysis.modules
Submodules
----------
mythril.analysis.callgraph module
---------------------------------
.. automodule:: mythril.analysis.callgraph
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.ops module
---------------------------
.. automodule:: mythril.analysis.ops
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.report module
------------------------------
.. automodule:: mythril.analysis.report
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.security module
--------------------------------
.. automodule:: mythril.analysis.security
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.solver module
------------------------------
.. automodule:: mythril.analysis.solver
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.swc\_data module
---------------------------------
.. automodule:: mythril.analysis.swc_data
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.symbolic module
--------------------------------
.. automodule:: mythril.analysis.symbolic
:members:
:undoc-members:
:show-inheritance:
mythril.analysis.traceexplore module
------------------------------------
.. automodule:: mythril.analysis.traceexplore
:members:
:undoc-members:
:show-inheritance:
Module contents
---------------
.. automodule:: mythril.analysis
:members:
:undoc-members:
:show-inheritance:

@ -0,0 +1,30 @@
mythril.disassembler package
============================
Submodules
----------
mythril.disassembler.asm module
-------------------------------
.. automodule:: mythril.disassembler.asm
:members:
:undoc-members:
:show-inheritance:
mythril.disassembler.disassembly module
---------------------------------------
.. automodule:: mythril.disassembler.disassembly
:members:
:undoc-members:
:show-inheritance:
Module contents
---------------
.. automodule:: mythril.disassembler
:members:
:undoc-members:
:show-inheritance:

@ -0,0 +1,46 @@
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:

@ -0,0 +1,54 @@
mythril.ethereum.interface.rpc package
======================================
Submodules
----------
mythril.ethereum.interface.rpc.base\_client module
--------------------------------------------------
.. automodule:: mythril.ethereum.interface.rpc.base_client
:members:
:undoc-members:
:show-inheritance:
mythril.ethereum.interface.rpc.client module
--------------------------------------------
.. automodule:: mythril.ethereum.interface.rpc.client
:members:
:undoc-members:
:show-inheritance:
mythril.ethereum.interface.rpc.constants module
-----------------------------------------------
.. automodule:: mythril.ethereum.interface.rpc.constants
:members:
:undoc-members:
:show-inheritance:
mythril.ethereum.interface.rpc.exceptions module
------------------------------------------------
.. automodule:: mythril.ethereum.interface.rpc.exceptions
:members:
:undoc-members:
:show-inheritance:
mythril.ethereum.interface.rpc.utils module
-------------------------------------------
.. automodule:: mythril.ethereum.interface.rpc.utils
:members:
:undoc-members:
:show-inheritance:
Module contents
---------------
.. automodule:: mythril.ethereum.interface.rpc
:members:
:undoc-members:
:show-inheritance:

@ -0,0 +1,18 @@
mythril.ethereum.interface package
==================================
Subpackages
-----------
.. toctree::
mythril.ethereum.interface.leveldb
mythril.ethereum.interface.rpc
Module contents
---------------
.. automodule:: mythril.ethereum.interface
:members:
:undoc-members:
:show-inheritance:

@ -0,0 +1,37 @@
mythril.ethereum package
========================
Subpackages
-----------
.. toctree::
mythril.ethereum.interface
Submodules
----------
mythril.ethereum.evmcontract module
-----------------------------------
.. automodule:: mythril.ethereum.evmcontract
:members:
:undoc-members:
:show-inheritance:
mythril.ethereum.util module
----------------------------
.. automodule:: mythril.ethereum.util
:members:
:undoc-members:
:show-inheritance:
Module contents
---------------
.. automodule:: mythril.ethereum
:members:
:undoc-members:
:show-inheritance:

@ -0,0 +1,30 @@
mythril.interfaces package
==========================
Submodules
----------
mythril.interfaces.cli module
-----------------------------
.. automodule:: mythril.interfaces.cli
:members:
:undoc-members:
:show-inheritance:
mythril.interfaces.epic module
------------------------------
.. automodule:: mythril.interfaces.epic
:members:
:undoc-members:
:show-inheritance:
Module contents
---------------
.. automodule:: mythril.interfaces
:members:
:undoc-members:
:show-inheritance:

@ -0,0 +1,103 @@
mythril.laser.ethereum package
==============================
Subpackages
-----------
.. toctree::
mythril.laser.ethereum.state
mythril.laser.ethereum.strategy
mythril.laser.ethereum.transaction
Submodules
----------
mythril.laser.ethereum.call module
----------------------------------
.. automodule:: mythril.laser.ethereum.call
:members:
:undoc-members:
:show-inheritance:
mythril.laser.ethereum.cfg module
---------------------------------
.. automodule:: mythril.laser.ethereum.cfg
:members:
:undoc-members:
:show-inheritance:
mythril.laser.ethereum.evm\_exceptions module
---------------------------------------------
.. automodule:: mythril.laser.ethereum.evm_exceptions
:members:
:undoc-members:
:show-inheritance:
mythril.laser.ethereum.gas module
---------------------------------
.. automodule:: mythril.laser.ethereum.gas
: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:
mythril.laser.ethereum.natives module
-------------------------------------
.. automodule:: mythril.laser.ethereum.natives
:members:
:undoc-members:
:show-inheritance:
mythril.laser.ethereum.svm module
---------------------------------
.. automodule:: mythril.laser.ethereum.svm
:members:
:undoc-members:
:show-inheritance:
mythril.laser.ethereum.taint\_analysis module
---------------------------------------------
.. automodule:: mythril.laser.ethereum.taint_analysis
:members:
:undoc-members:
:show-inheritance:
mythril.laser.ethereum.util module
----------------------------------
.. automodule:: mythril.laser.ethereum.util
:members:
:undoc-members:
:show-inheritance:
Module contents
---------------
.. automodule:: mythril.laser.ethereum
:members:
:undoc-members:
:show-inheritance:

@ -0,0 +1,86 @@
mythril.laser.ethereum.state package
====================================
Submodules
----------
mythril.laser.ethereum.state.account module
-------------------------------------------
.. automodule:: mythril.laser.ethereum.state.account
:members:
:undoc-members:
:show-inheritance:
mythril.laser.ethereum.state.annotation module
----------------------------------------------
.. automodule:: mythril.laser.ethereum.state.annotation
:members:
:undoc-members:
:show-inheritance:
mythril.laser.ethereum.state.calldata module
--------------------------------------------
.. automodule:: mythril.laser.ethereum.state.calldata
:members:
:undoc-members:
:show-inheritance:
mythril.laser.ethereum.state.constraints module
-----------------------------------------------
.. automodule:: mythril.laser.ethereum.state.constraints
:members:
:undoc-members:
:show-inheritance:
mythril.laser.ethereum.state.environment module
-----------------------------------------------
.. automodule:: mythril.laser.ethereum.state.environment
:members:
:undoc-members:
:show-inheritance:
mythril.laser.ethereum.state.global\_state module
-------------------------------------------------
.. automodule:: mythril.laser.ethereum.state.global_state
:members:
:undoc-members:
:show-inheritance:
mythril.laser.ethereum.state.machine\_state module
--------------------------------------------------
.. automodule:: mythril.laser.ethereum.state.machine_state
:members:
:undoc-members:
:show-inheritance:
mythril.laser.ethereum.state.memory module
------------------------------------------
.. automodule:: mythril.laser.ethereum.state.memory
:members:
:undoc-members:
:show-inheritance:
mythril.laser.ethereum.state.world\_state module
------------------------------------------------
.. automodule:: mythril.laser.ethereum.state.world_state
:members:
:undoc-members:
:show-inheritance:
Module contents
---------------
.. automodule:: mythril.laser.ethereum.state
:members:
:undoc-members:
:show-inheritance:

@ -0,0 +1,22 @@
mythril.laser.ethereum.strategy package
=======================================
Submodules
----------
mythril.laser.ethereum.strategy.basic module
--------------------------------------------
.. automodule:: mythril.laser.ethereum.strategy.basic
:members:
:undoc-members:
:show-inheritance:
Module contents
---------------
.. automodule:: mythril.laser.ethereum.strategy
:members:
:undoc-members:
:show-inheritance:

@ -0,0 +1,38 @@
mythril.laser.ethereum.transaction package
==========================================
Submodules
----------
mythril.laser.ethereum.transaction.concolic module
--------------------------------------------------
.. automodule:: mythril.laser.ethereum.transaction.concolic
:members:
:undoc-members:
:show-inheritance:
mythril.laser.ethereum.transaction.symbolic module
--------------------------------------------------
.. automodule:: mythril.laser.ethereum.transaction.symbolic
:members:
:undoc-members:
:show-inheritance:
mythril.laser.ethereum.transaction.transaction\_models module
-------------------------------------------------------------
.. automodule:: mythril.laser.ethereum.transaction.transaction_models
:members:
:undoc-members:
:show-inheritance:
Module contents
---------------
.. automodule:: mythril.laser.ethereum.transaction
:members:
:undoc-members:
:show-inheritance:

@ -0,0 +1,18 @@
mythril.laser package
=====================
Subpackages
-----------
.. toctree::
mythril.laser.ethereum
mythril.laser.smt
Module contents
---------------
.. automodule:: mythril.laser
:members:
:undoc-members:
:show-inheritance:

@ -0,0 +1,38 @@
mythril.laser.smt package
=========================
Submodules
----------
mythril.laser.smt.bitvec module
-------------------------------
.. automodule:: mythril.laser.smt.bitvec
:members:
:undoc-members:
:show-inheritance:
mythril.laser.smt.bool module
-----------------------------
.. automodule:: mythril.laser.smt.bool
:members:
:undoc-members:
:show-inheritance:
mythril.laser.smt.expression module
-----------------------------------
.. automodule:: mythril.laser.smt.expression
:members:
:undoc-members:
:show-inheritance:
Module contents
---------------
.. automodule:: mythril.laser.smt
:members:
:undoc-members:
:show-inheritance:

@ -0,0 +1,51 @@
mythril package
===============
Subpackages
-----------
.. toctree::
mythril.analysis
mythril.disassembler
mythril.ethereum
mythril.interfaces
mythril.laser
mythril.solidity
mythril.support
Submodules
----------
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:
Module contents
---------------
.. automodule:: mythril
:members:
:undoc-members:
:show-inheritance:

@ -0,0 +1,22 @@
mythril.solidity package
========================
Submodules
----------
mythril.solidity.soliditycontract module
----------------------------------------
.. automodule:: mythril.solidity.soliditycontract
:members:
:undoc-members:
:show-inheritance:
Module contents
---------------
.. automodule:: mythril.solidity
:members:
:undoc-members:
:show-inheritance:

@ -0,0 +1,46 @@
mythril.support package
=======================
Submodules
----------
mythril.support.loader module
-----------------------------
.. automodule:: mythril.support.loader
:members:
:undoc-members:
:show-inheritance:
mythril.support.signatures module
---------------------------------
.. automodule:: mythril.support.signatures
:members:
:undoc-members:
:show-inheritance:
mythril.support.support\_utils module
-------------------------------------
.. automodule:: mythril.support.support_utils
:members:
:undoc-members:
:show-inheritance:
mythril.support.truffle module
------------------------------
.. automodule:: mythril.support.truffle
:members:
:undoc-members:
:show-inheritance:
Module contents
---------------
.. automodule:: mythril.support
:members:
:undoc-members:
:show-inheritance:

@ -0,0 +1,25 @@
import signal
from types import FrameType
from mythril.exceptions import OutOfTimeError
def sigalrm_handler(signum: int, frame: FrameType) -> None:
raise OutOfTimeError
def start_timeout(timeout: int) -> None:
"""
Starts a timeout
:param timeout: Time in seconds to set the timeout for
:return: None
"""
signal.signal(signal.SIGALRM, sigalrm_handler)
signal.alarm(timeout)
def disable_timeout() -> None:
"""
Ensures that the timeout is disabled
:return: None
"""
signal.alarm(0)

@ -1,3 +1,5 @@
"""This module provides helper functions for the analysis modules to deal with
call functionality."""
from typing import Union
from mythril.analysis.ops import VarType, Call, get_variable
@ -5,6 +7,11 @@ from mythril.laser.ethereum.state.global_state import GlobalState
def get_call_from_state(state: GlobalState) -> Union[Call, None]:
"""
:param state:
:return:
"""
instruction = state.get_current_instruction()
op = instruction["opcode"]

@ -1,8 +1,12 @@
"""This module contains the configuration and functions to create call
graphs."""
import re
from jinja2 import Environment, PackageLoader, select_autoescape
from mythril.laser.ethereum.svm import NodeFlags
from z3 import Z3Exception
from mythril.laser.ethereum.svm import NodeFlags
from mythril.laser.smt import simplify
default_opts = {
@ -122,6 +126,12 @@ phrack_color = {
def extract_nodes(statespace, color_map):
"""
:param statespace:
:param color_map:
:return:
"""
nodes = []
for node_key in statespace.nodes:
node = statespace.nodes[node_key]
@ -169,6 +179,11 @@ def extract_nodes(statespace, color_map):
def extract_edges(statespace):
"""
:param statespace:
:return:
"""
edges = []
for edge in statespace.edges:
if edge.condition is None:
@ -201,6 +216,14 @@ def generate_graph(
physics=False,
phrackify=False,
):
"""
:param statespace:
:param title:
:param physics:
:param phrackify:
:return:
"""
env = Environment(
loader=PackageLoader("mythril.analysis"),
autoescape=select_autoescape(["html", "xml"]),

@ -1,3 +1,6 @@
"""This module contains the base class for all user-defined detection
modules."""
import logging
from typing import List
@ -5,6 +8,11 @@ log = logging.getLogger(__name__)
class DetectionModule:
"""The base detection module.
All custom-built detection modules must inherit from this class.
"""
def __init__(
self,
name: str,
@ -25,11 +33,30 @@ class DetectionModule:
self.name,
)
self.entrypoint = entrypoint
self._issues = []
@property
def issues(self):
"""
Returns the issues
"""
return self._issues
def reset_module(self):
"""
Resets issues
"""
self._issues = []
def execute(self, statespace):
"""The entry point for execution, which is being called by Mythril.
:param statespace:
:return:
"""
raise NotImplementedError()
def __repr__(self):
def __repr__(self) -> str:
return (
"<"
"DetectionModule "

@ -1,3 +1,4 @@
"""This module contains the detection code for insecure delegate call usage."""
import re
import logging
from typing import List
@ -14,7 +15,10 @@ log = logging.getLogger(__name__)
class DelegateCallModule(DetectionModule):
"""This module detects calldata being forwarded using DELEGATECALL."""
def __init__(self):
""""""
super().__init__(
name="DELEGATECALL Usage in Fallback Function",
swc_id=DELEGATECALL_TO_UNTRUSTED_CONTRACT,
@ -22,13 +26,13 @@ class DelegateCallModule(DetectionModule):
entrypoint="callback",
pre_hooks=["DELEGATECALL"],
)
self._issues = []
@property
def issues(self) -> list:
return self._issues
def execute(self, state: GlobalState) -> list:
"""
:param state:
:return:
"""
log.debug("Executing module: DELEGATE_CALL")
self._issues.extend(_analyze_states(state))
return self.issues

@ -1,19 +1,26 @@
"""This module contains the detection code for predictable variable
dependence."""
import logging
import re
from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.analysis.ops import Call, VarType
from mythril.analysis import solver
from mythril.analysis.report import Issue
from mythril.analysis.call_helpers import get_call_from_state
from mythril.analysis.swc_data import TIMESTAMP_DEPENDENCE, PREDICTABLE_VARS_DEPENDENCE
from mythril.analysis.modules.base import DetectionModule
from mythril.analysis.ops import Call, VarType
from mythril.analysis.report import Issue
from mythril.analysis.swc_data import PREDICTABLE_VARS_DEPENDENCE, TIMESTAMP_DEPENDENCE
from mythril.exceptions import UnsatError
import logging
from mythril.laser.ethereum.state.global_state import GlobalState
log = logging.getLogger(__name__)
class PredictableDependenceModule(DetectionModule):
"""This module detects whether Ether is sent using predictable
parameters."""
def __init__(self):
""""""
super().__init__(
name="Dependence of Predictable Variables",
swc_id="{} {}".format(TIMESTAMP_DEPENDENCE, PREDICTABLE_VARS_DEPENDENCE),
@ -25,13 +32,13 @@ class PredictableDependenceModule(DetectionModule):
entrypoint="callback",
pre_hooks=["CALL", "CALLCODE", "DELEGATECALL", "STATICCALL"],
)
self._issues = []
@property
def issues(self) -> list:
return self._issues
def execute(self, state: GlobalState) -> list:
"""
:param state:
:return:
"""
log.debug("Executing module: DEPENDENCE_ON_PREDICTABLE_VARS")
self._issues.extend(_analyze_states(state))
return self.issues
@ -41,6 +48,11 @@ detector = PredictableDependenceModule()
def _analyze_states(state: GlobalState) -> list:
"""
:param state:
:return:
"""
issues = []
call = get_call_from_state(state)
if call is None:
@ -149,12 +161,15 @@ def _analyze_states(state: GlobalState) -> list:
r = re.search(r"storage_([a-z0-9_&^]+)", str(constraint))
if r: # block.blockhash(storage_0)
"""
We actually can do better here by adding a constraint blockhash_block_storage_0 == 0
and checking model satisfiability. When this is done, severity can be raised
from 'Informational' to 'Warning'.
Checking that storage at given index can be tainted is not necessary, since it usually contains
block.number of the 'commit' transaction in commit-reveal workflow.
"""We actually can do better here by adding a constraint
blockhash_block_storage_0 == 0 and checking model
satisfiability.
When this is done, severity can be raised from
'Informational' to 'Warning'. Checking that storage
at given index can be tainted is not necessary,
since it usually contains block.number of the
'commit' transaction in commit-reveal workflow.
"""
index = r.group(1)
@ -183,6 +198,11 @@ def _analyze_states(state: GlobalState) -> list:
def solve(call: Call) -> bool:
"""
:param call:
:return:
"""
try:
model = solver.get_model(call.node.constraints)
log.debug("[DEPENDENCE_ON_PREDICTABLE_VARS] MODEL: " + str(model))

@ -1,3 +1,4 @@
"""This module contains the detection code for deprecated op codes."""
from mythril.analysis.report import Issue
from mythril.analysis.swc_data import DEPRICATED_FUNCTIONS_USAGE
from mythril.analysis.modules.base import DetectionModule
@ -12,6 +13,11 @@ Check for usage of deprecated opcodes
def _analyze_state(state):
"""
:param state:
:return:
"""
node = state.node
instruction = state.get_current_instruction()
@ -51,23 +57,26 @@ def _analyze_state(state):
class DeprecatedOperationsModule(DetectionModule):
"""This module checks for the usage of deprecated op codes."""
def __init__(self):
""""""
super().__init__(
name="Deprecated Operations",
swc_id=DEPRICATED_FUNCTIONS_USAGE,
description=(DESCRIPTION),
description=DESCRIPTION,
entrypoint="callback",
pre_hooks=["ORIGIN", "CALLCODE"],
)
self._issues = []
def execute(self, state: GlobalState):
"""
:param state:
:return:
"""
self._issues.extend(_analyze_state(state))
return self.issues
@property
def issues(self):
return self._issues
detector = DeprecatedOperationsModule()

@ -1,13 +1,15 @@
from mythril.analysis.ops import *
"""This module contains the detection code for unauthorized ether
withdrawal."""
import logging
from copy import copy
from mythril.analysis import solver
from mythril.analysis.modules.base import DetectionModule
from mythril.analysis.report import Issue
from mythril.analysis.swc_data import UNPROTECTED_ETHER_WITHDRAWAL
from mythril.analysis.modules.base import DetectionModule
from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.exceptions import UnsatError
from mythril.laser.smt import symbol_factory, UGT, Sum, BVAddNoOverflow
import logging
from copy import copy
from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.laser.smt import UGT, BVAddNoOverflow, Sum, symbol_factory
log = logging.getLogger(__name__)
@ -25,59 +27,12 @@ An issue is reported if:
"""
def _analyze_state(state):
instruction = state.get_current_instruction()
node = state.node
if instruction["opcode"] != "CALL":
return []
call_value = state.mstate.stack[-3]
target = state.mstate.stack[-2]
eth_sent_total = symbol_factory.BitVecVal(0, 256)
constraints = copy(node.constraints)
for tx in state.world_state.transaction_sequence:
if tx.caller == 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF:
# There's sometimes no overflow check on balances added.
# But we don't care about attacks that require more 2^^256 ETH to be sent.
constraints += [BVAddNoOverflow(eth_sent_total, tx.call_value, False)]
eth_sent_total = Sum(eth_sent_total, tx.call_value)
constraints += [UGT(call_value, eth_sent_total), target == state.environment.sender]
try:
transaction_sequence = solver.get_transaction_sequence(state, constraints)
debug = str(transaction_sequence)
issue = Issue(
contract=node.contract_name,
function_name=node.function_name,
address=instruction["address"],
swc_id=UNPROTECTED_ETHER_WITHDRAWAL,
title="Ether thief",
_type="Warning",
bytecode=state.environment.code.bytecode,
description="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.",
debug=debug,
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
)
except UnsatError:
log.debug("[ETHER_THIEF] no model found")
return []
return [issue]
class EtherThief(DetectionModule):
"""This module search for cases where Ether can be withdrawn to a user-
specified address."""
def __init__(self):
""""""
super().__init__(
name="Ether Thief",
swc_id=UNPROTECTED_ETHER_WITHDRAWAL,
@ -85,15 +40,86 @@ class EtherThief(DetectionModule):
entrypoint="callback",
pre_hooks=["CALL"],
)
self._issues = []
self._cache_addresses = {}
def reset_module(self):
"""
Resets the module by clearing everything
:return:
"""
super().reset_module()
self._cache_addresses = {}
def execute(self, state: GlobalState):
self._issues.extend(_analyze_state(state))
"""
:param state:
:return:
"""
self._issues.extend(self._analyze_state(state))
return self.issues
@property
def issues(self):
return self._issues
def _analyze_state(self, state):
"""
:param state:
:return:
"""
instruction = state.get_current_instruction()
node = state.node
if instruction["opcode"] != "CALL":
return []
address = instruction["address"]
if self._cache_addresses.get(address, False):
return []
call_value = state.mstate.stack[-3]
target = state.mstate.stack[-2]
eth_sent_total = symbol_factory.BitVecVal(0, 256)
constraints = copy(node.constraints)
for tx in state.world_state.transaction_sequence:
if tx.caller == 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF:
# There's sometimes no overflow check on balances added.
# But we don't care about attacks that require more 2^^256 ETH to be sent.
constraints += [BVAddNoOverflow(eth_sent_total, tx.call_value, False)]
eth_sent_total = Sum(eth_sent_total, tx.call_value)
constraints += [
UGT(call_value, eth_sent_total),
target == state.environment.sender,
]
try:
transaction_sequence = solver.get_transaction_sequence(state, constraints)
debug = str(transaction_sequence)
issue = Issue(
contract=node.contract_name,
function_name=node.function_name,
address=address,
swc_id=UNPROTECTED_ETHER_WITHDRAWAL,
title="Ether thief",
_type="Warning",
bytecode=state.environment.code.bytecode,
description="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.",
debug=debug,
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
)
except UnsatError:
log.debug("[ETHER_THIEF] no model found")
return []
self._cache_addresses[address] = True
return [issue]
detector = EtherThief()

@ -1,16 +1,22 @@
"""This module contains the detection code for reachable exceptions."""
import logging
from mythril.analysis import solver
from mythril.analysis.modules.base import DetectionModule
from mythril.analysis.report import Issue
from mythril.analysis.swc_data import ASSERT_VIOLATION
from mythril.exceptions import UnsatError
from mythril.analysis import solver
from mythril.analysis.modules.base import DetectionModule
import logging
from mythril.laser.ethereum.state.global_state import GlobalState
log = logging.getLogger(__name__)
def _analyze_state(state) -> list:
"""
:param state:
:return:
"""
log.info("Exceptions module: found ASSERT_FAIL instruction")
node = state.node
@ -50,7 +56,10 @@ def _analyze_state(state) -> list:
class ReachableExceptionsModule(DetectionModule):
""""""
def __init__(self):
""""""
super().__init__(
name="Reachable Exceptions",
swc_id=ASSERT_VIOLATION,
@ -58,15 +67,15 @@ class ReachableExceptionsModule(DetectionModule):
entrypoint="callback",
pre_hooks=["ASSERT_FAIL"],
)
self._issues = []
def execute(self, state: GlobalState) -> list:
"""
:param state:
:return:
"""
self._issues.extend(_analyze_state(state))
return self.issues
@property
def issues(self) -> list:
return self._issues
detector = ReachableExceptionsModule()

@ -1,7 +1,10 @@
from mythril.analysis.report import Issue
"""This module contains the detection code for potentially insecure low-level
calls."""
from mythril.analysis import solver
from mythril.analysis.swc_data import REENTRANCY
from mythril.analysis.modules.base import DetectionModule
from mythril.analysis.report import Issue
from mythril.laser.smt import UGT, symbol_factory
from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.exceptions import UnsatError
@ -19,7 +22,11 @@ an informational issue.
def _analyze_state(state):
"""
:param state:
:return:
"""
node = state.node
gas = state.mstate.stack[-1]
to = state.mstate.stack[-2]
@ -91,23 +98,27 @@ def _analyze_state(state):
class ExternalCalls(DetectionModule):
"""This module searches for low level calls (e.g. call.value()) that
forward all gas to the callee."""
def __init__(self):
""""""
super().__init__(
name="External calls",
swc_id=REENTRANCY,
description=(DESCRIPTION),
description=DESCRIPTION,
entrypoint="callback",
pre_hooks=["CALL"],
)
self._issues = []
def execute(self, state: GlobalState):
"""
:param state:
:return:
"""
self._issues.extend(_analyze_state(state))
return self.issues
@property
def issues(self):
return self._issues
detector = ExternalCalls()

@ -1,3 +1,5 @@
"""This module contains the detection code for integer overflows and
underflows."""
from mythril.analysis import solver
from mythril.analysis.report import Issue
from mythril.analysis.swc_data import INTEGER_OVERFLOW_AND_UNDERFLOW
@ -30,7 +32,10 @@ class OverUnderflowAnnotation:
class IntegerOverflowUnderflowModule(DetectionModule):
"""This module searches for integer over- and underflows."""
def __init__(self):
""""""
super().__init__(
name="Integer Overflow and Underflow",
swc_id=INTEGER_OVERFLOW_AND_UNDERFLOW,
@ -42,24 +47,34 @@ class IntegerOverflowUnderflowModule(DetectionModule):
entrypoint="callback",
pre_hooks=["ADD", "MUL", "SUB", "SSTORE", "JUMPI"],
)
self.overflow_cache = {}
self.underflow_cache = {}
self._issues = []
self._overflow_cache = {}
self._underflow_cache = {}
@property
def issues(self):
return self._issues
def reset_module(self):
"""
Resets the module
:return:
"""
super().reset_module()
self._overflow_cache = {}
self._underflow_cache = {}
def execute(self, state: GlobalState):
address = state.get_current_instruction()["address"]
has_overflow = self.overflow_cache.get(address, False)
has_underflow = self.underflow_cache.get(address, False)
"""Executes analysis module for integer underflow and integer overflow.
if state.get_current_instruction()["opcode"] == "ADD" and not has_overflow:
:param state: Statespace to analyse
:return: Found issues
"""
address = state.get_current_instruction()["address"]
has_overflow = self._overflow_cache.get(address, False)
has_underflow = self._underflow_cache.get(address, False)
if has_overflow or has_underflow:
return
if state.get_current_instruction()["opcode"] == "ADD":
self._handle_add(state)
elif state.get_current_instruction()["opcode"] == "MUL" and not has_overflow:
elif state.get_current_instruction()["opcode"] == "MUL":
self._handle_mul(state)
elif state.get_current_instruction()["opcode"] == "SUB" and not has_underflow:
elif state.get_current_instruction()["opcode"] == "SUB":
self._handle_sub(state)
elif state.get_current_instruction()["opcode"] == "SSTORE":
self._handle_sstore(state)
@ -129,7 +144,6 @@ class IntegerOverflowUnderflowModule(DetectionModule):
if not isinstance(value, Expression):
return
for annotation in value.annotations:
if not isinstance(annotation, OverUnderflowAnnotation):
continue
@ -157,14 +171,14 @@ class IntegerOverflowUnderflowModule(DetectionModule):
)
address = ostate.get_current_instruction()["address"]
if annotation.operator == "subtraction" and self.underflow_cache.get(
if annotation.operator == "subtraction" and self._underflow_cache.get(
address, False
):
return
if annotation.operator != "subtraction" and self.overflow_cache.get(
continue
if annotation.operator != "subtraction" and self._overflow_cache.get(
address, False
):
return
continue
try:
issue.debug = str(
@ -173,11 +187,11 @@ class IntegerOverflowUnderflowModule(DetectionModule):
)
)
except UnsatError:
return
continue
if annotation.operator == "subtraction":
self.underflow_cache[address] = True
self._underflow_cache[address] = True
else:
self.overflow_cache[address] = True
self._overflow_cache[address] = True
self._issues.append(issue)
@ -190,30 +204,44 @@ class IntegerOverflowUnderflowModule(DetectionModule):
continue
ostate = annotation.overflowing_state
node = ostate.node
title = (
"Integer Underflow"
if annotation.operator == "subtraction"
else "Integer Overflow"
)
issue = Issue(
contract=node.contract_name,
function_name=node.function_name,
address=ostate.get_current_instruction()["address"],
swc_id=INTEGER_OVERFLOW_AND_UNDERFLOW,
bytecode=ostate.environment.code.bytecode,
title="Integer Overflow",
title=title,
_type="Warning",
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
)
issue.description = "This binary {} operation can result in integer overflow.\n".format(
annotation.operator
issue.description = "This binary {} operation can result in {}.\n".format(
annotation.operator, title.lower()
)
address = ostate.get_current_instruction()["address"]
print(
self._overflow_cache,
self._underflow_cache,
address,
issue.address,
[_issue.address for _issue in self._issues],
)
if annotation.operator == "subtraction" and self.underflow_cache.get(
if annotation.operator == "subtraction" and self._underflow_cache.get(
address, False
):
return
if annotation.operator != "subtraction" and self.overflow_cache.get(
continue
if annotation.operator != "subtraction" and self._overflow_cache.get(
address, False
):
return
continue
try:
issue.debug = str(
@ -222,13 +250,12 @@ class IntegerOverflowUnderflowModule(DetectionModule):
)
)
except UnsatError:
return
continue
if annotation.operator == "subtraction":
self.underflow_cache[address] = True
self._underflow_cache[address] = True
else:
self.overflow_cache[address] = True
self._overflow_cache[address] = True
self._issues.append(issue)
@staticmethod

@ -1,3 +1,5 @@
"""This module contains the detection code to find multiple sends occurring in
a single transaction."""
from copy import copy
from mythril.analysis.report import Issue
@ -22,7 +24,10 @@ class MultipleSendsAnnotation(StateAnnotation):
class MultipleSendsModule(DetectionModule):
"""This module checks for multiple sends in a single transaction."""
def __init__(self):
""""""
super().__init__(
name="Multiple Sends",
swc_id=MULTIPLE_SENDS,
@ -37,16 +42,11 @@ class MultipleSendsModule(DetectionModule):
"STOP",
],
)
self._issues = []
def execute(self, state: GlobalState):
self._issues.extend(_analyze_state(state))
return self.issues
@property
def issues(self):
return self._issues
def _analyze_state(state: GlobalState):
"""

@ -59,23 +59,26 @@ def _analyze_state(state):
class SuicideModule(DetectionModule):
"""This module checks if the contact can be 'accidentally' killed by
anyone."""
def __init__(self):
super().__init__(
name="Unprotected Suicide",
swc_id=UNPROTECTED_SELFDESTRUCT,
description=(DESCRIPTION),
description=DESCRIPTION,
entrypoint="callback",
pre_hooks=["SUICIDE"],
)
self._issues = []
def execute(self, state: GlobalState):
"""
:param state:
:return:
"""
self._issues.extend(_analyze_state(state))
return self.issues
@property
def issues(self):
return self._issues
detector = SuicideModule()

@ -1,19 +1,22 @@
"""This module contains the detection code to find the existence of transaction
order dependence."""
import copy
import logging
import re
import copy
from mythril.analysis import solver
from mythril.analysis.modules.base import DetectionModule
from mythril.analysis.ops import *
from mythril.analysis.report import Issue
from mythril.analysis.swc_data import TX_ORDER_DEPENDENCE
from mythril.analysis.modules.base import DetectionModule
from mythril.exceptions import UnsatError
log = logging.getLogger(__name__)
class TxOrderDependenceModule(DetectionModule):
"""This module finds the existence of transaction order dependence."""
def __init__(self):
super().__init__(
name="Transaction Order Dependence",
@ -27,7 +30,11 @@ class TxOrderDependenceModule(DetectionModule):
)
def execute(self, statespace):
""" Executes the analysis module"""
"""Executes the analysis module.
:param statespace:
:return:
"""
log.debug("Executing module: TOD")
issues = []
@ -66,22 +73,34 @@ class TxOrderDependenceModule(DetectionModule):
return issues
# TODO: move to __init__ or util module
def _get_states_with_opcode(self, statespace, opcode):
""" Gets all (state, node) tuples in statespace with opcode"""
@staticmethod
def _get_states_with_opcode(statespace, opcode):
"""Gets all (state, node) tuples in statespace with opcode.
:param statespace:
:param opcode:
"""
for k in statespace.nodes:
node = statespace.nodes[k]
for state in node.states:
if state.get_current_instruction()["opcode"] == opcode:
yield state, node
def _dependent_on_storage(self, expression):
""" Checks if expression is dependent on a storage symbol and returns the influencing storages"""
@staticmethod
def _dependent_on_storage(expression):
"""Checks if expression is dependent on a storage symbol and returns
the influencing storages.
:param expression:
:return:
"""
pattern = re.compile(r"storage_[a-z0-9_&^]*[0-9]+")
return pattern.findall(str(simplify(expression)))
def _get_storage_variable(self, storage, state):
"""
Get storage z3 object given storage name and the state
@staticmethod
def _get_storage_variable(storage, state):
"""Get storage z3 object given storage name and the state.
:param storage: storage name example: storage_0
:param state: state to retrieve the variable from
:return: z3 object representing storage
@ -93,7 +112,12 @@ class TxOrderDependenceModule(DetectionModule):
return None
def _can_change(self, constraints, variable):
""" Checks if the variable can change given some constraints """
"""Checks if the variable can change given some constraints.
:param constraints:
:param variable:
:return:
"""
_constraints = copy.deepcopy(constraints)
try:
model = solver.get_model(_constraints)
@ -109,7 +133,11 @@ class TxOrderDependenceModule(DetectionModule):
return False
def _get_influencing_storages(self, call):
""" Examines a Call object and returns an iterator of all storages that influence the call value or direction"""
"""Examines a Call object and returns an iterator of all storages that
influence the call value or direction.
:param call:
"""
state = call.state
node = call.node
@ -129,7 +157,11 @@ class TxOrderDependenceModule(DetectionModule):
yield storage
def _get_influencing_sstores(self, statespace, interesting_storages):
""" Gets sstore (state, node) tuples that write to interesting_storages"""
"""Gets sstore (state, node) tuples that write to interesting_storages.
:param statespace:
:param interesting_storages:
"""
for sstore_state, node in self._get_states_with_opcode(statespace, "SSTORE"):
index, value = sstore_state.mstate.stack[-1], sstore_state.mstate.stack[-2]
try:
@ -142,9 +174,12 @@ class TxOrderDependenceModule(DetectionModule):
yield sstore_state, node
# TODO: remove
def _try_constraints(self, constraints, new_constraints):
"""
Tries new constraints
@staticmethod
def _try_constraints(constraints, new_constraints):
"""Tries new constraints.
:param constraints:
:param new_constraints:
:return Model if satisfiable otherwise None
"""
_constraints = copy.deepcopy(constraints)

@ -1,3 +1,5 @@
"""This module contains detection code to find occurrences of calls whose
return value remains unchecked."""
from copy import copy
from mythril.analysis import solver
@ -24,6 +26,8 @@ class UncheckedRetvalAnnotation(StateAnnotation):
class UncheckedRetvalModule(DetectionModule):
"""A detection module to test whether CALL return value is checked."""
def __init__(self):
super().__init__(
name="Unchecked Return Value",
@ -41,16 +45,16 @@ class UncheckedRetvalModule(DetectionModule):
pre_hooks=["STOP", "RETURN"],
post_hooks=["CALL", "DELEGATECALL", "STATICCALL", "CALLCODE"],
)
self._issues = []
def execute(self, state: GlobalState) -> list:
"""
:param state:
:return:
"""
self._issues.extend(_analyze_state(state))
return self.issues
@property
def issues(self):
return self._issues
def _analyze_state(state: GlobalState) -> list:
instruction = state.get_current_instruction()

@ -1,23 +1,44 @@
from mythril.laser.smt import simplify
"""This module contains various helper methods for dealing with EVM
operations."""
from enum import Enum
from mythril.laser.ethereum import util
from mythril.laser.smt import simplify
class VarType(Enum):
"""An enum denoting whether a value is symbolic or concrete."""
SYMBOLIC = 1
CONCRETE = 2
class Variable:
"""The representation of a variable with value and type."""
def __init__(self, val, _type):
"""
:param val:
:param _type:
"""
self.val = val
self.type = _type
def __str__(self):
"""
:return:
"""
return str(self.val)
def get_variable(i):
"""
:param i:
:return:
"""
try:
return Variable(util.get_concrete_int(i), VarType.CONCRETE)
except TypeError:
@ -25,13 +46,23 @@ def get_variable(i):
class Op:
"""The base type for operations referencing current node and state."""
def __init__(self, node, state, state_index):
"""
:param node:
:param state:
:param state_index:
"""
self.node = node
self.state = state
self.state_index = state_index
class Call(Op):
"""The representation of a CALL operation."""
def __init__(
self,
node,
@ -43,7 +74,17 @@ class Call(Op):
value=Variable(0, VarType.CONCRETE),
data=None,
):
"""
:param node:
:param state:
:param state_index:
:param _type:
:param to:
:param gas:
:param value:
:param data:
"""
super().__init__(node, state, state_index)
self.to = to
self.gas = gas
@ -53,6 +94,8 @@ class Call(Op):
class SStore(Op):
"""The respresentation of an SSTORE operation."""
def __init__(self, node, state, state_index, value):
super().__init__(node, state, state_index)
self.value = value

@ -1,3 +1,4 @@
"""This module provides classes that make up an issue report."""
import logging
import json
import operator
@ -9,6 +10,8 @@ log = logging.getLogger(__name__)
class Issue:
"""Representation of an issue and its location."""
def __init__(
self,
contract,
@ -22,7 +25,19 @@ class Issue:
description="",
debug="",
):
"""
:param contract:
:param function_name:
:param address:
:param swc_id:
:param title:
:param bytecode:
:param gas_used:
:param _type:
:param description:
:param debug:
"""
self.title = title
self.contract = contract
self.function = function_name
@ -48,7 +63,10 @@ class Issue:
@property
def as_dict(self):
"""
:return:
"""
issue = {
"title": self.title,
"swc-id": self.swc_id,
@ -72,6 +90,10 @@ class Issue:
return issue
def add_code_info(self, contract):
"""
:param contract:
"""
if self.address:
codeinfo = contract.get_source_info(
self.address, constructor=(self.function == "constructor")
@ -82,25 +104,43 @@ class Issue:
class Report:
"""A report containing the content of multiple issues."""
environment = Environment(
loader=PackageLoader("mythril.analysis"), trim_blocks=True
)
def __init__(self, verbose=False):
"""
:param verbose:
"""
self.issues = {}
self.verbose = verbose
pass
def sorted_issues(self):
"""
:return:
"""
issue_list = [issue.as_dict for key, issue in self.issues.items()]
return sorted(issue_list, key=operator.itemgetter("address", "title"))
def append_issue(self, issue):
"""
:param issue:
"""
m = hashlib.md5()
m.update((issue.contract + str(issue.address) + issue.title).encode("utf-8"))
self.issues[m.digest()] = issue
def as_text(self):
"""
:return:
"""
name = self._file_name()
template = Report.environment.get_template("report_as_text.jinja2")
return template.render(
@ -108,11 +148,18 @@ class Report:
)
def as_json(self):
"""
:return:
"""
result = {"success": True, "error": None, "issues": self.sorted_issues()}
return json.dumps(result, sort_keys=True)
def as_swc_standard_format(self):
""" Format defined for integration and correlation"""
"""Format defined for integration and correlation.
:return:
"""
result = {
"issues": [
{
@ -126,6 +173,10 @@ class Report:
return json.dumps(result, sort_keys=True)
def as_markdown(self):
"""
:return:
"""
filename = self._file_name()
template = Report.environment.get_template("report_as_markdown.jinja2")
return template.render(
@ -133,5 +184,9 @@ class Report:
)
def _file_name(self):
"""
:return:
"""
if len(self.issues.values()) > 0:
return list(self.issues.values())[0].filename

@ -1,4 +1,5 @@
from mythril.analysis.modules.integer import IntegerOverflowUnderflowModule
"""This module contains functionality for hooking in detection modules and
executing them."""
from collections import defaultdict
from ethereum.opcodes import opcodes
from mythril.analysis import modules
@ -12,12 +13,10 @@ OPCODE_LIST = [c[0] for _, c in opcodes.items()]
def reset_callback_modules():
"""Clean the issue records of every callback-based module."""
modules = get_detection_modules("callback")
for module in modules:
module.detector._issues = []
if isinstance(module.detector, IntegerOverflowUnderflowModule):
module.detector.overflow_cache = {}
module.detector.underflow_cache = {}
module.detector.reset_module()
def get_detection_module_hooks(modules, hook_type="pre"):
@ -29,6 +28,7 @@ def get_detection_module_hooks(modules, hook_type="pre"):
if hook_type == "pre"
else module.detector.post_hooks
)
for op_code in map(lambda x: x.upper(), hooks):
if op_code in OPCODE_LIST:
hook_dict[op_code].append(module.detector.execute)
@ -46,6 +46,12 @@ def get_detection_module_hooks(modules, hook_type="pre"):
def get_detection_modules(entrypoint, include_modules=()):
"""
:param entrypoint:
:param include_modules:
:return:
"""
include_modules = list(include_modules)
_modules = []
@ -69,6 +75,12 @@ def get_detection_modules(entrypoint, include_modules=()):
def fire_lasers(statespace, module_names=()):
"""
:param statespace:
:param module_names:
:return:
"""
log.info("Starting analysis")
issues = []

@ -1,3 +1,4 @@
"""This module contains analysis module helpers to solve path constraints."""
from z3 import sat, unknown, FuncInterp
import z3
@ -12,6 +13,13 @@ log = logging.getLogger(__name__)
def get_model(constraints, minimize=(), maximize=()):
"""
:param constraints:
:param minimize:
:param maximize:
:return:
"""
s = Optimize()
s.set_timeout(100000)
@ -37,7 +45,11 @@ def get_model(constraints, minimize=(), maximize=()):
def pretty_print_model(model):
"""
:param model:
:return:
"""
ret = ""
for d in model.decls():
@ -57,13 +69,10 @@ def pretty_print_model(model):
def get_transaction_sequence(global_state, constraints):
"""
Generate concrete transaction sequence
"""Generate concrete transaction sequence.
:param global_state: GlobalState to generate transaction sequence for
:param constraints: list of constraints used to generate transaction sequence
:param caller: address of caller
:param max_callvalue: maximum callvalue for a transaction
"""
transaction_sequence = global_state.world_state.transaction_sequence

@ -1,3 +1,5 @@
"""This module maps SWC IDs to their registry equivalents."""
DEFAULT_FUNCTION_VISIBILITY = "100"
INTEGER_OVERFLOW_AND_UNDERFLOW = "101"
OUTDATED_COMPILER_VERSION = "102"

@ -1,21 +1,25 @@
"""This module contains a wrapper around LASER for extended analysis
purposes."""
import copy
from mythril.analysis.security import get_detection_module_hooks, get_detection_modules
from mythril.laser.ethereum import svm
from mythril.laser.ethereum.state.account import Account
from mythril.solidity.soliditycontract import SolidityContract, EVMContract
import copy
from .ops import get_variable, SStore, Call, VarType
from mythril.laser.ethereum.strategy.basic import (
DepthFirstSearchStrategy,
BreadthFirstSearchStrategy,
DepthFirstSearchStrategy,
ReturnRandomNaivelyStrategy,
ReturnWeightedRandomStrategy,
)
from mythril.solidity.soliditycontract import EVMContract, SolidityContract
from .ops import Call, SStore, VarType, get_variable
class SymExecWrapper:
"""Wrapper class for the LASER Symbolic virtual machine.
"""
Wrapper class for the LASER Symbolic virtual machine. Symbolically executes the code and does a bit of pre-analysis for convenience.
Symbolically executes the code and does a bit of pre-analysis for
convenience.
"""
def __init__(
@ -31,7 +35,18 @@ class SymExecWrapper:
modules=(),
compulsory_statespace=True,
):
"""
:param contract:
:param address:
:param strategy:
:param dynloader:
:param max_depth:
:param execution_timeout:
:param create_timeout:
:param transaction_count:
:param modules:
"""
if strategy == "dfs":
s_strategy = DepthFirstSearchStrategy
elif strategy == "bfs":
@ -191,7 +206,12 @@ class SymExecWrapper:
state_index += 1
def find_storage_write(self, address, index):
"""
:param address:
:param index:
:return:
"""
# Find an SSTOR not constrained by caller that writes to storage index "index"
try:

@ -1,3 +1,5 @@
"""This module provides a function to convert a state space into a set of state
nodes and transition edges."""
from z3 import Z3Exception
from mythril.laser.smt import simplify
from mythril.laser.ethereum.svm import NodeFlags
@ -48,6 +50,11 @@ colors = [
def get_serializable_statespace(statespace):
"""
:param statespace:
:return:
"""
nodes = []
edges = []
@ -78,6 +85,11 @@ def get_serializable_statespace(statespace):
color = color_map[node.get_cfg_dict()["contract_name"]]
def get_state_accounts(node_state):
"""
:param node_state:
:return:
"""
state_accounts = []
for key in node_state.accounts:
account = node_state.accounts[key].as_dict

@ -1,16 +1,19 @@
"""This module contains various helper classes and functions to deal with EVM
code disassembly."""
import re
from collections import Generator
from ethereum.opcodes import opcodes
regex_PUSH = re.compile("^PUSH(\d*)$")
regex_PUSH = re.compile(r"^PUSH(\d*)$")
# Additional mnemonic to catch failed assertions
opcodes[254] = ["ASSERT_FAIL", 0, 0, 0]
class EvmInstruction:
""" Model to hold the information of the disassembly """
"""Model to hold the information of the disassembly."""
def __init__(self, address, op_code, argument=None):
self.address = address
@ -18,6 +21,10 @@ class EvmInstruction:
self.argument = argument
def to_dict(self) -> dict:
"""
:return:
"""
result = {"address": self.address, "opcode": self.op_code}
if self.argument:
result["argument"] = self.argument
@ -25,6 +32,11 @@ class EvmInstruction:
def instruction_list_to_easm(instruction_list: list) -> str:
"""Convert a list of instructions into an easm op code string.
:param instruction_list:
:return:
"""
result = ""
for instruction in instruction_list:
@ -37,6 +49,11 @@ def instruction_list_to_easm(instruction_list: list) -> str:
def get_opcode_from_name(operation_name: str) -> int:
"""Get an op code based on its name.
:param operation_name:
:return:
"""
for op_code, value in opcodes.items():
if operation_name == value[0]:
return op_code
@ -44,10 +61,10 @@ def get_opcode_from_name(operation_name: str) -> int:
def find_op_code_sequence(pattern: list, instruction_list: list) -> Generator:
"""
Returns all indices in instruction_list that point to instruction sequences following a pattern
:param pattern: The pattern to look for.
Example: [["PUSH1", "PUSH2"], ["EQ"]] where ["PUSH1", "EQ"] satisfies the pattern
"""Returns all indices in instruction_list that point to instruction
sequences following a pattern.
:param pattern: The pattern to look for, e.g. [["PUSH1", "PUSH2"], ["EQ"]] where ["PUSH1", "EQ"] satisfies pattern
:param instruction_list: List of instructions to look in
:return: Indices to the instruction sequences
"""
@ -57,10 +74,9 @@ def find_op_code_sequence(pattern: list, instruction_list: list) -> Generator:
def is_sequence_match(pattern: list, instruction_list: list, index: int) -> bool:
"""
Checks if the instructions starting at index follow a pattern
:param pattern: List of lists describing a pattern.
Example: [["PUSH1", "PUSH2"], ["EQ"]] where ["PUSH1", "EQ"] satisfies the pattern
"""Checks if the instructions starting at index follow a pattern.
:param pattern: List of lists describing a pattern, e.g. [["PUSH1", "PUSH2"], ["EQ"]] where ["PUSH1", "EQ"] satisfies pattern
:param instruction_list: List of instructions
:param index: Index to check for
:return: Pattern matched
@ -75,7 +91,11 @@ def is_sequence_match(pattern: list, instruction_list: list, index: int) -> bool
def disassemble(bytecode: str) -> list:
"""Disassembles evm bytecode and returns a list of instructions"""
"""Disassembles evm bytecode and returns a list of instructions.
:param bytecode:
:return:
"""
instruction_list = []
address = 0
length = len(bytecode)

@ -1,20 +1,25 @@
"""This module contains the class used to represent disassembly code."""
from mythril.ethereum import util
from mythril.disassembler import asm
from mythril.support.signatures import SignatureDB
class Disassembly(object):
"""
Disassembly class
"""Disassembly class.
Stores bytecode, and its disassembly.
Additionally it will gather the following information on the existing functions in the disassembled code:
- function hashes
- function name to entry point mapping
- function entry point to function name mapping
- function hashes
- function name to entry point mapping
- function entry point to function name mapping
"""
def __init__(self, code: str, enable_online_lookup: bool = False):
"""
:param code:
:param enable_online_lookup:
"""
self.bytecode = code
self.instruction_list = asm.disassemble(util.safe_decode(code))
@ -42,16 +47,21 @@ class Disassembly(object):
self.address_to_function_name[jump_target] = function_name
def get_easm(self):
"""
:return:
"""
return asm.instruction_list_to_easm(self.instruction_list)
def get_function_info(
index: int, instruction_list: list, signature_database: SignatureDB
) -> (str, int, str):
"""
Finds the function information for a call table entry
Solidity uses the first 4 bytes of the calldata to indicate which function the message call should execute
The generated code that directs execution to the correct function looks like this:
"""Finds the function information for a call table entry Solidity uses the
first 4 bytes of the calldata to indicate which function the message call
should execute The generated code that directs execution to the correct
function looks like this:
- PUSH function_hash
- EQ
- PUSH entry_point

@ -1,18 +1,31 @@
from mythril.disassembler.disassembly import Disassembly
from ethereum import utils
import persistent
"""This module contains the class representing EVM contracts, aka Smart
Contracts."""
import re
import persistent
from ethereum import utils
from mythril.disassembler.disassembly import Disassembly
class EVMContract(persistent.Persistent):
"""This class represents an address with associated code (Smart
Contract)."""
def __init__(
self, code="", creation_code="", name="Unknown", enable_online_lookup=False
):
"""Create a new contract.
# Workaround: We currently do not support compile-time linking.
# Dynamic contract addresses of the format __[contract-name]_____________ are replaced with a generic address
# Apply this for creation_code & code
Workaround: We currently do not support compile-time linking.
Dynamic contract addresses of the format __[contract-name]_____________ are replaced with a generic address
Apply this for creation_code & code
:param code:
:param creation_code:
:param name:
:param enable_online_lookup:
"""
creation_code = re.sub(r"(_{2}.{38})", "aa" * 20, creation_code)
code = re.sub(r"(_{2}.{38})", "aa" * 20, code)
@ -25,7 +38,10 @@ class EVMContract(persistent.Persistent):
)
def as_dict(self):
"""
:return:
"""
return {
"name": self.name,
"code": self.code,
@ -34,15 +50,25 @@ class EVMContract(persistent.Persistent):
}
def get_easm(self):
"""
:return:
"""
return self.disassembly.get_easm()
def get_creation_easm(self):
"""
:return:
"""
return self.creation_disassembly.get_easm()
def matches_expression(self, expression):
"""
:param expression:
:return:
"""
str_eval = ""
easm_code = None

@ -1,11 +1,18 @@
"""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
from mythril import ethereum
import time
from ethereum.messages import Log
import rlp
from rlp.sedes import big_endian_int, binary
from ethereum import utils
from ethereum.utils import hash32, address, int256
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__)
@ -15,17 +22,27 @@ 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
: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
@ -36,9 +53,7 @@ class CountableList(object):
class ReceiptForStorage(rlp.Serializable):
"""
Receipt format stored in levelDB
"""
"""Receipt format stored in levelDB."""
fields = [
("state_root", binary),
@ -52,9 +67,7 @@ class ReceiptForStorage(rlp.Serializable):
class AccountIndexer(object):
"""
Updates address index
"""
"""Updates address index."""
def __init__(self, ethDB):
self.db = ethDB
@ -64,9 +77,8 @@ class AccountIndexer(object):
self.updateIfNeeded()
def get_contract_by_hash(self, contract_hash):
"""
get mapped contract_address by its hash, if not found try indexing
"""
"""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
@ -75,9 +87,7 @@ class AccountIndexer(object):
raise AddressNotFoundError
def _process(self, startblock):
"""
Processesing method
"""
"""Processesing method."""
log.debug("Processing blocks %d to %d" % (startblock, startblock + BATCH_SIZE))
addresses = []
@ -99,9 +109,7 @@ class AccountIndexer(object):
return addresses
def updateIfNeeded(self):
"""
update address index
"""
"""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

@ -1,3 +1,4 @@
"""This module contains a LevelDB client."""
import binascii
import rlp
from mythril.ethereum.interface.leveldb.accountindexing import CountableList
@ -33,32 +34,31 @@ address_mapping_head_key = b"accountMapping" # head (latest) number of indexed
def _format_block_number(number):
"""
formats block number to uint64 big endian
"""
"""Format block number to uint64 big endian."""
return utils.zpad(utils.int_to_big_endian(number), 8)
def _encode_hex(v):
"""
encodes hash as hex
"""
"""Encode a hash string as hex."""
return "0x" + utils.encode_hex(v)
class LevelDBReader(object):
"""
level db reading interface, can be used with snapshot
"""
"""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):
"""
gets head state
"""Get head state.
:return:
"""
if not self.head_state:
root = self._get_head_block().state_root
@ -66,24 +66,29 @@ class LevelDBReader(object):
return self.head_state
def _get_account(self, address):
"""
gets account by 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):
"""
gets block hash by block 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):
"""
gets head block header
"""Get head block header.
:return:
"""
if not self.head_block_header:
block_hash = self.db.get(head_header_key)
@ -101,12 +106,21 @@ class LevelDBReader(object):
return self.head_block_header
def _get_block_number(self, block_hash):
"""Get block number by its 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"""
"""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)
@ -114,16 +128,28 @@ class LevelDBReader(object):
return header
def _get_address_by_hash(self, block_hash):
"""Get mapped address by its 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"""
"""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"""
"""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)
@ -132,55 +158,56 @@ class LevelDBReader(object):
class LevelDBWriter(object):
"""
level db writing interface
"""
"""level db writing interface."""
def __init__(self, db):
"""
:param db:
"""
self.db = db
self.wb = None
def _set_last_indexed_number(self, number):
"""
sets latest indexed block 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
"""
"""Start writing a batch."""
self.wb = self.db.write_batch()
def _commit_batch(self):
"""
commit batch
"""
"""Commit a batch."""
self.wb.write()
def _store_account_address(self, address):
"""
get block transaction receipts by block header hash & number
"""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
"""
"""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
"""
"""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)
@ -189,8 +216,10 @@ class EthLevelDB(object):
yield contract, account.address, account.balance
def search(self, expression, callback_func):
"""
searches through all contract accounts
"""Search through all contract accounts.
:param expression:
:param callback_func:
"""
cnt = 0
indexer = AccountIndexer(self)
@ -202,10 +231,12 @@ class EthLevelDB(object):
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.
"""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
@ -218,7 +249,11 @@ class EthLevelDB(object):
log.info("Searched %d contracts" % cnt)
def contract_hash_to_address(self, contract_hash):
"""Tries to find corresponding account address"""
"""Try to find corresponding account address.
:param contract_hash:
:return:
"""
address_hash = binascii.a2b_hex(utils.remove_0x_head(contract_hash))
indexer = AccountIndexer(self)
@ -226,16 +261,20 @@ class EthLevelDB(object):
return _encode_hex(indexer.get_contract_by_hash(address_hash))
def eth_getBlockHeaderByNumber(self, number):
"""
gets block header by block 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):
"""
gets block body by block number
"""Get block body by block number.
:param number:
:return:
"""
block_hash = self.reader._get_block_hash(number)
block_number = _format_block_number(number)
@ -245,22 +284,29 @@ class EthLevelDB(object):
return body
def eth_getCode(self, address):
"""
gets account code
"""Get account code.
:param address:
:return:
"""
account = self.reader._get_account(address)
return _encode_hex(account.code)
def eth_getBalance(self, address):
"""
gets account balance
"""Get account balance.
:param address:
:return:
"""
account = self.reader._get_account(address)
return account.balance
def eth_getStorageAt(self, address, position):
"""
gets account storage data at position
"""Get account storage data at position.
:param address:
:param position:
:return:
"""
account = self.reader._get_account(address)
return _encode_hex(

@ -1,29 +1,23 @@
"""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
"""
"""Adopts pythereum BaseDB using plyvel."""
def __init__(self, path):
self.db = plyvel.DB(path)
def get(self, key):
"""
gets value for key
"""
"""gets value for key."""
return self.db.get(key)
def put(self, key, value):
"""
puts value for key
"""
"""puts value for key."""
self.db.put(key, value)
def write_batch(self):
"""
start writing a batch
"""
"""start writing a batch."""
return self.db.write_batch()

@ -1,3 +1,4 @@
"""This module implements wrappers around the pyethereum state for LevelDB."""
import rlp
import binascii
from ethereum.utils import (
@ -47,9 +48,7 @@ STATE_DEFAULTS = {
class Account(rlp.Serializable):
"""
adjusted account from ethereum.state
"""
"""adjusted account from ethereum.state."""
fields = [
("nonce", big_endian_int),
@ -59,6 +58,15 @@ class Account(rlp.Serializable):
]
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)
@ -72,14 +80,14 @@ class Account(rlp.Serializable):
@property
def code(self):
"""
code rlp data
"""
"""code rlp data."""
return self.db.get(self.code_hash)
def get_storage_data(self, key):
"""
get storage data
"""get storage data.
:param key:
:return:
"""
if key not in self.storage_cache:
v = self.storage_trie.get(utils.encode_int32(key))
@ -90,8 +98,12 @@ class Account(rlp.Serializable):
@classmethod
def blank_account(cls, db, addr, initial_nonce=0):
"""
creates a blank account
"""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)
@ -99,18 +111,22 @@ class Account(rlp.Serializable):
return o
def is_blank(self):
"""
checks if is a blank account
"""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
"""
"""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)
@ -118,7 +134,12 @@ class State:
self.cache = {}
def get_and_cache_account(self, addr):
"""Gets and caches an account for an addres, creates blank if not found"""
"""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]
@ -138,9 +159,7 @@ class State:
return o
def get_all_accounts(self):
"""
iterates through trie to and yields non-blank leafs as accounts
"""
"""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, address=address_hash)

@ -1,6 +1,11 @@
"""This module provides a basic RPC interface client.
This code is adapted from: https://github.com/ConsenSys/ethjsonrpc
"""
from abc import abstractmethod
from .constants import BLOCK_TAGS, BLOCK_TAG_LATEST
from .constants import BLOCK_TAG_LATEST, BLOCK_TAGS
from .utils import hex_to_dec, validate_block
GETH_DEFAULT_RPC_PORT = 8545
@ -10,18 +15,25 @@ PYETHAPP_DEFAULT_RPC_PORT = 4000
MAX_RETRIES = 3
JSON_MEDIA_TYPE = "application/json"
"""
This code is adapted from: https://github.com/ConsenSys/ethjsonrpc
"""
class BaseClient(object):
"""The base RPC client class."""
@abstractmethod
def _call(self, method, params=None, _id=1):
"""TODO: documentation
:param method:
:param params:
:param _id:
:return:
"""
pass
def eth_coinbase(self):
"""
"""TODO: documentation
https://github.com/ethereum/wiki/wiki/JSON-RPC#eth_coinbase
TESTED
@ -29,7 +41,8 @@ class BaseClient(object):
return self._call("eth_coinbase")
def eth_blockNumber(self):
"""
"""TODO: documentation
https://github.com/ethereum/wiki/wiki/JSON-RPC#eth_blocknumber
TESTED
@ -37,7 +50,8 @@ class BaseClient(object):
return hex_to_dec(self._call("eth_blockNumber"))
def eth_getBalance(self, address=None, block=BLOCK_TAG_LATEST):
"""
"""TODO: documentation
https://github.com/ethereum/wiki/wiki/JSON-RPC#eth_getbalance
TESTED
@ -47,7 +61,8 @@ class BaseClient(object):
return hex_to_dec(self._call("eth_getBalance", [address, block]))
def eth_getStorageAt(self, address=None, position=0, block=BLOCK_TAG_LATEST):
"""
"""TODO: documentation
https://github.com/ethereum/wiki/wiki/JSON-RPC#eth_getstorageat
TESTED
@ -56,7 +71,8 @@ class BaseClient(object):
return self._call("eth_getStorageAt", [address, hex(position), block])
def eth_getCode(self, address, default_block=BLOCK_TAG_LATEST):
"""
"""TODO: documentation
https://github.com/ethereum/wiki/wiki/JSON-RPC#eth_getcode
NEEDS TESTING
@ -67,7 +83,8 @@ class BaseClient(object):
return self._call("eth_getCode", [address, default_block])
def eth_getBlockByNumber(self, block=BLOCK_TAG_LATEST, tx_objects=True):
"""
"""TODO: documentation
https://github.com/ethereum/wiki/wiki/JSON-RPC#eth_getblockbynumber
TESTED
@ -76,7 +93,8 @@ class BaseClient(object):
return self._call("eth_getBlockByNumber", [block, tx_objects])
def eth_getTransactionReceipt(self, tx_hash):
"""
"""TODO: documentation
https://github.com/ethereum/wiki/wiki/JSON-RPC#eth_gettransactionreceipt
TESTED

@ -1,15 +1,21 @@
"""This module contains a basic Ethereum RPC client.
This code is adapted from: https://github.com/ConsenSys/ethjsonrpc
"""
import json
import logging
import requests
from requests.adapters import HTTPAdapter
from requests.exceptions import ConnectionError as RequestsConnectionError
from .base_client import BaseClient
from .exceptions import (
ConnectionError,
BadStatusCodeError,
BadJsonError,
BadResponseError,
BadStatusCodeError,
ConnectionError,
)
from .base_client import BaseClient
log = logging.getLogger(__name__)
@ -20,17 +26,17 @@ PYETHAPP_DEFAULT_RPC_PORT = 4000
MAX_RETRIES = 3
JSON_MEDIA_TYPE = "application/json"
"""
This code is adapted from: https://github.com/ConsenSys/ethjsonrpc
"""
class EthJsonRpc(BaseClient):
"""
Ethereum JSON-RPC client class
"""
"""Ethereum JSON-RPC client class."""
def __init__(self, host="localhost", port=GETH_DEFAULT_RPC_PORT, tls=False):
"""
:param host:
:param port:
:param tls:
"""
self.host = host
self.port = port
self.tls = tls
@ -38,7 +44,13 @@ class EthJsonRpc(BaseClient):
self.session.mount(self.host, HTTPAdapter(max_retries=MAX_RETRIES))
def _call(self, method, params=None, _id=1):
"""
:param method:
:param params:
:param _id:
:return:
"""
params = params or []
data = {"jsonrpc": "2.0", "method": method, "params": params, "id": _id}
scheme = "http"
@ -64,4 +76,5 @@ class EthJsonRpc(BaseClient):
raise BadResponseError(response)
def close(self):
"""Close the RPC client's session."""
self.session.close()

@ -1,3 +1,5 @@
"""This file contains constants used used by the Ethereum JSON RPC
interface."""
BLOCK_TAG_EARLIEST = "earliest"
BLOCK_TAG_LATEST = "latest"
BLOCK_TAG_PENDING = "pending"

@ -1,18 +1,35 @@
"""This module contains exceptions regarding JSON-RPC communication."""
class EthJsonRpcError(Exception):
"""The JSON-RPC base exception type."""
pass
class ConnectionError(EthJsonRpcError):
"""An RPC exception denoting there was an error in connecting to the RPC
instance."""
pass
class BadStatusCodeError(EthJsonRpcError):
"""An RPC exception denoting a bad status code returned by the RPC
instance."""
pass
class BadJsonError(EthJsonRpcError):
"""An RPC exception denoting that the RPC instance returned a bad JSON
object."""
pass
class BadResponseError(EthJsonRpcError):
"""An RPC exception denoting that the RPC instance returned a bad
response."""
pass

@ -1,22 +1,33 @@
"""This module contains various utility functions regarding the RPC data format
and validation."""
from .constants import BLOCK_TAGS
def hex_to_dec(x):
"""
Convert hex to decimal
"""Convert hex to decimal.
:param x:
:return:
"""
return int(x, 16)
def clean_hex(d):
"""
Convert decimal to hex and remove the "L" suffix that is appended to large
numbers
"""Convert decimal to hex and remove the "L" suffix that is appended to
large numbers.
:param d:
:return:
"""
return hex(d).rstrip("L")
def validate_block(block):
"""
:param block:
:return:
"""
if isinstance(block, str):
if block not in BLOCK_TAGS:
raise ValueError("invalid block tag")
@ -26,14 +37,18 @@ def validate_block(block):
def wei_to_ether(wei):
"""
Convert wei to ether
"""Convert wei to ether.
:param wei:
:return:
"""
return 1.0 * wei / 10 ** 18
def ether_to_wei(ether):
"""
Convert ether to wei
"""Convert ether to wei.
:param ether:
:return:
"""
return ether * 10 ** 18

@ -1,16 +1,23 @@
from ethereum.abi import encode_abi, encode_int
from ethereum.utils import zpad
from ethereum.abi import method_id
from mythril.exceptions import CompilerError
from subprocess import Popen, PIPE
"""This module contains various utility functions regarding unit conversion and
solc integration."""
import binascii
import os
import json
import os
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 mythril.exceptions import CompilerError
def safe_decode(hex_encoded_string):
"""
:param hex_encoded_string:
:return:
"""
if hex_encoded_string.startswith("0x"):
return bytes.fromhex(hex_encoded_string[2:])
else:
@ -18,7 +25,13 @@ def safe_decode(hex_encoded_string):
def get_solc_json(file, solc_binary="solc", solc_args=None):
"""
:param file:
:param solc_binary:
:param solc_args:
:return:
"""
cmd = [solc_binary, "--combined-json", "bin,bin-runtime,srcmap,srcmap-runtime"]
if solc_args:
@ -58,6 +71,13 @@ def get_solc_json(file, solc_binary="solc", solc_args=None):
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)
@ -65,14 +85,28 @@ def encode_calldata(func_name, arg_types, args):
def get_random_address():
"""
:return:
"""
return binascii.b2a_hex(os.urandom(20)).decode("UTF-8")
def get_indexed_address(index):
"""
:param index:
:return:
"""
return "0x" + (hex(index)[2:] * 40)
def solc_exists(version):
"""
:param version:
:return:
"""
solc_binaries = [
os.path.join(
os.environ.get("HOME", str(Path.home())),

@ -1,22 +1,45 @@
"""This module contains general exceptions used by Mythril."""
class MythrilBaseException(Exception):
"""The Mythril exception base type."""
pass
class OutOfTimeError(MythrilBaseException):
pass
class CompilerError(MythrilBaseException):
"""A Mythril exception denoting an error during code compilation."""
pass
class UnsatError(MythrilBaseException):
"""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."""
pass
class CriticalError(MythrilBaseException):
"""A Mythril exception denoting an unknown critical error has been
encountered."""
pass
class AddressNotFoundError(MythrilBaseException):
"""A Mythril exception denoting the given smart contract address was not
found."""
pass

@ -5,23 +5,30 @@
http://www.github.com/ConsenSys/mythril
"""
import logging, coloredlogs
import argparse
import json
import logging
import os
import sys
import argparse
# logging.basicConfig(level=logging.DEBUG)
import coloredlogs
from mythril.exceptions import CriticalError, AddressNotFoundError
import mythril.support.signatures as sigs
from mythril.exceptions import AddressNotFoundError, CriticalError
from mythril.mythril import Mythril
from mythril.version import VERSION
import mythril.support.signatures as sigs
# logging.basicConfig(level=logging.DEBUG)
log = logging.getLogger(__name__)
def exit_with_error(format_, message):
"""
:param format_:
:param message:
"""
if format_ == "text" or format_ == "markdown":
log.error(message)
else:
@ -31,6 +38,7 @@ def exit_with_error(format_, message):
def main():
"""The main CLI interface entry point."""
parser = argparse.ArgumentParser(
description="Security analysis of Ethereum smart contracts"
)

@ -1,3 +1,4 @@
"""Don't ask."""
#!/usr/bin/env python
#
# "THE BEER-WARE LICENSE" (Revision 43~maze)
@ -20,6 +21,7 @@ PY3 = sys.version_info >= (3,)
# Reset terminal colors at exit
def reset():
""""""
sys.stdout.write("\x1b[0m")
sys.stdout.flush()
@ -49,6 +51,8 @@ COLOR_ANSI = (
class LolCat(object):
"""Cats lel."""
def __init__(self, mode=256, output=sys.stdout):
self.mode = mode
self.output = output
@ -57,6 +61,11 @@ class LolCat(object):
return sum(map(lambda c: (c[0] - c[1]) ** 2, zip(rgb1, rgb2)))
def ansi(self, rgb):
"""
:param rgb:
:return:
"""
r, g, b = rgb
if self.mode in (8, 16):
@ -93,15 +102,31 @@ class LolCat(object):
return "38;5;%d" % (color,)
def wrap(self, *codes):
"""
:param codes:
:return:
"""
return "\x1b[%sm" % ("".join(codes),)
def rainbow(self, freq, i):
"""
:param freq:
:param i:
:return:
"""
r = math.sin(freq * i) * 127 + 128
g = math.sin(freq * i + 2 * math.pi / 3) * 127 + 128
b = math.sin(freq * i + 4 * math.pi / 3) * 127 + 128
return [r, g, b]
def cat(self, fd, options):
"""
:param fd:
:param options:
"""
if options.animate:
self.output.write("\x1b[?25l")
@ -113,6 +138,11 @@ class LolCat(object):
self.output.write("\x1b[?25h")
def println(self, s, options):
"""
:param s:
:param options:
"""
s = s.rstrip()
if options.force or self.output.isatty():
s = STRIP_ANSI.sub("", s)
@ -126,6 +156,12 @@ class LolCat(object):
self.output.flush()
def println_ani(self, s, options):
"""
:param s:
:param options:
:return:
"""
if not s:
return
@ -137,6 +173,11 @@ class LolCat(object):
time.sleep(1.0 / options.speed)
def println_plain(self, s, options):
"""
:param s:
:param options:
"""
for i, c in enumerate(s if PY3 else s.decode(options.charset_py2, "replace")):
rgb = self.rainbow(options.freq, options.os + i / options.spread)
self.output.write(
@ -150,9 +191,7 @@ class LolCat(object):
def detect_mode(term_hint="xterm-256color"):
"""
Poor-mans color mode detection.
"""
"""Poor-mans color mode detection."""
if "ANSICON" in os.environ:
return 16
elif os.environ.get("ConEmuANSI", "OFF") == "ON":

@ -1,3 +1,7 @@
"""This module contains the business logic used by Instruction in
instructions.py to get the necessary elements from the stack and determine the
parameters for the new global state."""
import logging
from typing import Union, List
@ -26,9 +30,9 @@ log = logging.getLogger(__name__)
def get_call_parameters(
global_state: GlobalState, dynamic_loader: DynLoader, with_value=False
):
"""
Gets call parameters from global state
Pops the values from the stack and determines output parameters
"""Gets call parameters from global state Pops the values from the stack
and determines output parameters.
:param global_state: state to look in
:param dynamic_loader: dynamic loader to use
:param with_value: whether to pop the value argument from the stack
@ -66,8 +70,8 @@ def get_callee_address(
dynamic_loader: DynLoader,
symbolic_to_address: Expression,
):
"""
Gets the address of the callee
"""Gets the address of the callee.
:param global_state: state to look in
:param dynamic_loader: dynamic loader to use
:param symbolic_to_address: The (symbolic) callee address
@ -109,8 +113,8 @@ def get_callee_address(
def get_callee_account(
global_state: GlobalState, callee_address: str, dynamic_loader: DynLoader
):
"""
Gets the callees account from the global_state
"""Gets the callees account from the global_state.
:param global_state: state to look in
:param callee_address: address of the callee
:param dynamic_loader: dynamic loader to use
@ -153,8 +157,8 @@ def get_call_data(
memory_start: Union[int, Expression],
memory_size: Union[int, Expression],
):
"""
Gets call_data from the global_state
"""Gets call_data from the global_state.
:param global_state: state to look in
:param memory_start: Start index
:param memory_size: Size

@ -1,11 +1,15 @@
from flags import Flags
"""This module."""
from enum import Enum
from typing import Dict
from flags import Flags
gbl_next_uid = 0 # node counter
class JumpType(Enum):
"""An enum to represent the types of possible JUMP scenarios."""
CONDITIONAL = 1
UNCONDITIONAL = 2
CALL = 3
@ -14,11 +18,15 @@ class JumpType(Enum):
class NodeFlags(Flags):
"""A collection of flags to denote the type a call graph node can have."""
FUNC_ENTRY = 1
CALL_RETURN = 2
class Node:
"""The representation of a call graph node."""
def __init__(
self,
contract_name: str,
@ -26,6 +34,12 @@ class Node:
constraints=None,
function_name="unknown",
):
"""
:param contract_name:
:param start_addr:
:param constraints:
"""
constraints = constraints if constraints else []
self.contract_name = contract_name
self.start_addr = start_addr
@ -41,6 +55,10 @@ class Node:
gbl_next_uid += 1
def get_cfg_dict(self) -> Dict:
"""
:return:
"""
code = ""
for state in self.states:
instruction = state.get_current_instruction()
@ -60,6 +78,8 @@ class Node:
class Edge:
"""The respresentation of a call graph edge."""
def __init__(
self,
node_from: int,
@ -67,14 +87,29 @@ class Edge:
edge_type=JumpType.UNCONDITIONAL,
condition=None,
):
"""
:param node_from:
:param node_to:
:param edge_type:
:param condition:
"""
self.node_from = node_from
self.node_to = node_to
self.type = edge_type
self.condition = condition
def __str__(self) -> str:
"""
:return:
"""
return str(self.as_dict)
@property
def as_dict(self) -> Dict[str, int]:
"""
:return:
"""
return {"from": self.node_from, "to": self.node_to}

@ -1,22 +1,37 @@
"""This module contains EVM exception types used by LASER."""
class VmException(Exception):
"""The base VM exception type."""
pass
class StackUnderflowException(IndexError, VmException):
"""A VM exception regarding stack underflows."""
pass
class StackOverflowException(VmException):
"""A VM exception regarding stack overflows."""
pass
class InvalidJumpDestination(VmException):
"""A VM exception regarding JUMPs to invalid destinations."""
pass
class InvalidInstruction(VmException):
"""A VM exception denoting an invalid op code has been encountered."""
pass
class OutOfGasException(VmException):
"""A VM exception denoting the current execution has run out of gas."""
pass

@ -1,8 +1,16 @@
"""This module contains functions for dynamic gas calculation and a gas cost
table."""
from ethereum import opcodes
from ethereum.utils import ceil32
def calculate_native_gas(size: int, contract: str):
"""
:param size:
:param contract:
:return:
"""
gas_value = None
word_num = ceil32(size) // 32
if contract == "ecrecover":
@ -19,6 +27,11 @@ def calculate_native_gas(size: int, contract: str):
def calculate_sha3_gas(length: int):
"""
:param length:
:return:
"""
gas_val = 30 + opcodes.GSHA3WORD * (ceil32(length) // 32)
return gas_val, gas_val

@ -1,3 +1,5 @@
"""This module contains a representation class for EVM instructions and
transitions between them."""
import binascii
import logging
@ -58,21 +60,39 @@ keccak_function_manager = KeccakFunctionManager()
class StateTransition(object):
"""Decorator that handles global state copy and original return.
This decorator calls the decorated instruction mutator function on a copy of the state that
is passed to it. After the call, the resulting new states' program counter is automatically
incremented if `increment_pc=True`.
This decorator calls the decorated instruction mutator function on a
copy of the state that is passed to it. After the call, the
resulting new states' program counter is automatically incremented
if `increment_pc=True`.
"""
def __init__(self, increment_pc=True, enable_gas=True):
"""
:param increment_pc:
:param enable_gas:
"""
self.increment_pc = increment_pc
self.enable_gas = enable_gas
@staticmethod
def call_on_state_copy(func: Callable, func_obj: "Instruction", state: GlobalState):
"""
:param func:
:param func_obj:
:param state:
:return:
"""
global_state_copy = copy(state)
return func(func_obj, global_state_copy)
def increment_states_pc(self, states: List[GlobalState]) -> List[GlobalState]:
"""
:param states:
:return:
"""
if self.increment_pc:
for state in states:
state.mstate.pc += 1
@ -80,6 +100,11 @@ class StateTransition(object):
@staticmethod
def check_gas_usage_limit(global_state: GlobalState):
"""
:param global_state:
:return:
"""
global_state.mstate.check_gas()
if isinstance(global_state.current_transaction.gas_limit, BitVec):
value = global_state.current_transaction.gas_limit.value
@ -93,6 +118,11 @@ class StateTransition(object):
raise OutOfGasException()
def accumulate_gas(self, global_state: GlobalState):
"""
:param global_state:
:return:
"""
if not self.enable_gas:
return global_state
opcode = global_state.instruction["opcode"]
@ -105,6 +135,12 @@ class StateTransition(object):
def wrapper(
func_obj: "Instruction", global_state: GlobalState
) -> List[GlobalState]:
"""
:param func_obj:
:param global_state:
:return:
"""
new_global_states = self.call_on_state_copy(func, func_obj, global_state)
new_global_states = [
self.accumulate_gas(state) for state in new_global_states
@ -115,16 +151,25 @@ class StateTransition(object):
class Instruction:
"""
Instruction class is used to mutate a state according to the current instruction
"""
"""Instruction class is used to mutate a state according to the current
instruction."""
def __init__(self, op_code: str, dynamic_loader: DynLoader):
"""
:param op_code:
:param dynamic_loader:
"""
self.dynamic_loader = dynamic_loader
self.op_code = op_code.upper()
def evaluate(self, global_state: GlobalState, post=False) -> List[GlobalState]:
""" Performs the mutation for this instruction """
"""Performs the mutation for this instruction.
:param global_state:
:param post:
:return:
"""
# Generalize some ops
log.debug("Evaluating {}".format(self.op_code))
op = self.op_code.lower()
@ -150,10 +195,20 @@ class Instruction:
@StateTransition()
def jumpdest_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
return [global_state]
@StateTransition()
def push_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
push_instruction = global_state.get_current_instruction()
push_value = push_instruction["argument"][2:]
@ -170,12 +225,22 @@ class Instruction:
@StateTransition()
def dup_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
value = int(global_state.get_current_instruction()["opcode"][3:], 10)
global_state.mstate.stack.append(global_state.mstate.stack[-value])
return [global_state]
@StateTransition()
def swap_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
depth = int(self.op_code[4:])
stack = global_state.mstate.stack
stack[-depth - 1], stack[-1] = stack[-1], stack[-depth - 1]
@ -183,11 +248,21 @@ class Instruction:
@StateTransition()
def pop_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
global_state.mstate.stack.pop()
return [global_state]
@StateTransition()
def and_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
stack = global_state.mstate.stack
op1, op2 = stack.pop(), stack.pop()
if isinstance(op1, Bool):
@ -208,6 +283,11 @@ class Instruction:
@StateTransition()
def or_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
stack = global_state.mstate.stack
op1, op2 = stack.pop(), stack.pop()
@ -227,18 +307,33 @@ class Instruction:
@StateTransition()
def xor_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
mstate = global_state.mstate
mstate.stack.append(mstate.stack.pop() ^ mstate.stack.pop())
return [global_state]
@StateTransition()
def not_(self, global_state: GlobalState):
"""
:param global_state:
:return:
"""
mstate = global_state.mstate
mstate.stack.append(symbol_factory.BitVecVal(TT256M1, 256) - mstate.stack.pop())
return [global_state]
@StateTransition()
def byte_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
mstate = global_state.mstate
op0, op1 = mstate.stack.pop(), mstate.stack.pop()
if not isinstance(op1, Expression):
@ -267,6 +362,11 @@ class Instruction:
# Arithmetic
@StateTransition()
def add_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
global_state.mstate.stack.append(
(
helper.pop_bitvec(global_state.mstate)
@ -277,6 +377,11 @@ class Instruction:
@StateTransition()
def sub_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
global_state.mstate.stack.append(
(
helper.pop_bitvec(global_state.mstate)
@ -287,6 +392,11 @@ class Instruction:
@StateTransition()
def mul_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
global_state.mstate.stack.append(
(
helper.pop_bitvec(global_state.mstate)
@ -297,6 +407,11 @@ class Instruction:
@StateTransition()
def div_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
op0, op1 = (
util.pop_bitvec(global_state.mstate),
util.pop_bitvec(global_state.mstate),
@ -309,6 +424,11 @@ class Instruction:
@StateTransition()
def sdiv_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
s0, s1 = (
util.pop_bitvec(global_state.mstate),
util.pop_bitvec(global_state.mstate),
@ -321,6 +441,11 @@ class Instruction:
@StateTransition()
def mod_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
s0, s1 = (
util.pop_bitvec(global_state.mstate),
util.pop_bitvec(global_state.mstate),
@ -330,6 +455,11 @@ class Instruction:
@StateTransition()
def smod_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
s0, s1 = (
util.pop_bitvec(global_state.mstate),
util.pop_bitvec(global_state.mstate),
@ -339,6 +469,11 @@ class Instruction:
@StateTransition()
def addmod_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
s0, s1, s2 = (
util.pop_bitvec(global_state.mstate),
util.pop_bitvec(global_state.mstate),
@ -349,6 +484,11 @@ class Instruction:
@StateTransition()
def mulmod_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
s0, s1, s2 = (
util.pop_bitvec(global_state.mstate),
util.pop_bitvec(global_state.mstate),
@ -359,6 +499,11 @@ class Instruction:
@StateTransition()
def exp_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
state = global_state.mstate
base, exponent = util.pop_bitvec(state), util.pop_bitvec(state)
@ -379,6 +524,11 @@ class Instruction:
@StateTransition()
def signextend_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
state = global_state.mstate
s0, s1 = state.stack.pop(), state.stack.pop()
@ -402,6 +552,11 @@ class Instruction:
# Comparisons
@StateTransition()
def lt_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
state = global_state.mstate
exp = ULT(util.pop_bitvec(state), util.pop_bitvec(state))
state.stack.append(exp)
@ -409,6 +564,11 @@ class Instruction:
@StateTransition()
def gt_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
state = global_state.mstate
op1, op2 = util.pop_bitvec(state), util.pop_bitvec(state)
exp = UGT(op1, op2)
@ -417,6 +577,11 @@ class Instruction:
@StateTransition()
def slt_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
state = global_state.mstate
exp = util.pop_bitvec(state) < util.pop_bitvec(state)
state.stack.append(exp)
@ -424,6 +589,11 @@ class Instruction:
@StateTransition()
def sgt_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
state = global_state.mstate
exp = util.pop_bitvec(state) > util.pop_bitvec(state)
@ -432,6 +602,11 @@ class Instruction:
@StateTransition()
def eq_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
state = global_state.mstate
op1 = state.stack.pop()
@ -454,6 +629,11 @@ class Instruction:
@StateTransition()
def iszero_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
state = global_state.mstate
val = state.stack.pop()
@ -469,6 +649,11 @@ class Instruction:
# Call data
@StateTransition()
def callvalue_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
state = global_state.mstate
environment = global_state.environment
state.stack.append(environment.callvalue)
@ -477,6 +662,11 @@ class Instruction:
@StateTransition()
def calldataload_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
state = global_state.mstate
environment = global_state.environment
op0 = state.stack.pop()
@ -489,6 +679,11 @@ class Instruction:
@StateTransition()
def calldatasize_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
state = global_state.mstate
environment = global_state.environment
state.stack.append(environment.calldata.calldatasize)
@ -496,6 +691,11 @@ class Instruction:
@StateTransition()
def calldatacopy_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
state = global_state.mstate
environment = global_state.environment
op0, op1, op2 = state.stack.pop(), state.stack.pop(), state.stack.pop()
@ -590,6 +790,11 @@ class Instruction:
# Environment
@StateTransition()
def address_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
state = global_state.mstate
environment = global_state.environment
state.stack.append(environment.address)
@ -597,6 +802,11 @@ class Instruction:
@StateTransition()
def balance_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
state = global_state.mstate
address = state.stack.pop()
state.stack.append(global_state.new_bitvec("balance_at_" + str(address), 256))
@ -604,6 +814,11 @@ class Instruction:
@StateTransition()
def origin_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
state = global_state.mstate
environment = global_state.environment
state.stack.append(environment.origin)
@ -611,6 +826,11 @@ class Instruction:
@StateTransition()
def caller_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
state = global_state.mstate
environment = global_state.environment
state.stack.append(environment.sender)
@ -618,6 +838,11 @@ class Instruction:
@StateTransition()
def codesize_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
state = global_state.mstate
environment = global_state.environment
disassembly = environment.code
@ -626,6 +851,11 @@ class Instruction:
@StateTransition(enable_gas=False)
def sha3_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
global keccak_function_manager
state = global_state.mstate
@ -676,11 +906,21 @@ class Instruction:
@StateTransition()
def gasprice_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
global_state.mstate.stack.append(global_state.new_bitvec("gasprice", 256))
return [global_state]
@StateTransition()
def codecopy_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
memory_offset, code_offset, size = (
global_state.mstate.stack.pop(),
global_state.mstate.stack.pop(),
@ -767,6 +1007,11 @@ class Instruction:
@StateTransition()
def extcodesize_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
state = global_state.mstate
addr = state.stack.pop()
environment = global_state.environment
@ -793,6 +1038,11 @@ class Instruction:
@StateTransition()
def extcodecopy_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
# FIXME: not implemented
state = global_state.mstate
addr = state.stack.pop()
@ -802,6 +1052,11 @@ class Instruction:
@StateTransition()
def returndatacopy_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
# FIXME: not implemented
state = global_state.mstate
start, s2, size = state.stack.pop(), state.stack.pop(), state.stack.pop()
@ -810,11 +1065,21 @@ class Instruction:
@StateTransition()
def returndatasize_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
global_state.mstate.stack.append(global_state.new_bitvec("returndatasize", 256))
return [global_state]
@StateTransition()
def blockhash_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
state = global_state.mstate
blocknumber = state.stack.pop()
state.stack.append(
@ -824,21 +1089,41 @@ class Instruction:
@StateTransition()
def coinbase_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
global_state.mstate.stack.append(global_state.new_bitvec("coinbase", 256))
return [global_state]
@StateTransition()
def timestamp_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
global_state.mstate.stack.append(global_state.new_bitvec("timestamp", 256))
return [global_state]
@StateTransition()
def number_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
global_state.mstate.stack.append(global_state.new_bitvec("block_number", 256))
return [global_state]
@StateTransition()
def difficulty_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
global_state.mstate.stack.append(
global_state.new_bitvec("block_difficulty", 256)
)
@ -846,12 +1131,22 @@ class Instruction:
@StateTransition()
def gaslimit_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
global_state.mstate.stack.append(global_state.mstate.gas_limit)
return [global_state]
# Memory operations
@StateTransition()
def mload_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
state = global_state.mstate
op0 = state.stack.pop()
@ -875,6 +1170,11 @@ class Instruction:
@StateTransition()
def mstore_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
state = global_state.mstate
op0, value = state.stack.pop(), state.stack.pop()
@ -897,6 +1197,11 @@ class Instruction:
@StateTransition()
def mstore8_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
state = global_state.mstate
op0, value = state.stack.pop(), state.stack.pop()
@ -920,6 +1225,11 @@ class Instruction:
@StateTransition()
def sload_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
global keccak_function_manager
state = global_state.mstate
@ -966,6 +1276,13 @@ class Instruction:
def _sload_helper(
global_state: GlobalState, index: Union[int, Expression], constraints=None
):
"""
:param global_state:
:param index:
:param constraints:
:return:
"""
try:
data = global_state.environment.active_account.storage[index]
except KeyError:
@ -980,6 +1297,12 @@ class Instruction:
@staticmethod
def _get_constraints(keccak_keys, this_key, argument):
"""
:param keccak_keys:
:param this_key:
:param argument:
"""
global keccak_function_manager
for keccak_key in keccak_keys:
if keccak_key == this_key:
@ -989,6 +1312,11 @@ class Instruction:
@StateTransition()
def sstore_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
global keccak_function_manager
state = global_state.mstate
index, value = state.stack.pop(), state.stack.pop()
@ -1044,6 +1372,14 @@ class Instruction:
@staticmethod
def _sstore_helper(global_state, index, value, constraint=None):
"""
:param global_state:
:param index:
:param value:
:param constraint:
:return:
"""
try:
global_state.environment.active_account = deepcopy(
global_state.environment.active_account
@ -1065,6 +1401,11 @@ class Instruction:
@StateTransition(increment_pc=False, enable_gas=False)
def jump_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
state = global_state.mstate
disassembly = global_state.environment.code
try:
@ -1099,6 +1440,11 @@ class Instruction:
@StateTransition(increment_pc=False, enable_gas=False)
def jumpi_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
state = global_state.mstate
disassembly = global_state.environment.code
min_gas, max_gas = OPCODE_GAS["JUMPI"]
@ -1169,22 +1515,42 @@ class Instruction:
@StateTransition()
def pc_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
global_state.mstate.stack.append(global_state.mstate.pc - 1)
return [global_state]
@StateTransition()
def msize_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
global_state.mstate.stack.append(global_state.new_bitvec("msize", 256))
return [global_state]
@StateTransition()
def gas_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
# TODO: Push a Constrained variable which lies between min gas and max gas
global_state.mstate.stack.append(global_state.new_bitvec("gas", 256))
return [global_state]
@StateTransition()
def log_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
# TODO: implement me
state = global_state.mstate
dpth = int(self.op_code[3:])
@ -1195,6 +1561,11 @@ class Instruction:
@StateTransition()
def create_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
# TODO: implement me
state = global_state.mstate
state.stack.pop(), state.stack.pop(), state.stack.pop()
@ -1204,6 +1575,10 @@ class Instruction:
@StateTransition()
def return_(self, global_state: GlobalState):
"""
:param global_state:
"""
state = global_state.mstate
offset, length = state.stack.pop(), state.stack.pop()
return_data = [global_state.new_bitvec("return_data", 8)]
@ -1217,6 +1592,10 @@ class Instruction:
@StateTransition()
def suicide_(self, global_state: GlobalState):
"""
:param global_state:
"""
target = global_state.mstate.stack.pop()
account_created = False
# Often the target of the suicide instruction will be symbolic
@ -1248,6 +1627,10 @@ class Instruction:
@StateTransition()
def revert_(self, global_state: GlobalState) -> None:
"""
:param global_state:
"""
state = global_state.mstate
offset, length = state.stack.pop(), state.stack.pop()
return_data = [global_state.new_bitvec("return_data", 8)]
@ -1263,20 +1646,36 @@ class Instruction:
@StateTransition()
def assert_fail_(self, global_state: GlobalState):
"""
:param global_state:
"""
# 0xfe: designated invalid opcode
raise InvalidInstruction
@StateTransition()
def invalid_(self, global_state: GlobalState):
"""
:param global_state:
"""
raise InvalidInstruction
@StateTransition()
def stop_(self, global_state: GlobalState):
"""
:param global_state:
"""
global_state.current_transaction.end(global_state)
@StateTransition()
def call_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
instr = global_state.get_current_instruction()
environment = global_state.environment
@ -1321,6 +1720,11 @@ class Instruction:
@StateTransition()
def call_post(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
instr = global_state.get_current_instruction()
try:
@ -1383,6 +1787,11 @@ class Instruction:
@StateTransition()
def callcode_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
instr = global_state.get_current_instruction()
environment = global_state.environment
@ -1416,6 +1825,11 @@ class Instruction:
@StateTransition()
def callcode_post(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
instr = global_state.get_current_instruction()
try:
@ -1476,6 +1890,11 @@ class Instruction:
@StateTransition()
def delegatecall_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
instr = global_state.get_current_instruction()
environment = global_state.environment
@ -1509,6 +1928,11 @@ class Instruction:
@StateTransition()
def delegatecall_post(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
instr = global_state.get_current_instruction()
try:
@ -1569,6 +1993,11 @@ class Instruction:
@StateTransition()
def staticcall_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
# TODO: implement me
instr = global_state.get_current_instruction()
try:

@ -1,18 +1,38 @@
"""This module contains a function manager to deal with symbolic Keccak
values."""
from mythril.laser.smt import Expression
class KeccakFunctionManager:
"""A keccak function manager for symbolic expressions."""
def __init__(self):
""""""
self.keccak_expression_mapping = {}
def is_keccak(self, expression: Expression) -> bool:
"""
:param expression:
:return:
"""
return str(expression) in self.keccak_expression_mapping.keys()
def get_argument(self, expression: str) -> Expression:
"""
:param expression:
:return:
"""
if not self.is_keccak(expression):
raise ValueError("Expression is not a recognized keccac result")
return self.keccak_expression_mapping[str(expression)][1]
def add_keccak(self, expression: Expression, argument: Expression) -> None:
"""
:param expression:
:param argument:
"""
index = str(expression)
self.keccak_expression_mapping[index] = (expression, argument)

@ -1,27 +1,34 @@
# -*- coding: utf8 -*-
"""This nodule defines helper functions to deal with native calls."""
import hashlib
import logging
from typing import Union, List
from typing import List, Union
from ethereum.utils import ecrecover_to_pub
from py_ecc.secp256k1 import N as secp256k1n
from rlp.utils import ALL_BYTES
from mythril.laser.ethereum.state.calldata import BaseCalldata, ConcreteCalldata
from mythril.laser.ethereum.util import bytearray_to_int, sha3, get_concrete_int
from mythril.laser.ethereum.util import bytearray_to_int, sha3
from mythril.laser.smt import Concat, simplify
log = logging.getLogger(__name__)
class NativeContractException(Exception):
"""An exception denoting an error during a native call."""
pass
def int_to_32bytes(
i: int
) -> bytes: # used because int can't fit as bytes function's input
"""
:param i:
:return:
"""
o = [0] * 32
for x in range(32):
o[31 - x] = i & 0xFF
@ -30,6 +37,12 @@ def int_to_32bytes(
def extract32(data: bytearray, i: int) -> int:
"""
:param data:
:param i:
:return:
"""
if i >= len(data):
return 0
o = data[i : min(i + 32, len(data))]
@ -38,6 +51,11 @@ def extract32(data: bytearray, i: int) -> int:
def ecrecover(data: Union[bytes, str, List[int]]) -> bytes:
"""
:param data:
:return:
"""
# TODO: Add type hints
try:
data = bytearray(data)
@ -60,6 +78,11 @@ def ecrecover(data: Union[bytes, str, List[int]]) -> bytes:
def sha256(data: Union[bytes, str, List[int]]) -> bytes:
"""
:param data:
:return:
"""
try:
data = bytes(data)
except TypeError:
@ -68,6 +91,11 @@ def sha256(data: Union[bytes, str, List[int]]) -> bytes:
def ripemd160(data: Union[bytes, str, List[int]]) -> bytes:
"""
:param data:
:return:
"""
try:
data = bytes(data)
except TypeError:
@ -78,6 +106,11 @@ def ripemd160(data: Union[bytes, str, List[int]]) -> bytes:
def identity(data: Union[bytes, str, List[int]]) -> bytes:
"""
:param data:
:return:
"""
# Group up into an array of 32 byte words instead
# of an array of bytes. If saved to memory, 32 byte
# words are currently needed, but a correct memory
@ -91,8 +124,11 @@ def identity(data: Union[bytes, str, List[int]]) -> bytes:
def native_contracts(address: int, data: BaseCalldata):
"""
takes integer address 1, 2, 3, 4
"""Takes integer address 1, 2, 3, 4.
:param address:
:param data:
:return:
"""
functions = (ecrecover, sha256, ripemd160, identity)

@ -1,19 +1,22 @@
from typing import Dict, Union, Any, KeysView
"""This module contains account-related functionality.
This includes classes representing accounts and their storage.
"""
from typing import Any, Dict, KeysView, Union
from z3 import ExprRef
from mythril.laser.smt import symbol_factory
from mythril.disassembler.disassembly import Disassembly
from mythril.laser.smt import symbol_factory
class Storage:
"""
Storage class represents the storage of an Account
"""
"""Storage class represents the storage of an Account."""
def __init__(self, concrete=False, address=None, dynamic_loader=None):
"""
Constructor for Storage
"""Constructor for Storage.
:param concrete: bool indicating whether to interpret uninitialized storage as concrete versus symbolic
"""
self._storage = {}
@ -52,13 +55,15 @@ class Storage:
self._storage[key] = value
def keys(self) -> KeysView:
"""
:return:
"""
return self._storage.keys()
class Account:
"""
Account class representing ethereum accounts
"""
"""Account class representing ethereum accounts."""
def __init__(
self,
@ -69,8 +74,8 @@ class Account:
concrete_storage=False,
dynamic_loader=None,
):
"""
Constructor for account
"""Constructor for account.
:param address: Address of the account
:param code: The contract code of the account
:param contract_name: The name associated with the account
@ -98,13 +103,25 @@ class Account:
return str(self.as_dict)
def set_balance(self, balance: ExprRef) -> None:
"""
:param balance:
"""
self.balance = balance
def add_balance(self, balance: ExprRef) -> None:
"""
:param balance:
"""
self.balance += balance
@property
def as_dict(self) -> Dict:
"""
:return:
"""
return {
"nonce": self.nonce,
"code": self.code,

@ -1,13 +1,21 @@
"""This module includes classes used for annotating trace information.
This includes the base StateAnnotation class, as well as an adaption,
which will not be copied on every new state.
"""
class StateAnnotation:
"""
The StateAnnotation class is used to persist information over traces. This allows modules to reason about traces
without the need to traverse the state space themselves.
"""The StateAnnotation class is used to persist information over traces.
This allows modules to reason about traces without the need to
traverse the state space themselves.
"""
@property
def persist_to_world_state(self) -> bool:
"""
If this function returns true then laser will also annotate the world state.
"""If this function returns true then laser will also annotate the
world state.
If you want annotations to persist through different user initiated message call transactions
then this should be enabled.
@ -18,10 +26,11 @@ class StateAnnotation:
class NoCopyAnnotation(StateAnnotation):
"""
This class provides a base annotation class for annotations that shouldn't be copied on every new state.
Rather the same object should be propagated.
This is very useful if you are looking to analyze a property over multiple substates
"""This class provides a base annotation class for annotations that
shouldn't be copied on every new state.
Rather the same object should be propagated. This is very useful if
you are looking to analyze a property over multiple substates
"""
def __copy__(self):

@ -1,26 +1,42 @@
"""This module declares classes to represent call data."""
from typing import Union, Any
from mythril.laser.smt import K, Array, If, simplify, Concat, Expression, BitVec
from mythril.laser.smt import symbol_factory
from mythril.laser.ethereum.util import get_concrete_int
from enum import Enum
from typing import Any, Union
from z3 import Model
from z3.z3types import Z3Exception
from mythril.laser.ethereum.util import get_concrete_int
from mythril.laser.smt import (
Array,
BitVec,
Concat,
Expression,
If,
K,
simplify,
symbol_factory,
)
class BaseCalldata:
"""
Base calldata class
This represents the calldata provided when sending a transaction to a contract
"""
"""Base calldata class This represents the calldata provided when sending a
transaction to a contract."""
def __init__(self, tx_id):
"""
:param tx_id:
"""
self.tx_id = tx_id
@property
def calldatasize(self) -> Expression:
"""
:return: Calldata size for this calldata object
"""
result = self.size
@ -29,11 +45,20 @@ class BaseCalldata:
return result
def get_word_at(self, offset: int) -> Expression:
""" Gets word at offset"""
"""Gets word at offset.
:param offset:
:return:
"""
parts = self[offset : offset + 32]
return simplify(Concat(parts))
def __getitem__(self, item: Union[int, slice]) -> Any:
"""
:param item:
:return:
"""
if isinstance(item, int) or isinstance(item, Expression):
return self._load(item)
@ -64,22 +89,34 @@ class BaseCalldata:
raise ValueError
def _load(self, item: Union[int, Expression]) -> Any:
"""
:param item:
"""
raise NotImplementedError()
@property
def size(self) -> Union[Expression, int]:
""" Returns the exact size of this calldata, this is not normalized"""
"""Returns the exact size of this calldata, this is not normalized.
:return: unnormalized call data size
"""
raise NotImplementedError()
def concrete(self, model: Model) -> list:
""" Returns a concrete version of the calldata using the provided model"""
"""Returns a concrete version of the calldata using the provided model.
:param model:
"""
raise NotImplementedError
class ConcreteCalldata(BaseCalldata):
"""A concrete call data representation."""
def __init__(self, tx_id: int, calldata: list):
"""
Initializes the ConcreteCalldata object
"""Initializes the ConcreteCalldata object.
:param tx_id: Id of the transaction that the calldata is for.
:param calldata: The concrete calldata content
"""
@ -96,21 +133,37 @@ class ConcreteCalldata(BaseCalldata):
super().__init__(tx_id)
def _load(self, item: Union[int, Expression]) -> BitVec:
"""
:param item:
:return:
"""
item = symbol_factory.BitVecVal(item, 256) if isinstance(item, int) else item
return simplify(self._calldata[item])
def concrete(self, model: Model) -> list:
"""
:param model:
:return:
"""
return self._concrete_calldata
@property
def size(self) -> int:
"""
:return:
"""
return len(self._concrete_calldata)
class BasicConcreteCalldata(BaseCalldata):
"""A base class to represent concrete call data."""
def __init__(self, tx_id: int, calldata: list):
"""
Initializes the ConcreteCalldata object, that doesn't use z3 arrays
"""Initializes the ConcreteCalldata object, that doesn't use z3 arrays.
:param tx_id: Id of the transaction that the calldata is for.
:param calldata: The concrete calldata content
"""
@ -118,6 +171,11 @@ class BasicConcreteCalldata(BaseCalldata):
super().__init__(tx_id)
def _load(self, item: Union[int, Expression]) -> Any:
"""
:param item:
:return:
"""
if isinstance(item, int):
try:
return self._calldata[item]
@ -130,17 +188,28 @@ class BasicConcreteCalldata(BaseCalldata):
return value
def concrete(self, model: Model) -> list:
"""
:param model:
:return:
"""
return self._calldata
@property
def size(self) -> int:
"""
:return:
"""
return len(self._calldata)
class SymbolicCalldata(BaseCalldata):
"""A class for representing symbolic call data."""
def __init__(self, tx_id: int):
"""
Initializes the SymbolicCalldata object
"""Initializes the SymbolicCalldata object.
:param tx_id: Id of the transaction that the calldata is for.
"""
self._size = symbol_factory.BitVecSym(str(tx_id) + "_calldatasize", 256)
@ -148,6 +217,11 @@ class SymbolicCalldata(BaseCalldata):
super().__init__(tx_id)
def _load(self, item: Union[int, Expression]) -> Any:
"""
:param item:
:return:
"""
item = symbol_factory.BitVecVal(item, 256) if isinstance(item, int) else item
return simplify(
If(
@ -158,6 +232,11 @@ class SymbolicCalldata(BaseCalldata):
)
def concrete(self, model: Model) -> list:
"""
:param model:
:return:
"""
concrete_length = model.eval(self.size.raw, model_completion=True).as_long()
result = []
for i in range(concrete_length):
@ -169,13 +248,19 @@ class SymbolicCalldata(BaseCalldata):
@property
def size(self) -> Expression:
"""
:return:
"""
return self._size
class BasicSymbolicCalldata(BaseCalldata):
"""A basic class representing symbolic call data."""
def __init__(self, tx_id: int):
"""
Initializes the SymbolicCalldata object
"""Initializes the SymbolicCalldata object.
:param tx_id: Id of the transaction that the calldata is for.
"""
self._reads = []
@ -199,6 +284,11 @@ class BasicSymbolicCalldata(BaseCalldata):
return simplify(return_value)
def concrete(self, model: Model) -> list:
"""
:param model:
:return:
"""
concrete_length = get_concrete_int(model.eval(self.size, model_completion=True))
result = []
for i in range(concrete_length):
@ -210,4 +300,8 @@ class BasicSymbolicCalldata(BaseCalldata):
@property
def size(self) -> Expression:
"""
:return:
"""
return self._size

@ -1,35 +1,77 @@
"""This module contains the class used to represent state-change constraints in
the call graph."""
class Constraints(list):
"""
This class should maintain a solver and it's constraints, This class tries to make the Constraints() object
as a simple list of constraints with some background processing.
"""This class should maintain a solver and it's constraints, This class
tries to make the Constraints() object as a simple list of constraints with
some background processing.
TODO: add the solver to this class after callback refactor
"""
def __init__(self, constraint_list=None, solver=None, possibility=None):
"""
:param constraint_list:
:param solver:
:param possibility:
"""
super(Constraints, self).__init__(constraint_list or [])
self.solver = solver
self.__possibility = possibility
def check_possibility(self):
"""
:return:
"""
return True
def append(self, constraint):
"""
:param constraint:
"""
super(Constraints, self).append(constraint)
def pop(self, index=-1):
"""
:param index:
"""
raise NotImplementedError
def __copy__(self):
"""
:return:
"""
constraint_list = super(Constraints, self).copy()
return Constraints(constraint_list)
def __deepcopy__(self, memodict=None):
"""
:param memodict:
:return:
"""
return self.__copy__()
def __add__(self, constraints):
"""
:param constraints:
:return:
"""
constraints_list = super(Constraints, self).__add__(constraints)
return Constraints(constraint_list=constraints_list)
def __iadd__(self, constraints):
"""
:param constraints:
:return:
"""
super(Constraints, self).__iadd__(constraints)
return self

@ -1,16 +1,17 @@
"""This module contains the representation for an execution state's
environment."""
from typing import Dict
from z3 import ExprRef, BitVecVal
from z3 import ExprRef
from mythril.laser.smt import symbol_factory
from mythril.laser.ethereum.state.account import Account
from mythril.laser.ethereum.state.calldata import BaseCalldata
from mythril.laser.smt import symbol_factory
class Environment:
"""
The environment class represents the current execution environment for the symbolic executor
"""
"""The environment class represents the current execution environment for
the symbolic executor."""
def __init__(
self,
@ -22,6 +23,17 @@ class Environment:
origin: ExprRef,
code=None,
):
"""
:param active_account:
:param sender:
:param calldata:
:param gasprice:
:param callvalue:
:param origin:
:param code:
:param calldata_type:
"""
# Metadata
self.active_account = active_account
@ -39,10 +51,18 @@ class Environment:
self.callvalue = callvalue
def __str__(self) -> str:
"""
:return:
"""
return str(self.as_dict)
@property
def as_dict(self) -> Dict:
"""
:return:
"""
return dict(
active_account=self.active_account,
sender=self.sender,

@ -1,3 +1,4 @@
"""This module contains a representation of the global execution state."""
from typing import Dict, Union, List, Iterable
from copy import copy, deepcopy
@ -11,9 +12,7 @@ from mythril.laser.ethereum.state.annotation import StateAnnotation
class GlobalState:
"""
GlobalState represents the current globalstate
"""
"""GlobalState represents the current globalstate."""
def __init__(
self,
@ -25,7 +24,16 @@ class GlobalState:
last_return_data=None,
annotations=None,
):
""" Constructor for GlobalState"""
"""Constructor for GlobalState.
:param world_state:
:param environment:
:param node:
:param machine_state:
:param transaction_stack:
:param last_return_data:
:param annotations:
"""
self.node = node
self.world_state = world_state
self.environment = environment
@ -38,6 +46,10 @@ class GlobalState:
self._annotations = annotations or []
def __copy__(self) -> "GlobalState":
"""
:return:
"""
world_state = copy(self.world_state)
environment = copy(self.environment)
mstate = deepcopy(self.mstate)
@ -54,11 +66,18 @@ class GlobalState:
@property
def accounts(self) -> Dict:
"""
:return:
"""
return self.world_state.accounts
# TODO: remove this, as two instructions are confusing
def get_current_instruction(self) -> Dict:
""" Gets the current instruction for this GlobalState"""
"""Gets the current instruction for this GlobalState.
:return:
"""
instructions = self.environment.code.instruction_list
return instructions[self.mstate.pc]
@ -67,6 +86,10 @@ class GlobalState:
def current_transaction(
self
) -> Union["MessageCallTransaction", "ContractCreationTransaction", None]:
"""
:return:
"""
# TODO: Remove circular to transaction package to import Transaction classes
try:
return self.transaction_stack[-1][0]
@ -75,13 +98,27 @@ class GlobalState:
@property
def instruction(self) -> Dict:
"""
:return:
"""
return self.get_current_instruction()
def new_bitvec(self, name: str, size=256) -> BitVec:
"""
:param name:
:param size:
:return:
"""
transaction_id = self.current_transaction.id
return symbol_factory.BitVecSym("{}_{}".format(transaction_id, name), size)
def annotate(self, annotation: StateAnnotation) -> None:
"""
:param annotation:
"""
self._annotations.append(annotation)
if annotation.persist_to_world_state:
@ -89,12 +126,17 @@ class GlobalState:
@property
def annotations(self) -> List[StateAnnotation]:
"""
:return:
"""
return self._annotations
def get_annotations(self, annotation_type: type) -> Iterable[StateAnnotation]:
"""
Filters annotations for the queried annotation type. Designed particularly for
modules with annotations: globalstate.get_annotations(MySpecificModuleAnnotation)
"""Filters annotations for the queried annotation type. Designed
particularly for modules with annotations:
globalstate.get_annotations(MySpecificModuleAnnotation)
:param annotation_type: The type to filter annotations for
:return: filter of matching annotations
"""

@ -1,3 +1,5 @@
"""This module contains a representation of the EVM's machine state and its
stack."""
from copy import copy
from typing import Union, Any, List, Dict
@ -14,13 +16,15 @@ from mythril.laser.ethereum.state.memory import Memory
class MachineStack(list):
"""
Defines EVM stack, overrides the default list to handle overflows
"""
"""Defines EVM stack, overrides the default list to handle overflows."""
STACK_LIMIT = 1024
def __init__(self, default_list=None):
"""
:param default_list:
"""
if default_list is None:
default_list = []
super(MachineStack, self).__init__(default_list)
@ -50,6 +54,11 @@ class MachineStack(list):
raise StackUnderflowException("Trying to pop from an empty stack")
def __getitem__(self, item: Union[int, slice]) -> Any:
"""
:param item:
:return:
"""
try:
return super(MachineStack, self).__getitem__(item)
except IndexError:
@ -58,21 +67,22 @@ class MachineStack(list):
)
def __add__(self, other):
"""
Implement list concatenation if needed
"""Implement list concatenation if needed.
:param other:
"""
raise NotImplementedError("Implement this if needed")
def __iadd__(self, other):
"""
Implement list concatenation if needed
"""Implement list concatenation if needed.
:param other:
"""
raise NotImplementedError("Implement this if needed")
class MachineState:
"""
MachineState represents current machine state also referenced to as \mu
"""MachineState represents current machine state also referenced to as \mu.
"""
def __init__(
@ -86,7 +96,17 @@ class MachineState:
max_gas_used=0,
min_gas_used=0,
):
""" Constructor for machineState """
"""Constructor for machineState.
:param gas_limit:
:param pc:
:param stack:
:param memory:
:param constraints:
:param depth:
:param max_gas_used:
:param min_gas_used:
"""
self.pc = pc
self.stack = MachineStack(stack)
self.memory = memory or Memory()
@ -97,11 +117,23 @@ class MachineState:
self.depth = depth
def calculate_extension_size(self, start: int, size: int) -> int:
"""
:param start:
:param size:
:return:
"""
if self.memory_size > start + size:
return 0
return start + size - self.memory_size
def calculate_memory_gas(self, start: int, size: int):
"""
:param start:
:param size:
:return:
"""
# https://github.com/ethereum/pyethereum/blob/develop/ethereum/vm.py#L148
oldsize = self.memory_size // 32
old_totalfee = (
@ -114,12 +146,13 @@ class MachineState:
return new_totalfee - old_totalfee
def check_gas(self):
"""Check whether the machine is out of gas."""
if self.min_gas_used > self.gas_limit:
raise OutOfGasException()
def mem_extend(self, start: int, size: int) -> None:
"""
Extends the memory of this machine state
"""Extends the memory of this machine state.
:param start: Start of memory extension
:param size: Size of memory extension
"""
@ -132,12 +165,20 @@ class MachineState:
self.memory.extend(m_extend)
def memory_write(self, offset: int, data: List[int]) -> None:
""" Writes data to memory starting at offset """
"""Writes data to memory starting at offset.
:param offset:
:param data:
"""
self.mem_extend(offset, len(data))
self.memory[offset : offset + len(data)] = data
def pop(self, amount=1) -> Union[BitVec, List[BitVec]]:
""" Pops amount elements from the stack"""
"""Pops amount elements from the stack.
:param amount:
:return:
"""
if amount > len(self.stack):
raise StackUnderflowException
values = self.stack[-amount:][::-1]
@ -146,6 +187,11 @@ class MachineState:
return values[0] if amount == 1 else values
def __deepcopy__(self, memodict=None):
"""
:param memodict:
:return:
"""
memodict = {} if memodict is None else memodict
return MachineState(
gas_limit=self.gas_limit,
@ -159,14 +205,26 @@ class MachineState:
)
def __str__(self):
"""
:return:
"""
return str(self.as_dict)
@property
def memory_size(self) -> int:
"""
:return:
"""
return len(self.memory)
@property
def as_dict(self) -> Dict:
"""
:return:
"""
return dict(
pc=self.pc,
stack=self.stack,

@ -1,30 +1,44 @@
"""This module contains a representation of a smart contract's memory."""
from typing import Union
from z3 import Z3Exception
from mythril.laser.ethereum import util
from mythril.laser.smt import (
BitVec,
symbol_factory,
If,
Concat,
simplify,
Bool,
Concat,
Extract,
If,
simplify,
symbol_factory,
)
from mythril.laser.ethereum import util
class Memory:
"""A class representing contract memory with random access."""
def __init__(self):
""""""
self._memory = []
def __len__(self):
"""
:return:
"""
return len(self._memory)
def extend(self, size):
"""
:param size:
"""
self._memory.extend(bytearray(size))
def get_word_at(self, index: int) -> Union[int, BitVec]:
"""
Access a word from a specified memory index
"""Access a word from a specified memory index.
:param index: integer representing the index to access
:return: 32 byte word at the specified index
"""
@ -49,8 +63,8 @@ class Memory:
return result
def write_word_at(self, index: int, value: Union[int, BitVec, bool, Bool]) -> None:
"""
Writes a 32 byte word to memory at the specified index`
"""Writes a 32 byte word to memory at the specified index`
:param index: index to write to
:param value: the value to write to memory
"""
@ -81,6 +95,11 @@ class Memory:
self[index + 31 - (i // 8)] = Extract(i + 7, i, value_to_write)
def __getitem__(self, item: Union[int, slice]) -> Union[BitVec, int, list]:
"""
:param item:
:return:
"""
if isinstance(item, slice):
start, step, stop = item.start, item.step, item.stop
if start is None:
@ -97,6 +116,11 @@ class Memory:
return 0
def __setitem__(self, key: Union[int, slice], value: Union[BitVec, int, list]):
"""
:param key:
:param value:
"""
if isinstance(key, slice):
start, step, stop = key.start, key.step, key.stop

@ -1,3 +1,4 @@
"""This module contains a representation of the EVM's world state."""
from copy import copy
from random import randint
from typing import List, Iterator
@ -7,15 +8,16 @@ from mythril.laser.ethereum.state.annotation import StateAnnotation
class WorldState:
"""
The WorldState class represents the world state as described in the yellow paper
"""
"""The WorldState class represents the world state as described in the
yellow paper."""
def __init__(
self, transaction_sequence=None, annotations: List[StateAnnotation] = None
) -> None:
"""
Constructor for the world state. Initializes the accounts record
"""Constructor for the world state. Initializes the accounts record.
:param transaction_sequence:
:param annotations:
"""
self.accounts = {}
self.node = None
@ -23,14 +25,18 @@ class WorldState:
self._annotations = annotations or []
def __getitem__(self, item: str) -> Account:
"""
Gets an account from the worldstate using item as key
"""Gets an account from the worldstate using item as key.
:param item: Address of the account to get
:return: Account associated with the address
"""
return self.accounts[item]
def __copy__(self) -> "WorldState":
"""
:return:
"""
new_annotations = [copy(a) for a in self._annotations]
new_world_state = WorldState(
transaction_sequence=self.transaction_sequence[:],
@ -43,8 +49,8 @@ class WorldState:
def create_account(
self, balance=0, address=None, concrete_storage=False, dynamic_loader=None
) -> Account:
"""
Create non-contract account
"""Create non-contract account.
:param address: The account's address
:param balance: Initial balance for the account
:param concrete_storage: Interpret account storage as concrete
@ -62,9 +68,10 @@ class WorldState:
return new_account
def create_initialized_contract_account(self, contract_code, storage) -> None:
"""
Creates a new contract account, based on the contract code and storage provided
The contract code only includes the runtime contract bytecode
"""Creates a new contract account, based on the contract code and
storage provided The contract code only includes the runtime contract
bytecode.
:param contract_code: Runtime bytecode for the contract
:param storage: Initial storage for the contract
:return: The new account
@ -77,27 +84,43 @@ class WorldState:
self._put_account(new_account)
def annotate(self, annotation: StateAnnotation) -> None:
"""
:param annotation:
"""
self._annotations.append(annotation)
@property
def annotations(self) -> List[StateAnnotation]:
"""
:return:
"""
return self._annotations
def get_annotations(self, annotation_type: type) -> Iterator[StateAnnotation]:
"""
Filters annotations for the queried annotation type. Designed particularly for
modules with annotations: worldstate.get_annotations(MySpecificModuleAnnotation)
"""Filters annotations for the queried annotation type. Designed
particularly for modules with annotations:
worldstate.get_annotations(MySpecificModuleAnnotation)
:param annotation_type: The type to filter annotations for
:return: filter of matching annotations
"""
return filter(lambda x: isinstance(x, annotation_type), self.annotations)
def _generate_new_address(self) -> str:
""" Generates a new address for the global state"""
"""Generates a new address for the global state.
:return:
"""
while True:
address = "0x" + "".join([str(hex(randint(0, 16)))[-1] for _ in range(20)])
if address not in self.accounts.keys():
return address
def _put_account(self, account: Account) -> None:
"""
:param account:
"""
self.accounts[account.address] = account

@ -2,6 +2,8 @@ from abc import ABC, abstractmethod
class BasicSearchStrategy(ABC):
""""""
__slots__ = "work_list", "max_depth"
def __init__(self, work_list, max_depth):
@ -13,6 +15,7 @@ class BasicSearchStrategy(ABC):
@abstractmethod
def get_strategic_global_state(self):
""""""
raise NotImplementedError("Must be implemented by a subclass")
def __next__(self):

@ -1,9 +1,7 @@
"""
This module implements basic symbolic execution search strategies
"""
from mythril.laser.ethereum.state.global_state import GlobalState
from typing import List
"""This module implements basic symbolic execution search strategies."""
from random import randrange
from mythril.laser.ethereum.state.global_state import GlobalState
from . import BasicSearchStrategy
try:
@ -16,8 +14,8 @@ except ImportError:
from bisect import bisect
def choices(population, weights=None):
"""
Returns a random element out of the population based on weight.
"""Returns a random element out of the population based on weight.
If the relative weights or cumulative weights are not specified,
the selections are made with equal probability.
"""
@ -32,31 +30,41 @@ except ImportError:
class DepthFirstSearchStrategy(BasicSearchStrategy):
"""
Implements a depth first search strategy
I.E. Follow one path to a leaf, and then continue to the next one
"""Implements a depth first search strategy I.E.
Follow one path to a leaf, and then continue to the next one
"""
def get_strategic_global_state(self) -> GlobalState:
"""
:return:
"""
return self.work_list.pop()
class BreadthFirstSearchStrategy(BasicSearchStrategy):
"""
Implements a breadth first search strategy
I.E. Execute all states of a "level" before continuing
"""Implements a breadth first search strategy I.E.
Execute all states of a "level" before continuing
"""
def get_strategic_global_state(self) -> GlobalState:
"""
:return:
"""
return self.work_list.pop(0)
class ReturnRandomNaivelyStrategy(BasicSearchStrategy):
"""
chooses a random state from the worklist with equal likelihood
"""
"""chooses a random state from the worklist with equal likelihood."""
def get_strategic_global_state(self) -> GlobalState:
"""
:return:
"""
if len(self.work_list) > 0:
return self.work_list.pop(randrange(len(self.work_list)))
else:
@ -64,11 +72,14 @@ class ReturnRandomNaivelyStrategy(BasicSearchStrategy):
class ReturnWeightedRandomStrategy(BasicSearchStrategy):
"""
chooses a random state from the worklist with likelihood based on inverse proportion to depth
"""
"""chooses a random state from the worklist with likelihood based on
inverse proportion to depth."""
def get_strategic_global_state(self) -> GlobalState:
"""
:return:
"""
probability_distribution = [
1 / (global_state.mstate.depth + 1) for global_state in self.work_list
]

@ -1,10 +1,13 @@
"""This module implements the main symbolic execution engine."""
import logging
from collections import defaultdict
from copy import copy
from datetime import datetime, timedelta
from functools import reduce
from typing import List, Tuple, Union, Callable, Dict
from typing import Callable, Dict, List, Tuple, Union
from mythril import alarm
from mythril.exceptions import OutOfTimeError
from mythril.laser.ethereum.cfg import NodeFlags, Node, Edge, JumpType
from mythril.laser.ethereum.evm_exceptions import StackUnderflowException
from mythril.laser.ethereum.evm_exceptions import VmException
@ -14,11 +17,9 @@ from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.laser.ethereum.state.world_state import WorldState
from mythril.laser.ethereum.strategy.basic import DepthFirstSearchStrategy
from mythril.laser.ethereum.transaction import (
TransactionStartSignal,
TransactionEndSignal,
ContractCreationTransaction,
)
from mythril.laser.ethereum.transaction import (
TransactionEndSignal,
TransactionStartSignal,
execute_contract_creation,
execute_message_call,
)
@ -27,17 +28,20 @@ log = logging.getLogger(__name__)
class SVMError(Exception):
pass
"""An exception denoting an unexpected state in symbolic execution."""
"""
Main symbolic execution engine.
"""
pass
class LaserEVM:
"""
Laser EVM class
"""The LASER EVM.
Just as Mithril had to be mined at great efforts to provide the
Dwarves with their exceptional armour, LASER stands at the heart of
Mythril, digging deep in the depths of call graphs, unearthing the
most precious symbolic call data, that is then hand-forged into
beautiful and strong security issues by the experienced smiths we
call detection modules. It is truly a magnificent symbiosis.
"""
def __init__(
@ -51,6 +55,16 @@ class LaserEVM:
transaction_count=2,
requires_statespace=True,
):
"""
:param accounts:
:param dynamic_loader:
:param max_depth:
:param execution_timeout:
:param create_timeout:
:param strategy:
:param transaction_count:
"""
world_state = WorldState()
world_state.accounts = accounts
# this sets the initial world state
@ -67,7 +81,7 @@ class LaserEVM:
self.max_depth = max_depth
self.transaction_count = transaction_count
self.execution_timeout = execution_timeout
self.execution_timeout = execution_timeout or 0
self.create_timeout = create_timeout
self.requires_statespace = requires_statespace
@ -83,6 +97,11 @@ class LaserEVM:
log.info("LASER EVM initialized with dynamic loader: " + str(dynamic_loader))
def register_hooks(self, hook_type: str, hook_dict: Dict[str, List[Callable]]):
"""
:param hook_type:
:param hook_dict:
"""
if hook_type == "pre":
entrypoint = self.pre_hooks
elif hook_type == "post":
@ -97,35 +116,53 @@ class LaserEVM:
@property
def accounts(self) -> Dict[str, Account]:
"""
:return:
"""
return self.world_state.accounts
def sym_exec(
self, main_address=None, creation_code=None, contract_name=None
) -> None:
"""
:param main_address:
:param creation_code:
:param contract_name:
"""
log.debug("Starting LASER execution")
self.time = datetime.now()
if main_address:
log.info("Starting message call transaction to {}".format(main_address))
self._execute_transactions(main_address)
try:
alarm.start_timeout(self.execution_timeout)
self.time = datetime.now()
if main_address:
log.info("Starting message call transaction to {}".format(main_address))
self._execute_transactions(main_address)
elif creation_code:
log.info("Starting contract creation transaction")
created_account = execute_contract_creation(
self, creation_code, contract_name
)
log.info(
"Finished contract creation, found {} open states".format(
len(self.open_states)
elif creation_code:
log.info("Starting contract creation transaction")
created_account = execute_contract_creation(
self, creation_code, contract_name
)
)
if len(self.open_states) == 0:
log.warning(
"No contract was created during the execution of contract creation "
"Increase the resources for creation execution (--max-depth or --create-timeout)"
log.info(
"Finished contract creation, found {} open states".format(
len(self.open_states)
)
)
if len(self.open_states) == 0:
log.warning(
"No contract was created during the execution of contract creation "
"Increase the resources for creation execution (--max-depth or --create-timeout)"
)
self._execute_transactions(created_account.address)
self._execute_transactions(created_account.address)
except OutOfTimeError:
log.warning("Timeout occurred, ending symbolic execution")
finally:
alarm.disable_timeout()
log.info("Finished symbolic execution")
if self.requires_statespace:
@ -144,8 +181,9 @@ class LaserEVM:
log.info("Achieved {:.2f}% coverage for code: {}".format(cov, code))
def _execute_transactions(self, address):
"""
This function executes multiple transactions on the address based on the coverage
"""This function executes multiple transactions on the address based on
the coverage.
:param address: Address of the contract
:return:
"""
@ -170,7 +208,11 @@ class LaserEVM:
)
def _get_covered_instructions(self) -> int:
""" Gets the total number of covered instructions for all accounts in the svm"""
"""Gets the total number of covered instructions for all accounts in
the svm.
:return:
"""
total_covered_instructions = 0
for _, cv in self.coverage.items():
total_covered_instructions += reduce(
@ -179,17 +221,20 @@ class LaserEVM:
return total_covered_instructions
def exec(self, create=False, track_gas=False) -> Union[List[GlobalState], None]:
"""
:param create:
:param track_gas:
:return:
"""
final_states = []
for global_state in self.strategy:
if self.execution_timeout and not create:
if (
self.time + timedelta(seconds=self.execution_timeout)
<= datetime.now()
):
return final_states + [global_state] if track_gas else None
elif self.create_timeout and create:
if self.time + timedelta(seconds=self.create_timeout) <= datetime.now():
return final_states + [global_state] if track_gas else None
if (
self.create_timeout
and create
and self.time + timedelta(seconds=self.create_timeout) <= datetime.now()
):
return final_states + [global_state] if track_gas else None
try:
new_states, op_code = self.execute_state(global_state)
@ -208,6 +253,11 @@ class LaserEVM:
def execute_state(
self, global_state: GlobalState
) -> Tuple[List[GlobalState], Union[str, None]]:
"""
:param global_state:
:return:
"""
instructions = global_state.environment.code.instruction_list
try:
op_code = instructions[global_state.mstate.pc]["opcode"]
@ -288,6 +338,14 @@ class LaserEVM:
revert_changes=False,
return_data=None,
) -> List[GlobalState]:
"""
:param return_global_state:
:param global_state:
:param revert_changes:
:param return_data:
:return:
"""
# Resume execution of the transaction initializing instruction
op_code = return_global_state.environment.code.instruction_list[
return_global_state.mstate.pc
@ -313,6 +371,10 @@ class LaserEVM:
return new_global_states
def _measure_coverage(self, global_state: GlobalState) -> None:
"""
:param global_state:
"""
code = global_state.environment.code.bytecode
number_of_instructions = len(global_state.environment.code.instruction_list)
instruction_index = global_state.mstate.pc
@ -326,6 +388,11 @@ class LaserEVM:
self.coverage[code][1][instruction_index] = True
def manage_cfg(self, opcode: str, new_states: List[GlobalState]) -> None:
"""
:param opcode:
:param new_states:
"""
if opcode == "JUMP":
assert len(new_states) <= 1
for state in new_states:
@ -363,6 +430,12 @@ class LaserEVM:
def _new_node_state(
self, state: GlobalState, edge_type=JumpType.UNCONDITIONAL, condition=None
) -> None:
"""
:param state:
:param edge_type:
:param condition:
"""
new_node = Node(state.environment.active_account.contract_name)
old_node = state.node
state.node = new_node
@ -408,6 +481,12 @@ class LaserEVM:
new_node.function_name = environment.active_function_name
def _execute_pre_hook(self, op_code: str, global_state: GlobalState) -> None:
"""
:param op_code:
:param global_state:
:return:
"""
if op_code not in self.pre_hooks.keys():
return
for hook in self.pre_hooks[op_code]:
@ -416,6 +495,12 @@ class LaserEVM:
def _execute_post_hook(
self, op_code: str, global_states: List[GlobalState]
) -> None:
"""
:param op_code:
:param global_states:
:return:
"""
if op_code not in self.post_hooks.keys():
return
@ -424,7 +509,18 @@ class LaserEVM:
hook(global_state)
def pre_hook(self, op_code: str) -> Callable:
"""
:param op_code:
:return:
"""
def hook_decorator(func: Callable):
"""
:param func:
:return:
"""
if op_code not in self.pre_hooks.keys():
self.pre_hooks[op_code] = []
self.pre_hooks[op_code].append(func)
@ -433,7 +529,18 @@ class LaserEVM:
return hook_decorator
def post_hook(self, op_code: str) -> Callable:
"""
:param op_code:
:return:
"""
def hook_decorator(func: Callable):
"""
:param func:
:return:
"""
if op_code not in self.post_hooks.keys():
self.post_hooks[op_code] = []
self.post_hooks[op_code].append(func)

@ -1,53 +1,72 @@
import logging
"""This module implements classes needed to perform taint analysis."""
import copy
from typing import Union, List, Tuple
import logging
from typing import List, Tuple, Union
import mythril.laser.ethereum.util as helper
from mythril.analysis.symbolic import SymExecWrapper
from mythril.laser.ethereum.cfg import JumpType, Node
from mythril.laser.ethereum.state.environment import Environment
from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.analysis.symbolic import SymExecWrapper
from mythril.laser.smt import Expression
log = logging.getLogger(__name__)
class TaintRecord:
"""
TaintRecord contains tainting information for a specific (state, node)
the information specifies the taint status before executing the operation belonging to the state
"""
"""TaintRecord contains tainting information for a specific (state, node)
the information specifies the taint status before executing the operation
belonging to the state."""
def __init__(self):
""" Builds a taint record """
"""Builds a taint record."""
self.stack = []
self.memory = {}
self.storage = {}
self.states = []
def stack_tainted(self, index: int) -> Union[bool, None]:
""" Returns taint value of stack element at index"""
"""Returns taint value of stack element at index.
:param index:
:return:
"""
if index < len(self.stack):
return self.stack[index]
return None
def memory_tainted(self, index: int) -> bool:
""" Returns taint value of memory element at index"""
"""Returns taint value of memory element at index.
:param index:
:return:
"""
if index in self.memory.keys():
return self.memory[index]
return False
def storage_tainted(self, index: int) -> bool:
""" Returns taint value of storage element at index"""
"""Returns taint value of storage element at index.
:param index:
:return:
"""
if index in self.storage.keys():
return self.storage[index]
return False
def add_state(self, state: GlobalState) -> None:
""" Adds state with this taint record """
"""Adds state with this taint record.
:param state:
"""
self.states.append(state)
def clone(self) -> "TaintRecord":
""" Clones this record"""
"""Clones this record.
:return:
"""
clone = TaintRecord()
clone.stack = copy.deepcopy(self.stack)
clone.memory = copy.deepcopy(self.memory)
@ -56,14 +75,16 @@ class TaintRecord:
class TaintResult:
""" Taint analysis result obtained after having ran the taint runner"""
"""Taint analysis result obtained after having ran the taint runner."""
def __init__(self):
"""Create a new tains result."""
self.records = []
def check(self, state: GlobalState, stack_index: int) -> Union[bool, None]:
"""
Checks if stack variable is tainted, before executing the instruction
"""Checks if stack variable is tainted, before executing the
instruction.
:param state: state to check variable in
:param stack_index: index of stack variable
:return: tainted
@ -74,11 +95,18 @@ class TaintResult:
return record.stack_tainted(stack_index)
def add_records(self, records: List[TaintRecord]) -> None:
""" Adds records to this taint result """
"""Adds records to this taint result.
:param records:
"""
self.records += records
def _try_get_record(self, state: GlobalState) -> Union[TaintRecord, None]:
""" Finds record belonging to the state """
"""Finds record belonging to the state.
:param state:
:return:
"""
for record in self.records:
if state in record.states:
return record
@ -86,20 +114,19 @@ class TaintResult:
class TaintRunner:
"""
Taint runner, is able to run taint analysis on symbolic execution result
"""
"""Taint runner, is able to run taint analysis on symbolic execution
result."""
@staticmethod
def execute(
statespace: SymExecWrapper, node: Node, state: GlobalState, initial_stack=None
) -> TaintResult:
"""
Runs taint analysis on the statespace
"""Runs taint analysis on the statespace.
:param initial_stack:
:param statespace: symbolic statespace to run taint analysis on
:param node: taint introduction node
:param state: taint introduction state
:param stack_indexes: stack indexes to introduce taint
:return: TaintResult object containing analysis results
"""
if initial_stack is None:
@ -136,6 +163,14 @@ class TaintRunner:
environment: Environment,
transaction_stack_length: int,
) -> List[Node]:
"""
:param node:
:param statespace:
:param environment:
:param transaction_stack_length:
:return:
"""
direct_children = [
statespace.nodes[edge.node_to]
for edge in statespace.edges
@ -161,8 +196,8 @@ class TaintRunner:
def execute_node(
node: Node, last_record: TaintRecord, state_index=0
) -> List[TaintRecord]:
"""
Runs taint analysis on a given node
"""Runs taint analysis on a given node.
:param node: node to analyse
:param last_record: last taint record to work from
:param state_index: state index to start from
@ -176,6 +211,12 @@ class TaintRunner:
@staticmethod
def execute_state(record: TaintRecord, state: GlobalState) -> TaintRecord:
"""
:param record:
:param state:
:return:
"""
assert len(state.mstate.stack) == len(record.stack)
""" Runs taint analysis on a state """
record.add_state(state)
@ -212,6 +253,11 @@ class TaintRunner:
@staticmethod
def mutate_stack(record: TaintRecord, mutator: Tuple[int, int]) -> None:
"""
:param record:
:param mutator:
"""
pop, push = mutator
values = []
@ -225,16 +271,31 @@ class TaintRunner:
@staticmethod
def mutate_push(op: str, record: TaintRecord) -> None:
"""
:param op:
:param record:
"""
TaintRunner.mutate_stack(record, (0, 1))
@staticmethod
def mutate_dup(op: str, record: TaintRecord) -> None:
"""
:param op:
:param record:
"""
depth = int(op[3:])
index = len(record.stack) - depth
record.stack.append(record.stack[index])
@staticmethod
def mutate_swap(op: str, record: TaintRecord) -> None:
"""
:param op:
:param record:
"""
depth = int(op[4:])
l = len(record.stack) - 1
i = l - depth
@ -242,6 +303,12 @@ class TaintRunner:
@staticmethod
def mutate_mload(record: TaintRecord, op0: Expression) -> None:
"""
:param record:
:param op0:
:return:
"""
_ = record.stack.pop()
try:
index = helper.get_concrete_int(op0)
@ -254,6 +321,12 @@ class TaintRunner:
@staticmethod
def mutate_mstore(record: TaintRecord, op0: Expression) -> None:
"""
:param record:
:param op0:
:return:
"""
_, value_taint = record.stack.pop(), record.stack.pop()
try:
index = helper.get_concrete_int(op0)
@ -265,6 +338,12 @@ class TaintRunner:
@staticmethod
def mutate_sload(record: TaintRecord, op0: Expression) -> None:
"""
:param record:
:param op0:
:return:
"""
_ = record.stack.pop()
try:
index = helper.get_concrete_int(op0)
@ -277,6 +356,12 @@ class TaintRunner:
@staticmethod
def mutate_sstore(record: TaintRecord, op0: Expression) -> None:
"""
:param record:
:param op0:
:return:
"""
_, value_taint = record.stack.pop(), record.stack.pop()
try:
index = helper.get_concrete_int(op0)
@ -288,12 +373,22 @@ class TaintRunner:
@staticmethod
def mutate_log(record: TaintRecord, op: str) -> None:
"""
:param record:
:param op:
"""
depth = int(op[3:])
for _ in range(depth + 2):
record.stack.pop()
@staticmethod
def mutate_call(record: TaintRecord, op: str) -> None:
"""
:param record:
:param op:
"""
pops = 6
if op in ("CALL", "CALLCODE"):
pops += 1

@ -1,3 +1,5 @@
"""This module contains functions to set up and execute concolic message
calls."""
from typing import List, Union
from mythril.disassembler.disassembly import Disassembly
@ -22,7 +24,20 @@ def execute_message_call(
value,
track_gas=False,
) -> Union[None, List[GlobalState]]:
""" Executes a message call transaction from all open states """
"""Execute a message call transaction from all open states.
:param laser_evm:
:param callee_address:
:param caller_address:
:param origin_address:
:param code:
:param data:
:param gas_limit:
:param gas_price:
:param value:
:param track_gas:
:return:
"""
# TODO: Resolve circular import between .transaction and ..svm to import LaserEVM here
open_states = laser_evm.open_states[:]
del laser_evm.open_states[:]
@ -48,7 +63,11 @@ def execute_message_call(
def _setup_global_state_for_execution(laser_evm, transaction) -> None:
""" Sets up global state and cfg for a transactions execution"""
"""Set up global state and cfg for a transactions execution.
:param laser_evm:
:param transaction:
"""
# TODO: Resolve circular import between .transaction and ..svm to import LaserEVM here
global_state = transaction.initial_global_state()
global_state.transaction_stack.append((transaction, None))

@ -1,3 +1,5 @@
"""This module contains functions setting up and executing transactions with
symbolic values."""
import logging
@ -19,7 +21,11 @@ ATTACKER_ADDRESS = 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF
def execute_message_call(laser_evm, callee_address: str) -> None:
""" Executes a message call transaction from all open states """
"""Executes a message call transaction from all open states.
:param laser_evm:
:param callee_address:
"""
# TODO: Resolve circular import between .transaction and ..svm to import LaserEVM here
open_states = laser_evm.open_states[:]
del laser_evm.open_states[:]
@ -55,7 +61,13 @@ def execute_message_call(laser_evm, callee_address: str) -> None:
def execute_contract_creation(
laser_evm, contract_initialization_code, contract_name=None
) -> Account:
""" Executes a contract creation transaction from all open states"""
"""Executes a contract creation transaction from all open states.
:param laser_evm:
:param contract_initialization_code:
:param contract_name:
:return:
"""
# TODO: Resolve circular import between .transaction and ..svm to import LaserEVM here
open_states = laser_evm.open_states[:]
del laser_evm.open_states[:]
@ -93,7 +105,11 @@ def execute_contract_creation(
def _setup_global_state_for_execution(laser_evm, transaction) -> None:
""" Sets up global state and cfg for a transactions execution"""
"""Sets up global state and cfg for a transactions execution.
:param laser_evm:
:param transaction:
"""
# TODO: Resolve circular import between .transaction and ..svm to import LaserEVM here
global_state = transaction.initial_global_state()
global_state.transaction_stack.append((transaction, None))

@ -1,26 +1,34 @@
"""This module contians the transaction models used throughout LASER's symbolic
execution."""
import array
from z3 import ExprRef
from typing import Union
from mythril.disassembler.disassembly import Disassembly
from mythril.laser.smt import symbol_factory
from mythril.laser.ethereum.state.environment import Environment
from mythril.laser.ethereum.state.calldata import BaseCalldata, SymbolicCalldata
from mythril.laser.ethereum.state.calldata import ConcreteCalldata
from mythril.laser.ethereum.state.account import Account
from mythril.laser.ethereum.state.world_state import WorldState
from mythril.laser.ethereum.state.calldata import BaseCalldata, SymbolicCalldata
from mythril.laser.ethereum.state.environment import Environment
from mythril.laser.ethereum.state.global_state import GlobalState
from z3 import ExprRef
import array
from mythril.laser.ethereum.state.world_state import WorldState
from mythril.disassembler.disassembly import Disassembly
from mythril.laser.smt import symbol_factory
_next_transaction_id = 0
def get_next_transaction_id() -> int:
"""
:return:
"""
global _next_transaction_id
_next_transaction_id += 1
return _next_transaction_id
class TransactionEndSignal(Exception):
""" Exception raised when a transaction is finalized"""
"""Exception raised when a transaction is finalized."""
def __init__(self, global_state: GlobalState, revert=False):
self.global_state = global_state
@ -28,7 +36,7 @@ class TransactionEndSignal(Exception):
class TransactionStartSignal(Exception):
""" Exception raised when a new transaction is started"""
"""Exception raised when a new transaction is started."""
def __init__(
self,
@ -79,7 +87,11 @@ class BaseTransaction:
if call_data is None and init_call_data:
self.call_data = SymbolicCalldata(self.id)
else:
self.call_data = call_data if isinstance(call_data, BaseCalldata) else None
self.call_data = (
call_data
if isinstance(call_data, BaseCalldata)
else ConcreteCalldata(self.id, [])
)
self.call_value = (
call_value
@ -90,6 +102,12 @@ class BaseTransaction:
self.return_data = None
def initial_global_state_from_environment(self, environment, active_function):
"""
:param environment:
:param active_function:
:return:
"""
# Initialize the execution environment
global_state = GlobalState(self.world_state, environment, None)
global_state.environment.active_function_name = active_function
@ -97,13 +115,13 @@ class BaseTransaction:
class MessageCallTransaction(BaseTransaction):
""" Transaction object models an transaction"""
"""Transaction object models an transaction."""
def __init__(self, *args, **kwargs):
super().__init__(*args, **kwargs)
def initial_global_state(self) -> GlobalState:
"""Initialize the execution environment"""
"""Initialize the execution environment."""
environment = Environment(
self.callee_account,
self.caller,
@ -118,12 +136,18 @@ class MessageCallTransaction(BaseTransaction):
)
def end(self, global_state: GlobalState, return_data=None, revert=False) -> None:
"""
:param global_state:
:param return_data:
:param revert:
"""
self.return_data = return_data
raise TransactionEndSignal(global_state, revert)
class ContractCreationTransaction(BaseTransaction):
""" Transaction object models an transaction"""
"""Transaction object models an transaction."""
def __init__(self, *args, **kwargs):
super().__init__(*args, **kwargs, init_call_data=False)
@ -133,7 +157,7 @@ class ContractCreationTransaction(BaseTransaction):
)
def initial_global_state(self) -> GlobalState:
"""Initialize the execution environment"""
"""Initialize the execution environment."""
environment = Environment(
self.callee_account,
self.caller,
@ -148,7 +172,12 @@ class ContractCreationTransaction(BaseTransaction):
)
def end(self, global_state: GlobalState, return_data=None, revert=False):
"""
:param global_state:
:param return_data:
:param revert:
"""
if (
not all([isinstance(element, int) for element in return_data])
or len(return_data) == 0

@ -1,13 +1,11 @@
"""This module contains various utility conversion functions and constants for
LASER."""
import re
from mythril.laser.smt import is_false, is_true, simplify, If, BitVec, Bool, Expression
from mythril.laser.smt import symbol_factory
import logging
from typing import Union, List, Dict
from typing import Dict, List, Union
import sha3 as _sha3
from mythril.laser.smt import BitVec, Bool, Expression, If, simplify, symbol_factory
TT256 = 2 ** 256
TT256M1 = 2 ** 256 - 1
@ -15,10 +13,20 @@ TT255 = 2 ** 255
def sha3(seed: str) -> bytes:
"""
:param seed:
:return:
"""
return _sha3.keccak_256(bytes(seed)).digest()
def safe_decode(hex_encoded_string: str) -> bytes:
"""
:param hex_encoded_string:
:return:
"""
if hex_encoded_string.startswith("0x"):
return bytes.fromhex(hex_encoded_string[2:])
else:
@ -26,12 +34,23 @@ def safe_decode(hex_encoded_string: str) -> bytes:
def to_signed(i: int) -> int:
"""
:param i:
:return:
"""
return i if i < TT255 else i - TT256
def get_instruction_index(
instruction_list: List[Dict], address: int
) -> Union[int, None]:
"""
:param instruction_list:
:param address:
:return:
"""
index = 0
for instr in instruction_list:
if instr["address"] == address:
@ -41,6 +60,12 @@ def get_instruction_index(
def get_trace_line(instr: Dict, state: "MachineState") -> str:
"""
:param instr:
:param state:
:return:
"""
stack = str(state.stack[::-1])
# stack = re.sub("(\d+)", lambda m: hex(int(m.group(1))), stack)
stack = re.sub("\n", "", stack)
@ -48,6 +73,11 @@ def get_trace_line(instr: Dict, state: "MachineState") -> str:
def pop_bitvec(state: "MachineState") -> BitVec:
"""
:param state:
:return:
"""
# pop one element from stack, converting boolean expressions and
# concrete Python variables to BitVecVal
@ -69,6 +99,11 @@ def pop_bitvec(state: "MachineState") -> BitVec:
def get_concrete_int(item: Union[int, Expression]) -> int:
"""
:param item:
:return:
"""
if isinstance(item, int):
return item
elif isinstance(item, BitVec):
@ -83,6 +118,12 @@ def get_concrete_int(item: Union[int, Expression]) -> int:
def concrete_int_from_bytes(concrete_bytes: bytes, start_index: int) -> int:
"""
:param concrete_bytes:
:param start_index:
:return:
"""
concrete_bytes = [
byte.value if isinstance(byte, BitVec) and not byte.symbolic else byte
for byte in concrete_bytes
@ -93,13 +134,23 @@ def concrete_int_from_bytes(concrete_bytes: bytes, start_index: int) -> int:
def concrete_int_to_bytes(val):
"""
:param val:
:return:
"""
# logging.debug("concrete_int_to_bytes " + str(val))
if type(val) == int:
return val.to_bytes(32, byteorder="big")
return (simplify(val).value).to_bytes(32, byteorder="big")
return simplify(val).value.to_bytes(32, byteorder="big")
def bytearray_to_int(arr):
"""
:param arr:
:return:
"""
o = 0
for a in arr:
o = (o << 8) + a

@ -23,9 +23,7 @@ import z3
class SymbolFactory:
"""
A symbol factory provides a default interface for all the components of mythril to create symbols
"""
"""A symbol factory provides a default interface for all the components of mythril to create symbols"""
@staticmethod
def Bool(value: bool, annotations=None):
@ -39,8 +37,8 @@ class SymbolFactory:
@staticmethod
def BitVecVal(value: int, size: int, annotations=None):
"""
Creates a new bit vector with a concrete value
"""Creates a new bit vector with a concrete value.
:param value: The concrete value to set the bit vector to
:param size: The size of the bit vector
:param annotations: The annotations to initialize the bit vector with
@ -50,8 +48,8 @@ class SymbolFactory:
@staticmethod
def BitVecSym(name: str, size: int, annotations=None):
"""
Creates a new bit vector with a symbolic value
"""Creates a new bit vector with a symbolic value.
:param name: The name of the symbolic bit vector
:param size: The size of the bit vector
:param annotations: The annotations to initialize the bit vector with
@ -79,13 +77,13 @@ class _SmtSymbolFactory(SymbolFactory):
@staticmethod
def BitVecVal(value: int, size: int, annotations=None):
""" Creates a new bit vector with a concrete value """
"""Creates a new bit vector with a concrete value."""
raw = z3.BitVecVal(value, size)
return BitVec(raw, annotations)
@staticmethod
def BitVecSym(name: str, size: int, annotations=None):
""" Creates a new bit vector with a symbolic value """
"""Creates a new bit vector with a symbolic value."""
raw = z3.BitVec(name, size)
return BitVec(raw, annotations)
@ -103,12 +101,12 @@ class _Z3SymbolFactory(SymbolFactory):
@staticmethod
def BitVecVal(value: int, size: int, annotations=None):
""" Creates a new bit vector with a concrete value """
"""Creates a new bit vector with a concrete value."""
return z3.BitVecVal(value, size)
@staticmethod
def BitVecSym(name: str, size: int, annotations=None):
""" Creates a new bit vector with a symbolic value """
"""Creates a new bit vector with a symbolic value."""
return z3.BitVec(name, size)

@ -1,14 +1,20 @@
from mythril.laser.smt.bitvec import BitVec
"""This module contains an SMT abstraction of arrays.
This includes an Array class to implement basic store and set
operations, as well as as a K-array, which can be initialized with
default values over a certain range.
"""
import z3
from mythril.laser.smt.bitvec import BitVec
class BaseArray:
"""
Base array type, implements basic store and set operations
"""
"""Base array type, which implements basic store and set operations."""
def __getitem__(self, item: BitVec):
""" Gets item from the array, item can be symbolic"""
"""Gets item from the array, item can be symbolic."""
if isinstance(item, slice):
raise ValueError(
"Instance of BaseArray, does not support getitem with slices"
@ -16,14 +22,16 @@ class BaseArray:
return BitVec(z3.Select(self.raw, item.raw))
def __setitem__(self, key: BitVec, value: BitVec):
""" Sets an item in the array, key can be symbolic"""
"""Sets an item in the array, key can be symbolic."""
self.raw = z3.Store(self.raw, key.raw, value.raw)
class Array(BaseArray):
"""A basic symbolic array."""
def __init__(self, name: str, domain: int, value_range: int):
"""
Initializes a symbolic array
"""Initializes a symbolic array.
:param name: Name of the array
:param domain: The domain for the array (10 -> all the values that a bv of size 10 could take)
:param value_range: The range for the values in the array (10 -> all the values that a bv of size 10 could take)
@ -34,9 +42,12 @@ class Array(BaseArray):
class K(BaseArray):
"""A basic symbolic array, which can be initialized with a default
value."""
def __init__(self, domain: int, value_range: int, value: int):
"""
Initializes an array with a default value
"""Initializes an array with a default value.
:param domain: The domain for the array (10 -> all the values that a bv of size 10 could take)
:param value_range: The range for the values in the array (10 -> all the values that a bv of size 10 could take)
:param value: The default value to use for this array

@ -1,39 +1,60 @@
"""This module provides classes for an SMT abstraction of bit vectors."""
from typing import Union
import z3
from mythril.laser.smt.expression import Expression
from mythril.laser.smt.bool import Bool
from mythril.laser.smt.expression import Expression
from typing import Union
# fmt: off
class BitVec(Expression):
"""
Bit vector symbol
"""
"""A bit vector symbol."""
def __init__(self, raw, annotations=None):
"""
:param raw:
:param annotations:
"""
super().__init__(raw, annotations)
def size(self):
"""TODO: documentation
:return:
"""
return self.raw.size()
@property
def symbolic(self):
""" Returns whether this symbol doesn't have a concrete value """
"""Returns whether this symbol doesn't have a concrete value.
:return:
"""
self.simplify()
return not isinstance(self.raw, z3.BitVecNumRef)
@property
def value(self):
""" Returns the value of this symbol if concrete, otherwise None"""
"""Returns the value of this symbol if concrete, otherwise None.
:return:
"""
if self.symbolic:
return None
assert isinstance(self.raw, z3.BitVecNumRef)
return self.raw.as_long()
def __add__(self, other) -> "BitVec":
""" Create an addition expression """
"""Create an addition expression.
:param other:
:return:
"""
if isinstance(other, int):
return BitVec(self.raw + other, annotations=self.annotations)
@ -41,7 +62,11 @@ class BitVec(Expression):
return BitVec(self.raw + other.raw, annotations=union)
def __sub__(self, other) -> "BitVec":
""" Create a subtraction expression """
"""Create a subtraction expression.
:param other:
:return:
"""
if isinstance(other, int):
return BitVec(self.raw - other, annotations=self.annotations)
@ -50,44 +75,76 @@ class BitVec(Expression):
return BitVec(self.raw - other.raw, annotations=union)
def __mul__(self, other) -> "BitVec":
""" Create a multiplication expression """
"""Create a multiplication expression.
:param other:
:return:
"""
union = self.annotations + other.annotations
return BitVec(self.raw * other.raw, annotations=union)
def __truediv__(self, other) -> "BitVec":
""" Create a signed division expression """
"""Create a signed division expression.
:param other:
:return:
"""
union = self.annotations + other.annotations
return BitVec(self.raw / other.raw, annotations=union)
def __and__(self, other) -> "BitVec":
""" Create an and expression """
"""Create an and expression.
:param other:
:return:
"""
if not isinstance(other, BitVec):
other = BitVec(z3.BitVecVal(other, 256))
union = self.annotations + other.annotations
return BitVec(self.raw & other.raw, annotations=union)
def __or__(self, other) -> "BitVec":
""" Create an or expression """
"""Create an or expression.
:param other:
:return:
"""
union = self.annotations + other.annotations
return BitVec(self.raw | other.raw, annotations=union)
def __xor__(self, other) -> "BitVec":
""" Create a xor expression """
"""Create a xor expression.
:param other:
:return:
"""
union = self.annotations + other.annotations
return BitVec(self.raw ^ other.raw, annotations=union)
def __lt__(self, other) -> Bool:
""" Create a signed less than expression """
"""Create a signed less than expression.
:param other:
:return:
"""
union = self.annotations + other.annotations
return Bool(self.raw < other.raw, annotations=union)
def __gt__(self, other) -> Bool:
""" Create a signed greater than expression """
"""Create a signed greater than expression.
:param other:
:return:
"""
union = self.annotations + other.annotations
return Bool(self.raw > other.raw, annotations=union)
def __eq__(self, other) -> Bool:
""" Create an equality expression """
"""Create an equality expression.
:param other:
:return:
"""
if not isinstance(other, BitVec):
return Bool(self.raw == other, annotations=self.annotations)
@ -95,7 +152,11 @@ class BitVec(Expression):
return Bool(self.raw == other.raw, annotations=union)
def __ne__(self, other) -> Bool:
""" Create an inequality expression """
"""Create an inequality expression.
:param other:
:return:
"""
if not isinstance(other, BitVec):
return Bool(self.raw != other, annotations=self.annotations)
@ -104,7 +165,13 @@ class BitVec(Expression):
def If(a: Bool, b: BitVec, c: BitVec):
""" Create an if-then-else expression """
"""Create an if-then-else expression.
:param a:
:param b:
:param c:
:return:
"""
if not isinstance(a, Expression):
a = Bool(z3.BoolVal(a))
if not isinstance(b, Expression):
@ -116,24 +183,44 @@ def If(a: Bool, b: BitVec, c: BitVec):
def UGT(a: BitVec, b: BitVec) -> Bool:
""" Create an unsigned greater than expression """
"""Create an unsigned greater than expression.
:param a:
:param b:
:return:
"""
annotations = a.annotations + b.annotations
return Bool(z3.UGT(a.raw, b.raw), annotations)
def UGE(a: BitVec, b:BitVec) -> Bool:
"""Create an unsigned greater or equals expression.
:param a:
:param b:
:return:
"""
annotations = a.annotations + b.annotations
return Bool(z3.UGE(a.raw, b.raw), annotations)
def ULT(a: BitVec, b: BitVec) -> Bool:
""" Create an unsigned less than expression """
"""Create an unsigned less than expression.
:param a:
:param b:
:return:
"""
annotations = a.annotations + b.annotations
return Bool(z3.ULT(a.raw, b.raw), annotations)
def Concat(*args) -> BitVec:
""" Create a concatenation expression """
"""Create a concatenation expression.
:param args:
:return:
"""
# The following statement is used if a list is provided as an argument to concat
if len(args) == 1 and isinstance(args[0], list):
@ -147,30 +234,54 @@ def Concat(*args) -> BitVec:
def Extract(high: int, low: int, bv: BitVec) -> BitVec:
""" Create an extract expression"""
"""Create an extract expression.
:param high:
:param low:
:param bv:
:return:
"""
return BitVec(z3.Extract(high, low, bv.raw), annotations=bv.annotations)
def URem(a: BitVec, b: BitVec) -> BitVec:
""" Create an unsigned remainder expression"""
"""Create an unsigned remainder expression.
:param a:
:param b:
:return:
"""
union = a.annotations + b.annotations
return BitVec(z3.URem(a.raw, b.raw), annotations=union)
def SRem(a: BitVec, b: BitVec) -> BitVec:
""" Create a signed remainder expression"""
"""Create a signed remainder expression.
:param a:
:param b:
:return:
"""
union = a.annotations + b.annotations
return BitVec(z3.SRem(a.raw, b.raw), annotations=union)
def UDiv(a: BitVec, b: BitVec) -> BitVec:
""" Create an unsigned division expression """
"""Create an unsigned division expression.
:param a:
:param b:
:return:
"""
union = a.annotations + b.annotations
return BitVec(z3.UDiv(a.raw, b.raw), annotations=union)
def Sum(*args) -> BitVec:
""" Create sum expression"""
"""Create sum expression.
:return:
"""
nraw = z3.Sum([a.raw for a in args])
annotations = []
for bv in args:
@ -179,7 +290,13 @@ def Sum(*args) -> BitVec:
def BVAddNoOverflow(a: Union[BitVec, int], b: Union[BitVec, int], signed: bool) -> Bool:
"""Creates predicate that verifies that the addition doesn't overflow"""
"""Creates predicate that verifies that the addition doesn't overflow.
:param a:
:param b:
:param signed:
:return:
"""
if not isinstance(a, Expression):
a = BitVec(z3.BitVecVal(a, 256))
if not isinstance(b, Expression):
@ -188,7 +305,14 @@ def BVAddNoOverflow(a: Union[BitVec, int], b: Union[BitVec, int], signed: bool)
def BVMulNoOverflow(a: Union[BitVec, int], b: Union[BitVec, int], signed: bool) -> Bool:
"""Creates predicate that verifies that the multiplication doesn't overflow"""
"""Creates predicate that verifies that the multiplication doesn't
overflow.
:param a:
:param b:
:param signed:
:return:
"""
if not isinstance(a, Expression):
a = BitVec(z3.BitVecVal(a, 256))
if not isinstance(b, Expression):
@ -197,7 +321,13 @@ def BVMulNoOverflow(a: Union[BitVec, int], b: Union[BitVec, int], signed: bool)
def BVSubNoUnderflow(a: Union[BitVec, int], b: Union[BitVec, int], signed: bool) -> Bool:
"""Creates predicate that verifies that the subtraction doesn't overflow"""
"""Creates predicate that verifies that the subtraction doesn't overflow.
:param a:
:param b:
:param signed:
:return:
"""
if not isinstance(a, Expression):
a = BitVec(z3.BitVecVal(a, 256))
if not isinstance(b, Expression):

@ -1,31 +1,43 @@
import z3
"""This module provides classes for an SMT abstraction of boolean
expressions."""
from typing import Union
import z3
from mythril.laser.smt.expression import Expression
# fmt: off
class Bool(Expression):
"""
This is a Bool expression
"""
"""This is a Bool expression."""
@property
def is_false(self) -> bool:
""" Specifies whether this variable can be simplified to false"""
"""Specifies whether this variable can be simplified to false.
:return:
"""
self.simplify()
return z3.is_false(self.raw)
@property
def is_true(self) -> bool:
""" Specifies whether this variable can be simplified to true"""
"""Specifies whether this variable can be simplified to true.
:return:
"""
self.simplify()
return z3.is_true(self.raw)
@property
def value(self) -> Union[bool, None]:
""" Returns the concrete value of this bool if concrete, otherwise None"""
"""Returns the concrete value of this bool if concrete, otherwise None.
:return: Concrete value or None
"""
self.simplify()
if self.is_true:
return True
@ -35,16 +47,30 @@ class Bool(Expression):
return None
def __eq__(self, other):
"""
:param other:
:return:
"""
if isinstance(other, Expression):
return Bool(self.raw == other.raw, self.annotations + other.annotations)
return Bool(self.raw == other, self.annotations)
def __ne__(self, other):
"""
:param other:
:return:
"""
if isinstance(other, Expression):
return Bool(self.raw != other.raw, self.annotations + other.annotations)
return Bool(self.raw != other, self.annotations)
def __bool__(self):
"""
:return:
"""
if self.value is not None:
return self.value
else:
@ -52,21 +78,38 @@ class Bool(Expression):
def Or(a: Bool, b: Bool):
""" Create an or expression"""
"""Create an or expression.
:param a:
:param b:
:return:
"""
union = a.annotations + b.annotations
return Bool(z3.Or(a.raw, b.raw), annotations=union)
def Not(a: Bool):
""" Create a Not expression"""
"""Create a Not expression.
:param a:
:return:
"""
return Bool(z3.Not(a.raw), a.annotations)
def is_false(a: Bool) -> bool:
""" Returns whether the provided bool can be simplified to false"""
"""Returns whether the provided bool can be simplified to false.
:param a:
:return:
"""
return z3.is_false(a.raw)
def is_true(a: Bool) -> bool:
""" Returns whether the provided bool can be simplified to true"""
"""Returns whether the provided bool can be simplified to true.
:param a:
:return:
"""
return z3.is_true(a.raw)

@ -1,29 +1,41 @@
"""This module contains the SMT abstraction for a basic symbol expression."""
import z3
class Expression:
"""
This is the base symbol class and maintains functionality for simplification and annotations
"""
"""This is the base symbol class and maintains functionality for
simplification and annotations."""
def __init__(self, raw, annotations=None):
"""
:param raw:
:param annotations:
"""
self.raw = raw
self._annotations = annotations or []
@property
def annotations(self):
""" Gets the annotations for this expression """
"""Gets the annotations for this expression.
:return:
"""
return self._annotations
def annotate(self, annotation):
""" Annotates this expression with the given annotation"""
"""Annotates this expression with the given annotation.
:param annotation:
"""
if isinstance(annotation, list):
self._annotations += annotation
else:
self._annotations.append(annotation)
def simplify(self):
""" Simplifies this expression """
"""Simplify this expression."""
self.raw = z3.simplify(self.raw)
def __repr__(self):
@ -31,6 +43,10 @@ class Expression:
def simplify(expression: Expression):
""" Simplifies the expression """
"""Simplify the expression .
:param expression:
:return:
"""
expression.simplify()
return expression

@ -1,22 +1,30 @@
"""This module contains an abstract SMT representation of an SMT solver."""
import z3
from mythril.laser.smt.bool import Bool
from mythril.laser.smt.expression import Expression
class Solver:
"""
An smt solver object
"""
"""An SMT solver object."""
def __init__(self):
""""""
self.raw = z3.Solver()
def set_timeout(self, timeout: int) -> None:
""" Sets the timeout that will be used by this solver, timeout is in milliseconds"""
"""Sets the timeout that will be used by this solver, timeout is in
milliseconds.
:param timeout:
"""
self.raw.set(timeout=timeout)
def add(self, constraints: list) -> None:
""" Adds the constraints to this solver """
"""Adds the constraints to this solver.
:param constraints:
:return:
"""
if not isinstance(constraints, list):
self.raw.add(constraints.raw)
return
@ -24,7 +32,11 @@ class Solver:
self.raw.add(constraints)
def append(self, constraints: list) -> None:
""" Adds the constraints to this solver """
"""Adds the constraints to this solver.
:param constraints:
:return:
"""
if not isinstance(constraints, list):
self.raw.append(constraints.raw)
return
@ -32,35 +44,49 @@ class Solver:
self.raw.add(constraints)
def check(self):
""" Returns z3 smt check result"""
"""Returns z3 smt check result.
:return:
"""
return self.raw.check()
def model(self):
""" Returns z3 model for a solution"""
"""Returns z3 model for a solution.
:return:
"""
return self.raw.model()
def reset(self) -> None:
""" Resets this solver """
"""Reset this solver."""
self.raw.reset()
def pop(self, num) -> None:
""" Pop num constraints from this solver """
"""Pop num constraints from this solver.
:param num:
"""
self.raw.pop(num)
class Optimize(Solver):
"""
An optimizing smt solver
"""
"""An optimizing smt solver."""
def __init__(self):
"""Create a new optimizing solver instance."""
super().__init__()
self.raw = z3.Optimize()
def minimize(self, element: Expression):
""" In solving this solver will try to minimize the passed expression """
"""In solving this solver will try to minimize the passed expression.
:param element:
"""
self.raw.minimize(element.raw)
def maximize(self, element: Expression):
""" In solving this solver will try to maximize the passed expression """
"""In solving this solver will try to maximize the passed expression.
:param element:
"""
self.raw.maximize(element.raw)

@ -5,27 +5,33 @@
http://www.github.com/b-mueller/mythril
"""
import codecs
import logging
import os
import platform
import re
import traceback
from pathlib import Path
from shutil import copyfile
from configparser import ConfigParser
import solc
from ethereum import utils
import codecs
from solc.exceptions import SolcError
import solc
from configparser import ConfigParser
import platform
from shutil import copyfile
from mythril.analysis.callgraph import generate_graph
from mythril.analysis.report import Report
from mythril.analysis.security import fire_lasers
from mythril.analysis.symbolic import SymExecWrapper
from mythril.analysis.traceexplore import get_serializable_statespace
from mythril.ethereum import util
from mythril.ethereum.evmcontract import EVMContract
from mythril.solidity.soliditycontract import SolidityContract, get_contracts_from_file
from mythril.ethereum.interface.leveldb.client import EthLevelDB
from mythril.ethereum.interface.rpc.client import EthJsonRpc
from mythril.ethereum.interface.rpc.exceptions import ConnectionError
from mythril.exceptions import CompilerError, CriticalError, NoContractFoundError
from mythril.solidity.soliditycontract import SolidityContract, get_contracts_from_file
from mythril.support import signatures
from mythril.support.truffle import analyze_truffle_project
from mythril.support.loader import DynLoader
from mythril.exceptions import CompilerError, NoContractFoundError, CriticalError
from mythril.analysis.symbolic import SymExecWrapper
@ -33,21 +39,22 @@ from mythril.analysis.callgraph import generate_graph
from mythril.analysis.traceexplore import get_serializable_statespace
from mythril.analysis.security import fire_lasers, retrieve_callback_issues
from mythril.analysis.report import Report
from mythril.support.truffle import analyze_truffle_project
from mythril.ethereum.interface.leveldb.client import EthLevelDB
log = logging.getLogger(__name__)
class Mythril(object):
"""
Mythril main interface class.
"""Mythril main interface class.
1. create mythril object
2. set rpc or leveldb interface if needed
3. load contracts (from solidity, bytecode, address)
4. fire_lasers
Example:
.. code-block:: python
mythril = Mythril()
mythril.set_api_rpc_infura()
@ -70,13 +77,13 @@ class Mythril(object):
# (optional) graph
for contract in mythril.contracts:
print(mythril.graph_html(args)) # prints html or save it to file
# prints html or save it to file
print(mythril.graph_html(args))
# (optional) other funcs
mythril.dump_statespaces(args)
mythril.disassemble(contract)
mythril.get_state_variable_from_storage(args)
"""
def __init__(
@ -132,8 +139,8 @@ class Mythril(object):
return mythril_dir
def _init_config(self):
"""
If no config file exists, create it and add default options.
"""If no config file exists, create it and add default options.
Default LevelDB path is specified based on OS
dynamic loading is set to infura by default in the file
Returns: leveldb directory
@ -206,14 +213,22 @@ class Mythril(object):
config.set("defaults", "dynamic_loading", "infura")
def analyze_truffle_project(self, *args, **kwargs):
"""
:param args:
:param kwargs:
:return:
"""
return analyze_truffle_project(
self.sigs, *args, **kwargs
) # just passthru by passing signatures for now
@staticmethod
def _init_solc_binary(version):
# Figure out solc binary and version
# Only proper versions are supported. No nightlies, commits etc (such as available in remix)
"""Figure out solc binary and version.
Only proper versions are supported. No nightlies, commits etc (such as available in remix).
"""
if not version:
return os.environ.get("SOLC") or "solc"
@ -248,15 +263,26 @@ class Mythril(object):
return solc_binary
def set_api_leveldb(self, leveldb):
"""
:param leveldb:
:return:
"""
self.eth_db = EthLevelDB(leveldb)
self.eth = self.eth_db
return self.eth
def set_api_rpc_infura(self):
"""Set the RPC mode to INFURA on mainnet."""
self.eth = EthJsonRpc("mainnet.infura.io", 443, True)
log.info("Using INFURA for RPC queries")
def set_api_rpc(self, rpc=None, rpctls=False):
"""
:param rpc:
:param rpctls:
"""
if rpc == "ganache":
rpcconfig = ("localhost", 8545, False)
else:
@ -279,10 +305,12 @@ class Mythril(object):
raise CriticalError("Invalid RPC settings, check help for details.")
def set_api_rpc_localhost(self):
"""Set the RPC mode to a local instance."""
self.eth = EthJsonRpc("localhost", 8545)
log.info("Using default RPC settings: http://localhost:8545")
def set_api_from_config_path(self):
"""Set the RPC mode based on a given config file."""
config = ConfigParser(allow_no_value=False)
config.optionxform = str
config.read(self.config_path, "utf-8")
@ -298,7 +326,18 @@ class Mythril(object):
self.set_api_rpc(dynamic_loading)
def search_db(self, search):
"""
:param search:
"""
def search_callback(_, address, balance):
"""
:param _:
:param address:
:param balance:
"""
print("Address: " + address + ", balance: " + str(balance))
try:
@ -308,13 +347,23 @@ class Mythril(object):
raise CriticalError("Syntax error in search expression.")
def contract_hash_to_address(self, hash):
"""
:param hash:
"""
if not re.match(r"0x[a-fA-F0-9]{64}", hash):
raise CriticalError("Invalid address hash. Expected format is '0x...'.")
print(self.eth_db.contract_hash_to_address(hash))
def load_from_bytecode(self, code, bin_runtime=False, address=None):
"""
:param code:
:param bin_runtime:
:param address:
:return:
"""
if address is None:
address = util.get_indexed_address(0)
if bin_runtime:
@ -336,6 +385,11 @@ class Mythril(object):
return address, self.contracts[-1] # return address and contract object
def load_from_address(self, address):
"""
:param address:
:return:
"""
if not re.match(r"0x[a-fA-F0-9]{40}", address):
raise CriticalError("Invalid contract address. Expected format is '0x...'.")
@ -366,7 +420,7 @@ class Mythril(object):
def load_from_solidity(self, solidity_files):
"""
UPDATES self.sigs!
:param solidity_files:
:return:
"""
@ -423,7 +477,16 @@ class Mythril(object):
execution_timeout=None,
create_timeout=None,
):
"""
:param strategy:
:param contract:
:param address:
:param max_depth:
:param execution_timeout:
:param create_timeout:
:return:
"""
sym = SymExecWrapper(
contract,
address,
@ -451,6 +514,18 @@ class Mythril(object):
execution_timeout=None,
create_timeout=None,
):
"""
:param strategy:
:param contract:
:param address:
:param max_depth:
:param enable_physics:
:param phrackify:
:param execution_timeout:
:param create_timeout:
:return:
"""
sym = SymExecWrapper(
contract,
address,
@ -478,7 +553,19 @@ class Mythril(object):
create_timeout=None,
transaction_count=None,
):
"""
:param strategy:
:param contracts:
:param address:
:param modules:
:param verbose_report:
:param max_depth:
:param execution_timeout:
:param create_timeout:
:param transaction_count:
:return:
"""
all_issues = []
for contract in contracts or self.contracts:
try:
@ -523,6 +610,12 @@ class Mythril(object):
return report
def get_state_variable_from_storage(self, address, params=None):
"""
:param address:
:param params:
:return:
"""
if params is None:
params = []
(position, length, mappings) = (0, 1, [])
@ -603,8 +696,18 @@ class Mythril(object):
@staticmethod
def disassemble(contract):
"""
:param contract:
:return:
"""
return contract.get_easm()
@staticmethod
def hash_for_function_signature(sig):
"""
:param sig:
:return:
"""
return "0x%s" % utils.sha3(sig)[:4].hex()

@ -1,3 +1,5 @@
"""This module contains representation classes for Solidity files, contracts
and source mappings."""
import mythril.laser.ethereum.util as helper
from mythril.ethereum.evmcontract import EVMContract
from mythril.ethereum.util import get_solc_json
@ -5,6 +7,8 @@ from mythril.exceptions import NoContractFoundError
class SourceMapping:
"""Representation of a source mapping for a Solidity file."""
def __init__(self, solidity_file_idx, offset, length, lineno):
self.solidity_file_idx = solidity_file_idx
self.offset = offset
@ -13,12 +17,16 @@ class SourceMapping:
class SolidityFile:
"""Representation of a file containing Solidity code."""
def __init__(self, filename, data):
self.filename = filename
self.data = data
class SourceCodeInfo:
"""Metadata class containing a code reference for a specific file."""
def __init__(self, filename, lineno, code):
self.filename = filename
self.lineno = lineno
@ -26,6 +34,12 @@ class SourceCodeInfo:
def get_contracts_from_file(input_file, solc_args=None, solc_binary="solc"):
"""
:param input_file:
:param solc_args:
:param solc_binary:
"""
data = get_solc_json(input_file, solc_args=solc_args, solc_binary=solc_binary)
try:
@ -43,6 +57,8 @@ def get_contracts_from_file(input_file, solc_args=None, solc_binary="solc"):
class SolidityContract(EVMContract):
"""Representation of a Solidity contract."""
def __init__(self, input_file, name=None, solc_args=None, solc_binary="solc"):
data = get_solc_json(input_file, solc_args=solc_args, solc_binary=solc_binary)
@ -101,6 +117,12 @@ class SolidityContract(EVMContract):
super().__init__(code, creation_code, name=name)
def get_source_info(self, address, constructor=False):
"""
:param address:
:param constructor:
:return:
"""
disassembly = self.creation_disassembly if constructor else self.disassembly
mappings = self.constructor_mappings if constructor else self.mappings
index = helper.get_instruction_index(disassembly.instruction_list, address)
@ -119,6 +141,11 @@ class SolidityContract(EVMContract):
return SourceCodeInfo(filename, lineno, code)
def _get_solc_mappings(self, srcmap, constructor=False):
"""
:param srcmap:
:param constructor:
"""
mappings = self.constructor_mappings if constructor else self.mappings
for item in srcmap:
mapping = item.split(":")

@ -1,3 +1,5 @@
"""This module contains the dynamic loader logic to get on-chain storage data
and dependencies."""
from mythril.disassembler.disassembly import Disassembly
import logging
import re
@ -6,14 +8,27 @@ log = logging.getLogger(__name__)
class DynLoader:
"""The dynamic loader class."""
def __init__(self, eth, contract_loading=True, storage_loading=True):
"""
:param eth:
:param contract_loading:
:param storage_loading:
"""
self.eth = eth
self.storage_cache = {}
self.contract_loading = contract_loading
self.storage_loading = storage_loading
def read_storage(self, contract_address, index):
"""
:param contract_address:
:param index:
:return:
"""
if not self.storage_loading:
raise Exception(
"Cannot load from the storage when the storage_loading flag is false"
@ -44,7 +59,12 @@ class DynLoader:
return data
def dynld(self, contract_address, dependency_address):
"""
:param contract_address:
:param dependency_address:
:return:
"""
if not self.contract_loading:
raise ValueError("Cannot load contract when contract_loading flag is false")

@ -1,31 +1,39 @@
#!/usr/bin/env python3
# -*- coding: UTF-8 -*-
"""mythril.py: Function Signature Database
"""
import os
import time
"""The Mythril function signature database."""
import functools
import logging
import sqlite3
import multiprocessing
import functools
from typing import List
import os
import sqlite3
import time
from collections import defaultdict
from subprocess import PIPE, Popen
from typing import List
from subprocess import Popen, PIPE
from mythril.exceptions import CompilerError
log = logging.getLogger(__name__)
lock = multiprocessing.Lock()
def synchronized(sync_lock):
""" Synchronization decorator """
"""A decorator synchronizing multi-process access to a resource."""
def wrapper(f):
"""The decorator's core function.
:param f:
:return:
"""
@functools.wraps(f)
def inner_wrapper(*args, **kw):
"""
:param args:
:param kw:
:return:
"""
with sync_lock:
return f(*args, **kw)
@ -35,10 +43,21 @@ def synchronized(sync_lock):
class Singleton(type):
"""A metaclass type implementing the singleton pattern."""
_instances = {}
@synchronized(lock)
def __call__(cls, *args, **kwargs):
"""Delegate the call to an existing resource or a a new one.
This is not thread- or process-safe by default. It must be protected with
a lock.
:param args:
:param kwargs:
:return:
"""
if cls not in cls._instances:
cls._instances[cls] = super(Singleton, cls).__call__(*args, **kwargs)
return cls._instances[cls]
@ -55,21 +74,36 @@ except ImportError:
class SQLiteDB(object):
"""
Simple context manager for sqlite3 databases. Commits everything at exit.
"""Simple context manager for sqlite3 databases.
Commits everything at exit.
"""
def __init__(self, path):
"""
:param path:
"""
self.path = path
self.conn = None
self.cursor = None
def __enter__(self):
"""
:return:
"""
self.conn = sqlite3.connect(self.path)
self.cursor = self.conn.cursor()
return self.cursor
def __exit__(self, exc_class, exc, traceback):
"""
:param exc_class:
:param exc:
:param traceback:
"""
self.conn.commit()
self.conn.close()
@ -78,7 +112,13 @@ class SQLiteDB(object):
class SignatureDB(object, metaclass=Singleton):
""""""
def __init__(self, enable_online_lookup: bool = False, path: str = None) -> None:
"""
:param enable_online_lookup:
:param path:
"""
self.enable_online_lookup = enable_online_lookup
self.online_lookup_miss = set()
self.online_lookup_timeout = 0
@ -104,8 +144,8 @@ class SignatureDB(object, metaclass=Singleton):
)
def __getitem__(self, item: str) -> List[str]:
"""
Provide dict interface db[sighash]
"""Provide dict interface db[sighash]
:param item: 4-byte signature string
:return: list of matching text signature strings
"""
@ -113,8 +153,8 @@ class SignatureDB(object, metaclass=Singleton):
@staticmethod
def _normalize_byte_sig(byte_sig: str) -> str:
"""
Adds a leading 0x to the byte signature if it's not already there.
"""Adds a leading 0x to the byte signature if it's not already there.
:param byte_sig: 4-byte signature string
:return: normalized byte signature string
"""
@ -142,10 +182,9 @@ class SignatureDB(object, metaclass=Singleton):
)
def get(self, byte_sig: str, online_timeout: int = 2) -> List[str]:
"""
Get a function text signature for a byte signature
1) try local cache
2) try online lookup (if enabled; if not flagged as unavailable)
"""Get a function text signature for a byte signature 1) try local
cache 2) try online lookup (if enabled; if not flagged as unavailable)
:param byte_sig: function signature hash as hexstr
:param online_timeout: online lookup timeout
:return: list of matching function text signatures
@ -193,8 +232,10 @@ class SignatureDB(object, metaclass=Singleton):
def import_solidity_file(
self, file_path: str, solc_binary: str = "solc", solc_args: str = None
):
"""
Import Function Signatures from solidity source files
"""Import Function Signatures from solidity source files.
:param solc_binary:
:param solc_args:
:param file_path: solidity source code file path
:return:
"""
@ -239,11 +280,7 @@ class SignatureDB(object, metaclass=Singleton):
@staticmethod
def lookup_online(byte_sig: str, timeout: int, proxies=None) -> List[str]:
"""
Lookup function signatures from 4byte.directory.
//tintinweb: the smart-contract-sanctuary project dumps contracts from etherscan.io and feeds them into
4bytes.directory.
https://github.com/tintinweb/smart-contract-sanctuary
"""Lookup function signatures from 4byte.directory.
:param byte_sig: function signature hash as hexstr
:param timeout: optional timeout for online lookup

@ -0,0 +1 @@
"""This module contains utility functions for the Mythril support package."""

@ -1,24 +1,31 @@
"""This module contains functionality used to easily analyse Truffle
projects."""
import json
import logging
import os
from pathlib import PurePath
import re
import sys
import json
import logging
from pathlib import PurePath
from ethereum.utils import sha3
from mythril.ethereum.evmcontract import EVMContract
from mythril.solidity.soliditycontract import SourceMapping
from mythril.analysis.report import Report
from mythril.analysis.security import fire_lasers
from mythril.analysis.symbolic import SymExecWrapper
from mythril.analysis.report import Report
from mythril.ethereum import util
from mythril.ethereum.evmcontract import EVMContract
from mythril.laser.ethereum.util import get_instruction_index
from mythril.solidity.soliditycontract import SourceMapping
log = logging.getLogger(__name__)
def analyze_truffle_project(sigs, args):
"""
:param sigs:
:param args:
"""
project_root = os.getcwd()
build_dir = os.path.join(project_root, "build", "contracts")
@ -135,6 +142,11 @@ def analyze_truffle_project(sigs, args):
def get_sigs_from_truffle(sigs, contract_data):
"""
:param sigs:
:param contract_data:
"""
abis = contract_data["abi"]
for abi in abis:
if abi["type"] != "function":
@ -146,6 +158,12 @@ def get_sigs_from_truffle(sigs, contract_data):
def get_mappings(source, deployed_source_map):
"""
:param source:
:param deployed_source_map:
:return:
"""
mappings = []
for item in deployed_source_map:
mapping = item.split(":")

@ -1,3 +1,7 @@
# This file is suitable for sourcing inside POSIX shell, e.g. bash as
# well as for importing into Python
"""This file contains the current Mythril version.
This file is suitable for sourcing inside POSIX shell, e.g. bash as well
as for importing into Python.
"""
VERSION = "v0.19.11" # NOQA

@ -1,13 +1,11 @@
# -*- coding: utf-8 -*-
"""
install mythril and deploy source-dist and wheel to pypi.python.org
"""install mythril and deploy source-dist and wheel to pypi.python.org.
deps (requires up2date version):
*) pip install --upgrade pip wheel setuptools twine
publish to pypi w/o having to convert Readme.md to RST:
1) #> python setup.py sdist bdist_wheel
2) #> twine upload dist/* #<specify bdist_wheel version to upload>; #optional --repository <testpypi> or --repository-url <testpypi-url>
"""
from setuptools import setup, find_packages
from setuptools.command.install import install
@ -27,11 +25,12 @@ exec(open(str(version_path), "r").read())
class VerifyVersionCommand(install):
"""Custom command to verify that the git tag matches our version"""
"""Custom command to verify that the git tag matches our version."""
description = "verify that the git tag matches our version"
def run(self):
""""""
tag = os.getenv("CIRCLE_TAG")
if tag != VERSION:
@ -42,8 +41,8 @@ class VerifyVersionCommand(install):
def read_file(fname):
"""
return file contents
"""return file contents.
:param fname: path relative to setup.py
:return: file contents
"""

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

Loading…
Cancel
Save