mythril.laser.ethereum package

Subpackages

• mythril.laser.ethereum.function_managers package
  • Submodules
  • mythril.laser.ethereum.function_managers.exponent_function_manager module
    • ExponentFunctionManager
      • ExponentFunctionManager.create_condition()
  • mythril.laser.ethereum.function_managers.keccak_function_manager module
    • KeccakFunctionManager
      • KeccakFunctionManager.create_conditions()
      • KeccakFunctionManager.create_keccak()
      • KeccakFunctionManager.find_concrete_keccak()
      • KeccakFunctionManager.get_concrete_hash_data()
      • KeccakFunctionManager.get_empty_keccak_hash()
      • KeccakFunctionManager.get_function()
      • KeccakFunctionManager.hash_matcher
      • KeccakFunctionManager.reset()
      • KeccakFunctionManager.set_data()
  • Module contents
• mythril.laser.ethereum.state package
  • Submodules
  • mythril.laser.ethereum.state.account module
    • Account
      • Account.add_balance()
      • Account.as_dict
      • Account.serialised_code()
      • Account.set_balance()
      • Account.set_storage()
    • Storage
  • mythril.laser.ethereum.state.annotation module
    • MergeableStateAnnotation
      • MergeableStateAnnotation.check_merge_annotation()
      • MergeableStateAnnotation.merge_annotation()
    • NoCopyAnnotation
    • StateAnnotation
      • StateAnnotation.persist_over_calls
      • StateAnnotation.persist_to_world_state
      • StateAnnotation.search_importance
  • mythril.laser.ethereum.state.calldata module
    • BaseCalldata
      • BaseCalldata.calldatasize
      • BaseCalldata.concrete()
      • BaseCalldata.get_word_at()
      • BaseCalldata.size
    • BasicConcreteCalldata
      • BasicConcreteCalldata.concrete()
      • BasicConcreteCalldata.size
    • BasicSymbolicCalldata
      • BasicSymbolicCalldata.concrete()
      • BasicSymbolicCalldata.size
    • ConcreteCalldata
      • ConcreteCalldata.concrete()
      • ConcreteCalldata.size
    • SymbolicCalldata
      • SymbolicCalldata.concrete()
      • SymbolicCalldata.size
  • mythril.laser.ethereum.state.constraints module
    • Constraints
      • Constraints.append()
      • Constraints.as_list
      • Constraints.copy()
      • Constraints.get_all_constraints()
      • Constraints.get_model()
      • Constraints.is_possible()
  • mythril.laser.ethereum.state.environment module
    • Environment
      • Environment.as_dict
  • mythril.laser.ethereum.state.global_state module
    • GlobalState
      • GlobalState.accounts
      • GlobalState.add_annotations()
      • GlobalState.annotate()
      • GlobalState.annotations
      • GlobalState.current_transaction
      • GlobalState.get_annotations()
      • GlobalState.get_current_instruction()
      • GlobalState.instruction
      • GlobalState.new_bitvec()
  • mythril.laser.ethereum.state.machine_state module
    • MachineStack
      • MachineStack.STACK_LIMIT
      • MachineStack.append()
      • MachineStack.pop()
    • MachineState
      • MachineState.as_dict
      • MachineState.calculate_extension_size()
      • MachineState.calculate_memory_gas()
      • MachineState.check_gas()
      • MachineState.mem_extend()
      • MachineState.memory_size
      • MachineState.memory_write()
      • MachineState.pop()
  • mythril.laser.ethereum.state.memory module
    • Memory
      • Memory.extend()
      • Memory.get_word_at()
      • Memory.write_word_at()
    • convert_bv()
  • mythril.laser.ethereum.state.return_data module
    • ReturnData
      • ReturnData.size
  • mythril.laser.ethereum.state.world_state module
    • WorldState
      • WorldState.accounts
      • WorldState.accounts_exist_or_load()
      • WorldState.annotate()
      • WorldState.annotations
      • WorldState.create_account()
      • WorldState.create_initialized_contract_account()
      • WorldState.get_annotations()
      • WorldState.put_account()
  • 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
    • BreadthFirstSearchStrategy
      • BreadthFirstSearchStrategy.get_strategic_global_state()
      • BreadthFirstSearchStrategy.view_strategic_global_state()
    • DepthFirstSearchStrategy
      • DepthFirstSearchStrategy.get_strategic_global_state()
      • DepthFirstSearchStrategy.view_strategic_global_state()
    • ReturnRandomNaivelyStrategy
      • ReturnRandomNaivelyStrategy.get_strategic_global_state()
      • ReturnRandomNaivelyStrategy.view_strategic_global_state()
    • ReturnWeightedRandomStrategy
      • ReturnWeightedRandomStrategy.get_strategic_global_state()
      • ReturnWeightedRandomStrategy.view_strategic_global_state()
  • mythril.laser.ethereum.strategy.beam module
    • BeamSearch
      • BeamSearch.beam_priority()
      • BeamSearch.get_strategic_global_state()
      • BeamSearch.sort_and_eliminate_states()
      • BeamSearch.view_strategic_global_state()
  • mythril.laser.ethereum.strategy.concolic module
    • ConcolicStrategy
      • ConcolicStrategy.check_completion_criterion()
      • ConcolicStrategy.get_strategic_global_state()
    • TraceAnnotation
      • TraceAnnotation.persist_over_calls
  • Module contents
    • BasicSearchStrategy
      • BasicSearchStrategy.get_strategic_global_state()
      • BasicSearchStrategy.run_check()
    • CriterionSearchStrategy
      • CriterionSearchStrategy.get_strategic_global_state()
      • CriterionSearchStrategy.set_criterion_satisfied()
• mythril.laser.ethereum.transaction package
  • Submodules
  • mythril.laser.ethereum.transaction.concolic module
    • execute_contract_creation()
    • execute_message_call()
    • execute_transaction()
  • mythril.laser.ethereum.transaction.symbolic module
    • Actors
      • Actors.attacker
      • Actors.creator
    • execute_contract_creation()
    • execute_message_call()
    • execute_message_call_preprocessing()
    • execute_transaction()
    • generate_function_constraints()
  • mythril.laser.ethereum.transaction.transaction_models module
    • BaseTransaction
      • BaseTransaction.initial_global_state()
      • BaseTransaction.initial_global_state_from_environment()
    • ContractCreationTransaction
      • ContractCreationTransaction.end()
      • ContractCreationTransaction.initial_global_state()
    • MessageCallTransaction
      • MessageCallTransaction.end()
      • MessageCallTransaction.initial_global_state()
    • TransactionEndSignal
    • TransactionStartSignal
    • TxIdManager
      • TxIdManager.get_next_tx_id()
      • TxIdManager.restart_counter()
      • TxIdManager.set_counter()
  • 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: GlobalState, memory_start: int | BitVec, memory_size: int | 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: GlobalState, dynamic_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: GlobalState, callee_address: str | BitVec, dynamic_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: GlobalState, dynamic_loader: DynLoader, symbolic_to_address: 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.native_call(global_state: GlobalState, callee_address: str | BitVec, call_data: BaseCalldata, memory_out_offset: int | Expression, memory_out_size: int | Expression) → List[GlobalState] | None

mythril.laser.ethereum.cfg module

This module.

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

Bases: object

The respresentation of a call graph edge.

property as_dict: Dict[str, int]

Returns:

class mythril.laser.ethereum.cfg.JumpType(value)

Bases: 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

Returns:

class mythril.laser.ethereum.cfg.NodeFlags(*args, **kwargs)

Bases: 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: VmException

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

exception mythril.laser.ethereum.evm_exceptions.InvalidJumpDestination

Bases: VmException

A VM exception regarding JUMPs to invalid destinations.

exception mythril.laser.ethereum.evm_exceptions.OutOfGasException

Bases: VmException

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

exception mythril.laser.ethereum.evm_exceptions.StackOverflowException

Bases: VmException

A VM exception regarding stack overflows.

exception mythril.laser.ethereum.evm_exceptions.StackUnderflowException

Bases: IndexError, 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: 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.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: DynLoader, pre_hooks: List[Callable] | None = None, post_hooks: List[Callable] | None = None)

Bases: object

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

add_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

addmod_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

address_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

and_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

assert_fail_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

balance_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

basefee_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

beginsub_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

blockhash_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

byte_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

call_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

call_post(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

callcode_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

callcode_post(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

calldatacopy_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

calldataload_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

calldatasize_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

caller_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

callvalue_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

chainid_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

codecopy_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

codesize_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

coinbase_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

create2_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

create2_post(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

create_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

create_post(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

delegatecall_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

delegatecall_post(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

difficulty_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

div_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

dup_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

empty_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

eq_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

evaluate(global_state: GlobalState, post=False) → List[GlobalState]

Performs the mutation for this instruction.

Parameters:

• global_state

• post

Returns:

exp_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

extcodecopy_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

extcodehash_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

extcodesize_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

gas_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

gaslimit_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

gasprice_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

gt_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

invalid_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

iszero_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

jump_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

jumpdest_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

jumpi_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

jumpsub_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

log_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

lt_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

mload_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

mod_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

msize_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

mstore8_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

mstore_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

mul_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

mulmod_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

not_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

number_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

or_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

origin_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

pc_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

pop_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

post_handler(global_state, function_name: str)

push_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

return_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

returndatacopy_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

returndatasize_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

returnsub_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

revert_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

sar_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

sdiv_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

selfbalance_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

selfdestruct_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

sgt_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

sha3_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

shl_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

shr_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

signextend_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

sload_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

slt_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

smod_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

sstore_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

staticcall_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

staticcall_post(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

stop_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

sub_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

swap_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

timestamp_(global_state: GlobalState) → List[GlobalState]

Parameters:

• func_obj

• global_state

Returns:

xor_(global_state: GlobalState) → List[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: GlobalState)

Parameters:

global_state

Returns:

static call_on_state_copy(func: Callable, func_obj: Instruction, state: GlobalState)

Parameters:

• func

• func_obj

• state

Returns:

static check_gas_usage_limit(global_state: GlobalState)

Parameters:

global_state

Returns:

increment_states_pc(states: List[GlobalState]) → List[GlobalState]

Parameters:

states

Returns:

mythril.laser.ethereum.instructions.transfer_ether(global_state: GlobalState, sender: BitVec, receiver: BitVec, value: int | 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: 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) → List[GlobalState] | None

Parameters:

• create

• track_gas

Returns:

exec_preprocessing()

Parameters:

• create

• track_gas

Returns:

execute_state(global_state: GlobalState) → Tuple[List[GlobalState], str | None]

Execute a single instruction in global_state.

Parameters:

global_state

Returns:

A list of successor states.

execute_state_preprocessing(global_state: GlobalState) → Tuple[List[GlobalState], str | None]

Execute a single instruction in global_state.

Parameters:

global_state

Returns:

A list of successor states.

execute_transactions(address) → None

This function helps runs plugins that can order transactions. Such plugins should set self.executed_transactions as True after its execution

Parameters:

address – Address of the contract

Returns:

None

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

handle_vm_exception(global_state: GlobalState, op_code: str, error_msg: str) → List[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[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:

preprocessing_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: WorldState | None = None, target_address: int | None = None, creation_code: str | None = None, contract_name: str | None = 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(*args, **kwargs)

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: List[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: int | Expression) → int

Parameters:

item

Returns:

mythril.laser.ethereum.util.get_instruction_index(instruction_list: List[Dict], address: int) → int | None

Parameters:

• instruction_list

• address

Returns:

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

Parameters:

• instr

• state

Returns:

mythril.laser.ethereum.util.insert_ret_val(global_state: GlobalState)

mythril.laser.ethereum.util.pop_bitvec(state: MachineState) → 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