Em um artigo anterior, discutimos a verificação formal avançada de sistemas Zero-Knowledge Proof (ZKP): como verificar uma instrução ZK. Ao verificar formalmente cada instrução zkWasm, podemos garantir totalmente a segurança técnica e a correção de todo o circuito zkWasm. Neste artigo, nos concentraremos na perspectiva da descoberta de vulnerabilidades, analisando vulnerabilidades específicas identificadas durante os processos de auditoria e verificação e as lições aprendidas com elas. Para uma discussão geral sobre verificação formal avançada de blockchains ZKP, consulte o artigo sobre verificação formal avançada de blockchains ZKP.

Antes de discutir as vulnerabilidades do ZK, vamos primeiro entender como o CertiK executa a verificação formal do ZK. Para sistemas complexos como o ZK Virtual Machine (zkVM), o primeiro passo na verificação formal (FV) é definir claramente o que precisa ser verificado e suas propriedades. Isso requer uma revisão abrangente do design, da implementação de código e da configuração de teste do sistema ZK. Esse processo se sobrepõe às auditorias regulares, mas difere na medida em que, após a revisão, as metas e propriedades de verificação devem ser estabelecidas. Na CertiK, nos referimos a isso como verificação orientada a auditoria. O trabalho de auditoria e verificação geralmente é integrado. Para o zkWasm, realizamos auditoria e verificação formal simultaneamente.

O que é uma vulnerabilidade ZK?

A principal característica dos sistemas Zero-Knowledge Proof (ZKP) é que eles permitem a transferência de uma breve prova criptografada de cálculos executados offline ou privadamente (como transações de blockchain) para um verificador ZKP. O verificador verifica e confirma a prova para garantir que o cálculo ocorreu como alegado. Nesse contexto, uma vulnerabilidade ZK permitiria que um hacker enviasse provas ZK forjadas para transações falsas e as aceitasse pelo verificador ZKP.

Para um provador zkVM, o processo de prova ZK envolve a execução de um programa, a geração de registros de execução para cada etapa e a conversão desses registros de execução em um conjunto de tabelas numéricas (um processo conhecido como "aritmética"). Esses números devem satisfazer um conjunto de restrições (o "circuito"), que incluem as relações entre células de tabela específicas, constantes fixas, restrições de pesquisa de banco de dados entre tabelas e equações polinomiais (ou "portas") que cada par de linhas de tabela adjacentes deve satisfazer. A verificação on-chain pode confirmar a existência de uma tabela que atenda a todas as restrições sem revelar os números específicos dentro da tabela.

Tabela de aritmética em zkWasm

A precisão de cada restrição é crucial. Qualquer erro em uma restrição, seja ela muito fraca ou ausente, pode permitir que um hacker envie provas enganosas. Essas tabelas podem parecer representar uma execução válida de um contrato inteligente, mas não na realidade. Em comparação com as VMs tradicionais, a opacidade das transações zkVM amplifica essas vulnerabilidades. Em cadeias não-ZK, os detalhes dos cálculos de transações são registrados publicamente no blockchain; no entanto, zkVMs não armazenam esses detalhes on-chain. Essa falta de transparência torna difícil determinar as especificidades de um ataque ou mesmo se um ataque ocorreu.

O circuito ZK que impõe as regras de execução das instruções zkVM é extremamente complexo. Para zkWasm, a implementação de seu circuito ZK envolve mais de 6.000 linhas de código Rust e centenas de restrições. Essa complexidade geralmente significa que pode haver várias vulnerabilidades esperando para serem descobertas.

Arquitetura do circuito zkWasm

De fato, através da auditoria e verificação formal do zkWasm, descobrimos várias dessas vulnerabilidades. A seguir, discutiremos dois exemplos representativos e examinaremos as diferenças entre eles.

Vulnerabilidade de código: ataque de injeção de dados Load8

A primeira vulnerabilidade envolve a instrução Load8 em zkWasm. No zkWasm, as leituras de memória de heap são realizadas usando um conjunto de instruções LoadN, onde N é o tamanho dos dados a serem carregados. Por exemplo, o Load64 deve ler dados de 64 bits de um endereço de memória zkWasm. O Load8 deve ler dados de 8 bits (ou seja, um byte) da memória e preenchê-los com zeros para criar um valor de 64 bits. Internamente, o zkWasm representa a memória como uma matriz de bytes de 64 bits, portanto, ele precisa "selecionar" uma parte da matriz de memória. Isso é feito usando quatro variáveis intermediárias (u16_cells), que juntas formam o valor de carga completo de 64 bits.

As restrições para essas instruções LoadN são definidas da seguinte maneira:

Essa restrição é dividida em três casos: Load32, Load16 e Load8. Load64 não tem restrições porque as unidades de memória são exatamente 64 bits. Para o caso Load32, o código garante que os 4 bytes altos (32 bits) na unidade de memória devem ser zero.

Para o caso Load16, o código garante que os 6 bytes (48 bits) altos na unidade de memória devem ser zero.

Para o caso Load8, ele deve exigir que os 7 bytes altos (56 bits) na unidade de memória sejam zero. Infelizmente, esse não é o caso no código.

Como você pode ver, apenas os 9 a 16 bits altos são restritos a zero. Os outros 48 bits altos podem ser qualquer valor e ainda passar como "leitura da memória".

Explorando essa vulnerabilidade, um hacker pode adulterar a prova ZK de uma sequência de execução legítima, fazendo com que a instrução Load8 carregue esses bytes inesperados, resultando em corrupção de dados. Além disso, por meio da organização cuidadosa de código e dados circundantes, pode desencadear execuções e transferências falsas, levando ao roubo de dados e ativos. Essas transações forjadas podem passar pelos cheques dos verificadores zkWasm e ser incorretamente reconhecidas como transações legítimas pelo blockchain.

Corrigir esta vulnerabilidade é, na verdade, bastante simples.

Essa vulnerabilidade representa uma classe de vulnerabilidades ZK chamadas "vulnerabilidades de código" porque elas se originam da implementação do código e podem ser facilmente corrigidas por meio de pequenas modificações de código local. Como você pode concordar, essas vulnerabilidades também são relativamente mais fáceis de serem identificadas pelas pessoas.

Vulnerabilidade de design: Ataque de retorno forjado

Vamos dar uma olhada em outra vulnerabilidade, desta vez sobre a invocação e retorno de zkWasm. Invocação e retorno são instruções fundamentais da VM que permitem que um contexto em execução (por exemplo, uma função) chame outro e retome a execução do contexto de chamada depois que o chamador concluir sua execução. Cada invocação espera um retorno mais tarde. Os dados dinâmicos rastreados pelo zkWasm durante o ciclo de vida da invocação e do retorno são conhecidos como "quadro de chamada". Como o zkWasm executa instruções sequencialmente, todos os quadros de chamada podem ser ordenados com base em sua ocorrência durante o tempo de execução. Abaixo está um exemplo de código de invocação/retorno em execução no zkWasm.

Os usuários podem chamar a função buy_token() para comprar tokens (possivelmente por pagamento ou transferência de outros itens valiosos). Uma de suas principais etapas é aumentar o saldo da conta do token em 1 chamando a função add_token(). Como o próprio provador ZK não oferece suporte à estrutura de dados do quadro de chamada, a Tabela de Execução (E-Table) e a Jump Table (J-Table) são necessárias para registrar e acompanhar o histórico completo desses quadros de chamada.

A figura acima ilustra o processo de buy_token() chamando add_token() e retornando de add_token() para buy_token(). Pode-se ver que o saldo da conta token aumenta em 1. Na Tabela de Execução, cada etapa de execução ocupa uma linha, incluindo o número do quadro de chamada atual que está sendo executado, o nome da função de contexto atual (apenas para fins de ilustração), o número da instrução em execução atual dentro da função e a instrução atual armazenada na tabela (apenas para fins de ilustração). Na Tabela de Atalhos, cada quadro de chamada ocupa uma linha, armazenando o número de seu quadro de chamador, o nome de contexto da função de chamador (apenas para fins de ilustração) e a próxima posição de instrução do quadro de chamador (para que o quadro possa retornar). Em ambas as tabelas, há uma coluna "jops" que controla se a instrução atual é uma chamada/retorno (na Tabela de Execução) e o número total de instruções de chamada/retorno para esse quadro (na Tabela de salto).

Como esperado, cada chamada deve ter um retorno correspondente, e cada quadro deve ter apenas uma chamada e um retorno. Como mostrado na figura acima, o valor "jops" para o primeiro quadro na Tabela de Salto é 2, correspondendo à primeira e terceira linhas na Tabela de Execução, onde o valor "jops" é 1. Tudo parece normal no momento.

No entanto, há um problema aqui: enquanto uma chamada e um retorno aumentarão a contagem de "jops" para o quadro para 2, duas chamadas ou dois retornos também resultarão em uma contagem de 2. Ter duas chamadas ou dois retornos por quadro pode parecer absurdo, mas é importante lembrar que é exatamente isso que um hacker tentaria fazer quebrando expectativas.

Você pode estar se sentindo animado agora, mas será que realmente encontramos o problema?

Acontece que duas chamadas não são um problema porque as restrições da Tabela de Execução e da Tabela de Salto impedem que duas chamadas sejam codificadas na mesma linha de um quadro, pois cada chamada gera um novo número de quadro, ou seja, o número de quadro de chamada atual mais 1.

No entanto, a situação não é tão afortunada para dois retornos: como nenhum novo quadro é criado após o retorno, um hacker poderia realmente obter a Tabela de Execução e a Tabela de Salto de uma sequência de execução legítima e injetar retornos forjados (e quadros correspondentes). Por exemplo, o exemplo anterior de Tabela de Execução e Tabela de Atalhos de buy_token() chamando add_token() pode ser adulterado por um hacker para o seguinte cenário:

O hacker injetou dois retornos forjados entre a chamada original e o retorno na Tabela de Execução e adicionou uma nova linha de quadro forjada na Tabela de Atalhos (o retorno original e as etapas de execução de instruções subsequentes na Tabela de Execução precisam ser incrementados em 4). Como a contagem de "jops" para cada linha na Tabela de Salto é 2, as restrições são satisfeitas, e o verificador de prova zkWasm aceitaria a "prova" dessa sequência de execução forjada. Como visto na figura, o saldo da conta token aumenta 3 vezes em vez de 1. Portanto, o hacker poderia obter 3 tokens pelo preço de 1.

Há várias maneiras de resolver esse problema. Uma abordagem óbvia é rastrear separadamente chamadas e retornos e garantir que cada quadro tenha exatamente uma chamada e um retorno.

Você deve ter notado que até agora não mostramos uma única linha de código para esta vulnerabilidade. A principal razão é que não há nenhuma linha de código problemática; A implementação de código se alinha perfeitamente com os designs de tabela e restrição. O problema está dentro do próprio design, e a correção também.

Você pode pensar que essa vulnerabilidade deveria ser óbvia, mas na realidade, não é. Isto porque existe um intervalo entre "duas chamadas ou duas devoluções também resultarão numa contagem de 'jops' de 2" e "dois retornos são realmente possíveis". Este último requer uma análise detalhada e abrangente de várias restrições na Tabela de Execução e na Tabela de Saltos, tornando desafiador realizar um raciocínio informal completo.

Comparação de duas vulnerabilidades

A "Vulnerabilidade de Injeção de Dados Load8" e a "Vulnerabilidade de Retorno de Falsificação" têm o potencial de permitir que hackers manipulem provas ZK, criem transações falsas, enganem verificadores de provas e se envolvam em roubo ou sequestro. No entanto, a sua natureza e a forma como foram descobertos são bastante diferentes.

A "Vulnerabilidade de injeção de dados Load8" foi descoberta durante a auditoria do zkWasm. Essa não foi uma tarefa fácil, pois tivemos que revisar centenas de restrições em mais de 6.000 linhas de código Rust e dezenas de instruções zkWasm. Apesar disso, a vulnerabilidade foi relativamente fácil de detectar e confirmar. Como essa vulnerabilidade foi corrigida antes do início da verificação formal, ela não foi encontrada durante o processo de verificação. Se essa vulnerabilidade não tivesse sido descoberta durante a auditoria, poderíamos esperar que ela fosse encontrada durante a verificação da instrução Load8.

A "Vulnerabilidade de devolução de falsificação" foi descoberta durante a verificação formal após a auditoria. Uma razão pela qual não conseguimos descobri-lo durante a auditoria é que o zkWasm tem um mecanismo semelhante a "jops" chamado "mops", que rastreia instruções de acesso à memória correspondentes a dados históricos para cada unidade de memória durante o tempo de execução do zkWasm. As restrições nas contagens de mops são realmente corretas porque ele rastreia apenas um tipo de instrução de memória, gravações de memória e os dados históricos de cada unidade de memória são imutáveis e gravados apenas uma vez (contagem de mops é 1). Mas, mesmo que tivéssemos notado essa vulnerabilidade potencial durante a auditoria, ainda assim não teríamos sido capazes de confirmar ou descartar facilmente todos os cenários possíveis sem um raciocínio formal rigoroso sobre todas as restrições relevantes, pois na verdade não há nenhuma linha de código incorreta.

Em resumo, essas duas vulnerabilidades pertencem às categorias de "vulnerabilidades de código" e "vulnerabilidades de design", respectivamente. As vulnerabilidades de código são relativamente simples, mais fáceis de descobrir (código defeituoso) e mais fáceis de raciocinar e confirmar. As vulnerabilidades de design podem ser muito sutis, mais difíceis de descobrir (sem código "defeituoso") e mais difíceis de raciocinar e confirmar.

Práticas recomendadas para descobrir vulnerabilidades do ZK

Com base em nossa experiência em auditoria e verificação formal do zkVM e outras cadeias ZK e não-ZK, aqui estão algumas sugestões sobre como proteger melhor os sistemas ZK:

Verificando o código e o design

Como mencionado anteriormente, tanto o código quanto o design do ZK podem conter vulnerabilidades. Ambos os tipos de vulnerabilidades podem comprometer a integridade do sistema ZK, portanto, devem ser abordadas antes que o sistema seja colocado em operação. Um problema com sistemas ZK, em comparação com sistemas não-ZK, é que quaisquer ataques são mais difíceis de detectar e analisar porque seus detalhes computacionais não estão disponíveis publicamente ou retidos na cadeia. Como resultado, as pessoas podem estar cientes de que um ataque hacker ocorreu, mas podem não saber os detalhes técnicos de como isso aconteceu. Isso torna o custo de qualquer vulnerabilidade ZK muito alto. Consequentemente, o valor de garantir a segurança dos sistemas ZK com antecedência também é muito alto.

Realizar auditorias e verificações formais

As duas vulnerabilidades que discutimos aqui foram descobertas por meio de auditoria e verificação formal. Alguns podem supor que a verificação formal por si só evita a necessidade de auditoria, uma vez que todas as vulnerabilidades seriam detectadas por meio de verificação formal. No entanto, nossa recomendação é realizar ambos. Como explicado no início deste artigo, o trabalho de verificação formal de alta qualidade começa com uma revisão completa, inspeção e raciocínio informal sobre o código e o design, que se sobrepõe à auditoria. Além disso, encontrar e resolver vulnerabilidades mais simples durante a auditoria pode simplificar e agilizar o processo de verificação formal.

Se você estiver conduzindo uma auditoria e uma verificação formal para um sistema ZK, a abordagem ideal é executar ambos simultaneamente. Isso permite que auditores e engenheiros de verificação formal colaborem de forma eficiente, potencialmente descobrindo mais vulnerabilidades, pois entradas de auditoria de alta qualidade são necessárias para a verificação formal.

Se o seu projeto ZK já passou por auditoria (kudos) ou múltiplas auditorias (big kudos), nossa sugestão é realizar uma verificação formal no circuito com base nos resultados da auditoria anterior. Nossa experiência com auditoria e verificação formal em projetos como zkVM e outros, ZK e não-ZK, tem mostrado repetidamente que a verificação formal muitas vezes captura vulnerabilidades perdidas durante a auditoria. Dada a natureza do ZKP, embora os sistemas ZK devam oferecer melhor segurança e escalabilidade de blockchain do que as soluções não-ZK, a criticidade de sua segurança e correção é muito maior do que os sistemas tradicionais não-ZK. Portanto, o valor da verificação formal de alta qualidade para sistemas ZK excede em muito o de sistemas não-ZK.

Garanta a segurança de circuitos e contratos inteligentes

As aplicações ZK normalmente consistem em dois componentes: circuitos e contratos inteligentes. Para aplicativos baseados em zkVM, existem circuitos zkVM universais e aplicativos de contrato inteligente. Para aplicativos não baseados em zkVM, há circuitos ZK específicos do aplicativo junto com contratos inteligentes correspondentes implantados na cadeia L1 ou na outra extremidade de uma ponte.

Nossos esforços de auditoria e verificação formal para zkWasm envolvem apenas o circuito zkWasm. No entanto, do ponto de vista da segurança geral para aplicativos ZK, é crucial auditar e verificar formalmente seus contratos inteligentes também. Afinal, seria lamentável se, depois de investir esforços significativos para garantir a segurança do circuito, a frouxidão no escrutínio de contratos inteligentes levasse ao comprometimento da aplicação.

Dois tipos de contratos inteligentes merecem atenção especial. O primeiro tipo lida diretamente com provas ZK. Embora possam não ser de grande escala, seu risco é excepcionalmente alto. O segundo tipo compreende contratos inteligentes de média a grande escala executados sobre o zkVM. Sabemos que esses contratos às vezes podem ser altamente complexos, e os mais valiosos devem passar por auditoria e verificação, especialmente porque seus detalhes de execução não são visíveis on-chain. Felizmente, após anos de desenvolvimento, a verificação formal para contratos inteligentes agora é prática e preparada para metas apropriadas de alto valor.

Vamos resumir o impacto da verificação formal (FV) nos sistemas ZK e seus componentes com os seguintes pontos.

Declaração:

1. Este artigo é reproduzido de [panewslab], os direitos autorais pertencem ao autor original [CertiK], se você tiver alguma objeção à reimpressão, entre em contato com a equipe do Gate Learn e a equipe lidará com isso o mais rápido possível de acordo com os procedimentos relevantes.

2. Disclaimer: Os pontos de vista e opiniões expressos neste artigo representam apenas os pontos de vista pessoais do autor e não constituem qualquer conselho de investimento.

3. Outras versões linguísticas do artigo são traduzidas pela equipe do Gate Learn e não são mencionadas em Gate.io, o artigo traduzido não pode ser reproduzido, distribuído ou plagiado.