Merge branch 'develop' into memory_refactor

pull/764/head
Nathan 6 years ago committed by GitHub
commit 7ff3b3f8ab
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
  1. 98
      mythril/analysis/modules/deprecated_ops.py
  2. 4
      mythril/analysis/security.py
  3. 18
      mythril/analysis/solver.py
  4. 3
      mythril/analysis/symbolic.py
  5. 2
      mythril/disassembler/disassembly.py
  6. 4
      mythril/ethereum/evmcontract.py
  7. 6
      mythril/ethereum/util.py
  8. 10
      mythril/interfaces/cli.py
  9. 10
      mythril/laser/ethereum/instructions.py
  10. 11
      mythril/laser/ethereum/natives.py
  11. 31
      mythril/laser/ethereum/state/annotation.py
  12. 82
      mythril/laser/ethereum/state/calldata.py
  13. 17
      mythril/laser/ethereum/state/global_state.py
  14. 20
      mythril/laser/ethereum/state/world_state.py
  15. 3
      mythril/laser/ethereum/transaction/transaction_models.py
  16. 73
      mythril/laser/smt/__init__.py
  17. 128
      mythril/laser/smt/bitvec.py
  18. 44
      mythril/laser/smt/bool.py
  19. 32
      mythril/laser/smt/expression.py
  20. 16
      mythril/mythril.py
  21. 55
      mythril/support/signatures.py
  22. 10
      tests/__init__.py
  23. 4
      tests/mythril_dir/config.ini
  24. BIN
      tests/mythril_dir/signatures.db.example
  25. 122
      tests/svm_test.py
  26. 12
      tests/testdata/outputs_expected/kinds_of_calls.sol.o.json
  27. 12
      tests/testdata/outputs_expected/kinds_of_calls.sol.o.markdown
  28. 10
      tests/testdata/outputs_expected/kinds_of_calls.sol.o.text
  29. 2
      tests/testdata/outputs_expected/origin.sol.o.json
  30. 2
      tests/testdata/outputs_expected/origin.sol.o.markdown
  31. 2
      tests/testdata/outputs_expected/origin.sol.o.text
  32. 57499
      tests/testdata/outputs_expected_laser_result/calls.sol.json
  33. 472
      tests/testdata/outputs_expected_laser_result/constructor_assert.sol.json
  34. 54936
      tests/testdata/outputs_expected_laser_result/environments.sol.json
  35. 61845
      tests/testdata/outputs_expected_laser_result/ether_send.sol.json
  36. 59235
      tests/testdata/outputs_expected_laser_result/exceptions.sol.json
  37. 73258
      tests/testdata/outputs_expected_laser_result/kinds_of_calls.sol.json
  38. 40884
      tests/testdata/outputs_expected_laser_result/metacoin.sol.json
  39. 11621
      tests/testdata/outputs_expected_laser_result/multi_contracts.sol.json
  40. 42097
      tests/testdata/outputs_expected_laser_result/nonascii.sol.json
  41. 24336
      tests/testdata/outputs_expected_laser_result/origin.sol.json
  42. 52771
      tests/testdata/outputs_expected_laser_result/overflow.sol.json
  43. 17652
      tests/testdata/outputs_expected_laser_result/returnvalue.sol.json
  44. 1141641
      tests/testdata/outputs_expected_laser_result/rubixi.sol.json
  45. 8420
      tests/testdata/outputs_expected_laser_result/suicide.sol.json
  46. 52771
      tests/testdata/outputs_expected_laser_result/underflow.sol.json

@ -1,64 +1,72 @@
from mythril.analysis.report import Issue
from mythril.analysis.swc_data import TX_ORIGIN_USAGE
from mythril.analysis.swc_data import DEPRICATED_FUNCTIONS_USAGE
from mythril.analysis.modules.base import DetectionModule
from mythril.laser.ethereum.state.global_state import GlobalState
import logging
DESCRIPTION = """
Check for usage of deprecated opcodes
"""
MODULE DESCRIPTION:
Check for constraints on tx.origin (i.e., access to some functionality is restricted to a specific origin).
"""
def _analyze_state(state):
node = state.node
instruction = state.get_current_instruction()
if instruction["opcode"] == "ORIGIN":
logging.debug("ORIGIN in function " + node.function_name)
title = "Use of tx.origin"
description = (
"The function `{}` retrieves the transaction origin (tx.origin) using the ORIGIN opcode. "
"Use msg.sender instead.\nSee also: "
"https://solidity.readthedocs.io/en/develop/security-considerations.html#tx-origin".format(
node.function_name
)
)
swc_id = DEPRICATED_FUNCTIONS_USAGE
elif instruction["opcode"] == "CALLCODE":
logging.debug("CALLCODE in function " + node.function_name)
title = "Use of callcode"
description = (
"The function `{}` uses callcode. Callcode does not persist sender or value over the call. "
"Use delegatecall instead.".format(node.function_name)
)
swc_id = DEPRICATED_FUNCTIONS_USAGE
issue = Issue(
contract=node.contract_name,
function_name=node.function_name,
address=instruction["address"],
title=title,
bytecode=state.environment.code.bytecode,
_type="Warning",
swc_id=swc_id,
description=description,
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
)
return [issue]
class DeprecatedOperationsModule(DetectionModule):
def __init__(self):
super().__init__(
name="Deprecated Operations",
swc_id=TX_ORIGIN_USAGE,
hooks=["ORIGIN"],
description=(
"Check for constraints on tx.origin (i.e., access to some "
"functionality is restricted to a specific origin)."
),
swc_id=DEPRICATED_FUNCTIONS_USAGE,
hooks=["ORIGIN", "CALLCODE"],
description=(DESCRIPTION),
entrypoint="callback",
)
self._issues = []
def execute(self, statespace):
logging.debug("Executing module: DEPRECATED OPCODES")
issues = []
for k in statespace.nodes:
node = statespace.nodes[k]
for state in node.states:
instruction = state.get_current_instruction()
if instruction["opcode"] == "ORIGIN":
description = (
"The function `{}` retrieves the transaction origin (tx.origin) using the ORIGIN opcode. "
"Use msg.sender instead.\nSee also: "
"https://solidity.readthedocs.io/en/develop/security-considerations.html#tx-origin".format(
node.function_name
)
)
issue = Issue(
contract=node.contract_name,
function_name=node.function_name,
address=instruction["address"],
title="Use of tx.origin",
bytecode=state.environment.code.bytecode,
_type="Warning",
swc_id=TX_ORIGIN_USAGE,
description=description,
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
)
issues.append(issue)
def execute(self, state: GlobalState):
self._issues.extend(_analyze_state(state))
return self.issues
return issues
@property
def issues(self):
return self._issues
detector = DeprecatedOperationsModule()

@ -15,9 +15,9 @@ def reset_callback_modules():
module.detector._issues = []
def get_detection_module_hooks():
def get_detection_module_hooks(modules):
hook_dict = defaultdict(list)
_modules = get_detection_modules(entrypoint="callback")
_modules = get_detection_modules(entrypoint="callback", include_modules=modules)
for module in _modules:
for op_code in map(lambda x: x.upper(), module.detector.hooks):
if op_code in OPCODE_LIST:

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

@ -28,6 +28,7 @@ class SymExecWrapper:
execution_timeout=None,
create_timeout=None,
transaction_count=2,
modules=(),
):
if strategy == "dfs":
@ -60,7 +61,7 @@ class SymExecWrapper:
transaction_count=transaction_count,
)
self.laser.register_hooks(
hook_type="pre", hook_dict=get_detection_module_hooks()
hook_type="pre", hook_dict=get_detection_module_hooks(modules)
)
if isinstance(contract, SolidityContract):

@ -73,7 +73,7 @@ def get_function_info(
function_names = signature_database.get(function_hash)
if len(function_names) > 1:
# In this case there was an ambiguous result
function_name = "**ambiguous** {}".format(function_names[0])
function_name = "[{}] (ambiguous)".format(", ".join(function_names))
elif len(function_names) == 1:
function_name = function_names[0]
else:

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

@ -78,9 +78,11 @@ def solc_exists(version):
os.environ.get("HOME", str(Path.home())),
".py-solc/solc-v" + version,
"bin/solc",
), # py-solc setup
"/usr/bin/solc", # Ubuntu PPA setup
) # py-solc setup
]
if version.startswith("0.5"):
# Temporary fix to support v0.5.x with Ubuntu PPA setup
solc_binaries.append("/usr/bin/solc")
for solc_path in solc_binaries:
if os.path.exists(solc_path):
return solc_path

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

@ -49,6 +49,7 @@ from mythril.laser.ethereum.transaction import (
TransactionStartSignal,
ContractCreationTransaction,
)
from mythril.support.loader import DynLoader
from mythril.analysis.solver import get_model
@ -986,8 +987,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

@ -0,0 +1,73 @@
from mythril.laser.smt.bitvec import BitVec
from mythril.laser.smt.expression import Expression
from mythril.laser.smt.bool import Bool
import z3
class SymbolFactory:
"""
A symbol factory provides a default interface for all the components of mythril to create symbols
"""
@staticmethod
def BitVecVal(value: int, size: int, annotations=None):
"""
Creates a new bit vector with a concrete value
:param value: The concrete value to set the bit vector to
:param size: The size of the bit vector
:param annotations: The annotations to initialize the bit vector with
:return: The freshly created bit vector
"""
raise NotImplementedError()
@staticmethod
def BitVecSym(name: str, size: int, annotations=None):
"""
Creates a new bit vector with a symbolic value
:param name: The name of the symbolic bit vector
:param size: The size of the bit vector
:param annotations: The annotations to initialize the bit vector with
:return: The freshly created bit vector
"""
raise NotImplementedError()
class _SmtSymbolFactory(SymbolFactory):
"""
An implementation of a SymbolFactory that creates symbols using
the classes in: mythril.laser.smt
"""
@staticmethod
def BitVecVal(value: int, size: int, annotations=None):
""" Creates a new bit vector with a concrete value """
raw = z3.BitVecVal(value, size)
return BitVec(raw, annotations)
@staticmethod
def BitVecSym(name: str, size: int, annotations=None):
""" Creates a new bit vector with a symbolic value """
raw = z3.BitVec(name, size)
return BitVec(raw, annotations)
class _Z3SymbolFactory(SymbolFactory):
"""
An implementation of a SymbolFactory that directly returns
z3 symbols
"""
@staticmethod
def BitVecVal(value: int, size: int, annotations=None):
""" Creates a new bit vector with a concrete value """
return z3.BitVecVal(value, size)
@staticmethod
def BitVecSym(name: str, size: int, annotations=None):
""" Creates a new bit vector with a symbolic value """
return z3.BitVec(name, size)
# This is the instance that other parts of mythril should use
symbol_factory = _Z3SymbolFactory()

@ -0,0 +1,128 @@
import z3
from mythril.laser.smt.expression import Expression
from mythril.laser.smt.bool import Bool
# fmt: off
class BitVec(Expression):
"""
Bit vector symbol
"""
def __init__(self, raw, annotations=None):
super().__init__(raw, annotations)
@property
def symbolic(self):
""" Returns whether this symbol doesn't have a concrete value """
self.simplify()
return not isinstance(self.raw, z3.BitVecNumRef)
@property
def value(self):
""" Returns the value of this symbol if concrete, otherwise None"""
if self.symbolic:
return None
assert isinstance(self.raw, z3.BitVecNumRef)
return self.raw.as_long()
def __add__(self, other: "BV") -> "BV":
""" Create an addition expression """
union = self.annotations + other.annotations
return BitVec(self.raw + other.raw, annotations=union)
def __sub__(self, other: "BV") -> "BV":
""" Create a subtraction expression """
union = self.annotations + other.annotations
return BitVec(self.raw - other.raw, annotations=union)
def __mul__(self, other: "BV") -> "BV":
""" Create a multiplication expression """
union = self.annotations + other.annotations
return BitVec(self.raw * other.raw, annotations=union)
def __truediv__(self, other: "BV") -> "BV":
""" Create a signed division expression """
union = self.annotations + other.annotations
return BitVec(self.raw / other.raw, annotations=union)
def __and__(self, other: "BV") -> "BV":
""" Create an and expression """
union = self.annotations + other.annotations
return BitVec(self.raw & other.raw, annotations=union)
def __or__(self, other: "BV") -> "BV":
""" Create an or expression """
union = self.annotations + other.annotations
return BitVec(self.raw | other.raw, annotations=union)
def __xor__(self, other: "BV") -> "BV":
""" Create a xor expression """
union = self.annotations + other.annotations
return BitVec(self.raw ^ other.raw, annotations=union)
def __lt__(self, other: "BV") -> Bool:
""" Create a signed less than expression """
union = self.annotations + other.annotations
return Bool(self.raw < other.raw, annotations=union)
def __gt__(self, other: "BV") -> Bool:
""" Create a signed greater than expression """
union = self.annotations + other.annotations
return Bool(self.raw < other.raw, annotations=union)
def __eq__(self, other: "BV") -> Bool:
""" Create an equality expression """
union = self.annotations + other.annotations
return Bool(self.raw == other.raw, annotations=union)
def If(a: Bool, b: BitVec, c: BitVec):
""" Create an if-then-else expression """
union = a.annotations + b.annotations + c.annotations
return BitVec(z3.If(a, b, c), union)
def UGT(a: BitVec, b: BitVec) -> Bool:
""" Create an unsigned greater than expression """
annotations = a.annotations + b.annotations
return Bool(z3.UGT(a, b), annotations)
def ULT(a: BitVec, b: BitVec) -> Bool:
""" Create an unsigned less than expression """
annotations = a.annotations + b.annotations
return Bool(z3.ULT(a, b), annotations)
def Concat(*args) -> BitVec:
""" Create a concatenation expression """
nraw = z3.Concat([a.raw for a in args])
annotations = []
for bv in args:
annotations += bv.annotations
return BitVec(nraw, annotations)
def Extract(high: int, low: int, bv: BitVec) -> BitVec:
""" Create an extract expression"""
return BitVec(z3.Extract(high, low, bv.raw), annotations=bv.annotations)
def URem(a: BitVec, b: BitVec) -> BitVec:
""" Create an unsigned remainder expression"""
union = a.annotations + b.annotations
return BitVec(z3.URem(a.raw, b.raw), annotations=union)
def SRem(a: BitVec, b: BitVec) -> BitVec:
""" Create a signed remainder expression"""
union = a.annotations + b.annotations
return BitVec(z3.SRem(a.raw, b.raw), annotations=union)
def UDiv(a: BitVec, b: BitVec) -> BitVec:
""" Create an unsigned division expression """
union = a.annotations + b.annotations
return BitVec(z3.UDiv(a.raw, b.raw), annotations=union)

@ -0,0 +1,44 @@
import z3
from typing import Union
from mythril.laser.smt.expression import Expression
# fmt: off
class Bool(Expression):
"""
This is a Bool expression
"""
@property
def is_false(self) -> bool:
""" Specifies whether this variable can be simplified to false"""
self.simplify()
return z3.is_false(self.raw)
@property
def is_true(self) -> bool:
""" Specifies whether this variable can be simplified to true"""
self.simplify()
return z3.is_true(self.raw)
@property
def value(self) -> Union[bool, None]:
""" Returns the concrete value of this bool if concrete, otherwise None"""
if self.is_true:
return True
elif self.is_false:
return False
else:
return None
def is_false(a: Bool) -> bool:
""" Returns whether the provided bool can be simplified to false"""
return is_false(a)
def is_true(a: Bool) -> bool:
""" Returns whether the provided bool can be simplified to true"""
return is_true(a)

@ -0,0 +1,32 @@
import z3
class Expression:
"""
This is the base symbol class and maintains functionality for simplification and annotations
"""
def __init__(self, raw, annotations=None):
self.raw = raw
self._annotations = annotations or []
@property
def annotations(self):
""" Gets the annotations for this expression """
return self._annotations
def annotate(self, annotation):
""" Annotates this expression with the given annotation"""
if isinstance(annotation, list):
self._annotations += annotation
else:
self._annotations.append(annotation)
def simplify(self):
""" Simplifies this expression """
self.raw = z3.simplify(self.raw)
def simplify(expression: Expression):
""" Simplifies the expression """
expression.simplify()

@ -17,6 +17,7 @@ from solc.exceptions import SolcError
import solc
from configparser import ConfigParser
import platform
from shutil import copyfile
from mythril.ethereum import util
from mythril.ethereum.evmcontract import EVMContract
@ -116,11 +117,18 @@ class Mythril(object):
except KeyError:
mythril_dir = os.path.join(os.path.expanduser("~"), ".mythril")
# Initialize data directory and signature database
if not os.path.exists(mythril_dir):
# Initialize data directory
logging.info("Creating mythril data directory")
os.mkdir(mythril_dir)
db_path = str(Path(mythril_dir) / "signatures.db")
if not os.path.exists(db_path):
# if the default mythril dir doesn't contain a signature DB
# initialize it with the default one from the project root
parent_dir = Path(__file__).parent.parent
copyfile(str(parent_dir / "signatures.db"), db_path)
return mythril_dir
def _init_config(self):
@ -227,6 +235,9 @@ class Mythril(object):
else:
try:
solc.install_solc("v" + version)
solc_binary = util.solc_exists(version)
if not solc_binary:
raise SolcError()
except SolcError:
raise CriticalError(
"There was an error when trying to install the specified solc version"
@ -483,6 +494,7 @@ class Mythril(object):
execution_timeout=execution_timeout,
create_timeout=create_timeout,
transaction_count=transaction_count,
modules=modules,
)
issues = fire_lasers(sym, modules)

@ -6,12 +6,42 @@ import os
import time
import logging
import sqlite3
import multiprocessing
import functools
from typing import List
from collections import defaultdict
from subprocess import Popen, PIPE
from mythril.exceptions import CompilerError
lock = multiprocessing.Lock()
def synchronized(sync_lock):
""" Synchronization decorator """
def wrapper(f):
@functools.wraps(f)
def inner_wrapper(*args, **kw):
with sync_lock:
return f(*args, **kw)
return inner_wrapper
return wrapper
class Singleton(type):
_instances = {}
@synchronized(lock)
def __call__(cls, *args, **kwargs):
if cls not in cls._instances:
cls._instances[cls] = super(Singleton, cls).__call__(*args, **kwargs)
return cls._instances[cls]
try:
# load if available but do not fail
import ethereum_input_decoder
@ -24,7 +54,7 @@ except ImportError:
class SQLiteDB(object):
"""
Simple CM for sqlite3 databases. Commits everything at exit.
Simple context manager for sqlite3 databases. Commits everything at exit.
"""
def __init__(self, path):
@ -45,11 +75,15 @@ class SQLiteDB(object):
return "<SQLiteDB path={}>".format(self.path)
class SignatureDB(object):
class SignatureDB(object, metaclass=Singleton):
def __init__(self, enable_online_lookup: bool = False, path: str = None) -> None:
self.enable_online_lookup = enable_online_lookup
self.online_lookup_miss = set()
self.online_lookup_timeout = 0
# if we're analysing a Solidity file, store its hashes
# here to prevent unnecessary lookups
self.solidity_sigs = defaultdict(list)
if path is None:
self.path = os.environ.get("MYTHRIL_DIR") or os.path.join(
os.path.expanduser("~"), ".mythril"
@ -116,6 +150,12 @@ class SignatureDB(object):
"""
byte_sig = self._normalize_byte_sig(byte_sig)
# check if we have any Solidity signatures to look up
text_sigs = self.solidity_sigs.get(byte_sig)
if text_sigs is not None:
return text_sigs
# try lookup in the local DB
with SQLiteDB(self.path) as cur:
cur.execute("SELECT text_sig FROM signatures WHERE byte_sig=?", (byte_sig,))
@ -156,7 +196,6 @@ class SignatureDB(object):
:param file_path: solidity source code file path
:return:
"""
sigs = {}
cmd = [solc_binary, "--hashes", file_path]
if solc_args:
cmd.extend(solc_args.split())
@ -184,12 +223,16 @@ class SignatureDB(object):
for line in stdout:
# the ':' need not be checked but just to be sure
if all(map(lambda x: x in line, ["(", ")", ":"])):
sigs["0x" + line.split(":")[0]] = [line.split(":")[1].strip()]
solc_bytes = "0x" + line.split(":")[0]
solc_text = line.split(":")[1].strip()
self.solidity_sigs[solc_bytes].append(solc_text)
logging.debug("Signatures: found %d signatures after parsing" % len(sigs))
logging.debug(
"Signatures: found %d signatures after parsing" % len(self.solidity_sigs)
)
# update DB with what we've found
for byte_sig, text_sigs in sigs.items():
for byte_sig, text_sigs in self.solidity_sigs.items():
for text_sig in text_sigs:
self.add(byte_sig, text_sig)

@ -18,16 +18,6 @@ MYTHRIL_DIR = TESTS_DIR / "mythril_dir"
class BaseTestCase(TestCase):
def setUp(self):
self.changed_files = []
self.ori_mythril_dir = os.environ.get("MYTHRIL_DIR", "")
os.environ["MYTHRIL_DIR"] = str(MYTHRIL_DIR)
shutil.copyfile(
str(MYTHRIL_DIR / "signatures.db.example"),
str(MYTHRIL_DIR / "signatures.db"),
)
def tearDown(self):
os.environ["MYTHRIL_DIR"] = self.ori_mythril_dir
os.remove(str(MYTHRIL_DIR / "signatures.db"))
def compare_files_error_message(self):
message = "Following output files are changed, compare them manually to see differences: \n"

@ -1,4 +0,0 @@
[defaults]
leveldb_dir = /Users/bernhardmueller/Library/Ethereum/geth/chaindata
dynamic_loading = infura

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

@ -1,6 +1,18 @@
{
"error": null,
"issues": [
{
"address": 618,
"contract": "Unknown",
"debug": "<DEBUG-DATA>",
"description": "The function `_function_0x141f32ff` uses callcode. Callcode does
"function": "_function_0x141f32ff",
"max_gas_used": 1141,
"min_gas_used": 389,
"swc-id": "111",
"title": "Use of callcode",
"type": "Warning"
},
{
"address": 626,
"contract": "Unknown",

@ -1,5 +1,17 @@
# Analysis results for test-filename.sol
## Use of callcode
- SWC ID: 111
- Type: Warning
- Contract: Unknown
- Function name: `_function_0x141f32ff`
- PC address: 618
- Estimated Gas Usage: 389 - 1141
### Description
The function `_function_0x141f32ff` uses callcode. Callcode does not persist sender or value over the call. Use delegatecall instead.
## Unchecked CALL return value
- SWC ID: 104
- Type: Informational

@ -1,3 +1,13 @@
==== Use of callcode ====
SWC ID: 111
Type: Warning
Contract: Unknown
Function name: _function_0x141f32ff
PC address: 618
Estimated Gas Usage: 389 - 1141
The function `_function_0x141f32ff` uses callcode. Callcode does not persist sender or value over the call. Use delegatecall instead.
--------------------
==== Unchecked CALL return value ====
SWC ID: 104
Type: Informational

@ -9,7 +9,7 @@
"function": "transferOwnership(address)",
"max_gas_used": 1051,
"min_gas_used": 626,
"swc-id": "115",
"swc-id": "111",
"title": "Use of tx.origin",
"type": "Warning"
}

@ -1,7 +1,7 @@
# Analysis results for test-filename.sol
## Use of tx.origin
- SWC ID: 115
- SWC ID: 111
- Type: Warning
- Contract: Unknown
- Function name: `transferOwnership(address)`

@ -1,5 +1,5 @@
==== Use of tx.origin ====
SWC ID: 115
SWC ID: 111
Type: Warning
Contract: Unknown
Function name: transferOwnership(address)

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