Merge branch 'develop' into feature/type-hints-develop

README.md

@@ -9,7 +9,7 @@
 ![Master Build Status](https://img.shields.io/circleci/project/github/ConsenSys/mythril-classic/master.svg)
 [![Waffle.io - Columns and their card count](https://badge.waffle.io/ConsenSys/mythril-classic.svg?columns=In%20Progress)](https://waffle.io/ConsenSys/mythril-classic/)
 [![Sonarcloud - Maintainability](https://sonarcloud.io/api/project_badges/measure?project=mythril&metric=sqale_rating)](https://sonarcloud.io/dashboard?id=mythril)
-[![PyPI Statistics](https://pypistats.com/badge/mythril.svg)](https://pypistats.com/package/mythril)
+[![Downloads](https://pepy.tech/badge/mythril)](https://pepy.tech/project/mythril)
 
 Mythril Classic is an open-source security analysis tool for Ethereum smart contracts. It uses concolic analysis, taint analysis and control flow checking to detect a variety of security vulnerabilities. 
 

mythril/analysis/solver.py

@@ -1,4 +1,4 @@
-from z3 import Solver, simplify, sat, unknown, FuncInterp, UGE
+from z3 import Solver, simplify, sat, unknown, FuncInterp, UGE, Optimize
 from mythril.exceptions import UnsatError
 from mythril.laser.ethereum.transaction.transaction_models import (
     ContractCreationTransaction,
@@ -6,12 +6,17 @@ from mythril.laser.ethereum.transaction.transaction_models import (
 import logging
 
 
-def get_model(constraints):
-    s = Solver()
+def get_model(constraints, minimize=(), maximize=()):
+    s = Optimize()
     s.set("timeout", 100000)
 
     for constraint in constraints:
         s.add(constraint)
+    for e in minimize:
+        s.minimize(e)
+    for e in maximize:
+        s.maximize(e)
+
     result = s.check()
     if result == sat:
         return s.model()
@@ -62,6 +67,7 @@ def get_transaction_sequence(global_state, constraints):
     txs = {}
     creation_tx_ids = []
     tx_constraints = constraints.copy()
+    minimize = []
 
     for transaction in transaction_sequence:
         tx_id = str(transaction.id)
@@ -74,12 +80,14 @@ def get_transaction_sequence(global_state, constraints):
                     UGE(max_calldatasize, transaction.call_data.calldatasize)
                 )
 
+            minimize.append(transaction.call_data.calldatasize)
+
             txs[tx_id] = tx_template.copy()
 
         else:
             creation_tx_ids.append(tx_id)
 
-    model = get_model(tx_constraints)
+    model = get_model(tx_constraints, minimize=minimize)
 
     for transaction in transaction_sequence:
         if not isinstance(transaction, ContractCreationTransaction):
@@ -105,7 +113,7 @@ def get_transaction_sequence(global_state, constraints):
         if "caller" in name:
             # caller is 'creator' for creation transactions
             tx_id = name.replace("caller", "")
-            caller = "0x" + ("%x" % model[d].as_long()).zfill(64)
+            caller = "0x" + ("%x" % model[d].as_long()).zfill(40)
 
             txs[tx_id]["caller"] = caller
 

mythril/analysis/symbolic.py

@@ -1,6 +1,6 @@
 from mythril.laser.ethereum import svm
 from mythril.laser.ethereum.state import Account
-from mythril.ether.soliditycontract import SolidityContract
+from mythril.ether.soliditycontract import SolidityContract, ETHContract
 import copy
 import logging
 from .ops import get_variable, SStore, Call, VarType
@@ -64,6 +64,10 @@ class SymExecWrapper:
             self.laser.sym_exec(
                 creation_code=contract.creation_code, contract_name=contract.name
             )
+        elif isinstance(contract, ETHContract) and contract.creation_code:
+            self.laser.sym_exec(
+                creation_code=contract.creation_code, contract_name=contract.name
+            )
         else:
             self.laser.sym_exec(address)
 

mythril/ether/ethcontract.py

@@ -6,7 +6,7 @@ import re
 
 class ETHContract(persistent.Persistent):
     def __init__(
-        self, code, creation_code="", name="Unknown", enable_online_lookup=False
+        self, code="", creation_code="", name="Unknown", enable_online_lookup=False
     ):
 
         # Workaround: We currently do not support compile-time linking.
@@ -27,7 +27,6 @@ class ETHContract(persistent.Persistent):
     def as_dict(self):
 
         return {
-            "address": self.address,
             "name": self.name,
             "code": self.code,
             "creation_code": self.creation_code,

mythril/interfaces/cli.py

@@ -90,6 +90,11 @@ def main():
         action="store_true",
         help="auto-load dependencies from the blockchain",
     )
+    inputs.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.",
+    )
 
     outputs = parser.add_argument_group("output formats")
     outputs.add_argument(
@@ -316,10 +321,10 @@ def main():
 
         if args.code:
             # Load from bytecode
-            address, _ = mythril.load_from_bytecode(args.code)
+            address, _ = mythril.load_from_bytecode(args.code, args.bin_runtime)
         elif args.codefile:
             bytecode = "".join([l.strip() for l in args.codefile if len(l.strip()) > 0])
-            address, _ = mythril.load_from_bytecode(bytecode)
+            address, _ = mythril.load_from_bytecode(bytecode, args.bin_runtime)
         elif args.address:
             # Get bytecode from a contract address
             address, _ = mythril.load_from_address(args.address)

mythril/laser/ethereum/instructions.py

@@ -422,7 +422,11 @@ class Instruction:
         environment = global_state.environment
         op0 = state.stack.pop()
 
-        state.stack.append(environment.calldata.get_word_at(op0))
+        value, constraints = environment.calldata.get_word_at(op0)
+
+        state.stack.append(value)
+        state.constraints.extend(constraints)
+
         return [global_state]
 
     @StateTransition()
@@ -502,7 +506,10 @@ class Instruction:
 
                 new_memory = []
                 for i in range(size):
-                    new_memory.append(environment.calldata[i_data])
+                    value, constraints = environment.calldata[i_data]
+                    new_memory.append(value)
+                    state.constraints.extend(constraints)
+
                     i_data = (
                         i_data + 1 if isinstance(i_data, int) else simplify(i_data + 1)
                     )

mythril/laser/ethereum/natives.py

@@ -1,6 +1,5 @@
 # -*- coding: utf8 -*-
 
-import copy
 import hashlib
 import logging
 from typing import Union
@@ -9,8 +8,9 @@ from ethereum.utils import ecrecover_to_pub
 from py_ecc.secp256k1 import N as secp256k1n
 from rlp.utils import ALL_BYTES
 
-from mythril.laser.ethereum.util import bytearray_to_int, sha3
 from mythril.laser.ethereum.state import Calldata
+from mythril.laser.ethereum.util import bytearray_to_int, sha3, get_concrete_int
+from z3 import Concat, simplify
 
 
 class NativeContractException(Exception):
@@ -76,11 +76,16 @@ def ripemd160(data: Union[bytes, str]) -> bytes:
 
 
 def identity(data: Union[bytes, str]) -> bytes:
-    try:
-        data = bytes(data)
-    except TypeError:
-        raise NativeContractException
-    return copy.copy(data)
+    # Group up into an array of 32 byte words instead
+    # of an array of bytes. If saved to memory, 32 byte
+    # words are currently needed, but a correct memory
+    # implementation would be byte indexed for the most
+    # part.
+    return data
+    result = []
+    for i in range(0, len(data), 32):
+        result.append(simplify(Concat(data[i : i + 32])))
+    return result
 
 
 def native_contracts(address: int, data: Calldata):
@@ -88,4 +93,11 @@ def native_contracts(address: int, data: Calldata):
     takes integer address 1, 2, 3, 4
     """
     functions = (ecrecover, sha256, ripemd160, identity)
-    return functions[address - 1](data.starting_calldata)
+
+    try:
+        data = [get_concrete_int(e) for e in data._calldata]
+    except TypeError:
+        # Symbolic calldata
+        data = data._calldata
+
+    return functions[address - 1](data)

mythril/laser/ethereum/state.py

@@ -3,16 +3,15 @@ from z3 import (
     BitVecVal,
     BitVecRef,
     BitVecSort,
-    Solver,
     ExprRef,
     Concat,
     sat,
     simplify,
     Array,
     ForAll,
-    Solver,
-    UGT,
     Implies,
+    UGE,
+    UGT,
 )
 from z3.z3types import Z3Exception
 from mythril.disassembler.disassembly import Disassembly
@@ -46,7 +45,7 @@ class Calldata:
         :param starting_calldata: byte array representing the concrete calldata of a transaction
         """
         self.tx_id = tx_id
-        if starting_calldata:
+        if not starting_calldata is None:
             self._calldata = []
             self.calldatasize = BitVecVal(len(starting_calldata), 256)
             self.concrete = True
@@ -57,31 +56,21 @@ class Calldata:
             self.calldatasize = BitVec("{}_calldatasize".format(self.tx_id), 256)
             self.concrete = False
 
-        self.starting_calldata = starting_calldata or []
-
-    @property
-    def constraints(self):
-        constraints = []
         if self.concrete:
-            for calldata_byte in self.starting_calldata:
+            for calldata_byte in starting_calldata:
                 if type(calldata_byte) == int:
                     self._calldata.append(BitVecVal(calldata_byte, 8))
                 else:
                     self._calldata.append(calldata_byte)
-            constraints.append(self.calldatasize == len(self.starting_calldata))
-        else:
-            x = BitVec("x", 256)
-            constraints.append(
-                ForAll(x, Implies(self[x] != 0, UGT(self.calldatasize, x)))
-            )
-        return constraints
 
     def concretized(self, model):
         result = []
         for i in range(
             get_concrete_int(model.eval(self.calldatasize, model_completion=True))
         ):
-            result.append(get_concrete_int(model.eval(self[i], model_completion=True)))
+            result.append(
+                get_concrete_int(model.eval(self._calldata[i], model_completion=True))
+            )
 
         return result
 
@@ -103,15 +92,23 @@ class Calldata:
             except Z3Exception:
                 raise IndexError("Invalid Calldata Slice")
 
-            return simplify(Concat(dataparts))
+            values, constraints = zip(*dataparts)
+            result_constraints = []
+            for c in constraints:
+                result_constraints.extend(c)
+            return (simplify(Concat(values)), result_constraints)
 
         if self.concrete:
             try:
-                return self._calldata[get_concrete_int(item)]
+                return (self._calldata[get_concrete_int(item)], ())
             except IndexError:
-                return BitVecVal(0, 8)
+                return (BitVecVal(0, 8), ())
         else:
-            return self._calldata[item]
+            constraints = [
+                Implies(self._calldata[item] != 0, UGT(self.calldatasize, item))
+            ]
+
+            return (self._calldata[item], constraints)
 
 
 class Storage:

mythril/laser/ethereum/svm.py

@@ -137,7 +137,7 @@ class LaserEVM:
                 / float(coverage[0])
                 * 100
             )
-            logging.info("Achieved {} coverage for code: {}".format(cov, code))
+            logging.info("Achieved {:.2f}% coverage for code: {}".format(cov, code))
 
     def _get_covered_instructions(self) -> int:
         """ Gets the total number of covered instructions for all accounts in the svm"""

mythril/laser/ethereum/transaction/transaction_models.py

@@ -102,9 +102,6 @@ class MessageCallTransaction:
 
         global_state = GlobalState(self.world_state, environment, None)
         global_state.environment.active_function_name = "fallback"
-        global_state.mstate.constraints.extend(
-            global_state.environment.calldata.constraints
-        )
 
         return global_state
 
@@ -184,9 +181,6 @@ class ContractCreationTransaction:
 
         global_state = GlobalState(self.world_state, environment, None)
         global_state.environment.active_function_name = "constructor"
-        global_state.mstate.constraints.extend(
-            global_state.environment.calldata.constraints
-        )
 
         return global_state
 

mythril/mythril.py

@@ -311,13 +311,24 @@ class Mythril(object):
 
         print(self.eth_db.contract_hash_to_address(hash))
 
-    def load_from_bytecode(self, code):
+    def load_from_bytecode(self, code, bin_runtime=False):
         address = util.get_indexed_address(0)
-        self.contracts.append(
-            ETHContract(
-                code, name="MAIN", enable_online_lookup=self.enable_online_lookup
+        if bin_runtime:
+            self.contracts.append(
+                ETHContract(
+                    code=code,
+                    name="MAIN",
+                    enable_online_lookup=self.enable_online_lookup,
+                )
+            )
+        else:
+            self.contracts.append(
+                ETHContract(
+                    creation_code=code,
+                    name="MAIN",
+                    enable_online_lookup=self.enable_online_lookup,
+                )
             )
-        )
         return address, self.contracts[-1]  # return address and contract object
 
     def load_from_address(self, address):

tests/cmd_line_test.py

@@ -10,7 +10,7 @@ def output_of(command):
 
 class CommandLineToolTestCase(BaseTestCase):
     def test_disassemble_code_correctly(self):
-        command = "python3 {} MYTH -d -c 0x5050".format(MYTH)
+        command = "python3 {} MYTH -d --bin-runtime -c 0x5050".format(MYTH)
         self.assertEqual("0 POP\n1 POP\n", output_of(command))
 
     def test_disassemble_solidity_file_correctly(self):

tests/laser/state/calldata_test.py

@@ -2,7 +2,7 @@ import pytest
 from mythril.laser.ethereum.state import Calldata
 from z3 import Solver, simplify
 from z3.z3types import Z3Exception
-
+from mock import MagicMock
 
 uninitialized_test_data = [
     ([]),  # Empty concrete calldata
@@ -17,10 +17,12 @@ def test_concrete_calldata_uninitialized_index(starting_calldata):
     solver = Solver()
 
     # Act
-    value = calldata[100]
-    value2 = calldata.get_word_at(200)
+    value, constraint1 = calldata[100]
+    value2, constraint2 = calldata.get_word_at(200)
+
+    solver.add(constraint1)
+    solver.add(constraint2)
 
-    solver.add(calldata.constraints)
     solver.check()
     model = solver.model()
 
@@ -38,7 +40,6 @@ def test_concrete_calldata_calldatasize():
     solver = Solver()
 
     # Act
-    solver.add(calldata.constraints)
     solver.check()
     model = solver.model()
 
@@ -54,11 +55,11 @@ def test_symbolic_calldata_constrain_index():
     solver = Solver()
 
     # Act
-    constraint = calldata[100] == 50
+    value, calldata_constraints = calldata[100]
+    constraint = value == 50
 
-    value = calldata[100]
+    solver.add([constraint] + calldata_constraints)
 
-    solver.add(calldata.constraints + [constraint])
     solver.check()
     model = solver.model()
 
@@ -76,9 +77,10 @@ def test_concrete_calldata_constrain_index():
     solver = Solver()
 
     # Act
-    constraint = calldata[2] == 3
+    value, calldata_constraints = calldata[2]
+    constraint = value == 3
 
-    solver.add(calldata.constraints + [constraint])
+    solver.add([constraint] + calldata_constraints)
     result = solver.check()
 
     # Assert
@@ -88,14 +90,18 @@ def test_concrete_calldata_constrain_index():
 def test_concrete_calldata_constrain_index():
     # Arrange
     calldata = Calldata(0)
+    mstate = MagicMock()
+    mstate.constraints = []
     solver = Solver()
 
     # Act
     constraints = []
-    constraints.append(calldata[51] == 1)
+    value, calldata_constraints = calldata[51]
+    constraints.append(value == 1)
     constraints.append(calldata.calldatasize == 50)
 
-    solver.add(calldata.constraints + constraints)
+    solver.add(constraints + calldata_constraints)
+
     result = solver.check()
 
     # Assert

tests/laser/transaction/symbolic_test.py

@@ -10,9 +10,6 @@ from mythril.laser.ethereum.svm import LaserEVM
 from mythril.laser.ethereum.state import WorldState, Account
 import unittest.mock as mock
 from unittest.mock import MagicMock
-from mythril.laser.ethereum.transaction.symbolic import (
-    _setup_global_state_for_execution,
-)
 
 
 def _is_message_call(_, transaction):
@@ -70,25 +67,3 @@ def test_execute_contract_creation(mocked_setup: MagicMock):
     # laser_evm.exec.assert_called_once()
     assert laser_evm.exec.call_count == 1
     assert len(laser_evm.open_states) == 0
-
-
-def test_calldata_constraints_in_transaction():
-    # Arrange
-    laser_evm = LaserEVM({})
-    world_state = WorldState()
-
-    correct_constraints = [MagicMock(), MagicMock(), MagicMock()]
-
-    transaction = MessageCallTransaction(
-        world_state, Account("ca11ee"), Account("ca114")
-    )
-    transaction.call_data = MagicMock()
-    transaction.call_data.constraints = correct_constraints
-
-    # Act
-    _setup_global_state_for_execution(laser_evm, transaction)
-
-    # Assert
-    state = laser_evm.work_list[0]
-    for constraint in correct_constraints:
-        assert constraint in state.environment.calldata.constraints