|
|
@ -1,7 +1,10 @@ |
|
|
|
"""This module contains analysis module helpers to solve path constraints.""" |
|
|
|
"""This module contains analysis module helpers to solve path constraints.""" |
|
|
|
|
|
|
|
from typing import Dict, List |
|
|
|
from z3 import sat, unknown, FuncInterp |
|
|
|
from z3 import sat, unknown, FuncInterp |
|
|
|
import z3 |
|
|
|
import z3 |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
from mythril.laser.ethereum.state.global_state import GlobalState |
|
|
|
|
|
|
|
from mythril.laser.ethereum.transaction import BaseTransaction |
|
|
|
from mythril.laser.smt import simplify, UGE, Optimize, symbol_factory |
|
|
|
from mythril.laser.smt import simplify, UGE, Optimize, symbol_factory |
|
|
|
from mythril.laser.ethereum.time_handler import time_handler |
|
|
|
from mythril.laser.ethereum.time_handler import time_handler |
|
|
|
from mythril.exceptions import UnsatError |
|
|
|
from mythril.exceptions import UnsatError |
|
|
@ -74,7 +77,7 @@ def pretty_print_model(model): |
|
|
|
return ret |
|
|
|
return ret |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
def get_transaction_sequence(global_state, constraints): |
|
|
|
def get_transaction_sequence(global_state: GlobalState, constraints) -> Dict[str, List[Dict[str, str]]]: |
|
|
|
"""Generate concrete transaction sequence. |
|
|
|
"""Generate concrete transaction sequence. |
|
|
|
|
|
|
|
|
|
|
|
:param global_state: GlobalState to generate transaction sequence for |
|
|
|
:param global_state: GlobalState to generate transaction sequence for |
|
|
@ -85,17 +88,24 @@ def get_transaction_sequence(global_state, constraints): |
|
|
|
|
|
|
|
|
|
|
|
# gaslimit & gasprice don't exist yet |
|
|
|
# gaslimit & gasprice don't exist yet |
|
|
|
tx_template = { |
|
|
|
tx_template = { |
|
|
|
"calldata": None, |
|
|
|
"origin": None, |
|
|
|
"call_value": None, |
|
|
|
"value": None, |
|
|
|
"caller": "0xCA11EDEADBEEF37E636E6CA11EDEADBEEFCA11ED", |
|
|
|
"address": None, |
|
|
|
} |
|
|
|
"input": None, |
|
|
|
|
|
|
|
"gasLimit": "<GAS_LIMIT>", |
|
|
|
concrete_transactions = {} |
|
|
|
"blockCoinbase": "<ARBITRARY_COINBASE>", |
|
|
|
|
|
|
|
"blockDifficulty": "<ARBITRARY_DIFFICULTY>", |
|
|
|
|
|
|
|
"blockGasLimit": "<ARBITRARY_GAS_LIMIT>", |
|
|
|
|
|
|
|
"blockNumber": "<ARBITRARY_BLOCKNUMBER>", |
|
|
|
|
|
|
|
"blockTime": "<ARBITRARY_BLOCKTIME>" |
|
|
|
|
|
|
|
} # type: Dict[str, str] |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
concrete_transactions = [] |
|
|
|
creation_tx_ids = [] |
|
|
|
creation_tx_ids = [] |
|
|
|
tx_constraints = constraints.copy() |
|
|
|
tx_constraints = constraints.copy() |
|
|
|
minimize = [] |
|
|
|
minimize = [] |
|
|
|
|
|
|
|
|
|
|
|
transactions = [] |
|
|
|
transactions = [] # type: List[BaseTransaction] |
|
|
|
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): |
|
|
@ -109,8 +119,6 @@ def get_transaction_sequence(global_state, constraints): |
|
|
|
minimize.append(transaction.call_data.calldatasize) |
|
|
|
minimize.append(transaction.call_data.calldatasize) |
|
|
|
minimize.append(transaction.call_value) |
|
|
|
minimize.append(transaction.call_value) |
|
|
|
|
|
|
|
|
|
|
|
concrete_transactions[tx_id] = tx_template.copy() |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
else: |
|
|
|
else: |
|
|
|
creation_tx_ids.append(tx_id) |
|
|
|
creation_tx_ids.append(tx_id) |
|
|
|
|
|
|
|
|
|
|
@ -118,20 +126,28 @@ def get_transaction_sequence(global_state, constraints): |
|
|
|
|
|
|
|
|
|
|
|
for transaction in transactions: |
|
|
|
for transaction in transactions: |
|
|
|
tx_id = str(transaction.id) |
|
|
|
tx_id = str(transaction.id) |
|
|
|
|
|
|
|
concrete_transaction = tx_template.copy() |
|
|
|
concrete_transactions[tx_id]["calldata"] = "0x" + "".join( |
|
|
|
concrete_transaction["input"] = "0x" + "".join( |
|
|
|
[ |
|
|
|
[ |
|
|
|
hex(b)[2:] if len(hex(b)) % 2 == 0 else "0" + hex(b)[2:] |
|
|
|
hex(b)[2:] if len(hex(b)) % 2 == 0 else "0" + hex(b)[2:] |
|
|
|
for b in transaction.call_data.concrete(model) |
|
|
|
for b in transaction.call_data.concrete(model) |
|
|
|
] |
|
|
|
] |
|
|
|
) |
|
|
|
) |
|
|
|
|
|
|
|
|
|
|
|
concrete_transactions[tx_id]["call_value"] = ( |
|
|
|
concrete_transaction["value"] = ( |
|
|
|
"0x%x" |
|
|
|
"0x%x" |
|
|
|
% model.eval(transaction.call_value.raw, model_completion=True).as_long() |
|
|
|
% model.eval(transaction.call_value.raw, model_completion=True).as_long() |
|
|
|
) |
|
|
|
) |
|
|
|
concrete_transactions[tx_id]["caller"] = "0x" + ( |
|
|
|
concrete_transaction["origin"] = "0x" + ( |
|
|
|
"%x" % model.eval(transaction.caller.raw, model_completion=True).as_long() |
|
|
|
"%x" % model.eval(transaction.caller.raw, model_completion=True).as_long() |
|
|
|
).zfill(40) |
|
|
|
).zfill(40) |
|
|
|
|
|
|
|
concrete_transaction["address"] = ( |
|
|
|
|
|
|
|
"%s" % transaction.callee_account.address |
|
|
|
|
|
|
|
) |
|
|
|
|
|
|
|
concrete_transactions.append(concrete_transaction) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
steps = { |
|
|
|
|
|
|
|
"steps": concrete_transactions |
|
|
|
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
|
|
return concrete_transactions |
|
|
|
return steps |
|
|
|