如何驗(yàn)證區(qū)塊鏈開發(fā)程序和驗(yàn)證程序的正確性

無bug編程是一項(xiàng)艱巨的任務(wù)，也是關(guān)鍵系統(tǒng)面臨的基本挑戰(zhàn)。為此，形式化方法提供了開發(fā)程序和驗(yàn)證程序正確性的技術(shù)。

正式核查是一項(xiàng)艱苦的工作。它要求很高，需要大量的腦力，需要大量的投資，但它已經(jīng)成為軟件行業(yè)許多領(lǐng)域的強(qiáng)制性標(biāo)準(zhǔn)。

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

但是，采用這種方式是一把雙刃劍：與以前的任何其他網(wǎng)絡(luò)相比，經(jīng)濟(jì)上都會直接受到威脅。

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

本文旨在介紹正式的驗(yàn)證，回顧區(qū)塊鏈時代的現(xiàn)有工具，并強(qiáng)調(diào)以太坊特有的挑戰(zhàn)。

正式驗(yàn)證的簡短介紹

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

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

在進(jìn)一步討論之前，應(yīng)該簡要介紹一些數(shù)學(xué)概念。

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

規(guī)范： 程序的規(guī)范是對分配給它的任務(wù)和允許用例的明確描述。指定一個程序需要抽象它的屬性，因此是一項(xiàng)困難的任務(wù)。根據(jù)規(guī)范驗(yàn)證程序?qū)崿F(xiàn)的正確性也很困難。

動態(tài)分析包括執(zhí)行代碼或模擬代碼，以發(fā)現(xiàn)任何bug。創(chuàng)建測試計(jì)劃包括列出要測試的用例，并為每個用例建立一個測試。由于這些測試不能全面，動態(tài)分析一般不能構(gòu)成正確性的證明。

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

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

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

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

總結(jié)一下，要理解正式驗(yàn)證智能合約的挑戰(zhàn)，必須牢記兩個基本概念：

1. 我們不能證明合約是明智的。我們證明了它們的一些性質(zhì)。我們根據(jù)規(guī)范證明了它們的正確性。

2. 要被認(rèn)為是有效的，必須在一個單一的、可信的邏輯框架內(nèi)生成一個證明，從規(guī)范語言級別到虛擬機(jī)執(zhí)行級別。

在構(gòu)建區(qū)塊鏈時考慮到驗(yàn)證

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

很難否認(rèn)，每個區(qū)塊鏈都是為了滿足特定的期望子集而設(shè)計(jì)的，比如快速采用或安全性。

直接的結(jié)果是，正式的驗(yàn)證在一些框架上是當(dāng)前的現(xiàn)實(shí)，而在另一些框架上可能是長期的目標(biāo)。

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

合約語言

在軟件行業(yè)，特別是在區(qū)塊鏈領(lǐng)域，區(qū)分三種類型的語言是很有幫助的：

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

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

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

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

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

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

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

由于促進(jìn)了中間代碼的正式驗(yàn)證，不同的區(qū)塊鏈框架在驗(yàn)證智能合約方面的能力出現(xiàn)了重大差異。

驗(yàn)證方法

根據(jù)前面對語言的分類，我們可以區(qū)分出三種主要的驗(yàn)證方法：

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

（II）：中間表示形式可專門設(shè)計(jì)為驗(yàn)證工具（例如證明助手）的目標(biāo)。這可以根據(jù)規(guī)范為代碼優(yōu)化和動態(tài)驗(yàn)證提供非常合適的環(huán)境。中間代碼表示形式可以來自高級合約的編譯，也可以來自低級代碼的反編譯。

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

圖2：基于與規(guī)范化比較對象的不同驗(yàn)證方法。

正式的語義

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

在大多數(shù)情況下，定義在任何級別上使用的所有語言的正式語義都是至關(guān)重要的，因?yàn)樗鼮殚_發(fā)單個可信邏輯框架提供了條件，在這個框架中，從一種形式主義到另一種形式的轉(zhuǎn)換都要經(jīng)過正式建模和驗(yàn)證。

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

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

到目前為止，以太坊的實(shí)際合約驗(yàn)證

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

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

智能合約的模型檢查表明，由于狀態(tài)組合，智能合約在實(shí)踐中不可行?；赩eriSolid?的模型提供了一個方便的界面來排列，還避免了已知安全流而構(gòu)建的塊，從而強(qiáng)加一些屬性，并自動生成正確的Solidity 智能合約。但是，到目前為止，僅支持一組屬性，不能將 Solidity 代碼編譯為字節(jié)碼。

基于Hoare 邏輯的幾個項(xiàng)目尋求帶來的益處，以正式驗(yàn)證其源代碼中智能合約。一些人試圖對 Solidity 代碼進(jìn)行說明 ，而另一些人則選擇直接使用ML 函數(shù)式編程語言進(jìn)行開發(fā)，從而獲得正確的構(gòu)建程序。這種類型的努力可能會引起很多關(guān)注，因?yàn)樗鼈儠?dǎo)致強(qiáng)大的開發(fā)人員工具和出色的經(jīng)驗(yàn)。

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

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

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

結(jié)論

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

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