🎆Summa: Unconstrained Constants Assignemnt

Book an audit with Zokyo

Summary

Related Vulnerabilities: 1. Under-constrained Circuits, 8. Assigned but not Constrained

Identified By: Summa

The circuit, written in Halo2, makes use of an external LessThan gadget that returns 1 if the lhs is less than the rhs. The logic of the circuit constrains the output to be equal to 1 using an auxiliary value check. However, the check value is assigned during witness generation. This allows a malicious prover to set check to any value, including 0, which would cause the circuit to generate a valid proof for a lhs that is greater than the rhs.

Background

Summa is a zk proof of solvency protocol. As part of the (simplified) logic of the protocol, the prover needs to prove that their assets_sum is greater than the liabilities_sum. The circuit would use a gadget from zk-evm to perform such less_than verification. The gadget would return 1 if the lhs is less than the rhs, and 0 otherwise.

The Vulnerability

The circuit would have a custom gate to enforce that check is equal to lt which is the output of the comparison performed by the gadget

    meta.create_gate(
        "verifies that `check` from current config equal to is_lt from LtChip",
        |meta| {
            let q_enable = meta.query_selector(lt_selector);

            let check = meta.query_advice(col_c, Rotation::cur());

            vec![q_enable * (config.lt_config.is_lt(meta, None) - check)]
        },
    );

Later on the circuit would have an assignment function to be called during witness generation to assign the value 1 to check

    // set check to be equal to 1
    region.assign_advice(
        || "check",
        self.config.advice[2],
        0,
        || Value::known(Fp::from(1)),
    )?;

However, this design erroneusly suppose that any prover would be using the assignment function provided by the library. A malicious prover can simply take the function and modify it to assign a different Value::known to check, even 0. This would cause the circuit to generate a valid proof for a lhs that is greater than the rhs.

The Fix

To fix the issue, the custom gate has been modified to take a constant expression (and set it to 1!) rather than a value obtained from the advice column (which is the one that can be modified by the prover during witness generation).

    meta.create_gate("is_lt is 1", |meta| {
        let q_enable = meta.query_selector(lt_selector);

        vec![
            q_enable * (config.lt_config.is_lt(meta, None) - Expression::Constant(Fp::from(1))),
        ]
    });

Conclusion The vulnerability emerges from how the circuit ensures the correctness of this less-than check. The circuit uses a mechanism known as a gate to verify that the output of the less-than gadget (termed as lt) is as expected. For this purpose, an auxiliary value, termed as 'check', is used. If everything is functioning properly, 'check' should be set to 1, indicating that the lhs is indeed less than the rhs.

However, the assignment of the value to 'check' happens during a phase called 'witness generation'. The circuit, as designed, incorrectly assumes that everyone would use the provided assignment function, which always assigns the value of 1 to 'check'. The vulnerability arises from the fact that a malicious user (or 'prover') could modify this function to assign any other value, including 0. By doing so, they could trick the circuit into accepting an incorrect statement: that the lhs is greater than the rhs.

In simpler terms, even if someone's assets are not greater than their liabilities, they could potentially prove otherwise by exploiting this vulnerability.

References:

1. Issue

2. PR