From 85a941a2553d688d75aeb0afb63bbe2dbfe73c08 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Thu, 5 Apr 2018 00:21:55 +0200 Subject: [PATCH 01/12] Reformat code to separate integer under and overflow modules --- mythril/analysis/modules/integer.py | 77 +++++++++++++++++------------ 1 file changed, 46 insertions(+), 31 deletions(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index 941c8ebf..e3432730 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -7,7 +7,6 @@ import re import copy import logging - ''' MODULE DESCRIPTION: @@ -17,7 +16,11 @@ For every SUB instruction, check if there's a possible state where op1 > op0. def execute(statespace): - + """ + Executes analysis module for integer underflow + :param statespace: Statespace to analyse + :return: Found issues + """ logging.debug("Executing module: INTEGER") issues = [] @@ -26,52 +29,64 @@ def execute(statespace): node = statespace.nodes[k] for state in node.states: + logging.debug("Checking for integer underflow") + issues += _check_integer_underflow(state, node) + logging.debug("Checking for integer overflow") + issues += _check_integer_overflow(state, node) - instruction = state.get_current_instruction() + return issues - if(instruction['opcode'] == "SUB"): - stack = state.mstate.stack +def _check_integer_overflow(state, node): + return [] - op0 = stack[-1] - op1 = stack[-2] - constraints = copy.deepcopy(node.constraints) +def _check_integer_underflow(state, node): + issues = [] + instruction = state.get_current_instruction() - if type(op0) == int and type(op1) == int: - continue + if instruction['opcode'] == "SUB": - if (re.search(r'calldatasize_', str(op0))) \ - or (re.search(r'256\*.*If\(1', str(op0), re.DOTALL) or re.search(r'256\*.*If\(1', str(op1), re.DOTALL)) \ - or (re.search(r'32 \+.*calldata', str(op0), re.DOTALL) or re.search(r'32 \+.*calldata', str(op1), re.DOTALL)): + stack = state.mstate.stack - # Filter for patterns that contain bening nteger underflows. + op0 = stack[-1] + op1 = stack[-2] - # Pattern 1: (96 + calldatasize_MAIN) - (96), where (96 + calldatasize_MAIN) would underflow if calldatasize is very large. - # Pattern 2: (256*If(1 & storage_0 == 0, 1, 0)) - 1, this would underlow if storage_0 = 0 + constraints = copy.deepcopy(node.constraints) - continue + # Filter for patterns that contain bening nteger underflows. - logging.debug("[INTEGER_UNDERFLOW] Checking SUB " + str(op0) + ", " + str(op1) + " at address " + str(instruction['address'])) + # Pattern 1: (96 + calldatasize_MAIN) - (96), where (96 + calldatasize_MAIN) would underflow if calldatasize is very large. + # Pattern 2: (256*If(1 & storage_0 == 0, 1, 0)) - 1, this would underlow if storage_0 = 0 + if type(op0) == int and type(op1) == int: + return + if re.search(r'calldatasize_', str(op0)): + return + if re.search(r'256\*.*If\(1', str(op0), re.DOTALL) or re.search(r'256\*.*If\(1', str(op1), re.DOTALL): + return + if re.search(r'32 \+.*calldata', str(op0), re.DOTALL) or re.search(r'32 \+.*calldata', str(op1), re.DOTALL): + return - allowed_types = [int, BitVecRef, BitVecNumRef] + logging.debug("[INTEGER_UNDERFLOW] Checking SUB {0}, {1} at address {2}".format(str(op0), str(op1), + str(instruction['address']))) - if type(op0) in allowed_types and type(op1) in allowed_types: - constraints.append(UGT(op1,op0)) + allowed_types = [int, BitVecRef, BitVecNumRef] - try: + if type(op0) in allowed_types and type(op1) in allowed_types: + constraints.append(UGT(op1, op0)) - model = solver.get_model(constraints) + try: - issue = Issue(node.contract_name, node.function_name, instruction['address'], "Integer Underflow", "Warning") + model = solver.get_model(constraints) - issue.description = "A possible integer underflow exists in the function " + node.function_name + ".\n" \ - "The subtraction may result in a value < 0." + issue = Issue(node.contract_name, node.function_name, instruction['address'], "Integer Underflow", + "Warning") - issue.debug = solver.pretty_print_model(model) - issues.append(issue) + issue.description = "A possible integer underflow exists in the function " + node.function_name + ".\n" \ + "The subtraction may result in a value < 0." - except UnsatError: - logging.debug("[INTEGER_UNDERFLOW] no model found") + issue.debug = solver.pretty_print_model(model) + issues.append(issue) - return issues + except UnsatError: + logging.debug("[INTEGER_UNDERFLOW] no model found") From 398677a557ed035f2e0be453dc5bcb0903bc3ff9 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Thu, 5 Apr 2018 00:35:28 +0200 Subject: [PATCH 02/12] Implement initial integer overflow analysis --- mythril/analysis/modules/integer.py | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index e3432730..ef65d6bf 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -38,6 +38,34 @@ def execute(statespace): def _check_integer_overflow(state, node): + """Checks if an overflow occurs""" + issues = [] + + # Check the instruction + instruction = state.get_current_instruction() + if instruction['opcode'] != "ADD": + return + + constraints = copy.deepcopy(node.constraints) + + stack = state.mstate.stack + op0, op1 = stack[-1], stack[-2] + constraints.append(UGT(op0 + op1, (2 ** 32) - 1)) + + try: + model = solver.get_model(constraints) + + issue = Issue(node.contract_name, node.function_name, instruction['address'], "Integer Underflow", + "Warning") + + issue.description = "A possible integer overflow exists in the function {}.\n " \ + "Addition will result in a lower value".format(node.function_name) + issue.debug = solver.pretty_print_model(model) + issues.append(issue) + + except UnsatError: + logging.debug("[INTEGER_UNDERFLOW] no model found") + return [] From aa5db8ba3b60e9065199fd1d298ad024afb8afc3 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Thu, 5 Apr 2018 00:41:07 +0200 Subject: [PATCH 03/12] Add function documentation --- mythril/analysis/modules/integer.py | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index ef65d6bf..a773eb80 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -38,7 +38,12 @@ def execute(statespace): def _check_integer_overflow(state, node): - """Checks if an overflow occurs""" + """ + Checks for integer overflow + :param state: state from node to examine + :param node: node to examine + :return: found issue + """ issues = [] # Check the instruction @@ -48,8 +53,11 @@ def _check_integer_overflow(state, node): constraints = copy.deepcopy(node.constraints) + # Formulate overflow constraints stack = state.mstate.stack op0, op1 = stack[-1], stack[-2] + + # An integer overflow is possible if op0 + op1, constraints.append(UGT(op0 + op1, (2 ** 32) - 1)) try: From b087826bad60fa4f78e2d55c994b37059f12040c Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Thu, 5 Apr 2018 00:41:25 +0200 Subject: [PATCH 04/12] Create test overflow solidity file --- tests/testdata/inputs/overflow.sol | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) create mode 100644 tests/testdata/inputs/overflow.sol diff --git a/tests/testdata/inputs/overflow.sol b/tests/testdata/inputs/overflow.sol new file mode 100644 index 00000000..f61a8b0e --- /dev/null +++ b/tests/testdata/inputs/overflow.sol @@ -0,0 +1,20 @@ +contract Over { + + mapping(address => uint) balances; + uint public totalSupply; + + function Token(uint _initialSupply) { + balances[msg.sender] = totalSupply = _initialSupply; + } + + function sendeth(address _to, uint _value) public returns (bool) { + require(balances[msg.sender] - _value >= 0); + balances[msg.sender] -= _value; + balances[_to] += _value; + return true; + } + + function balanceOf(address _owner) public constant returns (uint balance) { + return balances[_owner]; + } +} From b6128f1d8ef365498861d5ba3221915b8ad07f5d Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Thu, 5 Apr 2018 01:03:23 +0200 Subject: [PATCH 05/12] Make sure an empty list is returned, instead of None --- mythril/analysis/modules/integer.py | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index a773eb80..c43eca62 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -49,7 +49,7 @@ def _check_integer_overflow(state, node): # Check the instruction instruction = state.get_current_instruction() if instruction['opcode'] != "ADD": - return + return [] constraints = copy.deepcopy(node.constraints) @@ -63,7 +63,7 @@ def _check_integer_overflow(state, node): try: model = solver.get_model(constraints) - issue = Issue(node.contract_name, node.function_name, instruction['address'], "Integer Underflow", + issue = Issue(node.contract_name, node.function_name, instruction['address'], "Integer Overflow ", "Warning") issue.description = "A possible integer overflow exists in the function {}.\n " \ @@ -74,7 +74,7 @@ def _check_integer_overflow(state, node): except UnsatError: logging.debug("[INTEGER_UNDERFLOW] no model found") - return [] + return issues def _check_integer_underflow(state, node): @@ -95,13 +95,13 @@ def _check_integer_underflow(state, node): # Pattern 1: (96 + calldatasize_MAIN) - (96), where (96 + calldatasize_MAIN) would underflow if calldatasize is very large. # Pattern 2: (256*If(1 & storage_0 == 0, 1, 0)) - 1, this would underlow if storage_0 = 0 if type(op0) == int and type(op1) == int: - return + return [] if re.search(r'calldatasize_', str(op0)): - return + return [] if re.search(r'256\*.*If\(1', str(op0), re.DOTALL) or re.search(r'256\*.*If\(1', str(op1), re.DOTALL): - return + return [] if re.search(r'32 \+.*calldata', str(op0), re.DOTALL) or re.search(r'32 \+.*calldata', str(op1), re.DOTALL): - return + return [] logging.debug("[INTEGER_UNDERFLOW] Checking SUB {0}, {1} at address {2}".format(str(op0), str(op1), str(instruction['address']))) @@ -126,3 +126,4 @@ def _check_integer_underflow(state, node): except UnsatError: logging.debug("[INTEGER_UNDERFLOW] no model found") + return issues From 86a9b852d6428da12b1ad8988280e91423de586b Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Thu, 5 Apr 2018 02:31:22 +0200 Subject: [PATCH 06/12] add function documentation --- mythril/analysis/modules/integer.py | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index c43eca62..fe0dd8ad 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -78,6 +78,12 @@ def _check_integer_overflow(state, node): def _check_integer_underflow(state, node): + """ + Checks for integer underflow + :param state: state from node to examine + :param node: node to examine + :return: found issue + """ issues = [] instruction = state.get_current_instruction() From d995789aadea4ae3d5d7f1deb7a4b701797189c0 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Thu, 5 Apr 2018 02:36:28 +0200 Subject: [PATCH 07/12] Add expected output --- myth | 2 + .../outputs_expected/overflow.sol.easm | 365 ++++++++++++++++++ .../outputs_expected/overflow.sol.graph.html | 168 ++++++++ .../outputs_expected/overflow.sol.json | 39 ++ .../outputs_expected/overflow.sol.markdown | 46 +++ .../outputs_expected/overflow.sol.text | 42 ++ 6 files changed, 662 insertions(+) create mode 100644 tests/testdata/outputs_expected/overflow.sol.easm create mode 100644 tests/testdata/outputs_expected/overflow.sol.graph.html create mode 100644 tests/testdata/outputs_expected/overflow.sol.json create mode 100644 tests/testdata/outputs_expected/overflow.sol.markdown create mode 100644 tests/testdata/outputs_expected/overflow.sol.text diff --git a/myth b/myth index 83c41a09..8ebdc1a2 100755 --- a/myth +++ b/myth @@ -33,6 +33,8 @@ from mythril.analysis.traceexplore import get_serializable_statespace from mythril.analysis.security import fire_lasers from mythril.analysis.report import Report +# logging.basicConfig(level=logging.DEBUG) + def searchCallback(code_hash, code, addresses, balances): print("Matched contract with code hash " + code_hash) diff --git a/tests/testdata/outputs_expected/overflow.sol.easm b/tests/testdata/outputs_expected/overflow.sol.easm new file mode 100644 index 00000000..0ed8f651 --- /dev/null +++ b/tests/testdata/outputs_expected/overflow.sol.easm @@ -0,0 +1,365 @@ +0 PUSH1 0x60 +2 PUSH1 0x40 +4 MSTORE +5 PUSH1 0x04 +7 CALLDATASIZE +8 LT +9 PUSH2 0x0062 +12 JUMPI +13 PUSH1 0x00 +15 CALLDATALOAD +16 PUSH29 0x0100000000000000000000000000000000000000000000000000000000 +46 SWAP1 +47 DIV +48 PUSH4 0xffffffff +53 AND +54 DUP1 +55 PUSH4 0x18160ddd +60 EQ +61 PUSH2 0x0067 +64 JUMPI +65 DUP1 +66 PUSH4 0x6241bfd1 +71 EQ +72 PUSH2 0x0090 +75 JUMPI +76 DUP1 +77 PUSH4 0x70a08231 +82 EQ +83 PUSH2 0x00b3 +86 JUMPI +87 DUP1 +88 PUSH4 0xa3210e87 +93 EQ +94 PUSH2 0x0100 +97 JUMPI +98 JUMPDEST +99 PUSH1 0x00 +101 DUP1 +102 REVERT +103 JUMPDEST +104 CALLVALUE +105 ISZERO +106 PUSH2 0x0072 +109 JUMPI +110 PUSH1 0x00 +112 DUP1 +113 REVERT +114 JUMPDEST +115 PUSH2 0x007a +118 PUSH2 0x015a +121 JUMP +122 JUMPDEST +123 PUSH1 0x40 +125 MLOAD +126 DUP1 +127 DUP3 +128 DUP2 +129 MSTORE +130 PUSH1 0x20 +132 ADD +133 SWAP2 +134 POP +135 POP +136 PUSH1 0x40 +138 MLOAD +139 DUP1 +140 SWAP2 +141 SUB +142 SWAP1 +143 RETURN +144 JUMPDEST +145 CALLVALUE +146 ISZERO +147 PUSH2 0x009b +150 JUMPI +151 PUSH1 0x00 +153 DUP1 +154 REVERT +155 JUMPDEST +156 PUSH2 0x00b1 +159 PUSH1 0x04 +161 DUP1 +162 DUP1 +163 CALLDATALOAD +164 SWAP1 +165 PUSH1 0x20 +167 ADD +168 SWAP1 +169 SWAP2 +170 SWAP1 +171 POP +172 POP +173 PUSH2 0x0160 +176 JUMP +177 JUMPDEST +178 STOP +179 JUMPDEST +180 CALLVALUE +181 ISZERO +182 PUSH2 0x00be +185 JUMPI +186 PUSH1 0x00 +188 DUP1 +189 REVERT +190 JUMPDEST +191 PUSH2 0x00ea +194 PUSH1 0x04 +196 DUP1 +197 DUP1 +198 CALLDATALOAD +199 PUSH20 0xffffffffffffffffffffffffffffffffffffffff +220 AND +221 SWAP1 +222 PUSH1 0x20 +224 ADD +225 SWAP1 +226 SWAP2 +227 SWAP1 +228 POP +229 POP +230 PUSH2 0x01ab +233 JUMP +234 JUMPDEST +235 PUSH1 0x40 +237 MLOAD +238 DUP1 +239 DUP3 +240 DUP2 +241 MSTORE +242 PUSH1 0x20 +244 ADD +245 SWAP2 +246 POP +247 POP +248 PUSH1 0x40 +250 MLOAD +251 DUP1 +252 SWAP2 +253 SUB +254 SWAP1 +255 RETURN +256 JUMPDEST +257 CALLVALUE +258 ISZERO +259 PUSH2 0x010b +262 JUMPI +263 PUSH1 0x00 +265 DUP1 +266 REVERT +267 JUMPDEST +268 PUSH2 0x0140 +271 PUSH1 0x04 +273 DUP1 +274 DUP1 +275 CALLDATALOAD +276 PUSH20 0xffffffffffffffffffffffffffffffffffffffff +297 AND +298 SWAP1 +299 PUSH1 0x20 +301 ADD +302 SWAP1 +303 SWAP2 +304 SWAP1 +305 DUP1 +306 CALLDATALOAD +307 SWAP1 +308 PUSH1 0x20 +310 ADD +311 SWAP1 +312 SWAP2 +313 SWAP1 +314 POP +315 POP +316 PUSH2 0x01f3 +319 JUMP +320 JUMPDEST +321 PUSH1 0x40 +323 MLOAD +324 DUP1 +325 DUP3 +326 ISZERO +327 ISZERO +328 ISZERO +329 ISZERO +330 DUP2 +331 MSTORE +332 PUSH1 0x20 +334 ADD +335 SWAP2 +336 POP +337 POP +338 PUSH1 0x40 +340 MLOAD +341 DUP1 +342 SWAP2 +343 SUB +344 SWAP1 +345 RETURN +346 JUMPDEST +347 PUSH1 0x01 +349 SLOAD +350 DUP2 +351 JUMP +352 JUMPDEST +353 DUP1 +354 PUSH1 0x01 +356 DUP2 +357 SWAP1 +358 SSTORE +359 PUSH1 0x00 +361 DUP1 +362 CALLER +363 PUSH20 0xffffffffffffffffffffffffffffffffffffffff +384 AND +385 PUSH20 0xffffffffffffffffffffffffffffffffffffffff +406 AND +407 DUP2 +408 MSTORE +409 PUSH1 0x20 +411 ADD +412 SWAP1 +413 DUP2 +414 MSTORE +415 PUSH1 0x20 +417 ADD +418 PUSH1 0x00 +420 SHA3 +421 DUP2 +422 SWAP1 +423 SSTORE +424 POP +425 POP +426 JUMP +427 JUMPDEST +428 PUSH1 0x00 +430 DUP1 +431 PUSH1 0x00 +433 DUP4 +434 PUSH20 0xffffffffffffffffffffffffffffffffffffffff +455 AND +456 PUSH20 0xffffffffffffffffffffffffffffffffffffffff +477 AND +478 DUP2 +479 MSTORE +480 PUSH1 0x20 +482 ADD +483 SWAP1 +484 DUP2 +485 MSTORE +486 PUSH1 0x20 +488 ADD +489 PUSH1 0x00 +491 SHA3 +492 SLOAD +493 SWAP1 +494 POP +495 SWAP2 +496 SWAP1 +497 POP +498 JUMP +499 JUMPDEST +500 PUSH1 0x00 +502 DUP1 +503 DUP3 +504 PUSH1 0x00 +506 DUP1 +507 CALLER +508 PUSH20 0xffffffffffffffffffffffffffffffffffffffff +529 AND +530 PUSH20 0xffffffffffffffffffffffffffffffffffffffff +551 AND +552 DUP2 +553 MSTORE +554 PUSH1 0x20 +556 ADD +557 SWAP1 +558 DUP2 +559 MSTORE +560 PUSH1 0x20 +562 ADD +563 PUSH1 0x00 +565 SHA3 +566 SLOAD +567 SUB +568 LT +569 ISZERO +570 ISZERO +571 ISZERO +572 PUSH2 0x0244 +575 JUMPI +576 PUSH1 0x00 +578 DUP1 +579 REVERT +580 JUMPDEST +581 DUP2 +582 PUSH1 0x00 +584 DUP1 +585 CALLER +586 PUSH20 0xffffffffffffffffffffffffffffffffffffffff +607 AND +608 PUSH20 0xffffffffffffffffffffffffffffffffffffffff +629 AND +630 DUP2 +631 MSTORE +632 PUSH1 0x20 +634 ADD +635 SWAP1 +636 DUP2 +637 MSTORE +638 PUSH1 0x20 +640 ADD +641 PUSH1 0x00 +643 SHA3 +644 PUSH1 0x00 +646 DUP3 +647 DUP3 +648 SLOAD +649 SUB +650 SWAP3 +651 POP +652 POP +653 DUP2 +654 SWAP1 +655 SSTORE +656 POP +657 DUP2 +658 PUSH1 0x00 +660 DUP1 +661 DUP6 +662 PUSH20 0xffffffffffffffffffffffffffffffffffffffff +683 AND +684 PUSH20 0xffffffffffffffffffffffffffffffffffffffff +705 AND +706 DUP2 +707 MSTORE +708 PUSH1 0x20 +710 ADD +711 SWAP1 +712 DUP2 +713 MSTORE +714 PUSH1 0x20 +716 ADD +717 PUSH1 0x00 +719 SHA3 +720 PUSH1 0x00 +722 DUP3 +723 DUP3 +724 SLOAD +725 ADD +726 SWAP3 +727 POP +728 POP +729 DUP2 +730 SWAP1 +731 SSTORE +732 POP +733 PUSH1 0x01 +735 SWAP1 +736 POP +737 SWAP3 +738 SWAP2 +739 POP +740 POP +741 JUMP +742 STOP diff --git a/tests/testdata/outputs_expected/overflow.sol.graph.html b/tests/testdata/outputs_expected/overflow.sol.graph.html new file mode 100644 index 00000000..982a1479 --- /dev/null +++ b/tests/testdata/outputs_expected/overflow.sol.graph.html @@ -0,0 +1,168 @@ + + + + + + + + + + + + +

Mythril / LASER Symbolic VM

+


+ + + diff --git a/tests/testdata/outputs_expected/overflow.sol.json b/tests/testdata/outputs_expected/overflow.sol.json new file mode 100644 index 00000000..8f826cb2 --- /dev/null +++ b/tests/testdata/outputs_expected/overflow.sol.json @@ -0,0 +1,39 @@ +{ + "success": true, + "error": null, + "issues": [ + { + "title": "Integer Underflow", + "description": "A possible integer underflow exists in the function sendeth(address,uint256).\nThe subtraction may result in a value < 0.", + "function": "sendeth(address,uint256)", + "type": "Warning", + "address": 649, + "debug": "", + "filename": "/inputs/overflow.sol", + "lineno": 12, + "code": "balances[msg.sender] -= _value" + }, + { + "title": "Integer Overflow ", + "description": "A possible integer overflow exists in the function sendeth(address,uint256).\n Addition will result in a lower value", + "function": "sendeth(address,uint256)", + "type": "Warning", + "address": 725, + "debug": "", + "filename": "/inputs/overflow.sol", + "lineno": 13, + "code": "balances[_to] += _value" + }, + { + "title": "Integer Underflow", + "description": "A possible integer underflow exists in the function sendeth(address,uint256).\nThe subtraction may result in a value < 0.", + "function": "sendeth(address,uint256)", + "type": "Warning", + "address": 567, + "debug": "", + "filename": "/inputs/overflow.sol", + "lineno": 11, + "code": "balances[msg.sender] - _value" + } + ] +} \ No newline at end of file diff --git a/tests/testdata/outputs_expected/overflow.sol.markdown b/tests/testdata/outputs_expected/overflow.sol.markdown new file mode 100644 index 00000000..13cd479a --- /dev/null +++ b/tests/testdata/outputs_expected/overflow.sol.markdown @@ -0,0 +1,46 @@ +# Analysis Results +## Integer Underflow +- Type: Warning +- Contract: Over +- Function name: `sendeth(address,uint256)` +- PC address: 649 + +### Description +A possible integer underflow exists in the function sendeth(address,uint256). +The subtraction may result in a value < 0. + +In */inputs/overflow.sol:12* + +``` +balances[msg.sender] -= _value +``` +## Integer Overflow +- Type: Warning +- Contract: Over +- Function name: `sendeth(address,uint256)` +- PC address: 725 + +### Description +A possible integer overflow exists in the function sendeth(address,uint256). + Addition will result in a lower value + +In */inputs/overflow.sol:13* + +``` +balances[_to] += _value +``` +## Integer Underflow +- Type: Warning +- Contract: Over +- Function name: `sendeth(address,uint256)` +- PC address: 567 + +### Description +A possible integer underflow exists in the function sendeth(address,uint256). +The subtraction may result in a value < 0. + +In */inputs/overflow.sol:11* + +``` +balances[msg.sender] - _value +``` diff --git a/tests/testdata/outputs_expected/overflow.sol.text b/tests/testdata/outputs_expected/overflow.sol.text new file mode 100644 index 00000000..d1e92a78 --- /dev/null +++ b/tests/testdata/outputs_expected/overflow.sol.text @@ -0,0 +1,42 @@ +==== Integer Underflow ==== +Type: Warning +Contract: Over +Function name: sendeth(address,uint256) +PC address: 649 +A possible integer underflow exists in the function sendeth(address,uint256). +The subtraction may result in a value < 0. +-------------------- +In file: /inputs/overflow.sol:12 + +balances[msg.sender] -= _value + +-------------------- + +==== Integer Overflow ==== +Type: Warning +Contract: Over +Function name: sendeth(address,uint256) +PC address: 725 +A possible integer overflow exists in the function sendeth(address,uint256). + Addition will result in a lower value +-------------------- +In file: /inputs/overflow.sol:13 + +balances[_to] += _value + +-------------------- + +==== Integer Underflow ==== +Type: Warning +Contract: Over +Function name: sendeth(address,uint256) +PC address: 567 +A possible integer underflow exists in the function sendeth(address,uint256). +The subtraction may result in a value < 0. +-------------------- +In file: /inputs/overflow.sol:11 + +balances[msg.sender] - _value + +-------------------- + From 8b0f6d4ec845e18d3973856fe0803bdf54730e14 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Mon, 9 Apr 2018 21:05:47 +0200 Subject: [PATCH 08/12] Initial implementation of check whether overflowed value gets used --- mythril/analysis/modules/integer.py | 76 +++++++++++++++++++++++++++-- 1 file changed, 73 insertions(+), 3 deletions(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index fe0dd8ad..99301ee3 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -32,14 +32,15 @@ def execute(statespace): logging.debug("Checking for integer underflow") issues += _check_integer_underflow(state, node) logging.debug("Checking for integer overflow") - issues += _check_integer_overflow(state, node) + issues += _check_integer_overflow(statespace, state, node) return issues -def _check_integer_overflow(state, node): +def _check_integer_overflow(statespace, state, node): """ Checks for integer overflow + :param statespace: statespace that is being examined :param state: state from node to examine :param node: node to examine :return: found issue @@ -63,11 +64,16 @@ def _check_integer_overflow(state, node): try: model = solver.get_model(constraints) + # If we get to this point then there has been an integer overflow + interesting_usages = _search_children(statespace, node, (op0 + op1), index=node.states.index(state)) + if len(interesting_usages) == 0: + return issues + issue = Issue(node.contract_name, node.function_name, instruction['address'], "Integer Overflow ", "Warning") issue.description = "A possible integer overflow exists in the function {}.\n " \ - "Addition will result in a lower value".format(node.function_name) + "Addition will result in a lower value.".format(node.function_name) issue.debug = solver.pretty_print_model(model) issues.append(issue) @@ -133,3 +139,67 @@ def _check_integer_underflow(state, node): except UnsatError: logging.debug("[INTEGER_UNDERFLOW] no model found") return issues + + +MAX_SEARCH_DEPTH = 64 + + +def _check_usage(state, expression): + """Delegates checks to _check_{instruction_name}()""" + opcode = state.get_current_instruction()['opcode'] + + if opcode == 'JUMPI': + if _check_jumpi(state, expression): + return [state] + elif opcode == 'SSTORE': + if _check_sstore(state, expression): + return [state] + return [] + + +def _check_jumpi(state, expression): + """ Check if conditional jump is dependent on the result of expression""" + assert state.get_current_instruction()['opcode'] is 'JUMPI' + condition = state.mstate.stack[-2] + return str(expression) in str(condition) + + +def _check_sstore(state, expression): + """ Check if store operation is dependent on the result of expression""" + assert state.get_current_instruction()['opcode'] is 'SSTORE' + value = state.mstate.stack[-2] + return str(expression) in str(value) + + +def _search_children(statespace, node, expression, index=0, depth=0, analyze=_check_usage, opcodes=('JUMPI', 'SSTORE')): + """ + Checks the statespace for child states with instructions that match the opcodes and see if their elements are + dependent on expression. + :param statespace: The statespace to explore + :param node: Current node to explore from + :param expression: expression to look for + :param index: Current state index node.states[index] == current_state + :param depth: Current depth level + :param analyze: Analysis method, returns array of positive children + :param opcodes: opcodes to look for + :return: List of states that match the opcodes and are dependent on expression + """ + logging.debug("SEARCHING NODE %d", node.uid) + + results = [] + + if depth >= MAX_SEARCH_DEPTH: + return [] + + for j in range(index, len(node.states)): + current_state = node.states[j] + current_instruction = current_state.get_current_instruction() + if current_instruction['opcode'] in opcodes: + results += analyze(current_state, expression) + + children = [edge.node_to for edge in statespace.edges if edge.node_from is node] + for child in children: + results += _search_children(statespace, child, depth=depth+1, analyze=analyze, opcodes=opcodes) + + return results + From a70c861e2140fc94872d692ddcfd974dd0d2e7c4 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Mon, 9 Apr 2018 21:15:46 +0200 Subject: [PATCH 09/12] Clean up method. and documentation --- mythril/analysis/modules/integer.py | 30 +++++++++++++++-------------- tests/testdata/inputs/overflow.sol | 1 + 2 files changed, 17 insertions(+), 14 deletions(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index 99301ee3..62213982 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -12,6 +12,7 @@ MODULE DESCRIPTION: Check for integer underflows. For every SUB instruction, check if there's a possible state where op1 > op0. +For every ADD instruction, check if there's a possible state where op1 + op0 > 2^32 - 1 ''' @@ -65,7 +66,10 @@ def _check_integer_overflow(statespace, state, node): model = solver.get_model(constraints) # If we get to this point then there has been an integer overflow + # Find out if the overflowed value is actually used interesting_usages = _search_children(statespace, node, (op0 + op1), index=node.states.index(state)) + + # Stop if it isn't if len(interesting_usages) == 0: return issues @@ -141,9 +145,6 @@ def _check_integer_underflow(state, node): return issues -MAX_SEARCH_DEPTH = 64 - - def _check_usage(state, expression): """Delegates checks to _check_{instruction_name}()""" opcode = state.get_current_instruction()['opcode'] @@ -171,35 +172,36 @@ def _check_sstore(state, expression): return str(expression) in str(value) -def _search_children(statespace, node, expression, index=0, depth=0, analyze=_check_usage, opcodes=('JUMPI', 'SSTORE')): +def _search_children(statespace, node, expression, index=0, depth=0, max_depth=64): """ - Checks the statespace for child states with instructions that match the opcodes and see if their elements are - dependent on expression. + 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 expression: Expression to look for :param index: Current state index node.states[index] == current_state :param depth: Current depth level - :param analyze: Analysis method, returns array of positive children - :param opcodes: opcodes to look for + :param max_depth: Max depth to explore :return: List of states that match the opcodes and are dependent on expression """ logging.debug("SEARCHING NODE %d", node.uid) results = [] - if depth >= MAX_SEARCH_DEPTH: + if depth >= max_depth: return [] + # Explore current node from index for j in range(index, len(node.states)): current_state = node.states[j] current_instruction = current_state.get_current_instruction() - if current_instruction['opcode'] in opcodes: - results += analyze(current_state, expression) + if current_instruction['opcode'] in ('JUMPI', 'SSTORE'): + results += _check_usage(current_state, expression) - children = [edge.node_to for edge in statespace.edges if edge.node_from is node] + # Recursively search children + children = [statespace.nodes[edge.node_to] for edge in statespace.edges if edge.node_from == node.uid] for child in children: - results += _search_children(statespace, child, depth=depth+1, analyze=analyze, opcodes=opcodes) + results += _search_children(statespace, child, depth=depth+1, max_depth=max_depth) return results diff --git a/tests/testdata/inputs/overflow.sol b/tests/testdata/inputs/overflow.sol index f61a8b0e..5d511797 100644 --- a/tests/testdata/inputs/overflow.sol +++ b/tests/testdata/inputs/overflow.sol @@ -11,6 +11,7 @@ contract Over { require(balances[msg.sender] - _value >= 0); balances[msg.sender] -= _value; balances[_to] += _value; + balances[_to] = 2; return true; } From 8d11a4541b73c44b5c84b1c71dd81f4d9e7ced9b Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Mon, 9 Apr 2018 21:19:50 +0200 Subject: [PATCH 10/12] Adapt debug logging string --- mythril/analysis/modules/integer.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index 62213982..6f3c7031 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -184,7 +184,7 @@ def _search_children(statespace, node, expression, index=0, depth=0, max_depth=6 :param max_depth: Max depth to explore :return: List of states that match the opcodes and are dependent on expression """ - logging.debug("SEARCHING NODE %d", node.uid) + logging.debug("SEARCHING NODE for usage of an overflowed variable %d", node.uid) results = [] From 425bd17a9673d38924365e5e057358bebbad9a93 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Mon, 9 Apr 2018 21:22:47 +0200 Subject: [PATCH 11/12] Adapt debug line --- mythril/analysis/modules/integer.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index 6f3c7031..8210fe59 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -82,7 +82,7 @@ def _check_integer_overflow(statespace, state, node): issues.append(issue) except UnsatError: - logging.debug("[INTEGER_UNDERFLOW] no model found") + logging.debug("[INTEGER_OVERFLOW] no model found") return issues From 5d1fbe97ad4da5b3a5c36a6f73f7b51bc3bbee2a Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Tue, 10 Apr 2018 19:07:06 +0200 Subject: [PATCH 12/12] Add missing expression argument --- mythril/analysis/modules/integer.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index 8210fe59..f1ad92d1 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -201,7 +201,7 @@ def _search_children(statespace, node, expression, index=0, depth=0, max_depth=6 # Recursively search children children = [statespace.nodes[edge.node_to] for edge in statespace.edges if edge.node_from == node.uid] for child in children: - results += _search_children(statespace, child, depth=depth+1, max_depth=max_depth) + results += _search_children(statespace, child, expression, depth=depth+1, max_depth=max_depth) return results