Kontor-Crypto implements Proof-of-Retrievability using recursive SNARKs. Storage nodes generate proofs (~10KB, ~30ms to verify) demonstrating possession of challenged file sectors without revealing data. Challenges are derived deterministically from public randomness. The system must prevent proof forgery, replay attacks, ledger substitution, metadata tampering, and DoS.
synthesize_por_circuit() defines R1CS constraints enforcing proof validity. Verify: constraint completeness, gating logic for padding slots, uniformity (fixed constraint count), public input binding of security-critical values.
derive_index_unbiased() and poseidon_hash_tagged() determine audited data. Challenges must be unpredictable, uniformly distributed, domain-separated, deterministic, and unbiased.
Plan::make_plan() and build_z0_primary() bind proofs to specific files and ledger state. Public I/O layout in src/config.rs::PublicIOLayout (lines 46-181). Verify prover/verifier construct identical inputs, aggregated root derived from verifier's ledger only, canonical ordering, no prover-controlled values.
Single-file proofs use file root from metadata; multi-file uses ledger.tree.root() from verifier's ledger. Prover cannot influence which root is used.
verify() performs validation before SNARK verification. Check error vs invalid proof distinction (Ok(false) vs Err), no panics on malformed input, challenge ID binding.
Proof::from_bytes() / to_bytes() handle network boundary. Verify buffer overflow protection, version validation, trailing data rejection, fixed encoding.
Arecibo's prove_step has deliberate first-call no-op: RecursiveSNARK::new() synthesizes step 0, first prove_step() bumps counter only. Must call prove_step() exactly N times for N challenges, verify with num_steps = N. Check loop counts, off-by-one errors, state updates during no-op, proving/verification step count match.
depth_is_positive (OR of public depth bits) gates processing to slots with public_depth > 0. State updates (442-448), leaf outputs (450-462), root verification (404-418) all gated. Padding slots (depth=0) cannot forge proofs.
state_new = H(TAG_STATE_UPDATE, state_old, leaf) cryptographically links sequential steps, preventing reordering and ensuring all challenges are covered. Verify TAG_STATE_UPDATE = 7, proper state threading, no step skipping.
Files are chunked into fixed 31-byte symbols (max field element size for Pallas curve). Multi-codeword Reed-Solomon encoding (231 data + 24 parity symbols per codeword, ~10% overhead). Each 31-byte symbol = one Merkle leaf. This ensures provers must store actual data (not just hashes), preventing hash-only attacks. Verify fixed symbol size enforcement, power-of-2 tree padding, symbol-level RS encoding.
Poseidon Hash (via nova-snark): collision resistance, preimage resistance, random oracle in domain-separated contexts.
Nova SNARKs (nova-snark v0.41.0): soundness, completeness, knowledge soundness.
Pallas/Vesta Curves (pasta_curves): discrete log hardness, cycle properties.
Reed-Solomon (reed-solomon-erasure v6.0.0): reconstruction guarantees.
Verify version pinning, security advisories, no known vulnerabilities, component compatibility.
| Function | Inputs | DoS Risk | Handled |
|---|---|---|---|
prepare_file() |
data size, filename | Large files | ✅ |
Challenge::new() |
num_challenges, prover_id | Extreme values | ✅ |
prove() |
challenges.len(), num_challenges | Resource exhaustion | ✅ |
verify() |
proof bytes, challenges | Malformed data | ✅ |
reconstruct_file() |
sector count, metadata | Invalid combinations | ✅ |
FileLedger::load() |
file size, contents | Large/malformed files | ✅ |
Boundary conditions: empty inputs, maximum sizes (file/challenge/ledger count), zero values (depth, size, count), type boundaries (usize::MAX, u64::MAX).
Prover cannot generate valid proof without data. Check circuit constraints (synth.rs), Merkle path validation, state chaining (prevents step skipping), no freely-chosen witness values. Tests: security_malicious_prover.rs (9).
Honest prover always succeeds. Review error paths in prove(), witness generation for valid cases, no false rejections. Tests: all e2e.
Proof bound to specific challenges and ledger. Public inputs include aggregated_root (from ledger), challenge IDs derived deterministically (includes prover_id), verified before SNARK check, state chain creates temporal binding. Tests: security_replay_attack.rs, security_ledger_root_pinning.rs.
Same inputs → same outputs. No randomness, canonical ordering (BTreeMap), fixed serialization. Tests: regression.rs, api_consistency.rs.
Parser vulnerabilities, buffer overflows. Mitigations: magic byte validation, length checks, trailing data rejection, version validation.
Memory exhaustion, DoS. Limits: MAX_NUM_CHALLENGES (10,000), PRACTICAL_MAX_FILES (1,024), parameter cache (50), no unbounded loops.
Checked arithmetic, documented type conversions, bounds enforced before casts.
Root commitment binds (root, depth): rc = H(TAG_RC, root, depth). Public depth in circuit, ledger lookup uses rc, gating prevents depth=0 abuse.
Verifier derives aggregated root from its own ledger, not prover-supplied, cryptographically bound via public inputs.
State evolution one-way: state_new = H(TAG_STATE_UPDATE, state_old, leaf). Circuit enforces state threading, no skipping/reordering.
- Security and regression coverage spans dedicated suites in:
security_*.rs,validation.rs,verifier_edge_cases.rs,regression.rscircuit_*tests for constraint/wiring/uniformity invariantsledger_*tests for state evolution and persistence security
- Fuzzing coverage is implemented under
fuzz/with corpus-backed targets for:- proof parsing
- ledger loading
- symbol decoding
- challenge ID derivation
- Current enumerated test cases (
cargo test --workspace -- --list): 275
Remaining gaps: concurrency stress testing, timing/side-channel analysis.
Files: src/params.rs, src/api/prove.rs, src/api/verify.rs
Parameters generated on-demand, deterministically:
-
Shape derivation (
src/api/plan.rs):files_per_step= next power of 2 ≥ num_files,file_tree_depth= max depth across challenged files,aggregated_tree_depth= ledger depth (0 for single-file). -
Circuit witness (
src/params.rs::generate_params_for_shape()): dummy challenges/ledger matching shape,generate_circuit_witness(), no real file data. -
Nova setup (lines 132-137):
PublicParams::setup()with IPA commitment (ipa_pc), Pallas/Vesta cycle, floor keys fromnova-snark. -
Key generation (lines 139-142):
CompressedSNARK::setup(&pp)produces(ProverKey, VerifierKey). -
Cache: bundle as
PorParams, store for reuse.
Determinism: No randomness, shape from validated challenges only, fixed algorithm/constants. All nodes generate bit-identical parameters for same shape. No trusted setup, parameters regenerated independently. Test: regression.rs::regression_parameter_generation_consistency() (136-165).
Cache key: (files_per_step, file_tree_depth, aggregated_tree_depth). FIFO eviction at MAX_CACHE_SIZE (50). Mutex-protected, process-local, in-memory only. Generated lazily: prove() → setup_proving_environment() → load_or_generate_params() (132-136), verify() → load_or_generate_params() (71-75). Not bundled or downloaded.
Verifier generates parameters from challenge shape independently. If prover used different parameters, CompressedSNARK::verify() fails. Proof tied to circuit structure; mismatch produces invalid proof.
Security: Parameters uniquely determined by shape, cache process-local, keys from validated metadata, bounded size (50), mutex-protected.
Audit: Verify deterministic shape derivation (src/api/plan.rs, src/config.rs), no randomness (src/params.rs), identical circuit construction, cache key includes all shape parameters (33-37), verifier independence (71-75 in verify.rs), mismatch causes failure.
| Dependency | Version | Role | Audit Status |
|---|---|---|---|
nova-snark |
0.41.0 | Nova SNARK & Poseidon hash | Microsoft Research |
reed-solomon-erasure |
6.0.0 | Erasure coding | ? |
ff |
0.13 | Finite field arithmetic | ? |
Code: Features complete, tests passing, no TODO/FIXME in critical paths, review done.
Documentation: README accurate, public APIs documented, security properties documented, limitations listed.
Testing: cargo nextest run clean, 57+ security tests, edge cases, regressions, circuit uniformity.
Dependencies: cargo audit clean, versions pinned, licenses compatible, critical deps audited.