优惠论坛

标题: SAFEGCD的实现已正式验证（转） [打印本页]
作者: 22301    时间: 2024-11-26 10:45
标题: SAFEGCD的实现已正式验证（转）
比特币和其他区块链（如Liquid）的安全性取决于ECDSA和Schnorr签名等数字签名算法的使用。一个名为libsecp256k1的C库，以该库所操作的椭圆曲线命名，被比特币核心和Liquid使用，以提供这些数字签名算法。这些算法利用了一种称为模逆的数学计算，这是计算中相对昂贵的组成部分。
# F  x3 B/ F* H! K' P: {9 f  z* I1 pDaniel J.Bernstein和Bo-Yin Yang在“快速恒定时间gcd计算和模反演”中开发了一种新的模反演算法。2021年，Peter Dettman为libsecp256k1实现了这种被称为“safegcd”的算法。作为这种新算法审查过程的一部分，Blockstream Research是第一个通过使用Coq证明助手正式验证算法确实在256位输入上以正确的模逆结果终止，从而完成算法设计正式验证的公司。
$ Z7 b& a4 U" ]. t$ E4 H. i. c算法与实现之间的差距
% V5 ^2 G4 C* }" J# Q2021年的形式化工作只表明Bernstein和Yang设计的算法是正确的。然而，在libsecp256k1中使用该算法需要在C编程语言中实现safegcd算法的数学描述。例如，该算法的数学描述执行向量的矩阵乘法，向量的宽度可达256位有符号整数，但C编程语言本身只提供高达64位（或128位，某些语言扩展）的整数。
. T& g# @9 J+ l! L! S; z实现safegcd算法需要使用C的64位整数对矩阵乘法和其他计算进行编程。此外，还添加了许多其他优化，以使实现更快。最后，libsecp256k1中的safegcd算法有四种单独的实现：两种用于签名生成的恒定时间算法，一种针对32位系统进行了优化，另一种针对64位系统进行优化，还有两种用于验证签名的可变时间算法，同样适用于32位系统和64位系统。
/ m8 M# `7 N" v* Z" h. `" s可验证C% p; w6 b* k4 X4 X, _  \) |
为了验证C代码正确实现了safegcd算法，必须检查所有实现细节。我们使用Verifiable C，它是Verified Software Toolchain的一部分，用于使用Coq定理证明器对C代码进行推理。. k  ~3 ?3 L5 A' G8 s: A
验证通过为每个正在进行验证的函数使用分离逻辑指定先决条件和后置条件来进行。分离逻辑是一种专门用于推理子程序、内存分配、并发性等的逻辑。8 _5 F% A  l2 H, G) t+ H
一旦给每个函数一个规范，验证就从函数的前提条件开始，在函数体中的每个语句后建立一个新的不变量，直到最终在函数体末尾或每个返回语句末尾建立后置条件。大部分形式化工作都花在代码行之间，使用不变量将每个C表达式的原始操作转换为关于所操纵的数据结构在数学上表示什么的更高级语句。例如，C语言认为的64位整数数组实际上可能是256位整数的表示。
; V1 `+ U1 B' t2 g最终结果是一个形式化的证明，由Coq证明助手验证，libsecp256k1的safegcd模块化逆算法的64位可变时间实现在功能上是正确的。
1 h8 M- x( j8 F7 N验证的局限性
8 J4 w! v! S0 O函数正确性证明存在一些局限性。Verifiable C中使用的分离逻辑实现了所谓的部分正确性。这意味着它只证明C代码在返回时返回正确的结果，但它本身并不能证明终止。我们通过使用我们之前在safegcd算法上的Coq边界证明来证明主循环的循环计数器值实际上从未超过11次迭代，从而减轻了这一限制。) v0 V" S5 M( A) p8 l
另一个问题是C语言本身没有正式的规范。相反，Verifiable C项目使用CompCert编译器项目来提供C语言的正式规范。这保证了当使用CompCert编译器编译经过验证的C程序时，生成的汇编代码将符合其规范（受上述限制）。然而，这并不能保证GCC、clang或任何其他编译器生成的代码一定能工作。例如，允许C编译器在函数调用中对参数有不同的求值顺序。即使C语言有正式的规范，任何本身没有经过正式验证的编译器仍然可能对程序进行错误编译。这确实发生在实践中。
# }4 H3 X& ^3 a- V7 p6 E5 Z# V最后，Verifiable C不支持传递结构、返回结构或分配结构。虽然在libsecp256k1中，结构总是通过指针传递（在Verifiable C中是允许的），但也有少数情况下使用结构赋值。对于模块化逆正确性证明，有3个赋值必须被一个专门的函数调用替换，该函数调用逐个字段执行结构赋值。6 k8 K8 @. Q# T2 R% ?) J
摘要& c4 R1 Y5 q. X+ B" @5 Z, F( G2 u
Blockstream Research已经正式验证了libsecp256k1的模逆函数的正确性。这项工作进一步证明了C代码的验证在实践中是可能的。使用通用证明助手，我们可以验证基于复杂数学论证的软件。( i0 v$ ?# R6 F; @9 E
没有什么能阻止libsecp256k1中实现的其他函数也被验证。因此，libsecp256k1可以获得尽可能高的软件正确性保证。
; o+ }* r2 ^' s& H+ q* K4 ^" L7 O; \, I( v1 \- T
作者: 22301    时间: 2024-11-26 10:45
这个倒也是可以去了解下看看了啊。
作者: rainwang    时间: 2024-11-26 19:16
验证了啊，那就是设计者的目标达到了
作者: 赚钱小样    时间: 2024-11-27 09:49
这个得到了验证也是很好的了吧
作者: 舞出精彩    时间: 2024-11-27 11:47
这么看的话也是会有验证了
作者: 爱美的女人    时间: 2024-11-28 19:53
正式验证的是要怎么实现了
作者: 如梦的生活    时间: 2024-11-29 21:37
那看来这个软件还是比较不错的哟。
作者: 德罗星    时间: 2024-12-2 20:29
是正确且安全无比起来的啊.



欢迎光临 优惠论坛 (https://www.tcelue.ooo/) Powered by Discuz! X3.1