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

Add array based implementation of calldata (#778)

Browse Source 
* mythril/laser/ethereum/state: add array based implementation

* Create symbolic calldata

* remove debug statement

* Return the concrete calldata, and adapt natives to new calldata pattern

* remove debugging statement from test

* Move simplifies and remove clean

* move simplify to expected place

* remove unused test: svm_test.py
pull/792/head
JoranHonig 6 years ago committed by GitHub
parent 5dd544d301
commit e661eac348
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
19 changed files with 85 additions and 1699571 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. 11
      mythril/laser/ethereum/natives.py
  2. 82
      mythril/laser/ethereum/state/calldata.py
  3. 3
      mythril/laser/ethereum/transaction/transaction_models.py
  4. 122
      tests/svm_test.py
  5. 57499
      tests/testdata/outputs_expected_laser_result/calls.sol.json
  6. 472
      tests/testdata/outputs_expected_laser_result/constructor_assert.sol.json
  7. 54936
      tests/testdata/outputs_expected_laser_result/environments.sol.json
  8. 61845
      tests/testdata/outputs_expected_laser_result/ether_send.sol.json
  9. 59235
      tests/testdata/outputs_expected_laser_result/exceptions.sol.json
  10. 73258
      tests/testdata/outputs_expected_laser_result/kinds_of_calls.sol.json
  11. 40884
      tests/testdata/outputs_expected_laser_result/metacoin.sol.json
  12. 11621
      tests/testdata/outputs_expected_laser_result/multi_contracts.sol.json
  13. 42097
      tests/testdata/outputs_expected_laser_result/nonascii.sol.json
  14. 24336
      tests/testdata/outputs_expected_laser_result/origin.sol.json
  15. 52771
      tests/testdata/outputs_expected_laser_result/overflow.sol.json
  16. 17652
      tests/testdata/outputs_expected_laser_result/returnvalue.sol.json
  17. 1141641
      tests/testdata/outputs_expected_laser_result/rubixi.sol.json
  18. 8420
      tests/testdata/outputs_expected_laser_result/suicide.sol.json
  19. 52771
      tests/testdata/outputs_expected_laser_result/underflow.sol.json

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

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

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

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

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

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