Vulnerabilidades ZK : Rochas afiadas escondidas em águas profundas

Neste artigo, falaremos sobre vulnerabilidades comuns em programas Circom e suas causas principais. Se não estiver familiarizado com o zkSNARKs, o R1CS ou a linguagem de programação Circom, recomendamos fortemente que leia primeiro a nossa publicação anterior no blog Uma introdução suave às ZKPs e ao Circom antes de continuar aqui.

Histórico

Como auditores de segurança da Veridise, analisamos muitos circuitos ZK e descobrimos vulnerabilidades potencialmente desastrosas. (Por exemplo, veja nosso artigo anterior Circom-Pairing: Um Bug ZK de Um Milhão de Dólares Descoberto Precocemente). Ao refletir sobre nosso tempo de auditoria de circuitos ZK, uma das coisas que notamos foi como foi útil (especialmente no início) ter o rastreador de vulnerabilidades comuns do 0xPARC. Ao analisar o código em uma framework nova ou desconhecida, especialmente em um novo paradigma como o ZK, é fácil se perder. E ter um documento que detalha os tipos comuns de bugs na estrutura fornece uma lista concreta de coisas a serem procuradas. No entanto, descobrimos rapidamente que muitos dos bugs que estávamos descobrindo nesses circuitos não eram cobertos pelo rastreador. Por isso, decidimos reexaminar os bugs que encontramos, identificar os padrões comuns e compartilhá-los para ajudar os implementadores de ZK a evitar (e ajudar os auditores de ZK a encontrar 🙂) essas pedras afiadas escondidas em águas profundas.

Discrepâncias na Computação de Restrições

Lembre-se de nossa postagem anterior no blog (Uma Introdução Suave a ZKPs e Circom) que muitas linguagens ZKP, incluindo o Circom, compilam o programa em dois programas diferentes: (a) uma função geradora de testemunhas (doravante denominada "computação") e (b) um conjunto de restrições. Intuitivamente, para que o circuito esteja correto, a computação P e as restrições C devem ter a mesma semântica entre si: Dado um input x, deve ser o caso de P(x) = y (em que y é o sinal de saída) se e somente se C(x,y) for avaliada como verdadeira. Referimo-nos a essa relação como a "invariante ZKP fundamental" e, se essa invariante não for válida, o programa provavelmente contém um bug. Referimo-nos a esses problemas como "discrepâncias de computação de restrição".

Mas como essas discrepâncias de computação de restrições surgem na prática? Alguém pode se sentir tentado a pensar que isso nunca deve acontecer porque você sempre pode usar o operador <== no Circom. Lembre-se de que, no artigo anterior, esse operador gera restrições e executa simultaneamente a atribuição para o gerador de testemunhas. Portanto, se você sempre usa <== em vez de < — e ===, por que esses problemas surgiriam?

Bem, o problema é que muitos tipos de computação não podem ser expressos diretamente como uma restrição (especialmente devido ao requisito de que as restrições devem ser compiláveis até R1CS). Como resultado, há muitas situações em que não é possível usar o operador <== e é preciso tentar expressar a computação e a restrição de forma diferente, garantindo, ao mesmo tempo, que a nossa invariante ZKP fundamental seja satisfeita.

Para obter mais informações sobre essas vulnerabilidades causadas por "discrepâncias de restrição de computação", vamos considerar o circuito Edwards2Montgomery:

    template Edwards2Montgomery() {
       signal input in[2];
       signal output out[2];
       out[0] <-- (1 + in[1]) / (1 - in[1]);
       out[1] <-- out[0] / in[0];
       out[0] * (1-in[1]) === (1 + in[1]);
       out[1] * in[0] === out[0];
    }
    component main = Edwards2Montgomery();

O circuito tem o objetivo de converter um ponto numa curva de Edward para um na curva de Montgomery correspondente. Vamos considerar as restrições aqui primeiro: quando out[0] = 0, out[1] = 0 e in[1] = -1, as duas restrições serão: 0 * 2 === 0 e 0 * in[0] === 0 . Observe que ambas as equações serão satisfeitas (e a prova verificada) independentemente do que seja fornecido para in[0]!

Para resumir, as semânticas de out[1] ← out[0] / in[0] são diferentes de suas restrições correspondentes out[1] * in[0] === out[0] quando out[1] e out[0] são 0. Claramente, esse código viola a invariante ZK fundamental porque, na parte restritiva, in[1] pode ter um valor arbitrário e ainda satisfazer a restrição! Para resolver o problema, o desenvolvedor precisa restringir os divisores a valor diferente de zero.

Dependências de input e output ausentes

Um segundo padrão de bug que encontramos em grande quantidade durante nossas auditorias está relacionado à ausência de dependências entre os inputs e outputs do circuito. Como exemplo, considere o seguinte bug que encontramos durante uma de nossas auditorias:

    template ChunkedMul(m, n, base){
       signal input in1[m];
       signal input in2[n];
       signal carry[m+n];
       signal output out[m+n];
       component lt[m+n];
       ...
       // carry[m+n-1] é limitado por in1 e in2 anteriormente.
       out[m+n-1] <-- carry[m+n-1];
       for(i = 0; i< m+n; i++) {
           lt[i] = LessThanPower(base);
           lt[i].in <== out[i];
           out[i] * lt[i].out === out[i];
       }
    }
    component main = ChunkedMul(3, 3, 51);

Este trecho de código do projeto ed25519-circom corresponde ao template do circuito ChunkedMul, que implementa um algoritmo de multiplicação em partes para realizar a multiplicação de dois valores. Esses valores são representados por arrays (de tamanho m e tamanho n) de modo que cada elemento do array seja menor que 2 ** base.O sinal de output out é declarado como um array de tamanho m+n e deve representar o resultado da multiplicação. Entretanto, realmente, existe uma vulnerabilidade aqui: (Suponha que estejamos na iteração quando i = m+n-1, mostrada no trecho de código acima.)

    // carry[m+n-1] é limitado por in1 e in2 anteriormente.
    out[m+n-1] <-- carry[m+n-1];
    lt[m+n-1] = LessThanPower(base);
    lt[m+n-1].in <== out[m+n-1];
    out[m+n-1] * lt[m+n-1].out === out[m+n-1];

A intenção do desenvolvedor aqui é atribuir o valor de carry[m+n-1] para out[m+n-1] e restringir out[m+n-1] a ser menor que 2 ** base.

Vamos verificar as restrições aqui:

Primeiro, o sinal intermediário

carry[m+n-1] é limitado pelos sinais de input in1 e in2.

Segundo, out[m+n-1] e lt[m+n-1] são limitados um pelo outro.

E então…?

É óbvio que out[m+n-1] não é limitado por carry[m+n-1] e quaisquer outros sinais que sejam limitados por quaisquer sinais de input!

Portanto, um usuário mal-intencionado pode convencer o verificador de que o sinal out[m+n-1] é um valor arbitrário menor que 2 ** base! De acordo com a documentação do projeto, esse template implementa um operador crucial que é aplicado diretamente aos inputs do algoritmo geral. Assim, a vulnerabilidade descoberta por nossa auditoria expõe uma superfície de ataque substancial para todo o sistema. Para corrigir esse problema, o desenvolvedor precisa acrescentar restrições adicionais, afirmando que out[m+n-1] é igual a carry[m+n-1].

Uso de componentes inseguros

Muitas linguagens ZKP suportam os chamados "componentes", que são circuitos auxiliares usados na definição de circuito de nível superior. Essencialmente, podemos pensar em "componentes" como a chamada de uma biblioteca de terceiros em uma linguagem de programação comum. Mas, assim como as APIs tradicionais fazem certas suposições sobre como devem ser usadas (por exemplo, o input não deve ser zero ou "read" não deve ser chamada antes de "open"), os componentes geralmente também fazem certas suposições sobre seu uso! Por exemplo, um componente pode considerar que os usuários restringirão seus sinais de input ou output de determinadas maneiras. Assim, se o desenvolvedor não estiver ciente dessas suposições (implícitas ou explícitas) feitas pelo componente, ele pode acabar usando-o de forma insegura e introduzir bugs sutis no aplicativo. De fato, o bug descrito em Circom-Pairing: Um Bug ZK de Um Milhão de Dólares Descoberto Precocemente é exatamente esse caso: o bug é causado pelo fato de o output de um componente não ter restrições no circuito de nível superior!

ZKAP: A ferramenta protege seu circuito ZKP

Embora alguns erros nos programas Circom sejam bastante óbvios e possam ser detectados por meio de verificações sintáticas simples, outros são muito mais sutis e exigem uma compreensão profunda da semântica do programa. Para nos ajudar (e a outros) a encontrar erros em programas Circom de forma mais confiável, criamos uma nova ferramenta de análise estática chamada ZKAP, que pode ser usada para detectar uma grande família de erros em circuitos ZK. Se estiver interessado em saber mais, consulte a pré-impressão de uma de nossas publicações recentes: https://eprint.iacr.org/2023/190.pdf

Sobre a Veridise

A Veridise é uma empresa de segurança de blockchain que fornece auditorias e ferramentas de análise de software para todas as camadas do ecossistema de blockchain, incluindo contratos inteligentes, aplicativos web3, circuitos de conhecimento zero e implementações de blockchains. Cofundada por uma equipe de pesquisadores de verificação formal e segurança de software, a Veridise fornece ferramentas de última geração para fortalecer a segurança das blockchains. Nossos clientes podem trabalhar conosco de várias maneiras, inclusive nos contratando para auditorias de segurança, usando nossas ferramentas automatizadas de análise de segurança (para testes, análise estática, verificação formal) ou uma combinação delas.

Se estiver interessado em obter mais informações, siga-nos nas mídias sociais ou visite nosso site:

Esse artigo foi escrito por Veridise e traduzido por Fátima Lima. O original pode ser lido aqui.

Website | Twitter | Facebook | LinkedIn | Github | Request Audit