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
[source]¶ Bases:
mythril.analysis.module.base.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
= 2¶
-
name
= 'Caller can redirect execution to arbitrary bytecode locations'¶
-
pre_hooks
= ['JUMP', 'JUMPI']¶
-
swc_id
= '127'¶
-
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
[source]¶ Bases:
mythril.analysis.module.base.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
= 2¶
-
name
= 'Caller can write to arbitrary storage locations'¶
-
pre_hooks
= ['SSTORE']¶
-
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
[source]¶ Bases:
mythril.analysis.module.base.DetectionModule
This module detects delegatecall to a user-supplied address.
-
description
= 'Check for invocations of delegatecall to a user-supplied address.'¶
-
entry_point
= 2¶
-
name
= 'Delegatecall to a user-specified address'¶
-
pre_hooks
= ['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
[source]¶ Bases:
mythril.analysis.module.base.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
= 2¶
-
name
= 'Control flow depends on tx.origin'¶
-
post_hooks
= ['ORIGIN']¶
-
pre_hooks
= ['JUMPI']¶
-
swc_id
= '115'¶
-
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
[source]¶ Bases:
mythril.laser.ethereum.state.annotation.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)[source]¶ 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
[source]¶ Bases:
mythril.analysis.module.base.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
= 2¶
-
name
= 'Control flow depends on a predictable environment variable'¶
-
post_hooks
= ['BLOCKHASH', 'COINBASE', 'GASLIMIT', 'TIMESTAMP', 'NUMBER']¶
-
pre_hooks
= ['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
[source]¶ Bases:
mythril.analysis.module.base.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
= 2¶
-
name
= 'Any sender can withdraw ETH from the contract account'¶
-
post_hooks
= ['CALL', 'STATICCALL']¶
-
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
[source]¶ Bases:
mythril.analysis.module.base.DetectionModule
-
description
= 'Checks whether any exception states are reachable.'¶
-
entry_point
= 2¶
-
name
= 'Assertion violation'¶
-
pre_hooks
= ['INVALID', 'JUMP', 'REVERT']¶
-
swc_id
= '110'¶
-
-
class
mythril.analysis.module.modules.exceptions.
LastJumpAnnotation
(last_jump: Optional[int] = None)[source]¶ Bases:
mythril.laser.ethereum.state.annotation.StateAnnotation
State Annotation used if an overflow is both possible and used in the annotated path
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
[source]¶ Bases:
mythril.analysis.module.base.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
= 2¶
-
name
= 'External call to another contract'¶
-
pre_hooks
= ['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
[source]¶ Bases:
mythril.analysis.module.base.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
= 2¶
-
name
= 'Integer overflow or underflow'¶
-
pre_hooks
= ['ADD', 'MUL', 'EXP', 'SUB', 'SSTORE', 'JUMPI', 'STOP', 'RETURN', 'CALL']¶
-
swc_id
= '101'¶
-
-
class
mythril.analysis.module.modules.integer.
OverUnderflowAnnotation
(overflowing_state: mythril.laser.ethereum.state.global_state.GlobalState, operator: str, constraint: mythril.laser.smt.bool.Bool)[source]¶ Bases:
object
Symbol Annotation used if a BitVector can overflow
-
class
mythril.analysis.module.modules.integer.
OverUnderflowStateAnnotation
[source]¶ Bases:
mythril.laser.ethereum.state.annotation.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
[source]¶ Bases:
mythril.analysis.module.base.DetectionModule
This module checks for multiple sends in a single transaction.
-
description
= 'Check for multiple sends in a single transaction'¶
-
entry_point
= 2¶
-
name
= 'Multiple external calls in the same transaction'¶
-
pre_hooks
= ['CALL', 'DELEGATECALL', 'STATICCALL', 'CALLCODE', 'RETURN', 'STOP']¶
-
swc_id
= '113'¶
-
-
class
mythril.analysis.module.modules.multiple_sends.
MultipleSendsAnnotation
[source]¶ Bases:
mythril.laser.ethereum.state.annotation.StateAnnotation
mythril.analysis.module.modules.state_change_external_calls module¶
-
class
mythril.analysis.module.modules.state_change_external_calls.
StateChangeAfterCall
[source]¶ Bases:
mythril.analysis.module.base.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
= 2¶
-
name
= 'State change after an external call'¶
-
pre_hooks
= ['CALL', 'DELEGATECALL', 'CALLCODE', 'SSTORE', 'SLOAD', 'CREATE', 'CREATE2']¶
-
swc_id
= '107'¶
-
-
class
mythril.analysis.module.modules.state_change_external_calls.
StateChangeCallsAnnotation
(call_state: mythril.laser.ethereum.state.global_state.GlobalState, user_defined_address: bool)[source]¶ Bases:
mythril.laser.ethereum.state.annotation.StateAnnotation
mythril.analysis.module.modules.suicide module¶
-
class
mythril.analysis.module.modules.suicide.
AccidentallyKillable
[source]¶ Bases:
mythril.analysis.module.base.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
= 2¶
-
name
= 'Contract can be accidentally killed by anyone'¶
-
pre_hooks
= ['SELFDESTRUCT']¶
-
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.
UncheckedRetval
[source]¶ Bases:
mythril.analysis.module.base.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
= 2¶
-
name
= 'Return value of an external call is not checked'¶
-
post_hooks
= ['CALL', 'DELEGATECALL', 'STATICCALL', 'CALLCODE']¶
-
pre_hooks
= ['STOP', 'RETURN']¶
-
swc_id
= '104'¶
-
-
class
mythril.analysis.module.modules.unchecked_retval.
UncheckedRetvalAnnotation
[source]¶ Bases:
mythril.laser.ethereum.state.annotation.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
[source]¶ Bases:
mythril.analysis.module.base.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
= 2¶
-
name
= 'A user-defined assertion has been triggered'¶
-
pre_hooks
= ['LOG1', 'MSTORE']¶
-
swc_id
= '110'¶
-