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:

// 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:

1.3 Core Invariants by Protocol Type

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?

Step 3: Infer Implicit Conditions

Code flow analysis:

// 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

## 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?"