evm: Fix MUL overflow false positive (#767)

* initial

* Add test for mul checker

* clean

* Rename and clean

* Rm testing

* Better comment, and clean

* Split tests, add more tests

* Clean up stuff, remove unnecessary masking

* fmt

* Add back constrain to make it match the originall buggy situation

* Clean up surrounding code, make it unit testable

* Correct name

* Use individual arguments for helpers

manticore/ethereum.py

@@ -1,7 +1,7 @@
 import string
 
 from . import Manticore
-from .core.smtlib import ConstraintSet, Operators, solver, issymbolic, Array, Expression, Constant
+from .core.smtlib import ConstraintSet, Operators, solver, issymbolic, Array, Expression, Constant, operators
 from .core.smtlib.visitors import arithmetic_simplifier
 from .platforms import evm
 from .core.state import State
@@ -55,13 +55,30 @@ class IntegerOverflow(Detector):
     '''
         Detects potential overflow and underflow conditions on ADD and SUB instructions.
     '''
+    @staticmethod
+    def _can_add_overflow(state, result, a, b):
+        # TODO FIXME (mark) this is using a signed LT. need to check if this is correct
+        return state.can_be_true(result < a) or state.can_be_true(result < b)
+
+    @staticmethod
+    def _can_mul_overflow(state, result, a, b):
+        return state.can_be_true(operators.ULT(result, a) & operators.ULT(result, b))
+
+    @staticmethod
+    def _can_sub_underflow(state, a, b):
+        return state.can_be_true(b > a)
+
     def did_evm_execute_instruction_callback(self, state, instruction, arguments, result):
         mnemonic = instruction.semantics
-        if mnemonic in ('ADD', 'MUL'):
+
-            if state.can_be_true(result < arguments[0]) or state.can_be_true(result < arguments[1]):
+        if mnemonic == 'ADD':
+            if self._can_add_overflow(state, result, *arguments):
+                self.add_finding(state, "Integer overflow at {} instruction".format(mnemonic))
+        elif mnemonic == 'MUL':
+            if self._can_mul_overflow(state, result, *arguments):
                 self.add_finding(state, "Integer overflow at {} instruction".format(mnemonic))
         elif mnemonic == 'SUB':
-            if state.can_be_true(arguments[1] > arguments[0]):
+            if self._can_sub_underflow(state, *arguments):
                 self.add_finding(state, "Integer underflow at {} instruction".format(mnemonic))
             
 class UninitializedMemory(Detector):

tests/test_eth.py

@@ -1,15 +1,20 @@
 import unittest
 import os
 
+from manticore.core.smtlib import ConstraintSet, operators
+from manticore.core.state import State
 from manticore.ethereum import ManticoreEVM, IntegerOverflow, Detector
+from manticore.platforms.evm import EVMWorld
 
 THIS_DIR = os.path.dirname(os.path.abspath(__file__))
 
 # FIXME(mark): Remove these two lines when logging works for ManticoreEVM
 from manticore.utils.log import init_logging
+
 init_logging()
 
-class EthDetectors(unittest.TestCase):
+
+class EthDetectorsIntegrationTest(unittest.TestCase):
     def test_int_ovf(self):
         mevm = ManticoreEVM()
         mevm.register_detector(IntegerOverflow())
@@ -21,6 +26,50 @@ class EthDetectors(unittest.TestCase):
         self.assertIn('overflow at ADD', all_findings)
         self.assertIn('overflow at MUL', all_findings)
 
+
+class EthDetectors(unittest.TestCase):
+    def setUp(self):
+        self.io = IntegerOverflow()
+        self.state = self.make_mock_evm_state()
+
+    @staticmethod
+    def make_mock_evm_state():
+        cs = ConstraintSet()
+        fakestate = State(cs, EVMWorld(cs))
+        return fakestate
+
+    def test_mul_no_overflow(self):
+        """
+        Regression test added for issue 714, where we were using the ADD ovf check for MUL
+        """
+        arguments = [1 << (8 * 31), self.state.new_symbolic_value(256)]
+        self.state.constrain(operators.ULT(arguments[1], 256))
+
+        # TODO(mark) We should actually call into the EVM cpu here, and below, rather than
+        # effectively copy pasting what the MUL does
+        result = arguments[0] * arguments[1]
+
+        check = self.io._can_mul_overflow(self.state, result, *arguments)
+        self.assertFalse(check)
+
+    def test_mul_overflow0(self):
+        arguments = [2 << (8 * 31), self.state.new_symbolic_value(256)]
+        self.state.constrain(operators.ULT(arguments[1], 256))
+
+        result = arguments[0] * arguments[1]
+
+        check = self.io._can_mul_overflow(self.state, result, *arguments)
+        self.assertTrue(check)
+
+    def test_mul_overflow1(self):
+        arguments = [1 << 255, self.state.new_symbolic_value(256)]
+
+        result = arguments[0] * arguments[1]
+
+        check = self.io._can_mul_overflow(self.state, result, *arguments)
+        self.assertTrue(check)
+
+
 class EthTests(unittest.TestCase):
     def test_emit_did_execute_end_instructions(self):
         class TestDetector(Detector):