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
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

Faster Sumchecks: Part I

In this blog post, we explore how to optimize the sumcheck protocol, particularly when working with values in a small field and randomness from a large field, as often needed in zkVMs. We introduce various algorithms aimed at reducing expensive operations, focusing on minimizing large multiplications. Starting from using simple evaluation tables to more sophisticated techniques like precomputing accumulators and leveraging Lagrange interpolation, we demonstrate how to efficiently organize computations to speed up proving times. Readers will gain insights into handling arithmetic operations within the sumcheck protocol and learn about optimizing specific cases in zero-knowledge proofs.

Jason Park · November 21, 2025

Sum-Check as an Algebraic Tensor Reduction: Part III

This post is all about the maps that let us move between modules without breaking their structure. We’ll see when a map is truly “linear,” when two modules are (secretly) the same, and why two-input maps deserve special attention. Along the way, (bi-)linear maps and isomorphisms become less like abstract definitions and more like tools we can actually use. By the end, we’ll have all the tooling we need to tackle abstract tensor products head-on.

Marco Besier · May 18, 2026

Breaking Down Bulletproofs: No Pairings, No Trusted Setup

Learn how Bulletproofs enables efficient zero-knowledge proofs without trusted setups by computing inner products in a verifiable way. This post breaks down the core folding technique that reduces large vectors to single elements through recursive compression, making proofs both compact and fast to verify. Used in Monero, Mina's Kimchi, and Zcash's Halo 2, Bulletproofs is a practical alternative to pairing-based schemes.

David Wong · October 23, 2025