Description

In brevis-sdk, the type Int248 is implemented in sdk/api_int248.go, intended as an in-circuit, signed 248-bit integer type. The value is stored in the field Val, which is a single circuit variable holding a value that is at most 248 bits wide, with the little-endian bits of Val corresponding to the two's complement representation of the represented signed integer. The Int248 type also has two additional fields, SignBit and signBitSet. The first, SignBit, is a circuit variable that may hold the value's sign bit, and signBitSet is a native Boolean that indicates whether the sign bit indicated by SignBit is reliable or not. The purpose of caching the sign bit this way is to reduce circuit variables and constraints needed by avoiding deconstructing Val into bits unnecessarily.

The method function ensureSignBit is used to update SignBit by extracting it from Val should signBitSet be false:

func (api *Int248API) ensureSignBit(v Int248) Int248 {
	if v.signBitSet {
		return v
	}
	bin := api.g.ToBinary(v.Val, 248)
	v.SignBit = bin[247]
	v.signBitSet = true
	return v
}

Whenever signBitSet is true, ensureSignBit returns immediately, thereby not requiring any additional circuit variables or constraints.

Functions operating on Int248 that require the sign bit can then call ensureSignBit first and then use SignBit rather than computing it themselves, as can be seen, for example, in the case of IsGreaterThan:

func (api *Int248API) IsGreaterThan(a, b Int248) Uint248 {
	a = api.ensureSignBit(a)
	b = api.ensureSignBit(b)

	cmp := api.g.Cmp(a.Val, b.Val)
	isGtAsUint := api.g.IsZero(api.g.Sub(cmp, 1))

	isLt := api.g.Lookup2(
		a.SignBit, b.SignBit,
		isGtAsUint, // a, b both pos
		0,          // a neg, b pos
		1,          // a pos, b neg
		isGtAsUint, // a, b both neg
	)

	return newU248(isLt)
}

The FromValues method function is used to update an Int248 by retrieving a new value from a raw circuit variable. It is implemented as follows:

func (v Int248) FromValues(vs ...frontend.Variable) CircuitVariable {
	if len(vs) != 1 {
		panic("Int248.FromValues only takes 1 param")
	}
	v.Val = vs[0]
	return v
}

This updates Val only, but it does not invalidate the cached sign in SignBit. Should signBitSet have been true before, then the cached sign will continue to be considered valid. However, there is no consistency check done to ensure that the cached sign bit is consistent with the sign bit of the new value.

Impact

Comparison functions such as IsLessThan and IsGreaterThan use SignBit to calculate the result, so an incorrect cached sign bit can lead to incorrect return values for those comparison functions.

The pattern of overwriting a previous value of an Int248 using FromValues in a way that can cause this problem occurs in practice, for example, in the Reduce method function in sdk/datastream.go. Therefore, Reduce can return Int248 with an incorrectly cached sign, leading to incorrect results when then applying IsLessThan or IsGreaterThan.

The Reduce function is in turn used for MaxGeneric, which, with a maximum, can be computed over a data stream.

The following proof of concept demonstrates how the MaxGeneric function using Int248 types behaves incorrectly:

package sdk

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

	"github.com/consensys/gnark-crypto/ecc"
	"github.com/consensys/gnark/frontend"
	"github.com/consensys/gnark/test"
)

type TestZellicMaxInt248FromValuesSignCircuit struct {
	g           frontend.API
	i248        *Int248API
	Values      [3]Int248
	ExpectedMax Int248
}

func TestZellicMaxInt248FromValuesSign(t *testing.T) {
	c := &TestZellicMaxInt248FromValuesSignCircuit{
		Values: [3]Int248{
			ConstInt248(big.NewInt(1)),
			ConstInt248(big.NewInt(47)),
			ConstInt248(big.NewInt(42)),
		},
		ExpectedMax: ConstInt248(big.NewInt(47)),
	}
	err := test.IsSolved(c, c, ecc.BN254.ScalarField())
	check(err)
}

func (c *TestZellicMaxInt248FromValuesSignCircuit) Define(g frontend.API) error {
	api := NewCircuitAPI(g)
	c.g = g
	c.i248 = newInt248API(g)

	listForDataStream := List[Int248](c.Values[:])
	datastream := NewDataStream(api,
		DataPoints[Int248]{
			Raw:     listForDataStream,
			Toggles: []frontend.Variable{1, 1, 1},
		},
	)

	max := MaxGeneric(
		// We take maximum over the values set in the circuit struct.
		datastream,
		// The initial maximum is the smallest possible Int248, -(1<<247).
		ConstInt248(new(big.Int).Sub(big.NewInt(0), new(big.Int).Lsh(big.NewInt(1), 247))),
		c.i248.IsGreaterThan,
	)

	fmt.Println("Calculated max:")
	c.g.Println(max.SignBit, max.Val)
	fmt.Println("Expected max:")
	c.g.Println(c.ExpectedMax.SignBit, c.ExpectedMax.Val)
	c.i248.AssertIsEqual(max, c.ExpectedMax)

	return nil
}

In this test, it is attempted to calculate the maximum of the Int248 values 1, 47, and 42 using MaxGeneric. As the initial maximum (so the maximum that would be returned if the list we take the maximum over were empty), we take the lowest possible Int248, which is the negative value $-2^{247}$. Because this value is negative, the FromValues bug will cause the current maximum value in the reduction performed by MaxGeneric to always have a cached sign bit indicating a negative value. As our list contains only positive values, each comparison will indicate that the new value is larger than the current maximum (being positive, while the current maximum is negative). Thus, MaxGeneric will incorrectly return the last value as the maximum. Additionally, the returned maximum will have a cached sign bit incorrectly indicating that this value is negative.

Running the above test outputs the following:

=== RUN   TestZellicMaxInt248FromValuesSign
Calculated max:
(test.engine) zellic_max_int248_test.go:55 1 42
Expected max:
(test.engine) zellic_max_int248_test.go:57 0 47
--- FAIL: TestZellicMaxInt248FromValuesSign (0.01s)
panic: [assertIsEqual] 42 == 47
sdk.(*Int248API).AssertIsEqual
        api_int248.go:285
sdk.(*TestZellicMaxInt248FromValuesSignCircuit).Define
        zellic_max_int248_test.go:58
 [recovered]
        panic: [assertIsEqual] 42 == 47
sdk.(*Int248API).AssertIsEqual
        api_int248.go:285
sdk.(*TestZellicMaxInt248FromValuesSignCircuit).Define
        zellic_max_int248_test.go:58

The upshot is that various computations that users may do with Int248 types can result in incorrect results.

Note that the above example also demonstrates how the incorrect result of MaxGeneric breaks the assumption that the result of MaxGeneric does not depend on the order the list is given in. If a specific order of the list is not otherwise enforced by the app circuit, this could thus allow an attacker to use the order of the data points to manipulate the return value.

Recommendations

The FromValues method function should set signBitSet to false, thereby invalidating the cached sign bit and ensuring that ensureSignBit will recompute the correct sign bit:

func (v Int248) FromValues(vs ...frontend.Variable) CircuitVariable {
	if len(vs) != 1 {
		panic("Int248.FromValues only takes 1 param")
	}
	v.Val = vs[0]
+    v.signBitSet = false
	return v
}

Remediation

This issue has been acknowledged by Brevis, and a fix was implemented in commit 3191f301↗.