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

Use different SMT array for each map

Browse Source
pull/1102/head
Nikhil Parasaram 5 years ago
parent dd7b255fc9
commit efd7c95f86
5 changed files with 6 additions and 161 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. 3
      mythril/analysis/modules/integer.py
  2. 2
      mythril/analysis/solver.py
  3. 104
      mythril/laser/ethereum/instructions.py
  4. 38
      mythril/laser/ethereum/keccak.py
  5. 20
      mythril/laser/ethereum/state/account.py

3
mythril/analysis/modules/integer.py
Unescape View File

@ -230,7 +230,6 @@ class IntegerOverflowUnderflowModule(DetectionModule):
or annotation.overflowing_state in state_annotation.ostates_seen
):
continue
state_annotation.overflowing_state_annotations.append(annotation)
state_annotation.ostates_seen.add(annotation.overflowing_state)
@ -248,7 +247,6 @@ class IntegerOverflowUnderflowModule(DetectionModule):
or annotation.overflowing_state in state_annotation.ostates_seen
):
continue
state_annotation.overflowing_state_annotations.append(annotation)
state_annotation.ostates_seen.add(annotation.overflowing_state)
@ -311,7 +309,6 @@ class IntegerOverflowUnderflowModule(DetectionModule):
try:
constraints = state.mstate.constraints + [annotation.constraint]
transaction_sequence = solver.get_transaction_sequence(
state, constraints
)

2
mythril/analysis/solver.py
Unescape View File

@ -28,7 +28,7 @@ def get_model(constraints, minimize=(), maximize=(), enforce_execution_time=True
:return:
"""
s = Optimize()
timeout = 100000
timeout = 200000
if enforce_execution_time:
timeout = min(timeout, time_handler.time_remaining() - 500)
if timeout <= 0:

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

@ -18,15 +18,11 @@ from mythril.laser.smt import (
ULT,
UGT,
BitVec,
is_true,
Bool,
BitVecFunc,
is_false,
URem,
SRem,
If,
Bool,
Or,
Not,
LShR,
)
@ -43,7 +39,6 @@ from mythril.laser.ethereum.evm_exceptions import (
OutOfGasException,
)
from mythril.laser.ethereum.gas import OPCODE_GAS
from mythril.laser.ethereum.keccak import KeccakFunctionManager
from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.laser.ethereum.transaction import (
MessageCallTransaction,
@ -58,8 +53,6 @@ log = logging.getLogger(__name__)
TT256 = 2 ** 256
TT256M1 = 2 ** 256 - 1
keccak_function_manager = KeccakFunctionManager()
class StateTransition(object):
"""Decorator that handles global state copy and original return.
@ -195,7 +188,6 @@ class Instruction:
if not post
else getattr(self, op + "_" + "post", None)
)
if instruction_mutator is None:
raise NotImplementedError
@ -419,6 +411,7 @@ class Instruction:
* helper.pop_bitvec(global_state.mstate)
)
)
return [global_state]
@StateTransition()
@ -895,7 +888,6 @@ class Instruction:
:param global_state:
:return:
"""
global keccak_function_manager
state = global_state.mstate
op0, op1 = state.stack.pop(), state.stack.pop()
@ -950,7 +942,6 @@ class Instruction:
)
log.debug("Created BitVecFunc hash.")
keccak_function_manager.add_keccak(result, state.memory[index])
else:
keccak = utils.sha3(data.value.to_bytes(length, byteorder="big"))
result = symbol_factory.BitVecFuncVal(
@ -1366,64 +1357,13 @@ class Instruction:
:param global_state:
:return:
"""
global keccak_function_manager
state = global_state.mstate
index = state.stack.pop()
log.debug("Storage access at index " + str(index))
"""
if index not in global_state.environment.active_account.storage.keys():
for key in global_state.environment.active_account.storage.keys():
if not isinstance(index, BitVecFunc) or not isinstance(key, BitVecFunc):
global_state.mstate.constraints.append(Bool(key.raw != index.raw))
continue
key_map = Extract(255, 0, key.input_)
index_map = Extract(255, 0, index.input_)
if simplify(key_map == index_map):
continue
global_state.mstate.constraints.append(key != index)
"""
state.stack.append(global_state.environment.active_account.storage[index])
return [global_state]
@staticmethod
def _sload_helper(
global_state: GlobalState, index: Union[str, int], constraints=None
):
"""
:param global_state:
:param index:
:param constraints:
:return:
"""
try:
data = global_state.environment.active_account.storage[index]
except KeyError:
data = global_state.new_bitvec("storage_" + str(index), 256)
global_state.environment.active_account.storage[index] = data
if constraints is not None:
global_state.mstate.constraints += constraints
global_state.mstate.stack.append(data)
return [global_state]
@staticmethod
def _get_constraints(keccak_keys, this_key, argument):
"""
:param keccak_keys:
:param this_key:
:param argument:
"""
global keccak_function_manager
for keccak_key in keccak_keys:
if keccak_key == this_key:
continue
keccak_argument = keccak_function_manager.get_argument(keccak_key)
yield keccak_argument != argument
@StateTransition()
def sstore_(self, global_state: GlobalState) -> List[GlobalState]:
"""
@ -1431,54 +1371,12 @@ class Instruction:
:param global_state:
:return:
"""
global keccak_function_manager
state = global_state.mstate
index, value = state.stack.pop(), state.stack.pop()
"""
if index not in global_state.environment.active_account.storage.keys():
for key in global_state.environment.active_account.storage.keys():
if not isinstance(index, BitVecFunc) or not isinstance(key, BitVecFunc):
global_state.mstate.constraints.append(Bool(key.raw != index.raw))
continue
key_map = Extract(255, 0, key.input_)
index_map = Extract(255, 0, index.input_)
if simplify(key_map == index_map):
continue
global_state.mstate.constraints.append(key != index)
"""
log.debug("Write to storage[" + str(index) + "]")
global_state.environment.active_account.storage[index] = value
return [global_state]
@staticmethod
def _sstore_helper(global_state, index, value, constraint=None):
"""
:param global_state:
:param index:
:param value:
:param constraint:
:return:
"""
try:
global_state.environment.active_account = deepcopy(
global_state.environment.active_account
)
global_state.accounts[
global_state.environment.active_account.address.value
] = global_state.environment.active_account
global_state.environment.active_account.storage[index] = (
value if not isinstance(value, Expression) else simplify(value)
)
except KeyError:
log.debug("Error writing to storage: Invalid index")
if constraint is not None:
global_state.mstate.constraints.append(constraint)
return [global_state]
@StateTransition(increment_pc=False, enable_gas=False)
def jump_(self, global_state: GlobalState) -> List[GlobalState]:
"""

38
mythril/laser/ethereum/keccak.py
Unescape View File

@ -1,38 +0,0 @@
"""This module contains a function manager to deal with symbolic Keccak
values."""
from mythril.laser.smt import Expression
class KeccakFunctionManager:
"""A keccak function manager for symbolic expressions."""
def __init__(self):
""""""
self.keccak_expression_mapping = {}
def is_keccak(self, expression: Expression) -> bool:
"""
:param expression:
:return:
"""
return str(expression) in self.keccak_expression_mapping.keys()
def get_argument(self, expression: Expression) -> Expression:
"""
:param expression:
:return:
"""
if not self.is_keccak(expression):
raise ValueError("Expression is not a recognized keccac result")
return self.keccak_expression_mapping[str(expression)][1]
def add_keccak(self, expression: Expression, argument: Expression) -> None:
"""
:param expression:
:param argument:
"""
index = str(expression)
self.keccak_expression_mapping[index] = (expression, argument)

20
mythril/laser/ethereum/state/account.py
Unescape View File

@ -2,7 +2,7 @@
This includes classes representing accounts and their storage.
"""
from copy import deepcopy, copy
from copy import deepcopy
from typing import Any, Dict, Union
@ -14,9 +14,7 @@ from mythril.laser.smt import symbol_factory
class Storage:
"""Storage class represents the storage of an Account."""
def __init__(
self, concrete=False, address=None, dynamic_loader=None, keys=None
) -> None:
def __init__(self, concrete=False, address=None, dynamic_loader=None) -> None:
"""Constructor for Storage.
:param concrete: bool indicating whether to interpret uninitialized storage as concrete versus symbolic
@ -28,12 +26,10 @@ class Storage:
self._standard_storage = Array("Storage", 256, 256)
self._map_storage = {}
self._keys = keys or set()
self.dynld = dynamic_loader
self.address = address
def __getitem__(self, item: Union[str, int]) -> Any:
self._keys.add(item)
storage = self._get_corresponding_storage(item)
return simplify(storage[item])
@ -42,7 +38,6 @@ class Storage:
if not isinstance(key, BitVecFunc) or key.func_name != "keccak256":
return None
index = Extract(255, 0, key.input_)
print(simplify(index), key.input_)
return simplify(index)
def _get_corresponding_storage(self, key):
@ -61,17 +56,13 @@ class Storage:
return storage
def __setitem__(self, key, value: Any) -> None:
self._keys.add(key)
storage = self._get_corresponding_storage(key)
storage[key] = value
def __deepcopy__(self, memodict={}):
concrete = isinstance(self._standard_storage, K)
storage = Storage(
concrete=concrete,
address=self.address,
dynamic_loader=self.dynld,
keys=deepcopy(self._keys),
concrete=concrete, address=self.address, dynamic_loader=self.dynld
)
storage._standard_storage = deepcopy(self._standard_storage)
storage._map_storage = deepcopy(self._map_storage)
@ -80,9 +71,6 @@ class Storage:
def __str__(self):
return str(self._standard_storage)
def keys(self):
return self._keys
class Account:
"""Account class representing ethereum accounts."""
@ -172,6 +160,6 @@ class Account:
contract_name=self.contract_name,
balances=self._balances,
)
new_account.storage = copy(self.storage)
new_account.storage = deepcopy(self.storage)
new_account.code = self.code
return new_account

Write Preview
Loading…
Cancel
Save