加固 Turso：使用形式方法與 Quint 發現 SQLite 錯誤

對於任何構建資料庫的團隊而言，SQLite 代表了可靠性的黃金標準。由於 Turso 是 SQLite 的重寫版，維持相同的信任等級不僅是一個目標——更是必須。為了達成此目標，Turso 採用了嚴謹的測試堆疊，包括 Deterministic Simulation Testing (DST)、差分測試工具、模糊測試器以及併發模擬器。

儘管採取了如此全面的方法，團隊仍發現策略中存在一個缺口：形式方法。雖然傳統上被視為難以接近或過於複雜，形式方法卻能提供傳統測試無法達到的數學確定性。透過整合 Quint——一個現代的形式驗證工具，Turso 能夠進一步加強其硬化流程，最終在 SQLite 本身發現超過 10 個錯誤。

形式方法的挑戰

形式方法，例如 TLA+，是驗證系統正確性的業界基準。然而，它們常常面臨高門檻以及「誰在監督監督者」的問題——即驗證系統模型本身是否正確的困難。

為了克服這些挑戰，Turso 與社群成員 Pavan Nambi 合作，使用 Quint。Quint 將 Temporal Logic of Actions (TLA) 的理論基礎與現代型別檢查與開發工具結合，使其對工程師更易於使用。

團隊並未嘗試建模整個 SQLite 系統的艱鉅任務，而是聚焦於 C API。由於 C API 文件完善，且是大多數 SQLite 驅動程式的主要介面，對其建模提供了高效的覆蓋點。此方法讓團隊能以 API 規格作為真實來源，同時驗證模型與實際實作。

「Quinting」流程

找錯誤的方法論是一個重複的四步循環：

  1. Model the Contract：識別已文件化的 SQLite C API 合約，並在 Quint 中建模所需的狀態與屬性。
  2. Generate Traces：使用 Quint 產生一系列可能違反合約的狀態（軌跡）。
  3. Execute：將這些軌跡轉譯成小型 C 程式，並對 SQLite 執行。
  4. Compare：將系統觀測到的行為與文件化的結果進行比較。

當模型檢查器偵測到失敗時，會產生一個反例——一個導致違規的具體狀態序列。雖然許多反例僅驗證模型正確，其他則揭示系統偏離了自身的規格。

案例研究：sqlite3_deserialize()

一個顯著的例子涉及 sqlite3_deserialize() 函式，該函式允許將序列化的資料庫映像載入連線中，作為記憶體內資料庫。

根據規格，若目標資料庫目前正處於讀取交易或參與備份操作，sqlite3_deserialize() 應回傳 SQLITE_BUSY。Quint 模型產生了一條包含以下序列的軌跡：

  1. 開啟資料庫 → 建立表格 → 序列化資料庫。
  2. 開始從資料庫讀取。
  3. 在讀取交易仍然活躍時呼叫 sqlite3_deserialize()。

雖然預期會回傳 SQLITE_BUSY，實際結果卻是系統崩潰。由於崩潰幾乎從未是預期的行為，這立即確認了錯誤出現在實作而非模型中。此問題隨後在 SQLite 原始碼中得到修正。

結果與發現

使用 Quint 的探索相當高效，發現了各式各樣的錯誤，從最佳化的邏輯錯誤到關鍵性崩潰皆有涵蓋。主要發現包括：

  • Optimization Failures：EXISTS-to-join 最佳化錯誤地套用 LIMIT/OFFSET 或遺失外部關聯，導致有效列被過濾。
  • Constraint Violations：約束名稱被引用後變成無法刪除，或 xfer 最佳化繞過檢查約束，導致資料庫不一致的錯誤。
  • Stability Issues：在內部表格執行 ALTER ADD CHECK 或在 sqlite3changegroup_change_finish() 中因 NULL pzErr 而發生的崩潰。
  • Memory and Alignment：與 sqlite3_mutex 128 位元組對齊相關的未定義行為。

結論

SQLite 是現存最徹底測試的軟體之一。然而，透過 Quint 套用形式方法，Turso 能夠發現那些躲過數十年傳統測試的錯誤。

透過將形式軌跡轉譯為可執行的 C 程式，Turso 不僅加固了自身的實作，也對更廣大的 SQLite 生態系統的穩定性作出了重大貢獻。這顯示，當形式方法應用於特定且明確定義的介面（如 C API）時，便是一項提升現代軟體可靠性的強大工具。

Sources