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

Merge pull request #211 from JoranHonig/features/integerpool

Browse Source 
Run overflow detection in a thread pool
pull/212/head
Bernhard Mueller 7 years ago committed by GitHub
parent ad34e05b37 5891bcc1cb
commit ffa8cfb284
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
3 changed files with 83 additions and 44 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. 113
      mythril/analysis/modules/integer.py
  2. 2
      mythril/analysis/modules/transaction_order_independence.py
  3. 12
      mythril/analysis/solver.py

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

@ -4,10 +4,13 @@ from mythril.analysis.ops import *
from mythril.analysis.report import Issue
from mythril.exceptions import UnsatError
from laser.ethereum.taint_analysis import TaintRunner
from multiprocessing.pool import ThreadPool
from threading import RLock
import re
import copy
import logging
import datetime
locker = RLock()
'''
MODULE DESCRIPTION:
@ -22,19 +25,47 @@ def execute(statespace):
:param statespace: Statespace to analyse
:return: Found issues
"""
pool = ThreadPool(4)
logging.debug("Executing module: INTEGER")
issues = []
results = []
durations = []
start = datetime.datetime.now()
for k in statespace.nodes:
node = statespace.nodes[k]
results.append(pool.apply_async(check_node, [statespace, node]))
pool.close()
pool.join()
for k in statespace.nodes:
node = statespace.nodes[k]
for state in node.states:
issues += _check_integer_underflow(statespace, state, node)
issues += _check_integer_overflow(statespace, state, node)
results += _check_integer_underflow(statespace, state, node)
for result in results:
g, d = result.get()
if g is not None:
issues += g
durations.append(d)
t = durations[0]
for i in durations[1:]:
t += i
stop = datetime.datetime.now()
print(t)
print(stop-start)
return issues
def check_node(statespace, node):
start = datetime.datetime.now()
results = []
for state in node.states:
results += _check_integer_overflow(statespace, state, node)
end = datetime.datetime.now()
return results, end - start
def _check_integer_overflow(statespace, state, node):
"""
@ -45,6 +76,7 @@ def _check_integer_overflow(statespace, state, node):
:return: found issue
"""
issues = []
# try:
# Check the instruction
instruction = state.get_current_instruction()
@ -52,8 +84,10 @@ def _check_integer_overflow(statespace, state, node):
return issues
# Formulate overflow constraints
ctx = state.context
stack = state.mstate.stack
op0, op1 = stack[-1], stack[-2]
op0, op1 = stack[1], stack[-2]
# An integer overflow is possible if op0 + op1 or op0 * op1 > MAX_UINT
# Do a type check
@ -63,9 +97,9 @@ def _check_integer_overflow(statespace, state, node):
# Change ints to BitVec
if type(op0) is int:
op0 = BitVecVal(op0, 256)
op0 = BitVecVal(op0, 256, ctx)
if type(op1) is int:
op1 = BitVecVal(op1, 256)
op1 = BitVecVal(op1, 256, ctx)
# Formulate expression
if instruction['opcode'] == "ADD":
@ -73,17 +107,20 @@ def _check_integer_overflow(statespace, state, node):
else:
expr = op1 * op0
assert op0.ctx == op1.ctx
assert expr.ctx == ctx
# Check satisfiable
constraint = Or(And(ULT(expr, op0), op1 != 0), And(ULT(expr, op1), op0 != 0))
constraint = Or(And(ULT(expr, op0), op1 != 0, ctx), And(ULT(expr, op1), op0 != 0, ctx), ctx)
model = _try_constraints(node.constraints, [constraint])
if model is None:
logging.debug("[INTEGER_OVERFLOW] no model found")
return issues
if not _verify_integer_overflow(statespace, node, expr, state, model, constraint, op0, op1):
if not _verify_integer_overflow(statespace, node, state, constraint):
return issues
# Build issue
issue = Issue(node.contract_name, node.function_name, instruction['address'], "Integer Overflow ", "Warning")
@ -96,11 +133,11 @@ def _check_integer_overflow(statespace, state, node):
return issues
def _verify_integer_overflow(statespace, node, expr, state, model, constraint, op0, op1):
def _verify_integer_overflow(statespace, node, state, constraint):
""" Verifies existence of integer overflow """
# If we get to this point then there has been an integer overflow
# Find out if the overflowed value is actually used
interesting_usages = _search_children(statespace, node, expr, constraint=[constraint], index=node.states.index(state))
interesting_usages = _search_children(statespace, node, constraint=[constraint], index=node.states.index(state))
# Stop if it isn't
if len(interesting_usages) == 0:
@ -114,9 +151,13 @@ def _try_constraints(constraints, new_constraints):
Tries new constraints
:return Model if satisfiable otherwise None
"""
_constraints = copy.deepcopy(constraints)
_constraints = constraints[:]
ctx = constraints[0].ctx if len(constraints) > 0 else None
for constraint in new_constraints:
_constraints.append(copy.deepcopy(constraint))
if ctx is not None:
_constraints.append(copy.deepcopy(constraint).translate(ctx))
else:
_constraints.append(copy.deepcopy(constraint))
try:
model = solver.get_model(_constraints)
return model
@ -136,12 +177,9 @@ def _check_integer_underflow(statespace, state, node):
if instruction['opcode'] == "SUB":
stack = state.mstate.stack
op0 = stack[-1]
op1 = stack[-2]
constraints = copy.deepcopy(node.constraints)
# Filter for patterns that indicate benign underflows
# Pattern 1: (96 + calldatasize_MAIN) - (96), where (96 + calldatasize_MAIN) would underflow if calldatasize is very large.
@ -159,32 +197,33 @@ def _check_integer_underflow(statespace, state, node):
str(instruction['address'])))
allowed_types = [int, BitVecRef, BitVecNumRef]
if type(op0) in allowed_types and type(op1) in allowed_types:
constraints.append(UGT(op1, op0))
if not (type(op0) in allowed_types and type(op1) in allowed_types):
return []
try:
c = UGT(op1, op0)
model = solver.get_model(constraints)
model = _try_constraints(node.constraints, [c])
if model is None:
logging.debug("[INTEGER_UNDERFLOW] no model found")
return []
# If we get to this point then there has been an integer overflow
# Find out if the overflowed value is actually used
interesting_usages = _search_children(statespace, node, (op0 - op1), index=node.states.index(state))
# If we get to this point then there has been an integer underflow
# Find out if the overflowed value is actually used
interesting_usages = _search_children(statespace, node, index=node.states.index(state))
# Stop if it isn't
if len(interesting_usages) == 0:
return issues
# Stop if it isn't
if len(interesting_usages) == 0:
return issues
issue = Issue(node.contract_name, node.function_name, instruction['address'], "Integer Underflow",
"Warning")
issue = Issue(node.contract_name, node.function_name, instruction['address'], "Integer Underflow",
"Warning")
issue.description = "A possible integer underflow exists in the function `" + node.function_name + "`.\n" \
"The subtraction may result in a value < 0."
issue.description = "A possible integer underflow exists in the function `" + node.function_name + "`.\n" \
"The subtraction may result in a value < 0."
issue.debug = solver.pretty_print_model(model)
issues.append(issue)
issue.debug = solver.pretty_print_model(model)
issues.append(issue)
except UnsatError:
logging.debug("[INTEGER_UNDERFLOW] no model found")
return issues
@ -212,7 +251,7 @@ def _check_sstore(state, taint_result):
return taint_result.check(state, -2)
def _search_children(statespace, node, expression, taint_result=None, constraint=[], index=0, depth=0, max_depth=64):
def _search_children(statespace, node, taint_result=None, constraint=[], index=0, depth=0, max_depth=64):
"""
Checks the statespace for children states, with JUMPI or SSTORE instuctions,
for dependency on expression
@ -260,7 +299,7 @@ def _search_children(statespace, node, expression, taint_result=None, constraint
]
for child in children:
results += _search_children(statespace, child, expression, taint_result, depth=depth + 1, max_depth=max_depth)
results += _search_children(statespace, child, taint_result, depth=depth + 1, max_depth=max_depth)
return results

2
mythril/analysis/modules/transaction_order_independence.py
Unescape View File

@ -128,7 +128,7 @@ def _try_constraints(constraints, new_constraints):
"""
_constraints = copy.deepcopy(constraints)
for constraint in new_constraints:
_constraints.append(copy.deepcopy(constraint))
_constraints.append(copy.deepcopy(constraint).translate(constraints[0].ctx))
try:
model = solver.get_model(_constraints)
return model

12
mythril/analysis/solver.py
Unescape View File

@ -1,13 +1,13 @@
from z3 import Solver, simplify, sat
from z3 import Solver, simplify, sat, ExprRef, SolverFor
from mythril.exceptions import UnsatError
def get_model(constraints):
s = Solver()
s.set("timeout", 10000)
for constraint in constraints:
s.add(constraint)
def get_model(constraints):
context = constraints[0].ctx
s = Solver(ctx=context)
s.set("timeout", 5000)
s.add(constraints)
if (s.check() == sat):

Write Preview
Loading…
Cancel
Save