diff --git a/.circleci/config.yml b/.circleci/config.yml index b0989c61..8926f5e6 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -103,6 +103,8 @@ jobs: 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 \ diff --git a/README.md b/README.md index 586d6fd8..df3ad81c 100644 --- a/README.md +++ b/README.md @@ -32,11 +32,50 @@ Install from Pypi: $ pip3 install mythril ``` -See the [Wiki](https://github.com/ConsenSys/mythril/wiki/Installation-and-Setup) for more detailed instructions. +See the [docs](https://mythril-classic.readthedocs.io/en/master/installation.html) for more detailed instructions. ## Usage -Instructions for using Mythril are found on the [Wiki](https://github.com/ConsenSys/mythril/wiki). +Run: + +``` +$ myth analyze +``` + +Or: + +``` +$ myth analyze -a +``` + +Specify the maximum number of transaction to explore with `-t `. You can also set a timeout with `--execution-timeout `. Example ([source code](https://gist.github.com/b-mueller/2b251297ce88aa7628680f50f177a81a#file-killbilly-sol)): + +``` +==== Unprotected Selfdestruct ==== +SWC ID: 106 +Severity: High +Contract: KillBilly +Function name: commencekilling() +PC address: 354 +Estimated Gas Usage: 574 - 999 +The contract can be killed by anyone. +Anyone can kill this contract and withdraw its balance to an arbitrary address. +-------------------- +In file: killbilly.sol:22 + +selfdestruct(msg.sender) + +-------------------- +Transaction Sequence: + +Caller: [CREATOR], data: [CONTRACT CREATION], value: 0x0 +Caller: [ATTACKER], function: killerize(address), txdata: 0x9fa299ccbebebebebebebebebebebebedeadbeefdeadbeefdeadbeefdeadbeefdeadbeef, value: 0x0 +Caller: [ATTACKER], function: activatekillability(), txdata: 0x84057065, value: 0x0 +Caller: [ATTACKER], function: commencekilling(), txdata: 0x7c11da20, value: 0x0 +``` + + +Instructions for using Mythril are found on the [docs](https://mythril-classic.readthedocs.io/en/master/). For support or general discussions please join the Mythril community on [Discord](https://discord.gg/E3YrVtG). diff --git a/all_tests.sh b/all_tests.sh index 61cd7d67..7fd0ae81 100755 --- a/all_tests.sh +++ b/all_tests.sh @@ -7,22 +7,6 @@ assert sys.version_info[0:2] >= (3,5), \ """Please make sure you are using Python 3.5 or later. You ran with {}""".format(sys.version)' || exit $? -echo "Checking solc version..." -out=$(solc --version) || { - echo 2>&1 "Please make sure you have solc installed, version 0.4.21 or greater" - - } -case $out in - *Version:\ 0.4.2[1-9]* ) - echo $out - ;; - * ) - echo $out - echo "Please make sure your solc version is at least 0.4.21" - exit 1 - ;; -esac - echo "Checking that truffle is installed..." if ! which truffle ; then echo "Please make sure you have etherum truffle installed (npm install -g truffle)" diff --git a/docs/source/index.rst b/docs/source/index.rst index e3f9df42..77ff628d 100644 --- a/docs/source/index.rst +++ b/docs/source/index.rst @@ -9,6 +9,7 @@ Welcome to Mythril's documentation! installation security-analysis analysis-modules + mythx-analysis mythril diff --git a/docs/source/module-list.rst b/docs/source/module-list.rst index 11c40d02..101ff94f 100644 --- a/docs/source/module-list.rst +++ b/docs/source/module-list.rst @@ -67,3 +67,9 @@ Unchecked Retval **************** The `unchecked retval module `_ detects `SWC-104 (Unchecked Call Return Value) `_. + +**************** +Unchecked Retval +**************** + +The `user supplied assertion module `_ detects `SWC-110 (Assert Violation) `_ for user-supplied assertions. User supplied assertions should be log messages of the form: :code:`emit AssertionFailed(string)`. diff --git a/docs/source/mythx-analysis.rst b/docs/source/mythx-analysis.rst new file mode 100644 index 00000000..eddb0db9 --- /dev/null +++ b/docs/source/mythx-analysis.rst @@ -0,0 +1,63 @@ +MythX Analysis +================= + +Run :code:`myth pro` with one of the input options described below will run a `MythX analysis `_ on the desired input. This includes a run of Mythril, the fuzzer Harvey, and the static analysis engine Maru and has some false-positive filtering only possible by combining the tool capabilities. + +************** +Authentication +************** + +In order to authenticate with the MythX API, set the environment variables ``MYTHX_PASSWORD`` and ``MYTHX_ETH_ADDRESS``. + +.. code-block:: bash + + $ export MYTHX_ETH_ADDRESS='0x0000000000000000000000000000000000000000' + $ export MYTHX_PASSWORD='password' + +*********************** +Analyzing Solidity Code +*********************** + +The input format is the same as a regular Mythril analysis. + +.. code-block:: bash + + $ myth pro ether_send.sol + ==== Unprotected Ether Withdrawal ==== + SWC ID: 105 + Severity: High + Contract: Crowdfunding + Function name: withdrawfunds() + PC address: 730 + Anyone can withdraw ETH from the contract account. + 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. + -------------------- + In file: tests/testdata/input_contracts/ether_send.sol:21 + + msg.sender.transfer(address(this).balance) + + -------------------- + +If an input file contains multiple contract definitions, Mythril analyzes the *last* bytecode output produced by solc. You can override this by specifying the contract name explicitly: + +.. code-block:: bash + + myth pro OmiseGo.sol:OMGToken + +To specify a contract address, use :code:`-a
` + +**************************** +Analyzing On-Chain Contracts +**************************** + +Analyzing a mainnet contract via INFURA: + +.. code-block:: bash + + myth pro -a 0x5c436ff914c458983414019195e0f4ecbef9e6dd + +Adding the :code:`-l` flag will cause mythril to automatically retrieve dependencies, such as dynamically linked library contracts: + +.. code-block:: bash + + myth -v4 pro -l -a 0xEbFD99838cb0c132016B9E117563CB41f2B02264 diff --git a/docs/source/security-analysis.rst b/docs/source/security-analysis.rst index 2e276f70..26166d97 100644 --- a/docs/source/security-analysis.rst +++ b/docs/source/security-analysis.rst @@ -1,7 +1,7 @@ Security Analysis ================= -Run :code:`myth -x` with one of the input options described below will run the analysis modules in the `/analysis/modules `_ directory. +Run :code:`myth analyze` with one of the input options described below will run the analysis modules in the `/analysis/modules `_ directory. *********************** Analyzing Solidity Code diff --git a/mythril/__version__.py b/mythril/__version__.py index 3490630e..9085271a 100644 --- a/mythril/__version__.py +++ b/mythril/__version__.py @@ -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.12" +__version__ = "v0.21.17" diff --git a/mythril/analysis/analysis_args.py b/mythril/analysis/analysis_args.py new file mode 100644 index 00000000..fcd5fc36 --- /dev/null +++ b/mythril/analysis/analysis_args.py @@ -0,0 +1,30 @@ +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() diff --git a/mythril/analysis/call_helpers.py b/mythril/analysis/call_helpers.py index 6cb796df..cb6f55d7 100644 --- a/mythril/analysis/call_helpers.py +++ b/mythril/analysis/call_helpers.py @@ -4,6 +4,7 @@ from typing import Union from mythril.analysis.ops import VarType, Call, get_variable from mythril.laser.ethereum.state.global_state import GlobalState +from mythril.laser.ethereum.natives import PRECOMPILE_COUNT def get_call_from_state(state: GlobalState) -> Union[Call, None]: @@ -17,7 +18,7 @@ def get_call_from_state(state: GlobalState) -> Union[Call, None]: op = instruction["opcode"] stack = state.mstate.stack - if op in ("CALL", "CALLCODE", "STATICCALL"): + if op in ("CALL", "CALLCODE"): gas, to, value, meminstart, meminsz, memoutstart, memoutsz = ( get_variable(stack[-1]), get_variable(stack[-2]), @@ -28,7 +29,7 @@ def get_call_from_state(state: GlobalState) -> Union[Call, None]: get_variable(stack[-7]), ) - if to.type == VarType.CONCRETE and 0 < to.val < 5: + if to.type == VarType.CONCRETE and 0 < to.val <= PRECOMPILE_COUNT: return None if meminstart.type == VarType.CONCRETE and meminsz.type == VarType.CONCRETE: diff --git a/mythril/analysis/modules/base.py b/mythril/analysis/modules/base.py index d45072fd..bcecf6a7 100644 --- a/mythril/analysis/modules/base.py +++ b/mythril/analysis/modules/base.py @@ -3,6 +3,7 @@ modules.""" import logging from typing import List, Set + from mythril.analysis.report import Issue log = logging.getLogger(__name__) @@ -34,21 +35,14 @@ class DetectionModule: self.name, ) self.entrypoint = entrypoint - self._issues = [] # type: List[Issue] - self._cache = set() # type: Set[int] - - @property - def issues(self): - """ - Returns the issues - """ - return self._issues + self.issues = [] # type: List[Issue] + self.cache = set() # type: Set[int] def reset_module(self): """ Resets issues """ - self._issues = [] + self.issues = [] def execute(self, statespace) -> None: """The entry point for execution, which is being called by Mythril. diff --git a/mythril/analysis/modules/delegatecall.py b/mythril/analysis/modules/delegatecall.py index b0e0435d..e9229468 100644 --- a/mythril/analysis/modules/delegatecall.py +++ b/mythril/analysis/modules/delegatecall.py @@ -1,79 +1,24 @@ """This module contains the detection code for insecure delegate call usage.""" -import json import logging -from copy import copy -from typing import List, cast, Dict +from typing import List -from mythril.analysis import solver +from mythril.analysis.potential_issues import ( + get_potential_issues_annotation, + PotentialIssue, +) from mythril.analysis.swc_data import DELEGATECALL_TO_UNTRUSTED_CONTRACT from mythril.laser.ethereum.transaction.symbolic import ATTACKER_ADDRESS from mythril.laser.ethereum.transaction.transaction_models import ( ContractCreationTransaction, ) -from mythril.analysis.report import Issue from mythril.analysis.modules.base import DetectionModule from mythril.exceptions import UnsatError -from mythril.laser.ethereum.state.annotation import StateAnnotation from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.smt import symbol_factory, UGT log = logging.getLogger(__name__) -class DelegateCallAnnotation(StateAnnotation): - def __init__(self, call_state: GlobalState, constraints: List) -> None: - """ - Initialize DelegateCall Annotation - :param call_state: Call state - """ - self.call_state = call_state - self.constraints = constraints - self.return_value = call_state.new_bitvec( - "retval_{}".format(call_state.get_current_instruction()["address"]), 256 - ) - - def _copy__(self): - return DelegateCallAnnotation(self.call_state, copy(self.constraints)) - - def get_issue(self, global_state: GlobalState, transaction_sequence: Dict) -> Issue: - """ - Returns Issue for the annotation - :param global_state: Global State - :param transaction_sequence: Transaction sequence - :return: Issue - """ - - address = self.call_state.get_current_instruction()["address"] - logging.debug( - "[DELEGATECALL] Detected delegatecall to a user-supplied address : {}".format( - address - ) - ) - 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. " - ) - - return Issue( - contract=self.call_state.environment.active_account.contract_name, - function_name=self.call_state.environment.active_function_name, - address=address, - swc_id=DELEGATECALL_TO_UNTRUSTED_CONTRACT, - title="Delegatecall Proxy To User-Supplied Address", - bytecode=global_state.environment.code.bytecode, - severity="Medium", - description_head=description_head, - description_tail=description_tail, - transaction_sequence=transaction_sequence, - gas_used=( - global_state.mstate.min_gas_used, - global_state.mstate.max_gas_used, - ), - ) - - class DelegateCallModule(DetectionModule): """This module detects calldata being forwarded using DELEGATECALL.""" @@ -84,7 +29,7 @@ class DelegateCallModule(DetectionModule): swc_id=DELEGATECALL_TO_UNTRUSTED_CONTRACT, description="Check for invocations of delegatecall(msg.data) in the fallback function.", entrypoint="callback", - pre_hooks=["DELEGATECALL", "RETURN", "STOP"], + pre_hooks=["DELEGATECALL"], ) def _execute(self, state: GlobalState) -> None: @@ -93,63 +38,68 @@ class DelegateCallModule(DetectionModule): :param state: :return: """ - if state.get_current_instruction()["address"] in self._cache: + 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) + potential_issues = self._analyze_state(state) + + annotation = get_potential_issues_annotation(state) + annotation.potential_issues.extend(potential_issues) - @staticmethod - def _analyze_state(state: GlobalState) -> List[Issue]: + def _analyze_state(self, state: GlobalState) -> List[PotentialIssue]: """ :param state: the current state :return: returns the issues for that corresponding state """ - issues = [] - op_code = state.get_current_instruction()["opcode"] - annotations = cast( - List[DelegateCallAnnotation], - list(state.get_annotations(DelegateCallAnnotation)), - ) + gas = state.mstate.stack[-1] + to = state.mstate.stack[-2] + + constraints = [ + to == ATTACKER_ADDRESS, + UGT(gas, symbol_factory.BitVecVal(2300, 256)), + state.new_bitvec( + "retval_{}".format(state.get_current_instruction()["address"]), 256 + ) + == 1, + ] - if len(annotations) == 0 and op_code in ("RETURN", "STOP"): - return [] + for tx in state.world_state.transaction_sequence: + if not isinstance(tx, ContractCreationTransaction): + constraints.append(tx.caller == ATTACKER_ADDRESS) - if op_code == "DELEGATECALL": - gas = state.mstate.stack[-1] - to = state.mstate.stack[-2] + try: + address = state.get_current_instruction()["address"] - constraints = [ - to == ATTACKER_ADDRESS, - UGT(gas, symbol_factory.BitVecVal(2300, 256)), - ] + logging.debug( + "[DELEGATECALL] Detected potential delegatecall to a user-supplied address : {}".format( + address + ) + ) - for tx in state.world_state.transaction_sequence: - if not isinstance(tx, ContractCreationTransaction): - constraints.append(tx.caller == ATTACKER_ADDRESS) + 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. " + ) - state.annotate(DelegateCallAnnotation(state, constraints)) + return [ + PotentialIssue( + contract=state.environment.active_account.contract_name, + function_name=state.environment.active_function_name, + address=address, + swc_id=DELEGATECALL_TO_UNTRUSTED_CONTRACT, + bytecode=state.environment.code.bytecode, + title="Delegatecall Proxy To User-Supplied Address", + severity="Medium", + description_head=description_head, + description_tail=description_tail, + constraints=constraints, + detector=self, + ) + ] + except UnsatError: return [] - else: - for annotation in annotations: - try: - transaction_sequence = solver.get_transaction_sequence( - state, - state.mstate.constraints - + annotation.constraints - + [annotation.return_value == 1], - ) - issues.append( - annotation.get_issue( - state, transaction_sequence=transaction_sequence - ) - ) - except UnsatError: - continue - - return issues detector = DelegateCallModule() diff --git a/mythril/analysis/modules/dependence_on_predictable_vars.py b/mythril/analysis/modules/dependence_on_predictable_vars.py index 2ff7a454..a9c730fa 100644 --- a/mythril/analysis/modules/dependence_on_predictable_vars.py +++ b/mythril/analysis/modules/dependence_on_predictable_vars.py @@ -74,12 +74,12 @@ class PredictableDependenceModule(DetectionModule): :param state: :return: """ - if state.get_current_instruction()["address"] in self._cache: + 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) + self.cache.add(issue.address) + self.issues.extend(issues) @staticmethod def _analyze_state(state: GlobalState) -> list: diff --git a/mythril/analysis/modules/deprecated_ops.py b/mythril/analysis/modules/deprecated_ops.py index a0b69f98..85766537 100644 --- a/mythril/analysis/modules/deprecated_ops.py +++ b/mythril/analysis/modules/deprecated_ops.py @@ -1,6 +1,8 @@ """This module contains the detection code for deprecated op codes.""" -from mythril.analysis.report import Issue -from mythril.analysis.solver import get_transaction_sequence, UnsatError +from mythril.analysis.potential_issues import ( + PotentialIssue, + get_potential_issues_annotation, +) from mythril.analysis.swc_data import DEPRECATED_FUNCTIONS_USAGE from mythril.analysis.modules.base import DetectionModule from mythril.laser.ethereum.state.global_state import GlobalState @@ -32,15 +34,14 @@ class DeprecatedOperationsModule(DetectionModule): :param state: :return: """ - if state.get_current_instruction()["address"] in self._cache: + 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): + annotation = get_potential_issues_annotation(state) + annotation.potential_issues.extend(issues) + + def _analyze_state(self, state): """ :param state: @@ -74,27 +75,22 @@ class DeprecatedOperationsModule(DetectionModule): ) swc_id = DEPRECATED_FUNCTIONS_USAGE else: - return - try: - transaction_sequence = get_transaction_sequence( - state, state.mstate.constraints - ) - except UnsatError: - return - issue = Issue( + 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, - gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), - transaction_sequence=transaction_sequence, + constraints=[], ) - return [issue] + return [potential_issue] detector = DeprecatedOperationsModule() diff --git a/mythril/analysis/modules/dos.py b/mythril/analysis/modules/dos.py index 20426727..cb9ac2f3 100644 --- a/mythril/analysis/modules/dos.py +++ b/mythril/analysis/modules/dos.py @@ -7,6 +7,7 @@ from mythril.analysis.swc_data import DOS_WITH_BLOCK_GAS_LIMIT from mythril.analysis.report import Issue from mythril.analysis.modules.base import DetectionModule from mythril.analysis.solver import get_transaction_sequence, UnsatError +from mythril.analysis.analysis_args import analysis_args from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.state.annotation import StateAnnotation from mythril.laser.ethereum import util @@ -55,7 +56,7 @@ class DosModule(DetectionModule): :return: """ issues = self._analyze_state(state) - self._issues.extend(issues) + self.issues.extend(issues) def _analyze_state(self, state: GlobalState) -> List[Issue]: """ @@ -90,7 +91,7 @@ class DosModule(DetectionModule): else: annotation.jump_targets[target] = 1 - if annotation.jump_targets[target] > 2: + if annotation.jump_targets[target] > min(2, analysis_args.loop_bound - 1): annotation.loop_start = address elif annotation.loop_start is not None: diff --git a/mythril/analysis/modules/ether_thief.py b/mythril/analysis/modules/ether_thief.py index 76952a54..13066795 100644 --- a/mythril/analysis/modules/ether_thief.py +++ b/mythril/analysis/modules/ether_thief.py @@ -1,28 +1,28 @@ """This module contains the detection code for unauthorized ether withdrawal.""" import logging -import json from copy import copy -from mythril.analysis import solver from mythril.analysis.modules.base import DetectionModule -from mythril.analysis.report import Issue +from mythril.analysis.potential_issues import ( + get_potential_issues_annotation, + PotentialIssue, +) from mythril.laser.ethereum.transaction.symbolic import ( ATTACKER_ADDRESS, CREATOR_ADDRESS, ) from mythril.analysis.swc_data import UNPROTECTED_ETHER_WITHDRAWAL -from mythril.exceptions import UnsatError -from mythril.laser.ethereum.transaction import ContractCreationTransaction from mythril.laser.ethereum.state.global_state import GlobalState -from mythril.laser.smt import UGT, Sum, symbol_factory, BVAddNoOverflow -from mythril.laser.smt.bitvec import If +from mythril.laser.ethereum.transaction import ContractCreationTransaction + +from mythril.laser.smt import UGT, symbol_factory, UGE log = logging.getLogger(__name__) DESCRIPTION = """ -Search for cases where Ether can be withdrawn to a user-specified address. +Search for cases where Ether can be withdrawn to a user-specified address. An issue is reported if: @@ -61,90 +61,77 @@ class EtherThief(DetectionModule): :param state: :return: """ - if state.get_current_instruction()["address"] in self._cache: + 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) + potential_issues = self._analyze_state(state) - @staticmethod - def _analyze_state(state): + annotation = get_potential_issues_annotation(state) + annotation.potential_issues.extend(potential_issues) + + def _analyze_state(self, state): """ :param state: :return: """ + state = copy(state) instruction = state.get_current_instruction() - if instruction["opcode"] != "CALL": - return [] - - address = instruction["address"] - value = state.mstate.stack[-3] target = state.mstate.stack[-2] - eth_sent_by_attacker = symbol_factory.BitVecVal(0, 256) - constraints = copy(state.mstate.constraints) + """ + Require that the current transaction is sent by the attacker and + that the Ether sent to the attacker's address is greater than the + amount of Ether the attacker sent. + """ for tx in state.world_state.transaction_sequence: - """ - Constraint: The call value must be greater than the sum of Ether sent by the attacker over all - transactions. This prevents false positives caused by legitimate refund functions. - Also constrain the addition from overflowing (otherwise the solver produces solutions with - ridiculously high call values). - """ - constraints += [BVAddNoOverflow(eth_sent_by_attacker, tx.call_value, False)] - eth_sent_by_attacker = Sum( - eth_sent_by_attacker, - tx.call_value * If(tx.caller == ATTACKER_ADDRESS, 1, 0), - ) - """ Constraint: All transactions must originate from regular users (not the creator/owner). This prevents false positives where the owner willingly transfers ownership to another address. """ - if not isinstance(tx, ContractCreationTransaction): constraints += [tx.caller != CREATOR_ADDRESS] - """ - Require that the current transaction is sent by the attacker and - that the Ether is sent to the attacker's address. - """ + attacker_address_bitvec = symbol_factory.BitVecVal(ATTACKER_ADDRESS, 256) constraints += [ - UGT(value, eth_sent_by_attacker), + UGE( + state.world_state.balances[state.environment.active_account.address], + value, + ) + ] + state.world_state.balances[attacker_address_bitvec] += value + state.world_state.balances[state.environment.active_account.address] -= value + + constraints += [ + UGT( + state.world_state.balances[attacker_address_bitvec], + state.world_state.starting_balances[attacker_address_bitvec], + ), target == ATTACKER_ADDRESS, state.current_transaction.caller == ATTACKER_ADDRESS, ] - try: - - transaction_sequence = solver.get_transaction_sequence(state, constraints) - - issue = Issue( - contract=state.environment.active_account.contract_name, - function_name=state.environment.active_function_name, - address=instruction["address"], - swc_id=UNPROTECTED_ETHER_WITHDRAWAL, - title="Unprotected Ether Withdrawal", - severity="High", - bytecode=state.environment.code.bytecode, - description_head="Anyone can withdraw ETH from the contract account.", - description_tail="Arbitrary senders other than the contract creator can withdraw ETH from the contract" - + " account without previously having sent an equivalent amount of ETH to it. This is likely to be" - + " a vulnerability.", - transaction_sequence=transaction_sequence, - gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), - ) - except UnsatError: - log.debug("[ETHER_THIEF] no model found") - return [] + potential_issue = PotentialIssue( + contract=state.environment.active_account.contract_name, + function_name=state.environment.active_function_name, + address=instruction["address"], + swc_id=UNPROTECTED_ETHER_WITHDRAWAL, + title="Unprotected Ether Withdrawal", + severity="High", + bytecode=state.environment.code.bytecode, + description_head="Anyone can withdraw ETH from the contract account.", + description_tail="Arbitrary senders other than the contract creator can withdraw ETH from the contract" + + " account without previously having sent an equivalent amount of ETH to it. This is likely to be" + + " a vulnerability.", + detector=self, + constraints=constraints, + ) - return [issue] + return [potential_issue] detector = EtherThief() diff --git a/mythril/analysis/modules/exceptions.py b/mythril/analysis/modules/exceptions.py index fe593e8d..804df576 100644 --- a/mythril/analysis/modules/exceptions.py +++ b/mythril/analysis/modules/exceptions.py @@ -33,8 +33,8 @@ class ReachableExceptionsModule(DetectionModule): """ issues = self._analyze_state(state) for issue in issues: - self._cache.add(issue.address) - self._issues.extend(issues) + self.cache.add(issue.address) + self.issues.extend(issues) @staticmethod def _analyze_state(state) -> list: diff --git a/mythril/analysis/modules/external_calls.py b/mythril/analysis/modules/external_calls.py index e80c8802..8a249a74 100644 --- a/mythril/analysis/modules/external_calls.py +++ b/mythril/analysis/modules/external_calls.py @@ -2,19 +2,23 @@ calls.""" from mythril.analysis import solver +from mythril.analysis.potential_issues import ( + PotentialIssue, + get_potential_issues_annotation, +) from mythril.analysis.swc_data import REENTRANCY +from mythril.laser.ethereum.state.constraints import Constraints from mythril.laser.ethereum.transaction.symbolic import ATTACKER_ADDRESS from mythril.laser.ethereum.transaction.transaction_models import ( ContractCreationTransaction, ) from mythril.analysis.modules.base import DetectionModule -from mythril.analysis.report import Issue from mythril.laser.smt import UGT, symbol_factory, Or, BitVec +from mythril.laser.ethereum.natives import PRECOMPILE_COUNT from mythril.laser.ethereum.state.global_state import GlobalState from mythril.exceptions import UnsatError from copy import copy import logging -import json log = logging.getLogger(__name__) @@ -33,7 +37,7 @@ def _is_precompile_call(global_state: GlobalState): constraints += [ Or( to < symbol_factory.BitVecVal(1, 256), - to > symbol_factory.BitVecVal(16, 256), + to > symbol_factory.BitVecVal(PRECOMPILE_COUNT, 256), ) ] @@ -64,13 +68,12 @@ class ExternalCalls(DetectionModule): :param state: :return: """ - issues = self._analyze_state(state) - for issue in issues: - self._cache.add(issue.address) - self._issues.extend(issues) + potential_issues = self._analyze_state(state) + + annotation = get_potential_issues_annotation(state) + annotation.potential_issues.extend(potential_issues) - @staticmethod - def _analyze_state(state): + def _analyze_state(self, state: GlobalState): """ :param state: @@ -82,10 +85,10 @@ class ExternalCalls(DetectionModule): address = state.get_current_instruction()["address"] try: - constraints = copy(state.mstate.constraints) + constraints = Constraints([UGT(gas, symbol_factory.BitVecVal(2300, 256))]) transaction_sequence = solver.get_transaction_sequence( - state, constraints + [UGT(gas, symbol_factory.BitVecVal(2300, 256))] + state, constraints + state.mstate.constraints ) # Check whether we can also set the callee address @@ -98,7 +101,7 @@ class ExternalCalls(DetectionModule): constraints.append(tx.caller == ATTACKER_ADDRESS) transaction_sequence = solver.get_transaction_sequence( - state, constraints + state, constraints + state.mstate.constraints ) description_head = "A call to a user-supplied address is executed." @@ -109,7 +112,7 @@ class ExternalCalls(DetectionModule): "contract state." ) - issue = Issue( + issue = PotentialIssue( contract=state.environment.active_account.contract_name, function_name=state.environment.active_function_name, address=address, @@ -119,8 +122,8 @@ class ExternalCalls(DetectionModule): severity="Medium", description_head=description_head, description_tail=description_tail, - transaction_sequence=transaction_sequence, - gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), + constraints=constraints, + detector=self, ) except UnsatError: @@ -137,7 +140,7 @@ class ExternalCalls(DetectionModule): "that the callee contract has been reviewed carefully." ) - issue = Issue( + issue = PotentialIssue( contract=state.environment.active_account.contract_name, function_name=state.environment.active_function_name, address=address, @@ -147,8 +150,8 @@ class ExternalCalls(DetectionModule): severity="Low", description_head=description_head, description_tail=description_tail, - transaction_sequence=transaction_sequence, - gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), + constraints=constraints, + detector=self, ) except UnsatError: diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index c7c7c24a..78d93f31 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -113,7 +113,7 @@ class IntegerOverflowUnderflowModule(DetectionModule): address = _get_address_from_state(state) - if address in self._cache: + if address in self.cache: return opcode = state.get_current_instruction()["opcode"] @@ -331,8 +331,8 @@ class IntegerOverflowUnderflowModule(DetectionModule): ) address = _get_address_from_state(ostate) - self._cache.add(address) - self._issues.append(issue) + self.cache.add(address) + self.issues.append(issue) detector = IntegerOverflowUnderflowModule() diff --git a/mythril/analysis/modules/multiple_sends.py b/mythril/analysis/modules/multiple_sends.py index be3b7474..e6b95085 100644 --- a/mythril/analysis/modules/multiple_sends.py +++ b/mythril/analysis/modules/multiple_sends.py @@ -45,12 +45,12 @@ class MultipleSendsModule(DetectionModule): ) def _execute(self, state: GlobalState) -> None: - if state.get_current_instruction()["address"] in self._cache: + 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) + self.cache.add(issue.address) + self.issues.extend(issues) @staticmethod def _analyze_state(state: GlobalState): diff --git a/mythril/analysis/modules/state_change_external_calls.py b/mythril/analysis/modules/state_change_external_calls.py index 9b331dd0..a05f4ffd 100644 --- a/mythril/analysis/modules/state_change_external_calls.py +++ b/mythril/analysis/modules/state_change_external_calls.py @@ -1,6 +1,10 @@ +from mythril.analysis.potential_issues import ( + PotentialIssue, + get_potential_issues_annotation, +) from mythril.analysis.swc_data import REENTRANCY from mythril.analysis.modules.base import DetectionModule -from mythril.analysis.report import Issue +from mythril.laser.ethereum.state.constraints import Constraints from mythril.laser.smt import symbol_factory, UGT, BitVec, Or from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.state.annotation import StateAnnotation @@ -32,10 +36,12 @@ class StateChangeCallsAnnotation(StateAnnotation): new_annotation.state_change_states = self.state_change_states[:] return new_annotation - def get_issue(self, global_state: GlobalState) -> Optional[Issue]: + def get_issue( + self, global_state: GlobalState, detector: DetectionModule + ) -> Optional[PotentialIssue]: if not self.state_change_states: return None - constraints = copy(global_state.mstate.constraints) + constraints = Constraints() gas = self.call_state.mstate.stack[-1] to = self.call_state.mstate.stack[-2] constraints += [ @@ -50,10 +56,11 @@ class StateChangeCallsAnnotation(StateAnnotation): try: transaction_sequence = solver.get_transaction_sequence( - global_state, constraints + global_state, constraints + global_state.mstate.constraints ) except UnsatError: return None + severity = "Medium" if self.user_defined_address else "Low" address = global_state.get_current_instruction()["address"] logging.debug( @@ -67,7 +74,7 @@ class StateChangeCallsAnnotation(StateAnnotation): "state change takes place. This can lead to business logic vulnerabilities." ) - return Issue( + return PotentialIssue( contract=global_state.environment.active_account.contract_name, function_name=global_state.environment.active_function_name, address=address, @@ -77,7 +84,8 @@ class StateChangeCallsAnnotation(StateAnnotation): description_tail=description_tail, swc_id=REENTRANCY, bytecode=global_state.environment.code.bytecode, - transaction_sequence=transaction_sequence, + constraints=constraints, + detector=detector, ) @@ -104,12 +112,12 @@ class StateChange(DetectionModule): ) def _execute(self, state: GlobalState) -> None: - if state.get_current_instruction()["address"] in self._cache: + 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) + + annotation = get_potential_issues_annotation(state) + annotation.potential_issues.extend(issues) @staticmethod def _add_external_call(global_state: GlobalState) -> None: @@ -139,8 +147,7 @@ class StateChange(DetectionModule): except UnsatError: pass - @staticmethod - def _analyze_state(global_state: GlobalState) -> List[Issue]: + def _analyze_state(self, global_state: GlobalState) -> List[PotentialIssue]: annotations = cast( List[StateChangeCallsAnnotation], @@ -171,7 +178,9 @@ class StateChange(DetectionModule): for annotation in annotations: if not annotation.state_change_states: continue - vulnerabilities.append(annotation.get_issue(global_state)) + issue = annotation.get_issue(global_state, self) + if issue: + vulnerabilities.append(issue) return vulnerabilities @staticmethod diff --git a/mythril/analysis/modules/suicide.py b/mythril/analysis/modules/suicide.py index 509b3137..b55fcd3f 100644 --- a/mythril/analysis/modules/suicide.py +++ b/mythril/analysis/modules/suicide.py @@ -46,12 +46,12 @@ class SuicideModule(DetectionModule): :param state: :return: """ - if state.get_current_instruction()["address"] in self._cache: + 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) + self.cache.add(issue.address) + self.issues.extend(issues) @staticmethod def _analyze_state(state): @@ -60,9 +60,7 @@ class SuicideModule(DetectionModule): to = state.mstate.stack[-1] - log.debug( - "[SUICIDE] SUICIDE in function " + state.environment.active_function_name - ) + log.debug("SUICIDE in function %s", state.environment.active_function_name) description_head = "The contract can be killed by anyone." @@ -103,7 +101,7 @@ class SuicideModule(DetectionModule): ) return [issue] except UnsatError: - log.info("[UNCHECKED_SUICIDE] no model found") + log.debug("No model found") return [] diff --git a/mythril/analysis/modules/unchecked_retval.py b/mythril/analysis/modules/unchecked_retval.py index e5e99e3a..5aa8f005 100644 --- a/mythril/analysis/modules/unchecked_retval.py +++ b/mythril/analysis/modules/unchecked_retval.py @@ -55,12 +55,12 @@ class UncheckedRetvalModule(DetectionModule): :param state: :return: """ - if state.get_current_instruction()["address"] in self._cache: + 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) + self.cache.add(issue.address) + self.issues.extend(issues) def _analyze_state(self, state: GlobalState) -> list: instruction = state.get_current_instruction() @@ -116,13 +116,9 @@ class UncheckedRetvalModule(DetectionModule): assert state.environment.code.instruction_list[state.mstate.pc - 1][ "opcode" ] in ["CALL", "DELEGATECALL", "STATICCALL", "CALLCODE"] - retval = state.mstate.stack[-1] - # Use Typed Dict after release of mypy 0.670 and remove type ignore + return_value = state.mstate.stack[-1] retvals.append( - { # type: ignore - "address": state.instruction["address"] - 1, - "retval": retval, - } + {"address": state.instruction["address"] - 1, "retval": return_value} ) return [] diff --git a/mythril/analysis/modules/user_assertions.py b/mythril/analysis/modules/user_assertions.py new file mode 100644 index 00000000..bef9c33a --- /dev/null +++ b/mythril/analysis/modules/user_assertions.py @@ -0,0 +1,100 @@ +"""This module contains the detection code for potentially insecure low-level +calls.""" + +from mythril.analysis.potential_issues import ( + PotentialIssue, + get_potential_issues_annotation, +) +from mythril.analysis.swc_data import ASSERT_VIOLATION +from mythril.analysis.modules.base import DetectionModule +from mythril.laser.ethereum.state.global_state import GlobalState +import logging +import eth_abi + +log = logging.getLogger(__name__) + +DESCRIPTION = """ + +Search for reachable user-supplied exceptions. +Report a warning if an log message is emitted: 'emit AssertionFailed(string)' + +""" + +assertion_failed_hash = ( + 0xB42604CB105A16C8F6DB8A41E6B00C0C1B4826465E8BC504B3EB3E88B3E6A4A0 +) + + +class UserAssertions(DetectionModule): + """This module searches for user supplied exceptions: emit AssertionFailed("Error").""" + + def __init__(self): + """""" + super().__init__( + name="External calls", + swc_id=ASSERT_VIOLATION, + description=DESCRIPTION, + entrypoint="callback", + pre_hooks=["LOG1"], + ) + + def _execute(self, state: GlobalState) -> None: + """ + + :param state: + :return: + """ + potential_issues = self._analyze_state(state) + + annotation = get_potential_issues_annotation(state) + annotation.potential_issues.extend(potential_issues) + + def _analyze_state(self, state: GlobalState): + """ + + :param state: + :return: + """ + topic, size, mem_start = state.mstate.stack[-3:] + + if topic.symbolic or topic.value != assertion_failed_hash: + return [] + + message = None + if not mem_start.symbolic and not size.symbolic: + message = eth_abi.decode_single( + "string", + bytes( + state.mstate.memory[ + mem_start.value + 32 : mem_start.value + size.value + ] + ), + ).decode("utf8") + + 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( + message + ) + else: + description_tail = "A user-provided assertion failed. Make sure the user-provided assertion is correct." + + address = state.get_current_instruction()["address"] + issue = PotentialIssue( + contract=state.environment.active_account.contract_name, + function_name=state.environment.active_function_name, + address=address, + swc_id=ASSERT_VIOLATION, + title="Assertion Failed", + bytecode=state.environment.code.bytecode, + severity="Medium", + description_head=description_head, + description_tail=description_tail, + constraints=[], + detector=self, + ) + + return [issue] + + +detector = UserAssertions() diff --git a/mythril/analysis/potential_issues.py b/mythril/analysis/potential_issues.py new file mode 100644 index 00000000..99340330 --- /dev/null +++ b/mythril/analysis/potential_issues.py @@ -0,0 +1,108 @@ +from mythril.analysis.report import Issue +from mythril.analysis.solver import get_transaction_sequence +from mythril.exceptions import UnsatError +from mythril.laser.ethereum.state.annotation import StateAnnotation +from mythril.laser.ethereum.state.global_state import GlobalState + + +class PotentialIssue: + """Representation of a potential issue""" + + def __init__( + self, + contract, + function_name, + address, + swc_id, + title, + bytecode, + detector, + severity=None, + description_head="", + description_tail="", + constraints=None, + ): + """ + + :param contract: The contract + :param function_name: Function name where the issue is detected + :param address: The address of the issue + :param swc_id: Issue's corresponding swc-id + :param title: Title + :param bytecode: bytecode of the issue + :param detector: The detector the potential issue belongs to + :param gas_used: amount of gas used + :param severity: The severity of the issue + :param description_head: The top part of description + :param description_tail: The bottom part of the description + :param constraints: The non-path related constraints for the potential issue + """ + self.title = title + self.contract = contract + self.function_name = function_name + self.address = address + self.description_head = description_head + self.description_tail = description_tail + self.severity = severity + self.swc_id = swc_id + self.bytecode = bytecode + self.constraints = constraints or [] + self.detector = detector + + +class PotentialIssuesAnnotation(StateAnnotation): + def __init__(self): + self.potential_issues = [] + + +def get_potential_issues_annotation(state: GlobalState) -> PotentialIssuesAnnotation: + """ + Returns the potential issues annotation of the given global state, and creates one if + one does not already exist. + + :param state: The global state + :return: + """ + for annotation in state.annotations: + if isinstance(annotation, PotentialIssuesAnnotation): + return annotation + + annotation = PotentialIssuesAnnotation() + state.annotate(annotation) + return annotation + + +def check_potential_issues(state: GlobalState) -> None: + """ + Called at the end of a transaction, checks potential issues, and + adds valid issues to the detector. + + :param state: The final global state of a transaction + :return: + """ + annotation = get_potential_issues_annotation(state) + for potential_issue in annotation.potential_issues: + try: + transaction_sequence = get_transaction_sequence( + state, state.mstate.constraints + potential_issue.constraints + ) + except UnsatError: + continue + + annotation.potential_issues.remove(potential_issue) + potential_issue.detector.cache.add(potential_issue.address) + potential_issue.detector.issues.append( + Issue( + contract=potential_issue.contract, + function_name=potential_issue.function_name, + address=potential_issue.address, + title=potential_issue.title, + bytecode=potential_issue.bytecode, + swc_id=potential_issue.swc_id, + gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), + severity=potential_issue.severity, + description_head=potential_issue.description_head, + description_tail=potential_issue.description_tail, + transaction_sequence=transaction_sequence, + ) + ) diff --git a/mythril/analysis/report.py b/mythril/analysis/report.py index 1a39c0ff..d40c466b 100644 --- a/mythril/analysis/report.py +++ b/mythril/analysis/report.py @@ -238,7 +238,7 @@ class Report: return {} logs = [] # type: List[Dict] for exception in self.exceptions: - logs += [{"level": "error", "hidden": "true", "msg": exception}] + logs += [{"level": "error", "hidden": True, "msg": exception}] return {"logs": logs} def as_swc_standard_format(self): diff --git a/mythril/analysis/security.py b/mythril/analysis/security.py index 71f0a516..ed741ecb 100644 --- a/mythril/analysis/security.py +++ b/mythril/analysis/security.py @@ -6,22 +6,28 @@ from mythril.analysis import modules import pkgutil import importlib.util import logging +import os +import sys log = logging.getLogger(__name__) OPCODE_LIST = [c[0] for _, c in opcodes.items()] -def reset_callback_modules(): +def reset_callback_modules(module_names=(), custom_modules_directory=""): """Clean the issue records of every callback-based module.""" - modules = get_detection_modules("callback") + modules = get_detection_modules("callback", module_names, custom_modules_directory) for module in modules: module.detector.reset_module() -def get_detection_module_hooks(modules, hook_type="pre"): +def get_detection_module_hooks(modules, hook_type="pre", custom_modules_directory=""): hook_dict = defaultdict(list) - _modules = get_detection_modules(entrypoint="callback", include_modules=modules) + _modules = get_detection_modules( + entrypoint="callback", + include_modules=modules, + custom_modules_directory=custom_modules_directory, + ) for module in _modules: hooks = ( module.detector.pre_hooks @@ -45,14 +51,13 @@ def get_detection_module_hooks(modules, hook_type="pre"): return dict(hook_dict) -def get_detection_modules(entrypoint, include_modules=()): +def get_detection_modules(entrypoint, include_modules=(), custom_modules_directory=""): """ :param entrypoint: :param include_modules: :return: """ - module = importlib.import_module("mythril.analysis.modules.base") module.log.setLevel(log.level) @@ -60,27 +65,35 @@ def get_detection_modules(entrypoint, include_modules=()): _modules = [] - if not include_modules: - for loader, module_name, _ in pkgutil.walk_packages(modules.__path__): + for loader, module_name, _ in pkgutil.walk_packages(modules.__path__): + if include_modules and module_name not in include_modules: + continue + + if module_name != "base": + module = importlib.import_module("mythril.analysis.modules." + module_name) + module.log.setLevel(log.level) + if module.detector.entrypoint == entrypoint: + _modules.append(module) + if custom_modules_directory: + custom_modules_path = os.path.abspath(custom_modules_directory) + if custom_modules_path not in sys.path: + sys.path.append(custom_modules_path) + + for loader, module_name, _ in pkgutil.walk_packages([custom_modules_path]): + if include_modules and module_name not in include_modules: + continue + if module_name != "base": - module = importlib.import_module( - "mythril.analysis.modules." + module_name - ) + module = importlib.import_module(module_name, custom_modules_path) module.log.setLevel(log.level) if module.detector.entrypoint == entrypoint: _modules.append(module) - else: - for module_name in include_modules: - module = importlib.import_module("mythril.analysis.modules." + module_name) - if module.__name__ != "base" and module.detector.entrypoint == entrypoint: - module.log.setLevel(log.level) - _modules.append(module) log.info("Found %s detection modules", len(_modules)) return _modules -def fire_lasers(statespace, module_names=()): +def fire_lasers(statespace, module_names=(), custom_modules_directory=""): """ :param statespace: @@ -91,22 +104,28 @@ def fire_lasers(statespace, module_names=()): issues = [] for module in get_detection_modules( - entrypoint="post", include_modules=module_names + entrypoint="post", + include_modules=module_names, + custom_modules_directory=custom_modules_directory, ): log.info("Executing " + module.detector.name) issues += module.detector.execute(statespace) - issues += retrieve_callback_issues(module_names) + issues += retrieve_callback_issues(module_names, custom_modules_directory) return issues -def retrieve_callback_issues(module_names=()): +def retrieve_callback_issues(module_names=(), custom_modules_directory=""): issues = [] for module in get_detection_modules( - entrypoint="callback", include_modules=module_names + entrypoint="callback", + include_modules=module_names, + custom_modules_directory=custom_modules_directory, ): log.debug("Retrieving results for " + module.detector.name) issues += module.detector.issues - reset_callback_modules() + reset_callback_modules( + module_names=module_names, custom_modules_directory=custom_modules_directory + ) return issues diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index 968215bc..00de6bd4 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -4,6 +4,7 @@ from typing import Dict, Tuple, Union from z3 import sat, unknown, FuncInterp import z3 +from mythril.analysis.analysis_args import analysis_args from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.state.constraints import Constraints from mythril.laser.ethereum.transaction import BaseTransaction @@ -29,7 +30,7 @@ def get_model(constraints, minimize=(), maximize=(), enforce_execution_time=True :return: """ s = Optimize() - timeout = 100000 + timeout = analysis_args.solver_timeout if enforce_execution_time: timeout = min(timeout, time_handler.time_remaining() - 500) if timeout <= 0: @@ -94,7 +95,7 @@ def get_transaction_sequence( concrete_transactions = [] tx_constraints, minimize = _set_minimisation_constraints( - transaction_sequence, constraints.copy(), [], 5000 + transaction_sequence, constraints.copy(), [], 5000, global_state.world_state ) try: @@ -102,19 +103,23 @@ def get_transaction_sequence( except UnsatError: raise UnsatError - min_price_dict = {} # type: Dict[str, int] + # Include creation account in initial state + # Note: This contains the code, which should not exist until after the first tx + initial_world_state = transaction_sequence[0].world_state + initial_accounts = initial_world_state.accounts + for transaction in transaction_sequence: concrete_transaction = _get_concrete_transaction(model, transaction) concrete_transactions.append(concrete_transaction) - caller = concrete_transaction["origin"] - value = int(concrete_transaction["value"], 16) - min_price_dict[caller] = min_price_dict.get(caller, 0) + value - - if isinstance(transaction_sequence[0], ContractCreationTransaction): - initial_accounts = transaction_sequence[0].prev_world_state.accounts - else: - initial_accounts = transaction_sequence[0].world_state.accounts + min_price_dict = {} # type: Dict[str, int] + for address in initial_accounts.keys(): + min_price_dict[address] = model.eval( + initial_world_state.starting_balances[ + symbol_factory.BitVecVal(address, 256) + ].raw, + model_completion=True, + ).as_long() concrete_initial_state = _get_concrete_state(initial_accounts, min_price_dict) @@ -132,7 +137,7 @@ def _get_concrete_state(initial_accounts: Dict, min_price_dict: Dict[str, int]): data = dict() # type: Dict[str, Union[int, str]] data["nonce"] = account.nonce data["code"] = account.code.bytecode - data["storage"] = account.storage.printable_storage + data["storage"] = str(account.storage) data["balance"] = hex(min_price_dict.get(address, 0)) accounts[hex(address)] = data return {"accounts": accounts} @@ -147,16 +152,17 @@ def _get_concrete_transaction(model: z3.Model, transaction: BaseTransaction): "%x" % model.eval(transaction.caller.raw, model_completion=True).as_long() ).zfill(40) + input_ = "" if isinstance(transaction, ContractCreationTransaction): address = "" - input_ = transaction.code.bytecode - else: - input_ = "".join( - [ - hex(b)[2:] if len(hex(b)) % 2 == 0 else "0" + hex(b)[2:] - for b in transaction.call_data.concrete(model) - ] - ) + input_ += transaction.code.bytecode + + input_ += "".join( + [ + hex(b)[2:] if len(hex(b)) % 2 == 0 else "0" + hex(b)[2:] + for b in transaction.call_data.concrete(model) + ] + ) # Create concrete transaction dict concrete_transaction = dict() # type: Dict[str, str] @@ -170,7 +176,7 @@ def _get_concrete_transaction(model: z3.Model, transaction: BaseTransaction): def _set_minimisation_constraints( - transaction_sequence, constraints, minimize, max_size + transaction_sequence, constraints, minimize, max_size, world_state ) -> Tuple[Constraints, tuple]: """ Set constraints that minimise key transaction values @@ -192,5 +198,21 @@ def _set_minimisation_constraints( # Minimize minimize.append(transaction.call_data.calldatasize) minimize.append(transaction.call_value) + constraints.append( + UGE( + symbol_factory.BitVecVal(1000000000000000000000, 256), + world_state.starting_balances[transaction.caller], + ) + ) + + for account in world_state.accounts.values(): + # Lazy way to prevent overflows and to ensure "reasonable" balances + # Each account starts with less than 100 ETH + constraints.append( + UGE( + symbol_factory.BitVecVal(100000000000000000000, 256), + world_state.starting_balances[account.address], + ) + ) return constraints, tuple(minimize) diff --git a/mythril/analysis/symbolic.py b/mythril/analysis/symbolic.py index e6c2bf24..ce98b0ce 100644 --- a/mythril/analysis/symbolic.py +++ b/mythril/analysis/symbolic.py @@ -14,6 +14,7 @@ from mythril.laser.ethereum.strategy.basic import ( BasicSearchStrategy, ) +from mythril.laser.ethereum.natives import PRECOMPILE_COUNT from mythril.laser.ethereum.transaction.symbolic import ( ATTACKER_ADDRESS, CREATOR_ADDRESS, @@ -47,7 +48,7 @@ class SymExecWrapper: dynloader=None, max_depth=22, execution_timeout=None, - loop_bound=2, + loop_bound=3, create_timeout=None, transaction_count=2, modules=(), @@ -55,6 +56,8 @@ class SymExecWrapper: enable_iprof=False, disable_dependency_pruning=False, run_analysis_modules=True, + enable_coverage_strategy=False, + custom_modules_directory="", ): """ @@ -92,7 +95,8 @@ class SymExecWrapper: ) requires_statespace = ( - compulsory_statespace or len(get_detection_modules("post", modules)) > 0 + compulsory_statespace + or len(get_detection_modules("post", modules, custom_modules_directory)) > 0 ) if not contract.creation_code: self.accounts = {hex(ATTACKER_ADDRESS): attacker_account} @@ -102,6 +106,8 @@ class SymExecWrapper: hex(ATTACKER_ADDRESS): attacker_account, } + instruction_laser_plugin = PluginFactory.build_instruction_coverage_plugin() + self.laser = svm.LaserEVM( dynamic_loader=dynloader, max_depth=max_depth, @@ -111,6 +117,8 @@ class SymExecWrapper: transaction_count=transaction_count, requires_statespace=requires_statespace, enable_iprof=enable_iprof, + enable_coverage_strategy=enable_coverage_strategy, + instruction_laser_plugin=instruction_laser_plugin, ) if loop_bound is not None: @@ -118,7 +126,7 @@ class SymExecWrapper: plugin_loader = LaserPluginLoader(self.laser) plugin_loader.load(PluginFactory.build_mutation_pruner_plugin()) - plugin_loader.load(PluginFactory.build_instruction_coverage_plugin()) + plugin_loader.load(instruction_laser_plugin) if not disable_dependency_pruning: plugin_loader.load(PluginFactory.build_dependency_pruner_plugin()) @@ -130,11 +138,19 @@ class SymExecWrapper: if run_analysis_modules: self.laser.register_hooks( hook_type="pre", - hook_dict=get_detection_module_hooks(modules, hook_type="pre"), + hook_dict=get_detection_module_hooks( + modules, + hook_type="pre", + custom_modules_directory=custom_modules_directory, + ), ) self.laser.register_hooks( hook_type="post", - hook_dict=get_detection_module_hooks(modules, hook_type="post"), + hook_dict=get_detection_module_hooks( + modules, + hook_type="post", + custom_modules_directory=custom_modules_directory, + ), ) if isinstance(contract, SolidityContract): @@ -197,7 +213,10 @@ class SymExecWrapper: get_variable(stack[-7]), ) - if to.type == VarType.CONCRETE and to.val < 5: + if ( + to.type == VarType.CONCRETE + and 0 < to.val <= PRECOMPILE_COUNT + ): # ignore prebuilts continue diff --git a/mythril/analysis/templates/report_as_markdown.jinja2 b/mythril/analysis/templates/report_as_markdown.jinja2 index 4583eb26..360648ea 100644 --- a/mythril/analysis/templates/report_as_markdown.jinja2 +++ b/mythril/analysis/templates/report_as_markdown.jinja2 @@ -6,15 +6,21 @@ - SWC ID: {{ issue['swc-id'] }} - Severity: {{ issue.severity }} - Contract: {{ issue.contract | default("Unknown") }} +{% if issue.function %} - Function name: `{{ issue.function }}` +{% endif %} - PC address: {{ issue.address }} +{% if issue.min_gas_used or issue.max_gas_used %} - Estimated Gas Usage: {{ issue.min_gas_used }} - {{ issue.max_gas_used }} +{% endif %} ### Description {{ issue.description.rstrip() }} {% if issue.filename and issue.lineno %} In file: {{ issue.filename }}:{{ issue.lineno }} +{% elif issue.filename %} +In file: {{ issue.filename }} {% endif %} {% if issue.code %} @@ -26,11 +32,17 @@ In file: {{ issue.filename }}:{{ issue.lineno }} {% endif %} {% if issue.tx_sequence %} +### Initial State: + +{% for key, value in issue.tx_sequence.initialState.accounts.items() %} +Account: {% if key == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %}[CREATOR]{% elif key == "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef" %}[ATTACKER]{% else %}[SOMEGUY]{% endif %}, balance: {{value.balance}}, nonce:{{value.nonce}}, storage:{{value.storage}} +{% endfor %} + ### Transaction Sequence {% for step in issue.tx_sequence.steps %} {% if step == issue.tx_sequence.steps[0] and step.input != "0x" and step.origin == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %} -Caller: [CREATOR], data: [CONTRACT CREATION], value: {{ step.value }} +Caller: [CREATOR], data: {{ step.input }}, value: {{ step.value }} {% else %} Caller: {% if step.origin == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %}[CREATOR]{% elif step.origin == "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef" %}[ATTACKER]{% else %}[SOMEGUY]{% endif %}, function: {{ step.name }}, txdata: {{ step.input }}, value: {{ step.value }} {% endif %} diff --git a/mythril/analysis/templates/report_as_text.jinja2 b/mythril/analysis/templates/report_as_text.jinja2 index d7b84355..1488807c 100644 --- a/mythril/analysis/templates/report_as_text.jinja2 +++ b/mythril/analysis/templates/report_as_text.jinja2 @@ -4,9 +4,13 @@ SWC ID: {{ issue['swc-id'] }} Severity: {{ issue.severity }} Contract: {{ issue.contract | default("Unknown") }} +{% if issue.function %} Function name: {{ issue.function }} +{% endif %} PC address: {{ issue.address }} +{% if issue.min_gas_used or issue.max_gas_used %} Estimated Gas Usage: {{ issue.min_gas_used }} - {{ issue.max_gas_used }} +{% endif %} {{ issue.description }} -------------------- {% if issue.filename and issue.lineno %} @@ -19,11 +23,17 @@ In file: {{ issue.filename }}:{{ issue.lineno }} -------------------- {% endif %} {% if issue.tx_sequence %} +Initial State: + +{% for key, value in issue.tx_sequence.initialState.accounts.items() %} +Account: {% if key == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %}[CREATOR]{% elif key == "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef" %}[ATTACKER]{% else %}[SOMEGUY]{% endif %}, balance: {{value.balance}}, nonce:{{value.nonce}}, storage:{{value.storage}} +{% endfor %} + Transaction Sequence: {% for step in issue.tx_sequence.steps %} {% if step == issue.tx_sequence.steps[0] and step.input != "0x" and step.origin == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %} -Caller: [CREATOR], data: [CONTRACT CREATION], value: {{ step.value }} +Caller: [CREATOR], data: {{ step.input }}, value: {{ step.value }} {% else %} Caller: {% if step.origin == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %}[CREATOR]{% elif step.origin == "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef" %}[ATTACKER]{% else %}[SOMEGUY]{% endif %}, function: {{ step.name }}, txdata: {{ step.input }}, value: {{ step.value }} {% endif %} diff --git a/mythril/ethereum/util.py b/mythril/ethereum/util.py index 2b6c7771..0fd72dcb 100644 --- a/mythril/ethereum/util.py +++ b/mythril/ethereum/util.py @@ -3,6 +3,7 @@ solc integration.""" import binascii import json import os +import solcx from pathlib import Path from subprocess import PIPE, Popen @@ -24,39 +25,44 @@ def safe_decode(hex_encoded_string): return bytes.fromhex(hex_encoded_string) -def get_solc_json(file, solc_binary="solc", solc_args=None): +def get_solc_json(file, solc_binary="solc", solc_settings_json=None): """ :param file: :param solc_binary: - :param solc_args: + :param solc_settings_json: :return: """ - - cmd = [solc_binary, "--combined-json", "bin,bin-runtime,srcmap,srcmap-runtime,ast"] - - if solc_args: - cmd.extend(solc_args.split()) - if not "--allow-paths" in cmd: - cmd.extend(["--allow-paths", "."]) - else: - for i, arg in enumerate(cmd): - if arg == "--allow-paths": - cmd[i + 1] += ",." - - cmd.append(file) + cmd = [solc_binary, "--standard-json", "--allow-paths", "."] + + settings = json.loads(solc_settings_json) if solc_settings_json else {} + settings.update( + { + "outputSelection": { + "*": { + "": ["ast"], + "*": [ + "metadata", + "evm.bytecode", + "evm.deployedBytecode", + "evm.methodIdentifiers", + ], + } + } + } + ) + input_json = json.dumps( + { + "language": "Solidity", + "sources": {file: {"urls": [file]}}, + "settings": settings, + } + ) try: - p = Popen(cmd, stdout=PIPE, stderr=PIPE) + p = Popen(cmd, stdin=PIPE, stdout=PIPE, stderr=PIPE) + stdout, stderr = p.communicate(bytes(input_json, "utf8")) - stdout, stderr = p.communicate() - ret = p.returncode - - if ret != 0: - raise CompilerError( - "Solc experienced a fatal error (code %d).\n\n%s" - % (ret, stderr.decode("UTF-8")) - ) except FileNotFoundError: raise CompilerError( "Compiler not found. Make sure that solc is installed and in PATH, or set the SOLC environment variable." @@ -64,10 +70,15 @@ def get_solc_json(file, solc_binary="solc", solc_args=None): out = stdout.decode("UTF-8") - if not len(out): - raise CompilerError("Compilation failed.") + result = json.loads(out) - return json.loads(out) + for error in result.get("errors", []): + if error["severity"] == "error": + raise CompilerError( + "Solc experienced a fatal error.\n\n%s" % error["formattedMessage"] + ) + + return result def encode_calldata(func_name, arg_types, args): @@ -107,16 +118,25 @@ def solc_exists(version): :param version: :return: """ - solc_binaries = [ - os.path.join( - os.environ.get("HOME", str(Path.home())), - ".py-solc/solc-v" + version, - "bin/solc", - ) # py-solc setup - ] - if version.startswith("0.5"): - # Temporary fix to support v0.5.x with Ubuntu PPA setup - solc_binaries.append("/usr/bin/solc") + + solc_binaries = [] + if version.startswith("0.4"): + solc_binaries = [ + os.path.join( + os.environ.get("HOME", str(Path.home())), + ".py-solc/solc-v" + version, + "bin/solc", + ) # py-solc setup + ] + else: + # we are using solc-x for the the 0.5 and higher + solc_binaries = [os.path.join(solcx.__path__[0], "bin", "solc-v" + version)] + for solc_path in solc_binaries: if os.path.exists(solc_path): return solc_path + + # Last resort is to use the system installation + default_binary = "/usr/bin/solc" + if os.path.exists(default_binary): + return default_binary diff --git a/mythril/interfaces/cli.py b/mythril/interfaces/cli.py index fc665b8a..1501120f 100644 --- a/mythril/interfaces/cli.py +++ b/mythril/interfaces/cli.py @@ -15,7 +15,8 @@ import coloredlogs import traceback import mythril.support.signatures as sigs -from argparse import ArgumentParser, Namespace +from argparse import ArgumentParser, Namespace, RawTextHelpFormatter +from mythril import mythx from mythril.exceptions import AddressNotFoundError, CriticalError from mythril.mythril import ( MythrilAnalyzer, @@ -27,12 +28,14 @@ from mythril.__version__ import __version__ as VERSION ANALYZE_LIST = ("analyze", "a") DISASSEMBLE_LIST = ("disassemble", "d") +PRO_LIST = ("pro", "p") log = logging.getLogger(__name__) COMMAND_LIST = ( ANALYZE_LIST + DISASSEMBLE_LIST + + PRO_LIST + ( "read-storage", "leveldb-search", @@ -41,6 +44,7 @@ COMMAND_LIST = ( "version", "truffle", "help", + "pro", ) ) @@ -63,16 +67,34 @@ def exit_with_error(format_, message): "sourceType": "", "sourceFormat": "", "sourceList": [], - "meta": { - "logs": [{"level": "error", "hidden": "true", "msg": message}] - }, + "meta": {"logs": [{"level": "error", "hidden": True, "msg": message}]}, } ] print(json.dumps(result)) sys.exit() -def get_input_parser() -> ArgumentParser: +def get_runtime_input_parser() -> ArgumentParser: + """ + Returns Parser which handles input + :return: Parser which handles input + """ + parser = ArgumentParser(add_help=False) + parser.add_argument( + "-a", + "--address", + help="pull contract from the blockchain", + metavar="CONTRACT_ADDRESS", + ) + parser.add_argument( + "--bin-runtime", + action="store_true", + help="Only when -c or -f is used. Consider the input bytecode as binary runtime code, default being the contract creation bytecode.", + ) + return parser + + +def get_creation_input_parser() -> ArgumentParser: """ Returns Parser which handles input :return: Parser which handles input @@ -91,17 +113,6 @@ def get_input_parser() -> ArgumentParser: metavar="BYTECODEFILE", type=argparse.FileType("r"), ) - parser.add_argument( - "-a", - "--address", - help="pull contract from the blockchain", - metavar="CONTRACT_ADDRESS", - ) - parser.add_argument( - "--bin-runtime", - action="store_true", - help="Only when -c or -f is used. Consider the input bytecode as binary runtime code, default being the contract creation bytecode.", - ) return parser @@ -146,7 +157,10 @@ def get_utilities_parser() -> ArgumentParser: :return: Parser which handles utility flags """ parser = argparse.ArgumentParser(add_help=False) - parser.add_argument("--solc-args", help="Extra arguments for solc") + parser.add_argument( + "--solc-json", + help="Json for the optional 'settings' parameter of solc's standard-json input", + ) parser.add_argument( "--solv", help="specify solidity compiler version. If not present, will try to install it (Experimental)", @@ -160,7 +174,8 @@ def main() -> None: rpc_parser = get_rpc_parser() utilities_parser = get_utilities_parser() - input_parser = get_input_parser() + runtime_input_parser = get_runtime_input_parser() + creation_input_parser = get_creation_input_parser() output_parser = get_output_parser() parser = argparse.ArgumentParser( description="Security analysis of Ethereum smart contracts" @@ -174,8 +189,15 @@ def main() -> None: analyzer_parser = subparsers.add_parser( ANALYZE_LIST[0], help="Triggers the analysis of the smart contract", - parents=[rpc_parser, utilities_parser, input_parser, output_parser], + parents=[ + rpc_parser, + utilities_parser, + creation_input_parser, + runtime_input_parser, + output_parser, + ], aliases=ANALYZE_LIST[1:], + formatter_class=RawTextHelpFormatter, ) create_analyzer_parser(analyzer_parser) @@ -183,10 +205,25 @@ def main() -> None: DISASSEMBLE_LIST[0], help="Disassembles the smart contract", aliases=DISASSEMBLE_LIST[1:], - parents=[rpc_parser, utilities_parser, input_parser], + parents=[ + rpc_parser, + utilities_parser, + creation_input_parser, + runtime_input_parser, + ], + formatter_class=RawTextHelpFormatter, ) create_disassemble_parser(disassemble_parser) + pro_parser = subparsers.add_parser( + PRO_LIST[0], + help="Analyzes input with the MythX API (https://mythx.io)", + aliases=PRO_LIST[1:], + parents=[utilities_parser, creation_input_parser, output_parser], + formatter_class=RawTextHelpFormatter, + ) + create_pro_parser(pro_parser) + read_storage_parser = subparsers.add_parser( "read-storage", help="Retrieves storage slots from a given address through rpc", @@ -225,7 +262,32 @@ def create_disassemble_parser(parser: ArgumentParser): :param parser: :return: """ - parser.add_argument("solidity_file", nargs="*") + # Using nargs=* would the implementation below for getting code for both disassemble and analyze + parser.add_argument( + "solidity_files", + nargs="*", + help="Inputs file name and contract name. Currently supports a single contract\n" + "usage: file1.sol:OptionalContractName", + ) + + +def create_pro_parser(parser: ArgumentParser): + """ + Modify parser to handle mythx analysis + :param parser: + :return: + """ + parser.add_argument( + "solidity_files", + nargs="*", + help="Inputs file name and contract name. \n" + "usage: file1.sol:OptionalContractName file2.sol file3.sol:OptionalContractName", + ) + parser.add_argument( + "--full", + help="Run a full analysis. Default: quick analysis", + action="store_true", + ) def create_read_storage_parser(read_storage_parser: ArgumentParser): @@ -292,7 +354,12 @@ def create_analyzer_parser(analyzer_parser: ArgumentParser): :param analyzer_parser: :return: """ - analyzer_parser.add_argument("solidity_file", nargs="*") + analyzer_parser.add_argument( + "solidity_files", + nargs="*", + help="Inputs file name and contract name. \n" + "usage: file1.sol:OptionalContractName file2.sol file3.sol:OptionalContractName", + ) commands = analyzer_parser.add_argument_group("commands") commands.add_argument("-g", "--graph", help="generate a control flow graph") commands.add_argument( @@ -346,11 +413,17 @@ def create_analyzer_parser(analyzer_parser: ArgumentParser): default=86400, help="The amount of seconds to spend on symbolic execution", ) + options.add_argument( + "--solver-timeout", + type=int, + default=10000, + help="The maximum amount of time(in milli seconds) the solver spends for queries from analysis modules", + ) options.add_argument( "--create-timeout", type=int, default=10, - help="The amount of seconds to spend on " "the initial contract creation", + help="The amount of seconds to spend on the initial contract creation", ) options.add_argument( "-l", @@ -360,8 +433,9 @@ def create_analyzer_parser(analyzer_parser: ArgumentParser): ) options.add_argument( "--no-onchain-storage-access", + "--no-onchain-access", action="store_true", - help="turns off getting the data from onchain contracts", + help="turns off getting the data from onchain contracts (both loading storage and contract code)", ) options.add_argument( @@ -384,6 +458,16 @@ def create_analyzer_parser(analyzer_parser: ArgumentParser): action="store_true", help="Deactivate dependency-based pruning", ) + options.add_argument( + "--enable-coverage-strategy", + action="store_true", + help="enable coverage based search strategy", + ) + options.add_argument( + "--custom-modules-directory", + help="designates a separate directory to search for custom analysis modules", + metavar="CUSTOM_MODULES_DIRECTORY", + ) def validate_args(args: Namespace): @@ -410,6 +494,8 @@ def validate_args(args: Namespace): exit_with_error( args.outform, "Invalid -v value, you can find valid values in usage" ) + if args.command in DISASSEMBLE_LIST and len(args.solidity_files) > 1: + exit_with_error("text", "Only a single arg is supported for using disassemble") if args.command in ANALYZE_LIST: if args.query_signature and sigs.ethereum_input_decoder is None: @@ -494,15 +580,15 @@ def load_code(disassembler: MythrilDisassembler, args: Namespace): elif args.__dict__.get("address", False): # Get bytecode from a contract address address, _ = disassembler.load_from_address(args.address) - elif args.__dict__.get("solidity_file", False): + elif args.__dict__.get("solidity_files", False): # Compile Solidity source file(s) - if args.command in ANALYZE_LIST and args.graph and len(args.solidity_file) > 1: + if args.command in ANALYZE_LIST and args.graph and len(args.solidity_files) > 1: exit_with_error( args.outform, "Cannot generate call graphs from multiple input files. Please do it one at a time.", ) address, _ = disassembler.load_from_solidity( - args.solidity_file + args.solidity_files ) # list of files else: exit_with_error( @@ -534,6 +620,17 @@ def execute_command( ) print(storage) + elif args.command in PRO_LIST: + mode = "full" if args.full else "quick" + report = mythx.analyze(disassembler.contracts, mode) + outputs = { + "json": report.as_json(), + "jsonv2": report.as_swc_standard_format(), + "text": report.as_text(), + "markdown": report.as_markdown(), + } + print(outputs[args.outform]) + elif args.command in DISASSEMBLE_LIST: if disassembler.contracts[0].code: print("Runtime Disassembly: \n" + disassembler.contracts[0].get_easm()) @@ -552,6 +649,12 @@ def execute_command( enable_iprof=args.enable_iprof, disable_dependency_pruning=args.disable_dependency_pruning, onchain_storage_access=not args.no_onchain_storage_access, + solver_timeout=args.solver_timeout, + requires_dynld=not args.no_onchain_storage_access, + enable_coverage_strategy=args.enable_coverage_strategy, + custom_modules_directory=args.custom_modules_directory + if args.custom_modules_directory + else "", ) if not disassembler.contracts: @@ -658,12 +761,12 @@ def parse_args_and_execute(parser: ArgumentParser, args: Namespace) -> None: config = set_config(args) leveldb_search(config, args) query_signature = args.__dict__.get("query_signature", None) - solc_args = args.__dict__.get("solc_args", None) + solc_json = args.__dict__.get("solc_json", None) solv = args.__dict__.get("solv", None) disassembler = MythrilDisassembler( eth=config.eth, solc_version=solv, - solc_args=solc_args, + solc_settings_json=solc_json, enable_online_lookup=query_signature, ) if args.command == "truffle": diff --git a/mythril/interfaces/old_cli.py b/mythril/interfaces/old_cli.py index 0157c2b7..27bde387 100644 --- a/mythril/interfaces/old_cli.py +++ b/mythril/interfaces/old_cli.py @@ -44,9 +44,7 @@ def exit_with_error(format_, message): "sourceType": "", "sourceFormat": "", "sourceList": [], - "meta": { - "logs": [{"level": "error", "hidden": "true", "msg": message}] - }, + "meta": {"logs": [{"level": "error", "hidden": True, "msg": message}]}, } ] print(json.dumps(result)) @@ -213,6 +211,12 @@ def create_parser(parser: argparse.ArgumentParser) -> None: default=2, help="Maximum number of transactions issued by laser", ) + options.add_argument( + "--solver-timeout", + type=int, + default=10000, + help="The maximum amount of time(in milli seconds) the solver spends for queries from analysis modules", + ) options.add_argument( "--execution-timeout", type=int, @@ -225,7 +229,10 @@ def create_parser(parser: argparse.ArgumentParser) -> None: default=10, help="The amount of seconds to spend on " "the initial contract creation", ) - options.add_argument("--solc-args", help="Extra arguments for solc") + options.add_argument( + "--solc-json", + help="Json for the optional 'settings' parameter of solc's standard-json input", + ) options.add_argument( "--phrack", action="store_true", help="Phrack-style call graph" ) @@ -419,6 +426,7 @@ def execute_command( enable_iprof=args.enable_iprof, disable_dependency_pruning=args.disable_dependency_pruning, onchain_storage_access=not args.no_onchain_storage_access, + solver_timeout=args.solver_timeout, ) if args.disassemble: @@ -517,7 +525,7 @@ def parse_args(parser: argparse.ArgumentParser, args: argparse.Namespace) -> Non disassembler = MythrilDisassembler( eth=config.eth, solc_version=args.solv, - solc_args=args.solc_args, + solc_settings_json=args.solc_json, enable_online_lookup=args.query_signature, ) if args.truffle: diff --git a/mythril/laser/ethereum/call.py b/mythril/laser/ethereum/call.py index 918c1d3f..24a8e2f3 100644 --- a/mythril/laser/ethereum/call.py +++ b/mythril/laser/ethereum/call.py @@ -4,19 +4,20 @@ parameters for the new global state.""" import logging import re -from typing import Union, List, cast, Callable +from typing import Union, List, cast, Callable, Optional import mythril.laser.ethereum.util as util from mythril.laser.ethereum import natives from mythril.laser.ethereum.gas import OPCODE_GAS from mythril.laser.ethereum.state.account import Account +from mythril.laser.ethereum.natives import PRECOMPILE_COUNT from mythril.laser.ethereum.state.calldata import ( BaseCalldata, SymbolicCalldata, ConcreteCalldata, ) from mythril.laser.ethereum.state.global_state import GlobalState -from mythril.laser.smt import BitVec +from mythril.laser.smt import BitVec, is_true from mythril.laser.smt import simplify, Expression, symbol_factory from mythril.support.loader import DynLoader @@ -49,7 +50,11 @@ def get_call_parameters( callee_account = None call_data = get_call_data(global_state, memory_input_offset, memory_input_size) - if int(callee_address, 16) >= 5 or int(callee_address, 16) == 0: + if ( + isinstance(callee_address, BitVec) + or int(callee_address, 16) > PRECOMPILE_COUNT + or int(callee_address, 16) == 0 + ): callee_account = get_callee_account( global_state, callee_address, dynamic_loader ) @@ -84,11 +89,11 @@ def get_callee_address( except TypeError: log.debug("Symbolic call encountered") - match = re.search(r"storage_(\d+)", str(simplify(symbolic_to_address))) + match = re.search(r"Storage\[(\d+)\]", str(simplify(symbolic_to_address))) log.debug("CALL to: " + str(simplify(symbolic_to_address))) if match is None or dynamic_loader is None: - raise ValueError() + return symbolic_to_address index = int(match.group(1)) log.debug("Dynamic contract address at storage index {}".format(index)) @@ -100,8 +105,7 @@ def get_callee_address( ) # TODO: verify whether this happens or not except: - log.debug("Error accessing contract storage.") - raise ValueError + return symbolic_to_address # testrpc simply returns the address, geth response is more elaborate. if not re.match(r"^0x[0-9a-f]{40}$", callee_address): @@ -111,7 +115,9 @@ def get_callee_address( def get_callee_account( - global_state: GlobalState, callee_address: str, dynamic_loader: DynLoader + global_state: GlobalState, + callee_address: Union[str, BitVec], + dynamic_loader: DynLoader, ): """Gets the callees account from the global_state. @@ -120,28 +126,31 @@ def get_callee_account( :param dynamic_loader: dynamic loader to use :return: Account belonging to callee """ - environment = global_state.environment - accounts = global_state.accounts + if isinstance(callee_address, BitVec): + if callee_address.symbolic: + return Account(callee_address, balances=global_state.world_state.balances) + else: + callee_address = hex(callee_address.value)[2:] try: return global_state.accounts[int(callee_address, 16)] except KeyError: # We have a valid call address, but contract is not in the modules list - log.debug("Module with address " + callee_address + " not loaded.") + log.debug("Module with address %s not loaded.", callee_address) if dynamic_loader is None: - raise ValueError() + raise ValueError("dynamic_loader is None") log.debug("Attempting to load dependency") try: code = dynamic_loader.dynld(callee_address) except ValueError as error: - log.debug("Unable to execute dynamic loader because: {}".format(str(error))) + log.debug("Unable to execute dynamic loader because: %s", error) raise error if code is None: log.debug("No code returned, not a contract account?") - raise ValueError() + raise ValueError("No code returned") log.debug("Dependency loaded: " + callee_address) callee_account = Account( @@ -151,7 +160,7 @@ def get_callee_account( dynamic_loader=dynamic_loader, balances=global_state.world_state.balances, ) - accounts[callee_address] = callee_account + global_state.accounts[int(callee_address, 16)] = callee_account return callee_account @@ -189,10 +198,10 @@ def get_call_data( ) uses_entire_calldata = simplify( - memory_size - global_state.environment.calldata.calldatasize == 0 + memory_size == global_state.environment.calldata.calldatasize ) - if uses_entire_calldata is True: + if is_true(uses_entire_calldata): return global_state.environment.calldata try: @@ -203,18 +212,24 @@ def get_call_data( ] return ConcreteCalldata(transaction_id, calldata_from_mem) except TypeError: - log.debug("Unsupported symbolic calldata offset") + log.debug( + "Unsupported symbolic calldata offset %s size %s", memory_start, memory_size + ) return SymbolicCalldata(transaction_id) def native_call( global_state: GlobalState, - callee_address: str, + callee_address: Union[str, BitVec], call_data: BaseCalldata, memory_out_offset: Union[int, Expression], memory_out_size: Union[int, Expression], -) -> Union[List[GlobalState], None]: - if not 0 < int(callee_address, 16) < 5: +) -> Optional[List[GlobalState]]: + + if ( + isinstance(callee_address, BitVec) + or not 0 < int(callee_address, 16) <= PRECOMPILE_COUNT + ): return None log.debug("Native contract called: " + callee_address) diff --git a/mythril/laser/ethereum/evm_exceptions.py b/mythril/laser/ethereum/evm_exceptions.py index 63460e2b..647c52e4 100644 --- a/mythril/laser/ethereum/evm_exceptions.py +++ b/mythril/laser/ethereum/evm_exceptions.py @@ -35,3 +35,9 @@ class OutOfGasException(VmException): """A VM exception denoting the current execution has run out of gas.""" pass + + +class WriteProtection(VmException): + """A VM exception denoting that a write operation is executed on a write protected environment""" + + pass diff --git a/mythril/laser/ethereum/gas.py b/mythril/laser/ethereum/gas.py index 7e283d15..0a0c0a38 100644 --- a/mythril/laser/ethereum/gas.py +++ b/mythril/laser/ethereum/gas.py @@ -180,10 +180,7 @@ OPCODE_GAS = { "LOG3": (4 * 375, 4 * 375 + 8 * 32), "LOG4": (5 * 375, 5 * 375 + 8 * 32), "CREATE": (32000, 32000), - "CREATE2": ( - 32000, - 32000, - ), # TODO: The gas value is dynamic, to be done while implementing create2 + "CREATE2": (32000, 32000), # TODO: Make the gas values dynamic "CALL": (700, 700 + 9000 + 25000), "NATIVE_COST": calculate_native_gas, "CALLCODE": (700, 700 + 9000 + 25000), diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index b3e3eaa6..2f1c7f03 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -6,7 +6,6 @@ import logging from copy import copy, deepcopy from typing import cast, Callable, List, Set, Union, Tuple, Any from datetime import datetime -from math import ceil from ethereum import utils from mythril.laser.smt import ( @@ -25,18 +24,24 @@ from mythril.laser.smt import ( Bool, Not, LShR, + UGE, ) from mythril.laser.smt import symbol_factory +from mythril.disassembler.disassembly import Disassembly + +from mythril.laser.ethereum.state.calldata import ConcreteCalldata, SymbolicCalldata + import mythril.laser.ethereum.util as helper from mythril.laser.ethereum import util -from mythril.laser.ethereum.call import get_call_parameters, native_call +from mythril.laser.ethereum.call import get_call_parameters, native_call, get_call_data from mythril.laser.ethereum.evm_exceptions import ( VmException, StackUnderflowException, InvalidJumpDestination, InvalidInstruction, OutOfGasException, + WriteProtection, ) from mythril.laser.ethereum.gas import OPCODE_GAS from mythril.laser.ethereum.state.global_state import GlobalState @@ -44,8 +49,11 @@ from mythril.laser.ethereum.transaction import ( MessageCallTransaction, TransactionStartSignal, ContractCreationTransaction, + get_next_transaction_id, ) +from mythril.support.support_utils import get_code_hash + from mythril.support.loader import DynLoader log = logging.getLogger(__name__) @@ -54,6 +62,30 @@ TT256 = 2 ** 256 TT256M1 = 2 ** 256 - 1 +def transfer_ether( + global_state: GlobalState, + sender: BitVec, + receiver: BitVec, + value: Union[int, BitVec], +): + """ + Perform an Ether transfer between two accounts + + :param global_state: The global state in which the Ether transfer occurs + :param sender: The sender of the Ether + :param receiver: The recipient of the Ether + :param value: The amount of Ether to send + :return: + """ + value = value if isinstance(value, BitVec) else symbol_factory.BitVecVal(value, 256) + + global_state.mstate.constraints.append( + UGE(global_state.world_state.balances[sender], value) + ) + global_state.world_state.balances[receiver] += value + global_state.world_state.balances[sender] -= value + + class StateTransition(object): """Decorator that handles global state copy and original return. @@ -63,14 +95,18 @@ class StateTransition(object): if `increment_pc=True`. """ - def __init__(self, increment_pc=True, enable_gas=True): + def __init__( + self, increment_pc=True, enable_gas=True, is_state_mutation_instruction=False + ): """ :param increment_pc: :param enable_gas: + :param is_state_mutation_instruction: The function mutates state """ self.increment_pc = increment_pc self.enable_gas = enable_gas + self.is_state_mutation_instruction = is_state_mutation_instruction @staticmethod def call_on_state_copy(func: Callable, func_obj: "Instruction", state: GlobalState): @@ -140,6 +176,13 @@ class StateTransition(object): :param global_state: :return: """ + if self.is_state_mutation_instruction and global_state.environment.static: + raise WriteProtection( + "The function {} cannot be executed in a static call".format( + func.__name__[:-1] + ) + ) + new_global_states = self.call_on_state_copy(func, func_obj, global_state) new_global_states = [ self.accumulate_gas(state) for state in new_global_states @@ -172,7 +215,8 @@ class Instruction: :return: """ # Generalize some ops - log.debug("Evaluating {}".format(self.op_code)) + log.debug("Evaluating %s at %i", self.op_code, global_state.mstate.pc) + op = self.op_code.lower() if self.op_code.startswith("PUSH"): op = "push" @@ -732,51 +776,45 @@ class Instruction: """ state = global_state.mstate environment = global_state.environment - state.stack.append(environment.calldata.calldatasize) - return [global_state] - @StateTransition() - def calldatacopy_(self, global_state: GlobalState) -> List[GlobalState]: - """ + if isinstance(global_state.current_transaction, ContractCreationTransaction): + log.debug("Attempt to use CALLDATASIZE in creation transaction") + state.stack.append(0) + else: + state.stack.append(environment.calldata.calldatasize) - :param global_state: - :return: - """ - state = global_state.mstate + return [global_state] + + @staticmethod + def _calldata_copy_helper(global_state, mstate, mstart, dstart, size): environment = global_state.environment - op0, op1, op2 = state.stack.pop(), state.stack.pop(), state.stack.pop() try: - mstart = util.get_concrete_int(op0) + mstart = util.get_concrete_int(mstart) except TypeError: log.debug("Unsupported symbolic memory offset in CALLDATACOPY") return [global_state] try: - dstart = util.get_concrete_int(op1) # type: Union[int, BitVec] + dstart = util.get_concrete_int(dstart) # type: Union[int, BitVec] except TypeError: log.debug("Unsupported symbolic calldata offset in CALLDATACOPY") - dstart = simplify(op1) + dstart = simplify(dstart) - size_sym = False try: - size = util.get_concrete_int(op2) # type: Union[int, BitVec] + size = util.get_concrete_int(size) # type: Union[int, BitVec] except TypeError: log.debug("Unsupported symbolic size in CALLDATACOPY") - size = simplify(op2) - size_sym = True - - if size_sym: size = 320 # The excess size will get overwritten size = cast(int, size) if size > 0: try: - state.mem_extend(mstart, size) + mstate.mem_extend(mstart, size) except TypeError as e: log.debug("Memory allocation error: {}".format(e)) - state.mem_extend(mstart, 1) - state.memory[mstart] = global_state.new_bitvec( + mstate.mem_extend(mstart, 1) + mstate.memory[mstart] = global_state.new_bitvec( "calldata_" + str(environment.active_account.contract_name) + "[" @@ -801,12 +839,12 @@ class Instruction: else simplify(cast(BitVec, i_data) + 1) ) for i in range(len(new_memory)): - state.memory[i + mstart] = new_memory[i] + mstate.memory[i + mstart] = new_memory[i] except IndexError: log.debug("Exception copying calldata to memory") - state.memory[mstart] = global_state.new_bitvec( + mstate.memory[mstart] = global_state.new_bitvec( "calldata_" + str(environment.active_account.contract_name) + "[" @@ -818,6 +856,22 @@ class Instruction: ) return [global_state] + @StateTransition() + def calldatacopy_(self, global_state: GlobalState) -> List[GlobalState]: + """ + + :param global_state: + :return: + """ + state = global_state.mstate + op0, op1, op2 = state.stack.pop(), state.stack.pop(), state.stack.pop() + + if isinstance(global_state.current_transaction, ContractCreationTransaction): + log.debug("Attempt to use CALLDATACOPY in creation transaction") + return [global_state] + + return self._calldata_copy_helper(global_state, state, op0, op1, op2) + # Environment @StateTransition() def address_(self, global_state: GlobalState) -> List[GlobalState]: @@ -840,7 +894,11 @@ class Instruction: """ state = global_state.mstate address = state.stack.pop() - state.stack.append(global_state.new_bitvec("balance_at_" + str(address), 256)) + + balance = global_state.world_state.balances[ + global_state.environment.active_account.address + ] + state.stack.append(balance) return [global_state] @StateTransition() @@ -877,9 +935,31 @@ class Instruction: state = global_state.mstate environment = global_state.environment disassembly = environment.code - state.stack.append(len(disassembly.bytecode) // 2) + calldata = global_state.environment.calldata + if isinstance(global_state.current_transaction, ContractCreationTransaction): + # Hacky way to ensure constructor arguments work - Pick some reasonably large size. + no_of_bytes = len(disassembly.bytecode) // 2 + if isinstance(calldata, ConcreteCalldata): + no_of_bytes += calldata.size + else: + no_of_bytes += 0x200 # space for 16 32-byte arguments + global_state.mstate.constraints.append( + global_state.environment.calldata.size == no_of_bytes + ) + + else: + no_of_bytes = len(disassembly.bytecode) // 2 + state.stack.append(no_of_bytes) return [global_state] + @staticmethod + def _sha3_gas_helper(global_state, length): + min_gas, max_gas = cast(Callable, OPCODE_GAS["SHA3_FUNC"])(length) + global_state.mstate.min_gas_used += min_gas + global_state.mstate.max_gas_used += max_gas + StateTransition.check_gas_usage_limit(global_state) + return global_state + @StateTransition(enable_gas=False) def sha3_(self, global_state: GlobalState) -> List[GlobalState]: """ @@ -905,10 +985,7 @@ class Instruction: state.max_gas_used += gas_tuple[1] return [global_state] - min_gas, max_gas = cast(Callable, OPCODE_GAS["SHA3_FUNC"])(length) - state.min_gas_used += min_gas - state.max_gas_used += max_gas - StateTransition.check_gas_usage_limit(global_state) + Instruction._sha3_gas_helper(global_state, length) state.mem_extend(index, length) data_list = [ @@ -961,34 +1038,6 @@ class Instruction: global_state.mstate.stack.append(global_state.environment.gasprice) return [global_state] - @staticmethod - def _handle_symbolic_args( - global_state: GlobalState, concrete_memory_offset: int - ) -> None: - """ - In contract creation transaction with dynamic arguments(like arrays, maps) solidity will try to - execute CODECOPY with code size as len(with_args) - len(without_args) which in our case - would be 0, hence we are writing 10 symbol words onto the memory on the assumption that - no one would use 10 array/map arguments for constructor. - :param global_state: The global state - :param concrete_memory_offset: The memory offset on which symbols should be written - """ - no_of_words = ceil( - min(len(global_state.environment.code.bytecode) / 2, 320) / 32 - ) - global_state.mstate.mem_extend(concrete_memory_offset, 32 * no_of_words) - for i in range(no_of_words): - global_state.mstate.memory.write_word_at( - concrete_memory_offset + i * 32, - global_state.new_bitvec( - "code_{}({})".format( - concrete_memory_offset + i * 32, - global_state.environment.active_account.contract_name, - ), - 256, - ), - ) - @StateTransition() def codecopy_(self, global_state: GlobalState) -> List[GlobalState]: """ @@ -1001,6 +1050,63 @@ class Instruction: global_state.mstate.stack.pop(), global_state.mstate.stack.pop(), ) + code = global_state.environment.code.bytecode + if code[0:2] == "0x": + code = code[2:] + code_size = len(code) // 2 + + if isinstance(global_state.current_transaction, ContractCreationTransaction): + # Treat creation code after the expected disassembly as calldata. + # This is a slightly hacky way to ensure that symbolic constructor + # arguments work correctly. + mstate = global_state.mstate + offset = code_offset - code_size + log.debug("Copying from code offset: {} with size: {}".format(offset, size)) + + if isinstance(global_state.environment.calldata, SymbolicCalldata): + if code_offset >= code_size: + return self._calldata_copy_helper( + global_state, mstate, memory_offset, offset, size + ) + else: + # Copy from both code and calldata appropriately. + concrete_code_offset = helper.get_concrete_int(code_offset) + concrete_size = helper.get_concrete_int(size) + + code_copy_offset = concrete_code_offset + code_copy_size = ( + concrete_size + if concrete_code_offset + concrete_size <= code_size + else code_size - concrete_code_offset + ) + code_copy_size = code_copy_size if code_copy_size >= 0 else 0 + + calldata_copy_offset = ( + concrete_code_offset - code_size + if concrete_code_offset - code_size > 0 + else 0 + ) + calldata_copy_size = concrete_code_offset + concrete_size - code_size + calldata_copy_size = ( + calldata_copy_size if calldata_copy_size >= 0 else 0 + ) + + [global_state] = self._code_copy_helper( + code=global_state.environment.code.bytecode, + memory_offset=memory_offset, + code_offset=code_copy_offset, + size=code_copy_size, + op="CODECOPY", + global_state=global_state, + ) + return self._calldata_copy_helper( + global_state=global_state, + mstate=mstate, + mstart=memory_offset + code_copy_size, + dstart=calldata_copy_offset, + size=calldata_copy_size, + ) + return self._code_copy_helper( code=global_state.environment.code.bytecode, memory_offset=memory_offset, @@ -1041,9 +1147,9 @@ class Instruction: @staticmethod def _code_copy_helper( code: str, - memory_offset: BitVec, - code_offset: BitVec, - size: BitVec, + memory_offset: Union[int, BitVec], + code_offset: Union[int, BitVec], + size: Union[int, BitVec], op: str, global_state: GlobalState, ) -> List[GlobalState]: @@ -1089,13 +1195,6 @@ class Instruction: if code[0:2] == "0x": code = code[2:] - if concrete_size == 0 and isinstance( - global_state.current_transaction, ContractCreationTransaction - ): - if concrete_code_offset >= len(code) // 2: - Instruction._handle_symbolic_args(global_state, concrete_memory_offset) - return [global_state] - for i in range(concrete_size): if 2 * (concrete_code_offset + i + 1) <= len(code): global_state.mstate.memory[concrete_memory_offset + i] = int( @@ -1155,18 +1254,26 @@ class Instruction: global_state=global_state, ) - @StateTransition + @StateTransition() def extcodehash_(self, global_state: GlobalState) -> List[GlobalState]: """ :param global_state: :return: List of global states possible, list of size 1 in this case """ - # TODO: To be implemented - address = global_state.mstate.stack.pop() - global_state.mstate.stack.append( - global_state.new_bitvec("extcodehash_{}".format(str(address)), 256) - ) + world_state = global_state.world_state + stack = global_state.mstate.stack + address = Extract(159, 0, stack.pop()) + + if address.symbolic: + code_hash = symbol_factory.BitVecVal(int(get_code_hash(""), 16), 256) + elif address.value not in world_state.accounts: + code_hash = symbol_factory.BitVecVal(0, 256) + else: + addr = "0" * (40 - len(hex(address.value)[2:])) + hex(address.value)[2:] + code = world_state.accounts_exist_or_load(addr, self.dynamic_loader) + code_hash = symbol_factory.BitVecVal(int(get_code_hash(code), 16), 256) + stack.append(code_hash) return [global_state] @StateTransition() @@ -1368,11 +1475,10 @@ class Instruction: state = global_state.mstate index = state.stack.pop() - state.stack.append(global_state.environment.active_account.storage[index]) return [global_state] - @StateTransition() + @StateTransition(is_state_mutation_instruction=True) def sstore_(self, global_state: GlobalState) -> List[GlobalState]: """ @@ -1381,7 +1487,6 @@ class Instruction: """ state = global_state.mstate index, value = state.stack.pop(), state.stack.pop() - global_state.environment.active_account.storage[index] = value return [global_state] @@ -1540,7 +1645,7 @@ class Instruction: global_state.mstate.stack.append(global_state.new_bitvec("gas", 256)) return [global_state] - @StateTransition() + @StateTransition(is_state_mutation_instruction=True) def log_(self, global_state: GlobalState) -> List[GlobalState]: """ @@ -1555,37 +1660,112 @@ class Instruction: # Not supported return [global_state] - @StateTransition() + def _create_transaction_helper( + self, global_state, call_value, mem_offset, mem_size, create2_salt=None + ): + mstate = global_state.mstate + environment = global_state.environment + world_state = global_state.world_state + + call_data = get_call_data(global_state, mem_offset, mem_offset + mem_size) + + code_raw = [] + code_end = call_data.size + for i in range(call_data.size): + if call_data[i].symbolic: + code_end = i + break + code_raw.append(call_data[i].value) + + code_str = bytes.hex(bytes(code_raw)) + + next_transaction_id = get_next_transaction_id() + constructor_arguments = ConcreteCalldata( + next_transaction_id, call_data[code_end:] + ) + code = Disassembly(code_str) + + caller = environment.active_account.address + gas_price = environment.gasprice + origin = environment.origin + + contract_address = None + if create2_salt: + salt = hex(create2_salt)[2:] + salt = "0" * (64 - len(salt)) + salt + + addr = hex(caller.value)[2:] + addr = "0" * (40 - len(addr)) + addr + + Instruction._sha3_gas_helper(global_state, len(code_str[2:] // 2)) + + contract_address = int( + get_code_hash("0xff" + addr + salt + get_code_hash(code_str)[2:])[26:], + 16, + ) + transaction = ContractCreationTransaction( + world_state=world_state, + caller=caller, + code=code, + call_data=constructor_arguments, + gas_price=gas_price, + gas_limit=mstate.gas_limit, + origin=origin, + call_value=call_value, + contract_address=contract_address, + ) + raise TransactionStartSignal(transaction, self.op_code, global_state) + + @StateTransition(is_state_mutation_instruction=True) def create_(self, global_state: GlobalState) -> List[GlobalState]: """ :param global_state: :return: """ - # TODO: implement me - state = global_state.mstate - state.stack.pop(), state.stack.pop(), state.stack.pop() - # Not supported - state.stack.append(0) - return [global_state] + call_value, mem_offset, mem_size = global_state.mstate.pop(3) + + return self._create_transaction_helper( + global_state, call_value, mem_offset, mem_size + ) @StateTransition() + def create_post(self, global_state: GlobalState) -> List[GlobalState]: + call_value, mem_offset, mem_size = global_state.mstate.pop(3) + call_data = get_call_data(global_state, mem_offset, mem_offset + mem_size) + if global_state.last_return_data: + return_val = symbol_factory.BitVecVal( + int(global_state.last_return_data, 16), 256 + ) + else: + return_val = symbol_factory.BitVecVal(0, 256) + global_state.mstate.stack.append(return_val) + return [global_state] + + @StateTransition(is_state_mutation_instruction=True) def create2_(self, global_state: GlobalState) -> List[GlobalState]: """ :param global_state: :return: """ - # TODO: implement me - state = global_state.mstate - endowment, memory_start, memory_length, salt = ( - state.stack.pop(), - state.stack.pop(), - state.stack.pop(), - state.stack.pop(), + call_value, mem_offset, mem_size, salt = global_state.mstate.pop(4) + + return self._create_transaction_helper( + global_state, call_value, mem_offset, mem_size, salt ) - # Not supported - state.stack.append(0) + + @StateTransition() + def create2_post(self, global_state: GlobalState) -> List[GlobalState]: + call_value, mem_offset, mem_size, salt = global_state.mstate.pop(4) + call_data = get_call_data(global_state, mem_offset, mem_offset + mem_size) + if global_state.last_return_data: + return_val = symbol_factory.BitVecVal( + int(global_state.last_return_data), 256 + ) + else: + return_val = symbol_factory.BitVecVal(0, 256) + global_state.mstate.stack.append(return_val) return [global_state] @StateTransition() @@ -1605,7 +1785,7 @@ class Instruction: return_data = state.memory[offset : offset + length] global_state.current_transaction.end(global_state, return_data) - @StateTransition() + @StateTransition(is_state_mutation_instruction=True) def suicide_(self, global_state: GlobalState): """ @@ -1615,7 +1795,7 @@ class Instruction: transfer_amount = global_state.environment.active_account.balance() # Often the target of the suicide instruction will be symbolic # If it isn't then we'll transfer the balance to the indicated contract - global_state.world_state[target].add_balance(transfer_amount) + global_state.world_state.balances[target] += transfer_amount global_state.environment.active_account = deepcopy( global_state.environment.active_account @@ -1689,6 +1869,10 @@ class Instruction: if callee_account is not None and callee_account.code.bytecode == "": log.debug("The call is related to ether transfer between accounts") + sender = environment.active_account.address + receiver = callee_account.address + transfer_ether(global_state, sender, receiver, value) + global_state.mstate.stack.append( global_state.new_bitvec("retval_" + str(instr["address"]), 256) ) @@ -1706,6 +1890,21 @@ class Instruction: ) return [global_state] + if environment.static: + if isinstance(value, int) and value > 0: + raise WriteProtection( + "Cannot call with non zero value in a static call" + ) + if isinstance(value, BitVec): + if value.symbolic: + global_state.mstate.constraints.append( + value == symbol_factory.BitVecVal(0, 256) + ) + elif value.value > 0: + raise WriteProtection( + "Cannot call with non zero value in a static call" + ) + native_result = native_call( global_state, callee_address, call_data, memory_out_offset, memory_out_size ) @@ -1720,20 +1919,81 @@ class Instruction: callee_account=callee_account, call_data=call_data, call_value=value, + static=environment.static, ) - raise TransactionStartSignal(transaction, self.op_code) + raise TransactionStartSignal(transaction, self.op_code, global_state) @StateTransition() def call_post(self, global_state: GlobalState) -> List[GlobalState]: """ + :param global_state: + :return: + """ + + return self.post_handler(global_state, function_name="call") + + @StateTransition() + def callcode_(self, global_state: GlobalState) -> List[GlobalState]: + """ + + :param global_state: + :return: + """ + instr = global_state.get_current_instruction() + environment = global_state.environment + + try: + callee_address, callee_account, call_data, value, gas, _, _ = get_call_parameters( + global_state, self.dynamic_loader, True + ) + if callee_account is not None and callee_account.code.bytecode == "": + log.debug("The call is related to ether transfer between accounts") + sender = global_state.environment.active_account.address + receiver = callee_account.address + transfer_ether(global_state, sender, receiver, value) + + global_state.mstate.stack.append( + global_state.new_bitvec("retval_" + str(instr["address"]), 256) + ) + return [global_state] + + except ValueError as e: + log.debug( + "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format( + e + ) + ) + global_state.mstate.stack.append( + global_state.new_bitvec("retval_" + str(instr["address"]), 256) + ) + return [global_state] + + transaction = MessageCallTransaction( + world_state=global_state.world_state, + gas_price=environment.gasprice, + gas_limit=gas, + origin=environment.origin, + code=callee_account.code, + caller=environment.address, + callee_account=environment.active_account, + call_data=call_data, + call_value=value, + static=environment.static, + ) + raise TransactionStartSignal(transaction, self.op_code, global_state) + + @StateTransition() + def callcode_post(self, global_state: GlobalState) -> List[GlobalState]: + """ + :param global_state: :return: """ instr = global_state.get_current_instruction() try: - callee_address, callee_account, call_data, value, gas, memory_out_offset, memory_out_size = get_call_parameters( + callee_address, _, _, value, _, memory_out_offset, memory_out_size = get_call_parameters( global_state, self.dynamic_loader, True ) except ValueError as e: @@ -1754,7 +2014,6 @@ class Instruction: ) global_state.mstate.stack.append(return_value) global_state.mstate.constraints.append(return_value == 0) - return [global_state] try: @@ -1787,11 +2046,10 @@ class Instruction: return_value = global_state.new_bitvec("retval_" + str(instr["address"]), 256) global_state.mstate.stack.append(return_value) global_state.mstate.constraints.append(return_value == 1) - return [global_state] @StateTransition() - def callcode_(self, global_state: GlobalState) -> List[GlobalState]: + def delegatecall_(self, global_state: GlobalState) -> List[GlobalState]: """ :param global_state: @@ -1802,8 +2060,20 @@ class Instruction: try: callee_address, callee_account, call_data, value, gas, _, _ = get_call_parameters( - global_state, self.dynamic_loader, True + global_state, self.dynamic_loader ) + + if callee_account is not None and callee_account.code.bytecode == "": + log.debug("The call is related to ether transfer between accounts") + sender = global_state.environment.active_account.address + receiver = callee_account.address + transfer_ether(global_state, sender, receiver, value) + + global_state.mstate.stack.append( + global_state.new_bitvec("retval_" + str(instr["address"]), 256) + ) + return [global_state] + except ValueError as e: log.debug( "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format( @@ -1821,15 +2091,16 @@ class Instruction: gas_limit=gas, origin=environment.origin, code=callee_account.code, - caller=environment.address, + caller=environment.sender, callee_account=environment.active_account, call_data=call_data, - call_value=value, + call_value=environment.callvalue, + static=environment.static, ) - raise TransactionStartSignal(transaction, self.op_code) + raise TransactionStartSignal(transaction, self.op_code, global_state) @StateTransition() - def callcode_post(self, global_state: GlobalState) -> List[GlobalState]: + def delegatecall_post(self, global_state: GlobalState) -> List[GlobalState]: """ :param global_state: @@ -1839,7 +2110,7 @@ class Instruction: try: callee_address, _, _, value, _, memory_out_offset, memory_out_size = get_call_parameters( - global_state, self.dynamic_loader, True + global_state, self.dynamic_loader ) except ValueError as e: log.debug( @@ -1878,7 +2149,7 @@ class Instruction: ) return [global_state] - # Copy memory + # Copy memory global_state.mstate.mem_extend( memory_out_offset, min(memory_out_size, len(global_state.last_return_data)) ) @@ -1894,7 +2165,7 @@ class Instruction: return [global_state] @StateTransition() - def delegatecall_(self, global_state: GlobalState) -> List[GlobalState]: + def staticcall_(self, global_state: GlobalState) -> List[GlobalState]: """ :param global_state: @@ -1902,11 +2173,22 @@ class Instruction: """ instr = global_state.get_current_instruction() environment = global_state.environment - try: - callee_address, callee_account, call_data, value, gas, _, _ = get_call_parameters( + callee_address, callee_account, call_data, value, gas, memory_out_offset, memory_out_size = get_call_parameters( global_state, self.dynamic_loader ) + + if callee_account is not None and callee_account.code.bytecode == "": + log.debug("The call is related to ether transfer between accounts") + sender = environment.active_account.address + receiver = callee_account.address + transfer_ether(global_state, sender, receiver, value) + + global_state.mstate.stack.append( + global_state.new_bitvec("retval_" + str(instr["address"]), 256) + ) + return [global_state] + except ValueError as e: log.debug( "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format( @@ -1918,36 +2200,43 @@ class Instruction: ) return [global_state] + native_result = native_call( + global_state, callee_address, call_data, memory_out_offset, memory_out_size + ) + + if native_result: + return native_result + transaction = MessageCallTransaction( world_state=global_state.world_state, gas_price=environment.gasprice, gas_limit=gas, origin=environment.origin, code=callee_account.code, - caller=environment.sender, - callee_account=environment.active_account, + caller=environment.address, + callee_account=callee_account, call_data=call_data, - call_value=environment.callvalue, + call_value=value, + static=True, ) - raise TransactionStartSignal(transaction, self.op_code) + raise TransactionStartSignal(transaction, self.op_code, global_state) @StateTransition() - def delegatecall_post(self, global_state: GlobalState) -> List[GlobalState]: - """ + def staticcall_post(self, global_state: GlobalState) -> List[GlobalState]: + return self.post_handler(global_state, function_name="staticcall") - :param global_state: - :return: - """ + def post_handler(self, global_state, function_name: str): instr = global_state.get_current_instruction() try: - callee_address, _, _, value, _, memory_out_offset, memory_out_size = get_call_parameters( - global_state, self.dynamic_loader + with_value = function_name is not "staticcall" + callee_address, callee_account, call_data, value, gas, memory_out_offset, memory_out_size = get_call_parameters( + global_state, self.dynamic_loader, with_value ) except ValueError as e: log.debug( - "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format( - e + "Could not determine required parameters for {}, putting fresh symbol on the stack. \n{}".format( + function_name, e ) ) global_state.mstate.stack.append( @@ -1980,7 +2269,7 @@ class Instruction: ) return [global_state] - # Copy memory + # Copy memory global_state.mstate.mem_extend( memory_out_offset, min(memory_out_size, len(global_state.last_return_data)) ) @@ -1993,39 +2282,5 @@ class Instruction: return_value = global_state.new_bitvec("retval_" + str(instr["address"]), 256) global_state.mstate.stack.append(return_value) global_state.mstate.constraints.append(return_value == 1) - return [global_state] - @StateTransition() - def staticcall_(self, global_state: GlobalState) -> List[GlobalState]: - """ - - :param global_state: - :return: - """ - # TODO: implement me - instr = global_state.get_current_instruction() - try: - callee_address, callee_account, call_data, value, gas, memory_out_offset, memory_out_size = get_call_parameters( - global_state, self.dynamic_loader - ) - except ValueError as e: - log.debug( - "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format( - e - ) - ) - global_state.mstate.stack.append( - global_state.new_bitvec("retval_" + str(instr["address"]), 256) - ) - return [global_state] - - native_result = native_call( - global_state, callee_address, call_data, memory_out_offset, memory_out_size - ) - if native_result: - return native_result - - global_state.mstate.stack.append( - global_state.new_bitvec("retval_" + str(instr["address"]), 256) - ) return [global_state] diff --git a/mythril/laser/ethereum/natives.py b/mythril/laser/ethereum/natives.py index ef38d8c9..991a172c 100644 --- a/mythril/laser/ethereum/natives.py +++ b/mythril/laser/ethereum/natives.py @@ -6,12 +6,20 @@ from typing import List, Union from ethereum.utils import ecrecover_to_pub from py_ecc.secp256k1 import N as secp256k1n +import py_ecc.optimized_bn128 as bn128 from rlp.utils import ALL_BYTES from mythril.laser.ethereum.state.calldata import BaseCalldata, ConcreteCalldata -from mythril.laser.ethereum.util import bytearray_to_int -from ethereum.utils import sha3 -from mythril.laser.smt import Concat, simplify +from mythril.laser.ethereum.util import extract_copy, extract32 +from ethereum.utils import ( + sha3, + big_endian_to_int, + safe_ord, + zpad, + int_to_big_endian, + encode_int32, +) +from ethereum.specials import validate_point log = logging.getLogger(__name__) @@ -22,35 +30,6 @@ class NativeContractException(Exception): pass -def int_to_32bytes( - i: int -) -> bytes: # used because int can't fit as bytes function's input - """ - - :param i: - :return: - """ - o = [0] * 32 - for x in range(32): - o[31 - x] = i & 0xFF - i >>= 8 - return bytes(o) - - -def extract32(data: bytearray, i: int) -> int: - """ - - :param data: - :param i: - :return: - """ - if i >= len(data): - return 0 - o = data[i : min(i + 32, len(data))] - o.extend(bytearray(32 - len(o))) - return bytearray_to_int(o) - - def ecrecover(data: List[int]) -> List[int]: """ @@ -59,14 +38,14 @@ def ecrecover(data: List[int]) -> List[int]: """ # TODO: Add type hints try: - byte_data = bytearray(data) - v = extract32(byte_data, 32) - r = extract32(byte_data, 64) - s = extract32(byte_data, 96) + bytes_data = bytearray(data) + v = extract32(bytes_data, 32) + r = extract32(bytes_data, 64) + s = extract32(bytes_data, 96) except TypeError: raise NativeContractException - message = b"".join([ALL_BYTES[x] for x in byte_data[0:32]]) + message = b"".join([ALL_BYTES[x] for x in bytes_data[0:32]]) if r >= secp256k1n or s >= secp256k1n or v < 27 or v > 28: return [] try: @@ -85,10 +64,10 @@ def sha256(data: List[int]) -> List[int]: :return: """ try: - byte_data = bytes(data) + bytes_data = bytes(data) except TypeError: raise NativeContractException - return list(bytearray(hashlib.sha256(byte_data).digest())) + return list(bytearray(hashlib.sha256(bytes_data).digest())) def ripemd160(data: List[int]) -> List[int]: @@ -120,6 +99,114 @@ def identity(data: List[int]) -> List[int]: return data +def mod_exp(data: List[int]) -> List[int]: + """ + TODO: Some symbolic parts can be handled here + Modular Exponentiation + :param data: Data with + :return: modular exponentiation + """ + bytes_data = bytearray(data) + baselen = extract32(bytes_data, 0) + explen = extract32(bytes_data, 32) + modlen = extract32(bytes_data, 64) + if baselen == 0: + return [0] * modlen + if modlen == 0: + return [] + + first_exp_bytes = extract32(bytes_data, 96 + baselen) >> (8 * max(32 - explen, 0)) + bitlength = -1 + while first_exp_bytes: + bitlength += 1 + first_exp_bytes >>= 1 + + base = bytearray(baselen) + extract_copy(bytes_data, base, 0, 96, baselen) + exp = bytearray(explen) + extract_copy(bytes_data, exp, 0, 96 + baselen, explen) + mod = bytearray(modlen) + extract_copy(bytes_data, mod, 0, 96 + baselen + explen, modlen) + if big_endian_to_int(mod) == 0: + return [0] * modlen + o = pow(big_endian_to_int(base), big_endian_to_int(exp), big_endian_to_int(mod)) + return [safe_ord(x) for x in zpad(int_to_big_endian(o), modlen)] + + +def ec_add(data: List[int]) -> List[int]: + bytes_data = bytearray(data) + x1 = extract32(bytes_data, 0) + y1 = extract32(bytes_data, 32) + x2 = extract32(bytes_data, 64) + y2 = extract32(bytes_data, 96) + p1 = validate_point(x1, y1) + p2 = validate_point(x2, y2) + if p1 is False or p2 is False: + return [] + o = bn128.normalize(bn128.add(p1, p2)) + return [safe_ord(x) for x in (encode_int32(o[0].n) + encode_int32(o[1].n))] + + +def ec_mul(data: List[int]) -> List[int]: + bytes_data = bytearray(data) + x = extract32(bytes_data, 0) + y = extract32(bytes_data, 32) + m = extract32(bytes_data, 64) + p = validate_point(x, y) + if p is False: + return [] + o = bn128.normalize(bn128.multiply(p, m)) + return [safe_ord(c) for c in (encode_int32(o[0].n) + encode_int32(o[1].n))] + + +def ec_pair(data: List[int]) -> List[int]: + if len(data) % 192: + return [] + + zero = (bn128.FQ2.one(), bn128.FQ2.one(), bn128.FQ2.zero()) + exponent = bn128.FQ12.one() + bytes_data = bytearray(data) + for i in range(0, len(bytes_data), 192): + x1 = extract32(bytes_data, i) + y1 = extract32(bytes_data, i + 32) + x2_i = extract32(bytes_data, i + 64) + x2_r = extract32(bytes_data, i + 96) + y2_i = extract32(bytes_data, i + 128) + y2_r = extract32(bytes_data, i + 160) + p1 = validate_point(x1, y1) + if p1 is False: + return [] + for v in (x2_i, x2_r, y2_i, y2_r): + if v >= bn128.field_modulus: + return [] + fq2_x = bn128.FQ2([x2_r, x2_i]) + fq2_y = bn128.FQ2([y2_r, y2_i]) + if (fq2_x, fq2_y) != (bn128.FQ2.zero(), bn128.FQ2.zero()): + p2 = (fq2_x, fq2_y, bn128.FQ2.one()) + if not bn128.is_on_curve(p2, bn128.b2): + return [] + else: + p2 = zero + if bn128.multiply(p2, bn128.curve_order)[-1] != bn128.FQ2.zero(): + return [] + exponent *= bn128.pairing(p2, p1, final_exponentiate=False) + result = bn128.final_exponentiate(exponent) == bn128.FQ12.one() + return [0] * 31 + [1 if result else 0] + + +PRECOMPILE_FUNCTIONS = ( + ecrecover, + sha256, + ripemd160, + identity, + mod_exp, + ec_add, + ec_mul, + ec_pair, +) +PRECOMPILE_COUNT = len(PRECOMPILE_FUNCTIONS) + + def native_contracts(address: int, data: BaseCalldata) -> List[int]: """Takes integer address 1, 2, 3, 4. @@ -127,11 +214,10 @@ def native_contracts(address: int, data: BaseCalldata) -> List[int]: :param data: :return: """ - functions = (ecrecover, sha256, ripemd160, identity) if isinstance(data, ConcreteCalldata): concrete_data = data.concrete(None) else: raise NativeContractException() - return functions[address - 1](concrete_data) + return PRECOMPILE_FUNCTIONS[address - 1](concrete_data) diff --git a/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py b/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py index bb78fdd8..dacc6bd8 100644 --- a/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py +++ b/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py @@ -1,7 +1,10 @@ from mythril.laser.ethereum.svm import LaserEVM from mythril.laser.ethereum.plugins.plugin import LaserPlugin from mythril.laser.ethereum.plugins.signals import PluginSkipState -from mythril.laser.ethereum.state.annotation import StateAnnotation +from mythril.laser.ethereum.plugins.implementations.plugin_annotations import ( + DependencyAnnotation, + WSDependencyAnnotation, +) from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.transaction.transaction_models import ( ContractCreationTransaction, @@ -9,62 +12,12 @@ from mythril.laser.ethereum.transaction.transaction_models import ( from mythril.exceptions import UnsatError from mythril.analysis import solver from typing import cast, List, Dict, Set -from copy import copy import logging log = logging.getLogger(__name__) -class DependencyAnnotation(StateAnnotation): - """Dependency Annotation - - This annotation tracks read and write access to the state during each transaction. - """ - - def __init__(self): - self.storage_loaded = [] # type: List - self.storage_written = {} # type: Dict[int, List] - self.path = [0] # type: List - self.blocks_seen = set() # type: Set[int] - - def __copy__(self): - result = DependencyAnnotation() - result.storage_loaded = copy(self.storage_loaded) - result.storage_written = copy(self.storage_written) - result.path = copy(self.path) - result.blocks_seen = copy(self.blocks_seen) - return result - - def get_storage_write_cache(self, iteration: int): - if iteration not in self.storage_written: - self.storage_written[iteration] = [] - - return self.storage_written[iteration] - - def extend_storage_write_cache(self, iteration: int, value: object): - if iteration not in self.storage_written: - self.storage_written[iteration] = [value] - elif value not in self.storage_written[iteration]: - self.storage_written[iteration].append(value) - - -class WSDependencyAnnotation(StateAnnotation): - """Dependency Annotation for World state - - This world state annotation maintains a stack of state annotations. - It is used to transfer individual state annotations from one transaction to the next. - """ - - def __init__(self): - self.annotations_stack = [] - - def __copy__(self): - result = WSDependencyAnnotation() - result.annotations_stack = copy(self.annotations_stack) - return result - - def get_dependency_annotation(state: GlobalState) -> DependencyAnnotation: """ Returns a dependency annotation @@ -134,6 +87,7 @@ class DependencyPruner(LaserPlugin): def _reset(self): self.iteration = 0 + self.calls_on_path = {} # type: Dict[int, bool] self.sloads_on_path = {} # type: Dict[int, List[object]] self.sstores_on_path = {} # type: Dict[int, List[object]] self.storage_accessed_global = set() # type: Set @@ -166,6 +120,17 @@ class DependencyPruner(LaserPlugin): else: self.sstores_on_path[address] = [target_location] + def update_calls(self, path: List[int]) -> None: + """Update the dependency map for the block offsets on the given path. + + :param path + :param target_location + """ + + for address in path: + if address in self.sstores_on_path: + self.calls_on_path[address] = True + def wanna_execute(self, address: int, annotation: DependencyAnnotation) -> bool: """Decide whether the basic block starting at 'address' should be executed. @@ -175,6 +140,9 @@ class DependencyPruner(LaserPlugin): storage_write_cache = annotation.get_storage_write_cache(self.iteration - 1) + if address in self.calls_on_path: + return True + # Skip "pure" paths that don't have any dependencies. if address not in self.sloads_on_path: @@ -270,6 +238,13 @@ class DependencyPruner(LaserPlugin): self.update_sloads(annotation.path, location) self.storage_accessed_global.add(location) + @symbolic_vm.pre_hook("CALL") + def call_hook(state: GlobalState): + annotation = get_dependency_annotation(state) + + self.update_calls(annotation.path) + annotation.has_call = True + @symbolic_vm.pre_hook("STOP") def stop_hook(state: GlobalState): _transaction_end(state) @@ -293,11 +268,14 @@ class DependencyPruner(LaserPlugin): for index in annotation.storage_written: self.update_sstores(annotation.path, index) + if annotation.has_call: + self.update_calls(annotation.path) + def _check_basic_block(address: int, annotation: DependencyAnnotation): """This method is where the actual pruning happens. :param address: Start address (bytecode offset) of the block - :param annotation + :param annotation: """ # Don't skip any blocks in the contract creation transaction @@ -338,13 +316,3 @@ class DependencyPruner(LaserPlugin): annotation.storage_loaded = [] world_state_annotation.annotations_stack.append(annotation) - - log.debug( - "Iteration {}: Adding world state at address {}, end of function {}.\nDependency map: {}\nStorage written: {}".format( - self.iteration, - state.get_current_instruction()["address"], - state.node.function_name, - self.sloads_on_path, - annotation.storage_written[self.iteration], - ) - ) diff --git a/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py b/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py index 8a6fc9d6..6bc13d9e 100644 --- a/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py +++ b/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py @@ -1,23 +1,16 @@ -from mythril.laser.ethereum.state.annotation import StateAnnotation -from mythril.laser.ethereum.svm import LaserEVM from mythril.laser.ethereum.plugins.signals import PluginSkipWorldState from mythril.laser.ethereum.plugins.plugin import LaserPlugin +from mythril.laser.ethereum.plugins.implementations.plugin_annotations import ( + MutationAnnotation, +) from mythril.laser.ethereum.state.global_state import GlobalState +from mythril.laser.ethereum.svm import LaserEVM from mythril.laser.ethereum.transaction.transaction_models import ( ContractCreationTransaction, ) from mythril.laser.smt import And, symbol_factory -class MutationAnnotation(StateAnnotation): - """Mutation Annotation - - This is the annotation used by the MutationPruner plugin to record mutations - """ - - pass - - class MutationPruner(LaserPlugin): """Mutation pruner plugin @@ -42,7 +35,11 @@ class MutationPruner(LaserPlugin): """ @symbolic_vm.pre_hook("SSTORE") - def mutator_hook(global_state: GlobalState): + def sstore_mutator_hook(global_state: GlobalState): + global_state.annotate(MutationAnnotation()) + + @symbolic_vm.pre_hook("CALL") + def call_mutator_hook(global_state: GlobalState): global_state.annotate(MutationAnnotation()) @symbolic_vm.laser_hook("add_world_state") diff --git a/mythril/laser/ethereum/plugins/implementations/plugin_annotations.py b/mythril/laser/ethereum/plugins/implementations/plugin_annotations.py new file mode 100644 index 00000000..209e562e --- /dev/null +++ b/mythril/laser/ethereum/plugins/implementations/plugin_annotations.py @@ -0,0 +1,65 @@ +from mythril.laser.ethereum.state.annotation import StateAnnotation + +from copy import copy +from typing import Dict, List, Set + + +class MutationAnnotation(StateAnnotation): + """Mutation Annotation + + This is the annotation used by the MutationPruner plugin to record mutations + """ + + def __init__(self): + pass + + +class DependencyAnnotation(StateAnnotation): + """Dependency Annotation + + This annotation tracks read and write access to the state during each transaction. + """ + + def __init__(self): + self.storage_loaded = [] # type: List + self.storage_written = {} # type: Dict[int, List] + self.has_call = False # type: bool + self.path = [0] # type: List + self.blocks_seen = set() # type: Set[int] + + def __copy__(self): + result = DependencyAnnotation() + result.storage_loaded = copy(self.storage_loaded) + result.storage_written = copy(self.storage_written) + result.has_call = self.has_call + result.path = copy(self.path) + result.blocks_seen = copy(self.blocks_seen) + return result + + def get_storage_write_cache(self, iteration: int): + if iteration not in self.storage_written: + self.storage_written[iteration] = [] + + return self.storage_written[iteration] + + def extend_storage_write_cache(self, iteration: int, value: object): + if iteration not in self.storage_written: + self.storage_written[iteration] = [value] + elif value not in self.storage_written[iteration]: + self.storage_written[iteration].append(value) + + +class WSDependencyAnnotation(StateAnnotation): + """Dependency Annotation for World state + + This world state annotation maintains a stack of state annotations. + It is used to transfer individual state annotations from one transaction to the next. + """ + + def __init__(self): + self.annotations_stack = [] + + def __copy__(self): + result = WSDependencyAnnotation() + result.annotations_stack = copy(self.annotations_stack) + return result diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py index f5196287..c6afa0c3 100644 --- a/mythril/laser/ethereum/state/account.py +++ b/mythril/laser/ethereum/state/account.py @@ -2,8 +2,9 @@ This includes classes representing accounts and their storage. """ +import logging from copy import copy, deepcopy -from typing import Any, Dict, Union, Tuple, cast +from typing import Any, Dict, Union, Tuple, Set, cast from mythril.laser.smt import ( @@ -19,6 +20,28 @@ from mythril.laser.smt import ( from mythril.disassembler.disassembly import Disassembly from mythril.laser.smt import symbol_factory +log = logging.getLogger(__name__) + + +class StorageRegion: + def __getitem__(self, item): + raise NotImplementedError + + def __setitem__(self, key, value): + raise NotImplementedError + + +class ArrayStorageRegion(StorageRegion): + """ An ArrayStorageRegion is a storage region that leverages smt array theory to resolve expressions""" + + pass + + +class IteStorageRegion(StorageRegion): + """ An IteStorageRegion is a storage region that uses Ite statements to implement a storage""" + + pass + class Storage: """Storage class represents the storage of an Account.""" @@ -37,6 +60,7 @@ class Storage: self.printable_storage = {} # type: Dict[BitVec, BitVec] self.dynld = dynamic_loader + self.storage_keys_loaded = set() # type: Set[int] self.address = address @staticmethod @@ -51,17 +75,18 @@ class Storage: def __getitem__(self, item: BitVec) -> BitVec: storage, is_keccak_storage = self._get_corresponding_storage(item) if is_keccak_storage: - item = self._sanitize(cast(BitVecFunc, item).input_) - value = storage[item] + sanitized_item = self._sanitize(cast(BitVecFunc, item).input_) + else: + sanitized_item = item if ( - value.value == 0 - and self.address - and item.symbolic is False + self.address and self.address.value != 0 + and item.symbolic is False + and int(item.value) not in self.storage_keys_loaded and (self.dynld and self.dynld.storage_loading) ): try: - storage[item] = symbol_factory.BitVecVal( + storage[sanitized_item] = symbol_factory.BitVecVal( int( self.dynld.read_storage( contract_address="0x{:040X}".format(self.address.value), @@ -71,12 +96,12 @@ class Storage: ), 256, ) - self.printable_storage[item] = storage[item] - return storage[item] - except ValueError: - pass + self.storage_keys_loaded.add(int(item.value)) + self.printable_storage[item] = storage[sanitized_item] + except ValueError as e: + log.debug("Couldn't read storage at %s: %s", item, e) - return simplify(storage[item]) + return simplify(storage[sanitized_item]) @staticmethod def get_map_index(key: BitVec) -> BitVec: @@ -113,15 +138,18 @@ class Storage: if is_keccak_storage: key = self._sanitize(key.input_) storage[key] = value + if key.symbolic is False: + self.storage_keys_loaded.add(int(key.value)) - def __deepcopy__(self, memodict={}): + def __deepcopy__(self, memodict=dict()): concrete = isinstance(self._standard_storage, K) storage = Storage( concrete=concrete, address=self.address, dynamic_loader=self.dynld ) storage._standard_storage = deepcopy(self._standard_storage) storage._map_storage = deepcopy(self._map_storage) - storage.print_storage = copy(self.printable_storage) + storage.printable_storage = copy(self.printable_storage) + storage.storage_keys_loaded = copy(self.storage_keys_loaded) return storage def __str__(self) -> str: diff --git a/mythril/laser/ethereum/state/annotation.py b/mythril/laser/ethereum/state/annotation.py index 6a321776..0f25a311 100644 --- a/mythril/laser/ethereum/state/annotation.py +++ b/mythril/laser/ethereum/state/annotation.py @@ -12,6 +12,8 @@ class StateAnnotation: traverse the state space themselves. """ + # TODO: Remove this? It seems to be used only in the MutationPruner, and + # we could simply use world state annotations if we want them to be persisted. @property def persist_to_world_state(self) -> bool: """If this function returns true then laser will also annotate the diff --git a/mythril/laser/ethereum/state/calldata.py b/mythril/laser/ethereum/state/calldata.py index a8ebfa2b..f7fa0036 100644 --- a/mythril/laser/ethereum/state/calldata.py +++ b/mythril/laser/ethereum/state/calldata.py @@ -70,7 +70,7 @@ class BaseCalldata: try: current_index = ( start - if isinstance(start, Expression) + if isinstance(start, BitVec) else symbol_factory.BitVecVal(start, 256) ) parts = [] diff --git a/mythril/laser/ethereum/state/environment.py b/mythril/laser/ethereum/state/environment.py index a3300f9a..4cfb51e0 100644 --- a/mythril/laser/ethereum/state/environment.py +++ b/mythril/laser/ethereum/state/environment.py @@ -22,6 +22,7 @@ class Environment: callvalue: ExprRef, origin: ExprRef, code=None, + static=False, ) -> None: """ @@ -32,7 +33,7 @@ class Environment: :param callvalue: :param origin: :param code: - :param calldata_type: + :param static: Makes the environment static. """ # Metadata @@ -50,6 +51,7 @@ class Environment: self.gasprice = gasprice self.origin = origin self.callvalue = callvalue + self.static = static def __str__(self) -> str: """ diff --git a/mythril/laser/ethereum/state/global_state.py b/mythril/laser/ethereum/state/global_state.py index 86364a69..0e15209d 100644 --- a/mythril/laser/ethereum/state/global_state.py +++ b/mythril/laser/ethereum/state/global_state.py @@ -52,6 +52,14 @@ class GlobalState: self.last_return_data = last_return_data self._annotations = annotations or [] + def add_annotations(self, annotations: List[StateAnnotation]): + """ + Function used to add annotations to global state + :param annotations: + :return: + """ + self._annotations += annotations + def __copy__(self) -> "GlobalState": """ @@ -86,9 +94,12 @@ class GlobalState: :return: """ - instructions = self.environment.code.instruction_list - return instructions[self.mstate.pc] + try: + return instructions[self.mstate.pc] + except KeyError: + new_instruction = {"address": self.mstate.pc, "opcode": "STOP"} + return new_instruction @property def current_transaction( diff --git a/mythril/laser/ethereum/state/world_state.py b/mythril/laser/ethereum/state/world_state.py index 236da526..20628877 100644 --- a/mythril/laser/ethereum/state/world_state.py +++ b/mythril/laser/ethereum/state/world_state.py @@ -27,6 +27,7 @@ class WorldState: """ self._accounts = {} # type: Dict[int, Account] self.balances = Array("balance", 256, 256) + self.starting_balances = copy(self.balances) self.node = None # type: Optional['Node'] self.transaction_sequence = transaction_sequence or [] @@ -60,6 +61,7 @@ class WorldState: annotations=new_annotations, ) new_world_state.balances = copy(self.balances) + new_world_state.starting_balances = copy(self.starting_balances) for account in self._accounts.values(): new_world_state.put_account(copy(account)) new_world_state.node = self.node @@ -115,7 +117,7 @@ class WorldState: concrete_storage=concrete_storage, ) if balance: - new_account.set_balance(symbol_factory.BitVecVal(balance, 256)) + new_account.add_balance(symbol_factory.BitVecVal(balance, 256)) self.put_account(new_account) return new_account diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 9755fc33..af52c12b 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -3,14 +3,18 @@ import logging from collections import defaultdict from copy import copy from datetime import datetime, timedelta -from typing import Callable, Dict, DefaultDict, List, Tuple, Union +from typing import Callable, Dict, DefaultDict, List, Tuple, Optional +from mythril.analysis.potential_issues import check_potential_issues from mythril.laser.ethereum.cfg import NodeFlags, Node, Edge, JumpType from mythril.laser.ethereum.evm_exceptions import StackUnderflowException from mythril.laser.ethereum.evm_exceptions import VmException from mythril.laser.ethereum.instructions import Instruction from mythril.laser.ethereum.iprof import InstructionProfiler from mythril.laser.ethereum.plugins.signals import PluginSkipWorldState, PluginSkipState +from mythril.laser.ethereum.plugins.implementations.plugin_annotations import ( + MutationAnnotation, +) from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.state.world_state import WorldState from mythril.laser.ethereum.strategy.basic import DepthFirstSearchStrategy @@ -55,6 +59,8 @@ class LaserEVM: transaction_count=2, requires_statespace=True, enable_iprof=False, + enable_coverage_strategy=False, + instruction_laser_plugin=None, ) -> None: """ Initializes the laser evm object @@ -73,6 +79,7 @@ class LaserEVM: self.total_states = 0 self.dynamic_loader = dynamic_loader + # TODO: What about using a deque here? self.work_list = [] # type: List[GlobalState] self.strategy = strategy(self.work_list, max_depth) self.max_depth = max_depth @@ -102,6 +109,13 @@ class LaserEVM: self.iprof = InstructionProfiler() if enable_iprof else None + if enable_coverage_strategy: + from mythril.laser.ethereum.plugins.implementations.coverage.coverage_strategy import ( + CoverageStrategy, + ) + + self.strategy = CoverageStrategy(self.strategy, instruction_laser_plugin) + log.info("LASER EVM initialized with dynamic loader: " + str(dynamic_loader)) def extend_strategy(self, extension: ABCMeta, *args) -> None: @@ -200,7 +214,7 @@ class LaserEVM: for hook in self._stop_sym_trans_hooks: hook() - def exec(self, create=False, track_gas=False) -> Union[List[GlobalState], None]: + def exec(self, create=False, track_gas=False) -> Optional[List[GlobalState]]: """ :param create: @@ -214,6 +228,7 @@ class LaserEVM: and create and self.time + timedelta(seconds=self.create_timeout) <= datetime.now() ): + log.debug("Hit create timeout, returning.") return final_states + [global_state] if track_gas else None if ( @@ -222,6 +237,7 @@ class LaserEVM: <= datetime.now() and not create ): + log.debug("Hit execution timeout, returning.") return final_states + [global_state] if track_gas else None try: @@ -234,8 +250,7 @@ class LaserEVM: state for state in new_states if state.mstate.constraints.is_possible ] - self.manage_cfg(op_code, new_states) - + self.manage_cfg(op_code, new_states) # TODO: What about op_code is None? if new_states: self.work_list += new_states elif track_gas: @@ -246,6 +261,7 @@ class LaserEVM: def _add_world_state(self, global_state: GlobalState): """ Stores the world_state of the passed global state in the open states""" + for hook in self._add_world_state_hooks: try: hook(global_state) @@ -256,11 +272,11 @@ class LaserEVM: def execute_state( self, global_state: GlobalState - ) -> Tuple[List[GlobalState], Union[str, None]]: - """ + ) -> Tuple[List[GlobalState], Optional[str]]: + """Execute a single instruction in global_state. :param global_state: - :return: + :return: A list of successor states. """ # Execute hooks for hook in self._execute_state_hooks: @@ -312,7 +328,11 @@ class LaserEVM: global_state.transaction_stack ) + [(start_signal.transaction, global_state)] new_global_state.node = global_state.node - new_global_state.mstate.constraints = global_state.mstate.constraints + new_global_state.mstate.constraints = ( + start_signal.global_state.mstate.constraints + ) + + log.debug("Starting new transaction %s", start_signal.transaction) return [new_global_state], op_code @@ -321,11 +341,15 @@ class LaserEVM: -1 ] + log.debug("Ending transaction %s.", transaction) + if return_global_state is None: if ( not isinstance(transaction, ContractCreationTransaction) or transaction.return_data ) and not end_signal.revert: + check_potential_issues(global_state) + end_signal.global_state.world_state.node = global_state.node self._add_world_state(end_signal.global_state) new_global_states = [] @@ -333,6 +357,19 @@ class LaserEVM: # First execute the post hook for the transaction ending instruction self._execute_post_hook(op_code, [end_signal.global_state]) + # Propogate codecall based annotations + if return_global_state.get_current_instruction()["opcode"] in ( + "DELEGATECALL", + "CALLCODE", + ): + new_annotations = [ + annotation + for annotation in global_state.get_annotations( + MutationAnnotation + ) + ] + return_global_state.add_annotations(new_annotations) + new_global_states = self._end_message_call( copy(return_global_state), global_state, @@ -373,6 +410,15 @@ class LaserEVM: return_global_state.environment.active_account = global_state.accounts[ return_global_state.environment.active_account.address.value ] + if isinstance( + global_state.current_transaction, ContractCreationTransaction + ): + return_global_state.mstate.min_gas_used += ( + global_state.mstate.min_gas_used + ) + return_global_state.mstate.max_gas_used += ( + global_state.mstate.max_gas_used + ) # Execute the post instruction handler new_global_states = Instruction( @@ -396,6 +442,7 @@ class LaserEVM: for state in new_states: self._new_node_state(state) elif opcode == "JUMPI": + assert len(new_states) <= 2 for state in new_states: self._new_node_state( state, JumpType.CONDITIONAL, state.mstate.constraints[-1] diff --git a/mythril/laser/ethereum/transaction/symbolic.py b/mythril/laser/ethereum/transaction/symbolic.py index 1a895048..b8b6692c 100644 --- a/mythril/laser/ethereum/transaction/symbolic.py +++ b/mythril/laser/ethereum/transaction/symbolic.py @@ -23,7 +23,7 @@ ATTACKER_ADDRESS = 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF ACTOR_ADDRESSES = [ symbol_factory.BitVecVal(0xAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFE, 256), symbol_factory.BitVecVal(0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF, 256), - symbol_factory.BitVecVal(0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEE, 256), + symbol_factory.BitVecVal(0xAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA, 256), ] @@ -85,6 +85,8 @@ def execute_contract_creation( new_account = None for open_world_state in open_states: next_transaction_id = get_next_transaction_id() + # call_data "should" be '[]', but it is easier to model the calldata symbolically + # and add logic in codecopy/codesize/calldatacopy/calldatasize than to model code "correctly" transaction = ContractCreationTransaction( world_state=open_world_state, identifier=next_transaction_id, @@ -98,7 +100,7 @@ def execute_contract_creation( code=Disassembly(contract_initialization_code), caller=symbol_factory.BitVecVal(CREATOR_ADDRESS, 256), contract_name=contract_name, - call_data=[], + call_data=None, call_value=symbol_factory.BitVecSym( "call_value{}".format(next_transaction_id), 256 ), diff --git a/mythril/laser/ethereum/transaction/transaction_models.py b/mythril/laser/ethereum/transaction/transaction_models.py index 93cc7e3b..b36cc61d 100644 --- a/mythril/laser/ethereum/transaction/transaction_models.py +++ b/mythril/laser/ethereum/transaction/transaction_models.py @@ -4,7 +4,7 @@ execution.""" import array from copy import deepcopy from z3 import ExprRef -from typing import Union, Optional, cast +from typing import Union, Optional from mythril.laser.ethereum.state.calldata import ConcreteCalldata from mythril.laser.ethereum.state.account import Account @@ -12,8 +12,10 @@ from mythril.laser.ethereum.state.calldata import BaseCalldata, SymbolicCalldata from mythril.laser.ethereum.state.environment import Environment from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.state.world_state import WorldState -from mythril.disassembler.disassembly import Disassembly -from mythril.laser.smt import symbol_factory +from mythril.laser.smt import symbol_factory, UGE, BitVec +import logging + +log = logging.getLogger(__name__) _next_transaction_id = 0 @@ -43,9 +45,11 @@ class TransactionStartSignal(Exception): self, transaction: Union["MessageCallTransaction", "ContractCreationTransaction"], op_code: str, + global_state: GlobalState, ) -> None: self.transaction = transaction self.op_code = op_code + self.global_state = global_state class BaseTransaction: @@ -64,6 +68,7 @@ class BaseTransaction: code=None, call_value=None, init_call_data=True, + static=False, ) -> None: assert isinstance(world_state, WorldState) self.world_state = world_state @@ -99,7 +104,7 @@ class BaseTransaction: if call_value is not None else symbol_factory.BitVecSym("callvalue{}".format(identifier), 256) ) - + self.static = static self.return_data = None # type: str def initial_global_state_from_environment(self, environment, active_function): @@ -115,16 +120,31 @@ class BaseTransaction: sender = environment.sender receiver = environment.active_account.address - value = environment.callvalue + value = ( + environment.callvalue + if isinstance(environment.callvalue, BitVec) + else symbol_factory.BitVecVal(environment.callvalue, 256) + ) - global_state.world_state.balances[sender] -= value + global_state.mstate.constraints.append( + UGE(global_state.world_state.balances[sender], value) + ) global_state.world_state.balances[receiver] += value + global_state.world_state.balances[sender] -= value return global_state def initial_global_state(self) -> GlobalState: raise NotImplementedError + def __str__(self) -> str: + return "{} {} from {} to {:#42x}".format( + self.__class__.__name__, + self.id, + self.caller, + int(str(self.callee_account.address)) if self.callee_account else -1, + ) + class MessageCallTransaction(BaseTransaction): """Transaction object models an transaction.""" @@ -142,6 +162,7 @@ class MessageCallTransaction(BaseTransaction): self.call_value, self.origin, code=self.code or self.callee_account.code, + static=self.static, ) return super().initial_global_state_from_environment( environment, active_function="fallback" @@ -174,13 +195,18 @@ class ContractCreationTransaction(BaseTransaction): code=None, call_value=None, contract_name=None, + contract_address=None, ) -> None: self.prev_world_state = deepcopy(world_state) + contract_address = ( + contract_address if isinstance(contract_address, int) else None + ) callee_account = world_state.create_account( - 0, concrete_storage=True, creator=caller.value + 0, concrete_storage=True, creator=caller.value, address=contract_address ) - callee_account.contract_name = contract_name - # TODO: set correct balance for new account + callee_account.contract_name = contract_name or callee_account.contract_name + # init_call_data "should" be false, but it is easier to model the calldata symbolically + # and add logic in codecopy/codesize/calldatacopy/calldatasize than to model code "correctly" super().__init__( world_state=world_state, callee_account=callee_account, @@ -192,7 +218,7 @@ class ContractCreationTransaction(BaseTransaction): origin=origin, code=code, call_value=call_value, - init_call_data=False, + init_call_data=True, ) def initial_global_state(self) -> GlobalState: diff --git a/mythril/laser/ethereum/util.py b/mythril/laser/ethereum/util.py index 9cb5d950..ff544559 100644 --- a/mythril/laser/ethereum/util.py +++ b/mythril/laser/ethereum/util.py @@ -45,7 +45,7 @@ def get_instruction_index( """ index = 0 for instr in instruction_list: - if instr["address"] == address: + if instr["address"] >= address: return index index += 1 return None @@ -150,3 +150,27 @@ def bytearray_to_int(arr): for a in arr: o = (o << 8) + a return o + + +def extract_copy( + data: bytearray, mem: bytearray, memstart: int, datastart: int, size: int +): + for i in range(size): + if datastart + i < len(data): + mem[memstart + i] = data[datastart + i] + else: + mem[memstart + i] = 0 + + +def extract32(data: bytearray, i: int) -> int: + """ + + :param data: + :param i: + :return: + """ + if i >= len(data): + return 0 + o = data[i : min(i + 32, len(data))] + o.extend(bytearray(32 - len(o))) + return bytearray_to_int(o) diff --git a/mythril/laser/smt/__init__.py b/mythril/laser/smt/__init__.py index f441948e..6ab752ce 100644 --- a/mythril/laser/smt/__init__.py +++ b/mythril/laser/smt/__init__.py @@ -1,8 +1,10 @@ -from mythril.laser.smt.bitvec import ( - BitVec, +from mythril.laser.smt.bitvec import BitVec + +from mythril.laser.smt.bitvec_helper import ( If, UGT, ULT, + ULE, Concat, Extract, URem, @@ -15,6 +17,7 @@ from mythril.laser.smt.bitvec import ( BVSubNoUnderflow, LShR, ) + from mythril.laser.smt.bitvecfunc import BitVecFunc from mythril.laser.smt.expression import Expression, simplify from mythril.laser.smt.bool import Bool, is_true, is_false, Or, Not, And diff --git a/mythril/laser/smt/array.py b/mythril/laser/smt/array.py index 00107df1..9289b290 100644 --- a/mythril/laser/smt/array.py +++ b/mythril/laser/smt/array.py @@ -8,7 +8,8 @@ default values over a certain range. from typing import cast import z3 -from mythril.laser.smt.bitvec import BitVec, If +from mythril.laser.smt.bitvec import BitVec +from mythril.laser.smt.bitvec_helper import If from mythril.laser.smt.bool import Bool diff --git a/mythril/laser/smt/bitvec.py b/mythril/laser/smt/bitvec.py index df537582..b308e863 100644 --- a/mythril/laser/smt/bitvec.py +++ b/mythril/laser/smt/bitvec.py @@ -1,10 +1,11 @@ """This module provides classes for an SMT abstraction of bit vectors.""" -from typing import Union, overload, List, Set, cast, Any, Optional, Callable from operator import lshift, rshift, ne, eq +from typing import Union, Set, cast, Any, Optional, Callable + import z3 -from mythril.laser.smt.bool import Bool, And, Or +from mythril.laser.smt.bool import Bool from mythril.laser.smt.expression import Expression Annotations = Set[Any] @@ -276,276 +277,5 @@ class BitVec(Expression[z3.BitVecRef]): return self.raw.__hash__() -def _comparison_helper( - a: BitVec, b: BitVec, operation: Callable, default_value: bool, inputs_equal: bool -) -> Bool: - annotations = a.annotations.union(b.annotations) - if isinstance(a, BitVecFunc): - if not a.symbolic and not b.symbolic: - return Bool(operation(a.raw, b.raw), annotations=annotations) - - if ( - not isinstance(b, BitVecFunc) - or not a.func_name - or not a.input_ - or not a.func_name == b.func_name - ): - return Bool(z3.BoolVal(default_value), annotations=annotations) - - return And( - Bool(operation(a.raw, b.raw), annotations=annotations), - a.input_ == b.input_ if inputs_equal else a.input_ != b.input_, - ) - - return Bool(operation(a.raw, b.raw), annotations) - - -def _arithmetic_helper(a: BitVec, b: BitVec, operation: Callable) -> BitVec: - raw = operation(a.raw, b.raw) - union = a.annotations.union(b.annotations) - - if isinstance(a, BitVecFunc) and isinstance(b, BitVecFunc): - return BitVecFunc(raw=raw, func_name=None, input_=None, annotations=union) - elif isinstance(a, BitVecFunc): - return BitVecFunc( - raw=raw, func_name=a.func_name, input_=a.input_, annotations=union - ) - elif isinstance(b, BitVecFunc): - return BitVecFunc( - raw=raw, func_name=b.func_name, input_=b.input_, annotations=union - ) - - return BitVec(raw, annotations=union) - - -def LShR(a: BitVec, b: BitVec): - return _arithmetic_helper(a, b, z3.LShR) - - -def If(a: Union[Bool, bool], b: Union[BitVec, int], c: Union[BitVec, int]) -> BitVec: - """Create an if-then-else expression. - - :param a: - :param b: - :param c: - :return: - """ - # TODO: Handle BitVecFunc - - if not isinstance(a, Bool): - a = Bool(z3.BoolVal(a)) - if not isinstance(b, BitVec): - b = BitVec(z3.BitVecVal(b, 256)) - if not isinstance(c, BitVec): - c = BitVec(z3.BitVecVal(c, 256)) - union = a.annotations.union(b.annotations).union(c.annotations) - return BitVec(z3.If(a.raw, b.raw, c.raw), union) - - -def UGT(a: BitVec, b: BitVec) -> Bool: - """Create an unsigned greater than expression. - - :param a: - :param b: - :return: - """ - return _comparison_helper(a, b, z3.UGT, default_value=False, inputs_equal=False) - - -def UGE(a: BitVec, b: BitVec) -> Bool: - """Create an unsigned greater or equals expression. - - :param a: - :param b: - :return: - """ - return Or(UGT(a, b), a == b) - - -def ULT(a: BitVec, b: BitVec) -> Bool: - """Create an unsigned less than expression. - - :param a: - :param b: - :return: - """ - return _comparison_helper(a, b, z3.ULT, default_value=False, inputs_equal=False) - - -def ULE(a: BitVec, b: BitVec) -> Bool: - """Create an unsigned less than expression. - - :param a: - :param b: - :return: - """ - return Or(ULT(a, b), a == b) - - -@overload -def Concat(*args: List[BitVec]) -> BitVec: ... - - -@overload -def Concat(*args: BitVec) -> BitVec: ... - - -def Concat(*args: Union[BitVec, List[BitVec]]) -> BitVec: - """Create a concatenation expression. - - :param args: - :return: - """ - # The following statement is used if a list is provided as an argument to concat - if len(args) == 1 and isinstance(args[0], list): - bvs = args[0] # type: List[BitVec] - else: - bvs = cast(List[BitVec], args) - - nraw = z3.Concat([a.raw for a in bvs]) - annotations = set() # type: Annotations - bitvecfunc = False - for bv in bvs: - annotations = annotations.union(bv.annotations) - if isinstance(bv, BitVecFunc): - bitvecfunc = True - - if bitvecfunc: - # Added this not so good and misleading NOTATION to help with this - str_hash = ",".join(["hashed({})".format(hash(bv)) for bv in bvs]) - input_string = "MisleadingNotationConcat({})".format(str_hash) - - return BitVecFunc( - raw=nraw, func_name="Hybrid", input_=BitVec(z3.BitVec(input_string, 256), annotations=annotations) - ) - - return BitVec(nraw, annotations) - - -def Extract(high: int, low: int, bv: BitVec) -> BitVec: - """Create an extract expression. - - :param high: - :param low: - :param bv: - :return: - """ - raw = z3.Extract(high, low, bv.raw) - if isinstance(bv, BitVecFunc): - input_string = "MisleadingNotationExtract({}, {}, hashed({}))".format(high, low, hash(bv)) - # Is there a better value to set func_name and input to in this case? - return BitVecFunc( - raw=raw, func_name="Hybrid", input_=BitVec(z3.BitVec(input_string, 256), annotations=bv.annotations) - ) - - return BitVec(raw, annotations=bv.annotations) - - -def URem(a: BitVec, b: BitVec) -> BitVec: - """Create an unsigned remainder expression. - - :param a: - :param b: - :return: - """ - return _arithmetic_helper(a, b, z3.URem) - - -def SRem(a: BitVec, b: BitVec) -> BitVec: - """Create a signed remainder expression. - - :param a: - :param b: - :return: - """ - return _arithmetic_helper(a, b, z3.SRem) - - -def UDiv(a: BitVec, b: BitVec) -> BitVec: - """Create an unsigned division expression. - - :param a: - :param b: - :return: - """ - return _arithmetic_helper(a, b, z3.UDiv) - - -def Sum(*args: BitVec) -> BitVec: - """Create sum expression. - - :return: - """ - raw = z3.Sum([a.raw for a in args]) - annotations = set() # type: Annotations - bitvecfuncs = [] - - for bv in args: - annotations = annotations.union(bv.annotations) - if isinstance(bv, BitVecFunc): - bitvecfuncs.append(bv) - - if len(bitvecfuncs) >= 2: - return BitVecFunc(raw=raw, func_name="Hybrid", input_=None, annotations=annotations) - elif len(bitvecfuncs) == 1: - return BitVecFunc( - raw=raw, - func_name=bitvecfuncs[0].func_name, - input_=bitvecfuncs[0].input_, - annotations=annotations, - ) - - return BitVec(raw, annotations) - - -def BVAddNoOverflow(a: Union[BitVec, int], b: Union[BitVec, int], signed: bool) -> Bool: - """Creates predicate that verifies that the addition doesn't overflow. - - :param a: - :param b: - :param signed: - :return: - """ - if not isinstance(a, BitVec): - a = BitVec(z3.BitVecVal(a, 256)) - if not isinstance(b, BitVec): - b = BitVec(z3.BitVecVal(b, 256)) - return Bool(z3.BVAddNoOverflow(a.raw, b.raw, signed)) - - -def BVMulNoOverflow(a: Union[BitVec, int], b: Union[BitVec, int], signed: bool) -> Bool: - """Creates predicate that verifies that the multiplication doesn't - overflow. - - :param a: - :param b: - :param signed: - :return: - """ - if not isinstance(a, BitVec): - a = BitVec(z3.BitVecVal(a, 256)) - if not isinstance(b, BitVec): - b = BitVec(z3.BitVecVal(b, 256)) - return Bool(z3.BVMulNoOverflow(a.raw, b.raw, signed)) - - -def BVSubNoUnderflow( - a: Union[BitVec, int], b: Union[BitVec, int], signed: bool -) -> Bool: - """Creates predicate that verifies that the subtraction doesn't overflow. - - :param a: - :param b: - :param signed: - :return: - """ - if not isinstance(a, BitVec): - a = BitVec(z3.BitVecVal(a, 256)) - if not isinstance(b, BitVec): - b = BitVec(z3.BitVecVal(b, 256)) - - return Bool(z3.BVSubNoUnderflow(a.raw, b.raw, signed)) - - # TODO: Fix circular import issues from mythril.laser.smt.bitvecfunc import BitVecFunc diff --git a/mythril/laser/smt/bitvec_helper.py b/mythril/laser/smt/bitvec_helper.py new file mode 100644 index 00000000..8e68e0c9 --- /dev/null +++ b/mythril/laser/smt/bitvec_helper.py @@ -0,0 +1,291 @@ +from typing import Union, overload, List, Set, cast, Any, Optional, Callable +from operator import lshift, rshift, ne, eq +import z3 + +from mythril.laser.smt.bool import Bool, And, Or +from mythril.laser.smt.bitvec import BitVec +from mythril.laser.smt.bitvecfunc import BitVecFunc +from mythril.laser.smt.bitvecfunc import _arithmetic_helper as _func_arithmetic_helper +from mythril.laser.smt.bitvecfunc import _comparison_helper as _func_comparison_helper + +Annotations = Set[Any] + + +def _comparison_helper( + a: BitVec, b: BitVec, operation: Callable, default_value: bool, inputs_equal: bool +) -> Bool: + annotations = a.annotations.union(b.annotations) + if isinstance(a, BitVecFunc): + return _func_comparison_helper(a, b, operation, default_value, inputs_equal) + return Bool(operation(a.raw, b.raw), annotations) + + +def _arithmetic_helper(a: BitVec, b: BitVec, operation: Callable) -> BitVec: + raw = operation(a.raw, b.raw) + union = a.annotations.union(b.annotations) + + if isinstance(a, BitVecFunc): + return _func_arithmetic_helper(a, b, operation) + elif isinstance(b, BitVecFunc): + return _func_arithmetic_helper(b, a, operation) + + return BitVec(raw, annotations=union) + + +def LShR(a: BitVec, b: BitVec): + return _arithmetic_helper(a, b, z3.LShR) + + +def If(a: Union[Bool, bool], b: Union[BitVec, int], c: Union[BitVec, int]) -> BitVec: + """Create an if-then-else expression. + + :param a: + :param b: + :param c: + :return: + """ + # TODO: Handle BitVecFunc + + if not isinstance(a, Bool): + a = Bool(z3.BoolVal(a)) + if not isinstance(b, BitVec): + b = BitVec(z3.BitVecVal(b, 256)) + if not isinstance(c, BitVec): + c = BitVec(z3.BitVecVal(c, 256)) + union = a.annotations.union(b.annotations).union(c.annotations) + + bvf = [] # type: List[BitVecFunc] + if isinstance(a, BitVecFunc): + bvf += [a] + if isinstance(b, BitVecFunc): + bvf += [b] + if isinstance(c, BitVecFunc): + bvf += [c] + if bvf: + raw = z3.If(a.raw, b.raw, c.raw) + nested_functions = [nf for func in bvf for nf in func.nested_functions] + bvf + return BitVecFunc(raw, func_name="Hybrid", nested_functions=nested_functions) + + return BitVec(z3.If(a.raw, b.raw, c.raw), union) + + +def UGT(a: BitVec, b: BitVec) -> Bool: + """Create an unsigned greater than expression. + + :param a: + :param b: + :return: + """ + return _comparison_helper(a, b, z3.UGT, default_value=False, inputs_equal=False) + + +def UGE(a: BitVec, b: BitVec) -> Bool: + """Create an unsigned greater or equals expression. + + :param a: + :param b: + :return: + """ + return Or(UGT(a, b), a == b) + + +def ULT(a: BitVec, b: BitVec) -> Bool: + """Create an unsigned less than expression. + + :param a: + :param b: + :return: + """ + return _comparison_helper(a, b, z3.ULT, default_value=False, inputs_equal=False) + + +def ULE(a: BitVec, b: BitVec) -> Bool: + """Create an unsigned less than expression. + + :param a: + :param b: + :return: + """ + return Or(ULT(a, b), a == b) + + +@overload +def Concat(*args: List[BitVec]) -> BitVec: + ... + + +@overload +def Concat(*args: BitVec) -> BitVec: + ... + + +def Concat(*args: Union[BitVec, List[BitVec]]) -> BitVec: + """Create a concatenation expression. + + :param args: + :return: + """ + # The following statement is used if a list is provided as an argument to concat + if len(args) == 1 and isinstance(args[0], list): + bvs = args[0] # type: List[BitVec] + else: + bvs = cast(List[BitVec], args) + + nraw = z3.Concat([a.raw for a in bvs]) + annotations = set() # type: Annotations + + nested_functions = [] # type: List[BitVecFunc] + for bv in bvs: + annotations = annotations.union(bv.annotations) + if isinstance(bv, BitVecFunc): + nested_functions += bv.nested_functions + nested_functions += [bv] + + if nested_functions: + return BitVecFunc( + raw=nraw, + func_name="Hybrid", + input_=BitVec(z3.BitVec("", 256), annotations=annotations), + nested_functions=nested_functions, + ) + + return BitVec(nraw, annotations) + + +def Extract(high: int, low: int, bv: BitVec) -> BitVec: + """Create an extract expression. + + :param high: + :param low: + :param bv: + :return: + """ + raw = z3.Extract(high, low, bv.raw) + if isinstance(bv, BitVecFunc): + input_string = "" + # Is there a better value to set func_name and input to in this case? + return BitVecFunc( + raw=raw, + func_name="Hybrid", + input_=BitVec(z3.BitVec(input_string, 256), annotations=bv.annotations), + nested_functions=bv.nested_functions + [bv], + ) + + return BitVec(raw, annotations=bv.annotations) + + +def URem(a: BitVec, b: BitVec) -> BitVec: + """Create an unsigned remainder expression. + + :param a: + :param b: + :return: + """ + return _arithmetic_helper(a, b, z3.URem) + + +def SRem(a: BitVec, b: BitVec) -> BitVec: + """Create a signed remainder expression. + + :param a: + :param b: + :return: + """ + return _arithmetic_helper(a, b, z3.SRem) + + +def UDiv(a: BitVec, b: BitVec) -> BitVec: + """Create an unsigned division expression. + + :param a: + :param b: + :return: + """ + return _arithmetic_helper(a, b, z3.UDiv) + + +def Sum(*args: BitVec) -> BitVec: + """Create sum expression. + + :return: + """ + raw = z3.Sum([a.raw for a in args]) + annotations = set() # type: Annotations + bitvecfuncs = [] + + for bv in args: + annotations = annotations.union(bv.annotations) + if isinstance(bv, BitVecFunc): + bitvecfuncs.append(bv) + + nested_functions = [ + nf for func in bitvecfuncs for nf in func.nested_functions + ] + bitvecfuncs + + if len(bitvecfuncs) >= 2: + return BitVecFunc( + raw=raw, + func_name="Hybrid", + input_=None, + annotations=annotations, + nested_functions=nested_functions, + ) + elif len(bitvecfuncs) == 1: + return BitVecFunc( + raw=raw, + func_name=bitvecfuncs[0].func_name, + input_=bitvecfuncs[0].input_, + annotations=annotations, + nested_functions=nested_functions, + ) + + return BitVec(raw, annotations) + + +def BVAddNoOverflow(a: Union[BitVec, int], b: Union[BitVec, int], signed: bool) -> Bool: + """Creates predicate that verifies that the addition doesn't overflow. + + :param a: + :param b: + :param signed: + :return: + """ + if not isinstance(a, BitVec): + a = BitVec(z3.BitVecVal(a, 256)) + if not isinstance(b, BitVec): + b = BitVec(z3.BitVecVal(b, 256)) + return Bool(z3.BVAddNoOverflow(a.raw, b.raw, signed)) + + +def BVMulNoOverflow(a: Union[BitVec, int], b: Union[BitVec, int], signed: bool) -> Bool: + """Creates predicate that verifies that the multiplication doesn't + overflow. + + :param a: + :param b: + :param signed: + :return: + """ + if not isinstance(a, BitVec): + a = BitVec(z3.BitVecVal(a, 256)) + if not isinstance(b, BitVec): + b = BitVec(z3.BitVecVal(b, 256)) + return Bool(z3.BVMulNoOverflow(a.raw, b.raw, signed)) + + +def BVSubNoUnderflow( + a: Union[BitVec, int], b: Union[BitVec, int], signed: bool +) -> Bool: + """Creates predicate that verifies that the subtraction doesn't overflow. + + :param a: + :param b: + :param signed: + :return: + """ + if not isinstance(a, BitVec): + a = BitVec(z3.BitVecVal(a, 256)) + if not isinstance(b, BitVec): + b = BitVec(z3.BitVecVal(b, 256)) + + return Bool(z3.BVSubNoUnderflow(a.raw, b.raw, signed)) diff --git a/mythril/laser/smt/bitvecfunc.py b/mythril/laser/smt/bitvecfunc.py index 6a96d2f1..c645b146 100644 --- a/mythril/laser/smt/bitvecfunc.py +++ b/mythril/laser/smt/bitvecfunc.py @@ -1,11 +1,10 @@ -from typing import Optional, Union, cast, Callable - +import operator +from itertools import product +from typing import Optional, Union, cast, Callable, List import z3 -from mythril.laser.smt.bitvec import BitVec, Bool, And, Annotations -from mythril.laser.smt.bool import Or - -import operator +from mythril.laser.smt.bitvec import BitVec, Annotations +from mythril.laser.smt.bool import Or, Bool, And def _arithmetic_helper( @@ -26,18 +25,19 @@ def _arithmetic_helper( union = a.annotations.union(b.annotations) if isinstance(b, BitVecFunc): - # TODO: Find better value to set input and name to in this case? - input_string = "MisleadingNotationop(invhash({}) {} invhash({})".format( - hash(a), operation, hash(b) - ) return BitVecFunc( raw=raw, func_name="Hybrid", - input_=BitVec(z3.BitVec(input_string, 256), annotations=union), + input_=BitVec(z3.BitVec("", 256), annotations=union), + nested_functions=a.nested_functions + b.nested_functions + [a, b], ) return BitVecFunc( - raw=raw, func_name=a.func_name, input_=a.input_, annotations=union + raw=raw, + func_name=a.func_name, + input_=a.input_, + annotations=union, + nested_functions=a.nested_functions + [a], ) @@ -62,23 +62,58 @@ def _comparison_helper( union = a.annotations.union(b.annotations) if not a.symbolic and not b.symbolic: + if operation == z3.UGT: + operation = operator.gt + if operation == z3.ULT: + operation = operator.lt return Bool(z3.BoolVal(operation(a.value, b.value)), annotations=union) - if ( not isinstance(b, BitVecFunc) or not a.func_name or not a.input_ or not a.func_name == b.func_name + or str(operation) not in ("", "") ): return Bool(z3.BoolVal(default_value), annotations=union) + condition = True + for a_nest, b_nest in product(a.nested_functions, b.nested_functions): + if a_nest.func_name != b_nest.func_name: + continue + if a_nest.func_name == "Hybrid": + continue + # a.input (eq/neq) b.input ==> a == b + if inputs_equal: + condition = z3.And( + condition, + z3.Or( + z3.Not((a_nest.input_ == b_nest.input_).raw), + (a_nest.raw == b_nest.raw), + ), + z3.Or( + z3.Not((a_nest.raw == b_nest.raw)), + (a_nest.input_ == b_nest.input_).raw, + ), + ) + else: + condition = z3.And( + condition, + z3.Or( + z3.Not((a_nest.input_ != b_nest.input_).raw), + (a_nest.raw == b_nest.raw), + ), + z3.Or( + z3.Not((a_nest.raw == b_nest.raw)), + (a_nest.input_ != b_nest.input_).raw, + ), + ) + return And( Bool(cast(z3.BoolRef, operation(a.raw, b.raw)), annotations=union), + Bool(condition) if b.nested_functions else Bool(True), a.input_ == b.input_ if inputs_equal else a.input_ != b.input_, ) - return a.input_ == b.input_ - class BitVecFunc(BitVec): """A bit vector function symbol. Used in place of functions like sha3.""" @@ -89,6 +124,7 @@ class BitVecFunc(BitVec): func_name: Optional[str], input_: "BitVec" = None, annotations: Optional[Annotations] = None, + nested_functions: Optional[List["BitVecFunc"]] = None, ): """ @@ -100,6 +136,10 @@ class BitVecFunc(BitVec): self.func_name = func_name self.input_ = input_ + self.nested_functions = nested_functions or [] + self.nested_functions = list(dict.fromkeys(self.nested_functions)) + if isinstance(input_, BitVecFunc): + self.nested_functions.extend(input_.nested_functions) super().__init__(raw, annotations) def __add__(self, other: Union[int, "BitVec"]) -> "BitVecFunc": diff --git a/mythril/mythril/mythril_analyzer.py b/mythril/mythril/mythril_analyzer.py index 3bef8203..d5e87369 100644 --- a/mythril/mythril/mythril_analyzer.py +++ b/mythril/mythril/mythril_analyzer.py @@ -10,6 +10,7 @@ from mythril.support.source_support import Source from mythril.support.loader import DynLoader 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 @@ -39,6 +40,9 @@ class MythrilAnalyzer: create_timeout: Optional[int] = None, enable_iprof: bool = False, disable_dependency_pruning: bool = False, + solver_timeout: Optional[int] = None, + enable_coverage_strategy: bool = False, + custom_modules_directory: str = "", ): """ @@ -59,6 +63,11 @@ class MythrilAnalyzer: self.create_timeout = create_timeout self.enable_iprof = enable_iprof 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) def dump_statespace(self, contract: EVMContract = None) -> str: """ @@ -81,6 +90,8 @@ class MythrilAnalyzer: enable_iprof=self.enable_iprof, disable_dependency_pruning=self.disable_dependency_pruning, run_analysis_modules=False, + enable_coverage_strategy=self.enable_coverage_strategy, + custom_modules_directory=self.custom_modules_directory, ) return get_serializable_statespace(sym) @@ -116,6 +127,8 @@ class MythrilAnalyzer: enable_iprof=self.enable_iprof, disable_dependency_pruning=self.disable_dependency_pruning, run_analysis_modules=False, + enable_coverage_strategy=self.enable_coverage_strategy, + custom_modules_directory=self.custom_modules_directory, ) return generate_graph(sym, physics=enable_physics, phrackify=phrackify) @@ -153,18 +166,23 @@ class MythrilAnalyzer: compulsory_statespace=False, enable_iprof=self.enable_iprof, disable_dependency_pruning=self.disable_dependency_pruning, + enable_coverage_strategy=self.enable_coverage_strategy, + custom_modules_directory=self.custom_modules_directory, ) - - issues = fire_lasers(sym, modules) + issues = fire_lasers(sym, modules, self.custom_modules_directory) except KeyboardInterrupt: log.critical("Keyboard Interrupt") - issues = retrieve_callback_issues(modules) + issues = retrieve_callback_issues( + modules, self.custom_modules_directory + ) except Exception: log.critical( "Exception occurred, aborting analysis. Please report this issue to the Mythril GitHub page.\n" + traceback.format_exc() ) - issues = retrieve_callback_issues(modules) + issues = retrieve_callback_issues( + modules, self.custom_modules_directory + ) exceptions.append(traceback.format_exc()) for issue in issues: issue.add_code_info(contract) diff --git a/mythril/mythril/mythril_disassembler.py b/mythril/mythril/mythril_disassembler.py index bfd7e23c..e7ef1e3b 100644 --- a/mythril/mythril/mythril_disassembler.py +++ b/mythril/mythril/mythril_disassembler.py @@ -1,10 +1,10 @@ import logging import re import solc +import solcx import os from ethereum import utils -from solc.exceptions import SolcError from typing import List, Tuple, Optional from mythril.ethereum import util from mythril.ethereum.interface.rpc.client import EthJsonRpc @@ -30,11 +30,11 @@ class MythrilDisassembler: self, eth: Optional[EthJsonRpc] = None, solc_version: str = None, - solc_args: str = None, + solc_settings_json: str = None, enable_online_lookup: bool = False, ) -> None: self.solc_binary = self._init_solc_binary(solc_version) - self.solc_args = solc_args + self.solc_settings_json = solc_settings_json self.eth = eth self.enable_online_lookup = enable_online_lookup self.sigs = signatures.SignatureDB(enable_online_lookup=enable_online_lookup) @@ -63,15 +63,24 @@ class MythrilDisassembler: solc_binary = os.environ.get("SOLC") or "solc" else: solc_binary = util.solc_exists(version) - if solc_binary: + if solc_binary and solc_binary != util.solc_exists( + "default_ubuntu_version" + ): log.info("Given version is already installed") else: try: - solc.install_solc("v" + version) + if version.startswith("0.4"): + solc.install_solc("v" + version) + else: + solcx.install_solc("v" + version) solc_binary = util.solc_exists(version) if not solc_binary: - raise SolcError() - except SolcError: + raise solc.exceptions.SolcError() + except solc.exceptions.SolcError: + raise CriticalError( + "There was an error when trying to install the specified solc version" + ) + except solcx.exceptions.SolcError: raise CriticalError( "There was an error when trying to install the specified solc version" ) @@ -163,13 +172,15 @@ class MythrilDisassembler: try: # import signatures from solidity source self.sigs.import_solidity_file( - file, solc_binary=self.solc_binary, solc_args=self.solc_args + file, + solc_binary=self.solc_binary, + solc_settings_json=self.solc_settings_json, ) if contract_name is not None: contract = SolidityContract( input_file=file, name=contract_name, - solc_args=self.solc_args, + solc_settings_json=self.solc_settings_json, solc_binary=self.solc_binary, ) self.contracts.append(contract) @@ -177,7 +188,7 @@ class MythrilDisassembler: else: for contract in get_contracts_from_file( input_file=file, - solc_args=self.solc_args, + solc_settings_json=self.solc_settings_json, solc_binary=self.solc_binary, ): self.contracts.append(contract) diff --git a/mythril/mythx/__init__.py b/mythril/mythx/__init__.py new file mode 100644 index 00000000..f1ebede0 --- /dev/null +++ b/mythril/mythx/__init__.py @@ -0,0 +1,111 @@ +import sys + +import os +import time + +from mythx_models.exceptions import MythXAPIError +from typing import List, Dict, Any + +from mythril.analysis.report import Issue, Report +from mythril.solidity.soliditycontract import SolidityContract + +from pythx import Client + +import logging + +log = logging.getLogger(__name__) + +TRIAL_ETH_ADDRESS = "0x0000000000000000000000000000000000000000" +TRIAL_PASSWORD = "trial" + + +def analyze(contracts: List[SolidityContract], analysis_mode: str = "quick") -> Report: + """ + Analyze contracts via the MythX API. + + :param contracts: List of solidity contracts to analyze + :param analysis_mode: The mode to submit the analysis request with. "quick" or "full" (default: "quick") + :return: Report with analyzed contracts + """ + assert analysis_mode in ("quick", "full"), "analysis_mode must be 'quick' or 'full'" + + c = Client( + eth_address=os.environ.get("MYTHX_ETH_ADDRESS", TRIAL_ETH_ADDRESS), + password=os.environ.get("MYTHX_PASSWORD", TRIAL_PASSWORD), + ) + + if c.eth_address == TRIAL_ETH_ADDRESS: + print( + "You are currently running MythX in Trial mode. This mode reports only a partial analysis of your smart contracts, limited to three vulnerabilities. To get a more complete analysis, sign up for a free account at https://mythx.io." + ) + + issues = [] # type: List[Issue] + + # TODO: Analyze multiple contracts asynchronously. + for contract in contracts: + source_codes = {} + source_list = [] + sources = {} # type: Dict[str, Any] + main_source = None + + try: + main_source = contract.input_file + for solidity_file in contract.solidity_files: + source_codes[solidity_file.filename] = solidity_file.data + for filename in contract.solc_json["sources"].keys(): + sources[filename] = {} + if source_codes[filename]: + sources[filename]["source"] = source_codes[filename] + sources[filename]["ast"] = contract.solc_json["sources"][filename][ + "ast" + ] + + source_list.append(filename) + + source_list.sort( + key=lambda fname: contract.solc_json["sources"][fname]["id"] + ) + except AttributeError: + # No solidity file + pass + + assert contract.creation_code, "Creation bytecode must exist." + try: + resp = c.analyze( + contract_name=contract.name, + analysis_mode=analysis_mode, + bytecode=contract.creation_code or None, + deployed_bytecode=contract.code or None, + sources=sources or None, + main_source=main_source, + source_list=source_list or None, + ) + except MythXAPIError as e: + log.critical(e) + + while not c.analysis_ready(resp.uuid): + log.info(c.status(resp.uuid).analysis) + time.sleep(5) + + for issue in c.report(resp.uuid): + issue = Issue( + contract=contract.name, + function_name=None, + address=issue.locations[0].source_map.components[0].offset + if issue.locations + else -1, + swc_id=issue.swc_id[4:] or "None", # remove 'SWC-' prefix + title=issue.swc_title, + bytecode=contract.creation_code, + severity=issue.severity.capitalize(), + description_head=issue.description_short, + description_tail=issue.description_long, + ) + issue.add_code_info(contract) + issues.append(issue) + + report = Report(contracts=contracts) + for issue in issues: + report.append_issue(issue) + + return report diff --git a/mythril/solidity/soliditycontract.py b/mythril/solidity/soliditycontract.py index f8594701..772141c8 100644 --- a/mythril/solidity/soliditycontract.py +++ b/mythril/solidity/soliditycontract.py @@ -44,23 +44,28 @@ class SourceCodeInfo: self.solc_mapping = mapping -def get_contracts_from_file(input_file, solc_args=None, solc_binary="solc"): +def get_contracts_from_file(input_file, solc_settings_json=None, solc_binary="solc"): """ :param input_file: - :param solc_args: + :param solc_settings_json: :param solc_binary: """ - data = get_solc_json(input_file, solc_args=solc_args, solc_binary=solc_binary) + data = get_solc_json( + input_file, solc_settings_json=solc_settings_json, solc_binary=solc_binary + ) try: - for key, contract in data["contracts"].items(): - filename, name = key.split(":") - if filename == input_file and len(contract["bin-runtime"]): + for contract_name in data["contracts"][input_file].keys(): + if len( + data["contracts"][input_file][contract_name]["evm"]["deployedBytecode"][ + "object" + ] + ): yield SolidityContract( input_file=input_file, - name=name, - solc_args=solc_args, + name=contract_name, + solc_settings_json=solc_settings_json, solc_binary=solc_binary, ) except KeyError: @@ -70,16 +75,22 @@ def get_contracts_from_file(input_file, solc_args=None, solc_binary="solc"): class SolidityContract(EVMContract): """Representation of a Solidity contract.""" - def __init__(self, input_file, name=None, solc_args=None, solc_binary="solc"): - data = get_solc_json(input_file, solc_args=solc_args, solc_binary=solc_binary) + def __init__( + self, input_file, name=None, solc_settings_json=None, solc_binary="solc" + ): + data = get_solc_json( + input_file, solc_settings_json=solc_settings_json, solc_binary=solc_binary + ) self.solidity_files = [] + self.solc_json = data + self.input_file = input_file - for filename in data["sourceList"]: + for filename, contract in data["sources"].items(): with open(filename, "r", encoding="utf-8") as file: code = file.read() full_contract_src_maps = self.get_full_contract_src_maps( - data["sources"][filename]["AST"] + contract["ast"] ) self.solidity_files.append( SolidityFile(filename, code, full_contract_src_maps) @@ -91,32 +102,28 @@ class SolidityContract(EVMContract): srcmap_constructor = [] srcmap = [] if name: - for key, contract in sorted(data["contracts"].items()): - filename, _name = key.split(":") - - if ( - filename == input_file - and name == _name - and len(contract["bin-runtime"]) - ): - code = contract["bin-runtime"] - creation_code = contract["bin"] - srcmap = contract["srcmap-runtime"].split(";") - srcmap_constructor = contract["srcmap"].split(";") - has_contract = True - break + contract = data["contracts"][input_file][name] + if len(contract["evm"]["deployedBytecode"]["object"]): + code = contract["evm"]["deployedBytecode"]["object"] + creation_code = contract["evm"]["bytecode"]["object"] + srcmap = contract["evm"]["deployedBytecode"]["sourceMap"].split(";") + srcmap_constructor = contract["evm"]["bytecode"]["sourceMap"].split(";") + has_contract = True # If no contract name is specified, get the last bytecode entry for the input file else: - for key, contract in sorted(data["contracts"].items()): - filename, name = key.split(":") - - if filename == input_file and len(contract["bin-runtime"]): - code = contract["bin-runtime"] - creation_code = contract["bin"] - srcmap = contract["srcmap-runtime"].split(";") - srcmap_constructor = contract["srcmap"].split(";") + for contract_name, contract in sorted( + data["contracts"][input_file].items() + ): + if len(contract["evm"]["deployedBytecode"]["object"]): + name = contract_name + code = contract["evm"]["deployedBytecode"]["object"] + creation_code = contract["evm"]["bytecode"]["object"] + srcmap = contract["evm"]["deployedBytecode"]["sourceMap"].split(";") + srcmap_constructor = contract["evm"]["bytecode"]["sourceMap"].split( + ";" + ) has_contract = True if not has_contract: @@ -139,8 +146,8 @@ class SolidityContract(EVMContract): :return: The source maps """ source_maps = set() - for child in ast["children"]: - if "contractKind" in child["attributes"]: + for child in ast["nodes"]: + if child.get("contractKind"): source_maps.add(child["src"]) return source_maps diff --git a/mythril/support/loader.py b/mythril/support/loader.py index f46feff5..2da25d7b 100644 --- a/mythril/support/loader.py +++ b/mythril/support/loader.py @@ -3,6 +3,11 @@ and dependencies.""" from mythril.disassembler.disassembly import Disassembly import logging import re +import functools +from mythril.ethereum.interface.rpc.client import EthJsonRpc +from typing import Optional + +LRU_CACHE_SIZE = 4096 log = logging.getLogger(__name__) @@ -10,7 +15,9 @@ log = logging.getLogger(__name__) class DynLoader: """The dynamic loader class.""" - def __init__(self, eth, contract_loading=True, storage_loading=True): + def __init__( + self, eth: Optional[EthJsonRpc], contract_loading=True, storage_loading=True + ): """ :param eth: @@ -18,11 +25,11 @@ class DynLoader: :param storage_loading: """ self.eth = eth - self.storage_cache = {} self.contract_loading = contract_loading self.storage_loading = storage_loading - def read_storage(self, contract_address: str, index: int): + @functools.lru_cache(LRU_CACHE_SIZE) + def read_storage(self, contract_address: str, index: int) -> str: """ :param contract_address: @@ -30,43 +37,28 @@ class DynLoader: :return: """ if not self.storage_loading: - raise Exception( + raise ValueError( "Cannot load from the storage when the storage_loading flag is false" ) + if not self.eth: + raise ValueError("Cannot load from the storage when eth is None") - try: - contract_ref = self.storage_cache[contract_address] - data = contract_ref[index] - - except KeyError: - - self.storage_cache[contract_address] = {} - - data = self.eth.eth_getStorageAt( - contract_address, position=index, block="latest" - ) - - self.storage_cache[contract_address][index] = data - - except IndexError: - - data = self.eth.eth_getStorageAt( - contract_address, position=index, block="latest" - ) - - self.storage_cache[contract_address][index] = data - - return data + return self.eth.eth_getStorageAt( + contract_address, position=index, block="latest" + ) - def dynld(self, dependency_address): + @functools.lru_cache(LRU_CACHE_SIZE) + def dynld(self, dependency_address: str) -> Optional[Disassembly]: """ :param dependency_address: :return: """ if not self.contract_loading: raise ValueError("Cannot load contract when contract_loading flag is false") + if not self.eth: + raise ValueError("Cannot load from the storage when eth is None") - log.debug("Dynld at contract " + dependency_address) + log.debug("Dynld at contract %s", dependency_address) # Ensure that dependency_address is the correct length, with 0s prepended as needed. dependency_address = ( @@ -81,7 +73,7 @@ class DynLoader: else: return None - log.debug("Dependency address: " + dependency_address) + log.debug("Dependency address: %s", dependency_address) code = self.eth.eth_getCode(dependency_address) diff --git a/mythril/support/signatures.py b/mythril/support/signatures.py index e0deb9ea..67a1bf1d 100644 --- a/mythril/support/signatures.py +++ b/mythril/support/signatures.py @@ -1,5 +1,6 @@ """The Mythril function signature database.""" import functools +import json import logging import multiprocessing import os @@ -9,6 +10,7 @@ from collections import defaultdict from subprocess import PIPE, Popen from typing import List, Set, DefaultDict, Dict +from mythril.ethereum.util import get_solc_json from mythril.exceptions import CompilerError log = logging.getLogger(__name__) @@ -231,53 +233,20 @@ class SignatureDB(object, metaclass=Singleton): return [] def import_solidity_file( - self, file_path: str, solc_binary: str = "solc", solc_args: str = None + self, file_path: str, solc_binary: str = "solc", solc_settings_json: str = None ): """Import Function Signatures from solidity source files. :param solc_binary: - :param solc_args: + :param solc_settings_json: :param file_path: solidity source code file path :return: """ - cmd = [solc_binary, "--hashes", file_path] - if solc_args: - cmd.extend(solc_args.split()) + solc_json = get_solc_json(file_path, solc_binary, solc_settings_json) - try: - p = Popen(cmd, stdout=PIPE, stderr=PIPE) - stdout, stderr = p.communicate() - ret = p.returncode - - if ret != 0: - raise CompilerError( - "Solc has experienced a fatal error (code {}).\n\n{}".format( - ret, stderr.decode("utf-8") - ) - ) - except FileNotFoundError: - raise CompilerError( - ( - "Compiler not found. Make sure that solc is installed and in PATH, " - "or the SOLC environment variable is set." - ) - ) - - stdout = stdout.decode("unicode_escape").split("\n") - for line in stdout: - # the ':' need not be checked but just to be sure - if all(map(lambda x: x in line, ["(", ")", ":"])): - solc_bytes = "0x" + line.split(":")[0] - solc_text = line.split(":")[1].strip() - self.solidity_sigs[solc_bytes].append(solc_text) - log.debug( - "Signatures: found %d signatures after parsing" % len(self.solidity_sigs) - ) - - # update DB with what we've found - for byte_sig, text_sigs in self.solidity_sigs.items(): - for text_sig in text_sigs: - self.add(byte_sig, text_sig) + for contract in solc_json["contracts"][file_path].values(): + for name, hash in contract["evm"]["methodIdentifiers"].items(): + self.add("0x" + hash, name) @staticmethod def lookup_online(byte_sig: str, timeout: int, proxies=None) -> List[str]: diff --git a/requirements.txt b/requirements.txt index 1b49350c..13b69082 100644 --- a/requirements.txt +++ b/requirements.txt @@ -1,7 +1,7 @@ coloredlogs>=10.0 configparser>=3.5.0 coverage -py_ecc==1.4.2 +py_ecc==1.6.0 eth_abi==1.3.0 eth-account>=0.1.0a2,<=0.3.0 ethereum>=2.3.2 @@ -12,19 +12,21 @@ eth-keys>=0.2.0b3,<0.3.0 eth-rlp>=0.1.0 eth-tester==0.1.0b32 eth-typing>=2.0.0 -eth-utils>=1.0.1 jinja2>=2.9 mock persistent>=4.2.0 plyvel py-flags +py-solc-x==0.6.0 py-solc pytest>=3.6.0 pytest-cov pytest_mock -requests +requests>=2.22.0 rlp>=1.0.1 +semantic_version==2.8.1 transaction>=2.2.1 z3-solver>=4.8.5.0 pysha3 matplotlib +pythx diff --git a/setup.py b/setup.py index d76f546e..5955ab26 100755 --- a/setup.py +++ b/setup.py @@ -25,14 +25,15 @@ REQUIRES_PYTHON = ">=3.5.0" # What packages are required for this module to be executed? REQUIRED = [ "coloredlogs>=10.0", - "py_ecc==1.4.2", + "py_ecc==1.6.0", "ethereum>=2.3.2", "z3-solver>=4.8.5.0", - "requests", + "requests>=2.22.0", "py-solc", + "py-solc-x==0.6.0", + "semantic_version==2.8.1", "plyvel", "eth_abi==1.3.0", - "eth-utils>=1.0.1", "eth-account>=0.1.0a2,<=0.3.0", "eth-hash>=0.1.0", "eth-keyfile>=0.5.1", @@ -50,6 +51,7 @@ REQUIRED = [ "persistent>=4.2.0", "ethereum-input-decoder>=0.2.2", "matplotlib", + "pythx", ] TESTS_REQUIRE = ["mypy", "pytest>=3.6.0", "pytest_mock", "pytest-cov"] diff --git a/tests/disassembler_test.py b/tests/disassembler_test.py index d3955d82..ffdc5f08 100644 --- a/tests/disassembler_test.py +++ b/tests/disassembler_test.py @@ -3,12 +3,6 @@ from mythril.ethereum import util from tests import * -def _compile_to_code(input_file): - compiled = util.get_solc_json(str(input_file)) - code = list(compiled["contracts"].values())[0]["bin-runtime"] - return code - - class DisassemblerTestCase(BaseTestCase): def test_instruction_list(self): code = "0x606060405236156100ca5763ffffffff60e060020a600035041663054f7d9c81146100d3578063095c21e3146100f45780630ba50baa146101165780631a3719321461012857806366529e3f14610153578063682789a81461017257806389f21efc146101915780638da5cb5b146101ac5780638f4ffcb1146101d55780639a1f2a5714610240578063b5f522f71461025b578063bd94b005146102b6578063c5ab5a13146102c8578063cc424839146102f1578063deb077b914610303578063f3fef3a314610322575b6100d15b5b565b005b34610000576100e0610340565b604080519115158252519081900360200190f35b3461000057610104600435610361565b60408051918252519081900360200190f35b34610000576100d1600435610382565b005b3461000057610104600160a060020a03600435166103b0565b60408051918252519081900360200190f35b346100005761010461041e565b60408051918252519081900360200190f35b3461000057610104610424565b60408051918252519081900360200190f35b34610000576100d1600160a060020a036004351661042b565b005b34610000576101b961046f565b60408051600160a060020a039092168252519081900360200190f35b3461000057604080516020600460643581810135601f81018490048402850184019095528484526100d1948235600160a060020a039081169560248035966044359093169594608494929391019190819084018382808284375094965061048595505050505050565b005b34610000576100d1600160a060020a03600435166106e7565b005b346100005761026b60043561072b565b60408051600160a060020a0390991689526020890197909752878701959095526060870193909352608086019190915260a085015260c084015260e083015251908190036101000190f35b34610000576100d160043561077a565b005b34610000576101b9610830565b60408051600160a060020a039092168252519081900360200190f35b34610000576100d160043561083f565b005b34610000576101046108a1565b60408051918252519081900360200190f35b34610000576100d1600160a060020a03600435166024356108a7565b005b60015474010000000000000000000000000000000000000000900460ff1681565b600681815481101561000057906000526020600020900160005b5054905081565b600054600160a060020a036301000000909104811690331681146103a557610000565b60038290555b5b5050565b6005546040805160006020918201819052825160e260020a631d010437028152600160a060020a03868116600483015293519194939093169263740410dc92602480830193919282900301818787803b156100005760325a03f115610000575050604051519150505b919050565b60035481565b6006545b90565b600054600160a060020a0363010000009091048116903316811461044e57610000565b60018054600160a060020a031916600160a060020a0384161790555b5b5050565b60005463010000009004600160a060020a031681565b6000600060006000600060006000600160149054906101000a900460ff16156104ad57610000565b87600081518110156100005760209101015160005460f860020a918290048202975002600160f860020a031990811690871614156105405760009450600196505b600587101561053057878781518110156100005790602001015160f860020a900460f860020a0260f860020a900485610100020194505b6001909601956104ee565b61053b8b868c610955565b6106d6565b600054610100900460f860020a02600160f860020a0319908116908716141561069e57506001955060009250829150819050805b60058710156105b657878781518110156100005790602001015160f860020a900460f860020a0260f860020a900481610100020190505b600190960195610574565b600596505b60098710156105fd57878781518110156100005790602001015160f860020a900460f860020a0260f860020a900484610100020193505b6001909601956105bb565b600996505b600d87101561064457878781518110156100005790602001015160f860020a900460f860020a0260f860020a900483610100020192505b600190960195610602565b600d96505b601187101561068b57878781518110156100005790602001015160f860020a900460f860020a0260f860020a900482610100020191505b600190960195610649565b61053b8b828c878787610bc4565b6106d6565b60005462010000900460f860020a02600160f860020a031990811690871614156106d15761053b8b8b610e8e565b6106d6565b610000565b5b5b5b5b5050505050505050505050565b600054600160a060020a0363010000009091048116903316811461070a57610000565b60058054600160a060020a031916600160a060020a0384161790555b5b5050565b600760208190526000918252604090912080546001820154600283015460038401546004850154600586015460068701549690970154600160a060020a03909516969395929491939092909188565b600081815260076020526040812054600160a060020a0390811690331681146107a257610000565b600083815260076020526040902080546004820154600583015460038401549395506107dc93600160a060020a039093169291029061105e565b50600060058301556107ed83611151565b6040805184815290517fb5dc9baf0cb4e7e4759fa12eadebddf9316e26147d5a9ae150c4228d5a1dd23f9181900360200190a161082933611244565b5b5b505050565b600154600160a060020a031681565b600054600160a060020a0363010000009091048116903316811461086257610000565b600080546040516301000000909104600160a060020a0316916108fc851502918591818181858888f1935050505015156103ab57610000565b5b5b5050565b60025481565b600054600160a060020a036301000000909104811690331681146108ca57610000565b6000805460408051602090810184905281517fa9059cbb0000000000000000000000000000000000000000000000000000000081526301000000909304600160a060020a0390811660048501526024840187905291519187169363a9059cbb9360448082019492918390030190829087803b156100005760325a03f115610000575050505b5b505050565b610100604051908101604052806000600160a060020a03168152602001600081526020016000815260200160008152602001600081526020016000815260200160008152602001600081525060006007600085815260200190815260200160002061010060405190810160405290816000820160009054906101000a9004600160a060020a0316600160a060020a0316600160a060020a0316815260200160018201548152602001600282015481526020016003820154815260200160048201548152602001600582015481526020016006820154815260200160078201548152505091508260001415610a4857610000565b8160400151838115610000570615610a5f57610000565b6002548410610a6d57610000565b8160400151838115610000570490508160a00151811115610a8d57610000565b610a9c8584846020015161128e565b1515610aa757610000565b60a082018051829003815260008581526007602081815260409283902086518154600160a060020a031916600160a060020a038216178255918701516001820181905593870151600282015560608701516003820155608087015160048201559351600585015560c0860151600685015560e08601519390910192909255610b319190859061105e565b1515610b3c57610000565b610b518582846080015102846060015161105e565b1515610b5c57610000565b60a0820151158015610b71575060c082015115155b15610b7f57610b7f84611151565b5b6040805185815290517fb5dc9baf0cb4e7e4759fa12eadebddf9316e26147d5a9ae150c4228d5a1dd23f9181900360200190a1610bbc85611244565b5b5050505050565b831515610bd057610000565b82851415610bdd57610000565b801580610be8575081155b15610bf257610000565b80848115610000570615610c0557610000565b6005546040805160006020918201819052825160e260020a631d010437028152600160a060020a038b8116600483015293518695949094169363740410dc9360248084019491938390030190829087803b156100005760325a03f11561000057505050604051805190501015610c7a57610000565b610c8586858761128e565b1515610c9057610000565b600554604080517fbe0140a6000000000000000000000000000000000000000000000000000000008152600160a060020a03898116600483015260006024830181905260448301869052925193169263be0140a69260648084019391929182900301818387803b156100005760325a03f115610000575050506101006040519081016040528087600160a060020a03168152602001848152602001838152602001868152602001828681156100005704815260200182815260200160068054905081526020014281525060076000600254815260200190815260200160002060008201518160000160006101000a815481600160a060020a030219169083600160a060020a031602179055506020820151816001015560408201518160020155606082015181600301556080820151816004015560a0820151816005015560c0820151816006015560e0820151816007015590505060068054806001018281815481835581811511610e2757600083815260209020610e279181019083015b80821115610e235760008155600101610e0f565b5090565b5b505050916000526020600020900160005b50600280549182905560018201905560408051918252517fb5dc9baf0cb4e7e4759fa12eadebddf9316e26147d5a9ae150c4228d5a1dd23f92509081900360200190a1610e8586611244565b5b505050505050565b600354818115610000570615610ea357610000565b600160009054906101000a9004600160a060020a0316600160a060020a031663cf35bdd060016000604051602001526040518263ffffffff1660e060020a02815260040180828152602001915050602060405180830381600087803b156100005760325a03f115610000575050604080518051600080546020938401829052845160e060020a6323b872dd028152600160a060020a038981166004830152630100000090920482166024820152604481018890529451921694506323b872dd936064808201949392918390030190829087803b156100005760325a03f1156100005750506040515115159050610f9857610000565b600554600354600160a060020a039091169063be0140a6908490600190858115610000576040805160e060020a63ffffffff8816028152600160a060020a039095166004860152921515602485015204604483015251606480830192600092919082900301818387803b156100005760325a03f1156100005750505061101d82611244565b60408051600160a060020a038416815290517f30a29a0aa75376a69254bb98dbd11db423b7e8c3473fb5bf0fcba60bcbc42c4b9181900360200190a15b5050565b600081151561106c57610000565b6001546040805160006020918201819052825160e460020a630cf35bdd028152600481018790529251600160a060020a039094169363cf35bdd09360248082019493918390030190829087803b156100005760325a03f1156100005750505060405180519050600160a060020a031663a9059cbb85856000604051602001526040518363ffffffff1660e060020a0281526004018083600160a060020a0316600160a060020a0316815260200182815260200192505050602060405180830381600087803b156100005760325a03f115610000575050604051519150505b9392505050565b6000818152600760205260409020600690810154815490919060001981019081101561000057906000526020600020900160005b5054600682815481101561000057906000526020600020900160005b50556006805460001981018083559091908280158290116111e7576000838152602090206111e79181019083015b80821115610e235760008155600101610e0f565b5090565b5b50506006548314915061122d9050578060076000600684815481101561000057906000526020600020900160005b505481526020810191909152604001600020600601555b6000828152600760205260408120600601555b5050565b60045481600160a060020a031631101561128957600454604051600160a060020a0383169180156108fc02916000818181858888f19350505050151561128957610000565b5b5b50565b600081151561129c57610000565b6001546040805160006020918201819052825160e460020a630cf35bdd028152600481018790529251600160a060020a039094169363cf35bdd09360248082019493918390030190829087803b156100005760325a03f11561000057505060408051805160006020928301819052835160e060020a6323b872dd028152600160a060020a038a811660048301523081166024830152604482018a905294519490921694506323b872dd93606480840194939192918390030190829087803b156100005760325a03f115610000575050604051519150505b93925050505600a165627a7a723058204dee0e1bf170a9d122508f3e876c4a84893b12a7345591521af4ca737bb765000029" diff --git a/tests/instructions/create_test.py b/tests/instructions/create_test.py new file mode 100644 index 00000000..0a97565e --- /dev/null +++ b/tests/instructions/create_test.py @@ -0,0 +1,72 @@ +from mythril.disassembler.disassembly import Disassembly +from mythril.laser.ethereum.state.environment import Environment +from mythril.laser.ethereum.state.account import Account +from mythril.laser.ethereum.state.machine_state import MachineState +from mythril.laser.ethereum.state.global_state import GlobalState +from mythril.laser.ethereum.state.world_state import WorldState +from mythril.laser.ethereum.instructions import Instruction +from mythril.laser.ethereum.transaction.transaction_models import MessageCallTransaction +from mythril.laser.ethereum.state.calldata import ConcreteCalldata +from mythril.laser.ethereum.svm import LaserEVM +from mythril.laser.smt import symbol_factory + +# contract A { +# uint256 public val = 10; +# } +contract_init_code = "6080604052600a600055348015601457600080fd5b506084806100236000396000f3fe6080604052348015600f57600080fd5b506004361060285760003560e01c80633c6bb43614602d575b600080fd5b60336049565b6040518082815260200191505060405180910390f35b6000548156fea265627a7a72315820d3cfe7a909450a953cbd7e47d8c17477f2609baa5208d043e965efec69d1ed9864736f6c634300050b0032" +contract_runtime_code = "6080604052348015600f57600080fd5b506004361060285760003560e01c80633c6bb43614602d575b600080fd5b60336049565b6040518082815260200191505060405180910390f35b6000548156fea265627a7a72315820d3cfe7a909450a953cbd7e47d8c17477f2609baa5208d043e965efec69d1ed9864736f6c634300050b0032" + +last_state = None +created_contract_account = None + + +def execute_create(): + global last_state + global created_contract_account + if not last_state and not created_contract_account: + code_raw = [] + for i in range(len(contract_init_code) // 2): + code_raw.append(int(contract_init_code[2 * i : 2 * (i + 1)], 16)) + calldata = ConcreteCalldata(0, code_raw) + + world_state = WorldState() + account = world_state.create_account(balance=1000000, address=101) + account.code = Disassembly("60a760006000f000") + environment = Environment(account, None, calldata, None, None, None) + og_state = GlobalState( + world_state, environment, None, MachineState(gas_limit=8000000) + ) + og_state.transaction_stack.append( + (MessageCallTransaction(world_state=WorldState(), gas_limit=8000000), None) + ) + + laser = LaserEVM() + states = [og_state] + last_state = og_state + for state in states: + new_states, op_code = laser.execute_state(state) + last_state = state + if op_code == "STOP": + break + states.extend(new_states) + + created_contract_address = last_state.mstate.stack[-1].value + created_contract_account = last_state.world_state.accounts[ + created_contract_address + ] + + return last_state, created_contract_account + + +def test_create_has_code(): + last_state, created_contract_account = execute_create() + assert created_contract_account.code.bytecode == contract_runtime_code + + +def test_create_has_storage(): + last_state, created_contract_account = execute_create() + storage = created_contract_account.storage + # From contract, val = 10. + assert storage[symbol_factory.BitVecVal(0, 256)] == symbol_factory.BitVecVal( + 10, 256 + ) diff --git a/tests/instructions/extcodehash_test.py b/tests/instructions/extcodehash_test.py new file mode 100644 index 00000000..14f2ad65 --- /dev/null +++ b/tests/instructions/extcodehash_test.py @@ -0,0 +1,48 @@ +from mythril.disassembler.disassembly import Disassembly +from mythril.laser.ethereum.state.environment import Environment +from mythril.laser.ethereum.state.account import Account +from mythril.laser.ethereum.state.machine_state import MachineState +from mythril.laser.ethereum.state.global_state import GlobalState +from mythril.laser.ethereum.state.world_state import WorldState +from mythril.laser.ethereum.instructions import Instruction +from mythril.laser.ethereum.transaction.transaction_models import MessageCallTransaction + +from mythril.support.support_utils import get_code_hash + +from mythril.laser.smt import symbol_factory + +# Arrange +world_state = WorldState() +account = world_state.create_account(balance=10, address=101) +account.code = Disassembly("60606040") +world_state.create_account(balance=10, address=1000) +environment = Environment(account, None, None, None, None, None) +og_state = GlobalState(world_state, environment, None, MachineState(gas_limit=8000000)) +og_state.transaction_stack.append( + (MessageCallTransaction(world_state=WorldState(), gas_limit=8000000), None) +) + +instruction = Instruction("extcodehash", dynamic_loader=None) + + +def test_extcodehash_no_account(): + + # If account does not exist, return 0 + og_state.mstate.stack = [symbol_factory.BitVecVal(1, 256)] + new_state = instruction.evaluate(og_state)[0] + assert new_state.mstate.stack[-1] == 0 + + +def test_extcodehash_no_code(): + + # If account code does not exist, return hash of empty set. + og_state.mstate.stack = [symbol_factory.BitVecVal(1000, 256)] + new_state = instruction.evaluate(og_state)[0] + assert hex(new_state.mstate.stack[-1].value) == get_code_hash("") + + +def test_extcodehash_return_hash(): + # If account code exists, return hash of the code. + og_state.mstate.stack = [symbol_factory.BitVecVal(101, 256)] + new_state = instruction.evaluate(og_state)[0] + assert hex(new_state.mstate.stack[-1].value) == get_code_hash("60606040") diff --git a/tests/instructions/static_call_test.py b/tests/instructions/static_call_test.py new file mode 100644 index 00000000..b9bcc26c --- /dev/null +++ b/tests/instructions/static_call_test.py @@ -0,0 +1,124 @@ +import pytest +from mock import patch + +from mythril.disassembler.disassembly import Disassembly +from mythril.laser.smt import symbol_factory +from mythril.laser.ethereum.state.environment import Environment +from mythril.laser.ethereum.state.account import Account +from mythril.laser.ethereum.state.machine_state import MachineState +from mythril.laser.ethereum.state.global_state import GlobalState +from mythril.laser.ethereum.state.world_state import WorldState +from mythril.laser.ethereum.instructions import Instruction +from mythril.laser.ethereum.transaction.transaction_models import MessageCallTransaction +from mythril.laser.ethereum.call import SymbolicCalldata +from mythril.laser.ethereum.transaction import TransactionStartSignal + +from mythril.laser.ethereum.evm_exceptions import WriteProtection + + +def get_global_state(): + active_account = Account("0x0", code=Disassembly("60606040")) + environment = Environment( + active_account, None, SymbolicCalldata("2"), None, None, None + ) + world_state = WorldState() + world_state.put_account(active_account) + state = GlobalState(world_state, environment, None, MachineState(gas_limit=8000000)) + state.transaction_stack.append( + (MessageCallTransaction(world_state=world_state, gas_limit=8000000), None) + ) + return state + + +@patch( + "mythril.laser.ethereum.instructions.get_call_parameters", + return_value=( + "0", + Account(code=Disassembly(code="0x00"), address="0x19"), + 0, + 0, + 0, + 0, + 0, + ), +) +def test_staticcall(f1): + # Arrange + state = get_global_state() + state.mstate.stack = [10, 10, 10, 10, 10, 10, 10, 10, 0] + instruction = Instruction("staticcall", dynamic_loader=None) + + # Act and Assert + with pytest.raises(TransactionStartSignal) as ts: + instruction.evaluate(state) + assert ts.value.transaction.static + assert ts.value.transaction.initial_global_state().environment.static + + +test_data = ( + "suicide", + "create", + "create2", + "log0", + "log1", + "log2", + "log3", + "log4", + "sstore", +) + + +@pytest.mark.parametrize("input", test_data) +def test_staticness(input): + # Arrange + state = get_global_state() + state.environment.static = True + state.mstate.stack = [] + instruction = Instruction(input, dynamic_loader=None) + + # Act and Assert + with pytest.raises(WriteProtection): + instruction.evaluate(state) + + +test_data_call = ((0, True), (100, False)) + + +@pytest.mark.parametrize("input, success", test_data_call) +@patch("mythril.laser.ethereum.instructions.get_call_parameters") +def test_staticness_call_concrete(f1, input, success): + # Arrange + state = get_global_state() + state.environment.static = True + state.mstate.stack = [] + code = Disassembly(code="616263") + f1.return_value = ("0", Account(code=code, address="0x19"), 0, input, 0, 0, 0) + instruction = Instruction("call", dynamic_loader=None) + + # Act and Assert + if success: + with pytest.raises(TransactionStartSignal) as ts: + instruction.evaluate(state) + assert ts.value.transaction.static + else: + with pytest.raises(WriteProtection): + instruction.evaluate(state) + + +@patch("mythril.laser.ethereum.instructions.get_call_parameters") +def test_staticness_call_symbolic(f1): + # Arrange + state = get_global_state() + state.environment.static = True + state.mstate.stack = [] + call_value = symbol_factory.BitVecSym("x", 256) + code = Disassembly(code="616263") + f1.return_value = ("0", Account(code=code, address="0x19"), 0, call_value, 0, 0, 0) + instruction = Instruction("call", dynamic_loader=None) + + # Act and Assert + with pytest.raises(TransactionStartSignal) as ts: + instruction.evaluate(state) + + assert ts.value.transaction.static + assert ts.value.global_state.mstate.constraints[-1] == (call_value == 0) diff --git a/tests/laser/Precompiles/test_ec_add.py b/tests/laser/Precompiles/test_ec_add.py new file mode 100644 index 00000000..4ede2cf0 --- /dev/null +++ b/tests/laser/Precompiles/test_ec_add.py @@ -0,0 +1,27 @@ +from mock import patch +from eth_utils import decode_hex +from mythril.laser.ethereum.natives import ec_add +from py_ecc.optimized_bn128 import FQ + +VECTOR_A = decode_hex( + "0000000000000000000000000000000000000000000000000000000000000001" + "0000000000000000000000000000000000000000000000000000000000000020" + "0000000000000000000000000000000000000000000000000000000000000020" + "03" + "fffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2e" + "fffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2f" +) + + +def test_ec_add_sanity(): + assert ec_add(VECTOR_A) == [] + + +@patch("mythril.laser.ethereum.natives.validate_point", return_value=1) +@patch("mythril.laser.ethereum.natives.bn128.add", return_value=1) +@patch("mythril.laser.ethereum.natives.bn128.normalize") +def test_ec_add(f1, f2, f3): + FQ.fielf_modulus = 128 + a = FQ(val=1) + f1.return_value = (a, a) + assert ec_add(VECTOR_A) == ([0] * 31 + [1]) * 2 diff --git a/tests/laser/Precompiles/test_elliptic_curves.py b/tests/laser/Precompiles/test_elliptic_curves.py new file mode 100644 index 00000000..28908f58 --- /dev/null +++ b/tests/laser/Precompiles/test_elliptic_curves.py @@ -0,0 +1,35 @@ +from mock import patch +from mythril.laser.ethereum.natives import ec_pair +from py_ecc.optimized_bn128 import FQ + + +def test_ec_pair_192_check(): + vec_c = [0] * 100 + assert ec_pair(vec_c) == [] + + +@patch("mythril.laser.ethereum.natives.validate_point", return_value=1) +@patch("mythril.laser.ethereum.natives.bn128.is_on_curve", return_value=True) +@patch("mythril.laser.ethereum.natives.bn128.pairing", return_value=1) +@patch("mythril.laser.ethereum.natives.bn128.normalize") +def test_ec_pair(f1, f2, f3, f4): + FQ.fielf_modulus = 100 + a = FQ(val=1) + f1.return_value = (a, a) + vec_c = [0] * 192 + assert ec_pair(vec_c) == [0] * 31 + [1] + + +@patch("mythril.laser.ethereum.natives.validate_point", return_value=False) +def test_ec_pair_point_validation_failure(f1): + vec_c = [0] * 192 + assert ec_pair(vec_c) == [] + + +@patch("mythril.laser.ethereum.natives.validate_point", return_value=1) +def test_ec_pair_field_exceed_mod(f1): + FQ.fielf_modulus = 100 + a = FQ(val=1) + f1.return_value = (a, a) + vec_c = [10] * 192 + assert ec_pair(vec_c) == [] diff --git a/tests/laser/Precompiles/test_elliptic_mul.py b/tests/laser/Precompiles/test_elliptic_mul.py new file mode 100644 index 00000000..c3b3be9d --- /dev/null +++ b/tests/laser/Precompiles/test_elliptic_mul.py @@ -0,0 +1,27 @@ +from mock import patch +from eth_utils import decode_hex +from mythril.laser.ethereum.natives import ec_mul +from py_ecc.optimized_bn128 import FQ + +VECTOR_A = decode_hex( + "0000000000000000000000000000000000000000000000000000000000000001" + "0000000000000000000000000000000000000000000000000000000000000020" + "0000000000000000000000000000000000000000000000000000000000000020" + "03" + "fffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2e" + "fffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2f" +) + + +@patch("mythril.laser.ethereum.natives.validate_point", return_value=1) +@patch("mythril.laser.ethereum.natives.bn128.multiply", return_value=1) +@patch("mythril.laser.ethereum.natives.bn128.normalize") +def test_ec_mul(f1, f2, f3): + FQ.fielf_modulus = 128 + a = FQ(val=1) + f1.return_value = (a, a) + assert ec_mul(VECTOR_A) == ([0] * 31 + [1]) * 2 + + +def test_ec_mul_validation_failure(): + assert ec_mul(VECTOR_A) == [] diff --git a/tests/laser/Precompiles/test_mod_exp.py b/tests/laser/Precompiles/test_mod_exp.py new file mode 100644 index 00000000..d050c929 --- /dev/null +++ b/tests/laser/Precompiles/test_mod_exp.py @@ -0,0 +1,61 @@ +import pytest +from eth_utils import decode_hex +from mythril.laser.ethereum.natives import mod_exp +from ethereum.utils import big_endian_to_int + + +EIP198_VECTOR_A = decode_hex( + "0000000000000000000000000000000000000000000000000000000000000001" + "0000000000000000000000000000000000000000000000000000000000000020" + "0000000000000000000000000000000000000000000000000000000000000020" + "03" + "fffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2e" + "fffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2f" +) + +EIP198_VECTOR_B = decode_hex( + "0000000000000000000000000000000000000000000000000000000000000000" + "0000000000000000000000000000000000000000000000000000000000000020" + "0000000000000000000000000000000000000000000000000000000000000020" + "fffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2e" + "fffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2f" +) + +EIP198_VECTOR_C = decode_hex( + "0000000000000000000000000000000000000000000000000000000000000001" + "0000000000000000000000000000000000000000000000000000000000000002" + "0000000000000000000000000000000000000000000000000000000000000020" + "03" + "ffff" + "8000000000000000000000000000000000000000000000000000000000000000" + "07" +) + +EIP198_VECTOR_D = decode_hex( + "0000000000000000000000000000000000000000000000000000000000000001" + "0000000000000000000000000000000000000000000000000000000000000002" + "0000000000000000000000000000000000000000000000000000000000000020" + "03" + "ffff" + "80" +) + + +@pytest.mark.parametrize( + "data,expected", + ( + (EIP198_VECTOR_A, 1), + (EIP198_VECTOR_B, 0), + ( + EIP198_VECTOR_C, + 26689440342447178617115869845918039756797228267049433585260346420242739014315, + ), + ( + EIP198_VECTOR_D, + 26689440342447178617115869845918039756797228267049433585260346420242739014315, + ), + ), +) +def test_modexp_result(data, expected): + actual = mod_exp(data) + assert big_endian_to_int(actual) == expected diff --git a/tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicide0.json b/tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicide0.json index ae80e8f6..456a7c16 100644 --- a/tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicide0.json +++ b/tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicide0.json @@ -47,7 +47,7 @@ } }, "0xcd1722f3947def4cf144679da39c4c32bdc35681" : { - "balance" : "0x17", + "balance" : "0x0186a0", "code" : "0x6000355415600957005b60203560003555", "nonce" : "0x00", "storage" : { @@ -55,4 +55,4 @@ } } } -} \ No newline at end of file +} diff --git a/tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicideNotExistingAccount.json b/tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicideNotExistingAccount.json index ecf5d3bc..b72d6bcc 100644 --- a/tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicideNotExistingAccount.json +++ b/tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicideNotExistingAccount.json @@ -54,7 +54,7 @@ } }, "0xcd1722f3947def4cf144679da39c4c32bdc35681" : { - "balance" : "0x17", + "balance" : "0x0186a0", "code" : "0x6000355415600957005b60203560003555", "nonce" : "0x00", "storage" : { @@ -62,4 +62,4 @@ } } } -} \ No newline at end of file +} diff --git a/tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicideSendEtherToMe.json b/tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicideSendEtherToMe.json index 7a8f19b8..f27557ed 100644 --- a/tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicideSendEtherToMe.json +++ b/tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicideSendEtherToMe.json @@ -47,7 +47,7 @@ } }, "0xcd1722f3947def4cf144679da39c4c32bdc35681" : { - "balance" : "0x17", + "balance" : "0x0186a0", "code" : "0x6000355415600957005b60203560003555", "nonce" : "0x00", "storage" : { @@ -55,4 +55,4 @@ } } } -} \ No newline at end of file +} diff --git a/tests/laser/smt/bitvecfunc_test.py b/tests/laser/smt/bitvecfunc_test.py index ea19dad1..37217c73 100644 --- a/tests/laser/smt/bitvecfunc_test.py +++ b/tests/laser/smt/bitvecfunc_test.py @@ -1,4 +1,4 @@ -from mythril.laser.smt import Solver, symbol_factory, bitvec +from mythril.laser.smt import Solver, symbol_factory, UGT, UGE, ULT, ULE import z3 import pytest @@ -42,10 +42,10 @@ def test_bitvecfunc_arithmetic(operation, expected): (operator.le, z3.sat), (operator.gt, z3.unsat), (operator.ge, z3.sat), - (bitvec.UGT, z3.unsat), - (bitvec.UGE, z3.sat), - (bitvec.ULT, z3.unsat), - (bitvec.ULE, z3.sat), + (UGT, z3.unsat), + (UGE, z3.sat), + (ULT, z3.unsat), + (ULE, z3.sat), ], ) def test_bitvecfunc_bitvecfunc_comparison(operation, expected): @@ -80,3 +80,158 @@ def test_bitvecfunc_bitvecfuncval_comparison(): # Assert assert s.check() == z3.sat assert s.model().eval(input2.raw) == 1337 + + +def test_bitvecfunc_nested_comparison(): + # arrange + s = Solver() + + input1 = symbol_factory.BitVecSym("input1", 256) + input2 = symbol_factory.BitVecSym("input2", 256) + + bvf1 = symbol_factory.BitVecFuncSym("bvf1", "sha3", 256, input_=input1) + bvf2 = symbol_factory.BitVecFuncSym("bvf2", "sha3", 256, input_=bvf1) + + bvf3 = symbol_factory.BitVecFuncSym("bvf3", "sha3", 256, input_=input2) + bvf4 = symbol_factory.BitVecFuncSym("bvf4", "sha3", 256, input_=bvf3) + + # Act + s.add(input1 == input2) + s.add(bvf2 == bvf4) + + # Assert + assert s.check() == z3.sat + + +def test_bitvecfunc_unequal_nested_comparison(): + # arrange + s = Solver() + + input1 = symbol_factory.BitVecSym("input1", 256) + input2 = symbol_factory.BitVecSym("input2", 256) + + bvf1 = symbol_factory.BitVecFuncSym("bvf1", "sha3", 256, input_=input1) + bvf2 = symbol_factory.BitVecFuncSym("bvf2", "sha3", 256, input_=bvf1) + + bvf3 = symbol_factory.BitVecFuncSym("bvf3", "sha3", 256, input_=input2) + bvf4 = symbol_factory.BitVecFuncSym("bvf4", "sha3", 256, input_=bvf3) + + # Act + s.add(input1 != input2) + s.add(bvf2 == bvf4) + + # Assert + assert s.check() == z3.unsat + + +def test_bitvecfunc_ext_nested_comparison(): + # arrange + s = Solver() + + input1 = symbol_factory.BitVecSym("input1", 256) + input2 = symbol_factory.BitVecSym("input2", 256) + input3 = symbol_factory.BitVecSym("input3", 256) + input4 = symbol_factory.BitVecSym("input4", 256) + + bvf1 = symbol_factory.BitVecFuncSym("bvf1", "sha3", 256, input_=input1) + bvf2 = symbol_factory.BitVecFuncSym("bvf2", "sha3", 256, input_=bvf1 + input3) + + bvf3 = symbol_factory.BitVecFuncSym("bvf3", "sha3", 256, input_=input2) + bvf4 = symbol_factory.BitVecFuncSym("bvf4", "sha3", 256, input_=bvf3 + input4) + + # Act + s.add(input1 == input2) + s.add(input3 == input4) + s.add(bvf2 == bvf4) + + # Assert + assert s.check() == z3.sat + + +def test_bitvecfunc_ext_unequal_nested_comparison(): + # Arrange + s = Solver() + + input1 = symbol_factory.BitVecSym("input1", 256) + input2 = symbol_factory.BitVecSym("input2", 256) + input3 = symbol_factory.BitVecSym("input3", 256) + input4 = symbol_factory.BitVecSym("input4", 256) + + bvf1 = symbol_factory.BitVecFuncSym("bvf1", "sha3", 256, input_=input1) + bvf2 = symbol_factory.BitVecFuncSym("bvf2", "sha3", 256, input_=bvf1 + input3) + + bvf3 = symbol_factory.BitVecFuncSym("bvf3", "sha3", 256, input_=input2) + bvf4 = symbol_factory.BitVecFuncSym("bvf4", "sha3", 256, input_=bvf3 + input4) + + # Act + s.add(input1 == input2) + s.add(input3 != input4) + s.add(bvf2 == bvf4) + + # Assert + assert s.check() == z3.unsat + + +def test_bitvecfunc_ext_unequal_nested_comparison_f(): + # Arrange + s = Solver() + + input1 = symbol_factory.BitVecSym("input1", 256) + input2 = symbol_factory.BitVecSym("input2", 256) + input3 = symbol_factory.BitVecSym("input3", 256) + input4 = symbol_factory.BitVecSym("input4", 256) + + bvf1 = symbol_factory.BitVecFuncSym("bvf1", "sha3", 256, input_=input1) + bvf2 = symbol_factory.BitVecFuncSym("bvf2", "sha3", 256, input_=bvf1 + input3) + + bvf3 = symbol_factory.BitVecFuncSym("bvf3", "sha3", 256, input_=input2) + bvf4 = symbol_factory.BitVecFuncSym("bvf4", "sha3", 256, input_=bvf3 + input4) + + # Act + s.add(input1 != input2) + s.add(input3 == input4) + s.add(bvf2 == bvf4) + + # Assert + assert s.check() == z3.unsat + + +def test_bitvecfunc_find_input(): + # Arrange + s = Solver() + + input1 = symbol_factory.BitVecSym("input1", 256) + input2 = symbol_factory.BitVecSym("input2", 256) + + bvf1 = symbol_factory.BitVecFuncSym("bvf1", "sha3", 256, input_=input1) + bvf2 = symbol_factory.BitVecFuncSym("bvf3", "sha3", 256, input_=input2) + + # Act + s.add(input1 == symbol_factory.BitVecVal(1, 256)) + s.add(bvf1 == bvf2) + + # Assert + assert s.check() == z3.sat + assert s.model()[input2.raw] == 1 + + +def test_bitvecfunc_nested_find_input(): + # Arrange + s = Solver() + + input1 = symbol_factory.BitVecSym("input1", 256) + input2 = symbol_factory.BitVecSym("input2", 256) + + bvf1 = symbol_factory.BitVecFuncSym("bvf1", "sha3", 256, input_=input1) + bvf2 = symbol_factory.BitVecFuncSym("bvf2", "sha3", 256, input_=bvf1) + + bvf3 = symbol_factory.BitVecFuncSym("bvf3", "sha3", 256, input_=input2) + bvf4 = symbol_factory.BitVecFuncSym("bvf4", "sha3", 256, input_=bvf3) + + # Act + s.add(input1 == symbol_factory.BitVecVal(123, 256)) + s.add(bvf2 == bvf4) + + # Assert + assert s.check() == z3.sat + assert s.model()[input2.raw] == 123 diff --git a/tests/laser/transaction/create_transaction_test.py b/tests/laser/transaction/create_transaction_test.py index 5c4e93ad..574dcc06 100644 --- a/tests/laser/transaction/create_transaction_test.py +++ b/tests/laser/transaction/create_transaction_test.py @@ -44,7 +44,7 @@ def test_sym_exec(): contract, address=(util.get_indexed_address(0)), strategy="dfs", - execution_timeout=10, + execution_timeout=25, ) issues = fire_lasers(sym) diff --git a/tests/native_test.py b/tests/native_test.py index b9fd3671..82bb36b4 100644 --- a/tests/native_test.py +++ b/tests/native_test.py @@ -76,6 +76,8 @@ class NativeTests(BaseTestCase): @staticmethod def runTest(): """""" + # The solidity version (0.5.3 at the moment) should be kept in sync with + # pragma in ./tests/native_tests.sol disassembly = SolidityContract( "./tests/native_tests.sol", solc_binary=MythrilDisassembler._init_solc_binary("0.5.3"), diff --git a/tests/native_tests.sol b/tests/native_tests.sol index f786c1bd..15b32021 100644 --- a/tests/native_tests.sol +++ b/tests/native_tests.sol @@ -1,4 +1,4 @@ -pragma solidity 0.5.0; +pragma solidity ^0.5.0; contract Caller { diff --git a/tox.ini b/tox.ini index e50f07fe..804b6791 100644 --- a/tox.ini +++ b/tox.ini @@ -1,5 +1,5 @@ [tox] -envlist = py35,py36 +envlist = py36 [testenv] deps =