一切皆是信任决策

# 一切都是一场信任抉择 来源：https://nrd.sh/blog/everything-is-a-trust-decision.html ## 远不止打包那么简单¶ (https://nrd.sh/blog/everything-is-a-trust-devision.html#far-more-general-than-packaging) 上次我论证了 Nix 在一切方面都是对的，除了存储（store）。最后我顺带提了一句：系统能够*验证*什么与系统只能*担保*什么之间的界限，应该是元数据里的一个字段，而不是一种感觉。[1] 我说得太轻了。它不是一个字段。它是一个定理，而且并非关于打包。它关乎任何需要保存记录并希望从中得到的答案保持真实的东西：一个软件包索引、一个透明日志、一连串关键事件、已发表的科学文献。本文讲的就是这种形态，以及它对任何基于记录构建系统的人提出了什么要求。你其实整天都在做信任抉择。这种形态要求你将它们明确化。 在论证之前，先说几个事实，因为论证依赖于这些。这是我的首个科学贡献。我和共同作者 Zach Collier 用两种形式提出了一个问题。每个人都知道信任有边界；Thompson 四十年前就划了一条。但没人能证明这些边界是穷尽的——超过某条线之后，就没有任何东西可以验证，而剩下的每种信任都已被命名。那么：是否存在一个可证明的验证上限，超过上限的部分是否被完全解释清楚了？答案在一篇名为《Factoring Trust: A Machine-Checked Calculus of Where Verification Must End》的论文中，该论文正在 CSF 2027（IEEE 计算机安全基础研讨会）进行双盲评审，因此论文及其背后的 Lean 4 开发在评审结果出来前将保持私密。大部分形式化工作是我自己在 AI 辅助下完成的，并遵循我最后描述的一种规范。这对阅读本文有一点影响：每当我提到机器检查了某事，目前这代表我个人的承诺，由具名者负责，评审结束后它将成为你可自行运行的验证。我在此将其评级为“担保”，因为它本质上就是担保。 为何在评审前发布？因为我判断这个发现太重要了，不能让它束之高阁一年。而且本周发生的事也支持了我的观点。一个实验室宣布解决了一个千禧年大奖难题，两位率先发帖的研究者公开质疑他们的工作成果如何被使用，争论现在聚焦在谁有权描述事件经过。[2] 我不知道谁是对的。我知道，一份标明日期、公开说明你发现了什么及其可信度的声明，是最廉价的保险，而这恰好是本文所讨论的规范。 ## Thompson 开启的问题¶ (https://nrd.sh/blog/everything-is-a-trust-decision.html#the-question-thompson-opened) 这是一个古老的问题。苏格拉底被称为雅典最智慧的人，他自己的解释是，唯独他知道他所知有尽。他无法说出尽头在哪里，只能表明每个他考察的人都站在尽头之外而不自知。[3] 二十四个世纪后，Ken Thompson 将这个尽头置于机器内部：你无法信任你自己并未完全创建的代码，再怎么审查源代码也无济于事。[4] 他以一个道德论断而非一幅地图作为结尾。验证必须在某处终止。他没有说在哪里，也没有说尽头之外是什么样子。 四十年来，说出答案所需的不同部分散落在各个领域。分布式系统理论证明了机器群体能够达成哪些知识状态。[5] 密码学精确证明了协议能容忍哪些腐败参与者组合。[6] 安全工程在可信计算基周围画出了边界，并用 Lampson 的话说，承认其内部的东西“不容易搞清楚”。[7] 有人认为这个限制是社会性的，根本不能成为定理。[8] 而构建防篡改日志的人们，只是逐一列举他们系统的可信方，却从未追问这个列表是否完整，或者为什么是这些方而不是其他。[9] 据我们所知，没有人问过：对于一个不断增长的记录，一个有限检查器能够解决的声明是否存在一个精确的边界，使得边界之外的东西恰恰是你必须信任的，以及这个边界本身是定理还是策略。如果你知道哪个来源以这种方式提出过问题，请告诉我。这个主张附带日期。 我将宣称，这个问题现在已经终结。不是信任（那是庞大的、主要是人类的），而是这个问题。在本文结束时，你将看到在记录上验证止于何处，那之外剩下什么，它分为三种已命名的类型，以及每种的代价。 从你已有的做法开始。一个锁文件固定了你*依赖什么*，而非*谁为其背书*。一个签名提交是某人的话。你信任存储中的 CA 根是你曾经决定相信、然后就不再思考的东西。你的依赖所拉入的、你从未打开过的传递性依赖，则根本不是任何人的话。 那是四种不同的立场。拿取你运行的任何制品及其下的所有传递性依赖：它的源代码、它的依赖、依赖的依赖、编译器、密钥。将每一个称为一个部分。每个部分恰好属于这四者之一。有些你已**关闭**：一个可重复运行的检查通过了，这基于某人对该事物是其所声称样子的担保。其余的是*开放表面*，它分为三路。其中一些你被**给予**并选择原样接受：种子，即你运行的编译器、哈希函数、根密钥。一些是由你承认但尚未检查的主体**担保**的。还有一些是**匿名**的：无人担保，无人检查。 这是第一个等式，它属于论文的两个演算中的第二个——关于构建之物的那个： Σ = G ⊎ V ⊎ A 制品的开放表面Σ（验证未能关闭的其下一切）是你被给予的、被担保的和匿名的部分的不相交并。每个开放部分恰好属于一个且仅一个桶。这种划分是会计分类每个部分的方式，分类器没有第五种裁决；定理稍后出现，当桶开始移动时。 本文的主旨就在这个等式之下。信任不是验证的敌人。它是验证留下的东西，它可以被命名、计数和移动。第四个桶——你选择当作给定的东西——不是失败，而是一个决策。零信任不存在。具名的信任存在。 这个标题刻意呼应“一切皆文件”。这个口号之所以历经五十年，是因为它对架构而言是字面真理，你可以用它来约束 Unix。我在此追求同样的标准和同样的结果：一套你可以用来约束系统的规范。一切都是一场信任抉择，而证明就是你在其上签名的记录。所以，把每一个都写下来，签名，并放在可以被计数的地方。不是无信任，而是少一点信任，并精确说明剩下什么。 ## 一个声明如何才能持久¶ (https://nrd.sh/blog/everything-is-a-trust-decision.html#what-it-means-for-a-claim-to-last) 以上一切都是一个快照。真正的问题是当记录增长时会发生什么。你昨天验证了某事。一夜之间，日志新增了一万条。你会再次检查吗？ 三个词承载本节其余部分，取其通常含义： - **记录**是一条仅可追加的条目序列。永不强制推送的 Git 历史。一个透明日志。一个只增不删的软件包索引。 - **证书**是你用来检查而非重读记录的东西：一条 Merkle 路径、一个签名、一个证明。 - 一个声明是**持久的**，当无论追加什么，其证书都能持续工作。 柏拉图对那种被“为何为真”的解释所固定的观点有个词：它变得*monimos*，即持久。[10] 在论文中，一个固定声明得以持久的记录被称为*monimograph*（持久记录），这个词在结尾处当我们讨论一个并非如此的记录时会很重要。论文的第一个演算精确处理这种对象，其判断是需要记住的： R ⊢ +c ◃ π 在记录 R 上，声明 c 通过证书 π 成立，并且在 R 的每一个扩展上都持续成立。那个加号是关键。不是“现在为真”，而是“从此刻起为真”。使那个加号有效的规则是：如果记录从 R 扩展到 R′，且 c 在 R 处持久，那么 c 在 R′ 处成立：证书在 R 处创建，锚定在那里，你永远不需要一个新证书。机器检查这一点，目前以我的承诺为担保。 ## 哪些声明能持久¶ (https://nrd.sh/blog/everything-is-a-trust-decision.html#exactly-which-claims-can-last) 看看每个开发者都知道的声明：“这个提交是最新的。”它现在为真。它可以从记录中计算得出。下一次推送就会推翻它。没有任何类型的证书，在任何假设下，都无法让“最新”持久。这不是 Merkle 树或签名的局限。这是声明的本质：一张比赛进行中的记分牌照片，在你拍摄的那一刻为真，片刻之后就毫无意义。 核心猜想指出了哪些声明能够持久，这是一个双向蕴含： ∃ durable scheme for c ⟺ determined(c) ∧ certifiable(c) ∧ monotone(c) 确定性（Determined）意味着仅记录本身决定了答案；谁在问、谁写的并不重要。可证明（Certifiable）意味着一个具备你实际能力的检查器能够识别其证书。单调性（Monotone）意味着一旦为真，追加更多条目不能使其为假。一个声明拥有持久证书，当且仅当这三个条件都满足，机器从两个方向检查这一点：给定这三个条件，它会构建验证器。 为什么是三个而不是四个？因为图景中有三样东西：声明、检查器和记录的增长。每个条件对应其中一个可能失效的部分。没有第四个部分会失效。所以数量是定理，而不是某个权威喜欢的分类法。 “最新”不满足第三个条件。仅凭这一个事实，就使得生产环境中的每个透明日志都必须增长一个活性层：八卦传播、见证者、新鲜度检查。证书透明度（Certificate Transparency）项目最初提供了包含证明和一致性证明，然后发现还需要八卦协议。[11] 该领域是通过吃苦头发现的；演算则表明它必然如此。来自分布式系统的读者会从另一面认出第三个条件。CALM 定理指出单调性规范不需要协调，而我们的“观察者”正是这种协调，按声明购买。CALM 没有类似物的是检查器这一腿，而演算补充的是这三个条件是穷尽的。[12] 这三个条件对你的领域只字不提，而这正是设计杠杆。演算不知道条目意味着什么，签名是什么，或者构建做什么。它固定了认知过程，将这些选择全部留给你，这意味着它们需要由你正确处理。在构建之前，对你系统生死攸关的声明进行分类，因为这种分类会告诉你哪些声明可以只检查一次，哪些将必须永远检查，你之后构建的任何东西都无法将一个声明跨越那条线。 关于检查在何处停止，有一点诚实说明。“一个具备你实际能力的检查器”是一个参数，机器在两个设置上检查这个双向蕴含：无限能力，和仅可计算。多项式时间——大多数开发者关心的设置——在论文中是未来工作。我认为这不会削弱任何东西。在任何能力下，检查器要么存在要么不存在，因此三个条件的计数在每个设置下都是相同的定理；在多项式时间下变化的是下限，因为我们的证明将哈希视为绝对绑定，而多项式版本必须将其视为计算绑定，这使其成为密码学中的一个带有困难假设和安全参数的定理，且其可信计算基至今尚无可用的多项式时间定义。我预计在分区保持不变的情况下它会随之而来。 ## 无需阅读一切即可检查的内容¶ (https://nrd.sh/blog/everything-is-a-trust-decision.html#what-you-can-check-without-reading-everything) 为什么每个人都倾向于使用 Merkle 树？这是正确的直觉还是一种时尚？ 一个仅凭摘要就能检查的声明，其答案在两个记录片段上的组合，等于分别在每个片段上答案的组合： h(x ++ y) = h(x) ⊕ h(y) 假设除了绑定哈希外别无他物，这些声明以及只有这些声明，是一个有限检查器在任何规模下都能整体处理的。亚里士多德有一个词描述小到能一目了然的城市，叫“eusynoptic”（易视察的），而一个记录恰好对这类形状的声明是“易视察”的。[13] 机器检查表明，演算的持久项恰恰是这些函数，即 Bird 列表理论中的列表同态。[14] 简洁证明系统超出了这个类别，并以困难假设为代价；在类别内，限制是免费的。 这就是树的来源。因为 ⊕ 结合式地组合，你可以任意方式括起这个折叠。平衡的括法就是一棵树。一个条目的证书就是它向下的一个路径。这就是 Merkle 树，其对数证明正是代数所产生的形状。树是结合性的可视化，它是一个正确的直觉。它也很容易说得过多，所以这里精确说明什么是真实的：在假设只有绑定哈希的构造中，树对于证书*长度*是最优的，这是一个下界，属于 Tamassia 和 Triandopoulos，[15] 而常数大小的替代方案存在，如累加器和向量承诺，它们用困难假设换取了常数大小。[16] 然而，单条目是简单的情况，不是这个类别重要的原因。此类别中的声明是一个对它触及的每个条目的折叠，而同态使检查器能够从摘要中、以有限的工作量获取整个折叠，无论有多少条目。一个声明可以在其涉及的条目之后陈述，也可以随着记录增长而扩展，只要构建它的每一部分都能持久，整个声明就持久，你可以在任何时候验证它。当一部分不能持久时，演算会指出是哪一部分，而这正是你检查停止的地方。 这是设计杠杆的实践。演算提供给你一个四部分接口：你从每个条目读出什么、两个读数如何组合、你对总和做什么、以及你在记录的哪个范围上操作。提供这些，它就告诉你你的声明落在哪个单元格，以及它是否可以拥有一个持久证书。以“这个闭包中没有任何包被撤回”为例。将每个条目读作“这是否是撤回了我的某个包”，用或（OR）组合，最终取反，范围设为整个迄今为止的记录。确定的、可从摘要检查、但非单调：下一个条目可能就是那个撤回。这个声明是一通电话。改变一个参数，范围，设为“截至条目 1,204”，它就变成了一张你可以签发的回执。