mythril.analysis package

Subpackages

Submodules

mythril.analysis.analysis_args module

mythril.analysis.call_helpers module

This module provides helper functions for the analysis modules to deal with call functionality.

mythril.analysis.call_helpers.get_call_from_state(state: GlobalState) → Call | None[source]
Parameters:

state

Returns:

mythril.analysis.callgraph module

This module contains the configuration and functions to create call graphs.

mythril.analysis.callgraph.extract_edges(statespace)[source]
Parameters:

statespace

Returns:

mythril.analysis.callgraph.extract_nodes(statespace)[source]
Parameters:

  • statespace

  • color_map

Returns:

mythril.analysis.callgraph.generate_graph(statespace, title='Mythril / Ethereum LASER Symbolic VM', physics=False, phrackify=False)[source]
Parameters:

  • statespace

  • title

  • physics

  • phrackify

Returns:

mythril.analysis.issue_annotation module

class mythril.analysis.issue_annotation.IssueAnnotation(conditions: List[Bool], issue: Issue, detector)[source]

Bases: StateAnnotation

property persist_over_calls: bool

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

The default is set to False

persist_to_world_state() → bool[source]

If this function returns true then laser will also annotate the world state.

If you want annotations to persist through different user initiated message call transactions then this should be enabled.

The default is set to False

mythril.analysis.ops module

This module contains various helper methods for dealing with EVM operations.

class mythril.analysis.ops.Call(node, state, state_index, _type, to, gas, value=<mythril.analysis.ops.Variable object>, data=None)[source]

Bases: Op

The representation of a CALL operation.

class mythril.analysis.ops.Op(node, state, state_index)[source]

Bases: object

The base type for operations referencing current node and state.

class mythril.analysis.ops.VarType(value)[source]

Bases: Enum

An enum denoting whether a value is symbolic or concrete.

CONCRETE = 2
SYMBOLIC = 1
class mythril.analysis.ops.Variable(val, _type)[source]

Bases: object

The representation of a variable with value and type.

mythril.analysis.ops.get_variable(i)[source]
Parameters:

i

Returns:

mythril.analysis.potential_issues module

class mythril.analysis.potential_issues.PotentialIssue(contract, function_name, address, swc_id, title, bytecode, detector, severity=None, description_head='', description_tail='', constraints=None)[source]

Bases: object

Representation of a potential issue

class mythril.analysis.potential_issues.PotentialIssuesAnnotation[source]

Bases: StateAnnotation

property search_importance

Used in estimating the priority of a state annotated with the corresponding annotation. Default is 1

mythril.analysis.potential_issues.check_potential_issues(state: GlobalState) → None[source]

Called at the end of a transaction, checks potential issues, and adds valid issues to the detector.

Parameters:

state – The final global state of a transaction

Returns:

mythril.analysis.potential_issues.get_potential_issues_annotation(state: GlobalState) → PotentialIssuesAnnotation[source]

Returns the potential issues annotation of the given global state, and creates one if one does not already exist.

Parameters:

state – The global state

Returns:

mythril.analysis.report module

This module provides classes that make up an issue report.

class mythril.analysis.report.Issue(contract: str, function_name: str, address: int, swc_id: str, title: str, bytecode: str, gas_used=(None, None), severity=None, description_head='', description_tail='', transaction_sequence=None, source_location=None)[source]

Bases: object

Representation of an issue and its location.

static add_block_data(transaction_sequence: Dict)[source]

Adds sane block data to a transaction_sequence

add_code_info(contract)[source]
Parameters:

contract

property as_dict
Returns:

static decode_bytes(val)[source]
resolve_function_names()[source]

Resolves function names for each step

static resolve_input(data, function_name)[source]

Adds decoded calldate to the tx sequence.

property transaction_sequence_jsonv2

Returns the transaction sequence as a json string with pre-generated block data

property transaction_sequence_users

Returns the transaction sequence without pre-generated block data

class mythril.analysis.report.Report(contracts=None, exceptions=None, execution_info: List[ExecutionInfo] | None = None)[source]

Bases: object

A report containing the content of multiple issues.

append_issue(issue)[source]
Parameters:

issue

as_json()[source]
Returns:

as_markdown()[source]
Returns:

as_swc_standard_format()[source]

Format defined for integration and correlation.

Returns:

as_text()[source]
Returns:

environment = <jinja2.environment.Environment object>
sorted_issues()[source]
Returns:

mythril.analysis.security module

This module contains functionality for hooking in detection modules and executing them.

mythril.analysis.security.fire_lasers(statespace, white_list: List[str] | None = None) → List[Issue][source]

Fire lasers at analysed statespace object

Parameters:

  • statespace – Symbolic statespace to analyze

  • white_list – Optionally whitelist modules to use for the analysis

Returns:

Discovered issues

mythril.analysis.security.retrieve_callback_issues(white_list: List[str] | None = None) → List[Issue][source]

Get the issues discovered by callback type detection modules

mythril.analysis.solver module

This module contains analysis module helpers to solve path constraints.

mythril.analysis.solver.get_transaction_sequence(global_state: GlobalState, constraints: Constraints) → Dict[str, Any][source]

Generate concrete transaction sequence. Note: This function only considers the constraints in constraint argument, which in some cases is expected to differ from global_state’s constraints

Parameters:

  • global_state – GlobalState to generate transaction sequence for

  • constraints – list of constraints used to generate transaction sequence

mythril.analysis.solver.pretty_print_model(model)[source]

Pretty prints a z3 model

Parameters:

model

Returns:

mythril.analysis.swc_data module

This module maps SWC IDs to their registry equivalents.

mythril.analysis.symbolic module

This module contains a wrapper around LASER for extended analysis purposes.

class mythril.analysis.symbolic.SymExecWrapper(contract, address: int | str | BitVec, strategy: str, dynloader=None, max_depth: int = 22, execution_timeout: int | None = None, loop_bound: int = 3, create_timeout: int | None = None, transaction_count: int = 2, modules: List[str] | None = None, compulsory_statespace: bool = True, disable_dependency_pruning: bool = False, run_analysis_modules: bool = True, custom_modules_directory: str = '')[source]

Bases: object

Wrapper class for the LASER Symbolic virtual machine.

Symbolically executes the code and does a bit of pre-analysis for convenience.

property execution_info: List[ExecutionInfo]

mythril.analysis.traceexplore module

This module provides a function to convert a state space into a set of state nodes and transition edges.

mythril.analysis.traceexplore.get_serializable_statespace(statespace)[source]
Parameters:

statespace

Returns:

Module contents