1606776394
## Formal Verification - Add TLA+ specs for UTXO conservation (formal/tla/UTXOConservation.tla) - Add TLA+ specs for GHOSTDAG ordering (formal/tla/GHOSTDAGOrdering.tla) - Add mathematical proof of DAA convergence (formal/proofs/) - Document Kani verification approach (formal/kani/) ## Bug Bounty Program - Add SECURITY.md with vulnerability disclosure process - Add docs/BUG_BOUNTY.md with $500-$100,000 reward tiers - Define scope, rules, and response SLA ## Web Wallet Dilithium3 WASM Integration - Build WASM module via Docker (498KB optimized) - Add wasm-crypto.ts lazy loader for Dilithium3 - Add createHybridSignatureLocal() for full client-side signing - Add createHybridSignatureSmart() for auto-mode selection - Add Dockerfile.wasm and build scripts ## Security Review ($0 Approach) - Add .github/workflows/security.yml CI workflow - Add deny.toml for cargo-deny license/security checks - Add Dockerfile.security for audit container - Add scripts/security-audit.sh for local audits - Configure cargo-audit, cargo-deny, cargo-geiger, gitleaks
123 lines
3.5 KiB
Markdown
123 lines
3.5 KiB
Markdown
# Synor Formal Verification
|
|
|
|
This directory contains formal verification artifacts for the Synor blockchain.
|
|
|
|
## Overview
|
|
|
|
Formal verification provides mathematical proofs that critical system properties hold for **all possible inputs**, not just tested examples.
|
|
|
|
## Verification Layers
|
|
|
|
| Layer | Tool | What It Verifies |
|
|
|-------|------|------------------|
|
|
| **Specification** | TLA+ | State machine invariants |
|
|
| **Code** | Kani | Rust implementation correctness |
|
|
| **Property** | Proptest | Random input testing |
|
|
| **Mathematical** | Proofs | Algorithm correctness |
|
|
|
|
## Directory Structure
|
|
|
|
```
|
|
formal/
|
|
├── tla/ # TLA+ specifications
|
|
│ ├── UTXOConservation.tla # UTXO value conservation
|
|
│ └── GHOSTDAGOrdering.tla # DAG ordering determinism
|
|
├── kani/ # Kani proof harnesses
|
|
│ └── README.md # How to use Kani
|
|
└── proofs/ # Mathematical proofs
|
|
└── DifficultyConvergence.md
|
|
```
|
|
|
|
## Critical Invariants Verified
|
|
|
|
### 1. UTXO Conservation
|
|
**Property:** Total value of UTXOs equals total minted (coinbase) minus fees.
|
|
|
|
**Verification:**
|
|
- [x] TLA+ specification (`tla/UTXOConservation.tla`)
|
|
- [x] Property testing (`crates/synor-consensus/tests/property_tests.rs`)
|
|
- [ ] Kani proofs (TODO)
|
|
|
|
### 2. No Double-Spend
|
|
**Property:** Each UTXO can only be spent once.
|
|
|
|
**Verification:**
|
|
- [x] TLA+ specification (in UTXOConservation.tla)
|
|
- [x] Property testing (utxo_add_remove_identity)
|
|
- [x] Unit tests
|
|
|
|
### 3. DAG Ordering Determinism
|
|
**Property:** Given the same DAG, all nodes compute identical blue sets and ordering.
|
|
|
|
**Verification:**
|
|
- [x] TLA+ specification (`tla/GHOSTDAGOrdering.tla`)
|
|
- [x] Unit tests (65 tests in synor-dag)
|
|
|
|
### 4. Difficulty Convergence
|
|
**Property:** Under stable hashrate, block time converges to target.
|
|
|
|
**Verification:**
|
|
- [x] Mathematical proof (`proofs/DifficultyConvergence.md`)
|
|
- [x] Property testing (difficulty_adjustment_bounded)
|
|
|
|
### 5. Supply Bounded
|
|
**Property:** Total supply never exceeds MAX_SUPPLY (21M).
|
|
|
|
**Verification:**
|
|
- [x] TLA+ specification (SupplyBounded invariant)
|
|
- [x] Property testing (amount tests)
|
|
- [x] Compile-time enforcement
|
|
|
|
## Running Verification
|
|
|
|
### TLA+ (TLC Model Checker)
|
|
|
|
```bash
|
|
# Install TLA+ Toolbox or use CLI
|
|
tlc formal/tla/UTXOConservation.tla
|
|
|
|
# Or use online version: https://lamport.azurewebsites.net/tla/toolbox.html
|
|
```
|
|
|
|
### Property Tests
|
|
|
|
```bash
|
|
cargo test -p synor-consensus property
|
|
```
|
|
|
|
### Kani (when installed)
|
|
|
|
```bash
|
|
cargo install --locked kani-verifier
|
|
kani setup
|
|
|
|
cd crates/synor-consensus
|
|
kani --tests
|
|
```
|
|
|
|
## Verification Status
|
|
|
|
| Component | Property | TLA+ | Kani | Proptest | Math |
|
|
|-----------|----------|:----:|:----:|:--------:|:----:|
|
|
| UTXO | Conservation | ✅ | ⏳ | ✅ | - |
|
|
| UTXO | No double-spend | ✅ | ⏳ | ✅ | - |
|
|
| DAG | Ordering determinism | ✅ | ⏳ | - | - |
|
|
| Difficulty | Convergence | - | - | ✅ | ✅ |
|
|
| Difficulty | Bounded adjustment | - | - | ✅ | ✅ |
|
|
| Amount | Overflow safety | - | ⏳ | ✅ | - |
|
|
|
|
Legend: ✅ Done | ⏳ Planned | - Not applicable
|
|
|
|
## Next Steps
|
|
|
|
1. **Install Kani** and add proof harnesses to each crate
|
|
2. **Run TLC** on TLA+ specs with small model
|
|
3. **CI Integration** for property tests and Kani
|
|
4. **Expand proofs** for network layer properties
|
|
|
|
## References
|
|
|
|
- [TLA+ Hyperbook](https://lamport.azurewebsites.net/tla/hyperbook.html)
|
|
- [Kani Documentation](https://model-checking.github.io/kani/)
|
|
- [Proptest Book](https://altsysrq.github.io/proptest-book/)
|
|
- [Amazon S3 ShardStore TLA+](https://github.com/awslabs/aws-s3-tla)
|