提交与退订相关提交成功感谢您与我们联系我们的团队成员将尽快与您取得联系。您已成功退订感谢您订阅我们的时事通讯在这些定期邮件中您将了解到 Ubuntu 的最新动态以及即将举办的活动信息届时还有机会与我们的团队成员面对面交流。您的偏好设置已成功更新。请重试或者提交错误报告。导航与博客相关有 Canonical Ubuntu 相关导航包括搜索、菜单、产品、用例、支持、社区、下载 Ubuntu 等。还有博客相关有物联网、桌面端、云与服务器、网页与设计、人员与文化等分类。用 TLA 追查 SQLite 漏洞2026 年 6 月 25 日阿尔贝托·卡雷罗发布文章本文由 Canonical 的 dqlite 团队成员马尔科·马尼诺和阿尔贝托·卡雷罗撰写。文章聚焦用 TLA 追查一个存在 16 年的 SQLite 漏洞探讨 dqlite 是否会受影响。SQLite 漏洞剖析最近SQLite 发布新版本修复了一个长期存在的漏洞该漏洞与预写日志Write Ahead LogWAL的检查点机制有关可能导致数据库损坏。此漏洞关键在于其在代码库中存在时间长、发现和复现难度大自 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 中需将函数拆分为不同操作模拟从共享内存中读取数据的过程因为共享内存可能会发生变化。