智慧型合約的形式化驗證
最後編輯: @bskrksyp9(opens in a new tab), 2024年7月26日
智慧型合約讓建立去中心化、去信任且穩健的應用程式，來引進新的應用案例並解放使用者的價值變得更加可行。 因為智慧型合約掌握了大量的價值，所以對開發者來說，安全是最關鍵的考量。
形式化驗證是增進智慧型合約安全的其中一種推薦方法。 形式化驗證是一種使用多年的方法，採用形式化方法(opens in a new tab)來規範、設計和驗證程式，目的是要確保關鍵硬體與軟體系統的正確性。
當在智慧型合約中實作形式化驗證時，可以證明合約的商業邏輯符合預先定義的規範。 相較於其他評估合約程式碼正確性的方法，形式化驗證更能保證智慧型合約功能性上的正確。
什麼是形式化驗證？
形式化驗證指的是一個用形式化規範評估系統正確性的過程。 簡而言之，形式化驗證讓我們可以檢查一個系統的行為是否滿足一些要求（即，它會按我們的想法運作）。
採用形式化模型對系統（此案例中為智慧型合約）的預期行為進行描述，同時藉由規範語言支援形式化屬性的建立。 然後，形式化驗證技術可以驗證一個合約的實作是否符合其規範，並導出合約正確性的數學證明。 當一個合約滿足其規範，則被稱為「功能正確」、「設計正確」，或「建構正確」。
形式化模型是什麼？
在電腦科學中，形式化模型(opens in a new tab)是指對計算過程的數學描述。 程式被抽象成數學函式（方程），模型則描述了給定輸入時如何計算函式的輸出。
形式化模型提供了一個抽象層次，可以在該抽象層次上對程式行為的分析進行評估。 有了形式化模型，形式化規範得以建立，用來描述所涉模型所需要的屬性。
採用不同的技術來建立智慧型合約模型，以便進行形式化驗證。 例如，有些模型用來推理智慧型合約的高階行為。 這些模型建立技術對智慧型合約套用黑盒檢視，把智慧型合約視為可以接受輸入並按照那些輸入執行計算的系統。
高階模型專注在智慧型合約與外部代理，例如外部帳戶 (EOA)、合約帳戶和區塊鏈環境，之間的關係。 這些模型有助於定義屬性，規定合約該如何回應某些使用者互動的行為。
相反地，其他形式化模型專注於智慧型合約的低階行為。 雖然高階模型有助於推理合約的功能，它們可能無法擷取實作內部運作的細節。 低階模型對程式分析應用白盒檢視，並仰賴智慧型合約應用程式的較低階表示，例如程式追蹤和控制流圖(opens in a new tab)，來推理與合約執行相關的屬性。
低階模型被認爲是理想的，因爲它們代表了智慧型合約在以太坊執行環境（即以太坊虛擬機）中的實際執行。 低階模型建立技術對於在智慧型合約中建立關鍵的安全屬性和偵測潛在漏洞尤其有用。
什麽是形式化規範？
規範不過是特定系統必須滿足的技術要求。 在編程中，規範代表程式執行的總體思路（即程式應該做什麽）。
在智慧型合約的背景下，形式化規範指的是屬性—合約必須滿足的要求的形式化描述。 這樣的屬性被描述爲「不變量」，並代表了關於合約執行的邏輯斷言，該斷言在任何情況下都必須為 true，沒有例外。
因此，我們可以將形式化規範想做是用形式化語言編寫的陳述式集合，描述了智慧型合約的預期執行。 規範涵蓋了合約的屬性，並定義了合約在各種情況下應該如何運作。 形式化驗證的目的是確定智慧型合約是否具備這些屬性（不變量）以及在執行過程中不會違反這些屬性。
形式化規範對於開發智慧型合約的安全實作至關重要。 無法實作不變量或在執行期間違反其屬性的合約容易出現漏洞，可能會損害合約功能或導致合約遭到惡意利用。
智慧型合約形式化規範的類型
形式化規範使程式執行的正確性可以用數學方法進行推理。 與形式化模型一樣，形式化規範可以擷取合約實作的高階屬性或低階行爲。
形式化規範是由程式邏輯(opens in a new tab)的元素推導出，透過這些元素可以對程式的屬性做形式化推理。 程式邏輯採用形式化規則來（用數學語言）表達程序的預期行為。 形式化規範可以使用各種程式邏輯來建立，包括可達性邏輯(opens in a new tab)、時間邏輯(opens in a new tab)以及霍爾邏輯(opens in a new tab)。
智慧型合約的形式規範大致上可分成高階或低階規範。 無論規範屬於什麽類別，都必須充分且明確地描述所分析之系統的屬性。
高階規範
顧名思義，高階規範（也被稱爲「模型導向規範」）描述程式的高階行爲。 高階規範將智慧型合約建模為有限狀態機器(opens in a new tab) (FSM)，它能夠透過執行操作來轉換狀態，並使用時間邏輯來為有限狀態機器模型定義形式化屬性。
時間邏輯(opens in a new tab)是「時間限定命題的推理規則（例如，「我 總是很餓」，或「我最終會餓」）」。 當應用於形式化驗證時，時間邏輯被用來聲明關於建模為狀態機器的正確系統行為的斷言。 具體來說，時間邏輯描述智慧型合約可以進入的未來狀態，以及它如何在狀態之間轉換。
高階規範通常擷取智慧型合約的兩個關鍵時間屬性：安全和活躍性。 安全屬性代表「任何壞事都不會發生」的想法，且通常表達不變量。 安全屬性可以定義一般軟體要求，例如免於死鎖(opens in a new tab)或表達合約的領域特有屬性（如函式存取控制的不變量、狀態變數的容許值或代幣轉賬的條件）。
以下方安全要求為例，其描述了在 ERC-20 代幣合約中使用 transfer() 或 transferFrom() 的條件：「發送者的餘額決不可少於要求發送的代幣金額」。 這種合約不變量的自然語言描述可以轉化為形式化（數學）規範，以進行嚴格的有效性檢查。
活躍性屬性斷言「好事終將發生」，並涉及合約逐步通過不同狀態的能力。 活躍性屬性的一個例子是「流動性」，代表一個合約在收到要求時將其餘額轉帳給使用者的能力。 如果違反該屬性，使用者就無法提取存儲在合約中的資產，就像 Parity 錢包事件(opens in a new tab)中發生的那樣。
低階規範
高階規範以合約的有限狀態模型作為起點，並定義該模型所需的屬性。 相較之下，低階規範（也稱為「屬性導向規範」）通常將程式（智慧型合約）建模成由數學函式集合組成的系統，並描述這類系統的正確行為。
簡單來説，低階規範分析程式追蹤並試圖透過這些追蹤定義智慧型合約的屬性。 追蹤是指改變智慧型合約狀態的函式執行序列；因此，低階規範幫助指定合約内部執行的要求。
低階形式化規範可以出具為霍爾式屬性或執行路徑中的不變量。
霍爾式屬性
霍爾邏輯(opens in a new tab)提供了一套形式化規則，用於推理包括智慧型合約等程式的正確性。 霍爾式屬性使用霍爾三元組 {P}c{Q} 表示，其中 c 是一個程式，P 和 Q 為c（即程式）的狀態述詞，正式描述分別為前置條件和後置條件。
前置條件是描述正確執行函式所需條件的述詞；叫用合約的使用者必須滿足該要求。 後置條件是描述函式正確執行時所建立之條件的述詞；使用者在叫用函式後可以預計該條件為 true。 在霍爾邏輯中，不變量是指透過執行函式保留的述詞（即，它不會改變）。
霍爾式規範可以保證部分正確性或完全正確性。 如果前置條件在函式執行之前為 true，並且如果執行終止，後置條件也爲 true，則合約函式的實作為「部分正確」。 如果前置條件在函式執行之前為 true，執行被保證終止且實際終止時，後置條件為 true，則會獲得完全正確性證明。
獲得完全正確性證明很難，因為一些執行在終止前可能會延遲，或根本不會終止。 也就是説，由於以太坊的燃料機制會防止無限程式迴圈（執行要麼成功終止，要麼因為「燃料耗盡」錯誤而終止），執行是否會終止可以説是一個有爭議的問題。
使用霍爾邏輯建立的智慧型合約規範會具有前置條件、後置條件以及為執行合約中的函式和迴圈而定義的不變量。 前置條件通常包括函式輸入錯誤的可能性，後置條件則描述對此類輸入的預期回應（例如，抛出一個特定例外狀況）。 用這種方式，霍爾式屬性可以很有效地確保合約實作的正確性。
許多形式化驗證框架使用霍爾式規範來證明函式的語義正確性。 也可以透過使用 Solidity 中的 require 和 assert 陳述式，直接向合約程式碼新增霍爾式屬性（做為斷言）。
require 陳述式表達前置條件或不變量，並且通常用於驗證使用者輸入，而 assert 則會擷取一個安全必要的後置條件。 例如，可以使用 require 做為前置條件檢查呼叫帳戶的身分，來實現正確的函式存取控制（安全屬性的一個範例）。 相似地，透過在函式執行后使用 assert 確認合約的狀態，可以防止違反合約中狀態變數許可值的不變量（例如，流通中的代幣總數）。
追蹤層級屬性
基於追蹤的規範描述了在不同狀態之間轉換合約的操作以及這些操作之間的關係。 如前所述，追蹤是以特定方式改變合約狀態的操作序列。
該方法依賴於智慧型合約模型做為狀態轉換系統，該系統具有一些預定義屬性（由狀態變數描述）以及一組預定義轉換（由合約函式描述）。 此外，控制流程圖(opens in a new tab) (CFG)，即程式執行流程的圖形化表示，常常用於描述合約的操作語義。 在這裡，每個追蹤代表控制流程圖上的一條路徑。
追蹤層級規範主要用來推理智慧型合約中的內部執行模式。 透過建立追蹤層級規範，我們斷言一個智慧型合約的容許執行路徑（即，狀態轉換）。 使用類似於符號執行的技術，我們可以從形式上驗證執行永遠不會追隨未在形式化模型中定義的路徑。
我們使用一個已具有一些公開可存取函式的去中心化自治組織 (DAO) 合約做為範例，介紹追蹤層級屬性。 在這裡，我們假設去中心化自治組織 (DAO) 合約允許使用者執行以下操作：
存入資金
存入資金後對提案進行投票
在沒有對提案投票的情況下申請退款
追蹤層級屬性的範例可以是「沒有存入資金的使用者無法對提案進行投票」或「沒有對提案進行投票的使用者應該一律能夠申請退款」。 這兩個屬性斷言均優先執行順序（存入資金之前不能進行投票，以及對提案進行投票之後不能申請退款）。
智慧型合約的形式化驗證技術
模型檢查
模型檢查是一種形式化驗證技術，使用演算法對照規範檢查智慧型合約的形式化模型。 在模型檢查中，智慧型合約通常表示爲狀態轉換系統，同時使用時間邏輯來定義許可合約狀態屬性。
模型檢查需要建立系統的抽象數學表示（即合約），並使用根植於命題邏輯(opens in a new tab)的公式來表示該系統的屬性。 這樣簡化了模型檢查演算法的工作，也就是說證明數學模型符合給定的邏輯公式。
形式化驗證裡的模型檢查主要用來評價時間屬性，該屬性描述了合約行為與時間的關係。 智慧型合約的時間屬性包括我們之前說明的安全和活躍性。
例如，與存取控制相關的安全屬性（例如，只有合約的擁有者能夠呼叫 selfdestruct ）可以使用形式化邏輯來編寫。 之後，模型檢查演算法可以驗證合約是否符合此形式化規範。
模型檢查使用狀態空間探索，其中涉及構造智慧型合約的所有可能狀態，並試圖找出導致違反屬性的可達狀態。 然而，這可能會導致無限的狀態數量（稱爲「狀態爆炸問題」），因此，模型檢查器需仰賴抽象技術來實現高效分析智慧型合約。
定理證明
定理證明是以數學方式推論程式（包括智慧型合約）之正確性的方法。 這需要將合約系統的模型和規範轉換成數學公式（邏輯陳述式）。
定理證明的目的是驗證這些陳述式之間的邏輯等價性。 「邏輯等價性」（也被稱爲「邏輯雙向蘊含」）是兩個陳述式之間的一種關係，例如，第一個陳述式當且僅當第二個陳述式為 true 時才為 true。
關於合約模型及其屬性的陳述式之間的這種必要關係（邏輯等價性），被公式化為可證明的陳述式（又稱定理）。 使用形式化推理系統，自動定理證明器可以驗證定理的有效性。 換言之，自動定理證明器可以結論性地證明智慧型合約模型確切符合其規範。
模型檢查將合約建模為具有有限狀態的轉換系統，而定理證明可以處理無限狀態系統的分析。 不過，這意味著自動定理證明器無法永遠知道邏輯問題是否為「可判定」。
因此，在推導正確性證明時，定理證明器常常需要人類協助給予指導。 定理證明中對人力的使用使其比完全自動化的模型檢查更加昂貴。
符號執行
符號執行是一種透過使用符號值（如 x > 5）而不是具體值（如 x == 5）執行函式來分析智慧型合約的方法。 作爲一種形式化驗證技術，符號執行用於對智慧型合約程式碼中的追蹤層級屬性進行形式化推理。
符號執行將執行追蹤表示爲針對符號輸入值的數學公式，也稱爲路徑斷言。 SMT 求解器(opens in a new tab)用於檢查路徑述詞是否爲「可滿足」（即存在能夠滿足該公式的值）。 假如某脆弱路徑是可滿足的，SMT 求解器會產生一個具體值來觸發針對該路徑的引導執行。
假設一個智慧型合約函式接受輸入的 uint 值 (x)，並在 x 大於 5 且小於 10 時回退呼叫。 使用正常測試程序尋找觸發錯誤的 x 值需要運行數十個測試用例（甚至更多），並且不保證真正找到觸發錯誤的輸入。
相反，符號執行工具會使用符號值來執行函式：X > 5 ∧ X < 10（即，x 大於 5 且 x 小於 10）。 之後，相關的路徑述詞 x = X > 5 ∧ X < 10 會提供給 SMT 求解器進行求解。 如果一個特定值滿足公式 x = X > 5 ∧ X < 10，SMT 求解器將會計算它 - 例如，求解器可能會產生 7 作爲 x 的值。
因爲符號執行仰賴程式的輸入，而探索所有可達狀態的一系列輸入可能是無限的，所以這仍然是一種測試形式。 不過，如範例所示，符號執行在尋找觸發違反屬性的輸入方面比常規測試更有效率。
此外，符號執行與其他隨機產生函式輸入的基於屬性的技術（如模糊測試）相比，產生的誤報更少。 如果錯誤狀態在符號執行期間被觸發，則可以產生觸發該錯誤的具體值並重現該問題。
符號執行也可以提供某程度的數學正確性證明。 仔細思考下面具溢位保護的合約函式範例：
1function safe_add(uint x, uint y) returns(uint z){23 z = x + y;4 require(z>=x);5 require(z>=y);67 return z;
導致整數溢位的執行追蹤需要滿足以下公式：z = x + y AND (z >= x) AND (z=>y) AND (z < x OR z < y)。這種公式不太可能有解，因此它提供了函式 safe_add 永不溢出的數學證明。
為什麼要對智慧型合約使用形式化驗證？
可靠性的需求
形式化驗證被用於評估安全關鍵系統的正確性，這些系統的失敗會產生災難性後果，例如死亡、受傷或金融崩潰。 智慧型合約是控制巨額價值的高價值應用程式，設計中的簡單錯誤可能會導致使用者遭受無法挽回的損失(opens in a new tab)。 然而，在合約部署之前進行形式化驗證，則可以增加其在區塊鏈上如期運行的保證。
可靠性是任何智慧型合約都渴求的一種品質，尤其是因爲在以太坊虛擬機 (EVM) 上部署的程式碼通常是不可變的。 合約推出後的升級並不是輕易能夠達成的，形式化驗證成為確保合約可靠性的需求下不可缺少的必需品。 形式化驗證能夠檢測棘手的問題，比如整數下溢和上溢、可重入性和糟糕的燃料最佳化，審核者和測試者可能會漏掉這些問題。
証明功能正確性
程式測試是證明智慧型合約符合某些要求的最常見方法。 這包括用預期合約會處理到的樣本資料來執行合約，並且分析合約的行為。 假如對樣本資料合約傳回預期的結果，則開發者對合約的正確性做了客觀性的證明。
然而，這種方法無法證明樣本資料之外的輸入值也能正確執行。 因此，測試合約可以幫助檢測漏洞（例如，如果程式碼路徑在執行期間未能返回期望的結果），但它無法結論性地證明沒有漏洞。
相反，形式化驗證可以從形式上證明智慧型合約能在無限執行範圍内滿足要求，而無需運行該合約。 這需要建立一個形式化規範來準確描述正確的合約行爲，並開發合約系統的形式化（數學）模型。 之後我們可以透過形式化證明程序來檢查合約模型與其規範之間的一致性。
透過形式化驗證，驗證合約商業邏輯是否滿足要求的問題就成爲一個能夠被證明或反駁的數學命題。 透過命題的形式化證明，我們可以在有限的步驟內驗證無限數量的測試用例。 這種方式的形式化驗證在證明合約相較於規範的功能正確性方面具有更好的前景。
理想的驗證目標
驗證目標是指要進行形式化驗證的系統。 形式化驗證最適合用於「嵌入式系統」（作為更大系統一部分的小型、簡單軟體元件）。 也非常適合具有較少規則的專業化領域，因為這樣更容易修改工具來驗證特定領域的屬性。
智慧型合約至少在某種程度上滿足這兩個要求。 例如，以太坊合約的規模較小，這使它們適合進行形式化驗證。 此外，以太坊虛擬機遵循簡單的規則，這使得為以太坊虛擬機中所運行的程式驗證語義屬性變得更加容易。
更短的開發周期
形式化驗證技術，例如模型檢查和符號執行，通常比常規的智慧型合約程式碼分析更有效率（在測試和審核期間的表現）。 這是因為形式化驗證仰賴符號值來測試斷言（「如果使用者嘗試提取 n 個以太幣會怎樣？」）， 而目前常用的測試則使用具體值（「如果使用者嘗試提取 5 個以太幣會怎樣？」）。
符號輸入變數可以涵蓋多個類別的具體值，因此形式化驗證能夠確保在更短時間内覆蓋更多程式碼。 在有效率的使用下，形式化驗證可以加速開發者的開發流程。
此外，形式化驗證透過減少代價高昂的設計錯誤，也改進了去中心化應用程式 (dapps) 的建置過程。 升級合約（如果可能）來修復漏洞，需要大量重寫程式碼基底並投入更多努力在開發上。 形式化驗證可以偵測合約實現中可能會被測試者和審核者漏掉的許多錯誤，並提供充足的機會在合約部署之前修復這些問題。
形式化驗證的缺點
人力成本
形式化驗證，尤其是需要人爲引導證明器來推導出正確性證明的半自動驗證，需要花費大量人力。 而且，建立形式化規範是一項複雜的過程，要求很高的技能水平。
這些因素（人力與技能）使形式化驗證相比評估合約正確性的常規方法（例如測試和審核），要求更高且更加昂貴。 然而，鑑於智慧型合約實作中的錯誤代價，完整驗證審核的成本仍然是可以接受的。
漏報
形式化驗證只能檢查智慧型合約的執行是否與形式化規範相符， 因此，確保規範正確描述智慧型合約的預期行為非常重要。
如果規範編寫得很糟糕，就無法透過形式化驗證審核來偵測違反屬性的情況（這會導致執行漏洞）。 這種情況下，開發者可能會錯誤地假設合約沒有漏洞。
效能問題
形式化驗證會遇到一些效能問題。 例如，在模型檢查和符號檢查期間分別遇到狀態和路徑爆炸問題，就可能會影響驗證程序。 另外，形式化驗證經常在其底層使用 SMT 求解器和其他約束求解器，而這些求解器仰賴計算密集型流程。
此外，程式驗證器并不總是能夠確認屬性（由邏輯公式描述）是否可以被滿足（「可判定性問題(opens in a new tab)」），因爲程式可能永遠不會終止。 因此，即使規範良好，有些合約屬性也可能無法被證明。
以太坊智慧型合約的形式化驗證工具
用於建立形式化規範的規範語言
Act - _*Act 允許指定存儲更新、前置/後置條件以及合約不變量。</0> 其工具套件還具有證明後端，可透過 Coq、SMT 求解器或 hevm 來證明許多屬性。**
Scribble - _*Scribble 將以 Scribble 規範語言編寫的程式碼注解轉換爲用於檢查規範的具體斷言。**
Dafny — _*Dafny 是一種驗證就緒的程式設計語言，仰賴高階註釋來推理和證明程式碼的正確性。**
用於檢查正確性的程式驗證器
Certora Prover - Certora Prover 是一種自動形式化驗證工具，用於檢查智慧型合約程式碼的正確性。 規範採用 CVL（Certora 驗證語言）編寫，結合使用靜態分析和約束求解來偵測屬性違反。
Solidity SMTChecker - _* Solidity 的 SMTChecker 是一個基於 SMT（可滿足性模數理論）和 Horn 求解的内置模型檢查器。 它在編譯期間確認合約的源程式碼是否符合規範，並以靜態方式檢查安全屬性的違反情況。**
solc-verify - _*solc-verify 是 Solidity 編譯器的一個延伸版本，可以使用注解和模組化程式驗證在 Solidity 程式碼上執行自動形式化驗證。**
KEVM - _*KEVM 是用 K 框架編寫的以太坊虛擬機 (EVM) 的形式化語義。 KEVM 是可執行的，並且可以用可達性邏輯來證明某些與屬性相關的斷言。**
定理證明的邏輯框架
Isabelle - Isabelle/HOL 是一個證明助手，允許使用形式化語言來表示數學公式，並提供驗證明這些公式的工具。 主要應用於數學證明的形式化，特別是形式化驗證，它涉及證明電腦硬體或軟體的正確性以及證明電腦語言和協定的屬性。
Coq - Coq 是一個互動式定理證明器，允許你使用定理來定義程式並以互動方式產生經機器檢查的正確性證明。
用於偵測智慧型合約中易受攻擊模式的基於符號執行的工具
Manticore – _一種基於符號執行的以太坊虛擬機位元組碼分析工具。*
hevm - _*hevm 是用於以太坊虛擬機位元組碼的符號執行引擎和等價性檢查器。**
Mythril - 用於檢測以太坊智慧型合約漏洞的符號執行工具