From 8ee33f48ddb860ff873231cab8640e675d7f3ae8 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Thu, 18 Jul 2019 21:03:47 +0200 Subject: [PATCH 01/13] Update README.md --- README.md | 40 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) diff --git a/README.md b/README.md index 586d6fd8..6074ac61 100644 --- a/README.md +++ b/README.md @@ -36,6 +36,46 @@ See the [Wiki](https://github.com/ConsenSys/mythril/wiki/Installation-and-Setup) ## Usage +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/b7c852f5ccaee91da04a789bd1c5ee4b)): + +``` +$ myth analyze killbilly.sol -t3 --execution-timeout 60 +==== Unprotected Selfdestruct ==== +SWC ID: 106 +Severity: High +Contract: KillBilly +Function name: commencekilling() +PC address: 534 +Estimated Gas Usage: 596 - 1021 +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: 0x9fa299cc0101010101010101010101011020200840000080808004014001010101010101, value: 0x0 +Caller: [ATTACKER], function: activatekillability(address), txdata: 0x5aa60cd80101010101010101010101011020200840000080808004014001010101010101, value: 0x0 +Caller: [ATTACKER], function: commencekilling(), txdata: 0x7c11da20, value: 0x0 +``` + + Instructions for using Mythril are found on the [Wiki](https://github.com/ConsenSys/mythril/wiki). For support or general discussions please join the Mythril community on [Discord](https://discord.gg/E3YrVtG). From dd64fd5f5bab1dfdd9f3776c9b2e7bd71e5169ca Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Thu, 18 Jul 2019 21:09:33 +0200 Subject: [PATCH 02/13] Update README.md --- README.md | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index 6074ac61..669b86da 100644 --- a/README.md +++ b/README.md @@ -48,17 +48,16 @@ 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/b7c852f5ccaee91da04a789bd1c5ee4b)): +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)): ``` -$ myth analyze killbilly.sol -t3 --execution-timeout 60 ==== Unprotected Selfdestruct ==== SWC ID: 106 Severity: High Contract: KillBilly Function name: commencekilling() -PC address: 534 -Estimated Gas Usage: 596 - 1021 +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. -------------------- @@ -70,8 +69,8 @@ selfdestruct(msg.sender) Transaction Sequence: Caller: [CREATOR], data: [CONTRACT CREATION], value: 0x0 -Caller: [ATTACKER], function: killerize(address), txdata: 0x9fa299cc0101010101010101010101011020200840000080808004014001010101010101, value: 0x0 -Caller: [ATTACKER], function: activatekillability(address), txdata: 0x5aa60cd80101010101010101010101011020200840000080808004014001010101010101, 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 ``` From 35d88019bd760e3afbc6e2c8cd7a9efd8fb2bed8 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Thu, 18 Jul 2019 21:09:58 +0200 Subject: [PATCH 03/13] Update README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 669b86da..4eee32a3 100644 --- a/README.md +++ b/README.md @@ -48,7 +48,7 @@ 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)): +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 ==== From b3d522b49ca28af1284339a6accbcb93ef4dc88b Mon Sep 17 00:00:00 2001 From: e-ngo <52668908+e-ngo@users.noreply.github.com> Date: Tue, 23 Jul 2019 22:06:24 -0700 Subject: [PATCH 04/13] Enable coverage based search strategy through CLI (#1171) * Enable coverage based search strategy through CLI * Ran black on files changed * Refactored code * Removed redundant code --- mythril/analysis/symbolic.py | 7 ++++++- mythril/interfaces/cli.py | 6 ++++++ mythril/laser/ethereum/svm.py | 9 +++++++++ mythril/mythril/mythril_analyzer.py | 5 +++++ 4 files changed, 26 insertions(+), 1 deletion(-) diff --git a/mythril/analysis/symbolic.py b/mythril/analysis/symbolic.py index 8528a51f..4164758f 100644 --- a/mythril/analysis/symbolic.py +++ b/mythril/analysis/symbolic.py @@ -55,6 +55,7 @@ class SymExecWrapper: enable_iprof=False, disable_dependency_pruning=False, run_analysis_modules=True, + enable_coverage_strategy=False, ): """ @@ -102,6 +103,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 +114,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 +123,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()) diff --git a/mythril/interfaces/cli.py b/mythril/interfaces/cli.py index f18aa254..839d1fd5 100644 --- a/mythril/interfaces/cli.py +++ b/mythril/interfaces/cli.py @@ -391,6 +391,11 @@ 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", + ) def validate_args(args: Namespace): @@ -561,6 +566,7 @@ def execute_command( 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, ) if not disassembler.contracts: diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 9755fc33..c5d5c68e 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -55,6 +55,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 @@ -102,6 +104,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: diff --git a/mythril/mythril/mythril_analyzer.py b/mythril/mythril/mythril_analyzer.py index 497c4c33..deb86281 100644 --- a/mythril/mythril/mythril_analyzer.py +++ b/mythril/mythril/mythril_analyzer.py @@ -41,6 +41,7 @@ class MythrilAnalyzer: enable_iprof: bool = False, disable_dependency_pruning: bool = False, solver_timeout: Optional[int] = None, + enable_coverage_strategy: bool = False, ): """ @@ -61,6 +62,7 @@ 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 analysis_args.set_loop_bound(loop_bound) analysis_args.set_solver_timeout(solver_timeout) @@ -86,6 +88,7 @@ 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, ) return get_serializable_statespace(sym) @@ -121,6 +124,7 @@ 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, ) return generate_graph(sym, physics=enable_physics, phrackify=phrackify) @@ -158,6 +162,7 @@ class MythrilAnalyzer: compulsory_statespace=False, enable_iprof=self.enable_iprof, disable_dependency_pruning=self.disable_dependency_pruning, + enable_coverage_strategy=self.enable_coverage_strategy, ) issues = fire_lasers(sym, modules) From 8071a3c617870ab653a275a43da7b0ae57f9d9d0 Mon Sep 17 00:00:00 2001 From: e-ngo <52668908+e-ngo@users.noreply.github.com> Date: Thu, 25 Jul 2019 00:16:39 -0700 Subject: [PATCH 05/13] Updated jinja templates to report initial state of the transaction sequences. (#1173) --- mythril/analysis/templates/report_as_markdown.jinja2 | 6 ++++++ mythril/analysis/templates/report_as_text.jinja2 | 6 ++++++ 2 files changed, 12 insertions(+) diff --git a/mythril/analysis/templates/report_as_markdown.jinja2 b/mythril/analysis/templates/report_as_markdown.jinja2 index 4583eb26..9e690c43 100644 --- a/mythril/analysis/templates/report_as_markdown.jinja2 +++ b/mythril/analysis/templates/report_as_markdown.jinja2 @@ -26,6 +26,12 @@ 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 %} diff --git a/mythril/analysis/templates/report_as_text.jinja2 b/mythril/analysis/templates/report_as_text.jinja2 index d7b84355..aa5c4876 100644 --- a/mythril/analysis/templates/report_as_text.jinja2 +++ b/mythril/analysis/templates/report_as_text.jinja2 @@ -19,6 +19,12 @@ 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 %} From 9cb791958d669c32d0416f9289e7ce7751d62ec8 Mon Sep 17 00:00:00 2001 From: Aleksandr Sobolev Date: Thu, 25 Jul 2019 17:18:22 +0600 Subject: [PATCH 06/13] Inject missing env variables (#1174) --- .circleci/config.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.circleci/config.yml b/.circleci/config.yml index f18896f1..ae1a05d1 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 \ From dbe1f5210aab74340016c441477448754943800d Mon Sep 17 00:00:00 2001 From: palkeo Date: Mon, 29 Jul 2019 18:24:22 +0200 Subject: [PATCH 07/13] Various small fixes. --- mythril/analysis/modules/ether_thief.py | 16 ++++++++++------ mythril/laser/ethereum/call.py | 16 ++++++++-------- mythril/laser/ethereum/instructions.py | 2 +- mythril/laser/ethereum/state/account.py | 3 ++- mythril/laser/ethereum/svm.py | 17 ++++++++++------- 5 files changed, 31 insertions(+), 23 deletions(-) diff --git a/mythril/analysis/modules/ether_thief.py b/mythril/analysis/modules/ether_thief.py index a6836f7b..d7098179 100644 --- a/mythril/analysis/modules/ether_thief.py +++ b/mythril/analysis/modules/ether_thief.py @@ -21,7 +21,7 @@ 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: @@ -79,8 +79,6 @@ class EtherThief(DetectionModule): if instruction["opcode"] != "CALL": return [] - address = instruction["address"] - value = state.mstate.stack[-3] target = state.mstate.stack[-2] @@ -92,10 +90,10 @@ class EtherThief(DetectionModule): """ 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 + 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)] + constraints += [BVAddNoOverflow(eth_sent_by_attacker, tx.call_value, signed=False)] eth_sent_by_attacker = Sum( eth_sent_by_attacker, tx.call_value * If(tx.caller == ATTACKER_ADDRESS, 1, 0), @@ -120,6 +118,8 @@ class EtherThief(DetectionModule): state.current_transaction.caller == ATTACKER_ADDRESS, ] + log.debug("Constraints: %s", constraints) + try: transaction_sequence = solver.get_transaction_sequence(state, constraints) @@ -140,9 +140,13 @@ class EtherThief(DetectionModule): gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), ) except UnsatError: - log.debug("[ETHER_THIEF] no model found") + log.debug("No model found") return [] + log.debug("Found ether thief issue: %s", issue.as_dict) + + log.debug("Model: %s", solver.pretty_print_model(solver.get_model(constraints))) + return [issue] diff --git a/mythril/laser/ethereum/call.py b/mythril/laser/ethereum/call.py index 918c1d3f..b003e2fb 100644 --- a/mythril/laser/ethereum/call.py +++ b/mythril/laser/ethereum/call.py @@ -4,7 +4,7 @@ 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 @@ -84,6 +84,7 @@ def get_callee_address( except TypeError: log.debug("Symbolic call encountered") + # TODO: This is broken. Now it should be Storage[(\d+)]. match = re.search(r"storage_(\d+)", str(simplify(symbolic_to_address))) log.debug("CALL to: " + str(simplify(symbolic_to_address))) @@ -99,7 +100,7 @@ def get_callee_address( "0x{:040X}".format(environment.active_account.address.value), index ) # TODO: verify whether this happens or not - except: + except Exception: log.debug("Error accessing contract storage.") raise ValueError @@ -120,28 +121,27 @@ def get_callee_account( :param dynamic_loader: dynamic loader to use :return: Account belonging to callee """ - environment = global_state.environment accounts = global_state.accounts 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( @@ -213,7 +213,7 @@ def native_call( call_data: BaseCalldata, memory_out_offset: Union[int, Expression], memory_out_size: Union[int, Expression], -) -> Union[List[GlobalState], None]: +) -> Optional[List[GlobalState]]: if not 0 < int(callee_address, 16) < 5: return None diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index b3e3eaa6..16cb4d38 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -172,7 +172,7 @@ 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" diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py index 1a32ad37..6f50e8ec 100644 --- a/mythril/laser/ethereum/state/account.py +++ b/mythril/laser/ethereum/state/account.py @@ -93,7 +93,8 @@ class Storage: ) self.printable_storage[item] = storage[item] return storage[item] - except ValueError: + except ValueError as e: + log.debug("Couldn't read storage at %s: %s", item, e) pass return simplify(storage[item]) diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index c5d5c68e..c9fc393c 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -3,7 +3,7 @@ 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.laser.ethereum.cfg import NodeFlags, Node, Edge, JumpType from mythril.laser.ethereum.evm_exceptions import StackUnderflowException @@ -75,6 +75,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 @@ -209,7 +210,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: @@ -223,6 +224,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 ( @@ -231,6 +233,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: @@ -243,8 +246,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: @@ -265,11 +267,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: @@ -405,6 +407,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] From 83f0cc966de4a5e61f3aad82820cf066acb047cc Mon Sep 17 00:00:00 2001 From: palkeo Date: Mon, 29 Jul 2019 18:35:37 +0200 Subject: [PATCH 08/13] Reformat with black. --- mythril/analysis/modules/ether_thief.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/mythril/analysis/modules/ether_thief.py b/mythril/analysis/modules/ether_thief.py index d7098179..67df35cd 100644 --- a/mythril/analysis/modules/ether_thief.py +++ b/mythril/analysis/modules/ether_thief.py @@ -93,7 +93,9 @@ class EtherThief(DetectionModule): 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, signed=False)] + constraints += [ + BVAddNoOverflow(eth_sent_by_attacker, tx.call_value, signed=False) + ] eth_sent_by_attacker = Sum( eth_sent_by_attacker, tx.call_value * If(tx.caller == ATTACKER_ADDRESS, 1, 0), From a2a85081f60c883c756f6b7b4e283e41900fb3de Mon Sep 17 00:00:00 2001 From: palkeo Date: Mon, 29 Jul 2019 19:39:01 +0200 Subject: [PATCH 09/13] Add a logger in account.py --- mythril/laser/ethereum/state/account.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py index 6f50e8ec..26f04a01 100644 --- a/mythril/laser/ethereum/state/account.py +++ b/mythril/laser/ethereum/state/account.py @@ -2,6 +2,7 @@ This includes classes representing accounts and their storage. """ +import logging from copy import copy, deepcopy from typing import Any, Dict, Union, Tuple, cast @@ -19,6 +20,8 @@ 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): From 49fbb5f82ff151484785158bd238c871cc44232e Mon Sep 17 00:00:00 2001 From: palkeo Date: Mon, 29 Jul 2019 20:43:25 +0200 Subject: [PATCH 10/13] Fix #1176: retrieve map items. --- mythril/laser/ethereum/state/account.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py index 26f04a01..b5dcb3ae 100644 --- a/mythril/laser/ethereum/state/account.py +++ b/mythril/laser/ethereum/state/account.py @@ -76,8 +76,9 @@ class Storage: if is_keccak_storage: item = self._sanitize(cast(BitVecFunc, item).input_) value = storage[item] + if ( - value.value == 0 + (value.value == 0 or value.value is None) # 0 for Array, None for K and self.address and item.symbolic is False and self.address.value != 0 From 739ac0337b60740c06a148b4233333a6b0cff4f1 Mon Sep 17 00:00:00 2001 From: palkeo Date: Mon, 29 Jul 2019 20:49:05 +0200 Subject: [PATCH 11/13] Fix #1176: load map items --- mythril/laser/ethereum/state/account.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py index 1a32ad37..07e82fad 100644 --- a/mythril/laser/ethereum/state/account.py +++ b/mythril/laser/ethereum/state/account.py @@ -74,7 +74,7 @@ class Storage: item = self._sanitize(cast(BitVecFunc, item).input_) value = storage[item] if ( - value.value == 0 + (value.value == 0 or value.value is None) # 0 for Array, None for K and self.address and item.symbolic is False and self.address.value != 0 From d22b791ba733474814805ff9447862ec548a9171 Mon Sep 17 00:00:00 2001 From: palkeo Date: Mon, 29 Jul 2019 21:40:55 +0200 Subject: [PATCH 12/13] Remove logging messages, and a "pass" --- mythril/analysis/modules/ether_thief.py | 6 ------ mythril/laser/ethereum/state/account.py | 1 - 2 files changed, 7 deletions(-) diff --git a/mythril/analysis/modules/ether_thief.py b/mythril/analysis/modules/ether_thief.py index 67df35cd..c1c5c442 100644 --- a/mythril/analysis/modules/ether_thief.py +++ b/mythril/analysis/modules/ether_thief.py @@ -120,8 +120,6 @@ class EtherThief(DetectionModule): state.current_transaction.caller == ATTACKER_ADDRESS, ] - log.debug("Constraints: %s", constraints) - try: transaction_sequence = solver.get_transaction_sequence(state, constraints) @@ -145,10 +143,6 @@ class EtherThief(DetectionModule): log.debug("No model found") return [] - log.debug("Found ether thief issue: %s", issue.as_dict) - - log.debug("Model: %s", solver.pretty_print_model(solver.get_model(constraints))) - return [issue] diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py index b5dcb3ae..929efea7 100644 --- a/mythril/laser/ethereum/state/account.py +++ b/mythril/laser/ethereum/state/account.py @@ -99,7 +99,6 @@ class Storage: return storage[item] except ValueError as e: log.debug("Couldn't read storage at %s: %s", item, e) - pass return simplify(storage[item]) From 0844497e412c59df4cb0ed1aecdfdf7c3210dce9 Mon Sep 17 00:00:00 2001 From: palkeo Date: Mon, 29 Jul 2019 22:06:39 +0200 Subject: [PATCH 13/13] =?UTF-8?q?Revert=20commit=20that=20should=20not=20h?= =?UTF-8?q?ave=20been=20here=20(other=C2=A0PR)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- mythril/laser/ethereum/state/account.py | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py index 929efea7..07fb4323 100644 --- a/mythril/laser/ethereum/state/account.py +++ b/mythril/laser/ethereum/state/account.py @@ -76,9 +76,8 @@ class Storage: if is_keccak_storage: item = self._sanitize(cast(BitVecFunc, item).input_) value = storage[item] - if ( - (value.value == 0 or value.value is None) # 0 for Array, None for K + value.value == 0 and self.address and item.symbolic is False and self.address.value != 0