使用 TLA+ 追踪一个存在16年之久的 SQLite WAL 漏洞

# 用 TLA+ 追踪一个 16 年的 SQLite 漏洞：dqlite 是否受影响？ | Ubuntu 来源：https://ubuntu.com/blog/hunting-a-16-year-old-sqlite-bug-with-tla-is-dqlite-affected - 分享到： - Facebook (https://www.facebook.com/sharer/sharer.php?u=https://www.ubuntu.com/blog/hunting-a-16-year-old-sqlite-bug-with-tla-is-dqlite-affected) - Twitter (https://twitter.com/share?text=Hunting%20a%2016-year-old%20SQLite%20bug%20with%20TLA%2B%3A%20is%20dqlite%20affected%3F&url=https://www.ubuntu.com/blog/hunting-a-16-year-old-sqlite-bug-with-tla-is-dqlite-affected&hashtags=ubuntu) - LinkedIn (https://www.linkedin.com/shareArticle?mini=true&url=https://www.ubuntu.com/blog/hunting-a-16-year-old-sqlite-bug-with-tla-is-dqlite-affected&title=Hunting%20a%2016-year-old%20SQLite%20bug%20with%20TLA%2B%3A%20is%20dqlite%20affected%3F) *本文由 Canonical 的 dqlite 团队 Marco Manino 和 Alberto Carretero 撰写*。 ## 1. SQLite 漏洞剖析 最近 SQLite 发布了一个新版本 (https://www.sqlite.org/releaselog/3_51_3.html)，修复了一个长期存在的漏洞 (https://www.sqlite.org/wal.html#walresetbug)，该漏洞涉及预写日志（WAL）检查点（checkpoint）的方式，会导致数据库损坏。这个漏洞的重要之处不在于它对现实世界的影响（非常低），而在于它在仓库中存在了多久、发现它有多难，以及复现它有多难。事实上，这个漏洞自 2010 年以来就一直存在，*长达 16 年*！此外，对我们 dqlite 团队来说，关键问题是：dqlite 是否会受此影响？为了弄清这一点，我们首先需要理解导致数据库损坏的确切步骤序列。为此，我们将使用 TLA+ 对 SQLite 的行为进行建模，快速找到一条能让我们推理此漏洞的轨迹。然后，我们将创建一个不同的模型来描述 dqlite 如何使用 sqlite，并检查该漏洞是否可能发生。 ## 2. SQLite 中的 WAL 和检查点简要介绍 SQLite 使用 WAL 模式来使读取操作不被写入操作阻塞。其实现方式是将数据写入一个称为预写日志（WAL）的特殊临时区域。写入者可以向 WAL 末尾追加内容，而读取者可以忽略新数据直到其稳定。最终，临时区域会被移到数据库中；这称为检查点（checkpoint）。为了防止 WAL 无限增长，如果前一次检查点成功移动了所有页面，写入者会尝试“重置”它——即覆盖它。如果你想了解更多，可以在官方文档 (https://sqlite.org/wal.html) 中找到非常清晰的描述。 SQLite 使用锁和共享内存来协调对 WAL 的更改。对于我们的用例，只需考虑写入和检查点即可；因此，我们只关心两个锁： - 检查点锁（`CKPT_LOCK`），在执行检查点之前获取，以防止多个检查点同时发生 - 写入锁（`WRITE_LOCK`），在向 WAL 追加新页面之前获取 共享内存包含协调写入者、检查点和读取者所需的信息，以及一个用于索引 WAL 中页面以提高读取性能的数据结构。如我们所说，读取者并不参与；因此，唯一有趣的字段是： - `walSalt`，包含一个计数器，每次 WAL 重置时会递增 - `mxFrame`，表示 WAL 的长度 - `nBackfill`，表示已经检查点通过的页面数量，也就是说，`[nBackfill+1, mxFrame]` 此时尚未复制到数据库 ## 3. 在 TLA+ 中对漏洞进行建模 编写 TLA+ 的部分难点在于决定要建模什么以及*不*建模什么。我们希望设计出尽可能简单的规范，同时仍然忠实于现实，并能从中提取有用的见解。 首先要建模的是上一节描述的数据库和 WAL： `` \* 文件。 VARIABLE wal VARIABLE db \* wal-index 变量： VARIABLE nBackfill VARIABLE mxFrame \* 我们只捕获 salt 的连续部分。 VARIABLE walSalt Init ≜ \* wal 和 db 初始为空。 ∧ wal = ⟨⟩ ∧ db = {} ∧ nBackfill = 0 ∧ mxFrame = 0 ∧ walSalt = 0 `` 由于生成数据不在模型范围内，我们可以采用更简单的方法。我们可以将每个数据页建模为一个唯一的数字，那么 WAL 可以是这些数字的序列，而数据库是它们的集合。具体来说，检查点会将 WAL 序列中的页面按照追加到 WAL 的顺序移动到数据库的集合中。要生成唯一数字，使用一个不断递增的计数器即可。 我们需要建模两个相互交互并产生漏洞的动作：追加和检查点。让我们先查看 SQLite 中向 WAL 追加页面的 C 代码，以定义我们的 TLA+ 动作： 负责向 WAL 追加帧的 SQLite 代码`` static int walFrames( Wal *pWal, /* Wal 句柄 */ int szPage, /* 数据库页面大小（字节） */ PgHdr *pList, /* 待写入的脏页列表 */ Pgno nTruncate, /* 提交后的数据库大小 */ int isCommit, /* 是否为提交 */ int sync_flags /* 传递给 OsSync() 的标志（或 0） */ ){ int rc; /* 用于捕获返回码 */ u32 iFrame; /* 下一个帧地址 */ PgHdr *p; /* 遍历 pList 的迭代器 */ PgHdr *pLast = 0; /* 列表中的最后一帧 */ int nExtra = 0; /* 最后一页的额外副本数量 */ int szFrame; /* 单个帧的大小 */ i64 iOffset; /* WAL 文件中的下一个写入字节 */ WalWriter w; /* 写入者 */ u32 iFirst = 0; /* 可能被覆盖的第一个帧 */ WalIndexHdr *pLive; /* 指向共享头的指针 */ assert( pList ); assert( pWal->writeLock ); /* 如果这组帧完成了事务，则 nTruncate>0。 ** 如果 nTruncate==0，则这组帧不会完成事务。 */ assert( (isCommit!=0)==(nTruncate!=0) ); #if defined(SQLITE_TEST) && defined(SQLITE_DEBUG) { int cnt; for(cnt=0, p=pList; p; p=p->pDirty, cnt++){} WALTRACE(("WAL%p: frame write begin. %d frames. mxFrame=%d. %s\n", pWal, cnt, pWal->hdr.mxFrame, isCommit ? "Commit" : "Spill")); } #endif pLive = (WalIndexHdr*)walIndexHdr(pWal); if( memcmp(&pWal->hdr, (void *)pLive, sizeof(WalIndexHdr))!=0 ){ iFirst = pLive->mxFrame+1; } /* 检查是否可以将这些帧写入日志文件的起始位置， ** 而不是追加到 pWal->hdr.mxFrame 处。 */ if( SQLITE_OK!=(rc = walRestartLog(pWal)) ){ return rc; } /* 如果这是写入日志的第一帧，则将 WAL 头写入 WAL 文件的起始位置。 ** 有关 WAL 头格式的描述，请参见本源文件顶部的注释。 */ iFrame = pWal->hdr.mxFrame; if( iFrame==0 ){ u8 aWalHdr[WAL_HDRSIZE]; /* 用于组装 wal-header 的缓冲区 */ u32 aCksum[2]; /* wal-header 的校验和 */ sqlite3Put4byte(&aWalHdr[0], (WAL_MAGIC | SQLITE_BIGENDIAN)); sqlite3Put4byte(&aWalHdr[4], WAL_MAX_VERSION); sqlite3Put4byte(&aWalHdr[8], szPage); sqlite3Put4byte(&aWalHdr[12], pWal->nCkpt); if( pWal->nCkpt==0 ) sqlite3_randomness(8, pWal->hdr.aSalt); memcpy(&aWalHdr[16], pWal->hdr.aSalt, 8); walChecksumBytes(1, aWalHdr, WAL_HDRSIZE-2*4, 0, aCksum); sqlite3Put4byte(&aWalHdr[24], aCksum[0]); sqlite3Put4byte(&aWalHdr[28], aCksum[1]); pWal->szPage = szPage; pWal->hdr.bigEndCksum = SQLITE_BIGENDIAN; pWal->hdr.aFrameCksum[0] = aCksum[0]; pWal->hdr.aFrameCksum[1] = aCksum[1]; pWal->truncateOnCommit = 1; rc = sqlite3OsWrite(pWal->pWalFd, aWalHdr, sizeof(aWalHdr), 0); WALTRACE(("WAL%p: wal-header write %s\n", pWal, rc ? "failed" : "ok")); if( rc!=SQLITE_OK ){ return rc; } /* 同步头（除非 SQLITE_IOCAP_SEQUENTIAL 为真， ** 或者通过 PRAGMA synchronous=OFF 关闭所有同步）。 ** 否则，WAL 重启后的乱序写入可能导致数据库损坏。 ** 请参见 ticket： ** ** https://sqlite.org/src/info/ff5be73dee */ if( pWal->syncHeader ){ rc = sqlite3OsSync(pWal->pWalFd, CKPT_SYNC_FLAGS(sync_flags)); if( rc ) return rc; } } if( (int)pWal->szPage!=szPage ){ return SQLITE_CORRUPT_BKPT; /* TH3 测试案例：cov1/corrupt155.test */ } /* 设置将帧写入 WAL 所需的信息 */ w.pWal = pWal; w.pFd = pWal->pWalFd; w.iSyncPoint = 0; w.syncFlags = sync_flags; w.szPage = szPage; iOffset = walFrameOffset(iFrame+1, szPage); szFrame = szPage + WAL_FRAME_HDRSIZE; /* 将所有帧恰好一次写入日志文件 */ for(p=pList; p; p=p->pDirty){ int nDbSize; /* 通常为 0。正数表示提交标志 */ /* 检查当前事务是否已将该页写入 wal 文件。 ** 如果是，则覆盖现有帧，并将 Wal.writeLock 设置为 WAL_WRITELOCK_RECKSUM - ** 表示提交时必须重新计算校验和。 */ if( iFirst && (p->pDirty || isCommit==0) ){ u32 iWrite = 0; VVA_ONLY(rc =) walFindFrame(pWal, p->pgno, &iWrite); assert( rc==SQLITE_OK || iWrite==0 ); if( iWrite>=iFirst ){ i64 iOff = walFrameOffset(iWrite, szPage) + WAL_FRAME_HDRSIZE; void *pData; if( pWal->iReCksum==0 || iWriteiReCksum ){ pWal->iReCksum = iWrite; } pData = p->pData; rc = sqlite3OsWrite(pWal->pWalFd, pData, szPage, iOff); if( rc ) return rc; p->flags &= ~PGHDR_WAL_APPEND; continue; } } iFrame++; assert( iOffset==walFrameOffset(iFrame, szPage) ); nDbSize = (isCommit && p->pDirty==0) ? nTruncate : 0; rc = walWriteOneFrame(&w, p, nDbSize, iOffset); if( rc ) return rc; pLast = p; iOffset += szFrame; p->flags |= PGHDR_WAL_APPEND; } /* 如果需要，重新计算 wal 文件中的校验和。 */ if( isCommit && pWal->iReCksum ){ rc = walRewriteChecksums(pWal, iFrame); if( rc ) return rc; } /* 如果这是事务的结束，则可能需要填充 ** 事务和/或同步 WAL 文件。 ** ** 仅当这组帧完成事务并且 PRAGMA synchronous=FULL 时才会 ** 进行填充和同步。如果 synchronous==NORMAL 或 synchronous==OFF， ** 则不需要填充或同步。 ** ** 如果定义了 SQLITE_IOCAP_POWERSAFE_OVERWRITE，则不需要填充，仅进行同步。 ** 如果需要填充，则重复最后一帧（带有提交标记）直到跨越下一个扇区边界。 ** 仅同步 WAL 中最后一个扇区边界之前的部分； ** 在同步之后写入最后一帧超出扇区边界的部分。 */ if( isCommit && WAL_SYNC_FLAGS(sync_flags)!=0 ){ int bSync = 1; if( pWal->padToSectorBoundary ){ int sectorSize = sqlite3SectorSize(pWal->pWalFd); w.iSyncPoint = ((iOffset+sectorSize-1)/sectorSize)*sectorSize; bSync = (w.iSyncPoint==iOffset); testcase( bSync ); while( iOffsettruncateOnCommit && pWal->mxWalSize>=0 ){ i64 sz = pWal->mxWalSize; if( walFrameOffset(iFrame+nExtra+1, szPage)>pWal->mxWalSize ){ sz = walFrameOffset(iFrame+nExtra+1, szPage); } walLimitSize(pWal, sz); pWal->truncateOnCommit = 0; } /* 将数据追加到 wal-index。不需要锁定 ** wal-index 来执行此操作，因为对 wal-index 持有的 SQLITE_SHM_WRITE 锁 ** 保证没有其他写入者，并且没有现有读取者可能使用的数据被覆盖。 */ iFrame = pWal->hdr.mxFrame; for(p=pList; p && rc==SQLITE_OK; p=p->pDirty){ if( (p->flags & PGHDR_WAL_APPEND)==0 ) continue; iFrame++; rc = walIndexAppend(pWal, iFrame, p->pgno); } assert( pLast!=0 || nExtra==0 ); while( rc==SQLITE_OK && nExtra>0 ){ iFrame++; nExtra--; rc = walIndexAppend(pWal, iFrame, pLast->pgno); } if( rc==SQLITE_OK ){ /* 更新头的私有副本。 */ pWal->hdr.szPage = (u16)((szPage&0xff00) | (szPage>>16)); testcase( szPage<=32768 ); testcase( szPage>=65536 ); pWal->hdr.mxFrame = iFrame; if( isCommit ){ pWal->hdr.iChange++; pWal->hdr.nPage = nTruncate; } /* 如果是提交，也更新 wal-index 头。 */ if( isCommit ){ walIndexWriteHdr(pWal); pWal->iCallback = iFrame; } } WALTRACE(("WAL%p: frame write %s\n", pWal, rc ? "failed" : "ok")); return rc; } static int walRestartLog(Wal *pWal){ int rc = SQLITE_OK; int cnt; if( pWal->readLock==0 ){ volatile WalCkptInfo *pInfo = walCkptInfo(pWal); assert( pInfo->nBackfill==pWal->hdr.mxFrame ); if( pInfo->nBackfill>0 ){ u32 salt1; sqlite3_randomness(4, &salt1); rc = walLockExclusive(pWal, WAL_READ_LOCK(1), WAL_NREADER-1); if( rc==SQLITE_OK ){ /* 如果所有读者都在使用 WAL_READ_LOCK(0)（换句话说，如果没有 ** 读者当前正在使用 WAL），则事务的帧将覆盖现有日志的起始部分。 ** 相应地更新 wal-index 头。 ** ** 理论上，此时只更新头的缓存也是可以的。但更新实际的 wal-index 头 ** 也是安全的，并且意味着如果此事务被回滚，sqlite3WalUndo() 无需处理特殊情况。 */ walRestartHdr(pWal, salt1); walUnlockExclusive(pWal, WAL_READ_LOCK(1), WAL_NREADER-1); }else if( rc!=SQLITE_BUSY ){ return rc; } } walUnlockShared(pWal, WAL_READ_LOCK(0)); pWal->readLock = -1; cnt = 0; do{ int notUsed; rc = walTryBeginRead(pWal, ¬Used, 1, &cnt); }while( rc==WAL_RETRY ); assert( (rc&0xff)!=SQLITE_BUSY ); /* 当 useWal==1 时不可能出现 BUSY */ testcase( (rc&0xff)==SQLITE_IOERR ); testcase( rc==SQLITE_PROTOCOL ); testcase( rc==SQLITE_OK ); } return rc; } static void walRestartHdr(Wal *pWal, u32 salt1){ volatile WalCkptInfo *pInfo = walCkptInfo(pWal); int i; /* 循环计数器 */ u32 *aSalt = pWal->hdr.aSalt; /* 大端盐值 */ pWal->nCkpt++; pWal->hdr.mxFrame = 0; sqlite3Put4byte((u8*)&aSalt[0], 1 + sqlite3Get4byte((u8*)&aSalt[0])); memcpy(&pWal->hdr.aSalt[1], &salt1, 4); walIndexWriteHdr(pWal); AtomicStore(&pInfo->nBackfill, 0); pInfo->nBackfillAttempted = 0; pInfo->aReadMark[1] = 0; for(i=2; iaReadMark[i] = READMARK_NOT_USED; assert( pInfo->aReadMark[0]==0 ); } `` 我们在上面的代码中高亮显示了相关部分，现在来看如何将其转化为 TLA+。为了建模所需的行为，我们将重点关注上面代码中的两个动作：`WalAppendTakeLock` 和 `WalAppend`。我们还需要一个新的变量来表示写入锁（上面代码中的第一个 `assert`）： `` \* 写入 WAL 所需的锁。 VARIABLE writeLock WalAppendTakeLock ≜ ∧ writeLock = "notTaken" ∧ writeLock' = "takenForAppend" ∧ UNCHANGED ⟨ wal, db, nBackfill, mxFrame, frameNumber, checkPointState, safeMxFrame, walSalt, pWalSalt ⟩ WalAppend ≜ ∧ writeLock = "takenForAppend" \* sqlite 代码中的 if 条件被写为断言，因为 \* 检查 pWal->readLock == 0 给出了相同的保证。如果 \* 写入者已获取读锁 0，则表示 wal 中没有任何帧未被检查点通过。 ∧ IF (nBackfill > 0 ∧ mxFrame = nBackfill) THEN \* 重启 Wal 并追加。 \* 我们没有读取者，因此每个检查点后的写入者都会重启 wal。 ∧ wal' = ⟨ frameNumber ⟩ ∧ mxFrame' = 1 ∧ nBackfill' = 0 ∧ walSalt' = walSalt + 1 ELSE ∧ wal' = Append(wal, frameNumber) ∧ mxFrame' = mxFrame + 1 ∧ UNCHANGED ⟨ nBackfill, walSalt ⟩ ∧ frameNumber' = frameNumber + 1 ∧ writeLock' = "notTaken" ∧ UNCHANGED ⟨ db, checkpoint_vars ⟩ `` 接下来，让我们关注检查点，这是谜题的另一部分： 负责检查点的 SQLite 代码`` static int walCheckpoint( Wal *pWal, /* Wal 连接 */ sqlite3 *db, /* 在此句柄上检查中断 */ int eMode, /* PASSIVE、FULL 或 RESTART 之一 */ int (*xBusy)(void*), /* 忙时调用的函数 */ void *pBusyArg, /* xBusyHandler 的上下文参数 */ int sync_flags, /* OsSync() 的标志（或 0） */ u8 *zBuf /* 临时缓冲区 */ ){ int rc = SQLITE_OK; /* 返回码 */ int szPage; /* 数据库页面大小 */ WalIterator *pIter = 0; /* Wal 迭代器上下文 */ u32 iDbpage = 0; /* 要写入的下一个数据库页面 */ u32 iFrame = 0; /* 包含 iDbpage 数据的 Wal 帧 */ u32 mxSafeFrame; /* 可以回填的最大帧 */ u32 mxPage; /* 要写入的最大数据库页面 */ int i; /* 循环计数器 */ volatile WalCkptInfo *pInfo; /* 共享指针 */ int(*xBusy2)(void*) = xBusy; /* 忙时处理程序 */ void *pBusyArg2 = pBusyArg; /* 忙时处理程序参数 */ int nBackfillAttempted = 0; /* 已尝试的回填数 */ int bBusy = 0; /* 如果 xBusy 返回 true 则为真 */ static const u8 aFrame[4] = { 0, 0, 0, 0 }; /* 用于校验的帧数据 */``