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

Merge remote-tracking branch 'origin/features/smt-abs' into features/smt-abs

Browse Source
pull/788/head
Joran Honig 6 years ago
parent c9454eedc5 1865bd2978
commit 6434dc1e33
21 changed files with 104 additions and 1699579 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. 18
      mythril/analysis/solver.py
  2. 9
      mythril/laser/ethereum/instructions.py
  3. 11
      mythril/laser/ethereum/natives.py
  4. 82
      mythril/laser/ethereum/state/calldata.py
  5. 3
      mythril/laser/ethereum/transaction/transaction_models.py
  6. 122
      tests/svm_test.py
  7. 57499
      tests/testdata/outputs_expected_laser_result/calls.sol.json
  8. 472
      tests/testdata/outputs_expected_laser_result/constructor_assert.sol.json
  9. 54936
      tests/testdata/outputs_expected_laser_result/environments.sol.json
  10. 61845
      tests/testdata/outputs_expected_laser_result/ether_send.sol.json
  11. 59235
      tests/testdata/outputs_expected_laser_result/exceptions.sol.json
  12. 73258
      tests/testdata/outputs_expected_laser_result/kinds_of_calls.sol.json
  13. 40884
      tests/testdata/outputs_expected_laser_result/metacoin.sol.json
  14. 11621
      tests/testdata/outputs_expected_laser_result/multi_contracts.sol.json
  15. 42097
      tests/testdata/outputs_expected_laser_result/nonascii.sol.json
  16. 24336
      tests/testdata/outputs_expected_laser_result/origin.sol.json
  17. 52771
      tests/testdata/outputs_expected_laser_result/overflow.sol.json
  18. 17652
      tests/testdata/outputs_expected_laser_result/returnvalue.sol.json
  19. 1141641
      tests/testdata/outputs_expected_laser_result/rubixi.sol.json
  20. 8420
      tests/testdata/outputs_expected_laser_result/suicide.sol.json
  21. 52771
      tests/testdata/outputs_expected_laser_result/underflow.sol.json

18
mythril/analysis/solver.py
Unescape View File

@ -76,26 +76,32 @@ def get_transaction_sequence(global_state, constraints):
minimize = [] minimize = []
transactions = [] transactions = []
model = None
for transaction in transaction_sequence: for transaction in transaction_sequence:
tx_id = str(transaction.id) tx_id = str(transaction.id)
if not isinstance(transaction, ContractCreationTransaction): if not isinstance(transaction, ContractCreationTransaction):
transactions.append(transaction) transactions.append(transaction)
# Constrain calldatasize # Constrain calldatasize
max_calldatasize = 5000 max_calldatasize = 5000
if max_calldatasize != None: tx_constraints.append(
tx_constraints.append( UGE(max_calldatasize, transaction.call_data.calldatasize)
UGE(max_calldatasize, transaction.call_data.calldatasize) )
)
minimize.append(transaction.call_data.calldatasize) minimize.append(transaction.call_data.calldatasize)
minimize.append(transaction.call_value)
concrete_transactions[tx_id] = tx_template.copy() concrete_transactions[tx_id] = tx_template.copy()
try:
model = get_model(tx_constraints, minimize=minimize)
break
except UnsatError:
continue
else: else:
creation_tx_ids.append(tx_id) creation_tx_ids.append(tx_id)
model = get_model(tx_constraints, minimize=minimize) if model is None:
model = get_model(tx_constraints, minimize=minimize)
for transaction in transactions: for transaction in transactions:
tx_id = str(transaction.id) tx_id = str(transaction.id)

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

@ -992,8 +992,13 @@ class Instruction:
for keccak_key in keccak_keys: for keccak_key in keccak_keys:
key_argument = keccak_function_manager.get_argument(keccak_key) key_argument = keccak_function_manager.get_argument(keccak_key)
index_argument = keccak_function_manager.get_argument(index) index_argument = keccak_function_manager.get_argument(index)
condition = key_argument == index_argument
if is_true(simplify(key_argument == index_argument)): condition = (
condition
if type(condition) == bool
else is_true(simplify(condition))
)
if condition:
return self._sstore_helper( return self._sstore_helper(
copy(global_state), copy(global_state),
keccak_key, keccak_key,

11
mythril/laser/ethereum/natives.py
Unescape View File

@ -8,7 +8,7 @@ from ethereum.utils import ecrecover_to_pub
from py_ecc.secp256k1 import N as secp256k1n from py_ecc.secp256k1 import N as secp256k1n
from rlp.utils import ALL_BYTES from rlp.utils import ALL_BYTES
from mythril.laser.ethereum.state.calldata import BaseCalldata from mythril.laser.ethereum.state.calldata import BaseCalldata, ConcreteCalldata
from mythril.laser.ethereum.util import bytearray_to_int, sha3, get_concrete_int from mythril.laser.ethereum.util import bytearray_to_int, sha3, get_concrete_int
from z3 import Concat, simplify from z3 import Concat, simplify
@ -94,10 +94,9 @@ def native_contracts(address: int, data: BaseCalldata):
""" """
functions = (ecrecover, sha256, ripemd160, identity) functions = (ecrecover, sha256, ripemd160, identity)
try: if isinstance(data, ConcreteCalldata):
data = [get_concrete_int(e) for e in data._calldata] data = data.concrete(None)
except TypeError: else:
# Symbolic calldata raise NativeContractException()
data = data._calldata
return functions[address - 1](data) return functions[address - 1](data)

82
mythril/laser/ethereum/state/calldata.py
Unescape View File

@ -1,6 +1,19 @@
from enum import Enum from enum import Enum
from typing import Union, Any from typing import Union, Any
from z3 import BitVecVal, BitVecRef, BitVec, simplify, Concat, If, ExprRef from z3 import (
BitVecVal,
BitVecRef,
BitVec,
simplify,
Concat,
If,
ExprRef,
K,
Array,
BitVecSort,
Store,
is_bv,
)
from z3.z3types import Z3Exception, Model from z3.z3types import Z3Exception, Model
from mythril.laser.ethereum.util import get_concrete_int from mythril.laser.ethereum.util import get_concrete_int
@ -32,7 +45,8 @@ class BaseCalldata:
def get_word_at(self, offset: int) -> ExprRef: def get_word_at(self, offset: int) -> ExprRef:
""" Gets word at offset""" """ Gets word at offset"""
return self[offset : offset + 32] parts = self[offset : offset + 32]
return simplify(Concat(parts))
def __getitem__(self, item: Union[int, slice]) -> Any: def __getitem__(self, item: Union[int, slice]) -> Any:
if isinstance(item, int) or isinstance(item, ExprRef): if isinstance(item, int) or isinstance(item, ExprRef):
@ -49,12 +63,16 @@ class BaseCalldata:
) )
parts = [] parts = []
while simplify(current_index != stop): while simplify(current_index != stop):
parts.append(self._load(current_index)) element = self._load(current_index)
if not isinstance(element, ExprRef):
element = BitVecVal(element, 8)
parts.append(element)
current_index = simplify(current_index + step) current_index = simplify(current_index + step)
except Z3Exception: except Z3Exception:
raise IndexError("Invalid Calldata Slice") raise IndexError("Invalid Calldata Slice")
return simplify(Concat(parts)) return parts
raise ValueError raise ValueError
@ -78,6 +96,31 @@ class ConcreteCalldata(BaseCalldata):
:param tx_id: Id of the transaction that the calldata is for. :param tx_id: Id of the transaction that the calldata is for.
:param calldata: The concrete calldata content :param calldata: The concrete calldata content
""" """
self._concrete_calldata = calldata
self._calldata = K(BitVecSort(256), BitVecVal(0, 8))
for i, element in enumerate(calldata, 0):
self._calldata = Store(self._calldata, i, element)
super().__init__(tx_id)
def _load(self, item: Union[int, ExprRef]) -> BitVecSort(8):
item = BitVecVal(item, 256) if isinstance(item, int) else item
return simplify(self._calldata[item])
def concrete(self, model: Model) -> list:
return self._concrete_calldata
@property
def size(self) -> int:
return len(self._concrete_calldata)
class BasicConcreteCalldata(BaseCalldata):
def __init__(self, tx_id: int, calldata: list):
"""
Initializes the ConcreteCalldata object, that doesn't use z3 arrays
:param tx_id: Id of the transaction that the calldata is for.
:param calldata: The concrete calldata content
"""
self._calldata = calldata self._calldata = calldata
super().__init__(tx_id) super().__init__(tx_id)
@ -102,6 +145,37 @@ class ConcreteCalldata(BaseCalldata):
class SymbolicCalldata(BaseCalldata): class SymbolicCalldata(BaseCalldata):
def __init__(self, tx_id: int):
"""
Initializes the SymbolicCalldata object
:param tx_id: Id of the transaction that the calldata is for.
"""
self._size = BitVec(str(tx_id) + "_calldatasize", 256)
self._calldata = Array(
"{}_calldata".format(tx_id), BitVecSort(256), BitVecSort(8)
)
super().__init__(tx_id)
def _load(self, item: Union[int, ExprRef]) -> Any:
item = BitVecVal(item, 256) if isinstance(item, int) else item
return simplify(If(item < self._size, simplify(self._calldata[item]), 0))
def concrete(self, model: Model) -> list:
concrete_length = get_concrete_int(model.eval(self.size, model_completion=True))
result = []
for i in range(concrete_length):
value = self._load(i)
c_value = get_concrete_int(model.eval(value, model_completion=True))
result.append(c_value)
return result
@property
def size(self) -> ExprRef:
return self._size
class BasicSymbolicCalldata(BaseCalldata):
def __init__(self, tx_id: int): def __init__(self, tx_id: int):
""" """
Initializes the SymbolicCalldata object Initializes the SymbolicCalldata object

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

@ -79,9 +79,10 @@ class BaseTransaction:
self.caller = caller self.caller = caller
self.callee_account = callee_account self.callee_account = callee_account
if call_data is None and init_call_data: if call_data is None and init_call_data:
self.call_data = ConcreteCalldata(self.id, call_data) self.call_data = SymbolicCalldata(self.id)
else: else:
self.call_data = call_data if isinstance(call_data, BaseCalldata) else None self.call_data = call_data if isinstance(call_data, BaseCalldata) else None
self.call_data_type = ( self.call_data_type = (
call_data_type call_data_type
if call_data_type is not None if call_data_type is not None

122
tests/svm_test.py
Unescape View File

@ -1,122 +0,0 @@
import json
from mythril.analysis.security import get_detection_module_hooks
from mythril.analysis.symbolic import SymExecWrapper
from mythril.analysis.callgraph import generate_graph
from mythril.ethereum.evmcontract import EVMContract
from mythril.solidity.soliditycontract import SolidityContract
from mythril.mythril import Mythril
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 import svm
from tests import (
BaseTestCase,
TESTDATA_INPUTS_CONTRACTS,
TESTDATA_OUTPUTS_EXPECTED_LASER_RESULT,
TESTDATA_OUTPUTS_CURRENT_LASER_RESULT,
)
class LaserEncoder(json.JSONEncoder):
def default(self, o):
if getattr(o, "__module__", None) == "z3.z3":
return str(o)
return str(o)
def _all_info(laser):
accounts = {}
for address, _account in laser.world_state.accounts.items():
account = _account.as_dict
account["code"] = account["code"].instruction_list
account["balance"] = str(account["balance"])
accounts[address] = account
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 {
"accounts": accounts,
"nodes": nodes,
"edges": edges,
"total_states": laser.total_states,
"max_depth": laser.max_depth,
}
class SVMTestCase(BaseTestCase):
def setUp(self):
super(SVMTestCase, self).setUp()
svm.gbl_next_uid = 0
def test_laser_result(self):
for input_file in TESTDATA_INPUTS_CONTRACTS.iterdir():
if input_file.name in ["weak_random.sol", "environments.sol"]:
continue
output_expected = TESTDATA_OUTPUTS_EXPECTED_LASER_RESULT / (
input_file.name + ".json"
)
output_current = TESTDATA_OUTPUTS_CURRENT_LASER_RESULT / (
input_file.name + ".json"
)
disassembly = SolidityContract(
str(input_file), solc_binary=Mythril._init_solc_binary("0.5.0")
).disassembly
account = Account("0x0000000000000000000000000000000000000000", disassembly)
accounts = {account.address: account}
laser = svm.LaserEVM(accounts, max_depth=22, transaction_count=1)
laser.register_hooks(
hook_type="post", hook_dict=get_detection_module_hooks()
)
laser.sym_exec(account.address)
laser_info = _all_info(laser)
output_current.write_text(
json.dumps(laser_info, cls=LaserEncoder, indent=4)
)
if not (output_expected.read_text() == output_expected.read_text()):
self.found_changed_files(input_file, output_expected, output_current)
self.assert_and_show_changed_files()
def runTest(self):
code = "0x60606040525b603c5b60006010603e565b9050593681016040523660008237602060003683856040603f5a0204f41560545760206000f35bfe5b50565b005b73c3b2ae46792547a96b9f84405e36d0e07edcd05c5b905600a165627a7a7230582062a884f947232ada573f95940cce9c8bfb7e4e14e21df5af4e884941afb55e590029"
contract = EVMContract(code)
sym = SymExecWrapper(contract, "0xd0a6E6C543bC68Db5db3A191B171A77407Ff7ccf")
html = generate_graph(sym)
self.assertTrue("0 PUSH1 0x60\\n2 PUSH1 0x40\\n4 MSTORE\\n5 JUMPDEST" in html)

57499
tests/testdata/outputs_expected_laser_result/calls.sol.json vendored
View File

File diff suppressed because it is too large Load Diff

472
tests/testdata/outputs_expected_laser_result/constructor_assert.sol.json vendored
Unescape View File

@ -1,472 +0,0 @@
{
"accounts": {
"0x0000000000000000000000000000000000000000": {
"storage": "<mythril.laser.ethereum.state.Storage object at 0x7f18fbbcab70>",
"nonce": 0,
"balance": "balance",
"code": [
{
"address": 0,
"argument": "0x80",
"opcode": "PUSH1"
},
{
"address": 2,
"argument": "0x40",
"opcode": "PUSH1"
},
{
"address": 4,
"opcode": "MSTORE"
},
{
"address": 5,
"argument": "0x00",
"opcode": "PUSH1"
},
{
"address": 7,
"opcode": "DUP1"
},
{
"address": 8,
"opcode": "REVERT"
},
{
"address": 9,
"opcode": "STOP"
}
]
}
},
"total_states": 5,
"nodes": {
"933": {
"contract_name": "unknown",
"flags": "NodeFlags()",
"constraints": [],
"function_name": "unknown",
"start_addr": 0,
"uid": 933,
"states": [
{
"accounts": "dict_keys(['0x0000000000000000000000000000000000000000'])",
"mstate": {
"gas": 10000000,
"memory": [],
"pc": 0,
"memsize": 0,
"stack": []
},
"environment": {
"sender": "caller",
"callvalue": "call_value",
"origin": "origin",
"active_account": "0x0000000000000000000000000000000000000000",
"gasprice": "gas_price",
"calldata": [],
"calldata_type": "CalldataType.SYMBOLIC"
}
},
{
"accounts": "dict_keys(['0x0000000000000000000000000000000000000000'])",
"mstate": {
"gas": 10000000,
"memory": [],
"pc": 1,
"memsize": 0,
"stack": [
"128"
]
},
"environment": {
"sender": "caller",
"callvalue": "call_value",
"origin": "origin",
"active_account": "0x0000000000000000000000000000000000000000",
"gasprice": "gas_price",
"calldata": [],
"calldata_type": "CalldataType.SYMBOLIC"
}
},
{
"accounts": "dict_keys(['0x0000000000000000000000000000000000000000'])",
"mstate": {
"gas": 10000000,
"memory": [],
"pc": 2,
"memsize": 0,
"stack": [
"128",
"64"
]
},
"environment": {
"sender": "caller",
"callvalue": "call_value",
"origin": "origin",
"active_account": "0x0000000000000000000000000000000000000000",
"gasprice": "gas_price",
"calldata": [],
"calldata_type": "CalldataType.SYMBOLIC"
}
},
{
"accounts": "dict_keys(['0x0000000000000000000000000000000000000000'])",
"mstate": {
"gas": 10000000,
"memory": [
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
128
],
"pc": 3,
"memsize": 96,
"stack": []
},
"environment": {
"sender": "caller",
"callvalue": "call_value",
"origin": "origin",
"active_account": "0x0000000000000000000000000000000000000000",
"gasprice": "gas_price",
"calldata": [],
"calldata_type": "CalldataType.SYMBOLIC"
}
},
{
"accounts": "dict_keys(['0x0000000000000000000000000000000000000000'])",
"mstate": {
"gas": 10000000,
"memory": [
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
128
],
"pc": 4,
"memsize": 96,
"stack": [
"0"
]
},
"environment": {
"sender": "caller",
"callvalue": "call_value",
"origin": "origin",
"active_account": "0x0000000000000000000000000000000000000000",
"gasprice": "gas_price",
"calldata": [],
"calldata_type": "CalldataType.SYMBOLIC"
}
},
{
"accounts": "dict_keys(['0x0000000000000000000000000000000000000000'])",
"mstate": {
"gas": 10000000,
"memory": [
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
0,
128
],
"pc": 5,
"memsize": 96,
"stack": [
"0",
"0"
]
},
"environment": {
"sender": "caller",
"callvalue": "call_value",
"origin": "origin",
"active_account": "0x0000000000000000000000000000000000000000",
"gasprice": "gas_price",
"calldata": [],
"calldata_type": "CalldataType.SYMBOLIC"
}
}
]
}
},
"max_depth": 22,
"edges": []
}

54936
tests/testdata/outputs_expected_laser_result/environments.sol.json vendored
View File

File diff suppressed because it is too large Load Diff

61845
tests/testdata/outputs_expected_laser_result/ether_send.sol.json vendored
View File

File diff suppressed because it is too large Load Diff

59235
tests/testdata/outputs_expected_laser_result/exceptions.sol.json vendored
View File

File diff suppressed because it is too large Load Diff

73258
tests/testdata/outputs_expected_laser_result/kinds_of_calls.sol.json vendored
View File

File diff suppressed because it is too large Load Diff

40884
tests/testdata/outputs_expected_laser_result/metacoin.sol.json vendored
View File

File diff suppressed because it is too large Load Diff

11621
tests/testdata/outputs_expected_laser_result/multi_contracts.sol.json vendored
View File

File diff suppressed because it is too large Load Diff

42097
tests/testdata/outputs_expected_laser_result/nonascii.sol.json vendored
View File

File diff suppressed because it is too large Load Diff

24336
tests/testdata/outputs_expected_laser_result/origin.sol.json vendored
View File

File diff suppressed because it is too large Load Diff

52771
tests/testdata/outputs_expected_laser_result/overflow.sol.json vendored
View File

File diff suppressed because it is too large Load Diff

17652
tests/testdata/outputs_expected_laser_result/returnvalue.sol.json vendored
View File

File diff suppressed because it is too large Load Diff

1141641
tests/testdata/outputs_expected_laser_result/rubixi.sol.json vendored
View File

File diff suppressed because it is too large Load Diff

8420
tests/testdata/outputs_expected_laser_result/suicide.sol.json vendored
View File

File diff suppressed because it is too large Load Diff

52771
tests/testdata/outputs_expected_laser_result/underflow.sol.json vendored
View File

File diff suppressed because it is too large Load Diff
Write Preview
Loading…
Cancel
Save