diff --git a/mythril/analysis/modules/external_calls.py b/mythril/analysis/modules/external_calls.py index 554cbb93..e24470a6 100644 --- a/mythril/analysis/modules/external_calls.py +++ b/mythril/analysis/modules/external_calls.py @@ -5,7 +5,7 @@ from mythril.analysis import solver from mythril.analysis.swc_data import REENTRANCY from mythril.analysis.modules.base import DetectionModule 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.exceptions import UnsatError from copy import copy @@ -71,6 +71,8 @@ def _analyze_state(state): ) except UnsatError: + if _is_precompile_call(state): + return [] log.debug( "[EXTERNAL_CALLS] Callee address cannot be modified. Reporting informational issue." @@ -104,6 +106,23 @@ def _analyze_state(state): 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): """This module searches for low level calls (e.g. call.value()) that forward all gas to the callee."""