[WIP] Transaction displacement attack detector

.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

manticore/ethereum/__init__.py

@@ -17,6 +17,7 @@
     DetectUninitializedStorage,
     DetectRaceCondition,
     DetectManipulableBalance,
+    DetectTransactionDisplacement,
 )
 from .account import EVMAccount, EVMContract
 from .solidity import SolidityMetadata

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
     ]

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

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++;
+    }
+}

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);
+    }
+}

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);
+    }
+}

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