122 lines
2.8 KiB
Markdown
122 lines
2.8 KiB
Markdown
|
# Formal Verification - Trustless Bridge
|
||
|
|
|
||
|
|
## Overview
|
||
|
|
|
||
|
|
This directory contains formal verification specifications and configuration for the trustless bridge system using Certora Prover.
|
||
|
|
|
||
|
|
## Directory Structure
|
||
|
|
|
||
|
|
```
|
||
|
|
verification/
|
||
|
|
├── certora/
|
||
|
|
│ ├── certora.conf # Certora configuration file
|
||
|
|
│ └── specs/ # Specification files
|
||
|
|
│ ├── BondManager.spec
|
||
|
|
│ ├── ChallengeManager.spec
|
||
|
|
│ ├── InboxETH.spec
|
||
|
|
│ ├── LiquidityPoolETH.spec
|
||
|
|
│ └── Lockbox138.spec
|
||
|
|
├── reports/ # Generated verification reports
|
||
|
|
└── README.md # This file
|
||
|
|
```
|
||
|
|
|
||
|
|
## Quick Start
|
||
|
|
|
||
|
|
### Prerequisites
|
||
|
|
|
||
|
|
1. **Certora License**: Obtain license from [Certora](https://www.certora.com/)
|
||
|
|
2. **Certora Installation**: Install Certora Prover
|
||
|
|
3. **Dependencies**: Ensure all contract dependencies are available
|
||
|
|
|
||
|
|
### Run Verification
|
||
|
|
|
||
|
|
```bash
|
||
|
|
# Run all verifications
|
||
|
|
bash scripts/bridge/trustless/verify-contracts.sh
|
||
|
|
|
||
|
|
# Or run individual contract
|
||
|
|
certoraRun contracts/bridge/trustless/BondManager.sol \
|
||
|
|
--verify BondManager:verification/certora/specs/BondManager.spec \
|
||
|
|
--solc solc-0.8.19
|
||
|
|
```
|
||
|
|
|
||
|
|
## Specification Files
|
||
|
|
|
||
|
|
### BondManager.spec
|
||
|
|
Verifies:
|
||
|
|
- Bond calculation correctness
|
||
|
|
- Slashing mechanics (50/50 split)
|
||
|
|
- State exclusivity (cannot be slashed and released)
|
||
|
|
- Total bonds tracking
|
||
|
|
- Reentrancy protection
|
||
|
|
|
||
|
|
### ChallengeManager.spec
|
||
|
|
Verifies:
|
||
|
|
- Challenge window enforcement
|
||
|
|
- Finalization rules
|
||
|
|
- Fraud proof verification
|
||
|
|
- State exclusivity
|
||
|
|
- Reentrancy protection
|
||
|
|
|
||
|
|
### InboxETH.spec
|
||
|
|
Verifies:
|
||
|
|
- Rate limiting (cooldown, hourly limit)
|
||
|
|
- Minimum deposit enforcement
|
||
|
|
- Relayer fee calculation
|
||
|
|
- No duplicate claims
|
||
|
|
- Reentrancy protection
|
||
|
|
|
||
|
|
### LiquidityPoolETH.spec
|
||
|
|
Verifies:
|
||
|
|
- Minimum ratio enforcement
|
||
|
|
- Fee calculation
|
||
|
|
- Liquidity tracking
|
||
|
|
- Pending claims management
|
||
|
|
- Access control
|
||
|
|
- Reentrancy protection
|
||
|
|
|
||
|
|
### Lockbox138.spec
|
||
|
|
Verifies:
|
||
|
|
- Deposit ID uniqueness
|
||
|
|
- Replay protection (nonce)
|
||
|
|
- Processed deposits tracking
|
||
|
|
- Input validation
|
||
|
|
- Reentrancy protection
|
||
|
|
|
||
|
|
## Configuration
|
||
|
|
|
||
|
|
The `certora.conf` file contains:
|
||
|
|
- Contract paths
|
||
|
|
- Solidity compiler version (0.8.19)
|
||
|
|
- Rule files (specifications)
|
||
|
|
- Prover options
|
||
|
|
- Output settings
|
||
|
|
|
||
|
|
## Reports
|
||
|
|
|
||
|
|
Verification reports are saved to `verification/reports/`:
|
||
|
|
- Individual contract reports
|
||
|
|
- Summary reports
|
||
|
|
- Counterexample traces (if violations found)
|
||
|
|
|
||
|
|
## Documentation
|
||
|
|
|
||
|
|
See `docs/bridge/trustless/FORMAL_VERIFICATION.md` for:
|
||
|
|
- Detailed property descriptions
|
||
|
|
- How to interpret results
|
||
|
|
- CI/CD integration
|
||
|
|
- Troubleshooting
|
||
|
|
|
||
|
|
## Status
|
||
|
|
|
||
|
|
✅ **Specifications Complete**: All specification files created
|
||
|
|
⏳ **Verification Pending**: Requires Certora license to run
|
||
|
|
|
||
|
|
## Next Steps
|
||
|
|
|
||
|
|
1. Obtain Certora license
|
||
|
|
2. Run initial verification
|
||
|
|
3. Address any property violations
|
||
|
|
4. Integrate into CI/CD pipeline
|
||
|
|
|