我们如何在加固Turso时使用Quint在SQLite中发现超过10个漏洞

# 我们如何用 Quint 在加固 Turso 时发现 SQLite 中超过 10 个 Bug 来源：https://turso.tech/blog/how-we-used-quint-to-find-over-10-bugs-in-sqlite 从我们启动 Turso 的那一刻起，我们就将测试视为重中之重。这别无选择：Turso 是对 SQLite 的重写，而 SQLite 在可靠性方面设定了极高的标准。我们始终听到，*这一点*比任何具体功能都更让用户喜爱 SQLite。 我们的第一个版本就已经内置了确定性仿真测试机制。如今，除了最初的 DST，我们还拥有差分测试工具、模糊测试器、并发模拟器，并充分利用了 [Antithesis](http://antithesis.com/)。 我们绝不会错过任何进一步提升的机会。正因如此，我们吸引了一大群质量爱好者加入我们的开源社区。本文将详细介绍我们的开源贡献者之一 Pavan Nambi 如何使用 [Quint](https://github.com/informalsystems/quint) 如此严格地加强测试，以至于最终在 SQLite 本身中发现了 10 个（甚至更多）Bug。 ## 形式化方法 尽管我们在测试方面纪律严明，但形式化方法仍是我们进展缓慢的一个领域。传统上，形式化方法对普通人来说非常难以接近，并且通常伴随着"谁来监视监视者"的附加挑战，即如何验证系统模型本身的正确性。TLA+ 是形式化验证的黄金标准，但最近也出现了其他工具，试图解决形式化方法中可及性的问题。 其中一个工具就是 [Quint](https://github.com/informalsystems/quint)。根据其 GitHub 页面，Quint "将动作时序逻辑 [TLA](https://en.wikipedia.org/wiki/Temporal_logic_of_actions) 的坚实理论基础与最先进的类型检查和开发工具相结合"。 Pavan 决定尝试一下，但很快就得出结论，尝试对整个系统进行建模几乎是不可能的。就在这时，他有了一个想法：大多数使用 SQLite 的驱动程序都是通过 C API 来使用的。Turso 暴露了一个与 SQLite 兼容的 C API。这个 C API 也文档齐全、规范明确。如果他能用 Quint 对 C API 进行建模，那就能达到相当不错的覆盖率。API 的规范写得很好，更容易为其编写 Quint 规范，而且我们还可以针对 SQLite 本身运行它，以双重检查该规范是否正确。 ## 使用 Quint 测试 SQLite 有了这个想法，过程变得简单了。我们只需重复以下步骤： - 选取一个文档化的 SQLite C API 契约，然后仅针对该契约建模所需的状态和属性。 - 生成一个小 trace。 - 针对 SQLite 运行它。 - 将文档化结果与观察结果进行比较。 如果模型检查器失败，我们会得到一个反例：一系列导致违规的状态序列。 期望是，针对 SQLite 运行它有助于我们验证模型。在许多情况下确实如此。但在其他情况下，经过仔细检查，系统与模型存在偏差，因为系统本身有误。 ### 一个例子：sqlite3_deserialize() 这里有一个例子：函数 `sqlite3_deserialize()` 允许你获取一个序列化的 SQLite 数据库映像，并将其作为内存数据库加载到数据库连接中。当你有一个基于文件的数据库，但希望完全加载到内存中并随后作为内存数据库进行操作时，这很有用。 根据该 API 的规范，如果目标数据库当前处于读事务中，或者涉及备份操作，则 `sqlite3_deserialize()` 应返回 `SQLITE_BUSY`。 Quint 通过生成 traces 来工作。Traces 只是一系列状态，而不是 SQL 语句。这些 traces 可以被翻译成你想要的任何东西，以便对系统执行。在我们的案例中，是翻译成一个小的 C 程序。 Quint 模型自动生成了一个违反了该契约的 trace： 1. 打开数据库。 2. 创建表。 3. 序列化数据库。 4. 开始从数据库读取。 5. 在读事务活动期间，调用 `sqlite3_deserialize()`，期望返回 `SQLITE_BUSY`。 总之，如果在反序列化操作期间正在进行读事务，数据库应该返回 busy。C 程序根据 trace 将数据库从一个状态移动到另一个状态。但在这个案例中，数据库没有返回 `SQLITE_BUSY`：它反而崩溃了。 崩溃有一个很大的优点：很容易知道这不是模型的问题，因为崩溃几乎从来不应该是正确的行为。 这个问题在 SQLite 的[这个提交](https://sqlite.org/src/vinfo/b7b0745d6def6b14?diff=1&proof=980092359)中得到了修复。 ## 随后还有更多 在整个使用 Quint 的探索过程中，发现了以下 Bug： - EXISTS 到 JOIN 的优化错误地将 LIMIT/OFFSET 应用于重复的 join 行，仿佛它们是真实输出行（[链接](https://sqlite.org/forum/info/2c43f36255a630e3)） - 嵌套的 EXISTS 到 JOIN 重写丢失了外部关联，导致有效行被过滤掉（[链接](https://sqlite.org/forum/info/077c02e8edbb6762)） - 带有嵌入式引号的带引号约束名可能通过 DROP CONSTRAINT 变得无法删除（[链接](https://sqlite.org/forum/info/b36322acab668a8e)） - 当 WHERE 子句中的相关子查询被 BETWEEN 包装时，UPDATE 单次传递规划中的错误结果回归（[链接](https://sqlite.org/forum/info/0ab502f519068a50)） - 当 ALTER ADD CHECK 与内部 sqlite_ 表一起使用时，SQLite 崩溃（[链接](https://sqlite.org/forum/info/6256ee34ed09078b)） - sqlite3_deserialize() 在活动读事务期间崩溃而非返回 SQLITE_BUSY（[链接](https://sqlite.org/forum/info/39134ba0298d89cf)） - sqlite3_deserialize() 应拒绝涉及备份的数据库，但备份/反序列化交错导致崩溃（[链接](https://sqlite.org/forum/info/15a83c3a9df01cdd)） - sqlite3_mutex 128 字节对齐的未定义行为（[链接](https://sqlite.org/forum/info/ca4fc78036c3f3ae)） - sqlite3changegroup_change_finish() 中 NULL pzErr 崩溃（[链接](https://sqlite.org/forum/info/80e765eb24d26f01)） - xfer 优化通过 ANY 绕过了 BLOB 类型检查，导致 integrity_check 失败（[链接](https://sqlite.org/forum/info/4955d2235c22ef4e)） - xfer 优化绕过了检查约束，导致数据库不一致（[链接](https://sqlite.org/forum/info/6dcc95e3ca750dbc)） - sqlite3_uri_int64() 对于无效的现有值返回默认值而非零（文档不匹配，非真正 Bug）（[链接](https://sqlite.org/forum/info/a9d160c662548fe6)） 除了上述发现之外，还有其它发现正在与 SQLite 团队合作验证中。 ## 总结 形式化方法，特别是 Quint，能够探索 Turso 模拟器之前无法触及的规范部分。总体概念类似，但 Quint 不是生成随机 SQL 语句序列并强制执行系统级属性，而是生成一系列 traces，这些 traces 可以翻译成我们想要的任何底层平台。 在这个案例中，我们将 Quint traces 翻译成与 C API 交互的 C 程序。Turso 因此受益。SQLite 也是如此：至少发现了 10 个 Bug，并已报告和修复。 SQLite 是一款出色的软件，已经存在并经过严格测试数十年。然而，仍然潜伏着之前手段未能发现的 Bug。形式化方法发现了它们。