Description

The assertInputUniqueness function in sdk/host_circuit.go is passed a list of circuit variables in and the integer (assumed to be zero or one) shouldCheck. The intention is that if shouldCheck is one, then the function will constrain each nonzero component of in to only occur once (i.e., there should be no duplicate values within in except zero).

The function is implemented as follows:

func assertInputUniqueness(api frontend.API, in []frontend.Variable, shouldCheck int) {
	multicommit.WithCommitment(api, func(api frontend.API, gamma frontend.Variable) error {
		sorted, err := api.Compiler().NewHint(SortHint, len(in), in...)
		if err != nil {
			panic(err)
		}
		// Grand product check. Asserts the following equation holds:
		// ∑_{a \in in} a+ɣ = ∑_{b \in sorted} b+ɣ
		var lhs, rhs frontend.Variable = 0, 0
		for i := 0; i < len(sorted); i++ {
			lhs = api.Mul(lhs, api.Add(in[i], gamma))
			rhs = api.Mul(rhs, api.Add(sorted[i], gamma))
		}
		api.AssertIsEqual(lhs, rhs)

		for i := 0; i < len(sorted)-1; i++ {
			a, b := sorted[i], sorted[i+1]
			// are both a and b zero? if yes, then it's valid; if not, then they must be different
			bothZero := api.Select(api.IsZero(a), api.IsZero(b), 0)
			isDifferent := api.Sub(1, api.IsZero(api.Sub(a, b)))
			isValid := api.Select(bothZero, 1, isDifferent)
			isValid = api.Select(shouldCheck, isValid, 1)
			api.AssertIsEqual(isValid, 1)
		}
		return nil
	}, in...)
}

The overall idea behind this implementation is as follows. Another list sorted of same length as in is obtained from a hint. Hints allow the prover to provide assignments, but they do not introduce any constraints. This list sorted is intended to contain the same components as in but permuted so as to make sorted sorted, as the name suggests. Two things need to be checked to constrain sorted to actually be the sorted permutation of in: First, it needs to be enforced that sorted is a permutation of in, or equivalently, that value occurring in sorted also occur in in, and with the same multiplicity. Second, sorted must be constrained to be sorted.

Once sorted is known to be a sorted permutation of in, we can check uniqueness of nonzero entries of sorted instead of doing the same for in. As sorted is sorted, this is easier, as it suffices to check that two successive entries are different or both zero.

The line

sorted, err := api.Compiler().NewHint(SortHint, len(in), in...)

in the implementation fetches the sorted list from a hint, with no constraints introduced on sorted so far.

The logic following this

      // Grand product check. Asserts the following equation holds:
// ∑_{a \in in} a+ɣ = ∑_{b \in sorted} b+ɣ
var lhs, rhs frontend.Variable = 0, 0
for i := 0; i < len(sorted); i++ {
	lhs = api.Mul(lhs, api.Add(in[i], gamma))
	rhs = api.Mul(rhs, api.Add(sorted[i], gamma))
}
api.AssertIsEqual(lhs, rhs)

then performs the check that sorted is a permutation of in. Concretely, this checks the identity

If we consider $\gamma$ a variable, then we can consider both sides to be polynomials in $\gamma$. The multiset defined by in is precisely given by the multiset given by the additive inverses of the roots of the polynomial on the left-hand side (we consider the roots as a multiset, so count them with multiplicity), analogously for sorted and the polynomial on the right-hand side. Thus, to show that the sorted is a permutation of in, or equivalently that their underlying multisets are equal, it suffices to show that the two polynomials on the left- and right-hand side are equal. If the polynomials were not equal, then evaluating the polynomials at one random point has a likelihood of at most len(in) / r to obtain an equality, where r is the order of the field over which the circuit is defined (a 254-bit prime), and we use that len(in) is the degree of the polynomial. As len(in) is much smaller than r, the check succeeding at a single random point implies with high likelihood that the polynomials were already equal, and hence sorted is a permutation of in. As random challenges cannot be obtained within a circuit, gnark's commitment functionality is used to obtain a random challenge derived from in.

The final piece of code of the implementation is the following:

for i := 0; i < len(sorted)-1; i++ {
	a, b := sorted[i], sorted[i+1]
	// are both a and b zero? if yes, then it's valid; if not, then they must be different
	bothZero := api.Select(api.IsZero(a), api.IsZero(b), 0)
	isDifferent := api.Sub(1, api.IsZero(api.Sub(a, b)))
	isValid := api.Select(bothZero, 1, isDifferent)
	isValid = api.Select(shouldCheck, isValid, 1)
	api.AssertIsEqual(isValid, 1)
}

This performs constraints that, as long as shouldCheck is one, two successive entries of sorted must be different or both zero.

The discussed parts of the implementation are correct. However, what is missing is checking that sorted is not just any permutation but a sorted permutation of in.

Impact

As the check for sorted being sorted is missing, it is possible to make invalid lists pass all constraints. As a concrete example, consider in = [1, 1, 0, 0, 0]. A malicious prover could use sorted = [1, 0, 1, 0, 0]. This is in fact a permutation of in, and it also satisfies that two successive entries are either different or both zero. However, 1 occurs twice in in, so the nonzero entries are not unique.

Thus, assertInputUniqueness is unsound. As long as no single value occurs more often than len(in) / 2 times in in, a malicious prover can find an assignment for sorted that will satisfy the constraints.

This function appears to be intended to be used when application-circuit writers configure the circuit to check that inputs are unique, though this is currently commented out; see Finding ref↗.

Recommendations

Add constraints to ensure that sorted is sorted.

Remediation

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