智能合約的形式化驗證
智能合約使得建立去中心化、無須信任且穩健的應用程式成為可能，這些應用程式引入了新的使用案例並為使用者解鎖了價值。由於智能合約處理大量價值，安全性是開發人員的關鍵考量。
形式化驗證是提升智能合約安全性的推薦技術之一。形式化驗證使用形式化方法 (opens in a new tab)來規範、設計和驗證程式，多年來一直被用於確保關鍵硬體和軟體系統的正確性。
當應用於智能合約時，形式化驗證可以證明合約的業務邏輯符合預先定義的規範。與測試等其他評估合約程式碼正確性的方法相比，形式化驗證為智能合約的功能正確性提供了更強的保證。
什麼是形式化驗證？
形式化驗證是指根據形式化規範評估系統正確性的過程。簡單來說，形式化驗證允許我們檢查系統的行為是否滿足某些要求（即它是否執行了我們想要的操作）。
系統（在此情況下為智能合約）的預期行為使用形式化建模來描述，而規範語言則能夠建立形式化屬性。形式化驗證技術隨後可以驗證合約的實作是否符合其規範，並推導出前者正確性的數學證明。當合約滿足其規範時，它被描述為「功能正確」、「設計正確」或「建構正確」。
什麼是形式化模型？
在電腦科學中，形式化模型 (opens in a new tab)是計算過程的數學描述。程式被抽象為數學函數（方程式），模型描述了在給定輸入的情況下如何計算函數的輸出。
形式化模型提供了一定程度的抽象，可以在此基礎上評估對程式行為的分析。形式化模型的存在允許建立「形式化規範」，該規範描述了相關模型的預期屬性。
不同的技術被用於對智能合約進行建模以進行形式化驗證。例如，某些模型用於推論智能合約的高階行為。這些建模技術對智能合約應用黑箱視角，將它們視為接受輸入並根據這些輸入執行計算的系統。
高階模型側重於智能合約與外部代理之間的關係，例如外部擁有帳戶 (EOA)、合約帳戶和區塊鏈環境。此類模型有助於定義屬性，這些屬性規範了合約在回應某些使用者互動時應如何表現。
相反地，其他形式化模型則側重於智能合約的低階行為。雖然高階模型有助於推論合約的功能，但它們可能無法捕捉有關實作內部運作的細節。低階模型對程式分析應用白箱視角，並依賴智能合約應用程式的較低階表示（例如程式追蹤和控制流程圖 (opens in a new tab)）來推論與合約執行相關的屬性。
低階模型被認為是理想的，因為它們代表了智能合約在以太坊執行環境（即 EVM）中的實際執行。低階建模技術在建立智能合約中的關鍵安全屬性和偵測潛在漏洞方面特別有用。
什麼是形式化規範？
規範簡而言之就是特定系統必須滿足的技術要求。在程式設計中，規範代表了關於程式執行的一般概念（即程式應該做什麼）。
在智能合約的背景下，形式化規範是指「屬性」——對合約必須滿足的要求的形式化描述。此類屬性被描述為「不變數」，代表關於合約執行的邏輯斷言，這些斷言在任何可能的情況下都必須保持為真，沒有任何例外。
因此，我們可以將形式化規範視為以形式化語言編寫的陳述集合，這些陳述描述了智能合約的預期執行。規範涵蓋了合約的屬性，並定義了合約在不同情況下應如何表現。形式化驗證的目的是確定智能合約是否具備這些屬性（不變數），並且這些屬性在執行期間不會被違反。
形式化規範在開發安全的智能合約實作中至關重要。未能實作不變數或在執行期間違反其屬性的合約容易出現漏洞，這些漏洞可能會損害功能或導致惡意利用。
智能合約形式化規範的類型
形式化規範能夠對程式執行的正確性進行數學推論。與形式化模型一樣，形式化規範可以捕捉合約實作的高階屬性或低階行為。
形式化規範是使用程式邏輯 (opens in a new tab)的元素推導出來的，這允許對程式的屬性進行形式化推論。程式邏輯具有形式化規則，這些規則（以數學語言）表達了程式的預期行為。各種程式邏輯被用於建立形式化規範，包括可達性邏輯 (opens in a new tab)、時序邏輯 (opens in a new tab)和霍爾邏輯 (Hoare logic) (opens in a new tab)。
智能合約的形式化規範可以大致分為高階或低階規範。無論規範屬於哪個類別，它都必須充分且明確地描述所分析系統的屬性。
高階規範
顧名思義，高階規範（也稱為「導向模型的規範」）描述了程式的高階行為。高階規範將智能合約建模為有限狀態機 (opens in a new tab) (FSM)，它可以透過執行操作在狀態之間轉換，並使用時序邏輯來定義 FSM 模型的形式化屬性。
時序邏輯 (opens in a new tab)是「用於推論受時間限制的命題的規則（例如，『我_總是_很餓』或『我_最終_會餓』）」。當應用於形式化驗證時，時序邏輯用於陳述關於建模為狀態機的系統正確行為的斷言。具體來說，時序邏輯描述了智能合約未來可能處於的狀態以及它如何在狀態之間轉換。
高階規範通常捕捉智能合約的兩個關鍵時序屬性：安全性 (safety) 和 活躍性 (liveness)。安全性屬性代表「永遠不會發生壞事」的概念，通常表達不變性。安全性屬性可以定義一般的軟體要求，例如沒有死結 (opens in a new tab)，或者表達合約的特定領域屬性（例如，函數存取控制的不變數、狀態變數的容許值或代幣轉帳的條件）。
以這個涵蓋在 ERC-20 代幣合約中使用 transfer() 或 transferFrom() 條件的安全性要求為例：_「發送者的餘額永遠不會低於請求發送的代幣數量。」_這種對合約不變數的自然語言描述可以轉化為形式化（數學）規範，然後可以嚴格檢查其有效性。
活躍性屬性斷言「最終會發生好事」，並涉及合約在不同狀態之間進展的能力。活躍性屬性的一個例子是「流動性」，它指的是合約根據請求將其餘額轉帳給使用者的能力。如果違反了此屬性，使用者將無法提取儲存在合約中的資產，就像 Parity 錢包事件 (opens in a new tab)中發生的那樣。
低階規範
高階規範以合約的有限狀態模型為起點，並定義該模型的預期屬性。相比之下，低階規範（也稱為「導向屬性的規範」）通常將程式（智能合約）建模為包含數學函數集合的系統，並描述此類系統的正確行為。
簡單來說，低階規範分析_程式追蹤_，並嘗試在這些追蹤上定義智能合約的屬性。追蹤是指改變智能合約狀態的函數執行序列；因此，低階規範有助於規範合約內部執行的要求。
低階形式化規範可以作為霍爾風格 (Hoare-style) 屬性或執行路徑上的不變數給出。
霍爾風格屬性
霍爾邏輯 (opens in a new tab)提供了一組形式化規則，用於推論程式（包括智能合約）的正確性。霍爾風格屬性由霍爾三元組 {P}c{Q} 表示，其中 c 是一個程式，而 P 和 Q 是關於 c（即程式）狀態的謂詞，分別被形式化地描述為_前置條件_和_後置條件_。
前置條件是描述正確執行函數所需條件的謂詞；呼叫合約的使用者必須滿足此要求。後置條件是描述函數如果正確執行所建立條件的謂詞；使用者可以預期在呼叫函數後此條件為真。霍爾邏輯中的_不變數_是透過執行函數而保留（即不改變）的謂詞。
霍爾風格規範可以保證_部分正確性_或_完全正確性_。如果前置條件在函數執行前為真，並且如果執行終止，後置條件也為真，則合約函數的實作是「部分正確的」。如果在函數執行前前置條件為真，保證執行會終止，並且當它終止時，後置條件為真，則獲得完全正確性的證明。
獲得完全正確性的證明很困難，因為某些執行可能會在終止前延遲，或者根本不終止。話雖如此，執行是否終止的問題可以說是一個沒有意義的問題，因為以太坊的燃料機制可以防止無限的程式迴圈（執行要麼成功終止，要麼因為「燃料耗盡」錯誤而結束）。
使用霍爾邏輯建立的智能合約規範將為合約中函數和迴圈的執行定義前置條件、後置條件和不變數。前置條件通常包括函數輸入錯誤的可能性，而後置條件描述對此類輸入的預期回應（例如，拋出特定例外）。透過這種方式，霍爾風格屬性可有效確保合約實作的正確性。
許多形式化驗證框架使用霍爾風格規範來證明函數的語意正確性。也可以透過在 Solidity 中使用 require 和 assert 陳述式，將霍爾風格屬性（作為斷言）直接新增到合約程式碼中。
require 陳述式表達前置條件或不變數，通常用於驗證使用者輸入，而 assert 捕捉安全性所需的後置條件。例如，函數的適當存取控制（安全性屬性的一個例子）可以使用 require 作為對呼叫帳戶身分的前置條件檢查來實現。同樣地，合約中狀態變數容許值的不變數（例如，流通中的代幣總數）可以透過使用 assert 在函數執行後確認合約的狀態來防止被違反。
追蹤層級屬性
基於追蹤的規範描述了使合約在不同狀態之間轉換的操作以及這些操作之間的關係。如前所述，追蹤是以特定方式改變合約狀態的操作序列。
這種方法依賴於將智能合約建模為狀態轉換系統，該系統具有一些預先定義的狀態（由狀態變數描述）以及一組預先定義的轉換（由合約函數描述）。此外，控制流程圖 (opens in a new tab) (CFG) 是程式執行流程的圖形表示，通常用於描述合約的操作語意。在這裡，每個追蹤都表示為控制流程圖上的一條路徑。
主要來說，追蹤層級規範用於推論智能合約中內部執行的模式。透過建立追蹤層級規範，我們斷言智能合約的容許執行路徑（即狀態轉換）。使用符號執行等技術，我們可以形式化驗證執行永遠不會遵循形式化模型中未定義的路徑。
讓我們使用一個具有一些可公開存取函數的 DAO 合約範例來描述追蹤層級屬性。在這裡，我們假設 DAO 合約允許使用者執行以下操作：
-
存入資金
-
存入資金後對提案進行投票
-
如果他們不對提案進行投票，則申領退款
追蹤層級屬性的範例可以是_「未存入資金的使用者無法對提案進行投票」或「未對提案進行投票的使用者應始終能夠申領退款」。這兩個屬性都斷言了首選的執行順序（投票不能發生在存入資金_之前，申領退款不能發生在對提案進行投票_之後_）。
智能合約形式化驗證的技術
模型檢查
模型檢查是一種形式化驗證技術，其中演算法根據其規範檢查智能合約的形式化模型。在模型檢查中，智能合約通常表示為狀態轉換系統，而容許合約狀態的屬性則使用時序邏輯來定義。
模型檢查需要建立系統（即合約）的抽象數學表示，並使用植根於命題邏輯 (opens in a new tab)的公式來表達該系統的屬性。這簡化了模型檢查演算法的任務，即證明數學模型滿足給定的邏輯公式。
形式化驗證中的模型檢查主要用於評估描述合約隨時間推移行為的時序屬性。智能合約的時序屬性包括_安全性_和_活躍性_，我們在前面已經解釋過。
例如，與存取控制相關的安全屬性（例如，只有合約的擁有者可以呼叫 selfdestruct）可以用形式邏輯編寫。此後，模型檢查演算法可以驗證合約是否滿足此形式化規範。
模型檢查使用狀態空間探索，這涉及建構智能合約的所有可能狀態，並嘗試尋找導致違反屬性的可達狀態。然而，這可能導致無限數量的狀態（稱為「狀態爆炸問題」），因此模型檢查器依賴抽象技術來實現對智能合約的有效分析。
定理證明
定理證明是一種對程式（包括智能合約）正確性進行數學推論的方法。它涉及將合約系統的模型及其規範轉換為數學公式（邏輯陳述）。
定理證明的目標是驗證這些陳述之間的邏輯等價性。「邏輯等價性」（也稱為「邏輯雙向蘊涵」）是兩個陳述之間的一種關係，使得第一個陳述為真_若且唯若_第二個陳述為真。
關於合約模型及其屬性的陳述之間所需的關係（邏輯等價性）被表述為可證明的陳述（稱為定理）。使用形式化推論系統，自動化定理證明者可以驗證定理的有效性。換句話說，定理證明者可以確鑿地證明智能合約的模型精確地符合其規範。
雖然模型檢查將合約建模為具有有限狀態的轉換系統，但定理證明可以處理無限狀態系統的分析。然而，這意味著自動化定理證明者無法總是知道邏輯問題是否「可判定」。
因此，通常需要人工協助來引導定理證明者推導出正確性證明。在定理證明中使用人力使其比完全自動化的模型檢查使用起來更昂貴。
符號執行
符號執行是一種透過使用_符號值_（例如 x > 5）而不是_具體值_（例如 x == 5）執行函數來分析智能合約的方法。作為一種形式化驗證技術，符號執行用於形式化推論合約程式碼中的追蹤層級屬性。
符號執行將執行追蹤表示為符號輸入值的數學公式，也稱為_路徑謂詞_。SMT 求解器 (opens in a new tab)用於檢查路徑謂詞是否「可滿足」（即存在可以滿足公式的值）。如果易受攻擊的路徑是可滿足的，SMT 求解器將產生一個具體值，該值會觸發並引導執行朝向該路徑。
假設智能合約的函數接受一個 uint 值 (x) 作為輸入，並在 x 大於 5 且小於 10 時還原 (revert)。使用一般測試程序尋找觸發錯誤的 x 值將需要執行數十個（或更多）測試案例，且無法保證實際找到觸發錯誤的輸入。
相反地，符號執行工具將使用符號值執行函數：X > 5 ∧ X < 10（即 x 大於 5 且 x 小於 10）。然後將相關的路徑謂詞 x = X > 5 ∧ X < 10 交給 SMT 求解器進行求解。如果特定值滿足公式 x = X > 5 ∧ X < 10，SMT 求解器將計算它——例如，求解器可能會產生 7 作為 x 的值。
因為符號執行依賴於程式的輸入，而探索所有可達狀態的輸入集合可能是無限的，所以它仍然是一種測試形式。然而，如範例所示，在尋找觸發違反屬性的輸入方面，符號執行比一般測試更有效率。
此外，與隨機產生函數輸入的其他基於屬性的技術（例如模糊測試）相比，符號執行產生的誤報更少。如果在符號執行期間觸發了錯誤狀態，則可以產生觸發錯誤的具體值並重現該問題。
符號執行也可以提供某種程度的正確性數學證明。考慮以下具有溢位保護的合約函數範例：
function safe_add(uint x, uint y) returns(uint z){
z = x + y;
require(z>=x);
require(z>=y);
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) 中的程式碼通常是不可變的。由於發布後的升級不容易進行，保證合約可靠性的需求使得形式化驗證成為必要。形式化驗證能夠偵測棘手的問題，例如整數下溢和溢位、重入攻擊以及不良的燃料最佳化，這些問題可能會逃過稽核員和測試人員的眼睛。
證明功能正確性
程式測試是證明智能合約滿足某些要求的最常見方法。這涉及使用預期處理的資料樣本執行合約並分析其行為。如果合約對樣本資料傳回預期結果，則開發人員就有了其正確性的客觀證明。
然而，這種方法無法證明不屬於樣本的輸入值的正確執行。因此，測試合約可能有助於偵測錯誤（即，如果某些程式碼路徑在執行期間未能傳回預期結果），但它無法確鑿地證明沒有錯誤。
相反地，形式化驗證可以形式化地證明智能合約滿足無限範圍執行的要求，而_完全不需要_執行合約。這需要建立精確描述正確合約行為的形式化規範，並開發合約系統的形式化（數學）模型。然後我們可以遵循形式化證明程序來檢查合約模型與其規範之間的一致性。
透過形式化驗證，驗證合約的業務邏輯是否滿足要求的問題是一個可以被證明或反證的數學命題。透過形式化證明一個命題，我們可以用有限的步驟驗證無限數量的測試案例。透過這種方式，形式化驗證在證明合約相對於規範在功能上是正確的方面具有更好的前景。
理想的驗證目標
驗證目標描述了要進行形式化驗證的系統。形式化驗證最適合用於「嵌入式系統」（構成較大系統一部分的小型、簡單的軟體）。它們也是規則較少的專門領域的理想選擇，因為這使得修改用於驗證特定領域屬性的工具變得更加容易。
智能合約——至少在某種程度上——滿足了這兩個要求。例如，以太坊合約的體積小，使其易於進行形式化驗證。同樣地，EVM 遵循簡單的規則，這使得規範和驗證在 EVM 中執行的程式的語意屬性變得更加容易。
更快的開發週期
形式化驗證技術（例如模型檢查和符號執行）通常比對智能合約程式碼的常規分析（在測試或稽核期間執行）更有效率。這是因為形式化驗證依賴符號值來測試斷言（「如果使用者嘗試提取 n 個以太幣會怎樣？」），這與使用具體值的測試（「如果使用者嘗試提取 5 個以太幣會怎樣？」）不同。
符號輸入變數可以涵蓋多種類別的具體值，因此形式化驗證方法有望在更短的時間內提供更多的程式碼覆蓋率。如果有效使用，形式化驗證可以加速開發人員的開發週期。
形式化驗證還透過減少代價高昂的設計錯誤，改善了建置去中心化應用程式 (dapp) 的過程。升級合約（在可能的情況下）以修復漏洞需要大量重寫程式碼庫，並在開發上花費更多精力。形式化驗證可以偵測合約實作中許多可能逃過測試人員和稽核員眼睛的錯誤，並提供充足的機會在部署合約之前修復這些問題。
形式化驗證的缺點
人工成本
形式化驗證，特別是由人類引導證明者推導正確性證明的半自動化驗證，需要大量的人工勞動。此外，建立形式化規範是一項複雜的活動，需要高水準的技能。
與測試和稽核等評估合約正確性的常用方法相比，這些因素（精力和技能）使得形式化驗證要求更高且更昂貴。儘管如此，考慮到智能合約實作中錯誤的代價，支付全面驗證稽核的成本是切合實際的。
偽陰性 (False negatives)
形式化驗證只能檢查智能合約的執行是否符合形式化規範。因此，確保規範正確描述智能合約的預期行為非常重要。
如果規範寫得很差，形式化驗證稽核就無法偵測到違反屬性的情況（這指向易受攻擊的執行）。在這種情況下，開發人員可能會錯誤地認為合約沒有錯誤。
效能問題
形式化驗證會遇到許多效能問題。例如，在模型檢查和符號檢查期間分別遇到的狀態和路徑爆炸問題可能會影響驗證程序。此外，形式化驗證工具通常在其底層使用 SMT 求解器和其他約束求解器，而這些求解器依賴於計算密集型程序。
此外，程式驗證器並不總是能夠確定屬性（描述為邏輯公式）是否可以被滿足（「可判定性問題 (opens in a new tab)」），因為程式可能永遠不會終止。因此，即使合約規範良好，也可能無法證明其某些屬性。
以太坊智能合約的形式化驗證工具
用於建立形式化規範的規範語言
Act：Act 允許規範儲存更新、前置/後置條件和合約不變數。其工具套件還具有證明後端，能夠透過 Coq、SMT 求解器或 hevm 證明許多屬性。
Scribble - Scribble 將 Scribble 規範語言中的程式碼註解轉換為檢查規範的具體斷言。
Dafny - Dafny 是一種支援驗證的程式語言，它依賴高階註解來推論和證明程式碼的正確性。
用於檢查正確性的程式驗證器
Certora Prover - Certora Prover 是一種自動形式化驗證工具，用於檢查智能合約中的程式碼正確性。規範以 CVL (Certora Verification Language) 編寫，並結合靜態分析和約束求解來偵測屬性違規。
Solidity SMTChecker - Solidity 的 SMTChecker 是一個基於 SMT（可滿足性模理論）和 Horn 求解的內建模型檢查器。它在編譯期間確認合約的原始碼是否符合規範，並靜態檢查是否違反安全性屬性。
solc-verify - solc-verify 是 Solidity 編譯器的擴充版本，可以使用註解和模組化程式驗證對 Solidity 程式碼執行自動化形式化驗證。
KEVM - KEVM 是以 K 框架編寫的以太坊虛擬機 (EVM) 的形式化語意。KEVM 是可執行的，並且可以使用可達性邏輯證明某些與屬性相關的斷言。
用於定理證明的邏輯框架
Isabelle - Isabelle/HOL 是一個證明助手，允許以形式化語言表達數學公式，並提供證明這些公式的工具。主要應用是數學證明的形式化，特別是形式化驗證，其中包括證明電腦硬體或軟體的正確性，以及證明電腦語言和協定的屬性。
Rocq - Rocq 是一個互動式定理證明者，讓您可以使用定理定義程式，並互動式地產生機器檢查的正確性證明。
基於符號執行的工具，用於偵測智能合約中的易受攻擊模式
曼蒂科爾 - 一個基於符號執行的 EVM 位元組碼分析工具。
hevm - hevm 是 EVM 位元組碼的符號執行引擎和等價性檢查器。
Mythril - 一個用於偵測以太坊智能合約漏洞的符號執行工具