Skip to content

SECURITY_MODEL.md

Latest commit

 

History

History
164 lines (127 loc) · 17.2 KB

SECURITY_MODEL.md

File metadata and controls

164 lines (127 loc) · 17.2 KB
Raw

Security Model

AppleZKProver is not production proving software yet. It is a GPU-accelerated cryptographic proving backend under active development. The security model below defines the bar that future code must meet before the project claims production-grade proof security.

Assets

  • private witness bytes uploaded to GPU buffers,
  • intermediate hash states,
  • Merkle leaves and internal nodes,
  • future field/codeword buffers,
  • future transcript challenges,
  • final commitments, openings, and proofs,
  • public PCS statements and verifier decisions.
  • public application proof statements, statement digests, and verifier decisions.

Attacker Model

The primary attacker can:

  • supply malformed public inputs,
  • request unusually shaped workloads,
  • observe public outputs and timings,
  • run verifier code on untrusted proof bytes,
  • trigger repeated prover executions on the same machine.

The current model does not defend against:

  • a compromised operating system,
  • a malicious kernel driver,
  • physical access to GPU memory,
  • same-machine privileged inspection,
  • fault injection,
  • side-channel attacks from hostile co-tenants on the same device.

Those exclusions must be revisited before any production deployment claim.

Trust Boundaries

  • CPU API boundary: untrusted callers provide byte arrays, counts, lengths, and strides.
  • GPU command boundary: Swift encoders pass trusted buffer layouts to Metal kernels.
  • CPU oracle boundary: CPU reference code is the correctness source for tests, not an optimized prover path.
  • Verifier boundary: verifier code must never trust prover-generated metadata without checking it.

Current Guarantees

The current package aims to guarantee:

  • SHA3-256 CPU oracle matches known test vectors,
  • Keccak-256 CPU oracle matches known test vectors and is domain-separated from SHA3-256,
  • GPU SHA3 one-block output matches the CPU oracle for tested inputs,
  • GPU Keccak-256 one-block output matches the CPU oracle for tested inputs,
  • GPU Merkle roots match CPU Merkle roots for tested layouts,
  • GPU threadgroup Merkle treelets and fused upper reductions use disjoint ping-pong scratch spans for child reads and parent writes,
  • CPU Merkle opening verification recomputes the SHA3 leaf hash and all parent hashes from the supplied bottom-up sibling path,
  • GPU Merkle opening extraction for raw SHA3 leaves matches the independent CPU opening oracle for tested layouts,
  • CPU FIPS 205 SLH-DSA covers all 12 SHA2/SHAKE parameter sets, rejects malformed structured key/signature lengths, separates pure and pre-hash domains with context length checks, pins SHA2 category 3/5 F/H/T_l hash selection with reference vectors, exposes SHA-256/SHA-512 compression-level traces, HMAC pad-level traces, MGF1 counter-level traces, WOTS+/FORS public-key reconstruction composition traces, XMSS authentication path composition traces, hypertree layer composition traces, SHAKE/SHA3 sponge-level traces backed by Keccak-f[1600] round-level constraint traces, and exposes executable arithmetization reports with independently rechecked operation traces for hash primitives, address encodings, compressed SHA2 address encodings, WOTS+ chain replay, WOTS+/FORS public-key reconstruction, XMSS root reconstruction, hypertree root reconstruction, and slh_verify_internal acceptance checks,
  • invalid non-power-of-two Merkle leaf counts are rejected,
  • fixed-rate GPU SHA3 rejects inputs longer than 136 bytes,
  • CPU Merkle oracle layout failures and one-block hash length failures return typed errors instead of process traps,
  • zero-length one-block messages are handled as valid SHA3 input,
  • CPU and GPU transcript squeeze paths consume the full SHA3-256 rate, advance through additional squeeze blocks with Keccak-F1600, and use rejection sampling for field reduction,
  • M31 vector add, subtract, negate, multiply, square, and inverse plans match the independent CPU oracle for tested canonical inputs and edge values, with public inverse inputs required to be nonzero,
  • M31 dot-product plans match the independent CPU oracle for tested canonical inputs, edge values, and non-power-of-two vector lengths,
  • the M31 sum-check chunk transcript uses versioned header, round, and challenge frames with stable CPU vectors and GPU differential coverage,
  • QM31 FRI fold-chain transcript modes use versioned, domain-separated frames and rejection-sampled secure-field challenge limbs,
  • the Merkle-bound QM31 FRI chain mode commits each current resident QM31 layer before deriving that layer's fold challenge and verifies generated roots against an independent CPU oracle in the public checked path,
  • the linear QM31 FRI proof format uses versioned serialization, binds commitments and final values into query sampling, verifies every queried Merkle decommitment, and checks fold consistency with a CPU-only verifier,
  • the resident Circle PCS/FRI proof emitter returns canonical proof bytes from an already-resident evaluation/codeword buffer, keeps the materialized committed-layer log private, and proveVerified decodes those bytes before checking them with the independent CPU verifier,
  • the Circle FFT codeword plan validates canonical bounded P(x) + yQ(x) coefficients, rejects overlapping coefficient/output resident ranges, writes codewords into resident buffers with FFT stages, and is checked against a direct CPU Circle-domain oracle before feeding the resident proof emitter in the verified path,
  • the composed Circle coefficient-to-proof plan accepts Circle FFT-basis coefficient buffers, keeps the generated codeword and intermediate FRI layers private, and reads back only public proof material: commitments, final layer, queried leaves, sibling paths, and encoded proof bytes,
  • CircleWitnessToFFTBasisPlanV1 transforms private resident monomial coefficient witness columns into resident Circle FFT-basis coefficients with a public M31 transform matrix; this avoids coefficient readback but does not verify AIR semantics,
  • AIRTraceResidentSynthesisPlanV1 accepts private column-major M31 witness columns, checks canonicality on GPU, and writes the row-major resident AIRExecutionTraceV1 layout checked against the CPU witness-to-AIR trace oracle in the verified test path,
  • CirclePCSFRIParameterSetV1.conservative128 fixes the V1 Circle PCS/FRI verifier profile at logBlowupFactor = 4, queryCount = 36, foldingStep = 1, and grindingBits = 0; lower-level V1 proof and transcript surfaces support verifier-checked nonzero grinding through an 8-byte nonce, but the conservative public profile claims no grinding credit,
  • CirclePCSFRIArtifactManifestV1.current records the implemented PCS slice and explicitly marks sumcheck/GKR artifact integration as unsupported inside the PCS artifact. The resident codeword-to-commitment path fuses final Circle FFT butterflies with first-layer SHA3 leaf hashing while still materializing the first layer for verifier query openings,
  • CirclePCSFRIContractVerifierV1 is the public CPU-only verifier contract for the implemented Circle PCS/FRI slice. It enforces the profile, canonical domain, exact round count, terminal constant final layer, combined coefficient budget, transcript binding, Merkle openings, structured polynomial claims, and claimed first-layer evaluation openings,
  • the checked-in Circle PCS/FRI corpus pins canonical accepted proof bytes, expected proof digests, and tamper/rejection vectors for the strict contract,
  • M31SumcheckProofV1 serializes the narrow M31 chunk coefficient log, transcript challenges, and final folded vector; M31SumcheckVerifierV1 independently replays the framed transcript, checks fold consistency, and binds initial/final vector digests,
  • M31SumcheckVerificationReportV1 classifies that verifier result as only a revealedEvaluationVectorFoldingTrace; M31MultilinearSumcheckProofV1 separately verifies a public full multilinear evaluation-table sum-check, and AIRConstraintMultilinearSumcheckProofV1 binds that proof to the canonical AIR constraint-reduction vector with a zero-sum claim. These public sum-check paths still reveal their initial vectors and are not zero-knowledge,
  • ApplicationProofV1 binds witness commitment, AIR definition, and GKR claim digests into one ApplicationProofStatementV1 digest, then verifies the embedded M31SumcheckProofV1 and CirclePCSFRIProofV1 with CPU-only verifier code,
  • ApplicationProofVerificationReportV1 separates the accepted implemented component slice from the unsupported witness/AIR/GKR theorem scope for ApplicationProofV1 proof bytes alone,
  • ApplicationProofManifestV1.current records that AIR semantic verification, witness-to-AIR trace production, AIR-to-sum-check reduction, GKR verification, end-to-end theorem verification, and M31 sum-check zero-knowledge remain unsupported inside the ApplicationProofV1 artifact,
  • AIRProofV1 is a standalone public revealed-trace AIR proof scaffold. It binds AIR definition, witness trace, transcript-composed constraint-evaluation digests, and a CPU public trace quotient-divisibility certificate. Its verifier rederives the public trace, AIR composition oracle, and quotient certificate. It is not succinct, does not prove quotient low degree through PCS openings, and is not zero-knowledge,
  • AIRProofQuotientPCSArtifactV1 wraps AIRProofV1 with a public Circle PCS bundle for packed quotient coefficient chunks. It verifies the public AIR proof, the quotient PCS proofs, and the bundle-to-quotient-proof binding. The quotient coefficients and witness remain public, so this is not zero-knowledge and not a succinct AIR/GKR theorem proof,
  • ApplicationTheoremVerifierV1 provides a public sidecar theorem path that binds a public witness trace digest, verifies witness-to-AIR trace production, AIR transition/boundary constraints, AIR-to-M31-sum-check vector reduction, and a CPU layered arithmetic GKR claim; ApplicationWitnessLayoutV1 validates named public M31 witness layouts before trace production, AIRTraceToCirclePCSWitnessV1 can pack public AIR trace rows into QM31 CirclePCSFRIPolynomialClaimV1 chunks without moving AIR semantics into the PCS proof, AIRTraceToCircleFFTBasisWitnessV1 can derive matching Circle FFT-basis coefficient chunks for those arbitrary public trace layouts without making them resident-private or zero-knowledge, AIRTraceCirclePCSProofBundleV1 proves every generated public trace chunk with the strict Circle PCS verifier contract and strict bundle encoding/digest support, AIRTracePCSOpeningConstraintVerifierV1 checks AIR constraints directly on PCS-opened trace rows while reporting whether those openings cover the full AIR, AIRTracePCSOpeningQueryPlannerV1 derives public transition query rows from initial trace PCS commitment roots so AIRTracePCSQueriedOpeningBundleV1 can reject non-query row claims, AIRTraceQuotientPCSQueryAlignmentVerifierV1 checks matching public quotient PCS openings at those query storage indices, AIRSharedDomainQuotientIdentityPCSProofBundleV1 checks the public AIR quotient identity at shared row-domain trace, shifted-trace, and quotient PCS openings, and ApplicationPublicTheoremIntegratedArtifactV1 packages the public theorem artifact with the AIR sumcheck and quotient-identity reports behind a strict codec and corpus-pinned digest surface so callers have one integrated public verifier surface; ApplicationTheoremManifestV1.current records that this path is not zero-knowledge and is not a succinct proof,
  • ApplicationPublicTheoremArtifactV1 packages the application statement, application proof, public witness trace, AIR definition, and GKR claim into one decodable public theorem artifact. The artifact verifier checks the same AIR/GKR theorem without out-of-band sidecar inputs, but the witness and GKR inputs are public and the artifact is not zero-knowledge. ApplicationPublicTheoremArtifactCorpusV1.json pins stable public theorem digests and semantic AIR/GKR rejection vectors,
  • ApplicationPublicTheoremTracePCSArtifactV1 packages the public theorem artifact with an AIR trace PCS proof bundle, verifies that the bundle matches the regenerated public AIR trace, and requires the application proof's PCS statement/proof pair to appear inside that bundle. This is a public trace-commitment artifact, not a zero-knowledge or succinct AIR/GKR proof,
  • Keccak-F1600 permutation-only batch plans are differentially tested against the CPU permutation oracle for scalar and opt-in simdgroup kernels,
  • reusable hash, Keccak-F permutation, Merkle, M31 vector, and M31 sum-check plans expose explicit buffer clearing methods; Merkle and M31 clearing includes shared upload ring slots and private scratch buffers,
  • shared upload ring copies clear unused slot tails before reuse, and strided GPU result buffers clear unwritten padding before returning Data,
  • verified accelerator APIs are available for fixed-rate SHA3/Keccak hashes, Keccak-F1600 permutation batches, raw-leaf Merkle commitments, raw-leaf Merkle openings, planned Merkle commitments, M31 vector arithmetic, M31 dot products, M31 sum-check chunks, QM31 vector arithmetic, QM31 FRI folds, QM31 FRI fold chains, Circle codeword generation, and resident Circle PCS/FRI proof emission,
  • the M31 GPU fold path uses the 2^31 - 1 Mersenne reduction instead of generic integer remainder for canonical M31 values.

These are correctness guarantees for the implemented slice. They are not a full proof-system security claim.

Malicious Accelerator Handling

The GPU is not a cryptographic verifier. A production verifier must be CPU-only and deterministic. When a caller does not trust accelerator execution, it must use the verified APIs so the CPU oracle independently recomputes the GPU result before accepting it.

The verified APIs defend against incorrect accelerator results for CPU-visible inputs. They do not defend against a compromised OS, malicious kernel driver, or a caller that supplies only GPU-resident private buffers without a CPU copy or independently known expected result.

Required Cryptographic Rules

All future protocol code must follow these rules:

  • every hash use must have an explicit domain tag,
  • SHA3-256 and Keccak-256 must never be treated as interchangeable because their padding domains differ,
  • leaf hash, parent hash, transcript hash, challenge derivation, and proof serialization must use distinct domains,
  • Fiat-Shamir transcripts must absorb all public commitments and protocol parameters in a deterministic order,
  • verifier code must recompute challenges independently,
  • proof formats must version all cryptographic choices,
  • malformed proof inputs must fail closed,
  • CPU verifier code must not depend on GPU execution.

GPU Memory Rules

GPU buffers can contain private witness data. Runtime code must therefore make buffer lifetime and clearing explicit.

Required rules:

  • public APIs must document whether each input is public, private, or derived,
  • reusable plans and arenas must support clearing private regions before reuse, including shared upload ring slots,
  • shared upload staging must clear stale tail bytes when a shorter copy reuses a larger slot,
  • result buffers with public strides must clear unwritten padding before returning host-visible bytes,
  • benchmarks must not log witness-derived buffers,
  • only final public commitments and requested openings should be copied back by default,
  • debug paths that read intermediate buffers must be opt-in and clearly marked.

Timing And Side-Channel Rules

The current SHA3/Merkle kernels operate on public lengths and regular memory layouts. Future private-witness code must avoid:

  • secret-dependent branch divergence,
  • secret-dependent memory addressing,
  • secret-dependent command topology,
  • logging or serializing private intermediate data.

The M31 sum-check and dot-product uploaded-buffer APIs assume canonical field elements already reside in the buffer. They intentionally do not modulo-reduce uploaded values in the GPU path; callers that need CPU-side input validation must use the public array API. M31 vector inversion rejects zero through the public array API before dispatch because zero has no field inverse. M31SumcheckProofV1 is not zero-knowledge; its first coefficient slice is the initial evaluation vector for the narrow chunk proof.

When avoiding those patterns is impossible, the API must document the leakage and the code must not be used for private-witness production proving.

Input Validation Rules

Every GPU-facing API must validate:

  • count bounds,
  • stride and length consistency,
  • power-of-two requirements where applicable,
  • maximum one-block hash length,
  • output stride requirements,
  • integer multiplication overflow before buffer sizing.

Malformed inputs must return typed errors rather than trapping in library code.

Review Gates

Before this project claims production security:

  • all proof verifiers must be CPU-only and deterministic,
  • fuzzing must cover public deserialization and verifier inputs,
  • GPU/CPU differential tests must run over randomized workloads,
  • cryptographic parameter choices must be documented,
  • Circle witness/AIR/sumcheck/GKR outputs must either have semantic verifiers integrated into the same proof artifact or be explicitly excluded from the statement class before any full proof-system claim,
  • lattice-based parameter choices, if added later, must include an independent lattice-estimator reproduction artifact,
  • an external cryptography review must be completed.