From aad81074f7178d5deb299710c745bd21c5da947c Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Wed, 3 Apr 2019 14:36:16 +0200 Subject: [PATCH 1/4] add type hints to strategy --- mythril/laser/ethereum/strategy/__init__.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/mythril/laser/ethereum/strategy/__init__.py b/mythril/laser/ethereum/strategy/__init__.py index 58672339..140880b0 100644 --- a/mythril/laser/ethereum/strategy/__init__.py +++ b/mythril/laser/ethereum/strategy/__init__.py @@ -1,4 +1,6 @@ from abc import ABC, abstractmethod +from typing import List +from mythril.laser.ethereum.state.global_state import GlobalState class BasicSearchStrategy(ABC): @@ -7,7 +9,7 @@ class BasicSearchStrategy(ABC): __slots__ = "work_list", "max_depth" def __init__(self, work_list, max_depth): - self.work_list = work_list + self.work_list = work_list # type: List[GlobalState] self.max_depth = max_depth def __iter__(self): From c966152d4c3ca8c831ac954b29504f394887d884 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Wed, 3 Apr 2019 14:36:50 +0200 Subject: [PATCH 2/4] move coverage plugin to separate package and add function to check if an instruction has previously been covered --- .../plugins/implementations/coverage/__init__.py | 1 + .../{coverage.py => coverage/coverage_plugin.py} | 9 +++++++++ 2 files changed, 10 insertions(+) create mode 100644 mythril/laser/ethereum/plugins/implementations/coverage/__init__.py rename mythril/laser/ethereum/plugins/implementations/{coverage.py => coverage/coverage_plugin.py} (92%) diff --git a/mythril/laser/ethereum/plugins/implementations/coverage/__init__.py b/mythril/laser/ethereum/plugins/implementations/coverage/__init__.py new file mode 100644 index 00000000..7aff2047 --- /dev/null +++ b/mythril/laser/ethereum/plugins/implementations/coverage/__init__.py @@ -0,0 +1 @@ +from mythril.laser.ethereum.plugins.implementations.coverage.coverage_plugin import InstructionCoveragePlugin diff --git a/mythril/laser/ethereum/plugins/implementations/coverage.py b/mythril/laser/ethereum/plugins/implementations/coverage/coverage_plugin.py similarity index 92% rename from mythril/laser/ethereum/plugins/implementations/coverage.py rename to mythril/laser/ethereum/plugins/implementations/coverage/coverage_plugin.py index ba113b00..75c6bfa4 100644 --- a/mythril/laser/ethereum/plugins/implementations/coverage.py +++ b/mythril/laser/ethereum/plugins/implementations/coverage/coverage_plugin.py @@ -87,3 +87,12 @@ class InstructionCoveragePlugin(LaserPlugin): for _, cv in self.coverage.items(): total_covered_instructions += sum(cv[1]) return total_covered_instructions + + def is_instruction_covered(self, bytecode, index): + if bytecode not in self.coverage.keys(): + return False + + try: + return self.coverage[bytecode][index] + except IndexError: + return False From 1737e50e73e6f90463d55bc17a1752235da8ffca Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Wed, 3 Apr 2019 14:37:45 +0200 Subject: [PATCH 3/4] implement instruction coverage based plugin This search strategy directs the symbolic execution towards "fresh" instructions. --- .../coverage/coverage_strategy.py | 34 +++++++++++++++++++ 1 file changed, 34 insertions(+) create mode 100644 mythril/laser/ethereum/plugins/implementations/coverage/coverage_strategy.py diff --git a/mythril/laser/ethereum/plugins/implementations/coverage/coverage_strategy.py b/mythril/laser/ethereum/plugins/implementations/coverage/coverage_strategy.py new file mode 100644 index 00000000..4390a775 --- /dev/null +++ b/mythril/laser/ethereum/plugins/implementations/coverage/coverage_strategy.py @@ -0,0 +1,34 @@ +from mythril.laser.ethereum.strategy import BasicSearchStrategy +from mythril.laser.ethereum.state.global_state import GlobalState +from mythril.laser.ethereum.plugins.implementations.coverage import InstructionCoveragePlugin + + +class CoverageStrategy(BasicSearchStrategy): + """Implements a instruction coverage based search strategy + + This strategy is quite simple and effective, it prioritizes the execution of instructions that have previously been + uncovered. Once there is no such global state left in the work list, it will resort to using the super_strategy. + + This strategy is intended to be used "on top of" another one + """ + def __init__(self, super_strategy: BasicSearchStrategy, instruction_coverage_plugin: InstructionCoveragePlugin): + self.super_strategy = super_strategy + self.instruction_coverage_plugin = instruction_coverage_plugin + BasicSearchStrategy.__init__(self, super_strategy.work_list, super_strategy.max_depth) + + def get_strategic_global_state(self) -> GlobalState: + """ + Returns the first uncovered global state in the work list if it exists, + otherwise super_strategy.get_strategic_global_state() is returned. + """ + for global_state in self.work_list: + if not self._is_covered(global_state): + self.work_list.remove(global_state) + return global_state + return self.super_strategy.get_strategic_global_state() + + def _is_covered(self, global_state: GlobalState) -> bool: + """ Checks if the instruction for the given global state is already covered""" + bytecode = global_state.environment.code.bytecode + index = global_state.mstate.pc + return self.instruction_coverage_plugin.is_instruction_covered(bytecode, index) From c4b25f482b437f9215796ef243aed13e970d669d Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Wed, 3 Apr 2019 14:40:36 +0200 Subject: [PATCH 4/4] apply style changes --- .../plugins/implementations/coverage/__init__.py | 4 +++- .../implementations/coverage/coverage_strategy.py | 15 ++++++++++++--- 2 files changed, 15 insertions(+), 4 deletions(-) diff --git a/mythril/laser/ethereum/plugins/implementations/coverage/__init__.py b/mythril/laser/ethereum/plugins/implementations/coverage/__init__.py index 7aff2047..b600877d 100644 --- a/mythril/laser/ethereum/plugins/implementations/coverage/__init__.py +++ b/mythril/laser/ethereum/plugins/implementations/coverage/__init__.py @@ -1 +1,3 @@ -from mythril.laser.ethereum.plugins.implementations.coverage.coverage_plugin import InstructionCoveragePlugin +from mythril.laser.ethereum.plugins.implementations.coverage.coverage_plugin import ( + InstructionCoveragePlugin, +) diff --git a/mythril/laser/ethereum/plugins/implementations/coverage/coverage_strategy.py b/mythril/laser/ethereum/plugins/implementations/coverage/coverage_strategy.py index 4390a775..2ffa29d6 100644 --- a/mythril/laser/ethereum/plugins/implementations/coverage/coverage_strategy.py +++ b/mythril/laser/ethereum/plugins/implementations/coverage/coverage_strategy.py @@ -1,6 +1,8 @@ from mythril.laser.ethereum.strategy import BasicSearchStrategy from mythril.laser.ethereum.state.global_state import GlobalState -from mythril.laser.ethereum.plugins.implementations.coverage import InstructionCoveragePlugin +from mythril.laser.ethereum.plugins.implementations.coverage import ( + InstructionCoveragePlugin, +) class CoverageStrategy(BasicSearchStrategy): @@ -11,10 +13,17 @@ class CoverageStrategy(BasicSearchStrategy): This strategy is intended to be used "on top of" another one """ - def __init__(self, super_strategy: BasicSearchStrategy, instruction_coverage_plugin: InstructionCoveragePlugin): + + def __init__( + self, + super_strategy: BasicSearchStrategy, + instruction_coverage_plugin: InstructionCoveragePlugin, + ): self.super_strategy = super_strategy self.instruction_coverage_plugin = instruction_coverage_plugin - BasicSearchStrategy.__init__(self, super_strategy.work_list, super_strategy.max_depth) + BasicSearchStrategy.__init__( + self, super_strategy.work_list, super_strategy.max_depth + ) def get_strategic_global_state(self) -> GlobalState: """