From 6b794fecaa65e38d56ca7bd7e6ea2a9156842f35 Mon Sep 17 00:00:00 2001 From: Mark Mossberg Date: Thu, 21 Dec 2017 12:54:24 -0500 Subject: [PATCH] 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 | 4 +--- manticore/__main__.py | 24 +------------------ manticore/seth.py | 41 +++++++++++++++++++++++++++++---- scripts/travis_install.sh | 12 ++++++++++ tests/binaries/int_overflow.sol | 13 +++++++++++ tests/test_eth.py | 22 ++++++++++++++++++ 6 files changed, 85 insertions(+), 31 deletions(-) create mode 100755 scripts/travis_install.sh create mode 100644 tests/binaries/int_overflow.sol create mode 100644 tests/test_eth.py diff --git a/.travis.yml b/.travis.yml index a42109c..49cb438 100644 --- a/.travis.yml +++ b/.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 diff --git a/manticore/__main__.py b/manticore/__main__.py index 668ab6d..cf4a320 100644 --- a/manticore/__main__.py +++ b/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() diff --git a/manticore/seth.py b/manticore/seth.py index 93930f2..642f3ee 100644 --- a/manticore/seth.py +++ b/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 ''' diff --git a/scripts/travis_install.sh b/scripts/travis_install.sh new file mode 100755 index 0000000..aa88787 --- /dev/null +++ b/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 diff --git a/tests/binaries/int_overflow.sol b/tests/binaries/int_overflow.sol new file mode 100644 index 0000000..ddcec4d --- /dev/null +++ b/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; + } +} \ No newline at end of file diff --git a/tests/test_eth.py b/tests/test_eth.py new file mode 100644 index 0000000..c0f8828 --- /dev/null +++ b/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)