Formally Verifying Noir Zero Knowledge Programs with NAVe

Resumo Técnico: Verificação Formal de Programas de Zero Conhecimento Noir com NAVe

Definição do Problema
Sistemas de prova de Conhecimento Zero (ZK) dependem de circuitos aritméticos — conjuntos de equações polinomiais sobre corpos finitos — para verificar que uma entrada privada $W$ satisfaz uma relação $R(X, W)$ sem revelar $W$. Linguagens de Domínio Específico (DSLs) de alto nível como Noir simplificam a criação desses circuitos ao compilar o código em uma representação intermediária chamada ACIR (Representação Intermediária de Circuito Abstrato). No entanto, essa abstração introduz vulnerabilidades sutis. Especificamente, o Noir suporta "código não restrito" (via funções unconstrained e blocos unsafe) projetado para melhorar a eficiência da prova ao delegar computações complexas ao provador. Se os desenvolvedores falharem em adicionar manualmente as correspondentes restrições (por exemplo, via declarações assert) para os resultados do código não restrito, o circuito aritmético gerado pode não capturar com precisão a relação pretendida. Esse erro de "sub-restrição" (under-constrained) pode levar a vulnerabilidades de segurança graves, como permitir que um provador gere provas válidas para afirmações falsas. As ferramentas de verificação formal existentes visam majoritariamente linguagens de circuito de nível mais baixo (como Circom) ou exigem prova de teorema interativa, carecendo de verificação automatizada e escalável para programas Noir de alto nível e seus recursos específicos, como manipulação de memória e funções de caixa-preta.

Metodologia
Os autores propõem o NAVe (Noir Acir Verifier), um framework de verificação formal de código aberto que opera na representação intermediária ACIR, em vez do código-fonte de alto nível do Noir. Essa escolha garante estabilidade contra a evolução da linguagem e permite que a ferramenta suporte potencialmente outras linguagens que visam o ACIR.

1. Formalização via SMT-LIB: O núcleo do NAVe é uma formalização de um subconjunto de opcodes do ACIR em fórmulas de Satisfatibilidade Modulo Teorias (SMT). Os autores implementam duas codificações distintas:

   • Codificação de Campo Finito: Utiliza uma teoria não padrão de corpos finitos de ordem prima implementada no solver cvc5. Esta abordagem utiliza operadores específicos como ff.add, ff.mul e ff.bitsum para modelar diretamente a aritmética de campo.
   • Codificação de Aritmética de Inteiros: Aproveita a teoria padrão de inteiros no SMT-LIB. Baseia-se no isomorfismo entre corpos finitos de ordem prima $p$ e inteiros módulo $p$, codificando operações de campo como aritmética modular de inteiros (ex: (mod (+ ...) p)).

2. Semântica de Opcode: A formalização cobre opcodes chave do ACIR:

   • AssertZero: Codificado como uma restrição de equação polinomial igual a zero.
   • BlackBoxFuncCall: Especificamente formalizado para o opcode de verificação de intervalo (Range). Na codificação de campo finito, isso é modelado usando uma decomposição binária (bitsum) e restrições garantindo que os bits sejam 0 ou 1. Na codificação de inteiros, é modelado usando restrições de ordenação de inteiros padrão ($x < 2^n$).
   • MemoryOp e MemoryInit: Formalizados para rastrear mutações de arrays usando um mapa de índices para valores de testemunha (witness), lidando com operações de leitura e escrita sequencialmente.
   • BrilligCall: Representando o código não restrito, estes são traduzidos como a restrição sempre satisfeita true (ou ignorados), pois o objetivo do verificador é checar as restrições fora dos blocos não restritos.

3. Fluxo de Trabalho de Verificação:

   • A ferramenta integra-se ao Nargo, o gerenciador de pacotes do Noir, como um comando formal-verify.
   • Desenvolvedores anotam programas Noir com declarações verify_assert(b: bool). Diferente das declarações assert padrão que geram restrições de circuito, o verify_assert cria uma obrigação de prova.
   • O NAVe compila o programa Noir para ACIR, traduz os opcodes do ACIR em fórmulas SMT e constró a fórmula de verificação $F = \text{ACIR}_{\text{constraints}} \land \neg \text{verify\_assert}_{\text{condition}}$.
   • O solver cvc5 verifica a satisfatibilidade de $F$. Se $F$ for insatisfatível, a condição de verificação é válida (o programa está corretamente restrito). Se $F$ for satisfatível, o solver retorna um modelo (contraexemplo) mostrando uma atribuição de testemunha que viola a condição, auxiliando na depuração.

Principais Contribuições

• Formalização do ACIR: A primeira formalização de um subconjunto da linguagem ACIR usando SMT-LIB, cobrindo recursos complexos como operações de memória, verificações de intervalo e a distinção entre código restrito e não restrito.
• Estratégia de Codificação Dupla: A proposta de duas codificações complementares (teoria de campo finito e aritmética de inteiros) para aproveitar diferentes capacidades de solver.
• Ferramenta NAVe: Um verificador formal automatizado de código aberto integrado ao ecossistema Noir (Nargo), projetado para ser acessível a desenvolvedores sem exigir prova de teorema interativa.
• Avaliação Empírica: Uma avaliação abrangente do NAVe em um conjunto de programas de teste Noir, analisando o desempenho através de diferentes tipos de restrições e configurações de solver.

Resultos
Os autores avaliaram o NAVe em 4 conjuntos distintos de programas Noir (condições verificadas, condições falsificadas, com e sem verificações de intervalo) usando o solver cvc5.

• Desempenho do Solver: Nenhum backend único (codificação de inteiros, campo finito --ff=gb ou campo finito --ff=split) superou consistentemente os outros. Os resultados indicam que as codificações são complementares; alguns programas são resolvidos mais rapidamente por uma codificação, enquanto outros sofrem timeout naquela mesma codificação, mas têm sucesso em outra.
• Impacto de Verificações de Intervalo: Programas contendo verificações de Range (opcodes BlackBoxFuncCall) aumentaram significativamente o tempo de verificação. A configuração --ff=split, que aproxima a teoria de campo finito, mostrou desempenho superior em programas com grandes verificações de intervalo comparado à configuração padrão --ff=gb, embora ainda ocorram timeouts em casos complexos.
• Geração de Contraexemplos: A ferramenta gerou com sucesso contraexemplos para condições falsificadas, demonstrando sua utilidade na identificação de lógica sub-restrita.

Significância e Alegações
O artigo afirma que o NAVe aborda uma lacuna crítica no ecossistema ZK ao fornecer um método automatizado e escalável para verificar programas ZK de alto nível contra bugs de sub-restrição, uma classe de erros que levou a vulnerabilidades reais. Ao visar o ACIR, a ferramenta permanece robusta contra mudanças na sintaxe de alto nível do Noir e é potencialmente aplicável a outras linguagens que visam a mesma representação intermediária.

Os autores enquadram modestamente seu trabalho como um passo em direção a capacidades de verificação mais amplas. Eles reconhecem que sua formalização atual cobre apenas um subconjunto do ACIR (excluindo opcodes Call recursivos e a maioria dos BlackBoxFuncCalls exceto Range). Eles identificam o alto custo de verificar as verificações de intervalo como uma limitação primária, sugerindo que o trabalho futuro deve focar no desenvolvimento de abstrações ou aproximações para lidar com essas restrições complexas de forma eficiente. O artigo posiciona o NAVe não como uma solução completa para todas as necessidades de verificação ZK, mas como uma ferramenta prática e integrada que demonstra a viabilidade da verificação formal automatizada para o Noir e traça um caminho para melhorar o tratamento de restrições de nível de bit pelos solvers.