スキルベースの SQLite バグ解析と dqlite の安全性への影響

Canonical の dqlite チーム所属の Marco Manino氏と Alberto Carretero氏が執筆した記事です。 本記事は、SQLite に存在していた深刻なバグの解析を行い、同じく分散データベースである dqlite がこの脆弱性から無傷かどうかに焦点を当てています。

1. SQLite バグの構造分析と意義

最近、SQLite は長年存在した問題点の一つ、WAL (Write Ahead Log) のチェックポイント処理におけるバグを修正する新版本を発表しました。

• データ破損リスクは低い: このバグが直接引き起こすデータ損失の可能性は実用的には非常に低いです。
• 最も重要な発見点:
  • バグがリポジトリに存在した期間：実に 16 年間（2010 年以降）。
  • 見つけるのに要した困難さ。
  • 再現させるのに必要な困難さ。

dqlite チームにとっての懸念点: 「dqlite もこの影響を受けるのか？」という点が最大の関心事です。

バグ解析のアプローチ

データベースが破損するに至る一連の手順を理解するためには、以下を実施します。

1. TLA+（形式記述言語）を用いたモデル化
   • SQLite の動作モデルを作成し、バグを誘発する実行経路（トレース）を特定します。
2. dqlite 特有のモデル作成
   • dqlite が SQLite をどのように利用しているかを記述した別のモデルを作成。
3. 影響確認
   • dqlite の環境下でも同様のバグが発生する可能性を確認します。

2. SQLite における WAL とチェックポイントの概要

SQLite は、読み書き処理をブロックしないために WAL モードを使用しています。

ワークフロー

1. 追記 (Append): 書き込み側は、特別な暫定領域である WAL の末尾 にデータを追記します。
2. 無視: 読み込み側は、データがメインデータベースへ移動するまで WAL を無視します。
3. チェックポイント (Checkpoint): 暫定領域のデータをメインデータベースへ移動させる作業です。

リセットロジック

• WAL が無限に成長しないよう、前回のチェックポイントで全ページが移動済みであれば、書き込み側は WAL を**「リセット」（上書き）**しようとします。

ロッキング機構

SQLite は WAL への変更をロックと共有メモリで管理します。本件の分析では以下の 2 つのロックが重要になります。

• チェックポイントロック (CKPT_LOCK)
  • チェックポイントを走る前に取得されます。
  • 複数回の同時実行を防ぐ役割を持ちます。
• 書き込みロック (WRITE_LOCK)
  • WAL に新しいページを追記する前に取得されます。

共有メモリ構造体 (WAL-index)

読み込み側の関与を除外し、以下のフィールドが本件の分析において重要です。

• walSalt

  : WAL がリセットされるたびにインクリメントされるカウンター。

• mxFrame

  : WAL の長さ（フレーム数）。

• nBackfill

  : すでにチェックポイントされたページの量を表す。

  • [nBackfill+1, mxFrame]

    範囲のデータは、まだデータベースへコピーされていません。

3. TLA+ を用いたバグモデル化

TLA+ を記述する際の課題は、「何をモデル化すべきか」そして「何は除外すべきか」を判断することです。我々は現実を反映しつつ、最も単純で有用な仕様に至りました。

データベースと WAL のモデル定義

データの生成モデル化はスコープ外とするため、簡素化されたアプローチを採用します。

• 各データページを一意の番号として捉える。
• WAL: ページ番号のシーケンス。
• データベース: ページ番号の集合。
• チェックポイント時：WAL のシーケンス内のページが、追記された順序に合わせてデータベースへ移動する。

\* 変数定義
VARIABLE wal          \* ファイル群（シーケンス）
VARIABLE db           \* データベース（集合）

VARIABLE nBackfill    \* インデックス変数
VARIABLE mxFrame      \* 最後のフレーム番号
VARIABLE walSalt      \* salt のシーケンシャル部分のみ捕捉

Init ≜
    ∧ wal = ⟨⟩         \* 初期状態：WAL は空
    ∧ db = {}          \* データベースは空
    ∧ nBackfill = 0
    ∧ mxFrame = 0
    ∧ walSalt = 0

追記ロジック (

WalAppend

)

SQLite の C コードを参考にした TLA+ アクションです。特に重要な要素は以下の通りです。

• 必要アクション:

  WalAppendTakeLock

  と

  WalAppend

  。
• ロック変数: 書き込みを表す

  writeLock

  を追加。

\* WAL に書き込むためのロック状態
VARIABLE writeLock

WalAppendTakeLock ≜
    ∧ writeLock = "notTaken"
    ∧ writeLock' = "takenForAppend"
    ∧ UNCHANGED ⟨ wal, db, nBackfill, mxFrame, frameNumber, checkPointState, safeMxFrame, walSalt, pWalSalt ⟩

WalAppend ≜
    ∧ writeLock = "takenForAppend"
    
    \* 条件：WAL がリセット済みか（読み込み側がいないため常に成立）
    IF (nBackfill > 0 ∧ mxFrame = nBackfill)
       THEN
        \* WAL の再開始と追記。WAL を破棄し、新しいフレームから書き始める。
        ∧ wal' = ⟨ frameNumber ⟩
        ∧ mxFrame' = 1
        ∧ nBackfill' = 0
        ∧ walSalt' = walSalt + 1          \* Salt のリセットとインクリメント
       ELSE
        \* 通常の追記処理。
        ∧ wal' = Append(wal, frameNumber)
        ∧ mxFrame' = mxFrame + 1
        ∧ UNCHANGED ⟨ nBackfill, walSalt ⟩
    
    ∧ frameNumber' = frameNumber + 1
    ∧ writeLock' = "notTaken"
    ∧ UNCHANGED ⟨ db, checkpoint_vars ⟩

チェックポイントロジック (

Checkpoint

)

共有メモリの読み出しがその間に変化しうるため、複数のアクションに分けて記述します。

• pWal

  : WAL-index ヘッダーのコピー（不変）。

• pInfo

  : 共有メモリへのポインタ（揮発性）。
• 重要概念:

  backfill

  はライブヘッダーから読み込まれるのに対し、

  safeMxFrame

  は古いコピーから読み込まれます。

\* チェックポイント用変数
VARIABLE safeMxFrame  \* ヘッダーのコピー値
VARIABLE pWalSalt     \* Salt のコピー値
VARIABLE checkPointState \* 状態機: notStarted -> copiedHeader -> waitingForLock -> (finished) -> notStarted

CheckPointCopyHeader ≜
    ∧ checkPointState = "notStarted"
    ∧ safeMxFrame' = mxFrame       \* ライブ mxFrame の読み取り
    ∧ pWalSalt' = walSalt          \* ライブ walSalt の読み取り
    ∧ checkPointState' = "copiedHeader"
    ∧ UNCHANGED ⟨ wal, nBackfill, db, mxFrame, frameNumber, walSalt, writeLock ⟩

StartCheckpoint ≜
    ∧ checkPointState = "copiedHeader"
    \* 重要：ここでは backfill を safeMxFrame と比較
    ∧ IF nBackfill < safeMxFrame
       THEN checkPointState' = "waitingForLock"  \* チェックポイント開始の準備完了
       ELSE checkPointState' = "notStarted"      \* もう追記がないため不要
    ∧ UNCHANGED ⟨ wal, nBackfill, db, mxFrame, frameNumber, safeMxFrame, walSalt, pWalSalt, writeLock ⟩

Checkpoint ≜
    ∧ checkPointState = "waitingForLock"
    
    \* ページを wal から db へ移動（コピー処理）
    ∧ db' = db ∪ { wal[j] : j ∈ nBackfill+1‥Len(wal) }
    
    \* nBackfill は安全なフレーム数まで進める
    ∧ nBackfill' = safeMxFrame
    
    \* 状態のクリア
    ∧ safeMxFrame' = 0
    ∧ pWalSalt' = 0
    ∧ checkPointState' = "notStarted"
    ∧ UNCHANGED ⟨ mxFrame, wal, frameNumber, walSalt, writeLock ⟩

詳細な仕様のダウンロード: TLA+ Model Source

4. バグの再現と分析

モデルを構築し、データ損失を引き起こす**不変条件（Invariant）**を定義します。

\* データベースに「穴」が生じないこと。
NoPageIsLost ≜ ∀ f ∈ 1‥Cardinality(db) : f ∈ db

モデルチェックの結果

モデルチェッカーを実行したところ、瞬く間に**矛盾する例（カウンターサンプル）**が見つかりました。

• 発生ステップ: データベース内のページ欠落を引き起こす状態遷移はわずか 20 ステート で発生します。
• 妥当性の確認: このシーケンスは SQLite 自身から発表されたバグ報告の内容と非常に類似しており、モデルの正確性を検証しています。

競合状態の詳細分析 (Trace Analysis)

以下のようなステップでバグが誘発されます。

1. Step 1: コネクション A がチェックポイントを起動（完了待ちの状態）。
2. Step 2: ショート後に、コネクション B もチェックポイントを起動。
3. Step 3: ステップ 2 の間、別のコネクション C によりトランザクションがコミットされ、WAL がリセットされ、新しいデータが WAL 先頭へ追記されます。
4. Step 4 (誤認): ステップ 2 のチェックポイント処理が、ステップ 3 の WAL リセットに気づきません。
   • 結果として、WAL-Index ヘッダーのフィールドを誤って設定。
   • 「一部のみチェック済み」として認識されつつ、実際は未チェックポイントの状態になっています。
5. Step 5: さらに多くのトランザクションがコミットされ、WAL がさらに成長します。
6. Step 6 (データ損失): ステップ 3 で書き込まれたデータの一部が、ステップ 2 のチェックポイント処理中にスキップされます。結果としてデータベースファイルに到達せず、破損が発生。

5. dqlite に影響はあるのか？

この疑問を解くため、SQLite との差異を捉えた dqlite 用のモデルを作成し、再度モデルチェックを実行しました。

dqlite の防衛策

dqlite は Raft による書き込み調整を必要とするため、より制限的なアプローチを採用しています。

1. 全ユーザーチェックポイントと自動チェックポイントをブロック。
2. ロック強化: SQLite よりも多くのロックを取得し、チェックポイント中の読み書きの同時実行を防ぎます。
3. 「一時停止全世界」(Stop-the-world) の設計: チェックポイント処理はシステム全体を一時停止するアクションとなります。

dqlite のコード特徴

SQLite の実装に対して、以下の違いがあります。

static int vfsCheckpoint(sqlite3 *conn, struct vfsMainFile *f) {
    // ... (共有メモリロック取得など)
    
    /* すべてのロックを占有し、何ものも進行させないことを試みる */
    int rv = vfsShmLock(&f->database->shm, 0, SQLITE_SHM_NLOCK, true);
    if (rv != SQLITE_OK) return rv;
    
    f->exclMask = VFS__CHECKPOINT_MASK;

    PRE(f->database->wal.n_tx == 0); // トランザクションがないことを確認

    int wal_size;
    int ckpt;
    /* 読みのトランザクションが進行中でないため、WAL の全額チェックポイントが可能 */
    rv = sqlite3_wal_checkpoint_v2(conn, NULL, SQLITE_CHECKPOINT_TRUNCATE, &wal_size, &ckpt);
    
    dqlite_assert(rv == SQLITE_OK);
    dqlite_assert(wal_size == 0);

    // ... (ロック解放など)
}

TLA+ モデルでの検証

TLA+ モデルでは、既存の仕様 (

INSTANCE

• DqliteCheckpointTakeLock: チェックポイント開始時に書き込みロックを取得。
• DqliteCheckPointCopyHeader: ロックが保持された状態でコピー処理を強制実行。
• 結果: 追記とチェックポイントの両方で書き込みロックを取得しているため、これらが同時に進行することができず、データ競合が発生しないことを確認しました。

結論: dqlite はこのバグの影響を全く受けないことが判明しました。

6. ボーナス：SQLite での修正内容

2026 年 3 月 5 日、SQLite はこのバグを公表し、修正版を発表しました。

修正の概要

チェックポイントを開始してから WAL のリセットが発生したかどうかを確認する追加チェックを追加することで、データ競合を回避します。

修正済みコード断片の解説

// read-lock slot 0 がロックされたので重要：ヘッダーが読み取られて以来、WAL がラップ（リセット）されていないことを確認
int bChg = memcmp(pLive->aSalt, pWal->hdr.aSalt, sizeof(pWal->hdr.aSalt));

if( 0==bChg ){
    // salt が変更されていない場合：通常通りチェックポイントを進行
    pInfo->nBackfillAttempted = mxSafeFrame; SEH_INJECT_FAULT;
} else {
    // salt が変更された場合（WAL リセットを検知）
    // 破損を回避するために、チェックポイントロジックを完全にスキップ
    return SQLITE_OK; 
}

修正を組み込んだ TLA+ モデル

Checkpoint

Checkpoint ≜
    ∧ checkPointState = "waitingForLock"
    
    \* salt が一致している場合：WAL リセットなしとみなす → チェックポイント進行
    IF walSalt = pWalSalt
       THEN
        ∧ db' = db ∪ { wal[j] : j ∈ nBackfill+1‥Len(wal) }
        ∧ nBackfill' = safeMxFrame
       \* salt が不一致する場合（WAL リセット検知）：チェックポイントをスキップ（破損回避）
    ELSE
        ∧ UNCHANGED ⟨ nBackfill, db ⟩
    
    \* 状態のリセット
    ∧ safeMxFrame' = 0
    ∧ pWalSalt' = 0
    ∧ checkPointState' = "notStarted"

モデルチェッカーへの入力を行ったところ、現在エラーが発生しないため、修正の有効性が確認できました。