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 \ diff --git a/README.md b/README.md index 586d6fd8..4eee32a3 100644 --- a/README.md +++ b/README.md @@ -36,6 +36,45 @@ 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/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 [Wiki](https://github.com/ConsenSys/mythril/wiki). For support or general discussions please join the Mythril community on [Discord](https://discord.gg/E3YrVtG). diff --git a/mythril/analysis/modules/ether_thief.py b/mythril/analysis/modules/ether_thief.py index a6836f7b..c1c5c442 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,12 @@ 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), @@ -140,7 +140,7 @@ 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 [] return [issue] 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/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 %} 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/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 239f7714..bd6c41bb 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 8e3f2cc8..a9953781 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, List @@ -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): @@ -60,7 +63,7 @@ class ArrayStorageRegion(StorageRegion): 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 @@ -78,8 +81,8 @@ class ArrayStorageRegion(StorageRegion): 256, ) return storage[item] - except ValueError: - pass + except ValueError as e: + log.debug("Couldn't read storage at %s: %s", item, e) return simplify(storage[item]) diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 9755fc33..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 @@ -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 @@ -73,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 @@ -102,6 +105,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 +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: @@ -214,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 ( @@ -222,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: @@ -234,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: @@ -256,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: @@ -396,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] 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)