2026 年 6 月 25 日，Ubuntu 团队的一篇技术博客悄然上线。标题里藏着两个看似矛盾的事实：SQLite——这个地球上使用最广泛的数据库——被找到了一个漏洞；这个漏洞，从 2010 年就躺在代码里了。
换句话说，它藏了 16 年。
16 年是什么概念？2010 年，iPhone 4 刚发布，微信还没诞生，人们还在用按键手机发短信。而就在那一年，这个漏洞随着一行代码被写入 SQLite，从此安安静静地住进了每一台智能手机、每一个浏览器、每一个操作系统里。数亿设备，16 年的时间——从来没有人发现过它。
最终，找到它的不是人，是一道数学题。
图：Ubuntu 团队用 TLA+ 建模 SQLite WAL 的检查点行为。模型只需 20 步就能复现这个隐藏了 16 年的漏洞。来源：ubuntu.com
先搞清楚一件事：SQLite 是什么，为什么它在你手机里
笔者先解释一个前提：SQLite 不是一个”软件”——你手机上找不到一个叫”SQLite”的图标。它是一种”数据库引擎”，专门用来在手机、电脑、浏览器里存储和管理数据。
举个例子：你微信里的聊天记录，你手机通讯录里的联系人，你浏览器保存的密码，你用支付宝、淘宝、抖音时产生的各种本地数据——背后几乎都是 SQLite 在默默工作。它是世界上装机量最大的数据库，没有之一。据估计，全球有超过一万亿个 SQLite 数据库在运行。
而这样一个”地基”级别的软件，居然有一个漏洞在里头躺了 16 年。这件事本身就足以让人后背发凉。
但这个故事真正精彩的地方在于：这个 bug 是怎么被找到的。
一个注定不可能被人类发现的问题
先看漏洞本身。SQLite 有一种叫 WAL（写前日志，Write-Ahead Log）的工作模式，简单理解就是：当多个程序同时读写数据库时，WAL 充当一个”缓冲本”。写的人先写在缓冲本上，读的人暂时不受影响，等写完再一起搬到正式账本上。这个过程叫”检查点”（checkpoint）。
漏洞就出在”搬”这个动作和”写”这个动作同时发生的时候。用生活里的话说：
假设你和一个同事同时操作一份电子表格。同事正在往”草稿区”追加新数据，而你负责把草稿区里已经确认的内容搬到正式文件里。你扫了一眼草稿区，看到有 100 条记录需要搬，于是你搬了 50 条——此时同事又追加了 5 条新记录，并且”重置”了草稿区的计数。你继续搬剩下的 50 条，但因为计数被重置了，你实际上只搬了旧的序号，漏掉了一些真正应该搬走的数据。
结果就是：正式文件里少了几条记录。数据丢了。
这就是 SQLite 官方文档里描述的漏洞：WAL 检查点过程中的一个”竞态条件”——两个操作没有协调好先后顺序，在极其精确的时间窗口内撞在了一起。
关键在于”极其精确”这四个字。触发这个漏洞需要满足一连串苛刻的条件：写操作和检查点操作必须同时发生，必须在检查点读到 WAL 大小之后、开始搬运之前这短短的一瞬间里，另一个写操作刚好完成并重置了 WAL。这个时间窗口可能只有几微秒。
人类靠写测试用例来找 bug，本质上是”猜”——猜哪里可能出错，然后在那个地方反复尝试。但这个漏洞的触发窗口窄到了”猜都猜不到”的程度。不论你安排多少测试人员、写多少自动化测试脚本，你都不可能覆盖每一种操作顺序的组合——因为可能的组合数量是天文数字。
这就是为什么这个漏洞能在数亿设备里安安稳稳地躺了 16 年。
TLA+ 是什么：不是测试软件，是数学证明
要理解 Ubuntu 团队是怎么找到这个漏洞的，需要先理解一个概念：形式化验证。
笔者用最简单的比喻来说：传统测试像是”抽查”——你在一袋米里随机抓几把，看看有没有沙子。形式化验证像是”数学证明”——你可以用逻辑推导出”这袋米里到底有没有沙子”，不需要一把一把地翻。
TLA+ 就是一种形式化验证工具。它的全名叫 Temporal Logic of Actions，由计算机科学界的传奇人物 Leslie Lamport 发明——这位老先生也是 LaTeX（学术论文排版系统）的创造者，还设计了 Paxos 共识算法（今天几乎所有分布式系统的基础）。
TLA+ 做的事情说起来简单：你把你想要检查的软件行为抽象成一个数学模型——不需要写代码，只需要用数学语言描述”这个东西在不同情况下应该怎么变化”。然后，TLA+ 的模型检查器会穷举所有可能的状态组合，验证你定义的规则是否永远成立。
用 Ubuntu 团队的话说，他们用 TLA+ 建立了 SQLite WAL 的行为模型之后，模型检查器”只用 20 步就找到了反例”。20 步。16 年 vs. 20 步。
图：TLA+ 模型的静态版本，展示了写操作和检查点操作之间的竞态条件如何导致数据丢失。来源：ubuntu.com
为什么人类的肉眼测试永远赢不了这场仗
这里有一个深层的问题值得展开：为什么数学方法能找到一个 16 年都没人发现的漏洞？数学方法之所以能做到，根源在于方法论的本质区别。
人类的测试方法——不管是手动点来点去，还是写自动化脚本——本质上是”枚举式”的：你列出一些你觉得可能出问题的场景，然后在每个场景里验证。问题是，软件系统的状态空间是组合爆炸的。一个有 100 个操作步骤的系统，可能的状态顺序排列是 100 的阶乘——这个数字比宇宙中的原子数量还多。你不可能穷举。
而 TLA+ 这种形式化验证工具，虽然理论上也面临”状态爆炸”的问题，但它能做一件人类做不到的事：它检查的是：在我定义的所有情况下，会不会出现问题。
这句话值得品味两遍。
人类测试回答的问题是：“我看到了什么问题？” 形式化验证回答的问题是：“有没有可能出问题？”
前者是被动的、依赖想象力的、很容易漏掉东西的。后者是主动的、穷举的、不会漏掉任何一个计算出来的状态。
Ubuntu 的工程师并没有比 SQLite 的开发者更聪明——SQLite 的开发团队以极高的代码质量著称，测试套件覆盖率是业内顶尖的。但工具不同。尺子和显微镜看到的世界不是同一个维度。
竞争对手为什么没被影响：一个意外的发现
这个故事还有一个有趣的番外。Ubuntu 团队之所以会去做这个验证，是因为他们自己维护着一个叫 Dqlite 的项目——一个基于 SQLite 的分布式数据库。他们想知道：SQLite 的这个漏洞，会不会也存在于 Dqlite 里？
于是他们又建了一个 Dqlite 的 TLA+ 模型。结果发现：Dqlite 不受影响。
原因很简单：Dqlite 的设计比 SQLite 更”保守”。它在做检查点的时候会锁住整个写操作，确保”搬”和”写”不会同时发生。虽然这会牺牲一点性能，但恰好躲过了这个竞态条件。
Dqlite 的设计未必更好。但有时候你无意中做的一个保守选择，可能会在 16 年后突然被证明是正确的。软件工程的因果链条就是这么奇妙。
SQLite 的修复：一行代码的事
2026 年 3 月 5 日，SQLite 官方发布了漏洞修复。修复极其简单：在检查点过程中多加了一次检查，确认 WAL 没有被重置过。如果被重置了，就重新开始。
换句话说，16 年的隐患，一行代码就解决了。
但代码本身简单不意味着问题简单——找到这一行代码需要放在哪里、需要检查什么条件，这个过程太难了。难到 SQLite 的那些世界上最懂数据库的工程师们，16 年都没有发现。
这件事意味着什么：一个正在改变的趋势
笔者有两点想讲。
第一，SQLite 这个案例不是孤例。Amazon、Microsoft、Oracle 等公司早已在关键基础设施中使用 TLA+ 来做形式化验证——AWS 的 S3、DynamoDB 等核心服务在早期设计阶段就经过了 TLA+ 的模型检查。只是这些案例大多发生在企业内部的封闭系统里，普通人看不到。而 SQLite 作为一个无处不在的开源项目，它的漏洞被形式化验证找到，是一个具有公共可见性的标志性事件。
第二，形式化验证的”门槛”正在降低。TLA+ 不是给普通人用的——它需要数学思维和系统建模能力。但就像 20 年前没人觉得”自动化测试”是人人都该做的事、现在却是标配一样，形式化验证也正在从”大神专用”走向”团队标配”。Ubuntu 团队这次用 TLA+ 发现的，是业界最成熟、最广泛使用的数据库里的漏洞——这个事实本身就在告诉所有人：你信任的那些基础软件，也可能藏着连它们的作者都不知道的问题。而数学，是找到这些问题的唯一可靠途径。
16 年前，人们靠直觉和勤奋来测试软件。 16 年后，一道数学题用 20 步就找到了人类肉眼永远看不到的漏洞。
这是工具进步了。
参考链接：