From a83fb67f454869dbfe7184bc0fe204123e0139b3 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Mon, 4 Feb 2019 08:59:45 +0100 Subject: [PATCH 01/22] add OverUndeflowStateAnnotation This annotation is used to keep track of traces which can have both an overflow, and use of that overflow --- mythril/analysis/modules/integer.py | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index 6cbfd5ac..9b141a5f 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -8,6 +8,7 @@ from mythril.analysis.report import Issue from mythril.analysis.swc_data import INTEGER_OVERFLOW_AND_UNDERFLOW from mythril.exceptions import UnsatError from mythril.laser.ethereum.state.global_state import GlobalState +from mythril.laser.ethereum.state.annotation import StateAnnotation from mythril.analysis.modules.base import DetectionModule from mythril.laser.smt import ( @@ -27,6 +28,17 @@ log = logging.getLogger(__name__) class OverUnderflowAnnotation: + """ Symbol Annotation used if a BitVector can overflow""" + def __init__( + self, overflowing_state: GlobalState, operator: str, constraint + ) -> None: + self.overflowing_state = overflowing_state + self.operator = operator + self.constraint = constraint + + +class OverUnderflowStateAnnotation(StateAnnotation): + """ State Annotation used if an overflow both possible and used in the annotated path""" def __init__( self, overflowing_state: GlobalState, operator: str, constraint ) -> None: From 8ab0fb1c411ea20c445782fd487a43e5fd017b56 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Mon, 4 Feb 2019 09:01:11 +0100 Subject: [PATCH 02/22] add function end handler and use state annotation --- mythril/analysis/modules/integer.py | 70 ++++++++++------------------- 1 file changed, 24 insertions(+), 46 deletions(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index 9b141a5f..e0e12bf8 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -177,7 +177,8 @@ class IntegerOverflowUnderflowModule(DetectionModule): def _get_title(_type): return "Integer {}".format(_type) - def _handle_sstore(self, state): + @staticmethod + def _handle_sstore(state: GlobalState) -> None: stack = state.mstate.stack value = stack[-2] @@ -186,59 +187,36 @@ class IntegerOverflowUnderflowModule(DetectionModule): for annotation in value.annotations: if not isinstance(annotation, OverUnderflowAnnotation): continue - - _type = "Underflow" if annotation.operator == "subtraction" else "Overflow" - ostate = annotation.overflowing_state - node = ostate.node - - issue = Issue( - contract=node.contract_name, - function_name=node.function_name, - address=ostate.get_current_instruction()["address"], - swc_id=INTEGER_OVERFLOW_AND_UNDERFLOW, - bytecode=ostate.environment.code.bytecode, - title=self._get_title(_type), - severity="High", - description_head=self._get_description_head(annotation, _type), - description_tail=self._get_description_tail(annotation, _type), - gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), - ) - - address = _get_address_from_state(ostate) - - if annotation.operator == "subtraction" and self._underflow_cache.get( - address, False - ): - continue - if annotation.operator != "subtraction" and self._overflow_cache.get( - address, False - ): - continue - - try: - - transaction_sequence = solver.get_transaction_sequence( - state, node.constraints + [annotation.constraint] + state.annotate( + OverUnderflowStateAnnotation( + annotation.overflowing_state, + annotation.operator, + annotation.constraint, ) + ) - issue.debug = json.dumps(transaction_sequence, indent=4) - - except UnsatError: - continue - if annotation.operator == "subtraction": - self._underflow_cache[address] = True - else: - self._overflow_cache[address] = True - - self._issues.append(issue) - - def _handle_jumpi(self, state): + @staticmethod + def _handle_jumpi(state): stack = state.mstate.stack value = stack[-2] for annotation in value.annotations: if not isinstance(annotation, OverUnderflowAnnotation): continue + state.annotate( + OverUnderflowStateAnnotation( + annotation.overflowing_state, + annotation.operator, + annotation.constraint, + ) + ) + + def _handle_transaction_end(self, state: GlobalState) -> None: + for annotation in cast( + List[OverUnderflowStateAnnotation], + state.get_annotations(OverUnderflowStateAnnotation), + ): + ostate = annotation.overflowing_state node = ostate.node From e33a32a3a66fe888dd247dde4e53a018daf68b73 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Mon, 4 Feb 2019 09:01:33 +0100 Subject: [PATCH 03/22] add hooks and type dependencies --- mythril/analysis/modules/integer.py | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index e0e12bf8..99353fba 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -2,7 +2,7 @@ underflows.""" import json -from typing import Dict +from typing import Dict, cast, List from mythril.analysis import solver from mythril.analysis.report import Issue from mythril.analysis.swc_data import INTEGER_OVERFLOW_AND_UNDERFLOW @@ -61,7 +61,7 @@ class IntegerOverflowUnderflowModule(DetectionModule): "there's a possible state where op1 + op0 > 2^32 - 1" ), entrypoint="callback", - pre_hooks=["ADD", "MUL", "SUB", "SSTORE", "JUMPI"], + pre_hooks=["ADD", "MUL", "SUB", "SSTORE", "JUMPI", "STOP", "RETURN"], ) self._overflow_cache = {} # type: Dict[int, bool] self._underflow_cache = {} # type: Dict[int, bool] @@ -96,6 +96,8 @@ class IntegerOverflowUnderflowModule(DetectionModule): self._handle_sstore(state) elif state.get_current_instruction()["opcode"] == "JUMPI": self._handle_jumpi(state) + elif state.get_current_instruction()["opcode"] in ("RETURN", "STOP"): + self._handle_transaction_end(state) def _handle_add(self, state): stack = state.mstate.stack From 734d6c9b4aba17855ec9624f2de1e17d2d151ce9 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Mon, 4 Feb 2019 09:02:00 +0100 Subject: [PATCH 04/22] add ident argument This will make sure the test outputs are nice and indented --- tests/report_test.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/report_test.py b/tests/report_test.py index 380ba30e..a95eb63d 100644 --- a/tests/report_test.py +++ b/tests/report_test.py @@ -18,7 +18,7 @@ def _fix_debug_data(json_str): read_json = json.loads(json_str) for issue in read_json["issues"]: issue["debug"] = "" - return json.dumps(read_json, sort_keys=True) + return json.dumps(read_json, sort_keys=True, indent=4) def _generate_report(input_file): From 103361f55557f3a40f82dbe918c47a9ee0e5d368 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Mon, 4 Feb 2019 09:03:16 +0100 Subject: [PATCH 05/22] adapt gasvalue for testcases --- .../outputs_expected/calls.sol.o.json | 111 +++++++++++++++++- .../outputs_expected/ether_send.sol.o.json | 6 +- .../outputs_expected/exceptions.sol.o.json | 59 +++++++++- .../kinds_of_calls.sol.o.json | 72 +++++++++++- .../outputs_expected/metacoin.sol.o.json | 6 +- .../multi_contracts.sol.o.json | 20 +++- .../outputs_expected/nonascii.sol.o.json | 6 +- .../outputs_expected/origin.sol.o.json | 20 +++- .../outputs_expected/overflow.sol.o.json | 59 +++++----- .../outputs_expected/overflow.sol.o.markdown | 4 +- .../outputs_expected/overflow.sol.o.text | 4 +- .../outputs_expected/returnvalue.sol.o.json | 46 +++++++- .../outputs_expected/suicide.sol.o.json | 36 +++--- .../outputs_expected/underflow.sol.o.json | 59 +++++----- .../outputs_expected/underflow.sol.o.markdown | 4 +- .../outputs_expected/underflow.sol.o.text | 4 +- 16 files changed, 425 insertions(+), 91 deletions(-) diff --git a/tests/testdata/outputs_expected/calls.sol.o.json b/tests/testdata/outputs_expected/calls.sol.o.json index 1342a258..7086d59d 100644 --- a/tests/testdata/outputs_expected/calls.sol.o.json +++ b/tests/testdata/outputs_expected/calls.sol.o.json @@ -1 +1,110 @@ -{"error": null, "issues": [{"address": 661, "contract": "Unknown", "debug": "", "description": "The contract executes an external message call.\nAn external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully.", "function": "thisisfine()", "max_gas_used": 1254, "min_gas_used": 643, "severity": "Low", "sourceMap": null, "swc-id": "107", "title": "External Call To Fixed Address"}, {"address": 661, "contract": "Unknown", "debug": "", "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.", "function": "thisisfine()", "max_gas_used": 35972, "min_gas_used": 1361, "severity": "Low", "sourceMap": null, "swc-id": "104", "title": "Unchecked Call Return Value"}, {"address": 779, "contract": "Unknown", "debug": "", "description": "The contract executes an external message call.\nAn external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully.", "function": "callstoredaddress()", "max_gas_used": 1298, "min_gas_used": 687, "severity": "Low", "sourceMap": null, "swc-id": "107", "title": "External Call To Fixed Address"}, {"address": 779, "contract": "Unknown", "debug": "", "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.", "function": "callstoredaddress()", "max_gas_used": 36016, "min_gas_used": 1405, "severity": "Low", "sourceMap": null, "swc-id": "104", "title": "Unchecked Call Return Value"}, {"address": 858, "contract": "Unknown", "debug": "", "description": "The contract executes an external message call.\nAn external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully.", "function": "reentrancy()", "max_gas_used": 1320, "min_gas_used": 709, "severity": "Low", "sourceMap": null, "swc-id": "107", "title": "External Call To Fixed Address"}, {"address": 858, "contract": "Unknown", "debug": "", "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.", "function": "reentrancy()", "max_gas_used": 61052, "min_gas_used": 6441, "severity": "Low", "sourceMap": null, "swc-id": "104", "title": "Unchecked Call Return Value"}, {"address": 912, "contract": "Unknown", "debug": "", "description": "A call to a user-supplied address is executed.\nThe callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on thecontract state.", "function": "calluseraddress(address)", "max_gas_used": 616, "min_gas_used": 335, "severity": "Medium", "sourceMap": null, "swc-id": "107", "title": "External Call To User-Supplied Address"}, {"address": 912, "contract": "Unknown", "debug": "", "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.", "function": "calluseraddress(address)", "max_gas_used": 35336, "min_gas_used": 1055, "severity": "Low", "sourceMap": null, "swc-id": "104", "title": "Unchecked Call Return Value"}], "success": true} \ No newline at end of file +{ + "error": null, + "issues": [ + { + "address": 661, + "contract": "Unknown", + "debug": "", + "description": "The contract executes an external message call.\nAn external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully.", + "function": "thisisfine()", + "max_gas_used": 1254, + "min_gas_used": 643, + "severity": "Low", + "sourceMap": null, + "swc-id": "107", + "title": "External Call To Fixed Address" + }, + { + "address": 661, + "contract": "Unknown", + "debug": "", + "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.", + "function": "thisisfine()", + "max_gas_used": 35972, + "min_gas_used": 1361, + "severity": "Low", + "sourceMap": null, + "swc-id": "104", + "title": "Unchecked Call Return Value" + }, + { + "address": 779, + "contract": "Unknown", + "debug": "", + "description": "The contract executes an external message call.\nAn external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully.", + "function": "callstoredaddress()", + "max_gas_used": 1298, + "min_gas_used": 687, + "severity": "Low", + "sourceMap": null, + "swc-id": "107", + "title": "External Call To Fixed Address" + }, + { + "address": 779, + "contract": "Unknown", + "debug": "", + "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.", + "function": "callstoredaddress()", + "max_gas_used": 36016, + "min_gas_used": 1405, + "severity": "Low", + "sourceMap": null, + "swc-id": "104", + "title": "Unchecked Call Return Value" + }, + { + "address": 858, + "contract": "Unknown", + "debug": "", + "description": "The contract executes an external message call.\nAn external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully.", + "function": "reentrancy()", + "max_gas_used": 1320, + "min_gas_used": 709, + "severity": "Low", + "sourceMap": null, + "swc-id": "107", + "title": "External Call To Fixed Address" + }, + { + "address": 858, + "contract": "Unknown", + "debug": "", + "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.", + "function": "reentrancy()", + "max_gas_used": 61052, + "min_gas_used": 6441, + "severity": "Low", + "sourceMap": null, + "swc-id": "104", + "title": "Unchecked Call Return Value" + }, + { + "address": 912, + "contract": "Unknown", + "debug": "", + "description": "A call to a user-supplied address is executed.\nThe callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on thecontract state.", + "function": "calluseraddress(address)", + "max_gas_used": 616, + "min_gas_used": 335, + "severity": "Medium", + "sourceMap": null, + "swc-id": "107", + "title": "External Call To User-Supplied Address" + }, + { + "address": 912, + "contract": "Unknown", + "debug": "", + "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.", + "function": "calluseraddress(address)", + "max_gas_used": 35336, + "min_gas_used": 1055, + "severity": "Low", + "sourceMap": null, + "swc-id": "104", + "title": "Unchecked Call Return Value" + } + ], + "success": true +} \ No newline at end of file diff --git a/tests/testdata/outputs_expected/ether_send.sol.o.json b/tests/testdata/outputs_expected/ether_send.sol.o.json index 237b1c1e..712f50c1 100644 --- a/tests/testdata/outputs_expected/ether_send.sol.o.json +++ b/tests/testdata/outputs_expected/ether_send.sol.o.json @@ -1 +1,5 @@ -{"error": null, "issues": [], "success": true} \ No newline at end of file +{ + "error": null, + "issues": [], + "success": true +} \ No newline at end of file diff --git a/tests/testdata/outputs_expected/exceptions.sol.o.json b/tests/testdata/outputs_expected/exceptions.sol.o.json index de103061..e529a0ae 100644 --- a/tests/testdata/outputs_expected/exceptions.sol.o.json +++ b/tests/testdata/outputs_expected/exceptions.sol.o.json @@ -1 +1,58 @@ -{"error": null, "issues": [{"address": 446, "contract": "Unknown", "debug": "", "description": "A reachable exception has been detected.\nIt is possible to trigger an exception (opcode 0xfe). Exceptions can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. Note that explicit `assert()` should only be used to check invariants. Use `require()` for regular input checking.", "function": "assert3(uint256)", "max_gas_used": 301, "min_gas_used": 206, "severity": "Low", "sourceMap": null, "swc-id": "110", "title": "Exception State"}, {"address": 484, "contract": "Unknown", "debug": "", "description": "A reachable exception has been detected.\nIt is possible to trigger an exception (opcode 0xfe). Exceptions can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. Note that explicit `assert()` should only be used to check invariants. Use `require()` for regular input checking.", "function": "arrayaccess(uint256)", "max_gas_used": 351, "min_gas_used": 256, "severity": "Low", "sourceMap": null, "swc-id": "110", "title": "Exception State"}, {"address": 506, "contract": "Unknown", "debug": "", "description": "A reachable exception has been detected.\nIt is possible to trigger an exception (opcode 0xfe). Exceptions can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. Note that explicit `assert()` should only be used to check invariants. Use `require()` for regular input checking.", "function": "divisionby0(uint256)", "max_gas_used": 367, "min_gas_used": 272, "severity": "Low", "sourceMap": null, "swc-id": "110", "title": "Exception State"}, {"address": 531, "contract": "Unknown", "debug": "", "description": "A reachable exception has been detected.\nIt is possible to trigger an exception (opcode 0xfe). Exceptions can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. Note that explicit `assert()` should only be used to check invariants. Use `require()` for regular input checking.", "function": "assert1()", "max_gas_used": 363, "min_gas_used": 268, "severity": "Low", "sourceMap": null, "swc-id": "110", "title": "Exception State"}], "success": true} \ No newline at end of file +{ + "error": null, + "issues": [ + { + "address": 446, + "contract": "Unknown", + "debug": "", + "description": "A reachable exception has been detected.\nIt is possible to trigger an exception (opcode 0xfe). Exceptions can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. Note that explicit `assert()` should only be used to check invariants. Use `require()` for regular input checking.", + "function": "assert3(uint256)", + "max_gas_used": 301, + "min_gas_used": 206, + "severity": "Low", + "sourceMap": null, + "swc-id": "110", + "title": "Exception State" + }, + { + "address": 484, + "contract": "Unknown", + "debug": "", + "description": "A reachable exception has been detected.\nIt is possible to trigger an exception (opcode 0xfe). Exceptions can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. Note that explicit `assert()` should only be used to check invariants. Use `require()` for regular input checking.", + "function": "arrayaccess(uint256)", + "max_gas_used": 351, + "min_gas_used": 256, + "severity": "Low", + "sourceMap": null, + "swc-id": "110", + "title": "Exception State" + }, + { + "address": 506, + "contract": "Unknown", + "debug": "", + "description": "A reachable exception has been detected.\nIt is possible to trigger an exception (opcode 0xfe). Exceptions can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. Note that explicit `assert()` should only be used to check invariants. Use `require()` for regular input checking.", + "function": "divisionby0(uint256)", + "max_gas_used": 367, + "min_gas_used": 272, + "severity": "Low", + "sourceMap": null, + "swc-id": "110", + "title": "Exception State" + }, + { + "address": 531, + "contract": "Unknown", + "debug": "", + "description": "A reachable exception has been detected.\nIt is possible to trigger an exception (opcode 0xfe). Exceptions can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. Note that explicit `assert()` should only be used to check invariants. Use `require()` for regular input checking.", + "function": "assert1()", + "max_gas_used": 363, + "min_gas_used": 268, + "severity": "Low", + "sourceMap": null, + "swc-id": "110", + "title": "Exception State" + } + ], + "success": true +} \ No newline at end of file diff --git a/tests/testdata/outputs_expected/kinds_of_calls.sol.o.json b/tests/testdata/outputs_expected/kinds_of_calls.sol.o.json index b18d1c40..8e595704 100644 --- a/tests/testdata/outputs_expected/kinds_of_calls.sol.o.json +++ b/tests/testdata/outputs_expected/kinds_of_calls.sol.o.json @@ -1 +1,71 @@ -{"error": null, "issues": [{"address": 618, "contract": "Unknown", "debug": "", "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.", "function": "_function_0x141f32ff", "max_gas_used": 35865, "min_gas_used": 1113, "severity": "Low", "sourceMap": null, "swc-id": "104", "title": "Unchecked Call Return Value"}, {"address": 618, "contract": "Unknown", "debug": "", "description": "Use of callcode is deprecated.\nThe callcode method executes code of another contract in the context of the caller account. Due to a bug in the implementation it does not persist sender and value over the call. It was therefore deprecated and may be removed in the future. Use the delegatecall method instead.", "function": "_function_0x141f32ff", "max_gas_used": 1141, "min_gas_used": 389, "severity": "Medium", "sourceMap": null, "swc-id": "111", "title": "Use of callcode"}, {"address": 849, "contract": "Unknown", "debug": "", "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.", "function": "_function_0x9b58bc26", "max_gas_used": 35922, "min_gas_used": 1170, "severity": "Low", "sourceMap": null, "swc-id": "104", "title": "Unchecked Call Return Value"}, {"address": 1038, "contract": "Unknown", "debug": "", "description": "A call to a user-supplied address is executed.\nThe callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on thecontract state.", "function": "_function_0xeea4c864", "max_gas_used": 1223, "min_gas_used": 471, "severity": "Medium", "sourceMap": null, "swc-id": "107", "title": "External Call To User-Supplied Address"}, {"address": 1038, "contract": "Unknown", "debug": "", "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.", "function": "_function_0xeea4c864", "max_gas_used": 35947, "min_gas_used": 1195, "severity": "Low", "sourceMap": null, "swc-id": "104", "title": "Unchecked Call Return Value"}], "success": true} \ No newline at end of file +{ + "error": null, + "issues": [ + { + "address": 618, + "contract": "Unknown", + "debug": "", + "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.", + "function": "_function_0x141f32ff", + "max_gas_used": 35865, + "min_gas_used": 1113, + "severity": "Low", + "sourceMap": null, + "swc-id": "104", + "title": "Unchecked Call Return Value" + }, + { + "address": 618, + "contract": "Unknown", + "debug": "", + "description": "Use of callcode is deprecated.\nThe callcode method executes code of another contract in the context of the caller account. Due to a bug in the implementation it does not persist sender and value over the call. It was therefore deprecated and may be removed in the future. Use the delegatecall method instead.", + "function": "_function_0x141f32ff", + "max_gas_used": 1141, + "min_gas_used": 389, + "severity": "Medium", + "sourceMap": null, + "swc-id": "111", + "title": "Use of callcode" + }, + { + "address": 849, + "contract": "Unknown", + "debug": "", + "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.", + "function": "_function_0x9b58bc26", + "max_gas_used": 35922, + "min_gas_used": 1170, + "severity": "Low", + "sourceMap": null, + "swc-id": "104", + "title": "Unchecked Call Return Value" + }, + { + "address": 1038, + "contract": "Unknown", + "debug": "", + "description": "A call to a user-supplied address is executed.\nThe callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on thecontract state.", + "function": "_function_0xeea4c864", + "max_gas_used": 1223, + "min_gas_used": 471, + "severity": "Medium", + "sourceMap": null, + "swc-id": "107", + "title": "External Call To User-Supplied Address" + }, + { + "address": 1038, + "contract": "Unknown", + "debug": "", + "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.", + "function": "_function_0xeea4c864", + "max_gas_used": 35947, + "min_gas_used": 1195, + "severity": "Low", + "sourceMap": null, + "swc-id": "104", + "title": "Unchecked Call Return Value" + } + ], + "success": true +} \ No newline at end of file diff --git a/tests/testdata/outputs_expected/metacoin.sol.o.json b/tests/testdata/outputs_expected/metacoin.sol.o.json index 237b1c1e..712f50c1 100644 --- a/tests/testdata/outputs_expected/metacoin.sol.o.json +++ b/tests/testdata/outputs_expected/metacoin.sol.o.json @@ -1 +1,5 @@ -{"error": null, "issues": [], "success": true} \ No newline at end of file +{ + "error": null, + "issues": [], + "success": true +} \ No newline at end of file diff --git a/tests/testdata/outputs_expected/multi_contracts.sol.o.json b/tests/testdata/outputs_expected/multi_contracts.sol.o.json index 64a7bee7..8ade4afb 100644 --- a/tests/testdata/outputs_expected/multi_contracts.sol.o.json +++ b/tests/testdata/outputs_expected/multi_contracts.sol.o.json @@ -1 +1,19 @@ -{"error": null, "issues": [{"address": 142, "contract": "Unknown", "debug": "", "description": "Anyone can withdraw ETH from the contract account.\nArbitrary senders other than the contract creator can withdraw ETH from the contract account without previously having sent an equivalent amount of ETH to it. This is likely to be a vulnerability.", "function": "transfer()", "max_gas_used": 467, "min_gas_used": 186, "severity": "High", "sourceMap": null, "swc-id": "105", "title": "Unprotected Ether Withdrawal"}], "success": true} \ No newline at end of file +{ + "error": null, + "issues": [ + { + "address": 142, + "contract": "Unknown", + "debug": "", + "description": "Anyone can withdraw ETH from the contract account.\nArbitrary senders other than the contract creator can withdraw ETH from the contract account without previously having sent an equivalent amount of ETH to it. This is likely to be a vulnerability.", + "function": "transfer()", + "max_gas_used": 467, + "min_gas_used": 186, + "severity": "High", + "sourceMap": null, + "swc-id": "105", + "title": "Unprotected Ether Withdrawal" + } + ], + "success": true +} \ No newline at end of file diff --git a/tests/testdata/outputs_expected/nonascii.sol.o.json b/tests/testdata/outputs_expected/nonascii.sol.o.json index 237b1c1e..712f50c1 100644 --- a/tests/testdata/outputs_expected/nonascii.sol.o.json +++ b/tests/testdata/outputs_expected/nonascii.sol.o.json @@ -1 +1,5 @@ -{"error": null, "issues": [], "success": true} \ No newline at end of file +{ + "error": null, + "issues": [], + "success": true +} \ No newline at end of file diff --git a/tests/testdata/outputs_expected/origin.sol.o.json b/tests/testdata/outputs_expected/origin.sol.o.json index 5b786178..d9c74bc1 100644 --- a/tests/testdata/outputs_expected/origin.sol.o.json +++ b/tests/testdata/outputs_expected/origin.sol.o.json @@ -1 +1,19 @@ -{"error": null, "issues": [{"address": 317, "contract": "Unknown", "debug": "", "description": "Use of tx.origin is deprecated.\nThe smart contract retrieves the transaction origin (tx.origin) using msg.origin. Use of msg.origin is deprecated and the instruction may be removed in the future. Use msg.sender instead.\nSee also: https://solidity.readthedocs.io/en/develop/security-considerations.html#tx-origin", "function": "transferOwnership(address)", "max_gas_used": 1051, "min_gas_used": 626, "severity": "Medium", "sourceMap": null, "swc-id": "111", "title": "Use of tx.origin"}], "success": true} \ No newline at end of file +{ + "error": null, + "issues": [ + { + "address": 317, + "contract": "Unknown", + "debug": "", + "description": "Use of tx.origin is deprecated.\nThe smart contract retrieves the transaction origin (tx.origin) using msg.origin. Use of msg.origin is deprecated and the instruction may be removed in the future. Use msg.sender instead.\nSee also: https://solidity.readthedocs.io/en/develop/security-considerations.html#tx-origin", + "function": "transferOwnership(address)", + "max_gas_used": 1051, + "min_gas_used": 626, + "severity": "Medium", + "sourceMap": null, + "swc-id": "111", + "title": "Use of tx.origin" + } + ], + "success": true +} \ No newline at end of file diff --git a/tests/testdata/outputs_expected/overflow.sol.o.json b/tests/testdata/outputs_expected/overflow.sol.o.json index f14878cc..285fdf31 100644 --- a/tests/testdata/outputs_expected/overflow.sol.o.json +++ b/tests/testdata/outputs_expected/overflow.sol.o.json @@ -1,29 +1,32 @@ { - "error": null, - "issues": [{ - "address": 567, - "contract": "Unknown", - "debug": "", - "description": "The binary subtraction can underflow.\nThe operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.", - "function": "sendeth(address,uint256)", - "max_gas_used": 1053, - "min_gas_used": 768, - "severity": "High", - "sourceMap": null, - "swc-id": "101", - "title": "Integer Underflow" - }, { - "address": 649, - "contract": "Unknown", - "debug": "", - "description": "The binary subtraction can underflow.\nThe operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.", - "function": "sendeth(address,uint256)", - "max_gas_used": 1774, - "min_gas_used": 1299, - "severity": "High", - "sourceMap": null, - "swc-id": "101", - "title": "Integer Underflow" - }], - "success": true -} + "error": null, + "issues": [ + { + "address": 567, + "contract": "Unknown", + "debug": "", + "description": "The binary subtraction can underflow.\nThe operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.", + "function": "sendeth(address,uint256)", + "max_gas_used": 78152, + "min_gas_used": 17016, + "severity": "High", + "sourceMap": null, + "swc-id": "101", + "title": "Integer Underflow" + }, + { + "address": 649, + "contract": "Unknown", + "debug": "", + "description": "The binary subtraction can underflow.\nThe operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.", + "function": "sendeth(address,uint256)", + "max_gas_used": 78152, + "min_gas_used": 17016, + "severity": "High", + "sourceMap": null, + "swc-id": "101", + "title": "Integer Underflow" + } + ], + "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 8ece5099..0d589f0d 100644 --- a/tests/testdata/outputs_expected/overflow.sol.o.markdown +++ b/tests/testdata/outputs_expected/overflow.sol.o.markdown @@ -6,7 +6,7 @@ - Contract: Unknown - Function name: `sendeth(address,uint256)` - PC address: 567 -- Estimated Gas Usage: 768 - 1053 +- Estimated Gas Usage: 17016 - 78152 ### Description @@ -19,7 +19,7 @@ The operands of the subtraction operation are not sufficiently constrained. The - Contract: Unknown - Function name: `sendeth(address,uint256)` - PC address: 649 -- Estimated Gas Usage: 1299 - 1774 +- Estimated Gas Usage: 17016 - 78152 ### Description diff --git a/tests/testdata/outputs_expected/overflow.sol.o.text b/tests/testdata/outputs_expected/overflow.sol.o.text index 745404aa..934ccdd7 100644 --- a/tests/testdata/outputs_expected/overflow.sol.o.text +++ b/tests/testdata/outputs_expected/overflow.sol.o.text @@ -4,7 +4,7 @@ Severity: High Contract: Unknown Function name: sendeth(address,uint256) PC address: 567 -Estimated Gas Usage: 768 - 1053 +Estimated Gas Usage: 17016 - 78152 The binary subtraction can underflow. The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion. -------------------- @@ -15,7 +15,7 @@ Severity: High Contract: Unknown Function name: sendeth(address,uint256) PC address: 649 -Estimated Gas Usage: 1299 - 1774 +Estimated Gas Usage: 17016 - 78152 The binary subtraction can underflow. The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion. -------------------- diff --git a/tests/testdata/outputs_expected/returnvalue.sol.o.json b/tests/testdata/outputs_expected/returnvalue.sol.o.json index 2c741ba2..b31986bd 100644 --- a/tests/testdata/outputs_expected/returnvalue.sol.o.json +++ b/tests/testdata/outputs_expected/returnvalue.sol.o.json @@ -1 +1,45 @@ -{"error": null, "issues": [{"address": 196, "contract": "Unknown", "debug": "", "description": "The contract executes an external message call.\nAn external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully.", "function": "callchecked()", "max_gas_used": 1210, "min_gas_used": 599, "severity": "Low", "sourceMap": null, "swc-id": "107", "title": "External Call To Fixed Address"}, {"address": 285, "contract": "Unknown", "debug": "", "description": "The contract executes an external message call.\nAn external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully.", "function": "callnotchecked()", "max_gas_used": 1232, "min_gas_used": 621, "severity": "Low", "sourceMap": null, "swc-id": "107", "title": "External Call To Fixed Address"}, {"address": 285, "contract": "Unknown", "debug": "", "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.", "function": "callnotchecked()", "max_gas_used": 35950, "min_gas_used": 1339, "severity": "Low", "sourceMap": null, "swc-id": "104", "title": "Unchecked Call Return Value"}], "success": true} \ No newline at end of file +{ + "error": null, + "issues": [ + { + "address": 196, + "contract": "Unknown", + "debug": "", + "description": "The contract executes an external message call.\nAn external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully.", + "function": "callchecked()", + "max_gas_used": 1210, + "min_gas_used": 599, + "severity": "Low", + "sourceMap": null, + "swc-id": "107", + "title": "External Call To Fixed Address" + }, + { + "address": 285, + "contract": "Unknown", + "debug": "", + "description": "The contract executes an external message call.\nAn external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully.", + "function": "callnotchecked()", + "max_gas_used": 1232, + "min_gas_used": 621, + "severity": "Low", + "sourceMap": null, + "swc-id": "107", + "title": "External Call To Fixed Address" + }, + { + "address": 285, + "contract": "Unknown", + "debug": "", + "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.", + "function": "callnotchecked()", + "max_gas_used": 35950, + "min_gas_used": 1339, + "severity": "Low", + "sourceMap": null, + "swc-id": "104", + "title": "Unchecked Call Return Value" + } + ], + "success": true +} \ No newline at end of file diff --git a/tests/testdata/outputs_expected/suicide.sol.o.json b/tests/testdata/outputs_expected/suicide.sol.o.json index 39921898..054f1981 100644 --- a/tests/testdata/outputs_expected/suicide.sol.o.json +++ b/tests/testdata/outputs_expected/suicide.sol.o.json @@ -1,19 +1,19 @@ { - "error" : null, - "issues" : [ - { - "title" : "Unprotected Selfdestruct", - "swc-id" : "106", - "severity" : "High", - "contract" : "Unknown", - "description" : "The contract can be killed by anyone.\nAnyone can kill this contract and withdraw its balance to an arbitrary address.", - "function" : "kill(address)", - "min_gas_used" : 168, - "max_gas_used" : 263, - "debug" : "", - "sourceMap" : null, - "address" : 146 - } - ], - "success" : true -} + "error": null, + "issues": [ + { + "address": 146, + "contract": "Unknown", + "debug": "", + "description": "The contract can be killed by anyone.\nAnyone can kill this contract and withdraw its balance to an arbitrary address.", + "function": "kill(address)", + "max_gas_used": 263, + "min_gas_used": 168, + "severity": "High", + "sourceMap": null, + "swc-id": "106", + "title": "Unprotected Selfdestruct" + } + ], + "success": true +} \ No newline at end of file diff --git a/tests/testdata/outputs_expected/underflow.sol.o.json b/tests/testdata/outputs_expected/underflow.sol.o.json index f14878cc..5761ec2e 100644 --- a/tests/testdata/outputs_expected/underflow.sol.o.json +++ b/tests/testdata/outputs_expected/underflow.sol.o.json @@ -1,29 +1,32 @@ { - "error": null, - "issues": [{ - "address": 567, - "contract": "Unknown", - "debug": "", - "description": "The binary subtraction can underflow.\nThe operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.", - "function": "sendeth(address,uint256)", - "max_gas_used": 1053, - "min_gas_used": 768, - "severity": "High", - "sourceMap": null, - "swc-id": "101", - "title": "Integer Underflow" - }, { - "address": 649, - "contract": "Unknown", - "debug": "", - "description": "The binary subtraction can underflow.\nThe operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.", - "function": "sendeth(address,uint256)", - "max_gas_used": 1774, - "min_gas_used": 1299, - "severity": "High", - "sourceMap": null, - "swc-id": "101", - "title": "Integer Underflow" - }], - "success": true -} + "error": null, + "issues": [ + { + "address": 567, + "contract": "Unknown", + "debug": "", + "description": "The binary subtraction can underflow.\nThe operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.", + "function": "sendeth(address,uint256)", + "max_gas_used": 52858, + "min_gas_used": 11912, + "severity": "High", + "sourceMap": null, + "swc-id": "101", + "title": "Integer Underflow" + }, + { + "address": 649, + "contract": "Unknown", + "debug": "", + "description": "The binary subtraction can underflow.\nThe operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.", + "function": "sendeth(address,uint256)", + "max_gas_used": 52858, + "min_gas_used": 11912, + "severity": "High", + "sourceMap": null, + "swc-id": "101", + "title": "Integer Underflow" + } + ], + "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 8ece5099..19f4ca9c 100644 --- a/tests/testdata/outputs_expected/underflow.sol.o.markdown +++ b/tests/testdata/outputs_expected/underflow.sol.o.markdown @@ -6,7 +6,7 @@ - Contract: Unknown - Function name: `sendeth(address,uint256)` - PC address: 567 -- Estimated Gas Usage: 768 - 1053 +- Estimated Gas Usage: 11912 - 52858 ### Description @@ -19,7 +19,7 @@ The operands of the subtraction operation are not sufficiently constrained. The - Contract: Unknown - Function name: `sendeth(address,uint256)` - PC address: 649 -- Estimated Gas Usage: 1299 - 1774 +- Estimated Gas Usage: 11912 - 52858 ### Description diff --git a/tests/testdata/outputs_expected/underflow.sol.o.text b/tests/testdata/outputs_expected/underflow.sol.o.text index 745404aa..84a35ab7 100644 --- a/tests/testdata/outputs_expected/underflow.sol.o.text +++ b/tests/testdata/outputs_expected/underflow.sol.o.text @@ -4,7 +4,7 @@ Severity: High Contract: Unknown Function name: sendeth(address,uint256) PC address: 567 -Estimated Gas Usage: 768 - 1053 +Estimated Gas Usage: 11912 - 52858 The binary subtraction can underflow. The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion. -------------------- @@ -15,7 +15,7 @@ Severity: High Contract: Unknown Function name: sendeth(address,uint256) PC address: 649 -Estimated Gas Usage: 1299 - 1774 +Estimated Gas Usage: 11912 - 52858 The binary subtraction can underflow. The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion. -------------------- From 1bd944c23eb3af39e7af262d9d883fe2e23aa682 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Mon, 4 Feb 2019 09:08:31 +0100 Subject: [PATCH 06/22] apply style rules --- mythril/analysis/modules/integer.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index 99353fba..c57e6f96 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -29,6 +29,7 @@ log = logging.getLogger(__name__) class OverUnderflowAnnotation: """ Symbol Annotation used if a BitVector can overflow""" + def __init__( self, overflowing_state: GlobalState, operator: str, constraint ) -> None: @@ -39,6 +40,7 @@ class OverUnderflowAnnotation: class OverUnderflowStateAnnotation(StateAnnotation): """ State Annotation used if an overflow both possible and used in the annotated path""" + def __init__( self, overflowing_state: GlobalState, operator: str, constraint ) -> None: From 3e3eb1805091ad141f8a06c2267768202a5bd9a3 Mon Sep 17 00:00:00 2001 From: Nathan Date: Tue, 5 Feb 2019 13:58:27 -0500 Subject: [PATCH 07/22] Update docs theme to the read the docs theme --- docs/source/conf.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/source/conf.py b/docs/source/conf.py index e99ac6cf..36f41a8c 100644 --- a/docs/source/conf.py +++ b/docs/source/conf.py @@ -81,7 +81,7 @@ pygments_style = None # The theme to use for HTML and HTML Help pages. See the documentation for # a list of builtin themes. # -html_theme = "alabaster" +html_theme = "sphinx_rtd_theme" # Theme options are theme-specific and customize the look and feel of a theme # further. For a list of options available for each theme, see the From 42edd276c3b00b24bf750e1464bd6e8042769329 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Wed, 6 Feb 2019 08:32:29 +0100 Subject: [PATCH 08/22] move solver files to separate directory --- mythril/laser/smt/solver/__init__.py | 2 ++ mythril/laser/smt/{ => solver}/independence_solver.py | 0 mythril/laser/smt/{ => solver}/solver.py | 0 tests/laser/smt/independece_solver_test.py | 2 +- 4 files changed, 3 insertions(+), 1 deletion(-) create mode 100644 mythril/laser/smt/solver/__init__.py rename mythril/laser/smt/{ => solver}/independence_solver.py (100%) rename mythril/laser/smt/{ => solver}/solver.py (100%) diff --git a/mythril/laser/smt/solver/__init__.py b/mythril/laser/smt/solver/__init__.py new file mode 100644 index 00000000..3ea2c947 --- /dev/null +++ b/mythril/laser/smt/solver/__init__.py @@ -0,0 +1,2 @@ +from mythril.laser.smt.solver.solver import Solver, Optimize, BaseSolver +from mythril.laser.smt.solver.independence_solver import IndependenceSolver diff --git a/mythril/laser/smt/independence_solver.py b/mythril/laser/smt/solver/independence_solver.py similarity index 100% rename from mythril/laser/smt/independence_solver.py rename to mythril/laser/smt/solver/independence_solver.py diff --git a/mythril/laser/smt/solver.py b/mythril/laser/smt/solver/solver.py similarity index 100% rename from mythril/laser/smt/solver.py rename to mythril/laser/smt/solver/solver.py diff --git a/tests/laser/smt/independece_solver_test.py b/tests/laser/smt/independece_solver_test.py index 829b4707..27288752 100644 --- a/tests/laser/smt/independece_solver_test.py +++ b/tests/laser/smt/independece_solver_test.py @@ -1,4 +1,4 @@ -from mythril.laser.smt.independence_solver import ( +from mythril.laser.smt.solver.independence_solver import ( _get_expr_variables, DependenceBucket, DependenceMap, From 61f937b5755f80eee34813a41d419a632145c522 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Wed, 6 Feb 2019 09:31:16 +0100 Subject: [PATCH 09/22] fix bug in independence solver --- mythril/laser/smt/solver/independence_solver.py | 2 +- solidity_examples/BECToken.sol | 3 +-- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/mythril/laser/smt/solver/independence_solver.py b/mythril/laser/smt/solver/independence_solver.py index 781a26fd..9a07d650 100644 --- a/mythril/laser/smt/solver/independence_solver.py +++ b/mythril/laser/smt/solver/independence_solver.py @@ -63,7 +63,7 @@ class DependenceMap: relevant_buckets.add(new_bucket) new_bucket = self._merge_buckets(relevant_buckets) - for variable in variables: + for variable in new_bucket.variables: self.variable_map[str(variable)] = new_bucket def _merge_buckets(self, bucket_list: Set[DependenceBucket]) -> DependenceBucket: diff --git a/solidity_examples/BECToken.sol b/solidity_examples/BECToken.sol index 3a14fd12..98bd5a09 100644 --- a/solidity_examples/BECToken.sol +++ b/solidity_examples/BECToken.sol @@ -1,4 +1,3 @@ -pragma solidity 0.5.0; /** * @title SafeMath @@ -296,4 +295,4 @@ contract BecToken is PausableToken { //if ether is sent to this address, send it back. revert(); } -} \ No newline at end of file +} From 79758523dbc57e9e6049b544f1c94389a3de1be0 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Wed, 6 Feb 2019 09:34:43 +0100 Subject: [PATCH 10/22] fix type mismatch in constraints --- mythril/laser/ethereum/state/constraints.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/mythril/laser/ethereum/state/constraints.py b/mythril/laser/ethereum/state/constraints.py index b967ea8e..ba8cfdc2 100644 --- a/mythril/laser/ethereum/state/constraints.py +++ b/mythril/laser/ethereum/state/constraints.py @@ -1,7 +1,7 @@ """This module contains the class used to represent state-change constraints in the call graph.""" -from mythril.laser.smt import Solver, Bool +from mythril.laser.smt import Solver, Bool, symbol_factory from typing import Iterable, List, Optional from z3 import unsat @@ -38,6 +38,7 @@ class Constraints(list): solver = Solver() solver.set_timeout(self._default_timeout) for constraint in self[:]: + constraint = symbol_factory.Bool(constraint) if isinstance(constraint, bool) else constraint solver.add(constraint) self._is_possible = solver.check() != unsat return self._is_possible From a7583a1d16075f7e5fe35d66634e106367d237e8 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Wed, 6 Feb 2019 09:35:04 +0100 Subject: [PATCH 11/22] implement solver statistics tracking --- mythril/laser/smt/__init__.py | 2 +- mythril/laser/smt/solver/__init__.py | 1 + .../laser/smt/solver/independence_solver.py | 3 ++ mythril/laser/smt/solver/solver.py | 3 +- mythril/laser/smt/solver/solver_statistics.py | 35 +++++++++++++++++++ 5 files changed, 42 insertions(+), 2 deletions(-) create mode 100644 mythril/laser/smt/solver/solver_statistics.py diff --git a/mythril/laser/smt/__init__.py b/mythril/laser/smt/__init__.py index 98f52d7e..28f0c42b 100644 --- a/mythril/laser/smt/__init__.py +++ b/mythril/laser/smt/__init__.py @@ -17,7 +17,7 @@ from mythril.laser.smt.bitvec import ( from mythril.laser.smt.expression import Expression, simplify from mythril.laser.smt.bool import Bool, is_true, is_false, Or, Not, And from mythril.laser.smt.array import K, Array, BaseArray -from mythril.laser.smt.solver import Solver, Optimize +from mythril.laser.smt.solver import Solver, Optimize, SolverStatistics from mythril.laser.smt.model import Model from typing import Union, Any, Optional, List, TypeVar, Generic diff --git a/mythril/laser/smt/solver/__init__.py b/mythril/laser/smt/solver/__init__.py index 3ea2c947..f2839b9a 100644 --- a/mythril/laser/smt/solver/__init__.py +++ b/mythril/laser/smt/solver/__init__.py @@ -1,2 +1,3 @@ from mythril.laser.smt.solver.solver import Solver, Optimize, BaseSolver from mythril.laser.smt.solver.independence_solver import IndependenceSolver +from mythril.laser.smt.solver.solver_statistics import SolverStatistics diff --git a/mythril/laser/smt/solver/independence_solver.py b/mythril/laser/smt/solver/independence_solver.py index 9a07d650..8f64de46 100644 --- a/mythril/laser/smt/solver/independence_solver.py +++ b/mythril/laser/smt/solver/independence_solver.py @@ -2,6 +2,8 @@ import z3 from mythril.laser.smt.model import Model from mythril.laser.smt.bool import Bool +from mythril.laser.smt.solver.solver_statistics import stat_smt_query + from typing import Set, Tuple, Dict, List, cast @@ -118,6 +120,7 @@ class IndependenceSolver: ] # type: List[z3.BoolRef] self.constraints.extend(raw_constraints) + @stat_smt_query def check(self) -> z3.CheckSatResult: """Returns z3 smt check result. """ dependence_map = DependenceMap() diff --git a/mythril/laser/smt/solver/solver.py b/mythril/laser/smt/solver/solver.py index b3754e94..d489097d 100644 --- a/mythril/laser/smt/solver/solver.py +++ b/mythril/laser/smt/solver/solver.py @@ -5,7 +5,7 @@ from typing import Union, cast, TypeVar, Generic, List, Sequence from mythril.laser.smt.expression import Expression from mythril.laser.smt.model import Model from mythril.laser.smt.bool import Bool - +from mythril.laser.smt.solver.solver_statistics import stat_smt_query T = TypeVar("T", bound=Union[z3.Solver, z3.Optimize]) @@ -42,6 +42,7 @@ class BaseSolver(Generic[T]): """ self.add(*constraints) + @stat_smt_query def check(self) -> z3.CheckSatResult: """Returns z3 smt check result. diff --git a/mythril/laser/smt/solver/solver_statistics.py b/mythril/laser/smt/solver/solver_statistics.py new file mode 100644 index 00000000..54169dbf --- /dev/null +++ b/mythril/laser/smt/solver/solver_statistics.py @@ -0,0 +1,35 @@ +from time import time + +from mythril.support.support_utils import Singleton + +from typing import Callable + + +def stat_smt_query(func: Callable): + stat_store = SolverStatistics() + + def function_wrapper(*args, **kwargs): + if not stat_store.enabled: + return func(*args, **kwargs) + + stat_store.query_count += 1 + begin = time() + + result = func(*args, **kwargs) + + end = time() + stat_store.solver_time += (end - begin) + + return result + + return function_wrapper + + +class SolverStatistics(object, metaclass=Singleton): + def __init__(self): + self.enabled = False + self.query_count = 0 + self.solver_time = 0 + + def __repr__(self): + return "Query count: {} \nSolver time: {}".format(self.query_count, self.solver_time) From 5c303b87860a7ed40adf55073250f5ed804792de Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Wed, 6 Feb 2019 09:35:29 +0100 Subject: [PATCH 12/22] enable statistics tracking --- mythril/laser/ethereum/state/constraints.py | 6 +++++- mythril/laser/smt/solver/solver_statistics.py | 6 ++++-- mythril/mythril.py | 3 +++ 3 files changed, 12 insertions(+), 3 deletions(-) diff --git a/mythril/laser/ethereum/state/constraints.py b/mythril/laser/ethereum/state/constraints.py index ba8cfdc2..5d064928 100644 --- a/mythril/laser/ethereum/state/constraints.py +++ b/mythril/laser/ethereum/state/constraints.py @@ -38,7 +38,11 @@ class Constraints(list): solver = Solver() solver.set_timeout(self._default_timeout) for constraint in self[:]: - constraint = symbol_factory.Bool(constraint) if isinstance(constraint, bool) else constraint + constraint = ( + symbol_factory.Bool(constraint) + if isinstance(constraint, bool) + else constraint + ) solver.add(constraint) self._is_possible = solver.check() != unsat return self._is_possible diff --git a/mythril/laser/smt/solver/solver_statistics.py b/mythril/laser/smt/solver/solver_statistics.py index 54169dbf..0f5ff4c4 100644 --- a/mythril/laser/smt/solver/solver_statistics.py +++ b/mythril/laser/smt/solver/solver_statistics.py @@ -18,7 +18,7 @@ def stat_smt_query(func: Callable): result = func(*args, **kwargs) end = time() - stat_store.solver_time += (end - begin) + stat_store.solver_time += end - begin return result @@ -32,4 +32,6 @@ class SolverStatistics(object, metaclass=Singleton): self.solver_time = 0 def __repr__(self): - return "Query count: {} \nSolver time: {}".format(self.query_count, self.solver_time) + return "Query count: {} \nSolver time: {}".format( + self.query_count, self.solver_time + ) diff --git a/mythril/mythril.py b/mythril/mythril.py index 5c08ab8a..9224a0a0 100644 --- a/mythril/mythril.py +++ b/mythril/mythril.py @@ -35,6 +35,7 @@ from mythril.analysis.security import fire_lasers, retrieve_callback_issues from mythril.analysis.report import Report from mythril.support.truffle import analyze_truffle_project from mythril.ethereum.interface.leveldb.client import EthLevelDB +from mythril.laser.smt import SolverStatistics log = logging.getLogger(__name__) @@ -566,6 +567,7 @@ class Mythril(object): :return: """ all_issues = [] + SolverStatistics().enabled = True for contract in contracts or self.contracts: try: sym = SymExecWrapper( @@ -600,6 +602,7 @@ class Mythril(object): issue.add_code_info(contract) all_issues += issues + log.info("Solver statistics: \n: {}".format(str(SolverStatistics()))) source_data = Source() source_data.get_source_from_contracts_list(self.contracts) From 0afa10151e82c513ddd66fa437cb36483ac8e1f1 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Wed, 6 Feb 2019 09:43:10 +0100 Subject: [PATCH 13/22] clean up log message --- mythril/mythril.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/mythril.py b/mythril/mythril.py index 9224a0a0..2f082ba0 100644 --- a/mythril/mythril.py +++ b/mythril/mythril.py @@ -602,7 +602,7 @@ class Mythril(object): issue.add_code_info(contract) all_issues += issues - log.info("Solver statistics: \n: {}".format(str(SolverStatistics()))) + log.info("Solver statistics: \n{}".format(str(SolverStatistics()))) source_data = Source() source_data.get_source_from_contracts_list(self.contracts) From 0a2a4484ab98dd9edf29954f67f7a22963d88a0a Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Wed, 6 Feb 2019 13:07:09 +0100 Subject: [PATCH 14/22] add hooks to svm required for benchmarking --- mythril/laser/ethereum/svm.py | 22 ++++++++++++++++++++-- 1 file changed, 20 insertions(+), 2 deletions(-) diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 34d2bd86..56e4b948 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -3,7 +3,6 @@ import logging from collections import defaultdict from copy import copy from datetime import datetime, timedelta -from functools import reduce from typing import Callable, Dict, DefaultDict, List, Tuple, Union from mythril.laser.ethereum.cfg import NodeFlags, Node, Edge, JumpType @@ -15,7 +14,7 @@ from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.state.world_state import WorldState from mythril.laser.ethereum.strategy.basic import DepthFirstSearchStrategy from mythril.laser.ethereum.time_handler import time_handler -from mythril.laser.ethereum.plugins.signals import PluginSignal, PluginSkipWorldState +from mythril.laser.ethereum.plugins.signals import PluginSkipWorldState from mythril.laser.ethereum.transaction import ( ContractCreationTransaction, TransactionEndSignal, @@ -97,6 +96,10 @@ class LaserEVM: self.post_hooks = defaultdict(list) # type: DefaultDict[str, List[Callable]] self._add_world_state_hooks = [] # type: List[Callable] + self._execute_state_hooks = [] # type: List[Callable] + self._start_sym_exec_hooks = [] # type: List[Callable] + self._stop_sym_exec_hooks = [] # type: List[Callable] + self.iprof = InstructionProfiler() if enable_iprof else None log.info("LASER EVM initialized with dynamic loader: " + str(dynamic_loader)) @@ -119,6 +122,8 @@ class LaserEVM: :param contract_name: """ log.debug("Starting LASER execution") + for hook in self._start_sym_exec_hooks: + hook() time_handler.start_execution(self.execution_timeout) self.time = datetime.now() @@ -161,6 +166,9 @@ class LaserEVM: if self.iprof is not None: log.info("Instruction Statistics:\n{}".format(self.iprof)) + for hook in self._stop_sym_exec_hooks: + hook() + def _execute_transactions(self, address): """This function executes multiple transactions on the address based on the coverage. @@ -262,6 +270,10 @@ class LaserEVM: :param global_state: :return: """ + # Execute hooks + for hook in self._execute_state_hooks: + hook(global_state) + instructions = global_state.environment.code.instruction_list try: @@ -509,6 +521,12 @@ class LaserEVM: """registers the hook with this Laser VM""" if hook_type == "add_world_state": self._add_world_state_hooks.append(hook) + elif hook_type == "execute_state": + self._execute_state_hooks.append(hook) + elif hook_type == "start_sym_exec": + self._start_sym_exec_hooks.append(hook) + elif hook_type == "stop_sym_exec": + self._stop_sym_exec_hooks.append(hook) else: raise ValueError( "Invalid hook type %s. Must be one of {add_world_state}", hook_type From f6ac9fd7f8fe8551022418715486c3441125a5b5 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Wed, 6 Feb 2019 13:14:24 +0100 Subject: [PATCH 15/22] add documentation to benchmark --- mythril/laser/ethereum/plugins/benchmark.py | 88 +++++++++++++++++++++ 1 file changed, 88 insertions(+) create mode 100644 mythril/laser/ethereum/plugins/benchmark.py diff --git a/mythril/laser/ethereum/plugins/benchmark.py b/mythril/laser/ethereum/plugins/benchmark.py new file mode 100644 index 00000000..d608f5c6 --- /dev/null +++ b/mythril/laser/ethereum/plugins/benchmark.py @@ -0,0 +1,88 @@ +from mythril.laser.ethereum.svm import LaserEVM +from time import time +import matplotlib.pyplot as plt +import logging + +log = logging.getLogger(__name__) + + +class BenchmarkPlugin: + """Benchmark Plugin + + This plugin aggregates the following information: + - duration + - code coverage over time + - final code coverage + - total number of executed instructions + + """ + + def __init__(self, name=None): + """Creates BenchmarkPlugin + + :param name: name of this benchmark, used for storing the results + """ + self.nr_of_executed_insns = 0 + self.begin = None + self.end = None + self.coverage = {} + self.name = name + + def initialize(self, symbolic_vm: LaserEVM): + """Initializes the BenchmarkPlugin + + Introduces hooks in symbolic_vm to track the desired values + :param symbolic_vm: Symbolic virtual machine to analyze + """ + self._reset() + + @symbolic_vm.laser_hook("execute_state") + def execute_state_hook(_): + current_time = time() - self.begin + self.nr_of_executed_insns += 1 + + for key, value in symbolic_vm.coverage.items(): + try: + self.coverage[key][current_time] = sum(value[1]) * 100 / value[0] + except KeyError: + self.coverage[key] = {} + self.coverage[key][current_time] = sum(value[1]) * 100 / value[0] + + @symbolic_vm.laser_hook("start_sym_exec") + def start_sym_exec_hook(): + self.begin = time() + + @symbolic_vm.laser_hook("stop_sym_exec") + def stop_sym_exec_hook(): + self.end = time() + + self._write_to_graph() + self._store_report() + + def _reset(self): + """Reset this plugin""" + self.nr_of_executed_insns = 0 + self.begin = None + self.end = None + self.coverage = {} + + def _store_report(self): + """Store the results of this plugin""" + pass + + def _write_to_graph(self): + """Write the coverage results to a graph""" + traces = [] + for byte_code, trace_data in self.coverage.items(): + traces += [ + list(trace_data.keys()), + list(trace_data.values()), + 'r--' + ] + + plt.plot(*traces) + plt.axis([0, self.end - self.begin, 0, 100]) + plt.xlabel("Duration (seconds)") + plt.ylabel("Coverage (percentage)") + + plt.savefig("{}.png".format(self.name)) From f675b088896b10d1f76b8f6b3180aee92b9e2cad Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Thu, 7 Feb 2019 13:19:38 +0100 Subject: [PATCH 16/22] apply style rules --- mythril/laser/ethereum/plugins/benchmark.py | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/mythril/laser/ethereum/plugins/benchmark.py b/mythril/laser/ethereum/plugins/benchmark.py index d608f5c6..530c312e 100644 --- a/mythril/laser/ethereum/plugins/benchmark.py +++ b/mythril/laser/ethereum/plugins/benchmark.py @@ -74,11 +74,7 @@ class BenchmarkPlugin: """Write the coverage results to a graph""" traces = [] for byte_code, trace_data in self.coverage.items(): - traces += [ - list(trace_data.keys()), - list(trace_data.values()), - 'r--' - ] + traces += [list(trace_data.keys()), list(trace_data.values()), "r--"] plt.plot(*traces) plt.axis([0, self.end - self.begin, 0, 100]) From 0e700ce58d5db4d15bca8c0ee9995fed2ac5bf01 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Fri, 8 Feb 2019 11:44:04 +0100 Subject: [PATCH 17/22] add dock strings --- mythril/laser/smt/solver/solver_statistics.py | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/mythril/laser/smt/solver/solver_statistics.py b/mythril/laser/smt/solver/solver_statistics.py index 0f5ff4c4..48460094 100644 --- a/mythril/laser/smt/solver/solver_statistics.py +++ b/mythril/laser/smt/solver/solver_statistics.py @@ -6,6 +6,7 @@ from typing import Callable def stat_smt_query(func: Callable): + """Measures statistics for annotated smt query check function""" stat_store = SolverStatistics() def function_wrapper(*args, **kwargs): @@ -26,6 +27,10 @@ def stat_smt_query(func: Callable): class SolverStatistics(object, metaclass=Singleton): + """ Solver Statistics Class + + Keeps track of the important statistics around smt queries + """ def __init__(self): self.enabled = False self.query_count = 0 From 3ad020a6a213d677aadd5bc6739672d150f2fac0 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Sat, 9 Feb 2019 21:10:53 +0530 Subject: [PATCH 18/22] Redirect stdout to null when executing self.raw.check() --- mythril/laser/smt/solver.py | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/mythril/laser/smt/solver.py b/mythril/laser/smt/solver.py index b3754e94..55d6d4ef 100644 --- a/mythril/laser/smt/solver.py +++ b/mythril/laser/smt/solver.py @@ -1,4 +1,6 @@ """This module contains an abstract SMT representation of an SMT solver.""" +import os +import sys import z3 from typing import Union, cast, TypeVar, Generic, List, Sequence @@ -44,10 +46,14 @@ class BaseSolver(Generic[T]): def check(self) -> z3.CheckSatResult: """Returns z3 smt check result. - - :return: + Also suppresses the stdout when running z3 library's check() to avoid unnecessary output + :return: The evaluated result which is either of sat, unsat or unknown """ - return self.raw.check() + old_stdout = sys.stdout + sys.stdout = open(os.devnull, "w") + evaluate = self.raw.check() + sys.stdout = old_stdout + return evaluate def model(self) -> Model: """Returns z3 model for a solution. From f421811d1b8db7b103c070dede5f1f5ad803fa3e Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Mon, 11 Feb 2019 16:22:27 +0700 Subject: [PATCH 19/22] Update README.md --- README.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index d3344d43..f1c7d314 100644 --- a/README.md +++ b/README.md @@ -13,9 +13,11 @@ Mythril Classic is an open-source security analysis tool for Ethereum smart contracts. It uses concolic analysis, taint analysis and control flow checking to detect a variety of security vulnerabilities. +Note that Mythril Classic is an experimental tool. If you are a smart contract developer, we recommend using [MythX](https://mythx.io), our next-gen smart contract security API that [integrates with Truffle Framework](https://github.com/ConsenSys/truffle-security) and other development environments. + Whether you want to contribute, need support, or want to learn what we have cooking for the future, our [Discord server](https://discord.gg/E3YrVtG) will serve your needs. -Oh and by the way, we're also building an [easy-to-use security analysis API called MythX](https://mythx.io) that integrates seamlessly with Truffle, Visual Studio Code, Github and other environments. If you're looking for tooling to plug into your SDLC you should check it out. + ## Installation and setup From c4a96568edd283d16fb78025935da64c13678f3d Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Mon, 11 Feb 2019 16:24:56 +0700 Subject: [PATCH 20/22] Update README.md --- README.md | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/README.md b/README.md index f1c7d314..39ac44f0 100644 --- a/README.md +++ b/README.md @@ -13,12 +13,10 @@ Mythril Classic is an open-source security analysis tool for Ethereum smart contracts. It uses concolic analysis, taint analysis and control flow checking to detect a variety of security vulnerabilities. -Note that Mythril Classic is an experimental tool. If you are a smart contract developer, we recommend using [MythX](https://mythx.io), our next-gen smart contract security API that [integrates with Truffle Framework](https://github.com/ConsenSys/truffle-security) and other development environments. +To smart contract developers we recommend using [MythX](https://mythx.io), our next-gen smart contract security API that [integrates with Truffle Framework](https://github.com/ConsenSys/truffle-security) and other development environments. Whether you want to contribute, need support, or want to learn what we have cooking for the future, our [Discord server](https://discord.gg/E3YrVtG) will serve your needs. - - ## Installation and setup Get it with [Docker](https://www.docker.com): From d757d422f3643e20b41935a940eaa19dbf9091e9 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Mon, 11 Feb 2019 16:26:51 +0700 Subject: [PATCH 21/22] Update README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 39ac44f0..d0c6cdfb 100644 --- a/README.md +++ b/README.md @@ -13,7 +13,7 @@ Mythril Classic is an open-source security analysis tool for Ethereum smart contracts. It uses concolic analysis, taint analysis and control flow checking to detect a variety of security vulnerabilities. -To smart contract developers we recommend using [MythX](https://mythx.io), our next-gen smart contract security API that [integrates with Truffle Framework](https://github.com/ConsenSys/truffle-security) and other development environments. +If you a smart contract developer who wants convenience and comprehensive results, you should be using [MythX](https://mythx.io), our next-gen smart contract security API that [integrates with Truffle Framework](https://github.com/ConsenSys/truffle-security) and other development environments. Whether you want to contribute, need support, or want to learn what we have cooking for the future, our [Discord server](https://discord.gg/E3YrVtG) will serve your needs. From aa4ac48045d46f07b79feea4d75a459762da27c6 Mon Sep 17 00:00:00 2001 From: JoranHonig Date: Mon, 11 Feb 2019 11:13:19 +0100 Subject: [PATCH 22/22] add missing word to comment 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 c57e6f96..7df300ec 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -39,7 +39,7 @@ class OverUnderflowAnnotation: class OverUnderflowStateAnnotation(StateAnnotation): - """ State Annotation used if an overflow both possible and used in the annotated path""" + """ State Annotation used if an overflow is both possible and used in the annotated path""" def __init__( self, overflowing_state: GlobalState, operator: str, constraint