Merge branch 'develop' into feature/regioned_storage

.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 \

README.md

@@ -36,6 +36,45 @@ See the [Wiki](https://github.com/ConsenSys/mythril/wiki/Installation-and-Setup)
 
 ## Usage
 
+Run:
+
+```
+$ myth analyze <solidity-file>
+```
+
+Or:
+
+```
+$ myth analyze -a <contract-address>
+```
+
+Specify the maximum number of transaction to explore with `-t <number>`. You can also set a timeout with `--execution-timeout <seconds>`. 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).

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]

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())

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 %}

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 %}

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:

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
 

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"

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])
 

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]

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)