smom-dbis-138/docs/bridge/trustless/FORMAL_VERIFICATION.md

Formal Verification - Trustless Bridge

Overview

This document describes the formal verification approach for the trustless bridge system using Certora Prover. Formal verification provides mathematical proofs that the contracts satisfy critical security properties.

Verification Tool

Tool: Certora Prover
License: Commercial (requires Certora license)
Configuration: verification/certora/certora.conf

Verified Contracts

1. BondManager

Specification: verification/certora/specs/BondManager.spec

Properties Verified:

• Bond Calculation: Bond amount always >= max(depositAmount * multiplier / 10000, minBond)
• State Exclusivity: Bond cannot be both slashed and released
• Slashing Split: Slashing correctly splits 50% to challenger, 50% burned
• Total Bonds Tracking: totalBonds[relayer] correctly updated on all operations
• No Duplicate Bonds: Cannot post bond twice for same depositId
• Reentrancy Protection: All state-changing functions protected

Critical Invariants:

invariant bondStateExclusive(uint256 depositId)
    bonds[depositId].slashed == false || bonds[depositId].released == false;

2. ChallengeManager

Specification: verification/certora/specs/ChallengeManager.spec

Properties Verified:

• Challenge Window: Cannot finalize before window expires
• Challenge Timing: Cannot challenge after window expires
• Finalization Rules: Cannot finalize challenged or already-finalized claims
• Fraud Proof Verification: Only valid proofs accepted
• State Exclusivity: Claim cannot be both finalized and challenged
• Reentrancy Protection: All functions protected

Critical Invariants:

invariant claimStateExclusive(uint256 depositId)
    claims[depositId].finalized == false || claims[depositId].challenged == false;

3. InboxETH

Specification: verification/certora/specs/InboxETH.spec

Properties Verified:

• Rate Limiting: Cooldown period enforced (60 seconds)
• Rate Limiting: Hourly limit enforced (100 claims/hour)
• Minimum Deposit: Minimum deposit amount enforced (0.001 ETH)
• Relayer Fee Calculation: Fee = (amount * relayerFeeBps) / 10000
• No Duplicate Claims: Cannot submit duplicate claims for same depositId
• Fee Claiming: Fee can only be claimed after finalization, by relayer, once
• Reentrancy Protection: All functions protected

4. LiquidityPoolETH

Specification: verification/certora/specs/LiquidityPoolETH.spec

Properties Verified:

• Minimum Ratio Enforcement: Withdrawals blocked if below minimum ratio
• Fee Calculation: LP fee calculated correctly
• Liquidity Tracking: totalLiquidity correctly updated
• Pending Claims Tracking: pendingClaims correctly managed
• Access Control: Only authorized addresses can release funds
• Reentrancy Protection: All functions protected

Critical Invariants:

invariant liquidityRatioMaintained(AssetType assetType)
    pools[assetType].totalLiquidity >= (pools[assetType].pendingClaims * minLiquidityRatioBps) / 10000;

5. Lockbox138

Specification: verification/certora/specs/Lockbox138.spec

Properties Verified:

• Deposit ID Uniqueness: Each depositId is unique
• Replay Protection: Nonce prevents duplicate deposits
• Processed Deposits: processedDeposits[depositId] correctly tracked
• Nonce Increment: Nonces increment correctly per depositor
• Input Validation: Zero amounts and recipients rejected
• Reentrancy Protection: All functions protected

Critical Invariants:

invariant depositIdUniqueness(uint256 depositId)
    processedDeposits[depositId] == true || processedDeposits[depositId] == false;

Running Verification

Prerequisites

1. Certora License: Obtain license from Certora
2. Certora Installation: Install Certora Prover
3. Dependencies: Ensure all contract dependencies are available

Run All Verifications

bash scripts/bridge/trustless/verify-contracts.sh

Run Individual Contract Verification

certoraRun contracts/bridge/trustless/BondManager.sol \
  --verify BondManager:verification/certora/specs/BondManager.spec \
  --solc solc-0.8.19 \
  --optimistic_loop \
  --loop_iter 3 \
  --smt_timeout 600

Using Configuration File

certoraRun verification/certora/certora.conf

Interpreting Results

Verification Passed ✅

• All specified properties hold
• No counterexamples found
• Contracts satisfy all invariants

Verification Failed ❌

• Counterexample found
• Property violation detected
• Review counterexample to understand issue

Verification Timeout ⏱️

• Prover could not complete in time
• May need to adjust timeout or simplify specification
• Consider breaking into smaller properties

Critical Properties

Economic Security

1. Bond Sizing: Bond always >= 110% of deposit (or minimum)
2. Slashing Correctness: Slashing splits 50/50 correctly
3. Economic Invariant: Fraud is always unprofitable

State Invariants

1. No Double Processing: Each depositId processed once
2. Challenge Window: Finalization only after window expires
3. Bond State: Bond cannot be both slashed and released

Access Control

1. Authorization: Only authorized addresses can call admin functions
2. Permissionless: Public functions accessible to all

Reentrancy Protection

1. No Reentrancy: All state-changing functions protected
2. External Calls: Safe external call patterns

Integration with CI/CD

GitHub Actions Example

name: Formal Verification

on: [push, pull_request]

jobs:
  verify:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v2
      - name: Run Formal Verification
        run: |
          bash scripts/bridge/trustless/verify-contracts.sh

Pre-commit Hook

Add to .git/hooks/pre-commit:

#!/bin/bash
# Run formal verification before commit
bash scripts/bridge/trustless/verify-contracts.sh

Specification Files

All specification files are located in verification/certora/specs/:

• BondManager.spec - Bond management properties
• ChallengeManager.spec - Challenge and finalization properties
• InboxETH.spec - Rate limiting and fee properties
• LiquidityPoolETH.spec - Liquidity and ratio properties
• Lockbox138.spec - Deposit uniqueness and replay protection

Updating Specifications

When updating contracts:

1. Review affected specifications
2. Update properties if contract logic changes
3. Re-run verification
4. Update documentation if properties change

Limitations

• Certora License Required: Commercial tool requiring license
• Specification Complexity: Complex properties may timeout
• Loop Handling: Requires careful handling of loops
• External Calls: May require additional modeling

Alternative Tools

If Certora is not available, consider:

• K Framework: Open-source formal verification
• Dafny: Microsoft's verification-aware language
• Why3: Multi-prover verification platform

Resources

• Certora Documentation
• Certora Prover Guide
• Specification Language Reference

Status

Current Status: ✅ Specifications created and ready for verification

Next Steps:

1. Obtain Certora license
2. Run initial verification
3. Address any property violations
4. Integrate into CI/CD pipeline