网站建设推广公众号制作推广青岛,深圳专业做网站建网站价格,js 转wordpress,wordpress在哪放商务通代码1. 引言
比特币和其他链#xff08;如 Liquid#xff09;的安全性取决于 ECDSA 和 Schnorr 签名等数字签名算法的使用。Bitcoin Core 和 Liquid 都使用名为 libsecp256k1 的 C 库来提供这些数字签名算法#xff0c;该库以其所运行的椭圆曲线命名。这些算法利用一种称为modu…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
