Provably bug-free BIPs and implementations using hac-spec
演讲者: Jonas Nick
日期: October 14, 2022
记录者: Bryan Bishop
译者: Ajian
标签: Cryptography
类别: Core dev tech
引言
我是 Jonas，我的演讲主题是 “可证明无硬伤（bug-free）的 BIP 及其实现”。我还没有写出这样的 BIP，更不用说这样的实现了，但如果你的时间偏好足够低，在未来的某一天，这样的 BIP 会出现的。我的演讲只有 15 分钟，有任何问题都请举手。
先补充一个背景。规范（specifications）就应该没有 bug，我们希望它易于实现、不容易被误解。这使得规范的编写成了一件缓慢而且吃力不讨好的事。
本演讲将介绍一个提升整个流程、使之更少出错的小步骤。
比特币升级提议 2 号
可能这里的许多人都熟悉 BIP2。BIP 应该长什么样？BIP 的流程应该怎么走？这都是在 BIP2 里面规范的，比如 “BIP 应该用 mediawiki 格式编写”。我猜，它也有自己的优点和缺点吧？但也还好。
结果，大部分的 BIP 都是用 mediawiki 格式编写的，但也有一些补充性的材料，比如图表，就不是 mediawiki 格式的。总体上使用 mediawiki 格式。MuSig BIP 是一套签名规范 —— 我们先不管它说了什么 —— 但可读性是可疑的，不太好。只能说也不太糟。 它包含一些伪代码，是我们编写的。我们只是编写了某种形式的伪代码，也许人们可以读懂。比如你看这里，sec_nonce 是斜体的，这意味着它是一个数字或者说变量，但这很难看出来。“出错应该尽可能明显（fail if that fails）” 是一个极为重要的原则，但在规范中很难做到。
另一个问题是正确性。这些伪代码显然无法在机器上执行，这意味着你没法为它们编写测试。即使 4 双、 6 双眼睛帮你看过了，也很难保证绝无错误，总可能有什么东西是大家都没注意到的。即使是 taproot BIP，也有各种各样的错误，比如位（bits）到整数（integers）的转换，等等。
难事一桩。我们必须花更多时间来改善这种情况，而这会让整个流程变得更慢。
参考代码
在 MuSig2 BIP 中，我们不止有伪代码，还有参考代码，是用 python 写的。Python 代码至少比伪代码好读，对实现者来说。事实上，它也是可以执行、可以测试的，我们设计了随机测试，还有测试界面，我们甚至使用了奇怪的 python 类型检查器（type-checker），来帮助发现 bug。看起来还好。
论文
同一种东西还有第三种表示，就是 MuSig2 论文。它好不好读我就不知道了，论文用的是数学符号，不是计算机可以立即处理的东西。
Schnorr BIP
在 Schnorr BIP 中，我们也附上了论文，我们编写了一套规范，然后编写了参考实现，还有其他人看过规范和参考代码之后的实现。那么问题来了，论文中有安全性证明，但别的东西都没有安全性证明。这意味着，如果你把论文翻译成了规范，规范可能依然存在错误。同样地，当你把参考代码翻译成实现时，也可能犯错；实现者总有可能误解规范和参考代码。可能出错的地方有很多。
减半聚合 BIP
最近我们提出了一份关于 “减半聚合（half-aggregation）” 的 BIP。这里，我们只做了一件非常简单的事，就是合并了规范和参考代码，这样出错的地方会更少。
什么是减半聚合？就是一种聚合多个 BIP340 Schnorr 签名的非交互式流程。你也可以叫它 “压缩”，因为它以许多签名为输入，然后产生一个体积更小的签名。它由两个算法组成。第一种叫做 “聚合”，就是获得一系列的公钥、消息和签名，然后产生一个聚合结果。这个结果要么是一个聚合签名，要么表示错误。第二种算法是 “验证聚合”，以聚合签名、许多公钥和消息为输入，产生一个验证结果。
它使用了什么语言呢？不是 rust，是 hac-spec，只不过它依然被命名为 “halfagg.rs”，实际上也是 rust，我们后面会详细说。这就是我们的规范，它不是伪代码，所以我们可以运行测试。
Rust 更好
我认为，在这个场景中，rust 是比 python 更好的语言。你有一个合适的类型系统，而且可以获得编译器的帮助，可以更好地处理错误。还有 cargo 包管理器，以及围绕它的整个生态系统。
对于不熟悉 rust 的朋友来说，rust 会比 python 难懂一些，而且有一些你刚一接触会觉得很难理解的东西，比如问题标记操作码（question mark operator）。对于从未读过 rust 代码的人来说，它似乎令人困惑，因为它看起来微不足道，但实际上并非如此。
减半聚合的规范不是用 rust 写的，是用 hac-spec 写的。
Hac-spec
Hac-spec 可以为嵌入 rust 的高可信度密码学生成简洁、可执行、可验证的规范。Hac-spec 的语法是 rust 的语法的一个子集，这意味着你可以使用 rust 编译器生成程序并复用 rust 生态中的工具。
这里的 “可验证” 是什么意思呢？意思是 hac-spec 有形式化的语义（formal semantics）（“可以精确定义每个操作码的动作”）。
换句话来说，伪代码是由你的直觉来定义的，python 代码是由 python 解释器来定义的。Python 没有形式化的语义。一段 python 代码到到底是什么意思，是由解释它的 python 解释器决定的。但是，hac-spec 有结构化的操作性语义。每个操作码都有精确定义的功能。这些符号到底是什么意思并不重要，我们不要深究了，你不需要知道它们是什么意思。
说得清楚一些，rust 代码也是由 rust 编译器定义的。从这个角度看，它跟 python 没有什么区别。但是，hac-spec 有形式化的语义，但 rust 没有。这是重要的区别。它意味着如果你运行测试，你使用 rust 编译器得到的程序，可能跟 hac-spec 对这段程序的描述不同。我不知道这在实践中是否重要，可能会有影响吧。
为什么要使用形式化的语义？
这意味着，由此得到的规范是完全清楚明确的。并且它还允许我们分析它。为了分析伪代码，我们必须分析我们对这段伪代码的直觉，而这种直觉完全是人人不同的。可以分析，就意味着，我们可以使用证明助手以及理论上的证明器，来证明代码的特性。这些是允许我们证明东西的证明工具。
它们可以帮助我们证明这份规范没有数组越界访问（array out-of-bound access）问题以及整数溢出问题。这在减半聚合算法中是很有帮助的，因为你可能会得到无限数量的公钥来验证签名，但你的计算机有一个定长（fixed-width）的 int（整数） 类型，那么它什么时候会溢出呢？你能一次性验证多少个公钥？
另一方面，你可以证明这个规范在密码学证据上是否完整。这里，完整性意味着对有效的 BIP340 签名应用聚合算法将总是能产生一个有效的减半聚合签名。这可以帮助减少 bug 。
我们可以证明的另一个东西是，给定一个规范，一份实现是正确的：这份实现的所有行为都完全匹配该规范的状态。这个领域就叫 “形式化验证”。
状态
理想的情况下：这篇论文有一个安全性证据，这份规范有一个 “无硬伤证据” 和完整性证据，而且这个实现有一个正确性证据。这一般来说需要用专门的语言来编写实现。但其中一些跳跃之间可能依然有错误。
遥远的未来
在遥远的未来，我们可以抛弃这种奇怪的论文记号方案，直接为规范生成安全性证据。也许它会比我的幻灯片里提到的别的事情都要难得多，但这将消除大量的 bug 。
问：但这个安全性证据本身是写在论文里面的？
答：安全性证据需要用 hac-spec 来编写。而且你需要模拟器（simulators）。这个编译器将证明，根据你的定义，你的证据是正确的。C 代码已经有了 Coq 。你定义一种证据，用 Haskell 编写证据，然后验证 C 代码与之匹配。Coq 实际上是用 Coq 编写 的。这是一种证明语言。
问：这很酷。
答：实际上是很难做到的。同时，问题在于，安全性证据，只是一个术语。但一个安全性证据可能只涵盖了一些东西，而没有涵盖另一些东西。所以，问题在于安全性的定义。但这也是形式化验证领域人们尝试推进了 20 年的东西：撇除论文，用 Coq 编写所有的证据。我认同，但这是很难做到的。
从我对这个研讨会的印象来看，我觉得令人难以忘怀。许多事情正在发生。这个生态系统有许多的工具，和糟糕的说明书，但 hac-spec 是一个例外。你只需要用 hac-spec 编写你的规范，然后你就可以将规范翻译成其它语言，并允许你证明这份规范的一些东西。或者你也可以翻译成 Coq。
你可以选择自己要证明什么。你可以随你的心意逐步优化证据。在 Coq 的案例中，大量的变量来自代码生成器，但也许你改变了规范，就会得到新的变量名称，然后你必须为新的 Coq 输出调整你的证据，令人难过。你可以写一个这样的引理（lemma）：没有整数溢出，也没有缓冲区溢出，然后从中再生成一个证据。这需要非常专业化的技巧，以及大量的工作。我应该指出这一点。
问：hac-spec 里面有证明语言吗？
答：hac-spec 只是一种用于编写规范的形式化定义。但它并不包含证据编译器或者验证器。所以你必须使用 Coq 或者别的东西。没错。你只有形式化的语义。它是完全形式化的。切换成 Coq 的语义也是完全形式化的。hac-spec 的语义是完全形式化的。但翻译成 Coq 的话 …… 也许我们应该为 Coq 运行测试，看看它是否能工作。
在数字签名这个案例中，安全性证据证明的是什么？它是否证明了这种签名是无法伪造的？是否证明了它可以跟 taproot 的调整兼容？你在证明什么？如果你订阅了邮件组，这周我们才在 MuSig2 BIP 中发现了一个漏洞。它通常会发生在一个很模糊的场景中，作为一个签名者，你可能会被骗进这样的陷阱里面，但这是 MuSig2 BIP 中的一个漏洞。问题在于，我们的论文中的证据是正确的，而规范也在很大程度上是正确的；我们应该在规范中说明，不应该使用 taproot 调整，这样我们的规范才能是正确的。但我们没有。规范没有考虑到调整的影响。所以说，安全性证据，也要对精确的方案才有用。
为了证明一份规范的某一些属性，你需要把它翻译成另一种这方面的语言，比如 Coq、Fstar 和 easycrypt。
结论
你会给自己的测试界面运行 Coq 代码吗？这只是我的一个想法，确保 Coq 代码是正确的。
问：如果我想编写一份 BIP，并证明它是正确的，我需要用 hac-spec 来编写一份规范，然后用 Coq 来编写一个证据？
答：是的。你用 hac-sepc 来编写规范，不用 Coq，这样其他人也能阅读它。
问：应该也可以用 hac-spec 来编写证据吧？不行吗？
答：不是很管用。
问：我不是说使用同一种语言，只是觉得应该可以在同一个框架下完成，不需要迁移到别的框架。
答：嗯，这就是为什么人们要用 Coq 。因为它有一个很大的生态系统。
问：我一直在学习 Coq 。但感觉从来没学会。
答：这些东西都很难。但如果你把它们换成别的东西，会更难。
如果你是一个密码学方面的 BIP 的作者，你可能需要考虑用 hac-spec（而不是伪代码）来编写你的规范，这样你还可以完全抛开 python 代码什么的。在减半聚合 BIP 中，我为阅读 rust 有困难的朋友添加了注释。这种 hac-spec 的子集依然难以阅读，比如它也有问题标记操作码，这是我能找到的最好的例子了。别的语言都没有这种东西。你很容易忽略它们，但它们是极为重要的的。我自己也中招了。Hac-spec 强制你使用问题标记操作码，你不能只返回。你可能会忽略到问题标记。它们可能正式定义了问题标记。以前你只能返回错误，不能返回正确。
一个问题是，我们真的需要伪代码吗？它帮到了谁？它也引入了犯错的风险，比如将规范翻译成伪代码的实话，或者某人阅读了伪代码然后误解了它。而且理解起来还难受。我自己宁愿去掉伪代码，因为这样还少一点事。
在整数溢出检查中，你也需要编写 Coq 证据吗？是的。我在 hac-spec 中得到了形式化的定义，但也仅此而已 …… 如果 python 有一套形式化的定义，那也是一样的。天下没有免费的午餐。
也许还有一种办法可以实现形式化验证。这是一个已经成熟的领域，只是在圈子之外没有多少关注。也许比特币可以成为一个应用它的研究领域。我从没听过银行在大型机上使用它们。
那么，它在密码学 BIP 之外的地方有用吗？Hac-spec 只是 rust 的一个子集，你可以做许多事，标准库有一些受限，但可能有别的应用。
问：你可以用它打开 socket 吗？我觉得不行。
答：Fstar 是另一种交互式的理论证明器，类似于 Coq。你也可以将它翻译成 easy-crypt，它稍微有点区别，因为它是一种用于实现计算机密码学证明的专门语言。Hac-spec 不以代码生成为目标，它不是为了快速生成跟 spec 匹配的代码而设计的。但有了 hac-spec，你不需要是一个形式化理论专家，也能阅读规范。
也许证明工程在未来会变得更加简单。也许 GPT-3/Codex 会给你关于如何制作证明的建议，比如给你提示或者帮助你。Coq 也有 Copilot 。幸运的话，到那时候我们就可以邀请别人形式化分析我们的规范，因为我们无法自己做完所有的事。