https://nickler.ninja/

我是 Jonas，我的演讲主题是 “可证明无硬伤（bug-free）的 BIP 及其实现”。我还没有写出这样的 BIP，更不用说这样的实现了，但如果你的时间偏好足够低，在未来的某一天，这样的 BIP 会出现的。我的演讲只有 15 分钟，有任何问题都请举手。

先补充一个背景。规范（specifications）就应该没有 bug，我们希望它易于实现、不容易被误解。这使得规范的编写成了一件缓慢而且吃力不讨好的事。

本演讲将介绍一个提升整个流程、使之更少出错的小步骤。

可能这里的许多人都熟悉 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 中，我们也附上了论文，我们编写了一套规范，然后编写了参考实现，还有其他人看过规范和参考代码之后的实现。那么问题来了，论文中有安全性证明，但别的东西都没有安全性证明。这意味着，如果你把论文翻译成了规范，规范可能依然存在错误。同样地，当你把参考代码翻译成实现时，也可能犯错；实现者总有可能误解规范和参考代码。可能出错的地方有很多。

最近我们提出了一份关于 “减半聚合（half-aggregation）” 的 BIP。这里，我们只做了一件非常简单的事，就是合并了规范和参考代码，这样出错的地方会更少。

什么是减半聚合？就是一种聚合多个 BIP340 Schnorr 签名的非交互式流程。你也可以叫它 “压缩”，因为它以许多签名为输入，然后产生一个体积更小的签名。它由两个算法组成。第一种叫做 “聚合”，就是获得一系列的公钥、消息和签名，然后产生一个聚合结果。这个结果要么是一个聚合签名，要么表示错误。第二种算法是 “验证聚合”，以聚合签名、许多公钥和消息为输入，产生一个验证结果。

它使用了什么语言呢？不是 rust，是 hac-spec，只不过它依然被命名为 “halfagg.rs”，实际上也是 rust，我们后面会详细说。这就是我们的规范，它不是伪代码，所以我们可以运行测试。

我认为，在这个场景中，rust 是比 python 更好的语言。你有一个合适的类型系统，而且可以获得编译器的帮助，可以更好地处理错误。还有 cargo 包管理器，以及围绕它的整个生态系统。

对于不熟悉 rust 的朋友来说，rust 会比 python 难懂一些，而且有一些你刚一接触会觉得很难理解的东西，比如问题标记操作码（question mark operator）。对于从未读过 rust 代码的人来说，它似乎令人困惑，因为它看起来微不足道，但实际上并非如此。

减半聚合的规范不是用 rust 写的，是用 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 。幸运的话，到那时候我们就可以邀请别人形式化分析我们的规范，因为我们无法自己做完所有的事。