Verificação formal de zk-SNARKs: método de prova de memória

Ao realizar a verificação formal de sistemas de zk-SNARKs, o processamento do subsistema de memória é um desafio crucial. Ao contrário das máquinas virtuais tradicionais, o zkVM utiliza tabelas de execução e tabelas auxiliares para representar o estado da memória, o que requer métodos de verificação especiais.

O sistema de memória do zkWasm é composto por uma tabela de execução e uma tabela de memória. A tabela de execução registra o processo de execução das instruções, enquanto a tabela de memória armazena todo o histórico de acessos à memória. Para simplificar o desenvolvimento, o zkWasm fornece uma camada de abstração, permitindo a operação da memória através das funções alloc_memory_table_lookup_write_cell e alloc_memory_table_lookup_read_cell.

Durante o processo de verificação, tratamos a tabela de memória como uma estrutura de dados mutável, construindo um mapeamento de dados de endereço através da função memory_at. Isso pode provar que as restrições geradas pela função alloc são equivalentes às operações set e get realizadas no mapeamento, simplificando assim a verificação de instruções para uma forma semelhante a um interpretador não-ZK.

Para evitar que atacantes manipulem a tabela de memória, o zkWasm adotou um mecanismo de contagem para rastrear o número de entradas válidas. A tabela de execução e a tabela de memória mantêm contadores separadamente, garantindo a consistência entre ambas através de restrições. Isso exige maior precisão durante a verificação, sendo necessário provar que cada instrução corresponde ao número correto de entradas na tabela de memória.

O processo de verificação adota uma abordagem de cima para baixo, incluindo três etapas:

1. O número estimado de entradas que o comando deve criar
2. O número de entradas na tabela de provas não deve ser superior ao esperado
3. Provar por indução que cum_mops e instructions_mops estão sempre consistentes na tabela.

Este método de verificação detalhada ajuda a identificar erros potenciais, como um problema crítico no mecanismo de contagem da tabela de saltos.

Para realizar a verificação modular, dividimos o sistema em três partes independentes: verificação do circuito de instruções, verificação da tabela de execução e implementação da tabela de memória. Essa estrutura permite que vários engenheiros trabalhem em paralelo, aumentando a eficiência da verificação.

De um modo geral, embora a verificação zkVM apresente diferenças ao lidar com estados dinâmicos, ainda é possível adotar uma abordagem modular semelhante à verificação de intérpretes tradicionais, através do alinhamento do nível de abstração na implementação. Esta abordagem minimiza o impacto das diferenças, permitindo que cada instrução seja verificada de forma independente com base na interface get-set.