Skip to content

Commit 2b5445f

Browse files
authored
Add new features (#1841)
1 parent 1396933 commit 2b5445f

21 files changed

+953
-15
lines changed

mythril/analysis/symbolic.py

+2
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,7 @@
2424
MutationPrunerBuilder,
2525
DependencyPrunerBuilder,
2626
CoveragePluginBuilder,
27+
CoverageMetricsPluginBuilder,
2728
CallDepthLimitBuilder,
2829
InstructionProfilerBuilder,
2930
SymbolicSummaryPluginBuilder,
@@ -143,6 +144,7 @@ def __init__(
143144
)
144145

145146
plugin_loader = LaserPluginLoader()
147+
plugin_loader.load(CoverageMetricsPluginBuilder())
146148
if not args.disable_coverage_strategy:
147149
plugin_loader.load(CoveragePluginBuilder())
148150
if not args.disable_mutation_pruner:

mythril/concolic/concolic_execution.py

-1
Original file line numberDiff line numberDiff line change
@@ -74,7 +74,6 @@ def concolic_execution(
7474
:param solver_timeout: Solver timeout
7575
7676
"""
77-
7877
init_state, trace = concrete_execution(concrete_data)
7978
args.solver_timeout = solver_timeout
8079
output_list = flip_branches(

mythril/concolic/find_trace.py

+5-5
Original file line numberDiff line numberDiff line change
@@ -12,11 +12,13 @@
1212
from mythril.laser.ethereum.state.world_state import WorldState
1313
from mythril.laser.ethereum.state.account import Account
1414
from mythril.laser.ethereum.time_handler import time_handler
15+
from mythril.laser.plugin.plugins import TraceFinderBuilder
1516
from mythril.laser.ethereum.transaction.concolic import execute_transaction
1617
from mythril.laser.plugin.loader import LaserPluginLoader
1718
from mythril.laser.smt import Expression, BitVec, symbol_factory
1819
from mythril.laser.ethereum.transaction.transaction_models import tx_id_manager
1920
from mythril.plugin.discovery import PluginDiscovery
21+
from mythril.support.support_args import args
2022

2123

2224
def setup_concrete_initial_state(concrete_data: ConcreteData) -> WorldState:
@@ -30,12 +32,11 @@ def setup_concrete_initial_state(concrete_data: ConcreteData) -> WorldState:
3032
account = Account(address, concrete_storage=True)
3133
account.code = Disassembly(details["code"][2:])
3234
account.nonce = details["nonce"]
33-
if isinstance(type(details["storage"]), str):
35+
if isinstance(details["storage"], str):
3436
details["storage"] = eval(details["storage"]) # type: ignore
3537
for key, value in details["storage"].items():
3638
key_bitvec = symbol_factory.BitVecVal(int(key, 16), 256)
3739
account.storage[key_bitvec] = symbol_factory.BitVecVal(int(value, 16), 256)
38-
3940
world_state.put_account(account)
4041
account.set_balance(int(details["balance"], 16))
4142
return world_state
@@ -47,16 +48,15 @@ def concrete_execution(concrete_data: ConcreteData) -> Tuple[WorldState, List]:
4748
:param concrete_data: Concrete data
4849
:return: path trace
4950
"""
51+
args.pruning_factor = 1
5052
tx_id_manager.restart_counter()
5153
init_state = setup_concrete_initial_state(concrete_data)
5254
laser_evm = LaserEVM(execution_timeout=1000)
5355
laser_evm.open_states = [deepcopy(init_state)]
5456
plugin_loader = LaserPluginLoader()
55-
assert PluginDiscovery().is_installed("myth_concolic_execution")
56-
trace_plugin = PluginDiscovery().installed_plugins["myth_concolic_execution"]()
57+
plugin_loader.load(TraceFinderBuilder())
5758
time_handler.start_execution(laser_evm.execution_timeout)
5859

59-
plugin_loader.load(trace_plugin)
6060
laser_evm.time = datetime.now()
6161
plugin_loader.instrument_virtual_machine(laser_evm, None)
6262
for transaction in concrete_data["steps"]:

mythril/interfaces/cli.py

+8-9
Original file line numberDiff line numberDiff line change
@@ -300,15 +300,14 @@ def main() -> None:
300300
)
301301
create_disassemble_parser(disassemble_parser)
302302

303-
if PluginDiscovery().is_installed("myth_concolic_execution"):
304-
concolic_parser = subparsers.add_parser(
305-
CONCOLIC_LIST[0],
306-
help="Runs concolic execution to flip the desired branches",
307-
aliases=CONCOLIC_LIST[1:],
308-
parents=[],
309-
formatter_class=RawTextHelpFormatter,
310-
)
311-
create_concolic_parser(concolic_parser)
303+
concolic_parser = subparsers.add_parser(
304+
CONCOLIC_LIST[0],
305+
help="Runs concolic execution to flip the desired branches",
306+
aliases=CONCOLIC_LIST[1:],
307+
parents=[],
308+
formatter_class=RawTextHelpFormatter,
309+
)
310+
create_concolic_parser(concolic_parser)
312311

313312
foundry_parser = subparsers.add_parser(
314313
FOUNDRY_LIST[0],

mythril/laser/plugin/plugins/__init__.py

+2
Original file line numberDiff line numberDiff line change
@@ -12,3 +12,5 @@
1212
from mythril.laser.plugin.plugins.call_depth_limiter import CallDepthLimitBuilder
1313
from mythril.laser.plugin.plugins.instruction_profiler import InstructionProfilerBuilder
1414
from mythril.laser.plugin.plugins.summary import SymbolicSummaryPluginBuilder
15+
from mythril.laser.plugin.plugins.trace import TraceFinderBuilder
16+
from mythril.laser.plugin.plugins.coverage_metrics import CoverageMetricsPluginBuilder
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
from .metrics_plugin import CoverageMetricsPluginBuilder
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
BATCH_OF_STATES = 5
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,73 @@
1+
import json
2+
from typing import Dict, List
3+
4+
from mythril.support.support_utils import get_code_hash
5+
from mythril.laser.execution_info import ExecutionInfo
6+
7+
8+
class InstructionCoverageInfo(ExecutionInfo):
9+
def __init__(self):
10+
self._instruction_coverage = {} # type: Dict[str, int]
11+
12+
def as_dict(self):
13+
return dict(instruction_discovery_time=self._instruction_coverage)
14+
15+
def get_code_instr_hex(self, code: str, instruction: int):
16+
code_hash = get_code_hash(code)[2:]
17+
instruction_hex = hex(instruction)[2:]
18+
return "{}:{}".format(code_hash, instruction_hex)
19+
20+
def is_covered(self, code: str, instruction: int):
21+
code_instr_hex = self.get_code_instr_hex(code, instruction)
22+
return code_instr_hex in self._instruction_coverage
23+
24+
def add_data(self, code: str, instruction: int, discovery_time: int):
25+
code_instr_hex = self.get_code_instr_hex(code, instruction)
26+
self._instruction_coverage[code_instr_hex] = discovery_time
27+
28+
def output(self, filename: str):
29+
with open(filename, "w") as outfile:
30+
json.dump(
31+
self._instruction_coverage, default=lambda o: o.__dict__, fp=outfile
32+
)
33+
34+
35+
class CoverageData:
36+
def __init__(
37+
self,
38+
instructions_covered: int,
39+
total_instructions: int,
40+
branches_covered: int,
41+
tx_id: int,
42+
total_branches: int,
43+
state_counter: int,
44+
code: str,
45+
time_elapsed: int,
46+
):
47+
self.instructions_covered = instructions_covered
48+
self.total_instructions = total_instructions
49+
self.branches_covered = branches_covered
50+
self.tx_id = tx_id
51+
self.total_branches = total_branches
52+
self.state_counter = state_counter
53+
self.code_hash = get_code_hash(code)[2:]
54+
self.time_elapsed = time_elapsed
55+
56+
def as_dict(self):
57+
return self.__dict__
58+
59+
60+
class CoverageTimeSeries(ExecutionInfo):
61+
def __init__(self):
62+
self.coverage = [] # type: List[CoverageData]
63+
64+
def output(self, filename: str):
65+
with open(filename, "w") as outfile:
66+
json.dump(self.coverage, default=lambda o: o.__dict__, fp=outfile)
67+
68+
def as_dict(self):
69+
return dict(coverage=self.coverage)
70+
71+
def add_data(self, *args, **kwargs):
72+
cov_data = CoverageData(*args, **kwargs)
73+
self.coverage.append(cov_data.as_dict())
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,131 @@
1+
from mythril.laser.ethereum.svm import LaserEVM
2+
from mythril.laser.plugin.interface import LaserPlugin
3+
from mythril.laser.plugin.builder import PluginBuilder
4+
from mythril.laser.ethereum.state.global_state import GlobalState
5+
from .coverage_data import (
6+
CoverageTimeSeries,
7+
InstructionCoverageInfo,
8+
)
9+
from .constants import BATCH_OF_STATES
10+
from typing import Dict, Tuple, List
11+
12+
import time
13+
import logging
14+
15+
log = logging.getLogger(__name__)
16+
17+
18+
class CoverageMetricsPluginBuilder(PluginBuilder):
19+
"""CoveragePlugin
20+
Checks Instruction and branch coverage and puts it to data.json file
21+
which appears in the directory in which mythril is run.
22+
"""
23+
24+
plugin_default_enabled = True
25+
enabled = True
26+
27+
author = "MythX Development Team"
28+
plugin_name = "MythX Coverage Metrics"
29+
plugin_license = "All rights reserved."
30+
plugin_type = "Laser Plugin"
31+
plugin_description = (
32+
"This plugin measures coverage throughout symbolic execution,"
33+
" reporting it at the end in the MythX coverage format."
34+
)
35+
36+
def __call__(self, *args, **kwargs):
37+
"""Constructs the plugin"""
38+
return LaserCoveragePlugin()
39+
40+
41+
class LaserCoveragePlugin(LaserPlugin):
42+
def __init__(self):
43+
self.instruction_coverage_data = {} # type: Dict[str, Tuple[int, Dict[bool]]]
44+
self.branch_possibilities = {} # type: Dict[str, Dict[int, List]]
45+
self.tx_id = 0
46+
self.state_counter = 0
47+
self.coverage = CoverageTimeSeries()
48+
self.instruction_coverage_info = InstructionCoverageInfo()
49+
self.start_time = time.time_ns()
50+
51+
def initialize(self, symbolic_vm: LaserEVM) -> None:
52+
"""Initializes the instruction coverage plugin
53+
54+
Introduces hooks for each instruction
55+
:param symbolic_vm: The symbolic virtual machine to initialise this plugin for
56+
"""
57+
log.info("Initializing coverage metrics plugin")
58+
59+
self.instruction_coverage_data = {}
60+
self.branch_possibilities = {}
61+
self.tx_id = 0
62+
63+
# Add the instruction coverage ExecutionInfo to laser vm for use in reporting
64+
symbolic_vm.execution_info.append(self.instruction_coverage_info)
65+
symbolic_vm.execution_info.append(self.coverage)
66+
67+
@symbolic_vm.laser_hook("execute_state")
68+
def execute_state_hook(global_state: GlobalState):
69+
self._update_instruction_coverage_data(global_state)
70+
self._update_branch_coverage_data(global_state)
71+
self.state_counter += 1
72+
if self.state_counter == BATCH_OF_STATES:
73+
self._record_coverage()
74+
self.state_counter = 0
75+
76+
@symbolic_vm.laser_hook("stop_sym_trans")
77+
def execute_stop_sym_trans_hook():
78+
self.tx_id += 1
79+
80+
# The following is useful for debugging
81+
# @symbolic_vm.laser_hook("stop_sym_exec")
82+
# def execute_stop_sym_exec_hook():
83+
# self.coverage.output("coverage_data.json")
84+
# self.instruction_coverage_info.output("instruction_discovery_data.json")
85+
86+
def _update_instruction_coverage_data(self, global_state: GlobalState):
87+
"""Records instruction coverage"""
88+
code = global_state.environment.code.bytecode
89+
if code not in self.instruction_coverage_data.keys():
90+
number_of_instructions = len(global_state.environment.code.instruction_list)
91+
self.instruction_coverage_data[code] = (number_of_instructions, {})
92+
current_instr = global_state.get_current_instruction()["address"]
93+
if self.instruction_coverage_info.is_covered(code, current_instr) is False:
94+
self.instruction_coverage_info.add_data(
95+
code, current_instr, time.time_ns() - self.start_time
96+
)
97+
self.instruction_coverage_data[code][1][current_instr] = True
98+
99+
def _update_branch_coverage_data(self, global_state: GlobalState):
100+
"""Records branch coverage"""
101+
code = global_state.environment.code.bytecode
102+
if code not in self.branch_possibilities:
103+
self.branch_possibilities[code] = {}
104+
105+
if global_state.get_current_instruction()["opcode"] != "JUMPI":
106+
return
107+
addr = global_state.get_current_instruction()["address"]
108+
jump_addr = global_state.mstate.stack[-1]
109+
if jump_addr.symbolic:
110+
log.debug("Encountered a symbolic jump, ignoring it for branch coverage")
111+
return
112+
self.branch_possibilities[code][addr] = [addr + 1, jump_addr.value]
113+
114+
def _record_coverage(self):
115+
for code, code_cov in self.instruction_coverage_data.items():
116+
total_branches = 0
117+
branches_covered = 0
118+
for jumps, branches in self.branch_possibilities[code].items():
119+
for branch in branches:
120+
total_branches += 1
121+
branches_covered += branch in code_cov[1]
122+
self.coverage.add_data(
123+
code=code,
124+
instructions_covered=len(code_cov[1]),
125+
total_instructions=code_cov[0],
126+
branches_covered=branches_covered,
127+
tx_id=self.tx_id,
128+
total_branches=total_branches,
129+
state_counter=self.state_counter,
130+
time_elapsed=time.time_ns() - self.start_time,
131+
)

mythril/laser/plugin/plugins/trace.py

+48
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,48 @@
1+
from mythril.laser.plugin.interface import LaserPlugin
2+
from mythril.laser.plugin.builder import PluginBuilder
3+
from mythril.laser.ethereum.state.global_state import GlobalState
4+
from mythril.laser.ethereum.svm import LaserEVM
5+
from typing import List, Tuple
6+
7+
8+
class TraceFinderBuilder(PluginBuilder):
9+
name = "trace-finder"
10+
plugin_default_enabled = True
11+
enabled = True
12+
13+
author = "MythX Development Team"
14+
name = "MythX Trace Finder"
15+
plugin_license = "All rights reserved."
16+
plugin_type = "Laser Plugin"
17+
plugin_version = "0.0.1 "
18+
plugin_description = "This plugin merges states after the end of a transaction"
19+
20+
def __call__(self, *args, **kwargs):
21+
return TraceFinder()
22+
23+
24+
class TraceFinder(LaserPlugin):
25+
def __init__(self):
26+
self._reset()
27+
28+
def _reset(self):
29+
self.tx_trace: List[List[Tuple[int, str]]] = []
30+
31+
def initialize(self, symbolic_vm: LaserEVM):
32+
"""Initializes Trace Finder
33+
34+
Introduces hooks during the start of the execution and each execution state
35+
:param symbolic_vm:
36+
:return:
37+
"""
38+
self._reset()
39+
40+
@symbolic_vm.laser_hook("start_exec")
41+
def start_sym_trans_hook():
42+
self.tx_trace.append([])
43+
44+
@symbolic_vm.laser_hook("execute_state")
45+
def trace_jumpi_hook(global_state: GlobalState):
46+
self.tx_trace[-1].append(
47+
(global_state.mstate.pc, global_state.current_transaction.id)
48+
)

0 commit comments

Comments
 (0)