CVE-2023-44378 (Go, published 2023-10-09T14:15Z)
Description: value: gnark is a zk-SNARK library that offers a high-level API to design circuits. Prior to version 0.9.0, for some in-circuit values, it is possible to construct two valid decomposition to bits. In addition to the canonical decomposition of `a`, for small values there exists a second decomposition for `a+r` (where `r` is the modulus the values are being reduced by). The second decomposition was possible due to overflowing the field where the values are defined. Upgrading to version 0.9.0 should fix the issue without needing to change the calls to value comparison methods.
Severity: nan (CVSS v3 base score: 5.5)
Weakness: CWE-191 \u2014 Integer Underflow (Wrap or Wraparound)
The product subtracts one value from another, such that the result is less than the minimum allowable integer value, which produces a value that is not equal to the correct result.
Repository: https://github.com/Consensys/gnark
Files changed:
frontend/api.go
frontend/cs/r1cs/api.go
frontend/cs/r1cs/api_assertions.go
frontend/cs/scs/api.go
frontend/cs/scs/api_assertions.go
internal/backend/circuits/hint.go
internal/regression_tests/doc.go
internal/regression_tests/issue_836_test.go
std/math/bits/conversion.go
std/math/bits/conversion_binary.go
std/math/bits/intf_constcheck.go
test/engine.go
Commit message: fix: assert that the binary decomposition of a variable is less than the modulus (#835)

The issue was reported by Marcin Kostrzewa @ Reilabs (@kustosz).

* test: add internal regression test pacakge for tracking filed bugs

* test: add test for reproducing non-unique binary decomposition

* refactor: make comparison against a constant bound public

Even though the method is public this method is not listable as we export
interfaces with smaller method sets. The method can be accessed by implicitly
implementing interface with the method `MustBeLessOrEqCst(aBits
[]frontend.Variable, bound *big.Int, aForDebug frontend.Variable)`.

We use the method for checking in `std/math/bits` package that the binary
decomposition of the bound returned by hint is less than the modulus.

* feat: add option to omit uniqueness check when binary decomposing value

* fix: check that the binary decomposition is unique when nbBits=modlen

* refactor: use bits gadget directly for option control

* docs: describe in documentation alternatives to Cmp and LEQ

* test: add test for math/cmp cases

* feat: add TestEngine checking

* test: reduce binary decomposition length to accomodate tinyfield

* refactor: rename to OmitModulusCheck

* fix: limit decomposition length to fieldbitlen

* feat: allow less than nbBits in constant comparison

* test: update circuit statistics

* feat: allow decomposition length be longer than field length

* Revert "feat: add TestEngine checking"

This reverts commit 8da5d07924d2faf0d014f1e00781516fa0070dff.

* test: implement constant comparison for test engine

* test: rename file to track issue

Vulnerable code:
	// Cmp returns 1 if i1>i2, 0 if i1=i2, -1 if i1<i2
	// AssertIsLessOrEqual fails if  v > bound
	"github.com/consensys/gnark/internal/utils"
	vars, _ := builder.toVariables(i1, i2)
	bi1 := builder.ToBinary(vars[0], builder.cs.FieldBitLen())
	bi2 := builder.ToBinary(vars[1], builder.cs.FieldBitLen())
		vv := builder.toVariable(v)
		builder.mustBeLessOrEqCst(vv, builder.cs.ToBigInt(cb))
	aBits := bits.ToBinary(builder, a, bits.WithNbDigits(nbBits), bits.WithUnconstrainedOutputs())
	boundBits := builder.ToBinary(bound, nbBits)
func (builder *builder) mustBeLessOrEqCst(a expr.LinearExpression, bound *big.Int) {
	debug := builder.newDebugInfo("mustBeLessOrEq", a, " <= ", builder.toVariable(bound))

	// note that at this stage, we didn't boolean-constraint these new variables yet
	// (as opposed to ToBinary)
	aBits := bits.ToBinary(builder, a, bits.WithNbDigits(nbBits), bits.WithUnconstrainedOutputs())
	bi1 := builder.ToBinary(i1, builder.cs.FieldBitLen())
	bi2 := builder.ToBinary(i2, builder.cs.FieldBitLen())
	"github.com/consensys/gnark/internal/utils"
	switch b := bound.(type) {
	case expr.Term:
	default:
		builder.mustBeLessOrEqCst(v, utils.FromInterface(b))
	aBits := bits.ToBinary(builder, a, bits.WithNbDigits(nbBits), bits.WithUnconstrainedOutputs())
	boundBits := builder.ToBinary(bound, nbBits)
func (builder *builder) mustBeLessOrEqCst(a frontend.Variable, bound big.Int) {
	if ca, ok := builder.constantValue(a); ok {
		// a is constant, compare the big int values
		ba := builder.cs.ToBigInt(ca)
		if ba.Cmp(&bound) == 1 {
			panic(fmt.Sprintf("AssertIsLessOrEqual: %s > %s", ba.String(), bound.String()))
		}
	}

	debug := builder.newDebugInfo("mustBeLessOrEq", a, " <= ", bound)

	// note that at this stage, we didn't boolean-constraint these new variables yet
	// (as opposed to ToBinary)
	aBits := bits.ToBinary(builder, a, bits.WithNbDigits(nbBits), bits.WithUnconstrainedOutputs())
	bits := api.ToBinary(linearExpression, 10)
// WithNbDigits sets the resulting number of digits (nbDigits) to be used in the base conversion.
// nbDigits must be > 0. If nbDigits is lower than the length of full decomposition and
// WithUnconstrainedOutputs option is not used, then the conversion functions will generate an
// unsatisfiable constraint. If WithNbDigits option is not set, then the full decomposition is
// returned.

Fixed code:
	// Cmp returns:
	//  * 1 if i1>i2,
	//  * 0 if i1=i2,
	//  * -1 if i1<i2.
	//
	// If the absolute difference between the variables i1 and i2 is known, then
	// it is more efficient to use the bounded methdods in package
	// [github.com/consensys/gnark/std/math/bits].
	// AssertIsLessOrEqual fails if v > bound.
	//
	// If the absolute difference between the variables b and bound is known, then
	// it is more efficient to use the bounded methdods in package
	// [github.com/consensys/gnark/std/math/bits].
	"github.com/consensys/gnark/internal/utils"

	nbBits := builder.cs.FieldBitLen()
	// in AssertIsLessOrEq we omitted comparison against modulus for the left
	// side as if `a+r<b` implies `a<b`, then here we compute the inequality
	// directly.
	bi1 := bits.ToBinary(builder, i1, bits.WithNbDigits(nbBits))
	bi2 := bits.ToBinary(builder, i2, bits.WithNbDigits(nbBits))
	nbBits := builder.cs.FieldBitLen()
	vBits := bits.ToBinary(builder, v, bits.WithNbDigits(nbBits), bits.WithUnconstrainedOutputs())

		builder.MustBeLessOrEqCst(vBits, builder.cs.ToBigInt(cb), v)
	aBits := bits.ToBinary(builder, a, bits.WithNbDigits(nbBits), bits.WithUnconstrainedOutputs(), bits.OmitModulusCheck())
	boundBits := bits.ToBinary(builder, bound, bits.WithNbDigits(nbBits))
// MustBeLessOrEqCst asserts that value represented using its bit decomposition
// aBits is less or equal than constant bound. The method boolean constraints
// the bits in aBits, so the caller can provide unconstrained bits.
func (builder *builder) MustBeLessOrEqCst(aBits []frontend.Variable, bound *big.Int, aForDebug frontend.Variable) {
	if len(aBits) > nbBits {
		panic("more input bits than field bit length")
	}
	for i := len(aBits); i < nbBits; i++ {
		aBits = append(aBits, 0)
	}
	debug := builder.newDebugInfo("mustBeLessOrEq", aForDebug, " <= ", builder.toVariable(bound))
	nbBits := builder.cs.FieldBitLen()
	// in AssertIsLessOrEq we omitted comparison against modulus for the left
	// side as if `a+r<b` implies `a<b`, then here we compute the inequality
	// directly.
	bi1 := bits.ToBinary(builder, i1, bits.WithNbDigits(nbBits))
	bi2 := bits.ToBinary(builder, i2, bits.WithNbDigits(nbBits))
	cv, vConst := builder.constantValue(v)
	cb, bConst := builder.constantValue(bound)

	// both inputs are constants
	if vConst && bConst {
		bv, bb := builder.cs.ToBigInt(cv), builder.cs.ToBigInt(cb)
		if bv.Cmp(bb) == 1 {
			panic(fmt.Sprintf("AssertIsLessOrEqual: %s > %s", bv.String(), bb.String()))
		}
	}

	nbBits := builder.cs.FieldBitLen()
	vBits := bits.ToBinary(builder, v, bits.WithNbDigits(nbBits), bits.WithUnconstrainedOutputs())

	// bound is constant
	if bConst {
		builder.MustBeLessOrEqCst(vBits, builder.cs.ToBigInt(cb), v)
		return
	}

	if b, ok := bound.(expr.Term); ok {
	} else {
		panic(fmt.Sprintf("expected bound type expr.Term, got %T", bound))
	aBits := bits.ToBinary(builder, a, bits.WithNbDigits(nbBits), bits.WithUnconstrainedOutputs(), bits.OmitModulusCheck())
	boundBits := bits.ToBinary(builder, bound, bits.WithNbDigits(nbBits)) // enforces range check against modulus
// MustBeLessOrEqCst asserts that value represented using its bit decomposition
// aBits is less or equal than constant bound. The method boolean constraints
// the bits in aBits, so the caller can provide unconstrained bits.
func (builder *builder) MustBeLessOrEqCst(aBits []frontend.Variable, bound *big.Int, aForDebug frontend.Variable) {
	if len(aBits) > nbBits {
		panic("more input bits than field bit length")
	}
	for i := len(aBits); i < nbBits; i++ {
		aBits = append(aBits, 0)
	}
	debug := builder.newDebugInfo("mustBeLessOrEq", aForDebug, " <= ", bound)
	bits := api.ToBinary(linearExpression, 6)
// Package regressiontests includes tests to avoid re-introducing regressions.
package regressiontests
package regressiontests

import (
	"fmt"
	"math/big"
	"testing"

	"github.com/consensys/gnark/constraint/solver"
	"github.com/consensys/gnark/frontend"
	"github.com/consensys/gnark/std/math/cmp"
	"github.com/consensys/gnark/test"
)

type CmpCircuit struct {
	Left      frontend.Variable
	Right     frontend.Variable
	ExpCmpRes frontend.Variable
}

func (c *CmpCircuit) Define(api frontend.API) error {
	r := api.Cmp(c.Left, c.Right)
	api.AssertIsEqual(r, c.ExpCmpRes)
	return nil
}

type AssertIsLessOrEqCircuit struct {
	Smaller, Bigger frontend.Variable
}

func (c *AssertIsLessOrEqCircuit) Define(api frontend.API) error {
	api.AssertIsLessOrEqual(c.Smaller, c.Bigger)
	return nil
}

type MathCmpAssertIsLessOrEqCircuitBounded struct {
	Left  frontend.Variable
	Right frontend.Variable
}

func (c *MathCmpAssertIsLessOrEqCircuitBounded) Define(api frontend.API) error {
	cmper := cmp.NewBoundedComparator(api, big.NewInt(6), false)
	cmper.AssertIsLessEq(c.Left, c.Right)
	return nil
}

type MathCmpAssertIsLessOrEqCircuitFull struct {
	Left  frontend.Variable
	Right frontend.Variable
}

func (c *MathCmpAssertIsLessOrEqCircuitFull) Define(api frontend.API) error {
	api.AssertIsEqual(1, cmp.IsLessOrEqual(api, c.Left, c.Right))
	return nil
}

func getNBitsHint() (solver.HintID, error) {
	for _, v := range solver.GetRegisteredHints() {
		if solver.GetHintName(v) == "github.com/consensys/gnark/std/math/bits.nBits" {
			return solver.GetHintID(v), nil
		}
	}
	return 0, fmt.Errorf("nBits hint not found")
}

func TestIssue836Cmp(t *testing.T) {
	assert := test.NewAssert(t)
	assignmentNoHintGood := CmpCircuit{
		Left:      10,
		Right:     5,
		ExpCmpRes: 1,
	}
	assignmentNoHintBad := CmpCircuit{
		Left:      5,
		Right:     10,
		ExpCmpRes: 1,
	}
	assignmentHintBad := CmpCircuit{
		Left:      10,
		Right:     5,
		ExpCmpRes: -1,
	}
	toReplaceHint, err := getNBitsHint()
	if err != nil {
		t.Fatalf("couldn't find hint to replace: %v", err)
	}
	assert.CheckCircuit(&CmpCircuit{}, test.WithValidAssignment(&assignmentNoHintGood), test.WithInvalidAssignment(&assignmentNoHintBad))
	assert.CheckCircuit(&CmpCircuit{}, test.WithInvalidAssignment(&assignmentHintBad), test.NoTestEngine(), test.WithSolverOpts(solver.OverrideHint(toReplaceHint, maliciousNbitsHint)))
}

func TestIssue836AssertIsLess(t *testing.T) {
	assert := test.NewAssert(t)
	assignmentNoHintGood := AssertIsLessOrEqCircuit{
		Smaller: 5,
		Bigger:  10,
	}
	assignmentNoHintBad := AssertIsLessOrEqCircuit{
		Smaller: 11,
		Bigger:  10,
	}
	assignmentHintBad := AssertIsLessOrEqCircuit{
		Smaller: 10,
		Bigger:  5,
	}
	toReplaceHint, err := getNBitsHint()
	if err != nil {
		t.Fatalf("couldn't find hint to replace: %v", err)
	}
	assert.CheckCircuit(&AssertIsLessOrEqCircuit{}, test.WithValidAssignment(&assignmentNoHintGood), test.WithInvalidAssignment(&assignmentNoHintBad))
	assert.CheckCircuit(&AssertIsLessOrEqCircuit{}, test.WithInvalidAssignment(&assignmentHintBad), test.NoTestEngine(), test.WithSolverOpts(solver.OverrideHint(toReplaceHint, maliciousNbitsHint)))
}

func TestIssue836MathCmpAssertIsLessEqBounded(t *testing.T) {
	assert := test.NewAssert(t)
	assignmentNoHintGood := MathCmpAssertIsLessOrEqCircuitBounded{
		Left:  5,
		Right: 10,
	}
	assignmentNoHintBad := MathCmpAssertIsLessOrEqCircuitBounded{
		Left:  11,
		Right: 10,
	}
	assignmentHintBad := MathCmpAssertIsLessOrEqCircuitBounded{
		Left:  10,
		Right: 5,
	}
	toReplaceHint, err := getNBitsHint()
	if err != nil {
		t.Fatalf("couldn't find hint to replace: %v", err)
	}
	assert.CheckCircuit(&MathCmpAssertIsLessOrEqCircuitBounded{}, test.WithValidAssignment(&assignmentNoHintGood), test.WithInvalidAssignment(&assignmentNoHintBad))
	assert.CheckCircuit(&MathCmpAssertIsLessOrEqCircuitBounded{}, test.WithInvalidAssignment(&assignmentHintBad), test.NoTestEngine(), test.WithSolverOpts(solver.OverrideHint(toReplaceHint, maliciousNbitsHint)))
}

func TestIssueXXXMathCmpAssertIsLessEqFull(t *testing.T) {
	assert := test.NewAssert(t)
	assignmentNoHintGood := MathCmpAssertIsLessOrEqCircuitFull{
		Left:  5,
		Right: 10,
	}
	assignmentNoHintBad := MathCmpAssertIsLessOrEqCircuitFull{
		Left:  11,
		Right: 10,
	}
	assignmentHintBad := MathCmpAssertIsLessOrEqCircuitFull{
		Left:  10,
		Right: 5,
	}
	toReplaceHint, err := getNBitsHint()
	if err != nil {
		t.Fatalf("couldn't find hint to replace: %v", err)
	}
	assert.CheckCircuit(&MathCmpAssertIsLessOrEqCircuitFull{}, test.WithValidAssignment(&assignmentNoHintGood), test.WithInvalidAssignment(&assignmentNoHintBad))
	assert.CheckCircuit(&MathCmpAssertIsLessOrEqCircuitFull{}, test.WithInvalidAssignment(&assignmentHintBad), test.NoTestEngine(), test.WithSolverOpts(solver.OverrideHint(toReplaceHint, maliciousNbitsHint)))
}

func maliciousNbitsHint(mod *big.Int, inputs []*big.Int, results []*big.Int) error {
	n := inputs[0]
	// This is a malicious hint. If n is less equal than 5, then add the
	// modulus. This creates a non-unique binary decomposition of the value.
	if n.Cmp(big.NewInt(5)) <= 0 {
		n = n.Add(n, mod)
	}
	for i := 0; i < len(results); i++ {
		results[i].SetUint64(uint64(n.Bit(i)))
	}
	return nil
}

	omitModulusCheck bool
// WithNbDigits sets the resulting number of digits (nbDigits) to be used in the
// base conversion.
//
// nbDigits must be > 0. If nbDigits is lower than the length of full
// decomposition and [WithUnconstrainedOutputs] option is not used, then the
// conversion functions will generate an unsatisfiable constraint.
//
// If nbDigits is larger than the bitlength of the modulus, then the returned
// slice has length nbDigits with excess bits being 0.
//
// If WithNbDigits option is not set, then the full decomposition is returned.

// OmitModulusCheck omits the comparison against native field modulus in
// case the bitlength of the decomposed value (if [WithNbDigits] not set or set
// to bitlength of the native modulus) eqals bitlength of the modulus.
//
// The check is otherwise required as there are possibly multiple correct binary
// decompositions. For example, when decomposing small a the decomposition could
// return the slices for both a or a+r, where r is the native modulus and the
// enforced constraints are correct due to implicit modular reduction by r.
//
// This option can be used in case the decomposed output is manually checked to
// be unique or if uniqueness is not required.
func OmitModulusCheck() BaseConversionOption {
	return func(opt *baseConversionConfig) error {
		opt.omitModulusCheck = true
		return nil
	}
}
	// by default we also check that the value to be decomposed is less than the
	// modulus. However, we can omit the check when the number of bits we want
	// to decompose to is less than the modulus or it was strictly requested.
	omitReducednessCheck := cfg.omitModulusCheck || cfg.NbDigits < api.Compiler().FieldBitLen()

	// if we decompose into more bits than fieldbitlen then the rest would be
	// always zeros. Reduce the always-zeros to have fewer edge-cases elsewhere.
	var paddingBits int
	if cfg.NbDigits > api.Compiler().FieldBitLen() {
		paddingBits = cfg.NbDigits - api.Compiler().FieldBitLen()
		cfg.NbDigits = api.Compiler().FieldBitLen()
	}
	if !omitReducednessCheck {
		if cmper, ok := api.Compiler().(bitsComparatorConstant); ok {
			bound := new(big.Int).Sub(api.Compiler().Field(), big.NewInt(1))
			cmper.MustBeLessOrEqCst(bits, api.Compiler().Field(), bound)
		} else {
			panic("builder does not expose comparison to constant")
		}
	}

	// restore the zero bits which exceed the field bit-length when requested by
	// setting WithNbDigits larger than the field bitlength.
	bits = append(bits, make([]frontend.Variable, paddingBits)...)
	for i := cfg.NbDigits; i < len(bits); i++ {
		bits[i] = 0 // frontend.Variable is interface{}, we get nil pointer err if trying to access it.
	}
package bits

import (
	"math/big"

	"github.com/consensys/gnark/frontend"
)

// bitsComparatorConstant allows to use the built-in comparison against a
// constant bound. We use the direct implementation due to the added efficiency
// of directly creating constraints instead of using API.
type bitsComparatorConstant interface {
	MustBeLessOrEqCst(aBits []frontend.Variable, bound *big.Int, aForDebug frontend.Variable)
}

// MustBeLessOrEqCst implements method comparing value given by its bits aBits
// to a bound.
func (e *engine) MustBeLessOrEqCst(aBits []frontend.Variable, bound *big.Int, aForDebug frontend.Variable) {
	v := new(big.Int)
	for i, b := range aBits {
		bb, ok := b.(*big.Int)
		if !ok {
			panic("not big.Int bit")
		}
		if !bb.IsUint64() {
			panic("given bit large")
		}
		bbu := uint(bb.Uint64())
		if bbu > 1 {
			fmt.Println(bbu)
			panic("given bit is not a bit")
		}
		v.SetBit(v, i, bbu)
	}
	if v.Cmp(bound) > 0 {
		panic(fmt.Sprintf("%d > %d", v, bound))
	}
}