Merge pull request #1353 from ConsenSys/feature/laser_plugins

Mythril Laser Plugins
pull/1377/head
JoranHonig 5 years ago committed by GitHub
commit 9e1403ab95
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
  1. 1
      mythril/analysis/__init__.py
  2. 31
      mythril/analysis/symbolic.py
  3. 1
      mythril/interfaces/cli.py
  4. 7
      mythril/laser/ethereum/plugins/implementations/__init__.py
  5. 3
      mythril/laser/ethereum/plugins/implementations/coverage/__init__.py
  6. 41
      mythril/laser/ethereum/plugins/plugin_factory.py
  7. 38
      mythril/laser/ethereum/plugins/plugin_loader.py
  8. 8
      mythril/laser/ethereum/state/annotation.py
  9. 33
      mythril/laser/ethereum/svm.py
  10. 1
      mythril/laser/plugin/__init__.py
  11. 21
      mythril/laser/plugin/builder.py
  12. 0
      mythril/laser/plugin/interface.py
  13. 68
      mythril/laser/plugin/loader.py
  14. 11
      mythril/laser/plugin/plugins/__init__.py
  15. 10
      mythril/laser/plugin/plugins/benchmark.py
  16. 3
      mythril/laser/plugin/plugins/coverage/__init__.py
  17. 10
      mythril/laser/plugin/plugins/coverage/coverage_plugin.py
  18. 4
      mythril/laser/plugin/plugins/coverage/coverage_strategy.py
  19. 14
      mythril/laser/plugin/plugins/dependency_pruner.py
  20. 16
      mythril/laser/plugin/plugins/mutation_pruner.py
  21. 4
      mythril/laser/plugin/plugins/plugin_annotations.py
  22. 0
      mythril/laser/plugin/plugins/summary_backup/__init__.py
  23. 0
      mythril/laser/plugin/signals.py
  24. 5
      mythril/mythril/mythril_analyzer.py
  25. 10
      mythril/plugin/interface.py
  26. 22
      mythril/plugin/loader.py

@ -1 +0,0 @@
from mythril.analysis.symbolic import SymExecWrapper

@ -1,12 +1,7 @@
"""This module contains a wrapper around LASER for extended analysis
purposes."""
from mythril.analysis.module import (
EntryPoint,
DetectionModule,
ModuleLoader,
get_detection_module_hooks,
)
from mythril.analysis.module import EntryPoint, ModuleLoader, get_detection_module_hooks
from mythril.laser.ethereum import svm
from mythril.laser.ethereum.iprof import InstructionProfiler
from mythril.laser.ethereum.state.account import Account
@ -23,14 +18,17 @@ from mythril.laser.ethereum.natives import PRECOMPILE_COUNT
from mythril.laser.ethereum.transaction.symbolic import ACTORS
from mythril.laser.ethereum.plugins.plugin_factory import PluginFactory
from mythril.laser.ethereum.plugins.plugin_loader import LaserPluginLoader
from mythril.laser.plugin.loader import LaserPluginLoader
from mythril.laser.plugin.plugins import (
MutationPrunerBuilder,
DependencyPrunerBuilder,
CoveragePluginBuilder,
)
from mythril.laser.ethereum.strategy.extensions.bounded_loops import (
BoundedLoopsStrategy,
)
from mythril.laser.smt import symbol_factory, BitVec
from typing import Union, List, Type, Optional, Tuple
from typing import Union, List, Type, Optional
from mythril.solidity.soliditycontract import EVMContract, SolidityContract
from .ops import Call, VarType, get_variable
@ -58,7 +56,6 @@ class SymExecWrapper:
iprof: Optional[InstructionProfiler] = None,
disable_dependency_pruning: bool = False,
run_analysis_modules: bool = True,
enable_coverage_strategy: bool = False,
custom_modules_directory: str = "",
):
"""
@ -114,8 +111,6 @@ class SymExecWrapper:
hex(ACTORS.attacker.value): attacker_account,
}
instruction_laser_plugin = PluginFactory.build_instruction_coverage_plugin()
self.laser = svm.LaserEVM(
dynamic_loader=dynloader,
max_depth=max_depth,
@ -125,19 +120,17 @@ class SymExecWrapper:
transaction_count=transaction_count,
requires_statespace=requires_statespace,
iprof=iprof,
enable_coverage_strategy=enable_coverage_strategy,
instruction_laser_plugin=instruction_laser_plugin,
)
if loop_bound is not None:
self.laser.extend_strategy(BoundedLoopsStrategy, loop_bound)
plugin_loader = LaserPluginLoader(self.laser)
plugin_loader.load(PluginFactory.build_mutation_pruner_plugin())
plugin_loader.load(instruction_laser_plugin)
plugin_loader = LaserPluginLoader()
plugin_loader.load(CoveragePluginBuilder())
plugin_loader.load(MutationPrunerBuilder())
if not disable_dependency_pruning:
plugin_loader.load(PluginFactory.build_dependency_pruner_plugin())
plugin_loader.load(DependencyPrunerBuilder())
world_state = WorldState()
for account in self.accounts.values():

@ -690,7 +690,6 @@ def execute_command(
use_onchain_data=not args.no_onchain_data,
solver_timeout=args.solver_timeout,
parallel_solving=args.parallel_solving,
enable_coverage_strategy=args.enable_coverage_strategy,
custom_modules_directory=args.custom_modules_directory
if args.custom_modules_directory
else "",

@ -1,7 +0,0 @@
""" Plugin implementations
This module contains the implementation of some features
- benchmarking
- pruning
"""

@ -1,3 +0,0 @@
from mythril.laser.ethereum.plugins.implementations.coverage.coverage_plugin import (
InstructionCoveragePlugin,
)

@ -1,41 +0,0 @@
from mythril.laser.ethereum.plugins.plugin import LaserPlugin
class PluginFactory:
""" The plugin factory constructs the plugins provided with laser """
@staticmethod
def build_benchmark_plugin(name: str) -> LaserPlugin:
""" Creates an instance of the benchmark plugin with the given name """
from mythril.laser.ethereum.plugins.implementations.benchmark import (
BenchmarkPlugin,
)
return BenchmarkPlugin(name)
@staticmethod
def build_mutation_pruner_plugin() -> LaserPlugin:
""" Creates an instance of the mutation pruner plugin"""
from mythril.laser.ethereum.plugins.implementations.mutation_pruner import (
MutationPruner,
)
return MutationPruner()
@staticmethod
def build_instruction_coverage_plugin() -> LaserPlugin:
""" Creates an instance of the instruction coverage plugin"""
from mythril.laser.ethereum.plugins.implementations.coverage import (
InstructionCoveragePlugin,
)
return InstructionCoveragePlugin()
@staticmethod
def build_dependency_pruner_plugin() -> LaserPlugin:
""" Creates an instance of the mutation pruner plugin"""
from mythril.laser.ethereum.plugins.implementations.dependency_pruner import (
DependencyPruner,
)
return DependencyPruner()

@ -1,38 +0,0 @@
from mythril.laser.ethereum.svm import LaserEVM
from mythril.laser.ethereum.plugins.plugin import LaserPlugin
from typing import List
import logging
log = logging.getLogger(__name__)
class LaserPluginLoader:
"""
The LaserPluginLoader is used to abstract the logic relating to plugins.
Components outside of laser thus don't have to be aware of the interface that plugins provide
"""
def __init__(self, symbolic_vm: LaserEVM) -> None:
""" Initializes the plugin loader
:param symbolic_vm: symbolic virtual machine to load plugins for
"""
self.symbolic_vm = symbolic_vm
self.laser_plugins = [] # type: List[LaserPlugin]
def load(self, laser_plugin: LaserPlugin) -> None:
""" Loads the plugin
:param laser_plugin: plugin that will be loaded in the symbolic virtual machine
"""
log.info("Loading plugin: {}".format(str(laser_plugin)))
laser_plugin.initialize(self.symbolic_vm)
self.laser_plugins.append(laser_plugin)
def is_enabled(self, laser_plugin: LaserPlugin) -> bool:
""" Returns whether the plugin is loaded in the symbolic_vm
:param laser_plugin: plugin that will be checked
"""
return laser_plugin in self.laser_plugins

@ -26,6 +26,14 @@ class StateAnnotation:
"""
return False
@property
def persist_over_calls(self) -> bool:
"""If this function returns true then laser will propagate the annotation between calls
The default is set to False
"""
return False
class NoCopyAnnotation(StateAnnotation):
"""This class provides a base annotation class for annotations that

@ -11,10 +11,7 @@ from mythril.laser.ethereum.evm_exceptions import StackUnderflowException
from mythril.laser.ethereum.evm_exceptions import VmException
from mythril.laser.ethereum.instructions import Instruction, transfer_ether
from mythril.laser.ethereum.instruction_data import get_required_stack_elements
from mythril.laser.ethereum.plugins.signals import PluginSkipWorldState, PluginSkipState
from mythril.laser.ethereum.plugins.implementations.plugin_annotations import (
MutationAnnotation,
)
from mythril.laser.plugin.signals import PluginSkipWorldState, PluginSkipState
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
@ -61,8 +58,6 @@ class LaserEVM:
transaction_count=2,
requires_statespace=True,
iprof=None,
enable_coverage_strategy=False,
instruction_laser_plugin=None,
) -> None:
"""
Initializes the laser evm object
@ -111,13 +106,6 @@ class LaserEVM:
self.iprof = iprof
if enable_coverage_strategy:
from mythril.laser.ethereum.plugins.implementations.coverage.coverage_strategy import (
CoverageStrategy,
)
self.strategy = CoverageStrategy(self.strategy, instruction_laser_plugin)
log.info("LASER EVM initialized with dynamic loader: " + str(dynamic_loader))
def extend_strategy(self, extension: ABCMeta, *args) -> None:
@ -393,18 +381,13 @@ class LaserEVM:
# First execute the post hook for the transaction ending instruction
self._execute_post_hook(op_code, [end_signal.global_state])
# Propogate codecall based annotations
if return_global_state.get_current_instruction()["opcode"] in (
"DELEGATECALL",
"CALLCODE",
):
new_annotations = [
annotation
for annotation in global_state.get_annotations(
MutationAnnotation
)
]
return_global_state.add_annotations(new_annotations)
# Propagate annotations
new_annotations = [
annotation
for annotation in global_state.annotations
if annotation.persist_over_calls
]
return_global_state.add_annotations(new_annotations)
new_global_states = self._end_message_call(
copy(return_global_state),

@ -18,4 +18,3 @@ For the implementation of plugins the following modules are of interest:
Which show the basic interfaces with which plugins are able to interact
"""
from mythril.laser.ethereum.plugins.signals import PluginSignal

@ -0,0 +1,21 @@
from mythril.laser.plugin.interface import LaserPlugin
from abc import ABC, abstractmethod
from typing import Optional
class PluginBuilder(ABC):
""" PluginBuilder
The plugin builder interface enables construction of Laser plugins
"""
plugin_name = "Default Plugin Name"
def __init__(self):
self.enabled = True
@abstractmethod
def __call__(self, *args, **kwargs) -> LaserPlugin:
"""Constructs the plugin"""
pass

@ -0,0 +1,68 @@
import logging
from typing import Dict, List, Optional
from mythril.laser.ethereum.svm import LaserEVM
from mythril.laser.plugin.builder import PluginBuilder
from mythril.support.support_utils import Singleton
log = logging.getLogger(__name__)
class LaserPluginLoader(object, metaclass=Singleton):
"""
The LaserPluginLoader is used to abstract the logic relating to plugins.
Components outside of laser thus don't have to be aware of the interface that plugins provide
"""
def __init__(self) -> None:
""" Initializes the plugin loader """
self.laser_plugin_builders = {} # type: Dict[str, PluginBuilder]
def load(self, plugin_builder: PluginBuilder) -> None:
""" Enables a Laser Plugin
:param plugin_builder: Builder that constructs the plugin
"""
log.info(f"Loading laser plugin: {plugin_builder.plugin_name}")
if plugin_builder.plugin_name in self.laser_plugin_builders:
log.warning(
f"Laser plugin with name {plugin_builder.plugin_name} was already loaded, skipping..."
)
return
self.laser_plugin_builders[plugin_builder.plugin_name] = plugin_builder
def is_enabled(self, plugin_name: str) -> bool:
""" Returns whether the plugin is loaded in the symbolic_vm
:param plugin_name: Name of the plugin to check
"""
if plugin_name not in self.laser_plugin_builders:
return False
else:
return self.laser_plugin_builders[plugin_name].enabled
def enable(self, plugin_name: str):
if plugin_name not in self.laser_plugin_builders:
return ValueError(f"Plugin with name: {plugin_name} was not loaded")
self.laser_plugin_builders[plugin_name].enabled = True
def instrument_virtual_machine(
self, symbolic_vm: LaserEVM, with_plugins: Optional[List[str]]
):
""" Load enabled plugins into the passed symbolic virtual machine
:param symbolic_vm: The virtual machine to instrument the plugins with
:param with_plugins: Override the globally enabled/disabled builders and load all plugins in the list
"""
for plugin_name, plugin_builder in self.laser_plugin_builders.items():
enabled = (
plugin_builder.enabled
if not with_plugins
else plugin_name in with_plugins
)
if not enabled:
continue
log.info(f"Instrumenting symbolic vm with plugin: {plugin_name}")
plugin = plugin_builder()
plugin.initialize(symbolic_vm)

@ -0,0 +1,11 @@
""" Plugin implementations
This module contains the implementation of some features
- benchmarking
- pruning
"""
from mythril.laser.plugin.plugins.benchmark import BenchmarkPluginBuilder
from mythril.laser.plugin.plugins.coverage.coverage_plugin import CoveragePluginBuilder
from mythril.laser.plugin.plugins.dependency_pruner import DependencyPrunerBuilder
from mythril.laser.plugin.plugins.mutation_pruner import MutationPrunerBuilder

@ -1,5 +1,6 @@
from mythril.laser.ethereum.svm import LaserEVM
from mythril.laser.ethereum.plugins.plugin import LaserPlugin
from mythril.laser.plugin.interface import LaserPlugin
from mythril.laser.plugin.builder import PluginBuilder
from time import time
import matplotlib.pyplot as plt
import logging
@ -7,6 +8,13 @@ import logging
log = logging.getLogger(__name__)
class BenchmarkPluginBuilder(PluginBuilder):
plugin_name = "benchmark"
def __call__(self, *args, **kwargs):
return BenchmarkPlugin()
# TODO: introduce dependency on coverage plugin
class BenchmarkPlugin(LaserPlugin):
"""Benchmark Plugin

@ -0,0 +1,3 @@
from mythril.laser.plugin.plugins.coverage.coverage_plugin import (
InstructionCoveragePlugin,
)

@ -1,5 +1,6 @@
from mythril.laser.ethereum.svm import LaserEVM
from mythril.laser.ethereum.plugins.plugin import LaserPlugin
from mythril.laser.plugin.interface import LaserPlugin
from mythril.laser.plugin.builder import PluginBuilder
from mythril.laser.ethereum.state.global_state import GlobalState
from typing import Dict, Tuple, List
@ -9,6 +10,13 @@ import logging
log = logging.getLogger(__name__)
class CoveragePluginBuilder(PluginBuilder):
plugin_name = "coverage"
def __call__(self, *args, **kwargs):
return InstructionCoveragePlugin()
class InstructionCoveragePlugin(LaserPlugin):
"""InstructionCoveragePlugin

@ -1,8 +1,6 @@
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.plugin.plugins.coverage import InstructionCoveragePlugin
class CoverageStrategy(BasicSearchStrategy):

@ -1,7 +1,8 @@
from mythril.laser.ethereum.svm import LaserEVM
from mythril.laser.ethereum.plugins.plugin import LaserPlugin
from mythril.laser.ethereum.plugins.signals import PluginSkipState
from mythril.laser.ethereum.plugins.implementations.plugin_annotations import (
from mythril.laser.plugin.interface import LaserPlugin
from mythril.laser.plugin.builder import PluginBuilder
from mythril.laser.plugin.signals import PluginSkipState
from mythril.laser.plugin.plugins.plugin_annotations import (
DependencyAnnotation,
WSDependencyAnnotation,
)
@ -69,6 +70,13 @@ def get_ws_dependency_annotation(state: GlobalState) -> WSDependencyAnnotation:
return annotation
class DependencyPrunerBuilder(PluginBuilder):
plugin_name = "dependency-pruner"
def __call__(self, *args, **kwargs):
return DependencyPruner()
class DependencyPruner(LaserPlugin):
"""Dependency Pruner Plugin

@ -1,8 +1,7 @@
from mythril.laser.ethereum.plugins.signals import PluginSkipWorldState
from mythril.laser.ethereum.plugins.plugin import LaserPlugin
from mythril.laser.ethereum.plugins.implementations.plugin_annotations import (
MutationAnnotation,
)
from mythril.laser.plugin.signals import PluginSkipWorldState
from mythril.laser.plugin.interface import LaserPlugin
from mythril.laser.plugin.builder import PluginBuilder
from mythril.laser.plugin.plugins.plugin_annotations import MutationAnnotation
from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.laser.ethereum.svm import LaserEVM
from mythril.laser.smt import UGT, symbol_factory
@ -13,6 +12,13 @@ from mythril.analysis import solver
from mythril.exceptions import UnsatError
class MutationPrunerBuilder(PluginBuilder):
plugin_name = "mutation-pruner"
def __call__(self, *args, **kwargs):
return MutationPruner()
class MutationPruner(LaserPlugin):
"""Mutation pruner plugin

@ -13,6 +13,10 @@ class MutationAnnotation(StateAnnotation):
def __init__(self):
pass
@property
def persist_over_calls(self) -> bool:
return True
class DependencyAnnotation(StateAnnotation):
"""Dependency Annotation

@ -43,7 +43,6 @@ class MythrilAnalyzer:
enable_iprof: bool = False,
disable_dependency_pruning: bool = False,
solver_timeout: Optional[int] = None,
enable_coverage_strategy: bool = False,
custom_modules_directory: str = "",
sparse_pruning: bool = False,
unconstrained_storage: bool = False,
@ -67,7 +66,6 @@ class MythrilAnalyzer:
self.create_timeout = create_timeout
self.iprof = InstructionProfiler() if enable_iprof else None
self.disable_dependency_pruning = disable_dependency_pruning
self.enable_coverage_strategy = enable_coverage_strategy
self.custom_modules_directory = custom_modules_directory
args.sparse_pruning = sparse_pruning
args.solver_timeout = solver_timeout
@ -91,7 +89,6 @@ class MythrilAnalyzer:
iprof=self.iprof,
disable_dependency_pruning=self.disable_dependency_pruning,
run_analysis_modules=False,
enable_coverage_strategy=self.enable_coverage_strategy,
custom_modules_directory=self.custom_modules_directory,
)
@ -125,7 +122,6 @@ class MythrilAnalyzer:
iprof=self.iprof,
disable_dependency_pruning=self.disable_dependency_pruning,
run_analysis_modules=False,
enable_coverage_strategy=self.enable_coverage_strategy,
custom_modules_directory=self.custom_modules_directory,
)
return generate_graph(sym, physics=enable_physics, phrackify=phrackify)
@ -160,7 +156,6 @@ class MythrilAnalyzer:
compulsory_statespace=False,
iprof=self.iprof,
disable_dependency_pruning=self.disable_dependency_pruning,
enable_coverage_strategy=self.enable_coverage_strategy,
custom_modules_directory=self.custom_modules_directory,
)
issues = fire_lasers(sym, modules)

@ -1,4 +1,5 @@
from abc import ABC, abstractmethod
from mythril.laser.plugin.builder import PluginBuilder as LaserPluginBuilder
class MythrilPlugin:
@ -33,3 +34,12 @@ class MythrilCLIPlugin(MythrilPlugin):
"""
pass
class MythrilLaserPlugin(MythrilPlugin, LaserPluginBuilder, ABC):
""" Mythril Laser Plugin interface
Plugins of this type are used to instrument the laser EVM
"""
pass

@ -1,17 +1,20 @@
from mythril.analysis.module import DetectionModule
from mythril.plugin.interface import MythrilCLIPlugin, MythrilPlugin
from mythril.plugin.interface import MythrilCLIPlugin, MythrilPlugin, MythrilLaserPlugin
from mythril.plugin.discovery import PluginDiscovery
from mythril.support.support_utils import Singleton
from mythril.analysis.module.loader import ModuleLoader
from mythril.laser.plugin.builder import PluginBuilder as LaserPluginBuilder
from mythril.laser.plugin.loader import LaserPluginLoader
import logging
log = logging.getLogger(__name__)
class UnsupportedPluginType(Exception):
"""Raised when a plugin with an unsupported type is loaded"""
pass
@ -27,7 +30,13 @@ class MythrilPluginLoader(object, metaclass=Singleton):
self._load_default_enabled()
def load(self, plugin: MythrilPlugin):
"""Loads the passed plugin"""
"""Loads the passed plugin
This function handles input validation and dispatches loading to type specific loaders.
Supported plugin types:
- laser plugins
- detection modules
"""
if not isinstance(plugin, MythrilPlugin):
raise ValueError("Passed plugin is not of type MythrilPlugin")
logging.info(f"Loading plugin: {plugin.name}")
@ -48,7 +57,14 @@ class MythrilPluginLoader(object, metaclass=Singleton):
log.info(f"Loading detection module: {plugin.name}")
ModuleLoader().register_module(plugin)
@staticmethod
def _load_laser_plugin(plugin: MythrilLaserPlugin):
"""Loads the laser plugin"""
log.info(f"Loading laser plugin: {plugin.name}")
LaserPluginLoader().load(plugin)
def _load_default_enabled(self):
"""Loads the plugins that have the default enabled flag"""
log.info("Loading installed analysis modules that are enabled by default")
for plugin_name in PluginDiscovery().get_plugins(default_enabled=True):
plugin = PluginDiscovery().build_plugin(plugin_name)

Loading…
Cancel
Save