Unconstrained arithmetic operations
Description
The sdk provides multiple arithmetic types to application-circuit writers. This finding concerns underconstraints in the implementations of the arithmetic functions Div and Sqrt in multiple of these types, making them unsound. In the case of Div, the types Uint32, Uint64, Uint248, and Uint521 are impacted. In the case of Sqrt, all of these except Uint521 are impacted (the Uint521 type does not have a Sqrt function). We will discuss these issues using the example of Uint64.
The Div function is implemented as follows in sdk/api_uint64.go:
// Div computes the standard unsigned integer division (like Go) and returns the
// quotient and remainder. Uses QuoRemHint
func (api *Uint64API) Div(a, b Uint64) (quotient, remainder Uint64) {
out, err := api.g.Compiler().NewHint(QuoRemHint, 2, a.Val, b.Val)
if err != nil {
panic(fmt.Errorf("failed to initialize Div hint instance: %s", err.Error()))
}
q, r := out[0], out[1]
orig := api.g.Add(api.g.Mul(q, b.Val), r)
api.g.AssertIsEqual(orig, a.Val)
return newU64(q), newU64(r)
}Note that hints do not introduce any constraints but only assign values to circuit variables. The first lines of this function
out, err := api.g.Compiler().NewHint(QuoRemHint, 2, a.Val, b.Val)
if err != nil {
panic(fmt.Errorf("failed to initialize Div hint instance: %s", err.Error()))
}
q, r := out[0], out[1]thus introduce no constraints and only assign q and r. The QuoRemHint function will correctly compute these assignments so that q and r will be the quotient and remainder of dividing a.Val by b.Val, respectively. However, a malicious prover is free to replace these assignments by any other assignment.
The only constraint imposed on q and r is then a = q*b + r. This does not suffice to enforce that q and r are the correct quotient and remainder, however. A malicious prover may for example use any assignment for q of their choosing and then satisfy the constraint by setting r = a - q*b. Analogously, as long as b is nonzero, a malicious prover can choose any r and then set q = (a - r) / b to satisfy the constraint.
The Sqrt function is implemented as follows:
// Sqrt returns √a. Uses SqrtHint
func (api *Uint64API) Sqrt(a Uint64) Uint64 {
out, err := api.g.Compiler().NewHint(SqrtHint, 1, a.Val)
if err != nil {
panic(fmt.Errorf("failed to initialize SqrtHint instance: %s", err.Error()))
}
return newU64(out[0])
}Here, the return-circuit variable is completely unconstrained.
Impact
For Div, a malicious prover has one degree of freedom in setting q and r and can assign arbitrary values to one of these two circuit variables. In many use cases of Div, only one of the two return values will be used. For example, the Mean function provided for data streams in sdk/datastream.go is implemented as follows:
// Mean calculates the arithmetic mean over the selected fields of the data stream. Uses Sum.
func Mean(ds *DataStream[Uint248]) Uint248 {
sum := Sum(ds)
quo, _ := ds.api.Uint248.Div(sum, Count(ds))
return quo
}Only the quotient is used, and so a malicious prover can make Mean return any value of their choosing.
For Sqrt, a malicious prover can return any value of their choosing.
Recommendations
For Div, the remainder should be range checked to be 0 <= r < b and q range checked such that q*b cannot overflow.
For Sqrt, the inequalities out[0] * out[0] <= a < (out[0] - 1)*(out[0] - 1) should be checked. Additionally, out[0] will need to be range checked to prevent the multiplications overflowing.
Remediation
This issue has been acknowledged by Brevis, and fixes were implemented in the following commits: