Skip to content

check intmul doesn't overflow modulo 2^128-1 #910

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
josephjohnston wants to merge 1 commit into from
Closed

check intmul doesn't overflow modulo 2^128-1 #910

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion crates/examples/snapshots/ethsign.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ ethsign circuit
--
Number of gates: 265672
Number of evaluation instructions: 311772
Number of AND constraints: 335708
Number of AND constraints: 361166
Number of MUL constraints: 25458
Length of value vec: 524288
Constants: 82
Expand Down
2 changes: 1 addition & 1 deletion crates/examples/snapshots/zklogin.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ zklogin circuit
--
Number of gates: 462908
Number of evaluation instructions: 550412
Number of AND constraints: 577527
Number of AND constraints: 604407
Number of MUL constraints: 26880
Length of value vec: 1048576
Constants: 710
Expand Down
19 changes: 18 additions & 1 deletion crates/frontend/src/compiler/gate/imul.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
//! Uses the MulConstraint: X * Y = (HI << 64) | LO

use crate::compiler::{
constraint_builder::ConstraintBuilder,
constraint_builder::{ConstraintBuilder, sll},
gate::opcode::OpcodeShape,
gate_graph::{Gate, GateData, GateParam, Wire},
};
Expand All @@ -27,6 +27,23 @@ pub fn constrain(_gate: Gate, data: &GateData, builder: &mut ConstraintBuilder)

// Create MulConstraint: X * Y = (HI << 64) | LO
builder.mul().a(*x).b(*y).hi(*hi).lo(*lo).build();

// Security fix: IntMul reduction proves x*y ≡ lo + 2^64*hi (mod 2^128-1), but we need (mod
// 2^128). Attack: If x=0 or y=0, malicious prover sets lo=hi=2^64-1, giving lo + 2^64*hi =
// 2^128-1 ≡ 0 (mod 2^128-1). This passes the IntMul check but violates the intended x*y = lo +
// 2^64*hi over integers.
//
// Fix: Check LSB multiplication x[0] * y[0] = lo[0].
// If x=0 or y=0, then x[0]*y[0] = 0, so lo[0] must be 0. But the attack has lo[0] = 1, failing
// this check.
//
// Implementation: Shift LSBs to MSB position for AND constraint.
builder
.and()
.a(sll(*x, 63))
.b(sll(*y, 63))
.c(sll(*lo, 63))
.build();
Comment thread
josephjohnston marked this conversation as resolved.
}

pub fn emit_eval_bytecode(
Expand Down