Security Model

Audits & Formal Verification

Security Model • Proof Soundness • Intent Replay Resistance • Position Spoofing Edge Cases

Overview

SnarkSide's security model is grounded not in obfuscation or validator trust, but in zero-knowledge soundness, constraint determinism, and non-interactive state transitions. Traditional smart contract audits do not fully apply—because user logic is encrypted, and execution is circuit-constrained, not contract-bound.

Auditing SnarkSide thus requires a hybrid model:

  • Formal cryptographic proof audits (circuit soundness, commitment security)

  • Protocol-level economic game analysis (liquidation incentives, LP leakage)

  • Smart contract verification (verifier logic, root commitment updates)

  • MPC relayer architecture review (handshake privacy, batching constraints)

This section documents the design decisions and assumptions underpinning SnarkSide’s security model, and the formal verification efforts aligned with its mainnet launch.

1. Proof Soundness Guarantees

All trades, vault updates, and liquidations are executed only if their accompanying Groth16 proof passes verification on-chain. Each proof:

  • Asserts constraint satisfaction for a specific circuit

  • Verifies commitment to Merkleized vault or intent trees

  • Is signed via a SNARK public input root

  • Guarantees position validity, leverage compliance, oracle normalization

Proof generation enforces:

  • Non-malleability (via fixed circuit template hashing)

  • Soundness under Fiat-Shamir heuristic

  • Field isolation (BN254 field; Poseidon hashing; trusted setup keys)

Example: Enforced Margin Constraint (in Circom)

component marginCheck = LessThan(64);
marginCheck.in[0] <== totalCollateral;
marginCheck.in[1] <== requiredCollateral;

Failure to satisfy this constraint results in a proof rejection—ensuring that no over-leveraged position can enter the protocol, regardless of relayer behavior.

2. Intent Replay Resistance

Every trade or vault action in SnarkSide is scoped by:

  • Salted intent hash

  • Epoch-specific nonce

  • Nullifier commitment (Merkle preimage reference)

These form the basis of non-replayability.

Intent Schema (ZK-Hashed):

{
  "action": "open",
  "market": "ETH-PERP",
  "size": "50000",
  "leverage": 10,
  "expiry": 1723609823,
  "salt": "0x1d78...",
  "nonce": 8421
}

Intent nullifiers are published on-chain during batch settlement:

mapping(bytes32 => bool) public nullifierUsed;

Any attempt to reuse an intent or vault position—whether altered or reordered—will fail SNARK verification due to nullifier reuse detection.

3. Position Spoofing Edge Cases

SnarkSide encrypts every margin vault as a blinded note, whose existence is only provable if:

  • The note is part of the vault Merkle tree

  • The vault’s field commitments match a valid circuit witness

  • The trade proof was generated with the user’s blinding key

Possible spoofing vectors:

Vector
Mitigation

Ghost positions

Merkle inclusion proof required; no phantom vaults accepted

Overwritten margin state

Nullifier uniqueness guarantees single-use vault slots

Fake LP shares

LP claim proofs tied to specific Oblivion Pool batch roots

Fake liquidation proofs

Oracle commitment + vault state proof required simultaneously

Cross-market spoofing

Market ID binding in SNARK public inputs (circuit root ID scoped)

Additionally, third-party relayers cannot fabricate valid intent or vault data, since they lack:

  • The prover’s private key for vault witness generation

  • The user’s blinding salt for note decryption

  • The correct Merkle path for vault state authentication

4. Formal Verification Tools & Methods

SnarkSide is undergoing multi-pronged verification:

a. Circom Circuit Testing

  • circuit-tester framework with 10,000+ fuzzed inputs

  • Coverage targets include:

    • Intent circuit

    • Vault transition circuit

    • Liquidation oracle circuit

    • Batch verifier constraints

b. zkAudit Proof Verifier Suite

  • Groth16 verifier test cases (w/ incorrect input replays)

  • Rejection paths for proof tampering

  • Constraint boundary checks (e.g., invalid leverage, expiry overflow)

c. Solidity Contract Audits

  • Vault contract: write-once nullifier register

  • Settlement verifier: public input hash derivation

  • Oracle: commit-reveal finality assertion

d. MPC Relay Layer Testing

  • Encrypted handshake flow simulation

  • Replay detection on bundle input

  • Intention grouping edge-case detection

5. Planned Audits and External Review

SnarkSide has engaged with cryptographic security researchers and plans to undergo:

  • Formal circuit soundness audit with ZK Labs (Q4)

  • On-chain verifier and settlement audit via Trail of Bits (pending)

  • Relayer gossip privacy model audit (w/ support from Zero Knowledge Podcast R&D DAO)

Conclusion

SnarkSide does not trust smart contracts alone. Its core invariant is this: if a state change cannot be proven under SNARK constraints, it cannot exist.

All attacks—replay, spoof, overreach—fail because they cannot produce a valid proof. In this design, audits aren’t just a precaution. They’re embedded in the math itself.

PreviousMainnet StrategyNextAudit Timeline

Last updated