Skip to content

Mythril Analysis Scope & Methodology

Status: methodology only — not a completed audit report. No executed analysis result, severity assessment, or independent audit assurance is published on this page.

Overview

Mythril is a symbolic execution tool for EVM bytecode that detects security vulnerabilities by exploring execution paths. It is particularly effective at finding integer overflow/underflow, reentrancy, and access control issues.

Proposed V2 Scope

Match the source commit, compiler settings, and deployment before analysis. This starting scope does not establish coverage of the Saving-specific strategy/routes, HyperEVM execution components, or GHO Staking V3. Those require explicitly defined, source-matched scopes.

Contract Network Description
KingsVaultV2.sol Ethereum Synchronous ERC-4626 vault
KingsVaultV2Async.sol Ethereum Async redeem vault (escrow-based)
Controller.sol Ethereum UUPS-upgradeable coordinator
AaveV3Strategy.sol Ethereum Aave V3 lending strategy adapter
ERC4626Strategy.sol Ethereum Generic ERC-4626 strategy adapter
HyperStrategy.sol Ethereum CCTP V2 cross-chain strategy (Ethereum-side)

Review Questions

These are analysis targets, not detected vulnerabilities. Tool classifications and coverage must be recorded from an actual run; a generic Ether-withdrawal or SELFDESTRUCT category does not by itself establish a finding about ERC-20 fee minting or UUPS upgrades.

Area Checks to perform
Reentrancy Explore token/strategy callbacks and cross-function accounting changes. Distinguish request/execution bookkeeping from the paths that actually transfer USDC.
Arithmetic and pricing Explore rounding, zero-value cases, fee accounting, and processing-asset updates using the current source's state model.
Asset and share authorization Verify who may transfer assets, mint shares, harvest tokens, and choose recipients.
Upgrade authorization Verify initialization, the actual privileged role, implementation changes, and storage compatibility separately from any SELFDESTRUCT checks.
Caller identity Verify that authorization cannot be bypassed through forwarding or inappropriate reliance on tx.origin.
External calls and messages Check return handling, failure propagation, message provenance, nonce freshness, and attestation validation.

Areas of Focus

  1. Share Price Manipulation via Dual-Pricing: Explore whether symbolic execution reveals paths where _convertToShares / _convertToAssets can be manipulated through specific deposit/withdraw/confirm orderings to bypass MAX/MIN protection.
  2. Fee Calculation Edge Cases: Resolve the current fee-accounting functions from the pinned source, then test zero supply/assets, losses, book-value changes, configurable rates, and profitable confirmation. The current V2 portal rate is 0%; test both that configuration and permitted rate changes without treating a hypothetical test as a deployed finding.
  3. Cross-Function Reentrancy (Async Vault): Interactions between withdraw → executeRedeem → claim that could exploit escrow state inconsistencies mid-transaction.
  4. Emergency Function Safety: Verify emergencyRedeem(address receiver) in both KingsVaultV2 and KingsVaultV2Async against the current ABI and source, including pending/executed requests, reserved assets, repeated calls, and assets still outside the vault.
  5. CCTP Message Replay and Ordering: Verify transmitter nonce enforcement and the strategy's accepted source, sender, and remote-state nonce checks. Distinguish Keeper relay authorization from transmitter callback authorization.

Running

Illustrative commands only; confirm the configuration, compiler inputs, source paths, and supported command options for the pinned tool version:

myth analyze src/vaults/KingsVaultV2Async.sol --solc-json mythril.config.json --execution-timeout 900
myth analyze src/controllers/Controller.sol --solc-json mythril.config.json --execution-timeout 900

Evidence Required for a Published Result

Publish the run date, source commit, compiler/build settings, Mythril version and command, analyzed contracts and exclusions, execution limits, raw output, finding triage, remediation commits, and retest results. Symbolic execution has coverage limits; absence of a reported issue is not proof of safety. A source-level result must not be represented as a deployed-contract audit without a documented source-to-bytecode and configuration match.