eth int overflow: tests, mul support (#656)

* Move algorithm into ManticoreEVM

* Rm buggy unused line

* Initial eth testing setup

* Check for overflow in mul also

* clarifying comment

* Install solc for travis

* Add sudo

* x

* Rm travis_retry, since we rarely actually use it, and it's not available in this script for some reason

* Check for specific findings

* Fix test

* Clean up transaction firing logic

* Use less strict check, better for floating point

.travis.yml

@@ -15,8 +15,6 @@ os:
 python:
 - 2.7.13
 install:
-- travis_retry pip install -U pip
-- travis_retry pip uninstall -y Manticore || echo "Manticore not cached"  # uninstall any old, cached Manticore
-- travis_retry pip install --no-binary keystone-engine -e .[dev]  # ks can have pip install issues
+- scripts/travis_install.sh
 script:
 - scripts/travis_test.sh

manticore/__main__.py

@@ -84,29 +84,7 @@ def ethereum_cli(args):
 
     logger.info("Beginning analysis")
 
-    with open(args.argv[0]) as f:
-        source_code = f.read()
-
-    user_account = m.create_account(balance=1000)
-    contract_account = m.solidity_create_contract(source_code, owner=user_account)
-    attacker_account = m.create_account(balance=1000)
-
-    last_coverage = None
-    new_coverage = 0
-    while new_coverage != last_coverage and new_coverage < 100:
-
-        symbolic_data = m.make_symbolic_buffer(320)
-        symbolic_value = m.make_symbolic_value()
-
-        m.transaction(caller=attacker_account,
-                         address=contract_account,
-                         data=symbolic_data,
-                         value=symbolic_value )
-
-        last_coverage = new_coverage
-        new_coverage = m.global_coverage(contract_account)
-
-    m.finalize()
+    m.multi_tx_analysis(args.argv[0])
 
 def main():
     log.init_logging()

manticore/seth.py

@@ -54,13 +54,13 @@ class IntegerOverflow(Detector):
         Detects any it overflow on instructions ADD and SUB.
     '''
     def did_evm_execute_instruction_callback(self, state, instruction, arguments, result):
-        if instruction.semantics == 'ADD':
+        mnemonic = instruction.semantics
+        if mnemonic in ('ADD', 'MUL'):
             if state.can_be_true(result < arguments[0]) or state.can_be_true(result < arguments[1]):
-                self.add_finding(state, "Integer overflow at ADD instruction")
-        if instruction.semantics == 'SUB':
+                self.add_finding(state, "Integer overflow at {} instruction".format(mnemonic))
+        elif mnemonic == 'SUB':
             if state.can_be_true(arguments[1] > arguments[0]):
-                src = self._get_src(state)
-                self.add_finding(state, "Integer underflow at SUB instruction")
+                self.add_finding(state, "Integer underflow at {} instruction".format(mnemonic))
             
 class UnitializedMemory(Detector):
     '''
@@ -823,6 +823,37 @@ class ManticoreEVM(Manticore):
 
         return status
 
+    def multi_tx_analysis(self, solidity_filename):
+        with open(solidity_filename) as f:
+            source_code = f.read()
+
+        user_account = self.create_account(balance=1000)
+        contract_account = self.solidity_create_contract(source_code, owner=user_account)
+        attacker_account = self.create_account(balance=1000)
+
+        prev_coverage = 0
+        current_coverage = 0
+
+        while current_coverage < 100:
+
+            symbolic_data = self.make_symbolic_buffer(320)
+            symbolic_value = self.make_symbolic_value()
+
+            self.transaction(caller=attacker_account,
+                          address=contract_account,
+                          data=symbolic_data,
+                          value=symbolic_value )
+
+            prev_coverage = current_coverage
+            current_coverage = self.global_coverage(contract_account)
+            found_new_coverage = prev_coverage < current_coverage
+
+            if not found_new_coverage:
+                break
+
+        self.finalize()
+
+
     def run(self, **kwargs):
         ''' Run any pending transaction on any running state '''
 

scripts/travis_install.sh

@@ -0,0 +1,12 @@
+#!/usr/bin/env bash
+
+function install_solc {
+    sudo wget -O /usr/bin/solc https://github.com/ethereum/solidity/releases/download/v0.4.19/solc-static-linux
+    sudo chmod +x /usr/bin/solc
+}
+
+install_solc
+
+pip install -U pip
+pip uninstall -y Manticore || echo "Manticore not cached"  # uninstall any old, cached Manticore
+pip install --no-binary keystone-engine -e .[dev]  # ks can have pip install issues

tests/binaries/int_overflow.sol

@@ -0,0 +1,13 @@
+contract IntOverflowUnderflow {
+    function intoverflow_add(uint input) {
+        uint local = input + 1;
+    }
+
+    function intoverflow_mul(uint input) {
+        uint local = input * 2;
+    }
+
+    function intunderflow(uint input) {
+        uint local = input - 1;
+    }
+}

tests/test_eth.py

@@ -0,0 +1,22 @@
+import unittest
+import os
+
+from manticore.seth import ManticoreEVM, IntegerOverflow
+
+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):
+    def test_int_ovf(self):
+        mevm = ManticoreEVM()
+        mevm.register_detector(IntegerOverflow())
+        filename = os.path.join(THIS_DIR, 'binaries/int_overflow.sol')
+        mevm.multi_tx_analysis(filename)
+        self.assertEqual(len(mevm.global_findings), 3)
+        all_findings = ''.join(map(lambda x: x[2], mevm.global_findings))
+        self.assertIn('underflow at SUB', all_findings)
+        self.assertIn('overflow at ADD', all_findings)
+        self.assertIn('overflow at MUL', all_findings)