使用Temporal Logic of Actions (TLA+)提升系统安全性

# 使用动作时序逻辑（TLA+）提升系统安全性 来源：https://depot.dev/blog/tla-verification 最难发现的分布式系统错误并不在任何单个操作中。两个进程各自执行正确操作，但顺序出人意料，导致数据丢失。测试无法捕捉这类错误，因为测试只运行你设想的交错顺序，而错误恰恰出现在你未曾想到的交错中。 在 Depot Registry 的规模下，这不再是假设。当请求量达到一定规模，百万分之一的交错会成为现实，并按你无法控制的节奏发生。因此，当我们在重建 Depot Registry（https://depot.dev/blog/now-available-depot-registry-v2）的垃圾回收器时，我们使用 TLA+ 进行了模型检查。模型检查器发现了一个测试和代码审查遗漏的真实错误。它还迫使我们精确处理一个乍听之下荒谬的设计决策：我们的注册表存储不可变的、内容寻址的 Blob（定义上永远不会改变），而且反正依赖于 S3 存储桶版本控制。 ## 什么是 TLA+？ **TLA+** 是一种将系统描述为状态和转换的语言。**TLC** 是一个模型检查器，它探索每个可达状态和每个可能的交错，然后告诉你你的不变性条件在所有这些情况下是否成立。你不是用 TLA+ 编写实现代码，而是编写一个足够小以便检查器能够完整探索的简化模型，但又足够接近真实情况，以便模型中的错误能指向你系统中的错误。 这是一个简单的模型：两个客户端从一个共享钱包中取款，各自在没有锁的情况下执行读取-然后-写入操作。 ``` ---------------- MODULE Wallet ---------------- EXTENDS Integers VARIABLES balance, read Init == balance = 10 /\ read = [c \in {"a", "b"} |-> -1] Check(c) == read[c] = -1 /\ read' = [read EXCEPT ![c] = balance] /\ UNCHANGED balance Withdraw(c) == read[c] >= 8 /\ balance' = balance - 8 /\ read' = [read EXCEPT ![c] = -2] Next == \E c \in {"a", "b"}: Check(c) \/ Withdraw(c) NoOverdraft == balance >= 0 ======================================== ``` 每个定义都是一个转换：`Check(c)` 读取余额，`Withdraw(c)` 在客户端看到足够资金时减去 8。`/\` 表示"并且"，`\/` 表示"或者"。带撇号的变量 `balance'` 表示下一状态的值，`NoOverdraft` 是我们希望在所有地方都成立的不变性条件。TLC 通过四个步骤打破了它：客户端 `a` 检查并看到 10，客户端 `b` 检查并看到 10，两者都取款，然后余额变为 -6。这就是经典的检查-然后-竞态条件，被机械地发现，并提供逐步的追踪以精确展示如何重现它。没有哪次测试运行是"不幸运"的；检查器只是尝试了每一种排序。 钱包只是一个简单的例子。以下是我们注册表 GC 模型中一个真实不变性条件的相同思路： ``` ManifestNeedsData == \A p \in PusherIDs: manifestExists[p] => s3Versions /= {} ``` 从左到右阅读： - `ManifestNeedsData` 是名称，`==` 表示"定义为"。 - `\A` 表示"对所有"。 - `p \in PusherIDs` 表示 `p` 遍历模型中的每个推送者。 - `manifestExists[p]` 询问推送者 `p` 是否有一个已提交的清单。 - `=>` 表示"如果左侧为真，则右侧必须为真"。 - `s3Versions /= {}` 表示 S3 版本集不为空。 综合起来，这个不变性条件大致相当于这段伪代码： ``` for each p in PusherIDs: if manifestExists[p]: assert s3Versions is not empty ``` 最后一个子句可能看起来太弱：它说*某个* S3 版本存在，而不是*正确的* Blob 存在。这是有意为之。此模型只有一个 Blob 摘要，因为我们关心的竞态是 GC 是否能在清单仍然需要它时删除该 Blob。在多摘要模型中，不变性条件将需要按摘要索引：`s3Versions[manifestDigest[p]] /= {}`。 审查模型意味着询问这类选择是否保留了你想要回答的问题。建模可移动部分（上传、数据库事务、GC 工作进程），声明必须始终为真的内容，然后让检查器对你的设计做生产流量最终会做的事情。 ## 为什么我们现在能负担得起 TLA+？ TLA+ 已经存在了几十年，但它有一个声誉问题：每个人都同意它很强大，但几乎没有人愿意投入数周时间在不断变化的实现旁边编写和维护一个忠实的模型。我们以前也是这种情况。今年之前，我们 GC 的规范每次都会在优先级之争中落败。变化在于我们不再手工编写模型。一个代理读取实现代码——Go 事务、SQL 和 S3 调用——并将其翻译成规范。我们审查其余部分：不变性条件是否表达了我们的意思？模型是否恰当地抽象了应该抽象的内容？ 编写 TLA+ 是昂贵的部分。决定什么是必须始终为真的部分一直很便宜，而且这是需要人类完成的部分。结果是注册表三层垃圾回收器的规范，它建模了并发的推送者、两个 GC 域、一个计数器协调器和注入的计数器漂移，所有这些都是交错的。它植根于真实的实现，事务对事务。TLC 在大约 21 分钟内探索了 14,290,224 个不同的状态，并证明了 10 个安全不变性条件和 2 个活性属性。最重要的不变性条件是第一个：一个已提交的清单永远不会丢失其 Blob 数据。 我们现在像其他人一样使用 AI 来更快地发布产品。但我们也用它来构建比我们以前有时间验证的更正确的系统。 ## 竞态：为什么我们不可变的 Blob 使用 S3 版本控制？ OCI 注册表是内容可寻址的。在 Depot Registry 中，Blob 位于 `blobs/sha256/`，摘要是内容的哈希值。上传同一个 Blob 两次，你会在相同的键上获得字节完全相同的数据。任何东西都不会就地更改。 在该模型下，S3 存储桶版本控制看起来毫无意义：对象的每个版本都会是相同的。但问题在于删除操作。垃圾回收必须删除不再被任何东西引用的 Blob。GC 工作进程标记一个引用计数为零的 Blob，等待宽限期，重新验证，然后删除。但引用存在于 MySQL 中，而字节存在于 S3 中，没有跨这两个系统的事务。这就打开了一个缺口： 1. GC 验证该 Blob 没有引用并决定删除它。 2. 并发地，一个客户端推送一个包含完全相同 Blob 的镜像。相同的摘要，相同的键。上传写入 S3 并提交了一个新的引用。 3. GC 的删除操作生效，移除了一个刚刚提交的清单现在指向的对象。 每个单独的步骤都是正确的。然而，这种交错删除了活跃的数据。而"一个客户端在 Blob 成为垃圾时重新推送它"并非罕见：当一个流行的基础镜像循环使用时就会发生这种情况。 你可以尝试用锁或更仔细的重新检查来修复这个问题，但你无法在一个原子步骤中重新检查 S3 并进行删除。因此，我们使删除操作本身变得精确。该存储桶已**启用版本控制**：重新上传相同的键会成为一个新版本，而不是覆盖。当 GC 标记一个 Blob 时，它会记录它看到的特定 S3 版本 ID。当它删除时，它只删除那个版本： 1. GC 标记 Blob 并捕获版本 `v1`。 2. 并发的推送将相同的字节写为版本 `v2` 并提交其引用。 3. GC 删除 `v1`，且只删除 `v1`。`v2`，即新清单所基于的版本，则未被触及。 我们使用版本控制并非为了保留历史记录。Blob 的每个版本在字节级别都是相同的，因此没有需要保留的历史。我们将其用作删除屏障：它将"删除此键"变为"删除我检查过的那些字节"，这使得删除操作在与写入操作竞态时是安全的。这就是本节标题中谜题的答案，对于任何进行垃圾回收的内容可寻址存储来说，都是一个好模式：版本控制，而非不可变内容，使删除变得安全。 ## 将疑虑转化为一行 TLA+ 注册表设计中的一个担忧是其引用计数器在故障下的行为。为了减少热门 Blob 上的争用，我们使用了一个轻量级的 saga：增加引用计数，执行工作，并在失败时用递减来补偿。协调器在崩溃阻止补偿完成时修复计数器。重要的细节是，错误的计数器不是对称的。计数过高会延迟 GC，而计数过低可能导致 GC 将被引用的 Blob 视为垃圾并删除活跃数据。这种不对称性就是我们的疑虑，所以我们告诉代理精确地验证这一点。它返回了一个不变性条件： ``` ManifestCountNeverUndercounts == blobActive => blobManifestCount >= TrueGlobalManifestCount ``` 每当 Blob 的行是活跃的时，*存储的*计数器必须至少等于从物理链接行推导出的*真实*计数。使用 `>=` 而不是 `=` 直接体现了这种不对称性：计数过高是可容忍的，计数过低则是违规。 为了使这个不变性条件告诉我们有用的信息，模型还必须包含不正确的计数器。我们添加了一个专门的漂移进程，按照与失败补偿和历史不同步相同的方向改变它们： ``` process DriftInjector = "drift" begin Drift: await driftBudget > 0; either await blobActive /\ blobLinkCount > 0; blobLinkCount := blobLinkCount - 1; \* undercount or await blobActive /\ blobLinkCount < N + DRIFT; blobLinkCount := blobLinkCount + 1; \* overcount end either; driftBudget := driftBudget - 1; goto Drift; end process; ``` 规范的这一部分是用 PlusCal 编写的，这是一种前端语法，可以编译成 TLA+，这就是为什么它读起来像伪代码。`await` 会阻塞步骤直到其条件成立，而 `either/or` 是非确定性选择：TLC 在这个进程可能运行的任何地方都会探索两个分支，与推送者、GC 工作进程和协调器交错。该进程不代表某个特定的错误，而是代表当另一个操作运行时，计数器可能在任一方向出错的更普遍情况。然后检查器可以验证破坏性步骤会重新计算物理行，而不是依赖一个过时的计数器。 模型也有为其自身内部簿记而设的不变性条件： ``` S3HeadOK == /\ (s3Versions = {}) <=> (s3Current = 0) /\ (s3Versions /= {}) => /\ s3Current \in s3Versions /\ s3Current = MaxVersion(s3Versions) ``` `S3HeadOK` 表示"当前版本"指针仅在版本集为空时才为空，否则指向最新版本。它不表达产品保证；它检查模型的 S3 抽象是否保持内部一致性。这些检查有助于区分被建模系统的故障与模型本身的错误。 测试和模型检查覆盖不同的领域。测试演练具体的实现，而模型探索那些难以刻意重现的交错。 ## 自己开始使用的提示和技巧 形式化验证过去是只有时间充裕的团队才能享受的奢侈。这个约束已经消失了。繁琐的部分——将实现忠实地翻译成规范——现在可以委托给代理，而你则做出判断决策。以下是我们希望六个月前就知道的事情。 **选择你的战场：** 不要将 TLA+ 抛向一切。好的候选者是竞争过程、棘手的事务边界、自主工作进程在时间上的竞态，或者跨越多个系统且没有共享事务的工作。例如，一个 CRUD 端点不需要模型检查器。 **行动导向：** 当你还在学习 TLA+ 时，目标不是正确性证明。那是以后的事，如果有的话。当人们听到"TLA+"时，第一个反对意见总是"但如果模型不匹配现实怎么办？"这不是重点：测试和形式化验证的存在都是为了增加信任，模型检查器是增加信任的另一个调节旋钮。所以不要等到你理解生成的规范中的每一行才运行它。运行它，看看会输出什么。最坏的情况是你损失了一个下午；最好的情况是你找到了一条可以深入挖掘的线索。如果错误的代价很高，那才是你投入真正时间在规范本身寻找缺陷的时候。 **借鉴这个工作流程：** 使用更便宜的模型生成交错过程的序列图，无论是在设计阶段还是从现有的实现中。审查它们，简化，并抽象掉无关紧要的步骤。我喜欢用 Codex 进行这种探索：它能很好地渲染图表，侧边聊天让你可以轻松地深入一个主题，而不会偏离主线。一旦图表表达了你的意思，将其交给一个前沿模型（在我们这里，是以额外高努力运行的 Fable）来生成 TLA+ 规范。第一个规范将是一个黑箱：你还不懂 TLA+，所以你只能判断输入和输出。这没关系。从那里开始。 **改进工作流程：** 现在让黑箱变得透明，一次处理一个部分。切入点是不变性条件，因为它们是可读的部分：关于什么必须始终为真的简短陈述。通常有 1-3 个明显的。让代理提出更多；然后无情地削减。经过几次迭代后，规范的其余部分也不再晦涩：你开始识别转换，然后质疑它们。我们重试的行为真的是这样吗？模型是否允许这里有两个工作进程？现在你是在白盒阅读规范，发现模型本身的问题，而不仅仅是信任它的输出。 **将疑虑转化为不变性条件：** 描述你*不确信*的是什么，因为那正是检查器可以为你购买的信心。对我们来说，是 GC 计数器中的一个不对称性——计数过高总是安全的，计数过低则永远不安全——而前一节（https://depot.dev/blog/tla-verification#turning-a-doubt-into-a-line-of-tla）解释了代理如何处理这个疑虑。你的疑虑是规范的最佳需求。 **将发现视为线索，而非裁决：** 模型可能不匹配现实，因此一个被违反的不变性条件是一个起点，一条可以继续深入挖掘的线索。拿走反例追踪，将其转化为序列图，并放大直到你完全理解竞态并修复它，或者发现模型与实现之间的不匹配。无论哪种结果都是进展：你从未知的未知变成了可以指出的东西。 你现在工具箱中有了另一个工具：测试检查你想到的交错；TLA+ 探索你没想到的交错。 ## 常见问题 **什么是 TLA+，TLC 模型检查器做什么？** TLA+ 是一种将系统描述为状态和转换的语言。TLC 是模型检查器，它探索每个可达状态和每个可能的交错，然后告诉你你的不变性条件在所有这些情况下是否成立。你不是用 TLA+ 编写实现代码，而是编写一个足够小以便检查器能够完整探索的简化模型，但又足够接近真实情况，以便模型中的错误能指向你系统中的错误。 **为什么一个具有不可变 Blob 的内容可寻址注册表需要 S3 存储桶版本控制？** 版本控制不是用来跟踪 Blob 的更改，因为字节永远不会就地更改。它是为了使删除变得安全。垃圾回收必须移除未被引用的 Blob，但引用存在于 MySQL 中，而字节存在于 S3 中，并且没有跨这两个系统的事务。这个缺口让客户端可以在 GC 决定删除它的同一时刻重新推送一个 Blob。版本控制将"删除此键"变为"删除我检查过的那个版本"，因此 GC 移除旧版本，而新推送的版本则不受影响。 **如果代理编写 TLA+ 规范，我如何相信模型匹配我的实现？** 你不应该完全相信，至少一开始不应该。模型检查器是另一个信任调节旋钮，而不是正确性证明。从不变性条件开始，因为它们是可读的部分，问问它们是否表达了你的意思。然后向外扩展，直到你能够白盒阅读转换并质疑它们：模型真的允许两个工作进程吗？模型真的允许这种重试行为吗？如果存在不匹配，你已经发现了问题，而不是在生产环境中发现它。