Merge remote-tracking branch 'origin/develop' into feature/laser_plugins

pull/1353/head
Joran Honig 5 years ago
commit ba564ce437
  1. 94
      .circleci/config.yml
  2. 2
      README.md
  3. 4
      mythril/__init__.py
  4. 2
      mythril/__version__.py
  5. 30
      mythril/analysis/analysis_args.py
  6. 4
      mythril/analysis/module/loader.py
  7. 13
      mythril/analysis/module/modules/arbitrary_jump.py
  8. 11
      mythril/analysis/module/modules/arbitrary_write.py
  9. 16
      mythril/analysis/module/modules/delegatecall.py
  10. 112
      mythril/analysis/module/modules/dependence_on_origin.py
  11. 95
      mythril/analysis/module/modules/dependence_on_predictable_vars.py
  12. 90
      mythril/analysis/module/modules/deprecated_ops.py
  13. 52
      mythril/analysis/module/modules/ether_thief.py
  14. 16
      mythril/analysis/module/modules/exceptions.py
  15. 54
      mythril/analysis/module/modules/external_calls.py
  16. 34
      mythril/analysis/module/modules/integer.py
  17. 7
      mythril/analysis/module/modules/multiple_sends.py
  18. 21
      mythril/analysis/module/modules/state_change_external_calls.py
  19. 17
      mythril/analysis/module/modules/suicide.py
  20. 11
      mythril/analysis/module/modules/unchecked_retval.py
  21. 4
      mythril/analysis/module/modules/user_assertions.py
  22. 46
      mythril/analysis/solver.py
  23. 17
      mythril/interfaces/cli.py
  24. 4
      mythril/laser/ethereum/state/account.py
  25. 40
      mythril/laser/ethereum/state/constraints.py
  26. 52
      mythril/laser/ethereum/strategy/extensions/bounded_loops.py
  27. 12
      mythril/laser/ethereum/svm.py
  28. 14
      mythril/laser/ethereum/transaction/symbolic.py
  29. 37
      mythril/laser/plugin/plugins/mutation_pruner.py
  30. 10
      mythril/mythril/mythril_analyzer.py
  31. 21
      mythril/plugin/discovery.py
  32. 49
      mythril/support/model.py
  33. 13
      mythril/support/support_args.py
  34. 4
      tests/cmd_line_test.py
  35. 2
      tests/graph_test.py
  36. 3
      tests/laser/evm_testsuite/evm_test.py
  37. 20
      tests/laser/strategy/test_loop_bound.py
  38. 1
      tests/statespace_test.py

@ -78,45 +78,45 @@ jobs:
# command: if [ -z "$CIRCLE_PR_NUMBER" ]; then ./run-integration-tests.sh; fi
# working_directory: /home
integration_tests:
docker:
- image: circleci/python:3.6.4
working_directory: ~/project
steps:
- checkout
- setup_remote_docker
- run:
name: Clone Edelweiss
command: git clone --recurse-submodules https://$GITHUB_TOKEN@github.com/Consensys/Edelweiss.git
- run:
name: Update SWC-registry
working_directory: ~/project/Edelweiss
command: git submodule update --recursive --remote
- run:
name: Build Edelweiss
command: |
docker build \
--build-arg AWS_ACCESS_KEY_ID=$S3_AWS_ACCESS_KEY_ID \
--build-arg AWS_SECRET_ACCESS_KEY=$S3_AWS_SECRET_ACCESS_KEY \
--build-arg AWS_DEFAULT_REGION=us-east-1 --rm -t "edelweiss-mythril:latest" . -f Edelweiss/dockerfiles/mythril/Dockerfile
- run:
name: Run Edelweiss
command: |
docker run \
-e CIRCLE_BRANCH=$CIRCLE_BRANCH \
-e CIRCLE_SHA1=$CIRCLE_SHA1 \
-e CIRCLE_BUILD_NUM=$CIRCLE_BUILD_NUM \
-e CIRCLE_BUILD_URL=$CIRCLE_BUILD_URL \
-e CIRCLE_WEBHOOK_URL=$CIRCLE_WEBHOOK_URL \
-e MONGO_URL=$MONGO_URL \
--rm edelweiss-mythril:latest \
--timeout 90 \
--output-dir /opt/edelweiss \
--s3 \
--dynamodb \
--circle-ci CircleCI/mythril.csv \
--ignore-false-positives $IGNORE_FALSE_POSITIVES \
--ignore-regressions $IGNORE_REGRESSIONS
# integration_tests:
# docker:
# - image: circleci/python:3.6.4
# working_directory: ~/project
# steps:
# - checkout
# - setup_remote_docker
# - run:
# name: Clone Edelweiss
# command: git clone --recurse-submodules https://$GITHUB_TOKEN@github.com/Consensys/Edelweiss.git
# - run:
# name: Update SWC-registry
# working_directory: ~/project/Edelweiss
# command: git submodule update --recursive --remote
# - run:
# name: Build Edelweiss
# command: |
# docker build \
# --build-arg AWS_ACCESS_KEY_ID=$S3_AWS_ACCESS_KEY_ID \
# --build-arg AWS_SECRET_ACCESS_KEY=$S3_AWS_SECRET_ACCESS_KEY \
# --build-arg AWS_DEFAULT_REGION=us-east-1 --rm -t "edelweiss-mythril:latest" . -f Edelweiss/dockerfiles/mythril/Dockerfile
# - run:
# name: Run Edelweiss
# command: |
# docker run \
# -e CIRCLE_BRANCH=$CIRCLE_BRANCH \
# -e CIRCLE_SHA1=$CIRCLE_SHA1 \
# -e CIRCLE_BUILD_NUM=$CIRCLE_BUILD_NUM \
# -e CIRCLE_BUILD_URL=$CIRCLE_BUILD_URL \
# -e CIRCLE_WEBHOOK_URL=$CIRCLE_WEBHOOK_URL \
# -e MONGO_URL=$MONGO_URL \
# --rm edelweiss-mythril:latest \
# --timeout 90 \
# --output-dir /opt/edelweiss \
# --s3 \
# --dynamodb \
# --circle-ci CircleCI/mythril.csv \
# --ignore-false-positives $IGNORE_FALSE_POSITIVES \
# --ignore-regressions $IGNORE_REGRESSIONS
pypi_release:
<<: *defaults
@ -167,16 +167,6 @@ workflows:
filters:
tags:
only: /.*/
- integration_tests:
filters:
branches:
only:
- develop
- master
tags:
only: /v[0-9]+(\.[0-9]+)*/
requires:
- test
- pypi_release:
filters:
branches:
@ -184,13 +174,13 @@ workflows:
tags:
only: /v[0-9]+(\.[0-9]+)*/
requires:
- integration_tests
- test
- dockerhub_dev_release:
filters:
branches:
only: develop
requires:
- integration_tests
- test
- dockerhub_release:
filters:
branches:
@ -198,4 +188,4 @@ workflows:
tags:
only: /v[0-9]+(\.[0-9]+)*/
requires:
- integration_tests
- test

@ -12,7 +12,7 @@
[![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)
Mythril is a security analysis tool for EVM bytecode. It detects security vulnerabilities in smart contracts built for Ethereum, Hedera, Quorum, Vechain, Roostock, Tron and other EVM-compatible blockchains. It uses symbolic execution, SMT solving and taint analysis detect a variety of security vulnerabilities. It's also used (in combination with other tools and techniques) in the [MythX](https://mythx.io) security analysis platform.
Mythril is a security analysis tool for EVM bytecode. It detects security vulnerabilities in smart contracts built for Ethereum, Hedera, Quorum, Vechain, Roostock, Tron and other EVM-compatible blockchains. It uses symbolic execution, SMT solving and taint analysis to detect a variety of security vulnerabilities. It's also used (in combination with other tools and techniques) in the [MythX](https://mythx.io) security analysis platform.
If you are a smart contract developer, we recommend using [MythX tools](https://github.com/b-mueller/awesome-mythx-smart-contract-security-tools) which are optimized for usability and cover a wider range of security issues.

@ -8,7 +8,3 @@ from .__version__ import __version__ as VERSION # NOQA
from mythril.plugin.loader import MythrilPluginLoader
log = logging.getLogger(__name__)
# Initialise core Mythril Components
log.info("Initializing core Mythril components")
_ = MythrilPluginLoader()

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

@ -1,30 +0,0 @@
from mythril.support.support_utils import Singleton
class AnalysisArgs(object, metaclass=Singleton):
"""
This module helps in preventing args being sent through multiple of classes to reach analysis modules
"""
def __init__(self):
self._loop_bound = 3
self._solver_timeout = 10000
def set_loop_bound(self, loop_bound: int):
if loop_bound is not None:
self._loop_bound = loop_bound
def set_solver_timeout(self, solver_timeout: int):
if solver_timeout is not None:
self._solver_timeout = solver_timeout
@property
def loop_bound(self):
return self._loop_bound
@property
def solver_timeout(self):
return self._solver_timeout
analysis_args = AnalysisArgs()

@ -7,7 +7,7 @@ from mythril.analysis.module.modules.delegatecall import ArbitraryDelegateCall
from mythril.analysis.module.modules.dependence_on_predictable_vars import (
PredictableVariables,
)
from mythril.analysis.module.modules.deprecated_ops import DeprecatedOperations
from mythril.analysis.module.modules.dependence_on_origin import TxOrigin
from mythril.analysis.module.modules.ether_thief import EtherThief
from mythril.analysis.module.modules.exceptions import Exceptions
from mythril.analysis.module.modules.external_calls import ExternalCalls
@ -88,7 +88,7 @@ class ModuleLoader(object, metaclass=Singleton):
ArbitraryStorage(),
ArbitraryDelegateCall(),
PredictableVariables(),
DeprecatedOperations(),
TxOrigin(),
EtherThief(),
Exceptions(),
ExternalCalls(),

@ -14,9 +14,9 @@ Search for jumps to arbitrary locations in the bytecode
class ArbitraryJump(DetectionModule):
"""This module searches for JUMPs to an arbitrary instruction."""
"""This module searches for JUMPs to a user-specified location."""
name = "Jump to an arbitrary bytecode location"
name = "Caller can redirect execution to arbitrary bytecode locations"
swc_id = ARBITRARY_JUMP
description = DESCRIPTION
entry_point = EntryPoint.CALLBACK
@ -63,11 +63,12 @@ class ArbitraryJump(DetectionModule):
address=state.get_current_instruction()["address"],
swc_id=ARBITRARY_JUMP,
title="Jump to an arbitrary instruction",
severity="Medium",
severity="High",
bytecode=state.environment.code.bytecode,
description_head="The caller can jump to any point in the code.",
description_tail="This can lead to unintended consequences."
"Please avoid using low level code as much as possible",
description_head="The caller can redirect execution to arbitrary bytecode locations.",
description_tail="It is possible to redirect the control flow to arbitrary locations in the code. "
"This may allow an attacker to bypass security controls or manipulate the business logic of the "
"smart contract. Avoid using low-level-operations and assembly to prevent this issue.",
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
transaction_sequence=transaction_sequence,
)

@ -21,7 +21,7 @@ Search for any writes to an arbitrary storage slot
class ArbitraryStorage(DetectionModule):
"""This module searches for a feasible write to an arbitrary storage slot."""
name = "Write to an arbitrary storage location"
name = "Caller can write to arbitrary storage locations"
swc_id = WRITE_TO_ARBITRARY_STORAGE
description = DESCRIPTION
entry_point = EntryPoint.CALLBACK
@ -64,12 +64,13 @@ class ArbitraryStorage(DetectionModule):
function_name=state.environment.active_function_name,
address=state.get_current_instruction()["address"],
swc_id=WRITE_TO_ARBITRARY_STORAGE,
title="Write to an arbitrary storage slot",
title="Write to an arbitrary storage location",
severity="High",
bytecode=state.environment.code.bytecode,
description_head="Any storage slot can be written by the caller.",
description_tail="The attacker can modify any value in the storage."
+ " This can lead to unintended consequences.",
description_head="The caller can write to arbitrary storage locations.",
description_tail="It is possible to write to arbitrary storage locations. By modifying the values of "
"storage variables, attackers may bypass security controls or manipulate the business logic of "
"the smart contract.",
detector=self,
constraints=constraints,
)

@ -20,13 +20,11 @@ log = logging.getLogger(__name__)
class ArbitraryDelegateCall(DetectionModule):
"""This module detects calldata being forwarded using DELEGATECALL."""
"""This module detects delegatecall to a user-supplied address."""
name = "Delegatecall to a user-specified address"
swc_id = DELEGATECALL_TO_UNTRUSTED_CONTRACT
description = (
"Check for invocations of delegatecall(msg.data) in the fallback function."
)
description = "Check for invocations of delegatecall to a user-supplied address."
entry_point = EntryPoint.CALLBACK
pre_hooks = ["DELEGATECALL"]
@ -75,9 +73,9 @@ class ArbitraryDelegateCall(DetectionModule):
description_head = "The contract delegates execution to another contract with a user-supplied address."
description_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. "
"The smart contract delegates execution to a user-supplied address.This could allow an attacker to "
"execute arbitrary code in the context of this contract account and manipulate the state of the "
"contract account or execute actions on its behalf."
)
return [
@ -87,8 +85,8 @@ class ArbitraryDelegateCall(DetectionModule):
address=address,
swc_id=DELEGATECALL_TO_UNTRUSTED_CONTRACT,
bytecode=state.environment.code.bytecode,
title="Delegatecall Proxy To User-Supplied Address",
severity="Medium",
title="Delegatecall to user-supplied address",
severity="High",
description_head=description_head,
description_tail=description_tail,
constraints=constraints,

@ -0,0 +1,112 @@
"""This module contains the detection code for predictable variable
dependence."""
import logging
from copy import copy
from mythril.analysis.module.base import DetectionModule, EntryPoint
from mythril.analysis.report import Issue
from mythril.exceptions import UnsatError
from mythril.analysis import solver
from mythril.analysis.swc_data import TX_ORIGIN_USAGE
from mythril.laser.ethereum.state.global_state import GlobalState
from typing import List
log = logging.getLogger(__name__)
class TxOriginAnnotation:
"""Symbol annotation added to a variable that is initialized with a call to the ORIGIN instruction."""
def __init__(self) -> None:
pass
class TxOrigin(DetectionModule):
"""This module detects whether control flow decisions are made based on the transaction origin."""
name = "Control flow depends on tx.origin"
swc_id = TX_ORIGIN_USAGE
description = "Check whether control flow decisions are influenced by tx.origin"
entry_point = EntryPoint.CALLBACK
pre_hooks = ["JUMPI"]
post_hooks = ["ORIGIN"]
def _execute(self, state: GlobalState) -> None:
"""
:param state:
:return:
"""
if state.get_current_instruction()["address"] in self.cache:
return
issues = self._analyze_state(state)
for issue in issues:
self.cache.add(issue.address)
self.issues.extend(issues)
@staticmethod
def _analyze_state(state: GlobalState) -> list:
"""
:param state:
:return:
"""
issues = []
if state.get_current_instruction()["opcode"] == "JUMPI":
# We're in JUMPI prehook
for annotation in state.mstate.stack[-2].annotations:
if isinstance(annotation, TxOriginAnnotation):
constraints = copy(state.world_state.constraints)
try:
transaction_sequence = solver.get_transaction_sequence(
state, constraints
)
except UnsatError:
continue
description = (
"The tx.origin environment variable has been found to influence a control flow decision. "
"Note that using tx.origin as a security control might cause a situation where a user "
"inadvertently authorizes a smart contract to perform an action on their behalf. It is "
"recommended to use msg.sender instead."
)
severity = "Low"
"""
Note: We report the location of the JUMPI instruction. Usually this maps to an if or
require statement.
"""
issue = Issue(
contract=state.environment.active_account.contract_name,
function_name=state.environment.active_function_name,
address=state.get_current_instruction()["address"],
swc_id=TX_ORIGIN_USAGE,
bytecode=state.environment.code.bytecode,
title="Dependence on tx.origin",
severity=severity,
description_head="Use of tx.origin as a part of authorization control.",
description_tail=description,
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
transaction_sequence=transaction_sequence,
)
issues.append(issue)
else:
# In ORIGIN posthook
state.mstate.stack[-1].annotate(TxOriginAnnotation())
return issues
detector = TxOrigin()

@ -17,31 +17,19 @@ from typing import cast, List
log = logging.getLogger(__name__)
predictable_ops = ["COINBASE", "GASLIMIT", "TIMESTAMP", "NUMBER"]
final_ops = ["CALL", "SUICIDE", "STOP", "RETURN"]
class PredictableValueAnnotation:
"""Symbol annotation used if a variable is initialized from a predictable environment variable."""
def __init__(self, operation: str, add_constraints=None) -> None:
def __init__(self, operation: str) -> None:
self.operation = operation
self.add_constraints = add_constraints
class PredictablePathAnnotation(StateAnnotation):
"""State annotation used when a path is chosen based on a predictable variable."""
def __init__(self, operation: str, location: int, add_constraints=None) -> None:
self.operation = operation
self.location = location
self.add_constraints = add_constraints
class OldBlockNumberUsedAnnotation(StateAnnotation):
"""State annotation set in blockhash prehook if the input value is lower than the current block number."""
"""Symbol annotation used if a variable is initialized from a predictable environment variable."""
def __init__(self, constraints) -> None:
self.block_constraints = constraints
def __init__(self) -> None:
pass
@ -52,11 +40,11 @@ class PredictableVariables(DetectionModule):
name = "Control flow depends on a predictable environment variable"
swc_id = "{} {}".format(TIMESTAMP_DEPENDENCE, WEAK_RANDOMNESS)
description = (
"Check whether important control flow decisions are influenced by block.coinbase,"
"Check whether control flow decisions are influenced by block.coinbase,"
"block.gaslimit, block.timestamp or block.number."
)
entry_point = EntryPoint.CALLBACK
pre_hooks = ["BLOCKHASH", "JUMPI"] + final_ops
pre_hooks = ["JUMPI", "BLOCKHASH"]
post_hooks = ["BLOCKHASH"] + predictable_ops
def _execute(self, state: GlobalState) -> None:
@ -86,18 +74,15 @@ class PredictableVariables(DetectionModule):
opcode = state.get_current_instruction()["opcode"]
if opcode in final_ops:
if opcode == "JUMPI":
for annotation in state.annotations:
# Look for predictable state variables in jump condition
if isinstance(annotation, PredictablePathAnnotation):
if annotation.add_constraints:
constraints = (
state.world_state.constraints
+ annotation.add_constraints
)
else:
constraints = copy(state.world_state.constraints)
for annotation in state.mstate.stack[-2].annotations:
if isinstance(annotation, PredictableValueAnnotation):
constraints = state.world_state.constraints
try:
transaction_sequence = solver.get_transaction_sequence(
state, constraints
@ -105,15 +90,15 @@ class PredictableVariables(DetectionModule):
except UnsatError:
continue
description = (
"The "
+ annotation.operation
+ " is used in to determine a control flow decision. "
annotation.operation
+ " is used to determine a control flow decision. "
)
description += (
"Note that the values of variables like coinbase, gaslimit, block number and timestamp "
"are predictable and can be manipulated by a malicious miner. Also keep in mind that attackers "
"know hashes of earlier blocks. Don't use any of those environment variables for random number "
"generation or to make critical control flow decisions."
"Note that the values of variables like coinbase, gaslimit, block number and timestamp are "
"predictable and can be manipulated by a malicious miner. Also keep in mind that "
"attackers know hashes of earlier blocks. Don't use any of those environment variables "
"as sources of randomness and be aware that use of these variables introduces "
"a certain level of trust into miners."
)
"""
@ -121,12 +106,7 @@ class PredictableVariables(DetectionModule):
determine control flow.
"""
severity = "Medium" if "hash" in annotation.operation else "Low"
"""
Note: We report the location of the JUMPI that lead to this path. Usually this maps to an if or
require statement.
"""
severity = "Low"
swc_id = (
TIMESTAMP_DEPENDENCE
@ -137,12 +117,14 @@ class PredictableVariables(DetectionModule):
issue = Issue(
contract=state.environment.active_account.contract_name,
function_name=state.environment.active_function_name,
address=annotation.location,
address=state.get_current_instruction()["address"],
swc_id=swc_id,
bytecode=state.environment.code.bytecode,
title="Dependence on predictable environment variable",
severity=severity,
description_head="A control flow decision is made based on a predictable variable.",
description_head="A control flow decision is made based on {}.".format(
annotation.operation
),
description_tail=description,
gas_used=(
state.mstate.min_gas_used,
@ -153,27 +135,10 @@ class PredictableVariables(DetectionModule):
issues.append(issue)
elif opcode == "JUMPI":
# Look for predictable state variables in jump condition
for annotation in state.mstate.stack[-2].annotations:
if isinstance(annotation, PredictableValueAnnotation):
state.annotate(
PredictablePathAnnotation(
annotation.operation,
state.get_current_instruction()["address"],
add_constraints=annotation.add_constraints,
)
)
break
elif opcode == "BLOCKHASH":
param = state.mstate.stack[-1]
try:
constraint = [
ULT(param, state.environment.block_number),
ULT(
@ -184,10 +149,13 @@ class PredictableVariables(DetectionModule):
# Why the second constraint? Because without it Z3 returns a solution where param overflows.
try:
solver.get_model(
state.world_state.constraints + constraint # type: ignore
)
state.annotate(OldBlockNumberUsedAnnotation(constraint))
state.annotate(OldBlockNumberUsedAnnotation())
except UnsatError:
pass
@ -210,17 +178,14 @@ class PredictableVariables(DetectionModule):
if len(annotations):
# We can append any block constraint here
state.mstate.stack[-1].annotate(
PredictableValueAnnotation(
"block hash of a previous block",
add_constraints=annotations[0].block_constraints,
)
PredictableValueAnnotation("The block hash of a previous block")
)
else:
# Always create an annotation when COINBASE, GASLIMIT, TIMESTAMP or NUMBER is executed.
state.mstate.stack[-1].annotate(
PredictableValueAnnotation(
"block.{} environment variable".format(opcode.lower())
"The block.{} environment variable".format(opcode.lower())
)
)

@ -1,90 +0,0 @@
"""This module contains the detection code for deprecated op codes."""
from mythril.analysis.potential_issues import (
PotentialIssue,
get_potential_issues_annotation,
)
from mythril.analysis.swc_data import DEPRECATED_FUNCTIONS_USAGE
from mythril.analysis.module.base import DetectionModule, EntryPoint
from mythril.laser.ethereum.state.global_state import GlobalState
import logging
log = logging.getLogger(__name__)
DESCRIPTION = """
Check for usage of deprecated opcodes
"""
class DeprecatedOperations(DetectionModule):
"""This module checks for the usage of deprecated op codes."""
name = "Usage of deprecated instructions"
swc_id = DEPRECATED_FUNCTIONS_USAGE
description = DESCRIPTION
entry_point = EntryPoint.CALLBACK
pre_hooks = ["ORIGIN", "CALLCODE"]
def _execute(self, state: GlobalState) -> None:
"""
:param state:
:return:
"""
if state.get_current_instruction()["address"] in self.cache:
return
issues = self._analyze_state(state)
annotation = get_potential_issues_annotation(state)
annotation.potential_issues.extend(issues)
def _analyze_state(self, state):
"""
:param state:
:return:
"""
node = state.node
instruction = state.get_current_instruction()
if instruction["opcode"] == "ORIGIN":
log.debug("ORIGIN in function " + node.function_name)
title = "Use of tx.origin"
description_head = "Use of tx.origin is deprecated."
description_tail = (
"The smart contract retrieves the transaction origin (tx.origin) using msg.origin. "
"Use of msg.origin is deprecated and the instruction may be removed in the future. "
"Use msg.sender instead.\nSee also: "
"https://solidity.readthedocs.io/en/develop/security-considerations.html#tx-origin"
)
swc_id = DEPRECATED_FUNCTIONS_USAGE
elif instruction["opcode"] == "CALLCODE":
log.debug("CALLCODE in function " + state.environment.active_function_name)
title = "Use of callcode"
description_head = "Use of callcode is deprecated."
description_tail = (
"The callcode method executes code of another contract in the context of the caller account. "
"Due to a bug in the implementation it does not persist sender and value over the call. It was "
"therefore deprecated and may be removed in the future. Use the delegatecall method instead."
)
swc_id = DEPRECATED_FUNCTIONS_USAGE
else:
return []
potential_issue = PotentialIssue(
contract=state.environment.active_account.contract_name,
function_name=state.environment.active_function_name,
address=instruction["address"],
title=title,
bytecode=state.environment.code.bytecode,
detector=self,
swc_id=swc_id,
severity="Medium",
description_head=description_head,
description_tail=description_tail,
constraints=[],
)
return [potential_issue]
detector = DeprecatedOperations()

@ -11,24 +11,16 @@ from mythril.analysis.potential_issues import (
from mythril.laser.ethereum.transaction.symbolic import ACTORS
from mythril.analysis.swc_data import UNPROTECTED_ETHER_WITHDRAWAL
from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.laser.ethereum.transaction import ContractCreationTransaction
from mythril.laser.smt import UGT, UGE
from mythril.laser.smt.bool import And
from mythril.analysis import solver
from mythril.exceptions import UnsatError
from mythril.laser.smt import UGT
log = logging.getLogger(__name__)
DESCRIPTION = """
Search for cases where Ether can be withdrawn to a user-specified address.
An issue is reported if:
- The transaction sender does not match contract creator;
- The sender address can be chosen arbitrarily;
- The receiver address is identical to the sender address;
- The sender can withdraw *more* than the total amount they sent over all transactions.
An issue is reported if there is a valid end state where the attacker has successfully
increased their Ether balance.
"""
@ -36,11 +28,11 @@ class EtherThief(DetectionModule):
"""This module search for cases where Ether can be withdrawn to a user-
specified address."""
name = "Attacker can profitably withdraw Ether from the contract account"
name = "Any sender can withdraw ETH from the contract account"
swc_id = UNPROTECTED_ETHER_WITHDRAWAL
description = DESCRIPTION
entry_point = EntryPoint.CALLBACK
pre_hooks = ["STOP"]
post_hooks = ["CALL", "STATICCALL"]
def reset_module(self):
"""
@ -51,7 +43,6 @@ class EtherThief(DetectionModule):
def _execute(self, state: GlobalState) -> None:
"""
:param state:
:return:
"""
@ -64,7 +55,6 @@ class EtherThief(DetectionModule):
def _analyze_state(self, state):
"""
:param state:
:return:
"""
@ -73,32 +63,40 @@ class EtherThief(DetectionModule):
constraints = copy(state.world_state.constraints)
attacker_address_bitvec = ACTORS.attacker
constraints += [
UGT(
state.world_state.balances[attacker_address_bitvec],
state.world_state.starting_balances[attacker_address_bitvec],
)
state.world_state.balances[ACTORS.attacker],
state.world_state.starting_balances[ACTORS.attacker],
),
state.environment.sender == ACTORS.attacker,
state.current_transaction.caller == state.current_transaction.origin,
]
try:
# Pre-solve so we only add potential issues if the attacker's balance is increased.
solver.get_model(constraints)
potential_issue = PotentialIssue(
contract=state.environment.active_account.contract_name,
function_name=state.environment.active_function_name,
address=instruction["address"],
address=instruction["address"]
- 1, # In post hook we use offset of previous instruction
swc_id=UNPROTECTED_ETHER_WITHDRAWAL,
title="Unprotected Ether Withdrawal",
severity="High",
bytecode=state.environment.code.bytecode,
description_head="Anyone can withdraw ETH from the contract account.",
description_tail="Arbitrary senders other than the contract creator can withdraw ETH from the contract"
+ " account without previously having sent an equivalent amount of ETH to it. This is likely to be"
+ " a vulnerability.",
description_head="Any sender can withdraw Ether from the contract account.",
description_tail="Arbitrary senders other than the contract creator can profitably extract Ether "
"from the contract account. Verify the business logic carefully and make sure that appropriate "
"security controls are in place to prevent unexpected loss of funds.",
detector=self,
constraints=constraints,
)
return [potential_issue]
except UnsatError:
return []
detector = EtherThief()

@ -14,7 +14,7 @@ log = logging.getLogger(__name__)
class Exceptions(DetectionModule):
""""""
name = "Exception or assertion violation"
name = "Assertion violation"
swc_id = ASSERT_VIOLATION
description = "Checks whether any exception states are reachable."
entry_point = EntryPoint.CALLBACK
@ -46,11 +46,11 @@ class Exceptions(DetectionModule):
address = state.get_current_instruction()["address"]
description_tail = (
"It is possible to trigger an exception (opcode 0xfe). "
"Exceptions can be caused by type errors, division by zero, "
"out-of-bounds array access, or assert violations. "
"Note that explicit `assert()` should only be used to check invariants. "
"Use `require()` for regular input checking."
"It is possible to trigger an assertion violation. Note that Solidity assert() statements should "
"only be used to check invariants. Review the transaction trace generated for this issue and "
"either make sure your program logic is correct, or use require() instead of assert() if your goal "
"is to constrain user inputs or enforce preconditions. Remember to validate inputs from both callers "
"(for instance, via passed arguments) and callees (for instance, via return values)."
)
transaction_sequence = solver.get_transaction_sequence(
state, state.world_state.constraints
@ -61,8 +61,8 @@ class Exceptions(DetectionModule):
address=address,
swc_id=ASSERT_VIOLATION,
title="Exception State",
severity="Low",
description_head="A reachable exception has been detected.",
severity="Medium",
description_head="An assertion violation was triggered.",
description_tail=description_tail,
bytecode=state.environment.code.bytecode,
transaction_sequence=transaction_sequence,

@ -21,9 +21,7 @@ log = logging.getLogger(__name__)
DESCRIPTION = """
Search for low level calls (e.g. call.value()) that forward all gas to the callee.
Report a warning if the callee address can be set by the sender, otherwise create
an informational issue.
Search for external calls with unrestricted gas to a user-specified address.
"""
@ -78,27 +76,21 @@ class ExternalCalls(DetectionModule):
address = state.get_current_instruction()["address"]
try:
constraints = Constraints([UGT(gas, symbol_factory.BitVecVal(2300, 256))])
solver.get_transaction_sequence(
state, constraints + state.world_state.constraints
constraints = Constraints(
[UGT(gas, symbol_factory.BitVecVal(2300, 256)), to == ACTORS.attacker]
)
# Check whether we can also set the callee address
try:
new_constraints = constraints + [to == ACTORS.attacker]
solver.get_transaction_sequence(
state, new_constraints + state.world_state.constraints
state, constraints + state.world_state.constraints
)
description_head = "A call to a user-supplied address is executed."
description_tail = (
"The callee address of an external message call can be set by "
"the caller. Note that the callee can contain arbitrary code and may re-enter any function "
"in this contract. Review the business logic carefully to prevent averse effects on the "
"contract state."
"An external message call to an address specified by the caller is executed. Note that "
"the callee account might contain arbitrary code and could re-enter any function "
"within this contract. Reentering the contract in an intermediate state may lead to "
"unexpected behaviour. Make sure that no state modifications "
"are executed after this call and/or reentrancy guards are in place."
)
issue = PotentialIssue(
@ -108,34 +100,6 @@ class ExternalCalls(DetectionModule):
swc_id=REENTRANCY,
title="External Call To User-Supplied Address",
bytecode=state.environment.code.bytecode,
severity="Medium",
description_head=description_head,
description_tail=description_tail,
constraints=new_constraints,
detector=self,
)
except UnsatError:
if _is_precompile_call(state):
return []
log.debug(
"[EXTERNAL_CALLS] Callee address cannot be modified. Reporting informational issue."
)
description_head = "The contract executes an external message call."
description_tail = (
"An external function call to a fixed contract address is executed. Make sure "
"that the callee contract has been reviewed carefully."
)
issue = PotentialIssue(
contract=state.environment.active_account.contract_name,
function_name=state.environment.active_function_name,
address=address,
swc_id=REENTRANCY,
title="External Call To Fixed Address",
bytecode=state.environment.code.bytecode,
severity="Low",
description_head=description_head,
description_tail=description_tail,

@ -194,25 +194,6 @@ class IntegerArithmetics(DetectionModule):
stack[index] = symbol_factory.BitVecVal(value, 256)
return stack[index]
@staticmethod
def _get_description_head(annotation, _type):
return "The binary {} can {}.".format(annotation.operator, _type.lower())
@staticmethod
def _get_description_tail(annotation, _type):
return (
"The operands of the {} operation are not sufficiently constrained. "
"The {} could therefore result in an integer {}. Prevent the {} by checking inputs "
"or ensure sure that the {} is caught by an assertion.".format(
annotation.operator,
annotation.operator,
_type.lower(),
_type.lower(),
_type.lower(),
)
)
@staticmethod
def _get_title(_type):
return "Integer {}".format(_type)
@ -317,17 +298,24 @@ class IntegerArithmetics(DetectionModule):
except UnsatError:
continue
_type = "Underflow" if annotation.operator == "subtraction" else "Overflow"
description_head = "The arithmetic operator can {}.".format(
"underflow" if annotation.operator == "subtraction" else "overflow"
)
description_tail = "It is possible to cause an integer overflow or underflow in the arithmetic operation. "
"Prevent this by constraining inputs using the require() statement or use the OpenZeppelin "
"SafeMath library for integer arithmetic operations. "
"Refer to the transaction trace generated for this issue to reproduce the issue."
issue = Issue(
contract=ostate.environment.active_account.contract_name,
function_name=ostate.environment.active_function_name,
address=ostate.get_current_instruction()["address"],
swc_id=INTEGER_OVERFLOW_AND_UNDERFLOW,
bytecode=ostate.environment.code.bytecode,
title=self._get_title(_type),
title="Integer Arithmetic Bugs",
severity="High",
description_head=self._get_description_head(annotation, _type),
description_tail=self._get_description_tail(annotation, _type),
description_head=description_head,
description_tail=description_tail,
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
transaction_sequence=transaction_sequence,
)

@ -75,8 +75,11 @@ class MultipleSends(DetectionModule):
except UnsatError:
continue
description_tail = (
"This call is executed after a previous call in the same transaction. "
"Try to isolate each call, transfer or send into its own transaction."
"This call is executed following another call within the same transaction. It is possible "
"that the call never gets executed if a prior call fails permanently. This might be caused "
"intentionally by a malicious callee. If possible, refactor the code such that each transaction "
"only executes one external call or "
"make sure that all callees can be trusted (i.e. they’re part of your own codebase)."
)
issue = Issue(

@ -19,7 +19,7 @@ log = logging.getLogger(__name__)
DESCRIPTION = """
Check whether there is a state change of the contract after the execution of an external call
Check whether the account state is accesses after the execution of an external call
"""
CALL_LIST = ["CALL", "DELEGATECALL", "CALLCODE"]
@ -69,22 +69,27 @@ class StateChangeCallsAnnotation(StateAnnotation):
logging.debug(
"[EXTERNAL_CALLS] Detected state changes at addresses: {}".format(address)
)
read_or_write = "write"
read_or_write = "Write to"
if global_state.get_current_instruction()["opcode"] == "SLOAD":
read_or_write = "read"
read_or_write = "Read of"
address_type = "user defined" if self.user_defined_address else "fixed"
description_head = "Persistent state {} after call".format(read_or_write)
description_head = "{} persistent state following external call".format(
read_or_write
)
description_tail = (
"The contract account state is changed after an external call to a {} address. "
"Consider that the called contract could re-enter the function before this "
"state change takes place".format(address_type)
"The contract account state is accessed after an external call to a {} address. "
"To prevent reentrancy issues, consider accessing the state only before the call, especially if the callee is untrusted. "
"Alternatively, a reentrancy lock can be used to prevent "
"untrusted callees from re-entering the contract in an intermediate state.".format(
address_type
)
)
return PotentialIssue(
contract=global_state.environment.active_account.contract_name,
function_name=global_state.environment.active_function_name,
address=address,
title="State change after external call",
title="State access after external call",
severity=severity,
description_head=description_head,
description_tail=description_tail,

@ -63,7 +63,7 @@ class AccidentallyKillable(DetectionModule):
log.debug("SUICIDE in function %s", state.environment.active_function_name)
description_head = "The contract can be killed by anyone."
description_head = "Any sender can cause the contract to self-destruct."
constraints = []
@ -80,15 +80,24 @@ class AccidentallyKillable(DetectionModule):
+ constraints
+ [to == ACTORS.attacker],
)
description_tail = (
"Anyone can kill this contract and withdraw its balance to an arbitrary "
"address."
"Any sender can trigger execution of the SELFDESTRUCT instruction to destroy this "
"contract account and withdraw its balance to an arbitrary address. Review the transaction trace "
"generated for this issue and make sure that appropriate security controls are in place to prevent "
"unrestricted access."
)
except UnsatError:
transaction_sequence = solver.get_transaction_sequence(
state, state.world_state.constraints + constraints
)
description_tail = "Arbitrary senders can kill this contract."
description_tail = (
"Any sender can trigger execution of the SELFDESTRUCT instruction to destroy this "
"contract account. Review the transaction trace generated for this issue and make sure that "
"appropriate security controls are in place to prevent unrestricted access."
)
issue = Issue(
contract=state.environment.active_account.contract_name,
function_name=state.environment.active_function_name,

@ -86,9 +86,10 @@ class UncheckedRetval(DetectionModule):
continue
description_tail = (
"External calls return a boolean value. If the callee contract halts with an exception, 'false' is "
"returned and execution continues in the caller. It is usually recommended to wrap external calls "
"into a require statement to prevent unexpected states."
"External calls return a boolean value. If the callee halts with an exception, 'false' is "
"returned and execution continues in the caller. "
"The caller should check whether an exception happened and react accordingly to avoid unexpected behavior. "
"For example it is often desirable to wrap external calls in require() so the transaction is reverted if the call fails."
)
issue = Issue(
@ -96,9 +97,9 @@ class UncheckedRetval(DetectionModule):
function_name=state.environment.active_function_name,
address=retval["address"],
bytecode=state.environment.code.bytecode,
title="Unchecked Call Return Value",
title="Unchecked return value from external call.",
swc_id=UNCHECKED_RET_VAL,
severity="Low",
severity="Medium",
description_head="The return value of a message call is not checked.",
description_tail=description_tail,
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),

@ -69,11 +69,11 @@ class UserAssertions(DetectionModule):
description_head = "A user-provided assertion failed."
if message:
description_tail = "A user-provided assertion failed with message '{}'. Make sure the user-provided assertion is correct.".format(
description_tail = "A user-provided assertion failed with the message '{}'".format(
message
)
else:
description_tail = "A user-provided assertion failed. Make sure the user-provided assertion is correct."
description_tail = "A user-provided assertion failed."
address = state.get_current_instruction()["address"]
issue = PotentialIssue(

@ -1,10 +1,9 @@
"""This module contains analysis module helpers to solve path constraints."""
from functools import lru_cache
from typing import Dict, List, Tuple, Union
from z3 import sat, unknown, FuncInterp
from z3 import FuncInterp
import z3
from mythril.analysis.analysis_args import analysis_args
from mythril.support.model import get_model
from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.laser.ethereum.state.constraints import Constraints
from mythril.laser.ethereum.keccak_function_manager import (
@ -12,8 +11,7 @@ from mythril.laser.ethereum.keccak_function_manager import (
hash_matcher,
)
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.smt import UGE, symbol_factory
from mythril.exceptions import UnsatError
from mythril.laser.ethereum.transaction.transaction_models import (
ContractCreationTransaction,
@ -23,44 +21,6 @@ import logging
log = logging.getLogger(__name__)
# LRU cache works great when used in powers of 2
@lru_cache(maxsize=2 ** 23)
def get_model(constraints, minimize=(), maximize=(), enforce_execution_time=True):
"""
:param constraints:
:param minimize:
:param maximize:
:param enforce_execution_time: Bool variable which enforces --execution-timeout's time
:return:
"""
s = Optimize()
timeout = analysis_args.solver_timeout
if enforce_execution_time:
timeout = min(timeout, time_handler.time_remaining() - 500)
if timeout <= 0:
raise UnsatError
s.set_timeout(timeout)
for constraint in constraints:
if type(constraint) == bool and not constraint:
raise UnsatError
constraints = [constraint for constraint in constraints if type(constraint) != bool]
for constraint in constraints:
s.add(constraint)
for e in minimize:
s.minimize(e)
for e in maximize:
s.maximize(e)
result = s.check()
if result == sat:
return s.model()
elif result == unknown:
log.debug("Timeout encountered while solving expression using z3")
raise UnsatError
def pretty_print_model(model):
""" Pretty prints a z3 model

@ -23,6 +23,7 @@ from mythril.exceptions import (
CriticalError,
)
from mythril.laser.ethereum.transaction.symbolic import ACTORS
from mythril.plugin.loader import MythrilPluginLoader
from mythril.mythril import (
MythrilAnalyzer,
MythrilDisassembler,
@ -34,6 +35,9 @@ from mythril.analysis.module import ModuleLoader
from mythril.__version__ import __version__ as VERSION
# Initialise core Mythril Component
_ = MythrilPluginLoader()
ANALYZE_LIST = ("analyze", "a")
DISASSEMBLE_LIST = ("disassemble", "d")
PRO_LIST = ("pro", "p")
@ -446,6 +450,17 @@ def create_analyzer_parser(analyzer_parser: ArgumentParser):
action="store_true",
help="Don't attempt to retrieve contract code, variables and balances from the blockchain",
)
options.add_argument(
"--sparse-pruning",
action="store_true",
help="Checks for reachability after the end of tx. Recommended for short execution timeouts < 1 min",
)
options.add_argument(
"--unconstrained-storage",
action="store_true",
help="Default storage value is symbolic, turns off the on-chain storage loading",
)
options.add_argument(
"--phrack", action="store_true", help="Phrack-style call graph"
)
@ -672,6 +687,8 @@ def execute_command(
custom_modules_directory=args.custom_modules_directory
if args.custom_modules_directory
else "",
sparse_pruning=args.sparse_pruning,
unconstrained_storage=args.unconstrained_storage,
)
if not disassembler.contracts:

@ -10,6 +10,7 @@ from typing import Any, Dict, Union, Set
from mythril.laser.smt import Array, K, BitVec, simplify, BaseArray
from mythril.disassembler.disassembly import Disassembly
from mythril.laser.smt import symbol_factory
from mythril.support.support_args import args
log = logging.getLogger(__name__)
@ -22,7 +23,7 @@ class Storage:
:param concrete: bool indicating whether to interpret uninitialized storage as concrete versus symbolic
"""
if concrete:
if concrete and args.unconstrained_storage is False:
self._standard_storage = K(256, 256, 0) # type: BaseArray
else:
self._standard_storage = Array("Storage", 256, 256)
@ -41,6 +42,7 @@ class Storage:
and item.symbolic is False
and int(item.value) not in self.storage_keys_loaded
and (self.dynld and self.dynld.active)
and args.unconstrained_storage is False
):
try:
storage[item] = symbol_factory.BitVecVal(

@ -1,10 +1,9 @@
"""This module contains the class used to represent state-change constraints in
the call graph."""
from mythril.laser.smt import Solver, Bool, symbol_factory, simplify
from mythril.exceptions import UnsatError
from mythril.laser.smt import Bool, simplify
from mythril.support.model import get_model
from typing import Iterable, List, Optional, Union
from z3 import unsat
class Constraints(list):
@ -14,21 +13,14 @@ class Constraints(list):
"""
def __init__(
self,
constraint_list: Optional[List[Bool]] = None,
is_possible: Optional[bool] = None,
) -> None:
def __init__(self, constraint_list: Optional[List[Bool]] = None,) -> None:
"""
:param constraint_list: List of constraints
:param is_possible: Whether it is possible to satisfy the constraints or not
"""
constraint_list = constraint_list or []
constraint_list = self._get_smt_bool_list(constraint_list)
super(Constraints, self).__init__(constraint_list)
self._default_timeout = 100
self._is_possible = is_possible
@property
def is_possible(self) -> bool:
@ -36,19 +28,11 @@ class Constraints(list):
:return: True/False based on the existence of solution of constraints
"""
if self._is_possible is not None:
return self._is_possible
solver = Solver()
solver.set_timeout(self._default_timeout)
for constraint in self[:]:
constraint = (
symbol_factory.Bool(constraint)
if isinstance(constraint, bool)
else constraint
)
solver.add(constraint)
self._is_possible = solver.check() != unsat
return self._is_possible
try:
get_model(tuple(self[:]))
except UnsatError:
return False
return True
def append(self, constraint: Union[bool, Bool]) -> None:
"""
@ -59,7 +43,6 @@ class Constraints(list):
simplify(constraint) if isinstance(constraint, Bool) else Bool(constraint)
)
super(Constraints, self).append(constraint)
self._is_possible = None
def pop(self, index: int = -1) -> None:
"""
@ -81,7 +64,7 @@ class Constraints(list):
:return: The copied constraint List
"""
constraint_list = super(Constraints, self).copy()
return Constraints(constraint_list, is_possible=self._is_possible)
return Constraints(constraint_list)
def copy(self) -> "Constraints":
return self.__copy__()
@ -102,7 +85,7 @@ class Constraints(list):
"""
constraints_list = self._get_smt_bool_list(constraints)
constraints_list = super(Constraints, self).__add__(constraints_list)
return Constraints(constraint_list=constraints_list, is_possible=None)
return Constraints(constraint_list=constraints_list)
def __iadd__(self, constraints: Iterable[Union[bool, Bool]]) -> "Constraints":
"""
@ -112,7 +95,6 @@ class Constraints(list):
"""
list_constraints = self._get_smt_bool_list(constraints)
super(Constraints, self).__iadd__(list_constraints)
self._is_possible = None
return self
@staticmethod

@ -45,7 +45,8 @@ class BoundedLoopsStrategy(BasicSearchStrategy):
self, super_strategy.work_list, super_strategy.max_depth
)
def calculate_hash(self, i, j, trace):
@staticmethod
def calculate_hash(i: int, j: int, trace: List[int]) -> int:
"""
calculate hash(trace[i: j])
:param i:
@ -61,7 +62,8 @@ class BoundedLoopsStrategy(BasicSearchStrategy):
return key
def count_key(self, trace, key, start, size):
@staticmethod
def count_key(trace: List[int], key: int, start: int, size: int) -> int:
"""
Count continuous loops in the trace.
:param trace:
@ -69,15 +71,36 @@ class BoundedLoopsStrategy(BasicSearchStrategy):
:param size:
:return:
"""
count = 0
count = 1
i = start
while i >= 0:
if self.calculate_hash(i, i + size, trace) != key:
if BoundedLoopsStrategy.calculate_hash(i, i + size, trace) != key:
break
count += 1
i -= size
return count
@staticmethod
def get_loop_count(trace: List[int]) -> int:
"""
Gets the loop count
:param trace: annotation trace
:return:
"""
found = False
for i in range(len(trace) - 3, 0, -1):
if trace[i] == trace[-2] and trace[i + 1] == trace[-1]:
found = True
break
if found:
key = BoundedLoopsStrategy.calculate_hash(i + 1, len(trace) - 1, trace)
size = len(trace) - i - 2
count = BoundedLoopsStrategy.count_key(trace, key, i + 1, size)
else:
count = 0
return count
def get_strategic_global_state(self) -> GlobalState:
""" Returns the next state
@ -107,28 +130,9 @@ class BoundedLoopsStrategy(BasicSearchStrategy):
return state
# create unique instruction identifier
found = False
for i in range(len(annotation.trace) - 3, 0, -1):
if (
annotation.trace[i] == annotation.trace[-2]
and annotation.trace[i + 1] == annotation.trace[-1]
):
found = True
break
if found:
key = self.calculate_hash(
i, len(annotation.trace) - 1, annotation.trace
)
size = len(annotation.trace) - i - 1
count = self.count_key(annotation.trace, key, i, size)
else:
count = 0
count = BoundedLoopsStrategy.get_loop_count(annotation.trace)
# The creation transaction gets a higher loop bound to give it a better chance of success.
# TODO: There's probably a nicer way to do this
if isinstance(
state.current_transaction, ContractCreationTransaction
) and count < max(8, self.bound):

@ -26,7 +26,7 @@ from mythril.laser.ethereum.transaction import (
execute_message_call,
)
from mythril.laser.smt import symbol_factory
from mythril.support.support_args import args
log = logging.getLogger(__name__)
@ -191,6 +191,15 @@ class LaserEVM:
self.time = datetime.now()
for i in range(self.transaction_count):
if len(self.open_states) == 0:
break
old_states_count = len(self.open_states)
self.open_states = [
state for state in self.open_states if state.constraints.is_possible
]
prune_count = old_states_count - len(self.open_states)
if prune_count:
log.info("Pruned {} unreachable states".format(prune_count))
log.info(
"Starting message call transaction, iteration: {}, {} initial states".format(
i, len(self.open_states)
@ -236,6 +245,7 @@ class LaserEVM:
except NotImplementedError:
log.debug("Encountered unimplemented instruction")
continue
if args.sparse_pruning is False:
new_states = [
state
for state in new_states

@ -83,6 +83,11 @@ def execute_message_call(laser_evm, callee_address: BitVec) -> None:
continue
next_transaction_id = get_next_transaction_id()
external_sender = symbol_factory.BitVecSym(
"sender_{}".format(next_transaction_id), 256
)
transaction = MessageCallTransaction(
world_state=open_world_state,
identifier=next_transaction_id,
@ -90,12 +95,8 @@ def execute_message_call(laser_evm, callee_address: BitVec) -> None:
"gas_price{}".format(next_transaction_id), 256
),
gas_limit=8000000, # block gas limit
origin=symbol_factory.BitVecSym(
"origin{}".format(next_transaction_id), 256
),
caller=symbol_factory.BitVecSym(
"sender_{}".format(next_transaction_id), 256
),
origin=external_sender,
caller=external_sender,
callee_account=open_world_state[callee_address],
call_data=SymbolicCalldata(next_transaction_id),
call_value=symbol_factory.BitVecSym(
@ -145,6 +146,7 @@ def execute_contract_creation(
)
_setup_global_state_for_execution(laser_evm, transaction)
new_account = new_account or transaction.callee_account
laser_evm.exec(True)
return new_account

@ -4,10 +4,12 @@ from mythril.laser.plugin.builder import PluginBuilder
from mythril.laser.plugin.plugins.plugin_annotations import MutationAnnotation
from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.laser.ethereum.svm import LaserEVM
from mythril.laser.smt import UGT, symbol_factory
from mythril.laser.ethereum.transaction.transaction_models import (
ContractCreationTransaction,
)
from mythril.laser.smt import And, symbol_factory
from mythril.analysis import solver
from mythril.exceptions import UnsatError
class MutationPrunerBuilder(PluginBuilder):
@ -44,6 +46,10 @@ class MutationPruner(LaserPlugin):
def sstore_mutator_hook(global_state: GlobalState):
global_state.annotate(MutationAnnotation())
"""FIXME: Check for changes in world_state.balances instead of adding MutationAnnotation for all calls.
Requires world_state.starting_balances to be initalized at every tx start *after* call value has been added.
"""
@symbolic_vm.pre_hook("CALL")
def call_mutator_hook(global_state: GlobalState):
global_state.annotate(MutationAnnotation())
@ -54,17 +60,30 @@ class MutationPruner(LaserPlugin):
@symbolic_vm.laser_hook("add_world_state")
def world_state_filter_hook(global_state: GlobalState):
if And(
*global_state.world_state.constraints[:]
+ [
global_state.environment.callvalue
> symbol_factory.BitVecVal(0, 256)
]
).is_false:
return
if isinstance(
global_state.current_transaction, ContractCreationTransaction
):
return
if isinstance(global_state.environment.callvalue, int):
callvalue = symbol_factory.BitVecVal(
global_state.environment.callvalue, 256
)
else:
callvalue = global_state.environment.callvalue
try:
constraints = global_state.world_state.constraints + [
UGT(callvalue, symbol_factory.BitVecVal(0, 256))
]
solver.get_model(constraints)
return
except UnsatError:
# callvalue is constrained to 0, therefore there is no balance based world state mutation
pass
if len(list(global_state.get_annotations(MutationAnnotation))) == 0:
raise PluginSkipWorldState

@ -9,9 +9,9 @@ from mythril.laser.ethereum.iprof import InstructionProfiler
from . import MythrilDisassembler
from mythril.support.source_support import Source
from mythril.support.loader import DynLoader
from mythril.support.support_args import args
from mythril.analysis.symbolic import SymExecWrapper
from mythril.analysis.callgraph import generate_graph
from mythril.analysis.analysis_args import analysis_args
from mythril.analysis.traceexplore import get_serializable_statespace
from mythril.analysis.security import fire_lasers, retrieve_callback_issues
from mythril.analysis.report import Report, Issue
@ -44,6 +44,8 @@ class MythrilAnalyzer:
disable_dependency_pruning: bool = False,
solver_timeout: Optional[int] = None,
custom_modules_directory: str = "",
sparse_pruning: bool = False,
unconstrained_storage: bool = False,
):
"""
@ -64,9 +66,9 @@ class MythrilAnalyzer:
self.iprof = InstructionProfiler() if enable_iprof else None
self.disable_dependency_pruning = disable_dependency_pruning
self.custom_modules_directory = custom_modules_directory
analysis_args.set_loop_bound(loop_bound)
analysis_args.set_solver_timeout(solver_timeout)
args.sparse_pruning = sparse_pruning
args.solver_timeout = solver_timeout
args.unconstrained_storage = unconstrained_storage
def dump_statespace(self, contract: EVMContract = None) -> str:
"""

@ -2,7 +2,7 @@ import pkg_resources
from mythril.support.support_utils import Singleton
from mythril.plugin.interface import MythrilPlugin
from typing import List
from typing import List, Dict, Any, Optional
class PluginDiscovery(object, metaclass=Singleton):
@ -12,21 +12,30 @@ class PluginDiscovery(object, metaclass=Singleton):
"""
# Installed plugins structure. Retrieves all modules that have an entry point for mythril.plugins
_installed_plugins = {
_installed_plugins = None # type: Optional[Dict[str, Any]]
def init_installed_plugins(self):
self._installed_plugins = {
entry_point.name: entry_point.load()
for entry_point in pkg_resources.iter_entry_points("mythril.plugins")
}
@property
def installed_plugins(self):
if self._installed_plugins is None:
self.init_installed_plugins()
return self._installed_plugins
def is_installed(self, plugin_name: str) -> bool:
"""Returns whether there is python package with a plugin with plugin_name"""
return plugin_name in self._installed_plugins.keys()
return plugin_name in self.installed_plugins.keys()
def build_plugin(self, plugin_name: str) -> MythrilPlugin:
"""Returns the plugin for the given plugin_name if it is installed"""
if not self.is_installed(plugin_name):
raise ValueError(f"Plugin with name: `{plugin_name}` is not installed")
plugin = self._installed_plugins.get(plugin_name)
plugin = self.installed_plugins.get(plugin_name)
if plugin is None or not issubclass(plugin, MythrilPlugin):
raise ValueError(f"No valid plugin was found for {plugin_name}")
@ -40,10 +49,10 @@ class PluginDiscovery(object, metaclass=Singleton):
:return: List of plugin names
"""
if default_enabled is None:
return list(self._installed_plugins.keys())
return list(self.installed_plugins.keys())
return [
plugin_name
for plugin_name, plugin_class in self._installed_plugins.items()
for plugin_name, plugin_class in self.installed_plugins.items()
if plugin_class.plugin_default_enabled == default_enabled
]

@ -0,0 +1,49 @@
from functools import lru_cache
from z3 import sat, unknown
from mythril.support.support_args import args
from mythril.laser.smt import Optimize
from mythril.laser.ethereum.time_handler import time_handler
from mythril.exceptions import UnsatError
import logging
log = logging.getLogger(__name__)
# LRU cache works great when used in powers of 2
@lru_cache(maxsize=2 ** 23)
def get_model(constraints, minimize=(), maximize=(), enforce_execution_time=True):
"""
Returns a model based on given constraints as a tuple
:param constraints: Tuple of constraints
:param minimize: Tuple of minimization conditions
:param maximize: Tuple of maximization conditions
:param enforce_execution_time: Bool variable which enforces --execution-timeout's time
:return:
"""
s = Optimize()
timeout = args.solver_timeout
if enforce_execution_time:
timeout = min(timeout, time_handler.time_remaining() - 500)
if timeout <= 0:
raise UnsatError
s.set_timeout(timeout)
for constraint in constraints:
if type(constraint) == bool and not constraint:
raise UnsatError
constraints = [constraint for constraint in constraints if type(constraint) != bool]
for constraint in constraints:
s.add(constraint)
for e in minimize:
s.minimize(e)
for e in maximize:
s.maximize(e)
result = s.check()
if result == sat:
return s.model()
elif result == unknown:
log.debug("Timeout encountered while solving expression using z3")
raise UnsatError

@ -0,0 +1,13 @@
class Args:
"""
This module helps in preventing args being sent through multiple of classes to reach
any analysis/laser module
"""
def __init__(self):
self.solver_timeout = 10000
self.sparse_pruning = True
self.unconstrained_storage = False
args = Args()

@ -44,12 +44,12 @@ class CommandLineToolTestCase(BaseTestCase):
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))
self.assertIn("115", 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))
self.assertIn("115", output_of(command))
def test_invalid_args_iprof(self):
solidity_file = str(TESTDATA / "input_contracts" / "origin.sol")

@ -13,6 +13,7 @@ def test_generate_graph():
continue
contract = EVMContract(input_file.read_text())
disassembler = MythrilDisassembler()
disassembler.contracts.append(contract)
analyzer = MythrilAnalyzer(
disassembler=disassembler,
@ -20,6 +21,7 @@ def test_generate_graph():
execution_timeout=5,
max_depth=30,
address=(util.get_indexed_address(0)),
solver_timeout=10000,
)
analyzer.graph_html(transaction_count=1)

@ -1,6 +1,7 @@
from mythril.laser.ethereum.svm import LaserEVM
from mythril.laser.ethereum.state.account import Account
from mythril.laser.ethereum.state.world_state import WorldState
from mythril.laser.ethereum.time_handler import time_handler
from mythril.laser.ethereum.keccak_function_manager import keccak_function_manager
from mythril.disassembler.disassembly import Disassembly
from mythril.laser.ethereum.transaction.concolic import execute_message_call
@ -130,9 +131,9 @@ def test_vmtest(
world_state.put_account(account)
account.set_balance(int(details["balance"], 16))
time_handler.start_execution(10000)
laser_evm = LaserEVM()
laser_evm.open_states = [world_state]
# Act
laser_evm.time = datetime.now()

@ -0,0 +1,20 @@
import pytest
from mythril.laser.ethereum.strategy.extensions.bounded_loops import (
BoundedLoopsStrategy,
)
@pytest.mark.parametrize(
"trace, count",
[
([6, 7, 7, 7], 3),
([6, 8, 6, 7, 6, 7, 6, 7, 6, 7], 4),
([6, 6, 6, 6], 4),
([6, 7, 8] * 10, 10),
([7, 9, 10] + list(range(1, 100)) * 100, 100),
([7, 10, 15], 0),
([7] * 100, 100),
],
)
def test_loop_count(trace, count):
assert count == BoundedLoopsStrategy.get_loop_count(trace)

@ -18,6 +18,7 @@ def test_statespace_dump():
execution_timeout=5,
max_depth=30,
address=(util.get_indexed_address(0)),
solver_timeout=10000,
)
analyzer.dump_statespace(contract=contract)

Loading…
Cancel
Save