soundness problem of advice lookup

[lispc]

here is an example of soundness bug

scroll-tech#212

let me explain, usually we use advice columns as lookup table, but it is difficult if not impossible to constrain that there is no evil row after the region where selectors are applied.

In the above example, all state circuit constraints are gated by a selector, but if we usually the selector be true on range [0, rws.len()) in debug environment, and [0, state_circuit_pad_to/max_rws] in prod environment ,and the max_rws currently is 1<<k-64. So there are some rows where there are no constraints at all in this lookup table...

Two solutions for this type of problem:

(1) the selector must be exact same len with 1<<k-blinding_rows or same with l_active.
(2) don't allow "all lookup table are adivce" design pattern. At least one column should be fixed column. When doing lookup, we either assert (input1, input2) in (table1_fixed, table2_any), or assert an_input_product in table_product_with_at_least_one_fixed_col.

[lispc]

btw in the original zcash/halo2, only fixed columns are allowed to be lookup table. So there are no this type of problem in their circuits.

[han0110]

I think the first solution should be the originally expected one, but the second one sounds even easier to implement without too much overhead. I think it should be fine to adopt either one.

[naure]

(1) Clearly all rows should be constrained. There should not be a concept of selector, meaning a flag that disables rules. Instead, there can be case flags, meaning a flag that chooses between either this rule or that rule. In the example given, the cases are data or padding, and the second rule enforces padding values, e.g. tag == padding.

(2) A fixed column sounds exactly like the mechanism of the blinding factors, so it will have the same problem. The actual data will need to be constrained and padded up to the fixed size provisioned by the fixed table.

The simplest seems to be to reserve a tag for padding.

[lispc]

do you think end_block can handle this? or this is indeed a problem? @ed255

[icemelon]

Another alternative solution is that we include the selector column in the lookup argument such that we only look up into the rows with the selector set to 1.

[lispc]

Another alternative solution is that we include the selector column in the lookup argument such that we only look up into the rows with the selector set to 1.

Yes that is my second proposal it is more robust / intuitive than first proposal. 2**k-blinding_rows may be a bit complex and error-prone dealing with multi subcircuits?

[icemelon]

Another alternative solution is that we include the selector column in the lookup argument such that we only look up into the rows with the selector set to 1.

Yes that is my second proposal it is more robust / intuitive than first proposal. 2**k-blinding_rows may be a bit complex and error-prone dealing with multi subcircuits?

This selector column doesn't need to be a fixed column. The only requirement is that constraints are enabled when the selector is set to 1.

[ed255]

(1) Clearly all rows should be constrained. There should not be a concept of selector, meaning a flag that disables rules. Instead, there can be case flags, meaning a flag that chooses between either this rule or that rule. In the example given, the cases are data or padding, and the second rule enforces padding values, e.g. tag == padding.

This is what I have in mind for the long term, but it will require removal of blinding factors (because otherwise the rows with blinding factors will never pass the constraints). I think this should work with all tables as long as we have a strategy to do padding (which uses a special tag in the lookup table so that a padding row can't be mistaken by a non-padding row).

Also when thinking about multi subcircuits, I believe this will only work if all the circuits/regions are layouted horizontally, but I think that's the current case, right? If two different tables of different circuits are layouted vertically (so they reuse columns), we definitely need a different selector for each circuit/region.

While we don't have the blinding factors removed, making sure that the tables take 2^k-blinding_rows rows seems the less intrusive way to me. We could add some checks to make sure the circuit selectors are enabled in all the 0 to 2^k-blinding_rows rows, to make it less error prone.

do you think end_block can handle this? or this is indeed a problem? @ed255

So what EndBlock does regarding the tables is based on the list of enabled rows of each table, make sure that number of non-padding entries in each table is the expected one. But if the number of enabled rows of a table is < 2^{k-blinding_rows} and we use selectors, we could still have a malicious row after the enabled rows and before the blinding rows.

[ed255]

Two solutions for this type of problem:

(1) the selector must be exact same len with 1<<k-blinding_rows or same with l_active.

A practical issue that I see with this approach is that it forces us to enable selectors in many rows, which affects the performance of the MockProver verification in unit tests. To keep the same performance as now we would need to play around with verify_at_rows which could be misused to skip constraint checks.

(2) don't allow "all lookup table are adivce" design pattern. At least one column should be fixed column. When doing lookup, we either assert (input1, input2) in (table1_fixed, table2_any), or assert an_input_product in table_product_with_at_least_one_fixed_col.

I think we could implement this approach as a solution to this issue: make sure that all tables contain a fixed column (which I think most of the times this column can be the same selector column of the circuit that verifies the table). This way all lookup expressions contain the selector, which will be 1 when the lookup is enabled; and this will remove the possibility to do a lookup to a non-active row.

[ChihChengLiang]

Add a fixed column selector in the dynamic lookup so that the prover can not witness malicious lookup values between used rows and unusable rows.