Description

Several of the sdk's types provide functions for Boolean operations And, Or, and Not as well as a Select function, which also expects a Boolean value as the first argument.

These functions' documentation does not indicate whether the caller should be responsible for ensuring that relevant arguments are Boolean (so either zero or one) or whether this will be done by the function itself.

In the cases of And, Or, and Not, this is enforced by the functions themselves. For example, And is implemented for Uint32 as follows (in sdk/api_uint32.go):

// And returns 1 if a && b [&& other[0] [&& other[1]...]] is true, and 0 otherwise
func (api *Uint32API) And(a, b Uint32, other ...Uint32) Uint32 {
	res := api.g.And(a.Val, b.Val)
	for _, v := range other {
		res = api.g.And(res, v.Val)
	}
	return newU32(res)
}

The gnark API's And function is ultimately used, which does have a documentation comment↗ that could be read as suggesting that the caller should be responsible for checking that the arguments are either zero or one, but it in fact carries out that check itself:

// Or returns a & b
! // a and b must be 0 or 1
func (builder *builder) And(a, b frontend.Variable) frontend.Variable {
! 	builder.AssertIsBoolean(a)
! 	builder.AssertIsBoolean(b)
	res := builder.Mul(a, b)
	builder.MarkBoolean(res)
	return res
}

Thus, while gnark's documentation suggests that the caller of gnark's And, and thus the caller of brevis-sdk's And, needs to verify Booleaness of the arguments themselves, in fact, in the current version of gnark used by brevis-sdk, the gnark API is implemented so as to carry out this check.

The Select function is implemented as follows:

// Select returns a if s == 1, and b if s == 0
func (api *Uint32API) Select(s Uint32, a, b Uint32) Uint32 {
	return newU32(api.g.Select(s.Val, a.Val, b.Val))
}

Here, the gnark API is again used. With regards to Select, however, we need to distinguish between the two different implementations that gnark provides for the API, for different constraint systems. The Select implementation for R1CS constraint systems in frontend/cs/r1cs/api.go begins as follows:

// Select if i0 is true, yields i1 else yields i2
func (builder *builder) Select(i0, i1, i2 frontend.Variable) frontend.Variable {

	vars, _ := builder.toVariables(i0, i1, i2)
	cond := vars[0]

	// ensures that cond is boolean
! 	builder.AssertIsBoolean(cond)

Thus, in this case, gnark handles enforcing that the selector is indeed a Boolean.

In the case of SCS constraint systems, however, Select is implemented in frontend/cs/scs/api.go as follows:

// Select if b is true, yields i1 else yields i2
func (builder *builder) Select(b frontend.Variable, i1, i2 frontend.Variable) frontend.Variable {
	_b, bConstant := builder.constantValue(b)

	if bConstant {
		if !builder.IsBoolean(b) {
			panic(fmt.Sprintf("%s should be 0 or 1", builder.cs.String(_b)))
		}
		if _b.IsZero() {
			return i2
		}
		return i1
	}

	u := builder.Sub(i1, i2)
	l := builder.Mul(u, b)

	return builder.Add(l, i2)
}

Note that in the nonconstant case, Select just returns i2 + b*(i1 - i2), with no checks done with regards to b being Boolean. Should the selector b not be constrained by the caller but be arbitrarily assignable by a malicious prover, then, assuming i1 != i2, the attacker may cause arbitrary results of Select. If the malicious prover wishes to obtain a value v, they can set the selector to b = (v - i2) / (i1 - i2).

The Brevis sdk circuits appear to be instantiated using the SCS constraint system; see for example test/constraints_test.go. Thus, the caller of the Select function as implemented for Uint32 and similar types provided by the sdk must enforce that the selector is either zero or one themselves. As the documentation does not state this, and similar functions, as well as Select with a R1CS constraint system, would not require this, there is a risk that users may not be aware that they need to constrain the selector themselves.

Impact

Users that are unaware of gnark's API implementation for SCS constraint systems may not realize that they need to constrain the selector for Select calls to be Boolean, thereby potentially allowing malicious provers to cause arbitrary return values.

Recommendations

We recommend to document which functions constrain arguments to be Boolean and for which it is required of the caller to ensure this. Additionally, it may be considered to add a constraint verifying this to the implementations of Select.

Remediation

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