diff --git a/mythril/analysis/issue_annotation.py b/mythril/analysis/issue_annotation.py new file mode 100644 index 00000000..1f2f09a3 --- /dev/null +++ b/mythril/analysis/issue_annotation.py @@ -0,0 +1,26 @@ +from typing import List + +from mythril.analysis.report import Issue +from mythril.laser.ethereum.state.annotation import StateAnnotation +from mythril.laser.smt import Bool + + +class IssueAnnotation(StateAnnotation): + def __init__(self, conditions: List[Bool], issue: Issue, detector): + """ + Issue Annotation to propogate issues + - conditions: A list of independent conditions [a, b, c, ...] + Each of these have to be independently be satisfied + - issue: The issue of the annotation + - detector: The detection module + """ + self.conditions = conditions + self.issue = issue + self.detector = detector + + def persist_to_world_state(self) -> bool: + return True + + @property + def persist_over_calls(self) -> bool: + return True diff --git a/mythril/analysis/module/base.py b/mythril/analysis/module/base.py index df44403e..7e15e924 100644 --- a/mythril/analysis/module/base.py +++ b/mythril/analysis/module/base.py @@ -4,10 +4,11 @@ This module includes an definition of the DetectionModule interface. DetectionModules implement different analysis rules to find weaknesses and vulnerabilities. """ import logging -from typing import List, Set, Optional, Tuple, Union +from typing import List, Set, Optional, Tuple from mythril.analysis.report import Issue from mythril.laser.ethereum.state.global_state import GlobalState +from mythril.support.support_args import args from mythril.support.support_utils import get_code_hash from abc import ABC, abstractmethod from enum import Enum @@ -86,7 +87,8 @@ class DetectionModule(ABC): result = self._execute(target) log.debug("Exiting analysis module: {}".format(self.__class__.__name__)) - if result: + + if result and not args.use_issue_annotations: self.update_cache(result) self.issues += result diff --git a/mythril/analysis/module/modules/arbitrary_jump.py b/mythril/analysis/module/modules/arbitrary_jump.py index df4cfaae..a113d471 100644 --- a/mythril/analysis/module/modules/arbitrary_jump.py +++ b/mythril/analysis/module/modules/arbitrary_jump.py @@ -1,9 +1,11 @@ """This module contains the detection code for Arbitrary jumps.""" import logging from mythril.analysis.solver import get_transaction_sequence, UnsatError +from mythril.analysis.issue_annotation import IssueAnnotation from mythril.analysis.module.base import DetectionModule, Issue, EntryPoint from mythril.analysis.swc_data import ARBITRARY_JUMP from mythril.laser.ethereum.state.global_state import GlobalState +from mythril.laser.smt import And log = logging.getLogger(__name__) @@ -37,8 +39,7 @@ class ArbitraryJump(DetectionModule): """ return self._analyze_state(state) - @staticmethod - def _analyze_state(state): + def _analyze_state(self, state): """ :param state: @@ -70,6 +71,14 @@ class ArbitraryJump(DetectionModule): gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), transaction_sequence=transaction_sequence, ) + state.annotate( + IssueAnnotation( + conditions=[And(*state.world_state.constraints)], + issue=issue, + detector=self, + ) + ) + return [issue] diff --git a/mythril/analysis/module/modules/delegatecall.py b/mythril/analysis/module/modules/delegatecall.py index 7e7c2829..b0699a9c 100644 --- a/mythril/analysis/module/modules/delegatecall.py +++ b/mythril/analysis/module/modules/delegatecall.py @@ -14,7 +14,7 @@ from mythril.laser.ethereum.transaction.transaction_models import ( from mythril.analysis.module.base import DetectionModule, EntryPoint from mythril.exceptions import UnsatError from mythril.laser.ethereum.state.global_state import GlobalState -from mythril.laser.smt import symbol_factory, UGT +from mythril.laser.smt import symbol_factory, UGT, Bool log = logging.getLogger(__name__) diff --git a/mythril/analysis/module/modules/dependence_on_origin.py b/mythril/analysis/module/modules/dependence_on_origin.py index 5e8e2c4e..7e9b575f 100644 --- a/mythril/analysis/module/modules/dependence_on_origin.py +++ b/mythril/analysis/module/modules/dependence_on_origin.py @@ -2,13 +2,14 @@ dependence.""" import logging from copy import copy - +from mythril.analysis.issue_annotation import IssueAnnotation from mythril.analysis.module.base import DetectionModule, EntryPoint from mythril.analysis.report import Issue from mythril.exceptions import UnsatError from mythril.analysis import solver from mythril.analysis.swc_data import TX_ORIGIN_USAGE from mythril.laser.ethereum.state.global_state import GlobalState +from mythril.laser.smt import And from typing import List log = logging.getLogger(__name__) @@ -40,8 +41,7 @@ class TxOrigin(DetectionModule): """ return self._analyze_state(state) - @staticmethod - def _analyze_state(state: GlobalState) -> List[Issue]: + def _analyze_state(self, state: GlobalState) -> List[Issue]: """ :param state: @@ -92,6 +92,11 @@ class TxOrigin(DetectionModule): gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), transaction_sequence=transaction_sequence, ) + state.annotate( + IssueAnnotation( + conditions=[And(*constraints)], issue=issue, detector=self + ) + ) issues.append(issue) diff --git a/mythril/analysis/module/modules/dependence_on_predictable_vars.py b/mythril/analysis/module/modules/dependence_on_predictable_vars.py index 8702f865..0fdc4af7 100644 --- a/mythril/analysis/module/modules/dependence_on_predictable_vars.py +++ b/mythril/analysis/module/modules/dependence_on_predictable_vars.py @@ -2,11 +2,12 @@ dependence.""" import logging +from mythril.analysis.issue_annotation import IssueAnnotation from mythril.analysis.module.base import DetectionModule, EntryPoint from mythril.analysis.report import Issue from mythril.exceptions import UnsatError from mythril.analysis import solver -from mythril.laser.smt import ULT, symbol_factory +from mythril.laser.smt import And, ULT, symbol_factory from mythril.analysis.swc_data import TIMESTAMP_DEPENDENCE, WEAK_RANDOMNESS from mythril.analysis.module.module_helpers import is_prehook from mythril.laser.ethereum.state.global_state import GlobalState @@ -54,8 +55,7 @@ class PredictableVariables(DetectionModule): """ return self._analyze_state(state) - @staticmethod - def _analyze_state(state: GlobalState) -> List[Issue]: + def _analyze_state(self, state: GlobalState) -> List[Issue]: """ :param state: @@ -126,7 +126,13 @@ class PredictableVariables(DetectionModule): ), transaction_sequence=transaction_sequence, ) - + state.annotate( + IssueAnnotation( + conditions=[And(*constraints)], + issue=issue, + detector=self, + ) + ) issues.append(issue) elif opcode == "BLOCKHASH": diff --git a/mythril/analysis/module/modules/exceptions.py b/mythril/analysis/module/modules/exceptions.py index d2c90e20..2ed93d97 100644 --- a/mythril/analysis/module/modules/exceptions.py +++ b/mythril/analysis/module/modules/exceptions.py @@ -3,6 +3,7 @@ import logging from typing import List, cast from mythril.analysis import solver +from mythril.analysis.issue_annotation import IssueAnnotation from mythril.analysis.module.base import DetectionModule, EntryPoint from mythril.analysis.report import Issue from mythril.analysis.swc_data import ASSERT_VIOLATION @@ -10,6 +11,7 @@ from mythril.exceptions import UnsatError from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.state.annotation import StateAnnotation from mythril.laser.ethereum import util +from mythril.laser.smt import And log = logging.getLogger(__name__) @@ -45,8 +47,7 @@ class Exceptions(DetectionModule): """ return self._analyze_state(state) - @staticmethod - def _analyze_state(state) -> List[Issue]: + def _analyze_state(self, state) -> List[Issue]: """ :param state: @@ -103,6 +104,14 @@ class Exceptions(DetectionModule): gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), source_location=annotations[0].last_jump, ) + state.annotate( + IssueAnnotation( + conditions=[And(*state.world_state.constraints)], + issue=issue, + detector=self, + ) + ) + return [issue] except UnsatError: diff --git a/mythril/analysis/module/modules/integer.py b/mythril/analysis/module/modules/integer.py index b71fcdec..cd5c597e 100644 --- a/mythril/analysis/module/modules/integer.py +++ b/mythril/analysis/module/modules/integer.py @@ -4,6 +4,7 @@ underflows.""" from math import log2, ceil from typing import cast, List, Set from mythril.analysis import solver +from mythril.analysis.issue_annotation import IssueAnnotation from mythril.analysis.report import Issue from mythril.analysis.swc_data import INTEGER_OVERFLOW_AND_UNDERFLOW from mythril.exceptions import UnsatError @@ -102,7 +103,7 @@ class IntegerArithmetics(DetectionModule): self._ostates_satisfiable = set() self._ostates_unsatisfiable = set() - def _execute(self, state: GlobalState) -> None: + def _execute(self, state: GlobalState) -> List[Issue]: """Executes analysis module for integer underflow and integer overflow. :param state: Statespace to analyse @@ -122,8 +123,12 @@ class IntegerArithmetics(DetectionModule): "STOP": [self._handle_transaction_end], "EXP": [self._handle_exp], } + results = [] for func in funcs[opcode]: - func(state) + result = func(state) + if result and len(result) > 0: + results += result + return results def _get_args(self, state): stack = state.mstate.stack @@ -253,10 +258,10 @@ class IntegerArithmetics(DetectionModule): if isinstance(annotation, OverUnderflowAnnotation): state_annotation.overflowing_state_annotations.add(annotation) - def _handle_transaction_end(self, state: GlobalState) -> None: + def _handle_transaction_end(self, state: GlobalState) -> List[Issue]: state_annotation = _get_overflowunderflow_state_annotation(state) - + issues = [] for annotation in state_annotation.overflowing_state_annotations: ostate = annotation.overflowing_state @@ -313,10 +318,13 @@ class IntegerArithmetics(DetectionModule): gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), transaction_sequence=transaction_sequence, ) - - address = _get_address_from_state(ostate) - self.cache.add(address) - self.issues.append(issue) + state.annotate( + IssueAnnotation( + issue=issue, detector=self, conditions=[And(*constraints)] + ) + ) + issues.append(issue) + return issues detector = IntegerArithmetics() diff --git a/mythril/analysis/module/modules/multiple_sends.py b/mythril/analysis/module/modules/multiple_sends.py index 2dc2bf1f..97e39ef2 100644 --- a/mythril/analysis/module/modules/multiple_sends.py +++ b/mythril/analysis/module/modules/multiple_sends.py @@ -2,13 +2,14 @@ a single transaction.""" from copy import copy from typing import cast, List - +from mythril.analysis.issue_annotation import IssueAnnotation from mythril.analysis.report import Issue from mythril.analysis.solver import get_transaction_sequence, UnsatError from mythril.analysis.swc_data import MULTIPLE_SENDS from mythril.analysis.module.base import DetectionModule, EntryPoint from mythril.laser.ethereum.state.annotation import StateAnnotation from mythril.laser.ethereum.state.global_state import GlobalState +from mythril.laser.smt import And import logging log = logging.getLogger(__name__) @@ -36,8 +37,7 @@ class MultipleSends(DetectionModule): def _execute(self, state: GlobalState) -> None: return self._analyze_state(state) - @staticmethod - def _analyze_state(state: GlobalState): + def _analyze_state(self, state: GlobalState): """ :param state: the current state :return: returns the issues for that corresponding state @@ -90,7 +90,13 @@ class MultipleSends(DetectionModule): gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), transaction_sequence=transaction_sequence, ) - + state.annotate( + IssueAnnotation( + conditions=[And(*state.world_state.constraints)], + issue=issue, + detector=self, + ) + ) return [issue] return [] diff --git a/mythril/analysis/module/modules/suicide.py b/mythril/analysis/module/modules/suicide.py index 1c834e69..7dae7f53 100644 --- a/mythril/analysis/module/modules/suicide.py +++ b/mythril/analysis/module/modules/suicide.py @@ -2,6 +2,7 @@ from mythril.analysis import solver from mythril.analysis.report import Issue from mythril.analysis.swc_data import UNPROTECTED_SELFDESTRUCT from mythril.exceptions import UnsatError +from mythril.analysis.issue_annotation import IssueAnnotation from mythril.analysis.module.base import DetectionModule, EntryPoint from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.transaction.symbolic import ACTORS @@ -49,8 +50,7 @@ class AccidentallyKillable(DetectionModule): """ return self._analyze_state(state) - @staticmethod - def _analyze_state(state): + def _analyze_state(self, state): log.info("Suicide module: Analyzing suicide instruction") instruction = state.get_current_instruction() @@ -60,20 +60,22 @@ class AccidentallyKillable(DetectionModule): description_head = "Any sender can cause the contract to self-destruct." - constraints = [] + attacker_constraints = [] for tx in state.world_state.transaction_sequence: if not isinstance(tx, ContractCreationTransaction): - constraints.append( + attacker_constraints.append( And(tx.caller == ACTORS.attacker, tx.caller == tx.origin) ) try: try: - transaction_sequence = solver.get_transaction_sequence( - state, + constraints = ( state.world_state.constraints - + constraints - + [to == ACTORS.attacker], + + [to == ACTORS.attacker] + + attacker_constraints + ) + transaction_sequence = solver.get_transaction_sequence( + state, constraints ) description_tail = ( @@ -84,8 +86,9 @@ class AccidentallyKillable(DetectionModule): ) except UnsatError: + constraints = state.world_state.constraints + attacker_constraints transaction_sequence = solver.get_transaction_sequence( - state, state.world_state.constraints + constraints + state, constraints ) description_tail = ( "Any sender can trigger execution of the SELFDESTRUCT instruction to destroy this " @@ -106,6 +109,12 @@ class AccidentallyKillable(DetectionModule): transaction_sequence=transaction_sequence, gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), ) + state.annotate( + IssueAnnotation( + conditions=[And(*constraints)], issue=issue, detector=self + ) + ) + return [issue] except UnsatError: log.debug("No model found") diff --git a/mythril/analysis/module/modules/unchecked_retval.py b/mythril/analysis/module/modules/unchecked_retval.py index 2d9cc555..05bd4399 100644 --- a/mythril/analysis/module/modules/unchecked_retval.py +++ b/mythril/analysis/module/modules/unchecked_retval.py @@ -4,12 +4,13 @@ from copy import copy from typing import cast, List from mythril.analysis import solver +from mythril.analysis.issue_annotation import IssueAnnotation from mythril.analysis.report import Issue from mythril.analysis.swc_data import UNCHECKED_RET_VAL from mythril.analysis.module.base import DetectionModule, EntryPoint from mythril.exceptions import UnsatError +from mythril.laser.smt import And from mythril.laser.smt.bitvec import BitVec - from mythril.laser.ethereum.state.annotation import StateAnnotation from mythril.laser.ethereum.state.global_state import GlobalState @@ -112,6 +113,14 @@ class UncheckedRetval(DetectionModule): gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), transaction_sequence=transaction_sequence, ) + conditions = [ + And(*(state.world_state.constraints + [retval["retval"] == 1])), + And(*(state.world_state.constraints + [retval["retval"] == 1])), + ] + + state.annotate( + IssueAnnotation(conditions=conditions, issue=issue, detector=self) + ) issues.append(issue) diff --git a/mythril/analysis/module/modules/user_assertions.py b/mythril/analysis/module/modules/user_assertions.py index d5bcf645..a45d53bf 100644 --- a/mythril/analysis/module/modules/user_assertions.py +++ b/mythril/analysis/module/modules/user_assertions.py @@ -2,11 +2,12 @@ calls.""" from mythril.analysis import solver +from mythril.analysis.issue_annotation import IssueAnnotation from mythril.analysis.potential_issues import Issue from mythril.analysis.swc_data import ASSERT_VIOLATION from mythril.analysis.module.base import DetectionModule, EntryPoint from mythril.laser.ethereum.state.global_state import GlobalState -from mythril.laser.smt import Extract +from mythril.laser.smt import Extract, And from mythril.exceptions import UnsatError import logging import eth_abi @@ -110,6 +111,13 @@ class UserAssertions(DetectionModule): transaction_sequence=transaction_sequence, gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), ) + state.annotate( + IssueAnnotation( + detector=self, + issue=issue, + conditions=[And(*state.world_state.constraints)], + ) + ) return [issue] except UnsatError: diff --git a/mythril/analysis/potential_issues.py b/mythril/analysis/potential_issues.py index ca2fb4ea..3b7e3e07 100644 --- a/mythril/analysis/potential_issues.py +++ b/mythril/analysis/potential_issues.py @@ -1,8 +1,11 @@ from mythril.analysis.report import Issue +from mythril.analysis.issue_annotation import IssueAnnotation from mythril.analysis.solver import get_transaction_sequence from mythril.exceptions import UnsatError from mythril.laser.ethereum.state.annotation import StateAnnotation from mythril.laser.ethereum.state.global_state import GlobalState +from mythril.laser.smt import And +from mythril.support.support_args import args class PotentialIssue: @@ -96,20 +99,29 @@ def check_potential_issues(state: GlobalState) -> None: continue potential_issue.detector.cache.add(potential_issue.address) - potential_issue.detector.issues.append( - Issue( - contract=potential_issue.contract, - function_name=potential_issue.function_name, - address=potential_issue.address, - title=potential_issue.title, - bytecode=potential_issue.bytecode, - swc_id=potential_issue.swc_id, - gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), - severity=potential_issue.severity, - description_head=potential_issue.description_head, - description_tail=potential_issue.description_tail, - transaction_sequence=transaction_sequence, + issue = Issue( + contract=potential_issue.contract, + function_name=potential_issue.function_name, + address=potential_issue.address, + title=potential_issue.title, + bytecode=potential_issue.bytecode, + swc_id=potential_issue.swc_id, + gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), + severity=potential_issue.severity, + description_head=potential_issue.description_head, + description_tail=potential_issue.description_tail, + transaction_sequence=transaction_sequence, + ) + state.annotate( + IssueAnnotation( + detector=potential_issue.detector, + issue=issue, + conditions=[ + And(*(state.world_state.constraints + potential_issue.constraints)) + ], ) ) - potential_issue.detector.update_cache() + if args.use_issue_annotations is False: + potential_issue.detector.issues.append(issue) + potential_issue.detector.update_cache() annotation.potential_issues = unsat_potential_issues diff --git a/mythril/support/support_args.py b/mythril/support/support_args.py index 730311ab..8734a36c 100644 --- a/mythril/support/support_args.py +++ b/mythril/support/support_args.py @@ -1,4 +1,8 @@ -class Args: +from typing import List +from mythril.support.support_utils import Singleton + + +class Args(object, metaclass=Singleton): """ This module helps in preventing args being sent through multiple of classes to reach any analysis/laser module @@ -14,6 +18,7 @@ class Args: self.solver_log = None self.transaction_sequences: List[List[str]] = None self.use_integer_module = True + self.use_issue_annotations = False args = Args()