Resumo Técnico: Rumo à Verificação Formal Automatizada de zkEVMs Usando Síntese de Restrições Guiada por LLM

1. Declaração do Problema

As Zero-Knowledge Ethereum Virtual Machines (zkEVMs) asseguram rollups de Camada-2 gerando provas que verificam a correção da execução off-chain. No entanto, a segurança deste pipeline depende de uma premissa crítica: a implementação subjacente em Rust da zkEVM deve realizar fielmente a semântica pretendida da máquina virtual. Bugs de implementação sutis — como contabilidade de gas incorreta, atualizações de estado ausentes ou verificações de limite falhas — podem permitir que o sistema gere provas criptográficas válidas para estados semanticamente defeituosos.

Embora os solvers SMT possam, teoricamente, prevenir isso via verificação formal, a prática atual é limitada pela síntese de especificação. Há uma carência de métodos automatizados para traduzir manipuladores de opcodes de baixo nível em modelos de verificação precisos e prontos para solvers. Os fluxos de trabalho existentes dependem de especificações manuais insustentáveis e testes de mutação feitos à mão, que não escalam com otimizações frequentes e são limitados a comportamentos que os desenvolvedores explicitamente antecipam. Por outro lado, abordagens diretas de Large Language Models (LLMs) para busca de bugs sofrem com alucinações e carecem de garantias formais, pois não conseguem produzir de forma confiável os modelos de transição de estado detalhados e executáveis necessários para a verificação de zkEVMs.

2. Metodologia: VeriSynth

Os autores propõem o VeriSynth, um framework que sintetiza modelos de verificação em Python/Z3 executáveis diretamente do código-fonte Rust da zkEVM. A filosofia central de design é um paradigma híbrido: o LLM atua estritamente como um frontend de formalização para traduzir o código em restrições simbólicas candidatas, enquanto um solver SMT serve como o árbitro de correção.

O framework opera através de um pipeline de ciclo fechado composto por três mecanismos principais:

A. Decomposição Semântica

Arquivos de origem da zkEVM intermeiam manipuladores de opcode, rotinas auxiliares e objetos de estado. O VeriSynth primeiro decompõe a entrada em unidades de verificação semanticamente coerentes (ex: uma unidade do tipo SSTORE que abrange leituras de armazenamento, computação de gas e escritas). Isso isola as transições de estado em unidades modulares, tornando-as tratáveis para modelagem enquanto preserva dependências explícitas através de interfaces de unidade.

B. Prompting Baseado em Recuperação

Para estabilizar a geração do LLM, o VeriSynth emprega prompting com aumento de recuperação (retrieval-augmented prompting). Ele recupera exemplos previamente validados de um banco de dados de referência com base na similaridade semântica (família de opcode, componentes de estado e padrões de modelagem). Esses exemplos recuperados servem como âncoras semânticas, guiando o LLM sobre o vocabulário simbólico, esquemas de estado e estruturas de transição sem copiar seus modelos como templates. Isso garante que os modelos gerados adiram às decisões de modelagem previamente verificadas.

C. Síntese de Restrições Guiada por LLM e Auto-Reparo

O LLM traduz cada unidade semântica em um modelo SMT executável (script Python/Z3) codificando:

• Variáveis de Estado: Pré-estado e pós-estado para stack, memória, armazenamento, gas e contexto.
• Restrições: Condições de guarda, relações de transição de estado e contabilidade de recursos (gas/reembolso).
• Obrigações: Propriedades de segurança (ex: limites de gas, preservação da altura da stack).

O modelo gerado passa por um processo de verificação de quatro estágios:

1. Parsing: Verificação de erros de sintaxe e declarações ausentes.
2. Checagem de Sort: Validação de larguras de bit-vector e tipos simbólicos.
3. Execução: Execução da consulta do solver com um tempo limite (timeout) delimitado.
4. Checagem Semântica: Verificação se o modelo satisfaz as obrigações de segurança.

Se a verificação falhar, o sistema entra em um loop de auto-reparo. Os diagnósticos do compilador ou contraexemplos do solver são retroalimentados ao LLM como feedback estruturado para refinar o modelo. Este loop continua até que o modelo passe ou que um orçamento de reparo (máximo de 3 iterações) seja esgotado.

3. Principais Contribuições

1. Framework VeriSynth: O primeiro framework a sintetizar modelos de verificação Python/Z3 executáveis a partir de código-fonte de nível de fonte de zkEVM em Rust, utilizando o paradigma "LLM propõe, solver decide".
2. Benchmark de Nível de Fonte: A construção do primeiro benchmark de bugs de nível de fonte para implementações de Rust de zkEVM, contendo 95 amostras injetadas com falhas através de cinco famílias semânticas (aritmética/bitwise, memória/armazenamento, gas/reembolso, caminhos de call/create e ambiente/contexto).
3. Validação Empírica: Uma avaliação sistemática demonstrando que o VeriSynth supera substancialmente os baselines diretos de LLM e os fluxos de trabalho de testes de mutação manuais industriais.

4. Resultados Experimentais

Avaliado no benchmark de 95 amostras, o VeriSynth alcançou os seguintes resultados:

• Taxa de Detecção de Bugs: O VeriSynth detectou 87 de 95 bugs (91,6%).
  • Superou significativamente o baseline de apenas LLM (46,3%) e o baseline de LLM Conversacional (61,1%), que carece de fundamentação por recuperação e reparo estruturado.
  • Também superou o fluxo de trabalho de teste de mutação em Rust escrito à mão da Scroll, que expôs apenas 55 bugs (57,9%). O VeriSynth detectou 32 bugs adicionais que escaparam das asserções manuais.
• Generalização: O desempenho permaneceu alto em diversas famílias de opcodes, variando de 95,5% (aritmética/bitwise) a 85,7% (caminhos de call/create), sendo este último o mais complexo devido aos componentes interagentes.
• Estudos de Ablação:
  • Auto-Reparo: O componente mais crítico. Remover o auto-reparo reduziu a taxa de detecção de 91,6% para 66,3%, pois muitos modelos iniciais falharam devido a erros de sintaxe ou de sort, em vez de mal-entendidos semânticos.
  • Fundamentação por Recuperação (Retrieval Grounding): Remover este componente reduziu a detecção para 71,6%, confirmando seu papel como um prior de modelagem.
  • Decomposição Semântica: Remover este componente reduziu a detecção para 75,8%, destacando a dificuldade de modelar efeitos de estado dispersos no código bruto.
  • Validação de Solver: Remover a validação Z3 (dependendo apenas do julgamento do LLM) resultou em uma taxa de detecção de 47,4%, próxima ao baseline de apenas LLM.
• Custo de Tokens: O custo médio foi de aproximadamente 100K tokens por amostra (total de ~9,5M para o benchmark), com uma média de 1,8 rodadas de reparo por amostra.

5. Significância e Alegações

O artigo afirma que o VeriSynth aborda a lacuna crítica entre a semântica implícita de nível de fonte e os requisitos de verificação formal em zkEVMs. Ao tratar o LLM como um frontend de formalização em vez de um oráculo de correção, o framework aproveita a capacidade do LLM de entender a estrutura do código enquanto confia no solver SMT para validação rigorosa.

Os autores enfatizam que o VeriSynth complementa, em vez de substituir, o teste manual. Ele detecta falhas de implementação que frequentemente passam despercebidas por testes feitos à mão porque sintetiza restrições semânticas explícitas em vez de depender de casos de teste antecipados pelos desenvolvedores. O trabalho estabelece um novo baseline para avaliar a síntese de modelos de verificação automatizada na camada de infraestrutura, indo além da análise de nível de contrato ou de bytecode para o nível de código-fonte, onde reside a lógica de execução real.

O artigo conclui que, embora o custo de tokens não seja trivial, ele é limitado e aceitável para a verificação offline de lógica de segurança crítica, oferecendo um tradeoff prático entre automação e rigor de verificação. O trabalho futuro é identificado como a estimativa sistemática de falsos positivos em amostras positivas e a validação entre projetos.