Merge pull request #1099 from ConsenSys/develop

Merge updates from develop
ether_thief_fix
Bernhard Mueller 5 years ago committed by GitHub
commit 1a3f4a4acb
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
  1. 60
      .circleci/config.yml
  2. 2
      Dockerfile
  3. 19
      Pipfile
  4. 6
      README.md
  5. 6
      docs/source/about.rst
  6. 2
      docs/source/analysis-modules.rst
  7. 28
      docs/source/conf.py
  8. 2
      docs/source/create-module.rst
  9. 2
      docs/source/index.rst
  10. 22
      docs/source/module-list.rst
  11. 2
      docs/source/security-analysis.rst
  12. 2
      mythril/__init__.py
  13. 2
      mythril/__version__.py
  14. 45
      mythril/analysis/modules/delegatecall.py
  15. 4
      mythril/analysis/modules/dos.py
  16. 6
      mythril/analysis/modules/ether_thief.py
  17. 5
      mythril/analysis/modules/exceptions.py
  18. 16
      mythril/analysis/modules/external_calls.py
  19. 201
      mythril/analysis/modules/integer.py
  20. 18
      mythril/analysis/modules/suicide.py
  21. 44
      mythril/analysis/report.py
  22. 142
      mythril/analysis/solver.py
  23. 66
      mythril/analysis/symbolic.py
  24. 4
      mythril/analysis/templates/report_as_markdown.jinja2
  25. 4
      mythril/analysis/templates/report_as_text.jinja2
  26. 582
      mythril/interfaces/cli.py
  27. 2
      mythril/laser/ethereum/call.py
  28. 143
      mythril/laser/ethereum/instructions.py
  29. 330
      mythril/laser/ethereum/plugins/implementations/dependency_pruner.py
  30. 9
      mythril/laser/ethereum/plugins/plugin_factory.py
  31. 10
      mythril/laser/ethereum/plugins/signals.py
  32. 6
      mythril/laser/ethereum/state/account.py
  33. 22
      mythril/laser/ethereum/state/world_state.py
  34. 0
      mythril/laser/ethereum/strategy/extensions/__init__.py
  35. 84
      mythril/laser/ethereum/strategy/extensions/bounded_loops.py
  36. 31
      mythril/laser/ethereum/svm.py
  37. 2
      mythril/laser/ethereum/transaction/concolic.py
  38. 15
      mythril/laser/ethereum/transaction/symbolic.py
  39. 36
      mythril/laser/ethereum/transaction/transaction_models.py
  40. 7
      mythril/laser/smt/bitvec.py
  41. 11
      mythril/mythril/mythril_analyzer.py
  42. 2
      requirements.txt
  43. 138
      setup.py
  44. 4
      tests/cli_tests/test_cli_opts.py
  45. 58
      tests/cmd_line_test.py
  46. 50
      tests/laser/state/world_state_account_exist_load_test.py
  47. 4
      tests/report_test.py
  48. 36
      tests/testdata/outputs_expected/calls.sol.o.json
  49. 27
      tests/testdata/outputs_expected/calls.sol.o.jsonv2
  50. 8
      tests/testdata/outputs_expected/ether_send.sol.o.json
  51. 6
      tests/testdata/outputs_expected/ether_send.sol.o.jsonv2
  52. 16
      tests/testdata/outputs_expected/exceptions.sol.o.json
  53. 12
      tests/testdata/outputs_expected/exceptions.sol.o.jsonv2
  54. 24
      tests/testdata/outputs_expected/kinds_of_calls.sol.o.json
  55. 18
      tests/testdata/outputs_expected/kinds_of_calls.sol.o.jsonv2
  56. 4
      tests/testdata/outputs_expected/multi_contracts.sol.o.json
  57. 3
      tests/testdata/outputs_expected/multi_contracts.sol.o.jsonv2
  58. 4
      tests/testdata/outputs_expected/origin.sol.o.json
  59. 3
      tests/testdata/outputs_expected/origin.sol.o.jsonv2
  60. 12
      tests/testdata/outputs_expected/overflow.sol.o.json
  61. 9
      tests/testdata/outputs_expected/overflow.sol.o.jsonv2
  62. 12
      tests/testdata/outputs_expected/returnvalue.sol.o.json
  63. 9
      tests/testdata/outputs_expected/returnvalue.sol.o.jsonv2
  64. 4
      tests/testdata/outputs_expected/suicide.sol.o.json
  65. 3
      tests/testdata/outputs_expected/suicide.sol.o.jsonv2
  66. 12
      tests/testdata/outputs_expected/underflow.sol.o.json
  67. 9
      tests/testdata/outputs_expected/underflow.sol.o.jsonv2

@ -78,44 +78,42 @@ jobs:
# command: if [ -z "$CIRCLE_PR_NUMBER" ]; then ./run-integration-tests.sh; fi # command: if [ -z "$CIRCLE_PR_NUMBER" ]; then ./run-integration-tests.sh; fi
# working_directory: /home # working_directory: /home
- run:
name: Call webhook
command: |
curl -I -X POST -H -d "https://circleci.com/api/v1/project/${ORGANIZATION}/${WEBHOOK_PROJECT}/tree/master?circle-token=${CIRCLE_TOKEN}" | head -n 1 | cut -d$' ' -f2
integration_tests: integration_tests:
docker: docker:
- image: mythril/mythx-ci - image: circleci/python:3.6.4
working_directory: /home working_directory: ~/project
steps: steps:
- checkout: - checkout
path: /home/mythril-classic - setup_remote_docker
- run: - run:
name: Builds `mythril-classic` name: Clone Edelweiss
command: cd mythril-classic && python3 setup.py install command: git clone --recurse-submodules https://$GITHUB_TOKEN@github.com/Consensys/Edelweiss.git
- run: - run:
name: Installs other MythX components name: Update SWC-registry
command: | working_directory: ~/project/Edelweiss
./install-mythx-components.sh pythx edelweiss harvey-cli \ command: git submodule update --recursive --remote
harvey-tyro maestro maru maru-tyro mythril-api \
mythril-tyro tyro
- run: - run:
background: true name: Build Edelweiss
name: Launches MythX platform command: |
command: ./launch-mythx.sh docker build \
- run: --build-arg AWS_ACCESS_KEY_ID=$S3_AWS_ACCESS_KEY_ID \
name: Waits for MythX to spin-up --build-arg AWS_SECRET_ACCESS_KEY=$S3_AWS_SECRET_ACCESS_KEY \
command: sleep 15s --build-arg AWS_DEFAULT_REGION=us-east-1 --rm -t "edelweiss-mythril:latest" . -f Edelweiss/dockerfiles/mythril/Dockerfile
- run: - run:
name: Quick Edelweiss test name: Run Edelweiss
command: /home/run-edelweiss-test.sh CircleCI/latest.quick.csv 5 command: |
docker run \
# TODO: Temporary disabled -e CIRCLE_BUILD_NUM=$CIRCLE_BUILD_NUM \
# - run: -e CIRCLE_BUILD_URL=$CIRCLE_BUILD_URL \
# name: Full Edelweiss test -e CIRCLE_WEBHOOK_URL=$CIRCLE_WEBHOOK_URL \
# environment: --rm edelweiss-mythril:latest \
# MYTHX_API_FULL_MODE: true --timeout 30 \
# command: /home/run-edelweiss-test.sh CircleCI/latest.full.csv --output-dir /opt/edelweiss \
--plugin-dir /opt/mythril \
--s3 \
--circle-ci CircleCI/mythril.csv \
--ignore-false-positives $IGNORE_FALSE_POSITIVES \
--ignore-regressions $IGNORE_REGRESSIONS
pypi_release: pypi_release:
<<: *defaults <<: *defaults

@ -39,8 +39,6 @@ COPY . /opt/mythril
RUN cd /opt/mythril \ RUN cd /opt/mythril \
&& python setup.py install && python setup.py install
RUN useradd -m mythril
USER mythril
WORKDIR /home/mythril WORKDIR /home/mythril
RUN ( [ ! -z "${SOLC}" ] && set -e && for ver in $SOLC; do python -m solc.install v${ver}; done ) || true RUN ( [ ! -z "${SOLC}" ] && set -e && for ver in $SOLC; do python -m solc.install v${ver}; done ) || true

@ -1,19 +0,0 @@
[[source]]
url = "https://pypi.python.org/simple"
verify_ssl = true
name = "pypi"
[packages]
"e1839a8" = {path = ".", editable = true}
[dev-packages]
pylint = "*"
yapf = "*"
pytest = "*"
pytest-mock = "*"
pytest-cov = "*"
[requires]
[pipenv]
allow_prereleases = true

@ -6,8 +6,8 @@
[![Discord](https://img.shields.io/discord/481002907366588416.svg)](https://discord.gg/E3YrVtG) [![Discord](https://img.shields.io/discord/481002907366588416.svg)](https://discord.gg/E3YrVtG)
[![PyPI](https://badge.fury.io/py/mythril.svg)](https://pypi.python.org/pypi/mythril) [![PyPI](https://badge.fury.io/py/mythril.svg)](https://pypi.python.org/pypi/mythril)
[![Read the Docs](https://readthedocs.org/projects/mythril/badge/?version=master)](https://mythril.readthedocs.io/en/master/) [![Read the Docs](https://readthedocs.org/projects/mythril-classic/badge/?version=master)](https://mythril-classic.readthedocs.io/en/master/)
![Master Build Status](https://img.shields.io/circleci/project/github/ConsenSys/mythril/master.svg) ![Master Build Status](https://img.shields.io/circleci/build/github/ConsenSys/mythril.svg?token=97124ecfaee54366859cae98b5dafc0714325f8b)
[![Sonarcloud - Maintainability](https://sonarcloud.io/api/project_badges/measure?project=mythril&metric=sqale_rating)](https://sonarcloud.io/dashboard?id=mythril) [![Sonarcloud - Maintainability](https://sonarcloud.io/api/project_badges/measure?project=mythril&metric=sqale_rating)](https://sonarcloud.io/dashboard?id=mythril)
[![Pypi Installs](https://pepy.tech/badge/mythril)](https://pepy.tech/project/mythril) [![Pypi Installs](https://pepy.tech/badge/mythril)](https://pepy.tech/project/mythril)
[![DockerHub Pulls](https://img.shields.io/docker/pulls/mythril/myth.svg?label=DockerHub&nbsp;Pulls)](https://cloud.docker.com/u/mythril/repository/docker/mythril/myth) [![DockerHub Pulls](https://img.shields.io/docker/pulls/mythril/myth.svg?label=DockerHub&nbsp;Pulls)](https://cloud.docker.com/u/mythril/repository/docker/mythril/myth)
@ -41,7 +41,7 @@ Instructions for using Mythril are found on the [Wiki](https://github.com/Consen
For support or general discussions please join the Mythril community on [Discord](https://discord.gg/E3YrVtG). For support or general discussions please join the Mythril community on [Discord](https://discord.gg/E3YrVtG).
## Bulding the Documentation ## Bulding the Documentation
Mythril's documentation is contained in the `docs` folder and is published to [Read the Docs](https://mythril.readthedocs.io/en/master/). It is based on Sphinx and can be built using the Makefile contained in the subdirectory: Mythril's documentation is contained in the `docs` folder and is published to [Read the Docs](https://mythril-classic.readthedocs.io/en/master/). It is based on Sphinx and can be built using the Makefile contained in the subdirectory:
``` ```
cd docs cd docs

@ -1,6 +1,6 @@
What is Mythril Classic? What is Mythril?
======================== ========================
Mythril Classic is a security analysis tool for Ethereum smart contracts. It was `introduced at HITBSecConf 2018 <https://github.com/b-mueller/smashing-smart-contracts/blob/master/smashing-smart-contracts-1of1.pdf>`_. Mythril is a security analysis tool for Ethereum smart contracts. It was `introduced at HITBSecConf 2018 <https://github.com/b-mueller/smashing-smart-contracts/blob/master/smashing-smart-contracts-1of1.pdf>`_.
Mythril Classic detects a range of security issues, including integer underflows, owner-overwrite-to-Ether-withdrawal, and others. Note that Mythril is targeted at finding common vulnerabilities, and is not able to discover issues in the business logic of an application. Furthermore, Mythril and symbolic executors are generally unsound, as they are often unable to explore all possible states of a program. Mythril detects a range of security issues, including integer underflows, owner-overwrite-to-Ether-withdrawal, and others. Note that Mythril is targeted at finding common vulnerabilities, and is not able to discover issues in the business logic of an application. Furthermore, Mythril and symbolic executors are generally unsound, as they are often unable to explore all possible states of a program.

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

@ -20,14 +20,14 @@ sys.path.insert(0, os.path.abspath("../../"))
# -- Project information ----------------------------------------------------- # -- Project information -----------------------------------------------------
project = "Mythril Classic" project = "Mythril"
copyright = "2018, Bernhard Mueller" copyright = "2019, ConsenSys Diligence"
author = "Bernhard Mueller" author = "ConsenSys Dilligence"
# The short X.Y version # The short X.Y version
version = "" version = ""
# The full version, including alpha/beta/rc tags # The full version, including alpha/beta/rc tags
from mythril.version import VERSION from mythril.__version__ import __version__ as VERSION
release = VERSION release = VERSION
@ -108,7 +108,7 @@ html_static_path = ["_static"]
# -- Options for HTMLHelp output --------------------------------------------- # -- Options for HTMLHelp output ---------------------------------------------
# Output file base name for HTML help builder. # Output file base name for HTML help builder.
htmlhelp_basename = "MythrilClassicdoc" htmlhelp_basename = "Mythrildoc"
# -- Options for LaTeX output ------------------------------------------------ # -- Options for LaTeX output ------------------------------------------------
@ -132,13 +132,7 @@ latex_elements = {
# (source start file, target name, title, # (source start file, target name, title,
# author, documentclass [howto, manual, or own class]). # author, documentclass [howto, manual, or own class]).
latex_documents = [ latex_documents = [
( (master_doc, "Mythril.tex", "Mythril Documentation", "Bernhard Mueller", "manual")
master_doc,
"MythrilClassic.tex",
"Mythril Classic Documentation",
"Bernhard Mueller",
"manual",
)
] ]
@ -146,9 +140,7 @@ latex_documents = [
# One entry per manual page. List of tuples # One entry per manual page. List of tuples
# (source start file, name, description, authors, manual section). # (source start file, name, description, authors, manual section).
man_pages = [ man_pages = [(master_doc, "mythril", "Mythril Documentation", [author], 1)]
(master_doc, "mythrilclassic", "Mythril Classic Documentation", [author], 1)
]
# -- Options for Texinfo output ---------------------------------------------- # -- Options for Texinfo output ----------------------------------------------
@ -159,10 +151,10 @@ man_pages = [
texinfo_documents = [ texinfo_documents = [
( (
master_doc, master_doc,
"MythrilClassic", "Mythril",
"Mythril Classic Documentation", "Mythril Documentation",
author, author,
"MythrilClassic", "Mythril",
"One line description of project.", "One line description of project.",
"Miscellaneous", "Miscellaneous",
) )

@ -1,4 +1,4 @@
Creating a Module Creating a Module
================= =================
Create a module in the :code:`analysis/modules` directory, and create an instance of a class that inherits :code:`DetectionModule` named :code:`detector`. Take a look at the `suicide module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/suicide.py>`_ as an example. Create a module in the :code:`analysis/modules` directory, and create an instance of a class that inherits :code:`DetectionModule` named :code:`detector`. Take a look at the `suicide module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/suicide.py>`_ as an example.

@ -1,4 +1,4 @@
Welcome to Mythril Classic's documentation! Welcome to Mythril's documentation!
=========================================== ===========================================
.. toctree:: .. toctree::

@ -5,65 +5,65 @@ Modules
Delegate Call To Untrusted Contract Delegate Call To Untrusted Contract
*********************************** ***********************************
The `delegatecall module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/delegatecall.py>`_ detects `SWC-112 (DELEGATECALL to Untrusted Callee) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-112>`_. The `delegatecall module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/delegatecall.py>`_ detects `SWC-112 (DELEGATECALL to Untrusted Callee) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-112>`_.
*********************************** ***********************************
Dependence on Predictable Variables Dependence on Predictable Variables
*********************************** ***********************************
The `predictable variables module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/dependence_on_predictable_vars.py>`_ detects `SWC-120 (Weak Randomness) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-120>`_ and `SWC-116 (Timestamp Dependence) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-116>`_. The `predictable variables module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/dependence_on_predictable_vars.py>`_ detects `SWC-120 (Weak Randomness) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-120>`_ and `SWC-116 (Timestamp Dependence) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-116>`_.
****************** ******************
Deprecated Opcodes Deprecated Opcodes
****************** ******************
The `deprecated opcodes module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/deprecated_ops.py>`_ detects `SWC-111 (Use of Deprecated Functions) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-111>`_. The `deprecated opcodes module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/deprecated_ops.py>`_ detects `SWC-111 (Use of Deprecated Functions) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-111>`_.
*********** ***********
Ether Thief Ether Thief
*********** ***********
The `Ether Thief module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/ether_thief.py>`_ detects `SWC-105 (Unprotected Ether Withdrawal) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-105>`_. The `Ether Thief module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/ether_thief.py>`_ detects `SWC-105 (Unprotected Ether Withdrawal) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-105>`_.
********** **********
Exceptions Exceptions
********** **********
The `exceptions module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/exceptions.py>`_ detects `SWC-110 (Assert Violation) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-110>`_. The `exceptions module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/exceptions.py>`_ detects `SWC-110 (Assert Violation) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-110>`_.
************** **************
External Calls External Calls
************** **************
The `external calls module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/external_calls.py>`_ warns about `SWC-117 (Reentrancy) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-107>`_ by detecting calls to external contracts. The `external calls module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/external_calls.py>`_ warns about `SWC-117 (Reentrancy) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-107>`_ by detecting calls to external contracts.
******* *******
Integer Integer
******* *******
The `integer module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/integer.py>`_ detects `SWC-101 (Integer Overflow and Underflow) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-101>`_. The `integer module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/integer.py>`_ detects `SWC-101 (Integer Overflow and Underflow) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-101>`_.
************** **************
Multiple Sends Multiple Sends
************** **************
The `multiple sends module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/multiple_sends.py>`_ detects `SWC-113 (Denial of Service with Failed Call) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-113>`_ by checking for multiple calls or sends in a single transaction. The `multiple sends module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/multiple_sends.py>`_ detects `SWC-113 (Denial of Service with Failed Call) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-113>`_ by checking for multiple calls or sends in a single transaction.
******* *******
Suicide Suicide
******* *******
The `suicide module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/suicide.py>`_ detects `SWC-106 (Unprotected SELFDESTRUCT) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-106>`_. The `suicide module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/suicide.py>`_ detects `SWC-106 (Unprotected SELFDESTRUCT) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-106>`_.
**************************** ****************************
State Change External Calls State Change External Calls
**************************** ****************************
The `state change external calls module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/state_change_external_calls.py>`_ detects `SWC-107 (Reentrancy) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-107>`_ by detecting state change after calls to an external contract. The `state change external calls module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/state_change_external_calls.py>`_ detects `SWC-107 (Reentrancy) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-107>`_ by detecting state change after calls to an external contract.
**************** ****************
Unchecked Retval Unchecked Retval
**************** ****************
The `unchecked retval module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/unchecked_retval.py>`_ detects `SWC-104 (Unchecked Call Return Value) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-104>`_. The `unchecked retval module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/unchecked_retval.py>`_ detects `SWC-104 (Unchecked Call Return Value) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-104>`_.

@ -1,7 +1,7 @@
Security Analysis Security Analysis
================= =================
Run :code:`myth -x` with one of the input options described below will run the analysis modules in the `/analysis/modules <https://github.com/ConsenSys/mythril-classic/tree/master/mythril/analysis/modules>`_ directory. Run :code:`myth -x` with one of the input options described below will run the analysis modules in the `/analysis/modules <https://github.com/ConsenSys/mythril/tree/master/mythril/analysis/modules>`_ directory.
*********************** ***********************
Analyzing Solidity Code Analyzing Solidity Code

@ -3,4 +3,4 @@
__docformat__ = "restructuredtext" __docformat__ = "restructuredtext"
# Accept mythril.VERSION to get mythril's current version number # Accept mythril.VERSION to get mythril's current version number
from .version import VERSION # NOQA from .__version__ import __version__ as VERSION # NOQA

@ -4,4 +4,4 @@ This file is suitable for sourcing inside POSIX shell, e.g. bash as well
as for importing into Python. as for importing into Python.
""" """
VERSION = "v0.20.7" # NOQA __version__ = "v0.21.3"

@ -2,10 +2,14 @@
import json import json
import logging import logging
from copy import copy from copy import copy
from typing import List, cast from typing import List, cast, Dict
from mythril.analysis import solver from mythril.analysis import solver
from mythril.analysis.swc_data import DELEGATECALL_TO_UNTRUSTED_CONTRACT from mythril.analysis.swc_data import DELEGATECALL_TO_UNTRUSTED_CONTRACT
from mythril.laser.ethereum.transaction.symbolic import ATTACKER_ADDRESS
from mythril.laser.ethereum.transaction.transaction_models import (
ContractCreationTransaction,
)
from mythril.analysis.report import Issue from mythril.analysis.report import Issue
from mythril.analysis.modules.base import DetectionModule from mythril.analysis.modules.base import DetectionModule
from mythril.exceptions import UnsatError from mythril.exceptions import UnsatError
@ -17,17 +21,21 @@ log = logging.getLogger(__name__)
class DelegateCallAnnotation(StateAnnotation): class DelegateCallAnnotation(StateAnnotation):
def __init__(self, call_state: GlobalState) -> None: def __init__(self, call_state: GlobalState, constraints: List) -> None:
""" """
Initialize DelegateCall Annotation Initialize DelegateCall Annotation
:param call_state: Call state :param call_state: Call state
""" """
self.call_state = call_state self.call_state = call_state
self.constraints = constraints
self.return_value = call_state.new_bitvec( self.return_value = call_state.new_bitvec(
"retval_{}".format(call_state.get_current_instruction()["address"]), 256 "retval_{}".format(call_state.get_current_instruction()["address"]), 256
) )
def get_issue(self, global_state: GlobalState, transaction_sequence: str) -> Issue: def _copy__(self):
return DelegateCallAnnotation(self.call_state, copy(self.constraints))
def get_issue(self, global_state: GlobalState, transaction_sequence: Dict) -> Issue:
""" """
Returns Issue for the annotation Returns Issue for the annotation
:param global_state: Global State :param global_state: Global State
@ -58,7 +66,7 @@ class DelegateCallAnnotation(StateAnnotation):
severity="Medium", severity="Medium",
description_head=description_head, description_head=description_head,
description_tail=description_tail, description_tail=description_tail,
debug=transaction_sequence, transaction_sequence=transaction_sequence,
gas_used=( gas_used=(
global_state.mstate.min_gas_used, global_state.mstate.min_gas_used,
global_state.mstate.max_gas_used, global_state.mstate.max_gas_used,
@ -107,29 +115,32 @@ def _analyze_states(state: GlobalState) -> List[Issue]:
gas = state.mstate.stack[-1] gas = state.mstate.stack[-1]
to = state.mstate.stack[-2] to = state.mstate.stack[-2]
constraints = copy(state.mstate.constraints) constraints = [
# Check whether we can also set the callee address to == ATTACKER_ADDRESS,
constraints += [
to == 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF,
UGT(gas, symbol_factory.BitVecVal(2300, 256)), UGT(gas, symbol_factory.BitVecVal(2300, 256)),
] ]
try:
solver.get_model(constraints)
state.annotate(DelegateCallAnnotation(call_state=state))
except UnsatError: for tx in state.world_state.transaction_sequence:
log.debug("[DELEGATECALL] Annotation skipped.") if not isinstance(tx, ContractCreationTransaction):
constraints.append(tx.caller == ATTACKER_ADDRESS)
state.annotate(DelegateCallAnnotation(state, constraints))
return [] return []
else: else:
for annotation in annotations: for annotation in annotations:
try: try:
transaction_sequence = solver.get_transaction_sequence( transaction_sequence = solver.get_transaction_sequence(
state, state.mstate.constraints + [annotation.return_value == 1] state,
state.mstate.constraints
+ annotation.constraints
+ [annotation.return_value == 1],
)
issues.append(
annotation.get_issue(
state, transaction_sequence=transaction_sequence
)
) )
debug = json.dumps(transaction_sequence, indent=4)
issues.append(annotation.get_issue(state, transaction_sequence=debug))
except UnsatError: except UnsatError:
continue continue

@ -44,8 +44,8 @@ class DOS(DetectionModule):
self._jumpdest_count = {} # type: Dict[object, dict] self._jumpdest_count = {} # type: Dict[object, dict]
def _execute(self, state: GlobalState) -> None: def _execute(self, state: GlobalState) -> None:
"""
"""
:param state: :param state:
:return: :return:
""" """
@ -70,7 +70,7 @@ class DOS(DetectionModule):
try: try:
self._jumpdest_count[transaction][target] += 1 self._jumpdest_count[transaction][target] += 1
if self._jumpdest_count[transaction][target] == 4: if self._jumpdest_count[transaction][target] == 3:
annotation = ( annotation = (
LoopAnnotation(address, target) LoopAnnotation(address, target)

@ -122,8 +122,6 @@ class EtherThief(DetectionModule):
transaction_sequence = solver.get_transaction_sequence(state, constraints) transaction_sequence = solver.get_transaction_sequence(state, constraints)
debug = json.dumps(transaction_sequence, indent=4)
issue = Issue( issue = Issue(
contract=state.environment.active_account.contract_name, contract=state.environment.active_account.contract_name,
function_name=state.environment.active_function_name, function_name=state.environment.active_function_name,
@ -136,14 +134,14 @@ class EtherThief(DetectionModule):
description_tail="Arbitrary senders other than the contract creator can withdraw ETH from the contract" 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" + " account without previously having sent an equivalent amount of ETH to it. This is likely to be"
+ " a vulnerability.", + " a vulnerability.",
debug=debug, transaction_sequence=transaction_sequence,
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
) )
except UnsatError: except UnsatError:
log.debug("[ETHER_THIEF] no model found") log.debug("[ETHER_THIEF] no model found")
return [] return []
self._cache_addresses[address] = True # self._cache_addresses[address] = True
return [issue] return [issue]

@ -18,8 +18,6 @@ def _analyze_state(state) -> list:
:param state: :param state:
:return: :return:
""" """
log.info("Exceptions module: found ASSERT_FAIL instruction")
log.debug("ASSERT_FAIL in function " + state.environment.active_function_name) log.debug("ASSERT_FAIL in function " + state.environment.active_function_name)
try: try:
@ -36,7 +34,6 @@ def _analyze_state(state) -> list:
transaction_sequence = solver.get_transaction_sequence( transaction_sequence = solver.get_transaction_sequence(
state, state.mstate.constraints state, state.mstate.constraints
) )
debug = json.dumps(transaction_sequence, indent=4)
issue = Issue( issue = Issue(
contract=state.environment.active_account.contract_name, contract=state.environment.active_account.contract_name,
@ -48,7 +45,7 @@ def _analyze_state(state) -> list:
description_head="A reachable exception has been detected.", description_head="A reachable exception has been detected.",
description_tail=description_tail, description_tail=description_tail,
bytecode=state.environment.code.bytecode, bytecode=state.environment.code.bytecode,
debug=debug, transaction_sequence=transaction_sequence,
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
) )
return [issue] return [issue]

@ -3,6 +3,10 @@ calls."""
from mythril.analysis import solver from mythril.analysis import solver
from mythril.analysis.swc_data import REENTRANCY from mythril.analysis.swc_data import REENTRANCY
from mythril.laser.ethereum.transaction.symbolic import ATTACKER_ADDRESS
from mythril.laser.ethereum.transaction.transaction_models import (
ContractCreationTransaction,
)
from mythril.analysis.modules.base import DetectionModule from mythril.analysis.modules.base import DetectionModule
from mythril.analysis.report import Issue from mythril.analysis.report import Issue
from mythril.laser.smt import UGT, symbol_factory, Or, BitVec from mythril.laser.smt import UGT, symbol_factory, Or, BitVec
@ -44,10 +48,14 @@ def _analyze_state(state):
# Check whether we can also set the callee address # Check whether we can also set the callee address
try: try:
constraints += [to == 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF] constraints += [to == ATTACKER_ADDRESS]
for tx in state.world_state.transaction_sequence:
if not isinstance(tx, ContractCreationTransaction):
constraints.append(tx.caller == ATTACKER_ADDRESS)
transaction_sequence = solver.get_transaction_sequence(state, constraints) 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_head = "A call to a user-supplied address is executed."
description_tail = ( description_tail = (
"The callee address of an external message call can be set by " "The callee address of an external message call can be set by "
@ -66,7 +74,7 @@ def _analyze_state(state):
severity="Medium", severity="Medium",
description_head=description_head, description_head=description_head,
description_tail=description_tail, description_tail=description_tail,
debug=debug, transaction_sequence=transaction_sequence,
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
) )
@ -95,7 +103,7 @@ def _analyze_state(state):
severity="Low", severity="Low",
description_head=description_head, description_head=description_head,
description_tail=description_tail, description_tail=description_tail,
debug=debug, transaction_sequence=transaction_sequence,
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
) )

@ -4,7 +4,7 @@ underflows."""
import json import json
from math import log2, ceil from math import log2, ceil
from typing import Dict, cast, List from typing import cast, List, Dict, Set
from mythril.analysis import solver from mythril.analysis import solver
from mythril.analysis.report import Issue from mythril.analysis.report import Issue
from mythril.analysis.swc_data import INTEGER_OVERFLOW_AND_UNDERFLOW from mythril.analysis.swc_data import INTEGER_OVERFLOW_AND_UNDERFLOW
@ -13,6 +13,7 @@ from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.laser.ethereum.util import get_concrete_int from mythril.laser.ethereum.util import get_concrete_int
from mythril.laser.ethereum.state.annotation import StateAnnotation from mythril.laser.ethereum.state.annotation import StateAnnotation
from mythril.analysis.modules.base import DetectionModule from mythril.analysis.modules.base import DetectionModule
from copy import copy
from mythril.laser.smt import ( from mythril.laser.smt import (
BVAddNoOverflow, BVAddNoOverflow,
@ -28,11 +29,8 @@ from mythril.laser.smt import (
import logging import logging
log = logging.getLogger(__name__) log = logging.getLogger(__name__)
DISABLE_EFFECT_CHECK = True
class OverUnderflowAnnotation: class OverUnderflowAnnotation:
""" Symbol Annotation used if a BitVector can overflow""" """ Symbol Annotation used if a BitVector can overflow"""
@ -48,12 +46,19 @@ class OverUnderflowAnnotation:
class OverUnderflowStateAnnotation(StateAnnotation): class OverUnderflowStateAnnotation(StateAnnotation):
""" State Annotation used if an overflow is both possible and used in the annotated path""" """ State Annotation used if an overflow is both possible and used in the annotated path"""
def __init__( def __init__(self) -> None:
self, overflowing_state: GlobalState, operator: str, constraint: Bool self.overflowing_state_annotations = [] # type: List[OverUnderflowAnnotation]
) -> None: self.ostates_seen = set() # type: Set[GlobalState]
self.overflowing_state = overflowing_state
self.operator = operator def __copy__(self):
self.constraint = constraint new_annotation = OverUnderflowStateAnnotation()
new_annotation.overflowing_state_annotations = copy(
self.overflowing_state_annotations
)
new_annotation.ostates_seen = copy(self.ostates_seen)
return new_annotation
class IntegerOverflowUnderflowModule(DetectionModule): class IntegerOverflowUnderflowModule(DetectionModule):
@ -72,8 +77,19 @@ class IntegerOverflowUnderflowModule(DetectionModule):
entrypoint="callback", entrypoint="callback",
pre_hooks=["ADD", "MUL", "EXP", "SUB", "SSTORE", "JUMPI", "STOP", "RETURN"], pre_hooks=["ADD", "MUL", "EXP", "SUB", "SSTORE", "JUMPI", "STOP", "RETURN"],
) )
"""
Cache addresses for which overflows or underflows already have been detected.
"""
self._overflow_cache = {} # type: Dict[int, bool] self._overflow_cache = {} # type: Dict[int, bool]
self._underflow_cache = {} # type: Dict[int, bool]
"""
Cache satisfiability of overflow constraints
"""
self._ostates_satisfiable = set() # type: Set[GlobalState]
self._ostates_unsatisfiable = set() # type: Set[GlobalState]
def reset_module(self): def reset_module(self):
""" """
@ -82,7 +98,8 @@ class IntegerOverflowUnderflowModule(DetectionModule):
""" """
super().reset_module() super().reset_module()
self._overflow_cache = {} self._overflow_cache = {}
self._underflow_cache = {} self._ostates_satisfiable = set()
self._ostates_unsatisfiable = set()
def _execute(self, state: GlobalState) -> None: def _execute(self, state: GlobalState) -> None:
"""Executes analysis module for integer underflow and integer overflow. """Executes analysis module for integer underflow and integer overflow.
@ -90,12 +107,14 @@ class IntegerOverflowUnderflowModule(DetectionModule):
:param state: Statespace to analyse :param state: Statespace to analyse
:return: Found issues :return: Found issues
""" """
address = _get_address_from_state(state) address = _get_address_from_state(state)
has_overflow = self._overflow_cache.get(address, False)
has_underflow = self._underflow_cache.get(address, False) if self._overflow_cache.get(address, False):
if has_overflow or has_underflow:
return return
opcode = state.get_current_instruction()["opcode"] opcode = state.get_current_instruction()["opcode"]
funcs = { funcs = {
"ADD": [self._handle_add], "ADD": [self._handle_add],
"SUB": [self._handle_sub], "SUB": [self._handle_sub],
@ -121,11 +140,6 @@ class IntegerOverflowUnderflowModule(DetectionModule):
op0, op1 = self._get_args(state) op0, op1 = self._get_args(state)
c = Not(BVAddNoOverflow(op0, op1, False)) c = Not(BVAddNoOverflow(op0, op1, False))
# Check satisfiable
model = self._try_constraints(state.mstate.constraints, [c])
if model is None:
return
annotation = OverUnderflowAnnotation(state, "addition", c) annotation = OverUnderflowAnnotation(state, "addition", c)
op0.annotate(annotation) op0.annotate(annotation)
@ -133,11 +147,6 @@ class IntegerOverflowUnderflowModule(DetectionModule):
op0, op1 = self._get_args(state) op0, op1 = self._get_args(state)
c = Not(BVMulNoOverflow(op0, op1, False)) c = Not(BVMulNoOverflow(op0, op1, False))
# Check satisfiable
model = self._try_constraints(state.mstate.constraints, [c])
if model is None:
return
annotation = OverUnderflowAnnotation(state, "multiplication", c) annotation = OverUnderflowAnnotation(state, "multiplication", c)
op0.annotate(annotation) op0.annotate(annotation)
@ -145,11 +154,6 @@ class IntegerOverflowUnderflowModule(DetectionModule):
op0, op1 = self._get_args(state) op0, op1 = self._get_args(state)
c = Not(BVSubNoUnderflow(op0, op1, False)) c = Not(BVSubNoUnderflow(op0, op1, False))
# Check satisfiable
model = self._try_constraints(state.mstate.constraints, [c])
if model is None:
return
annotation = OverUnderflowAnnotation(state, "subtraction", c) annotation = OverUnderflowAnnotation(state, "subtraction", c)
op0.annotate(annotation) op0.annotate(annotation)
@ -174,9 +178,7 @@ class IntegerOverflowUnderflowModule(DetectionModule):
) )
else: else:
constraint = op0.value ** op1.value >= 2 ** 256 constraint = op0.value ** op1.value >= 2 ** 256
model = self._try_constraints(state.mstate.constraints, [constraint])
if model is None:
return
annotation = OverUnderflowAnnotation(state, "exponentiation", constraint) annotation = OverUnderflowAnnotation(state, "exponentiation", constraint)
op0.annotate(annotation) op0.annotate(annotation)
@ -213,36 +215,42 @@ class IntegerOverflowUnderflowModule(DetectionModule):
@staticmethod @staticmethod
def _handle_sstore(state: GlobalState) -> None: def _handle_sstore(state: GlobalState) -> None:
stack = state.mstate.stack stack = state.mstate.stack
value = stack[-2] value = stack[-2]
if not isinstance(value, Expression): if not isinstance(value, Expression):
return return
state_annotation = _get_overflowunderflow_state_annotation(state)
for annotation in value.annotations: for annotation in value.annotations:
if not isinstance(annotation, OverUnderflowAnnotation): if (
not isinstance(annotation, OverUnderflowAnnotation)
or annotation.overflowing_state in state_annotation.ostates_seen
):
continue continue
state.annotate(
OverUnderflowStateAnnotation( state_annotation.overflowing_state_annotations.append(annotation)
annotation.overflowing_state, state_annotation.ostates_seen.add(annotation.overflowing_state)
annotation.operator,
annotation.constraint,
)
)
@staticmethod @staticmethod
def _handle_jumpi(state): def _handle_jumpi(state):
stack = state.mstate.stack stack = state.mstate.stack
value = stack[-2] value = stack[-2]
state_annotation = _get_overflowunderflow_state_annotation(state)
for annotation in value.annotations: for annotation in value.annotations:
if not isinstance(annotation, OverUnderflowAnnotation): if (
not isinstance(annotation, OverUnderflowAnnotation)
or annotation.overflowing_state in state_annotation.ostates_seen
):
continue continue
state.annotate(
OverUnderflowStateAnnotation( state_annotation.overflowing_state_annotations.append(annotation)
annotation.overflowing_state, state_annotation.ostates_seen.add(annotation.overflowing_state)
annotation.operator,
annotation.constraint,
)
)
@staticmethod @staticmethod
def _handle_return(state: GlobalState) -> None: def _handle_return(state: GlobalState) -> None:
@ -251,50 +259,58 @@ class IntegerOverflowUnderflowModule(DetectionModule):
locations in the memory returned by RETURN opcode. locations in the memory returned by RETURN opcode.
:param state: The Global State :param state: The Global State
""" """
stack = state.mstate.stack stack = state.mstate.stack
try: try:
offset, length = get_concrete_int(stack[-1]), get_concrete_int(stack[-2]) offset, length = get_concrete_int(stack[-1]), get_concrete_int(stack[-2])
except TypeError: except TypeError:
return return
state_annotation = _get_overflowunderflow_state_annotation(state)
for element in state.mstate.memory[offset : offset + length]: for element in state.mstate.memory[offset : offset + length]:
if not isinstance(element, Expression): if not isinstance(element, Expression):
continue continue
for annotation in element.annotations: for annotation in element.annotations:
if isinstance(annotation, OverUnderflowAnnotation): if (
state.annotate( isinstance(annotation, OverUnderflowAnnotation)
OverUnderflowStateAnnotation( and annotation not in state_annotation.overflowing_state_annotations
annotation.overflowing_state, ):
annotation.operator, state_annotation.overflowing_state_annotations.append(annotation)
annotation.constraint,
)
)
def _handle_transaction_end(self, state: GlobalState) -> None: def _handle_transaction_end(self, state: GlobalState) -> None:
for annotation in cast(
List[OverUnderflowStateAnnotation], state_annotation = _get_overflowunderflow_state_annotation(state)
state.get_annotations(OverUnderflowStateAnnotation),
): for annotation in state_annotation.overflowing_state_annotations:
ostate = annotation.overflowing_state ostate = annotation.overflowing_state
address = _get_address_from_state(ostate)
if annotation.operator == "subtraction" and self._underflow_cache.get( if ostate in self._ostates_unsatisfiable:
address, False
):
continue continue
if annotation.operator != "subtraction" and self._overflow_cache.get( if ostate not in self._ostates_satisfiable:
address, False try:
): constraints = ostate.mstate.constraints + [annotation.constraint]
continue solver.get_model(constraints)
self._ostates_satisfiable.add(ostate)
except:
self._ostates_unsatisfiable.add(ostate)
continue
log.debug(
"Checking overflow in {} at transaction end address {}, ostate address {}".format(
state.get_current_instruction()["opcode"],
state.get_current_instruction()["address"],
ostate.get_current_instruction()["address"],
)
)
try: try:
# This check can be disabled if the contraints are to difficult for z3 to solve
# within any reasonable time. constraints = state.mstate.constraints + [annotation.constraint]
if DISABLE_EFFECT_CHECK:
constraints = ostate.mstate.constraints + [annotation.constraint]
else:
constraints = state.mstate.constraints + [annotation.constraint]
transaction_sequence = solver.get_transaction_sequence( transaction_sequence = solver.get_transaction_sequence(
state, constraints state, constraints
@ -314,29 +330,32 @@ class IntegerOverflowUnderflowModule(DetectionModule):
description_head=self._get_description_head(annotation, _type), description_head=self._get_description_head(annotation, _type),
description_tail=self._get_description_tail(annotation, _type), description_tail=self._get_description_tail(annotation, _type),
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
transaction_sequence=transaction_sequence,
) )
issue.debug = json.dumps(transaction_sequence, indent=4) address = _get_address_from_state(ostate)
self._overflow_cache[address] = True
if annotation.operator == "subtraction":
self._underflow_cache[address] = True
else:
self._overflow_cache[address] = True
self._issues.append(issue) 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() detector = IntegerOverflowUnderflowModule()
def _get_address_from_state(state): def _get_address_from_state(state):
return state.get_current_instruction()["address"] return state.get_current_instruction()["address"]
def _get_overflowunderflow_state_annotation(
state: GlobalState
) -> OverUnderflowStateAnnotation:
state_annotations = cast(
List[OverUnderflowStateAnnotation],
list(state.get_annotations(OverUnderflowStateAnnotation)),
)
if len(state_annotations) == 0:
state_annotation = OverUnderflowStateAnnotation()
state.annotate(state_annotation)
return state_annotation
else:
return state_annotations[0]

@ -4,6 +4,10 @@ from mythril.analysis.swc_data import UNPROTECTED_SELFDESTRUCT
from mythril.exceptions import UnsatError from mythril.exceptions import UnsatError
from mythril.analysis.modules.base import DetectionModule from mythril.analysis.modules.base import DetectionModule
from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.laser.ethereum.transaction.symbolic import ATTACKER_ADDRESS
from mythril.laser.ethereum.transaction.transaction_models import (
ContractCreationTransaction,
)
import logging import logging
import json import json
@ -58,12 +62,17 @@ class SuicideModule(DetectionModule):
description_head = "The contract can be killed by anyone." description_head = "The contract can be killed by anyone."
constraints = []
for tx in state.world_state.transaction_sequence:
if not isinstance(tx, ContractCreationTransaction):
constraints.append(tx.caller == ATTACKER_ADDRESS)
try: try:
try: try:
transaction_sequence = solver.get_transaction_sequence( transaction_sequence = solver.get_transaction_sequence(
state, state,
state.mstate.constraints state.mstate.constraints + constraints + [to == ATTACKER_ADDRESS],
+ [to == 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF],
) )
description_tail = ( description_tail = (
"Anyone can kill this contract and withdraw its balance to an arbitrary " "Anyone can kill this contract and withdraw its balance to an arbitrary "
@ -71,11 +80,10 @@ class SuicideModule(DetectionModule):
) )
except UnsatError: except UnsatError:
transaction_sequence = solver.get_transaction_sequence( transaction_sequence = solver.get_transaction_sequence(
state, state.mstate.constraints state, state.mstate.constraints + constraints
) )
description_tail = "Arbitrary senders can kill this contract." description_tail = "Arbitrary senders can kill this contract."
debug = json.dumps(transaction_sequence, indent=4)
self._cache_address[instruction["address"]] = True self._cache_address[instruction["address"]] = True
issue = Issue( issue = Issue(
@ -88,7 +96,7 @@ class SuicideModule(DetectionModule):
severity="High", severity="High",
description_head=description_head, description_head=description_head,
description_tail=description_tail, description_tail=description_tail,
debug=debug, transaction_sequence=transaction_sequence,
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
) )
return [issue] return [issue]

@ -31,7 +31,7 @@ class Issue:
severity=None, severity=None,
description_head="", description_head="",
description_tail="", description_tail="",
debug="", transaction_sequence=None,
): ):
""" """
@ -55,7 +55,6 @@ class Issue:
self.description_tail = description_tail self.description_tail = description_tail
self.description = "%s\n%s" % (description_head, description_tail) self.description = "%s\n%s" % (description_head, description_tail)
self.severity = severity self.severity = severity
self.debug = debug
self.swc_id = swc_id self.swc_id = swc_id
self.min_gas_used, self.max_gas_used = gas_used self.min_gas_used, self.max_gas_used = gas_used
self.filename = None self.filename = None
@ -64,6 +63,38 @@ class Issue:
self.source_mapping = None self.source_mapping = None
self.discovery_time = time() - StartTime().global_start_time self.discovery_time = time() - StartTime().global_start_time
self.bytecode_hash = get_code_hash(bytecode) self.bytecode_hash = get_code_hash(bytecode)
self.transaction_sequence = transaction_sequence
@property
def transaction_sequence_users(self):
""" Returns the transaction sequence in json without pre-generated block data"""
return (
json.dumps(self.transaction_sequence, indent=4)
if self.transaction_sequence
else None
)
@property
def transaction_sequence_jsonv2(self):
""" Returns the transaction sequence in json with pre-generated block data"""
return (
json.dumps(self.add_block_data(self.transaction_sequence), indent=4)
if self.transaction_sequence
else None
)
@staticmethod
def add_block_data(transaction_sequence: Dict):
""" Adds sane block data to a transaction_sequence """
for step in transaction_sequence["steps"]:
step["gasLimit"] = "0x7d000"
step["gasPrice"] = "0x773594000"
step["blockCoinbase"] = "0xcbcbcbcbcbcbcbcbcbcbcbcbcbcbcbcbcbcbcbcb"
step["blockDifficulty"] = "0xa7d7343662e26"
step["blockGasLimit"] = "0x7d0000"
step["blockNumber"] = "0x66e393"
step["blockTime"] = "0x5bfa4639"
return transaction_sequence
@property @property
def as_dict(self): def as_dict(self):
@ -79,7 +110,7 @@ class Issue:
"function": self.function, "function": self.function,
"severity": self.severity, "severity": self.severity,
"address": self.address, "address": self.address,
"debug": self.debug, "tx_sequence": self.transaction_sequence_users,
"min_gas_used": self.min_gas_used, "min_gas_used": self.min_gas_used,
"max_gas_used": self.max_gas_used, "max_gas_used": self.max_gas_used,
"sourceMap": self.source_mapping, "sourceMap": self.source_mapping,
@ -168,6 +199,7 @@ class Report:
""" """
name = self._file_name() name = self._file_name()
template = Report.environment.get_template("report_as_text.jinja2") template = Report.environment.get_template("report_as_text.jinja2")
return template.render( return template.render(
filename=name, issues=self.sorted_issues(), verbose=self.verbose filename=name, issues=self.sorted_issues(), verbose=self.verbose
) )
@ -203,7 +235,9 @@ class Report:
title = SWC_TO_TITLE[issue.swc_id] title = SWC_TO_TITLE[issue.swc_id]
except KeyError: except KeyError:
title = "Unspecified Security Issue" title = "Unspecified Security Issue"
extra = {"discoveryTime": int(issue.discovery_time * 10 ** 9)}
if issue.transaction_sequence_jsonv2:
extra["testCase"] = str(issue.transaction_sequence_jsonv2)
_issues.append( _issues.append(
{ {
"swcID": "SWC-" + issue.swc_id, "swcID": "SWC-" + issue.swc_id,
@ -214,7 +248,7 @@ class Report:
}, },
"severity": issue.severity, "severity": issue.severity,
"locations": [{"sourceMap": "%d:1:%d" % (issue.address, idx)}], "locations": [{"sourceMap": "%d:1:%d" % (issue.address, idx)}],
"extra": {"discoveryTime": int(issue.discovery_time * 10 ** 9)}, "extra": extra,
} }
) )
meta_data = self._get_exception_data() meta_data = self._get_exception_data()

@ -1,8 +1,13 @@
"""This module contains analysis module helpers to solve path constraints.""" """This module contains analysis module helpers to solve path constraints."""
from typing import Dict, List, Union
from z3 import sat, unknown, FuncInterp from z3 import sat, unknown, FuncInterp
import z3 import z3
from mythril.laser.smt import simplify, UGE, Optimize, symbol_factory from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.laser.ethereum.state.world_state import Account
from mythril.laser.ethereum.state.constraints import Constraints
from mythril.laser.ethereum.transaction import BaseTransaction
from mythril.laser.smt import UGE, Optimize, symbol_factory
from mythril.laser.ethereum.time_handler import time_handler from mythril.laser.ethereum.time_handler import time_handler
from mythril.exceptions import UnsatError from mythril.exceptions import UnsatError
from mythril.laser.ethereum.transaction.transaction_models import ( from mythril.laser.ethereum.transaction.transaction_models import (
@ -51,7 +56,7 @@ def get_model(constraints, minimize=(), maximize=(), enforce_execution_time=True
def pretty_print_model(model): def pretty_print_model(model):
""" """ Pretty prints a z3 model
:param model: :param model:
:return: :return:
@ -74,7 +79,9 @@ def pretty_print_model(model):
return ret return ret
def get_transaction_sequence(global_state, constraints): def get_transaction_sequence(
global_state: GlobalState, constraints: Constraints
) -> Dict:
"""Generate concrete transaction sequence. """Generate concrete transaction sequence.
:param global_state: GlobalState to generate transaction sequence for :param global_state: GlobalState to generate transaction sequence for
@ -83,55 +90,102 @@ def get_transaction_sequence(global_state, constraints):
transaction_sequence = global_state.world_state.transaction_sequence transaction_sequence = global_state.world_state.transaction_sequence
# gaslimit & gasprice don't exist yet concrete_transactions = []
tx_template = {
"calldata": None,
"call_value": None,
"caller": "0xCA11EDEADBEEF37E636E6CA11EDEADBEEFCA11ED",
}
concrete_transactions = {} tx_constraints, minimize = _set_minimisation_constraints(
creation_tx_ids = [] transaction_sequence, constraints.copy(), [], 5000
tx_constraints = constraints.copy() )
minimize = [] model = get_model(tx_constraints, minimize=minimize)
transactions = [] min_price_dict = {} # type: Dict[str, int]
for transaction in transaction_sequence: for transaction in transaction_sequence:
tx_id = str(transaction.id) concrete_transaction = _get_concrete_transaction(model, transaction)
if not isinstance(transaction, ContractCreationTransaction): concrete_transactions.append(concrete_transaction)
transactions.append(transaction)
# Constrain calldatasize caller = concrete_transaction["origin"]
max_calldatasize = symbol_factory.BitVecVal(5000, 256) value = int(concrete_transaction["value"], 16)
tx_constraints.append( min_price_dict[caller] = min_price_dict.get(caller, 0) + value
UGE(max_calldatasize, transaction.call_data.calldatasize)
) if isinstance(transaction_sequence[0], ContractCreationTransaction):
initial_accounts = transaction_sequence[0].prev_world_state.accounts
else:
initial_accounts = transaction_sequence[0].world_state.accounts
concrete_initial_state = _get_concrete_state(initial_accounts, min_price_dict)
steps = {"initialState": concrete_initial_state, "steps": concrete_transactions}
return steps
def _get_concrete_state(initial_accounts: Dict, min_price_dict: Dict[str, int]):
""" Gets a concrete state """
accounts = {}
for address, account in initial_accounts.items():
# Skip empty default account
data = dict() # type: Dict[str, Union[int, str]]
data["nonce"] = account.nonce
data["code"] = account.code.bytecode
data["storage"] = str(account.storage)
data["balance"] = min_price_dict.get(address, 0)
accounts[hex(address)] = data
return accounts
def _get_concrete_transaction(model: z3.Model, transaction: BaseTransaction):
""" Gets a concrete transaction from a transaction and z3 model"""
# Get concrete values from transaction
address = hex(transaction.callee_account.address.value)
value = model.eval(transaction.call_value.raw, model_completion=True).as_long()
caller = "0x" + (
"%x" % model.eval(transaction.caller.raw, model_completion=True).as_long()
).zfill(40)
if isinstance(transaction, ContractCreationTransaction):
address = ""
input_ = transaction.code.bytecode
else:
input_ = "".join(
[
hex(b)[2:] if len(hex(b)) % 2 == 0 else "0" + hex(b)[2:]
for b in transaction.call_data.concrete(model)
]
)
minimize.append(transaction.call_data.calldatasize) # Create concrete transaction dict
minimize.append(transaction.call_value) concrete_transaction = dict() # type: Dict[str, str]
concrete_transaction["input"] = "0x" + input_
concrete_transaction["value"] = "0x%x" % value
# Fixme: base origin assignment on origin symbol
concrete_transaction["origin"] = caller
concrete_transaction["address"] = "%s" % address
concrete_transactions[tx_id] = tx_template.copy() return concrete_transaction
else:
creation_tx_ids.append(tx_id)
model = get_model(tx_constraints, minimize=minimize) def _set_minimisation_constraints(
transaction_sequence, constraints, minimize, max_size
):
""" Set constraints that minimise key transaction values
for transaction in transactions: Constraints generated:
tx_id = str(transaction.id) - Upper bound on calldata size
- Minimisation of call value's and calldata sizes
concrete_transactions[tx_id]["calldata"] = "0x" + "".join( :param transaction_sequence: Transaction for which the constraints should be applied
[ :param constraints: The constraints array which should contain any added constraints
hex(b)[2:] if len(hex(b)) % 2 == 0 else "0" + hex(b)[2:] :param minimize: The minimisation array which should contain any variables that should be minimised
for b in transaction.call_data.concrete(model) :param max_size: The max size of the calldata array
] :return: updated constraints, minimize
) """
for transaction in transaction_sequence:
# Set upper bound on calldata size
max_calldata_size = symbol_factory.BitVecVal(max_size, 256)
constraints.append(UGE(max_calldata_size, transaction.call_data.calldatasize))
concrete_transactions[tx_id]["call_value"] = ( # Minimize
"0x%x" minimize.append(transaction.call_data.calldatasize)
% model.eval(transaction.call_value.raw, model_completion=True).as_long() minimize.append(transaction.call_value)
)
concrete_transactions[tx_id]["caller"] = "0x" + (
"%x" % model.eval(transaction.caller.raw, model_completion=True).as_long()
).zfill(40)
return concrete_transactions return constraints, minimize

@ -16,6 +16,19 @@ from mythril.laser.ethereum.strategy.basic import (
ReturnWeightedRandomStrategy, ReturnWeightedRandomStrategy,
BasicSearchStrategy, BasicSearchStrategy,
) )
from mythril.laser.ethereum.transaction.symbolic import (
ATTACKER_ADDRESS,
CREATOR_ADDRESS,
)
from mythril.laser.ethereum.plugins.plugin_factory import PluginFactory
from mythril.laser.ethereum.plugins.plugin_loader import LaserPluginLoader
from mythril.laser.ethereum.strategy.extensions.bounded_loops import (
BoundedLoopsStrategy,
)
from mythril.laser.smt import symbol_factory, BitVec from mythril.laser.smt import symbol_factory, BitVec
from typing import Union, List, Dict, Type from typing import Union, List, Dict, Type
from mythril.solidity.soliditycontract import EVMContract, SolidityContract from mythril.solidity.soliditycontract import EVMContract, SolidityContract
@ -37,11 +50,14 @@ class SymExecWrapper:
dynloader=None, dynloader=None,
max_depth=22, max_depth=22,
execution_timeout=None, execution_timeout=None,
loop_bound=4,
create_timeout=None, create_timeout=None,
transaction_count=2, transaction_count=2,
modules=(), modules=(),
compulsory_statespace=True, compulsory_statespace=True,
enable_iprof=False, enable_iprof=False,
disable_dependency_pruning=False,
run_analysis_modules=True,
): ):
""" """
@ -71,9 +87,23 @@ class SymExecWrapper:
else: else:
raise ValueError("Invalid strategy argument supplied") raise ValueError("Invalid strategy argument supplied")
creator_account = Account(
hex(CREATOR_ADDRESS), "", dynamic_loader=dynloader, contract_name=None
)
attacker_account = Account(
hex(ATTACKER_ADDRESS), "", dynamic_loader=dynloader, contract_name=None
)
requires_statespace = ( requires_statespace = (
compulsory_statespace or len(get_detection_modules("post", modules)) > 0 compulsory_statespace or len(get_detection_modules("post", modules)) > 0
) )
if not contract.creation_code:
self.accounts = {hex(ATTACKER_ADDRESS): attacker_account}
else:
self.accounts = {
hex(CREATOR_ADDRESS): creator_account,
hex(ATTACKER_ADDRESS): attacker_account,
}
self.laser = svm.LaserEVM( self.laser = svm.LaserEVM(
dynamic_loader=dynloader, dynamic_loader=dynloader,
@ -86,26 +116,41 @@ class SymExecWrapper:
enable_iprof=enable_iprof, enable_iprof=enable_iprof,
) )
if loop_bound is not None:
self.laser.extend_strategy(BoundedLoopsStrategy, loop_bound)
plugin_loader = LaserPluginLoader(self.laser) plugin_loader = LaserPluginLoader(self.laser)
plugin_loader.load(PluginFactory.build_mutation_pruner_plugin()) plugin_loader.load(PluginFactory.build_mutation_pruner_plugin())
plugin_loader.load(PluginFactory.build_instruction_coverage_plugin()) plugin_loader.load(PluginFactory.build_instruction_coverage_plugin())
self.laser.register_hooks( if not disable_dependency_pruning:
hook_type="pre", plugin_loader.load(PluginFactory.build_dependency_pruner_plugin())
hook_dict=get_detection_module_hooks(modules, hook_type="pre"),
) world_state = WorldState()
self.laser.register_hooks( for account in self.accounts.values():
hook_type="post", world_state.put_account(account)
hook_dict=get_detection_module_hooks(modules, hook_type="post"),
) if run_analysis_modules:
self.laser.register_hooks(
hook_type="pre",
hook_dict=get_detection_module_hooks(modules, hook_type="pre"),
)
self.laser.register_hooks(
hook_type="post",
hook_dict=get_detection_module_hooks(modules, hook_type="post"),
)
if isinstance(contract, SolidityContract): if isinstance(contract, SolidityContract):
self.laser.sym_exec( self.laser.sym_exec(
creation_code=contract.creation_code, contract_name=contract.name creation_code=contract.creation_code,
contract_name=contract.name,
world_state=world_state,
) )
elif isinstance(contract, EVMContract) and contract.creation_code: elif isinstance(contract, EVMContract) and contract.creation_code:
self.laser.sym_exec( self.laser.sym_exec(
creation_code=contract.creation_code, contract_name=contract.name creation_code=contract.creation_code,
contract_name=contract.name,
world_state=world_state,
) )
else: else:
account = Account( account = Account(
@ -115,7 +160,6 @@ class SymExecWrapper:
contract_name=contract.name, contract_name=contract.name,
concrete_storage=False, concrete_storage=False,
) )
world_state = WorldState()
world_state.put_account(account) world_state.put_account(account)
self.laser.sym_exec(world_state=world_state, target_address=address.value) self.laser.sym_exec(world_state=world_state, target_address=address.value)

@ -24,11 +24,11 @@ In file: {{ issue.filename }}:{{ issue.lineno }}
{{ issue.code }} {{ issue.code }}
``` ```
{% endif %} {% endif %}
{% if verbose and issue.debug %} {% if verbose and issue.tx_sequence %}
-------------------- --------------------
### Debugging Information: ### Debugging Information:
{{ issue.debug }} {{ issue.tx_sequence }}
{% endif %} {% endif %}
{% endfor %} {% endfor %}

@ -18,11 +18,11 @@ In file: {{ issue.filename }}:{{ issue.lineno }}
-------------------- --------------------
{% endif %} {% endif %}
{% if verbose and issue.debug %} {% if verbose and issue.tx_sequence %}
-------------------- --------------------
Transaction Sequence: Transaction Sequence:
{{ issue.debug }} {{ issue.tx_sequence }}
{% endif %} {% endif %}
{% endfor %} {% endfor %}

@ -15,6 +15,7 @@ import coloredlogs
import traceback import traceback
import mythril.support.signatures as sigs import mythril.support.signatures as sigs
from argparse import ArgumentParser, Namespace
from mythril.exceptions import AddressNotFoundError, CriticalError from mythril.exceptions import AddressNotFoundError, CriticalError
from mythril.mythril import ( from mythril.mythril import (
MythrilAnalyzer, MythrilAnalyzer,
@ -22,15 +23,33 @@ from mythril.mythril import (
MythrilConfig, MythrilConfig,
MythrilLevelDB, MythrilLevelDB,
) )
from mythril.version import VERSION from mythril.__version__ import __version__ as VERSION
ANALYZE_LIST = ("analyze", "a")
DISASSEMBLE_LIST = ("disassemble", "d")
log = logging.getLogger(__name__) log = logging.getLogger(__name__)
COMMAND_LIST = (
ANALYZE_LIST
+ DISASSEMBLE_LIST
+ (
"read-storage",
"leveldb-search",
"function-to-hash",
"hash-to-address",
"version",
"truffle",
"help",
)
)
def exit_with_error(format_, message): def exit_with_error(format_, message):
""" """
:param format_: Exits with error
:param message: :param format_: The format of the message
:param message: message
""" """
if format_ == "text" or format_ == "markdown": if format_ == "text" or format_ == "markdown":
log.error(message) log.error(message)
@ -53,94 +72,46 @@ def exit_with_error(format_, message):
sys.exit() sys.exit()
def main() -> None: def get_input_parser() -> ArgumentParser:
"""The main CLI interface entry point."""
parser = argparse.ArgumentParser(
description="Security analysis of Ethereum smart contracts"
)
create_parser(parser)
# Get config values
args = parser.parse_args()
parse_args(parser=parser, args=args)
def create_parser(parser: argparse.ArgumentParser) -> None:
""" """
Creates the parser by setting all the possible arguments Returns Parser which handles input
:param parser: The parser :return: Parser which handles input
""" """
parser.add_argument("solidity_file", nargs="*") parser = ArgumentParser(add_help=False)
parser.add_argument(
commands = parser.add_argument_group("commands")
commands.add_argument("-g", "--graph", help="generate a control flow graph")
commands.add_argument(
"-V",
"--version",
action="store_true",
help="print the Mythril version number and exit",
)
commands.add_argument(
"-x",
"--fire-lasers",
action="store_true",
help="detect vulnerabilities, use with -c, -a or solidity file(s)",
)
commands.add_argument(
"--truffle",
action="store_true",
help="analyze a truffle project (run from project dir)",
)
commands.add_argument(
"-d", "--disassemble", action="store_true", help="print disassembly"
)
commands.add_argument(
"-j",
"--statespace-json",
help="dumps the statespace json",
metavar="OUTPUT_FILE",
)
inputs = parser.add_argument_group("input arguments")
inputs.add_argument(
"-c", "-c",
"--code", "--code",
help='hex-encoded bytecode string ("6060604052...")', help='hex-encoded bytecode string ("6060604052...")',
metavar="BYTECODE", metavar="BYTECODE",
) )
inputs.add_argument( parser.add_argument(
"-f", "-f",
"--codefile", "--codefile",
help="file containing hex-encoded bytecode string", help="file containing hex-encoded bytecode string",
metavar="BYTECODEFILE", metavar="BYTECODEFILE",
type=argparse.FileType("r"), type=argparse.FileType("r"),
) )
inputs.add_argument( parser.add_argument(
"-a", "-a",
"--address", "--address",
help="pull contract from the blockchain", help="pull contract from the blockchain",
metavar="CONTRACT_ADDRESS", metavar="CONTRACT_ADDRESS",
) )
inputs.add_argument( parser.add_argument(
"-l",
"--dynld",
action="store_true",
help="auto-load dependencies from the blockchain",
)
inputs.add_argument(
"--no-onchain-storage-access",
action="store_true",
help="turns off getting the data from onchain contracts",
)
inputs.add_argument(
"--bin-runtime", "--bin-runtime",
action="store_true", action="store_true",
help="Only when -c or -f is used. Consider the input bytecode as binary runtime code, default being the contract creation bytecode.", help="Only when -c or -f is used. Consider the input bytecode as binary runtime code, default being the contract creation bytecode.",
) )
return parser
outputs = parser.add_argument_group("output formats") def get_output_parser() -> ArgumentParser:
outputs.add_argument( """
Get parser which handles output
:return: Parser which handles output
"""
parser = argparse.ArgumentParser(add_help=False)
parser.add_argument(
"-o", "-o",
"--outform", "--outform",
choices=["text", "markdown", "json", "jsonv2"], choices=["text", "markdown", "json", "jsonv2"],
@ -148,43 +119,199 @@ def create_parser(parser: argparse.ArgumentParser) -> None:
help="report output format", help="report output format",
metavar="<text/markdown/json/jsonv2>", metavar="<text/markdown/json/jsonv2>",
) )
outputs.add_argument( parser.add_argument(
"--verbose-report", "--verbose-report",
action="store_true", action="store_true",
help="Include debugging information in report", help="Include debugging information in report",
) )
return parser
def get_rpc_parser() -> ArgumentParser:
"""
Get parser which handles RPC flags
:return: Parser which handles rpc inputs
"""
parser = argparse.ArgumentParser(add_help=False)
parser.add_argument(
"--rpc",
help="custom RPC settings",
metavar="HOST:PORT / ganache / infura-[network_name]",
default="infura-mainnet",
)
parser.add_argument(
"--rpctls", type=bool, default=False, help="RPC connection over TLS"
)
return parser
database = parser.add_argument_group("local contracts database") def get_utilities_parser() -> ArgumentParser:
database.add_argument( """
"-s", "--search", help="search the contract database", metavar="EXPRESSION" Get parser which handles utilities flags
:return: Parser which handles utility flags
"""
parser = argparse.ArgumentParser(add_help=False)
parser.add_argument("--solc-args", help="Extra arguments for solc")
parser.add_argument(
"--solv",
help="specify solidity compiler version. If not present, will try to install it (Experimental)",
metavar="SOLV",
)
return parser
def main() -> None:
"""The main CLI interface entry point."""
rpc_parser = get_rpc_parser()
utilities_parser = get_utilities_parser()
input_parser = get_input_parser()
output_parser = get_output_parser()
parser = argparse.ArgumentParser(
description="Security analysis of Ethereum smart contracts"
)
parser.add_argument("--epic", action="store_true", help=argparse.SUPPRESS)
parser.add_argument(
"-v", type=int, help="log level (0-5)", metavar="LOG_LEVEL", default=2
)
subparsers = parser.add_subparsers(dest="command", help="Commands")
analyzer_parser = subparsers.add_parser(
ANALYZE_LIST[0],
help="Triggers the analysis of the smart contract",
parents=[rpc_parser, utilities_parser, input_parser, output_parser],
aliases=ANALYZE_LIST[1:],
)
create_analyzer_parser(analyzer_parser)
disassemble_parser = subparsers.add_parser(
DISASSEMBLE_LIST[0],
help="Disassembles the smart contract",
aliases=DISASSEMBLE_LIST[1:],
parents=[rpc_parser, utilities_parser, input_parser],
)
create_disassemble_parser(disassemble_parser)
read_storage_parser = subparsers.add_parser(
"read-storage",
help="Retrieves storage slots from a given address through rpc",
parents=[rpc_parser],
)
leveldb_search_parser = subparsers.add_parser(
"leveldb-search", help="Searches the code fragment in local leveldb"
) )
database.add_argument( contract_func_to_hash = subparsers.add_parser(
"function-to-hash", help="Returns the hash signature of the function"
)
contract_hash_to_addr = subparsers.add_parser(
"hash-to-address",
help="converts the hashes in the blockchain to ethereum address",
)
subparsers.add_parser(
"version", parents=[output_parser], help="Outputs the version"
)
create_read_storage_parser(read_storage_parser)
create_hash_to_addr_parser(contract_hash_to_addr)
create_func_to_hash_parser(contract_func_to_hash)
create_leveldb_parser(leveldb_search_parser)
subparsers.add_parser("truffle", parents=[analyzer_parser], add_help=False)
subparsers.add_parser("help", add_help=False)
# Get config values
args = parser.parse_args()
parse_args_and_execute(parser=parser, args=args)
def create_disassemble_parser(parser: ArgumentParser):
"""
Modify parser to handle disassembly
:param parser:
:return:
"""
parser.add_argument("solidity_file", nargs="*")
def create_read_storage_parser(read_storage_parser: ArgumentParser):
"""
Modify parser to handle storage slots
:param read_storage_parser:
:return:
"""
read_storage_parser.add_argument(
"storage_slots",
help="read state variables from storage index",
metavar="INDEX,NUM_SLOTS,[array] / mapping,INDEX,[KEY1, KEY2...]",
)
read_storage_parser.add_argument(
"address", help="contract address", metavar="ADDRESS"
)
def create_leveldb_parser(parser: ArgumentParser):
"""
Modify parser to handle leveldb-search
:param parser:
:return:
"""
parser.add_argument("search")
parser.add_argument(
"--leveldb-dir", "--leveldb-dir",
help="specify leveldb directory for search or direct access operations", help="specify leveldb directory for search or direct access operations",
metavar="LEVELDB_PATH", metavar="LEVELDB_PATH",
) )
utilities = parser.add_argument_group("utilities")
utilities.add_argument( def create_func_to_hash_parser(parser: ArgumentParser):
"--hash", help="calculate function signature hash", metavar="SIGNATURE" """
) Modify parser to handle func_to_hash command
utilities.add_argument( :param parser:
"--storage", :return:
help="read state variables from storage index, use with -a", """
metavar="INDEX,NUM_SLOTS,[array] / mapping,INDEX,[KEY1, KEY2...]", parser.add_argument(
"func_name", help="calculate function signature hash", metavar="SIGNATURE"
) )
utilities.add_argument(
"--solv",
help="specify solidity compiler version. If not present, will try to install it (Experimental)", def create_hash_to_addr_parser(hash_parser: ArgumentParser):
metavar="SOLV", """
Modify parser to handle hash_to_addr command
:param hash_parser:
:return:
"""
hash_parser.add_argument(
"hash", help="Find the address from hash", metavar="FUNCTION_NAME"
) )
utilities.add_argument( hash_parser.add_argument(
"--contract-hash-to-address", "--leveldb-dir",
help="returns corresponding address for a contract address hash", help="specify leveldb directory for search or direct access operations",
metavar="SHA3_TO_LOOK_FOR", metavar="LEVELDB_PATH",
) )
options = parser.add_argument_group("options")
def create_analyzer_parser(analyzer_parser: ArgumentParser):
"""
Modify parser to handle analyze command
:param analyzer_parser:
:return:
"""
analyzer_parser.add_argument("solidity_file", nargs="*")
commands = analyzer_parser.add_argument_group("commands")
commands.add_argument("-g", "--graph", help="generate a control flow graph")
commands.add_argument(
"-j",
"--statespace-json",
help="dumps the statespace json",
metavar="OUTPUT_FILE",
)
commands.add_argument(
"--truffle",
action="store_true",
help="analyze a truffle project (run from project dir)",
)
options = analyzer_parser.add_argument_group("options")
options.add_argument( options.add_argument(
"-m", "-m",
"--modules", "--modules",
@ -197,13 +324,20 @@ def create_parser(parser: argparse.ArgumentParser) -> None:
default=50, default=50,
help="Maximum recursion depth for symbolic execution", help="Maximum recursion depth for symbolic execution",
) )
options.add_argument( options.add_argument(
"--strategy", "--strategy",
choices=["dfs", "bfs", "naive-random", "weighted-random"], choices=["dfs", "bfs", "naive-random", "weighted-random"],
default="bfs", default="bfs",
help="Symbolic execution strategy", help="Symbolic execution strategy",
) )
options.add_argument(
"-b",
"--loop-bound",
type=int,
default=4,
help="Bound loops at n iterations",
metavar="N",
)
options.add_argument( options.add_argument(
"-t", "-t",
"--transaction-count", "--transaction-count",
@ -223,15 +357,23 @@ def create_parser(parser: argparse.ArgumentParser) -> None:
default=10, default=10,
help="The amount of seconds to spend on " "the initial contract creation", help="The amount of seconds to spend on " "the initial contract creation",
) )
options.add_argument("--solc-args", help="Extra arguments for solc")
options.add_argument( options.add_argument(
"--phrack", action="store_true", help="Phrack-style call graph" "-l",
"--dynld",
action="store_true",
help="auto-load dependencies from the blockchain",
) )
options.add_argument( options.add_argument(
"--enable-physics", action="store_true", help="enable graph physics simulation" "--no-onchain-storage-access",
action="store_true",
help="turns off getting the data from onchain contracts",
) )
options.add_argument( options.add_argument(
"-v", type=int, help="log level (0-5)", metavar="LOG_LEVEL", default=2 "--phrack", action="store_true", help="Phrack-style call graph"
)
options.add_argument(
"--enable-physics", action="store_true", help="enable graph physics simulation"
) )
options.add_argument( options.add_argument(
"-q", "-q",
@ -242,37 +384,20 @@ def create_parser(parser: argparse.ArgumentParser) -> None:
options.add_argument( options.add_argument(
"--enable-iprof", action="store_true", help="enable the instruction profiler" "--enable-iprof", action="store_true", help="enable the instruction profiler"
) )
options.add_argument(
rpc = parser.add_argument_group("RPC options") "--disable-dependency-pruning",
action="store_true",
rpc.add_argument( help="Deactivate dependency-based pruning",
"--rpc",
help="custom RPC settings",
metavar="HOST:PORT / ganache / infura-[network_name]",
default="infura-mainnet",
)
rpc.add_argument(
"--rpctls", type=bool, default=False, help="RPC connection over TLS"
) )
parser.add_argument("--epic", action="store_true", help=argparse.SUPPRESS)
def validate_args(parser: argparse.ArgumentParser, args: argparse.Namespace): def validate_args(args: Namespace):
if not ( """
args.search Validate cli args
or args.hash :param args:
or args.disassemble :return:
or args.graph """
or args.fire_lasers if args.__dict__.get("v", False):
or args.storage
or args.truffle
or args.statespace_json
or args.contract_hash_to_address
):
parser.print_help()
sys.exit()
if args.v:
if 0 <= args.v < 6: if 0 <= args.v < 6:
log_levels = [ log_levels = [
logging.NOTSET, logging.NOTSET,
@ -291,81 +416,92 @@ def validate_args(parser: argparse.ArgumentParser, args: argparse.Namespace):
args.outform, "Invalid -v value, you can find valid values in usage" args.outform, "Invalid -v value, you can find valid values in usage"
) )
if args.query_signature: if args.command in ANALYZE_LIST:
if sigs.ethereum_input_decoder is None: if args.query_signature and sigs.ethereum_input_decoder is None:
exit_with_error( exit_with_error(
args.outform, args.outform,
"The --query-signature function requires the python package ethereum-input-decoder", "The --query-signature function requires the python package ethereum-input-decoder",
) )
if args.enable_iprof: if args.enable_iprof and args.v < 4:
if args.v < 4:
exit_with_error( exit_with_error(
args.outform, args.outform,
"--enable-iprof must be used with -v LOG_LEVEL where LOG_LEVEL >= 4", "--enable-iprof must be used with -v LOG_LEVEL where LOG_LEVEL >= 4",
) )
elif not (args.graph or args.fire_lasers or args.statespace_json):
exit_with_error(
args.outform,
"--enable-iprof must be used with one of -g, --graph, -x, --fire-lasers, -j and --statespace-json",
)
def quick_commands(args: argparse.Namespace): def set_config(args: Namespace):
if args.hash: """
print(MythrilDisassembler.hash_for_function_signature(args.hash)) Set config based on args
sys.exit() :param args:
:return: modified config
"""
def set_config(args: argparse.Namespace):
config = MythrilConfig() config = MythrilConfig()
if args.dynld or not args.no_onchain_storage_access and not (args.rpc or args.i): if (
args.command in ANALYZE_LIST
and (args.dynld or not args.no_onchain_storage_access)
) and not (args.rpc or args.i):
config.set_api_from_config_path() config.set_api_from_config_path()
if args.address: if args.__dict__.get("address", None):
# Establish RPC connection if necessary # Establish RPC connection if necessary
config.set_api_rpc(rpc=args.rpc, rpctls=args.rpctls) config.set_api_rpc(rpc=args.rpc, rpctls=args.rpctls)
elif args.search or args.contract_hash_to_address: if args.command in ("hash-to-address", "leveldb-search"):
# Open LevelDB if necessary # Open LevelDB if necessary
config.set_api_leveldb( if not args.__dict__.get("leveldb_dir", None):
config.leveldb_dir if not args.leveldb_dir else args.leveldb_dir leveldb_dir = config.leveldb_dir
) else:
leveldb_dir = args.leveldb_dir
config.set_api_leveldb(leveldb_dir)
return config return config
def leveldb_search(config: MythrilConfig, args: argparse.Namespace): def leveldb_search(config: MythrilConfig, args: Namespace):
if args.search or args.contract_hash_to_address: """
Handle leveldb search
:param config:
:param args:
:return:
"""
if args.command in ("hash-to-address", "leveldb-search"):
leveldb_searcher = MythrilLevelDB(config.eth_db) leveldb_searcher = MythrilLevelDB(config.eth_db)
if args.search: if args.command == "leveldb-search":
# Database search ops # Database search ops
leveldb_searcher.search_db(args.search) leveldb_searcher.search_db(args.search)
else: else:
# search corresponding address # search corresponding address
try: try:
leveldb_searcher.contract_hash_to_address(args.contract_hash_to_address) leveldb_searcher.contract_hash_to_address(args.hash)
except AddressNotFoundError: except AddressNotFoundError:
print("Address not found.") print("Address not found.")
sys.exit() sys.exit()
def get_code(disassembler: MythrilDisassembler, args: argparse.Namespace): def load_code(disassembler: MythrilDisassembler, args: Namespace):
"""
Loads code into disassembly and returns address
:param disassembler:
:param args:
:return: Address
"""
address = None address = None
if args.code: if args.__dict__.get("code", False):
# Load from bytecode # Load from bytecode
code = args.code[2:] if args.code.startswith("0x") else args.code code = args.code[2:] if args.code.startswith("0x") else args.code
address, _ = disassembler.load_from_bytecode(code, args.bin_runtime) address, _ = disassembler.load_from_bytecode(code, args.bin_runtime)
elif args.codefile: elif args.__dict__.get("codefile", False):
bytecode = "".join([l.strip() for l in args.codefile if len(l.strip()) > 0]) bytecode = "".join([l.strip() for l in args.codefile if len(l.strip()) > 0])
bytecode = bytecode[2:] if bytecode.startswith("0x") else bytecode bytecode = bytecode[2:] if bytecode.startswith("0x") else bytecode
address, _ = disassembler.load_from_bytecode(bytecode, args.bin_runtime) address, _ = disassembler.load_from_bytecode(bytecode, args.bin_runtime)
elif args.address: elif args.__dict__.get("address", False):
# Get bytecode from a contract address # Get bytecode from a contract address
address, _ = disassembler.load_from_address(args.address) address, _ = disassembler.load_from_address(args.address)
elif args.solidity_file: elif args.__dict__.get("solidity_file", False):
# Compile Solidity source file(s) # Compile Solidity source file(s)
if args.graph and len(args.solidity_file) > 1: if args.command in ANALYZE_LIST and args.graph and len(args.solidity_file) > 1:
exit_with_error( exit_with_error(
args.outform, args.outform,
"Cannot generate call graphs from multiple input files. Please do it one at a time.", "Cannot generate call graphs from multiple input files. Please do it one at a time.",
@ -375,8 +511,8 @@ def get_code(disassembler: MythrilDisassembler, args: argparse.Namespace):
) # list of files ) # list of files
else: else:
exit_with_error( exit_with_error(
args.outform, args.__dict__.get("outform", "text"),
"No input bytecode. Please provide EVM code via -c BYTECODE, -a ADDRESS, or -i SOLIDITY_FILES", "No input bytecode. Please provide EVM code via -c BYTECODE, -a ADDRESS, -f BYTECODE_FILE or <SOLIDITY_FILE>",
) )
return address return address
@ -384,43 +520,44 @@ def get_code(disassembler: MythrilDisassembler, args: argparse.Namespace):
def execute_command( def execute_command(
disassembler: MythrilDisassembler, disassembler: MythrilDisassembler,
address: str, address: str,
parser: argparse.ArgumentParser, parser: ArgumentParser,
args: argparse.Namespace, args: Namespace,
): ):
"""
Execute command
:param disassembler:
:param address:
:param parser:
:param args:
:return:
"""
if args.storage: if args.command == "read-storage":
if not args.address:
exit_with_error(
args.outform,
"To read storage, provide the address of a deployed contract with the -a option.",
)
storage = disassembler.get_state_variable_from_storage( storage = disassembler.get_state_variable_from_storage(
address=address, params=[a.strip() for a in args.storage.strip().split(",")] address=address,
params=[a.strip() for a in args.storage_slots.strip().split(",")],
) )
print(storage) print(storage)
return
analyzer = MythrilAnalyzer(
strategy=args.strategy,
disassembler=disassembler,
address=address,
max_depth=args.max_depth,
execution_timeout=args.execution_timeout,
create_timeout=args.create_timeout,
enable_iprof=args.enable_iprof,
onchain_storage_access=not args.no_onchain_storage_access,
)
if args.disassemble:
# or mythril.disassemble(mythril.contracts[0])
elif args.command in DISASSEMBLE_LIST:
if disassembler.contracts[0].code: if disassembler.contracts[0].code:
print("Runtime Disassembly: \n" + disassembler.contracts[0].get_easm()) print("Runtime Disassembly: \n" + disassembler.contracts[0].get_easm())
if disassembler.contracts[0].creation_code: if disassembler.contracts[0].creation_code:
print("Disassembly: \n" + disassembler.contracts[0].get_creation_easm()) print("Disassembly: \n" + disassembler.contracts[0].get_creation_easm())
elif args.graph or args.fire_lasers: elif args.command in ANALYZE_LIST:
analyzer = MythrilAnalyzer(
strategy=args.strategy,
disassembler=disassembler,
address=address,
max_depth=args.max_depth,
execution_timeout=args.execution_timeout,
create_timeout=args.create_timeout,
enable_iprof=args.enable_iprof,
disable_dependency_pruning=args.disable_dependency_pruning,
onchain_storage_access=not args.no_onchain_storage_access,
)
if not disassembler.contracts: if not disassembler.contracts:
exit_with_error( exit_with_error(
args.outform, "input files do not contain any valid contracts" args.outform, "input files do not contain any valid contracts"
@ -440,6 +577,21 @@ def execute_command(
except Exception as e: except Exception as e:
exit_with_error(args.outform, "Error saving graph: " + str(e)) exit_with_error(args.outform, "Error saving graph: " + str(e))
elif args.statespace_json:
if not analyzer.contracts:
exit_with_error(
args.outform, "input files do not contain any valid contracts"
)
statespace = analyzer.dump_statespace(contract=analyzer.contracts[0])
try:
with open(args.statespace_json, "w") as f:
json.dump(statespace, f)
except Exception as e:
exit_with_error(args.outform, "Error saving json: " + str(e))
else: else:
try: try:
report = analyzer.fire_lasers( report = analyzer.fire_lasers(
@ -458,29 +610,24 @@ def execute_command(
print(outputs[args.outform]) print(outputs[args.outform])
except ModuleNotFoundError as e: except ModuleNotFoundError as e:
exit_with_error( exit_with_error(
args.outform, "Error loading analyis modules: " + format(e) args.outform, "Error loading analysis modules: " + format(e)
) )
elif args.statespace_json:
if not analyzer.contracts:
exit_with_error(
args.outform, "input files do not contain any valid contracts"
)
statespace = analyzer.dump_statespace(contract=analyzer.contracts[0])
try:
with open(args.statespace_json, "w") as f:
json.dump(statespace, f)
except Exception as e:
exit_with_error(args.outform, "Error saving json: " + str(e))
else: else:
parser.print_help() parser.print_help()
def parse_args(parser: argparse.ArgumentParser, args: argparse.Namespace) -> None: def contract_hash_to_address(args: Namespace):
"""
prints the hash from function signature
:param args:
:return:
"""
print(MythrilDisassembler.hash_for_function_signature(args.func_name))
sys.exit()
def parse_args_and_execute(parser: ArgumentParser, args: Namespace) -> None:
""" """
Parses the arguments Parses the arguments
:param parser: The parser :param parser: The parser
@ -493,42 +640,55 @@ def parse_args(parser: argparse.ArgumentParser, args: argparse.Namespace) -> Non
os.system(" ".join(sys.argv) + " | python3 " + path + "/epic.py") os.system(" ".join(sys.argv) + " | python3 " + path + "/epic.py")
sys.exit() sys.exit()
if args.version: if args.command not in COMMAND_LIST or args.command is None:
parser.print_help()
sys.exit()
if args.command == "version":
if args.outform == "json": if args.outform == "json":
print(json.dumps({"version_str": VERSION})) print(json.dumps({"version_str": VERSION}))
else: else:
print("Mythril version {}".format(VERSION)) print("Mythril version {}".format(VERSION))
sys.exit() sys.exit()
if args.command == "help":
parser.print_help()
sys.exit()
# Parse cmdline args # Parse cmdline args
validate_args(parser, args) validate_args(args)
try: try:
quick_commands(args) if args.command == "function-to-hash":
contract_hash_to_address(args)
config = set_config(args) config = set_config(args)
leveldb_search(config, args) leveldb_search(config, args)
query_signature = args.__dict__.get("query_signature", None)
solc_args = args.__dict__.get("solc_args", None)
solv = args.__dict__.get("solv", None)
disassembler = MythrilDisassembler( disassembler = MythrilDisassembler(
eth=config.eth, eth=config.eth,
solc_version=args.solv, solc_version=solv,
solc_args=args.solc_args, solc_args=solc_args,
enable_online_lookup=args.query_signature, enable_online_lookup=query_signature,
) )
if args.truffle: if args.command == "truffle":
try: try:
disassembler.analyze_truffle_project(args) disassembler.analyze_truffle_project(args)
except FileNotFoundError: except FileNotFoundError:
print( print(
"Build directory not found. Make sure that you start the analysis from the project root, and that 'truffle compile' has executed successfully." "Build directory not found. Make sure that you start the analysis from the project root, "
"and that 'truffle compile' has executed successfully."
) )
sys.exit() sys.exit()
address = get_code(disassembler, args) address = load_code(disassembler, args)
execute_command( execute_command(
disassembler=disassembler, address=address, parser=parser, args=args disassembler=disassembler, address=address, parser=parser, args=args
) )
except CriticalError as ce: except CriticalError as ce:
exit_with_error(args.outform, str(ce)) exit_with_error(args.__dict__.get("outform", "text"), str(ce))
except Exception: except Exception:
exit_with_error(args.outform, traceback.format_exc()) exit_with_error(args.__dict__.get("outform", "text"), traceback.format_exc())
if __name__ == "__main__": if __name__ == "__main__":

@ -96,7 +96,7 @@ def get_callee_address(
# attempt to read the contract address from instance storage # attempt to read the contract address from instance storage
try: try:
callee_address = dynamic_loader.read_storage( callee_address = dynamic_loader.read_storage(
str(hex(environment.active_account.address.value)), index hex(environment.active_account.address.value), index
) )
# TODO: verify whether this happens or not # TODO: verify whether this happens or not
except: except:

@ -768,18 +768,8 @@ class Instruction:
size_sym = True size_sym = True
if size_sym: if size_sym:
state.mem_extend(mstart, 1) size = 320 # The excess size will get overwritten
state.memory[mstart] = global_state.new_bitvec(
"calldata_"
+ str(environment.active_account.contract_name)
+ "["
+ str(dstart)
+ ": + "
+ str(size)
+ "]",
8,
)
return [global_state]
size = cast(int, size) size = cast(int, size)
if size > 0: if size > 0:
try: try:
@ -1019,16 +1009,61 @@ class Instruction:
global_state.mstate.stack.pop(), global_state.mstate.stack.pop(),
global_state.mstate.stack.pop(), global_state.mstate.stack.pop(),
) )
return self._code_copy_helper(
code=global_state.environment.code.bytecode,
memory_offset=memory_offset,
code_offset=code_offset,
size=size,
op="CODECOPY",
global_state=global_state,
)
@StateTransition()
def extcodesize_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
state = global_state.mstate
addr = state.stack.pop()
try:
addr = hex(helper.get_concrete_int(addr))
except TypeError:
log.debug("unsupported symbolic address for EXTCODESIZE")
state.stack.append(global_state.new_bitvec("extcodesize_" + str(addr), 256))
return [global_state]
try:
code = global_state.world_state.accounts_exist_or_load(
addr, self.dynamic_loader
)
except (ValueError, AttributeError) as e:
log.debug("error accessing contract storage due to: " + str(e))
state.stack.append(global_state.new_bitvec("extcodesize_" + str(addr), 256))
return [global_state]
state.stack.append(len(code) // 2)
return [global_state]
@staticmethod
def _code_copy_helper(
code: str,
memory_offset: BitVec,
code_offset: BitVec,
size: BitVec,
op: str,
global_state: GlobalState,
) -> List[GlobalState]:
try: try:
concrete_memory_offset = helper.get_concrete_int(memory_offset) concrete_memory_offset = helper.get_concrete_int(memory_offset)
except TypeError: except TypeError:
log.debug("Unsupported symbolic memory offset in CODECOPY") log.debug("Unsupported symbolic memory offset in {}".format(op))
return [global_state] return [global_state]
try: try:
size = helper.get_concrete_int(size) concrete_size = helper.get_concrete_int(size)
global_state.mstate.mem_extend(concrete_memory_offset, size) global_state.mstate.mem_extend(concrete_memory_offset, concrete_size)
except TypeError: except TypeError:
# except both attribute error and Exception # except both attribute error and Exception
@ -1046,9 +1081,9 @@ class Instruction:
try: try:
concrete_code_offset = helper.get_concrete_int(code_offset) concrete_code_offset = helper.get_concrete_int(code_offset)
except TypeError: except TypeError:
log.debug("Unsupported symbolic code offset in CODECOPY") log.debug("Unsupported symbolic code offset in {}".format(op))
global_state.mstate.mem_extend(concrete_memory_offset, size) global_state.mstate.mem_extend(concrete_memory_offset, concrete_size)
for i in range(size): for i in range(concrete_size):
global_state.mstate.memory[ global_state.mstate.memory[
concrete_memory_offset + i concrete_memory_offset + i
] = global_state.new_bitvec( ] = global_state.new_bitvec(
@ -1059,21 +1094,20 @@ class Instruction:
) )
return [global_state] return [global_state]
bytecode = global_state.environment.code.bytecode if code[0:2] == "0x":
if bytecode[0:2] == "0x": code = code[2:]
bytecode = bytecode[2:]
if size == 0 and isinstance( if concrete_size == 0 and isinstance(
global_state.current_transaction, ContractCreationTransaction global_state.current_transaction, ContractCreationTransaction
): ):
if concrete_code_offset >= len(bytecode) // 2: if concrete_code_offset >= len(code) // 2:
self._handle_symbolic_args(global_state, concrete_memory_offset) Instruction._handle_symbolic_args(global_state, concrete_memory_offset)
return [global_state] return [global_state]
for i in range(size): for i in range(concrete_size):
if 2 * (concrete_code_offset + i + 1) <= len(bytecode): if 2 * (concrete_code_offset + i + 1) <= len(code):
global_state.mstate.memory[concrete_memory_offset + i] = int( global_state.mstate.memory[concrete_memory_offset + i] = int(
bytecode[ code[
2 2
* (concrete_code_offset + i) : 2 * (concrete_code_offset + i) : 2
* (concrete_code_offset + i + 1) * (concrete_code_offset + i + 1)
@ -1093,35 +1127,41 @@ class Instruction:
return [global_state] return [global_state]
@StateTransition() @StateTransition()
def extcodesize_(self, global_state: GlobalState) -> List[GlobalState]: def extcodecopy_(self, global_state: GlobalState) -> List[GlobalState]:
""" """
:param global_state: :param global_state:
:return: :return:
""" """
state = global_state.mstate state = global_state.mstate
addr = state.stack.pop() addr, memory_offset, code_offset, size = (
environment = global_state.environment state.stack.pop(),
state.stack.pop(),
state.stack.pop(),
state.stack.pop(),
)
try: try:
addr = hex(helper.get_concrete_int(addr)) addr = hex(helper.get_concrete_int(addr))
except TypeError: except TypeError:
log.debug("unsupported symbolic address for EXTCODESIZE") log.debug("unsupported symbolic address for EXTCODECOPY")
state.stack.append(global_state.new_bitvec("extcodesize_" + str(addr), 256))
return [global_state] return [global_state]
try: try:
code = self.dynamic_loader.dynld(addr) code = global_state.world_state.accounts_exist_or_load(
addr, self.dynamic_loader
)
except (ValueError, AttributeError) as e: except (ValueError, AttributeError) as e:
log.debug("error accessing contract storage due to: " + str(e)) log.debug("error accessing contract storage due to: " + str(e))
state.stack.append(global_state.new_bitvec("extcodesize_" + str(addr), 256))
return [global_state] return [global_state]
if code is None: return self._code_copy_helper(
state.stack.append(0) code=code,
else: memory_offset=memory_offset,
state.stack.append(len(code.bytecode) // 2) code_offset=code_offset,
size=size,
return [global_state] op="EXTCODECOPY",
global_state=global_state,
)
@StateTransition @StateTransition
def extcodehash_(self, global_state: GlobalState) -> List[GlobalState]: def extcodehash_(self, global_state: GlobalState) -> List[GlobalState]:
@ -1137,20 +1177,6 @@ class Instruction:
) )
return [global_state] return [global_state]
@StateTransition()
def extcodecopy_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
# FIXME: not implemented
state = global_state.mstate
addr = state.stack.pop()
start, s2, size = state.stack.pop(), state.stack.pop(), state.stack.pop()
return [global_state]
@StateTransition() @StateTransition()
def returndatacopy_(self, global_state: GlobalState) -> List[GlobalState]: def returndatacopy_(self, global_state: GlobalState) -> List[GlobalState]:
""" """
@ -1852,6 +1878,14 @@ class Instruction:
callee_address, callee_account, call_data, value, gas, memory_out_offset, memory_out_size = get_call_parameters( callee_address, callee_account, call_data, value, gas, memory_out_offset, memory_out_size = get_call_parameters(
global_state, self.dynamic_loader, True global_state, self.dynamic_loader, True
) )
if callee_account is not None and callee_account.code.bytecode == "":
log.debug("The call is related to ether transfer between accounts")
global_state.mstate.stack.append(
global_state.new_bitvec("retval_" + str(instr["address"]), 256)
)
return [global_state]
except ValueError as e: except ValueError as e:
log.debug( log.debug(
"Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format( "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(
@ -1869,7 +1903,6 @@ class Instruction:
) )
if native_result: if native_result:
return native_result return native_result
transaction = MessageCallTransaction( transaction = MessageCallTransaction(
world_state=global_state.world_state, world_state=global_state.world_state,
gas_price=environment.gasprice, gas_price=environment.gasprice,

@ -0,0 +1,330 @@
from mythril.laser.ethereum.svm import LaserEVM
from mythril.laser.ethereum.plugins.plugin import LaserPlugin
from mythril.laser.ethereum.plugins.signals import PluginSkipState
from mythril.laser.ethereum.state.annotation import StateAnnotation
from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.laser.ethereum.transaction.transaction_models import (
ContractCreationTransaction,
)
from mythril.exceptions import UnsatError
from z3.z3types import Z3Exception
from mythril.analysis import solver
from typing import cast, List, Dict, Set
from copy import copy
import logging
log = logging.getLogger(__name__)
class DependencyAnnotation(StateAnnotation):
"""Dependency Annotation
This annotation tracks read and write access to the state during each transaction.
"""
def __init__(self):
self.storage_loaded = [] # type: List
self.storage_written = {} # type: Dict[int, List]
self.has_call = False
self.path = [0] # type: List
def __copy__(self):
result = DependencyAnnotation()
result.storage_loaded = copy(self.storage_loaded)
result.storage_written = copy(self.storage_written)
result.path = copy(self.path)
result.has_call = self.has_call
return result
def get_storage_write_cache(self, iteration: int):
if iteration not in self.storage_written:
self.storage_written[iteration] = []
return self.storage_written[iteration]
def extend_storage_write_cache(self, iteration: int, value: object):
if iteration not in self.storage_written:
self.storage_written[iteration] = [value]
else:
if value not in self.storage_written[iteration]:
self.storage_written[iteration].append(value)
class WSDependencyAnnotation(StateAnnotation):
"""Dependency Annotation for World state
This world state annotation maintains a stack of state annotations.
It is used to transfer individual state annotations from one transaction to the next.
"""
def __init__(self):
self.annotations_stack = []
def __copy__(self):
result = WSDependencyAnnotation()
result.annotations_stack = copy(self.annotations_stack)
return result
def get_dependency_annotation(state: GlobalState) -> DependencyAnnotation:
""" Returns a dependency annotation
:param state: A global state object
"""
annotations = cast(
List[DependencyAnnotation], list(state.get_annotations(DependencyAnnotation))
)
if len(annotations) == 0:
"""FIXME: Hack for carrying over state annotations from the STOP and RETURN states of
the previous states. The states are pushed on a stack in the world state annotation
and popped off the stack in the subsequent iteration. This might break if any
other strategy than bfs is used (?).
"""
try:
world_state_annotation = get_ws_dependency_annotation(state)
annotation = world_state_annotation.annotations_stack.pop()
except IndexError:
annotation = DependencyAnnotation()
state.annotate(annotation)
else:
annotation = annotations[0]
return annotation
def get_ws_dependency_annotation(state: GlobalState) -> WSDependencyAnnotation:
""" Returns the world state annotation
:param state: A global state object
"""
annotations = cast(
List[WSDependencyAnnotation],
list(state.world_state.get_annotations(WSDependencyAnnotation)),
)
if len(annotations) == 0:
annotation = WSDependencyAnnotation()
state.world_state.annotate(annotation)
else:
annotation = annotations[0]
return annotation
class DependencyPruner(LaserPlugin):
"""Dependency Pruner Plugin
For every basic block, this plugin keeps a list of storage locations that
are accessed (read) in the execution path containing that block. This map
is built up over the whole symbolic execution run.
After the initial build up of the map in the first transaction, blocks are
executed only if any of the storage locations written to in the previous
transaction can have an effect on that block or any of its successors.
"""
def __init__(self):
"""Creates DependencyPruner"""
self._reset()
def _reset(self):
self.iteration = 0
self.dependency_map = {} # type: Dict[int, List[object]]
self.protected_addresses = set() # type: Set[int]
def update_dependency_map(self, path: List[int], target_location: object) -> None:
"""Update the dependency map for the block offsets on the given path.
:param path
:param target_location
"""
try:
for address in path:
if address in self.dependency_map:
if target_location not in self.dependency_map[address]:
self.dependency_map[address].append(target_location)
else:
self.dependency_map[address] = [target_location]
except Z3Exception as e:
# This should not happen unless there's a bug in laser, such as an invalid type being generated.
log.debug("Error updating dependency map: {}".format(e))
def protect_path(self, path: List[int]) -> None:
"""Prevent an execution path of being pruned.
:param path
"""
for address in path:
self.protected_addresses.add(address)
def wanna_execute(self, address: int, storage_write_cache) -> bool:
"""Decide whether the basic block starting at 'address' should be executed.
:param address
:param storage_write_cache
"""
if address in self.protected_addresses or address not in self.dependency_map:
return True
dependencies = self.dependency_map[address]
# Return if *any* dependency is found
for location in storage_write_cache:
for dependency in dependencies:
try:
solver.get_model([location == dependency])
return True
except UnsatError:
continue
return False
def initialize(self, symbolic_vm: LaserEVM) -> None:
"""Initializes the DependencyPruner
:param symbolic_vm
"""
self._reset()
@symbolic_vm.laser_hook("start_sym_trans")
def start_sym_trans_hook():
self.iteration += 1
@symbolic_vm.post_hook("CALL")
def call_hook(state: GlobalState):
annotation = get_dependency_annotation(state)
annotation.has_call = True
self.protect_path(annotation.path)
@symbolic_vm.post_hook("JUMP")
def jump_hook(state: GlobalState):
address = state.get_current_instruction()["address"]
annotation = get_dependency_annotation(state)
_check_basic_block(address, annotation)
@symbolic_vm.pre_hook("JUMPDEST")
def jumpdest_hook(state: GlobalState):
address = state.get_current_instruction()["address"]
annotation = get_dependency_annotation(state)
_check_basic_block(address, annotation)
@symbolic_vm.post_hook("JUMPI")
def jumpi_hook(state: GlobalState):
address = state.get_current_instruction()["address"]
annotation = get_dependency_annotation(state)
_check_basic_block(address, annotation)
@symbolic_vm.pre_hook("SSTORE")
def sstore_hook(state: GlobalState):
annotation = get_dependency_annotation(state)
annotation.extend_storage_write_cache(
self.iteration, state.mstate.stack[-1]
)
@symbolic_vm.pre_hook("SLOAD")
def sload_hook(state: GlobalState):
annotation = get_dependency_annotation(state)
location = state.mstate.stack[-1]
if location not in annotation.storage_loaded:
annotation.storage_loaded.append(location)
# We backwards-annotate the path here as sometimes execution never reaches a stop or return
# (and this may change in a future transaction).
self.update_dependency_map(annotation.path, location)
@symbolic_vm.pre_hook("STOP")
def stop_hook(state: GlobalState):
_transaction_end(state)
@symbolic_vm.pre_hook("RETURN")
def return_hook(state: GlobalState):
_transaction_end(state)
def _transaction_end(state: GlobalState) -> None:
"""When a stop or return is reached, the storage locations read along the path are entered into
the dependency map for all nodes encountered in this path.
:param state:
"""
annotation = get_dependency_annotation(state)
if annotation.has_call:
self.protect_path(annotation.path)
for index in annotation.storage_loaded:
self.update_dependency_map(annotation.path, index)
def _check_basic_block(address: int, annotation: DependencyAnnotation):
"""This method is where the actual pruning happens.
:param address: Start address (bytecode offset) of the block
:param annotation
"""
# Don't skip any blocks in the contract creation transaction
if self.iteration < 2:
return
annotation.path.append(address)
if self.wanna_execute(
address, annotation.get_storage_write_cache(self.iteration - 1)
):
return
else:
log.debug(
"Skipping state: Storage slots {} not read in block at address {}".format(
annotation.get_storage_write_cache(self.iteration - 1), address
)
)
raise PluginSkipState
@symbolic_vm.laser_hook("add_world_state")
def world_state_filter_hook(state: GlobalState):
if isinstance(state.current_transaction, ContractCreationTransaction):
# Reset iteration variable
self.iteration = 0
return
world_state_annotation = get_ws_dependency_annotation(state)
annotation = get_dependency_annotation(state)
# Reset the state annotation except for storage written which is carried on to
# the next transaction
annotation.path = [0]
annotation.storage_loaded = []
annotation.has_call = False
world_state_annotation.annotations_stack.append(annotation)
log.debug(
"Iteration {}: Adding world state at address {}, end of function {}.\nDependency map: {}\nStorage written: {}".format(
self.iteration,
state.get_current_instruction()["address"],
state.node.function_name,
self.dependency_map,
annotation.storage_written[self.iteration],
)
)

@ -30,3 +30,12 @@ class PluginFactory:
) )
return InstructionCoveragePlugin() return InstructionCoveragePlugin()
@staticmethod
def build_dependency_pruner_plugin() -> LaserPlugin:
""" Creates an instance of the mutation pruner plugin"""
from mythril.laser.ethereum.plugins.implementations.dependency_pruner import (
DependencyPruner,
)
return DependencyPruner()

@ -15,3 +15,13 @@ class PluginSkipWorldState(PluginSignal):
""" """
pass pass
class PluginSkipState(PluginSignal):
""" Plugin to skip world state
Plugins that raise this signal while the add_world_state hook is being executed
will force laser to abandon that world state.
"""
pass

@ -38,7 +38,8 @@ class Storage:
self._storage[item] = symbol_factory.BitVecVal( self._storage[item] = symbol_factory.BitVecVal(
int( int(
self.dynld.read_storage( self.dynld.read_storage(
contract_address=self.address, index=int(item) contract_address=hex(self.address.value),
index=int(item),
), ),
16, 16,
), ),
@ -73,6 +74,9 @@ class Storage:
storage._storage = copy(self._storage) storage._storage = copy(self._storage)
return storage return storage
def __str__(self):
return str(self._storage)
class Account: class Account:
"""Account class representing ethereum accounts.""" """Account class representing ethereum accounts."""

@ -3,6 +3,7 @@ from copy import copy
from random import randint from random import randint
from typing import Dict, List, Iterator, Optional, TYPE_CHECKING from typing import Dict, List, Iterator, Optional, TYPE_CHECKING
from mythril.support.loader import DynLoader
from mythril.laser.smt import symbol_factory, Array, BitVec from mythril.laser.smt import symbol_factory, Array, BitVec
from ethereum.utils import mk_contract_address from ethereum.utils import mk_contract_address
from mythril.laser.ethereum.state.account import Account from mythril.laser.ethereum.state.account import Account
@ -64,6 +65,27 @@ class WorldState:
new_world_state.node = self.node new_world_state.node = self.node
return new_world_state return new_world_state
def accounts_exist_or_load(self, addr: str, dynamic_loader: DynLoader) -> str:
"""
returns account if it exists, else it loads from the dynamic loader
:param addr: address
:param dynamic_loader: Dynamic Loader
:return: The code
"""
addr_bitvec = symbol_factory.BitVecVal(int(addr, 16), 256)
if addr_bitvec.value in self.accounts:
code = self.accounts[addr_bitvec.value].code
else:
code = dynamic_loader.dynld(addr)
self.create_account(
balance=0, address=addr_bitvec.value, dynamic_loader=dynamic_loader
)
if code is None:
code = ""
else:
code = code.bytecode
return code
def create_account( def create_account(
self, self,
balance=0, balance=0,

@ -0,0 +1,84 @@
from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.laser.ethereum.strategy.basic import BasicSearchStrategy
from mythril.laser.ethereum.state.annotation import StateAnnotation
from mythril.laser.ethereum import util
from typing import Dict, cast, List
from copy import copy
import logging
log = logging.getLogger(__name__)
class JumpdestCountAnnotation(StateAnnotation):
"""State annotation that counts the number of jumps per destination."""
def __init__(self) -> None:
self._jumpdest_count = {} # type: Dict[int, int]
def __copy__(self):
result = JumpdestCountAnnotation()
result._jumpdest_count = copy(self._jumpdest_count)
return result
class BoundedLoopsStrategy(BasicSearchStrategy):
"""Adds loop pruning to the search strategy.
Ignores JUMPI instruction if the destination was targeted >JUMPDEST_LIMIT times.
"""
def __init__(self, super_strategy: BasicSearchStrategy, *args) -> None:
""""""
self.super_strategy = super_strategy
self.jumpdest_limit = args[0][0]
log.info(
"Loaded search strategy extension: Loop bounds (limit = {})".format(
self.jumpdest_limit
)
)
BasicSearchStrategy.__init__(
self, super_strategy.work_list, super_strategy.max_depth
)
def get_strategic_global_state(self) -> GlobalState:
"""
:return:
"""
while True:
state = self.super_strategy.get_strategic_global_state()
opcode = state.get_current_instruction()["opcode"]
if opcode != "JUMPI":
return state
annotations = cast(
List[JumpdestCountAnnotation],
list(state.get_annotations(JumpdestCountAnnotation)),
)
if len(annotations) == 0:
annotation = JumpdestCountAnnotation()
state.annotate(annotation)
else:
annotation = annotations[0]
try:
target = util.get_concrete_int(state.mstate.stack[-1])
except TypeError:
return state
try:
annotation._jumpdest_count[target] += 1
except KeyError:
annotation._jumpdest_count[target] = 1
if annotation._jumpdest_count[target] > self.jumpdest_limit:
log.debug("JUMPDEST limit reached, skipping JUMPI")
continue
return state

@ -10,10 +10,11 @@ from mythril.laser.ethereum.evm_exceptions import StackUnderflowException
from mythril.laser.ethereum.evm_exceptions import VmException from mythril.laser.ethereum.evm_exceptions import VmException
from mythril.laser.ethereum.instructions import Instruction from mythril.laser.ethereum.instructions import Instruction
from mythril.laser.ethereum.iprof import InstructionProfiler from mythril.laser.ethereum.iprof import InstructionProfiler
from mythril.laser.ethereum.plugins.signals import PluginSkipWorldState from mythril.laser.ethereum.plugins.signals import PluginSkipWorldState, PluginSkipState
from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.laser.ethereum.state.world_state import WorldState from mythril.laser.ethereum.state.world_state import WorldState
from mythril.laser.ethereum.strategy.basic import DepthFirstSearchStrategy from mythril.laser.ethereum.strategy.basic import DepthFirstSearchStrategy
from abc import ABCMeta
from mythril.laser.ethereum.time_handler import time_handler from mythril.laser.ethereum.time_handler import time_handler
from mythril.laser.ethereum.transaction import ( from mythril.laser.ethereum.transaction import (
ContractCreationTransaction, ContractCreationTransaction,
@ -68,6 +69,7 @@ class LaserEVM:
:param enable_iprof: Variable indicating whether instruction profiling should be turned on :param enable_iprof: Variable indicating whether instruction profiling should be turned on
""" """
self.open_states = [] # type: List[WorldState] self.open_states = [] # type: List[WorldState]
self.total_states = 0 self.total_states = 0
self.dynamic_loader = dynamic_loader self.dynamic_loader = dynamic_loader
@ -102,6 +104,9 @@ class LaserEVM:
log.info("LASER EVM initialized with dynamic loader: " + str(dynamic_loader)) log.info("LASER EVM initialized with dynamic loader: " + str(dynamic_loader))
def extend_strategy(self, extension: ABCMeta, *args) -> None:
self.strategy = extension(self.strategy, args)
def sym_exec( def sym_exec(
self, self,
world_state: WorldState = None, world_state: WorldState = None,
@ -121,7 +126,7 @@ class LaserEVM:
:param creation_code The creation code to create the target contract in the symbolic environment :param creation_code The creation code to create the target contract in the symbolic environment
:param contract_name The name that the created account should be associated with :param contract_name The name that the created account should be associated with
""" """
pre_configuration_mode = world_state is not None and target_address is not None pre_configuration_mode = target_address is not None
scratch_mode = creation_code is not None and contract_name is not None scratch_mode = creation_code is not None and contract_name is not None
if pre_configuration_mode == scratch_mode: if pre_configuration_mode == scratch_mode:
raise ValueError("Symbolic execution started with invalid parameters") raise ValueError("Symbolic execution started with invalid parameters")
@ -140,14 +145,16 @@ class LaserEVM:
elif scratch_mode: elif scratch_mode:
log.info("Starting contract creation transaction") log.info("Starting contract creation transaction")
created_account = execute_contract_creation( created_account = execute_contract_creation(
self, creation_code, contract_name self, creation_code, contract_name, world_state=world_state
) )
log.info( log.info(
"Finished contract creation, found {} open states".format( "Finished contract creation, found {} open states".format(
len(self.open_states) len(self.open_states)
) )
) )
if len(self.open_states) == 0: if len(self.open_states) == 0:
log.warning( log.warning(
"No contract was created during the execution of contract creation " "No contract was created during the execution of contract creation "
@ -267,7 +274,12 @@ class LaserEVM:
self._add_world_state(global_state) self._add_world_state(global_state)
return [], None return [], None
self._execute_pre_hook(op_code, global_state) try:
self._execute_pre_hook(op_code, global_state)
except PluginSkipState:
self._add_world_state(global_state)
return [], None
try: try:
new_global_states = Instruction( new_global_states = Instruction(
op_code, self.dynamic_loader, self.iprof op_code, self.dynamic_loader, self.iprof
@ -436,7 +448,11 @@ class LaserEVM:
environment = state.environment environment = state.environment
disassembly = environment.code disassembly = environment.code
if address in disassembly.address_to_function_name: if isinstance(
state.world_state.transaction_sequence[-1], ContractCreationTransaction
):
environment.active_function_name = "constructor"
elif address in disassembly.address_to_function_name:
# Enter a new function # Enter a new function
environment.active_function_name = disassembly.address_to_function_name[ environment.active_function_name = disassembly.address_to_function_name[
address address
@ -534,7 +550,10 @@ class LaserEVM:
for hook in self.post_hooks[op_code]: for hook in self.post_hooks[op_code]:
for global_state in global_states: for global_state in global_states:
hook(global_state) try:
hook(global_state)
except PluginSkipState:
global_states.remove(global_state)
def pre_hook(self, op_code: str) -> Callable: def pre_hook(self, op_code: str) -> Callable:
""" """

@ -88,7 +88,7 @@ def _setup_global_state_for_execution(laser_evm, transaction) -> None:
condition=None, condition=None,
) )
) )
global_state.world_state.transaction_sequence.append(transaction)
global_state.node = new_node global_state.node = new_node
new_node.states.append(global_state) new_node.states.append(global_state)
laser_evm.work_list.append(global_state) laser_evm.work_list.append(global_state)

@ -68,7 +68,7 @@ def execute_message_call(laser_evm, callee_address: BitVec) -> None:
def execute_contract_creation( def execute_contract_creation(
laser_evm, contract_initialization_code, contract_name=None laser_evm, contract_initialization_code, contract_name=None, world_state=None
) -> Account: ) -> Account:
"""Executes a contract creation transaction from all open states. """Executes a contract creation transaction from all open states.
@ -80,15 +80,9 @@ def execute_contract_creation(
# TODO: Resolve circular import between .transaction and ..svm to import LaserEVM here # TODO: Resolve circular import between .transaction and ..svm to import LaserEVM here
del laser_evm.open_states[:] del laser_evm.open_states[:]
world_state = WorldState() world_state = world_state or WorldState()
open_states = [world_state] open_states = [world_state]
new_account = world_state.create_account( new_account = None
0, concrete_storage=True, dynamic_loader=None, creator=CREATOR_ADDRESS
)
if contract_name:
new_account.contract_name = contract_name
for open_world_state in open_states: for open_world_state in open_states:
next_transaction_id = get_next_transaction_id() next_transaction_id = get_next_transaction_id()
transaction = ContractCreationTransaction( transaction = ContractCreationTransaction(
@ -103,13 +97,14 @@ def execute_contract_creation(
), ),
code=Disassembly(contract_initialization_code), code=Disassembly(contract_initialization_code),
caller=symbol_factory.BitVecVal(CREATOR_ADDRESS, 256), caller=symbol_factory.BitVecVal(CREATOR_ADDRESS, 256),
callee_account=new_account, contract_name=contract_name,
call_data=[], call_data=[],
call_value=symbol_factory.BitVecSym( call_value=symbol_factory.BitVecSym(
"call_value{}".format(next_transaction_id), 256 "call_value{}".format(next_transaction_id), 256
), ),
) )
_setup_global_state_for_execution(laser_evm, transaction) _setup_global_state_for_execution(laser_evm, transaction)
new_account = new_account or transaction.callee_account
laser_evm.exec(True) laser_evm.exec(True)
return new_account return new_account

@ -2,6 +2,7 @@
execution.""" execution."""
import array import array
from copy import deepcopy
from z3 import ExprRef from z3 import ExprRef
from typing import Union, Optional, cast from typing import Union, Optional, cast
@ -161,12 +162,37 @@ class MessageCallTransaction(BaseTransaction):
class ContractCreationTransaction(BaseTransaction): class ContractCreationTransaction(BaseTransaction):
"""Transaction object models an transaction.""" """Transaction object models an transaction."""
def __init__(self, *args, **kwargs) -> None: def __init__(
# Remove ignore after https://github.com/python/mypy/issues/4335 is fixed self,
super().__init__(*args, **kwargs, init_call_data=False) # type: ignore world_state: WorldState,
caller: ExprRef = None,
call_data=None,
identifier: Optional[str] = None,
gas_price=None,
gas_limit=None,
origin=None,
code=None,
call_value=None,
contract_name=None,
) -> None:
self.prev_world_state = deepcopy(world_state)
callee_account = world_state.create_account(
0, concrete_storage=True, creator=caller.value
)
callee_account.contract_name = contract_name
# TODO: set correct balance for new account # TODO: set correct balance for new account
self.callee_account = self.callee_account or self.world_state.create_account( super().__init__(
0, concrete_storage=True world_state=world_state,
callee_account=callee_account,
caller=caller,
call_data=call_data,
identifier=identifier,
gas_price=gas_price,
gas_limit=gas_limit,
origin=origin,
code=code,
call_value=call_value,
init_call_data=False,
) )
def initial_global_state(self) -> GlobalState: def initial_global_state(self) -> GlobalState:

@ -243,6 +243,13 @@ class BitVec(Expression[z3.BitVecRef]):
""" """
return self._handle_shift(other, rshift) return self._handle_shift(other, rshift)
def __hash__(self) -> int:
"""
:return:
"""
return self.raw.__hash__()
def _comparison_helper( def _comparison_helper(
a: BitVec, b: BitVec, operation: Callable, default_value: bool, inputs_equal: bool a: BitVec, b: BitVec, operation: Callable, default_value: bool, inputs_equal: bool

@ -35,8 +35,10 @@ class MythrilAnalyzer:
address: Optional[str] = None, address: Optional[str] = None,
max_depth: Optional[int] = None, max_depth: Optional[int] = None,
execution_timeout: Optional[int] = None, execution_timeout: Optional[int] = None,
loop_bound: Optional[int] = None,
create_timeout: Optional[int] = None, create_timeout: Optional[int] = None,
enable_iprof: bool = False, enable_iprof: bool = False,
disable_dependency_pruning: bool = False,
): ):
""" """
@ -53,8 +55,10 @@ class MythrilAnalyzer:
self.address = address self.address = address
self.max_depth = max_depth self.max_depth = max_depth
self.execution_timeout = execution_timeout self.execution_timeout = execution_timeout
self.loop_bound = loop_bound
self.create_timeout = create_timeout self.create_timeout = create_timeout
self.enable_iprof = enable_iprof self.enable_iprof = enable_iprof
self.disable_dependency_pruning = disable_dependency_pruning
def dump_statespace(self, contract: EVMContract = None) -> str: def dump_statespace(self, contract: EVMContract = None) -> str:
""" """
@ -75,6 +79,8 @@ class MythrilAnalyzer:
execution_timeout=self.execution_timeout, execution_timeout=self.execution_timeout,
create_timeout=self.create_timeout, create_timeout=self.create_timeout,
enable_iprof=self.enable_iprof, enable_iprof=self.enable_iprof,
disable_dependency_pruning=self.disable_dependency_pruning,
run_analysis_modules=False,
) )
return get_serializable_statespace(sym) return get_serializable_statespace(sym)
@ -108,6 +114,8 @@ class MythrilAnalyzer:
transaction_count=transaction_count, transaction_count=transaction_count,
create_timeout=self.create_timeout, create_timeout=self.create_timeout,
enable_iprof=self.enable_iprof, enable_iprof=self.enable_iprof,
disable_dependency_pruning=self.disable_dependency_pruning,
run_analysis_modules=False,
) )
return generate_graph(sym, physics=enable_physics, phrackify=phrackify) return generate_graph(sym, physics=enable_physics, phrackify=phrackify)
@ -140,12 +148,15 @@ class MythrilAnalyzer:
), ),
max_depth=self.max_depth, max_depth=self.max_depth,
execution_timeout=self.execution_timeout, execution_timeout=self.execution_timeout,
loop_bound=self.loop_bound,
create_timeout=self.create_timeout, create_timeout=self.create_timeout,
transaction_count=transaction_count, transaction_count=transaction_count,
modules=modules, modules=modules,
compulsory_statespace=False, compulsory_statespace=False,
enable_iprof=self.enable_iprof, enable_iprof=self.enable_iprof,
disable_dependency_pruning=self.disable_dependency_pruning,
) )
issues = fire_lasers(sym, modules) issues = fire_lasers(sym, modules)
except KeyboardInterrupt: except KeyboardInterrupt:
log.critical("Keyboard Interrupt") log.critical("Keyboard Interrupt")

@ -8,7 +8,7 @@ ethereum>=2.3.2
ethereum-input-decoder>=0.2.2 ethereum-input-decoder>=0.2.2
eth-hash>=0.1.0 eth-hash>=0.1.0
eth-keyfile>=0.5.1 eth-keyfile>=0.5.1
eth-keys>=0.2.0b3 eth-keys>=0.2.0b3,<0.3.0
eth-rlp>=0.1.0 eth-rlp>=0.1.0
eth-tester==0.1.0b32 eth-tester==0.1.0b32
eth-typing>=2.0.0 eth-typing>=2.0.0

@ -9,21 +9,82 @@ publish to pypi w/o having to convert Readme.md to RST:
""" """
from setuptools import setup, find_packages from setuptools import setup, find_packages
from setuptools.command.install import install from setuptools.command.install import install
from pathlib import Path
import sys import sys
import os import os
import io
# To make lint checkers happy we set VERSION here, but # Package meta-data.
# it is redefined by the exec below NAME = "mythril"
DESCRIPTION = "Security analysis tool for Ethereum smart contracts"
URL = "https://github.com/ConsenSys/mythril"
AUTHOR = "ConsenSys Dilligence"
AUTHOR_MAIL = None
REQUIRES_PYTHON = ">=3.5.0"
# What packages are required for this module to be executed?
REQUIRED = [
"coloredlogs>=10.0",
"py_ecc==1.4.2",
"ethereum>=2.3.2",
"z3-solver>=4.8.5.0",
"requests",
"py-solc",
"plyvel",
"eth_abi==1.3.0",
"eth-utils>=1.0.1",
"eth-account>=0.1.0a2,<=0.3.0",
"eth-hash>=0.1.0",
"eth-keyfile>=0.5.1",
"eth-keys>=0.2.0b3,<0.3.0",
"eth-rlp>=0.1.0",
"eth-tester==0.1.0b32",
"eth-typing>=2.0.0",
"coverage",
"jinja2>=2.9",
"rlp>=1.0.1",
"transaction>=2.2.1",
"py-flags",
"mock",
"configparser>=3.5.0",
"persistent>=4.2.0",
"ethereum-input-decoder>=0.2.2",
"matplotlib",
]
TESTS_REQUIRE = ["mypy", "pytest>=3.6.0", "pytest_mock", "pytest-cov"]
# What packages are optional?
EXTRAS = {
# 'fancy feature': ['django'],
}
# If version is set to None then it will be fetched from __version__.py
VERSION = None VERSION = None
# Package version (vX.Y.Z). It must match git tag being used for CircleCI here = os.path.abspath(os.path.dirname(__file__))
# deployment; otherwise the build will failed.
# Import the README and use it as the long-description.
# Note: this will only work if 'README.md' is present in your MANIFEST.in file!
try:
with io.open(os.path.join(here, "README.md"), encoding="utf-8") as f:
long_description = "\n" + f.read()
except FileNotFoundError:
long_description = DESCRIPTION
version_path = (Path(__file__).parent / "mythril" / "version.py").absolute()
exec(open(str(version_path), "r").read())
# Load the package's __version__.py module as a dictionary.
about = {}
if not VERSION:
project_slug = NAME.lower().replace("-", "_").replace(" ", "_")
with open(os.path.join(here, project_slug, "__version__.py")) as f:
exec(f.read(), about)
else:
about["__version__"] = VERSION
# Package version (vX.Y.Z). It must match git tag being used for CircleCI
# deployment; otherwise the build will failed.
class VerifyVersionCommand(install): class VerifyVersionCommand(install):
"""Custom command to verify that the git tag matches our version.""" """Custom command to verify that the git tag matches our version."""
@ -33,32 +94,22 @@ class VerifyVersionCommand(install):
"""""" """"""
tag = os.getenv("CIRCLE_TAG") tag = os.getenv("CIRCLE_TAG")
if tag != VERSION: if tag != about["__version__"]:
info = "Git tag: {0} does not match the version of this app: {1}".format( info = "Git tag: {0} does not match the version of this app: {1}".format(
tag, VERSION tag, about["__version__"]
) )
sys.exit(info) sys.exit(info)
def read_file(fname):
"""return file contents.
:param fname: path relative to setup.py
:return: file contents
"""
with open(os.path.join(os.path.dirname(__file__), fname), "r") as fd:
return fd.read()
setup( setup(
name="mythril", name=NAME,
version=VERSION[1:], version=about["__version__"][1:],
description="Security analysis tool for Ethereum smart contracts", description=DESCRIPTION,
long_description=read_file("README.md") if os.path.isfile("README.md") else "", long_description=long_description,
long_description_content_type="text/markdown", # requires twine and recent setuptools long_description_content_type="text/markdown", # requires twine and recent setuptools
url="https://github.com/b-mueller/mythril", url=URL,
author="Bernhard Mueller", author=AUTHOR,
author_email="bernhard.mueller11@gmail.com", author_mail=AUTHOR_MAIL,
license="MIT", license="MIT",
classifiers=[ classifiers=[
"Development Status :: 3 - Alpha", "Development Status :: 3 - Alpha",
@ -71,37 +122,10 @@ setup(
], ],
keywords="hacking disassembler security ethereum", keywords="hacking disassembler security ethereum",
packages=find_packages(exclude=["contrib", "docs", "tests"]), packages=find_packages(exclude=["contrib", "docs", "tests"]),
install_requires=[ install_requires=REQUIRED,
"coloredlogs>=10.0", tests_require=TESTS_REQUIRE,
"py_ecc==1.4.2", python_requires=REQUIRES_PYTHON,
"ethereum>=2.3.2", extras_require=EXTRAS,
"z3-solver>=4.8.5.0",
"requests",
"py-solc",
"plyvel",
"eth_abi==1.3.0",
"eth-utils>=1.0.1",
"eth-account>=0.1.0a2,<=0.3.0",
"eth-hash>=0.1.0",
"eth-keyfile>=0.5.1",
"eth-keys>=0.2.0b3",
"eth-rlp>=0.1.0",
"eth-tester==0.1.0b32",
"eth-typing>=2.0.0",
"coverage",
"jinja2>=2.9",
"rlp>=1.0.1",
"transaction>=2.2.1",
"py-flags",
"mock",
"configparser>=3.5.0",
"persistent>=4.2.0",
"ethereum-input-decoder>=0.2.2",
"matplotlib",
],
tests_require=["mypy", "pytest>=3.6.0", "pytest_mock", "pytest-cov"],
python_requires=">=3.5",
extras_require={},
package_data={"mythril.analysis.templates": ["*"], "mythril.support.assets": ["*"]}, package_data={"mythril.analysis.templates": ["*"], "mythril.support.assets": ["*"]},
include_package_data=True, include_package_data=True,
entry_points={"console_scripts": ["myth=mythril.interfaces.cli:main"]}, entry_points={"console_scripts": ["myth=mythril.interfaces.cli:main"]},

@ -8,7 +8,7 @@ import sys
def test_version_opt(capsys): def test_version_opt(capsys):
# Check that "myth --version" returns a string with the word # Check that "myth --version" returns a string with the word
# "version" in it # "version" in it
sys.argv = ["mythril", "--version"] sys.argv = ["mythril", "version"]
with pytest.raises(SystemExit) as pytest_wrapped_e: with pytest.raises(SystemExit) as pytest_wrapped_e:
main() main()
assert pytest_wrapped_e.type == SystemExit assert pytest_wrapped_e.type == SystemExit
@ -16,7 +16,7 @@ def test_version_opt(capsys):
assert captured.out.find(" version ") >= 1 assert captured.out.find(" version ") >= 1
# Check that "myth --version -o json" returns a JSON object # Check that "myth --version -o json" returns a JSON object
sys.argv = ["mythril", "--version", "-o", "json"] sys.argv = ["mythril", "version", "-o", "json"]
with pytest.raises(SystemExit) as pytest_wrapped_e: with pytest.raises(SystemExit) as pytest_wrapped_e:
main() main()
assert pytest_wrapped_e.type == SystemExit assert pytest_wrapped_e.type == SystemExit

@ -1,5 +1,6 @@
from subprocess import check_output from subprocess import check_output
from tests import BaseTestCase, TESTDATA, PROJECT_DIR, TESTS_DIR from tests import BaseTestCase, TESTDATA, PROJECT_DIR, TESTS_DIR
from mock import patch
MYTH = str(PROJECT_DIR / "myth") MYTH = str(PROJECT_DIR / "myth")
@ -15,23 +16,64 @@ def output_of(command):
class CommandLineToolTestCase(BaseTestCase): class CommandLineToolTestCase(BaseTestCase):
def test_disassemble_code_correctly(self): def test_disassemble_code_correctly(self):
command = "python3 {} MYTH -d --bin-runtime -c 0x5050 --solv 0.5.0".format(MYTH) command = "python3 {} disassemble --bin-runtime -c 0x5050".format(MYTH)
self.assertIn("0 POP\n1 POP\n", output_of(command)) self.assertIn("0 POP\n1 POP\n", output_of(command))
def test_disassemble_solidity_file_correctly(self): def test_disassemble_solidity_file_correctly(self):
solidity_file = str(TESTDATA / "input_contracts" / "metacoin.sol") solidity_file = str(TESTDATA / "input_contracts" / "metacoin.sol")
command = "python3 {} -d {} --solv 0.5.0".format(MYTH, solidity_file) command = "python3 {} disassemble {}".format(MYTH, solidity_file)
self.assertIn("2 PUSH1 0x40\n4 MSTORE", output_of(command)) self.assertIn("2 PUSH1 0x40\n4 MSTORE", output_of(command))
def test_hash_a_function_correctly(self): def test_hash_a_function_correctly(self):
command = "python3 {} --solv 0.5.0 --hash 'setOwner(address)'".format(MYTH) command = "python3 {} function-to-hash 'setOwner(address)'".format(MYTH)
self.assertIn("0x13af4035\n", output_of(command)) self.assertIn("0x13af4035\n", output_of(command))
def test_failure_json(self):
command = "python3 {} analyze doesnt_exist.sol -o json".format(MYTH)
print(output_of(command))
self.assertIn(""""success": false""", output_of(command))
def test_failure_text(self):
command = "python3 {} analyze doesnt_exist.sol".format(MYTH)
assert output_of(command) == ""
def test_failure_jsonv2(self):
command = "python3 {} analyze doesnt_exist.sol -o jsonv2".format(MYTH)
self.assertIn(""""level": "error""" "", output_of(command))
def test_analyze(self):
solidity_file = str(TESTDATA / "input_contracts" / "origin.sol")
command = "python3 {} analyze {}".format(MYTH, solidity_file)
self.assertIn("111", output_of(command))
def test_analyze_bytecode(self):
solidity_file = str(TESTDATA / "inputs" / "origin.sol.o")
command = "python3 {} analyze --bin-runtime -f {}".format(MYTH, solidity_file)
self.assertIn("111", output_of(command))
def test_invalid_args_iprof(self):
solidity_file = str(TESTDATA / "input_contracts" / "origin.sol")
command = "python3 {} analyze {} --enable-iprof -o json".format(
MYTH, solidity_file
)
self.assertIn(""""success": false""", output_of(command))
def test_only_epic(self):
command = "python3 {}".format(MYTH)
self.assertIn("usage: ", output_of(command))
def test_storage(self):
solidity_file = str(TESTDATA / "input_contracts" / "origin.sol")
command = """python3 {} read-storage "438767356, 3" 0x76799f77587738bfeef09452df215b63d2cfb08a """.format(
MYTH
)
self.assertIn("0x1a270efc", output_of(command))
class TruffleTestCase(BaseTestCase): class TruffleTestCase(BaseTestCase):
def test_analysis_truffle_project(self): def test_analysis_truffle_project(self):
truffle_project_root = str(TESTS_DIR / "truffle_project") truffle_project_root = str(TESTS_DIR / "truffle_project")
command = "cd {}; truffle compile; python3 {} --truffle -t 2".format( command = "cd {}; truffle compile; python3 {} truffle -t 2".format(
truffle_project_root, MYTH truffle_project_root, MYTH
) )
self.assertIn("=== Unprotected Ether Withdrawal ====", output_of(command)) self.assertIn("=== Unprotected Ether Withdrawal ====", output_of(command))
@ -39,7 +81,7 @@ class TruffleTestCase(BaseTestCase):
class InfuraTestCase(BaseTestCase): class InfuraTestCase(BaseTestCase):
def test_infura_mainnet(self): def test_infura_mainnet(self):
command = "python3 {} --rpc infura-mainnet -d -a 0x2a0c0dbecc7e4d658f48e01e3fa353f44050c208".format( command = "python3 {} disassemble --rpc infura-mainnet -a 0x2a0c0dbecc7e4d658f48e01e3fa353f44050c208".format(
MYTH MYTH
) )
output = output_of(command) output = output_of(command)
@ -47,21 +89,21 @@ class InfuraTestCase(BaseTestCase):
self.assertIn("7278 POP\n7279 POP\n7280 JUMP\n7281 STOP", output) self.assertIn("7278 POP\n7279 POP\n7280 JUMP\n7281 STOP", output)
def test_infura_rinkeby(self): def test_infura_rinkeby(self):
command = "python3 {} --rpc infura-rinkeby -d -a 0xB6f2bFED892a662bBF26258ceDD443f50Fa307F5".format( command = "python3 {} disassemble --rpc infura-rinkeby -a 0xB6f2bFED892a662bBF26258ceDD443f50Fa307F5".format(
MYTH MYTH
) )
output = output_of(command) output = output_of(command)
self.assertIn("34 JUMPDEST\n35 CALLVALUE", output) self.assertIn("34 JUMPDEST\n35 CALLVALUE", output)
def test_infura_kovan(self): def test_infura_kovan(self):
command = "python3 {} --rpc infura-kovan -d -a 0xE6bBF9B5A3451242F82f8cd458675092617a1235".format( command = "python3 {} disassemble --rpc infura-kovan -a 0xE6bBF9B5A3451242F82f8cd458675092617a1235".format(
MYTH MYTH
) )
output = output_of(command) output = output_of(command)
self.assertIn("9999 PUSH1 0x00\n10001 NOT\n10002 AND\n10003 PUSH1 0x00", output) self.assertIn("9999 PUSH1 0x00\n10001 NOT\n10002 AND\n10003 PUSH1 0x00", output)
def test_infura_ropsten(self): def test_infura_ropsten(self):
command = "python3 {} --rpc infura-ropsten -d -a 0x6e0E0e02377Bc1d90E8a7c21f12BA385C2C35f78".format( command = "python3 {} disassemble --rpc infura-ropsten -a 0x6e0E0e02377Bc1d90E8a7c21f12BA385C2C35f78".format(
MYTH MYTH
) )
output = output_of(command) output = output_of(command)

@ -0,0 +1,50 @@
import pytest
from mythril.disassembler.disassembly import Disassembly
from mythril.laser.ethereum.state.environment import Environment
from mythril.laser.ethereum.state.account import Account
from mythril.laser.ethereum.state.machine_state import MachineState
from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.laser.ethereum.state.world_state import WorldState
from mythril.support.loader import DynLoader
from mythril.ethereum.interface.rpc.client import EthJsonRpc
from mythril.laser.ethereum.instructions import Instruction
def _get_global_state():
active_account = Account("0x0", code=Disassembly("60606040"))
passive_account = Account(
"0x325345346564645654645", code=Disassembly("6060604061626364")
)
environment = Environment(active_account, None, None, None, None, None)
world_state = WorldState()
world_state.put_account(active_account)
world_state.put_account(passive_account)
return GlobalState(world_state, environment, None, MachineState(gas_limit=8000000))
@pytest.mark.parametrize(
"addr, eth, code_len",
[
(
"0xb09C477eCDAd49DD5Ac26c2C64914C3a6693843a",
EthJsonRpc("rinkeby.infura.io", 443, True),
1548,
),
(
"0x863DF6BFa4469f3ead0bE8f9F2AAE51c91A907b4",
EthJsonRpc("mainnet.infura.io", 443, True),
0,
),
(
"0x325345346564645654645",
EthJsonRpc("mainnet.infura.io", 443, True),
16,
), # This contract tests Address Cache
],
)
def test_extraction(addr, eth, code_len):
global_state = _get_global_state()
dynamic_loader = DynLoader(eth=eth)
code = global_state.world_state.accounts_exist_or_load(addr, dynamic_loader)
assert len(code) == code_len

@ -17,7 +17,8 @@ def _fix_path(text):
def _fix_debug_data(json_str): def _fix_debug_data(json_str):
read_json = json.loads(json_str) read_json = json.loads(json_str)
for issue in read_json["issues"]: for issue in read_json["issues"]:
issue["debug"] = "<DEBUG-DATA>" issue["tx_sequence"] = "<TX-DATA>"
return json.dumps(read_json, sort_keys=True, indent=4) return json.dumps(read_json, sort_keys=True, indent=4)
@ -25,6 +26,7 @@ def _add_jsonv2_stubs(json_str):
read_json = json.loads(json_str) read_json = json.loads(json_str)
for issue in read_json[0]["issues"]: for issue in read_json[0]["issues"]:
issue["extra"]["discoveryTime"] = "<DISCOVERY-TIME-DATA>" issue["extra"]["discoveryTime"] = "<DISCOVERY-TIME-DATA>"
issue["extra"]["testCase"] = "<TEST-CASE>"
return json.dumps(read_json, sort_keys=True, indent=4) return json.dumps(read_json, sort_keys=True, indent=4)

@ -4,7 +4,6 @@
{ {
"address": 661, "address": 661,
"contract": "Unknown", "contract": "Unknown",
"debug": "<DEBUG-DATA>",
"description": "A call to a user-supplied address is executed.\nThe 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.", "description": "A call to a user-supplied address is executed.\nThe 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.",
"function": "thisisfine()", "function": "thisisfine()",
"max_gas_used": 1254, "max_gas_used": 1254,
@ -12,12 +11,12 @@
"severity": "Medium", "severity": "Medium",
"sourceMap": null, "sourceMap": null,
"swc-id": "107", "swc-id": "107",
"title": "External Call To User-Supplied Address" "title": "External Call To User-Supplied Address",
"tx_sequence": "<TX-DATA>"
}, },
{ {
"address": 661, "address": 661,
"contract": "Unknown", "contract": "Unknown",
"debug": "<DEBUG-DATA>",
"description": "The return value of a message call is not checked.\nExternal 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.", "description": "The return value of a message call is not checked.\nExternal 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.",
"function": "thisisfine()", "function": "thisisfine()",
"max_gas_used": 35972, "max_gas_used": 35972,
@ -25,12 +24,12 @@
"severity": "Low", "severity": "Low",
"sourceMap": null, "sourceMap": null,
"swc-id": "104", "swc-id": "104",
"title": "Unchecked Call Return Value" "title": "Unchecked Call Return Value",
"tx_sequence": "<TX-DATA>"
}, },
{ {
"address": 779, "address": 779,
"contract": "Unknown", "contract": "Unknown",
"debug": "<DEBUG-DATA>",
"description": "A call to a user-supplied address is executed.\nThe 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.", "description": "A call to a user-supplied address is executed.\nThe 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.",
"function": "callstoredaddress()", "function": "callstoredaddress()",
"max_gas_used": 1298, "max_gas_used": 1298,
@ -38,12 +37,12 @@
"severity": "Medium", "severity": "Medium",
"sourceMap": null, "sourceMap": null,
"swc-id": "107", "swc-id": "107",
"title": "External Call To User-Supplied Address" "title": "External Call To User-Supplied Address",
"tx_sequence": "<TX-DATA>"
}, },
{ {
"address": 779, "address": 779,
"contract": "Unknown", "contract": "Unknown",
"debug": "<DEBUG-DATA>",
"description": "The return value of a message call is not checked.\nExternal 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.", "description": "The return value of a message call is not checked.\nExternal 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.",
"function": "callstoredaddress()", "function": "callstoredaddress()",
"max_gas_used": 36016, "max_gas_used": 36016,
@ -51,12 +50,12 @@
"severity": "Low", "severity": "Low",
"sourceMap": null, "sourceMap": null,
"swc-id": "104", "swc-id": "104",
"title": "Unchecked Call Return Value" "title": "Unchecked Call Return Value",
"tx_sequence": "<TX-DATA>"
}, },
{ {
"address": 858, "address": 858,
"contract": "Unknown", "contract": "Unknown",
"debug": "<DEBUG-DATA>",
"description": "A call to a user-supplied address is executed.\nThe 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.", "description": "A call to a user-supplied address is executed.\nThe 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.",
"function": "reentrancy()", "function": "reentrancy()",
"max_gas_used": 1320, "max_gas_used": 1320,
@ -64,12 +63,12 @@
"severity": "Medium", "severity": "Medium",
"sourceMap": null, "sourceMap": null,
"swc-id": "107", "swc-id": "107",
"title": "External Call To User-Supplied Address" "title": "External Call To User-Supplied Address",
"tx_sequence": "<TX-DATA>"
}, },
{ {
"address": 858, "address": 858,
"contract": "Unknown", "contract": "Unknown",
"debug": "<DEBUG-DATA>",
"description": "The return value of a message call is not checked.\nExternal 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.", "description": "The return value of a message call is not checked.\nExternal 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.",
"function": "reentrancy()", "function": "reentrancy()",
"max_gas_used": 61052, "max_gas_used": 61052,
@ -77,12 +76,12 @@
"severity": "Low", "severity": "Low",
"sourceMap": null, "sourceMap": null,
"swc-id": "104", "swc-id": "104",
"title": "Unchecked Call Return Value" "title": "Unchecked Call Return Value",
"tx_sequence": "<TX-DATA>"
}, },
{ {
"address": 869, "address": 869,
"contract": "Unknown", "contract": "Unknown",
"debug": "<DEBUG-DATA>",
"description": "The contract account state is changed after an external call. \nConsider that the called contract could re-enter the function before this state change takes place. This can lead to business logic vulnerabilities.", "description": "The contract account state is changed after an external call. \nConsider that the called contract could re-enter the function before this state change takes place. This can lead to business logic vulnerabilities.",
"function": "reentrancy()", "function": "reentrancy()",
"max_gas_used": null, "max_gas_used": null,
@ -90,12 +89,12 @@
"severity": "Medium", "severity": "Medium",
"sourceMap": null, "sourceMap": null,
"swc-id": "107", "swc-id": "107",
"title": "State change after external call" "title": "State change after external call",
"tx_sequence": "<TX-DATA>"
}, },
{ {
"address": 912, "address": 912,
"contract": "Unknown", "contract": "Unknown",
"debug": "<DEBUG-DATA>",
"description": "A call to a user-supplied address is executed.\nThe 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.", "description": "A call to a user-supplied address is executed.\nThe 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.",
"function": "calluseraddress(address)", "function": "calluseraddress(address)",
"max_gas_used": 616, "max_gas_used": 616,
@ -103,12 +102,12 @@
"severity": "Medium", "severity": "Medium",
"sourceMap": null, "sourceMap": null,
"swc-id": "107", "swc-id": "107",
"title": "External Call To User-Supplied Address" "title": "External Call To User-Supplied Address",
"tx_sequence": "<TX-DATA>"
}, },
{ {
"address": 912, "address": 912,
"contract": "Unknown", "contract": "Unknown",
"debug": "<DEBUG-DATA>",
"description": "The return value of a message call is not checked.\nExternal 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.", "description": "The return value of a message call is not checked.\nExternal 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.",
"function": "calluseraddress(address)", "function": "calluseraddress(address)",
"max_gas_used": 35336, "max_gas_used": 35336,
@ -116,7 +115,8 @@
"severity": "Low", "severity": "Low",
"sourceMap": null, "sourceMap": null,
"swc-id": "104", "swc-id": "104",
"title": "Unchecked Call Return Value" "title": "Unchecked Call Return Value",
"tx_sequence": "<TX-DATA>"
} }
], ],
"success": true "success": true

@ -7,7 +7,8 @@
"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." "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."
}, },
"extra": { "extra": {
"discoveryTime": "<DISCOVERY-TIME-DATA>" "discoveryTime": "<DISCOVERY-TIME-DATA>",
"testCase": "<TEST-CASE>"
}, },
"locations": [ "locations": [
{ {
@ -24,7 +25,8 @@
"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." "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."
}, },
"extra": { "extra": {
"discoveryTime": "<DISCOVERY-TIME-DATA>" "discoveryTime": "<DISCOVERY-TIME-DATA>",
"testCase": "<TEST-CASE>"
}, },
"locations": [ "locations": [
{ {
@ -41,7 +43,8 @@
"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." "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."
}, },
"extra": { "extra": {
"discoveryTime": "<DISCOVERY-TIME-DATA>" "discoveryTime": "<DISCOVERY-TIME-DATA>",
"testCase": "<TEST-CASE>"
}, },
"locations": [ "locations": [
{ {
@ -58,7 +61,8 @@
"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." "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."
}, },
"extra": { "extra": {
"discoveryTime": "<DISCOVERY-TIME-DATA>" "discoveryTime": "<DISCOVERY-TIME-DATA>",
"testCase": "<TEST-CASE>"
}, },
"locations": [ "locations": [
{ {
@ -75,7 +79,8 @@
"tail": "Consider that the called contract could re-enter the function before this state change takes place. This can lead to business logic vulnerabilities." "tail": "Consider that the called contract could re-enter the function before this state change takes place. This can lead to business logic vulnerabilities."
}, },
"extra": { "extra": {
"discoveryTime": "<DISCOVERY-TIME-DATA>" "discoveryTime": "<DISCOVERY-TIME-DATA>",
"testCase": "<TEST-CASE>"
}, },
"locations": [ "locations": [
{ {
@ -92,7 +97,8 @@
"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." "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."
}, },
"extra": { "extra": {
"discoveryTime": "<DISCOVERY-TIME-DATA>" "discoveryTime": "<DISCOVERY-TIME-DATA>",
"testCase": "<TEST-CASE>"
}, },
"locations": [ "locations": [
{ {
@ -109,7 +115,8 @@
"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." "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."
}, },
"extra": { "extra": {
"discoveryTime": "<DISCOVERY-TIME-DATA>" "discoveryTime": "<DISCOVERY-TIME-DATA>",
"testCase": "<TEST-CASE>"
}, },
"locations": [ "locations": [
{ {
@ -126,7 +133,8 @@
"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." "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."
}, },
"extra": { "extra": {
"discoveryTime": "<DISCOVERY-TIME-DATA>" "discoveryTime": "<DISCOVERY-TIME-DATA>",
"testCase": "<TEST-CASE>"
}, },
"locations": [ "locations": [
{ {
@ -143,7 +151,8 @@
"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." "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."
}, },
"extra": { "extra": {
"discoveryTime": "<DISCOVERY-TIME-DATA>" "discoveryTime": "<DISCOVERY-TIME-DATA>",
"testCase": "<TEST-CASE>"
}, },
"locations": [ "locations": [
{ {

@ -4,7 +4,6 @@
{ {
"address": 722, "address": 722,
"contract": "Unknown", "contract": "Unknown",
"debug": "<DEBUG-DATA>",
"description": "Anyone can withdraw ETH from the contract account.\nArbitrary 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.", "description": "Anyone can withdraw ETH from the contract account.\nArbitrary 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.",
"function": "withdrawfunds()", "function": "withdrawfunds()",
"max_gas_used": 1749, "max_gas_used": 1749,
@ -12,12 +11,12 @@
"severity": "High", "severity": "High",
"sourceMap": null, "sourceMap": null,
"swc-id": "105", "swc-id": "105",
"title": "Unprotected Ether Withdrawal" "title": "Unprotected Ether Withdrawal",
"tx_sequence": "<TX-DATA>"
}, },
{ {
"address": 883, "address": 883,
"contract": "Unknown", "contract": "Unknown",
"debug": "<DEBUG-DATA>",
"description": "The binary addition can overflow.\nThe operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion.", "description": "The binary addition can overflow.\nThe operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion.",
"function": "invest()", "function": "invest()",
"max_gas_used": 26883, "max_gas_used": 26883,
@ -25,7 +24,8 @@
"severity": "High", "severity": "High",
"sourceMap": null, "sourceMap": null,
"swc-id": "101", "swc-id": "101",
"title": "Integer Overflow" "title": "Integer Overflow",
"tx_sequence": "<TX-DATA>"
} }
], ],
"success": true "success": true

@ -7,7 +7,8 @@
"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." "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."
}, },
"extra": { "extra": {
"discoveryTime": "<DISCOVERY-TIME-DATA>" "discoveryTime": "<DISCOVERY-TIME-DATA>",
"testCase": "<TEST-CASE>"
}, },
"locations": [ "locations": [
{ {
@ -24,7 +25,8 @@
"tail": "The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion." "tail": "The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion."
}, },
"extra": { "extra": {
"discoveryTime": "<DISCOVERY-TIME-DATA>" "discoveryTime": "<DISCOVERY-TIME-DATA>",
"testCase": "<TEST-CASE>"
}, },
"locations": [ "locations": [
{ {

@ -4,7 +4,6 @@
{ {
"address": 446, "address": 446,
"contract": "Unknown", "contract": "Unknown",
"debug": "<DEBUG-DATA>",
"description": "A reachable exception has been detected.\nIt 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.", "description": "A reachable exception has been detected.\nIt 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.",
"function": "assert3(uint256)", "function": "assert3(uint256)",
"max_gas_used": 301, "max_gas_used": 301,
@ -12,12 +11,12 @@
"severity": "Low", "severity": "Low",
"sourceMap": null, "sourceMap": null,
"swc-id": "110", "swc-id": "110",
"title": "Exception State" "title": "Exception State",
"tx_sequence": "<TX-DATA>"
}, },
{ {
"address": 484, "address": 484,
"contract": "Unknown", "contract": "Unknown",
"debug": "<DEBUG-DATA>",
"description": "A reachable exception has been detected.\nIt 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.", "description": "A reachable exception has been detected.\nIt 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.",
"function": "arrayaccess(uint256)", "function": "arrayaccess(uint256)",
"max_gas_used": 351, "max_gas_used": 351,
@ -25,12 +24,12 @@
"severity": "Low", "severity": "Low",
"sourceMap": null, "sourceMap": null,
"swc-id": "110", "swc-id": "110",
"title": "Exception State" "title": "Exception State",
"tx_sequence": "<TX-DATA>"
}, },
{ {
"address": 506, "address": 506,
"contract": "Unknown", "contract": "Unknown",
"debug": "<DEBUG-DATA>",
"description": "A reachable exception has been detected.\nIt 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.", "description": "A reachable exception has been detected.\nIt 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.",
"function": "divisionby0(uint256)", "function": "divisionby0(uint256)",
"max_gas_used": 367, "max_gas_used": 367,
@ -38,12 +37,12 @@
"severity": "Low", "severity": "Low",
"sourceMap": null, "sourceMap": null,
"swc-id": "110", "swc-id": "110",
"title": "Exception State" "title": "Exception State",
"tx_sequence": "<TX-DATA>"
}, },
{ {
"address": 531, "address": 531,
"contract": "Unknown", "contract": "Unknown",
"debug": "<DEBUG-DATA>",
"description": "A reachable exception has been detected.\nIt 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.", "description": "A reachable exception has been detected.\nIt 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.",
"function": "assert1()", "function": "assert1()",
"max_gas_used": 363, "max_gas_used": 363,
@ -51,7 +50,8 @@
"severity": "Low", "severity": "Low",
"sourceMap": null, "sourceMap": null,
"swc-id": "110", "swc-id": "110",
"title": "Exception State" "title": "Exception State",
"tx_sequence": "<TX-DATA>"
} }
], ],
"success": true "success": true

@ -7,7 +7,8 @@
"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." "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."
}, },
"extra": { "extra": {
"discoveryTime": "<DISCOVERY-TIME-DATA>" "discoveryTime": "<DISCOVERY-TIME-DATA>",
"testCase": "<TEST-CASE>"
}, },
"locations": [ "locations": [
{ {
@ -24,7 +25,8 @@
"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." "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."
}, },
"extra": { "extra": {
"discoveryTime": "<DISCOVERY-TIME-DATA>" "discoveryTime": "<DISCOVERY-TIME-DATA>",
"testCase": "<TEST-CASE>"
}, },
"locations": [ "locations": [
{ {
@ -41,7 +43,8 @@
"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." "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."
}, },
"extra": { "extra": {
"discoveryTime": "<DISCOVERY-TIME-DATA>" "discoveryTime": "<DISCOVERY-TIME-DATA>",
"testCase": "<TEST-CASE>"
}, },
"locations": [ "locations": [
{ {
@ -58,7 +61,8 @@
"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." "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."
}, },
"extra": { "extra": {
"discoveryTime": "<DISCOVERY-TIME-DATA>" "discoveryTime": "<DISCOVERY-TIME-DATA>",
"testCase": "<TEST-CASE>"
}, },
"locations": [ "locations": [
{ {

@ -4,7 +4,6 @@
{ {
"address": 618, "address": 618,
"contract": "Unknown", "contract": "Unknown",
"debug": "<DEBUG-DATA>",
"description": "The return value of a message call is not checked.\nExternal 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.", "description": "The return value of a message call is not checked.\nExternal 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.",
"function": "_function_0x141f32ff", "function": "_function_0x141f32ff",
"max_gas_used": 35865, "max_gas_used": 35865,
@ -12,12 +11,12 @@
"severity": "Low", "severity": "Low",
"sourceMap": null, "sourceMap": null,
"swc-id": "104", "swc-id": "104",
"title": "Unchecked Call Return Value" "title": "Unchecked Call Return Value",
"tx_sequence": "<TX-DATA>"
}, },
{ {
"address": 618, "address": 618,
"contract": "Unknown", "contract": "Unknown",
"debug": "<DEBUG-DATA>",
"description": "Use of callcode is deprecated.\nThe 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.", "description": "Use of callcode is deprecated.\nThe 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.",
"function": "_function_0x141f32ff", "function": "_function_0x141f32ff",
"max_gas_used": 1141, "max_gas_used": 1141,
@ -25,12 +24,12 @@
"severity": "Medium", "severity": "Medium",
"sourceMap": null, "sourceMap": null,
"swc-id": "111", "swc-id": "111",
"title": "Use of callcode" "title": "Use of callcode",
"tx_sequence": "<TX-DATA>"
}, },
{ {
"address": 849, "address": 849,
"contract": "Unknown", "contract": "Unknown",
"debug": "<DEBUG-DATA>",
"description": "The contract delegates execution to another contract with a user-supplied address.\nThe smart contract delegates execution to a user-supplied address. Note that callers can execute arbitrary contracts and that the callee contract can access the storage of the calling contract. ", "description": "The contract delegates execution to another contract with a user-supplied address.\nThe smart contract delegates execution to a user-supplied address. Note that callers can execute arbitrary contracts and that the callee contract can access the storage of the calling contract. ",
"function": "_function_0x9b58bc26", "function": "_function_0x9b58bc26",
"max_gas_used": 35928, "max_gas_used": 35928,
@ -38,12 +37,12 @@
"severity": "Medium", "severity": "Medium",
"sourceMap": null, "sourceMap": null,
"swc-id": "112", "swc-id": "112",
"title": "Delegatecall Proxy To User-Supplied Address" "title": "Delegatecall Proxy To User-Supplied Address",
"tx_sequence": "<TX-DATA>"
}, },
{ {
"address": 849, "address": 849,
"contract": "Unknown", "contract": "Unknown",
"debug": "<DEBUG-DATA>",
"description": "The return value of a message call is not checked.\nExternal 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.", "description": "The return value of a message call is not checked.\nExternal 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.",
"function": "_function_0x9b58bc26", "function": "_function_0x9b58bc26",
"max_gas_used": 35928, "max_gas_used": 35928,
@ -51,12 +50,12 @@
"severity": "Low", "severity": "Low",
"sourceMap": null, "sourceMap": null,
"swc-id": "104", "swc-id": "104",
"title": "Unchecked Call Return Value" "title": "Unchecked Call Return Value",
"tx_sequence": "<TX-DATA>"
}, },
{ {
"address": 1038, "address": 1038,
"contract": "Unknown", "contract": "Unknown",
"debug": "<DEBUG-DATA>",
"description": "A call to a user-supplied address is executed.\nThe 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.", "description": "A call to a user-supplied address is executed.\nThe 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.",
"function": "_function_0xeea4c864", "function": "_function_0xeea4c864",
"max_gas_used": 1229, "max_gas_used": 1229,
@ -64,12 +63,12 @@
"severity": "Medium", "severity": "Medium",
"sourceMap": null, "sourceMap": null,
"swc-id": "107", "swc-id": "107",
"title": "External Call To User-Supplied Address" "title": "External Call To User-Supplied Address",
"tx_sequence": "<TX-DATA>"
}, },
{ {
"address": 1038, "address": 1038,
"contract": "Unknown", "contract": "Unknown",
"debug": "<DEBUG-DATA>",
"description": "The return value of a message call is not checked.\nExternal 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.", "description": "The return value of a message call is not checked.\nExternal 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.",
"function": "_function_0xeea4c864", "function": "_function_0xeea4c864",
"max_gas_used": 35953, "max_gas_used": 35953,
@ -77,7 +76,8 @@
"severity": "Low", "severity": "Low",
"sourceMap": null, "sourceMap": null,
"swc-id": "104", "swc-id": "104",
"title": "Unchecked Call Return Value" "title": "Unchecked Call Return Value",
"tx_sequence": "<TX-DATA>"
} }
], ],
"success": true "success": true

@ -7,7 +7,8 @@
"tail": "The smart contract delegates execution to a user-supplied address. Note that callers can execute arbitrary contracts and that the callee contract can access the storage of the calling contract. " "tail": "The smart contract delegates execution to a user-supplied address. Note that callers can execute arbitrary contracts and that the callee contract can access the storage of the calling contract. "
}, },
"extra": { "extra": {
"discoveryTime": "<DISCOVERY-TIME-DATA>" "discoveryTime": "<DISCOVERY-TIME-DATA>",
"testCase": "<TEST-CASE>"
}, },
"locations": [ "locations": [
{ {
@ -24,7 +25,8 @@
"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." "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."
}, },
"extra": { "extra": {
"discoveryTime": "<DISCOVERY-TIME-DATA>" "discoveryTime": "<DISCOVERY-TIME-DATA>",
"testCase": "<TEST-CASE>"
}, },
"locations": [ "locations": [
{ {
@ -41,7 +43,8 @@
"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." "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."
}, },
"extra": { "extra": {
"discoveryTime": "<DISCOVERY-TIME-DATA>" "discoveryTime": "<DISCOVERY-TIME-DATA>",
"testCase": "<TEST-CASE>"
}, },
"locations": [ "locations": [
{ {
@ -58,7 +61,8 @@
"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." "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."
}, },
"extra": { "extra": {
"discoveryTime": "<DISCOVERY-TIME-DATA>" "discoveryTime": "<DISCOVERY-TIME-DATA>",
"testCase": "<TEST-CASE>"
}, },
"locations": [ "locations": [
{ {
@ -75,7 +79,8 @@
"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." "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."
}, },
"extra": { "extra": {
"discoveryTime": "<DISCOVERY-TIME-DATA>" "discoveryTime": "<DISCOVERY-TIME-DATA>",
"testCase": "<TEST-CASE>"
}, },
"locations": [ "locations": [
{ {
@ -92,7 +97,8 @@
"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." "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."
}, },
"extra": { "extra": {
"discoveryTime": "<DISCOVERY-TIME-DATA>" "discoveryTime": "<DISCOVERY-TIME-DATA>",
"testCase": "<TEST-CASE>"
}, },
"locations": [ "locations": [
{ {

@ -4,7 +4,6 @@
{ {
"address": 142, "address": 142,
"contract": "Unknown", "contract": "Unknown",
"debug": "<DEBUG-DATA>",
"description": "Anyone can withdraw ETH from the contract account.\nArbitrary 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.", "description": "Anyone can withdraw ETH from the contract account.\nArbitrary 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.",
"function": "transfer()", "function": "transfer()",
"max_gas_used": 467, "max_gas_used": 467,
@ -12,7 +11,8 @@
"severity": "High", "severity": "High",
"sourceMap": null, "sourceMap": null,
"swc-id": "105", "swc-id": "105",
"title": "Unprotected Ether Withdrawal" "title": "Unprotected Ether Withdrawal",
"tx_sequence": "<TX-DATA>"
} }
], ],
"success": true "success": true

@ -7,7 +7,8 @@
"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." "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."
}, },
"extra": { "extra": {
"discoveryTime": "<DISCOVERY-TIME-DATA>" "discoveryTime": "<DISCOVERY-TIME-DATA>",
"testCase": "<TEST-CASE>"
}, },
"locations": [ "locations": [
{ {

@ -4,7 +4,6 @@
{ {
"address": 317, "address": 317,
"contract": "Unknown", "contract": "Unknown",
"debug": "<DEBUG-DATA>",
"description": "Use of tx.origin is deprecated.\nThe 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", "description": "Use of tx.origin is deprecated.\nThe 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",
"function": "transferOwnership(address)", "function": "transferOwnership(address)",
"max_gas_used": 1051, "max_gas_used": 1051,
@ -12,7 +11,8 @@
"severity": "Medium", "severity": "Medium",
"sourceMap": null, "sourceMap": null,
"swc-id": "111", "swc-id": "111",
"title": "Use of tx.origin" "title": "Use of tx.origin",
"tx_sequence": "<TX-DATA>"
} }
], ],
"success": true "success": true

@ -7,7 +7,8 @@
"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" "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"
}, },
"extra": { "extra": {
"discoveryTime": "<DISCOVERY-TIME-DATA>" "discoveryTime": "<DISCOVERY-TIME-DATA>",
"testCase": "<TEST-CASE>"
}, },
"locations": [ "locations": [
{ {

@ -4,7 +4,6 @@
{ {
"address": 567, "address": 567,
"contract": "Unknown", "contract": "Unknown",
"debug": "<DEBUG-DATA>",
"description": "The binary subtraction can underflow.\nThe operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.", "description": "The binary subtraction can underflow.\nThe operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.",
"function": "sendeth(address,uint256)", "function": "sendeth(address,uint256)",
"max_gas_used": 78155, "max_gas_used": 78155,
@ -12,12 +11,12 @@
"severity": "High", "severity": "High",
"sourceMap": null, "sourceMap": null,
"swc-id": "101", "swc-id": "101",
"title": "Integer Underflow" "title": "Integer Underflow",
"tx_sequence": "<TX-DATA>"
}, },
{ {
"address": 649, "address": 649,
"contract": "Unknown", "contract": "Unknown",
"debug": "<DEBUG-DATA>",
"description": "The binary subtraction can underflow.\nThe operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.", "description": "The binary subtraction can underflow.\nThe operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.",
"function": "sendeth(address,uint256)", "function": "sendeth(address,uint256)",
"max_gas_used": 78155, "max_gas_used": 78155,
@ -25,12 +24,12 @@
"severity": "High", "severity": "High",
"sourceMap": null, "sourceMap": null,
"swc-id": "101", "swc-id": "101",
"title": "Integer Underflow" "title": "Integer Underflow",
"tx_sequence": "<TX-DATA>"
}, },
{ {
"address": 725, "address": 725,
"contract": "Unknown", "contract": "Unknown",
"debug": "<DEBUG-DATA>",
"description": "The binary addition can overflow.\nThe operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion.", "description": "The binary addition can overflow.\nThe operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion.",
"function": "sendeth(address,uint256)", "function": "sendeth(address,uint256)",
"max_gas_used": 78155, "max_gas_used": 78155,
@ -38,7 +37,8 @@
"severity": "High", "severity": "High",
"sourceMap": null, "sourceMap": null,
"swc-id": "101", "swc-id": "101",
"title": "Integer Overflow" "title": "Integer Overflow",
"tx_sequence": "<TX-DATA>"
} }
], ],
"success": true "success": true

@ -7,7 +7,8 @@
"tail": "The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion." "tail": "The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion."
}, },
"extra": { "extra": {
"discoveryTime": "<DISCOVERY-TIME-DATA>" "discoveryTime": "<DISCOVERY-TIME-DATA>",
"testCase": "<TEST-CASE>"
}, },
"locations": [ "locations": [
{ {
@ -24,7 +25,8 @@
"tail": "The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion." "tail": "The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion."
}, },
"extra": { "extra": {
"discoveryTime": "<DISCOVERY-TIME-DATA>" "discoveryTime": "<DISCOVERY-TIME-DATA>",
"testCase": "<TEST-CASE>"
}, },
"locations": [ "locations": [
{ {
@ -41,7 +43,8 @@
"tail": "The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion." "tail": "The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion."
}, },
"extra": { "extra": {
"discoveryTime": "<DISCOVERY-TIME-DATA>" "discoveryTime": "<DISCOVERY-TIME-DATA>",
"testCase": "<TEST-CASE>"
}, },
"locations": [ "locations": [
{ {

@ -4,7 +4,6 @@
{ {
"address": 196, "address": 196,
"contract": "Unknown", "contract": "Unknown",
"debug": "<DEBUG-DATA>",
"description": "A call to a user-supplied address is executed.\nThe 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.", "description": "A call to a user-supplied address is executed.\nThe 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.",
"function": "callchecked()", "function": "callchecked()",
"max_gas_used": 1210, "max_gas_used": 1210,
@ -12,12 +11,12 @@
"severity": "Medium", "severity": "Medium",
"sourceMap": null, "sourceMap": null,
"swc-id": "107", "swc-id": "107",
"title": "External Call To User-Supplied Address" "title": "External Call To User-Supplied Address",
"tx_sequence": "<TX-DATA>"
}, },
{ {
"address": 285, "address": 285,
"contract": "Unknown", "contract": "Unknown",
"debug": "<DEBUG-DATA>",
"description": "A call to a user-supplied address is executed.\nThe 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.", "description": "A call to a user-supplied address is executed.\nThe 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.",
"function": "callnotchecked()", "function": "callnotchecked()",
"max_gas_used": 1232, "max_gas_used": 1232,
@ -25,12 +24,12 @@
"severity": "Medium", "severity": "Medium",
"sourceMap": null, "sourceMap": null,
"swc-id": "107", "swc-id": "107",
"title": "External Call To User-Supplied Address" "title": "External Call To User-Supplied Address",
"tx_sequence": "<TX-DATA>"
}, },
{ {
"address": 285, "address": 285,
"contract": "Unknown", "contract": "Unknown",
"debug": "<DEBUG-DATA>",
"description": "The return value of a message call is not checked.\nExternal 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.", "description": "The return value of a message call is not checked.\nExternal 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.",
"function": "callnotchecked()", "function": "callnotchecked()",
"max_gas_used": 35950, "max_gas_used": 35950,
@ -38,7 +37,8 @@
"severity": "Low", "severity": "Low",
"sourceMap": null, "sourceMap": null,
"swc-id": "104", "swc-id": "104",
"title": "Unchecked Call Return Value" "title": "Unchecked Call Return Value",
"tx_sequence": "<TX-DATA>"
} }
], ],
"success": true "success": true

@ -7,7 +7,8 @@
"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." "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."
}, },
"extra": { "extra": {
"discoveryTime": "<DISCOVERY-TIME-DATA>" "discoveryTime": "<DISCOVERY-TIME-DATA>",
"testCase": "<TEST-CASE>"
}, },
"locations": [ "locations": [
{ {
@ -24,7 +25,8 @@
"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." "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."
}, },
"extra": { "extra": {
"discoveryTime": "<DISCOVERY-TIME-DATA>" "discoveryTime": "<DISCOVERY-TIME-DATA>",
"testCase": "<TEST-CASE>"
}, },
"locations": [ "locations": [
{ {
@ -41,7 +43,8 @@
"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." "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."
}, },
"extra": { "extra": {
"discoveryTime": "<DISCOVERY-TIME-DATA>" "discoveryTime": "<DISCOVERY-TIME-DATA>",
"testCase": "<TEST-CASE>"
}, },
"locations": [ "locations": [
{ {

@ -4,7 +4,6 @@
{ {
"address": 146, "address": 146,
"contract": "Unknown", "contract": "Unknown",
"debug": "<DEBUG-DATA>",
"description": "The contract can be killed by anyone.\nAnyone can kill this contract and withdraw its balance to an arbitrary address.", "description": "The contract can be killed by anyone.\nAnyone can kill this contract and withdraw its balance to an arbitrary address.",
"function": "kill(address)", "function": "kill(address)",
"max_gas_used": 263, "max_gas_used": 263,
@ -12,7 +11,8 @@
"severity": "High", "severity": "High",
"sourceMap": null, "sourceMap": null,
"swc-id": "106", "swc-id": "106",
"title": "Unprotected Selfdestruct" "title": "Unprotected Selfdestruct",
"tx_sequence": "<TX-DATA>"
} }
], ],
"success": true "success": true

@ -7,7 +7,8 @@
"tail": "Anyone can kill this contract and withdraw its balance to an arbitrary address." "tail": "Anyone can kill this contract and withdraw its balance to an arbitrary address."
}, },
"extra": { "extra": {
"discoveryTime": "<DISCOVERY-TIME-DATA>" "discoveryTime": "<DISCOVERY-TIME-DATA>",
"testCase": "<TEST-CASE>"
}, },
"locations": [ "locations": [
{ {

@ -4,7 +4,6 @@
{ {
"address": 567, "address": 567,
"contract": "Unknown", "contract": "Unknown",
"debug": "<DEBUG-DATA>",
"description": "The binary subtraction can underflow.\nThe operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.", "description": "The binary subtraction can underflow.\nThe operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.",
"function": "sendeth(address,uint256)", "function": "sendeth(address,uint256)",
"max_gas_used": 52861, "max_gas_used": 52861,
@ -12,12 +11,12 @@
"severity": "High", "severity": "High",
"sourceMap": null, "sourceMap": null,
"swc-id": "101", "swc-id": "101",
"title": "Integer Underflow" "title": "Integer Underflow",
"tx_sequence": "<TX-DATA>"
}, },
{ {
"address": 649, "address": 649,
"contract": "Unknown", "contract": "Unknown",
"debug": "<DEBUG-DATA>",
"description": "The binary subtraction can underflow.\nThe operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.", "description": "The binary subtraction can underflow.\nThe operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.",
"function": "sendeth(address,uint256)", "function": "sendeth(address,uint256)",
"max_gas_used": 52861, "max_gas_used": 52861,
@ -25,12 +24,12 @@
"severity": "High", "severity": "High",
"sourceMap": null, "sourceMap": null,
"swc-id": "101", "swc-id": "101",
"title": "Integer Underflow" "title": "Integer Underflow",
"tx_sequence": "<TX-DATA>"
}, },
{ {
"address": 725, "address": 725,
"contract": "Unknown", "contract": "Unknown",
"debug": "<DEBUG-DATA>",
"description": "The binary addition can overflow.\nThe operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion.", "description": "The binary addition can overflow.\nThe operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion.",
"function": "sendeth(address,uint256)", "function": "sendeth(address,uint256)",
"max_gas_used": 52861, "max_gas_used": 52861,
@ -38,7 +37,8 @@
"severity": "High", "severity": "High",
"sourceMap": null, "sourceMap": null,
"swc-id": "101", "swc-id": "101",
"title": "Integer Overflow" "title": "Integer Overflow",
"tx_sequence": "<TX-DATA>"
} }
], ],
"success": true "success": true

@ -7,7 +7,8 @@
"tail": "The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion." "tail": "The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion."
}, },
"extra": { "extra": {
"discoveryTime": "<DISCOVERY-TIME-DATA>" "discoveryTime": "<DISCOVERY-TIME-DATA>",
"testCase": "<TEST-CASE>"
}, },
"locations": [ "locations": [
{ {
@ -24,7 +25,8 @@
"tail": "The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion." "tail": "The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion."
}, },
"extra": { "extra": {
"discoveryTime": "<DISCOVERY-TIME-DATA>" "discoveryTime": "<DISCOVERY-TIME-DATA>",
"testCase": "<TEST-CASE>"
}, },
"locations": [ "locations": [
{ {
@ -41,7 +43,8 @@
"tail": "The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion." "tail": "The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion."
}, },
"extra": { "extra": {
"discoveryTime": "<DISCOVERY-TIME-DATA>" "discoveryTime": "<DISCOVERY-TIME-DATA>",
"testCase": "<TEST-CASE>"
}, },
"locations": [ "locations": [
{ {

Loading…
Cancel
Save