Em um artigo anterior, discutimos a verificação formal avançada de sistemas de Prova de Conhecimento Zero (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 perspetiva 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 a CertiK executa a verificação formal do ZK. Para sistemas complexos como a 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, implementação de código e configuração de teste do sistema ZK. Este processo sobrepõe-se a auditorias regulares, mas difere na medida em que, após a revisão, os objetivos de verificação e as propriedades devem ser estabelecidos. Na CertiK, referimo-nos a isto como verificação orientada para auditorias. Os trabalhos de auditoria e verificação são geralmente integrados. 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 blockchain) para um verificador ZKP. O verificador verifica e confirma a prova para garantir que o cálculo ocorreu como alegado. Neste contexto, uma vulnerabilidade ZK permitiria a um hacker enviar provas ZK falsificadas para transações falsas e tê-las aceitas 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 específicas da tabela, 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 VMs tradicionais, a opacidade das transações zkVM amplifica essas vulnerabilidades. Em cadeias não-ZK, os detalhes dos cálculos de transação são registrados publicamente no blockchain; no entanto, zkVMs não armazenam esses detalhes on-chain. Esta 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 a zkWasm, a implementação do 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 de Circuitos zkWasm

De facto, através da auditoria e verificação formal do zkWasm, descobrimos várias dessas vulnerabilidades. Abaixo, 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. Em zkWasm, as leituras de memória de pilha são realizadas usando um conjunto de instruções LoadN, onde N é o tamanho dos dados a serem carregados. Por exemplo, Load64 deve ler dados de 64 bits de um endereço de memória zkWasm. 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, zkWasm representa a memória como uma matriz de bytes de 64 bits, por isso 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 forma:

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 (32 bits) altos 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 (56 bits) altos na unidade de memória sejam zero. Infelizmente, este não é o caso no código.

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

Explorando esta 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, através de uma organização cuidadosa do código e dos dados circundantes, pode desencadear execuções e transferências falsas, levando ao roubo de dados e ativos. Essas transações falsificadas 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.

Esta vulnerabilidade representa uma classe de vulnerabilidades ZK chamadas "vulnerabilidades de código" porque se originam da implementação do código e podem ser facilmente corrigidas através de pequenas modificações no 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 relativa à invocação e retorno do 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 destinatário concluir sua execução. Cada invocação espera um retorno mais tarde. Os dados dinâmicos rastreados pelo zkWasm durante o ciclo de vida de invocação e 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 de token em 1 chamando a função add_token(). Como o provador ZK em si não suporta a estrutura de dados do quadro de chamada, a Tabela de Execução (E-Table) e a Tabela de Atalhos (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 do 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 Saltos, cada quadro de chamada ocupa uma linha, armazenando o número do quadro do chamador, o nome do contexto da função do chamador (apenas para fins de ilustração) e a próxima posição de instrução do quadro do 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 Saltos).

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 as 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 Atalhos impedem que duas chamadas sejam codificadas na mesma linha de um quadro, porque 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 feliz para dois retornos: uma vez que nenhum novo quadro é criado após o retorno, um hacker poderia realmente obter a Tabela de Execução e a Tabela de Atalhos de uma sequência de execução legítima e injetar retornos falsificados (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 no 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 Jump Table é 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 do token aumenta 3 vezes em vez de 1. Portanto, o hacker poderia obter 3 tokens pelo preço de 1.

Existem várias formas de abordar esta questão. 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 existe uma linha de código problemática; A implementação do código se alinha perfeitamente com os designs de tabela e restrição. O problema está dentro do próprio design, assim como a correção.

Você pode pensar que essa vulnerabilidade deveria ser óbvia, mas, na realidade, não é. Isso ocorre porque há uma lacuna entre "duas chamadas ou dois retornos também resultarão em uma 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 difícil 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. Esta não foi uma tarefa fácil, pois tivemos que rever centenas de restrições em mais de 6.000 linhas de código Rust e dezenas de instruções zkWasm. Apesar disso, a vulnerabilidade era relativamente fácil de detetar 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 Retorno 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 ao "jops" chamado "mops", que rastreia as instruções de acesso à memória correspondentes aos dados históricos de 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 não teríamos sido capazes de confirmar ou excluir facilmente todos os cenários possíveis sem um raciocínio formal rigoroso sobre todas as restrições relevantes, já que, na verdade, não há nenhuma linha de código que esteja 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:

Verificação do código e do desenho ou modelo

Como mencionado anteriormente, tanto o código quanto o design do ZK podem conter vulnerabilidades. Ambos os tipos de vulnerabilidades podem potencialmente comprometer a integridade do sistema ZK, por isso devem ser resolvidos antes que o sistema seja colocado em operação. Um problema com os sistemas ZK, em comparação com os sistemas não-ZK, é que quaisquer ataques são mais difíceis de detetar e analisar porque seus detalhes computacionais não estão publicamente disponíveis 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ção formal

As duas vulnerabilidades que discutimos aqui foram descobertas através 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 detetadas através 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 à medida que informações 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 várias 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, mostrou 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 do 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.

Garantir a segurança de circuitos e contratos inteligentes

As aplicações ZK normalmente consistem em dois componentes: circuitos e contratos inteligentes. Para aplicações baseadas em zkVM, existem circuitos zkVM universais e aplicações de contratos inteligentes. Para aplicativos não baseados em zkVM, existem circuitos ZK específicos do aplicativo, juntamente 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 dos contratos inteligentes levasse ao comprometimento da aplicação.

Dois tipos de contratos inteligentes merecem especial atenção. O primeiro tipo lida diretamente com provas ZK. Embora possam não ser de grande escala, o seu risco é excecionalmente elevado. O segundo tipo compreende contratos inteligentes de média a grande escala executados em cima do zkVM. Sabemos que estes contratos podem, por vezes, ser altamente complexos, e os mais valiosos devem ser submetidos a auditoria e verificação, especialmente porque os 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 a partir 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. Declaração de exoneração de responsabilidade: 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 equipa do Gate Learn e não são mencionadas no Gate.io, o artigo traduzido não pode ser reproduzido, distribuído ou plagiado.