智能合約是一項重要的技術，它使得創建去中心化、無需信任且穩健的應用成爲可能，爲用戶帶來了新的用例併釋放了價值。由於智能合約處理大量價值，安全性對開髮人員來説至關重要。因此，形式化驗證成爲提高智能合約安全性的一種推薦技術。
形式化驗證採用正式方法來指定、設計和驗證程序，多年來一直用於確保關鍵硬件和軟件繫統的正確性。當應用於智能合約時，形式化驗證可以證明合衕的業務邏輯符合預定義的規範。與其他用於評估合衕代碼正確性的方法（如測試）相比，形式化驗證提供更強的保證，確保智能合約在功能上是正確的。
在接下來的章節中，我們將詳細介紹形式化驗證的各個方麵，包括如何建立正式模型、定義正式規範以及使用模型檢查、定理證明和符號執行等技術來驗證智能合約的正確性。通過深入了解這些技術，讀者將能夠更好地理解如何應用形式化驗證來提高智能合約的安全性。
什麽是形式化驗證？
形式化驗證是指根據形式化規範評估繫統正確性的過程。簡單來説，形式化驗證使我們能夠檢查繫統的行爲是否滿足某些要求（即它做我們想要的事）。
繫統的預期行爲（在本例中爲智能合約）使用形式化建模來描述，而規範語言則支持創建形式化屬性。然後，形式化驗證技術可以驗證合約的實現是否符合其規範，併推導出前者正確性的數學證明。當合約滿足其規範時，它被描述爲“功能上正確”、“設計上正確”或“構建上正確”。
什麽是正式模型？
在計算機科學中，正式模型（在新標簽頁中打開）是對計算過程的數學描述。程序被抽象爲數學函數（方程），模型描述了給定輸入時如何計算函數的輸出。
正式模型提供了一個分析程序行爲的抽象層次。正式模型的存在允許創建正式規範，它描述了所討論模型的期望屬性。
用於正式驗證智能合約的不衕技術手段。例如，一些模型用於推理智能合約的高層行爲。這些建模技術將智能合約視爲黑盒繫統，接受輸入併基於這些輸入執行計算。
高層模型關註智能合約與外部代理的關繫，如外部擁有的賬戶（EOA）、合約賬戶和區塊鏈環境。這些模型有助於定義指定合約在特定用戶交互下應有行爲的屬性。
相反，其他正式模型專註於智能合約的低層行爲。盡管高層模型有助於推理合約的功能，但它們可能無法捕捉到實現的內部工作細節。低層模型將程序分析應用白盒視角，併依賴於智能合約應用的低層錶示，如程序軌跡和控製流圖（在新標簽頁中打開），來推理與合約執行相關的屬性。
低層模型被認爲是理想的，因爲它們代錶了智能合約在以太坊執行環境（即EVM）中的實際執行。低層建模技術在確立智能合約的關鍵安全屬性和檢測潛在漏洞方麵特別有用。
什麽是正式規範？
規範簡單來説就是一個特定繫統必鬚滿足的技術要求。在編程中，規範代錶了對程序執行的一般概念（即程序應該做什麽）。
在智能合約的背景下，正式規範指的是屬性——對合約必鬚滿足的要求的正式描述。這些屬性被描述爲“不變量”，代錶了關於合約執行的邏輯斷言，在任何可能的情況下都必鬚保持真實，沒有任何例外。
因此，我們可以將正式規範視爲用正式語言編寫的陳述集合，這些陳述描述了智能合約的預期執行方式。規範涵蓋了合約的屬性，併定義了合約在不衕情況下應如何錶現。正式驗證的目的是確定一個智能合約是否具有這些屬性（不變量），以及在執行過程中這些屬性是否沒有被違反。
在開髮安全的智能合約實現方麵，正式規範至關重要。未能實現不變量或在執行過程中違反其屬性的合約容易出現漏洞，這可能損害功能或導緻惡意利用。
智能合約的正式規範類型
智能合約的形式化規範類型
形式化規範使得可以用數學的方式推理程序執行的正確性。與形式化模型一樣，形式化規範可以捕捉合約實現的高級屬性或低級行爲。
形式化規範是使用程序邏輯的元素推導出來的，這允許對程序的屬性進行形式化推理。程序邏輯有形式化的規則，用數學語言錶達程序預期的行爲。在創建形式化規範時使用了各種程序邏輯，包括可達性邏輯、時態邏輯和霍爾邏輯。
智能合約的形式化規範可以大緻分類爲高級規範和低級規範。無論規範屬於哪個類別，它都必鬚充分且明確地描述所分析繫統的屬性。
高級規範
正如其名稱所示，高級規範（也稱爲“模型導曏規範”）描述了程序的高級行爲。高級規範將智能合約建模爲有限狀態機
（FSM），通過執行操作在狀態之間轉換，使用時序邏輯來定義FSM模型的形式屬性。
是“關於時間方麵的命題推理規則（例如，“我總是餓的”或“我最終會餓”）。”在形式驗證中應用時，時序邏輯用於陳述關於以狀態機爲模型的繫統正確行爲的斷言。具體來説，時序邏輯描述了智能合約可以處於的未來狀態以及它如何在狀態之間轉換。
高級規範通常捕捉智能合約的兩個關鍵時序屬性：安全性和活性。安全性屬性代錶“永遠不會髮生壞事”的理念，通常錶示爲不變性。安全性屬性可能定義一般軟件要求，例如無死鎖
，或錶達合約的特定領域屬性（例如，函數訪問控製的不變性、狀態變量的可接受值，或代幣轉移的條件）。
例如，這個涉及ERC-20代幣合約中使用transfer()或transferFrom()的安全要求：“髮送者的餘額永遠不會低於要髮送的代幣數量。”這種自然語言描述的合約不變量可以轉換爲形式化（數學）規範，然後可以嚴格檢查其有效性。
活性屬性主張“最終會髮生某些好事”，併涉及合約通過不衕狀態的進展能力。活性屬性的一個例子是“流動性”，指的是合約按要求曏用戶轉移餘額的能力。如果違反了這個屬性，用戶將無法提取存儲在合約中的資産，就像髮生在Parity錢包事件中的那樣
（在新標簽頁中打開）。
低級規範
高級規範以有限狀態模型的合約爲起點，定義了這個模型的期望屬性。相比之下，低級規範（也稱爲“屬性導曏規範”）通常將程序（智能合約）建模爲包含一繫列數學函數的繫統，併描述這些繫統的正確行爲。
簡單來説，低級規範分析程序跟蹤，併試圖定義智能合約在這些跟蹤上的屬性。跟蹤指的是改變智能合約狀態的一繫列函數執行序列；因此，低級規範有助於指定合約內部執行的要求。
低級形式規範可以以霍爾屬性或執行路徑上的不變量來給出。
霍爾式屬性
霍爾邏輯（Hoare Logic）爲推理程序正確性（包括智能合約）提供了一套正式規則。霍爾式屬性用霍爾三元組 {P}c{Q} 錶示，其中 c 是一個程序，P 和 Q 是關於 c（即程序）狀態的謂詞，正式描述爲前置條件和後置條件。
前置條件是描述函數正確執行所需條件的謂詞；調用合約的用戶必鬚滿足這一要求。後置條件是描述如果函數正確執行後所建立的條件的謂詞；用戶可以期望在調用該函數後這一條件爲真。霍爾邏輯中的不變量是指在函數執行中保持不變的謂詞（即它不會改變）。
霍爾規範可以保證部分正確性或完全正確性。如果在執行函數之前前置條件成立，併且如果執行終止，後置條件也爲真，則合約函數的實現被認爲是“部分正確”的。如果在函數執行之前前置條件爲真，且執行保證終止，當其終止時，後置條件爲真，則可以證明完全正確性。
穫得完全正確性的證明是睏難的，因爲某些執行可能在終止之前延遲，或根本不會終止。盡管如此，執行是否終止的問題可以説是無關緊要的，因爲以太坊的 gas 機製防止了無限程序循環（執行要麽成功終止，要麽因“gas不足”錯誤而結束）。
使用霍爾邏輯創建的智能合約規範將爲合約中的函數和循環的執行定義前置條件、後置條件和不變量。前置條件通常包括對函數的錯誤輸入的可能性，後置條件描述對這些輸入的預期響應（例如，拋出特定異常）。通過這種方式，霍爾屬性對於確保合約實現的正確性是有效的。
許多形式驗證框架使用霍爾式屬性來證明函數的語義正確性。也可以通過在 Solidity 中使用 require 和 assert 語句，將霍爾屬性（作爲斷言）直接添加到合約代碼中。
require 語句錶達前置條件或不變量，通常用於驗證用戶輸入，而 assert 捕捉對安全性必要的後置條件。例如，通過使用 require 作爲對調用賬戶身份的前置條件檢查，可以實現函數的適當訪問控製（一個安全屬性的例子）。類似地，可以通過使用 assert 來確認函數執行後合約的狀態，以保護合約中狀態變量的允許值不受侵犯（例如，流通中的代幣總數）。
追蹤級屬性
基於追蹤的規範描述了使合約在不衕狀態之間轉換的操作及這些操作之間的關繫。如前所述，追蹤是一繫列改變合約狀態的操作序列。
這種方法依賴於將智能合約視爲帶有一些預定義狀態（由狀態變量描述）的狀態轉換繫統，以及一組預定義轉換（由合約函數描述）。此外，控製流程圖（CFG），即程序執行流的圖形錶示，通常用於描述合約的操作語義。在這裡，每個追蹤都錶示爲控製流圖上的一條路徑。
主要地，追蹤級規範用於推理智能合約內部執行的模式。通過創建追蹤級規範，我們斷言智能合約的允許執行路徑（即，狀態轉換）。使用諸如符號執行之類的技術，我們可以正式驗證執行永遠不會遵循未在正式模型中定義的路徑。
讓我們用一個DAO合約的例子來描述追蹤級屬性。這裡，我們假設DAO合約允許用戶執行以下操作：
存款
存款後對提案進行投票
如果他們不對提案進行投票，則可要求退款
追蹤級屬性的示例可以是“未存款的用戶不能對提案進行投票”或“未對提案進行投票的用戶應始終能夠要求退款”。這兩個屬性都斷言了首選的執行序列（投票不能在存款之前髮生，要求退款不能在對提案進行投票之後髮生）。
智能合約的形式驗證技術
模型檢查
模型檢查是一種形式化驗證技術，其中算法會檢查智能合約的形式化模型是否符合其規範。在模型檢查中，智能合約通常被錶示爲狀態轉換繫統，而允許的合約狀態屬性則使用時序邏輯來定義。
模型檢查需要創建一個繫統（即合約）的抽象數學錶示，併使用基於命題邏輯的公式來錶達此繫統的屬性。這簡化了模型檢查算法的任務，即證明數學模型滿足給定的邏輯公式。
在形式化驗證中，模型檢查主要用於評估描述合約隨時間行爲的時序屬性。智能合約的時序屬性包括安全性和活性，我們之前已經解釋過了。
例如，與訪問控製相關的安全屬性（例如，隻有合約的所有者才能調用 selfdestruct）可以用形式邏輯來編寫。之後，模型檢查算法可以驗證合約是否滿足這個形式規範。
模型檢查使用狀態空間探索，包括構建智能合約的所有可能狀態，併嘗試找到導緻屬性違規的可達狀態。然而，這可能導緻無限數量的狀態（稱爲“狀態爆炸問題”），因此模型檢查器依賴於抽象技術，以使對智能合約的有效分析成爲可能。
定理證明
定理證明是一種用於數學上推理程序正確性的方法，包括智能合約。它涉及將合約繫統的模型及其規格轉換成數學公式（邏輯語句）。
定理證明的目的是驗證這些語句之間的邏輯等價性。所謂的“邏輯等價性”（也稱爲“邏輯雙條件”）是指兩個語句之間的一種關繫，使得第一個語句真實僅當且僅當第二個語句真實。
關於合約模型及其屬性的所需關繫（邏輯等價性）被形式化爲一個可證明的語句（稱爲定理）。通過使用一個正式的推理繫統，自動定理證明器可以驗證定理的有效性。換句話説，定理證明器可以確鑿地證明智能合約的模型與其規格完全匹配。
盡管模型檢查將合約建模爲具有有限狀態的轉換繫統，但定理證明可以處理無限狀態繫統的分析。然而，這意味著自動定理證明器併不總是知道邏輯問題是否“可判定”。
因此，通常需要人爲協助來引導定理證明器推導出正確性證明。定理證明中使用人力使其比全自動的模型檢查更昂貴。
符號執行
符號執行是一種通過使用符號值（例如，x > 5）而不是具體值（例如，x == 5）執行函數來分析智能合約的方法。作爲一種形式驗證技術，符號執行用於形式化地推理合約代碼中的跟蹤級屬性。
符號執行將執行跟蹤錶示爲對符號輸入值的數學公式，也稱爲路徑謂詞。SMT解算器用於檢查路徑謂詞是否“可滿足”（即存在可以滿足公式的值）。如果一個脆弱路徑是可滿足的，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 的值。
因爲符號執行依賴於程序的輸入，而探索所有可達狀態的輸入集可能是無限的，它仍然是一種測試形式。然而，正如示例所示，符號執行比常規測試更有效地找到觸髮屬性違規的輸入。
此外，與其他基於屬性的技術（例如，隨機生成函數輸入的模糊測試）相比，符號執行産生的誤報更少。如果在符號執行期間觸髮了錯誤狀態，那麽可以生成一個觸髮錯誤的具體值併重現問題。
符號執行還可以提供某種程度的正確性數學證明。考慮以下具有溢出保護的合約函數示例：
導緻整數溢出的執行跟蹤需要滿足以下公式：z = x + y 且 (z >= x) 且 (z>=y) 且 (z < x 或 z < y) 這樣的公式不太可能被解出，因此它作爲 safe_add 函數永不溢出的數學證明。
爲什麽對智能合約使用形式化驗證？
對於可靠性的需求
形式化驗證用於評估安全關鍵繫統的正確性，這些繫統的失敗可能會導緻災難性後果，如死亡、受傷或財務崩潰。智能合約是控製巨大價值的高價值應用程序，設計中的簡單錯誤可能會給用戶造成不可輓回的損失。
然而，在部署之前對合約進行形式化驗證，可以增加它在區塊鏈上運行時錶現如預期的保證。
可靠性是任何智能合約中非常渴望的質量，特別是因爲在以太坊虛擬機（EVM）中的代碼通常是不可變的。由於髮布後升級不易實現，因此保證合衕可靠性的需要使得形式驗證成爲必要。形式驗證能夠檢測棘手的問題，例如整數下溢和溢出、可重入以及較差的 Gas 優化，這些問題可能會被審計員和測試人員忽略。
證明功能正確性
程序測試是證明智能合約滿足某些要求的最常見方法。這涉及使用預期處理的數據樣本執行合約併分析其行爲。如果合約返回樣本數據的預期結果，那麽開髮人員就可以客觀地證明其正確性。
但是，此方法無法證明對於不屬於樣本的輸入值的正確執行。因此，測試合約可能有助於檢測錯誤（即，如果某些代碼路徑在執行過程中未能返回所需的結果），但它不能最終證明不存在錯誤。
相反，形式驗證可以正式證明智能合約滿足無限範圍的執行要求，而無需運行合約。這需要創建一個精確描述正確合約行爲的正式規範，併開髮合約繫統的正式（數學）模型。然後我們可以遵循正式的證明程序來檢查合衕模型與其規範之間的一緻性。
通過形式化驗證，驗證合約的業務邏輯是否滿足要求的問題是一個可以證明或反駁的數學命題。通過形式化地證明一個命題，我們可以用有限的步驟驗證無限數量的測試用例。通過這種方式，形式驗證更有可能證明合衕在功能上相對於規範是正確的。
理想的驗證目標
驗證目標描述了要形式化驗證的繫統。形式驗證最適合用於“嵌入式繫統”（構成較大繫統一部分的小型、簡單的軟件）。它們也非常適合規則很少的專門領域，因爲這使得修改用於驗證特定領域屬性的工具變得更加容易。
智能合約——至少在某種程度上——滿足了這兩個要求。例如，以太坊合約的小規模使其易於接受形式驗證。衕樣，EVM 遵循簡單的規則，這使得指定和驗證 EVM 中運行的程序的語義屬性變得更加容易。
更快的開髮周期
形式驗證技術，例如模型檢查和符號執行，通常比智能合約代碼的常規分析（在測試或審計期間執行）更有效。這是因爲形式驗證依賴於符號值來測試斷言（“如果用戶嘗試提取 n 以太怎麽辦？”），這與使用具體值的測試（“如果用戶嘗試提取 5 以太怎麽辦？”）不衕。
符號輸入變量可以覆蓋多個類別的具體值，因此形式驗證方法可以在更短的時間內覆蓋更多的代碼。如果有效使用，形式驗證可以加快開髮人員的開髮周期。
形式驗證還可以通過減少代價高昂的設計錯誤來改進構建去中心化應用程序（dapp）的過程。升級合約（如果可能）以修覆漏洞需要大量重寫代碼庫併在開髮上投入更多精力。形式驗證可以檢測合衕實施中的許多錯誤，這些錯誤可能會被測試人員和審計人員忽略，併提供充足的機會在部署合衕之前解決這些問題。
形式驗證的缺點
體力勞動成本
形式驗證，尤其是由人類引導證明者得出正確性證明的半自動驗證，需要大量的體力勞動。此外，創建正式規範是一項覆雜的活動，需要高水平的技能。
與評估合衕正確性的常用方法（例如測試和審計）相比，這些因素（努力和技能）使得形式驗證要求更高、成本更高。盡管如此，考慮到智能合約實施中錯誤的成本，支付全麵驗證審計的費用是可行的。
漏報
形式化驗證隻能檢查智能合約的執行是否符合形式化規範。因此，確保規範正確描述智能合約的預期行爲非常重要。
如果規範寫得不好，那麽正式的驗證審計就無法檢測到違反屬性的行爲（這錶明執行過程中存在漏洞）。在這種情況下，開髮人員可能會錯誤地認爲合約沒有錯誤。
性能問題
形式驗證會遇到許多性能問題。例如，在模型檢查和符號檢查期間分別遇到的狀態和路徑爆炸問題可能會影響驗證過程。此外，形式驗證工具通常在其底層使用 SMT 求解器和其他約束求解器，併且這些求解器依賴於計算密集型過程。
此外，程序驗證者併不總是能夠確定某個屬性（描述爲邏輯公式）是否可以滿足（“可判定性問題”）因爲程序可能永遠不會終止。因此，即使合約明確指定，也可能無法證明合約的某些屬性。
以太坊智能合約的形式化驗證工具
用於創建正式規範的規範語言
行爲:法案允許指定存儲更新、前置/後置條件和契約不變量。其工具套件還具有證明後端，能夠通過 Coq、SMT 求解器或 hevm 證明許多屬性。
Scribble 將 Scribble 規範語言中的代碼註釋轉換爲檢查規範的具體斷言。
Dafny 是一種可驗證的編程語言，它依靠高級註釋來推理和證明代碼的正確性。
用於檢查正確性的程序驗證器
Certora Prover 是一種自動形式驗證工具，用於檢查智能合約中代碼的正確性。規範以 CVL（Certora 驗證語言）編寫，併結合靜態分析和約束求解來檢測屬性違規。
Solidity SMTChecker-Solidity 的 SMTChecker 是基於 SMT（可滿足性模理論）和 Horn 求解的內置模型檢查器。它確認合約的源代碼在編譯期間是否符合規範，併靜態檢查是否違反安全屬性。
solc-verify 是 Solidity 編譯器的擴展版本，可以使用註釋和模塊化程序驗證對 Solidity 代碼進行自動化形式驗證。
KEVM 是用 K 框架編寫的以太坊虛擬機（EVM）的形式語義。 KEVM 是可執行的，可以使用可達性邏輯證明某些與屬性相關的斷言。
定理證明的邏輯框架
Isabelle/HOL 是一個證明助手，允許用形式語言錶達數學公式，併提供證明這些公式的工具。主要應用是數學證明的形式化，特別是形式驗證，包括證明計算機硬件或軟件的正確性以及證明計算機語言和協議的屬性。
Coq 是一個交互式定理證明器，可讓您使用定理定義程序併交互式生成機器檢查的正確性證明。
用於檢測智能合約中易受攻擊模式的基於符號執行的工具
Manticore - 一款基於符號執行的EVM字節碼分析工具。
hevm - hevm 是 EVM 字節碼的符號執行引擎和等價檢查器。
Consensys/mythril-用於檢測以太坊智能合約漏洞的符號執行工具
聲明：
- 本文轉載自[ethereum]，著作權歸屬原作者[@ abooo96]，如對轉載有異議，請聯繫Gate Learn團隊，團隊會根據相關流程盡速處理。
- 免責聲明：本文所錶達的觀點和意見僅代錶作者個人觀點，不構成任何投資建議。
- 文章其他語言版本由Gate Learn團隊翻譯， 在未提及Gate.io的情況下不得覆製、傳播或抄襲經翻譯文章。
相关文章
如何質押 ETH？
