Zellic - Audit Reports

Category: Coding Mistakes

Proving that multiples of $p$ are unequal to $0$ modulo $p$ possible

Critical Severity

High Impact

Low Likelihood

Description

The assert_is_not_equal function for bigfield elements is implemented as follows:

template <typename Builder, typename T> void bigfield<Builder, T>::assert_is_not_equal(const bigfield& other) const
{
    // Why would we use this for 2 constants? Turns out, in biggroup
    const auto get_overload_count = [target_modulus = modulus_u512](const uint512_t& maximum_value) {
        uint512_t target = target_modulus;
        size_t overload_count = 0;
        while (target < maximum_value) {
            ++overload_count;
            target += target_modulus;
        }
        return overload_count;
    };
    const size_t lhs_overload_count = get_overload_count(get_maximum_value());
    const size_t rhs_overload_count = get_overload_count(other.get_maximum_value());

    // if (a == b) then (a == b mod n)
    // to save gates, we only check that (a == b mod n)

    // if numeric val of a = a' + p.q
    // we want to check (a' + p.q == b mod n)
    const field_t<Builder> base_diff = prime_basis_limb - other.prime_basis_limb;
    auto diff = base_diff;
    field_t<Builder> prime_basis(get_context(), modulus);
    field_t<Builder> prime_basis_accumulator = prime_basis;
    // Each loop iteration adds 1 gate
    // (prime_basis and prime_basis accumulator are constant so only the * operator adds a gate)
    for (size_t i = 0; i < lhs_overload_count; ++i) {
        diff = diff * (base_diff - prime_basis_accumulator);
        prime_basis_accumulator += prime_basis;
    }
    prime_basis_accumulator = prime_basis;
    for (size_t i = 0; i < rhs_overload_count; ++i) {
        diff = diff * (base_diff + prime_basis_accumulator);
        prime_basis_accumulator += prime_basis;
    }
    diff.assert_is_not_zero();
}

The way this function is intended to work can be summarized as follows. We have two unsigned integers, say $a$ and $b$ , which we want to prove are unequal modulo $p$ . Assume for the moment $a > b$ . If $k \cdot p$ is a bound for the maximum value that $a - b$ might be, then this follows if we can show, in integers, that $a - b - i \cdot p \neq = 0$ for $i = 0, 1, ..., k$ . The case for $b \geq a$ is symmetrical.

The second half of the function's implementation carries out these checks (modulo $r$ , the native circuit prime modulus, but this is not relevant for this finding). To obtain the parameter $k$ so that $a - b \leq k \cdot p$ , the code assumes that $b$ has the minimum possible value it could have, namely zero, and $a$ has the maximum value it possibly could have (which can be calculated from the maximum values of its limbs).

The function get_overload_count is then intended on argument $m$ to calculate $m / p$ . However, the function is incorrect if $m$ is a multiple of $p$ . In that case, the loop stops one iteration too early, causing the return value to be too small by one. For example, consider the case where the argument is $p$ itself. In that case, target < maximum_value will be $p < p$ , which is false, so the loop body will never run and the function will return 0. Thus, if $a = p$ , and this is the maximum value that $a$ can have, then for the case of $b$ being smaller than $a$ , only $a - b \neq = 0$ is checked, but not $a - b - p \neq = 0$ , as it should be. Thus, if $a = p$ with $b = 0$ , then assert_is_not_equal will not detect that those values are equal modulo $p$ , so a malicious prover can succeed in incorrectly proving that those values are unequal.

The following test case demonstrates this issue:

static void test_zellic_assert_not_equal()
{
    std::cout << "\nIn Zellic assert_is_not_equal!" << std::endl;
    auto builder = Builder();
    fq_ct zero = fq_ct::create_from_u512_as_witness(&builder, uint256_t(0));
    fq_ct alsozero = fq_ct::create_from_u512_as_witness(&builder, fq_ct::modulus_u512);
    for (size_t i  = 0; i < 4; i++) {
        zero.binary_basis_limbs[i].maximum_value = zero.binary_basis_limbs[i].element.get_value();
        alsozero.binary_basis_limbs[i].maximum_value = alsozero.binary_basis_limbs[i].element.get_value();
    }
    info("\nzero:");
    for (size_t limb_index = 0; limb_index < 4 ; limb_index++) {
        info("Limb ", limb_index, ": ", zero.binary_basis_limbs[limb_index]);
    }
    info("Prime limb: ", zero.prime_basis_limb);
    info("\nalsozero:");
    for (size_t limb_index = 0; limb_index < 4 ; limb_index++) {
        info("Limb ", limb_index, ": ", alsozero.binary_basis_limbs[limb_index]);
    }
    info("Prime limb: ", alsozero.prime_basis_limb);
    zero.assert_is_not_equal(alsozero);
    bool result = CircuitChecker::check(builder);
    EXPECT_EQ(result, true);
}

In this test case, assert_is_not_equal is used to prove that $0$ and $p$ are unequal modulo $p$ . The test case succeeds, even though it should not:

% ./build/bin/stdlib_primitives_tests '--gtest_filter=stdlib_bigfield/1.zellicassertnotequal'
Running main() from /home/user/aztec-packages/barretenberg/cpp/build/_deps/gtest-src/googletest/src/gtest_main.cc
Note: Google Test filter = stdlib_bigfield/1.zellicassertnotequal
[==========] Running 1 test from 1 test suite.
[----------] Global test environment set-up.
[----------] 1 test from stdlib_bigfield/1, where TypeParam = bb::UltraCircuitBuilder_<bb::UltraArith<bb::field<bb::Bn254FrParams> > >
[ RUN      ] stdlib_bigfield/1.zellicassertnotequal

In Zellic assert_is_not_equal!

zero:
Limb 0: { 0x0000000000000000000000000000000000000000000000000000000000000000 < 0x0000000000000000000000000000000000000000000000000000000000000000 }
Limb 1: { 0x0000000000000000000000000000000000000000000000000000000000000000 < 0x0000000000000000000000000000000000000000000000000000000000000000 }
Limb 2: { 0x0000000000000000000000000000000000000000000000000000000000000000 < 0x0000000000000000000000000000000000000000000000000000000000000000 }
Limb 3: { 0x0000000000000000000000000000000000000000000000000000000000000000 < 0x0000000000000000000000000000000000000000000000000000000000000000 }
Prime limb: 0x0000000000000000000000000000000000000000000000000000000000000000

alsozero:
Limb 0: { 0x00000000000000000000000000000000000000000000000d3c208c16d87cfd47 < 0x00000000000000000000000000000000000000000000000d3c208c16d87cfd47 }
Limb 1: { 0x000000000000000000000000000000000000000000000005d97816a916871ca8 < 0x000000000000000000000000000000000000000000000005d97816a916871ca8 }
Limb 2: { 0x00000000000000000000000000000000000000000000000029b85045b6818158 < 0x00000000000000000000000000000000000000000000000029b85045b6818158 }
Limb 3: { 0x00000000000000000000000000000000000000000000000000030644e72e131a < 0x00000000000000000000000000000000000000000000000000030644e72e131a }
Prime limb: 0x000000000000000000000000000000006f4d8248eeb859fbf83e9682e87cfd46
[       OK ] stdlib_bigfield/1.zellicassertnotequal (17 ms)
[----------] 1 test from stdlib_bigfield/1 (17 ms total)

[----------] Global test environment tear-down
[==========] 1 test from 1 test suite ran. (17 ms total)
[  PASSED  ] 1 test.

Impact

Malicious provers can prove that bigfield elements are unequal even though they are not, under certain conditions. The condition that is required for this to be the case is that the maximum value for one of the elements has to be a multiple of the emulated prime modulus. As the maximum values are determined on circuit generation and cannot be changed by the malicious prover, this case is unlikely to occur in practice.

Recommendations

Change the condition in the loop from < to <=.

- while (target < maximum_value) {
+ while (target <= maximum_value) {
    ++overload_count;
    target += target_modulus;
}

Remediation

This issue has been acknowledged by Aztec, and a fix was implemented in commit 763d5eb3↗.

Proving that multiples of p are unequal to 0 modulo p possible

Description

Impact

Recommendations

Remediation

Proving that multiples of $p$ are unequal to $0$ modulo $p$ possible