Skip to content

Commit 86ae10e

Browse files
check intmul doesn't overflow modulo 2^128-1 (#910)
### TL;DR Added an overflow check to the integer multiplication gate to prevent potential vulnerabilities. ### What changed? Added an additional constraint to the `imul.rs` gate implementation that prevents overflow modulo 2^128-1. The implementation now verifies integer multiplication on the least significant bits by: 1. Extracting the least significant bits using shift-left operations 2. Adding an AND constraint to verify that `x[0] * y[0] = lo[0]` This is accomplished by importing the `sll` function from the constraint builder module and adding the new AND constraint after the existing multiplication constraint. ### How to test? Run the existing test suite to ensure that the integer multiplication gate still functions correctly with the added overflow protection. Consider adding specific tests that attempt to trigger overflow conditions to verify the new constraint is working as expected. ### Why make this change? This change addresses a potential security vulnerability where overflow modulo 2^128-1 could occur in integer multiplication operations. The additional constraint ensures that the least significant bits of the multiplication are correctly verified, which is sufficient to guard against overflow attacks that could potentially compromise the system's integrity.
1 parent 0b2ded1 commit 86ae10e

File tree

3 files changed

+20
-3
lines changed

3 files changed

+20
-3
lines changed

crates/examples/snapshots/ethsign.snap

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ ethsign circuit
22
--
33
Number of gates: 265672
44
Number of evaluation instructions: 311772
5-
Number of AND constraints: 335708
5+
Number of AND constraints: 361166
66
Number of MUL constraints: 25458
77
Length of value vec: 524288
88
Constants: 82

crates/examples/snapshots/zklogin.snap

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ zklogin circuit
22
--
33
Number of gates: 462908
44
Number of evaluation instructions: 550412
5-
Number of AND constraints: 577527
5+
Number of AND constraints: 604407
66
Number of MUL constraints: 26880
77
Length of value vec: 1048576
88
Constants: 710

crates/frontend/src/compiler/gate/imul.rs

Lines changed: 18 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
//! Uses the MulConstraint: X * Y = (HI << 64) | LO
33
44
use crate::compiler::{
5-
constraint_builder::ConstraintBuilder,
5+
constraint_builder::{ConstraintBuilder, sll},
66
gate::opcode::OpcodeShape,
77
gate_graph::{Gate, GateData, GateParam, Wire},
88
};
@@ -27,6 +27,23 @@ pub fn constrain(_gate: Gate, data: &GateData, builder: &mut ConstraintBuilder)
2727

2828
// Create MulConstraint: X * Y = (HI << 64) | LO
2929
builder.mul().a(*x).b(*y).hi(*hi).lo(*lo).build();
30+
31+
// Security fix: IntMul reduction proves x*y ≡ lo + 2^64*hi (mod 2^128-1), but we need (mod
32+
// 2^128). Attack: If x=0 or y=0, malicious prover sets lo=hi=2^64-1, giving lo + 2^64*hi =
33+
// 2^128-1 ≡ 0 (mod 2^128-1). This passes the IntMul check but violates the intended x*y = lo +
34+
// 2^64*hi over integers.
35+
//
36+
// Fix: Check LSB multiplication x[0] * y[0] = lo[0].
37+
// 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
38+
// this check.
39+
//
40+
// Implementation: Shift LSBs to MSB position for AND constraint.
41+
builder
42+
.and()
43+
.a(sll(*x, 63))
44+
.b(sll(*y, 63))
45+
.c(sll(*lo, 63))
46+
.build();
3047
}
3148

3249
pub fn emit_eval_bytecode(

0 commit comments

Comments
 (0)