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<\/em>, which constitutes a relatively resource-intensive aspect of the calculations.<\/p>\n In \u201cFast constant-time gcd computation and modular inversion<\/a>,\u201d Daniel J. Bernstein and Bo-Yin Yang introduce a new modular inversion method. In 2021, this method, termed \u201csafegcd,\u201d was applied<\/a> 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<\/a> of the algorithm\u2019s structure, utilizing the Coq proof assistant to confirm that the algorithm does indeed complete with the correct modular inverse output for 256-bit inputs.<\/p>\n 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).<\/p>\n To implement the safegcd algorithm, one needs to program the matrix multiplication and other calculations utilizing C\u2019s 64-bit integers. Furthermore, numerous additional enhancements<\/a> 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.<\/p>\n To ensure that the C code accurately executes the safegcd algorithm, all implementation specifics must be scrutinized. We use Verifiable C<\/a>, a part of the Verified Software Toolchain, for reasoning about C code with the aid of the Coq theorem prover.<\/p>\n The verification process commences by outlining preconditions and postconditions using separation logic for each function subjected to verification. Separation logic<\/a> is a logic tailored for reasoning about subroutines, memory allocations, concurrency, and more.<\/p>\n After assigning a specification to each function, verification moves forward by starting from a function\u2019s 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 \u201cbetween\u201d 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.<\/p>\n The final outcome is a formal proof<\/a>, validated by the Coq proof assistant, demonstrating that libsecp256k1\u2019s 64-bit variable time implementation of the safegcd modular inverse algorithm is functionally sound.<\/p>\n There are several constraints to the proof of functional correctness. The separation logic employed in Verifiable C enforces what is termed as partial correctness<\/a>. This indicates that it only certifies the C code returns with the correct result if<\/em> it returns, but it does not ensure termination itself. We address this limitation by utilizing our prior Coq proof<\/a> regarding the bounds on the safegcd algorithm to confirm that the loop counter in the primary loop never surpasses 11 iterations.<\/p>\n Another concern is that the C language lacks a formal specification. Instead, the Verifiable C project employs the CompCert compiler project<\/a> 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<\/a> in practical scenarios.<\/p>\n 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.<\/p>\n Blockstream Research has formally validated the accuracy of libsecp256k1\u2019s 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.<\/p>\n 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.<\/p>\nThe Disparity between Algorithm and Implementation<\/h2>\n
Verifiable C<\/h2>\n
Constraints of the Verification<\/h2>\n
Conclusion<\/h2>\n