A Blockstream atingiu um novo marco no desenvolvimento do Bitcoin, certificando e verificando uma nova função criptográfica para Bitcoin: safegcd.
Num mundo onde a segurança e a eficiência são cruciais para o sucesso das criptomoedas, a Blockstream, uma das empresas mais inovadoras na tecnologia blockchain, deu um passo gigante para fortalecer a infraestrutura Bitcoin. Lembremos que a segurança do Bitcoin depende em grande parte de algoritmos de assinatura digital como o ECDSA, que garantem a autenticidade e integridade das transações. No entanto, esses algoritmos enfrentam o desafio constante de equilibrar velocidade e segurança, especialmente quando se trata de operações matemáticas complexas, como inversas modulares.
A Blockstream enfrentou esse desafio com o desenvolvimento e implementação de um novo algoritmo chamado “seguro«. Este algoritmo, que combina velocidade e segurança, passou por rigorosa verificação formal para garantir sua correção. O resultado é um avanço significativo que não só melhora o desempenho das operações de assinatura e verificação do Bitcoin, mas também fornece uma forte garantia matemática de seu correto funcionamento. Neste artigo, exploraremos como a Blockstream alcançou esse marco e quais implicações isso tem para o futuro do Bitcoin.
Um enorme desafio para a segurança do Bitcoin
E no centro da assinatura digital e dos algoritmos de derivação de chave está uma operação matemática conhecida como reverso modular. Esta operação é relativamente cara em termos de recursos computacionais, tornando-se um gargalo para o desempenho do Bitcoin. Mas também é vital para a sua segurança, o que o torna especialmente importante quando se trata de uma boa implementação.
Isto levou a dois métodos principais para calcular inversos modulares: o uso de uma técnica chamada “escada de expoentes” (muito lenta) e o algoritmo GCD estendido de Euclides (rápido, mas difícil de tornar constante no tempo). Atualmente, a biblioteca libsecp256k1, criada e utilizada pelo Bitcoin Core, sempre opta pela escada de expoentes quando configurada para uso no Bitcoin Core. Embora seguro, este método é notoriamente lento, o que limita o desempenho da carteira.
Solução da Blockstream: Safegcd
Para resolver isso, a Blockstream decidiu criar uma implementação GCD que manteria o Bitcoin seguro neste ponto, mas também permitiria melhorar o desempenho da rede. Foi assim que em 2021, a Blockstream implementou um novo algoritmo inverso modular chamado “safegcd”. Este algoritmo, desenvolvido por Daniel J. Bernstein e Bo-Yin Yang, oferece uma alternativa rápida e constante no tempo. Safegcd funciona iterando um cálculo simples até que uma condição de encerramento seja alcançada. Para garantir que o algoritmo seja constante no tempo, ele pode ser iterado um número fixo de vezes, mesmo que a condição de término seja atingida antecipadamente.
A chave para tornar safegcd constante no tempo é determinar quantas iterações são necessárias para todas as entradas possíveis de 256 bits (o tamanho das entradas no caso de secp256k1). Inicialmente, estimou-se que seriam necessárias 741 iterações, mas Pieter Wuille, engenheiro da Blockstream, desenvolveu um método para reduzir esse número para 724 iterações. Mais tarde, Wuille e Gregory Maxwell descobriram uma variante do algoritmo que requer apenas 590 iterações. Esta otimização melhoraria o desempenho das assinaturas ECDSA em 25% e a verificação de assinaturas em 15% em comparação com a escada de expoentes.
Verificação formal: garantindo a correção
Mas, apesar das melhorias de desempenho, a implementação de um novo algoritmo como o safegcd traz riscos. Se houver um erro no cálculo das iterações necessárias, o algoritmo pode não terminar corretamente, resultando em valores incorretos e, por fim, falha na verificação da assinatura. Isso seria devastador para a segurança do Bitcoin.
Para mitigar esse risco, a Blockstream Research realizou uma verificação formal do algoritmo safegcd usando o assistente de teste Coq. Coq é uma ferramenta baseada na teoria dos tipos dependentes que combina um sistema de dedução matemática com uma linguagem de programação funcional. Isso permite testar por reflexão, método que combina a execução de um programa funcional com dedução matemática para verificar a correção do algoritmo.
A verificação formal consistiu em implementar o algoritmo de cálculo do casco convexo no Coq e comprovar que esse cálculo está correto. O resultado é um teorema que garante que o algoritmo safegcd termine em 590 iterações. Esta verificação foi realizada em 2,5 dias em hardware de consumo, demonstrando a viabilidade da técnica.
Implementação em libseCP256k1
La implementação do safegcd em libseCP256k1 foi um esforço colaborativo. Peter Dettman, o desenvolvedor que implementou o algoritmo, trabalhou em estreita colaboração com a equipe Blockstream para integrar o safegcd à biblioteca. O processo incluiu a adição de funções ctz (contagem de zeros à direita) para otimizar as operações de bits, a implementação do algoritmo safegcd em módulos separados, a adição de testes extensivos e a refatoração do código para se preparar para a transição para o safegcd.
Além disso, otimizações adicionais foram feitas para melhorar o desempenho em sistemas de 32 e 64 bits. Essas otimizações são cruciais porque o Bitcoin geralmente funciona em hardware muito fraco, como dispositivos móveis e sistemas embarcados, onde a eficiência é vital.
Desta forma, a implementação e verificação formal do algoritmo safegcd pela Blockstream representa um marco significativo na segurança e eficiência do Bitcoin. Este desenvolvimento não só melhora o desempenho das operações de assinatura e verificação, mas também fornece garantias matemáticas de que o algoritmo funciona corretamente.
Além disso, a verificação formal do safegcd demonstra que é possível verificar na prática softwares complexos e críticos, o que abre a porta para a verificação de outras funções implementadas no libsecp256k1, podendo levar a maior segurança e confiabilidade na rede Bitcoin.
