This resource is a collection of use cases and patterns for assertions. The goal is to show how assertions can be used to prevent hacks and vulnerabilities in smart contracts and protocols. The content of the book is a great source for inspiration for how to write assertions for your own use cases and protocols.

Each entry in the book shows a code snippet of an assertion. Each assertion is accompanied by a minimal interface for the protocol the assertion is written for. Full examples that include mock protocol code and test cases are available in the Phylax Assertion Examples Repository.

​
Getting Started

It’s a good idea to check out the two links below to get started with assertions, but it’s not required to understand the content of the book.

If you have questions or issues, please reach out on telegram @phylax_credible_layer.

If you think an assertion is missing, please don’t hesitate to open a PR or reach out. We love digging into new hacks and use cases and writing assertions for them!

​
Table of Contents

​
Access Control & Administrative Changes

  • Implementation Address Change: Protects against unauthorized changes to proxy implementation addresses, preventing attackers from replacing contract logic with malicious code.

  • 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.