Verificando formalmente as especificações do Ethereum 2.0 Fase 0

NewsDevelopersEnterpriseBlockchain ExplainedEvents and ConferencesPressboletins informativos

Assine a nossa newsletter.

Endereço de email

Nós respeitamos sua privacidade

HomeBlogBlockchain Development

Verificando formalmente as especificações do Ethereum 2.0 Fase 0

Uma atualização do ConsenSys R&D em seu esforço para trazer confiabilidade à Rede Beacon e aos principais fundamentos da Eth2. por Franck Cassez 10 de agosto de 2020Postado em 10 de agosto de 2020

A equipe de verificação automatizada no ConsenSys R&D tenho trabalhado em uma especificação formal e verificação da cadeia de balizas por alguns meses. Temos o prazer de informar que muito progresso foi feito e embora ainda não tenhamos concluído, conseguimos desenvolver um kernel sólido e formalmente verificado da cadeia Beacon. Pela primeira vez, nosso trabalho fornece um nível incomparável de confiabilidade para os principais alicerces da infraestrutura Eth2.0.

Metodologia

Verificação vs. Teste

Usamos o premiado linguagem de programação com reconhecimento de verificação Dafny escrever um formal (funcional e lógico) especificação de cada função Beacon Chain, um implementação de cada função, e um prova que a implementação está de acordo com sua especificação. Em outras palavras, verificamos matematicamente a ausência de bugs. As implementações que eventualmente provamos corretas são baseadas em as especificações oficiais Eth2.0 com a ressalva de que corrigimos e relatamos alguns bugs e inconsistências.

Nossa metodologia é diferente de testar enquanto nós provar matematicamente conformidade das funções com suas especificações, para todo entradas. O teste não pode abranger um número infinito de entradas e, como consequência, pode descobrir bugs, mas não provar a ausência de bugs.

E o melhor é que não precisamos publicar um paper nem revisar as provas. As provas são parte da base do código e escritas como programas. Sim, no Dafny, você pode escrever uma prova como um programa amigável para o desenvolvedor. Também o as provas são verificadas mecanicamente por um provador de teorema, não deixando espaço para provas incompletas ou falhas.

Propriedades que provamos

As propriedades variam desde a ausência de aritmética sob / overflows e Índice fora dos limites, a conformidade de cada função com as pré / pós-condições lógicas (lógica de primeira ordem) (exemplo merkelise aqui), para as mais complexas envolvendo composições de funções. Por exemplo, temos o seguinte propriedade do SSZ Serializar / desserializar funções: para cada objeto x, desserializar (serializar (x)) = x, ou seja, desserializar um objeto serializado retorna o objeto original. Também estabelecemos um número de invariantes, e os utilizou para provar que as operações centrais da Beacon Chain e ForkChoice (state_transition, on_block) na realidade construir uma cadeia de blocos: para qualquer bloco b na loja, os ancestrais de b formam uma sequência finita totalmente ordenada que leva ao bloco de gênese, que é a propriedade principal de um blockchain!

Os benefícios da verificação formal

Qualquer metodista formal insistiria que a verificação é uma prática recomendada de segurança. Veja exatamente como essa metodologia garante uma infraestrutura segura e confiável para Ethereum 2.0.

Especificação funcional

Primeiro, elevamos as especificações oficiais Eth2.0 para um especificação lógica e funcional formal. Para cada função, definimos formalmente o que se espera que a função calcule, não como. Isso fornece especificações de referência amigáveis ao desenvolvedor independente de idioma que podem ser usados para desenvolver implementações mais seguras, com menos esforço.

Modularidade

Em segundo lugar, nossas especificações, implementações e arquitetura de prova são modular. Como resultado, podemos facilmente experimente novas implementações (por exemplo, otimizações) e verificar seu impacto no sistema geral. Pense em um hack inteligente para implementar uma função? Altere a implementação e peça a Dafny para verificar se ainda está em conformidade com suas especificações. Em caso afirmativo, as provas dos componentes que usam esta função não são afetadas.

Executabilidade

Terceiro, nossas implementações são executável. Podemos compilar e executar um programa Dafny. Melhor ainda, você pode automaticamente gerar código em algumas linguagens de programação populares como C #, Go (e logo Java) do código Dafny. Isso pode ser usado para complementar as bases de código existentes ou para gerar testes certificados. A implementação a ser testada pode usar nossas funções comprovadamente corretas para calcular o resultado esperado de um teste e compará-lo com seu próprio resultado.

Tudo em um único idioma

Por último, mas não menos importante, nossa base de código é independente. Ele contém as especificações, implementações, documentações e provas, tudo em uma linguagem de programação única, legível, simples e semanticamente bem definida.

Perguntas e considerações

E sobre a solidez do mecanismo de verificação?

Você pode estar se perguntando: “e se o compilador / verificador Dafny tiver bugs?” Na verdade, sabemos que Dafny tem erros (problemas de repo dafny), mas não contamos com a ausência de bugs no Dafny. Contamos com Dafny (e seu mecanismo de verificação) para ser som. Solidez significa que quando Dafny relata que as provas estão corretas, elas estão de fato corretas.

E se a especificação que escrevemos não for a correta?

Nesse caso, provaríamos conformidade com um requisito incorreto. Sim, isso pode acontecer e não existe solução mágica para resolver este problema. No entanto, como mencionamos antes, Dafny é executável. Isso nos permite executar o código e ter alguma confiança de que nossas especificações são as corretas. E nossas especificações são escritas em lógica de primeira ordem, sem espaço para disputa sobre o significado, portanto, se você notar um problema, nos informe e nós o corrigiremos.

E se Dafny não puder provar que uma implementação está em conformidade com uma especificação?

Isso pode acontecer, mas, neste caso, Dafny tem alguns mecanismos de feedback para ajudar a investigar quais etapas de uma prova não podem ser verificadas. E até agora, sempre conseguimos construir provas que Dafny pode verificar automaticamente.

Agradecemos o seu feedback, por favor verifique nosso repositório eth2.0-dafny. Estamos entusiasmados em ver o desenvolvimento do Ethereum 2.0 atingir seus marcos recentes do testnet e esperamos trabalhar com equipes em todo o ecossistema para garantir que a próxima fase da rede seja construída sobre uma base sólida.

Agradecimento: obrigado aos meus companheiros de equipe Joanne Fuller, Roberto Saltini (equipe de verificação automatizada), Nicolas Liochon e Avery Erwin pelos comentários sobre uma versão preliminar deste post.

Acompanhe o Ethereum 2.0

Assine o boletim informativo da ConsenSys para receber as últimas notícias da Eth2 diretamente na sua caixa de entrada. Se inscrever Ethereum 2.0Pesquisa e DesenvolvimentoSegurançaNewsletterSubscreva nossa newsletter para obter as últimas notícias da Ethereum, soluções empresariais, recursos para desenvolvedores e muito mais.Endereço de e-mailConteúdo exclusivoWebinar