Resumo Técnico: ZKFUZZ: Fundação e Framework para Fuzzing Eficaz de Circuitos de Conhecimento Zero

1. Declaração do Problema

Circuitos de Conhecimento Zero (ZK) são fundamentais para computações que preservam a privacidade, permitindo provas sucintas e verificação eficiente em aplicações que vão desde criptomoedas anônimas até aprendizado de máquina verificável. No entanto, desenvolver circuitos ZK corretos é notoriamente difícil devido ao desalinhamento entre a lógica de computação de propósito geral e as restrições polinomiais de campos finitos.

Existem duas classes principais de vulnerabilidades:

• Circuitos sub-restritos: As restrições são muito frouxas, permitindo que provadores maliciosos gerem provas válidas para testemunhos inválidos (violando a correção ou soundness).
• Circuitos super-restritos: As restrições são muito rígidas, fazendo com que o sistema rejeite testemunhos válidos de provadores honestos (violando a completude ou completeness).

Os métodos existentes de detecção enfrentam limitações significativas:

• Análise Estática: Ferramentas como Circomspect e ZKAP frequentemente sofrem com altas taxas de falsos positivos e falham em capturar problemas semânticos profundos, particularmente aqueles envolvendo computações intermediárias ou terminação anormal de programas.
• Métodos Formais: Ferramentas que dependem de solucionadores SMT (por exemplo, Picus, ConsCS) lutam para escalar para tamanhos de circuitos do mundo real e frequentemente dependem de definições incompletas de vulnerabilidades, focando apenas na não determinística das restrições, enquanto ignoram casos onde a computação aborta ou onde valores intermediários não correspondem.
• Lacunas de Definição: Definições formais anteriores de bugs ZK são incompletas. Elas frequentemente ignoram a "terminação anormal" (onde uma computação falha mas as restrições ainda são satisfeitas) e não levam em conta o conjunto completo de traços de execução, incluindo valores intermediários.

2. Metodologia

2.1 Fundamento Teórico: Teste de Consistência Traço-Restrição (TCCT)

Os autores introduzem o TCCT, um framework formal independente de linguagem que define vulnerabilidades ZK como discrepâncias entre dois conjuntos:

1. Conjunto de Traços $T(P)$: O conjunto de todos os traços de execução possíveis (entrada, valores intermediários, saída) produzidos pelo programa de computação de testemunho $P$.
2. Conjunto de Satisfação de Restrições $S(C)$: O conjunto de todas as tuplas (entrada, valores intermediários, saída) que satisfazem as restrições do circuito $C$.

O TCCT define um circuito como bem-restrito se e somente se:

• Sem Sub-restricção: A projeção de $S(C)$ sobre pares entrada-saída é um subconjunto da projeção de $T(P)$. Isso garante que nenhum traço inválido seja aceito.
• Sem Super-restricção: $T(P)$ é um subconjunto de $S(C)$. Isso garante que todos os traços válidos (incluindo valores intermediários específicos) sejam aceitos.

Esta formulação captura vulnerabilidades causadas por abortos de computação (onde $P$ falha mas $C$ aceita a entrada) e incompatibilidades em valores intermediários, que definições anteriores ignoravam. Os autores provam que decidir sobre sub-restricção ou super-restricção é NP-completo, e o TCCT completo é co-NP-completo.

2.2 Design do Sistema: ZKFUZZ

O ZKFUZZ é um framework de análise dinâmica que detecta violações do TCCT usando uma abordagem de mutação conjunta de programa e geração de entrada. Diferentemente do fuzzing tradicional que apenas muta entradas, o ZKFUZZ muta tanto a lógica do programa quanto as entradas.

Fluxo de Trabalho Principal:

1. Mutação: O sistema gera mutantes ($P'$) do programa de computação original ($P$). As mutações incluem remover asserções, transformar atribuições (por exemplo, substituindo operadores ou valores) e modificar atribuições fracas.
2. Execução: Tanto o programa original ($P$) quanto o mutante ($P'$) são executados em entradas amostradas ($x$).
3. Verificação:
   • Detecção de Super-restricção: Se $P(x)$ produzir um traço válido que falha em $C$, o circuito é super-restrito.
   • Detecção de Sub-restricção: Se $P'(x)$ produzir um traço com uma saída diferente ($y' \neq y$) que ainda satisfaz $C$, o circuito é sub-restrito (já que a lógica do mutante é semanticamente diferente, a saída não deveria ser aceita).
4. Busca Guiada: Para navegar no vasto espaço de busca de grandes campos primos e infinitas possibilidades de mutação, o ZKFUZZ emprega um algoritmo genético:
   • Função de Aptidão: Uma nova função de aptidão min-soma calcula a soma dos erros de restrição através de todas as restrições para um determinado traço. O mutante é pontuado pela soma mínima de erros através das entradas amostradas. Isso difere dos métodos anteriores baseados apenas em máximos e é mais adequado para mutação conjunta.
   • Seletores de Alvo: O sistema usa análise estática para guiar a mutação e a geração de entrada em direção a padrões de alto risco, tais como:
     • Divisão por Zero: Gerar entradas onde numerador e denominador são ambos zero.
     • Verificação de Hash: Forçar entradas a satisfazer restrições de igualdade de hash.
     • Distribuição Distorcida: Viesar a geração de entrada em direção a casos extremos (0, 1 e valores próximos ao módulo do campo $q$).
     • Lista Branca: Pular modelos conhecidos como seguros (por exemplo, IsZero, Num2Bits) para focar em código propenso a erros.

3. Contribuições Principais

1. Framework TCCT: Um modelo formal unificado e independente de linguagem que subsume definições anteriores e captura o espaço completo de bugs ZK, incluindo aqueles que surgem de terminação anormal e incompatibilidades de valores intermediários.
2. Sistema ZKFUZZ: Um framework de fuzzing inovador que muta conjuntamente programas e entradas para detectar violações do TCCT, utilizando uma função de aptidão min-soma e heurísticas de busca guiada.
3. Validação Empírica: Avaliação em 452 circuitos Circom do mundo real, demonstrando desempenho superior em relação a ferramentas de última geração.
4. Protótipo Noir: Uma implementação preliminar para Noir, uma DSL ZK diferente, demonstrando o potencial do framework para independência de linguagem.

4. Resultados

Os autores avaliaram o ZKFUZZ em 452 circuitos Circom do mundo real, comparando-o com quatro ferramentas de última geração: Circomspect, ZKAP, Picus e ConsCS.

• Detecção de Bugs: O ZKFUZZ identificou 85 bugs únicos, incluindo 59 vulnerabilidades zero-day anteriormente desconhecidas. Destes, 39 foram confirmados por desenvolvedores e 14 foram corrigidos.
• Comparação: O ZKFUZZ encontrou 30% a 300% mais bugs do que as ferramentas existentes em vários tamanhos de circuitos.
• Precisão: O ZKFUZZ alcançou 100% de precisão (zero falsos positivos), enquanto analisadores estáticos como Circomspect e ZKAP tiveram altas taxas de falsos positivos (precisão variando de 0,06 a 0,75).
• Velocidade: O ZKFUZZ++ (com seletores de alvo) identificou mais de 90% dos bugs dentro de 100 segundos, superando significativamente métodos formais e analisadores estáticos.
• Impacto: Os bugs descobertos incluíram vulnerabilidades críticas de sub-restricção em projetos como zk-regex e passport-zk-circuits, que poderiam permitir que atacantes forjassem provas ou extraíssem fundos.

5. Significado e Alegações

O artigo alega que o ZKFUZZ representa um avanço significativo na segurança de circuitos ZK ao abordar a incompletude fundamental das definições anteriores de vulnerabilidades. Ao formalizar bugs como inconsistências traço-restrição (TCCT), os autores expõem uma grande classe de vulnerabilidades (quase 50% dos bugs do mundo real em sua avaliação) que eram anteriormente indetectáveis por ferramentas focadas apenas na não determinística das restrições.

A capacidade do sistema de detectar bugs sem falsos positivos torna-o uma ferramenta prática para desenvolvedores, que frequentemente ignoram alertas de analisadores estáticos com altos falsos positivos. Além disso, a detecção bem-sucedida de bugs em circuitos Noir sugere que o framework TCCT e a arquitetura do ZKFUZZ não se limitam ao Circom, mas podem generalizar-se para outras linguagens ZK que compilam para formatos de restrição padronizados.

Os autores enfatizam que seu trabalho foca em vulnerabilidades que surgem do desalinhamento entre computação e restrições (correção e completude), excluindo explicitamente bugs nos sistemas de prova subjacentes, erros de lógica pura (como entradas não utilizadas) ou vazamentos de conhecimento zero em nível de protocolo.