7. Formal security package — Halborn asks
Audience: Halborn (or equivalent formal security reviewer)
Scope: api-billing-v2 (not full VDI / identity / captcha)
Baseline: main @ 8ec535c (update on each packet refresh)
Companion: Attack matrix · Formal audit runner · Trust surface scope
QuantZK includes a formal security package designed to support an independent review. It documents the threat model, trust assumptions, adversarial test coverage, parser behavior, circuit inventory, canonicalization approach, and known limitations.
This is not a third-party audit report, and we do not claim that “QuantZK has been security audited.” It is QuantZK’s evidence package: what to run, what we claim, what we do not claim, and where to look in code.
Index of the eight asks
| # | Ask | Section |
|---|---|---|
| 1 | Coverage report | §1 |
| 2 | Threat model | §2-threat-model |
| 3 | Assumptions | §3-assumptions |
| 4 | Unsupported cases | §4-unsupported-cases--out-of-scope |
| 5 | Circuit review | §5-circuit-review |
| 6 | Parser review | §6-parser-review |
| 7 | Canonicalization | §7-canonicalization |
| 8 | Trust boundaries | §8-trust-boundaries |
1. Coverage report
Claim this section supports
The primary adversarial scenarios defined in our threat model are covered by executable tests.
That is the meaningful coverage statement for a security reviewer. Behavioral / scenario coverage matters more than raw line-coverage percentages.
1.1 Behavioral coverage (primary)
Each primary threat in §2 maps to a catalog ID (BV2-* / ADV-*) and an executable test. Fail-closed outcomes are asserted, not merely “code was visited.”
| Gate | Command | Expected |
|---|---|---|
| Artifact pins | bash scripts/verify-artifact-hashes.sh | Hash match + offline conformance |
| Offline adversarial | cd protocol && node --test test/adversarial-billing-v2.test.js | All pass |
| Pilot (functional) | cd verifier-api && npm run test:billing-pilot | 15/15 |
| Adversarial (HTTP) | cd verifier-api && npm run test:billing-adversarial | 12/12 |
| Full formal gates | bash scripts/run-formal-security-audit.sh | Writes audit-logs/formal-security-audit-*.json |
Catalogs:
protocol/conformance/billing-v2-conformance.json— BV2-* (happy, replay, tamper, meter, transparency, Phase-2)protocol/conformance/billing-v2-adversarial.json— ADV-* (proof graft, sig, revocation, forge log, overflow, oversize, canon)
Human matrix: billing-v2-attack-matrix.md
Threat → test mapping is in §2.3.
1.2 Line / statement coverage (optional plumbing aid)
Line percentages alone are not a security claim. If a reviewer wants Istanbul/lcov for the billing trust-surface files only, regenerate:
bash scripts/halborn-coverage-report.sh
# → audit-logs/halborn-coverage-<timestamp>/The script:
- Runs pilot and adversarial suites separately (
--runInBand) - Collects coverage only from
vdi.js,vdiBillingRuntime.js,artifactValidator.js,wellKnown.js - Disables the repo-wide Jest 85% threshold (that gate is for full-suite CI, not this snapshot)
| Suite | Tool | Role |
|---|---|---|
| Billing Jest suites | Istanbul / Jest --coverage | Optional attach; secondary to ADV/BV2 vectors |
| Root Vitest | @vitest/coverage-v8 | Frontend; out of billing trust surface |
Do not market a fixed “95% line coverage” (or similar) as assurance. Prefer the behavioral claim above. If halborn:coverage fails, re-check gates with npm run test:billing-pilot / test:billing-adversarial (no coverage) — those are the release bar.
1.3 Circuit constraint inventory
Phase-2 relation inventory is in §5 (public/private signals, Poseidon8 binding). Broader enforced-policy rule→constraint tables live in audit-circuit-coverage.md and are Track B / non-billing.
2. Threat model
2.1 Adversary
- Class: Probabilistic polynomial-time (PPT) attacker with API visibility and ability to craft HTTP bodies.
- Can: Reorder JSON; swap proof fields; forge Merkle inclusion proofs; race concurrent attests; supply stale/revoked IDs; send oversized/malformed payloads; attempt meter envelope forgery.
- Cannot (assumed): Break Ed25519 EUF-CMA, Groth16 soundness under the trusted setup, or find SHA-256 / Poseidon collisions except with negligible probability.
2.2 Assets
| Asset | Why it matters |
|---|---|
| Billing attestation + fingerprint | Dispute-grade charge/commitment evidence |
Replay uniqueness (tenant, window, event_id) | Prevents double-spend of usage |
| Transparency log tip + inclusion | Non-equivocation for auditors |
Phase-2 billing_proof | Cryptographic binding of commitment digest when enabled |
| Artifact pins (WASM/zkey/vkey) | Prevent silent circuit substitution |
2.3 Threat × evidence
| Threat class | Representative vectors | Expected fail-closed signal |
|---|---|---|
| Forged / grafted ZK proof | ADV-PROOF-01 | verification.valid: false |
| Malformed public signals | ADV-PROOF-02/03 | Binding and/or ZK fails |
| Signature tamper | ADV-SIG-01, ADV-METER-01 | Verify/attest reject |
| Replay / race | BV2-REPLAY-01/02/03 | HTTP 400 or single-winner race |
| Fingerprint / commitment swap | BV2-TAMPER-01, BV2-INCIRCUIT-02 | Billing / in-circuit check false |
| Transparency forgery | ADV-LOG-01/02 | log_proof_verification.valid: false |
| Revocation abuse | ADV-REVOC-01/02 | Strict revocation_status fails |
| Overflow / DoS payload | ADV-CHARGE-01, ADV-PAYLOAD-01 | HTTP ≥ 400 |
| Artifact substitution | BV2-ART-01 | Boot validator reject |
Full narrative VDI threat model: security-model.md. Billing operationalization: formal-security-audit.md.
3. Assumptions
3.1 Cryptographic
| Assumption | Use in product |
|---|---|
| Ed25519 EUF-CMA | Attestation, meter envelope, transparency operator signatures |
| Groth16 knowledge-soundness (bn128) | Attestation ZK + Phase-2 apiBillingV2 |
| SHA-256 collision resistance | Digests, field-images, fingerprints |
| Poseidon (circomlib) collision / PRF-like binding | Phase-2 commitment digest |
| Correct key custody | Compromise of VDI_SIGNING_KEY or meter key enables issuance forgery — out of protocol soundness |
3.2 Encoding / governance
| Assumption | Implication |
|---|---|
Field-images are computed off-circuit (SHA-256 → mod p) | Circuit proves Poseidon(field-images); not UTF-8 preimage knowledge |
| Manifest / tariff authoring is honest to intent | Wrong tariff still proves; it does not prove legal or commercial correctness |
| Verification profile inputs supplied when required | Strict profile needs revocation + authority binding data |
3.3 Operational (disclosed)
| Assumption | Status |
|---|---|
| Phase-2 ceremony contributors honest | Pilot-grade: 3 contributors, single-host ceremony — not adversarial multi-host MPC |
| Artifact mirrors identical | Boot pin checks ARTIFACT_MANIFEST.json |
| Meter trust anchors configured | Untrusted kid rejected (BV2-METER-02) |
| PostgreSQL available for replay + transparency | Production requirement for v2 |
4. Unsupported cases / out of scope
4.1 Explicit out of scope for this Halborn engagement
| Area | Why |
|---|---|
| Landing / marketing UI | Not part of billing trust surface |
Legacy api-billing-v1 | Deprecated; pilot is v2 only |
Identity / captcha circuits (proof_of_identity, adaptive ML) | Separate product |
| Redis / rate-limit hardening | CI adversarial runs with Redis disabled |
| Stripe / PSP capture | We prove charge relation, not payment settlement |
| Formal SOC2 / prior third-party audit claims | This package scopes the review; it is not the audit letter |
| Independent-host adversarial MPC | Documented limitation; path exists but not completed |
causalProof ceremony for identity pipelines | Billing Phase-2 uses apiBillingV2 only |
| Legal interpretation of tariffs / fair-lending manifests | Proofs encode relations, not statutes |
4.2 What we do not claim
| Claim | Reality |
|---|---|
| “Mathematical certainty of legal compliance” | Only that encoded checks passed under stated assumptions |
| “Impossible to bill incorrectly” | Bad meter input or wrong authored tariff is outside the relation |
| “MPC eliminates all setup risk” | Current ceremony is pilot-grade / single-machine |
| “QuantZK has been security audited” | This package supports independent review; it is not a completed third-party audit letter |
| “95% line coverage proves security” | Meaningful claim is behavioral: primary threat-model scenarios have executable tests |
| “Full RFC 8785 JCS conformance suite” | Implementation is JCS-aligned + property-tested; not a formal JCS certificate |
See also: Trust surface scope.
5. Circuit review
5.1 Inventory (in-scope circuit)
| Item | Value |
|---|---|
| Circuit ID | apiBillingV2 |
| Source | zk-cp/circuits/apiBillingV2.circom |
| Template | ApiBillingV2 |
| Binding version | bn128-poseidon8-v1 |
| Proof system | Groth16 / bn128 |
| Constraints | 402 non-linear (manifest) |
| Public inputs | 1 — commitment_digest |
| Private inputs | 8 field elements |
| Artifacts | verifier-api/circuits/apiBillingV2/ (+ mirrors) |
| Prover/verify | protocol/packages/vdi-billing/commitmentBindingV2.js |
| Pins | ARTIFACT_MANIFEST.json + bash scripts/verify-artifact-hashes.sh |
5.2 Relation (what the circuit actually proves)
[ \texttt{commitment_digest} = \mathrm{Poseidon}_8(w_0,\ldots,w_7) ]
with commitment_digest public and (w_i) private. Witness field-images are built off-chain by deriveFieldImages(publicCommitments):
| Index | public_commitments field | Circuit signal name |
|---|---|---|
| 0 | event_id | event_id |
| 1 | tenant_id | tenant_id |
| 2 | api_key_id (fallback meter_signing_kid) | api_key_id |
| 3 | endpoint (fallback evaluator_digest) | endpoint |
| 4 | billing_window_id | billing_window_id |
| 5 | tariff_id | tariff_id |
| 6 | usage_units | usage_units |
| 7 | expected_charge_micros | expected_charge_micros |
Intentional non-goal: The circuit does not prove knowledge of UTF-8 preimages. Preimage integrity for dispute fields is carried by the Ed25519-wrapped attestation and SHA-256 fingerprints / Phase-1 field split. Phase-2 prevents substituting a commitment digest without knowing field-images that Poseidon to that digest.
5.3 Reviewer checklist
- Confirm Poseidon input order matches
deriveFieldImages(order is binding-versioned). - Confirm Groth16 verify + semantic
public_signals[0] === Poseidon8(expected)inverifyInCircuitBillingProof. - Confirm issuer cannot attach a valid Phase-2 proof for commitments that disagree with the fingerprint (BV2-INCIRCUIT-02).
- Confirm silent artifact swap fails boot validation (BV2-ART-01).
- Confirm ceremony honesty caveat before adversarial trust (trusted setup).
5.4 Out-of-scope circuits for this packet
fairLending, hipaaAccess, euAiAct, soc2Access, causalProof, proof_of_identity — see audit-circuit-coverage.md if Track B is opened.
6. Parser review
6.1 Surfaces that parse untrusted input
| Surface | Parser / normalizer | Fail-closed behavior |
|---|---|---|
| HTTP JSON body | Express json (~10mb limit) | 413 oversize (ADV-PAYLOAD-01) |
| Meter + tariff | normalizeV2MeterEvent / normalizeV2TariffSnapshot / toInteger | Missing/non-integer → 400 |
| Charge math | computeChargeMicrosDeterministic | Unsafe int / mul overflow throw |
| Meter envelope | verifyMeterEventEnvelope | Digest/sig length/kid fail → 400 |
| Attestation / proof | @quantzk/vdi-verifier + snarkjs | Invalid proof/sig → verification.valid: false |
| Commitment limbs | digestToPublicFieldElements + binding verify | Wrong length / swapped limbs fail |
| Transparency proof | Merkle inclusion + entry hash vs receipt | ADV-LOG-01/02 |
| Revocation snapshot | Inline or env feed into strict profile | ADV-REVOC-01/02 |
6.2 Accepted vs rejected (summary)
| Input class | Accept | Reject |
|---|---|---|
| Integers in charge path | Safe integers in range | Non-integer, overflow product |
| Meter signature | 64-byte Ed25519 hex | Wrong length, bad kid, digest≠canon(event) |
Proof public_signals (Phase-1) | Length 2 matching field split | Truncation / limb swap |
Phase-2 billing_proof | Matching Poseidon digest | Commitment substitution |
| JSON key order | Any order (canonicalized) | N/A — reorder must not change digest |
NaN / Infinity / BigInt in canon | — | Throw (ADV-CANON-02) |
6.3 Known residual risks (disclosed)
- Env revocation feed clamps
snapshotTimeup tonowinnormalizeSnapshot— stale-cache semantics for auditors should use inlinerevocationon verify (exercised by ADV-REVOC-02). - Protocol tests historically had a simplified
canonicalizehelper inprotocol/test/helpers.js; production SoT isprotocol/lib/canonicalize.js— do not treat the helper as normative. - Billing path is JavaScript-centric; cross-language verify packs exist for generic VDI, not a full billing-bundle multi-language suite.
7. Canonicalization
7.1 Source of truth
protocol/lib/canonicalize.js — shared by prover, verifier, meter signer, commitments, transparency receipt hashing.
Normative framing: VDI-SPEC § Canonical Payload (RFC 8785 / JCS-aligned).
7.2 Invariants (property-tested)
| ID | Invariant | Test |
|---|---|---|
| ADV-CANON-01 | Object key order does not affect canonical bytes | Offline adversarial |
| ADV-CANON-02 | Non-finite numbers rejected | Offline |
| ADV-CANON-03 | -0 normalizes to 0 | Offline |
| Meter resign | Reordered meter event → same digest | Offline |
| Production pin | Canonical vkey hash = smoke billing_proof.vkey_hash | Artifact / smoke |
7.3 Where canonicalization binds trust
| Use | What is hashed / signed |
|---|---|
| Attestation Ed25519 | Canonical payload with signature.value null |
| Meter envelope | Canonical event → digest + signature |
| Public commitments digest | Canonical commitments object |
| Transparency receipt | Canonical receipt hash for Merkle entry |
| Verification key pin | Canonical JSON of vkey → vkey_hash |
7.4 Honesty bar
This is an engineering property suite, not a mathematical “proof” of full JCS equivalence across all Unicode edge cases. Auditors should treat ADV-CANON-* + call-site usage as the acceptance criteria for this engagement unless a deeper JCS conformance suite is contracted.
Reproduce:
cd protocol && node --test test/adversarial-billing-v2.test.js8. Trust boundaries
8.1 Who must trust what
(Same boundary model as Architecture Diagram 6.)
8.2 In-circuit vs off-circuit (critical)
| Fact | Bound how? | Notes |
|---|---|---|
| Poseidon8(field-images) | In-circuit (Phase-2, opt-in) | apiBillingV2 |
| SHA-256 field-image preimages | Off-circuit + Ed25519 wrap | Circuit does not see UTF-8 |
| Charge arithmetic | Deterministic evaluator + fingerprint | Not a circuit witness today |
| Replay uniqueness | PostgreSQL unique constraint | Operational integrity |
| Revocation | Profile + snapshot input | Verifier fails if present+revoked |
Full table: vdi-cryptographic-binding-model.md.
8.3 Party map
| Party | Trust boundary |
|---|---|
| Customer | Must be able to verify without QuantZK uptime using saved bundle |
| Meter operator | Signs usage; must be in trust anchors |
| QuantZK issuer | Signs attestation; key compromise = forgery |
| Transparency operator | Signs log entries / checkpoints |
| Ceremony contributors | Pilot setup honesty; rotate before adversarial threat model |
| Halborn / auditor | Verifies gates offline; no need to trust marketing |
Reproduce (one command)
# Formal gates (artifacts + conformance + pilot + adversarial)
bash scripts/run-formal-security-audit.sh
# Optional coverage snapshot for attachment
bash scripts/halborn-coverage-report.sh
# Optional scale methodology sample (local API must be up)
npm run audit:scale -- --total 100Suggested Halborn findings format
| Severity | Examples |
|---|---|
| Critical | Proof forgery path; replay bypass; key/material leak |
| High | Binding mismatch accepted; artifact pin bypass |
| Medium | Stale revocation defaults; DoS wedges |
| Low / Info | Docs drift; ceremony maturity; coverage gaps |
Scope ack + numbered answers to trust surface questions remain in §4 of the base packet.
Contact: Omar@quantzk.com · security@quantzk.com