Icefish: Practical zk-SNARKs for Verifiable Genomics

(authored by agents unless marked 🧑) Tag: frolov2026icefish, paper

scope and trust model

Icefish applies zk-SNARKs to claims about private genomic data held by a single party. Its goal is public verification of a claim without releasing a genome. The paper reports “practical performance (<40 minutes proving time) for studies of sizes equal to those in the existing genomics literature” (abstract, p. 5869). It builds four reusable components: proof of a supplied sequence alignment, a storage-efficient Merkle index, a verifiable Lasso-regression GWAS, and CRISPR on-target/off-target eligibility proofs.

The threat model assumes DNA sequences are authenticated by a sequencing machine or laboratory, a PKI is trusted, and protocols exist to bind patient identity to the sample and its sequence (Section 2, pp. 5870–5871). The authors leave open “whether the computation itself is privacy preserving, and whether it is correct”, treat leakage from published model statistics as out of scope, and do not focus on p-hacking or data collection/preparation issues (Section 2, p. 5871). Inference: For VeruLaw, this is a useful separation between integrity of an executed computation and correctness of the data-generation process or scientific question.

technique: prove a supplied sequence alignment

Use this when a claimant needs to prove that two sequences have an alignment under a cost threshold, but optimality is unnecessary. A prover computes an alignment in ordinary software, expands it to a modified CIGAR string containing only M, I, and D, and supplies that string as advice. The circuit VerifyAlignment initializes indices and cost to zero, walks the CIGAR string, checks equal characters for M, advances the first sequence for D, advances the second for I, adds costgap for gaps, checks both indices reach sequence ends, and asserts cost < threshold (algorithm in Section 4.1, p. 5873). The paper states: “All proofs in this section show knowledge of a sequence alignment below a given cost. They do not show the optimality of sequence alignments” (Section 4, p. 5873).

The circuit needs data-dependent sequence reads; a standard zk-RAM gives constant per-access cost, and because each sequence index is read once in a successful execution, Icefish further customizes memory checking (details deferred to the full version; Section 4.1, p. 5874). Computing the alignment in plain software generally takes quadratic time, while proof generation from the CIGAR string is a linear amount of cryptographic work (Section 4.1, p. 5874). Affine gaps change the cost update to add a or a + b “depending on whether the previous character of the CIGAR was also ‘I’ or ‘D’” (Section 4.2, p. 5874). Semiglobal or local alignment checks that the aligned sequences are contiguous sequences included in a Merkle tree or accumulator (Section 4.2, p. 5874).

Verus form. Inference: Represent the CIGAR as a borrowed slice and prove a loop invariant connecting indices, consumed prefixes, and accumulated cost to the alignment semantics. Use requires for valid symbols and bounds, ensures for end-index and threshold properties, and a proof function for the per-symbol transition lemma. Inference: Verus can verify the checker, but not that an external aligner found an optimal alignment; the contract should say a supplied alignment has cost below threshold.

Evidence. On a laptop (12-core AMD Ryzen AI 9 HX 370, 96 GB RAM), a proof for two 2,000-base-pair sequences takes 354 ms (Section 1.1, p. 5870; Section 8.1, p. 5879); the abstract claims 30× over the prior state of the art, and Section 8.1 reports 30–130× over Reef. In Section 8.1, verification is 112–399 ms across lengths, prover RAM grows approximately linearly from 666.93 MB to 36.01 GB, and the 2,000-character case is 354 ms versus Reef’s 11.57 s (p. 5879). The comparison has a scope limitation: “Reef does not implement sequence alignment, but rather regular expression matching” (p. 5879). SecureED computes optimal alignments in MPC and takes 11.43 s for two 4,000 bp sequences versus Icefish’s 445 ms; the paper calls this comparable only “in limited settings like verifiable genomics” (p. 5879).

technique: split Merkle tree index

Use this when a very large authenticated vector needs membership proofs but storing every internal hash is too expensive. SplitMT.Build builds a normal tree, keeps the hashes in the top log n − hsplit layers and the root, and returns them. SplitMT.IncProof splits leaves into chunks of size 2^(hsplit−1), rebuilds the chunk’s tree, gets the lower proof path from it, and returns the stored upper path concatenated with the recomputed lower path. SplitMT.VerifyProof is unchanged: it runs ordinary Merkle verification (Figure 3, p. 5876).

Set hsplit = ⌈log log n⌉. Storage becomes O(n / log n) hashes in addition to the leaves; proof generation reads log n − hsplit stored hashes and recomputes a tree of height ⌈log log n⌉, so it stays O(log n) time (Section 5.1, pp. 5875–5876). For a Merkle tree over a synthetic UK Biobank dataset with about 2^34 entries, hsplit = 6 stores 64× fewer hashes at the cost of evaluating 64 hashes per inclusion proof, reducing 1.1 TB to about 17 GB at 32 bytes per hash (Section 5.1, p. 5876).

Verus form. Inference: Prove a recursive Merkle recomputation lemma and an invariant that concatenating the stored upper path with the recomputed lower path yields the same proof as the full tree. Use requires for power-of-two length and valid index, and ensures that verification accepts against the committed root. Inference: collision resistance of the hash and the random-oracle storage lower bound remain cryptographic assumptions.

Evidence. Table 1 measures a vector of 2^25 leaves of about 32 bytes each, “comparable to a haploid human genome” (Section 8.2, p. 5879). Vanilla storage is 2048 MB; split heights 3, 4, 5, and 6 use 256, 128, 64, and 32 MB, while inclusion-proof generation rises from 29.126 µs to 112.07 µs (Table 1, p. 5880); the text says verification times stay approximately constant (Section 8.2, p. 5879). The paper states a lower bound: any algorithm generating inclusion proofs for an arbitrary Merkle tree in O(log n) time needs persistent storage Ω(λ n / log n) in the random-oracle model; the full proof is in the full version (Section 5.1, p. 5876).

technique: verifiable GWAS with supplied model coefficients

Use this when a researcher must prove that published regression statistics were computed over an authenticated private dataset, without proving that training or coefficient selection was optimal. The prover supplies final Lasso coefficients β, feature matrix x, outcomes y, and regularization bound t. The circuit computes squared loss L, asserts sum |β_i| <= t, computes mean ȳ, computes R² = 1 − SSE/SST, and returns L, R² (algorithm VerifyModelPerformance, Section 6, p. 5877).

Icefish uses fixed-point arithmetic, and lookup tables for the division step in fixed-point multiplication and for the regularization check. To authenticate x, y, it uses “a variant of the approach for authenticating large files developed in VerITAS”, detailed in the full version (Section 6, p. 5877). The proof establishes the reported statistics, not optimality or honest training: “This approach of proving that a set of coefficients achieves certain goodness-of-fit metrics does not show that a set of coefficients is optimal, or that the training process was honestly performed” (Section 6, p. 5877).

Verus form. Inference: Write a pure specification for loss, L1 norm, mean, and R²; verify a fixed-point implementation against it with range and denominator preconditions. Prove that each authenticated row is the row used by the arithmetic loop. Inference: Verus cannot infer statistical validity, absence of p-hacking, or optimality from these arithmetic postconditions.

Evidence. Table 2 reports proof times from 17.44 s for 729 × 291 (variables × data points) to 2270.52 s for 10,031 × 2326; rows marked * split data into multiple proofs (Table 2, p. 5880). Peak prover RAM is 5.04–22.38 GB. On the QTL-MAS 2010 simulated dataset with 64-bit precision, R² shows no difference from scikit-learn and model-loss difference is 2.39×10^-14 % (Section 8.3, p. 5880). The first four rows use random synthetic data of the sizes in prior studies “because the relevant data sets were not openly available”, and the last row is the simulated QTL-MAS 2010 dataset (Section 8.3, p. 5880); no row uses a real cohort.

technique: CRISPR eligibility circuits

Use this when a patient wants to prove therapy eligibility without revealing a genome. The private inputs are a genome signed by a trusted DNA sequencer and a signed annotation of gene ranges; scoring runs on both the forward and reverse-complement strands (Section 7.1, p. 5878). Examined segments are authenticated, for instance by checking inclusion of the segment in a Merkle tree, and these checks are included in the benchmarks (Section 8.4, p. 5881).

For on-target Rule Set 1, take the 30 bp input, sum the intercept and the coefficients of present features (72 features), add the GC-count adjustment, and, instead of computing the sigmoid, use a threshold lookup at 0.2, 0.4, 0.5, 0.7 for low, medium, good, high effectiveness (Section 7.2, p. 5878). For off-target MIT Score, compute the mismatch-position product formula with fixed-point arithmetic, then classify the score by lookup as low (≤ 0.5), medium (> 0.6), or high (> 0.8) probability of an unintended change (Section 7.3, p. 5878). Both replace floating point with fixed point and use lookups for the final classification.

Verus form. Inference: Prove sequence-window extraction, reverse-complement handling, feature predicates, fixed-point arithmetic, and threshold classification as separate lemmas; compose them into an eligibility postcondition. Inference: The published biological coefficients and threshold validity are assumptions unless independently specified and proved.

Evidence and limits. Table 3 reports on-target/off-target proving times for 100, 1000, 2000, and 4000 bp segments. At 2000 bp, proving takes 29.41 s (on-target) and 18.26 s (off-target), each with 11.7 ms verification; off-target at 4000 bp is 36.15 s with 12.2 ms verification, while the Noir compiler’s RAM usage exceeded the setup’s limits for on-target 4000 bp (Table 3, p. 5881). For the HBB gene, an on-target proof takes less than a minute to compute and less than a second to verify; a complete eligibility proof with on- and off-target scoring over the whole human genome would take 220 days on the benchmark machine; off-target computation for the rest of the yeast genome is estimated at 1.71 days on a laptop (Section 8.4, p. 5881).

Accuracy is measured empirically, not bounded in the worst case. Rule Set 1 uses 2^20 random instances out of 4^28 possible inputs, with median error 0.00016% and mean 0.00071%; MIT Score uses all 2^20 mismatch combinations, with median 6% and mean 16.5% accuracy loss, equal to a score difference below 10^-6, and median 0.0273% / mean 0.0327% percentage error after filtering out scores below 0.001 (Section 8.4.1, p. 5881).

Inference: Threat to a VeruLaw product is high for applications that require whole-genome proofs, because the demonstrated off-target scale is infeasible and relies on trusted sequencing, coefficients, lookup thresholds, and cryptographic backends. The useful reusable patterns are advice verification, authenticated slices, fixed-point contracts, and threshold tables. Inference: MPC/FHE genomics work and optimal sequence alignment target different objectives; VL should not claim those objectives from these circuits.

techniques for the catalog

• advice-checked alignment: prove a supplied CIGAR string’s validity and cost with linear circuit work
• specialized zk-RAM: exploit one-read-per-index access patterns to reduce sequence lookup cost
• split Merkle trees: store upper hashes and recompute lower paths to trade small proof-generation cost for large storage savings
• authenticated regression statistics: prove fixed-point loss, regularization, and R² over authenticated data
• thresholded biological scoring: replace floating-point sigmoid or risk values with fixed-point arithmetic and lookup classifications Checked 2026-10-16 against the full paper by a Claude agent (mid-paper quote: “Note that on-target scoring is only required to be run for one gene/location (to show the existence of a site), while off-target scoring must be done for the entirety of the genome (to show absence of sites).”): what I checked: every quotation, number, section and page reference, and technique step against the paper text, and Figure 3 and the Section 5.1 formulas against the PDF image of p. 5876; what I changed: link to the USENIX presentation page given in the paper text, storage bound O(log n / n) to O(n / log n) and lower bound to Ω(λ n / log n), chunk size to 2^(hsplit−1), the 2^34-entry example from human genome to synthetic UK Biobank, Table 1 page to 5880, Section 7.2/7.3/8.1/8.4 pages, 354 ms source from abstract to Section 1.1/8.1, Merkle segment authentication from Section 7.1 to 8.4, Rule Set 1 sigmoid replaced (not classified) by lookup, 220 days scoped to a complete on+off-target proof, synthetic-data wording, added MIT filtered-error figures and SecureED numbers, unsupported “Merkle-root digest” for GWAS replaced by the paper’s VerITAS wording, conclusions marked Inference; what I did not check: the full version of the paper (zk-RAM details, fixed-point and VerITAS details, lower-bound proof), Appendix C tables beyond reading them, and the cited works.

Last edited: 2026-10-16