From 6d364d01448f0d70d8643bfdae17985f42345dd3 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Tue, 8 May 2018 12:27:26 +0200 Subject: [PATCH] Use proper taint analysis from laser --- TOY.sol | 17 ++++++++ mythril/analysis/modules/integer.py | 44 +++++++++------------ tests/mythril_dir/signatures.json | 1 + tests/testdata/input_contracts/overflow.sol | 1 - 4 files changed, 36 insertions(+), 27 deletions(-) create mode 100644 TOY.sol create mode 100644 tests/mythril_dir/signatures.json diff --git a/TOY.sol b/TOY.sol new file mode 100644 index 00000000..bcc810fd --- /dev/null +++ b/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); + } +} diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index 51e28f22..b85adb1b 100644 --- a/mythril/analysis/modules/integer.py +++ b/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_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): +def _check_jumpi(state, taint_result): """ 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 _check_taint(condition, expression) + return taint_result.check(state, -2) -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 _check_taint(value, expression) + return taint_result.check(state, -2) -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 diff --git a/tests/mythril_dir/signatures.json b/tests/mythril_dir/signatures.json new file mode 100644 index 00000000..350ab336 --- /dev/null +++ b/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()"} \ No newline at end of file diff --git a/tests/testdata/input_contracts/overflow.sol b/tests/testdata/input_contracts/overflow.sol index 5d511797..f61a8b0e 100644 --- a/tests/testdata/input_contracts/overflow.sol +++ b/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; }