axiom-crypto / halo2-lib

Monorepo of halo2 crates
MIT License
236 stars 145 forks source link

[fix] soundness bug in `BasicDynLookupConfig::assign_virtual_table_to_raw` #224

Closed jonathanpwang closed 9 months ago

jonathanpwang commented 9 months ago

The problem is that in assign_virtual_table_to_raw it was using assign_virtual_to_raw, which has the following danger:

The fix is that now assign_virtual_table_to_raw uses constrain_virtual_equals_external, and we have modified constrain_virtual_equals_external so that it checks whether the virtual cell has already been assigned or not. It is only allowed to not have been assigned if the type_id of the virtual cell was marked as EXTERNAL_CELL_TYPE_ID. This marks the virtual cell as safe from ever being reassigned by a different virtual region manager.

The usage in the latter case is demonstrated in the memory.rs test.

We add a check whenever we do assigned_advice.insert that there was not already a cell present or that the occupied raw cell equals the raw cell to be inserted (this latter case is just because keygen_vk and keygen_pk each call synthesize and we cannot call clear because of mutable borrows).