diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 92ddd8358..151ccbd1f 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -157,7 +157,7 @@ jobs: mkdir truffle_tests cd truffle_tests truffle unbox metacoin - coverage run -m manticore . --contract MetaCoin --workspace output + coverage run -m manticore . --exclude-all --contract MetaCoin --workspace output # Truffle smoke test. We test if manticore is able to generate states # from a truffle project. if [ "$(ls output/*tx -l | wc -l)" != "34" ]; then diff --git a/manticore/ethereum/__init__.py b/manticore/ethereum/__init__.py index 068a7c8be..25a059846 100644 --- a/manticore/ethereum/__init__.py +++ b/manticore/ethereum/__init__.py @@ -17,6 +17,7 @@ DetectUninitializedStorage, DetectRaceCondition, DetectManipulableBalance, + DetectTransactionDisplacement, ) from .account import EVMAccount, EVMContract from .solidity import SolidityMetadata diff --git a/manticore/ethereum/cli.py b/manticore/ethereum/cli.py index 388fe7b30..7d4b0b80a 100644 --- a/manticore/ethereum/cli.py +++ b/manticore/ethereum/cli.py @@ -13,6 +13,7 @@ DetectRaceCondition, DetectorClassification, DetectManipulableBalance, + DetectTransactionDisplacement, ) from ..core.plugin import Profiler from .manticore import ManticoreEVM @@ -55,6 +56,7 @@ def get_detectors_classes(): DetectExternalCallAndLeak, DetectEnvInstruction, DetectManipulableBalance, + DetectTransactionDisplacement, # The RaceCondition detector has been disabled for now as it seems to collide with IntegerOverflow detector # DetectRaceCondition ] diff --git a/manticore/ethereum/detectors.py b/manticore/ethereum/detectors.py index 521525e28..77318a6ad 100644 --- a/manticore/ethereum/detectors.py +++ b/manticore/ethereum/detectors.py @@ -1,7 +1,7 @@ from manticore.core.smtlib.visitors import simplify import hashlib from enum import Enum -from typing import Optional +from typing import Optional, Iterable import logging from contextlib import contextmanager @@ -15,6 +15,9 @@ taint_with, ) from ..core.plugin import Plugin +from ..platforms.evm import Transaction +from ..utils import config +from .state import State logger = logging.getLogger(__name__) @@ -871,3 +874,228 @@ def did_evm_execute_instruction_callback(self, state, instruction, arguments, re for op in arguments: if istainted(op, "BALANCE"): self.add_finding_here(state, "Manipulable balance used in a strict comparison") + + +DEBUG_REPLAY = False + +WARNED = "warned" +TROUBLEMAKER = "troublemaker" +IN_DID_RUN_CALLBACK = "in_did_run_callback" +REPLAYING = "replaying" + + +class DetectTransactionDisplacement(Detector): + """ + Detects cases where: + * transaction Y returns successfully + * for some transaction X from a different account, when X precedes Y, Y reverts + """ + + ARGUMENT = "transaction-displacement" + HELP = "Susceptible to transaction displacement attacks" + IMPACT = DetectorClassification.MEDIUM + CONFIDENCE = DetectorClassification.HIGH + + def __init__(self, *args, **kwargs): + super().__init__(*args, **kwargs) + + @classmethod + def state_context_name(cls, name: str): + return cls.__name__ + "." + name + + @classmethod + def debug(cls, msg: str, *args): + logger.debug(cls.__name__ + ": " + msg, *args) + + @classmethod + def info(cls, msg: str, *args): + logger.info(cls.__name__ + ": " + msg, *args) + + def will_run_callback(self, states: Iterable[State]): + with self.locked_context(value_type=dict) as context: + if context.get(IN_DID_RUN_CALLBACK): + return + + if not context.get(WARNED): + consts = config.get_group("evm") + if consts.sha3 is consts.sha3.symbolicate: + logger.warn( + "Unsound symbolication can cause the transaction displacement attack" + + " detector to produce false positives" + ) + context[WARNED] = True + + if not context.get(TROUBLEMAKER): + # sam.moelius: Use same initial balance as in ManticoreEVM.multi_tx_analysis. + troublemaker = self.manticore.create_account( + balance=10000000000000000000, name="troublemaker", + ) + context[TROUBLEMAKER] = troublemaker.address + self.debug("troublemaker = %s", hex(troublemaker.address)) + + for state in states: + if state.platform._pending_transaction.type != "CALL": + continue + + with state as new_state: + # sam.moelius: The state returned by StateBase.__enter__ references the original + # platform, but we want an actual copy so that we can clear its + # _pending_transaction field. As convoluted as this may seem, the easiest way + # to completely copy a state appears to be to _save and re_load it. + state_id = self.manticore._save(new_state) + new_state = self.manticore._load(state_id) + new_state.platform._pending_transaction = None + assert self.manticore._save(new_state, state_id) == state_id + + assert self.state_context_name("state_id") not in state.context + state.context[self.state_context_name("state_id")] = state_id + + self.debug("saved state %r as state %r", state.id, state_id) + + def did_close_transaction_callback(self, state: State, tx: Transaction): + if not tx.is_human: + return + + if tx.sort != "CALL": + return + + with self.locked_context(value_type=dict) as context: + + if not context.get(IN_DID_RUN_CALLBACK): + + state_id = state.context[self.state_context_name("state_id")] + del state.context[self.state_context_name("state_id")] + + if tx.return_value != 0: + tx = tx.concretize(state, constrain=True) + with self.locked_context("queue", list) as context_queue: + context_queue.append((state_id, tx)) + self.debug("queued (%s, %s)", state_id, tx) + else: + # sam.moelius: Do not remove state_id. There could be multiple states whose + # self.state_context_name("state_id") field is state_id. + # self.manticore._remove(state_id) + pass + + else: + + if context.get(REPLAYING): + if tx.return_value == 0: + assert not DEBUG_REPLAY, str(state.platform) + self.add_finding( + state, + tx.address, + 0, + f"{tx.result} caused by transaction displacement", + False, + ) + + def did_run_callback(self): + with self.locked_context(value_type=dict) as context: + if context.get(IN_DID_RUN_CALLBACK): + return + + # sam.moelius: Exiting early avoids unnecessary log messages. + with self.locked_context("queue", list) as context_queue: + if not context_queue: + return + + context[IN_DID_RUN_CALLBACK] = True + + # sam.moelius: Leaving the "with" block saves the context. + + saved_states = [] + with self.manticore.locked_context("ethereum.saved_states", list) as context_saved_states: + while context_saved_states: + saved_states.append(context_saved_states.pop()) + + queue = [] + with self.locked_context("queue", list) as context_queue: + while context_queue: + queue.append(context_queue.pop()) + + self.info("injecting transactions (%d queued states)", len(queue)) + + for state_id, tx in queue: + # sam.moelius: This is an optimization. In the first iteration, the troublemaker's + # transaction has the same data as the original transaction. If the replayed original + # transaction then reverts, no symbolic exploration is performed. + for copy_tx in True, False: + # sam.moelius: Manticore deletes states in the ready queue. But this state_id may + # have been queued with multiple txs. So make a copy of this state. + state = self.manticore._load(state_id) + with state as new_state: + new_state_id = self.manticore._save(new_state) + self.debug("copied state %r to state %r", state.id, new_state_id) + + assert not self.manticore._ready_states + self.manticore._ready_states.append(new_state_id) + + if not DEBUG_REPLAY: + troublemaker = None + with self.locked_context(value_type=dict) as context: + troublemaker = context[TROUBLEMAKER] + context[REPLAYING] = False + + symbolic_address = self.manticore.make_symbolic_value() + symbolic_data = self.manticore.make_symbolic_buffer( + 320 if not copy_tx else len(tx.data) + ) + symbolic_value = self.manticore.make_symbolic_value() + + if copy_tx: + self.manticore.constrain(symbolic_data == tx.data) + + self.manticore.transaction( + caller=troublemaker, + address=symbolic_address, + data=symbolic_data, + value=symbolic_value, + ) + + self.info( + "replaying original transaction (%d alive states)", + self.manticore.count_ready_states(), + ) + + with self.locked_context(value_type=dict) as context: + context[REPLAYING] = True + + terminated_state_count = self.manticore.count_terminated_states() + + self.manticore.transaction( + caller=tx.caller, + data=tx.data, + address=tx.address, + value=tx.value, + gas=tx.gas, + price=tx.price, + ) + + # sam.moelius: Move ready states to the terminated list so that test cases are + # generated for them. + while self.manticore._ready_states: + state_id = self.manticore._ready_states.pop() + self.manticore._terminated_states.append(state_id) + + # sam.moelius: This check could not be done in the loop just above, because states + # may have been added to the terminated list when the original transaction was + # replayed. + exit_early = False + for i in range(terminated_state_count, self.manticore.count_terminated_states()): + state_id = self.manticore._terminated_states[i] + state = self.manticore._load(state_id) + if self.get_findings(state): + exit_early = True + self.debug("exiting early") + break + if exit_early: + break + + with self.manticore.locked_context("ethereum.saved_states", list) as context_saved_states: + assert not context_saved_states + while saved_states: + context_saved_states.append(saved_states.pop()) + + with self.locked_context(value_type=dict) as context: + context[IN_DID_RUN_CALLBACK] = False diff --git a/tests/ethereum/contracts/basic.sol b/tests/ethereum/contracts/basic.sol new file mode 100644 index 000000000..597e96e18 --- /dev/null +++ b/tests/ethereum/contracts/basic.sol @@ -0,0 +1,12 @@ +contract Basic { + uint256 n; + + constructor(uint256 _n) public { + n = _n; + } + + function submit(uint256 _x) external { + require(_x == n, "wrong value"); + n++; + } +} diff --git a/tests/ethereum/contracts/sqrt.sol b/tests/ethereum/contracts/sqrt.sol new file mode 100644 index 000000000..c63ee9589 --- /dev/null +++ b/tests/ethereum/contracts/sqrt.sol @@ -0,0 +1,16 @@ +contract Sqrt { + uint256 n; + + constructor(uint256 _n) public payable { + require(0 < _n, "not positive"); + n = _n; + } + + function submit(uint256 _x) external { + require(0 < _x, "not positive"); + require(_x * _x <= n, "too big"); + require(n < (_x + 1) * (_x + 1), "too small"); + n = 0; + msg.sender.transfer(address(this).balance); + } +} diff --git a/tests/ethereum/contracts/sqrt_better.sol b/tests/ethereum/contracts/sqrt_better.sol new file mode 100644 index 000000000..4f91c4306 --- /dev/null +++ b/tests/ethereum/contracts/sqrt_better.sol @@ -0,0 +1,22 @@ +contract Sqrt { + uint256 n; + mapping(address => bytes32) commits; + + constructor(uint256 _n) public payable { + require(0 < _n, "not positive"); + n = _n; + } + + function commit(bytes32 _value) external { + commits[msg.sender] = _value; + } + + function reveal(uint256 _x, uint256 _salt) external { + require(keccak256(abi.encode(_x, _salt)) == commits[msg.sender], "not committed to"); + require(0 < _x, "not positive"); + require(_x * _x <= n, "too big"); + require(n < (_x + 1) * (_x + 1), "too small"); + n = 0; + msg.sender.transfer(address(this).balance); + } +} diff --git a/tests/ethereum/test_general.py b/tests/ethereum/test_general.py index f77c5a58a..255c99490 100644 --- a/tests/ethereum/test_general.py +++ b/tests/ethereum/test_general.py @@ -21,6 +21,7 @@ State, DetectExternalCallAndLeak, DetectIntegerOverflow, + DetectTransactionDisplacement, Detector, NoAliveStates, ABI, @@ -31,6 +32,7 @@ from manticore.ethereum.solidity import SolidityMetadata from manticore.platforms import evm from manticore.platforms.evm import EVMWorld, ConcretizeArgument, concretized_args, Return, Stop +from manticore.utils import config, log from manticore.utils.deprecated import ManticoreDeprecationWarning solver = Z3Solver.instance() @@ -61,6 +63,45 @@ def test_int_ovf(self): self.assertIn("Unsigned integer overflow at MUL instruction", all_findings) +class EthDetectorsTransactionDisplacement(unittest.TestCase): + def test_transaction_displacement_basic(self): + # log.set_verbosity(5) + consts = config.get_group("evm") + consts.sha3 = consts.sha3.concretize + mevm = ManticoreEVM() + mevm.register_detector(DetectTransactionDisplacement()) + filename = os.path.join(THIS_DIR, "contracts/basic.sol") + mevm.multi_tx_analysis(filename, tx_limit=1) + mevm.finalize() + self.assertEqual(len(mevm.global_findings), 1) + all_findings = "".join([x[2] for x in mevm.global_findings]) + self.assertIn("REVERT caused by transaction displacement", all_findings) + + def test_transaction_displacement_sqrt(self): + # log.set_verbosity(5) + consts = config.get_group("evm") + consts.sha3 = consts.sha3.concretize + mevm = ManticoreEVM() + mevm.register_detector(DetectTransactionDisplacement()) + filename = os.path.join(THIS_DIR, "contracts/sqrt.sol") + mevm.multi_tx_analysis(filename, tx_limit=1) + mevm.finalize() + self.assertEqual(len(mevm.global_findings), 1) + all_findings = "".join([x[2] for x in mevm.global_findings]) + self.assertIn("REVERT caused by transaction displacement", all_findings) + + def test_transaction_displacement_sqrt_better(self): + # log.set_verbosity(5) + consts = config.get_group("evm") + consts.sha3 = consts.sha3.concretize + mevm = ManticoreEVM() + mevm.register_detector(DetectTransactionDisplacement()) + filename = os.path.join(THIS_DIR, "contracts/sqrt_better.sol") + mevm.multi_tx_analysis(filename, tx_limit=2) + mevm.finalize() + self.assertEqual(len(mevm.global_findings), 0) + + class EthAbiTests(unittest.TestCase): _multiprocess_can_split = True