Safegcd 的实施得到正式验证

介绍

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

在 ”快速恒定时间 gcd 计算和模反演”，Daniel J. Bernstein 和 Bo-Yin Yang 开发了一种新的模反演算法。 2021 年，该算法被称为“safegcd” 实施的由 Peter Dettman 编写的 libsecp256k1。作为该新颖算法审查过程的一部分，Blockstream Research 是第一个完成形式验证通过使用 Coq 证明助手正式验证算法确实以 256 位输入上的正确模逆结果终止，从而了解算法的设计。

算法与实现之间的差距

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

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

可验证C

为了验证 C 代码正确实现了 safegcd 算法，必须检查所有实现细节。我们使用可验证C，是验证软件工具链的一部分，用于使用 Coq 定理证明器推理 C 代码。

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

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

最终结果是正式证明，经 Coq 证明助手验证，libsecp256k1 的 safegcd 模逆算法的 64 位可变时间实现在功能上是正确的。

验证的局限性

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

另一个问题是C语言本身没有正式的规范。相反，可验证的 C 项目使用 CompCert 编译器项目提供 C 语言的正式规范。这保证了当使用 CompCert 编译器编译经过验证的 C 程序时，生成的汇编代码将满足其规范（受上述限制）。然而，这并不能保证 GCC、clang 或任何其他编译器生成的代码一定能工作。例如，C 编译器允许对函数调用中的参数有不同的求值顺序。即使 C 语言有正式规范，任何本身未经正式验证的编译器仍然可能会错误编译程序。这确实发生在实践中。

最后，可验证 C 不支持传递结构、返回结构或分配结构。虽然在 libsecp256k1 中，结构始终通过指针传递（这在可验证 C 中是允许的），但也有少数情况会使用结构赋值。对于模块化逆向正确性证明，有 3 个赋值必须由专门的函数调用替换，该函数逐个字段执行结构赋值。