mythril.analysis.module.modules package

Submodules

mythril.analysis.module.modules.arbitrary_jump module

This module contains the detection code for Arbitrary jumps.

class mythril.analysis.module.modules.arbitrary_jump.ArbitraryJump

Bases: DetectionModule

This module searches for JUMPs to a user-specified location.

description = '\n\nSearch for jumps to arbitrary locations in the bytecode\n'

entry_point: EntryPoint = 2

name = 'Caller can redirect execution to arbitrary bytecode locations'

pre_hooks: List[str] = ['JUMP', 'JUMPI']

reset_module()

Resets the module by clearing everything :return:

swc_id = '127'

mythril.analysis.module.modules.arbitrary_jump.is_unique_jumpdest(jump_dest: BitVec, state: GlobalState) → bool

Handles cases where jump_dest evaluates to a single concrete value

mythril.analysis.module.modules.arbitrary_write module

This module contains the detection code for arbitrary storage write.

class mythril.analysis.module.modules.arbitrary_write.ArbitraryStorage

Bases: DetectionModule

This module searches for a feasible write to an arbitrary storage slot.

description = '\n\nSearch for any writes to an arbitrary storage slot\n'

entry_point: EntryPoint = 2

name = 'Caller can write to arbitrary storage locations'

pre_hooks: List[str] = ['SSTORE']

reset_module()

Resets the module by clearing everything :return:

swc_id = '124'

mythril.analysis.module.modules.delegatecall module

This module contains the detection code for insecure delegate call usage.

class mythril.analysis.module.modules.delegatecall.ArbitraryDelegateCall

Bases: DetectionModule

This module detects delegatecall to a user-supplied address.

description = 'Check for invocations of delegatecall to a user-supplied address.'

entry_point: EntryPoint = 2

name = 'Delegatecall to a user-specified address'

pre_hooks: List[str] = ['DELEGATECALL']

swc_id = '112'

mythril.analysis.module.modules.dependence_on_origin module

This module contains the detection code for predictable variable dependence.

class mythril.analysis.module.modules.dependence_on_origin.TxOrigin

Bases: DetectionModule

This module detects whether control flow decisions are made based on the transaction origin.

description = 'Check whether control flow decisions are influenced by tx.origin'

entry_point: EntryPoint = 2

name = 'Control flow depends on tx.origin'

post_hooks: List[str] = ['ORIGIN']

pre_hooks: List[str] = ['JUMPI']

swc_id = '115'

class mythril.analysis.module.modules.dependence_on_origin.TxOriginAnnotation

Bases: object

Symbol annotation added to a variable that is initialized with a call to the ORIGIN instruction.

mythril.analysis.module.modules.dependence_on_predictable_vars module

This module contains the detection code for predictable variable dependence.

class mythril.analysis.module.modules.dependence_on_predictable_vars.OldBlockNumberUsedAnnotation

Bases: StateAnnotation

Symbol annotation used if a variable is initialized from a predictable environment variable.

class mythril.analysis.module.modules.dependence_on_predictable_vars.PredictableValueAnnotation(operation: str)

Bases: object

Symbol annotation used if a variable is initialized from a predictable environment variable.

class mythril.analysis.module.modules.dependence_on_predictable_vars.PredictableVariables

Bases: DetectionModule

This module detects whether control flow decisions are made using predictable parameters.

description = 'Check whether control flow decisions are influenced by block.coinbase,block.gaslimit, block.timestamp or block.number.'

entry_point: EntryPoint = 2

name = 'Control flow depends on a predictable environment variable'

post_hooks: List[str] = ['BLOCKHASH', 'COINBASE', 'GASLIMIT', 'TIMESTAMP', 'NUMBER']

pre_hooks: List[str] = ['JUMPI', 'BLOCKHASH']

swc_id = '116 120'

mythril.analysis.module.modules.ether_thief module

This module contains the detection code for unauthorized ether withdrawal.

class mythril.analysis.module.modules.ether_thief.EtherThief

Bases: DetectionModule

This module search for cases where Ether can be withdrawn to a user- specified address.

description = '\nSearch for cases where Ether can be withdrawn to a user-specified address.\nAn issue is reported if there is a valid end state where the attacker has successfully\nincreased their Ether balance.\n'

entry_point: EntryPoint = 2

name = 'Any sender can withdraw ETH from the contract account'

post_hooks: List[str] = ['CALL', 'STATICCALL']

reset_module()

Resets the module by clearing everything :return:

swc_id = '105'

mythril.analysis.module.modules.exceptions module

This module contains the detection code for reachable exceptions.

class mythril.analysis.module.modules.exceptions.Exceptions

Bases: DetectionModule

description = 'Checks whether any exception states are reachable.'

entry_point: EntryPoint = 2

name = 'Assertion violation'

pre_hooks: List[str] = ['INVALID', 'JUMP', 'REVERT']

swc_id = '110'

class mythril.analysis.module.modules.exceptions.LastJumpAnnotation(last_jump: int | None = None)

Bases: StateAnnotation

State Annotation used if an overflow is both possible and used in the annotated path

mythril.analysis.module.modules.exceptions.is_assertion_failure(global_state)

mythril.analysis.module.modules.external_calls module

This module contains the detection code for potentially insecure low-level calls.

class mythril.analysis.module.modules.external_calls.ExternalCalls

Bases: DetectionModule

This module searches for low level calls (e.g. call.value()) that forward all gas to the callee.

description = '\n\nSearch for external calls with unrestricted gas to a user-specified address.\n\n'

entry_point: EntryPoint = 2

name = 'External call to another contract'

pre_hooks: List[str] = ['CALL']

swc_id = '107'

mythril.analysis.module.modules.integer module

This module contains the detection code for integer overflows and underflows.

class mythril.analysis.module.modules.integer.IntegerArithmetics

Bases: DetectionModule

This module searches for integer over- and underflows.

description = "For every SUB instruction, check if there's a possible state where op1 > op0. For every ADD, MUL instruction, check if there's a possible state where op1 + op0 > 2^32 - 1"

entry_point: EntryPoint = 2

name = 'Integer overflow or underflow'

pre_hooks: List[str] = ['ADD', 'MUL', 'EXP', 'SUB', 'SSTORE', 'JUMPI', 'STOP', 'RETURN', 'CALL']

reset_module()

Resets the module :return:

swc_id = '101'

class mythril.analysis.module.modules.integer.OverUnderflowAnnotation(overflowing_state: GlobalState, operator: str, constraint: Bool)

Bases: object

Symbol Annotation used if a BitVector can overflow

class mythril.analysis.module.modules.integer.OverUnderflowStateAnnotation

Bases: StateAnnotation

State Annotation used if an overflow is both possible and used in the annotated path

mythril.analysis.module.modules.multiple_sends module

This module contains the detection code to find multiple sends occurring in a single transaction.

class mythril.analysis.module.modules.multiple_sends.MultipleSends

Bases: DetectionModule

This module checks for multiple sends in a single transaction.

description = 'Check for multiple sends in a single transaction'

entry_point: EntryPoint = 2

name = 'Multiple external calls in the same transaction'

pre_hooks: List[str] = ['CALL', 'DELEGATECALL', 'STATICCALL', 'CALLCODE', 'RETURN', 'STOP']

swc_id = '113'

class mythril.analysis.module.modules.multiple_sends.MultipleSendsAnnotation

Bases: StateAnnotation

mythril.analysis.module.modules.state_change_external_calls module

class mythril.analysis.module.modules.state_change_external_calls.StateChangeAfterCall

Bases: DetectionModule

This module searches for state change after low level calls (e.g. call.value()) that forward gas to the callee.

description = '\n\nCheck whether the account state is accesses after the execution of an external call\n'

entry_point: EntryPoint = 2

name = 'State change after an external call'

pre_hooks: List[str] = ['CALL', 'DELEGATECALL', 'CALLCODE', 'SSTORE', 'SLOAD', 'CREATE', 'CREATE2']

swc_id = '107'

class mythril.analysis.module.modules.state_change_external_calls.StateChangeCallsAnnotation(call_state: GlobalState, user_defined_address: bool)

Bases: StateAnnotation

get_issue(global_state: GlobalState, detector: DetectionModule) → PotentialIssue | None

mythril.analysis.module.modules.suicide module

class mythril.analysis.module.modules.suicide.AccidentallyKillable

Bases: DetectionModule

This module checks if the contact can be ‘accidentally’ killed by anyone.

description = "\nCheck if the contact can be 'accidentally' killed by anyone.\nFor kill-able contracts, also check whether it is possible to direct the contract balance to the attacker.\n"

entry_point: EntryPoint = 2

name = 'Contract can be accidentally killed by anyone'

pre_hooks: List[str] = ['SELFDESTRUCT']

reset_module()

Resets the module :return:

swc_id = '106'

mythril.analysis.module.modules.unchecked_retval module

This module contains detection code to find occurrences of calls whose return value remains unchecked.

class mythril.analysis.module.modules.unchecked_retval.RetVal

Bases: TypedDict

address: int

retval: BitVec

class mythril.analysis.module.modules.unchecked_retval.UncheckedRetval

Bases: DetectionModule

A detection module to test whether CALL return value is checked.

description = 'Test whether CALL return value is checked. For direct calls, the Solidity compiler auto-generates this check. E.g.:\n    Alice c = Alice(address);\n    c.ping(42);\nHere the CALL will be followed by IZSERO(retval), if retval = ZERO then state is reverted. For low-level-calls this check is omitted. E.g.:\n    c.call.value(0)(bytes4(sha3("ping(uint256)")),1);'

entry_point: EntryPoint = 2

name = 'Return value of an external call is not checked'

post_hooks: List[str] = ['CALL', 'DELEGATECALL', 'STATICCALL', 'CALLCODE']

pre_hooks: List[str] = ['STOP', 'RETURN']

swc_id = '104'

class mythril.analysis.module.modules.unchecked_retval.UncheckedRetvalAnnotation

Bases: StateAnnotation

mythril.analysis.module.modules.user_assertions module

This module contains the detection code for potentially insecure low-level calls.

class mythril.analysis.module.modules.user_assertions.UserAssertions

Bases: DetectionModule

This module searches for user supplied exceptions: emit AssertionFailed(“Error”).

description = "\n\nSearch for reachable user-supplied exceptions.\nReport a warning if an log message is emitted: 'emit AssertionFailed(string)'\n\n"

entry_point: EntryPoint = 2

name = 'A user-defined assertion has been triggered'

pre_hooks: List[str] = ['LOG1', 'MSTORE']

swc_id = '110'

Module contents