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

Refactor integer module

Browse Source
integer_experimental
Bernhard Mueller 6 years ago
parent 85c599d832
commit c121372792
1 changed files with 70 additions and 45 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. 115
      mythril/analysis/modules/integer.py

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

@ -13,6 +13,7 @@ from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.laser.ethereum.util import get_concrete_int
from mythril.laser.ethereum.state.annotation import StateAnnotation
from mythril.analysis.modules.base import DetectionModule
from copy import copy
from mythril.laser.smt import (
BVAddNoOverflow,
@ -27,8 +28,6 @@ from mythril.laser.smt import (
)
import logging
log = logging.getLogger(__name__)
DISABLE_EFFECT_CHECK = True
@ -49,11 +48,18 @@ class OverUnderflowStateAnnotation(StateAnnotation):
""" State Annotation used if an overflow is both possible and used in the annotated path"""
def __init__(
self, overflowing_state: GlobalState, operator: str, constraint: Bool
self
) -> None:
self.overflowing_state = overflowing_state
self.operator = operator
self.constraint = constraint
self.overflowing_state_annotations = [] # type: List[OverUnderflowAnnotation]
self.ostates_seen = [] # type: List[GlobalState]
def __copy__(self):
new_annotation = OverUnderflowStateAnnotation()
new_annotation.overflowing_state_annotations = copy(self.overflowing_state_annotations)
new_annotation.ostates_seen = copy(self.ostates_seen)
return new_annotation
class IntegerOverflowUnderflowModule(DetectionModule):
@ -90,12 +96,16 @@ class IntegerOverflowUnderflowModule(DetectionModule):
:param state: Statespace to analyse
:return: Found issues
"""
address = _get_address_from_state(state)
has_overflow = self._overflow_cache.get(address, False)
has_underflow = self._underflow_cache.get(address, False)
if has_overflow or has_underflow:
return
opcode = state.get_current_instruction()["opcode"]
logging.info("Integer overflow module instruction: " + opcode)
funcs = {
"ADD": [self._handle_add],
"SUB": [self._handle_sub],
@ -121,11 +131,6 @@ class IntegerOverflowUnderflowModule(DetectionModule):
op0, op1 = self._get_args(state)
c = Not(BVAddNoOverflow(op0, op1, False))
# Check satisfiable
model = self._try_constraints(state.mstate.constraints, [c])
if model is None:
return
annotation = OverUnderflowAnnotation(state, "addition", c)
op0.annotate(annotation)
@ -133,11 +138,6 @@ class IntegerOverflowUnderflowModule(DetectionModule):
op0, op1 = self._get_args(state)
c = Not(BVMulNoOverflow(op0, op1, False))
# Check satisfiable
model = self._try_constraints(state.mstate.constraints, [c])
if model is None:
return
annotation = OverUnderflowAnnotation(state, "multiplication", c)
op0.annotate(annotation)
@ -145,11 +145,6 @@ class IntegerOverflowUnderflowModule(DetectionModule):
op0, op1 = self._get_args(state)
c = Not(BVSubNoUnderflow(op0, op1, False))
# Check satisfiable
model = self._try_constraints(state.mstate.constraints, [c])
if model is None:
return
annotation = OverUnderflowAnnotation(state, "subtraction", c)
op0.annotate(annotation)
@ -174,9 +169,7 @@ class IntegerOverflowUnderflowModule(DetectionModule):
)
else:
constraint = op0.value ** op1.value >= 2 ** 256
model = self._try_constraints(state.mstate.constraints, [constraint])
if model is None:
return
annotation = OverUnderflowAnnotation(state, "exponentiation", constraint)
op0.annotate(annotation)
@ -213,36 +206,54 @@ class IntegerOverflowUnderflowModule(DetectionModule):
@staticmethod
def _handle_sstore(state: GlobalState) -> None:
stack = state.mstate.stack
value = stack[-2]
if not isinstance(value, Expression):
return
state_annotations = cast(
List[OverUnderflowStateAnnotation],
list(state.get_annotations(OverUnderflowStateAnnotation)),
)
if len(state_annotations) == 0:
state_annotation = OverUnderflowStateAnnotation()
state.annotate(state_annotation)
else:
state_annotation = state_annotations[0]
for annotation in value.annotations:
if not isinstance(annotation, OverUnderflowAnnotation):
if not isinstance(annotation, OverUnderflowAnnotation) or annotation.overflowing_state in state_annotation.ostates_seen:
continue
state.annotate(
OverUnderflowStateAnnotation(
annotation.overflowing_state,
annotation.operator,
annotation.constraint,
)
)
state_annotation.overflowing_state_annotations.append(annotation)
state_annotation.ostates_seen.append(annotation.overflowing_state)
@staticmethod
def _handle_jumpi(state):
stack = state.mstate.stack
value = stack[-2]
state_annotations = cast(
List[OverUnderflowStateAnnotation],
list(state.get_annotations(OverUnderflowStateAnnotation)),
)
if len(state_annotations) == 0:
state_annotation = OverUnderflowStateAnnotation()
state.annotate(state_annotation)
else:
state_annotation = state_annotations[0]
for annotation in value.annotations:
if not isinstance(annotation, OverUnderflowAnnotation):
if not isinstance(annotation, OverUnderflowAnnotation) or annotation.overflowing_state in state_annotation.ostates_seen:
continue
state.annotate(
OverUnderflowStateAnnotation(
annotation.overflowing_state,
annotation.operator,
annotation.constraint,
)
)
state_annotation.overflowing_state_annotations.append(annotation)
state_annotation.ostates_seen.append(annotation.overflowing_state)
@staticmethod
def _handle_return(state: GlobalState) -> None:
@ -256,11 +267,14 @@ class IntegerOverflowUnderflowModule(DetectionModule):
offset, length = get_concrete_int(stack[-1]), get_concrete_int(stack[-2])
except TypeError:
return
''' TODO: Rewrite this
for element in state.mstate.memory[offset : offset + length]:
if not isinstance(element, Expression):
continue
for annotation in element.annotations:
if isinstance(annotation, OverUnderflowAnnotation):
state.annotate(
OverUnderflowStateAnnotation(
annotation.overflowing_state,
@ -268,12 +282,23 @@ class IntegerOverflowUnderflowModule(DetectionModule):
annotation.constraint,
)
)
'''
def _handle_transaction_end(self, state: GlobalState) -> None:
for annotation in cast(
state_annotations = cast(
List[OverUnderflowStateAnnotation],
state.get_annotations(OverUnderflowStateAnnotation),
):
list(state.get_annotations(OverUnderflowStateAnnotation)),
)
if len(state_annotations) == 0:
return
annotations = state_annotations[0].overflowing_state_annotations
logging.info("Number of potentially overflowing states: {}".format(len(annotations)))
for annotation in annotations:
ostate = annotation.overflowing_state
address = _get_address_from_state(ostate)
@ -289,7 +314,7 @@ class IntegerOverflowUnderflowModule(DetectionModule):
continue
try:
# This check can be disabled if the contraints are to difficult for z3 to solve
# This check can be disabled if the constraints are to difficult for z3 to solve
# within any reasonable time.
if DISABLE_EFFECT_CHECK:
constraints = ostate.mstate.constraints + [annotation.constraint]
@ -326,7 +351,7 @@ class IntegerOverflowUnderflowModule(DetectionModule):
@staticmethod
def _try_constraints(constraints, new_constraints):
""" Tries new constraints
""" Tries new constraints
:return Model if satisfiable otherwise None
"""
try:

Write Preview
Loading…
Cancel
Save