A segurança do Bitcoin e de outras blockchains, como a Liquid, depende de algoritmos de assinatura digital como ECDSA e assinaturas Schnorr. Uma biblioteca C chamada libsecp256k1 fornece esses algoritmos e é usada tanto pelo Bitcoin Core quanto pela Liquid. Esses algoritmos usam um cálculo chamado inverso modular, que é uma parte cara do processo.
Em “Cálculo rápido de gcd em tempo constante e inversão modular”, Daniel J. Bernstein e Bo-Yin Yang criaram um novo algoritmo de inversão modular chamado “safegcd.” Este algoritmo foi implementado para o libsecp256k1 por Peter Dettman em 2021. A Blockstream Research verificou formalmente o design do algoritmo usando o assistente de prova Coq, mostrando que ele calcula corretamente o inverso modular para entradas de 256 bits.
No entanto, a implementação do algoritmo safegcd exigiu adaptar a descrição matemática para se encaixar na linguagem de programação C, que suporta nativamente apenas inteiros de até 64 bits. Várias otimizações foram adicionadas para tornar a implementação rápida, resultando em quatro implementações separadas do algoritmo safegcd no libsecp256k1.
Para garantir que o código C implemente corretamente o algoritmo safegcd, o C Verificável, parte da Ferramenta de Software Verificado, foi usado com o provador de teoremas Coq. Isso envolveu especificar pré-condições e pós-condições para cada função em verificação usando lógica de separação. O processo de verificação então começou a partir da pré-condição da função e estabeleceu um novo invariável após cada declaração no corpo da função, até que a pós-condição fosse alcançada no final do corpo da função ou nas declarações de retorno.
A maior parte do esforço de formalização foi gasto traduzindo as operações brutas de cada expressão C em declarações de nível superior sobre o que as estruturas de dados sendo manipuladas representam matematicamente. A verificação resultou em uma prova formal, verificada pelo assistente de prova Coq, de que a implementação de tempo variável de 64 bits do algoritmo de inverso modular safegcd do libsecp256k1 é funcionalmente correta.
No entanto, existem algumas limitações na prova de correção funcional. A lógica de separação usada em C Verificável prova apenas a correção parcial, o que significa que ela apenas mostra que o código C retorna o resultado correto se retornar, mas não prova a terminação em si. Para abordar isso, uma prova anterior do Coq dos limites do algoritmo safegcd foi usada para provar que o valor do contador do loop do loop principal nunca excede 11 iterações.
Outra limitação é que a linguagem C em si não possui uma especificação formal. Em vez disso, o projeto C Verificável usa o projeto de compilador CompCert para fornecer uma especificação formal da linguagem C. Isso garante que, quando um programa C verificado é compilado com o compilador CompCert, o código de montagem resultante atenderá à sua especificação, mas não garante que o código gerado por outros compiladores funcionará necessariamente.
Além disso, C Verificável não suporta passar, retornar ou atribuir estruturas. No libsecp256k1, as estruturas são sempre passadas por ponteiro, o que é permitido em C Verificável, mas há algumas ocasiões em que a atribuição de estruturas é usada. Em resumo, a Blockstream Research verificou formalmente a correção da função de inverso modular do libsecp256k1, fornecendo mais evidências de que a verificação de código C é possível na prática.
Este trabalho também destaca que o restante das funções implementadas no libsecp256k1 poderia ser verificado também, permitindo que a biblioteca alcançasse as maiores garantias possíveis de correção de software.
Fonte
<p>O post Como as Assinaturas Digitais Tornam o Bitcoin Seguro! apareceu primeiro no CoinBuzzFeed.</p>
