mythril.laser.ethereum package

Subpackages

• mythril.laser.ethereum.function_managers package
  • Submodules
  • mythril.laser.ethereum.function_managers.exponent_function_manager module
  • mythril.laser.ethereum.function_managers.keccak_function_manager module
  • Module contents
• mythril.laser.ethereum.state package
  • Submodules
  • mythril.laser.ethereum.state.account module
  • mythril.laser.ethereum.state.annotation module
  • mythril.laser.ethereum.state.calldata module
  • mythril.laser.ethereum.state.constraints module
  • mythril.laser.ethereum.state.environment module
  • mythril.laser.ethereum.state.global_state module
  • mythril.laser.ethereum.state.machine_state module
  • mythril.laser.ethereum.state.memory module
  • mythril.laser.ethereum.state.return_data module
  • mythril.laser.ethereum.state.world_state module
  • Module contents
• mythril.laser.ethereum.strategy package
  • Subpackages
    • mythril.laser.ethereum.strategy.extensions package
      • Submodules
      • mythril.laser.ethereum.strategy.extensions.bounded_loops module
      • Module contents
  • Submodules
  • mythril.laser.ethereum.strategy.basic module
  • mythril.laser.ethereum.strategy.beam module
  • mythril.laser.ethereum.strategy.concolic module
  • Module contents
• mythril.laser.ethereum.transaction package
  • Submodules
  • mythril.laser.ethereum.transaction.concolic module
  • mythril.laser.ethereum.transaction.symbolic module
  • mythril.laser.ethereum.transaction.transaction_models module
  • Module contents

Submodules

mythril.laser.ethereum.call module

This module contains the business logic used by Instruction in instructions.py to get the necessary elements from the stack and determine the parameters for the new global state.

mythril.laser.ethereum.call.get_call_data(global_state: mythril.laser.ethereum.state.global_state.GlobalState, memory_start: Union[int, mythril.laser.smt.bitvec.BitVec], memory_size: Union[int, mythril.laser.smt.bitvec.BitVec])

Gets call_data from the global_state.

Parameters:

• global_state – state to look in
• memory_start – Start index
• memory_size – Size

Returns:

Tuple containing: call_data array from memory or empty array if symbolic, type found

mythril.laser.ethereum.call.get_call_parameters(global_state: mythril.laser.ethereum.state.global_state.GlobalState, dynamic_loader: mythril.support.loader.DynLoader, with_value=False)

Gets call parameters from global state Pops the values from the stack and determines output parameters.

Parameters:

• global_state – state to look in
• dynamic_loader – dynamic loader to use
• with_value – whether to pop the value argument from the stack

Returns:

callee_account, call_data, value, call_data_type, gas

mythril.laser.ethereum.call.get_callee_account(global_state: mythril.laser.ethereum.state.global_state.GlobalState, callee_address: Union[str, mythril.laser.smt.bitvec.BitVec], dynamic_loader: mythril.support.loader.DynLoader)

Gets the callees account from the global_state.

Parameters:

• global_state – state to look in
• callee_address – address of the callee
• dynamic_loader – dynamic loader to use

Returns:

Account belonging to callee

mythril.laser.ethereum.call.get_callee_address(global_state: mythril.laser.ethereum.state.global_state.GlobalState, dynamic_loader: mythril.support.loader.DynLoader, symbolic_to_address: mythril.laser.smt.expression.Expression)

Gets the address of the callee.

Parameters:

• global_state – state to look in
• dynamic_loader – dynamic loader to use
• symbolic_to_address – The (symbolic) callee address

Returns:

Address of the callee

mythril.laser.ethereum.call.insert_ret_val(global_state: mythril.laser.ethereum.state.global_state.GlobalState)

mythril.laser.ethereum.call.native_call(global_state: mythril.laser.ethereum.state.global_state.GlobalState, callee_address: Union[str, mythril.laser.smt.bitvec.BitVec], call_data: mythril.laser.ethereum.state.calldata.BaseCalldata, memory_out_offset: Union[int, mythril.laser.smt.expression.Expression], memory_out_size: Union[int, mythril.laser.smt.expression.Expression]) → Optional[List[mythril.laser.ethereum.state.global_state.GlobalState]]

mythril.laser.ethereum.cfg module

This module.

class mythril.laser.ethereum.cfg.Edge(node_from: int, node_to: int, edge_type=<JumpType.UNCONDITIONAL: 2>, condition=None)

Bases: object

The respresentation of a call graph edge.

as_dict

Returns:

class mythril.laser.ethereum.cfg.JumpType

Bases: enum.Enum

An enum to represent the types of possible JUMP scenarios.

CALL = 3

CONDITIONAL = 1

RETURN = 4

Transaction = 5

UNCONDITIONAL = 2

class mythril.laser.ethereum.cfg.Node(contract_name: str, start_addr=0, constraints=None, function_name='unknown')

Bases: object

The representation of a call graph node.

get_cfg_dict() → Dict[KT, VT]

Returns:

class mythril.laser.ethereum.cfg.NodeFlags

Bases: flags.Flags

A collection of flags to denote the type a call graph node can have.

mythril.laser.ethereum.evm_exceptions module

This module contains EVM exception types used by LASER.

exception mythril.laser.ethereum.evm_exceptions.InvalidInstruction

Bases: mythril.laser.ethereum.evm_exceptions.VmException

A VM exception denoting an invalid op code has been encountered.

exception mythril.laser.ethereum.evm_exceptions.InvalidJumpDestination

Bases: mythril.laser.ethereum.evm_exceptions.VmException

A VM exception regarding JUMPs to invalid destinations.

exception mythril.laser.ethereum.evm_exceptions.OutOfGasException

Bases: mythril.laser.ethereum.evm_exceptions.VmException

A VM exception denoting the current execution has run out of gas.

exception mythril.laser.ethereum.evm_exceptions.StackOverflowException

Bases: mythril.laser.ethereum.evm_exceptions.VmException

A VM exception regarding stack overflows.

exception mythril.laser.ethereum.evm_exceptions.StackUnderflowException

Bases: IndexError, mythril.laser.ethereum.evm_exceptions.VmException

A VM exception regarding stack underflows.

exception mythril.laser.ethereum.evm_exceptions.VmException

Bases: Exception

The base VM exception type.

exception mythril.laser.ethereum.evm_exceptions.WriteProtection

Bases: mythril.laser.ethereum.evm_exceptions.VmException

A VM exception denoting that a write operation is executed on a write protected environment

mythril.laser.ethereum.instruction_data module

mythril.laser.ethereum.instruction_data.calculate_native_gas(size: int, contract: str)

Parameters:

• size –
• contract –

Returns:

mythril.laser.ethereum.instruction_data.calculate_sha3_gas(length: int)

Parameters:length – Returns:

mythril.laser.ethereum.instruction_data.ceil32(value: int, *, ceiling: int = 32) → int

mythril.laser.ethereum.instruction_data.get_opcode_gas(opcode: str) → Tuple[int, int]

mythril.laser.ethereum.instruction_data.get_required_stack_elements(opcode: str) → int

mythril.laser.ethereum.instructions module

This module contains a representation class for EVM instructions and transitions between them.

class mythril.laser.ethereum.instructions.Instruction(op_code: str, dynamic_loader: mythril.support.loader.DynLoader, pre_hooks: List[Callable] = None, post_hooks: List[Callable] = None)

Bases: object

Instruction class is used to mutate a state according to the current instruction.

add_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

addmod_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

address_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

and_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

assert_fail_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

balance_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

basefee_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

beginsub_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

blockhash_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

byte_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

call_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

call_post(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

callcode_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

callcode_post(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

calldatacopy_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

calldataload_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

calldatasize_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

caller_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

callvalue_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

chainid_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

codecopy_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

codesize_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

coinbase_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

create2_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

create2_post(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

create_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

create_post(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

delegatecall_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

delegatecall_post(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

difficulty_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

div_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

dup_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

eq_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

evaluate(global_state: mythril.laser.ethereum.state.global_state.GlobalState, post=False) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Performs the mutation for this instruction.

Parameters:

• global_state –
• post –

Returns:

exp_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

extcodecopy_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

extcodehash_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

extcodesize_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

gas_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

gaslimit_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

gasprice_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

gt_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

invalid_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

iszero_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

jump_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

jumpdest_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

jumpi_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

jumpsub_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

log_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

lt_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

mload_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

mod_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

msize_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

mstore8_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

mstore_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

mul_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

mulmod_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

not_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

number_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

or_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

origin_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

pc_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

pop_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

post_handler(global_state, function_name: str)

push_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

return_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

returndatacopy_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

returndatasize_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

returnsub_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

revert_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

sar_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

sdiv_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

selfbalance_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

selfdestruct_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

sgt_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

sha3_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

shl_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

shr_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

signextend_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

sload_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

slt_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

smod_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

sstore_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

staticcall_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

staticcall_post(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

stop_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

sub_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

swap_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

timestamp_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

xor_(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:

• func_obj –
• global_state –

Returns:

class mythril.laser.ethereum.instructions.StateTransition(increment_pc=True, enable_gas=True, is_state_mutation_instruction=False)

Bases: object

Decorator that handles global state copy and original return.

This decorator calls the decorated instruction mutator function on a copy of the state that is passed to it. After the call, the resulting new states’ program counter is automatically incremented if increment_pc=True.

accumulate_gas(global_state: mythril.laser.ethereum.state.global_state.GlobalState)

Parameters:global_state – Returns:

static call_on_state_copy(func: Callable, func_obj: mythril.laser.ethereum.instructions.Instruction, state: mythril.laser.ethereum.state.global_state.GlobalState)

Parameters:

• func –
• func_obj –
• state –

Returns:

static check_gas_usage_limit(global_state: mythril.laser.ethereum.state.global_state.GlobalState)

Parameters:global_state – Returns:

increment_states_pc(states: List[mythril.laser.ethereum.state.global_state.GlobalState]) → List[mythril.laser.ethereum.state.global_state.GlobalState]

Parameters:states – Returns:

mythril.laser.ethereum.instructions.transfer_ether(global_state: mythril.laser.ethereum.state.global_state.GlobalState, sender: mythril.laser.smt.bitvec.BitVec, receiver: mythril.laser.smt.bitvec.BitVec, value: Union[int, mythril.laser.smt.bitvec.BitVec])

Perform an Ether transfer between two accounts

Parameters:

• global_state – The global state in which the Ether transfer occurs
• sender – The sender of the Ether
• receiver – The recipient of the Ether
• value – The amount of Ether to send

Returns:

mythril.laser.ethereum.natives module

This nodule defines helper functions to deal with native calls.

exception mythril.laser.ethereum.natives.NativeContractException

Bases: Exception

An exception denoting an error during a native call.

mythril.laser.ethereum.natives.blake2b_fcompress(data: List[int]) → List[int]

blake2b hashing :param data: :return:

mythril.laser.ethereum.natives.ec_add(data: List[int]) → List[int]

mythril.laser.ethereum.natives.ec_mul(data: List[int]) → List[int]

mythril.laser.ethereum.natives.ec_pair(data: List[int]) → List[int]

mythril.laser.ethereum.natives.ecrecover(data: List[int]) → List[int]

Parameters:data – Returns:

mythril.laser.ethereum.natives.ecrecover_to_pub(rawhash, v, r, s)

mythril.laser.ethereum.natives.encode_int32(v)

mythril.laser.ethereum.natives.identity(data: List[int]) → List[int]

Parameters:data – Returns:

mythril.laser.ethereum.natives.int_to_32bytearray(i)

mythril.laser.ethereum.natives.mod_exp(data: List[int]) → List[int]

TODO: Some symbolic parts can be handled here Modular Exponentiation :param data: Data with <length_of_BASE> <length_of_EXPONENT> <length_of_MODULUS> <BASE> <EXPONENT> <MODULUS> :return: modular exponentiation

mythril.laser.ethereum.natives.native_contracts(address: int, data: mythril.laser.ethereum.state.calldata.BaseCalldata) → List[int]

Takes integer address 1, 2, 3, 4.

Parameters:

• address –
• data –

Returns:

mythril.laser.ethereum.natives.ripemd160(data: List[int]) → List[int]

Parameters:data – Returns:

mythril.laser.ethereum.natives.safe_ord(value)

mythril.laser.ethereum.natives.sha256(data: List[int]) → List[int]

Parameters:data – Returns:

mythril.laser.ethereum.svm module

This module implements the main symbolic execution engine.

class mythril.laser.ethereum.svm.LaserEVM(dynamic_loader=None, max_depth=inf, execution_timeout=60, create_timeout=10, strategy=<class 'mythril.laser.ethereum.strategy.basic.DepthFirstSearchStrategy'>, transaction_count=2, requires_statespace=True, iprof=None, use_reachability_check=True, beam_width=None)

Bases: object

The LASER EVM.

Just as Mithril had to be mined at great efforts to provide the Dwarves with their exceptional armour, LASER stands at the heart of Mythril, digging deep in the depths of call graphs, unearthing the most precious symbolic call data, that is then hand-forged into beautiful and strong security issues by the experienced smiths we call detection modules. It is truly a magnificent symbiosis.

exec(create=False, track_gas=False) → Optional[List[mythril.laser.ethereum.state.global_state.GlobalState]]

Parameters:

• create –
• track_gas –

Returns:

execute_state(global_state: mythril.laser.ethereum.state.global_state.GlobalState) → Tuple[List[mythril.laser.ethereum.state.global_state.GlobalState], Optional[str]]

Execute a single instruction in global_state.

Parameters:global_state – Returns:A list of successor states.

extend_strategy(extension: abc.ABCMeta, **kwargs) → None

handle_vm_exception(global_state: mythril.laser.ethereum.state.global_state.GlobalState, op_code: str, error_msg: str) → List[mythril.laser.ethereum.state.global_state.GlobalState]

instr_hook(hook_type, opcode) → Callable

Registers the annoted function with register_instr_hooks

Parameters:

• hook_type – Type of hook pre/post
• opcode – The opcode related to the function

laser_hook(hook_type: str) → Callable

Registers the annotated function with register_laser_hooks

Parameters:hook_type – Returns:hook decorator

manage_cfg(opcode: str, new_states: List[mythril.laser.ethereum.state.global_state.GlobalState]) → None

Parameters:

• opcode –
• new_states –

post_hook(op_code: str) → Callable

Parameters:op_code – Returns:

pre_hook(op_code: str) → Callable

Parameters:op_code – Returns:

register_hooks(hook_type: str, hook_dict: Dict[str, List[Callable]])

Parameters:

• hook_type –
• hook_dict –

register_instr_hooks(hook_type: str, opcode: str, hook: Callable)

Registers instructions hooks from plugins

register_laser_hooks(hook_type: str, hook: Callable)

registers the hook with this Laser VM

sym_exec(world_state: mythril.laser.ethereum.state.world_state.WorldState = None, target_address: int = None, creation_code: str = None, contract_name: str = None) → None

Starts symbolic execution There are two modes of execution. Either we analyze a preconfigured configuration, in which case the world_state and target_address variables must be supplied. Or we execute the creation code of a contract, in which case the creation code and desired name of that contract should be provided.

:param world_state The world state configuration from which to perform analysis :param target_address The address of the contract account in the world state which analysis should target :param creation_code The creation code to create the target contract in the symbolic environment :param contract_name The name that the created account should be associated with

exception mythril.laser.ethereum.svm.SVMError

Bases: Exception

An exception denoting an unexpected state in symbolic execution.

mythril.laser.ethereum.time_handler module

class mythril.laser.ethereum.time_handler.TimeHandler

Bases: object

start_execution(execution_time)

time_remaining()

mythril.laser.ethereum.util module

This module contains various utility conversion functions and constants for LASER.

mythril.laser.ethereum.util.bytearray_to_int(arr)

Parameters:arr – Returns:

mythril.laser.ethereum.util.concrete_int_from_bytes(concrete_bytes: Union[List[Union[mythril.laser.smt.bitvec.BitVec, int]], bytes], start_index: int) → int

Parameters:

• concrete_bytes –
• start_index –

Returns:

mythril.laser.ethereum.util.concrete_int_to_bytes(val)

Parameters:val – Returns:

mythril.laser.ethereum.util.extract32(data: bytearray, i: int) → int

Parameters:

• data –
• i –

Returns:

mythril.laser.ethereum.util.extract_copy(data: bytearray, mem: bytearray, memstart: int, datastart: int, size: int)

mythril.laser.ethereum.util.get_concrete_int(item: Union[int, mythril.laser.smt.expression.Expression]) → int

Parameters:item – Returns:

mythril.laser.ethereum.util.get_instruction_index(instruction_list: List[Dict[KT, VT]], address: int) → Optional[int]

Parameters:

• instruction_list –
• address –

Returns:

mythril.laser.ethereum.util.get_trace_line(instr: Dict[KT, VT], state: MachineState) → str

Parameters:

• instr –
• state –

Returns:

mythril.laser.ethereum.util.pop_bitvec(state: MachineState) → mythril.laser.smt.bitvec.BitVec

Parameters:state – Returns:

mythril.laser.ethereum.util.safe_decode(hex_encoded_string: str) → bytes

Parameters:hex_encoded_string – Returns:

mythril.laser.ethereum.util.to_signed(i: int) → int

Parameters:i – Returns:

Module contents