Merge branch 'develop' of github.com:ConsenSys/mythril into state_merge

state_merge
Nikhil Parasaram 5 years ago
commit 6af60cd6a6
  1. 2
      README.md
  2. 17
      docs/source/module-list.rst
  3. 2
      mythril/__version__.py
  4. 10
      mythril/analysis/modules/external_calls.py
  5. 6
      mythril/analysis/modules/integer.py
  6. 21
      mythril/analysis/solver.py
  7. 2
      mythril/analysis/templates/report_as_markdown.jinja2
  8. 4
      mythril/analysis/templates/report_as_text.jinja2
  9. 8
      mythril/analysis/traceexplore.py
  10. 2
      mythril/interfaces/cli.py
  11. 37
      mythril/laser/ethereum/call.py
  12. 14
      mythril/laser/ethereum/instruction_data.py
  13. 85
      mythril/laser/ethereum/instructions.py
  14. 31
      mythril/laser/ethereum/natives.py
  15. 3
      mythril/laser/ethereum/state/environment.py
  16. 2
      mythril/support/opcodes.py
  17. 9
      mythril/support/signatures.py
  18. 1
      requirements.txt
  19. 4
      setup.py
  20. 36
      tests/graph_test.py
  21. 73
      tests/instructions/create_test.py
  22. 4
      tests/instructions/static_call_test.py
  23. 42
      tests/laser/Precompiles/test_blake2.py
  24. 93
      tests/native_test.py
  25. 112
      tests/native_tests.sol
  26. 23
      tests/statespace_test.py
  27. 2
      tox.ini

@ -79,7 +79,7 @@ Instructions for using Mythril are found on the [docs](https://mythril-classic.r
For support or general discussions please join the Mythril community on [Discord](https://discord.gg/E3YrVtG).
## Bulding the Documentation
## Building the Documentation
Mythril's documentation is contained in the `docs` folder and is published to [Read the Docs](https://mythril-classic.readthedocs.io/en/master/). It is based on Sphinx and can be built using the Makefile contained in the subdirectory:
```

@ -69,7 +69,20 @@ Unchecked Retval
The `unchecked retval module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/unchecked_retval.py>`_ detects `SWC-104 (Unchecked Call Return Value) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-104>`_.
****************
Unchecked Retval
User Supplied assertion
****************
The `user supplied assertion module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/user_assertions.py>`_ detects `SWC-110 (Assert Violation) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-110>`_ for user-supplied assertions. User supplied assertions should be log messages of the form: :code:`emit AssertionFailed(string)`.
****************
Arbitrary Storage Write
****************
The `user supplied assertion module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/unchecked_retval.py>`_ detects `SWC-110 (Assert Violation) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-110>`_ for user-supplied assertions. User supplied assertions should be log messages of the form: :code:`emit AssertionFailed(string)`.
The `arbitrary storage write module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/arbitrary_write.py>`_ detects `SWC-124 (Write to Arbitrary Storage Location) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-124>`_.
****************
Arbitrary Jump
****************
The `arbitrary jump module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/arbitrary_jump.py>`_ detects `SWC-127 (Arbitrary Jump with Function Type Variable) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-127>`_.

@ -4,4 +4,4 @@ This file is suitable for sourcing inside POSIX shell, e.g. bash as well
as for importing into Python.
"""
__version__ = "v0.21.20"
__version__ = "v0.21.21"

@ -94,14 +94,10 @@ class ExternalCalls(DetectionModule):
# Check whether we can also set the callee address
try:
constraints += [to == ACTORS.attacker]
for tx in state.world_state.transaction_sequence:
if not isinstance(tx, ContractCreationTransaction):
constraints.append(tx.caller == ACTORS.attacker)
new_constraints = constraints + [to == ACTORS.attacker]
solver.get_transaction_sequence(
state, constraints + state.world_state.constraints
state, new_constraints + state.world_state.constraints
)
description_head = "A call to a user-supplied address is executed."
@ -122,7 +118,7 @@ class ExternalCalls(DetectionModule):
severity="Medium",
description_head=description_head,
description_tail=description_tail,
constraints=constraints,
constraints=new_constraints,
detector=self,
)

@ -2,13 +2,12 @@
underflows."""
from math import log2, ceil
from typing import cast, List, Dict, Set
from typing import cast, List, Set
from mythril.analysis import solver
from mythril.analysis.report import Issue
from mythril.analysis.swc_data import INTEGER_OVERFLOW_AND_UNDERFLOW
from mythril.exceptions import UnsatError
from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.laser.ethereum.util import get_concrete_int
from mythril.laser.ethereum.state.annotation import StateAnnotation
from mythril.analysis.modules.base import DetectionModule
from copy import copy
@ -18,6 +17,7 @@ from mythril.laser.smt import (
BVSubNoUnderflow,
BVMulNoOverflow,
BitVec,
If,
symbol_factory,
Not,
Expression,
@ -191,6 +191,8 @@ class IntegerOverflowUnderflowModule(DetectionModule):
value = stack[index]
if isinstance(value, BitVec):
return value
if isinstance(value, Bool):
return If(value, 1, 0)
stack[index] = symbol_factory.BitVecVal(value, 256)
return stack[index]

@ -130,11 +130,32 @@ def get_transaction_sequence(
_replace_with_actual_sha(concrete_transactions, model, code)
else:
_replace_with_actual_sha(concrete_transactions, model)
_add_calldata_placeholder(concrete_transactions, transaction_sequence)
steps = {"initialState": concrete_initial_state, "steps": concrete_transactions}
return steps
def _add_calldata_placeholder(
concrete_transactions: List[Dict[str, str]],
transaction_sequence: List[BaseTransaction],
):
"""
Add's a calldata placeholder into the concrete transactions
:param concrete_transactions:
:param transaction_sequence:
:return:
"""
for tx in concrete_transactions:
tx["calldata"] = tx["input"]
if not isinstance(transaction_sequence[0], ContractCreationTransaction):
return
code_len = len(transaction_sequence[0].code.bytecode)
concrete_transactions[0]["calldata"] = concrete_transactions[0]["input"][
code_len + 2 :
]
def _replace_with_actual_sha(
concrete_transactions: List[Dict[str, str]], model: z3.Model, code=None
):

@ -42,7 +42,7 @@ Account: {% if key == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %}[CREATOR]{%
{% for step in issue.tx_sequence.steps %}
{% if step == issue.tx_sequence.steps[0] and step.input != "0x" and step.origin == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %}
Caller: [CREATOR], data: [CONTRACT_CREATION], value: {{ step.value }}
Caller: [CREATOR], calldata: {{ step.calldata }}, value: {{ step.value }}
{% else %}
Caller: {% if step.origin == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %}[CREATOR]{% elif step.origin == "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef" %}[ATTACKER]{% else %}[SOMEGUY]{% endif %}, function: {{ step.name }}, txdata: {{ step.input }}, value: {{ step.value }}
{% endif %}

@ -32,8 +32,8 @@ Account: {% if key == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %}[CREATOR]{%
Transaction Sequence:
{% for step in issue.tx_sequence.steps %}
{% if step == issue.tx_sequence.steps[0] and step.input != "0x" and step.origin == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %}
Caller: [CREATOR], data: [CONTRACT_CREATION], value: {{ step.value }}
{% if step == issue.tx_sequence.steps[0] and step.address == "" and step.origin == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %}
Caller: [CREATOR], calldata: {{ step.calldata }}, value: {{ step.value }}
{% else %}
Caller: {% if step.origin == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %}[CREATOR]{% elif step.origin == "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef" %}[ATTACKER]{% else %}[SOMEGUY]{% endif %}, function: {{ step.name }}, txdata: {{ step.input }}, value: {{ step.value }}
{% endif %}

@ -81,8 +81,12 @@ def get_serializable_statespace(statespace):
if (len(code_split) < 7)
else "\\n".join(code_split[:6]) + "\\n(click to expand +)"
)
try:
color = color_map[node.get_cfg_dict()["contract_name"]]
except KeyError:
color = colors[i]
i += 1
color_map[node.get_cfg_dict()["contract_name"]] = color
def get_state_accounts(node_state):
"""
@ -97,7 +101,7 @@ def get_serializable_statespace(statespace):
account["balance"] = str(account["balance"])
storage = {}
for storage_key in account["storage"].keys():
for storage_key in account["storage"].printable_storage:
storage[str(storage_key)] = str(account["storage"][storage_key])
state_accounts.append({"address": key, "storage": storage})

@ -384,7 +384,7 @@ def create_analyzer_parser(analyzer_parser: ArgumentParser):
options.add_argument(
"--max-depth",
type=int,
default=50,
default=128,
help="Maximum recursion depth for symbolic execution",
)
options.add_argument(

@ -10,7 +10,7 @@ import mythril.laser.ethereum.util as util
from mythril.laser.ethereum import natives
from mythril.laser.ethereum.instruction_data import calculate_native_gas
from mythril.laser.ethereum.state.account import Account
from mythril.laser.ethereum.natives import PRECOMPILE_COUNT
from mythril.laser.ethereum.natives import PRECOMPILE_COUNT, PRECOMPILE_FUNCTIONS
from mythril.laser.ethereum.state.calldata import (
BaseCalldata,
SymbolicCalldata,
@ -73,6 +73,11 @@ def get_call_parameters(
)
def _get_padded_hex_address(address: int) -> str:
hex_address = hex(address)[2:]
return "0x{}{}".format("0" * (40 - len(hex_address)), hex_address)
def get_callee_address(
global_state: GlobalState,
dynamic_loader: DynLoader,
@ -86,9 +91,10 @@ def get_callee_address(
:return: Address of the callee
"""
environment = global_state.environment
try:
callee_address = hex(util.get_concrete_int(symbolic_to_address))
callee_address = _get_padded_hex_address(
util.get_concrete_int(symbolic_to_address)
)
except TypeError:
log.debug("Symbolic call encountered")
@ -221,6 +227,14 @@ def get_call_data(
return SymbolicCalldata(transaction_id)
def insert_ret_val(global_state: GlobalState):
retval = global_state.new_bitvec(
"retval_" + str(global_state.get_current_instruction()["address"]), 256
)
global_state.mstate.stack.append(retval)
global_state.world_state.constraints.append(retval == 1)
def native_call(
global_state: GlobalState,
callee_address: Union[str, BitVec],
@ -243,22 +257,27 @@ def native_call(
log.debug("CALL with symbolic start or offset not supported")
return [global_state]
contract_list = ["ecrecover", "sha256", "ripemd160", "identity"]
call_address_int = int(callee_address, 16)
native_gas_min, native_gas_max = calculate_native_gas(
global_state.mstate.calculate_extension_size(mem_out_start, mem_out_sz),
contract_list[call_address_int - 1],
PRECOMPILE_FUNCTIONS[call_address_int - 1].__name__,
)
global_state.mstate.min_gas_used += native_gas_min
global_state.mstate.max_gas_used += native_gas_max
global_state.mstate.mem_extend(mem_out_start, mem_out_sz)
try:
data = natives.native_contracts(call_address_int, call_data)
except natives.NativeContractException:
for i in range(mem_out_sz):
global_state.mstate.memory[mem_out_start + i] = global_state.new_bitvec(
contract_list[call_address_int - 1] + "(" + str(call_data) + ")", 8
PRECOMPILE_FUNCTIONS[call_address_int - 1].__name__
+ "("
+ str(call_data)
+ ")",
8,
)
insert_ret_val(global_state)
return [global_state]
for i in range(
@ -266,9 +285,5 @@ def native_call(
): # If more data is used then it's chopped off
global_state.mstate.memory[mem_out_start + i] = data[i]
retval = global_state.new_bitvec(
"retval_" + str(global_state.get_current_instruction()["address"]), 256
)
global_state.mstate.stack.append(retval)
global_state.world_state.constraints.append(retval == 1)
insert_ret_val(global_state)
return [global_state]

@ -48,7 +48,7 @@ OPCODES = {
STACK: BIN_OPERATOR_TUPLE,
},
"ADDRESS": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE},
"BALANCE": {GAS: (400, 400), STACK: UN_OPERATOR_TUPLE},
"BALANCE": {GAS: (700, 700), STACK: UN_OPERATOR_TUPLE},
"ORIGIN": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE},
"CALLER": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE},
"CALLVALUE": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE},
@ -69,7 +69,7 @@ OPCODES = {
GAS: (700, 700 + 3 * 768), # https://ethereum.stackexchange.com/a/47556
STACK: (4, 0),
},
"EXTCODEHASH": {GAS: (400, 400), STACK: UN_OPERATOR_TUPLE},
"EXTCODEHASH": {GAS: (700, 700), STACK: UN_OPERATOR_TUPLE},
"RETURNDATASIZE": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE},
"RETURNDATACOPY": {GAS: (3, 3), STACK: (3, 0)},
"BLOCKHASH": {GAS: (20, 20), STACK: UN_OPERATOR_TUPLE},
@ -78,13 +78,15 @@ OPCODES = {
"NUMBER": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE},
"DIFFICULTY": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE},
"GASLIMIT": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE},
"CHAINID": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE},
"SELFBALANCE": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE},
"POP": {GAS: (2, 2), STACK: (1, 0)},
# assume 1KB memory r/w cost as upper bound
"MLOAD": {GAS: (3, 96), STACK: UN_OPERATOR_TUPLE},
"MSTORE": {GAS: (3, 98), STACK: (2, 0)},
"MSTORE8": {GAS: (3, 98), STACK: (2, 0)},
# assume 64 byte r/w cost as upper bound
"SLOAD": {GAS: (400, 400), STACK: UN_OPERATOR_TUPLE},
"SLOAD": {GAS: (800, 800), STACK: UN_OPERATOR_TUPLE},
"SSTORE": {GAS: (5000, 25000), STACK: (1, 0)},
"JUMP": {GAS: (8, 8), STACK: (1, 0)},
"JUMPI": {GAS: (10, 10), STACK: (2, 0)},
@ -199,7 +201,7 @@ def calculate_native_gas(size: int, contract: str):
:param contract:
:return:
"""
gas_value = None
gas_value = 0
word_num = ceil32(size) // 32
if contract == "ecrecover":
gas_value = opcodes.GECRECOVER
@ -210,7 +212,9 @@ def calculate_native_gas(size: int, contract: str):
elif contract == "identity":
gas_value = opcodes.GIDENTITYBASE + word_num * opcodes.GIDENTITYWORD
else:
raise ValueError("Unknown contract type {}".format(contract))
# TODO: Add gas for other precompiles, computation should be shifted to natives.py
# as some data isn't available here
pass
return gas_value, gas_value

@ -732,7 +732,6 @@ class Instruction:
:return:
"""
state = global_state.mstate
val = state.stack.pop()
exp = Not(val) if isinstance(val, Bool) else val == 0
@ -930,6 +929,27 @@ class Instruction:
state.stack.append(environment.sender)
return [global_state]
@StateTransition()
def chainid_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
global_state.mstate.stack.append(global_state.environment.chainid)
return [global_state]
@StateTransition()
def selfbalance_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return:
"""
balance = global_state.environment.active_account.balance()
global_state.mstate.stack.append(balance)
return [global_state]
@StateTransition()
def codesize_(self, global_state: GlobalState) -> List[GlobalState]:
"""
@ -1395,7 +1415,6 @@ class Instruction:
state.mem_extend(offset, 32)
data = state.memory.get_word_at(offset)
state.stack.append(data)
return [global_state]
@ -1518,7 +1537,6 @@ class Instruction:
states = []
op0, condition = state.stack.pop(), state.stack.pop()
try:
jump_addr = util.get_concrete_int(op0)
except TypeError:
@ -1712,7 +1730,6 @@ class Instruction:
:return:
"""
call_value, mem_offset, mem_size = global_state.mstate.pop(3)
return self._create_transaction_helper(
global_state, call_value, mem_offset, mem_size
)
@ -1739,7 +1756,7 @@ class Instruction:
return self._handle_create_type_post(global_state, opcode="create2")
@staticmethod
def _handle_create_type_post(global_state, opcode="cre ate"):
def _handle_create_type_post(global_state, opcode="create"):
if opcode == "create2":
global_state.mstate.pop(4)
else:
@ -1837,6 +1854,27 @@ class Instruction:
"""
global_state.current_transaction.end(global_state)
@staticmethod
def _write_symbolic_returndata(
global_state: GlobalState, memory_out_offset: BitVec, memory_out_size: BitVec
):
"""
Writes symbolic return-data into memory, The memory offset and size should be concrete
:param global_state:
:param memory_out_offset:
:param memory_out_size:
:return:
"""
if memory_out_offset.symbolic is True or memory_out_size.symbolic is True:
return
for i in range(memory_out_size.value):
global_state.mstate.memory[memory_out_offset + i] = global_state.new_bitvec(
"call_output_var({})_{}".format(
simplify(memory_out_offset + i), global_state.mstate.pc,
),
8,
)
@StateTransition()
def call_(self, global_state: GlobalState) -> List[GlobalState]:
"""
@ -1847,6 +1885,7 @@ class Instruction:
instr = global_state.get_current_instruction()
environment = global_state.environment
memory_out_size, memory_out_offset = global_state.mstate.stack[-7:-5]
try:
(
callee_address,
@ -1875,6 +1914,9 @@ class Instruction:
e
)
)
self._write_symbolic_returndata(
global_state, memory_out_offset, memory_out_size
)
# TODO: decide what to do in this case
global_state.mstate.stack.append(
global_state.new_bitvec("retval_" + str(instr["address"]), 256)
@ -1933,7 +1975,7 @@ class Instruction:
"""
instr = global_state.get_current_instruction()
environment = global_state.environment
memory_out_size, memory_out_offset = global_state.mstate.stack[-7:-5]
try:
(
callee_address,
@ -1944,6 +1986,7 @@ class Instruction:
_,
_,
) = get_call_parameters(global_state, self.dynamic_loader, True)
if callee_account is not None and callee_account.code.bytecode == "":
log.debug("The call is related to ether transfer between accounts")
sender = global_state.environment.active_account.address
@ -1961,6 +2004,9 @@ class Instruction:
e
)
)
self._write_symbolic_returndata(
global_state, memory_out_offset, memory_out_size
)
global_state.mstate.stack.append(
global_state.new_bitvec("retval_" + str(instr["address"]), 256)
)
@ -1988,7 +2034,7 @@ class Instruction:
:return:
"""
instr = global_state.get_current_instruction()
memory_out_size, memory_out_offset = global_state.mstate.stack[-7:-5]
try:
(
callee_address,
@ -2005,6 +2051,9 @@ class Instruction:
e
)
)
self._write_symbolic_returndata(
global_state, memory_out_offset, memory_out_size
)
global_state.mstate.stack.append(
global_state.new_bitvec("retval_" + str(instr["address"]), 256)
)
@ -2016,6 +2065,9 @@ class Instruction:
"retval_" + str(instr["address"]), 256
)
global_state.mstate.stack.append(return_value)
self._write_symbolic_returndata(
global_state, memory_out_offset, memory_out_size
)
global_state.world_state.constraints.append(return_value == 0)
return [global_state]
@ -2060,6 +2112,7 @@ class Instruction:
"""
instr = global_state.get_current_instruction()
environment = global_state.environment
memory_out_size, memory_out_offset = global_state.mstate.stack[-6:-4]
try:
(
@ -2089,6 +2142,9 @@ class Instruction:
e
)
)
self._write_symbolic_returndata(
global_state, memory_out_offset, memory_out_size
)
global_state.mstate.stack.append(
global_state.new_bitvec("retval_" + str(instr["address"]), 256)
)
@ -2116,6 +2172,7 @@ class Instruction:
:return:
"""
instr = global_state.get_current_instruction()
memory_out_size, memory_out_offset = global_state.mstate.stack[-6:-4]
try:
(
@ -2136,6 +2193,9 @@ class Instruction:
global_state.mstate.stack.append(
global_state.new_bitvec("retval_" + str(instr["address"]), 256)
)
self._write_symbolic_returndata(
global_state, memory_out_offset, memory_out_size
)
return [global_state]
if global_state.last_return_data is None:
@ -2188,6 +2248,7 @@ class Instruction:
"""
instr = global_state.get_current_instruction()
environment = global_state.environment
memory_out_size, memory_out_offset = global_state.mstate.stack[-6:-4]
try:
(
callee_address,
@ -2216,6 +2277,9 @@ class Instruction:
e
)
)
self._write_symbolic_returndata(
global_state, memory_out_offset, memory_out_size
)
global_state.mstate.stack.append(
global_state.new_bitvec("retval_" + str(instr["address"]), 256)
)
@ -2248,6 +2312,10 @@ class Instruction:
def post_handler(self, global_state, function_name: str):
instr = global_state.get_current_instruction()
if function_name in ("staticcall", "delegatecall"):
memory_out_size, memory_out_offset = global_state.mstate.stack[-6:-4]
else:
memory_out_size, memory_out_offset = global_state.mstate.stack[-7:-5]
try:
with_value = function_name is not "staticcall"
@ -2266,6 +2334,9 @@ class Instruction:
function_name, e
)
)
self._write_symbolic_returndata(
global_state, memory_out_offset, memory_out_size
)
global_state.mstate.stack.append(
global_state.new_bitvec("retval_" + str(instr["address"]), 256)
)

@ -2,13 +2,17 @@
import hashlib
import logging
from typing import List, Union
import blake2b
from typing import List
from ethereum.utils import ecrecover_to_pub
from py_ecc.secp256k1 import N as secp256k1n
import py_ecc.optimized_bn128 as bn128
from rlp.utils import ALL_BYTES
from eth_utils import ValidationError
from eth._utils.blake2.coders import extract_blake2b_parameters
from mythril.laser.ethereum.state.calldata import BaseCalldata, ConcreteCalldata
from mythril.laser.ethereum.util import extract_copy, extract32
from ethereum.utils import (
@ -192,6 +196,20 @@ def ec_pair(data: List[int]) -> List[int]:
return [0] * 31 + [1 if result else 0]
def blake2b_fcompress(data: List[int]) -> List[int]:
"""
blake2b hashing
:param data:
:return:
"""
try:
parameters = extract_blake2b_parameters(bytes(data))
except ValidationError as v:
logging.debug("Invalid blake2b params: {}".format(v))
return []
return list(bytearray(blake2b.compress(*parameters)))
PRECOMPILE_FUNCTIONS = (
ecrecover,
sha256,
@ -201,7 +219,9 @@ PRECOMPILE_FUNCTIONS = (
ec_add,
ec_mul,
ec_pair,
blake2b_fcompress,
)
PRECOMPILE_COUNT = len(PRECOMPILE_FUNCTIONS)
@ -213,9 +233,10 @@ def native_contracts(address: int, data: BaseCalldata) -> List[int]:
:return:
"""
if isinstance(data, ConcreteCalldata):
concrete_data = data.concrete(None)
else:
if not isinstance(data, ConcreteCalldata):
raise NativeContractException()
concrete_data = data.concrete(None)
try:
return PRECOMPILE_FUNCTIONS[address - 1](concrete_data)
except TypeError:
raise NativeContractException

@ -41,7 +41,10 @@ class Environment:
self.active_function_name = ""
self.address = active_account.address
# TODO: Add tx_2 > tx_1 then block_no(tx_2) > block_no(tx_1)
self.block_number = symbol_factory.BitVecSym("block_number", 256)
self.chainid = symbol_factory.BitVecSym("chain_id", 256)
# Ib
self.code = active_account.code if code is None else code

@ -51,6 +51,8 @@ opcodes = {
0x43: ("NUMBER", 0, 1, 2),
0x44: ("DIFFICULTY", 0, 1, 2),
0x45: ("GASLIMIT", 0, 1, 2),
0x46: ("CHAINID", 0, 1, 2),
0x47: ("SELFBALANCE", 0, 1, 5),
0x50: ("POP", 1, 0, 2),
0x51: ("MLOAD", 1, 1, 3),
0x52: ("MSTORE", 2, 0, 3),

@ -245,8 +245,13 @@ class SignatureDB(object, metaclass=Singleton):
solc_json = get_solc_json(file_path, solc_binary, solc_settings_json)
for contract in solc_json["contracts"][file_path].values():
for name, hash in contract["evm"]["methodIdentifiers"].items():
self.add("0x" + hash, name)
for name, hash_ in contract["evm"]["methodIdentifiers"].items():
sig = "0x{}".format(hash_)
if sig in self.solidity_sigs:
self.solidity_sigs[sig].append(name)
else:
self.solidity_sigs[sig] = [name]
self.add(sig, name)
@staticmethod
def lookup_online(byte_sig: str, timeout: int, proxies=None) -> List[str]:

@ -17,6 +17,7 @@ mock
persistent>=4.2.0
plyvel
py-flags
py-evm==0.3.0a13
py-solc-x==0.6.0
py-solc
pytest>=3.6.0

@ -19,7 +19,7 @@ DESCRIPTION = "Security analysis tool for Ethereum smart contracts"
URL = "https://github.com/ConsenSys/mythril"
AUTHOR = "ConsenSys Dilligence"
AUTHOR_MAIL = None
REQUIRES_PYTHON = ">=3.5.0"
REQUIRES_PYTHON = ">=3.6.0"
# What packages are required for this module to be executed?
@ -52,6 +52,7 @@ REQUIRED = [
"ethereum-input-decoder>=0.2.2",
"matplotlib",
"pythx",
"py-evm==0.3.0a13",
]
TESTS_REQUIRE = ["mypy", "pytest>=3.6.0", "pytest_mock", "pytest-cov"]
@ -118,7 +119,6 @@ setup(
"Intended Audience :: Science/Research",
"Topic :: Software Development :: Disassemblers",
"License :: OSI Approved :: MIT License",
"Programming Language :: Python :: 3.5",
"Programming Language :: Python :: 3.6",
"Programming Language :: Python :: 3.7",
],

@ -1,26 +1,16 @@
from mythril.analysis.callgraph import generate_graph
"""
This test only checks whether dumping is successful, not whether the dumped state space makes sense
"""
from mythril.mythril import MythrilAnalyzer, MythrilDisassembler
from mythril.ethereum import util
from mythril.solidity.soliditycontract import EVMContract
from tests import (
BaseTestCase,
TESTDATA_INPUTS,
TESTDATA_OUTPUTS_EXPECTED,
TESTDATA_OUTPUTS_CURRENT,
)
import re
from tests import TESTDATA_INPUTS
class GraphTest(BaseTestCase):
def test_generate_graph(self):
def test_generate_graph():
for input_file in TESTDATA_INPUTS.iterdir():
output_expected = TESTDATA_OUTPUTS_EXPECTED / (
input_file.name + ".graph.html"
)
output_current = TESTDATA_OUTPUTS_CURRENT / (
input_file.name + ".graph.html"
)
if input_file.name != "origin.sol.o":
continue
contract = EVMContract(input_file.read_text())
disassembler = MythrilDisassembler()
disassembler.contracts.append(contract)
@ -32,14 +22,4 @@ class GraphTest(BaseTestCase):
address=(util.get_indexed_address(0)),
)
html = analyzer.graph_html(transaction_count=1)
output_current.write_text(html)
lines_expected = re.findall(
r"'label': '.*'", str(output_current.read_text())
)
lines_found = re.findall(r"'label': '.*'", str(output_current.read_text()))
if not (lines_expected == lines_found):
self.found_changed_files(input_file, output_expected, output_current)
self.assert_and_show_changed_files()
analyzer.graph_html(transaction_count=1)

@ -1,73 +0,0 @@
from mythril.disassembler.disassembly import Disassembly
from mythril.laser.ethereum.cfg import Node
from mythril.laser.ethereum.state.environment import Environment
from mythril.laser.ethereum.state.machine_state import MachineState
from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.laser.ethereum.state.world_state import WorldState
from mythril.laser.ethereum.instructions import Instruction
from mythril.laser.ethereum.transaction.transaction_models import MessageCallTransaction
from mythril.laser.ethereum.state.calldata import ConcreteCalldata
from mythril.laser.ethereum.svm import LaserEVM
from mythril.laser.smt import symbol_factory
# contract A {
# uint256 public val = 10;
# }
contract_init_code = "6080604052600a600055348015601457600080fd5b506084806100236000396000f3fe6080604052348015600f57600080fd5b506004361060285760003560e01c80633c6bb43614602d575b600080fd5b60336049565b6040518082815260200191505060405180910390f35b6000548156fea265627a7a72315820d3cfe7a909450a953cbd7e47d8c17477f2609baa5208d043e965efec69d1ed9864736f6c634300050b0032"
contract_runtime_code = "6080604052348015600f57600080fd5b506004361060285760003560e01c80633c6bb43614602d575b600080fd5b60336049565b6040518082815260200191505060405180910390f35b6000548156fea265627a7a72315820d3cfe7a909450a953cbd7e47d8c17477f2609baa5208d043e965efec69d1ed9864736f6c634300050b0032"
last_state = None
created_contract_account = None
def execute_create():
global last_state
global created_contract_account
if not last_state and not created_contract_account:
code_raw = []
for i in range(len(contract_init_code) // 2):
code_raw.append(int(contract_init_code[2 * i : 2 * (i + 1)], 16))
calldata = ConcreteCalldata(0, code_raw)
world_state = WorldState()
world_state.node = Node("Contract")
account = world_state.create_account(balance=1000000, address=101)
account.code = Disassembly("60a760006000f000")
environment = Environment(account, None, calldata, None, None, None)
og_state = GlobalState(
world_state, environment, world_state.node, MachineState(gas_limit=8000000)
)
og_state.transaction_stack.append(
(MessageCallTransaction(world_state=WorldState(), gas_limit=8000000), None)
)
laser = LaserEVM()
states = [og_state]
last_state = og_state
for state in states:
new_states, op_code = laser.execute_state(state)
last_state = state
if op_code == "STOP":
break
states.extend(new_states)
created_contract_address = last_state.mstate.stack[-1].value
created_contract_account = last_state.world_state.accounts[
created_contract_address
]
return last_state, created_contract_account
def test_create_has_code():
last_state, created_contract_account = execute_create()
assert created_contract_account.code.bytecode == contract_runtime_code
def test_create_has_storage():
last_state, created_contract_account = execute_create()
storage = created_contract_account.storage
# From contract, val = 10.
assert storage[symbol_factory.BitVecVal(0, 256)] == symbol_factory.BitVecVal(
10, 256
)

@ -90,7 +90,7 @@ def test_staticness_call_concrete(f1, input, success):
# Arrange
state = get_global_state()
state.environment.static = True
state.mstate.stack = []
state.mstate.stack = [10] * 100
code = Disassembly(code="616263")
f1.return_value = ("0", Account(code=code, address="0x19"), 0, input, 0, 0, 0)
instruction = Instruction("call", dynamic_loader=None)
@ -110,7 +110,7 @@ def test_staticness_call_symbolic(f1):
# Arrange
state = get_global_state()
state.environment.static = True
state.mstate.stack = []
state.mstate.stack = [10] * 100
call_value = symbol_factory.BitVecSym("x", 256)
code = Disassembly(code="616263")
f1.return_value = ("0", Account(code=code, address="0x19"), 0, call_value, 0, 0, 0)

@ -0,0 +1,42 @@
import pytest
from mythril.laser.ethereum.natives import blake2b_fcompress
# Test cases taken from https://eips.ethereum.org/EIPS/eip-152.
# One of the test case is expected to take a few hrs so I ignored it
@pytest.mark.parametrize(
"input_hex, expected_result",
(
("", ""),
(
"00000c48c9bdf267e6096a3ba7ca8485ae67bb2bf894fe72f36e3cf1361d5f3af54fa5d182e6ad7f520e511f6c3e2b8c68059b6bbd41fbabd9831f79217e1319cde05b61626300000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000300000000000000000000000000000001", # noqa: E501
"",
),
(
"000000000c48c9bdf267e6096a3ba7ca8485ae67bb2bf894fe72f36e3cf1361d5f3af54fa5d182e6ad7f520e511f6c3e2b8c68059b6bbd41fbabd9831f79217e1319cde05b61626300000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000300000000000000000000000000000001", # noqa: E501
"",
),
(
"0000000c48c9bdf267e6096a3ba7ca8485ae67bb2bf894fe72f36e3cf1361d5f3af54fa5d182e6ad7f520e511f6c3e2b8c68059b6bbd41fbabd9831f79217e1319cde05b61626300000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000300000000000000000000000000000002", # noqa: E501
"",
),
(
"0000000048c9bdf267e6096a3ba7ca8485ae67bb2bf894fe72f36e3cf1361d5f3af54fa5d182e6ad7f520e511f6c3e2b8c68059b6bbd41fbabd9831f79217e1319cde05b61626300000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000300000000000000000000000000000001", # noqa: E501
"08c9bcf367e6096a3ba7ca8485ae67bb2bf894fe72f36e3cf1361d5f3af54fa5d282e6ad7f520e511f6c3e2b8c68059b9442be0454267ce079217e1319cde05b", # noqa: E501
),
(
"0000000c48c9bdf267e6096a3ba7ca8485ae67bb2bf894fe72f36e3cf1361d5f3af54fa5d182e6ad7f520e511f6c3e2b8c68059b6bbd41fbabd9831f79217e1319cde05b61626300000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000300000000000000000000000000000001", # noqa: E501
"ba80a53f981c4d0d6a2797b69f12f6e94c212f14685ac4b74b12bb6fdbffa2d17d87c5392aab792dc252d5de4533cc9518d38aa8dbf1925ab92386edd4009923", # noqa: E501
),
(
"0000000c48c9bdf267e6096a3ba7ca8485ae67bb2bf894fe72f36e3cf1361d5f3af54fa5d182e6ad7f520e511f6c3e2b8c68059b6bbd41fbabd9831f79217e1319cde05b61626300000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000300000000000000000000000000000000", # noqa: E501
"75ab69d3190a562c51aef8d88f1c2775876944407270c42c9844252c26d2875298743e7f6d5ea2f2d3e8d226039cd31b4e426ac4f2d3d666a610c2116fde4735", # noqa: E501
),
(
"0000000148c9bdf267e6096a3ba7ca8485ae67bb2bf894fe72f36e3cf1361d5f3af54fa5d182e6ad7f520e511f6c3e2b8c68059b6bbd41fbabd9831f79217e1319cde05b61626300000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000300000000000000000000000000000001", # noqa: E501
"b63a380cb2897d521994a85234ee2c181b5f844d2c624c002677e9703449d2fba551b3a8333bcdf5f2f7e08993d53923de3d64fcc68c034e717b9293fed7a421", # noqa: E501
),
),
)
def test_blake2(input_hex, expected_result):
input_hex = bytearray.fromhex(input_hex)
assert blake2b_fcompress(input_hex) == list(bytearray.fromhex(expected_result))

@ -1,93 +0,0 @@
from mythril.solidity.soliditycontract import SolidityContract
from mythril.mythril import MythrilDisassembler
from mythril.laser.ethereum.state.account import Account
from mythril.laser.ethereum.state.machine_state import MachineState
from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.laser.ethereum.state.world_state import WorldState
from mythril.laser.ethereum import svm
from tests import BaseTestCase
SHA256_TEST = [(0, False) for _ in range(4)]
RIPEMD160_TEST = [(0, False) for _ in range(2)]
ECRECOVER_TEST = [(0, False) for _ in range(2)]
IDENTITY_TEST = [(0, False) for _ in range(2)]
# These are Random numbers to check whether the 'if condition' is entered or not
# (True means entered)
SHA256_TEST[0] = (hex(5555555555555555), True)
SHA256_TEST[1] = (hex(323232325445454546), False)
SHA256_TEST[2] = (hex(34756834765834658), True)
SHA256_TEST[3] = (hex(8756476956956795876987), False)
RIPEMD160_TEST[0] = (hex(999999999999999999993), True)
RIPEMD160_TEST[1] = (hex(1111111111112), False)
ECRECOVER_TEST[0] = (hex(674837568743979857398564869), True)
ECRECOVER_TEST[1] = (hex(3487683476979311), False)
IDENTITY_TEST[0] = (hex(87426857369875698), True)
IDENTITY_TEST[1] = (hex(476934798798347), False)
def _all_info(laser):
nodes = {}
for uid, node in laser.nodes.items():
states = []
for state in node.states:
if isinstance(state, MachineState):
states.append(state.as_dict)
elif isinstance(state, GlobalState):
environment = state.environment.as_dict
environment["active_account"] = environment["active_account"].address
states.append(
{
"accounts": state.accounts.keys(),
"environment": environment,
"mstate": state.mstate.as_dict,
}
)
nodes[uid] = {
"uid": node.uid,
"contract_name": node.contract_name,
"start_addr": node.start_addr,
"states": states,
"constraints": node.constraints,
"function_name": node.function_name,
"flags": str(node.flags),
}
edges = [edge.as_dict for edge in laser.edges]
return {
"nodes": nodes,
"edges": edges,
"total_states": laser.total_states,
"max_depth": laser.max_depth,
}
def _test_natives(laser_info, test_list, test_name):
for i, j in test_list:
assert (str(i) in laser_info or str(int(i, 16)) in laser_info) == j
class NativeTests(BaseTestCase):
@staticmethod
def runTest():
""""""
# The solidity version (0.5.3 at the moment) should be kept in sync with
# pragma in ./tests/native_tests.sol
disassembly = SolidityContract("./tests/native_tests.sol").disassembly
account = Account("0x0000000000000000000000000000000000000000", disassembly)
world_state = WorldState()
world_state.put_account(account)
laser = svm.LaserEVM(max_depth=100, transaction_count=1)
laser.sym_exec(world_state=world_state, target_address=account.address.value)
laser_info = str(_all_info(laser))
_test_natives(laser_info, SHA256_TEST, "SHA256")
_test_natives(laser_info, RIPEMD160_TEST, "RIPEMD160")
_test_natives(laser_info, ECRECOVER_TEST, "ECRECOVER")
_test_natives(laser_info, IDENTITY_TEST, "IDENTITY")

@ -1,112 +0,0 @@
pragma solidity ^0.5.0;
contract Caller {
//Just some useless variables
address public fixedAddress;
address public storedAddress;
//useless (but good for testing as they contribute as decoys)
uint256 private statevar;
bytes32 private far;
constructor (address addr) public {
fixedAddress = addr;
}
/*
// Commented out because this causes laser to enter an infinite loop... :/
// It sets the free memory pointer to a symbolic value, and things break
//some typical function as a decoy
function thisisfine() public {
(bool success, bytes memory mem) = fixedAddress.call("");
}
*/
function sha256Test1() public returns (uint256) {
uint256 i;
if (sha256(abi.encodePacked("ab", "c")) == sha256("abc")) {
// True
i = 5555555555555555;
} else {
// False
i = 323232325445454546;
}
return i;
}
function sha256Test2() public returns (uint256) {
uint256 i;
if (sha256("abd") == sha256(abi.encodePacked("ab", "d"))) {
// True
i = 34756834765834658;
} else {
// False
i = 8756476956956795876987;
}
return i;
}
function ripemdTest() public returns (uint256) {
uint256 i;
bytes20 v1 = ripemd160("");
bytes20 v2 = ripemd160("hhhhh");
if (v1 != v2) {
// True
i = 999999999999999999993;
} else {
// False
i = 1111111111112;
}
return i;
}
function ecrecoverTest() public returns (uint256) {
bytes32 foobar1 = 0x1c8aff950685c2ed4bc3174f3472287b56d9517b9c948127319a09a7a36deac8;
bytes32 foobar2 = 0x38d18acb67d25c8bb9942764b62f18e17054f66a817bd4295423adf9ed98873e;
uint8 v = 28;
bytes32 r = 0x9242685bf161793cc25603c231bc2f568eb630ea16aa137d2664ac8038825608;
bytes32 s = 0x4f8ae3bd7535248d0bd448298cc2e2071e56992d0774dc340c368ae950852ada;
uint256 i;
address addr1 = ecrecover(keccak256(abi.encodePacked(foobar1)), v, r, s);
address addr2 = ecrecover(keccak256(abi.encodePacked(foobar1, foobar2)), v, r, s);
if (addr1 != addr2) {
// True
i = 674837568743979857398564869;
} else {
// False
i = 3487683476979311;
}
return i;
}
//identity is invoked here in compiler and not below
function needIdentityInvoke(uint sea) public returns (uint) {
return sea;
}
function identityFunction(int input) public returns(int out) {
assembly {
let x := mload(0x40)
mstore(x, input)
let success := call(500000000, 0x4, 100000, x, 0x20, x, 0x20)
out := mload(x)
mstore(0x40, x)
}
}
function identityTest1() public returns (uint256) {
uint256 i;
if (identityFunction(100) == 100) {
// True
i = 87426857369875698;
} else {
// False
i = 476934798798347;
}
return i;
}
}

@ -0,0 +1,23 @@
from mythril.mythril import MythrilAnalyzer, MythrilDisassembler
from mythril.ethereum import util
from mythril.solidity.soliditycontract import EVMContract
from tests import TESTDATA_INPUTS
def test_statespace_dump():
for input_file in TESTDATA_INPUTS.iterdir():
if input_file.name not in ("origin.sol.o", "suicide.sol.o"):
# It's too slow, so it's better to skip some tests.
continue
contract = EVMContract(input_file.read_text())
disassembler = MythrilDisassembler()
disassembler.contracts.append(contract)
analyzer = MythrilAnalyzer(
disassembler=disassembler,
strategy="dfs",
execution_timeout=5,
max_depth=30,
address=(util.get_indexed_address(0)),
)
analyzer.dump_statespace(contract=contract)

@ -1,5 +1,5 @@
[tox]
envlist = py35, py36
envlist = py36
[testenv]
deps =

Loading…
Cancel
Save