mythril.laser.ethereum.strategy package

Subpackages

• mythril.laser.ethereum.strategy.extensions package
  • Submodules
  • mythril.laser.ethereum.strategy.extensions.bounded_loops module
    • BoundedLoopsStrategy
      • BoundedLoopsStrategy.calculate_hash()
      • BoundedLoopsStrategy.count_key()
      • BoundedLoopsStrategy.get_loop_count()
      • BoundedLoopsStrategy.get_strategic_global_state()
    • JumpdestCountAnnotation
  • Module contents

Submodules

mythril.laser.ethereum.strategy.basic module

This module implements basic symbolic execution search strategies.

class mythril.laser.ethereum.strategy.basic.BreadthFirstSearchStrategy(work_list, max_depth, **kwargs)

Bases: BasicSearchStrategy

Implements a breadth first search strategy I.E.

Execute all states of a “level” before continuing

get_strategic_global_state() → GlobalState

Returns:

view_strategic_global_state() → GlobalState

Returns:

class mythril.laser.ethereum.strategy.basic.DepthFirstSearchStrategy(work_list, max_depth, **kwargs)

Bases: BasicSearchStrategy

Implements a depth first search strategy I.E.

Follow one path to a leaf, and then continue to the next one

get_strategic_global_state() → GlobalState

Returns:

view_strategic_global_state() → GlobalState

Returns:

class mythril.laser.ethereum.strategy.basic.ReturnRandomNaivelyStrategy(work_list, max_depth, **kwargs)

Bases: BasicSearchStrategy

chooses a random state from the worklist with equal likelihood.

get_strategic_global_state() → GlobalState

Returns:

view_strategic_global_state() → GlobalState

Returns:

class mythril.laser.ethereum.strategy.basic.ReturnWeightedRandomStrategy(work_list, max_depth, **kwargs)

Bases: BasicSearchStrategy

chooses a random state from the worklist with likelihood based on inverse proportion to depth.

get_strategic_global_state() → GlobalState

Returns:

view_strategic_global_state() → GlobalState

Returns:

mythril.laser.ethereum.strategy.beam module

class mythril.laser.ethereum.strategy.beam.BeamSearch(work_list, max_depth, beam_width, **kwargs)

Bases: BasicSearchStrategy

chooses a random state from the worklist with equal likelihood.

static beam_priority(state)

get_strategic_global_state() → GlobalState

Returns:

sort_and_eliminate_states()

view_strategic_global_state() → GlobalState

Returns:

mythril.laser.ethereum.strategy.concolic module

class mythril.laser.ethereum.strategy.concolic.ConcolicStrategy(work_list: List[GlobalState], max_depth: int, trace: List[List[Tuple[int, str]]], flip_branch_addresses: List[str])

Bases: CriterionSearchStrategy

Executes program concolically using the input trace till a specific branch

check_completion_criterion()

get_strategic_global_state() → GlobalState

This function does the following:- 1) Choose the states by following the concolic trace. 2) In case we have an executed JUMPI that is in flip_branch_addresses, flip that branch. :return:

class mythril.laser.ethereum.strategy.concolic.TraceAnnotation(trace=None)

Bases: StateAnnotation

This is the annotation used by the ConcolicStrategy to store concolic traces.

property persist_over_calls: bool

If this function returns true then laser will propagate the annotation between calls

The default is set to False

Module contents

class mythril.laser.ethereum.strategy.BasicSearchStrategy(work_list, max_depth, **kwargs)

Bases: ABC

A basic search strategy which halts based on depth

abstract get_strategic_global_state()

run_check()

class mythril.laser.ethereum.strategy.CriterionSearchStrategy(work_list, max_depth, **kwargs)

Bases: BasicSearchStrategy

If a criterion is satisfied, the search halts

get_strategic_global_state()

set_criterion_satisfied()