Finding bugs in Raft implementations

在 Raft 实现中寻找漏洞

Introduction

引言

The Raft consensus protocol is one of the foundations of the internet. Raft offers a formal specification in TLA+ and a concrete, detailed implementation guide, and hundreds of groups have created open-source implementations of the algorithm by following the instructions in the guide. It is, by far, the most widely used consensus algorithm in production systems. Raft 共识协议是互联网的基石之一。Raft 提供了基于 TLA+ 的形式化规范以及一份具体且详尽的实现指南，数百个团队通过遵循该指南中的说明，创建了该算法的开源实现。它是目前生产系统中应用最广泛的共识算法。

Despite the paper’s famously accessible style, we’ve found bugs in every Raft implementation we’ve tested, including HashiCorp Raft, Aeron Cluster, OpenRaft, and MicroRaft — despite the investment in formal methods, careful code review, unit testing, and years of testing in production. The bugs we found manifest as violations of Raft’s main invariant (called state machine safety in the paper, commonly referred to elsewhere as total order delivery). 尽管该论文以通俗易懂著称，但我们在测试过的每一个 Raft 实现中都发现了漏洞，包括 HashiCorp Raft、Aeron Cluster、OpenRaft 和 MicroRaft——尽管这些项目投入了形式化方法、严谨的代码审查、单元测试以及多年的生产环境测试。我们发现的漏洞表现为对 Raft 主要不变性（论文中称为“状态机安全”，在其他地方通常被称为“全序交付”）的破坏。

If you’re using a Raft implementation, you might want to check it for bugs. We’ve sent bug reports upstream. This isn’t intended as a critique of Raft, its authors, its implementers, or any particular implementation. Raft implementations, even with a formal specification and a detailed implementation guide, are not easy to write. Rather, this is a story about correctness in distributed systems — the inevitability of bugs, the inadequacy of any single approach, and the high cost of learned helplessness. 如果你正在使用 Raft 实现，你可能需要检查一下是否存在漏洞。我们已经向相关上游提交了漏洞报告。这并非旨在批评 Raft 本身、其作者、实现者或任何特定的实现。即使有形式化规范和详细的实现指南，Raft 的实现依然难以编写。相反，这是一个关于分布式系统正确性的故事——关于漏洞的不可避免性、单一方法的局限性，以及习得性无助所带来的高昂代价。

This is a long post. The first section is a position paper, but the rest is a detailed analysis of the issues we found, using one implementation as an example, a discussion of how we found them, and why we think they’re there. 这是一篇长文。第一部分是立场声明，其余部分则是对我们所发现问题的详细分析，以其中一个实现为例，探讨了我们是如何发现这些问题的，以及我们认为问题存在的原因。

Why this matters

为什么这很重要

If you’ve worked on distributed systems, you’ve been part of a war room at some point (if you haven’t, don’t worry, you will be), dealing with an outage like this one, or this one — both of which were caused by consensus failures. When a consensus issue results in an incident, it’s inevitably far reaching and extremely painful to root cause, replicate, and fix. 如果你从事过分布式系统工作，你一定曾在某个时刻参与过“作战室”（如果还没有，别担心，迟早会有的），处理过类似这样的或那样的宕机事件——这两者都是由共识失败引起的。当共识问题导致事故时，其影响往往极其深远，且在根因分析、复现和修复方面极其痛苦。

Many consensus issues remain “unsolved”, because they evade reproduction. It’s hard to know exactly what the real world consequences of these problems are, because consensus protocols sit so low in the stack. Are they corrupting the archive of someone’s personal D&D game? Security risks at a nuclear plant? Delaying trains in Germany? It all depends on where the protocol’s deployed. 许多共识问题至今仍未“解决”，因为它们难以复现。很难确切知道这些问题在现实世界中的后果，因为共识协议位于技术栈的底层。它们是在破坏某人个人 D&D 游戏的存档吗？还是在核电站造成安全风险？亦或是导致德国的火车延误？这完全取决于协议部署在哪里。

What’s certain is that these bugs are a colossal waste of developer time, and affect millions, if not hundreds of millions, of users. Yet we accept consensus issues and other deep distributed systems bugs as a fact of life — but once upon a time we accepted cholera, and waiting for your turn on the mainframe, as facts of life as well. Developers deserve something better. Everyone who depends on the software we write deserves something better. 可以肯定的是，这些漏洞是对开发者时间的巨大浪费，并影响了数百万甚至数亿用户。然而，我们却将共识问题和其他深层的分布式系统漏洞视为生活常态——但曾几何时，我们也曾将霍乱，以及在大型机前排队等待，视为生活常态。开发者值得更好的环境。每一个依赖我们所编写软件的人，都值得更好的保障。

Bugs are not a fact of life

漏洞并非生活常态

We have long accepted consensus bugs as inevitable because consensus protocols are just really, really hard to test properly. To really, thoroughly test a Raft implementation — or any distributed system — you effectively need to imagine every possible thing that could go wrong in your entire stack, and write a test to see if it will break your consensus protocol. It’s virtually impossible to write enough tests to provide this kind of assurance in critical systems. 长期以来，我们一直认为共识漏洞是不可避免的，因为共识协议确实非常、非常难以进行充分测试。要真正彻底地测试一个 Raft 实现（或任何分布式系统），你实际上需要设想整个技术栈中可能出错的每一个环节，并编写测试用例来验证它是否会破坏共识协议。在关键系统中，编写足够的测试来提供这种保证几乎是不可能的。

We get around this in two ways. First, we inflict the testing on our users, in the form of outages, downstream bugs, war rooms, and so on. It’s impossible for a team of developers to write enough tests, but with enough deployments and enough users across enough system configurations, you’re eventually going to find all the problems. Second, we rely on formal verification, and this is how consensus algorithms are built today. We define a model that we can mathematically prove to be correct, and then we… translate this perfect, platonic thing into code. 我们通过两种方式来规避这个问题。首先，我们将测试压力转嫁给用户，表现为宕机、下游漏洞、作战室等形式。开发团队不可能编写足够的测试，但通过足够多的部署、足够多的用户以及足够多样的系统配置，最终总能发现所有问题。其次，我们依赖形式化验证，这也是当今共识算法的构建方式。我们定义一个可以在数学上证明其正确的模型，然后……将这个完美的、柏拉图式的构想转化为代码。

Most Raft implementations are built this way. There are degrees here. The Raft protocol is one of very few consensus protocols that meets the strictest standard of “formal verification,” with a manual proof, a model check, and a mechanized proof-of-correctness. Every public consensus protocol we’re aware of has a manual proof/written correctness argument, but only Raft, Paxos, and MultiPaxos have mechanized proofs. 大多数 Raft 实现都是这样构建的。这其中存在程度差异。Raft 协议是极少数符合最严格“形式化验证”标准的共识协议之一，它拥有人工证明、模型检查和机械化的正确性证明。我们所知的每一个公开共识协议都有人工证明或书面的正确性论证，但只有 Raft、Paxos 和 MultiPaxos 拥有机械化证明。

Specifications are not code

规范不等于代码

Formal verification is a great starting point, in that it helps confirm that a core design is sound. Implementing a distributed consensus protocol without starting from a formal spec would result in many orders of magnitude more bugs than any Raft implementation has. Conversely, one might wonder what the FoundationDB team might have done if they’d started with a formal spec. But the issues here demonstrate the difficulties inherent in going from a formal specification to actual production code. 形式化验证是一个很好的起点，因为它有助于确认核心设计是稳健的。如果不从形式化规范开始实现分布式共识协议，产生的漏洞数量将比任何 Raft 实现多出几个数量级。反之，人们可能会好奇，如果 FoundationDB 团队从一开始就有形式化规范，他们会做得如何。但这里的问题证明了从形式化规范过渡到实际生产代码所固有的困难。

As long as the implementations are being done by unreliable, imperfect programmers (whether humans or LLMs), the actual code, and the systems using it, will only be as solid as the implementors’ assumptions — not the formally verified model. Furthermore, formal specifications are rarely truly complete — in the case of Raft, the TLA spec covers the core protocol, but doesn’t speak to details like installSnapshot, or replica replacement, or handling network packet corruption. 只要实现工作是由不可靠、不完美的程序员（无论是人类还是大模型）完成的，那么实际代码及其所使用的系统，其稳健程度就仅取决于实现者的假设，而非形式化验证的模型。此外，形式化规范很少是真正完整的——以 Raft 为例，TLA 规范涵盖了核心协议，但并未涉及诸如 installSnapshot、副本替换或处理网络数据包损坏等细节。

Testing can actually be simple

测试其实可以很简单

Surfacing these bugs didn’t require particularly deep knowledge of consensus or distributed systems. We found these using a simple approach, which a junior engineer could implement in less than a day, literally the simplest state-machine replication workload we could come up with. The key is that this is happening while the system is running in Antithesis, subject to the kind of faults that happen in a real world environment. We want to emphasize this point because all too often, we encounter a learned helplessness around… 发现这些漏洞并不需要对共识或分布式系统有特别深厚的知识。我们使用了一种简单的方法，初级工程师可以在不到一天的时间内实现，这实际上是我们能想到的最简单的状态机复制工作负载。关键在于，这是在系统运行于 Antithesis 环境中时发生的，并经受了现实世界中可能发生的各种故障。我们想强调这一点，因为我们太常遇到关于……的习得性无助。