從最初的 “The DAO” 智能合約開始，重入漏洞就一直困擾着各種區塊鏈上的智能合約，隨後，又發生了一系列備受矚目的漏洞，智能合約中數億甚至數十億美元的資金被盜。
這些漏洞很難通過測試發現，因爲它們只在智能合約代碼的不同部分按特定順序執行時纔會出現，此類順序的數量非常龐大，因此簡單的測試無法實現。
在之前的博客文章中，我們展示瞭如何使用 TLA+（一個能夠全面測試軟件設計的通用工具包）進行形式化驗證，有效地消除互聯網計算機上智能合約（或稱“容器”）中的重入漏洞。
這些博客文章如下：
使用 TLA+ 消除智能合約錯誤：介紹 TLA+，使用 ckBTC 案例研究來說明模型檢查如何查找並幫助修復可重入錯誤。
使用 TLA+ 模型清除錯誤：瞭解 DFINITY 的開源 TLA+ 模型（NNS、ckBTC 等）以及面向開發人員的真實示例。
教程 - 使用 TLA+ 製作互聯網計算機容器：有關如何使用 TLA+ 和 PlusCal 建模互聯網計算機容器並檢查其屬性的分步技術指南。
雖然我們發現 TLA+ 在消除重入錯誤方面非常有效，但它的使用存在一個侷限性：TLA+ 模型對應於某個時間點的代碼快照，但隨着代碼的演進，這些模型可能會過時，甚至可能無人察覺，重入錯誤可能會再次出現在代碼庫中。
在本文中，我們提出了一種解決這個問題的方法：一個自動化框架，用於測試 Rust 容器與其 TLA+ 規範之間的一致性。
TLA+ 和同步挑戰
在 TLA+ 方法中，我們不是直接測試代碼，而是構建代碼的簡化模型，然後，我們指示 TLA+ 工具（即 TLC 模型檢查器）系統地檢查模型中所有可能的執行序列（直至達到一定範圍），並確保無論序列如何，某些提供的屬性都成立。
例如，在神經網絡（NNS）治理模型中，我們可以檢查神經元的投票權是否正確基於其質押的 ICP，然後，TLC 可以發現任何可重入漏洞，這些漏洞的執行序列可能允許攻擊者獲得更多投票權，或者實際上告訴我們不存在此類漏洞。
這種方法的一大優勢是 TLA+ 模型比代碼更簡單，無需人工輸入即可有效分析模型，正因如此，一些科技巨頭，例如微軟和 AWS，也使用 TLA+ 來驗證其關鍵基礎設施。
然而，驗證保證僅適用於模型，而不適用於代碼本身，雖然可以有效地手動檢查模型與代碼的一致性，但隨着代碼的演變，這項工作變得繁瑣乏味，每次代碼更改都可能需要檢查模型是否仍然能夠正確捕獲代碼。
因此，模型和代碼往往會隨着時間的推移而失去同步，這意味着在創建和檢查模型時提供的強一致性保證最終會消失。
這正是我們在最近的一個功能中解決的問題，我們開發了一個框架，用於自動測試 Rust 容器代碼與其 TLA+ 模型之間的對應關係，並將其應用於我們的治理容器，現在，我們的 CI（持續集成）流水線會持續測試治理代碼是否與模型存在偏差。
這讓我們和更廣泛的 ICP 社區能夠安心，因爲 NNS 是安全的，並且能夠抵禦任何試圖通過重入漏洞實現 NNS 接管的攻擊者，此外，該框架並非特定於治理：它可以應用於其他互聯網計算機容器，包括社區容器。
工作原理
TLA+ 模型將系統描述爲過渡系統，在此類系統中，所謂的過渡謂詞描述了系統如何將其狀態從一個狀態轉換爲另一個狀態，當謂詞對兩個狀態 s1 和 s2 爲“真”時，系統可以從狀態 s1 轉換爲 s2，如果謂詞對 s2 和某些 s3 也爲“真”，則系統可以從 s1 轉換爲 s2，再轉換爲 s3，依此類推。
給定過渡謂詞和另一個指定哪些狀態是有效起始狀態的“初始”謂詞，模型檢查器可以構建所有有效的狀態序列（也稱爲軌跡），此外，用戶可以指定一個謂詞來定義“好”狀態和“壞”狀態，然後模型檢查器可以在通過某些有效的狀態序列達到壞狀態時發出警報。
這和我們的容器有什麼關係？容器在處理消息時會改變狀態，這些消息可以是用戶消息、來自其他容器的消息，也可以是系統生成的“心跳”或“計時器”消息，消息由所謂的消息處理器處理。
由於 ICP 保證消息處理器的執行是原子的，我們可以在 TLA+ 中對容器進行建模，方法是將轉換謂詞定義爲“相關容器的某個消息處理器已執行”，並在 TLA+ 謂詞中定義我們認爲每個消息處理器執行的操作。
那麼問題是：我們是否在 TLA+ 中正確捕獲了消息處理程序實際執行的操作？
爲了解答這個問題，我們構建了一個工具，可以複用現有的容器測試，從此類測試執行中收集狀態對，每個收集到的狀態對描述了容器在每個消息處理程序開始和結束時的狀態，或者至少描述了與 TLA+ 模型相關的狀態部分（具體哪些相關由用戶決定）。
現在，我們可以調用 TLA+ 模型的轉換謂詞，並詢問：我們觀察到的狀態對是否真的滿足謂詞？如果不滿足，那麼我們就知道代碼做了一些 TLA+ 模型未考慮到的事情，併發出警報（導致 CI 失敗）。
如上所述，隨着代碼的不斷髮展，這一點尤爲重要：現在，導致 TLA+ 模型與代碼不兼容的意外更改有機會被自動檢測到。
工作量有多大？
該工具需要三個主要步驟：
構建 TLA+ 模型本身。
對 Rust 容器代碼進行插樁，以檢測每個消息處理程序的開始和結束，並描述如何將容器狀態映射到 TLA+ 值，插樁可以分爲兩種類型：散佈在整個生產代碼中的插樁，以及保存在單獨模塊中的插樁，我們專注於精簡第一種類型的插樁，例如，對於治理而言，添加到生產代碼中的代碼不超過 100 行，雖然我們沒有專注於保持第二種類型的插樁精簡，但此類代碼仍然不超過 1000 行。
對測試進行插樁，以調用檢查記錄狀態是否滿足轉換謂詞的函數，對於僅使用 Rust 的測試（即沒有構建實際的 Wasm 容器並將其上傳到副本），每個測試只需一行代碼即可完成此操作，對於基於 Wasm 的測試，需要進行一些額外的工作來通過查詢來公開和獲取記錄狀態，但每個測試也只需一行代碼。
有關如何設置工具的更詳細的技術說明可在 IC GitHub 存儲庫中找到。
結論
此工具專注於提供一種廉價而有效的方法，用於檢查模型與 Rust 容器代碼之間的對應關係，然而，它只能根據您已編寫的測試中觀察到的情況來檢測偏差，它無法檢測僅在未經測試的場景下才會發生的偏差。
因此，通過這種方式獲得的保證，相比其他一些驗證方法（尤其是代碼級驗證）獲得的非常強的保證，要弱得多。
然而，與編寫 TLA+ 模型、自動進行模型檢查以及使用提供的工具對代碼進行插樁相比，代碼級驗證也更加費力，我們相信，這種方法在所需的工作量和所提供的收益之間找到了一個最佳平衡點。
此外，它與測試具有協同作用：測試覆蓋率越高，您就越能確信您的代碼與 TLA+ 模型同步，從而避免出現重入錯誤。
如果您已經開始爲自己的容器編寫 TLA+ 模型，則可以從IC 存儲庫中獲取將模型鏈接到代碼的工具（包括文檔）。
否則，如果您剛剛開始爲自己的容器使用 TLA+，這裏有一些有用的資源：
我們的博客文章介紹了 TLA+ 如何以及爲何有助於防止重入漏洞；
使用 TLA+ 建模互聯網計算機容器的技術教程或視頻（第 1 部分、第 2 部分）；
免費提供的 TLA+ 資源：(學習 TLA+)一書、(指定系統)一書、TLA+ 視頻課程；
Internet Computer 關於 TLA+ 的文檔頁面。
你關心的 IC 內容
技術進展 | 項目信息 | 全球活動
收藏關注 IC 幣安頻道
掌握最新資訊