invariant-analysis

# Invariant Analysis Framework ## Purpose **"What conditions must ALWAYS be true? How can they be violated?"** Systematically extract protocol invariants and explore violation paths where these conditions can be broken. --- ## 1. Invariant Types ### 1.1 Explicit Invariants Directly verifiable in code: ```solidity // require/assert conditions require(totalSupply() == sum(balances), "Supply mismatch"); require(debt <= collateral * LTV / 100, "Undercollateralized"); // Documented conditions (NatSpec) /// @invariant totalAssets >= totalSupply /// @invariant userDebt[user] <= userCollateral[user] * LTV ``` ### 1.2 Implicit Invariants Must be inferred from code flow: | Pattern | Implicit Invariant | |---------|-------------------| | `shares = deposit * totalSupply / totalAssets` | totalAssets > 0 when totalSupply > 0 | | `balance[from] -= amount` | balance[from] >= amount | | `rewardPerToken += reward / totalStaked` | totalStaked > 0 when reward > 0 | | `collateralValue / debtValue >= LTV` | debtValue > 0 when loan exists | ### 1.3 Core Invariants by Protocol Type | Protocol Type | Invariant Example | |---------------|-------------------| | **Vault** | `totalShares == 0 ↔ totalAssets == 0` | | **AMM** | `reserveX * reserveY >= k` | | **Lending** | `totalBorrowed <= totalDeposited * utilizationCap` | | **Staking** | `sum(userStakes) == totalStaked` | | **Bridge** | `mintedOnL2 == lockedOnL1` | --- ## 2. Invariant Extraction Process ### Step 1: Collect Explicit Conditions ``` Grep("require\\(|assert\\(|revert.*if", glob="**/*.sol") Grep("@invariant|@notice.*must|@dev.*always", glob="**/*.sol") ``` ### Step 2: Analyze State Variable Relationships For each state variable: 1. Where is it modified? (setter functions) 2. Where is it read? (getter, calculation functions) 3. What relationships does it have with other variables? | Variable | Modification Functions | Read Functions | Relationship | |----------|----------------------|----------------|--------------| | totalSupply | mint, burn | deposit, withdraw | == sum(balances) | | totalAssets | deposit, withdraw, fee | convertToShares | >= totalSupply value | ### Step 3: Infer Implicit Conditions Code flow analysis: ```solidity // This code implicitly requires amount <= balance[from] function transfer(address to, uint256 amount) { balance[from] -= amount; // ← Reverts on underflow balance[to] += amount; } ``` --- ## 3. Violation Path Exploration ### 3.1 Single Function Violation ``` deposit(0) → shares = 0 * totalSupply / totalAssets = 0 → User fund loss (asset deposited, no shares received) ``` ### 3.2 Multi-Function Combination Violation ``` 1. deposit(1 wei) → shares = 1 2. Direct asset transfer (donate) → totalAssets increases, totalSupply unchanged 3. Next user deposit(X) → shares = X * 1 / (1 + donated) ≈ 0 → First depositor attack ``` ### 3.3 State Transition Order Violation ``` Normal: initialize() → setOracle() → deposit() Attack: deposit() (oracle not set) → price = 0 → infinite mint ``` ### 3.4 Edge Case Violation Test values: - `0` - Zero value handling - `1` - Minimum value - `type(uint256).max` - Overflow - `totalSupply == 0` - Initial state - `balance == 0` - Empty account --- ## 4. Output Format ```markdown ## Invariant Analysis Results ### Extracted Invariants | ID | Condition | Type | Maintenance Points | |----|-----------|------|-------------------| | INV-01 | totalSupply == sum(balances) | Explicit | mint, burn, transfer | | INV-02 | totalAssets >= totalShares (by value) | Implicit | deposit, withdraw | | INV-03 | userDebt <= userCollateral * LTV | Explicit | borrow, repay, liquidate | ### Potential Violation Paths | Invariant | Violation Scenario | Risk Level | |-----------|-------------------|------------| | INV-02 | First depositor attack via donation | High | | INV-03 | Oracle manipulation → forced liquidation | Critical | ### Detailed Analysis #### INV-02 Violation: First Depositor Attack - **Condition**: totalAssets / totalShares ratio can be manipulated - **Path**: deposit(1) → donate(1M) → next user deposit results in shares = 0 - **Impact**: Subsequent depositor fund loss - **Verification**: Check deposit() function ``` --- ## 5. Search Queries ``` # Find explicit invariants Grep("require\\(|assert\\(", glob="**/*.sol") Grep("@invariant|must.*always|never.*allow", glob="**/*.sol") # Find state variables Grep("mapping.*=>.*uint|uint256.*public|uint256.*private", glob="**/*.sol") # Find modification points Grep("\\+=|-=|\\*=|/=|=", glob="**/*.sol") ``` --- ## 6. Attacker Mindset - "If this invariant breaks, can I steal funds?" - "What function combination can bypass this invariant?" - "Does this invariant hold in initial state (empty pool)?" - "Can I force division by zero or overflow?"