Skip to content

Mythril Analysis

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.

Scope

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)

Key Vulnerability Classes

SWC ID Name Relevance to King's Vault
SWC-107 Reentrancy withdraw, claim, emergencyRedeem, executeRedeem — all transfer USDC
SWC-101 Integer Overflow/Underflow Dual-pricing share conversions, fee share calculation, _processingAssets decrement
SWC-105 Unprotected Ether Withdrawal Fee collection via share minting; harvestOnlyForController
SWC-106 Unprotected SELFDESTRUCT UUPS proxy upgrade on Controller
SWC-115 Authorization through tx.origin Must use msg.sender for all role checks
SWC-104 Unchecked Call Return Value External calls to Aave Pool, ERC-4626 vaults, CoreWriter, CCTP MessageTransmitter

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: Edge cases where prevSupply == 0, prevAssets == 0, or newAssets <= prevAssets might cause division by zero or unexpected fee share minting in Controller._calculateFee().
  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() in both KingsVaultV2 and KingsVaultV2Async cannot extract more than a user's pro-rata share via repeated calls or share manipulation.
  5. CCTP Message Replay: Verify HyperStrategy.completeDivest() and updateRemoteState() cannot be replayed — relying on CCTP transmitter's internal nonce enforcement.

Running

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

Results should be committed to this page after each audit cycle.