From c07dd05a81eaec40c43c095522ee8b7d95c89340 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Wed, 11 Jul 2018 14:56:50 +0200 Subject: [PATCH] Use dfs by default --- mythril/analysis/symbolic.py | 12 ++++++++++-- mythril/interfaces/cli.py | 5 ++++- mythril/laser/ethereum/svm.py | 4 ++-- mythril/mythril.py | 8 ++++---- 4 files changed, 20 insertions(+), 9 deletions(-) diff --git a/mythril/analysis/symbolic.py b/mythril/analysis/symbolic.py index 238fe928..5ddf416b 100644 --- a/mythril/analysis/symbolic.py +++ b/mythril/analysis/symbolic.py @@ -3,6 +3,7 @@ from mythril.laser.ethereum import svm import copy import logging from .ops import get_variable, SStore, Call, VarType +from mythril.laser.ethereum.strategy.basic import DepthFirstSearchStrategy, BreadthFirstSearchStrategy class SymExecWrapper: @@ -11,13 +12,20 @@ class SymExecWrapper: Wrapper class for the LASER Symbolic virtual machine. Symbolically executes the code and does a bit of pre-analysis for convenience. ''' - def __init__(self, contract, address, dynloader=None, max_depth=None, execution_timeout=None): + def __init__(self, contract, address, strategy, dynloader=None, max_depth=None, execution_timeout=None): + s_strategy = None + if strategy == 'dfs': + s_strategy = DepthFirstSearchStrategy + elif strategy == 'bfs': + s_strategy = BreadthFirstSearchStrategy + else: + raise ValueError("Invalid strategy argument supplied") account = svm.Account(address, contract.disassembly, contract_name=contract.name) self.accounts = {address: account} - self.laser = svm.LaserEVM(self.accounts, dynamic_loader=dynloader, max_depth=max_depth, execution_timeout=execution_timeout) + self.laser = svm.LaserEVM(self.accounts, dynamic_loader=dynloader, max_depth=max_depth, execution_timeout=execution_timeout, strategy=s_strategy) self.laser.sym_exec(address) diff --git a/mythril/interfaces/cli.py b/mythril/interfaces/cli.py index 23c8fa0d..a729ca3a 100644 --- a/mythril/interfaces/cli.py +++ b/mythril/interfaces/cli.py @@ -66,6 +66,9 @@ def main(): options.add_argument('--max-depth', type=int, default=22, help='Maximum recursion depth for symbolic execution') options.add_argument('--execution-timeout', type=int, default=60, help="The amount of seconds to spend on " "symbolic execution") + outputs.add_argument('--strategy', choices=['dfs', 'bfs'], default='dfs', + help='Symbolic execution strategy') + options.add_argument('--solc-args', help='Extra arguments for solc') options.add_argument('--phrack', action='store_true', help='Phrack-style call graph') options.add_argument('--enable-physics', action='store_true', help='enable graph physics simulation') @@ -194,7 +197,7 @@ def main(): exit_with_error(args.outform, "Error saving graph: " + str(e)) else: - report = mythril.fire_lasers(address=address, + report = mythril.fire_lasers(strategy=args.strategy, address=address, modules=[m.strip() for m in args.modules.strip().split(",")] if args.modules else [], verbose_report=args.verbose_report, max_depth=args.max_depth, execution_timeout=args.execution_timeout) diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index e8ea9331..2106a086 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -23,7 +23,7 @@ class LaserEVM: """ Laser EVM class """ - def __init__(self, accounts, dynamic_loader=None, max_depth=float('inf'), execution_timeout=60, strategy=None): + def __init__(self, accounts, dynamic_loader=None, max_depth=float('inf'), execution_timeout=60, strategy=DepthFirstSearchStrategy): self.accounts = accounts self.nodes = {} @@ -33,7 +33,7 @@ class LaserEVM: self.dynamic_loader = dynamic_loader self.work_list = [] - self.strategy = DepthFirstSearchStrategy(self.work_list, max_depth) if strategy is None else strategy + self.strategy = strategy(self.work_list, max_depth) self.max_depth = max_depth self.execution_timeout = execution_timeout diff --git a/mythril/mythril.py b/mythril/mythril.py index 9d0ce96f..ff0d5b8a 100644 --- a/mythril/mythril.py +++ b/mythril/mythril.py @@ -34,7 +34,6 @@ from mythril.analysis.security import fire_lasers from mythril.analysis.report import Report from mythril.leveldb.client import EthLevelDB - # logging.basicConfig(level=logging.DEBUG) class Mythril(object): @@ -316,15 +315,16 @@ class Mythril(object): max_depth=max_depth) return generate_graph(sym, physics=enable_physics, phrackify=phrackify) - def fire_lasers(self, contracts=None, address=None, + def fire_lasers(self, strategy, contracts=None, address=None, modules=None, - verbose_report=False, max_depth=None, execution_timeout=None): + verbose_report=False, max_depth=None, execution_timeout=None, ): + all_issues = [] if self.dynld and self.eth is None: self.set_api_rpc_infura() for contract in (contracts or self.contracts): - sym = SymExecWrapper(contract, address, + sym = SymExecWrapper(contract, address, strategy, dynloader=DynLoader(self.eth) if self.dynld else None, max_depth=max_depth, execution_timeout=execution_timeout)