From 476e5dc4e890281fab040e8d3f586c2113ec5135 Mon Sep 17 00:00:00 2001 From: Maxime Biais Date: Thu, 18 Oct 2018 14:19:45 +0200 Subject: [PATCH 1/9] Add a new CLI option to load contract creation bytecode from the command line --- mythril/analysis/symbolic.py | 4 +++- mythril/ether/ethcontract.py | 5 ++--- mythril/interfaces/cli.py | 7 ++++--- mythril/laser/ethereum/svm.py | 2 +- mythril/mythril.py | 8 ++++++-- 5 files changed, 16 insertions(+), 10 deletions(-) diff --git a/mythril/analysis/symbolic.py b/mythril/analysis/symbolic.py index c9431257..71037a6b 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 @@ -35,6 +35,8 @@ class SymExecWrapper: if isinstance(contract, SolidityContract): 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 801e063b..b27f2011 100644 --- a/mythril/ether/ethcontract.py +++ b/mythril/ether/ethcontract.py @@ -6,8 +6,8 @@ import re class ETHContract(persistent.Persistent): - def __init__(self, code, creation_code="", name="Unknown", enable_online_lookup=True): - + def __init__(self, code="", creation_code="", name="Unknown", enable_online_lookup=True): + # Workaround: We currently do not support compile-time linking. # Dynamic contract addresses of the format __[contract-name]_____________ are replaced with a generic address # Apply this for creation_code & code @@ -24,7 +24,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 1784add4..0d1d9ba5 100644 --- a/mythril/interfaces/cli.py +++ b/mythril/interfaces/cli.py @@ -43,10 +43,11 @@ def main(): inputs = parser.add_argument_group('input arguments') inputs.add_argument('-c', '--code', help='hex-encoded bytecode string ("6060604052...")', metavar='BYTECODE') - inputs.add_argument('-f', '--codefile', help='file containing hex-encoded bytecode string', + inputs.add_argument('-f', '--codefile', help='file containing hex-encoded bytecode string', metavar='BYTECODEFILE', type=argparse.FileType('r')) inputs.add_argument('-a', '--address', help='pull contract from the blockchain', metavar='CONTRACT_ADDRESS') inputs.add_argument('-l', '--dynld', action='store_true', help='auto-load dependencies from the blockchain') + inputs.add_argument('--contract-creation', dest="is_contract_creation", action='store_true', help='Only when -c or -f is used. Consider the input bytecode as contract creation code.') outputs = parser.add_argument_group('output formats') outputs.add_argument('-o', '--outform', choices=['text', 'markdown', 'json'], default='text', @@ -166,10 +167,10 @@ def main(): if args.code: # Load from bytecode - address, _ = mythril.load_from_bytecode(args.code) + address, _ = mythril.load_from_bytecode(args.code, args.is_contract_creation) 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.is_contract_creation) elif args.address: # Get bytecode from a contract address address, _ = mythril.load_from_address(args.address) diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index f1bd80b5..e29e4e76 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -93,7 +93,7 @@ class LaserEVM: logging.info("%d nodes, %d edges, %d total states", len(self.nodes), len(self.edges), self.total_states) for code, coverage in self.coverage.items(): cov = reduce(lambda sum_, val: sum_ + 1 if val else sum_, coverage[1]) / 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/mythril.py b/mythril/mythril.py index 123ab904..185c823d 100644 --- a/mythril/mythril.py +++ b/mythril/mythril.py @@ -277,9 +277,13 @@ class Mythril(object): print(self.eth_db.contract_hash_to_address(hash)) - def load_from_bytecode(self, code): + def load_from_bytecode(self, code, is_contract_creation=False): address = util.get_indexed_address(0) - self.contracts.append(ETHContract(code, name="MAIN")) + if (is_contract_creation): + self.contracts.append(ETHContract(creation_code=code, name="MAIN")) + else: + self.contracts.append(ETHContract(code=code, name="MAIN")) + print(self.contracts) return address, self.contracts[-1] # return address and contract object def load_from_address(self, address): From 957575087ba99540a70727f7f93ffe805225df27 Mon Sep 17 00:00:00 2001 From: Maxime Biais Date: Fri, 26 Oct 2018 10:05:57 +0200 Subject: [PATCH 2/9] Replace --contract-creation option by --bin-runtime Default bytecode expected is now the contract creation bytecode. --- mythril/interfaces/cli.py | 6 +++--- mythril/mythril.py | 8 ++++---- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/mythril/interfaces/cli.py b/mythril/interfaces/cli.py index feb7777d..7358ce9d 100644 --- a/mythril/interfaces/cli.py +++ b/mythril/interfaces/cli.py @@ -48,7 +48,7 @@ def main(): metavar='BYTECODEFILE', type=argparse.FileType('r')) inputs.add_argument('-a', '--address', help='pull contract from the blockchain', metavar='CONTRACT_ADDRESS') inputs.add_argument('-l', '--dynld', action='store_true', help='auto-load dependencies from the blockchain') - inputs.add_argument('--contract-creation', dest="is_contract_creation", action='store_true', help='Only when -c or -f is used. Consider the input bytecode as contract creation code.') + 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('-o', '--outform', choices=['text', 'markdown', 'json'], default='text', @@ -175,10 +175,10 @@ def main(): if args.code: # Load from bytecode - address, _ = mythril.load_from_bytecode(args.code, args.is_contract_creation) + 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, args.is_contract_creation) + 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/mythril.py b/mythril/mythril.py index 8097aa18..64243d75 100644 --- a/mythril/mythril.py +++ b/mythril/mythril.py @@ -278,12 +278,12 @@ class Mythril(object): print(self.eth_db.contract_hash_to_address(hash)) - def load_from_bytecode(self, code, is_contract_creation=False): + def load_from_bytecode(self, code, bin_runtime=False): address = util.get_indexed_address(0) - if (is_contract_creation): - self.contracts.append(ETHContract(creation_code=code, name="MAIN", enable_online_lookup=self.enable_online_lookup)) - else: + 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): From 85a2926a568e1350e1cef1e9bd5199c1f55e0973 Mon Sep 17 00:00:00 2001 From: Nathan Date: Wed, 31 Oct 2018 13:15:48 -0400 Subject: [PATCH 3/9] related calldata and concretion improvements/fixes --- mythril/analysis/solver.py | 18 ++++++++---- mythril/laser/ethereum/instructions.py | 3 ++ mythril/laser/ethereum/state.py | 39 +++++++++++++++----------- 3 files changed, 38 insertions(+), 22 deletions(-) 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/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index c31d5f46..53d4d2a0 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -420,6 +420,7 @@ class Instruction: op0 = state.stack.pop() state.stack.append(environment.calldata.get_word_at(op0)) + environment.calldata.update_constraints(state) return [global_state] @StateTransition() @@ -504,6 +505,8 @@ class Instruction: i_data + 1 if isinstance(i_data, int) else simplify(i_data + 1) ) + environment.calldata.update_constraints(state) + for i in range(0, len(new_memory), 32): state.memory[i + mstart] = simplify(Concat(new_memory[i : i + 32])) except IndexError: diff --git a/mythril/laser/ethereum/state.py b/mythril/laser/ethereum/state.py index 20c17c62..15b5ac9e 100644 --- a/mythril/laser/ethereum/state.py +++ b/mythril/laser/ethereum/state.py @@ -4,16 +4,15 @@ from z3 import ( BitVecRef, BitVecNumRef, BitVecSort, - Solver, ExprRef, Concat, sat, simplify, Array, ForAll, - Solver, - UGT, Implies, + UGE, + UGT, ) from z3.z3types import Z3Exception from mythril.disassembler.disassembly import Disassembly @@ -45,6 +44,8 @@ class Calldata: :param starting_calldata: byte array representing the concrete calldata of a transaction """ self.tx_id = tx_id + self._constraints = [] + self._not_yet_added_constraints = [] if starting_calldata: self._calldata = [] self.calldatasize = BitVecVal(len(starting_calldata), 256) @@ -56,28 +57,29 @@ 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 + + @property + def constraints(self): + return self._constraints + + def update_constraints(self, mstate): + """ + Update constraints of a mstate + :param mstate: mstate to add constraints to + """ + mstate.constraints.extend(self._not_yet_added_constraints) + + self._constraints += self._not_yet_added_constraints + self._not_yet_added_constraints = [] def concretized(self, model): result = [] - for i in range( get_concrete_int(model.eval(self.calldatasize, model_completion=True)) ): @@ -111,6 +113,9 @@ class Calldata: except IndexError: return BitVecVal(0, 8) else: + constraints = [Implies(item != 0, UGT(self.calldatasize, item))] + self._not_yet_added_constraints += constraints + return self._calldata[item] From 18c182d5e129223cd6697ed047094330a92b3a74 Mon Sep 17 00:00:00 2001 From: Nathan Date: Wed, 31 Oct 2018 14:05:32 -0400 Subject: [PATCH 4/9] remove now unused code and update unit tests for new Calldata constraints handling --- mythril/laser/ethereum/state.py | 2 +- .../transaction/transaction_models.py | 3 -- tests/laser/state/calldata_test.py | 29 +++++++++++++++---- tests/laser/transaction/symbolic_test.py | 25 ---------------- 4 files changed, 24 insertions(+), 35 deletions(-) diff --git a/mythril/laser/ethereum/state.py b/mythril/laser/ethereum/state.py index 15b5ac9e..649837ee 100644 --- a/mythril/laser/ethereum/state.py +++ b/mythril/laser/ethereum/state.py @@ -46,7 +46,7 @@ class Calldata: self.tx_id = tx_id self._constraints = [] self._not_yet_added_constraints = [] - if starting_calldata: + if not starting_calldata is None: self._calldata = [] self.calldatasize = BitVecVal(len(starting_calldata), 256) self.concrete = True diff --git a/mythril/laser/ethereum/transaction/transaction_models.py b/mythril/laser/ethereum/transaction/transaction_models.py index 4aee343f..eb85b295 100644 --- a/mythril/laser/ethereum/transaction/transaction_models.py +++ b/mythril/laser/ethereum/transaction/transaction_models.py @@ -173,9 +173,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/tests/laser/state/calldata_test.py b/tests/laser/state/calldata_test.py index c2d76c81..2c77a58f 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 @@ -14,13 +14,17 @@ uninitialized_test_data = [ def test_concrete_calldata_uninitialized_index(starting_calldata): # Arrange calldata = Calldata(0, starting_calldata) + mstate = MagicMock() + mstate.constraints = [] solver = Solver() # Act value = calldata[100] value2 = calldata.get_word_at(200) - solver.add(calldata.constraints) + calldata.update_constraints(mstate) + solver.add(mstate.constraints) + solver.check() model = solver.model() @@ -38,7 +42,6 @@ def test_concrete_calldata_calldatasize(): solver = Solver() # Act - solver.add(calldata.constraints) solver.check() model = solver.model() @@ -51,6 +54,8 @@ def test_concrete_calldata_calldatasize(): def test_symbolic_calldata_constrain_index(): # Arrange calldata = Calldata(0) + mstate = MagicMock() + mstate.constraints = [] solver = Solver() # Act @@ -58,7 +63,10 @@ def test_symbolic_calldata_constrain_index(): value = calldata[100] - solver.add(calldata.constraints + [constraint]) + calldata.update_constraints(mstate) + solver.add(mstate.constraints) + solver.add(constraint) + solver.check() model = solver.model() @@ -73,12 +81,16 @@ def test_symbolic_calldata_constrain_index(): def test_concrete_calldata_constrain_index(): # Arrange calldata = Calldata(0, [1, 4, 7, 3, 7, 2, 9]) + mstate = MagicMock() + mstate.constraints = [] solver = Solver() # Act constraint = calldata[2] == 3 - solver.add(calldata.constraints + [constraint]) + calldata.update_constraints(mstate) + solver.add(mstate.constraints) + solver.add(constraint) result = solver.check() # Assert @@ -88,6 +100,8 @@ def test_concrete_calldata_constrain_index(): def test_concrete_calldata_constrain_index(): # Arrange calldata = Calldata(0) + mstate = MagicMock() + mstate.constraints = [] solver = Solver() # Act @@ -95,7 +109,10 @@ def test_concrete_calldata_constrain_index(): constraints.append(calldata[51] == 1) constraints.append(calldata.calldatasize == 50) - solver.add(calldata.constraints + constraints) + calldata.update_constraints(mstate) + solver.add(mstate.constraints) + solver.add(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 From c9f6f8b2f31ccdbd648827fd18368c94803b6605 Mon Sep 17 00:00:00 2001 From: Nathan Date: Wed, 31 Oct 2018 15:04:20 -0400 Subject: [PATCH 5/9] update natives.py to reflect calldata fixes --- mythril/laser/ethereum/natives.py | 24 ++++++++++++++++++++---- 1 file changed, 20 insertions(+), 4 deletions(-) diff --git a/mythril/laser/ethereum/natives.py b/mythril/laser/ethereum/natives.py index 3091c963..bb741929 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 @@ -8,7 +7,8 @@ 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.util import bytearray_to_int, sha3, get_concrete_int +from z3 import Concat, simplify class NativeContractException(Exception): @@ -70,7 +70,16 @@ def ripemd160(data): def identity(data): - 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, data): @@ -79,4 +88,11 @@ def native_contracts(address, data): """ 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) From fe728cc98d223ba16402e2240c35a8adc83ffd9b Mon Sep 17 00:00:00 2001 From: Maxime Biais Date: Mon, 5 Nov 2018 09:59:13 +0100 Subject: [PATCH 6/9] Reformat files using _black_ --- mythril/interfaces/cli.py | 2 +- mythril/mythril.py | 10 +++++++--- 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/mythril/interfaces/cli.py b/mythril/interfaces/cli.py index 01c059f0..51bae2a2 100644 --- a/mythril/interfaces/cli.py +++ b/mythril/interfaces/cli.py @@ -93,7 +93,7 @@ def main(): 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." + 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") diff --git a/mythril/mythril.py b/mythril/mythril.py index 2580166f..67d917f2 100644 --- a/mythril/mythril.py +++ b/mythril/mythril.py @@ -313,16 +313,20 @@ class Mythril(object): def load_from_bytecode(self, code, bin_runtime=False): address = util.get_indexed_address(0) - if (bin_runtime): + if bin_runtime: self.contracts.append( ETHContract( - code=code, name="MAIN", enable_online_lookup=self.enable_online_lookup + 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 + creation_code=code, + name="MAIN", + enable_online_lookup=self.enable_online_lookup, ) ) return address, self.contracts[-1] # return address and contract object From 28c611fc0697e694e52b9c9431dcfc911d419dcf Mon Sep 17 00:00:00 2001 From: Nathan Date: Tue, 6 Nov 2018 08:30:54 -0500 Subject: [PATCH 7/9] fix calldata constraint --- mythril/laser/ethereum/state.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/mythril/laser/ethereum/state.py b/mythril/laser/ethereum/state.py index 649837ee..0c39fbf1 100644 --- a/mythril/laser/ethereum/state.py +++ b/mythril/laser/ethereum/state.py @@ -113,7 +113,9 @@ class Calldata: except IndexError: return BitVecVal(0, 8) else: - constraints = [Implies(item != 0, UGT(self.calldatasize, item))] + constraints = [ + Implies(self._calldata[item] != 0, UGT(self.calldatasize, item)) + ] self._not_yet_added_constraints += constraints return self._calldata[item] From 2662ae07544a72185878fc8e76ed5e1fa78d3338 Mon Sep 17 00:00:00 2001 From: Nathan Date: Tue, 6 Nov 2018 10:59:03 -0500 Subject: [PATCH 8/9] calldata getitem returns tuple with constraints --- mythril/laser/ethereum/instructions.py | 14 ++++--- mythril/laser/ethereum/state.py | 33 ++++++----------- .../transaction/transaction_models.py | 3 -- tests/laser/state/calldata_test.py | 37 +++++++------------ 4 files changed, 33 insertions(+), 54 deletions(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 53d4d2a0..8b838aa2 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -419,8 +419,11 @@ class Instruction: environment = global_state.environment op0 = state.stack.pop() - state.stack.append(environment.calldata.get_word_at(op0)) - environment.calldata.update_constraints(state) + value, constraints = environment.calldata.get_word_at(op0) + + state.stack.append(value) + state.constraints.extend(constraints) + return [global_state] @StateTransition() @@ -500,13 +503,14 @@ 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) ) - environment.calldata.update_constraints(state) - for i in range(0, len(new_memory), 32): state.memory[i + mstart] = simplify(Concat(new_memory[i : i + 32])) except IndexError: diff --git a/mythril/laser/ethereum/state.py b/mythril/laser/ethereum/state.py index 0c39fbf1..9c739308 100644 --- a/mythril/laser/ethereum/state.py +++ b/mythril/laser/ethereum/state.py @@ -44,8 +44,6 @@ class Calldata: :param starting_calldata: byte array representing the concrete calldata of a transaction """ self.tx_id = tx_id - self._constraints = [] - self._not_yet_added_constraints = [] if not starting_calldata is None: self._calldata = [] self.calldatasize = BitVecVal(len(starting_calldata), 256) @@ -64,26 +62,14 @@ class Calldata: else: self._calldata.append(calldata_byte) - @property - def constraints(self): - return self._constraints - - def update_constraints(self, mstate): - """ - Update constraints of a mstate - :param mstate: mstate to add constraints to - """ - mstate.constraints.extend(self._not_yet_added_constraints) - - self._constraints += self._not_yet_added_constraints - self._not_yet_added_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 @@ -105,20 +91,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: constraints = [ Implies(self._calldata[item] != 0, UGT(self.calldatasize, item)) ] - self._not_yet_added_constraints += constraints - return self._calldata[item] + return (self._calldata[item], constraints) class Storage: diff --git a/mythril/laser/ethereum/transaction/transaction_models.py b/mythril/laser/ethereum/transaction/transaction_models.py index eb85b295..3cc1afac 100644 --- a/mythril/laser/ethereum/transaction/transaction_models.py +++ b/mythril/laser/ethereum/transaction/transaction_models.py @@ -91,9 +91,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 diff --git a/tests/laser/state/calldata_test.py b/tests/laser/state/calldata_test.py index 2c77a58f..e93799c3 100644 --- a/tests/laser/state/calldata_test.py +++ b/tests/laser/state/calldata_test.py @@ -14,16 +14,14 @@ uninitialized_test_data = [ def test_concrete_calldata_uninitialized_index(starting_calldata): # Arrange calldata = Calldata(0, starting_calldata) - mstate = MagicMock() - mstate.constraints = [] solver = Solver() # Act - value = calldata[100] - value2 = calldata.get_word_at(200) + value, constraint1 = calldata[100] + value2, constraint2 = calldata.get_word_at(200) - calldata.update_constraints(mstate) - solver.add(mstate.constraints) + solver.add(constraint1) + solver.add(constraint2) solver.check() model = solver.model() @@ -54,18 +52,13 @@ def test_concrete_calldata_calldatasize(): def test_symbolic_calldata_constrain_index(): # Arrange calldata = Calldata(0) - mstate = MagicMock() - mstate.constraints = [] solver = Solver() # Act - constraint = calldata[100] == 50 + value, calldata_constraints = calldata[100] + constraint = value == 50 - value = calldata[100] - - calldata.update_constraints(mstate) - solver.add(mstate.constraints) - solver.add(constraint) + solver.add([constraint] + calldata_constraints) solver.check() model = solver.model() @@ -81,16 +74,13 @@ def test_symbolic_calldata_constrain_index(): def test_concrete_calldata_constrain_index(): # Arrange calldata = Calldata(0, [1, 4, 7, 3, 7, 2, 9]) - mstate = MagicMock() - mstate.constraints = [] solver = Solver() # Act - constraint = calldata[2] == 3 + value, calldata_constraints = calldata[2] + constraint = value == 3 - calldata.update_constraints(mstate) - solver.add(mstate.constraints) - solver.add(constraint) + solver.add([constraint] + calldata_constraints) result = solver.check() # Assert @@ -106,12 +96,11 @@ def test_concrete_calldata_constrain_index(): # Act constraints = [] - constraints.append(calldata[51] == 1) + value, calldata_constraints = calldata[51] + constraints.append(value == 1) constraints.append(calldata.calldatasize == 50) - calldata.update_constraints(mstate) - solver.add(mstate.constraints) - solver.add(constraints) + solver.add(constraints + calldata_constraints) result = solver.check() From 754eaf4fe1db7b89eb6afb05a3922dbcb9a51aea Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Tue, 6 Nov 2018 23:26:09 +0700 Subject: [PATCH 9/9] Add the much cooler "total downloads" badge --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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.