Merge branch 'develop' into fix/ambiguous-sigs

pull/785/head
Nikhil Parasaram 6 years ago committed by GitHub
commit 76e01a939c
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
  1. 18
      mythril/analysis/solver.py
  2. 4
      mythril/ethereum/evmcontract.py
  3. 10
      mythril/interfaces/cli.py
  4. 9
      mythril/laser/ethereum/instructions.py
  5. 11
      mythril/laser/ethereum/natives.py
  6. 31
      mythril/laser/ethereum/state/annotation.py
  7. 82
      mythril/laser/ethereum/state/calldata.py
  8. 17
      mythril/laser/ethereum/state/global_state.py
  9. 20
      mythril/laser/ethereum/state/world_state.py
  10. 3
      mythril/laser/ethereum/transaction/transaction_models.py
  11. 122
      tests/svm_test.py
  12. 57499
      tests/testdata/outputs_expected_laser_result/calls.sol.json
  13. 472
      tests/testdata/outputs_expected_laser_result/constructor_assert.sol.json
  14. 54936
      tests/testdata/outputs_expected_laser_result/environments.sol.json
  15. 61845
      tests/testdata/outputs_expected_laser_result/ether_send.sol.json
  16. 59235
      tests/testdata/outputs_expected_laser_result/exceptions.sol.json
  17. 73258
      tests/testdata/outputs_expected_laser_result/kinds_of_calls.sol.json
  18. 40884
      tests/testdata/outputs_expected_laser_result/metacoin.sol.json
  19. 11621
      tests/testdata/outputs_expected_laser_result/multi_contracts.sol.json
  20. 42097
      tests/testdata/outputs_expected_laser_result/nonascii.sol.json
  21. 24336
      tests/testdata/outputs_expected_laser_result/origin.sol.json
  22. 52771
      tests/testdata/outputs_expected_laser_result/overflow.sol.json
  23. 17652
      tests/testdata/outputs_expected_laser_result/returnvalue.sol.json
  24. 1141641
      tests/testdata/outputs_expected_laser_result/rubixi.sol.json
  25. 8420
      tests/testdata/outputs_expected_laser_result/suicide.sol.json
  26. 52771
      tests/testdata/outputs_expected_laser_result/underflow.sol.json

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

@ -37,6 +37,10 @@ class EVMContract(persistent.Persistent):
return self.disassembly.get_easm()
def get_creation_easm(self):
return self.creation_disassembly.get_easm()
def matches_expression(self, expression):
str_eval = ""

@ -364,10 +364,12 @@ def main():
print(storage)
elif args.disassemble:
easm_text = mythril.contracts[
0
].get_easm() # or mythril.disassemble(mythril.contracts[0])
sys.stdout.write(easm_text)
# or mythril.disassemble(mythril.contracts[0])
if mythril.contracts[0].code:
print("Runtime Disassembly: \n" + mythril.contracts[0].get_easm())
if mythril.contracts[0].creation_code:
print("Disassembly: \n" + mythril.contracts[0].get_creation_easm())
elif args.graph or args.fire_lasers:
if not mythril.contracts:

@ -991,8 +991,13 @@ class Instruction:
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(simplify(key_argument == index_argument)):
condition = key_argument == index_argument
condition = (
condition
if type(condition) == bool
else is_true(simplify(condition))
)
if condition:
return self._sstore_helper(
copy(global_state),
keccak_key,

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

@ -0,0 +1,31 @@
class StateAnnotation:
"""
The StateAnnotation class is used to persist information over traces. This allows modules to reason about traces
without the need to traverse the state space themselves.
"""
@property
def persist_to_world_state(self) -> bool:
"""
If this function returns true then laser will also annotate the world state.
If you want annotations to persist through different user initiated message call transactions
then this should be enabled.
The default is set to False
"""
return False
class NoCopyAnnotation(StateAnnotation):
"""
This class provides a base annotation class for annotations that shouldn't be copied on every new state.
Rather the same object should be propagated.
This is very useful if you are looking to analyze a property over multiple substates
"""
def __copy__(self):
return self
def __deepcopy__(self, _):
return self

@ -1,6 +1,19 @@
from enum import Enum
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 mythril.laser.ethereum.util import get_concrete_int
@ -32,7 +45,8 @@ class BaseCalldata:
def get_word_at(self, offset: int) -> ExprRef:
""" 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:
if isinstance(item, int) or isinstance(item, ExprRef):
@ -49,12 +63,16 @@ class BaseCalldata:
)
parts = []
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)
except Z3Exception:
raise IndexError("Invalid Calldata Slice")
return simplify(Concat(parts))
return parts
raise ValueError
@ -78,6 +96,31 @@ class ConcreteCalldata(BaseCalldata):
:param tx_id: Id of the transaction that the calldata is for.
: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
super().__init__(tx_id)
@ -102,6 +145,37 @@ class ConcreteCalldata(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):
"""
Initializes the SymbolicCalldata object

@ -1,4 +1,4 @@
from typing import Dict, Union
from typing import Dict, Union, List
from copy import copy, deepcopy
from z3 import BitVec
@ -6,6 +6,7 @@ from z3 import BitVec
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.annotation import StateAnnotation
class GlobalState:
@ -33,7 +34,7 @@ class GlobalState:
self.transaction_stack = transaction_stack if transaction_stack else []
self.op_code = ""
self.last_return_data = last_return_data
self.annotations = annotations or []
self._annotations = annotations or []
def __copy__(self) -> "GlobalState":
world_state = copy(self.world_state)
@ -47,7 +48,7 @@ class GlobalState:
mstate,
transaction_stack=transaction_stack,
last_return_data=self.last_return_data,
annotations=self.annotations,
annotations=[copy(a) for a in self._annotations],
)
@property
@ -78,3 +79,13 @@ class GlobalState:
def new_bitvec(self, name: str, size=256) -> BitVec:
transaction_id = self.current_transaction.id
return BitVec("{}_{}".format(transaction_id, name), size)
def annotate(self, annotation: StateAnnotation) -> None:
self._annotations.append(annotation)
if annotation.persist_to_world_state:
self.world_state.annotate(annotation)
@property
def annotations(self) -> List[StateAnnotation]:
return self._annotations

@ -1,7 +1,9 @@
from copy import copy
from random import randint
from typing import List
from mythril.laser.ethereum.state.account import Account
from mythril.laser.ethereum.state.annotation import StateAnnotation
class WorldState:
@ -9,13 +11,16 @@ class WorldState:
The WorldState class represents the world state as described in the yellow paper
"""
def __init__(self, transaction_sequence=None):
def __init__(
self, transaction_sequence=None, annotations: List[StateAnnotation] = None
) -> None:
"""
Constructor for the world state. Initializes the accounts record
"""
self.accounts = {}
self.node = None
self.transaction_sequence = transaction_sequence or []
self._annotations = annotations or []
def __getitem__(self, item: str) -> Account:
"""
@ -26,7 +31,11 @@ class WorldState:
return self.accounts[item]
def __copy__(self) -> "WorldState":
new_world_state = WorldState(transaction_sequence=self.transaction_sequence[:])
new_annotations = [copy(a) for a in self._annotations]
new_world_state = WorldState(
transaction_sequence=self.transaction_sequence[:],
annotations=new_annotations,
)
new_world_state.accounts = copy(self.accounts)
new_world_state.node = self.node
return new_world_state
@ -67,6 +76,13 @@ class WorldState:
new_account.storage = storage
self._put_account(new_account)
def annotate(self, annotation: StateAnnotation) -> None:
self._annotations.append(annotation)
@property
def annotations(self) -> List[StateAnnotation]:
return self._annotations
def _generate_new_address(self) -> str:
""" Generates a new address for the global state"""
while True:

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

@ -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)

File diff suppressed because it is too large Load Diff

@ -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": []
}

File diff suppressed because it is too large Load Diff

File diff suppressed because it is too large Load Diff

File diff suppressed because it is too large Load Diff

File diff suppressed because it is too large Load Diff

File diff suppressed because it is too large Load Diff

File diff suppressed because it is too large Load Diff

File diff suppressed because it is too large Load Diff

File diff suppressed because it is too large Load Diff

File diff suppressed because it is too large Load Diff

File diff suppressed because it is too large Load Diff

File diff suppressed because it is too large Load Diff

File diff suppressed because it is too large Load Diff

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