Nesta série de blogs sobre verificação formal avançada de provas de conhecimento zero, discutimos como verificar instruções ZK e uma análise aprofundada de duas vulnerabilidades ZK. Conforme mostrado em relatórios públicos e bases de código, ao verificar formalmente cada instrução zkWasm, encontramos e corrigimos todas as vulnerabilidades, permitindo-nos verificar completamente a segurança técnica e a exatidão de todo o circuito zkWasm.
Embora tenhamos mostrado o processo de verificação de uma instrução zkWasm e introduzido os conceitos preliminares do projeto relacionado, os leitores familiarizados com a verificação formal podem estar mais interessados em compreender a verificação do zkVM com outros sistemas ZK menores ou outros tipos de exclusividade de bytecode. sobre. Neste artigo, discutiremos em profundidade alguns dos pontos técnicos encontrados ao validar o subsistema de memória zkWasm. A memória é a parte mais exclusiva do zkVM, e lidar com isso é fundamental para todas as outras verificações do zkVM.
Verificação formal: máquina virtual (VM) versus máquina virtual ZK (zkVM)
Nosso objetivo final é verificar a exatidão do zkWasm, que é semelhante ao teorema de exatidão dos intérpretes de bytecode comuns (VMs, como o intérprete EVM usado pelos nós Ethereum). Ou seja, cada etapa de execução do intérprete corresponde a uma etapa legal baseada na semântica operacional da linguagem. Conforme mostrado na figura abaixo, se o estado atual da estrutura de dados do interpretador de bytecode for SL, e este estado for marcado como estado SH na especificação de alto nível da máquina Wasm, então quando o intérprete passar para o estado SL', haverá deve ser um O estado legal correspondente de alto nível SH', e a especificação Wasm estipula que SH deve passar para SH'.
Da mesma forma, o zkVM possui um teorema de correção semelhante: cada nova linha na tabela de execução do zkWasm corresponde a uma etapa legal baseada na semântica operacional da linguagem. Conforme mostrado na figura abaixo, se o estado atual de uma linha da estrutura de dados na tabela de execução for SR, e esse estado for expresso como estado SH na especificação de alto nível da máquina Wasm, então o estado da próxima linha da tabela de execução SR' deve corresponder a um estado de alto nível SH' , e a especificação Wasm estipula que SH deve passar para SH'.
Pode-se ver que a especificação de estados de alto nível e etapas do Wasm são consistentes tanto em VM quanto em zkVM, portanto, pode se basear na experiência anterior de verificação de intérpretes ou compiladores de linguagem de programação. O que há de especial na verificação zkVM é o tipo de estrutura de dados que constitui o estado de baixo nível do sistema.
Primeiro, como afirmamos em uma postagem anterior do blog, o provador zk é essencialmente uma operação inteira módulo números primos grandes, enquanto a especificação Wasm e o interpretador normal lidam com números inteiros de 32 ou 64 bits. A maior parte da implementação do zkVM envolve isso, portanto, o processamento correspondente também precisa ser feito durante a verificação. No entanto, este é um problema "local": cada linha de código torna-se mais complexa devido às operações aritméticas que precisa de tratar, mas a estrutura geral do código e da prova não muda.
Outra grande diferença é como as estruturas de dados dimensionadas dinamicamente são tratadas. Em um interpretador de bytecode regular, a memória, a pilha de dados e a pilha de chamadas são todas implementadas como estruturas de dados mutáveis. Da mesma forma, a especificação Wasm representa a memória como um tipo de dados com métodos get/set. Por exemplo, o interpretador EVM de Geth possui um tipo de dados `Memory`, que é implementado como uma matriz de bytes que representa a memória física e é gravado e lido através dos métodos `Set 32` e `GetPtr`. Para implementar uma instrução de armazenamento de memória, Geth chama `Set 32` para modificar a memória física.
func opMstore(pc *uint 64, interpretador *EVMInterpreter, escopo *ScopeContext) ([]byte, erro) {
//popula o valor da pilha
mStart, val := escopo.Stack.pop(), escopo.Stack.pop()
escopo.Memory.Set 32(mStart.Uint 64(), val)
retorno zero, zero
}
Na prova de correção do intérprete acima, provamos que seu estado de alto nível e seu estado de baixo nível correspondem entre si após atribuir valores à memória concreta no intérprete e à memória abstrata na especificação.
Porém, com o zkVM, a situação fica mais complicada.
Tabela de memória e camada de abstração de memória do zkWasm
No zkVM, existem colunas na tabela de execução para dados de tamanho fixo (semelhantes aos registros da CPU), mas não podem ser usadas para lidar com estruturas de dados de tamanho dinâmico, que são implementadas consultando tabelas auxiliares. A tabela de execução do zkWasm possui uma coluna EID, cujos valores são 1, 2, 3..., e possui duas tabelas auxiliares, uma tabela de memória e uma tabela de salto, que são utilizadas para representar dados de memória e pilha de chamadas respectivamente.
A seguir está um exemplo de como implementar um programa de retirada:
saldo interno, valor;
void principal() {
saldo = 100;
quantidade = 10;
saldo -= valor; // retirar
}
O conteúdo e a estrutura da tabela de execução são bastante simples. Possui 6 etapas de execução (EID 1 a 6), cada etapa possui uma linha listando seu opcode, e se a instrução for uma leitura ou gravação de memória, seu endereço e dados:
Cada linha na tabela de memória contém endereço, dados, EID inicial e EID final. O EID inicial é o EID da etapa de execução que grava esses dados neste endereço, e o EID final é o EID da próxima etapa de execução que gravará esse endereço. (Ele também contém uma contagem, que discutiremos em detalhes posteriormente.) Para o circuito de instrução de leitura de memória Wasm, ele usa uma restrição de pesquisa para garantir que haja uma entrada apropriada na tabela, de modo que o EID da instrução de leitura esteja no gama do início ao fim dentro. (Da mesma forma, cada linha da tabela de salto corresponde a um quadro da pilha de chamadas e cada linha é rotulada com o EID da etapa de instrução de chamada que a criou.)
Este sistema de memória é muito diferente de um interpretador VM regular: a tabela de memória não é uma memória mutável que é atualizada gradualmente, mas contém um histórico de todos os acessos à memória ao longo do rastreamento de execução. Para simplificar o trabalho dos programadores, o zkWasm fornece uma camada de abstração, implementada por meio de duas funções de entrada convenientes. Eles são:
alloc_memory_table_lookup_write_cell
e
Alloc_memory_table_lookup_read_cell
Seus parâmetros são os seguintes:
Por exemplo, o código que implementa as instruções de armazenamento de memória em zkWasm contém uma chamada para a função 'write alloc':
deixe memory_table_lookup_heap_write1 = alocador
.alloc_memory_table_lookup_write_cell_with_value(
"armazenar resolução de gravação 1",
construtor_de_restrição,
eid,
mover |____| constante_from!(LocationType::Heap como u 64),
mover |meta| load_block_index.expr(meta), // endereço
mover |____| constante_from!( 0), // é de 32 bits
mover |____| constante_from!( 1), // (sempre) ativado
);
deixe store_value_in_heap1 = memory_table_lookup_heap_write1.value_cell;
A função `alloc` é responsável por lidar com restrições de pesquisa entre tabelas e restrições aritméticas relacionadas ao `eid` atual às entradas da tabela de memória. A partir disso, os programadores podem tratar essas tabelas como memória comum, e o valor de `store_value_in_heap1` foi atribuído ao endereço `load_block_index` após a execução do código.
Da mesma forma, as instruções de leitura de memória são implementadas usando a função `read_alloc`. No exemplo de sequência de execução acima, há uma restrição de leitura para cada instrução de carregamento e uma restrição de gravação para cada instrução de armazenamento, e cada restrição é satisfeita por uma entrada na tabela de memória.
mtable_lookup_write(linha 1.eid, linha 1.store_addr, linha 1.store_value)
⇐ (linha 1.eid= 1 ∧ linha 1.store_addr=saldo ∧ linha 1.store_value= 100 ∧ ...)
mtable_lookup_write(linha 2.eid, linha 2.store_addr, linha 2.store_value)
⇐ (linha 2.eid= 2 ∧ linha 2.store_addr=quantidade ∧ linha 2.store_value= 10 ∧ ...)
mtable_lookup_read(linha 3.eid, linha 3.load_addr, linha 3.load_value)
⇐ ( 2
mtable_lookup_read(linha 4.eid, linha 4.load_addr, linha 4.load_value)
⇐ ( 1
mtable_lookup_write(linha 6.eid, linha 6.store_addr, linha 6.store_value)
⇐ (linha 6.eid= 6 ∧ linha 6.store_addr=saldo ∧ linha 6.store_value= 90 ∧ ...)
A estrutura da verificação formal deve corresponder às abstrações utilizadas no software que está sendo verificado, para que a prova siga a mesma lógica do código. Para zkWasm, isso significa que precisamos verificar o circuito da tabela de memória e as funções de "alocar célula de leitura/gravação" como um módulo, que faz interface como uma memória variável. Dada tal interface, a verificação de cada circuito de instrução pode ser realizada de maneira semelhante a um interpretador regular, enquanto a complexidade adicional do ZK é encapsulada no módulo do subsistema de memória.
Na verificação, implementamos a ideia de que “a tabela de memória pode realmente ser considerada uma estrutura de dados mutável”. Ou seja, escreva a função `memory_at type`, que varre completamente a tabela de memória e constrói o mapeamento de dados de endereço correspondente. (O intervalo de valores da variável `type` aqui são três tipos diferentes de dados de memória Wasm: heap, pilha de dados e variáveis globais.) Em seguida, provamos que as restrições de memória geradas pela função alloc são equivalentes ao uso de set e get funções Alterações de dados feitas pelo mapeamento de dados de endereço correspondente. Podemos provar:
Para cada eid, se as seguintes restrições forem válidas
memory_table_lookup_read_cell valor de deslocamento do tipo eid
mas
get (memory_at eid type) offset = Algum valor
E, se as seguintes restrições forem válidas
memory_table_lookup_write_cell valor de deslocamento do tipo eid
mas
memory_at (eid+ 1) tipo = definir valor de deslocamento (memory_at eid type)
Depois disso, a verificação de cada instrução pode ser baseada em operações get e set no mapa de dados de endereço, semelhantes aos interpretadores de bytecode não ZK.
Mecanismo de contagem de gravação de memória do zkWasm
No entanto, a descrição simplificada acima não revela todo o conteúdo da tabela de memória e da tabela de saltos. Na estrutura do zkVM, essas tabelas podem ser manipuladas por invasores, que podem facilmente manipular as instruções de carregamento de memória e retornar valores arbitrários inserindo uma linha de dados.
Tomando o programa de saque como exemplo, o invasor tem a oportunidade de injetar dados falsos no saldo da conta, forjando uma operação de gravação de memória de US$ 110 antes da operação de saque. Este processo pode ser alcançado adicionando uma linha de dados à tabela de memória e modificando os valores das células existentes na tabela de memória e na tabela de execução. Isto resultará em saques “gratuitos”, pois o saldo da conta ainda permanecerá em US$ 100 após a operação.
Para garantir que a tabela de memória (e a tabela de salto) contenha apenas entradas válidas geradas pelas instruções de gravação de memória (e chamada e retorno) realmente executadas, zkWasm usa um mecanismo de contagem especial para monitorar o número de entradas. Especificamente, a tabela de memória possui uma coluna dedicada que monitora o número total de entradas gravadas na memória. Ao mesmo tempo, a tabela de execução também contém um contador para contar o número de operações de escrita na memória esperadas para cada instrução. Certifique-se de que as duas contagens sejam consistentes definindo uma restrição de igualdade. A lógica deste método é muito intuitiva: cada vez que uma operação de escrita for realizada na memória, ela será contada uma vez, devendo haver um registro correspondente na tabela da memória. Portanto, o invasor não pode inserir nenhuma entrada adicional na tabela de memória.
A afirmação lógica acima é um pouco vaga e, no processo de prova mecanizada, precisa ser mais precisa. Primeiro, precisamos revisar a afirmação do lema de escrita em memória mencionado acima. Definimos a função `mops_at eid type` para contar as entradas da tabela de memória com um determinado `eid` e `type` (a maioria das instruções criará 0 ou 1 entradas em um eid ). A declaração completa do teorema tem um pré-requisito adicional afirmando que não há entradas falsas na tabela de memória:
Se as seguintes restrições forem válidas
(valor de deslocamento do tipo memory_table_lookup_write_cell eid)
E as seguintes novas restrições são estabelecidas
(tipo mops_at eid) = 1
mas
(memory_at(eid+ 1) type) = definir o valor de deslocamento (memory_at eid type)
Isto exige que a nossa verificação seja mais precisa do que no caso anterior. Meramente derivar da restrição de igualdade de que o número total de entradas da tabela de memória é igual ao número total de gravações de memória na execução não é suficiente para completar a verificação. Para provar a correção de uma instrução, precisamos saber que cada instrução corresponde ao número correto de entradas da tabela de memória. Por exemplo, precisamos descartar se um invasor poderia omitir uma entrada na tabela de memória para uma instrução na sequência de execução e criar uma nova entrada maliciosa na tabela de memória para outra instrução não relacionada.
Para provar isso, usamos uma abordagem top-down para limitar o número de entradas da tabela de memória correspondentes a uma determinada instrução, o que envolve três etapas. Primeiro, estimamos o número de entradas que devem ser criadas para instruções na sequência de execução com base no tipo de instrução. Chamamos o número esperado de gravações da i-ésima etapa até o final da execução de `instructions_mops i`, e o número correspondente de entradas na tabela de memória da i-ésima instrução até o final da execução de `cum_mops (eid i) `. Ao analisar as restrições de pesquisa de cada instrução, podemos provar que ela não cria menos entradas do que o esperado, o que leva à conclusão de que cada segmento de [i... numRows] rastreado cria não menos entradas do que o esperado:
Lema cum_mops_bound': forall n i,
0 ≤ eu ->
i + Z.of_nat n = etable_numRow ->
MTable.cum_mops (etable_values eid_cell i) (max_eid+ 1) ≥ instruções_mops' i n.
Segundo, se você puder mostrar que a tabela não possui mais entradas do que o esperado, então ela possui exatamente o número certo de entradas, o que é óbvio.
Lema cum_mops_equal': para todos n i,
0 ≤ eu ->
i + Z.of_nat n = etable_numRow ->
MTable.cum_mops (etable_values eid_cell i) (max_eid+ 1) ≤ instruções_mops' i n ->
MTable.cum_mops (etable_values eid_cell i) (max_eid+ 1) = instruções_mops' i n.
Agora prossiga para a etapa três. Nosso teorema de correção afirma que para qualquer n, cum_mops e instruções_mops são sempre consistentes da linha n até o final da tabela:
Lema cum_mops_equal: para todos n,
0 <= Z.of_nat n < etable_numRow ->
MTable.cum_mops (etable_values eid_cell (Z.of_nat n)) (max_eid+ 1) = instruções_mops (Z.of_nat n)
A verificação é completada resumindo n. A primeira linha da tabela é a restrição de igualdade do zkWasm, indicando que o número total de entradas na tabela de memória está correto, ou seja, cum_mops 0 = instruções_mops 0 . Para as linhas seguintes, a hipótese indutiva nos diz:
cum_mops n = instruções_mops n
e esperamos provar
cum_mops (n+ 1) = instruções_mops (n+ 1)
Preste atenção aqui
cum_mops n = mop_at n + cum_mops (n+ 1)
e
instruções_mops n = instruções_mops n + instruções_mops (n+ 1)
Portanto, podemos obter
mops_at n + cum_mops (n+ 1) = instrução_mops n + instruções_mops (n+ 1)
Anteriormente, mostramos que cada instrução criará não menos que o número esperado de entradas, por ex.
mops_at n ≥ instrução_mops n.
Então pode-se concluir
cum_mops (n+ 1) ≤ instruções_mops (n+ 1)
Aqui precisamos aplicar o segundo lema acima.
(Usando um lema semelhante para verificar a tabela de salto, pode-se provar que cada instrução de chamada pode produzir com precisão uma entrada na tabela de salto, portanto, esta técnica de prova é geralmente aplicável. No entanto, ainda precisamos de mais trabalho de verificação para provar que o retorno Correção de a instrução. O eid retornado é diferente do eid da instrução de chamada que criou o quadro de chamada, portanto, também precisamos de uma propriedade invariante adicional para declarar que o valor de eid é incrementado em uma direção durante a sequência de execução.)
Descrever o processo de prova com tantos detalhes é típico da verificação formal e é a razão pela qual a verificação de um trecho específico de código geralmente leva mais tempo do que escrevê-lo. Mas compensa? Valeu a pena neste caso porque encontramos um bug crítico no mecanismo de contagem da tabela de saltos durante a prova. Esse bug foi descrito em detalhes em um artigo anterior - em resumo, versões mais antigas do código eram responsáveis por instruções de chamada e retorno, e um invasor poderia criar um salto falso adicionando instruções de retorno adicionais às entradas da tabela de execução para abrir espaço. . Embora um mecanismo de contagem incorreto possa satisfazer a intuição de que toda instrução de chamada e retorno conta, surgem problemas quando tentamos refinar essa intuição em uma declaração de teorema mais precisa.
Torne o processo de prova modular
Pela discussão acima, podemos ver que existe uma dependência circular entre a prova sobre o circuito de cada instrução e a prova sobre a coluna de contagem da tabela de execução. Para provar a exatidão do circuito de instrução, precisamos raciocinar sobre as gravações na memória nele, ou seja, precisamos saber o número de entradas da tabela de memória em um EID específico e precisamos provar que a operação de gravação na memória conta; a tabela de execução está correta e também é necessário provar que cada instrução realiza pelo menos um número mínimo de escritas na memória.
Além disso, há outro fator a considerar. O projeto zkWasm é bastante grande, portanto o trabalho de verificação precisa ser modularizado para que vários engenheiros de verificação possam dividir o trabalho. Portanto, atenção especial precisa ser dada à sua complexidade na desconstrução da prova do mecanismo de contagem. Por exemplo, para a instrução LocalGet, dois teoremas são os seguintes:
Teorema opcode_mops_correct_local_get : para todos i,
0 <= i ->
etable_values eid_cell i > 0 ->
opcode_mops_correct LocalGet i.
Teorema LocalGetOp_correct : para todos i st y xs,
0 <= i ->
etable_values enable_cell i = 1 ->
mops_at_correct i ->
etable_values (ops_cell LocalGet) i = 1 ->
state_rel i st ->
wasm_stack st = xs ->
(etable_values offset_cell i) > 1 ->
nth_error xs (Z.to_nat (etable_values offset_cell i - 1)) = Algum y ->
state_rel (i+ 1) (update_stack (incr_iid st) (y :: xs)).
A primeira declaração do teorema
opcode_mops_correct LocalGet i
Quando expandido, significa que a instrução cria pelo menos uma entrada de tabela de memória na linha i (o número 1 é especificado na especificação de opcode LocalGet de zkWasm).
O segundo teorema é o teorema da correção completa da instrução, que cita
mops_at_correct eu
Como hipótese, isso significa que a instrução cria exatamente uma entrada na tabela de memória.
Um engenheiro de verificação pode provar esses dois teoremas independentemente e então combiná-los com uma prova sobre a tabela de execução para provar a correção de todo o sistema. Vale a pena notar que todas as provas para instruções individuais podem ser realizadas no nível das restrições de leitura/gravação sem conhecer a implementação específica da tabela de memória. Portanto, o projeto está dividido em três partes que podem ser tratadas de forma independente.
Resumir
A verificação dos circuitos do zkVM linha por linha não é fundamentalmente diferente da verificação de aplicações ZK em outros campos, porque ambos exigem raciocínio semelhante sobre restrições aritméticas. De uma perspectiva de alto nível, a verificação do zkVM requer muitos dos mesmos métodos de verificação formal usados em interpretadores e compiladores de linguagens de programação. A principal diferença aqui é o estado da máquina virtual dimensionada dinamicamente. No entanto, o impacto dessas diferenças pode ser minimizado estruturando cuidadosamente a estrutura de verificação para corresponder à camada de abstração usada na implementação, permitindo que cada instrução seja implementada como um módulo independente baseado na interface get-set como para um interpretador químico regular. verificação.
