> For the complete documentation index, see [llms.txt](https://zokyo-auditing-tutorials.gitbook.io/zokyo-tutorials/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://zokyo-auditing-tutorials.gitbook.io/zokyo-tutorials/tutorial-16-zero-knowledge-zk/bugs-in-the-wild/summa-unconstrained-constants-assignemnt.md).

# Summa: Unconstrained Constants Assignemnt

{% hint style="info" %}
[**Book an audit with Zokyo**](https://www.zokyo.io/)
{% endhint %}

**Summary**

Related Vulnerabilities: 1.[ Under-constrained Circuits](/zokyo-tutorials/tutorial-16-zero-knowledge-zk/common-vulnerabilities-in-zk-code/under-constrained-circuits.md), 8. [Assigned but not Constrained](/zokyo-tutorials/tutorial-16-zero-knowledge-zk/common-vulnerabilities-in-zk-code/assigned-but-not-constrained.md)

Identified By: [Summa](https://github.com/summa-dev)

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](https://github.com/privacy-scaling-explorations/zkevm-circuits/blob/4cfccfa6c3b251284ff61eeb907d548d59206753/gadgets/src/less_than.rs) 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](https://github.com/summa-dev/summa-solvency/issues/32)
2. [PR](https://github.com/summa-dev/summa-solvency/pull/40)