Overview
The protection of Bitcoin and other blockchains, like Liquid, relies on the implementation of digital signature algorithms, including ECDSA and Schnorr signatures. A C library known as libsecp256k1, named after the elliptic curve it functions on, is utilized by both Bitcoin Core and Liquid to offer these digital signature algorithms. These algorithms incorporate a mathematical process known as a modular inverse, which constitutes a relatively resource-intensive aspect of the calculations.
In “Fast constant-time gcd computation and modular inversion,” Daniel J. Bernstein and Bo-Yin Yang introduce a new modular inversion method. In 2021, this method, termed “safegcd,” was applied to libsecp256k1 by Peter Dettman. As part of the evaluation process for this innovative algorithm, Blockstream Research was the first to execute a formal validation of the algorithm’s structure, utilizing the Coq proof assistant to confirm that the algorithm does indeed complete with the correct modular inverse output for 256-bit inputs.
The Disparity between Algorithm and Implementation
The formalization initiative in 2021 simply demonstrated that the algorithm created by Bernstein and Yang functions accurately. However, employing that algorithm in libsecp256k1 necessitates the translation of the mathematical characterization of the safegcd algorithm into the C programming language. For instance, the mathematical representation of the algorithm executes matrix multiplication of vectors that can extend up to 256 bit signed integers, but the C programming language primarily supports integers up to 64 bits (or 128 bits with certain language extensions).
To implement the safegcd algorithm, one needs to program the matrix multiplication and other calculations utilizing C’s 64-bit integers. Furthermore, numerous additional enhancements have been incorporated to accelerate the implementation. Ultimately, there are four distinct implementations of the safegcd algorithm in libsecp256k1: two constant time algorithms for signature generation, one tailored for 32-bit systems and another for 64-bit systems, alongside two variable time algorithms for signature validation, again one for 32-bit systems and one for 64-bit systems.
Verifiable C
To ensure that the C code accurately executes the safegcd algorithm, all implementation specifics must be scrutinized. We use Verifiable C, a part of the Verified Software Toolchain, for reasoning about C code with the aid of the Coq theorem prover.
The verification process commences by outlining preconditions and postconditions using separation logic for each function subjected to verification. Separation logic is a logic tailored for reasoning about subroutines, memory allocations, concurrency, and more.
After assigning a specification to each function, verification moves forward by starting from a function’s precondition, establishing a new invariant after each statement within the function body, culminating in the establishment of the postcondition at the conclusion of the function body or at the end of each return statement. Much of the formalization effort is concentrated “between” the lines of code, employing the invariants to interpret the basic operations of each C expression into more abstract statements about what the data structures being manipulated signify mathematically. For instance, what the C language perceives as an array of 64-bit integers may, in actuality, represent a 256-bit integer.
The final outcome is a formal proof, validated by the Coq proof assistant, demonstrating that libsecp256k1’s 64-bit variable time implementation of the safegcd modular inverse algorithm is functionally sound.
Constraints of the Verification
There are several constraints to the proof of functional correctness. The separation logic employed in Verifiable C enforces what is termed as partial correctness. This indicates that it only certifies the C code returns with the correct result if it returns, but it does not ensure termination itself. We address this limitation by utilizing our prior Coq proof regarding the bounds on the safegcd algorithm to confirm that the loop counter in the primary loop never surpasses 11 iterations.
Another concern is that the C language lacks a formal specification. Instead, the Verifiable C project employs the CompCert compiler project to provide a formal specification of the C language. This ensures that when a verified C program is compiled using the CompCert compiler, the resulting assembly code will adhere to its specification (subject to the aforementioned limitation). Nevertheless, this does not guarantee that the code produced by GCC, clang, or any other compiler will necessarily function correctly. For instance, C compilers may follow different evaluation orders for arguments within a function call. Even if the C language had a formal specification, any compiler that is not itself formally verified could still miscompile programs. This does occur in practical scenarios.
Finally, Verifiable C does not accommodate passing structures, returning structures, or assigning structures. Although in libsecp256k1, structures are consistently passed by pointer (which is permitted in Verifiable C), there are some instances where structure assignments are utilized. For the modular inverse correctness proof, there were 3 assignments that needed to be substituted with a specialized function call that executes the structure assignment field by field.
Conclusion
Blockstream Research has formally validated the accuracy of libsecp256k1’s modular inverse function. This initiative further substantiates that the verification of C code is feasible in real-world applications. Employing a general-purpose proof assistant enables us to validate software constructed upon intricate mathematical foundations.
There is nothing preventing the rest of the functions implemented within libsecp256k1 from being verified as well. Thus, it remains possible for libsecp256k1 to achieve the highest attainable software correctness guarantees.
This is a guest article by Russell O’Connor and Andrew Poelstra. The views expressed are solely their own and do not necessarily represent those of BTC Inc or Bitcoin Magazine.