用 TLA+ 追查 16 年 SQLite 漏洞：dqlite 会受影响吗？

提交与退订相关

提交成功！感谢您与我们联系，我们的团队成员将尽快与您取得联系。您已成功退订！感谢您订阅我们的时事通讯，在这些定期邮件中，您将了解到 Ubuntu 的最新动态以及即将举办的活动信息，届时还有机会与我们的团队成员面对面交流。您的偏好设置已成功更新。请重试，或者提交错误报告。

导航与博客相关

有 Canonical Ubuntu 相关导航，包括搜索、菜单、产品、用例、支持、社区、下载 Ubuntu 等。还有博客相关，有物联网、桌面端、云与服务器、网页与设计、人员与文化等分类。

用 TLA+ 追查 SQLite 漏洞

2026 年 6 月 25 日，阿尔贝托·卡雷罗发布文章，本文由 Canonical 的 dqlite 团队成员马尔科·马尼诺和阿尔贝托·卡雷罗撰写。文章聚焦用 TLA+ 追查一个存在 16 年的 SQLite 漏洞，探讨 dqlite 是否会受影响。

SQLite 漏洞剖析

最近，SQLite 发布新版本，修复了一个长期存在的漏洞，该漏洞与预写日志（Write Ahead Log，WAL）的检查点机制有关，可能导致数据库损坏。此漏洞关键在于其在代码库中存在时间长、发现和复现难度大，自 2010 年起已存在 16 年。对 dqlite 团队来说，关键问题是 dqlite 是否会受此漏洞影响。为找到答案，需了解导致数据库损坏的确切步骤序列，将用 TLA+ 对 SQLite 的行为进行建模，找出追踪信息，再创建新模型描述 dqlite 如何使用 SQLite 并检查漏洞是否会出现。

关于 SQLite 中 WAL 和检查点的简要介绍

SQLite 使用 WAL 模式，使读者不会被写入者阻塞，将数据写入名为预写日志（WAL）的特殊暂存区域，写入者可在 WAL 末尾追加数据，读者可忽略新数据直到数据稳定，最终暂存区域的数据会被移动到数据库中，此过程称为检查点。为防止 WAL 无限增长，写入者会尝试“重置”WAL。若想了解更多可查看官方文档。SQLite 使用锁和共享内存来协调对 WAL 的更改，关注写入和检查点操作，有检查点锁（`CKPT_LOCK`）和写入锁（`WRITE_LOCK`）。共享内存包含协调所需信息和用于索引 WAL 页面的数据结构，重要字段有 `walSalt`、`mxFrame`、`nBackfill`。

用 TLA+ 对漏洞进行建模

编写 TLA+ 规范难点在于决定建模内容，要创建简单且能反映现实情况并提取有用见解的规范。首先对数据库和 WAL 进行建模，将每个数据页面建模为唯一数字，WAL 表示为数字序列，数据库表示为数字集合，检查点操作会将页面从 WAL 序列移动到数据库集合中，用递增计数器生成唯一数字。需要对导致漏洞的追加和检查点两个操作进行建模，展示了 SQLite 中向 WAL 追加页面的 C 代码，并转换为 TLA+ 操作，关注 `WalAppendTakeLock` 和 `WalAppend`，还需新变量表示写入锁。接着关注检查点操作，展示了 SQLite 中负责检查点操作的代码，在 TLA+ 中需将函数拆分为不同操作，模拟从共享内存中读取数据的过程，因为共享内存可能会发生变化。