mythril.analysis package

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: mythril.laser.ethereum.state.global_state.GlobalState) → Optional[mythril.analysis.ops.Call][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[mythril.laser.smt.bool.Bool], issue: mythril.analysis.report.Issue, detector)[source]

Bases: mythril.laser.ethereum.state.annotation.StateAnnotation

persist_over_calls

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: mythril.analysis.ops.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[source]

Bases: enum.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: mythril.laser.ethereum.state.annotation.StateAnnotation

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: mythril.laser.ethereum.state.global_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: mythril.laser.ethereum.state.global_state.GlobalState) → mythril.analysis.potential_issues.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[KT, VT])[source]

Adds sane block data to a transaction_sequence

add_code_info(contract)[source]
Parameters:contract –
as_dict
Returns:
resolve_function_names()[source]

Resolves function names for each step

static resolve_input(data, function_name)[source]

Adds decoded calldate to the tx sequence.

transaction_sequence_jsonv2

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

transaction_sequence_users

Returns the transaction sequence without pre-generated block data

class mythril.analysis.report.Report(contracts=None, exceptions=None, execution_info: Optional[List[mythril.laser.execution_info.ExecutionInfo]] = 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: Optional[List[str]] = None) → List[mythril.analysis.report.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: Optional[List[str]] = None) → List[mythril.analysis.report.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: mythril.laser.ethereum.state.global_state.GlobalState, constraints: mythril.laser.ethereum.state.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: Union[int, str, mythril.laser.smt.bitvec.BitVec], strategy: str, dynloader=None, max_depth: int = 22, execution_timeout: Optional[int] = None, loop_bound: int = 3, create_timeout: Optional[int] = None, transaction_count: int = 2, modules: Optional[List[str]] = 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.

execution_info

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