無bug編程是一項艱巨的任務，也是關鍵系統面臨的基本挑戰。為此，形式化方法提供了開發程序和驗證程序正確性的技術。

正式核查是一項艱苦的工作。它要求很高，需要大量的腦力，需要大量的投資，但它已經成為軟件行業許多領域的強制性標準。

從區塊鏈的早期開始，這種科學似乎就違背了開發人員采用這種技術的必要性，但同時也降低了這種必要性。最流行的智能合約語言的成功難道不歸功于它類似javascript的語言嗎？

但是，采用這種方式是一把雙刃劍：與以前的任何其他網絡相比，經濟上都會直接受到威脅。

既然新的共識方法和區塊鏈協議的安全性得到了越來越多的科學文獻的支持，現在是時候重新引入正式的方法，讓智能合與開發人員受益了。經過幾十年的研究，這門科學是建立分散式應用信心的必要紐帶。

本文旨在介紹正式的驗證，回顧區塊鏈時代的現有工具，并強調以太坊特有的挑戰。

正式驗證的簡短介紹

智能合約是一種自我執行的工具，它的增長是隨著區塊鏈的興起而出現的。隨著這項技術的采用，這些金融工具的實際存款額不斷增加，同時它們的復雜性也嚴重升級。這種情況會周期性地導致代價高昂的bug和漏洞，從而為更嚴格的程序分析方法帶來光明。

在這方面，在永久部署分散式的應用程序之前，測試和審計通常為開發人員和用戶提供一定的保證。但是，由于沒有代碼檢查可以100%保證消除所有bug，所以正式的驗證可以通過數學方法帶來更高的可信度。這就是為什么這一領域受到以太坊基金會的積極支持，并可能迅速得到更廣泛的應用。

在進一步討論之前，應該簡要介紹一些數學概念。

正確性： 如果一個程序執行分配給它的任務沒有錯誤，并且在所有可能的情況下都是正確的，那么這個程序就是正確的。

規范： 程序的規范是對分配給它的任務和允許用例的明確描述。指定一個程序需要抽象它的屬性，因此是一項困難的任務。根據規范驗證程序實現的正確性也很困難。

動態分析包括執行代碼或模擬代碼，以發現任何bug。創建測試計劃包括列出要測試的用例，并為每個用例建立一個測試。由于這些測試不能全面，動態分析一般不能構成正確性的證明。

另一方面，靜態分析包括遍歷代碼而不執行代碼，以證明某些屬性。存在不同的方法，例如基于模型檢查或Hoare邏輯。形式驗證依賴于靜態分析。

Hoare邏輯有助于證明，從驗證某些屬性的初始狀態（前置條件）開始，通過執行一系列指令，我們可以獲得驗證其他屬性的狀態（后置條件）。如果總是這樣，這就叫做完全正確。

如果有一個帶有Hoare三元組（前置條件-指令-后置條件）的自然演繹，那么程序相對于其前置條件和后置條件是正確的。

像Coq這樣的證明助手幫助交互式地構建這樣的演繹樹。

總結一下，要理解正式驗證智能合約的挑戰，必須牢記兩個基本概念：

1. 我們不能證明合約是明智的。我們證明了它們的一些性質。我們根據規范證明了它們的正確性。

2. 要被認為是有效的，必須在一個單一的、可信的邏輯框架內生成一個證明，從規范語言級別到虛擬機執行級別。

在構建區塊鏈時考慮到驗證

2016 年初，一組研究人員分析了部署在以太坊主網上的字節碼，以查找常見的安全缺陷。他們驚人的評估被大量引用：在19366份研究合約中，8833份至少存在一次安全漏洞。在本文提倡改進以太坊的操作語義以幫助形式化驗證的同時，出現了一個問題：一些區塊鏈框架是否比其他框架更不容易進行形式化驗證？

很難否認，每個區塊鏈都是為了滿足特定的期望子集而設計的，比如快速采用或安全性。

直接的結果是，正式的驗證在一些框架上是當前的現實，而在另一些框架上可能是長期的目標。

在這方面，2018年發表的一份有趣的研究報告概述了合同語言和驗證方法，作為對當前解決方案的全面調查。它有助于確定以下區分因素，并概述當前主要框架上正式方法的可用性。

合約語言

在軟件行業，特別是在區塊鏈領域，區分三種類型的語言是很有幫助的：

· 高級語言，如以太坊上的solability或Vyper， Tezos上的Liquidity，都旨在易于學習，并幫助大型開發人員社區編寫智能契約。

· 底層基于堆棧的語言，如比特幣腳本，代表了實際機器之前的最后一個抽象步驟

· 中間表示，如Tezos上的Michelson或Ziliqa上的Scilla，是對合約驗證和代碼優化最合適的支持。

圖1：不同級別的智能合約語言和編譯過程。（A）與更直接的（B）相比，便于驗證和代碼優化。

只有一種低級語言，比特幣腳本在于第一個區塊鏈上編寫智能合約。當圖靈完備的區塊鏈框架出現時，就需要更富表現力的高級合約語言。

它們中的一些本質上允許直接編譯字節碼，如（B） path（圖1）所示。例如，在以太坊上，solid作為一種智能合約語言被廣泛采用，開發人員的代碼可以直接編譯為EVM字節碼。

還設計了其他高級語言，以便可以首先將合約代碼編譯為中級表示，然后再編譯為低級語言，如（a） path（圖1）所示。

由于促進了中間代碼的正式驗證，不同的區塊鏈框架在驗證智能合約方面的能力出現了重大差異。

驗證方法

根據前面對語言的分類，我們可以區分出三種主要的驗證方法：

（I）：規范可以直接在字節碼級別進行評估。由于合約源不一定可用，因此提供了一種方法來評估已經部署的合約上的一些屬性。

（II）：中間表示形式可專門設計為驗證工具（例如證明助手）的目標。這可以根據規范為代碼優化和動態驗證提供非常合適的環境。中間代碼表示形式可以來自高級合約的編譯，也可以來自低級代碼的反編譯。

（III）：一些工具也直接針對高級語言進行推理。這種方法在驗證時為開發人員提供了寶貴的直接反饋。

圖2：基于與規范化比較對象的不同驗證方法。

正式的語義

當新的編程語言出現時，它們的語義可能被正式地描述出來。程序的確切行為由正式語義定義，而對于具有非正式語義的語言，則需要更靈活性的編譯器。

在大多數情況下，定義在任何級別上使用的所有語言的正式語義都是至關重要的，因為它為開發單個可信邏輯框架提供了條件，在這個框架中，從一種形式主義到另一種形式的轉換都要經過正式建模和驗證。

所有翻譯的正確性決定了一個人對整個框架的信心程度。如果對程序的中間表示形式執行形式化驗證，則反向翻譯將允許以更高級別的原始語言顯示有意義的消息。此外，如果轉換成機器字節碼不安全，那么沒有人可以正式信任它的執行，無論在其他級別的驗證工作如何。

例如，與Tezos和Cardano相反，EVM的正式語義只被描述在帖子前。并且，由于 Solidity 編譯器變化迅速，在缺少允許逐構造自動生成驗證工具的正式語義的情況下，后者也需要遵循變化的速度。這些原因使得在以太坊上對智能合約的正式驗證比其他區塊鏈更難。

到目前為止，以太坊的實際合約驗證

如上所述，靜態分析可以用多種方法進行。在智能合約中，大多數都是基于模型或基于驗證的。在以太坊上介紹有前途的項目，并將注意力吸引到他們的LIM上，這可能會帶來驚人的啟示。

在以上綜述的基礎上，介紹以太坊上有前途的項目，并提請注意它們的局限性，這可能具有驚人的啟示意義。

智能合約的模型檢查表明，由于狀態組合，智能合約在實踐中不可行。基于VeriSolid?的模型提供了一個方便的界面來排列，還避免了已知安全流而構建的塊，從而強加一些屬性，并自動生成正確的Solidity 智能合約。但是，到目前為止，僅支持一組屬性，不能將 Solidity 代碼編譯為字節碼。

基于Hoare 邏輯的幾個項目尋求帶來的益處，以正式驗證其源代碼中智能合約。一些人試圖對 Solidity 代碼進行說明 ，而另一些人則選擇直接使用ML 函數式編程語言進行開發，從而獲得正確的構建程序。這種類型的努力可能會引起很多關注，因為它們會導致強大的開發人員工具和出色的經驗。

然而，應該指出的是，在Why3中實現所有可靠類型和邏輯（公共/私有函數、gas注意事項……）需要大量的工作，而且目前還沒有從Why3到EVM的可生產的完整編譯器。

研究團隊還嘗試對字節碼進行全編譯，以驗證中間表示的前期/后期樣式中的協定屬性。但更復雜的合約需要全面實施 EVM 字節碼，例如，可以這樣評估一些GAS消耗屬性。當還支持從高級語言翻譯為相同的中間表示形式時，可以驗證功能正確性，并使在兩個中間表示形式（一個來自高級代碼的編譯，另一個來自字節碼的反編譯）等效。如果沒有，由于缺乏可用的用戶反饋，這種方法不太可能幫助開發人員在實踐中驗證他們的智能合約。

目前在以太坊上可用的最完整的環境可能是K-framework。如果定義了語言的正式規范，它就可以處理各種工具的自動生成，比如解釋器和編譯器。盡管如此，這個框架要求很高（需要大量規范的手工翻譯，這很容易出錯），而且仍然存在一些缺陷（例如，主網上的EVM實現可能與機器語義不匹配）。盡管如此，已經進行了大量的工作來使這個現有的框架適應區塊鏈。

結論

隨著區塊鏈價值的增加和分散化應用程序復雜性的增加，推廣一種更嚴格的程序分析方法似乎是向客戶和合與所有者提供更高安全級別的唯一可接受的方法。

形式驗證是一門成熟的科學，可以為實現這一目標作出重大貢獻。但是，盡管一些區塊鏈的設計考慮到了這一目標，但在以太坊上驗證智能合與，尤其是那些以可靠方式編寫的合與，還遠遠不夠明顯。然而，在其他框架上，今天可以進行正式的驗證。現在要靠分散式應用程序的創建者來迎接這一挑戰，并努力為更安全的智能合約鋪平道路。