Gulshan Yadav 1606776394 feat: Phase 7 critical tasks - security, formal verification, WASM crypto

## 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

2026-01-10 01:40:03 +05:30

2.9 KiB

Raw Blame History

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

# Install Kani
cargo install --locked kani-verifier
kani setup

Running Proofs

# 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:

Uses kani::any() to generate arbitrary inputs
Sets up preconditions with kani::assume()
Executes the code under test
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:

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

#[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

2.9 KiB Raw Blame History