ZisK: a missing sign constraint in signed remainder
ZisK's arithmetic circuit checked the magnitude of a signed remainder without fully constraining its sign. For a negative dividend, the checked relations allowed a nonzero remainder to be encoded as positive. For example, REM(-7, 3) should return -1; the reported assignment encodes +1.
The ZisK team accepted the report as Critical and confirmed that PR #1228 had already fixed it. The patch closed both this remainder-sign finding and Cody Gunton's independently reported quotient-sign flaw. The PR now credits both reports.
Affected revision: 6182c8be · Fix: 683e6d9 · Patched version listed by the advisory: 1.1.0-alpha
Validation scope: this report checked the relevant constraints, lookup-table membership and witness-code components. It did not generate an end-to-end forged proof or demonstrate an exploit against a deployed application.
Why the sign matters
A zero-knowledge virtual machine lets a verifier check a program's execution without rerunning it. Its constraints must therefore distinguish the correct computation from an incorrect one.
For ordinary signed division, RISC-V rounds the quotient toward zero. A nonzero remainder must have the dividend's sign, and its magnitude must be smaller than the divisor's. Thus:
-7 = 3 × (-2) + (-1)Checking only the magnitudes gives 7 = 3 × 2 + 1. That equation cannot distinguish a remainder of -1 from +1. The circuit must also bind the output sign.
Where the constraint was missing
At the affected revision, arith.pil represented signs with four boolean flags: na for the quotient, nb for the divisor, np for the dividend and nr for the remainder. The lookup-table generator rejected invalid combinations.
The table required np == nr in the division-by-zero case:
// arith_table.pil:150, at 6182c8be
if (div_by_zero && (!div || nb || np != nr || signed != na)) continue;On the ordinary signed path, its sign filter was weaker:
// arith_table.pil:163
if (!np & nr) continue;This enforces nr <= np. A non-negative dividend forces nr = 0, but a negative dividend permits either sign.
Allowing both signs is necessary for one case: exact division. For -6 / 3, the remainder is zero, so its negative flag must be clear. The missing constraint was the distinction between zero and positive. Nothing required the remainder to be zero when a negative dividend was paired with nr = 0.
The candidate witness
For REM(-7, 3), the report examined this assignment:
div = 1, signed = 1, div_by_zero = 0
na = 1, nb = 0, np = 1, nr = 0
|quotient| = 2, |remainder| = 1The magnitude identity holds (2 × 3 + 1 = 7), the remainder bound holds (1 < 3), and the lookup table accepts the flags. With nr = 0, the output-sign selector encodes +1 rather than -1.
The report also replayed table membership and chunk range checks against the project's witness code. It did not independently solve all chunked two's-complement identities in arith.pil:131–209 or run the complete proving pipeline. Those limits distinguish the evidence presented here from an end-to-end proof forgery.
The flaw concerns signed REM and REMW with a negative dividend and nonzero remainder. An incorrect sign could change a guest program's subsequent arithmetic or control flow. The vendor rated the soundness finding Critical; this report does not establish exploitation of any deployed application.
How the fix handles zero
On July 27, Cody Gunton published a working malicious witness for a related quotient-sign flaw: DIV(1, -1) could be represented as +1. ZisK opened PR #1228 on July 29, crediting his report, and merged it on July 30. The fix closed the remainder-sign issue as well.
Commit 683e6d9 introduces result_is_zero and remainder_is_zero, ties those flags to the corresponding values, and distinguishes a negative remainder from zero:
// arith.pil
remainder_is_zero * div * sum_all_ds === 0;
// arith_table.pil
if (neg_dividend == 1 && remainder_is_zero == 0 && neg_remainder != 1) continue;
if (neg_dividend == 1 && remainder_is_zero == 1 && neg_remainder != 0) continue;The original report proposed requiring the dividend and remainder signs to match directly. That proposal was too strict: it would reject valid exact divisions with a negative dividend and zero remainder. The shipped fix handles both cases correctly.
The fix commit is included in v1.1.0-alpha and v1.2.0-alpha. The vendor advisory identifies 1.1.0-alpha as the patched version.
Disclosure timeline
- June 5, 2026: identified and checked at
6182c8be. - June 6: reported privately by email and GitHub Security Advisory, with a proposed 90-day disclosure window.
- July 27: Cody Gunton published the related quotient-sign finding.
- July 29–30: ZisK opened and merged PR #1228, fixing both issues.
- August 18 and 26: releases
v1.1.0-alphaandv1.2.0-alphaincluded the fix. - September 17: ZisK accepted and published GHSA-qjgg-fcj3-p9x3 as Critical, confirming the existing fix. This was the first recorded response to this report. No CVE was assigned at publication.
- September 18: the PR description was updated to credit the independently reported remainder-sign finding alongside the quotient-sign report.
Correction to the original report
The advisory's reference to RISC Zero's CVE-2025-52484 was imprecise. That finding involved register confusion, not a missing remainder-sign constraint. It is a related example of incorrect execution being accepted, not the same mechanism. The clarification was sent to ZisK after the report.
Reported by Paul Jordan Anderson, Cerin Amroth Research. Contact: jordan@cerinamroth.com. The disclosure was unconditional; no bounty program covered this report.