State Invariant Detection

State Invariant Detection

Automatically infer mathematical relationships between state variables, then find functions that break those relationships. Catches the most devastating DeFi vulnerabilities: unauthorized minting, broken tokenomics, accounting discrepancies, and state desynchronization.

When to Use

• Auditing token contracts for supply/balance mismatches
• Analyzing staking, vault, or pool contracts for accounting errors
• Detecting conservation law violations in treasury/fund management
• Finding AMM/DEX constant product violations
• Verifying that aggregate variables stay synchronized with individual records

When NOT to Use

• Guard-state consistency analysis (use semantic-guard-analysis)
• Full multi-dimensional audit (use behavioral-state-analysis)
• Entry point identification only (use entry-point-analyzer)

Core Concept: State Variable Proportionality

Hypothesis: In well-designed contracts, state variables maintain mathematical relationships (invariants) that should never be violated.

When a function modifies one side of a relationship without updating the other, the invariant breaks — creating exploitable accounting errors.

Five Types of State Relationships

Type 1: Sum Relationships (Aggregation)

Copy code
totalSupply = Σ balance[i] for all users i

Found in: ERC20 tokens, staking pools, vaults, share systems

Type 2: Difference Relationships (Conservation)

Copy code
totalFunds = availableFunds + lockedFunds

Found in: Treasuries, liquidity pools, vesting contracts

Type 3: Ratio Relationships (Proportional)

Copy code
k = reserveA × reserveB  (constant product)
sharePrice = totalAssets / totalShares

Found in: AMMs, DEXs, vault share pricing, collateralization

Type 4: Monotonic Relationships (Ordering)

Copy code
newValue ≥ oldValue  (only increases)

Found in: Timestamps, nonces, accumulated rewards, total distributions

Type 5: Synchronization Relationships (Coupling)

Copy code
If stateA changes, stateB must change correspondingly

Found in: Deposit/mint pairs, burn/release pairs, collateral/borrowing power

For detailed definitions and examples, see {baseDir}/references/invariant-types.md.

The Three-Phase Detection Architecture

Phase 1: State Variable Clustering

Group state variables that appear to be related.

Algorithm:

Copy code
For each pair of state variables (A, B):
  1. Track all functions that modify A
  2. Track all functions that modify B
  3. Calculate co-modification frequency:

     CoMod(A, B) = |Functions modifying both A and B| / |Functions modifying A or B|

  4. If CoMod(A, B) > 0.6 → A and B are likely related

Example:

solidityCopy code
// mint() modifies BOTH totalSupply and balances → co-modified
// burn() modifies BOTH totalSupply and balances → co-modified
// transfer() modifies ONLY balances → does not co-modify

CoMod(totalSupply, balances) = 2/3 = 66.7%
Cluster identified: (totalSupply, balances)

Phase 2: Invariant Inference

Determine the mathematical relationship between clustered variables.

Method 1 — Delta Pattern Matching:

Copy code
mint():     Δtotal = +amount, Δbalance = +amount  → Same direction, same magnitude
burn():     Δtotal = -amount, Δbalance = -amount  → Same direction, same magnitude
transfer(): Δbalance1 = -x, Δbalance2 = +x       → Net zero change

Inference: totalSupply = Σ balances (Aggregation invariant)

Method 2 — Delta Correlation:

Copy code
If ΔA = ΔB in all cases      → Direct proportional (A = B + constant)
If ΔA = -ΔB in all cases     → Inverse proportional (A + B = constant)
If ΔA × constant = ΔB        → Ratio relationship
If ΔA occurs whenever ΔB     → Synchronization invariant

Method 3 — Expression Mining:

Parse actual code operations:

solidityCopy code
// Code: totalSupply += amount; balances[user] += amount;
// Extracted: Δtotal = Δbalance
// Inferred: total = Σ balances

// Code: available = total - locked;
// Extracted: available + locked = total
// Inferred: Conservation law

Invariant Confidence:

Copy code
Confidence(I) = |functions preserving I| / |functions modifying variables in I|

Phase 3: Invariant Violation Detection

Find functions that break established relationships.

Algorithm:

Copy code
For each inferred invariant I(stateA, stateB):
  For each function F that modifies stateA or stateB:

    Before: Capture (stateA, stateB)
    Simulate: Execute F
    After: Capture (stateA', stateB')

    If I(stateA, stateB) = True AND I(stateA', stateB') = False:
      → F is VULNERABLE

Vulnerability Set:

Copy code
V_I = {F ∈ Functions | ∃σ : I(σ) = True ∧ I(F(σ)) = False}

Workflow

Copy code
Task Progress:
- [ ] Step 1: Identify all state variables in the contract
- [ ] Step 2: Build co-modification matrix for all variable pairs
- [ ] Step 3: Cluster related variables (CoMod > 0.6)
- [ ] Step 4: Infer invariant type for each cluster (delta patterns)
- [ ] Step 5: Test each function against inferred invariants
- [ ] Step 6: Apply temporal filtering (only flag persistent violations)
- [ ] Step 7: Score severity and generate report

Dual-Layer Integration

This skill is Layer 2 of the Semantic State Protocol. For maximum coverage, combine with Layer 1 (semantic-guard-analysis):

Output Format

markdownCopy code
## State-State Invariant Violation Report

### Finding: [Title]

**Function:** `functionName()` at `Contract.sol:L42`
**Severity:** [CRITICAL | HIGH | MEDIUM]
**Invariant:** `[mathematical expression]`

**Before Execution:**
  stateA = [value], stateB = [value]
  Invariant: [expression] = True ✓

**After Execution:**
  stateA = [value'], stateB = [value']
  Invariant: [expression] = False ✗

**Root Cause:**
[Which state variable was modified without updating its counterpart]

**Impact:**
[Accounting errors, inflated supply, broken pricing, exploitable drift]

**Attack Scenario:**
1. [Step-by-step exploit leveraging the desynchronization]

**Recommendation:**
[Specific fix — add the missing state update]

Quick Detection Checklist

When analyzing a contract, immediately check:

• Does every function that modifies balances also update totalSupply (or have a valid reason not to)?
• Does every function that moves between available and locked maintain total = available + locked?
• Does every swap/trade function maintain the constant product k = reserveA * reserveB?
• Do aggregate counters (totalStaked, totalRewards) stay synchronized with per-user mappings?
• Are monotonic variables (nonces, timestamps) ever decremented?

For detailed case studies, see {baseDir}/references/case-studies.md.

Rationalizations to Reject

• "The totalSupply is just for display" → Protocols use totalSupply for share pricing, voting power, market cap — drift is exploitable
• "Admin functions can bypass invariants" → Admin functions that break accounting create permanent protocol insolvency
• "The difference is small" → Small accounting errors compound over time and transactions
• "It's an emergency function" → Emergency functions that break state invariants create worse emergencies
• "Transfer doesn't need to update totalSupply" → Correct, but verify the NET change in sum(balances) is zero