TheDude
/
mythril
mirror of https://github.com/ConsenSys/mythril
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Merge pull request #501 from JoranHonig/working/suicide_restructure

Browse Source 
storage reimplementation and suicide bugfix
pull/511/head
JoranHonig 6 years ago committed by GitHub
parent 8df53bf737 c12f0976d9
commit e982d10259
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
17 changed files with 304 additions and 225 deletions
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Show Stats Download Patch File Download Diff File
  1. 117
      mythril/analysis/modules/suicide.py
  2. 249
      mythril/laser/ethereum/instructions.py
  3. 17
      mythril/laser/ethereum/keccak.py
  4. 14
      mythril/laser/ethereum/state.py
  5. 4
      mythril/laser/ethereum/svm.py
  6. 3
      mythril/laser/ethereum/transaction/concolic.py
  7. 38
      mythril/laser/ethereum/transaction/symbolic.py
  8. 46
      mythril/laser/ethereum/transaction/transaction_models.py
  9. 4
      solidity_examples/rubixi.sol
  10. 2
      tests/report_test.py
  11. 4
      tests/testdata/input_contracts/metacoin.sol
  12. 2
      tests/testdata/outputs_expected/metacoin.sol.o.json
  13. 14
      tests/testdata/outputs_expected/metacoin.sol.o.markdown
  14. 10
      tests/testdata/outputs_expected/metacoin.sol.o.text
  15. 2
      tests/testdata/outputs_expected/suicide.sol.o.json
  16. 2
      tests/testdata/outputs_expected/suicide.sol.o.markdown
  17. 1
      tests/testdata/outputs_expected/suicide.sol.o.text

117
mythril/analysis/modules/suicide.py
Unescape View File

@ -1,9 +1,7 @@
from z3 import *
from mythril.analysis import solver
from mythril.analysis.ops import *
from mythril.analysis.report import Issue
from mythril.exceptions import UnsatError
import re
import logging
@ -15,86 +13,59 @@ Check for SUICIDE instructions that either can be reached by anyone, or where ms
'''
def execute(statespace):
def execute(state_space):
logging.debug("Executing module: UNCHECKED_SUICIDE")
issues = []
for k in statespace.nodes:
node = statespace.nodes[k]
for k in state_space.nodes:
node = state_space.nodes[k]
for state in node.states:
issues += _analyze_state(state, node)
instruction = state.get_current_instruction()
if(instruction['opcode'] == "SUICIDE"):
logging.debug("[UNCHECKED_SUICIDE] suicide in function " + node.function_name)
description = "The function `" + node.function_name + "` executes the SUICIDE instruction. "
stack = copy.deepcopy(state.mstate.stack)
to = stack.pop()
if ("caller" in str(to)):
description += "The remaining Ether is sent to the caller's address.\n"
elif ("storage" in str(to)):
description += "The remaining Ether is sent to a stored address.\n"
elif ("calldata" in str(to)):
description += "The remaining Ether is sent to an address provided as a function argument.\n"
elif (type(to) == BitVecNumRef):
description += "The remaining Ether is sent to: " + hex(to.as_long()) + "\n"
else:
description += "The remaining Ether is sent to: " + str(to) + "\n"
constrained = False
can_solve = True
index = 0
while(can_solve and index < len(node.constraints)):
constraint = node.constraints[index]
index += 1
m = re.search(r'storage_([a-z0-9_&^]+)', str(constraint))
if (m):
constrained = True
idx = m.group(1)
logging.debug("STORAGE CONSTRAINT FOUND: " + idx)
func = statespace.find_storage_write(state.environment.active_account.address, idx)
if func:
description += "\nThere is a check on storage index " + str(idx) + ". This storage index can be written to by calling the function `" + func + "`."
break
else:
logging.debug("[UNCHECKED_SUICIDE] No storage writes to index " + str(idx))
can_solve = False
break
elif (re.search(r"caller", str(constraint)) and re.search(r'[0-9]{20}', str(constraint))):
can_solve = False
break
if not constrained:
description += "\nIt seems that this function can be called without restrictions."
if can_solve:
try:
model = solver.get_model(node.constraints)
debug = "SOLVER OUTPUT:\n" + solver.pretty_print_model(model)
return issues
issue = Issue(node.contract_name, node.function_name, instruction['address'], "Unchecked SUICIDE", "Warning", description, debug)
issues.append(issue)
except UnsatError:
logging.debug("[UNCHECKED_SUICIDE] no model found")
def _analyze_state(state, node):
issues = []
instruction = state.get_current_instruction()
if instruction['opcode'] != "SUICIDE":
return []
to = state.mstate.stack[-1]
logging.debug("[UNCHECKED_SUICIDE] suicide in function " + node.function_name)
description = "The function `" + node.function_name + "` executes the SUICIDE instruction. "
if "caller" in str(to):
description += "The remaining Ether is sent to the caller's address.\n"
elif "storage" in str(to):
description += "The remaining Ether is sent to a stored address.\n"
elif "calldata" in str(to):
description += "The remaining Ether is sent to an address provided as a function argument.\n"
elif type(to) == BitVecNumRef:
description += "The remaining Ether is sent to: " + hex(to.as_long()) + "\n"
else:
description += "The remaining Ether is sent to: " + str(to) + "\n"
not_creator_constraints = []
if len(state.world_state.transaction_sequence) > 1:
creator = state.world_state.transaction_sequence[0].caller
for transaction in state.world_state.transaction_sequence[1:]:
not_creator_constraints.append(Not(Extract(159, 0, transaction.caller) == Extract(159, 0, creator)))
not_creator_constraints.append(Not(Extract(159, 0, transaction.caller) == 0))
try:
model = solver.get_model(node.constraints + not_creator_constraints)
debug = "SOLVER OUTPUT:\n" + solver.pretty_print_model(model)
issue = Issue(node.contract_name, node.function_name, instruction['address'], "Unchecked SUICIDE", "Warning", description, debug)
issues.append(issue)
except UnsatError:
logging.debug("[UNCHECKED_SUICIDE] no model found")
return issues

249
mythril/laser/ethereum/instructions.py
Unescape View File

@ -2,22 +2,24 @@ import binascii
import logging
from copy import copy, deepcopy
import ethereum.opcodes as opcodes
from ethereum import utils
from z3 import BitVec, Extract, UDiv, simplify, Concat, ULT, UGT, BitVecNumRef, Not, \
is_false, is_expr, ExprRef, URem, SRem
from z3 import BitVecVal, If, BoolRef
from z3 import Extract, UDiv, simplify, Concat, ULT, UGT, BitVecNumRef, Not, \
is_false, is_expr, ExprRef, URem, SRem, BitVec, Solver, is_true, BitVecVal, If, BoolRef, Or
import mythril.laser.ethereum.util as helper
from mythril.laser.ethereum import util
from mythril.laser.ethereum.call import get_call_parameters
from mythril.laser.ethereum.state import GlobalState, MachineState, Environment, CalldataType
from mythril.laser.ethereum.state import GlobalState, CalldataType
import mythril.laser.ethereum.natives as natives
from mythril.laser.ethereum.transaction import MessageCallTransaction, TransactionEndSignal, TransactionStartSignal, ContractCreationTransaction
from mythril.laser.ethereum.transaction import MessageCallTransaction, TransactionStartSignal, ContractCreationTransaction
from mythril.laser.ethereum.keccak import KeccakFunctionManager
TT256 = 2 ** 256
TT256M1 = 2 ** 256 - 1
keccak_function_manager = KeccakFunctionManager()
class StackUnderflowException(Exception):
pass
@ -162,7 +164,7 @@ class Instruction:
result = 0
except AttributeError:
logging.debug("BYTE: Unsupported symbolic byte offset")
result = BitVec(str(simplify(op1)) + "[" + str(simplify(op0)) + "]", 256)
result = global_state.new_bitvec(str(simplify(op1)) + "[" + str(simplify(op0)) + "]", 256)
mstate.stack.append(result)
return [global_state]
@ -236,7 +238,7 @@ class Instruction:
base, exponent = util.pop_bitvec(state), util.pop_bitvec(state)
if (type(base) != BitVecNumRef) or (type(exponent) != BitVecNumRef):
state.stack.append(BitVec("(" + str(simplify(base)) + ")**(" + str(simplify(exponent)) + ")", 256))
state.stack.append(global_state.new_bitvec("(" + str(simplify(base)) + ")**(" + str(simplify(exponent)) + ")", 256))
else:
state.stack.append(pow(base.as_long(), exponent.as_long(), 2**256))
@ -343,12 +345,12 @@ class Instruction:
b = environment.calldata[offset]
except AttributeError:
logging.debug("CALLDATALOAD: Unsupported symbolic index")
state.stack.append(BitVec(
state.stack.append(global_state.new_bitvec(
"calldata_" + str(environment.active_account.contract_name) + "[" + str(simplify(op0)) + "]", 256))
return [global_state]
except IndexError:
logging.debug("Calldata not set, using symbolic variable instead")
state.stack.append(BitVec(
state.stack.append(global_state.new_bitvec(
"calldata_" + str(environment.active_account.contract_name) + "[" + str(simplify(op0)) + "]", 256))
return [global_state]
@ -363,11 +365,11 @@ class Instruction:
state.stack.append(BitVecVal(int.from_bytes(val, byteorder='big'), 256))
# FIXME: broad exception catch
except:
state.stack.append(BitVec(
state.stack.append(global_state.new_bitvec(
"calldata_" + str(environment.active_account.contract_name) + "[" + str(simplify(op0)) + "]", 256))
else:
# symbolic variable
state.stack.append(BitVec(
state.stack.append(global_state.new_bitvec(
"calldata_" + str(environment.active_account.contract_name) + "[" + str(simplify(op0)) + "]", 256))
return [global_state]
@ -377,7 +379,7 @@ class Instruction:
state = global_state.mstate
environment = global_state.environment
if environment.calldata_type == CalldataType.SYMBOLIC:
state.stack.append(BitVec("calldatasize_" + environment.active_account.contract_name, 256))
state.stack.append(global_state.new_bitvec("calldatasize_" + environment.active_account.contract_name, 256))
else:
state.stack.append(BitVecVal(len(environment.calldata), 256))
return [global_state]
@ -415,7 +417,7 @@ class Instruction:
if dstart_sym or size_sym:
state.mem_extend(mstart, 1)
state.memory[mstart] = BitVec(
state.memory[mstart] = global_state.new_bitvec(
"calldata_" + str(environment.active_account.contract_name) + "[" + str(dstart) + ": + " + str(
size) + "]", 256)
return [global_state]
@ -427,7 +429,7 @@ class Instruction:
except:
logging.debug("Memory allocation error: mstart = " + str(mstart) + ", size = " + str(size))
state.mem_extend(mstart, 1)
state.memory[mstart] = BitVec(
state.memory[mstart] = global_state.new_bitvec(
"calldata_" + str(environment.active_account.contract_name) + "[" + str(dstart) + ": + " + str(
size) + "]", 256)
return [global_state]
@ -441,7 +443,7 @@ class Instruction:
except:
logging.debug("Exception copying calldata to memory")
state.memory[mstart] = BitVec(
state.memory[mstart] = global_state.new_bitvec(
"calldata_" + str(environment.active_account.contract_name) + "[" + str(dstart) + ": + " + str(
size) + "]", 256)
return [global_state]
@ -458,7 +460,7 @@ class Instruction:
def balance_(self, global_state):
state = global_state.mstate
address = state.stack.pop()
state.stack.append(BitVec("balance_at_" + str(address), 256))
state.stack.append(global_state.new_bitvec("balance_at_" + str(address), 256))
return [global_state]
@instruction
@ -485,6 +487,8 @@ class Instruction:
@instruction
def sha3_(self, global_state):
global keccak_function_manager
state = global_state.mstate
environment = global_state.environment
op0, op1 = state.stack.pop(), state.stack.pop()
@ -507,23 +511,22 @@ class Instruction:
i += 1
# FIXME: broad exception catch
except:
argument = str(state.memory[index]).replace(" ", "_")
svar = str(state.memory[index])
svar = svar.replace(" ", "_")
state.stack.append(BitVec("keccac_" + svar, 256))
result = BitVec("KECCAC[{}]".format(argument), 256)
keccak_function_manager.add_keccak(result, state.memory[index])
state.stack.append(result)
return [global_state]
keccac = utils.sha3(utils.bytearray_to_bytestr(data))
logging.debug("Computed SHA3 Hash: " + str(binascii.hexlify(keccac)))
keccak = utils.sha3(utils.bytearray_to_bytestr(data))
logging.debug("Computed SHA3 Hash: " + str(binascii.hexlify(keccak)))
state.stack.append(BitVecVal(util.concrete_int_from_bytes(keccac, 0), 256))
state.stack.append(BitVecVal(util.concrete_int_from_bytes(keccak, 0), 256))
return [global_state]
@instruction
def gasprice_(self, global_state):
global_state.mstate.stack.append(BitVec("gasprice", 256))
global_state.mstate.stack.append(global_state.new_bitvec("gasprice", 256))
return [global_state]
@instruction
@ -543,7 +546,7 @@ class Instruction:
# except both attribute error and Exception
global_state.mstate.mem_extend(concrete_memory_offset, 1)
global_state.mstate.memory[concrete_memory_offset] = \
BitVec("code({})".format(global_state.environment.active_account.contract_name), 256)
global_state.new_bitvec("code({})".format(global_state.environment.active_account.contract_name), 256)
return [global_state]
try:
@ -553,7 +556,7 @@ class Instruction:
global_state.mstate.mem_extend(concrete_memory_offset, concrete_size)
for i in range(concrete_size):
global_state.mstate.memory[concrete_memory_offset + i] = \
BitVec("code({})".format(global_state.environment.active_account.contract_name), 256)
global_state.new_bitvec("code({})".format(global_state.environment.active_account.contract_name), 256)
return [global_state]
bytecode = global_state.environment.code.bytecode
@ -562,7 +565,7 @@ class Instruction:
if concrete_code_offset >= len(global_state.environment.code.bytecode) // 2:
global_state.mstate.mem_extend(concrete_memory_offset, 1)
global_state.mstate.memory[concrete_memory_offset] = \
BitVec("code({})".format(global_state.environment.active_account.contract_name), 256)
global_state.new_bitvec("code({})".format(global_state.environment.active_account.contract_name), 256)
return [global_state]
for i in range(concrete_size):
@ -571,7 +574,7 @@ class Instruction:
int(bytecode[2*(concrete_code_offset + i): 2*(concrete_code_offset + i + 1)], 16)
else:
global_state.mstate.memory[concrete_memory_offset + i] = \
BitVec("code({})".format(global_state.environment.active_account.contract_name), 256)
global_state.new_bitvec("code({})".format(global_state.environment.active_account.contract_name), 256)
return [global_state]
@ -584,14 +587,14 @@ class Instruction:
addr = hex(helper.get_concrete_int(addr))
except AttributeError:
logging.info("unsupported symbolic address for EXTCODESIZE")
state.stack.append(BitVec("extcodesize_" + str(addr), 256))
state.stack.append(global_state.new_bitvec("extcodesize_" + str(addr), 256))
return [global_state]
try:
code = self.dynamic_loader.dynld(environment.active_account.address, addr)
except Exception as e:
logging.info("error accessing contract storage due to: " + str(e))
state.stack.append(BitVec("extcodesize_" + str(addr), 256))
state.stack.append(global_state.new_bitvec("extcodesize_" + str(addr), 256))
return [global_state]
if code is None:
@ -611,39 +614,39 @@ class Instruction:
@instruction
def returndatasize_(self, global_state):
global_state.mstate.stack.append(BitVec("returndatasize", 256))
global_state.mstate.stack.append(global_state.new_bitvec("returndatasize", 256))
return [global_state]
@instruction
def blockhash_(self, global_state):
state = global_state.mstate
blocknumber = state.stack.pop()
state.stack.append(BitVec("blockhash_block_" + str(blocknumber), 256))
state.stack.append(global_state.new_bitvec("blockhash_block_" + str(blocknumber), 256))
return [global_state]
@instruction
def coinbase_(self, global_state):
global_state.mstate.stack.append(BitVec("coinbase", 256))
global_state.mstate.stack.append(global_state.new_bitvec("coinbase", 256))
return [global_state]
@instruction
def timestamp_(self, global_state):
global_state.mstate.stack.append(BitVec("timestamp", 256))
global_state.mstate.stack.append(global_state.new_bitvec("timestamp", 256))
return [global_state]
@instruction
def number_(self, global_state):
global_state.mstate.stack.append(BitVec("block_number", 256))
global_state.mstate.stack.append(global_state.new_bitvec("block_number", 256))
return [global_state]
@instruction
def difficulty_(self, global_state):
global_state.mstate.stack.append(BitVec("block_difficulty", 256))
global_state.mstate.stack.append(global_state.new_bitvec("block_difficulty", 256))
return [global_state]
@instruction
def gaslimit_(self, global_state):
global_state.mstate.stack.append(BitVec("block_gaslimit", 256))
global_state.mstate.stack.append(global_state.new_bitvec("block_gaslimit", 256))
return [global_state]
# Memory operations
@ -658,14 +661,14 @@ class Instruction:
offset = util.get_concrete_int(op0)
except AttributeError:
logging.debug("Can't MLOAD from symbolic index")
data = BitVec("mem[" + str(simplify(op0)) + "]", 256)
data = global_state.new_bitvec("mem[" + str(simplify(op0)) + "]", 256)
state.stack.append(data)
return [global_state]
try:
data = util.concrete_int_from_bytes(state.memory, offset)
except IndexError: # Memory slot not allocated
data = BitVec("mem[" + str(offset) + "]", 256)
data = global_state.new_bitvec("mem[" + str(offset) + "]", 256)
except TypeError: # Symbolic memory
data = state.memory[offset]
@ -730,26 +733,68 @@ class Instruction:
@instruction
def sload_(self, global_state):
global keccak_function_manager
state = global_state.mstate
index = state.stack.pop()
logging.debug("Storage access at index " + str(index))
try:
index = util.get_concrete_int(index)
except AttributeError:
index = str(index)
return self._sload_helper(global_state, index)
except AttributeError:
if not keccak_function_manager.is_keccak(index):
return self._sload_helper(global_state, str(index))
storage_keys = global_state.environment.active_account.storage.keys()
keccak_keys = list(filter(keccak_function_manager.is_keccak, storage_keys))
results = []
constraints = []
for keccak_key in keccak_keys:
key_argument = keccak_function_manager.get_argument(keccak_key)
index_argument = keccak_function_manager.get_argument(index)
constraints.append((keccak_key, key_argument == index_argument))
for (keccak_key, constraint) in constraints:
if constraint in state.constraints:
results += self._sload_helper(global_state, keccak_key, [constraint])
if len(results) > 0:
return results
for (keccak_key, constraint) in constraints:
results += self._sload_helper(copy(global_state), keccak_key, [constraint])
if len(results) > 0:
return results
return self._sload_helper(global_state, str(index))
def _sload_helper(self, global_state, index, constraints=None):
try:
data = global_state.environment.active_account.storage[index]
except KeyError:
data = BitVec("storage_" + str(index), 256)
data = global_state.new_bitvec("storage_" + str(index), 256)
global_state.environment.active_account.storage[index] = data
state.stack.append(data)
if constraints is not None:
global_state.mstate.constraints += constraints
global_state.mstate.stack.append(data)
return [global_state]
def _get_constraints(self, keccak_keys, this_key, argument):
global keccak_function_manager
for keccak_key in keccak_keys:
if keccak_key == this_key:
continue
keccak_argument = keccak_function_manager.get_argument(keccak_key)
yield keccak_argument != argument
@instruction
def sstore_(self, global_state):
global keccak_function_manager
state = global_state.mstate
index, value = state.stack.pop(), state.stack.pop()
@ -757,17 +802,52 @@ class Instruction:
try:
index = util.get_concrete_int(index)
return self._sstore_helper(global_state, index, value)
except AttributeError:
index = str(index)
is_keccak = keccak_function_manager.is_keccak(index)
if not is_keccak:
return self._sstore_helper(global_state, str(index), value)
storage_keys = global_state.environment.active_account.storage.keys()
keccak_keys = filter(keccak_function_manager.is_keccak, storage_keys)
solver = Solver()
solver.set(timeout=1000)
results = []
new = False
for keccak_key in keccak_keys:
key_argument = keccak_function_manager.get_argument(keccak_key)
index_argument = keccak_function_manager.get_argument(index)
if is_true(key_argument == index_argument):
return self._sstore_helper(copy(global_state), keccak_key, value, key_argument == index_argument)
results += self._sstore_helper(copy(global_state), keccak_key, value, key_argument == index_argument)
new = Or(new, key_argument != index_argument)
if len(results) > 0:
results += self._sstore_helper(copy(global_state), str(index), value, new)
return results
return self._sstore_helper(global_state, str(index), value)
def _sstore_helper(self, global_state, index, value, constraint=None):
try:
global_state.environment.active_account = deepcopy(global_state.environment.active_account)
global_state.accounts[
global_state.environment.active_account.address] = global_state.environment.active_account
global_state.environment.active_account.storage[index] = value
global_state.environment.active_account.storage[index] =\
value if not isinstance(value, ExprRef) else simplify(value)
except KeyError:
logging.debug("Error writing to storage: Invalid index")
if constraint is not None:
global_state.mstate.constraints.append(constraint)
return [global_state]
@instruction
@ -856,12 +936,12 @@ class Instruction:
@instruction
def msize_(self, global_state):
global_state.mstate.stack.append(BitVec("msize", 256))
global_state.mstate.stack.append(global_state.new_bitvec("msize", 256))
return [global_state]
@instruction
def gas_(self, global_state):
global_state.mstate.stack.append(BitVec("gas", 256))
global_state.mstate.stack.append(global_state.new_bitvec("gas", 256))
return [global_state]
@instruction
@ -887,7 +967,7 @@ class Instruction:
def return_(self, global_state):
state = global_state.mstate
offset, length = state.stack.pop(), state.stack.pop()
return_data = [BitVec("return_data", 256)]
return_data = [global_state.new_bitvec("return_data", 256)]
try:
return_data = state.memory[util.get_concrete_int(offset):util.get_concrete_int(offset + length)]
except AttributeError:
@ -927,9 +1007,9 @@ class Instruction:
"Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(e)
)
# TODO: decide what to do in this case
global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256))
global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256))
return [global_state]
global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256))
global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256))
if 0 < int(callee_address, 16) < 5:
logging.info("Native contract called: " + callee_address)
@ -951,7 +1031,7 @@ class Instruction:
except natives.NativeContractException:
contract_list = ['ecerecover', 'sha256', 'ripemd160', 'identity']
for i in range(mem_out_sz):
global_state.mstate.memory[mem_out_start + i] = BitVec(contract_list[call_address_int - 1] +
global_state.mstate.memory[mem_out_start + i] = global_state.new_bitvec(contract_list[call_address_int - 1] +
"(" + str(call_data) + ")", 256)
return [global_state]
@ -965,11 +1045,11 @@ class Instruction:
transaction = MessageCallTransaction(global_state.world_state,
callee_account,
BitVecVal(int(environment.active_account.address, 16), 256),
call_data,
environment.gasprice,
value,
environment.origin,
call_data_type)
call_data=call_data,
gas_price=environment.gasprice,
call_value=value,
origin=environment.origin,
call_data_type=call_data_type)
raise TransactionStartSignal(transaction, self.op_code)
@instruction
@ -983,12 +1063,12 @@ class Instruction:
logging.info(
"Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(e)
)
global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256))
global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256))
return [global_state]
if global_state.last_return_data is None:
# Put return value on stack
return_value = BitVec("retval_" + str(instr['address']), 256)
return_value = global_state.new_bitvec("retval_" + str(instr['address']), 256)
global_state.mstate.stack.append(return_value)
global_state.mstate.constraints.append(return_value == 0)
@ -998,7 +1078,7 @@ class Instruction:
memory_out_offset = util.get_concrete_int(memory_out_offset) if isinstance(memory_out_offset, ExprRef) else memory_out_offset
memory_out_size = util.get_concrete_int(memory_out_size) if isinstance(memory_out_size, ExprRef) else memory_out_size
except AttributeError:
global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256))
global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256))
return [global_state]
# Copy memory
@ -1007,7 +1087,7 @@ class Instruction:
global_state.mstate.memory[i + memory_out_offset] = global_state.last_return_data[i]
# Put return value on stack
return_value = BitVec("retval_" + str(instr['address']), 256)
return_value = global_state.new_bitvec("retval_" + str(instr['address']), 256)
global_state.mstate.stack.append(return_value)
global_state.mstate.constraints.append(return_value == 1)
@ -1025,18 +1105,18 @@ class Instruction:
logging.info(
"Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(e)
)
global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256))
global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256))
return [global_state]
transaction = MessageCallTransaction(global_state.world_state,
environment.active_account,
environment.address,
call_data,
environment.gasprice,
value,
environment.origin,
call_data_type,
callee_account.code
call_data=call_data,
gas_price=environment.gasprice,
call_value=value,
origin=environment.origin,
call_data_type=call_data_type,
code=callee_account.code
)
raise TransactionStartSignal(transaction, self.op_code)
@ -1051,12 +1131,12 @@ class Instruction:
logging.info(
"Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(e)
)
global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256))
global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256))
return [global_state]
if global_state.last_return_data is None:
# Put return value on stack
return_value = BitVec("retval_" + str(instr['address']), 256)
return_value = global_state.new_bitvec("retval_" + str(instr['address']), 256)
global_state.mstate.stack.append(return_value)
global_state.mstate.constraints.append(return_value == 0)
@ -1066,7 +1146,7 @@ class Instruction:
memory_out_offset = util.get_concrete_int(memory_out_offset) if isinstance(memory_out_offset, ExprRef) else memory_out_offset
memory_out_size = util.get_concrete_int(memory_out_size) if isinstance(memory_out_size, ExprRef) else memory_out_size
except AttributeError:
global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256))
global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256))
return [global_state]
# Copy memory
@ -1075,7 +1155,7 @@ class Instruction:
global_state.mstate.memory[i + memory_out_offset] = global_state.last_return_data[i]
# Put return value on stack
return_value = BitVec("retval_" + str(instr['address']), 256)
return_value = global_state.new_bitvec("retval_" + str(instr['address']), 256)
global_state.mstate.stack.append(return_value)
global_state.mstate.constraints.append(return_value == 1)
@ -1094,18 +1174,18 @@ class Instruction:
logging.info(
"Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(e)
)
global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256))
global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256))
return [global_state]
transaction = MessageCallTransaction(global_state.world_state,
environment.active_account,
environment.sender,
call_data,
environment.gasprice,
environment.callvalue,
environment.origin,
call_data_type,
callee_account.code
gas_price=environment.gasprice,
call_value=environment.callvalue,
origin=environment.origin,
call_data_type=call_data_type,
code=callee_account.code
)
raise TransactionStartSignal(transaction, self.op_code)
@ -1121,12 +1201,12 @@ class Instruction:
logging.info(
"Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(e)
)
global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256))
global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256))
return [global_state]
if global_state.last_return_data is None:
# Put return value on stack
return_value = BitVec("retval_" + str(instr['address']), 256)
return_value = global_state.new_bitvec("retval_" + str(instr['address']), 256)
global_state.mstate.stack.append(return_value)
global_state.mstate.constraints.append(return_value == 0)
@ -1138,7 +1218,7 @@ class Instruction:
memory_out_size = util.get_concrete_int(memory_out_size) if isinstance(memory_out_size,
ExprRef) else memory_out_size
except AttributeError:
global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256))
global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256))
return [global_state]
# Copy memory
@ -1148,7 +1228,7 @@ class Instruction:
global_state.mstate.memory[i + memory_out_offset] = global_state.last_return_data[i]
# Put return value on stack
return_value = BitVec("retval_" + str(instr['address']), 256)
return_value = global_state.new_bitvec("retval_" + str(instr['address']), 256)
global_state.mstate.stack.append(return_value)
global_state.mstate.constraints.append(return_value == 1)
@ -1158,5 +1238,6 @@ class Instruction:
def staticcall_(self, global_state):
# TODO: implement me
instr = global_state.get_current_instruction()
global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256))
global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256))
return [global_state]

17
mythril/laser/ethereum/keccak.py
Unescape View File

@ -0,0 +1,17 @@
from z3 import ExprRef
class KeccakFunctionManager:
def __init__(self):
self.keccak_expression_mapping = {}
def is_keccak(self, expression) -> bool:
return str(expression) in self.keccak_expression_mapping.keys()
def get_argument(self, expression) -> ExprRef:
if not self.is_keccak(expression):
raise ValueError("Expression is not a recognized keccac result")
return self.keccak_expression_mapping[str(expression)][1]
def add_keccak(self, expression: ExprRef, argument: ExprRef):
index = str(expression)
self.keccak_expression_mapping[index] = (expression, argument)

14
mythril/laser/ethereum/state.py
Unescape View File

@ -1,4 +1,4 @@
from z3 import BitVec, BitVecVal
from z3 import BitVec, BitVecVal, Solver, ExprRef, sat
from copy import copy, deepcopy
from enum import Enum
from random import randint
@ -41,6 +41,8 @@ class Storage:
def __setitem__(self, key, value):
self._storage[key] = value
def keys(self):
return self._storage.keys()
class Account:
"""
@ -214,17 +216,23 @@ class GlobalState:
def instruction(self):
return self.get_current_instruction()
def new_bitvec(self, name, size=256):
transaction_id = self.current_transaction.id
node_id = self.node.uid
return BitVec("{}_{}".format(transaction_id, name), size)
class WorldState:
"""
The WorldState class represents the world state as described in the yellow paper
"""
def __init__(self):
def __init__(self, transaction_sequence=None):
"""
Constructor for the world state. Initializes the accounts record
"""
self.accounts = {}
self.node = None
self.transaction_sequence = transaction_sequence or []
def __getitem__(self, item):
"""
@ -235,7 +243,7 @@ class WorldState:
return self.accounts[item]
def __copy__(self):
new_world_state = WorldState()
new_world_state = WorldState(transaction_sequence=self.transaction_sequence[:])
new_world_state.accounts = copy(self.accounts)
new_world_state.node = self.node
return new_world_state

4
mythril/laser/ethereum/svm.py
Unescape View File

@ -185,6 +185,10 @@ class LaserEVM:
elif opcode == "JUMPI":
for state in new_states:
self._new_node_state(state, JumpType.CONDITIONAL, state.mstate.constraints[-1])
elif opcode in ("SLOAD", "SSTORE") and len(new_states) > 1:
for state in new_states:
self._new_node_state(state, JumpType.CONDITIONAL, state.mstate.constraints[-1])
elif opcode in ("CALL", 'CALLCODE', 'DELEGATECALL', 'STATICCALL'):
assert len(new_states) <= 1
for state in new_states:

3
mythril/laser/ethereum/transaction/concolic.py
Unescape View File

@ -1,4 +1,4 @@
from mythril.laser.ethereum.transaction.transaction_models import MessageCallTransaction, ContractCreationTransaction
from mythril.laser.ethereum.transaction.transaction_models import MessageCallTransaction, ContractCreationTransaction, get_next_transaction_id
from z3 import BitVec
from mythril.laser.ethereum.state import GlobalState, Environment, CalldataType, Account, WorldState
from mythril.disassembler.disassembly import Disassembly
@ -12,6 +12,7 @@ def execute_message_call(laser_evm, callee_address, caller_address, origin_addre
for open_world_state in open_states:
transaction = MessageCallTransaction(
identifier=get_next_transaction_id(),
world_state=open_world_state,
callee_account=open_world_state[callee_address],
caller=caller_address,

38
mythril/laser/ethereum/transaction/symbolic.py
Unescape View File

@ -1,8 +1,10 @@
from mythril.laser.ethereum.transaction.transaction_models import MessageCallTransaction, ContractCreationTransaction
from z3 import BitVec
from mythril.laser.ethereum.state import CalldataType
from z3 import BitVec, Extract, Not
from mythril.disassembler.disassembly import Disassembly
from mythril.laser.ethereum.cfg import Node, Edge, JumpType
from mythril.laser.ethereum.state import CalldataType
from mythril.laser.ethereum.transaction.transaction_models import MessageCallTransaction, ContractCreationTransaction,\
get_next_transaction_id
def execute_message_call(laser_evm, callee_address):
@ -11,15 +13,17 @@ def execute_message_call(laser_evm, callee_address):
del laser_evm.open_states[:]
for open_world_state in open_states:
next_transaction_id = get_next_transaction_id()
transaction = MessageCallTransaction(
open_world_state,
open_world_state[callee_address],
BitVec("caller", 256),
[],
BitVec("gas_price", 256),
BitVec("call_value", 256),
BitVec("origin", 256),
CalldataType.SYMBOLIC,
world_state=open_world_state,
callee_account=open_world_state[callee_address],
caller=BitVec("caller{}".format(next_transaction_id), 256),
identifier=next_transaction_id,
call_data=[],
gas_price=BitVec("gas_price{}".format(next_transaction_id), 256),
call_value=BitVec("call_value{}".format(next_transaction_id), 256),
origin=BitVec("origin{}".format(next_transaction_id), 256),
call_data_type=CalldataType.SYMBOLIC,
)
_setup_global_state_for_execution(laser_evm, transaction)
@ -36,18 +40,19 @@ def execute_contract_creation(laser_evm, contract_initialization_code, contract_
new_account.contract_name = contract_name
for open_world_state in open_states:
next_transaction_id = get_next_transaction_id()
transaction = ContractCreationTransaction(
open_world_state,
BitVec("caller", 256),
BitVec("creator{}".format(next_transaction_id), 256),
next_transaction_id,
new_account,
Disassembly(contract_initialization_code),
[],
BitVec("gas_price", 256),
BitVec("call_value", 256),
BitVec("origin", 256),
BitVec("gas_price{}".format(next_transaction_id), 256),
BitVec("call_value{}".format(next_transaction_id), 256),
BitVec("origin{}".format(next_transaction_id), 256),
CalldataType.SYMBOLIC
)
_setup_global_state_for_execution(laser_evm, transaction)
laser_evm.exec(True)
@ -69,6 +74,7 @@ def _setup_global_state_for_execution(laser_evm, transaction):
global_state.mstate.constraints = transaction.world_state.node.constraints
new_node.constraints = global_state.mstate.constraints
global_state.world_state.transaction_sequence.append(transaction)
global_state.node = new_node
new_node.states.append(global_state)
laser_evm.work_list.append(global_state)

46
mythril/laser/ethereum/transaction/transaction_models.py
Unescape View File

@ -4,6 +4,13 @@ from mythril.laser.ethereum.state import GlobalState, Environment, WorldState
from z3 import BitVec
import array
_next_transaction_id = 0
def get_next_transaction_id():
global _next_transaction_id
_next_transaction_id += 1
return _next_transaction_id
class TransactionEndSignal(Exception):
""" Exception raised when a transaction is finalized"""
@ -25,21 +32,23 @@ class MessageCallTransaction:
callee_account,
caller,
call_data=(),
gas_price=BitVec("gasprice", 256),
call_value=BitVec("callvalue", 256),
origin=BitVec("origin", 256),
call_data_type=BitVec("call_data_type", 256),
identifier=None,
gas_price=None,
call_value=None,
origin=None,
call_data_type=None,
code=None
):
assert isinstance(world_state, WorldState)
self.id = identifier or get_next_transaction_id()
self.world_state = world_state
self.callee_account = callee_account
self.caller = caller
self.call_data = call_data
self.gas_price = gas_price
self.call_value = call_value
self.origin = origin
self.call_data_type = call_data_type
self.gas_price = BitVec("gasprice{}".format(identifier), 256) if gas_price is None else gas_price
self.call_value = BitVec("callvalue{}".format(identifier), 256) if call_value is None else call_value
self.origin = BitVec("origin{}".format(identifier), 256) if origin is None else origin
self.call_data_type = BitVec("call_data_type{}".format(identifier), 256) if call_data_type is None else call_data_type
self.code = code
self.return_data = None
@ -71,27 +80,30 @@ class ContractCreationTransaction:
def __init__(self,
world_state,
caller,
identifier=None,
callee_account=None,
code=None,
call_data=(),
gas_price=BitVec("gasprice", 256),
call_value=BitVec("callvalue", 256),
origin=BitVec("origin", 256),
call_data_type=BitVec("call_data_type", 256),
gas_price=None,
call_value=None,
origin=None,
call_data_type=None,
):
assert isinstance(world_state, WorldState)
self.id = identifier or get_next_transaction_id()
self.world_state = world_state
# TODO: set correct balance for new account
self.callee_account = callee_account if callee_account else world_state.create_account(0, concrete_storage=True)
self.caller = caller
self.call_data = call_data
self.gas_price = gas_price
self.call_value = call_value
self.gas_price = BitVec("gasprice{}".format(identifier), 256) if gas_price is None else gas_price
self.call_value = BitVec("callvalue{}".format(identifier), 256) if call_value is None else call_value
self.origin = BitVec("origin{}".format(identifier), 256) if origin is None else origin
self.call_data_type = BitVec("call_data_type{}".format(identifier), 256) if call_data_type is None else call_data_type
self.call_data = call_data
self.origin = origin
self.call_data_type = call_data_type
self.code = code
self.return_data = None

4
solidity_examples/rubixi.sol
Unescape View File

@ -45,7 +45,7 @@ contract Rubixi {
addPayout(_fee);
}
//Function called for valid tx to the contract
//Function called for valid tx to the contract
function addPayout(uint _fee) private {
//Adds new address to participant array
participants.push(Participant(msg.sender, (msg.value * pyramidMultiplier) / 100));
@ -149,4 +149,4 @@ contract Rubixi {
Payout = participants[orderInPyramid].payout / 1 ether;
}
}
}
}

2
tests/report_test.py
Unescape View File

@ -24,7 +24,7 @@ def _fix_debug_data(json_str):
def _generate_report(input_file):
contract = ETHContract(input_file.read_text())
sym = SymExecWrapper(contract, address=(util.get_indexed_address(0)), strategy="dfs")
sym = SymExecWrapper(contract, address=(util.get_indexed_address(0)), strategy="dfs", execution_timeout=30)
issues = fire_lasers(sym)
report = Report()

4
tests/testdata/input_contracts/metacoin.sol vendored
Unescape View File

@ -1,8 +1,8 @@
pragma solidity ^0.4.17;
contract metaCoin {
contract MetaCoin {
mapping (address => uint) public balances;
function metaCoin() public {
function MetaCoin() public {
balances[msg.sender] = 10000;
}

2
tests/testdata/outputs_expected/metacoin.sol.o.json vendored
Unescape View File

@ -1 +1 @@
{"error": null, "issues": [{"address": 498, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "A possible integer overflow exists in the function `sendToken(address,uint256)`.\nThe addition or multiplication may result in a value higher than the maximum representable integer.", "function": "sendToken(address,uint256)", "title": "Integer Overflow", "type": "Warning"}], "success": true}
{"error": null, "issues": [], "success": true}

14
tests/testdata/outputs_expected/metacoin.sol.o.markdown vendored
Unescape View File

@ -1,13 +1,3 @@
# Analysis results for test-filename.sol
# Analysis results for None
## Integer Overflow
- Type: Warning
- Contract: Unknown
- Function name: `sendToken(address,uint256)`
- PC address: 498
### Description
A possible integer overflow exists in the function `sendToken(address,uint256)`.
The addition or multiplication may result in a value higher than the maximum representable integer.
The analysis was completed successfully. No issues were detected.

10
tests/testdata/outputs_expected/metacoin.sol.o.text vendored
Unescape View File

@ -1,9 +1 @@
==== Integer Overflow ====
Type: Warning
Contract: Unknown
Function name: sendToken(address,uint256)
PC address: 498
A possible integer overflow exists in the function `sendToken(address,uint256)`.
The addition or multiplication may result in a value higher than the maximum representable integer.
--------------------
The analysis was completed successfully. No issues were detected.

2
tests/testdata/outputs_expected/suicide.sol.o.json vendored
Unescape View File

@ -1 +1 @@
{"error": null, "issues": [{"address": 146, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The function `_function_0xcbf0b0c0` executes the SUICIDE instruction. The remaining Ether is sent to an address provided as a function argument.\n\nIt seems that this function can be called without restrictions.", "function": "_function_0xcbf0b0c0", "title": "Unchecked SUICIDE", "type": "Warning"}], "success": true}
{"error": null, "issues": [{"address": 146, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The function `_function_0xcbf0b0c0` executes the SUICIDE instruction. The remaining Ether is sent to an address provided as a function argument.\n", "function": "_function_0xcbf0b0c0", "title": "Unchecked SUICIDE", "type": "Warning"}], "success": true}

2
tests/testdata/outputs_expected/suicide.sol.o.markdown vendored
Unescape View File

@ -10,5 +10,3 @@
### Description
The function `_function_0xcbf0b0c0` executes the SUICIDE instruction. The remaining Ether is sent to an address provided as a function argument.
It seems that this function can be called without restrictions.

1
tests/testdata/outputs_expected/suicide.sol.o.text vendored
Unescape View File

@ -5,6 +5,5 @@ Function name: _function_0xcbf0b0c0
PC address: 146
The function `_function_0xcbf0b0c0` executes the SUICIDE instruction. The remaining Ether is sent to an address provided as a function argument.
It seems that this function can be called without restrictions.
--------------------

Write Preview
Loading…
Cancel
Save