Detecting the use of BALANCE in a strict comparison

manticore/core/smtlib/expression.py

@@ -76,15 +76,14 @@ def get_taints(arg, taint=None):
     return
 
 
-def taint_with(arg, taint, value_bits=256, index_bits=256):
+def taint_with(arg, *taints, value_bits=256, index_bits=256):
     """
     Helper to taint a value.
     :param arg: a value or Expression
     :param taint: a regular expression matching a taint value (eg. 'IMPORTANT.*'). If None, this function checks for any taint value.
     """
 
-    tainted_fset = frozenset((taint,))
-
+    tainted_fset = frozenset(tuple(taints))
     if not issymbolic(arg):
         if isinstance(arg, int):
             arg = BitVecConstant(value_bits, arg)
@@ -93,8 +92,11 @@ def taint_with(arg, taint, value_bits=256, index_bits=256):
             raise ValueError("type not supported")
 
     else:
-        arg = copy.copy(arg)
-        arg._taint |= tainted_fset
+        if isinstance(arg, BitVecVariable):
+            arg = arg + BitVecConstant(value_bits, 0, taint=tainted_fset)
+        else:
+            arg = copy.copy(arg)
+            arg._taint |= tainted_fset
 
     return arg
 

manticore/core/smtlib/solver.py

@@ -27,6 +27,7 @@
 from ...exceptions import Z3NotFoundError, SolverError, SolverUnknown, TooManySolutions
 from ...utils import config
 from . import issymbolic
+import time
 
 logger = logging.getLogger(__name__)
 consts = config.get_group("smt")
@@ -433,6 +434,7 @@ def get_all_values(self, constraints, expression, maxcnt=None, silent=False):
 
             result = []
 
+            start = time.time()
             while self._is_sat():
                 value = self._getvalue(var)
                 result.append(value)
@@ -447,7 +449,8 @@ def get_all_values(self, constraints, expression, maxcnt=None, silent=False):
                         break
                     else:
                         raise TooManySolutions(result)
-
+                if time.time() - start > consts.timeout:
+                    raise SolverError("Timeout")
             return result
 
     def optimize(self, constraints: ConstraintSet, x: BitVec, goal: str, M=10000):
@@ -471,6 +474,7 @@ def optimize(self, constraints: ConstraintSet, x: BitVec, goal: str, M=10000):
             self._reset(temp_cs.to_string(related_to=X))
             self._send(aux.declaration)
 
+            start = time.time()
             if getattr(self, f"support_{goal}"):
                 self._push()
                 try:
@@ -511,6 +515,8 @@ def optimize(self, constraints: ConstraintSet, x: BitVec, goal: str, M=10000):
                 i = i + 1
                 if i > M:
                     raise SolverError("Optimizing error, maximum number of iterations was reached")
+                if time.time() - start > consts.timeout:
+                    raise SolverError("Timeout")
             if last_value is not None:
                 return last_value
             raise SolverError("Optimizing error, unsat or unknown core")
@@ -522,6 +528,7 @@ def get_value(self, constraints, expression):
         if not issymbolic(expression):
             return expression
         assert isinstance(expression, (Bool, BitVec, Array))
+        start = time.time()
         with constraints as temp_cs:
             if isinstance(expression, Bool):
                 var = temp_cs.new_bool()
@@ -547,6 +554,8 @@ def get_value(self, constraints, expression):
                     m = pattern.match(ret)
                     expr, value = m.group("expr"), m.group("value")
                     result.append(int(value, base))
+                    if time.time() - start > consts.timeout:
+                        raise SolverError("Timeout")
                 return bytes(result)
 
             temp_cs.add(var == expression)

manticore/core/state.py

@@ -38,7 +38,7 @@ class Concretize(StateException):
 
     """
 
-    _ValidPolicies = ["MINMAX", "ALL", "SAMPLED", "ONE"]
+    _ValidPolicies = ["MIN", "MAX", "MINMAX", "ALL", "SAMPLED", "ONE"]
 
     def __init__(self, message, expression, setstate=None, policy=None, **kwargs):
         if policy is None:
@@ -244,9 +244,9 @@ def concretize(self, symbolic, policy, maxcount=7):
         if policy == "MINMAX":
             vals = self._solver.minmax(self._constraints, symbolic)
         elif policy == "MAX":
-            vals = self._solver.max(self._constraints, symbolic)
+            vals = (self._solver.max(self._constraints, symbolic),)
         elif policy == "MIN":
-            vals = self._solver.min(self._constraints, symbolic)
+            vals = (self._solver.min(self._constraints, symbolic),)
         elif policy == "SAMPLED":
             m, M = self._solver.minmax(self._constraints, symbolic)
             vals += [m, M]

manticore/core/worker.py

@@ -132,7 +132,7 @@ def run(self, *args):
                         assert current_state is None
                     # Handling Forking and terminating exceptions
                     except Concretize as exc:
-                        logger.debug("[%r] Debug %r", self.id, exc)
+                        logger.info("[%r] Debug %r", self.id, exc)
                         # The fork() method can decides which state to keep
                         # exploring. For example when the fork results in a
                         # single state it is better to just keep going.

manticore/ethereum/__init__.py

@@ -16,6 +16,7 @@
     DetectUninitializedMemory,
     DetectUninitializedStorage,
     DetectRaceCondition,
+    DetectManipulableBalance,
 )
 from .account import EVMAccount, EVMContract
 from .abi import ABI

manticore/ethereum/cli.py

@@ -12,6 +12,7 @@
     DetectEnvInstruction,
     DetectRaceCondition,
     DetectorClassification,
+    DetectManipulableBalance,
 )
 from ..core.plugin import Profiler
 from .manticore import ManticoreEVM
@@ -36,6 +37,7 @@ def get_detectors_classes():
         DetectDelegatecall,
         DetectExternalCallAndLeak,
         DetectEnvInstruction,
+        DetectManipulableBalance,
         # The RaceCondition detector has been disabled for now as it seems to collide with IntegerOverflow detector
         # DetectRaceCondition
     ]

manticore/ethereum/detectors.py

@@ -75,6 +75,7 @@ def add_finding(self, state, address, pc, finding, at_init, constraint=True):
         self.get_findings(state).append((address, pc, finding, at_init, constraint))
         with self.locked_global_findings() as gf:
             gf.append((address, pc, finding, at_init))
+
         # Fixme for ever broken logger
         logger.warning(finding)
 
@@ -838,3 +839,28 @@ def did_evm_execute_instruction_callback(self, state, instruction, arguments, re
 
                             self.__findings.add(unique_key)
                             self.add_finding_here(state, msg)
+
+
+class DetectManipulableBalance(Detector):
+    """
+    Detects the use of manipulable balance in strict compare.
+    """
+
+    ARGUMENT = "lockdrop"
+    HELP = "Use balance in EQ"
+    IMPACT = DetectorClassification.HIGH
+    CONFIDENCE = DetectorClassification.HIGH
+
+    def did_evm_execute_instruction_callback(self, state, instruction, arguments, result):
+        vm = state.platform.current_vm
+        mnemonic = instruction.semantics
+
+        if mnemonic == "BALANCE":
+            # replace result with tainted value
+            result = taint_with(result, "BALANCE")
+            vm.change_last_result(result)
+        elif mnemonic == "EQ":
+            # check if balance tainted
+            for op in arguments:
+                if istainted(op, "BALANCE"):
+                    self.add_finding_here(state, "Manipulable balance used in a strict comparison")

manticore/ethereum/manticore.py

@@ -762,13 +762,15 @@ def solidity_create_contract(
                     if lib_name not in deps:
                         contract_names.append(lib_name)
             except Exception as e:
+                logger.info("Failed to compile contract", str(e))
                 self.kill()
                 raise
 
         # If the contract was created successfully in at least 1 state return account
         for state in self.ready_states:
             if state.platform.get_code(int(contract_account)):
                 return contract_account
+        logger.info("Failed to compile contract", contract_names)
         return None
 
     def get_nonce(self, address):
@@ -1622,7 +1624,10 @@ def finalizer(state_id):
             logger.debug("Generating testcase for state_id %d", state_id)
             last_tx = st.platform.last_transaction
             message = last_tx.result if last_tx else "NO STATE RESULT (?)"
-            self.generate_testcase(st, message=message)
+            try:
+                self.generate_testcase(st, message=message)
+            except Exception as e:
+                print(e)
 
         def worker_finalize(q):
             try:

manticore/platforms/evm.py

@@ -67,6 +67,12 @@
     ),
 )
 
+consts.add(
+    "calldata_max_offset",
+    default=1024 * 1024,
+    description="Max calldata offset to explore with. Iff offset or size in a calldata related instruction are symbolic it wil wbe constrained to this constant",
+)
+
 # Auxiliary constants and functions
 TT256 = 2 ** 256
 TT256M1 = 2 ** 256 - 1
@@ -543,7 +549,9 @@ def wrapper(*args, **kwargs):
                         f"Concretizing {func.__name__}'s {index} argument and dropping its taints: "
                         "the value might not be tracked properly (in case of using detectors)"
                     )
-                logger.info(f"Concretizing instruction argument {arg} by {policy}")
+                logger.info(
+                    f"Concretizing instruction {args[0].world.current_vm.instruction} argument {arg} by {policy}"
+                )
                 raise ConcretizeArgument(index, policy=policy)
             return func(*args, **kwargs)
 
@@ -1200,7 +1208,7 @@ def setstate(state, value):
             raise Concretize(
                 "Concretize PC", expression=expression, setstate=setstate, policy="ALL"
             )
-        # print (self)
+        # print(self.instruction)
         try:
             # import time
             # limbo = 0.0
@@ -1591,7 +1599,9 @@ def CALLDATALOAD(self, offset):
         if issymbolic(offset):
             if Z3Solver().can_be_true(self._constraints, offset == self._used_calldata_size):
                 self.constraints.add(offset == self._used_calldata_size)
-            raise ConcretizeArgument(1, policy="SAMPLED")
+                offset = self._used_calldata_size
+            else:
+                raise ConcretizeArgument(1, policy="SAMPLED")
 
         self._use_calldata(offset, 32)
 
@@ -1632,18 +1642,36 @@ def CALLDATACOPY_gas(self, mem_offset, data_offset, size):
     def CALLDATACOPY(self, mem_offset, data_offset, size):
         """Copy input data in current environment to memory"""
         if issymbolic(size):
-            if Z3Solver().can_be_true(self._constraints, size <= len(self.data) + 32):
-                self.constraints.add(size <= len(self.data) + 32)
+            if not Z3Solver().can_be_true(
+                self._constraints, Operators.ULE(size, len(self.data) + data_offset + 32)
+            ):
+                print("omg it can not be small")
+                import pdb
+
+                pdb.set_trace()
+                raise ConcretizeArgument(3, policy="MIN")
+            self.constraints.add(Operators.ULE(size, len(self.data) + data_offset + 32))
             raise ConcretizeArgument(3, policy="SAMPLED")
 
         if issymbolic(data_offset):
             if Z3Solver().can_be_true(self._constraints, data_offset == self._used_calldata_size):
                 self.constraints.add(data_offset == self._used_calldata_size)
-            raise ConcretizeArgument(2, policy="SAMPLED")
+                data_offset = self._used_calldata_size
+                print("symbolic data_offset", data_offset, "choosing", self._used_calldata_size)
+            else:
+                logger.debug("symbolic data_offset MIN")
+                raise ConcretizeArgument(2, policy="MIN")
 
         # account for calldata usage
         self._use_calldata(data_offset, size)
         self._allocate(mem_offset, size)
+        if size > consts.calldata_max_offset:
+            logger.info("CALLDATACOPY absurd size %d. OOG policy used: %r", size, consts.oog)
+            raise TerminateState(
+                "CALLDATACOPY absurd size %d. OOG policy used: %r" % (size, consts.oog),
+                testcase=True,
+            )
+
         for i in range(size):
             try:
                 c = Operators.ITEBV(
@@ -1796,8 +1824,7 @@ def MSTORE_gas(self, address, value):
     def MSTORE(self, address, value):
         """Save word to memory"""
         if istainted(self.pc):
-            for taint in get_taints(self.pc):
-                value = taint_with(value, taint)
+            value = taint_with(value, *get_taints(self.pc))
         self._allocate(address, 32)
         self._store(address, value, 32)
 

tests/ethereum/contracts/detectors/balance_not_ok.sol

@@ -0,0 +1,12 @@
+contract DetectThis {
+    event Log(string);
+    function foo() payable public{
+        uint256 eth2;
+        uint256 eth = msg.value;
+        eth2 = address(msg.sender).balance;
+        if(eth2 == eth){
+            emit Log("Found a bug");
+        }
+    }
+}
+

tests/ethereum/contracts/detectors/balance_ok.sol

@@ -0,0 +1,12 @@
+contract DetectThis {
+    event Log(string);
+    function foo() payable public{
+        uint256 eth2;
+        uint256 eth = msg.value;
+        eth2 = address(msg.sender).balance;
+        if(eth2 >= eth){
+            emit Log("Found a bug");
+        }
+    }
+}
+

tests/ethereum/test_detectors.py

@@ -19,6 +19,7 @@
     DetectExternalCallAndLeak,
     DetectEnvInstruction,
     DetectRaceCondition,
+    DetectManipulableBalance,
     State,
 )
 from manticore.ethereum.plugins import LoopDepthLimiter
@@ -390,5 +391,19 @@ def test_race_condition2(self):
         )
 
 
+class EthBalance(EthDetectorTest):
+    """ Test the detection of funny delegatecalls """
+
+    DETECTOR_CLASS = DetectManipulableBalance
+
+    def test_balance_ok(self):
+        name = inspect.currentframe().f_code.co_name[5:]
+        self._test(name, set())
+
+    def test_balance_not_ok(self):
+        name = inspect.currentframe().f_code.co_name[5:]
+        self._test(name, {(("Manipulable balance used in a strict comparison", False))})
+
+
 if __name__ == "__main__":
     unittest.main()

tests/ethereum/test_general.py

@@ -1313,8 +1313,17 @@ def test_concretizer(self):
         def inner_func(self, a, b):
             return a, b
 
+        class X:
+            class Y:
+                class Z:
+                    instruction = "instruction"
+
+                current_vm = Z()
+
+            world = Y()
+
         with self.assertRaises(ConcretizeArgument) as cm:
-            inner_func(None, self.bv, 34)
+            inner_func(X(), self.bv, 34)
 
         self.assertEqual(cm.exception.pos, 1)
         self.assertEqual(cm.exception.policy, policy)
@@ -1324,8 +1333,17 @@ def test_concretizer_default(self):
         def inner_func(self, a, b):
             return a, b
 
+        class X:
+            class Y:
+                class Z:
+                    instruction = "instruction"
+
+                current_vm = Z()
+
+            world = Y()
+
         with self.assertRaises(ConcretizeArgument) as cm:
-            inner_func(None, 34, self.bv)
+            inner_func(X(), 34, self.bv)
 
         self.assertEqual(cm.exception.pos, 2)
         # Make sure the policy isn't blank, i.e. we didn't pass through