零知识证明的形式化验证：内存证明方法

在对零知识证明系统进行形式化验证时,内存子系统的处理是一个关键挑战。与传统虚拟机不同,zkVM使用执行表和辅助表来表示内存状态,这需要特殊的验证方法。

zkWasm的内存系统由执行表和内存表组成。执行表记录了指令执行过程,而内存表则保存了所有内存访问的历史记录。为了简化开发,zkWasm提供了抽象层,通过alloc_memory_table_lookup_write_cell和alloc_memory_table_lookup_read_cell两个函数来操作内存。

在验证过程中,我们将内存表视为可变数据结构,通过memory_at函数构建地址数据映射。这样可以证明alloc函数生成的约束等价于对映射进行的set和get操作,从而将指令验证简化为类似非ZK解释器的形式。

为防止攻击者操纵内存表,zkWasm采用了计数机制来追踪有效条目数量。执行表和内存表分别维护计数器,通过约束确保两者一致。这要求验证时更加精确,需要证明每条指令对应正确数量的内存表条目。

验证过程采用自顶向下的方式,包括三个步骤:

1. 预估指令应创建的条目数量
2. 证明表中条目数不多于预期
3. 通过归纳法证明cum_mops和instructions_mops在表中始终一致

这种详细的验证方法有助于发现潜在错误,如跳转表计数机制中的一个关键问题。

为实现模块化验证,我们将系统分为三个独立部分:指令电路验证、执行表验证和内存表实现。这种结构使多位工程师可以并行工作,提高验证效率。

总的来说,zkVM验证虽然在处理动态状态时存在差异,但通过匹配实现中的抽象层,仍可以采用类似于传统解释器验证的模块化方法。这种方法最大限度地减少了差异带来的影响,使得每条指令都能基于get-set接口进行独立验证。