ZK/SEC Research notes from zkSecurity
All posts
cryptography · algebra · soundness

Powers-of-Funbenius

Thumbnail image

Introduction

In this post we just want to cover a fun bug we found: fun because the math itself is interesting, and fun because it breaks just the right way. The bug is issue #44 in Inferno, which is a Rust implementation of the Limbo MPC-in-the-head zero-knowledge argument, which is an improvement upon the KKW scheme. The bug in the implementation is one character long, surprisingly common, usually not game ending, but over binary extension fields everything breaks in just the right way...

Limbo

Limbo proves satisfiability of an arithmetic circuit $C$ over any field $\mathbb{F}_p$, usually, applied to small fields, as in Inferno, $\mathbb{F}_p = \mathbb{F}_2$. So every wire carries a binary value, addition is XOR and multiplication is bitwise AND. The advantage is that you don't pay "embedding into a large field for soundness"-overhead for each of the bits you want to operate on, which means very good concrete computational and communication costs. The "disadvantage" of Limbo is that of classical MPC-in-the-head: communication/verifier cost is linear.

The way that things work in Limbo is that the prover commits to every wire value of $C$ evaluated on $w$ via additive secret sharings between $n$ virtual MPC parties, run "in the prover's head"; the verifier later opens a subset of the parties' views and checks consistency.

Linear gates (addition, scalar multiplication) act locally on shares, so the parties evaluate them for free with no additional commitments. Multiplication gates are the hard part: shares of $x_\ell$ and $y_\ell$ do not combine locally into a sharing of $x_\ell \cdot y_\ell$. So for every multiplication gate $\ell \in [m]$ the prover additionally commits to a sharing of the claimed output $z_\ell$, and the verifier has to check that the prover did not lie:

$$ \forall \ell \in [m].\ z_\ell = x_\ell \cdot y_\ell $$

Where $x_\ell, y_\ell$ are the input wires to the $\ell$-th multiplication gate (themselves linear combinations of earlier wires, hence already shared) and $z_\ell$ is the freshly committed claim. Every multiplication gate contributes a gate error:

$$ e_\ell := x_\ell y_\ell - z_\ell \in \mathbb{F}_p $$

The prover is honest iff every $e_\ell = 0$. Checking each gate individually is expensive, so Limbo collapses all $m$ gate errors into a single check. The errors live in $\mathbb{F}_p$, but the verifier picks a challenge $r \in \mathbb{F}_q$ from a large extension field $\mathbb{F}_q \supseteq \mathbb{F}_p$, in Inferno we have $\mathbb{F}_q = \mathbb{F}_{2^{64}}$, and asks the prover to convince him that:

$$ f(r) := \sum_{\ell = 1}^{m} e_\ell \cdot r^\ell = 0 $$

The errors $e_\ell$ become the coefficients of a polynomial $f(X) \in \mathbb{F}_p[X]$, and $r$ is a uniformly random evaluation point in $\mathbb{F}_q$. If the prover is honest, $f$ is the zero polynomial and $f(r) = 0$ trivially. If even one $e_\ell$ is non-zero, $f$ is a non-zero polynomial of degree at most $m$, so by Schwartz-Zippel it vanishes at $r$ with probability at most $m / |\mathbb{F}_q|$. This is Π-MultCheck from Limbo, §4.1, and the rest of the protocol is built on top of it.

Note: the field $\mathbb{F}_{2^{64}}$ in Inferno is not large enough for computational soundness, this is solved by simply repeating the check multiple times in parallel when compiling the protocol with Fiat-Shamir.

The Code

Here is the relevant snippet of round.rs which implements the evaluation of $f(r)$:

pub(crate) fn round1<S: LinearSharing<F, N>, F: FiniteField, const N: usize>(
    round0: Round<S::SelfWithPrimeField>,
    mults: &[S::SelfWithPrimeField],
    challenge: F,
) -> Round<S> {
    let mut sum = S::default();
    let mut xs = vec![S::default(); round0.xs.len()];
    let mut ys = vec![S::default(); round0.ys.len()];
    let mut r = challenge;
    for (i, ((x, y), z)) in round0
        .xs
        .iter()
        .zip(round0.ys.iter())
        .zip(mults.iter())
        .enumerate()
    {
        sum += S::multiply_by_superfield(z, r);
        xs[i] = S::multiply_by_superfield(x, r);
        ys[i] = S::lift_into_superfield(y);
        r *= r;
    }
    Round { xs, ys, z: Some(sum) }
}

The intent is for r to take the values $r, r^2, r^3, \ldots, r^m$, the intention is to compute:

$$ \begin{align} \mathsf{sum} &= \sum_i r^i \cdot z_i \\ \mathsf{xs}_i &= r_i \cdot x_i \\ \mathsf{ys}_i &= y_i \end{align} $$

The triple $(\mathsf{xs}, \mathsf{ys}, \mathsf{sum})$ is the inner-product instance that the rest of the protocol verifies: downstream the verifier checks that $\langle \mathsf{xs}, \mathsf{ys} \rangle = \mathsf{sum}$. With the intended values, completeness is automatic when the prover is honest ($z_i = x_i y_i$). Soundness reduces to evaluating $f$ at $r$:

$$ \begin{align} \langle \mathsf{xs}, \mathsf{ys} \rangle - \mathsf{sum} &= \langle \vec{r} \circ \vec{x}, \vec{y} \rangle - \mathsf{sum} \\ &= \sum_i r^i \cdot x_i y_i - \sum_i r^i \cdot z_i \\ &= \sum_i r^i \cdot (x_i y_i - z_i) \\ &= \sum_i r^i \cdot e_i = f(r) \end{align} $$

So checking $\langle \mathsf{xs}, \mathsf{ys} \rangle = \mathsf{sum}$ is exactly checking $f(r) = 0$.

The Bug

The problem is that, instead of r *= challenge, the code uses r *= r, maybe you already spotted this. This is repeated squaring, not successive powers, so r actually takes the values: $r, r^2, r^4, r^8, \ldots, r^{2^{m-1}}$ and the check the verifier ends up performing is therefore:

$$ f(r) := \sum_{i=0}^{m-1} e_i \cdot r^{2^i} = 0 $$

Where $e_i = x_i y_i - z_i$ is the error at multiplication gate $i$.

Observe that $f(r)$ does not have degree $m-1$, but instead has degree $2^{m-1}$; which is huge! So the usual soundness argument, based on the Schwartz–Zippel lemma:

$$ f(X) \neq 0 \implies \mathbb{P}_{r}\left[ f(r) = 0 \right] \leq \frac{\deg(f)}{|\mathbb{F}_q|} $$

Yields nothing when $m \geq 64$, in which case the right side is greater than $1$ for Inferno because $\mathbb{F}_q = \mathbb{F}_{2^{64}}$. Okay, so theoretically broken, but is this just a proof gap? It turns out no, to see why, we need to look at the Frobenius endomorphism...

The Frobenius Endomorphism

The Frobenius endomorphism on $\mathbb{F}_{2^k}$ is the map:

$$ \phi: \mathbb{F}_{2^k} \to \mathbb{F}_{2^k},\quad \phi(x) = x^2 $$

Its $i$-th power is repeated squaring, which is the same as raising to the $2^i$-th power:

$$ \phi^i(x) = \underbrace{\phi(\phi(\ldots(x)\ldots))}_{i\text{ times}} = x^{2^i} $$

Linearity

Observe that $\phi$ is $\mathbb{F}_2$-linear, because of the "Freshman's dream":

$$ \phi(a + b) = (a + b)^2 = a^2 + 2ab + b^2 = a^2 + b^2 = \phi(a) + \phi(b) $$

Because $2 = 0$ in characteristic 2, and multiplication by scalars in $\mathbb{F}_2$ also works:

$$ \phi(0 \cdot a) = 0 = 0 \cdot \phi(a),\quad \phi(1 \cdot a) = \phi(a) = 1 \cdot \phi(a) $$

Composition of $\mathbb{F}_2$ linear maps is also $\mathbb{F}_2$-linear, so every power $\phi^i$ is also linear. Furthermore, any linear combination of linear maps is of course also linear, so:

$$ X \mapsto \sum_i e_i \cdot \phi^i(X) = \sum_i \phi^i(e_i \cdot X) = \sum e_i \cdot X^{2^i} $$

Where $e \in \mathbb{F}_2$ is also a linear map from $\mathbb{F}_q$ to $\mathbb{F}_q$.

Periodicity

Finally, on $\mathbb{F}_{2^k}$ we have $\phi^k = \mathrm{id}$, because for every element of $x \in \mathbb{F}_{2^k}$:

$$ x^{2^k-1} = 1 \implies x^{2^k} = x \implies \phi^k(x) = x $$

Hence:

$$ \phi^i = \phi^{i \bmod k} $$

Only $k$ distinct powers exist as functions $\mathbb{F}_{2^k} \to \mathbb{F}_{2^k}$.

The Exploit

All of this spells doom...

The obvious issue is that $f(r)$ is a combination of these powers-of-Frobenius, so if e.g.

$$ f(r) = \sum_{i=0}^{64} e_i \cdot r^{2^i} $$

Then $\vec{e} = (0, 0, \ldots, 0)$ and $\vec{e} = (1, 0, 0, \ldots, -1)$ have the same evaluation for every $r$ since: $x = \phi^{64}(x)$ so $r - \phi^{64}(r) = 0$ for every $r$. Observe that $-1 = 1$ in $\mathbb{F}_2$ and the simplest attack is therefore to simply "flip" the results of the two multiplications: pick any two multiplication gates with indices $a \neq b$ but such that $a \equiv b \pmod{64}$, and set both errors to $1$:

$$ f(r) = \phi^a(r) + \phi^b(r) = \phi^{a \bmod 64}(r) + \phi^{b \bmod 64}(r) = 0 $$

All this requires is a circuit with more than $64$ multiplication gates, which is pretty certain to be the case, not many useful circuits with less than $65$ multiplications...

However the curious reader might wonder if this could be exploited with fewer than $65$ gates. The answer is yes, partially. If we view $r \in \mathbb{F}_{2^{64}}$ as a vector in a $64$-dimensional $\mathbb{F}_2$-vector space, the attack works whenever:

$$ r \in \ker(f_{e}) $$

Where $f_e$ is the linear map:

$$ r \mapsto \sum_i e_i \cdot \phi^i(r) $$

The acceptance probability for this error vector is:

$$ \frac{|\ker(f_e)|}{|\mathbb{F}_{2^{64}}|} = 2^{\dim_{\mathbb{F}_2}(\ker(f_e)) - 64} $$

For the attack we only need to exhibit an error vector with a large kernel. Let:

$$ N = \phi + \mathrm{id} $$

This is the map $N(r) = r^2 + r$. Since $\phi^{64} = \mathrm{id}$ on $\mathbb{F}_{2^{64}}$, we have:

$$ N^{64} = (\phi + \mathrm{id})^{64} = \phi^{64} + \mathrm{id} = 0 $$

Where we used the Freshman's dream for commuting maps in characteristic $2$. Also:

$$ \ker(N) = \{ r \in \mathbb{F}_{2^{64}} : r^2 + r = 0 \} = \mathbb{F}_2 $$

So $\dim_{\mathbb{F}_2}\ker(N) = 1$. Now consider the kernels obtained by successively applying $N$:

$$ \{0\} = \ker(N^0) \subseteq \ker(N) \subseteq \ker(N^2) \subseteq \cdots \subseteq \ker(N^{64}) = \mathbb{F}_{2^{64}} $$

Each step can add at most one dimension. Indeed, modulo $\ker(N^j)$, the only new information in $r \in \ker(N^{j + 1})$ is $N^j r$, and this lies in the one-dimensional space $\ker(N)$. But the chain starts at dimension $0$ and ends at dimension $64$, so every step adds exactly one dimension to the kernel:

$$ \dim_{\mathbb{F}_2}\ker(N^t) = \dim_{\mathbb{F}_2}\ker(N^{t - 1}) + 1 = t $$

Now choose the gate errors so that the broken check is exactly $N^t$. Expanding $N^t$ gives:

$$ N^t = (\phi + \mathrm{id})^t = \sum_{i=0}^t \binom{t}{i}\phi^i = \sum_{i=0}^t e_i \phi^i,\quad e_i = \binom{t}{i} \bmod 2 $$

Set the error at gate $i$ to this coefficient $e_i$. Then:

$$ f_e(r) = \sum_{i=0}^t e_i \phi^i(r) = N^t(r) $$

Hence $\dim_{\mathbb{F}_2}\ker(f_e) = t$, and the verifier accepts this error vector with probability $2^{t - 64}$. For $t = 32$, the Freshman's dream gives $N^{32} = \phi^{32} + \mathrm{id}$, so we only need errors at gates $0$ and $32$. This is a circuit with $33$ multiplication gates. The intended check would have accepted with probability around $33/2^{64}$, the broken check accepts with probability $2^{-32}$.

Keep reading
Latest

Optimizing Cryptography with AI

Many of us are using AI to generate code. Vibe coding cryptography is especially sensitive - you have to uphold strict mathematical correctness. This can lead to wrong security guarantees and soundness bugs. We will discuss what are some patterns to do it well.

Kobi Gurkan · August 11, 2026

Introducing zkvmBlast: Differential Fuzzing for Ethereum's zkVMs

zkVMs are moving to the center of Ethereum's roadmap, which means a bug in a zkVM is turning into a bug in Ethereum itself. We built zkvmBlast, a zkVM-agnostic differential fuzzer that runs the same program across SP1, RISC0, OpenVM, Pico, Zisk, and Airbender against a reference simulator and flags any disagreement. It hunts for both soundness and completeness bugs, with a deliberate focus on completeness, an under-explored class that can turn a single valid block into a liveness failure. We share the first batch of findings.

Stefanos Chaliasos, Martín Ochoa, Varun Thakore · August 10, 2026

Circom-Auditor: Open-Source Skills for Finding Vulnerabilities in Circom Code

We are releasing zk-skills, a set of open-source security skills for AI coding agents, starting with circom-auditor: a first line of defense against vulnerabilities in Circom circuits, compatible with both Claude Code and Codex. On the zkbugs benchmark it detects up to 66 of 70 known bugs when pointed at the vulnerable circuits, and up to 40 of 56 when let loose on the full original codebases, far ahead of existing Circom security tools.

Stefanos Chaliasos, Hao Pham, False Witness Team · August 05, 2026
Recommended

Soundness Failures in LaBRADOR Implementations from NTT -Friendly Rings

Post-quantum cryptography is making its way into production libraries, and correct implementation is far from trivial. We reviewed several LaBRADOR implementations on GitHub and found three of them broken, with soundness collapsing as far as a single bit, because of parameter choices that look perfectly reasonable in many lattice-based protocols; a power-of-2 modulus, a composite modulus, or NTT-friendly rings for efficient ring multiplication. The post goes through how each of those choices undermines the protocol's soundness argument, and why NTT-friendliness, of all things, turns out to be the wrong instinct if not handled carefully.

Georgios Raikos · April 30, 2026

Uncovering the Query Collision Bug in Halo2: How a Single Extra Query Breaks Soundness

We recently discovered a subtle but important soundness issue in Halo2, which we’ve named the query collision bug. It affects certain edge-case circuits and was present in widely used versions, including the main Zcash implementation and PSE’s fork. We disclosed the issue to the relevant teams, including Zcash, PSE, and Axiom, all of whom have since patched it. While no known production circuits were affected, the bug reveals a surprising vulnerability in the proving system that deserves attention.

Suneal Gong · July 09, 2025

Uncovering the Phantom Challenge Soundness Bug in Solana's ZK ElGamal Proof Program

In June 2025, we uncovered a serious soundness issue in Solana's ZK ElGamal Proof Program that could let attackers manipulate confidential token transfers undetected. We worked with the Anza team to quickly address the flaw by pausing and disabling vulnerable components. This post dives into the root cause, which was a subtle mistake in handling prover-generated challenges within sigma OR proofs, revealing broader lessons in zero-knowledge protocol security. If you're interested in cryptographic protocol design, this could provide valuable insights.

Suneal Gong · June 26, 2025
More to explore

zkSecurity partners with ZPrize to make you win hundreds of thousands of dollars!

We're gearing up for this year's ZPrize competition, where we'll be hosting the High Throughput Signature Verification category. This challenge is all about creating the most efficient signature verification circuit using Aleo's Varuna proof system. Participants will work with ECDSA on the Bitcoin and Ethereum curve and the Ethereum hash function, keccak256. It's a great chance to dive into some of the hottest problems in arithmetic circuits and optimize cryptographic algorithms. If you're curious about pushing the boundaries in ZK, join us and share your feedback on our prize specification through our Discord channel.

ZK/SEC · August 27, 2023

Comparison of formal verification frameworks for arithmetic circuits

A hands-on comparison of formal verification frameworks for arithmetic circuits, evaluating those in the ACL2 Book (r1cs, PFCS), acl2-jolt, Garden (Rocq), zk-lean, sp1-lean, and Clean. Each framework is tested on reproducibility, available examples (from basic field elements to RISC-V VM instructions), and practical verification tasks including the IsZero and weighted-sum circuits. The evaluation includes both human and Claude Code's ability to work with each framework, revealing insights about installation difficulty, proof automation capabilities, and the maturity of publicly available examples. This post maps the current landscape of formally verified ZK circuits and discusses what's coming next in this rapidly evolving field.

Yoichi Hirai · November 19, 2025

Threshold ECDSA: Building CGGMP from scratch

A step-by-step build of CGGMP, an n-of-n threshold ECDSA scheme where parties jointly produce a signature without ever reconstructing the private key. We start from the multiplicative-to-additive (MtA) protocol and a semi-honest version of the signing protocol, then harden it into a maliciously secure one by layering in zero-knowledge proofs at each step. Along the way we cover the auxiliary Ring-Pedersen and Paillier parameters and the proofs that make them safe to use.

Samuel Tang · July 27, 2026