diff --git a/README.md b/README.md index 4b975def..2b3c0fda 100644 --- a/README.md +++ b/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. diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index d41b24c0..37b5a0de 100644 --- a/mythril/analysis/solver.py +++ b/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 diff --git a/mythril/analysis/symbolic.py b/mythril/analysis/symbolic.py index 539fbb24..5bd88896 100644 --- a/mythril/analysis/symbolic.py +++ b/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) diff --git a/mythril/ether/ethcontract.py b/mythril/ether/ethcontract.py index 8914c882..d63f2938 100644 --- a/mythril/ether/ethcontract.py +++ b/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, diff --git a/mythril/interfaces/cli.py b/mythril/interfaces/cli.py index 3f1ad99b..280cc06b 100644 --- a/mythril/interfaces/cli.py +++ b/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) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 2d0913b2..ee9cd974 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/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) ) diff --git a/mythril/laser/ethereum/natives.py b/mythril/laser/ethereum/natives.py index 2de3cfde..f2c75a2f 100644 --- a/mythril/laser/ethereum/natives.py +++ b/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) diff --git a/mythril/laser/ethereum/state.py b/mythril/laser/ethereum/state.py index 0889677f..32f4e68f 100644 --- a/mythril/laser/ethereum/state.py +++ b/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: diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index ed167f22..3b3e4e53 100644 --- a/mythril/laser/ethereum/svm.py +++ b/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""" diff --git a/mythril/laser/ethereum/transaction/transaction_models.py b/mythril/laser/ethereum/transaction/transaction_models.py index 57c747f7..3f2e2e03 100644 --- a/mythril/laser/ethereum/transaction/transaction_models.py +++ b/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 diff --git a/mythril/mythril.py b/mythril/mythril.py index 6477d3b2..6c20f563 100644 --- a/mythril/mythril.py +++ b/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): diff --git a/tests/cmd_line_test.py b/tests/cmd_line_test.py index 394c5d42..9de57a5f 100644 --- a/tests/cmd_line_test.py +++ b/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): diff --git a/tests/laser/state/calldata_test.py b/tests/laser/state/calldata_test.py index c2d76c81..e93799c3 100644 --- a/tests/laser/state/calldata_test.py +++ b/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 diff --git a/tests/laser/transaction/symbolic_test.py b/tests/laser/transaction/symbolic_test.py index 5c18d190..2ca12f63 100644 --- a/tests/laser/transaction/symbolic_test.py +++ b/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