From e3fe79f7773c1faf15147369806133d57ce442de Mon Sep 17 00:00:00 2001 From: Aleksandr Sobolev Date: Fri, 14 Jun 2019 15:26:52 +0600 Subject: [PATCH 1/8] Define ENV variable to suspend regressions reporting for some testcases --- .circleci/config.yml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.circleci/config.yml b/.circleci/config.yml index 6174655f..8be4f6b6 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -111,7 +111,8 @@ jobs: --output-dir /opt/edelweiss \ --plugin-dir /opt/mythril \ --s3 \ - --circle-ci CircleCI/mythril.csv + --circle-ci CircleCI/mythril.csv\ + --ignore-regressions $IGNORE_REGRESSIONS pypi_release: <<: *defaults From 22d286e13637434845090b003298f54e7011269f Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Fri, 14 Jun 2019 15:19:30 +0200 Subject: [PATCH 2/8] Check constraints on caller in delegatecall module --- mythril/analysis/modules/delegatecall.py | 38 ++++++++++++++++-------- 1 file changed, 26 insertions(+), 12 deletions(-) diff --git a/mythril/analysis/modules/delegatecall.py b/mythril/analysis/modules/delegatecall.py index 71bc0fb4..eee0b20f 100644 --- a/mythril/analysis/modules/delegatecall.py +++ b/mythril/analysis/modules/delegatecall.py @@ -6,6 +6,10 @@ from typing import List, cast from mythril.analysis import solver from mythril.analysis.swc_data import DELEGATECALL_TO_UNTRUSTED_CONTRACT +from mythril.laser.ethereum.transaction.symbolic import ATTACKER_ADDRESS +from mythril.laser.ethereum.transaction.transaction_models import ( + ContractCreationTransaction, +) from mythril.analysis.report import Issue from mythril.analysis.modules.base import DetectionModule from mythril.exceptions import UnsatError @@ -17,16 +21,26 @@ log = logging.getLogger(__name__) class DelegateCallAnnotation(StateAnnotation): - def __init__(self, call_state: GlobalState) -> None: + def __init__(self, call_state: GlobalState, constraints: List) -> None: """ Initialize DelegateCall Annotation :param call_state: Call state """ self.call_state = call_state + self.constraints = constraints self.return_value = call_state.new_bitvec( "retval_{}".format(call_state.get_current_instruction()["address"]), 256 ) + """ + def __copy__(self): + result = DelegateCallAnnotation() + result.call_state = self.call_state + result.return_value = self.return_value + result.constraints = copy(self.constraints) + return result + """ + def get_issue(self, global_state: GlobalState, transaction_sequence: str) -> Issue: """ Returns Issue for the annotation @@ -107,26 +121,26 @@ def _analyze_states(state: GlobalState) -> List[Issue]: gas = state.mstate.stack[-1] to = state.mstate.stack[-2] - constraints = copy(state.mstate.constraints) - # Check whether we can also set the callee address - - constraints += [ - to == 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF, + constraints = [ + to == ATTACKER_ADDRESS, UGT(gas, symbol_factory.BitVecVal(2300, 256)), ] - try: - solver.get_model(constraints) - state.annotate(DelegateCallAnnotation(call_state=state)) - except UnsatError: - log.debug("[DELEGATECALL] Annotation skipped.") + for tx in state.world_state.transaction_sequence: + if not isinstance(tx, ContractCreationTransaction): + constraints.append(tx.caller == ATTACKER_ADDRESS) + + state.annotate(DelegateCallAnnotation(state, constraints)) return [] else: for annotation in annotations: try: transaction_sequence = solver.get_transaction_sequence( - state, state.mstate.constraints + [annotation.return_value == 1] + state, + state.mstate.constraints + + annotation.constraints + + [annotation.return_value == 1], ) debug = json.dumps(transaction_sequence, indent=4) issues.append(annotation.get_issue(state, transaction_sequence=debug)) From 34d627086489c8be621e281f2403abbaa7713926 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Fri, 14 Jun 2019 15:50:27 +0200 Subject: [PATCH 3/8] Add caller constraints to all relevant modules --- mythril/analysis/modules/delegatecall.py | 3 --- mythril/analysis/modules/ether_thief.py | 14 ++++++++------ mythril/analysis/modules/external_calls.py | 11 ++++++++++- mythril/analysis/modules/suicide.py | 19 ++++++++++++------- 4 files changed, 30 insertions(+), 17 deletions(-) diff --git a/mythril/analysis/modules/delegatecall.py b/mythril/analysis/modules/delegatecall.py index eee0b20f..4eeec52b 100644 --- a/mythril/analysis/modules/delegatecall.py +++ b/mythril/analysis/modules/delegatecall.py @@ -1,7 +1,6 @@ """This module contains the detection code for insecure delegate call usage.""" import json import logging -from copy import copy from typing import List, cast from mythril.analysis import solver @@ -32,14 +31,12 @@ class DelegateCallAnnotation(StateAnnotation): "retval_{}".format(call_state.get_current_instruction()["address"]), 256 ) - """ def __copy__(self): result = DelegateCallAnnotation() result.call_state = self.call_state result.return_value = self.return_value result.constraints = copy(self.constraints) return result - """ def get_issue(self, global_state: GlobalState, transaction_sequence: str) -> Issue: """ diff --git a/mythril/analysis/modules/ether_thief.py b/mythril/analysis/modules/ether_thief.py index 3fa65aa7..064ef0b7 100644 --- a/mythril/analysis/modules/ether_thief.py +++ b/mythril/analysis/modules/ether_thief.py @@ -8,6 +8,9 @@ from mythril.analysis import solver from mythril.analysis.modules.base import DetectionModule from mythril.analysis.report import Issue from mythril.laser.ethereum.transaction.symbolic import ATTACKER_ADDRESS +from mythril.laser.ethereum.transaction.transaction_models import ( + ContractCreationTransaction, +) from mythril.analysis.swc_data import UNPROTECTED_ETHER_WITHDRAWAL from mythril.exceptions import UnsatError from mythril.laser.ethereum.state.global_state import GlobalState @@ -85,11 +88,10 @@ class EtherThief(DetectionModule): constraints += [BVAddNoOverflow(eth_sent_total, tx.call_value, False)] eth_sent_total = Sum(eth_sent_total, tx.call_value) - constraints += [ - tx.caller == ATTACKER_ADDRESS, - UGT(call_value, eth_sent_total), - target == ATTACKER_ADDRESS, - ] + if not isinstance(tx, ContractCreationTransaction): + constraints.append(tx.caller == ATTACKER_ADDRESS) + + constraints += [UGT(call_value, eth_sent_total), target == ATTACKER_ADDRESS] try: @@ -116,7 +118,7 @@ class EtherThief(DetectionModule): log.debug("[ETHER_THIEF] no model found") return [] - self._cache_addresses[address] = True + # self._cache_addresses[address] = True return [issue] diff --git a/mythril/analysis/modules/external_calls.py b/mythril/analysis/modules/external_calls.py index 510dd82c..21605503 100644 --- a/mythril/analysis/modules/external_calls.py +++ b/mythril/analysis/modules/external_calls.py @@ -3,6 +3,10 @@ calls.""" from mythril.analysis import solver from mythril.analysis.swc_data import REENTRANCY +from mythril.laser.ethereum.transaction.symbolic import ATTACKER_ADDRESS +from mythril.laser.ethereum.transaction.transaction_models import ( + ContractCreationTransaction, +) from mythril.analysis.modules.base import DetectionModule from mythril.analysis.report import Issue from mythril.laser.smt import UGT, symbol_factory, Or, BitVec @@ -44,7 +48,12 @@ def _analyze_state(state): # Check whether we can also set the callee address try: - constraints += [to == 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF] + constraints += [to == ATTACKER_ADDRESS] + + for tx in state.world_state.transaction_sequence: + if not isinstance(tx, ContractCreationTransaction): + constraints.append(tx.caller == ATTACKER_ADDRESS) + transaction_sequence = solver.get_transaction_sequence(state, constraints) debug = json.dumps(transaction_sequence, indent=4) diff --git a/mythril/analysis/modules/suicide.py b/mythril/analysis/modules/suicide.py index 57c593e2..a35636b1 100644 --- a/mythril/analysis/modules/suicide.py +++ b/mythril/analysis/modules/suicide.py @@ -5,6 +5,9 @@ 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 +from mythril.laser.ethereum.transaction.transaction_models import ( + ContractCreationTransaction, +) import logging import json @@ -58,16 +61,18 @@ class SuicideModule(DetectionModule): ) description_head = "The contract can be killed by anyone." - caller = state.current_transaction.caller + + constraints = [] + + for tx in state.world_state.transaction_sequence: + if not isinstance(tx, ContractCreationTransaction): + constraints.append(tx.caller == ATTACKER_ADDRESS) + try: try: transaction_sequence = solver.get_transaction_sequence( state, - state.mstate.constraints - + [ - to == 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF, - caller == ATTACKER_ADDRESS, - ], + state.mstate.constraints + constraints + [to == ATTACKER_ADDRESS], ) description_tail = ( "Anyone can kill this contract and withdraw its balance to an arbitrary " @@ -75,7 +80,7 @@ class SuicideModule(DetectionModule): ) except UnsatError: transaction_sequence = solver.get_transaction_sequence( - state, state.mstate.constraints + [caller == ATTACKER_ADDRESS] + state, state.mstate.constraints + constraints ) description_tail = "Arbitrary senders can kill this contract." From a7bad0e96b63039b120c938af12b7224ecff218c Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Fri, 14 Jun 2019 16:35:29 +0200 Subject: [PATCH 4/8] Fix annotation copy --- mythril/analysis/modules/delegatecall.py | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/mythril/analysis/modules/delegatecall.py b/mythril/analysis/modules/delegatecall.py index 4eeec52b..55d61532 100644 --- a/mythril/analysis/modules/delegatecall.py +++ b/mythril/analysis/modules/delegatecall.py @@ -2,6 +2,7 @@ import json import logging from typing import List, cast +from copy import copy from mythril.analysis import solver from mythril.analysis.swc_data import DELEGATECALL_TO_UNTRUSTED_CONTRACT @@ -32,11 +33,7 @@ class DelegateCallAnnotation(StateAnnotation): ) def __copy__(self): - result = DelegateCallAnnotation() - result.call_state = self.call_state - result.return_value = self.return_value - result.constraints = copy(self.constraints) - return result + return DelegateCallAnnotation(self.call_state, copy(self.constraints)) def get_issue(self, global_state: GlobalState, transaction_sequence: str) -> Issue: """ From b65828bf84e78076d07491d6acc528c96309ca0a Mon Sep 17 00:00:00 2001 From: Aleksandr Sobolev Date: Mon, 17 Jun 2019 15:17:04 +0600 Subject: [PATCH 5/8] Change cli param to ignore-false-positives --- .circleci/config.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.circleci/config.yml b/.circleci/config.yml index 8be4f6b6..7666ad6a 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -112,7 +112,7 @@ jobs: --plugin-dir /opt/mythril \ --s3 \ --circle-ci CircleCI/mythril.csv\ - --ignore-regressions $IGNORE_REGRESSIONS + --ignore-false-positives $IGNORE_FALSE_POSITIVES pypi_release: <<: *defaults From da779aa56aad8e93b2c1ad079e5a4a944fe14b98 Mon Sep 17 00:00:00 2001 From: Aleksandr Sobolev Date: Mon, 17 Jun 2019 15:18:04 +0600 Subject: [PATCH 6/8] Added branch to CircleCI config for debugging new changes --- .circleci/config.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.circleci/config.yml b/.circleci/config.yml index 7666ad6a..9937aa62 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -169,6 +169,7 @@ workflows: only: - develop - master + - feature/ignore-regressions tags: only: /v[0-9]+(\.[0-9]+)*/ requires: From 01b221f914e522b11ab658412d19921961bb4710 Mon Sep 17 00:00:00 2001 From: Aleksandr Sobolev Date: Tue, 18 Jun 2019 12:21:45 +0600 Subject: [PATCH 7/8] Pass list of files to ignore false positives --- .circleci/config.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.circleci/config.yml b/.circleci/config.yml index 9937aa62..0ea11528 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -112,7 +112,7 @@ jobs: --plugin-dir /opt/mythril \ --s3 \ --circle-ci CircleCI/mythril.csv\ - --ignore-false-positives $IGNORE_FALSE_POSITIVES + --ignore-false-positives guess_the_random_number_fixed.sol simple_dao.sol old_blockhash.sol pypi_release: <<: *defaults From 9b960a298501b786b5fb4903d960d847274dcae6 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Tue, 18 Jun 2019 17:45:42 +0200 Subject: [PATCH 8/8] Add missing line to fix recursive intializaton :) --- mythril/analysis/modules/delegatecall.py | 1 + 1 file changed, 1 insertion(+) diff --git a/mythril/analysis/modules/delegatecall.py b/mythril/analysis/modules/delegatecall.py index 8404b21a..52b656ee 100644 --- a/mythril/analysis/modules/delegatecall.py +++ b/mythril/analysis/modules/delegatecall.py @@ -32,6 +32,7 @@ class DelegateCallAnnotation(StateAnnotation): "retval_{}".format(call_state.get_current_instruction()["address"]), 256 ) + def _copy__(self): return DelegateCallAnnotation(self.call_state, copy(self.constraints)) def get_issue(self, global_state: GlobalState, transaction_sequence: Dict) -> Issue: