比特币libsecp256k1中safegcd算法形式化验证完成

1. 引言

比特币和其他链（如 Liquid）的安全性取决于 ECDSA 和 Schnorr 签名等数字签名算法的使用。Bitcoin Core 和 Liquid 都使用名为 libsecp256k1 的 C 库来提供这些数字签名算法，该库以其所运行的椭圆曲线命名。这些算法利用一种称为modular inverse模逆的数学计算，这是计算中相对昂贵的组成部分。

• 2019年：Daniel J. Bernstein 和 Bo-Yin Yang 2019年论文 Fast constant-time gcd computation and modular inversion 中，开发了一种新的模逆算法。
• 2021 年，Peter Dettman 为 libsecp256k1实现了这种称为“safegcd”的算法。详情见：Safegcd inverses, drop Jacobi symbols, remove libgmp #831。

作为safegcd这种新算法审查过程的一部分，Blockstream Research 率先完成了该算法设计的形式化验证（见2021年2月 Blockstream团队Russell O’Connor 和 Andrew Poelstra 博客 A Formal Proof of safegcd Bounds），使用 Coq 证明助手形式化验证了该算法确实在 256 位输入上以正确的模逆结果终止。

2. 算法与实现之间的差距

2021 年的形式化工作仅表明 Bernstein 和 Yang 设计的算法可以正常工作。但是，在 libsecp256k1 中使用该算法需要在 C 编程语言中实现 safegcd 算法的数学描述。如，该算法的数学描述执行向量的矩阵乘法，这些向量的宽度可以达到 256 位有符号整数，但是 C 编程语言本身只会提供高达 64 位（或使用某些语言扩展的 128 位）的整数。

• 实现 safegcd 算法需要使用 C 的 64 位整数对矩阵乘法和其他计算进行编程。
• 此外，还添加了许多其他优化以使实现速度更快。优化细节见：The safegcd implementation in libsecp256k1 explained。
• 最后，libsecp256k1 中有四种单独的 safegcd 算法实现：
  • 两种用于签名生成的恒定时间算法：一种针对 32 位系统进行了优化，一种针对 64 位系统进行了优化。
  • 以及两种用于签名验证的可变时间算法：同样一种用于 32 位系统，一种用于 64 位系统。

3. Verifiable C

为了验证 C 代码是否正确实现了 safegcd 算法，必须检查所有实现细节。Blockstream使用可Verifiable C（验证软件工具链的一部分）来使用 Coq 定理证明器对 C 代码进行推理。

验证通过为每个正在验证的函数使用Separation logic分离逻辑指定先决条件和后置条件来进行。分离逻辑是一种专门用于推理子程序、内存分配、并发性等的逻辑。

一旦为每个函数指定了规范，验证过程将从函数的先决条件开始，并在函数主体中的每个语句后建立新的不变量，直到最终在函数主体末尾或每个返回语句末尾建立后置条件。大部分形式化工作都花在代码行之间，使用不变量将每个 C 表达式的原始操作转换为有关被操作的数据结构在数学上代表什么的更高级语句。如，C 语言视为 64 位整数数组的内容实际上可能是 256 位整数的表示。

最终结果是经过 Coq 证明助手验证的formal proof正式证明，即 libsecp256k1 的 safegcd 模逆算法的 64 位可变时间实现在功能上是正确的，详细可参看：

• https://htmlpreview.github.io/?https://github.com/BlockstreamResearch/simplicity/blob/master/alectryon/verif_modinv64_impl.v.html

4. 验证的局限性

功能正确性证明存在一些限制。Verifiable C 中使用的分离逻辑实现了所谓的部分正确性。这意味着它仅证明 C 代码在返回时返回正确的结果，但不能证明终止本身。通过使用之前2021年的 Coq 对 safegcd 算法界限的证明来减轻这一限制，以证明主循环的循环计数器值实际上从未超过 11 次迭代。

另一个问题是 C 语言本身没有正式规范。相反，Verifiable C 项目使用CompCert 编译器项目来提供 C 语言的正式规范。这保证了当使用 CompCert 编译器编译经过验证的 C 程序时，生成的汇编代码将符合其规范。但是，这并不能保证 GCC、clang 或任何其他编译器生成的代码一定能正常工作。如，C 编译器允许对函数调用中的参数有不同的求值顺序。即使 C 语言有正式规范，任何未经正式验证的编译器仍然可能错误编译程序。这在实践中确实会发生——如，见2020年9月memcmp may be miscompiled by GCC #823。
最后，Verifiable C 不支持传递结构、返回结构或分配结构。虽然在 libsecp256k1 中，结构始终通过指针传递（这在Verifiable C 中是允许的），但在某些情况下会使用结构分配。对于模逆正确性证明，有 3 个分配必须由一个专门的函数调用替换，该函数调用逐个字段执行结构分配。

5. 小结

Blockstream Research 已正式验证了 libsecp256k1 模逆函数的正确性。这项工作进一步证明 C 代码验证在实践中是可行的。使用通用证明助手可以验证基于复杂数学参数构建的软件。

没有什么可以阻止 libsecp256k1 中实现的其余函数也得到验证。因此，libsecp256k1 可以获得最高的软件正确性保证。

参考资料

[1] Blockstream团队Russell O’Connor 和 Andrew Poelstra 2024年11月25日在比特币杂志上博客 Safegcd’s Implementation Formally Verified