Merge branch 'develop' into improvement/tool-based-integration-tests

pull/1065/head
Bernhard Mueller 6 years ago committed by GitHub
commit 08d1d30a91
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
  1. 4
      README.md
  2. 6
      docs/source/about.rst
  3. 2
      docs/source/analysis-modules.rst
  4. 20
      docs/source/conf.py
  5. 2
      docs/source/create-module.rst
  6. 2
      docs/source/index.rst
  7. 22
      docs/source/module-list.rst
  8. 2
      docs/source/security-analysis.rst
  9. 2
      mythril/__version__.py
  10. 4
      mythril/analysis/modules/dos.py
  11. 2
      mythril/analysis/modules/exceptions.py
  12. 198
      mythril/analysis/modules/integer.py
  13. 10
      mythril/analysis/modules/suicide.py
  14. 7
      mythril/analysis/symbolic.py
  15. 10
      mythril/interfaces/cli.py
  16. 0
      mythril/laser/ethereum/strategy/extensions/__init__.py
  17. 84
      mythril/laser/ethereum/strategy/extensions/bounded_loops.py
  18. 4
      mythril/laser/ethereum/svm.py
  19. 4
      mythril/mythril/mythril_analyzer.py

@ -6,7 +6,7 @@
[![Discord](https://img.shields.io/discord/481002907366588416.svg)](https://discord.gg/E3YrVtG)
[![PyPI](https://badge.fury.io/py/mythril.svg)](https://pypi.python.org/pypi/mythril)
[![Read the Docs](https://readthedocs.org/projects/mythril/badge/?version=master)](https://mythril.readthedocs.io/en/master/)
[![Read the Docs](https://readthedocs.org/projects/mythril-classic/badge/?version=master)](https://mythril-classic.readthedocs.io/en/master/)
![Master Build Status](https://img.shields.io/circleci/build/github/ConsenSys/mythril.svg?token=97124ecfaee54366859cae98b5dafc0714325f8b)
[![Sonarcloud - Maintainability](https://sonarcloud.io/api/project_badges/measure?project=mythril&metric=sqale_rating)](https://sonarcloud.io/dashboard?id=mythril)
[![Pypi Installs](https://pepy.tech/badge/mythril)](https://pepy.tech/project/mythril)
@ -41,7 +41,7 @@ Instructions for using Mythril are found on the [Wiki](https://github.com/Consen
For support or general discussions please join the Mythril community on [Discord](https://discord.gg/E3YrVtG).
## Bulding the Documentation
Mythril's documentation is contained in the `docs` folder and is published to [Read the Docs](https://mythril.readthedocs.io/en/master/). It is based on Sphinx and can be built using the Makefile contained in the subdirectory:
Mythril's documentation is contained in the `docs` folder and is published to [Read the Docs](https://mythril-classic.readthedocs.io/en/master/). It is based on Sphinx and can be built using the Makefile contained in the subdirectory:
```
cd docs

@ -1,6 +1,6 @@
What is Mythril Classic?
What is Mythril?
========================
Mythril Classic is a security analysis tool for Ethereum smart contracts. It was `introduced at HITBSecConf 2018 <https://github.com/b-mueller/smashing-smart-contracts/blob/master/smashing-smart-contracts-1of1.pdf>`_.
Mythril is a security analysis tool for Ethereum smart contracts. It was `introduced at HITBSecConf 2018 <https://github.com/b-mueller/smashing-smart-contracts/blob/master/smashing-smart-contracts-1of1.pdf>`_.
Mythril Classic detects a range of security issues, including integer underflows, owner-overwrite-to-Ether-withdrawal, and others. Note that Mythril is targeted at finding common vulnerabilities, and is not able to discover issues in the business logic of an application. Furthermore, Mythril and symbolic executors are generally unsound, as they are often unable to explore all possible states of a program.
Mythril detects a range of security issues, including integer underflows, owner-overwrite-to-Ether-withdrawal, and others. Note that Mythril is targeted at finding common vulnerabilities, and is not able to discover issues in the business logic of an application. Furthermore, Mythril and symbolic executors are generally unsound, as they are often unable to explore all possible states of a program.

@ -1,7 +1,7 @@
Analysis Modules
================
Mythril Classic's detection capabilities are written in modules in the `/analysis/modules <https://github.com/ConsenSys/mythril-classic/tree/master/mythril/analysis/modules>`_ directory.
Mythril's detection capabilities are written in modules in the `/analysis/modules <https://github.com/ConsenSys/mythril/tree/master/mythril/analysis/modules>`_ directory.
.. toctree::

@ -108,7 +108,7 @@ html_static_path = ["_static"]
# -- Options for HTMLHelp output ---------------------------------------------
# Output file base name for HTML help builder.
htmlhelp_basename = "MythrilClassicdoc"
htmlhelp_basename = "Mythrildoc"
# -- Options for LaTeX output ------------------------------------------------
@ -132,13 +132,7 @@ latex_elements = {
# (source start file, target name, title,
# author, documentclass [howto, manual, or own class]).
latex_documents = [
(
master_doc,
"MythrilClassic.tex",
"Mythril Classic Documentation",
"Bernhard Mueller",
"manual",
)
(master_doc, "Mythril.tex", "Mythril Documentation", "Bernhard Mueller", "manual")
]
@ -146,9 +140,7 @@ latex_documents = [
# One entry per manual page. List of tuples
# (source start file, name, description, authors, manual section).
man_pages = [
(master_doc, "mythrilclassic", "Mythril Classic Documentation", [author], 1)
]
man_pages = [(master_doc, "mythril", "Mythril Documentation", [author], 1)]
# -- Options for Texinfo output ----------------------------------------------
@ -159,10 +151,10 @@ man_pages = [
texinfo_documents = [
(
master_doc,
"MythrilClassic",
"Mythril Classic Documentation",
"Mythril",
"Mythril Documentation",
author,
"MythrilClassic",
"Mythril",
"One line description of project.",
"Miscellaneous",
)

@ -1,4 +1,4 @@
Creating a Module
=================
Create a module in the :code:`analysis/modules` directory, and create an instance of a class that inherits :code:`DetectionModule` named :code:`detector`. Take a look at the `suicide module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/suicide.py>`_ as an example.
Create a module in the :code:`analysis/modules` directory, and create an instance of a class that inherits :code:`DetectionModule` named :code:`detector`. Take a look at the `suicide module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/suicide.py>`_ as an example.

@ -1,4 +1,4 @@
Welcome to Mythril Classic's documentation!
Welcome to Mythril's documentation!
===========================================
.. toctree::

@ -5,65 +5,65 @@ Modules
Delegate Call To Untrusted Contract
***********************************
The `delegatecall module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/delegatecall.py>`_ detects `SWC-112 (DELEGATECALL to Untrusted Callee) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-112>`_.
The `delegatecall module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/delegatecall.py>`_ detects `SWC-112 (DELEGATECALL to Untrusted Callee) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-112>`_.
***********************************
Dependence on Predictable Variables
***********************************
The `predictable variables module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/dependence_on_predictable_vars.py>`_ detects `SWC-120 (Weak Randomness) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-120>`_ and `SWC-116 (Timestamp Dependence) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-116>`_.
The `predictable variables module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/dependence_on_predictable_vars.py>`_ detects `SWC-120 (Weak Randomness) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-120>`_ and `SWC-116 (Timestamp Dependence) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-116>`_.
******************
Deprecated Opcodes
******************
The `deprecated opcodes module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/deprecated_ops.py>`_ detects `SWC-111 (Use of Deprecated Functions) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-111>`_.
The `deprecated opcodes module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/deprecated_ops.py>`_ detects `SWC-111 (Use of Deprecated Functions) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-111>`_.
***********
Ether Thief
***********
The `Ether Thief module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/ether_thief.py>`_ detects `SWC-105 (Unprotected Ether Withdrawal) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-105>`_.
The `Ether Thief module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/ether_thief.py>`_ detects `SWC-105 (Unprotected Ether Withdrawal) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-105>`_.
**********
Exceptions
**********
The `exceptions module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/exceptions.py>`_ detects `SWC-110 (Assert Violation) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-110>`_.
The `exceptions module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/exceptions.py>`_ detects `SWC-110 (Assert Violation) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-110>`_.
**************
External Calls
**************
The `external calls module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/external_calls.py>`_ warns about `SWC-117 (Reentrancy) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-107>`_ by detecting calls to external contracts.
The `external calls module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/external_calls.py>`_ warns about `SWC-117 (Reentrancy) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-107>`_ by detecting calls to external contracts.
*******
Integer
*******
The `integer module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/integer.py>`_ detects `SWC-101 (Integer Overflow and Underflow) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-101>`_.
The `integer module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/integer.py>`_ detects `SWC-101 (Integer Overflow and Underflow) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-101>`_.
**************
Multiple Sends
**************
The `multiple sends module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/multiple_sends.py>`_ detects `SWC-113 (Denial of Service with Failed Call) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-113>`_ by checking for multiple calls or sends in a single transaction.
The `multiple sends module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/multiple_sends.py>`_ detects `SWC-113 (Denial of Service with Failed Call) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-113>`_ by checking for multiple calls or sends in a single transaction.
*******
Suicide
*******
The `suicide module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/suicide.py>`_ detects `SWC-106 (Unprotected SELFDESTRUCT) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-106>`_.
The `suicide module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/suicide.py>`_ detects `SWC-106 (Unprotected SELFDESTRUCT) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-106>`_.
****************************
State Change External Calls
****************************
The `state change external calls module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/state_change_external_calls.py>`_ detects `SWC-107 (Reentrancy) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-107>`_ by detecting state change after calls to an external contract.
The `state change external calls module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/state_change_external_calls.py>`_ detects `SWC-107 (Reentrancy) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-107>`_ by detecting state change after calls to an external contract.
****************
Unchecked Retval
****************
The `unchecked retval module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/unchecked_retval.py>`_ detects `SWC-104 (Unchecked Call Return Value) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-104>`_.
The `unchecked retval module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/unchecked_retval.py>`_ detects `SWC-104 (Unchecked Call Return Value) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-104>`_.

@ -1,7 +1,7 @@
Security Analysis
=================
Run :code:`myth -x` with one of the input options described below will run the analysis modules in the `/analysis/modules <https://github.com/ConsenSys/mythril-classic/tree/master/mythril/analysis/modules>`_ directory.
Run :code:`myth -x` with one of the input options described below will run the analysis modules in the `/analysis/modules <https://github.com/ConsenSys/mythril/tree/master/mythril/analysis/modules>`_ directory.
***********************
Analyzing Solidity Code

@ -4,4 +4,4 @@ This file is suitable for sourcing inside POSIX shell, e.g. bash as well
as for importing into Python.
"""
__version__ = "v0.20.8"
__version__ = "v0.20.9"

@ -44,8 +44,8 @@ class DOS(DetectionModule):
self._jumpdest_count = {} # type: Dict[object, dict]
def _execute(self, state: GlobalState) -> None:
"""
"""
:param state:
:return:
"""
@ -70,7 +70,7 @@ class DOS(DetectionModule):
try:
self._jumpdest_count[transaction][target] += 1
if self._jumpdest_count[transaction][target] == 4:
if self._jumpdest_count[transaction][target] == 3:
annotation = (
LoopAnnotation(address, target)

@ -18,8 +18,6 @@ def _analyze_state(state) -> list:
:param state:
:return:
"""
log.info("Exceptions module: found ASSERT_FAIL instruction")
log.debug("ASSERT_FAIL in function " + state.environment.active_function_name)
try:

@ -4,7 +4,7 @@ underflows."""
import json
from math import log2, ceil
from typing import Dict, cast, List
from typing import cast, List, Dict, Set
from mythril.analysis import solver
from mythril.analysis.report import Issue
from mythril.analysis.swc_data import INTEGER_OVERFLOW_AND_UNDERFLOW
@ -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,
@ -28,11 +29,8 @@ from mythril.laser.smt import (
import logging
log = logging.getLogger(__name__)
DISABLE_EFFECT_CHECK = True
class OverUnderflowAnnotation:
""" Symbol Annotation used if a BitVector can overflow"""
@ -48,12 +46,19 @@ class OverUnderflowAnnotation:
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
) -> None:
self.overflowing_state = overflowing_state
self.operator = operator
self.constraint = constraint
def __init__(self) -> None:
self.overflowing_state_annotations = [] # type: List[OverUnderflowAnnotation]
self.ostates_seen = set() # type: Set[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):
@ -72,8 +77,19 @@ class IntegerOverflowUnderflowModule(DetectionModule):
entrypoint="callback",
pre_hooks=["ADD", "MUL", "EXP", "SUB", "SSTORE", "JUMPI", "STOP", "RETURN"],
)
"""
Cache addresses for which overflows or underflows already have been detected.
"""
self._overflow_cache = {} # type: Dict[int, bool]
self._underflow_cache = {} # type: Dict[int, bool]
"""
Cache satisfiability of overflow constraints
"""
self._ostates_satisfiable = set() # type: Set[GlobalState]
self._ostates_unsatisfiable = set() # type: Set[GlobalState]
def reset_module(self):
"""
@ -82,7 +98,8 @@ class IntegerOverflowUnderflowModule(DetectionModule):
"""
super().reset_module()
self._overflow_cache = {}
self._underflow_cache = {}
self._ostates_satisfiable = set()
self._ostates_unsatisfiable = set()
def _execute(self, state: GlobalState) -> None:
"""Executes analysis module for integer underflow and integer overflow.
@ -90,12 +107,14 @@ 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:
if self._overflow_cache.get(address, False):
return
opcode = state.get_current_instruction()["opcode"]
funcs = {
"ADD": [self._handle_add],
"SUB": [self._handle_sub],
@ -121,11 +140,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 +147,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 +154,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 +178,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 +215,42 @@ class IntegerOverflowUnderflowModule(DetectionModule):
@staticmethod
def _handle_sstore(state: GlobalState) -> None:
stack = state.mstate.stack
value = stack[-2]
if not isinstance(value, Expression):
return
state_annotation = _get_overflowunderflow_state_annotation(state)
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.add(annotation.overflowing_state)
@staticmethod
def _handle_jumpi(state):
stack = state.mstate.stack
value = stack[-2]
state_annotation = _get_overflowunderflow_state_annotation(state)
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.add(annotation.overflowing_state)
@staticmethod
def _handle_return(state: GlobalState) -> None:
@ -251,50 +259,58 @@ class IntegerOverflowUnderflowModule(DetectionModule):
locations in the memory returned by RETURN opcode.
:param state: The Global State
"""
stack = state.mstate.stack
try:
offset, length = get_concrete_int(stack[-1]), get_concrete_int(stack[-2])
except TypeError:
return
state_annotation = _get_overflowunderflow_state_annotation(state)
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,
annotation.operator,
annotation.constraint,
)
)
if (
isinstance(annotation, OverUnderflowAnnotation)
and annotation not in state_annotation.overflowing_state_annotations
):
state_annotation.overflowing_state_annotations.append(annotation)
def _handle_transaction_end(self, state: GlobalState) -> None:
for annotation in cast(
List[OverUnderflowStateAnnotation],
state.get_annotations(OverUnderflowStateAnnotation),
):
state_annotation = _get_overflowunderflow_state_annotation(state)
for annotation in state_annotation.overflowing_state_annotations:
ostate = annotation.overflowing_state
address = _get_address_from_state(ostate)
if annotation.operator == "subtraction" and self._underflow_cache.get(
address, False
):
if ostate in self._ostates_unsatisfiable:
continue
if annotation.operator != "subtraction" and self._overflow_cache.get(
address, False
):
continue
if ostate not in self._ostates_satisfiable:
try:
constraints = ostate.mstate.constraints + [annotation.constraint]
solver.get_model(constraints)
self._ostates_satisfiable.add(ostate)
except:
self._ostates_unsatisfiable.add(ostate)
continue
log.debug(
"Checking overflow in {} at transaction end address {}, ostate address {}".format(
state.get_current_instruction()["opcode"],
state.get_current_instruction()["address"],
ostate.get_current_instruction()["address"],
)
)
try:
# This check can be disabled if the contraints are to difficult for z3 to solve
# within any reasonable time.
if DISABLE_EFFECT_CHECK:
constraints = ostate.mstate.constraints + [annotation.constraint]
else:
constraints = state.mstate.constraints + [annotation.constraint]
constraints = state.mstate.constraints + [annotation.constraint]
transaction_sequence = solver.get_transaction_sequence(
state, constraints
@ -318,25 +334,29 @@ class IntegerOverflowUnderflowModule(DetectionModule):
issue.debug = json.dumps(transaction_sequence, indent=4)
if annotation.operator == "subtraction":
self._underflow_cache[address] = True
else:
self._overflow_cache[address] = True
address = _get_address_from_state(ostate)
self._overflow_cache[address] = True
self._issues.append(issue)
@staticmethod
def _try_constraints(constraints, new_constraints):
""" Tries new constraints
:return Model if satisfiable otherwise None
"""
try:
return solver.get_model(constraints + new_constraints)
except UnsatError:
return None
detector = IntegerOverflowUnderflowModule()
def _get_address_from_state(state):
return state.get_current_instruction()["address"]
def _get_overflowunderflow_state_annotation(
state: GlobalState
) -> OverUnderflowStateAnnotation:
state_annotations = cast(
List[OverUnderflowStateAnnotation],
list(state.get_annotations(OverUnderflowStateAnnotation)),
)
if len(state_annotations) == 0:
state_annotation = OverUnderflowStateAnnotation()
state.annotate(state_annotation)
return state_annotation
else:
return state_annotations[0]

@ -4,6 +4,7 @@ from mythril.analysis.swc_data import UNPROTECTED_SELFDESTRUCT
from mythril.exceptions import UnsatError
from mythril.analysis.modules.base import DetectionModule
from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.laser.ethereum.transaction.symbolic import ATTACKER_ADDRESS
import logging
import json
@ -57,13 +58,16 @@ class SuicideModule(DetectionModule):
)
description_head = "The contract can be killed by anyone."
caller = state.current_transaction.caller
try:
try:
transaction_sequence = solver.get_transaction_sequence(
state,
state.mstate.constraints
+ [to == 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF],
+ [
to == 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF,
caller == ATTACKER_ADDRESS,
],
)
description_tail = (
"Anyone can kill this contract and withdraw its balance to an arbitrary "
@ -71,7 +75,7 @@ class SuicideModule(DetectionModule):
)
except UnsatError:
transaction_sequence = solver.get_transaction_sequence(
state, state.mstate.constraints
state, state.mstate.constraints + [caller == ATTACKER_ADDRESS]
)
description_tail = "Arbitrary senders can kill this contract."

@ -16,6 +16,9 @@ from mythril.laser.ethereum.strategy.basic import (
ReturnWeightedRandomStrategy,
BasicSearchStrategy,
)
from mythril.laser.ethereum.strategy.extensions.bounded_loops import (
BoundedLoopsStrategy,
)
from mythril.laser.smt import symbol_factory, BitVec
from typing import Union, List, Dict, Type
from mythril.solidity.soliditycontract import EVMContract, SolidityContract
@ -37,6 +40,7 @@ class SymExecWrapper:
dynloader=None,
max_depth=22,
execution_timeout=None,
loop_bound=4,
create_timeout=None,
transaction_count=2,
modules=(),
@ -87,6 +91,9 @@ class SymExecWrapper:
enable_iprof=enable_iprof,
)
if loop_bound is not None:
self.laser.extend_strategy(BoundedLoopsStrategy, loop_bound)
plugin_loader = LaserPluginLoader(self.laser)
plugin_loader.load(PluginFactory.build_mutation_pruner_plugin())
plugin_loader.load(PluginFactory.build_instruction_coverage_plugin())

@ -197,13 +197,20 @@ def create_parser(parser: argparse.ArgumentParser) -> None:
default=50,
help="Maximum recursion depth for symbolic execution",
)
options.add_argument(
"--strategy",
choices=["dfs", "bfs", "naive-random", "weighted-random"],
default="bfs",
help="Symbolic execution strategy",
)
options.add_argument(
"-b",
"--loop-bound",
type=int,
default=4,
help="Bound loops at n iterations",
metavar="N",
)
options.add_argument(
"-t",
"--transaction-count",
@ -407,6 +414,7 @@ def execute_command(
address=address,
max_depth=args.max_depth,
execution_timeout=args.execution_timeout,
loop_bound=args.loop_bound,
create_timeout=args.create_timeout,
enable_iprof=args.enable_iprof,
onchain_storage_access=not args.no_onchain_storage_access,

@ -0,0 +1,84 @@
from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.laser.ethereum.strategy.basic import BasicSearchStrategy
from mythril.laser.ethereum.state.annotation import StateAnnotation
from mythril.laser.ethereum import util
from typing import Dict, cast, List
from copy import copy
import logging
log = logging.getLogger(__name__)
class JumpdestCountAnnotation(StateAnnotation):
"""State annotation that counts the number of jumps per destination."""
def __init__(self) -> None:
self._jumpdest_count = {} # type: Dict[int, int]
def __copy__(self):
result = JumpdestCountAnnotation()
result._jumpdest_count = copy(self._jumpdest_count)
return result
class BoundedLoopsStrategy(BasicSearchStrategy):
"""Adds loop pruning to the search strategy.
Ignores JUMPI instruction if the destination was targeted >JUMPDEST_LIMIT times.
"""
def __init__(self, super_strategy: BasicSearchStrategy, *args) -> None:
""""""
self.super_strategy = super_strategy
self.jumpdest_limit = args[0][0]
log.info(
"Loaded search strategy extension: Loop bounds (limit = {})".format(
self.jumpdest_limit
)
)
BasicSearchStrategy.__init__(
self, super_strategy.work_list, super_strategy.max_depth
)
def get_strategic_global_state(self) -> GlobalState:
"""
:return:
"""
while True:
state = self.super_strategy.get_strategic_global_state()
opcode = state.get_current_instruction()["opcode"]
if opcode != "JUMPI":
return state
annotations = cast(
List[JumpdestCountAnnotation],
list(state.get_annotations(JumpdestCountAnnotation)),
)
if len(annotations) == 0:
annotation = JumpdestCountAnnotation()
state.annotate(annotation)
else:
annotation = annotations[0]
try:
target = util.get_concrete_int(state.mstate.stack[-1])
except TypeError:
return state
try:
annotation._jumpdest_count[target] += 1
except KeyError:
annotation._jumpdest_count[target] = 1
if annotation._jumpdest_count[target] > self.jumpdest_limit:
log.debug("JUMPDEST limit reached, skipping JUMPI")
continue
return state

@ -14,6 +14,7 @@ from mythril.laser.ethereum.plugins.signals import PluginSkipWorldState
from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.laser.ethereum.state.world_state import WorldState
from mythril.laser.ethereum.strategy.basic import DepthFirstSearchStrategy
from abc import ABCMeta
from mythril.laser.ethereum.time_handler import time_handler
from mythril.laser.ethereum.transaction import (
ContractCreationTransaction,
@ -102,6 +103,9 @@ class LaserEVM:
log.info("LASER EVM initialized with dynamic loader: " + str(dynamic_loader))
def extend_strategy(self, extension: ABCMeta, *args) -> None:
self.strategy = extension(self.strategy, args)
def sym_exec(
self,
world_state: WorldState = None,

@ -35,6 +35,7 @@ class MythrilAnalyzer:
address: Optional[str] = None,
max_depth: Optional[int] = None,
execution_timeout: Optional[int] = None,
loop_bound: Optional[int] = None,
create_timeout: Optional[int] = None,
enable_iprof: bool = False,
):
@ -53,6 +54,7 @@ class MythrilAnalyzer:
self.address = address
self.max_depth = max_depth
self.execution_timeout = execution_timeout
self.loop_bound = loop_bound
self.create_timeout = create_timeout
self.enable_iprof = enable_iprof
@ -142,12 +144,14 @@ class MythrilAnalyzer:
),
max_depth=self.max_depth,
execution_timeout=self.execution_timeout,
loop_bound=self.loop_bound,
create_timeout=self.create_timeout,
transaction_count=transaction_count,
modules=modules,
compulsory_statespace=False,
enable_iprof=self.enable_iprof,
)
issues = fire_lasers(sym, modules)
except KeyboardInterrupt:
log.critical("Keyboard Interrupt")

Loading…
Cancel
Save