Mythril Symbolic

Basic Usage

Analyze Source Code

# Analyze single file
myth analyze Contract.sol

# Analyze with Solidity version
myth analyze Contract.sol --solv 0.8.20

# Analyze specific contract
myth analyze Contract.sol:MyContract

Analyze Bytecode

# Analyze deployed contract
myth analyze -a 0x<address> --rpc <rpc_url>

# Analyze bytecode file
myth analyze --bin-runtime contract.bin

Configuration Options

Transaction Depth

# Default depth (2)
myth analyze Contract.sol

# Increased depth for complex interactions
myth analyze Contract.sol --execution-timeout 300 -t 3

# Deep analysis (slow)
myth analyze Contract.sol --execution-timeout 600 -t 4

Timeout Settings

# Set execution timeout (seconds)
myth analyze Contract.sol --execution-timeout 300

# Set solver timeout
myth analyze Contract.sol --solver-timeout 10000

# Quick scan
myth analyze Contract.sol --execution-timeout 60 -t 2

Module Selection

# Run specific modules
myth analyze Contract.sol --modules ether_thief,suicide

# Available modules
# - ether_thief
# - suicide
# - integer_overflow/underflow
# - delegatecall
# - arbitrary_write
# - state_change_external_call

Output Formats

Standard Output

myth analyze Contract.sol

JSON Output

myth analyze Contract.sol -o json > report.json

Markdown Output

myth analyze Contract.sol -o markdown > report.md

JSONV2 (Detailed)

myth analyze Contract.sol -o jsonv2 > detailed.json

Vulnerability Detection

Reentrancy Detection

Mythril detects reentrancy by tracking:

• External calls
• State changes after calls
• ETH transfers

==== External Call To User-Supplied Address ====
SWC ID: 107
Severity: Low
Contract: Vulnerable
Function name: withdraw()
PC address: 1234
Estimated Gas Usage: 2500 - 10000
Type: Informational
...

Integer Overflow/Underflow

==== Integer Overflow ====
SWC ID: 101
Severity: High
Contract: Token
Function name: transfer(address,uint256)
PC address: 567
Estimated Gas Usage: 3000 - 5000
A possible integer overflow exists in the function...

Unprotected Self-Destruct

==== Unprotected Selfdestruct ====
SWC ID: 106
Severity: High
Contract: Vulnerable
Function name: kill()
Any sender can trigger self-destruction...

Advanced Usage

Concolic Execution

# Use concrete values where possible
myth analyze Contract.sol --strategy dfs --execution-timeout 300

Custom Constraints

# Analyze with constraints file
myth analyze Contract.sol --constraints constraints.json

State Space Pruning

# Limit state explosion
myth analyze Contract.sol --max-depth 30 --call-depth-limit 3

CI/CD Integration

GitHub Actions