> 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)


---

# Agent Instructions
This documentation is published with GitBook. GitBook is the documentation platform designed so that both humans and AI agents can read, navigate, and reason over technical content effectively. Learn more at gitbook.com.

## Querying This Documentation
If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.

Perform an HTTP GET request on the current page URL with the `ask` query parameter, and the optional `goal` query parameter:

```
GET https://zokyo-auditing-tutorials.gitbook.io/zokyo-tutorials/tutorial-16-zero-knowledge-zk/bugs-in-the-wild/summa-unconstrained-constants-assignemnt.md?ask=<question>&goal=<endgoal>
```

`ask` is the immediate question: it should be specific, self-contained, and written in natural language.
`goal` is optional and describes the broader end goal you are ultimately trying to accomplish on behalf of the user. GitBook uses it to tailor the answer towards what is most useful for that goal.

The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.

Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.
