From f7ab134608c1309ffd8d4947d0a30dcd97a827b5 Mon Sep 17 00:00:00 2001 From: Dominik Muhs Date: Thu, 8 Nov 2018 20:47:18 +0100 Subject: [PATCH] Merge latest develop branch --- mythril/analysis/modules/integer.py | 12 ++++++------ .../testdata/outputs_expected/ether_send.sol.o.json | 2 +- .../outputs_expected/ether_send.sol.o.markdown | 2 +- .../testdata/outputs_expected/ether_send.sol.o.text | 2 +- tests/testdata/outputs_expected/overflow.sol.o.json | 2 +- .../outputs_expected/overflow.sol.o.markdown | 2 +- tests/testdata/outputs_expected/overflow.sol.o.text | 2 +- tests/testdata/outputs_expected/underflow.sol.o.json | 2 +- .../outputs_expected/underflow.sol.o.markdown | 2 +- tests/testdata/outputs_expected/underflow.sol.o.text | 2 +- 10 files changed, 15 insertions(+), 15 deletions(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index c82f12a8..b4489b5e 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -75,10 +75,13 @@ class IntegerOverflowUnderflowModule(DetectionModule): op1 = BitVecVal(op1, 256) # Formulate expression + # FIXME: handle exponentiation if instruction["opcode"] == "ADD": + operator = "add" expr = op0 + op1 # constraint = Not(BVAddNoOverflow(op0, op1, signed=False)) else: + operator = "multiply" expr = op1 * op0 # constraint = Not(BVMulNoOverflow(op0, op1, signed=False)) @@ -90,11 +93,6 @@ class IntegerOverflowUnderflowModule(DetectionModule): logging.debug("[INTEGER_OVERFLOW] no model found") return issues - if not self._verify_integer_overflow( - statespace, node, expr, state, model, constraint, op0, op1 - ): - return issues - # Build issue issue = Issue( contract=node.contract_name, @@ -106,7 +104,9 @@ class IntegerOverflowUnderflowModule(DetectionModule): _type="Warning", ) - issue.description = "The arithmetic operation can result in integer overflow.\n" + issue.description = "This binary {} operation can result in integer overflow.\n".format( + operator + ) issue.debug = "Transaction Sequence: " + str( solver.get_transaction_sequence(state, node.constraints) ) diff --git a/tests/testdata/outputs_expected/ether_send.sol.o.json b/tests/testdata/outputs_expected/ether_send.sol.o.json index 03d3f2d6..d4e504c3 100644 --- a/tests/testdata/outputs_expected/ether_send.sol.o.json +++ b/tests/testdata/outputs_expected/ether_send.sol.o.json @@ -1 +1 @@ -{"error": null, "issues": [{"address": 722, "contract": "Unknown", "debug": "", "description": "It seems that an attacker is able to execute an call instruction, this can mean that the attacker is able to extract funds out of the contract.", "function": "withdrawfunds()", "swc_id": "105", "title": "Ether send", "type": "Warning"}, {"address": 883, "contract": "Unknown", "debug": "", "description": "The arithmetic operation can result in integer overflow.\n", "function": "invest()", "swc_id": "101", "title": "Integer Overflow", "type": "Warning"}], "success": true} +{"error": null, "issues": [{"address": 722, "contract": "Unknown", "debug": "", "description": "It seems that an attacker is able to execute an call instruction, this can mean that the attacker is able to extract funds out of the contract.", "function": "withdrawfunds()", "swc_id": "105", "title": "Ether send", "type": "Warning"}, {"address": 883, "contract": "Unknown", "debug": "", "description": "This binary add operation can result in integer overflow.\n", "function": "invest()", "swc_id": "101", "title": "Integer Overflow", "type": "Warning"}], "success": true} \ No newline at end of file diff --git a/tests/testdata/outputs_expected/ether_send.sol.o.markdown b/tests/testdata/outputs_expected/ether_send.sol.o.markdown index c4e23873..e3dc9d83 100644 --- a/tests/testdata/outputs_expected/ether_send.sol.o.markdown +++ b/tests/testdata/outputs_expected/ether_send.sol.o.markdown @@ -20,4 +20,4 @@ It seems that an attacker is able to execute an call instruction, this can mean ### Description -The arithmetic operation can result in integer overflow. +This binary add operation can result in integer overflow. diff --git a/tests/testdata/outputs_expected/ether_send.sol.o.text b/tests/testdata/outputs_expected/ether_send.sol.o.text index 6be210d9..23ede087 100644 --- a/tests/testdata/outputs_expected/ether_send.sol.o.text +++ b/tests/testdata/outputs_expected/ether_send.sol.o.text @@ -13,7 +13,7 @@ Type: Warning Contract: Unknown Function name: invest() PC address: 883 -The arithmetic operation can result in integer overflow. +This binary add operation can result in integer overflow. -------------------- diff --git a/tests/testdata/outputs_expected/overflow.sol.o.json b/tests/testdata/outputs_expected/overflow.sol.o.json index d651908c..aaf15405 100644 --- a/tests/testdata/outputs_expected/overflow.sol.o.json +++ b/tests/testdata/outputs_expected/overflow.sol.o.json @@ -1 +1 @@ -{"error": null, "issues": [{"address": 567, "contract": "Unknown", "debug": "", "description": "The subtraction can result in an integer underflow.\n", "function": "sendeth(address,uint256)", "swc_id": "101", "title": "Integer Underflow", "type": "Warning"}, {"address": 649, "contract": "Unknown", "debug": "", "description": "The subtraction can result in an integer underflow.\n", "function": "sendeth(address,uint256)", "swc_id": "101", "title": "Integer Underflow", "type": "Warning"}, {"address": 725, "contract": "Unknown", "debug": "", "description": "The arithmetic operation can result in integer overflow.\n", "function": "sendeth(address,uint256)", "swc_id": "101", "title": "Integer Overflow", "type": "Warning"}], "success": true} \ No newline at end of file +{"error": null, "issues": [{"address": 567, "contract": "Unknown", "debug": "", "description": "The subtraction can result in an integer underflow.\n", "function": "sendeth(address,uint256)", "swc_id": "101", "title": "Integer Underflow", "type": "Warning"}, {"address": 649, "contract": "Unknown", "debug": "", "description": "The subtraction can result in an integer underflow.\n", "function": "sendeth(address,uint256)", "swc_id": "101", "title": "Integer Underflow", "type": "Warning"}, {"address": 725, "contract": "Unknown", "debug": "", "description": "This binary add operation can result in integer overflow.\n", "function": "sendeth(address,uint256)", "swc_id": "101", "title": "Integer Overflow", "type": "Warning"}], "success": true} \ No newline at end of file diff --git a/tests/testdata/outputs_expected/overflow.sol.o.markdown b/tests/testdata/outputs_expected/overflow.sol.o.markdown index f042f183..50d2e435 100644 --- a/tests/testdata/outputs_expected/overflow.sol.o.markdown +++ b/tests/testdata/outputs_expected/overflow.sol.o.markdown @@ -31,4 +31,4 @@ The subtraction can result in an integer underflow. ### Description -The arithmetic operation can result in integer overflow. +This binary add operation can result in integer overflow. diff --git a/tests/testdata/outputs_expected/overflow.sol.o.text b/tests/testdata/outputs_expected/overflow.sol.o.text index ad480ffd..ebbdabd3 100644 --- a/tests/testdata/outputs_expected/overflow.sol.o.text +++ b/tests/testdata/outputs_expected/overflow.sol.o.text @@ -24,7 +24,7 @@ Type: Warning Contract: Unknown Function name: sendeth(address,uint256) PC address: 725 -The arithmetic operation can result in integer overflow. +This binary add operation can result in integer overflow. -------------------- diff --git a/tests/testdata/outputs_expected/underflow.sol.o.json b/tests/testdata/outputs_expected/underflow.sol.o.json index d651908c..aaf15405 100644 --- a/tests/testdata/outputs_expected/underflow.sol.o.json +++ b/tests/testdata/outputs_expected/underflow.sol.o.json @@ -1 +1 @@ -{"error": null, "issues": [{"address": 567, "contract": "Unknown", "debug": "", "description": "The subtraction can result in an integer underflow.\n", "function": "sendeth(address,uint256)", "swc_id": "101", "title": "Integer Underflow", "type": "Warning"}, {"address": 649, "contract": "Unknown", "debug": "", "description": "The subtraction can result in an integer underflow.\n", "function": "sendeth(address,uint256)", "swc_id": "101", "title": "Integer Underflow", "type": "Warning"}, {"address": 725, "contract": "Unknown", "debug": "", "description": "The arithmetic operation can result in integer overflow.\n", "function": "sendeth(address,uint256)", "swc_id": "101", "title": "Integer Overflow", "type": "Warning"}], "success": true} \ No newline at end of file +{"error": null, "issues": [{"address": 567, "contract": "Unknown", "debug": "", "description": "The subtraction can result in an integer underflow.\n", "function": "sendeth(address,uint256)", "swc_id": "101", "title": "Integer Underflow", "type": "Warning"}, {"address": 649, "contract": "Unknown", "debug": "", "description": "The subtraction can result in an integer underflow.\n", "function": "sendeth(address,uint256)", "swc_id": "101", "title": "Integer Underflow", "type": "Warning"}, {"address": 725, "contract": "Unknown", "debug": "", "description": "This binary add operation can result in integer overflow.\n", "function": "sendeth(address,uint256)", "swc_id": "101", "title": "Integer Overflow", "type": "Warning"}], "success": true} \ No newline at end of file diff --git a/tests/testdata/outputs_expected/underflow.sol.o.markdown b/tests/testdata/outputs_expected/underflow.sol.o.markdown index f042f183..50d2e435 100644 --- a/tests/testdata/outputs_expected/underflow.sol.o.markdown +++ b/tests/testdata/outputs_expected/underflow.sol.o.markdown @@ -31,4 +31,4 @@ The subtraction can result in an integer underflow. ### Description -The arithmetic operation can result in integer overflow. +This binary add operation can result in integer overflow. diff --git a/tests/testdata/outputs_expected/underflow.sol.o.text b/tests/testdata/outputs_expected/underflow.sol.o.text index ad480ffd..ebbdabd3 100644 --- a/tests/testdata/outputs_expected/underflow.sol.o.text +++ b/tests/testdata/outputs_expected/underflow.sol.o.text @@ -24,7 +24,7 @@ Type: Warning Contract: Unknown Function name: sendeth(address,uint256) PC address: 725 -The arithmetic operation can result in integer overflow. +This binary add operation can result in integer overflow. --------------------