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
112 lines
2.9 KiB
Markdown
112 lines
2.9 KiB
Markdown
# Kani Formal Verification for Synor
|
|
|
|
This directory contains Kani model checking proofs for critical Synor components.
|
|
|
|
## What is Kani?
|
|
|
|
Kani is a bit-precise model checker for Rust. It can verify that Rust programs are free of:
|
|
- Runtime panics
|
|
- Memory safety issues
|
|
- Assertion violations
|
|
- Undefined behavior
|
|
|
|
Unlike property testing (proptest), Kani exhaustively checks **all possible inputs** within defined bounds.
|
|
|
|
## Installation
|
|
|
|
```bash
|
|
# Install Kani
|
|
cargo install --locked kani-verifier
|
|
kani setup
|
|
```
|
|
|
|
## Running Proofs
|
|
|
|
```bash
|
|
# Run all Kani proofs in a crate
|
|
cd crates/synor-consensus
|
|
kani --tests
|
|
|
|
# Run specific proof
|
|
kani --harness utxo_add_never_overflows
|
|
|
|
# Run with bounded loops (for performance)
|
|
kani --harness utxo_conservation --default-unwind 10
|
|
```
|
|
|
|
## Proof Structure
|
|
|
|
Each proof harness:
|
|
1. Uses `kani::any()` to generate arbitrary inputs
|
|
2. Sets up preconditions with `kani::assume()`
|
|
3. Executes the code under test
|
|
4. Asserts postconditions with `kani::assert()` or standard `assert!`
|
|
|
|
## Proofs Included
|
|
|
|
### UTXO Module (`crates/synor-consensus/src/utxo_kani.rs`)
|
|
- `utxo_add_never_overflows` - Adding UTXOs cannot overflow total value
|
|
- `utxo_conservation` - Total value is conserved across operations
|
|
- `utxo_no_double_spend` - Same outpoint cannot exist twice
|
|
|
|
### Difficulty Module (`crates/synor-consensus/src/difficulty_kani.rs`)
|
|
- `difficulty_bits_roundtrip` - bits conversion is approximately reversible
|
|
- `difficulty_bounded_adjustment` - adjustment stays within bounds
|
|
- `target_difficulty_inverse` - higher difficulty = smaller target
|
|
|
|
### Amount Module (`crates/synor-types/src/amount_kani.rs`)
|
|
- `amount_checked_add_sound` - checked_add returns None on overflow
|
|
- `amount_saturating_sub_bounded` - saturating_sub never exceeds original
|
|
- `amount_max_supply_respected` - operations respect MAX_SUPPLY
|
|
|
|
## CI Integration
|
|
|
|
Add to `.github/workflows/kani.yml`:
|
|
|
|
```yaml
|
|
name: Kani Verification
|
|
on: [push, pull_request]
|
|
|
|
jobs:
|
|
kani:
|
|
runs-on: ubuntu-latest
|
|
steps:
|
|
- uses: actions/checkout@v4
|
|
- uses: model-checking/kani-github-action@v1
|
|
- run: kani --tests --workspace
|
|
```
|
|
|
|
## Writing New Proofs
|
|
|
|
```rust
|
|
#[cfg(kani)]
|
|
mod kani_proofs {
|
|
use super::*;
|
|
|
|
#[kani::proof]
|
|
fn my_function_never_panics() {
|
|
let input: u64 = kani::any();
|
|
// Preconditions
|
|
kani::assume(input < MAX_VALUE);
|
|
|
|
// Code under test
|
|
let result = my_function(input);
|
|
|
|
// Postconditions
|
|
assert!(result.is_ok());
|
|
}
|
|
}
|
|
```
|
|
|
|
## Limitations
|
|
|
|
- Kani has bounded model checking, so loops need unwinding limits
|
|
- Complex floating point is approximated
|
|
- External FFI calls are stubbed
|
|
- Network/filesystem operations are not verified
|
|
|
|
## References
|
|
|
|
- [Kani Documentation](https://model-checking.github.io/kani/)
|
|
- [AWS Kani Blog](https://aws.amazon.com/blogs/opensource/how-we-use-kani/)
|
|
- [Kani GitHub](https://github.com/model-checking/kani)
|