Introdução
A segurança do Bitcoin e de outros blockchains, como o Liquid, depende do uso de algoritmos de assinaturas digitais, como as assinaturas ECDSA e Schnorr. A biblioteca AC chamada libsecp256k1, em homenagem à curva elíptica na qual a biblioteca opera, é usada tanto pelo Bitcoin Core quanto pelo Liquid, para fornecer esses algoritmos de assinatura digital. Esses algoritmos fazem uso de um cálculo matemático chamado modular inversoque é um componente relativamente caro do cálculo.
Em “Cálculo gcd rápido em tempo constante e inversão modular”, Daniel J. Bernstein e Bo-Yin Yang desenvolvem um novo algoritmo de inversão modular. Em 2021, este algoritmo, conhecido como “safegcd”, foi implementado para libsecp256k1 por Peter Dettman. Como parte do processo de verificação deste novo algoritmo, a Blockstream Research foi a primeira a concluir uma verificação formal do design do algoritmo usando o assistente de prova Coq para verificar formalmente se o algoritmo realmente termina com o resultado inverso modular correto em 256 bits. entradas.
A lacuna entre algoritmo e implementação
O esforço de formalização em 2021 apenas mostrou que o algoritmo desenhado por Bernstein e Yang funciona corretamente. No entanto, o uso desse algoritmo em libsecp256k1 requer a implementação da descrição matemática do algoritmo safegcd na linguagem de programação C. Por exemplo, a descrição matemática do algoritmo realiza a multiplicação de matrizes de vetores que podem ter a largura de inteiros com sinal de 256 bits, no entanto, a linguagem de programação C fornecerá nativamente apenas números inteiros de até 64 bits (ou 128 bits com algumas extensões de linguagem).
A implementação do algoritmo safegcd requer a programação da multiplicação de matrizes e outros cálculos usando inteiros de 64 bits de C. Além disso, muitas outras otimizações foram adicionadas para tornar a implementação mais rápida. No final, existem quatro implementações separadas do algoritmo safegcd em libsecp256k1: dois algoritmos de tempo constante para geração de assinatura, um otimizado para sistemas de 32 bits e outro otimizado para sistemas de 64 bits, e dois algoritmos de tempo variável para verificação de assinatura, novamente um para sistemas de 32 bits e outro para sistemas de 64 bits.
C verificável
Para verificar se o código C implementa corretamente o algoritmo safegcd, todos os detalhes de implementação devem ser verificados. Usamos Verifiable C, parte do Verified Software Toolchain para raciocinar sobre o código C usando o provador do teorema Coq.
A verificação prossegue especificando pré-condições e pós-condições usando lógica de separação para cada função submetida à verificação. A lógica de separação é uma lógica especializada para raciocinar sobre sub-rotinas, alocações de memória, simultaneidade e muito mais.
Uma vez que cada função recebe uma especificação, a verificação prossegue começando pela pré-condição de uma função e estabelecendo uma nova invariante após cada instrução no corpo da função, até finalmente estabelecer a pós-condição no final do corpo da função ou no final de cada declaração de retorno. A maior parte do esforço de formalização é gasto “entre” as linhas de código, usando os invariantes para traduzir as operações brutas de cada expressão C em declarações de nível superior sobre o que as estruturas de dados que estão sendo manipuladas representam matematicamente. Por exemplo, o que a linguagem C considera um array de números inteiros de 64 bits pode na verdade ser uma representação de um número inteiro de 256 bits.
O resultado final é uma prova formal, verificada pelo assistente de prova Coq, de que a implementação de tempo variável de 64 bits do algoritmo inverso modular safegcd da libsecp256k1 está funcionalmente correta.
Limitações da Verificação
Existem algumas limitações para a prova de correção funcional. A lógica de separação usada em Verifiable C implementa o que é conhecido como correção parcial. Isso significa que apenas prova que o código C retorna com o resultado correto se ele retorna, mas não prova o término em si. Mitigamos essa limitação usando nossa prova Coq anterior dos limites do algoritmo safegcd para provar que o valor do contador de loop do loop principal de fato nunca excede 11 iterações.
Outra questão é que a própria linguagem C não possui especificação formal. Em vez disso, o projeto Verifiable C usa o projeto do compilador CompCert para fornecer uma especificação formal de uma linguagem C. Isso garante que quando um programa C verificado for compilado com o compilador CompCert, o código assembly resultante atenderá às suas especificações (sujeito à limitação acima). No entanto, isso não garante que o código gerado pelo GCC, clang ou qualquer outro compilador funcione necessariamente. Por exemplo, os compiladores C podem ter ordens de avaliação diferentes para argumentos em uma chamada de função. E mesmo que a linguagem C tivesse uma especificação formal, qualquer compilador que não fosse formalmente verificado ainda poderia compilar programas incorretamente. Isso ocorre na prática.
Por último, Verifiable C não suporta passagem de estruturas, retorno de estruturas ou atribuição de estruturas. Enquanto em libsecp256k1 as estruturas são sempre passadas por ponteiro (o que é permitido em Verifiable C), há algumas ocasiões em que a atribuição de estrutura é usada. Para a prova modular de correção inversa, houve 3 atribuições que tiveram que ser substituídas por uma chamada de função especializada que realiza a atribuição da estrutura campo por campo.
Resumo
A Blockstream Research verificou formalmente a exatidão da função inversa modular do libsecp256k1. Este trabalho fornece mais evidências de que a verificação do código C é possível na prática. Usar um assistente de prova de uso geral nos permite verificar software construído com base em argumentos matemáticos complexos.
Nada impede que o restante das funções implementadas em libsecp256k1 também sejam verificadas. Assim, é possível que libsecp256k1 obtenha as mais altas garantias possíveis de correção de software.
Este é um post convidado de Russell O'Connor e Andrew Poelstra. As opiniões expressas são inteiramente próprias e não refletem necessariamente as da BTC Inc ou da Bitcoin Magazine.
Fonte: bitcoinmagazine.com
