Comprehensive Protocol Suites
This is a collection of assertion suites for full protocols. These are deep dive use cases based on deployed and used protocols and a great starting point for understanding how to write assertions for your own protocols.- Aave V3 Suite: A comprehensive collection of assertions for the Aave V3 lending protocol, demonstrating real-world application of assertion patterns.
- Optimism FMA Suite: Assertions based on Optimism’s Failure Mode Analysis framework, covering cross-chain message passing and bridge security.
Access Control & Administrative Changes
- Implementation Address Change: Protects against unauthorized changes to proxy implementation addresses, preventing attackers from replacing contract logic with malicious code.
- KYC Whitelist: Ensures that only KYC accredited users can interact with a contract based on a unified KYC registry.
- Owner Change: Ensures ownership of a contract cannot be transferred unexpectedly, preventing attackers from gaining administrative control over critical protocol functions.
- Timelock Verification: Verifies that administrative actions are executed only after the required timelock period, preventing rushed or malicious changes to protocol parameters.
Liquidity Pool & AMM Security
- Constant Product: Ensures the constant product formula (k = x * y) is maintained in AMM pools, preventing price manipulation attacks and unauthorized token drains.
- Price Within Ticks: Verifies that concentrated liquidity positions in AMM protocols maintain prices within expected tick boundaries, protecting against price manipulation.
- Fee Calculations: Ensures trading fees are correctly calculated and distributed, preventing fee theft or unexpected losses in AMM protocols.
Lending Protocol Safety
- Lending Health Factor: Enforces minimum health factor requirements in lending protocols, preventing under-collateralized positions and protecting protocol solvency.
- Liquidation Health Factor: Ensures liquidations only occur when health factors fall below the liquidation threshold, protecting borrowers from premature or incorrect liquidations.
- Sum of All Positions: Verifies that the sum of all user positions matches the total asset balance, detecting accounting errors or unauthorized fund movements.
- Tokens Borrowed Invariant: Enforces that the relationship between borrowed tokens and collateral remains within safe protocol limits, preventing critical invariant violations.
Oracle Security
- Oracle Liveness Validation: Verifies that oracle data is fresh and updated within an acceptable time window, preventing the use of stale or manipulated price data.
- TWAP Deviation: Ensures the time-weighted average price doesn’t deviate excessively from previous values, detecting price manipulation attempts or oracle failures.
- Intra-Transaction Oracle Deviation: Monitors price oracle readings during a transaction to detect excessive deviations that might indicate flash loan attacks or price manipulation.
Vault & ERC4626 Security
- ERC4626 Assets to Shares: Verifies correct conversion between assets and shares in ERC4626 vaults, preventing accounting errors that could lead to fund loss.
- ERC4626 Deposit and Withdraw: Ensures deposit and withdrawal operations maintain correct accounting in ERC4626 vaults, protecting user funds during transfers.
- Harvest Increases Balance: Verifies that yield-generating operations like harvests always increase the total balance of vaults, preventing value extraction attacks.
Emergency & Special Mode Protection
- Panic State Validation: Validates critical protocol state variables during panic or emergency modes, ensuring fallback mechanisms work correctly when normal operations are suspended.
Data Integrity & Message Verification
- Farcaster Protocol Integrity: Ensures the integrity of cross-chain messages in the Farcaster protocol, preventing unauthorized or malformed message processing.
Fund Protection
- ERC20 Drain: Prevents excessive token outflows in a single transaction, mitigating the impact of potential exploits by limiting how quickly funds can be drained.
- Ether Drain: Monitors and limits ETH outflows from contracts, protecting against unauthorized withdrawals that could deplete protocol reserves.
Next: Explore previous hacks analysis to see how assertions could have prevented real-world exploits.