Merge branch 'develop' into fix/quick

pull/1358/head
JoranHonig 5 years ago committed by GitHub
commit 5faac03012
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
  1. 30
      mythril/analysis/analysis_args.py
  2. 4
      mythril/analysis/module/loader.py
  3. 13
      mythril/analysis/module/modules/arbitrary_jump.py
  4. 9
      mythril/analysis/module/modules/arbitrary_write.py
  5. 10
      mythril/analysis/module/modules/delegatecall.py
  6. 112
      mythril/analysis/module/modules/dependence_on_origin.py
  7. 111
      mythril/analysis/module/modules/dependence_on_predictable_vars.py
  8. 85
      mythril/analysis/module/modules/deprecated_ops.py
  9. 9
      mythril/analysis/module/modules/ether_thief.py
  10. 16
      mythril/analysis/module/modules/exceptions.py
  11. 8
      mythril/analysis/module/modules/external_calls.py
  12. 12
      mythril/analysis/module/modules/integer.py
  13. 6
      mythril/analysis/module/modules/multiple_sends.py
  14. 19
      mythril/analysis/module/modules/state_change_external_calls.py
  15. 17
      mythril/analysis/module/modules/suicide.py
  16. 9
      mythril/analysis/module/modules/unchecked_retval.py
  17. 4
      mythril/analysis/module/modules/user_assertions.py
  18. 46
      mythril/analysis/solver.py
  19. 6
      mythril/interfaces/cli.py
  20. 40
      mythril/laser/ethereum/state/constraints.py
  21. 22
      mythril/laser/ethereum/svm.py
  22. 8
      mythril/mythril/mythril_analyzer.py
  23. 49
      mythril/support/model.py
  24. 12
      mythril/support/support_args.py
  25. 4
      tests/cmd_line_test.py
  26. 2
      tests/graph_test.py
  27. 3
      tests/laser/evm_testsuite/evm_test.py
  28. 1
      tests/statespace_test.py

@ -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="The caller can write to arbitrary storage locations.",
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_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,
)

@ -73,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 [
@ -85,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,41 +135,27 @@ 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(
state.environment.block_number,
symbol_factory.BitVecVal(2 ** 255, 256),
),
]
constraint = [
ULT(param, state.environment.block_number),
ULT(
state.environment.block_number,
symbol_factory.BitVecVal(2 ** 255, 256),
),
]
# Why the second constraint? Because without it Z3 returns a solution where param overflows.
# 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,85 +0,0 @@
"""This module contains the detection code for deprecated op codes."""
from mythril.analysis.report import Issue
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)
self.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 []
issue = Issue(
contract=state.environment.active_account.contract_name,
function_name=state.environment.active_function_name,
address=instruction["address"],
title=title,
bytecode=state.environment.code.bytecode,
swc_id=swc_id,
severity="Medium",
description_head=description_head,
description_tail=description_tail,
)
return [issue]
detector = DeprecatedOperations()

@ -28,7 +28,7 @@ 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
@ -86,9 +86,10 @@ class EtherThief(DetectionModule):
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. 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,
)

@ -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 exception or assertion violation was triggered.",
description_tail=description_tail,
bytecode=state.environment.code.bytecode,
transaction_sequence=transaction_sequence,

@ -86,10 +86,10 @@ class ExternalCalls(DetectionModule):
description_head = "A call to a user-supplied address is executed."
description_tail = (
"An external message is sent to an address specified by the caller. Note that "
"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 "
"with this contract. Reentering the contract in an intermediate state may lead to "
"unexpected behaviour. Make sure that state is no state modifications "
"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."
)
@ -100,7 +100,7 @@ class ExternalCalls(DetectionModule):
swc_id=REENTRANCY,
title="External Call To User-Supplied Address",
bytecode=state.environment.code.bytecode,
severity="Medium",
severity="Low",
description_head=description_head,
description_tail=description_tail,
constraints=constraints,

@ -202,14 +202,10 @@ class IntegerArithmetics(DetectionModule):
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(),
"It is possible to cause an integer {} in the {} operation. Prevent the {} 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 {}.".format(
_type.lower(), annotation.operator, _type.lower(), _type.lower()
)
)

@ -75,8 +75,10 @@ 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."
)
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,25 @@ 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. Note that the callee "
"could re-enter any function in this contract before the state access has occurred. Review the contract "
"logic carefully and consider performing all state operations before executing the external call, "
"especially if the callee is not trusted.".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. It is often desirable to wrap external calls "
"into a require() statement so the transaction is reverted if the call fails. Make sure that "
"no unexpected behaviour occurs if the call is unsuccessful."
)
issue = Issue(
@ -96,7 +97,7 @@ 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",
description_head="The return value of a message call is not checked.",

@ -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

@ -446,6 +446,11 @@ 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(
"--phrack", action="store_true", help="Phrack-style call graph"
)
@ -673,6 +678,7 @@ def execute_command(
custom_modules_directory=args.custom_modules_directory
if args.custom_modules_directory
else "",
sparse_pruning=args.sparse_pruning,
)
if not disassembler.contracts:

@ -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

@ -29,7 +29,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__)
@ -203,6 +203,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)
@ -248,11 +257,12 @@ class LaserEVM:
except NotImplementedError:
log.debug("Encountered unimplemented instruction")
continue
new_states = [
state
for state in new_states
if state.world_state.constraints.is_possible
]
if args.sparse_pruning is False:
new_states = [
state
for state in new_states
if state.world_state.constraints.is_possible
]
self.manage_cfg(op_code, new_states) # TODO: What about op_code is None?
if new_states:

@ -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
@ -45,6 +45,7 @@ class MythrilAnalyzer:
solver_timeout: Optional[int] = None,
enable_coverage_strategy: bool = False,
custom_modules_directory: str = "",
sparse_pruning: bool = False,
):
"""
@ -66,9 +67,8 @@ class MythrilAnalyzer:
self.disable_dependency_pruning = disable_dependency_pruning
self.enable_coverage_strategy = enable_coverage_strategy
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
def dump_statespace(self, contract: EVMContract = None) -> str:
"""

@ -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,12 @@
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
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()

@ -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