Use proper taint analysis from laser

TOY.sol

@@ -0,0 +1,17 @@
+pragma solidity ^0.4.2;
+
+contract TOY  {
+
+    address public owner;
+    bool public FLAG;
+
+    modifier checkOwner {
+        require(msg.sender == owner);  _;
+    }
+
+    function TOY() { owner = msg.sender; }
+    function setFlag(bool newFLAG) public { FLAG = newFLAG;  }
+    function boom() public checkOwner {
+        selfdestruct(owner);
+    }
+}

mythril/analysis/modules/integer.py

@@ -3,6 +3,7 @@ from mythril.analysis import solver
 from mythril.analysis.ops import *
 from mythril.analysis.report import Issue
 from mythril.exceptions import UnsatError
+from laser.ethereum.taint_analysis import TaintRunner
 import re
 import copy
 import logging
@@ -204,55 +205,40 @@ def _check_integer_underflow(statespace, state, node):
     return issues
 
 
-def _check_usage(state, expression):
+def _check_usage(state, taint_result):
     """Delegates checks to _check_{instruction_name}()"""
     opcode = state.get_current_instruction()['opcode']
 
     if opcode == 'JUMPI':
-        if _check_jumpi(state, expression):
+        if _check_jumpi(state, taint_result):
             return [state]
     elif opcode == 'SSTORE':
-        if _check_sstore(state, expression):
+        if _check_sstore(state, taint_result):
             return [state]
     return []
 
-
+def _check_jumpi(state, taint_result):
-def _check_taint(statement, expression):
-    """Checks if statement is influenced by tainted expression"""
-    _expression, _statement = str(expression).replace(' ', ''), str(statement).replace(' ', '')
-    found = _expression in _statement
-
-    if found:
-        i = _statement.index(_expression)
-        char = _statement[i - 1]
-        if char == '_':
-            return False
-    return found
-
-
-def _check_jumpi(state, expression):
     """ Check if conditional jump is dependent on the result of expression"""
     logging.debug(state.get_current_instruction()['opcode'])
     assert state.get_current_instruction()['opcode'] == 'JUMPI'
-    condition = state.mstate.stack[-2]
+    return taint_result.check(state, -2)
-    return _check_taint(condition, expression)
 
 
-def _check_sstore(state, expression):
+def _check_sstore(state, taint_result):
     """ Check if store operation is dependent on the result of expression"""
     logging.debug(state.get_current_instruction()['opcode'])
     assert state.get_current_instruction()['opcode'] == 'SSTORE'
-    value = state.mstate.stack[-2]
+    return taint_result.check(state, -2)
-    return _check_taint(value, expression)
 
 
-def _search_children(statespace, node, expression, constraint=[], index=0, depth=0, max_depth=64):
+def _search_children(statespace, node, expression, taint_result=None, constraint=[], index=0, depth=0, max_depth=64):
     """
     Checks the statespace for children states, with JUMPI or SSTORE instuctions,
     for dependency on expression
     :param statespace: The statespace to explore
     :param node: Current node to explore from
     :param expression: Expression to look for
+    :param taint_result: Result of taint analysis
     :param index: Current state index node.states[index] == current_state
     :param depth: Current depth level
     :param max_depth: Max depth to explore
@@ -260,6 +246,12 @@ def _search_children(statespace, node, expression, constraint=[], index=0, depth
     """
     logging.debug("SEARCHING NODE for usage of an overflowed variable %d", node.uid)
 
+    if taint_result == None:
+        state = node.states[index]
+        taint_stack = [False for _ in state.mstate.stack]
+        taint_stack[-1] = True
+        taint_result = TaintRunner.execute(statespace, node, state, initial_stack=taint_stack)
+
     results = []
 
     if depth >= max_depth:
@@ -270,7 +262,7 @@ def _search_children(statespace, node, expression, constraint=[], index=0, depth
         current_state = node.states[j]
         current_instruction = current_state.get_current_instruction()
         if current_instruction['opcode'] in ('JUMPI', 'SSTORE'):
-            element = _check_usage(current_state, expression)
+            element = _check_usage(current_state, taint_result)
             if len(element) < 1:
                 continue
             # if _check_requires(element[0], node, statespace, constraint):
@@ -287,7 +279,7 @@ def _search_children(statespace, node, expression, constraint=[], index=0, depth
         ]
 
     for child in children:
-        results += _search_children(statespace, child, expression, depth=depth + 1, max_depth=max_depth)
+        results += _search_children(statespace, child, expression, taint_result, depth=depth + 1, max_depth=max_depth)
 
     return results
 

tests/mythril_dir/signatures.json

@@ -0,0 +1 @@
+{"0xd132391a": "setSaleEndTime(uint256)", "0xdb3b6263": "transitionToState(uint256,BountyStages)", "0xd7bb99ba": "contribute()", "0x605120cf": "validPurchase())", "0x2aa5ed61": "DayLimit(uint256)", "0x412664ae": "sendToken(address,uint256)", "0xfdacd576": "setCompleted(uint256)", "0x5a048d78": "claim(Target)", "0xf3fef3a3": "withdraw(address,uint256)", "0xba51a6df": "changeRequirement(uint256)", "0xec8ac4d8": "buyTokens(address)", "0xa0e67e2b": "getOwners()", "0x42a6b21a": "getContributionLimit(address)", "0x00362a95": "donate(address)", "0x422d4cd6": "increasePayout(uint256,uint256,uint256)", "0x86647bac": "getBountyArbiter(uint256)", "0xf3fde261": "onTransition(bytes32)", "0x8b51d13f": "getConfirmationCount(uint256)", "0x180aadb7": "underLimit(uint256)", "0xe20056e6": "replaceOwner(address,address)", "0xb94b0a3a": "getFulfillment(uint256,uint256)", "0xa3210e87": "sendeth(address,uint256)", "0xf8b2cb4f": "getBalance(address)", "0x66188463": "decreaseApproval(address,uint256)", "0xb5dc40c3": "getConfirmations(uint256)", "0xf3d3402a": "changeBountyData(uint256,string)", "0xe7dde9a3": "_setDailyLimit(uint256)", "0xd9583497": "acceptFulfillment(uint256,uint256)", "0x0a0cd8c8": "setupDone()", "0x7bd703e8": "getBalanceInEth(address)", "0xd6d22fa4": "MetaCoin()", "0x2e1a7d4d": "withdraw(uint256)", "0xe5c46944": "MultiSigWallet(address[],uint256)", "0x2a4f6533": "createTokenContract())", "0x6241bfd1": "Token(uint256)", "0x5d19606e": "transferIssuer(uint256,address)", "0x6c343ffe": "withdrawfunds()", "0x19045a25": "recover(bytes32,bytes)", "0x200094e0": "deployContract())", "0x1e688c14": "fulfillBounty(uint256,string)", "0x16b57509": "killBounty(uint256)", "0xaa3288f4": "getBalance())", "0xcae9ca51": "approveAndCall(address,uint256,bytes)", "0x70a08231": "balanceOf(address)", "0x56885cd8": "crowdfunding()", "0xc01a8c84": "confirmTransaction(uint256)", "0x9d4468ff": "today())", "0x2d1fdef6": "extendDeadline(uint256,uint256)", "0x4a4c82c6": "_resetSpentToday()", "0x992a3e75": "changeBountyPaysTokens(uint256,bool,address)", "0x4bc9fdc2": "calcMaxWithdraw()", "0xdd62ed3e": "allowance(address,address)", "0xc6427474": "submitTransaction(address,uint256,bytes)", "0x16ae6b67": "checkInvariant())", "0x07f9f7ba": "StandardBounties(address)", "0x20ea8d86": "revokeConfirmation(uint256)", "0xcdad6576": "changeBountyArbiter(uint256,address)", "0xe92dfb23": "LimitBalance(uint256)", "0xa8abe69a": "getTransactionIds(uint256,uint256,bool,bool)", "0x23b872dd": "transferFrom(address,address,uint256)", "0x8c590917": "contribute(uint256,uint256)", "0xc11a4b47": "Origin()", "0xf2fde38b": "transferOwnership(address)", "0x9d735286": "forwardFunds()", "0x173825d9": "removeOwner(address)", "0xd6c0ceab": "changeBountyDeadline(uint256,uint256)", "0x1a787915": "startConditions(bytes32)", "0xa360b26f": "Migrations()", "0xec096f8d": "addTransaction(address,uint256,bytes)", "0xee8c4bbf": "getBounty(uint256)", "0x90b98a11": "sendCoin(address,uint256)", "0xabaf5880": "Crowdsale(uint256,uint256,uint256,address)", "0xc9e61599": "createTarget())", "0x7065cb48": "addOwner(address)", "0x452ccadb": "changeBountyFulfillmentAmount(uint256,uint256)", "0x626a413a": "activateBounty(uint256,uint256)", "0xf0349d5f": "setupStages()", "0xd73dd623": "increaseApproval(address,uint256)", "0xfbe334f8": "getNumFulfillments(uint256)", "0x19dba3d2": "getBountyToken(uint256)", "0x525f8a5c": "setSaleStartTime(uint256)", "0xe8b5e51f": "invest()", "0xa9059cbb": "transfer(address,uint256)", "0x6e42787f": "hasEnded())", "0x091cde0b": "DisbursementHandler(address)", "0x4e3b52fe": "metaCoin()", "0xee22610b": "executeTransaction(uint256)", "0x54741525": "getTransactionCount(bool,bool)", "0x0900f010": "upgrade(address)", "0xcd38aa87": "chooseWinner()", "0xa60745aa": "getBountyData(uint256)", "0x095ea7b3": "approve(address,uint256)", "0x41ac5dd0": "updateFulfillment(uint256,uint256,string)", "0x784547a7": "isConfirmed(uint256)", "0x27816235": "onSaleEnded()", "0x3278ba2f": "getNumBounties()"}

tests/testdata/input_contracts/overflow.sol

@@ -11,7 +11,6 @@ contract Over {
     require(balances[msg.sender] - _value >= 0);
     balances[msg.sender] -= _value;
     balances[_to] += _value;
-    balances[_to] = 2;
     return true;
   }