Blockstream has reached a new milestone in Bitcoin development, certifying and verifying a new cryptographic function for Bitcoin: safegcd.
In a world where security and efficiency are crucial to the success of cryptocurrencies, Blockstream, one of the most innovative companies in blockchain technology, has taken a giant step to strengthen Bitcoin’s infrastructure. Recall that Bitcoin’s security relies heavily on digital signature algorithms such as ECDSA, which guarantee the authenticity and integrity of transactions. However, these algorithms face the constant challenge of balancing speed and security, especially when it comes to complex mathematical operations such as modular inverses.
Blockstream has addressed this challenge with the development and implementation of a new algorithm called “safegcd«. This algorithm, which combines speed and security, has undergone rigorous formal verification to ensure its correctness. The result is a significant advancement that not only improves the performance of Bitcoin’s signing and verification operations, but also provides a strong mathematical guarantee of its correct operation. In this article, we will explore how Blockstream has achieved this milestone and what implications it has for the future of Bitcoin.
A huge challenge for Bitcoin security
And at the heart of digital signature and key derivation algorithms is a mathematical operation known as the modular reverseThis operation is relatively expensive in terms of computational resources, which makes it a bottleneck for Bitcoin's performance. But it is also vital for its security, which makes it especially important when it comes to having a good implementation of it.
This has led to two main methods for computing modular inverses: using a technique called “exponent ladder” (very slow) and the Euclidean extended GCD algorithm (fast but difficult to make constant in time). Currently, the libsecp256k1 library, created and used by Bitcoin Core, always opts for the exponent ladder when configuring for use in Bitcoin Core. While secure, this method is notoriously slow, something that limits the wallet’s performance.
Blockstream's solution: Safegcd
To solve this, Blockstream set out to create a GCD implementation that would allow Bitcoin to remain secure at this point, but also allow it to improve network performance. Thus, in 2021, Blockstream implemented a new modular inverse algorithm called “safegcd.” This algorithm, developed by Daniel J. Bernstein and Bo-Yin Yang, offers an alternative that is both fast and constant in time. Safegcd works by iterating a simple calculation until a termination condition is reached. To ensure that the algorithm is constant in time, it can be iterated a fixed number of times, even if the termination condition is reached earlier.
The key to making safegcd constant in time is determining how many iterations are needed for all possible 256-bit inputs (the size of the inputs in the case of secp256k1). Initially, it was estimated that 741 iterations were needed, but Pieter Wuille, an engineer at Blockstream, developed a method to reduce this number to 724 iterations. Later, Wuille and Gregory Maxwell discovered a variant of the algorithm that only requires 590 iterations. This optimization would improve the performance of ECDSA signatures by 25% and signature verification by 15% compared to the exponent ladder.
Formal verification: ensuring correctness
But despite the performance gains, implementing a novel algorithm like safegcd comes with risks. If there is an error in calculating the required iterations, the algorithm might not terminate correctly, resulting in incorrect values and ultimately failed signature verification. This would be devastating for Bitcoin's security.
To mitigate this risk, Blockstream Research performed a formal verification of the safegcd algorithm using the Coq proof assistant. Coq is a tool based on dependent type theory that combines a mathematical deduction system with a functional programming language. This allows for proof by reflection, a method that combines the execution of a functional program with mathematical deduction to verify the correctness of the algorithm.
The formal verification consisted of implementing the convex hull computation algorithm in Coq and proving that this computation is correct. The result is a theorem that guarantees that the safegcd algorithm terminates in 590 iterations. This verification was performed in 2,5 days on commodity hardware, demonstrating the feasibility of the technique.
Implementation in libsecp256k1
La the implementation The development of safegcd in libsecp256k1 was a collaborative effort. Peter Dettman, the developer who implemented the algorithm, worked closely with the Blockstream team to integrate safegcd into the library. The process included adding ctz (count trailing zeros) functions to optimize bit operations, implementing the safegcd algorithm in separate modules, adding extensive testing, and refactoring the code to prepare for the transition to safegcd.
Additionally, additional optimizations were made to improve performance on 32-bit and 64-bit systems. These optimizations are crucial because Bitcoin often runs on very weak hardware, such as mobile devices and embedded systems, where efficiency is vital.
Blockstream's implementation and formal verification of the safegcd algorithm thus represents a significant milestone in Bitcoin's security and efficiency. This development not only improves the performance of signing and verification operations, but also provides mathematical guarantees that the algorithm works correctly.
Furthermore, the formal verification of safegcd demonstrates that it is possible to verify complex and critical software in practice, which opens the door to verification of other functions implemented in libsecp256k1, and could lead to increased security and reliability of the Bitcoin network.
