From c6a0644c460189d4cdf2f3d15177d40df5f6969c Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Sun, 28 Oct 2018 19:37:44 +0100 Subject: [PATCH 01/10] fix missing call variable --- mythril/analysis/modules/dependence_on_predictable_vars.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/mythril/analysis/modules/dependence_on_predictable_vars.py b/mythril/analysis/modules/dependence_on_predictable_vars.py index d390c047..ea7095d1 100644 --- a/mythril/analysis/modules/dependence_on_predictable_vars.py +++ b/mythril/analysis/modules/dependence_on_predictable_vars.py @@ -66,7 +66,7 @@ def execute(statespace): function_name=call.node.function_name, address=address, swc_id=swc_type, - bytecode=state.environment.code.bytecode, + bytecode=call.state.environment.code.bytecode, title="Dependence on predictable environment variable", _type="Warning", description=description, @@ -144,7 +144,7 @@ def execute(statespace): contract=call.node.contract_name, function_name=call.node.function_name, address=address, - bytecode=state.environment.code.bytecode, + bytecode=call.state.environment.code.bytecode, title="Dependence on predictable variable", _type="Informational", description=description, From 0f8e9144a64d22dac51757d20b7282df5cfb8a17 Mon Sep 17 00:00:00 2001 From: Haozhong Zhang Date: Tue, 16 Oct 2018 16:55:58 +0800 Subject: [PATCH 02/10] analysis/transaction_order_dependence: import missing `copy` module in transaction_order_dependence.py copy.deepcopy() is used in transaction_order_dependence.py, but the `copy` module is not imported. --- mythril/analysis/modules/transaction_order_dependence.py | 1 + 1 file changed, 1 insertion(+) diff --git a/mythril/analysis/modules/transaction_order_dependence.py b/mythril/analysis/modules/transaction_order_dependence.py index 4528459c..9db7c104 100644 --- a/mythril/analysis/modules/transaction_order_dependence.py +++ b/mythril/analysis/modules/transaction_order_dependence.py @@ -1,5 +1,6 @@ import logging import re +import copy from mythril.analysis import solver from mythril.analysis.ops import * From ce4075b8df3e8d6bcfdd309b91b3a3fad2177f3d Mon Sep 17 00:00:00 2001 From: Haozhong Zhang Date: Tue, 9 Oct 2018 13:52:12 +0800 Subject: [PATCH 03/10] laser/instruction: remove unused solver in sstore_() --- mythril/laser/ethereum/instructions.py | 5 ----- 1 file changed, 5 deletions(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index c31d5f46..cabdaba1 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -18,7 +18,6 @@ from z3 import ( URem, SRem, BitVec, - Solver, is_true, BitVecVal, If, @@ -43,7 +42,6 @@ from mythril.laser.ethereum.transaction import ( TransactionStartSignal, ContractCreationTransaction, ) -from mythril.analysis.solver import get_model TT256 = 2 ** 256 TT256M1 = 2 ** 256 - 1 @@ -924,9 +922,6 @@ class Instruction: storage_keys = global_state.environment.active_account.storage.keys() keccak_keys = filter(keccak_function_manager.is_keccak, storage_keys) - solver = Solver() - solver.set(timeout=1000) - results = [] new = False From 725bfec464594070d568f6a24880abd16afb05a4 Mon Sep 17 00:00:00 2001 From: Haozhong Zhang Date: Tue, 30 Oct 2018 20:53:30 +0800 Subject: [PATCH 04/10] laser/instruction: simplify before checking by Z3 is_true() Z3 is_true() does not automatically consider `expr == expr` to be true, so `is_true(key_argument == index_argument)` in `sstore_()` will miss lots of positive conditions and then generate lots of unnecessary subsequent paths. Take the following contract for example ``` contract Foo { mapping(address => uint) public balances; function bar(address _to, uint256 _value) public { require(balances[_to] + _value >= balances[_to]); balances[_to] += _value; balances[_to] += _value; } ``` Before this commit, - 772 nodes/771 edges/8288 states are generated. After this commit, - only 237 nodes/236 edges/3204 states are generated. --- mythril/laser/ethereum/instructions.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index cabdaba1..edefece9 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -929,7 +929,7 @@ class Instruction: key_argument = keccak_function_manager.get_argument(keccak_key) index_argument = keccak_function_manager.get_argument(index) - if is_true(key_argument == index_argument): + if is_true(simplify(key_argument == index_argument)): return self._sstore_helper( copy(global_state), keccak_key, From 91015e63baae514393e0cb6a7ea64e80a3b93d67 Mon Sep 17 00:00:00 2001 From: Haozhong Zhang Date: Tue, 30 Oct 2018 21:17:06 +0800 Subject: [PATCH 05/10] analysis/integer: remove unnecessary deepcopy of constraints `solver.get_model()` has no way to mutate constraints passed to it, so the expensive deepcopy of constraints before calling `solver.get_model()`is unnecessary. --- mythril/analysis/modules/integer.py | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index b5c952f8..4e6f9b25 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -127,11 +127,8 @@ def _try_constraints(constraints, new_constraints): Tries new constraints :return Model if satisfiable otherwise None """ - _constraints = copy.deepcopy(constraints) - for constraint in new_constraints: - _constraints.append(copy.deepcopy(constraint)) try: - model = solver.get_model(_constraints) + model = solver.get_model(constraints + new_constraints) return model except UnsatError: return None From adeec0264f36de23656eeb38cbf4a9a22f3ddc56 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Wed, 31 Oct 2018 12:28:51 +0100 Subject: [PATCH 06/10] subtraction typo fix --- mythril/analysis/modules/integer.py | 2 +- tests/testdata/outputs_expected/overflow.sol.o.json | 2 +- tests/testdata/outputs_expected/overflow.sol.o.markdown | 4 ++-- tests/testdata/outputs_expected/overflow.sol.o.text | 4 ++-- tests/testdata/outputs_expected/underflow.sol.o.json | 2 +- tests/testdata/outputs_expected/underflow.sol.o.markdown | 4 ++-- tests/testdata/outputs_expected/underflow.sol.o.text | 4 ++-- 7 files changed, 11 insertions(+), 11 deletions(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index 54926a6a..df0d8988 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -210,7 +210,7 @@ def _check_integer_underflow(statespace, state, node): ) issue.description = ( - "The substraction can result in an integer underflow.\n" + "The subtraction can result in an integer underflow.\n" ) issue.debug = "Transaction Sequence: " + str( diff --git a/tests/testdata/outputs_expected/overflow.sol.o.json b/tests/testdata/outputs_expected/overflow.sol.o.json index fb92acaf..d651908c 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 substraction 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 substraction 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": "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 diff --git a/tests/testdata/outputs_expected/overflow.sol.o.markdown b/tests/testdata/outputs_expected/overflow.sol.o.markdown index 4f86063c..f042f183 100644 --- a/tests/testdata/outputs_expected/overflow.sol.o.markdown +++ b/tests/testdata/outputs_expected/overflow.sol.o.markdown @@ -9,7 +9,7 @@ ### Description -The substraction can result in an integer underflow. +The subtraction can result in an integer underflow. ## Integer Underflow - SWC ID: 101 @@ -20,7 +20,7 @@ The substraction can result in an integer underflow. ### Description -The substraction can result in an integer underflow. +The subtraction can result in an integer underflow. ## Integer Overflow - SWC ID: 101 diff --git a/tests/testdata/outputs_expected/overflow.sol.o.text b/tests/testdata/outputs_expected/overflow.sol.o.text index acdce40b..ad480ffd 100644 --- a/tests/testdata/outputs_expected/overflow.sol.o.text +++ b/tests/testdata/outputs_expected/overflow.sol.o.text @@ -4,7 +4,7 @@ Type: Warning Contract: Unknown Function name: sendeth(address,uint256) PC address: 567 -The substraction can result in an integer underflow. +The subtraction can result in an integer underflow. -------------------- @@ -14,7 +14,7 @@ Type: Warning Contract: Unknown Function name: sendeth(address,uint256) PC address: 649 -The substraction can result in an integer underflow. +The subtraction can result in an integer underflow. -------------------- diff --git a/tests/testdata/outputs_expected/underflow.sol.o.json b/tests/testdata/outputs_expected/underflow.sol.o.json index fb92acaf..d651908c 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 substraction 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 substraction 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": "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 diff --git a/tests/testdata/outputs_expected/underflow.sol.o.markdown b/tests/testdata/outputs_expected/underflow.sol.o.markdown index 4f86063c..f042f183 100644 --- a/tests/testdata/outputs_expected/underflow.sol.o.markdown +++ b/tests/testdata/outputs_expected/underflow.sol.o.markdown @@ -9,7 +9,7 @@ ### Description -The substraction can result in an integer underflow. +The subtraction can result in an integer underflow. ## Integer Underflow - SWC ID: 101 @@ -20,7 +20,7 @@ The substraction can result in an integer underflow. ### Description -The substraction can result in an integer underflow. +The subtraction can result in an integer underflow. ## Integer Overflow - SWC ID: 101 diff --git a/tests/testdata/outputs_expected/underflow.sol.o.text b/tests/testdata/outputs_expected/underflow.sol.o.text index acdce40b..ad480ffd 100644 --- a/tests/testdata/outputs_expected/underflow.sol.o.text +++ b/tests/testdata/outputs_expected/underflow.sol.o.text @@ -4,7 +4,7 @@ Type: Warning Contract: Unknown Function name: sendeth(address,uint256) PC address: 567 -The substraction can result in an integer underflow. +The subtraction can result in an integer underflow. -------------------- @@ -14,7 +14,7 @@ Type: Warning Contract: Unknown Function name: sendeth(address,uint256) PC address: 649 -The substraction can result in an integer underflow. +The subtraction can result in an integer underflow. -------------------- From 0d0d8e5ac3cdaaaf8a16f585dd278587c25263e5 Mon Sep 17 00:00:00 2001 From: Haozhong Zhang Date: Wed, 31 Oct 2018 19:55:49 +0800 Subject: [PATCH 07/10] dependencies: bump the minimal Z3 version to 4.8 Following commits will use overflow checking APIs that are only available in newer versions of Z3. --- requirements.txt | 2 +- setup.py | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/requirements.txt b/requirements.txt index d829a885..3691a704 100644 --- a/requirements.txt +++ b/requirements.txt @@ -24,5 +24,5 @@ pytest_mock requests rlp>=1.0.1 transaction>=2.2.1 -z3-solver>=4.5 +z3-solver>=4.8 pysha3 diff --git a/setup.py b/setup.py index 6aa0dfb7..c52d2153 100755 --- a/setup.py +++ b/setup.py @@ -75,7 +75,7 @@ setup( install_requires=[ "coloredlogs>=10.0", "ethereum>=2.3.2", - "z3-solver>=4.5", + "z3-solver>=4.8", "requests", "py-solc", "plyvel", From ee674ff803d7f309fd5b296ce51f4d0c47a0d7a2 Mon Sep 17 00:00:00 2001 From: Haozhong Zhang Date: Wed, 31 Oct 2018 11:30:30 +0800 Subject: [PATCH 08/10] analysis/integer: fix the overflow check of bit vector multiplication Differently than the bit vector addition, an overflowed bit vector multiplication does not necessarily result in a value less than any of its operands (e.g., the multiplication of two 8-bit vectors 0x7 and 4 produces 0xC). Fix this issue by using Z3 BVMulNoOverflow in the overflow check of bit vector multiplication. --- mythril/analysis/modules/integer.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index df0d8988..709d2c2e 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -72,11 +72,12 @@ def _check_integer_overflow(statespace, state, node): # Formulate expression if instruction["opcode"] == "ADD": expr = op0 + op1 + constraint = Or(And(ULT(expr, op0), op1 != 0), And(ULT(expr, op1), op0 != 0)) else: expr = op1 * op0 + constraint = Not(BVMulNoOverflow(op0, op1, signed=False)) # Check satisfiable - constraint = Or(And(ULT(expr, op0), op1 != 0), And(ULT(expr, op1), op0 != 0)) model = _try_constraints(node.constraints, [constraint]) if model is None: From a982a7d7fd461c2b670a43e9544164de3ae84b5e Mon Sep 17 00:00:00 2001 From: Haozhong Zhang Date: Wed, 31 Oct 2018 19:58:46 +0800 Subject: [PATCH 09/10] analysis/integer: switch addition overflow check to dedicated Z3 API Use Z3 API BVAddNoOverflow() in the constraint to check the bit vector addition overflow. --- 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 709d2c2e..bb75c550 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -72,7 +72,7 @@ def _check_integer_overflow(statespace, state, node): # Formulate expression if instruction["opcode"] == "ADD": expr = op0 + op1 - constraint = Or(And(ULT(expr, op0), op1 != 0), And(ULT(expr, op1), op0 != 0)) + constraint = Not(BVAddNoOverflow(op0, op1, signed=False)) else: expr = op1 * op0 constraint = Not(BVMulNoOverflow(op0, op1, signed=False)) From 9cbf1d55e5781fdae8ec64f18b9edb5f15b732f8 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Wed, 31 Oct 2018 20:57:37 +0100 Subject: [PATCH 10/10] revert changes to support z3 4.5 --- mythril/analysis/modules/integer.py | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index 8916ed13..aea9ff06 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -72,11 +72,12 @@ def _check_integer_overflow(statespace, state, node): # Formulate expression if instruction["opcode"] == "ADD": expr = op0 + op1 - constraint = Not(BVAddNoOverflow(op0, op1, signed=False)) + # constraint = Not(BVAddNoOverflow(op0, op1, signed=False)) else: expr = op1 * op0 - constraint = Not(BVMulNoOverflow(op0, op1, signed=False)) + # constraint = Not(BVMulNoOverflow(op0, op1, signed=False)) + constraint = Or(And(ULT(expr, op0), op1 != 0), And(ULT(expr, op1), op0 != 0)) # Check satisfiable model = _try_constraints(node.constraints, [constraint])