nox security
security properties and formal guarantees of nox
security bounds
SOUNDNESS: Invalid transactions rejected with probability ≥ 1 - 2^(-128)
PRIVACY: Cannot distinguish transactions with same public structure
CONSERVATION: Σ(energy) = initial + minted - burned (mathematically enforced)
QUANTUM RESIST: Hash-based security only, ~128-bit post-quantum (Grover limit)
attack surface
Attack │ Defense
────────────────┼─────────────────────────────────────────────
Double Spend │ Nullifier set prevents reuse
Inflation │ Circuit enforces conservation
Front-Running │ Privacy hides transaction contents
Sybil │ Focus proportional to stake
DoS │ Focus-based metering limits computation
Eclipse │ Namespace completeness proofs
Replay │ Nonces and nullifiers ensure uniqueness
Forgery │ ZK proofs unforgeable without witness
formal properties
Turing completeness
Theorem: nox is Turing-complete. Proof: Construct encoding of arbitrary Turing machine M via patterns 0-4, 9. ∎
confluence
Theorem: nox is confluent. Proof: Orthogonal rewrite system by Huet-Levy (1980). ∎
cost determinism
Theorem: Cost is identical across all reduction orders and implementations. Proof: By structural induction on formula. ∎
focus conservation
Theorem: $\sum_i \text{focus}(i) = 1$ for all valid states. Proof: All operations preserve sum; invalid transitions rejected by verification. ∎
privacy soundness
Theorem: A valid ZK proof implies all circuit constraints are satisfied with probability $\geq 1 - 2^{-128}$. Proof: By STARK/Plonky2 soundness. ∎
double-spend prevention
Theorem: Same record cannot be spent twice. Proof:
- Each record has unique (nonce, owner_secret) pair
- Nullifier = H(nonce, owner_secret) is deterministic
- Same record → same nullifier
- Nullifier set is append-only
- Transaction rejected if nullifier already in set ∎
complexity comparison
┌─────────────────────┬───────────────┬───────────────┬───────────────┬───────────────┐
│ Operation │ Traditional │ Blockchain │ Database │ nox │
│ │ (RAM model) │ (Ethereum) │ (SQL/NoSQL) │ │
├─────────────────────┼───────────────┼───────────────┼───────────────┼───────────────┤
│ Equality check │ O(n) compare │ O(n) compare │ O(n) compare │ O(1) hash │
│ Membership proof │ O(n) scan │ O(log n) MPT │ O(log n) index│ O(log² n) poly│
│ Completeness proof │ impossible │ impossible │ impossible │ O(log² n) poly│
│ Computation verify │ O(n) re-exec │ O(n) re-exec │ N/A │ O(log n) STARK│
│ Recursive verify │ O(n) re-exec │ O(n) re-exec │ N/A │ O(1) composed │
│ Privacy + verify │ incompatible │ incompatible │ incompatible │ O(1) ZK proof │
├─────────────────────┼───────────────┼───────────────┼───────────────┼───────────────┤
│ Cost determinism │ ✗ cache-dep │ ~ gas approx │ ✗ query-dep │ ✓ structural │
│ Parallel safety │ ✗ explicit │ ✗ sequential │ ✗ locks │ ✓ confluent │
└─────────────────────┴───────────────┴───────────────┴───────────────┴───────────────┘
see cyber/nox for the execution model, cyber/bbg for the ZK privacy architecture, cyber/stark for proof verification