Skip to content

Commit 1396933

Browse files
norhhnorhh
authored
Add additional analysis modules (#1836)
* Update z3 * Add analysis modules * Modify test
1 parent 57dbd0c commit 1396933

12 files changed

+486
-6
lines changed

‎mythril/analysis/module/loader.py

+11-3
Original file line numberDiff line numberDiff line change
@@ -14,12 +14,17 @@
1414
from mythril.analysis.module.modules.external_calls import ExternalCalls
1515
from mythril.analysis.module.modules.integer import IntegerArithmetics
1616
from mythril.analysis.module.modules.multiple_sends import MultipleSends
17+
from mythril.analysis.module.modules.requirements_violation import RequirementsViolation
1718
from mythril.analysis.module.modules.state_change_external_calls import (
1819
StateChangeAfterCall,
1920
)
2021
from mythril.analysis.module.modules.suicide import AccidentallyKillable
22+
from mythril.analysis.module.modules.transaction_order_dependence import (
23+
TransactionOrderDependence,
24+
)
2125
from mythril.analysis.module.modules.unchecked_retval import UncheckedRetval
2226
from mythril.analysis.module.modules.user_assertions import UserAssertions
27+
from mythril.analysis.module.modules.unexpected_ether import UnexpectedEther
2328

2429
from mythril.analysis.module.base import EntryPoint
2530

@@ -90,19 +95,22 @@ def get_detection_modules(
9095
def _register_mythril_modules(self):
9196
self._modules.extend(
9297
[
98+
AccidentallyKillable(),
9399
ArbitraryJump(),
94100
ArbitraryStorage(),
95101
ArbitraryDelegateCall(),
96-
PredictableVariables(),
97-
TxOrigin(),
98102
EtherThief(),
99103
Exceptions(),
100104
ExternalCalls(),
101105
IntegerArithmetics(),
102106
MultipleSends(),
107+
PredictableVariables(),
108+
RequirementsViolation(),
103109
StateChangeAfterCall(),
104-
AccidentallyKillable(),
110+
TransactionOrderDependence(),
111+
TxOrigin(),
105112
UncheckedRetval(),
113+
UnexpectedEther(),
106114
UserAssertions(),
107115
]
108116
)

‎mythril/analysis/module/modules/requirements_violation.py

+85
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,85 @@
1+
"""This module contains the detection code for requirement violations in a call"""
2+
import logging
3+
4+
from mythril.analysis import solver
5+
from mythril.analysis.module.base import DetectionModule
6+
from mythril.analysis.report import Issue
7+
from mythril.analysis.issue_annotation import IssueAnnotation
8+
from mythril.laser.smt import And
9+
from mythril.analysis.swc_data import REQUIREMENT_VIOLATION
10+
from mythril.exceptions import UnsatError
11+
from mythril.laser.ethereum.state.global_state import GlobalState
12+
13+
from typing import List
14+
15+
log = logging.getLogger(__name__)
16+
17+
18+
class RequirementsViolation(DetectionModule):
19+
"""This module detects transaction order dependence"""
20+
21+
name = "Requirement Violation"
22+
swc_id = REQUIREMENT_VIOLATION
23+
description = "Checks whether any requirements violate in a call."
24+
entrypoint = "callback"
25+
pre_hooks = ["REVERT"]
26+
plugin_default_enabled = True
27+
28+
def _execute(self, state: GlobalState) -> List[Issue]:
29+
"""
30+
31+
:param state:
32+
:return:
33+
"""
34+
issues = self._analyze_state(state)
35+
for issue in issues:
36+
self.cache.add((issue.source_location, issue.bytecode_hash))
37+
return issues
38+
39+
def _analyze_state(self, state) -> List[Issue]:
40+
"""
41+
42+
:param state:
43+
:return:
44+
"""
45+
46+
if len(state.transaction_stack) < 2:
47+
return []
48+
49+
try:
50+
address = state.get_current_instruction()["address"]
51+
description_head = "A requirement was violated in a nested call and the call was reverted as a result."
52+
description_tail = "Make sure valid inputs are provided to the nested call (for instance, via passed arguments)."
53+
transaction_sequence = solver.get_transaction_sequence(
54+
state, state.world_state.constraints
55+
)
56+
issue = Issue(
57+
contract=state.environment.active_account.contract_name,
58+
function_name=state.environment.active_function_name,
59+
address=address,
60+
swc_id=REQUIREMENT_VIOLATION,
61+
title="requirement violation",
62+
severity="Medium",
63+
description_head=description_head,
64+
description_tail=description_tail,
65+
bytecode=state.environment.code.bytecode,
66+
transaction_sequence=transaction_sequence,
67+
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
68+
)
69+
state.annotate(
70+
IssueAnnotation(
71+
conditions=[And(*state.world_state.constraints)],
72+
issue=issue,
73+
detector=self,
74+
)
75+
)
76+
77+
return [issue]
78+
79+
except UnsatError:
80+
log.debug("no model found")
81+
82+
return []
83+
84+
85+
detector = RequirementsViolation()

‎mythril/analysis/module/modules/transaction_order_dependence.py

+138
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,138 @@
1+
"""This module contains the detection code for transaction order dependence."""
2+
3+
from mythril.analysis import solver
4+
from mythril.analysis.potential_issues import (
5+
PotentialIssue,
6+
get_potential_issues_annotation,
7+
)
8+
from mythril.analysis.swc_data import TX_ORDER_DEPENDENCE
9+
from mythril.laser.ethereum.transaction.symbolic import ACTORS
10+
from mythril.analysis.module.base import DetectionModule
11+
from mythril.laser.smt import Or, Bool
12+
from mythril.laser.ethereum.state.global_state import GlobalState
13+
from mythril.exceptions import UnsatError
14+
import logging
15+
16+
log = logging.getLogger(__name__)
17+
18+
DESCRIPTION = """
19+
20+
Search for calls whose value depends on balance or storage.
21+
22+
"""
23+
24+
25+
class BalanceAnnotation:
26+
def __init__(self, caller):
27+
self.caller = caller
28+
29+
30+
class StorageAnnotation:
31+
def __init__(self, caller):
32+
self.caller = caller
33+
34+
35+
class TransactionOrderDependence(DetectionModule):
36+
"""This module detects transaction order dependence."""
37+
38+
name = "Transaction Order Dependence"
39+
swc_id = TX_ORDER_DEPENDENCE
40+
description = DESCRIPTION
41+
entrypoint = "callback"
42+
pre_hooks = ["CALL"]
43+
post_hooks = ["BALANCE", "SLOAD"]
44+
plugin_default_enabled = True
45+
46+
def _execute(self, state: GlobalState) -> None:
47+
"""
48+
49+
:param state:
50+
:return:
51+
"""
52+
potential_issues = self._analyze_state(state)
53+
54+
annotation = get_potential_issues_annotation(state)
55+
annotation.potential_issues.extend(potential_issues)
56+
57+
@staticmethod
58+
def annotate_balance_storage_vals(state, opcode):
59+
val = state.mstate.stack[-1]
60+
if opcode == "BALANCE":
61+
annotation = BalanceAnnotation
62+
else:
63+
annotation = StorageAnnotation
64+
if len(val.get_annotations(annotation)) == 0:
65+
state.mstate.stack[-1].annotate(annotation(state.environment.sender))
66+
return []
67+
68+
def _analyze_state(self, state: GlobalState):
69+
"""
70+
71+
:param state:
72+
:return:
73+
"""
74+
opcode = state.get_current_instruction()["opcode"]
75+
if opcode != "CALL":
76+
opcode = state.environment.code.instruction_list[state.mstate.pc - 1][
77+
"opcode"
78+
]
79+
if opcode in ("BALANCE", "SLOAD"):
80+
self.annotate_balance_storage_vals(state, opcode)
81+
return []
82+
83+
value = state.mstate.stack[-3]
84+
if (
85+
len(value.get_annotations(StorageAnnotation))
86+
+ len(value.get_annotations(BalanceAnnotation))
87+
== 0
88+
):
89+
return []
90+
callers = []
91+
92+
storage_annotations = value.get_annotations(StorageAnnotation)
93+
if len(storage_annotations) == 1:
94+
callers.append(storage_annotations[0].caller)
95+
balance_annotations = value.get_annotations(BalanceAnnotation)
96+
if len(balance_annotations) == 1:
97+
callers.append(balance_annotations[0].caller)
98+
99+
address = state.get_current_instruction()["address"]
100+
call_constraint = Bool(False)
101+
for caller in callers:
102+
call_constraint = Or(call_constraint, ACTORS.attacker == caller)
103+
104+
try:
105+
constraints = state.world_state.constraints + [call_constraint]
106+
107+
solver.get_transaction_sequence(state, constraints)
108+
109+
description_head = (
110+
"The value of the call is dependent on balance or storage write"
111+
)
112+
description_tail = (
113+
"This can lead to race conditions. An attacker may be able to run a transaction after our transaction "
114+
"which can change the value of the call"
115+
)
116+
117+
issue = PotentialIssue(
118+
contract=state.environment.active_account.contract_name,
119+
function_name=state.environment.active_function_name,
120+
address=address,
121+
swc_id=TX_ORDER_DEPENDENCE,
122+
title="Transaction Order Dependence",
123+
bytecode=state.environment.code.bytecode,
124+
severity="Medium",
125+
description_head=description_head,
126+
description_tail=description_tail,
127+
constraints=constraints,
128+
detector=self,
129+
)
130+
131+
except UnsatError:
132+
log.debug("[Transaction Order Dependence] No model found.")
133+
return []
134+
135+
return [issue]
136+
137+
138+
detector = TransactionOrderDependence()

0 commit comments

Comments
 (0)