TLA+揪出SQLite WAL隐藏16年的漏洞

背景

SQLite 是一款广泛使用的嵌入式数据库，其 Write Ahead Log（WAL）模式允许多个读取器与写入器并发工作，而写入器不会阻塞读取器。然而，近期 SQLite 发布了一个新版本，修复了一个在 WAL checkpoint 机制中存在了长达 16 年的 bug（自 2010 年起），该 bug 可能导致数据库损坏。问题的实际影响虽然很低，但它长年隐藏在代码库中、极难发现和复现的特性引起了开发者社区的关注。对于 Canonical 旗下维护分布式 SQLite 扩展库 dqlite 的团队来说，一个关键问题是：dqlite 是否也会受此 bug 影响？

为了回答这个问题，团队使用 TLA+（一种形式化建模语言）对 SQLite 的行为进行建模，以精确复现导致数据库损坏的执行序列，然后针对 dqlite 使用 SQLite 的方式进行建模，检查该 bug 是否会在 dqlite 中发生。

核心内容

1. SQLite WAL 与 checkpoint 机制简介

SQLite 的 WAL 模式通过写入一个称为 Write Ahead Log（WAL）的暂存区域来实现读写并发。写入器可以向 WAL 末尾追加数据，读取器在数据被稳定前可以忽略新写入。最终，暂存区的内容会被移入主数据库，这个过程称为 checkpoint。为了防止 WAL 无限增长，如果前一次 checkpoint 成功将所有页面移入数据库，写入器会尝试“重置”WAL（即覆盖从头开始写入）。

SQLite 使用锁和共享内存来协调 WAL 的变化。对于本文关注的写入和 checkpoint 操作，只需关注两类锁：

• checkpoint 锁（CKPT_LOCK）：在运行 checkpoint 前获取，防止多个 checkpoint 同时进行。
• 写入锁（WRITE_LOCK）：在向 WAL 追加新页面前获取。

共享内存中存储了协调写入器、checkpointer 和读取器所需的信息，以及用于加速读取性能的 WAL 页面索引数据结构。其中与 bug 相关的字段包括：

• walSalt：每次 WAL 重置时递增的计数器。
• mxFrame：WAL 中当前帧（页面）的总数。
• nBackfill：已经完成 checkpoint 的页面数量，即区间 [nBackfill+1, mxFrame] 中的页面尚未被复制到数据库。

2. 使用 TLA+ 建模 bug

TLA+ 建模的难点在于决定哪些细节需要纳入模型，哪些可以省略。作者的目标是构建尽可能简单但足够忠实于现实、且能从中提取有用见解的规约（spec）。

首先，建模数据库和 WAL 文件：

\* files.
VARIABLE wal
VARIABLE db

\* wal-index variables:
VARIABLE nBackfill
VARIABLE mxFrame

\* We will only capture the sequential part of the salt.
VARIABLE walSalt

Init ≜
  \* wal and db are initially empty.
  ∧ wal = ⟨⟩
  ∧ db = {}
  ∧ nBackfill = 0
  ∧ mxFrame = 0
  ∧ walSalt = 0

由于生成实际数据不在模型范围内，作者采用简化方法：将每个页面建模为一个唯一数字，WAL 是这些数字的序列，数据库是这些数字的集合。Checkpoint 会将 WAL 中按追加顺序的页面移入数据库集合。唯一数字通过一个始终递增的计数器生成。

接下来需要建模两个相互作用并最终导致 bug 的动作：追加页面（Appending） 和 checkpoint。

追加页面的 C 代码逻辑

SQLite 中负责向 WAL 追加帧的函数是 walFrames，其关键逻辑如下：

• 首先检查是否可以将这些帧写入日志文件的开头（即重置 WAL），而不是追加到末尾。
• 如果是第一次写入帧，则需要先写入 WAL 文件头（包含魔数、版本、页面大小、salt 等）。
• 然后计算将要写入的帧序号 iFrame（即当前 mxFrame + 1），并计算写入偏移 iOffset。
• 遍历脏页链表，将每个帧写入 WAL 文件。如果之前已经写入过同一页面，则可以覆盖已有帧并重新计算校验和。

文中未完整展示所有代码，但点出了关键点：重置 WAL 的操作（walRestartLog）如果与 checkpoint 操作交错执行，可能导致共享内存中的状态不一致，从而触发 bug。

bug 的本质

该 bug 存在于 checkpoint 和写入操作之间的竞态条件中。具体而言，当一个写入器在 checkpoint 之后重置 WAL（即覆盖从头开始写入新的帧）时，如果 checkpoint 器读取共享内存中的 mxFrame 和 nBackfill 等字段的时机不当，可能会误以为某些页面尚未 checkpoint，从而错误地将其复制到数据库，导致写入了错误的数据（或旧数据覆盖新数据），最终造成数据库损坏。

3. 检查 dqlite 是否受影响

dqlite 是 Canonical 开发的分布式 SQLite 扩展，它通过 raft 共识协议在多个节点间复制 SQLite 数据库。dqlite 在内部使用 SQLite 的 WAL 模式，并在此基础上实现了自己的日志管理机制（比如使用自己的 checkpoint 策略）。因此，dqlite 团队需要验证上述 SQLite 的 WAL checkpoint bug 是否可能在 dqlite 的典型使用模式下被触发。

作者的方法是为 dqlite 使用 SQLite 的方式建立另一个 TLA+ 模型，该模型描述了 dqlite 如何调用 SQLite 的写入和 checkpoint 接口。然后通过模型检测（model checking）来寻找与原始 bug 类似的竞态条件序列。如果模型检测能够找到一个违反一致性条件的轨迹，则说明 dqlite 也可能受影响。

（注：原文在此处未给出最终结论，但指明了后续工作方向。实际文章中可能包含具体检测结果，但由于输入截断，我们依据已有信息进行呈现。）

关键要点

• bug 历史：SQLite WAL 模式下的 checkpoint bug 自 2010 年起存在，长达 16 年，直到最近才被发现并修复。
• 触发条件：该 bug 源于写入器在 checkpoint 后重置 WAL 时，与 checkpoint 器读取共享内存状态之间的竞态条件，可能导致错误的数据复制到数据库。
• 低实际影响：虽然理论上会导致数据库损坏，但在实际场景中触发概率极低，因此长期未被发现。
• 难以复现：bug 的触发需要精确的时序交错，传统测试方法（如压力测试、随机测试）很难稳定复现。
• TLA+ 建模的价值：通过形式化建模，团队能够快速精确地描述系统行为，并自动搜索到导致错误的执行轨迹，从而透彻理解 bug 的根源。
• dqlite 的关注点：dqlite 团队需要确认其分布式环境下使用 SQLite 的方式是否也会触及相同的竞态条件，从而评估该 bug 对 dqlite 用户的潜在风险。
• 方法可复制：这种用 TLA+ 分析第三方库中隐蔽 bug 并评估自身项目受影响程度的方法，对其他依赖 SQLite 或类似库的项目具有参考意义。

意义与影响

• 对 SQLite 生态：修复此 bug 提升了 SQLite WAL 模式的可靠性，尤其是对使用 checkpoint 功能的用户（如高并发写入场景）。同时，它展示了即使是经过严格测试的流行库，也可能隐藏着长寿命的竞态条件 bug。
• 对形式化验证领域：该案例是 TLA+ 在真实软件工程中成功应用的又一范例。它证明了即使不建模所有细节，简化的模型也能捕获复杂的并发错误，从而帮助开发者快速定位和复现问题。
• 对 dqlite 及类似项目：通过检查 dqlite 是否受影响，团队可以决定是否需要立即升级 SQLite 依赖或采取额外防护措施。这也提示其他基于 SQLite 构建的分布式系统应审查自己的 checkpoint 策略是否与 SQLite 的最新修复兼容。
• 业界启示：长期存在的 bug 提醒我们，代码审查和常规测试无法覆盖所有并发路径。将形式化方法引入关键组件的分析流程，可以作为一种有效的补充手段，降低