mirror of https://github.com/ConsenSys/mythril
Nikhil Parasaram
6 years ago
commit
ef2a56c898
@ -1,2 +1,5 @@ |
||||
tests/testdata/* linguist-detectable=false |
||||
static/* linguist-documentation |
||||
static/* linguist-documentation |
||||
|
||||
# Solidity |
||||
*.sol linguist-language=Solidity |
||||
|
||||
@ -1,2 +1,2 @@ |
||||
include mythril/disassembler/signatures.json |
||||
include signatures.db |
||||
include mythril/analysis/templates/* |
||||
|
||||
@ -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: |
||||
@ -1,6 +1,6 @@ |
||||
# We use RsT document formatting in docstring. For example :param to mark parameters. |
||||
# See PEP 287 |
||||
__docformat__ = 'restructuredtext' |
||||
__docformat__ = "restructuredtext" |
||||
|
||||
# Accept mythril.VERSION to get mythril's current version number |
||||
from .version import VERSION # NOQA |
||||
|
||||
@ -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) |
||||
@ -0,0 +1,59 @@ |
||||
"""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 |
||||
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"] |
||||
|
||||
stack = state.mstate.stack |
||||
|
||||
if op in ("CALL", "CALLCODE"): |
||||
gas, to, value, meminstart, meminsz, memoutstart, memoutsz = ( |
||||
get_variable(stack[-1]), |
||||
get_variable(stack[-2]), |
||||
get_variable(stack[-3]), |
||||
get_variable(stack[-4]), |
||||
get_variable(stack[-5]), |
||||
get_variable(stack[-6]), |
||||
get_variable(stack[-7]), |
||||
) |
||||
|
||||
if to.type == VarType.CONCRETE and to.val < 5: |
||||
return None |
||||
|
||||
if meminstart.type == VarType.CONCRETE and meminsz.type == VarType.CONCRETE: |
||||
return Call( |
||||
state.node, |
||||
state, |
||||
None, |
||||
op, |
||||
to, |
||||
gas, |
||||
value, |
||||
state.mstate.memory[meminstart.val : meminsz.val * 4], |
||||
) |
||||
else: |
||||
return Call(state.node, state, None, op, to, gas, value) |
||||
|
||||
else: |
||||
gas, to, meminstart, meminsz, memoutstart, memoutsz = ( |
||||
get_variable(stack[-1]), |
||||
get_variable(stack[-2]), |
||||
get_variable(stack[-3]), |
||||
get_variable(stack[-4]), |
||||
get_variable(stack[-5]), |
||||
get_variable(stack[-6]), |
||||
) |
||||
|
||||
return Call(state.node, state, None, op, to, gas) |
||||
@ -0,0 +1,69 @@ |
||||
"""This module contains the base class for all user-defined detection |
||||
modules.""" |
||||
|
||||
import logging |
||||
from typing import List |
||||
|
||||
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, |
||||
swc_id: str, |
||||
description: str, |
||||
entrypoint: str = "post", |
||||
pre_hooks: List[str] = None, |
||||
post_hooks: List[str] = None, |
||||
): |
||||
self.name = name |
||||
self.swc_id = swc_id |
||||
self.pre_hooks = pre_hooks if pre_hooks else [] |
||||
self.post_hooks = post_hooks if post_hooks else [] |
||||
self.description = description |
||||
if entrypoint not in ("post", "callback"): |
||||
log.error( |
||||
"Invalid entrypoint in module %s, must be one of {post, callback}", |
||||
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) -> str: |
||||
return ( |
||||
"<" |
||||
"DetectionModule " |
||||
"name={0.name} " |
||||
"swc_id={0.swc_id} " |
||||
"pre_hooks={0.pre_hooks} " |
||||
"post_hooks={0.post_hooks} " |
||||
"description={0.description}" |
||||
">" |
||||
).format(self) |
||||
@ -1,129 +1,224 @@ |
||||
"""This module contains the detection code for predictable variable |
||||
dependence.""" |
||||
import logging |
||||
import re |
||||
from z3 import * |
||||
from mythril.analysis.ops import VarType |
||||
|
||||
from mythril.analysis import solver |
||||
from mythril.analysis.call_helpers import get_call_from_state |
||||
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 TIMESTAMP_DEPENDENCE, PREDICTABLE_VARS_DEPENDENCE |
||||
from mythril.analysis.swc_data import TIMESTAMP_DEPENDENCE, WEAK_RANDOMNESS |
||||
from mythril.exceptions import UnsatError |
||||
import logging |
||||
from mythril.laser.ethereum.state.global_state import GlobalState |
||||
|
||||
''' |
||||
MODULE DESCRIPTION: |
||||
log = logging.getLogger(__name__) |
||||
|
||||
Check for CALLs that send >0 Ether as a result of computation based on predictable variables such as |
||||
block.coinbase, block.gaslimit, block.timestamp, block.number |
||||
|
||||
TODO: |
||||
- block.blockhash(block.number-1) |
||||
- block.blockhash(some_block_past_256_blocks_from_now)==0 |
||||
- external source of random numbers (e.g. Oraclize) |
||||
''' |
||||
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, WEAK_RANDOMNESS), |
||||
description=( |
||||
"Check for CALLs that send >0 Ether as a result of computation " |
||||
"based on predictable variables such as block.coinbase, " |
||||
"block.gaslimit, block.timestamp, block.number" |
||||
), |
||||
entrypoint="callback", |
||||
pre_hooks=["CALL", "CALLCODE", "DELEGATECALL", "STATICCALL"], |
||||
) |
||||
|
||||
def execute(statespace): |
||||
def execute(self, state: GlobalState) -> list: |
||||
""" |
||||
|
||||
logging.debug("Executing module: DEPENDENCE_ON_PREDICTABLE_VARS") |
||||
:param state: |
||||
:return: |
||||
""" |
||||
log.debug("Executing module: DEPENDENCE_ON_PREDICTABLE_VARS") |
||||
self._issues.extend(_analyze_states(state)) |
||||
return self.issues |
||||
|
||||
issues = [] |
||||
|
||||
for call in statespace.calls: |
||||
|
||||
if "callvalue" in str(call.value): |
||||
logging.debug("[DEPENDENCE_ON_PREDICTABLE_VARS] Skipping refund function") |
||||
continue |
||||
|
||||
# We're only interested in calls that send Ether |
||||
|
||||
if call.value.type == VarType.CONCRETE and call.value.val == 0: |
||||
continue |
||||
|
||||
address = call.state.get_current_instruction()['address'] |
||||
|
||||
description = "In the function `" + call.node.function_name + "` " |
||||
description += "the following predictable state variables are used to determine Ether recipient:\n" |
||||
|
||||
# First check: look for predictable state variables in node & call recipient constraints |
||||
|
||||
vars = ["coinbase", "gaslimit", "timestamp", "number"] |
||||
|
||||
found = [] |
||||
for var in vars: |
||||
for constraint in call.node.constraints + [call.to]: |
||||
if var in str(constraint): |
||||
found.append(var) |
||||
|
||||
if len(found): |
||||
for item in found: |
||||
description += "- block.{}\n".format(item) |
||||
if solve(call): |
||||
swc_type = TIMESTAMP_DEPENDENCE if item == 'timestamp' else PREDICTABLE_VARS_DEPENDENCE |
||||
issue = Issue(contract=call.node.contract_name, function=call.node.function_name, address=address, |
||||
swc_id=swc_type, title="Dependence on predictable environment variable", |
||||
_type="Warning", description=description) |
||||
issues.append(issue) |
||||
|
||||
# Second check: blockhash |
||||
|
||||
for constraint in call.node.constraints + [call.to]: |
||||
if "blockhash" in str(constraint): |
||||
description = "In the function `" + call.node.function_name + "` " |
||||
if "number" in str(constraint): |
||||
m = re.search(r'blockhash\w+(\s-\s(\d+))*', str(constraint)) |
||||
if m and solve(call): |
||||
|
||||
found = m.group(1) |
||||
|
||||
if found: # block.blockhash(block.number - N) |
||||
description += "predictable expression 'block.blockhash(block.number - " + m.group(2) + \ |
||||
")' is used to determine Ether recipient" |
||||
if int(m.group(2)) > 255: |
||||
description += ", this expression will always be equal to zero." |
||||
elif "storage" in str(constraint): # block.blockhash(block.number - storage_0) |
||||
description += "predictable expression 'block.blockhash(block.number - " + \ |
||||
"some_storage_var)' is used to determine Ether recipient" |
||||
else: # block.blockhash(block.number) |
||||
description += "predictable expression 'block.blockhash(block.number)'" + \ |
||||
" is used to determine Ether recipient" |
||||
description += ", this expression will always be equal to zero." |
||||
|
||||
issue = Issue(contract=call.node.contract_name, function=call.node.function_name, |
||||
address=address, title="Dependence on predictable variable", |
||||
_type="Warning", description=description, swc_id=PREDICTABLE_VARS_DEPENDENCE) |
||||
detector = PredictableDependenceModule() |
||||
|
||||
|
||||
def _analyze_states(state: GlobalState) -> list: |
||||
""" |
||||
|
||||
:param state: |
||||
:return: |
||||
""" |
||||
issues = [] |
||||
call = get_call_from_state(state) |
||||
if call is None: |
||||
return [] |
||||
if "callvalue" in str(call.value): |
||||
log.debug("[DEPENDENCE_ON_PREDICTABLE_VARS] Skipping refund function") |
||||
return [] |
||||
|
||||
# We're only interested in calls that send Ether |
||||
if call.value.type == VarType.CONCRETE and call.value.val == 0: |
||||
return [] |
||||
|
||||
address = call.state.get_current_instruction()["address"] |
||||
|
||||
description = ( |
||||
"The contract sends Ether depending on the values of the following variables:\n" |
||||
) |
||||
|
||||
# First check: look for predictable state variables in node & call recipient constraints |
||||
|
||||
vars = ["coinbase", "gaslimit", "timestamp", "number"] |
||||
found = [] |
||||
|
||||
for var in vars: |
||||
for constraint in call.node.constraints[:] + [call.to]: |
||||
if var in str(constraint): |
||||
found.append(var) |
||||
|
||||
if len(found): |
||||
for item in found: |
||||
description += "- block.{}\n".format(item) |
||||
if solve(call): |
||||
swc_id = TIMESTAMP_DEPENDENCE if item == "timestamp" else WEAK_RANDOMNESS |
||||
|
||||
description += ( |
||||
"Note that the values of variables like coinbase, gaslimit, block number and timestamp " |
||||
"are predictable and/or can be manipulated by a malicious miner. " |
||||
"Don't use them for random number generation or to make critical decisions." |
||||
) |
||||
|
||||
issue = Issue( |
||||
contract=call.node.contract_name, |
||||
function_name=call.node.function_name, |
||||
address=address, |
||||
swc_id=swc_id, |
||||
bytecode=call.state.environment.code.bytecode, |
||||
title="Dependence on predictable environment variable", |
||||
severity="Low", |
||||
description_head="Sending of Ether depends on a predictable variable.", |
||||
description_tail=description, |
||||
gas_used=( |
||||
call.state.mstate.min_gas_used, |
||||
call.state.mstate.max_gas_used, |
||||
), |
||||
) |
||||
issues.append(issue) |
||||
|
||||
# Second check: blockhash |
||||
|
||||
for constraint in call.node.constraints[:] + [call.to]: |
||||
if "blockhash" in str(constraint): |
||||
if "number" in str(constraint): |
||||
m = re.search(r"blockhash\w+(\s-\s(\d+))*", str(constraint)) |
||||
if m and solve(call): |
||||
|
||||
found = m.group(1) |
||||
|
||||
if found: # block.blockhash(block.number - N) |
||||
description = ( |
||||
"The predictable expression 'block.blockhash(block.number - " |
||||
+ m.group(2) |
||||
+ ")' is used to determine Ether recipient" |
||||
) |
||||
if int(m.group(2)) > 255: |
||||
description += ( |
||||
", this expression will always be equal to zero." |
||||
) |
||||
elif "storage" in str( |
||||
constraint |
||||
): # block.blockhash(block.number - storage_0) |
||||
description = ( |
||||
"The predictable expression 'block.blockhash(block.number - " |
||||
+ "some_storage_var)' is used to determine Ether recipient" |
||||
) |
||||
else: # block.blockhash(block.number) |
||||
description = ( |
||||
"The predictable expression 'block.blockhash(block.number)'" |
||||
+ " is used to determine Ether recipient" |
||||
) |
||||
description += ", this expression will always be equal to zero." |
||||
|
||||
issue = Issue( |
||||
contract=call.node.contract_name, |
||||
function_name=call.node.function_name, |
||||
address=address, |
||||
bytecode=call.state.environment.code.bytecode, |
||||
title="Dependence on Predictable Variable", |
||||
severity="Low", |
||||
description_head="Sending of Ether depends on the blockhash.", |
||||
description_tail=description, |
||||
swc_id=WEAK_RANDOMNESS, |
||||
gas_used=( |
||||
call.state.mstate.min_gas_used, |
||||
call.state.mstate.max_gas_used, |
||||
), |
||||
) |
||||
issues.append(issue) |
||||
break |
||||
else: |
||||
|
||||
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. |
||||
""" |
||||
|
||||
index = r.group(1) |
||||
if index and solve(call): |
||||
description = ( |
||||
"A block hash is calculated using the block.blockhash(uint blockNumber) method. " |
||||
"The block number is obtained from storage index {}".format( |
||||
index |
||||
) |
||||
) |
||||
issue = Issue( |
||||
contract=call.node.contract_name, |
||||
function_name=call.node.function_name, |
||||
address=address, |
||||
bytecode=call.state.environment.code.bytecode, |
||||
title="Dependence on Predictable Variable", |
||||
severity="Low", |
||||
description_head="Sending of Ether depends on the blockhash.", |
||||
description_tail=description, |
||||
swc_id=WEAK_RANDOMNESS, |
||||
gas_used=( |
||||
call.state.mstate.min_gas_used, |
||||
call.state.mstate.max_gas_used, |
||||
), |
||||
) |
||||
issues.append(issue) |
||||
break |
||||
else: |
||||
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. |
||||
''' |
||||
|
||||
index = r.group(1) |
||||
if index and solve(call): |
||||
description += 'block.blockhash() is calculated using a value from storage ' \ |
||||
'at index {}'.format(index) |
||||
issue = Issue(contract=call.node.contract_name, function=call.node.function_name, |
||||
address=address, title="Dependence on predictable variable", |
||||
_type="Informational", description=description, swc_id=PREDICTABLE_VARS_DEPENDENCE) |
||||
issues.append(issue) |
||||
break |
||||
return issues |
||||
|
||||
|
||||
def solve(call): |
||||
def solve(call: Call) -> bool: |
||||
""" |
||||
|
||||
:param call: |
||||
:return: |
||||
""" |
||||
try: |
||||
model = solver.get_model(call.node.constraints) |
||||
logging.debug("[DEPENDENCE_ON_PREDICTABLE_VARS] MODEL: " + str(model)) |
||||
log.debug("[DEPENDENCE_ON_PREDICTABLE_VARS] MODEL: " + str(model)) |
||||
pretty_model = solver.pretty_print_model(model) |
||||
|
||||
for d in model.decls(): |
||||
logging.debug("[DEPENDENCE_ON_PREDICTABLE_VARS] main model: %s = 0x%x" % (d.name(), model[d].as_long())) |
||||
log.debug("[DEPENDENCE_ON_PREDICTABLE_VARS] main model: \n%s" % pretty_model) |
||||
return True |
||||
|
||||
except UnsatError: |
||||
logging.debug("[DEPENDENCE_ON_PREDICTABLE_VARS] no model found") |
||||
log.debug("[DEPENDENCE_ON_PREDICTABLE_VARS] no model found") |
||||
return False |
||||
|
||||
@ -1,36 +1,87 @@ |
||||
"""This module contains the detection code for deprecated op codes.""" |
||||
from mythril.analysis.report import Issue |
||||
from mythril.analysis.swc_data import TX_ORIGIN_USAGE |
||||
from mythril.analysis.swc_data import DEPRICATED_FUNCTIONS_USAGE |
||||
from mythril.analysis.modules.base import DetectionModule |
||||
from mythril.laser.ethereum.state.global_state import GlobalState |
||||
import logging |
||||
|
||||
log = logging.getLogger(__name__) |
||||
|
||||
''' |
||||
MODULE DESCRIPTION: |
||||
DESCRIPTION = """ |
||||
Check for usage of deprecated opcodes |
||||
""" |
||||
|
||||
Check for constraints on tx.origin (i.e., access to some functionality is restricted to a specific origin). |
||||
''' |
||||
|
||||
def _analyze_state(state): |
||||
""" |
||||
|
||||
def execute(statespace): |
||||
:param state: |
||||
:return: |
||||
""" |
||||
node = state.node |
||||
instruction = state.get_current_instruction() |
||||
|
||||
logging.debug("Executing module: DEPRECATED OPCODES") |
||||
if instruction["opcode"] == "ORIGIN": |
||||
log.debug("ORIGIN in function " + node.function_name) |
||||
title = "Use of tx.origin" |
||||
description_head = "Use of tx.origin is deprecated." |
||||
description_tail = ( |
||||
"The smart contract retrieves the transaction origin (tx.origin) using msg.origin. " |
||||
"Use of msg.origin is deprecated and the instruction may be removed in the future. " |
||||
"Use msg.sender instead.\nSee also: " |
||||
"https://solidity.readthedocs.io/en/develop/security-considerations.html#tx-origin".format( |
||||
node.function_name |
||||
) |
||||
) |
||||
swc_id = DEPRICATED_FUNCTIONS_USAGE |
||||
|
||||
issues = [] |
||||
elif instruction["opcode"] == "CALLCODE": |
||||
log.debug("CALLCODE in function " + node.function_name) |
||||
title = "Use of callcode" |
||||
description_head = "Use of callcode is deprecated." |
||||
description_tail = ( |
||||
"The callcode method executes code of another contract in the context of the caller account. " |
||||
"Due to a bug in the implementation it does not persist sender and value over the call. It was " |
||||
"therefore deprecated and may be removed in the future. Use the delegatecall method instead." |
||||
) |
||||
swc_id = DEPRICATED_FUNCTIONS_USAGE |
||||
|
||||
for k in statespace.nodes: |
||||
node = statespace.nodes[k] |
||||
issue = Issue( |
||||
contract=node.contract_name, |
||||
function_name=node.function_name, |
||||
address=instruction["address"], |
||||
title=title, |
||||
bytecode=state.environment.code.bytecode, |
||||
swc_id=swc_id, |
||||
severity="Medium", |
||||
description_head=description_head, |
||||
description_tail=description_tail, |
||||
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), |
||||
) |
||||
return [issue] |
||||
|
||||
for state in node.states: |
||||
|
||||
instruction = state.get_current_instruction() |
||||
class DeprecatedOperationsModule(DetectionModule): |
||||
"""This module checks for the usage of deprecated op codes.""" |
||||
|
||||
if instruction['opcode'] == "ORIGIN": |
||||
description = "The function `{}` retrieves the transaction origin (tx.origin) using the ORIGIN opcode. " \ |
||||
"Use msg.sender instead.\nSee also: " \ |
||||
"https://solidity.readthedocs.io/en/develop/security-considerations.html#tx-origin".format(node.function_name) |
||||
def __init__(self): |
||||
"""""" |
||||
super().__init__( |
||||
name="Deprecated Operations", |
||||
swc_id=DEPRICATED_FUNCTIONS_USAGE, |
||||
description=DESCRIPTION, |
||||
entrypoint="callback", |
||||
pre_hooks=["ORIGIN", "CALLCODE"], |
||||
) |
||||
|
||||
issue = Issue(contract=node.contract_name, function=node.function_name, address=instruction['address'], |
||||
title="Use of tx.origin", _type="Warning", swc_id=TX_ORIGIN_USAGE, |
||||
description=description) |
||||
issues.append(issue) |
||||
def execute(self, state: GlobalState): |
||||
""" |
||||
|
||||
return issues |
||||
:param state: |
||||
:return: |
||||
""" |
||||
self._issues.extend(_analyze_state(state)) |
||||
return self.issues |
||||
|
||||
|
||||
detector = DeprecatedOperationsModule() |
||||
|
||||
@ -1,127 +0,0 @@ |
||||
from z3 import * |
||||
from mythril.analysis.ops import * |
||||
from mythril.analysis import solver |
||||
from mythril.analysis.report import Issue |
||||
from mythril.analysis.swc_data import UNPROTECTED_ETHER_WITHDRAWAL |
||||
from mythril.exceptions import UnsatError |
||||
import re |
||||
import logging |
||||
|
||||
|
||||
''' |
||||
MODULE DESCRIPTION: |
||||
|
||||
Check for CALLs that send >0 Ether to either the transaction sender, or to an address provided as a function argument. |
||||
If msg.sender is checked against a value in storage, check whether that storage index is tainted (i.e. there's an unconstrained write |
||||
to that index). |
||||
''' |
||||
|
||||
|
||||
def execute(statespace): |
||||
|
||||
logging.debug("Executing module: ETHER_SEND") |
||||
|
||||
issues = [] |
||||
|
||||
for call in statespace.calls: |
||||
|
||||
state = call.state |
||||
address = state.get_current_instruction()['address'] |
||||
|
||||
if "callvalue" in str(call.value): |
||||
logging.debug("[ETHER_SEND] Skipping refund function") |
||||
continue |
||||
|
||||
# We're only interested in calls that send Ether |
||||
|
||||
if call.value.type == VarType.CONCRETE and call.value.val == 0: |
||||
continue |
||||
|
||||
interesting = False |
||||
|
||||
description = "In the function `" + call.node.function_name + "` " |
||||
|
||||
if re.search(r'caller', str(call.to)): |
||||
description += "a non-zero amount of Ether is sent to msg.sender.\n" |
||||
interesting = True |
||||
|
||||
elif re.search(r'calldata', str(call.to)): |
||||
description += "a non-zero amount of Ether is sent to an address taken from function arguments.\n" |
||||
interesting = True |
||||
|
||||
else: |
||||
m = re.search(r'storage_([a-z0-9_&^]+)', str(call.to)) |
||||
|
||||
if m: |
||||
idx = m.group(1) |
||||
|
||||
description += "a non-zero amount of Ether is sent to an address taken from storage slot " + str(idx) + ".\n" |
||||
|
||||
func = statespace.find_storage_write(state.environment.active_account.address, idx) |
||||
|
||||
if func: |
||||
description += "There is a check on storage index " + str(idx) + ". This storage slot can be written to by calling the function `" + func + "`.\n" |
||||
interesting = True |
||||
else: |
||||
logging.debug("[ETHER_SEND] No storage writes to index " + str(idx)) |
||||
|
||||
if interesting: |
||||
|
||||
node = call.node |
||||
|
||||
can_solve = True |
||||
constrained = False |
||||
|
||||
index = 0 |
||||
|
||||
while can_solve and index < len(node.constraints): |
||||
|
||||
constraint = node.constraints[index] |
||||
index += 1 |
||||
logging.debug("[ETHER_SEND] Constraint: " + str(constraint)) |
||||
|
||||
m = re.search(r'storage_([a-z0-9_&^]+)', str(constraint)) |
||||
|
||||
if m: |
||||
|
||||
constrained = True |
||||
idx = m.group(1) |
||||
|
||||
func = statespace.find_storage_write(state.environment.active_account.address, idx) |
||||
|
||||
if func: |
||||
description += "\nThere is a check on storage index " + str(idx) + ". This storage slot can be written to by calling the function `" + func + "`." |
||||
else: |
||||
logging.debug("[ETHER_SEND] No storage writes to index " + str(idx)) |
||||
can_solve = False |
||||
break |
||||
|
||||
# CALLER may also be constrained to hardcoded address. I.e. 'caller' and some integer |
||||
|
||||
elif re.search(r"caller", str(constraint)) and re.search(r'[0-9]{20}', str(constraint)): |
||||
constrained = True |
||||
can_solve = False |
||||
break |
||||
|
||||
if not constrained: |
||||
description += "It seems that this function can be called without restrictions." |
||||
|
||||
if can_solve: |
||||
|
||||
try: |
||||
model = solver.get_model(node.constraints) |
||||
|
||||
for d in model.decls(): |
||||
logging.debug("[ETHER_SEND] main model: %s = 0x%x" % (d.name(), model[d].as_long())) |
||||
|
||||
debug = "SOLVER OUTPUT:\n" + solver.pretty_print_model(model) |
||||
|
||||
issue = Issue(contract=call.node.contract_name, function=call.node.function_name, address=address, |
||||
title="Ether send", _type="Warning", swc_id=UNPROTECTED_ETHER_WITHDRAWAL, |
||||
description=description, debug=debug) |
||||
issues.append(issue) |
||||
|
||||
except UnsatError: |
||||
logging.debug("[ETHER_SEND] no model found") |
||||
|
||||
return issues |
||||
@ -0,0 +1,127 @@ |
||||
"""This module contains the detection code for unauthorized ether |
||||
withdrawal.""" |
||||
import logging |
||||
import json |
||||
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.exceptions import UnsatError |
||||
from mythril.laser.ethereum.state.global_state import GlobalState |
||||
from mythril.laser.smt import UGT, BVAddNoOverflow, Sum, symbol_factory |
||||
|
||||
log = logging.getLogger(__name__) |
||||
|
||||
DESCRIPTION = """ |
||||
|
||||
Search for cases where Ether can be withdrawn to a user-specified address. |
||||
|
||||
An issue is reported if: |
||||
|
||||
- The transaction sender does not match contract creator; |
||||
- The sender address can be chosen arbitrarily; |
||||
- The receiver address is identical to the sender address; |
||||
- The sender can withdraw *more* than the total amount they sent over all transactions. |
||||
|
||||
""" |
||||
|
||||
|
||||
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, |
||||
description=DESCRIPTION, |
||||
entrypoint="callback", |
||||
pre_hooks=["CALL"], |
||||
) |
||||
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): |
||||
""" |
||||
|
||||
:param state: |
||||
:return: |
||||
""" |
||||
self._issues.extend(self._analyze_state(state)) |
||||
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 = json.dumps(transaction_sequence, indent=4) |
||||
|
||||
issue = Issue( |
||||
contract=node.contract_name, |
||||
function_name=node.function_name, |
||||
address=instruction["address"], |
||||
swc_id=UNPROTECTED_ETHER_WITHDRAWAL, |
||||
title="Unprotected Ether Withdrawal", |
||||
severity="High", |
||||
bytecode=state.environment.code.bytecode, |
||||
description_head="Anyone can withdraw ETH from the contract account.", |
||||
description_tail="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,51 +1,84 @@ |
||||
"""This module contains the detection code for reachable exceptions.""" |
||||
import logging |
||||
import json |
||||
|
||||
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 |
||||
import logging |
||||
from mythril.laser.ethereum.state.global_state import GlobalState |
||||
|
||||
log = logging.getLogger(__name__) |
||||
|
||||
|
||||
''' |
||||
MODULE DESCRIPTION: |
||||
def _analyze_state(state) -> list: |
||||
""" |
||||
|
||||
Checks whether any exception states are reachable. |
||||
:param state: |
||||
:return: |
||||
""" |
||||
log.info("Exceptions module: found ASSERT_FAIL instruction") |
||||
node = state.node |
||||
|
||||
''' |
||||
log.debug("ASSERT_FAIL in function " + node.function_name) |
||||
|
||||
try: |
||||
address = state.get_current_instruction()["address"] |
||||
|
||||
def execute(statespace): |
||||
description_tail = ( |
||||
"It is possible to trigger an exception (opcode 0xfe). " |
||||
"Exceptions can be caused by type errors, division by zero, " |
||||
"out-of-bounds array access, or assert violations. " |
||||
"Note that explicit `assert()` should only be used to check invariants. " |
||||
"Use `require()` for regular input checking." |
||||
) |
||||
|
||||
logging.debug("Executing module: EXCEPTIONS") |
||||
transaction_sequence = solver.get_transaction_sequence(state, node.constraints) |
||||
debug = json.dumps(transaction_sequence, indent=4) |
||||
|
||||
issues = [] |
||||
issue = Issue( |
||||
contract=node.contract_name, |
||||
function_name=node.function_name, |
||||
address=address, |
||||
swc_id=ASSERT_VIOLATION, |
||||
title="Exception State", |
||||
severity="Low", |
||||
description_head="A reachable exception has been detected.", |
||||
description_tail=description_tail, |
||||
bytecode=state.environment.code.bytecode, |
||||
debug=debug, |
||||
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), |
||||
) |
||||
return [issue] |
||||
|
||||
for k in statespace.nodes: |
||||
node = statespace.nodes[k] |
||||
except UnsatError: |
||||
log.debug("no model found") |
||||
|
||||
for state in node.states: |
||||
return [] |
||||
|
||||
instruction = state.get_current_instruction() |
||||
if instruction['opcode'] == "ASSERT_FAIL": |
||||
try: |
||||
model = solver.get_model(node.constraints) |
||||
address = state.get_current_instruction()['address'] |
||||
|
||||
description = "A reachable exception (opcode 0xfe) has been detected. " \ |
||||
"This can be caused by type errors, division by zero, " \ |
||||
"out-of-bounds array access, or assert violations. " |
||||
description += "This is acceptable in most situations. " \ |
||||
"Note however that `assert()` should only be used to check invariants. " \ |
||||
"Use `require()` for regular input checking. " |
||||
class ReachableExceptionsModule(DetectionModule): |
||||
"""""" |
||||
|
||||
debug = "The exception is triggered under the following conditions:\n\n" |
||||
def __init__(self): |
||||
"""""" |
||||
super().__init__( |
||||
name="Reachable Exceptions", |
||||
swc_id=ASSERT_VIOLATION, |
||||
description="Checks whether any exception states are reachable.", |
||||
entrypoint="callback", |
||||
pre_hooks=["ASSERT_FAIL"], |
||||
) |
||||
|
||||
debug += solver.pretty_print_model(model) |
||||
def execute(self, state: GlobalState) -> list: |
||||
""" |
||||
|
||||
issues.append(Issue(contract=node.contract_name, function=node.function_name, address=address, |
||||
swc_id=ASSERT_VIOLATION, title="Exception state", _type="Informational", |
||||
description=description, debug=debug)) |
||||
:param state: |
||||
:return: |
||||
""" |
||||
self._issues.extend(_analyze_state(state)) |
||||
return self.issues |
||||
|
||||
except UnsatError: |
||||
logging.debug("[EXCEPTIONS] no model found") |
||||
|
||||
return issues |
||||
detector = ReachableExceptionsModule() |
||||
|
||||
@ -1,134 +1,130 @@ |
||||
from z3 import * |
||||
from mythril.analysis.ops import * |
||||
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 |
||||
import re |
||||
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 |
||||
import logging |
||||
|
||||
|
||||
''' |
||||
MODULE DESCRIPTION: |
||||
|
||||
Check for call.value()() to external addresses |
||||
''' |
||||
|
||||
MAX_SEARCH_DEPTH = 64 |
||||
|
||||
|
||||
def search_children(statespace, node, start_index=0, depth=0, results=None): |
||||
if results is None: |
||||
results = [] |
||||
logging.debug("SEARCHING NODE %d", node.uid) |
||||
|
||||
if depth < MAX_SEARCH_DEPTH: |
||||
|
||||
n_states = len(node.states) |
||||
|
||||
if n_states > start_index: |
||||
|
||||
for j in range(start_index, n_states): |
||||
if node.states[j].get_current_instruction()['opcode'] == 'SSTORE': |
||||
results.append(node.states[j].get_current_instruction()['address']) |
||||
|
||||
children = [] |
||||
|
||||
for edge in statespace.edges: |
||||
if edge.node_from == node.uid: |
||||
children.append(statespace.nodes[edge.node_to]) |
||||
|
||||
if len(children): |
||||
for node in children: |
||||
return search_children(statespace, node, depth=depth + 1, results=results) |
||||
|
||||
return results |
||||
|
||||
|
||||
calls_visited = [] |
||||
|
||||
|
||||
def execute(statespace): |
||||
|
||||
issues = [] |
||||
|
||||
for call in statespace.calls: |
||||
|
||||
state = call.state |
||||
address = state.get_current_instruction()['address'] |
||||
|
||||
if call.type == "CALL": |
||||
|
||||
logging.info("[EXTERNAL_CALLS] Call to: %s, value = %s, gas = %s" % (str(call.to), str(call.value), str(call.gas))) |
||||
|
||||
if call.to.type == VarType.SYMBOLIC and (call.gas.type == VarType.CONCRETE and call.gas.val > 2300) or (call.gas.type == VarType.SYMBOLIC and "2300" not in str(call.gas)): |
||||
|
||||
description = "This contract executes a message call to " |
||||
|
||||
target = str(call.to) |
||||
user_supplied = False |
||||
|
||||
if "calldata" in target or "caller" in target: |
||||
|
||||
if "calldata" in target: |
||||
description += "an address provided as a function argument. " |
||||
else: |
||||
description += "the address of the transaction sender. " |
||||
|
||||
user_supplied = True |
||||
else: |
||||
m = re.search(r'storage_([a-z0-9_&^]+)', str(call.to)) |
||||
|
||||
if m: |
||||
idx = m.group(1) |
||||
|
||||
func = statespace.find_storage_write(state.environment.active_account.address, idx) |
||||
|
||||
if func: |
||||
|
||||
description += \ |
||||
"an address found at storage slot " + str(idx) + ". " + \ |
||||
"This storage slot can be written to by calling the function `" + func + "`. " |
||||
user_supplied = True |
||||
|
||||
if user_supplied: |
||||
|
||||
description += "Generally, it is not recommended to call user-supplied addresses using Solidity's call() construct. " \ |
||||
"Note that attackers might leverage reentrancy attacks to exploit race conditions or manipulate this contract's state." |
||||
|
||||
issue = Issue(contract=call.node.contract_name, function=call.node.function_name, |
||||
address=address, title="Message call to external contract", _type="Warning", |
||||
description=description, swc_id=REENTRANCY) |
||||
|
||||
else: |
||||
|
||||
description += "to another contract. Make sure that the called contract is trusted and does not execute user-supplied code." |
||||
|
||||
issue = Issue(contract=call.node.contract_name, function=call.node.function_name, address=address, |
||||
title="Message call to external contract", _type="Informational", |
||||
description=description, swc_id=REENTRANCY) |
||||
|
||||
issues.append(issue) |
||||
|
||||
if address not in calls_visited: |
||||
calls_visited.append(address) |
||||
|
||||
logging.debug("[EXTERNAL_CALLS] Checking for state changes starting from " + call.node.function_name) |
||||
|
||||
# Check for SSTORE in remaining instructions in current node & nodes down the CFG |
||||
|
||||
state_change_addresses = search_children(statespace, call.node, call.state_index + 1, depth=0, results=[]) |
||||
|
||||
logging.debug("[EXTERNAL_CALLS] Detected state changes at addresses: " + str(state_change_addresses)) |
||||
|
||||
if len(state_change_addresses): |
||||
for address in state_change_addresses: |
||||
description = "The contract account state is changed after an external call. " \ |
||||
"Consider that the called contract could re-enter the function before this " \ |
||||
"state change takes place. This can lead to business logic vulnerabilities." |
||||
|
||||
issue = Issue(contract=call.node.contract_name, function=call.node.function_name, |
||||
address=address, title="State change after external call", _type="Warning", |
||||
description=description, swc_id=REENTRANCY) |
||||
issues.append(issue) |
||||
|
||||
return issues |
||||
import json |
||||
|
||||
log = logging.getLogger(__name__) |
||||
|
||||
DESCRIPTION = """ |
||||
|
||||
Search for low level calls (e.g. call.value()) that forward all gas to the callee. |
||||
Report a warning if the callee address can be set by the sender, otherwise create |
||||
an informational issue. |
||||
|
||||
""" |
||||
|
||||
|
||||
def _analyze_state(state): |
||||
""" |
||||
|
||||
:param state: |
||||
:return: |
||||
""" |
||||
node = state.node |
||||
gas = state.mstate.stack[-1] |
||||
to = state.mstate.stack[-2] |
||||
|
||||
address = state.get_current_instruction()["address"] |
||||
|
||||
try: |
||||
constraints = node.constraints |
||||
transaction_sequence = solver.get_transaction_sequence( |
||||
state, constraints + [UGT(gas, symbol_factory.BitVecVal(2300, 256))] |
||||
) |
||||
|
||||
# Check whether we can also set the callee address |
||||
|
||||
try: |
||||
constraints += [to == 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF] |
||||
transaction_sequence = solver.get_transaction_sequence(state, constraints) |
||||
|
||||
debug = json.dumps(transaction_sequence, indent=4) |
||||
description_head = "A call to a user-supplied address is executed." |
||||
description_tail = ( |
||||
"The callee address of an external message call can be set by " |
||||
"the caller. Note that the callee can contain arbitrary code and may re-enter any function " |
||||
"in this contract. Review the business logic carefully to prevent averse effects on the" |
||||
"contract state." |
||||
) |
||||
|
||||
issue = Issue( |
||||
contract=node.contract_name, |
||||
function_name=node.function_name, |
||||
address=address, |
||||
swc_id=REENTRANCY, |
||||
title="External Call To User-Supplied Address", |
||||
bytecode=state.environment.code.bytecode, |
||||
severity="Medium", |
||||
description_head=description_head, |
||||
description_tail=description_tail, |
||||
debug=debug, |
||||
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), |
||||
) |
||||
|
||||
except UnsatError: |
||||
|
||||
log.debug( |
||||
"[EXTERNAL_CALLS] Callee address cannot be modified. Reporting informational issue." |
||||
) |
||||
|
||||
debug = json.dumps(transaction_sequence, indent=4) |
||||
description_head = "The contract executes an external message call." |
||||
description_tail = ( |
||||
"An external function call to a fixed contract address is executed. Make sure " |
||||
"that the callee contract has been reviewed carefully." |
||||
) |
||||
|
||||
issue = Issue( |
||||
contract=node.contract_name, |
||||
function_name=state.node.function_name, |
||||
address=address, |
||||
swc_id=REENTRANCY, |
||||
title="External Call To Fixed Address", |
||||
bytecode=state.environment.code.bytecode, |
||||
severity="Low", |
||||
description_head=description_head, |
||||
description_tail=description_tail, |
||||
debug=debug, |
||||
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), |
||||
) |
||||
|
||||
except UnsatError: |
||||
log.debug("[EXTERNAL_CALLS] No model found.") |
||||
return [] |
||||
|
||||
return [issue] |
||||
|
||||
|
||||
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, |
||||
entrypoint="callback", |
||||
pre_hooks=["CALL"], |
||||
) |
||||
|
||||
def execute(self, state: GlobalState): |
||||
""" |
||||
|
||||
:param state: |
||||
:return: |
||||
""" |
||||
self._issues.extend(_analyze_state(state)) |
||||
return self.issues |
||||
|
||||
|
||||
detector = ExternalCalls() |
||||
|
||||
@ -1,291 +1,290 @@ |
||||
from z3 import * |
||||
"""This module contains the detection code for integer overflows and |
||||
underflows.""" |
||||
|
||||
import json |
||||
|
||||
from mythril.analysis import solver |
||||
from mythril.analysis.ops import * |
||||
from mythril.analysis.report import Issue |
||||
from mythril.analysis.swc_data import INTEGER_OVERFLOW_AND_UNDERFLOW |
||||
from mythril.exceptions import UnsatError |
||||
from mythril.laser.ethereum.taint_analysis import TaintRunner |
||||
import re |
||||
import copy |
||||
from mythril.laser.ethereum.state.global_state import GlobalState |
||||
from mythril.analysis.modules.base import DetectionModule |
||||
|
||||
from mythril.laser.smt import ( |
||||
BVAddNoOverflow, |
||||
BVSubNoUnderflow, |
||||
BVMulNoOverflow, |
||||
BitVec, |
||||
symbol_factory, |
||||
Not, |
||||
Expression, |
||||
) |
||||
|
||||
import logging |
||||
|
||||
''' |
||||
MODULE DESCRIPTION: |
||||
|
||||
Check for integer underflows. |
||||
For every SUB instruction, check if there's a possible state where op1 > op0. |
||||
For every ADD, MUL instruction, check if there's a possible state where op1 + op0 > 2^32 - 1 |
||||
''' |
||||
|
||||
|
||||
def execute(statespace): |
||||
""" |
||||
Executes analysis module for integer underflow and integer overflow |
||||
:param statespace: Statespace to analyse |
||||
:return: Found issues |
||||
""" |
||||
logging.debug("Executing module: INTEGER") |
||||
|
||||
issues = [] |
||||
|
||||
for k in statespace.nodes: |
||||
node = statespace.nodes[k] |
||||
|
||||
for state in node.states: |
||||
issues += _check_integer_underflow(statespace, state, node) |
||||
issues += _check_integer_overflow(statespace, state, node) |
||||
|
||||
return issues |
||||
|
||||
|
||||
def _check_integer_overflow(statespace, state, node): |
||||
""" |
||||
Checks for integer overflow |
||||
:param statespace: statespace that is being examined |
||||
:param state: state from node to examine |
||||
:param node: node to examine |
||||
:return: found issue |
||||
""" |
||||
issues = [] |
||||
|
||||
# Check the instruction |
||||
instruction = state.get_current_instruction() |
||||
if instruction['opcode'] not in ("ADD", "MUL"): |
||||
return issues |
||||
|
||||
# Formulate overflow constraints |
||||
stack = state.mstate.stack |
||||
op0, op1 = stack[-1], stack[-2] |
||||
|
||||
# An integer overflow is possible if op0 + op1 or op0 * op1 > MAX_UINT |
||||
# Do a type check |
||||
allowed_types = [int, BitVecRef, BitVecNumRef] |
||||
if not (type(op0) in allowed_types and type(op1) in allowed_types): |
||||
return issues |
||||
|
||||
# Change ints to BitVec |
||||
if type(op0) is int: |
||||
op0 = BitVecVal(op0, 256) |
||||
if type(op1) is int: |
||||
op1 = BitVecVal(op1, 256) |
||||
|
||||
# Formulate expression |
||||
if instruction['opcode'] == "ADD": |
||||
expr = op0 + op1 |
||||
else: |
||||
expr = op1 * op0 |
||||
|
||||
# Check satisfiable |
||||
constraint = Or(And(ULT(expr, op0), op1 != 0), And(ULT(expr, op1), op0 != 0)) |
||||
model = _try_constraints(node.constraints, [constraint]) |
||||
|
||||
if model is None: |
||||
logging.debug("[INTEGER_OVERFLOW] no model found") |
||||
return issues |
||||
|
||||
if not _verify_integer_overflow(statespace, node, expr, state, model, constraint, op0, op1): |
||||
return issues |
||||
|
||||
# Build issue |
||||
issue = Issue(contract=node.contract_name, function=node.function_name, address=instruction['address'], |
||||
swc_id=INTEGER_OVERFLOW_AND_UNDERFLOW, title="Integer Overflow", _type="Warning") |
||||
|
||||
issue.description = "A possible integer overflow exists in the function `{}`.\n" \ |
||||
"The addition or multiplication may result in a value higher than the maximum representable integer.".format( |
||||
node.function_name) |
||||
issue.debug = solver.pretty_print_model(model) |
||||
issues.append(issue) |
||||
|
||||
return issues |
||||
|
||||
|
||||
def _verify_integer_overflow(statespace, node, expr, state, model, constraint, op0, op1): |
||||
""" Verifies existence of integer overflow """ |
||||
# If we get to this point then there has been an integer overflow |
||||
# Find out if the overflowed value is actually used |
||||
interesting_usages = _search_children(statespace, node, expr, constraint=[constraint], index=node.states.index(state)) |
||||
|
||||
# Stop if it isn't |
||||
if len(interesting_usages) == 0: |
||||
return False |
||||
|
||||
return _try_constraints(node.constraints, [Not(constraint)]) is not None |
||||
|
||||
def _try_constraints(constraints, new_constraints): |
||||
""" |
||||
Tries new constraints |
||||
:return Model if satisfiable otherwise None |
||||
""" |
||||
_constraints = copy.deepcopy(constraints) |
||||
for constraint in new_constraints: |
||||
_constraints.append(copy.deepcopy(constraint)) |
||||
try: |
||||
model = solver.get_model(_constraints) |
||||
return model |
||||
except UnsatError: |
||||
return None |
||||
|
||||
|
||||
def _check_integer_underflow(statespace, state, node): |
||||
""" |
||||
Checks for integer underflow |
||||
:param state: state from node to examine |
||||
:param node: node to examine |
||||
:return: found issue |
||||
""" |
||||
issues = [] |
||||
instruction = state.get_current_instruction() |
||||
if instruction['opcode'] == "SUB": |
||||
log = logging.getLogger(__name__) |
||||
|
||||
|
||||
class OverUnderflowAnnotation: |
||||
def __init__(self, overflowing_state: GlobalState, operator: str, constraint): |
||||
self.overflowing_state = overflowing_state |
||||
self.operator = operator |
||||
self.constraint = constraint |
||||
|
||||
|
||||
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, |
||||
description=( |
||||
"For every SUB instruction, check if there's a possible state " |
||||
"where op1 > op0. For every ADD, MUL instruction, check if " |
||||
"there's a possible state where op1 + op0 > 2^32 - 1" |
||||
), |
||||
entrypoint="callback", |
||||
pre_hooks=["ADD", "MUL", "SUB", "SSTORE", "JUMPI"], |
||||
) |
||||
self._overflow_cache = {} |
||||
self._underflow_cache = {} |
||||
|
||||
def reset_module(self): |
||||
""" |
||||
Resets the module |
||||
:return: |
||||
""" |
||||
super().reset_module() |
||||
self._overflow_cache = {} |
||||
self._underflow_cache = {} |
||||
|
||||
def execute(self, state: GlobalState): |
||||
"""Executes analysis module for integer underflow and integer overflow. |
||||
|
||||
:param state: Statespace to analyse |
||||
:return: Found issues |
||||
""" |
||||
address = _get_address_from_state(state) |
||||
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": |
||||
self._handle_mul(state) |
||||
elif state.get_current_instruction()["opcode"] == "SUB": |
||||
self._handle_sub(state) |
||||
elif state.get_current_instruction()["opcode"] == "SSTORE": |
||||
self._handle_sstore(state) |
||||
elif state.get_current_instruction()["opcode"] == "JUMPI": |
||||
self._handle_jumpi(state) |
||||
|
||||
def _handle_add(self, state): |
||||
stack = state.mstate.stack |
||||
op0, op1 = ( |
||||
self._make_bitvec_if_not(stack, -1), |
||||
self._make_bitvec_if_not(stack, -2), |
||||
) |
||||
c = Not(BVAddNoOverflow(op0, op1, False)) |
||||
|
||||
# Check satisfiable |
||||
model = self._try_constraints(state.node.constraints, [c]) |
||||
if model is None: |
||||
return |
||||
|
||||
annotation = OverUnderflowAnnotation(state, "addition", c) |
||||
op0.annotate(annotation) |
||||
|
||||
def _handle_mul(self, state): |
||||
stack = state.mstate.stack |
||||
op0, op1 = ( |
||||
self._make_bitvec_if_not(stack, -1), |
||||
self._make_bitvec_if_not(stack, -2), |
||||
) |
||||
|
||||
op0 = stack[-1] |
||||
op1 = stack[-2] |
||||
c = Not(BVMulNoOverflow(op0, op1, False)) |
||||
|
||||
constraints = copy.deepcopy(node.constraints) |
||||
# Check satisfiable |
||||
model = self._try_constraints(state.node.constraints, [c]) |
||||
if model is None: |
||||
return |
||||
|
||||
# Filter for patterns that indicate benign underflows |
||||
annotation = OverUnderflowAnnotation(state, "multiplication", c) |
||||
op0.annotate(annotation) |
||||
|
||||
# Pattern 1: (96 + calldatasize_MAIN) - (96), where (96 + calldatasize_MAIN) would underflow if calldatasize is very large. |
||||
# Pattern 2: (256*If(1 & storage_0 == 0, 1, 0)) - 1, this would underlow if storage_0 = 0 |
||||
if type(op0) == int and type(op1) == int: |
||||
return [] |
||||
if re.search(r'calldatasize_', str(op0)): |
||||
return [] |
||||
if re.search(r'256\*.*If\(1', str(op0), re.DOTALL) or re.search(r'256\*.*If\(1', str(op1), re.DOTALL): |
||||
return [] |
||||
if re.search(r'32 \+.*calldata', str(op0), re.DOTALL) or re.search(r'32 \+.*calldata', str(op1), re.DOTALL): |
||||
return [] |
||||
def _handle_sub(self, state): |
||||
stack = state.mstate.stack |
||||
op0, op1 = ( |
||||
self._make_bitvec_if_not(stack, -1), |
||||
self._make_bitvec_if_not(stack, -2), |
||||
) |
||||
c = Not(BVSubNoUnderflow(op0, op1, False)) |
||||
|
||||
# Check satisfiable |
||||
model = self._try_constraints(state.node.constraints, [c]) |
||||
if model is None: |
||||
return |
||||
|
||||
annotation = OverUnderflowAnnotation(state, "subtraction", c) |
||||
op0.annotate(annotation) |
||||
|
||||
@staticmethod |
||||
def _make_bitvec_if_not(stack, index): |
||||
value = stack[index] |
||||
if isinstance(value, BitVec): |
||||
return value |
||||
stack[index] = symbol_factory.BitVecVal(value, 256) |
||||
return stack[index] |
||||
|
||||
@staticmethod |
||||
def _get_description_head(annotation, _type): |
||||
return "The binary {} can {}.".format(annotation.operator, _type.lower()) |
||||
|
||||
@staticmethod |
||||
def _get_description_tail(annotation, _type): |
||||
|
||||
return ( |
||||
"The operands of the {} operation are not sufficiently constrained. " |
||||
"The {} could therefore result in an integer {}. Prevent the {} by checking inputs " |
||||
"or ensure sure that the {} is caught by an assertion.".format( |
||||
annotation.operator, |
||||
annotation.operator, |
||||
_type.lower(), |
||||
_type.lower(), |
||||
_type.lower(), |
||||
) |
||||
) |
||||
|
||||
@staticmethod |
||||
def _get_title(_type): |
||||
return "Integer {}".format(_type) |
||||
|
||||
def _handle_sstore(self, state): |
||||
stack = state.mstate.stack |
||||
value = stack[-2] |
||||
|
||||
logging.debug("[INTEGER_UNDERFLOW] Checking SUB {0}, {1} at address {2}".format(str(op0), str(op1), |
||||
str(instruction['address']))) |
||||
allowed_types = [int, BitVecRef, BitVecNumRef] |
||||
if not isinstance(value, Expression): |
||||
return |
||||
for annotation in value.annotations: |
||||
if not isinstance(annotation, OverUnderflowAnnotation): |
||||
continue |
||||
|
||||
if type(op0) in allowed_types and type(op1) in allowed_types: |
||||
constraints.append(UGT(op1, op0)) |
||||
_type = "Underflow" if annotation.operator == "subtraction" else "Overflow" |
||||
ostate = annotation.overflowing_state |
||||
node = ostate.node |
||||
|
||||
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=self._get_title(_type), |
||||
severity="High", |
||||
description_head=self._get_description_head(annotation, _type), |
||||
description_tail=self._get_description_tail(annotation, _type), |
||||
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), |
||||
) |
||||
|
||||
address = _get_address_from_state(ostate) |
||||
|
||||
if annotation.operator == "subtraction" and self._underflow_cache.get( |
||||
address, False |
||||
): |
||||
continue |
||||
if annotation.operator != "subtraction" and self._overflow_cache.get( |
||||
address, False |
||||
): |
||||
continue |
||||
|
||||
try: |
||||
|
||||
model = solver.get_model(constraints) |
||||
transaction_sequence = solver.get_transaction_sequence( |
||||
state, node.constraints + [annotation.constraint] |
||||
) |
||||
|
||||
issue.debug = json.dumps(transaction_sequence, indent=4) |
||||
|
||||
except UnsatError: |
||||
continue |
||||
if annotation.operator == "subtraction": |
||||
self._underflow_cache[address] = True |
||||
else: |
||||
self._overflow_cache[address] = True |
||||
|
||||
self._issues.append(issue) |
||||
|
||||
# If we get to this point then there has been an integer overflow |
||||
# Find out if the overflowed value is actually used |
||||
interesting_usages = _search_children(statespace, node, (op0 - op1), index=node.states.index(state)) |
||||
def _handle_jumpi(self, state): |
||||
stack = state.mstate.stack |
||||
value = stack[-2] |
||||
|
||||
# Stop if it isn't |
||||
if len(interesting_usages) == 0: |
||||
return issues |
||||
for annotation in value.annotations: |
||||
if not isinstance(annotation, OverUnderflowAnnotation): |
||||
continue |
||||
ostate = annotation.overflowing_state |
||||
node = ostate.node |
||||
|
||||
_type = "Underflow" if annotation.operator == "subtraction" else "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=self._get_title(_type), |
||||
severity="High", |
||||
description_head=self._get_description_head(annotation, _type), |
||||
description_tail=self._get_description_tail(annotation, _type), |
||||
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), |
||||
) |
||||
|
||||
address = _get_address_from_state(ostate) |
||||
|
||||
if annotation.operator == "subtraction" and self._underflow_cache.get( |
||||
address, False |
||||
): |
||||
continue |
||||
|
||||
if annotation.operator != "subtraction" and self._overflow_cache.get( |
||||
address, False |
||||
): |
||||
continue |
||||
|
||||
issue = Issue(contract=node.contract_name, function=node.function_name, address=instruction['address'], |
||||
swc_id=INTEGER_OVERFLOW_AND_UNDERFLOW, title="Integer Underflow", _type="Warning") |
||||
try: |
||||
|
||||
issue.description = "A possible integer underflow exists in the function `" + node.function_name + "`.\n" \ |
||||
"The subtraction may result in a value < 0." |
||||
transaction_sequence = solver.get_transaction_sequence( |
||||
state, node.constraints + [annotation.constraint] |
||||
) |
||||
|
||||
issue.debug = solver.pretty_print_model(model) |
||||
issues.append(issue) |
||||
issue.debug = json.dumps(transaction_sequence, indent=4) |
||||
|
||||
except UnsatError: |
||||
logging.debug("[INTEGER_UNDERFLOW] no model found") |
||||
return issues |
||||
|
||||
|
||||
def _check_usage(state, taint_result): |
||||
"""Delegates checks to _check_{instruction_name}()""" |
||||
opcode = state.get_current_instruction()['opcode'] |
||||
|
||||
if opcode == 'JUMPI': |
||||
if _check_jumpi(state, taint_result): |
||||
return [state] |
||||
elif opcode == 'SSTORE': |
||||
if _check_sstore(state, taint_result): |
||||
return [state] |
||||
return [] |
||||
|
||||
def _check_jumpi(state, taint_result): |
||||
""" Check if conditional jump is dependent on the result of expression""" |
||||
assert state.get_current_instruction()['opcode'] == 'JUMPI' |
||||
return taint_result.check(state, -2) |
||||
|
||||
|
||||
def _check_sstore(state, taint_result): |
||||
""" Check if store operation is dependent on the result of expression""" |
||||
assert state.get_current_instruction()['opcode'] == 'SSTORE' |
||||
return taint_result.check(state, -2) |
||||
|
||||
|
||||
def _search_children(statespace, node, expression, taint_result=None, constraint=None, index=0, depth=0, max_depth=64): |
||||
""" |
||||
Checks the statespace for children states, with JUMPI or SSTORE instuctions, |
||||
for dependency on expression |
||||
:param statespace: The statespace to explore |
||||
:param node: Current node to explore from |
||||
:param expression: Expression to look for |
||||
:param taint_result: Result of taint analysis |
||||
:param index: Current state index node.states[index] == current_state |
||||
:param depth: Current depth level |
||||
:param max_depth: Max depth to explore |
||||
:return: List of states that match the opcodes and are dependent on expression |
||||
""" |
||||
if constraint is None: |
||||
constraint = [] |
||||
|
||||
logging.debug("SEARCHING NODE for usage of an overflowed variable %d", node.uid) |
||||
|
||||
if taint_result is None: |
||||
state = node.states[index] |
||||
taint_stack = [False for _ in state.mstate.stack] |
||||
taint_stack[-1] = True |
||||
taint_result = TaintRunner.execute(statespace, node, state, initial_stack=taint_stack) |
||||
|
||||
results = [] |
||||
|
||||
if depth >= max_depth: |
||||
return [] |
||||
|
||||
# Explore current node from index |
||||
for j in range(index, len(node.states)): |
||||
current_state = node.states[j] |
||||
current_instruction = current_state.get_current_instruction() |
||||
if current_instruction['opcode'] in ('JUMPI', 'SSTORE'): |
||||
element = _check_usage(current_state, taint_result) |
||||
if len(element) < 1: |
||||
continue |
||||
if _check_requires(element[0], node, statespace, constraint): |
||||
continue |
||||
results += element |
||||
|
||||
# Recursively search children |
||||
children = \ |
||||
[ |
||||
statespace.nodes[edge.node_to] |
||||
for edge in statespace.edges |
||||
if edge.node_from == node.uid |
||||
# and _try_constraints(statespace.nodes[edge.node_to].constraints, constraint) is not None |
||||
] |
||||
|
||||
for child in children: |
||||
results += _search_children(statespace, child, expression, taint_result, depth=depth + 1, max_depth=max_depth) |
||||
|
||||
return results |
||||
|
||||
|
||||
def _check_requires(state, node, statespace, constraint): |
||||
"""Checks if usage of overflowed statement results in a revert statement""" |
||||
instruction = state.get_current_instruction() |
||||
if instruction['opcode'] is not "JUMPI": |
||||
return False |
||||
children = [ |
||||
statespace.nodes[edge.node_to] |
||||
for edge in statespace.edges |
||||
if edge.node_from == node.uid |
||||
] |
||||
|
||||
for child in children: |
||||
opcodes = [s.get_current_instruction()['opcode'] for s in child.states] |
||||
if "REVERT" in opcodes or "ASSERT_FAIL" in opcodes: |
||||
return True |
||||
# I added the following case, bc of false positives if the max depth is not high enough |
||||
if len(children) == 0: |
||||
return True |
||||
return False |
||||
|
||||
if annotation.operator == "subtraction": |
||||
self._underflow_cache[address] = True |
||||
else: |
||||
self._overflow_cache[address] = True |
||||
self._issues.append(issue) |
||||
|
||||
@staticmethod |
||||
def _try_constraints(constraints, new_constraints): |
||||
""" |
||||
Tries new constraints |
||||
:return Model if satisfiable otherwise None |
||||
""" |
||||
try: |
||||
return solver.get_model(constraints + new_constraints) |
||||
except UnsatError: |
||||
return None |
||||
|
||||
|
||||
detector = IntegerOverflowUnderflowModule() |
||||
|
||||
|
||||
def _get_address_from_state(state): |
||||
return state.get_current_instruction()["address"] |
||||
|
||||
@ -1,61 +1,107 @@ |
||||
from mythril.analysis.report import Issue |
||||
from mythril.analysis.swc_data import * |
||||
from mythril.laser.ethereum.cfg import JumpType |
||||
""" |
||||
MODULE DESCRIPTION: |
||||
"""This module contains the detection code to find multiple sends occurring in |
||||
a single transaction.""" |
||||
from copy import copy |
||||
|
||||
Check for multiple sends in a single transaction |
||||
""" |
||||
from mythril.analysis.report import Issue |
||||
from mythril.analysis.swc_data import MULTIPLE_SENDS |
||||
from mythril.analysis.modules.base import DetectionModule |
||||
from mythril.laser.ethereum.state.annotation import StateAnnotation |
||||
from mythril.laser.ethereum.state.global_state import GlobalState |
||||
import logging |
||||
from mythril.analysis.call_helpers import get_call_from_state |
||||
|
||||
log = logging.getLogger(__name__) |
||||
|
||||
|
||||
class MultipleSendsAnnotation(StateAnnotation): |
||||
def __init__(self): |
||||
self.calls = [] |
||||
|
||||
def __copy__(self): |
||||
result = MultipleSendsAnnotation() |
||||
result.calls = copy(self.calls) |
||||
return result |
||||
|
||||
|
||||
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, |
||||
description="Check for multiple sends in a single transaction", |
||||
entrypoint="callback", |
||||
pre_hooks=[ |
||||
"CALL", |
||||
"DELEGATECALL", |
||||
"STATICCALL", |
||||
"CALLCODE", |
||||
"RETURN", |
||||
"STOP", |
||||
], |
||||
) |
||||
|
||||
def execute(self, state: GlobalState): |
||||
self._issues.extend(_analyze_state(state)) |
||||
return self.issues |
||||
|
||||
def execute(statespace): |
||||
issues = [] |
||||
|
||||
for call in statespace.calls: |
||||
findings = [] |
||||
# explore state |
||||
findings += _explore_states(call, statespace) |
||||
# explore nodes |
||||
findings += _explore_nodes(call, statespace) |
||||
def _analyze_state(state: GlobalState): |
||||
""" |
||||
:param state: the current state |
||||
:return: returns the issues for that corresponding state |
||||
""" |
||||
node = state.node |
||||
instruction = state.get_current_instruction() |
||||
|
||||
if len(findings) > 0: |
||||
node = call.node |
||||
instruction = call.state.get_current_instruction() |
||||
issue = Issue(contract=node.contract_name, function=node.function_name, address=instruction['address'], |
||||
swc_id=MULTIPLE_SENDS, title="Multiple Calls", _type="Informational") |
||||
annotations = [a for a in state.get_annotations(MultipleSendsAnnotation)] |
||||
if len(annotations) == 0: |
||||
log.debug("Creating annotation for state") |
||||
state.annotate(MultipleSendsAnnotation()) |
||||
annotations = [a for a in state.get_annotations(MultipleSendsAnnotation)] |
||||
|
||||
issue.description = \ |
||||
"Multiple sends exist in one transaction. Try to isolate each external call into its own transaction," \ |
||||
" as external calls can fail accidentally or deliberately.\nConsecutive calls: \n" |
||||
calls = annotations[0].calls |
||||
|
||||
for finding in findings: |
||||
issue.description += \ |
||||
"Call at address: {}\n".format(finding.state.get_current_instruction()['address']) |
||||
if instruction["opcode"] in ["CALL", "DELEGATECALL", "STATICCALL", "CALLCODE"]: |
||||
call = get_call_from_state(state) |
||||
if call: |
||||
calls += [call] |
||||
|
||||
issues.append(issue) |
||||
return issues |
||||
else: # RETURN or STOP |
||||
if len(calls) > 1: |
||||
|
||||
description_tail = ( |
||||
"Consecutive calls are executed at the following bytecode offsets:\n" |
||||
) |
||||
|
||||
def _explore_nodes(call, statespace): |
||||
children = _child_nodes(statespace, call.node) |
||||
sending_children = list(filter(lambda call: call.node in children, statespace.calls)) |
||||
return sending_children |
||||
for call in calls: |
||||
description_tail += "Offset: {}\n".format( |
||||
call.state.get_current_instruction()["address"] |
||||
) |
||||
|
||||
description_tail += ( |
||||
"Try to isolate each external call into its own transaction," |
||||
" as external calls can fail accidentally or deliberately.\n" |
||||
) |
||||
|
||||
def _explore_states(call, statespace): |
||||
other_calls = list( |
||||
filter(lambda other: other.node == call.node and other.state_index > call.state_index, statespace.calls) |
||||
) |
||||
return other_calls |
||||
issue = Issue( |
||||
contract=node.contract_name, |
||||
function_name=node.function_name, |
||||
address=instruction["address"], |
||||
swc_id=MULTIPLE_SENDS, |
||||
bytecode=state.environment.code.bytecode, |
||||
title="Multiple Calls in a Single Transaction", |
||||
severity="Medium", |
||||
description_head="Multiple sends are executed in one transaction.", |
||||
description_tail=description_tail, |
||||
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), |
||||
) |
||||
|
||||
return [issue] |
||||
|
||||
def _child_nodes(statespace, node): |
||||
result = [] |
||||
children = [statespace.nodes[edge.node_to] for edge in statespace.edges if edge.node_from == node.uid |
||||
and edge.type != JumpType.Transaction] |
||||
return [] |
||||
|
||||
for child in children: |
||||
result.append(child) |
||||
result += _child_nodes(statespace, child) |
||||
|
||||
return result |
||||
detector = MultipleSendsModule() |
||||
|
||||
@ -1,74 +1,101 @@ |
||||
from mythril.analysis import solver |
||||
from mythril.analysis.ops import * |
||||
from mythril.analysis.report import Issue |
||||
from mythril.analysis.swc_data import UNPROTECTED_SELFDESTRUCT |
||||
from mythril.exceptions import UnsatError |
||||
from mythril.analysis.modules.base import DetectionModule |
||||
from mythril.laser.ethereum.state.global_state import GlobalState |
||||
import logging |
||||
import json |
||||
|
||||
log = logging.getLogger(__name__) |
||||
|
||||
DESCRIPTION = """ |
||||
Check if the contact can be 'accidentally' killed by anyone. |
||||
For kill-able contracts, also check whether it is possible to direct the contract balance to the attacker. |
||||
""" |
||||
|
||||
|
||||
class SuicideModule(DetectionModule): |
||||
"""This module checks if the contact can be 'accidentally' killed by |
||||
anyone.""" |
||||
|
||||
def __init__(self): |
||||
super().__init__( |
||||
name="Unprotected Selfdestruct", |
||||
swc_id=UNPROTECTED_SELFDESTRUCT, |
||||
description=DESCRIPTION, |
||||
entrypoint="callback", |
||||
pre_hooks=["SUICIDE"], |
||||
) |
||||
self._cache_address = {} |
||||
|
||||
def reset_module(self): |
||||
""" |
||||
Resets the module |
||||
:return: |
||||
""" |
||||
super().reset_module() |
||||
self._cache_address = {} |
||||
|
||||
def execute(self, state: GlobalState): |
||||
""" |
||||
|
||||
:param state: |
||||
:return: |
||||
""" |
||||
self._issues.extend(self._analyze_state(state)) |
||||
return self.issues |
||||
|
||||
def _analyze_state(self, state): |
||||
log.info("Suicide module: Analyzing suicide instruction") |
||||
node = state.node |
||||
instruction = state.get_current_instruction() |
||||
if self._cache_address.get(instruction["address"], False): |
||||
return [] |
||||
to = state.mstate.stack[-1] |
||||
|
||||
log.debug("[SUICIDE] SUICIDE in function " + node.function_name) |
||||
|
||||
description_head = "The contract can be killed by anyone." |
||||
|
||||
try: |
||||
try: |
||||
transaction_sequence = solver.get_transaction_sequence( |
||||
state, |
||||
node.constraints |
||||
+ [to == 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF], |
||||
) |
||||
description_tail = "Arbitrary senders can kill this contract and withdraw its balance to their own account." |
||||
except UnsatError: |
||||
transaction_sequence = solver.get_transaction_sequence( |
||||
state, node.constraints |
||||
) |
||||
description_tail = ( |
||||
"Arbitrary senders can kill this contract but it is not possible to set the target address to which" |
||||
"the contract balance is sent." |
||||
) |
||||
|
||||
debug = json.dumps(transaction_sequence, indent=4) |
||||
self._cache_address[instruction["address"]] = True |
||||
|
||||
issue = Issue( |
||||
contract=node.contract_name, |
||||
function_name=node.function_name, |
||||
address=instruction["address"], |
||||
swc_id=UNPROTECTED_SELFDESTRUCT, |
||||
bytecode=state.environment.code.bytecode, |
||||
title="Unprotected Selfdestruct", |
||||
severity="High", |
||||
description_head=description_head, |
||||
description_tail=description_tail, |
||||
debug=debug, |
||||
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), |
||||
) |
||||
return [issue] |
||||
except UnsatError: |
||||
log.info("[UNCHECKED_SUICIDE] no model found") |
||||
|
||||
|
||||
''' |
||||
MODULE DESCRIPTION: |
||||
|
||||
Check for SUICIDE instructions that either can be reached by anyone, or where msg.sender is checked against a tainted storage index |
||||
(i.e. there's a write to that index is unconstrained by msg.sender). |
||||
''' |
||||
|
||||
|
||||
def execute(state_space): |
||||
|
||||
logging.debug("Executing module: UNCHECKED_SUICIDE") |
||||
|
||||
issues = [] |
||||
|
||||
for k in state_space.nodes: |
||||
node = state_space.nodes[k] |
||||
|
||||
for state in node.states: |
||||
issues += _analyze_state(state, node) |
||||
|
||||
return issues |
||||
|
||||
|
||||
def _analyze_state(state, node): |
||||
issues = [] |
||||
instruction = state.get_current_instruction() |
||||
|
||||
if instruction['opcode'] != "SUICIDE": |
||||
return [] |
||||
|
||||
to = state.mstate.stack[-1] |
||||
|
||||
logging.debug("[UNCHECKED_SUICIDE] suicide in function " + node.function_name) |
||||
description = "The function `" + node.function_name + "` executes the SUICIDE instruction. " |
||||
|
||||
if "caller" in str(to): |
||||
description += "The remaining Ether is sent to the caller's address.\n" |
||||
elif "storage" in str(to): |
||||
description += "The remaining Ether is sent to a stored address.\n" |
||||
elif "calldata" in str(to): |
||||
description += "The remaining Ether is sent to an address provided as a function argument.\n" |
||||
elif type(to) == BitVecNumRef: |
||||
description += "The remaining Ether is sent to: " + hex(to.as_long()) + "\n" |
||||
else: |
||||
description += "The remaining Ether is sent to: " + str(to) + "\n" |
||||
|
||||
not_creator_constraints = [] |
||||
if len(state.world_state.transaction_sequence) > 1: |
||||
creator = state.world_state.transaction_sequence[0].caller |
||||
for transaction in state.world_state.transaction_sequence[1:]: |
||||
not_creator_constraints.append(Not(Extract(159, 0, transaction.caller) == Extract(159, 0, creator))) |
||||
not_creator_constraints.append(Not(Extract(159, 0, transaction.caller) == 0)) |
||||
|
||||
try: |
||||
model = solver.get_model(node.constraints + not_creator_constraints) |
||||
|
||||
debug = "SOLVER OUTPUT:\n" + solver.pretty_print_model(model) |
||||
|
||||
issue = Issue(contract=node.contract_name, function=node.function_name, address=instruction['address'], |
||||
swc_id=UNPROTECTED_SELFDESTRUCT, title="Unchecked SUICIDE", _type="Warning", |
||||
description=description, debug=debug) |
||||
issues.append(issue) |
||||
except UnsatError: |
||||
logging.debug("[UNCHECKED_SUICIDE] no model found") |
||||
|
||||
return issues |
||||
|
||||
detector = SuicideModule() |
||||
|
||||
@ -1,136 +1,198 @@ |
||||
"""This module contains the detection code to find the existence of transaction |
||||
order dependence.""" |
||||
import copy |
||||
import logging |
||||
import re |
||||
|
||||
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.exceptions import UnsatError |
||||
|
||||
''' |
||||
MODULE DESCRIPTION: |
||||
This module finds the existance of transaction order dependence vulnerabilities. |
||||
The following webpage contains an extensive description of the vulnerability: |
||||
https://consensys.github.io/smart-contract-best-practices/known_attacks/#transaction-ordering-dependence-tod-front-running |
||||
''' |
||||
|
||||
|
||||
def execute(statespace): |
||||
""" Executes the analysis module""" |
||||
logging.debug("Executing module: TOD") |
||||
|
||||
issues = [] |
||||
|
||||
for call in statespace.calls: |
||||
# Do analysis |
||||
interesting_storages = list(_get_influencing_storages(call)) |
||||
changing_sstores = list(_get_influencing_sstores(statespace, interesting_storages)) |
||||
|
||||
# Build issue if necessary |
||||
if len(changing_sstores) > 0: |
||||
node = call.node |
||||
instruction = call.state.get_current_instruction() |
||||
issue = Issue(contract=node.contract_name, function=node.function_name, address=instruction['address'], |
||||
title="Transaction order dependence", swc_id=TX_ORDER_DEPENDENCE, _type="Warning") |
||||
|
||||
issue.description = \ |
||||
"A possible transaction order dependence vulnerability exists in function {}. The value or " \ |
||||
"direction of the call statement is determined from a tainted storage location"\ |
||||
.format(node.function_name) |
||||
issues.append(issue) |
||||
|
||||
return issues |
||||
|
||||
|
||||
# TODO: move to __init__ or util module |
||||
def _get_states_with_opcode(statespace, opcode): |
||||
""" Gets all (state, node) tuples in statespace with 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(expression): |
||||
""" Checks if expression is dependent on a storage symbol and returns the influencing storages""" |
||||
pattern = re.compile(r"storage_[a-z0-9_&^]*[0-9]+") |
||||
return pattern.findall(str(simplify(expression))) |
||||
|
||||
|
||||
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 |
||||
""" |
||||
index = int(re.search('[0-9]+', storage).group()) |
||||
try: |
||||
return state.environment.active_account.storage[index] |
||||
except KeyError: |
||||
return None |
||||
|
||||
|
||||
def _can_change(constraints, variable): |
||||
""" Checks if the variable can change given some constraints """ |
||||
_constraints = copy.deepcopy(constraints) |
||||
try: |
||||
model = solver.get_model(_constraints) |
||||
except UnsatError: |
||||
return False |
||||
try: |
||||
initial_value = int(str(model.eval(variable, model_completion=True))) |
||||
return _try_constraints(constraints, [variable != initial_value]) is not None |
||||
except AttributeError: |
||||
return False |
||||
|
||||
def _get_influencing_storages(call): |
||||
""" Examines a Call object and returns an iterator of all storages that influence the call value or direction""" |
||||
state = call.state |
||||
node = call.node |
||||
|
||||
# Get relevant storages |
||||
to, value = call.to, call.value |
||||
storages = [] |
||||
if to.type == VarType.SYMBOLIC: |
||||
storages += _dependent_on_storage(to.val) |
||||
if value.type == VarType.SYMBOLIC: |
||||
storages += _dependent_on_storage(value.val) |
||||
|
||||
# See if they can change within the constraints of the node |
||||
for storage in storages: |
||||
variable = _get_storage_variable(storage, state) |
||||
can_change = _can_change(node.constraints, variable) |
||||
if can_change: |
||||
yield storage |
||||
|
||||
|
||||
def _get_influencing_sstores(statespace, interesting_storages): |
||||
""" Gets sstore (state, node) tuples that write to interesting_storages""" |
||||
for sstore_state, node in _get_states_with_opcode(statespace, 'SSTORE'): |
||||
index, value = sstore_state.mstate.stack[-1], sstore_state.mstate.stack[-2] |
||||
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", |
||||
swc_id=TX_ORDER_DEPENDENCE, |
||||
description=( |
||||
"This module finds the existance of transaction order dependence " |
||||
"vulnerabilities. The following webpage contains an extensive description " |
||||
"of the vulnerability: " |
||||
"https://consensys.github.io/smart-contract-best-practices/known_attacks/#transaction-ordering-dependence-tod-front-running" |
||||
), |
||||
) |
||||
|
||||
def execute(self, statespace): |
||||
"""Executes the analysis module. |
||||
|
||||
:param statespace: |
||||
:return: |
||||
""" |
||||
log.debug("Executing module: TOD") |
||||
|
||||
issues = [] |
||||
|
||||
for call in statespace.calls: |
||||
# Do analysis |
||||
interesting_storages = list(self._get_influencing_storages(call)) |
||||
changing_sstores = list( |
||||
self._get_influencing_sstores(statespace, interesting_storages) |
||||
) |
||||
|
||||
description_tail = ( |
||||
"A transaction order dependence vulnerability may exist in this contract. The value or " |
||||
"target of the call statement is loaded from a writable storage location." |
||||
) |
||||
|
||||
# Build issue if necessary |
||||
if len(changing_sstores) > 0: |
||||
node = call.node |
||||
instruction = call.state.get_current_instruction() |
||||
issue = Issue( |
||||
contract=node.contract_name, |
||||
function_name=node.function_name, |
||||
address=instruction["address"], |
||||
title="Transaction Order Dependence", |
||||
bytecode=call.state.environment.code.bytecode, |
||||
swc_id=TX_ORDER_DEPENDENCE, |
||||
severity="Medium", |
||||
description_head="The call outcome may depend on transaction order.", |
||||
description_tail=description_tail, |
||||
gas_used=( |
||||
call.state.mstate.min_gas_used, |
||||
call.state.mstate.max_gas_used, |
||||
), |
||||
) |
||||
|
||||
issues.append(issue) |
||||
|
||||
return issues |
||||
|
||||
# TODO: move to __init__ or util module |
||||
@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 |
||||
|
||||
@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))) |
||||
|
||||
@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 |
||||
""" |
||||
index = int(re.search("[0-9]+", storage).group()) |
||||
try: |
||||
index = util.get_concrete_int(index) |
||||
except TypeError: |
||||
index = str(index) |
||||
if "storage_{}".format(index) not in interesting_storages: |
||||
continue |
||||
|
||||
yield sstore_state, node |
||||
|
||||
|
||||
# TODO: remove |
||||
def _try_constraints(constraints, new_constraints): |
||||
""" |
||||
Tries new constraints |
||||
:return Model if satisfiable otherwise None |
||||
""" |
||||
_constraints = copy.deepcopy(constraints) |
||||
for constraint in new_constraints: |
||||
_constraints.append(copy.deepcopy(constraint)) |
||||
try: |
||||
model = solver.get_model(_constraints) |
||||
return model |
||||
except UnsatError: |
||||
return None |
||||
return state.environment.active_account.storage[index] |
||||
except KeyError: |
||||
return None |
||||
|
||||
def _can_change(self, constraints, variable): |
||||
"""Checks if the variable can change given some constraints. |
||||
|
||||
:param constraints: |
||||
:param variable: |
||||
:return: |
||||
""" |
||||
_constraints = copy.deepcopy(constraints) |
||||
try: |
||||
model = solver.get_model(_constraints) |
||||
except UnsatError: |
||||
return False |
||||
try: |
||||
initial_value = int(str(model.eval(variable, model_completion=True))) |
||||
return ( |
||||
self._try_constraints(constraints, [variable != initial_value]) |
||||
is not None |
||||
) |
||||
except AttributeError: |
||||
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. |
||||
|
||||
:param call: |
||||
""" |
||||
state = call.state |
||||
node = call.node |
||||
|
||||
# Get relevant storages |
||||
to, value = call.to, call.value |
||||
storages = [] |
||||
if to.type == VarType.SYMBOLIC: |
||||
storages += self._dependent_on_storage(to.val) |
||||
if value.type == VarType.SYMBOLIC: |
||||
storages += self._dependent_on_storage(value.val) |
||||
|
||||
# See if they can change within the constraints of the node |
||||
for storage in storages: |
||||
variable = self._get_storage_variable(storage, state) |
||||
can_change = self._can_change(node.constraints, variable) |
||||
if can_change: |
||||
yield storage |
||||
|
||||
def _get_influencing_sstores(self, statespace, 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: |
||||
index = util.get_concrete_int(index) |
||||
except TypeError: |
||||
index = str(index) |
||||
if "storage_{}".format(index) not in interesting_storages: |
||||
continue |
||||
|
||||
yield sstore_state, node |
||||
|
||||
# TODO: remove |
||||
@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) |
||||
for constraint in new_constraints: |
||||
_constraints.append(copy.deepcopy(constraint)) |
||||
try: |
||||
model = solver.get_model(_constraints) |
||||
return model |
||||
except UnsatError: |
||||
return None |
||||
|
||||
|
||||
detector = TxOrderDependenceModule() |
||||
|
||||
@ -1,100 +1,111 @@ |
||||
"""This module contains detection code to find occurrences of calls whose |
||||
return value remains unchecked.""" |
||||
from copy import copy |
||||
|
||||
from mythril.analysis import solver |
||||
from mythril.analysis.report import Issue |
||||
from mythril.analysis.swc_data import UNCHECKED_RET_VAL |
||||
from mythril.analysis.modules.base import DetectionModule |
||||
from mythril.exceptions import UnsatError |
||||
from mythril.laser.ethereum.state.annotation import StateAnnotation |
||||
from mythril.laser.ethereum.state.global_state import GlobalState |
||||
|
||||
from mythril.laser.ethereum.svm import NodeFlags |
||||
import logging |
||||
import re |
||||
|
||||
|
||||
''' |
||||
MODULE DESCRIPTION: |
||||
|
||||
Test whether CALL return value is checked. |
||||
|
||||
For direct calls, the Solidity compiler auto-generates this check. E.g.: |
||||
|
||||
Alice c = Alice(address); |
||||
c.ping(42); |
||||
|
||||
Here the CALL will be followed by IZSERO(retval), if retval = ZERO then state is reverted. |
||||
|
||||
For low-level-calls this check is omitted. E.g.: |
||||
|
||||
c.call.value(0)(bytes4(sha3("ping(uint256)")),1); |
||||
|
||||
''' |
||||
|
||||
|
||||
def execute(statespace): |
||||
|
||||
logging.debug("Executing module: UNCHECKED_RETVAL") |
||||
|
||||
issues = [] |
||||
|
||||
for k in statespace.nodes: |
||||
|
||||
node = statespace.nodes[k] |
||||
|
||||
if NodeFlags.CALL_RETURN in node.flags: |
||||
|
||||
retval_checked = False |
||||
|
||||
for state in node.states: |
||||
|
||||
instr = state.get_current_instruction() |
||||
|
||||
if instr['opcode'] == 'ISZERO' and re.search(r'retval', str(state.mstate.stack[-1])): |
||||
retval_checked = True |
||||
break |
||||
|
||||
if not retval_checked: |
||||
|
||||
address = state.get_current_instruction()['address'] |
||||
issue = Issue(contract=node.contract_name, function=node.function_name, address=address, |
||||
title="Unchecked CALL return value", swc_id=UNCHECKED_RET_VAL) |
||||
|
||||
issue.description = \ |
||||
"The return value of an external call is not checked. " \ |
||||
"Note that execution continue even if the called contract throws." |
||||
|
||||
issues.append(issue) |
||||
|
||||
else: |
||||
|
||||
n_states = len(node.states) |
||||
|
||||
for idx in range(0, n_states - 1): # Ignore CALLs at last position in a node |
||||
|
||||
state = node.states[idx] |
||||
instr = state.get_current_instruction() |
||||
|
||||
if instr['opcode'] == 'CALL': |
||||
|
||||
retval_checked = False |
||||
|
||||
for _idx in range(idx, idx + 10): |
||||
|
||||
try: |
||||
_state = node.states[_idx] |
||||
_instr = _state.get_current_instruction() |
||||
|
||||
if _instr['opcode'] == 'ISZERO' and re.search(r'retval', str(_state .mstate.stack[-1])): |
||||
retval_checked = True |
||||
break |
||||
|
||||
except IndexError: |
||||
break |
||||
|
||||
if not retval_checked: |
||||
|
||||
address = instr['address'] |
||||
issue = Issue(contract=node.contract_name, function=node.function_name, |
||||
address=address, title="Unchecked CALL return value", swc_id=UNCHECKED_RET_VAL) |
||||
|
||||
issue.description = \ |
||||
"The return value of an external call is not checked. " \ |
||||
"Note that execution continue even if the called contract throws." |
||||
|
||||
issues.append(issue) |
||||
|
||||
return issues |
||||
log = logging.getLogger(__name__) |
||||
|
||||
|
||||
class UncheckedRetvalAnnotation(StateAnnotation): |
||||
def __init__(self): |
||||
self.retvals = [] |
||||
|
||||
def __copy__(self): |
||||
result = UncheckedRetvalAnnotation() |
||||
result.retvals = copy(self.retvals) |
||||
return result |
||||
|
||||
|
||||
class UncheckedRetvalModule(DetectionModule): |
||||
"""A detection module to test whether CALL return value is checked.""" |
||||
|
||||
def __init__(self): |
||||
super().__init__( |
||||
name="Unchecked Return Value", |
||||
swc_id=UNCHECKED_RET_VAL, |
||||
description=( |
||||
"Test whether CALL return value is checked. " |
||||
"For direct calls, the Solidity compiler auto-generates this check. E.g.:\n" |
||||
" Alice c = Alice(address);\n" |
||||
" c.ping(42);\n" |
||||
"Here the CALL will be followed by IZSERO(retval), if retval = ZERO then state is reverted. " |
||||
"For low-level-calls this check is omitted. E.g.:\n" |
||||
' c.call.value(0)(bytes4(sha3("ping(uint256)")),1);' |
||||
), |
||||
entrypoint="callback", |
||||
pre_hooks=["STOP", "RETURN"], |
||||
post_hooks=["CALL", "DELEGATECALL", "STATICCALL", "CALLCODE"], |
||||
) |
||||
|
||||
def execute(self, state: GlobalState) -> list: |
||||
""" |
||||
|
||||
:param state: |
||||
:return: |
||||
""" |
||||
self._issues.extend(_analyze_state(state)) |
||||
return self.issues |
||||
|
||||
|
||||
def _analyze_state(state: GlobalState) -> list: |
||||
instruction = state.get_current_instruction() |
||||
node = state.node |
||||
|
||||
annotations = [a for a in state.get_annotations(UncheckedRetvalAnnotation)] |
||||
if len(annotations) == 0: |
||||
state.annotate(UncheckedRetvalAnnotation()) |
||||
annotations = [a for a in state.get_annotations(UncheckedRetvalAnnotation)] |
||||
|
||||
retvals = annotations[0].retvals |
||||
|
||||
if instruction["opcode"] in ("STOP", "RETURN"): |
||||
issues = [] |
||||
for retval in retvals: |
||||
try: |
||||
solver.get_model(node.constraints + [retval["retval"] == 0]) |
||||
except UnsatError: |
||||
continue |
||||
|
||||
description_tail = ( |
||||
"External calls return a boolean value. If the callee contract halts with an exception, 'false' is " |
||||
"returned and execution continues in the caller. It is usually recommended to wrap external calls " |
||||
"into a require statement to prevent unexpected states." |
||||
) |
||||
|
||||
issue = Issue( |
||||
contract=node.contract_name, |
||||
function_name=node.function_name, |
||||
address=retval["address"], |
||||
bytecode=state.environment.code.bytecode, |
||||
title="Unchecked Call Return Value", |
||||
swc_id=UNCHECKED_RET_VAL, |
||||
severity="Low", |
||||
description_head="The return value of a message call is not checked.", |
||||
description_tail=description_tail, |
||||
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), |
||||
) |
||||
|
||||
issues.append(issue) |
||||
|
||||
return issues |
||||
else: |
||||
log.debug("End of call, extracting retval") |
||||
assert state.environment.code.instruction_list[state.mstate.pc - 1][ |
||||
"opcode" |
||||
] in ["CALL", "DELEGATECALL", "STATICCALL", "CALLCODE"] |
||||
retval = state.mstate.stack[-1] |
||||
retvals.append({"address": state.instruction["address"] - 1, "retval": retval}) |
||||
|
||||
return [] |
||||
|
||||
|
||||
detector = UncheckedRetvalModule() |
||||
|
||||
@ -1,80 +1,237 @@ |
||||
import hashlib |
||||
"""This module provides classes that make up an issue report.""" |
||||
import logging |
||||
import json |
||||
import operator |
||||
from jinja2 import PackageLoader, Environment |
||||
import _pysha3 as sha3 |
||||
import hashlib |
||||
|
||||
from mythril.solidity.soliditycontract import SolidityContract |
||||
from mythril.analysis.swc_data import SWC_TO_TITLE |
||||
from mythril.support.source_support import Source |
||||
|
||||
class Issue: |
||||
|
||||
def __init__(self, contract, function, address, swc_id, title, _type="Informational", description="", debug=""): |
||||
log = logging.getLogger(__name__) |
||||
|
||||
|
||||
class Issue: |
||||
"""Representation of an issue and its location.""" |
||||
|
||||
def __init__( |
||||
self, |
||||
contract, |
||||
function_name, |
||||
address, |
||||
swc_id, |
||||
title, |
||||
bytecode, |
||||
gas_used=(None, None), |
||||
severity=None, |
||||
description_head="", |
||||
description_tail="", |
||||
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 |
||||
self.function = function_name |
||||
self.address = address |
||||
self.description = description |
||||
self.type = _type |
||||
self.description_head = description_head |
||||
self.description_tail = description_tail |
||||
self.description = "%s\n%s" % (description_head, description_tail) |
||||
self.severity = severity |
||||
self.debug = debug |
||||
self.swc_id = swc_id |
||||
self.min_gas_used, self.max_gas_used = gas_used |
||||
self.filename = None |
||||
self.code = None |
||||
self.lineno = None |
||||
|
||||
self.source_mapping = None |
||||
|
||||
try: |
||||
keccak = sha3.keccak_256() |
||||
keccak.update(bytes.fromhex(bytecode)) |
||||
self.bytecode_hash = "0x" + keccak.hexdigest() |
||||
except ValueError: |
||||
log.debug( |
||||
"Unable to change the bytecode to bytes. Bytecode: {}".format(bytecode) |
||||
) |
||||
self.bytecode_hash = "" |
||||
|
||||
@property |
||||
def as_dict(self): |
||||
|
||||
issue = {'title': self.title, 'swc_id': self.swc_id, 'contract': self.contract, 'description': self.description, |
||||
'function': self.function, 'type': self.type, 'address': self.address, 'debug': self.debug} |
||||
""" |
||||
|
||||
:return: |
||||
""" |
||||
issue = { |
||||
"title": self.title, |
||||
"swc-id": self.swc_id, |
||||
"contract": self.contract, |
||||
"description": self.description, |
||||
"function": self.function, |
||||
"severity": self.severity, |
||||
"address": self.address, |
||||
"debug": self.debug, |
||||
"min_gas_used": self.min_gas_used, |
||||
"max_gas_used": self.max_gas_used, |
||||
"sourceMap": self.source_mapping, |
||||
} |
||||
|
||||
if self.filename and self.lineno: |
||||
issue['filename'] = self.filename |
||||
issue['lineno'] = self.lineno |
||||
issue["filename"] = self.filename |
||||
issue["lineno"] = self.lineno |
||||
|
||||
if self.code: |
||||
issue['code'] = self.code |
||||
issue["code"] = self.code |
||||
|
||||
return issue |
||||
|
||||
def add_code_info(self, contract): |
||||
if self.address: |
||||
codeinfo = contract.get_source_info(self.address, constructor=(self.function == 'constructor')) |
||||
""" |
||||
|
||||
:param contract: |
||||
""" |
||||
if self.address and isinstance(contract, SolidityContract): |
||||
codeinfo = contract.get_source_info( |
||||
self.address, constructor=(self.function == "constructor") |
||||
) |
||||
self.filename = codeinfo.filename |
||||
self.code = codeinfo.code |
||||
self.lineno = codeinfo.lineno |
||||
self.source_mapping = codeinfo.solc_mapping |
||||
else: |
||||
self.source_mapping = self.address |
||||
|
||||
|
||||
class Report: |
||||
environment = Environment(loader=PackageLoader('mythril.analysis'), trim_blocks=True) |
||||
"""A report containing the content of multiple issues.""" |
||||
|
||||
environment = Environment( |
||||
loader=PackageLoader("mythril.analysis"), trim_blocks=True |
||||
) |
||||
|
||||
def __init__(self, verbose=False, source=None): |
||||
""" |
||||
|
||||
def __init__(self, verbose=False): |
||||
:param verbose: |
||||
""" |
||||
self.issues = {} |
||||
self.verbose = verbose |
||||
pass |
||||
self.solc_version = "" |
||||
self.meta = {} |
||||
self.source = source or Source() |
||||
|
||||
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')) |
||||
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')) |
||||
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(filename=name, issues=self.sorted_issues(), verbose=self.verbose) |
||||
template = Report.environment.get_template("report_as_text.jinja2") |
||||
return template.render( |
||||
filename=name, issues=self.sorted_issues(), verbose=self.verbose |
||||
) |
||||
|
||||
def as_json(self): |
||||
result = {'success': True, 'error': None, 'issues': self.sorted_issues()} |
||||
""" |
||||
|
||||
: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. |
||||
|
||||
:return: |
||||
""" |
||||
_issues = [] |
||||
source_list = [] |
||||
|
||||
for key, issue in self.issues.items(): |
||||
|
||||
if issue.bytecode_hash not in source_list: |
||||
idx = len(source_list) |
||||
source_list.append(issue.bytecode_hash) |
||||
else: |
||||
idx = source_list.index(issue.bytecode_hash) |
||||
|
||||
try: |
||||
title = SWC_TO_TITLE[issue.swc_id] |
||||
except KeyError: |
||||
title = "Unspecified Security Issue" |
||||
|
||||
_issues.append( |
||||
{ |
||||
"swcID": "SWC-" + issue.swc_id, |
||||
"swcTitle": title, |
||||
"description": { |
||||
"head": issue.description_head, |
||||
"tail": issue.description_tail, |
||||
}, |
||||
"severity": issue.severity, |
||||
"locations": [{"sourceMap": "%d:1:%d" % (issue.address, idx)}], |
||||
"extra": {}, |
||||
} |
||||
) |
||||
|
||||
result = [ |
||||
{ |
||||
"issues": _issues, |
||||
"sourceType": "raw-bytecode", |
||||
"sourceFormat": "evm-byzantium-bytecode", |
||||
"sourceList": source_list, |
||||
"meta": {}, |
||||
} |
||||
] |
||||
|
||||
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(filename=filename, issues=self.sorted_issues(), verbose=self.verbose) |
||||
template = Report.environment.get_template("report_as_markdown.jinja2") |
||||
return template.render( |
||||
filename=filename, issues=self.sorted_issues(), verbose=self.verbose |
||||
) |
||||
|
||||
def _file_name(self): |
||||
""" |
||||
|
||||
:return: |
||||
""" |
||||
if len(self.issues.values()) > 0: |
||||
return list(self.issues.values())[0].filename |
||||
|
||||
@ -1,22 +1,106 @@ |
||||
from mythril.analysis.report import Report |
||||
"""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 |
||||
import pkgutil |
||||
import importlib.util |
||||
import logging |
||||
|
||||
log = logging.getLogger(__name__) |
||||
|
||||
def fire_lasers(statespace, module_names=None): |
||||
OPCODE_LIST = [c[0] for _, c in opcodes.items()] |
||||
|
||||
issues = [] |
||||
_modules = [] |
||||
|
||||
for loader, name, is_pkg in pkgutil.walk_packages(modules.__path__): |
||||
_modules.append(loader.find_module(name).load_module(name)) |
||||
def reset_callback_modules(): |
||||
"""Clean the issue records of every callback-based module.""" |
||||
modules = get_detection_modules("callback") |
||||
for module in modules: |
||||
module.detector.reset_module() |
||||
|
||||
logging.info("Starting analysis") |
||||
|
||||
def get_detection_module_hooks(modules, hook_type="pre"): |
||||
hook_dict = defaultdict(list) |
||||
_modules = get_detection_modules(entrypoint="callback", include_modules=modules) |
||||
for module in _modules: |
||||
if not module_names or module.__name__ in module_names: |
||||
logging.info("Executing " + str(module)) |
||||
issues += module.execute(statespace) |
||||
hooks = ( |
||||
module.detector.pre_hooks |
||||
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) |
||||
elif op_code.endswith("*"): |
||||
to_register = filter(lambda x: x.startswith(op_code[:-1]), OPCODE_LIST) |
||||
for actual_hook in to_register: |
||||
hook_dict[actual_hook].append(module.detector.execute) |
||||
else: |
||||
log.error( |
||||
"Encountered invalid hook opcode %s in module %s", |
||||
op_code, |
||||
module.detector.name, |
||||
) |
||||
return dict(hook_dict) |
||||
|
||||
|
||||
def get_detection_modules(entrypoint, include_modules=()): |
||||
""" |
||||
|
||||
:param entrypoint: |
||||
:param include_modules: |
||||
:return: |
||||
""" |
||||
include_modules = list(include_modules) |
||||
|
||||
_modules = [] |
||||
|
||||
if not include_modules: |
||||
for loader, module_name, _ in pkgutil.walk_packages(modules.__path__): |
||||
if module_name != "base": |
||||
module = importlib.import_module( |
||||
"mythril.analysis.modules." + module_name |
||||
) |
||||
if module.detector.entrypoint == entrypoint: |
||||
_modules.append(module) |
||||
else: |
||||
for module_name in include_modules: |
||||
module = importlib.import_module("mythril.analysis.modules." + module_name) |
||||
if module.__name__ != "base" and module.detector.entrypoint == entrypoint: |
||||
_modules.append(module) |
||||
|
||||
log.info("Found %s detection modules", len(_modules)) |
||||
return _modules |
||||
|
||||
|
||||
def fire_lasers(statespace, module_names=()): |
||||
""" |
||||
|
||||
:param statespace: |
||||
:param module_names: |
||||
:return: |
||||
""" |
||||
log.info("Starting analysis") |
||||
|
||||
issues = [] |
||||
for module in get_detection_modules( |
||||
entrypoint="post", include_modules=module_names |
||||
): |
||||
log.info("Executing " + module.detector.name) |
||||
issues += module.detector.execute(statespace) |
||||
|
||||
issues += retrieve_callback_issues(module_names) |
||||
return issues |
||||
|
||||
|
||||
def retrieve_callback_issues(module_names=()): |
||||
issues = [] |
||||
for module in get_detection_modules( |
||||
entrypoint="callback", include_modules=module_names |
||||
): |
||||
log.debug("Retrieving results for " + module.detector.name) |
||||
issues += module.detector.issues |
||||
|
||||
reset_callback_modules() |
||||
return issues |
||||
|
||||
@ -1,32 +1,131 @@ |
||||
from z3 import Solver, simplify, sat, unknown |
||||
"""This module contains analysis module helpers to solve path constraints.""" |
||||
from z3 import sat, unknown, FuncInterp |
||||
import z3 |
||||
|
||||
from mythril.laser.smt import simplify, UGE, Optimize, symbol_factory |
||||
from mythril.exceptions import UnsatError |
||||
from mythril.laser.ethereum.transaction.transaction_models import ( |
||||
ContractCreationTransaction, |
||||
) |
||||
import logging |
||||
|
||||
def get_model(constraints): |
||||
s = Solver() |
||||
s.set("timeout", 100000) |
||||
log = logging.getLogger(__name__) |
||||
|
||||
|
||||
def get_model(constraints, minimize=(), maximize=()): |
||||
""" |
||||
|
||||
:param constraints: |
||||
:param minimize: |
||||
:param maximize: |
||||
:return: |
||||
""" |
||||
s = Optimize() |
||||
s.set_timeout(100000) |
||||
|
||||
for constraint in constraints: |
||||
if type(constraint) == bool and not constraint: |
||||
raise UnsatError |
||||
|
||||
constraints = [constraint for constraint in constraints if type(constraint) != bool] |
||||
|
||||
for constraint in constraints: |
||||
s.add(constraint) |
||||
for e in minimize: |
||||
s.minimize(e) |
||||
for e in maximize: |
||||
s.maximize(e) |
||||
|
||||
result = s.check() |
||||
if result == sat: |
||||
return s.model() |
||||
elif result == unknown: |
||||
logging.info("Timeout encountered while solving expression using z3") |
||||
log.debug("Timeout encountered while solving expression using z3") |
||||
raise UnsatError |
||||
|
||||
|
||||
def pretty_print_model(model): |
||||
""" |
||||
|
||||
:param model: |
||||
:return: |
||||
""" |
||||
ret = "" |
||||
|
||||
for d in model.decls(): |
||||
if type(model[d]) == FuncInterp: |
||||
condition = model[d].as_list() |
||||
ret += "%s: %s\n" % (d.name(), condition) |
||||
continue |
||||
|
||||
try: |
||||
condition = "0x%x" % model[d].as_long() |
||||
except: |
||||
condition = str(simplify(model[d])) |
||||
condition = str(z3.simplify(model[d])) |
||||
|
||||
ret += ("%s: %s\n" % (d.name(), condition)) |
||||
ret += "%s: %s\n" % (d.name(), condition) |
||||
|
||||
return ret |
||||
|
||||
|
||||
def get_transaction_sequence(global_state, constraints): |
||||
"""Generate concrete transaction sequence. |
||||
|
||||
:param global_state: GlobalState to generate transaction sequence for |
||||
:param constraints: list of constraints used to generate transaction sequence |
||||
""" |
||||
|
||||
transaction_sequence = global_state.world_state.transaction_sequence |
||||
|
||||
# gaslimit & gasprice don't exist yet |
||||
tx_template = { |
||||
"calldata": None, |
||||
"call_value": None, |
||||
"caller": "0xCA11EDEADBEEF37E636E6CA11EDEADBEEFCA11ED", |
||||
} |
||||
|
||||
concrete_transactions = {} |
||||
creation_tx_ids = [] |
||||
tx_constraints = constraints.copy() |
||||
minimize = [] |
||||
|
||||
transactions = [] |
||||
for transaction in transaction_sequence: |
||||
tx_id = str(transaction.id) |
||||
if not isinstance(transaction, ContractCreationTransaction): |
||||
transactions.append(transaction) |
||||
# Constrain calldatasize |
||||
max_calldatasize = symbol_factory.BitVecVal(5000, 256) |
||||
tx_constraints.append( |
||||
UGE(max_calldatasize, transaction.call_data.calldatasize) |
||||
) |
||||
|
||||
minimize.append(transaction.call_data.calldatasize) |
||||
minimize.append(transaction.call_value) |
||||
|
||||
concrete_transactions[tx_id] = tx_template.copy() |
||||
|
||||
else: |
||||
creation_tx_ids.append(tx_id) |
||||
|
||||
model = get_model(tx_constraints, minimize=minimize) |
||||
|
||||
for transaction in transactions: |
||||
tx_id = str(transaction.id) |
||||
|
||||
concrete_transactions[tx_id]["calldata"] = "0x" + "".join( |
||||
[ |
||||
hex(b)[2:] if len(hex(b)) % 2 == 0 else "0" + hex(b)[2:] |
||||
for b in transaction.call_data.concrete(model) |
||||
] |
||||
) |
||||
|
||||
concrete_transactions[tx_id]["call_value"] = ( |
||||
"0x%x" |
||||
% model.eval(transaction.call_value.raw, model_completion=True).as_long() |
||||
) |
||||
concrete_transactions[tx_id]["caller"] = "0x" + ( |
||||
"%x" % model.eval(transaction.caller.raw, model_completion=True).as_long() |
||||
).zfill(40) |
||||
|
||||
return concrete_transactions |
||||
|
||||
@ -1,25 +1,63 @@ |
||||
DEFAULT_FUNCTION_VISIBILITY = '100' |
||||
INTEGER_OVERFLOW_AND_UNDERFLOW = '101' |
||||
OUTDATED_COMPILER_VERSION = '102' |
||||
FLOATING_PRAGMA = '103' |
||||
UNCHECKED_RET_VAL = '104' |
||||
UNPROTECTED_ETHER_WITHDRAWAL = '105' |
||||
UNPROTECTED_SELFDESTRUCT = '106' |
||||
REENTRANCY = '107' |
||||
DEFAULT_STATE_VARIABLE_VISIBILITY = '108' |
||||
UNINITIALIZED_STORAGE_POINTER = '109' |
||||
ASSERT_VIOLATION = '110' |
||||
DEPRICATED_FUNCTIONS_USAGE = '111' |
||||
DELEGATECALL_TO_UNTRUSTED_CONTRACT = '112' |
||||
MULTIPLE_SENDS = '113' |
||||
TX_ORDER_DEPENDENCE = '114' |
||||
TX_ORIGIN_USAGE = '115' |
||||
TIMESTAMP_DEPENDENCE = '116' |
||||
# TODO: SWC ID 116 is missing, Add it if it's added to the https://github.com/SmartContractSecurity/SWC-registry |
||||
INCORRECT_CONSTRUCTOR_NAME = '118' |
||||
SHADOWING_STATE_VARIABLES = '119' |
||||
WEAK_RANDOMNESS = '120' |
||||
SIGNATURE_REPLAY = '121' |
||||
IMPROPER_VERIFICATION_BASED_ON_MSG_SENDER = '122' |
||||
"""This module maps SWC IDs to their registry equivalents.""" |
||||
|
||||
PREDICTABLE_VARS_DEPENDENCE = 'N/A' # TODO: Add the swc id when this is added to the SWC Registry |
||||
DEFAULT_FUNCTION_VISIBILITY = "100" |
||||
INTEGER_OVERFLOW_AND_UNDERFLOW = "101" |
||||
OUTDATED_COMPILER_VERSION = "102" |
||||
FLOATING_PRAGMA = "103" |
||||
UNCHECKED_RET_VAL = "104" |
||||
UNPROTECTED_ETHER_WITHDRAWAL = "105" |
||||
UNPROTECTED_SELFDESTRUCT = "106" |
||||
REENTRANCY = "107" |
||||
DEFAULT_STATE_VARIABLE_VISIBILITY = "108" |
||||
UNINITIALIZED_STORAGE_POINTER = "109" |
||||
ASSERT_VIOLATION = "110" |
||||
DEPRICATED_FUNCTIONS_USAGE = "111" |
||||
DELEGATECALL_TO_UNTRUSTED_CONTRACT = "112" |
||||
MULTIPLE_SENDS = "113" |
||||
TX_ORDER_DEPENDENCE = "114" |
||||
TX_ORIGIN_USAGE = "115" |
||||
TIMESTAMP_DEPENDENCE = "116" |
||||
INCORRECT_CONSTRUCTOR_NAME = "118" |
||||
SHADOWING_STATE_VARIABLES = "119" |
||||
WEAK_RANDOMNESS = "120" |
||||
SIGNATURE_REPLAY = "121" |
||||
IMPROPER_VERIFICATION_BASED_ON_MSG_SENDER = "122" |
||||
REQUIREMENT_VIOLATION = "123" |
||||
WRITE_TO_ARBITRARY_STORAGE = "124" |
||||
INCORRECT_INHERITANCE_ORDER = "125" |
||||
ARBITRARY_JUMP = "127" |
||||
DOS_WITH_BLOCK_GAS_LIMIT = "128" |
||||
TYPOGRAPHICAL_ERROR = "129" |
||||
|
||||
|
||||
SWC_TO_TITLE = { |
||||
"100": "Function Default Visibility", |
||||
"101": "Integer Overflow and Underflow", |
||||
"102": "Outdated Compiler Version", |
||||
"103": "Floating Pragma", |
||||
"104": "Unchecked Call Return Value", |
||||
"105": "Unprotected Ether Withdrawal", |
||||
"106": "Unprotected SELFDESTRUCT Instruction", |
||||
"107": "Reentrancy", |
||||
"108": "State Variable Default Visibility", |
||||
"109": "Uninitialized Storage Pointer", |
||||
"110": "Assert Violation", |
||||
"111": "Use of Deprecated Solidity Functions", |
||||
"112": "Delegatecall to Untrusted Callee", |
||||
"113": "DoS with Failed Call", |
||||
"114": "Transaction Order Dependence", |
||||
"115": "Authorization through tx.origin", |
||||
"116": "Timestamp Dependence", |
||||
"117": "Signature Malleability", |
||||
"118": "Incorrect Constructor Name", |
||||
"119": "Shadowing State Variables", |
||||
"120": "Weak Sources of Randomness from Chain Attributes", |
||||
"121": "Missing Protection against Signature Replay Attacks", |
||||
"122": "Lack of Proper Signature Verification", |
||||
"123": "Requirement Violation", |
||||
"124": "Write to Arbitrary Storage Location", |
||||
"125": "Incorrect Inheritance Order", |
||||
"127": "Arbitrary Jump with Function Type Variable", |
||||
"128": "DoS With Block Gas Limit", |
||||
"129": "Typographical Error", |
||||
} |
||||
|
||||
@ -0,0 +1,127 @@ |
||||
"""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(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.""" |
||||
|
||||
def __init__(self, address, op_code, argument=None): |
||||
self.address = address |
||||
self.op_code = op_code |
||||
self.argument = argument |
||||
|
||||
def to_dict(self) -> dict: |
||||
""" |
||||
|
||||
:return: |
||||
""" |
||||
result = {"address": self.address, "opcode": self.op_code} |
||||
if self.argument: |
||||
result["argument"] = self.argument |
||||
return result |
||||
|
||||
|
||||
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: |
||||
result += "{} {}".format(instruction["address"], instruction["opcode"]) |
||||
if "argument" in instruction: |
||||
result += " " + instruction["argument"] |
||||
result += "\n" |
||||
|
||||
return result |
||||
|
||||
|
||||
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 |
||||
raise RuntimeError("Unknown opcode") |
||||
|
||||
|
||||
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, 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 |
||||
""" |
||||
for i in range(0, len(instruction_list) - len(pattern) + 1): |
||||
if is_sequence_match(pattern, instruction_list, i): |
||||
yield i |
||||
|
||||
|
||||
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, 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 |
||||
""" |
||||
for index, pattern_slot in enumerate(pattern, start=index): |
||||
try: |
||||
if not instruction_list[index]["opcode"] in pattern_slot: |
||||
return False |
||||
except IndexError: |
||||
return False |
||||
return True |
||||
|
||||
|
||||
def disassemble(bytecode: str) -> list: |
||||
"""Disassembles evm bytecode and returns a list of instructions. |
||||
|
||||
:param bytecode: |
||||
:return: |
||||
""" |
||||
instruction_list = [] |
||||
address = 0 |
||||
length = len(bytecode) |
||||
if "bzzr" in str(bytecode[-43:]): |
||||
# ignore swarm hash |
||||
length -= 43 |
||||
|
||||
while address < length: |
||||
try: |
||||
op_code = opcodes[bytecode[address]] |
||||
except KeyError: |
||||
instruction_list.append(EvmInstruction(address, "INVALID")) |
||||
address += 1 |
||||
continue |
||||
|
||||
op_code_name = op_code[0] |
||||
current_instruction = EvmInstruction(address, op_code_name) |
||||
|
||||
match = re.search(regex_PUSH, op_code_name) |
||||
if match: |
||||
argument_bytes = bytecode[address + 1 : address + 1 + int(match.group(1))] |
||||
current_instruction.argument = "0x" + argument_bytes.hex() |
||||
address += int(match.group(1)) |
||||
|
||||
instruction_list.append(current_instruction) |
||||
address += 1 |
||||
|
||||
# We use a to_dict() here for compatibility reasons |
||||
return [element.to_dict() for element in instruction_list] |
||||
@ -1,60 +1,96 @@ |
||||
from mythril.ether import asm, util |
||||
from mythril.support.signatures import SignatureDb |
||||
import logging |
||||
"""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. |
||||
|
||||
def __init__(self, code, enable_online_lookup=True): |
||||
self.instruction_list = asm.disassemble(util.safe_decode(code)) |
||||
self.func_hashes = [] |
||||
self.func_to_addr = {} |
||||
self.addr_to_func = {} |
||||
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 |
||||
""" |
||||
|
||||
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)) |
||||
|
||||
signatures = SignatureDb(enable_online_lookup=enable_online_lookup) # control if you want to have online sighash lookups |
||||
try: |
||||
signatures.open() # open from default locations |
||||
except FileNotFoundError: |
||||
logging.info("Missing function signature file. Resolving of function names from signature file disabled.") |
||||
self.func_hashes = [] |
||||
self.function_name_to_address = {} |
||||
self.address_to_function_name = {} |
||||
|
||||
# Parse jump table & resolve function names |
||||
# open from default locations |
||||
# control if you want to have online signature hash lookups |
||||
signatures = SignatureDB(enable_online_lookup=enable_online_lookup) |
||||
|
||||
# Need to take from PUSH1 to PUSH4 because solc seems to remove excess 0s at the beginning for optimizing |
||||
jmptable_indices = asm.find_opcode_sequence([("PUSH1", "PUSH2", "PUSH3", "PUSH4"), ("EQ",)], |
||||
self.instruction_list) |
||||
|
||||
for i in jmptable_indices: |
||||
func_hash = self.instruction_list[i]['argument'] |
||||
|
||||
# Append with missing 0s at the beginning |
||||
func_hash = "0x" + func_hash[2:].rjust(8, "0") |
||||
|
||||
self.func_hashes.append(func_hash) |
||||
try: |
||||
# tries local cache, file and optional online lookup |
||||
# may return more than one function signature. since we cannot probe for the correct one we'll use the first |
||||
func_names = signatures.get(func_hash) |
||||
if len(func_names) > 1: |
||||
# ambigious result |
||||
func_name = "**ambiguous** %s" % func_names[0] # return first hit but note that result was ambiguous |
||||
else: |
||||
# only one item |
||||
func_name = func_names[0] |
||||
except KeyError: |
||||
func_name = "_function_" + func_hash |
||||
|
||||
try: |
||||
offset = self.instruction_list[i + 2]['argument'] |
||||
jump_target = int(offset, 16) |
||||
|
||||
self.func_to_addr[func_name] = jump_target |
||||
self.addr_to_func[jump_target] = func_name |
||||
except: |
||||
continue |
||||
|
||||
signatures.write() # store resolved signatures (potentially resolved online) |
||||
jump_table_indices = asm.find_op_code_sequence( |
||||
[("PUSH1", "PUSH2", "PUSH3", "PUSH4"), ("EQ",)], self.instruction_list |
||||
) |
||||
|
||||
for index in jump_table_indices: |
||||
function_hash, jump_target, function_name = get_function_info( |
||||
index, self.instruction_list, signatures |
||||
) |
||||
self.func_hashes.append(function_hash) |
||||
|
||||
if jump_target is not None and function_name is not None: |
||||
self.function_name_to_address[function_name] = jump_target |
||||
self.address_to_function_name[jump_target] = function_name |
||||
|
||||
def get_easm(self): |
||||
# todo: tintinweb - print funcsig resolved data from self.addr_to_func? |
||||
""" |
||||
|
||||
: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: |
||||
|
||||
- PUSH function_hash |
||||
- EQ |
||||
- PUSH entry_point |
||||
- JUMPI |
||||
|
||||
This function takes an index that points to the first instruction, and from that finds out the function hash, |
||||
function entry and the function name. |
||||
|
||||
:param index: Start of the entry pattern |
||||
:param instruction_list: Instruction list for the contract that is being analyzed |
||||
:param signature_database: Database used to map function hashes to their respective function names |
||||
:return: function hash, function entry point, function name |
||||
""" |
||||
|
||||
# Append with missing 0s at the beginning |
||||
function_hash = "0x" + instruction_list[index]["argument"][2:].rjust(8, "0") |
||||
function_names = signature_database.get(function_hash) |
||||
if len(function_names) > 1: |
||||
# In this case there was an ambiguous result |
||||
function_name = "[{}] (ambiguous)".format(", ".join(function_names)) |
||||
elif len(function_names) == 1: |
||||
function_name = function_names[0] |
||||
else: |
||||
function_name = "_function_" + function_hash |
||||
|
||||
try: |
||||
offset = instruction_list[index + 2]["argument"] |
||||
entry_point = int(offset, 16) |
||||
except (KeyError, IndexError): |
||||
return function_hash, None, None |
||||
|
||||
return function_hash, entry_point, function_name |
||||
|
||||
@ -1,3 +0,0 @@ |
||||
import time |
||||
|
||||
start_time = time.time() |
||||
@ -1,152 +0,0 @@ |
||||
import sys |
||||
import re |
||||
from ethereum.opcodes import opcodes |
||||
from mythril.ether import util |
||||
|
||||
|
||||
regex_PUSH = re.compile('^PUSH(\d*)$') |
||||
|
||||
# Additional mnemonic to catch failed assertions |
||||
|
||||
opcodes[254] = ['ASSERT_FAIL', 0, 0, 0] |
||||
|
||||
|
||||
def instruction_list_to_easm(instruction_list): |
||||
easm = "" |
||||
|
||||
for instruction in instruction_list: |
||||
|
||||
easm += str(instruction['address']) + " " + instruction['opcode'] |
||||
|
||||
if 'argument' in instruction: |
||||
easm += " " + instruction['argument'] |
||||
|
||||
easm += "\n" |
||||
|
||||
return easm |
||||
|
||||
|
||||
def easm_to_instruction_list(easm): |
||||
|
||||
regex_CODELINE = re.compile('^([A-Z0-9]+)(?:\s+([0-9a-fA-Fx]+))?$') |
||||
|
||||
instruction_list = [] |
||||
|
||||
codelines = easm.split('\n') |
||||
|
||||
for line in codelines: |
||||
|
||||
m = re.search(regex_CODELINE, line) |
||||
|
||||
if not m: |
||||
# Invalid code line |
||||
continue |
||||
|
||||
instruction = {'opcode': m.group(1)} |
||||
|
||||
if m.group(2): |
||||
instruction['argument'] = m.group(2)[2:] |
||||
|
||||
instruction_list.append(instruction) |
||||
|
||||
return instruction_list |
||||
|
||||
|
||||
def get_opcode_from_name(name): |
||||
|
||||
for opcode, value in opcodes.items(): |
||||
|
||||
if name == value[0]: |
||||
|
||||
return opcode |
||||
|
||||
raise RuntimeError("Unknown opcode") |
||||
|
||||
|
||||
def find_opcode_sequence(pattern, instruction_list): |
||||
match_indexes = [] |
||||
|
||||
pattern_length = len(pattern) |
||||
|
||||
for i in range(0, len(instruction_list) - pattern_length + 1): |
||||
|
||||
if instruction_list[i]['opcode'] in pattern[0]: |
||||
|
||||
matched = True |
||||
|
||||
for j in range(1, len(pattern)): |
||||
|
||||
if not (instruction_list[i + j]['opcode'] in pattern[j]): |
||||
matched = False |
||||
break |
||||
|
||||
if matched: |
||||
match_indexes.append(i) |
||||
|
||||
return match_indexes |
||||
|
||||
|
||||
def disassemble(bytecode): |
||||
|
||||
instruction_list = [] |
||||
addr = 0 |
||||
|
||||
length = len(bytecode) |
||||
|
||||
if "bzzr" in str(bytecode[-43:]): |
||||
# ignore swarm hash |
||||
length -= 43 |
||||
|
||||
while addr < length: |
||||
|
||||
instruction = {'address': addr} |
||||
|
||||
try: |
||||
if sys.version_info > (3, 0): |
||||
opcode = opcodes[bytecode[addr]] |
||||
else: |
||||
opcode = opcodes[ord(bytecode[addr])] |
||||
|
||||
except KeyError: |
||||
|
||||
# invalid opcode |
||||
instruction_list.append({'address': addr, 'opcode': "INVALID"}) |
||||
addr += 1 |
||||
continue |
||||
|
||||
instruction['opcode'] = opcode[0] |
||||
|
||||
m = re.search(regex_PUSH, opcode[0]) |
||||
|
||||
if m: |
||||
argument = bytecode[addr+1:addr+1+int(m.group(1))] |
||||
instruction['argument'] = "0x" + argument.hex() |
||||
|
||||
addr += int(m.group(1)) |
||||
|
||||
|
||||
instruction_list.append(instruction) |
||||
|
||||
addr += 1 |
||||
|
||||
return instruction_list |
||||
|
||||
|
||||
def assemble(instruction_list): |
||||
|
||||
bytecode = b"" |
||||
|
||||
for instruction in instruction_list: |
||||
|
||||
try: |
||||
opcode = get_opcode_from_name(instruction['opcode']) |
||||
except RuntimeError: |
||||
opcode = 0xbb |
||||
|
||||
bytecode += opcode.to_bytes(1, byteorder='big') |
||||
|
||||
if 'argument' in instruction: |
||||
|
||||
bytecode += util.safe_decode(instruction['argument']) |
||||
|
||||
return bytecode |
||||
@ -1,71 +0,0 @@ |
||||
from mythril.disassembler.disassembly import Disassembly |
||||
from ethereum import utils |
||||
import persistent |
||||
import re |
||||
|
||||
|
||||
class ETHContract(persistent.Persistent): |
||||
|
||||
def __init__(self, code, creation_code="", name="Unknown", enable_online_lookup=True): |
||||
|
||||
# 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 |
||||
|
||||
creation_code = re.sub(r'(_{2}.{38})', 'aa' * 20, creation_code) |
||||
code = re.sub(r'(_{2}.{38})', 'aa' * 20, code) |
||||
|
||||
self.creation_code = creation_code |
||||
self.name = name |
||||
self.code = code |
||||
self.disassembly = Disassembly(code, enable_online_lookup=enable_online_lookup) |
||||
self.creation_disassembly = Disassembly(creation_code, enable_online_lookup=enable_online_lookup) |
||||
|
||||
def as_dict(self): |
||||
|
||||
return { |
||||
'address': self.address, |
||||
'name': self.name, |
||||
'code': self.code, |
||||
'creation_code': self.creation_code, |
||||
'disassembly': self.disassembly |
||||
} |
||||
|
||||
def get_easm(self): |
||||
|
||||
return self.disassembly.get_easm() |
||||
|
||||
def matches_expression(self, expression): |
||||
|
||||
str_eval = '' |
||||
easm_code = None |
||||
|
||||
tokens = re.split("\s+(and|or|not)\s+", expression, re.IGNORECASE) |
||||
|
||||
for token in tokens: |
||||
|
||||
if token in ("and", "or", "not"): |
||||
str_eval += " " + token + " " |
||||
continue |
||||
|
||||
m = re.match(r'^code#([a-zA-Z0-9\s,\[\]]+)#', token) |
||||
|
||||
if m: |
||||
if easm_code is None: |
||||
easm_code = self.get_easm() |
||||
|
||||
code = m.group(1).replace(",", "\\n") |
||||
str_eval += "\"" + code + "\" in easm_code" |
||||
continue |
||||
|
||||
m = re.match(r'^func#([a-zA-Z0-9\s_,(\\)\[\]]+)#$', token) |
||||
|
||||
if m: |
||||
|
||||
sign_hash = "0x" + utils.sha3(m.group(1))[:4].hex() |
||||
|
||||
str_eval += "\"" + sign_hash + "\" in self.disassembly.func_hashes" |
||||
|
||||
continue |
||||
|
||||
return eval(str_eval.strip()) |
||||
@ -1,75 +0,0 @@ |
||||
from ethereum import vm, messages, transactions |
||||
from ethereum.state import State |
||||
from ethereum.slogging import get_logger |
||||
from mythril.ether import util |
||||
from logging import StreamHandler |
||||
from io import StringIO |
||||
import re |
||||
|
||||
|
||||
def trace(code, calldata = ""): |
||||
|
||||
log_handlers = ['eth.vm.op', 'eth.vm.op.stack', 'eth.vm.op.memory', 'eth.vm.op.storage'] |
||||
|
||||
output = StringIO() |
||||
stream_handler = StreamHandler(output) |
||||
|
||||
for handler in log_handlers: |
||||
log_vm_op = get_logger(handler) |
||||
log_vm_op.setLevel("TRACE") |
||||
log_vm_op.addHandler(stream_handler) |
||||
|
||||
addr = bytes.fromhex('0123456789ABCDEF0123456789ABCDEF01234567') |
||||
|
||||
state = State() |
||||
|
||||
ext = messages.VMExt(state, transactions.Transaction(0, 0, 21000, addr, 0, addr)) |
||||
|
||||
message = vm.Message(addr, addr, 0, 21000, calldata) |
||||
|
||||
res, gas, dat = vm.vm_execute(ext, message, util.safe_decode(code)) |
||||
|
||||
stream_handler.flush() |
||||
|
||||
ret = output.getvalue() |
||||
|
||||
lines = ret.split("\n") |
||||
|
||||
trace = [] |
||||
|
||||
for line in lines: |
||||
|
||||
m = re.search(r'pc=b\'(\d+)\'.*op=([A-Z0-9]+)', line) |
||||
|
||||
if m: |
||||
pc = m.group(1) |
||||
op = m.group(2) |
||||
|
||||
m = re.match(r'.*stack=(\[.*?\])', line) |
||||
|
||||
if m: |
||||
|
||||
stackitems = re.findall(r'b\'(\d+)\'', m.group(1)) |
||||
|
||||
stack = "[" |
||||
|
||||
if len(stackitems): |
||||
|
||||
for i in range(0, len(stackitems) - 1): |
||||
stack += hex(int(stackitems[i])) + ", " |
||||
|
||||
stack += hex(int(stackitems[-1])) |
||||
|
||||
stack += "]" |
||||
|
||||
else: |
||||
stack = "[]" |
||||
|
||||
if re.match(r'^PUSH.*', op): |
||||
val = re.search(r'pushvalue=(\d+)', line).group(1) |
||||
pushvalue = hex(int(val)) |
||||
trace.append({'pc': pc, 'op': op, 'stack': stack, 'pushvalue': pushvalue}) |
||||
else: |
||||
trace.append({'pc': pc, 'op': op, 'stack': stack}) |
||||
|
||||
return trace |
||||
@ -1,125 +0,0 @@ |
||||
import mythril.laser.ethereum.util as helper |
||||
from mythril.ether.ethcontract import ETHContract |
||||
from mythril.ether.util import get_solc_json |
||||
from mythril.exceptions import NoContractFoundError |
||||
|
||||
|
||||
class SourceMapping: |
||||
|
||||
def __init__(self, solidity_file_idx, offset, length, lineno): |
||||
self.solidity_file_idx = solidity_file_idx |
||||
self.offset = offset |
||||
self.length = length |
||||
self.lineno = lineno |
||||
|
||||
|
||||
class SolidityFile: |
||||
|
||||
def __init__(self, filename, data): |
||||
self.filename = filename |
||||
self.data = data |
||||
|
||||
|
||||
class SourceCodeInfo: |
||||
|
||||
def __init__(self, filename, lineno, code): |
||||
self.filename = filename |
||||
self.lineno = lineno |
||||
self.code = code |
||||
|
||||
|
||||
def get_contracts_from_file(input_file, solc_args=None): |
||||
data = get_solc_json(input_file, solc_args=solc_args) |
||||
for key, contract in data['contracts'].items(): |
||||
filename, name = key.split(":") |
||||
if filename == input_file and len(contract['bin-runtime']): |
||||
yield SolidityContract(input_file, name, solc_args) |
||||
|
||||
|
||||
class SolidityContract(ETHContract): |
||||
|
||||
def __init__(self, input_file, name=None, solc_args=None): |
||||
|
||||
data = get_solc_json(input_file, solc_args=solc_args) |
||||
|
||||
self.solidity_files = [] |
||||
|
||||
for filename in data['sourceList']: |
||||
with open(filename, 'r', encoding='utf-8') as file: |
||||
code = file.read() |
||||
self.solidity_files.append(SolidityFile(filename, code)) |
||||
|
||||
has_contract = False |
||||
|
||||
# If a contract name has been specified, find the bytecode of that specific contract |
||||
srcmap_constructor = [] |
||||
srcmap = [] |
||||
if name: |
||||
for key, contract in sorted(data['contracts'].items()): |
||||
filename, _name = key.split(":") |
||||
|
||||
if filename == input_file and name == _name and len(contract['bin-runtime']): |
||||
code = contract['bin-runtime'] |
||||
creation_code = contract['bin'] |
||||
srcmap = contract['srcmap-runtime'].split(";") |
||||
srcmap_constructor = contract['srcmap'].split(";") |
||||
has_contract = True |
||||
break |
||||
|
||||
# If no contract name is specified, get the last bytecode entry for the input file |
||||
|
||||
else: |
||||
for key, contract in sorted(data['contracts'].items()): |
||||
filename, name = key.split(":") |
||||
|
||||
if filename == input_file and len(contract['bin-runtime']): |
||||
code = contract['bin-runtime'] |
||||
creation_code = contract['bin'] |
||||
srcmap = contract['srcmap-runtime'].split(";") |
||||
srcmap_constructor = contract['srcmap'].split(";") |
||||
has_contract = True |
||||
|
||||
if not has_contract: |
||||
raise NoContractFoundError |
||||
|
||||
self.mappings = [] |
||||
|
||||
self.constructor_mappings = [] |
||||
|
||||
self._get_solc_mappings(srcmap) |
||||
self._get_solc_mappings(srcmap_constructor, constructor=True) |
||||
|
||||
super().__init__(code, creation_code, name=name) |
||||
|
||||
def get_source_info(self, address, constructor=False): |
||||
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) |
||||
solidity_file = self.solidity_files[mappings[index].solidity_file_idx] |
||||
|
||||
filename = solidity_file.filename |
||||
|
||||
offset = mappings[index].offset |
||||
length = mappings[index].length |
||||
|
||||
code = solidity_file.data.encode('utf-8')[offset:offset + length].decode('utf-8', errors="ignore") |
||||
lineno = mappings[index].lineno |
||||
|
||||
return SourceCodeInfo(filename, lineno, code) |
||||
|
||||
def _get_solc_mappings(self, srcmap, constructor=False): |
||||
mappings = self.constructor_mappings if constructor else self.mappings |
||||
for item in srcmap: |
||||
mapping = item.split(":") |
||||
|
||||
if len(mapping) > 0 and len(mapping[0]) > 0: |
||||
offset = int(mapping[0]) |
||||
|
||||
if len(mapping) > 1 and len(mapping[1]) > 0: |
||||
length = int(mapping[1]) |
||||
|
||||
if len(mapping) > 2 and len(mapping[2]) > 0: |
||||
idx = int(mapping[2]) |
||||
lineno = self.solidity_files[idx].data.encode('utf-8')[0:offset].count('\n'.encode('utf-8')) + 1 |
||||
|
||||
mappings.append(SourceMapping(idx, offset, length, lineno)) |
||||
@ -0,0 +1,139 @@ |
||||
"""This module contains the class representing EVM contracts, aka Smart |
||||
Contracts.""" |
||||
import re |
||||
import _pysha3 as sha3 |
||||
import logging |
||||
|
||||
log = logging.getLogger(__name__) |
||||
|
||||
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 |
||||
|
||||
: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) |
||||
|
||||
self.creation_code = creation_code |
||||
self.name = name |
||||
self.code = code |
||||
self.disassembly = Disassembly(code, enable_online_lookup=enable_online_lookup) |
||||
self.creation_disassembly = Disassembly( |
||||
creation_code, enable_online_lookup=enable_online_lookup |
||||
) |
||||
|
||||
@property |
||||
def bytecode_hash(self): |
||||
""" |
||||
|
||||
:return: runtime bytecode hash |
||||
""" |
||||
return self._get_hash(self.code[2:]) |
||||
|
||||
@property |
||||
def creation_bytecode_hash(self): |
||||
""" |
||||
|
||||
:return: Creation bytecode hash |
||||
""" |
||||
return self._get_hash(self.creation_code[2:]) |
||||
|
||||
@staticmethod |
||||
def _get_hash(code): |
||||
""" |
||||
:param code: bytecode |
||||
:return: Returns hash of the given bytecode |
||||
""" |
||||
try: |
||||
keccak = sha3.keccak_256() |
||||
keccak.update(bytes.fromhex(code[2:])) |
||||
return "0x" + keccak.hexdigest() |
||||
except ValueError: |
||||
log.debug( |
||||
"Unable to change the bytecode to bytes. Bytecode: {}".format(code) |
||||
) |
||||
return "" |
||||
|
||||
def as_dict(self): |
||||
""" |
||||
|
||||
:return: |
||||
""" |
||||
return { |
||||
"name": self.name, |
||||
"code": self.code, |
||||
"creation_code": self.creation_code, |
||||
"disassembly": self.disassembly, |
||||
} |
||||
|
||||
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 |
||||
|
||||
tokens = re.split("\s+(and|or|not)\s+", expression, re.IGNORECASE) |
||||
|
||||
for token in tokens: |
||||
|
||||
if token in ("and", "or", "not"): |
||||
str_eval += " " + token + " " |
||||
continue |
||||
|
||||
m = re.match(r"^code#([a-zA-Z0-9\s,\[\]]+)#", token) |
||||
|
||||
if m: |
||||
if easm_code is None: |
||||
easm_code = self.get_easm() |
||||
|
||||
code = m.group(1).replace(",", "\\n") |
||||
str_eval += '"' + code + '" in easm_code' |
||||
continue |
||||
|
||||
m = re.match(r"^func#([a-zA-Z0-9\s_,(\\)\[\]]+)#$", token) |
||||
|
||||
if m: |
||||
|
||||
sign_hash = "0x" + utils.sha3(m.group(1))[:4].hex() |
||||
|
||||
str_eval += '"' + sign_hash + '" in self.disassembly.func_hashes' |
||||
|
||||
continue |
||||
|
||||
return eval(str_eval.strip()) |
||||
@ -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,8 +1,6 @@ |
||||
BLOCK_TAG_EARLIEST = 'earliest' |
||||
BLOCK_TAG_LATEST = 'latest' |
||||
BLOCK_TAG_PENDING = 'pending' |
||||
BLOCK_TAGS = ( |
||||
BLOCK_TAG_EARLIEST, |
||||
BLOCK_TAG_LATEST, |
||||
BLOCK_TAG_PENDING, |
||||
) |
||||
"""This file contains constants used used by the Ethereum JSON RPC |
||||
interface.""" |
||||
BLOCK_TAG_EARLIEST = "earliest" |
||||
BLOCK_TAG_LATEST = "latest" |
||||
BLOCK_TAG_PENDING = "pending" |
||||
BLOCK_TAGS = (BLOCK_TAG_EARLIEST, BLOCK_TAG_LATEST, BLOCK_TAG_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,38 +1,54 @@ |
||||
"""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. |
||||
|
||||
:param d: |
||||
:return: |
||||
""" |
||||
Convert decimal to hex and remove the "L" suffix that is appended to large |
||||
numbers |
||||
""" |
||||
return hex(d).rstrip('L') |
||||
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') |
||||
raise ValueError("invalid block tag") |
||||
if isinstance(block, int): |
||||
block = hex(block) |
||||
return block |
||||
|
||||
|
||||
def wei_to_ether(wei): |
||||
"""Convert wei to ether. |
||||
|
||||
:param wei: |
||||
:return: |
||||
""" |
||||
Convert wei to ether |
||||
""" |
||||
return 1.0 * wei / 10**18 |
||||
return 1.0 * wei / 10 ** 18 |
||||
|
||||
|
||||
def ether_to_wei(ether): |
||||
"""Convert ether to wei. |
||||
|
||||
:param ether: |
||||
:return: |
||||
""" |
||||
Convert ether to wei |
||||
""" |
||||
return ether * 10**18 |
||||
return ether * 10 ** 18 |
||||
|
||||
@ -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 |
||||
|
||||
@ -0,0 +1,288 @@ |
||||
"""Don't ask.""" |
||||
#!/usr/bin/env python |
||||
# |
||||
# "THE BEER-WARE LICENSE" (Revision 43~maze) |
||||
# |
||||
# <maze@pyth0n.org> wrote these files. As long as you retain this notice you |
||||
# can do whatever you want with this stuff. If we meet some day, and you think |
||||
# this stuff is worth it, you can buy me a beer in return. |
||||
|
||||
# https://github.com/tehmaze/lolcat |
||||
|
||||
import atexit |
||||
import math |
||||
import os |
||||
import random |
||||
import re |
||||
import sys |
||||
import time |
||||
|
||||
PY3 = sys.version_info >= (3,) |
||||
|
||||
# Reset terminal colors at exit |
||||
def reset(): |
||||
"""""" |
||||
sys.stdout.write("\x1b[0m") |
||||
sys.stdout.flush() |
||||
|
||||
|
||||
atexit.register(reset) |
||||
|
||||
|
||||
STRIP_ANSI = re.compile(r"\x1b\[(\d+)(;\d+)?(;\d+)?[m|K]") |
||||
COLOR_ANSI = ( |
||||
(0x00, 0x00, 0x00), |
||||
(0xCD, 0x00, 0x00), |
||||
(0x00, 0xCD, 0x00), |
||||
(0xCD, 0xCD, 0x00), |
||||
(0x00, 0x00, 0xEE), |
||||
(0xCD, 0x00, 0xCD), |
||||
(0x00, 0xCD, 0xCD), |
||||
(0xE5, 0xE5, 0xE5), |
||||
(0x7F, 0x7F, 0x7F), |
||||
(0xFF, 0x00, 0x00), |
||||
(0x00, 0xFF, 0x00), |
||||
(0xFF, 0xFF, 0x00), |
||||
(0x5C, 0x5C, 0xFF), |
||||
(0xFF, 0x00, 0xFF), |
||||
(0x00, 0xFF, 0xFF), |
||||
(0xFF, 0xFF, 0xFF), |
||||
) |
||||
|
||||
|
||||
class LolCat(object): |
||||
"""Cats lel.""" |
||||
|
||||
def __init__(self, mode=256, output=sys.stdout): |
||||
self.mode = mode |
||||
self.output = output |
||||
|
||||
def _distance(self, rgb1, rgb2): |
||||
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): |
||||
colors = COLOR_ANSI[: self.mode] |
||||
matches = [ |
||||
(self._distance(c, map(int, rgb)), i) for i, c in enumerate(colors) |
||||
] |
||||
matches.sort() |
||||
color = matches[0][1] |
||||
|
||||
return "3%d" % (color,) |
||||
else: |
||||
gray_possible = True |
||||
sep = 2.5 |
||||
|
||||
while gray_possible: |
||||
if r < sep or g < sep or b < sep: |
||||
gray = r < sep and g < sep and b < sep |
||||
gray_possible = False |
||||
|
||||
sep += 42.5 |
||||
|
||||
if gray: |
||||
color = 232 + int(float(sum(rgb) / 33.0)) |
||||
else: |
||||
color = sum( |
||||
[16] |
||||
+ [ |
||||
int(6 * float(val) / 256) * mod |
||||
for val, mod in zip(rgb, [36, 6, 1]) |
||||
] |
||||
) |
||||
|
||||
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") |
||||
|
||||
for line in fd: |
||||
options.os += 1 |
||||
self.println(line, options) |
||||
|
||||
if options.animate: |
||||
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) |
||||
|
||||
if options.animate: |
||||
self.println_ani(s, options) |
||||
else: |
||||
self.println_plain(s, options) |
||||
|
||||
self.output.write("\n") |
||||
self.output.flush() |
||||
|
||||
def println_ani(self, s, options): |
||||
""" |
||||
|
||||
:param s: |
||||
:param options: |
||||
:return: |
||||
""" |
||||
if not s: |
||||
return |
||||
|
||||
for i in range(1, options.duration): |
||||
self.output.write("\x1b[%dD" % (len(s),)) |
||||
self.output.flush() |
||||
options.os += options.spread |
||||
self.println_plain(s, options) |
||||
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( |
||||
"".join( |
||||
[ |
||||
self.wrap(self.ansi(rgb)), |
||||
c if PY3 else c.encode(options.charset_py2, "replace"), |
||||
] |
||||
) |
||||
) |
||||
|
||||
|
||||
def detect_mode(term_hint="xterm-256color"): |
||||
"""Poor-mans color mode detection.""" |
||||
if "ANSICON" in os.environ: |
||||
return 16 |
||||
elif os.environ.get("ConEmuANSI", "OFF") == "ON": |
||||
return 256 |
||||
else: |
||||
term = os.environ.get("TERM", term_hint) |
||||
if term.endswith("-256color") or term in ("xterm", "screen"): |
||||
return 256 |
||||
elif term.endswith("-color") or term in ("rxvt",): |
||||
return 16 |
||||
else: |
||||
return 256 # optimistic default |
||||
|
||||
|
||||
def run(): |
||||
"""Main entry point.""" |
||||
import optparse |
||||
|
||||
parser = optparse.OptionParser(usage=r"%prog [<options>] [file ...]") |
||||
parser.add_option( |
||||
"-p", "--spread", type="float", default=3.0, help="Rainbow spread" |
||||
) |
||||
parser.add_option( |
||||
"-F", "--freq", type="float", default=0.1, help="Rainbow frequency" |
||||
) |
||||
parser.add_option("-S", "--seed", type="int", default=0, help="Rainbow seed") |
||||
parser.add_option( |
||||
"-a", |
||||
"--animate", |
||||
action="store_true", |
||||
default=False, |
||||
help="Enable psychedelics", |
||||
) |
||||
parser.add_option( |
||||
"-d", "--duration", type="int", default=12, help="Animation duration" |
||||
) |
||||
parser.add_option( |
||||
"-s", "--speed", type="float", default=20.0, help="Animation speed" |
||||
) |
||||
parser.add_option( |
||||
"-f", |
||||
"--force", |
||||
action="store_true", |
||||
default=False, |
||||
help="Force colour even when stdout is not a tty", |
||||
) |
||||
|
||||
parser.add_option( |
||||
"-3", action="store_const", dest="mode", const=8, help="Force 3 bit colour mode" |
||||
) |
||||
parser.add_option( |
||||
"-4", |
||||
action="store_const", |
||||
dest="mode", |
||||
const=16, |
||||
help="Force 4 bit colour mode", |
||||
) |
||||
parser.add_option( |
||||
"-8", |
||||
action="store_const", |
||||
dest="mode", |
||||
const=256, |
||||
help="Force 8 bit colour mode", |
||||
) |
||||
|
||||
parser.add_option( |
||||
"-c", |
||||
"--charset-py2", |
||||
default="utf-8", |
||||
help="Manually set a charset to convert from, for python 2.7", |
||||
) |
||||
|
||||
options, args = parser.parse_args() |
||||
options.os = random.randint(0, 256) if options.seed == 0 else options.seed |
||||
options.mode = options.mode or detect_mode() |
||||
|
||||
lolcat = LolCat(mode=options.mode) |
||||
|
||||
if not args: |
||||
args = ["-"] |
||||
|
||||
for filename in args: |
||||
if filename == "-": |
||||
lolcat.cat(sys.stdin, options) |
||||
else: |
||||
try: |
||||
with open(filename, "r") as handle: |
||||
lolcat.cat(handle, options) |
||||
except IOError as error: |
||||
sys.stderr.write(str(error) + "\n") |
||||
|
||||
|
||||
if __name__ == "__main__": |
||||
sys.exit(run()) |
||||
@ -1,18 +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 |
||||
|
||||
@ -0,0 +1,188 @@ |
||||
"""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": |
||||
gas_value = opcodes.GECRECOVER |
||||
elif contract == "sha256": |
||||
gas_value = opcodes.GSHA256BASE + word_num * opcodes.GSHA256WORD |
||||
elif contract == "ripemd160": |
||||
gas_value = opcodes.GRIPEMD160BASE + word_num * opcodes.GRIPEMD160WORD |
||||
elif contract == "identity": |
||||
gas_value = opcodes.GIDENTITYBASE + word_num * opcodes.GIDENTITYWORD |
||||
else: |
||||
raise ValueError("Unknown contract type {}".format(contract)) |
||||
return gas_value, gas_value |
||||
|
||||
|
||||
def calculate_sha3_gas(length: int): |
||||
""" |
||||
|
||||
:param length: |
||||
:return: |
||||
""" |
||||
gas_val = 30 + opcodes.GSHA3WORD * (ceil32(length) // 32) |
||||
return gas_val, gas_val |
||||
|
||||
|
||||
# opcode -> (min_gas, max_gas) |
||||
OPCODE_GAS = { |
||||
"STOP": (0, 0), |
||||
"ADD": (3, 3), |
||||
"MUL": (5, 5), |
||||
"SUB": (3, 3), |
||||
"DIV": (5, 5), |
||||
"SDIV": (5, 5), |
||||
"MOD": (5, 5), |
||||
"SMOD": (5, 5), |
||||
"ADDMOD": (8, 8), |
||||
"MULMOD": (8, 8), |
||||
"EXP": (10, 340), # exponent max 2^32 |
||||
"SIGNEXTEND": (5, 5), |
||||
"LT": (3, 3), |
||||
"GT": (3, 3), |
||||
"SLT": (3, 3), |
||||
"SGT": (3, 3), |
||||
"EQ": (3, 3), |
||||
"ISZERO": (3, 3), |
||||
"AND": (3, 3), |
||||
"OR": (3, 3), |
||||
"XOR": (3, 3), |
||||
"NOT": (3, 3), |
||||
"BYTE": (3, 3), |
||||
"SHA3": ( |
||||
30, |
||||
30 + 6 * 8, |
||||
), # max can be larger, but usually storage location with 8 words |
||||
"SHA3_FUNC": calculate_sha3_gas, |
||||
"ADDRESS": (2, 2), |
||||
"BALANCE": (400, 400), |
||||
"ORIGIN": (2, 2), |
||||
"CALLER": (2, 2), |
||||
"CALLVALUE": (2, 2), |
||||
"CALLDATALOAD": (3, 3), |
||||
"CALLDATASIZE": (2, 2), |
||||
"CALLDATACOPY": (2, 2 + 3 * 768), # https://ethereum.stackexchange.com/a/47556 |
||||
"CODESIZE": (2, 2), |
||||
"CODECOPY": (2, 2 + 3 * 768), # https://ethereum.stackexchange.com/a/47556, |
||||
"GASPRICE": (2, 2), |
||||
"EXTCODESIZE": (700, 700), |
||||
"EXTCODECOPY": (700, 700 + 3 * 768), # https://ethereum.stackexchange.com/a/47556 |
||||
"RETURNDATASIZE": (2, 2), |
||||
"RETURNDATACOPY": (3, 3), |
||||
"BLOCKHASH": (20, 20), |
||||
"COINBASE": (2, 2), |
||||
"TIMESTAMP": (2, 2), |
||||
"NUMBER": (2, 2), |
||||
"DIFFICULTY": (2, 2), |
||||
"GASLIMIT": (2, 2), |
||||
"POP": (2, 2), |
||||
# assume 1KB memory r/w cost as upper bound |
||||
"MLOAD": (3, 96), |
||||
"MSTORE": (3, 98), |
||||
"MSTORE8": (3, 98), |
||||
# assume 64 byte r/w cost as upper bound |
||||
"SLOAD": (400, 400), |
||||
"SSTORE": (5000, 25000), |
||||
"JUMP": (8, 8), |
||||
"JUMPI": (10, 10), |
||||
"PC": (2, 2), |
||||
"MSIZE": (2, 2), |
||||
"GAS": (2, 2), |
||||
"JUMPDEST": (1, 1), |
||||
"PUSH1": (3, 3), |
||||
"PUSH2": (3, 3), |
||||
"PUSH3": (3, 3), |
||||
"PUSH4": (3, 3), |
||||
"PUSH5": (3, 3), |
||||
"PUSH6": (3, 3), |
||||
"PUSH7": (3, 3), |
||||
"PUSH8": (3, 3), |
||||
"PUSH9": (3, 3), |
||||
"PUSH10": (3, 3), |
||||
"PUSH11": (3, 3), |
||||
"PUSH12": (3, 3), |
||||
"PUSH13": (3, 3), |
||||
"PUSH14": (3, 3), |
||||
"PUSH15": (3, 3), |
||||
"PUSH16": (3, 3), |
||||
"PUSH17": (3, 3), |
||||
"PUSH18": (3, 3), |
||||
"PUSH19": (3, 3), |
||||
"PUSH20": (3, 3), |
||||
"PUSH21": (3, 3), |
||||
"PUSH22": (3, 3), |
||||
"PUSH23": (3, 3), |
||||
"PUSH24": (3, 3), |
||||
"PUSH25": (3, 3), |
||||
"PUSH26": (3, 3), |
||||
"PUSH27": (3, 3), |
||||
"PUSH28": (3, 3), |
||||
"PUSH29": (3, 3), |
||||
"PUSH30": (3, 3), |
||||
"PUSH31": (3, 3), |
||||
"PUSH32": (3, 3), |
||||
"DUP1": (3, 3), |
||||
"DUP2": (3, 3), |
||||
"DUP3": (3, 3), |
||||
"DUP4": (3, 3), |
||||
"DUP5": (3, 3), |
||||
"DUP6": (3, 3), |
||||
"DUP7": (3, 3), |
||||
"DUP8": (3, 3), |
||||
"DUP9": (3, 3), |
||||
"DUP10": (3, 3), |
||||
"DUP11": (3, 3), |
||||
"DUP12": (3, 3), |
||||
"DUP13": (3, 3), |
||||
"DUP14": (3, 3), |
||||
"DUP15": (3, 3), |
||||
"DUP16": (3, 3), |
||||
"SWAP1": (3, 3), |
||||
"SWAP2": (3, 3), |
||||
"SWAP3": (3, 3), |
||||
"SWAP4": (3, 3), |
||||
"SWAP5": (3, 3), |
||||
"SWAP6": (3, 3), |
||||
"SWAP7": (3, 3), |
||||
"SWAP8": (3, 3), |
||||
"SWAP9": (3, 3), |
||||
"SWAP10": (3, 3), |
||||
"SWAP11": (3, 3), |
||||
"SWAP12": (3, 3), |
||||
"SWAP13": (3, 3), |
||||
"SWAP14": (3, 3), |
||||
"SWAP15": (3, 3), |
||||
"SWAP16": (3, 3), |
||||
# apparently Solidity only allows byte32 as input to the log |
||||
# function. Virtually it could be as large as the block gas limit |
||||
# allows, but let's stick to the reasonable standard here. |
||||
# https://ethereum.stackexchange.com/a/1691 |
||||
"LOG0": (375, 375 + 8 * 32), |
||||
"LOG1": (2 * 375, 2 * 375 + 8 * 32), |
||||
"LOG2": (3 * 375, 3 * 375 + 8 * 32), |
||||
"LOG3": (4 * 375, 4 * 375 + 8 * 32), |
||||
"LOG4": (5 * 375, 5 * 375 + 8 * 32), |
||||
"CREATE": (32000, 32000), |
||||
"CALL": (700, 700 + 9000 + 25000), |
||||
"NATIVE_COST": calculate_native_gas, |
||||
"CALLCODE": (700, 700 + 9000 + 25000), |
||||
"RETURN": (0, 0), |
||||
"DELEGATECALL": (700, 700 + 9000 + 25000), |
||||
"STATICCALL": (700, 700 + 9000 + 25000), |
||||
"REVERT": (0, 0), |
||||
"SUICIDE": (5000, 30000), |
||||
"ASSERT_FAIL": (0, 0), |
||||
"INVALID": (0, 0), |
||||
} |
||||
File diff suppressed because it is too large
Load Diff
@ -0,0 +1,79 @@ |
||||
from collections import namedtuple |
||||
from datetime import datetime |
||||
from typing import Dict, List, Tuple |
||||
|
||||
# Type annotations: |
||||
# start_time: datetime |
||||
# end_time: datetime |
||||
_InstrExecRecord = namedtuple("_InstrExecRecord", ["start_time", "end_time"]) |
||||
|
||||
# Type annotations: |
||||
# total_time: float |
||||
# total_nr: float |
||||
# min_time: float |
||||
# max_time: float |
||||
_InstrExecStatistic = namedtuple( |
||||
"_InstrExecStatistic", ["total_time", "total_nr", "min_time", "max_time"] |
||||
) |
||||
|
||||
# Map the instruction opcode to its records if all execution times |
||||
_InstrExecRecords = Dict[str, List[_InstrExecRecord]] |
||||
|
||||
# Map the instruction opcode to the statistic of its execution times |
||||
_InstrExecStatistics = Dict[str, _InstrExecStatistic] |
||||
|
||||
|
||||
class InstructionProfiler: |
||||
"""Performance profile for the execution of each instruction. |
||||
""" |
||||
|
||||
def __init__(self): |
||||
self.records = dict() |
||||
|
||||
def record(self, op: int, start_time: datetime, end_time: datetime): |
||||
try: |
||||
self.records[op].append(_InstrExecRecord(start_time, end_time)) |
||||
except KeyError: |
||||
self.records[op] = [_InstrExecRecord(start_time, end_time)] |
||||
|
||||
def _make_stats(self) -> Tuple[float, _InstrExecStatistics]: |
||||
periods = { |
||||
op: list( |
||||
map(lambda r: r.end_time.timestamp() - r.start_time.timestamp(), rs) |
||||
) |
||||
for op, rs in self.records.items() |
||||
} |
||||
|
||||
stats = dict() |
||||
total_time = 0 |
||||
|
||||
for _, (op, times) in enumerate(periods.items()): |
||||
stat = _InstrExecStatistic( |
||||
total_time=sum(times), |
||||
total_nr=len(times), |
||||
min_time=min(times), |
||||
max_time=max(times), |
||||
) |
||||
total_time += stat.total_time |
||||
stats[op] = stat |
||||
|
||||
return total_time, stats |
||||
|
||||
def __str__(self): |
||||
total, stats = self._make_stats() |
||||
|
||||
s = "Total: {} s\n".format(total) |
||||
|
||||
for op in sorted(stats): |
||||
stat = stats[op] |
||||
s += "[{:12s}] {:>8.4f} %, nr {:>6}, total {:>8.4f} s, avg {:>8.4f} s, min {:>8.4f} s, max {:>8.4f} s\n".format( |
||||
op, |
||||
stat.total_time * 100 / total, |
||||
stat.total_nr, |
||||
stat.total_time, |
||||
stat.total_time / stat.total_nr, |
||||
stat.min_time, |
||||
stat.max_time, |
||||
) |
||||
|
||||
return s |
||||
@ -1,18 +1,38 @@ |
||||
from z3 import ExprRef, BitVecRef |
||||
"""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: BitVecRef) -> bool: |
||||
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) -> ExprRef: |
||||
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: ExprRef, argument: ExprRef) -> None: |
||||
def add_keccak(self, expression: Expression, argument: Expression) -> None: |
||||
""" |
||||
|
||||
:param expression: |
||||
:param argument: |
||||
""" |
||||
index = str(expression) |
||||
self.keccak_expression_mapping[index] = (expression, argument) |
||||
|
||||
@ -1,355 +0,0 @@ |
||||
from z3 import BitVec, BitVecVal, BitVecRef, BitVecNumRef, Solver, ExprRef, sat |
||||
from mythril.disassembler.disassembly import Disassembly |
||||
from mythril.laser.ethereum.cfg import Node |
||||
from copy import copy, deepcopy |
||||
from enum import Enum |
||||
from random import randint |
||||
from typing import KeysView, Dict, List, Union, Any |
||||
from mythril.laser.ethereum.evm_exceptions import StackOverflowException, StackUnderflowException |
||||
|
||||
|
||||
class CalldataType(Enum): |
||||
CONCRETE = 1 |
||||
SYMBOLIC = 2 |
||||
|
||||
|
||||
class Storage: |
||||
""" |
||||
Storage class represents the storage of an Account |
||||
""" |
||||
def __init__(self, concrete=False, address=None, dynamic_loader=None): |
||||
""" |
||||
Constructor for Storage |
||||
:param concrete: bool indicating whether to interpret uninitialized storage as concrete versus symbolic |
||||
""" |
||||
self._storage = {} |
||||
self.concrete = concrete |
||||
self.dynld = dynamic_loader |
||||
self.address = address |
||||
|
||||
def __getitem__(self, item: int) -> int: |
||||
try: |
||||
return self._storage[item] |
||||
except KeyError: |
||||
if self.address and int(self.address[2:], 16) != 0 and self.dynld: |
||||
try: |
||||
self._storage[item] = int(self.dynld.read_storage(contract_address=self.address, index=int(item)), 16) |
||||
return self._storage[item] |
||||
except ValueError: |
||||
pass |
||||
if self.concrete: |
||||
return 0 |
||||
self._storage[item] = BitVec("storage_" + str(item), 256) |
||||
return self._storage[item] |
||||
|
||||
def __setitem__(self, key: str, value: BitVecRef) -> None: |
||||
self._storage[key] = value |
||||
|
||||
def keys(self) -> KeysView: |
||||
return self._storage.keys() |
||||
|
||||
|
||||
class Account: |
||||
""" |
||||
Account class representing ethereum accounts |
||||
""" |
||||
def __init__(self, address: str, code=None, contract_name="unknown", balance=None, concrete_storage=False, |
||||
dynamic_loader=None): |
||||
""" |
||||
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 |
||||
:param balance: The balance for the account |
||||
:param concrete_storage: Interpret storage as concrete |
||||
""" |
||||
self.nonce = 0 |
||||
self.code = code or Disassembly("") |
||||
self.balance = balance if balance else BitVec("balance", 256) |
||||
self.storage = Storage(concrete_storage, address=address, dynamic_loader=dynamic_loader) |
||||
|
||||
# Metadata |
||||
self.address = address |
||||
self.contract_name = contract_name |
||||
|
||||
self.deleted = False |
||||
|
||||
def __str__(self) -> str: |
||||
return str(self.as_dict) |
||||
|
||||
def set_balance(self, balance: BitVecRef) -> None: |
||||
self.balance = balance |
||||
|
||||
def add_balance(self, balance: BitVecRef) -> None: |
||||
self.balance += balance |
||||
|
||||
@property |
||||
def as_dict(self) -> Dict: |
||||
return {'nonce': self.nonce, 'code': self.code, 'balance': self.balance, 'storage': self.storage} |
||||
|
||||
|
||||
class Environment: |
||||
""" |
||||
The environment class represents the current execution environment for the symbolic executor |
||||
""" |
||||
def __init__( |
||||
self, |
||||
active_account: Account, |
||||
sender: BitVecRef, |
||||
calldata: List, |
||||
gasprice: BitVecRef, |
||||
callvalue: BitVecRef, |
||||
origin: BitVecRef, |
||||
code=None, |
||||
calldata_type=CalldataType.SYMBOLIC, |
||||
): |
||||
# Metadata |
||||
|
||||
self.active_account = active_account |
||||
self.active_function_name = "" |
||||
|
||||
self.address = BitVecVal(int(active_account.address, 16), 256) |
||||
|
||||
# Ib |
||||
self.code = active_account.code if code is None else code |
||||
|
||||
self.sender = sender |
||||
self.calldata = calldata |
||||
self.calldata_type = calldata_type |
||||
self.gasprice = gasprice |
||||
self.origin = origin |
||||
self.callvalue = callvalue |
||||
|
||||
def __str__(self) -> str: |
||||
return str(self.as_dict) |
||||
|
||||
@property |
||||
def as_dict(self) -> Dict: |
||||
return dict(active_account=self.active_account, sender=self.sender, calldata=self.calldata, |
||||
gasprice=self.gasprice, callvalue=self.callvalue, origin=self.origin, |
||||
calldata_type=self.calldata_type) |
||||
|
||||
|
||||
class MachineStack(list): |
||||
""" |
||||
Defines EVM stack, overrides the default list to handle overflows |
||||
""" |
||||
STACK_LIMIT = 1024 |
||||
|
||||
def __init__(self, default_list=None): |
||||
if default_list is None: |
||||
default_list = [] |
||||
super(MachineStack, self).__init__(default_list) |
||||
|
||||
def append(self, element: BitVecNumRef) -> None: |
||||
""" |
||||
:param element: element to be appended to the list |
||||
:function: appends the element to list if the size is less than STACK_LIMIT, else throws an error |
||||
""" |
||||
if super(MachineStack, self).__len__() >= self.STACK_LIMIT: |
||||
raise StackOverflowException("Reached the EVM stack limit of {}, you can't append more " |
||||
"elements".format(self.STACK_LIMIT)) |
||||
super(MachineStack, self).append(element) |
||||
|
||||
def pop(self, index=-1) -> BitVecNumRef: |
||||
""" |
||||
:param index:index to be popped, same as the list() class. |
||||
:returns popped value |
||||
:function: same as list() class but throws StackUnderflowException for popping from an empty list |
||||
""" |
||||
|
||||
try: |
||||
return super(MachineStack, self).pop(index) |
||||
except IndexError: |
||||
raise StackUnderflowException("Trying to pop from an empty stack") |
||||
|
||||
def __getitem__(self, item: int) -> Any: |
||||
try: |
||||
return super(MachineStack, self).__getitem__(item) |
||||
except IndexError: |
||||
raise StackUnderflowException("Trying to access a stack element which doesn't exist") |
||||
|
||||
def __add__(self, other): |
||||
""" |
||||
Implement list concatenation if needed |
||||
""" |
||||
raise NotImplementedError('Implement this if needed') |
||||
|
||||
def __iadd__(self, other): |
||||
""" |
||||
Implement list concatenation if needed |
||||
""" |
||||
raise NotImplementedError('Implement this if needed') |
||||
|
||||
|
||||
class MachineState: |
||||
""" |
||||
MachineState represents current machine state also referenced to as \mu |
||||
""" |
||||
def __init__(self, gas: int): |
||||
""" Constructor for machineState """ |
||||
self.pc = 0 |
||||
self.stack = MachineStack() |
||||
self.memory = [] |
||||
self.gas = gas |
||||
self.constraints = [] |
||||
self.depth = 0 |
||||
|
||||
def mem_extend(self, start: int, size: int) -> None: |
||||
""" |
||||
Extends the memory of this machine state |
||||
:param start: Start of memory extension |
||||
:param size: Size of memory extension |
||||
""" |
||||
if self.memory_size > start + size: |
||||
return |
||||
m_extend = (start + size - self.memory_size) |
||||
self.memory.extend(bytearray(m_extend)) |
||||
|
||||
def memory_write(self, offset: int, data: List[int]) -> None: |
||||
""" Writes data to memory starting at offset """ |
||||
self.mem_extend(offset, len(data)) |
||||
self.memory[offset:offset+len(data)] = data |
||||
|
||||
def pop(self, amount=1) -> Union[BitVecRef, List[BitVecRef]]: |
||||
""" Pops amount elements from the stack""" |
||||
if amount >= len(self.stack): |
||||
raise StackUnderflowException |
||||
values = self.stack[-amount:][::-1] |
||||
del self.stack[-amount:] |
||||
|
||||
return values[0] if amount == 1 else values |
||||
|
||||
def __str__(self) -> str: |
||||
return str(self.as_dict) |
||||
|
||||
@property |
||||
def memory_size(self) -> int: |
||||
return len(self.memory) |
||||
|
||||
@property |
||||
def as_dict(self) -> Dict: |
||||
return dict(pc=self.pc, stack=self.stack, memory=self.memory, memsize=self.memory_size, gas=self.gas) |
||||
|
||||
|
||||
class GlobalState: |
||||
""" |
||||
GlobalState represents the current globalstate |
||||
""" |
||||
def __init__( |
||||
self, |
||||
world_state: "WorldState", |
||||
environment: Environment, |
||||
node: Node, |
||||
machine_state=None, |
||||
transaction_stack=None, |
||||
last_return_data=None |
||||
): |
||||
""" Constructor for GlobalState""" |
||||
self.node = node |
||||
self.world_state = world_state |
||||
self.environment = environment |
||||
self.mstate = machine_state if machine_state else MachineState(gas=10000000) |
||||
self.transaction_stack = transaction_stack if transaction_stack else [] |
||||
self.op_code = "" |
||||
self.last_return_data = last_return_data |
||||
|
||||
def __copy__(self) -> "GlobalState": |
||||
world_state = copy(self.world_state) |
||||
environment = copy(self.environment) |
||||
mstate = deepcopy(self.mstate) |
||||
transaction_stack = copy(self.transaction_stack) |
||||
return GlobalState(world_state, environment, self.node, mstate, transaction_stack=transaction_stack, |
||||
last_return_data=self.last_return_data) |
||||
|
||||
@property |
||||
def accounts(self) -> Dict: |
||||
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""" |
||||
|
||||
instructions = self.environment.code.instruction_list |
||||
return instructions[self.mstate.pc] |
||||
|
||||
@property |
||||
def current_transaction(self) -> Union["MessageCallTransaction", "ContractCreationTransaction", None]: |
||||
# TODO: Remove circular to transaction package to import Transaction classes |
||||
try: |
||||
return self.transaction_stack[-1][0] |
||||
except IndexError: |
||||
return None |
||||
|
||||
@property |
||||
def instruction(self) -> Dict: |
||||
return self.get_current_instruction() |
||||
|
||||
def new_bitvec(self, name: str, size=256) -> BitVec: |
||||
transaction_id = self.current_transaction.id |
||||
node_id = self.node.uid |
||||
return BitVec("{}_{}".format(transaction_id, name), size) |
||||
|
||||
|
||||
class WorldState: |
||||
""" |
||||
The WorldState class represents the world state as described in the yellow paper |
||||
""" |
||||
def __init__(self, transaction_sequence=None): |
||||
""" |
||||
Constructor for the world state. Initializes the accounts record |
||||
""" |
||||
self.accounts = {} |
||||
self.node = None |
||||
self.transaction_sequence = transaction_sequence or [] |
||||
|
||||
def __getitem__(self, item: str) -> Account: |
||||
""" |
||||
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": |
||||
new_world_state = WorldState(transaction_sequence=self.transaction_sequence[:]) |
||||
new_world_state.accounts = copy(self.accounts) |
||||
new_world_state.node = self.node |
||||
return new_world_state |
||||
|
||||
def create_account(self, balance=0, address=None, concrete_storage=False, dynamic_loader=None) -> 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 |
||||
:param dynamic_loader: used for dynamically loading storage from the block chain |
||||
:return: The new account |
||||
""" |
||||
address = address if address else self._generate_new_address() |
||||
new_account = Account(address, balance=balance, dynamic_loader=dynamic_loader, concrete_storage=concrete_storage) |
||||
self._put_account(new_account) |
||||
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 |
||||
:param contract_code: Runtime bytecode for the contract |
||||
:param storage: Initial storage for the contract |
||||
:return: The new account |
||||
""" |
||||
# TODO: Add type hints |
||||
new_account = Account(self._generate_new_address(), code=contract_code, balance=0) |
||||
new_account.storage = storage |
||||
self._put_account(new_account) |
||||
|
||||
def _generate_new_address(self) -> str: |
||||
""" Generates a new address for the global state""" |
||||
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: |
||||
self.accounts[account.address] = account |
||||
@ -0,0 +1 @@ |
||||
# Hello! |
||||
@ -0,0 +1,130 @@ |
||||
"""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.disassembler.disassembly import Disassembly |
||||
from mythril.laser.smt import symbol_factory |
||||
|
||||
|
||||
class Storage: |
||||
"""Storage class represents the storage of an Account.""" |
||||
|
||||
def __init__(self, concrete=False, address=None, dynamic_loader=None): |
||||
"""Constructor for Storage. |
||||
|
||||
:param concrete: bool indicating whether to interpret uninitialized storage as concrete versus symbolic |
||||
""" |
||||
self._storage = {} |
||||
self.concrete = concrete |
||||
self.dynld = dynamic_loader |
||||
self.address = address |
||||
|
||||
def __getitem__(self, item: Union[int, slice]) -> Any: |
||||
try: |
||||
return self._storage[item] |
||||
except KeyError: |
||||
if ( |
||||
self.address |
||||
and int(self.address[2:], 16) != 0 |
||||
and (self.dynld and self.dynld.storage_loading) |
||||
): |
||||
try: |
||||
self._storage[item] = symbol_factory.BitVecVal( |
||||
int( |
||||
self.dynld.read_storage( |
||||
contract_address=self.address, index=int(item) |
||||
), |
||||
16, |
||||
), |
||||
256, |
||||
) |
||||
return self._storage[item] |
||||
except ValueError: |
||||
pass |
||||
if self.concrete: |
||||
return symbol_factory.BitVecVal(0, 256) |
||||
self._storage[item] = symbol_factory.BitVecVal(0, 256) |
||||
return self._storage[item] |
||||
|
||||
def __setitem__(self, key: str, value: ExprRef) -> None: |
||||
self._storage[key] = value |
||||
|
||||
def keys(self) -> KeysView: |
||||
""" |
||||
|
||||
:return: |
||||
""" |
||||
return self._storage.keys() |
||||
|
||||
|
||||
class Account: |
||||
"""Account class representing ethereum accounts.""" |
||||
|
||||
def __init__( |
||||
self, |
||||
address: str, |
||||
code=None, |
||||
contract_name="unknown", |
||||
balance=None, |
||||
concrete_storage=False, |
||||
dynamic_loader=None, |
||||
): |
||||
"""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 |
||||
:param balance: The balance for the account |
||||
:param concrete_storage: Interpret storage as concrete |
||||
""" |
||||
self.nonce = 0 |
||||
self.code = code or Disassembly("") |
||||
self.balance = ( |
||||
balance |
||||
if balance |
||||
else symbol_factory.BitVecSym("{}_balance".format(address), 256) |
||||
) |
||||
self.storage = Storage( |
||||
concrete_storage, address=address, dynamic_loader=dynamic_loader |
||||
) |
||||
|
||||
# Metadata |
||||
self.address = address |
||||
self.contract_name = contract_name |
||||
|
||||
self.deleted = False |
||||
|
||||
def __str__(self) -> str: |
||||
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, |
||||
"balance": self.balance, |
||||
"storage": self.storage, |
||||
} |
||||
@ -0,0 +1,40 @@ |
||||
"""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. |
||||
""" |
||||
|
||||
@property |
||||
def persist_to_world_state(self) -> bool: |
||||
"""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. |
||||
|
||||
The default is set to False |
||||
""" |
||||
return False |
||||
|
||||
|
||||
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 |
||||
""" |
||||
|
||||
def __copy__(self): |
||||
return self |
||||
|
||||
def __deepcopy__(self, _): |
||||
return self |
||||
@ -0,0 +1,307 @@ |
||||
"""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 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.""" |
||||
|
||||
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 |
||||
if isinstance(result, int): |
||||
return symbol_factory.BitVecVal(result, 256) |
||||
return result |
||||
|
||||
def get_word_at(self, offset: int) -> Expression: |
||||
"""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) |
||||
|
||||
if isinstance(item, slice): |
||||
start = 0 if item.start is None else item.start |
||||
step = 1 if item.step is None else item.step |
||||
stop = self.size if item.stop is None else item.stop |
||||
|
||||
try: |
||||
current_index = ( |
||||
start |
||||
if isinstance(start, Expression) |
||||
else symbol_factory.BitVecVal(start, 256) |
||||
) |
||||
parts = [] |
||||
while simplify(current_index != stop): |
||||
element = self._load(current_index) |
||||
if not isinstance(element, Expression): |
||||
element = symbol_factory.BitVecVal(element, 8) |
||||
|
||||
parts.append(element) |
||||
current_index = simplify(current_index + step) |
||||
except Z3Exception: |
||||
raise IndexError("Invalid Calldata Slice") |
||||
|
||||
return parts |
||||
|
||||
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. |
||||
|
||||
:return: unnormalized call data size |
||||
""" |
||||
raise NotImplementedError() |
||||
|
||||
def concrete(self, model: Model) -> list: |
||||
"""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. |
||||
|
||||
:param tx_id: Id of the transaction that the calldata is for. |
||||
:param calldata: The concrete calldata content |
||||
""" |
||||
self._concrete_calldata = calldata |
||||
self._calldata = K(256, 8, 0) |
||||
for i, element in enumerate(calldata, 0): |
||||
element = ( |
||||
symbol_factory.BitVecVal(element, 8) |
||||
if isinstance(element, int) |
||||
else element |
||||
) |
||||
self._calldata[symbol_factory.BitVecVal(i, 256)] = element |
||||
|
||||
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. |
||||
|
||||
:param tx_id: Id of the transaction that the calldata is for. |
||||
:param calldata: The concrete calldata content |
||||
""" |
||||
self._calldata = calldata |
||||
super().__init__(tx_id) |
||||
|
||||
def _load(self, item: Union[int, Expression]) -> Any: |
||||
""" |
||||
|
||||
:param item: |
||||
:return: |
||||
""" |
||||
if isinstance(item, int): |
||||
try: |
||||
return self._calldata[item] |
||||
except IndexError: |
||||
return 0 |
||||
|
||||
value = symbol_factory.BitVecVal(0x0, 8) |
||||
for i in range(self.size): |
||||
value = If(item == i, self._calldata[i], value) |
||||
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. |
||||
|
||||
:param tx_id: Id of the transaction that the calldata is for. |
||||
""" |
||||
self._size = symbol_factory.BitVecSym(str(tx_id) + "_calldatasize", 256) |
||||
self._calldata = Array("{}_calldata".format(tx_id), 256, 8) |
||||
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( |
||||
item < self._size, |
||||
simplify(self._calldata[item]), |
||||
symbol_factory.BitVecVal(0, 8), |
||||
) |
||||
) |
||||
|
||||
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): |
||||
value = self._load(i) |
||||
c_value = model.eval(value.raw, model_completion=True).as_long() |
||||
result.append(c_value) |
||||
|
||||
return result |
||||
|
||||
@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. |
||||
|
||||
:param tx_id: Id of the transaction that the calldata is for. |
||||
""" |
||||
self._reads = [] |
||||
self._size = BitVec(str(tx_id) + "_calldatasize", 256) |
||||
super().__init__(tx_id) |
||||
|
||||
def _load(self, item: Union[int, Expression], clean=False) -> Any: |
||||
x = symbol_factory.BitVecVal(item, 256) if isinstance(item, int) else item |
||||
|
||||
symbolic_base_value = If( |
||||
x >= self._size, |
||||
symbol_factory.BitVecVal(0, 8), |
||||
BitVec("{}_calldata_{}".format(self.tx_id, str(item)), 8), |
||||
) |
||||
return_value = symbolic_base_value |
||||
for r_index, r_value in self._reads: |
||||
return_value = If(r_index == item, r_value, return_value) |
||||
|
||||
if not clean: |
||||
self._reads.append((item, symbolic_base_value)) |
||||
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): |
||||
value = self._load(i, clean=True) |
||||
c_value = get_concrete_int(model.eval(value, model_completion=True)) |
||||
result.append(c_value) |
||||
|
||||
return result |
||||
|
||||
@property |
||||
def size(self) -> Expression: |
||||
""" |
||||
|
||||
:return: |
||||
""" |
||||
return self._size |
||||
@ -0,0 +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. |
||||
|
||||
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 |
||||
@ -0,0 +1,73 @@ |
||||
"""This module contains the representation for an execution state's |
||||
environment.""" |
||||
from typing import Dict |
||||
|
||||
from z3 import ExprRef |
||||
|
||||
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.""" |
||||
|
||||
def __init__( |
||||
self, |
||||
active_account: Account, |
||||
sender: ExprRef, |
||||
calldata: BaseCalldata, |
||||
gasprice: ExprRef, |
||||
callvalue: ExprRef, |
||||
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 |
||||
self.active_function_name = "" |
||||
|
||||
self.address = symbol_factory.BitVecVal(int(active_account.address, 16), 256) |
||||
|
||||
# Ib |
||||
self.code = active_account.code if code is None else code |
||||
|
||||
self.sender = sender |
||||
self.calldata = calldata |
||||
self.gasprice = gasprice |
||||
self.origin = origin |
||||
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, |
||||
calldata=self.calldata, |
||||
gasprice=self.gasprice, |
||||
callvalue=self.callvalue, |
||||
origin=self.origin, |
||||
) |
||||
@ -0,0 +1,143 @@ |
||||
"""This module contains a representation of the global execution state.""" |
||||
from typing import Dict, Union, List, Iterable |
||||
|
||||
from copy import copy, deepcopy |
||||
from z3 import BitVec |
||||
|
||||
from mythril.laser.smt import symbol_factory |
||||
from mythril.laser.ethereum.cfg import Node |
||||
from mythril.laser.ethereum.state.environment import Environment |
||||
from mythril.laser.ethereum.state.machine_state import MachineState |
||||
from mythril.laser.ethereum.state.annotation import StateAnnotation |
||||
|
||||
|
||||
class GlobalState: |
||||
"""GlobalState represents the current globalstate.""" |
||||
|
||||
def __init__( |
||||
self, |
||||
world_state: "WorldState", |
||||
environment: Environment, |
||||
node: Node, |
||||
machine_state=None, |
||||
transaction_stack=None, |
||||
last_return_data=None, |
||||
annotations=None, |
||||
): |
||||
"""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 |
||||
self.mstate = ( |
||||
machine_state if machine_state else MachineState(gas_limit=1000000000) |
||||
) |
||||
self.transaction_stack = transaction_stack if transaction_stack else [] |
||||
self.op_code = "" |
||||
self.last_return_data = last_return_data |
||||
self._annotations = annotations or [] |
||||
|
||||
def __copy__(self) -> "GlobalState": |
||||
""" |
||||
|
||||
:return: |
||||
""" |
||||
world_state = copy(self.world_state) |
||||
environment = copy(self.environment) |
||||
mstate = deepcopy(self.mstate) |
||||
transaction_stack = copy(self.transaction_stack) |
||||
return GlobalState( |
||||
world_state, |
||||
environment, |
||||
self.node, |
||||
mstate, |
||||
transaction_stack=transaction_stack, |
||||
last_return_data=self.last_return_data, |
||||
annotations=[copy(a) for a in self._annotations], |
||||
) |
||||
|
||||
@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. |
||||
|
||||
:return: |
||||
""" |
||||
|
||||
instructions = self.environment.code.instruction_list |
||||
return instructions[self.mstate.pc] |
||||
|
||||
@property |
||||
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] |
||||
except IndexError: |
||||
return None |
||||
|
||||
@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: |
||||
self.world_state.annotate(annotation) |
||||
|
||||
@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) |
||||
|
||||
:param annotation_type: The type to filter annotations for |
||||
:return: filter of matching annotations |
||||
""" |
||||
return filter(lambda x: isinstance(x, annotation_type), self.annotations) |
||||
@ -0,0 +1,236 @@ |
||||
"""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 |
||||
|
||||
from z3 import BitVec |
||||
|
||||
from ethereum import opcodes, utils |
||||
from mythril.laser.ethereum.evm_exceptions import ( |
||||
StackOverflowException, |
||||
StackUnderflowException, |
||||
OutOfGasException, |
||||
) |
||||
from mythril.laser.ethereum.state.constraints import Constraints |
||||
from mythril.laser.ethereum.state.memory import Memory |
||||
|
||||
|
||||
class MachineStack(list): |
||||
"""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) |
||||
|
||||
def append(self, element: BitVec) -> None: |
||||
""" |
||||
:param element: element to be appended to the list |
||||
:function: appends the element to list if the size is less than STACK_LIMIT, else throws an error |
||||
""" |
||||
if super(MachineStack, self).__len__() >= self.STACK_LIMIT: |
||||
raise StackOverflowException( |
||||
"Reached the EVM stack limit of {}, you can't append more " |
||||
"elements".format(self.STACK_LIMIT) |
||||
) |
||||
super(MachineStack, self).append(element) |
||||
|
||||
def pop(self, index=-1) -> BitVec: |
||||
""" |
||||
:param index:index to be popped, same as the list() class. |
||||
:returns popped value |
||||
:function: same as list() class but throws StackUnderflowException for popping from an empty list |
||||
""" |
||||
|
||||
try: |
||||
return super(MachineStack, self).pop(index) |
||||
except IndexError: |
||||
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: |
||||
raise StackUnderflowException( |
||||
"Trying to access a stack element which doesn't exist" |
||||
) |
||||
|
||||
def __add__(self, other): |
||||
"""Implement list concatenation if needed. |
||||
|
||||
:param other: |
||||
""" |
||||
raise NotImplementedError("Implement this if needed") |
||||
|
||||
def __iadd__(self, other): |
||||
"""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. |
||||
""" |
||||
|
||||
def __init__( |
||||
self, |
||||
gas_limit: int, |
||||
pc=0, |
||||
stack=None, |
||||
memory=None, |
||||
constraints=None, |
||||
depth=0, |
||||
max_gas_used=0, |
||||
min_gas_used=0, |
||||
): |
||||
"""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() |
||||
self.gas_limit = gas_limit |
||||
self.min_gas_used = min_gas_used # lower gas usage bound |
||||
self.max_gas_used = max_gas_used # upper gas usage bound |
||||
self.constraints = constraints or Constraints() |
||||
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 = ( |
||||
oldsize * opcodes.GMEMORY + oldsize ** 2 // opcodes.GQUADRATICMEMDENOM |
||||
) |
||||
newsize = utils.ceil32(start + size) // 32 |
||||
new_totalfee = ( |
||||
newsize * opcodes.GMEMORY + newsize ** 2 // opcodes.GQUADRATICMEMDENOM |
||||
) |
||||
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. |
||||
|
||||
:param start: Start of memory extension |
||||
:param size: Size of memory extension |
||||
""" |
||||
m_extend = self.calculate_extension_size(start, size) |
||||
if m_extend: |
||||
extend_gas = self.calculate_memory_gas(start, size) |
||||
self.min_gas_used += extend_gas |
||||
self.max_gas_used += extend_gas |
||||
self.check_gas() |
||||
self.memory.extend(m_extend) |
||||
|
||||
def memory_write(self, offset: int, data: List[int]) -> None: |
||||
"""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. |
||||
|
||||
:param amount: |
||||
:return: |
||||
""" |
||||
if amount > len(self.stack): |
||||
raise StackUnderflowException |
||||
values = self.stack[-amount:][::-1] |
||||
del self.stack[-amount:] |
||||
|
||||
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, |
||||
max_gas_used=self.max_gas_used, |
||||
min_gas_used=self.min_gas_used, |
||||
pc=self.pc, |
||||
stack=copy(self.stack), |
||||
memory=copy(self.memory), |
||||
constraints=copy(self.constraints), |
||||
depth=self.depth, |
||||
) |
||||
|
||||
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, |
||||
memory=self.memory, |
||||
memsize=self.memory_size, |
||||
gas=self.gas_limit, |
||||
max_gas_used=self.max_gas_used, |
||||
min_gas_used=self.min_gas_used, |
||||
) |
||||
@ -0,0 +1,142 @@ |
||||
"""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, |
||||
Bool, |
||||
Concat, |
||||
Extract, |
||||
If, |
||||
simplify, |
||||
symbol_factory, |
||||
) |
||||
|
||||
|
||||
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. |
||||
|
||||
:param index: integer representing the index to access |
||||
:return: 32 byte word at the specified index |
||||
""" |
||||
try: |
||||
return symbol_factory.BitVecVal( |
||||
util.concrete_int_from_bytes( |
||||
bytes([util.get_concrete_int(b) for b in self[index : index + 32]]), |
||||
0, |
||||
), |
||||
256, |
||||
) |
||||
except: |
||||
result = simplify( |
||||
Concat( |
||||
[ |
||||
b if isinstance(b, BitVec) else symbol_factory.BitVecVal(b, 8) |
||||
for b in self[index : index + 32] |
||||
] |
||||
) |
||||
) |
||||
assert result.size() == 256 |
||||
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` |
||||
|
||||
:param index: index to write to |
||||
:param value: the value to write to memory |
||||
""" |
||||
try: |
||||
# Attempt to concretize value |
||||
if isinstance(value, bool): |
||||
_bytes = ( |
||||
int(1).to_bytes(32, byteorder="big") |
||||
if value |
||||
else int(0).to_bytes(32, byteorder="big") |
||||
) |
||||
else: |
||||
_bytes = util.concrete_int_to_bytes(value) |
||||
assert len(_bytes) == 32 |
||||
self[index : index + 32] = _bytes |
||||
except (Z3Exception, AttributeError): # BitVector or BoolRef |
||||
if isinstance(value, Bool): |
||||
value_to_write = If( |
||||
value, |
||||
symbol_factory.BitVecVal(1, 256), |
||||
symbol_factory.BitVecVal(0, 256), |
||||
) |
||||
else: |
||||
value_to_write = value |
||||
assert value_to_write.size() == 256 |
||||
|
||||
for i in range(0, value_to_write.size(), 8): |
||||
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: |
||||
start = 0 |
||||
if stop is None: # 2**256 is just a bit too big |
||||
raise IndexError("Invalid Memory Slice") |
||||
if step is None: |
||||
step = 1 |
||||
return [self[i] for i in range(start, stop, step)] |
||||
|
||||
try: |
||||
return self._memory[item] |
||||
except IndexError: |
||||
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 |
||||
|
||||
if start is None: |
||||
start = 0 |
||||
if stop is None: |
||||
raise IndexError("Invalid Memory Slice") |
||||
if step is None: |
||||
step = 1 |
||||
|
||||
for i in range(0, stop - start, step): |
||||
self[start + i] = value[i] |
||||
|
||||
else: |
||||
if isinstance(value, int): |
||||
assert 0 <= value <= 0xFF |
||||
if isinstance(value, BitVec): |
||||
assert value.size() == 8 |
||||
self._memory[key] = value |
||||
@ -0,0 +1,126 @@ |
||||
"""This module contains a representation of the EVM's world state.""" |
||||
from copy import copy |
||||
from random import randint |
||||
from typing import List, Iterator |
||||
|
||||
from mythril.laser.ethereum.state.account import Account |
||||
from mythril.laser.ethereum.state.annotation import StateAnnotation |
||||
|
||||
|
||||
class WorldState: |
||||
"""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. |
||||
|
||||
:param transaction_sequence: |
||||
:param annotations: |
||||
""" |
||||
self.accounts = {} |
||||
self.node = None |
||||
self.transaction_sequence = transaction_sequence or [] |
||||
self._annotations = annotations or [] |
||||
|
||||
def __getitem__(self, item: str) -> Account: |
||||
"""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[:], |
||||
annotations=new_annotations, |
||||
) |
||||
new_world_state.accounts = copy(self.accounts) |
||||
new_world_state.node = self.node |
||||
return new_world_state |
||||
|
||||
def create_account( |
||||
self, balance=0, address=None, concrete_storage=False, dynamic_loader=None |
||||
) -> 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 |
||||
:param dynamic_loader: used for dynamically loading storage from the block chain |
||||
:return: The new account |
||||
""" |
||||
address = address if address else self._generate_new_address() |
||||
new_account = Account( |
||||
address, |
||||
balance=balance, |
||||
dynamic_loader=dynamic_loader, |
||||
concrete_storage=concrete_storage, |
||||
) |
||||
self._put_account(new_account) |
||||
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. |
||||
|
||||
:param contract_code: Runtime bytecode for the contract |
||||
:param storage: Initial storage for the contract |
||||
:return: The new account |
||||
""" |
||||
# TODO: Add type hints |
||||
new_account = Account( |
||||
self._generate_new_address(), code=contract_code, balance=0 |
||||
) |
||||
new_account.storage = storage |
||||
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) |
||||
|
||||
: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. |
||||
|
||||
: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 |
||||
@ -0,0 +1,28 @@ |
||||
from abc import ABC, abstractmethod |
||||
|
||||
|
||||
class BasicSearchStrategy(ABC): |
||||
"""""" |
||||
|
||||
__slots__ = "work_list", "max_depth" |
||||
|
||||
def __init__(self, work_list, max_depth): |
||||
self.work_list = work_list |
||||
self.max_depth = max_depth |
||||
|
||||
def __iter__(self): |
||||
return self |
||||
|
||||
@abstractmethod |
||||
def get_strategic_global_state(self): |
||||
"""""" |
||||
raise NotImplementedError("Must be implemented by a subclass") |
||||
|
||||
def __next__(self): |
||||
try: |
||||
global_state = self.get_strategic_global_state() |
||||
if global_state.mstate.depth >= self.max_depth: |
||||
return self.__next__() |
||||
return global_state |
||||
except IndexError: |
||||
raise StopIteration |
||||
Some files were not shown because too many files have changed in this diff Show More
Loading…
Reference in new issue