|
|
@ -5,7 +5,7 @@ from mythril.analysis import solver |
|
|
|
from mythril.analysis.swc_data import REENTRANCY |
|
|
|
from mythril.analysis.swc_data import REENTRANCY |
|
|
|
from mythril.analysis.modules.base import DetectionModule |
|
|
|
from mythril.analysis.modules.base import DetectionModule |
|
|
|
from mythril.analysis.report import Issue |
|
|
|
from mythril.analysis.report import Issue |
|
|
|
from mythril.laser.smt import UGT, symbol_factory |
|
|
|
from mythril.laser.smt import UGT, symbol_factory, Or, BitVec |
|
|
|
from mythril.laser.ethereum.state.global_state import GlobalState |
|
|
|
from mythril.laser.ethereum.state.global_state import GlobalState |
|
|
|
from mythril.exceptions import UnsatError |
|
|
|
from mythril.exceptions import UnsatError |
|
|
|
from copy import copy |
|
|
|
from copy import copy |
|
|
@ -71,6 +71,8 @@ def _analyze_state(state): |
|
|
|
) |
|
|
|
) |
|
|
|
|
|
|
|
|
|
|
|
except UnsatError: |
|
|
|
except UnsatError: |
|
|
|
|
|
|
|
if _is_precompile_call(state): |
|
|
|
|
|
|
|
return [] |
|
|
|
|
|
|
|
|
|
|
|
log.debug( |
|
|
|
log.debug( |
|
|
|
"[EXTERNAL_CALLS] Callee address cannot be modified. Reporting informational issue." |
|
|
|
"[EXTERNAL_CALLS] Callee address cannot be modified. Reporting informational issue." |
|
|
@ -104,6 +106,23 @@ def _analyze_state(state): |
|
|
|
return [issue] |
|
|
|
return [issue] |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
def _is_precompile_call(global_state: GlobalState): |
|
|
|
|
|
|
|
to = global_state.mstate.stack[-2] # type: BitVec |
|
|
|
|
|
|
|
constraints = copy(global_state.mstate.constraints) |
|
|
|
|
|
|
|
constraints += [ |
|
|
|
|
|
|
|
Or( |
|
|
|
|
|
|
|
to < symbol_factory.BitVecVal(1, 256), |
|
|
|
|
|
|
|
to > symbol_factory.BitVecVal(16, 256), |
|
|
|
|
|
|
|
) |
|
|
|
|
|
|
|
] |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
try: |
|
|
|
|
|
|
|
solver.get_model(constraints) |
|
|
|
|
|
|
|
return False |
|
|
|
|
|
|
|
except UnsatError: |
|
|
|
|
|
|
|
return True |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
class ExternalCalls(DetectionModule): |
|
|
|
class ExternalCalls(DetectionModule): |
|
|
|
"""This module searches for low level calls (e.g. call.value()) that |
|
|
|
"""This module searches for low level calls (e.g. call.value()) that |
|
|
|
forward all gas to the callee.""" |
|
|
|
forward all gas to the callee.""" |
|
|
|