Overview of the Importance of Secure Bitcoin Signatures
When it comes to the security of cryptocurrencies like Bitcoin and blockchains such as Liquid, one crucial aspect is the use of digital signature algorithms like ECDSA and Schnorr signatures. These algorithms play a vital role in ensuring the authenticity and integrity of transactions. A key component in these algorithms is the use of a mathematical computation known as a modular inverse, which can be resource-intensive.
To address this challenge, a C library called libsecp256k1, named after the elliptic curve it operates on, is utilized by both Bitcoin Core and Liquid to implement these digital signature algorithms. Recently, a new modular inversion algorithm called “safegcd” was developed by Daniel J. Bernstein and Bo-Yin Yang, and later implemented for libsecp256k1 by Peter Dettman in 2021. As part of the validation process for this novel algorithm, Blockstream Research conducted a formal verification using the Coq proof assistant to ensure the algorithm terminates correctly with the expected modular inverse result on 256-bit inputs.
Addressing the Gap Between Algorithm Design and Implementation
While the formal verification confirmed the correctness of the safeguard algorithm, implementing it in libsecp256k1 required translating the mathematical description into C programming language. This presented challenges as the C language only supports integers up to 64 bits (or 128 bits with extensions), while the algorithm involved operations on 256-bit integers. Multiple optimizations were made to the implementation to ensure efficiency, resulting in four separate implementations of the safeguard algorithm in libsecp256k1 tailored for different systems.
Ensuring Correctness of the C Code Implementation
To verify that the C code accurately reflects the safeguard algorithm, Verifiable C, a tool within the Verified Software Toolchain, was utilized. This tool allows for reasoning about C code using the Coq theorem prover, enabling the specification of preconditions and postconditions for each function undergoing verification. Separation logic, specialized for reasoning about memory allocations and more, was employed to establish invariants at each step of the function, ensuring the correctness of the implementation.
Challenges and Limitations in Verification
While the verification process confirmed the functional correctness of the safeguard algorithm implementation, there are limitations to be aware of. The partial correctness of separation logic only guarantees the correct result if the code terminates, not the termination itself. Additionally, the lack of a formal specification for the C language necessitated the use of the CompCert compiler project to ensure correctness when compiled. Furthermore, limitations in Verifiable C’s support for structure operations required adjustments in the code to accommodate these constraints.
Conclusion
Blockstream Research’s successful verification of libsecp256k1’s modular inverse function demonstrates the feasibility of verifying C code in practice. This achievement showcases the potential for ensuring software correctness in complex mathematical implementations. With the possibility of extending verification to other functions within libsecp256k1, the potential for achieving the highest level of software correctness guarantees is within reach.
This post was written by Russell O’Connor and Andrew Poelstra. The views expressed are their own and do not necessarily reflect those of BTC Inc or Bitcoin Magazine.