From 571c8708ba7ab0e8021984850c00b062b75999cb Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Wed, 16 Jan 2019 15:44:06 +0700 Subject: [PATCH] Add constantinople reentrancy check modules --- .../analysis/modules/constantinople_bug_1.py | 93 ++++++++++++++++++ .../analysis/modules/constantinople_bug_2.py | 96 +++++++++++++++++++ mythril/laser/ethereum/gas.py | 10 +- .../laser/ethereum/plugins/mutation_pruner.py | 10 +- 4 files changed, 197 insertions(+), 12 deletions(-) create mode 100644 mythril/analysis/modules/constantinople_bug_1.py create mode 100644 mythril/analysis/modules/constantinople_bug_2.py diff --git a/mythril/analysis/modules/constantinople_bug_1.py b/mythril/analysis/modules/constantinople_bug_1.py new file mode 100644 index 00000000..08837965 --- /dev/null +++ b/mythril/analysis/modules/constantinople_bug_1.py @@ -0,0 +1,93 @@ +"""This module checks for the Constantinople reentrancy vulnerability reported by ChainSecurity.""" + +from mythril.analysis import solver +from mythril.analysis.swc_data import REENTRANCY +from mythril.analysis.modules.base import DetectionModule +from mythril.laser.ethereum.plugins.mutation_pruner import MutationAnnotation +from mythril.analysis.report import Issue +from mythril.laser.ethereum.state.global_state import GlobalState +from mythril.exceptions import UnsatError +import logging + +log = logging.getLogger(__name__) + +DESCRIPTION = """ + +This module reports an issue when: + +1. The STOP or RETURN instruction is reached AND +2. A state variable has been modified during the transaction AND +2. The minimum gas used by the transaction is less than or equal to 1600. + + +""" + + +def _analyze_state(state): + """ + :param state: + :return: + """ + node = state.node + + if len(list(state.get_annotations(MutationAnnotation))) > 0: + + if state.mstate.min_gas_used <= 1600: + + # Verify that this state is reachable + + try: + constraints = node.constraints + transaction_sequence = solver.get_transaction_sequence( + state, constraints + ) + + except UnsatError: + log.debug("State is unreachable.") + return [] + + issue = Issue( + contract=node.contract_name, + function_name=node.function_name, + address=state.instruction["address"], + swc_id=REENTRANCY, + title="State write for 1600 gas or less", + severity="Medium", + bytecode=state.environment.code.bytecode, + description_head="Caller can modify state for 1600 gas or less.", + description_tail="The planned Constantinople hard fork reduces the gas cost for writing to state " + +"variables that have been written to in the same transaction. In some cases " + +"this may cause re-rentrancy vulnerabilities in previously safe contracts.", + debug=transaction_sequence, + gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), + ) + + return [issue] + + return [] + + +class ConstantinopleReentrancy(DetectionModule): + + def __init__(self): + """""" + super().__init__( + name="Constantinople reentrancy vulnerability", + swc_id=REENTRANCY, + description=DESCRIPTION, + entrypoint="callback", + pre_hooks=["STOP", "RETURN"], + ) + + def execute(self, state: GlobalState): + """ + + :param state: + :return: + """ + + self._issues.extend(_analyze_state(state)) + return self.issues + + +detector = ConstantinopleReentrancy() diff --git a/mythril/analysis/modules/constantinople_bug_2.py b/mythril/analysis/modules/constantinople_bug_2.py new file mode 100644 index 00000000..4c05c1de --- /dev/null +++ b/mythril/analysis/modules/constantinople_bug_2.py @@ -0,0 +1,96 @@ +"""This module contains the detection code for potentially insecure low-level +calls.""" + +from mythril.analysis import solver +from mythril.analysis.swc_data import REENTRANCY +from mythril.analysis.modules.base import DetectionModule +from mythril.analysis.report import Issue +from mythril.laser.smt import UGT, symbol_factory +from mythril.laser.ethereum.state.global_state import GlobalState +from mythril.laser.ethereum.state.annotation import StateAnnotation +from mythril.exceptions import UnsatError +import logging +import json + +log = logging.getLogger(__name__) + +DESCRIPTION = """ + +Search for external calls followed by a state change (CALL / SSTORE). + +""" + +class PostCallAnnotation(StateAnnotation): + pass + + +def _analyze_state(state): + """ + :param state: + :return: + """ + node = state.node + + if len(list(state.get_annotations(PostCallAnnotation))) > 0: + + # Verify that this state is reachable + + try: + constraints = node.constraints + transaction_sequence = solver.get_transaction_sequence( + state, constraints + ) + + except UnsatError: + log.debug("State is unreachable.") + return [] + + issue = Issue( + contract=node.contract_name, + function_name=node.function_name, + address=state.instruction["address"], + swc_id=REENTRANCY, + title="State change after external call", + severity="Medium", + bytecode=state.environment.code.bytecode, + description_head="State change after external call.", + description_tail="The contract account state is changed after an external call. Consider that the " + "called contract could re-enter the function before this state change takes place. This can lead to " + "business logic vulnerabilities.", + debug=transaction_sequence, + gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), + ) + + return [issue] + + elif state.instruction["opcode"] == "CALL": + state.annotate(PostCallAnnotation()) + + return [] + + +class ExternalCalls(DetectionModule): + """This module searches for low level calls (e.g. call.value()) that + forward all gas to the callee.""" + + def __init__(self): + """""" + super().__init__( + name="External calls", + swc_id=REENTRANCY, + description=DESCRIPTION, + entrypoint="callback", + pre_hooks=["CALL", "SSTORE"] + ) + + def execute(self, state: GlobalState): + """ + + :param state: + :return: + """ + self._issues.extend(_analyze_state(state)) + return self.issues + + +detector = ExternalCalls() diff --git a/mythril/laser/ethereum/gas.py b/mythril/laser/ethereum/gas.py index 43c5d48b..6f7b3c06 100644 --- a/mythril/laser/ethereum/gas.py +++ b/mythril/laser/ethereum/gas.py @@ -94,7 +94,7 @@ OPCODE_GAS = { "MSTORE8": (3, 98), # assume 64 byte r/w cost as upper bound "SLOAD": (400, 400), - "SSTORE": (5000, 25000), + "SSTORE": (200, 25000), "JUMP": (8, 8), "JUMPI": (10, 10), "PC": (2, 2), @@ -170,10 +170,10 @@ OPCODE_GAS = { # allows, but let's stick to the reasonable standard here. # https://ethereum.stackexchange.com/a/1691 "LOG0": (375, 375 + 8 * 32), - "LOG1": (2 * 375, 2 * 375 + 8 * 32), - "LOG2": (3 * 375, 3 * 375 + 8 * 32), - "LOG3": (4 * 375, 4 * 375 + 8 * 32), - "LOG4": (5 * 375, 5 * 375 + 8 * 32), + "LOG1": (375, 2 * 375 + 8 * 32), + "LOG2": (375, 3 * 375 + 8 * 32), + "LOG3": (375, 4 * 375 + 8 * 32), + "LOG4": (375, 5 * 375 + 8 * 32), "CREATE": (32000, 32000), "CALL": (700, 700 + 9000 + 25000), "NATIVE_COST": calculate_native_gas, diff --git a/mythril/laser/ethereum/plugins/mutation_pruner.py b/mythril/laser/ethereum/plugins/mutation_pruner.py index 8af16126..4029ba0e 100644 --- a/mythril/laser/ethereum/plugins/mutation_pruner.py +++ b/mythril/laser/ethereum/plugins/mutation_pruner.py @@ -3,7 +3,7 @@ from mythril.laser.ethereum.svm import LaserEVM from mythril.laser.ethereum.plugins.signals import PluginSkipWorldState from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.transaction.transaction_models import ( - ContractCreationTransaction, + MessageCallTransaction, ) @@ -48,9 +48,5 @@ class MutationPruner: @symbolic_vm.laser_hook("add_world_state") def world_state_filter_hook(global_state: GlobalState): - if isinstance( - global_state.current_transaction, ContractCreationTransaction - ): - return - if len(list(global_state.get_annotations(MutationAnnotation))) == 0: - raise PluginSkipWorldState + if isinstance(global_state.current_transaction, MessageCallTransaction) and len(list(global_state.get_annotations(MutationAnnotation))) == 0: + raise PluginSkipWorldState