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 |
|---|---|---|
KingsVaultV2AsyncRedeem.sol |
Ethereum | Main vault (ERC-4626 / ERC-7540) |
KPortfolio.sol |
Ethereum | Portfolio fund router |
AaveEarnPool.sol |
Ethereum | Aave V3 adapter |
ERC4626EarnPool.sol |
Ethereum | Morpho Steakhouse adapter |
HyperStrategy.sol |
HyperEVM | Cross-chain strategy executor |
Key Vulnerability Classes
| SWC ID | Name | Relevance to King's Vault |
|---|---|---|
| SWC-107 | Reentrancy | withdraw, settle, depositPool, withdrawPool |
| SWC-101 | Integer Overflow/Underflow | PPS calculation, fee share minting |
| SWC-105 | Unprotected Ether Withdrawal | Fee collection, emergency redeem |
| SWC-106 | Unprotected SELFDESTRUCT | Proxy / upgrade patterns |
| SWC-115 | Authorization through tx.origin |
Must use msg.sender for access control |
| SWC-104 | Unchecked Call Return Value | External calls to Aave, Morpho, CoreWriter |
Areas of Focus
- Share Price Manipulation: Explore whether symbolic execution reveals paths where PPS can be manipulated through specific deposit/withdraw/settle orderings.
- Fee Calculation Edge Cases: Edge cases where
totalSupply == 0orPPS_HWM == PPS_currentmight cause division by zero or unexpected minting. - Cross-Function Reentrancy: Interactions between
deposit → settle → redeemthat could exploit state inconsistencies mid-transaction. - Emergency Function Safety: Verify
windingUp()andemergencyRedeem()cannot be exploited to extract more than the user's pro-rata share.
Running
myth analyze src/vaults/KingsVaultV2AsyncRedeem.sol --solc-json mythril.config.json --execution-timeout 900
Results should be committed to this page after each audit cycle.