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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

合約語(yǔ)言

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

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

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

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

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

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

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

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

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

驗(yàn)證方法

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

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

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

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

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

正式的語(yǔ)義

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

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

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

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

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

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

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

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

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

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

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

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

結(jié)論

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

形式驗(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)證?，F(xiàn)在要靠分散式應(yīng)用程序的創(chuàng)建者來(lái)迎接這一挑戰(zhàn)，并努力為更安全的智能合約鋪平道路。